author  wenzelm 
Tue, 25 May 1999 20:24:10 +0200  
changeset 6729  b6e167580a32 
parent 6723  f342449d73ca 
child 6851  526c0b90bcef 
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 

6424  8 
(Co)Inductive Definition module for HOL. 
5094  9 

10 
Features: 

6424  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 

5094  16 

6424  17 
The recursive sets must *already* be declared as constants in the 
18 
current theory! 

5094  19 

20 
Introduction rules have the form 

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

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

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

24 
ti, t are any terms 

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

26 

6424  27 
Sums are used only for mutual recursion. Products are used only to 
28 
derive "streamlined" induction rules for relations. 

5094  29 
*) 
30 

31 
signature INDUCTIVE_PACKAGE = 

32 
sig 

6424  33 
val quiet_mode: bool ref 
6437  34 
val get_inductive: theory > string > 
35 
{names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm, 

36 
induct: thm, intrs: thm list, mk_cases: string > thm, mono: thm, unfold: thm} 

37 
val print_inductives: theory > unit 

6424  38 
val add_inductive_i: bool > bool > bstring > bool > bool > bool > term list > 
6521  39 
theory attribute list > ((bstring * term) * theory attribute list) list > 
40 
thm list > thm list > theory > theory * 

6424  41 
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm, 
6437  42 
intrs: thm list, mk_cases: string > thm, mono: thm, unfold: thm} 
6521  43 
val add_inductive: bool > bool > string list > Args.src list > 
44 
((bstring * string) * Args.src list) list > (xstring * Args.src list) list > 

45 
(xstring * Args.src list) list > theory > theory * 

6424  46 
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm, 
6437  47 
intrs: thm list, mk_cases: string > thm, mono: thm, unfold: thm} 
48 
val setup: (theory > theory) list 

5094  49 
end; 
50 

6424  51 
structure InductivePackage: INDUCTIVE_PACKAGE = 
5094  52 
struct 
53 

6424  54 
(** utilities **) 
55 

56 
(* messages *) 

57 

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

60 

6424  61 
fun coind_prefix true = "co" 
62 
 coind_prefix false = ""; 

63 

64 

65 
(* misc *) 

66 

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

69 
ex_mono, Collect_mono, in_mono, vimage_mono]; 

70 

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

72 

73 
(*Delete needless equality assumptions*) 

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

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

76 

77 
(*For simplifying the elimination rule*) 

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

78 
val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject]; 
5094  79 

6394  80 
val vimage_name = Sign.intern_const (Theory.sign_of Vimage.thy) "op ``"; 
81 
val mono_name = Sign.intern_const (Theory.sign_of Ord.thy) "mono"; 

5094  82 

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

84 

85 
fun mk_inj cs sumT c x = 

86 
let 

87 
fun mk_inj' T n i = 

88 
if n = 1 then x else 

89 
let val n2 = n div 2; 

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

91 
in 

92 
if i <= n2 then 

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

94 
else 

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

96 
end 

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

98 
end; 

99 

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

101 

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

103 
let 

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

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

106 
in 

107 
Const (vimage_name, vimageT) $ 

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

109 
end; 

110 

6424  111 

112 

113 
(** wellformedness checks **) 

5094  114 

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

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

117 

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

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

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

121 

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

123 
\ ' t : S_i '"; 

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

125 
\ ' t : M S_i '"; 

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

127 

128 
fun check_rule sign cs r = 

129 
let 

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

131 
(case prem of 

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

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

134 
err_in_prem sign r prem msg3 else () 

135 
 _ => err_in_prem sign r prem msg2) 

136 
else () 

137 

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

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

6424  140 
if u mem cs then seq (check_prem o HOLogic.dest_Trueprop) 
5094  141 
(Logic.strip_imp_prems r) 
142 
else err_in_rule sign r msg1 

143 
 _ => err_in_rule sign r msg1) 

144 
end; 

145 

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

147 

6424  148 

5094  149 

6437  150 
(*** theory data ***) 
151 

152 
(* data kind 'HOL/inductive' *) 

153 

154 
type inductive_info = 

155 
{names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm, 

156 
induct: thm, intrs: thm list, mk_cases: string > thm, mono: thm, unfold: thm}; 

157 

158 
structure InductiveArgs = 

159 
struct 

160 
val name = "HOL/inductive"; 

161 
type T = inductive_info Symtab.table; 

162 

163 
val empty = Symtab.empty; 

