author  paulson 
Tue, 19 Jan 1999 11:18:11 +0100  
changeset 6141  a6922171b396 
parent 6092  d9db67970c73 
child 6394  3d9fd50fcc43 
permissions  rwrr 
5094  1 
(* Title: HOL/Tools/inductive_package.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Stefan Berghofer, TU Muenchen 

5 
Copyright 1994 University of Cambridge 

6 
1998 TU Muenchen 

7 

8 
(Co)Inductive Definition module for HOL 

9 

10 
Features: 

11 
* least or greatest fixedpoints 

12 
* userspecified product and sum constructions 

13 
* mutually recursive definitions 

14 
* definitions involving arbitrary monotone operators 

15 
* automatically proves introduction and elimination rules 

16 

17 
The recursive sets must *already* be declared as constants in parent theory! 

18 

19 
Introduction rules have the form 

20 
[ ti:M(Sj), ..., P(x), ... ] ==> t: Sk ] 

21 
where M is some monotone operator (usually the identity) 

22 
P(x) is any side condition on the free variables 

23 
ti, t are any terms 

24 
Sj, Sk are two of the sets being defined in mutual recursion 

25 

26 
Sums are used only for mutual recursion; 

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

28 
*) 

29 

30 
signature INDUCTIVE_PACKAGE = 

31 
sig 

5662  32 
val quiet_mode : bool ref 
5094  33 
val add_inductive_i : bool > bool > bstring > bool > bool > bool > term list > 
34 
term list > thm list > thm list > theory > theory * 

35 
{defs:thm list, elims:thm list, raw_induct:thm, induct:thm, 

36 
intrs:thm list, 

6141  37 
mk_cases:string > thm, mono:thm, 
5094  38 
unfold:thm} 
39 
val add_inductive : bool > bool > string list > string list 

5718
e5094d678285
Changed interface of add_inductive: monos and con_defs are now
berghofe
parents:
5662
diff
changeset

40 
> xstring list > xstring list > theory > theory * 
5094  41 
{defs:thm list, elims:thm list, raw_induct:thm, induct:thm, 
42 
intrs:thm list, 

6141  43 
mk_cases:string > thm, mono:thm, 
5094  44 
unfold:thm} 
45 
end; 

46 

47 
structure InductivePackage : INDUCTIVE_PACKAGE = 

48 
struct 

49 

5662  50 
val quiet_mode = ref false; 
51 
fun message s = if !quiet_mode then () else writeln s; 

52 

5094  53 
(*For proving monotonicity of recursion operator*) 
54 
val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, 

55 
ex_mono, Collect_mono, in_mono, vimage_mono]; 

56 

57 
val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (concl_of vimageD); 

58 

59 
(*Delete needless equality assumptions*) 

60 
val refl_thin = prove_goal HOL.thy "!!P. [ a=a; P ] ==> P" 

61 
(fn _ => [assume_tac 1]); 

62 

63 
(*For simplifying the elimination rule*) 

5120
f7f5442c934a
Removed disjE from list of rules used to simplify elimination
berghofe
parents:
5108
diff
changeset

64 
val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject]; 
5094  65 

66 
val vimage_name = Sign.intern_const (sign_of Vimage.thy) "op ``"; 

67 
val mono_name = Sign.intern_const (sign_of Ord.thy) "mono"; 

68 

69 
(* make injections needed in mutually recursive definitions *) 

70 

71 
fun mk_inj cs sumT c x = 

72 
let 

73 
fun mk_inj' T n i = 

74 
if n = 1 then x else 

75 
let val n2 = n div 2; 

76 
val Type (_, [T1, T2]) = T 

77 
in 

78 
if i <= n2 then 

