1 (* Title: FOL/ex/Quantifiers_Int.thy |
1 (* Title: FOL/ex/Quantifiers_Int.thy |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Copyright 1991 University of Cambridge |
3 Copyright 1991 University of Cambridge |
4 *) |
4 *) |
5 |
5 |
6 section {* First-Order Logic: quantifier examples (intuitionistic version) *} |
6 section \<open>First-Order Logic: quantifier examples (intuitionistic version)\<close> |
7 |
7 |
8 theory Quantifiers_Int |
8 theory Quantifiers_Int |
9 imports IFOL |
9 imports IFOL |
10 begin |
10 begin |
11 |
11 |
14 |
14 |
15 lemma "(EX x y. P(x,y)) --> (EX y x. P(x,y))" |
15 lemma "(EX x y. P(x,y)) --> (EX y x. P(x,y))" |
16 by (tactic "IntPr.fast_tac @{context} 1") |
16 by (tactic "IntPr.fast_tac @{context} 1") |
17 |
17 |
18 |
18 |
19 -- {* Converse is false *} |
19 -- \<open>Converse is false\<close> |
20 lemma "(ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))" |
20 lemma "(ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))" |
21 by (tactic "IntPr.fast_tac @{context} 1") |
21 by (tactic "IntPr.fast_tac @{context} 1") |
22 |
22 |
23 lemma "(ALL x. P-->Q(x)) <-> (P--> (ALL x. Q(x)))" |
23 lemma "(ALL x. P-->Q(x)) <-> (P--> (ALL x. Q(x)))" |
24 by (tactic "IntPr.fast_tac @{context} 1") |
24 by (tactic "IntPr.fast_tac @{context} 1") |
26 |
26 |
27 lemma "(ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)" |
27 lemma "(ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)" |
28 by (tactic "IntPr.fast_tac @{context} 1") |
28 by (tactic "IntPr.fast_tac @{context} 1") |
29 |
29 |
30 |
30 |
31 text {* Some harder ones *} |
31 text \<open>Some harder ones\<close> |
32 |
32 |
33 lemma "(EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))" |
33 lemma "(EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))" |
34 by (tactic "IntPr.fast_tac @{context} 1") |
34 by (tactic "IntPr.fast_tac @{context} 1") |
35 |
35 |
36 -- {* Converse is false *} |
36 -- \<open>Converse is false\<close> |
37 lemma "(EX x. P(x)&Q(x)) --> (EX x. P(x)) & (EX x. Q(x))" |
37 lemma "(EX x. P(x)&Q(x)) --> (EX x. P(x)) & (EX x. Q(x))" |
38 by (tactic "IntPr.fast_tac @{context} 1") |
38 by (tactic "IntPr.fast_tac @{context} 1") |
39 |
39 |
40 |
40 |
41 text {* Basic test of quantifier reasoning *} |
41 text \<open>Basic test of quantifier reasoning\<close> |
42 |
42 |
43 -- {* TRUE *} |
43 -- \<open>TRUE\<close> |
44 lemma "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))" |
44 lemma "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))" |
45 by (tactic "IntPr.fast_tac @{context} 1") |
45 by (tactic "IntPr.fast_tac @{context} 1") |
46 |
46 |
47 lemma "(ALL x. Q(x)) --> (EX x. Q(x))" |
47 lemma "(ALL x. Q(x)) --> (EX x. Q(x))" |
48 by (tactic "IntPr.fast_tac @{context} 1") |
48 by (tactic "IntPr.fast_tac @{context} 1") |
49 |
49 |
50 |
50 |
51 text {* The following should fail, as they are false! *} |
51 text \<open>The following should fail, as they are false!\<close> |
52 |
52 |
53 lemma "(ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))" |
53 lemma "(ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))" |
54 apply (tactic "IntPr.fast_tac @{context} 1")? |
54 apply (tactic "IntPr.fast_tac @{context} 1")? |
55 oops |
55 oops |
56 |
56 |
65 schematic_lemma "(P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))" |
65 schematic_lemma "(P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))" |
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 {* Back to things that are provable \dots *} |
70 text \<open>Back to things that are provable \dots\<close> |
71 |
71 |
72 lemma "(ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))" |
72 lemma "(ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))" |
73 by (tactic "IntPr.fast_tac @{context} 1") |
73 by (tactic "IntPr.fast_tac @{context} 1") |
74 |
74 |
75 -- {* An example of why exI should be delayed as long as possible *} |
75 -- \<open>An example of why exI should be delayed as long as possible\<close> |
76 lemma "(P --> (EX x. Q(x))) & P --> (EX x. Q(x))" |
76 lemma "(P --> (EX x. Q(x))) & P --> (EX x. Q(x))" |
77 by (tactic "IntPr.fast_tac @{context} 1") |
77 by (tactic "IntPr.fast_tac @{context} 1") |
78 |
78 |
79 schematic_lemma "(ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)" |
79 schematic_lemma "(ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)" |
80 by (tactic "IntPr.fast_tac @{context} 1") |
80 by (tactic "IntPr.fast_tac @{context} 1") |
81 |
81 |
82 lemma "(ALL x. Q(x)) --> (EX x. Q(x))" |
82 lemma "(ALL x. Q(x)) --> (EX x. Q(x))" |
83 by (tactic "IntPr.fast_tac @{context} 1") |
83 by (tactic "IntPr.fast_tac @{context} 1") |
84 |
84 |
85 |
85 |
86 text {* Some slow ones *} |
86 text \<open>Some slow ones\<close> |
87 |
87 |
88 -- {* Principia Mathematica *11.53 *} |
88 -- \<open>Principia Mathematica *11.53\<close> |
89 lemma "(ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))" |
89 lemma "(ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))" |
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 "(EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))" |
93 lemma "(EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))" |