31 val id_thms = id_simps_get ctxt |
31 val id_thms = id_simps_get ctxt |
32 in |
32 in |
33 MetaSimplifier.rewrite_term thy id_thms [] trm |
33 MetaSimplifier.rewrite_term thy id_thms [] trm |
34 end |
34 end |
35 |
35 |
36 (******************************) |
36 |
37 (* Aggregate Rep/Abs Function *) |
37 |
38 (******************************) |
38 (*** Aggregate Rep/Abs Function ***) |
39 |
39 |
40 (* The flag repF is for types in negative position; absF is for types *) |
40 (* The flag repF is for types in negative position; absF is for types |
41 (* in positive position. Because of this, function types need to be *) |
41 in positive position. Because of this, function types need to be |
42 (* treated specially, since there the polarity changes. *) |
42 treated specially, since there the polarity changes. *) |
43 |
|
44 datatype flag = absF | repF |
43 datatype flag = absF | repF |
45 |
44 |
46 fun negF absF = repF |
45 fun negF absF = repF |
47 | negF repF = absF |
46 | negF repF = absF |
48 |
47 |
63 end |
62 end |
64 |
63 |
65 (* makes a Free out of a TVar *) |
64 (* makes a Free out of a TVar *) |
66 fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT) |
65 fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT) |
67 |
66 |
68 (* produces an aggregate map function for the *) |
67 (* produces an aggregate map function for the rty-part of a quotient |
69 (* rty-part of a quotient definition; abstracts *) |
68 definition; abstracts over all variables listed in vs (these variables |
70 (* over all variables listed in vs (these variables *) |
69 correspond to the type variables in rty) |
71 (* correspond to the type variables in rty) *) |
70 |
72 (* *) |
71 for example for: (?'a list * ?'b) |
73 (* for example for: (?'a list * ?'b) *) |
72 it produces: %a b. prod_map (map a) b *) |
74 (* it produces: %a b. prod_map (map a) b *) |
|
75 fun mk_mapfun ctxt vs rty = |
73 fun mk_mapfun ctxt vs rty = |
76 let |
74 let |
77 val vs' = map (mk_Free) vs |
75 val vs' = map (mk_Free) vs |
78 |
76 |
79 fun mk_mapfun_aux rty = |
77 fun mk_mapfun_aux rty = |
84 | _ => raise LIFT_MATCH ("mk_mapfun (default)") |
82 | _ => raise LIFT_MATCH ("mk_mapfun (default)") |
85 in |
83 in |
86 fold_rev Term.lambda vs' (mk_mapfun_aux rty) |
84 fold_rev Term.lambda vs' (mk_mapfun_aux rty) |
87 end |
85 end |
88 |
86 |
89 (* looks up the (varified) rty and qty for *) |
87 (* looks up the (varified) rty and qty for a quotient definition *) |
90 (* a quotient definition *) |
|
91 fun get_rty_qty ctxt s = |
88 fun get_rty_qty ctxt s = |
92 let |
89 let |
93 val thy = ProofContext.theory_of ctxt |
90 val thy = ProofContext.theory_of ctxt |
94 val exc = LIFT_MATCH ("No quotient type " ^ (quote s) ^ " found.") |
91 val exc = LIFT_MATCH ("No quotient type " ^ (quote s) ^ " found.") |
95 val qdata = (quotdata_lookup thy s) handle NotFound => raise exc |
92 val qdata = (quotdata_lookup thy s) handle NotFound => raise exc |
96 in |
93 in |
97 (#rtyp qdata, #qtyp qdata) |
94 (#rtyp qdata, #qtyp qdata) |
98 end |
95 end |
99 |
96 |
100 (* takes two type-environments and looks *) |
97 (* takes two type-environments and looks up in both of them the |
101 (* up in both of them the variable v, which *) |
98 variable v, which must be listed in the environment *) |
102 (* must be listed in the environment *) |
|
103 fun double_lookup rtyenv qtyenv v = |
99 fun double_lookup rtyenv qtyenv v = |
104 let |
100 let |
105 val v' = fst (dest_TVar v) |
101 val v' = fst (dest_TVar v) |
106 in |
102 in |
107 (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v'))) |
103 (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v'))) |
134 in |
130 in |
135 raise LIFT_MATCH (space_implode " " |
131 raise LIFT_MATCH (space_implode " " |
136 ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) |
132 ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) |
137 end |
133 end |
138 |
134 |
139 (* produces an aggregate absrep function *) |
135 (* produces an aggregate absrep function |
140 (* *) |
136 |
141 (* - In case of equal types we just return the identity. *) |
137 - In case of equal types we just return the identity. |
142 (* *) |
138 |
143 (* - In case of function types and TFrees, we recurse, taking in *) |
139 - In case of function types and TFrees, we recurse, taking in |
144 (* the first case the polarity change into account. *) |
140 the first case the polarity change into account. |
145 (* *) |
141 |
146 (* - If the type constructors are equal, we recurse for the *) |
142 - If the type constructors are equal, we recurse for the |
147 (* arguments and build the appropriate map function. *) |
143 arguments and build the appropriate map function. |
148 (* *) |
144 |
149 (* - If the type constructors are unequal, there must be an *) |
145 - If the type constructors are unequal, there must be an |
150 (* instance of quotient types: *) |
146 instance of quotient types: |
151 (* - we first look up the corresponding rty_pat and qty_pat *) |
147 - we first look up the corresponding rty_pat and qty_pat |
152 (* from the quotient definition; the arguments of qty_pat *) |
148 from the quotient definition; the arguments of qty_pat |
153 (* must be some distinct TVars *) |
149 must be some distinct TVars |
154 (* - we then match the rty_pat with rty and qty_pat with qty; *) |
150 - we then match the rty_pat with rty and qty_pat with qty; |
155 (* if matching fails the types do not match *) |
151 if matching fails the types do not match |
156 (* - the matching produces two environments; we look up the *) |
152 - the matching produces two environments; we look up the |
157 (* assignments for the qty_pat variables and recurse on the *) |
153 assignments for the qty_pat variables and recurse on the |
158 (* assignments *) |
154 assignments |
159 (* - we prefix the aggregate map function for the rty_pat, *) |
155 - we prefix the aggregate map function for the rty_pat, |
160 (* which is an abstraction over all type variables *) |
156 which is an abstraction over all type variables |
161 (* - finally we compose the result with the appropriate *) |
157 - finally we compose the result with the appropriate |
162 (* absrep function *) |
158 absrep function |
163 (* *) |
159 |
164 (* The composition is necessary for types like *) |
160 The composition is necessary for types like |
165 (* *) |
161 |
166 (* ('a list) list / ('a foo) foo *) |
162 ('a list) list / ('a foo) foo |
167 (* *) |
163 |
168 (* The matching is necessary for types like *) |
164 The matching is necessary for types like |
169 (* *) |
165 |
170 (* ('a * 'a) list / 'a bar *) |
166 ('a * 'a) list / 'a bar *) |
171 |
|
172 fun absrep_fun flag ctxt (rty, qty) = |
167 fun absrep_fun flag ctxt (rty, qty) = |
173 if rty = qty |
168 if rty = qty |
174 then mk_identity rty |
169 then mk_identity rty |
175 else |
170 else |
176 case (rty, qty) of |
171 case (rty, qty) of |
211 fun absrep_fun_chk flag ctxt (rty, qty) = |
206 fun absrep_fun_chk flag ctxt (rty, qty) = |
212 absrep_fun flag ctxt (rty, qty) |
207 absrep_fun flag ctxt (rty, qty) |
213 |> Syntax.check_term ctxt |
208 |> Syntax.check_term ctxt |
214 |> id_simplify ctxt |
209 |> id_simplify ctxt |
215 |
210 |
216 (**********************************) |
211 |
217 (* Aggregate Equivalence Relation *) |
212 |
218 (**********************************) |
213 (*** Aggregate Equivalence Relation ***) |
219 |
214 |
220 (* instantiates TVars so that the term is of type ty *) |
215 (* instantiates TVars so that the term is of type ty *) |
221 fun force_typ ctxt trm ty = |
216 fun force_typ ctxt trm ty = |
222 let |
217 let |
223 val thy = ProofContext.theory_of ctxt |
218 val thy = ProofContext.theory_of ctxt |
269 in |
264 in |
270 raise LIFT_MATCH (space_implode " " |
265 raise LIFT_MATCH (space_implode " " |
271 ["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.)"]) |
272 end |
267 end |
273 |
268 |
274 (* builds the aggregate equivalence relation *) |
269 (* builds the aggregate equivalence relation |
275 (* that will be the argument of Respects *) |
270 that will be the argument of Respects *) |
276 fun equiv_relation ctxt (rty, qty) = |
271 fun equiv_relation ctxt (rty, qty) = |
277 if rty = qty |
272 if rty = qty |
278 then HOLogic.eq_const rty |
273 then HOLogic.eq_const rty |
279 else |
274 else |
280 case (rty, qty) of |
275 case (rty, qty) of |
466 regularize_trm ctxt (rtrm, qtrm) |
460 regularize_trm ctxt (rtrm, qtrm) |
467 |> Syntax.check_term ctxt |
461 |> Syntax.check_term ctxt |
468 |> id_simplify ctxt |
462 |> id_simplify ctxt |
469 |
463 |
470 |
464 |
471 (*********************) |
465 |
472 (* Rep/Abs Injection *) |
466 (*** Rep/Abs Injection ***) |
473 (*********************) |
|
474 |
467 |
475 (* |
468 (* |
476 Injection of Rep/Abs means: |
469 Injection of Rep/Abs means: |
477 |
470 |
478 For abstractions |
471 For abstractions: |
479 : |
472 |
480 * If the type of the abstraction needs lifting, then we add Rep/Abs |
473 * If the type of the abstraction needs lifting, then we add Rep/Abs |
481 around the abstraction; otherwise we leave it unchanged. |
474 around the abstraction; otherwise we leave it unchanged. |
482 |
475 |
483 For applications: |
476 For applications: |
484 |
477 |
511 in |
504 in |
512 raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str]) |
505 raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str]) |
513 end |
506 end |
514 |
507 |
515 |
508 |
516 (* bound variables need to be treated properly, *) |
509 (* bound variables need to be treated properly, |
517 (* as the type of subterms needs to be calculated *) |
510 as the type of subterms needs to be calculated *) |
518 |
|
519 fun inj_repabs_trm ctxt (rtrm, qtrm) = |
511 fun inj_repabs_trm ctxt (rtrm, qtrm) = |
520 case (rtrm, qtrm) of |
512 case (rtrm, qtrm) of |
521 (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') => |
513 (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') => |
522 Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm ctxt (t, t')) |
514 Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm ctxt (t, t')) |
523 |
515 |