proper header;
authorwenzelm
Mon Apr 06 13:28:54 2015 +0200 (2015-04-06)
changeset 599315ec4f97dd6d4
parent 59930 bdbc4b761c31
child 59932 74872a13f628
proper header;
misc tuning;
src/Tools/induction.ML
     1.1 --- a/src/Tools/induction.ML	Mon Apr 06 12:51:25 2015 +0200
     1.2 +++ b/src/Tools/induction.ML	Mon Apr 06 13:28:54 2015 +0200
     1.3 @@ -1,6 +1,14 @@
     1.4 +(*  Title:      Tools/induction.ML
     1.5 +    Author:     Tobias Nipkow, TU Muenchen
     1.6 +
     1.7 +Alternative proof method "induction" that gives induction hypotheses the
     1.8 +name "IH".
     1.9 +*)
    1.10 +
    1.11  signature INDUCTION =
    1.12  sig
    1.13 -  val induction_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
    1.14 +  val induction_tac: Proof.context -> bool ->
    1.15 +    (binding option * (term * bool)) option list list ->
    1.16      (string * typ) list list -> term option list -> thm list option ->
    1.17      thm list -> int -> cases_tactic
    1.18  end
    1.19 @@ -11,13 +19,13 @@
    1.20  val ind_hypsN = "IH";
    1.21  
    1.22  fun preds_of t =
    1.23 - (case strip_comb t of
    1.24 +  (case strip_comb t of
    1.25      (p as Var _, _) => [p]
    1.26    | (p as Free _, _) => [p]
    1.27 -  | (_, ts) => flat(map preds_of ts))
    1.28 +  | (_, ts) => maps preds_of ts);
    1.29  
    1.30  fun name_hyps (arg as ((cases, consumes), th)) =
    1.31 -  if not(forall (null o #2 o #1) cases) then arg
    1.32 +  if not (forall (null o #2 o #1) cases) then arg
    1.33    else
    1.34      let
    1.35        val (prems, concl) = Logic.strip_horn (Thm.prop_of th);
    1.36 @@ -25,18 +33,18 @@
    1.37        val ps = preds_of concl;
    1.38  
    1.39        fun hname_of t =
    1.40 -        if exists_subterm (member (op =) ps) t
    1.41 -        then ind_hypsN else Rule_Cases.case_hypsN
    1.42 +        if exists_subterm (member (op aconv) ps) t
    1.43 +        then ind_hypsN else Rule_Cases.case_hypsN;
    1.44  
    1.45 -      val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems'
    1.46 -      val n = Int.min (length hnamess, length cases) 
    1.47 -      val cases' = map (fn (((cn,_),concls),hns) => ((cn,hns),concls))
    1.48 -        (take n cases ~~ take n hnamess)
    1.49 -    in ((cases',consumes),th) end
    1.50 +      val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems';
    1.51 +      val n = Int.min (length hnamess, length cases);
    1.52 +      val cases' =
    1.53 +        map (fn (((cn, _), concls), hns) => ((cn, hns), concls))
    1.54 +          (take n cases ~~ take n hnamess);
    1.55 +    in ((cases', consumes), th) end;
    1.56  
    1.57 -val induction_tac = Induct.gen_induct_tac (K name_hyps)
    1.58 +val induction_tac = Induct.gen_induct_tac (K name_hyps);
    1.59  
    1.60 -val _ = Theory.setup (Induct.gen_induct_setup @{binding induction} induction_tac)
    1.61 +val _ = Theory.setup (Induct.gen_induct_setup @{binding induction} induction_tac);
    1.62  
    1.63  end
    1.64 -