Theory SML_Rings

(* Title: Examples/SML_Relativization/Algebra/SML_Rings.thy
   Author: Mihails Milehins
   Copyright 2021 (C) Mihails Milehins
*)
section‹Relativization of the results about rings›
theory SML_Rings
  imports 
    SML_Semirings
    Complex_Main
begin



subsection‹Rings›


subsubsection‹Definitions and common properties›

locale ring_ow =
  semiring_ow U plus times + ab_group_add_ow U plus zero minus uminus
  for U :: "'ag set" and plus zero minus uminus times
begin

sublocale semiring_0_cancel_ow ..

end

lemma ring_ow: "class.ring = ring_ow UNIV"
  unfolding class.ring_def ring_ow_def ab_group_add_ow semiring_ow
  by (simp add: conj_commute)

lemma ring_ow_UNIV_axioms: "ring_ow (UNIV::'a::ring set) (+) 0 (-) uminus (*)"
  by (fold ring_ow) (rule ring_class.ring_axioms)


subsubsection‹Transfer rules›

context
  includes lifting_syntax
begin

lemma ring_transfer[transfer_rule]:
  assumes[transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "(
      (A ===> A ===> A) ===> 
      A ===> 
      (A ===> A ===> A) ===> 
      (A ===> A) ===> 
      (A ===> A ===> A) ===> 
      (=)
    ) 
    (ring_ow (Collect (Domainp A))) class.ring"
  unfolding ring_ow_def class.ring_def
  apply transfer_prover_start
  apply transfer_step+
  by blast

end


subsubsection‹Relativization›

context ring_ow
begin

