Theory CZH_Sets_NOP

(* Copyright 2021 (C) Mihails Milehins *)

section‹‹n›-ary operation›
theory CZH_Sets_NOP
  imports CZH_Sets_FBRelations
begin



subsection‹Partial ‹n›-ary operation›

locale pnop = vsv f for A n f :: V +
  assumes pnop_n: "n ∈∘ ω" 
    and pnop_vdomain: "𝒟∘ f ⊆∘ A ^× n"
    and pnop_vrange: "ℛ∘ f ⊆∘ A"


text‹Rules.›

lemma pnopI[intro]:
  assumes "vsv f"
    and "n ∈∘ ω"
    and "𝒟∘ f ⊆∘ A ^× n"
    and "ℛ∘ f ⊆∘ A"
  shows "pnop A n f"
  using assms unfolding pnop_def pnop_axioms_def by blast

lemma pnopD[dest]:
  assumes "pnop A n f"
  shows "vsv f"
    and "n ∈∘ ω"
    and "𝒟∘ f ⊆∘ A ^× n"
    and "ℛ∘ f ⊆∘ A"
  using assms unfolding pnop_def pnop_axioms_def by blast+

lemma pnopE[elim]:
  assumes "pnop A n f"
  obtains "vsv f"
    and "n ∈∘ ω"
    and "𝒟∘ f ⊆∘ A ^× n"
    and "ℛ∘ f ⊆∘ A"
  using assms by force



subsection‹Total ‹n›-ary operation›

locale nop = vsv f for A n f :: V +
  assumes nop_n: "n ∈∘ ω" 
    and nop_vdomain: "𝒟∘ f = A ^× n"
    and nop_vrange: "ℛ∘ f ⊆∘ A"

sublocale nop ⊆ pnop A n f
proof(intro pnopI)
  show "vsv f" by (rule vsv_axioms)
  show "n ∈∘ ω" by (rule nop_n)
  from nop_vdomain show "𝒟∘ f ⊆∘ A ^× n" by simp
  show "ℛ∘ f ⊆∘ A" by (rule nop_vrange)
qed


text‹Rules.›

lemma nopI[intro]:
  assumes "vsv f"
    and "n ∈∘ ω"
    and "𝒟∘ f = A ^× n"
    and "ℛ∘ f ⊆∘ A"
  shows "nop A n f"
  using assms unfolding nop_def nop_axioms_def by blast

lemma nopD[dest]:
  assumes "nop A n f"
  shows "vsv f"
    and "n ∈∘ ω"
    and "𝒟∘ f = A ^× n"
    and "ℛ∘ f ⊆∘ A"
  using assms unfolding nop_def nop_axioms_def by blast+

lemma nopE[elim]:
  assumes "nop A n f"
  obtains "vsv f"
    and "n ∈∘ ω"
    and "𝒟∘ f = A ^× n"
    and "ℛ∘ f ⊆∘ A"
  using assms by force



subsection‹Injective ‹n›-ary operation›

locale nop_v11 = v11 f for A n f :: V +
  assumes nop_v11_n: "n ∈∘ ω" 
    and nop_v11_vdomain: "𝒟∘ f = A ^× n"
    and nop_v11_vrange: "ℛ∘ f ⊆∘ A"

sublocale nop_v11 ⊆ nop 
proof
  show "vsv f" by (rule vsv_axioms)
  show "n ∈∘ ω" by (rule nop_v11_n)
  show "𝒟∘ f = A ^× n" by (rule nop_v11_vdomain)
  show "ℛ∘ f ⊆∘ A" by (rule nop_v11_vrange)
qed


text‹Rules.›

lemma nop_v11I[intro]:
  assumes "v11 f"
    and "n ∈∘ ω"
    and "𝒟∘ f = A ^× n"
    and "ℛ∘ f ⊆∘ A"
  shows "nop_v11 A n f"
  using assms unfolding nop_v11_def nop_v11_axioms_def by blast

lemma nop_v11D[dest]:
  assumes "nop_v11 A n f"
  shows "v11 f"
    and "n ∈∘ ω"
    and "𝒟∘ f = A ^× n"
    and "ℛ∘ f ⊆∘ A"
  using assms unfolding nop_v11_def nop_v11_axioms_def by blast+

lemma nop_v11E[elim]:
  assumes "nop_v11 A n f"
  obtains "v11 f"
    and "n ∈∘ ω"
    and "𝒟∘ f = A ^× n"
    and "ℛ∘ f ⊆∘ A"
  using assms by force



subsection‹Surjective ‹n›-ary operation›

