--- a/FSet.thy	Sat Oct 24 10:16:53 2009 +0200
+++ b/FSet.thy	Sat Oct 24 13:00:54 2009 +0200
@@ -278,11 +278,11 @@
   let
     val g = build_regularize_goal thm rty rel lthy;
     val tac =
-       (simp_tac ((Simplifier.context lthy HOL_ss) addsimps
+       atac ORELSE' (simp_tac ((Simplifier.context lthy HOL_ss) addsimps
         [(@{thm equiv_res_forall} OF [rel_eqv]),
-         (@{thm equiv_res_exists} OF [rel_eqv])])) THEN'
-         (rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN'
-         (RANGE [fn _ => all_tac, atac]) THEN' (MetisTools.metis_tac lthy []);
+         (@{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);
   in
@@ -392,23 +392,31 @@
 ML Goal.prove
 
 ML {*
-fun repabs lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms =
+fun repabs_eq lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms =
   let
     val rt = build_repabs_term lthy thm constructors rty qty;
     val rg = Logic.mk_equals ((Thm.prop_of thm), rt);
     fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN'
       (REPEAT_ALL_NEW (r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm rsp_thms));
     val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1);
-(*    val tac2 =
-     (simp_tac ((Simplifier.context lthy HOL_ss) addsimps [cthm]))
-     THEN' (rtac thm);
-    val cgoal = cterm_of (ProofContext.theory_of lthy) rt;
-    val cthm = Goal.prove_internal [] cgoal (fn _ => tac2); *)
+  in
+    (rt, cthm, thm)
+  end
+*}
+
+ML {*
+fun repabs_eq2 lthy (rt, thm, othm) =
+  let
+    fun tac2 ctxt =
+     (simp_tac ((Simplifier.context ctxt empty_ss) addsimps [symmetric thm]))
+     THEN' (rtac othm);
+    val cthm = Goal.prove lthy [] [] rt (fn x => tac2 (#context x) 1);
   in
     cthm
   end
 *}
 
+
 ML {*
 fun r_mk_comb_tac_fset ctxt =
   r_mk_comb_tac ctxt @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp}
@@ -430,14 +438,6 @@
 apply (tactic {* rtac thm 1 *})
 done
 
-ML {* val ind_r_a = atomize_thm @{thm list_induct_hol4} *}
-ML {* val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context} *}
-ML {* val ind_r_t =
-  repabs @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
-   @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}
-   @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp}
-*}
-
 thm list.recs(2)
 
 thm m2
@@ -465,21 +465,21 @@
   by (simp add: id_def)
 
 ML {*
- val t = prop_of @{thm LAMBDA_PRS}
- val tt = Drule.instantiate' [SOME @{ctyp "'a list"}, SOME @{ctyp "'a fset"}, SOME @{ctyp "bool"}, SOME @{ctyp "bool"}] [] @{thm LAMBDA_PRS}
- val ttt = @{thm LAMBDA_PRS} OF [@{thm QUOTIENT_fset}, @{thm IDENTITY_QUOTIENT}]
- val tttt = @{thm "HOL.sym"} OF [ttt]
+   val lpis = @{thm LAMBDA_PRS} OF [@{thm QUOTIENT_fset}, @{thm IDENTITY_QUOTIENT}];
+   val lpist = @{thm "HOL.sym"} OF [lpis];
+   val lam_prs = MetaSimplifier.rewrite_rule [@{thm id_apply2}] lpist
 *}
+
+text {* the proper way to do it *}
 ML {*
- val ttttt = MetaSimplifier.rewrite_rule [@{thm id_apply2}] tttt
- val zzz = @{thm m2_t}
+ val lpi = Drule.instantiate'
+   [SOME @{ctyp "'a list"}, SOME @{ctyp "'a fset"}, SOME @{ctyp "bool"}, SOME @{ctyp "bool"}] [] @{thm LAMBDA_PRS};
 *}
