nipkow@45014: signature INDUCTION =
nipkow@45014: sig
nipkow@45014:   val induction_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
nipkow@45014:     (string * typ) list list -> term option list -> thm list option ->
nipkow@45014:     thm list -> int -> cases_tactic
nipkow@45014:   val setup: theory -> theory
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 =
nipkow@45014:  (case strip_comb t of
nipkow@45014:     (p as Var _, _) => [p]
nipkow@45014:   | (p as Free _, _) => [p]
nipkow@45014:   | (_, ts) => flat(map preds_of ts))
nipkow@45014: 
nipkow@45014: fun name_hyps thy (arg as ((cases,consumes),th)) =
nipkow@45014:   if not(forall (null o #2 o #1) cases) then arg
nipkow@45014:   else
nipkow@45014:     let
nipkow@45014:       val (prems, concl) = Logic.strip_horn (prop_of th);
nipkow@45014:       val prems' = drop consumes prems;
nipkow@45014:       val ps = preds_of concl;
nipkow@45014: 
nipkow@45014:       fun hname_of t =
nipkow@45014:         if exists_subterm (member (op =) ps) t
nipkow@45014:         then ind_hypsN else Rule_Cases.case_hypsN
nipkow@45014: 
nipkow@45014:       val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems'
nipkow@45014:       val n = Int.min (length hnamess, length cases) 
nipkow@45014:       val cases' = map (fn (((cn,_),concls),hns) => ((cn,hns),concls))
nipkow@45014:         (take n cases ~~ take n hnamess)
nipkow@45014:     in ((cases',consumes),th) end
nipkow@45014: 
nipkow@45014: val induction_tac = Induct.gen_induct_tac name_hyps
nipkow@45014: 
nipkow@45014: val setup = Induct.gen_induct_setup @{binding induction} induction_tac
nipkow@45014: 
nipkow@45014: end
nipkow@45014: