1537 lemma ex_in_conv: "(\<exists>x. x \<in> A) = (A \<noteq> {})" |
1537 lemma ex_in_conv: "(\<exists>x. x \<in> A) = (A \<noteq> {})" |
1538 by blast |
1538 by blast |
1539 |
1539 |
1540 lemma distinct_lemma: "f x \<noteq> f y ==> x \<noteq> y" |
1540 lemma distinct_lemma: "f x \<noteq> f y ==> x \<noteq> y" |
1541 by iprover |
1541 by iprover |
|
1542 |
|
1543 lemma ball_simps [simp, no_atp]: |
|
1544 "\<And>A P Q. (\<forall>x\<in>A. P x \<or> Q) \<longleftrightarrow> ((\<forall>x\<in>A. P x) \<or> Q)" |
|
1545 "\<And>A P Q. (\<forall>x\<in>A. P \<or> Q x) \<longleftrightarrow> (P \<or> (\<forall>x\<in>A. Q x))" |
|
1546 "\<And>A P Q. (\<forall>x\<in>A. P \<longrightarrow> Q x) \<longleftrightarrow> (P \<longrightarrow> (\<forall>x\<in>A. Q x))" |
|
1547 "\<And>A P Q. (\<forall>x\<in>A. P x \<longrightarrow> Q) \<longleftrightarrow> ((\<exists>x\<in>A. P x) \<longrightarrow> Q)" |
|
1548 "\<And>P. (\<forall>x\<in>{}. P x) \<longleftrightarrow> True" |
|
1549 "\<And>P. (\<forall>x\<in>UNIV. P x) \<longleftrightarrow> (\<forall>x. P x)" |
|
1550 "\<And>a B P. (\<forall>x\<in>insert a B. P x) \<longleftrightarrow> (P a \<and> (\<forall>x\<in>B. P x))" |
|
1551 "\<And>P Q. (\<forall>x\<in>Collect Q. P x) \<longleftrightarrow> (\<forall>x. Q x \<longrightarrow> P x)" |
|
1552 "\<And>A P f. (\<forall>x\<in>f`A. P x) \<longleftrightarrow> (\<forall>x\<in>A. P (f x))" |
|
1553 "\<And>A P. (\<not> (\<forall>x\<in>A. P x)) \<longleftrightarrow> (\<exists>x\<in>A. \<not> P x)" |
|
1554 by auto |
|
1555 |
|
1556 lemma bex_simps [simp, no_atp]: |
|
1557 "\<And>A P Q. (\<exists>x\<in>A. P x \<and> Q) \<longleftrightarrow> ((\<exists>x\<in>A. P x) \<and> Q)" |
|
1558 "\<And>A P Q. (\<exists>x\<in>A. P \<and> Q x) \<longleftrightarrow> (P \<and> (\<exists>x\<in>A. Q x))" |
|
1559 "\<And>P. (\<exists>x\<in>{}. P x) \<longleftrightarrow> False" |
|
1560 "\<And>P. (\<exists>x\<in>UNIV. P x) \<longleftrightarrow> (\<exists>x. P x)" |
|
1561 "\<And>a B P. (\<exists>x\<in>insert a B. P x) \<longleftrightarrow> (P a | (\<exists>x\<in>B. P x))" |
|
1562 "\<And>P Q. (\<exists>x\<in>Collect Q. P x) \<longleftrightarrow> (\<exists>x. Q x \<and> P x)" |
|
1563 "\<And>A P f. (\<exists>x\<in>f`A. P x) \<longleftrightarrow> (\<exists>x\<in>A. P (f x))" |
|
1564 "\<And>A P. (\<not>(\<exists>x\<in>A. P x)) \<longleftrightarrow> (\<forall>x\<in>A. \<not> P x)" |
|
1565 by auto |
1542 |
1566 |
1543 |
1567 |
1544 subsubsection {* Monotonicity of various operations *} |
1568 subsubsection {* Monotonicity of various operations *} |
1545 |
1569 |
1546 lemma image_mono: "A \<subseteq> B ==> f`A \<subseteq> f`B" |
1570 lemma image_mono: "A \<subseteq> B ==> f`A \<subseteq> f`B" |