diff -r c6db12ddb60c -r c785fff02a8f Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Thu May 27 18:37:52 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Thu May 27 18:40:10 2010 +0200
@@ -1,7 +1,9 @@
+
 (*<*)
 theory Paper
 imports "Quotient"
         "LaTeXsugar"
+        "../Nominal/FSet"
 begin
 
 notation (latex output)
@@ -10,6 +12,8 @@
   fun_map ("_ ---> _" [51, 51] 50)
 and
   fun_rel ("_ ===> _" [51, 51] 50)
+and
+  list_eq (infix "\<approx>" 50) (* Not sure if we want this notation...? *)
 
 ML {*
 fun nth_conj n (_, r) = nth (HOLogic.dest_conj r) n;
@@ -75,18 +79,19 @@
   surprising, none of them can deal compositions of quotients, for example with 
   lifting theorems about @{text "concat"}:
 
-  @{thm concat.simps(1)}\\
-  @{thm concat.simps(2)[no_vars]}
+  @{thm [display] concat.simps(1)}
+  @{thm [display] concat.simps(2)[no_vars]}
 
   \noindent
-  One would like to lift this definition to the operation
-  
-  @{text [display] "union definition"}
+  One would like to lift this definition to the operation:
+
+  @{thm [display] fconcat_empty[no_vars]}
+  @{thm [display] fconcat_insert[no_vars]}
 
   \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. 
+  sets.
 *}
 
 subsection {* Contributions *}
@@ -101,7 +106,7 @@
   \item We define quotient composition, function map composition and
     relation map composition. This lets lifting polymorphic types with
     subtypes quotiented as well. We extend the notions of
-    respectfullness and preservation to cope with quotient
+    respectfulness and preservation to cope with quotient
     composition.
 
   \item We allow lifting only some occurrences of quotiented
@@ -140,8 +145,8 @@
 
   \end{definition}
 
-  \begin{definition}[Relation map and function map]
-  @{thm fun_rel_def[no_vars]}\\
+  \begin{definition}[Relation map and function map]\\
+  @{thm fun_rel_def[of "R1" "R2", no_vars]}\\
   @{thm fun_map_def[no_vars]}
   \end{definition}
 
@@ -153,75 +158,303 @@
 
 *}
 
-section {* Constants *}
-
-(* Describe what containers are? *)
+subsection {* Higher Order Logic *}
 
 text {*
-  \begin{definition}[Composition of Relations]
-  @{abbrev "rel_conj R1 R2"}
-  \end{definition}
+
+  Types:
+  \begin{eqnarray}\nonumber
+  @{text "\<sigma> ::="} & @{text "\<alpha>"} & \textrm{(type variable)} \\ \nonumber
+      @{text "|"} & @{text "(\<sigma>,\<dots>,\<sigma>)\<kappa>"} & \textrm{(type construction)}
+  \end{eqnarray}
+
+  Terms:
+  \begin{eqnarray}\nonumber
+  @{text "t ::="} & @{text "x\<^isup>\<sigma>"} & \textrm{(variable)} \\ \nonumber
+      @{text "|"} & @{text "c\<^isup>\<sigma>"} & \textrm{(constant)} \\ \nonumber
+      @{text "|"} & @{text "t t"} & \textrm{(application)} \\ \nonumber
+      @{text "|"} & @{text "\<lambda>x\<^isup>\<sigma>. t"} & \textrm{(abstraction)} \\ \nonumber
+  \end{eqnarray}
+
+*}
 
