|
1 |
|
2 signature QUOTIENT_DEF = |
|
3 sig |
|
4 datatype flag = absF | repF |
|
5 val get_fun: flag -> Proof.context -> typ * typ -> term |
|
6 val make_def: binding -> typ -> mixfix -> Attrib.binding -> term -> |
|
7 Proof.context -> (term * thm) * local_theory |
|
8 |
|
9 val quotdef: (binding * typ * mixfix) * (Attrib.binding * term) -> |
|
10 local_theory -> (term * thm) * local_theory |
|
11 val quotdef_cmd: (binding * string * mixfix) * (Attrib.binding * string) -> |
|
12 local_theory -> local_theory |
|
13 end; |
|
14 |
|
15 structure Quotient_Def: QUOTIENT_DEF = |
|
16 struct |
|
17 |
|
18 (* wrapper for define *) |
|
19 fun define name mx attr rhs lthy = |
|
20 let |
|
21 val ((rhs, (_ , thm)), lthy') = |
|
22 Local_Theory.define ((name, mx), (attr, rhs)) lthy |
|
23 in |
|
24 ((rhs, thm), lthy') |
|
25 end |
|
26 |
|
27 datatype flag = absF | repF |
|
28 |
|
29 fun negF absF = repF |
|
30 | negF repF = absF |
|
31 |
|
32 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) |
|
33 |
|
34 fun get_fun_aux lthy s fs = |
|
35 case (maps_lookup (ProofContext.theory_of lthy) s) of |
|
36 SOME info => list_comb (Const (#mapfun info, dummyT), fs) |
|
37 | NONE => raise |
|
38 (LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."])) |
|
39 |
|
40 fun get_const flag lthy _ qty = |
|
41 (* FIXME: check here that _ and qty are related *) |
|
42 let |
|
43 val thy = ProofContext.theory_of lthy |
|
44 val qty_name = Long_Name.base_name (fst (dest_Type qty)) |
|
45 in |
|
46 case flag of |
|
47 absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT) |
|
48 | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT) |
|
49 end |
|
50 |
|
51 |
|
52 (* calculates the aggregate abs and rep functions for a given type; |
|
53 repF is for constants' arguments; absF is for constants; |
|
54 function types need to be treated specially, since repF and absF |
|
55 change *) |
|
56 |
|
57 fun get_fun flag lthy (rty, qty) = |
|
58 if rty = qty then mk_identity qty else |
|
59 case (rty, qty) of |
|
60 (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) => |
|
61 let |
|
62 val fs_ty1 = get_fun (negF flag) lthy (ty1, ty1') |
|
63 val fs_ty2 = get_fun flag lthy (ty2, ty2') |
|
64 in |
|
65 get_fun_aux lthy "fun" [fs_ty1, fs_ty2] |
|
66 end |
|
67 | (Type (s, []), Type (s', [])) => |
|
68 if s = s' |
|
69 then mk_identity qty |
|
70 else get_const flag lthy rty qty |
|
71 | (Type (s, tys), Type (s', tys')) => |
|
72 if s = s' |
|
73 then get_fun_aux lthy s' (map (get_fun flag lthy) (tys ~~ tys')) |
|
74 else get_const flag lthy rty qty |
|
75 | (TFree x, TFree x') => |
|
76 if x = x' |
|
77 then mk_identity qty |
|
78 else raise (LIFT_MATCH "get_fun") |
|
79 | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun") |
|
80 | _ => raise (LIFT_MATCH "get_fun") |
|
81 |
|
82 fun make_def qconst_bname qty mx attr rhs lthy = |
|
83 let |
|
84 val absrep_trm = get_fun absF lthy (fastype_of rhs, qty) $ rhs |
|
85 |> Syntax.check_term lthy |
|
86 |
|
87 val ((trm, thm), lthy') = define qconst_bname mx attr absrep_trm lthy |
|
88 |
|
89 fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs, def = thm} |
|
90 val lthy'' = Local_Theory.declaration true |
|
91 (fn phi => |
|
92 let |
|
93 val qconst_str = fst (Term.dest_Const (Morphism.term phi trm)) |
|
94 in |
|
95 qconsts_update_gen qconst_str (qcinfo phi) |
|
96 end) lthy' |
|
97 in |
|
98 ((trm, thm), lthy'') |
|
99 end |
|
100 |
|
101 (* interface and syntax setup *) |
|
102 |
|
103 (* the ML-interface takes a 5-tuple consisting of *) |
|
104 (* *) |
|
105 (* - the name of the constant to be lifted *) |
|
106 (* - its type *) |
|
107 (* - its mixfix annotation *) |
|
108 (* - a meta-equation defining the constant, *) |
|
109 (* and the attributes of for this meta-equality *) |
|
110 |
|
111 fun quotdef ((bind, qty, mx), (attr, prop)) lthy = |
|
112 let |
|
113 val (_, prop') = LocalDefs.cert_def lthy prop |
|
114 val (_, rhs) = Primitive_Defs.abs_def prop' |
|
115 in |
|
116 make_def bind qty mx attr rhs lthy |
|
117 end |
|
118 |
|
119 fun quotdef_cmd ((bind, qtystr, mx), (attr, propstr)) lthy = |
|
120 let |
|
121 val qty = Syntax.read_typ lthy qtystr |
|
122 val prop = Syntax.read_prop lthy propstr |
|
123 in |
|
124 quotdef ((bind, qty, mx), (attr, prop)) lthy |> snd |
|
125 end |
|
126 |
|
127 val quotdef_parser = |
|
128 (OuterParse.binding -- |
|
129 (OuterParse.$$$ "::" |-- OuterParse.!!! (OuterParse.typ -- |
|
130 OuterParse.opt_mixfix' --| OuterParse.where_)) >> OuterParse.triple2) -- |
|
131 (SpecParse.opt_thm_name ":" -- OuterParse.prop) |
|
132 |
|
133 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants" |
|
134 OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd) |
|
135 |
|
136 end; (* structure *) |
|
137 |
|
138 open Quotient_Def; |
|
139 |
|
140 |