Theory SML_Monoids

(* Title: Examples/SML_Relativization/Algebra/SML_Monoids.thy
   Author: Mihails Milehins
   Copyright 2021 (C) Mihails Milehins
*)
section‹Relativization of the results about monoids›
theory SML_Monoids
  imports 
    SML_Semigroups
    "../Foundations/Product_Type_Ext"
    "../Foundations/Transfer_Ext"
begin



subsection‹Simple monoids›


subsubsection‹Definitions and common properties›

locale neutral_ow =
  fixes U :: "'ag set" and z :: "'ag" (‹1ow›)
  assumes z_closed[simp]: "1ow ∈ U" 
begin

notation z (‹1ow›)

tts_register_sbts ‹1ow› | U by (meson Domainp.cases z_closed)

lemma not_empty[simp]: "U ≠ {}" using z_closed by blast

lemma neutral_map: "(λy. 1ow) ` A ⊆ U" using z_closed by auto

end

locale monoid_ow = semigroup_ow U f + neutral_ow U z
  for U :: "'ag set" and f z +
  assumes left_neutral_mow[simp]: "a ∈ U ⟹ (1ow *ow a) = a"
    and right_neutral_mow[simp]: "a ∈ U ⟹ (a *ow 1ow) = a"

locale zero_ow = zero: neutral_ow U zero
  for U :: "'ag set" and zero :: "'ag" (‹0ow›)
begin

notation zero (‹0ow›)

lemma zero_closed: "0ow ∈ U" by (rule zero.z_closed)

end

lemma monoid_ow: "monoid = monoid_ow UNIV"
  unfolding 
    monoid_def monoid_ow_def monoid_axioms_def monoid_ow_axioms_def
    neutral_ow_def
    semigroup_ow
  by simp

locale one_ow = one: neutral_ow U one
  for U :: "'ag set" and one :: "'ag" (‹1ow›)
begin

notation one (‹1ow›)

lemma one_closed: "1ow ∈ U" by (rule one.z_closed)

end

locale power_ow = one_ow U one + times_ow U times
  for U :: "'ag set" and one :: "'ag" (‹1ow›) and times (infixl ‹*ow› 70)

primrec power_with :: "['a, ['a, 'a] ⇒ 'a, 'a, nat] ⇒ 'a"
  (‹'(/with _ _ : _ ^ow _/')› [1000, 999, 1000, 1000] 10)
  where
    power_0: "power_with one times a 0 = one" for one times
  | power_Suc: "power_with one times a (Suc n) = 
      times a (power_with one times a n)" for one times

lemma power_with[ud_with]: "power = power_with 1 (*)"
  apply(intro ext)
  subgoal for x n by (induction n) auto
  done

context power_ow
begin

abbreviation power (‹(_ ^ow _)› [81, 80] 80) where 
  "power ≡ power_with 1ow (*ow)"

end

locale monoid_add_ow =
  semigroup_add_ow U plus + zero_ow U zero for U :: "'ag set" and plus zero +
  assumes add_0_left: "a ∈ U ⟹ (0ow +ow a) = a"
  assumes add_0_right: "a ∈ U ⟹ (a +ow 0ow) = a"
begin

sublocale add: monoid_ow U ‹(+ow)› ‹0ow› 
  by unfold_locales (simp add: add_0_left add_0_right)+

end

lemma monoid_add_ow: "class.monoid_add = monoid_add_ow UNIV"
  unfolding 
    class.monoid_add_def monoid_add_ow_def
    class.monoid_add_axioms_def monoid_add_ow_axioms_def
    zero_ow_def neutral_ow_def
    semigroup_add_ow
  by simp

locale monoid_mult_ow = semigroup_mult_ow U times + one_ow U one 
  for U :: "'ag set" and one times  +
  assumes mult_1_left: "a ∈ U ⟹ (1ow *ow a) = a"
  assumes mult_1_right: "a ∈ U ⟹ (a *ow 1ow) = a"