6556  164 
val copy = I; 
6437  165 
val prep_ext = I; 
166 
val merge: T * T > T = Symtab.merge (K true); 

167 

168 
fun print sg tab = 

169 
Pretty.writeln (Pretty.strs ("(co)inductives:" :: 

170 
map (Sign.cond_extern sg Sign.constK o fst) (Symtab.dest tab))); 

171 
end; 

172 

173 
structure InductiveData = TheoryDataFun(InductiveArgs); 

174 
val print_inductives = InductiveData.print; 

175 

176 

177 
(* get and put data *) 

178 

179 
fun get_inductive thy name = 

180 
(case Symtab.lookup (InductiveData.get thy, name) of 

181 
Some info => info 

182 
 None => error ("Unknown (co)inductive set " ^ quote name)); 

183 

184 
fun put_inductives names info thy = 

185 
let 

186 
fun upd (tab, name) = Symtab.update_new ((name, info), tab); 

187 
val tab = foldl upd (InductiveData.get thy, names) 

188 
handle Symtab.DUP name => error ("Duplicate definition of (co)inductive set " ^ quote name); 

189 
in InductiveData.put tab thy end; 

190 

191 

192 

6424  193 
(*** properties of (co)inductive sets ***) 
194 

195 
(** elimination rules **) 

5094  196 

197 
fun mk_elims cs cTs params intr_ts = 

198 
let 

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

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

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

202 

203 
fun dest_intr r = 

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

205 
HOLogic.dest_Trueprop (Logic.strip_imp_concl r) 

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

207 

208 
val intrs = map dest_intr intr_ts; 

209 

210 
fun mk_elim (c, T) = 

211 
let 

212 
val a = Free (aname, T); 

213 

214 
fun mk_elim_prem (_, t, ts) = 

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

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

217 
in 

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

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

220 
end 

221 
in 

222 
map mk_elim (cs ~~ cTs) 

223 
end; 

224 

6424  225 

226 

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

5094  228 

229 
fun mk_indrule cs cTs params intr_ts = 

230 
let 

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

232 

233 
(* predicates for induction rule *) 

234 

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

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

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

238 

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

240 

241 
fun mk_ind_prem r = 

242 
let 

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

244 

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

246 
let val n = find_index_eq u cs in 

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

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

