author | wenzelm |
Sat, 02 Sep 2000 21:49:51 +0200 | |
changeset 9803 | bc883b390d91 |
parent 9624 | de254f375477 |
child 9893 | 93d2fde0306c |
permissions | -rw-r--r-- |
6442 | 1 |
(* Title: HOL/Tools/induct_method.ML |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
9230 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
6442 | 5 |
|
8376 | 6 |
Proof by cases and induction on types and sets. |
6442 | 7 |
*) |
8 |
||
9 |
signature INDUCT_METHOD = |
|
10 |
sig |
|
8376 | 11 |
val dest_global_rules: theory -> |
12 |
{type_cases: (string * thm) list, set_cases: (string * thm) list, |
|
13 |
type_induct: (string * thm) list, set_induct: (string * thm) list} |
|
8308 | 14 |
val print_global_rules: theory -> unit |
8376 | 15 |
val dest_local_rules: Proof.context -> |
16 |
{type_cases: (string * thm) list, set_cases: (string * thm) list, |
|
17 |
type_induct: (string * thm) list, set_induct: (string * thm) list} |
|
8308 | 18 |
val print_local_rules: Proof.context -> unit |
8431 | 19 |
val vars_of: term -> term list |
8695 | 20 |
val concls_of: thm -> term list |
8308 | 21 |
val cases_type_global: string -> theory attribute |
22 |
val cases_set_global: string -> theory attribute |
|
23 |
val cases_type_local: string -> Proof.context attribute |
|
24 |
val cases_set_local: string -> Proof.context attribute |
|
25 |
val induct_type_global: string -> theory attribute |
|
26 |
val induct_set_global: string -> theory attribute |
|
27 |
val induct_type_local: string -> Proof.context attribute |
|
28 |
val induct_set_local: string -> Proof.context attribute |
|
9299 | 29 |
val simp_case_tac: bool -> simpset -> int -> tactic |
6442 | 30 |
val setup: (theory -> theory) list |
31 |
end; |
|
32 |
||
33 |
structure InductMethod: INDUCT_METHOD = |
|
34 |
struct |
|
35 |
||
8337 | 36 |
|
8308 | 37 |
(** global and local induct data **) |
6442 | 38 |
|
8308 | 39 |
(* rules *) |
40 |
||
41 |
type rules = (string * thm) NetRules.T; |
|
42 |
||
43 |
fun eq_rule ((s1:string, th1), (s2, th2)) = s1 = s2 andalso Thm.eq_thm (th1, th2); |
|
44 |
||
45 |
val type_rules = NetRules.init eq_rule (Thm.concl_of o #2); |
|
46 |
val set_rules = NetRules.init eq_rule (Thm.major_prem_of o #2); |
|
47 |
||
48 |
fun lookup_rule (rs:rules) name = Library.assoc (NetRules.rules rs, name); |
|
49 |
||
50 |
fun print_rules kind rs = |
|
51 |
let val thms = map snd (NetRules.rules rs) |
|
8315 | 52 |
in Pretty.writeln (Pretty.big_list kind (map Display.pretty_thm thms)) end; |
8308 | 53 |
|
54 |
||
55 |
(* theory data kind 'HOL/induct_method' *) |
|
56 |
||
57 |
structure GlobalInductArgs = |
|
58 |
struct |
|
59 |
val name = "HOL/induct_method"; |
|
60 |
type T = (rules * rules) * (rules * rules); |
|
61 |
||
62 |
val empty = ((type_rules, set_rules), (type_rules, set_rules)); |
|
63 |
val copy = I; |
|
64 |
val prep_ext = I; |
|
65 |
fun merge (((casesT1, casesS1), (inductT1, inductS1)), |
|
66 |
((casesT2, casesS2), (inductT2, inductS2))) = |
|
67 |
((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)), |
|
68 |
(NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2))); |
|
69 |
||
70 |
fun print _ ((casesT, casesS), (inductT, inductS)) = |
|
8315 | 71 |
(print_rules "type cases:" casesT; |
72 |
print_rules "set cases:" casesS; |
|
73 |
print_rules "type induct:" inductT; |
|
74 |
print_rules "set induct:" inductS); |
|
8376 | 75 |
|
76 |
fun dest ((casesT, casesS), (inductT, inductS)) = |
|
77 |
{type_cases = NetRules.rules casesT, |
|
78 |
set_cases = NetRules.rules casesS, |
|
79 |
type_induct = NetRules.rules inductT, |
|
80 |
set_induct = NetRules.rules inductS}; |
|
8308 | 81 |
end; |
82 |
||
83 |
structure GlobalInduct = TheoryDataFun(GlobalInductArgs); |
|
84 |
val print_global_rules = GlobalInduct.print; |
|
8376 | 85 |
val dest_global_rules = GlobalInductArgs.dest o GlobalInduct.get; |
8308 | 86 |
|
87 |
||
88 |
(* proof data kind 'HOL/induct_method' *) |
|
89 |
||
90 |
structure LocalInductArgs = |
|
91 |
struct |
|
92 |
val name = "HOL/induct_method"; |
|
93 |
type T = GlobalInductArgs.T; |
|
8278 | 94 |
|
8308 | 95 |
fun init thy = GlobalInduct.get thy; |
96 |
fun print x = GlobalInductArgs.print x; |
|
97 |
end; |
|
98 |
||
99 |
structure LocalInduct = ProofDataFun(LocalInductArgs); |
|
100 |
val print_local_rules = LocalInduct.print; |
|
8376 | 101 |
val dest_local_rules = GlobalInductArgs.dest o LocalInduct.get; |
8308 | 102 |
|
103 |
||
104 |
(* access rules *) |
|
105 |
||
106 |
val get_cases = #1 o LocalInduct.get; |
|
107 |
val get_induct = #2 o LocalInduct.get; |
|
108 |
||
109 |
val lookup_casesT = lookup_rule o #1 o get_cases; |
|
110 |
val lookup_casesS = lookup_rule o #2 o get_cases; |
|
111 |
val lookup_inductT = lookup_rule o #1 o get_induct; |
|
112 |
val lookup_inductS = lookup_rule o #2 o get_induct; |
|
113 |
||
114 |
||
115 |
||
116 |
(** attributes **) |
|
117 |
||
118 |
local |
|
119 |
||
120 |
fun mk_att f g name (x, thm) = (f (g (name, thm)) x, thm); |
|
121 |
||
122 |
fun add_casesT rule x = apfst (apfst (NetRules.insert rule)) x; |
|
123 |
fun add_casesS rule x = apfst (apsnd (NetRules.insert rule)) x; |
|
124 |
fun add_inductT rule x = apsnd (apfst (NetRules.insert rule)) x; |
|
125 |
fun add_inductS rule x = apsnd (apsnd (NetRules.insert rule)) x; |
|
126 |
||
127 |
in |
|
128 |
||
129 |
val cases_type_global = mk_att GlobalInduct.map add_casesT; |
|
130 |
val cases_set_global = mk_att GlobalInduct.map add_casesS; |
|
131 |
val induct_type_global = mk_att GlobalInduct.map add_inductT; |
|
132 |
val induct_set_global = mk_att GlobalInduct.map add_inductS; |
|
133 |
||
134 |
val cases_type_local = mk_att LocalInduct.map add_casesT; |
|
135 |
val cases_set_local = mk_att LocalInduct.map add_casesS; |
|
136 |
val induct_type_local = mk_att LocalInduct.map add_inductT; |
|
137 |
val induct_set_local = mk_att LocalInduct.map add_inductS; |
|
138 |
||
139 |
end; |
|
140 |
||
141 |
||
142 |
||
143 |
(** misc utils **) |
|
8278 | 144 |
|
9597 | 145 |
(* align lists *) |
146 |
||
147 |
fun align_left msg xs ys = |
|
148 |
let val m = length xs and n = length ys |
|
149 |
in if m < n then error msg else (Library.take (n, xs) ~~ ys) end; |
|
150 |
||
151 |
fun align_right msg xs ys = |
|
152 |
let val m = length xs and n = length ys |
|
153 |
in if m < n then error msg else (Library.drop (m - n, xs) ~~ ys) end; |
|
154 |
||
155 |
||
8695 | 156 |
(* thms and terms *) |
157 |
||
158 |
val concls_of = HOLogic.dest_conj o HOLogic.dest_Trueprop o Thm.concl_of; |
|
8344 | 159 |
|
8278 | 160 |
fun vars_of tm = (*ordered left-to-right, preferring right!*) |
8308 | 161 |
Term.foldl_aterms (fn (ts, t as Var _) => t :: ts | (ts, _) => ts) ([], tm) |
8278 | 162 |
|> Library.distinct |> rev; |
163 |
||
8308 | 164 |
fun type_name t = |
165 |
#1 (Term.dest_Type (Term.type_of t)) |
|
9597 | 166 |
handle TYPE _ => raise TERM ("Type of term argument is too general", [t]); |
167 |
||
168 |
fun prep_inst align cert (tm, ts) = |
|
169 |
let |
|
170 |
fun prep_var (x, Some t) = Some (cert x, cert t) |
|
171 |
| prep_var (_, None) = None; |
|
172 |
in |
|
173 |
align "Rule has fewer variables than instantiations given" (vars_of tm) ts |
|
174 |
|> mapfilter prep_var |
|
175 |
end; |
|
8278 | 176 |
|
177 |
||
8337 | 178 |
(* simplifying cases rules *) |
179 |
||
180 |
local |
|
181 |
||
182 |
(*delete needless equality assumptions*) |
|
183 |
val refl_thin = prove_goal HOL.thy "!!P. [| a=a; P |] ==> P" |
|
184 |
(fn _ => [assume_tac 1]); |
|
185 |
||
186 |
val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject]; |
|
187 |
||
188 |
val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls; |
|
189 |
||
190 |
in |
|
191 |
||
9299 | 192 |
fun simp_case_tac solved ss i = |
193 |
EVERY' [elim_tac, asm_full_simp_tac ss, elim_tac, REPEAT o bound_hyp_subst_tac] i |
|
194 |
THEN_MAYBE (if solved then no_tac else all_tac); |
|
8337 | 195 |
|
196 |
end; |
|
197 |
||
198 |
||
8278 | 199 |
|
200 |
(** cases method **) |
|
201 |
||
8308 | 202 |
(* |
203 |
rule selection: |
|
204 |
cases - classical case split |
|
8376 | 205 |
cases t - datatype exhaustion |
206 |
<x:A> cases ... - set elimination |
|
8451 | 207 |
... cases ... R - explicit rule |
8308 | 208 |
*) |
8278 | 209 |
|
9066 | 210 |
val case_split = RuleCases.name ["True", "False"] case_split_thm; |
211 |
||
8344 | 212 |
local |
213 |
||
9597 | 214 |
(* FIXME |
215 |
fun cases_vars thm = |
|
216 |
(case try (vars_of o hd o Logic.strip_assums_hyp o Library.last_elem o Thm.prems_of) thm of |
|
8308 | 217 |
None => raise THM ("Malformed cases rule", 0, [thm]) |
9597 | 218 |
| Some xs => xs); |
219 |
*) |
|
8308 | 220 |
|
9299 | 221 |
fun simplified_cases ctxt cases thm = |
222 |
let |
|
223 |
val nprems = Thm.nprems_of thm; |
|
224 |
val opt_cases = |
|
225 |
Library.replicate (nprems - Int.min (nprems, length cases)) None @ |
|
226 |
map Some (Library.take (nprems, cases)); |
|
8337 | 227 |
|
9299 | 228 |
val tac = simp_case_tac true (Simplifier.get_local_simpset ctxt); |
229 |
fun simp ((i, c), (th, cs)) = |
|
230 |
(case try (Tactic.rule_by_tactic (tac i)) th of |
|
9313 | 231 |
None => (th, c :: cs) |
232 |
| Some th' => (th', None :: cs)); |
|
9299 | 233 |
|
234 |
val (thm', opt_cases') = foldr simp (1 upto Thm.nprems_of thm ~~ opt_cases, (thm, [])); |
|
235 |
in (thm', mapfilter I opt_cases') end; |
|
236 |
||
9624
de254f375477
changed 'opaque' option to 'open' (opaque is default);
wenzelm
parents:
9597
diff
changeset
|
237 |
fun cases_tac (ctxt, ((simplified, open_parms), args)) facts = |
8308 | 238 |
let |
239 |
val sg = ProofContext.sign_of ctxt; |
|
240 |
val cert = Thm.cterm_of sg; |
|
8278 | 241 |
|
9597 | 242 |
fun inst_rule insts thm = |
243 |
(align_right "Rule has fewer premises than arguments given" (Thm.prems_of thm) insts |
|
244 |
|> (flat o map (prep_inst align_left cert)) |
|
245 |
|> Drule.cterm_instantiate) thm; |
|
6442 | 246 |
|
8376 | 247 |
fun find_cases th = |
248 |
NetRules.may_unify (#2 (get_cases ctxt)) |
|
249 |
(Logic.strip_assums_concl (#prop (Thm.rep_thm th))); |
|
250 |
||
251 |
val rules = |
|
8344 | 252 |
(case (args, facts) of |
9597 | 253 |
(([], None), []) => [RuleCases.add case_split] |
254 |
| ((insts, None), []) => |
|
255 |
let |
|
256 |
val name = type_name (hd (flat (map (mapfilter I) insts))) |
|
257 |
handle Library.LIST _ => error "Unable to figure out type cases rule" |
|
258 |
in |
|
8308 | 259 |
(case lookup_casesT ctxt name of |
260 |
None => error ("No cases rule for type: " ^ quote name) |
|
9597 | 261 |
| Some thm => [(inst_rule insts thm, RuleCases.get thm)]) |
8308 | 262 |
end |
9597 | 263 |
| (([], None), th :: _) => map (RuleCases.add o #2) (find_cases th) |
264 |
| ((insts, None), th :: _) => |
|
9299 | 265 |
(case find_cases th of (*may instantiate first rule only!*) |
9597 | 266 |
(_, thm) :: _ => [(inst_rule insts thm, RuleCases.get thm)] |
8376 | 267 |
| [] => []) |
9597 | 268 |
| (([], Some thm), _) => [RuleCases.add thm] |
269 |
| ((insts, Some thm), _) => [(inst_rule insts thm, RuleCases.get thm)]); |
|
8376 | 270 |
|
9299 | 271 |
val cond_simp = if simplified then simplified_cases ctxt else rpair; |
272 |
||
8376 | 273 |
fun prep_rule (thm, cases) = |
9299 | 274 |
Seq.map (cond_simp cases) (Method.multi_resolves facts [thm]); |
9624
de254f375477
changed 'opaque' option to 'open' (opaque is default);
wenzelm
parents:
9597
diff
changeset
|
275 |
in Method.resolveq_cases_tac open_parms (Seq.flat (Seq.map prep_rule (Seq.of_list rules))) end; |
8278 | 276 |
|
8344 | 277 |
in |
278 |
||
8671 | 279 |
val cases_meth = Method.METHOD_CASES o (HEADGOAL oo cases_tac); |
8278 | 280 |
|
8344 | 281 |
end; |
282 |
||
8278 | 283 |
|
284 |
||
285 |
(** induct method **) |
|
286 |
||
8308 | 287 |
(* |
288 |
rule selection: |
|
289 |
induct - mathematical induction |
|
8376 | 290 |
induct x - datatype induction |
291 |
<x:A> induct ... - set induction |
|
8451 | 292 |
... induct ... R - explicit rule |
8308 | 293 |
*) |
8278 | 294 |
|
8344 | 295 |
local |
296 |
||
8376 | 297 |
infix 1 THEN_ALL_NEW_CASES; |
298 |
||
299 |
fun (tac1 THEN_ALL_NEW_CASES tac2) i st = |
|
300 |
st |> Seq.THEN (tac1 i, (fn (st', cases) => |
|
8540 | 301 |
Seq.map (rpair cases) (Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st) st'))); |
8376 | 302 |
|
303 |
||
8330 | 304 |
fun induct_rule ctxt t = |
305 |
let val name = type_name t in |
|
306 |
(case lookup_inductT ctxt name of |
|
307 |
None => error ("No induct rule for type: " ^ quote name) |
|
8332 | 308 |
| Some thm => (name, thm)) |
8330 | 309 |
end; |
310 |
||
8332 | 311 |
fun join_rules [(_, thm)] = thm |
8330 | 312 |
| join_rules raw_thms = |
313 |
let |
|
8332 | 314 |
val thms = (map (apsnd Drule.freeze_all) raw_thms); |
315 |
fun eq_prems ((_, th1), (_, th2)) = |
|
316 |
Term.aconvs (Thm.prems_of th1, Thm.prems_of th2); |
|
8330 | 317 |
in |
8332 | 318 |
(case Library.gen_distinct eq_prems thms of |
319 |
[(_, thm)] => |
|
320 |
let |
|
321 |
val cprems = Drule.cprems_of thm; |
|
322 |
val asms = map Thm.assume cprems; |
|
323 |
fun strip (_, th) = Drule.implies_elim_list th asms; |
|
324 |
in |
|
325 |
foldr1 (fn (th, th') => [th, th'] MRS conjI) (map strip thms) |
|
326 |
|> Drule.implies_intr_list cprems |
|
327 |
|> Drule.standard |
|
328 |
end |
|
329 |
| [] => error "No rule given" |
|
330 |
| bads => error ("Incompatible rules for " ^ commas_quote (map #1 bads))) |
|
8330 | 331 |
end; |
332 |
||
8376 | 333 |
|
9624
de254f375477
changed 'opaque' option to 'open' (opaque is default);
wenzelm
parents:
9597
diff
changeset
|
334 |
fun induct_tac (ctxt, ((stripped, open_parms), args)) facts = |
8308 | 335 |
let |
336 |
val sg = ProofContext.sign_of ctxt; |
|
337 |
val cert = Thm.cterm_of sg; |
|
338 |
||
339 |
fun inst_rule insts thm = |
|
9597 | 340 |
(align_right "Rule has fewer conclusions than arguments given" (concls_of thm) insts |
341 |
|> (flat o map (prep_inst align_right cert)) |
|
342 |
|> Drule.cterm_instantiate) thm; |
|
8278 | 343 |
|
8376 | 344 |
fun find_induct th = |
345 |
NetRules.may_unify (#2 (get_induct ctxt)) |
|
346 |
(Logic.strip_assums_concl (#prop (Thm.rep_thm th))); |
|
347 |
||
348 |
val rules = |
|
8308 | 349 |
(case (args, facts) of |
8540 | 350 |
(([], None), []) => [] |
8376 | 351 |
| ((insts, None), []) => |
8695 | 352 |
let val thms = map (induct_rule ctxt o last_elem o mapfilter I) insts |
353 |
handle Library.LIST _ => error "Unable to figure out type induction rule" |
|
8376 | 354 |
in [(inst_rule insts (join_rules thms), RuleCases.get (#2 (hd thms)))] end |
355 |
| (([], None), th :: _) => map (RuleCases.add o #2) (find_induct th) |
|
356 |
| ((insts, None), th :: _) => |
|
9299 | 357 |
(case find_induct th of (*may instantiate first rule only!*) |
358 |
(_, thm) :: _ => [(inst_rule insts thm, RuleCases.get thm)] |
|
8376 | 359 |
| [] => []) |
360 |
| (([], Some thm), _) => [RuleCases.add thm] |
|
361 |
| ((insts, Some thm), _) => [(inst_rule insts thm, RuleCases.get thm)]); |
|
362 |
||
363 |
fun prep_rule (thm, cases) = |
|
364 |
Seq.map (rpair cases) (Method.multi_resolves facts [thm]); |
|
9624
de254f375477
changed 'opaque' option to 'open' (opaque is default);
wenzelm
parents:
9597
diff
changeset
|
365 |
val tac = Method.resolveq_cases_tac open_parms |
de254f375477
changed 'opaque' option to 'open' (opaque is default);
wenzelm
parents:
9597
diff
changeset
|
366 |
(Seq.flat (Seq.map prep_rule (Seq.of_list rules))); |
8344 | 367 |
in |
8688 | 368 |
if stripped then tac THEN_ALL_NEW_CASES (REPEAT o Tactic.match_tac [impI, allI, ballI]) |
8376 | 369 |
else tac |
8344 | 370 |
end; |
371 |
||
372 |
in |
|
8278 | 373 |
|
8671 | 374 |
val induct_meth = Method.METHOD_CASES o (HEADGOAL oo induct_tac); |
8278 | 375 |
|
8344 | 376 |
end; |
377 |
||
8278 | 378 |
|
379 |
||
380 |
(** concrete syntax **) |
|
381 |
||
8308 | 382 |
val casesN = "cases"; |
383 |
val inductN = "induct"; |
|
8344 | 384 |
|
8337 | 385 |
val simplifiedN = "simplified"; |
8344 | 386 |
val strippedN = "stripped"; |
9624
de254f375477
changed 'opaque' option to 'open' (opaque is default);
wenzelm
parents:
9597
diff
changeset
|
387 |
val openN = "open"; |
8344 | 388 |
|
8308 | 389 |
val typeN = "type"; |
390 |
val setN = "set"; |
|
391 |
val ruleN = "rule"; |
|
392 |
||
393 |
||
394 |
(* attributes *) |
|
395 |
||
8815 | 396 |
fun spec k = (Args.$$$ k -- Args.colon) |-- Args.!!! Args.name; |
8308 | 397 |
|
398 |
fun attrib sign_of add_type add_set = Scan.depend (fn x => |
|
399 |
let val sg = sign_of x in |
|
400 |
spec typeN >> (add_type o Sign.intern_tycon sg) || |
|
401 |
spec setN >> (add_set o Sign.intern_const sg) |
|
402 |
end >> pair x); |
|
403 |
||
404 |
val cases_attr = |
|
405 |
(Attrib.syntax (attrib Theory.sign_of cases_type_global cases_set_global), |
|
406 |
Attrib.syntax (attrib ProofContext.sign_of cases_type_local cases_set_local)); |
|
407 |
||
408 |
val induct_attr = |
|
409 |
(Attrib.syntax (attrib Theory.sign_of induct_type_global induct_set_global), |
|
410 |
Attrib.syntax (attrib ProofContext.sign_of induct_type_local induct_set_local)); |
|
411 |
||
412 |
||
413 |
(* methods *) |
|
414 |
||
8278 | 415 |
local |
6442 | 416 |
|
8308 | 417 |
fun err k get name = |
418 |
(case get name of Some x => x |
|
419 |
| None => error ("No rule for " ^ k ^ " " ^ quote name)); |
|
6442 | 420 |
|
8308 | 421 |
fun rule get_type get_set = |
422 |
Scan.depend (fn ctxt => |
|
423 |
let val sg = ProofContext.sign_of ctxt in |
|
424 |
spec typeN >> (err typeN (get_type ctxt) o Sign.intern_tycon sg) || |
|
425 |
spec setN >> (err setN (get_set ctxt) o Sign.intern_const sg) |
|
426 |
end >> pair ctxt) || |
|
8815 | 427 |
Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.local_thm; |
6442 | 428 |
|
8308 | 429 |
val cases_rule = rule lookup_casesT lookup_casesS; |
430 |
val induct_rule = rule lookup_inductT lookup_inductS; |
|
6442 | 431 |
|
8815 | 432 |
val kind = (Args.$$$ typeN || Args.$$$ setN || Args.$$$ ruleN) -- Args.colon; |
8308 | 433 |
val term = Scan.unless (Scan.lift kind) Args.local_term; |
8695 | 434 |
val term_dummy = Scan.unless (Scan.lift kind) |
435 |
(Scan.lift (Args.$$$ "_") >> K None || Args.local_term >> Some); |
|
6446 | 436 |
|
9597 | 437 |
val instss = Args.and_list (Scan.repeat1 term_dummy); |
438 |
||
8278 | 439 |
in |
440 |
||
9299 | 441 |
val cases_args = Method.syntax |
9803 | 442 |
(Args.mode simplifiedN -- Args.mode openN -- (instss -- Scan.option cases_rule)); |
9299 | 443 |
|
8695 | 444 |
val induct_args = Method.syntax |
9803 | 445 |
(Args.mode strippedN -- Args.mode openN -- (instss -- Scan.option induct_rule)); |
8278 | 446 |
|
447 |
end; |
|
6446 | 448 |
|
449 |
||
6442 | 450 |
|
8278 | 451 |
(** theory setup **) |
6446 | 452 |
|
8278 | 453 |
val setup = |
8308 | 454 |
[GlobalInduct.init, LocalInduct.init, |
455 |
Attrib.add_attributes |
|
456 |
[(casesN, cases_attr, "cases rule for type or set"), |
|
457 |
(inductN, induct_attr, "induction rule for type or set")], |
|
458 |
Method.add_methods |
|
459 |
[("cases", cases_meth oo cases_args, "case analysis on types or sets"), |
|
9066 | 460 |
("induct", induct_meth oo induct_args, "induction on types or sets")], |
461 |
(#1 o PureThy.add_thms [(("case_split", case_split), [])])]; |
|
6442 | 462 |
|
463 |
end; |