# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259249004 -3600
# Node ID 559c01f40beeeed3bb6e732d0efc400614dacf9e
# Parent  7a1ab11ab02379b2481147e38072ad66124119c2
introduced a new property for Ball and ===> on the left

diff -r 7a1ab11ab023 -r 559c01f40bee FSet.thy
--- 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 *})
diff -r 7a1ab11ab023 -r 559c01f40bee LFex.thy
--- 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)