--- a/QuotMain.thy	Thu Oct 15 11:42:14 2009 +0200
+++ b/QuotMain.thy	Thu Oct 15 11:55:52 2009 +0200
@@ -774,31 +774,6 @@
 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 *}
 
-(* Has all the theorems about fset plugged in. These should be parameters to the tactic *)
-ML {*
-  fun transconv_fset_tac' ctxt =
-    REPEAT_ALL_NEW (FIRST' [
-      rtac @{thm list_eq_refl},
-      rtac @{thm cons_preserves},
-      rtac @{thm mem_respects},
-      rtac @{thm card1_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})),
-      Cong_Tac.cong_tac @{thm cong},
-      rtac @{thm ext}
-    ])
-*}
-
-ML {*
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1}))
-  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
-  val cgoal = cterm_of @{theory} goal
-  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
-*}
-
-(*notation ( output) "prop" ("#_" [1000] 1000) *)
-notation ( output) "Trueprop" ("#_" [1000] 1000)
-
 lemma atomize_eqv[atomize]: 
   shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)" 
 proof
@@ -819,10 +794,36 @@
   then show "A \<equiv> B" by (rule eq_reflection)
 qed
 
+(* Has all the theorems about fset plugged in. These should be parameters to the tactic *)
+ML {*
+  fun transconv_fset_tac' ctxt =
+    (LocalDefs.unfold_tac @{context} fset_defs) THEN
+    ObjectLogic.full_atomize_tac 1 THEN
+    REPEAT_ALL_NEW (FIRST' [
+      rtac @{thm list_eq_refl},
+      rtac @{thm cons_preserves},
+      rtac @{thm mem_respects},
+      rtac @{thm card1_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})),
+      Cong_Tac.cong_tac @{thm cong},
+      rtac @{thm ext}
+    ]) 1
+*}
+
+ML {*
+  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1}))
+  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
+  val cgoal = cterm_of @{theory} goal
+  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
+*}
+
+(*notation ( output) "prop" ("#_" [1000] 1000) *)
+notation ( output) "Trueprop" ("#_" [1000] 1000)
+
+
 prove {* (Thm.term_of cgoal2) *}
-  apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
-  apply (atomize(full))
-  apply (tactic {* transconv_fset_tac' @{context} 1 *})
+  apply (tactic {* transconv_fset_tac' @{context} *})
   done
 
 thm length_append (* Not true but worth checking that the goal is correct *)
@@ -833,9 +834,7 @@
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 *}
 prove {* Thm.term_of cgoal2 *}
-  apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
-  apply (atomize(full))
-  apply (tactic {* transconv_fset_tac' @{context} 1 *})
+  apply (tactic {* transconv_fset_tac' @{context} *})
   sorry
 
 thm m2
@@ -846,9 +845,7 @@
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 *}
 prove {* Thm.term_of cgoal2 *}
-  apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
-  apply (atomize(full))
-  apply (tactic {* transconv_fset_tac' @{context} 1 *})
+  apply (tactic {* transconv_fset_tac' @{context} *})
   done
 
 thm list_eq.intros(4)
@@ -862,9 +859,7 @@
 
 (* It is the same, but we need a name for it. *)
 prove zzz : {* Thm.term_of cgoal3 *}
-  apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
-  apply (atomize(full))
-  apply (tactic {* transconv_fset_tac' @{context} 1 *})
+  apply (tactic {* transconv_fset_tac' @{context} *})
   done
 
 lemma zzz' :
@@ -874,25 +869,15 @@
 thm QUOT_TYPE_I_fset.REPS_same
 ML {* val zzz'' = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *}
 
-
 thm list_eq.intros(5)
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)}))
   val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
-*}
-ML {*
-  val cgoal =
-    Toplevel.program (fn () =>
-      cterm_of @{theory} goal
-    )
-*}
-ML {*
+  val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
 *}
 prove {* Thm.term_of cgoal2 *}
-  apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
-  apply (atomize(full))
-  apply (tactic {* transconv_fset_tac' @{context} 1 *})
+  apply (tactic {* transconv_fset_tac' @{context} *})
   done
 
 section {* handling quantifiers - regularize *}
@@ -1041,9 +1026,6 @@
   cterm_of @{theory} (regularise @{term "All (P :: trm \<Rightarrow> bool)"} @{typ "trm"} @{term "RR"} @{context});
 *}
 
-
-
-
 ML {*
 fun atomize_thm thm =
 let
@@ -1061,9 +1043,6 @@
   trm == new_trm
 *)
 
-
-
-
 ML {* val li = Thm.freezeT (atomize_thm @{thm list.induct}) *}
 
 prove {*
@@ -1075,6 +1054,7 @@
   apply (rule RIGHT_RES_FORALL_REGULAR)
   prefer 2
   apply (assumption)
+  apply (auto)
   apply (rule allI)
   apply (rule impI)
   apply (rule impI)