Theory SML_Semirings

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



subsection‹Semirings›


subsubsection‹Definitions and common properties›

locale semiring_ow =
  ab_semigroup_add_ow U plus + semigroup_mult_ow U times 
  for U :: "'ag set" and plus times +
  assumes distrib_right[simp]: 
    "⟦ a ∈ U; b ∈ U; c ∈ U ⟧ ⟹ (a +⇩o⇩w b) *⇩o⇩w c = a *⇩o⇩w c +⇩o⇩w b *⇩o⇩w c"
  assumes distrib_left[simp]: 
    "⟦ a ∈ U; b ∈ U; c ∈ U ⟧ ⟹ a *⇩o⇩w (b +⇩o⇩w c) = a *⇩o⇩w b +⇩o⇩w a *⇩o⇩w c"

lemma semiring_ow: "class.semiring = semiring_ow UNIV"
  unfolding 
    class.semiring_def semiring_ow_def
    class.semiring_axioms_def semiring_ow_axioms_def
    ab_semigroup_add_ow semigroup_mult_ow
  by simp


subsubsection‹Transfer rules›

context
  includes lifting_syntax
begin

lemma semiring_transfer[transfer_rule]:
  assumes[transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "((A ===> A ===> A) ===> (A ===> A ===> A) ===> (=)) 
      (semiring_ow (Collect (Domainp A))) class.semiring"
  unfolding 
    semiring_ow_def class.semiring_def
    semiring_ow_axioms_def class.semiring_axioms_def
  apply transfer_prover_start
  apply transfer_step+
  by simp

end


subsubsection‹Relativization›

context semiring_ow
begin

tts_context
  tts: (?'a to U)
  substituting semiring_ow_axioms
  eliminating through simp
begin

tts_lemma combine_common_factor:
  assumes "a ∈ U" and "e ∈ U" and "b ∈ U" and "c ∈ U"
  shows "a *⇩o⇩w e +⇩o⇩w (b *⇩o⇩w e +⇩o⇩w c) = (a +⇩o⇩w b) *⇩o⇩w e +⇩o⇩w c"
    is semiring_class.combine_common_factor.

end

end



subsection‹Commutative semirings›


subsubsection‹Definitions and common properties›

locale comm_semiring_ow = 
  ab_semigroup_add_ow U plus + ab_semigroup_mult_ow U times
  for U :: "'ag set" and plus times +
  assumes distrib: 
    "⟦a ∈ U; b ∈ U; c ∈ U⟧ ⟹ (a +⇩o⇩w b) *⇩o⇩w c = a *⇩o⇩w c +⇩o⇩w b *⇩o⇩w c"
begin

sublocale semiring_ow
proof
  fix a b c :: 'ag
  assume "a ∈ U" and "b ∈ U" and "c ∈ U"
  then show "(a +⇩o⇩w b) *⇩o⇩w c = a *⇩o⇩w c +⇩o⇩w b *⇩o⇩w c" by (simp only: distrib)
  show "a *⇩o⇩w (b +⇩o⇩w c) = a *⇩o⇩w b +⇩o⇩w a *⇩o⇩w c"
  proof-
    from ‹a ∈ U› ‹b ∈ U› ‹c ∈ U› have "a *⇩o⇩w (b +⇩o⇩w c) = (b +⇩o⇩w c) *⇩o⇩w a" 
      by (simp add: mult_commute)
    with ‹a ∈ U› ‹b ∈ U› ‹c ∈ U› have "a *⇩o⇩w (b +⇩o⇩w c) = b *⇩o⇩w a +⇩o⇩w c *⇩o⇩w a" 
      by (simp only: distrib)
    with ‹a ∈ U› ‹b ∈ U› ‹c ∈ U› show ?thesis  by (simp only: mult_commute)
  qed
qed

end

lemma comm_semiring_ow: "class.comm_semiring = comm_semiring_ow UNIV"
  unfolding 
    class.comm_semiring_def comm_semiring_ow_def
    class.comm_semiring_axioms_def comm_semiring_ow_axioms_def
    ab_semigroup_add_ow ab_semigroup_mult_ow
  by simp


subsubsection‹Transfer rules›

context
  includes lifting_syntax
begin

lemma comm_semiring_transfer[transfer_rule]:
  assumes[transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "((A ===> A ===> A) ===> (A ===> A ===> A) ===> (=)) 
      (comm_semiring_ow (Collect (Domainp A))) class.comm_semiring"
    (is "?PR (comm_semiring_ow (Collect (Domainp A))) class.comm_semiring")
  unfolding 
    comm_semiring_ow_def class.comm_semiring_def
    comm_semiring_ow_axioms_def class.comm_semiring_axioms_def
  apply transfer_prover_start
  apply transfer_step+
  by simp

end



subsection‹Semirings with zero›


subsubsection‹Definitions and further results›

locale mult_zero_ow = times_ow U times + zero_ow U zero
  for U :: "'ag set" and times zero +
  assumes mult_zero_left[simp]: "a ∈ U ⟹ 0⇩o⇩w *⇩o⇩w a = 0⇩o⇩w"
  assumes mult_zero_right[simp]: "a ∈ U ⟹ a *⇩o⇩w 0⇩o⇩w = 0⇩o⇩w"

lemma mult_zero_ow: "class.mult_zero = mult_zero_ow UNIV"
  unfolding 
    class.mult_zero_def mult_zero_ow_def mult_zero_ow_axioms_def
    times_ow_def zero_ow_def neutral_ow_def
  by simp

locale semiring_0_ow = 
  semiring_ow U plus times + 
  comm_monoid_add_ow U plus zero + 
  mult_zero_ow U times zero
  for U :: "'ag set" and plus zero times 

lemma semiring_0_ow: "class.semiring_0 = semiring_0_ow UNIV"
  unfolding 
    class.semiring_0_def semiring_0_ow_def  
    mult_zero_ow comm_monoid_add_ow semiring_ow
  by (auto simp: conj_commute)


subsubsection‹Transfer rules›

context
  includes lifting_syntax
begin

lemma semiring_0_transfer[transfer_rule]:
  assumes[transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "((A ===> A ===> A) ===> A ===> (A ===> A ===> A) ===> (=)) 
      (semiring_0_ow (Collect (Domainp A))) class.semiring_0"
    (is "?PR (semiring_0_ow (Collect (Domainp A))) class.semiring_0")
proof-
  let ?semiring_0 =
    "(
      λplus zero times. 
        class.semiring_0 plus zero times ∧
        (∀a b. a ∈ UNIV ⟶ b ∈ UNIV ⟶ times a b ∈ UNIV) ∧ zero ∈ UNIV
    )" 
  have "?PR (semiring_0_ow (Collect (Domainp A))) ?semiring_0" 
    unfolding
      semiring_0_ow_def  class.semiring_0_def
      mult_zero_ow_def class.mult_zero_def
      mult_zero_ow_axioms_def
      times_ow_def zero_ow_def neutral_ow_def 
    apply transfer_prover_start
    apply transfer_step+
    by blast
  thus ?thesis by simp
qed

end



subsection‹Commutative semirings with zero›


subsubsection‹Definitions and common properties›

locale comm_semiring_0_ow = 
  comm_semiring_ow U plus times +  
  comm_monoid_add_ow U plus zero + 
  mult_zero_ow U times zero
  for U :: "'ag set" and plus zero times 
begin

sublocale semiring_0_ow by unfold_locales

end

lemma comm_semiring_0_ow: "class.comm_semiring_0 = comm_semiring_0_ow UNIV"
  unfolding 
    class.comm_semiring_0_def comm_semiring_0_ow_def
    comm_monoid_add_ow comm_semiring_ow mult_zero_ow
  by (auto simp: conj_commute)


subsubsection‹Transfer rules›

context
  includes lifting_syntax
begin

lemma comm_semiring_0_transfer[transfer_rule]:
  assumes[transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "((A ===> A ===> A) ===> A ===> (A ===> A ===> A) ===> (=)) 
      (comm_semiring_0_ow (Collect (Domainp A))) class.comm_semiring_0"
    (is "?PR (comm_semiring_0_ow (Collect (Domainp A))) class.comm_semiring_0")
proof-
  let ?comm_semiring_0 =
    "(
      λplus zero times. 
        class.comm_semiring_0 plus zero times ∧
        (∀a b. a ∈ UNIV ⟶ b ∈ UNIV ⟶ times a b ∈ UNIV) ∧ zero ∈ UNIV
    )" 
  have "?PR (comm_semiring_0_ow (Collect (Domainp A))) ?comm_semiring_0" 
    unfolding
      comm_semiring_0_ow_def class.comm_semiring_0_def
      mult_zero_ow_def class.mult_zero_def
      mult_zero_ow_axioms_def
      times_ow_def zero_ow_def neutral_ow_def 
    apply transfer_prover_start
    apply transfer_step+
    by blast
  thus ?thesis by simp
qed

end



subsection‹Cancellative semirings with zero›


subsubsection‹Definitions and common properties›

locale semiring_0_cancel_ow =
  semiring_ow U plus times + cancel_comm_monoid_add_ow U plus minus zero
  for U :: "'ag set" and plus minus zero times
begin

sublocale semiring_0_ow 
proof
  fix a
  show "a ∈ U ⟹ 0⇩o⇩w *⇩o⇩w a = 0⇩o⇩w"
  proof-
    assume "a ∈ U"
    have "0⇩o⇩w *⇩o⇩w a ∈ U" by (simp add: ‹a ∈ U› times_closed') 
    have "0⇩o⇩w *⇩o⇩w a +⇩o⇩w 0⇩o⇩w *⇩o⇩w a = 0⇩o⇩w *⇩o⇩w a +⇩o⇩w 0⇩o⇩w" 
      by (simp add: ‹a ∈ U› ‹0⇩o⇩w *⇩o⇩w a ∈ U› distrib_right[symmetric])
    then show ?thesis 
      unfolding add_left_cancel[OF ‹0⇩o⇩w *⇩o⇩w a ∈ U› ‹0⇩o⇩w *⇩o⇩w a ∈ U› zero_closed]
      by assumption
  qed
  show "a ∈ U ⟹ a *⇩o⇩w 0⇩o⇩w = 0⇩o⇩w"
  proof-
    assume "a ∈ U"
    have "a *⇩o⇩w 0⇩o⇩w ∈ U" by (simp add: ‹a ∈ U› times_closed')
    have "a *⇩o⇩w 0⇩o⇩w +⇩o⇩w a *⇩o⇩w 0⇩o⇩w = a *⇩o⇩w 0⇩o⇩w +⇩o⇩w 0⇩o⇩w"
      by (simp add: ‹a ∈ U› ‹a *⇩o⇩w 0⇩o⇩w ∈ U› distrib_left[symmetric])
    then show ?thesis
      unfolding add_left_cancel[OF ‹a *⇩o⇩w 0⇩o⇩w ∈ U› ‹a *⇩o⇩w 0⇩o⇩w ∈ U› zero_closed]
      by assumption
  qed
qed

end

lemma semiring_0_cancel_ow: 
  "class.semiring_0_cancel = semiring_0_cancel_ow UNIV"
  unfolding 
    class.semiring_0_cancel_def 
    semiring_0_cancel_ow_def
    cancel_comm_monoid_add_ow semiring_ow
  by (simp add: conj_commute)


subsubsection‹Transfer rules›

context
  includes lifting_syntax
begin

lemma semiring_0_cancel_transfer[transfer_rule]: 
  assumes[transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "(
      (A ===> A ===> A) ===> 
      (A ===> A ===> A) ===> 
      A ===> 
      (A ===> A ===> A) ===> 
      (=)
    ) (semiring_0_cancel_ow (Collect (Domainp A))) class.semiring_0_cancel"
  unfolding semiring_0_cancel_ow_def class.semiring_0_cancel_def
  apply transfer_prover_start
  apply transfer_step+
  by auto

end



subsection‹Commutative cancellative semirings with zero›


subsubsection‹Definitions and common properties›

locale comm_semiring_0_cancel_ow = 
  comm_semiring_ow U plus times + 
  cancel_comm_monoid_add_ow U plus minus zero
  for U :: "'ag set" and plus  minus zero times 
begin

sublocale semiring_0_cancel_ow by unfold_locales

sublocale comm_semiring_0_ow by unfold_locales

end

lemma comm_semiring_0_cancel_ow: 
  "class.comm_semiring_0_cancel = comm_semiring_0_cancel_ow UNIV"
  unfolding 
    class.comm_semiring_0_cancel_def comm_semiring_0_cancel_ow_def
    cancel_comm_monoid_add_ow comm_semiring_ow
  by (simp add: conj_commute)


subsubsection‹Transfer rules›

context
  includes lifting_syntax
begin

lemma comm_semiring_0_cancel_transfer[transfer_rule]:
  assumes[transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "(
      (A ===> A ===> A) ===> 
      (A ===> A ===> A) ===> 
      A ===> 
      (A ===> A ===> A) ===> 
      (=)
    ) 
    (comm_semiring_0_cancel_ow (Collect (Domainp A))) 
    class.comm_semiring_0_cancel"
  unfolding comm_semiring_0_cancel_ow_def class.comm_semiring_0_cancel_def
  apply transfer_prover_start
  apply transfer_step+
  by auto

end



subsection‹Class \<^class>‹zero_neq_one››


subsubsection‹Definitions and common properties›

locale zero_neq_one_ow = 
  zero_ow U zero + one_ow U one
  for U :: "'ag set" and one (‹1⇩o⇩w›) and zero (‹0⇩o⇩w›)  +
  assumes zero_neq_one[simp]: "0⇩o⇩w ≠ 1⇩o⇩w"

lemma zero_neq_one_ow: "class.zero_neq_one = zero_neq_one_ow UNIV"
  unfolding 
    class.zero_neq_one_def zero_neq_one_ow_def
    zero_neq_one_ow_axioms_def
    one_ow_def zero_ow_def neutral_ow_def
  by simp

ud ‹zero_neq_one.of_bool› (‹(with _ _ : «of'_bool» _)› [1000, 999, 1000] 10)
ud of_bool' ‹of_bool›

ctr parametricity
  in of_bool.with_def

context zero_neq_one_ow
begin

abbreviation of_bool where "of_bool ≡ of_bool.with 1⇩o⇩w 0⇩o⇩w"

end


subsubsection‹Transfer rules›

context
  includes lifting_syntax
begin

lemma zero_neq_one_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A"  
  shows 
    "(A ===> A ===> (=)) 
      (zero_neq_one_ow (Collect (Domainp A))) class.zero_neq_one" 
    (is "?PR (zero_neq_one_ow (Collect (Domainp A))) class.zero_neq_one")
proof-
  let ?zero_neq_one = 
    "(λone zero. class.zero_neq_one one zero ∧ one ∈ UNIV ∧ zero ∈ UNIV)"
  have "?PR (zero_neq_one_ow (Collect (Domainp A))) ?zero_neq_one"
    unfolding 
      zero_neq_one_ow_def class.zero_neq_one_def
      zero_neq_one_ow_axioms_def
      zero_ow_def one_ow_def neutral_ow_def
    apply transfer_prover_start
    apply transfer_step+
    by auto
  thus ?thesis by simp
qed

end


subsubsection‹Relativization›

context zero_neq_one_ow
begin

tts_context
  tts: (?'a to U) 
  rewriting ctr_simps
  substituting zero_neq_one_ow_axioms
  eliminating through simp
begin

tts_lemma split_of_bool_asm:
  shows "P (of_bool p) = (¬ (p ∧ ¬ P 1⇩o⇩w ∨ ¬ p ∧ ¬ P 0⇩o⇩w))"
    is zero_neq_one_class.split_of_bool_asm.
    
tts_lemma of_bool_eq_iff:
  shows "(of_bool p = local.of_bool q) = (p = q)"
    is zero_neq_one_class.of_bool_eq_iff.
    
tts_lemma split_of_bool:
  shows "P (of_bool p) = ((p ⟶ P 1⇩o⇩w) ∧ (¬ p ⟶ P 0⇩o⇩w))"
    is zero_neq_one_class.split_of_bool.

tts_lemma one_neq_zero: "1⇩o⇩w ≠ 0⇩o⇩w"
  is zero_neq_one_class.one_neq_zero.
    
tts_lemma of_bool_eq:
  shows "of_bool False = 0⇩o⇩w" 
    is zero_neq_one_class.of_bool_eq(1)
    and "of_bool True = 1⇩o⇩w"
    is zero_neq_one_class.of_bool_eq(2).

end

end



subsection‹Semirings with zero and one (rigs)›


subsubsection‹Definitions and commmon properties›

locale semiring_1_ow =
  zero_neq_one_ow U one zero +
  semiring_0_ow U plus zero times + 
  monoid_mult_ow U one times
  for U :: "'ag set" and one times plus zero

lemma semiring_1_ow: "class.semiring_1 = semiring_1_ow UNIV"
  unfolding 
    class.semiring_1_def semiring_1_ow_def
    monoid_mult_ow semiring_0_ow zero_neq_one_ow
  by (auto simp: conj_commute)

ud ‹semiring_1.of_nat› (‹(with _ _ _ : «of'_nat» _)› [1000, 999, 998, 1000] 10)
ud of_nat' ‹of_nat›

ud ‹semiring_1.Nats› (‹(with _ _ _ : ℕ)› [1000, 999, 998] 10)
ud Nats' ‹Nats›

ctr parametricity
  in of_nat_ow: of_nat.with_def
    and Nats_ow: Nats.with_def

context semiring_1_ow
begin

abbreviation of_nat where "of_nat ≡ of_nat.with 1⇩o⇩w (+⇩o⇩w) 0⇩o⇩w"
abbreviation Nats (‹«ℕ»›) where "«ℕ» ≡ Nats.with 1⇩o⇩w (+⇩o⇩w) 0⇩o⇩w"
notation Nats (‹«ℕ»›)

end

context semiring_1
begin

lemma Nat_ss_UNIV: "ℕ ⊆ UNIV" by simp

end


subsubsection‹Transfer rules›

context
  includes lifting_syntax
begin

lemma semiring_1_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "(A ===> (A ===> A ===> A) ===> (A ===> A ===> A) ===> A ===> (=)) 
      (semiring_1_ow (Collect (Domainp A))) class.semiring_1"
  unfolding semiring_1_ow_def class.semiring_1_def
  apply transfer_prover_start
  apply transfer_step+
  by auto

end


subsubsection‹Relativization›

context semiring_1_ow
begin

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

tts_lemma Nat_ss_UNIV[simp]:
  shows "«ℕ» ⊆ U"
    is Nat_ss_UNIV.

end

lemma Nat_closed[simp, intro]: "a ∈ «ℕ» ⟹ a ∈ U" using Nat_ss_UNIV by blast

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

tts_lemma mult_of_nat_commute:
  assumes "y ∈ U"
  shows "of_nat x *⇩o⇩w y = y *⇩o⇩w of_nat x"
    is semiring_1_class.mult_of_nat_commute.

tts_lemma of_bool_conj: "of_bool (P ∧ Q) = of_bool P *⇩o⇩w of_bool Q"
  is semiring_1_class.of_bool_conj.

tts_lemma power_0_left: "0⇩o⇩w ^⇩o⇩w n = (if n = 0 then 1⇩o⇩w else 0⇩o⇩w)"
  is semiring_1_class.power_0_left.

tts_lemma of_nat_power: "of_nat ((with 1 (*) : m ^⇩o⇩w n)) = of_nat m ^⇩o⇩w n"
  is semiring_1_class.of_nat_power.

tts_lemma of_nat_of_bool: "of_nat (with 1 0 : «of_bool» P) = of_bool P"
  is semiring_1_class.of_nat_of_bool.

tts_lemma of_nat_in_Nats: "of_nat n ∈ «ℕ»"
  is semiring_1_class.of_nat_in_Nats.

tts_lemma zero_power2: "0⇩o⇩w ^⇩o⇩w 2 = 0⇩o⇩w"
  is semiring_1_class.zero_power2.

tts_lemma power_0_Suc: "0⇩o⇩w ^⇩o⇩w Suc n = 0⇩o⇩w"
  is semiring_1_class.power_0_Suc.

tts_lemma zero_power:
  assumes "0 < n"
  shows "0⇩o⇩w ^⇩o⇩w n = 0⇩o⇩w"
    is semiring_1_class.zero_power.

tts_lemma one_power2: "1⇩o⇩w ^⇩o⇩w 2 = 1⇩o⇩w"
  is semiring_1_class.one_power2.

tts_lemma of_nat_simps:
  shows "of_nat 0 = 0⇩o⇩w" 
    is semiring_1_class.of_nat_simps(1)
    and "of_nat (Suc m) = 1⇩o⇩w +⇩o⇩w of_nat m"
    is semiring_1_class.of_nat_simps(2).

tts_lemma of_nat_mult: "of_nat (m * n) = of_nat m *⇩o⇩w of_nat n"
  is semiring_1_class.of_nat_mult.

tts_lemma Nats_induct:
  assumes "x ∈ «ℕ»" and "⋀n. P (of_nat n)"
  shows "P x"
    is semiring_1_class.Nats_induct.

tts_lemma of_nat_add: "of_nat (m + n) = of_nat m +⇩o⇩w of_nat n"
  is semiring_1_class.of_nat_add.

tts_lemma of_nat_Suc: "of_nat (Suc m) = 1⇩o⇩w +⇩o⇩w of_nat m"
  is semiring_1_class.of_nat_Suc.

tts_lemma Nats_cases:
  assumes "x ∈ «ℕ»" 
  obtains (of_nat) n where "x = of_nat n"
    given semiring_1_class.Nats_cases by auto

tts_lemma Nats_mult:
  assumes "a ∈ «ℕ»" and "b ∈ «ℕ»"
  shows "a *⇩o⇩w b ∈ «ℕ»"
    is semiring_1_class.Nats_mult.

tts_lemma of_nat_1: "of_nat 1 = 1⇩o⇩w"
  is semiring_1_class.of_nat_1.

tts_lemma of_nat_0: "of_nat 0 = 0⇩o⇩w"
  is semiring_1_class.of_nat_0.

tts_lemma Nats_add:
  assumes "a ∈ «ℕ»" and "b ∈ «ℕ»"
  shows "a +⇩o⇩w b ∈ «ℕ»"
    is semiring_1_class.Nats_add.

tts_lemma Nats_1: "1⇩o⇩w ∈ «ℕ»"
  is semiring_1_class.Nats_1.

tts_lemma Nats_0: "0⇩o⇩w ∈ «ℕ»"
  is semiring_1_class.Nats_0.

end

end



subsection‹Commutative rigs›


subsubsection‹Definitions and common properties›

locale comm_semiring_1_ow = 
  zero_neq_one_ow U one zero +
  comm_semiring_0_ow U plus zero times +
  comm_monoid_mult_ow U times one
  for U :: "'ag set" and times one plus zero  
begin

sublocale semiring_1_ow by unfold_locales

end

lemma comm_semiring_1_ow: "class.comm_semiring_1 = comm_semiring_1_ow UNIV"
  unfolding 
    class.comm_semiring_1_def comm_semiring_1_ow_def
    comm_monoid_mult_ow comm_semiring_0_ow zero_neq_one_ow
  by (auto simp: conj_commute)


subsubsection‹Transfer rules›

context
  includes lifting_syntax
begin

lemma comm_semiring_1_transfer[transfer_rule]:
  assumes[transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "((A ===> A ===> A) ===> A ===> (A ===> A ===> A) ===> A ===> (=)) 
      (comm_semiring_1_ow (Collect (Domainp A))) class.comm_semiring_1"
  unfolding comm_semiring_1_ow_def class.comm_semiring_1_def
  apply transfer_prover_start
  apply transfer_step+
  by auto

end


subsubsection‹Relativization›

context comm_semiring_1_ow
begin

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

tts_lemma semiring_normalization_rules:
  shows 
    "⟦a ∈ U; m ∈ U; b ∈ U⟧ ⟹ a *⇩o⇩w m +⇩o⇩w b *⇩o⇩w m = (a +⇩o⇩w b) *⇩o⇩w m"
    "⟦a ∈ U; m ∈ U⟧ ⟹ a *⇩o⇩w m +⇩o⇩w m = (a +⇩o⇩w 1⇩o⇩w) *⇩o⇩w m"
    "⟦m ∈ U; a ∈ U⟧ ⟹ m +⇩o⇩w a *⇩o⇩w m = (a +⇩o⇩w 1⇩o⇩w) *⇩o⇩w m"
    "m ∈ U ⟹ m +⇩o⇩w m = (1⇩o⇩w +⇩o⇩w 1⇩o⇩w) *⇩o⇩w m"
    "a ∈ U ⟹ 0⇩o⇩w +⇩o⇩w a = a"
    "a ∈ U ⟹ a +⇩o⇩w 0⇩o⇩w = a"
    "⟦a ∈ U; b ∈ U⟧ ⟹ a *⇩o⇩w b = b *⇩o⇩w a"
    "⟦a ∈ U; b ∈ U; c ∈ U⟧ ⟹ (a +⇩o⇩w b) *⇩o⇩w c = a *⇩o⇩w c +⇩o⇩w b *⇩o⇩w c"
    "a ∈ U ⟹ 0⇩o⇩w *⇩o⇩w a = 0⇩o⇩w"
    "a ∈ U ⟹ a *⇩o⇩w 0⇩o⇩w = 0⇩o⇩w"
    "a ∈ U ⟹ 1⇩o⇩w *⇩o⇩w a = a"
    "a ∈ U ⟹ a *⇩o⇩w 1⇩o⇩w = a"
    "⟦lx ∈ U; ly ∈ U; rx ∈ U; ry ∈ U⟧ ⟹ 
      lx *⇩o⇩w ly *⇩o⇩w (rx *⇩o⇩w ry) = lx *⇩o⇩w rx *⇩o⇩w (ly *⇩o⇩w ry)"
    "⟦lx ∈ U; ly ∈ U; rx ∈ U; ry ∈ U⟧ ⟹ 
      lx *⇩o⇩w ly *⇩o⇩w (rx *⇩o⇩w ry) = lx *⇩o⇩w (ly *⇩o⇩w (rx *⇩o⇩w ry))"
    "⟦lx ∈ U; ly ∈ U; rx ∈ U; ry ∈ U⟧ ⟹ 
      lx *⇩o⇩w ly *⇩o⇩w (rx *⇩o⇩w ry) = rx *⇩o⇩w (lx *⇩o⇩w ly *⇩o⇩w ry)"
    "⟦lx ∈ U; ly ∈ U; rx ∈ U⟧ ⟹ lx *⇩o⇩w ly *⇩o⇩w rx = lx *⇩o⇩w rx *⇩o⇩w ly"
    "⟦lx ∈ U; ly ∈ U; rx ∈ U⟧ ⟹ lx *⇩o⇩w ly *⇩o⇩w rx = lx *⇩o⇩w (ly *⇩o⇩w rx)"
    "⟦lx ∈ U; rx ∈ U; ry ∈ U⟧ ⟹ lx *⇩o⇩w (rx *⇩o⇩w ry) = lx *⇩o⇩w rx *⇩o⇩w ry"
    "⟦lx ∈ U; rx ∈ U; ry ∈ U⟧ ⟹ lx *⇩o⇩w (rx *⇩o⇩w ry) = rx *⇩o⇩w (lx *⇩o⇩w ry)"
    "⟦a ∈ U; b ∈ U; c ∈ U; d ∈ U⟧ ⟹ 
      a +⇩o⇩w b +⇩o⇩w (c +⇩o⇩w d) = a +⇩o⇩w c +⇩o⇩w (b +⇩o⇩w d)"
    "⟦a ∈ U; b ∈ U; c ∈ U⟧ ⟹ a +⇩o⇩w b +⇩o⇩w c = a +⇩o⇩w (b +⇩o⇩w c)"
    "⟦a ∈ U; c ∈ U; d ∈ U⟧ ⟹ a +⇩o⇩w (c +⇩o⇩w d) = c +⇩o⇩w (a +⇩o⇩w d)"
    "⟦a ∈ U; b ∈ U; c ∈ U⟧ ⟹ a +⇩o⇩w b +⇩o⇩w c = a +⇩o⇩w c +⇩o⇩w b"
    "⟦a ∈ U; c ∈ U⟧ ⟹ a +⇩o⇩w c = c +⇩o⇩w a"
    "⟦a ∈ U; c ∈ U; d ∈ U⟧ ⟹ a +⇩o⇩w (c +⇩o⇩w d) = a +⇩o⇩w c +⇩o⇩w d"
    "x ∈ U ⟹ x ^⇩o⇩w p *⇩o⇩w x ^⇩o⇩w q = x ^⇩o⇩w (p + q)"
    "x ∈ U ⟹ x *⇩o⇩w x ^⇩o⇩w q = x ^⇩o⇩w Suc q"
    "x ∈ U ⟹ x ^⇩o⇩w q *⇩o⇩w x = x ^⇩o⇩w Suc q"
    "x ∈ U ⟹ x *⇩o⇩w x = x ^⇩o⇩w 2"
    "⟦x ∈ U; y ∈ U⟧ ⟹ (x *⇩o⇩w y) ^⇩o⇩w q = x ^⇩o⇩w q *⇩o⇩w y ^⇩o⇩w q"
    "x ∈ U ⟹ (x ^⇩o⇩w p) ^⇩o⇩w q = x ^⇩o⇩w (p * q)"
    "x ∈ U ⟹ x ^⇩o⇩w 0 = 1⇩o⇩w"
    "x ∈ U ⟹ x ^⇩o⇩w 1 = x"
    "⟦x ∈ U; y ∈ U; z ∈ U⟧ ⟹ x *⇩o⇩w (y +⇩o⇩w z) = x *⇩o⇩w y +⇩o⇩w x *⇩o⇩w z"
    "x ∈ U ⟹ x ^⇩o⇩w Suc q = x *⇩o⇩w x ^⇩o⇩w q"
    "x ∈ U ⟹ x ^⇩o⇩w (2 * n) = x ^⇩o⇩w n *⇩o⇩w x ^⇩o⇩w n"
    is comm_semiring_1_class.semiring_normalization_rules.

tts_lemma le_imp_power_dvd:
  assumes "a ∈ U" and "m ≤ n"
  shows "a ^⇩o⇩w m «dvd» a ^⇩o⇩w n"
    is comm_semiring_1_class.le_imp_power_dvd.

tts_lemma dvd_0_left_iff:
  assumes "a ∈ U"
  shows "(0⇩o⇩w «dvd» a) = (a = 0⇩o⇩w)"
    is comm_semiring_1_class.dvd_0_left_iff.

tts_lemma dvd_power_same:
  assumes "x ∈ U" and "y ∈ U" and "x «dvd» y"
  shows "x ^⇩o⇩w n «dvd» y ^⇩o⇩w n"
    is comm_semiring_1_class.dvd_power_same.

tts_lemma power_le_dvd:
  assumes "a ∈ U" and "b ∈ U" and "a ^⇩o⇩w n «dvd» b" and "m ≤ n"
  shows "a ^⇩o⇩w m «dvd» b"
    is comm_semiring_1_class.power_le_dvd.

tts_lemma dvd_0_right:
  assumes "a ∈ U"
  shows "a «dvd» 0⇩o⇩w"
    is comm_semiring_1_class.dvd_0_right.

tts_lemma dvd_0_left:
  assumes "a ∈ U" and "0⇩o⇩w «dvd» a"
  shows "a = 0⇩o⇩w"
    is comm_semiring_1_class.dvd_0_left.

tts_lemma dvd_power:
  assumes "x ∈ U" and "0 < n ∨ x = 1⇩o⇩w"
  shows "x «dvd» x ^⇩o⇩w n"
    is comm_semiring_1_class.dvd_power.

tts_lemma dvd_add:
  assumes "a ∈ U" and "b ∈ U" and "c ∈ U" and "a «dvd» b" and "a «dvd» c"
  shows "a «dvd» b +⇩o⇩w c"
    is comm_semiring_1_class.dvd_add.

end

end



subsection‹Cancellative rigs›


subsubsection‹Definitions and common properties›

locale semiring_1_cancel_ow =
  semiring_ow U plus times +
  cancel_comm_monoid_add_ow U plus minus zero +
  zero_neq_one_ow U one zero +
  monoid_mult_ow U one times
  for U :: "'ag set" and plus minus zero one times
begin

sublocale semiring_0_cancel_ow ..
sublocale semiring_1_ow ..

end

lemma semiring_1_cancel_ow: 
  "class.semiring_1_cancel = semiring_1_cancel_ow UNIV"
  unfolding 
    class.semiring_1_cancel_def semiring_1_cancel_ow_def
    cancel_comm_monoid_add_ow monoid_mult_ow semiring_ow zero_neq_one_ow
  by (force simp: conj_commute)


subsubsection‹Transfer rules›

context
  includes lifting_syntax
begin

lemma semiring_1_cancel_transfer[transfer_rule]:
  includes lifting_syntax
  assumes[transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "(
      (A ===> A ===> A) ===> 
      (A ===> A ===> A) ===> 
      A ===> 
      A ===> 
      (A ===> A ===> A) ===> 
      (=)
    ) (semiring_1_cancel_ow (Collect (Domainp A))) class.semiring_1_cancel"
  unfolding semiring_1_cancel_ow_def class.semiring_1_cancel_def
  apply transfer_prover_start
  apply transfer_step+
  by blast

end



subsection‹Commutative cancellative rigs›


subsubsection‹Definitions and common properties›

locale comm_semiring_1_cancel_ow =
  comm_semiring_ow U plus times + 
  cancel_comm_monoid_add_ow U plus minus zero + 
  zero_neq_one_ow U one zero +  
  comm_monoid_mult_ow U times one 
  for U :: "'ag set" and plus minus zero times one + 
  assumes right_diff_distrib'[algebra_simps]: 
    "⟦ a ∈ U; b ∈ U; c ∈ U ⟧ ⟹ a *⇩o⇩w (b -⇩o⇩w c) = a *⇩o⇩w b -⇩o⇩w a *⇩o⇩w c" 
begin

sublocale semiring_1_cancel_ow ..
sublocale comm_semiring_0_cancel_ow ..
sublocale comm_semiring_1_ow ..

end


subsubsection‹Transfer rules›

context 
  includes lifting_syntax
begin

lemma comm_semiring_1_cancel_transfer[transfer_rule]:
  assumes[transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "(
      (A ===> A ===> A) ===> 
      (A ===> A ===> A) ===> 
      A ===> 
      (A ===> A ===> A) ===> 
      A ===> 
      (=)
    ) 
    (comm_semiring_1_cancel_ow (Collect (Domainp A))) 
    class.comm_semiring_1_cancel"
  unfolding 
    comm_semiring_1_cancel_ow_def class.comm_semiring_1_cancel_def
    comm_semiring_1_cancel_ow_axioms_def 
    class.comm_semiring_1_cancel_axioms_def
  apply transfer_prover_start
  apply transfer_step+
  by blast

end


subsubsection‹Relativization›

context comm_semiring_1_cancel_ow
begin

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

tts_lemma dvd_add_times_triv_right_iff:
  assumes "a ∈ U" and "b ∈ U" and "c ∈ U"
  shows "(a «dvd» b +⇩o⇩w c *⇩o⇩w a) = (a «dvd» b)"
  is comm_semiring_1_cancel_class.dvd_add_times_triv_right_iff.

tts_lemma dvd_add_times_triv_left_iff:
  assumes "a ∈ U" and "c ∈ U" and "b ∈ U"
  shows "(a «dvd» c *⇩o⇩w a +⇩o⇩w b) = (a «dvd» b)"
    is comm_semiring_1_cancel_class.dvd_add_times_triv_left_iff.

tts_lemma dvd_add_triv_right_iff:
  assumes "a ∈ U" and "b ∈ U"
  shows "(a «dvd» b +⇩o⇩w a) = (a «dvd» b)"
    is comm_semiring_1_cancel_class.dvd_add_triv_right_iff.

tts_lemma dvd_add_triv_left_iff:
  assumes "a ∈ U" and "b ∈ U"
  shows "(a «dvd» a +⇩o⇩w b) = (a «dvd» b)"
    is comm_semiring_1_cancel_class.dvd_add_triv_left_iff.

tts_lemma left_diff_distrib':
  assumes "b ∈ U" and "c ∈ U" and "a ∈ U"
  shows "(b -⇩o⇩w c) *⇩o⇩w a = b *⇩o⇩w a -⇩o⇩w c *⇩o⇩w a"
    is comm_semiring_1_cancel_class.left_diff_distrib'.

tts_lemma dvd_add_right_iff:
  assumes "a ∈ U" and "b ∈ U" and "c ∈ U" and "a «dvd» b"
  shows "(a «dvd» b +⇩o⇩w c) = (a «dvd» c)"
    is comm_semiring_1_cancel_class.dvd_add_right_iff.

tts_lemma dvd_add_left_iff:
  assumes "a ∈ U" and "c ∈ U" and "b ∈ U" and "a «dvd» c"
  shows "(a «dvd» b +⇩o⇩w c) = (a «dvd» b)"
    is comm_semiring_1_cancel_class.dvd_add_left_iff.

end

end

text‹\newpage›

end