# HG changeset patch # User wenzelm # Date 1428319734 -7200 # Node ID 5ec4f97dd6d42370089020fbe394dc68191d3e7e # Parent bdbc4b761c319ba96112ea7f5c3653d9a02bb30f proper header; misc tuning; diff -r bdbc4b761c31 -r 5ec4f97dd6d4 src/Tools/induction.ML --- 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 -