src/Tools/induction.ML
author wenzelm
Sun Dec 13 21:56:15 2015 +0100 (2015-12-13)
changeset 61841 4d3527b94f2a
parent 59970 e9f73d87d904
child 61844 007d3b34080f
permissions -rw-r--r--
more general types Proof.method / context_tactic;
proper context for Method.insert_tac;
tuned;
     1 (*  Title:      Tools/induction.ML
     2     Author:     Tobias Nipkow, TU Muenchen
     3 
     4 Alternative proof method "induction" that gives induction hypotheses the
     5 name "IH".
     6 *)
     7 
     8 signature INDUCTION =
     9 sig
    10   val induction_tac: bool -> (binding option * (term * bool)) option list list ->
    11     (string * typ) list list -> term option list -> thm list option ->
    12     thm list -> int -> context_tactic
    13 end
    14 
    15 structure Induction: INDUCTION =
    16 struct
    17 
    18 val ind_hypsN = "IH";
    19 
    20 fun preds_of t =
    21   (case strip_comb t of
    22     (p as Var _, _) => [p]
    23   | (p as Free _, _) => [p]
    24   | (_, ts) => maps preds_of ts);
    25 
    26 fun name_hyps (arg as ((cases, consumes), th)) =
    27   if not (forall (null o #2 o #1) cases) then arg
    28   else
    29     let
    30       val (prems, concl) = Logic.strip_horn (Thm.prop_of th);
    31       val prems' = drop consumes prems;
    32       val ps = preds_of concl;
    33 
    34       fun hname_of t =
    35         if exists_subterm (member (op aconv) ps) t
    36         then ind_hypsN else Rule_Cases.case_hypsN;
    37 
    38       val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems';
    39       val n = Int.min (length hnamess, length cases);
    40       val cases' =
    41         map (fn (((cn, _), concls), hns) => ((cn, hns), concls))
    42           (take n cases ~~ take n hnamess);
    43     in ((cases', consumes), th) end;
    44 
    45 val induction_tac = Induct.gen_induct_tac name_hyps;
    46 
    47 val _ = Theory.local_setup (Induct.gen_induct_setup @{binding induction} induction_tac);
    48 
    49 end