equal
deleted
inserted
replaced
31 text \<open>Some harder ones.\<close> |
31 text \<open>Some harder ones.\<close> |
32 |
32 |
33 lemma "(\<exists>x. P(x) \<or> Q(x)) \<longleftrightarrow> (\<exists>x. P(x)) \<or> (\<exists>x. Q(x))" |
33 lemma "(\<exists>x. P(x) \<or> Q(x)) \<longleftrightarrow> (\<exists>x. P(x)) \<or> (\<exists>x. Q(x))" |
34 by fast |
34 by fast |
35 |
35 |
36 -- \<open>Converse is false.\<close> |
36 \<comment> \<open>Converse is false.\<close> |
37 lemma "(\<exists>x. P(x) \<and> Q(x)) \<longrightarrow> (\<exists>x. P(x)) \<and> (\<exists>x. Q(x))" |
37 lemma "(\<exists>x. P(x) \<and> Q(x)) \<longrightarrow> (\<exists>x. P(x)) \<and> (\<exists>x. Q(x))" |
38 by fast |
38 by fast |
39 |
39 |
40 |
40 |
41 text \<open>Basic test of quantifier reasoning.\<close> |
41 text \<open>Basic test of quantifier reasoning.\<close> |
42 |
42 |
43 -- \<open>TRUE\<close> |
43 \<comment> \<open>TRUE\<close> |
44 lemma "(\<exists>y. \<forall>x. Q(x,y)) \<longrightarrow> (\<forall>x. \<exists>y. Q(x,y))" |
44 lemma "(\<exists>y. \<forall>x. Q(x,y)) \<longrightarrow> (\<forall>x. \<exists>y. Q(x,y))" |
45 by fast |
45 by fast |
46 |
46 |
47 lemma "(\<forall>x. Q(x)) \<longrightarrow> (\<exists>x. Q(x))" |
47 lemma "(\<forall>x. Q(x)) \<longrightarrow> (\<exists>x. Q(x))" |
48 by fast |
48 by fast |
70 text \<open>Back to things that are provable \dots\<close> |
70 text \<open>Back to things that are provable \dots\<close> |
71 |
71 |
72 lemma "(\<forall>x. P(x) \<longrightarrow> Q(x)) \<and> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))" |
72 lemma "(\<forall>x. P(x) \<longrightarrow> Q(x)) \<and> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))" |
73 by fast |
73 by fast |
74 |
74 |
75 text \<open>An example of why @{text exI} should be delayed as long as possible.\<close> |
75 text \<open>An example of why \<open>exI\<close> should be delayed as long as possible.\<close> |
76 lemma "(P \<longrightarrow> (\<exists>x. Q(x))) \<and> P \<longrightarrow> (\<exists>x. Q(x))" |
76 lemma "(P \<longrightarrow> (\<exists>x. Q(x))) \<and> P \<longrightarrow> (\<exists>x. Q(x))" |
77 by fast |
77 by fast |
78 |
78 |
79 schematic_goal "(\<forall>x. P(x) \<longrightarrow> Q(f(x))) \<and> (\<forall>x. Q(x) \<longrightarrow> R(g(x))) \<and> P(d) \<longrightarrow> R(?a)" |
79 schematic_goal "(\<forall>x. P(x) \<longrightarrow> Q(f(x))) \<and> (\<forall>x. Q(x) \<longrightarrow> R(g(x))) \<and> P(d) \<longrightarrow> R(?a)" |
80 by fast |
80 by fast |