1 |
1 |
2 signature QUOTIENT_DEF = |
2 signature QUOTIENT_DEF = |
3 sig |
3 sig |
4 datatype flag = absF | repF |
|
5 val get_fun: flag -> Proof.context -> typ * typ -> term |
|
6 |
|
7 val quotient_def: mixfix -> Attrib.binding -> term -> term -> |
4 val quotient_def: mixfix -> Attrib.binding -> term -> term -> |
8 Proof.context -> (term * thm) * local_theory |
5 Proof.context -> (term * thm) * local_theory |
9 val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) -> |
6 val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) -> |
10 local_theory -> local_theory |
7 local_theory -> local_theory |
11 end; |
8 end; |
12 |
9 |
13 structure Quotient_Def: QUOTIENT_DEF = |
10 structure Quotient_Def: QUOTIENT_DEF = |
14 struct |
11 struct |
15 |
12 |
16 open Quotient_Info; |
13 open Quotient_Info; |
17 open Quotient_Type; |
14 open Quotient_Term; |
18 |
15 |
19 (* wrapper for define *) |
16 (* wrapper for define *) |
20 fun define name mx attr rhs lthy = |
17 fun define name mx attr rhs lthy = |
21 let |
18 let |
22 val ((rhs, (_ , thm)), lthy') = |
19 val ((rhs, (_ , thm)), lthy') = |
23 Local_Theory.define ((name, mx), (attr, rhs)) lthy |
20 Local_Theory.define ((name, mx), (attr, rhs)) lthy |
24 in |
21 in |
25 ((rhs, thm), lthy') |
22 ((rhs, thm), lthy') |
26 end |
23 end |
27 |
24 |
28 datatype flag = absF | repF |
|
29 |
|
30 fun negF absF = repF |
|
31 | negF repF = absF |
|
32 |
|
33 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) |
|
34 |
|
35 fun mk_compose flag (trm1, trm2) = |
|
36 case flag of |
|
37 absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2 |
|
38 | repF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 |
|
39 |
|
40 fun get_fun_aux lthy s fs = |
|
41 let |
|
42 val thy = ProofContext.theory_of lthy |
|
43 val exc = LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."]) |
|
44 val info = maps_lookup thy s handle NotFound => raise exc |
|
45 in |
|
46 list_comb (Const (#mapfun info, dummyT), fs) |
|
47 end |
|
48 |
|
49 fun get_const flag lthy _ qty = |
|
50 (* FIXME: check here that the type-constructors of _ and qty are related *) |
|
51 let |
|
52 val thy = ProofContext.theory_of lthy |
|
53 val qty_name = Long_Name.base_name (fst (dest_Type qty)) |
|
54 in |
|
55 case flag of |
|
56 absF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT) |
|
57 | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT) |
|
58 end |
|
59 |
|
60 |
|
61 (* calculates the aggregate abs and rep functions for a given type; |
|
62 repF is for constants' arguments; absF is for constants; |
|
63 function types need to be treated specially, since repF and absF |
|
64 change *) |
|
65 |
|
66 fun get_fun flag lthy (rty, qty) = |
|
67 if rty = qty then mk_identity qty else |
|
68 case (rty, qty) of |
|
69 (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) => |
|
70 let |
|
71 val fs_ty1 = get_fun (negF flag) lthy (ty1, ty1') |
|
72 val fs_ty2 = get_fun flag lthy (ty2, ty2') |
|
73 in |
|
74 get_fun_aux lthy "fun" [fs_ty1, fs_ty2] |
|
75 end |
|
76 | (Type (s, _), Type (s', [])) => |
|
77 if s = s' |
|
78 then mk_identity qty |
|
79 else get_const flag lthy rty qty |
|
80 | (Type (s, tys), Type (s', tys')) => |
|
81 let |
|
82 val args = map (get_fun flag lthy) (tys ~~ tys') |
|
83 in |
|
84 if s = s' |
|
85 then get_fun_aux lthy s args |
|
86 else mk_compose flag (get_const flag lthy rty qty, get_fun_aux lthy s args) |
|
87 end |
|
88 | (TFree x, TFree x') => |
|
89 if x = x' |
|
90 then mk_identity qty |
|
91 else raise (LIFT_MATCH "get_fun (frees)") |
|
92 | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun (vars)") |
|
93 | _ => raise (LIFT_MATCH "get_fun (default)") |
|
94 |
25 |
95 (* interface and syntax setup *) |
26 (* interface and syntax setup *) |
96 |
27 |
97 (* the ML-interface takes a 4-tuple consisting of *) |
28 (* the ML-interface takes a 4-tuple consisting of *) |
98 (* *) |
29 (* *) |