# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1254214171 -7200
# Node ID 32c0985563a8312c3a4512a4b9613b0421cc67a1
# Parent  18d8bcd769b3748b03e22195f56db4ff2105e0b9
Tested new build_goal and removed old one, eq_reflection is included in atomize, card_suc tests.

diff -r 18d8bcd769b3 -r 32c0985563a8 QuotMain.thy
--- a/QuotMain.thy	Tue Sep 29 09:58:02 2009 +0200
+++ b/QuotMain.thy	Tue Sep 29 10:49:31 2009 +0200
@@ -866,44 +866,6 @@
   end
 *}
 
-ML {*
-fun build_goal' ctxt thm constructors qty mk_rep_abs =
-  let
-    fun is_const (Const (x, t)) = member (op =) constructors x
-      | is_const _ = false
-
-    fun maybe_mk_rep_abs t =
-      let
-        val _ = writeln ("Maybe: " ^ Syntax.string_of_term ctxt t)
-      in
-        if type_of t = qty then mk_rep_abs t else t
-      end
-(*      handle TYPE _ => t*)
-    fun build_aux ctxt1 (Abs (x, T, t)) =
-          let
-            val ([x'], ctxt2) = Variable.variant_fixes [x] ctxt1;
-            val v = Free (x', T);
-            val t' = subst_bound (v, t);
-            val rec_term = build_aux ctxt2 t';
-          in Term.lambda_name (x, v) rec_term end
-      | build_aux ctxt1 (f $ a) =
-          let
-            val (f, args) = strip_comb (f $ a)
-            val _ = writeln (Syntax.string_of_term ctxt f)
-           in
-            if is_const f then
-              maybe_mk_rep_abs
-                (list_comb (f, map maybe_mk_rep_abs (map (build_aux ctxt1) args)))
-            else list_comb (build_aux ctxt1 f, map (build_aux ctxt1) args)
-          end
-      | build_aux _ x =
-          if is_const x then maybe_mk_rep_abs x else x
-
-    val concl2 = term_of (#prop (crep_thm thm))
-  in
-  Logic.mk_equals (build_aux ctxt concl2, concl2)
-end *}
-
 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *}
 ML {* val fset_defs_sym = map (fn t => symmetric (unlam_def @{context} t)) fset_defs *}
 
@@ -1004,7 +966,7 @@
       CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})),
       DatatypeAux.cong_tac,
       rtac @{thm ext},
-      rtac @{thm eq_reflection},
+(*      rtac @{thm eq_reflection},*)
       CHANGED o (ObjectLogic.full_atomize_tac)
     ])
 *}
@@ -1096,19 +1058,6 @@
 thm QUOT_TYPE_I_fset.REPS_same
 ML {* val zzz'' = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *}
 
-ML Drule.instantiate'
-ML {* zzz'' *}
-text {*
-  A variable export will still be necessary in the end, but this is already the final theorem.
-*}
-ML {*
-  Toplevel.program (fn () =>
-    MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} (
-      Drule.instantiate' [] [NONE,SOME (@{cpat "REP_fset x"})] zzz''
-    )
-  )
-*}
-
 
 thm list_eq.intros(5)
 ML {*
@@ -1183,11 +1132,14 @@
 local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *}
 local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *}
 local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *}
+local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *}
 
 thm m1_lift
 thm leqi4_lift
 thm leqi5_lift
 thm m2_lift
+thm card_suc
+(* The above is not good, we lost the ABS in front of xs on the rhs, so can't be properly instantiated... *)
 
 ML Drule.instantiate'
 text {*
@@ -1223,10 +1175,6 @@
   )
 *}
 
-
-
-
-
 ML {* MRS *}
 thm card1_suc
 
@@ -1245,7 +1193,7 @@
 prove {* (Thm.term_of cgoal2) *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
   apply (tactic {* foo_tac' @{context} 1 *})
-
+  done
 
 (*
 datatype obj1 =
@@ -1254,6 +1202,3 @@
 | INVOKE1 "obj1 \<Rightarrow> string"
 | UPDATE1 "obj1 \<Rightarrow> string \<Rightarrow> (string \<Rightarrow> obj1)"
 *)
-
-
-yyes