Theory CZH_EX_Algebra

(* Copyright 2021 (C) Mihails Milehins *)

section‹Example III: abstract algebra›
theory CZH_EX_Algebra
  imports CZH_EX_TS
begin



subsection‹Background›


text‹
The section presents several examples of algebraic structures formalized
in ‹ZFC in HOL›. The definitions were adopted (with amendments) from the
main library of Isabelle/HOL.
›

named_theorems sgrp_struct_field_simps

lemmas [sgrp_struct_field_simps] = 𝒜_def



subsection‹Semigroup›


subsubsection‹Foundations›

definition mbinop where [sgrp_struct_field_simps]: "mbinop = 1⇩ℕ"

locale 𝒵_sgrp_basis = 𝒵_vfsequence α 𝔖 + op: binop ‹𝔖⦇𝒜⦈› ‹𝔖⦇mbinop⦈› 
  for α 𝔖 +
  assumes 𝒵_sgrp_length: "vcard 𝔖 = 2⇩ℕ"

abbreviation sgrp_app :: "V ⇒ V ⇒ V ⇒ V" (infixl ‹⊙⇩∘ı› 70)
  where "sgrp_app 𝔖 a b ≡ 𝔖⦇mbinop⦈⦇a, b⦈⇩∙"
notation sgrp_app (infixl ‹⊙⇩∘› 70)


text‹Rules.›

lemma 𝒵_sgrp_basisI[intro]:
  assumes "𝒵_vfsequence α 𝔖"
    and "vcard 𝔖 = 2⇩ℕ"
    and "binop (𝔖⦇𝒜⦈) (𝔖⦇mbinop⦈)"
  shows "𝒵_sgrp_basis α 𝔖"
  using assms unfolding 𝒵_sgrp_basis_def 𝒵_sgrp_basis_axioms_def by simp

lemma 𝒵_sgrp_basisD[dest]:
  assumes "𝒵_sgrp_basis α 𝔖"
  shows "𝒵_vfsequence α 𝔖"
    and "vcard 𝔖 = 2⇩ℕ"
    and "binop (𝔖⦇𝒜⦈) (𝔖⦇mbinop⦈)"
  using assms unfolding 𝒵_sgrp_basis_def 𝒵_sgrp_basis_axioms_def by auto

lemma 𝒵_sgrp_basisE[elim]:
  assumes "𝒵_sgrp_basis α 𝔖"
  shows "𝒵_vfsequence α 𝔖"
    and "vcard 𝔖 = 2⇩ℕ"
    and "binop (𝔖⦇𝒜⦈) (𝔖⦇mbinop⦈)"
  using assms unfolding 𝒵_sgrp_basis_def 𝒵_sgrp_basis_axioms_def by auto


subsubsection‹Simple semigroup›

locale 𝒵_sgrp = 𝒵_sgrp_basis α 𝔖 for α 𝔖 +
  assumes 𝒵_sgrp_assoc: 
    "⟦ a ∈⇩∘ 𝔖⦇𝒜⦈; b ∈⇩∘ 𝔖⦇𝒜⦈; c ∈⇩∘ 𝔖⦇𝒜⦈ ⟧ ⟹ 
      (a ⊙⇩∘⇘𝔖⇙ b) ⊙⇩∘⇘𝔖⇙ c = a ⊙⇩∘⇘𝔖⇙ (b ⊙⇩∘⇘𝔖⇙ c)"


text‹Rules.›

lemma 𝒵_sgrpI[intro]:
  assumes "𝒵_sgrp_basis α 𝔖" 
    and "⋀a b c. ⟦ a ∈⇩∘ 𝔖⦇𝒜⦈; b ∈⇩∘ 𝔖⦇𝒜⦈; c ∈⇩∘ 𝔖⦇𝒜⦈ ⟧ ⟹ 
      (a ⊙⇩∘⇘𝔖⇙ b) ⊙⇩∘⇘𝔖⇙ c = a ⊙⇩∘⇘𝔖⇙ (b ⊙⇩∘⇘𝔖⇙ c)"
  shows "𝒵_sgrp α 𝔖"
  using assms unfolding 𝒵_sgrp_def 𝒵_sgrp_axioms_def by simp

