author | wenzelm |
Sun, 12 Sep 2010 19:04:02 +0200 | |
changeset 39288 | f1ae2493d93f |
parent 37781 | 2fbbf0a48cef |
child 39557 | fe5722fce758 |
permissions | -rw-r--r-- |
6065 | 1 |
(* Title: ZF/Tools/datatype_package.ML |
6052 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 |
Copyright 1994 University of Cambridge |
|
4 |
||
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
5 |
Datatype/Codatatype Definitions. |
6052 | 6 |
|
7 |
The functor will be instantiated for normal sums/products (datatype defs) |
|
8 |
and non-standard sums/products (codatatype defs) |
|
9 |
||
10 |
Sums are used only for mutual recursion; |
|
11 |
Products are used only to derive "streamlined" induction rules for relations |
|
12 |
*) |
|
13 |
||
14 |
type datatype_result = |
|
15 |
{con_defs : thm list, (*definitions made in thy*) |
|
16 |
case_eqns : thm list, (*equations for case operator*) |
|
17 |
recursor_eqns : thm list, (*equations for the recursor*) |
|
18 |
free_iffs : thm list, (*freeness rewrite rules*) |
|
19 |
free_SEs : thm list, (*freeness destruct rules*) |
|
6112 | 20 |
mk_free : string -> thm}; (*function to make freeness theorems*) |
6052 | 21 |
|
22 |
signature DATATYPE_ARG = |
|
12183 | 23 |
sig |
6052 | 24 |
val intrs : thm list |
25 |
val elims : thm list |
|
12183 | 26 |
end; |
6052 | 27 |
|
28 |
signature DATATYPE_PACKAGE = |
|
12131 | 29 |
sig |
6052 | 30 |
(*Insert definitions for the recursive sets, which |
31 |
must *already* be declared as constants in parent theory!*) |
|
12183 | 32 |
val add_datatype_i: term * term list -> Ind_Syntax.constructor_spec list list -> |
33 |
thm list * thm list * thm list -> theory -> theory * inductive_result * datatype_result |
|
34 |
val add_datatype: string * string list -> (string * string list * mixfix) list list -> |
|
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26190
diff
changeset
|
35 |
(Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list * |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26190
diff
changeset
|
36 |
(Facts.ref * Attrib.src list) list -> theory -> theory * inductive_result * datatype_result |
12131 | 37 |
end; |
6052 | 38 |
|
12131 | 39 |
functor Add_datatype_def_Fun |
12183 | 40 |
(structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU |
41 |
and Ind_Package : INDUCTIVE_PACKAGE |
|
42 |
and Datatype_Arg : DATATYPE_ARG |
|
43 |
val coind : bool): DATATYPE_PACKAGE = |
|
6052 | 44 |
struct |
45 |
||
12183 | 46 |
(*con_ty_lists specifies the constructors in the form (name, prems, mixfix) *) |
6052 | 47 |
|
26189 | 48 |
(*univ or quniv constitutes the sum domain for mutual recursion; |
49 |
it is applied to the datatype parameters and to Consts occurring in the |
|
50 |
definition other than Nat.nat and the datatype sets themselves. |
|
51 |
FIXME: could insert all constant set expressions, e.g. nat->nat.*) |
|
52 |
fun data_domain co (rec_tms, con_ty_lists) = |
|
53 |
let val rec_hds = map head_of rec_tms |
|
54 |
val dummy = assert_all is_Const rec_hds |
|
55 |
(fn t => "Datatype set not previously declared as constant: " ^ |
|
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26336
diff
changeset
|
56 |
Syntax.string_of_term_global @{theory IFOL} t); |
26189 | 57 |
val rec_names = (*nat doesn't have to be added*) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
58 |
@{const_name nat} :: map (#1 o dest_Const) rec_hds |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
59 |
val u = if co then @{const QUniv.quniv} else @{const Univ.univ} |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32957
diff
changeset
|
60 |
val cs = (fold o fold) (fn (_, _, _, prems) => prems |> (fold o fold_aterms) |
36692
54b64d4ad524
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36610
diff
changeset
|
61 |
(fn t as Const (a, _) => if member (op =) rec_names a then I else insert (op =) t |
26189 | 62 |
| _ => I)) con_ty_lists []; |
63 |
in u $ Ind_Syntax.union_params (hd rec_tms, cs) end; |
|
64 |
||
12183 | 65 |
fun add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims) thy = |
6052 | 66 |
let |
67 |
val dummy = (*has essential ancestors?*) |
|
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
25985
diff
changeset
|
68 |
Theory.requires thy "Datatype_ZF" "(co)datatype definitions"; |
6052 | 69 |
|
13150
0c50d13d449a
better error messages for datatypes not declared Const
paulson
parents:
12876
diff
changeset
|
70 |
val rec_hds = map head_of rec_tms; |
0c50d13d449a
better error messages for datatypes not declared Const
paulson
parents:
12876
diff
changeset
|
71 |
|
0c50d13d449a
better error messages for datatypes not declared Const
paulson
parents:
12876
diff
changeset
|
72 |
val dummy = assert_all is_Const rec_hds |
0c50d13d449a
better error messages for datatypes not declared Const
paulson
parents:
12876
diff
changeset
|
73 |
(fn t => "Datatype set not previously declared as constant: " ^ |
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26336
diff
changeset
|
74 |
Syntax.string_of_term_global thy t); |
13150
0c50d13d449a
better error messages for datatypes not declared Const
paulson
parents:
12876
diff
changeset
|
75 |
|
0c50d13d449a
better error messages for datatypes not declared Const
paulson
parents:
12876
diff
changeset
|
76 |
val rec_names = map (#1 o dest_Const) rec_hds |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30345
diff
changeset
|
77 |
val rec_base_names = map Long_Name.base_name rec_names |
6052 | 78 |
val big_rec_base_name = space_implode "_" rec_base_names |
79 |
||
24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24707
diff
changeset
|
80 |
val thy_path = thy |> Sign.add_path big_rec_base_name |
6052 | 81 |
|
22578 | 82 |
val big_rec_name = Sign.intern_const thy_path big_rec_base_name; |
6052 | 83 |
|
22578 | 84 |
val intr_tms = Ind_Syntax.mk_all_intr_tms thy_path (rec_tms, con_ty_lists); |
6052 | 85 |
|
12131 | 86 |
val dummy = |
12243 | 87 |
writeln ((if coind then "Codatatype" else "Datatype") ^ " definition " ^ quote big_rec_name); |
6052 | 88 |
|
89 |
val case_varname = "f"; (*name for case variables*) |
|
90 |
||
91 |
(** Define the constructors **) |
|
92 |
||
93 |
(*The empty tuple is 0*) |
|
26190 | 94 |
fun mk_tuple [] = @{const "0"} |
7696 | 95 |
| mk_tuple args = foldr1 (fn (t1, t2) => Pr.pair $ t1 $ t2) args; |
6052 | 96 |
|
32765 | 97 |
fun mk_inject n k u = Balanced_Tree.access |
23419 | 98 |
{left = fn t => Su.inl $ t, right = fn t => Su.inr $ t, init = u} n k; |
6052 | 99 |
|
100 |
val npart = length rec_names; (*number of mutually recursive parts*) |
|
101 |
||
102 |
||
28965 | 103 |
val full_name = Sign.full_bname thy_path; |
6052 | 104 |
|
12131 | 105 |
(*Make constructor definition; |
6052 | 106 |
kpart is the number of this mutually recursive part*) |
12131 | 107 |
fun mk_con_defs (kpart, con_ty_list) = |
6052 | 108 |
let val ncon = length con_ty_list (*number of constructors*) |
12131 | 109 |
fun mk_def (((id,T,syn), name, args, prems), kcon) = |
110 |
(*kcon is index of constructor*) |
|
37781
2fbbf0a48cef
moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
37145
diff
changeset
|
111 |
Misc_Legacy.mk_defpair (list_comb (Const (full_name name, T), args), |
12131 | 112 |
mk_inject npart kpart |
113 |
(mk_inject ncon kcon (mk_tuple args))) |
|
6052 | 114 |
in ListPair.map mk_def (con_ty_list, 1 upto ncon) end; |
115 |
||
116 |
||
117 |
(*** Define the case operator ***) |
|
118 |
||
119 |
(*Combine split terms using case; yields the case operator for one part*) |
|
12131 | 120 |
fun call_case case_list = |
26190 | 121 |
let fun call_f (free,[]) = Abs("null", @{typ i}, free) |
12131 | 122 |
| call_f (free,args) = |
123 |
CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args)) |
|
26190 | 124 |
@{typ i} |
12131 | 125 |
free |
32765 | 126 |
in Balanced_Tree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_f case_list) end; |
6052 | 127 |
|
128 |
(** Generating function variables for the case definition |
|
129 |
Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **) |
|
130 |
||
131 |
(*The function variable for a single constructor*) |
|
33339 | 132 |
fun add_case ((_, T, _), name, args, _) (opno, cases) = |
6052 | 133 |
if Syntax.is_identifier name then |
134 |
(opno, (Free (case_varname ^ "_" ^ name, T), args) :: cases) |
|
135 |
else |
|
12131 | 136 |
(opno + 1, (Free (case_varname ^ "_op_" ^ string_of_int opno, T), args) |
6052 | 137 |
:: cases); |
138 |
||
139 |
(*Treatment of a list of constructors, for one part |
|
140 |
Result adds a list of terms, each a function variable with arguments*) |
|
33339 | 141 |
fun add_case_list con_ty_list (opno, case_lists) = |
142 |
let val (opno', case_list) = fold_rev add_case con_ty_list (opno, []) |
|
6052 | 143 |
in (opno', case_list :: case_lists) end; |
144 |
||
145 |
(*Treatment of all parts*) |
|
33339 | 146 |
val (_, case_lists) = fold_rev add_case_list con_ty_lists (1, []); |
6052 | 147 |
|
148 |
(*extract the types of all the variables*) |
|
32952 | 149 |
val case_typ = maps (map (#2 o #1)) con_ty_lists ---> @{typ "i => i"}; |
6052 | 150 |
|
151 |
val case_base_name = big_rec_base_name ^ "_case"; |
|
152 |
val case_name = full_name case_base_name; |
|
153 |
||
154 |
(*The list of all the function variables*) |
|
32952 | 155 |
val case_args = maps (map #1) case_lists; |
6052 | 156 |
|
12131 | 157 |
val case_const = Const (case_name, case_typ); |
6052 | 158 |
val case_tm = list_comb (case_const, case_args); |
159 |
||
37781
2fbbf0a48cef
moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
37145
diff
changeset
|
160 |
val case_def = Misc_Legacy.mk_defpair |
32765 | 161 |
(case_tm, Balanced_Tree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_case case_lists)); |
6052 | 162 |
|
163 |
||
164 |
(** Generating function variables for the recursor definition |
|
165 |
Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **) |
|
166 |
||
167 |
(*a recursive call for x is the application rec`x *) |
|
26190 | 168 |
val rec_call = @{const apply} $ Free ("rec", @{typ i}); |
6052 | 169 |
|
12131 | 170 |
(*look back down the "case args" (which have been reversed) to |
6052 | 171 |
determine the de Bruijn index*) |
172 |
fun make_rec_call ([], _) arg = error |
|
12131 | 173 |
"Internal error in datatype (variable name mismatch)" |
174 |
| make_rec_call (a::args, i) arg = |
|
175 |
if a = arg then rec_call $ Bound i |
|
176 |
else make_rec_call (args, i+1) arg; |
|
6052 | 177 |
|
178 |
(*creates one case of the "X_case" definition of the recursor*) |
|
12131 | 179 |
fun call_recursor ((case_var, case_args), (recursor_var, recursor_args)) = |
6052 | 180 |
let fun add_abs (Free(a,T), u) = Abs(a,T,u) |
12131 | 181 |
val ncase_args = length case_args |
182 |
val bound_args = map Bound ((ncase_args - 1) downto 0) |
|
183 |
val rec_args = map (make_rec_call (rev case_args,0)) |
|
184 |
(List.drop(recursor_args, ncase_args)) |
|
6052 | 185 |
in |
30190 | 186 |
List.foldr add_abs |
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
187 |
(list_comb (recursor_var, |
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
188 |
bound_args @ rec_args)) case_args |
6052 | 189 |
end |
190 |
||
191 |
(*Find each recursive argument and add a recursive call for it*) |
|
192 |
fun rec_args [] = [] |
|
24826 | 193 |
| rec_args ((Const(@{const_name mem},_)$arg$X)::prems) = |
6052 | 194 |
(case head_of X of |
12131 | 195 |
Const(a,_) => (*recursive occurrence?*) |
36692
54b64d4ad524
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36610
diff
changeset
|
196 |
if member (op =) rec_names a |
12131 | 197 |
then arg :: rec_args prems |
198 |
else rec_args prems |
|
199 |
| _ => rec_args prems) |
|
200 |
| rec_args (_::prems) = rec_args prems; |
|
6052 | 201 |
|
202 |
(*Add an argument position for each occurrence of a recursive set. |
|
203 |
Strictly speaking, the recursive arguments are the LAST of the function |
|
204 |
variable, but they all have type "i" anyway*) |
|
26190 | 205 |
fun add_rec_args args' T = (map (fn _ => @{typ i}) args') ---> T |
6052 | 206 |
|
207 |
(*Plug in the function variable type needed for the recursor |
|
208 |
as well as the new arguments (recursive calls)*) |
|
209 |
fun rec_ty_elem ((id, T, syn), name, args, prems) = |
|
12131 | 210 |
let val args' = rec_args prems |
211 |
in ((id, add_rec_args args' T, syn), |
|
212 |
name, args @ args', prems) |
|
6052 | 213 |
end; |
214 |
||
12131 | 215 |
val rec_ty_lists = (map (map rec_ty_elem) con_ty_lists); |
6052 | 216 |
|
217 |
(*Treatment of all parts*) |
|
33339 | 218 |
val (_, recursor_lists) = fold_rev add_case_list rec_ty_lists (1, []); |
6052 | 219 |
|
220 |
(*extract the types of all the variables*) |
|
32952 | 221 |
val recursor_typ = maps (map (#2 o #1)) rec_ty_lists ---> @{typ "i => i"}; |
6052 | 222 |
|
223 |
val recursor_base_name = big_rec_base_name ^ "_rec"; |
|
224 |
val recursor_name = full_name recursor_base_name; |
|
225 |
||
226 |
(*The list of all the function variables*) |
|
32952 | 227 |
val recursor_args = maps (map #1) recursor_lists; |
6052 | 228 |
|
229 |
val recursor_tm = |
|
12131 | 230 |
list_comb (Const (recursor_name, recursor_typ), recursor_args); |
6052 | 231 |
|
32952 | 232 |
val recursor_cases = map call_recursor (flat case_lists ~~ flat recursor_lists); |
6052 | 233 |
|
12131 | 234 |
val recursor_def = |
37781
2fbbf0a48cef
moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
37145
diff
changeset
|
235 |
Misc_Legacy.mk_defpair |
12131 | 236 |
(recursor_tm, |
26189 | 237 |
@{const Univ.Vrecursor} $ |
26190 | 238 |
absfree ("rec", @{typ i}, list_comb (case_const, recursor_cases))); |
6052 | 239 |
|
240 |
(* Build the new theory *) |
|
241 |
||
12183 | 242 |
val need_recursor = (not coind andalso recursor_typ <> case_typ); |
6052 | 243 |
|
12131 | 244 |
fun add_recursor thy = |
6052 | 245 |
if need_recursor then |
24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24707
diff
changeset
|
246 |
thy |> Sign.add_consts_i |
30345 | 247 |
[(Binding.name recursor_base_name, recursor_typ, NoSyn)] |
29579 | 248 |
|> (snd o PureThy.add_defs false [(Thm.no_attributes o apfst Binding.name) recursor_def]) |
6052 | 249 |
else thy; |
250 |
||
18358 | 251 |
val (con_defs, thy0) = thy_path |
24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24707
diff
changeset
|
252 |
|> Sign.add_consts_i |
30345 | 253 |
(map (fn (c, T, mx) => (Binding.name c, T, mx)) |
32952 | 254 |
((case_base_name, case_typ, NoSyn) :: map #1 (flat con_ty_lists))) |
27691
ce171cbd4b93
PureThy: dropped note_thmss_qualified, dropped _i suffix
haftmann
parents:
27261
diff
changeset
|
255 |
|> PureThy.add_defs false |
29579 | 256 |
(map (Thm.no_attributes o apfst Binding.name) |
12131 | 257 |
(case_def :: |
32952 | 258 |
flat (ListPair.map mk_con_defs (1 upto npart, con_ty_lists)))) |
18358 | 259 |
||> add_recursor |
24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24707
diff
changeset
|
260 |
||> Sign.parent_path |
6052 | 261 |
|
32952 | 262 |
val intr_names = map (Binding.name o #2) (flat con_ty_lists); |
12131 | 263 |
val (thy1, ind_result) = |
12187 | 264 |
thy0 |> Ind_Package.add_inductive_i |
265 |
false (rec_tms, dom_sum) (map Thm.no_attributes (intr_names ~~ intr_tms)) |
|
266 |
(monos, con_defs, type_intrs @ Datatype_Arg.intrs, type_elims @ Datatype_Arg.elims); |
|
6052 | 267 |
|
268 |
(**** Now prove the datatype theorems in this theory ****) |
|
269 |
||
270 |
||
271 |
(*** Prove the case theorems ***) |
|
272 |
||
12131 | 273 |
(*Each equation has the form |
6052 | 274 |
case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *) |
12131 | 275 |
fun mk_case_eqn (((_,T,_), name, args, _), case_free) = |
6052 | 276 |
FOLogic.mk_Trueprop |
277 |
(FOLogic.mk_eq |
|
278 |
(case_tm $ |
|
22578 | 279 |
(list_comb (Const (Sign.intern_const thy1 name,T), |
12131 | 280 |
args)), |
281 |
list_comb (case_free, args))); |
|
6052 | 282 |
|
26189 | 283 |
val case_trans = hd con_defs RS @{thm def_trans} |
35409 | 284 |
and split_trans = Pr.split_eq RS @{thm meta_eq_to_obj_eq} RS @{thm trans}; |
6052 | 285 |
|
17985 | 286 |
fun prove_case_eqn (arg, con_def) = |
20046 | 287 |
Goal.prove_global thy1 [] [] |
17985 | 288 |
(Ind_Syntax.traceIt "next case equation = " thy1 (mk_case_eqn arg)) |
289 |
(*Proves a single case equation. Could use simp_tac, but it's slower!*) |
|
290 |
(fn _ => EVERY |
|
28839
32d498cf7595
eliminated rewrite_tac/fold_tac, which are not well-formed tactics due to change of main conclusion;
wenzelm
parents:
28678
diff
changeset
|
291 |
[rewrite_goals_tac [con_def], |
17985 | 292 |
rtac case_trans 1, |
35409 | 293 |
REPEAT |
294 |
(resolve_tac [@{thm refl}, split_trans, |
|
295 |
Su.case_inl RS @{thm trans}, Su.case_inr RS @{thm trans}] 1)]); |
|
6052 | 296 |
|
35021
c839a4c670c6
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33385
diff
changeset
|
297 |
val free_iffs = map Drule.export_without_context (con_defs RL [@{thm def_swap_iff}]); |
6052 | 298 |
|
32952 | 299 |
val case_eqns = map prove_case_eqn (flat con_ty_lists ~~ case_args ~~ tl con_defs); |
6052 | 300 |
|
301 |
(*** Prove the recursor theorems ***) |
|
302 |
||
37781
2fbbf0a48cef
moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
37145
diff
changeset
|
303 |
val recursor_eqns = case try (Misc_Legacy.get_def thy1) recursor_base_name of |
15531 | 304 |
NONE => (writeln " [ No recursion operator ]"; |
12131 | 305 |
[]) |
15531 | 306 |
| SOME recursor_def => |
6052 | 307 |
let |
12131 | 308 |
(*Replace subterms rec`x (where rec is a Free var) by recursor_tm(x) *) |
24826 | 309 |
fun subst_rec (Const(@{const_name apply},_) $ Free _ $ arg) = recursor_tm $ arg |
12131 | 310 |
| subst_rec tm = |
311 |
let val (head, args) = strip_comb tm |
|
312 |
in list_comb (head, map subst_rec args) end; |
|
6052 | 313 |
|
12131 | 314 |
(*Each equation has the form |
315 |
REC(coni(args)) = f_coni(args, REC(rec_arg), ...) |
|
316 |
where REC = recursor(f_con1,...,f_conn) and rec_arg is a recursive |
|
317 |
constructor argument.*) |
|
318 |
fun mk_recursor_eqn (((_,T,_), name, args, _), recursor_case) = |
|
319 |
FOLogic.mk_Trueprop |
|
320 |
(FOLogic.mk_eq |
|
321 |
(recursor_tm $ |
|
22578 | 322 |
(list_comb (Const (Sign.intern_const thy1 name,T), |
12131 | 323 |
args)), |
18185 | 324 |
subst_rec (Term.betapplys (recursor_case, args)))); |
6052 | 325 |
|
35409 | 326 |
val recursor_trans = recursor_def RS @{thm def_Vrecursor} RS @{thm trans}; |
6052 | 327 |
|
12131 | 328 |
fun prove_recursor_eqn arg = |
20046 | 329 |
Goal.prove_global thy1 [] [] |
17985 | 330 |
(Ind_Syntax.traceIt "next recursor equation = " thy1 (mk_recursor_eqn arg)) |
331 |
(*Proves a single recursor equation.*) |
|
332 |
(fn _ => EVERY |
|
333 |
[rtac recursor_trans 1, |
|
334 |
simp_tac (rank_ss addsimps case_eqns) 1, |
|
20046 | 335 |
IF_UNSOLVED (simp_tac (rank_ss addsimps tl con_defs) 1)]); |
6052 | 336 |
in |
32952 | 337 |
map prove_recursor_eqn (flat con_ty_lists ~~ recursor_cases) |
6052 | 338 |
end |
339 |
||
340 |
val constructors = |
|
341 |
map (head_of o #1 o Logic.dest_equals o #prop o rep_thm) (tl con_defs); |
|
342 |
||
35021
c839a4c670c6
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33385
diff
changeset
|
343 |
val free_SEs = map Drule.export_without_context (Ind_Syntax.mk_free_SEs free_iffs); |
6052 | 344 |
|
6154
6a00a5baef2b
automatic insertion of datatype intr rules into claset
paulson
parents:
6141
diff
changeset
|
345 |
val {intrs, elim, induct, mutual_induct, ...} = ind_result |
6052 | 346 |
|
347 |
(*Typical theorems have the form ~con1=con2, con1=con2==>False, |
|
348 |
con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc. *) |
|
349 |
fun mk_free s = |
|
17985 | 350 |
let val thy = theory_of_thm elim in (*Don't use thy1: it will be stale*) |
24707 | 351 |
Goal.prove_global thy [] [] (Syntax.read_prop_global thy s) |
17985 | 352 |
(fn _ => EVERY |
353 |
[rewrite_goals_tac con_defs, |
|
20046 | 354 |
fast_tac (ZF_cs addSEs free_SEs @ Su.free_SEs) 1]) |
17985 | 355 |
end; |
6052 | 356 |
|
357 |
val simps = case_eqns @ recursor_eqns; |
|
358 |
||
359 |
val dt_info = |
|
12131 | 360 |
{inductive = true, |
361 |
constructors = constructors, |
|
362 |
rec_rewrites = recursor_eqns, |
|
363 |
case_rewrites = case_eqns, |
|
364 |
induct = induct, |
|
365 |
mutual_induct = mutual_induct, |
|
366 |
exhaustion = elim}; |
|
6052 | 367 |
|
368 |
val con_info = |
|
369 |
{big_rec_name = big_rec_name, |
|
12131 | 370 |
constructors = constructors, |
6052 | 371 |
(*let primrec handle definition by cases*) |
12131 | 372 |
free_iffs = free_iffs, |
373 |
rec_rewrites = (case recursor_eqns of |
|
374 |
[] => case_eqns | _ => recursor_eqns)}; |
|
6052 | 375 |
|
376 |
(*associate with each constructor the datatype name and rewrites*) |
|
377 |
val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors |
|
378 |
||
379 |
in |
|
380 |
(*Updating theory components: simprules and datatype info*) |
|
24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24707
diff
changeset
|
381 |
(thy1 |> Sign.add_path big_rec_base_name |
18377 | 382 |
|> PureThy.add_thmss |
29579 | 383 |
[((Binding.name "simps", simps), [Simplifier.simp_add]), |
384 |
((Binding.empty , intrs), [Classical.safe_intro NONE]), |
|
385 |
((Binding.name "con_defs", con_defs), []), |
|
386 |
((Binding.name "case_eqns", case_eqns), []), |
|
387 |
((Binding.name "recursor_eqns", recursor_eqns), []), |
|
388 |
((Binding.name "free_iffs", free_iffs), []), |
|
389 |
((Binding.name "free_elims", free_SEs), [])] |> snd |
|
17412 | 390 |
|> DatatypesData.map (Symtab.update (big_rec_name, dt_info)) |
391 |
|> ConstructorsData.map (fold Symtab.update con_pairs) |
|
24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24707
diff
changeset
|
392 |
|> Sign.parent_path, |
6052 | 393 |
ind_result, |
394 |
{con_defs = con_defs, |
|
395 |
case_eqns = case_eqns, |
|
396 |
recursor_eqns = recursor_eqns, |
|
397 |
free_iffs = free_iffs, |
|
398 |
free_SEs = free_SEs, |
|
399 |
mk_free = mk_free}) |
|
400 |
end; |
|
401 |
||
17936 | 402 |
fun add_datatype (sdom, srec_tms) scon_ty_lists (raw_monos, raw_type_intrs, raw_type_elims) thy = |
12183 | 403 |
let |
36610
bafd82950e24
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents:
35989
diff
changeset
|
404 |
val ctxt = ProofContext.init_global thy; |
27261
5b3101338f42
eliminated old Sign.read_term/Thm.read_cterm etc.;
wenzelm
parents:
26939
diff
changeset
|
405 |
fun read_is strs = |
39288 | 406 |
map (Syntax.parse_term ctxt #> Type.constraint @{typ i}) strs |
27261
5b3101338f42
eliminated old Sign.read_term/Thm.read_cterm etc.;
wenzelm
parents:
26939
diff
changeset
|
407 |
|> Syntax.check_terms ctxt; |
5b3101338f42
eliminated old Sign.read_term/Thm.read_cterm etc.;
wenzelm
parents:
26939
diff
changeset
|
408 |
|
5b3101338f42
eliminated old Sign.read_term/Thm.read_cterm etc.;
wenzelm
parents:
26939
diff
changeset
|
409 |
val rec_tms = read_is srec_tms; |
5b3101338f42
eliminated old Sign.read_term/Thm.read_cterm etc.;
wenzelm
parents:
26939
diff
changeset
|
410 |
val con_ty_lists = Ind_Syntax.read_constructs ctxt scon_ty_lists; |
12183 | 411 |
val dom_sum = |
26189 | 412 |
if sdom = "" then data_domain coind (rec_tms, con_ty_lists) |
27261
5b3101338f42
eliminated old Sign.read_term/Thm.read_cterm etc.;
wenzelm
parents:
26939
diff
changeset
|
413 |
else singleton read_is sdom; |
24725 | 414 |
val monos = Attrib.eval_thms ctxt raw_monos; |
415 |
val type_intrs = Attrib.eval_thms ctxt raw_type_intrs; |
|
416 |
val type_elims = Attrib.eval_thms ctxt raw_type_elims; |
|
417 |
in add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims) thy end; |
|
418 |
||
12183 | 419 |
|
420 |
(* outer syntax *) |
|
421 |
||
422 |
fun mk_datatype ((((dom, dts), monos), type_intrs), type_elims) = |
|
423 |
#1 o add_datatype (dom, map fst dts) (map snd dts) (monos, type_intrs, type_elims); |
|
424 |
||
425 |
val con_decl = |
|
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
426 |
Parse.name -- Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.term --| Parse.$$$ ")") [] -- |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
427 |
Parse.opt_mixfix >> Parse.triple1; |
12183 | 428 |
|
429 |
val datatype_decl = |
|
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
430 |
(Scan.optional ((Parse.$$$ "\<subseteq>" || Parse.$$$ "<=") |-- Parse.!!! Parse.term) "") -- |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
431 |
Parse.and_list1 (Parse.term -- (Parse.$$$ "=" |-- Parse.enum1 "|" con_decl)) -- |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
432 |
Scan.optional (Parse.$$$ "monos" |-- Parse.!!! Parse_Spec.xthms1) [] -- |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
433 |
Scan.optional (Parse.$$$ "type_intros" |-- Parse.!!! Parse_Spec.xthms1) [] -- |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
434 |
Scan.optional (Parse.$$$ "type_elims" |-- Parse.!!! Parse_Spec.xthms1) [] |
12183 | 435 |
>> (Toplevel.theory o mk_datatype); |
436 |
||
437 |
val coind_prefix = if coind then "co" else ""; |
|
438 |
||
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
439 |
val _ = |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
440 |
Outer_Syntax.command (coind_prefix ^ "datatype") |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
441 |
("define " ^ coind_prefix ^ "datatype") Keyword.thy_decl datatype_decl; |
12183 | 442 |
|
6052 | 443 |
end; |
12183 | 444 |