--- a/FSet.thy	Thu Nov 26 13:52:46 2009 +0100
+++ b/FSet.thy	Thu Nov 26 16:23:24 2009 +0100
@@ -355,6 +355,25 @@
 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 *})
@@ -362,10 +381,17 @@
 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(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 *})
@@ -373,17 +399,17 @@
 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 my_equiv_res_forallL)
-apply(rule cheat)
+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(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-done
+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 *})