Quelle Rings.thy Sprache: Isabelle

(*  Title:      HOL/Rings.thy
    Author:     Gertrud Bauer
    Author:     Steven Obua
    Author:     Tobias Nipkow
    Author:     Lawrence C Paulson
    Author:     Markus Wenzel
    Author:     Jeremy Avigad
*)

section \<open>Rings\<close>

theory Rings
  imports Groups Set Fun
begin

subsection \<open>Semirings and rings\<close>

class semiring = ab_semigroup_add + semigroup_mult +
  assumes distrib_right [algebra_simps, algebra_split_simps]: "(a + b) * c = a * c + b * c"
  assumes distrib_left [algebra_simps, algebra_split_simps]: "a * (b + c) = a * b + a * c"
begin

text \<open>For the \<open>combine_numerals\<close> simproc\<close>
lemma combine_common_factor: "a * e + (b * e + c) = (a + b) * e + c"
  by (simp add: distrib_right ac_simps)

end

class mult_zero = times + zero +
  assumes mult_zero_left [simp]: "0 * a = 0"
  assumes mult_zero_right [simp]: "a * 0 = 0"
begin

lemma mult_not_zero: "a * b \ 0 \ a \ 0 \ b \ 0"
  by auto

end

class semiring_0 = semiring + comm_monoid_add + mult_zero

class semiring_0_cancel = semiring + cancel_comm_monoid_add
begin

subclass semiring_0
proof
  fix a :: 'a
  have "0 * a + 0 * a = 0 * a + 0"
    by (simp add: distrib_right [symmetric])
  then show "0 * a = 0"
    by (simp only: add_left_cancel)
  have "a * 0 + a * 0 = a * 0 + 0"
    by (simp add: distrib_left [symmetric])
  then show "a * 0 = 0"
    by (simp only: add_left_cancel)
qed

end

class comm_semiring = ab_semigroup_add + ab_semigroup_mult +
  assumes distrib: "(a + b) * c = a * c + b * c"
begin

subclass semiring
proof
  fix a b c :: 'a
  show "(a + b) * c = a * c + b * c"
    by (simp add: distrib)
  have "a * (b + c) = (b + c) * a"
    by (simp add: ac_simps)
  also have "\ = b * a + c * a"
    by (simp only: distrib)
  also have "\ = a * b + a * c"
    by (simp add: ac_simps)
  finally show "a * (b + c) = a * b + a * c"
    by blast
qed

end

class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero
begin

subclass semiring_0 ..

end

class comm_semiring_0_cancel = comm_semiring + cancel_comm_monoid_add
begin

subclass semiring_0_cancel ..

subclass comm_semiring_0 ..

end

class zero_neq_one = zero + one +
  assumes zero_neq_one [simp]: "0 \ 1"
begin

lemma one_neq_zero [simp]: "1 \ 0"
  by (rule not_sym) (rule zero_neq_one)

definition of_bool :: "bool \ 'a"
  where "of_bool p = (if p then 1 else 0)"

lemma of_bool_eq [simp, code]:
  "of_bool False = 0"
  "of_bool True = 1"
  by (simp_all add: of_bool_def)

lemma of_bool_eq_iff: "of_bool p = of_bool q \ p = q"
  by (simp add: of_bool_def)

lemma split_of_bool [split]: "P (of_bool p) \ (p \ P 1) \ (\ p \ P 0)"
  by (cases p) simp_all

lemma split_of_bool_asm: "P (of_bool p) \ \ (p \ \ P 1 \ \ p \ \ P 0)"
  by (cases p) simp_all

lemma of_bool_eq_0_iff [simp]:
  \<open>of_bool P = 0 \<longleftrightarrow> \<not> P\<close>
  by simp

lemma of_bool_eq_1_iff [simp]:
  \<open>of_bool P = 1 \<longleftrightarrow> P\<close>
  by simp

end

class semiring_1 = zero_neq_one + semiring_0 + monoid_mult
begin

lemma of_bool_conj:
  "of_bool (P \ Q) = of_bool P * of_bool Q"
  by auto

end

lemma lambda_zero: "(\h::'a::mult_zero. 0) = (*) 0"
  by auto

lemma lambda_one: "(\x::'a::monoid_mult. x) = (*) 1"
  by auto

subsection \<open>Abstract divisibility\<close>

class dvd = times
begin

definition dvd :: "'a \ 'a \ bool" (infix \dvd\ 50)
  where "b dvd a \ (\k. a = b * k)"

lemma dvdI [intro?]: "a = b * k \ b dvd a"
  unfolding dvd_def ..

lemma dvdE [elim]: "b dvd a \ (\k. a = b * k \ P) \ P"
  unfolding dvd_def by blast

end

context comm_monoid_mult
begin

subclass dvd .

lemma dvd_refl [simp]: "a dvd a"
proof
  show "a = a * 1" by simp
qed

lemma dvd_trans [trans]:
  assumes "a dvd b" and "b dvd c"
  shows "a dvd c"
proof -
  from assms obtain v where "b = a * v"
    by auto
  moreover from assms obtain w where "c = b * w"
    by auto
  ultimately have "c = a * (v * w)"
    by (simp add: mult.assoc)
  then show ?thesis ..
qed

lemma subset_divisors_dvd: "{c. c dvd a} \ {c. c dvd b} \ a dvd b"
  by (auto simp add: subset_iff intro: dvd_trans)

lemma strict_subset_divisors_dvd: "{c. c dvd a} \ {c. c dvd b} \ a dvd b \ \ b dvd a"
  by (auto simp add: subset_iff intro: dvd_trans)

lemma one_dvd [simp]: "1 dvd a"
  by (auto intro: dvdI)

lemma dvd_mult [simp]: "a dvd (b * c)" if "a dvd c"
  using that by (auto intro: mult.left_commute dvdI)

lemma dvd_mult2 [simp]: "a dvd (b * c)" if "a dvd b"
  using that dvd_mult [of a b c] by (simp add: ac_simps)

lemma dvd_triv_right [simp]: "a dvd b * a"
  by (rule dvd_mult) (rule dvd_refl)

lemma dvd_triv_left [simp]: "a dvd a * b"
  by (rule dvd_mult2) (rule dvd_refl)

lemma mult_dvd_mono:
  assumes "a dvd b"
    and "c dvd d"
  shows "a * c dvd b * d"
proof -
  from \<open>a dvd b\<close> obtain b' where "b = a * b'" ..
  moreover from \<open>c dvd d\<close> obtain d' where "d = c * d'" ..
  ultimately have "b * d = (a * c) * (b' * d')"
    by (simp add: ac_simps)
  then show ?thesis ..
qed

lemma dvd_mult_left: "a * b dvd c \ a dvd c"
  by (simp add: dvd_def mult.assoc) blast

lemma dvd_mult_right: "a * b dvd c \ b dvd c"
  using dvd_mult_left [of b a c] by (simp add: ac_simps)

end

class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult
begin

subclass semiring_1 ..

lemma dvd_0_left_iff [simp]: "0 dvd a \ a = 0"
  by auto

lemma dvd_0_right [iff]: "a dvd 0"
proof
  show "0 = a * 0" by simp
qed

lemma dvd_0_left: "0 dvd a \ a = 0"
  by simp

lemma dvd_add [simp]:
  assumes "a dvd b" and "a dvd c"
  shows "a dvd (b + c)"
proof -
  from \<open>a dvd b\<close> obtain b' where "b = a * b'" ..
  moreover from \<open>a dvd c\<close> obtain c' where "c = a * c'" ..
  ultimately have "b + c = a * (b' + c')"
    by (simp add: distrib_left)
  then show ?thesis ..
qed

end

class semiring_1_cancel = semiring + cancel_comm_monoid_add
  + zero_neq_one + monoid_mult
begin

subclass semiring_0_cancel ..

subclass semiring_1 ..

end

class comm_semiring_1_cancel =
  comm_semiring + cancel_comm_monoid_add + zero_neq_one + comm_monoid_mult +
  assumes right_diff_distrib' [algebra_simps, algebra_split_simps]:
    "a * (b - c) = a * b - a * c"
begin

subclass semiring_1_cancel ..
subclass comm_semiring_0_cancel ..
subclass comm_semiring_1 ..

lemma left_diff_distrib' [algebra_simps, algebra_split_simps]:
  "(b - c) * a = b * a - c * a"
  by (simp add: algebra_simps)

lemma dvd_add_times_triv_left_iff [simp]: "a dvd c * a + b \ a dvd b"
proof -
  have "a dvd a * c + b \ a dvd b" (is "?P \ ?Q")
  proof
    assume ?Q
    then show ?P by simp
  next
    assume ?P
    then obtain d where "a * c + b = a * d" ..
    then have "a * c + b - a * c = a * d - a * c" by simp
    then have "b = a * d - a * c" by simp
    then have "b = a * (d - c)" by (simp add: algebra_simps)
    then show ?Q ..
  qed
  then show "a dvd c * a + b \ a dvd b" by (simp add: ac_simps)
qed

lemma dvd_add_times_triv_right_iff [simp]: "a dvd b + c * a \ a dvd b"
  using dvd_add_times_triv_left_iff [of a c b] by (simp add: ac_simps)

lemma dvd_add_triv_left_iff [simp]: "a dvd a + b \ a dvd b"
  using dvd_add_times_triv_left_iff [of a 1 b] by simp

