277
|
1 |
|
|
2 |
signature QUOTIENT_DEF =
|
|
3 |
sig
|
|
4 |
datatype flag = absF | repF
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
5 |
val get_fun: flag -> Proof.context -> typ * typ -> term
|
293
|
6 |
val make_def: binding -> typ -> mixfix -> Attrib.binding -> term ->
|
277
|
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 |
|
279
|
18 |
(* wrapper for define *)
|
277
|
19 |
fun define name mx attr rhs lthy =
|
|
20 |
let
|
|
21 |
val ((rhs, (_ , thm)), lthy') =
|
319
|
22 |
Local_Theory.define "" ((name, mx), (attr, rhs)) lthy
|
277
|
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 |
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
32 |
fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
|
277
|
33 |
|
324
|
34 |
fun ty_strs lthy (ty1, ty2) =
|
|
35 |
(quote (Syntax.string_of_typ lthy ty1),
|
|
36 |
quote (Syntax.string_of_typ lthy ty2))
|
|
37 |
|
|
38 |
fun ty_lift_error1 lthy rty qty =
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
39 |
let
|
324
|
40 |
val (rty_str, qty_str) = ty_strs lthy (rty, qty)
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
41 |
val msg = ["quotient type", qty_str, "and lifted type", rty_str, "do not match."]
|
277
|
42 |
in
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
43 |
raise LIFT_MATCH (space_implode " " msg)
|
277
|
44 |
end
|
|
45 |
|
324
|
46 |
fun ty_lift_error2 lthy rty qty =
|
|
47 |
let
|
|
48 |
val (rty_str, qty_str) = ty_strs lthy (rty, qty)
|
|
49 |
val msg = ["No type variables allowed in", qty_str, "and", rty_str, "."]
|
|
50 |
in
|
|
51 |
raise LIFT_MATCH (space_implode " " msg)
|
|
52 |
end
|
|
53 |
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
54 |
fun get_fun_aux lthy s fs =
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
55 |
case (maps_lookup (ProofContext.theory_of lthy) s) of
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
56 |
SOME info => list_comb (Const (#mapfun info, dummyT), fs)
|
324
|
57 |
| NONE => raise LIFT_MATCH (space_implode " " ["No map function for type", quote s, "."])
|
277
|
58 |
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
59 |
fun get_const flag lthy _ qty =
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
60 |
(* FIXME: check here that _ and qty are related *)
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
61 |
let
|
279
|
62 |
val thy = ProofContext.theory_of lthy
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
63 |
val qty_name = Long_Name.base_name (fst (dest_Type qty))
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
64 |
in
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
65 |
case flag of
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
66 |
absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT)
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
67 |
| repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT)
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
68 |
end
|
277
|
69 |
|
329
|
70 |
|
|
71 |
(* calculates the aggregate abs and rep functions for a given type;
|
|
72 |
repF is for constants' arguments; absF is for constants;
|
|
73 |
function types need to be treated specially, since repF and absF
|
|
74 |
change *)
|
|
75 |
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
76 |
fun get_fun flag lthy (rty, qty) =
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
77 |
case (rty, qty) of
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
78 |
(Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
79 |
let
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
80 |
val fs_ty1 = get_fun (negF flag) lthy (ty1, ty1')
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
81 |
val fs_ty2 = get_fun flag lthy (ty2, ty2')
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
82 |
in
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
83 |
get_fun_aux lthy "fun" [fs_ty1, fs_ty2]
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
84 |
end
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
85 |
| (Type (s, []), Type (s', [])) =>
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
86 |
if s = s'
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
87 |
then mk_identity qty
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
88 |
else get_const flag lthy rty qty
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
89 |
| (Type (s, tys), Type (s', tys')) =>
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
90 |
if s = s'
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
91 |
then get_fun_aux lthy s' (map (get_fun flag lthy) (tys ~~ tys'))
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
92 |
else get_const flag lthy rty qty
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
93 |
| (TFree x, TFree x') =>
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
94 |
if x = x'
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
95 |
then mk_identity qty
|
324
|
96 |
else ty_lift_error1 lthy rty qty
|
|
97 |
| (TVar _, TVar _) => ty_lift_error2 lthy rty qty
|
|
98 |
| _ => ty_lift_error1 lthy rty qty
|
277
|
99 |
|
329
|
100 |
fun make_def qconst_bname qty mx attr rhs lthy =
|
293
|
101 |
let
|
|
102 |
val rty = fastype_of rhs
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
103 |
val (arg_rtys, res_rty) = strip_type rty
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
104 |
val (arg_qtys, res_qty) = strip_type qty
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
105 |
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
106 |
val rep_fns = map (get_fun repF lthy) (arg_rtys ~~ arg_qtys)
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
107 |
val abs_fn = get_fun absF lthy (res_rty, res_qty)
|
293
|
108 |
|
|
109 |
fun mk_fun_map t s =
|
|
110 |
Const (@{const_name "fun_map"}, dummyT) $ t $ s
|
|
111 |
|
|
112 |
val absrep_trm = (fold_rev mk_fun_map rep_fns abs_fn $ rhs)
|
|
113 |
|> Syntax.check_term lthy
|
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
114 |
|
329
|
115 |
val ((trm, thm), lthy') = define qconst_bname mx attr absrep_trm lthy
|
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
116 |
|
329
|
117 |
val qconst_str = Binding.name_of qconst_bname
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
118 |
fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs}
|
319
|
119 |
val lthy'' = Local_Theory.declaration true
|
329
|
120 |
(fn phi => qconsts_update_gen qconst_str (qcinfo phi)) lthy'
|
293
|
121 |
in
|
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
122 |
((trm, thm), lthy'')
|
293
|
123 |
end
|
|
124 |
|
|
125 |
(* interface and syntax setup *)
|
|
126 |
|
|
127 |
(* the ML-interface takes a 5-tuple consisting of *)
|
|
128 |
(* *)
|
|
129 |
(* - the name of the constant to be lifted *)
|
|
130 |
(* - its type *)
|
|
131 |
(* - its mixfix annotation *)
|
|
132 |
(* - a meta-equation defining the constant, *)
|
|
133 |
(* and the attributes of for this meta-equality *)
|
277
|
134 |
|
|
135 |
fun quotdef ((bind, qty, mx), (attr, prop)) lthy =
|
|
136 |
let
|
319
|
137 |
val (_, prop') = LocalDefs.cert_def lthy prop
|
297
|
138 |
val (_, rhs) = Primitive_Defs.abs_def prop'
|
277
|
139 |
in
|
293
|
140 |
make_def bind qty mx attr rhs lthy
|
277
|
141 |
end
|
|
142 |
|
|
143 |
fun quotdef_cmd ((bind, qtystr, mx), (attr, propstr)) lthy =
|
|
144 |
let
|
287
|
145 |
val qty = Syntax.read_typ lthy qtystr
|
|
146 |
val prop = Syntax.read_prop lthy propstr
|
277
|
147 |
in
|
|
148 |
quotdef ((bind, qty, mx), (attr, prop)) lthy |> snd
|
|
149 |
end
|
|
150 |
|
279
|
151 |
val quotdef_parser =
|
|
152 |
(OuterParse.binding --
|
|
153 |
(OuterParse.$$$ "::" |-- OuterParse.!!! (OuterParse.typ --
|
|
154 |
OuterParse.opt_mixfix' --| OuterParse.where_)) >> OuterParse.triple2) --
|
|
155 |
(SpecParse.opt_thm_name ":" -- OuterParse.prop)
|
|
156 |
|
277
|
157 |
val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"
|
|
158 |
OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)
|
|
159 |
|
|
160 |
end; (* structure *)
|
|
161 |
|
307
|
162 |
open Quotient_Def;
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
163 |
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
164 |
|