-  The first operation that we describe is the generation of
-  aggregate Abs or Rep function for two given compound types.
-  This operation will be used for the constant defnitions
-  and for the translation of theorems statements. It relies on
-  knowing map functions and relation functions for container types.
-  It follows the following algorithm:
+section {* Constants *}
+
+(* Say more about containers? *)
+
+text {*
+
+  To define a constant on the lifted type, an aggregate abstraction
+  function is applied to the raw constant. Below we describe the operation
+  that generates
+  an aggregate @{term "Abs"} or @{term "Rep"} function given the
+  compound raw type and the compound quotient type.
+  This operation will also be used in translations of theorem statements
+  and in the lifting procedure.
+
+  The operation is additionally able to descend into types for which
+  maps are known. Such maps for most common types (list, pair, sum,
+  option, \ldots) are described in Homeier, and we assume that @{text "map"}
+  is the function that returns a map for a given type. Then REP/ABS is defined
+  as follows:
 
   \begin{itemize}
-  \item For equal types or free type variables return identity.
-
-  \item For function types recurse, change the Rep/Abs flag to
-     the opposite one for the domain type and compose the
-     results with @{term "fun_map"}.
-
-  \item For equal type constructors use the appropriate map function
-     applied to the results for the arguments.
-
-  \item For unequal type constructors are unequal, we look in the
-    quotients information for a raw type quotient type pair that
-    matches the given types. We apply the environment to the arguments
-    and recurse composing it with the aggregate map function.
+  \item @{text "ABS(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} = @{text "id"}
+  \item @{text "REP(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"}  =  @{text "id"}
+  \item @{text "ABS(\<sigma>, \<sigma>)"}  =  @{text "id"}
+  \item @{text "REP(\<sigma>, \<sigma>)"}  =  @{text "id"}
+  \item @{text "ABS(\<sigma>\<^isub>1\<rightarrow>\<sigma>\<^isub>2,\<tau>\<^isub>1\<rightarrow>\<tau>\<^isub>2)"}  =  @{text "REP(\<sigma>\<^isub>1,\<tau>\<^isub>1) ---> ABS(\<sigma>\<^isub>2,\<tau>\<^isub>2)"}
+  \item @{text "REP(\<sigma>\<^isub>1\<rightarrow>\<sigma>\<^isub>2,\<tau>\<^isub>1\<rightarrow>\<tau>\<^isub>2)"}  =  @{text "ABS(\<sigma>\<^isub>1,\<tau>\<^isub>1) ---> REP(\<sigma>\<^isub>2,\<tau>\<^isub>2)"}
+  \item @{text "ABS((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"}  =  @{text "(map \<kappa>) (ABS(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (ABS(\<sigma>\<^isub>n,\<tau>\<^isub>n))"}
+  \item @{text "REP((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"}  =  @{text "(map \<kappa>) (REP(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (REP(\<sigma>\<^isub>n,\<tau>\<^isub>n))"}
+  \item @{text "ABS((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"}  =  @{text "Abs_\<kappa>\<^isub>2 \<circ> (map \<kappa>\<^isub>1) (ABS(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (ABS(\<rho>\<^isub>p,\<nu>\<^isub>p)"} provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"}
+  \item @{text "REP((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"}  =  @{text "(map \<kappa>\<^isub>1) (REP(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (REP(\<rho>\<^isub>p,\<nu>\<^isub>p) \<circ> Rep_\<kappa>\<^isub>2"} provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"}
   \end{itemize}
 
+  Apart from the last 2 points the definition is same as the one implemented in
+  in Homeier's HOL package, below is the definition of @{term fconcat}
+  that shows the last points:
 
+  @{thm fconcat_def[no_vars]}
+
+  The aggregate @{term Abs} function takes a finite set of finite sets
+  and applies @{term "map rep_fset"} composed with @{term rep_fset} to
+  its input, obtaining a list of lists, passes the result to @{term concat}
+  obtaining a list and applies @{term abs_fset} obtaining the composed
+  finite set.
+*}
+
+subsection {* Respectfulness *}
+
+text {*
+
+  A respectfulness lemma for a constant states that the equivalence
+  class returned by this constant depends only on the equivalence
+  classes of the arguments applied to the constant. This can be
+  expressed in terms of an aggregate relation between the constant
+  and itself, for example the respectfullness for @{term "append"}
+  can be stated as:
+
+  @{thm [display] append_rsp[no_vars]}
+
+  \noindent
+  Which is equivalent to:
+
+  @{thm [display] append_rsp_unfolded[no_vars]}
+
+  Below we show the algorithm for finding the aggregate relation.
+  This algorithm uses
+  the relation composition which we define as:
+
+  \begin{definition}[Composition of Relations]
+  @{abbrev "rel_conj R1 R2"} where @{text OO} is the predicate
+  composition @{thm pred_compI[no_vars]}
+  \end{definition}
+
+  Given an aggregate raw type and quotient type:
+
+  \begin{itemize}
+  \item For equal types or free type variables return equality
+
+  \item For equal type constructors use the appropriate rel
+    function applied to the results for the argument pairs
+
+  \item For unequal type constructors, look in the quotients information
+    for a quotient type that matches the type constructor, and instantiate
+    the type appropriately getting back an instantiation environment. We
+    apply the environment to the arguments and recurse composing it with
+    the aggregate relation function.
+
+  \end{itemize}
+
+  Again, the the behaviour of our algorithm in the last situation is
+  novel, so lets look at the example of respectfullness for @{term concat}.
+  The statement as computed by the algorithm above is:
 
-  Rsp and Prs
+  @{thm [display] concat_rsp[no_vars]}
+
+  \noindent
+  By unfolding the definition of relation composition and relation map
+  we can see the equivalent statement just using the primitive list
+  equivalence relation:
+
+  @{thm [display] concat_rsp_unfolded[of "a" "a'" "b'" "b", no_vars]}
+
+  The statement reads that, for any lists of lists @{term a} and @{term b}
+  if there exist intermediate lists of lists @{term "a'"} and @{term "b'"}
+  such that each element of @{term a} is in the relation with an appropriate
+  element of @{term a'}, @{term a'} is in relation with @{term b'} and each
+  element of @{term b'} is in relation with the appropriate element of
+  @{term b}.
+
 *}
 
+subsection {* Preservation *}
+
+text {*
+  To be able to lift theorems that talk about constants that are not
+  lifted but whose type changes when lifting is performed additionally
+  preservation theorems are needed.
+
+  To lift theorems that talk about insertion in lists of lifted types
+  we need to know that for any quotient type with the abstraction and
+  representation functions @{text "Abs"} and @{text Rep} we have:
+
+  @{thm [display] (concl) cons_prs[no_vars]}
+
+  This is not enough to lift theorems that talk about quotient compositions.
+  For some constants (for example empty list) it is possible to show a
+  general compositional theorem, but for @{term "op #"} it is necessary
+  to show that it respects the particular quotient type:
+
+  @{thm [display] insert_preserve2[no_vars]}
+*}
+
+subsection {* Composition of Quotient theorems *}
+
+text {*
+  Given two quotients, one of which quotients a container, and the
+  other quotients the type in the container, we can write the
+  composition of those quotients. To compose two quotient theorems
+  we compose the relations with relation composition
+  and the abstraction and relation functions with function composition.
+  The @{term "Rep"} and @{term "Abs"} functions that we obtain are
+  the same as the ones created by in the aggregate functions and the
+  relation is the same as the one given by aggregate relations.
+  This becomes especially interesting
+  when we compose the quotient with itself, as there is no simple
+  intermediate step.
+
+  Lets take again the example of @{term concat}. To be able to lift
+  theorems that talk about it we will first prove the composition
+  quotient theorems, which then lets us perform the lifting procedure
+  in an unchanged way:
+
+  @{thm [display] quotient_compose_list[no_vars]}
+*}
+
+
 section {* Lifting Theorems *}
 
-text {* TBD *}
+text {*
+  The core of the quotient package takes an original theorem that
+  talks about the raw types, and the statement of the theorem that
+  it is supposed to produce. This is different from other existing
+  quotient packages, where only the raw theorems was necessary.
+  We notice that in some cases only some occurrences of the raw
+  types need to be lifted. This is for example the case in the
+  new Nominal package, where a raw datatype that talks about
+  pairs of natural numbers or strings (being lists of characters)
+  should not be changed to a quotient datatype with constructors
+  taking integers or finite sets of characters. To simplify the
+  use of the quotient package we additionally provide an automated
+  statement translation mechanism that replaces occurrences of
+  types that match given quotients by appropriate lifted types.
 
-text {* Why providing a statement to prove is necessary is some cases *}
+  Lifting the theorems is performed in three steps. In the following
+  we call these steps \emph{regularization}, \emph{injection} and
+  \emph{cleaning} following the names used in Homeier's HOL
+  implementation.
 
-subsection {* Regularization *}
+  We first define the statement of the regularized theorem based
+  on the original theorem and the goal theorem. Then we define
+  the statement of the injected theorem, based on the regularized
+  theorem and the goal. We then show the 3 proofs, and all three
+  can be performed independently from each other.
+
+*}
+
+subsection {* Regularization and Injection statements *}
 
 text {*
-Transformation of the theorem statement:
-\begin{itemize}
-\item Quantifiers and abstractions involving raw types replaced by bounded ones.
-\item Equalities involving raw types replaced by bounded ones.
-\end{itemize}
+
+  The function that gives the statement of the regularized theorem
+  takes the statement of the raw theorem (a term) and the statement
+  of the lifted theorem. The intuition behind the procedure is that
+  it replaces quantifiers and abstractions involving raw types
+  by bounded ones, and equalities involving raw types are replaced
+  by appropriate aggregate relations. It is defined as follows:
 
-The procedure.
+  \begin{itemize}
+  \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<sigma>. s) = \<lambda>x : \<sigma>. REG (t, s)"}
+  \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<tau>. s) = \<lambda>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}
+  \item @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<sigma>. s) = \<forall>x : \<sigma>. REG (t, s)"}
+  \item @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s) = \<forall>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}
+  \item @{text "REG ((op =) : \<sigma>, (op =) : \<sigma>) = (op =) : \<sigma>"}
+  \item @{text "REG ((op =) : \<sigma>, (op =) : \<tau>) = REL (\<sigma>, \<tau>) : \<sigma>"}
+  \item @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) = REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}
+  \item @{text "REG (v\<^isub>1, v\<^isub>2) = v\<^isub>1"}
+  \item @{text "REG (c\<^isub>1, c\<^isub>2) = c\<^isub>1"}
+  \end{itemize}
+
+  Existential quantifiers and unique existential quantifiers are defined
+  similarily to the universal one.
+
+  The function that gives the statment of the injected theorem
+  takes the statement of the regularized theorems and the statement
+  of the lifted theorem both as terms.
 
