# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1256289883 -7200
# Node ID 2ee03759a22f538ee74c00e3a31331ac17941e0c
# Parent  6b475324cef7e6cb4137702dd51a04ff669bbf00
Trying to get a simpler lemma with the whole infrastructure

diff -r 6b475324cef7 -r 2ee03759a22f QuotMain.thy
--- a/QuotMain.thy	Fri Oct 23 09:21:45 2009 +0200
+++ b/QuotMain.thy	Fri Oct 23 11:24:43 2009 +0200
@@ -731,6 +731,10 @@
 
 section {* RepAbs injection *}
 
+(* Needed to have a meta-equality *)
+lemma id_def_sym: "(\<lambda>x. x) \<equiv> id"
+by (simp add: id_def)
+
 ML {*
 fun build_repabs_term lthy thm constructors rty qty =
   let
@@ -783,7 +787,8 @@
         else list_comb(opp, tms)
       end
   in
-    build_aux lthy (Thm.prop_of thm)
+    MetaSimplifier.rewrite_term @{theory} @{thms id_def_sym} []
+      (build_aux lthy (Thm.prop_of thm))
   end
 *}
 
@@ -1031,13 +1036,6 @@
   (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
 *}
 
-ML {* 
-
-((simp_tac ((Simplifier.context @{context}  HOL_ss) addsimps @{thms FUN_REL.simps})) THEN' (fn _ => no_tac))
-*}
-
-ML {* ((simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps}))  THEN_ALL_NEW (fn _ => no_tac)) *}
-ML {* RANGE *}
 
 ML {*
 fun quotient_tac quot_thm =
@@ -1077,11 +1075,8 @@
 
 prove list_induct_tr: trm_r
 apply (atomize(full))
-apply (simp only: id_def[symmetric])
 (* APPLY_RSP_TAC *)
-apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
-apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
-apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 (* LAMBDA_RES_TAC *)
 apply (simp only: FUN_REL.simps)
 apply (rule allI)
@@ -1100,8 +1095,6 @@
 (* REFL_TAC *)
 apply (simp)
 (* APPLY_RSP_TAC *)
-apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (simp only: FUN_REL.simps)
@@ -1115,20 +1108,13 @@
 (* REFL_TAC *)
 apply (simp)
 (* APPLY_RSP *)
-apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 (* MK_COMB_TAC *)
 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
 (* REFL_TAC *)
 apply (simp)
 (* W(C (curry op THEN) (G... *)
-apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
-apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
-apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
-apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
 (* CONS respects *)
 apply (simp add: FUN_REL.simps)
 apply (rule allI)
@@ -1137,11 +1123,7 @@
 apply (rule impI)
 apply (rule cons_preserves)
 apply (assumption)
-apply (simp)
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
 apply (simp only: FUN_REL.simps)
 apply (rule allI)
 apply (rule allI)
@@ -1158,6 +1140,81 @@
 
 thm list.recs(2)
 
+ML {* atomize_thm @{thm m2} *}
+
+prove m2_r_p: {*
+   build_regularize_goal (atomize_thm @{thm m2}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}
+  apply (simp add: equiv_res_forall[OF equiv_list_eq])
+done
+
+ML {* val m2_r = @{thm m2_r_p} OF [atomize_thm @{thm m2}] *}
+ML {* val m2_t_g = build_repabs_goal @{context} m2_r consts @{typ "'a list"} @{typ "'a fset"} *}
+ML {* val m2_t = build_repabs_term @{context} m2_r consts @{typ "'a list"} @{typ "'a fset"} *}
+prove m2_t_p: m2_t_g
+apply (atomize(full))
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
+apply (simp add: FUN_REL.simps)
+prefer 2
+apply (simp only: FUN_REL.simps)
+apply (rule allI)
+apply (rule allI)
+apply (rule impI)
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
+prefer 2
+apply (simp only: FUN_REL.simps)
+apply (rule allI)
+apply (rule allI)
+apply (rule impI)
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
+apply (simp only: FUN_REL.simps)
+apply (rule allI)
+apply (rule allI)
+apply (rule impI)
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
+apply (simp only: FUN_REL.simps)
+apply (rule allI)
+apply (rule allI)
+apply (rule impI)
+apply (rule allI)
+apply (rule allI)
+apply (rule impI)
+apply (simp add:mem_respects)
+apply (simp only: FUN_REL.simps)
+apply (rule allI)
+apply (rule allI)
+apply (rule impI)
+apply (rule allI)
+apply (rule allI)
+apply (rule impI)
+apply (simp add:cons_preserves)
+apply (simp only: FUN_REL.simps)
+apply (rule allI)
+apply (rule allI)
+apply (rule impI)
+apply (rule allI)
+apply (rule allI)
+apply (rule impI)
+apply (simp add:mem_respects)
+apply (auto)
+done
+
+prove m2_t: m2_t
+apply (simp only: m2_t_p[symmetric])
+apply (tactic {* rtac m2_r 1 *})
+done
+
+thm LAMBDA_PRS
+ML {*
+ val t = prop_of @{thm LAMBDA_PRS}
+ val tt = Drule.instantiate' [SOME @{ctyp "'a list"}, SOME @{ctyp "'a fset"}] [] @{thm LAMBDA_PRS}
+ val ttt = tt OF [@{thm QUOTIENT_fset}, @{thm IDENTITY_QUOTIENT}]
+*}
+ML {* val tttt = @{thm "HOL.sym"} OF [ttt] *}
+ML {* val zzzz = MetaSimplifier.rewrite_rule  [tttt] @{thm m2_t} *}
+
+
+thm m2_t
+ML {* @{thm m2_t} *}
 
 ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *}