509 if Pattern.matches thy (rtrm', rtrm) |
509 if Pattern.matches thy (rtrm', rtrm) |
510 then rtrm else term_mismatch "regularize(constant mismatch)" ctxt rtrm qtrm |
510 then rtrm else term_mismatch "regularize(constant mismatch)" ctxt rtrm qtrm |
511 end |
511 end |
512 end |
512 end |
513 |
513 |
|
514 | (((t1 as Const (@{const_name "split"}, _)) $ Abs(v1, ty, Abs(v1', ty', s1))), |
|
515 ((t2 as Const (@{const_name "split"}, _)) $ Abs(v2, _ , Abs(v2', _ , s2)))) => |
|
516 (regularize_trm ctxt (t1, t2)) $ Abs(v1, ty, Abs(v1', ty', regularize_trm ctxt (s1, s2))) |
|
517 |
|
518 | (((t1 as Const (@{const_name "split"}, _)) $ Abs(v1, ty, s1)), |
|
519 ((t2 as Const (@{const_name "split"}, _)) $ Abs(v2, _ , s2))) => |
|
520 (regularize_trm ctxt (t1, t2)) $ Abs(v1, ty, regularize_trm ctxt (s1, s2)) |
|
521 |
514 | (t1 $ t2, t1' $ t2') => |
522 | (t1 $ t2, t1' $ t2') => |
515 (regularize_trm ctxt (t1, t1')) $ (regularize_trm ctxt (t2, t2')) |
523 (regularize_trm ctxt (t1, t1')) $ (regularize_trm ctxt (t2, t2')) |
516 |
524 |
517 | (Bound i, Bound i') => |
525 | (Bound i, Bound i') => |
518 if i = i' then rtrm |
526 if i = i' then rtrm |