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