src/Tools/induction.ML
author wenzelm
Wed Oct 29 19:01:49 2014 +0100 (2014-10-29)
changeset 58826 2ed2eaabe3df
parent 56506 c1f04411d43f
child 59582 0fbed69ff081
permissions -rw-r--r--
modernized setup;
nipkow@45014
     1
signature INDUCTION =
nipkow@45014
     2
sig
nipkow@45014
     3
  val induction_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
nipkow@45014
     4
    (string * typ) list list -> term option list -> thm list option ->
nipkow@45014
     5
    thm list -> int -> cases_tactic
nipkow@45014
     6
end
nipkow@45014
     7
nipkow@45014
     8
structure Induction: INDUCTION =
nipkow@45014
     9
struct
nipkow@45014
    10
nipkow@45014
    11
val ind_hypsN = "IH";
nipkow@45014
    12
nipkow@45014
    13
fun preds_of t =
nipkow@45014
    14
 (case strip_comb t of
nipkow@45014
    15
    (p as Var _, _) => [p]
nipkow@45014
    16
  | (p as Free _, _) => [p]
nipkow@45014
    17
  | (_, ts) => flat(map preds_of ts))
nipkow@45014
    18
wenzelm@56506
    19
fun name_hyps (arg as ((cases, consumes), th)) =
nipkow@45014
    20
  if not(forall (null o #2 o #1) cases) then arg
nipkow@45014
    21
  else
nipkow@45014
    22
    let
nipkow@45014
    23
      val (prems, concl) = Logic.strip_horn (prop_of th);
nipkow@45014
    24
      val prems' = drop consumes prems;
nipkow@45014
    25
      val ps = preds_of concl;
nipkow@45014
    26
nipkow@45014
    27
      fun hname_of t =
nipkow@45014
    28
        if exists_subterm (member (op =) ps) t
nipkow@45014
    29
        then ind_hypsN else Rule_Cases.case_hypsN
nipkow@45014
    30
nipkow@45014
    31
      val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems'
nipkow@45014
    32
      val n = Int.min (length hnamess, length cases) 
nipkow@45014
    33
      val cases' = map (fn (((cn,_),concls),hns) => ((cn,hns),concls))
nipkow@45014
    34
        (take n cases ~~ take n hnamess)
nipkow@45014
    35
    in ((cases',consumes),th) end
nipkow@45014
    36
wenzelm@56506
    37
val induction_tac = Induct.gen_induct_tac (K name_hyps)
nipkow@45014
    38
wenzelm@58826
    39
val _ = Theory.setup (Induct.gen_induct_setup @{binding induction} induction_tac)
nipkow@45014
    40
nipkow@45014
    41
end
nipkow@45014
    42