lemma 𝒵_sgrpD[dest]:
  assumes "𝒵_sgrp α 𝔖"
  shows "𝒵_sgrp_basis α 𝔖" 
    and "⋀a b c. ⟦ a ∈⇩∘ 𝔖⦇𝒜⦈; b ∈⇩∘ 𝔖⦇𝒜⦈; c ∈⇩∘ 𝔖⦇𝒜⦈ ⟧ ⟹ 
      (a ⊙⇩∘⇘𝔖⇙ b) ⊙⇩∘⇘𝔖⇙ c = a ⊙⇩∘⇘𝔖⇙ (b ⊙⇩∘⇘𝔖⇙ c)"
  using assms unfolding 𝒵_sgrp_def 𝒵_sgrp_axioms_def by simp_all

lemma 𝒵_sgrpE[elim]:
  assumes "𝒵_sgrp α 𝔖"
  obtains "𝒵_sgrp_basis α 𝔖" 
    and "⋀a b c. ⟦ a ∈⇩∘ 𝔖⦇𝒜⦈; b ∈⇩∘ 𝔖⦇𝒜⦈; c ∈⇩∘ 𝔖⦇𝒜⦈ ⟧ ⟹ 
      (a ⊙⇩∘⇘𝔖⇙ b) ⊙⇩∘⇘𝔖⇙ c = a ⊙⇩∘⇘𝔖⇙ (b ⊙⇩∘⇘𝔖⇙ c)"
  using assms by auto



subsection‹Commutative semigroup›

locale 𝒵_csgrp = 𝒵_sgrp α 𝔖 for α 𝔖 +
  assumes 𝒵_csgrp_commutative: 
    "⟦ a ∈⇩∘ 𝔖⦇𝒜⦈; b ∈⇩∘ 𝔖⦇𝒜⦈ ⟧ ⟹ a ⊙⇩∘⇘𝔖⇙ b = b ⊙⇩∘⇘𝔖⇙ a"


text‹Rules.›

lemma 𝒵_csgrpI[intro]:
  assumes "𝒵_sgrp α 𝔖"
    and "⋀a b. ⟦ a ∈⇩∘ 𝔖⦇𝒜⦈; b ∈⇩∘ 𝔖⦇𝒜⦈ ⟧ ⟹ a ⊙⇩∘⇘𝔖⇙ b = b ⊙⇩∘⇘𝔖⇙ a"
  shows "𝒵_csgrp α 𝔖"
  using assms unfolding 𝒵_csgrp_def 𝒵_csgrp_axioms_def by simp

lemma 𝒵_csgrpD[dest]:
  assumes "𝒵_csgrp α 𝔖"
  shows "𝒵_sgrp α 𝔖"
    and "⋀a b. ⟦ a ∈⇩∘ 𝔖⦇𝒜⦈; b ∈⇩∘ 𝔖⦇𝒜⦈ ⟧ ⟹ a ⊙⇩∘⇘𝔖⇙ b = b ⊙⇩∘⇘𝔖⇙ a"
  using assms unfolding 𝒵_csgrp_def 𝒵_csgrp_axioms_def by simp_all

lemma 𝒵_csgrpE[elim]:
  assumes "𝒵_csgrp α 𝔖"
  obtains "𝒵_sgrp α 𝔖"
    and "⋀a b. ⟦ a ∈⇩∘ 𝔖⦇𝒜⦈; b ∈⇩∘ 𝔖⦇𝒜⦈ ⟧ ⟹ a ⊙⇩∘⇘𝔖⇙ b = b ⊙⇩∘⇘𝔖⇙ a"
  using assms by auto



subsection‹Semiring›


subsubsection‹Foundations›