lemma dvd_add_triv_right_iff [simp]: "a dvd b + a \ a dvd b"
  using dvd_add_times_triv_right_iff [of a b 1] by simp

lemma dvd_add_right_iff:
  assumes "a dvd b"
  shows "a dvd b + c \ a dvd c" (is "?P \ ?Q")
proof
  assume ?P
  then obtain d where "b + c = a * d" ..
  moreover from \<open>a dvd b\<close> obtain e where "b = a * e" ..
  ultimately have "a * e + c = a * d" by simp
  then have "a * e + c - a * e = a * d - a * e" by simp
  then have "c = a * d - a * e" by simp
  then have "c = a * (d - e)" by (simp add: algebra_simps)
  then show ?Q ..
next
  assume ?Q
  with assms show ?P by simp
qed

lemma dvd_add_left_iff: "a dvd c \ a dvd b + c \ a dvd b"
  using dvd_add_right_iff [of a c b] by (simp add: ac_simps)

end

class ring = semiring + ab_group_add
begin

subclass semiring_0_cancel ..

text \<open>Distribution rules\<close>

lemma minus_mult_left: "- (a * b) = - a * b"
  by (rule minus_unique) (simp add: distrib_right [symmetric])

lemma minus_mult_right: "- (a * b) = a * - b"
  by (rule minus_unique) (simp add: distrib_left [symmetric])

text \<open>Extract signs from products\<close>
lemmas mult_minus_left [simp] = minus_mult_left [symmetric]
lemmas mult_minus_right [simp] = minus_mult_right [symmetric]

lemma minus_mult_minus [simp]: "- a * - b = a * b"
  by simp

lemma minus_mult_commute: "- a * b = a * - b"
  by simp

lemma right_diff_distrib [algebra_simps, algebra_split_simps]:
  "a * (b - c) = a * b - a * c"
  using distrib_left [of a b "-c "] by simp

lemma left_diff_distrib [algebra_simps, algebra_split_simps]:
  "(a - b) * c = a * c - b * c"
  using distrib_right [of a "- b" c] by simp

lemmas ring_distribs = distrib_left distrib_right left_diff_distrib right_diff_distrib

lemma eq_add_iff1: "a * e + c = b * e + d \ (a - b) * e + c = d"
  by (simp add: algebra_simps)

lemma eq_add_iff2: "a * e + c = b * e + d \ c = (b - a) * e + d"
  by (simp add: algebra_simps)

end

lemmas ring_distribs = distrib_left distrib_right left_diff_distrib right_diff_distrib

class comm_ring = comm_semiring + ab_group_add
begin

subclass ring ..
subclass comm_semiring_0_cancel ..

lemma square_diff_square_factored: "x * x - y * y = (x + y) * (x - y)"
  by (simp add: algebra_simps)

end

class ring_1 = ring + zero_neq_one + monoid_mult
begin

subclass semiring_1_cancel ..

lemma of_bool_not_iff:
  \<open>of_bool (\<not> P) = 1 - of_bool P\<close>
  by simp

lemma square_diff_one_factored: "x * x - 1 = (x + 1) * (x - 1)"
  by (simp add: algebra_simps)

end

class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult
begin

subclass ring_1 ..
subclass comm_semiring_1_cancel
  by standard (simp add: algebra_simps)

lemma dvd_minus_iff [simp]: "x dvd - y \ x dvd y"
proof
  assume "x dvd - y"
  then have "x dvd - 1 * - y" by (rule dvd_mult)
  then show "x dvd y" by simp
next
  assume "x dvd y"
  then have "x dvd - 1 * y" by (rule dvd_mult)
  then show "x dvd - y" by simp
qed

lemma minus_dvd_iff [simp]: "- x dvd y \ x dvd y"
proof
  assume "- x dvd y"
  then obtain k where "y = - x * k" ..
  then have "y = x * - k" by simp
  then show "x dvd y" ..
next
  assume "x dvd y"
  then obtain k where "y = x * k" ..
  then have "y = - x * - k" by simp
  then show "- x dvd y" ..
qed

lemma dvd_diff_right_iff:
  assumes "a dvd b"
  shows "a dvd b - c \ a dvd c" (is "?P \ ?Q")
  using dvd_add_right_iff[of a b "-c"] assms by auto

lemma dvd_diff_left_iff:
  shows "a dvd c \ a dvd b - c \ a dvd b"
  using dvd_add_left_iff[of a "-c" b] by auto

lemma dvd_diff [simp]: "x dvd y \ x dvd z \ x dvd (y - z)"
  using dvd_add [of x y "- z"] by simp

end

subsection \<open>Towards integral domains\<close>

class semiring_no_zero_divisors = semiring_0 +
  assumes no_zero_divisors: "a \ 0 \ b \ 0 \ a * b \ 0"
begin

lemma divisors_zero:
  assumes "a * b = 0"
  shows "a = 0 \ b = 0"
proof (rule classical)
  assume "\ ?thesis"
  then have "a \ 0" and "b \ 0" by auto
  with no_zero_divisors have "a * b \ 0" by blast
  with assms show ?thesis by simp
qed

lemma mult_eq_0_iff [simp]: "a * b = 0 \ a = 0 \ b = 0"
proof (cases "a = 0 \ b = 0")
  case False
  then have "a \ 0" and "b \ 0" by auto
    then show ?thesis using no_zero_divisors by simp
next
  case True
  then show ?thesis by auto
qed

end

class semiring_1_no_zero_divisors = semiring_1 + semiring_no_zero_divisors

class semiring_no_zero_divisors_cancel = semiring_no_zero_divisors +
  assumes mult_cancel_right [simp]: "a * c = b * c \ c = 0 \ a = b"
    and mult_cancel_left [simp]: "c * a = c * b \ c = 0 \ a = b"
begin

lemma mult_left_cancel: "c \ 0 \ c * a = c * b \ a = b"
  by simp

lemma mult_right_cancel: "c \ 0 \ a * c = b * c \ a = b"
  by simp

end

class ring_no_zero_divisors = ring + semiring_no_zero_divisors
begin

subclass semiring_no_zero_divisors_cancel
proof
  fix a b c
  have "a * c = b * c \ (a - b) * c = 0"
    by (simp add: algebra_simps)
  also have "\ \ c = 0 \ a = b"
    by auto
  finally show "a * c = b * c \ c = 0 \ a = b" .
  have "c * a = c * b \ c * (a - b) = 0"
    by (simp add: algebra_simps)
  also have "\ \ c = 0 \ a = b"
    by auto
  finally show "c * a = c * b \ c = 0 \ a = b" .
qed

end

class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
begin

subclass semiring_1_no_zero_divisors ..

lemma square_eq_1_iff: "x * x = 1 \ x = 1 \ x = - 1"
proof -
  have "(x - 1) * (x + 1) = x * x - 1"
    by (simp add: algebra_simps)
  then have "x * x = 1 \ (x - 1) * (x + 1) = 0"
    by simp
  then show ?thesis
    by (simp add: eq_neg_iff_add_eq_0)
qed

lemma mult_cancel_right1 [simp]: "c = b * c \ c = 0 \ b = 1"
  using mult_cancel_right [of 1 c b] by auto

lemma mult_cancel_right2 [simp]: "a * c = c \ c = 0 \ a = 1"
  using mult_cancel_right [of a c 1] by simp

lemma mult_cancel_left1 [simp]: "c = c * b \ c = 0 \ b = 1"
  using mult_cancel_left [of c 1 b] by force

lemma mult_cancel_left2 [simp]: "c * a = c \ c = 0 \ a = 1"
  using mult_cancel_left [of c a 1] by simp

end

class semidom = comm_semiring_1_cancel + semiring_no_zero_divisors
begin

subclass semiring_1_no_zero_divisors ..

end

class idom = comm_ring_1 + semiring_no_zero_divisors
begin

subclass semidom ..

subclass ring_1_no_zero_divisors ..

lemma dvd_mult_cancel_right [simp]:
  "a * c dvd b * c \ c = 0 \ a dvd b"
proof -
  have "a * c dvd b * c \ (\k. b * c = (a * k) * c)"
    by (auto simp add: ac_simps)
  also have "(\k. b * c = (a * k) * c) \ c = 0 \ a dvd b"
    by auto
  finally show ?thesis .
qed

lemma dvd_mult_cancel_left [simp]:
  "c * a dvd c * b \ c = 0 \ a dvd b"
  using dvd_mult_cancel_right [of a c b] by (simp add: ac_simps)

lemma square_eq_iff: "a * a = b * b \ a = b \ a = - b"
proof
  assume "a * a = b * b"
  then have "(a - b) * (a + b) = 0"
    by (simp add: algebra_simps)
  then show "a = b \ a = - b"
    by (simp add: eq_neg_iff_add_eq_0)
next
  assume "a = b \ a = - b"
  then show "a * a = b * b" by auto
qed

lemma inj_mult_left [simp]: \<open>inj ((*) a) \<longleftrightarrow> a \<noteq> 0\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
proof
  assume ?P
  show ?Q
  proof
    assume \<open>a = 0\<close>
    with \<open>?P\<close> have "inj ((*) 0)"
      by simp
    moreover have "0 * 0 = 0 * 1"
      by simp
    ultimately have "0 = 1"
      by (rule injD)
    then show False
      by simp
  qed
