5177
|
1 |
(* Title: HOL/Tools/datatype_aux.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Stefan Berghofer
|
|
4 |
Copyright 1998 TU Muenchen
|
|
5 |
|
|
6 |
Auxiliary functions for defining datatypes
|
|
7 |
*)
|
|
8 |
|
|
9 |
signature DATATYPE_AUX =
|
|
10 |
sig
|
|
11 |
val foldl1 : ('a * 'a -> 'a) -> 'a list -> 'a
|
|
12 |
|
|
13 |
val get_thy : string -> theory -> theory option
|
|
14 |
|
|
15 |
val store_thmss : string -> string list -> thm list list -> theory -> theory
|
|
16 |
val store_thms : string -> string list -> thm list -> theory -> theory
|
|
17 |
|
|
18 |
val split_conj_thm : thm -> thm list
|
|
19 |
val mk_conj : term list -> term
|
|
20 |
val mk_disj : term list -> term
|
|
21 |
|
|
22 |
val indtac : thm -> int -> tactic
|
|
23 |
val exh_tac : (string -> thm) -> int -> tactic
|
|
24 |
|
|
25 |
datatype dtyp =
|
|
26 |
DtTFree of string
|
|
27 |
| DtType of string * (dtyp list)
|
|
28 |
| DtRec of int;
|
|
29 |
|
|
30 |
type datatype_info
|
|
31 |
|
|
32 |
val dtyp_of_typ : (string * string list) list -> typ -> dtyp
|
|
33 |
val mk_Free : string -> typ -> int -> term
|
|
34 |
val is_rec_type : dtyp -> bool
|
|
35 |
val typ_of_dtyp : (int * (string * dtyp list *
|
|
36 |
(string * dtyp list) list)) list -> (string * sort) list -> dtyp -> typ
|
|
37 |
val dest_DtTFree : dtyp -> string
|
|
38 |
val dest_DtRec : dtyp -> int
|
|
39 |
val dest_TFree : typ -> string
|
|
40 |
val dest_conj : term -> term list
|
|
41 |
val get_nonrec_types : (int * (string * dtyp list *
|
|
42 |
(string * dtyp list) list)) list -> (string * sort) list -> typ list
|
|
43 |
val get_rec_types : (int * (string * dtyp list *
|
|
44 |
(string * dtyp list) list)) list -> (string * sort) list -> typ list
|
|
45 |
val check_nonempty : (int * (string * dtyp list *
|
|
46 |
(string * dtyp list) list)) list list -> unit
|
|
47 |
val unfold_datatypes :
|
|
48 |
datatype_info Symtab.table ->
|
|
49 |
(int * (string * dtyp list *
|
|
50 |
(string * dtyp list) list)) list -> int ->
|
|
51 |
(int * (string * dtyp list *
|
|
52 |
(string * dtyp list) list)) list list * int
|
|
53 |
end;
|
|
54 |
|
|
55 |
structure DatatypeAux : DATATYPE_AUX =
|
|
56 |
struct
|
|
57 |
|
|
58 |
(* FIXME: move to library ? *)
|
|
59 |
fun foldl1 f (x::xs) = foldl f (x, xs);
|
|
60 |
|
|
61 |
fun get_thy name thy = find_first
|
|
62 |
(equal name o Sign.name_of o sign_of) (ancestors_of thy);
|
|
63 |
|
|
64 |
(* store theorems in theory *)
|
|
65 |
|
|
66 |
fun store_thmss label tnames thmss thy =
|
|
67 |
foldr (fn ((tname, thms), thy') => thy' |>
|
|
68 |
(if length tnames = 1 then I else Theory.add_path tname) |>
|
|
69 |
PureThy.add_tthmss [((label, map Attribute.tthm_of thms), [])] |>
|
|
70 |
(if length tnames = 1 then I else Theory.parent_path))
|
|
71 |
(tnames ~~ thmss, thy);
|
|
72 |
|
|
73 |
fun store_thms label tnames thms thy =
|
|
74 |
foldr (fn ((tname, thm), thy') => thy' |>
|
|
75 |
(if length tnames = 1 then I else Theory.add_path tname) |>
|
|
76 |
PureThy.add_tthms [((label, Attribute.tthm_of thm), [])] |>
|
|
77 |
(if length tnames = 1 then I else Theory.parent_path))
|
|
78 |
(tnames ~~ thms, thy);
|
|
79 |
|
|
80 |
(* split theorem thm_1 & ... & thm_n into n theorems *)
|
|
81 |
|
|
82 |
fun split_conj_thm th =
|
|
83 |
((th RS conjunct1)::(split_conj_thm (th RS conjunct2))) handle _ => [th];
|
|
84 |
|
|
85 |
val mk_conj = foldr1 (HOLogic.mk_binop "op &");
|
|
86 |
val mk_disj = foldr1 (HOLogic.mk_binop "op |");
|
|
87 |
|
|
88 |
fun dest_conj (Const ("op &", _) $ t $ t') = t::(dest_conj t')
|
|
89 |
| dest_conj t = [t];
|
|
90 |
|
|
91 |
(* instantiate induction rule *)
|
|
92 |
|
|
93 |
fun indtac indrule i st =
|
|
94 |
let
|
|
95 |
val ts = dest_conj (HOLogic.dest_Trueprop (concl_of indrule));
|
|
96 |
val ts' = dest_conj (HOLogic.dest_Trueprop
|
|
97 |
(Logic.strip_imp_concl (nth_elem (i - 1, prems_of st))));
|
|
98 |
val getP = if can HOLogic.dest_imp (hd ts) then
|
|
99 |
(apfst Some) o HOLogic.dest_imp else pair None;
|
|
100 |
fun abstr (t1, t2) = (case t1 of
|
|
101 |
None => let val [Free (s, T)] = add_term_frees (t2, [])
|
|
102 |
in absfree (s, T, t2) end
|
|
103 |
| Some (_ $ t' $ _) => Abs ("x", fastype_of t', abstract_over (t', t2)))
|
|
104 |
val cert = cterm_of (sign_of_thm st);
|
|
105 |
val Ps = map (cert o head_of o snd o getP) ts;
|
|
106 |
val indrule' = cterm_instantiate (Ps ~~
|
|
107 |
(map (cert o abstr o getP) ts')) indrule
|
|
108 |
in
|
|
109 |
rtac indrule' i st
|
|
110 |
end;
|
|
111 |
|
|
112 |
(* perform exhaustive case analysis on last parameter of subgoal i *)
|
|
113 |
|
|
114 |
fun exh_tac exh_thm_of i state =
|
|
115 |
let
|
|
116 |
val sg = sign_of_thm state;
|
|
117 |
val prem = nth_elem (i - 1, prems_of state);
|
|
118 |
val params = Logic.strip_params prem;
|
|
119 |
val (_, Type (tname, _)) = hd (rev params);
|
|
120 |
val exhaustion = lift_rule (state, i) (exh_thm_of tname);
|
|
121 |
val prem' = hd (prems_of exhaustion);
|
|
122 |
val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem'));
|
|
123 |
val exhaustion' = cterm_instantiate [(cterm_of sg (head_of lhs),
|
|
124 |
cterm_of sg (foldr (fn ((_, T), t) => Abs ("z", T, t))
|
|
125 |
(params, Bound 0)))] exhaustion
|
|
126 |
in compose_tac (false, exhaustion', nprems_of exhaustion) i state
|
|
127 |
end;
|
|
128 |
|
|
129 |
(********************** Internal description of datatypes *********************)
|
|
130 |
|
|
131 |
datatype dtyp =
|
|
132 |
DtTFree of string
|
|
133 |
| DtType of string * (dtyp list)
|
|
134 |
| DtRec of int;
|
|
135 |
|
|
136 |
(* information about datatypes *)
|
|
137 |
|
|
138 |
type datatype_info =
|
|
139 |
{index : int,
|
|
140 |
descr : (int * (string * dtyp list *
|
|
141 |
(string * dtyp list) list)) list,
|
|
142 |
rec_names : string list,
|
|
143 |
rec_rewrites : thm list,
|
|
144 |
case_name : string,
|
|
145 |
case_rewrites : thm list,
|
|
146 |
induction : thm,
|
|
147 |
exhaustion : thm,
|
|
148 |
distinct : thm list,
|
|
149 |
inject : thm list,
|
|
150 |
nchotomy : thm,
|
|
151 |
case_cong : thm};
|
|
152 |
|
|
153 |
fun mk_Free s T i = Free (s ^ (string_of_int i), T);
|
|
154 |
|
|
155 |
fun subst_DtTFree _ substs (T as (DtTFree name)) =
|
|
156 |
(case assoc (substs, name) of
|
|
157 |
None => T
|
|
158 |
| Some U => U)
|
|
159 |
| subst_DtTFree i substs (DtType (name, ts)) =
|
|
160 |
DtType (name, map (subst_DtTFree i substs) ts)
|
|
161 |
| subst_DtTFree i _ (DtRec j) = DtRec (i + j);
|
|
162 |
|
|
163 |
fun dest_DtTFree (DtTFree a) = a;
|
|
164 |
fun dest_DtRec (DtRec i) = i;
|
|
165 |
|
|
166 |
fun is_rec_type (DtType (_, dts)) = exists is_rec_type dts
|
|
167 |
| is_rec_type (DtRec _) = true
|
|
168 |
| is_rec_type _ = false;
|
|
169 |
|
|
170 |
fun dest_TFree (TFree (n, _)) = n;
|
|
171 |
|
|
172 |
fun dtyp_of_typ _ (TFree (n, _)) = DtTFree n
|
|
173 |
| dtyp_of_typ _ (TVar _) = error "Illegal schematic type variable(s)"
|
|
174 |
| dtyp_of_typ new_dts (Type (tname, Ts)) =
|
|
175 |
(case assoc (new_dts, tname) of
|
|
176 |
None => DtType (tname, map (dtyp_of_typ new_dts) Ts)
|
|
177 |
| Some vs => if map (try dest_TFree) Ts = map Some vs then
|
|
178 |
DtRec (find_index (curry op = tname o fst) new_dts)
|
|
179 |
else error ("Illegal occurence of recursive type " ^ tname));
|
|
180 |
|
|
181 |
fun typ_of_dtyp descr sorts (DtTFree a) = TFree (a, the (assoc (sorts, a)))
|
|
182 |
| typ_of_dtyp descr sorts (DtRec i) =
|
|
183 |
let val (s, ds, _) = the (assoc (descr, i))
|
|
184 |
in Type (s, map (typ_of_dtyp descr sorts) ds) end
|
|
185 |
| typ_of_dtyp descr sorts (DtType (s, ds)) =
|
|
186 |
Type (s, map (typ_of_dtyp descr sorts) ds);
|
|
187 |
|
|
188 |
(* find all non-recursive types in datatype description *)
|
|
189 |
|
|
190 |
fun get_nonrec_types descr sorts =
|
|
191 |
let fun add (Ts, T as DtTFree _) = T ins Ts
|
|
192 |
| add (Ts, T as DtType _) = T ins Ts
|
|
193 |
| add (Ts, _) = Ts
|
|
194 |
in map (typ_of_dtyp descr sorts) (foldl (fn (Ts, (_, (_, _, constrs))) =>
|
|
195 |
foldl (fn (Ts', (_, cargs)) =>
|
|
196 |
foldl add (Ts', cargs)) (Ts, constrs)) ([], descr))
|
|
197 |
end;
|
|
198 |
|
|
199 |
(* get all recursive types in datatype description *)
|
|
200 |
|
|
201 |
fun get_rec_types descr sorts = map (fn (_ , (s, ds, _)) =>
|
|
202 |
Type (s, map (typ_of_dtyp descr sorts) ds)) descr;
|
|
203 |
|
|
204 |
(* nonemptiness check for datatypes *)
|
|
205 |
|
|
206 |
fun check_nonempty descr =
|
|
207 |
let
|
|
208 |
val descr' = flat descr;
|
|
209 |
fun is_nonempty_dt is i =
|
|
210 |
let
|
|
211 |
val (_, _, constrs) = the (assoc (descr', i));
|
|
212 |
fun arg_nonempty (DtRec i) = if i mem is then false
|
|
213 |
else is_nonempty_dt (i::is) i
|
|
214 |
| arg_nonempty _ = true;
|
|
215 |
in exists ((forall arg_nonempty) o snd) constrs
|
|
216 |
end
|
|
217 |
in assert_all (fn (i, _) => is_nonempty_dt [i] i) (hd descr)
|
|
218 |
(fn (_, (s, _, _)) => "Nonemptiness check failed for datatype " ^ s)
|
|
219 |
end;
|
|
220 |
|
|
221 |
(* unfold a list of mutually recursive datatype specifications *)
|
|
222 |
(* all types of the form DtType (dt_name, [..., DtRec _, ...]) *)
|
|
223 |
(* need to be unfolded *)
|
|
224 |
|
|
225 |
fun unfold_datatypes (dt_info : datatype_info Symtab.table) descr i =
|
|
226 |
let
|
|
227 |
fun get_dt_descr i tname dts =
|
|
228 |
(case Symtab.lookup (dt_info, tname) of
|
|
229 |
None => error (tname ^ " is not a datatype - can't use it in\
|
|
230 |
\ indirect recursion")
|
|
231 |
| (Some {index, descr, ...}) =>
|
|
232 |
let val (_, vars, _) = the (assoc (descr, index));
|
|
233 |
val subst = ((map dest_DtTFree vars) ~~ dts) handle _ =>
|
|
234 |
error ("Type constructor " ^ tname ^ " used with wrong\
|
|
235 |
\ number of arguments")
|
|
236 |
in (i + index, map (fn (j, (tn, args, cs)) => (i + j,
|
|
237 |
(tn, map (subst_DtTFree i subst) args,
|
|
238 |
map (apsnd (map (subst_DtTFree i subst))) cs))) descr)
|
|
239 |
end);
|
|
240 |
|
|
241 |
(* unfold a single constructor argument *)
|
|
242 |
|
|
243 |
fun unfold_arg ((i, Ts, descrs), T as (DtType (tname, dts))) =
|
|
244 |
if is_rec_type T then
|
|
245 |
let val (index, descr) = get_dt_descr i tname dts;
|
|
246 |
val (descr', i') = unfold_datatypes dt_info descr (i + length descr)
|
|
247 |
in (i', Ts @ [DtRec index], descrs @ descr') end
|
|
248 |
else (i, Ts @ [T], descrs)
|
|
249 |
| unfold_arg ((i, Ts, descrs), T) = (i, Ts @ [T], descrs);
|
|
250 |
|
|
251 |
(* unfold a constructor *)
|
|
252 |
|
|
253 |
fun unfold_constr ((i, constrs, descrs), (cname, cargs)) =
|
|
254 |
let val (i', cargs', descrs') = foldl unfold_arg ((i, [], descrs), cargs)
|
|
255 |
in (i', constrs @ [(cname, cargs')], descrs') end;
|
|
256 |
|
|
257 |
(* unfold a single datatype *)
|
|
258 |
|
|
259 |
fun unfold_datatype ((i, dtypes, descrs), (j, (tname, tvars, constrs))) =
|
|
260 |
let val (i', constrs', descrs') =
|
|
261 |
foldl unfold_constr ((i, [], descrs), constrs)
|
|
262 |
in (i', dtypes @ [(j, (tname, tvars, constrs'))], descrs')
|
|
263 |
end;
|
|
264 |
|
|
265 |
val (i', descr', descrs) = foldl unfold_datatype ((i, [],[]), descr);
|
|
266 |
|
|
267 |
in (descr' :: descrs, i') end;
|
|
268 |
|
|
269 |
end;
|