locale nop_onto = vsv f for A n f :: V +
  assumes nop_onto_n: "n ∈∘ ω" 
    and nop_onto_vdomain: "𝒟∘ f = A ^× n"
    and nop_onto_vrange: "ℛ∘ f = A"

sublocale nop_onto ⊆ nop 
proof
  show "vsv f" by (rule vsv_axioms)
  show "n ∈∘ ω" by (rule nop_onto_n)
  show "𝒟∘ f = A ^× n" by (rule nop_onto_vdomain)
  show "ℛ∘ f ⊆∘ A" by (simp add: nop_onto_vrange)
qed


text‹Rules.›

lemma nop_ontoI[intro]:
  assumes "vsv f"
    and "n ∈∘ ω"
    and "𝒟∘ f = A ^× n"
    and "ℛ∘ f = A"
  shows "nop_onto A n f"
  using assms unfolding nop_onto_def nop_onto_axioms_def by blast

lemma nop_ontoD[dest]:
  assumes "nop_onto A n f"
  shows "vsv f"
    and "n ∈∘ ω"
    and "𝒟∘ f = A ^× n"
    and "ℛ∘ f = A"
  using assms unfolding nop_onto_def nop_onto_axioms_def by auto

lemma nop_ontoE[elim]:
  assumes "nop_onto A n f"
  obtains "vsv f"
    and "n ∈∘ ω"
    and "𝒟∘ f = A ^× n"
    and "ℛ∘ f = A"
  using assms by force



subsection‹Bijective ‹n›-ary operation›

locale nop_bij = v11 f for A n f :: V +
  assumes nop_bij_n: "n ∈∘ ω" 
    and nop_bij_vdomain: "𝒟∘ f = A ^× n"
    and nop_bij_vrange: "ℛ∘ f = A"

sublocale nop_bij ⊆ nop_v11 
proof
  show "v11 f" by (rule v11_axioms)
  show "n ∈∘ ω" by (rule nop_bij_n)
  show "𝒟∘ f = A ^× n" by (rule nop_bij_vdomain)
  show "ℛ∘ f ⊆∘ A" by (simp add: nop_bij_vrange)
qed

sublocale nop_bij ⊆ nop_onto 
proof
  show "vsv f" by (rule vsv_axioms)
  show "n ∈∘ ω" by (rule nop_bij_n)
  show "𝒟∘ f = A ^× n" by (rule nop_bij_vdomain)
  show "ℛ∘ f = A" by (rule nop_bij_vrange)
qed


text‹Rules.›

lemma nop_bijI[intro]:
  assumes "v11 f"
    and "n ∈∘ ω"
    and "𝒟∘ f = A ^× n"
    and "ℛ∘ f = A"
  shows "nop_bij A n f"
  using assms unfolding nop_bij_def nop_bij_axioms_def by blast

lemma nop_bijD[dest]:
  assumes "nop_bij A n f"
  shows "v11 f"
    and "n ∈∘ ω"
    and "𝒟∘ f = A ^× n"
    and "ℛ∘ f = A"
  using assms unfolding nop_bij_def nop_bij_axioms_def by auto

lemma nop_bijE[elim]:
  assumes "nop_bij A n f"
  obtains "v11 f"
    and "n ∈∘ ω"
    and "𝒟∘ f = A ^× n"
    and "ℛ∘ f = A"
  using assms by force



subsection‹Scalar›

locale scalar = 
  fixes A f
  assumes scalar_nop: "nop A 0 f"

sublocale scalar ⊆ nop A 0 f
  rewrites scalar_vdomain[simp]: "A ^× 0 = set {0}"
  by (auto simp: scalar_nop)


text‹Rules.›

lemmas scalarI[intro] = scalar.intro

lemma scalarD[dest]:
  assumes "scalar A f"
  shows "nop A 0 f" 
  using assms unfolding scalar_def by auto

lemma scalarE[elim]:
  assumes "scalar A f"
  obtains "nop A 0 f"
  using assms by auto



subsection‹Unary operation›

locale unop = nop A ‹1ℕ› f for A f


text‹Rules.›

lemmas unopI[intro] = unop.intro

lemma unopD[dest]:
  assumes "unop A f"
  shows "nop A (1ℕ) f" 
  using assms unfolding unop_def by auto

lemma unopE[elim]:
  assumes "unop A f"
  obtains "nop A (1ℕ) f"
  using assms by blast



subsection‹Injective unary operation›

locale unop_v11 = nop_v11 A ‹1ℕ› f for A f

sublocale unop_v11 ⊆ unop A f by (intro unopI) (simp add: nop_axioms)


text‹Rules.›