249 
(c, HOLogic.Collect_const (HOLogic.dest_setT 

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

251 
end 

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

253 

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

255 
HOLogic.dest_Trueprop (Logic.strip_imp_concl r) 

256 

257 
in list_all_free (frees, 

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

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

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

261 
end; 

262 

263 
val ind_prems = map mk_ind_prem intr_ts; 

264 

265 
(* make conclusions for induction rules *) 

266 

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

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

269 
val Ts = HOLogic.prodT_factors T; 

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

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

272 
val tuple = HOLogic.mk_tuple T frees; 

273 
in ((HOLogic.mk_binop "op >" 

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

275 
end; 

276 

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

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

279 

280 
in (preds, ind_prems, mutual_ind_concl) 

281 
end; 

282 

6424  283 

5094  284 

6424  285 
(*** proofs for (co)inductive sets ***) 
286 

287 
(** prove monotonicity **) 

5094  288 

289 
fun prove_mono setT fp_fun monos thy = 

290 
let 

6427  291 
val _ = message " Proving monotonicity ..."; 
5094  292 

6394  293 
val mono = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop 
5094  294 
(Const (mono_name, (setT > setT) > HOLogic.boolT) $ fp_fun))) 
295 
(fn _ => [rtac monoI 1, REPEAT (ares_tac (basic_monos @ monos) 1)]) 

296 

297 
in mono end; 

298 

6424  299 

300 

301 
(** prove introduction rules **) 

5094  302 

303 
fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy = 

304 
let 

6427  305 
val _ = message " Proving the introduction rules ..."; 
5094  306 

307 
val unfold = standard (mono RS (fp_def RS 

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

309 

310 
fun select_disj 1 1 = [] 

311 
 select_disj _ 1 = [rtac disjI1] 

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

313 

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

6394  315 
(cterm_of (Theory.sign_of thy) intr) (fn prems => 
5094  316 
[(*insert prems and underlying sets*) 
317 
cut_facts_tac prems 1, 

318 
stac unfold 1, 

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

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

321 
EVERY1 (select_disj (length intr_ts) i), 

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

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

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

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

326 
rewrite_goals_tac con_defs, 

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

328 

329 
in (intrs, unfold) end; 

330 

6424  331 

332 

333 
(** prove elimination rules **) 

5094  334 

335 
fun prove_elims cs cTs params intr_ts unfold rec_sets_defs thy = 

336 
let 

6427  337 
val _ = message " Proving the elimination rules ..."; 
5094  338 

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

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

341 
map make_elim [Inl_inject, Inr_inject]; 

342 

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

6394  344 
(cterm_of (Theory.sign_of thy) t) (fn prems => 
5094  345 
[cut_facts_tac [hd prems] 1, 
346 
dtac (unfold RS subst) 1, 

347 
REPEAT (FIRSTGOAL (eresolve_tac rules1)), 

348 
REPEAT (FIRSTGOAL (eresolve_tac rules2)), 

349 
EVERY (map (fn prem => 

5149  350 
DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))])) 
5094  351 
(mk_elims cs cTs params intr_ts) 
352 

353 
in elims end; 

354 

6424  355 

5094  356 
(** derivation of simplified elimination rules **) 
357 

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

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

360 
for inference systems. 

361 
*) 

6141  362 
fun con_elim_tac ss = 
5094  363 
let val elim_tac = REPEAT o (eresolve_tac elim_rls) 
364 
in ALLGOALS(EVERY'[elim_tac, 

6141  365 
asm_full_simp_tac ss, 
366 
elim_tac, 

367 
REPEAT o bound_hyp_subst_tac]) 

5094  368 
THEN prune_params_tac 
369 
end; 

370 

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

6141  372 
fun mk_cases elims s = 
6394  373 
let val prem = assume (read_cterm (Thm.sign_of_thm (hd elims)) (s, propT)) 
6141  374 
fun mk_elim rl = rule_by_tactic (con_elim_tac (simpset())) (prem RS rl) 
375 
> standard 

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

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

379 
end; 

380 

6424  381 

382 

383 
(** prove induction rule **) 

5094  384 

385 
fun prove_indrule cs cTs sumT rec_const params intr_ts mono 

386 
fp_def rec_sets_defs thy = 

387 
let 

6427  388 
val _ = message " Proving the induction rule ..."; 
5094  389 

6394  390 
val sign = Theory.sign_of thy; 
5094  391 

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

393 

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

395 

396 
fun mk_ind_pred _ [P] = P 

397 
 mk_ind_pred T Ps = 

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

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

400 
in Const ("sum_case", 

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

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

403 
end; 

404 

405 
val ind_pred = mk_ind_pred sumT preds; 

406 

407 
val ind_concl = HOLogic.mk_Trueprop 

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

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

410 

411 
(* simplification rules for vimage and Collect *) 

412 

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

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

415 
(HOLogic.mk_Trueprop (HOLogic.mk_eq 

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

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

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

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

5553  420 
(map mk_meta_eq [sum_case_Inl, sum_case_Inr]), 
5094  421 
rtac refl 1])) cs; 
422 

423 
val induct = prove_goalw_cterm [] (cterm_of sign 

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

425 
[rtac (impI RS allI) 1, 

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

5553  427 
rewrite_goals_tac (map mk_meta_eq (vimage_Int::vimage_simps)), 
5094  428 
fold_goals_tac rec_sets_defs, 
429 
(*This CollectE and disjE separates out the introduction rules*) 

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

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

432 
some premise involves disjunction.*) 

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

434 
ORELSE' hyp_subst_tac)), 

5553  435 
rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]), 
5094  436 
EVERY (map (fn prem => 
5149  437 
DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]); 
5094  438 

439 
val lemma = prove_goalw_cterm rec_sets_defs (cterm_of sign 

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

441 
[cut_facts_tac prems 1, 

442 
REPEAT (EVERY 

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

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

5553  445 
rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]), 
5094  446 
atac 1])]) 
447 

448 
in standard (split_rule (induct RS lemma)) 

449 
end; 

450 

6424  451 

452 

453 
(*** specification of (co)inductive sets ****) 

454 

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

5094  456 

457 
fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs 

6521  458 
atts intros monos con_defs thy params paramTs cTs cnames = 
5094  459 
let 
6424  460 
val _ = if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^ 
461 
commas_quote cnames) else (); 

5094  462 

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

464 
val setT = HOLogic.mk_setT sumT; 

465 

