--- a/FSet.thy	Wed Nov 25 15:43:12 2009 +0100
+++ b/FSet.thy	Thu Nov 26 02:31:00 2009 +0100
@@ -345,12 +345,48 @@
 
 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *}
 ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *}
+
+lemma cheat: "P" sorry
+
+lemma imp_refl: "P \<longrightarrow> P" by simp
+
+thm Set.conj_mono
+thm Set.imp_mono
+ML {* Inductive.get_monos @{context} *}
+
 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
-apply (tactic {* lift_tac_fset @{context} @{thm list.induct} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *})
-apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
+apply(tactic {* procedure_tac @{thm list.induct} @{context} 1 *})
+defer
+apply(rule cheat)
+apply(rule cheat)
+apply(atomize (full))
+apply(rule my_equiv_res_forallR)
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply(rule my_equiv_res_forallR)
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply(rule Set.imp_mono)
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply(rule my_equiv_res_forallL)
+apply(rule cheat)
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
 done
 
+lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
+apply(tactic {* procedure_tac @{thm list.induct} @{context} 1 *})
+defer
+apply(rule cheat)
+apply(rule cheat)
+apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *})
+oops
+
 quotient_def
   fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 where

--- a/QuotMain.thy	Wed Nov 25 15:43:12 2009 +0100
+++ b/QuotMain.thy	Thu Nov 26 02:31:00 2009 +0100
@@ -474,23 +474,40 @@
 
 *)
 
-lemma my_equiv_res_forall2:
+lemma my_equiv_res_forallR:
   fixes P::"'a \<Rightarrow> bool"
   fixes Q::"'b \<Rightarrow> bool"
-  assumes a: "(All Q) \<longrightarrow> (All P)"
+  assumes b: "(All Q) \<longrightarrow> (All P)"
   shows "(All Q) \<longrightarrow> Ball (Respects E) P"
-using a by auto
+using b by auto
 
-lemma my_equiv_res_exists:
+lemma my_equiv_res_forallL:
+  fixes P::"'a \<Rightarrow> bool"
+  fixes Q::"'b \<Rightarrow> bool"
+  assumes a: "EQUIV E"
+  assumes b: "(All Q) \<longrightarrow> (All P)"
+  shows "Ball (Respects E) P \<longrightarrow> (All P)"
+using a b
+unfolding EQUIV_def
+by (metis IN_RESPECTS)
+
+lemma my_equiv_res_existsR:
   fixes P::"'a \<Rightarrow> bool"
   fixes Q::"'b \<Rightarrow> bool"
   assumes a: "EQUIV E"
   and     b: "(Ex Q) \<longrightarrow> (Ex P)"
   shows "(Ex Q) \<longrightarrow> Bex (Respects E) P"
-apply(subst equiv_res_exists)
-apply(rule a)
-apply(rule b)
-done
+using a b
+unfolding EQUIV_def
+by (metis IN_RESPECTS)
+
+lemma my_equiv_res_existsL:
+  fixes P::"'a \<Rightarrow> bool"
+  fixes Q::"'b \<Rightarrow> bool"
+  assumes b: "(Ex Q) \<longrightarrow> (Ex P)"
+  shows "Bex (Respects E) Q \<longrightarrow> (Ex P)"
+using b
+by (auto)
 
 lemma universal_twice:
   assumes *: "\<And>x. (P x \<longrightarrow> Q x)"
@@ -499,26 +516,10 @@
 
 lemma implication_twice:
   assumes a: "c \<longrightarrow> a"
-  assumes b: "a \<Longrightarrow> b \<longrightarrow> d"
+  assumes b: "b \<longrightarrow> d"
   shows "(a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
 using a b by auto
 
-ML {*
-(* FIXME: get_rid of rel_refl rel_eqv *)
-fun REGULARIZE_tac lthy rel_refl rel_eqv =
-   (REPEAT1 o FIRST1) 
-     [rtac rel_refl,
-      atac,
-      rtac @{thm universal_twice},
-      rtac @{thm impI} THEN' atac,
-      rtac @{thm implication_twice},
-      rtac @{thm my_equiv_res_forall2},
-      rtac (rel_eqv RS @{thm my_equiv_res_exists}),
-      (* For a = b \<longrightarrow> a \<approx> b *)
-      rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl,
-      rtac @{thm RIGHT_RES_FORALL_REGULAR}]
-*}
-
 (* version of REGULARIZE_tac including debugging information *)
 ML {*
 fun my_print_tac ctxt s thm =
@@ -543,8 +544,8 @@
       DT lthy "3" (rtac @{thm universal_twice}),
       DT lthy "4" (rtac @{thm impI} THEN' atac),
       DT lthy "5" (rtac @{thm implication_twice}),
-      DT lthy "6" (rtac @{thm my_equiv_res_forall2}),
-      DT lthy "7" (rtac (rel_eqv RS @{thm my_equiv_res_exists})),
+      DT lthy "6" (rtac @{thm my_equiv_res_forallR}),
+      DT lthy "7" (rtac (rel_eqv RS @{thm my_equiv_res_existsR})),
       (* For a = b \<longrightarrow> a \<approx> b *)
       DT lthy "8" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
       DT lthy "9" (rtac @{thm RIGHT_RES_FORALL_REGULAR})]
@@ -557,7 +558,7 @@
     rtac rel_refl,
     atac,
     rtac @{thm universal_twice},
-    (rtac @{thm impI} THEN' atac),
+    rtac @{thm impI} THEN' atac,
     rtac @{thm implication_twice},
     EqSubst.eqsubst_tac ctxt [0]
       [(@{thm equiv_res_forall} OF [rel_eqv]),
@@ -568,11 +569,30 @@
   ]);
 *}
 
+ML {*
+fun regularize_tac ctxt rel_eqv rel_refl =
+  (ObjectLogic.full_atomize_tac) THEN'
+  REPEAT_ALL_NEW (FIRST' 
+   [(K (print_tac "start")) THEN' (K no_tac), 
+    DT ctxt "1" (rtac rel_refl),
+    DT ctxt "2" atac,
+    DT ctxt "3" (rtac @{thm universal_twice}),
+    DT ctxt "4" (rtac @{thm impI} THEN' atac),
+    DT ctxt "5" (rtac @{thm implication_twice}),
+    DT ctxt "6" (EqSubst.eqsubst_tac ctxt [0]
+      [(@{thm equiv_res_forall} OF [rel_eqv]),
+       (@{thm equiv_res_exists} OF [rel_eqv])]),
+    (* For a = b \<longrightarrow> a \<approx> b *)
+    DT ctxt "7" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
+    DT ctxt "8" (rtac @{thm RIGHT_RES_FORALL_REGULAR})
+  ]);
+*}
+
+thm RIGHT_RES_FORALL_REGULAR
+
+section {* Injections of REP and ABSes *}
 
 (*
-Injections of REP and Abses
-***************************
-
 Injecting REPABS means:
 
   For abstractions: