diff -r 7f8b5ff303f4 -r 7f1ce97635fc QuotMain.thy
--- a/QuotMain.thy	Wed Nov 25 14:15:34 2009 +0100
+++ b/QuotMain.thy	Wed Nov 25 14:16:33 2009 +0100
@@ -604,8 +604,28 @@
 
 
 ML {*
-(* builds the relation for respects *)
+(*
+Regularizing an rtrm means:
+ - quantifiers over a type that needs lifting are replaced by
+   bounded quantifiers, for example:
+      \<forall>x. P     \<Longrightarrow>     \<forall>x \<in> (Respects R). P  /  All (Respects R) P
+
+   the relation R is given by the rty and qty;
  
+ - abstractions over a type that needs lifting are replaced
+   by bounded abstractions:
+      \<lambda>x. P     \<Longrightarrow>     Ball (Respects R) (\<lambda>x. P)
+
+ - equalities over the type being lifted are replaced by
+   corresponding relations:
+      A = B     \<Longrightarrow>     A \<approx> B
+
+   example with more complicated types of A, B:
+      A = B     \<Longrightarrow>     (op = \<Longrightarrow> op \<approx>) A B
+*)
+
+
+(* builds the relation that is the argument of respects *)
 fun mk_resp_arg lthy (rty, qty) =
 let
   val thy = ProofContext.theory_of lthy
@@ -660,26 +680,6 @@
 fun qnt_typ ty = domain_type (domain_type ty)  
 *}
 
-(*
-Regularizing an rtrm means:
- - quantifiers over a type that needs lifting are replaced by
-   bounded quantifiers, for example:
-      \<forall>x. P     \<Longrightarrow>     \<forall>x \<in> (Respects R). P  /  All (Respects R) P
-
-   the relation R is given by the rty and qty;
- 
- - abstractions over a type that needs lifting are replaced
-   by bounded abstractions:
-      \<lambda>x. P     \<Longrightarrow>     Ball (Respects R) (\<lambda>x. P)
-
- - equalities over the type being lifted are replaced by
-   corresponding relations:
-      A = B     \<Longrightarrow>     A \<approx> B
-
-   example with more complicated types of A, B:
-      A = B     \<Longrightarrow>     (op = \<Longrightarrow> op \<approx>) A B
-*)
-
 ML {*
 (* produces a regularized version of rtm      *)
 (* - the result is still not completely typed *)
@@ -746,8 +746,8 @@
 *}
 
 (*
-To prove that the old theorem implies the new one, we first
-atomize it and then try:
+To prove that the raw theorem implies the regularised one, 
+we try in order:
 
  - Reflexivity of the relation
  - Assumption
@@ -835,16 +835,28 @@
 *}
 
 ML {*
-fun REGULARIZE_prove rtrm qtrm rel_eqv rel_refl lthy =
-  let
-    val goal = mk_REGULARIZE_goal lthy rtrm qtrm
-  in
-    Goal.prove lthy [] [] goal 
-      (fn {context, ...} => REGULARIZE_tac' context rel_refl rel_eqv)
-  end
+fun regularize_tac ctxt rel_eqv rel_refl =
+  (ObjectLogic.full_atomize_tac) THEN'
+  REPEAT_ALL_NEW (FIRST' [
+    rtac rel_refl,
+    atac,
+    rtac @{thm universal_twice},
+    (rtac @{thm impI} THEN' atac),
+    rtac @{thm implication_twice},
+    EqSubst.eqsubst_tac ctxt [0]
+      [(@{thm equiv_res_forall} OF [rel_eqv]),
+       (@{thm equiv_res_exists} OF [rel_eqv])],
+    (* For a = b \<longrightarrow> a \<approx> b *)
+    (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
+    (rtac @{thm RIGHT_RES_FORALL_REGULAR})
+  ]);
 *}
 
+
 (*
+Injections of REP and Abses
+***************************
+
 Injecting REPABS means:
 
   For abstractions:
@@ -866,15 +878,12 @@
   * Otherwise just recurse.
 *)
 
-(* rep-abs injection *)
-
 ML {*
 fun mk_repabs lthy (T, T') trm = 
   Quotient_Def.get_fun repF lthy (T, T') 
     $ (Quotient_Def.get_fun absF lthy (T, T') $ trm)
 *}
 
-
 ML {*
 (* bound variables need to be treated properly,  *)
 (* as the type of subterms need to be calculated *)
@@ -939,35 +948,7 @@
 *}
 
 
-
-(*
-To prove that the old theorem implies the new one, we first
-atomize it and then try:
- - Reflexivity of the relation
- - Assumption
- - Elimnating quantifiers on both sides of toplevel implication
- - Simplifying implications on both sides of toplevel implication
- - Ball (Respects ?E) ?P = All ?P
- - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q
-*)
-
-ML {*
-fun regularize_tac ctxt rel_eqv rel_refl =
-  (ObjectLogic.full_atomize_tac) THEN'
-  REPEAT_ALL_NEW (FIRST' [
-    rtac rel_refl,
-    atac,
-    rtac @{thm universal_twice},
-    (rtac @{thm impI} THEN' atac),
-    rtac @{thm implication_twice},
-    EqSubst.eqsubst_tac ctxt [0]
-      [(@{thm equiv_res_forall} OF [rel_eqv]),
-       (@{thm equiv_res_exists} OF [rel_eqv])],
-    (* For a = b \<longrightarrow> a \<approx> b *)
-    (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
-    (rtac @{thm RIGHT_RES_FORALL_REGULAR})
-  ]);
-*}
+(* Genralisation of free variables in a goal *)
 
 ML {*
 fun inst_spec ctrm =
@@ -999,6 +980,18 @@
   end)  
 *}
 
+(* General outline of the lifting procedure *)
+(* **************************************** *)
+(*                                          *)
+(* - A is the original raw theorem          *)
+(* - B is the regularized theorem           *)
+(* - C is the rep/abs injected version of B *) 
+(* - D is the lifted theorem                *)
+(*                                          *)
+(* - b is the regularization step           *)
+(* - c is the rep/abs injection step        *)
+(* - d is the cleaning part                 *)
+
 lemma procedure:
   assumes a: "A"
   and     b: "A \<Longrightarrow> B"
@@ -1026,10 +1019,12 @@
   val thy = ProofContext.theory_of ctxt
   val rtrm' = HOLogic.dest_Trueprop rtrm
   val qtrm' = HOLogic.dest_Trueprop qtrm
-  val reg_goal = Syntax.check_term ctxt (REGULARIZE_trm ctxt rtrm' qtrm')
-                 handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm
-  val inj_goal = Syntax.check_term ctxt (inj_REPABS ctxt (reg_goal, qtrm'))
-                 handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm
+  val reg_goal = 
+        Syntax.check_term ctxt (REGULARIZE_trm ctxt rtrm' qtrm')
+        handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm
+  val inj_goal = 
+        Syntax.check_term ctxt (inj_REPABS ctxt (reg_goal, qtrm'))
+        handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm
 in
   Drule.instantiate' []
     [SOME (cterm_of thy rtrm'),