lemma unop_v11I[intro]:
  assumes "nop_v11 A (1ℕ) f"
  shows "unop_v11 A f"
  using assms by (rule unop_v11.intro)

lemma unop_v11D[dest]:
  assumes "unop_v11 A f"
  shows "nop_v11 A (1ℕ) f"
  using assms by (rule unop_v11.axioms)

lemma unop_v11E[elim]:
  assumes "unop_v11 A f"
  obtains "nop_v11 A (1ℕ) f"
  using assms by blast



subsection‹Surjective unary operation›

locale unop_onto = nop_onto A ‹1ℕ› f for A f

sublocale unop_onto ⊆ unop A f by (intro unopI) (simp add: nop_axioms)


text‹Rules.›

lemma unop_ontoI[intro]:
  assumes "nop_onto A (1ℕ) f"
  shows "unop_onto A f"
  using assms by (rule unop_onto.intro)

lemma unop_ontoD[dest]:
  assumes "unop_onto A f"
  shows "nop_onto A (1ℕ) f"
  using assms by (rule unop_onto.axioms)

lemma unop_ontoE[elim]:
  assumes "unop_onto A f"
  obtains "nop_onto A (1ℕ) f"
  using assms by blast

lemma unop_ontoI'[intro]:
  assumes "unop A f" and "A ⊆∘ ℛ∘ f"
  shows "unop_onto A f"
proof-
  interpret unop A f by (rule assms(1))
  from assms(2) nop_vrange have "A = ℛ∘ f" by simp
  with assms(1) show "unop_onto A f" by auto
qed



subsection‹Bijective unary operation›

locale unop_bij = nop_bij A ‹1ℕ› f for A f

sublocale unop_bij ⊆ unop_v11 A f  
  by (intro unop_v11I) (simp add: nop_v11_axioms)

sublocale unop_bij ⊆ unop_onto A f  
  by (intro unop_ontoI) (simp add: nop_onto_axioms)


text‹Rules.›

lemma unop_bijI[intro]:
  assumes "nop_bij A (1ℕ) f"
  shows "unop_bij A f"
  using assms by (rule unop_bij.intro)

lemma unop_bijD[dest]:
  assumes "unop_bij A f"
  shows "nop_bij A (1ℕ) f"
  using assms by (rule unop_bij.axioms)

lemma unop_bijE[elim]:
  assumes "unop_bij A f"
  obtains "nop_bij A (1ℕ) f"
  using assms by blast

lemma unop_bijI'[intro]:
  assumes "unop_v11 A f" and "A ⊆∘ ℛ∘ f"
  shows "unop_bij A f"
proof-
  interpret unop_v11 A f by (rule assms(1))
  from assms(2) nop_vrange have "A = ℛ∘ f" by simp
  with assms(1) show "unop_bij A f" by auto
qed



subsection‹Partial binary operation›

locale pbinop = pnop A ‹2ℕ› f for A f

sublocale pbinop ⊆ dom: fbrelation ‹𝒟∘ f› 
proof
  from pnop_vdomain show "fpairs (𝒟∘ f) = 𝒟∘ f"
    by (intro vsubset_antisym vsubsetI) auto
qed


text‹Rules.›

lemmas pbinopI[intro] = pbinop.intro

lemma pbinopD[dest]:
  assumes "pbinop A f"
  shows "pnop A (2ℕ) f"
  using assms unfolding pbinop_def by auto

lemma pbinopE[elim]:
  assumes "pbinop A f"
  obtains "pnop A (2ℕ) f"
  using assms by auto


text‹Elementary properties.›

lemma (in pbinop) fbinop_vcard: 
  assumes "x ∈∘ 𝒟∘ f" 
  shows "vcard x = 2ℕ"
proof-
  from assms dom.fbrelation_axioms obtain a b where x_def: "x = [a, b]∘" by blast
  show ?thesis by (auto simp: x_def nat_omega_simps)
qed




subsection‹Total binary operation›

locale binop = nop A ‹2ℕ› f for A f

sublocale binop ⊆ pbinop by unfold_locales


text‹Rules.›

lemmas binopI[intro] = binop.intro

lemma binopD[dest]:
  assumes "binop A f"
  shows "nop A (2ℕ) f"
  using assms unfolding binop_def by auto

lemma binopE[elim]:
  assumes "binop A f"
  obtains "nop A (2ℕ) f"
  using assms by auto


text‹Elementary properties.›

lemma binop_eqI:
  assumes "binop A g"
    and "binop A f"
    and "⋀a b. ⟦ a ∈∘ A; b ∈∘ A ⟧ ⟹ g⦇a, b⦈∙ = f⦇a, b⦈∙"
  shows "g = f"