-Example of non-regularizable theorem ($0 = 1$).
+  \begin{itemize}
+  \item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<sigma>) = \<lambda>x. (INJ (t, s)"}
+  \item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x. (INJ (t, s))))"}
+  \item @{text "INJ ((\<lambda>x \<in> R. t) : \<sigma>, (\<lambda>x. s) : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x \<in> R. (INJ (t, s))))"}
+  \item @{text "INJ (\<forall> t, \<forall> s) = \<forall> (INJ (t, s)"}
+  \item @{text "INJ (\<forall> t \<in> R, \<forall> s) = \<forall> (INJ (t, s) \<in> R"}
+  \item @{text "INJ (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) = INJ (t\<^isub>1, s\<^isub>1) INJ (t\<^isub>2, s\<^isub>2)"}
+  \item @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<sigma>) = v\<^isub>1"}
+  \item @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (v\<^isub>1))"}
+  \item @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<sigma>) = c\<^isub>1"}
+  \item @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (c\<^isub>1))"}
+  \end{itemize}
+
+  For existential quantifiers and unique existential quantifiers it is
+  defined similarily to the universal one.
+
+*}
+
+subsection {* Proof of Regularization *}
 
-Separtion of regularization from injection thanks to the following 2 lemmas:
-\begin{lemma}
-If @{term R2} is an equivalence relation, then:
-\begin{eqnarray}
-@{thm (rhs) ball_reg_eqv_range[no_vars]} & = & @{thm (lhs) ball_reg_eqv_range[no_vars]}\\
-@{thm (rhs) bex_reg_eqv_range[no_vars]} & = & @{thm (lhs) bex_reg_eqv_range[no_vars]}
-\end{eqnarray}
-\end{lemma}
+text {*
+  Example of non-regularizable theorem ($0 = 1$).
+
+
+  Separtion of regularization from injection thanks to the following 2 lemmas:
+  \begin{lemma}
+  If @{term R2} is an equivalence relation, then:
+  \begin{eqnarray}
+  @{thm (rhs) ball_reg_eqv_range[no_vars]} & = & @{thm (lhs) ball_reg_eqv_range[no_vars]}\\
+  @{thm (rhs) bex_reg_eqv_range[no_vars]} & = & @{thm (lhs) bex_reg_eqv_range[no_vars]}
+  \end{eqnarray}
+  \end{lemma}
+
+  Other lemmas used in regularization:
+  @{thm [display] ball_reg_eqv[no_vars]}
+  @{thm [display] bex_reg_eqv[no_vars]}
+  @{thm [display] babs_reg_eqv[no_vars]}
+  @{thm [display] babs_simp[no_vars]}
+
+  @{thm [display] ball_reg_right[no_vars]}
+  @{thm [display] bex_reg_left[no_vars]}
+  @{thm [display] bex1_bexeq_reg[no_vars]}
 
 *}
 
 subsection {* Injection *}
 
+text {*
+
+  The 2 key lemmas are:
+
+  @{thm [display] apply_rsp[no_vars]}
+  @{thm [display] rep_abs_rsp[no_vars]}
+
+
+
+*}
+
+
+
+
 subsection {* Cleaning *}
 
 text {* Preservation of quantifiers, abstractions, relations, quotient-constants