1 signature QUOTIENT_TERM = |
1 signature QUOTIENT_TERM = |
2 sig |
2 sig |
3 exception LIFT_MATCH of string |
3 exception LIFT_MATCH of string |
4 |
4 |
5 datatype flag = absF | repF |
5 datatype flag = absF | repF |
6 val get_fun: flag -> Proof.context -> (typ * typ) -> term |
6 |
|
7 val absrep_fun: flag -> Proof.context -> (typ * typ) -> term |
|
8 val absrep_fun_chk: flag -> Proof.context -> (typ * typ) -> term |
7 |
9 |
8 val regularize_trm: Proof.context -> (term * term) -> term |
10 val regularize_trm: Proof.context -> (term * term) -> term |
|
11 val regularize_trm_chk: Proof.context -> (term * term) -> term |
|
12 |
9 val inj_repabs_trm: Proof.context -> (term * term) -> term |
13 val inj_repabs_trm: Proof.context -> (term * term) -> term |
|
14 val inj_repabs_trm_chk: Proof.context -> (term * term) -> term |
10 end; |
15 end; |
11 |
16 |
12 structure Quotient_Term: QUOTIENT_TERM = |
17 structure Quotient_Term: QUOTIENT_TERM = |
13 struct |
18 struct |
14 |
19 |
31 fun mk_compose flag (trm1, trm2) = |
36 fun mk_compose flag (trm1, trm2) = |
32 case flag of |
37 case flag of |
33 absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2 |
38 absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2 |
34 | repF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 |
39 | repF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 |
35 |
40 |
36 fun get_fun_aux lthy s fs = |
41 fun absrep_fun_aux lthy s fs = |
37 let |
42 let |
38 val thy = ProofContext.theory_of lthy |
43 val thy = ProofContext.theory_of lthy |
39 val exc = LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."]) |
44 val exc = LIFT_MATCH (space_implode " " ["absrep_fun_aux: no map for type", quote s, "."]) |
40 val info = maps_lookup thy s handle NotFound => raise exc |
45 val info = maps_lookup thy s handle NotFound => raise exc |
41 in |
46 in |
42 list_comb (Const (#mapfun info, dummyT), fs) |
47 list_comb (Const (#mapfun info, dummyT), fs) |
43 end |
48 end |
44 |
49 |
51 case flag of |
56 case flag of |
52 absF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT) |
57 absF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT) |
53 | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT) |
58 | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT) |
54 end |
59 end |
55 |
60 |
56 fun get_fun flag lthy (rty, qty) = |
61 fun absrep_fun flag lthy (rty, qty) = |
57 if rty = qty then mk_identity qty else |
62 if rty = qty then mk_identity qty else |
58 case (rty, qty) of |
63 case (rty, qty) of |
59 (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) => |
64 (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) => |
60 let |
65 let |
61 val fs_ty1 = get_fun (negF flag) lthy (ty1, ty1') |
66 val fs_ty1 = absrep_fun (negF flag) lthy (ty1, ty1') |
62 val fs_ty2 = get_fun flag lthy (ty2, ty2') |
67 val fs_ty2 = absrep_fun flag lthy (ty2, ty2') |
63 in |
68 in |
64 get_fun_aux lthy "fun" [fs_ty1, fs_ty2] |
69 absrep_fun_aux lthy "fun" [fs_ty1, fs_ty2] |
65 end |
70 end |
66 | (Type (s, _), Type (s', [])) => |
71 | (Type (s, _), Type (s', [])) => |
67 if s = s' |
72 if s = s' |
68 then mk_identity qty |
73 then mk_identity qty |
69 else get_const flag lthy rty qty |
74 else get_const flag lthy rty qty |
70 | (Type (s, tys), Type (s', tys')) => |
75 | (Type (s, tys), Type (s', tys')) => |
71 let |
76 let |
72 val args = map (get_fun flag lthy) (tys ~~ tys') |
77 val args = map (absrep_fun flag lthy) (tys ~~ tys') |
73 in |
78 in |
74 if s = s' |
79 if s = s' |
75 then get_fun_aux lthy s args |
80 then absrep_fun_aux lthy s args |
76 else mk_compose flag (get_const flag lthy rty qty, get_fun_aux lthy s args) |
81 else mk_compose flag (get_const flag lthy rty qty, absrep_fun_aux lthy s args) |
77 end |
82 end |
78 | (TFree x, TFree x') => |
83 | (TFree x, TFree x') => |
79 if x = x' |
84 if x = x' |
80 then mk_identity qty |
85 then mk_identity qty |
81 else raise (LIFT_MATCH "get_fun (frees)") |
86 else raise (LIFT_MATCH "absrep_fun (frees)") |
82 | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun (vars)") |
87 | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)") |
83 | _ => raise (LIFT_MATCH "get_fun (default)") |
88 | _ => raise (LIFT_MATCH "absrep_fun (default)") |
84 |
89 |
|
90 fun absrep_fun_chk flag lthy (rty, qty) = |
|
91 absrep_fun flag lthy (rty, qty) |
|
92 |> Syntax.check_term lthy |
85 |
93 |
86 (* |
94 (* |
87 Regularizing an rtrm means: |
95 Regularizing an rtrm means: |
88 |
96 |
89 - Quantifiers over types that need lifting are replaced |
97 - Quantifiers over types that need lifting are replaced |
288 |
298 |
289 Vars case cannot occur. |
299 Vars case cannot occur. |
290 *) |
300 *) |
291 |
301 |
292 fun mk_repabs lthy (T, T') trm = |
302 fun mk_repabs lthy (T, T') trm = |
293 get_fun repF lthy (T, T') $ (get_fun absF lthy (T, T') $ trm) |
303 absrep_fun repF lthy (T, T') $ (absrep_fun absF lthy (T, T') $ trm) |
294 |
304 |
295 |
305 |
296 (* bound variables need to be treated properly, *) |
306 (* bound variables need to be treated properly, *) |
297 (* as the type of subterms needs to be calculated *) |
307 (* as the type of subterms needs to be calculated *) |
298 |
308 |