
diff -r bb5d3278f02e -r ec37a279ca55 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Mon Dec 07 21:54:14 2009 +0100
+++ b/Quot/QuotMain.thy	Mon Dec 07 23:45:51 2009 +0100
@@ -144,9 +144,10 @@
 
 declare [[map * = (prod_fun, prod_rel)]]
 declare [[map "fun" = (fun_map, fun_rel)]]
-(* FIXME: This should throw an exception:
-declare [[map "option" = (bla, blu)]]
-*)
+
+(* FIXME: This should throw an exception: *)
+(* declare [[map "option" = (bla, blu)]] *)
+
 
 (* identity quotient is not here as it has to be applied first *)
 lemmas [quotient_thm] =
@@ -294,7 +295,7 @@
    | _ => false
 *}
 
-section {* Regularization *} 
+section {* Computation of the Regularize Goal *} 
 
 (*
 Regularizing an rtrm means:
@@ -461,6 +462,8 @@
        raise (LIFT_MATCH "regularize (default)")
 *}
 
+section {* Regularize Tactic *}
+
 ML {*
 fun equiv_tac ctxt =
   (K (print_tac "equiv tac")) THEN'
@@ -532,20 +535,23 @@
   shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
 by (simp add: equivp_reflp)
 
-(* FIXME/TODO: How does regularizing work? *)
-(* FIXME/TODO: needs to be adapted
 
-To prove that the raw theorem implies the regularised one, 
-we try in order:
+(* Regularize Tactic *)
 
- - 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
+(* 0. preliminary simplification step according to *)
+thm ball_reg_eqv bex_reg_eqv babs_reg_eqv (* the latter of no use *)
+    ball_reg_eqv_range bex_reg_eqv_range
+(* 1. eliminating simple Ball/Bex instances*)
+thm ball_reg_right bex_reg_left
+(* 2. monos *)
+(* 3. commutation rules for ball and bex *)
+thm ball_all_comm bex_ex_comm
+(* 4. then rel-equality (which need to be instantiated to avoid loops *)
+thm eq_imp_rel
+(* 5. then simplification like 0 *)
+(* finally jump back to 1 *)
 
-*)
+
 ML {*
 fun regularize_tac ctxt =
 let
@@ -558,24 +564,19 @@
                        addsimprocs [simproc] addSolver equiv_solver
   (* TODO: Make sure that there are no list_rel, pair_rel etc involved *)
   (* can this cause loops in equiv_tac ? *)
-  val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt)
+  val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt)
 in
   simp_tac simpset THEN'
   REPEAT_ALL_NEW (CHANGED o FIRST' [
-    rtac @{thm ball_reg_right},
-    rtac @{thm bex_reg_left},
+    resolve_tac @{thms ball_reg_right bex_reg_left},
     resolve_tac (Inductive.get_monos ctxt),
-    rtac @{thm ball_all_comm},
-    rtac @{thm bex_ex_comm},
+    resolve_tac @{thms ball_all_comm bex_ex_comm},
     resolve_tac eq_eqvs,  
-    (* should be equivalent to the above, but causes loops:   *) 
-    (* rtac @{thm eq_imp_rel} THEN' SOLVES' (equiv_tac ctxt), *)
-    (* the culprit is aslread rtac @{thm eq_imp_rel}          *)
     simp_tac simpset])
 end
 *}
 
-section {* Injections of rep and abses *}
+section {* Calculation of the Injected Goal *}
 
 (*
 Injecting repabs means:
@@ -658,7 +659,7 @@
   | _ => raise (LIFT_MATCH "injection")
 *}
 
-section {* RepAbs Injection Tactic *}
+section {* Injection Tactic *}
 
 ML {*
 fun quotient_tac ctxt =
@@ -949,8 +950,8 @@
 ML {*
 fun inj_repabs_tac ctxt =
 let
-  val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) (equiv_rules_get ctxt)
-  val trans2 = map (fn x => @{thm equals_rsp} OF [x]) (quotient_rules_get ctxt)
+  val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt)
+  val trans2 = map (OF1 @{thm equals_rsp}) (quotient_rules_get ctxt)
 in
   inj_repabs_step_tac ctxt rel_refl trans2
 end
