src/Tools/induction.ML
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (8 weeks ago)
changeset 69981 3dced198b9ec
parent 67149 e61557884799
permissions -rw-r--r--
more strict AFP properties;
     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_context_tactic: 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   val induction_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
    14     (string * typ) list list -> term option list -> thm list option ->
    15     thm list -> int -> tactic
    16 end
    17 
    18 structure Induction: INDUCTION =
    19 struct
    20 
    21 val ind_hypsN = "IH";
    22 
    23 fun preds_of t =
    24   (case strip_comb t of
    25     (p as Var _, _) => [p]
    26   | (p as Free _, _) => [p]
    27   | (_, ts) => maps preds_of ts);
    28 
    29 val induction_context_tactic =
    30   Induct.gen_induct_context_tactic (fn arg as ((cases, consumes), th) =>
    31     if not (forall (null o #2 o #1) cases) then arg
    32     else
    33       let
    34         val (prems, concl) = Logic.strip_horn (Thm.prop_of th);
    35         val prems' = drop consumes prems;
    36         val ps = preds_of concl;
    37   
    38         fun hname_of t =
    39           if exists_subterm (member (op aconv) ps) t
    40           then ind_hypsN else Rule_Cases.case_hypsN;
    41   
    42         val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems';
    43         val n = Int.min (length hnamess, length cases);
    44         val cases' =
    45           map (fn (((cn, _), concls), hns) => ((cn, hns), concls))
    46             (take n cases ~~ take n hnamess);
    47       in ((cases', consumes), th) end);
    48 
    49 fun induction_tac ctxt x1 x2 x3 x4 x5 x6 x7 =
    50   Method.NO_CONTEXT_TACTIC ctxt (induction_context_tactic x1 x2 x3 x4 x5 x6 x7);
    51 
    52 val _ =
    53   Theory.local_setup (Induct.gen_induct_setup \<^binding>\<open>induction\<close> induction_context_tactic);
    54 
    55 end