197 by (cases p) (simp add: Let_def) |
198 by (cases p) (simp add: Let_def) |
198 |
199 |
199 theorem exE_realizer': "P (snd p) (fst p) \<Longrightarrow> |
200 theorem exE_realizer': "P (snd p) (fst p) \<Longrightarrow> |
200 (\<And>x y. P y x \<Longrightarrow> Q) \<Longrightarrow> Q" by (cases p) simp |
201 (\<And>x y. P y x \<Longrightarrow> Q) \<Longrightarrow> Q" by (cases p) simp |
201 |
202 |
202 setup {* |
|
203 Sign.add_const_constraint (@{const_name "default"}, SOME @{typ "'a::type"}) |
|
204 *} |
|
205 |
|
206 realizers |
203 realizers |
207 impI (P, Q): "\<lambda>pq. pq" |
204 impI (P, Q): "\<lambda>pq. pq" |
208 "\<Lambda> P Q pq (h: _). allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))" |
205 "\<Lambda> (c: _) (d: _) P Q pq (h: _). allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))" |
209 |
206 |
210 impI (P): "Null" |
207 impI (P): "Null" |
211 "\<Lambda> P Q (h: _). allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))" |
208 "\<Lambda> (c: _) P Q (h: _). allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))" |
212 |
209 |
213 impI (Q): "\<lambda>q. q" "\<Lambda> P Q q. impI \<cdot> _ \<cdot> _" |
210 impI (Q): "\<lambda>q. q" "\<Lambda> (c: _) P Q q. impI \<cdot> _ \<cdot> _" |
214 |
211 |
215 impI: "Null" "impI" |
212 impI: "Null" "impI" |
216 |
213 |
217 mp (P, Q): "\<lambda>pq. pq" |
214 mp (P, Q): "\<lambda>pq. pq" |
218 "\<Lambda> P Q pq (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)" |
215 "\<Lambda> (c: _) (d: _) P Q pq (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> c \<bullet> h)" |
219 |
216 |
220 mp (P): "Null" |
217 mp (P): "Null" |
221 "\<Lambda> P Q (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)" |
218 "\<Lambda> (c: _) P Q (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> c \<bullet> h)" |
222 |
219 |
223 mp (Q): "\<lambda>q. q" "\<Lambda> P Q q. mp \<cdot> _ \<cdot> _" |
220 mp (Q): "\<lambda>q. q" "\<Lambda> (c: _) P Q q. mp \<cdot> _ \<cdot> _" |
224 |
221 |
225 mp: "Null" "mp" |
222 mp: "Null" "mp" |
226 |
223 |
227 allI (P): "\<lambda>p. p" "\<Lambda> P p. allI \<cdot> _" |
224 allI (P): "\<lambda>p. p" "\<Lambda> (c: _) P (d: _) p. allI \<cdot> _ \<bullet> d" |
228 |
225 |
229 allI: "Null" "allI" |
226 allI: "Null" "allI" |
230 |
227 |
231 spec (P): "\<lambda>x p. p x" "\<Lambda> P x p. spec \<cdot> _ \<cdot> x" |
228 spec (P): "\<lambda>x p. p x" "\<Lambda> (c: _) P x (d: _) p. spec \<cdot> _ \<cdot> x \<bullet> d" |
232 |
229 |
233 spec: "Null" "spec" |
230 spec: "Null" "spec" |
234 |
231 |
235 exI (P): "\<lambda>x p. (x, p)" "\<Lambda> P x p. exI_realizer \<cdot> P \<cdot> p \<cdot> x" |
232 exI (P): "\<lambda>x p. (x, p)" "\<Lambda> (c: _) P x (d: _) p. exI_realizer \<cdot> P \<cdot> p \<cdot> x \<bullet> c \<bullet> d" |
236 |
233 |
237 exI: "\<lambda>x. x" "\<Lambda> P x (h: _). h" |
234 exI: "\<lambda>x. x" "\<Lambda> P x (c: _) (h: _). h" |
238 |
235 |
239 exE (P, Q): "\<lambda>p pq. let (x, y) = p in pq x y" |
236 exE (P, Q): "\<lambda>p pq. let (x, y) = p in pq x y" |
240 "\<Lambda> P Q p (h: _) pq. exE_realizer \<cdot> P \<cdot> p \<cdot> Q \<cdot> pq \<bullet> h" |
237 "\<Lambda> (c: _) (d: _) P Q (e: _) p (h: _) pq. exE_realizer \<cdot> P \<cdot> p \<cdot> Q \<cdot> pq \<bullet> c \<bullet> e \<bullet> d \<bullet> h" |
241 |
238 |
242 exE (P): "Null" |
239 exE (P): "Null" |
243 "\<Lambda> P Q p. exE_realizer' \<cdot> _ \<cdot> _ \<cdot> _" |
240 "\<Lambda> (c: _) P Q (d: _) p. exE_realizer' \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> c \<bullet> d" |
244 |
241 |
245 exE (Q): "\<lambda>x pq. pq x" |
242 exE (Q): "\<lambda>x pq. pq x" |
246 "\<Lambda> P Q x (h1: _) pq (h2: _). h2 \<cdot> x \<bullet> h1" |
243 "\<Lambda> (c: _) P Q (d: _) x (h1: _) pq (h2: _). h2 \<cdot> x \<bullet> h1" |
247 |
244 |
248 exE: "Null" |
245 exE: "Null" |
249 "\<Lambda> P Q x (h1: _) (h2: _). h2 \<cdot> x \<bullet> h1" |
246 "\<Lambda> P Q (c: _) x (h1: _) (h2: _). h2 \<cdot> x \<bullet> h1" |
250 |
247 |
251 conjI (P, Q): "Pair" |
248 conjI (P, Q): "Pair" |
252 "\<Lambda> P Q p (h: _) q. conjI_realizer \<cdot> P \<cdot> p \<cdot> Q \<cdot> q \<bullet> h" |
249 "\<Lambda> (c: _) (d: _) P Q p (h: _) q. conjI_realizer \<cdot> P \<cdot> p \<cdot> Q \<cdot> q \<bullet> c \<bullet> d \<bullet> h" |
253 |
250 |
254 conjI (P): "\<lambda>p. p" |
251 conjI (P): "\<lambda>p. p" |
255 "\<Lambda> P Q p. conjI \<cdot> _ \<cdot> _" |
252 "\<Lambda> (c: _) P Q p. conjI \<cdot> _ \<cdot> _" |
256 |
253 |
257 conjI (Q): "\<lambda>q. q" |
254 conjI (Q): "\<lambda>q. q" |
258 "\<Lambda> P Q (h: _) q. conjI \<cdot> _ \<cdot> _ \<bullet> h" |
255 "\<Lambda> (c: _) P Q (h: _) q. conjI \<cdot> _ \<cdot> _ \<bullet> h" |
259 |
256 |
260 conjI: "Null" "conjI" |
257 conjI: "Null" "conjI" |
261 |
258 |
262 conjunct1 (P, Q): "fst" |
259 conjunct1 (P, Q): "fst" |
263 "\<Lambda> P Q pq. conjunct1 \<cdot> _ \<cdot> _" |
260 "\<Lambda> (c: _) (d: _) P Q pq. conjunct1 \<cdot> _ \<cdot> _" |
264 |
261 |
265 conjunct1 (P): "\<lambda>p. p" |
262 conjunct1 (P): "\<lambda>p. p" |
266 "\<Lambda> P Q p. conjunct1 \<cdot> _ \<cdot> _" |
263 "\<Lambda> (c: _) P Q p. conjunct1 \<cdot> _ \<cdot> _" |
267 |
264 |
268 conjunct1 (Q): "Null" |
265 conjunct1 (Q): "Null" |
269 "\<Lambda> P Q q. conjunct1 \<cdot> _ \<cdot> _" |
266 "\<Lambda> (c: _) P Q q. conjunct1 \<cdot> _ \<cdot> _" |
270 |
267 |
271 conjunct1: "Null" "conjunct1" |
268 conjunct1: "Null" "conjunct1" |
272 |
269 |
273 conjunct2 (P, Q): "snd" |
270 conjunct2 (P, Q): "snd" |
274 "\<Lambda> P Q pq. conjunct2 \<cdot> _ \<cdot> _" |
271 "\<Lambda> (c: _) (d: _) P Q pq. conjunct2 \<cdot> _ \<cdot> _" |
275 |
272 |
276 conjunct2 (P): "Null" |
273 conjunct2 (P): "Null" |
277 "\<Lambda> P Q p. conjunct2 \<cdot> _ \<cdot> _" |
274 "\<Lambda> (c: _) P Q p. conjunct2 \<cdot> _ \<cdot> _" |
278 |
275 |
279 conjunct2 (Q): "\<lambda>p. p" |
276 conjunct2 (Q): "\<lambda>p. p" |
280 "\<Lambda> P Q p. conjunct2 \<cdot> _ \<cdot> _" |
277 "\<Lambda> (c: _) P Q p. conjunct2 \<cdot> _ \<cdot> _" |
281 |
278 |
282 conjunct2: "Null" "conjunct2" |
279 conjunct2: "Null" "conjunct2" |
283 |
280 |
284 disjI1 (P, Q): "Inl" |
281 disjI1 (P, Q): "Inl" |
285 "\<Lambda> P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_1 \<cdot> P \<cdot> _ \<cdot> p)" |
282 "\<Lambda> (c: _) (d: _) P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_1 \<cdot> P \<cdot> _ \<cdot> p \<bullet> arity_type_bool \<bullet> c \<bullet> d)" |
286 |
283 |
287 disjI1 (P): "Some" |
284 disjI1 (P): "Some" |
288 "\<Lambda> P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> P \<cdot> p)" |
285 "\<Lambda> (c: _) P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> P \<cdot> p \<bullet> arity_type_bool \<bullet> c)" |
289 |
286 |
290 disjI1 (Q): "None" |
287 disjI1 (Q): "None" |
291 "\<Lambda> P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _)" |
288 "\<Lambda> (c: _) P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool \<bullet> c)" |
292 |
289 |
293 disjI1: "Left" |
290 disjI1: "Left" |
294 "\<Lambda> P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_1 \<cdot> _ \<cdot> _)" |
291 "\<Lambda> P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool)" |
295 |
292 |
296 disjI2 (P, Q): "Inr" |
293 disjI2 (P, Q): "Inr" |
297 "\<Lambda> Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_2 \<cdot> _ \<cdot> Q \<cdot> q)" |
294 "\<Lambda> (d: _) (c: _) Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_2 \<cdot> _ \<cdot> Q \<cdot> q \<bullet> arity_type_bool \<bullet> c \<bullet> d)" |
298 |
295 |
299 disjI2 (P): "None" |
296 disjI2 (P): "None" |
300 "\<Lambda> Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _)" |
297 "\<Lambda> (c: _) Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool \<bullet> c)" |
301 |
298 |
302 disjI2 (Q): "Some" |
299 disjI2 (Q): "Some" |
303 "\<Lambda> Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> Q \<cdot> q)" |
300 "\<Lambda> (c: _) Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> Q \<cdot> q \<bullet> arity_type_bool \<bullet> c)" |
304 |
301 |
305 disjI2: "Right" |
302 disjI2: "Right" |
306 "\<Lambda> Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_2 \<cdot> _ \<cdot> _)" |
303 "\<Lambda> Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_2 \<cdot> _ \<cdot> _ \<bullet> arity_type_bool)" |
307 |
304 |
308 disjE (P, Q, R): "\<lambda>pq pr qr. |
305 disjE (P, Q, R): "\<lambda>pq pr qr. |
309 (case pq of Inl p \<Rightarrow> pr p | Inr q \<Rightarrow> qr q)" |
306 (case pq of Inl p \<Rightarrow> pr p | Inr q \<Rightarrow> qr q)" |
310 "\<Lambda> P Q R pq (h1: _) pr (h2: _) qr. |
307 "\<Lambda> (c: _) (d: _) (e: _) P Q R pq (h1: _) pr (h2: _) qr. |
311 disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2" |
308 disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> c \<bullet> d \<bullet> e \<bullet> h1 \<bullet> h2" |
312 |
309 |
313 disjE (Q, R): "\<lambda>pq pr qr. |
310 disjE (Q, R): "\<lambda>pq pr qr. |
314 (case pq of None \<Rightarrow> pr | Some q \<Rightarrow> qr q)" |
311 (case pq of None \<Rightarrow> pr | Some q \<Rightarrow> qr q)" |
315 "\<Lambda> P Q R pq (h1: _) pr (h2: _) qr. |
312 "\<Lambda> (c: _) (d: _) P Q R pq (h1: _) pr (h2: _) qr. |
316 disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2" |
313 disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> c \<bullet> d \<bullet> h1 \<bullet> h2" |
317 |
314 |
318 disjE (P, R): "\<lambda>pq pr qr. |
315 disjE (P, R): "\<lambda>pq pr qr. |
319 (case pq of None \<Rightarrow> qr | Some p \<Rightarrow> pr p)" |
316 (case pq of None \<Rightarrow> qr | Some p \<Rightarrow> pr p)" |
320 "\<Lambda> P Q R pq (h1: _) pr (h2: _) qr (h3: _). |
317 "\<Lambda> (c: _) (d: _) P Q R pq (h1: _) pr (h2: _) qr (h3: _). |
321 disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> qr \<cdot> pr \<bullet> h1 \<bullet> h3 \<bullet> h2" |
318 disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> qr \<cdot> pr \<bullet> c \<bullet> d \<bullet> h1 \<bullet> h3 \<bullet> h2" |
322 |
319 |
323 disjE (R): "\<lambda>pq pr qr. |
320 disjE (R): "\<lambda>pq pr qr. |
324 (case pq of Left \<Rightarrow> pr | Right \<Rightarrow> qr)" |
321 (case pq of Left \<Rightarrow> pr | Right \<Rightarrow> qr)" |
325 "\<Lambda> P Q R pq (h1: _) pr (h2: _) qr. |
322 "\<Lambda> (c: _) P Q R pq (h1: _) pr (h2: _) qr. |
326 disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2" |
323 disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> c \<bullet> h1 \<bullet> h2" |
327 |
324 |
328 disjE (P, Q): "Null" |
325 disjE (P, Q): "Null" |
329 "\<Lambda> P Q R pq. disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _" |
326 "\<Lambda> (c: _) (d: _) P Q R pq. disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _ \<bullet> c \<bullet> d \<bullet> arity_type_bool" |
330 |
327 |
331 disjE (Q): "Null" |
328 disjE (Q): "Null" |
332 "\<Lambda> P Q R pq. disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _" |
329 "\<Lambda> (c: _) P Q R pq. disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _ \<bullet> c \<bullet> arity_type_bool" |
333 |
330 |
334 disjE (P): "Null" |
331 disjE (P): "Null" |
335 "\<Lambda> P Q R pq (h1: _) (h2: _) (h3: _). |
332 "\<Lambda> (c: _) P Q R pq (h1: _) (h2: _) (h3: _). |
336 disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _ \<bullet> h1 \<bullet> h3 \<bullet> h2" |
333 disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _ \<bullet> c \<bullet> arity_type_bool \<bullet> h1 \<bullet> h3 \<bullet> h2" |
337 |
334 |
338 disjE: "Null" |
335 disjE: "Null" |
339 "\<Lambda> P Q R pq. disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _" |
336 "\<Lambda> P Q R pq. disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _ \<bullet> arity_type_bool" |
340 |
337 |
341 FalseE (P): "default" |
338 FalseE (P): "default" |
342 "\<Lambda> P. FalseE \<cdot> _" |
339 "\<Lambda> (c: _) P. FalseE \<cdot> _" |
343 |
340 |
344 FalseE: "Null" "FalseE" |
341 FalseE: "Null" "FalseE" |
345 |
342 |
346 notI (P): "Null" |
343 notI (P): "Null" |
347 "\<Lambda> P (h: _). allI \<cdot> _ \<bullet> (\<Lambda> x. notI \<cdot> _ \<bullet> (h \<cdot> x))" |
344 "\<Lambda> (c: _) P (h: _). allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. notI \<cdot> _ \<bullet> (h \<cdot> x))" |
348 |
345 |
349 notI: "Null" "notI" |
346 notI: "Null" "notI" |
350 |
347 |
351 notE (P, R): "\<lambda>p. default" |
348 notE (P, R): "\<lambda>p. default" |
352 "\<Lambda> P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)" |
349 "\<Lambda> (c: _) (d: _) P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> c \<bullet> h)" |
353 |
350 |
354 notE (P): "Null" |
351 notE (P): "Null" |
355 "\<Lambda> P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)" |
352 "\<Lambda> (c: _) P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> c \<bullet> h)" |
356 |
353 |
357 notE (R): "default" |
354 notE (R): "default" |
358 "\<Lambda> P R. notE \<cdot> _ \<cdot> _" |
355 "\<Lambda> (c: _) P R. notE \<cdot> _ \<cdot> _" |
359 |
356 |
360 notE: "Null" "notE" |
357 notE: "Null" "notE" |
361 |
358 |
362 subst (P): "\<lambda>s t ps. ps" |
359 subst (P): "\<lambda>s t ps. ps" |
363 "\<Lambda> s t P (h: _) ps. subst \<cdot> s \<cdot> t \<cdot> P ps \<bullet> h" |
360 "\<Lambda> (c: _) s t P (d: _) (h: _) ps. subst \<cdot> s \<cdot> t \<cdot> P ps \<bullet> d \<bullet> h" |
364 |
361 |
365 subst: "Null" "subst" |
362 subst: "Null" "subst" |
366 |
363 |
367 iffD1 (P, Q): "fst" |
364 iffD1 (P, Q): "fst" |
368 "\<Lambda> Q P pq (h: _) p. |
365 "\<Lambda> (d: _) (c: _) Q P pq (h: _) p. |
369 mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))" |
366 mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> d \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))" |
370 |
367 |
371 iffD1 (P): "\<lambda>p. p" |
368 iffD1 (P): "\<lambda>p. p" |
372 "\<Lambda> Q P p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h)" |
369 "\<Lambda> (c: _) Q P p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h)" |
373 |
370 |
374 iffD1 (Q): "Null" |
371 iffD1 (Q): "Null" |
375 "\<Lambda> Q P q1 (h: _) q2. |
372 "\<Lambda> (c: _) Q P q1 (h: _) q2. |
376 mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))" |
373 mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> c \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))" |
377 |
374 |
378 iffD1: "Null" "iffD1" |
375 iffD1: "Null" "iffD1" |
379 |
376 |
380 iffD2 (P, Q): "snd" |
377 iffD2 (P, Q): "snd" |
381 "\<Lambda> P Q pq (h: _) q. |
378 "\<Lambda> (c: _) (d: _) P Q pq (h: _) q. |
382 mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))" |
379 mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q \<bullet> d \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))" |
383 |
380 |
384 iffD2 (P): "\<lambda>p. p" |
381 iffD2 (P): "\<lambda>p. p" |
385 "\<Lambda> P Q p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h)" |
382 "\<Lambda> (c: _) P Q p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h)" |
386 |
383 |
387 iffD2 (Q): "Null" |
384 iffD2 (Q): "Null" |
388 "\<Lambda> P Q q1 (h: _) q2. |
385 "\<Lambda> (c: _) P Q q1 (h: _) q2. |
389 mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))" |
386 mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> c \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))" |
390 |
387 |
391 iffD2: "Null" "iffD2" |
388 iffD2: "Null" "iffD2" |
392 |
389 |
393 iffI (P, Q): "Pair" |
390 iffI (P, Q): "Pair" |
394 "\<Lambda> P Q pq (h1 : _) qp (h2 : _). conjI_realizer \<cdot> |
391 "\<Lambda> (c: _) (d: _) P Q pq (h1 : _) qp (h2 : _). conjI_realizer \<cdot> |
395 (\<lambda>pq. \<forall>x. P x \<longrightarrow> Q (pq x)) \<cdot> pq \<cdot> |
392 (\<lambda>pq. \<forall>x. P x \<longrightarrow> Q (pq x)) \<cdot> pq \<cdot> |
396 (\<lambda>qp. \<forall>x. Q x \<longrightarrow> P (qp x)) \<cdot> qp \<bullet> |
393 (\<lambda>qp. \<forall>x. Q x \<longrightarrow> P (qp x)) \<cdot> qp \<bullet> |
397 (allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet> |
394 (arity_type_fun \<bullet> c \<bullet> d) \<bullet> |
398 (allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))" |
395 (arity_type_fun \<bullet> d \<bullet> c) \<bullet> |
|
396 (allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet> |
|
397 (allI \<cdot> _ \<bullet> d \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))" |
399 |
398 |
400 iffI (P): "\<lambda>p. p" |
399 iffI (P): "\<lambda>p. p" |
401 "\<Lambda> P Q (h1 : _) p (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet> |
400 "\<Lambda> (c: _) P Q (h1 : _) p (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet> |
402 (allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet> |
401 (allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet> |
403 (impI \<cdot> _ \<cdot> _ \<bullet> h2)" |
402 (impI \<cdot> _ \<cdot> _ \<bullet> h2)" |
404 |
403 |
405 iffI (Q): "\<lambda>q. q" |
404 iffI (Q): "\<lambda>q. q" |
406 "\<Lambda> P Q q (h1 : _) (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet> |
405 "\<Lambda> (c: _) P Q q (h1 : _) (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet> |
407 (impI \<cdot> _ \<cdot> _ \<bullet> h1) \<bullet> |
406 (impI \<cdot> _ \<cdot> _ \<bullet> h1) \<bullet> |
408 (allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))" |
407 (allI \<cdot> _ \<bullet> c \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))" |
409 |
408 |
410 iffI: "Null" "iffI" |
409 iffI: "Null" "iffI" |
411 |
410 |
412 (* |
|
413 classical: "Null" |
|
414 "\<Lambda> P. classical \<cdot> _" |
|
415 *) |
|
416 |
|
417 setup {* |
|
418 Sign.add_const_constraint (@{const_name "default"}, SOME @{typ "'a::default"}) |
|
419 *} |
|
420 |
|
421 end |
411 end |