# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1274977842 -7200
# Node ID 4d8d9b8af76fd8489bb52fd40511a353b56d5c81
# Parent  31f1ec832d39ba3134eea335d9c27b1549ab5a5d# Parent  6ce64fb5cbd96364fa0de39605f5e0bf218b7217
merged

diff -r 31f1ec832d39 -r 4d8d9b8af76f Nominal/FSet.thy
--- a/Nominal/FSet.thy	Thu May 27 18:30:26 2010 +0200
+++ b/Nominal/FSet.thy	Thu May 27 18:30:42 2010 +0200
@@ -626,6 +626,11 @@
   apply auto
   done
 
+lemma insert_preserve2:
+  shows "((rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op #) =
+         (id ---> rep_fset ---> abs_fset) op #"
+  by (simp add: expand_fun_eq abs_o_rep[OF Quotient_fset] map_id Quotient_abs_rep[OF Quotient_fset])
+
 lemma [quot_preserve]:
   "(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op # = finsert"
   by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset]
diff -r 31f1ec832d39 -r 4d8d9b8af76f Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Thu May 27 18:30:26 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Thu May 27 18:30:42 2010 +0200
@@ -295,6 +295,19 @@
   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 *}
@@ -341,36 +354,106 @@
   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. The three steps are independent from each other.
+  implementation.
+
+  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 {*
+
+  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:
+
+  \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.
+
+  \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 *}
+
+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 {* Regularization *}
-
-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 procedure.
-
-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}
 
-*}
-
-subsection {* Injection *}
 
 subsection {* Cleaning *}