header {* Ring and field structures *}

 header {* (Ordered) Rings and Fields *}

 theory Ring_and_Field = Inductive:

 theory Ring_and_Field = OrderedGroup:

 subsection {* Abstract algebraic structures *}

 text {*

   The theory of partially ordered rings is taken from the books:

 subsection {* Types Classes @{text plus_ac0} and @{text times_ac1} *}

   \begin{itemize}

   \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 

 axclass plus_ac0 \<subseteq> plus, zero

   \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963

   commute:     "x + y = y + x"

   \end{itemize}

   assoc:       "(x + y) + z = x + (y + z)"

   Most of the used notions can also be looked up in 

   zero [simp]: "0 + x = x"

   \begin{itemize}

   \item \emph{www.mathworld.com} by Eric Weisstein et. al.

 lemma plus_ac0_left_commute: "x + (y+z) = y + ((x+z)::'a::plus_ac0)"

   \item \emph{Algebra I} by van der Waerden, Springer.

 by(rule mk_left_commute[of "op +",OF plus_ac0.assoc plus_ac0.commute])

   \end{itemize}

 *}

 lemma plus_ac0_zero_right [simp]: "x + 0 = (x ::'a::plus_ac0)"

 apply (rule plus_ac0.commute [THEN trans])

 axclass semiring \<subseteq> ab_semigroup_add, semigroup_mult

 apply (rule plus_ac0.zero)

   left_distrib: "(a + b) * c = a * c + b * c"

 done

   right_distrib: "a * (b + c) = a * b + a * c"

 lemmas plus_ac0 = plus_ac0.assoc plus_ac0.commute plus_ac0_left_commute

 axclass semiring_0 \<subseteq> semiring, comm_monoid_add

                   plus_ac0.zero plus_ac0_zero_right

 axclass comm_semiring \<subseteq> ab_semigroup_add, ab_semigroup_mult  

 axclass times_ac1 \<subseteq> times, one

   commute:     "x * y = y * x"

   assoc:       "(x * y) * z = x * (y * z)"

   one [simp]:  "1 * x = x"

 theorem times_ac1_left_commute: "(x::'a::times_ac1) * ((y::'a) * z) =

   y * (x * z)"

 by(rule mk_left_commute[of "op *",OF times_ac1.assoc times_ac1.commute])

 theorem times_ac1_one_right [simp]: "(x::'a::times_ac1) * 1 = x"

 proof -

   have "x * 1 = 1 * x"

     by (rule times_ac1.commute)

   also have "... = x"

     by (rule times_ac1.one)

   finally show ?thesis .

 qed

 theorems times_ac1 = times_ac1.assoc times_ac1.commute times_ac1_left_commute

   times_ac1.one times_ac1_one_right

 text{*This class is the same as @{text plus_ac0}, while using the same axiom

 names as the other axclasses.*}

 axclass abelian_semigroup \<subseteq> zero, plus

   add_assoc: "(a + b) + c = a + (b + c)"

   add_commute: "a + b = b + a"

   add_0 [simp]: "0 + a = a"

 text{*This class underlies both @{text semiring} and @{text ring}*}

 axclass almost_semiring \<subseteq> abelian_semigroup, one, times

   mult_assoc: "(a * b) * c = a * (b * c)"

   mult_1 [simp]: "1 * a = a"

   distrib: "(a + b) * c = a * c + b * c"

   left_distrib: "(a + b) * c = a * c + b * c"

 instance comm_semiring \<subseteq> semiring

   zero_neq_one [simp]: "0 \<noteq> 1"

 axclass semiring \<subseteq> almost_semiring

   add_left_imp_eq: "a + b = a + c ==> b=c"

     --{*This axiom is needed for semirings only: for rings, etc., it is

         redundant. Including it allows many more of the following results

         to be proved for semirings too.*}

 instance abelian_semigroup \<subseteq> plus_ac0

 proof

   fix x y z :: 'a

   show "x + y = y + x" by (rule add_commute)

   show "x + y + z = x + (y + z)" by (rule add_assoc)

   show "0+x = x" by (rule add_0)

 qed

 instance almost_semiring \<subseteq> times_ac1

 proof

   fix x y z :: 'a

   show "x * y = y * x" by (rule mult_commute)

   show "x * y * z = x * (y * z)" by (rule mult_assoc)

   show "1*x = x" by simp

 qed

 axclass abelian_group \<subseteq> abelian_semigroup, minus

    left_minus [simp]: "-a + a = 0"

    diff_minus: "a - b = a + -b"

 axclass ring \<subseteq> almost_semiring, abelian_group

 text{*Proving axiom @{text add_left_imp_eq} makes all @{text semiring}

       theorems available to members of @{term ring} *}

 instance ring \<subseteq> semiring

   assume "a + b = a + c"

   show "(a + b) * c = a * c + b * c" by (simp add: distrib)

   hence  "-a + a + b = -a + a + c" by (simp only: add_assoc)

   have "a * (b + c) = (b + c) * a" by (simp add: mult_ac)

   thus "b = c" by simp

   also have "... = b * a + c * a" by (simp only: distrib)

 qed

   also have "... = a * b + a * c" by (simp add: mult_ac)

   finally show "a * (b + c) = a * b + a * c" by blast

 text{*This class underlies @{text ordered_semiring} and @{text ordered_ring}*}

 qed

 axclass almost_ordered_semiring \<subseteq> semiring, linorder

   add_left_mono: "a \<le> b ==> c + a \<le> c + b"

 axclass comm_semiring_0 \<subseteq> comm_semiring, comm_monoid_add

   mult_strict_left_mono: "a < b ==> 0 < c ==> c * a < c * b"

 instance comm_semiring_0 \<subseteq> semiring_0 ..

 axclass ordered_semiring \<subseteq> almost_ordered_semiring

   zero_less_one [simp]: "0 < 1" --{*This too is needed for semirings only.*}

 axclass axclass_0_neq_1 \<subseteq> zero, one

   zero_neq_one [simp]: "0 \<noteq> 1"

 axclass ordered_ring \<subseteq> almost_ordered_semiring, ring

   abs_if: "\<bar>a\<bar> = (if a < 0 then -a else a)"

 axclass semiring_1 \<subseteq> axclass_0_neq_1, semiring_0, monoid_mult

 axclass field \<subseteq> ring, inverse

 axclass comm_semiring_1 \<subseteq> axclass_0_neq_1, comm_semiring_0, comm_monoid_mult (* previously almost_semiring *)

 instance comm_semiring_1 \<subseteq> semiring_1 ..

 axclass axclass_no_zero_divisors \<subseteq> zero, times

   no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"

 axclass comm_semiring_1_cancel \<subseteq> comm_semiring_1, cancel_ab_semigroup_add (* previously semiring *)

 axclass ring \<subseteq> semiring, ab_group_add

 instance ring \<subseteq> semiring_0 ..

 axclass comm_ring \<subseteq> comm_semiring_0, ab_group_add

 instance comm_ring \<subseteq> ring ..

 instance comm_ring \<subseteq> comm_semiring_0 ..

 axclass ring_1 \<subseteq> ring, semiring_1

 axclass comm_ring_1 \<subseteq> comm_ring, comm_semiring_1 (* previously ring *)

 instance comm_ring_1 \<subseteq> ring_1 ..

 instance comm_ring_1 \<subseteq> comm_semiring_1_cancel ..

 axclass idom \<subseteq> comm_ring_1, axclass_no_zero_divisors

 axclass field \<subseteq> comm_ring_1, inverse

 axclass ordered_field \<subseteq> ordered_ring, field

 lemma mult_zero_left [simp]: "0 * a = (0::'a::{semiring_0, cancel_semigroup_add})"

 proof -

   have "0*a + 0*a = 0*a + 0"

     by (simp add: left_distrib [symmetric])

   thus ?thesis 

     by (simp only: add_left_cancel)

 qed

 lemma mult_zero_right [simp]: "a * 0 = (0::'a::{semiring_0, cancel_semigroup_add})"

 proof -

   have "a*0 + a*0 = a*0 + 0"

     by (simp add: right_distrib [symmetric])

   thus ?thesis 

     by (simp only: add_left_cancel)

 qed

 lemma field_mult_eq_0_iff [simp]: "(a*b = (0::'a::field)) = (a = 0 | b = 0)"

 proof cases

   assume "a=0" thus ?thesis by simp

 next

   assume anz [simp]: "a\<noteq>0"

   { assume "a * b = 0"

     hence "inverse a * (a * b) = 0" by simp

     hence "b = 0"  by (simp (no_asm_use) add: mult_assoc [symmetric])}

   thus ?thesis by force

 qed

 instance field \<subseteq> idom

 by (intro_classes, simp)

      "a*e + (b*e + c) = (a+b)*e + (c::'a::almost_semiring)"

      "a*e + (b*e + c) = (a+b)*e + (c::'a::semiring)"

 by (simp add: mult_commute [of _ c] right_diff_distrib) 

 by (simp add: left_distrib diff_minus 

               minus_mult_left [symmetric] minus_mult_right [symmetric]) 

 lemma minus_diff_eq [simp]: "- (a - b) = b - (a::'a::ring)"

 by (simp add: diff_minus add_commute) 

 axclass pordered_semiring \<subseteq> semiring_0, pordered_ab_semigroup_add 

   mult_left_mono: "a <= b \<Longrightarrow> 0 <= c \<Longrightarrow> c * a <= c * b"

   mult_right_mono: "a <= b \<Longrightarrow> 0 <= c \<Longrightarrow> a * c <= b * c"

 subsection {* Ordering Rules for Addition *}

 axclass pordered_cancel_semiring \<subseteq> pordered_semiring, cancel_ab_semigroup_add

 lemma add_right_mono: "a \<le> (b::'a::almost_ordered_semiring) ==> a + c \<le> b + c"

 by (simp add: add_commute [of _ c] add_left_mono)

 axclass ordered_semiring_strict \<subseteq> semiring_0, ordered_cancel_ab_semigroup_add

   mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"

 text {* non-strict, in both arguments *}

   mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"

 lemma add_mono:

      "[|a \<le> b;  c \<le> d|] ==> a + c \<le> b + (d::'a::almost_ordered_semiring)"

 instance ordered_semiring_strict \<subseteq> pordered_cancel_semiring

   apply (erule add_right_mono [THEN order_trans])

 apply intro_classes

   apply (simp add: add_commute add_left_mono)

 apply (case_tac "a < b & 0 < c")

   done

 apply (auto simp add: mult_strict_left_mono order_less_le)

 apply (auto simp add: mult_strict_left_mono order_le_less)

 lemma add_strict_left_mono:

 apply (simp add: mult_strict_right_mono)

      "a < b ==> c + a < c + (b::'a::almost_ordered_semiring)"

 done

  by (simp add: order_less_le add_left_mono) 

 axclass pordered_comm_semiring \<subseteq> comm_semiring_0, pordered_ab_semigroup_add

 lemma add_strict_right_mono:

   mult_mono: "a <= b \<Longrightarrow> 0 <= c \<Longrightarrow> c * a <= c * b"

      "a < b ==> a + c < b + (c::'a::almost_ordered_semiring)"

  by (simp add: add_commute [of _ c] add_strict_left_mono)

 axclass pordered_cancel_comm_semiring \<subseteq> pordered_comm_semiring, cancel_ab_semigroup_add

 text{*Strict monotonicity in both arguments*}

 instance pordered_cancel_comm_semiring \<subseteq> pordered_comm_semiring ..

 lemma add_strict_mono: "[|a<b; c<d|] ==> a + c < b + (d::'a::almost_ordered_semiring)"

 apply (erule add_strict_right_mono [THEN order_less_trans])

 axclass ordered_comm_semiring_strict \<subseteq> comm_semiring_0, ordered_cancel_ab_semigroup_add

 apply (erule add_strict_left_mono)

   mult_strict_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"

 done

 instance pordered_comm_semiring \<subseteq> pordered_semiring

 lemma add_less_le_mono:

 by (intro_classes, insert mult_mono, simp_all add: mult_commute, blast+)

      "[| a<b; c\<le>d |] ==> a + c < b + (d::'a::almost_ordered_semiring)"

 apply (erule add_strict_right_mono [THEN order_less_le_trans])

 instance pordered_cancel_comm_semiring \<subseteq> pordered_cancel_semiring ..

 apply (erule add_left_mono) 

 done

 instance ordered_comm_semiring_strict \<subseteq> ordered_semiring_strict

 by (intro_classes, insert mult_strict_mono, simp_all add: mult_commute, blast+)

 lemma add_le_less_mono:

      "[| a\<le>b; c<d |] ==> a + c < b + (d::'a::almost_ordered_semiring)"

 instance ordered_comm_semiring_strict \<subseteq> pordered_cancel_comm_semiring

 apply (erule add_right_mono [THEN order_le_less_trans])

 apply (intro_classes)

 apply (erule add_strict_left_mono) 

 apply (case_tac "a < b & 0 < c")

 done

 apply (auto simp add: mult_strict_left_mono order_less_le)

 apply (auto simp add: mult_strict_left_mono order_le_less)

 lemma add_less_imp_less_left:

 done

       assumes less: "c + a < c + b"  shows "a < (b::'a::almost_ordered_semiring)"

 proof (rule ccontr)

 axclass pordered_ring \<subseteq> ring, pordered_semiring 

   assume "~ a < b"

   hence "b \<le> a" by (simp add: linorder_not_less)

 instance pordered_ring \<subseteq> pordered_ab_group_add ..

   hence "c+b \<le> c+a" by (rule add_left_mono)

   with this and less show False 

 instance pordered_ring \<subseteq> pordered_cancel_semiring ..

     by (simp add: linorder_not_less [symmetric])

 qed

 axclass lordered_ring \<subseteq> pordered_ring, lordered_ab_group_abs

 lemma add_less_imp_less_right:

 axclass axclass_abs_if \<subseteq> minus, ord, zero

       "a + c < b + c ==> a < (b::'a::almost_ordered_semiring)"

   abs_if: "abs a = (if (a < 0) then (-a) else a)"

 apply (rule add_less_imp_less_left [of c])

 apply (simp add: add_commute)  

 axclass ordered_ring_strict \<subseteq> ring, ordered_semiring_strict, axclass_abs_if

 done

 instance ordered_ring_strict \<subseteq> lordered_ab_group ..

 lemma add_less_cancel_left [simp]:

     "(c+a < c+b) = (a < (b::'a::almost_ordered_semiring))"

 instance ordered_ring_strict \<subseteq> lordered_ring

 by (blast intro: add_less_imp_less_left add_strict_left_mono) 

 by (intro_classes, simp add: abs_if join_eq_if)

 lemma add_less_cancel_right [simp]:

 axclass pordered_comm_ring \<subseteq> comm_ring, pordered_comm_semiring

     "(a+c < b+c) = (a < (b::'a::almost_ordered_semiring))"

 by (blast intro: add_less_imp_less_right add_strict_right_mono)

 axclass ordered_semidom \<subseteq> comm_semiring_1_cancel, ordered_comm_semiring_strict (* previously ordered_semiring *)

   zero_less_one [simp]: "0 < 1"

 lemma add_le_cancel_left [simp]:

     "(c+a \<le> c+b) = (a \<le> (b::'a::almost_ordered_semiring))"

 axclass ordered_idom \<subseteq> comm_ring_1, ordered_comm_semiring_strict, axclass_abs_if (* previously ordered_ring *)

 by (simp add: linorder_not_less [symmetric]) 

 instance ordered_idom \<subseteq> ordered_ring_strict ..

 lemma add_le_cancel_right [simp]:

     "(a+c \<le> b+c) = (a \<le> (b::'a::almost_ordered_semiring))"

 axclass ordered_field \<subseteq> field, ordered_idom

 by (simp add: linorder_not_less [symmetric]) 

 lemma add_le_imp_le_left:

       "c + a \<le> c + b ==> a \<le> (b::'a::almost_ordered_semiring)"

 by simp

 lemma add_le_imp_le_right:

       "a + c \<le> b + c ==> a \<le> (b::'a::almost_ordered_semiring)"

 by simp

 lemma add_increasing: "[|0\<le>a; b\<le>c|] ==> b \<le> a + (c::'a::almost_ordered_semiring)"

 by (insert add_mono [of 0 a b c], simp)

 subsection {* Ordering Rules for Unary Minus *}

 lemma le_imp_neg_le:

       assumes "a \<le> (b::'a::ordered_ring)" shows "-b \<le> -a"

 proof -

   have "-a+a \<le> -a+b"

     by (rule add_left_mono) 

   hence "0 \<le> -a+b"

     by simp

   hence "0 + (-b) \<le> (-a + b) + (-b)"

     by (rule add_right_mono) 

   thus ?thesis

     by (simp add: add_assoc)

 qed

 lemma neg_le_iff_le [simp]: "(-b \<le> -a) = (a \<le> (b::'a::ordered_ring))"

 proof 

   assume "- b \<le> - a"

   hence "- (- a) \<le> - (- b)"

     by (rule le_imp_neg_le)

   thus "a\<le>b" by simp

 next

   assume "a\<le>b"

   thus "-b \<le> -a" by (rule le_imp_neg_le)

 qed

 lemma neg_le_0_iff_le [simp]: "(-a \<le> 0) = (0 \<le> (a::'a::ordered_ring))"

 by (subst neg_le_iff_le [symmetric], simp)

 lemma neg_0_le_iff_le [simp]: "(0 \<le> -a) = (a \<le> (0::'a::ordered_ring))"

 by (subst neg_le_iff_le [symmetric], simp)

 lemma neg_less_iff_less [simp]: "(-b < -a) = (a < (b::'a::ordered_ring))"

 by (force simp add: order_less_le) 

 lemma neg_less_0_iff_less [simp]: "(-a < 0) = (0 < (a::'a::ordered_ring))"

 by (subst neg_less_iff_less [symmetric], simp)

 lemma neg_0_less_iff_less [simp]: "(0 < -a) = (a < (0::'a::ordered_ring))"

 by (subst neg_less_iff_less [symmetric], simp)

 text{*The next several equations can make the simplifier loop!*}

 lemma less_minus_iff: "(a < - b) = (b < - (a::'a::ordered_ring))"

 proof -

   have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less)

   thus ?thesis by simp

 qed

 lemma minus_less_iff: "(- a < b) = (- b < (a::'a::ordered_ring))"

 proof -

   have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less)

   thus ?thesis by simp

 qed

 lemma le_minus_iff: "(a \<le> - b) = (b \<le> - (a::'a::ordered_ring))"

 apply (simp add: linorder_not_less [symmetric])

 apply (rule minus_less_iff) 

 done

 lemma minus_le_iff: "(- a \<le> b) = (- b \<le> (a::'a::ordered_ring))"

 apply (simp add: linorder_not_less [symmetric])

 apply (rule less_minus_iff) 

 done

 subsection{*Subtraction Laws*}

 lemma add_diff_eq: "a + (b - c) = (a + b) - (c::'a::abelian_group)"

 by (simp add: diff_minus plus_ac0)

 lemma diff_add_eq: "(a - b) + c = (a + c) - (b::'a::abelian_group)"

 by (simp add: diff_minus plus_ac0)

 lemma diff_eq_eq: "(a-b = c) = (a = c + (b::'a::abelian_group))"

 by (auto simp add: diff_minus add_assoc)

 lemma eq_diff_eq: "(a = c-b) = (a + (b::'a::abelian_group) = c)"

 by (auto simp add: diff_minus add_assoc)

 lemma diff_diff_eq: "(a - b) - c = a - (b + (c::'a::abelian_group))"

 by (simp add: diff_minus plus_ac0)

 lemma diff_diff_eq2: "a - (b - c) = (a + c) - (b::'a::abelian_group)"

 by (simp add: diff_minus plus_ac0)

 text{*Further subtraction laws for ordered rings*}

 lemma less_iff_diff_less_0: "(a < b) = (a - b < (0::'a::ordered_ring))"

 proof -

   have  "(a < b) = (a + (- b) < b + (-b))"  

     by (simp only: add_less_cancel_right)

   also have "... =  (a - b < 0)" by (simp add: diff_minus)

   finally show ?thesis .

 qed

 lemma diff_less_eq: "(a-b < c) = (a < c + (b::'a::ordered_ring))"

 apply (subst less_iff_diff_less_0)

 apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])

 apply (simp add: diff_minus add_ac)

 done

 lemma less_diff_eq: "(a < c-b) = (a + (b::'a::ordered_ring) < c)"

 apply (subst less_iff_diff_less_0)

 apply (rule less_iff_diff_less_0 [of _ "c-b", THEN ssubst])

 apply (simp add: diff_minus add_ac)

 done

 lemma diff_le_eq: "(a-b \<le> c) = (a \<le> c + (b::'a::ordered_ring))"

 by (simp add: linorder_not_less [symmetric] less_diff_eq)

 lemma le_diff_eq: "(a \<le> c-b) = (a + (b::'a::ordered_ring) \<le> c)"

 by (simp add: linorder_not_less [symmetric] diff_less_eq)

 text{*This list of rewrites simplifies (in)equalities by bringing subtractions

   to the top and then moving negative terms to the other side.

   Use with @{text add_ac}*}

 lemmas compare_rls =

        diff_minus [symmetric]

        add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2

        diff_less_eq less_diff_eq diff_le_eq le_diff_eq

        diff_eq_eq eq_diff_eq

 text{*This list of rewrites decides ring equalities by ordered rewriting.*}

 lemmas ring_eq_simps =

   times_ac1.assoc times_ac1.commute times_ac1_left_commute

   left_distrib right_distrib left_diff_distrib right_diff_distrib

   plus_ac0.assoc plus_ac0.commute plus_ac0_left_commute

   add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2

   diff_eq_eq eq_diff_eq

 subsection{*Lemmas for the @{text cancel_numerals} simproc*}

 lemma eq_iff_diff_eq_0: "(a = b) = (a-b = (0::'a::abelian_group))"

 by (simp add: compare_rls)

 lemma le_iff_diff_le_0: "(a \<le> b) = (a-b \<le> (0::'a::ordered_ring))"

 by (simp add: compare_rls)

 apply (simp add: compare_rls minus_mult_left [symmetric]) 

 apply (simp add: compare_rls minus_mult_left [symmetric])

      "(a*e + c < b*e + d) = ((a-b)*e + c < (d::'a::ordered_ring))"

      "(a*e + c < b*e + d) = ((a-b)*e + c < (d::'a::pordered_ring))"

      "(a*e + c < b*e + d) = (c < (b-a)*e + (d::'a::ordered_ring))"

      "(a*e + c < b*e + d) = (c < (b-a)*e + (d::'a::pordered_ring))"

      "(a*e + c \<le> b*e + d) = ((a-b)*e + c \<le> (d::'a::ordered_ring))"

      "(a*e + c \<le> b*e + d) = ((a-b)*e + c \<le> (d::'a::pordered_ring))"

      "(a*e + c \<le> b*e + d) = (c \<le> (b-a)*e + (d::'a::ordered_ring))"

      "(a*e + c \<le> b*e + d) = (c \<le> (b-a)*e + (d::'a::pordered_ring))"

      "[|c*a \<le> c*b; 0 < c|] ==> a \<le> (b::'a::almost_ordered_semiring)"

      "[|c*a \<le> c*b; 0 < c|] ==> a \<le> (b::'a::ordered_semiring_strict)"

      "[|a*c \<le> b*c; 0 < c|] ==> a \<le> (b::'a::almost_ordered_semiring)"

      "[|a*c \<le> b*c; 0 < c|] ==> a \<le> (b::'a::ordered_semiring_strict)"

      "[|c*a < c*b; 0 \<le> c|] ==> a < (b::'a::almost_ordered_semiring)"

      "[|c*a < c*b; 0 \<le> c|] ==> a < (b::'a::ordered_semiring_strict)"

      "[|a*c < b*c; 0 \<le> c|] ==> a < (b::'a::almost_ordered_semiring)"

      "[|a*c < b*c; 0 \<le> c|] ==> a < (b::'a::ordered_semiring_strict)"

      "[|b < a; c < 0|] ==> c * a < c * (b::'a::ordered_ring)"

      "[|b < a; c < 0|] ==> c * a < c * (b::'a::ordered_ring_strict)"

      "[|b < a; c < 0|] ==> a * c < b * (c::'a::ordered_ring)"

      "[|b < a; c < 0|] ==> a * c < b * (c::'a::ordered_ring_strict)"

 lemma mult_pos: "[| (0::'a::almost_ordered_semiring) < a; 0 < b |] ==> 0 < a*b"

 lemma mult_pos: "[| (0::'a::ordered_semiring_strict) < a; 0 < b |] ==> 0 < a*b"

 lemma mult_pos_neg: "[| (0::'a::almost_ordered_semiring) < a; b < 0 |] ==> a*b < 0"

 lemma mult_pos_le: "[| (0::'a::pordered_cancel_semiring) \<le> a; 0 \<le> b |] ==> 0 \<le> a*b"

 by (drule mult_left_mono [of 0 b], auto)

 lemma mult_pos_neg: "[| (0::'a::ordered_semiring_strict) < a; b < 0 |] ==> a*b < 0"

 lemma mult_neg: "[| a < (0::'a::ordered_ring); b < 0 |] ==> 0 < a*b"

 lemma mult_pos_neg_le: "[| (0::'a::pordered_cancel_semiring) \<le> a; b \<le> 0 |] ==> a*b \<le> 0"

 by (drule mult_left_mono [of b 0], auto)

 lemma mult_pos_neg2: "[| (0::'a::ordered_semiring_strict) < a; b < 0 |] ==> b*a < 0" 

 by (drule mult_strict_right_mono[of b 0], auto)

 lemma mult_pos_neg2_le: "[| (0::'a::pordered_cancel_semiring) \<le> a; b \<le> 0 |] ==> b*a \<le> 0" 

 by (drule mult_right_mono[of b 0], auto)

 lemma mult_neg: "[| a < (0::'a::ordered_ring_strict); b < 0 |] ==> 0 < a*b"

      "[| 0 < a*b; 0 < a|] ==> 0 < (b::'a::almost_ordered_semiring)"

      "[| 0 < a*b; 0 < a|] ==> 0 < (b::'a::ordered_semiring_strict)"

      "((0::'a::ordered_ring) < a*b) = (0 < a & 0 < b | a < 0 & b < 0)"

      "((0::'a::ordered_ring_strict) < a*b) = (0 < a & 0 < b | a < 0 & b < 0)"

 apply (simp add: mult_commute [of a b]) 

 apply (blast dest: zero_less_mult_pos2)

 apply (blast dest: zero_less_mult_pos) 

 lemma mult_eq_0_iff [simp]: "(a*b = (0::'a::ordered_ring)) = (a = 0 | b = 0)"

 lemma mult_eq_0_iff [simp]: "(a*b = (0::'a::ordered_ring_strict)) = (a = 0 | b = 0)"

      "((0::'a::ordered_ring) \<le> a*b) = (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"

      "((0::'a::ordered_ring_strict) \<le> a*b) = (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"

      "(a*b < (0::'a::ordered_ring)) = (0 < a & b < 0 | a < 0 & 0 < b)"

      "(a*b < (0::'a::ordered_ring_strict)) = (0 < a & b < 0 | a < 0 & 0 < b)"

      "(a*b \<le> (0::'a::ordered_ring)) = (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"

      "(a*b \<le> (0::'a::ordered_ring_strict)) = (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"

 lemma zero_le_square: "(0::'a::ordered_ring) \<le> a*a"

 lemma split_mult_pos_le: "(0 \<le> a & 0 \<le> b) | (a \<le> 0 & b \<le> 0) \<Longrightarrow> 0 \<le> a * (b::_::pordered_ring)"

 by (auto simp add: mult_pos_le mult_neg_le)

 lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> (0::_::pordered_cancel_semiring)" 

 by (auto simp add: mult_pos_neg_le mult_pos_neg2_le)

 lemma zero_le_square: "(0::'a::ordered_ring_strict) \<le> a*a"

 text{*Proving axiom @{text zero_less_one} makes all @{text ordered_semiring}

 text{*Proving axiom @{text zero_less_one} makes all @{text ordered_semidom}

       theorems available to members of @{term ordered_ring} *}

       theorems available to members of @{term ordered_idom} *}

 instance ordered_ring \<subseteq> ordered_semiring

 instance ordered_idom \<subseteq> ordered_semidom

 lemma zero_le_one [simp]: "(0::'a::ordered_semiring) \<le> 1"

 lemma zero_le_one [simp]: "(0::'a::ordered_semidom) \<le> 1"

 lemma not_one_le_zero [simp]: "~ (1::'a::ordered_semiring) \<le> 0"

 lemma not_one_le_zero [simp]: "~ (1::'a::ordered_semidom) \<le> 0"

 by (simp add: linorder_not_le zero_less_one) 

 by (simp add: linorder_not_le) 

 lemma not_one_less_zero [simp]: "~ (1::'a::ordered_semiring) < 0"

 lemma not_one_less_zero [simp]: "~ (1::'a::ordered_semidom) < 0"

 by (simp add: linorder_not_less zero_le_one) 

 by (simp add: linorder_not_less) 

      "[|b \<le> a; c \<le> 0|] ==> c * a \<le> c * (b::'a::ordered_ring)"

      "[|b \<le> a; c \<le> 0|] ==> c * a \<le> c * (b::'a::pordered_ring)"

      "[|b \<le> a; c \<le> 0|] ==> a * c \<le> b * (c::'a::ordered_ring)"

      "[|b \<le> a; c \<le> 0|] ==> a * c \<le> b * (c::'a::pordered_ring)"

   by (simp add: mult_left_mono_neg mult_commute [of _ c]) 

 apply (drule mult_right_mono [of _ _ "-c"]) 

 apply (simp_all add: minus_mult_right [symmetric]) 

 done  

      "[|a<b; c<d; 0<b; 0\<le>c|] ==> a * c < b * (d::'a::ordered_semiring)"

      "[|a<b; c<d; 0<b; 0\<le>c|] ==> a * c < b * (d::'a::ordered_semiring_strict)"

      "[| a<b; c<d; 0 \<le> a; 0 \<le> c|] ==> a * c < b * (d::'a::ordered_semiring)"

      "[| a<b; c<d; 0 \<le> a; 0 \<le> c|] ==> a * c < b * (d::'a::ordered_semiring_strict)"

       ==> a * c  \<le>  b * (d::'a::ordered_semiring)"

       ==> a * c  \<le>  b * (d::'a::pordered_semiring)"

 lemma less_1_mult: "[| 1 < m; 1 < n |] ==> 1 < m*(n::'a::ordered_semiring)"

 lemma less_1_mult: "[| 1 < m; 1 < n |] ==> 1 < m*(n::'a::ordered_semidom)"

     "(a*c < b*c) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring)))"

     "(a*c < b*c) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring_strict)))"

     "(c*a < c*b) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring)))"

     "(c*a < c*b) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring_strict)))"

 by (simp add: mult_commute [of c] mult_less_cancel_right)

 apply (case_tac "c = 0")

 apply (auto simp add: linorder_neq_iff mult_strict_left_mono 

                       mult_strict_left_mono_neg)

 apply (auto simp add: linorder_not_less 

                       linorder_not_le [symmetric, of "c*a"]

                       linorder_not_le [symmetric, of a])

 apply (erule_tac [!] notE)

 apply (auto simp add: order_less_imp_le mult_left_mono 

                       mult_left_mono_neg)

 done

      "(a*c \<le> b*c) = ((0<c --> a\<le>b) & (c<0 --> b \<le> (a::'a::ordered_ring)))"

      "(a*c \<le> b*c) = ((0<c --> a\<le>b) & (c<0 --> b \<le> (a::'a::ordered_ring_strict)))"

      "(c*a \<le> c*b) = ((0<c --> a\<le>b) & (c<0 --> b \<le> (a::'a::ordered_ring)))"

      "(c*a \<le> c*b) = ((0<c --> a\<le>b) & (c<0 --> b \<le> (a::'a::ordered_ring_strict)))"

 by (simp add: mult_commute [of c] mult_le_cancel_right)

 by (simp add: linorder_not_less [symmetric] mult_less_cancel_left)

       shows "a < (b::'a::ordered_semiring)"

       shows "a < (b::'a::ordered_semiring_strict)"

     "[|a*c < b*c; 0 \<le> c|] ==> a < (b::'a::ordered_semiring)"

   assumes less: "a*c < b*c" and nonneg: "0 <= c"

   by (rule mult_less_imp_less_left, simp add: mult_commute)

   shows "a < (b::'a::ordered_semiring_strict)"

 proof (rule ccontr)

   assume "~ a < b"

   hence "b \<le> a" by (simp add: linorder_not_less)

   hence "b*c \<le> a*c" by (rule mult_right_mono)

   with this and less show False 

     by (simp add: linorder_not_less [symmetric])

 qed  

      "(a*c = b*c) = (c = (0::'a::ordered_ring) | a=b)"

      "(a*c = b*c) = (c = (0::'a::ordered_ring_strict) | a=b)"

      "(c*a = c*b) = (c = (0::'a::ordered_ring) | a=b)"

      "(c*a = c*b) = (c = (0::'a::ordered_ring_strict) | a=b)"

 by (simp add: mult_commute [of c] mult_cancel_right)

 apply (cut_tac linorder_less_linear [of 0 c])

 apply (force dest: mult_strict_left_mono_neg mult_strict_left_mono

              simp add: linorder_neq_iff)

 done

 text{*This list of rewrites decides ring equalities by ordered rewriting.*}

 lemmas ring_eq_simps =

   mult_ac

   left_distrib right_distrib left_diff_distrib right_diff_distrib

   add_ac

   add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2

   diff_eq_eq eq_diff_eq

 thm ring_eq_simps

 lemma less_add_one: "a < (a+1::'a::ordered_semiring)"

 lemma less_add_one: "a < (a+1::'a::ordered_semidom)"

 proof -

 proof -

   have "a+0 < (a+1::'a::ordered_semiring)"

   have "a+0 < (a+1::'a::ordered_semidom)"

 lemma zero_less_two: "0 < (1+1::'a::ordered_semiring)"

 lemma zero_less_two: "0 < (1+1::'a::ordered_semidom)"

 lemma abs_zero [simp]: "abs 0 = (0::'a::ordered_ring)"

 lemma abs_one [simp]: "abs 1 = (1::'a::ordered_idom)"

 by (simp add: abs_if)

 lemma abs_one [simp]: "abs 1 = (1::'a::ordered_ring)"

 lemma abs_mult: "abs (a * b) = abs a * abs (b::'a::ordered_ring)" 

 lemma abs_le_mult: "abs (a * b) \<le> (abs a) * (abs (b::'a::lordered_ring))" 

 apply (case_tac "a=0 | b=0", force) 

 proof -

 apply (auto elim: order_less_asym

   let ?x = "pprt a * pprt b - pprt a * nprt b - nprt a * pprt b + nprt a * nprt b"

             simp add: abs_if mult_less_0_iff linorder_neq_iff

   let ?y = "pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"

                   minus_mult_left [symmetric] minus_mult_right [symmetric])  

   have a: "(abs a) * (abs b) = ?x"

 done

     by (simp only: abs_prts[of a] abs_prts[of b] ring_eq_simps)

   {

 lemma abs_mult_self: "abs a * abs a = a * (a::'a::ordered_ring)"

     fix u v :: 'a

     have bh: "\<lbrakk>u = a; v = b\<rbrakk> \<Longrightarrow> u * v = ?y"

       apply (subst prts[of u], subst prts[of v])

       apply (simp add: left_distrib right_distrib add_ac) 

       done

   }

   note b = this[OF refl[of a] refl[of b]]

   note addm = add_mono[of "0::'a" _ "0::'a", simplified]

   note addm2 = add_mono[of _ "0::'a" _ "0::'a", simplified]

   have xy: "- ?x <= ?y"

     apply (simp add: compare_rls)

     apply (rule add_le_imp_le_left[of "-(pprt a * nprt b + nprt a * pprt b)"])

     apply (simp add: add_ac)

     proof -

       let ?r = "nprt a * nprt b +(nprt a * nprt b + (nprt a * pprt b + (pprt a * nprt b + (pprt a * pprt b + (pprt a * pprt b +

 	(- (nprt a * pprt b) + - (pprt a * nprt b)))))))"

       let ?rr = "nprt a * nprt b + nprt a * nprt b + ((nprt a * pprt b) + (- (nprt a * pprt b))) + ((pprt a * nprt b) + - (pprt a * nprt b))

 	+ pprt a * pprt b + pprt a * pprt b"

       have a:"?r = ?rr" by (simp only: add_ac)      

       have "0 <= ?rr"

 	apply (simp)

 	apply (rule addm)+

 	apply (simp_all add: mult_neg_le mult_pos_le)

 	done

       with a show "0 <= ?r" by simp

     qed

   have yx: "?y <= ?x"

     apply (simp add: add_ac)

     apply (simp add: compare_rls)

     apply (rule add_le_imp_le_right[of _ "-(pprt a * pprt b)"])

     apply (simp add: add_ac)

     apply (rule addm2, (simp add: mult_pos_neg_le mult_pos_neg2_le)+)+

     done

   have i1: "a*b <= abs a * abs b" by (simp only: a b yx)

   have i2: "- (abs a * abs b) <= a*b" by (simp only: a b xy)

   show ?thesis

     apply (rule abs_leI)

     apply (simp add: i1)

     apply (simp add: i2[simplified minus_le_iff])

     done

 qed

 lemma abs_eq_mult: 

   assumes "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)"

   shows "abs (a*b) = abs a * abs (b::'a::lordered_ring)"

 proof -

   have s: "(0 <= a*b) | (a*b <= 0)"

     apply (auto)    

     apply (rule_tac split_mult_pos_le)

     apply (rule_tac contrapos_np[of "a*b <= 0"])

     apply (simp)

     apply (rule_tac split_mult_neg_le)

     apply (insert prems)

     apply (blast)

     done

   have mulprts: "a * b = (pprt a + nprt a) * (pprt b + nprt b)"

     by (simp add: prts[symmetric])

   show ?thesis

   proof cases

     assume "0 <= a * b"

     then show ?thesis

       apply (simp_all add: mulprts abs_prts)

       apply (insert prems)

       apply (auto simp add: ring_eq_simps iff2imp[OF zero_le_iff_zero_nprt] iff2imp[OF le_zero_iff_zero_pprt]

 	iff2imp[OF le_zero_iff_pprt_id] iff2imp[OF zero_le_iff_nprt_id] order_antisym mult_pos_neg_le[of a b] mult_pos_neg2_le[of b a])

       done

   next

     assume "~(0 <= a*b)"

     with s have "a*b <= 0" by simp

     then show ?thesis

       apply (simp_all add: mulprts abs_prts)

       apply (insert prems)

       apply (auto simp add: ring_eq_simps iff2imp[OF zero_le_iff_zero_nprt] iff2imp[OF le_zero_iff_zero_pprt]

 	iff2imp[OF le_zero_iff_pprt_id] iff2imp[OF zero_le_iff_nprt_id] order_antisym mult_pos_le[of a b] mult_neg_le[of a b])

       done

   qed

 qed

 lemma abs_mult: "abs (a * b) = abs a * abs (b::'a::ordered_idom)" 

 by (simp add: abs_eq_mult linorder_linear)

 lemma abs_mult_self: "abs a * abs a = a * (a::'a::ordered_idom)"