--- 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 *}