--- a/FSet.thy	Thu Nov 26 16:23:24 2009 +0100
+++ b/FSet.thy	Thu Nov 26 19:51:31 2009 +0100
@@ -346,78 +346,12 @@
 
 lemma cheat: "P" sorry
 
-lemma imp_refl: "P \<longrightarrow> P" by simp
-
-lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P"
-apply(auto)
-done
-
-thm Set.conj_mono
-thm Set.imp_mono
-ML {* Inductive.get_monos @{context} *}
-thm LEFT_RES_FORALL_REGULAR
-
-lemma test: 
-  fixes P Q::"'a \<Rightarrow> bool"  
-  and x::"'a"
-  assumes a: "REFL R2"
-  and     b: "\<And>f. Q (f x) \<Longrightarrow> P (f x)"
-  shows "(\<forall>f\<in>(Respects (R1 ===> R2)). Q (f x)) \<longrightarrow> (\<forall>f. P (f x))"
-apply(rule impI)
-apply(rule allI)
-apply(drule_tac x="\<lambda>y. f x" in bspec)
-apply(simp add: Respects_def IN_RESPECTS)
-apply(rule impI)
-using a
-apply(simp add: REFL_def)
-using b
-apply -
-apply(simp)
-done
-
 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
-defer
-apply(rule cheat)
 apply(rule cheat)
-apply(atomize (full))
-apply(rule RIGHT_RES_FORALL_REGULAR)
-apply(rule RIGHT_RES_FORALL_REGULAR)
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+
-apply(rule LEFT_RES_FORALL_REGULAR)
-apply(rule conjI)
-using list_eq_refl
-thm Ball_def IN_RESPECTS FUN_REL.simps
-
-apply -
-apply(simp (no_asm) add: Respects_def)
-apply(blast)
-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 *})
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply(rule LEFT_RES_FORALL_REGULAR)
-apply(rule conjI)
-defer
-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 *})
-apply(unfold Respects_def)
-sorry
-
-lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
-apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
-defer
+prefer 2
 apply(rule cheat)
-apply(rule cheat)
-apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *})
-done
+apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
 
 quotient_def
   fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"