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') |
488 in |
488 in |
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 |
|
494 |
493 |
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') |
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 |