author  wenzelm 
Wed, 14 Nov 2001 18:46:30 +0100  
changeset 12183  c10cea75dd56 
parent 12131  673bc8469a08 
child 12187  a1000fcf636e 
permissions  rwrr 
6065  1 
(* Title: ZF/Tools/datatype_package.ML 
6052  2 
ID: $Id$ 
3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1994 University of Cambridge 

5 

6065  6 
Datatype/Codatatype Definitions 
6052  7 

8 
The functor will be instantiated for normal sums/products (datatype defs) 

9 
and nonstandard sums/products (codatatype defs) 

10 

11 
Sums are used only for mutual recursion; 

12 
Products are used only to derive "streamlined" induction rules for relations 

13 
*) 

14 

15 
type datatype_result = 

16 
{con_defs : thm list, (*definitions made in thy*) 

17 
case_eqns : thm list, (*equations for case operator*) 

18 
recursor_eqns : thm list, (*equations for the recursor*) 

19 
free_iffs : thm list, (*freeness rewrite rules*) 

20 
free_SEs : thm list, (*freeness destruct rules*) 

6112  21 
mk_free : string > thm}; (*function to make freeness theorems*) 
6052  22 

23 
signature DATATYPE_ARG = 

12183  24 
sig 
6052  25 
val intrs : thm list 
26 
val elims : thm list 

12183  27 
end; 
6052  28 

29 
(*Functor's result signature*) 

30 
signature DATATYPE_PACKAGE = 

12131  31 
sig 
6052  32 
(*Insert definitions for the recursive sets, which 
33 
must *already* be declared as constants in parent theory!*) 

12183  34 
val add_datatype_i: term * term list > Ind_Syntax.constructor_spec list list > 
35 
thm list * thm list * thm list > theory > theory * inductive_result * datatype_result 

36 
val add_datatype_x: string * string list > (string * string list * mixfix) list list > 

37 
thm list * thm list * thm list > theory > theory * inductive_result * datatype_result 

38 
val add_datatype: string * string list > (string * string list * mixfix) list list > 

39 
(xstring * Args.src list) list * (xstring * Args.src list) list * 

40 
(xstring * Args.src list) list > theory > theory * inductive_result * datatype_result 

12131  41 
end; 
6052  42 

12131  43 
functor Add_datatype_def_Fun 
12183  44 
(structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU 
45 
and Ind_Package : INDUCTIVE_PACKAGE 

46 
and Datatype_Arg : DATATYPE_ARG 

47 
val coind : bool): DATATYPE_PACKAGE = 

6052  48 
struct 
49 

12183  50 
(*con_ty_lists specifies the constructors in the form (name, prems, mixfix) *) 
6052  51 

12183  52 
fun add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims) thy = 
6052  53 
let 
54 
val dummy = (*has essential ancestors?*) 

55 
Theory.requires thy "Datatype" "(co)datatype definitions"; 

56 

57 
val rec_names = map (#1 o dest_Const o head_of) rec_tms 

58 
val rec_base_names = map Sign.base_name rec_names 

59 
val big_rec_base_name = space_implode "_" rec_base_names 

60 

61 
val thy_path = thy > Theory.add_path big_rec_base_name 

62 
val sign = sign_of thy_path 

63 

64 
val big_rec_name = Sign.intern_const sign big_rec_base_name; 

65 

12131  66 
val intr_tms = Ind_Syntax.mk_all_intr_tms sign (rec_tms, con_ty_lists); 
6052  67 

12131  68 
val dummy = 
12183  69 
writeln ((if coind then "Codatatype" else "Datatype") ^ " definition " ^ big_rec_name); 
6052  70 

71 
val case_varname = "f"; (*name for case variables*) 

72 

73 
(** Define the constructors **) 

74 

75 
(*The empty tuple is 0*) 

76 
fun mk_tuple [] = Const("0",iT) 

7696  77 
 mk_tuple args = foldr1 (fn (t1, t2) => Pr.pair $ t1 $ t2) args; 
6052  78 

7696  79 
fun mk_inject n k u = access_bal (fn t => Su.inl $ t, fn t => Su.inr $ t, u) n k; 
6052  80 

81 
val npart = length rec_names; (*number of mutually recursive parts*) 

82 

83 

84 
val full_name = Sign.full_name sign; 

85 

12131  86 
(*Make constructor definition; 
6052  87 
kpart is the number of this mutually recursive part*) 
12131  88 
fun mk_con_defs (kpart, con_ty_list) = 
6052  89 
let val ncon = length con_ty_list (*number of constructors*) 
12131  90 
fun mk_def (((id,T,syn), name, args, prems), kcon) = 
91 
(*kcon is index of constructor*) 

92 
Logic.mk_defpair (list_comb (Const (full_name name, T), args), 

93 
mk_inject npart kpart 

94 
(mk_inject ncon kcon (mk_tuple args))) 

6052  95 
in ListPair.map mk_def (con_ty_list, 1 upto ncon) end; 
96 

97 

98 
(*** Define the case operator ***) 

99 

100 
(*Combine split terms using case; yields the case operator for one part*) 

12131  101 
fun call_case case_list = 
6052  102 
let fun call_f (free,[]) = Abs("null", iT, free) 
12131  103 
 call_f (free,args) = 
104 
CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args)) 

