365 |
365 |
366 val mk_babs = Const (@{const_name Babs}, dummyT) |
366 val mk_babs = Const (@{const_name Babs}, dummyT) |
367 val mk_ball = Const (@{const_name Ball}, dummyT) |
367 val mk_ball = Const (@{const_name Ball}, dummyT) |
368 val mk_bex = Const (@{const_name Bex}, dummyT) |
368 val mk_bex = Const (@{const_name Bex}, dummyT) |
369 val mk_bex1 = Const (@{const_name Bex1}, dummyT) |
369 val mk_bex1 = Const (@{const_name Bex1}, dummyT) |
|
370 val mk_bexeq = Const (@{const_name Bexeq}, dummyT) |
370 val mk_resp = Const (@{const_name Respects}, dummyT) |
371 val mk_resp = Const (@{const_name Respects}, dummyT) |
371 |
372 |
372 (* - applies f to the subterm of an abstraction, |
373 (* - applies f to the subterm of an abstraction, |
373 otherwise to the given term, |
374 otherwise to the given term, |
374 - used by regularize, therefore abstracted |
375 - used by regularize, therefore abstracted |
464 | (Const (@{const_name "Ex1"}, ty) $ t, Const (@{const_name "Ex1"}, ty') $ t') => |
465 | (Const (@{const_name "Ex1"}, ty) $ t, Const (@{const_name "Ex1"}, ty') $ t') => |
465 let |
466 let |
466 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
467 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
467 in |
468 in |
468 if ty = ty' then Const (@{const_name "Ex1"}, ty) $ subtrm |
469 if ty = ty' then Const (@{const_name "Ex1"}, ty) $ subtrm |
469 else mk_bex1 $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
470 else mk_bexeq $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
470 end |
471 end |
471 |
472 |
472 | (Const (@{const_name "Bex1"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, Const (@{const_name "Ex1"}, ty') $ t') => |
473 | (Const (@{const_name "Bexeq"}, ty) $ resrel $ t, Const (@{const_name "Ex1"}, ty') $ t') => |
473 let |
474 let |
474 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
475 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
475 val needrel = Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) |
476 val needrel = Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) |
476 in |
477 in |
477 if resrel <> needrel |
478 if resrel <> needrel |
478 then term_mismatch "regularize(bex1)" ctxt resrel needrel |
479 then term_mismatch "regularize(bex1)" ctxt resrel needrel |
479 else mk_bex1 $ (mk_resp $ resrel) $ subtrm |
480 else mk_bexeq $ resrel $ subtrm |
480 end |
481 end |
481 |
482 |
482 | (* equalities need to be replaced by appropriate equivalence relations *) |
483 | (* equalities need to be replaced by appropriate equivalence relations *) |
483 (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => |
484 (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => |
484 if ty = ty' then rtrm |
485 if ty = ty' then rtrm |