proof-
  interpret g: binop A g by (rule assms(1))
  interpret f: binop A f by (rule assms(2))
  show ?thesis
  proof
    (
      rule vsv_eqI; 
      (intro g.vsv_axioms f.vsv_axioms)?;
      (unfold g.nop_vdomain f.nop_vdomain)
    )
    fix ab assume "ab ∈∘ A ^× 2ℕ"
    then obtain a b where ab_def: "ab = [a, b]∘" 
      and a: "a ∈∘ A"
      and b: "b ∈∘ A" 
      by auto
    show "g⦇ab⦈ = f⦇ab⦈" unfolding ab_def by (rule assms(3)[OF a b])
  qed simp
qed

lemma (in binop) binop_app_in_vrange[intro]:
  assumes "a ∈∘ A" and "b ∈∘ A"
  shows "f⦇a, b⦈∙ ∈∘ ℛ∘ f"
proof-
  from assms have "[a, b]∘ ∈∘ A ^× 2ℕ" by (auto simp: nat_omega_simps)
  then show ?thesis by (simp add: nop_vdomain vsv_vimageI2)
qed



subsection‹Injective binary operation›

locale binop_v11 = nop_v11 A ‹2ℕ› f for A f

sublocale binop_v11 ⊆ binop A f by (intro binopI) (simp add: nop_axioms)


text‹Rules.›

lemma binop_v11I[intro]:
  assumes "nop_v11 A (2ℕ) f"
  shows "binop_v11 A f"
  using assms by (rule binop_v11.intro)

lemma binop_v11D[dest]:
  assumes "binop_v11 A f"
  shows "nop_v11 A (2ℕ) f"
  using assms by (rule binop_v11.axioms)

lemma binop_v11E[elim]:
  assumes "binop_v11 A f"
  obtains "nop_v11 A (2ℕ) f"
  using assms by blast



subsection‹Surjective binary operation›

locale binop_onto = nop_onto A ‹2ℕ› f for A f

sublocale binop_onto ⊆ binop A f by (intro binopI) (simp add: nop_axioms)


text‹Rules.›

lemma binop_ontoI[intro]:
  assumes "nop_onto A (2ℕ) f"
  shows "binop_onto A f"
  using assms by (rule binop_onto.intro)

lemma binop_ontoD[dest]:
  assumes "binop_onto A f"
  shows "nop_onto A (2ℕ) f"
  using assms by (rule binop_onto.axioms)

lemma binop_ontoE[elim]:
  assumes "binop_onto A f"
  obtains "nop_onto A (2ℕ) f"
  using assms by blast

lemma binop_ontoI'[intro]:
  assumes "binop A f" and "A ⊆∘ ℛ∘ f"
  shows "binop_onto A f"
proof-
  interpret binop A f by (rule assms(1))
  from assms(2) nop_vrange have "A = ℛ∘ f" by simp
  with assms(1) show "binop_onto A f" by auto
qed



subsection‹Bijective binary operation›

locale binop_bij = nop_bij A ‹2ℕ› f for A f

sublocale binop_bij ⊆ binop_v11 A f 
  by (intro binop_v11I) (simp add: nop_v11_axioms)

sublocale binop_bij ⊆ binop_onto A f 
  by (intro binop_ontoI) (simp add: nop_onto_axioms)


text‹Rules.›

lemma binop_bijI[intro]:
  assumes "nop_bij A (2ℕ) f"
  shows "binop_bij A f"
  using assms by (rule binop_bij.intro)

lemma binop_bijD[dest]:
  assumes "binop_bij A f"
  shows "nop_bij A (2ℕ) f"
  using assms by (rule binop_bij.axioms)

lemma binop_bijE[elim]:
  assumes "binop_bij A f"
  obtains "nop_bij A (2ℕ) f"
  using assms by blast

lemma binop_bijI'[intro]:
  assumes "binop_v11 A f" and "A ⊆∘ ℛ∘ f"
  shows "binop_bij A f"
proof-
  interpret binop_v11 A f by (rule assms(1))
  from assms(2) nop_vrange have "A = ℛ∘ f" by simp
  with assms(1) show "binop_bij A f" by auto
qed



subsection‹Flip›

definition fflip :: "V ⇒ V"
  where "fflip f = (λab∈∘(𝒟∘ f)¯∙. f⦇ab⦇1ℕ⦈, ab⦇0⦈⦈∙)"


text‹Elementary properties.›

lemma fflip_vempty[simp]: "fflip 0 = 0" unfolding fflip_def by auto

lemma fflip_vsv: "vsv (fflip f)"
  by (intro vsvI) (auto simp: fflip_def)

