src/Tools/induction.ML
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45014 0e847655b2d8
child 56506 c1f04411d43f
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45014
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
     1
signature INDUCTION =
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
     2
sig
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
     3
  val induction_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
     4
    (string * typ) list list -> term option list -> thm list option ->
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
     5
    thm list -> int -> cases_tactic
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
     6
  val setup: theory -> theory
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
     7
end
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
     8
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
     9
structure Induction: INDUCTION =
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    10
struct
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    11
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    12
val ind_hypsN = "IH";
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    13
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    14
fun preds_of t =
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    15
 (case strip_comb t of
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    16
    (p as Var _, _) => [p]
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    17
  | (p as Free _, _) => [p]
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    18
  | (_, ts) => flat(map preds_of ts))
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    19
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    20
fun name_hyps thy (arg as ((cases,consumes),th)) =
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    21
  if not(forall (null o #2 o #1) cases) then arg
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    22
  else
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    23
    let
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    24
      val (prems, concl) = Logic.strip_horn (prop_of th);
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    25
      val prems' = drop consumes prems;
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    26
      val ps = preds_of concl;
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    27
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    28
      fun hname_of t =
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    29
        if exists_subterm (member (op =) ps) t
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    30
        then ind_hypsN else Rule_Cases.case_hypsN
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    31
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    32
      val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems'
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    33
      val n = Int.min (length hnamess, length cases) 
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    34
      val cases' = map (fn (((cn,_),concls),hns) => ((cn,hns),concls))
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    35
        (take n cases ~~ take n hnamess)
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    36
    in ((cases',consumes),th) end
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    37
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    38
val induction_tac = Induct.gen_induct_tac name_hyps
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    39
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    40
val setup = Induct.gen_induct_setup @{binding induction} induction_tac
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    41
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    42
end
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
diff changeset
    43