# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259239560 -3600
# Node ID 90e58455b2191c9cd0e24ce0086c2bcc7496834c
# Parent  199d1ae1401faaf990c0df8dc9b63425ce3cc059
changed left-res

diff -r 199d1ae1401f -r 90e58455b219 FSet.thy
--- a/FSet.thy	Thu Nov 26 12:21:47 2009 +0100
+++ b/FSet.thy	Thu Nov 26 13:46:00 2009 +0100
@@ -348,6 +348,10 @@
 
 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} *}
@@ -365,7 +369,10 @@
 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(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)
@@ -375,6 +382,7 @@
 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"
diff -r 199d1ae1401f -r 90e58455b219 QuotScript.thy
--- a/QuotScript.thy	Thu Nov 26 12:21:47 2009 +0100
+++ b/QuotScript.thy	Thu Nov 26 13:46:00 2009 +0100
@@ -482,13 +482,13 @@
   done
 
 lemma LEFT_RES_EXISTS_REGULAR:
-  assumes a: "!x :: 'a. (R x --> Q x --> P x)"
-  shows "Bex R Q ==> Ex P"
+  assumes a: "!x :: 'a. (R x \<Longrightarrow> Q x \<longrightarrow> P x)"
+  shows "Bex R Q \<longrightarrow> Ex P"
   using a by (metis COMBC_def Collect_def Collect_mem_eq)
 
 lemma RIGHT_RES_EXISTS_REGULAR:
-  assumes a: "!x :: 'a. (R x \<and> (P x --> Q x))"
-  shows "Ex P \<Longrightarrow> Bex R Q"
+  assumes a: "!x :: 'a. (R x \<and> (P x \<longrightarrow> Q x))"
+  shows "Ex P \<longrightarrow> Bex R Q"
   using a by (metis COMBC_def Collect_def Collect_mem_eq)
 
 (* TODO: Add similar *)