|
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 |
|
8 signature QUOTIENT_TERM = |
|
9 sig |
|
10 exception LIFT_MATCH of string |
|
11 |
|
12 datatype flag = AbsF | RepF |
|
13 |
|
14 val absrep_fun: flag -> Proof.context -> typ * typ -> term |
|
15 val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term |
|
16 |
|
17 (* Allows Nitpick to represent quotient types as single elements from raw type *) |
|
18 val absrep_const_chk: flag -> Proof.context -> string -> term |
|
19 |
|
20 val equiv_relation: Proof.context -> typ * typ -> term |
|
21 val equiv_relation_chk: Proof.context -> typ * typ -> term |
|
22 |
|
23 val regularize_trm: Proof.context -> term * term -> term |
|
24 val regularize_trm_chk: Proof.context -> term * term -> term |
|
25 |
|
26 val inj_repabs_trm: Proof.context -> term * term -> term |
|
27 val inj_repabs_trm_chk: Proof.context -> term * term -> term |
|
28 |
|
29 val quotient_lift_const: string * term -> local_theory -> term |
|
30 val quotient_lift_all: Proof.context -> term -> term |
|
31 end; |
|
32 |
|
33 structure Quotient_Term: QUOTIENT_TERM = |
|
34 struct |
|
35 |
|
36 open Quotient_Info; |
|
37 |
|
38 exception LIFT_MATCH of string |
|
39 |
|
40 |
|
41 |
|
42 (*** Aggregate Rep/Abs Function ***) |
|
43 |
|
44 |
|
45 (* The flag RepF is for types in negative position; AbsF is for types |
|
46 in positive position. Because of this, function types need to be |
|
47 treated specially, since there the polarity changes. |
|
48 *) |
|
49 |
|
50 datatype flag = AbsF | RepF |
|
51 |
|
52 fun negF AbsF = RepF |
|
53 | negF RepF = AbsF |
|
54 |
|
55 fun is_identity (Const (@{const_name "id"}, _)) = true |
|
56 | is_identity _ = false |
|
57 |
|
58 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) |
|
59 |
|
60 fun mk_fun_compose flag (trm1, trm2) = |
|
61 case flag of |
|
62 AbsF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2 |
|
63 | RepF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 |
|
64 |
|
65 fun get_mapfun ctxt s = |
|
66 let |
|
67 val thy = ProofContext.theory_of ctxt |
|
68 val exn = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.") |
|
69 val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn |
|
70 in |
|
71 Const (mapfun, dummyT) |
|
72 end |
|
73 |
|
74 (* makes a Free out of a TVar *) |
|
75 fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT) |
|
76 |
|
77 (* produces an aggregate map function for the |
|
78 rty-part of a quotient definition; abstracts |
|
79 over all variables listed in vs (these variables |
|
80 correspond to the type variables in rty) |
|
81 |
|
82 for example for: (?'a list * ?'b) |
|
83 it produces: %a b. prod_map (map a) b |
|
84 *) |
|
85 fun mk_mapfun ctxt vs rty = |
|
86 let |
|
87 val vs' = map (mk_Free) vs |
|
88 |
|
89 fun mk_mapfun_aux rty = |
|
90 case rty of |
|
91 TVar _ => mk_Free rty |
|
92 | Type (_, []) => mk_identity rty |
|
93 | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys) |
|
94 | _ => raise LIFT_MATCH "mk_mapfun (default)" |
|
95 in |
|
96 fold_rev Term.lambda vs' (mk_mapfun_aux rty) |
|
97 end |
|
98 |
|
99 (* looks up the (varified) rty and qty for |
|
100 a quotient definition |
|
101 *) |
|
102 fun get_rty_qty ctxt s = |
|
103 let |
|
104 val thy = ProofContext.theory_of ctxt |
|
105 val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.") |
|
106 val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn |
|
107 in |
|
108 (#rtyp qdata, #qtyp qdata) |
|
109 end |
|
110 |
|
111 (* takes two type-environments and looks |
|
112 up in both of them the variable v, which |
|
113 must be listed in the environment |
|
114 *) |
|
115 fun double_lookup rtyenv qtyenv v = |
|
116 let |
|
117 val v' = fst (dest_TVar v) |
|
118 in |
|
119 (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v'))) |
|
120 end |
|
121 |
|
122 (* matches a type pattern with a type *) |
|
123 fun match ctxt err ty_pat ty = |
|
124 let |
|
125 val thy = ProofContext.theory_of ctxt |
|
126 in |
|
127 Sign.typ_match thy (ty_pat, ty) Vartab.empty |
|
128 handle MATCH_TYPE => err ctxt ty_pat ty |
|
129 end |
|
130 |
|
131 (* produces the rep or abs constant for a qty *) |
|
132 fun absrep_const flag ctxt qty_str = |
|
133 let |
|
134 val thy = ProofContext.theory_of ctxt |
|
135 val qty_name = Long_Name.base_name qty_str |
|
136 in |
|
137 case flag of |
|
138 AbsF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT) |
|
139 | RepF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT) |
|
140 end |
|
141 |
|
142 (* Lets Nitpick represent elements of quotient types as elements of the raw type *) |
|
143 fun absrep_const_chk flag ctxt qty_str = |
|
144 Syntax.check_term ctxt (absrep_const flag ctxt qty_str) |
|
145 |
|
146 fun absrep_match_err ctxt ty_pat ty = |
|
147 let |
|
148 val ty_pat_str = Syntax.string_of_typ ctxt ty_pat |
|
149 val ty_str = Syntax.string_of_typ ctxt ty |
|
150 in |
|
151 raise LIFT_MATCH (space_implode " " |
|
152 ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) |
|
153 end |
|
154 |
|
155 |
|
156 (** generation of an aggregate absrep function **) |
|
157 |
|
158 (* - In case of equal types we just return the identity. |
|
159 |
|
160 - In case of TFrees we also return the identity. |
|
161 |
|
162 - In case of function types we recurse taking |
|
163 the polarity change into account. |
|
164 |
|
165 - If the type constructors are equal, we recurse for the |
|
166 arguments and build the appropriate map function. |
|
167 |
|
168 - If the type constructors are unequal, there must be an |
|
169 instance of quotient types: |
|
170 |
|
171 - we first look up the corresponding rty_pat and qty_pat |
|
172 from the quotient definition; the arguments of qty_pat |
|
173 must be some distinct TVars |
|
174 - we then match the rty_pat with rty and qty_pat with qty; |
|
175 if matching fails the types do not correspond -> error |
|
176 - the matching produces two environments; we look up the |
|
177 assignments for the qty_pat variables and recurse on the |
|
178 assignments |
|
179 - we prefix the aggregate map function for the rty_pat, |
|
180 which is an abstraction over all type variables |
|
181 - finally we compose the result with the appropriate |
|
182 absrep function in case at least one argument produced |
|
183 a non-identity function / |
|
184 otherwise we just return the appropriate absrep |
|
185 function |
|
186 |
|
187 The composition is necessary for types like |
|
188 |
|
189 ('a list) list / ('a foo) foo |
|
190 |
|
191 The matching is necessary for types like |
|
192 |
|
193 ('a * 'a) list / 'a bar |
|
194 |
|
195 The test is necessary in order to eliminate superfluous |
|
196 identity maps. |
|
197 *) |
|
198 |
|
199 fun absrep_fun flag ctxt (rty, qty) = |
|
200 if rty = qty |
|
201 then mk_identity rty |
|
202 else |
|
203 case (rty, qty) of |
|
204 (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) => |
|
205 let |
|
206 val arg1 = absrep_fun (negF flag) ctxt (ty1, ty1') |
|
207 val arg2 = absrep_fun flag ctxt (ty2, ty2') |
|
208 in |
|
209 list_comb (get_mapfun ctxt "fun", [arg1, arg2]) |
|
210 end |
|
211 | (Type (s, tys), Type (s', tys')) => |
|
212 if s = s' |
|
213 then |
|
214 let |
|
215 val args = map (absrep_fun flag ctxt) (tys ~~ tys') |
|
216 in |
|
217 list_comb (get_mapfun ctxt s, args) |
|
218 end |
|
219 else |
|
220 let |
|
221 val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s' |
|
222 val rtyenv = match ctxt absrep_match_err rty_pat rty |
|
223 val qtyenv = match ctxt absrep_match_err qty_pat qty |
|
224 val args_aux = map (double_lookup rtyenv qtyenv) vs |
|
225 val args = map (absrep_fun flag ctxt) args_aux |
|
226 val map_fun = mk_mapfun ctxt vs rty_pat |
|
227 val result = list_comb (map_fun, args) |
|
228 in |
|
229 if forall is_identity args |
|
230 then absrep_const flag ctxt s' |
|
231 else mk_fun_compose flag (absrep_const flag ctxt s', result) |
|
232 end |
|
233 | (TFree x, TFree x') => |
|
234 if x = x' |
|
235 then mk_identity rty |
|
236 else raise (LIFT_MATCH "absrep_fun (frees)") |
|
237 | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)") |
|
238 | _ => raise (LIFT_MATCH "absrep_fun (default)") |
|
239 |
|
240 fun absrep_fun_chk flag ctxt (rty, qty) = |
|
241 absrep_fun flag ctxt (rty, qty) |
|
242 |> Syntax.check_term ctxt |
|
243 |
|
244 |
|
245 |
|
246 |
|
247 (*** Aggregate Equivalence Relation ***) |
|
248 |
|
249 |
|
250 (* works very similar to the absrep generation, |
|
251 except there is no need for polarities |
|
252 *) |
|
253 |
|
254 (* instantiates TVars so that the term is of type ty *) |
|
255 fun force_typ ctxt trm ty = |
|
256 let |
|
257 val thy = ProofContext.theory_of ctxt |
|
258 val trm_ty = fastype_of trm |
|
259 val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty |
|
260 in |
|
261 map_types (Envir.subst_type ty_inst) trm |
|
262 end |
|
263 |
|
264 fun is_eq (Const (@{const_name "op ="}, _)) = true |
|
265 | is_eq _ = false |
|
266 |
|
267 fun mk_rel_compose (trm1, trm2) = |
|
268 Const (@{const_name "rel_conj"}, dummyT) $ trm1 $ trm2 |
|
269 |
|
270 fun get_relmap ctxt s = |
|
271 let |
|
272 val thy = ProofContext.theory_of ctxt |
|
273 val exn = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")") |
|
274 val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn |
|
275 in |
|
276 Const (relmap, dummyT) |
|
277 end |
|
278 |
|
279 fun mk_relmap ctxt vs rty = |
|
280 let |
|
281 val vs' = map (mk_Free) vs |
|
282 |
|
283 fun mk_relmap_aux rty = |
|
284 case rty of |
|
285 TVar _ => mk_Free rty |
|
286 | Type (_, []) => HOLogic.eq_const rty |
|
287 | Type (s, tys) => list_comb (get_relmap ctxt s, map mk_relmap_aux tys) |
|
288 | _ => raise LIFT_MATCH ("mk_relmap (default)") |
|
289 in |
|
290 fold_rev Term.lambda vs' (mk_relmap_aux rty) |
|
291 end |
|
292 |
|
293 fun get_equiv_rel ctxt s = |
|
294 let |
|
295 val thy = ProofContext.theory_of ctxt |
|
296 val exn = LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")") |
|
297 in |
|
298 #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn |
|
299 end |
|
300 |
|
301 fun equiv_match_err ctxt ty_pat ty = |
|
302 let |
|
303 val ty_pat_str = Syntax.string_of_typ ctxt ty_pat |
|
304 val ty_str = Syntax.string_of_typ ctxt ty |
|
305 in |
|
306 raise LIFT_MATCH (space_implode " " |
|
307 ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) |
|
308 end |
|
309 |
|
310 (* builds the aggregate equivalence relation |
|
311 that will be the argument of Respects |
|
312 *) |
|
313 fun equiv_relation ctxt (rty, qty) = |
|
314 if rty = qty |
|
315 then HOLogic.eq_const rty |
|
316 else |
|
317 case (rty, qty) of |
|
318 (Type (s, tys), Type (s', tys')) => |
|
319 if s = s' |
|
320 then |
|
321 let |
|
322 val args = map (equiv_relation ctxt) (tys ~~ tys') |
|
323 in |
|
324 list_comb (get_relmap ctxt s, args) |
|
325 end |
|
326 else |
|
327 let |
|
328 val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s' |
|
329 val rtyenv = match ctxt equiv_match_err rty_pat rty |
|
330 val qtyenv = match ctxt equiv_match_err qty_pat qty |
|
331 val args_aux = map (double_lookup rtyenv qtyenv) vs |
|
332 val args = map (equiv_relation ctxt) args_aux |
|
333 val rel_map = mk_relmap ctxt vs rty_pat |
|
334 val result = list_comb (rel_map, args) |
|
335 val eqv_rel = get_equiv_rel ctxt s' |
|
336 val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool}) |
|
337 in |
|
338 if forall is_eq args |
|
339 then eqv_rel' |
|
340 else mk_rel_compose (result, eqv_rel') |
|
341 end |
|
342 | _ => HOLogic.eq_const rty |
|
343 |
|
344 fun equiv_relation_chk ctxt (rty, qty) = |
|
345 equiv_relation ctxt (rty, qty) |
|
346 |> Syntax.check_term ctxt |
|
347 |
|
348 |
|
349 |
|
350 (*** Regularization ***) |
|
351 |
|
352 (* Regularizing an rtrm means: |
|
353 |
|
354 - Quantifiers over types that need lifting are replaced |
|
355 by bounded quantifiers, for example: |
|
356 |
|
357 All P ----> All (Respects R) P |
|
358 |
|
359 where the aggregate relation R is given by the rty and qty; |
|
360 |
|
361 - Abstractions over types that need lifting are replaced |
|
362 by bounded abstractions, for example: |
|
363 |
|
364 %x. P ----> Ball (Respects R) %x. P |
|
365 |
|
366 - Equalities over types that need lifting are replaced by |
|
367 corresponding equivalence relations, for example: |
|
368 |
|
369 A = B ----> R A B |
|
370 |
|
371 or |
|
372 |
|
373 A = B ----> (R ===> R) A B |
|
374 |
|
375 for more complicated types of A and B |
|
376 |
|
377 |
|
378 The regularize_trm accepts raw theorems in which equalities |
|
379 and quantifiers match exactly the ones in the lifted theorem |
|
380 but also accepts partially regularized terms. |
|
381 |
|
382 This means that the raw theorems can have: |
|
383 Ball (Respects R), Bex (Respects R), Bex1_rel (Respects R), Babs, R |
|
384 in the places where: |
|
385 All, Ex, Ex1, %, (op =) |
|
386 is required the lifted theorem. |
|
387 |
|
388 *) |
|
389 |
|
390 val mk_babs = Const (@{const_name Babs}, dummyT) |
|
391 val mk_ball = Const (@{const_name Ball}, dummyT) |
|
392 val mk_bex = Const (@{const_name Bex}, dummyT) |
|
393 val mk_bex1_rel = Const (@{const_name Bex1_rel}, dummyT) |
|
394 val mk_resp = Const (@{const_name Respects}, dummyT) |
|
395 |
|
396 (* - applies f to the subterm of an abstraction, |
|
397 otherwise to the given term, |
|
398 - used by regularize, therefore abstracted |
|
399 variables do not have to be treated specially |
|
400 *) |
|
401 fun apply_subt f (trm1, trm2) = |
|
402 case (trm1, trm2) of |
|
403 (Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f (t, t')) |
|
404 | _ => f (trm1, trm2) |
|
405 |
|
406 fun term_mismatch str ctxt t1 t2 = |
|
407 let |
|
408 val t1_str = Syntax.string_of_term ctxt t1 |
|
409 val t2_str = Syntax.string_of_term ctxt t2 |
|
410 val t1_ty_str = Syntax.string_of_typ ctxt (fastype_of t1) |
|
411 val t2_ty_str = Syntax.string_of_typ ctxt (fastype_of t2) |
|
412 in |
|
413 raise LIFT_MATCH (cat_lines [str, t1_str ^ "::" ^ t1_ty_str, t2_str ^ "::" ^ t2_ty_str]) |
|
414 end |
|
415 |
|
416 (* the major type of All and Ex quantifiers *) |
|
417 fun qnt_typ ty = domain_type (domain_type ty) |
|
418 |
|
419 (* Checks that two types match, for example: |
|
420 rty -> rty matches qty -> qty *) |
|
421 fun matches_typ thy rT qT = |
|
422 if rT = qT then true else |
|
423 case (rT, qT) of |
|
424 (Type (rs, rtys), Type (qs, qtys)) => |
|
425 if rs = qs then |
|
426 if length rtys <> length qtys then false else |
|
427 forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys) |
|
428 else |
|
429 (case Quotient_Info.quotdata_lookup_raw thy qs of |
|
430 SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo) |
|
431 | NONE => false) |
|
432 | _ => false |
|
433 |
|
434 |
|
435 (* produces a regularized version of rtrm |
|
436 |
|
437 - the result might contain dummyTs |
|
438 |
|
439 - for regularisation we do not need any |
|
440 special treatment of bound variables |
|
441 *) |
|
442 fun regularize_trm ctxt (rtrm, qtrm) = |
|
443 case (rtrm, qtrm) of |
|
444 (Abs (x, ty, t), Abs (_, ty', t')) => |
|
445 let |
|
446 val subtrm = Abs(x, ty, regularize_trm ctxt (t, t')) |
|
447 in |
|
448 if ty = ty' then subtrm |
|
449 else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm |
|
450 end |
|
451 | (Const (@{const_name "Babs"}, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) => |
|
452 let |
|
453 val subtrm = regularize_trm ctxt (t, t') |
|
454 val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty') |
|
455 in |
|
456 if resrel <> needres |
|
457 then term_mismatch "regularize (Babs)" ctxt resrel needres |
|
458 else mk_babs $ resrel $ subtrm |
|
459 end |
|
460 |
|
461 | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => |
|
462 let |
|
463 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
464 in |
|
465 if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm |
|
466 else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
|
467 end |
|
468 |
|
469 | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
|
470 let |
|
471 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
472 in |
|
473 if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm |
|
474 else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
|
475 end |
|
476 |
|
477 | (Const (@{const_name "Ex1"}, ty) $ (Abs (_, _, |
|
478 (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op :"}, _) $ _ $ |
|
479 (Const (@{const_name "Respects"}, _) $ resrel)) $ (t $ _)))), |
|
480 Const (@{const_name "Ex1"}, ty') $ t') => |
|
481 let |
|
482 val t_ = incr_boundvars (~1) t |
|
483 val subtrm = apply_subt (regularize_trm ctxt) (t_, t') |
|
484 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
|
485 in |
|
486 if resrel <> needrel |
|
487 then term_mismatch "regularize (Bex1)" ctxt resrel needrel |
|
488 else mk_bex1_rel $ resrel $ subtrm |
|
489 end |
|
490 |
|
491 | (Const (@{const_name "Ex1"}, ty) $ t, Const (@{const_name "Ex1"}, ty') $ t') => |
|
492 let |
|
493 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
494 in |
|
495 if ty = ty' then Const (@{const_name "Ex1"}, ty) $ subtrm |
|
496 else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
|
497 end |
|
498 |
|
499 | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, |
|
500 Const (@{const_name "All"}, ty') $ t') => |
|
501 let |
|
502 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
503 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
|
504 in |
|
505 if resrel <> needrel |
|
506 then term_mismatch "regularize (Ball)" ctxt resrel needrel |
|
507 else mk_ball $ (mk_resp $ resrel) $ subtrm |
|
508 end |
|
509 |
|
510 | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, |
|
511 Const (@{const_name "Ex"}, ty') $ t') => |
|
512 let |
|
513 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
514 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
|
515 in |
|
516 if resrel <> needrel |
|
517 then term_mismatch "regularize (Bex)" ctxt resrel needrel |
|
518 else mk_bex $ (mk_resp $ resrel) $ subtrm |
|
519 end |
|
520 |
|
521 | (Const (@{const_name "Bex1_rel"}, ty) $ resrel $ t, Const (@{const_name "Ex1"}, ty') $ t') => |
|
522 let |
|
523 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
524 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
|
525 in |
|
526 if resrel <> needrel |
|
527 then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel |
|
528 else mk_bex1_rel $ resrel $ subtrm |
|
529 end |
|
530 |
|
531 | (* equalities need to be replaced by appropriate equivalence relations *) |
|
532 (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => |
|
533 if ty = ty' then rtrm |
|
534 else equiv_relation ctxt (domain_type ty, domain_type ty') |
|
535 |
|
536 | (* in this case we just check whether the given equivalence relation is correct *) |
|
537 (rel, Const (@{const_name "op ="}, ty')) => |
|
538 let |
|
539 val rel_ty = fastype_of rel |
|
540 val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty') |
|
541 in |
|
542 if rel' aconv rel then rtrm |
|
543 else term_mismatch "regularise (relation mismatch)" ctxt rel rel' |
|
544 end |
|
545 |
|
546 | (_, Const _) => |
|
547 let |
|
548 val thy = ProofContext.theory_of ctxt |
|
549 fun same_const (Const (s, T)) (Const (s', T')) = (s = s') andalso matches_typ thy T T' |
|
550 | same_const _ _ = false |
|
551 in |
|
552 if same_const rtrm qtrm then rtrm |
|
553 else |
|
554 let |
|
555 val rtrm' = #rconst (qconsts_lookup thy qtrm) |
|
556 handle Quotient_Info.NotFound => term_mismatch "regularize(constant notfound)" ctxt rtrm qtrm |
|
557 in |
|
558 if Pattern.matches thy (rtrm', rtrm) |
|
559 then rtrm else term_mismatch "regularize(constant mismatch)" ctxt rtrm qtrm |
|
560 end |
|
561 end |
|
562 |
|
563 | (((t1 as Const (@{const_name "split"}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))), |
|
564 ((t2 as Const (@{const_name "split"}, _)) $ Abs (v2, _ , Abs(v2', _ , s2)))) => |
|
565 regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2))) |
|
566 |
|
567 | (((t1 as Const (@{const_name "split"}, _)) $ Abs (v1, ty, s1)), |
|
568 ((t2 as Const (@{const_name "split"}, _)) $ Abs (v2, _ , s2))) => |
|
569 regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2)) |
|
570 |
|
571 | (t1 $ t2, t1' $ t2') => |
|
572 regularize_trm ctxt (t1, t1') $ regularize_trm ctxt (t2, t2') |
|
573 |
|
574 | (Bound i, Bound i') => |
|
575 if i = i' then rtrm |
|
576 else raise (LIFT_MATCH "regularize (bounds mismatch)") |
|
577 |
|
578 | _ => |
|
579 let |
|
580 val rtrm_str = Syntax.string_of_term ctxt rtrm |
|
581 val qtrm_str = Syntax.string_of_term ctxt qtrm |
|
582 in |
|
583 raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")")) |
|
584 end |
|
585 |
|
586 fun regularize_trm_chk ctxt (rtrm, qtrm) = |
|
587 regularize_trm ctxt (rtrm, qtrm) |
|
588 |> Syntax.check_term ctxt |
|
589 |
|
590 |
|
591 |
|
592 (*** Rep/Abs Injection ***) |
|
593 |
|
594 (* |
|
595 Injection of Rep/Abs means: |
|
596 |
|
597 For abstractions: |
|
598 |
|
599 * If the type of the abstraction needs lifting, then we add Rep/Abs |
|
600 around the abstraction; otherwise we leave it unchanged. |
|
601 |
|
602 For applications: |
|
603 |
|
604 * If the application involves a bounded quantifier, we recurse on |
|
605 the second argument. If the application is a bounded abstraction, |
|
606 we always put an Rep/Abs around it (since bounded abstractions |
|
607 are assumed to always need lifting). Otherwise we recurse on both |
|
608 arguments. |
|
609 |
|
610 For constants: |
|
611 |
|
612 * If the constant is (op =), we leave it always unchanged. |
|
613 Otherwise the type of the constant needs lifting, we put |
|
614 and Rep/Abs around it. |
|
615 |
|
616 For free variables: |
|
617 |
|
618 * We put a Rep/Abs around it if the type needs lifting. |
|
619 |
|
620 Vars case cannot occur. |
|
621 *) |
|
622 |
|
623 fun mk_repabs ctxt (T, T') trm = |
|
624 absrep_fun RepF ctxt (T, T') $ (absrep_fun AbsF ctxt (T, T') $ trm) |
|
625 |
|
626 fun inj_repabs_err ctxt msg rtrm qtrm = |
|
627 let |
|
628 val rtrm_str = Syntax.string_of_term ctxt rtrm |
|
629 val qtrm_str = Syntax.string_of_term ctxt qtrm |
|
630 in |
|
631 raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str]) |
|
632 end |
|
633 |
|
634 |
|
635 (* bound variables need to be treated properly, |
|
636 as the type of subterms needs to be calculated *) |
|
637 fun inj_repabs_trm ctxt (rtrm, qtrm) = |
|
638 case (rtrm, qtrm) of |
|
639 (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') => |
|
640 Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm ctxt (t, t')) |
|
641 |
|
642 | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') => |
|
643 Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm ctxt (t, t')) |
|
644 |
|
645 | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) => |
|
646 let |
|
647 val rty = fastype_of rtrm |
|
648 val qty = fastype_of qtrm |
|
649 in |
|
650 mk_repabs ctxt (rty, qty) (Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))) |
|
651 end |
|
652 |
|
653 | (Abs (x, T, t), Abs (x', T', t')) => |
|
654 let |
|
655 val rty = fastype_of rtrm |
|
656 val qty = fastype_of qtrm |
|
657 val (y, s) = Term.dest_abs (x, T, t) |
|
658 val (_, s') = Term.dest_abs (x', T', t') |
|
659 val yvar = Free (y, T) |
|
660 val result = Term.lambda_name (y, yvar) (inj_repabs_trm ctxt (s, s')) |
|
661 in |
|
662 if rty = qty then result |
|
663 else mk_repabs ctxt (rty, qty) result |
|
664 end |
|
665 |
|
666 | (t $ s, t' $ s') => |
|
667 (inj_repabs_trm ctxt (t, t')) $ (inj_repabs_trm ctxt (s, s')) |
|
668 |
|
669 | (Free (_, T), Free (_, T')) => |
|
670 if T = T' then rtrm |
|
671 else mk_repabs ctxt (T, T') rtrm |
|
672 |
|
673 | (_, Const (@{const_name "op ="}, _)) => rtrm |
|
674 |
|
675 | (_, Const (_, T')) => |
|
676 let |
|
677 val rty = fastype_of rtrm |
|
678 in |
|
679 if rty = T' then rtrm |
|
680 else mk_repabs ctxt (rty, T') rtrm |
|
681 end |
|
682 |
|
683 | _ => inj_repabs_err ctxt "injection (default):" rtrm qtrm |
|
684 |
|
685 fun inj_repabs_trm_chk ctxt (rtrm, qtrm) = |
|
686 inj_repabs_trm ctxt (rtrm, qtrm) |
|
687 |> Syntax.check_term ctxt |
|
688 |
|
689 |
|
690 |
|
691 (*** Wrapper for automatically transforming an rthm into a qthm ***) |
|
692 |
|
693 (* subst_tys takes a list of (rty, qty) substitution pairs |
|
694 and replaces all occurences of rty in the given type |
|
695 by appropriate qty, with substitution *) |
|
696 fun subst_ty thy ty (rty, qty) r = |
|
697 if r <> NONE then r else |
|
698 case try (Sign.typ_match thy (rty, ty)) Vartab.empty of |
|
699 SOME inst => SOME (Envir.subst_type inst qty) |
|
700 | NONE => NONE |
|
701 fun subst_tys thy substs ty = |
|
702 case fold (subst_ty thy ty) substs NONE of |
|
703 SOME ty => ty |
|
704 | NONE => |
|
705 (case ty of |
|
706 Type (s, tys) => Type (s, map (subst_tys thy substs) tys) |
|
707 | x => x) |
|
708 |
|
709 (* subst_trms takes a list of (rtrm, qtrm) substitution pairs |
|
710 and if the given term matches any of the raw terms it |
|
711 returns the appropriate qtrm instantiated. If none of |
|
712 them matched it returns NONE. *) |
|
713 fun subst_trm thy t (rtrm, qtrm) s = |
|
714 if s <> NONE then s else |
|
715 case try (Pattern.match thy (rtrm, t)) (Vartab.empty, Vartab.empty) of |
|
716 SOME inst => SOME (Envir.subst_term inst qtrm) |
|
717 | NONE => NONE; |
|
718 fun subst_trms thy substs t = fold (subst_trm thy t) substs NONE |
|
719 |
|
720 (* prepares type and term substitution pairs to be used by above |
|
721 functions that let replace all raw constructs by appropriate |
|
722 lifted counterparts. *) |
|
723 fun get_ty_trm_substs ctxt = |
|
724 let |
|
725 val thy = ProofContext.theory_of ctxt |
|
726 val quot_infos = Quotient_Info.quotdata_dest ctxt |
|
727 val const_infos = Quotient_Info.qconsts_dest ctxt |
|
728 val ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos |
|
729 val const_substs = map (fn ci => (#rconst ci, #qconst ci)) const_infos |
|
730 fun rel_eq rel = HOLogic.eq_const (subst_tys thy ty_substs (domain_type (fastype_of rel))) |
|
731 val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos |
|
732 in |
|
733 (ty_substs, const_substs @ rel_substs) |
|
734 end |
|
735 |
|
736 fun quotient_lift_const (b, t) ctxt = |
|
737 let |
|
738 val thy = ProofContext.theory_of ctxt |
|
739 val (ty_substs, _) = get_ty_trm_substs ctxt; |
|
740 val (_, ty) = dest_Const t; |
|
741 val nty = subst_tys thy ty_substs ty; |
|
742 in |
|
743 Free(b, nty) |
|
744 end |
|
745 |
|
746 (* |
|
747 Takes a term and |
|
748 |
|
749 * replaces raw constants by the quotient constants |
|
750 |
|
751 * replaces equivalence relations by equalities |
|
752 |
|
753 * replaces raw types by the quotient types |
|
754 |
|
755 *) |
|
756 |
|
757 fun quotient_lift_all ctxt t = |
|
758 let |
|
759 val thy = ProofContext.theory_of ctxt |
|
760 val (ty_substs, substs) = get_ty_trm_substs ctxt |
|
761 fun lift_aux t = |
|
762 case subst_trms thy substs t of |
|
763 SOME x => x |
|
764 | NONE => |
|
765 (case t of |
|
766 a $ b => lift_aux a $ lift_aux b |
|
767 | Abs(a, ty, s) => |
|
768 let |
|
769 val (y, s') = Term.dest_abs (a, ty, s) |
|
770 val nty = subst_tys thy ty_substs ty |
|
771 in |
|
772 Abs(y, nty, abstract_over (Free (y, nty), lift_aux s')) |
|
773 end |
|
774 | Free(n, ty) => Free(n, subst_tys thy ty_substs ty) |
|
775 | Var(n, ty) => Var(n, subst_tys thy ty_substs ty) |
|
776 | Bound i => Bound i |
|
777 | Const(s, ty) => Const(s, subst_tys thy ty_substs ty)) |
|
778 in |
|
779 lift_aux t |
|
780 end |
|
781 |
|
782 |
|
783 end; (* structure *) |
|
784 |
|
785 |
|
786 |