stronger inc_induct and dec_induct
authorhoelzl
Tue Nov 12 19:28:52 2013 +0100 (2013-11-12)
changeset 54411f72e58a5a75f
parent 54410 0a578fb7fb73
child 54412 900c6d724250
stronger inc_induct and dec_induct
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Nat.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Nov 12 19:28:51 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Nov 12 19:28:52 2013 +0100
     1.3 @@ -2336,12 +2336,11 @@
     1.4    qed
     1.5    {
     1.6      fix n m :: nat
     1.7 -    assume "m \<le> n"
     1.8 -    then have "{A n..B n} \<subseteq> {A m..B m}"
     1.9 -    proof (induct rule: inc_induct)
    1.10 +    assume "m \<le> n" then have "{A n..B n} \<subseteq> {A m..B m}"
    1.11 +    proof (induction rule: inc_induct)
    1.12        case (step i)
    1.13        show ?case
    1.14 -        using AB(4) by (intro order_trans[OF step(2)] subset_interval_imp) auto
    1.15 +        using AB(4) by (intro order_trans[OF step.IH] subset_interval_imp) auto
    1.16      qed simp
    1.17    } note ABsubset = this
    1.18    have "\<exists>a. \<forall>n. a\<in>{A n..B n}"
     2.1 --- a/src/HOL/Nat.thy	Tue Nov 12 19:28:51 2013 +0100
     2.2 +++ b/src/HOL/Nat.thy	Tue Nov 12 19:28:52 2013 +0100
     2.3 @@ -1718,20 +1718,20 @@
     2.4  text {* Specialized induction principles that work "backwards": *}
     2.5  
     2.6  lemma inc_induct[consumes 1, case_names base step]:
     2.7 -  assumes less: "i <= j"
     2.8 +  assumes less: "i \<le> j"
     2.9    assumes base: "P j"
    2.10 -  assumes step: "!!i. [| i < j; P (Suc i) |] ==> P i"
    2.11 +  assumes step: "\<And>n. i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P (Suc n) \<Longrightarrow> P n"
    2.12    shows "P i"
    2.13 -  using less
    2.14 -proof (induct d=="j - i" arbitrary: i)
    2.15 +  using less step
    2.16 +proof (induct d\<equiv>"j - i" arbitrary: i)
    2.17    case (0 i)
    2.18    hence "i = j" by simp
    2.19    with base show ?case by simp
    2.20  next
    2.21 -  case (Suc d i)
    2.22 -  hence "i < j" "P (Suc i)"
    2.23 +  case (Suc d n)
    2.24 +  hence "n \<le> n" "n < j" "P (Suc n)"
    2.25      by simp_all
    2.26 -  thus "P i" by (rule step)
    2.27 +  then show "P n" by fact
    2.28  qed
    2.29  
    2.30  lemma strict_inc_induct[consumes 1, case_names base step]:
    2.31 @@ -1760,9 +1760,8 @@
    2.32  text {* Further induction rule similar to @{thm inc_induct} *}
    2.33  
    2.34  lemma dec_induct[consumes 1, case_names base step]:
    2.35 -  "i \<le> j \<Longrightarrow> P i \<Longrightarrow> (\<And>n. i \<le> n \<Longrightarrow> P n \<Longrightarrow> P (Suc n)) \<Longrightarrow> P j"
    2.36 +  "i \<le> j \<Longrightarrow> P i \<Longrightarrow> (\<And>n. i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P n \<Longrightarrow> P (Suc n)) \<Longrightarrow> P j"
    2.37    by (induct j arbitrary: i) (auto simp: le_Suc_eq)
    2.38 -
    2.39   
    2.40  subsection {* The divides relation on @{typ nat} *}
    2.41