79 
Const ("Inl", T1 > T) $ (mk_inj' T1 n2 i) 

80 
else 

81 
Const ("Inr", T2 > T) $ (mk_inj' T2 (n  n2) (i  n2)) 

82 
end 

83 
in mk_inj' sumT (length cs) (1 + find_index_eq c cs) 

84 
end; 

85 

86 
(* make "vimage" terms for selecting out components of mutually rec.def. *) 

87 

88 
fun mk_vimage cs sumT t c = if length cs < 2 then t else 

89 
let 

90 
val cT = HOLogic.dest_setT (fastype_of c); 

91 
val vimageT = [cT > sumT, HOLogic.mk_setT sumT] > HOLogic.mk_setT cT 

92 
in 

93 
Const (vimage_name, vimageT) $ 

94 
Abs ("y", cT, mk_inj cs sumT c (Bound 0)) $ t 

95 
end; 

96 

97 
(**************************** wellformedness checks **************************) 

98 

99 
fun err_in_rule sign t msg = error ("Illformed introduction rule\n" ^ 

100 
(Sign.string_of_term sign t) ^ "\n" ^ msg); 

101 

102 
fun err_in_prem sign t p msg = error ("Illformed premise\n" ^ 

103 
(Sign.string_of_term sign p) ^ "\nin introduction rule\n" ^ 

104 
(Sign.string_of_term sign t) ^ "\n" ^ msg); 

105 

106 
val msg1 = "Conclusion of introduction rule must have form\ 

107 
\ ' t : S_i '"; 

108 
val msg2 = "Premises mentioning recursive sets must have form\ 

109 
\ ' t : M S_i '"; 

110 
val msg3 = "Recursion term on left of member symbol"; 

111 

112 
fun check_rule sign cs r = 

113 
let 

114 
fun check_prem prem = if exists (Logic.occs o (rpair prem)) cs then 

115 
(case prem of 

116 
(Const ("op :", _) $ t $ u) => 

117 
if exists (Logic.occs o (rpair t)) cs then 

118 
err_in_prem sign r prem msg3 else () 

119 
 _ => err_in_prem sign r prem msg2) 

120 
else () 

121 

122 
in (case (HOLogic.dest_Trueprop o Logic.strip_imp_concl) r of 

123 
(Const ("op :", _) $ _ $ u) => 

124 
if u mem cs then map (check_prem o HOLogic.dest_Trueprop) 

125 
(Logic.strip_imp_prems r) 

126 
else err_in_rule sign r msg1 

127 
 _ => err_in_rule sign r msg1) 

128 
end; 

129 

130 
fun try' f msg sign t = (f t) handle _ => error (msg ^ Sign.string_of_term sign t); 

131 

132 
(*********************** properties of (co)inductive sets *********************) 

133 

134 
(***************************** elimination rules ******************************) 

135 

136 
fun mk_elims cs cTs params intr_ts = 

137 
let 

138 
val used = foldr add_term_names (intr_ts, []); 

139 
val [aname, pname] = variantlist (["a", "P"], used); 

140 
val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT)); 

141 

142 
fun dest_intr r = 

143 
let val Const ("op :", _) $ t $ u = 

144 
HOLogic.dest_Trueprop (Logic.strip_imp_concl r) 

145 
in (u, t, Logic.strip_imp_prems r) end; 

146 

147 
val intrs = map dest_intr intr_ts; 

148 

149 
fun mk_elim (c, T) = 

150 
let 

151 
val a = Free (aname, T); 

152 

153 
fun mk_elim_prem (_, t, ts) = 

154 
list_all_free (map dest_Free ((foldr add_term_frees (t::ts, [])) \\ params), 

155 
Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P)); 

156 
in 

157 
Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) :: 

