author  wenzelm 
Fri, 09 Nov 2001 22:53:10 +0100  
changeset 12131  673bc8469a08 
parent 9329  d2655dc8a4b4 
child 12183  c10cea75dd56 
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 

16 
type datatype_result = 

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

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

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

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

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

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

24 

25 
signature DATATYPE_ARG = 

12131  26 
sig 
6052  27 
val intrs : thm list 
28 
val elims : thm list 

29 
end; 

30 

31 

32 
(*Functor's result signature*) 

33 
signature DATATYPE_PACKAGE = 

12131  34 
sig 
6052  35 

36 
(*Insert definitions for the recursive sets, which 

37 
must *already* be declared as constants in parent theory!*) 

12131  38 
val add_datatype_i: 
39 
term * term list * Ind_Syntax.constructor_spec list list * 

6052  40 
thm list * thm list * thm list 
41 
> theory > theory * inductive_result * datatype_result 

42 

12131  43 
val add_datatype: 
44 
string * string list * 

6052  45 
(string * string list * mixfix) list list * 
46 
thm list * thm list * thm list 

47 
> theory > theory * inductive_result * datatype_result 

48 

12131  49 
end; 
6052  50 

51 

52 
(*Declares functions to add fixedpoint/constructor defs to a theory. 

53 
Recursive sets must *already* be declared as constants.*) 

12131  54 
functor Add_datatype_def_Fun 
55 
(structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU 

56 
and Ind_Package : INDUCTIVE_PACKAGE 

6052  57 
and Datatype_Arg : DATATYPE_ARG) 
58 
: DATATYPE_PACKAGE = 

59 
struct 

60 

61 

62 
(*con_ty_lists specifies the constructors in the form (name,prems,mixfix) *) 

12131  63 
fun add_datatype_i (dom_sum, rec_tms, con_ty_lists, 
64 
monos, type_intrs, type_elims) thy = 

6052  65 
let 
66 
open BasisLibrary 

67 
val dummy = (*has essential ancestors?*) 

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

69 

70 

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

72 
val rec_base_names = map Sign.base_name rec_names 

73 
val big_rec_base_name = space_implode "_" rec_base_names 

74 

75 
val thy_path = thy > Theory.add_path big_rec_base_name 

76 
val sign = sign_of thy_path 

77 

78 
val big_rec_name = Sign.intern_const sign big_rec_base_name; 

79 

12131  80 
val intr_tms = Ind_Syntax.mk_all_intr_tms sign (rec_tms, con_ty_lists); 
6052  81 

12131  82 
val dummy = 
83 
writeln ((if (#1 (dest_Const Fp.oper) = "Fixedpt.lfp") then "Datatype" 

84 
else "Codatatype") 

85 
^ " definition " ^ big_rec_name) 

6052  86 

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

88 

89 
(** Define the constructors **) 

90 

91 
(*The empty tuple is 0*) 

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

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

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

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

98 

99 

100 
val full_name = Sign.full_name sign; 

101 

12131  102 
(*Make constructor definition; 
6052  103 
kpart is the number of this mutually recursive part*) 
12131  104 
fun mk_con_defs (kpart, con_ty_list) = 
6052  105 
let val ncon = length con_ty_list (*number of constructors*) 
12131  106 
fun mk_def (((id,T,syn), name, args, prems), kcon) = 
107 
(*kcon is index of constructor*) 

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

109 
mk_inject npart kpart 

110 
(mk_inject ncon kcon (mk_tuple args))) 

6052  111 
in ListPair.map mk_def (con_ty_list, 1 upto ncon) end; 
112 

113 

114 
(*** Define the case operator ***) 

115 

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

12131  117 
fun call_case case_list = 
6052  118 
let fun call_f (free,[]) = Abs("null", iT, free) 
12131  119 
 call_f (free,args) = 
120 
CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args)) 

121 
Ind_Syntax.iT 

122 
free 

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

