# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1275715582 -7200
# Node ID b0b2198040d731fb6f4769640f2d7aef44b3863b
# Parent  ea7c3f21d6df3be9524a92076fedf871d15bc4c2
qpaper

diff -r ea7c3f21d6df -r b0b2198040d7 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Wed Jun 02 14:24:16 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Sat Jun 05 07:26:22 2010 +0200
@@ -1,3 +1,4 @@
+(* How to change the notation for \<lbrakk> \<rbrakk> meta-level implications? *)
 
 (*<*)
 theory Paper
@@ -6,12 +7,18 @@
         "../Nominal/FSet"
 begin
 
+print_syntax
+
 notation (latex output)
   rel_conj ("_ OOO _" [53, 53] 52)
 and
-  fun_map ("_ ---> _" [51, 51] 50)
+  "op -->" (infix "\<rightarrow>" 100)
+and
+  "==>" (infix "\<Rightarrow>" 100)
 and
-  fun_rel ("_ ===> _" [51, 51] 50)
+  fun_map (infix "\<longrightarrow>" 51)
+and
+  fun_rel (infix "\<Longrightarrow>" 51)
 and
   list_eq (infix "\<approx>" 50) (* Not sure if we want this notation...? *)
 
@@ -208,8 +215,8 @@
   \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\<rightarrow>\<sigma>\<^isub>2,\<tau>\<^isub>1\<rightarrow>\<tau>\<^isub>2)"}  =  @{text "REP(\<sigma>\<^isub>1,\<tau>\<^isub>1) \<longrightarrow> 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) \<longrightarrow> 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"}
@@ -217,8 +224,9 @@
   \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:
+  in Homeier's HOL package. Adding composition in last two cases is necessary
+  for compositional quotients. We ilustrate the different behaviour of the
+  definition by showing the derived definition of @{term fconcat}:
 
   @{thm fconcat_def[no_vars]}
 
@@ -247,7 +255,7 @@
   @{thm [display] append_rsp[no_vars]}
 
   \noindent
-  Which after unfolding @{term "op ===>"} is equivalent to:
+  Which after unfolding @{term "op \<Longrightarrow>"} is equivalent to:
 
   @{thm [display] append_rsp_unfolded[no_vars]}
 
@@ -363,7 +371,7 @@
   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 as all three
+  theorem and the goal. We then show the 3 proofs, as all three
   can be performed independently from each other.
 
 *}
@@ -418,10 +426,46 @@
 
 *}
 
-subsection {* Proof of Regularization *}
+subsection {* Proof procedure *}
+
+(* In the below the type-guiding 'QuotTrue' assumption is removed; since we
+   present in a paper a version with typed-variables it is not necessary *)
 
 text {*
-  Example of non-regularizable theorem ($0 = 1$).
+
+  With the above definitions of @{text "REG"} and @{text "INJ"} we can show
+  how the proof is performed. The first step is always the application of
+  of the following lemma:
+
+  @{term "[|A; A --> B; B = C; C = D|] ==> D"}
+
+  With @{text A} instantiated to the original raw theorem, 
+       @{text B} instantiated to @{text "REG(A)"},
+       @{text C} instantiated to @{text "INJ(REG(A))"},
+   and @{text D} instantiated to the statement of the lifted theorem.
+  The first assumption can be immediately discharged using the original
+  theorem and the three left subgoals are exactly the subgoals of regularization,
+  injection and cleaning. The three can be proved independently by the
+  framework and in case there are non-solved subgoals they can be left
+  to the user.
+
+  The injection and cleaning subgoals are always solved if the appropriate
+  respectfulness and preservation theorems are given. It is not the case
+  with regularization; sometimes a theorem given by the user does not
+  imply a regularized version and a stronger one needs to be proved. This
+  is outside of the scope of the quotient package, so the user is then left
+  with such obligations. As an example lets see the simplest possible
+  non-liftable theorem for integers: When we want to prove @{term "0 \<noteq> 1"}
+  on integers the fact that @{term "\<not> (0, 0) = (1, 0)"} is not enough. It
+  only shows that particular items in the equivalence classes are not equal,
+  a more general statement saying that the classes are not equal is necessary.
+*}
+
+subsection {* Proving Regularization *}
+
+text {*
+  Isabelle provides 
+
 
 
   Separtion of regularization from injection thanks to the following 2 lemmas: