diff --git a/src/HOL/Groups.thy b/src/HOL/Groups.thy
--- a/src/HOL/Groups.thy
+++ b/src/HOL/Groups.thy
@@ -1,1500 +1,1519 @@
 (*  Title:      HOL/Groups.thy
     Author:     Gertrud Bauer
     Author:     Steven Obua
     Author:     Lawrence C Paulson
     Author:     Markus Wenzel
     Author:     Jeremy Avigad
 *)
 
 section \<open>Groups, also combined with orderings\<close>
 
 theory Groups
   imports Orderings
 begin
 
 subsection \<open>Dynamic facts\<close>
 
 named_theorems ac_simps "associativity and commutativity simplification rules"
   and algebra_simps "algebra simplification rules for rings"
   and algebra_split_simps "algebra simplification rules for rings, with potential goal splitting"
   and field_simps "algebra simplification rules for fields"
   and field_split_simps "algebra simplification rules for fields, with potential goal splitting"
 
 text \<open>
   The rewrites accumulated in \<open>algebra_simps\<close> deal with the classical
   algebraic structures of groups, rings and family. They simplify terms by
   multiplying everything out (in case of a ring) and bringing sums and
   products into a canonical form (by ordered rewriting). As a result it
   decides group and ring equalities but also helps with inequalities.
 
   Of course it also works for fields, but it knows nothing about
   multiplicative inverses or division. This is catered for by \<open>field_simps\<close>.
 
   Facts in \<open>field_simps\<close> multiply with denominators in (in)equations if they
   can be proved to be non-zero (for equations) or positive/negative (for
   inequalities). Can be too aggressive and is therefore separate from the more
   benign \<open>algebra_simps\<close>.
 
   Collections \<open>algebra_split_simps\<close> and \<open>field_split_simps\<close>
   correspond to \<open>algebra_simps\<close> and \<open>field_simps\<close>
   but contain more aggresive rules that may lead to goal splitting.
 \<close>
 
 
 subsection \<open>Abstract structures\<close>
 
 text \<open>
   These locales provide basic structures for interpretation into bigger
   structures; extensions require careful thinking, otherwise undesired effects
   may occur due to interpretation.
 \<close>
 
 locale semigroup =
   fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<^bold>*" 70)
   assumes assoc [ac_simps]: "a \<^bold>* b \<^bold>* c = a \<^bold>* (b \<^bold>* c)"
 
 locale abel_semigroup = semigroup +
   assumes commute [ac_simps]: "a \<^bold>* b = b \<^bold>* a"
 begin
 
 lemma left_commute [ac_simps]: "b \<^bold>* (a \<^bold>* c) = a \<^bold>* (b \<^bold>* c)"
 proof -
   have "(b \<^bold>* a) \<^bold>* c = (a \<^bold>* b) \<^bold>* c"
     by (simp only: commute)
   then show ?thesis
     by (simp only: assoc)
 qed
 
 end
 
 locale monoid = semigroup +
   fixes z :: 'a ("\<^bold>1")
   assumes left_neutral [simp]: "\<^bold>1 \<^bold>* a = a"
   assumes right_neutral [simp]: "a \<^bold>* \<^bold>1 = a"
 
 locale comm_monoid = abel_semigroup +
   fixes z :: 'a ("\<^bold>1")
   assumes comm_neutral: "a \<^bold>* \<^bold>1 = a"
 begin
 
 sublocale monoid
   by standard (simp_all add: commute comm_neutral)
 
 end
 
 locale group = semigroup +
   fixes z :: 'a ("\<^bold>1")
   fixes inverse :: "'a \<Rightarrow> 'a"
   assumes group_left_neutral: "\<^bold>1 \<^bold>* a = a"
   assumes left_inverse [simp]:  "inverse a \<^bold>* a = \<^bold>1"
 begin
 
 lemma left_cancel: "a \<^bold>* b = a \<^bold>* c \<longleftrightarrow> b = c"
 proof
   assume "a \<^bold>* b = a \<^bold>* c"
   then have "inverse a \<^bold>* (a \<^bold>* b) = inverse a \<^bold>* (a \<^bold>* c)" by simp
   then have "(inverse a \<^bold>* a) \<^bold>* b = (inverse a \<^bold>* a) \<^bold>* c"
     by (simp only: assoc)
   then show "b = c" by (simp add: group_left_neutral)
 qed simp
 
 sublocale monoid
 proof
   fix a
   have "inverse a \<^bold>* a = \<^bold>1" by simp
   then have "inverse a \<^bold>* (a \<^bold>* \<^bold>1) = inverse a \<^bold>* a"
     by (simp add: group_left_neutral assoc [symmetric])
   with left_cancel show "a \<^bold>* \<^bold>1 = a"
     by (simp only: left_cancel)
 qed (fact group_left_neutral)
 
 lemma inverse_unique:
   assumes "a \<^bold>* b = \<^bold>1"
   shows "inverse a = b"
 proof -
   from assms have "inverse a \<^bold>* (a \<^bold>* b) = inverse a"
     by simp
   then show ?thesis
     by (simp add: assoc [symmetric])
 qed
 
 lemma inverse_neutral [simp]: "inverse \<^bold>1 = \<^bold>1"
   by (rule inverse_unique) simp
 
 lemma inverse_inverse [simp]: "inverse (inverse a) = a"
   by (rule inverse_unique) simp
 
 lemma right_inverse [simp]: "a \<^bold>* inverse a = \<^bold>1"
 proof -
   have "a \<^bold>* inverse a = inverse (inverse a) \<^bold>* inverse a"
     by simp
   also have "\<dots> = \<^bold>1"
     by (rule left_inverse)
   then show ?thesis by simp
 qed
 
 lemma inverse_distrib_swap: "inverse (a \<^bold>* b) = inverse b \<^bold>* inverse a"
 proof (rule inverse_unique)
   have "a \<^bold>* b \<^bold>* (inverse b \<^bold>* inverse a) =
     a \<^bold>* (b \<^bold>* inverse b) \<^bold>* inverse a"
     by (simp only: assoc)
   also have "\<dots> = \<^bold>1"
     by simp
   finally show "a \<^bold>* b \<^bold>* (inverse b \<^bold>* inverse a) = \<^bold>1" .
 qed
 
 lemma right_cancel: "b \<^bold>* a = c \<^bold>* a \<longleftrightarrow> b = c"
 proof
   assume "b \<^bold>* a = c \<^bold>* a"
   then have "b \<^bold>* a \<^bold>* inverse a= c \<^bold>* a \<^bold>* inverse a"
     by simp
   then show "b = c"
     by (simp add: assoc)
 qed simp
 
 end
 
 
 subsection \<open>Generic operations\<close>
 
 class zero =
   fixes zero :: 'a  ("0")
 
 class one =
   fixes one  :: 'a  ("1")
 
 hide_const (open) zero one
 
 lemma Let_0 [simp]: "Let 0 f = f 0"
   unfolding Let_def ..
 
 lemma Let_1 [simp]: "Let 1 f = f 1"
   unfolding Let_def ..
 
 setup \<open>
   Reorient_Proc.add
     (fn Const(\<^const_name>\<open>Groups.zero\<close>, _) => true
       | Const(\<^const_name>\<open>Groups.one\<close>, _) => true
       | _ => false)
 \<close>
 
 simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc
 simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
 
 typed_print_translation \<open>
   let
     fun tr' c = (c, fn ctxt => fn T => fn ts =>
       if null ts andalso Printer.type_emphasis ctxt T then
         Syntax.const \<^syntax_const>\<open>_constrain\<close> $ Syntax.const c $
           Syntax_Phases.term_of_typ ctxt T
       else raise Match);
   in map tr' [\<^const_syntax>\<open>Groups.one\<close>, \<^const_syntax>\<open>Groups.zero\<close>] end
 \<close> \<comment> \<open>show types that are presumably too general\<close>
 
 class plus =
   fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 65)
 
 class minus =
   fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "-" 65)
 
 class uminus =
   fixes uminus :: "'a \<Rightarrow> 'a"  ("- _" [81] 80)
 
 class times =
   fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
 
 
 subsection \<open>Semigroups and Monoids\<close>
 
 class semigroup_add = plus +
   assumes add_assoc [algebra_simps, algebra_split_simps, field_simps, field_split_simps]:
     "(a + b) + c = a + (b + c)"
 begin
 
 sublocale add: semigroup plus
   by standard (fact add_assoc)
 
 end
 
 hide_fact add_assoc
 
 class ab_semigroup_add = semigroup_add +
   assumes add_commute [algebra_simps, algebra_split_simps, field_simps, field_split_simps]:
     "a + b = b + a"
 begin
 
 sublocale add: abel_semigroup plus
   by standard (fact add_commute)
 
 declare add.left_commute [algebra_simps, algebra_split_simps, field_simps, field_split_simps]
 
 lemmas add_ac = add.assoc add.commute add.left_commute
 
 end
 
 hide_fact add_commute
 
 lemmas add_ac = add.assoc add.commute add.left_commute
 
 class semigroup_mult = times +
   assumes mult_assoc [algebra_simps, algebra_split_simps, field_simps, field_split_simps]:
     "(a * b) * c = a * (b * c)"
 begin
 
 sublocale mult: semigroup times
   by standard (fact mult_assoc)
 
 end
 
 hide_fact mult_assoc
 
 class ab_semigroup_mult = semigroup_mult +
   assumes mult_commute [algebra_simps, algebra_split_simps, field_simps, field_split_simps]:
     "a * b = b * a"
 begin
 
 sublocale mult: abel_semigroup times
   by standard (fact mult_commute)
 
 declare mult.left_commute [algebra_simps, algebra_split_simps, field_simps, field_split_simps]
 
 lemmas mult_ac = mult.assoc mult.commute mult.left_commute
 
 end
 
 hide_fact mult_commute
 
 lemmas mult_ac = mult.assoc mult.commute mult.left_commute
 
 class monoid_add = zero + semigroup_add +
   assumes add_0_left: "0 + a = a"
     and add_0_right: "a + 0 = a"
 begin
 
 sublocale add: monoid plus 0
   by standard (fact add_0_left add_0_right)+
 
 end
 
 lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0"
   by (fact eq_commute)
 
 class comm_monoid_add = zero + ab_semigroup_add +
   assumes add_0: "0 + a = a"
 begin
 
 subclass monoid_add
   by standard (simp_all add: add_0 add.commute [of _ 0])
 
 sublocale add: comm_monoid plus 0
   by standard (simp add: ac_simps)
 
 end
 
 class monoid_mult = one + semigroup_mult +
   assumes mult_1_left: "1 * a  = a"
     and mult_1_right: "a * 1 = a"
 begin
 
 sublocale mult: monoid times 1
   by standard (fact mult_1_left mult_1_right)+
 
 end
 
 lemma one_reorient: "1 = x \<longleftrightarrow> x = 1"
   by (fact eq_commute)
 
 class comm_monoid_mult = one + ab_semigroup_mult +
   assumes mult_1: "1 * a = a"
 begin
 
 subclass monoid_mult
   by standard (simp_all add: mult_1 mult.commute [of _ 1])
 
 sublocale mult: comm_monoid times 1
   by standard (simp add: ac_simps)
 
 end
 
 class cancel_semigroup_add = semigroup_add +
   assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
   assumes add_right_imp_eq: "b + a = c + a \<Longrightarrow> b = c"
 begin
 
 lemma add_left_cancel [simp]: "a + b = a + c \<longleftrightarrow> b = c"
   by (blast dest: add_left_imp_eq)
 
 lemma add_right_cancel [simp]: "b + a = c + a \<longleftrightarrow> b = c"
   by (blast dest: add_right_imp_eq)
 
 end
 
 class cancel_ab_semigroup_add = ab_semigroup_add + minus +
   assumes add_diff_cancel_left' [simp]: "(a + b) - a = b"
   assumes diff_diff_add [algebra_simps, algebra_split_simps, field_simps, field_split_simps]:
     "a - b - c = a - (b + c)"
 begin
 
 lemma add_diff_cancel_right' [simp]: "(a + b) - b = a"
   using add_diff_cancel_left' [of b a] by (simp add: ac_simps)
 
 subclass cancel_semigroup_add
 proof
   fix a b c :: 'a
   assume "a + b = a + c"
   then have "a + b - a = a + c - a"
     by simp
   then show "b = c"
     by simp
 next
   fix a b c :: 'a
   assume "b + a = c + a"
   then have "b + a - a = c + a - a"
     by simp
   then show "b = c"
     by simp
 qed
 
 lemma add_diff_cancel_left [simp]: "(c + a) - (c + b) = a - b"
   unfolding diff_diff_add [symmetric] by simp
 
 lemma add_diff_cancel_right [simp]: "(a + c) - (b + c) = a - b"
   using add_diff_cancel_left [symmetric] by (simp add: ac_simps)
 
 lemma diff_right_commute: "a - c - b = a - b - c"
   by (simp add: diff_diff_add add.commute)
 
 end
 
 class cancel_comm_monoid_add = cancel_ab_semigroup_add + comm_monoid_add
 begin
 
 lemma diff_zero [simp]: "a - 0 = a"
   using add_diff_cancel_right' [of a 0] by simp
 
 lemma diff_cancel [simp]: "a - a = 0"
 proof -
   have "(a + 0) - (a + 0) = 0"
     by (simp only: add_diff_cancel_left diff_zero)
   then show ?thesis by simp
 qed
 
 lemma add_implies_diff:
   assumes "c + b = a"
   shows "c = a - b"
 proof -
   from assms have "(b + c) - (b + 0) = a - b"
     by (simp add: add.commute)
   then show "c = a - b" by simp
 qed
 
 lemma add_cancel_right_right [simp]: "a = a + b \<longleftrightarrow> b = 0"
   (is "?P \<longleftrightarrow> ?Q")
 proof
   assume ?Q
   then show ?P by simp
 next
   assume ?P
   then have "a - a = a + b - a" by simp
   then show ?Q by simp
 qed
 
 lemma add_cancel_right_left [simp]: "a = b + a \<longleftrightarrow> b = 0"
   using add_cancel_right_right [of a b] by (simp add: ac_simps)
 
 lemma add_cancel_left_right [simp]: "a + b = a \<longleftrightarrow> b = 0"
   by (auto dest: sym)
 
 lemma add_cancel_left_left [simp]: "b + a = a \<longleftrightarrow> b = 0"
   by (auto dest: sym)
 
 end
 
 class comm_monoid_diff = cancel_comm_monoid_add +
   assumes zero_diff [simp]: "0 - a = 0"
 begin
 
 lemma diff_add_zero [simp]: "a - (a + b) = 0"
 proof -
   have "a - (a + b) = (a + 0) - (a + b)"
     by simp
   also have "\<dots> = 0"
     by (simp only: add_diff_cancel_left zero_diff)
   finally show ?thesis .
 qed
 
 end
 
 
 subsection \<open>Groups\<close>
 
 class group_add = minus + uminus + monoid_add +
   assumes left_minus: "- a + a = 0"
   assumes add_uminus_conv_diff [simp]: "a + (- b) = a - b"
 begin
 
 lemma diff_conv_add_uminus: "a - b = a + (- b)"
   by simp
 
 sublocale add: group plus 0 uminus
   by standard (simp_all add: left_minus)
 
 lemma minus_unique: "a + b = 0 \<Longrightarrow> - a = b"
   by (fact add.inverse_unique)
 
 lemma minus_zero: "- 0 = 0"
   by (fact add.inverse_neutral)
 
 lemma minus_minus: "- (- a) = a"
   by (fact add.inverse_inverse)
 
 lemma right_minus: "a + - a = 0"
   by (fact add.right_inverse)
 
 lemma diff_self [simp]: "a - a = 0"
   using right_minus [of a] by simp
 
 subclass cancel_semigroup_add
   by standard (simp_all add: add.left_cancel add.right_cancel)
 
 lemma minus_add_cancel [simp]: "- a + (a + b) = b"
   by (simp add: add.assoc [symmetric])
 
 lemma add_minus_cancel [simp]: "a + (- a + b) = b"
   by (simp add: add.assoc [symmetric])
 
 lemma diff_add_cancel [simp]: "a - b + b = a"
   by (simp only: diff_conv_add_uminus add.assoc) simp
 
 lemma add_diff_cancel [simp]: "a + b - b = a"
   by (simp only: diff_conv_add_uminus add.assoc) simp
 
 lemma minus_add: "- (a + b) = - b + - a"
   by (fact add.inverse_distrib_swap)
 
 lemma right_minus_eq [simp]: "a - b = 0 \<longleftrightarrow> a = b"
 proof
   assume "a - b = 0"
   have "a = (a - b) + b" by (simp add: add.assoc)
   also have "\<dots> = b" using \<open>a - b = 0\<close> by simp
   finally show "a = b" .
 next
   assume "a = b"
   then show "a - b = 0" by simp
 qed
 
 lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0"
   by (fact right_minus_eq [symmetric])
 
 lemma diff_0 [simp]: "0 - a = - a"
   by (simp only: diff_conv_add_uminus add_0_left)
 
 lemma diff_0_right [simp]: "a - 0 = a"
   by (simp only: diff_conv_add_uminus minus_zero add_0_right)
 
 lemma diff_minus_eq_add [simp]: "a - - b = a + b"
   by (simp only: diff_conv_add_uminus minus_minus)
 
 lemma neg_equal_iff_equal [simp]: "- a = - b \<longleftrightarrow> a = b"
 proof
   assume "- a = - b"
   then have "- (- a) = - (- b)" by simp
   then show "a = b" by simp
 next
   assume "a = b"
   then show "- a = - b" by simp
 qed
 
 lemma neg_equal_0_iff_equal [simp]: "- a = 0 \<longleftrightarrow> a = 0"
   by (subst neg_equal_iff_equal [symmetric]) simp
 
 lemma neg_0_equal_iff_equal [simp]: "0 = - a \<longleftrightarrow> 0 = a"
   by (subst neg_equal_iff_equal [symmetric]) simp
 
 text \<open>The next two equations can make the simplifier loop!\<close>
 
 lemma equation_minus_iff: "a = - b \<longleftrightarrow> b = - a"
 proof -
   have "- (- a) = - b \<longleftrightarrow> - a = b"
     by (rule neg_equal_iff_equal)
   then show ?thesis
     by (simp add: eq_commute)
 qed
 
 lemma minus_equation_iff: "- a = b \<longleftrightarrow> - b = a"
 proof -
   have "- a = - (- b) \<longleftrightarrow> a = -b"
     by (rule neg_equal_iff_equal)
   then show ?thesis
     by (simp add: eq_commute)
 qed
 
 lemma eq_neg_iff_add_eq_0: "a = - b \<longleftrightarrow> a + b = 0"
 proof
   assume "a = - b"
   then show "a + b = 0" by simp
 next
   assume "a + b = 0"
   moreover have "a + (b + - b) = (a + b) + - b"
     by (simp only: add.assoc)
   ultimately show "a = - b"
     by simp
 qed
 
 lemma add_eq_0_iff2: "a + b = 0 \<longleftrightarrow> a = - b"
   by (fact eq_neg_iff_add_eq_0 [symmetric])
 
 lemma neg_eq_iff_add_eq_0: "- a = b \<longleftrightarrow> a + b = 0"
   by (auto simp add: add_eq_0_iff2)
 
 lemma add_eq_0_iff: "a + b = 0 \<longleftrightarrow> b = - a"
   by (auto simp add: neg_eq_iff_add_eq_0 [symmetric])
 
 lemma minus_diff_eq [simp]: "- (a - b) = b - a"
   by (simp only: neg_eq_iff_add_eq_0 diff_conv_add_uminus add.assoc minus_add_cancel) simp
 
 lemma add_diff_eq [algebra_simps, algebra_split_simps, field_simps, field_split_simps]:
     "a + (b - c) = (a + b) - c"
   by (simp only: diff_conv_add_uminus add.assoc)
 
 lemma diff_add_eq_diff_diff_swap: "a - (b + c) = a - c - b"
   by (simp only: diff_conv_add_uminus add.assoc minus_add)
 
 lemma diff_eq_eq [algebra_simps, algebra_split_simps, field_simps, field_split_simps]:
   "a - b = c \<longleftrightarrow> a = c + b"
   by auto
 
 lemma eq_diff_eq [algebra_simps, algebra_split_simps, field_simps, field_split_simps]:
   "a = c - b \<longleftrightarrow> a + b = c"
   by auto
 
 lemma diff_diff_eq2 [algebra_simps, algebra_split_simps, field_simps, field_split_simps]:
   "a - (b - c) = (a + c) - b"
   by (simp only: diff_conv_add_uminus add.assoc) simp
 
 lemma diff_eq_diff_eq: "a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d"
   by (simp only: eq_iff_diff_eq_0 [of a b] eq_iff_diff_eq_0 [of c d])
 
 end
 
 class ab_group_add = minus + uminus + comm_monoid_add +
   assumes ab_left_minus: "- a + a = 0"
   assumes ab_diff_conv_add_uminus: "a - b = a + (- b)"
 begin
 
 subclass group_add
   by standard (simp_all add: ab_left_minus ab_diff_conv_add_uminus)
 
 subclass cancel_comm_monoid_add
 proof
   fix a b c :: 'a
   have "b + a - a = b"
     by simp
   then show "a + b - a = b"
     by (simp add: ac_simps)
   show "a - b - c = a - (b + c)"
     by (simp add: algebra_simps)
 qed
 
 lemma uminus_add_conv_diff [simp]: "- a + b = b - a"
   by (simp add: add.commute)
 
 lemma minus_add_distrib [simp]: "- (a + b) = - a + - b"
   by (simp add: algebra_simps)
 
 lemma diff_add_eq [algebra_simps, algebra_split_simps, field_simps, field_split_simps]:
   "(a - b) + c = (a + c) - b"
   by (simp add: algebra_simps)
 
 lemma minus_diff_commute:
   "- b - a = - a - b"
   by (simp only: diff_conv_add_uminus add.commute)
 
 end
 
 
 subsection \<open>(Partially) Ordered Groups\<close>
 
 text \<open>
   The theory of partially ordered groups is taken from the books:
 
     \<^item> \<^emph>\<open>Lattice Theory\<close> by Garret Birkhoff, American Mathematical Society, 1979
     \<^item> \<^emph>\<open>Partially Ordered Algebraic Systems\<close>, Pergamon Press, 1963
 
   Most of the used notions can also be looked up in
     \<^item> \<^url>\<open>http://www.mathworld.com\<close> by Eric Weisstein et. al.
     \<^item> \<^emph>\<open>Algebra I\<close> by van der Waerden, Springer
 \<close>
 
 class ordered_ab_semigroup_add = order + ab_semigroup_add +
   assumes add_left_mono: "a \<le> b \<Longrightarrow> c + a \<le> c + b"
 begin
 
 lemma add_right_mono: "a \<le> b \<Longrightarrow> a + c \<le> b + c"
   by (simp add: add.commute [of _ c] add_left_mono)
 
 text \<open>non-strict, in both arguments\<close>
 lemma add_mono: "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c \<le> b + d"
   apply (erule add_right_mono [THEN order_trans])
   apply (simp add: add.commute add_left_mono)
   done
 
 end
 
 text \<open>Strict monotonicity in both arguments\<close>
 class strict_ordered_ab_semigroup_add = ordered_ab_semigroup_add +
   assumes add_strict_mono: "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
 
 class ordered_cancel_ab_semigroup_add =
   ordered_ab_semigroup_add + cancel_ab_semigroup_add
 begin
 
 lemma add_strict_left_mono: "a < b \<Longrightarrow> c + a < c + b"
   by (auto simp add: less_le add_left_mono)
 
 lemma add_strict_right_mono: "a < b \<Longrightarrow> a + c < b + c"
   by (simp add: add.commute [of _ c] add_strict_left_mono)
 
 subclass strict_ordered_ab_semigroup_add
   apply standard
   apply (erule add_strict_right_mono [THEN less_trans])
   apply (erule add_strict_left_mono)
   done
 
 lemma add_less_le_mono: "a < b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c < b + d"
   apply (erule add_strict_right_mono [THEN less_le_trans])
   apply (erule add_left_mono)
   done
 
 lemma add_le_less_mono: "a \<le> b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
   apply (erule add_right_mono [THEN le_less_trans])
   apply (erule add_strict_left_mono)
   done
 
 end
 
 class ordered_ab_semigroup_add_imp_le = ordered_cancel_ab_semigroup_add +
   assumes add_le_imp_le_left: "c + a \<le> c + b \<Longrightarrow> a \<le> b"
 begin
 
 lemma add_less_imp_less_left:
   assumes less: "c + a < c + b"
   shows "a < b"
 proof -
   from less have le: "c + a \<le> c + b"
     by (simp add: order_le_less)
   have "a \<le> b"
     apply (insert le)
     apply (drule add_le_imp_le_left)
     apply (insert le)
     apply (drule add_le_imp_le_left)
     apply assumption
     done
   moreover have "a \<noteq> b"
   proof (rule ccontr)
     assume "\<not> ?thesis"
     then have "a = b" by simp
     then have "c + a = c + b" by simp
     with less show "False" by simp
   qed
   ultimately show "a < b"
     by (simp add: order_le_less)
 qed
 
 lemma add_less_imp_less_right: "a + c < b + c \<Longrightarrow> a < b"
   by (rule add_less_imp_less_left [of c]) (simp add: add.commute)
 
 lemma add_less_cancel_left [simp]: "c + a < c + b \<longleftrightarrow> a < b"
   by (blast intro: add_less_imp_less_left add_strict_left_mono)
 
 lemma add_less_cancel_right [simp]: "a + c < b + c \<longleftrightarrow> a < b"
   by (blast intro: add_less_imp_less_right add_strict_right_mono)
 
 lemma add_le_cancel_left [simp]: "c + a \<le> c + b \<longleftrightarrow> a \<le> b"
   apply auto
    apply (drule add_le_imp_le_left)
    apply (simp_all add: add_left_mono)
   done
 
 lemma add_le_cancel_right [simp]: "a + c \<le> b + c \<longleftrightarrow> a \<le> b"
   by (simp add: add.commute [of a c] add.commute [of b c])
 
 lemma add_le_imp_le_right: "a + c \<le> b + c \<Longrightarrow> a \<le> b"
   by simp
 
 lemma max_add_distrib_left: "max x y + z = max (x + z) (y + z)"
   unfolding max_def by auto
 
 lemma min_add_distrib_left: "min x y + z = min (x + z) (y + z)"
   unfolding min_def by auto
 
 lemma max_add_distrib_right: "x + max y z = max (x + y) (x + z)"
   unfolding max_def by auto
 
 lemma min_add_distrib_right: "x + min y z = min (x + y) (x + z)"
   unfolding min_def by auto
 
 end
 
 subsection \<open>Support for reasoning about signs\<close>
 
 class ordered_comm_monoid_add = comm_monoid_add + ordered_ab_semigroup_add
 begin
 
 lemma add_nonneg_nonneg [simp]: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a + b"
   using add_mono[of 0 a 0 b] by simp
 
 lemma add_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> a + b \<le> 0"
   using add_mono[of a 0 b 0] by simp
 
 lemma add_nonneg_eq_0_iff: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   using add_left_mono[of 0 y x] add_right_mono[of 0 x y] by auto
 
 lemma add_nonpos_eq_0_iff: "x \<le> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   using add_left_mono[of y 0 x] add_right_mono[of x 0 y] by auto
 
 lemma add_increasing: "0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c"
   using add_mono [of 0 a b c] by simp
 
 lemma add_increasing2: "0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c"
   by (simp add: add_increasing add.commute [of a])
 
 lemma add_decreasing: "a \<le> 0 \<Longrightarrow> c \<le> b \<Longrightarrow> a + c \<le> b"
   using add_mono [of a 0 c b] by simp
 
 lemma add_decreasing2: "c \<le> 0 \<Longrightarrow> a \<le> b \<Longrightarrow> a + c \<le> b"
   using add_mono[of a b c 0] by simp
 
 lemma add_pos_nonneg: "0 < a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 < a + b"
   using less_le_trans[of 0 a "a + b"] by (simp add: add_increasing2)
 
 lemma add_pos_pos: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a + b"
   by (intro add_pos_nonneg less_imp_le)
 
 lemma add_nonneg_pos: "0 \<le> a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a + b"
   using add_pos_nonneg[of b a] by (simp add: add_commute)
 
 lemma add_neg_nonpos: "a < 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> a + b < 0"
   using le_less_trans[of "a + b" a 0] by (simp add: add_decreasing2)
 
 lemma add_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> a + b < 0"
   by (intro add_neg_nonpos less_imp_le)
 
 lemma add_nonpos_neg: "a \<le> 0 \<Longrightarrow> b < 0 \<Longrightarrow> a + b < 0"
   using add_neg_nonpos[of b a] by (simp add: add_commute)
 
 lemmas add_sign_intros =
   add_pos_nonneg add_pos_pos add_nonneg_pos add_nonneg_nonneg
   add_neg_nonpos add_neg_neg add_nonpos_neg add_nonpos_nonpos
 
 end
 
 class strict_ordered_comm_monoid_add = comm_monoid_add + strict_ordered_ab_semigroup_add
 begin
 
 lemma pos_add_strict: "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
   using add_strict_mono [of 0 a b c] by simp
 
 end
 
 class ordered_cancel_comm_monoid_add = ordered_comm_monoid_add + cancel_ab_semigroup_add
 begin
 
 subclass ordered_cancel_ab_semigroup_add ..
 subclass strict_ordered_comm_monoid_add ..
 
 lemma add_strict_increasing: "0 < a \<Longrightarrow> b \<le> c \<Longrightarrow> b < a + c"
   using add_less_le_mono [of 0 a b c] by simp
 
 lemma add_strict_increasing2: "0 \<le> a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
   using add_le_less_mono [of 0 a b c] by simp
 
 end
 
 class ordered_ab_semigroup_monoid_add_imp_le = monoid_add + ordered_ab_semigroup_add_imp_le
 begin
 
 lemma add_less_same_cancel1 [simp]: "b + a < b \<longleftrightarrow> a < 0"
   using add_less_cancel_left [of _ _ 0] by simp
 
 lemma add_less_same_cancel2 [simp]: "a + b < b \<longleftrightarrow> a < 0"
   using add_less_cancel_right [of _ _ 0] by simp
 
 lemma less_add_same_cancel1 [simp]: "a < a + b \<longleftrightarrow> 0 < b"
   using add_less_cancel_left [of _ 0] by simp
 
 lemma less_add_same_cancel2 [simp]: "a < b + a \<longleftrightarrow> 0 < b"
   using add_less_cancel_right [of 0] by simp
 
 lemma add_le_same_cancel1 [simp]: "b + a \<le> b \<longleftrightarrow> a \<le> 0"
   using add_le_cancel_left [of _ _ 0] by simp
 
 lemma add_le_same_cancel2 [simp]: "a + b \<le> b \<longleftrightarrow> a \<le> 0"
   using add_le_cancel_right [of _ _ 0] by simp
 
 lemma le_add_same_cancel1 [simp]: "a \<le> a + b \<longleftrightarrow> 0 \<le> b"
   using add_le_cancel_left [of _ 0] by simp
 
 lemma le_add_same_cancel2 [simp]: "a \<le> b + a \<longleftrightarrow> 0 \<le> b"
   using add_le_cancel_right [of 0] by simp
 
 subclass cancel_comm_monoid_add
   by standard auto
 
 subclass ordered_cancel_comm_monoid_add
   by standard
 
 end
 
 class ordered_ab_group_add = ab_group_add + ordered_ab_semigroup_add
 begin
 
 subclass ordered_cancel_ab_semigroup_add ..
 
 subclass ordered_ab_semigroup_monoid_add_imp_le
 proof
   fix a b c :: 'a
   assume "c + a \<le> c + b"
   then have "(-c) + (c + a) \<le> (-c) + (c + b)"
     by (rule add_left_mono)
   then have "((-c) + c) + a \<le> ((-c) + c) + b"
     by (simp only: add.assoc)
   then show "a \<le> b" by simp
 qed
 
 lemma max_diff_distrib_left: "max x y - z = max (x - z) (y - z)"
   using max_add_distrib_left [of x y "- z"] by simp
 
 lemma min_diff_distrib_left: "min x y - z = min (x - z) (y - z)"
   using min_add_distrib_left [of x y "- z"] by simp
 
 lemma le_imp_neg_le:
   assumes "a \<le> b"
   shows "- b \<le> - a"
 proof -
   from assms have "- a + a \<le> - a + b"
     by (rule add_left_mono)
   then have "0 \<le> - a + b"
     by simp
   then have "0 + (- b) \<le> (- a + b) + (- b)"
     by (rule add_right_mono)
   then show ?thesis
     by (simp add: algebra_simps)
 qed
 
 lemma neg_le_iff_le [simp]: "- b \<le> - a \<longleftrightarrow> a \<le> b"
 proof
   assume "- b \<le> - a"
   then have "- (- a) \<le> - (- b)"
     by (rule le_imp_neg_le)
   then show "a \<le> b"
     by simp
 next
   assume "a \<le> b"
   then show "- b \<le> - a"
     by (rule le_imp_neg_le)
 qed
 
 lemma neg_le_0_iff_le [simp]: "- a \<le> 0 \<longleftrightarrow> 0 \<le> a"
   by (subst neg_le_iff_le [symmetric]) simp
 
 lemma neg_0_le_iff_le [simp]: "0 \<le> - a \<longleftrightarrow> a \<le> 0"
   by (subst neg_le_iff_le [symmetric]) simp
 
 lemma neg_less_iff_less [simp]: "- b < - a \<longleftrightarrow> a < b"
   by (auto simp add: less_le)
 
 lemma neg_less_0_iff_less [simp]: "- a < 0 \<longleftrightarrow> 0 < a"
   by (subst neg_less_iff_less [symmetric]) simp
 
 lemma neg_0_less_iff_less [simp]: "0 < - a \<longleftrightarrow> a < 0"
   by (subst neg_less_iff_less [symmetric]) simp
 
 text \<open>The next several equations can make the simplifier loop!\<close>
 
 lemma less_minus_iff: "a < - b \<longleftrightarrow> b < - a"
 proof -
   have "- (- a) < - b \<longleftrightarrow> b < - a"
     by (rule neg_less_iff_less)
   then show ?thesis by simp
 qed
 
 lemma minus_less_iff: "- a < b \<longleftrightarrow> - b < a"
 proof -
   have "- a < - (- b) \<longleftrightarrow> - b < a"
     by (rule neg_less_iff_less)
   then show ?thesis by simp
 qed
 
 lemma le_minus_iff: "a \<le> - b \<longleftrightarrow> b \<le> - a"
 proof -
   have mm: "- (- a) < - b \<Longrightarrow> - (- b) < -a" for a b :: 'a
     by (simp only: minus_less_iff)
   have "- (- a) \<le> - b \<longleftrightarrow> b \<le> - a"
     apply (auto simp only: le_less)
       apply (drule mm)
       apply (simp_all)
     apply (drule mm[simplified], assumption)
     done
   then show ?thesis by simp
 qed
 
 lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a"
   by (auto simp add: le_less minus_less_iff)
 
 lemma diff_less_0_iff_less [simp]: "a - b < 0 \<longleftrightarrow> a < b"
 proof -
   have "a - b < 0 \<longleftrightarrow> a + (- b) < b + (- b)"
     by simp
   also have "\<dots> \<longleftrightarrow> a < b"
     by (simp only: add_less_cancel_right)
   finally show ?thesis .
 qed
 
 lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric]
 
 lemma diff_less_eq [algebra_simps, algebra_split_simps, field_simps, field_split_simps]:
   "a - b < c \<longleftrightarrow> a < c + b"
   apply (subst less_iff_diff_less_0 [of a])
   apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
   apply (simp add: algebra_simps)
   done
 
 lemma less_diff_eq [algebra_simps, algebra_split_simps, field_simps, field_split_simps]:
   "a < c - b \<longleftrightarrow> a + b < c"
   apply (subst less_iff_diff_less_0 [of "a + b"])
   apply (subst less_iff_diff_less_0 [of a])
   apply (simp add: algebra_simps)
   done
 
 lemma diff_gt_0_iff_gt [simp]: "a - b > 0 \<longleftrightarrow> a > b"
   by (simp add: less_diff_eq)
 
 lemma diff_le_eq [algebra_simps, algebra_split_simps, field_simps, field_split_simps]:
   "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
   by (auto simp add: le_less diff_less_eq )
 
 lemma le_diff_eq [algebra_simps, algebra_split_simps, field_simps, field_split_simps]:
   "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
   by (auto simp add: le_less less_diff_eq)
 
 lemma diff_le_0_iff_le [simp]: "a - b \<le> 0 \<longleftrightarrow> a \<le> b"
   by (simp add: algebra_simps)
 
 lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]
 
 lemma diff_ge_0_iff_ge [simp]: "a - b \<ge> 0 \<longleftrightarrow> a \<ge> b"
   by (simp add: le_diff_eq)
 
 lemma diff_eq_diff_less: "a - b = c - d \<Longrightarrow> a < b \<longleftrightarrow> c < d"
   by (auto simp only: less_iff_diff_less_0 [of a b] less_iff_diff_less_0 [of c d])
 
 lemma diff_eq_diff_less_eq: "a - b = c - d \<Longrightarrow> a \<le> b \<longleftrightarrow> c \<le> d"
   by (auto simp only: le_iff_diff_le_0 [of a b] le_iff_diff_le_0 [of c d])
 
 lemma diff_mono: "a \<le> b \<Longrightarrow> d \<le> c \<Longrightarrow> a - c \<le> b - d"
   by (simp add: field_simps add_mono)
 
 lemma diff_left_mono: "b \<le> a \<Longrightarrow> c - a \<le> c - b"
   by (simp add: field_simps)
 
 lemma diff_right_mono: "a \<le> b \<Longrightarrow> a - c \<le> b - c"
   by (simp add: field_simps)
 
 lemma diff_strict_mono: "a < b \<Longrightarrow> d < c \<Longrightarrow> a - c < b - d"
   by (simp add: field_simps add_strict_mono)
 
 lemma diff_strict_left_mono: "b < a \<Longrightarrow> c - a < c - b"
   by (simp add: field_simps)
 
 lemma diff_strict_right_mono: "a < b \<Longrightarrow> a - c < b - c"
   by (simp add: field_simps)
 
 end
 
 locale group_cancel
 begin
 
 lemma add1: "(A::'a::comm_monoid_add) \<equiv> k + a \<Longrightarrow> A + b \<equiv> k + (a + b)"
   by (simp only: ac_simps)
 
 lemma add2: "(B::'a::comm_monoid_add) \<equiv> k + b \<Longrightarrow> a + B \<equiv> k + (a + b)"
   by (simp only: ac_simps)
 
 lemma sub1: "(A::'a::ab_group_add) \<equiv> k + a \<Longrightarrow> A - b \<equiv> k + (a - b)"
   by (simp only: add_diff_eq)
 
 lemma sub2: "(B::'a::ab_group_add) \<equiv> k + b \<Longrightarrow> a - B \<equiv> - k + (a - b)"
   by (simp only: minus_add diff_conv_add_uminus ac_simps)
 
 lemma neg1: "(A::'a::ab_group_add) \<equiv> k + a \<Longrightarrow> - A \<equiv> - k + - a"
   by (simp only: minus_add_distrib)
 
 lemma rule0: "(a::'a::comm_monoid_add) \<equiv> a + 0"
   by (simp only: add_0_right)
 
 end
 
 ML_file \<open>Tools/group_cancel.ML\<close>
 
 simproc_setup group_cancel_add ("a + b::'a::ab_group_add") =
   \<open>fn phi => fn ss => try Group_Cancel.cancel_add_conv\<close>
 
 simproc_setup group_cancel_diff ("a - b::'a::ab_group_add") =
   \<open>fn phi => fn ss => try Group_Cancel.cancel_diff_conv\<close>
 
 simproc_setup group_cancel_eq ("a = (b::'a::ab_group_add)") =
   \<open>fn phi => fn ss => try Group_Cancel.cancel_eq_conv\<close>
 
 simproc_setup group_cancel_le ("a \<le> (b::'a::ordered_ab_group_add)") =
   \<open>fn phi => fn ss => try Group_Cancel.cancel_le_conv\<close>
 
 simproc_setup group_cancel_less ("a < (b::'a::ordered_ab_group_add)") =
   \<open>fn phi => fn ss => try Group_Cancel.cancel_less_conv\<close>
 
 class linordered_ab_semigroup_add =
   linorder + ordered_ab_semigroup_add
 
 class linordered_cancel_ab_semigroup_add =
   linorder + ordered_cancel_ab_semigroup_add
 begin
 
 subclass linordered_ab_semigroup_add ..
 
 subclass ordered_ab_semigroup_add_imp_le
 proof
   fix a b c :: 'a
   assume le1: "c + a \<le> c + b"
   show "a \<le> b"
   proof (rule ccontr)
     assume *: "\<not> ?thesis"
     then have "b \<le> a" by (simp add: linorder_not_le)
     then have "c + b \<le> c + a" by (rule add_left_mono)
     with le1 have "a = b"
       apply -
       apply (drule antisym)
        apply simp_all
       done
     with * show False
       by (simp add: linorder_not_le [symmetric])
   qed
 qed
 
 end
 
 class linordered_ab_group_add = linorder + ordered_ab_group_add
 begin
 
 subclass linordered_cancel_ab_semigroup_add ..
 
 lemma equal_neg_zero [simp]: "a = - a \<longleftrightarrow> a = 0"
 proof
   assume "a = 0"
   then show "a = - a" by simp
 next
   assume A: "a = - a"
   show "a = 0"
   proof (cases "0 \<le> a")
     case True
     with A have "0 \<le> - a" by auto
     with le_minus_iff have "a \<le> 0" by simp
     with True show ?thesis by (auto intro: order_trans)
   next
     case False
     then have B: "a \<le> 0" by auto
     with A have "- a \<le> 0" by auto
     with B show ?thesis by (auto intro: order_trans)
   qed
 qed
 
 lemma neg_equal_zero [simp]: "- a = a \<longleftrightarrow> a = 0"
   by (auto dest: sym)
 
 lemma neg_less_eq_nonneg [simp]: "- a \<le> a \<longleftrightarrow> 0 \<le> a"
 proof
   assume *: "- a \<le> a"
   show "0 \<le> a"
   proof (rule classical)
     assume "\<not> ?thesis"
     then have "a < 0" by auto
     with * have "- a < 0" by (rule le_less_trans)
     then show ?thesis by auto
   qed
 next
   assume *: "0 \<le> a"
   then have "- a \<le> 0" by (simp add: minus_le_iff)
   from this * show "- a \<le> a" by (rule order_trans)
 qed
 
 lemma neg_less_pos [simp]: "- a < a \<longleftrightarrow> 0 < a"
   by (auto simp add: less_le)
 
 lemma less_eq_neg_nonpos [simp]: "a \<le> - a \<longleftrightarrow> a \<le> 0"
   using neg_less_eq_nonneg [of "- a"] by simp
 
 lemma less_neg_neg [simp]: "a < - a \<longleftrightarrow> a < 0"
   using neg_less_pos [of "- a"] by simp
 
 lemma double_zero [simp]: "a + a = 0 \<longleftrightarrow> a = 0"
 proof
   assume "a + a = 0"
   then have a: "- a = a" by (rule minus_unique)
   then show "a = 0" by (simp only: neg_equal_zero)
 next
   assume "a = 0"
   then show "a + a = 0" by simp
 qed
 
 lemma double_zero_sym [simp]: "0 = a + a \<longleftrightarrow> a = 0"
   apply (rule iffI)
    apply (drule sym)
    apply simp_all
   done
 
 lemma zero_less_double_add_iff_zero_less_single_add [simp]: "0 < a + a \<longleftrightarrow> 0 < a"
 proof
   assume "0 < a + a"
   then have "0 - a < a" by (simp only: diff_less_eq)
   then have "- a < a" by simp
   then show "0 < a" by simp
 next
   assume "0 < a"
   with this have "0 + 0 < a + a"
     by (rule add_strict_mono)
   then show "0 < a + a" by simp
 qed
 
 lemma zero_le_double_add_iff_zero_le_single_add [simp]: "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
   by (auto simp add: le_less)
 
 lemma double_add_less_zero_iff_single_add_less_zero [simp]: "a + a < 0 \<longleftrightarrow> a < 0"
 proof -
   have "\<not> a + a < 0 \<longleftrightarrow> \<not> a < 0"
     by (simp add: not_less)
   then show ?thesis by simp
 qed
 
 lemma double_add_le_zero_iff_single_add_le_zero [simp]: "a + a \<le> 0 \<longleftrightarrow> a \<le> 0"
 proof -
   have "\<not> a + a \<le> 0 \<longleftrightarrow> \<not> a \<le> 0"
     by (simp add: not_le)
   then show ?thesis by simp
 qed
 
 lemma minus_max_eq_min: "- max x y = min (- x) (- y)"
   by (auto simp add: max_def min_def)
 
 lemma minus_min_eq_max: "- min x y = max (- x) (- y)"
   by (auto simp add: max_def min_def)
 
 end
 
 class abs =
   fixes abs :: "'a \<Rightarrow> 'a"  ("\<bar>_\<bar>")
 
 class sgn =
   fixes sgn :: "'a \<Rightarrow> 'a"
 
 class ordered_ab_group_add_abs = ordered_ab_group_add + abs +
   assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"
     and abs_ge_self: "a \<le> \<bar>a\<bar>"
     and abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
     and abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>"
     and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
 begin
 
 lemma abs_minus_le_zero: "- \<bar>a\<bar> \<le> 0"
   unfolding neg_le_0_iff_le by simp
 
 lemma abs_of_nonneg [simp]:
   assumes nonneg: "0 \<le> a"
   shows "\<bar>a\<bar> = a"
 proof (rule antisym)
   show "a \<le> \<bar>a\<bar>" by (rule abs_ge_self)
   from nonneg le_imp_neg_le have "- a \<le> 0" by simp
   from this nonneg have "- a \<le> a" by (rule order_trans)
   then show "\<bar>a\<bar> \<le> a" by (auto intro: abs_leI)
 qed
 
 lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
   by (rule antisym) (auto intro!: abs_ge_self abs_leI order_trans [of "- \<bar>a\<bar>" 0 "\<bar>a\<bar>"])
 
 lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
 proof -
   have "\<bar>a\<bar> = 0 \<Longrightarrow> a = 0"
   proof (rule antisym)
     assume zero: "\<bar>a\<bar> = 0"
     with abs_ge_self show "a \<le> 0" by auto
     from zero have "\<bar>-a\<bar> = 0" by simp
     with abs_ge_self [of "- a"] have "- a \<le> 0" by auto
     with neg_le_0_iff_le show "0 \<le> a" by auto
   qed
   then show ?thesis by auto
 qed
 
 lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
   by simp
 
 lemma abs_0_eq [simp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
 proof -
   have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)
   then show ?thesis by simp
 qed
 
 lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0"
 proof
   assume "\<bar>a\<bar> \<le> 0"
   then have "\<bar>a\<bar> = 0" by (rule antisym) simp
   then show "a = 0" by simp
 next
   assume "a = 0"
   then show "\<bar>a\<bar> \<le> 0" by simp
 qed
 
 lemma abs_le_self_iff [simp]: "\<bar>a\<bar> \<le> a \<longleftrightarrow> 0 \<le> a"
 proof -
   have "0 \<le> \<bar>a\<bar>"
     using abs_ge_zero by blast
   then have "\<bar>a\<bar> \<le> a \<Longrightarrow> 0 \<le> a"
     using order.trans by blast
   then show ?thesis
     using abs_of_nonneg eq_refl by blast
 qed
 
 lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0"
   by (simp add: less_le)
 
 lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0"
 proof -
   have "x \<le> y \<Longrightarrow> \<not> y < x" for x y by auto
   then show ?thesis by simp
 qed
 
 lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>"
 proof -
   have "- a \<le> \<bar>-a\<bar>" by (rule abs_ge_self)
   then show ?thesis by simp
 qed
 
 lemma abs_minus_commute: "\<bar>a - b\<bar> = \<bar>b - a\<bar>"
 proof -
   have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>"
     by (simp only: abs_minus_cancel)
   also have "\<dots> = \<bar>b - a\<bar>" by simp
   finally show ?thesis .
 qed
 
 lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a"
   by (rule abs_of_nonneg) (rule less_imp_le)
 
 lemma abs_of_nonpos [simp]:
   assumes "a \<le> 0"
   shows "\<bar>a\<bar> = - a"
 proof -
   let ?b = "- a"
   have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?b)"
     unfolding abs_minus_cancel [of ?b]
     unfolding neg_le_0_iff_le [of ?b]
     unfolding minus_minus by (erule abs_of_nonneg)
   then show ?thesis using assms by auto
 qed
 
 lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a"
   by (rule abs_of_nonpos) (rule less_imp_le)
 
 lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b"
   using abs_ge_self by (blast intro: order_trans)
 
 lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b"
   using abs_le_D1 [of "- a"] by simp
 
 lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b"
   by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
 
 lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"
 proof -
   have "\<bar>a\<bar> = \<bar>b + (a - b)\<bar>"
     by (simp add: algebra_simps)
   then have "\<bar>a\<bar> \<le> \<bar>b\<bar> + \<bar>a - b\<bar>"
     by (simp add: abs_triangle_ineq)
   then show ?thesis
     by (simp add: algebra_simps)
 qed
 
 lemma abs_triangle_ineq2_sym: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>b - a\<bar>"
   by (simp only: abs_minus_commute [of b] abs_triangle_ineq2)
 
 lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>"
   by (simp add: abs_le_iff abs_triangle_ineq2 abs_triangle_ineq2_sym)
 
 lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
 proof -
   have "\<bar>a - b\<bar> = \<bar>a + - b\<bar>"
     by (simp add: algebra_simps)
   also have "\<dots> \<le> \<bar>a\<bar> + \<bar>- b\<bar>"
     by (rule abs_triangle_ineq)
   finally show ?thesis by simp
 qed
 
 lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
 proof -
   have "\<bar>a + b - (c + d)\<bar> = \<bar>(a - c) + (b - d)\<bar>"
     by (simp add: algebra_simps)
   also have "\<dots> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
     by (rule abs_triangle_ineq)
   finally show ?thesis .
 qed
 
 lemma abs_add_abs [simp]: "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>"
   (is "?L = ?R")
 proof (rule antisym)
   show "?L \<ge> ?R" by (rule abs_ge_self)
   have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by (rule abs_triangle_ineq)
   also have "\<dots> = ?R" by simp
   finally show "?L \<le> ?R" .
 qed
 
 end
 
 lemma dense_eq0_I:
   fixes x::"'a::{dense_linorder,ordered_ab_group_add_abs}"
   shows "(\<And>e. 0 < e \<Longrightarrow> \<bar>x\<bar> \<le> e) \<Longrightarrow> x = 0"
   apply (cases "\<bar>x\<bar> = 0")
    apply simp
   apply (simp only: zero_less_abs_iff [symmetric])
   apply (drule dense)
   apply (auto simp add: not_less [symmetric])
   done
 
 hide_fact (open) ab_diff_conv_add_uminus add_0 mult_1 ab_left_minus
 
 lemmas add_0 = add_0_left (* FIXME duplicate *)
 lemmas mult_1 = mult_1_left (* FIXME duplicate *)
 lemmas ab_left_minus = left_minus (* FIXME duplicate *)
 lemmas diff_diff_eq = diff_diff_add (* FIXME duplicate *)
 
 
 subsection \<open>Canonically ordered monoids\<close>
 
 text \<open>Canonically ordered monoids are never groups.\<close>
 
 class canonically_ordered_monoid_add = comm_monoid_add + order +
   assumes le_iff_add: "a \<le> b \<longleftrightarrow> (\<exists>c. b = a + c)"
 begin
 
 lemma zero_le[simp]: "0 \<le> x"
   by (auto simp: le_iff_add)
 
 lemma le_zero_eq[simp]: "n \<le> 0 \<longleftrightarrow> n = 0"
   by (auto intro: antisym)
 
 lemma not_less_zero[simp]: "\<not> n < 0"
   by (auto simp: less_le)
 
 lemma zero_less_iff_neq_zero: "0 < n \<longleftrightarrow> n \<noteq> 0"
   by (auto simp: less_le)
 
 text \<open>This theorem is useful with \<open>blast\<close>\<close>
 lemma gr_zeroI: "(n = 0 \<Longrightarrow> False) \<Longrightarrow> 0 < n"
   by (rule zero_less_iff_neq_zero[THEN iffD2]) iprover
 
 lemma not_gr_zero[simp]: "\<not> 0 < n \<longleftrightarrow> n = 0"
   by (simp add: zero_less_iff_neq_zero)
 
 subclass ordered_comm_monoid_add
   proof qed (auto simp: le_iff_add add_ac)
 
 lemma gr_implies_not_zero: "m < n \<Longrightarrow> n \<noteq> 0"
   by auto
 
 lemma add_eq_0_iff_both_eq_0[simp]: "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   by (intro add_nonneg_eq_0_iff zero_le)
 
 lemma zero_eq_add_iff_both_eq_0[simp]: "0 = x + y \<longleftrightarrow> x = 0 \<and> y = 0"
   using add_eq_0_iff_both_eq_0[of x y] unfolding eq_commute[of 0] .
 
+lemma less_eqE:
+  assumes \<open>a \<le> b\<close>
+  obtains c where \<open>b = a + c\<close>
+  using assms by (auto simp add: le_iff_add)
+
+lemma lessE:
+  assumes \<open>a < b\<close>
+  obtains c where \<open>b = a + c\<close> and \<open>c \<noteq> 0\<close>
+proof -
+  from assms have \<open>a \<le> b\<close> \<open>a \<noteq> b\<close>
+    by simp_all
+  from \<open>a \<le> b\<close> obtain c where \<open>b = a + c\<close>
+    by (rule less_eqE)
+  moreover have \<open>c \<noteq> 0\<close> using \<open>a \<noteq> b\<close> \<open>b = a + c\<close>
+    by auto
+  ultimately show ?thesis
+    by (rule that)
+qed
+
 lemmas zero_order = zero_le le_zero_eq not_less_zero zero_less_iff_neq_zero not_gr_zero
   \<comment> \<open>This should be attributed with \<open>[iff]\<close>, but then \<open>blast\<close> fails in \<open>Set\<close>.\<close>
 
 end
 
 class ordered_cancel_comm_monoid_diff =
   canonically_ordered_monoid_add + comm_monoid_diff + ordered_ab_semigroup_add_imp_le
 begin
 
 context
   fixes a b :: 'a
   assumes le: "a \<le> b"
 begin
 
 lemma add_diff_inverse: "a + (b - a) = b"
   using le by (auto simp add: le_iff_add)
 
 lemma add_diff_assoc: "c + (b - a) = c + b - a"
   using le by (auto simp add: le_iff_add add.left_commute [of c])
 
 lemma add_diff_assoc2: "b - a + c = b + c - a"
   using le by (auto simp add: le_iff_add add.assoc)
 
 lemma diff_add_assoc: "c + b - a = c + (b - a)"
   using le by (simp add: add.commute add_diff_assoc)
 
 lemma diff_add_assoc2: "b + c - a = b - a + c"
   using le by (simp add: add.commute add_diff_assoc)
 
 lemma diff_diff_right: "c - (b - a) = c + a - b"
   by (simp add: add_diff_inverse add_diff_cancel_left [of a c "b - a", symmetric] add.commute)
 
 lemma diff_add: "b - a + a = b"
   by (simp add: add.commute add_diff_inverse)
 
 lemma le_add_diff: "c \<le> b + c - a"
   by (auto simp add: add.commute diff_add_assoc2 le_iff_add)
 
 lemma le_imp_diff_is_add: "a \<le> b \<Longrightarrow> b - a = c \<longleftrightarrow> b = c + a"
   by (auto simp add: add.commute add_diff_inverse)
 
 lemma le_diff_conv2: "c \<le> b - a \<longleftrightarrow> c + a \<le> b"
   (is "?P \<longleftrightarrow> ?Q")
 proof
   assume ?P
   then have "c + a \<le> b - a + a"
     by (rule add_right_mono)
   then show ?Q
     by (simp add: add_diff_inverse add.commute)
 next
   assume ?Q
   then have "a + c \<le> a + (b - a)"
     by (simp add: add_diff_inverse add.commute)
   then show ?P by simp
 qed
 
 end
 
 end
 
 
 subsection \<open>Tools setup\<close>
 
 lemma add_mono_thms_linordered_semiring:
   fixes i j k :: "'a::ordered_ab_semigroup_add"
   shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
     and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
     and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l"
     and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"
   by (rule add_mono, clarify+)+
 
 lemma add_mono_thms_linordered_field:
   fixes i j k :: "'a::ordered_cancel_ab_semigroup_add"
   shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"
     and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"
     and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l"
     and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l"
     and "i < j \<and> k < l \<Longrightarrow> i + k < j + l"
   by (auto intro: add_strict_right_mono add_strict_left_mono
       add_less_le_mono add_le_less_mono add_strict_mono)
 
 code_identifier
   code_module Groups \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
 
 end