tts_context
  tts: (?'a to U)
  rewriting ctr_simps
  substituting ring_ow_axioms and zero.not_empty
  applying 
    [
      OF 
        plus_closed' 
        zero_closed 
        minus_closed' 
        add.inverse_closed'' 
        times_closed'
    ] 
begin

tts_lemma right_diff_distrib:
  assumes "a  U" and "b  U" and "c  U"
  shows "a *ow (b -ow c) = a *ow b -ow a *ow c"
    is Rings.ring_class.right_diff_distrib.

tts_lemma minus_mult_commute:
  assumes "a  U" and "b  U"
  shows "-ow a *ow b = a *ow -ow b"
    is Rings.ring_class.minus_mult_commute.

tts_lemma left_diff_distrib:
  assumes "a  U" and "b  U" and "c  U"
  shows "(a -ow b) *ow c = a *ow c -ow b *ow c"
    is Rings.ring_class.left_diff_distrib.

tts_lemma mult_minus_right:
  assumes "a  U" and "b  U"
  shows "a *ow -ow b = -ow (a *ow b)"
    is Rings.ring_class.mult_minus_right.

tts_lemma minus_mult_right:
  assumes "a  U" and "b  U"
  shows "-ow (a *ow b) = a *ow -ow b"
    is Rings.ring_class.minus_mult_right.

tts_lemma minus_mult_minus:
  assumes "a  U" and "b  U"
  shows "-ow a *ow -ow b = a *ow b"
    is Rings.ring_class.minus_mult_minus.

tts_lemma mult_minus_left:
  assumes "a  U" and "b  U"
  shows "-ow a *ow b = -ow (a *ow b)"
    is Rings.ring_class.mult_minus_left.

tts_lemma minus_mult_left:
  assumes "a  U" and "b  U"
  shows "-ow (a *ow b) = -ow a *ow b"
    is Rings.ring_class.minus_mult_left.

tts_lemma ring_distribs:
  assumes "a  U" and "b  U" and "c  U"
  shows 
    "a *ow (b +ow c) = a *ow b +ow a *ow c"
    "(a +ow b) *ow c = a *ow c +ow b *ow c"
    "(a -ow b) *ow c = a *ow c -ow b *ow c"
    "a *ow (b -ow c) = a *ow b -ow a *ow c"
    is Rings.ring_class.ring_distribs.

tts_lemma eq_add_iff2:
  assumes "a  U" and "e  U" and "c  U" and "b  U" and "d  U"
  shows "(a *ow e +ow c = b *ow e +ow d) = (c = (b -ow a) *ow e +ow d)"
    is Rings.ring_class.eq_add_iff2.

tts_lemma eq_add_iff1:
  assumes "a  U" and "e  U" and "c  U" and "b  U" and "d  U"
  shows "(a *ow e +ow c = b *ow e +ow d) = ((a -ow b) *ow e +ow c = d)"
    is Rings.ring_class.eq_add_iff1.

tts_lemma mult_diff_mult:
  assumes "x  U" and "y  U" and "a  U" and "b  U"
  shows "x *ow y -ow a *ow b = x *ow (y -ow b) +ow (x -ow a) *ow b"
    is Real.mult_diff_mult.

end

end



subsection‹Commutative rings›


subsubsection‹Definitions and common properties›

locale comm_ring_ow =
  comm_semiring_ow U plus times + ab_group_add_ow U plus zero minus uminus
  for U :: "'ag set" and plus zero minus uminus times
begin

sublocale ring_ow ..
sublocale comm_semiring_0_cancel_ow ..

end

lemma comm_ring_ow: "class.comm_ring = comm_ring_ow UNIV"
  unfolding 
    class.comm_ring_def comm_ring_ow_def 
    ab_group_add_ow comm_semiring_ow
  by (simp add: conj_commute)


subsubsection‹Transfer rules›

context
  includes lifting_syntax
begin

lemma comm_ring_transfer[transfer_rule]:
  assumes[transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "(
      (A ===> A ===> A) ===> 
      A ===> 
      (A ===> A ===> A) ===> 
      (A ===> A) ===>
      (A ===> A ===> A) ===>
      (=)
    ) 
    (comm_ring_ow (Collect (Domainp A))) class.comm_ring"
  unfolding comm_ring_ow_def class.comm_ring_def
  apply transfer_prover_start
  apply transfer_step+
  by blast

end


subsubsection‹Relativization›

context comm_ring_ow
begin

tts_context
  tts: (?'a to U)
  rewriting ctr_simps
  substituting comm_ring_ow_axioms and zero.not_empty
  applying 
    [
      OF 
        plus_closed' 
        zero_closed 
        minus_closed' 
        add.inverse_closed'' 
        times_closed'
    ] 
begin

tts_lemma square_diff_square_factored:
  assumes "x  U" and "y  U"
  shows "x *ow x -ow y *ow y = (x +ow y) *ow (x -ow y)"
    is comm_ring_class.square_diff_square_factored.

end

end



subsection‹Rings with identity›


subsubsection‹Definitions and common properties›

locale ring_1_ow =
  ring_ow U plus zero minus uminus times + 
  zero_neq_one_ow U one zero + 
  monoid_mult_ow U one times 
  for U :: "'ag set" and one times plus zero minus uminus
begin

sublocale semiring_1_cancel_ow ..

end

lemma ring_1_ow: "class.ring_1 = ring_1_ow UNIV"
  unfolding 
    class.ring_1_def ring_1_ow_def monoid_mult_ow ring_ow zero_neq_one_ow
  by (force simp: conj_commute)

lemma ring_1_ow_UNIV_axioms: 
  "ring_1_ow (UNIV::'a::ring_1 set) 1 (*) (+) 0 (-) uminus"
  by (fold ring_1_ow) (rule ring_1_class.ring_1_axioms)

ud ring_1.iszero ((with _ : «iszero» _) [1000, 1000] 10)
ud iszero' iszero 
ud ring_1.of_int
  ((with _ _ _ _ : «of'_int» _) [1000, 999, 998, 997, 1000] 10)
ud of_int' of_int
ud ring_1.Ints ((with _ _ _ _ : ) [1000, 999, 998, 997] 10)
ud Ints' Ints
ud diffs ((with _ _ _ _ : «diffs» _) [1000, 999, 998, 997, 1000] 10)

ctr parametricity  
  in iszero_ow: iszero.with_def 
    and of_int_ow: of_int.with_def
    and Ints_ow: Ints.with_def
    and diffs_ow: diffs.with_def

context ring_1_ow
begin

abbreviation iszero where "iszero  iszero.with 0ow"
abbreviation of_int where "of_int  of_int.with 1ow (+ow) 0ow (-ow)"
abbreviation Ints («ℤ») where "«ℤ»  Ints.with 1ow (+ow) 0ow (-ow)"
notation Ints («ℤ»)

end

context ring_1
begin

lemma Int_ss_UNIV: "  UNIV" by simp 

end


subsubsection‹Transfer rules›

context
  includes lifting_syntax
begin

lemma ring_1_transfer[transfer_rule]:
  assumes[transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "(
      A ===> 
      (A ===> A ===> A) ===>
      (A ===> A ===> A) ===>
      A ===>
      (A ===> A ===> A) ===> 
      (A ===> A) ===>
      (=)
    ) 
      (ring_1_ow (Collect (Domainp A))) class.ring_1"
  unfolding ring_1_ow_def class.ring_1_def
  apply transfer_prover_start
  apply transfer_step+
  by blast

end


subsubsection‹Relativization›

declare dvd.with[ud_with del]
declare dvd'.with[ud_with del]

context ring_1_ow
begin

tts_context
  tts: (?'a to U)
  substituting ring_1_ow_axioms and zero.not_empty
  eliminating through simp
begin

tts_lemma Int_ss_UNIV[simp]: "«ℤ»  U"
  is Int_ss_UNIV.

end

lemma Int_closed[simp,intro]: "a  «ℤ»  a  U" using Int_ss_UNIV by blast

tts_context
  tts: (?'a to U)
  rewriting ctr_simps
  substituting ring_1_ow_axioms and zero.not_empty
  eliminating through auto
begin

tts_lemma iszero_0: "iszero 0ow"
  is ring_1_class.iszero_0.
    
tts_lemma not_iszero_1: "¬ iszero 1ow"
  is ring_1_class.not_iszero_1.

tts_lemma Nats_subset_Ints: "«ℕ»  «ℤ»"
  is Int.ring_1_class.Nats_subset_Ints.

tts_lemma Ints_1: "1ow  «ℤ»"
  is Int.ring_1_class.Ints_1.

tts_lemma Ints_0: "0ow  «ℤ»"
  is Int.ring_1_class.Ints_0.

tts_lemma not_iszero_neg_1: "¬ iszero (-ow 1ow)"
  is Num.ring_1_class.not_iszero_neg_1.

tts_lemma of_int_1: "of_int 1 = 1ow"
  is Int.ring_1_class.of_int_1.

tts_lemma of_int_0: "of_int 0 = 0ow"
  is Int.ring_1_class.of_int_0.

tts_lemma Ints_of_int: "of_int z  «ℤ»"
  is Int.ring_1_class.Ints_of_int.

tts_lemma Ints_of_nat: "of_nat n  «ℤ»"
  is Int.ring_1_class.Ints_of_nat.

tts_lemma of_int_of_nat_eq:
  shows "local.of_int (with 1 (+) 0 : «of_nat» n) = local.of_nat n"
    is Int.ring_1_class.of_int_of_nat_eq.

tts_lemma of_int_of_bool:
  "of_int (with 1 0 : «of_bool» P) = of_bool P"
  is Int.ring_1_class.of_int_of_bool.

tts_lemma of_int_minus: "of_int (- z) = -ow of_int z"
  is Int.ring_1_class.of_int_minus.

tts_lemma mult_minus1_right:
  assumes "z  U"
  shows "z *ow -ow 1ow = -ow z"
    is Num.ring_1_class.mult_minus1_right.

tts_lemma mult_minus1:
  assumes "z  U"
  shows "-ow 1ow *ow z = -ow z"
    is Num.ring_1_class.mult_minus1.

tts_lemma eq_iff_iszero_diff:
  assumes "x  U" and "y  U"
  shows "(x = y) = iszero (x -ow y)"
    is Num.ring_1_class.eq_iff_iszero_diff.

tts_lemma minus_in_Ints_iff:
  assumes "x  U"
  shows "(-ow x  «ℤ») = (x  «ℤ»)"
    is Int.ring_1_class.minus_in_Ints_iff.

tts_lemma mult_of_int_commute:
  assumes "y  U"
  shows "of_int x *ow y = y *ow of_int x"
    is Int.ring_1_class.mult_of_int_commute.

tts_lemma of_int_power:
  "of_int ((with 1 (*) : z ^ow n)) = of_int z ^ow n"
    is Int.ring_1_class.of_int_power.

tts_lemma Ints_minus:
  assumes "a  «ℤ»"
  shows "-ow a  «ℤ»"
    is Int.ring_1_class.Ints_minus.

tts_lemma of_int_diff: "of_int (w - z) = of_int w -ow of_int z"
  is Int.ring_1_class.of_int_diff.

tts_lemma of_int_add: "of_int (w + z) = of_int w +ow of_int z"
  is Int.ring_1_class.of_int_add.

tts_lemma of_int_mult: "of_int (w * z) = of_int w *ow of_int z"
  is Int.ring_1_class.of_int_mult.

tts_lemma power_minus1_even: "(-ow 1ow) ^ow (2 * n) = 1ow"
  is Power.ring_1_class.power_minus1_even.

tts_lemma Ints_power:
  assumes "a  «ℤ»"
  shows "a ^ow n  «ℤ»"
    is Int.ring_1_class.Ints_power.

tts_lemma of_nat_nat:
  assumes "0  z"
  shows "of_nat (nat z) = of_int z"
    is Int.ring_1_class.of_nat_nat.

tts_lemma power2_minus:
  assumes "a  U"
  shows "(-ow a) ^ow 2 = a ^ow 2"
    is Power.ring_1_class.power2_minus.

tts_lemma power_minus1_odd:
  shows "(-ow 1ow) ^ow Suc (2 * n) = -ow 1ow"
    is Power.ring_1_class.power_minus1_odd.

tts_lemma power_minus:
  assumes "a  U"
  shows "(-ow a) ^ow n = (-ow 1ow) ^ow n *ow a ^ow n"
    is Power.ring_1_class.power_minus.

tts_lemma square_diff_one_factored:
  assumes "x  U"
  shows "x *ow x -ow 1ow = (x +ow 1ow) *ow (x -ow 1ow)"
    is Rings.ring_1_class.square_diff_one_factored.

tts_lemma neg_one_even_power:
  assumes "even n"
  shows "(-ow 1ow) ^ow n = 1ow"
    is Parity.ring_1_class.neg_one_even_power.

tts_lemma minus_one_power_iff:
  "(-ow 1ow) ^ow n = (if even n then 1ow else -ow 1ow)"
    is Parity.ring_1_class.minus_one_power_iff.

tts_lemma Nats_altdef1: "«ℕ» = {x  U. y0. x = of_int y}"
    is Int.ring_1_class.Nats_altdef1.

tts_lemma Ints_induct:
  assumes "q  «ℤ»" and "z. P (of_int z)"
  shows "P q"
    is Int.ring_1_class.Ints_induct.

tts_lemma of_int_of_nat:
  shows 
    "of_int k = (if k < 0 then -ow of_nat (nat (- k)) else of_nat (nat k))"
    is Int.ring_1_class.of_int_of_nat.

tts_lemma Ints_diff:
  assumes "a  «ℤ»" and "b  «ℤ»"
  shows "a -ow b  «ℤ»"
    is Int.ring_1_class.Ints_diff.

tts_lemma Ints_add:
  assumes "a  «ℤ»" and "b  «ℤ»"
  shows "a +ow b  «ℤ»"
    is Int.ring_1_class.Ints_add.

tts_lemma Ints_mult:
  assumes "a  «ℤ»" and "b  «ℤ»"
  shows "a *ow b  «ℤ»"
    is Int.ring_1_class.Ints_mult.

tts_lemma power_minus_even':
  assumes "a  U" and "even n"
  shows "(-ow a) ^ow n = a ^ow n"
    is Parity.ring_1_class.power_minus_even.

tts_lemma power_minus_even:
  assumes "a  U"
  shows "(-ow a) ^ow (2 * n) = a ^ow (2 * n)"
    is Power.ring_1_class.power_minus_even.

tts_lemma power_minus_odd:
  assumes "a  U" and "odd n"
  shows "(-ow a) ^ow n = -ow (a ^ow n)"
    is Parity.ring_1_class.power_minus_odd.

tts_lemma uminus_power_if:
  assumes "a  U"
  shows "(-ow a) ^ow n = (if even n then a ^ow n else -ow (a ^ow n))"
    is Parity.ring_1_class.uminus_power_if.

tts_lemma neg_one_power_add_eq_neg_one_power_diff:
  assumes "k  n"
  shows "(-ow 1ow) ^ow (n + k) = (-ow 1ow) ^ow (n - k)"
    is Parity.ring_1_class.neg_one_power_add_eq_neg_one_power_diff.

tts_lemma neg_one_odd_power:
  assumes "odd n"
  shows "(-ow 1ow) ^ow n = -ow 1ow"
    is Parity.ring_1_class.neg_one_odd_power.

tts_lemma Ints_cases:
  assumes "q  «ℤ»" and "z. q = of_int z  thesis"
  shows thesis
    is Int.ring_1_class.Ints_cases.

end

end

lemmas [ud_with] = dvd.with dvd'.with



subsection‹Commutative rings with identity›


subsubsection‹Definitions and common properties›

locale comm_ring_1_ow =
  comm_ring_ow U plus zero minus uminus times + 
  zero_neq_one_ow U one zero + 
  comm_monoid_mult_ow U times one 
  for U :: "'ag set" and times one plus zero minus uminus
begin

sublocale ring_1_ow ..
sublocale comm_semiring_1_cancel_ow 
  by unfold_locales (blast intro: right_diff_distrib)

end

lemma comm_ring_1_ow: "class.comm_ring_1 = comm_ring_1_ow UNIV"
  unfolding 
    class.comm_ring_1_def comm_ring_1_ow_def
    comm_monoid_mult_ow comm_ring_ow zero_neq_one_ow
  by (force simp: conj_commute)

lemma comm_ring_1_ow_UNIV_axioms:
  "comm_ring_1_ow (UNIV::'a::comm_ring_1 set) (*) 1 (+) 0 (-) uminus"
  by (fold comm_ring_1_ow) (rule comm_ring_1_class.comm_ring_1_axioms)


subsubsection‹Transfer rules›

context
  includes lifting_syntax
begin

lemma comm_ring_1_transfer[transfer_rule]:
  assumes[transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "(
      (A ===> A ===> A) ===>
      A ===> 
      (A ===> A ===> A) ===>
      A ===>
      (A ===> A ===> A) ===> 
      (A ===> A) ===>
      (=)
    ) (comm_ring_1_ow (Collect (Domainp A))) class.comm_ring_1"
  unfolding comm_ring_1_ow_def class.comm_ring_1_def
  apply transfer_prover_start
  apply transfer_step+
  by blast

end


subsubsection‹Relativization›

context comm_ring_1_ow
begin

tts_context
  tts: (?'a to U)
  rewriting ctr_simps
  substituting comm_ring_1_ow_axioms and zero.not_empty
  applying 
    [
      OF 
        times_closed' 
        one_closed 
        plus_closed'
        zero_closed 
        minus_closed'
        add.inverse_closed''
    ]
begin

tts_lemma ring_normalization_rules:
  assumes "x  U"
  shows "-ow x = -ow 1ow *ow x" "y  U  x -ow y = x +ow -ow y"
    is comm_ring_1_class.ring_normalization_rules.
    
tts_lemma left_minus_one_mult_self:
  assumes "a  U"
  shows "(-ow 1ow) ^ow n *ow ((-ow 1ow) ^ow n *ow a) = a"
    is Power.comm_ring_1_class.left_minus_one_mult_self.

tts_lemma minus_power_mult_self:
  assumes "a  U"
  shows "(-ow a) ^ow n *ow (-ow a) ^ow n = a ^ow (2 * n)"
    is Power.comm_ring_1_class.minus_power_mult_self.

tts_lemma minus_one_mult_self: "(-ow 1ow) ^ow n *ow (-ow 1ow) ^ow n = 1ow"
  is comm_ring_1_class.minus_one_mult_self.

tts_lemma power2_commute:
  assumes "x  U" and "y  U"
  shows "(x -ow y) ^ow 2 = (y -ow x) ^ow 2"
    is comm_ring_1_class.power2_commute.

tts_lemma minus_dvd_iff:
  assumes "x  U" and "y  U"
  shows "(-ow x «dvd» y) = (x «dvd» y)"
    is comm_ring_1_class.minus_dvd_iff.

tts_lemma dvd_minus_iff:
  assumes "x  U" and "y  U"
  shows "(x «dvd» -ow y) = (x «dvd» y)"
    is comm_ring_1_class.dvd_minus_iff.

tts_lemma dvd_diff:
  assumes "x  U" and "y  U" and "z  U" and "x «dvd» y" and "x «dvd» z"
  shows "x «dvd» y -ow z"
    is comm_ring_1_class.dvd_diff.

end

end

text‹\newpage›

end