Theory Missing_Unsorted

(*  
    Author:      René Thiemann 
                 Akihisa Yamada
                 Jose Divason
    License:     BSD
*)
section ‹Missing Unsorted›

text ‹This theory contains several lemmas which might be of interest to the Isabelle distribution.
  For instance, we prove that $b^n \cdot n^k$ is bounded by a constant whenever $0 < b < 1$.›

theory Missing_Unsorted
imports
  HOL.Complex "HOL-Computational_Algebra.Factorial_Ring"
begin

lemma bernoulli_inequality: assumes x: "-1 ≤ (x :: 'a :: linordered_field)"
  shows "1 + of_nat n * x ≤ (1 + x) ^ n"
proof (induct n)
  case (Suc n)
  have "1 + of_nat (Suc n) * x = 1 + x + of_nat n * x" by (simp add: field_simps)
  also have "… ≤ … + of_nat n * x ^ 2" by simp
  also have "… = (1 + of_nat n * x) * (1 + x)" by (simp add: field_simps power2_eq_square)
  also have "… ≤ (1 + x) ^ n * (1 + x)"
    by (rule mult_right_mono[OF Suc], insert x, auto)
  also have "… = (1 + x) ^ (Suc n)" by simp
  finally show ?case .
qed simp

context
  fixes b :: "'a :: archimedean_field"
  assumes b: "0 < b" "b < 1"
begin
private lemma pow_one: "b ^ x ≤ 1" using power_Suc_less_one[OF b, of "x - 1"] by (cases x, auto)

private lemma pow_zero: "0 < b ^ x" using b(1) by simp

lemma exp_tends_to_zero: assumes c: "c > 0"
  shows "∃ x. b ^ x ≤ c" 
proof (rule ccontr)
  assume not: "¬ ?thesis"
  define bb where "bb = inverse b"
  define cc where "cc = inverse c"
  from b have bb: "bb > 1" unfolding bb_def by (rule one_less_inverse)  
  from c have cc: "cc > 0" unfolding cc_def by simp
  define bbb where "bbb = bb - 1"
  have id: "bb = 1 + bbb" and bbb: "bbb > 0" and bm1: "bbb ≥ -1" unfolding bbb_def using bb by auto
  have "∃ n. cc / bbb < of_nat n" by (rule reals_Archimedean2)
  then obtain n where lt: "cc / bbb < of_nat n" by auto
  from not have "¬ b ^ n ≤ c" by auto
  hence bnc: "b ^ n > c" by simp
  have "bb ^ n = inverse (b ^ n)" unfolding bb_def by (rule power_inverse)
  also have "… < cc" unfolding cc_def
    by (rule less_imp_inverse_less[OF bnc c])
  also have "… < bbb * of_nat n" using lt bbb by (metis mult.commute pos_divide_less_eq)
  also have "… ≤ bb ^ n"
    using bernoulli_inequality[OF bm1, folded id, of n] by (simp add: ac_simps)
  finally show False by simp
qed

lemma linear_exp_bound: "∃ p. ∀ x. b ^ x * of_nat x ≤ p"
proof -
  from b have "1 - b > 0" by simp
  from exp_tends_to_zero[OF this]
  obtain x0 where x0: "b ^ x0 ≤ 1 - b" ..
  {
    fix x
    assume "x ≥ x0"
    hence "∃ y. x = x0 + y" by arith
    then obtain y where x: "x = x0 + y" by auto
    have "b ^ x = b ^ x0 * b ^ y" unfolding x by (simp add: power_add)
    also have "… ≤ b ^ x0" using pow_one[of y] pow_zero[of x0] by auto
    also have "… ≤ 1 - b" by (rule x0)
    finally have "b ^ x ≤ 1 - b" .
  } note x0 = this
  define bs where "bs = insert 1 { b ^ Suc x * of_nat (Suc x) | x . x ≤ x0}"
  have bs: "finite bs" unfolding bs_def by auto
  define p where "p = Max bs"
  have bs: "⋀ b. b ∈ bs ⟹ b ≤ p" unfolding p_def using bs by simp
  hence p1: "p ≥ 1" unfolding bs_def by auto
  show ?thesis
  proof (rule exI[of _ p], intro allI)
    fix x
    show "b ^ x * of_nat x ≤ p"
    proof (induct x)
      case (Suc x)
      show ?case
      proof (cases "x ≤ x0")
        case True
        show ?thesis 
          by (rule bs, unfold bs_def, insert True, auto)
      next
        case False
        let ?x = "of_nat x :: 'a"
        have "b ^ (Suc x) * of_nat (Suc x) = b * (b ^ x * ?x) + b ^ Suc x" by (simp add: field_simps)
        also have "… ≤ b * p + b ^ Suc x"
          by (rule add_right_mono[OF mult_left_mono[OF Suc]], insert b, auto)
        also have "… = p - ((1 - b) * p - b ^ (Suc x))" by (simp add: field_simps)
        also have "… ≤ p - 0"
        proof -
          have "b ^ Suc x ≤ 1 - b" using x0[of "Suc x"] False by auto
          also have "… ≤ (1 - b) * p" using b p1 by auto
          finally show ?thesis
            by (intro diff_left_mono, simp)
        qed
        finally show ?thesis by simp
      qed
    qed (insert p1, auto)
  qed
