# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1256554536 -3600
# Node ID ca1a24aa822ebdbb8fa496fdd8628f7ec7aa5fee
# Parent  01151c3853ce95b7067751021358dd60379b0ae1
Finished the code for adding lower defs, and more things moved to QuotMain

diff -r 01151c3853ce -r ca1a24aa822e FSet.thy
--- a/FSet.thy	Mon Oct 26 11:34:02 2009 +0100
+++ b/FSet.thy	Mon Oct 26 11:55:36 2009 +0100
@@ -167,32 +167,7 @@
 *}
 
 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *}
-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 *}
+ML {* val fset_defs_sym = add_lower_defs @{context} fset_defs *}
 
 lemma memb_rsp:
   fixes z
@@ -271,31 +246,6 @@
   apply (metis)
   done
 
-ML {*
-fun repabs_eq lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms =
-  let
-    val rt = build_repabs_term lthy thm constructors rty qty;
-    val rg = Logic.mk_equals ((Thm.prop_of thm), rt);
-    fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN'
-      (REPEAT_ALL_NEW (r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm rsp_thms));
-    val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1);
-  in
-    (rt, cthm, thm)
-  end
-*}
-
-ML {*
-fun repabs_eq2 lthy (rt, thm, othm) =
-  let
-    fun tac2 ctxt =
-     (simp_tac ((Simplifier.context ctxt empty_ss) addsimps [symmetric thm]))
-     THEN' (rtac othm);
-    val cthm = Goal.prove lthy [] [] rt (fn x => tac2 (#context x) 1);
-  in
-    cthm
-  end
-*}
-
 (* The all_prs and ex_prs should be proved for the instance... *)
 ML {*
 fun r_mk_comb_tac_fset ctxt =
@@ -420,7 +370,7 @@
 ML {* ObjectLogic.rulify rthm *}
 
 
-ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *}
+ML {* val card1_suc_a = atomize_thm @{thm card1_suc} *}
 
 prove card1_suc_r_p: {*
    build_regularize_goal (atomize_thm @{thm card1_suc}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}
diff -r 01151c3853ce -r ca1a24aa822e QuotMain.thy
--- a/QuotMain.thy	Mon Oct 26 11:34:02 2009 +0100
+++ b/QuotMain.thy	Mon Oct 26 11:55:36 2009 +0100
@@ -720,6 +720,31 @@
     ])
 *}
 
+ML {*
+fun repabs_eq lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms =
+  let
+    val rt = build_repabs_term lthy thm constructors rty qty;
+    val rg = Logic.mk_equals ((Thm.prop_of thm), rt);
+    fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN'
+      (REPEAT_ALL_NEW (r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm rsp_thms));
+    val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1);
+  in
+    (rt, cthm, thm)
+  end
+*}
+
+ML {*
+fun repabs_eq2 lthy (rt, thm, othm) =
+  let
+    fun tac2 ctxt =
+     (simp_tac ((Simplifier.context ctxt empty_ss) addsimps [symmetric thm]))
+     THEN' (rtac othm);
+    val cthm = Goal.prove lthy [] [] rt (fn x => tac2 (#context x) 1);
+  in
+    cthm
+  end
+*}
+
 section {* Cleaning the goal *}
 
 text {* Does the same as 'subst' in a given theorem *}
@@ -738,4 +763,29 @@
   end
 *}
 
+text {* expects atomized definition *}
+ML {*
+  fun add_lower_defs_aux 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_aux ctxt f)
+    end
+    handle _ => [thm]
+*}
+
+ML {*
+fun add_lower_defs ctxt defs =
+  let
+    val defs_pre_sym = map symmetric defs
+    val defs_atom = map atomize_thm defs_pre_sym
+    val defs_all = flat (map (add_lower_defs_aux ctxt) defs_atom)
+    val defs_sym = map (fn t => eq_reflection OF [t]) defs_all
+  in
+    map Thm.varifyT defs_sym
+  end
+*}
+
+
 end