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 |
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 |
508 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
508 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
509 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
509 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
510 in |
510 in |
511 if resrel <> needrel |
511 if resrel <> needrel |
512 then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel |
512 then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel |
513 else mk_bexeq $ resrel $ subtrm |
513 else mk_bex1_rel $ resrel $ subtrm |
514 end |
514 end |
515 |
515 |
516 | (Const (@{const_name "Bex1"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, |
516 | (Const (@{const_name "Bex1"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, |
517 Const (@{const_name "Ex1"}, ty') $ t') => |
517 Const (@{const_name "Ex1"}, ty') $ t') => |
518 let |
518 let |
519 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
519 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
520 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
520 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
521 in |
521 in |
522 if resrel <> needrel |
522 if resrel <> needrel |
523 then term_mismatch "regularize (Bex1)" ctxt resrel needrel |
523 then term_mismatch "regularize (Bex1)" ctxt resrel needrel |
524 else mk_bexeq $ resrel $ subtrm |
524 else mk_bex1_rel $ resrel $ subtrm |
525 end |
525 end |
526 |
526 |
527 | (* equalities need to be replaced by appropriate equivalence relations *) |
527 | (* equalities need to be replaced by appropriate equivalence relations *) |
528 (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => |
528 (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => |
529 if ty = ty' then rtrm |
529 if ty = ty' then rtrm |