6394  466 
val fp_name = if coind then Sign.intern_const (Theory.sign_of Gfp.thy) "gfp" 
467 
else Sign.intern_const (Theory.sign_of Lfp.thy) "lfp"; 

5094  468 

6424  469 
val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros); 
470 

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

473 

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

476 
(* is transformed into *) 

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

478 

479 
fun transform_rule r = 

480 
let 

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

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

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

486 

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

488 
(frees, foldr1 (app HOLogic.conj) 

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

492 
end 

493 

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

495 

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

5094  498 

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

500 

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

6394  502 
val full_rec_name = Sign.full_name (Theory.sign_of thy) rec_name; 
5094  503 

504 
val rec_const = list_comb 

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

506 

507 
val fp_def_term = Logic.mk_equals (rec_const, 

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

509 

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

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

512 

513 
val thy' = thy > 

514 
(if declare_consts then 

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

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

517 
else I) > 

518 
(if length cs < 2 then I else 

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

520 
Theory.add_path rec_name > 

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

522 

523 
(* get definitions from theory *) 

524 

6424  525 
val fp_def::rec_sets_defs = PureThy.get_thms thy' "defs"; 
5094  526 

527 
(* prove and store theorems *) 

528 

529 
val mono = prove_mono setT fp_fun monos thy'; 

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

531 
rec_sets_defs thy'; 

532 
val elims = if no_elim then [] else 

533 
prove_elims cs cTs params intr_ts unfold rec_sets_defs thy'; 

534 
val raw_induct = if no_ind then TrueI else 

535 
if coind then standard (rule_by_tactic 

5553  536 
(rewrite_tac [mk_meta_eq vimage_Un] THEN 
5094  537 
fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct))) 
538 
else 

539 
prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def 

540 
rec_sets_defs thy'; 

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

6424  544 
val thy'' = thy' 
6521  545 
> PureThy.add_thmss [(("intrs", intrs), atts)] 
6424  546 
> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts) 
547 
> (if no_elim then I else PureThy.add_thmss [(("elims", elims), [])]) 

548 
> (if no_ind then I else PureThy.add_thms 

549 
[((coind_prefix coind ^ "induct", induct), [])]) 

550 
> Theory.parent_path; 

5094  551 

552 
in (thy'', 

553 
{defs = fp_def::rec_sets_defs, 

554 
mono = mono, 

555 
unfold = unfold, 

556 
intrs = intrs, 

557 
elims = elims, 

558 
mk_cases = mk_cases elims, 

559 
raw_induct = raw_induct, 

560 
induct = induct}) 

561 
end; 

562 

6424  563 

564 

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

5094  566 

567 
fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs 

6521  568 
atts intros monos con_defs thy params paramTs cTs cnames = 
5094  569 
let 
6424  570 
val _ = if verbose then message ("Adding axioms for " ^ coind_prefix coind ^ 
571 
"inductive set(s) " ^ commas_quote cnames) else (); 

5094  572 

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

574 

6424  575 
val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros); 
5094  576 
val elim_ts = mk_elims cs cTs params intr_ts; 
577 

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

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

580 

6424  581 
val thy' = thy 
582 
> (if declare_consts then 

583 
Theory.add_consts_i 

584 
(map (fn (c, n) => (n, paramTs > fastype_of c, NoSyn)) (cs ~~ cnames)) 

585 
else I) 

586 
> Theory.add_path rec_name 

6521  587 
> PureThy.add_axiomss_i [(("intrs", intr_ts), atts), (("elims", elim_ts), [])] 
6424  588 
> (if coind then I else PureThy.add_axioms_i [(("internal_induct", ind_t), [])]); 
5094  589 

6424  590 
val intrs = PureThy.get_thms thy' "intrs"; 
591 
val elims = PureThy.get_thms thy' "elims"; 

