| changeset 856 | 433f7c17255f |
| parent 854 | 5961edda27d7 |
| parent 853 | 3fd1365f5729 |
| child 858 | bb012513fb39 |
| 855:017cb46b27bb | 856:433f7c17255f |
|---|---|
1 signature QUOTIENT_TERM = |
1 signature QUOTIENT_TERM = |
2 sig |
2 sig |
3 exception LIFT_MATCH of string |
3 exception LIFT_MATCH of string |
4 |
4 |
5 datatype flag = absF | repF |
5 datatype flag = absF | repF |
6 |
6 |
7 val absrep_fun: flag -> Proof.context -> (typ * typ) -> term |
7 val absrep_fun: flag -> Proof.context -> typ * typ -> term |
8 val absrep_fun_chk: flag -> Proof.context -> (typ * typ) -> term |
8 val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term |
9 |
9 |
10 val equiv_relation: Proof.context -> (typ * typ) -> term |
10 val equiv_relation: Proof.context -> typ * typ -> term |
11 val equiv_relation_chk: Proof.context -> (typ * typ) -> term |
11 val equiv_relation_chk: Proof.context -> typ * typ -> term |
12 |
12 |
13 val regularize_trm: Proof.context -> (term * term) -> term |
13 val regularize_trm: Proof.context -> term * term -> term |
14 val regularize_trm_chk: Proof.context -> (term * term) -> term |
14 val regularize_trm_chk: Proof.context -> term * term -> term |
15 |
15 |
16 val inj_repabs_trm: Proof.context -> (term * term) -> term |
16 val inj_repabs_trm: Proof.context -> term * term -> term |
17 val inj_repabs_trm_chk: Proof.context -> (term * term) -> term |
17 val inj_repabs_trm_chk: Proof.context -> term * term -> term |
18 end; |
18 end; |
19 |
19 |
20 structure Quotient_Term: QUOTIENT_TERM = |
20 structure Quotient_Term: QUOTIENT_TERM = |
21 struct |
21 struct |
22 |
22 |
50 | repF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 |
50 | repF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 |
51 |
51 |
52 fun get_mapfun ctxt s = |
52 fun get_mapfun ctxt s = |
53 let |
53 let |
54 val thy = ProofContext.theory_of ctxt |
54 val thy = ProofContext.theory_of ctxt |
55 val exc = LIFT_MATCH ("No map function for type " ^ (quote s) ^ " found.") |
55 val exc = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.") |
56 val mapfun = #mapfun (maps_lookup thy s) handle NotFound => raise exc |
56 val mapfun = #mapfun (maps_lookup thy s) handle NotFound => raise exc |
57 in |
57 in |
58 Const (mapfun, dummyT) |
58 Const (mapfun, dummyT) |
59 end |
59 end |
60 |
60 |
87 a quotient definition |
87 a quotient definition |
88 *) |
88 *) |
89 fun get_rty_qty ctxt s = |
89 fun get_rty_qty ctxt s = |
90 let |
90 let |
91 val thy = ProofContext.theory_of ctxt |
91 val thy = ProofContext.theory_of ctxt |
92 val exc = LIFT_MATCH ("No quotient type " ^ (quote s) ^ " found.") |
92 val exc = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.") |
93 val qdata = (quotdata_lookup thy s) handle NotFound => raise exc |
93 val qdata = (quotdata_lookup thy s) handle NotFound => raise exc |
94 in |
94 in |
95 (#rtyp qdata, #qtyp qdata) |
95 (#rtyp qdata, #qtyp qdata) |
96 end |
96 end |
97 |
97 |
349 - Equalities over types that need lifting are replaced by |
349 - Equalities over types that need lifting are replaced by |
350 corresponding equivalence relations, for example: |
350 corresponding equivalence relations, for example: |
351 |
351 |
352 A = B ----> R A B |
352 A = B ----> R A B |
353 |
353 |
354 or |
354 or |
355 |
355 |
356 A = B ----> (R ===> R) A B |
356 A = B ----> (R ===> R) A B |
357 |
357 |
358 for more complicated types of A and B |
358 for more complicated types of A and B |
359 *) |
359 *) |
360 |
360 |
361 |
361 |
362 val mk_babs = Const (@{const_name Babs}, dummyT) |
362 val mk_babs = Const (@{const_name Babs}, dummyT) |
363 val mk_ball = Const (@{const_name Ball}, dummyT) |
363 val mk_ball = Const (@{const_name Ball}, dummyT) |
364 val mk_bex = Const (@{const_name Bex}, dummyT) |
364 val mk_bex = Const (@{const_name Bex}, dummyT) |
365 val mk_resp = Const (@{const_name Respects}, dummyT) |
365 val mk_resp = Const (@{const_name Respects}, dummyT) |
366 |
366 |
373 case (trm1, trm2) of |
373 case (trm1, trm2) of |
374 (Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f (t, t')) |
374 (Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f (t, t')) |
375 | _ => f (trm1, trm2) |
375 | _ => f (trm1, trm2) |
376 |
376 |
377 (* the major type of All and Ex quantifiers *) |
377 (* the major type of All and Ex quantifiers *) |
378 fun qnt_typ ty = domain_type (domain_type ty) |
378 fun qnt_typ ty = domain_type (domain_type ty) |
379 |
379 |
380 (* produces a regularized version of rtrm |
380 (* produces a regularized version of rtrm |
381 |
381 |
382 - the result might contain dummyTs |
382 - the result might contain dummyTs |
383 |
383 |
384 - for regularisation we do not need any |
384 - for regularisation we do not need any |
385 special treatment of bound variables |
385 special treatment of bound variables |
485 fun regularize_trm_chk ctxt (rtrm, qtrm) = |
485 fun regularize_trm_chk ctxt (rtrm, qtrm) = |
486 regularize_trm ctxt (rtrm, qtrm) |
486 regularize_trm ctxt (rtrm, qtrm) |
487 |> Syntax.check_term ctxt |
487 |> Syntax.check_term ctxt |
488 |
488 |
489 |
489 |
490 (*********************) |
490 |
491 (* Rep/Abs Injection *) |
491 (*** Rep/Abs Injection ***) |
492 (*********************) |
|
493 |
492 |
494 (* |
493 (* |
495 Injection of Rep/Abs means: |
494 Injection of Rep/Abs means: |
496 |
495 |
497 For abstractions |
496 For abstractions: |
498 : |
497 |
499 * If the type of the abstraction needs lifting, then we add Rep/Abs |
498 * If the type of the abstraction needs lifting, then we add Rep/Abs |
500 around the abstraction; otherwise we leave it unchanged. |
499 around the abstraction; otherwise we leave it unchanged. |
501 |
500 |
502 For applications: |
501 For applications: |
503 |
502 |
530 in |
529 in |
531 raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str]) |
530 raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str]) |
532 end |
531 end |
533 |
532 |
534 |
533 |
535 (* bound variables need to be treated properly, *) |
534 (* bound variables need to be treated properly, |
536 (* as the type of subterms needs to be calculated *) |
535 as the type of subterms needs to be calculated *) |
537 |
|
538 fun inj_repabs_trm ctxt (rtrm, qtrm) = |
536 fun inj_repabs_trm ctxt (rtrm, qtrm) = |
539 case (rtrm, qtrm) of |
537 case (rtrm, qtrm) of |
540 (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') => |
538 (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') => |
541 Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm ctxt (t, t')) |
539 Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm ctxt (t, t')) |
542 |
540 |