author | wenzelm |
Thu, 11 Jan 2001 19:38:02 +0100 | |
changeset 10871 | 0ff9caa810b1 |
parent 10814 | 2ccc84b8f5a0 |
child 11035 | bad7568e76e0 |
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 |
|
8431 | 11 |
val vars_of: term -> term list |
8695 | 12 |
val concls_of: thm -> term list |
10728 | 13 |
val rewrite_cterm: thm list -> cterm -> cterm |
9299 | 14 |
val simp_case_tac: bool -> simpset -> int -> tactic |
6442 | 15 |
val setup: (theory -> theory) list |
16 |
end; |
|
17 |
||
18 |
structure InductMethod: INDUCT_METHOD = |
|
19 |
struct |
|
20 |
||
8337 | 21 |
|
10409 | 22 |
(** theory context references **) |
23 |
||
24 |
val inductive_atomize = thms "inductive_atomize"; |
|
10439
be2dc95dfe98
inductive_rulify2 accomodates malformed induction rules;
wenzelm
parents:
10409
diff
changeset
|
25 |
val inductive_rulify1 = thms "inductive_rulify1"; |
be2dc95dfe98
inductive_rulify2 accomodates malformed induction rules;
wenzelm
parents:
10409
diff
changeset
|
26 |
val inductive_rulify2 = thms "inductive_rulify2"; |
10409 | 27 |
|
28 |
||
29 |
||
8308 | 30 |
(** misc utils **) |
8278 | 31 |
|
9597 | 32 |
(* align lists *) |
33 |
||
34 |
fun align_left msg xs ys = |
|
35 |
let val m = length xs and n = length ys |
|
36 |
in if m < n then error msg else (Library.take (n, xs) ~~ ys) end; |
|
37 |
||
38 |
fun align_right msg xs ys = |
|
39 |
let val m = length xs and n = length ys |
|
40 |
in if m < n then error msg else (Library.drop (m - n, xs) ~~ ys) end; |
|
41 |
||
42 |
||
8695 | 43 |
(* thms and terms *) |
44 |
||
10803 | 45 |
fun imp_concl_of t = imp_concl_of (#2 (HOLogic.dest_imp t)) handle TERM _ => t; |
46 |
val concls_of = map imp_concl_of o HOLogic.dest_conj o HOLogic.dest_Trueprop o Thm.concl_of; |
|
8344 | 47 |
|
8278 | 48 |
fun vars_of tm = (*ordered left-to-right, preferring right!*) |
8308 | 49 |
Term.foldl_aterms (fn (ts, t as Var _) => t :: ts | (ts, _) => ts) ([], tm) |
8278 | 50 |
|> Library.distinct |> rev; |
51 |
||
8308 | 52 |
fun type_name t = |
53 |
#1 (Term.dest_Type (Term.type_of t)) |
|
9597 | 54 |
handle TYPE _ => raise TERM ("Type of term argument is too general", [t]); |
55 |
||
10409 | 56 |
fun prep_inst align cert f (tm, ts) = |
9597 | 57 |
let |
10409 | 58 |
fun prep_var (x, Some t) = |
59 |
let |
|
60 |
val cx = cert x; |
|
61 |
val {T = xT, sign, ...} = Thm.rep_cterm cx; |
|
62 |
val orig_ct = cert t; |
|
63 |
val ct = f orig_ct; |
|
64 |
in |
|
65 |
if Sign.typ_instance sign (#T (Thm.rep_cterm ct), xT) then Some (cx, ct) |
|
66 |
else error (Pretty.string_of (Pretty.block |
|
67 |
[Pretty.str "Ill-typed instantiation:", Pretty.fbrk, |
|
68 |
Display.pretty_cterm orig_ct, Pretty.str " ::", Pretty.brk 1, |
|
69 |
Display.pretty_ctyp (#T (Thm.crep_cterm orig_ct))])) |
|
70 |
end |
|
9597 | 71 |
| prep_var (_, None) = None; |
72 |
in |
|
73 |
align "Rule has fewer variables than instantiations given" (vars_of tm) ts |
|
74 |
|> mapfilter prep_var |
|
75 |
end; |
|
8278 | 76 |
|
10728 | 77 |
fun rewrite_cterm rews = |
78 |
#2 o Thm.dest_comb o #prop o Thm.crep_thm o Simplifier.full_rewrite (HOL_basic_ss addsimps rews); |
|
79 |
||
8278 | 80 |
|
8337 | 81 |
(* simplifying cases rules *) |
82 |
||
83 |
local |
|
84 |
||
85 |
(*delete needless equality assumptions*) |
|
10409 | 86 |
val refl_thin = prove_goal HOL.thy "!!P. a = a ==> P ==> P" (fn _ => [assume_tac 1]); |
8337 | 87 |
val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject]; |
88 |
val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls; |
|
89 |
||
90 |
in |
|
91 |
||
9299 | 92 |
fun simp_case_tac solved ss i = |
93 |
EVERY' [elim_tac, asm_full_simp_tac ss, elim_tac, REPEAT o bound_hyp_subst_tac] i |
|
94 |
THEN_MAYBE (if solved then no_tac else all_tac); |
|
8337 | 95 |
|
96 |
end; |
|
97 |
||
98 |
||
10542
92cd56dfc17e
resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents:
10527
diff
changeset
|
99 |
(* resolution and cases *) |
92cd56dfc17e
resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents:
10527
diff
changeset
|
100 |
|
92cd56dfc17e
resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents:
10527
diff
changeset
|
101 |
local |
92cd56dfc17e
resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents:
10527
diff
changeset
|
102 |
|
92cd56dfc17e
resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents:
10527
diff
changeset
|
103 |
fun gen_resolveq_tac tac rules i st = |
92cd56dfc17e
resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents:
10527
diff
changeset
|
104 |
Seq.flat (Seq.map (fn rule => tac rule i st) rules); |
92cd56dfc17e
resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents:
10527
diff
changeset
|
105 |
|
92cd56dfc17e
resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents:
10527
diff
changeset
|
106 |
in |
92cd56dfc17e
resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents:
10527
diff
changeset
|
107 |
|
92cd56dfc17e
resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents:
10527
diff
changeset
|
108 |
fun resolveq_cases_tac make tac = gen_resolveq_tac (fn (rule, (cases, facts)) => fn i => fn st => |
92cd56dfc17e
resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents:
10527
diff
changeset
|
109 |
Seq.map (rpair (make rule cases)) |
92cd56dfc17e
resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents:
10527
diff
changeset
|
110 |
((Method.insert_tac facts THEN' tac THEN' Tactic.rtac rule) i st)); |
92cd56dfc17e
resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents:
10527
diff
changeset
|
111 |
|
92cd56dfc17e
resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents:
10527
diff
changeset
|
112 |
end; |
92cd56dfc17e
resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents:
10527
diff
changeset
|
113 |
|
92cd56dfc17e
resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents:
10527
diff
changeset
|
114 |
|
8278 | 115 |
|
116 |
(** cases method **) |
|
117 |
||
8308 | 118 |
(* |
119 |
rule selection: |
|
120 |
cases - classical case split |
|
8376 | 121 |
cases t - datatype exhaustion |
122 |
<x:A> cases ... - set elimination |
|
8451 | 123 |
... cases ... R - explicit rule |
8308 | 124 |
*) |
8278 | 125 |
|
9066 | 126 |
val case_split = RuleCases.name ["True", "False"] case_split_thm; |
127 |
||
8344 | 128 |
local |
129 |
||
9299 | 130 |
fun simplified_cases ctxt cases thm = |
131 |
let |
|
132 |
val nprems = Thm.nprems_of thm; |
|
133 |
val opt_cases = |
|
134 |
Library.replicate (nprems - Int.min (nprems, length cases)) None @ |
|
135 |
map Some (Library.take (nprems, cases)); |
|
8337 | 136 |
|
9299 | 137 |
val tac = simp_case_tac true (Simplifier.get_local_simpset ctxt); |
138 |
fun simp ((i, c), (th, cs)) = |
|
139 |
(case try (Tactic.rule_by_tactic (tac i)) th of |
|
9313 | 140 |
None => (th, c :: cs) |
141 |
| Some th' => (th', None :: cs)); |
|
9299 | 142 |
|
143 |
val (thm', opt_cases') = foldr simp (1 upto Thm.nprems_of thm ~~ opt_cases, (thm, [])); |
|
144 |
in (thm', mapfilter I opt_cases') end; |
|
145 |
||
9624
de254f375477
changed 'opaque' option to 'open' (opaque is default);
wenzelm
parents:
9597
diff
changeset
|
146 |
fun cases_tac (ctxt, ((simplified, open_parms), args)) facts = |
8308 | 147 |
let |
148 |
val sg = ProofContext.sign_of ctxt; |
|
149 |
val cert = Thm.cterm_of sg; |
|
8278 | 150 |
|
9597 | 151 |
fun inst_rule insts thm = |
9914 | 152 |
(align_left "Rule has fewer premises than arguments given" (Thm.prems_of thm) insts |
10409 | 153 |
|> (flat o map (prep_inst align_left cert I)) |
9597 | 154 |
|> Drule.cterm_instantiate) thm; |
6442 | 155 |
|
8376 | 156 |
fun find_cases th = |
10271
45b996639c45
split over two files: induct_attrib.ML, induct_method.ML;
wenzelm
parents:
10013
diff
changeset
|
157 |
NetRules.may_unify (#2 (InductAttrib.get_cases ctxt)) |
8376 | 158 |
(Logic.strip_assums_concl (#prop (Thm.rep_thm th))); |
159 |
||
160 |
val rules = |
|
10803 | 161 |
(case (fst args, facts) of |
9597 | 162 |
(([], None), []) => [RuleCases.add case_split] |
163 |
| ((insts, None), []) => |
|
164 |
let |
|
165 |
val name = type_name (hd (flat (map (mapfilter I) insts))) |
|
166 |
handle Library.LIST _ => error "Unable to figure out type cases rule" |
|
167 |
in |
|
10271
45b996639c45
split over two files: induct_attrib.ML, induct_method.ML;
wenzelm
parents:
10013
diff
changeset
|
168 |
(case InductAttrib.lookup_casesT ctxt name of |
8308 | 169 |
None => error ("No cases rule for type: " ^ quote name) |
9597 | 170 |
| Some thm => [(inst_rule insts thm, RuleCases.get thm)]) |
8308 | 171 |
end |
9597 | 172 |
| (([], None), th :: _) => map (RuleCases.add o #2) (find_cases th) |
173 |
| ((insts, None), th :: _) => |
|
9299 | 174 |
(case find_cases th of (*may instantiate first rule only!*) |
9597 | 175 |
(_, thm) :: _ => [(inst_rule insts thm, RuleCases.get thm)] |
8376 | 176 |
| [] => []) |
9597 | 177 |
| (([], Some thm), _) => [RuleCases.add thm] |
10803 | 178 |
| ((insts, Some thm), _) => [(inst_rule insts thm, RuleCases.get thm)]) |
179 |
|> map (Library.apfst (Attrib.read_inst' (snd args) ctxt)); |
|
8376 | 180 |
|
9299 | 181 |
val cond_simp = if simplified then simplified_cases ctxt else rpair; |
182 |
||
10527 | 183 |
fun prep_rule (thm, (cases, n)) = Seq.map (apsnd (rpair (drop (n, facts))) o cond_simp cases) |
184 |
(Method.multi_resolves (take (n, facts)) [thm]); |
|
10409 | 185 |
in |
10542
92cd56dfc17e
resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents:
10527
diff
changeset
|
186 |
resolveq_cases_tac (RuleCases.make open_parms) (K all_tac) |
10409 | 187 |
(Seq.flat (Seq.map prep_rule (Seq.of_list rules))) |
188 |
end; |
|
8278 | 189 |
|
8344 | 190 |
in |
191 |
||
8671 | 192 |
val cases_meth = Method.METHOD_CASES o (HEADGOAL oo cases_tac); |
8278 | 193 |
|
8344 | 194 |
end; |
195 |
||
8278 | 196 |
|
197 |
||
198 |
(** induct method **) |
|
199 |
||
8308 | 200 |
(* |
201 |
rule selection: |
|
8376 | 202 |
induct x - datatype induction |
203 |
<x:A> induct ... - set induction |
|
8451 | 204 |
... induct ... R - explicit rule |
8308 | 205 |
*) |
8278 | 206 |
|
8344 | 207 |
local |
208 |
||
10803 | 209 |
val atomize_cterm = Thm.cterm_fun AutoBind.drop_judgment o rewrite_cterm inductive_atomize; |
10439
be2dc95dfe98
inductive_rulify2 accomodates malformed induction rules;
wenzelm
parents:
10409
diff
changeset
|
210 |
val atomize_tac = Tactic.rewrite_goal_tac inductive_atomize; |
be2dc95dfe98
inductive_rulify2 accomodates malformed induction rules;
wenzelm
parents:
10409
diff
changeset
|
211 |
val rulify_cterm = rewrite_cterm inductive_rulify2 o rewrite_cterm inductive_rulify1; |
be2dc95dfe98
inductive_rulify2 accomodates malformed induction rules;
wenzelm
parents:
10409
diff
changeset
|
212 |
|
be2dc95dfe98
inductive_rulify2 accomodates malformed induction rules;
wenzelm
parents:
10409
diff
changeset
|
213 |
val rulify_tac = |
be2dc95dfe98
inductive_rulify2 accomodates malformed induction rules;
wenzelm
parents:
10409
diff
changeset
|
214 |
Tactic.rewrite_goal_tac inductive_rulify1 THEN' |
be2dc95dfe98
inductive_rulify2 accomodates malformed induction rules;
wenzelm
parents:
10409
diff
changeset
|
215 |
Tactic.rewrite_goal_tac inductive_rulify2 THEN' |
10803 | 216 |
Tactic.norm_hhf_tac; |
10409 | 217 |
|
218 |
fun rulify_cases cert = |
|
10803 | 219 |
let |
220 |
val ruly = Thm.term_of o rulify_cterm o cert; |
|
221 |
fun ruly_case {fixes, assumes, binds} = |
|
10814 | 222 |
{fixes = fixes, assumes = map ruly assumes, |
223 |
binds = map (apsnd (apsome (AutoBind.drop_judgment o ruly))) binds}; |
|
10871 | 224 |
in map (apsnd ruly_case) ooo RuleCases.make_raw end; |
10409 | 225 |
|
10455 | 226 |
val weak_strip_tac = REPEAT o Tactic.match_tac [impI, allI, ballI]; |
227 |
||
10409 | 228 |
|
8376 | 229 |
infix 1 THEN_ALL_NEW_CASES; |
230 |
||
231 |
fun (tac1 THEN_ALL_NEW_CASES tac2) i st = |
|
232 |
st |> Seq.THEN (tac1 i, (fn (st', cases) => |
|
8540 | 233 |
Seq.map (rpair cases) (Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st) st'))); |
8376 | 234 |
|
235 |
||
8330 | 236 |
fun induct_rule ctxt t = |
237 |
let val name = type_name t in |
|
10271
45b996639c45
split over two files: induct_attrib.ML, induct_method.ML;
wenzelm
parents:
10013
diff
changeset
|
238 |
(case InductAttrib.lookup_inductT ctxt name of |
8330 | 239 |
None => error ("No induct rule for type: " ^ quote name) |
8332 | 240 |
| Some thm => (name, thm)) |
8330 | 241 |
end; |
242 |
||
8332 | 243 |
fun join_rules [(_, thm)] = thm |
8330 | 244 |
| join_rules raw_thms = |
245 |
let |
|
8332 | 246 |
val thms = (map (apsnd Drule.freeze_all) raw_thms); |
247 |
fun eq_prems ((_, th1), (_, th2)) = |
|
248 |
Term.aconvs (Thm.prems_of th1, Thm.prems_of th2); |
|
8330 | 249 |
in |
8332 | 250 |
(case Library.gen_distinct eq_prems thms of |
251 |
[(_, thm)] => |
|
252 |
let |
|
253 |
val cprems = Drule.cprems_of thm; |
|
254 |
val asms = map Thm.assume cprems; |
|
255 |
fun strip (_, th) = Drule.implies_elim_list th asms; |
|
256 |
in |
|
257 |
foldr1 (fn (th, th') => [th, th'] MRS conjI) (map strip thms) |
|
258 |
|> Drule.implies_intr_list cprems |
|
259 |
|> Drule.standard |
|
260 |
end |
|
261 |
| [] => error "No rule given" |
|
262 |
| bads => error ("Incompatible rules for " ^ commas_quote (map #1 bads))) |
|
8330 | 263 |
end; |
264 |
||
8376 | 265 |
|
9624
de254f375477
changed 'opaque' option to 'open' (opaque is default);
wenzelm
parents:
9597
diff
changeset
|
266 |
fun induct_tac (ctxt, ((stripped, open_parms), args)) facts = |
8308 | 267 |
let |
268 |
val sg = ProofContext.sign_of ctxt; |
|
269 |
val cert = Thm.cterm_of sg; |
|
270 |
||
271 |
fun inst_rule insts thm = |
|
9597 | 272 |
(align_right "Rule has fewer conclusions than arguments given" (concls_of thm) insts |
10409 | 273 |
|> (flat o map (prep_inst align_right cert atomize_cterm)) |
9597 | 274 |
|> Drule.cterm_instantiate) thm; |
8278 | 275 |
|
8376 | 276 |
fun find_induct th = |
10271
45b996639c45
split over two files: induct_attrib.ML, induct_method.ML;
wenzelm
parents:
10013
diff
changeset
|
277 |
NetRules.may_unify (#2 (InductAttrib.get_induct ctxt)) |
8376 | 278 |
(Logic.strip_assums_concl (#prop (Thm.rep_thm th))); |
279 |
||
280 |
val rules = |
|
10803 | 281 |
(case (fst args, facts) of |
8540 | 282 |
(([], None), []) => [] |
8376 | 283 |
| ((insts, None), []) => |
8695 | 284 |
let val thms = map (induct_rule ctxt o last_elem o mapfilter I) insts |
285 |
handle Library.LIST _ => error "Unable to figure out type induction rule" |
|
8376 | 286 |
in [(inst_rule insts (join_rules thms), RuleCases.get (#2 (hd thms)))] end |
287 |
| (([], None), th :: _) => map (RuleCases.add o #2) (find_induct th) |
|
288 |
| ((insts, None), th :: _) => |
|
9299 | 289 |
(case find_induct th of (*may instantiate first rule only!*) |
290 |
(_, thm) :: _ => [(inst_rule insts thm, RuleCases.get thm)] |
|
8376 | 291 |
| [] => []) |
292 |
| (([], Some thm), _) => [RuleCases.add thm] |
|
10803 | 293 |
| ((insts, Some thm), _) => [(inst_rule insts thm, RuleCases.get thm)]) |
294 |
|> map (Library.apfst (Attrib.read_inst' (snd args) ctxt)); |
|
8376 | 295 |
|
10527 | 296 |
fun prep_rule (thm, (cases, n)) = |
297 |
Seq.map (rpair (cases, drop (n, facts))) (Method.multi_resolves (take (n, facts)) [thm]); |
|
10542
92cd56dfc17e
resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents:
10527
diff
changeset
|
298 |
val tac = resolveq_cases_tac (rulify_cases cert open_parms) atomize_tac |
9624
de254f375477
changed 'opaque' option to 'open' (opaque is default);
wenzelm
parents:
9597
diff
changeset
|
299 |
(Seq.flat (Seq.map prep_rule (Seq.of_list rules))); |
8344 | 300 |
in |
10542
92cd56dfc17e
resolveq_cases_tac moved here from Pure/Isar/method.ML;
wenzelm
parents:
10527
diff
changeset
|
301 |
tac THEN_ALL_NEW_CASES (rulify_tac THEN' (if stripped then weak_strip_tac else K all_tac)) |
8344 | 302 |
end; |
303 |
||
304 |
in |
|
8278 | 305 |
|
8671 | 306 |
val induct_meth = Method.METHOD_CASES o (HEADGOAL oo induct_tac); |
8278 | 307 |
|
8344 | 308 |
end; |
309 |
||
8278 | 310 |
|
311 |
||
312 |
(** concrete syntax **) |
|
313 |
||
8337 | 314 |
val simplifiedN = "simplified"; |
8344 | 315 |
val strippedN = "stripped"; |
9624
de254f375477
changed 'opaque' option to 'open' (opaque is default);
wenzelm
parents:
9597
diff
changeset
|
316 |
val openN = "open"; |
8308 | 317 |
val ruleN = "rule"; |
10803 | 318 |
val ofN = "of"; |
8308 | 319 |
|
8278 | 320 |
local |
6442 | 321 |
|
8308 | 322 |
fun err k get name = |
323 |
(case get name of Some x => x |
|
324 |
| None => error ("No rule for " ^ k ^ " " ^ quote name)); |
|
6442 | 325 |
|
10271
45b996639c45
split over two files: induct_attrib.ML, induct_method.ML;
wenzelm
parents:
10013
diff
changeset
|
326 |
fun spec k = (Args.$$$ k -- Args.colon) |-- Args.!!! Args.name; |
45b996639c45
split over two files: induct_attrib.ML, induct_method.ML;
wenzelm
parents:
10013
diff
changeset
|
327 |
|
8308 | 328 |
fun rule get_type get_set = |
329 |
Scan.depend (fn ctxt => |
|
330 |
let val sg = ProofContext.sign_of ctxt in |
|
10271
45b996639c45
split over two files: induct_attrib.ML, induct_method.ML;
wenzelm
parents:
10013
diff
changeset
|
331 |
spec InductAttrib.typeN >> (err InductAttrib.typeN (get_type ctxt) o Sign.intern_tycon sg) || |
45b996639c45
split over two files: induct_attrib.ML, induct_method.ML;
wenzelm
parents:
10013
diff
changeset
|
332 |
spec InductAttrib.setN >> (err InductAttrib.setN (get_set ctxt) o Sign.intern_const sg) |
8308 | 333 |
end >> pair ctxt) || |
8815 | 334 |
Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.local_thm; |
6442 | 335 |
|
10271
45b996639c45
split over two files: induct_attrib.ML, induct_method.ML;
wenzelm
parents:
10013
diff
changeset
|
336 |
val cases_rule = rule InductAttrib.lookup_casesT InductAttrib.lookup_casesS; |
45b996639c45
split over two files: induct_attrib.ML, induct_method.ML;
wenzelm
parents:
10013
diff
changeset
|
337 |
val induct_rule = rule InductAttrib.lookup_inductT InductAttrib.lookup_inductS; |
6442 | 338 |
|
10803 | 339 |
val kind_inst = |
340 |
(Args.$$$ InductAttrib.typeN || Args.$$$ InductAttrib.setN || Args.$$$ ruleN || Args.$$$ ofN) |
|
341 |
-- Args.colon; |
|
342 |
val term = Scan.unless (Scan.lift kind_inst) Args.local_term; |
|
343 |
val term_dummy = Scan.unless (Scan.lift kind_inst) |
|
8695 | 344 |
(Scan.lift (Args.$$$ "_") >> K None || Args.local_term >> Some); |
6446 | 345 |
|
9597 | 346 |
val instss = Args.and_list (Scan.repeat1 term_dummy); |
347 |
||
10803 | 348 |
(* FIXME Attrib.insts': better use actual term args *) |
349 |
val rule_insts = |
|
350 |
Scan.lift (Scan.optional ((Args.$$$ ofN -- Args.colon) |-- Args.!!! Attrib.insts') ([], [])); |
|
351 |
||
8278 | 352 |
in |
353 |
||
9299 | 354 |
val cases_args = Method.syntax |
10803 | 355 |
(Args.mode simplifiedN -- Args.mode openN -- (instss -- Scan.option cases_rule -- rule_insts)); |
9299 | 356 |
|
8695 | 357 |
val induct_args = Method.syntax |
10803 | 358 |
(Args.mode strippedN -- Args.mode openN -- (instss -- Scan.option induct_rule -- rule_insts)); |
8278 | 359 |
|
360 |
end; |
|
6446 | 361 |
|
362 |
||
6442 | 363 |
|
8278 | 364 |
(** theory setup **) |
6446 | 365 |
|
8278 | 366 |
val setup = |
10271
45b996639c45
split over two files: induct_attrib.ML, induct_method.ML;
wenzelm
parents:
10013
diff
changeset
|
367 |
[Method.add_methods |
45b996639c45
split over two files: induct_attrib.ML, induct_method.ML;
wenzelm
parents:
10013
diff
changeset
|
368 |
[(InductAttrib.casesN, cases_meth oo cases_args, "case analysis on types or sets"), |
45b996639c45
split over two files: induct_attrib.ML, induct_method.ML;
wenzelm
parents:
10013
diff
changeset
|
369 |
(InductAttrib.inductN, induct_meth oo induct_args, "induction on types or sets")], |
9066 | 370 |
(#1 o PureThy.add_thms [(("case_split", case_split), [])])]; |
6442 | 371 |
|
372 |
end; |