277
|
1 |
|
|
2 |
signature QUOTIENT_DEF =
|
|
3 |
sig
|
|
4 |
datatype flag = absF | repF
|
|
5 |
val get_fun: flag -> (typ * typ) list -> Proof.context -> typ -> term * (typ * typ)
|
|
6 |
val make_def: binding -> term -> typ -> mixfix -> Attrib.binding -> (typ * typ) list ->
|
|
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') =
|
|
22 |
LocalTheory.define Thm.internalK ((name, mx), (attr, rhs)) lthy
|
|
23 |
in
|
|
24 |
((rhs, thm), lthy')
|
|
25 |
end
|
|
26 |
|
|
27 |
|
|
28 |
(* calculates the aggregate abs and rep functions for a given type;
|
|
29 |
repF is for constants' arguments; absF is for constants;
|
|
30 |
function types need to be treated specially, since repF and absF
|
|
31 |
change *)
|
|
32 |
|
|
33 |
datatype flag = absF | repF
|
|
34 |
|
|
35 |
fun negF absF = repF
|
|
36 |
| negF repF = absF
|
|
37 |
|
|
38 |
fun get_fun flag qenv lthy ty =
|
|
39 |
let
|
|
40 |
|
|
41 |
fun get_fun_aux s fs_tys =
|
|
42 |
let
|
|
43 |
val (fs, tys) = split_list fs_tys
|
|
44 |
val (otys, ntys) = split_list tys
|
|
45 |
val oty = Type (s, otys)
|
|
46 |
val nty = Type (s, ntys)
|
|
47 |
val ftys = map (op -->) tys
|
|
48 |
in
|
|
49 |
(case (maps_lookup (ProofContext.theory_of lthy) s) of
|
|
50 |
SOME info => (list_comb (Const (#mapfun info, ftys ---> (oty --> nty)), fs), (oty, nty))
|
|
51 |
| NONE => error ("no map association for type " ^ s))
|
|
52 |
end
|
|
53 |
|
|
54 |
fun get_fun_fun fs_tys =
|
|
55 |
let
|
|
56 |
val (fs, tys) = split_list fs_tys
|
|
57 |
val ([oty1, oty2], [nty1, nty2]) = split_list tys
|
|
58 |
val oty = nty1 --> oty2
|
|
59 |
val nty = oty1 --> nty2
|
|
60 |
val ftys = map (op -->) tys
|
|
61 |
in
|
|
62 |
(list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty))
|
|
63 |
end
|
|
64 |
|
|
65 |
fun get_const flag (qty, rty) =
|
|
66 |
let
|
|
67 |
val thy = ProofContext.theory_of lthy
|
|
68 |
val qty_name = Long_Name.base_name (fst (dest_Type qty))
|
|
69 |
in
|
|
70 |
case flag of
|
|
71 |
absF => (Const (Sign.full_bname thy ("ABS_" ^ qty_name), rty --> qty), (rty, qty))
|
|
72 |
| repF => (Const (Sign.full_bname thy ("REP_" ^ qty_name), qty --> rty), (qty, rty))
|
|
73 |
end
|
|
74 |
|
|
75 |
fun mk_identity ty = Abs ("", ty, Bound 0)
|
|
76 |
|
|
77 |
in
|
|
78 |
if (AList.defined (op=) qenv ty)
|
280
|
79 |
then (get_const flag (the (Quotient_Info.lookup_qenv (op=) qenv ty)))
|
277
|
80 |
else (case ty of
|
|
81 |
TFree _ => (mk_identity ty, (ty, ty))
|
|
82 |
| Type (_, []) => (mk_identity ty, (ty, ty))
|
|
83 |
| Type ("fun" , [ty1, ty2]) =>
|
|
84 |
get_fun_fun [get_fun (negF flag) qenv lthy ty1, get_fun flag qenv lthy ty2]
|
|
85 |
| Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys)
|
|
86 |
| _ => raise ERROR ("no type variables"))
|
|
87 |
end
|
|
88 |
|
|
89 |
fun make_def nconst_bname rhs qty mx attr qenv lthy =
|
|
90 |
let
|
|
91 |
val (arg_tys, res_ty) = strip_type qty
|
|
92 |
|
|
93 |
val rep_fns = map (fst o get_fun repF qenv lthy) arg_tys
|
|
94 |
val abs_fn = (fst o get_fun absF qenv lthy) res_ty
|
|
95 |
|
|
96 |
fun mk_fun_map t s =
|
|
97 |
Const (@{const_name "fun_map"}, dummyT) $ t $ s
|
|
98 |
|
|
99 |
val absrep_fn = fold_rev mk_fun_map rep_fns abs_fn
|
|
100 |
|> Syntax.check_term lthy
|
|
101 |
in
|
|
102 |
define nconst_bname mx attr (absrep_fn $ rhs) lthy
|
|
103 |
end
|
|
104 |
|
|
105 |
|
|
106 |
(* returns all subterms where two types differ *)
|
|
107 |
fun diff (T, S) Ds =
|
|
108 |
case (T, S) of
|
|
109 |
(TVar v, TVar u) => if v = u then Ds else (T, S)::Ds
|
|
110 |
| (TFree x, TFree y) => if x = y then Ds else (T, S)::Ds
|
|
111 |
| (Type (a, Ts), Type (b, Us)) =>
|
|
112 |
if a = b then diffs (Ts, Us) Ds else (T, S)::Ds
|
|
113 |
| _ => (T, S)::Ds
|
|
114 |
and diffs (T::Ts, U::Us) Ds = diffs (Ts, Us) (diff (T, U) Ds)
|
|
115 |
| diffs ([], []) Ds = Ds
|
|
116 |
| diffs _ _ = error "Unequal length of type arguments"
|
|
117 |
|
|
118 |
|
279
|
119 |
(* sanity check that the calculated quotient environment
|
|
120 |
matches with the stored quotient environment. *)
|
277
|
121 |
fun error_msg lthy (qty, rty) =
|
|
122 |
let
|
|
123 |
val qtystr = quote (Syntax.string_of_typ lthy qty)
|
|
124 |
val rtystr = quote (Syntax.string_of_typ lthy rty)
|
|
125 |
in
|
|
126 |
error (implode ["Quotient type ", qtystr, " does not match with ", rtystr])
|
|
127 |
end
|
|
128 |
|
|
129 |
fun sanity_chk lthy qenv =
|
|
130 |
let
|
286
|
131 |
val global_qenv = Quotient_Info.mk_qenv lthy
|
279
|
132 |
val thy = ProofContext.theory_of lthy
|
277
|
133 |
|
279
|
134 |
fun is_inst thy (qty, rty) (qty', rty') =
|
|
135 |
if Sign.typ_instance thy (qty, qty')
|
|
136 |
then let
|
|
137 |
val inst = Sign.typ_match thy (qty', qty) Vartab.empty
|
|
138 |
in
|
|
139 |
rty = Envir.subst_type inst rty'
|
|
140 |
end
|
|
141 |
else false
|
277
|
142 |
|
279
|
143 |
fun chk_inst (qty, rty) =
|
286
|
144 |
if exists (is_inst thy (qty, rty)) global_qenv
|
|
145 |
then true
|
279
|
146 |
else error_msg lthy (qty, rty)
|
277
|
147 |
in
|
|
148 |
forall chk_inst qenv
|
|
149 |
end
|
|
150 |
|
|
151 |
|
|
152 |
fun quotdef ((bind, qty, mx), (attr, prop)) lthy =
|
|
153 |
let
|
|
154 |
val (_, prop') = PrimitiveDefs.dest_def lthy (K true) (K false) (K false) prop
|
|
155 |
val (_, rhs) = PrimitiveDefs.abs_def prop'
|
|
156 |
|
|
157 |
val rty = fastype_of rhs
|
|
158 |
val qenv = distinct (op=) (diff (qty, rty) [])
|
|
159 |
in
|
|
160 |
sanity_chk lthy qenv;
|
|
161 |
make_def bind rhs qty mx attr qenv lthy
|
|
162 |
end
|
|
163 |
|
|
164 |
fun quotdef_cmd ((bind, qtystr, mx), (attr, propstr)) lthy =
|
|
165 |
let
|
|
166 |
val qty = (Syntax.check_typ lthy o Syntax.parse_typ lthy) qtystr
|
|
167 |
val prop = (Syntax.check_prop lthy o Syntax.parse_prop lthy) propstr
|
|
168 |
in
|
|
169 |
quotdef ((bind, qty, mx), (attr, prop)) lthy |> snd
|
|
170 |
end
|
|
171 |
|
279
|
172 |
|
|
173 |
val quotdef_parser =
|
|
174 |
(OuterParse.binding --
|
|
175 |
(OuterParse.$$$ "::" |-- OuterParse.!!! (OuterParse.typ --
|
|
176 |
OuterParse.opt_mixfix' --| OuterParse.where_)) >> OuterParse.triple2) --
|
|
177 |
(SpecParse.opt_thm_name ":" -- OuterParse.prop)
|
|
178 |
|
277
|
179 |
val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"
|
|
180 |
OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)
|
|
181 |
|
|
182 |
end; (* structure *)
|
|
183 |
|
|
184 |
open Quotient_Def; |