next
  assume ?Q then show ?P
    by (auto intro: injI)
qed

end

class idom_abs_sgn = idom + abs + sgn +
  assumes sgn_mult_abs: "sgn a * \a\ = a"
    and sgn_sgn [simp]: "sgn (sgn a) = sgn a"
    and abs_abs [simp]: "\\a\\ = \a\"
    and abs_0 [simp]: "\0\ = 0"
    and sgn_0 [simp]: "sgn 0 = 0"
    and sgn_1 [simp]: "sgn 1 = 1"
    and sgn_minus_1: "sgn (- 1) = - 1"
    and sgn_mult: "sgn (a * b) = sgn a * sgn b"
begin

lemma sgn_eq_0_iff:
  "sgn a = 0 \ a = 0"
proof -
  { assume "sgn a = 0"
    then have "sgn a * \a\ = 0"
      by simp
    then have "a = 0"
      by (simp add: sgn_mult_abs)
  } then show ?thesis
    by auto
qed

lemma abs_eq_0_iff:
  "\a\ = 0 \ a = 0"
proof -
  { assume "\a\ = 0"
    then have "sgn a * \a\ = 0"
      by simp
    then have "a = 0"
      by (simp add: sgn_mult_abs)
  } then show ?thesis
    by auto
qed

lemma abs_mult_sgn:
  "\a\ * sgn a = a"
  using sgn_mult_abs [of a] by (simp add: ac_simps)

lemma abs_1 [simp]:
  "\1\ = 1"
  using sgn_mult_abs [of 1] by simp