definition vplus :: V where [sgrp_struct_field_simps]: "vplus = 1⇩ℕ"
definition vmult :: V where [sgrp_struct_field_simps]: "vmult = 2⇩ℕ"

abbreviation vplus_app :: "V ⇒ V ⇒ V ⇒ V" (infixl ‹+⇩∘ı› 65)
  where "a +⇩∘⇘𝔖⇙ b ≡ 𝔖⦇vplus⦈⦇a,b⦈⇩∙"
notation vplus_app (infixl ‹+⇩∘ı› 65)

abbreviation vmult_app :: "V ⇒ V ⇒ V ⇒ V" (infixl ‹*⇩∘ı› 70)
  where "a *⇩∘⇘𝔖⇙ b ≡ 𝔖⦇vmult⦈⦇a,b⦈⇩∙"
notation vmult_app (infixl ‹*⇩∘ı› 70)


subsubsection‹Simple semiring›

locale 𝒵_srng = 𝒵_vfsequence α 𝔖 for α 𝔖 +
  assumes 𝒵_srng_length: "vcard 𝔖 = 3⇩ℕ"
    and 𝒵_srng_𝒵_csgrp_vplus: "𝒵_csgrp α [𝔖⦇𝒜⦈, 𝔖⦇vplus⦈]⇩∘"
    and 𝒵_srng_𝒵_sgrp_vmult: "𝒵_sgrp α [𝔖⦇𝒜⦈, 𝔖⦇vmult⦈]⇩∘"
    and 𝒵_srng_distrib_right: 
      "⟦ a ∈⇩∘ 𝔖⦇𝒜⦈; b ∈⇩∘ 𝔖⦇𝒜⦈; c ∈⇩∘ 𝔖⦇𝒜⦈ ⟧ ⟹
        (a +⇩∘⇘𝔖⇙ b) *⇩∘⇘𝔖⇙ c = (a *⇩∘⇘𝔖⇙ c) +⇩∘⇘𝔖⇙ (b *⇩∘⇘𝔖⇙ c)"
    and 𝒵_srng_distrib_left: 
      "⟦ a ∈⇩∘ 𝔖⦇𝒜⦈; b ∈⇩∘ 𝔖⦇𝒜⦈; c ∈⇩∘ 𝔖⦇𝒜⦈ ⟧ ⟹
        a *⇩∘⇘𝔖⇙ (b +⇩∘⇘𝔖⇙ c) = (a *⇩∘⇘𝔖⇙ b) +⇩∘⇘𝔖⇙ (a *⇩∘⇘𝔖⇙ c)"
begin

sublocale vplus: 𝒵_csgrp α ‹[𝔖⦇𝒜⦈, 𝔖⦇vplus⦈]⇩∘›
  rewrites "[𝔖⦇𝒜⦈, 𝔖⦇vplus⦈]⇩∘⦇𝒜⦈ = 𝔖⦇𝒜⦈"
    and "[𝔖⦇𝒜⦈, 𝔖⦇vplus⦈]⇩∘⦇mbinop⦈ = 𝔖⦇vplus⦈"
    and "sgrp_app [𝔖⦇𝒜⦈, 𝔖⦇vplus⦈]⇩∘ = vplus_app 𝔖"
proof(rule 𝒵_srng_𝒵_csgrp_vplus)
  show "[𝔖⦇𝒜⦈, 𝔖⦇vplus⦈]⇩∘⦇𝒜⦈ = 𝔖⦇𝒜⦈"
    and [simp]: "[𝔖⦇𝒜⦈, 𝔖⦇vplus⦈]⇩∘⦇mbinop⦈ = 𝔖⦇vplus⦈"
    by (auto simp: 𝒜_def mbinop_def nat_omega_simps)
  show "(⊙⇩∘⇘[𝔖⦇𝒜⦈, 𝔖⦇vplus⦈]⇩∘⇙) = (+⇩∘⇘𝔖⇙)" by simp
qed