5094  592 
val raw_induct = if coind then TrueI else 
6424  593 
standard (split_rule (PureThy.get_thm thy' "internal_induct")); 
5094  594 
val induct = if coind orelse length cs > 1 then raw_induct 
595 
else standard (raw_induct RSN (2, rev_mp)); 

596 

6424  597 
val thy'' = 
598 
thy' 

599 
> (if coind then I else PureThy.add_thms [(("induct", induct), [])]) 

600 
> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts) 

601 
> Theory.parent_path; 

5094  602 
in (thy'', 
603 
{defs = [], 

604 
mono = TrueI, 

605 
unfold = TrueI, 

606 
intrs = intrs, 

607 
elims = elims, 

608 
mk_cases = mk_cases elims, 

609 
raw_induct = raw_induct, 

610 
induct = induct}) 

611 
end; 

612 

6424  613 

614 

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

5094  616 

617 
fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs 

6521  618 
atts intros monos con_defs thy = 
5094  619 
let 
6424  620 
val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions"); 
6394  621 
val sign = Theory.sign_of thy; 
5094  622 

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

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

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

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

627 

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

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

630 

6437  631 
val full_cnames = map (try' (fst o dest_Const o head_of) 
5094  632 
"Recursive set not previously declared as constant: " sign) cs; 
6437  633 
val cnames = map Sign.base_name full_cnames; 
5094  634 

6424  635 
val _ = assert_all Syntax.is_identifier cnames (* FIXME why? *) 
5094  636 
(fn a => "Base name of recursive set not an identifier: " ^ a); 
6424  637 
val _ = seq (check_rule sign cs o snd o fst) intros; 
6437  638 

639 
val (thy1, result) = 

640 
(if ! quick_and_dirty then add_ind_axm else add_ind_def) 

6521  641 
verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos 
6437  642 
con_defs thy params paramTs cTs cnames; 
643 
val thy2 = thy1 > put_inductives full_cnames ({names = full_cnames, coind = coind}, result); 

644 
in (thy2, result) end; 

5094  645 

6424  646 

5094  647 

6424  648 
(** external interface **) 
649 

6521  650 
fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy = 
5094  651 
let 
6394  652 
val sign = Theory.sign_of thy; 
653 
val cs = map (readtm (Theory.sign_of thy) HOLogic.termTVar) c_strings; 

6424  654 

6521  655 
val atts = map (Attrib.global_attribute thy) srcs; 
6424  656 
val intr_names = map (fst o fst) intro_srcs; 
657 
val intr_ts = map (readtm (Theory.sign_of thy) propT o snd o fst) intro_srcs; 

658 
val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs; 

5094  659 

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

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

662 

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

664 
val add_term_consts_2 = 

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

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

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

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

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

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

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

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

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

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

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

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

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

678 
"' have incompatible types") 

679 
end; 

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

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

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

683 
val subst = fst o Type.freeze_thaw o 

684 
(map_term_types (typ_subst_TVars_2 env)); 

685 
val cs'' = map subst cs'; 

686 
val intr_ts'' = map subst intr_ts'; 

687 

6424  688 
val ((thy', con_defs), monos) = thy 
689 
> IsarThy.apply_theorems raw_monos 

690 
> apfst (IsarThy.apply_theorems raw_con_defs); 

691 
in 

692 
add_inductive_i verbose false "" coind false false cs'' 

6521  693 
atts ((intr_names ~~ intr_ts'') ~~ intr_atts) monos con_defs thy' 
5094  694 
end; 
695 

6424  696 

697 

6437  698 
(** package setup **) 
699 

700 
(* setup theory *) 

701 

702 
val setup = [InductiveData.init]; 

703 

704 

705 
(* outer syntax *) 

6424  706 

6723  707 
local structure P = OuterParse and K = OuterSyntax.Keyword in 
6424  708 

6521  709 
fun mk_ind coind (((sets, (atts, intrs)), monos), con_defs) = 
6723  710 
#1 o add_inductive true coind sets atts (map P.triple_swap intrs) monos con_defs; 
6424  711 

712 
fun ind_decl coind = 

6729  713 
(Scan.repeat1 P.term  P.marg_comment)  
714 
(P.$$$ "intrs"  

715 
P.!!! (P.opt_attribs  Scan.repeat1 (P.opt_thm_name ":"  P.term  P.marg_comment)))  

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

717 
Scan.optional (P.$$$ "con_defs"  P.!!! P.xthms1  P.marg_comment) [] 

6424  718 
>> (Toplevel.theory o mk_ind coind); 
719 

6723  720 
val inductiveP = 
721 
OuterSyntax.command "inductive" "define inductive sets" K.thy_decl (ind_decl false); 

722 

723 
val coinductiveP = 

724 
OuterSyntax.command "coinductive" "define coinductive sets" K.thy_decl (ind_decl true); 

6424  725 

726 
val _ = OuterSyntax.add_keywords ["intrs", "monos", "con_defs"]; 

727 
val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP]; 

728 

5094  729 
end; 
6424  730 

731 

732 
end; 