begin

sublocale mult: monoid_ow U ‹(*ow)› ‹1ow› 
  by unfold_locales (simp add: mult_1_left mult_1_right)+

sublocale power_ow ..

end

lemma monoid_mult_ow: "class.monoid_mult = monoid_mult_ow UNIV"
  unfolding 
    class.monoid_mult_def monoid_mult_ow_def
    class.monoid_mult_axioms_def monoid_mult_ow_axioms_def
    one_ow_def neutral_ow_def
    semigroup_mult_ow
  by simp


subsubsection‹Transfer rules›

context
  includes lifting_syntax
begin

lemma monoid_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "((A ===> A ===> A) ===> A ===> (=)) 
      (monoid_ow (Collect (Domainp A))) monoid"
proof-
  let ?P = "((A ===> A ===> A) ===> A ===> (=))"
  let ?monoid_ow = "monoid_ow (Collect (Domainp A))"
  have "?P ?monoid_ow (λf z. z ∈ UNIV ∧ monoid f z)"
    unfolding 
      monoid_def monoid_ow_def 
      monoid_axioms_def monoid_ow_axioms_def 
      neutral_ow_def
    apply transfer_prover_start
    apply transfer_step+
    unfolding Ball_def by blast
  thus ?thesis by simp
qed

lemma monoid_add_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "((A ===> A ===> A) ===> A ===> (=)) 
      (monoid_add_ow (Collect (Domainp A))) class.monoid_add"
proof-
  let ?P = "((A ===> A ===> A) ===> A ===> (=))"
  let ?monoid_add_ow = "monoid_add_ow (Collect (Domainp A))"
  have "?P ?monoid_add_ow (λf z. z ∈ UNIV ∧ class.monoid_add f z)"
    unfolding 
      class.monoid_add_def monoid_add_ow_def 
      class.monoid_add_axioms_def monoid_add_ow_axioms_def
      zero_ow_def neutral_ow_def
    apply transfer_prover_start
    apply transfer_step+
    unfolding Ball_def by blast
  thus ?thesis by simp
qed


lemma monoid_mult_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "(A ===> (A ===> A ===> A) ===> (=)) 
      (monoid_mult_ow (Collect (Domainp A))) class.monoid_mult"
proof-
  let ?P = "(A ===> (A ===> A ===> A) ===> (=))"
  let ?monoid_mult_ow = "monoid_mult_ow (Collect (Domainp A))"
  have "?P ?monoid_mult_ow (λz f. z ∈ UNIV ∧ class.monoid_mult z f)"
    unfolding 
      class.monoid_mult_def monoid_mult_ow_def 
      class.monoid_mult_axioms_def monoid_mult_ow_axioms_def
      one_ow_def neutral_ow_def
    apply transfer_prover_start
    apply transfer_step+
    unfolding Ball_def by blast
  thus ?thesis by simp
qed

