diff -r aa452130ae7f -r 1dd6a21cdd1c FSet.thy
--- 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