lemma sgn_abs [simp]:
  "\sgn a\ = of_bool (a \ 0)"
  using sgn_mult_abs [of "sgn a"] mult_cancel_left [of "sgn a" "\sgn a\" 1]
  by (auto simp add: sgn_eq_0_iff)

lemma abs_sgn [simp]:
  "sgn \a\ = of_bool (a \ 0)"
  using sgn_mult_abs [of "\a\"] mult_cancel_right [of "sgn \a\" "\a\" 1]
  by (auto simp add: abs_eq_0_iff)

lemma abs_mult:
  "\a * b\ = \a\ * \b\"
proof (cases "a = 0 \ b = 0")
  case True
  then show ?thesis
    by auto
next
  case False
  then have *: "sgn (a * b) \ 0"
    by (simp add: sgn_eq_0_iff)
  from abs_mult_sgn [of "a * b"] abs_mult_sgn [of a] abs_mult_sgn [of b]
  have "\a * b\ * sgn (a * b) = \a\ * sgn a * \b\ * sgn b"
    by (simp add: ac_simps)
  then have "\a * b\ * sgn (a * b) = \a\ * \b\ * sgn (a * b)"
    by (simp add: sgn_mult ac_simps)
  with * show ?thesis
    by simp
qed

lemma sgn_minus [simp]:
  "sgn (- a) = - sgn a"
proof -
  from sgn_minus_1 have "sgn (- 1 * a) = - 1 * sgn a"
    by (simp only: sgn_mult)
  then show ?thesis
    by simp
qed

lemma abs_minus [simp]:
  "\- a\ = \a\"
proof -
  have [simp]: "\- 1\ = 1"
    using sgn_mult_abs [of "- 1"] by simp
  then have "\- 1 * a\ = 1 * \a\"
    by (simp only: abs_mult)
  then show ?thesis
    by simp
qed

end

subsection \<open>(Partial) Division\<close>

class divide =
  fixes divide :: "'a \ 'a \ 'a" (infixl \div\ 70)

setup \<open>Sign.add_const_constraint (\<^const_name>\<open>divide\<close>, SOME \<^typ>\<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>)\<close>

context semiring
begin

lemma [field_simps, field_split_simps]:
  shows distrib_left_NO_MATCH: "NO_MATCH (x div y) a \ a * (b + c) = a * b + a * c"
    and distrib_right_NO_MATCH: "NO_MATCH (x div y) c \ (a + b) * c = a * c + b * c"
  by (rule distrib_left distrib_right)+

end

context ring
begin

lemma [field_simps, field_split_simps]:
  shows left_diff_distrib_NO_MATCH: "NO_MATCH (x div y) c \ (a - b) * c = a * c - b * c"
    and right_diff_distrib_NO_MATCH: "NO_MATCH (x div y) a \ a * (b - c) = a * b - a * c"
  by (rule left_diff_distrib right_diff_distrib)+

end

setup \<open>Sign.add_const_constraint (\<^const_name>\<open>divide\<close>, SOME \<^typ>\<open>'a::divide \<Rightarrow> 'a \<Rightarrow> 'a\<close>)\<close>

class divide_trivial = zero + one + divide +
  assumes div_by_0 [simp]: \<open>a div 0 = 0\<close>
    and div_by_1 [simp]: \<open>a div 1 = a\<close>
    and div_0 [simp]: \<open>0 div a = 0\<close>


text \<open>Algebraic classes with division\<close>

class semidom_divide = semidom + divide +
  assumes nonzero_mult_div_cancel_right [simp]: \<open>b \<noteq> 0 \<Longrightarrow> (a * b) div b = a\<close>
  assumes semidom_div_by_0: \<open>a div 0 = 0\<close>
begin

lemma nonzero_mult_div_cancel_left [simp]: \<open>a \<noteq> 0 \<Longrightarrow> (a * b) div a = b\<close>
  using nonzero_mult_div_cancel_right [of a b] by (simp add: ac_simps)

subclass divide_trivial
proof
  show [simp]: \<open>a div 0 = 0\<close> for a
    by (fact semidom_div_by_0)
  show \<open>a div 1 = a\<close> for a
    using nonzero_mult_div_cancel_right [of 1 a] by simp
  show \<open>0 div a = 0\<close> for a
    using nonzero_mult_div_cancel_right [of a 0] by (cases \<open>a = 0\<close>) simp_all
qed

subclass semiring_no_zero_divisors_cancel
proof
  show *: "a * c = b * c \ c = 0 \ a = b" for a b c
  proof (cases "c = 0")
    case True
    then show ?thesis by simp
  next
    case False
    have "a = b" if "a * c = b * c"
    proof -
      from that have "a * c div c = b * c div c"
        by simp
      with False show ?thesis
        by simp
    qed
    then show ?thesis by auto
  qed
  show "c * a = c * b \ c = 0 \ a = b" for a b c
    using * [of a c b] by (simp add: ac_simps)
qed

lemma div_self [simp]: "a \ 0 \ a div a = 1"
  using nonzero_mult_div_cancel_left [of a 1] by simp

lemma dvd_div_eq_0_iff:
  assumes "b dvd a"
  shows "a div b = 0 \ a = 0"
  using assms by (elim dvdE, cases "b = 0") simp_all

lemma dvd_div_eq_cancel:
  "a div c = b div c \ c dvd a \ c dvd b \ a = b"
  by (elim dvdE, cases "c = 0") simp_all

lemma dvd_div_eq_iff:
  "c dvd a \ c dvd b \ a div c = b div c \ a = b"
  by (elim dvdE, cases "c = 0") simp_all

lemma inj_on_mult:
  "inj_on ((*) a) A" if "a \ 0"
proof (rule inj_onI)
  fix b c
  assume "a * b = a * c"
  then have "a * b div a = a * c div a"
    by (simp only:)
  with that show "b = c"
    by simp
qed

end

class idom_divide = idom + semidom_divide
begin

lemma dvd_neg_div:
  assumes "b dvd a"
  shows "- a div b = - (a div b)"
proof (cases "b = 0")
  case True
  then show ?thesis by simp
next
  case False
  from assms obtain c where "a = b * c" ..
  then have "- a div b = (b * - c) div b"
    by simp
  from False also have "\ = - c"
    by (rule nonzero_mult_div_cancel_left)
  with False \<open>a = b * c\<close> show ?thesis
    by simp
qed

lemma dvd_div_neg:
  assumes "b dvd a"
  shows "a div - b = - (a div b)"
proof (cases "b = 0")
  case True
  then show ?thesis by simp
next
  case False
  then have "- b \ 0"
    by simp
  from assms obtain c where "a = b * c" ..
  then have "a div - b = (- b * - c) div - b"
    by simp
  from \<open>- b \<noteq> 0\<close> also have "\<dots> = - c"
    by (rule nonzero_mult_div_cancel_left)
  with False \<open>a = b * c\<close> show ?thesis
    by simp
qed

end

class algebraic_semidom = semidom_divide
begin

text \<open>
  Class \<^class>\<open>algebraic_semidom\<close> enriches a integral domain
  by notions from algebra, like units in a ring.
  It is a separate class to avoid spoiling fields with notions
  which are degenerated there.
\<close>

lemma dvd_times_left_cancel_iff [simp]:
  assumes "a \ 0"
  shows "a * b dvd a * c \ b dvd c"
    (is "?lhs \ ?rhs")
proof
  assume ?lhs
  then obtain d where "a * c = a * b * d" ..
  with assms have "c = b * d" by (simp add: ac_simps)
  then show ?rhs ..
next
  assume ?rhs
  then obtain d where "c = b * d" ..
  then have "a * c = a * b * d" by (simp add: ac_simps)
  then show ?lhs ..
qed

lemma dvd_times_right_cancel_iff [simp]:
  assumes "a \ 0"
  shows "b * a dvd c * a \ b dvd c"
  using dvd_times_left_cancel_iff [of a b c] assms by (simp add: ac_simps)

lemma div_dvd_iff_mult:
  assumes "b \ 0" and "b dvd a"
  shows "a div b dvd c \ a dvd c * b"
proof -
  from \<open>b dvd a\<close> obtain d where "a = b * d" ..
  with \<open>b \<noteq> 0\<close> show ?thesis by (simp add: ac_simps)
qed

lemma dvd_div_iff_mult:
  assumes "c \ 0" and "c dvd b"
  shows "a dvd b div c \ a * c dvd b"
proof -
  from \<open>c dvd b\<close> obtain d where "b = c * d" ..
  with \<open>c \<noteq> 0\<close> show ?thesis by (simp add: mult.commute [of a])
qed

lemma div_dvd_div [simp]:
  assumes "a dvd b" and "a dvd c"
  shows "b div a dvd c div a \ b dvd c"
proof (cases "a = 0")
  case True
  with assms show ?thesis by simp
next
  case False
  moreover from assms obtain k l where "b = a * k" and "c = a * l"
    by blast
  ultimately show ?thesis by simp
qed

lemma div_add [simp]:
  assumes "c dvd a" and "c dvd b"
  shows "(a + b) div c = a div c + b div c"
proof (cases "c = 0")
  case True
  then show ?thesis by simp
next
  case False
  moreover from assms obtain k l where "a = c * k" and "b = c * l"
    by blast
  moreover have "c * k + c * l = c * (k + l)"
    by (simp add: algebra_simps)
  ultimately show ?thesis
    by simp
qed

lemma div_mult_div_if_dvd:
  assumes "b dvd a" and "d dvd c"
  shows "(a div b) * (c div d) = (a * c) div (b * d)"
proof (cases "b = 0 \ c = 0")
  case True
  with assms show ?thesis by auto
next
  case False
  moreover from assms obtain k l where "a = b * k" and "c = d * l"
    by blast
  moreover have "b * k * (d * l) div (b * d) = (b * d) * (k * l) div (b * d)"
    by (simp add: ac_simps)
  ultimately show ?thesis by simp
qed

lemma dvd_div_eq_mult:
  assumes "a \ 0" and "a dvd b"
  shows "b div a = c \ b = c * a"
    (is "?lhs \ ?rhs")
proof
  assume ?rhs
  then show ?lhs by (simp add: assms)
next
  assume ?lhs
  then have "b div a * a = c * a" by simp
  moreover from assms have "b div a * a = b"
    by (auto simp add: ac_simps)
  ultimately show ?rhs by simp
qed

lemma dvd_div_mult_self [simp]: "a dvd b \ b div a * a = b"
  by (cases "a = 0") (auto simp add: ac_simps)

lemma dvd_mult_div_cancel [simp]: "a dvd b \ a * (b div a) = b"
  using dvd_div_mult_self [of a b] by (simp add: ac_simps)

lemma div_mult_swap:
  assumes "c dvd b"
  shows "a * (b div c) = (a * b) div c"
proof (cases "c = 0")
  case True
  then show ?thesis by simp
next
  case False
  from assms obtain d where "b = c * d" ..
  moreover from False have "a * divide (d * c) c = ((a * d) * c) div c"
    by simp
  ultimately show ?thesis by (simp add: ac_simps)
qed

lemma dvd_div_mult: "c dvd b \ b div c * a = (b * a) div c"
  using div_mult_swap [of c b a] by (simp add: ac_simps)

lemma dvd_div_mult2_eq:
  assumes "b * c dvd a"
  shows "a div (b * c) = a div b div c"
proof -
  from assms obtain k where "a = b * c * k" ..
  then show ?thesis
    by (cases "b = 0 \ c = 0") (auto, simp add: ac_simps)
qed

lemma dvd_div_div_eq_mult:
  assumes "a \ 0" "c \ 0" and "a dvd b" "c dvd d"
  shows "b div a = d div c \ b * c = a * d"
    (is "?lhs \ ?rhs")
proof -
  from assms have "a * c \ 0" by simp
  then have "?lhs \ b div a * (a * c) = d div c * (a * c)"
    by simp
  also have "\ \ (a * (b div a)) * c = (c * (d div c)) * a"
    by (simp add: ac_simps)
  also have "\ \ (a * b div a) * c = (c * d div c) * a"
    using assms by (simp add: div_mult_swap)
  also have "\ \ ?rhs"
    using assms by (simp add: ac_simps)
  finally show ?thesis .
qed

lemma dvd_mult_imp_div:
  assumes "a * c dvd b"
  shows "a dvd b div c"
proof (cases "c = 0")
  case True then show ?thesis by simp
next
  case False
  from \<open>a * c dvd b\<close> obtain d where "b = a * c * d" ..
  with False show ?thesis
    by (simp add: mult.commute [of a] mult.assoc)
qed

lemma div_div_eq_right:
  assumes "c dvd b" "b dvd a"
  shows   "a div (b div c) = a div b * c"
proof (cases "c = 0 \ b = 0")
  case True
  then show ?thesis
    by auto
next
  case False
  from assms obtain r s where "b = c * r" and "a = c * r * s"
    by blast
  moreover with False have "r \ 0"
    by auto
  ultimately show ?thesis using False
    by simp (simp add: mult.commute [of _ r] mult.assoc mult.commute [of c])
qed

lemma div_div_div_same:
  assumes "d dvd b" "b dvd a"
  shows   "(a div d) div (b div d) = a div b"
proof (cases "b = 0 \ d = 0")
  case True
  with assms show ?thesis
    by auto
next
  case False
  from assms obtain r s
    where "a = d * r * s" and "b = d * r"
    by blast
  with False show ?thesis
    by simp (simp add: ac_simps)
qed

text \<open>Units: invertible elements in a ring\<close>

abbreviation is_unit :: "'a \ bool"
  where "is_unit a \ a dvd 1"

lemma not_is_unit_0 [simp]: "\ is_unit 0"
  by simp

lemma unit_imp_dvd [dest]: "is_unit b \ b dvd a"
  by (rule dvd_trans [of _ 1]) simp_all

lemma unit_dvdE:
  assumes "is_unit a"
  obtains c where "a \ 0" and "b = a * c"
proof -
  from assms have "a dvd b" by auto
  then obtain c where "b = a * c" ..
  moreover from assms have "a \ 0" by auto
  ultimately show thesis using that by blast
qed

lemma dvd_unit_imp_unit: "a dvd b \ is_unit b \ is_unit a"
  by (rule dvd_trans)

lemma unit_div_1_unit [simp, intro]:
  assumes "is_unit a"
  shows "is_unit (1 div a)"
proof -
  from assms have "1 = 1 div a * a" by simp
  then show "is_unit (1 div a)" by (rule dvdI)
qed

lemma is_unitE [elim?]:
  assumes "is_unit a"
  obtains b where "a \ 0" and "b \ 0"
    and "is_unit b" and "1 div a = b" and "1 div b = a"
    and "a * b = 1" and "c div a = c * b"
proof (rule that)
  define b where "b = 1 div a"
  then show "1 div a = b" by simp
  from assms b_def show "is_unit b" by simp
  with assms show "a \ 0" and "b \ 0" by auto
  from assms b_def show "a * b = 1" by simp
  then have "1 = a * b" ..
  with b_def \<open>b \<noteq> 0\<close> show "1 div b = a" by simp
  from assms have "a dvd c" ..
  then obtain d where "c = a * d" ..
  with \<open>a \<noteq> 0\<close> \<open>a * b = 1\<close> show "c div a = c * b"
    by (simp add: mult.assoc mult.left_commute [of a])
qed

lemma unit_prod [intro]: "is_unit a \ is_unit b \ is_unit (a * b)"
  by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono)

lemma is_unit_mult_iff: "is_unit (a * b) \ is_unit a \ is_unit b"
  by (auto dest: dvd_mult_left dvd_mult_right)

lemma unit_div [intro]: "is_unit a \ is_unit b \ is_unit (a div b)"
  by (erule is_unitE [of b a]) (simp add: ac_simps unit_prod)

lemma mult_unit_dvd_iff:
  assumes "is_unit b"
  shows "a * b dvd c \ a dvd c"
proof
  assume "a * b dvd c"
  with assms show "a dvd c"
    by (simp add: dvd_mult_left)
next
  assume "a dvd c"
  then obtain k where "c = a * k" ..
  with assms have "c = (a * b) * (1 div b * k)"
    by (simp add: mult_ac)
  then show "a * b dvd c" by (rule dvdI)
qed

lemma mult_unit_dvd_iff': "is_unit a \ (a * b) dvd c \ b dvd c"
  using mult_unit_dvd_iff [of a b c] by (simp add: ac_simps)

lemma dvd_mult_unit_iff:
  assumes "is_unit b"
  shows "a dvd c * b \ a dvd c"
proof
  assume "a dvd c * b"
  with assms have "c * b dvd c * (b * (1 div b))"
    by (subst mult_assoc [symmetric]) simp
  also from assms have "b * (1 div b) = 1"
    by (rule is_unitE) simp
  finally have "c * b dvd c" by simp
  with \<open>a dvd c * b\<close> show "a dvd c" by (rule dvd_trans)
next
  assume "a dvd c"
  then show "a dvd c * b" by simp
qed

lemma dvd_mult_unit_iff': "is_unit b \ a dvd b * c \ a dvd c"
  using dvd_mult_unit_iff [of b a c] by (simp add: ac_simps)

lemma div_unit_dvd_iff: "is_unit b \ a div b dvd c \ a dvd c"
  by (erule is_unitE [of _ a]) (auto simp add: mult_unit_dvd_iff)

lemma dvd_div_unit_iff: "is_unit b \ a dvd c div b \ a dvd c"
  by (erule is_unitE [of _ c]) (simp add: dvd_mult_unit_iff)

lemmas unit_dvd_iff = mult_unit_dvd_iff mult_unit_dvd_iff'
  dvd_mult_unit_iff dvd_mult_unit_iff'
  div_unit_dvd_iff dvd_div_unit_iff (* FIXME consider named_theorems *)

lemma unit_mult_div_div [simp]: "is_unit a \ b * (1 div a) = b div a"
  by (erule is_unitE [of _ b]) simp

lemma unit_div_mult_self [simp]: "is_unit a \ b div a * a = b"
  by (rule dvd_div_mult_self) auto

lemma unit_div_1_div_1 [simp]: "is_unit a \ 1 div (1 div a) = a"
  by (erule is_unitE) simp

lemma unit_div_mult_swap: "is_unit c \ a * (b div c) = (a * b) div c"
  by (erule unit_dvdE [of _ b]) (simp add: mult.left_commute [of _ c])

lemma unit_div_commute: "is_unit b \ (a div b) * c = (a * c) div b"
  using unit_div_mult_swap [of b c a] by (simp add: ac_simps)

lemma unit_eq_div1: "is_unit b \ a div b = c \ a = c * b"
  by (auto elim: is_unitE)

lemma unit_eq_div2: "is_unit b \ a = c div b \ a * b = c"
  using unit_eq_div1 [of b c a] by auto

lemma unit_mult_left_cancel: "is_unit a \ a * b = a * c \ b = c"
  using mult_cancel_left [of a b c] by auto

lemma unit_mult_right_cancel: "is_unit a \ b * a = c * a \ b = c"
  using unit_mult_left_cancel [of a b c] by (auto simp add: ac_simps)

lemma unit_div_cancel:
  assumes "is_unit a"
  shows "b div a = c div a \ b = c"
proof -
  from assms have "is_unit (1 div a)" by simp
  then have "b * (1 div a) = c * (1 div a) \ b = c"
    by (rule unit_mult_right_cancel)
  with assms show ?thesis by simp
qed

lemma is_unit_div_mult2_eq:
  assumes "is_unit b" and "is_unit c"
  shows "a div (b * c) = a div b div c"
proof -
  from assms have "is_unit (b * c)"
    by (simp add: unit_prod)
  then have "b * c dvd a"
    by (rule unit_imp_dvd)
  then show ?thesis
    by (rule dvd_div_mult2_eq)
qed

lemma is_unit_div_mult_cancel_left:
  assumes "a \ 0" and "is_unit b"
  shows "a div (a * b) = 1 div b"
proof -
  from assms have "a div (a * b) = a div a div b"
    by (simp add: mult_unit_dvd_iff dvd_div_mult2_eq)
  with assms show ?thesis by simp
qed

lemma is_unit_div_mult_cancel_right:
  assumes "a \ 0" and "is_unit b"
  shows "a div (b * a) = 1 div b"
  using assms is_unit_div_mult_cancel_left [of a b] by (simp add: ac_simps)

lemma unit_div_eq_0_iff:
  assumes "is_unit b"
  shows "a div b = 0 \ a = 0"
  using assms by (simp add: dvd_div_eq_0_iff unit_imp_dvd)

lemma div_mult_unit2:
  "is_unit c \ b dvd a \ a div (b * c) = a div b div c"
  by (rule dvd_div_mult2_eq) (simp_all add: mult_unit_dvd_iff)

text \<open>Coprimality\<close>

definition coprime :: "'a \ 'a \ bool"
  where "coprime a b \ (\c. c dvd a \ c dvd b \ is_unit c)"

lemma coprimeI:
  assumes "\c. c dvd a \ c dvd b \ is_unit c"
  shows "coprime a b"
  using assms by (auto simp: coprime_def)

lemma not_coprimeI:
  assumes "c dvd a" and "c dvd b" and "\ is_unit c"
  shows "\ coprime a b"
  using assms by (auto simp: coprime_def)

lemma coprime_common_divisor:
  "is_unit c" if "coprime a b" and "c dvd a" and "c dvd b"
  using that by (auto simp: coprime_def)

lemma not_coprimeE:
  assumes "\ coprime a b"
  obtains c where "c dvd a" and "c dvd b" and "\ is_unit c"
  using assms by (auto simp: coprime_def)

lemma coprime_imp_coprime:
  "coprime a b" if "coprime c d"
    and "\e. \ is_unit e \ e dvd a \ e dvd b \ e dvd c"
    and "\e. \ is_unit e \ e dvd a \ e dvd b \ e dvd d"
proof (rule coprimeI)
  fix e
  assume "e dvd a" and "e dvd b"
  with that have "e dvd c" and "e dvd d"
    by (auto intro: dvd_trans)
  with \<open>coprime c d\<close> show "is_unit e"
    by (rule coprime_common_divisor)
qed

lemma coprime_divisors:
  "coprime a b" if "a dvd c" "b dvd d" and "coprime c d"
using \<open>coprime c d\<close> proof (rule coprime_imp_coprime)
  fix e
  assume "e dvd a" then show "e dvd c"
    using \<open>a dvd c\<close> by (rule dvd_trans)
  assume "e dvd b" then show "e dvd d"
    using \<open>b dvd d\<close> by (rule dvd_trans)
qed

lemma coprime_self [simp]:
  "coprime a a \ is_unit a" (is "?P \ ?Q")
proof
  assume ?P
  then show ?Q
    by (rule coprime_common_divisor) simp_all
next
  assume ?Q
  show ?P
    by (rule coprimeI) (erule dvd_unit_imp_unit, rule \<open>?Q\<close>)
qed

lemma coprime_commute [ac_simps]:
  "coprime b a \ coprime a b"
  unfolding coprime_def by auto

lemma is_unit_left_imp_coprime:
  "coprime a b" if "is_unit a"
proof (rule coprimeI)
  fix c
  assume "c dvd a"
  with that show "is_unit c"
    by (auto intro: dvd_unit_imp_unit)
qed

lemma is_unit_right_imp_coprime:
  "coprime a b" if "is_unit b"
  using that is_unit_left_imp_coprime [of b a] by (simp add: ac_simps)

lemma coprime_1_left [simp]:
  "coprime 1 a"
  by (rule coprimeI)

lemma coprime_1_right [simp]:
  "coprime a 1"
  by (rule coprimeI)

lemma coprime_0_left_iff [simp]:
  "coprime 0 a \ is_unit a"
  by (auto intro: coprimeI dvd_unit_imp_unit coprime_common_divisor [of 0 a a])

lemma coprime_0_right_iff [simp]:
  "coprime a 0 \ is_unit a"
  using coprime_0_left_iff [of a] by (simp add: ac_simps)

lemma coprime_mult_self_left_iff [simp]:
  "coprime (c * a) (c * b) \ is_unit c \ coprime a b"
  by (auto intro: coprime_common_divisor)
    (rule coprimeI, auto intro: coprime_common_divisor simp add: dvd_mult_unit_iff')+

lemma coprime_mult_self_right_iff [simp]:
  "coprime (a * c) (b * c) \ is_unit c \ coprime a b"
  using coprime_mult_self_left_iff [of c a b] by (simp add: ac_simps)

lemma coprime_absorb_left:
  assumes "x dvd y"
  shows   "coprime x y \ is_unit x"
  using assms coprime_common_divisor is_unit_left_imp_coprime by auto

lemma coprime_absorb_right:
  assumes "y dvd x"
  shows   "coprime x y \ is_unit y"
  using assms coprime_common_divisor is_unit_right_imp_coprime by auto

end

class unit_factor =
  fixes unit_factor :: "'a \ 'a"

class semidom_divide_unit_factor = semidom_divide + unit_factor +
  assumes unit_factor_0 [simp]: "unit_factor 0 = 0"
    and is_unit_unit_factor: "a dvd 1 \ unit_factor a = a"
    and unit_factor_is_unit: "a \ 0 \ unit_factor a dvd 1"
    and unit_factor_mult_unit_left: "a dvd 1 \ unit_factor (a * b) = a * unit_factor b"
  \<comment> \<open>This fine-grained hierarchy will later on allow lean normalization of polynomials\<close>
begin

lemma unit_factor_mult_unit_right: "a dvd 1 \ unit_factor (b * a) = unit_factor b * a"
  using unit_factor_mult_unit_left[of a b] by (simp add: mult_ac)

lemmas [simp] = unit_factor_mult_unit_left unit_factor_mult_unit_right

end

class normalization_semidom = algebraic_semidom + semidom_divide_unit_factor +
  fixes normalize :: "'a \ 'a"
  assumes unit_factor_mult_normalize [simp]: "unit_factor a * normalize a = a"
    and normalize_0 [simp]: "normalize 0 = 0"
begin

text \<open>
  Class \<^class>\<open>normalization_semidom\<close> cultivates the idea that each integral
  domain can be split into equivalence classes whose representants are
  associated, i.e. divide each other. \<^const>\<open>normalize\<close> specifies a canonical
  representant for each equivalence class. The rationale behind this is that
  it is easier to reason about equality than equivalences, hence we prefer to
  think about equality of normalized values rather than associated elements.
\<close>

declare unit_factor_is_unit [iff]

lemma unit_factor_dvd [simp]: "a \ 0 \ unit_factor a dvd b"
  by (rule unit_imp_dvd) simp

lemma unit_factor_self [simp]: "unit_factor a dvd a"
  by (cases "a = 0") simp_all

lemma normalize_mult_unit_factor [simp]: "normalize a * unit_factor a = a"
  using unit_factor_mult_normalize [of a] by (simp add: ac_simps)

lemma normalize_eq_0_iff [simp]: "normalize a = 0 \ a = 0"
  (is "?lhs \ ?rhs")
proof
  assume ?lhs
  moreover have "unit_factor a * normalize a = a" by simp
  ultimately show ?rhs by simp
next
  assume ?rhs
  then show ?lhs by simp
qed

lemma unit_factor_eq_0_iff [simp]: "unit_factor a = 0 \ a = 0"
  (is "?lhs \ ?rhs")
proof
  assume ?lhs
  moreover have "unit_factor a * normalize a = a" by simp
  ultimately show ?rhs by simp
next
  assume ?rhs
  then show ?lhs by simp
qed

lemma div_unit_factor [simp]: "a div unit_factor a = normalize a"
proof (cases "a = 0")
  case True
  then show ?thesis by simp
next
  case False
  then have "unit_factor a \ 0"
    by simp
  with nonzero_mult_div_cancel_left
  have "unit_factor a * normalize a div unit_factor a = normalize a"
    by blast
  then show ?thesis by simp
qed

lemma normalize_div [simp]: "normalize a div a = 1 div unit_factor a"
proof (cases "a = 0")
  case True
  then show ?thesis by simp
next
  case False
  have "normalize a div a = normalize a div (unit_factor a * normalize a)"
    by simp
  also have "\ = 1 div unit_factor a"
    using False by (subst is_unit_div_mult_cancel_right) simp_all
  finally show ?thesis .
qed

lemma is_unit_normalize:
  assumes "is_unit a"
  shows "normalize a = 1"
proof -
  from assms have "unit_factor a = a"
    by (rule is_unit_unit_factor)
  moreover from assms have "a \ 0"
    by auto
  moreover have "normalize a = a div unit_factor a"
    by simp
  ultimately show ?thesis
    by simp
qed

lemma unit_factor_1 [simp]: "unit_factor 1 = 1"
  by (rule is_unit_unit_factor) simp

lemma normalize_1 [simp]: "normalize 1 = 1"
  by (rule is_unit_normalize) simp

lemma normalize_1_iff: "normalize a = 1 \ is_unit a"
  (is "?lhs \ ?rhs")
proof
  assume ?rhs
  then show ?lhs by (rule is_unit_normalize)
next
  assume ?lhs
  then have "unit_factor a * normalize a = unit_factor a * 1"
    by simp
  then have "unit_factor a = a"
    by simp
  moreover
  from \<open>?lhs\<close> have "a \<noteq> 0" by auto
  then have "is_unit (unit_factor a)" by simp
  ultimately show ?rhs by simp
qed

lemma div_normalize [simp]: "a div normalize a = unit_factor a"
proof (cases "a = 0")
  case True
  then show ?thesis by simp
next
  case False
  then have "normalize a \ 0" by simp
  with nonzero_mult_div_cancel_right
  have "unit_factor a * normalize a div normalize a = unit_factor a" by blast
  then show ?thesis by simp
qed

lemma mult_one_div_unit_factor [simp]: "a * (1 div unit_factor b) = a div unit_factor b"
  by (cases "b = 0") simp_all

lemma inv_unit_factor_eq_0_iff [simp]:
  "1 div unit_factor a = 0 \ a = 0"
  (is "?lhs \ ?rhs")
proof
  assume ?lhs
  then have "a * (1 div unit_factor a) = a * 0"
    by simp
  then show ?rhs
    by simp
next
  assume ?rhs
  then show ?lhs by simp
qed

lemma unit_factor_idem [simp]: "unit_factor (unit_factor a) = unit_factor a"
  by (cases "a = 0") (auto intro: is_unit_unit_factor)

lemma normalize_unit_factor [simp]: "a \ 0 \ normalize (unit_factor a) = 1"
  by (rule is_unit_normalize) simp

lemma normalize_mult_unit_left [simp]:
  assumes "a dvd 1"
  shows   "normalize (a * b) = normalize b"
proof (cases "b = 0")
  case False
  have "a * unit_factor b * normalize (a * b) = unit_factor (a * b) * normalize (a * b)"
    using assms by (subst unit_factor_mult_unit_left) auto
  also have "\ = a * b" by simp
  also have "b = unit_factor b * normalize b" by simp
  hence "a * b = a * unit_factor b * normalize b"
    by (simp only: mult_ac)
  finally show ?thesis
    using assms False by auto
qed auto

lemma normalize_mult_unit_right [simp]:
  assumes "b dvd 1"
  shows   "normalize (a * b) = normalize a"
  using assms by (subst mult.commute) auto

lemma normalize_idem [simp]: "normalize (normalize a) = normalize a"
proof (cases "a = 0")
  case False
  have "normalize a = normalize (unit_factor a * normalize a)"
    by simp
  also from False have "\ = normalize (normalize a)"
    by (subst normalize_mult_unit_left) auto
  finally show ?thesis ..
qed auto

lemma unit_factor_normalize [simp]:
  assumes "a \ 0"
  shows "unit_factor (normalize a) = 1"
proof -
  from assms have *: "normalize a \ 0"
    by simp
  have "unit_factor (normalize a) * normalize (normalize a) = normalize a"
    by (simp only: unit_factor_mult_normalize)
  then have "unit_factor (normalize a) * normalize a = normalize a"
    by simp
  with * have "unit_factor (normalize a) * normalize a div normalize a = normalize a div normalize a"
    by simp
  with * show ?thesis
    by simp
qed

lemma normalize_dvd_iff [simp]: "normalize a dvd b \ a dvd b"
proof -
  have "normalize a dvd b \ unit_factor a * normalize a dvd b"
    using mult_unit_dvd_iff [of "unit_factor a" "normalize a" b]
      by (cases "a = 0") simp_all
  then show ?thesis by simp
qed

lemma dvd_normalize_iff [simp]: "a dvd normalize b \ a dvd b"
proof -
  have "a dvd normalize b \ a dvd normalize b * unit_factor b"
    using dvd_mult_unit_iff [of "unit_factor b" a "normalize b"]
      by (cases "b = 0") simp_all
  then show ?thesis by simp
qed

lemma normalize_idem_imp_unit_factor_eq:
  assumes "normalize a = a"
  shows "unit_factor a = of_bool (a \ 0)"
proof (cases "a = 0")
  case True
  then show ?thesis
    by simp
next
  case False
  then show ?thesis
    using assms unit_factor_normalize [of a] by simp
qed

lemma normalize_idem_imp_is_unit_iff:
  assumes "normalize a = a"
  shows "is_unit a \ a = 1"
  using assms by (cases "a = 0") (auto dest: is_unit_normalize)

lemma coprime_normalize_left_iff [simp]:
  "coprime (normalize a) b \ coprime a b"
  by (rule iffI; rule coprimeI) (auto intro: coprime_common_divisor)

lemma coprime_normalize_right_iff [simp]:
  "coprime a (normalize b) \ coprime a b"
  using coprime_normalize_left_iff [of b a] by (simp add: ac_simps)

text \<open>
  We avoid an explicit definition of associated elements but prefer explicit
  normalisation instead. In theory we could define an abbreviation like \<^prop>\<open>associated a b \<longleftrightarrow> normalize a = normalize b\<close> but this is counterproductive
  without suggestive infix syntax, which we do not want to sacrifice for this
  purpose here.
\<close>

lemma associatedI:
  assumes "a dvd b" and "b dvd a"
  shows "normalize a = normalize b"
proof (cases "a = 0 \ b = 0")
  case True
  with assms show ?thesis by auto
next
  case False
  from \<open>a dvd b\<close> obtain c where b: "b = a * c" ..
  moreover from \<open>b dvd a\<close> obtain d where a: "a = b * d" ..
  ultimately have "b * 1 = b * (c * d)"
    by (simp add: ac_simps)
  with False have "1 = c * d"
    unfolding mult_cancel_left by simp
  then have "is_unit c" and "is_unit d"
    by auto
  with a b show ?thesis
    by (simp add: is_unit_normalize)
qed

lemma associatedD1: "normalize a = normalize b \ a dvd b"
  using dvd_normalize_iff [of _ b, symmetric] normalize_dvd_iff [of a _, symmetric]
  by simp

lemma associatedD2: "normalize a = normalize b \ b dvd a"
  using dvd_normalize_iff [of _ a, symmetric] normalize_dvd_iff [of b _, symmetric]
  by simp

lemma associated_unit: "normalize a = normalize b \ is_unit a \ is_unit b"
  using dvd_unit_imp_unit by (auto dest!: associatedD1 associatedD2)

lemma associated_iff_dvd: "normalize a = normalize b \ a dvd b \ b dvd a"
  (is "?lhs \ ?rhs")
proof
  assume ?rhs
  then show ?lhs by (auto intro!: associatedI)
next
  assume ?lhs
  then have "unit_factor a * normalize a = unit_factor a * normalize b"
    by simp
  then have *: "normalize b * unit_factor a = a"
    by (simp add: ac_simps)
  show ?rhs
  proof (cases "a = 0 \ b = 0")
    case True
    with \<open>?lhs\<close> show ?thesis by auto
  next
    case False
    then have "b dvd normalize b * unit_factor a" and "normalize b * unit_factor a dvd b"
      by (simp_all add: mult_unit_dvd_iff dvd_mult_unit_iff)
    with * show ?thesis by simp
  qed
qed

lemma associated_eqI:
  assumes "a dvd b" and "b dvd a"
  assumes "normalize a = a" and "normalize b = b"
  shows "a = b"
proof -
  from assms have "normalize a = normalize b"
    unfolding associated_iff_dvd by simp
  with \<open>normalize a = a\<close> have "a = normalize b"
    by simp
  with \<open>normalize b = b\<close> show "a = b"
    by simp
qed

lemma normalize_unit_factor_eqI:
  assumes "normalize a = normalize b"
    and "unit_factor a = unit_factor b"
  shows "a = b"
proof -
  from assms have "unit_factor a * normalize a = unit_factor b * normalize b"
    by simp
  then show ?thesis
    by simp
qed

lemma normalize_mult_normalize_left [simp]: "normalize (normalize a * b) = normalize (a * b)"
  by (rule associated_eqI) (auto intro!: mult_dvd_mono)

lemma normalize_mult_normalize_right [simp]: "normalize (a * normalize b) = normalize (a * b)"
  by (rule associated_eqI) (auto intro!: mult_dvd_mono)

end

class normalization_semidom_multiplicative = normalization_semidom +
  assumes unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
begin

lemma normalize_mult: "normalize (a * b) = normalize a * normalize b"
proof (cases "a = 0 \ b = 0")
  case True
  then show ?thesis by auto
next
  case False
  have "unit_factor (a * b) * normalize (a * b) = a * b"
    by (rule unit_factor_mult_normalize)
  then have "normalize (a * b) = a * b div unit_factor (a * b)"
    by simp
  also have "\ = a * b div unit_factor (b * a)"
    by (simp add: ac_simps)
  also have "\ = a * b div unit_factor b div unit_factor a"
    using False by (simp add: unit_factor_mult is_unit_div_mult2_eq [symmetric])
  also have "\ = a * (b div unit_factor b) div unit_factor a"
    using False by (subst unit_div_mult_swap) simp_all
  also have "\ = normalize a * normalize b"
    using False
    by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric])
  finally show ?thesis .
qed

lemma dvd_unit_factor_div:
  assumes "b dvd a"
  shows "unit_factor (a div b) = unit_factor a div unit_factor b"
proof -
  from assms have "a = a div b * b"
    by simp
  then have "unit_factor a = unit_factor (a div b * b)"
    by simp
  then show ?thesis
    by (cases "b = 0") (simp_all add: unit_factor_mult)
qed

lemma dvd_normalize_div:
  assumes "b dvd a"
  shows "normalize (a div b) = normalize a div normalize b"
proof -
  from assms have "a = a div b * b"
    by simp
  then have "normalize a = normalize (a div b * b)"
    by simp
  then show ?thesis
    by (cases "b = 0") (simp_all add: normalize_mult)
qed

end

text \<open>Syntactic division remainder operator\<close>

class modulo = dvd + divide +
  fixes modulo :: "'a \ 'a \ 'a" (infixl \mod\ 70)

text \<open>Arbitrary quotient and remainder partitions\<close>

class semiring_modulo = comm_semiring_1_cancel + divide + modulo +
  assumes div_mult_mod_eq: \<open>a div b * b + a mod b = a\<close>
begin

lemma mod_div_decomp:
  fixes a b
  obtains q r where "q = a div b" and "r = a mod b"
    and "a = q * b + r"
proof -
  from div_mult_mod_eq have "a = a div b * b + a mod b" by simp
  moreover have "a div b = a div b" ..
  moreover have "a mod b = a mod b" ..
  note that ultimately show thesis by blast
qed

lemma mult_div_mod_eq: "b * (a div b) + a mod b = a"
  using div_mult_mod_eq [of a b] by (simp add: ac_simps)

lemma mod_div_mult_eq: "a mod b + a div b * b = a"
  using div_mult_mod_eq [of a b] by (simp add: ac_simps)

lemma mod_mult_div_eq: "a mod b + b * (a div b) = a"
  using div_mult_mod_eq [of a b] by (simp add: ac_simps)

lemma minus_div_mult_eq_mod: "a - a div b * b = a mod b"
  by (rule add_implies_diff [symmetric]) (fact mod_div_mult_eq)

lemma minus_mult_div_eq_mod: "a - b * (a div b) = a mod b"
  by (rule add_implies_diff [symmetric]) (fact mod_mult_div_eq)

lemma minus_mod_eq_div_mult: "a - a mod b = a div b * b"
  by (rule add_implies_diff [symmetric]) (fact div_mult_mod_eq)

lemma minus_mod_eq_mult_div: "a - a mod b = b * (a div b)"
  by (rule add_implies_diff [symmetric]) (fact mult_div_mod_eq)

lemma mod_0_imp_dvd [dest!]:
  "b dvd a" if "a mod b = 0"
proof -
  have "b dvd (a div b) * b" by simp
  also have "(a div b) * b = a"
    using div_mult_mod_eq [of a b] by (simp add: that)
  finally show ?thesis .
qed

lemma [nitpick_unfold]:
  "a mod b = a - a div b * b"
  by (fact minus_div_mult_eq_mod [symmetric])

end

class semiring_modulo_trivial = semiring_modulo + divide_trivial
begin

lemma mod_0 [simp]:
  \<open>0 mod a = 0\<close>
  using div_mult_mod_eq [of 0 a] by simp

lemma mod_by_0 [simp]:
  \<open>a mod 0 = a\<close>
  using div_mult_mod_eq [of a 0] by simp

lemma mod_by_1 [simp]:
  \<open>a mod 1 = 0\<close>
proof -
  have \<open>a + a mod 1 = a\<close>
    using div_mult_mod_eq [of a 1] by simp
  then have \<open>a + a mod 1 = a + 0\<close>
    by simp
  then show ?thesis
    by (rule add_left_imp_eq)
qed

end

subsection \<open>Quotient and remainder in integral domains\<close>

class semidom_modulo = algebraic_semidom + semiring_modulo
begin

subclass semiring_modulo_trivial ..

lemma mod_self [simp]:
  "a mod a = 0"
  using div_mult_mod_eq [of a a] by simp

lemma dvd_imp_mod_0 [simp]:
  "b mod a = 0" if "a dvd b"
  using that minus_div_mult_eq_mod [of b a] by simp

lemma mod_eq_0_iff_dvd:
  "a mod b = 0 \ b dvd a"
  by (auto intro: mod_0_imp_dvd)

lemma dvd_eq_mod_eq_0 [nitpick_unfold, code]:
  "a dvd b \ b mod a = 0"
  by (simp add: mod_eq_0_iff_dvd)

lemma dvd_mod_iff:
  assumes "c dvd b"
  shows "c dvd a mod b \ c dvd a"
proof -
  from assms have "(c dvd a mod b) \ (c dvd ((a div b) * b + a mod b))"
    by (simp add: dvd_add_right_iff)
  also have "(a div b) * b + a mod b = a"
    using div_mult_mod_eq [of a b] by simp
  finally show ?thesis .
qed

lemma dvd_mod_imp_dvd:
  assumes "c dvd a mod b" and "c dvd b"
  shows "c dvd a"
  using assms dvd_mod_iff [of c b a] by simp

lemma dvd_minus_mod [simp]:
  "b dvd a - a mod b"
  by (simp add: minus_mod_eq_div_mult)

lemma cancel_div_mod_rules:
  "((a div b) * b + a mod b) + c = a + c"
  "(b * (a div b) + a mod b) + c = a + c"
  by (simp_all add: div_mult_mod_eq mult_div_mod_eq)

end

class idom_modulo = idom + semidom_modulo
begin

subclass idom_divide ..

lemma div_diff [simp]:
  "c dvd a \ c dvd b \ (a - b) div c = a div c - b div c"
  using div_add [of _  _ "- b"] by (simp add: dvd_neg_div)

end

subsection \<open>Interlude: basic tool support for algebraic and arithmetic calculations\<close>

named_theorems arith "arith facts -- only ground formulas"
ML_file \<open>Tools/arith_data.ML\<close>

ML_file \<open>~~/src/Provers/Arith/cancel_div_mod.ML\<close>

ML \<open>
structure Cancel_Div_Mod_Ring = Cancel_Div_Mod
(
  val div_name = \<^const_name>\<open>divide\<close>;
  val mod_name = \<^const_name>\<open>modulo\<close>;
  val mk_binop = HOLogic.mk_binop;
  val mk_sum = Arith_Data.mk_sum;
  val dest_sum = Arith_Data.dest_sum;

  val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};

  val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
    @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps})
)
\<close>