sublocale vmult: 𝒵_sgrp α ‹[𝔖⦇𝒜⦈, 𝔖⦇vmult⦈]⇩∘›
  rewrites "[𝔖⦇𝒜⦈, 𝔖⦇vmult⦈]⇩∘⦇𝒜⦈ = 𝔖⦇𝒜⦈"
    and "[𝔖⦇𝒜⦈, 𝔖⦇vmult⦈]⇩∘⦇mbinop⦈ = 𝔖⦇vmult⦈"
    and "sgrp_app [𝔖⦇𝒜⦈, 𝔖⦇vmult⦈]⇩∘ = vmult_app 𝔖"
proof(rule 𝒵_srng_𝒵_sgrp_vmult)
  show "[𝔖⦇𝒜⦈, 𝔖⦇vmult⦈]⇩∘⦇𝒜⦈ = 𝔖⦇𝒜⦈"
    and [simp]: "[𝔖⦇𝒜⦈, 𝔖⦇vmult⦈]⇩∘⦇mbinop⦈ = 𝔖⦇vmult⦈"
    by (auto simp: 𝒜_def mbinop_def nat_omega_simps)
  show "(⊙⇩∘⇘[𝔖⦇𝒜⦈, 𝔖⦇vmult⦈]⇩∘⇙) = (*⇩∘⇘𝔖⇙)" by simp
qed

end


text‹Rules.›

lemma 𝒵_srngI[intro]:
  assumes "𝒵_vfsequence α 𝔖"
    and "vcard 𝔖 = 3⇩ℕ"
    and "𝒵_csgrp α [𝔖⦇𝒜⦈, 𝔖⦇vplus⦈]⇩∘"
    and "𝒵_sgrp α [𝔖⦇𝒜⦈, 𝔖⦇vmult⦈]⇩∘"
    and "⋀a b c. ⟦ a ∈⇩∘ 𝔖⦇𝒜⦈; b ∈⇩∘ 𝔖⦇𝒜⦈; c ∈⇩∘ 𝔖⦇𝒜⦈ ⟧ ⟹
      (a +⇩∘⇘𝔖⇙ b) *⇩∘⇘𝔖⇙ c = (a *⇩∘⇘𝔖⇙ c) +⇩∘⇘𝔖⇙ (b *⇩∘⇘𝔖⇙ c)"
    and "⋀a b c. ⟦ a ∈⇩∘ 𝔖⦇𝒜⦈; b ∈⇩∘ 𝔖⦇𝒜⦈; c ∈⇩∘ 𝔖⦇𝒜⦈ ⟧ ⟹
      a *⇩∘⇘𝔖⇙ (b +⇩∘⇘𝔖⇙ c) = (a *⇩∘⇘𝔖⇙ b) +⇩∘⇘𝔖⇙ (a *⇩∘⇘𝔖⇙ c)"
  shows "𝒵_srng α 𝔖"
  using assms unfolding 𝒵_srng_def 𝒵_srng_axioms_def by simp

lemma 𝒵_srngD[dest]:
  assumes "𝒵_srng α 𝔖"
  shows "𝒵_vfsequence α 𝔖"
    and "vcard 𝔖 = 3⇩ℕ"
    and "𝒵_csgrp α [𝔖⦇𝒜⦈, 𝔖⦇vplus⦈]⇩∘"
    and "𝒵_sgrp α [𝔖⦇𝒜⦈, 𝔖⦇vmult⦈]⇩∘"
    and "⋀a b c. ⟦ a ∈⇩∘ 𝔖⦇𝒜⦈; b ∈⇩∘ 𝔖⦇𝒜⦈; c ∈⇩∘ 𝔖⦇𝒜⦈ ⟧ ⟹
      (a +⇩∘⇘𝔖⇙ b) *⇩∘⇘𝔖⇙ c = (a *⇩∘⇘𝔖⇙ c) +⇩∘⇘𝔖⇙ (b *⇩∘⇘𝔖⇙ c)"
    and "⋀a b c. ⟦ a ∈⇩∘ 𝔖⦇𝒜⦈; b ∈⇩∘ 𝔖⦇𝒜⦈; c ∈⇩∘ 𝔖⦇𝒜⦈ ⟧ ⟹
      a *⇩∘⇘𝔖⇙ (b +⇩∘⇘𝔖⇙ c) = (a *⇩∘⇘𝔖⇙ b) +⇩∘⇘𝔖⇙ (a *⇩∘⇘𝔖⇙ c)"
  using assms unfolding 𝒵_srng_def 𝒵_srng_axioms_def by simp_all

