src/Tools/induction.ML
author wenzelm
Thu, 07 Apr 2016 20:51:52 +0200
changeset 62908 d7009a515733
parent 61844 007d3b34080f
child 67149 e61557884799
permissions -rw-r--r--
clarified mode of ROOT.ML files;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
59931
5ec4f97dd6d4 proper header;
wenzelm
parents: 59582
diff changeset
     1
(*  Title:      Tools/induction.ML
5ec4f97dd6d4 proper header;
wenzelm
parents: 59582
diff changeset
     2
    Author:     Tobias Nipkow, TU Muenchen
5ec4f97dd6d4 proper header;
wenzelm
parents: 59582
diff changeset
     3
5ec4f97dd6d4 proper header;
wenzelm
parents: 59582
diff changeset
     4
Alternative proof method "induction" that gives induction hypotheses the
5ec4f97dd6d4 proper header;
wenzelm
parents: 59582
diff changeset
     5
name "IH".
5ec4f97dd6d4 proper header;
wenzelm
parents: 59582
diff changeset
     6
*)
5ec4f97dd6d4 proper header;
wenzelm
parents: 59582
diff changeset
     7
45014
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
     8
signature INDUCTION =
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
     9
sig
61844
007d3b34080f tuned signature;
wenzelm
parents: 61841
diff changeset
    10
  val induction_context_tactic: bool -> (binding option * (term * bool)) option list list ->
45014
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    11
    (string * typ) list list -> term option list -> thm list option ->
61841
4d3527b94f2a more general types Proof.method / context_tactic;
wenzelm
parents: 59970
diff changeset
    12
    thm list -> int -> context_tactic
61844
007d3b34080f tuned signature;
wenzelm
parents: 61841
diff changeset
    13
  val induction_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
007d3b34080f tuned signature;
wenzelm
parents: 61841
diff changeset
    14
    (string * typ) list list -> term option list -> thm list option ->
007d3b34080f tuned signature;
wenzelm
parents: 61841
diff changeset
    15
    thm list -> int -> tactic
45014
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    16
end
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    17
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    18
structure Induction: INDUCTION =
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    19
struct
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    20
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    21
val ind_hypsN = "IH";
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    22
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    23
fun preds_of t =
59931
5ec4f97dd6d4 proper header;
wenzelm
parents: 59582
diff changeset
    24
  (case strip_comb t of
45014
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    25
    (p as Var _, _) => [p]
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    26
  | (p as Free _, _) => [p]
59931
5ec4f97dd6d4 proper header;
wenzelm
parents: 59582
diff changeset
    27
  | (_, ts) => maps preds_of ts);
45014
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    28
61844
007d3b34080f tuned signature;
wenzelm
parents: 61841
diff changeset
    29
val induction_context_tactic =
007d3b34080f tuned signature;
wenzelm
parents: 61841
diff changeset
    30
  Induct.gen_induct_context_tactic (fn arg as ((cases, consumes), th) =>
007d3b34080f tuned signature;
wenzelm
parents: 61841
diff changeset
    31
    if not (forall (null o #2 o #1) cases) then arg
007d3b34080f tuned signature;
wenzelm
parents: 61841
diff changeset
    32
    else
007d3b34080f tuned signature;
wenzelm
parents: 61841
diff changeset
    33
      let
007d3b34080f tuned signature;
wenzelm
parents: 61841
diff changeset
    34
        val (prems, concl) = Logic.strip_horn (Thm.prop_of th);
007d3b34080f tuned signature;
wenzelm
parents: 61841
diff changeset
    35
        val prems' = drop consumes prems;
007d3b34080f tuned signature;
wenzelm
parents: 61841
diff changeset
    36
        val ps = preds_of concl;
007d3b34080f tuned signature;
wenzelm
parents: 61841
diff changeset
    37
  
007d3b34080f tuned signature;
wenzelm
parents: 61841
diff changeset
    38
        fun hname_of t =
007d3b34080f tuned signature;
wenzelm
parents: 61841
diff changeset
    39
          if exists_subterm (member (op aconv) ps) t
007d3b34080f tuned signature;
wenzelm
parents: 61841
diff changeset
    40
          then ind_hypsN else Rule_Cases.case_hypsN;
007d3b34080f tuned signature;
wenzelm
parents: 61841
diff changeset
    41
  
007d3b34080f tuned signature;
wenzelm
parents: 61841
diff changeset
    42
        val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems';
007d3b34080f tuned signature;
wenzelm
parents: 61841
diff changeset
    43
        val n = Int.min (length hnamess, length cases);
007d3b34080f tuned signature;
wenzelm
parents: 61841
diff changeset
    44
        val cases' =
007d3b34080f tuned signature;
wenzelm
parents: 61841
diff changeset
    45
          map (fn (((cn, _), concls), hns) => ((cn, hns), concls))
007d3b34080f tuned signature;
wenzelm
parents: 61841
diff changeset
    46
            (take n cases ~~ take n hnamess);
007d3b34080f tuned signature;
wenzelm
parents: 61841
diff changeset
    47
      in ((cases', consumes), th) end);
45014
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    48
61844
007d3b34080f tuned signature;
wenzelm
parents: 61841
diff changeset
    49
fun induction_tac ctxt x1 x2 x3 x4 x5 x6 x7 =
007d3b34080f tuned signature;
wenzelm
parents: 61841
diff changeset
    50
  Method.NO_CONTEXT_TACTIC ctxt (induction_context_tactic x1 x2 x3 x4 x5 x6 x7);
45014
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    51
61844
007d3b34080f tuned signature;
wenzelm
parents: 61841
diff changeset
    52
val _ =
007d3b34080f tuned signature;
wenzelm
parents: 61841
diff changeset
    53
  Theory.local_setup (Induct.gen_induct_setup @{binding induction} induction_context_tactic);
45014
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    54
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    55
end