src/HOL/Nat.thy
changeset 27627 93016de79b02
parent 27625 3a45b555001a
child 27679 6392b92c3536
     1.1 --- a/src/HOL/Nat.thy	Thu Jul 17 13:50:33 2008 +0200
     1.2 +++ b/src/HOL/Nat.thy	Thu Jul 17 15:21:52 2008 +0200
     1.3 @@ -1302,47 +1302,19 @@
     1.4  begin
     1.5  
     1.6  lemma lift_Suc_mono_le:
     1.7 -  assumes mono: "!!n. f n \<le> f(Suc n)" shows "n\<le>n' \<Longrightarrow> f n \<le> f n'"
     1.8 -proof(induct k == "n'-n" arbitrary:n')
     1.9 -  case 0
    1.10 -  moreover hence "n' <= n" by simp
    1.11 -  ultimately have "n=n'" by(blast intro:order_antisym)
    1.12 -  thus ?case by simp
    1.13 -next
    1.14 -  case (Suc k)
    1.15 -  then obtain l where [simp]: "n' = Suc l"
    1.16 -  proof(cases n')
    1.17 -    case 0 thus ?thesis using Suc by simp
    1.18 -  next
    1.19 -    case Suc thus ?thesis using that by blast
    1.20 -  qed
    1.21 -  have "f n \<le> f l" using Suc by auto
    1.22 -  also have "\<dots> \<le> f n'" using mono by auto
    1.23 -  finally(order_trans) show ?case by auto
    1.24 -qed
    1.25 +  assumes mono: "!!n. f n \<le> f(Suc n)" and "n\<le>n'"
    1.26 +  shows "f n \<le> f n'"
    1.27 +proof (cases "n < n'")
    1.28 +  case True
    1.29 +  thus ?thesis
    1.30 +    by (induct n n' rule: less_Suc_induct[consumes 1]) (auto intro: mono)
    1.31 +qed (insert `n \<le> n'`, auto) -- {*trivial for @{prop "n = n'"} *}
    1.32  
    1.33  lemma lift_Suc_mono_less:
    1.34 -  assumes mono: "!!n. f n < f(Suc n)" shows "n<n' \<Longrightarrow> f n < f n'"
    1.35 -proof(induct k == "n' - Suc n" arbitrary:n')
    1.36 -  case 0
    1.37 -  hence "~ n' <= n \<longrightarrow> n' = Suc n" by(simp add:le_Suc_eq)
    1.38 -  moreover have "~ n' <= n"
    1.39 -  proof
    1.40 -    assume "n' <= n" thus False using `n<n'` by(auto dest: le_less_trans)
    1.41 -  qed
    1.42 -  ultimately show ?case by(simp add:mono)
    1.43 -next
    1.44 -  case (Suc k)
    1.45 -  then obtain l where [simp]: "n' = Suc l"
    1.46 -  proof(cases n')
    1.47 -    case 0 thus ?thesis using Suc by simp
    1.48 -  next
    1.49 -    case Suc thus ?thesis using that by blast
    1.50 -  qed
    1.51 -  have "f n < f l" using Suc by auto
    1.52 -  also have "\<dots> < f n'" using mono by auto
    1.53 -  finally(less_trans) show ?case by auto
    1.54 -qed
    1.55 +  assumes mono: "!!n. f n < f(Suc n)" and "n < n'"
    1.56 +  shows "f n < f n'"
    1.57 +using `n < n'`
    1.58 +by (induct n n' rule: less_Suc_induct[consumes 1]) (auto intro: mono)
    1.59  
    1.60  end
    1.61