5 quotient types. |
5 quotient types. |
6 *) |
6 *) |
7 |
7 |
8 signature QUOTIENT_TERM = |
8 signature QUOTIENT_TERM = |
9 sig |
9 sig |
10 exception LIFT_MATCH of string |
|
11 |
|
12 datatype flag = AbsF | RepF |
10 datatype flag = AbsF | RepF |
13 |
11 |
14 val absrep_fun: flag -> Proof.context -> typ * typ -> term |
12 val absrep_fun: flag -> Proof.context -> typ * typ -> term |
15 val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term |
13 val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term |
16 |
14 |
63 | RepF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 |
61 | RepF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 |
64 |
62 |
65 fun get_mapfun ctxt s = |
63 fun get_mapfun ctxt s = |
66 let |
64 let |
67 val thy = ProofContext.theory_of ctxt |
65 val thy = ProofContext.theory_of ctxt |
68 val exn = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.") |
66 val exn = error ("No map function for type " ^ quote s ^ " found.") |
69 val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn |
67 val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn |
70 in |
68 in |
71 Const (mapfun, dummyT) |
69 Const (mapfun, dummyT) |
72 end |
70 end |
73 |
71 |
89 fun mk_mapfun_aux rty = |
87 fun mk_mapfun_aux rty = |
90 case rty of |
88 case rty of |
91 TVar _ => mk_Free rty |
89 TVar _ => mk_Free rty |
92 | Type (_, []) => mk_identity rty |
90 | Type (_, []) => mk_identity rty |
93 | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys) |
91 | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys) |
94 | _ => raise LIFT_MATCH "mk_mapfun (default)" |
92 | _ => raise (error "mk_mapfun (default)") |
95 in |
93 in |
96 fold_rev Term.lambda vs' (mk_mapfun_aux rty) |
94 fold_rev Term.lambda vs' (mk_mapfun_aux rty) |
97 end |
95 end |
98 |
96 |
99 (* looks up the (varified) rty and qty for |
97 (* looks up the (varified) rty and qty for |
100 a quotient definition |
98 a quotient definition |
101 *) |
99 *) |
102 fun get_rty_qty ctxt s = |
100 fun get_rty_qty ctxt s = |
103 let |
101 let |
104 val thy = ProofContext.theory_of ctxt |
102 val thy = ProofContext.theory_of ctxt |
105 val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.") |
103 val exn = error ("No quotient type " ^ quote s ^ " found.") |
106 val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn |
104 val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn |
107 in |
105 in |
108 (#rtyp qdata, #qtyp qdata) |
106 (#rtyp qdata, #qtyp qdata) |
109 end |
107 end |
110 |
108 |
146 fun absrep_match_err ctxt ty_pat ty = |
144 fun absrep_match_err ctxt ty_pat ty = |
147 let |
145 let |
148 val ty_pat_str = Syntax.string_of_typ ctxt ty_pat |
146 val ty_pat_str = Syntax.string_of_typ ctxt ty_pat |
149 val ty_str = Syntax.string_of_typ ctxt ty |
147 val ty_str = Syntax.string_of_typ ctxt ty |
150 in |
148 in |
151 raise LIFT_MATCH (space_implode " " |
149 raise error (cat_lines |
152 ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) |
150 ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) |
153 end |
151 end |
154 |
152 |
155 |
153 |
156 (** generation of an aggregate absrep function **) |
154 (** generation of an aggregate absrep function **) |
231 else mk_fun_compose flag (absrep_const flag ctxt s', result) |
229 else mk_fun_compose flag (absrep_const flag ctxt s', result) |
232 end |
230 end |
233 | (TFree x, TFree x') => |
231 | (TFree x, TFree x') => |
234 if x = x' |
232 if x = x' |
235 then mk_identity rty |
233 then mk_identity rty |
236 else raise (LIFT_MATCH "absrep_fun (frees)") |
234 else raise (error "absrep_fun (frees)") |
237 | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)") |
235 | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)") |
238 | _ => raise (LIFT_MATCH "absrep_fun (default)") |
236 | _ => raise (error "absrep_fun (default)") |
239 |
237 |
240 fun absrep_fun_chk flag ctxt (rty, qty) = |
238 fun absrep_fun_chk flag ctxt (rty, qty) = |
241 absrep_fun flag ctxt (rty, qty) |
239 absrep_fun flag ctxt (rty, qty) |
242 |> Syntax.check_term ctxt |
240 |> Syntax.check_term ctxt |
243 |
241 |
268 Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2 |
266 Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2 |
269 |
267 |
270 fun get_relmap ctxt s = |
268 fun get_relmap ctxt s = |
271 let |
269 let |
272 val thy = ProofContext.theory_of ctxt |
270 val thy = ProofContext.theory_of ctxt |
273 val exn = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")") |
271 val exn = error ("get_relmap (no relation map function found for type " ^ s ^ ")") |
274 val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn |
272 val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn |
275 in |
273 in |
276 Const (relmap, dummyT) |
274 Const (relmap, dummyT) |
277 end |
275 end |
278 |
276 |
283 fun mk_relmap_aux rty = |
281 fun mk_relmap_aux rty = |
284 case rty of |
282 case rty of |
285 TVar _ => mk_Free rty |
283 TVar _ => mk_Free rty |
286 | Type (_, []) => HOLogic.eq_const rty |
284 | Type (_, []) => HOLogic.eq_const rty |
287 | Type (s, tys) => list_comb (get_relmap ctxt s, map mk_relmap_aux tys) |
285 | Type (s, tys) => list_comb (get_relmap ctxt s, map mk_relmap_aux tys) |
288 | _ => raise LIFT_MATCH ("mk_relmap (default)") |
286 | _ => raise (error "mk_relmap (default)") |
289 in |
287 in |
290 fold_rev Term.lambda vs' (mk_relmap_aux rty) |
288 fold_rev Term.lambda vs' (mk_relmap_aux rty) |
291 end |
289 end |
292 |
290 |
293 fun get_equiv_rel ctxt s = |
291 fun get_equiv_rel ctxt s = |
294 let |
292 let |
295 val thy = ProofContext.theory_of ctxt |
293 val thy = ProofContext.theory_of ctxt |
296 val exn = LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")") |
294 val exn = error ("get_quotdata (no quotient found for type " ^ s ^ ")") |
297 in |
295 in |
298 #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn |
296 #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn |
299 end |
297 end |
300 |
298 |
301 fun equiv_match_err ctxt ty_pat ty = |
299 fun equiv_match_err ctxt ty_pat ty = |
302 let |
300 let |
303 val ty_pat_str = Syntax.string_of_typ ctxt ty_pat |
301 val ty_pat_str = Syntax.string_of_typ ctxt ty_pat |
304 val ty_str = Syntax.string_of_typ ctxt ty |
302 val ty_str = Syntax.string_of_typ ctxt ty |
305 in |
303 in |
306 raise LIFT_MATCH (space_implode " " |
304 raise error (space_implode " " |
307 ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) |
305 ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) |
308 end |
306 end |
309 |
307 |
310 (* builds the aggregate equivalence relation |
308 (* builds the aggregate equivalence relation |
311 that will be the argument of Respects |
309 that will be the argument of Respects |
408 val t1_str = Syntax.string_of_term ctxt t1 |
406 val t1_str = Syntax.string_of_term ctxt t1 |
409 val t2_str = Syntax.string_of_term ctxt t2 |
407 val t2_str = Syntax.string_of_term ctxt t2 |
410 val t1_ty_str = Syntax.string_of_typ ctxt (fastype_of t1) |
408 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) |
409 val t2_ty_str = Syntax.string_of_typ ctxt (fastype_of t2) |
412 in |
410 in |
413 raise LIFT_MATCH (cat_lines [str, t1_str ^ "::" ^ t1_ty_str, t2_str ^ "::" ^ t2_ty_str]) |
411 raise error (cat_lines [str, t1_str ^ "::" ^ t1_ty_str, t2_str ^ "::" ^ t2_ty_str]) |
414 end |
412 end |
415 |
413 |
416 (* the major type of All and Ex quantifiers *) |
414 (* the major type of All and Ex quantifiers *) |
417 fun qnt_typ ty = domain_type (domain_type ty) |
415 fun qnt_typ ty = domain_type (domain_type ty) |
418 |
416 |
571 | (t1 $ t2, t1' $ t2') => |
569 | (t1 $ t2, t1' $ t2') => |
572 regularize_trm ctxt (t1, t1') $ regularize_trm ctxt (t2, t2') |
570 regularize_trm ctxt (t1, t1') $ regularize_trm ctxt (t2, t2') |
573 |
571 |
574 | (Bound i, Bound i') => |
572 | (Bound i, Bound i') => |
575 if i = i' then rtrm |
573 if i = i' then rtrm |
576 else raise (LIFT_MATCH "regularize (bounds mismatch)") |
574 else raise (error "regularize (bounds mismatch)") |
577 |
575 |
578 | _ => |
576 | _ => |
579 let |
577 let |
580 val rtrm_str = Syntax.string_of_term ctxt rtrm |
578 val rtrm_str = Syntax.string_of_term ctxt rtrm |
581 val qtrm_str = Syntax.string_of_term ctxt qtrm |
579 val qtrm_str = Syntax.string_of_term ctxt qtrm |
582 in |
580 in |
583 raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")")) |
581 raise (error ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")")) |
584 end |
582 end |
585 |
583 |
586 fun regularize_trm_chk ctxt (rtrm, qtrm) = |
584 fun regularize_trm_chk ctxt (rtrm, qtrm) = |
587 regularize_trm ctxt (rtrm, qtrm) |
585 regularize_trm ctxt (rtrm, qtrm) |
588 |> Syntax.check_term ctxt |
586 |> Syntax.check_term ctxt |
626 fun inj_repabs_err ctxt msg rtrm qtrm = |
624 fun inj_repabs_err ctxt msg rtrm qtrm = |
627 let |
625 let |
628 val rtrm_str = Syntax.string_of_term ctxt rtrm |
626 val rtrm_str = Syntax.string_of_term ctxt rtrm |
629 val qtrm_str = Syntax.string_of_term ctxt qtrm |
627 val qtrm_str = Syntax.string_of_term ctxt qtrm |
630 in |
628 in |
631 raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str]) |
629 raise error (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str]) |
632 end |
630 end |
633 |
631 |
634 |
632 |
635 (* bound variables need to be treated properly, |
633 (* bound variables need to be treated properly, |
636 as the type of subterms needs to be calculated *) |
634 as the type of subterms needs to be calculated *) |