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