author nipkow Thu, 17 Jul 2008 13:50:17 +0200 changeset 27625 3a45b555001a parent 27624 a925aa66e17a child 27626 1a3507f86b39
 src/HOL/Nat.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Nat.thy	Wed Jul 16 17:37:59 2008 +0200
+++ b/src/HOL/Nat.thy	Thu Jul 17 13:50:17 2008 +0200
@@ -1297,6 +1297,56 @@

lemmas [arith_split] = nat_diff_split split_min split_max

+
+context order
+begin
+
+lemma lift_Suc_mono_le:
+  assumes mono: "!!n. f n \<le> f(Suc n)" shows "n\<le>n' \<Longrightarrow> f n \<le> f n'"
+proof(induct k == "n'-n" arbitrary:n')
+  case 0
+  moreover hence "n' <= n" by simp
+  ultimately have "n=n'" by(blast intro:order_antisym)
+  thus ?case by simp
+next
+  case (Suc k)
+  then obtain l where [simp]: "n' = Suc l"
+  proof(cases n')
+    case 0 thus ?thesis using Suc by simp
+  next
+    case Suc thus ?thesis using that by blast
+  qed
+  have "f n \<le> f l" using Suc by auto
+  also have "\<dots> \<le> f n'" using mono by auto
+  finally(order_trans) show ?case by auto
+qed
+
+lemma lift_Suc_mono_less:
+  assumes mono: "!!n. f n < f(Suc n)" shows "n<n' \<Longrightarrow> f n < f n'"
+proof(induct k == "n' - Suc n" arbitrary:n')
+  case 0
+  hence "~ n' <= n \<longrightarrow> n' = Suc n" by(simp add:le_Suc_eq)
+  moreover have "~ n' <= n"
+  proof
+    assume "n' <= n" thus False using `n<n'` by(auto dest: le_less_trans)
+  qed
+  ultimately show ?case by(simp add:mono)
+next
+  case (Suc k)
+  then obtain l where [simp]: "n' = Suc l"
+  proof(cases n')
+    case 0 thus ?thesis using Suc by simp
+  next
+    case Suc thus ?thesis using that by blast
+  qed
+  have "f n < f l" using Suc by auto
+  also have "\<dots> < f n'" using mono by auto
+  finally(less_trans) show ?case by auto
+qed
+
+end
+
+
text{*Subtraction laws, mostly by Clemens Ballarin*}

lemma diff_less_mono: "[| a < (b::nat); c \<le> a |] ==> a-c < b-c"
@@ -1442,6 +1492,7 @@
text{*At present we prove no analogue of @{text not_less_Least} or @{text
Least_Suc}, since there appears to be no need.*}

+
subsection {* size of a datatype value *}

class size = type +```