158 
map mk_elim_prem (filter (equal c o #1) intrs), P) 

159 
end 

160 
in 

161 
map mk_elim (cs ~~ cTs) 

162 
end; 

163 

164 
(***************** premises and conclusions of induction rules ****************) 

165 

166 
fun mk_indrule cs cTs params intr_ts = 

167 
let 

168 
val used = foldr add_term_names (intr_ts, []); 

169 

170 
(* predicates for induction rule *) 

171 

172 
val preds = map Free (variantlist (if length cs < 2 then ["P"] else 

173 
map (fn i => "P" ^ string_of_int i) (1 upto length cs), used) ~~ 

174 
map (fn T => T > HOLogic.boolT) cTs); 

175 

176 
(* transform an introduction rule into a premise for induction rule *) 

177 

178 
fun mk_ind_prem r = 

179 
let 

180 
val frees = map dest_Free ((add_term_frees (r, [])) \\ params); 

181 

182 
fun subst (prem as (Const ("op :", T) $ t $ u), prems) = 

183 
let val n = find_index_eq u cs in 

184 
if n >= 0 then prem :: (nth_elem (n, preds)) $ t :: prems else 

185 
(subst_free (map (fn (c, P) => (c, HOLogic.mk_binop "op Int" 

186 
(c, HOLogic.Collect_const (HOLogic.dest_setT 

187 
(fastype_of c)) $ P))) (cs ~~ preds)) prem)::prems 

188 
end 

189 
 subst (prem, prems) = prem::prems; 

190 

191 
val Const ("op :", _) $ t $ u = 

192 
HOLogic.dest_Trueprop (Logic.strip_imp_concl r) 

193 

194 
in list_all_free (frees, 

195 
Logic.list_implies (map HOLogic.mk_Trueprop (foldr subst 

196 
(map HOLogic.dest_Trueprop (Logic.strip_imp_prems r), [])), 

197 
HOLogic.mk_Trueprop (nth_elem (find_index_eq u cs, preds) $ t))) 

198 
end; 

199 

200 
val ind_prems = map mk_ind_prem intr_ts; 

201 

202 
(* make conclusions for induction rules *) 

203 

204 
fun mk_ind_concl ((c, P), (ts, x)) = 

205 
let val T = HOLogic.dest_setT (fastype_of c); 

206 
val Ts = HOLogic.prodT_factors T; 

207 
val (frees, x') = foldr (fn (T', (fs, s)) => 

208 
((Free (s, T'))::fs, bump_string s)) (Ts, ([], x)); 

209 
val tuple = HOLogic.mk_tuple T frees; 

210 
in ((HOLogic.mk_binop "op >" 

211 
(HOLogic.mk_mem (tuple, c), P $ tuple))::ts, x') 

212 
end; 

213 

214 
val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 (app HOLogic.conj) 

215 
(fst (foldr mk_ind_concl (cs ~~ preds, ([], "xa"))))) 

216 

217 
in (preds, ind_prems, mutual_ind_concl) 

218 
end; 

219 

220 
(********************** proofs for (co)inductive sets *************************) 

221 

222 
(**************************** prove monotonicity ******************************) 

223 

224 
fun prove_mono setT fp_fun monos thy = 

225 
let 

5662  226 
val _ = message " Proving monotonicity..."; 
5094  227 

228 
val mono = prove_goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop 

229 
(Const (mono_name, (setT > setT) > HOLogic.boolT) $ fp_fun))) 

230 
(fn _ => [rtac monoI 1, REPEAT (ares_tac (basic_monos @ monos) 1)]) 

231 

232 
in mono end; 

233 

234 
(************************* prove introduction rules ***************************) 

235 

236 
fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy = 

237 
let 

5662  238 
val _ = message " Proving the introduction rules..."; 
5094  239 

240 
val unfold = standard (mono RS (fp_def RS 

241 
(if coind then def_gfp_Tarski else def_lfp_Tarski))); 

242 

243 
fun select_disj 1 1 = [] 

244 
 select_disj _ 1 = [rtac disjI1] 

245 
 select_disj n i = (rtac disjI2)::(select_disj (n  1) (i  1)); 

246 

247 
val intrs = map (fn (i, intr) => prove_goalw_cterm rec_sets_defs 

248 
(cterm_of (sign_of thy) intr) (fn prems => 

249 
[(*insert prems and underlying sets*) 

250 
cut_facts_tac prems 1, 

251 
stac unfold 1, 

252 
REPEAT (resolve_tac [vimageI2, CollectI] 1), 

253 
(*Now 12 subgoals: the disjunction, perhaps equality.*) 

254 
EVERY1 (select_disj (length intr_ts) i), 

255 
(*Not ares_tac, since refl must be tried before any equality assumptions; 

256 
backtracking may occur if the premises have extra variables!*) 

257 
DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 1 APPEND assume_tac 1), 

258 
(*Now solve the equations like Inl 0 = Inl ?b2*) 

259 
rewrite_goals_tac con_defs, 

260 
REPEAT (rtac refl 1)])) (1 upto (length intr_ts) ~~ intr_ts) 

261 

262 
in (intrs, unfold) end; 

263 

264 
(*************************** prove elimination rules **************************) 

265 

266 
fun prove_elims cs cTs params intr_ts unfold rec_sets_defs thy = 

267 
let 

5662  268 
val _ = message " Proving the elimination rules..."; 
5094  269 

270 
val rules1 = [CollectE, disjE, make_elim vimageD]; 

271 
val rules2 = [exE, conjE, Inl_neq_Inr, Inr_neq_Inl] @ 

272 
map make_elim [Inl_inject, Inr_inject]; 

273 

274 
val elims = map (fn t => prove_goalw_cterm rec_sets_defs 

275 
(cterm_of (sign_of thy) t) (fn prems => 

276 
[cut_facts_tac [hd prems] 1, 

277 
dtac (unfold RS subst) 1, 

278 
REPEAT (FIRSTGOAL (eresolve_tac rules1)), 

279 
REPEAT (FIRSTGOAL (eresolve_tac rules2)), 

280 
EVERY (map (fn prem => 

5149  281 
DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))])) 
5094  282 
(mk_elims cs cTs params intr_ts) 
283 

284 
in elims end; 

285 

286 
(** derivation of simplified elimination rules **) 

287 

288 
(*Applies freeness of the given constructors, which *must* be unfolded by 

289 
the given defs. Cannot simply use the local con_defs because con_defs=[] 

290 
for inference systems. 

291 
*) 

6141  292 
fun con_elim_tac ss = 
5094  293 
let val elim_tac = REPEAT o (eresolve_tac elim_rls) 
294 
in ALLGOALS(EVERY'[elim_tac, 

6141  295 
asm_full_simp_tac ss, 
296 
elim_tac, 

297 
REPEAT o bound_hyp_subst_tac]) 

5094  298 
THEN prune_params_tac 
299 
end; 

300 

301 
(*String s should have the form t:Si where Si is an inductive set*) 

6141  302 
fun mk_cases elims s = 
303 
let val prem = assume (read_cterm (sign_of_thm (hd elims)) (s, propT)) 

304 
fun mk_elim rl = rule_by_tactic (con_elim_tac (simpset())) (prem RS rl) 

305 
> standard 

306 
in case find_first is_some (map (try mk_elim) elims) of 

5094  307 
Some (Some r) => r 
308 
 None => error ("mk_cases: string '" ^ s ^ "' not of form 't : S_i'") 

309 
end; 

310 

311 
(**************************** prove induction rule ****************************) 

312 

313 
fun prove_indrule cs cTs sumT rec_const params intr_ts mono 

314 
fp_def rec_sets_defs thy = 

315 
let 

5662  316 
val _ = message " Proving the induction rule..."; 
5094  317 

318 
val sign = sign_of thy; 

319 

320 
val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts; 

321 

322 
(* make predicate for instantiation of abstract induction rule *) 

323 

324 
fun mk_ind_pred _ [P] = P 

325 
 mk_ind_pred T Ps = 

326 
let val n = (length Ps) div 2; 

327 
val Type (_, [T1, T2]) = T 

328 
in Const ("sum_case", 

329 
[T1 > HOLogic.boolT, T2 > HOLogic.boolT, T] > HOLogic.boolT) $ 

330 
mk_ind_pred T1 (take (n, Ps)) $ mk_ind_pred T2 (drop (n, Ps)) 

331 
end; 

332 

333 
val ind_pred = mk_ind_pred sumT preds; 

334 

335 
val ind_concl = HOLogic.mk_Trueprop 

336 
(HOLogic.all_const sumT $ Abs ("x", sumT, HOLogic.mk_binop "op >" 

337 
(HOLogic.mk_mem (Bound 0, rec_const), ind_pred $ Bound 0))); 

338 

339 
(* simplification rules for vimage and Collect *) 

340 

341 
val vimage_simps = if length cs < 2 then [] else 

342 
map (fn c => prove_goalw_cterm [] (cterm_of sign 

343 
(HOLogic.mk_Trueprop (HOLogic.mk_eq 

344 
(mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c, 

345 
HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $ 

346 
nth_elem (find_index_eq c cs, preds))))) 

347 
(fn _ => [rtac vimage_Collect 1, rewrite_goals_tac 

5553  348 
(map mk_meta_eq [sum_case_Inl, sum_case_Inr]), 
5094  349 
rtac refl 1])) cs; 
350 

351 
val induct = prove_goalw_cterm [] (cterm_of sign 

352 
(Logic.list_implies (ind_prems, ind_concl))) (fn prems => 

353 
[rtac (impI RS allI) 1, 

354 
DETERM (etac (mono RS (fp_def RS def_induct)) 1), 

5553  355 
rewrite_goals_tac (map mk_meta_eq (vimage_Int::vimage_simps)), 
5094  356 
fold_goals_tac rec_sets_defs, 
357 
(*This CollectE and disjE separates out the introduction rules*) 

358 
REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE])), 

