Theory Jordan_Normal_Form.Missing_Ring

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

text ‹This theory contains several lemmas which might be of interest to the Isabelle distribution.›

theory Missing_Ring
  imports
  "Missing_Misc"
  "HOL-Algebra.Ring"
begin

context ordered_cancel_semiring
begin

subclass ordered_cancel_ab_semigroup_add ..

end

text ‹partially ordered variant›
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 A: "a  b" "0  c"
  from A show "c * a  c * b"
    unfolding le_less
    using mult_strict_left_mono by (cases "c = 0") auto
  from A show "a * c  b * c"
    unfolding le_less
    using mult_strict_right_mono by (cases "c = 0") auto
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 ‹Legacy - use mult_neg_pos›
lemma mult_pos_neg2: "0 < a  b < 0  b * a < 0" 
by (drule mult_strict_right_mono [of b 0], auto)

text‹Strict monotonicity in both arguments›
lemma mult_strict_mono:
  assumes "a < b" and "c < d" and "0 < b" and "0  c"
  shows "a * c < b * d"
  using assms apply (cases "c=0")
  apply (simp)
  apply (erule mult_strict_right_mono [THEN less_trans])
  apply (force simp add: le_less)
  apply (erule mult_strict_left_mono, assumption)
  done

text‹This weaker variant has more natural premises›
lemma mult_strict_mono':
  assumes "a < b" and "c < d" and "0  a" and "0  c"
  shows "a * c < b * d"
by (rule mult_strict_mono) (insert assms, auto)

lemma mult_less_le_imp_less:
  assumes "a < b" and "c  d" and "0  a" and "0 < c"
  shows "a * c < b * d"
  using assms apply (subgoal_tac "a * c < b * c")
  apply (erule less_le_trans)
  apply (erule mult_left_mono)
  apply simp
  apply (erule mult_strict_right_mono)
  apply assumption
  done

lemma mult_le_less_imp_less:
  assumes "a  b" and "c < d" and "0 < a" and "0  c"
  shows "a * c < b * d"
  using assms apply (subgoal_tac "a * c  b * c")
  apply (erule le_less_trans)
  apply (erule mult_strict_left_mono)
  apply simp
  apply (erule mult_right_mono)
  apply simp
  done

end

class ordered_idom = idom + ordered_semiring_strict +
  assumes zero_less_one [simp]: "0 < 1" begin

subclass semiring_1 ..
subclass comm_ring_1 ..
subclass ordered_ring ..
subclass ordered_comm_semiring by(unfold_locales, fact mult_left_mono)
subclass ordered_ab_semigroup_add ..

lemma of_nat_ge_0[simp]: "of_nat x  0"
proof (induct x)
  case 0 thus ?case by auto
  next case (Suc x)
    hence "0  of_nat x" by auto
    also have "of_nat x < of_nat (Suc x)" by auto
    finally show ?case by auto
qed

lemma of_nat_eq_0[simp]: "of_nat x = 0  x = 0"
proof(induct x,simp)
  case (Suc x)
    have "of_nat (Suc x) > 0" apply(rule le_less_trans[of _ "of_nat x"]) by auto
    thus ?case by auto
qed

lemma inj_of_nat: "inj (of_nat :: nat  'a)"
proof(rule injI)
  fix x y show "of_nat x = of_nat y  x = y"
  proof (induct x arbitrary: y)
    case 0 thus ?case
      proof (induct y)
        case 0 thus ?case by auto
        next case (Suc y)
          hence "of_nat (Suc y) = 0" by auto
          hence "Suc y = 0" unfolding of_nat_eq_0 by auto
          hence False by auto
          thus ?case by auto
      qed
    next case (Suc x)
      thus ?case
      proof (induct y)
        case 0
          hence "of_nat (Suc x) = 0" by auto
          hence "Suc x = 0" unfolding of_nat_eq_0 by auto
          hence False by auto
          thus ?case by auto
        next case (Suc y) thus ?case by auto
      qed
  qed
qed

subclass ring_char_0 by(unfold_locales, fact inj_of_nat)

end

(*
instance linordered_idom ⊆ ordered_semiring_strict by (intro_classes,auto)
instance linordered_idom ⊆ ordered_idom by (intro_classes, auto)
*)

context comm_monoid
begin

lemma finprod_reindex_bij_betw: "bij_betw h S T 
   g  h ` S  carrier G 
   finprod G (λx. g (h x)) S = finprod G g T"
  using finprod_reindex[of g h S] unfolding bij_betw_def by auto

lemma finprod_reindex_bij_witness:
  assumes witness:
    "a. a  S  i (j a) = a"
    "a. a  S  j a  T"
    "b. b  T  j (i b) = b"
    "b. b  T  i b  S"
  assumes eq:
    "a. a  S  h (j a) = g a"
  assumes g: "g  S  carrier G"
  and h: "h  j ` S  carrier G"
  shows "finprod G g S = finprod G h T"
