equal
deleted
inserted
replaced
22 |
22 |
23 open Quotient_Info; |
23 open Quotient_Info; |
24 |
24 |
25 exception LIFT_MATCH of string |
25 exception LIFT_MATCH of string |
26 |
26 |
|
27 (* simplifies a term according to the id_rules *) |
|
28 fun id_simplify ctxt trm = |
|
29 let |
|
30 val thy = ProofContext.theory_of ctxt |
|
31 val id_thms = id_simps_get ctxt |
|
32 in |
|
33 MetaSimplifier.rewrite_term thy id_thms [] trm |
|
34 end |
|
35 |
27 (******************************) |
36 (******************************) |
28 (* Aggregate Rep/Abs Function *) |
37 (* Aggregate Rep/Abs Function *) |
29 (******************************) |
38 (******************************) |
30 |
39 |
31 (* 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 *) |
188 val args_aux = map (double_lookup rtyenv qtyenv) vs |
197 val args_aux = map (double_lookup rtyenv qtyenv) vs |
189 val args = map (absrep_fun flag ctxt) args_aux |
198 val args = map (absrep_fun flag ctxt) args_aux |
190 val map_fun = mk_mapfun ctxt vs rty_pat |
199 val map_fun = mk_mapfun ctxt vs rty_pat |
191 val result = list_comb (map_fun, args) |
200 val result = list_comb (map_fun, args) |
192 in |
201 in |
193 if tys' = [] orelse tys' = tys |
202 (*if tys' = [] orelse tys' = tys |
194 then absrep_const flag ctxt s' |
203 then absrep_const flag ctxt s' |
195 else mk_fun_compose flag (absrep_const flag ctxt s', result) |
204 else*) mk_fun_compose flag (absrep_const flag ctxt s', result) |
196 end |
205 end |
197 | (TFree x, TFree x') => |
206 | (TFree x, TFree x') => |
198 if x = x' |
207 if x = x' |
199 then mk_identity rty |
208 then mk_identity rty |
200 else raise (LIFT_MATCH "absrep_fun (frees)") |
209 else raise (LIFT_MATCH "absrep_fun (frees)") |
202 | _ => raise (LIFT_MATCH "absrep_fun (default)") |
211 | _ => raise (LIFT_MATCH "absrep_fun (default)") |
203 |
212 |
204 fun absrep_fun_chk flag ctxt (rty, qty) = |
213 fun absrep_fun_chk flag ctxt (rty, qty) = |
205 absrep_fun flag ctxt (rty, qty) |
214 absrep_fun flag ctxt (rty, qty) |
206 |> Syntax.check_term ctxt |
215 |> Syntax.check_term ctxt |
207 |
216 |> id_simplify ctxt |
208 |
217 |
209 (**********************************) |
218 (**********************************) |
210 (* Aggregate Equivalence Relation *) |
219 (* Aggregate Equivalence Relation *) |
211 (**********************************) |
220 (**********************************) |
212 |
221 |
289 val rel_map = mk_relmap ctxt vs rty_pat |
298 val rel_map = mk_relmap ctxt vs rty_pat |
290 val result = list_comb (rel_map, args) |
299 val result = list_comb (rel_map, args) |
291 val eqv_rel = get_equiv_rel ctxt s' |
300 val eqv_rel = get_equiv_rel ctxt s' |
292 val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool}) |
301 val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool}) |
293 in |
302 in |
294 if tys' = [] orelse tys' = tys |
303 (*if tys' = [] orelse tys' = tys |
295 then eqv_rel' |
304 then eqv_rel' |
296 else mk_rel_compose (result, eqv_rel') |
305 else*) mk_rel_compose (result, eqv_rel') |
297 end |
306 end |
298 | _ => HOLogic.eq_const rty |
307 | _ => HOLogic.eq_const rty |
299 |
308 |
300 fun equiv_relation_chk ctxt (rty, qty) = |
309 fun equiv_relation_chk ctxt (rty, qty) = |
301 equiv_relation ctxt (rty, qty) |
310 equiv_relation ctxt (rty, qty) |
302 |> Syntax.check_term ctxt |
311 |> Syntax.check_term ctxt |
|
312 |> id_simplify ctxt |
303 |
313 |
304 |
314 |
305 (******************) |
315 (******************) |
306 (* Regularization *) |
316 (* Regularization *) |
307 (******************) |
317 (******************) |
450 end |
460 end |
451 |
461 |
452 fun regularize_trm_chk ctxt (rtrm, qtrm) = |
462 fun regularize_trm_chk ctxt (rtrm, qtrm) = |
453 regularize_trm ctxt (rtrm, qtrm) |
463 regularize_trm ctxt (rtrm, qtrm) |
454 |> Syntax.check_term ctxt |
464 |> Syntax.check_term ctxt |
|
465 |> id_simplify ctxt |
455 |
466 |
456 |
467 |
457 (*********************) |
468 (*********************) |
458 (* Rep/Abs Injection *) |
469 (* Rep/Abs Injection *) |
459 (*********************) |
470 (*********************) |
488 *) |
499 *) |
489 |
500 |
490 fun mk_repabs ctxt (T, T') trm = |
501 fun mk_repabs ctxt (T, T') trm = |
491 absrep_fun repF ctxt (T, T') $ (absrep_fun absF ctxt (T, T') $ trm) |
502 absrep_fun repF ctxt (T, T') $ (absrep_fun absF ctxt (T, T') $ trm) |
492 |
503 |
|
504 fun inj_repabs_err ctxt msg rtrm qtrm = |
|
505 let |
|
506 val rtrm_str = Syntax.string_of_term ctxt rtrm |
|
507 val qtrm_str = Syntax.string_of_term ctxt qtrm |
|
508 in |
|
509 raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str]) |
|
510 end |
|
511 |
493 |
512 |
494 (* bound variables need to be treated properly, *) |
513 (* bound variables need to be treated properly, *) |
495 (* as the type of subterms needs to be calculated *) |
514 (* as the type of subterms needs to be calculated *) |
496 |
515 |
497 fun inj_repabs_trm ctxt (rtrm, qtrm) = |
516 fun inj_repabs_trm ctxt (rtrm, qtrm) = |
538 in |
557 in |
539 if rty = T' then rtrm |
558 if rty = T' then rtrm |
540 else mk_repabs ctxt (rty, T') rtrm |
559 else mk_repabs ctxt (rty, T') rtrm |
541 end |
560 end |
542 |
561 |
543 | _ => raise (LIFT_MATCH "injection (default)") |
562 | _ => inj_repabs_err ctxt "injection (default):" rtrm qtrm |
544 |
563 |
545 fun inj_repabs_trm_chk ctxt (rtrm, qtrm) = |
564 fun inj_repabs_trm_chk ctxt (rtrm, qtrm) = |
546 inj_repabs_trm ctxt (rtrm, qtrm) |
565 inj_repabs_trm ctxt (rtrm, qtrm) |
547 |> Syntax.check_term ctxt |
566 |> Syntax.check_term ctxt |
|
567 |> id_simplify ctxt |
548 |
568 |
549 end; (* structure *) |
569 end; (* structure *) |
550 |
570 |
551 |
571 |
552 |
572 |