359 
(*Now break down the individual cases. No disjE here in case 

360 
some premise involves disjunction.*) 

361 
REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE] 

362 
ORELSE' hyp_subst_tac)), 

5553  363 
rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]), 
5094  364 
EVERY (map (fn prem => 
5149  365 
DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]); 
5094  366 

367 
val lemma = prove_goalw_cterm rec_sets_defs (cterm_of sign 

368 
(Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems => 

369 
[cut_facts_tac prems 1, 

370 
REPEAT (EVERY 

371 
[REPEAT (resolve_tac [conjI, impI] 1), 

372 
TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1, 

5553  373 
rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]), 
5094  374 
atac 1])]) 
375 

376 
in standard (split_rule (induct RS lemma)) 

377 
end; 

378 

379 
(*************** definitional introduction of (co)inductive sets **************) 

380 

381 
fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs 

382 
intr_ts monos con_defs thy params paramTs cTs cnames = 

383 
let 

5662  384 
val _ = if verbose then message ("Proofs for " ^ 
5094  385 
(if coind then "co" else "") ^ "inductive set(s) " ^ commas cnames) else (); 
386 

387 
val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs; 

388 
val setT = HOLogic.mk_setT sumT; 

389 

390 
val fp_name = if coind then Sign.intern_const (sign_of Gfp.thy) "gfp" 