lemma power_with_transfer[transfer_rule]:  
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "(A ===> (A ===> A ===> A) ===> A ===> (=) ===> A) power_with power_with"
proof(intro rel_funI, elim subst)
  fix i i' m m' a a' n
  assume ii': "A i i'" and mm': "(A ===> A ===> A) m m'" and aa': "A a a'"
  show "A (power_with i m a n) (power_with i' m' a' n)"
    apply(induction n)
    subgoal by (simp add: ii')
    subgoal using mm' aa' by (auto elim: rel_funE)
    done
qed

end


subsubsection‹Relativization›

context power_ow
begin

tts_context
  tts: (?'a to U)
  sbterms: (‹(*)::[?'a::power,?'a::power] ⇒ ?'a::power› to ‹(*ow)›) 
    and (‹1::?'a::power› to ‹1ow›)
  rewriting ctr_simps
  substituting power_ow_axioms and one.not_empty
begin

tts_lemma power_Suc:
  assumes "a ∈ U"
  shows "a ^ow Suc n = a *ow a ^ow n"
    is power_class.power.power_Suc.

tts_lemma power_0:
  assumes "a ∈ U"
  shows "a ^ow 0 = 1ow"
  is power_class.power.power_0.
    
tts_lemma power_eq_if:
  assumes "p ∈ U"
  shows "p ^ow m = (if m = 0 then 1ow else p *ow p ^ow (m - 1))"
    is power_class.power_eq_if.
    
tts_lemma simps:
  assumes "a ∈ U"
  shows "a ^ow 0 = 1ow" 
    is power_class.power.simps(1)
    and "a ^ow Suc n = a *ow a ^ow n" 
    is power_class.power.simps(2).

end

end

context monoid_mult_ow
begin

tts_context
  tts: (?'a to U)
  rewriting ctr_simps
  substituting monoid_mult_ow_axioms and one.not_empty
  applying [OF one_closed mult.f_closed']
begin

tts_lemma power_commuting_commutes:
  assumes "x ∈ U" and "y ∈ U" and "x *ow y = y *ow x"
  shows "x ^ow n *ow y = y *ow x ^ow n"
    is monoid_mult_class.power_commuting_commutes.

tts_lemma left_right_inverse_power:
  assumes "x ∈ U" and "y ∈ U" and "x *ow y = 1ow"
  shows "x ^ow n *ow y ^ow n = 1ow"
    is monoid_mult_class.left_right_inverse_power.

tts_lemma power_numeral_even:
  assumes "z ∈ U"
  shows "z ^ow numeral (num.Bit0 w) = (let w = z ^ow numeral w in w *ow w)"
    is monoid_mult_class.power_numeral_even.

tts_lemma power_numeral_odd:
  assumes "z ∈ U"
  shows "z ^ow numeral (num.Bit1 w) = (let w = z ^ow numeral w in z *ow w *ow w)"
    is monoid_mult_class.power_numeral_odd.

tts_lemma power_minus_mult:
  assumes "a ∈ U" and "0 < n"
  shows "a ^ow (n - 1) *ow a = a ^ow n"
    is monoid_mult_class.power_minus_mult.

tts_lemma power_Suc0_right:
  assumes "a ∈ U" 
  shows "a ^ow Suc 0 = a"
    is monoid_mult_class.power_Suc0_right.

tts_lemma power2_eq_square:
  assumes "a ∈ U"
  shows "a ^ow 2 = a *ow a"
    is monoid_mult_class.power2_eq_square.

tts_lemma power_one_right:
  assumes "a ∈ U"
  shows "a ^ow 1 = a"
    is monoid_mult_class.power_one_right.

tts_lemma power_commutes:
  assumes "a ∈ U"
  shows "a ^ow n *ow a = a *ow a ^ow n"
    is monoid_mult_class.power_commutes.

tts_lemma power3_eq_cube:
  assumes "a ∈ U"
  shows "a ^ow 3 = a *ow a *ow a"
    is monoid_mult_class.power3_eq_cube.

tts_lemma power_even_eq:
  assumes "a ∈ U"
  shows "a ^ow (2 * n) = (a ^ow n) ^ow 2"
    is monoid_mult_class.power_even_eq.

tts_lemma power_odd_eq:
  assumes "a ∈ U"
  shows "a ^ow Suc (2 * n) = a *ow (a ^ow n) ^ow 2"
    is monoid_mult_class.power_odd_eq.

tts_lemma power_mult:
  assumes "a ∈ U"
  shows "a ^ow (m * n) = (a ^ow m) ^ow n"
    is monoid_mult_class.power_mult.

tts_lemma power_Suc2:
  assumes "a ∈ U"
  shows "a ^ow Suc n = a ^ow n *ow a"
    is monoid_mult_class.power_Suc2.

tts_lemma power_one: "1ow ^ow n = 1ow"
  is monoid_mult_class.power_one.

tts_lemma power_add:
  assumes "a ∈ U"
  shows "a ^ow (m + n) = a ^ow m *ow a ^ow n"
    is monoid_mult_class.power_add.

tts_lemma power_mult_numeral:
  assumes "a ∈ U"
  shows "(a ^ow numeral m) ^ow numeral n = a ^ow numeral (m * n)"
    is Power.power_mult_numeral.

tts_lemma power_add_numeral2:
  assumes "a ∈ U" and "b ∈ U"
  shows 
    "a ^ow numeral m *ow (a ^ow numeral n *ow b) = a ^ow numeral (m + n) *ow b"
    is Power.power_add_numeral2.

tts_lemma power_add_numeral:
  assumes "a ∈ U"
  shows "a ^ow numeral m *ow a ^ow numeral n = a ^ow numeral (m + n)"
    is Power.power_add_numeral.

end

end



subsection‹Commutative monoids›


subsubsection‹Definitions and common properties›

locale comm_monoid_ow = 
  abel_semigroup_ow U f + neutral_ow U z for U :: "'ag set" and f z +
  assumes comm_neutral: "a ∈ U ⟹ (a *ow 1ow) = a"
begin

sublocale monoid_ow U ‹(*ow)› ‹1ow›
  apply unfold_locales
  subgoal by (simp add: comm_neutral commute)
  subgoal using commute by (simp add: comm_neutral)
  done

end

lemma comm_monoid_ow: "comm_monoid = comm_monoid_ow UNIV"
  unfolding 
    comm_monoid_def comm_monoid_ow_def
    comm_monoid_axioms_def comm_monoid_ow_axioms_def
    neutral_ow_def
    abel_semigroup_ow
  by simp

locale comm_monoid_set_ow = comm_monoid_ow U f z for U :: "'ag set" and f z
begin

tts_register_sbts ‹(*ow)› | U by (rule tts_AA_A_transfer[OF f_closed])
                        
end

lemma comm_monoid_set_ow: "comm_monoid_set = comm_monoid_set_ow UNIV"
  unfolding comm_monoid_set_def comm_monoid_set_ow_def comm_monoid_ow by simp

locale comm_monoid_add_ow =
  ab_semigroup_add_ow U plus + zero_ow U zero   
  for U :: "'ag set" and plus zero +
  assumes add_0[simp]: "a ∈ U ⟹ 0ow +ow a = a"
begin

sublocale add: comm_monoid_ow U ‹(+ow)› ‹0ow›
  by unfold_locales (use add.commute in force)

sublocale monoid_add_ow U ‹(+ow)› ‹0ow› by unfold_locales simp+ 

sublocale sum: comm_monoid_set_ow U ‹(+ow)› ‹0ow› ..

notation sum.F (‹«sum»›)

abbreviation Sum (‹∑ow/ _› [1000] 1000)
  where "∑ow A ≡ («sum» (λx. x) A)"

notation Sum (‹∑ow/ _› [1000] 1000)

end

lemma comm_monoid_add_ow: "class.comm_monoid_add = comm_monoid_add_ow UNIV"
  unfolding 
    class.comm_monoid_add_def comm_monoid_add_ow_def
    class.comm_monoid_add_axioms_def comm_monoid_add_ow_axioms_def
    zero_ow_def neutral_ow_def
    ab_semigroup_add_ow
  by simp

locale dvd_ow = times_ow U times 
  for U :: "'ag set" and times

ud ‹dvd.dvd›
ud dvd' ‹dvd_class.dvd›

ctr relativization
  synthesis ctr_simps
  assumes [transfer_domain_rule, transfer_rule]: "Domainp A = (λx. x ∈ U)"
    and [transfer_rule]: "bi_unique A" "right_total A"
  trp (?'a A)
  in dvd_ow': dvd.with_def 
    (‹(on _ with _: _ «dvd» _)› [1000, 1000, 1000, 1000] 50)

ctr parametricity
  in dvd_ow'': dvd_ow'_def 

context dvd_ow
begin

abbreviation dvd (infixr ‹«dvd»› 50) where "a «dvd» b ≡ dvd_ow' U (*ow) a b"
notation dvd (infixr ‹«dvd»› 50)

end

locale comm_monoid_mult_ow =
  ab_semigroup_mult_ow U times + one_ow U one 
  for U :: "'ag set" and times one +
  assumes mult_1[simp]: "a ∈ U ⟹ 1ow *ow a = a"
begin

sublocale dvd_ow ..

sublocale mult: comm_monoid_ow U ‹(*ow)› ‹1ow›
  by unfold_locales (use mult.commute in force)

sublocale monoid_mult_ow U ‹1ow› ‹(*ow)› by unfold_locales simp+ 

sublocale prod: comm_monoid_set_ow U ‹(*ow)› ‹1ow› ..

notation prod.F (‹«prod»›)

abbreviation Prod (‹∏ow _› [1000] 1000)
  where "∏ow A ≡ («prod» (λx. x) A)"

notation Prod (‹∏ow _› [1000] 1000)

end

lemma comm_monoid_mult_ow: "class.comm_monoid_mult = comm_monoid_mult_ow UNIV"
  unfolding 
    class.comm_monoid_mult_def comm_monoid_mult_ow_def
    class.comm_monoid_mult_axioms_def comm_monoid_mult_ow_axioms_def  
    one_ow_def neutral_ow_def
    ab_semigroup_mult_ow
  by simp


subsubsection‹Transfer rules›

context
  includes lifting_syntax
begin

lemma bij_betw_transfer[transfer_rule]:
  assumes [transfer_rule]:
    "bi_unique A" "right_total A" "bi_unique B" "right_total B" 
  shows 
    "((A ===> B) ===> rel_set A ===> rel_set B ===> (=)) bij_betw bij_betw"
  unfolding bij_betw_def inj_on_def
  apply transfer_prover_start
  apply transfer_step+
  by simp

lemma comm_monoid_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A"
  shows 
    "((A ===> A ===> A) ===> A ===> (=)) 
      (comm_monoid_ow (Collect (Domainp A))) comm_monoid"
proof -
  let ?P = "((A ===> A ===> A) ===> A ===> (=))"
  let ?comm_monoid_ow = "comm_monoid_ow (Collect (Domainp A))"
  have "?P ?comm_monoid_ow 
    (λf z. z ∈ UNIV ∧ comm_monoid f z)"
    unfolding 
      comm_monoid_ow_def comm_monoid_def  
      comm_monoid_ow_axioms_def comm_monoid_axioms_def 
      neutral_ow_def
    apply transfer_prover_start
    apply transfer_step+
    by auto
  thus ?thesis by simp
qed

lemma comm_monoid_set_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "((A ===> A ===> A) ===> A ===> (=)) 
      (comm_monoid_set_ow (Collect (Domainp A))) comm_monoid_set"
  unfolding comm_monoid_set_ow_def comm_monoid_set_def
  apply transfer_prover_start
  apply transfer_step+
  by simp

lemma comm_monoid_add_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "((A ===> A ===> A) ===> A ===> (=)) 
      (comm_monoid_add_ow (Collect (Domainp A))) class.comm_monoid_add"
proof -
  let ?P = "((A ===> A ===> A) ===> A ===> (=))"
  let ?comm_monoid_add_ow = "comm_monoid_add_ow (Collect (Domainp A))"
  have "?P ?comm_monoid_add_ow (λf z. z ∈ UNIV ∧ class.comm_monoid_add f z)"
    unfolding 
      comm_monoid_add_ow_def class.comm_monoid_add_def 
      zero_ow_def neutral_ow_def 
      comm_monoid_add_ow_axioms_def class.comm_monoid_add_axioms_def
    apply transfer_prover_start
    apply transfer_step+
    by auto
  thus ?thesis by simp
qed

lemma comm_monoid_mult_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "((A ===> A ===> A) ===> A ===> (=)) 
      (comm_monoid_mult_ow (Collect (Domainp A))) class.comm_monoid_mult"
proof -
  let ?P = "((A ===> A ===> A) ===> A ===> (=))"
  let ?comm_monoid_mult_ow = "comm_monoid_mult_ow (Collect (Domainp A))"
  have "?P ?comm_monoid_mult_ow (λf z. z ∈ UNIV ∧ class.comm_monoid_mult f z)"
    unfolding 
      comm_monoid_mult_ow_def class.comm_monoid_mult_def 
      one_ow_def neutral_ow_def 
      comm_monoid_mult_ow_axioms_def class.comm_monoid_mult_axioms_def
    apply transfer_prover_start
    apply transfer_step+
    by auto
  thus ?thesis by simp
qed

lemma dvd_with_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "((A ===> A ===> A) ===> A ===> A ===> (=)) 
      (dvd_ow' (Collect (Domainp A))) dvd.with"
  unfolding dvd_ow'_def dvd.with_def by transfer_prover

end


subsubsection‹Relativization›

context dvd_ow
begin

tts_context
  tts: (?'a to U)
  sbterms: (‹(*)::[?'a::times, ?'a::times] ⇒ ?'a::times› to ‹(*ow)›)
  rewriting ctr_simps
  substituting dvd_ow_axioms 
  eliminating through simp
begin

tts_lemma dvdI:
  assumes "b ∈ U" and "k ∈ U" and "a = b *ow k"
  shows "b «dvd» a"
    is dvd_class.dvdI.

tts_lemma dvdE:
  assumes "b ∈ U" 
    and "a ∈ U" 
    and "b «dvd» a" 
    and "⋀k. ⟦k ∈ U; a = b *ow k⟧ ⟹ P"
  shows P
    is dvd_class.dvdE.

end

end

context comm_monoid_mult_ow
begin

tts_context
  tts: (?'a to U)
  rewriting ctr_simps
  substituting comm_monoid_mult_ow_axioms and one.not_empty
  applying [OF mult.f_closed' one_closed]
begin

tts_lemma strict_subset_divisors_dvd:
  assumes "a ∈ U" and "b ∈ U"
  shows 
    "({x ∈ U. x «dvd» a} ⊂ {x ∈ U. x «dvd» b}) = (a «dvd» b ∧ ¬ b «dvd» a)"
    is comm_monoid_mult_class.strict_subset_divisors_dvd.

tts_lemma subset_divisors_dvd:
  assumes "a ∈ U" and "b ∈ U"
  shows "({x ∈ U. x «dvd» a} ⊆ {x ∈ U. x «dvd» b}) = (a «dvd» b)"
    is comm_monoid_mult_class.subset_divisors_dvd.

tts_lemma power_mult_distrib:
  assumes "a ∈ U" and "b ∈ U"
  shows "(a *ow b) ^ow n = a ^ow n *ow b ^ow n"
    is Power.comm_monoid_mult_class.power_mult_distrib.

tts_lemma dvd_triv_right:
  assumes "a ∈ U" and "b ∈ U"
  shows "a «dvd» b *ow a"
    is comm_monoid_mult_class.dvd_triv_right.

tts_lemma dvd_mult_right:
  assumes "a ∈ U" and "b ∈ U" and "c ∈ U" and "a *ow b «dvd» c"
  shows "b «dvd» c"
    is comm_monoid_mult_class.dvd_mult_right.

tts_lemma mult_dvd_mono:
  assumes "a ∈ U" 
    and "b ∈ U" 
    and "c ∈ U" 
    and "d ∈ U"
    and "a «dvd» b"
    and "c «dvd» d"
  shows "a *ow c «dvd» b *ow d"
    is comm_monoid_mult_class.mult_dvd_mono.

tts_lemma dvd_triv_left:
  assumes "a ∈ U" and "b ∈ U"
  shows "a «dvd» a *ow b"
    is comm_monoid_mult_class.dvd_triv_left.

tts_lemma dvd_mult_left:
  assumes "a ∈ U" and "b ∈ U" and "c ∈ U" and "a *ow b «dvd» c"
  shows "a «dvd» c"
    is comm_monoid_mult_class.dvd_mult_left.

tts_lemma dvd_trans:
  assumes "a ∈ U" and "b ∈ U" and "c ∈ U" and "a «dvd» b" and "b «dvd» c"
  shows "a «dvd» c"
    is comm_monoid_mult_class.dvd_trans.

tts_lemma dvd_mult2:
  assumes "a ∈ U" and "b ∈ U" and "c ∈ U" and "a «dvd» b"
  shows "a «dvd» b *ow c"
    is comm_monoid_mult_class.dvd_mult2.

tts_lemma dvd_refl:
  assumes "a ∈ U"
  shows "a «dvd» a"
    is comm_monoid_mult_class.dvd_refl.

tts_lemma dvd_mult:
  assumes "a ∈ U" and "c ∈ U" and "b ∈ U" and "a «dvd» c"
  shows "a «dvd» b *ow c"
    is comm_monoid_mult_class.dvd_mult.

tts_lemma one_dvd:
  assumes "a ∈ U"
  shows "1ow «dvd» a"
    is comm_monoid_mult_class.one_dvd.

end

end



subsection‹Cancellative commutative monoids›


subsubsection‹Definitions and common properties›

locale cancel_comm_monoid_add_ow =
  cancel_ab_semigroup_add_ow U plus minus +
  comm_monoid_add_ow U plus zero
  for U :: "'ag set" and plus minus zero

lemma cancel_comm_monoid_add_ow: 
  "class.cancel_comm_monoid_add = cancel_comm_monoid_add_ow UNIV"
  unfolding 
    class.cancel_comm_monoid_add_def cancel_comm_monoid_add_ow_def
    cancel_ab_semigroup_add_ow comm_monoid_add_ow
  by simp


subsubsection‹Transfer rules›

context
  includes lifting_syntax
begin

lemma cancel_comm_monoid_add_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "((A ===> A ===> A) ===> (A ===> A ===> A) ===> A ===> (=)) 
      (cancel_comm_monoid_add_ow (Collect (Domainp A))) 
      class.cancel_comm_monoid_add"
  unfolding cancel_comm_monoid_add_ow_def class.cancel_comm_monoid_add_def
  by transfer_prover

end


subsubsection‹Relativization›

context cancel_comm_monoid_add_ow
begin

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

tts_lemma add_cancel_right_right:
  assumes "a ∈ U" and "b ∈ U"
  shows "(a = a +ow b) = (b = 0ow)"
    is cancel_comm_monoid_add_class.add_cancel_right_right.
    
tts_lemma add_cancel_right_left:
  assumes "a ∈ U" and "b ∈ U"
  shows "(a = b +ow a) = (b = 0ow)"
    is cancel_comm_monoid_add_class.add_cancel_right_left.

tts_lemma add_cancel_left_right:
  assumes "a ∈ U" and "b ∈ U"
  shows "(a +ow b = a) = (b = 0ow)"
    is cancel_comm_monoid_add_class.add_cancel_left_right.

tts_lemma add_cancel_left_left:
  assumes "b ∈ U" and "a ∈ U"
  shows "(b +ow a = a) = (b = 0ow)"
    is cancel_comm_monoid_add_class.add_cancel_left_left.

tts_lemma add_implies_diff:
  assumes "c ∈ U" and "b ∈ U" and "a ∈ U" and "c +ow b = a"
  shows "c = a -ow b"
    is cancel_comm_monoid_add_class.add_implies_diff.

tts_lemma diff_cancel:
  assumes "a ∈ U"
  shows "a -ow a = 0ow"
    is cancel_comm_monoid_add_class.diff_cancel.

tts_lemma diff_zero:
  assumes "a ∈ U"
  shows "a -ow 0ow = a"
    is cancel_comm_monoid_add_class.diff_zero.

end

end

text‹\newpage›

end