lemma vdomain_fflip[simp]: "𝒟∘ (fflip f) = (𝒟∘ f)¯∙" 
  unfolding fflip_def by simp

lemma (in pbinop) vrange_fflip: "ℛ∘ (fflip f) = ℛ∘ f"
  unfolding fflip_def
proof(intro vsubset_antisym vsubsetI)
  fix y assume "y ∈∘ ℛ∘ ((λx∈∘(𝒟∘ f)¯∙. f⦇x⦇1ℕ⦈, x⦇0⦈⦈∙))" 
  then obtain x where "x ∈∘ (𝒟∘ f)¯∙" and y_def: "y = f⦇x⦇1ℕ⦈, x⦇0⦈⦈∙" by fast
  then obtain a b where x_def: "x = [b, a]∘" by clarsimp
  have y_def': "y = f⦇a, b⦈∙" 
    unfolding y_def x_def by (simp add: nat_omega_simps)
  from x_def ‹x ∈∘ (𝒟∘ f)¯∙› have "[a, b]∘ ∈∘ 𝒟∘ f" by clarsimp
  then show "y ∈∘ ℛ∘ f" unfolding y_def' by (simp add: vsv_vimageI2)
next
  fix y assume "y ∈∘ ℛ∘ f"
  with vrange_atD obtain x where x: "x ∈∘ 𝒟∘ f" and y_def: "y = f⦇x⦈" by blast
  with dom.fbrelation obtain a b where x_def: "x = [a, b]∘" by blast
  from x have ba: "[b, a]∘ ∈∘ (𝒟∘ f)¯∙" unfolding x_def by clarsimp
  then have y_def': "y = f⦇[b, a]∘⦇1ℕ⦈, [b, a]∘⦇0⦈⦈∙"
    unfolding y_def x_def by (auto simp: nat_omega_simps)
  then show "y ∈∘ ℛ∘ ((λab∈∘(𝒟∘ f)¯∙. f⦇ab⦇1ℕ⦈, ab⦇0⦈⦈∙))"
    unfolding y_def'
    by (metis (lifting) ba beta rel_VLambda.vsv_vimageI2 vdomain_VLambda)
qed

lemma fflip_app[simp]: 
  assumes "[a, b]∘ ∈∘ 𝒟∘ f"
  shows "fflip f⦇b, a⦈∙ = f⦇a, b⦈∙"
proof-
  from assms have "[b, a]∘ ∈∘ 𝒟∘ (fflip f)" by clarsimp
  then show "fflip f⦇b, a⦈∙ = f⦇a, b⦈∙" 
    by (simp add: fflip_def ord_of_nat_succ_vempty)
qed

lemma (in pbinop) pbinop_fflip_fflip: "fflip (fflip f) = f"
proof(rule vsv_eqI)
  show "vsv (fflip (fflip f))" by (simp add: fflip_vsv)
  show "vsv f" by (rule vsv_axioms)
  show dom: "𝒟∘ (fflip (fflip f)) = 𝒟∘ f" by simp
  fix x assume prems: "x ∈∘ 𝒟∘ (fflip (fflip f))"
  with dom dom.fbrelation_axioms obtain a b where x_def: "x = [a, b]∘" by auto
  from prems show "fflip (fflip f)⦇x⦈ = f⦇x⦈" 
    unfolding x_def by (auto simp: fconverseI)
qed

lemma (in binop) pbinop_fflip_app[simp]: 
  assumes "a ∈∘ A" and "b ∈∘ A"
  shows "fflip f⦇b, a⦈∙ = f⦇a, b⦈∙"
proof-
  from assms have "[a, b]∘ ∈∘ 𝒟∘ f" 
    unfolding nop_vdomain by (auto simp: nat_omega_simps)
  then show ?thesis by auto
qed

lemma fflip_vsingleton: "fflip (set {⟨[a, b]∘, c⟩}) = set {⟨[b, a]∘, c⟩}"
proof-
  have dom_lhs: "𝒟∘ (fflip (set {⟨[a, b]∘, c⟩})) = set {[b, a]∘}"
    unfolding fflip_def by auto
  have dom_rhs: "𝒟∘ (set {⟨[b, a]∘, c⟩}) = set {[b, a]∘}" by simp
  show ?thesis
  proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
    fix q assume "q ∈∘ set {[b, a]∘}"
    then have q_def: "q = [b, a]∘" by simp
    show "fflip (set {⟨[a, b]∘, c⟩})⦇q⦈ = set {⟨[b, a]∘, c⟩}⦇q⦈"
      unfolding q_def by auto
  qed (auto simp: fflip_def)
qed

text‹\newpage›

end