equal
deleted
inserted
replaced
18 |
18 |
19 subsection\<open>Bounded Quantifiers\<close> |
19 subsection\<open>Bounded Quantifiers\<close> |
20 text \<open>\medskip |
20 text \<open>\medskip |
21 |
21 |
22 The following are not added to the default simpset because |
22 The following are not added to the default simpset because |
23 (a) they duplicate the body and (b) there are no similar rules for @{text Int}.\<close> |
23 (a) they duplicate the body and (b) there are no similar rules for \<open>Int\<close>.\<close> |
24 |
24 |
25 lemma ball_Un: "(\<forall>x \<in> A\<union>B. P(x)) \<longleftrightarrow> (\<forall>x \<in> A. P(x)) & (\<forall>x \<in> B. P(x))" |
25 lemma ball_Un: "(\<forall>x \<in> A\<union>B. P(x)) \<longleftrightarrow> (\<forall>x \<in> A. P(x)) & (\<forall>x \<in> B. P(x))" |
26 by blast |
26 by blast |
27 |
27 |
28 lemma bex_Un: "(\<exists>x \<in> A\<union>B. P(x)) \<longleftrightarrow> (\<exists>x \<in> A. P(x)) | (\<exists>x \<in> B. P(x))" |
28 lemma bex_Un: "(\<exists>x \<in> A\<union>B. P(x)) \<longleftrightarrow> (\<exists>x \<in> A. P(x)) | (\<exists>x \<in> B. P(x))" |