FSet.thy
changeset 395 90e58455b219
parent 392 98ccde1c184c
child 397 559c01f40bee
--- 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"