simproc_setup cancel_div_mod_int ("(a::'a::semidom_modulo) + b") =
  \<open>K Cancel_Div_Mod_Ring.proc\<close>

subsection \<open>Ordered semirings and rings\<close>

text \<open>
  The theory of partially ordered rings 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_semiring = semiring + ordered_comm_monoid_add +
  assumes mult_left_mono: "a \ b \ 0 \ c \ c * a \ c * b"
  assumes mult_right_mono: "a \ b \ 0 \ c \ a * c \ b * c"
begin

lemma mult_mono: "a \ b \ c \ d \ 0 \ b \ 0 \ c \ a * c \ b * d"
  apply (erule (1) mult_right_mono [THEN order_trans])
  apply (erule (1) mult_left_mono)
  done

lemma mult_mono': "a \ b \ c \ d \ 0 \ a \ 0 \ c \ a * c \ b * d"
  by (rule mult_mono) (fast intro: order_trans)+

end

lemma mono_mult:
  fixes a :: "'a::ordered_semiring"
  shows "a \ 0 \ mono ((*) a)"
  by (simp add: mono_def mult_left_mono)

class ordered_semiring_0 = semiring_0 + ordered_semiring
begin

lemma mult_nonneg_nonneg [simp]: "0 \ a \ 0 \ b \ 0 \ a * b"
  using mult_left_mono [of 0 b a] by simp

