# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259266619 -3600
# Node ID d676974e3c894ccd2fbef97d91181865e1b5427c
# Parent  4771198ecfd80dfe953fba281f2e67832134044f
more tuning

diff -r 4771198ecfd8 -r d676974e3c89 QuotMain.thy
--- a/QuotMain.thy	Thu Nov 26 21:04:17 2009 +0100
+++ b/QuotMain.thy	Thu Nov 26 21:16:59 2009 +0100
@@ -195,17 +195,17 @@
   val thm' = Thm.freezeT (forall_intr_vars thm)
   val thm'' = ObjectLogic.atomize (cprop_of thm')
 in
-  @{thm Pure.equal_elim_rule1} OF [thm'', thm']
+  @{thm equal_elim_rule1} OF [thm'', thm']
 end
 *}
 
-ML {* atomize_thm @{thm list.induct} *}
-
 section {* infrastructure about id *}
 
 (* Need to have a meta-equality *)
+
 lemma id_def_sym: "(\<lambda>x. x) \<equiv> id"
 by (simp add: id_def)
+
 (* TODO: can be also obtained with: *)
 ML {* symmetric (eq_reflection OF @{thms id_def}) *}
 
@@ -250,7 +250,7 @@
 
 section {*  Infrastructure about definitions *}
 
-text {* expects atomized definition *}
+(* expects atomized definitions *)
 ML {*
 fun add_lower_defs_aux lthy thm =
   let
@@ -274,7 +274,7 @@
   end
 *}
 
-section {* infrastructure about collecting theorems for calling lifting *}
+section {* Infrastructure for collecting theorems for calling lifting *}
 
 ML {*
 fun lookup_quot_data lthy qty =
@@ -316,12 +316,8 @@
   end
 *}
 
-
-
 section {* Regularization *} 
 
-
-ML {*
 (*
 Regularizing an rtrm means:
  - quantifiers over a type that needs lifting are replaced by
@@ -342,7 +338,7 @@
       A = B     \<Longrightarrow>     (op = \<Longrightarrow> op \<approx>) A B
 *)
 
-
+ML {*
 (* builds the relation that is the argument of respects *)
 fun mk_resp_arg lthy (rty, qty) =
 let
@@ -382,7 +378,6 @@
 val mk_resp = Const (@{const_name Respects}, dummyT)
 *}
 
-
 ML {*
 (* - applies f to the subterm of an abstraction,   *)
 (*   otherwise to the given term,                  *)
@@ -458,11 +453,6 @@
        raise (LIFT_MATCH "regularize (default)")
 *}
 
-ML {*
-fun mk_REGULARIZE_goal lthy rtrm qtrm =
-  Logic.mk_implies (rtrm, Syntax.check_term lthy (REGULARIZE_trm lthy rtrm qtrm))
-*}
-
 (*
 To prove that the raw theorem implies the regularised one, 
 we try in order:
@@ -521,13 +511,16 @@
   ]);
 *}
 
-lemma move_forall: "(\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)) \<Longrightarrow> ((\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y))"
+lemma move_forall: 
+  "(\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)) \<Longrightarrow> ((\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y))"
 by auto
 
-lemma move_exists: "((\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)) \<Longrightarrow> ((\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y))"
+lemma move_exists: 
+  "((\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)) \<Longrightarrow> ((\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y))"
 by auto
 
-lemma [mono]: "(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> (Ex P) \<longrightarrow> (Ex Q)"
+lemma [mono]: 
+  "(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> (Ex P) \<longrightarrow> (Ex Q)"
 by blast
 
 lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P"
@@ -693,12 +686,7 @@
 end
 *}
 
-ML {*
-fun mk_inj_REPABS_goal lthy (rtrm, qtrm) =
-  Logic.mk_equals (rtrm, Syntax.check_term lthy (inj_REPABS lthy (rtrm, qtrm)))
-*}
-
-section {* RepAbs injection tactic *}
+section {* RepAbs Injection Tactic *}
 (*
 To prove that the regularised theorem implies the abs/rep injected, we first
 atomize it and then try:
@@ -836,8 +824,10 @@
     bex_rsp_tac ctxt,
     FIRST' (map rtac rsp_thms),
     rtac refl,
-    (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thm)])),
-    (APPLY_RSP_TAC rty ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thm), SOLVES' (quotient_tac quot_thm)])),
+    (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' 
+         (RANGE [SOLVES' (quotient_tac quot_thm)])),
+    (APPLY_RSP_TAC rty ctxt THEN' 
+         (RANGE [SOLVES' (quotient_tac quot_thm), SOLVES' (quotient_tac quot_thm)])),
     Cong_Tac.cong_tac @{thm cong},
     rtac @{thm ext},
     rtac reflex_thm,
@@ -964,18 +954,6 @@
   THEN' (quotient_tac quot);
 *}
 
-ML {*
-let
-   val parser = Args.context -- Scan.lift Args.name_source
-   fun term_pat (ctxt, str) =
-      str |> ProofContext.read_term_pattern ctxt
-          |> ML_Syntax.print_term
-          |> ML_Syntax.atomic
-in
-   ML_Antiquote.inline "term_pat" (parser >> term_pat)
-end
-*}
-
 ML {* 
 fun prep_trm thy (x, (T, t)) = 
   (cterm_of thy (Var (x, T)), cterm_of thy t) 
@@ -1063,7 +1041,7 @@
   end
 *}
 
-(* Genralisation of free variables in a goal *)
+section {* Genralisation of free variables in a goal *}
 
 ML {*
 fun inst_spec ctrm =
@@ -1175,12 +1153,11 @@
       val rule = procedure_inst context (prop_of rthm') (term_of concl)
       val aps = find_aps (prop_of rthm') (term_of concl)
     in
-      rtac rule THEN' RANGE [
-        rtac rthm',
-        regularize_tac lthy [rel_eqv] rel_refl,
-        REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms),
-        clean_tac lthy quot defs reps_same absrep aps
-      ]
+      rtac rule THEN' 
+       RANGE [rtac rthm',
+              regularize_tac lthy [rel_eqv] rel_refl,
+              REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms),
+              clean_tac lthy quot defs reps_same absrep aps]
     end 1) lthy
 *}