--- a/QuotMain.thy	Mon Sep 21 18:18:01 2009 +0200
+++ b/QuotMain.thy	Mon Sep 21 18:18:29 2009 +0200
@@ -114,11 +114,12 @@
 qed
 
 lemma REPS_same:
-  shows "R (REP a) (REP b) = (a = b)"
+  shows "R (REP a) (REP b) \<equiv> (a = b)"
+  apply (rule eq_reflection)
 proof
   assume as: "R (REP a) (REP b)"
   from rep_prop
-  obtain x y 
+  obtain x y
     where eqs: "Rep a = R x" "Rep b = R y" by blast
   from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp
   then have "R x (Eps (R y))" using lem9 by simp
@@ -812,7 +813,7 @@
 ML {*@{thm arg_cong2}*}
 ML {*@{thm arg_cong2[of _ _ _ _ "op ="]} *}
 ML {* val cT = @{cpat "op ="} |> Thm.ctyp_of_term |> Thm.dest_ctyp |> hd *}
-ML {* 
+ML {*
   Toplevel.program (fn () =>
     Drule.instantiate' [SOME cT,SOME cT,SOME @{ctyp bool}] [NONE,NONE,NONE,NONE,SOME (@{cpat "op ="})] @{thm arg_cong2}
   )
@@ -836,8 +837,8 @@
       val concl = Thm.cprem_of thm n;
       val (_, cconcl) = Thm.dest_comb concl;
       val rewr = foo_conv cconcl;
-      val _ = tracing (Display.string_of_thm @{context} rewr)
-      val _ = tracing (Display.string_of_thm @{context} thm)
+(*      val _ = tracing (Display.string_of_thm @{context} rewr)
+      val _ = tracing (Display.string_of_thm @{context} thm)*)
     in
       rtac rewr n thm
     end
@@ -847,14 +848,15 @@
 (* Has all the theorems about fset plugged in. These should be parameters to the tactic *)
 
 ML {*
-  val foo_tac' =
-    FIRST' [
+  fun foo_tac' ctxt =
+    REPEAT_ALL_NEW (FIRST' [
       rtac @{thm list_eq_sym},
       rtac @{thm cons_preserves},
       rtac @{thm mem_respects},
-      foo_tac,
-      simp_tac (@{simpset} addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})
-    ]
+      rtac @{thm QUOT_TYPE_I_fset.R_trans2},
+      CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})),
+      foo_tac
+    ])
 *}
 
 thm m1
@@ -868,11 +870,7 @@
 
 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' @{context} 1 *})
   done
 
 
@@ -883,13 +881,10 @@
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 *}
-(* prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
+prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 2 *})
-  apply (tactic {* foo_tac' 2 *})
-  apply (tactic {* foo_tac' 2 *})
-  apply (tactic {* foo_tac' 1 *}) *)
+  apply (tactic {* foo_tac' @{context} 1 *})
+  sorry
 
 thm m2
 ML {*
@@ -900,19 +895,7 @@
 *}
 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' @{context} 1 *})
   done
 
 thm list_eq.intros(4)
@@ -927,19 +910,10 @@
 (* It is the same, but we need a name for it. *)
 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *} sorry
 lemma zzz :
-  "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx>
-    REP_fset (INSERT a (ABS_fset xs))) =  (a # a # xs \<approx> a # xs)"
+  "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs)))
+    = (a # a # xs \<approx> a # xs)"
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
-  apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
-  apply (rule QUOT_TYPE_I_fset.R_trans2)
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' @{context} 1 *})
   done
 
 lemma zzz' :
@@ -947,7 +921,20 @@
   using list_eq.intros(4) by (simp only: zzz)
 
 thm QUOT_TYPE_I_fset.REPS_same
-ML {* MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *}
+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 {*
@@ -958,15 +945,7 @@
 *}
 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
-  apply (rule QUOT_TYPE_I_fset.R_trans2)
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' @{context} 1 *})
   done
 
 (*