125 
(** Generating function variables for the case definition 

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

127 

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

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

130 
if Syntax.is_identifier name then 

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

132 
else 

12131  133 
(opno + 1, (Free (case_varname ^ "_op_" ^ string_of_int opno, T), args) 
6052  134 
:: cases); 
135 

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

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

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

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

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

141 

142 
(*Treatment of all parts*) 

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

144 

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

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

147 

148 
val case_base_name = big_rec_base_name ^ "_case"; 

149 
val case_name = full_name case_base_name; 

150 

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

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

153 

12131  154 
val case_const = Const (case_name, case_typ); 
6052  155 
val case_tm = list_comb (case_const, case_args); 
156 

157 
val case_def = Logic.mk_defpair 

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

160 

161 
(** Generating function variables for the recursor definition 

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

163 

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

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

166 

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

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

172 
if a = arg then rec_call $ Bound i 

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

6052  174 

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

12131  176 
fun call_recursor ((case_var, case_args), (recursor_var, recursor_args)) = 
6052  177 
let fun add_abs (Free(a,T), u) = Abs(a,T,u) 
12131  178 
val ncase_args = length case_args 
179 
val bound_args = map Bound ((ncase_args  1) downto 0) 

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

181 
(List.drop(recursor_args, ncase_args)) 

6052  182 
in 
12131  183 
foldr add_abs 
184 
(case_args, list_comb (recursor_var, 

185 
bound_args @ rec_args)) 

6052  186 
end 
187 

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

189 
fun rec_args [] = [] 

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

191 
(case head_of X of 

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

194 
then arg :: rec_args prems 

195 
else rec_args prems 

196 
 _ => rec_args prems) 

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

6052  198 

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

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

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

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

203 

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

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

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

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

209 
name, args @ args', prems) 

6052  210 
end; 
211 

12131  212 
val rec_ty_lists = (map (map rec_ty_elem) con_ty_lists); 
6052  213 

214 
(*Treatment of all parts*) 

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

216 

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

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

12131  219 
> (iT>iT); 
6052  220 

221 
val recursor_base_name = big_rec_base_name ^ "_rec"; 

222 
val recursor_name = full_name recursor_base_name; 

223 

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

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

226 

227 
val recursor_tm = 

12131  228 
list_comb (Const (recursor_name, recursor_typ), recursor_args); 
6052  229 

12131  230 
val recursor_cases = map call_recursor 
231 
(flat case_lists ~~ flat recursor_lists) 

6052  232 

12131  233 
val recursor_def = 
6052  234 
Logic.mk_defpair 
12131  235 
(recursor_tm, 
236 
Ind_Syntax.Vrecursor_const $ 

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

6052  238 

239 
(* Build the new theory *) 

240 

12131  241 
val need_recursor = 
6093  242 
(#1 (dest_Const Fp.oper) = "Fixedpt.lfp" andalso recursor_typ <> case_typ); 
6052  243 

12131  244 
fun add_recursor thy = 
6052  245 
if need_recursor then 
12131  246 
thy > Theory.add_consts_i 
247 
[(recursor_base_name, recursor_typ, NoSyn)] 

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

6052  249 
else thy; 
250 

8438  251 
val (thy0, con_defs) = thy_path 
12131  252 
> Theory.add_consts_i 
253 
((case_base_name, case_typ, NoSyn) :: 

254 
map #1 (flat con_ty_lists)) 

255 
> PureThy.add_defs_i false 

256 
(map Thm.no_attributes 

257 
(case_def :: 

258 
flat (ListPair.map mk_con_defs 

259 
(1 upto npart, con_ty_lists)))) 

260 
>> add_recursor 

261 
>> Theory.parent_path 

6052  262 

12131  263 
val (thy1, ind_result) = 
6052  264 
thy0 > Ind_Package.add_inductive_i 
12131  265 
false (rec_tms, dom_sum) (map (fn tm => (("", tm), [])) intr_tms) 
266 
(monos, con_defs, 

267 
type_intrs @ Datatype_Arg.intrs, 

268 
type_elims @ Datatype_Arg.elims) 

6052  269 

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

271 

272 

273 
(*** Prove the case theorems ***) 

274 

12131  275 
(*Each equation has the form 
6052  276 
case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *) 
12131  277 
fun mk_case_eqn (((_,T,_), name, args, _), case_free) = 
6052  278 
FOLogic.mk_Trueprop 
279 
(FOLogic.mk_eq 

280 
(case_tm $ 

12131  281 
(list_comb (Const (Sign.intern_const (sign_of thy1) name,T), 
282 
args)), 

283 
list_comb (case_free, args))); 

6052  284 

285 
val case_trans = hd con_defs RS Ind_Syntax.def_trans 

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

287 

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

12131  289 
fun case_tacsf con_def _ = 
6052  290 
[rewtac con_def, 
291 
rtac case_trans 1, 

12131  292 
REPEAT (resolve_tac [refl, split_trans, 
293 
Su.case_inl RS trans, 

294 
Su.case_inr RS trans] 1)]; 

6052  295 

296 
fun prove_case_eqn (arg,con_def) = 

12131  297 
prove_goalw_cterm [] 
298 
(Ind_Syntax.traceIt "next case equation = " 

299 
(cterm_of (sign_of thy1) (mk_case_eqn arg))) 

300 
(case_tacsf con_def); 

6052  301 

6112  302 
val free_iffs = con_defs RL [Ind_Syntax.def_swap_iff]; 
6052  303 

12131  304 
val case_eqns = 
305 
map prove_case_eqn 

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

6052  307 

308 
(*** Prove the recursor theorems ***) 

309 

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

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

12131  312 
[]) 
313 
 Some recursor_def => 

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

317 
 subst_rec tm = 

318 
let val (head, args) = strip_comb tm 

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

6052  320 

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

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

324 
constructor argument.*) 

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

326 
FOLogic.mk_Trueprop 

327 
(FOLogic.mk_eq 

328 
(recursor_tm $ 

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

330 
args)), 

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

6052  332 

12131  333 
val recursor_trans = recursor_def RS def_Vrecursor RS trans; 
6052  334 

12131  335 
(*Proves a single recursor equation.*) 
336 
fun recursor_tacsf _ = 

337 
[rtac recursor_trans 1, 

338 
simp_tac (rank_ss addsimps case_eqns) 1, 

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

6052  340 

12131  341 
fun prove_recursor_eqn arg = 
342 
prove_goalw_cterm [] 

343 
(Ind_Syntax.traceIt "next recursor equation = " 

344 
(cterm_of (sign_of thy1) (mk_recursor_eqn arg))) 

345 
recursor_tacsf 

6052  346 
in 
12131  347 
map prove_recursor_eqn (flat con_ty_lists ~~ recursor_cases) 
6052  348 
end 
349 

350 
val constructors = 

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

352 

6112  353 
val free_SEs = Ind_Syntax.mk_free_SEs free_iffs; 
6052  354 

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

355 
val {intrs, elim, induct, mutual_induct, ...} = ind_result 
6052  356 

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

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

359 
fun mk_free s = 

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

361 
con_defs s 

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

6052  364 

365 
val simps = case_eqns @ recursor_eqns; 

366 

367 
val dt_info = 

12131  368 
{inductive = true, 
369 
constructors = constructors, 

370 
rec_rewrites = recursor_eqns, 

371 
case_rewrites = case_eqns, 

372 
induct = induct, 

373 
mutual_induct = mutual_induct, 

374 
exhaustion = elim}; 

6052  375 

376 
val con_info = 

377 
{big_rec_name = big_rec_name, 

12131  378 
constructors = constructors, 
6052  379 
(*let primrec handle definition by cases*) 
12131  380 
free_iffs = free_iffs, 
381 
rec_rewrites = (case recursor_eqns of 

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

6052  383 

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

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

386 

387 
in 

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

389 
(thy1 > Theory.add_path big_rec_base_name 

12131  390 
> (#1 o PureThy.add_thmss [(("simps", simps), 
391 
[Simplifier.simp_add_global])]) 

392 
> (#1 o PureThy.add_thmss [(("", intrs), 

8124  393 
(*not "intrs" to avoid the warning that they 
12131  394 
are already stored by the inductive package*) 
395 
[Classical.safe_intro_global])]) 

396 
> DatatypesData.put 

397 
(Symtab.update 

398 
((big_rec_name, dt_info), DatatypesData.get thy1)) 

6052  399 
> ConstructorsData.put 
12131  400 
(foldr Symtab.update (con_pairs, ConstructorsData.get thy1)) 
401 
> Theory.parent_path, 

6052  402 
ind_result, 
403 
{con_defs = con_defs, 

404 
case_eqns = case_eqns, 

405 
recursor_eqns = recursor_eqns, 

406 
free_iffs = free_iffs, 

407 
free_SEs = free_SEs, 

408 
mk_free = mk_free}) 

409 
end; 

410 

411 

12131  412 
fun add_datatype (sdom, srec_tms, scon_ty_lists, 
413 
monos, type_intrs, type_elims) thy = 

6052  414 
let val sign = sign_of thy 
8819  415 
val read_i = Sign.simple_read_term sign Ind_Syntax.iT 
416 
val rec_tms = map read_i srec_tms 

6112  417 
val con_ty_lists = Ind_Syntax.read_constructs sign scon_ty_lists 
12131  418 
val dom_sum = 
6052  419 
if sdom = "" then 
12131  420 
Ind_Syntax.data_domain (#1(dest_Const Fp.oper) <> "Fixedpt.lfp") 
421 
(rec_tms, con_ty_lists) 

8819  422 
else read_i sdom 
12131  423 
in 
424 
add_datatype_i (dom_sum, rec_tms, con_ty_lists, 

425 
monos, type_intrs, type_elims) thy 

426 
end 

6052  427 

428 
end; 