386 |
386 |
387 val mk_babs = Const (@{const_name Babs}, dummyT) |
387 val mk_babs = Const (@{const_name Babs}, dummyT) |
388 val mk_ball = Const (@{const_name Ball}, dummyT) |
388 val mk_ball = Const (@{const_name Ball}, dummyT) |
389 val mk_bex = Const (@{const_name Bex}, dummyT) |
389 val mk_bex = Const (@{const_name Bex}, dummyT) |
390 val mk_bex1 = Const (@{const_name Bex1}, dummyT) |
390 val mk_bex1 = Const (@{const_name Bex1}, dummyT) |
391 val mk_bexeq = Const (@{const_name Bex1_rel}, dummyT) |
391 val mk_bex1_rel = Const (@{const_name Bex1_rel}, dummyT) |
392 val mk_resp = Const (@{const_name Respects}, dummyT) |
392 val mk_resp = Const (@{const_name Respects}, dummyT) |
393 |
393 |
394 (* - applies f to the subterm of an abstraction, |
394 (* - applies f to the subterm of an abstraction, |
395 otherwise to the given term, |
395 otherwise to the given term, |
396 - used by regularize, therefore abstracted |
396 - used by regularize, therefore abstracted |
444 val subtrm = Abs(x, ty, regularize_trm ctxt (t, t')) |
444 val subtrm = Abs(x, ty, regularize_trm ctxt (t, t')) |
445 in |
445 in |
446 if ty = ty' then subtrm |
446 if ty = ty' then subtrm |
447 else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm |
447 else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm |
448 end |
448 end |
449 | (Const (@{const_name "Babs"}, T) $ r $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) => |
449 | (Const (@{const_name "Babs"}, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) => |
450 let |
450 let |
451 val subtrm = regularize_trm ctxt (t, t') |
451 val subtrm = regularize_trm ctxt (t, t') |
452 val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty') |
452 val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty') |
453 in |
453 in |
454 if r <> needres |
454 if resrel <> needres |
455 then term_mismatch "regularize (Babs)" ctxt r needres |
455 then term_mismatch "regularize (Babs)" ctxt resrel needres |
456 else mk_babs $ r $ subtrm |
456 else mk_babs $ resrel $ subtrm |
457 end |
457 end |
458 |
458 |
459 | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => |
459 | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => |
460 let |
460 let |
461 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
461 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
475 | (Const (@{const_name "Ex1"}, ty) $ t, Const (@{const_name "Ex1"}, ty') $ t') => |
475 | (Const (@{const_name "Ex1"}, ty) $ t, Const (@{const_name "Ex1"}, ty') $ t') => |
476 let |
476 let |
477 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
477 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
478 in |
478 in |
479 if ty = ty' then Const (@{const_name "Ex1"}, ty) $ subtrm |
479 if ty = ty' then Const (@{const_name "Ex1"}, ty) $ subtrm |
480 else mk_bexeq $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
480 else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
481 end |
481 end |
482 |
482 |
483 | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, |
483 | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, |
484 Const (@{const_name "All"}, ty') $ t') => |
484 Const (@{const_name "All"}, ty') $ t') => |
485 let |
485 let |
489 if resrel <> needrel |
489 if resrel <> needrel |
490 then term_mismatch "regularize (Ball)" ctxt resrel needrel |
490 then term_mismatch "regularize (Ball)" ctxt resrel needrel |
491 else mk_ball $ (mk_resp $ resrel) $ subtrm |
491 else mk_ball $ (mk_resp $ resrel) $ subtrm |
492 end |
492 end |
493 |
493 |
494 |
|
495 | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, |
494 | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, |
496 Const (@{const_name "Ex"}, ty') $ t') => |
495 Const (@{const_name "Ex"}, ty') $ t') => |
497 let |
496 let |
498 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
497 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
499 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
498 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
508 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
507 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
509 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
508 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
510 in |
509 in |
511 if resrel <> needrel |
510 if resrel <> needrel |
512 then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel |
511 then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel |
513 else mk_bexeq $ resrel $ subtrm |
512 else mk_bex1_rel $ resrel $ subtrm |
514 end |
513 end |
515 |
514 |
516 | (Const (@{const_name "Bex1"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, |
515 | (Const (@{const_name "Bex1"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, |
517 Const (@{const_name "Ex1"}, ty') $ t') => |
516 Const (@{const_name "Ex1"}, ty') $ t') => |
518 let |
517 let |
519 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
518 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
520 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
519 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
521 in |
520 in |
522 if resrel <> needrel |
521 if resrel <> needrel |
523 then term_mismatch "regularize (Bex1)" ctxt resrel needrel |
522 then term_mismatch "regularize (Bex1)" ctxt resrel needrel |
524 else mk_bexeq $ resrel $ subtrm |
523 else mk_bex1_rel $ resrel $ subtrm |
525 end |
524 end |
526 |
525 |
527 | (* equalities need to be replaced by appropriate equivalence relations *) |
526 | (* equalities need to be replaced by appropriate equivalence relations *) |
528 (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => |
527 (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => |
529 if ty = ty' then rtrm |
528 if ty = ty' then rtrm |
554 if Pattern.matches thy (rtrm', rtrm) |
553 if Pattern.matches thy (rtrm', rtrm) |
555 then rtrm else term_mismatch "regularize(constant mismatch)" ctxt rtrm qtrm |
554 then rtrm else term_mismatch "regularize(constant mismatch)" ctxt rtrm qtrm |
556 end |
555 end |
557 end |
556 end |
558 |
557 |
559 | (((t1 as Const (@{const_name "split"}, _)) $ Abs(v1, ty, Abs(v1', ty', s1))), |
558 | (((t1 as Const (@{const_name "split"}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))), |
560 ((t2 as Const (@{const_name "split"}, _)) $ Abs(v2, _ , Abs(v2', _ , s2)))) => |
559 ((t2 as Const (@{const_name "split"}, _)) $ Abs (v2, _ , Abs(v2', _ , s2)))) => |
561 (regularize_trm ctxt (t1, t2)) $ Abs(v1, ty, Abs(v1', ty', regularize_trm ctxt (s1, s2))) |
560 regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2))) |
562 |
561 |
563 | (((t1 as Const (@{const_name "split"}, _)) $ Abs(v1, ty, s1)), |
562 | (((t1 as Const (@{const_name "split"}, _)) $ Abs (v1, ty, s1)), |
564 ((t2 as Const (@{const_name "split"}, _)) $ Abs(v2, _ , s2))) => |
563 ((t2 as Const (@{const_name "split"}, _)) $ Abs (v2, _ , s2))) => |
565 (regularize_trm ctxt (t1, t2)) $ Abs(v1, ty, regularize_trm ctxt (s1, s2)) |
564 regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2)) |
566 |
565 |
567 | (t1 $ t2, t1' $ t2') => |
566 | (t1 $ t2, t1' $ t2') => |
568 (regularize_trm ctxt (t1, t1')) $ (regularize_trm ctxt (t2, t2')) |
567 regularize_trm ctxt (t1, t1') $ regularize_trm ctxt (t2, t2') |
569 |
568 |
570 | (Bound i, Bound i') => |
569 | (Bound i, Bound i') => |
571 if i = i' then rtrm |
570 if i = i' then rtrm |
572 else raise (LIFT_MATCH "regularize (bounds mismatch)") |
571 else raise (LIFT_MATCH "regularize (bounds mismatch)") |
573 |
572 |