lemma mult_nonneg_nonpos: "0 \ a \ b \ 0 \ a * b \ 0"
  using mult_left_mono [of b 0 a] by simp

lemma mult_nonpos_nonneg: "a \ 0 \ 0 \ b \ a * b \ 0"
  using mult_right_mono [of a 0 b] by simp

text \<open>Legacy -- use @{thm [source] mult_nonpos_nonneg}.\<close>
lemma mult_nonneg_nonpos2: "0 \ a \ b \ 0 \ b * a \ 0"
  by (drule mult_right_mono [of b 0]) auto

lemma split_mult_neg_le: "(0 \ a \ b \ 0) \ (a \ 0 \ 0 \ b) \ a * b \ 0"
  by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)

end

class zero_less_one = order + zero + one +
  assumes zero_less_one [simp]: "0 < 1"
begin

subclass zero_neq_one
  by standard (simp add: less_imp_neq)

lemma zero_le_one [simp]:
  \<open>0 \<le> 1\<close> by (rule less_imp_le) simp

end

class ordered_semiring_1 = ordered_semiring_0 + semiring_1 + zero_less_one
begin

lemma convex_bound_le:
  assumes "x \ a" and "y \ a" and "0 \ u" and "0 \ v" and "u + v = 1"
  shows "u * x + v * y \ a"
