src/Tools/induction.ML
author wenzelm
Wed Apr 08 19:39:08 2015 +0200 (2015-04-08)
changeset 59970 e9f73d87d904
parent 59940 087d81f5213e
child 61841 4d3527b94f2a
permissions -rw-r--r--
proper context for Object_Logic operations;
     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: Proof.context -> bool ->
    11     (binding option * (term * bool)) option list list ->
    12     (string * typ) list list -> term option list -> thm list option ->
    13     thm list -> int -> cases_tactic
    14 end
    15 
    16 structure Induction: INDUCTION =
    17 struct
    18 
    19 val ind_hypsN = "IH";
    20 
    21 fun preds_of t =
    22   (case strip_comb t of
    23     (p as Var _, _) => [p]
    24   | (p as Free _, _) => [p]
    25   | (_, ts) => maps preds_of ts);
    26 
    27 fun name_hyps (arg as ((cases, consumes), th)) =
    28   if not (forall (null o #2 o #1) cases) then arg
    29   else
    30     let
    31       val (prems, concl) = Logic.strip_horn (Thm.prop_of th);
    32       val prems' = drop consumes prems;
    33       val ps = preds_of concl;
    34 
    35       fun hname_of t =
    36         if exists_subterm (member (op aconv) ps) t
    37         then ind_hypsN else Rule_Cases.case_hypsN;
    38 
    39       val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems';
    40       val n = Int.min (length hnamess, length cases);
    41       val cases' =
    42         map (fn (((cn, _), concls), hns) => ((cn, hns), concls))
    43           (take n cases ~~ take n hnamess);
    44     in ((cases', consumes), th) end;
    45 
    46 val induction_tac = Induct.gen_induct_tac name_hyps;
    47 
    48 val _ = Theory.local_setup (Induct.gen_induct_setup @{binding induction} induction_tac);
    49 
    50 end