391 
else Sign.intern_const (sign_of Lfp.thy) "lfp"; 

392 

5149  393 
val used = foldr add_term_names (intr_ts, []); 
394 
val [sname, xname] = variantlist (["S", "x"], used); 

395 

5094  396 
(* transform an introduction rule into a conjunction *) 
397 
(* [ t : ... S_i ... ; ... ] ==> u : S_j *) 

398 
(* is transformed into *) 

399 
(* x = Inj_j u & t : ... Inj_i `` S ... & ... *) 

400 

401 
fun transform_rule r = 

402 
let 

403 
val frees = map dest_Free ((add_term_frees (r, [])) \\ params); 

5149  404 
val subst = subst_free 
405 
(cs ~~ (map (mk_vimage cs sumT (Free (sname, setT))) cs)); 

5094  406 
val Const ("op :", _) $ t $ u = 
407 
HOLogic.dest_Trueprop (Logic.strip_imp_concl r) 

408 

409 
in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P)) 

410 
(frees, foldr1 (app HOLogic.conj) 

5149  411 
(((HOLogic.eq_const sumT) $ Free (xname, sumT) $ (mk_inj cs sumT u t)):: 
5094  412 
(map (subst o HOLogic.dest_Trueprop) 
413 
(Logic.strip_imp_prems r)))) 

414 
end 

415 

416 
(* make a disjunction of all introduction rules *) 

417 

5149  418 
val fp_fun = absfree (sname, setT, (HOLogic.Collect_const sumT) $ 
419 
absfree (xname, sumT, foldr1 (app HOLogic.disj) (map transform_rule intr_ts))); 

5094  420 

421 
(* add definiton of recursive sets to theory *) 

422 

423 
val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name; 

424 
val full_rec_name = Sign.full_name (sign_of thy) rec_name; 

425 

426 
val rec_const = list_comb 

427 
(Const (full_rec_name, paramTs > setT), params); 

428 