proof -
  have b: "bij_betw j S T"
    using bij_betw_byWitness[where A=S and f=j and f'=i and A'=T] witness by auto
  have fp: "finprod G g S = finprod G (λx. h (j x)) S"
    by (rule finprod_cong, insert eq g, auto)
  show ?thesis
    using finprod_reindex_bij_betw[OF b h] unfolding fp .
qed
end

lemmas (in abelian_monoid) finsum_reindex_bij_witness = add.finprod_reindex_bij_witness

locale csemiring = semiring + comm_monoid R

context cring
begin
sublocale csemiring ..
end

lemma (in comm_monoid) finprod_one': 
  "( a. a  A  f a = 𝟭)  finprod G f A = 𝟭"
  by (induct A rule: infinite_finite_induct, auto)

lemma (in comm_monoid) finprod_split: 
  "finite A  f ` A  carrier G  a  A  finprod G f A = f a  finprod G f (A - {a})"
  by (rule trans[OF trans[OF _ finprod_Un_disjoint[of "{a}" "A - {a}" f]]], auto,
  rule arg_cong[of _ _ "finprod G f"], auto)

lemma (in comm_monoid) finprod_finprod:
  "finite A  finite B  ( a b. a  A   b  B  g a b  carrier G) 
  finprod G (λ a. finprod G (g a) B) A = finprod G (λ (a,b). g a b) (A × B)"
