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