8 theory Quantifiers_Int |
8 theory Quantifiers_Int |
9 imports IFOL |
9 imports IFOL |
10 begin |
10 begin |
11 |
11 |
12 lemma \<open>(\<forall>x y. P(x,y)) \<longrightarrow> (\<forall>y x. P(x,y))\<close> |
12 lemma \<open>(\<forall>x y. P(x,y)) \<longrightarrow> (\<forall>y x. P(x,y))\<close> |
13 by (tactic "IntPr.fast_tac @{context} 1") |
13 by (tactic "IntPr.fast_tac \<^context> 1") |
14 |
14 |
15 lemma \<open>(\<exists>x y. P(x,y)) \<longrightarrow> (\<exists>y x. P(x,y))\<close> |
15 lemma \<open>(\<exists>x y. P(x,y)) \<longrightarrow> (\<exists>y x. P(x,y))\<close> |
16 by (tactic "IntPr.fast_tac @{context} 1") |
16 by (tactic "IntPr.fast_tac \<^context> 1") |
17 |
17 |
18 |
18 |
19 \<comment> \<open>Converse is false\<close> |
19 \<comment> \<open>Converse is false\<close> |
20 lemma \<open>(\<forall>x. P(x)) \<or> (\<forall>x. Q(x)) \<longrightarrow> (\<forall>x. P(x) \<or> Q(x))\<close> |
20 lemma \<open>(\<forall>x. P(x)) \<or> (\<forall>x. Q(x)) \<longrightarrow> (\<forall>x. P(x) \<or> Q(x))\<close> |
21 by (tactic "IntPr.fast_tac @{context} 1") |
21 by (tactic "IntPr.fast_tac \<^context> 1") |
22 |
22 |
23 lemma \<open>(\<forall>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<forall>x. Q(x)))\<close> |
23 lemma \<open>(\<forall>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<forall>x. Q(x)))\<close> |
24 by (tactic "IntPr.fast_tac @{context} 1") |
24 by (tactic "IntPr.fast_tac \<^context> 1") |
25 |
25 |
26 |
26 |
27 lemma \<open>(\<forall>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> ((\<exists>x. P(x)) \<longrightarrow> Q)\<close> |
27 lemma \<open>(\<forall>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> ((\<exists>x. P(x)) \<longrightarrow> Q)\<close> |
28 by (tactic "IntPr.fast_tac @{context} 1") |
28 by (tactic "IntPr.fast_tac \<^context> 1") |
29 |
29 |
30 |
30 |
31 text \<open>Some harder ones\<close> |
31 text \<open>Some harder ones\<close> |
32 |
32 |
33 lemma \<open>(\<exists>x. P(x) \<or> Q(x)) \<longleftrightarrow> (\<exists>x. P(x)) \<or> (\<exists>x. Q(x))\<close> |
33 lemma \<open>(\<exists>x. P(x) \<or> Q(x)) \<longleftrightarrow> (\<exists>x. P(x)) \<or> (\<exists>x. Q(x))\<close> |
34 by (tactic "IntPr.fast_tac @{context} 1") |
34 by (tactic "IntPr.fast_tac \<^context> 1") |
35 |
35 |
36 \<comment> \<open>Converse is false\<close> |
36 \<comment> \<open>Converse is false\<close> |
37 lemma \<open>(\<exists>x. P(x) \<and> Q(x)) \<longrightarrow> (\<exists>x. P(x)) \<and> (\<exists>x. Q(x))\<close> |
37 lemma \<open>(\<exists>x. P(x) \<and> Q(x)) \<longrightarrow> (\<exists>x. P(x)) \<and> (\<exists>x. Q(x))\<close> |
38 by (tactic "IntPr.fast_tac @{context} 1") |
38 by (tactic "IntPr.fast_tac \<^context> 1") |
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 \<comment> \<open>TRUE\<close> |
43 \<comment> \<open>TRUE\<close> |
44 lemma \<open>(\<exists>y. \<forall>x. Q(x,y)) \<longrightarrow> (\<forall>x. \<exists>y. Q(x,y))\<close> |
44 lemma \<open>(\<exists>y. \<forall>x. Q(x,y)) \<longrightarrow> (\<forall>x. \<exists>y. Q(x,y))\<close> |
45 by (tactic "IntPr.fast_tac @{context} 1") |
45 by (tactic "IntPr.fast_tac \<^context> 1") |
46 |
46 |
47 lemma \<open>(\<forall>x. Q(x)) \<longrightarrow> (\<exists>x. Q(x))\<close> |
47 lemma \<open>(\<forall>x. Q(x)) \<longrightarrow> (\<exists>x. Q(x))\<close> |
48 by (tactic "IntPr.fast_tac @{context} 1") |
48 by (tactic "IntPr.fast_tac \<^context> 1") |
49 |
49 |
50 |
50 |
51 text \<open>The following should fail, as they are false!\<close> |
51 text \<open>The following should fail, as they are false!\<close> |
52 |
52 |
53 lemma \<open>(\<forall>x. \<exists>y. Q(x,y)) \<longrightarrow> (\<exists>y. \<forall>x. Q(x,y))\<close> |
53 lemma \<open>(\<forall>x. \<exists>y. Q(x,y)) \<longrightarrow> (\<exists>y. \<forall>x. Q(x,y))\<close> |
54 apply (tactic "IntPr.fast_tac @{context} 1")? |
54 apply (tactic "IntPr.fast_tac \<^context> 1")? |
55 oops |
55 oops |
56 |
56 |
57 lemma \<open>(\<exists>x. Q(x)) \<longrightarrow> (\<forall>x. Q(x))\<close> |
57 lemma \<open>(\<exists>x. Q(x)) \<longrightarrow> (\<forall>x. Q(x))\<close> |
58 apply (tactic "IntPr.fast_tac @{context} 1")? |
58 apply (tactic "IntPr.fast_tac \<^context> 1")? |
59 oops |
59 oops |
60 |
60 |
61 schematic_goal \<open>P(?a) \<longrightarrow> (\<forall>x. P(x))\<close> |
61 schematic_goal \<open>P(?a) \<longrightarrow> (\<forall>x. P(x))\<close> |
62 apply (tactic "IntPr.fast_tac @{context} 1")? |
62 apply (tactic "IntPr.fast_tac \<^context> 1")? |
63 oops |
63 oops |
64 |
64 |
65 schematic_goal \<open>(P(?a) \<longrightarrow> (\<forall>x. Q(x))) \<longrightarrow> (\<forall>x. P(x) \<longrightarrow> Q(x))\<close> |
65 schematic_goal \<open>(P(?a) \<longrightarrow> (\<forall>x. Q(x))) \<longrightarrow> (\<forall>x. P(x) \<longrightarrow> Q(x))\<close> |
66 apply (tactic "IntPr.fast_tac @{context} 1")? |
66 apply (tactic "IntPr.fast_tac \<^context> 1")? |
67 oops |
67 oops |
68 |
68 |
69 |
69 |
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 \<open>(\<forall>x. P(x) \<longrightarrow> Q(x)) \<and> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))\<close> |
72 lemma \<open>(\<forall>x. P(x) \<longrightarrow> Q(x)) \<and> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))\<close> |
73 by (tactic "IntPr.fast_tac @{context} 1") |
73 by (tactic "IntPr.fast_tac \<^context> 1") |
74 |
74 |
75 \<comment> \<open>An example of why exI should be delayed as long as possible\<close> |
75 \<comment> \<open>An example of why exI should be delayed as long as possible\<close> |
76 lemma \<open>(P \<longrightarrow> (\<exists>x. Q(x))) \<and> P \<longrightarrow> (\<exists>x. Q(x))\<close> |
76 lemma \<open>(P \<longrightarrow> (\<exists>x. Q(x))) \<and> P \<longrightarrow> (\<exists>x. Q(x))\<close> |
77 by (tactic "IntPr.fast_tac @{context} 1") |
77 by (tactic "IntPr.fast_tac \<^context> 1") |
78 |
78 |
79 schematic_goal \<open>(\<forall>x. P(x) \<longrightarrow> Q(f(x))) \<and> (\<forall>x. Q(x) \<longrightarrow> R(g(x))) \<and> P(d) \<longrightarrow> R(?a)\<close> |
79 schematic_goal \<open>(\<forall>x. P(x) \<longrightarrow> Q(f(x))) \<and> (\<forall>x. Q(x) \<longrightarrow> R(g(x))) \<and> P(d) \<longrightarrow> R(?a)\<close> |
80 by (tactic "IntPr.fast_tac @{context} 1") |
80 by (tactic "IntPr.fast_tac \<^context> 1") |
81 |
81 |
82 lemma \<open>(\<forall>x. Q(x)) \<longrightarrow> (\<exists>x. Q(x))\<close> |
82 lemma \<open>(\<forall>x. Q(x)) \<longrightarrow> (\<exists>x. Q(x))\<close> |
83 by (tactic "IntPr.fast_tac @{context} 1") |
83 by (tactic "IntPr.fast_tac \<^context> 1") |
84 |
84 |
85 |
85 |
86 text \<open>Some slow ones\<close> |
86 text \<open>Some slow ones\<close> |
87 |
87 |
88 \<comment> \<open>Principia Mathematica *11.53\<close> |
88 \<comment> \<open>Principia Mathematica *11.53\<close> |
89 lemma \<open>(\<forall>x y. P(x) \<longrightarrow> Q(y)) \<longleftrightarrow> ((\<exists>x. P(x)) \<longrightarrow> (\<forall>y. Q(y)))\<close> |
89 lemma \<open>(\<forall>x y. P(x) \<longrightarrow> Q(y)) \<longleftrightarrow> ((\<exists>x. P(x)) \<longrightarrow> (\<forall>y. Q(y)))\<close> |
90 by (tactic "IntPr.fast_tac @{context} 1") |
90 by (tactic "IntPr.fast_tac \<^context> 1") |
91 |
91 |
92 (*Principia Mathematica *11.55 *) |
92 (*Principia Mathematica *11.55 *) |
93 lemma \<open>(\<exists>x y. P(x) \<and> Q(x,y)) \<longleftrightarrow> (\<exists>x. P(x) \<and> (\<exists>y. Q(x,y)))\<close> |
93 lemma \<open>(\<exists>x y. P(x) \<and> Q(x,y)) \<longleftrightarrow> (\<exists>x. P(x) \<and> (\<exists>y. Q(x,y)))\<close> |
94 by (tactic "IntPr.fast_tac @{context} 1") |
94 by (tactic "IntPr.fast_tac \<^context> 1") |
95 |
95 |
96 (*Principia Mathematica *11.61 *) |
96 (*Principia Mathematica *11.61 *) |
97 lemma \<open>(\<exists>y. \<forall>x. P(x) \<longrightarrow> Q(x,y)) \<longrightarrow> (\<forall>x. P(x) \<longrightarrow> (\<exists>y. Q(x,y)))\<close> |
97 lemma \<open>(\<exists>y. \<forall>x. P(x) \<longrightarrow> Q(x,y)) \<longrightarrow> (\<forall>x. P(x) \<longrightarrow> (\<exists>y. Q(x,y)))\<close> |
98 by (tactic "IntPr.fast_tac @{context} 1") |
98 by (tactic "IntPr.fast_tac \<^context> 1") |
99 |
99 |
100 end |
100 end |