--- a/FSet.thy	Sat Oct 24 13:00:54 2009 +0200
+++ b/FSet.thy	Sat Oct 24 14:00:18 2009 +0200
@@ -277,14 +277,13 @@
 fun regularize thm rty rel rel_eqv lthy =
   let
     val g = build_regularize_goal thm rty rel lthy;
-    val tac =
-       atac ORELSE' (simp_tac ((Simplifier.context lthy HOL_ss) addsimps
+    fun tac ctxt =
+       (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
         [(@{thm equiv_res_forall} OF [rel_eqv]),
          (@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW
-         ((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN'
-         (RANGE [fn _ => all_tac, atac]) THEN' (MetisTools.metis_tac lthy []));
-    val cgoal = cterm_of (ProofContext.theory_of lthy) g;
-    val cthm = Goal.prove_internal [] cgoal (fn _ => tac 1);
+         (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac])) ORELSE'
+         (MetisTools.metis_tac ctxt []));
+    val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1);
   in
     cthm OF [thm]
   end
@@ -438,8 +437,6 @@
 apply (tactic {* rtac thm 1 *})
 done
 
-thm list.recs(2)
-
 thm m2
 ML {* atomize_thm @{thm m2} *}
 
@@ -555,9 +552,12 @@
 ML {* ObjectLogic.rulify qthm *}
 
 thm fold1.simps(2)
-
+thm list.recs(2)
 
-ML {* val ind_r_a = atomize_thm @{thm fold1.simps(2)} *}
+ML {* val ind_r_a = atomize_thm @{thm m2} *}
+  (* prove {* build_regularize_goal ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}
+  apply (simp add: equiv_res_forall[OF equiv_list_eq] equiv_res_exists[OF equiv_list_eq]) done *)
+
 ML {* val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context} *}
 ML {*
   val rt = build_repabs_term @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
@@ -565,7 +565,7 @@
 *}
 (*prove rg
 apply(atomize(full))
-apply (tactic {*  (r_mk_comb_tac_fset @{context}) 1 *})*)
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})*)
 ML {* val (g, thm, othm) =
   Toplevel.program (fn () =>
   repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
@@ -614,95 +614,11 @@
 ML {* lift @{thm m1} *}
 ML {* lift @{thm list_eq.intros(4)} *}
 ML {* lift @{thm list_eq.intros(5)} *}
-
-(* 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 memb_rsp},
-      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_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
-  val cgoal = cterm_of @{theory} goal
-  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
-*}
+(* ML {* lift @{thm length_append} *} *)
 
 (*notation ( output) "prop" ("#_" [1000] 1000) *)
 notation ( output) "Trueprop" ("#_" [1000] 1000)
 
-
-prove {* (Thm.term_of cgoal2) *}
-  apply (tactic {* transconv_fset_tac' @{context} *})
-  done
-
-thm length_append (* Not true but worth checking that the goal is correct *)
-ML {*
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm length_append}))
-  val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
-  val cgoal = cterm_of @{theory} goal
-  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
-*}
-prove {* Thm.term_of cgoal2 *}
-  apply (tactic {* transconv_fset_tac' @{context} *})
-  sorry
-
-thm m2
-ML {*
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))
-  val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
-  val cgoal = cterm_of @{theory} goal
-  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
-*}
-prove {* Thm.term_of cgoal2 *}
-  apply (tactic {* transconv_fset_tac' @{context} *})
-  done
-
-thm list_eq.intros(4)
-ML {*
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(4)}))
-  val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
-  val cgoal = cterm_of @{theory} goal
-  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
-  val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2)
-*}
-
-(* It is the same, but we need a name for it. *)
-prove zzz : {* Thm.term_of cgoal3 *}
-  apply (tactic {* transconv_fset_tac' @{context} *})
-  done
-
-(*lemma zzz' :
-  "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs)))"
-  using list_eq.intros(4) by (simp only: zzz)
-
-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)
-(* prove {* build_repabs_goal @{context} (atomize_thm @{thm list_eq.intros(5)}) consts @{typ "'a list"} @{typ "'a fset"} *} *)
-ML {*
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)}))
-  val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
-  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 {* transconv_fset_tac' @{context} *})
-  done
-
 ML {*
   fun lift_theorem_fset_aux thm lthy =
     let

--- a/QuotScript.thy	Sat Oct 24 13:00:54 2009 +0200
+++ b/QuotScript.thy	Sat Oct 24 14:00:18 2009 +0200
@@ -127,7 +127,7 @@
   "FUN_REL E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
 
 abbreviation
-  FUN_REL_syn (infixr "===>" 55)
+  FUN_REL_syn ("_ ===> _")
 where
   "E1 ===> E2 \<equiv> FUN_REL E1 E2"  
 
@@ -509,7 +509,6 @@
   shows "!f. Ex f = Bex (Respects R) ((absf ---> id) f)"
   sorry
 
-(* Currently fixed, should be general *)
 lemma ho_all_prs: "op = ===> op = ===> op = All All"
   apply (auto)
   done