7 |
7 |
8 theory Quantifiers |
8 theory Quantifiers |
9 imports "../LK" |
9 imports "../LK" |
10 begin |
10 begin |
11 |
11 |
12 lemma "|- (ALL x. P) <-> P" |
12 lemma "|- (\<forall>x. P) \<longleftrightarrow> P" |
13 by fast |
13 by fast |
14 |
14 |
15 lemma "|- (ALL x y. P(x,y)) <-> (ALL y x. P(x,y))" |
15 lemma "|- (\<forall>x y. P(x,y)) \<longleftrightarrow> (\<forall>y x. P(x,y))" |
16 by fast |
16 by fast |
17 |
17 |
18 lemma "ALL u. P(u), ALL v. Q(v) |- ALL u v. P(u) & Q(v)" |
18 lemma "\<forall>u. P(u), \<forall>v. Q(v) |- \<forall>u v. P(u) \<and> Q(v)" |
19 by fast |
19 by fast |
20 |
20 |
21 |
21 |
22 text "Permutation of existential quantifier." |
22 text "Permutation of existential quantifier." |
23 |
23 |
24 lemma "|- (EX x y. P(x,y)) <-> (EX y x. P(x,y))" |
24 lemma "|- (\<exists>x y. P(x,y)) \<longleftrightarrow> (\<exists>y x. P(x,y))" |
25 by fast |
25 by fast |
26 |
26 |
27 lemma "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))" |
27 lemma "|- (\<forall>x. P(x) \<and> Q(x)) \<longleftrightarrow> (\<forall>x. P(x)) \<and> (\<forall>x. Q(x))" |
28 by fast |
28 by fast |
29 |
29 |
30 (*Converse is invalid*) |
30 (*Converse is invalid*) |
31 lemma "|- (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x)|Q(x))" |
31 lemma "|- (\<forall>x. P(x)) \<or> (\<forall>x. Q(x)) \<longrightarrow> (\<forall>x. P(x) \<or> Q(x))" |
32 by fast |
32 by fast |
33 |
33 |
34 |
34 |
35 text "Pushing ALL into an implication." |
35 text "Pushing \<forall>into an implication." |
36 |
36 |
37 lemma "|- (ALL x. P --> Q(x)) <-> (P --> (ALL x. Q(x)))" |
37 lemma "|- (\<forall>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<forall>x. Q(x)))" |
38 by fast |
38 by fast |
39 |
39 |
40 lemma "|- (ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)" |
40 lemma "|- (\<forall>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> ((\<exists>x. P(x)) \<longrightarrow> Q)" |
41 by fast |
41 by fast |
42 |
42 |
43 lemma "|- (EX x. P) <-> P" |
43 lemma "|- (\<exists>x. P) \<longleftrightarrow> P" |
44 by fast |
44 by fast |
45 |
45 |
46 |
46 |
47 text "Distribution of EX over disjunction." |
47 text "Distribution of \<exists>over disjunction." |
48 |
48 |
49 lemma "|- (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))" |
49 lemma "|- (\<exists>x. P(x) \<or> Q(x)) \<longleftrightarrow> (\<exists>x. P(x)) \<or> (\<exists>x. Q(x))" |
50 by fast |
50 by fast |
51 |
51 |
52 (*Converse is invalid*) |
52 (*Converse is invalid*) |
53 lemma "|- (EX x. P(x) & Q(x)) --> (EX x. P(x)) & (EX x. Q(x))" |
53 lemma "|- (\<exists>x. P(x) \<and> Q(x)) \<longrightarrow> (\<exists>x. P(x)) \<and> (\<exists>x. Q(x))" |
54 by fast |
54 by fast |
55 |
55 |
56 |
56 |
57 text "Harder examples: classical theorems." |
57 text "Harder examples: classical theorems." |
58 |
58 |
59 lemma "|- (EX x. P-->Q(x)) <-> (P --> (EX x. Q(x)))" |
59 lemma "|- (\<exists>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<exists>x. Q(x)))" |
60 by fast |
60 by fast |
61 |
61 |
62 lemma "|- (EX x. P(x)-->Q) <-> (ALL x. P(x)) --> Q" |
62 lemma "|- (\<exists>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q" |
63 by fast |
63 by fast |
64 |
64 |
65 lemma "|- (ALL x. P(x)) | Q <-> (ALL x. P(x) | Q)" |
65 lemma "|- (\<forall>x. P(x)) \<or> Q \<longleftrightarrow> (\<forall>x. P(x) \<or> Q)" |
66 by fast |
66 by fast |
67 |
67 |
68 |
68 |
69 text "Basic test of quantifier reasoning" |
69 text "Basic test of quantifier reasoning" |
70 |
70 |
71 lemma "|- (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))" |
71 lemma "|- (\<exists>y. \<forall>x. Q(x,y)) \<longrightarrow> (\<forall>x. \<exists>y. Q(x,y))" |
72 by fast |
72 by fast |
73 |
73 |
74 lemma "|- (ALL x. Q(x)) --> (EX x. Q(x))" |
74 lemma "|- (\<forall>x. Q(x)) \<longrightarrow> (\<exists>x. Q(x))" |
75 by fast |
75 by fast |
76 |
76 |
77 |
77 |
78 text "The following are invalid!" |
78 text "The following are invalid!" |
79 |
79 |
80 (*INVALID*) |
80 (*INVALID*) |
81 lemma "|- (ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))" |
81 lemma "|- (\<forall>x. \<exists>y. Q(x,y)) \<longrightarrow> (\<exists>y. \<forall>x. Q(x,y))" |
82 apply fast? |
82 apply fast? |
83 apply (rule _) |
83 apply (rule _) |
84 oops |
84 oops |
85 |
85 |
86 (*INVALID*) |
86 (*INVALID*) |
87 lemma "|- (EX x. Q(x)) --> (ALL x. Q(x))" |
87 lemma "|- (\<exists>x. Q(x)) \<longrightarrow> (\<forall>x. Q(x))" |
88 apply fast? |
88 apply fast? |
89 apply (rule _) |
89 apply (rule _) |
90 oops |
90 oops |
91 |
91 |
92 (*INVALID*) |
92 (*INVALID*) |
93 schematic_goal "|- P(?a) --> (ALL x. P(x))" |
93 schematic_goal "|- P(?a) \<longrightarrow> (\<forall>x. P(x))" |
94 apply fast? |
94 apply fast? |
95 apply (rule _) |
95 apply (rule _) |
96 oops |
96 oops |
97 |
97 |
98 (*INVALID*) |
98 (*INVALID*) |
99 schematic_goal "|- (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))" |
99 schematic_goal "|- (P(?a) \<longrightarrow> (\<forall>x. Q(x))) \<longrightarrow> (\<forall>x. P(x) \<longrightarrow> Q(x))" |
100 apply fast? |
100 apply fast? |
101 apply (rule _) |
101 apply (rule _) |
102 oops |
102 oops |
103 |
103 |
104 |
104 |
105 text "Back to things that are provable..." |
105 text "Back to things that are provable..." |
106 |
106 |
107 lemma "|- (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))" |
107 lemma "|- (\<forall>x. P(x) \<longrightarrow> Q(x)) \<and> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))" |
108 by fast |
108 by fast |
109 |
109 |
110 (*An example of why exR should be delayed as long as possible*) |
110 (*An example of why exR should be delayed as long as possible*) |
111 lemma "|- (P--> (EX x. Q(x))) & P--> (EX x. Q(x))" |
111 lemma "|- (P \<longrightarrow> (\<exists>x. Q(x))) \<and> P \<longrightarrow> (\<exists>x. Q(x))" |
112 by fast |
112 by fast |
113 |
113 |
114 |
114 |
115 text "Solving for a Var" |
115 text "Solving for a Var" |
116 |
116 |
117 schematic_goal "|- (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)" |
117 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)" |
118 by fast |
118 by fast |
119 |
119 |
120 |
120 |
121 text "Principia Mathematica *11.53" |
121 text "Principia Mathematica *11.53" |
122 |
122 |
123 lemma "|- (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))" |
123 lemma "|- (\<forall>x y. P(x) \<longrightarrow> Q(y)) \<longleftrightarrow> ((\<exists>x. P(x)) \<longrightarrow> (\<forall>y. Q(y)))" |
124 by fast |
124 by fast |
125 |
125 |
126 |
126 |
127 text "Principia Mathematica *11.55" |
127 text "Principia Mathematica *11.55" |
128 |
128 |
129 lemma "|- (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))" |
129 lemma "|- (\<exists>x y. P(x) \<and> Q(x,y)) \<longleftrightarrow> (\<exists>x. P(x) \<and> (\<exists>y. Q(x,y)))" |
130 by fast |
130 by fast |
131 |
131 |
132 |
132 |
133 text "Principia Mathematica *11.61" |
133 text "Principia Mathematica *11.61" |
134 |
134 |
135 lemma "|- (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))" |
135 lemma "|- (\<exists>y. \<forall>x. P(x) \<longrightarrow> Q(x,y)) \<longrightarrow> (\<forall>x. P(x) \<longrightarrow> (\<exists>y. Q(x,y)))" |
136 by fast |
136 by fast |
137 |
137 |
138 |
138 |
139 (*21 August 88: loaded in 45.7 secs*) |
139 (*21 August 88: loaded in 45.7 secs*) |
140 (*18 September 2005: loaded in 0.114 secs*) |
140 (*18 September 2005: loaded in 0.114 secs*) |