proof-
  from assms have "u * x + v * y \ u * a + v * a"
    by (simp add: add_mono mult_left_mono)
  with assms show ?thesis
    unfolding distrib_right[symmetric] by simp
qed

end

class ordered_cancel_semiring = ordered_semiring + cancel_comm_monoid_add
begin

subclass semiring_0_cancel ..

subclass ordered_semiring_0 ..

subclass ordered_cancel_ab_semigroup_add ..

end

class linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_add
begin

subclass ordered_cancel_semiring ..

subclass ordered_cancel_comm_monoid_add ..

subclass ordered_ab_semigroup_monoid_add_imp_le ..

lemma mult_left_less_imp_less: "c * a < c * b \ 0 \ c \ a < b"
  by (force simp add: mult_left_mono not_le [symmetric])

lemma mult_right_less_imp_less: "a * c < b * c \ 0 \ c \ a < b"
  by (force simp add: mult_right_mono not_le [symmetric])

end

class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add +
  assumes mult_strict_left_mono: "a < b \ 0 < c \ c * a < c * b"
  assumes mult_strict_right_mono: "a < b \ 0 < c \ a * c < b * c"
begin

subclass semiring_0_cancel ..

subclass ordered_semiring
proof
  fix a b c :: 'a
  assume \<section>: "a \<le> b" "0 \<le> c"
  thus "c * a \ c * b"
    unfolding le_less
    using mult_strict_left_mono by (cases "c = 0") auto
  show "a * c \ b * c"
    using \<section> by (force simp: le_less intro: mult_strict_right_mono dest: sym)