105 
Ind_Syntax.iT 

106 
free 

7696  107 
in fold_bal (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_f case_list) end; 
6052  108 

109 
(** Generating function variables for the case definition 

110 
Nonidentifiers (e.g. infixes) get a name of the form f_op_nnn. **) 

111 

112 
(*The function variable for a single constructor*) 

113 
fun add_case (((_, T, _), name, args, _), (opno, cases)) = 

114 
if Syntax.is_identifier name then 

115 
(opno, (Free (case_varname ^ "_" ^ name, T), args) :: cases) 

116 
else 

12131  117 
(opno + 1, (Free (case_varname ^ "_op_" ^ string_of_int opno, T), args) 
6052  118 
:: cases); 
119 

120 
(*Treatment of a list of constructors, for one part 

121 
Result adds a list of terms, each a function variable with arguments*) 

122 
fun add_case_list (con_ty_list, (opno, case_lists)) = 

123 
let val (opno', case_list) = foldr add_case (con_ty_list, (opno, [])) 

124 
in (opno', case_list :: case_lists) end; 

125 

126 
(*Treatment of all parts*) 

127 
val (_, case_lists) = foldr add_case_list (con_ty_lists, (1,[])); 

128 

129 
(*extract the types of all the variables*) 

130 
val case_typ = flat (map (map (#2 o #1)) con_ty_lists) > (iT>iT); 

131 

132 
val case_base_name = big_rec_base_name ^ "_case"; 

133 
val case_name = full_name case_base_name; 

134 

135 
(*The list of all the function variables*) 

136 
val case_args = flat (map (map #1) case_lists); 

137 

12131  138 
val case_const = Const (case_name, case_typ); 
6052  139 
val case_tm = list_comb (case_const, case_args); 
140 

141 
val case_def = Logic.mk_defpair 

7696  142 
(case_tm, fold_bal (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_case case_lists)); 
6052  143 

144 

145 
(** Generating function variables for the recursor definition 

146 
Nonidentifiers (e.g. infixes) get a name of the form f_op_nnn. **) 

147 

148 
(*a recursive call for x is the application rec`x *) 

149 
val rec_call = Ind_Syntax.apply_const $ Free ("rec", iT); 

150 

12131  151 
(*look back down the "case args" (which have been reversed) to 
6052  152 
determine the de Bruijn index*) 
153 
fun make_rec_call ([], _) arg = error 

12131  154 
"Internal error in datatype (variable name mismatch)" 
155 
 make_rec_call (a::args, i) arg = 

156 
if a = arg then rec_call $ Bound i 

157 
else make_rec_call (args, i+1) arg; 

6052  158 

159 
(*creates one case of the "X_case" definition of the recursor*) 

12131  160 
fun call_recursor ((case_var, case_args), (recursor_var, recursor_args)) = 
6052  161 
let fun add_abs (Free(a,T), u) = Abs(a,T,u) 
12131  162 
val ncase_args = length case_args 
163 
val bound_args = map Bound ((ncase_args  1) downto 0) 

164 
val rec_args = map (make_rec_call (rev case_args,0)) 

165 
(List.drop(recursor_args, ncase_args)) 

6052  166 
in 
12131  167 
foldr add_abs 
168 
(case_args, list_comb (recursor_var, 

169 
bound_args @ rec_args)) 

6052  170 
end 
171 

172 
(*Find each recursive argument and add a recursive call for it*) 

173 
fun rec_args [] = [] 

174 
 rec_args ((Const("op :",_)$arg$X)::prems) = 

175 
(case head_of X of 

12131  176 
Const(a,_) => (*recursive occurrence?*) 
177 
if a mem_string rec_names 

178 
then arg :: rec_args prems 

179 
else rec_args prems 

180 
 _ => rec_args prems) 

181 
 rec_args (_::prems) = rec_args prems; 

6052  182 

183 
(*Add an argument position for each occurrence of a recursive set. 

184 
Strictly speaking, the recursive arguments are the LAST of the function 

185 
variable, but they all have type "i" anyway*) 

186 
fun add_rec_args args' T = (map (fn _ => iT) args') > T 

187 

188 
(*Plug in the function variable type needed for the recursor 

189 
as well as the new arguments (recursive calls)*) 

190 
fun rec_ty_elem ((id, T, syn), name, args, prems) = 

12131  191 
let val args' = rec_args prems 
192 
in ((id, add_rec_args args' T, syn), 

193 
name, args @ args', prems) 

6052  194 
end; 
195 

12131  196 
val rec_ty_lists = (map (map rec_ty_elem) con_ty_lists); 
6052  197 

198 
(*Treatment of all parts*) 

199 
val (_, recursor_lists) = foldr add_case_list (rec_ty_lists, (1,[])); 

200 

201 
(*extract the types of all the variables*) 

202 
val recursor_typ = flat (map (map (#2 o #1)) rec_ty_lists) 

12131  203 
> (iT>iT); 
6052  204 

205 
val recursor_base_name = big_rec_base_name ^ "_rec"; 

206 
val recursor_name = full_name recursor_base_name; 

207 

208 
(*The list of all the function variables*) 

209 
val recursor_args = flat (map (map #1) recursor_lists); 

210 

211 
val recursor_tm = 

12131  212 
list_comb (Const (recursor_name, recursor_typ), recursor_args); 
6052  213 

12131  214 
val recursor_cases = map call_recursor 
215 
(flat case_lists ~~ flat recursor_lists) 

6052  216 

12131  217 
val recursor_def = 
6052  218 
Logic.mk_defpair 
12131  219 
(recursor_tm, 
220 
Ind_Syntax.Vrecursor_const $ 

221 
absfree ("rec", iT, list_comb (case_const, recursor_cases))); 

6052  222 

223 
(* Build the new theory *) 

224 

12183  225 
val need_recursor = (not coind andalso recursor_typ <> case_typ); 
6052  226 

12131  227 
fun add_recursor thy = 
6052  228 
if need_recursor then 
12131  229 
thy > Theory.add_consts_i 
230 
[(recursor_base_name, recursor_typ, NoSyn)] 

231 
> (#1 o PureThy.add_defs_i false [Thm.no_attributes recursor_def]) 

6052  232 
else thy; 
233 

8438  234 
val (thy0, con_defs) = thy_path 
12131  235 
> Theory.add_consts_i 
236 
((case_base_name, case_typ, NoSyn) :: 

237 
map #1 (flat con_ty_lists)) 

238 
> PureThy.add_defs_i false 

239 
(map Thm.no_attributes 

240 
(case_def :: 

241 
flat (ListPair.map mk_con_defs 

242 
(1 upto npart, con_ty_lists)))) 

243 
>> add_recursor 

244 
>> Theory.parent_path 

6052  245 

12131  246 
val (thy1, ind_result) = 
6052  247 
thy0 > Ind_Package.add_inductive_i 
12131  248 
false (rec_tms, dom_sum) (map (fn tm => (("", tm), [])) intr_tms) 
249 
(monos, con_defs, 

250 
type_intrs @ Datatype_Arg.intrs, 

251 
type_elims @ Datatype_Arg.elims) 

6052  252 

253 
(**** Now prove the datatype theorems in this theory ****) 

254 

255 

256 
(*** Prove the case theorems ***) 

257 

12131  258 
(*Each equation has the form 
6052  259 
case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *) 
12131  260 
fun mk_case_eqn (((_,T,_), name, args, _), case_free) = 
6052  261 
FOLogic.mk_Trueprop 
262 
(FOLogic.mk_eq 

263 
(case_tm $ 

12131  264 
(list_comb (Const (Sign.intern_const (sign_of thy1) name,T), 
265 
args)), 

266 
list_comb (case_free, args))); 

6052  267 

268 
val case_trans = hd con_defs RS Ind_Syntax.def_trans 

269 
and split_trans = Pr.split_eq RS meta_eq_to_obj_eq RS trans; 

270 

271 
(*Proves a single case equation. Could use simp_tac, but it's slower!*) 

12131  272 
fun case_tacsf con_def _ = 
6052  273 
[rewtac con_def, 
274 
rtac case_trans 1, 

12131  275 
REPEAT (resolve_tac [refl, split_trans, 
276 
Su.case_inl RS trans, 

277 
Su.case_inr RS trans] 1)]; 

6052  278 

279 
fun prove_case_eqn (arg,con_def) = 

12131  280 
prove_goalw_cterm [] 
281 
(Ind_Syntax.traceIt "next case equation = " 

282 
(cterm_of (sign_of thy1) (mk_case_eqn arg))) 

283 
(case_tacsf con_def); 

6052  284 

6112  285 
val free_iffs = con_defs RL [Ind_Syntax.def_swap_iff]; 
6052  286 

12131  287 
val case_eqns = 
288 
map prove_case_eqn 

289 
(flat con_ty_lists ~~ case_args ~~ tl con_defs); 

6052  290 

291 
(*** Prove the recursor theorems ***) 

292 

293 
val recursor_eqns = case try (get_def thy1) recursor_base_name of 

294 
None => (writeln " [ No recursion operator ]"; 

12131  295 
[]) 
296 
 Some recursor_def => 

6052  297 
let 
12131  298 
(*Replace subterms rec`x (where rec is a Free var) by recursor_tm(x) *) 
299 
fun subst_rec (Const("op `",_) $ Free _ $ arg) = recursor_tm $ arg 

300 
 subst_rec tm = 

301 
let val (head, args) = strip_comb tm 

302 
in list_comb (head, map subst_rec args) end; 

6052  303 

12131  304 
(*Each equation has the form 
305 
REC(coni(args)) = f_coni(args, REC(rec_arg), ...) 

306 
where REC = recursor(f_con1,...,f_conn) and rec_arg is a recursive 

307 
constructor argument.*) 

308 
fun mk_recursor_eqn (((_,T,_), name, args, _), recursor_case) = 

309 
FOLogic.mk_Trueprop 

310 
(FOLogic.mk_eq 

311 
(recursor_tm $ 

312 
(list_comb (Const (Sign.intern_const (sign_of thy1) name,T), 

313 
args)), 

314 
subst_rec (foldl betapply (recursor_case, args)))); 

6052  315 

12131  316 
val recursor_trans = recursor_def RS def_Vrecursor RS trans; 
6052  317 

12131  318 
(*Proves a single recursor equation.*) 
319 
fun recursor_tacsf _ = 

320 
[rtac recursor_trans 1, 

321 
simp_tac (rank_ss addsimps case_eqns) 1, 

322 
IF_UNSOLVED (simp_tac (rank_ss addsimps tl con_defs) 1)]; 

6052  323 

12131  324 
fun prove_recursor_eqn arg = 
325 
prove_goalw_cterm [] 

326 
(Ind_Syntax.traceIt "next recursor equation = " 

327 
(cterm_of (sign_of thy1) (mk_recursor_eqn arg))) 

328 
recursor_tacsf 

6052  329 
in 
12131  330 
map prove_recursor_eqn (flat con_ty_lists ~~ recursor_cases) 
6052  331 
end 
332 

333 
val constructors = 

334 
map (head_of o #1 o Logic.dest_equals o #prop o rep_thm) (tl con_defs); 

335 

6112  336 
val free_SEs = Ind_Syntax.mk_free_SEs free_iffs; 
6052  337 

6154
6a00a5baef2b
automatic insertion of datatype intr rules into claset
paulson
parents:
6141
diff
changeset

338 
val {intrs, elim, induct, mutual_induct, ...} = ind_result 
6052  339 

340 
(*Typical theorems have the form ~con1=con2, con1=con2==>False, 

341 
con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <> x=y, etc. *) 

342 
fun mk_free s = 

343 
prove_goalw (theory_of_thm elim) (*Don't use thy1: it will be stale*) 

344 
con_defs s 

12131  345 
(fn prems => [cut_facts_tac prems 1, 
346 
fast_tac (ZF_cs addSEs free_SEs @ Su.free_SEs) 1]); 

6052  347 

348 
val simps = case_eqns @ recursor_eqns; 

349 

350 
val dt_info = 

12131  351 
{inductive = true, 
352 
constructors = constructors, 

353 
rec_rewrites = recursor_eqns, 

354 
case_rewrites = case_eqns, 

355 
induct = induct, 

356 
mutual_induct = mutual_induct, 

357 
exhaustion = elim}; 

6052  358 

359 
val con_info = 

360 
{big_rec_name = big_rec_name, 

12131  361 
constructors = constructors, 
6052  362 
(*let primrec handle definition by cases*) 
12131  363 
free_iffs = free_iffs, 
364 
rec_rewrites = (case recursor_eqns of 

365 
[] => case_eqns  _ => recursor_eqns)}; 

6052  366 

367 
(*associate with each constructor the datatype name and rewrites*) 

368 
val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors 

369 

370 
in 

371 
(*Updating theory components: simprules and datatype info*) 

372 
(thy1 > Theory.add_path big_rec_base_name 

12183  373 
> (#1 o PureThy.add_thmss 
374 
[(("simps", simps), [Simplifier.simp_add_global]), 

375 
(("", intrs), [Classical.safe_intro_global])]) 

376 
> DatatypesData.map (fn tab => Symtab.update ((big_rec_name, dt_info), tab)) 

377 
> ConstructorsData.map (fn tab => foldr Symtab.update (con_pairs, tab)) 

12131  378 
> Theory.parent_path, 
6052  379 
ind_result, 
380 
{con_defs = con_defs, 

381 
case_eqns = case_eqns, 

382 
recursor_eqns = recursor_eqns, 

383 
free_iffs = free_iffs, 

384 
free_SEs = free_SEs, 

385 
mk_free = mk_free}) 

386 
end; 

387 

388 

12183  389 
fun add_datatype_x (sdom, srec_tms) scon_ty_lists (monos, type_intrs, type_elims) thy = 
390 
let 

391 
val sign = sign_of thy; 

392 
val read_i = Sign.simple_read_term sign Ind_Syntax.iT; 

393 
val rec_tms = map read_i srec_tms; 

394 
val con_ty_lists = Ind_Syntax.read_constructs sign scon_ty_lists 

395 
val dom_sum = 

396 
if sdom = "" then Ind_Syntax.data_domain coind (rec_tms, con_ty_lists) 

397 
else read_i sdom; 

398 
in add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims) thy end; 

399 

400 
fun add_datatype (sdom, srec_tms) scon_ty_lists (raw_monos, raw_type_intrs, raw_type_elims) thy = 

401 
let 

402 
val (thy', ((monos, type_intrs), type_elims)) = thy 

403 
> IsarThy.apply_theorems raw_monos 

404 
>>> IsarThy.apply_theorems raw_type_intrs 

405 
>>> IsarThy.apply_theorems raw_type_elims; 

406 
in add_datatype_x (sdom, srec_tms) scon_ty_lists (monos, type_intrs, type_elims) thy' end; 

407 

408 

409 
(* outer syntax *) 

410 

411 
local structure P = OuterParse and K = OuterSyntax.Keyword in 

412 

413 
fun mk_datatype ((((dom, dts), monos), type_intrs), type_elims) = 

414 
#1 o add_datatype (dom, map fst dts) (map snd dts) (monos, type_intrs, type_elims); 

415 

416 
val con_decl = 

417 
P.name  Scan.optional (P.$$$ "("  P.list1 P.term  P.$$$ ")") []  P.opt_mixfix 

418 
>> P.triple1; 

419 

420 
val datatype_decl = 

421 
(Scan.optional ((P.$$$ "\\<subseteq>"  P.$$$ "<=")  P.!!! P.term) "")  

422 
P.and_list1 (P.term  (P.$$$ "="  P.enum1 "" con_decl))  

423 
Scan.optional (P.$$$ "monos"  P.!!! P.xthms1  P.marg_comment) []  

424 
Scan.optional (P.$$$ "type_intros"  P.!!! P.xthms1  P.marg_comment) []  

425 
Scan.optional (P.$$$ "type_elims"  P.!!! P.xthms1  P.marg_comment) [] 

426 
>> (Toplevel.theory o mk_datatype); 

427 

428 
val coind_prefix = if coind then "co" else ""; 

429 

430 
val inductiveP = OuterSyntax.command (coind_prefix ^ "datatype") 

431 
("define " ^ coind_prefix ^ "datatype") K.thy_decl datatype_decl; 

432 

433 
val _ = OuterSyntax.add_parsers [inductiveP]; 

6052  434 

435 
end; 

12183  436 

437 
end; 