proof (induct A rule: finite_induct)
  case (insert a' A)
  note IH = this
  let ?l = "(ainsert a' A. finprod G (g a) B)"
  let ?r = "(ainsert a' A × B. case a of (a, b)  g a b)"
  have "?l = finprod G (g a') B  (aA. finprod G (g a) B)"
    using IH by simp
  also have "(aA. finprod G (g a) B) = finprod G (λ (a,b). g a b) (A × B)"
    by (rule IH(3), insert IH, auto)
  finally have idl: "?l = finprod G (g a') B  finprod G (λ (a,b). g a b) (A × B)" .
  from IH(2) have "insert a' A × B = {a'} × B  A × B" by auto
  hence "?r = (a{a'} × B  A × B. case a of (a, b)  g a b)" by simp
  also have " = (a{a'} × B. case a of (a, b)  g a b)  (a A × B. case a of (a, b)  g a b)"
    by (rule finprod_Un_disjoint, insert IH, auto)
  also have "(a{a'} × B. case a of (a, b)  g a b) = finprod G (g a') B"
    using IH(4) IH(5)
  proof (induct B rule: finite_induct)
    case (insert b' B)
    note IH = this
    have id: "(a{a'} × B. case a of (a, b)  g a b) = finprod G (g a') B"
      by (rule IH(3)[OF IH(4)], auto)
    have id2: " x F. {a'} × insert x F = insert (a',x) ({a'} × F)" by auto
    have id3: "(ainsert (a', b') ({a'} × B). case a of (a, b)  g a b)
      = g a' b'  (a({a'} × B). case a of (a, b)  g a b)"
      by (rule trans[OF finprod_insert], insert IH, auto)
    show ?case unfolding id2 id3 id
      by (rule sym, rule finprod_insert, insert IH, auto)
  qed simp
  finally have idr: "?r = finprod G (g a') B  (aA × B. case a of (a, b)  g a b)" .
  show ?case unfolding idl idr ..
qed simp

lemma (in comm_monoid) finprod_swap:
  assumes "finite A" "finite B" " a b. a  A   b  B  g a b  carrier G"
  shows "finprod G (λ (b,a). g a b) (B × A) = finprod G (λ (a,b). g a b) (A × B)"
proof -
  have [simp]: "(λ(a, b). (b, a)) ` (A × B) = B × A" by auto
  have [simp]: "(λ x. case case x of (a, b)  (b, a) of (a, b)  g b a) = (λ (a,b). g a b)"
    by (intro ext, auto)
  show ?thesis 
    by (rule trans[OF trans[OF _ finprod_reindex[of "λ (a,b). g b a" "λ (a,b). (b,a)"]]],
    insert assms, auto simp: inj_on_def)
qed

lemma (in comm_monoid) finprod_finprod_swap:
  "finite A  finite B  ( a b. a  A   b  B  g a b  carrier G) 
  finprod G (λ a. finprod G (g a) B) A = finprod G (λ b. finprod G (λ a. g a b) A) B"
  using finprod_finprod[of A B] finprod_finprod[of B A] finprod_swap[of A B]
  by simp



lemmas (in semiring) finsum_zero' = add.finprod_one' 
lemmas (in semiring) finsum_split = add.finprod_split 
lemmas (in semiring) finsum_finsum_swap = add.finprod_finprod_swap


lemma (in csemiring) finprod_zero: 
  "finite A  f  A  carrier R  aA. f a = 𝟬
    finprod R f A = 𝟬"
proof (induct A rule: finite_induct)
  case (insert a A)
  from finprod_insert[OF insert(1-2), of f] insert(4)
  have ins: "finprod R f (insert a A) = f a  finprod R f A" by simp
  have fA: "finprod R f A  carrier R"
    by (rule finprod_closed, insert insert, auto)
  show ?case
  proof (cases "f a = 𝟬")
    case True
    with fA show ?thesis unfolding ins by simp
  next
    case False
    with insert(5) have " a  A. f a = 𝟬" by auto
    from insert(3)[OF _ this] insert have "finprod R f A = 𝟬" by auto
    with insert show ?thesis unfolding ins by auto
  qed
qed simp

lemma (in semiring) finsum_product:
  assumes A: "finite A" and B: "finite B"
  and f: "f  A  carrier R" and g: "g  B  carrier R" 
  shows "finsum R f A  finsum R g B = (iA. jB. f i  g j)"
  unfolding finsum_ldistr[OF A finsum_closed[OF g] f]
proof (rule finsum_cong'[OF refl])
  fix a
  assume a: "a  A"
  show "f a  finsum R g B = (jB. f a  g j)"
  by (rule finsum_rdistr[OF B _ g], insert a f, auto)
qed (insert f g B, auto intro: finsum_closed)
    
lemma (in semiring) Units_one_side_I: 
  "a  carrier R  p  Units R  p  a = 𝟭  a  Units R"
  "a  carrier R  p  Units R  a  p = 𝟭  a  Units R"
  by (metis Units_closed Units_inv_Units Units_l_inv inv_unique)+


lemma permutes_funcset: "p permutes A  (p ` A  B) = (A  B)"
  by (simp add: permutes_image)

context comm_monoid
begin
lemma finprod_permute:
  assumes p: "p permutes S"
  and f: "f  S  carrier G"
  shows "finprod G f S = finprod G (f  p) S"
proof -
  from p permutes S have "inj p"
    by (rule permutes_inj)
  then have "inj_on p S"
    by (auto intro: subset_inj_on)
  from finprod_reindex[OF _ this, unfolded permutes_image[OF p], OF f]
  show ?thesis unfolding o_def .
qed

lemma finprod_singleton_set[simp]: assumes "f a  carrier G"
  shows "finprod G f {a} = f a"
proof -
  have "finprod G f {a} = f a  finprod G f {}"
    by (rule finprod_insert, insert assms, auto)
  also have " = f a" using assms by auto
  finally show ?thesis .
qed
end

lemmas (in semiring) finsum_permute = add.finprod_permute
lemmas (in semiring) finsum_singleton_set = add.finprod_singleton_set

context cring
begin

lemma finsum_permutations_inverse: 
  assumes f: "f  {p. p permutes S}  carrier R"
  shows "finsum R f {p. p permutes S} = finsum R (λp. f(Hilbert_Choice.inv p)) {p. p permutes S}"
  (is "?lhs = ?rhs")
proof -
  let ?inv = "Hilbert_Choice.inv"
  let ?S = "{p . p permutes S}"
  have th0: "inj_on ?inv ?S"
  proof (auto simp add: inj_on_def)
    fix q r
    assume q: "q permutes S"
      and r: "r permutes S"
      and qr: "?inv q = ?inv r"
    then have "?inv (?inv q) = ?inv (?inv r)"
      by simp
    with permutes_inv_inv[OF q] permutes_inv_inv[OF r] show "q = r"
      by metis
  qed
  have th1: "?inv ` ?S = ?S"
    using image_inverse_permutations by blast
  have th2: "?rhs = finsum R (f  ?inv) ?S"
    by (simp add: o_def)
  from finsum_reindex[OF _ th0, of f] show ?thesis unfolding th1 th2 using f .
qed

lemma finsum_permutations_compose_right: assumes q: "q permutes S"
  and *: "f  {p. p permutes S}  carrier R"
  shows "finsum R f {p. p permutes S} = finsum R (λp. f(p  q)) {p. p permutes S}"
  (is "?lhs = ?rhs")
proof -
  let ?S = "{p. p permutes S}"
  let ?inv = "Hilbert_Choice.inv"
  have th0: "?rhs = finsum R (f  (λp. p  q)) ?S"
    by (simp add: o_def)
  have th1: "inj_on (λp. p  q) ?S"
  proof (auto simp add: inj_on_def)
    fix p r
    assume "p permutes S"
      and r: "r permutes S"
      and rp: "p  q = r  q"
    then have "p  (q  ?inv q) = r  (q  ?inv q)"
      by (simp add: o_assoc)
    with permutes_surj[OF q, unfolded surj_iff] show "p = r"
      by simp
  qed
  have th3: "(λp. p  q) ` ?S = ?S"
    using image_compose_permutations_right[OF q] by auto
  from finsum_reindex[OF _ th1, of f]
  show ?thesis unfolding th0 th1 th3 using * .
qed

end

end