# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1253883035 -7200
# Node ID 3767a6f3d9ee83378c37dcd5ed887233d3ba5dd5
# Parent  395beba59d5511cab63845ec9f373487d7926ec9
A version of the tactic that exports variables correctly.
It still does not know how to instantiate the obtained theorems.

diff -r 395beba59d55 -r 3767a6f3d9ee QuotMain.thy
--- a/QuotMain.thy	Fri Sep 25 09:38:16 2009 +0200
+++ b/QuotMain.thy	Fri Sep 25 14:50:35 2009 +0200
@@ -1067,20 +1067,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 {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)}))
@@ -1123,6 +1109,62 @@
   apply (tactic {* foo_tac' @{context} 1 *})
   sorry
 
+ML {*
+  fun lift_theorem_fset_aux thm lthy =
+    let
+      val ((_, [novars]), lthy2) = Variable.import true [thm] lthy;
+      val goal = build_goal novars consts @{typ "'a list"} mk_rep_abs;
+      val cgoal = cterm_of @{theory} goal;
+      val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal);
+      val tac = (LocalDefs.unfold_tac @{context} fset_defs) THEN (foo_tac' @{context}) 1;
+      val cthm = Goal.prove_internal [] cgoal2 (fn _ => tac);
+      val nthm = MetaSimplifier.rewrite_rule [symmetric cthm] (snd (no_vars (Context.Theory @{theory}, thm)))
+      val nthm2 = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same QUOT_TYPE_I_fset.thm10} nthm;
+      val [nthm3] = ProofContext.export lthy2 lthy [nthm2]
+    in
+      nthm3
+    end
+*}
+
+ML {* lift_theorem_fset_aux @{thm m1} @{context} *}
+
+ML {*
+  fun lift_theorem_fset name thm lthy =
+    let
+      val lifted_thm = lift_theorem_fset_aux thm lthy;
+      val (_, lthy2) = note_thm (name, lifted_thm) lthy;
+    in
+      lthy2
+    end;
+*}
+
+local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *}
+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} *}
+
+thm m1_lift
+thm leqi4_lift
+thm leqi5_lift
+thm m2_lift
+
+ML Drule.instantiate'
+text {*
+  We lost the schematic variable again :(.
+  Another variable export will still be necessary...
+*}
+ML {*
+  Toplevel.program (fn () =>
+    MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} (
+      Drule.instantiate' [] [NONE, NONE, SOME (@{cpat "REP_fset x"})] @{thm m2_lift}
+    )
+  )
+*}
+
+
+
+
+ML {* MRS *}
 thm card1_suc
 
 ML {*