diff --git a/src/HOL/Nat.thy b/src/HOL/Nat.thy
--- a/src/HOL/Nat.thy
+++ b/src/HOL/Nat.thy
@@ -1,2529 +1,2533 @@
 (*  Title:      HOL/Nat.thy
     Author:     Tobias Nipkow
     Author:     Lawrence C Paulson
     Author:     Markus Wenzel
 *)
 
 section \<open>Natural numbers\<close>
 
 theory Nat
 imports Inductive Typedef Fun Rings
 begin
 
 subsection \<open>Type \<open>ind\<close>\<close>
 
 typedecl ind
 
 axiomatization Zero_Rep :: ind and Suc_Rep :: "ind \<Rightarrow> ind"
   \<comment> \<open>The axiom of infinity in 2 parts:\<close>
   where Suc_Rep_inject: "Suc_Rep x = Suc_Rep y \<Longrightarrow> x = y"
     and Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep"
 
 
 subsection \<open>Type nat\<close>
 
 text \<open>Type definition\<close>
 
 inductive Nat :: "ind \<Rightarrow> bool"
   where
     Zero_RepI: "Nat Zero_Rep"
   | Suc_RepI: "Nat i \<Longrightarrow> Nat (Suc_Rep i)"
 
 typedef nat = "{n. Nat n}"
   morphisms Rep_Nat Abs_Nat
   using Nat.Zero_RepI by auto
 
 lemma Nat_Rep_Nat: "Nat (Rep_Nat n)"
   using Rep_Nat by simp
 
 lemma Nat_Abs_Nat_inverse: "Nat n \<Longrightarrow> Rep_Nat (Abs_Nat n) = n"
   using Abs_Nat_inverse by simp
 
 lemma Nat_Abs_Nat_inject: "Nat n \<Longrightarrow> Nat m \<Longrightarrow> Abs_Nat n = Abs_Nat m \<longleftrightarrow> n = m"
   using Abs_Nat_inject by simp
 
 instantiation nat :: zero
 begin
 
 definition Zero_nat_def: "0 = Abs_Nat Zero_Rep"
 
 instance ..
 
 end
 
 definition Suc :: "nat \<Rightarrow> nat"
   where "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))"
 
 lemma Suc_not_Zero: "Suc m \<noteq> 0"
   by (simp add: Zero_nat_def Suc_def Suc_RepI Zero_RepI
       Nat_Abs_Nat_inject Suc_Rep_not_Zero_Rep Nat_Rep_Nat)
 
 lemma Zero_not_Suc: "0 \<noteq> Suc m"
   by (rule not_sym) (rule Suc_not_Zero)
 
 lemma Suc_Rep_inject': "Suc_Rep x = Suc_Rep y \<longleftrightarrow> x = y"
   by (rule iffI, rule Suc_Rep_inject) simp_all
 
 lemma nat_induct0:
   assumes "P 0"
     and "\<And>n. P n \<Longrightarrow> P (Suc n)"
   shows "P n"
   using assms
   apply (unfold Zero_nat_def Suc_def)
   apply (rule Rep_Nat_inverse [THEN subst]) \<comment> \<open>types force good instantiation\<close>
   apply (erule Nat_Rep_Nat [THEN Nat.induct])
   apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst])
   done
 
 free_constructors case_nat for "0 :: nat" | Suc pred
   where "pred (0 :: nat) = (0 :: nat)"
     apply atomize_elim
     apply (rename_tac n, induct_tac n rule: nat_induct0, auto)
    apply (simp add: Suc_def Nat_Abs_Nat_inject Nat_Rep_Nat Suc_RepI Suc_Rep_inject' Rep_Nat_inject)
   apply (simp only: Suc_not_Zero)
   done
 
 \<comment> \<open>Avoid name clashes by prefixing the output of \<open>old_rep_datatype\<close> with \<open>old\<close>.\<close>
 setup \<open>Sign.mandatory_path "old"\<close>
 
 old_rep_datatype "0 :: nat" Suc
     apply (erule nat_induct0)
     apply assumption
    apply (rule nat.inject)
   apply (rule nat.distinct(1))
   done
 
 setup \<open>Sign.parent_path\<close>
 
 \<comment> \<open>But erase the prefix for properties that are not generated by \<open>free_constructors\<close>.\<close>
 setup \<open>Sign.mandatory_path "nat"\<close>
 
 declare old.nat.inject[iff del]
   and old.nat.distinct(1)[simp del, induct_simp del]
 
 lemmas induct = old.nat.induct
 lemmas inducts = old.nat.inducts
 lemmas rec = old.nat.rec
 lemmas simps = nat.inject nat.distinct nat.case nat.rec
 
 setup \<open>Sign.parent_path\<close>
 
 abbreviation rec_nat :: "'a \<Rightarrow> (nat \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a"
   where "rec_nat \<equiv> old.rec_nat"
 
 declare nat.sel[code del]
 
 hide_const (open) Nat.pred \<comment> \<open>hide everything related to the selector\<close>
 hide_fact
   nat.case_eq_if
   nat.collapse
   nat.expand
   nat.sel
   nat.exhaust_sel
   nat.split_sel
   nat.split_sel_asm
 
 lemma nat_exhaust [case_names 0 Suc, cases type: nat]:
   "(y = 0 \<Longrightarrow> P) \<Longrightarrow> (\<And>nat. y = Suc nat \<Longrightarrow> P) \<Longrightarrow> P"
   \<comment> \<open>for backward compatibility -- names of variables differ\<close>
   by (rule old.nat.exhaust)
 
 lemma nat_induct [case_names 0 Suc, induct type: nat]:
   fixes n
   assumes "P 0" and "\<And>n. P n \<Longrightarrow> P (Suc n)"
   shows "P n"
   \<comment> \<open>for backward compatibility -- names of variables differ\<close>
   using assms by (rule nat.induct)
 
 hide_fact
   nat_exhaust
   nat_induct0
 
 ML \<open>
 val nat_basic_lfp_sugar =
   let
     val ctr_sugar = the (Ctr_Sugar.ctr_sugar_of_global \<^theory> \<^type_name>\<open>nat\<close>);
     val recx = Logic.varify_types_global \<^term>\<open>rec_nat\<close>;
     val C = body_type (fastype_of recx);
   in
     {T = HOLogic.natT, fp_res_index = 0, C = C, fun_arg_Tsss = [[], [[HOLogic.natT, C]]],
      ctr_sugar = ctr_sugar, recx = recx, rec_thms = @{thms nat.rec}}
   end;
 \<close>
 
 setup \<open>
 let
   fun basic_lfp_sugars_of _ [\<^typ>\<open>nat\<close>] _ _ ctxt =
       ([], [0], [nat_basic_lfp_sugar], [], [], [], TrueI (*dummy*), [], false, ctxt)
     | basic_lfp_sugars_of bs arg_Ts callers callssss ctxt =
       BNF_LFP_Rec_Sugar.default_basic_lfp_sugars_of bs arg_Ts callers callssss ctxt;
 in
   BNF_LFP_Rec_Sugar.register_lfp_rec_extension
     {nested_simps = [], special_endgame_tac = K (K (K (K no_tac))), is_new_datatype = K (K true),
      basic_lfp_sugars_of = basic_lfp_sugars_of, rewrite_nested_rec_call = NONE}
 end
 \<close>
 
 text \<open>Injectiveness and distinctness lemmas\<close>
 
 lemma inj_Suc [simp]:
   "inj_on Suc N"
   by (simp add: inj_on_def)
 
 lemma bij_betw_Suc [simp]:
   "bij_betw Suc M N \<longleftrightarrow> Suc ` M = N"
   by (simp add: bij_betw_def)
 
 lemma Suc_neq_Zero: "Suc m = 0 \<Longrightarrow> R"
   by (rule notE) (rule Suc_not_Zero)
 
 lemma Zero_neq_Suc: "0 = Suc m \<Longrightarrow> R"
   by (rule Suc_neq_Zero) (erule sym)
 
 lemma Suc_inject: "Suc x = Suc y \<Longrightarrow> x = y"
   by (rule inj_Suc [THEN injD])
 
 lemma n_not_Suc_n: "n \<noteq> Suc n"
   by (induct n) simp_all
 
 lemma Suc_n_not_n: "Suc n \<noteq> n"
   by (rule not_sym) (rule n_not_Suc_n)
 
 text \<open>A special form of induction for reasoning about \<^term>\<open>m < n\<close> and \<^term>\<open>m - n\<close>.\<close>
 lemma diff_induct:
   assumes "\<And>x. P x 0"
     and "\<And>y. P 0 (Suc y)"
     and "\<And>x y. P x y \<Longrightarrow> P (Suc x) (Suc y)"
   shows "P m n"
 proof (induct n arbitrary: m)
   case 0
   show ?case by (rule assms(1))
 next
   case (Suc n)
   show ?case
   proof (induct m)
     case 0
     show ?case by (rule assms(2))
   next
     case (Suc m)
     from \<open>P m n\<close> show ?case by (rule assms(3))
   qed
 qed
 
 
 subsection \<open>Arithmetic operators\<close>
 
 instantiation nat :: comm_monoid_diff
 begin
 
 primrec plus_nat
   where
     add_0: "0 + n = (n::nat)"
   | add_Suc: "Suc m + n = Suc (m + n)"
 
 lemma add_0_right [simp]: "m + 0 = m"
   for m :: nat
   by (induct m) simp_all
 
 lemma add_Suc_right [simp]: "m + Suc n = Suc (m + n)"
   by (induct m) simp_all
 
 declare add_0 [code]
 
 lemma add_Suc_shift [code]: "Suc m + n = m + Suc n"
   by simp
 
 primrec minus_nat
   where
     diff_0 [code]: "m - 0 = (m::nat)"
   | diff_Suc: "m - Suc n = (case m - n of 0 \<Rightarrow> 0 | Suc k \<Rightarrow> k)"
 
 declare diff_Suc [simp del]
 
 lemma diff_0_eq_0 [simp, code]: "0 - n = 0"
   for n :: nat
   by (induct n) (simp_all add: diff_Suc)
 
 lemma diff_Suc_Suc [simp, code]: "Suc m - Suc n = m - n"
   by (induct n) (simp_all add: diff_Suc)
 
 instance
 proof
   fix n m q :: nat
   show "(n + m) + q = n + (m + q)" by (induct n) simp_all
   show "n + m = m + n" by (induct n) simp_all
   show "m + n - m = n" by (induct m) simp_all
   show "n - m - q = n - (m + q)" by (induct q) (simp_all add: diff_Suc)
   show "0 + n = n" by simp
   show "0 - n = 0" by simp
 qed
 
 end
 
 hide_fact (open) add_0 add_0_right diff_0
 
 instantiation nat :: comm_semiring_1_cancel
 begin
 
 definition One_nat_def [simp]: "1 = Suc 0"
 
 primrec times_nat
   where
     mult_0: "0 * n = (0::nat)"
   | mult_Suc: "Suc m * n = n + (m * n)"
 
 lemma mult_0_right [simp]: "m * 0 = 0"
   for m :: nat
   by (induct m) simp_all
 
 lemma mult_Suc_right [simp]: "m * Suc n = m + (m * n)"
   by (induct m) (simp_all add: add.left_commute)
 
 lemma add_mult_distrib: "(m + n) * k = (m * k) + (n * k)"
   for m n k :: nat
   by (induct m) (simp_all add: add.assoc)
 
 instance
 proof
   fix k n m q :: nat
   show "0 \<noteq> (1::nat)"
     by simp
   show "1 * n = n"
     by simp
   show "n * m = m * n"
     by (induct n) simp_all
   show "(n * m) * q = n * (m * q)"
     by (induct n) (simp_all add: add_mult_distrib)
   show "(n + m) * q = n * q + m * q"
     by (rule add_mult_distrib)
   show "k * (m - n) = (k * m) - (k * n)"
     by (induct m n rule: diff_induct) simp_all
 qed
 
 end
 
 
 subsubsection \<open>Addition\<close>
 
 text \<open>Reasoning about \<open>m + 0 = 0\<close>, etc.\<close>
 
 lemma add_is_0 [iff]: "m + n = 0 \<longleftrightarrow> m = 0 \<and> n = 0"
   for m n :: nat
   by (cases m) simp_all
 
 lemma add_is_1: "m + n = Suc 0 \<longleftrightarrow> m = Suc 0 \<and> n = 0 \<or> m = 0 \<and> n = Suc 0"
   by (cases m) simp_all
 
 lemma one_is_add: "Suc 0 = m + n \<longleftrightarrow> m = Suc 0 \<and> n = 0 \<or> m = 0 \<and> n = Suc 0"
   by (rule trans, rule eq_commute, rule add_is_1)
 
 lemma add_eq_self_zero: "m + n = m \<Longrightarrow> n = 0"
   for m n :: nat
   by (induct m) simp_all
 
 lemma plus_1_eq_Suc:
   "plus 1 = Suc"
   by (simp add: fun_eq_iff)
 
 lemma Suc_eq_plus1: "Suc n = n + 1"
   by simp
 
 lemma Suc_eq_plus1_left: "Suc n = 1 + n"
   by simp
 
 
 subsubsection \<open>Difference\<close>
 
 lemma Suc_diff_diff [simp]: "(Suc m - n) - Suc k = m - n - k"
   by (simp add: diff_diff_add)
 
 lemma diff_Suc_1 [simp]: "Suc n - 1 = n"
   by simp
 
 
 subsubsection \<open>Multiplication\<close>
 
 lemma mult_is_0 [simp]: "m * n = 0 \<longleftrightarrow> m = 0 \<or> n = 0" for m n :: nat
   by (induct m) auto
 
 lemma mult_eq_1_iff [simp]: "m * n = Suc 0 \<longleftrightarrow> m = Suc 0 \<and> n = Suc 0"
 proof (induct m)
   case 0
   then show ?case by simp
 next
   case (Suc m)
   then show ?case by (induct n) auto
 qed
 
 lemma one_eq_mult_iff [simp]: "Suc 0 = m * n \<longleftrightarrow> m = Suc 0 \<and> n = Suc 0"
   apply (rule trans)
    apply (rule_tac [2] mult_eq_1_iff)
   apply fastforce
   done
 
 lemma nat_mult_eq_1_iff [simp]: "m * n = 1 \<longleftrightarrow> m = 1 \<and> n = 1"
   for m n :: nat
   unfolding One_nat_def by (rule mult_eq_1_iff)
 
 lemma nat_1_eq_mult_iff [simp]: "1 = m * n \<longleftrightarrow> m = 1 \<and> n = 1"
   for m n :: nat
   unfolding One_nat_def by (rule one_eq_mult_iff)
 
 lemma mult_cancel1 [simp]: "k * m = k * n \<longleftrightarrow> m = n \<or> k = 0"
   for k m n :: nat
 proof -
   have "k \<noteq> 0 \<Longrightarrow> k * m = k * n \<Longrightarrow> m = n"
   proof (induct n arbitrary: m)
     case 0
     then show "m = 0" by simp
   next
     case (Suc n)
     then show "m = Suc n"
       by (cases m) (simp_all add: eq_commute [of 0])
   qed
   then show ?thesis by auto
 qed
 
 lemma mult_cancel2 [simp]: "m * k = n * k \<longleftrightarrow> m = n \<or> k = 0"
   for k m n :: nat
   by (simp add: mult.commute)
 
 lemma Suc_mult_cancel1: "Suc k * m = Suc k * n \<longleftrightarrow> m = n"
   by (subst mult_cancel1) simp
 
 
 subsection \<open>Orders on \<^typ>\<open>nat\<close>\<close>
 
 subsubsection \<open>Operation definition\<close>
 
 instantiation nat :: linorder
 begin
 
 primrec less_eq_nat
   where
     "(0::nat) \<le> n \<longleftrightarrow> True"
   | "Suc m \<le> n \<longleftrightarrow> (case n of 0 \<Rightarrow> False | Suc n \<Rightarrow> m \<le> n)"
 
 declare less_eq_nat.simps [simp del]
 
 lemma le0 [iff]: "0 \<le> n" for
   n :: nat
   by (simp add: less_eq_nat.simps)
 
 lemma [code]: "0 \<le> n \<longleftrightarrow> True"
   for n :: nat
   by simp
 
 definition less_nat
   where less_eq_Suc_le: "n < m \<longleftrightarrow> Suc n \<le> m"
 
 lemma Suc_le_mono [iff]: "Suc n \<le> Suc m \<longleftrightarrow> n \<le> m"
   by (simp add: less_eq_nat.simps(2))
 
 lemma Suc_le_eq [code]: "Suc m \<le> n \<longleftrightarrow> m < n"
   unfolding less_eq_Suc_le ..
 
 lemma le_0_eq [iff]: "n \<le> 0 \<longleftrightarrow> n = 0"
   for n :: nat
   by (induct n) (simp_all add: less_eq_nat.simps(2))
 
 lemma not_less0 [iff]: "\<not> n < 0"
   for n :: nat
   by (simp add: less_eq_Suc_le)
 
 lemma less_nat_zero_code [code]: "n < 0 \<longleftrightarrow> False"
   for n :: nat
   by simp
 
 lemma Suc_less_eq [iff]: "Suc m < Suc n \<longleftrightarrow> m < n"
   by (simp add: less_eq_Suc_le)
 
 lemma less_Suc_eq_le [code]: "m < Suc n \<longleftrightarrow> m \<le> n"
   by (simp add: less_eq_Suc_le)
 
 lemma Suc_less_eq2: "Suc n < m \<longleftrightarrow> (\<exists>m'. m = Suc m' \<and> n < m')"
   by (cases m) auto
 
 lemma le_SucI: "m \<le> n \<Longrightarrow> m \<le> Suc n"
   by (induct m arbitrary: n) (simp_all add: less_eq_nat.simps(2) split: nat.splits)
 
 lemma Suc_leD: "Suc m \<le> n \<Longrightarrow> m \<le> n"
   by (cases n) (auto intro: le_SucI)
 
 lemma less_SucI: "m < n \<Longrightarrow> m < Suc n"
   by (simp add: less_eq_Suc_le) (erule Suc_leD)
 
 lemma Suc_lessD: "Suc m < n \<Longrightarrow> m < n"
   by (simp add: less_eq_Suc_le) (erule Suc_leD)
 
 instance
 proof
   fix n m q :: nat
   show "n < m \<longleftrightarrow> n \<le> m \<and> \<not> m \<le> n"
   proof (induct n arbitrary: m)
     case 0
     then show ?case
       by (cases m) (simp_all add: less_eq_Suc_le)
   next
     case (Suc n)
     then show ?case
       by (cases m) (simp_all add: less_eq_Suc_le)
   qed
   show "n \<le> n"
     by (induct n) simp_all
   then show "n = m" if "n \<le> m" and "m \<le> n"
     using that by (induct n arbitrary: m)
       (simp_all add: less_eq_nat.simps(2) split: nat.splits)
   show "n \<le> q" if "n \<le> m" and "m \<le> q"
     using that
   proof (induct n arbitrary: m q)
     case 0
     show ?case by simp
   next
     case (Suc n)
     then show ?case
       by (simp_all (no_asm_use) add: less_eq_nat.simps(2) split: nat.splits, clarify,
         simp_all (no_asm_use) add: less_eq_nat.simps(2) split: nat.splits, clarify,
         simp_all (no_asm_use) add: less_eq_nat.simps(2) split: nat.splits)
   qed
   show "n \<le> m \<or> m \<le> n"
     by (induct n arbitrary: m)
       (simp_all add: less_eq_nat.simps(2) split: nat.splits)
 qed
 
 end
 
 instantiation nat :: order_bot
 begin
 
 definition bot_nat :: nat
   where "bot_nat = 0"
 
 instance
   by standard (simp add: bot_nat_def)
 
 end
 
 instance nat :: no_top
   by standard (auto intro: less_Suc_eq_le [THEN iffD2])
 
 
 subsubsection \<open>Introduction properties\<close>
 
 lemma lessI [iff]: "n < Suc n"
   by (simp add: less_Suc_eq_le)
 
 lemma zero_less_Suc [iff]: "0 < Suc n"
   by (simp add: less_Suc_eq_le)
 
 
 subsubsection \<open>Elimination properties\<close>
 
 lemma less_not_refl: "\<not> n < n"
   for n :: nat
   by (rule order_less_irrefl)
 
 lemma less_not_refl2: "n < m \<Longrightarrow> m \<noteq> n"
   for m n :: nat
   by (rule not_sym) (rule less_imp_neq)
 
 lemma less_not_refl3: "s < t \<Longrightarrow> s \<noteq> t"
   for s t :: nat
   by (rule less_imp_neq)
 
 lemma less_irrefl_nat: "n < n \<Longrightarrow> R"
   for n :: nat
   by (rule notE, rule less_not_refl)
 
 lemma less_zeroE: "n < 0 \<Longrightarrow> R"
   for n :: nat
   by (rule notE) (rule not_less0)
 
 lemma less_Suc_eq: "m < Suc n \<longleftrightarrow> m < n \<or> m = n"
   unfolding less_Suc_eq_le le_less ..
 
 lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
   by (simp add: less_Suc_eq)
 
 lemma less_one [iff]: "n < 1 \<longleftrightarrow> n = 0"
   for n :: nat
   unfolding One_nat_def by (rule less_Suc0)
 
 lemma Suc_mono: "m < n \<Longrightarrow> Suc m < Suc n"
   by simp
 
 text \<open>"Less than" is antisymmetric, sort of.\<close>
 lemma less_antisym: "\<not> n < m \<Longrightarrow> n < Suc m \<Longrightarrow> m = n"
   unfolding not_less less_Suc_eq_le by (rule antisym)
 
 lemma nat_neq_iff: "m \<noteq> n \<longleftrightarrow> m < n \<or> n < m"
   for m n :: nat
   by (rule linorder_neq_iff)
 
 
 subsubsection \<open>Inductive (?) properties\<close>
 
 lemma Suc_lessI: "m < n \<Longrightarrow> Suc m \<noteq> n \<Longrightarrow> Suc m < n"
   unfolding less_eq_Suc_le [of m] le_less by simp
 
 lemma lessE:
   assumes major: "i < k"
     and 1: "k = Suc i \<Longrightarrow> P"
     and 2: "\<And>j. i < j \<Longrightarrow> k = Suc j \<Longrightarrow> P"
   shows P
 proof -
   from major have "\<exists>j. i \<le> j \<and> k = Suc j"
     unfolding less_eq_Suc_le by (induct k) simp_all
   then have "(\<exists>j. i < j \<and> k = Suc j) \<or> k = Suc i"
     by (auto simp add: less_le)
   with 1 2 show P by auto
 qed
 
 lemma less_SucE:
   assumes major: "m < Suc n"
     and less: "m < n \<Longrightarrow> P"
     and eq: "m = n \<Longrightarrow> P"
   shows P
   apply (rule major [THEN lessE])
    apply (rule eq)
    apply blast
   apply (rule less)
   apply blast
   done
 
 lemma Suc_lessE:
   assumes major: "Suc i < k"
     and minor: "\<And>j. i < j \<Longrightarrow> k = Suc j \<Longrightarrow> P"
   shows P
   apply (rule major [THEN lessE])
    apply (erule lessI [THEN minor])
   apply (erule Suc_lessD [THEN minor])
   apply assumption
   done
 
 lemma Suc_less_SucD: "Suc m < Suc n \<Longrightarrow> m < n"
   by simp
 
 lemma less_trans_Suc:
   assumes le: "i < j"
   shows "j < k \<Longrightarrow> Suc i < k"
 proof (induct k)
   case 0
   then show ?case by simp
 next
   case (Suc k)
   with le show ?case
     by simp (auto simp add: less_Suc_eq dest: Suc_lessD)
 qed
 
 text \<open>Can be used with \<open>less_Suc_eq\<close> to get \<^prop>\<open>n = m \<or> n < m\<close>.\<close>
 lemma not_less_eq: "\<not> m < n \<longleftrightarrow> n < Suc m"
   by (simp only: not_less less_Suc_eq_le)
 
 lemma not_less_eq_eq: "\<not> m \<le> n \<longleftrightarrow> Suc n \<le> m"
   by (simp only: not_le Suc_le_eq)
 
 text \<open>Properties of "less than or equal".\<close>
 
 lemma le_imp_less_Suc: "m \<le> n \<Longrightarrow> m < Suc n"
   by (simp only: less_Suc_eq_le)
 
 lemma Suc_n_not_le_n: "\<not> Suc n \<le> n"
   by (simp add: not_le less_Suc_eq_le)
 
 lemma le_Suc_eq: "m \<le> Suc n \<longleftrightarrow> m \<le> n \<or> m = Suc n"
   by (simp add: less_Suc_eq_le [symmetric] less_Suc_eq)
 
 lemma le_SucE: "m \<le> Suc n \<Longrightarrow> (m \<le> n \<Longrightarrow> R) \<Longrightarrow> (m = Suc n \<Longrightarrow> R) \<Longrightarrow> R"
   by (drule le_Suc_eq [THEN iffD1], iprover+)
 
 lemma Suc_leI: "m < n \<Longrightarrow> Suc m \<le> n"
   by (simp only: Suc_le_eq)
 
 text \<open>Stronger version of \<open>Suc_leD\<close>.\<close>
 lemma Suc_le_lessD: "Suc m \<le> n \<Longrightarrow> m < n"
   by (simp only: Suc_le_eq)
 
 lemma less_imp_le_nat: "m < n \<Longrightarrow> m \<le> n" for m n :: nat
   unfolding less_eq_Suc_le by (rule Suc_leD)
 
 text \<open>For instance, \<open>(Suc m < Suc n) = (Suc m \<le> n) = (m < n)\<close>\<close>
 lemmas le_simps = less_imp_le_nat less_Suc_eq_le Suc_le_eq
 
 
 text \<open>Equivalence of \<open>m \<le> n\<close> and \<open>m < n \<or> m = n\<close>\<close>
 
 lemma less_or_eq_imp_le: "m < n \<or> m = n \<Longrightarrow> m \<le> n"
   for m n :: nat
   unfolding le_less .
 
 lemma le_eq_less_or_eq: "m \<le> n \<longleftrightarrow> m < n \<or> m = n"
   for m n :: nat
   by (rule le_less)
 
 text \<open>Useful with \<open>blast\<close>.\<close>
 lemma eq_imp_le: "m = n \<Longrightarrow> m \<le> n"
   for m n :: nat
   by auto
 
 lemma le_refl: "n \<le> n"
   for n :: nat
   by simp
 
 lemma le_trans: "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
   for i j k :: nat
   by (rule order_trans)
 
 lemma le_antisym: "m \<le> n \<Longrightarrow> n \<le> m \<Longrightarrow> m = n"
   for m n :: nat
   by (rule antisym)
 
 lemma nat_less_le: "m < n \<longleftrightarrow> m \<le> n \<and> m \<noteq> n"
   for m n :: nat
   by (rule less_le)
 
 lemma le_neq_implies_less: "m \<le> n \<Longrightarrow> m \<noteq> n \<Longrightarrow> m < n"
   for m n :: nat
   unfolding less_le ..
 
 lemma nat_le_linear: "m \<le> n \<or> n \<le> m"
   for m n :: nat
   by (rule linear)
 
 lemmas linorder_neqE_nat = linorder_neqE [where 'a = nat]
 
 lemma le_less_Suc_eq: "m \<le> n \<Longrightarrow> n < Suc m \<longleftrightarrow> n = m"
   unfolding less_Suc_eq_le by auto
 
 lemma not_less_less_Suc_eq: "\<not> n < m \<Longrightarrow> n < Suc m \<longleftrightarrow> n = m"
   unfolding not_less by (rule le_less_Suc_eq)
 
 lemmas not_less_simps = not_less_less_Suc_eq le_less_Suc_eq
 
 lemma not0_implies_Suc: "n \<noteq> 0 \<Longrightarrow> \<exists>m. n = Suc m"
   by (cases n) simp_all
 
 lemma gr0_implies_Suc: "n > 0 \<Longrightarrow> \<exists>m. n = Suc m"
   by (cases n) simp_all
 
 lemma gr_implies_not0: "m < n \<Longrightarrow> n \<noteq> 0"
   for m n :: nat
   by (cases n) simp_all
 
 lemma neq0_conv[iff]: "n \<noteq> 0 \<longleftrightarrow> 0 < n"
   for n :: nat
   by (cases n) simp_all
 
 text \<open>This theorem is useful with \<open>blast\<close>\<close>
 lemma gr0I: "(n = 0 \<Longrightarrow> False) \<Longrightarrow> 0 < n"
   for n :: nat
   by (rule neq0_conv[THEN iffD1]) iprover
 
 lemma gr0_conv_Suc: "0 < n \<longleftrightarrow> (\<exists>m. n = Suc m)"
   by (fast intro: not0_implies_Suc)
 
 lemma not_gr0 [iff]: "\<not> 0 < n \<longleftrightarrow> n = 0"
   for n :: nat
   using neq0_conv by blast
 
 lemma Suc_le_D: "Suc n \<le> m' \<Longrightarrow> \<exists>m. m' = Suc m"
   by (induct m') simp_all
 
 text \<open>Useful in certain inductive arguments\<close>
 lemma less_Suc_eq_0_disj: "m < Suc n \<longleftrightarrow> m = 0 \<or> (\<exists>j. m = Suc j \<and> j < n)"
   by (cases m) simp_all
 
 lemma All_less_Suc: "(\<forall>i < Suc n. P i) = (P n \<and> (\<forall>i < n. P i))"
   by (auto simp: less_Suc_eq)
 
 lemma All_less_Suc2: "(\<forall>i < Suc n. P i) = (P 0 \<and> (\<forall>i < n. P(Suc i)))"
   by (auto simp: less_Suc_eq_0_disj)
 
 lemma Ex_less_Suc: "(\<exists>i < Suc n. P i) = (P n \<or> (\<exists>i < n. P i))"
   by (auto simp: less_Suc_eq)
 
 lemma Ex_less_Suc2: "(\<exists>i < Suc n. P i) = (P 0 \<or> (\<exists>i < n. P(Suc i)))"
   by (auto simp: less_Suc_eq_0_disj)
 
 text \<open>@{term mono} (non-strict) doesn't imply increasing, as the function could be constant\<close>
 lemma strict_mono_imp_increasing:
   fixes n::nat
   assumes "strict_mono f" shows "f n \<ge> n"
 proof (induction n)
   case 0
   then show ?case
     by auto
 next
   case (Suc n)
   then show ?case
     unfolding not_less_eq_eq [symmetric]
     using Suc_n_not_le_n assms order_trans strict_mono_less_eq by blast
 qed
 
 subsubsection \<open>Monotonicity of Addition\<close>
 
 lemma Suc_pred [simp]: "n > 0 \<Longrightarrow> Suc (n - Suc 0) = n"
   by (simp add: diff_Suc split: nat.split)
 
 lemma Suc_diff_1 [simp]: "0 < n \<Longrightarrow> Suc (n - 1) = n"
   unfolding One_nat_def by (rule Suc_pred)
 
 lemma nat_add_left_cancel_le [simp]: "k + m \<le> k + n \<longleftrightarrow> m \<le> n"
   for k m n :: nat
   by (induct k) simp_all
 
 lemma nat_add_left_cancel_less [simp]: "k + m < k + n \<longleftrightarrow> m < n"
   for k m n :: nat
   by (induct k) simp_all
 
 lemma add_gr_0 [iff]: "m + n > 0 \<longleftrightarrow> m > 0 \<or> n > 0"
   for m n :: nat
   by (auto dest: gr0_implies_Suc)
 
 text \<open>strict, in 1st argument\<close>
 lemma add_less_mono1: "i < j \<Longrightarrow> i + k < j + k"
   for i j k :: nat
   by (induct k) simp_all
 
 text \<open>strict, in both arguments\<close>
 lemma add_less_mono: "i < j \<Longrightarrow> k < l \<Longrightarrow> i + k < j + l"
   for i j k l :: nat
   apply (rule add_less_mono1 [THEN less_trans], assumption+)
   apply (induct j)
    apply simp_all
   done
 
-text \<open>Deleted \<open>less_natE\<close>; use \<open>less_imp_Suc_add RS exE\<close>\<close>
 lemma less_imp_Suc_add: "m < n \<Longrightarrow> \<exists>k. n = Suc (m + k)"
 proof (induct n)
   case 0
   then show ?case by simp
 next
   case Suc
   then show ?case
     by (simp add: order_le_less)
       (blast elim!: less_SucE intro!: Nat.add_0_right [symmetric] add_Suc_right [symmetric])
 qed
 
 lemma le_Suc_ex: "k \<le> l \<Longrightarrow> (\<exists>n. l = k + n)"
   for k l :: nat
   by (auto simp: less_Suc_eq_le[symmetric] dest: less_imp_Suc_add)
 
+lemma less_natE:
+  assumes \<open>m < n\<close>
+  obtains q where \<open>n = Suc (m + q)\<close>
+  using assms by (auto dest: less_imp_Suc_add intro: that)
+
 text \<open>strict, in 1st argument; proof is by induction on \<open>k > 0\<close>\<close>
 lemma mult_less_mono2:
   fixes i j :: nat
   assumes "i < j" and "0 < k"
   shows "k * i < k * j"
   using \<open>0 < k\<close>
 proof (induct k)
   case 0
   then show ?case by simp
 next
   case (Suc k)
   with \<open>i < j\<close> show ?case
     by (cases k) (simp_all add: add_less_mono)
 qed
 
 text \<open>Addition is the inverse of subtraction:
   if \<^term>\<open>n \<le> m\<close> then \<^term>\<open>n + (m - n) = m\<close>.\<close>
 lemma add_diff_inverse_nat: "\<not> m < n \<Longrightarrow> n + (m - n) = m"
   for m n :: nat
   by (induct m n rule: diff_induct) simp_all
 
 lemma nat_le_iff_add: "m \<le> n \<longleftrightarrow> (\<exists>k. n = m + k)"
   for m n :: nat
   using nat_add_left_cancel_le[of m 0] by (auto dest: le_Suc_ex)
 
 text \<open>The naturals form an ordered \<open>semidom\<close> and a \<open>dioid\<close>.\<close>
 
 instance nat :: linordered_semidom
 proof
   fix m n q :: nat
   show "0 < (1::nat)"
     by simp
   show "m \<le> n \<Longrightarrow> q + m \<le> q + n"
     by simp
   show "m < n \<Longrightarrow> 0 < q \<Longrightarrow> q * m < q * n"
     by (simp add: mult_less_mono2)
   show "m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> m * n \<noteq> 0"
     by simp
   show "n \<le> m \<Longrightarrow> (m - n) + n = m"
     by (simp add: add_diff_inverse_nat add.commute linorder_not_less)
 qed
 
 instance nat :: dioid
   by standard (rule nat_le_iff_add)
 
 declare le0[simp del] \<comment> \<open>This is now @{thm zero_le}\<close>
 declare le_0_eq[simp del] \<comment> \<open>This is now @{thm le_zero_eq}\<close>
 declare not_less0[simp del] \<comment> \<open>This is now @{thm not_less_zero}\<close>
 declare not_gr0[simp del] \<comment> \<open>This is now @{thm not_gr_zero}\<close>
 
 instance nat :: ordered_cancel_comm_monoid_add ..
 instance nat :: ordered_cancel_comm_monoid_diff ..
 
 
 subsubsection \<open>\<^term>\<open>min\<close> and \<^term>\<open>max\<close>\<close>
 
 lemma mono_Suc: "mono Suc"
   by (rule monoI) simp
 
 lemma min_0L [simp]: "min 0 n = 0"
   for n :: nat
   by (rule min_absorb1) simp
 
 lemma min_0R [simp]: "min n 0 = 0"
   for n :: nat
   by (rule min_absorb2) simp
 
 lemma min_Suc_Suc [simp]: "min (Suc m) (Suc n) = Suc (min m n)"
   by (simp add: mono_Suc min_of_mono)
 
 lemma min_Suc1: "min (Suc n) m = (case m of 0 \<Rightarrow> 0 | Suc m' \<Rightarrow> Suc(min n m'))"
   by (simp split: nat.split)
 
 lemma min_Suc2: "min m (Suc n) = (case m of 0 \<Rightarrow> 0 | Suc m' \<Rightarrow> Suc(min m' n))"
   by (simp split: nat.split)
 
 lemma max_0L [simp]: "max 0 n = n"
   for n :: nat
   by (rule max_absorb2) simp
 
 lemma max_0R [simp]: "max n 0 = n"
   for n :: nat
   by (rule max_absorb1) simp
 
 lemma max_Suc_Suc [simp]: "max (Suc m) (Suc n) = Suc (max m n)"
   by (simp add: mono_Suc max_of_mono)
 
 lemma max_Suc1: "max (Suc n) m = (case m of 0 \<Rightarrow> Suc n | Suc m' \<Rightarrow> Suc (max n m'))"
   by (simp split: nat.split)
 
 lemma max_Suc2: "max m (Suc n) = (case m of 0 \<Rightarrow> Suc n | Suc m' \<Rightarrow> Suc (max m' n))"
   by (simp split: nat.split)
 
 lemma nat_mult_min_left: "min m n * q = min (m * q) (n * q)"
   for m n q :: nat
   by (simp add: min_def not_le)
     (auto dest: mult_right_le_imp_le mult_right_less_imp_less le_less_trans)
 
 lemma nat_mult_min_right: "m * min n q = min (m * n) (m * q)"
   for m n q :: nat
   by (simp add: min_def not_le)
     (auto dest: mult_left_le_imp_le mult_left_less_imp_less le_less_trans)
 
 lemma nat_add_max_left: "max m n + q = max (m + q) (n + q)"
   for m n q :: nat
   by (simp add: max_def)
 
 lemma nat_add_max_right: "m + max n q = max (m + n) (m + q)"
   for m n q :: nat
   by (simp add: max_def)
 
 lemma nat_mult_max_left: "max m n * q = max (m * q) (n * q)"
   for m n q :: nat
   by (simp add: max_def not_le)
     (auto dest: mult_right_le_imp_le mult_right_less_imp_less le_less_trans)
 
 lemma nat_mult_max_right: "m * max n q = max (m * n) (m * q)"
   for m n q :: nat
   by (simp add: max_def not_le)
     (auto dest: mult_left_le_imp_le mult_left_less_imp_less le_less_trans)
 
 
 subsubsection \<open>Additional theorems about \<^term>\<open>(\<le>)\<close>\<close>
 
 text \<open>Complete induction, aka course-of-values induction\<close>
 
 instance nat :: wellorder
 proof
   fix P and n :: nat
   assume step: "(\<And>m. m < n \<Longrightarrow> P m) \<Longrightarrow> P n" for n :: nat
   have "\<And>q. q \<le> n \<Longrightarrow> P q"
   proof (induct n)
     case (0 n)
     have "P 0" by (rule step) auto
     with 0 show ?case by auto
   next
     case (Suc m n)
     then have "n \<le> m \<or> n = Suc m"
       by (simp add: le_Suc_eq)
     then show ?case
     proof
       assume "n \<le> m"
       then show "P n" by (rule Suc(1))
     next
       assume n: "n = Suc m"
       show "P n" by (rule step) (rule Suc(1), simp add: n le_simps)
     qed
   qed
   then show "P n" by auto
 qed
 
 
 lemma Least_eq_0[simp]: "P 0 \<Longrightarrow> Least P = 0"
   for P :: "nat \<Rightarrow> bool"
   by (rule Least_equality[OF _ le0])
 
 lemma Least_Suc: "P n \<Longrightarrow> \<not> P 0 \<Longrightarrow> (LEAST n. P n) = Suc (LEAST m. P (Suc m))"
   apply (cases n)
    apply auto
   apply (frule LeastI)
   apply (drule_tac P = "\<lambda>x. P (Suc x)" in LeastI)
   apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))")
    apply (erule_tac [2] Least_le)
   apply (cases "LEAST x. P x")
    apply auto
   apply (drule_tac P = "\<lambda>x. P (Suc x)" in Least_le)
   apply (blast intro: order_antisym)
   done
 
 lemma Least_Suc2: "P n \<Longrightarrow> Q m \<Longrightarrow> \<not> P 0 \<Longrightarrow> \<forall>k. P (Suc k) = Q k \<Longrightarrow> Least P = Suc (Least Q)"
   by (erule (1) Least_Suc [THEN ssubst]) simp
 
 lemma ex_least_nat_le: "\<not> P 0 \<Longrightarrow> P n \<Longrightarrow> \<exists>k\<le>n. (\<forall>i<k. \<not> P i) \<and> P k"
   for P :: "nat \<Rightarrow> bool"
   apply (cases n)
    apply blast
   apply (rule_tac x="LEAST k. P k" in exI)
   apply (blast intro: Least_le dest: not_less_Least intro: LeastI_ex)
   done
 
 lemma ex_least_nat_less: "\<not> P 0 \<Longrightarrow> P n \<Longrightarrow> \<exists>k<n. (\<forall>i\<le>k. \<not> P i) \<and> P (k + 1)"
   for P :: "nat \<Rightarrow> bool"
   apply (cases n)
    apply blast
   apply (frule (1) ex_least_nat_le)
   apply (erule exE)
   apply (case_tac k)
    apply simp
   apply (rename_tac k1)
   apply (rule_tac x=k1 in exI)
   apply (auto simp add: less_eq_Suc_le)
   done
 
 lemma nat_less_induct:
   fixes P :: "nat \<Rightarrow> bool"
   assumes "\<And>n. \<forall>m. m < n \<longrightarrow> P m \<Longrightarrow> P n"
   shows "P n"
   using assms less_induct by blast
 
 lemma measure_induct_rule [case_names less]:
   fixes f :: "'a \<Rightarrow> 'b::wellorder"
   assumes step: "\<And>x. (\<And>y. f y < f x \<Longrightarrow> P y) \<Longrightarrow> P x"
   shows "P a"
   by (induct m \<equiv> "f a" arbitrary: a rule: less_induct) (auto intro: step)
 
 text \<open>old style induction rules:\<close>
 lemma measure_induct:
   fixes f :: "'a \<Rightarrow> 'b::wellorder"
   shows "(\<And>x. \<forall>y. f y < f x \<longrightarrow> P y \<Longrightarrow> P x) \<Longrightarrow> P a"
   by (rule measure_induct_rule [of f P a]) iprover
 
 lemma full_nat_induct:
   assumes step: "\<And>n. (\<forall>m. Suc m \<le> n \<longrightarrow> P m) \<Longrightarrow> P n"
   shows "P n"
   by (rule less_induct) (auto intro: step simp:le_simps)
 
 text\<open>An induction rule for establishing binary relations\<close>
 lemma less_Suc_induct [consumes 1]:
   assumes less: "i < j"
     and step: "\<And>i. P i (Suc i)"
     and trans: "\<And>i j k. i < j \<Longrightarrow> j < k \<Longrightarrow> P i j \<Longrightarrow> P j k \<Longrightarrow> P i k"
   shows "P i j"
 proof -
   from less obtain k where j: "j = Suc (i + k)"
     by (auto dest: less_imp_Suc_add)
   have "P i (Suc (i + k))"
   proof (induct k)
     case 0
     show ?case by (simp add: step)
   next
     case (Suc k)
     have "0 + i < Suc k + i" by (rule add_less_mono1) simp
     then have "i < Suc (i + k)" by (simp add: add.commute)
     from trans[OF this lessI Suc step]
     show ?case by simp
   qed
   then show "P i j" by (simp add: j)
 qed
 
 text \<open>
   The method of infinite descent, frequently used in number theory.
   Provided by Roelof Oosterhuis.
   \<open>P n\<close> is true for all natural numbers if
   \<^item> case ``0'': given \<open>n = 0\<close> prove \<open>P n\<close>
   \<^item> case ``smaller'': given \<open>n > 0\<close> and \<open>\<not> P n\<close> prove there exists
     a smaller natural number \<open>m\<close> such that \<open>\<not> P m\<close>.
 \<close>
 
 lemma infinite_descent: "(\<And>n. \<not> P n \<Longrightarrow> \<exists>m<n. \<not> P m) \<Longrightarrow> P n" for P :: "nat \<Rightarrow> bool"
   \<comment> \<open>compact version without explicit base case\<close>
   by (induct n rule: less_induct) auto
 
 lemma infinite_descent0 [case_names 0 smaller]:
   fixes P :: "nat \<Rightarrow> bool"
   assumes "P 0"
     and "\<And>n. n > 0 \<Longrightarrow> \<not> P n \<Longrightarrow> \<exists>m. m < n \<and> \<not> P m"
   shows "P n"
   apply (rule infinite_descent)
   using assms
   apply (case_tac "n > 0")
    apply auto
   done
 
 text \<open>
   Infinite descent using a mapping to \<open>nat\<close>:
   \<open>P x\<close> is true for all \<open>x \<in> D\<close> if there exists a \<open>V \<in> D \<Rightarrow> nat\<close> and
   \<^item> case ``0'': given \<open>V x = 0\<close> prove \<open>P x\<close>
   \<^item> ``smaller'': given \<open>V x > 0\<close> and \<open>\<not> P x\<close> prove
   there exists a \<open>y \<in> D\<close> such that \<open>V y < V x\<close> and \<open>\<not> P y\<close>.
 \<close>
 corollary infinite_descent0_measure [case_names 0 smaller]:
   fixes V :: "'a \<Rightarrow> nat"
   assumes 1: "\<And>x. V x = 0 \<Longrightarrow> P x"
     and 2: "\<And>x. V x > 0 \<Longrightarrow> \<not> P x \<Longrightarrow> \<exists>y. V y < V x \<and> \<not> P y"
   shows "P x"
 proof -
   obtain n where "n = V x" by auto
   moreover have "\<And>x. V x = n \<Longrightarrow> P x"
   proof (induct n rule: infinite_descent0)
     case 0
     with 1 show "P x" by auto
   next
     case (smaller n)
     then obtain x where *: "V x = n " and "V x > 0 \<and> \<not> P x" by auto
     with 2 obtain y where "V y < V x \<and> \<not> P y" by auto
     with * obtain m where "m = V y \<and> m < n \<and> \<not> P y" by auto
     then show ?case by auto
   qed
   ultimately show "P x" by auto
 qed
 
 text \<open>Again, without explicit base case:\<close>
 lemma infinite_descent_measure:
   fixes V :: "'a \<Rightarrow> nat"
   assumes "\<And>x. \<not> P x \<Longrightarrow> \<exists>y. V y < V x \<and> \<not> P y"
   shows "P x"
 proof -
   from assms obtain n where "n = V x" by auto
   moreover have "\<And>x. V x = n \<Longrightarrow> P x"
   proof (induct n rule: infinite_descent, auto)
     show "\<exists>m < V x. \<exists>y. V y = m \<and> \<not> P y" if "\<not> P x" for x
       using assms and that by auto
   qed
   ultimately show "P x" by auto
 qed
 
 text \<open>A (clumsy) way of lifting \<open><\<close> monotonicity to \<open>\<le>\<close> monotonicity\<close>
 lemma less_mono_imp_le_mono:
   fixes f :: "nat \<Rightarrow> nat"
     and i j :: nat
   assumes "\<And>i j::nat. i < j \<Longrightarrow> f i < f j"
     and "i \<le> j"
   shows "f i \<le> f j"
   using assms by (auto simp add: order_le_less)
 
 
 text \<open>non-strict, in 1st argument\<close>
 lemma add_le_mono1: "i \<le> j \<Longrightarrow> i + k \<le> j + k"
   for i j k :: nat
   by (rule add_right_mono)
 
 text \<open>non-strict, in both arguments\<close>
 lemma add_le_mono: "i \<le> j \<Longrightarrow> k \<le> l \<Longrightarrow> i + k \<le> j + l"
   for i j k l :: nat
   by (rule add_mono)
 
 lemma le_add2: "n \<le> m + n"
   for m n :: nat
   by simp
 
 lemma le_add1: "n \<le> n + m"
   for m n :: nat
   by simp
 
 lemma less_add_Suc1: "i < Suc (i + m)"
   by (rule le_less_trans, rule le_add1, rule lessI)
 
 lemma less_add_Suc2: "i < Suc (m + i)"
   by (rule le_less_trans, rule le_add2, rule lessI)
 
 lemma less_iff_Suc_add: "m < n \<longleftrightarrow> (\<exists>k. n = Suc (m + k))"
   by (iprover intro!: less_add_Suc1 less_imp_Suc_add)
 
 lemma trans_le_add1: "i \<le> j \<Longrightarrow> i \<le> j + m"
   for i j m :: nat
   by (rule le_trans, assumption, rule le_add1)
 
 lemma trans_le_add2: "i \<le> j \<Longrightarrow> i \<le> m + j"
   for i j m :: nat
   by (rule le_trans, assumption, rule le_add2)
 
 lemma trans_less_add1: "i < j \<Longrightarrow> i < j + m"
   for i j m :: nat
   by (rule less_le_trans, assumption, rule le_add1)
 
 lemma trans_less_add2: "i < j \<Longrightarrow> i < m + j"
   for i j m :: nat
   by (rule less_le_trans, assumption, rule le_add2)
 
 lemma add_lessD1: "i + j < k \<Longrightarrow> i < k"
   for i j k :: nat
   by (rule le_less_trans [of _ "i+j"]) (simp_all add: le_add1)
 
 lemma not_add_less1 [iff]: "\<not> i + j < i"
   for i j :: nat
   apply (rule notI)
   apply (drule add_lessD1)
   apply (erule less_irrefl [THEN notE])
   done
 
 lemma not_add_less2 [iff]: "\<not> j + i < i"
   for i j :: nat
   by (simp add: add.commute)
 
 lemma add_leD1: "m + k \<le> n \<Longrightarrow> m \<le> n"
   for k m n :: nat
   by (rule order_trans [of _ "m + k"]) (simp_all add: le_add1)
 
 lemma add_leD2: "m + k \<le> n \<Longrightarrow> k \<le> n"
   for k m n :: nat
   apply (simp add: add.commute)
   apply (erule add_leD1)
   done
 
 lemma add_leE: "m + k \<le> n \<Longrightarrow> (m \<le> n \<Longrightarrow> k \<le> n \<Longrightarrow> R) \<Longrightarrow> R"
   for k m n :: nat
   by (blast dest: add_leD1 add_leD2)
 
 text \<open>needs \<open>\<And>k\<close> for \<open>ac_simps\<close> to work\<close>
 lemma less_add_eq_less: "\<And>k. k < l \<Longrightarrow> m + l = k + n \<Longrightarrow> m < n"
   for l m n :: nat
   by (force simp del: add_Suc_right simp add: less_iff_Suc_add add_Suc_right [symmetric] ac_simps)
 
 
 subsubsection \<open>More results about difference\<close>
 
 lemma Suc_diff_le: "n \<le> m \<Longrightarrow> Suc m - n = Suc (m - n)"
   by (induct m n rule: diff_induct) simp_all
 
 lemma diff_less_Suc: "m - n < Suc m"
   apply (induct m n rule: diff_induct)
     apply (erule_tac [3] less_SucE)
      apply (simp_all add: less_Suc_eq)
   done
 
 lemma diff_le_self [simp]: "m - n \<le> m"
   for m n :: nat
   by (induct m n rule: diff_induct) (simp_all add: le_SucI)
 
 lemma less_imp_diff_less: "j < k \<Longrightarrow> j - n < k"
   for j k n :: nat
   by (rule le_less_trans, rule diff_le_self)
 
 lemma diff_Suc_less [simp]: "0 < n \<Longrightarrow> n - Suc i < n"
   by (cases n) (auto simp add: le_simps)
 
 lemma diff_add_assoc: "k \<le> j \<Longrightarrow> (i + j) - k = i + (j - k)"
   for i j k :: nat
   by (fact ordered_cancel_comm_monoid_diff_class.diff_add_assoc) 
 
 lemma add_diff_assoc [simp]: "k \<le> j \<Longrightarrow> i + (j - k) = i + j - k"
   for i j k :: nat
   by (fact ordered_cancel_comm_monoid_diff_class.add_diff_assoc)
 
 lemma diff_add_assoc2: "k \<le> j \<Longrightarrow> (j + i) - k = (j - k) + i"
   for i j k :: nat
   by (fact ordered_cancel_comm_monoid_diff_class.diff_add_assoc2)
 
 lemma add_diff_assoc2 [simp]: "k \<le> j \<Longrightarrow> j - k + i = j + i - k"
   for i j k :: nat
   by (fact ordered_cancel_comm_monoid_diff_class.add_diff_assoc2)
 
 lemma le_imp_diff_is_add: "i \<le> j \<Longrightarrow> (j - i = k) = (j = k + i)"
   for i j k :: nat
   by auto
 
 lemma diff_is_0_eq [simp]: "m - n = 0 \<longleftrightarrow> m \<le> n"
   for m n :: nat
   by (induct m n rule: diff_induct) simp_all
 
 lemma diff_is_0_eq' [simp]: "m \<le> n \<Longrightarrow> m - n = 0"
   for m n :: nat
   by (rule iffD2, rule diff_is_0_eq)
 
 lemma zero_less_diff [simp]: "0 < n - m \<longleftrightarrow> m < n"
   for m n :: nat
   by (induct m n rule: diff_induct) simp_all
 
 lemma less_imp_add_positive:
   assumes "i < j"
   shows "\<exists>k::nat. 0 < k \<and> i + k = j"
 proof
   from assms show "0 < j - i \<and> i + (j - i) = j"
     by (simp add: order_less_imp_le)
 qed
 
 text \<open>a nice rewrite for bounded subtraction\<close>
 lemma nat_minus_add_max: "n - m + m = max n m"
   for m n :: nat
   by (simp add: max_def not_le order_less_imp_le)
 
 lemma nat_diff_split: "P (a - b) \<longleftrightarrow> (a < b \<longrightarrow> P 0) \<and> (\<forall>d. a = b + d \<longrightarrow> P d)"
   for a b :: nat
   \<comment> \<open>elimination of \<open>-\<close> on \<open>nat\<close>\<close>
   by (cases "a < b") (auto simp add: not_less le_less dest!: add_eq_self_zero [OF sym])
 
 lemma nat_diff_split_asm: "P (a - b) \<longleftrightarrow> \<not> (a < b \<and> \<not> P 0 \<or> (\<exists>d. a = b + d \<and> \<not> P d))"
   for a b :: nat
   \<comment> \<open>elimination of \<open>-\<close> on \<open>nat\<close> in assumptions\<close>
   by (auto split: nat_diff_split)
 
 lemma Suc_pred': "0 < n \<Longrightarrow> n = Suc(n - 1)"
   by simp
 
 lemma add_eq_if: "m + n = (if m = 0 then n else Suc ((m - 1) + n))"
   unfolding One_nat_def by (cases m) simp_all
 
 lemma mult_eq_if: "m * n = (if m = 0 then 0 else n + ((m - 1) * n))"
   for m n :: nat
   by (cases m) simp_all
 
 lemma Suc_diff_eq_diff_pred: "0 < n \<Longrightarrow> Suc m - n = m - (n - 1)"
   by (cases n) simp_all
 
 lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
   by (cases m) simp_all
 
 lemma Let_Suc [simp]: "Let (Suc n) f \<equiv> f (Suc n)"
   by (fact Let_def)
 
 
 subsubsection \<open>Monotonicity of multiplication\<close>
 
 lemma mult_le_mono1: "i \<le> j \<Longrightarrow> i * k \<le> j * k"
   for i j k :: nat
   by (simp add: mult_right_mono)
 
 lemma mult_le_mono2: "i \<le> j \<Longrightarrow> k * i \<le> k * j"
   for i j k :: nat
   by (simp add: mult_left_mono)
 
 text \<open>\<open>\<le>\<close> monotonicity, BOTH arguments\<close>
 lemma mult_le_mono: "i \<le> j \<Longrightarrow> k \<le> l \<Longrightarrow> i * k \<le> j * l"
   for i j k l :: nat
   by (simp add: mult_mono)
 
 lemma mult_less_mono1: "i < j \<Longrightarrow> 0 < k \<Longrightarrow> i * k < j * k"
   for i j k :: nat
   by (simp add: mult_strict_right_mono)
 
 text \<open>Differs from the standard \<open>zero_less_mult_iff\<close> in that there are no negative numbers.\<close>
 lemma nat_0_less_mult_iff [simp]: "0 < m * n \<longleftrightarrow> 0 < m \<and> 0 < n"
   for m n :: nat
 proof (induct m)
   case 0
   then show ?case by simp
 next
   case (Suc m)
   then show ?case by (cases n) simp_all
 qed
 
 lemma one_le_mult_iff [simp]: "Suc 0 \<le> m * n \<longleftrightarrow> Suc 0 \<le> m \<and> Suc 0 \<le> n"
 proof (induct m)
   case 0
   then show ?case by simp
 next
   case (Suc m)
   then show ?case by (cases n) simp_all
 qed
 
 lemma mult_less_cancel2 [simp]: "m * k < n * k \<longleftrightarrow> 0 < k \<and> m < n"
   for k m n :: nat
   apply (safe intro!: mult_less_mono1)
    apply (cases k)
     apply auto
   apply (simp add: linorder_not_le [symmetric])
   apply (blast intro: mult_le_mono1)
   done
 
 lemma mult_less_cancel1 [simp]: "k * m < k * n \<longleftrightarrow> 0 < k \<and> m < n"
   for k m n :: nat
   by (simp add: mult.commute [of k])
 
 lemma mult_le_cancel1 [simp]: "k * m \<le> k * n \<longleftrightarrow> (0 < k \<longrightarrow> m \<le> n)"
   for k m n :: nat
   by (simp add: linorder_not_less [symmetric], auto)
 
 lemma mult_le_cancel2 [simp]: "m * k \<le> n * k \<longleftrightarrow> (0 < k \<longrightarrow> m \<le> n)"
   for k m n :: nat
   by (simp add: linorder_not_less [symmetric], auto)
 
 lemma Suc_mult_less_cancel1: "Suc k * m < Suc k * n \<longleftrightarrow> m < n"
   by (subst mult_less_cancel1) simp
 
 lemma Suc_mult_le_cancel1: "Suc k * m \<le> Suc k * n \<longleftrightarrow> m \<le> n"
   by (subst mult_le_cancel1) simp
 
 lemma le_square: "m \<le> m * m"
   for m :: nat
   by (cases m) (auto intro: le_add1)
 
 lemma le_cube: "m \<le> m * (m * m)"
   for m :: nat
   by (cases m) (auto intro: le_add1)
 
 text \<open>Lemma for \<open>gcd\<close>\<close>
 lemma mult_eq_self_implies_10: "m = m * n \<Longrightarrow> n = 1 \<or> m = 0"
   for m n :: nat
   apply (drule sym)
   apply (rule disjCI)
   apply (rule linorder_cases)
     defer
     apply assumption
    apply (drule mult_less_mono2)
     apply auto
   done
 
 lemma mono_times_nat:
   fixes n :: nat
   assumes "n > 0"
   shows "mono (times n)"
 proof
   fix m q :: nat
   assume "m \<le> q"
   with assms show "n * m \<le> n * q" by simp
 qed
 
 text \<open>The lattice order on \<^typ>\<open>nat\<close>.\<close>
 
 instantiation nat :: distrib_lattice
 begin
 
 definition "(inf :: nat \<Rightarrow> nat \<Rightarrow> nat) = min"
 
 definition "(sup :: nat \<Rightarrow> nat \<Rightarrow> nat) = max"
 
 instance
   by intro_classes
     (auto simp add: inf_nat_def sup_nat_def max_def not_le min_def
       intro: order_less_imp_le antisym elim!: order_trans order_less_trans)
 
 end
 
 
 subsection \<open>Natural operation of natural numbers on functions\<close>
 
 text \<open>
   We use the same logical constant for the power operations on
   functions and relations, in order to share the same syntax.
 \<close>
 
 consts compow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
 
 abbreviation compower :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "^^" 80)
   where "f ^^ n \<equiv> compow n f"
 
 notation (latex output)
   compower ("(_\<^bsup>_\<^esup>)" [1000] 1000)
 
 text \<open>\<open>f ^^ n = f \<circ> \<dots> \<circ> f\<close>, the \<open>n\<close>-fold composition of \<open>f\<close>\<close>
 
 overloading
   funpow \<equiv> "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)"
 begin
 
 primrec funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
   where
     "funpow 0 f = id"
   | "funpow (Suc n) f = f \<circ> funpow n f"
 
 end
 
 lemma funpow_0 [simp]: "(f ^^ 0) x = x"
   by simp
 
 lemma funpow_Suc_right: "f ^^ Suc n = f ^^ n \<circ> f"
 proof (induct n)
   case 0
   then show ?case by simp
 next
   fix n
   assume "f ^^ Suc n = f ^^ n \<circ> f"
   then show "f ^^ Suc (Suc n) = f ^^ Suc n \<circ> f"
     by (simp add: o_assoc)
 qed
 
 lemmas funpow_simps_right = funpow.simps(1) funpow_Suc_right
 
 text \<open>For code generation.\<close>
 
 definition funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
   where funpow_code_def [code_abbrev]: "funpow = compow"
 
 lemma [code]:
   "funpow (Suc n) f = f \<circ> funpow n f"
   "funpow 0 f = id"
   by (simp_all add: funpow_code_def)
 
 hide_const (open) funpow
 
 lemma funpow_add: "f ^^ (m + n) = f ^^ m \<circ> f ^^ n"
   by (induct m) simp_all
 
 lemma funpow_mult: "(f ^^ m) ^^ n = f ^^ (m * n)"
   for f :: "'a \<Rightarrow> 'a"
   by (induct n) (simp_all add: funpow_add)
 
 lemma funpow_swap1: "f ((f ^^ n) x) = (f ^^ n) (f x)"
 proof -
   have "f ((f ^^ n) x) = (f ^^ (n + 1)) x" by simp
   also have "\<dots>  = (f ^^ n \<circ> f ^^ 1) x" by (simp only: funpow_add)
   also have "\<dots> = (f ^^ n) (f x)" by simp
   finally show ?thesis .
 qed
 
 lemma comp_funpow: "comp f ^^ n = comp (f ^^ n)"
   for f :: "'a \<Rightarrow> 'a"
   by (induct n) simp_all
 
 lemma Suc_funpow[simp]: "Suc ^^ n = ((+) n)"
   by (induct n) simp_all
 
 lemma id_funpow[simp]: "id ^^ n = id"
   by (induct n) simp_all
 
 lemma funpow_mono: "mono f \<Longrightarrow> A \<le> B \<Longrightarrow> (f ^^ n) A \<le> (f ^^ n) B"
   for f :: "'a \<Rightarrow> ('a::order)"
   by (induct n arbitrary: A B)
      (auto simp del: funpow.simps(2) simp add: funpow_Suc_right mono_def)
 
 lemma funpow_mono2:
   assumes "mono f"
     and "i \<le> j"
     and "x \<le> y"
     and "x \<le> f x"
   shows "(f ^^ i) x \<le> (f ^^ j) y"
   using assms(2,3)
 proof (induct j arbitrary: y)
   case 0
   then show ?case by simp
 next
   case (Suc j)
   show ?case
   proof(cases "i = Suc j")
     case True
     with assms(1) Suc show ?thesis
       by (simp del: funpow.simps add: funpow_simps_right monoD funpow_mono)
   next
     case False
     with assms(1,4) Suc show ?thesis
       by (simp del: funpow.simps add: funpow_simps_right le_eq_less_or_eq less_Suc_eq_le)
         (simp add: Suc.hyps monoD order_subst1)
   qed
 qed
 
 lemma inj_fn[simp]:
   fixes f::"'a \<Rightarrow> 'a"
   assumes "inj f"
   shows "inj (f^^n)"
 proof (induction n)
   case Suc thus ?case using inj_compose[OF assms Suc.IH] by (simp del: comp_apply)
 qed simp
 
 lemma surj_fn[simp]:
   fixes f::"'a \<Rightarrow> 'a"
   assumes "surj f"
   shows "surj (f^^n)"
 proof (induction n)
   case Suc thus ?case by (simp add: comp_surj[OF Suc.IH assms] del: comp_apply)
 qed simp
 
 lemma bij_fn[simp]:
   fixes f::"'a \<Rightarrow> 'a"
   assumes "bij f"
   shows "bij (f^^n)"
 by (rule bijI[OF inj_fn[OF bij_is_inj[OF assms]] surj_fn[OF bij_is_surj[OF assms]]])
 
 
 subsection \<open>Kleene iteration\<close>
 
 lemma Kleene_iter_lpfp:
   fixes f :: "'a::order_bot \<Rightarrow> 'a"
   assumes "mono f"
     and "f p \<le> p"
   shows "(f ^^ k) bot \<le> p"
 proof (induct k)
   case 0
   show ?case by simp
 next
   case Suc
   show ?case
     using monoD[OF assms(1) Suc] assms(2) by simp
 qed
 
 lemma lfp_Kleene_iter:
   assumes "mono f"
     and "(f ^^ Suc k) bot = (f ^^ k) bot"
   shows "lfp f = (f ^^ k) bot"
 proof (rule antisym)
   show "lfp f \<le> (f ^^ k) bot"
   proof (rule lfp_lowerbound)
     show "f ((f ^^ k) bot) \<le> (f ^^ k) bot"
       using assms(2) by simp
   qed
   show "(f ^^ k) bot \<le> lfp f"
     using Kleene_iter_lpfp[OF assms(1)] lfp_unfold[OF assms(1)] by simp
 qed
 
 lemma mono_pow: "mono f \<Longrightarrow> mono (f ^^ n)"
   for f :: "'a \<Rightarrow> 'a::complete_lattice"
   by (induct n) (auto simp: mono_def)
 
 lemma lfp_funpow:
   assumes f: "mono f"
   shows "lfp (f ^^ Suc n) = lfp f"
 proof (rule antisym)
   show "lfp f \<le> lfp (f ^^ Suc n)"
   proof (rule lfp_lowerbound)
     have "f (lfp (f ^^ Suc n)) = lfp (\<lambda>x. f ((f ^^ n) x))"
       unfolding funpow_Suc_right by (simp add: lfp_rolling f mono_pow comp_def)
     then show "f (lfp (f ^^ Suc n)) \<le> lfp (f ^^ Suc n)"
       by (simp add: comp_def)
   qed
   have "(f ^^ n) (lfp f) = lfp f" for n
     by (induct n) (auto intro: f lfp_fixpoint)
   then show "lfp (f ^^ Suc n) \<le> lfp f"
     by (intro lfp_lowerbound) (simp del: funpow.simps)
 qed
 
 lemma gfp_funpow:
   assumes f: "mono f"
   shows "gfp (f ^^ Suc n) = gfp f"
 proof (rule antisym)
   show "gfp f \<ge> gfp (f ^^ Suc n)"
   proof (rule gfp_upperbound)
     have "f (gfp (f ^^ Suc n)) = gfp (\<lambda>x. f ((f ^^ n) x))"
       unfolding funpow_Suc_right by (simp add: gfp_rolling f mono_pow comp_def)
     then show "f (gfp (f ^^ Suc n)) \<ge> gfp (f ^^ Suc n)"
       by (simp add: comp_def)
   qed
   have "(f ^^ n) (gfp f) = gfp f" for n
     by (induct n) (auto intro: f gfp_fixpoint)
   then show "gfp (f ^^ Suc n) \<ge> gfp f"
     by (intro gfp_upperbound) (simp del: funpow.simps)
 qed
 
 lemma Kleene_iter_gpfp:
   fixes f :: "'a::order_top \<Rightarrow> 'a"
   assumes "mono f"
     and "p \<le> f p"
   shows "p \<le> (f ^^ k) top"
 proof (induct k)
   case 0
   show ?case by simp
 next
   case Suc
   show ?case
     using monoD[OF assms(1) Suc] assms(2) by simp
 qed
 
 lemma gfp_Kleene_iter:
   assumes "mono f"
     and "(f ^^ Suc k) top = (f ^^ k) top"
   shows "gfp f = (f ^^ k) top"
     (is "?lhs = ?rhs")
 proof (rule antisym)
   have "?rhs \<le> f ?rhs"
     using assms(2) by simp
   then show "?rhs \<le> ?lhs"
     by (rule gfp_upperbound)
   show "?lhs \<le> ?rhs"
     using Kleene_iter_gpfp[OF assms(1)] gfp_unfold[OF assms(1)] by simp
 qed
 
 
 subsection \<open>Embedding of the naturals into any \<open>semiring_1\<close>: \<^term>\<open>of_nat\<close>\<close>
 
 context semiring_1
 begin
 
 definition of_nat :: "nat \<Rightarrow> 'a"
   where "of_nat n = (plus 1 ^^ n) 0"
 
 lemma of_nat_simps [simp]:
   shows of_nat_0: "of_nat 0 = 0"
     and of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
   by (simp_all add: of_nat_def)
 
 lemma of_nat_1 [simp]: "of_nat 1 = 1"
   by (simp add: of_nat_def)
 
 lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n"
   by (induct m) (simp_all add: ac_simps)
 
 lemma of_nat_mult [simp]: "of_nat (m * n) = of_nat m * of_nat n"
   by (induct m) (simp_all add: ac_simps distrib_right)
 
 lemma mult_of_nat_commute: "of_nat x * y = y * of_nat x"
   by (induct x) (simp_all add: algebra_simps)
 
 primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"
   where
     "of_nat_aux inc 0 i = i"
   | "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" \<comment> \<open>tail recursive\<close>
 
 lemma of_nat_code: "of_nat n = of_nat_aux (\<lambda>i. i + 1) n 0"
 proof (induct n)
   case 0
   then show ?case by simp
 next
   case (Suc n)
   have "\<And>i. of_nat_aux (\<lambda>i. i + 1) n (i + 1) = of_nat_aux (\<lambda>i. i + 1) n i + 1"
     by (induct n) simp_all
   from this [of 0] have "of_nat_aux (\<lambda>i. i + 1) n 1 = of_nat_aux (\<lambda>i. i + 1) n 0 + 1"
     by simp
   with Suc show ?case
     by (simp add: add.commute)
 qed
 
 lemma of_nat_of_bool [simp]:
   "of_nat (of_bool P) = of_bool P"
   by auto
 
 end
 
 declare of_nat_code [code]
 
 context semiring_1_cancel
 begin
 
 lemma of_nat_diff:
   \<open>of_nat (m - n) = of_nat m - of_nat n\<close> if \<open>n \<le> m\<close>
 proof -
   from that obtain q where \<open>m = n + q\<close>
     by (blast dest: le_Suc_ex)
   then show ?thesis
     by simp
 qed
 
 end
 
 text \<open>Class for unital semirings with characteristic zero.
  Includes non-ordered rings like the complex numbers.\<close>
 
 class semiring_char_0 = semiring_1 +
   assumes inj_of_nat: "inj of_nat"
 begin
 
 lemma of_nat_eq_iff [simp]: "of_nat m = of_nat n \<longleftrightarrow> m = n"
   by (auto intro: inj_of_nat injD)
 
 text \<open>Special cases where either operand is zero\<close>
 
 lemma of_nat_0_eq_iff [simp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
   by (fact of_nat_eq_iff [of 0 n, unfolded of_nat_0])
 
 lemma of_nat_eq_0_iff [simp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
   by (fact of_nat_eq_iff [of m 0, unfolded of_nat_0])
 
 lemma of_nat_1_eq_iff [simp]: "1 = of_nat n \<longleftrightarrow> n=1"
   using of_nat_eq_iff by fastforce
 
 lemma of_nat_eq_1_iff [simp]: "of_nat n = 1 \<longleftrightarrow> n=1"
   using of_nat_eq_iff by fastforce
 
 lemma of_nat_neq_0 [simp]: "of_nat (Suc n) \<noteq> 0"
   unfolding of_nat_eq_0_iff by simp
 
 lemma of_nat_0_neq [simp]: "0 \<noteq> of_nat (Suc n)"
   unfolding of_nat_0_eq_iff by simp
 
 end
 
 class ring_char_0 = ring_1 + semiring_char_0
 
 context linordered_nonzero_semiring
 begin
 
 lemma of_nat_0_le_iff [simp]: "0 \<le> of_nat n"
   by (induct n) simp_all
 
 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"
 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])
 
 lemma less_imp_of_nat_less: "m < n \<Longrightarrow> of_nat m < of_nat n"
   by simp
 
 lemma of_nat_less_imp_less: "of_nat m < of_nat n \<Longrightarrow> m < n"
   by simp
 
 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)
 
 text \<open>Special cases where either operand is zero\<close>
 
 lemma of_nat_le_0_iff [simp]: "of_nat m \<le> 0 \<longleftrightarrow> m = 0"
   by (rule of_nat_le_iff [of _ 0, simplified])
 
 lemma of_nat_0_less_iff [simp]: "0 < of_nat n \<longleftrightarrow> 0 < n"
   by (rule of_nat_less_iff [of 0, simplified])
 
 end
 
 context linordered_nonzero_semiring
 begin
 
 lemma of_nat_max: "of_nat (max x y) = max (of_nat x) (of_nat y)"
   by (auto simp: max_def ord_class.max_def)
 
 lemma of_nat_min: "of_nat (min x y) = min (of_nat x) (of_nat y)"
   by (auto simp: min_def ord_class.min_def)
 
 end
 
 context linordered_semidom
 begin
 
 subclass linordered_nonzero_semiring ..
 
 subclass semiring_char_0 ..
 
 end
 
 context linordered_idom
 begin
 
 lemma abs_of_nat [simp]:
   "\<bar>of_nat n\<bar> = of_nat n"
   by (simp add: abs_if)
 
 lemma sgn_of_nat [simp]:
   "sgn (of_nat n) = of_bool (n > 0)"
   by simp
 
 end
 
 lemma of_nat_id [simp]: "of_nat n = n"
   by (induct n) simp_all
 
 lemma of_nat_eq_id [simp]: "of_nat = id"
   by (auto simp add: fun_eq_iff)
 
 
 subsection \<open>The set of natural numbers\<close>
 
 context semiring_1
 begin
 
 definition Nats :: "'a set"  ("\<nat>")
   where "\<nat> = range of_nat"
 
 lemma of_nat_in_Nats [simp]: "of_nat n \<in> \<nat>"
   by (simp add: Nats_def)
 
 lemma Nats_0 [simp]: "0 \<in> \<nat>"
   apply (simp add: Nats_def)
   apply (rule range_eqI)
   apply (rule of_nat_0 [symmetric])
   done
 
 lemma Nats_1 [simp]: "1 \<in> \<nat>"
   apply (simp add: Nats_def)
   apply (rule range_eqI)
   apply (rule of_nat_1 [symmetric])
   done
 
 lemma Nats_add [simp]: "a \<in> \<nat> \<Longrightarrow> b \<in> \<nat> \<Longrightarrow> a + b \<in> \<nat>"
   apply (auto simp add: Nats_def)
   apply (rule range_eqI)
   apply (rule of_nat_add [symmetric])
   done
 
 lemma Nats_mult [simp]: "a \<in> \<nat> \<Longrightarrow> b \<in> \<nat> \<Longrightarrow> a * b \<in> \<nat>"
   apply (auto simp add: Nats_def)
   apply (rule range_eqI)
   apply (rule of_nat_mult [symmetric])
   done
 
 lemma Nats_cases [cases set: Nats]:
   assumes "x \<in> \<nat>"
   obtains (of_nat) n where "x = of_nat n"
   unfolding Nats_def
 proof -
   from \<open>x \<in> \<nat>\<close> have "x \<in> range of_nat" unfolding Nats_def .
   then obtain n where "x = of_nat n" ..
   then show thesis ..
 qed
 
 lemma Nats_induct [case_names of_nat, induct set: Nats]: "x \<in> \<nat> \<Longrightarrow> (\<And>n. P (of_nat n)) \<Longrightarrow> P x"
   by (rule Nats_cases) auto
 
 end
 
 lemma Nats_diff [simp]:
   fixes a:: "'a::linordered_idom"
   assumes "a \<in> \<nat>" "b \<in> \<nat>" "b \<le> a" shows "a - b \<in> \<nat>"
 proof -
   obtain i where i: "a = of_nat i"
     using Nats_cases assms by blast
   obtain j where j: "b = of_nat j"
     using Nats_cases assms by blast
   have "j \<le> i"
     using \<open>b \<le> a\<close> i j of_nat_le_iff by blast
   then have *: "of_nat i - of_nat j = (of_nat (i-j) :: 'a)"
     by (simp add: of_nat_diff)
   then show ?thesis
     by (simp add: * i j)
 qed
 
 
 subsection \<open>Further arithmetic facts concerning the natural numbers\<close>
 
 lemma subst_equals:
   assumes "t = s" and "u = t"
   shows "u = s"
   using assms(2,1) by (rule trans)
 
 locale nat_arith
 begin
 
 lemma add1: "(A::'a::comm_monoid_add) \<equiv> k + a \<Longrightarrow> A + b \<equiv> k + (a + b)"
   by (simp only: ac_simps)
 
 lemma add2: "(B::'a::comm_monoid_add) \<equiv> k + b \<Longrightarrow> a + B \<equiv> k + (a + b)"
   by (simp only: ac_simps)
 
 lemma suc1: "A == k + a \<Longrightarrow> Suc A \<equiv> k + Suc a"
   by (simp only: add_Suc_right)
 
 lemma rule0: "(a::'a::comm_monoid_add) \<equiv> a + 0"
   by (simp only: add_0_right)
 
 end
 
 ML_file \<open>Tools/nat_arith.ML\<close>
 
 simproc_setup nateq_cancel_sums
   ("(l::nat) + m = n" | "(l::nat) = m + n" | "Suc m = n" | "m = Suc n") =
   \<open>fn phi => try o Nat_Arith.cancel_eq_conv\<close>
 
 simproc_setup natless_cancel_sums
   ("(l::nat) + m < n" | "(l::nat) < m + n" | "Suc m < n" | "m < Suc n") =
   \<open>fn phi => try o Nat_Arith.cancel_less_conv\<close>
 
 simproc_setup natle_cancel_sums
   ("(l::nat) + m \<le> n" | "(l::nat) \<le> m + n" | "Suc m \<le> n" | "m \<le> Suc n") =
   \<open>fn phi => try o Nat_Arith.cancel_le_conv\<close>
 
 simproc_setup natdiff_cancel_sums
   ("(l::nat) + m - n" | "(l::nat) - (m + n)" | "Suc m - n" | "m - Suc n") =
   \<open>fn phi => try o Nat_Arith.cancel_diff_conv\<close>
 
 context order
 begin
 
 lemma lift_Suc_mono_le:
   assumes mono: "\<And>n. f n \<le> f (Suc n)"
     and "n \<le> n'"
   shows "f n \<le> f n'"
 proof (cases "n < n'")
   case True
   then show ?thesis
     by (induct n n' rule: less_Suc_induct) (auto intro: mono)
 next
   case False
   with \<open>n \<le> n'\<close> show ?thesis by auto
 qed
 
 lemma lift_Suc_antimono_le:
   assumes mono: "\<And>n. f n \<ge> f (Suc n)"
     and "n \<le> n'"
   shows "f n \<ge> f n'"
 proof (cases "n < n'")
   case True
   then show ?thesis
     by (induct n n' rule: less_Suc_induct) (auto intro: mono)
 next
   case False
   with \<open>n \<le> n'\<close> show ?thesis by auto
 qed
 
 lemma lift_Suc_mono_less:
   assumes mono: "\<And>n. f n < f (Suc n)"
     and "n < n'"
   shows "f n < f n'"
   using \<open>n < n'\<close> by (induct n n' rule: less_Suc_induct) (auto intro: mono)
 
 lemma lift_Suc_mono_less_iff: "(\<And>n. f n < f (Suc n)) \<Longrightarrow> f n < f m \<longleftrightarrow> n < m"
   by (blast intro: less_asym' lift_Suc_mono_less [of f]
     dest: linorder_not_less[THEN iffD1] le_eq_less_or_eq [THEN iffD1])
 
 end
 
 lemma mono_iff_le_Suc: "mono f \<longleftrightarrow> (\<forall>n. f n \<le> f (Suc n))"
   unfolding mono_def by (auto intro: lift_Suc_mono_le [of f])
 
 lemma antimono_iff_le_Suc: "antimono f \<longleftrightarrow> (\<forall>n. f (Suc n) \<le> f n)"
   unfolding antimono_def by (auto intro: lift_Suc_antimono_le [of f])
 
 lemma mono_nat_linear_lb:
   fixes f :: "nat \<Rightarrow> nat"
   assumes "\<And>m n. m < n \<Longrightarrow> f m < f n"
   shows "f m + k \<le> f (m + k)"
 proof (induct k)
   case 0
   then show ?case by simp
 next
   case (Suc k)
   then have "Suc (f m + k) \<le> Suc (f (m + k))" by simp
   also from assms [of "m + k" "Suc (m + k)"] have "Suc (f (m + k)) \<le> f (Suc (m + k))"
     by (simp add: Suc_le_eq)
   finally show ?case by simp
 qed
 
 
 text \<open>Subtraction laws, mostly by Clemens Ballarin\<close>
 
 lemma diff_less_mono:
   fixes a b c :: nat
   assumes "a < b" and "c \<le> a"
   shows "a - c < b - c"
 proof -
   from assms obtain d e where "b = c + (d + e)" and "a = c + e" and "d > 0"
     by (auto dest!: le_Suc_ex less_imp_Suc_add simp add: ac_simps)
   then show ?thesis by simp
 qed
 
 lemma less_diff_conv: "i < j - k \<longleftrightarrow> i + k < j"
   for i j k :: nat
   by (cases "k \<le> j") (auto simp add: not_le dest: less_imp_Suc_add le_Suc_ex)
 
 lemma less_diff_conv2: "k \<le> j \<Longrightarrow> j - k < i \<longleftrightarrow> j < i + k"
   for j k i :: nat
   by (auto dest: le_Suc_ex)
 
 lemma le_diff_conv: "j - k \<le> i \<longleftrightarrow> j \<le> i + k"
   for j k i :: nat
   by (cases "k \<le> j") (auto simp add: not_le dest!: less_imp_Suc_add le_Suc_ex)
 
 lemma diff_diff_cancel [simp]: "i \<le> n \<Longrightarrow> n - (n - i) = i"
   for i n :: nat
   by (auto dest: le_Suc_ex)
 
 lemma diff_less [simp]: "0 < n \<Longrightarrow> 0 < m \<Longrightarrow> m - n < m"
   for i n :: nat
   by (auto dest: less_imp_Suc_add)
 
 text \<open>Simplification of relational expressions involving subtraction\<close>
 
 lemma diff_diff_eq: "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k - (n - k) = m - n"
   for m n k :: nat
   by (auto dest!: le_Suc_ex)
 
 hide_fact (open) diff_diff_eq
 
 lemma eq_diff_iff: "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k = n - k \<longleftrightarrow> m = n"
   for m n k :: nat
   by (auto dest: le_Suc_ex)
 
 lemma less_diff_iff: "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k < n - k \<longleftrightarrow> m < n"
   for m n k :: nat
   by (auto dest!: le_Suc_ex)
 
 lemma le_diff_iff: "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k \<le> n - k \<longleftrightarrow> m \<le> n"
   for m n k :: nat
   by (auto dest!: le_Suc_ex)
 
 lemma le_diff_iff': "a \<le> c \<Longrightarrow> b \<le> c \<Longrightarrow> c - a \<le> c - b \<longleftrightarrow> b \<le> a"
   for a b c :: nat
   by (force dest: le_Suc_ex)
 
 
 text \<open>(Anti)Monotonicity of subtraction -- by Stephan Merz\<close>
 
 lemma diff_le_mono: "m \<le> n \<Longrightarrow> m - l \<le> n - l"
   for m n l :: nat
   by (auto dest: less_imp_le less_imp_Suc_add split: nat_diff_split)
 
 lemma diff_le_mono2: "m \<le> n \<Longrightarrow> l - n \<le> l - m"
   for m n l :: nat
   by (auto dest: less_imp_le le_Suc_ex less_imp_Suc_add less_le_trans split: nat_diff_split)
 
 lemma diff_less_mono2: "m < n \<Longrightarrow> m < l \<Longrightarrow> l - n < l - m"
   for m n l :: nat
   by (auto dest: less_imp_Suc_add split: nat_diff_split)
 
 lemma diffs0_imp_equal: "m - n = 0 \<Longrightarrow> n - m = 0 \<Longrightarrow> m = n"
   for m n :: nat
   by (simp split: nat_diff_split)
 
 lemma min_diff: "min (m - i) (n - i) = min m n - i"
   for m n i :: nat
   by (cases m n rule: le_cases)
     (auto simp add: not_le min.absorb1 min.absorb2 min.absorb_iff1 [symmetric] diff_le_mono)
 
 lemma inj_on_diff_nat:
   fixes k :: nat
   assumes "\<And>n. n \<in> N \<Longrightarrow> k \<le> n"
   shows "inj_on (\<lambda>n. n - k) N"
 proof (rule inj_onI)
   fix x y
   assume a: "x \<in> N" "y \<in> N" "x - k = y - k"
   with assms have "x - k + k = y - k + k" by auto
   with a assms show "x = y" by (auto simp add: eq_diff_iff)
 qed
 
 text \<open>Rewriting to pull differences out\<close>
 
 lemma diff_diff_right [simp]: "k \<le> j \<Longrightarrow> i - (j - k) = i + k - j"
   for i j k :: nat
   by (fact diff_diff_right)
 
 lemma diff_Suc_diff_eq1 [simp]:
   assumes "k \<le> j"
   shows "i - Suc (j - k) = i + k - Suc j"
 proof -
   from assms have *: "Suc (j - k) = Suc j - k"
     by (simp add: Suc_diff_le)
   from assms have "k \<le> Suc j"
     by (rule order_trans) simp
   with diff_diff_right [of k "Suc j" i] * show ?thesis
     by simp
 qed
 
 lemma diff_Suc_diff_eq2 [simp]:
   assumes "k \<le> j"
   shows "Suc (j - k) - i = Suc j - (k + i)"
 proof -
   from assms obtain n where "j = k + n"
     by (auto dest: le_Suc_ex)
   moreover have "Suc n - i = (k + Suc n) - (k + i)"
     using add_diff_cancel_left [of k "Suc n" i] by simp
   ultimately show ?thesis by simp
 qed
 
 lemma Suc_diff_Suc:
   assumes "n < m"
   shows "Suc (m - Suc n) = m - n"
 proof -
   from assms obtain q where "m = n + Suc q"
     by (auto dest: less_imp_Suc_add)
   moreover define r where "r = Suc q"
   ultimately have "Suc (m - Suc n) = r" and "m = n + r"
     by simp_all
   then show ?thesis by simp
 qed
 
 lemma one_less_mult: "Suc 0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> Suc 0 < m * n"
   using less_1_mult [of n m] by (simp add: ac_simps)
 
 lemma n_less_m_mult_n: "0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> n < m * n"
   using mult_strict_right_mono [of 1 m n] by simp
 
 lemma n_less_n_mult_m: "0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> n < n * m"
   using mult_strict_left_mono [of 1 m n] by simp
 
 
 text \<open>Induction starting beyond zero\<close>
 
 lemma nat_induct_at_least [consumes 1, case_names base Suc]:
   "P n" if "n \<ge> m" "P m" "\<And>n. n \<ge> m \<Longrightarrow> P n \<Longrightarrow> P (Suc n)"
 proof -
   define q where "q = n - m"
   with \<open>n \<ge> m\<close> have "n = m + q"
     by simp
   moreover have "P (m + q)"
     by (induction q) (use that in simp_all)
   ultimately show "P n"
     by simp
 qed
 
 lemma nat_induct_non_zero [consumes 1, case_names 1 Suc]:
   "P n" if "n > 0" "P 1" "\<And>n. n > 0 \<Longrightarrow> P n \<Longrightarrow> P (Suc n)"
 proof -
   from \<open>n > 0\<close> have "n \<ge> 1"
     by (cases n) simp_all
   moreover note \<open>P 1\<close>
   moreover have "\<And>n. n \<ge> 1 \<Longrightarrow> P n \<Longrightarrow> P (Suc n)"
     using \<open>\<And>n. n > 0 \<Longrightarrow> P n \<Longrightarrow> P (Suc n)\<close>
     by (simp add: Suc_le_eq)
   ultimately show "P n"
     by (rule nat_induct_at_least)
 qed
 
 
 text \<open>Specialized induction principles that work "backwards":\<close>
 
 lemma inc_induct [consumes 1, case_names base step]:
   assumes less: "i \<le> j"
     and base: "P j"
     and step: "\<And>n. i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P (Suc n) \<Longrightarrow> P n"
   shows "P i"
   using less step
 proof (induct "j - i" arbitrary: i)
   case (0 i)
   then have "i = j" by simp
   with base show ?case by simp
 next
   case (Suc d n)
   from Suc.hyps have "n \<noteq> j" by auto
   with Suc have "n < j" by (simp add: less_le)
   from \<open>Suc d = j - n\<close> have "d + 1 = j - n" by simp
   then have "d + 1 - 1 = j - n - 1" by simp
   then have "d = j - n - 1" by simp
   then have "d = j - (n + 1)" by (simp add: diff_diff_eq)
   then have "d = j - Suc n" by simp
   moreover from \<open>n < j\<close> have "Suc n \<le> j" by (simp add: Suc_le_eq)
   ultimately have "P (Suc n)"
   proof (rule Suc.hyps)
     fix q
     assume "Suc n \<le> q"
     then have "n \<le> q" by (simp add: Suc_le_eq less_imp_le)
     moreover assume "q < j"
     moreover assume "P (Suc q)"
     ultimately show "P q" by (rule Suc.prems)
   qed
   with order_refl \<open>n < j\<close> show "P n" by (rule Suc.prems)
 qed
 
 lemma strict_inc_induct [consumes 1, case_names base step]:
   assumes less: "i < j"
     and base: "\<And>i. j = Suc i \<Longrightarrow> P i"
     and step: "\<And>i. i < j \<Longrightarrow> P (Suc i) \<Longrightarrow> P i"
   shows "P i"
 using less proof (induct "j - i - 1" arbitrary: i)
   case (0 i)
   from \<open>i < j\<close> obtain n where "j = i + n" and "n > 0"
     by (auto dest!: less_imp_Suc_add)
   with 0 have "j = Suc i"
     by (auto intro: order_antisym simp add: Suc_le_eq)
   with base show ?case by simp
 next
   case (Suc d i)
   from \<open>Suc d = j - i - 1\<close> have *: "Suc d = j - Suc i"
     by (simp add: diff_diff_add)
   then have "Suc d - 1 = j - Suc i - 1" by simp
   then have "d = j - Suc i - 1" by simp
   moreover from * have "j - Suc i \<noteq> 0" by auto
   then have "Suc i < j" by (simp add: not_le)
   ultimately have "P (Suc i)" by (rule Suc.hyps)
   with \<open>i < j\<close> show "P i" by (rule step)
 qed
 
 lemma zero_induct_lemma: "P k \<Longrightarrow> (\<And>n. P (Suc n) \<Longrightarrow> P n) \<Longrightarrow> P (k - i)"
   using inc_induct[of "k - i" k P, simplified] by blast
 
 lemma zero_induct: "P k \<Longrightarrow> (\<And>n. P (Suc n) \<Longrightarrow> P n) \<Longrightarrow> P 0"
   using inc_induct[of 0 k P] by blast
 
 text \<open>Further induction rule similar to @{thm inc_induct}.\<close>
 
 lemma dec_induct [consumes 1, case_names base step]:
   "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"
 proof (induct j arbitrary: i)
   case 0
   then show ?case by simp
 next
   case (Suc j)
   from Suc.prems consider "i \<le> j" | "i = Suc j"
     by (auto simp add: le_Suc_eq)
   then show ?case
   proof cases
     case 1
     moreover have "j < Suc j" by simp
     moreover have "P j" using \<open>i \<le> j\<close> \<open>P i\<close>
     proof (rule Suc.hyps)
       fix q
       assume "i \<le> q"
       moreover assume "q < j" then have "q < Suc j"
         by (simp add: less_Suc_eq)
       moreover assume "P q"
       ultimately show "P (Suc q)" by (rule Suc.prems)
     qed
     ultimately show "P (Suc j)" by (rule Suc.prems)
   next
     case 2
     with \<open>P i\<close> show "P (Suc j)" by simp
   qed
 qed
 
 lemma transitive_stepwise_le:
   assumes "m \<le> n" "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" and "\<And>n. R n (Suc n)"
   shows "R m n"
 using \<open>m \<le> n\<close>  
   by (induction rule: dec_induct) (use assms in blast)+
 
 
 subsubsection \<open>Greatest operator\<close>
 
 lemma ex_has_greatest_nat:
   "P (k::nat) \<Longrightarrow> \<forall>y. P y \<longrightarrow> y \<le> b \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> y \<le> x)"
 proof (induction "b-k" arbitrary: b k rule: less_induct)
   case less
   show ?case
   proof cases
     assume "\<exists>n>k. P n"
     then obtain n where "n>k" "P n" by blast
     have "n \<le> b" using \<open>P n\<close> less.prems(2) by auto
     hence "b-n < b-k"
       by(rule diff_less_mono2[OF \<open>k<n\<close> less_le_trans[OF \<open>k<n\<close>]])
     from less.hyps[OF this \<open>P n\<close> less.prems(2)]
     show ?thesis .
   next
     assume "\<not> (\<exists>n>k. P n)"
     hence "\<forall>y. P y \<longrightarrow> y \<le> k" by (auto simp: not_less)
     thus ?thesis using less.prems(1) by auto
   qed
 qed
 
 lemma GreatestI_nat:
   "\<lbrakk> P(k::nat); \<forall>y. P y \<longrightarrow> y \<le> b \<rbrakk> \<Longrightarrow> P (Greatest P)"
 apply(drule (1) ex_has_greatest_nat)
 using GreatestI2_order by auto
 
 lemma Greatest_le_nat:
   "\<lbrakk> P(k::nat);  \<forall>y. P y \<longrightarrow> y \<le> b \<rbrakk> \<Longrightarrow> k \<le> (Greatest P)"
 apply(frule (1) ex_has_greatest_nat)
 using GreatestI2_order[where P=P and Q=\<open>\<lambda>x. k \<le> x\<close>] by auto
 
 lemma GreatestI_ex_nat:
   "\<lbrakk> \<exists>k::nat. P k;  \<forall>y. P y \<longrightarrow> y \<le> b \<rbrakk> \<Longrightarrow> P (Greatest P)"
 apply (erule exE)
 apply (erule (1) GreatestI_nat)
 done
 
 
 subsection \<open>Monotonicity of \<open>funpow\<close>\<close>
 
 lemma funpow_increasing: "m \<le> n \<Longrightarrow> mono f \<Longrightarrow> (f ^^ n) \<top> \<le> (f ^^ m) \<top>"
   for f :: "'a::{lattice,order_top} \<Rightarrow> 'a"
   by (induct rule: inc_induct)
     (auto simp del: funpow.simps(2) simp add: funpow_Suc_right
       intro: order_trans[OF _ funpow_mono])
 
 lemma funpow_decreasing: "m \<le> n \<Longrightarrow> mono f \<Longrightarrow> (f ^^ m) \<bottom> \<le> (f ^^ n) \<bottom>"
   for f :: "'a::{lattice,order_bot} \<Rightarrow> 'a"
   by (induct rule: dec_induct)
     (auto simp del: funpow.simps(2) simp add: funpow_Suc_right
       intro: order_trans[OF _ funpow_mono])
 
 lemma mono_funpow: "mono Q \<Longrightarrow> mono (\<lambda>i. (Q ^^ i) \<bottom>)"
   for Q :: "'a::{lattice,order_bot} \<Rightarrow> 'a"
   by (auto intro!: funpow_decreasing simp: mono_def)
 
 lemma antimono_funpow: "mono Q \<Longrightarrow> antimono (\<lambda>i. (Q ^^ i) \<top>)"
   for Q :: "'a::{lattice,order_top} \<Rightarrow> 'a"
   by (auto intro!: funpow_increasing simp: antimono_def)
 
 
 subsection \<open>The divides relation on \<^typ>\<open>nat\<close>\<close>
 
 lemma dvd_1_left [iff]: "Suc 0 dvd k"
   by (simp add: dvd_def)
 
 lemma dvd_1_iff_1 [simp]: "m dvd Suc 0 \<longleftrightarrow> m = Suc 0"
   by (simp add: dvd_def)
 
 lemma nat_dvd_1_iff_1 [simp]: "m dvd 1 \<longleftrightarrow> m = 1"
   for m :: nat
   by (simp add: dvd_def)
 
 lemma dvd_antisym: "m dvd n \<Longrightarrow> n dvd m \<Longrightarrow> m = n"
   for m n :: nat
   unfolding dvd_def by (force dest: mult_eq_self_implies_10 simp add: mult.assoc)
 
 lemma dvd_diff_nat [simp]: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m - n)"
   for k m n :: nat
   unfolding dvd_def by (blast intro: right_diff_distrib' [symmetric])
 
 lemma dvd_diffD: "k dvd m - n \<Longrightarrow> k dvd n \<Longrightarrow> n \<le> m \<Longrightarrow> k dvd m"
   for k m n :: nat
   apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
   apply (blast intro: dvd_add)
   done
 
 lemma dvd_diffD1: "k dvd m - n \<Longrightarrow> k dvd m \<Longrightarrow> n \<le> m \<Longrightarrow> k dvd n"
   for k m n :: nat
   by (drule_tac m = m in dvd_diff_nat) auto
 
 lemma dvd_mult_cancel:
   fixes m n k :: nat
   assumes "k * m dvd k * n" and "0 < k"
   shows "m dvd n"
 proof -
   from assms(1) obtain q where "k * n = (k * m) * q" ..
   then have "k * n = k * (m * q)" by (simp add: ac_simps)
   with \<open>0 < k\<close> have "n = m * q" by (auto simp add: mult_left_cancel)
   then show ?thesis ..
 qed
 
 lemma dvd_mult_cancel1: "0 < m \<Longrightarrow> m * n dvd m \<longleftrightarrow> n = 1"
   for m n :: nat
   apply auto
   apply (subgoal_tac "m * n dvd m * 1")
    apply (drule dvd_mult_cancel)
     apply auto
   done
 
 lemma dvd_mult_cancel2: "0 < m \<Longrightarrow> n * m dvd m \<longleftrightarrow> n = 1"
   for m n :: nat
   using dvd_mult_cancel1 [of m n] by (simp add: ac_simps)
 
 lemma dvd_imp_le: "k dvd n \<Longrightarrow> 0 < n \<Longrightarrow> k \<le> n"
   for k n :: nat
   by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
 
 lemma nat_dvd_not_less: "0 < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
   for m n :: nat
   by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
 
 lemma less_eq_dvd_minus:
   fixes m n :: nat
   assumes "m \<le> n"
   shows "m dvd n \<longleftrightarrow> m dvd n - m"
 proof -
   from assms have "n = m + (n - m)" by simp
   then obtain q where "n = m + q" ..
   then show ?thesis by (simp add: add.commute [of m])
 qed
 
 lemma dvd_minus_self: "m dvd n - m \<longleftrightarrow> n < m \<or> m dvd n"
   for m n :: nat
   by (cases "n < m") (auto elim!: dvdE simp add: not_less le_imp_diff_is_add dest: less_imp_le)
 
 lemma dvd_minus_add:
   fixes m n q r :: nat
   assumes "q \<le> n" "q \<le> r * m"
   shows "m dvd n - q \<longleftrightarrow> m dvd n + (r * m - q)"
 proof -
   have "m dvd n - q \<longleftrightarrow> m dvd r * m + (n - q)"
     using dvd_add_times_triv_left_iff [of m r] by simp
   also from assms have "\<dots> \<longleftrightarrow> m dvd r * m + n - q" by simp
   also from assms have "\<dots> \<longleftrightarrow> m dvd (r * m - q) + n" by simp
   also have "\<dots> \<longleftrightarrow> m dvd n + (r * m - q)" by (simp add: add.commute)
   finally show ?thesis .
 qed
 
 
 subsection \<open>Aliasses\<close>
 
 lemma nat_mult_1: "1 * n = n"
   for n :: nat
   by (fact mult_1_left)
 
 lemma nat_mult_1_right: "n * 1 = n"
   for n :: nat
   by (fact mult_1_right)
 
 lemma nat_add_left_cancel: "k + m = k + n \<longleftrightarrow> m = n"
   for k m n :: nat
   by (fact add_left_cancel)
 
 lemma nat_add_right_cancel: "m + k = n + k \<longleftrightarrow> m = n"
   for k m n :: nat
   by (fact add_right_cancel)
 
 lemma diff_mult_distrib: "(m - n) * k = (m * k) - (n * k)"
   for k m n :: nat
   by (fact left_diff_distrib')
 
 lemma diff_mult_distrib2: "k * (m - n) = (k * m) - (k * n)"
   for k m n :: nat
   by (fact right_diff_distrib')
 
 lemma le_add_diff: "k \<le> n \<Longrightarrow> m \<le> n + m - k"
   for k m n :: nat
   by (fact le_add_diff)  (* FIXME delete *)
 
 lemma le_diff_conv2: "k \<le> j \<Longrightarrow> (i \<le> j - k) = (i + k \<le> j)"
   for i j k :: nat
   by (fact le_diff_conv2) (* FIXME delete *)
 
 lemma diff_self_eq_0 [simp]: "m - m = 0"
   for m :: nat
   by (fact diff_cancel)
 
 lemma diff_diff_left [simp]: "i - j - k = i - (j + k)"
   for i j k :: nat
   by (fact diff_diff_add)
 
 lemma diff_commute: "i - j - k = i - k - j"
   for i j k :: nat
   by (fact diff_right_commute)
 
 lemma diff_add_inverse: "(n + m) - n = m"
   for m n :: nat
   by (fact add_diff_cancel_left')
 
 lemma diff_add_inverse2: "(m + n) - n = m"
   for m n :: nat
   by (fact add_diff_cancel_right')
 
 lemma diff_cancel: "(k + m) - (k + n) = m - n"
   for k m n :: nat
   by (fact add_diff_cancel_left)
 
 lemma diff_cancel2: "(m + k) - (n + k) = m - n"
   for k m n :: nat
   by (fact add_diff_cancel_right)
 
 lemma diff_add_0: "n - (n + m) = 0"
   for m n :: nat
   by (fact diff_add_zero)
 
 lemma add_mult_distrib2: "k * (m + n) = (k * m) + (k * n)"
   for k m n :: nat
   by (fact distrib_left)
 
 lemmas nat_distrib =
   add_mult_distrib distrib_left diff_mult_distrib diff_mult_distrib2
 
 
 subsection \<open>Size of a datatype value\<close>
 
 class size =
   fixes size :: "'a \<Rightarrow> nat" \<comment> \<open>see further theory \<open>Wellfounded\<close>\<close>
 
 instantiation nat :: size
 begin
 
 definition size_nat where [simp, code]: "size (n::nat) = n"
 
 instance ..
 
 end
 
 lemmas size_nat = size_nat_def
 
 
 subsection \<open>Code module namespace\<close>
 
 code_identifier
   code_module Nat \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
 
 hide_const (open) of_nat_aux
 
 end