lemma 𝒵_srngE[elim]:
  assumes "𝒵_srng α 𝔖"
  obtains "𝒵_vfsequence α 𝔖"
    and "vcard 𝔖 = 3⇩ℕ"
    and "𝒵_csgrp α [𝔖⦇𝒜⦈, 𝔖⦇vplus⦈]⇩∘"
    and "𝒵_sgrp α [𝔖⦇𝒜⦈, 𝔖⦇vmult⦈]⇩∘"
    and "⋀a b c. ⟦ a ∈⇩∘ 𝔖⦇𝒜⦈; b ∈⇩∘ 𝔖⦇𝒜⦈; c ∈⇩∘ 𝔖⦇𝒜⦈ ⟧ ⟹
      (a +⇩∘⇘𝔖⇙ b) *⇩∘⇘𝔖⇙ c = (a *⇩∘⇘𝔖⇙ c) +⇩∘⇘𝔖⇙ (b *⇩∘⇘𝔖⇙ c)"
    and "⋀a b c. ⟦ a ∈⇩∘ 𝔖⦇𝒜⦈; b ∈⇩∘ 𝔖⦇𝒜⦈; c ∈⇩∘ 𝔖⦇𝒜⦈ ⟧ ⟹
      a *⇩∘⇘𝔖⇙ (b +⇩∘⇘𝔖⇙ c) = (a *⇩∘⇘𝔖⇙ b) +⇩∘⇘𝔖⇙ (a *⇩∘⇘𝔖⇙ c)"
  using assms unfolding 𝒵_srng_def 𝒵_srng_axioms_def by auto



subsection‹Integer numbers form a semiring›

definition vint_struct :: V (‹𝔖⇩ℤ›)
  where "vint_struct = [ℤ⇩∘, vint_plus, vint_mult]⇩∘"

named_theorems vint_struct_simps

lemma vint_struct_𝒜[vint_struct_simps]: "𝔖⇩ℤ⦇𝒜⦈ = ℤ⇩∘"
  unfolding vint_struct_def by (auto simp: sgrp_struct_field_simps)

lemma vint_struct_vplus[vint_struct_simps]: "𝔖⇩ℤ⦇vplus⦈ = vint_plus"
  unfolding vint_struct_def 
  by (simp add: sgrp_struct_field_simps nat_omega_simps)

lemma vint_struct_vmult[vint_struct_simps]: "𝔖⇩ℤ⦇vmult⦈ = vint_mult"
  unfolding vint_struct_def 
  by (simp add: sgrp_struct_field_simps nat_omega_simps)

context 𝒵
begin