-prove asdfasdf : {* concl_of tt *}
+prove asdfasdf : {* concl_of lpi *}
 apply (tactic {* compose_tac (false, @{thm LAMBDA_PRS}, 2) 1 *})
 apply (tactic {* quotient_tac @{thm QUOTIENT_fset} 1 *})
 apply (tactic {* quotient_tac @{thm QUOTIENT_fset} 1 *})
 done
-
 thm HOL.sym[OF asdfasdf,simplified]
 
 ML {*
@@ -496,11 +496,31 @@
     Simplifier.rewrite_rule [rt] thm
   end
 *}
-ML ttttt
-ML {* val m2_t' = eqsubst_thm @{context} @{thms HOL.sym[OF asdfasdf,simplified]} @{thm m2_t} *}
-ML {* val rwr = @{thm FORALL_PRS[OF QUOTIENT_fset]} *}
-ML {* val rwrs = @{thm "HOL.sym"} OF [spec OF [rwr]] *}
-ML {* val ithm = eqsubst_thm @{context} [rwrs] m2_t' *}
+
+(* @{thms HOL.sym[OF asdfasdf,simplified]} *)
+
+ML {*
+  fun simp_lam_prs lthy thm = 
+    simp_lam_prs lthy (eqsubst_thm lthy [lam_prs] thm)
+    handle _ => thm
+*}
+
+ML {* val m2_t' = eqsubst_thm @{context} [lam_prs] @{thm m2_t} *}
+
+ML {*
+  fun simp_allex_prs lthy thm =
+    let
+      val rwf = @{thm FORALL_PRS[OF QUOTIENT_fset]};
+      val rwfs = @{thm "HOL.sym"} OF [spec OF [rwf]];
+      val rwe = @{thm EXISTS_PRS[OF QUOTIENT_fset]};
+      val rwes = @{thm "HOL.sym"} OF [spec OF [rwe]]
+    in
+      (simp_allex_prs lthy (eqsubst_thm lthy [rwfs, rwes] thm))
+    end
+    handle _ => thm
+*}
+
+ML {* val ithm = simp_allex_prs @{context} m2_t' *}
 ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *}
 ML {* ObjectLogic.rulify rthm *}
 
@@ -529,101 +549,71 @@
 ML {* val card1_suc_t_n = @{thm card1_suc_t} *}
 ML {* val card1_suc_t' = eqsubst_thm @{context} @{thms HOL.sym[OF asdfasdf,simplified]} @{thm card1_suc_t} *}
 ML {* val card1_suc_t'' = eqsubst_thm @{context} @{thms HOL.sym[OF asdfasdf,simplified]} card1_suc_t' *}
-ML {* val ithm = eqsubst_thm @{context} [rwrs] card1_suc_t'' *}
-ML {* val rwr = @{thm EXISTS_PRS[OF QUOTIENT_fset]} *}
-ML {* val rwrs = @{thm "HOL.sym"} OF [spec OF [rwr]] *}
-ML {* val jthm = eqsubst_thm @{context} [rwrs] ithm *}
-ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym jthm *}
+ML {* val ithm = simp_allex_prs @{context} card1_suc_t'' *}
+ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *}
 ML {* val qthm = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} rthm *}
 ML {* ObjectLogic.rulify qthm *}
 
-
-ML {* val li = Thm.freezeT (atomize_thm @{thm fold1.simps(2)}) *}
-prove fold1_def_2_r: {*
- Logic.mk_implies
-   ((prop_of li),
-   (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *}
-  apply (simp add: equiv_res_forall[OF equiv_list_eq])
-  done
-
-ML {* @{thm fold1_def_2_r} OF [li] *}
+thm fold1.simps(2)
 
 
-lemma yy:
-  shows "(False = x memb []) = (False = IN (x::nat) EMPTY)"
-unfolding IN_def EMPTY_def
-apply(rule_tac f="(op =) False" in arg_cong)
-apply(rule memb_rsp)
-apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
-apply(rule list_eq.intros)
-done
-
-lemma
-  shows "IN (x::nat) EMPTY = False"
-using m1
-apply -
-apply(rule yy[THEN iffD1, symmetric])
-apply(simp)
-done
-
-lemma
-  shows "((x=y) \<or> (IN x xs) = (IN (x::nat) (INSERT y xs))) =
-         ((x=y) \<or> x memb REP_fset xs = x memb (y # REP_fset xs))"
-unfolding IN_def INSERT_def
-apply(rule_tac f="(op \<or>) (x=y)" in arg_cong)
-apply(rule_tac f="(op =) (x memb REP_fset xs)" in arg_cong)
-apply(rule memb_rsp)
-apply(rule list_eq.intros(3))
-apply(unfold REP_fset_def ABS_fset_def)
-apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])
-apply(rule list_eq_refl)
-done
-
-lemma yyy:
-  shows "
-    (
-     (UNION EMPTY s = s) &
-     ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))
-    ) = (
-     ((ABS_fset ([] @ REP_fset s)) = s) &
-     ((ABS_fset ((e # (REP_fset s1)) @ REP_fset s2)) = ABS_fset (e # (REP_fset s1 @ REP_fset s2)))
-    )"
-  unfolding UNION_def EMPTY_def INSERT_def
-  apply(rule_tac f="(op &)" in arg_cong2)
-  apply(rule_tac f="(op =)" in arg_cong2)
-  apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
-  apply(rule append_respects_fst)
-  apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
-  apply(rule list_eq_refl)
-  apply(simp)
-  apply(rule_tac f="(op =)" in arg_cong2)
-  apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
-  apply(rule append_respects_fst)
-  apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
-  apply(rule list_eq_refl)
-  apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
-  apply(rule list_eq.intros(5))
-  apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
-  apply(rule list_eq_refl)
-done
-
-lemma
-  shows "
-     (UNION EMPTY s = s) &
-     ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))"
-  apply (simp add: yyy)
-  apply (simp add: QUOT_TYPE_I_fset.thm10)
-  done
+ML {* val ind_r_a = atomize_thm @{thm fold1.simps(2)} *}
+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"}
+  val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt);
+*}
+(*prove rg
+apply(atomize(full))
+apply (tactic {*  (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"}
+   @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}
+   @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp}
+  )
+*}
+ML {*
+    fun tac2 ctxt =
+     (simp_tac ((Simplifier.context ctxt empty_ss) addsimps [symmetric thm]))
+     THEN' (rtac othm); *}
+(* ML {*    val cthm = Goal.prove @{context} [] [] g (fn x => tac2 (#context x) 1);
+*} *)
 
 ML {*
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))
+  val ind_r_t2 =
+  Toplevel.program (fn () =>
+    repabs_eq2 @{context} (g, thm, othm)
+  )
 *}
+ML {* val ind_r_l = simp_lam_prs @{context} ind_r_t2 *}
+ML {* val ind_r_a = simp_allex_prs @{context} ind_r_l *}
+ML {* val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a *}
+ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *}
 
 ML {*
-cterm_of @{theory} (prop_of m1_novars);
-cterm_of @{theory} (build_repabs_term @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"});
+fun lift thm =
+let
+  val ind_r_a = atomize_thm thm;
+  val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context};
+  val (g, t, ot) =
+    repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
+     @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}
+     @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp};
+  val ind_r_t = repabs_eq2 @{context} (g, t, ot);
+  val ind_r_l = simp_lam_prs @{context} ind_r_t;
+  val ind_r_a = simp_allex_prs @{context} ind_r_l;
+  val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a;
+  val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d
+in
+  ObjectLogic.rulify ind_r_s
+end
 *}
 
+ML {* lift @{thm m2} *}
+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 {*

--- a/QuotScript.thy	Sat Oct 24 10:16:53 2009 +0200
+++ b/QuotScript.thy	Sat Oct 24 13:00:54 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 ("_ ===> _")
+  FUN_REL_syn (infixr "===>" 55)
 where
   "E1 ===> E2 \<equiv> FUN_REL E1 E2"  
 
@@ -509,6 +509,7 @@
   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