@@ -1043,29 +1044,14 @@
 fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)
 *}
 
-(*
- Cleaning the theorem consists of three rewriting steps.
- The first two need to be done before fun_map is unfolded
-
- 1) lambda_prs:
-     (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))  ---->  f
-
-    Implemented as conversion since it is not a pattern.
-
- 2) all_prs (the same for exists):
-     Ball (Respects R) ((abs ---> id) f)  ---->  All f
-
-    Rewriting with definitions from the argument defs
-     (rep ---> abs) oldConst ----> newconst
-
- 3) Quotient_rel_rep:
-      Rel (Rep x) (Rep y)  ---->  x = y
-
-    Quotient_abs_rep:
-      Abs (Rep x)  ---->  x
-
-    id_simps; fun_map.simps
-*)
+(* 1. conversion (is not a pattern) *)
+thm lambda_prs
+(* 2. folding of definitions: (rep ---> abs) oldConst == newconst *)
+(*    and simplification with                                     *)
+thm all_prs ex_prs 
+(* 3. simplification with *)
+thm fun_map.simps id_simps Quotient_abs_rep Quotient_rel_rep
+(* 4. Test for refl *)
 
 ML {*
 fun clean_tac lthy =
@@ -1085,7 +1071,7 @@
   end
 *}
 
-section {* Genralisation of free variables in a goal *}
+section {* Tactic for genralisation of free variables in a goal *}
 
 ML {*
 fun inst_spec ctrm =
@@ -1115,7 +1101,7 @@
   end)  
 *}
 
-section {* General outline of the lifting procedure *}
+section {* General shape of the lifting procedure *}
 
 (* - A is the original raw theorem          *)
 (* - B is the regularized theorem           *)
@@ -1132,8 +1118,8 @@
   and     c: "B = C"
   and     d: "C = D"
   shows   "D"
-  using a b c d
-  by simp
+using a b c d
+by simp
 
 ML {*
 fun lift_match_error ctxt fun_str rtrm qtrm =
@@ -1156,11 +1142,9 @@
   val reg_goal = 
         Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm')
         handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm
-  val _ = warning "Regularization done."
   val inj_goal = 
         Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm'))
         handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm
-  val _ = warning "RepAbs Injection done."
 in
   Drule.instantiate' []
     [SOME (cterm_of thy rtrm'),
@@ -1169,38 +1153,30 @@
 end
 *}
 
-(* Left for debugging *)
 ML {*
+(* leaves three subgoales to be proved *)
 fun procedure_tac ctxt rthm =
   ObjectLogic.full_atomize_tac
   THEN' gen_frees_tac ctxt
-  THEN' CSUBGOAL (fn (gl, i) =>
-    let
-      val rthm' = atomize_thm rthm
-      val rule = procedure_inst ctxt (prop_of rthm') (term_of gl)
-      val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb gl))] @{thm QUOT_TRUE_i}
-    in
-      (rtac rule THEN' RANGE [rtac rthm', (fn _ => all_tac), rtac thm]) i
-    end)
-*}
-
-ML {*
-fun lift_tac ctxt rthm =
-  ObjectLogic.full_atomize_tac
-  THEN' gen_frees_tac ctxt
   THEN' CSUBGOAL (fn (goal, i) =>
     let
       val rthm' = atomize_thm rthm
       val rule = procedure_inst ctxt (prop_of rthm') (term_of goal)
-      val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb goal))] @{thm QUOT_TRUE_i}
+      val bare_goal = snd (Thm.dest_comb goal)
+      val quot_weak = Drule.instantiate' [] [SOME bare_goal] @{thm QUOT_TRUE_i}
     in
-      (rtac rule THEN'
-       RANGE [rtac rthm',
-              regularize_tac ctxt,
-              rtac thm THEN' all_inj_repabs_tac ctxt,
-              clean_tac ctxt]) i
+      (rtac rule THEN' RANGE [rtac rthm', K all_tac, rtac quot_weak]) i
     end)
 *}
 
+ML {*
+(* automated tactics *)
+fun lift_tac ctxt rthm =
+  procedure_tac ctxt rthm
+  THEN' RANGE [regularize_tac ctxt,
+               all_inj_repabs_tac ctxt,
+               clean_tac ctxt]
+*}
+
 end
 




