Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
QuotScript.thy
changeset 432 9c33c0809733
parent 427 5a3965aa4d80
child 458 44a70e69ef92 
--- a/QuotScript.thy	Sat Nov 28 04:02:54 2009 +0100
+++ b/QuotScript.thy	Sat Nov 28 05:29:30 2009 +0100
@@ -517,6 +517,13 @@
   shows "Bex R Q"
   using a b by (metis COMBC_def Collect_def Collect_mem_eq)
 
+lemma ball_all_comm:
+  "(\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<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 bex_ex_comm:
+  "((\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)) \<Longrightarrow> ((\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y))"
+by auto
nominal2