8 struct |
8 struct |
9 |
9 |
10 (* |
10 (* |
11 Regularizing an rtrm means: |
11 Regularizing an rtrm means: |
12 |
12 |
13 - Quantifiers over a type that need lifting are replaced |
13 - Quantifiers over types that need lifting are replaced |
14 by bounded quantifiers, for example: |
14 by bounded quantifiers, for example: |
15 |
15 |
16 All P ===> All (Respects R) P |
16 All P ----> All (Respects R) P |
17 |
17 |
18 where the relation R is given by the rty and qty; |
18 where the aggregate relation R is given by the rty and qty; |
19 |
19 |
20 - Abstractions over a type that needs lifting are replaced |
20 - Abstractions over types that need lifting are replaced |
21 by bounded abstractions: |
21 by bounded abstractions, for example: |
22 |
22 |
23 %x. P ===> Ball (Respects R) %x. P |
23 %x. P ----> Ball (Respects R) %x. P |
24 |
24 |
25 - Equalities over the type being lifted are replaced by |
25 - Equalities over types that need lifting are replaced by |
26 corresponding equivalence relations: |
26 corresponding equivalence relations, for example: |
27 |
27 |
28 A = B ===> R A B |
28 A = B ----> R A B |
29 |
29 |
30 or |
30 or |
31 |
31 |
32 A = B ===> (R ===> R) A B |
32 A = B ----> (R ===> R) A B |
33 |
33 |
34 for more complicated types of A and B |
34 for more complicated types of A and B |
35 *) |
35 *) |
36 |
36 |
37 (* builds the relation that is the argument of respects *) |
37 (* builds the aggregate equivalence relation *) |
|
38 (* that will be the argument of Respects *) |
38 fun mk_resp_arg lthy (rty, qty) = |
39 fun mk_resp_arg lthy (rty, qty) = |
39 let |
40 let |
40 val thy = ProofContext.theory_of lthy |
41 val thy = ProofContext.theory_of lthy |
41 in |
42 in |
42 if rty = qty |
43 if rty = qty |
44 else |
45 else |
45 case (rty, qty) of |
46 case (rty, qty) of |
46 (Type (s, tys), Type (s', tys')) => |
47 (Type (s, tys), Type (s', tys')) => |
47 if s = s' |
48 if s = s' |
48 then let |
49 then let |
49 val SOME map_info = maps_lookup thy s |
50 val map_info = maps_lookup thy s |
50 (* FIXME dont return an option, raise an exception *) |
51 handle NotFound => |
|
52 raise LIFT_MATCH ("mk_resp_arg (no map function found for type " ^ s) |
51 val args = map (mk_resp_arg lthy) (tys ~~ tys') |
53 val args = map (mk_resp_arg lthy) (tys ~~ tys') |
52 in |
54 in |
53 list_comb (Const (#relfun map_info, dummyT), args) |
55 list_comb (Const (#relfun map_info, dummyT), args) |
54 end |
56 end |
55 else let |
57 else let |
86 fun qnt_typ ty = domain_type (domain_type ty) |
88 fun qnt_typ ty = domain_type (domain_type ty) |
87 |
89 |
88 |
90 |
89 (* produces a regularized version of rtrm *) |
91 (* produces a regularized version of rtrm *) |
90 (* *) |
92 (* *) |
91 (* - the result is still contains dummyT *) |
93 (* - the result still contains dummyTs *) |
92 (* *) |
94 (* *) |
93 (* - for regularisation we do not need any *) |
95 (* - for regularisation we do not need any *) |
94 (* special treatment of bound variables *) |
96 (* special treatment of bound variables *) |
95 |
97 |
96 fun regularize_trm lthy rtrm qtrm = |
98 fun regularize_trm lthy rtrm qtrm = |
122 | (* equalities need to be replaced by appropriate equivalence relations *) |
124 | (* equalities need to be replaced by appropriate equivalence relations *) |
123 (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => |
125 (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => |
124 if ty = ty' then rtrm |
126 if ty = ty' then rtrm |
125 else mk_resp_arg lthy (domain_type ty, domain_type ty') |
127 else mk_resp_arg lthy (domain_type ty, domain_type ty') |
126 |
128 |
127 | (* in this case we check whether the given equivalence relation is correct *) |
129 | (* in this case we just check whether the given equivalence relation is correct *) |
128 (rel, Const (@{const_name "op ="}, ty')) => |
130 (rel, Const (@{const_name "op ="}, ty')) => |
129 let |
131 let |
130 val exc = LIFT_MATCH "regularise (relation mismatch)" |
132 val exc = LIFT_MATCH "regularise (relation mismatch)" |
131 val rel_ty = (fastype_of rel) handle TERM _ => raise exc |
133 val rel_ty = (fastype_of rel) handle TERM _ => raise exc |
132 val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') |
134 val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') |
133 in |
135 in |
134 if rel' = rel then rtrm else raise exc |
136 if rel' aconv rel then rtrm else raise exc |
135 end |
137 end |
136 |
138 |
137 | (_, Const _) => |
139 | (_, Const _) => |
138 let |
140 let |
139 fun same_name (Const (s, T)) (Const (s', T')) = (s = s') (*andalso (T = T')*) |
141 fun same_name (Const (s, T)) (Const (s', T')) = (s = s') (*andalso (T = T')*) |
166 end |
168 end |
167 |
169 |
168 | (t1 $ t2, t1' $ t2') => |
170 | (t1 $ t2, t1' $ t2') => |
169 (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2') |
171 (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2') |
170 |
172 |
171 | (Free (x, ty), Free (x', ty')) => |
|
172 (* this case cannot arrise as we start with two fully atomized terms *) |
|
173 raise (LIFT_MATCH "regularize (frees)") |
|
174 |
|
175 | (Bound i, Bound i') => |
173 | (Bound i, Bound i') => |
176 if i = i' then rtrm |
174 if i = i' then rtrm |
177 else raise (LIFT_MATCH "regularize (bounds mismatch)") |
175 else raise (LIFT_MATCH "regularize (bounds mismatch)") |
178 |
176 |
179 | _ => |
177 | _ => |
185 end |
183 end |
186 |
184 |
187 |
185 |
188 |
186 |
189 (* |
187 (* |
190 Injecting of Rep/Abs means: |
188 Injection of Rep/Abs means: |
191 |
189 |
192 For abstractions |
190 For abstractions |
193 : |
191 : |
194 * If the type of the abstraction doesn't need lifting we recurse. |
192 * If the type of the abstraction needs lifting, then we add Rep/Abs |
195 |
193 around the abstraction; otherwise we leave it unchanged. |
196 * If it needs lifting then we add Rep/Abs around the whole term and |
194 |
197 check if the bound variable needs lifting. |
|
198 |
|
199 * If it does we recurse and put Rep/Abs around all occurences |
|
200 of the variable in the obtained subterm. This in combination |
|
201 with the Rep/Abs from above will let us change the type of |
|
202 the abstraction with rewriting. |
|
203 |
|
204 For applications: |
195 For applications: |
205 |
196 |
206 * If the term is Respects applied to anything we leave it unchanged |
197 * If the application involves a bounded quantifier, we recurse on |
207 |
198 the second argument. If the application is a bounded abstraction, |
208 * If the term needs lifting and the head is a constant that we know |
199 we always put an Re/Abs around it (since bounded abstractions |
209 how to lift, we put a Rep/Abs and recurse |
200 always need lifting). Otherwise we recurse on both arguments. |
210 |
201 |
211 * If the term needs lifting and the head is a Free applied to subterms |
202 For constants: |
212 (if it is not applied we treated it in Abs branch) then we |
203 |
213 put Rep/Abs and recurse |
204 * If the constant is (op =), we leave it always unchanged. |
214 |
205 Otherwise the type of the constant needs lifting, we put |
215 * Otherwise just recurse. |
206 and Rep/Abs around it. |
|
207 |
|
208 For free variables: |
|
209 |
|
210 * We put aRep/Abs around it if the type needs lifting. |
|
211 |
|
212 Vars case cannot occur. |
216 *) |
213 *) |
217 |
214 |
218 fun mk_repabs lthy (T, T') trm = |
215 fun mk_repabs lthy (T, T') trm = |
219 Quotient_Def.get_fun repF lthy (T, T') |
216 Quotient_Def.get_fun repF lthy (T, T') |
220 $ (Quotient_Def.get_fun absF lthy (T, T') $ trm) |
217 $ (Quotient_Def.get_fun absF lthy (T, T') $ trm) |