329 |
329 |
330 (*definition BAll :: "('a \<Rightarrow> prop) \<Rightarrow> ('a \<Rightarrow> prop) \<Rightarrow> prop" where |
330 (*definition BAll :: "('a \<Rightarrow> prop) \<Rightarrow> ('a \<Rightarrow> prop) \<Rightarrow> prop" where |
331 "BAll (R :: 'a \<Rightarrow> prop) (P :: 'a \<Rightarrow> prop) \<equiv> (\<And>x. (PROP R x \<Longrightarrow> PROP P x))"*) |
331 "BAll (R :: 'a \<Rightarrow> prop) (P :: 'a \<Rightarrow> prop) \<equiv> (\<And>x. (PROP R x \<Longrightarrow> PROP P x))"*) |
332 |
332 |
333 |
333 |
|
334 ML {* exists *} |
|
335 ML {* mem *} |
|
336 |
|
337 ML {* |
|
338 fun needs_lift (rty as Type (rty_s, _)) ty = |
|
339 case ty of |
|
340 Type (s, tys) => |
|
341 (s = rty_s) orelse (exists (needs_lift rty) tys) |
|
342 | _ => false |
|
343 |
|
344 *} |
|
345 |
334 ML {* |
346 ML {* |
335 (* trm \<Rightarrow> new_trm *) |
347 (* trm \<Rightarrow> new_trm *) |
336 fun regularise trm rty rel lthy = |
348 fun regularise trm rty rel lthy = |
337 case trm of |
349 case trm of |
338 Abs (x, T, t) => |
350 Abs (x, T, t) => |
339 if T = rty then let |
351 if (needs_lift rty T) then let |
340 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
352 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
341 val v = Free (x', rty); |
353 val v = Free (x', T); |
342 val t' = subst_bound (v, t); |
354 val t' = subst_bound (v, t); |
343 val rec_term = regularise t' rty rel lthy2; |
355 val rec_term = regularise t' rty rel lthy2; |
344 val lam_term = Term.lambda_name (x, v) rec_term; |
356 val lam_term = Term.lambda_name (x, v) rec_term; |
345 val sub_res_term = tyRel T rty rel lthy; |
357 val sub_res_term = tyRel T rty rel lthy; |
346 val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool}); |
358 val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool}); |
350 val rabs_term = (rabs $ res_term) $ lam_term; |
362 val rabs_term = (rabs $ res_term) $ lam_term; |
351 in |
363 in |
352 rabs_term |
364 rabs_term |
353 end else let |
365 end else let |
354 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
366 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
355 val v = Free (x', rty); |
367 val v = Free (x', fastype_of t); |
356 val t' = subst_bound (v, t); |
368 val t' = subst_bound (v, t); |
357 val rec_term = regularise t' rty rel lthy2; |
369 val rec_term = regularise t' rty rel lthy2; |
358 in |
370 in |
359 Term.lambda_name (x, v) rec_term |
371 Term.lambda_name (x, v) rec_term |
360 end |
372 end |
361 | ((Const (@{const_name "All"}, at)) $ (Abs (x, T, t))) => |
373 | ((Const (@{const_name "All"}, at)) $ (Abs (x, T, t))) => |
362 if T = rty then let |
374 if (needs_lift rty T) then let |
363 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
375 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
364 val v = Free (x', rty); |
376 val v = Free (x', T); |
365 val t' = subst_bound (v, t); |
377 val t' = subst_bound (v, t); |
366 val rec_term = regularise t' rty rel lthy2; |
378 val rec_term = regularise t' rty rel lthy2; |
367 val lam_term = Term.lambda_name (x, v) rec_term; |
379 val lam_term = Term.lambda_name (x, v) rec_term; |
368 val sub_res_term = tyRel T rty rel lthy; |
380 val sub_res_term = tyRel T rty rel lthy; |
369 val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool}); |
381 val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool}); |
373 val rall_term = (rall $ res_term) $ lam_term; |
385 val rall_term = (rall $ res_term) $ lam_term; |
374 in |
386 in |
375 rall_term |
387 rall_term |
376 end else let |
388 end else let |
377 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
389 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
378 val v = Free (x', rty); |
390 val v = Free (x', fastype_of t); |
379 val t' = subst_bound (v, t); |
391 val t' = subst_bound (v, t); |
380 val rec_term = regularise t' rty rel lthy2; |
392 val rec_term = regularise t' rty rel lthy2; |
381 val lam_term = Term.lambda_name (x, v) rec_term |
393 val lam_term = Term.lambda_name (x, v) rec_term |
382 in |
394 in |
383 Const(@{const_name "All"}, at) $ lam_term |
395 Const(@{const_name "All"}, at) $ lam_term |
384 end |
396 end |
385 | ((Const (@{const_name "Ex"}, at)) $ (Abs (x, T, t))) => |
397 | ((Const (@{const_name "Ex"}, at)) $ (Abs (x, T, t))) => |
386 if T = rty then let |
398 if (needs_lift rty T) then let |
387 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
399 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
388 val v = Free (x', rty); |
400 val v = Free (x', T); |
389 val t' = subst_bound (v, t); |
401 val t' = subst_bound (v, t); |
390 val rec_term = regularise t' rty rel lthy2; |
402 val rec_term = regularise t' rty rel lthy2; |
391 val lam_term = Term.lambda_name (x, v) rec_term; |
403 val lam_term = Term.lambda_name (x, v) rec_term; |
392 val sub_res_term = tyRel T rty rel lthy; |
404 val sub_res_term = tyRel T rty rel lthy; |
393 val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool}); |
405 val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool}); |
397 val rall_term = (rall $ res_term) $ lam_term; |
409 val rall_term = (rall $ res_term) $ lam_term; |
398 in |
410 in |
399 rall_term |
411 rall_term |
400 end else let |
412 end else let |
401 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
413 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
402 val v = Free (x', rty); |
414 val v = Free (x', fastype_of t); |
403 val t' = subst_bound (v, t); |
415 val t' = subst_bound (v, t); |
404 val rec_term = regularise t' rty rel lthy2; |
416 val rec_term = regularise t' rty rel lthy2; |
405 val lam_term = Term.lambda_name (x, v) rec_term |
417 val lam_term = Term.lambda_name (x, v) rec_term |
406 in |
418 in |
407 Const(@{const_name "All"}, at) $ lam_term |
419 Const(@{const_name "All"}, at) $ lam_term |