lemma 𝒵_srng_vint: "𝒵_srng α 𝔖⇩ℤ"
proof(intro 𝒵_srngI, unfold vint_struct_simps)

  interpret 𝔖: vfsequence ‹𝔖⇩ℤ› unfolding vint_struct_def by simp

  show vint_struct: "𝒵_vfsequence α 𝔖⇩ℤ"
  proof(intro 𝒵_vfsequenceI)
    show "vfsequence 𝔖⇩ℤ" unfolding vint_struct_def by simp
    show "ℛ⇩∘ 𝔖⇩ℤ ⊆⇩∘ Vset α"
    proof(intro vsubsetI)
      fix x assume "x ∈⇩∘ ℛ⇩∘ 𝔖⇩ℤ"
      then consider ‹x = ℤ⇩∘› | ‹x = vint_plus› | ‹x = vint_mult› 
        unfolding vint_struct_def by fastforce
      then show "x ∈⇩∘ Vset α"
      proof cases
        case 1 with 𝒵_Vset_ω2_vsubset_Vset vint_in_Vset_ω2 show ?thesis by auto
      next
        case 2
        have "𝒟⇩∘ vint_plus ∈⇩∘ Vset α"
          unfolding vint_plus.nop_vdomain
        proof(rule Limit_vcpower_in_VsetI)
          from Axiom_of_Infinity show "2⇩ℕ ∈⇩∘ Vset α" by auto
          from 𝒵_Vset_ω2_vsubset_Vset show "ℤ⇩∘ ∈⇩∘ Vset α" 
            by (auto intro: vint_in_Vset_ω2)
        qed auto
        moreover from 𝒵_Vset_ω2_vsubset_Vset have "ℛ⇩∘ vint_plus ∈⇩∘ Vset α"
          unfolding vint_plus.nop_onto_vrange by (auto intro: vint_in_Vset_ω2)
        ultimately show "x ∈⇩∘ Vset α"
          unfolding 2
          by (simp add: rel_VLambda.vbrelation_Limit_in_VsetI vint_plus_def)
      next
        case 3
        have "𝒟⇩∘ vint_mult ∈⇩∘ Vset α"
          unfolding vint_mult.nop_vdomain
        proof(rule Limit_vcpower_in_VsetI)
          from Axiom_of_Infinity show "2⇩ℕ ∈⇩∘ Vset α" by auto
          from 𝒵_Vset_ω2_vsubset_Vset show "ℤ⇩∘ ∈⇩∘ Vset α" 
            by (auto intro: vint_in_Vset_ω2)
        qed auto
        moreover from 𝒵_Vset_ω2_vsubset_Vset Axiom_of_Infinity have 
          "ℛ⇩∘ vint_mult ∈⇩∘ Vset α"
          unfolding vint_mult.nop_onto_vrange by (auto intro: vint_in_Vset_ω2)
        ultimately show "x ∈⇩∘ Vset α"
          unfolding 3
          by (simp add: rel_VLambda.vbrelation_Limit_in_VsetI vint_mult_def)
      qed
    qed
  qed (simp add: 𝒵_axioms)

  interpret vint_struct: 𝒵_vfsequence α ‹𝔖⇩ℤ› by (rule vint_struct)
  
  show "vcard 𝔖⇩ℤ = 3⇩ℕ" 
    unfolding vint_struct_def by (simp add: nat_omega_simps)

  have [vint_struct_simps]:
    "[ℤ⇩∘, vint_plus]⇩∘⦇𝒜⦈ = ℤ⇩∘" "[ℤ⇩∘, vint_plus]⇩∘⦇mbinop⦈ = vint_plus"
    "[ℤ⇩∘, vint_mult]⇩∘⦇𝒜⦈ = ℤ⇩∘" "[ℤ⇩∘, vint_mult]⇩∘⦇mbinop⦈ = vint_mult"
    by (auto simp: sgrp_struct_field_simps nat_omega_simps)

  have [vint_struct_simps]:
    "sgrp_app [ℤ⇩∘, vint_plus]⇩∘ = (+⇩ℤ)"
    "sgrp_app [ℤ⇩∘, vint_mult]⇩∘ = (*⇩ℤ)"
    unfolding vint_struct_simps by simp_all

  show "𝒵_csgrp α [ℤ⇩∘, vint_plus]⇩∘"
  proof(intro 𝒵_csgrpI, unfold vint_struct_simps)
    show "𝒵_sgrp α [ℤ⇩∘, vint_plus]⇩∘"
    proof(intro 𝒵_sgrpI 𝒵_sgrp_basisI, unfold vint_struct_simps)
      show "𝒵_vfsequence α [ℤ⇩∘, vint_plus]⇩∘"
      proof(intro 𝒵_vfsequenceI)
        show "ℛ⇩∘ [ℤ⇩∘, vint_plus]⇩∘ ⊆⇩∘ Vset α"
        proof(intro vfsequence_vrange_vconsI)
          from 𝒵_Vset_ω2_vsubset_Vset show [simp]: "ℤ⇩∘ ∈⇩∘ Vset α"
            by (auto intro: vint_in_Vset_ω2)
          show "vint_plus ∈⇩∘ Vset α"
          proof(rule vbrelation.vbrelation_Limit_in_VsetI)
            from Axiom_of_Infinity show "𝒟⇩∘ vint_plus ∈⇩∘ Vset α"
              unfolding vint_plus.nop_vdomain 
              by (intro Limit_vcpower_in_VsetI) auto
            from Axiom_of_Infinity show "ℛ⇩∘ vint_plus ∈⇩∘ Vset α" 
              unfolding vint_plus.nop_onto_vrange by auto
          qed (simp_all add: vint_plus_def)
        qed simp_all
      qed (simp_all add: 𝒵_axioms)
    qed 
      (
         auto simp:
          nat_omega_simps
          vint_plus.binop_axioms
          vint_assoc_law_addition
      ) 
  qed (simp add: vint_commutative_law_addition)

  show "𝒵_sgrp α [ℤ⇩∘, vint_mult]⇩∘"
  proof
    (
      intro 𝒵_sgrpI 𝒵_sgrp_basisI; 
      (unfold vint_struct_simps | tactic‹all_tac›)
    )
    show "𝒵_vfsequence α [ℤ⇩∘, vint_mult]⇩∘"
    proof(intro 𝒵_vfsequenceI; (unfold vint_struct_simps | tactic‹all_tac›))
      from 𝒵_axioms show "𝒵 α" by simp
      show "ℛ⇩∘ [ℤ⇩∘, vint_mult]⇩∘ ⊆⇩∘ Vset α"
      proof(intro vfsequence_vrange_vconsI)
        from 𝒵_Vset_ω2_vsubset_Vset show [simp]: "ℤ⇩∘ ∈⇩∘ Vset α"
          by (auto intro: vint_in_Vset_ω2)
        show "vint_mult ∈⇩∘ Vset α"
        proof(rule vbrelation.vbrelation_Limit_in_VsetI)
          from Axiom_of_Infinity show "𝒟⇩∘ vint_mult ∈⇩∘ Vset α"
            unfolding vint_mult.nop_vdomain 
            by (intro Limit_vcpower_in_VsetI) auto
          from Axiom_of_Infinity show "ℛ⇩∘ vint_mult ∈⇩∘ Vset α" 
            unfolding vint_mult.nop_onto_vrange by auto
        qed (simp_all add: vint_mult_def)
      qed simp_all
    qed auto
  qed
    (
      auto simp: 
        nat_omega_simps
        vint_mult.binop_axioms
        vint_assoc_law_multiplication
    )

qed
  (
    auto simp: 
      vint_commutative_law_multiplication 
      vint_plus_closed 
      vint_distributive_law
  )


text‹Interpretation.›

interpretation vint: 𝒵_srng α ‹𝔖⇩ℤ›
  rewrites "𝔖⇩ℤ⦇𝒜⦈ = ℤ⇩∘"
    and "𝔖⇩ℤ⦇vplus⦈ = vint_plus"
    and "𝔖⇩ℤ⦇vmult⦈ = vint_mult"
    and "vplus_app (𝔖⇩ℤ) = vint_plus_app"
    and "vmult_app (𝔖⇩ℤ) = vint_mult_app"
  unfolding vint_struct_simps by (rule 𝒵_srng_vint) simp_all

thm vint.vmult.𝒵_sgrp_assoc
thm vint.vplus.𝒵_sgrp_assoc
thm vint.𝒵_srng_distrib_left

end

text‹\newpage›

end