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