author  oheimb 
Thu, 24 Sep 1998 17:17:14 +0200  
changeset 5553  ae42b36a50c2 
parent 5303  22029546d109 
child 5662  72a2e33d3b9e 
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 

32 
val add_inductive_i : bool > bool > bstring > bool > bool > bool > term list > 

33 
term list > thm list > thm list > theory > theory * 

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

35 
intrs:thm list, 

36 
mk_cases:thm list > string > thm, mono:thm, 

37 
unfold:thm} 

38 
val add_inductive : bool > bool > string list > string list 

39 
> thm list > thm list > theory > theory * 

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

41 
intrs:thm list, 

42 
mk_cases:thm list > string > thm, mono:thm, 

43 
unfold:thm} 

44 
end; 

45 

46 
structure InductivePackage : INDUCTIVE_PACKAGE = 

47 
struct 

48 

49 
(*For proving monotonicity of recursion operator*) 

50 
val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, 

51 
ex_mono, Collect_mono, in_mono, vimage_mono]; 

52 

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

54 

55 
(*Delete needless equality assumptions*) 

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

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

58 

59 
(*For simplifying the elimination rule*) 

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

60 
val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject]; 
5094  61 

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

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

64 

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

66 

67 
fun mk_inj cs sumT c x = 

68 
let 

69 
fun mk_inj' T n i = 

70 
if n = 1 then x else 

71 
let val n2 = n div 2; 

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

73 
in 

74 
if i <= n2 then 

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

76 
else 

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

78 
end 

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

80 
end; 

81 

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

83 

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

85 
let 

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

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

88 
in 

89 
Const (vimage_name, vimageT) $ 

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

91 
end; 

92 

93 
(**************************** wellformedness checks **************************) 

94 

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

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

97 

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

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

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

101 

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

103 
\ ' t : S_i '"; 

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

105 
\ ' t : M S_i '"; 

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

107 

108 
fun check_rule sign cs r = 

109 
let 

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

111 
(case prem of 

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

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

114 
err_in_prem sign r prem msg3 else () 

115 
 _ => err_in_prem sign r prem msg2) 

116 
else () 

117 

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

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

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

121 
(Logic.strip_imp_prems r) 

122 
else err_in_rule sign r msg1 

123 
 _ => err_in_rule sign r msg1) 

124 
end; 

125 

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

127 

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

129 

130 
(***************************** elimination rules ******************************) 

131 

132 
fun mk_elims cs cTs params intr_ts = 

133 
let 

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

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

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

137 

138 
fun dest_intr r = 

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

140 
HOLogic.dest_Trueprop (Logic.strip_imp_concl r) 

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

142 

143 
val intrs = map dest_intr intr_ts; 

144 

145 
fun mk_elim (c, T) = 

146 
let 

147 
val a = Free (aname, T); 

148 

149 
fun mk_elim_prem (_, t, ts) = 

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

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

152 
in 

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

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

155 
end 

156 
in 

157 
map mk_elim (cs ~~ cTs) 

158 
end; 

159 

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

161 

162 
fun mk_indrule cs cTs params intr_ts = 

163 
let 

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

165 

166 
(* predicates for induction rule *) 

167 

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

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

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

171 

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

173 

174 
fun mk_ind_prem r = 

175 
let 

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

177 

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

179 
let val n = find_index_eq u cs in 

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

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

