--- 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"