qed

lemma mult_pos_pos[simp]: "0 < a \ 0 < b \ 0 < a * b"
  using mult_strict_left_mono [of 0 b a] by simp

lemma mult_pos_neg: "0 < a \ b < 0 \ a * b < 0"
  using mult_strict_left_mono [of b 0 a] by simp

lemma mult_neg_pos: "a < 0 \ 0 < b \ a * b < 0"
  using mult_strict_right_mono [of a 0 b] by simp

text \<open>Strict monotonicity in both arguments\<close>
lemma mult_strict_mono:
  assumes "a < b" "c < d" "0 < b" "0 \ c"
  shows "a * c < b * d"
proof-
  have "a * c \ b * c"
    using assms by (intro mult_right_mono) auto
  also have "... < b * d"
    using assms by (intro mult_strict_left_mono) auto
  finally show ?thesis .
qed

text \<open>This weaker variant has more natural premises\<close>
lemma mult_strict_mono':
  assumes "a < b" and "c < d" and "0 \ a" and "0 \ c"
  shows "a * c < b * d"
  using assms by (intro mult_strict_mono) auto

lemma mult_less_le_imp_less:
  assumes "a < b" "c \ d" "0 \ a" "0 < c"
  shows "a * c < b * d"
proof-
  have "a * c < b * c"
    using assms by (intro mult_strict_right_mono) auto
  also have "... \ b * d"
    using assms by (intro mult_left_mono) auto
  finally show ?thesis .
qed

lemma mult_le_less_imp_less:
  assumes "a \ b" and "c < d" and "0 < a" and "0 \ c"
  shows "a * c < b * d"
proof-
  have "a * c \ b * c"
    using assms by (intro mult_right_mono) auto
  also have "... < b * d"
    using assms by (intro mult_strict_left_mono) auto
  finally show ?thesis .
qed

end

class linordered_semiring_1 = linordered_semiring + semiring_1 + zero_less_one
begin

lemma convex_bound_le:
  assumes "x \ a" "y \ a" "0 \ u" "0 \ v" "u + v = 1"
  shows "u * x + v * y \ a"
proof-
  from assms have "u * x + v * y \ u * a + v * a"
    by (simp add: add_mono mult_left_mono)
  with assms show ?thesis
    unfolding distrib_right[symmetric] by simp
qed

end

subclass (in linordered_semiring_1) ordered_semiring_1 ..

class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add +
  assumes mult_strict_left_mono: "a < b \ 0 < c \ c * a < c * b"
  assumes mult_strict_right_mono: "a < b \ 0 < c \ a * c < b * c"
begin

subclass semiring_0_cancel ..

subclass linordered_semiring
proof
  fix a b c :: 'a
  assume *: "a \ b" "0 \ c"
  then show "c * a \ c * b"
    unfolding le_less
    using mult_strict_left_mono by (cases "c = 0") auto
  from * show "a * c \ b * c"
    unfolding le_less
    using mult_strict_right_mono by (cases "c = 0") auto
qed

subclass (in linordered_semiring_strict) ordered_semiring_strict
proof qed (auto simp: mult_strict_left_mono mult_strict_right_mono)

lemma mult_left_le_imp_le: "c * a \ c * b \ 0 < c \ a \ b"
  by (auto simp add: mult_strict_left_mono simp flip: not_less)

lemma mult_right_le_imp_le: "a * c \ b * c \ 0 < c \ a \ b"
  by (auto simp add: mult_strict_right_mono not_less [symmetric])

lemma zero_less_mult_pos:
  assumes "0 < a * b" "0 < a" shows "0 < b"
proof (cases "b \ 0")
  case True
  then show ?thesis
    using assms by (auto simp: le_less dest: less_not_sym mult_pos_neg [of a b])
qed (auto simp add: le_less not_less)

lemma zero_less_mult_pos2:
  assumes "0 < b * a" "0 < a" shows "0 < b"
proof (cases "b \ 0")
  case True
  then show ?thesis
    using assms by (auto simp: le_less dest: less_not_sym mult_neg_pos)
qed (auto simp add: le_less not_less)

end

class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1 + zero_less_one
begin

subclass linordered_semiring_1 ..

lemma convex_bound_lt:
  assumes "x < a" "y < a" "0 \ u" "0 \ v" "u + v = 1"
  shows "u * x + v * y < a"
proof -
  from assms have "u * x + v * y < u * a + v * a"
    by (cases "u = 0") (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono)
  with assms show ?thesis
    unfolding distrib_right[symmetric] by simp
qed

end

class ordered_semiring_1_strict = ordered_semiring_strict + semiring_1 + zero_less_one
  \<comment> \<open>analogous to \<^class>\<open>linordered_semiring_1_strict\<close> not requiring a total order\<close>
begin

subclass ordered_semiring_1 ..

lemma convex_bound_lt:
  assumes "x < a" and "y < a" and "0 \ u" and "0 \ v" and "u + v = 1"
  shows "u * x + v * y < a"
proof -
  from assms have "u * x + v * y < u * a + v * a"
--> --------------------

--> maximum size reached

--> --------------------

quality100%

¤ Dauer der Verarbeitung: 0.42 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.