182 
(c, HOLogic.Collect_const (HOLogic.dest_setT 

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

184 
end 

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

186 

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

188 
HOLogic.dest_Trueprop (Logic.strip_imp_concl r) 

189 

190 
in list_all_free (frees, 

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

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

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

194 
end; 

195 

196 
val ind_prems = map mk_ind_prem intr_ts; 

197 

198 
(* make conclusions for induction rules *) 

199 

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

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

202 
val Ts = HOLogic.prodT_factors T; 

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

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

205 
val tuple = HOLogic.mk_tuple T frees; 

206 
in ((HOLogic.mk_binop "op >" 

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

208 
end; 

209 

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

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

212 

213 
in (preds, ind_prems, mutual_ind_concl) 

214 
end; 

215 

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

217 

218 
(**************************** prove monotonicity ******************************) 

219 

220 
fun prove_mono setT fp_fun monos thy = 

221 
let 

222 
val _ = writeln " Proving monotonicity..."; 

223 

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

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

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

227 

228 
in mono end; 

229 

230 
(************************* prove introduction rules ***************************) 

231 

232 
fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy = 

233 
let 

234 
val _ = writeln " Proving the introduction rules..."; 

235 

236 
val unfold = standard (mono RS (fp_def RS 

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

238 

239 
fun select_disj 1 1 = [] 

240 
 select_disj _ 1 = [rtac disjI1] 

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

242 

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

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

245 
[(*insert prems and underlying sets*) 

246 
cut_facts_tac prems 1, 

247 
stac unfold 1, 

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

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

250 
EVERY1 (select_disj (length intr_ts) i), 

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

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

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

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

255 
rewrite_goals_tac con_defs, 

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

257 

258 
in (intrs, unfold) end; 

259 

260 
(*************************** prove elimination rules **************************) 

261 

262 
fun prove_elims cs cTs params intr_ts unfold rec_sets_defs thy = 

263 
let 

264 
val _ = writeln " Proving the elimination rules..."; 

265 

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

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

268 
map make_elim [Inl_inject, Inr_inject]; 

269 

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

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

272 
[cut_facts_tac [hd prems] 1, 

273 
dtac (unfold RS subst) 1, 

274 
REPEAT (FIRSTGOAL (eresolve_tac rules1)), 

275 
REPEAT (FIRSTGOAL (eresolve_tac rules2)), 

276 
EVERY (map (fn prem => 

5149  277 
DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))])) 
5094  278 
(mk_elims cs cTs params intr_ts) 
279 

280 
in elims end; 

281 

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

283 

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

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

286 
for inference systems. 

287 
*) 

288 
fun con_elim_tac simps = 

289 
let val elim_tac = REPEAT o (eresolve_tac elim_rls) 

290 
in ALLGOALS(EVERY'[elim_tac, 

5179
819f90f278db
Replaced Nat.thy by NatDef.thy because Nat.thy depends on
berghofe
parents:
5149
diff
changeset

291 
asm_full_simp_tac (simpset_of NatDef.thy addsimps simps), 
5094  292 
elim_tac, 
293 
REPEAT o bound_hyp_subst_tac]) 

294 
THEN prune_params_tac 

295 
end; 

296 

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

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

298 
fun mk_cases elims simps s = 
5094  299 
let val prem = assume (read_cterm (sign_of_thm (hd elims)) (s, propT)); 
300 
val elims' = map (try (fn r => 

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

301 
rule_by_tactic (con_elim_tac simps) (prem RS r) > standard)) elims 
5094  302 
in case find_first is_some elims' of 
303 
Some (Some r) => r 

304 
 None => error ("mk_cases: string '" ^ s ^ "' not of form 't : S_i'") 

305 
end; 

306 

307 
(**************************** prove induction rule ****************************) 

308 

309 
fun prove_indrule cs cTs sumT rec_const params intr_ts mono 

310 
fp_def rec_sets_defs thy = 

311 
let 

312 
val _ = writeln " Proving the induction rule..."; 

313 

314 
val sign = sign_of thy; 

315 

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

317 

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

319 

320 
fun mk_ind_pred _ [P] = P 

321 
 mk_ind_pred T Ps = 

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

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

324 
in Const ("sum_case", 

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

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

327 
end; 

328 

329 
val ind_pred = mk_ind_pred sumT preds; 

330 

331 
val ind_concl = HOLogic.mk_Trueprop 

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

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

334 

335 
(* simplification rules for vimage and Collect *) 

336 

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

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

339 
(HOLogic.mk_Trueprop (HOLogic.mk_eq 

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

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

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

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

5553  344 
(map mk_meta_eq [sum_case_Inl, sum_case_Inr]), 
5094  345 
rtac refl 1])) cs; 
346 

347 
val induct = prove_goalw_cterm [] (cterm_of sign 

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

349 
[rtac (impI RS allI) 1, 

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

5553  351 
rewrite_goals_tac (map mk_meta_eq (vimage_Int::vimage_simps)), 
5094  352 
fold_goals_tac rec_sets_defs, 
353 
(*This CollectE and disjE separates out the introduction rules*) 

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

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

356 
some premise involves disjunction.*) 

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

358 
ORELSE' hyp_subst_tac)), 

5553  359 
rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]), 
5094  360 
EVERY (map (fn prem => 
5149  361 
DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]); 
5094  362 

363 
val lemma = prove_goalw_cterm rec_sets_defs (cterm_of sign 

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

365 
[cut_facts_tac prems 1, 

366 
REPEAT (EVERY 

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

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

5553  369 
rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]), 
5094  370 
atac 1])]) 
371 

372 
in standard (split_rule (induct RS lemma)) 

373 
end; 

374 

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

376 

377 
fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs 

378 
intr_ts monos con_defs thy params paramTs cTs cnames = 

379 
let 

380 
val _ = if verbose then writeln ("Proofs for " ^ 

381 
(if coind then "co" else "") ^ "inductive set(s) " ^ commas cnames) else (); 

382 

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

384 
val setT = HOLogic.mk_setT sumT; 

385 

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

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

388 

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

391 

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

394 
(* is transformed into *) 

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

396 

397 
fun transform_rule r = 