429 
val fp_def_term = Logic.mk_equals (rec_const, 

430 
Const (fp_name, (setT > setT) > setT) $ fp_fun) 

431 

432 
val def_terms = fp_def_term :: (if length cs < 2 then [] else 

433 
map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs); 

434 

435 
val thy' = thy > 

436 
(if declare_consts then 

437 
Theory.add_consts_i (map (fn (c, n) => 

438 
(n, paramTs > fastype_of c, NoSyn)) (cs ~~ cnames)) 

439 
else I) > 

440 
(if length cs < 2 then I else 

441 
Theory.add_consts_i [(rec_name, paramTs > setT, NoSyn)]) > 

442 
Theory.add_path rec_name > 

443 
PureThy.add_defss_i [(("defs", def_terms), [])]; 

444 

445 
(* get definitions from theory *) 

446 

447 
val fp_def::rec_sets_defs = get_thms thy' "defs"; 

448 

449 
(* prove and store theorems *) 

450 

451 
val mono = prove_mono setT fp_fun monos thy'; 

452 
val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts con_defs 

453 
rec_sets_defs thy'; 

454 
val elims = if no_elim then [] else 

455 
prove_elims cs cTs params intr_ts unfold rec_sets_defs thy'; 

456 
val raw_induct = if no_ind then TrueI else 

457 
if coind then standard (rule_by_tactic 

5553  458 
(rewrite_tac [mk_meta_eq vimage_Un] THEN 
5094  459 
fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct))) 
460 
else 

461 
prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def 

462 
rec_sets_defs thy'; 

5108  463 
val induct = if coind orelse no_ind orelse length cs > 1 then raw_induct 
5094  464 
else standard (raw_induct RSN (2, rev_mp)); 
465 

466 
val thy'' = thy' > 

6092  467 
PureThy.add_thmss [(("intrs", intrs), [])] > 
468 
(if no_elim then I else PureThy.add_thmss 

469 
[(("elims", elims), [])]) > 

470 
(if no_ind then I else PureThy.add_thms 

471 
[(((if coind then "co" else "") ^ "induct", induct), [])]) > 

5094  472 
Theory.parent_path; 
473 

474 
in (thy'', 

475 
{defs = fp_def::rec_sets_defs, 

476 
mono = mono, 

477 
unfold = unfold, 

478 
intrs = intrs, 

479 
elims = elims, 

480 
mk_cases = mk_cases elims, 

481 
raw_induct = raw_induct, 

482 
induct = induct}) 

483 
end; 

484 

485 
(***************** axiomatic introduction of (co)inductive sets ***************) 

486 

487 
fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs 

488 
intr_ts monos con_defs thy params paramTs cTs cnames = 

489 
let 

5662  490 
val _ = if verbose then message ("Adding axioms for " ^ 
5094  491 
(if coind then "co" else "") ^ "inductive set(s) " ^ commas cnames) else (); 
492 

493 
val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name; 

494 

495 
val elim_ts = mk_elims cs cTs params intr_ts; 

496 

