--- a/src/Tools/induction.ML Mon Apr 06 12:51:25 2015 +0200
+++ b/src/Tools/induction.ML Mon Apr 06 13:28:54 2015 +0200
@@ -1,6 +1,14 @@
+(* Title: Tools/induction.ML
+ Author: Tobias Nipkow, TU Muenchen
+
+Alternative proof method "induction" that gives induction hypotheses the
+name "IH".
+*)
+
signature INDUCTION =
sig
- val induction_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
+ val induction_tac: Proof.context -> bool ->
+ (binding option * (term * bool)) option list list ->
(string * typ) list list -> term option list -> thm list option ->
thm list -> int -> cases_tactic
end
@@ -11,13 +19,13 @@
val ind_hypsN = "IH";
fun preds_of t =
- (case strip_comb t of
+ (case strip_comb t of
(p as Var _, _) => [p]
| (p as Free _, _) => [p]
- | (_, ts) => flat(map preds_of ts))
+ | (_, ts) => maps preds_of ts);
fun name_hyps (arg as ((cases, consumes), th)) =
- if not(forall (null o #2 o #1) cases) then arg
+ if not (forall (null o #2 o #1) cases) then arg
else
let
val (prems, concl) = Logic.strip_horn (Thm.prop_of th);
@@ -25,18 +33,18 @@
val ps = preds_of concl;
fun hname_of t =
- if exists_subterm (member (op =) ps) t
- then ind_hypsN else Rule_Cases.case_hypsN
+ if exists_subterm (member (op aconv) ps) t
+ then ind_hypsN else Rule_Cases.case_hypsN;
- val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems'
- val n = Int.min (length hnamess, length cases)
- val cases' = map (fn (((cn,_),concls),hns) => ((cn,hns),concls))
- (take n cases ~~ take n hnamess)
- in ((cases',consumes),th) end
+ val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems';
+ val n = Int.min (length hnamess, length cases);
+ val cases' =
+ map (fn (((cn, _), concls), hns) => ((cn, hns), concls))
+ (take n cases ~~ take n hnamess);
+ in ((cases', consumes), th) end;
-val induction_tac = Induct.gen_induct_tac (K name_hyps)
+val induction_tac = Induct.gen_induct_tac (K name_hyps);
-val _ = Theory.setup (Induct.gen_induct_setup @{binding induction} induction_tac)
+val _ = Theory.setup (Induct.gen_induct_setup @{binding induction} induction_tac);
end
-