qed

lemma poly_exp_bound: "∃ p. ∀ x. b ^ x * of_nat x ^ deg ≤ p" 
proof -
  show ?thesis
  proof (induct deg)
    case 0
    show ?case
      by (rule exI[of _ 1], intro allI, insert pow_one, auto)
  next
    case (Suc deg)
    then obtain q where IH: "⋀ x. b ^ x * (of_nat x) ^ deg ≤ q" by auto
    define p where "p = max 0 q"
    from IH have IH: "⋀ x. b ^ x * (of_nat x) ^ deg ≤ p" unfolding p_def using le_max_iff_disj by blast
    have p: "p ≥ 0" unfolding p_def by simp
    show ?case
    proof (cases "deg = 0")
      case True
      thus ?thesis using linear_exp_bound by simp
    next
      case False note deg = this
      define p' where "p' = p*p * 2 ^ Suc deg * inverse b"
      let ?f = "λ x. b ^ x * (of_nat x) ^ Suc deg"
      define f where "f = ?f"
      {
        fix x
        let ?x = "of_nat x :: 'a"
        have "f (2 * x) ≤ (2 ^ Suc deg) * (p * p)"
        proof (cases "x = 0")
          case False
          hence x1: "?x ≥ 1" by (cases x, auto)
          from x1 have x: "?x ^ (deg - 1) ≥ 1" by simp
          from x1 have xx: "?x ^ Suc deg ≥ 1" by (rule one_le_power)
          define c where "c = b ^ x * b ^ x * (2 ^ Suc deg)"
          have c: "c > 0" unfolding c_def using b by auto
          have "f (2 * x) = ?f (2 * x)" unfolding f_def by simp
          also have "b ^ (2 * x) = (b ^ x) * (b ^ x)" by (simp add: power2_eq_square power_even_eq)
          also have "of_nat (2 * x) = 2 * ?x" by simp
          also have "(2 * ?x) ^ Suc deg = 2 ^ Suc deg * ?x ^ Suc deg" by simp
          finally have "f (2 * x) = c * ?x ^ Suc deg" unfolding c_def by (simp add: ac_simps)
          also have "… ≤ c * ?x ^ Suc deg * ?x ^ (deg - 1)"
          proof -
            have "c * ?x ^ Suc deg > 0" using c xx by simp
            thus ?thesis unfolding mult_le_cancel_left1 using x by simp
          qed
          also have "… = c * ?x ^ (Suc deg + (deg - 1))" by (simp add: power_add)
          also have "Suc deg + (deg - 1) = deg + deg" using deg by simp
          also have "?x ^ (deg + deg) = (?x ^ deg) * (?x ^ deg)" by (simp add: power_add)
          also have "c * … = (2 ^ Suc deg) * ((b ^ x * ?x ^ deg) * (b ^ x * ?x ^ deg))" 
            unfolding c_def by (simp add: ac_simps)  
          also have "… ≤ (2 ^ Suc deg) * (p * p)"
            by (rule mult_left_mono[OF mult_mono[OF IH IH p]], insert pow_zero[of x], auto)
          finally show "f (2 * x) ≤ (2 ^ Suc deg) * (p * p)" .
        qed (auto simp: f_def)
        hence "?f (2 * x) ≤ (2 ^ Suc deg) * (p * p)" unfolding f_def .
      } note even = this
      show ?thesis
      proof (rule exI[of _ p'], intro allI)
        fix y
        show "?f y ≤ p'"
        proof (cases "even y")
          case True
          define x where "x = y div 2"
          have "y = 2 * x" unfolding x_def using True by simp
          from even[of x, folded this] have "?f y ≤ 2 ^ Suc deg * (p * p)" .
          also have "… ≤ … * inverse b"
            unfolding mult_le_cancel_left1 using b p
            by (simp add: algebra_split_simps one_le_inverse)
          also have "… = p'" unfolding p'_def by (simp add: ac_simps)
          finally show "?f y ≤ p'" .
        next
          case False
          define x where "x = y div 2"
          have "y = 2 * x + 1" unfolding x_def using False by simp
          hence "?f y = ?f (2 * x + 1)" by simp
          also have "… ≤ b ^ (2 * x + 1) * of_nat (2 * x + 2) ^ Suc deg"
            by (rule mult_left_mono[OF power_mono], insert b, auto) 
          also have "b ^ (2 * x + 1) = b ^ (2 * x + 2) * inverse b" using b by auto
          also have "b ^ (2 * x + 2) * inverse b * of_nat (2 * x + 2) ^ Suc deg = 
            inverse b * ?f (2 * (x + 1))" by (simp add: ac_simps)
          also have "… ≤ inverse b * ((2 ^ Suc deg) * (p * p))"
            by (rule mult_left_mono[OF even], insert b, auto)
          also have "… = p'" unfolding p'_def by (simp add: ac_simps)
          finally show "?f y ≤ p'" .
        qed
      qed
    qed
  qed
qed
end

lemma prod_list_replicate[simp]: "prod_list (replicate n a) = a ^ n"
  by (induct n, auto)

lemma prod_list_power: fixes xs :: "'a :: comm_monoid_mult list"
  shows "prod_list xs ^ n = (∏x←xs. x ^ n)"
  by (induct xs, auto simp: power_mult_distrib)

lemma set_upt_Suc: "{0 ..< Suc i} = insert i {0 ..< i}"
  by (fact atLeast0_lessThan_Suc)

lemma prod_pow[simp]: "(∏i = 0..<n. p) = (p :: 'a :: comm_monoid_mult) ^ n"
  by (induct n, auto simp: set_upt_Suc)


(* GCD and LCM part *)

lemma dvd_abs_mult_left_int [simp]:
  "¦a¦ * y dvd x ⟷ a * y dvd x" for x y a :: int
  using abs_dvd_iff [of "a * y"] abs_dvd_iff [of "¦a¦ * y"]
  by (simp add: abs_mult)
  
lemma gcd_abs_mult_right_int [simp]:
  "gcd x (¦a¦ * y) = gcd x (a * y)" for x y a :: int
  using gcd_abs2_int [of _ "a * y"] gcd_abs2_int [of _ "¦a¦ * y"]
  by (simp add: abs_mult)

lemma lcm_abs_mult_right_int [simp]:
  "lcm x (¦a¦ * y) = lcm x (a * y)" for x y a :: int
  using lcm_abs2_int [of _ "a * y"] lcm_abs2_int [of _ "¦a¦ * y"]
  by (simp add: abs_mult)

lemma gcd_abs_mult_left_int [simp]:
  "gcd x (a * ¦y¦) = gcd x (a * y)" for x y a :: int
  using gcd_abs2_int [of _ "a * ¦y¦"] gcd_abs2_int [of _ "a * y"]
  by (simp add: abs_mult)

lemma lcm_abs_mult_left_int [simp]:
  "lcm x (a * ¦y¦) = lcm x (a * y)" for x y a :: int
  using lcm_abs2_int [of _ "a * ¦y¦"] lcm_abs2_int [of _ "a * y"]
  by (simp add: abs_mult)


abbreviation (input) list_gcd :: "'a :: semiring_gcd list ⇒ 'a" where
  "list_gcd ≡ gcd_list"

abbreviation (input) list_lcm :: "'a :: semiring_gcd list ⇒ 'a" where
  "list_lcm ≡ lcm_list"


lemma list_gcd_simps: "list_gcd [] = 0" "list_gcd (x # xs) = gcd x (list_gcd xs)"
  by simp_all

lemma list_gcd: "x ∈ set xs ⟹ list_gcd xs dvd x"
  by (fact Gcd_fin_dvd)

lemma list_gcd_greatest: "(⋀ x. x ∈ set xs ⟹ y dvd x) ⟹ y dvd (list_gcd xs)"
  by (fact gcd_list_greatest)

lemma list_gcd_mult_int [simp]: 
  fixes xs :: "int list"
  shows "list_gcd (map (times a) xs) = ¦a¦ * list_gcd xs"
  by (simp add: Gcd_mult abs_mult)

lemma list_lcm_simps: "list_lcm [] = 1" "list_lcm (x # xs) = lcm x (list_lcm xs)"
  by simp_all

lemma list_lcm: "x ∈ set xs ⟹ x dvd list_lcm xs" 
  by (fact dvd_Lcm_fin)

lemma list_lcm_least: "(⋀ x. x ∈ set xs ⟹ x dvd y) ⟹ list_lcm xs dvd y"
  by (fact lcm_list_least)

lemma lcm_mult_distrib_nat: "(k :: nat) * lcm m n = lcm (k * m) (k * n)"
  by (simp add: lcm_mult_left)

lemma lcm_mult_distrib_int: "abs (k::int) * lcm m n = lcm (k * m) (k * n)"
  by (simp add: lcm_mult_left abs_mult)

lemma list_lcm_mult_int [simp]:
  fixes xs :: "int list"
  shows "list_lcm (map (times a) xs) = (if xs = [] then 1 else ¦a¦ * list_lcm xs)"
  by (simp add: Lcm_mult abs_mult)

lemma list_lcm_pos:
  "list_lcm xs ≥ (0 :: int)"
  "0 ∉ set xs ⟹ list_lcm xs ≠ 0"
  "0 ∉ set xs ⟹ list_lcm xs > 0" 
proof -
  have "0 ≤ ¦Lcm (set xs)¦"
    by (simp only: abs_ge_zero)
  then have "0 ≤ Lcm (set xs)"
    by simp
  then show "list_lcm xs ≥ 0"
    by simp
  assume "0 ∉ set xs"
  then show "list_lcm xs ≠ 0"
    by (simp add: Lcm_0_iff)
  with ‹list_lcm xs ≥ 0› show "list_lcm xs > 0"
    by (simp add: le_less)
qed

lemma quotient_of_nonzero: "snd (quotient_of r) > 0" "snd (quotient_of r) ≠ 0"
  using quotient_of_denom_pos' [of r] by simp_all

lemma quotient_of_int_div: assumes q: "quotient_of (of_int x / of_int y) = (a, b)"
  and y: "y ≠ 0" 
  shows "∃ z. z ≠ 0 ∧ x = a * z ∧ y = b * z"
proof -
  let ?r = "rat_of_int"
  define z where "z = gcd x y"
  define x' where "x' = x div z"
  define y' where "y' = y div z"
  have id: "x = z * x'" "y = z * y'" unfolding x'_def y'_def z_def by auto
  from y have y': "y' ≠ 0" unfolding id by auto
  have z: "z ≠ 0" unfolding z_def using y by auto
  have cop: "coprime x' y'" unfolding x'_def y'_def z_def 
    using div_gcd_coprime y by blast
  have "?r x / ?r y = ?r x' / ?r y'" unfolding id using z y y' by (auto simp: field_simps) 
  from assms[unfolded this] have quot: "quotient_of (?r x' / ?r y') = (a, b)" by auto
  from quotient_of_coprime[OF quot] have cop': "coprime a b" .
  hence cop: "coprime b a"
    by (simp add: ac_simps)
  from quotient_of_denom_pos[OF quot] have b: "b > 0" "b ≠ 0" by auto
  from quotient_of_div[OF quot] quotient_of_denom_pos[OF quot] y'
  have "?r x' * ?r b = ?r a * ?r y'" by (auto simp: field_simps)
  hence id': "x' * b = a * y'" unfolding of_int_mult[symmetric] by linarith
  from id'[symmetric] have "b dvd y' * a" unfolding mult.commute[of y'] by auto
  with cop y' have "b dvd y'"
    by (simp add: coprime_dvd_mult_left_iff) 
  then obtain z' where ybz: "y' = b * z'" unfolding dvd_def by auto
  from id[unfolded y' this] have y: "y = b * (z * z')" by auto
  with ‹y ≠ 0› have zz: "z * z' ≠ 0" by auto
  from quotient_of_div[OF q] ‹y ≠ 0› ‹b ≠ 0› 
  have "?r x * ?r b = ?r y * ?r a" by (auto simp: field_simps)
  hence id': "x * b = y * a" unfolding of_int_mult[symmetric] by linarith
  from this[unfolded y] b have x: "x = a * (z * z')" by auto
  show ?thesis unfolding x y using zz by blast
qed

fun max_list_non_empty :: "('a :: linorder) list ⇒ 'a" where
  "max_list_non_empty [x] = x"
| "max_list_non_empty (x # xs) = max x (max_list_non_empty xs)"

lemma max_list_non_empty: "x ∈ set xs ⟹ x ≤ max_list_non_empty xs"
proof (induct xs)
  case (Cons y ys) note oCons = this
  show ?case 
  proof (cases ys)
    case (Cons z zs)
    hence id: "max_list_non_empty (y # ys) = max y (max_list_non_empty ys)" by simp
    from oCons show ?thesis unfolding id by (auto simp: max.coboundedI2)
  qed (insert oCons, auto)
qed simp

lemma cnj_reals[simp]: "(cnj c ∈ ℝ) = (c ∈ ℝ)"
  using Reals_cnj_iff by fastforce

lemma sgn_real_mono: "x ≤ y ⟹ sgn x ≤ sgn (y :: real)"
  unfolding sgn_real_def
  by (auto split: if_splits)

lemma sgn_minus_rat: "sgn (- (x :: rat)) = - sgn x"
  by (fact Rings.sgn_minus)

lemma real_of_rat_sgn: "sgn (of_rat x) = real_of_rat (sgn x)"
  unfolding sgn_real_def sgn_rat_def by auto

lemma inverse_le_iff_sgn: assumes sgn: "sgn x = sgn y"
  shows "(inverse (x :: real) ≤ inverse y) = (y ≤ x)"
proof (cases "x = 0")
  case True
  with sgn have "sgn y = 0" by simp
  hence "y = 0" unfolding sgn_real_def by (cases "y = 0"; cases "y < 0"; auto)
  thus ?thesis using True by simp
next
  case False note x = this
  show ?thesis
  proof (cases "x < 0")
    case True
    with x sgn have "sgn y = -1" by simp
    hence "y < 0" unfolding sgn_real_def by (cases "y = 0"; cases "y < 0", auto)
    show ?thesis
      by (rule inverse_le_iff_le_neg[OF True ‹y < 0›])
  next
    case False
    with x have x: "x > 0" by auto
    with sgn have "sgn y = 1" by auto
    hence "y > 0" unfolding sgn_real_def by (cases "y = 0"; cases "y < 0", auto)
    show ?thesis
      by (rule inverse_le_iff_le[OF x ‹y > 0›])
  qed
qed

lemma inverse_le_sgn: assumes sgn: "sgn x = sgn y" and xy: "x ≤ (y :: real)"
  shows "inverse y ≤ inverse x"
  using xy inverse_le_iff_sgn[OF sgn] by auto

lemma set_list_update: "set (xs [i := k]) = 
  (if i < length xs then insert k (set (take i xs) ∪ set (drop (Suc i) xs)) else set xs)"
proof (induct xs arbitrary: i)
  case (Cons x xs i) 
  thus ?case
    by (cases i, auto)
qed simp

lemma prod_list_dvd: assumes "(x :: 'a :: comm_monoid_mult) ∈ set xs"
  shows "x dvd prod_list xs"
proof -
  from assms[unfolded in_set_conv_decomp] obtain ys zs where xs: "xs = ys @ x # zs" by auto
  show ?thesis unfolding xs dvd_def by (intro exI[of _ "prod_list (ys @ zs)"], simp add: ac_simps)
qed

lemma dvd_prod: 
fixes A::"'b set" 
assumes "∃b∈A. a dvd f b" "finite A"
shows "a dvd prod f A" 
using assms(2,1)
proof (induct A)
  case (insert x A)
  thus ?case 
    using comm_monoid_mult_class.dvd_mult dvd_mult2 insert_iff prod.insert by auto
qed auto

context
  fixes xs :: "'a :: comm_monoid_mult list"
begin
lemma prod_list_filter: "prod_list (filter f xs) * prod_list (filter (λ x. ¬ f x) xs) = prod_list xs"
  by (induct xs, auto simp: ac_simps)

lemma prod_list_partition: assumes "partition f xs = (ys, zs)"
  shows "prod_list xs = prod_list ys * prod_list zs"
  using assms by (subst prod_list_filter[symmetric, of f], auto simp: o_def)
end

lemma dvd_imp_mult_div_cancel_left[simp]:
  assumes "(a :: 'a :: semidom_divide) dvd b"
  shows "a * (b div a) = b"
proof(cases "b = 0")
  case True then show ?thesis by auto
next
  case False
  with dvdE[OF assms] obtain c where *: "b = a * c" by auto
  also with False have "a ≠ 0" by auto
  then have "a * c div a = c" by auto
  also note *[symmetric]
  finally show ?thesis.
qed

lemma (in semidom) prod_list_zero_iff[simp]: 
  "prod_list xs = 0 ⟷ 0 ∈ set xs" by (induction xs, auto)


context comm_monoid_mult begin

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

lemma is_unit_mult_iff[simp]:
  shows "(a * b) dvd 1 ⟷ a dvd 1 ∧ b dvd 1"
  by (auto dest: dvd_mult_left dvd_mult_right)

end

context comm_semiring_1
begin
lemma irreducibleE[elim]:
  assumes "irreducible p"
      and "p ≠ 0 ⟹ ¬ p dvd 1 ⟹ (⋀a b. p = a * b ⟹ a dvd 1 ∨ b dvd 1) ⟹ thesis"
  shows thesis using assms by (auto simp: irreducible_def)

lemma not_irreducibleE:
  assumes "¬ irreducible x"
      and "x = 0 ⟹ thesis"
      and "x dvd 1 ⟹ thesis"
      and "⋀a b. x = a * b ⟹ ¬ a dvd 1 ⟹ ¬ b dvd 1 ⟹ thesis"
  shows thesis using assms unfolding irreducible_def by auto

lemma prime_elem_dvd_prod_list:
  assumes p: "prime_elem p" and pA: "p dvd prod_list A" shows "∃a ∈ set A. p dvd a"
proof(insert pA, induct A)
  case Nil
  with p show ?case by (simp add: prime_elem_not_unit)
next
  case (Cons a A)
  then show ?case by (auto simp: prime_elem_dvd_mult_iff[OF p])
qed

lemma prime_elem_dvd_prod_mset:
  assumes p: "prime_elem p" and pA: "p dvd prod_mset A" shows "∃a ∈# A. p dvd a"
proof(insert pA, induct A)
  case empty
  with p show ?case by (simp add: prime_elem_not_unit)
next
  case (add a A)
  then show ?case by (auto simp: prime_elem_dvd_mult_iff[OF p])
qed

lemma mult_unit_dvd_iff[simp]:
  assumes "b dvd 1"
  shows "a * b dvd c ⟷ a dvd c"
proof
  assume "a * b dvd c"
  with assms show "a dvd c" using dvd_mult_left[of a b c] by simp
next
  assume "a dvd c"
  with assms mult_dvd_mono show "a * b dvd c" by fastforce
qed

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

lemma irreducibleD':
  assumes "irreducible a" "b dvd a"
  shows   "a dvd b ∨ b dvd 1"
proof -
  from assms obtain c where c: "a = b * c" by (elim dvdE)
  from irreducibleD[OF assms(1) this] have "b dvd 1 ∨ c dvd 1" .
  thus ?thesis by (auto simp: c)
qed

end



context idom
begin

text ‹
  Following lemmas are adapted and generalized so that they don't use "algebraic" classes.
›

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 (auto 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 irreducibleI':
  assumes "a ≠ 0" "¬ a dvd 1" "⋀b. b dvd a ⟹ a dvd b ∨ b dvd 1"
  shows   "irreducible a"
proof (rule irreducibleI)
  fix b c assume a_eq: "a = b * c"
  hence "a dvd b ∨ b dvd 1" by (intro assms) simp_all
  thus "b dvd 1 ∨ c dvd 1"
  proof
    assume "a dvd b"
    hence "b * c dvd b * 1" by (simp add: a_eq)
    moreover from ‹a ≠ 0› a_eq have "b ≠ 0" by auto
    ultimately show ?thesis using dvd_times_left_cancel_iff by fastforce
  qed blast
qed (simp_all add: assms(1,2))

lemma irreducible_altdef:
  shows "irreducible x ⟷ x ≠ 0 ∧ ¬ x dvd 1 ∧ (∀b. b dvd x ⟶ x dvd b ∨ b dvd 1)"
  using irreducibleI'[of x] irreducibleD'[of x] irreducible_not_unit[of x] by auto

lemma dvd_mult_unit_iff:
  assumes b: "b dvd 1"
  shows "a dvd c * b ⟷ a dvd c"
proof-
  from b obtain b' where 1: "b * b' = 1" by (elim dvdE, auto)
  then have b0: "b ≠ 0" by auto
  from 1 have "a = (a * b') * b" by (simp add: ac_simps)
  also have "… dvd c * b ⟷ a * b' dvd c" using b0 by auto
  finally show ?thesis by (auto intro: dvd_mult_left)
qed

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

lemma irreducible_mult_unit_left:
  shows "a dvd 1 ⟹ irreducible (a * p) ⟷ irreducible p"
  by (auto simp: irreducible_altdef mult.commute[of a] dvd_mult_unit_iff)

lemma irreducible_mult_unit_right:
  shows "a dvd 1 ⟹ irreducible (p * a) ⟷ irreducible p"
  by (auto simp: irreducible_altdef mult.commute[of a] dvd_mult_unit_iff)

lemma prime_elem_imp_irreducible:
  assumes "prime_elem p"
  shows   "irreducible p"
proof (rule irreducibleI)
  fix a b
  assume p_eq: "p = a * b"
  with assms have nz: "a ≠ 0" "b ≠ 0" by auto
  from p_eq have "p dvd a * b" by simp
  with ‹prime_elem p› have "p dvd a ∨ p dvd b" by (rule prime_elem_dvd_multD)
  with ‹p = a * b› have "a * b dvd 1 * b ∨ a * b dvd a * 1" by auto
  thus "a dvd 1 ∨ b dvd 1"
    by (simp only: dvd_times_left_cancel_iff[OF nz(1)] dvd_times_right_cancel_iff[OF nz(2)])
qed (insert assms, simp_all add: prime_elem_def)

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

lemma unit_mult_left_cancel: "a dvd 1 ⟹ a * b = a * c ⟷ b = c"
  using mult_cancel_left [of a b c] by auto

lemma unit_mult_right_cancel: "a dvd 1 ⟹ b * a = c * a ⟷ b = c"
  using unit_mult_left_cancel [of a b c] by (auto simp add: ac_simps)

text ‹New parts from here›

lemma irreducible_multD:
  assumes l: "irreducible (a*b)"
  shows "a dvd 1 ∧ irreducible b ∨ b dvd 1 ∧ irreducible a"
proof-
  from l have "a dvd 1 ∨ b dvd 1" using irreducibleD by auto
  then show ?thesis
  proof(elim disjE)
    assume a: "a dvd 1"
    with l have "irreducible b"
      unfolding irreducible_def
      by (metis is_unit_mult_iff mult.left_commute mult_not_zero)
    with a show ?thesis by auto
  next
    assume a: "b dvd 1"
    with l have "irreducible a"
      unfolding irreducible_def
      by (meson is_unit_mult_iff mult_not_zero semiring_normalization_rules(16))
    with a show ?thesis by auto
  qed
qed

end

lemma (in field) irreducible_field[simp]:
  "irreducible x ⟷ False" by (auto simp: dvd_field_iff irreducible_def)

lemma (in idom) irreducible_mult:
  shows "irreducible (a*b) ⟷ a dvd 1 ∧ irreducible b ∨ b dvd 1 ∧ irreducible a"
  by (auto dest: irreducible_multD simp: irreducible_mult_unit_left irreducible_mult_unit_right)


end