1 (* Title: Tools/induct.ML
2 Author: Markus Wenzel, TU Muenchen
4 Proof by cases, induction, and coinduction.
7 signature INDUCT_DATA =
12 val rulify_fallback: thm list
18 val vars_of: term -> term list
19 val dest_rules: Proof.context ->
20 {type_cases: (string * thm) list, pred_cases: (string * thm) list,
21 type_induct: (string * thm) list, pred_induct: (string * thm) list,
22 type_coinduct: (string * thm) list, pred_coinduct: (string * thm) list}
23 val print_rules: Proof.context -> unit
24 val lookup_casesT: Proof.context -> string -> thm option
25 val lookup_casesP: Proof.context -> string -> thm option
26 val lookup_inductT: Proof.context -> string -> thm option
27 val lookup_inductP: Proof.context -> string -> thm option
28 val lookup_coinductT: Proof.context -> string -> thm option
29 val lookup_coinductP: Proof.context -> string -> thm option
30 val find_casesT: Proof.context -> typ -> thm list
31 val find_casesP: Proof.context -> term -> thm list
32 val find_inductT: Proof.context -> typ -> thm list
33 val find_inductP: Proof.context -> term -> thm list
34 val find_coinductT: Proof.context -> typ -> thm list
35 val find_coinductP: Proof.context -> term -> thm list
36 val cases_type: string -> attribute
37 val cases_pred: string -> attribute
38 val cases_del: attribute
39 val induct_type: string -> attribute
40 val induct_pred: string -> attribute
41 val induct_del: attribute
42 val coinduct_type: string -> attribute
43 val coinduct_pred: string -> attribute
44 val coinduct_del: attribute
52 val fix_tac: Proof.context -> int -> (string * typ) list -> int -> tactic
53 val add_defs: (binding option * term) option list -> Proof.context ->
54 (term option list * thm list) * Proof.context
55 val atomize_term: theory -> term -> term
56 val atomize_tac: int -> tactic
57 val inner_atomize_tac: int -> tactic
58 val rulified_term: thm -> theory * term
59 val rulify_tac: int -> tactic
60 val internalize: int -> thm -> thm
61 val guess_instance: Proof.context -> thm -> int -> thm -> thm Seq.seq
62 val cases_tac: Proof.context -> term option list list -> thm option ->
63 thm list -> int -> cases_tactic
64 val get_inductT: Proof.context -> term option list list -> thm list list
65 val induct_tac: Proof.context -> (binding option * term) option list list ->
66 (string * typ) list list -> term option list -> thm list option ->
67 thm list -> int -> cases_tactic
68 val coinduct_tac: Proof.context -> term option list -> term option list -> thm option ->
69 thm list -> int -> cases_tactic
70 val setup: theory -> theory
73 functor Induct(Data: INDUCT_DATA): INDUCT =
79 (* encode_type -- for indexing purposes *)
81 fun encode_type (Type (c, Ts)) = Term.list_comb (Const (c, dummyT), map encode_type Ts)
82 | encode_type (TFree (a, _)) = Free (a, dummyT)
83 | encode_type (TVar (a, _)) = Var (a, dummyT);
86 (* variables -- ordered left-to-right, preferring right *)
89 rev (distinct (op =) (Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm []));
93 val mk_var = encode_type o #2 o Term.dest_Var;
95 fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle Empty =>
96 raise THM ("No variables in conclusion of rule", 0, [thm]);
100 fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle Empty =>
101 raise THM ("No variables in major premise of rule", 0, [thm]);
103 val left_var_concl = concl_var hd;
104 val right_var_concl = concl_var List.last;
114 type rules = (string * thm) Item_Net.T;
116 fun init_rules index : rules =
118 (fn ((s1, th1), (s2, th2)) => s1 = s2 andalso Thm.eq_thm_prop (th1, th2))
121 fun filter_rules (rs: rules) th =
122 filter (fn (_, th') => Thm.eq_thm_prop (th, th')) (Item_Net.content rs);
124 fun lookup_rule (rs: rules) = AList.lookup (op =) (Item_Net.content rs);
126 fun pretty_rules ctxt kind rs =
127 let val thms = map snd (Item_Net.content rs)
128 in Pretty.big_list kind (map (Display.pretty_thm ctxt) thms) end;
133 structure InductData = Generic_Data
135 type T = (rules * rules) * (rules * rules) * (rules * rules);
137 ((init_rules (left_var_prem o #2), init_rules (Thm.major_prem_of o #2)),
138 (init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)),
139 (init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)));
141 fun merge (((casesT1, casesP1), (inductT1, inductP1), (coinductT1, coinductP1)),
142 ((casesT2, casesP2), (inductT2, inductP2), (coinductT2, coinductP2))) =
143 ((Item_Net.merge (casesT1, casesT2), Item_Net.merge (casesP1, casesP2)),
144 (Item_Net.merge (inductT1, inductT2), Item_Net.merge (inductP1, inductP2)),
145 (Item_Net.merge (coinductT1, coinductT2), Item_Net.merge (coinductP1, coinductP2)));
148 val get_local = InductData.get o Context.Proof;
150 fun dest_rules ctxt =
151 let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP)) = get_local ctxt in
152 {type_cases = Item_Net.content casesT,
153 pred_cases = Item_Net.content casesP,
154 type_induct = Item_Net.content inductT,
155 pred_induct = Item_Net.content inductP,
156 type_coinduct = Item_Net.content coinductT,
157 pred_coinduct = Item_Net.content coinductP}
160 fun print_rules ctxt =
161 let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP)) = get_local ctxt in
162 [pretty_rules ctxt "coinduct type:" coinductT,
163 pretty_rules ctxt "coinduct pred:" coinductP,
164 pretty_rules ctxt "induct type:" inductT,
165 pretty_rules ctxt "induct pred:" inductP,
166 pretty_rules ctxt "cases type:" casesT,
167 pretty_rules ctxt "cases pred:" casesP]
168 |> Pretty.chunks |> Pretty.writeln
172 OuterSyntax.improper_command "print_induct_rules" "print induction and cases rules"
173 OuterKeyword.diag (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
174 Toplevel.keep (print_rules o Toplevel.context_of)));
179 val lookup_casesT = lookup_rule o #1 o #1 o get_local;
180 val lookup_casesP = lookup_rule o #2 o #1 o get_local;
181 val lookup_inductT = lookup_rule o #1 o #2 o get_local;
182 val lookup_inductP = lookup_rule o #2 o #2 o get_local;
183 val lookup_coinductT = lookup_rule o #1 o #3 o get_local;
184 val lookup_coinductP = lookup_rule o #2 o #3 o get_local;
187 fun find_rules which how ctxt x =
188 map snd (Item_Net.retrieve (which (get_local ctxt)) (how x));
190 val find_casesT = find_rules (#1 o #1) encode_type;
191 val find_casesP = find_rules (#2 o #1) I;
192 val find_inductT = find_rules (#1 o #2) encode_type;
193 val find_inductP = find_rules (#2 o #2) I;
194 val find_coinductT = find_rules (#1 o #3) encode_type;
195 val find_coinductP = find_rules (#2 o #3) I;
203 fun mk_att f g name arg =
204 let val (x, thm) = g arg in (InductData.map (f (name, thm)) x, thm) end;
206 fun del_att which = Thm.declaration_attribute (fn th => InductData.map (which (pairself (fn rs =>
207 fold Item_Net.remove (filter_rules rs th) rs))));
209 fun map1 f (x, y, z) = (f x, y, z);
210 fun map2 f (x, y, z) = (x, f y, z);
211 fun map3 f (x, y, z) = (x, y, f z);
213 fun add_casesT rule x = map1 (apfst (Item_Net.update rule)) x;
214 fun add_casesP rule x = map1 (apsnd (Item_Net.update rule)) x;
215 fun add_inductT rule x = map2 (apfst (Item_Net.update rule)) x;
216 fun add_inductP rule x = map2 (apsnd (Item_Net.update rule)) x;
217 fun add_coinductT rule x = map3 (apfst (Item_Net.update rule)) x;
218 fun add_coinductP rule x = map3 (apsnd (Item_Net.update rule)) x;
220 val consumes0 = Rule_Cases.consumes_default 0;
221 val consumes1 = Rule_Cases.consumes_default 1;
225 val cases_type = mk_att add_casesT consumes0;
226 val cases_pred = mk_att add_casesP consumes1;
227 val cases_del = del_att map1;
229 val induct_type = mk_att add_inductT consumes0;
230 val induct_pred = mk_att add_inductP consumes1;
231 val induct_del = del_att map2;
233 val coinduct_type = mk_att add_coinductT consumes0;
234 val coinduct_pred = mk_att add_coinductP consumes1;
235 val coinduct_del = del_att map3;
241 (** attribute syntax **)
243 val casesN = "cases";
244 val inductN = "induct";
245 val coinductN = "coinduct";
254 Scan.lift (Args.$$$ k -- Args.colon) |-- arg ||
255 Scan.lift (Args.$$$ k) >> K "";
257 fun attrib add_type add_pred del =
258 spec typeN Args.tyname >> add_type ||
259 spec predN Args.const >> add_pred ||
260 spec setN Args.const >> add_pred ||
261 Scan.lift Args.del >> K del;
266 Attrib.setup @{binding cases} (attrib cases_type cases_pred cases_del)
267 "declaration of cases rule" #>
268 Attrib.setup @{binding induct} (attrib induct_type induct_pred induct_del)
269 "declaration of induction rule" #>
270 Attrib.setup @{binding coinduct} (attrib coinduct_type coinduct_pred coinduct_del)
271 "declaration of coinduction rule";
281 fun align_left msg xs ys =
282 let val m = length xs and n = length ys
283 in if m < n then error msg else (Library.take (n, xs) ~~ ys) end;
285 fun align_right msg xs ys =
286 let val m = length xs and n = length ys
287 in if m < n then error msg else (Library.drop (m - n, xs) ~~ ys) end;
292 fun prep_inst ctxt align tune (tm, ts) =
294 val cert = Thm.cterm_of (ProofContext.theory_of ctxt);
295 fun prep_var (x, SOME t) =
298 val xT = #T (Thm.rep_cterm cx);
299 val ct = cert (tune t);
300 val tT = #T (Thm.rep_cterm ct);
302 if Type.could_unify (tT, xT) then SOME (cx, ct)
303 else error (Pretty.string_of (Pretty.block
304 [Pretty.str "Ill-typed instantiation:", Pretty.fbrk,
305 Syntax.pretty_term ctxt (Thm.term_of ct), Pretty.str " ::", Pretty.brk 1,
306 Syntax.pretty_typ ctxt tT]))
308 | prep_var (_, NONE) = NONE;
311 align "Rule has fewer variables than instantiations given" xs ts
312 |> map_filter prep_var
318 fun trace_rules _ kind [] = error ("Unable to figure out " ^ kind ^ " rule")
319 | trace_rules ctxt _ rules = Method.trace ctxt rules;
326 rule selection scheme:
327 cases - default case split
328 `A t` cases ... - predicate/set cases
330 ... cases ... r - explicit rule
335 fun get_casesT ctxt ((SOME t :: _) :: _) = find_casesT ctxt (Term.fastype_of t)
336 | get_casesT _ _ = [];
338 fun get_casesP ctxt (fact :: _) = find_casesP ctxt (Thm.concl_of fact)
339 | get_casesP _ _ = [];
343 fun cases_tac ctxt insts opt_rule facts =
345 val thy = ProofContext.theory_of ctxt;
348 if null insts then `Rule_Cases.get r
349 else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
350 |> maps (prep_inst ctxt align_left I)
351 |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r);
355 SOME r => Seq.single (inst_rule r)
357 (get_casesP ctxt facts @ get_casesT ctxt insts @ [Data.cases_default])
358 |> tap (trace_rules ctxt casesN)
359 |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
363 |> Seq.maps (Rule_Cases.consume [] facts)
364 |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
365 CASES (Rule_Cases.make_common false (thy, Thm.prop_of rule) cases)
366 (Method.insert_tac more_facts i THEN Tactic.rtac rule i) st)
373 (** induct method **)
375 val conjunction_congs = [@{thm Pure.all_conjunction}, @{thm imp_conjunction}];
380 fun atomize_term thy =
381 MetaSimplifier.rewrite_term thy Data.atomize []
382 #> ObjectLogic.drop_judgment thy;
384 val atomize_cterm = MetaSimplifier.rewrite true Data.atomize;
386 val atomize_tac = Simplifier.rewrite_goal_tac Data.atomize;
388 val inner_atomize_tac =
389 Simplifier.rewrite_goal_tac (map Thm.symmetric conjunction_congs) THEN' atomize_tac;
394 fun rulify_term thy =
395 MetaSimplifier.rewrite_term thy (Data.rulify @ conjunction_congs) [] #>
396 MetaSimplifier.rewrite_term thy Data.rulify_fallback [];
398 fun rulified_term thm =
400 val thy = Thm.theory_of_thm thm;
401 val rulify = rulify_term thy;
402 val (As, B) = Logic.strip_horn (Thm.prop_of thm);
403 in (thy, Logic.list_implies (map rulify As, rulify B)) end;
406 Simplifier.rewrite_goal_tac (Data.rulify @ conjunction_congs) THEN'
407 Simplifier.rewrite_goal_tac Data.rulify_fallback THEN'
408 Goal.conjunction_tac THEN_ALL_NEW
409 (Simplifier.rewrite_goal_tac [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac);
414 fun rule_instance ctxt inst rule =
415 Drule.cterm_instantiate (prep_inst ctxt align_left I (Thm.prop_of rule, inst)) rule;
417 fun internalize k th =
418 th |> Thm.permute_prems 0 k
419 |> Conv.fconv_rule (Conv.concl_conv (Thm.nprems_of th - k) atomize_cterm);
422 (* guess rule instantiation -- cannot handle pending goal parameters *)
426 fun dest_env thy env =
428 val cert = Thm.cterm_of thy;
429 val certT = Thm.ctyp_of thy;
430 val pairs = Vartab.dest (Envir.term_env env);
431 val types = Vartab.dest (Envir.type_env env);
432 val ts = map (cert o Envir.norm_term env o #2 o #2) pairs;
433 val xs = map2 (curry (cert o Var)) (map #1 pairs) (map (#T o Thm.rep_cterm) ts);
434 in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) types, xs ~~ ts) end;
438 fun guess_instance ctxt rule i st =
440 val thy = ProofContext.theory_of ctxt;
441 val maxidx = Thm.maxidx_of st;
442 val goal = Thm.term_of (Thm.cprem_of st i); (*exception Subscript*)
443 val params = rev (Term.rename_wrt_term goal (Logic.strip_params goal));
445 if not (null params) then
446 (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^
447 commas_quote (map (Syntax.string_of_term ctxt o Syntax.mark_boundT) params));
451 val rule' = Thm.incr_indexes (maxidx + 1) rule;
452 val concl = Logic.strip_assums_concl goal;
454 Unify.smash_unifiers thy [(Thm.concl_of rule', concl)] (Envir.empty (Thm.maxidx_of rule'))
455 |> Seq.map (fn env => Drule.instantiate (dest_env thy env) rule')
457 end handle Subscript => Seq.empty;
462 (* special renaming of rule parameters *)
464 fun special_rename_params ctxt [[SOME (Free (z, Type (T, _)))]] [thm] =
466 val x = Name.clean (ProofContext.revert_skolem ctxt z);
468 | index i (y :: ys) =
469 if x = y then x ^ string_of_int i :: index (i + 1) ys
470 else y :: index i ys;
471 fun rename_params [] = []
472 | rename_params ((y, Type (U, _)) :: ys) =
473 (if U = T then x else y) :: rename_params ys
474 | rename_params ((y, _) :: ys) = y :: rename_params ys;
477 val xs = rename_params (Logic.strip_params A);
479 (case filter (fn x' => x' = x) xs of
480 [] => xs | [_] => xs | _ => index 1 xs);
481 in Logic.list_rename_params (xs', A) end;
483 let val (As, C) = Logic.strip_horn p
484 in Logic.list_implies (map rename_asm As, C) end;
485 val cp' = cterm_fun rename_prop (Thm.cprop_of thm);
486 val thm' = Thm.equal_elim (Thm.reflexive cp') thm;
487 in [Rule_Cases.save thm thm'] end
488 | special_rename_params _ _ ths = ths;
495 fun goal_prefix k ((c as Const ("all", _)) $ Abs (a, T, B)) = c $ Abs (a, T, goal_prefix k B)
496 | goal_prefix 0 _ = Term.dummy_pattern propT
497 | goal_prefix k ((c as Const ("==>", _)) $ A $ B) = c $ A $ goal_prefix (k - 1) B
498 | goal_prefix _ _ = Term.dummy_pattern propT;
500 fun goal_params k (Const ("all", _) $ Abs (_, _, B)) = goal_params k B + 1
501 | goal_params 0 _ = 0
502 | goal_params k (Const ("==>", _) $ _ $ B) = goal_params (k - 1) B
503 | goal_params _ _ = 0;
505 fun meta_spec_tac ctxt n (x, T) = SUBGOAL (fn (goal, i) =>
507 val thy = ProofContext.theory_of ctxt;
508 val cert = Thm.cterm_of thy;
511 fun spec_rule prfx (xs, body) =
512 @{thm Pure.meta_spec}
513 |> Thm.rename_params_rule ([Name.clean (ProofContext.revert_skolem ctxt x)], 1)
514 |> Thm.lift_rule (cert prfx)
515 |> `(Thm.prop_of #> Logic.strip_assums_concl)
516 |-> (fn pred $ arg =>
517 Drule.cterm_instantiate
518 [(cert (Term.head_of pred), cert (Logic.rlist_abs (xs, body))),
519 (cert (Term.head_of arg), cert (Logic.rlist_abs (xs, v)))]);
521 fun goal_concl k xs (Const ("all", _) $ Abs (a, T, B)) = goal_concl k ((a, T) :: xs) B
522 | goal_concl 0 xs B =
523 if not (Term.exists_subterm (fn t => t aconv v) B) then NONE
524 else SOME (xs, Term.absfree (x, T, Term.incr_boundvars 1 B))
525 | goal_concl k xs (Const ("==>", _) $ _ $ B) = goal_concl (k - 1) xs B
526 | goal_concl _ _ _ = NONE;
528 (case goal_concl n [] goal of
530 (compose_tac (false, spec_rule (goal_prefix n goal) concl, 1) THEN' rtac asm_rl) i
534 fun miniscope_tac p = CONVERSION o
535 Conv.params_conv p (K (MetaSimplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq]));
539 fun fix_tac _ _ [] = K all_tac
540 | fix_tac ctxt n xs = SUBGOAL (fn (goal, i) =>
541 (EVERY' (map (meta_spec_tac ctxt n) xs) THEN'
542 (miniscope_tac (goal_params n goal) ctxt)) i);
549 fun add_defs def_insts =
551 fun add (SOME (SOME x, t)) ctxt =
552 let val ([(lhs, (_, th))], ctxt') =
553 LocalDefs.add_defs [((x, NoSyn), (Thm.empty_binding, t))] ctxt
554 in ((SOME lhs, [th]), ctxt') end
555 | add (SOME (NONE, t)) ctxt = ((SOME t, []), ctxt)
556 | add NONE ctxt = ((NONE, []), ctxt);
557 in fold_map add def_insts #> apfst (split_list #> apsnd flat) end;
563 rule selection scheme:
564 `A x` induct ... - predicate/set induction
565 induct x - type induction
566 ... induct ... r - explicit rule
569 fun get_inductT ctxt insts =
570 fold_rev (map_product cons) (insts |> map
571 ((fn [] => NONE | ts => List.last ts) #>
572 (fn NONE => TVar (("'a", 0), []) | SOME t => Term.fastype_of t) #>
573 find_inductT ctxt)) [[]]
574 |> filter_out (forall Rule_Cases.is_inner_rule);
576 fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
577 | get_inductP _ _ = [];
579 fun induct_tac ctxt def_insts arbitrary taking opt_rule facts =
581 val thy = ProofContext.theory_of ctxt;
583 val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
584 val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs;
586 fun inst_rule (concls, r) =
587 (if null insts then `Rule_Cases.get r
588 else (align_left "Rule has fewer conclusions than arguments given"
589 (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
590 |> maps (prep_inst ctxt align_right (atomize_term thy))
591 |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r))
592 |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
596 SOME rs => Seq.single (inst_rule (Rule_Cases.strict_mutual_rule ctxt rs))
598 (get_inductP ctxt facts @
599 map (special_rename_params defs_ctxt insts) (get_inductT ctxt insts))
600 |> map_filter (Rule_Cases.mutual_rule ctxt)
601 |> tap (trace_rules ctxt inductN o map #2)
602 |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
604 fun rule_cases rule =
605 Rule_Cases.make_nested false (Thm.prop_of rule) (rulified_term rule);
609 |> Seq.maps (Rule_Cases.consume (flat defs) facts)
610 |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
611 (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
613 (Method.insert_tac (more_facts @ nth_list atomized_defs (j - 1))
614 THEN' fix_tac defs_ctxt
615 (nth concls (j - 1) + more_consumes)
616 (nth_list arbitrary (j - 1))))
617 THEN' inner_atomize_tac) j))
618 THEN' atomize_tac) i st |> Seq.maps (fn st' =>
619 guess_instance ctxt (internalize more_consumes rule) i st'
620 |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
621 |> Seq.maps (fn rule' =>
622 CASES (rule_cases rule' cases)
623 (Tactic.rtac rule' i THEN
624 PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st'))))
625 THEN_ALL_NEW_CASES rulify_tac
630 (** coinduct method **)
633 rule selection scheme:
634 goal "A x" coinduct ... - predicate/set coinduction
635 coinduct x - type coinduction
636 coinduct ... r - explicit rule
641 fun get_coinductT ctxt (SOME t :: _) = find_coinductT ctxt (Term.fastype_of t)
642 | get_coinductT _ _ = [];
644 fun get_coinductP ctxt goal = find_coinductP ctxt (Logic.strip_assums_concl goal);
646 fun main_prop_of th =
647 if Rule_Cases.get_consumes th > 0 then Thm.major_prem_of th else Thm.concl_of th;
651 fun coinduct_tac ctxt inst taking opt_rule facts =
653 val thy = ProofContext.theory_of ctxt;
656 if null inst then `Rule_Cases.get r
657 else Drule.cterm_instantiate (prep_inst ctxt align_right I (main_prop_of r, inst)) r
658 |> pair (Rule_Cases.get r);
662 SOME r => Seq.single (inst_rule r)
664 (get_coinductP ctxt goal @ get_coinductT ctxt inst)
665 |> tap (trace_rules ctxt coinductN)
666 |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
668 SUBGOAL_CASES (fn (goal, i) => fn st =>
670 |> Seq.maps (Rule_Cases.consume [] facts)
671 |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
672 guess_instance ctxt rule i st
673 |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
674 |> Seq.maps (fn rule' =>
675 CASES (Rule_Cases.make_common false (thy, Thm.prop_of rule') cases)
676 (Method.insert_tac more_facts i THEN Tactic.rtac rule' i) st)))
683 (** concrete syntax **)
685 structure P = OuterParse;
687 val arbitraryN = "arbitrary";
688 val takingN = "taking";
693 fun single_rule [rule] = rule
694 | single_rule _ = error "Single rule expected";
696 fun named_rule k arg get =
697 Scan.lift (Args.$$$ k -- Args.colon) |-- Scan.repeat arg :|--
698 (fn names => Scan.peek (fn context => Scan.succeed (names |> map (fn name =>
699 (case get (Context.proof_of context) name of SOME x => x
700 | NONE => error ("No rule for " ^ k ^ " " ^ quote name))))));
702 fun rule get_type get_pred =
703 named_rule typeN Args.tyname get_type ||
704 named_rule predN Args.const get_pred ||
705 named_rule setN Args.const get_pred ||
706 Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;
708 val cases_rule = rule lookup_casesT lookup_casesP >> single_rule;
709 val induct_rule = rule lookup_inductT lookup_inductP;
710 val coinduct_rule = rule lookup_coinductT lookup_coinductP >> single_rule;
712 val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME;
715 ((Scan.lift (Args.binding --| (Args.$$$ "\<equiv>" || Args.$$$ "==")) >> SOME)
716 -- Args.term) >> SOME ||
717 inst >> Option.map (pair NONE);
719 val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) =>
720 error ("Bad free variable: " ^ Syntax.string_of_term ctxt t));
722 fun unless_more_args scan = Scan.unless (Scan.lift
723 ((Args.$$$ arbitraryN || Args.$$$ takingN || Args.$$$ typeN ||
724 Args.$$$ predN || Args.$$$ setN || Args.$$$ ruleN) -- Args.colon)) scan;
726 val arbitrary = Scan.optional (Scan.lift (Args.$$$ arbitraryN -- Args.colon) |--
727 P.and_list1' (Scan.repeat (unless_more_args free))) [];
729 val taking = Scan.optional (Scan.lift (Args.$$$ takingN -- Args.colon) |--
730 Scan.repeat1 (unless_more_args inst)) [];
735 Method.setup @{binding cases}
736 (P.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule >>
737 (fn (insts, opt_rule) => fn ctxt =>
738 METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL (cases_tac ctxt insts opt_rule facts)))))
739 "case analysis on types or predicates/sets";
742 Method.setup @{binding induct}
743 (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
744 (arbitrary -- taking -- Scan.option induct_rule) >>
745 (fn (insts, ((arbitrary, taking), opt_rule)) => fn ctxt =>
746 RAW_METHOD_CASES (fn facts =>
747 Seq.DETERM (HEADGOAL (induct_tac ctxt insts arbitrary taking opt_rule facts)))))
748 "induction on types or predicates/sets";
751 Method.setup @{binding coinduct}
752 (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
753 (fn ((insts, taking), opt_rule) => fn ctxt =>
754 RAW_METHOD_CASES (fn facts =>
755 Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts)))))
756 "coinduction on types or predicates/sets";
764 val setup = attrib_setup #> cases_setup #> induct_setup #> coinduct_setup;