# HG changeset patch
# User paulson
# Date 1519378106 0
# Node ID 19c77698a48dfadaa6945baf817ad83f5c487355
# Parent  b39f5bb7d4228e25c595f6c33b74d7c25c558d22# Parent  db202a00a29caeb9c34426ad764d98676a4b52ad
merged

diff -r b39f5bb7d422 -r 19c77698a48d src/HOL/Library/Extended_Nat.thy
--- a/src/HOL/Library/Extended_Nat.thy	Fri Feb 23 08:02:56 2018 +0100
+++ b/src/HOL/Library/Extended_Nat.thy	Fri Feb 23 09:28:26 2018 +0000
@@ -383,6 +383,8 @@
     by (simp split: enat.splits)
   show "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d" for a b c d :: enat
     by (cases a b c d rule: enat2_cases[case_product enat2_cases]) auto
+  show "a < b \<Longrightarrow> a + 1 < b + 1"
+    by (metis add_right_mono eSuc_minus_1 eSuc_plus_1 less_le)
 qed (simp add: zero_enat_def one_enat_def)
 
 (* BH: These equations are already proven generally for any type in
diff -r b39f5bb7d422 -r 19c77698a48d src/HOL/Library/Extended_Nonnegative_Real.thy
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Fri Feb 23 08:02:56 2018 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Fri Feb 23 09:28:26 2018 +0000
@@ -11,7 +11,7 @@
 lemma ereal_ineq_diff_add:
   assumes "b \<noteq> (-\<infinity>::ereal)" "a \<ge> b"
   shows "a = b + (a-b)"
-by (metis add.commute assms(1) assms(2) ereal_eq_minus_iff ereal_minus_le_iff ereal_plus_eq_PInfty)
+by (metis add.commute assms ereal_eq_minus_iff ereal_minus_le_iff ereal_plus_eq_PInfty)
 
 lemma Limsup_const_add:
   fixes c :: "'a::{complete_linorder, linorder_topology, topological_monoid_add, ordered_ab_semigroup_add}"
@@ -345,7 +345,11 @@
      (transfer ; auto intro: add_mono mult_mono mult_ac ereal_left_distrib ereal_mult_left_mono)+
 
 instance ennreal :: linordered_nonzero_semiring
-  proof qed (transfer; simp)
+proof
+  fix a b::ennreal
+  show "a < b \<Longrightarrow> a + 1 < b + 1"
+    by transfer (simp add: add_right_mono ereal_add_cancel_right less_le)
+qed (transfer; simp)
 
 instance ennreal :: strict_ordered_ab_semigroup_add
 proof
diff -r b39f5bb7d422 -r 19c77698a48d src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Fri Feb 23 08:02:56 2018 +0100
+++ b/src/HOL/Nat.thy	Fri Feb 23 09:28:26 2018 +0000
@@ -1774,7 +1774,7 @@
 
 class ring_char_0 = ring_1 + semiring_char_0
 
-context linordered_semidom
+context linordered_nonzero_semiring
 begin
 
 lemma of_nat_0_le_iff [simp]: "0 \<le> of_nat n"
@@ -1783,8 +1783,21 @@
 lemma of_nat_less_0_iff [simp]: "\<not> of_nat m < 0"
   by (simp add: not_less)
 
+lemma of_nat_mono[simp]: "i \<le> j \<Longrightarrow> of_nat i \<le> of_nat j"
+  by (auto simp: le_iff_add intro!: add_increasing2)
+
 lemma of_nat_less_iff [simp]: "of_nat m < of_nat n \<longleftrightarrow> m < n"
-  by (induct m n rule: diff_induct) (simp_all add: add_pos_nonneg)
+proof(induct m n rule: diff_induct)
+  case (1 m) then show ?case
+    by auto
+next
+  case (2 n) then show ?case
+    by (simp add: add_pos_nonneg)
+next
+  case (3 m n)
+  then show ?case
+    by (auto simp: add_commute [of 1] add_mono1 not_less add_right_mono leD)
+qed
 
 lemma of_nat_le_iff [simp]: "of_nat m \<le> of_nat n \<longleftrightarrow> m \<le> n"
   by (simp add: not_less [symmetric] linorder_not_less [symmetric])
@@ -1795,7 +1808,7 @@
 lemma of_nat_less_imp_less: "of_nat m < of_nat n \<Longrightarrow> m < n"
   by simp
 
-text \<open>Every \<open>linordered_semidom\<close> has characteristic zero.\<close>
+text \<open>Every \<open>linordered_nonzero_semiring\<close> has characteristic zero.\<close>
 
 subclass semiring_char_0
   by standard (auto intro!: injI simp add: eq_iff)
@@ -1810,6 +1823,14 @@
 
 end
 
+
+context linordered_semidom
+begin
+subclass linordered_nonzero_semiring ..
+subclass semiring_char_0 ..
+end
+
+
 context linordered_idom
 begin
 
diff -r b39f5bb7d422 -r 19c77698a48d src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Fri Feb 23 08:02:56 2018 +0100
+++ b/src/HOL/Rings.thy	Fri Feb 23 09:28:26 2018 +0000
@@ -2245,7 +2245,8 @@
 
 end
 
-class linordered_nonzero_semiring = ordered_comm_semiring + monoid_mult + linorder + zero_less_one
+class linordered_nonzero_semiring = ordered_comm_semiring + monoid_mult + linorder + zero_less_one +
+  assumes add_mono1: "a < b \<Longrightarrow> a + 1 < b + 1"
 begin
 
 subclass zero_neq_one
@@ -2278,7 +2279,15 @@
   assumes le_add_diff_inverse2 [simp]: "b \<le> a \<Longrightarrow> a - b + b = a"
 begin
 
-subclass linordered_nonzero_semiring ..
+subclass linordered_nonzero_semiring 
+proof
+  show "a + 1 < b + 1" if "a < b" for a b
+  proof (rule ccontr, simp add: not_less)
+    assume "b \<le> a"
+    with that show False
+      by (simp add: )
+  qed
+qed
 
 text \<open>Addition is the inverse of subtraction.\<close>