|
1 (**** quantifier examples -- process using Doc/tout quant.txt ****) |
|
2 |
|
3 Pretty.setmargin 72; (*existing macros just allow this margin*) |
|
4 print_depth 0; |
|
5 |
|
6 |
|
7 goal Int_Rule.thy "(ALL x y.P(x,y)) --> (ALL z w.P(w,z))"; |
|
8 by (resolve_tac [impI] 1); |
|
9 by (dresolve_tac [spec] 1); |
|
10 by (resolve_tac [allI] 1); |
|
11 by (dresolve_tac [spec] 1); |
|
12 by (resolve_tac [allI] 1); |
|
13 by (assume_tac 1); |
|
14 choplev 1; |
|
15 by (resolve_tac [allI] 1); |
|
16 by (resolve_tac [allI] 1); |
|
17 by (dresolve_tac [spec] 1); |
|
18 by (dresolve_tac [spec] 1); |
|
19 by (assume_tac 1); |
|
20 |
|
21 choplev 0; |
|
22 by (REPEAT (assume_tac 1 |
|
23 ORELSE resolve_tac [impI,allI] 1 |
|
24 ORELSE dresolve_tac [spec] 1)); |
|
25 |
|
26 |
|
27 - goal Int_Rule.thy "(ALL x y.P(x,y)) --> (ALL z w.P(w,z))"; |
|
28 Level 0 |
|
29 (ALL x y. P(x,y)) --> (ALL z w. P(w,z)) |
|
30 1. (ALL x y. P(x,y)) --> (ALL z w. P(w,z)) |
|
31 val it = [] : thm list |
|
32 - by (resolve_tac [impI] 1); |
|
33 Level 1 |
|
34 (ALL x y. P(x,y)) --> (ALL z w. P(w,z)) |
|
35 1. ALL x y. P(x,y) ==> ALL z w. P(w,z) |
|
36 val it = () : unit |
|
37 - by (dresolve_tac [spec] 1); |
|
38 Level 2 |
|
39 (ALL x y. P(x,y)) --> (ALL z w. P(w,z)) |
|
40 1. ALL y. P(?x1,y) ==> ALL z w. P(w,z) |
|
41 val it = () : unit |
|
42 - by (resolve_tac [allI] 1); |
|
43 Level 3 |
|
44 (ALL x y. P(x,y)) --> (ALL z w. P(w,z)) |
|
45 1. !!z. ALL y. P(?x1,y) ==> ALL w. P(w,z) |
|
46 val it = () : unit |
|
47 - by (dresolve_tac [spec] 1); |
|
48 Level 4 |
|
49 (ALL x y. P(x,y)) --> (ALL z w. P(w,z)) |
|
50 1. !!z. P(?x1,?y3(z)) ==> ALL w. P(w,z) |
|
51 val it = () : unit |
|
52 - by (resolve_tac [allI] 1); |
|
53 Level 5 |
|
54 (ALL x y. P(x,y)) --> (ALL z w. P(w,z)) |
|
55 1. !!z w. P(?x1,?y3(z)) ==> P(w,z) |
|
56 val it = () : unit |
|
57 - by (assume_tac 1); |
|
58 by: tactic returned no results |
|
59 |
|
60 uncaught exception ERROR |
|
61 - choplev 1; |
|
62 Level 1 |
|
63 (ALL x y. P(x,y)) --> (ALL z w. P(w,z)) |
|
64 1. ALL x y. P(x,y) ==> ALL z w. P(w,z) |
|
65 val it = () : unit |
|
66 - by (resolve_tac [allI] 1); |
|
67 Level 2 |
|
68 (ALL x y. P(x,y)) --> (ALL z w. P(w,z)) |
|
69 1. !!z. ALL x y. P(x,y) ==> ALL w. P(w,z) |
|
70 val it = () : unit |
|
71 - by (resolve_tac [allI] 1); |
|
72 Level 3 |
|
73 (ALL x y. P(x,y)) --> (ALL z w. P(w,z)) |
|
74 1. !!z w. ALL x y. P(x,y) ==> P(w,z) |
|
75 val it = () : unit |
|
76 - by (dresolve_tac [spec] 1); |
|
77 Level 4 |
|
78 (ALL x y. P(x,y)) --> (ALL z w. P(w,z)) |
|
79 1. !!z w. ALL y. P(?x3(z,w),y) ==> P(w,z) |
|
80 val it = () : unit |
|
81 - by (dresolve_tac [spec] 1); |
|
82 Level 5 |
|
83 (ALL x y. P(x,y)) --> (ALL z w. P(w,z)) |
|
84 1. !!z w. P(?x3(z,w),?y4(z,w)) ==> P(w,z) |
|
85 val it = () : unit |
|
86 - by (assume_tac 1); |
|
87 Level 6 |
|
88 (ALL x y. P(x,y)) --> (ALL z w. P(w,z)) |
|
89 No subgoals! |
|
90 |
|
91 > choplev 0; |
|
92 Level 0 |
|
93 (ALL x y. P(x,y)) --> (ALL z w. P(w,z)) |
|
94 1. (ALL x y. P(x,y)) --> (ALL z w. P(w,z)) |
|
95 > by (REPEAT (assume_tac 1 |
|
96 # ORELSE resolve_tac [impI,allI] 1 |
|
97 # ORELSE dresolve_tac [spec] 1)); |
|
98 Level 1 |
|
99 (ALL x y. P(x,y)) --> (ALL z w. P(w,z)) |
|
100 No subgoals! |
|
101 |
|
102 |
|
103 |
|
104 goal FOL_thy "ALL x. EX y. x=y"; |
|
105 by (resolve_tac [allI] 1); |
|
106 by (resolve_tac [exI] 1); |
|
107 by (resolve_tac [refl] 1); |
|
108 |
|
109 - goal Int_Rule.thy "ALL x. EX y. x=y"; |
|
110 Level 0 |
|
111 ALL x. EX y. x = y |
|
112 1. ALL x. EX y. x = y |
|
113 val it = [] : thm list |
|
114 - by (resolve_tac [allI] 1); |
|
115 Level 1 |
|
116 ALL x. EX y. x = y |
|
117 1. !!x. EX y. x = y |
|
118 val it = () : unit |
|
119 - by (resolve_tac [exI] 1); |
|
120 Level 2 |
|
121 ALL x. EX y. x = y |
|
122 1. !!x. x = ?y1(x) |
|
123 val it = () : unit |
|
124 - by (resolve_tac [refl] 1); |
|
125 Level 3 |
|
126 ALL x. EX y. x = y |
|
127 No subgoals! |
|
128 val it = () : unit |
|
129 - |
|
130 |
|
131 goal FOL_thy "EX y. ALL x. x=y"; |
|
132 by (resolve_tac [exI] 1); |
|
133 by (resolve_tac [allI] 1); |
|
134 by (resolve_tac [refl] 1); |
|
135 |
|
136 - goal Int_Rule.thy "EX y. ALL x. x=y"; |
|
137 Level 0 |
|
138 EX y. ALL x. x = y |
|
139 1. EX y. ALL x. x = y |
|
140 val it = [] : thm list |
|
141 - by (resolve_tac [exI] 1); |
|
142 Level 1 |
|
143 EX y. ALL x. x = y |
|
144 1. ALL x. x = ?y |
|
145 val it = () : unit |
|
146 - by (resolve_tac [allI] 1); |
|
147 Level 2 |
|
148 EX y. ALL x. x = y |
|
149 1. !!x. x = ?y |
|
150 val it = () : unit |
|
151 - by (resolve_tac [refl] 1); |
|
152 by: tactic returned no results |
|
153 |
|
154 uncaught exception ERROR |
|
155 |
|
156 |
|
157 |
|
158 goal FOL_thy "EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)"; |
|
159 by (resolve_tac [exI, allI] 1); |
|
160 by (resolve_tac [exI, allI] 1); |
|
161 by (resolve_tac [exI, allI] 1); |
|
162 by (resolve_tac [exI, allI] 1); |
|
163 by (resolve_tac [exI, allI] 1); |
|
164 |
|
165 - goal Int_Rule.thy "EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)"; |
|
166 Level 0 |
|
167 EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w) |
|
168 1. EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w) |
|
169 val it = [] : thm list |
|
170 - by (resolve_tac [exI, allI] 1); |
|
171 Level 1 |
|
172 EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w) |
|
173 1. ALL x. EX v. ALL y. EX w. P(?u,x,v,y,w) |
|
174 val it = () : unit |
|
175 - by (resolve_tac [exI, allI] 1); |
|
176 Level 2 |
|
177 EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w) |
|
178 1. !!x. EX v. ALL y. EX w. P(?u,x,v,y,w) |
|
179 val it = () : unit |
|
180 - by (resolve_tac [exI, allI] 1); |
|
181 Level 3 |
|
182 EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w) |
|
183 1. !!x. ALL y. EX w. P(?u,x,?v2(x),y,w) |
|
184 val it = () : unit |
|
185 - by (resolve_tac [exI, allI] 1); |
|
186 Level 4 |
|
187 EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w) |
|
188 1. !!x y. EX w. P(?u,x,?v2(x),y,w) |
|
189 val it = () : unit |
|
190 - by (resolve_tac [exI, allI] 1); |
|
191 Level 5 |
|
192 EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w) |
|
193 1. !!x y. P(?u,x,?v2(x),y,?w4(x,y)) |
|
194 val it = () : unit |
|
195 |
|
196 |
|
197 goal FOL_thy "(ALL x.P(x) --> Q) --> (EX x.P(x))-->Q"; |
|
198 by (REPEAT (resolve_tac [impI] 1)); |
|
199 by (eresolve_tac [exE] 1); |
|
200 by (dresolve_tac [spec] 1); |
|
201 by (eresolve_tac [mp] 1); |
|
202 by (assume_tac 1); |
|
203 |
|
204 - goal Int_Rule.thy "(ALL x.P(x) --> Q) --> (EX x.P(x))-->Q"; |
|
205 Level 0 |
|
206 (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q |
|
207 1. (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q |
|
208 val it = [] : thm list |
|
209 - by (REPEAT (resolve_tac [impI] 1)); |
|
210 Level 1 |
|
211 (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q |
|
212 1. [| ALL x. P(x) --> Q; EX x. P(x) |] ==> Q |
|
213 val it = () : unit |
|
214 - by (eresolve_tac [exE] 1); |
|
215 Level 2 |
|
216 (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q |
|
217 1. !!x. [| ALL x. P(x) --> Q; P(x) |] ==> Q |
|
218 val it = () : unit |
|
219 - by (dresolve_tac [spec] 1); |
|
220 Level 3 |
|
221 (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q |
|
222 1. !!x. [| P(x); P(?x3(x)) --> Q |] ==> Q |
|
223 val it = () : unit |
|
224 - by (eresolve_tac [mp] 1); |
|
225 Level 4 |
|
226 (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q |
|
227 1. !!x. P(x) ==> P(?x3(x)) |
|
228 val it = () : unit |
|
229 - by (assume_tac 1); |
|
230 Level 5 |
|
231 (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q |
|
232 No subgoals! |
|
233 |
|
234 |
|
235 goal FOL_thy "((EX x.P(x)) --> Q) --> (ALL x.P(x)-->Q)"; |
|
236 by (REPEAT (resolve_tac [impI] 1)); |
|
237 |
|
238 |
|
239 goal FOL_thy "(EX x.P(x) --> Q) --> (ALL x.P(x))-->Q"; |
|
240 by (REPEAT (resolve_tac [impI] 1)); |
|
241 by (eresolve_tac [exE] 1); |
|
242 by (eresolve_tac [mp] 1); |
|
243 by (eresolve_tac [spec] 1); |
|
244 |