349 (* FIXME: check that the types correspond to each other? *) |
349 (* FIXME: check that the types correspond to each other? *) |
350 end |
350 end |
351 *} |
351 *} |
352 |
352 |
353 ML {* |
353 ML {* |
|
354 fun matches_typ (ty, ty') = |
|
355 case (ty, ty') of |
|
356 (_, TVar _) => true |
|
357 | (TFree x, TFree x') => x = x' |
|
358 | (Type (s, tys), Type (s', tys')) => |
|
359 s = s' andalso |
|
360 if (length tys = length tys') |
|
361 then (List.all matches_typ (tys ~~ tys')) |
|
362 else false |
|
363 | _ => false |
|
364 *} |
|
365 ML {* |
|
366 fun matches_term (trm, trm') = |
|
367 case (trm, trm') of |
|
368 (_, Var _) => true |
|
369 | (Const (s, ty), Const (s', ty')) => s = s' andalso matches_typ (ty, ty') |
|
370 | (Free (x, ty), Free (x', ty')) => x = x' andalso matches_typ (ty, ty') |
|
371 | (Bound i, Bound j) => i = j |
|
372 | (Abs (_, T, t), Abs (_, T', t')) => matches_typ (T, T') andalso matches_term (t, t') |
|
373 | (t $ s, t' $ s') => matches_term (t, t') andalso matches_term (s, s') |
|
374 | _ => false |
|
375 *} |
|
376 |
|
377 ML {* |
354 val mk_babs = Const (@{const_name Babs}, dummyT) |
378 val mk_babs = Const (@{const_name Babs}, dummyT) |
355 val mk_ball = Const (@{const_name Ball}, dummyT) |
379 val mk_ball = Const (@{const_name Ball}, dummyT) |
356 val mk_bex = Const (@{const_name Bex}, dummyT) |
380 val mk_bex = Const (@{const_name Bex}, dummyT) |
357 val mk_resp = Const (@{const_name Respects}, dummyT) |
381 val mk_resp = Const (@{const_name Respects}, dummyT) |
358 *} |
382 *} |
386 in |
410 in |
387 if ty = ty' |
411 if ty = ty' |
388 then Abs (x, ty, subtrm) |
412 then Abs (x, ty, subtrm) |
389 else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm |
413 else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm |
390 end |
414 end |
|
415 |
391 | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => |
416 | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => |
392 let |
417 let |
393 val subtrm = apply_subt (regularize_trm lthy) t t' |
418 val subtrm = apply_subt (regularize_trm lthy) t t' |
394 in |
419 in |
395 if ty = ty' |
420 if ty = ty' |
396 then Const (@{const_name "All"}, ty) $ subtrm |
421 then Const (@{const_name "All"}, ty) $ subtrm |
397 else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
422 else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
398 end |
423 end |
|
424 |
399 | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
425 | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
400 let |
426 let |
401 val subtrm = apply_subt (regularize_trm lthy) t t' |
427 val subtrm = apply_subt (regularize_trm lthy) t t' |
402 in |
428 in |
403 if ty = ty' |
429 if ty = ty' |
404 then Const (@{const_name "Ex"}, ty) $ subtrm |
430 then Const (@{const_name "Ex"}, ty) $ subtrm |
405 else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
431 else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
406 end |
432 end |
407 (* FIXME: Should = only be replaced, when fully applied? *) |
433 |
408 (* Then there must be a 2nd argument *) |
434 | (* equalities need to be replaced by appropriate equivalence relations *) |
409 | (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') => |
435 (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => |
410 let |
436 if ty = ty' |
411 val subtrm = regularize_trm lthy t t' |
437 then rtrm |
|
438 else mk_resp_arg lthy (domain_type ty, domain_type ty') |
|
439 |
|
440 | (* in this case we check whether the given equivalence relation is correct *) |
|
441 (rel, Const (@{const_name "op ="}, ty')) => |
|
442 let |
|
443 val exc = LIFT_MATCH "regularise (relation mismatch)" |
|
444 val rel_ty = (fastype_of rel) handle TERM _ => raise exc |
|
445 val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') |
|
446 in |
|
447 if rel' = rel |
|
448 then rtrm |
|
449 else raise exc |
|
450 end |
|
451 | (_, Const (s, _)) => |
|
452 let |
|
453 fun same_name (Const (s, _)) (Const (s', _)) = (s = s') |
|
454 | same_name _ _ = false |
412 in |
455 in |
413 if ty = ty' |
456 if same_name rtrm qtrm |
414 then Const (@{const_name "op ="}, ty) $ subtrm |
457 then rtrm |
415 else mk_resp_arg lthy (domain_type ty, domain_type ty') $ subtrm |
458 else |
|
459 let |
|
460 fun exc1 s = LIFT_MATCH ("regularize (constant " ^ s ^ " not found)") |
|
461 val exc2 = LIFT_MATCH ("regularize (constant mismatch)") |
|
462 val thy = ProofContext.theory_of lthy |
|
463 val rtrm' = (#rconst (qconsts_lookup thy s)) handle NotFound => raise (exc1 s) |
|
464 in |
|
465 if matches_term (rtrm, rtrm') |
|
466 then rtrm |
|
467 else raise exc2 |
|
468 end |
416 end |
469 end |
|
470 |
417 | (t1 $ t2, t1' $ t2') => |
471 | (t1 $ t2, t1' $ t2') => |
418 (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2') |
472 (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2') |
|
473 |
419 | (Free (x, ty), Free (x', ty')) => |
474 | (Free (x, ty), Free (x', ty')) => |
420 (* this case cannot arrise as we start with two fully atomized terms *) |
475 (* this case cannot arrise as we start with two fully atomized terms *) |
421 raise (LIFT_MATCH "regularize (frees)") |
476 raise (LIFT_MATCH "regularize (frees)") |
|
477 |
422 | (Bound i, Bound i') => |
478 | (Bound i, Bound i') => |
423 if i = i' |
479 if i = i' |
424 then rtrm |
480 then rtrm |
425 else raise (LIFT_MATCH "regularize (bounds)") |
481 else raise (LIFT_MATCH "regularize (bounds mismatch)") |
426 | (Const (s, ty), Const (s', ty')) => |
482 |
427 if s = s' andalso ty = ty' |
483 |
428 then rtrm |
484 |
429 else rtrm (* FIXME: check correspondence according to definitions *) |
485 | (rt, qt) => |
430 | (rt, qt) => |
|
431 raise (LIFT_MATCH "regularize (default)") |
486 raise (LIFT_MATCH "regularize (default)") |
432 *} |
487 *} |
433 |
488 |
434 (* |
489 (* |
435 FIXME / TODO: needs to be adapted |
490 FIXME / TODO: needs to be adapted |
688 val (rhead, rargs) = strip_comb rtrm |
743 val (rhead, rargs) = strip_comb rtrm |
689 val (qhead, qargs) = strip_comb qtrm |
744 val (qhead, qargs) = strip_comb qtrm |
690 val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs) |
745 val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs) |
691 in |
746 in |
692 case (rhead, qhead) of |
747 case (rhead, qhead) of |
693 (Const _, Const _) => |
748 (Const (s, T), Const (s', T')) => |
694 if rty = qty |
749 if T = T' |
695 then list_comb (rhead, rargs') |
750 then list_comb (rhead, rargs') |
696 else mk_repabs lthy (rty, qty) (list_comb (rhead, rargs')) |
751 else list_comb (mk_repabs lthy (T, T') rhead, rargs') |
697 | (Free (x, T), Free (x', T')) => |
752 | (Free (x, T), Free (x', T')) => |
698 if T = T' |
753 if T = T' |
699 then list_comb (rhead, rargs') |
754 then list_comb (rhead, rargs') |
700 else list_comb (mk_repabs lthy (T, T') rhead, rargs') |
755 else list_comb (mk_repabs lthy (T, T') rhead, rargs') |
701 | (Abs _, Abs _) => |
756 | (Abs _, Abs _) => |