author  berghofe 
Thu, 19 Aug 1999 19:00:42 +0200  
changeset 7293  959e060f4a2f 
parent 7257  745cfc8871e2 
child 7349  228b711ad68c 
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 
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

34 
val unify_consts: Sign.sg > term list > term list > term list * term list 
6437  35 
val get_inductive: theory > string > 
36 
{names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm, 

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

38 
val print_inductives: theory > unit 

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

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

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

6424  47 
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm, 
6437  48 
intrs: thm list, mk_cases: string > thm, mono: thm, unfold: thm} 
7107  49 
val inductive_cases: (((bstring * Args.src list) * xstring) * string list) * Comment.text 
50 
> theory > theory 

51 
val inductive_cases_i: (((bstring * theory attribute list) * string) * term list) * Comment.text 

52 
> theory > theory 

6437  53 
val setup: (theory > theory) list 
5094  54 
end; 
55 

6424  56 
structure InductivePackage: INDUCTIVE_PACKAGE = 
5094  57 
struct 
58 

7107  59 

6424  60 
(** utilities **) 
61 

62 
(* messages *) 

63 

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

66 

6424  67 
fun coind_prefix true = "co" 
68 
 coind_prefix false = ""; 

69 

70 

7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

71 
(* the following code ensures that each recursive set *) 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

72 
(* always has the same type in all introduction rules *) 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

73 

75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

74 
fun unify_consts sign cs intr_ts = 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

