# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259075431 -3600
# Node ID 84621d9942f583cfbdd7455146c5c60ed60833f5
# Parent  ba057402ea537ba6b1419da121a3ea756235e632# Parent  4c455d58ac995956ae48e511437dc6dd18f67781
merged

diff -r ba057402ea53 -r 84621d9942f5 FSet.thy
--- a/FSet.thy	Tue Nov 24 15:31:29 2009 +0100
+++ b/FSet.thy	Tue Nov 24 16:10:31 2009 +0100
@@ -305,30 +305,46 @@
 
 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *}
 ML {* fun lift_thm_g_fset lthy t g = lift_thm_goal lthy qty "fset" rsp_thms defs t g *}
+ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
+ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *}
+ML {* val consts = lookup_quot_consts defs *}
+ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *}
 
-ML {* lift_thm_fset @{context} @{thm m1} *}
-ML {* lift_thm_g_fset @{context} @{thm m1} @{term "IN x EMPTY = False"} *}
+lemma "IN x EMPTY = False"
+by (tactic {* lift_tac_fset @{context} @{thm m1} 1 *})
 
-ML {* lift_thm_fset @{context} @{thm m2} *}
-ML {* lift_thm_g_fset @{context} @{thm m2} @{term "IN x (INSERT y xa) = (x = y \<or> IN x xa)"} *}
+lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)"
+by (tactic {* lift_tac_fset @{context} @{thm m2} 1 *})
 
-ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *}
-ML {* lift_thm_g_fset @{context} @{thm list_eq.intros(4)} @{term "INSERT a (INSERT a x) = INSERT a x"} *}
+lemma "INSERT a (INSERT a x) = INSERT a x"
+apply (tactic {* lift_tac_fset @{context} @{thm list_eq.intros(4)} 1 *})
+done
+
+lemma "x = xa \<longrightarrow> INSERT a x = INSERT a xa"
+apply (tactic {* lift_tac_fset @{context} @{thm list_eq.intros(5)} 1 *})
+done
 
-ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *}
-ML {* lift_thm_g_fset @{context} @{thm list_eq.intros(5)} @{term "x = xa \<Longrightarrow> INSERT a x = INSERT a xa"} *}
+lemma "CARD x = Suc n \<longrightarrow> (\<exists>a b. \<not> IN a b & x = INSERT a b)"
+apply (tactic {* lift_tac_fset @{context} @{thm card1_suc} 1 *})
+done
+
+lemma "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))"
+apply (tactic {* lift_tac_fset @{context} @{thm not_mem_card1} 1 *})
+done
 
-ML {* lift_thm_fset @{context} @{thm card1_suc} *}
-ML {* lift_thm_g_fset @{context} @{thm card1_suc} @{term "CARD x = Suc n \<Longrightarrow> \<exists>a b. \<not> IN a b \<and> x = INSERT a b"} *}
+ML {* atomize_thm @{thm fold1.simps(2)} *}
+(*ML {* lift_thm_g_fset @{context} @{thm fold1.simps(2)} @{term "FOLD f g (z::'b) (INSERT a x) =
+    (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"} *}*)
 
-ML {* lift_thm_fset @{context} @{thm not_mem_card1} *}
-ML {* lift_thm_g_fset @{context} @{thm not_mem_card1} @{term "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))"} *}
+lemma "\<forall>f g z a x. FOLD f g (z::'b) (INSERT a x) =
+  (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"
+apply (tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})
+done
 
-ML {* lift_thm_fset @{context} @{thm fold1.simps(2)} *}
+ML {* cterm_of @{theory} (atomize_goal @{theory} @{term "\<forall>x xa a. x = xa \<Longrightarrow> INSERT a x = INSERT a xa"}) *}
 
 (* Doesn't work with 'a, 'b, but works with 'b, 'a *)
-ML {* lift_thm_g_fset @{context} @{thm fold1.simps(2)} @{term "FOLD f g (z::'b) (INSERT a x) =
-    (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"} *}
+ML {* lift_thm_g_fset @{context} @{thm fold1.simps(2)} 
 
 ML {* lift_thm_fset @{context} @{thm append_assoc} *}
 ML {* lift_thm_g_fset @{context} @{thm append_assoc} @{term "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"} *}
@@ -338,6 +354,21 @@
 ML {* lift_thm_fset @{context} @{thm list.induct} *}
 ML {* lift_thm_g_fset @{context} @{thm list.induct} @{term "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"} *}
 
+
+
+apply(tactic {* procedure_tac @{thm m1} @{context} 1 *})
+apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *})
+apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *})
+apply(tactic {* clean_tac @{context} quot defs reps_same 1 *})
+apply(tactic {* TRY' (REPEAT_ALL_NEW (allex_prs_tac @{context} quot)) 1 *})
+apply(tactic {* TRY' (REPEAT_ALL_NEW (lambda_prs_tac @{context} quot)) 1 *})
+ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *}
+apply(tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1*})
+apply(tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
+
+
+
+
 (*ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *}*)
 
 quotient_def
@@ -374,9 +405,6 @@
 ML {* lift_thm_fset @{context} @{thm list.recs(2)} *}
 ML {* lift_thm_g_fset @{context} @{thm list.recs(2)} @{term "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"} *}
 
-ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
-ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *}
-ML {* val consts = lookup_quot_consts defs *}
 
 ML {* val gl = @{term "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"} *}
 ML {* val t_a = atomize_thm @{thm list.recs(2)} *}
diff -r ba057402ea53 -r 84621d9942f5 QuotMain.thy
--- a/QuotMain.thy	Tue Nov 24 15:31:29 2009 +0100
+++ b/QuotMain.thy	Tue Nov 24 16:10:31 2009 +0100
@@ -789,8 +789,8 @@
     ball_rsp_tac ctxt,
     bex_rsp_tac ctxt,
     FIRST' (map rtac rsp_thms),
+    rtac refl,
     (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
-    rtac refl,
     (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
     Cong_Tac.cong_tac @{thm cong},
     rtac @{thm ext},