# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259591534 -3600
# Node ID 0911d3aabf471e4d82938c979893ef2558c6dda5
# Parent  020e27417b59882e38630a8cdf77f0f685f369e8
clean_tac rewrites the definitions the other way

diff -r 020e27417b59 -r 0911d3aabf47 FSet.thy
--- a/FSet.thy	Mon Nov 30 12:14:20 2009 +0100
+++ b/FSet.thy	Mon Nov 30 15:32:14 2009 +0100
@@ -313,7 +313,6 @@
   val qtrm = @{term "\<forall>x. x memb [] = False"}
   val aps = find_aps rtrm qtrm 
 *}
-unfolding IN_def EMPTY_def
 apply(tactic {* clean_tac @{context} [quot] defs aps 1*})
 done
 
@@ -354,10 +353,12 @@
 lemma cheat: "P" sorry
 
 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
+apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
+ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 prefer 2
-apply(rule cheat)
+apply(tactic {* clean_tac @{context} [quot] defs [] 1 *})
 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) 
@@ -454,6 +455,8 @@
 lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
 apply (tactic {* procedure_tac @{context} @{thm list_induct_part} 1 *})
 apply (tactic {* regularize_tac @{context} [rel_eqv] 1 *})
+prefer 2
+apply (tactic {* clean_tac @{context} [quot] defs [(@{typ "('a list \<Rightarrow> 'c list \<Rightarrow> bool)"},@{typ "('a list \<Rightarrow> 'c fset \<Rightarrow> bool)"})] 1 *})
 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
 apply (rule FUN_QUOTIENT)
 apply (rule FUN_QUOTIENT)
@@ -523,7 +526,6 @@
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* clean_tac @{context} [quot] defs [(@{typ "('a list \<Rightarrow> 'c list \<Rightarrow> bool)"},@{typ "('a list \<Rightarrow> 'c fset \<Rightarrow> bool)"})] 1 *})
 done
 
 end
diff -r 020e27417b59 -r 0911d3aabf47 LFex.thy
--- a/LFex.thy	Mon Nov 30 12:14:20 2009 +0100
+++ b/LFex.thy	Mon Nov 30 15:32:14 2009 +0100
@@ -461,35 +461,7 @@
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2  1*})
-(*apply(tactic {* clean_tac @{context} quot defs aps 1 *}) *)
-apply (tactic {* lambda_prs_tac @{context} quot 1 *})
-apply (tactic {* simp_tac ((Simplifier.context @{context} empty_ss) addsimps (meta_reps_same @ meta_lower)) 1 *})
-apply (tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *})
-ML_prf {* val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot *}
-ML_prf {* val aps_thms = map (applic_prs @{context} absrep) aps *}
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply (rule refl) apply (rule ext)
-apply (tactic {* REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \<longrightarrow>"]}) 1 *})
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
+apply(tactic {* clean_tac @{context} quot defs aps 1 *})
 done
 
 (* Does not work:
diff -r 020e27417b59 -r 0911d3aabf47 QuotMain.thy
--- a/QuotMain.thy	Mon Nov 30 12:14:20 2009 +0100
+++ b/QuotMain.thy	Mon Nov 30 15:32:14 2009 +0100
@@ -738,7 +738,7 @@
       end
   | _ =>
       (**************************************************)
-      (*  new
+      (*  new *)
       let
         val (rhead, rargs) = strip_comb rtrm
         val (qhead, qargs) = strip_comb qtrm
@@ -765,10 +765,10 @@
              list_comb (inj_repabs_trm lthy (rhead, qhead), rargs') 
         | _ => raise (LIFT_MATCH "injection")
       end
-      *)
+      (**)
 
       (*************************************************)
-      (* old *)
+      (* old
       let
         val (rhead, rargs) = strip_comb rtrm
         val (qhead, qargs) = strip_comb qtrm
@@ -792,7 +792,7 @@
                mk_repabs lthy (rty, qty) (list_comb (inj_repabs_trm lthy (rhead, qhead), rargs')) 
           | _ => raise (LIFT_MATCH "injection")
       end
-      (**)
+      *)
 end
 *}
 
@@ -1029,6 +1029,7 @@
 fun find_aps rtm qtm = distinct (op =) (find_aps_all rtm qtm)
 *}
 
+(* TODO: This is slow *)
 ML {*
 fun allex_prs_tac lthy quot =
   (EqSubst.eqsubst_tac lthy [0] @{thms all_prs ex_prs}) THEN' (quotient_tac quot)
@@ -1103,6 +1104,7 @@
 *}
 
 (*
+ TODO: Update
  Cleaning the theorem consists of 5 kinds of rewrites.
  These rewrites can be done independently and in any order.
 
@@ -1124,18 +1126,16 @@
 ML {*
 fun clean_tac lthy quot defs aps =
   let
-    val lower = flat (map (add_lower_defs lthy) defs)
-    val meta_lower = map (fn x => @{thm eq_reflection} OF [x]) lower
     val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot
+    val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep;
     val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot
     val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same
-    val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps (meta_reps_same @ meta_lower)
-    val aps_thms = map (applic_prs lthy absrep) aps
+    val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps
+      (@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ meta_absrep @ meta_reps_same @ defs)
   in
     EVERY' [lambda_prs_tac lthy quot,
+            TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot),
             TRY o simp_tac simp_ctxt,
-            TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot),
-            TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] aps_thms),
             TRY o rtac refl]
   end
 *}