75 
(let 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

76 
val {tsig, ...} = Sign.rep_sg sign; 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

77 
val add_term_consts_2 = 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

78 
foldl_aterms (fn (cs, Const c) => c ins cs  (cs, _) => cs); 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

79 
fun varify (t, (i, ts)) = 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

80 
let val t' = map_term_types (incr_tvar (i + 1)) (Type.varify (t, [])) 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

81 
in (maxidx_of_term t', t'::ts) end; 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

82 
val (i, cs') = foldr varify (cs, (~1, [])); 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

83 
val (i', intr_ts') = foldr varify (intr_ts, (i, [])); 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

84 
val rec_consts = foldl add_term_consts_2 ([], cs'); 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

85 
val intr_consts = foldl add_term_consts_2 ([], intr_ts'); 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

86 
fun unify (env, (cname, cT)) = 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

87 
let val consts = map snd (filter (fn c => fst c = cname) intr_consts) 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

88 
in foldl (fn ((env', j'), Tp) => (Type.unify tsig j' env' Tp)) 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

89 
(env, (replicate (length consts) cT) ~~ consts) 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

90 
end; 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

91 
val (env, _) = foldl unify (([], i'), rec_consts); 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

92 
fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars env T 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

93 
in if T = T' then T else typ_subst_TVars_2 env T' end; 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

94 
val subst = fst o Type.freeze_thaw o 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

95 
(map_term_types (typ_subst_TVars_2 env)) 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

96 

75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

97 
in (map subst cs', map subst intr_ts') 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

98 
end) handle Type.TUNIFY => 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

99 
(warning "Occurrences of recursive constant have nonunifiable types"; (cs, intr_ts)); 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

100 

75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

101 

6424  102 
(* misc *) 
103 

7107  104 
(*for proving monotonicity of recursion operator*) 
105 
val default_monos = basic_monos @ [vimage_mono]; 

5094  106 

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

108 

109 
(*Delete needless equality assumptions*) 

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

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

112 

113 
(*For simplifying the elimination rule*) 

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

114 
val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject]; 
5094  115 

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

5094  118 

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

120 

121 
fun mk_inj cs sumT c x = 

122 
let 

123 
fun mk_inj' T n i = 

124 
if n = 1 then x else 

125 
let val n2 = n div 2; 

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

127 
in 

128 
if i <= n2 then 

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

130 
else 

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

132 
end 

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

134 
end; 

135 

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

137 

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

139 
let 

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

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

142 
in 

143 
Const (vimage_name, vimageT) $ 

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

145 
end; 

146 

6424  147 

148 

149 
(** wellformedness checks **) 

5094  150 

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

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

153 

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

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

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

157 

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

159 
\ ' t : S_i '"; 

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

161 
\ ' t : M S_i '"; 

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

163 

164 
fun check_rule sign cs r = 

165 
let 

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

167 
(case prem of 

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

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

170 
err_in_prem sign r prem msg3 else () 

171 
 _ => err_in_prem sign r prem msg2) 

172 
else () 

173 

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

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

6424  176 
if u mem cs then seq (check_prem o HOLogic.dest_Trueprop) 
5094  177 
(Logic.strip_imp_prems r) 
178 
else err_in_rule sign r msg1 

179 
 _ => err_in_rule sign r msg1) 

180 
end; 

181 

7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

182 
fun try' f msg sign t = (case (try f t) of 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

183 
Some x => x 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

184 
 None => error (msg ^ Sign.string_of_term sign t)); 
5094  185 

6424  186 

5094  187 

6437  188 
(*** theory data ***) 
189 

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

191 

192 
type inductive_info = 

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

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

195 

196 
structure InductiveArgs = 

197 
struct 

198 
val name = "HOL/inductive"; 

199 
type T = inductive_info Symtab.table; 

200 

201 
val empty = Symtab.empty; 

6556  202 
val copy = I; 
6437  203 
val prep_ext = I; 
204 
val merge: T * T > T = Symtab.merge (K true); 

205 

206 
fun print sg tab = 

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

6851  208 
map #1 (Sign.cond_extern_table sg Sign.constK tab))); 
6437  209 
end; 
210 

211 
structure InductiveData = TheoryDataFun(InductiveArgs); 

212 
val print_inductives = InductiveData.print; 

213 

214 

215 
(* get and put data *) 

216 

217 
fun get_inductive thy name = 

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

219 
Some info => info 

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

221 

222 
fun put_inductives names info thy = 

223 
let 

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

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

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

227 
in InductiveData.put tab thy end; 

228 

229 

230 

6424  231 
(*** properties of (co)inductive sets ***) 
232 

233 
(** elimination rules **) 

5094  234 

235 
fun mk_elims cs cTs params intr_ts = 

236 
let 

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

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

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

240 

241 
fun dest_intr r = 

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

243 
HOLogic.dest_Trueprop (Logic.strip_imp_concl r) 

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

245 

246 
val intrs = map dest_intr intr_ts; 

247 

248 
fun mk_elim (c, T) = 

249 
let 

250 
val a = Free (aname, T); 

251 

252 
fun mk_elim_prem (_, t, ts) = 

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

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

255 
in 

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

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

258 
end 

259 
in 

260 
map mk_elim (cs ~~ cTs) 

261 
end; 

262 

6424  263 

264 

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

5094  266 

267 
fun mk_indrule cs cTs params intr_ts = 

268 
let 

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

270 

271 
(* predicates for induction rule *) 

272 

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

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

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

276 

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

278 

279 
fun mk_ind_prem r = 

280 
let 

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

282 

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

284 
let val n = find_index_eq u cs in 

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

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

287 
(c, HOLogic.Collect_const (HOLogic.dest_setT 

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

289 
end 

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

291 

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

293 
HOLogic.dest_Trueprop (Logic.strip_imp_concl r) 

294 

295 
in list_all_free (frees, 

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

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

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

299 
end; 

300 

301 
val ind_prems = map mk_ind_prem intr_ts; 

302 

303 
(* make conclusions for induction rules *) 

304 

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

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

307 
val Ts = HOLogic.prodT_factors T; 

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

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

310 
val tuple = HOLogic.mk_tuple T frees; 

311 
in ((HOLogic.mk_binop "op >" 

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

313 
end; 

314 

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

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

317 

318 
in (preds, ind_prems, mutual_ind_concl) 

319 
end; 

320 

6424  321 

5094  322 

6424  323 
(*** proofs for (co)inductive sets ***) 
324 

325 
(** prove monotonicity **) 

5094  326 

327 
fun prove_mono setT fp_fun monos thy = 

328 
let 

6427  329 
val _ = message " Proving monotonicity ..."; 
5094  330 

6394  331 
val mono = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop 
5094  332 
(Const (mono_name, (setT > setT) > HOLogic.boolT) $ fp_fun))) 
7107  333 
(fn _ => [rtac monoI 1, REPEAT (ares_tac (default_monos @ monos) 1)]) 
5094  334 

335 
in mono end; 

336 

6424  337 

338 

339 
(** prove introduction rules **) 

5094  340 

341 
fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy = 

342 
let 

6427  343 
val _ = message " Proving the introduction rules ..."; 
5094  344 

345 
val unfold = standard (mono RS (fp_def RS 

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

347 

348 
fun select_disj 1 1 = [] 

349 
 select_disj _ 1 = [rtac disjI1] 

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

351 

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

6394  353 
(cterm_of (Theory.sign_of thy) intr) (fn prems => 
5094  354 
[(*insert prems and underlying sets*) 
355 
cut_facts_tac prems 1, 

356 
stac unfold 1, 

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

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

359 
EVERY1 (select_disj (length intr_ts) i), 

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

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

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

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

364 
rewrite_goals_tac con_defs, 

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

366 

367 
in (intrs, unfold) end; 

368 

6424  369 

370 

371 
(** prove elimination rules **) 

5094  372 

373 
fun prove_elims cs cTs params intr_ts unfold rec_sets_defs thy = 

374 
let 

6427  375 
val _ = message " Proving the elimination rules ..."; 
5094  376 

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

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

379 
map make_elim [Inl_inject, Inr_inject]; 

380 

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

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

385 
REPEAT (FIRSTGOAL (eresolve_tac rules1)), 

386 
REPEAT (FIRSTGOAL (eresolve_tac rules2)), 

387 
EVERY (map (fn prem => 

5149  388 
DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))])) 
5094  389 
(mk_elims cs cTs params intr_ts) 
390 

391 
in elims end; 

392 

6424  393 

5094  394 
(** derivation of simplified elimination rules **) 
395 

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

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

398 
for inference systems. 

399 
*) 

6141  400 
fun con_elim_tac ss = 
5094  401 
let val elim_tac = REPEAT o (eresolve_tac elim_rls) 
402 
in ALLGOALS(EVERY'[elim_tac, 

6141  403 
asm_full_simp_tac ss, 
404 
elim_tac, 

405 
REPEAT o bound_hyp_subst_tac]) 

5094  406 
THEN prune_params_tac 
407 
end; 

408 

7107  409 
(*cprop should have the form t:Si where Si is an inductive set*) 
410 
fun mk_cases_i elims ss cprop = 

411 
let 

412 
val prem = Thm.assume cprop; 

413 
fun mk_elim rl = standard (rule_by_tactic (con_elim_tac ss) (prem RS rl)); 

414 
in 

415 
(case get_first (try mk_elim) elims of 

416 
Some r => r 

417 
 None => error (Pretty.string_of (Pretty.block 

418 
[Pretty.str "mk_cases: proposition not of form 't : S_i'", Pretty.fbrk, 

419 
Display.pretty_cterm cprop]))) 

420 
end; 

421 

6141  422 
fun mk_cases elims s = 
7107  423 
mk_cases_i elims (simpset()) (Thm.read_cterm (Thm.sign_of_thm (hd elims)) (s, propT)); 
424 

425 

426 
(* inductive_cases(_i) *) 

427 

428 
fun gen_inductive_cases prep_att prep_const prep_prop 

429 
((((name, raw_atts), raw_set), raw_props), comment) thy = 

430 
let 

431 
val sign = Theory.sign_of thy; 

432 

433 
val atts = map (prep_att thy) raw_atts; 

434 
val (_, {elims, ...}) = get_inductive thy (prep_const sign raw_set); 

435 
val cprops = map (Thm.cterm_of sign o prep_prop (ProofContext.init thy)) raw_props; 

436 
val thms = map (mk_cases_i elims (Simplifier.simpset_of thy)) cprops; 

437 
in 

438 
thy 

439 
> IsarThy.have_theorems_i (((name, atts), map Thm.no_attributes thms), comment) 

5094  440 
end; 
441 

7107  442 
val inductive_cases = 
443 
gen_inductive_cases Attrib.global_attribute Sign.intern_const ProofContext.read_prop; 

444 

445 
val inductive_cases_i = gen_inductive_cases (K I) (K I) ProofContext.cert_prop; 

446 

6424  447 

448 

449 
(** prove induction rule **) 

5094  450 

451 
fun prove_indrule cs cTs sumT rec_const params intr_ts mono 

452 
fp_def rec_sets_defs thy = 

453 
let 

6427  454 
val _ = message " Proving the induction rule ..."; 
5094  455 

6394  456 
val sign = Theory.sign_of thy; 
5094  457 

7293  458 
val sum_case_rewrites = (case ThyInfo.lookup_theory "Datatype" of 
459 
None => [] 

460 
 Some thy' => map mk_meta_eq (PureThy.get_thms thy' "sum.cases")); 

461 

5094  462 
val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts; 
463 

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

465 

466 
fun mk_ind_pred _ [P] = P 

467 
 mk_ind_pred T Ps = 

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

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

7293  470 
in Const ("Datatype.sum.sum_case", 
5094  471 
[T1 > HOLogic.boolT, T2 > HOLogic.boolT, T] > HOLogic.boolT) $ 
472 
mk_ind_pred T1 (take (n, Ps)) $ mk_ind_pred T2 (drop (n, Ps)) 

473 
end; 

474 

475 
val ind_pred = mk_ind_pred sumT preds; 

476 

477 
val ind_concl = HOLogic.mk_Trueprop 

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

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

480 

481 
(* simplification rules for vimage and Collect *) 

482 

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

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

485 
(HOLogic.mk_Trueprop (HOLogic.mk_eq 

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

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

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

7293  489 
(fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, 
5094  490 
rtac refl 1])) cs; 
491 

492 
val induct = prove_goalw_cterm [] (cterm_of sign 

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

494 
[rtac (impI RS allI) 1, 

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

5553  496 
rewrite_goals_tac (map mk_meta_eq (vimage_Int::vimage_simps)), 
5094  497 
fold_goals_tac rec_sets_defs, 
498 
(*This CollectE and disjE separates out the introduction rules*) 

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

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

501 
some premise involves disjunction.*) 

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

503 
ORELSE' hyp_subst_tac)), 

7293  504 
rewrite_goals_tac sum_case_rewrites, 
5094  505 
EVERY (map (fn prem => 
5149  506 
DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]); 
5094  507 

508 
val lemma = prove_goalw_cterm rec_sets_defs (cterm_of sign 

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

510 
[cut_facts_tac prems 1, 

511 
REPEAT (EVERY 

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

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

7293  514 
rewrite_goals_tac sum_case_rewrites, 
5094  515 
atac 1])]) 
516 

517 
in standard (split_rule (induct RS lemma)) 

518 
end; 

519 

6424  520 

521 

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

523 

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

5094  525 

526 
fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs 

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

5094  531 

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

533 
val setT = HOLogic.mk_setT sumT; 

534 

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

5094  537 

6424  538 
val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros); 
539 

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

542 

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

545 
(* is transformed into *) 

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

547 

548 
fun transform_rule r = 

549 
let 

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

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

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

555 

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

557 
(frees, foldr1 (app HOLogic.conj) 

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

561 
end 

562 

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

564 

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

5094  567 

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

569 

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

6394  571 
val full_rec_name = Sign.full_name (Theory.sign_of thy) rec_name; 
5094  572 

573 
val rec_const = list_comb 

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

575 

576 
val fp_def_term = Logic.mk_equals (rec_const, 

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

578 

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

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

581 

582 
val thy' = thy > 

583 
(if declare_consts then 

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

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

586 
else I) > 

587 
(if length cs < 2 then I else 

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

589 
Theory.add_path rec_name > 

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

591 

592 
(* get definitions from theory *) 

593 

6424  594 
val fp_def::rec_sets_defs = PureThy.get_thms thy' "defs"; 
5094  595 

596 
(* prove and store theorems *) 

597 

598 
val mono = prove_mono setT fp_fun monos thy'; 

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

600 
rec_sets_defs thy'; 

601 
val elims = if no_elim then [] else 

602 
prove_elims cs cTs params intr_ts unfold rec_sets_defs thy'; 

603 
val raw_induct = if no_ind then TrueI else 

604 
if coind then standard (rule_by_tactic 

5553  605 
(rewrite_tac [mk_meta_eq vimage_Un] THEN 
5094  606 
fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct))) 
607 
else 

608 
prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def 

609 
rec_sets_defs thy'; 

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

6424  613 
val thy'' = thy' 
6521  614 
> PureThy.add_thmss [(("intrs", intrs), atts)] 
6424  615 
> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts) 
616 
> (if no_elim then I else PureThy.add_thmss [(("elims", elims), [])]) 

617 
> (if no_ind then I else PureThy.add_thms 

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

619 
> Theory.parent_path; 

5094  620 

621 
in (thy'', 

622 
{defs = fp_def::rec_sets_defs, 

623 
mono = mono, 

624 
unfold = unfold, 

625 
intrs = intrs, 

626 
elims = elims, 

627 
mk_cases = mk_cases elims, 

628 
raw_induct = raw_induct, 

629 
induct = induct}) 

630 
end; 

631 

6424  632 

633 

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

5094  635 

636 
fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs 

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

5094  641 

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

643 

6424  644 
val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros); 
5094  645 
val elim_ts = mk_elims cs cTs params intr_ts; 
646 

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

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

649 

6424  650 
val thy' = thy 
651 
> (if declare_consts then 

652 
Theory.add_consts_i 

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

654 
else I) 

655 
> Theory.add_path rec_name 

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

6424  659 
val intrs = PureThy.get_thms thy' "intrs"; 
660 
val elims = PureThy.get_thms thy' "elims"; 

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

665 

6424  666 
val thy'' = 
667 
thy' 

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

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

670 
> Theory.parent_path; 

5094  671 
in (thy'', 
672 
{defs = [], 

673 
mono = TrueI, 

674 
unfold = TrueI, 

675 
intrs = intrs, 

676 
elims = elims, 

677 
mk_cases = mk_cases elims, 

678 
raw_induct = raw_induct, 

679 
induct = induct}) 

680 
end; 

681 

6424  682 

683 

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

5094  685 

686 
fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs 

6521  687 
atts intros monos con_defs thy = 
5094  688 
let 
6424  689 
val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions"); 
6394  690 
val sign = Theory.sign_of thy; 
5094  691 

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

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

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

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

696 

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

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

699 

6437  700 
val full_cnames = map (try' (fst o dest_Const o head_of) 
5094  701 
"Recursive set not previously declared as constant: " sign) cs; 
6437  702 
val cnames = map Sign.base_name full_cnames; 
5094  703 

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

708 
val (thy1, result) = 

709 
(if ! quick_and_dirty then add_ind_axm else add_ind_def) 

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

713 
in (thy2, result) end; 

5094  714 

6424  715 

5094  716 

6424  717 
(** external interface **) 
718 

6521  719 
fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy = 
5094  720 
let 
6394  721 
val sign = Theory.sign_of thy; 
722 
val cs = map (readtm (Theory.sign_of thy) HOLogic.termTVar) c_strings; 

6424  723 

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

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

7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

728 
val (cs', intr_ts') = unify_consts sign cs intr_ts; 
5094  729 

6424  730 
val ((thy', con_defs), monos) = thy 
731 
> IsarThy.apply_theorems raw_monos 

732 
> apfst (IsarThy.apply_theorems raw_con_defs); 

733 
in 

7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

734 
add_inductive_i verbose false "" coind false false cs' 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

735 
atts ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy' 
5094  736 
end; 
737 

6424  738 

739 

6437  740 
(** package setup **) 
741 

742 
(* setup theory *) 

743 

744 
val setup = [InductiveData.init]; 

745 

746 

747 
(* outer syntax *) 

6424  748 

6723  749 
local structure P = OuterParse and K = OuterSyntax.Keyword in 
6424  750 

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

754 
fun ind_decl coind = 

6729  755 
(Scan.repeat1 P.term  P.marg_comment)  
756 
(P.$$$ "intrs"  

7152  757 
P.!!! (P.opt_attribs  Scan.repeat1 (P.opt_thm_name ":"  P.prop  P.marg_comment)))  
6729  758 
Scan.optional (P.$$$ "monos"  P.!!! P.xthms1  P.marg_comment) []  
759 
Scan.optional (P.$$$ "con_defs"  P.!!! P.xthms1  P.marg_comment) [] 

6424  760 
>> (Toplevel.theory o mk_ind coind); 
761 

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

764 

765 
val coinductiveP = 

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

6424  767 

7107  768 

769 
val ind_cases = 

770 
P.opt_thm_name "="  P.xname  P.$$$ ":"  Scan.repeat1 P.prop  P.marg_comment 

771 
>> (Toplevel.theory o inductive_cases); 

772 

773 
val inductive_casesP = 

774 
OuterSyntax.command "inductive_cases" "create simplified instances of elimination rules" 

775 
K.thy_decl ind_cases; 

776 

6424  777 
val _ = OuterSyntax.add_keywords ["intrs", "monos", "con_defs"]; 
7107  778 
val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP]; 
6424  779 

5094  780 
end; 
6424  781 

782 

783 
end; 