# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1273586326 -3600
# Node ID e08e3c29dbc0d5d3d235cf676c671bd8322ec8a1
# Parent  200954544cae6b1d870e458b7ac0805d6edb9f98
a bit for the introduction of the q-paper

diff -r 200954544cae -r e08e3c29dbc0 Nominal/Ex/Test.thy
--- a/Nominal/Ex/Test.thy	Tue May 11 12:18:26 2010 +0100
+++ b/Nominal/Ex/Test.thy	Tue May 11 14:58:46 2010 +0100
@@ -10,12 +10,16 @@
 (* example 4 from Terms.thy *)
 (* fv_eqvt does not work, we need to repaire defined permute functions
    defined fv and defined alpha... *)
-(* lists-datastructure does not work yet
-nominal_datatype trm4 =
-  Vr4 "name"
-| Ap4 "trm4" "trm4 list"
-| Lm4 x::"name" t::"trm4"  bind x in t
+(* lists-datastructure does not work yet *)
 
+(*
+nominal_datatype trm =
+  Vr "name"
+| Ap "trm" "trm list"
+| Lm x::"name" t::"trm"  bind x in t
+*)
+
+(*
 thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]
 thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]
 *)
diff -r 200954544cae -r e08e3c29dbc0 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Tue May 11 12:18:26 2010 +0100
+++ b/Quotient-Paper/Paper.thy	Tue May 11 14:58:46 2010 +0100
@@ -12,6 +12,9 @@
 section {* Introduction *}
 
 text {* 
+  {\hfill quote by Larry}\bigskip
+
+  \noindent
   Isabelle is a generic theorem prover in which many logics can be implemented. 
   The most widely used one, however, is
   Higher-Order Logic (HOL). This logic consists of a small number of 
@@ -27,10 +30,40 @@
   @{text [display] "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 - n \<^isub>2 = m\<^isub>1 - m \<^isub>2"}
 
   \noindent
-  The problem is that one 
+  Similarly one can construct the type of finite sets by quotienting lists
+  according to the equivalence relation
+
+  @{text [display] "xs \<approx> ys \<equiv> (\<forall>x. x \<in> xs \<longleftrightarrow> x \<in> ys)"}
+
+  \noindent
+  where @{text "\<in>"} stands for membership in a list.
+
+  The problem is that in order to start reasoning about, for example integers, 
+  definitions and theorems need to be transferred, or \emph{lifted}, 
+  from the ``raw'' type @{typ "nat \<times> nat"} to the quotient type @{typ int}. 
+  This lifting usually requires a lot of tedious reasoning effort.
+  The purpose of a \emph{quotient package} is to ease the lifting and automate
+  the reasoning involved as much as possible. Such a package is a central
+  component of the new version of Nominal Isabelle where representations 
+  of alpha-equated terms are constructed according to specifications given by
+  the user. 
   
+  In the context of HOL, there have been several quotient packages (...). The
+  most notable is the one by Homeier (...) implemented in HOL4. However, what is
+  surprising, none of them can deal compositions of quotients, for example with 
+  lifting theorems about @{text "concat"}:
 
+  @{text [display] "concat definition"}
+  
+  \noindent
+  One would like to lift this definition to the operation
+  
+  @{text [display] "union definition"}
 
+  \noindent
+  What is special about this operation is that we have as input
+  lists of lists which after lifting turn into finite sets of finite
+  sets. 
 *}
 
 subsection {* Contributions *}