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 |
53 | repF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 |
53 | repF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 |
54 |
54 |
55 fun get_mapfun ctxt s = |
55 fun get_mapfun ctxt s = |
56 let |
56 let |
57 val thy = ProofContext.theory_of ctxt |
57 val thy = ProofContext.theory_of ctxt |
58 val exc = LIFT_MATCH ("No map function for type " ^ (quote s) ^ " found.") |
58 val exc = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.") |
59 val mapfun = #mapfun (maps_lookup thy s) handle NotFound => raise exc |
59 val mapfun = #mapfun (maps_lookup thy s) handle NotFound => raise exc |
60 in |
60 in |
61 Const (mapfun, dummyT) |
61 Const (mapfun, dummyT) |
62 end |
62 end |
63 |
63 |
86 |
86 |
87 (* looks up the (varified) rty and qty for a quotient definition *) |
87 (* looks up the (varified) rty and qty for a quotient definition *) |
88 fun get_rty_qty ctxt s = |
88 fun get_rty_qty ctxt s = |
89 let |
89 let |
90 val thy = ProofContext.theory_of ctxt |
90 val thy = ProofContext.theory_of ctxt |
91 val exc = LIFT_MATCH ("No quotient type " ^ (quote s) ^ " found.") |
91 val exc = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.") |
92 val qdata = (quotdata_lookup thy s) handle NotFound => raise exc |
92 val qdata = (quotdata_lookup thy s) handle NotFound => raise exc |
93 in |
93 in |
94 (#rtyp qdata, #qtyp qdata) |
94 (#rtyp qdata, #qtyp qdata) |
95 end |
95 end |
96 |
96 |
265 raise LIFT_MATCH (space_implode " " |
265 raise LIFT_MATCH (space_implode " " |
266 ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) |
266 ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) |
267 end |
267 end |
268 |
268 |
269 (* builds the aggregate equivalence relation |
269 (* builds the aggregate equivalence relation |
270 that will be the argument of Respects *) |
270 that will be the argument of Respects *) |
271 fun equiv_relation ctxt (rty, qty) = |
271 fun equiv_relation ctxt (rty, qty) = |
272 if rty = qty |
272 if rty = qty |
273 then HOLogic.eq_const rty |
273 then HOLogic.eq_const rty |
274 else |
274 else |
275 case (rty, qty) of |
275 case (rty, qty) of |
305 |
305 |
306 |
306 |
307 (*** Regularization ***) |
307 (*** Regularization ***) |
308 |
308 |
309 (* Regularizing an rtrm means: |
309 (* Regularizing an rtrm means: |
310 |
310 |
311 - Quantifiers over types that need lifting are replaced |
311 - Quantifiers over types that need lifting are replaced |
312 by bounded quantifiers, for example: |
312 by bounded quantifiers, for example: |
313 |
313 |
314 All P ----> All (Respects R) P |
314 All P ----> All (Respects R) P |
315 |
315 |
316 where the aggregate relation R is given by the rty and qty; |
316 where the aggregate relation R is given by the rty and qty; |
317 |
317 |
318 - Abstractions over types that need lifting are replaced |
318 - Abstractions over types that need lifting are replaced |
319 by bounded abstractions, for example: |
319 by bounded abstractions, for example: |
320 |
320 |
321 %x. P ----> Ball (Respects R) %x. P |
321 %x. P ----> Ball (Respects R) %x. P |
322 |
322 |
323 - Equalities over types that need lifting are replaced by |
323 - Equalities over types that need lifting are replaced by |
324 corresponding equivalence relations, for example: |
324 corresponding equivalence relations, for example: |
325 |
325 |
326 A = B ----> R A B |
326 A = B ----> R A B |
327 |
327 |
328 or |
328 or |
329 |
329 |
330 A = B ----> (R ===> R) A B |
330 A = B ----> (R ===> R) A B |
331 |
331 |
332 for more complicated types of A and B |
332 for more complicated types of A and B |
333 *) |
333 *) |
334 |
334 |
335 |
335 |
336 val mk_babs = Const (@{const_name Babs}, dummyT) |
336 val mk_babs = Const (@{const_name Babs}, dummyT) |
337 val mk_ball = Const (@{const_name Ball}, dummyT) |
337 val mk_ball = Const (@{const_name Ball}, dummyT) |
338 val mk_bex = Const (@{const_name Bex}, dummyT) |
338 val mk_bex = Const (@{const_name Bex}, dummyT) |
339 val mk_resp = Const (@{const_name Respects}, dummyT) |
339 val mk_resp = Const (@{const_name Respects}, dummyT) |
340 |
340 |
346 case (trm1, trm2) of |
346 case (trm1, trm2) of |
347 (Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f (t, t')) |
347 (Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f (t, t')) |
348 | _ => f (trm1, trm2) |
348 | _ => f (trm1, trm2) |
349 |
349 |
350 (* the major type of All and Ex quantifiers *) |
350 (* the major type of All and Ex quantifiers *) |
351 fun qnt_typ ty = domain_type (domain_type ty) |
351 fun qnt_typ ty = domain_type (domain_type ty) |
352 |
352 |
353 |
353 |
354 (* produces a regularized version of rtrm *) |
354 (* produces a regularized version of rtrm |
355 (* *) |
355 - the result might contain dummyTs |
356 (* - the result might contain dummyTs *) |
356 - for regularisation we do not need to treat bound variables specially *) |
357 (* *) |
|
358 (* - for regularisation we do not need any *) |
|
359 (* special treatment of bound variables *) |
|
360 |
|
361 fun regularize_trm ctxt (rtrm, qtrm) = |
357 fun regularize_trm ctxt (rtrm, qtrm) = |
362 case (rtrm, qtrm) of |
358 case (rtrm, qtrm) of |
363 (Abs (x, ty, t), Abs (_, ty', t')) => |
359 (Abs (x, ty, t), Abs (_, ty', t')) => |
364 let |
360 let |
365 val subtrm = Abs(x, ty, regularize_trm ctxt (t, t')) |
361 val subtrm = Abs(x, ty, regularize_trm ctxt (t, t')) |