# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1256553242 -3600
# Node ID 01151c3853ce95b7067751021358dd60379b0ae1
# Parent  b8485573548d832ae85f9a8fa69812d76cc4dd37
Making all the definitions from the original ones

diff -r b8485573548d -r 01151c3853ce FSet.thy
--- a/FSet.thy	Mon Oct 26 10:20:20 2009 +0100
+++ b/FSet.thy	Mon Oct 26 11:34:02 2009 +0100
@@ -167,7 +167,29 @@
 *}
 
 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *}
-ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *}
+text {* expects atomized definition *}
+ML {*
+  fun add_lower_defs ctxt thm =
+    let
+      val e1 = @{thm fun_cong} OF [thm]
+      val f = eqsubst_thm ctxt @{thms fun_map.simps} e1
+    in
+      thm :: (add_lower_defs ctxt f)
+    end
+    handle _ => [thm]
+*}
+ML {* val fset_defs_pre_sym = map symmetric fset_defs *}
+ML {* val fset_defs_atom = map atomize_thm fset_defs_pre_sym *}
+ML {* val fset_defs_all = flat (map (add_lower_defs @{context}) fset_defs_atom) *}
+ML {* val fset_defs_sym = map (fn t => eq_reflection OF [t]) fset_defs_all *}
+ML {* val fset_defs_sym = map ObjectLogic.rulify fset_defs_sym *}
+ML {* val fset_defs_sym = map Thm.varifyT fset_defs_sym *}
+
+
+(*
+  ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *}
+*)
+
 
 thm fun_map.simps
 text {* Respectfullness *}
@@ -392,6 +414,8 @@
 *}
 
 ML {* val ithm = simp_allex_prs @{context} m2_t' *}
+ML fset_defs_sym
+
 ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *}
 ML {* ObjectLogic.rulify rthm *}
 
@@ -416,7 +440,6 @@
 apply (tactic {* rtac card1_suc_r 1 *})
 done
 
-
 ML {* val card1_suc_t_n = @{thm card1_suc_t} *}
 ML {* val card1_suc_t' = eqsubst_thm @{context} @{thms HOL.sym[OF lambda_prs_l_b,simplified]} @{thm card1_suc_t} *}
 ML {* val card1_suc_t'' = eqsubst_thm @{context} @{thms HOL.sym[OF lambda_prs_l_b,simplified]} card1_suc_t' *}
@@ -478,6 +501,8 @@
 ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT], symmetric]} *}
 ML {* val ind_r_a1 = eqsubst_thm @{context} [thm] ind_r_a *}
 
+
+ML {* hd fset_defs_sym *}
 ML {* val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a1 *}
 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *}
 ML {* ObjectLogic.rulify ind_r_s *}