--- a/LFex.thy	Thu Nov 26 13:52:46 2009 +0100
+++ b/LFex.thy	Thu Nov 26 16:23:24 2009 +0100
@@ -249,6 +249,27 @@
 lemma move_quant: "((\<forall>y. \<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>y. \<forall>x. B x y)) \<Longrightarrow> ((\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y))"
 by auto
 
+lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P"
+apply(auto)
+done
+
+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   "(Ball (Respects (R1 ===> R2)) (\<lambda>f. Q (f x)) \<longrightarrow> All (\<lambda>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(simp)
+done
+
 lemma "\<lbrakk>P1 TYP TYP; \<And>A A' K K' x. \<lbrakk>(A::TY) = A'; P2 A A'; (K::KIND) = K'; P1 K K'\<rbrakk> \<Longrightarrow> P1 (KPI A x K) (KPI A' x K');
  \<And>A A' K x x' K'.
     \<lbrakk>(A ::TY) = A'; P2 A A'; (K :: KIND) = ([(x, x')] \<bullet> K'); P1 K ([(x, x')] \<bullet> K'); x \<notin> FV_ty A'; x \<notin> FV_kind K' - {x'}\<rbrakk>
@@ -273,13 +294,54 @@
 apply(rule RIGHT_RES_FORALL_REGULAR)
 apply(rule RIGHT_RES_FORALL_REGULAR)
 apply(rule RIGHT_RES_FORALL_REGULAR)
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+
+apply(rule test)
+defer
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+
+apply(rule test)
+defer
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+
+apply(rule move_quant)
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+
+apply(rule move_quant)
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+
+apply(rule move_quant)
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+
+apply(rule test)
+defer
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+
+
+
+thm test[OF mp]
+
+
+prefer 2
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+
+apply(thin_tac "Respects (akind ===> akind ===> op =) x") 
+apply(thin_tac "Respects (aty ===> aty ===> op =) xa")
+apply(thin_tac "Respects (atrm ===> atrm ===> op =) xb")
+apply (simp add: Ball_def IN_RESPECTS Respects_def)
+apply (metis COMBK_def al_refl(3))
+
+apply(rule LEFT_RES_FORALL_REGULAR)
+apply(rule conjI)
+prefer 2
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+
+using al_refl
+apply(simp add: Respects_def)
+
+
 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 Set.imp_mono)
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply (simp add: Ball_def IN_RESPECTS Respects_def)
+apply (metis COMBK_def al_refl(3))
+
 apply(rule impI) apply(assumption)
 apply(rule Set.imp_mono)
 apply(rule impI) apply(assumption)