author  wenzelm 
Mon, 02 Aug 1999 17:58:23 +0200  
changeset 7152  44d46a112127 
parent 7107  ce69de572bca 
child 7257  745cfc8871e2 
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 

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

459 

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

461 

462 
fun mk_ind_pred _ [P] = P 

463 
 mk_ind_pred T Ps = 

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

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

466 
in Const ("sum_case", 

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

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

469 
end; 

470 

471 
val ind_pred = mk_ind_pred sumT preds; 

472 

473 
val ind_concl = HOLogic.mk_Trueprop 

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

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

476 

477 
(* simplification rules for vimage and Collect *) 

478 

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

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

481 
(HOLogic.mk_Trueprop (HOLogic.mk_eq 

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

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

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

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

5553  486 
(map mk_meta_eq [sum_case_Inl, sum_case_Inr]), 
5094  487 
rtac refl 1])) cs; 
488 

489 
val induct = prove_goalw_cterm [] (cterm_of sign 

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

491 
[rtac (impI RS allI) 1, 

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

5553  493 
rewrite_goals_tac (map mk_meta_eq (vimage_Int::vimage_simps)), 
5094  494 
fold_goals_tac rec_sets_defs, 
495 
(*This CollectE and disjE separates out the introduction rules*) 

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

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

498 
some premise involves disjunction.*) 

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

500 
ORELSE' hyp_subst_tac)), 

5553  501 
rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]), 
5094  502 
EVERY (map (fn prem => 
5149  503 
DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]); 
5094  504 

505 
val lemma = prove_goalw_cterm rec_sets_defs (cterm_of sign 

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

507 
[cut_facts_tac prems 1, 

508 
REPEAT (EVERY 

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

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

5553  511 
rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]), 
5094  512 
atac 1])]) 
513 

514 
in standard (split_rule (induct RS lemma)) 

515 
end; 

516 

6424  517 

518 

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

520 

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

5094  522 

523 
fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs 

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

5094  528 

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

530 
val setT = HOLogic.mk_setT sumT; 

531 

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

5094  534 

6424  535 
val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros); 
536 

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

539 

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

542 
(* is transformed into *) 

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

544 

545 
fun transform_rule r = 

546 
let 

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

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

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

552 

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

554 
(frees, foldr1 (app HOLogic.conj) 

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

558 
end 

559 

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

561 

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

5094  564 

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

566 

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

6394  568 
val full_rec_name = Sign.full_name (Theory.sign_of thy) rec_name; 
5094  569 

570 
val rec_const = list_comb 

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

572 

573 
val fp_def_term = Logic.mk_equals (rec_const, 

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

575 

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

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

578 

579 
val thy' = thy > 

580 
(if declare_consts then 

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

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

583 
else I) > 

584 
(if length cs < 2 then I else 

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

586 
Theory.add_path rec_name > 

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

588 

589 
(* get definitions from theory *) 

590 

6424  591 
val fp_def::rec_sets_defs = PureThy.get_thms thy' "defs"; 
5094  592 

593 
(* prove and store theorems *) 

594 

595 
val mono = prove_mono setT fp_fun monos thy'; 

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

597 
rec_sets_defs thy'; 

598 
val elims = if no_elim then [] else 

599 
prove_elims cs cTs params intr_ts unfold rec_sets_defs thy'; 

600 
val raw_induct = if no_ind then TrueI else 

601 
if coind then standard (rule_by_tactic 

5553  602 
(rewrite_tac [mk_meta_eq vimage_Un] THEN 
5094  603 
fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct))) 
604 
else 

605 
prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def 

606 
rec_sets_defs thy'; 

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

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

614 
> (if no_ind then I else PureThy.add_thms 

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

616 
> Theory.parent_path; 

5094  617 

618 
in (thy'', 

619 
{defs = fp_def::rec_sets_defs, 

620 
mono = mono, 

621 
unfold = unfold, 

622 
intrs = intrs, 

623 
elims = elims, 

624 
mk_cases = mk_cases elims, 

625 
raw_induct = raw_induct, 

626 
induct = induct}) 

627 
end; 

628 

6424  629 

630 

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

5094  632 

633 
fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs 

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

5094  638 

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

640 

6424  641 
val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros); 
5094  642 
val elim_ts = mk_elims cs cTs params intr_ts; 
643 

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

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

646 

6424  647 
val thy' = thy 
648 
> (if declare_consts then 

649 
Theory.add_consts_i 

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

651 
else I) 

652 
> Theory.add_path rec_name 

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

6424  656 
val intrs = PureThy.get_thms thy' "intrs"; 
657 
val elims = PureThy.get_thms thy' "elims"; 

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

662 

6424  663 
val thy'' = 
664 
thy' 

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

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

667 
> Theory.parent_path; 

5094  668 
in (thy'', 
669 
{defs = [], 

670 
mono = TrueI, 

671 
unfold = TrueI, 

672 
intrs = intrs, 

673 
elims = elims, 

674 
mk_cases = mk_cases elims, 

675 
raw_induct = raw_induct, 

676 
induct = induct}) 

677 
end; 

678 

6424  679 

680 

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

5094  682 

683 
fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs 

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

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

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

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

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

693 

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

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

696 

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

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

705 
val (thy1, result) = 

706 
(if ! quick_and_dirty then add_ind_axm else add_ind_def) 

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

710 
in (thy2, result) end; 

5094  711 

6424  712 

5094  713 

6424  714 
(** external interface **) 
715 

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

6424  720 

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

724 
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

725 
val (cs', intr_ts') = unify_consts sign cs intr_ts; 
5094  726 

6424  727 
val ((thy', con_defs), monos) = thy 
728 
> IsarThy.apply_theorems raw_monos 

729 
> apfst (IsarThy.apply_theorems raw_con_defs); 

730 
in 

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

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

732 
atts ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy' 
5094  733 
end; 
734 

6424  735 

736 

6437  737 
(** package setup **) 
738 

739 
(* setup theory *) 

740 

741 
val setup = [InductiveData.init]; 

742 

743 

744 
(* outer syntax *) 

6424  745 

6723  746 
local structure P = OuterParse and K = OuterSyntax.Keyword in 
6424  747 

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

751 
fun ind_decl coind = 

6729  752 
(Scan.repeat1 P.term  P.marg_comment)  
753 
(P.$$$ "intrs"  

7152  754 
P.!!! (P.opt_attribs  Scan.repeat1 (P.opt_thm_name ":"  P.prop  P.marg_comment)))  
6729  755 
Scan.optional (P.$$$ "monos"  P.!!! P.xthms1  P.marg_comment) []  
756 
Scan.optional (P.$$$ "con_defs"  P.!!! P.xthms1  P.marg_comment) [] 

6424  757 
>> (Toplevel.theory o mk_ind coind); 
758 

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

761 

762 
val coinductiveP = 

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

6424  764 

7107  765 

766 
val ind_cases = 

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

768 
>> (Toplevel.theory o inductive_cases); 

769 

770 
val inductive_casesP = 

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

772 
K.thy_decl ind_cases; 

773 

6424  774 
val _ = OuterSyntax.add_keywords ["intrs", "monos", "con_defs"]; 
7107  775 
val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP]; 
6424  776 

5094  777 
end; 
6424  778 

779 

780 
end; 