398 
let 

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

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

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

404 

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

406 
(frees, foldr1 (app HOLogic.conj) 

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

410 
end 

411 

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

413 

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

5094  416 

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

418 

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

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

421 

422 
val rec_const = list_comb 

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

424 

425 
val fp_def_term = Logic.mk_equals (rec_const, 

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

427 

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

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

430 

431 
val thy' = thy > 

432 
(if declare_consts then 

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

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

435 
else I) > 

436 
(if length cs < 2 then I else 

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

438 
Theory.add_path rec_name > 

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

440 

441 
(* get definitions from theory *) 

442 

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

444 

445 
(* prove and store theorems *) 

446 

447 
val mono = prove_mono setT fp_fun monos thy'; 

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

449 
rec_sets_defs thy'; 

450 
val elims = if no_elim then [] else 

451 
prove_elims cs cTs params intr_ts unfold rec_sets_defs thy'; 

452 
val raw_induct = if no_ind then TrueI else 

453 
if coind then standard (rule_by_tactic 

5553  454 
(rewrite_tac [mk_meta_eq vimage_Un] THEN 
5094  455 
fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct))) 
456 
else 

457 
prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def 

458 
rec_sets_defs thy'; 

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

462 
val thy'' = thy' > 

463 
PureThy.add_tthmss [(("intrs", map Attribute.tthm_of intrs), [])] > 

464 
(if no_elim then I else PureThy.add_tthmss 

465 
[(("elims", map Attribute.tthm_of elims), [])]) > 

466 
(if no_ind then I else PureThy.add_tthms 

467 
[(((if coind then "co" else "") ^ "induct", 

468 
Attribute.tthm_of induct), [])]) > 

469 
Theory.parent_path; 

470 

471 
in (thy'', 

472 
{defs = fp_def::rec_sets_defs, 

473 
mono = mono, 

474 
unfold = unfold, 

475 
intrs = intrs, 

476 
elims = elims, 

477 
mk_cases = mk_cases elims, 

478 
raw_induct = raw_induct, 

479 
induct = induct}) 

480 
end; 

481 

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

483 

484 
fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs 

485 
intr_ts monos con_defs thy params paramTs cTs cnames = 

486 
let 

487 
val _ = if verbose then writeln ("Adding axioms for " ^ 

488 
(if coind then "co" else "") ^ "inductive set(s) " ^ commas cnames) else (); 

489 

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

491 

492 
val elim_ts = mk_elims cs cTs params intr_ts; 

493 

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

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

496 

497 
val thy' = thy > 

498 
(if declare_consts then 

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

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

501 
else I) > 

502 
Theory.add_path rec_name > 

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

504 
(if coind then I 

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

506 

507 
val intrs = get_thms thy' "intrs"; 

508 
val elims = get_thms thy' "elims"; 

509 
val raw_induct = if coind then TrueI else 

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

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

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

513 

514 
val thy'' = thy' > 

515 
(if coind then I 

516 
else PureThy.add_tthms [(("induct", Attribute.tthm_of induct), [])]) > 

517 
Theory.parent_path 

518 

519 
in (thy'', 

520 
{defs = [], 

521 
mono = TrueI, 

522 
unfold = TrueI, 

523 
intrs = intrs, 

524 
elims = elims, 

525 
mk_cases = mk_cases elims, 

526 
raw_induct = raw_induct, 

527 
induct = induct}) 

528 
end; 

529 

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

531 

532 
fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs 

533 
intr_ts monos con_defs thy = 

534 
let 

535 
val _ = Theory.requires thy "Inductive" 

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

537 

538 
val sign = sign_of thy; 

539 

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

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

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

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

544 

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

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

547 

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

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

550 

551 
val _ = assert_all Syntax.is_identifier cnames 

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

553 

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

555 

556 
in 

557 
(if !quick_and_dirty then add_ind_axm else add_ind_def) 

558 
verbose declare_consts alt_name coind no_elim no_ind cs intr_ts monos 

559 
con_defs thy params paramTs cTs cnames 

560 
end; 

561 

562 
(***************************** external interface *****************************) 

563 

564 
fun add_inductive verbose coind c_strings intr_strings monos con_defs thy = 

565 
let 

566 
val sign = sign_of thy; 

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

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

569 

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

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

572 

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

574 
val add_term_consts_2 = 

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

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

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

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

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

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

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

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

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

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

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

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

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

588 
"' have incompatible types") 

589 
end; 

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

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

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

593 
val subst = fst o Type.freeze_thaw o 

594 
(map_term_types (typ_subst_TVars_2 env)); 

595 
val cs'' = map subst cs'; 

596 
val intr_ts'' = map subst intr_ts'; 

597 

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

599 
monos con_defs thy 

600 
end; 

601 

602 
end; 