wenzelm@59931: (*  Title:      Tools/induction.ML
wenzelm@59931:     Author:     Tobias Nipkow, TU Muenchen
wenzelm@59931: 
wenzelm@59931: Alternative proof method "induction" that gives induction hypotheses the
wenzelm@59931: name "IH".
wenzelm@59931: *)
wenzelm@59931: 
nipkow@45014: signature INDUCTION =
nipkow@45014: sig
wenzelm@61844:   val induction_context_tactic: bool -> (binding option * (term * bool)) option list list ->
nipkow@45014:     (string * typ) list list -> term option list -> thm list option ->
wenzelm@61841:     thm list -> int -> context_tactic
wenzelm@61844:   val induction_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
wenzelm@61844:     (string * typ) list list -> term option list -> thm list option ->
wenzelm@61844:     thm list -> int -> tactic
nipkow@45014: end
nipkow@45014: 
nipkow@45014: structure Induction: INDUCTION =
nipkow@45014: struct
nipkow@45014: 
nipkow@45014: val ind_hypsN = "IH";
nipkow@45014: 
nipkow@45014: fun preds_of t =
wenzelm@59931:   (case strip_comb t of
nipkow@45014:     (p as Var _, _) => [p]
nipkow@45014:   | (p as Free _, _) => [p]
wenzelm@59931:   | (_, ts) => maps preds_of ts);
nipkow@45014: 
wenzelm@61844: val induction_context_tactic =
wenzelm@61844:   Induct.gen_induct_context_tactic (fn arg as ((cases, consumes), th) =>
wenzelm@61844:     if not (forall (null o #2 o #1) cases) then arg
wenzelm@61844:     else
wenzelm@61844:       let
wenzelm@61844:         val (prems, concl) = Logic.strip_horn (Thm.prop_of th);
wenzelm@61844:         val prems' = drop consumes prems;
wenzelm@61844:         val ps = preds_of concl;
wenzelm@61844:   
wenzelm@61844:         fun hname_of t =
wenzelm@61844:           if exists_subterm (member (op aconv) ps) t
wenzelm@61844:           then ind_hypsN else Rule_Cases.case_hypsN;
wenzelm@61844:   
wenzelm@61844:         val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems';
wenzelm@61844:         val n = Int.min (length hnamess, length cases);
wenzelm@61844:         val cases' =
wenzelm@61844:           map (fn (((cn, _), concls), hns) => ((cn, hns), concls))
wenzelm@61844:             (take n cases ~~ take n hnamess);
wenzelm@61844:       in ((cases', consumes), th) end);
nipkow@45014: 
wenzelm@61844: fun induction_tac ctxt x1 x2 x3 x4 x5 x6 x7 =
wenzelm@61844:   Method.NO_CONTEXT_TACTIC ctxt (induction_context_tactic x1 x2 x3 x4 x5 x6 x7);
nipkow@45014: 
wenzelm@61844: val _ =
wenzelm@67149:   Theory.local_setup (Induct.gen_induct_setup \<^binding>\<open>induction\<close> induction_context_tactic);
nipkow@45014: 
nipkow@45014: end