|
1 (* Title: quotient_term.thy |
|
2 Author: Cezary Kaliszyk and Christian Urban |
|
3 |
|
4 Constructs terms corresponding to goals from |
|
5 lifting theorems to quotient types. |
|
6 *) |
|
7 |
1 signature QUOTIENT_TERM = |
8 signature QUOTIENT_TERM = |
2 sig |
9 sig |
3 exception LIFT_MATCH of string |
10 exception LIFT_MATCH of string |
4 |
11 |
5 datatype flag = absF | repF |
12 datatype flag = absF | repF |
6 |
|
7 val absrep_const_chk: flag -> Proof.context -> string -> term |
|
8 |
13 |
9 val absrep_fun: flag -> Proof.context -> typ * typ -> term |
14 val absrep_fun: flag -> Proof.context -> typ * typ -> term |
10 val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term |
15 val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term |
11 |
16 |
12 val equiv_relation: Proof.context -> typ * typ -> term |
17 val equiv_relation: Proof.context -> typ * typ -> term |
125 in |
130 in |
126 case flag of |
131 case flag of |
127 absF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT) |
132 absF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT) |
128 | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT) |
133 | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT) |
129 end |
134 end |
130 |
|
131 fun absrep_const_chk flag ctxt qty_str = |
|
132 Syntax.check_term ctxt (absrep_const flag ctxt qty_str) |
|
133 |
135 |
134 fun absrep_match_err ctxt ty_pat ty = |
136 fun absrep_match_err ctxt ty_pat ty = |
135 let |
137 let |
136 val ty_pat_str = Syntax.string_of_typ ctxt ty_pat |
138 val ty_pat_str = Syntax.string_of_typ ctxt ty_pat |
137 val ty_str = Syntax.string_of_typ ctxt ty |
139 val ty_str = Syntax.string_of_typ ctxt ty |
432 in |
434 in |
433 if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm |
435 if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm |
434 else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
436 else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
435 end |
437 end |
436 |
438 |
437 | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, Const (@{const_name "All"}, ty') $ t') => |
439 | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, |
|
440 Const (@{const_name "All"}, ty') $ t') => |
438 let |
441 let |
439 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
442 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
440 val needrel = Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) |
443 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
441 in |
444 in |
442 if resrel <> needrel |
445 if resrel <> needrel |
443 then term_mismatch "regularize(ball)" ctxt resrel needrel |
446 then term_mismatch "regularize (Ball)" ctxt resrel needrel |
444 else mk_ball $ (mk_resp $ resrel) $ subtrm |
447 else mk_ball $ (mk_resp $ resrel) $ subtrm |
445 end |
448 end |
446 |
449 |
447 | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
450 | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
448 let |
451 let |
450 in |
453 in |
451 if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm |
454 if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm |
452 else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
455 else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
453 end |
456 end |
454 |
457 |
455 | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
458 | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, |
|
459 Const (@{const_name "Ex"}, ty') $ t') => |
456 let |
460 let |
457 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
461 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
458 val needrel = Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) |
462 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
459 in |
463 in |
460 if resrel <> needrel |
464 if resrel <> needrel |
461 then term_mismatch "regularize(bex)" ctxt resrel needrel |
465 then term_mismatch "regularize (Bex)" ctxt resrel needrel |
462 else mk_bex $ (mk_resp $ resrel) $ subtrm |
466 else mk_bex $ (mk_resp $ resrel) $ subtrm |
463 end |
467 end |
464 |
468 |
465 | (Const (@{const_name "Ex1"}, ty) $ t, Const (@{const_name "Ex1"}, ty') $ t') => |
469 | (Const (@{const_name "Ex1"}, ty) $ t, Const (@{const_name "Ex1"}, ty') $ t') => |
466 let |
470 let |
471 end |
475 end |
472 |
476 |
473 | (Const (@{const_name "Bexeq"}, ty) $ resrel $ t, Const (@{const_name "Ex1"}, ty') $ t') => |
477 | (Const (@{const_name "Bexeq"}, ty) $ resrel $ t, Const (@{const_name "Ex1"}, ty') $ t') => |
474 let |
478 let |
475 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
479 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
476 val needrel = Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) |
480 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
477 in |
481 in |
478 if resrel <> needrel |
482 if resrel <> needrel |
479 then term_mismatch "regularize(bex1_res)" ctxt resrel needrel |
483 then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel |
480 else mk_bexeq $ resrel $ subtrm |
484 else mk_bexeq $ resrel $ subtrm |
481 end |
485 end |
482 |
486 |
483 | (Const (@{const_name "Bex1"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, Const (@{const_name "Ex1"}, ty') $ t') => |
487 | (Const (@{const_name "Bex1"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, |
|
488 Const (@{const_name "Ex1"}, ty') $ t') => |
484 let |
489 let |
485 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
490 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
486 val needrel = Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) |
491 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
487 in |
492 in |
488 if resrel <> needrel |
493 if resrel <> needrel |
489 then term_mismatch "regularize(bex1)" ctxt resrel needrel |
494 then term_mismatch "regularize (Bex1)" ctxt resrel needrel |
490 else mk_bexeq $ resrel $ subtrm |
495 else mk_bexeq $ resrel $ subtrm |
491 end |
496 end |
492 |
497 |
493 | (* equalities need to be replaced by appropriate equivalence relations *) |
498 | (* equalities need to be replaced by appropriate equivalence relations *) |
494 (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => |
499 (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => |
499 (rel, Const (@{const_name "op ="}, ty')) => |
504 (rel, Const (@{const_name "op ="}, ty')) => |
500 let |
505 let |
501 val rel_ty = fastype_of rel |
506 val rel_ty = fastype_of rel |
502 val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty') |
507 val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty') |
503 in |
508 in |
504 if rel' aconv rel then rtrm else term_mismatch "regularise (relation mismatch)" ctxt rel rel' |
509 if rel' aconv rel then rtrm |
|
510 else term_mismatch "regularise (relation mismatch)" ctxt rel rel' |
505 end |
511 end |
506 |
512 |
507 | (_, Const _) => |
513 | (_, Const _) => |
508 let |
514 let |
509 val thy = ProofContext.theory_of ctxt |
515 val thy = ProofContext.theory_of ctxt |