497 
val (_, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts; 

498 
val ind_t = Logic.list_implies (ind_prems, mutual_ind_concl); 

499 

500 
val thy' = thy > 

501 
(if declare_consts then 

502 
Theory.add_consts_i (map (fn (c, n) => 

503 
(n, paramTs > fastype_of c, NoSyn)) (cs ~~ cnames)) 

504 
else I) > 

505 
Theory.add_path rec_name > 

506 
PureThy.add_axiomss_i [(("intrs", intr_ts), []), (("elims", elim_ts), [])] > 

507 
(if coind then I 

508 
else PureThy.add_axioms_i [(("internal_induct", ind_t), [])]); 

509 

510 
val intrs = get_thms thy' "intrs"; 

511 
val elims = get_thms thy' "elims"; 

512 
val raw_induct = if coind then TrueI else 

513 
standard (split_rule (get_thm thy' "internal_induct")); 

514 
val induct = if coind orelse length cs > 1 then raw_induct 

515 
else standard (raw_induct RSN (2, rev_mp)); 

516 

517 
val thy'' = thy' > 

518 
(if coind then I 

6092  519 
else PureThy.add_thms [(("induct", induct), [])]) > 
5094  520 
Theory.parent_path 
521 

522 
in (thy'', 

523 
{defs = [], 

524 
mono = TrueI, 

525 
unfold = TrueI, 

526 
intrs = intrs, 

527 
elims = elims, 

528 
mk_cases = mk_cases elims, 

529 
raw_induct = raw_induct, 

530 
induct = induct}) 

531 
end; 

532 

533 
(********************** introduction of (co)inductive sets ********************) 

534 

535 
fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs 

536 
intr_ts monos con_defs thy = 

537 
let 

538 
val _ = Theory.requires thy "Inductive" 

539 
((if coind then "co" else "") ^ "inductive definitions"); 

540 

541 
val sign = sign_of thy; 

542 

543 
(*parameters should agree for all mutually recursive components*) 

544 
val (_, params) = strip_comb (hd cs); 

545 
val paramTs = map (try' (snd o dest_Free) "Parameter in recursive\ 

546 
\ component is not a free variable: " sign) params; 

547 

548 
val cTs = map (try' (HOLogic.dest_setT o fastype_of) 

549 
"Recursive component not of type set: " sign) cs; 

550 

551 
val cnames = map (try' (Sign.base_name o fst o dest_Const o head_of) 

552 
"Recursive set not previously declared as constant: " sign) cs; 

553 

554 
val _ = assert_all Syntax.is_identifier cnames 

555 
(fn a => "Base name of recursive set not an identifier: " ^ a); 

556 

557 
val _ = map (check_rule sign cs) intr_ts; 

558 

559 
in 

560 
(if !quick_and_dirty then add_ind_axm else add_ind_def) 

561 
verbose declare_consts alt_name coind no_elim no_ind cs intr_ts monos 

562 
con_defs thy params paramTs cTs cnames 

563 
end; 

564 

565 
(***************************** external interface *****************************) 

566 

567 
fun add_inductive verbose coind c_strings intr_strings monos con_defs thy = 

568 
let 

569 
val sign = sign_of thy; 

570 
val cs = map (readtm (sign_of thy) HOLogic.termTVar) c_strings; 

571 
val intr_ts = map (readtm (sign_of thy) propT) intr_strings; 

572 

573 
(* the following code ensures that each recursive set *) 

574 
(* always has the same type in all introduction rules *) 

575 

576 
val {tsig, ...} = Sign.rep_sg sign; 

577 
val add_term_consts_2 = 

578 
foldl_aterms (fn (cs, Const c) => c ins cs  (cs, _) => cs); 

579 
fun varify (t, (i, ts)) = 

580 
let val t' = map_term_types (incr_tvar (i + 1)) (Type.varify (t, [])) 

581 
in (maxidx_of_term t', t'::ts) end; 

582 
val (i, cs') = foldr varify (cs, (~1, [])); 

583 
val (i', intr_ts') = foldr varify (intr_ts, (i, [])); 

584 
val rec_consts = foldl add_term_consts_2 ([], cs'); 

585 
val intr_consts = foldl add_term_consts_2 ([], intr_ts'); 

586 
fun unify (env, (cname, cT)) = 

587 
let val consts = map snd (filter (fn c => fst c = cname) intr_consts) 

588 
in (foldl (fn ((env', j'), Tp) => Type.unify tsig j' env' Tp) 

589 
(env, (replicate (length consts) cT) ~~ consts)) handle _ => 

590 
error ("Occurrences of constant '" ^ cname ^ 

591 
"' have incompatible types") 

592 
end; 

593 
val (env, _) = foldl unify (([], i'), rec_consts); 

594 
fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars env T 

595 
in if T = T' then T else typ_subst_TVars_2 env T' end; 

596 
val subst = fst o Type.freeze_thaw o 

597 
(map_term_types (typ_subst_TVars_2 env)); 

598 
val cs'' = map subst cs'; 

599 
val intr_ts'' = map subst intr_ts'; 

600 

601 
in add_inductive_i verbose false "" coind false false cs'' intr_ts'' 

6092  602 
(PureThy.get_thmss thy monos) 
603 
(PureThy.get_thmss thy con_defs) thy 

5094  604 
end; 
605 

606 
end; 