# Theory Axioms

section ‹Axioms of registers›

theory Axioms
imports Main
begin

class domain
instance prod :: (domain,domain) domain
by intro_classes

typedecl 'a update
axiomatization comp_update :: "'a::domain update ⇒ 'a update ⇒ 'a update" where
comp_update_assoc: "comp_update (comp_update a b) c = comp_update a (comp_update b c)"
axiomatization id_update :: "'a::domain update" where
id_update_left: "comp_update id_update a = a" and
id_update_right: "comp_update a id_update = a"

axiomatization preregister :: ‹('a::domain update ⇒ 'b::domain update) ⇒ bool›
axiomatization where
comp_preregister: "preregister F ⟹ preregister G ⟹ preregister (G ∘ F)" and
id_preregister: ‹preregister id›
for F :: ‹'a::domain update ⇒ 'b::domain update› and G :: ‹'b update ⇒ 'c::domain update›

axiomatization where
preregister_mult_right: ‹preregister (λa. comp_update a z)› and
preregister_mult_left: ‹preregister (λa. comp_update z a)›
for z :: "'a::domain update"

axiomatization tensor_update :: ‹'a::domain update ⇒ 'b::domain update ⇒ ('a×'b) update›
where tensor_extensionality: "preregister F ⟹ preregister G ⟹ (⋀a b. F (tensor_update a b) = G (tensor_update a b)) ⟹ F = G"
for F G :: ‹('a×'b) update ⇒ 'c::domain update›

axiomatization where tensor_update_mult: ‹comp_update (tensor_update a c) (tensor_update b d) = tensor_update (comp_update a b) (comp_update c d)›
for a b :: ‹'a::domain update› and c d :: ‹'b::domain update›

axiomatization register :: ‹('a update ⇒ 'b update) ⇒ bool›
axiomatization where
register_preregister: "register F ⟹ preregister F" and
register_comp: "register F ⟹ register G ⟹ register (G ∘ F)"  and
register_mult: "register F ⟹ comp_update (F a) (F b) = F (comp_update a b)" and
register_of_id: ‹register F ⟹ F id_update = id_update› and
register_id: ‹register (id :: 'a update ⇒ 'a update)›
for F :: "'a::domain update ⇒ 'b::domain update" and G :: "'b update ⇒ 'c::domain update"

axiomatization where register_tensor_left: ‹register (λa. tensor_update a id_update)›
axiomatization where register_tensor_right: ‹register (λa. tensor_update id_update a)›

axiomatization register_pair ::
‹('a::domain update ⇒ 'c::domain update) ⇒ ('b::domain update ⇒ 'c update)
⇒ (('a×'b) update ⇒ 'c update)› where
register_pair_is_register: ‹register F ⟹ register G ⟹ (⋀a b. comp_update (F a) (G b) = comp_update (G b) (F a))
⟹ register (register_pair F G)› and
register_pair_apply: ‹register F ⟹ register G ⟹ (⋀a b. comp_update (F a) (G b) = comp_update (G b) (F a))
⟹ (register_pair F G) (tensor_update a b) = comp_update (F a) (G b)›

end


# Theory Laws

section ‹Generic laws about registers›

theory Laws
imports Axioms
begin

text ‹This notation is only used inside this file›
notation comp_update (infixl "*⇩u" 55)
notation tensor_update (infixr "⊗⇩u" 70)
notation register_pair ("'(_;_')")

subsection ‹Elementary facts›

declare id_preregister[simp]
declare id_update_left[simp]
declare id_update_right[simp]
declare register_preregister[simp]
declare register_comp[simp]
declare register_of_id[simp]
declare register_tensor_left[simp]
declare register_tensor_right[simp]
declare preregister_mult_right[simp]
declare preregister_mult_left[simp]
declare register_id[simp]

subsection ‹Preregisters›

lemma preregister_tensor_left[simp]: ‹preregister (λb::'b::domain update. tensor_update a b)›
for a :: ‹'a::domain update›
proof -
have ‹preregister ((λb1::('a×'b) update. (a ⊗⇩u id_update) *⇩u b1) o (λb. tensor_update id_update b))›
by (rule comp_preregister; simp)
then show ?thesis
qed

lemma preregister_tensor_right[simp]: ‹preregister (λa::'a::domain update. tensor_update a b)›
for b :: ‹'b::domain update›
proof -
have ‹preregister ((λa1::('a×'b) update. (id_update ⊗⇩u b) *⇩u a1) o (λa. tensor_update a id_update))›
by (rule comp_preregister, simp_all)
then show ?thesis
qed

subsection ‹Registers›

lemma id_update_tensor_register[simp]:
assumes ‹register F›
shows ‹register (λa::'a::domain update. id_update ⊗⇩u F a)›
using assms apply (rule register_comp[unfolded o_def])
by simp

lemma register_tensor_id_update[simp]:
assumes ‹register F›
shows ‹register (λa::'a::domain update. F a ⊗⇩u id_update)›
using assms apply (rule register_comp[unfolded o_def])
by simp

subsection ‹Tensor product of registers›

definition register_tensor  (infixr "⊗⇩r" 70) where
"register_tensor F G = register_pair (λa. tensor_update (F a) id_update) (λb. tensor_update id_update (G b))"

lemma register_tensor_is_register:
fixes F :: "'a::domain update ⇒ 'b::domain update" and G :: "'c::domain update ⇒ 'd::domain update"
shows "register F ⟹ register G ⟹ register (F ⊗⇩r G)"
unfolding register_tensor_def
apply (rule register_pair_is_register)

lemma register_tensor_apply[simp]:
fixes F :: "'a::domain update ⇒ 'b::domain update" and G :: "'c::domain update ⇒ 'd::domain update"
assumes ‹register F› and ‹register G›
shows "(F ⊗⇩r G) (a ⊗⇩u b) = F a ⊗⇩u G b"
unfolding register_tensor_def
apply (subst register_pair_apply)
unfolding register_tensor_def

definition "separating (_::'b::domain itself) A ⟷
(∀F G :: 'a::domain update ⇒ 'b update. preregister F ⟶ preregister G ⟶ (∀x∈A. F x = G x) ⟶ F = G)"

lemma separating_UNIV[simp]: ‹separating TYPE(_) UNIV›
unfolding separating_def by auto

lemma separating_mono: ‹A ⊆ B ⟹ separating TYPE('a::domain) A ⟹ separating TYPE('a) B›
unfolding separating_def by (meson in_mono)

lemma register_eqI: ‹separating TYPE('b::domain) A ⟹ preregister F ⟹ preregister G ⟹ (⋀x. x∈A ⟹ F x = G x) ⟹ F = (G::_ ⇒ 'b update)›
unfolding separating_def by auto

lemma separating_tensor:
fixes A :: ‹'a::domain update set› and B :: ‹'b::domain update set›
assumes [simp]: ‹separating TYPE('c::domain) A›
assumes [simp]: ‹separating TYPE('c) B›
shows ‹separating TYPE('c) {a ⊗⇩u b | a b. a∈A ∧ b∈B}›
proof (unfold separating_def, intro allI impI)
fix F G :: ‹('a×'b) update ⇒ 'c update›
assume [simp]: ‹preregister F› ‹preregister G›
have [simp]: ‹preregister (λx. F (a ⊗⇩u x))› for a
using _ ‹preregister F› apply (rule comp_preregister[unfolded o_def])
by simp
have [simp]: ‹preregister (λx. G (a ⊗⇩u x))› for a
using _ ‹preregister G› apply (rule comp_preregister[unfolded o_def])
by simp
have [simp]: ‹preregister (λx. F (x ⊗⇩u b))› for b
using _ ‹preregister F› apply (rule comp_preregister[unfolded o_def])
by simp
have [simp]: ‹preregister (λx. G (x ⊗⇩u b))› for b
using _ ‹preregister G› apply (rule comp_preregister[unfolded o_def])
by simp

assume ‹∀x∈{a ⊗⇩u b |a b. a∈A ∧ b∈B}. F x = G x›
then have EQ: ‹F (a ⊗⇩u b) = G (a ⊗⇩u b)› if ‹a ∈ A› and ‹b ∈ B› for a b
using that by auto
then have ‹F (a ⊗⇩u b) = G (a ⊗⇩u b)› if ‹a ∈ A› for a b
apply (rule register_eqI[where A=B, THEN fun_cong, where x=b, rotated -1])
using that by auto
then have ‹F (a ⊗⇩u b) = G (a ⊗⇩u b)› for a b
apply (rule register_eqI[where A=A, THEN fun_cong, where x=a, rotated -1])
by auto
then show "F = G"
apply (rule tensor_extensionality[rotated -1])
by auto
qed

lemma register_tensor_distrib:
assumes [simp]: ‹register F› ‹register G› ‹register H› ‹register L›
shows ‹(F ⊗⇩r G) o (H ⊗⇩r L) = (F o H) ⊗⇩r (G o L)›
apply (rule tensor_extensionality)
by (auto intro!: register_comp register_preregister register_tensor_is_register)

text ‹The following is easier to apply using the @{method rule}-method than @{thm [source] separating_tensor}›
lemma separating_tensor':
fixes A :: ‹'a::domain update set› and B :: ‹'b::domain update set›
assumes ‹separating TYPE('c::domain) A›
assumes ‹separating TYPE('c) B›
assumes ‹C = {a ⊗⇩u b | a b. a∈A ∧ b∈B}›
shows ‹separating TYPE('c) C›
using assms

lemma tensor_extensionality3:
fixes F G :: ‹('a::domain×'b::domain×'c::domain) update ⇒ 'd::domain update›
assumes [simp]: ‹register F› ‹register G›
assumes "⋀f g h. F (f ⊗⇩u g ⊗⇩u h) = G (f ⊗⇩u g ⊗⇩u h)"
shows "F = G"
proof (rule register_eqI[where A=‹{a⊗⇩ub⊗⇩uc| a b c. True}›])
have ‹separating TYPE('d) {b ⊗⇩u c |b c. True}›
apply (rule separating_tensor'[where A=UNIV and B=UNIV])
by auto
then show ‹separating TYPE('d) {a ⊗⇩u b ⊗⇩u c |a b c. True}›
apply (rule_tac separating_tensor'[where A=UNIV and B=‹{b⊗⇩uc| b c. True}›])
by auto
show ‹preregister F› ‹preregister G› by auto
show ‹x ∈ {a ⊗⇩u b ⊗⇩u c |a b c. True} ⟹ F x = G x› for x
using assms(3) by auto
qed

lemma tensor_extensionality3':
fixes F G :: ‹(('a::domain×'b::domain)×'c::domain) update ⇒ 'd::domain update›
assumes [simp]: ‹register F› ‹register G›
assumes "⋀f g h. F ((f ⊗⇩u g) ⊗⇩u h) = G ((f ⊗⇩u g) ⊗⇩u h)"
shows "F = G"
proof (rule register_eqI[where A=‹{(a⊗⇩ub)⊗⇩uc| a b c. True}›])
have ‹separating TYPE('d) {a ⊗⇩u b | a b. True}›
apply (rule separating_tensor'[where A=UNIV and B=UNIV])
by auto
then show ‹separating TYPE('d) {(a ⊗⇩u b) ⊗⇩u c |a b c. True}›
apply (rule_tac separating_tensor'[where B=UNIV and A=‹{a⊗⇩ub| a b. True}›])
by auto
show ‹preregister F› ‹preregister G› by auto
show ‹x ∈ {(a ⊗⇩u b) ⊗⇩u c |a b c. True} ⟹ F x = G x› for x
using assms(3) by auto
qed

lemma register_tensor_id[simp]: ‹id ⊗⇩r id = id›
apply (rule tensor_extensionality)

subsection ‹Pairs and compatibility›

definition compatible :: ‹('a::domain update ⇒ 'c::domain update)
⇒ ('b::domain update ⇒ 'c update) ⇒ bool› where
‹compatible F G ⟷ register F ∧ register G ∧ (∀a b. F a *⇩u G b = G b *⇩u F a)›

lemma compatibleI:
assumes "register F" and "register G"
assumes ‹⋀a b. (F a) *⇩u (G b) = (G b) *⇩u (F a)›
shows "compatible F G"
using assms unfolding compatible_def by simp

lemma swap_registers:
assumes "compatible R S"
shows "R a *⇩u S b = S b *⇩u R a"
using assms unfolding compatible_def by metis

lemma compatible_sym: "compatible x y ⟹ compatible y x"

lemma pair_is_register[simp]:
assumes "compatible F G"
shows "register (F; G)"
by (metis assms compatible_def register_pair_is_register)

lemma register_pair_apply:
assumes ‹compatible F G›
shows ‹(F; G) (a ⊗⇩u b) = (F a) *⇩u (G b)›
apply (rule register_pair_apply)
using assms unfolding compatible_def by metis+

lemma register_pair_apply':
assumes ‹compatible F G›
shows ‹(F; G) (a ⊗⇩u b) = (G b) *⇩u (F a)›
apply (subst register_pair_apply)
using assms by (auto simp: compatible_def intro: register_preregister)

lemma compatible_comp_left[simp]: "compatible F G ⟹ register H ⟹ compatible (F ∘ H) G"

lemma compatible_comp_right[simp]: "compatible F G ⟹ register H ⟹ compatible F (G ∘ H)"

lemma compatible_comp_inner[simp]:
"compatible F G ⟹ register H ⟹ compatible (H ∘ F) (H ∘ G)"
by (smt (verit, best) comp_apply compatible_def register_comp register_mult)

lemma compatible_register1: ‹compatible F G ⟹ register F›
lemma compatible_register2: ‹compatible F G ⟹ register G›

lemma pair_o_tensor:
assumes "compatible A B" and [simp]: ‹register C› and [simp]: ‹register D›
shows "(A; B) o (C ⊗⇩r D) = (A o C; B o D)"
apply (rule tensor_extensionality)
using assms by (simp_all add: register_tensor_is_register register_pair_apply comp_preregister)

lemma compatible_tensor_id_update_left[simp]:
fixes F :: "'a::domain update ⇒ 'c::domain update" and G :: "'b::domain update ⇒ 'c::domain update"
assumes "compatible F G"
shows "compatible (λa. id_update ⊗⇩u F a) (λa. id_update ⊗⇩u G a)"
using assms apply (rule compatible_comp_inner[unfolded o_def])
by simp

lemma compatible_tensor_id_update_right[simp]:
fixes F :: "'a::domain update ⇒ 'c::domain update" and G :: "'b::domain update ⇒ 'c::domain update"
assumes "compatible F G"
shows "compatible (λa. F a ⊗⇩u id_update) (λa. G a ⊗⇩u id_update)"
using assms apply (rule compatible_comp_inner[unfolded o_def])
by simp

lemma compatible_tensor_id_update_rl[simp]:
assumes "register F" and "register G"
shows "compatible (λa. F a ⊗⇩u id_update) (λa. id_update ⊗⇩u G a)"
apply (rule compatibleI)
using assms by (auto simp: tensor_update_mult)

lemma compatible_tensor_id_update_lr[simp]:
assumes "register F" and "register G"
shows "compatible (λa. id_update ⊗⇩u F a) (λa. G a ⊗⇩u id_update)"
apply (rule compatibleI)
using assms by (auto simp: tensor_update_mult)

lemma register_comp_pair:
assumes [simp]: ‹register F› and [simp]: ‹compatible G H›
shows "(F o G; F o H) = F o (G; H)"
proof (rule tensor_extensionality)
show ‹preregister (F ∘ G;F ∘ H)› and ‹preregister (F ∘ (G;H))›
by simp_all

have [simp]: ‹compatible (F o G) (F o H)›
apply (rule compatible_comp_inner, simp)
by simp
then have [simp]: ‹register (F ∘ G)› ‹register (F ∘ H)›
unfolding compatible_def by auto
from assms have [simp]: ‹register G› ‹register H›
unfolding compatible_def by auto
fix a b
show ‹(F ∘ G;F ∘ H) (a ⊗⇩u b) = (F ∘ (G;H)) (a ⊗⇩u b)›
by (auto simp: register_pair_apply register_mult tensor_update_mult)
qed

lemma swap_registers_left:
assumes "compatible R S"
shows "R a *⇩u S b *⇩u c = S b *⇩u R a *⇩u c"
using assms unfolding compatible_def by metis

lemma swap_registers_right:
assumes "compatible R S"
shows "c *⇩u R a *⇩u S b = c *⇩u S b *⇩u R a"
by (metis assms comp_update_assoc compatible_def)

lemmas compatible_ac_rules = swap_registers comp_update_assoc[symmetric] swap_registers_right

subsection ‹Fst and Snd›

definition Fst where ‹Fst a = a ⊗⇩u id_update›
definition Snd where ‹Snd a = id_update ⊗⇩u a›

lemma register_Fst[simp]: ‹register Fst›
unfolding Fst_def by (rule register_tensor_left)

lemma register_Snd[simp]: ‹register Snd›
unfolding Snd_def by (rule register_tensor_right)

lemma compatible_Fst_Snd[simp]: ‹compatible Fst Snd›
apply (rule compatibleI, simp, simp)
by (simp add: Fst_def Snd_def tensor_update_mult)

lemmas compatible_Snd_Fst[simp] = compatible_Fst_Snd[THEN compatible_sym]

definition ‹swap = (Snd; Fst)›

lemma swap_apply[simp]: "swap (a ⊗⇩u b) = (b ⊗⇩u a)"
unfolding swap_def
by (simp add: Axioms.register_pair_apply Fst_def Snd_def tensor_update_mult)

lemma swap_o_Fst: "swap o Fst = Snd"
by (auto simp add: Fst_def Snd_def)
lemma swap_o_Snd: "swap o Snd = Fst"
by (auto simp add: Fst_def Snd_def)

lemma register_swap[simp]: ‹register swap›

lemma pair_Fst_Snd: ‹(Fst; Snd) = id›
apply (rule tensor_extensionality)
by (simp_all add: register_pair_apply Fst_def Snd_def tensor_update_mult)

lemma swap_o_swap[simp]: ‹swap o swap = id›
by (metis swap_def compatible_Snd_Fst pair_Fst_Snd register_comp_pair register_swap swap_o_Fst swap_o_Snd)

lemma swap_swap[simp]: ‹swap (swap x) = x›

lemma inv_swap[simp]: ‹inv swap = swap›
by (meson inv_unique_comp swap_o_swap)

lemma register_pair_Fst:
assumes ‹compatible F G›
shows ‹(F;G) o Fst = F›
using assms by (auto intro!: ext simp: Fst_def register_pair_apply compatible_register2)

lemma register_pair_Snd:
assumes ‹compatible F G›
shows ‹(F;G) o Snd = G›
using assms by (auto intro!: ext simp: Snd_def register_pair_apply compatible_register1)

lemma register_Fst_register_Snd[simp]:
assumes ‹register F›
shows ‹(F o Fst; F o Snd) = F›
apply (rule tensor_extensionality)
using assms by (auto simp: register_pair_apply Fst_def Snd_def register_mult tensor_update_mult)

lemma register_Snd_register_Fst[simp]:
assumes ‹register F›
shows ‹(F o Snd; F o Fst) = F o swap›
apply (rule tensor_extensionality)
using assms by (auto simp: register_pair_apply Fst_def Snd_def register_mult tensor_update_mult)

lemma compatible3[simp]:
assumes [simp]: "compatible F G" and "compatible G H" and "compatible F H"
shows "compatible (F; G) H"
proof (rule compatibleI)
have [simp]: ‹register F› ‹register G› ‹register H›
using assms compatible_def by auto
then have [simp]: ‹preregister F› ‹preregister G› ‹preregister H›
using register_preregister by blast+
have [simp]: ‹preregister (λa. (F;G) a *⇩u z)› for z
apply (rule comp_preregister[unfolded o_def, of ‹(F;G)›])
by simp_all
have [simp]: ‹preregister (λa. z *⇩u (F;G) a)› for z
apply (rule comp_preregister[unfolded o_def, of ‹(F;G)›])
by simp_all
have "(F; G) (f ⊗⇩u g) *⇩u H h = H h *⇩u (F; G) (f ⊗⇩u g)" for f g h
proof -
have FH: "F f *⇩u H h = H h *⇩u F f"
using assms compatible_def by metis
have GH: "G g *⇩u H h = H h *⇩u G g"
using assms compatible_def by metis
have ‹(F; G) (f ⊗⇩u g) *⇩u (H h) = F f *⇩u G g *⇩u H h›
using ‹compatible F G› by (subst register_pair_apply, auto)
also have ‹… = H h *⇩u F f *⇩u G g›
using FH GH by (metis comp_update_assoc)
also have ‹… = H h *⇩u (F; G) (f ⊗⇩u g)›
using ‹compatible F G› by (subst register_pair_apply, auto simp: comp_update_assoc)
finally show ?thesis
by -
qed
then show "(F; G) fg *⇩u (H h) = (H h) *⇩u (F; G) fg" for fg h
apply (rule_tac tensor_extensionality[THEN fun_cong])
by auto
show "register H" and  "register (F; G)"
by simp_all
qed

lemma compatible3'[simp]:
assumes "compatible F G" and "compatible G H" and "compatible F H"
shows "compatible F (G; H)"
apply (rule compatible_sym)
apply (rule compatible3)
using assms by (auto simp: compatible_sym)

lemma pair_o_swap[simp]:
assumes [simp]: "compatible A B"
shows "(A; B) o swap = (B; A)"
proof (rule tensor_extensionality)
have [simp]: "preregister A" "preregister B"
apply (metis (no_types, opaque_lifting) assms compatible_register1 register_preregister)
by (metis (full_types) assms compatible_register2 register_preregister)
then show ‹preregister ((A; B) ∘ swap)›
by simp
show ‹preregister (B; A)›
by (metis (no_types, lifting) assms compatible_sym register_preregister pair_is_register)
show ‹((A; B) ∘ swap) (a ⊗⇩u b) = (B; A) (a ⊗⇩u b)› for a b
(* Without the "only:", we would not need the "apply subst",
but that proof fails when instantiated in Classical.thy *)
apply (simp only: o_def swap_apply)
apply (subst register_pair_apply, simp)
apply (subst register_pair_apply, simp add: compatible_sym)
by (metis (no_types, lifting) assms compatible_def)
qed

subsection ‹Compatibility of register tensor products›

lemma compatible_register_tensor:
fixes F :: ‹'a::domain update ⇒ 'e::domain update› and G :: ‹'b::domain update ⇒ 'f::domain update›
and F' :: ‹'c::domain update ⇒ 'e update› and G' :: ‹'d::domain update ⇒ 'f update›
assumes [simp]: ‹compatible F F'›
assumes [simp]: ‹compatible G G'›
shows ‹compatible (F ⊗⇩r G) (F' ⊗⇩r G')›
proof -
note [intro!] =
comp_preregister[OF _ preregister_mult_right, unfolded o_def]
comp_preregister[OF _ preregister_mult_left, unfolded o_def]
comp_preregister
register_tensor_is_register
have [simp]: ‹register F› ‹register G› ‹register F'› ‹register G'›
using assms compatible_def by blast+
have [simp]: ‹register (F ⊗⇩r G)› ‹register (F' ⊗⇩r G')›
have [simp]: ‹register (F;F')› ‹register (G;G')›
by auto
define reorder :: ‹(('a×'b) × ('c×'d)) update ⇒ (('a×'c) × ('b×'d)) update›
where ‹reorder = ((Fst o Fst; Snd o Fst); (Fst o Snd; Snd o Snd))›
have [simp]: ‹preregister reorder›
by (auto simp: reorder_def)
have [simp]: ‹reorder ((a ⊗⇩u b) ⊗⇩u (c ⊗⇩u d)) = ((a ⊗⇩u c) ⊗⇩u (b ⊗⇩u d))› for a b c d
by (simp add: Fst_def Snd_def tensor_update_mult)
define Φ where ‹Φ c d = ((F;F') ⊗⇩r (G;G')) o reorder o (λσ. σ ⊗⇩u (c ⊗⇩u d))› for c d
have [simp]: ‹preregister (Φ c d)› for c d
unfolding Φ_def
by (auto intro: register_preregister)
have ‹Φ c d (a ⊗⇩u b) = (F ⊗⇩r G) (a ⊗⇩u b) *⇩u (F' ⊗⇩r G') (c ⊗⇩u d)› for a b c d
unfolding Φ_def by (auto simp: register_pair_apply tensor_update_mult)
then have Φ1: ‹Φ c d σ = (F ⊗⇩r G) σ *⇩u (F' ⊗⇩r G') (c ⊗⇩u d)› for c d σ
apply (rule_tac fun_cong[of _ _ σ])
apply (rule tensor_extensionality)
by auto
have ‹Φ c d (a ⊗⇩u b) = (F' ⊗⇩r G') (c ⊗⇩u d) *⇩u (F ⊗⇩r G) (a ⊗⇩u b)› for a b c d
unfolding Φ_def apply (auto simp: register_pair_apply)
by (metis assms(1) assms(2) compatible_def tensor_update_mult)
then have Φ2: ‹Φ c d σ = (F' ⊗⇩r G') (c ⊗⇩u d) *⇩u (F ⊗⇩r G) σ› for c d σ
apply (rule_tac fun_cong[of _ _ σ])
apply (rule tensor_extensionality)
by auto
from Φ1 Φ2 have ‹(F ⊗⇩r G) σ *⇩u (F' ⊗⇩r G') τ = (F' ⊗⇩r G') τ *⇩u (F ⊗⇩r G) σ› for τ σ
apply (rule_tac fun_cong[of _ _ τ])
apply (rule tensor_extensionality)
by auto
then show ?thesis
apply (rule compatibleI[rotated -1])
by auto
qed

subsection ‹Associativity of the tensor product›

definition assoc :: ‹(('a::domain×'b::domain)×'c::domain) update ⇒ ('a×('b×'c)) update› where
‹assoc = ((Fst; Snd o Fst); Snd o Snd)›

lemma assoc_is_hom[simp]: ‹preregister assoc›
by (auto simp: assoc_def)

lemma assoc_apply[simp]: ‹assoc ((a ⊗⇩u b) ⊗⇩u c) = (a ⊗⇩u (b ⊗⇩u c))›
by (auto simp: assoc_def register_pair_apply Fst_def Snd_def tensor_update_mult)

definition assoc' :: ‹('a×('b×'c)) update ⇒ (('a::domain×'b::domain)×'c::domain) update› where
‹assoc' = (Fst o Fst; (Fst o Snd; Snd))›

lemma assoc'_is_hom[simp]: ‹preregister assoc'›
by (auto simp: assoc'_def)

lemma assoc'_apply[simp]: ‹assoc' (a ⊗⇩u (b ⊗⇩u c)) =  ((a ⊗⇩u b) ⊗⇩u c)›
by (auto simp: assoc'_def register_pair_apply Fst_def Snd_def tensor_update_mult)

lemma register_assoc[simp]: ‹register assoc›
unfolding assoc_def
by force

lemma register_assoc'[simp]: ‹register assoc'›
unfolding assoc'_def
by force

lemma pair_o_assoc[simp]:
assumes [simp]: ‹compatible F G› ‹compatible G H› ‹compatible F H›
shows ‹(F; (G; H)) ∘ assoc = ((F; G); H)›
proof (rule tensor_extensionality3')
show ‹register ((F; (G; H)) ∘ assoc)›
by simp
show ‹register ((F; G); H)›
by simp
show ‹((F; (G; H)) ∘ assoc) ((f ⊗⇩u g) ⊗⇩u h) = ((F; G); H) ((f ⊗⇩u g) ⊗⇩u h)› for f g h
by (simp add: register_pair_apply assoc_apply comp_update_assoc)
qed

lemma pair_o_assoc'[simp]:
assumes [simp]: ‹compatible F G› ‹compatible G H› ‹compatible F H›
shows ‹((F; G); H) ∘ assoc' = (F; (G; H))›
proof (rule tensor_extensionality3)
show ‹register (((F; G); H) ∘ assoc')›
by simp
show ‹register (F; (G; H))›
by simp
show ‹(((F; G); H) ∘ assoc') (f ⊗⇩u g ⊗⇩u h) = (F; (G; H)) (f ⊗⇩u g ⊗⇩u h)› for f g h
by (simp add: register_pair_apply assoc'_apply comp_update_assoc)
qed

lemma assoc'_o_assoc[simp]: ‹assoc' o assoc = id›
apply (rule tensor_extensionality3')
by auto

lemma assoc'_assoc[simp]: ‹assoc' (assoc x) = x›

lemma assoc_o_assoc'[simp]: ‹assoc o assoc' = id›
apply (rule tensor_extensionality3)
by auto

lemma assoc_assoc'[simp]: ‹assoc (assoc' x) = x›

lemma inv_assoc[simp]: ‹inv assoc = assoc'›
using assoc'_o_assoc assoc_o_assoc' inv_unique_comp by blast

lemma inv_assoc'[simp]: ‹inv assoc' = assoc›

lemma [simp]: ‹bij assoc›
using assoc'_o_assoc assoc_o_assoc' o_bij by blast

lemma [simp]: ‹bij assoc'›
using assoc'_o_assoc assoc_o_assoc' o_bij by blast

subsection ‹Iso-registers›

definition ‹iso_register F ⟷ register F ∧ (∃G. register G ∧ F o G = id ∧ G o F = id)›
for F :: ‹_::domain update ⇒ _::domain update›

lemma iso_registerI:
assumes ‹register F› ‹register G› ‹F o G = id› ‹G o F = id›
shows ‹iso_register F›
using assms(1) assms(2) assms(3) assms(4) iso_register_def by blast

lemma iso_register_inv: ‹iso_register F ⟹ iso_register (inv F)›
by (metis inv_unique_comp iso_register_def)

lemma iso_register_inv_comp1: ‹iso_register F ⟹ inv F o F = id›
using inv_unique_comp iso_register_def by blast

lemma iso_register_inv_comp2: ‹iso_register F ⟹ F o inv F = id›
using inv_unique_comp iso_register_def by blast

lemma iso_register_id[simp]: ‹iso_register id›

lemma iso_register_is_register: ‹iso_register F ⟹ register F›
using iso_register_def by blast

lemma iso_register_comp[simp]:
assumes [simp]: ‹iso_register F› ‹iso_register G›
shows ‹iso_register (F o G)›
proof -
from assms obtain F' G' where [simp]: ‹register F'› ‹register G'› ‹F o F' = id› ‹F' o F = id›
‹G o G' = id› ‹G' o G = id›
by (meson iso_register_def)
show ?thesis
apply (rule iso_registerI[where G=‹G' o F'›])
apply (auto simp: register_tensor_is_register iso_register_is_register register_tensor_distrib)
apply (metis ‹F ∘ F' = id› ‹G ∘ G' = id› fcomp_assoc fcomp_comp id_fcomp)
by (metis (no_types, lifting) ‹F ∘ F' = id› ‹F' ∘ F = id› ‹G' ∘ G = id› fun.map_comp inj_iff inv_unique_comp o_inv_o_cancel)
qed

lemma iso_register_tensor_is_iso_register[simp]:
assumes [simp]: ‹iso_register F› ‹iso_register G›
shows ‹iso_register (F ⊗⇩r G)›
proof -
from assms obtain F' G' where [simp]: ‹register F'› ‹register G'› ‹F o F' = id› ‹F' o F = id›
‹G o G' = id› ‹G' o G = id›
by (meson iso_register_def)
show ?thesis
apply (rule iso_registerI[where G=‹F' ⊗⇩r G'›])
by (auto simp: register_tensor_is_register iso_register_is_register register_tensor_distrib)
qed

lemma iso_register_bij: ‹iso_register F ⟹ bij F›
using iso_register_def o_bij by auto

lemma inv_register_tensor[simp]:
assumes [simp]: ‹iso_register F› ‹iso_register G›
shows ‹inv (F ⊗⇩r G) = inv F ⊗⇩r inv G›
apply (auto intro!: inj_imp_inv_eq bij_is_inj iso_register_bij
simp: register_tensor_distrib[unfolded o_def, THEN fun_cong] iso_register_is_register
iso_register_inv bij_is_surj iso_register_bij surj_f_inv_f)
by (metis eq_id_iff register_tensor_id)

lemma iso_register_swap[simp]: ‹iso_register swap›
apply (rule iso_registerI[of _ swap])
by auto

lemma iso_register_assoc[simp]: ‹iso_register assoc›
apply (rule iso_registerI[of _ assoc'])
by auto

lemma iso_register_assoc'[simp]: ‹iso_register assoc'›
apply (rule iso_registerI[of _ assoc])
by auto

definition ‹equivalent_registers F G ⟷ (register F ∧ (∃I. iso_register I ∧ F o I = G))›
for F G :: ‹_::domain update ⇒ _::domain update›

lemma iso_register_equivalent_id[simp]: ‹equivalent_registers id F ⟷ iso_register F›

lemma equivalent_registersI:
assumes ‹register F›
assumes ‹iso_register I›
assumes ‹F o I = G›
shows ‹equivalent_registers F G›
using assms unfolding equivalent_registers_def by blast

lemma equivalent_registers_register_left: ‹equivalent_registers F G ⟹ register F›
using equivalent_registers_def by auto

lemma equivalent_registers_register_right: ‹register G› if ‹equivalent_registers F G›
by (metis equivalent_registers_def iso_register_def register_comp that)

lemma equivalent_registers_sym:
assumes ‹equivalent_registers F G›
shows ‹equivalent_registers G F›
by (smt (verit) assms comp_id equivalent_registers_def equivalent_registers_register_right fun.map_comp iso_register_def)

lemma equivalent_registers_trans[trans]:
assumes ‹equivalent_registers F G› and ‹equivalent_registers G H›
shows ‹equivalent_registers F H›
proof -
from assms have [simp]: ‹register F› ‹register G›
by (auto simp: equivalent_registers_def)
from assms(1) obtain I where [simp]: ‹iso_register I› and ‹F o I = G›
using equivalent_registers_def by blast
from assms(2) obtain J where [simp]: ‹iso_register J› and ‹G o J = H›
using equivalent_registers_def by blast
have ‹register F›
by (auto simp: equivalent_registers_def)
moreover have ‹iso_register (I o J)›
using ‹iso_register I› ‹iso_register J› iso_register_comp by blast
moreover have ‹F o (I o J) = H›
by (simp add: ‹F ∘ I = G› ‹G ∘ J = H› o_assoc)
ultimately show ?thesis
by (rule equivalent_registersI)
qed

lemma equivalent_registers_assoc[simp]:
assumes [simp]: ‹compatible F G› ‹compatible F H› ‹compatible G H›
shows ‹equivalent_registers (F;(G;H)) ((F;G);H)›
apply (rule equivalent_registersI[where I=assoc])
by auto

lemma equivalent_registers_pair_right:
assumes [simp]: ‹compatible F G›
assumes eq: ‹equivalent_registers G H›
shows ‹equivalent_registers (F;G) (F;H)›
proof -
from eq obtain I where [simp]: ‹iso_register I› and ‹G o I = H›
by (metis equivalent_registers_def)
then have *: ‹(F;G) ∘ (id ⊗⇩r I) = (F;H)›
by (auto intro!: tensor_extensionality register_comp register_preregister register_tensor_is_register
simp:  register_pair_apply iso_register_is_register)
show ?thesis
apply (rule equivalent_registersI[where I=‹id ⊗⇩r I›])
using * by (auto intro!: iso_register_tensor_is_iso_register)
qed

lemma equivalent_registers_pair_left:
assumes [simp]: ‹compatible F G›
assumes eq: ‹equivalent_registers F H›
shows ‹equivalent_registers (F;G) (H;G)›
proof -
from eq obtain I where [simp]: ‹iso_register I› and ‹F o I = H›
by (metis equivalent_registers_def)
then have *: ‹(F;G) ∘ (I ⊗⇩r id) = (H;G)›
by (auto intro!: tensor_extensionality register_comp register_preregister register_tensor_is_register
simp:  register_pair_apply iso_register_is_register)
show ?thesis
apply (rule equivalent_registersI[where I=‹I ⊗⇩r id›])
using * by (auto intro!: iso_register_tensor_is_iso_register)
qed

lemma equivalent_registers_comp:
assumes ‹register H›
assumes ‹equivalent_registers F G›
shows ‹equivalent_registers (H o F) (H o G)›
by (metis (no_types, lifting) assms(1) assms(2) comp_assoc equivalent_registers_def register_comp)

subsection ‹Compatibility simplification›

text ‹The simproc ‹compatibility_warn› produces helpful warnings for subgoals of the form
\<^term>‹compatible x y› that are probably unsolvable due to missing declarations of
variable compatibility facts. Same for subgoals of the form \<^term>‹register x›.›
simproc_setup "compatibility_warn" ("compatible x y" | "register x") = ‹
let val thy_string = Markup.markup (Theory.get_markup \<^theory>) (Context.theory_name \<^theory>)
in
fn m => fn ctxt => fn ct => let
val (x,y) = case Thm.term_of ct of
Const(\<^const_name>‹compatible›,_ ) $x$ y => (x, SOME y)
| Const(\<^const_name>‹register›,_ ) \$ x => (x, NONE)
val str : string lazy = Lazy.lazy (fn () => Syntax.string_of_term ctxt (Thm.term_of ct))
fun w msg = warning (msg ^ "\n(Disable these warnings with: using [[simproc del: "^thy_string^".compatibility_warn]])")
val _ = case (x,y) of
(Free(n,T), SOME (Free(n',T'))) =>
if String.isPrefix ":" n orelse String.isPrefix ":" n' then
w ("Simplification subgoal " ^ Lazy.force str ^ " contains a bound variable.\n" ^
"Try to add some assumptions that makes this goal solvable by the simplifier")
else if n=n' then (if T=T' then ()
else w ("In simplification subgoal " ^ Lazy.force str ^
", variables have same name and different types.\n" ^
"Probably something is wrong."))
else w ("Simplification subgoal " ^ Lazy.force str ^
" occurred but cannot be solved.\n" ^
"›  somewhere.")
| (Free(n,T), NONE) =>
if String.isPrefix ":" n then
w ("Simplification subgoal '" ^ Lazy.force str ^ "' contains a bound variable.\n" ^
"Try to add some assumptions that makes this goal solvable by the simplifier")
else w ("Simplification subgoal " ^ Lazy.force str ^ " occurred but cannot be solved.\n" ^
| _ => ()
in NONE end
end›

named_theorems register_attribute_rule_immediate
named_theorems register_attribute_rule

lemmas [register_attribute_rule] = conjunct1 conjunct2 iso_register_is_register iso_register_is_register[OF iso_register_inv]
lemmas [register_attribute_rule_immediate] = compatible_sym compatible_register1 compatible_register2
asm_rl[of ‹compatible _ _›] asm_rl[of ‹iso_register _›] asm_rl[of ‹register _›] iso_register_inv

text ‹The following declares an attribute ‹[register]›. When the attribute is applied to a fact
of the form \<^term>‹register F›, \<^term>‹iso_register F›, \<^term>‹compatible F G› or a conjunction of these,
then those facts are added to the simplifier together with some derived theorems
(e.g., \<^term>‹compatible F G› also adds \<^term>‹register F›).

In theory ‹Laws_Complement›, support for \<^term>‹is_unit_register F› and \<^term>‹complements F G› is

setup ‹
let
Net.insert_term (K true) (Thm.concl_of thm, thm) results
handle Net.INSERT => results
fun try_rule f thm rule state = case SOME (rule OF [thm]) handle THM _ => NONE  of
NONE => state | SOME th => f th state
fun collect (rules,rules_immediate) thm results =
results |> fold (try_rule add thm) rules_immediate |> fold (try_rule (collect (rules,rules_immediate)) thm) rules
fun declare thm context = let
val ctxt = Context.proof_of context
val rules = Named_Theorems.get ctxt @{named_theorems register_attribute_rule}
val rules_immediate = Named_Theorems.get ctxt @{named_theorems register_attribute_rule_immediate}
val thms = collect (rules,rules_immediate) thm Net.empty |> Net.entries
(* val _ = \<^print> thms *)
in Simplifier.map_ss (fn ctxt => ctxt addsimps thms) context end
in
Attrib.setup \<^binding>‹register›
(Scan.succeed (Thm.declaration_attribute declare))
"Add register-related rules to the simplifier"
end
›

subsection ‹Notation›

no_notation comp_update (infixl "*⇩u" 55)
no_notation tensor_update (infixr "⊗⇩u" 70)

bundle register_notation begin
notation register_tensor (infixr "⊗⇩r" 70)
notation register_pair ("'(_;_')")
end

bundle no_register_notation begin
no_notation register_tensor (infixr "⊗⇩r" 70)
no_notation register_pair ("'(_;_')")
end

end


# Theory Axioms_Complement

section ‹Axioms of complements›

theory Axioms_Complement
imports Laws
begin

typedecl ('a, 'b) complement_domain
instance complement_domain :: (domain, domain) domain..

― ‹We need that there is at least one object in our category. We call is \<^term>‹some_domain›.›
typedecl some_domain
instance some_domain :: domain..

axiomatization where
complement_exists: ‹register F ⟹ ∃G :: ('a, 'b) complement_domain update ⇒ 'b update. compatible F G ∧ iso_register (F;G)› for F :: ‹'a::domain update ⇒ 'b::domain update›

axiomatization where complement_unique: ‹compatible F G ⟹ iso_register (F;G) ⟹ compatible F H ⟹ iso_register (F;H)
⟹ equivalent_registers G H›
for F :: ‹'a::domain update ⇒ 'b::domain update› and G :: ‹'g::domain update ⇒ 'b update› and H :: ‹'h::domain update ⇒ 'b update›

end


# Theory Laws_Complement

section ‹Generic laws about complements›

theory Laws_Complement
imports Laws Axioms_Complement
begin

notation comp_update (infixl "*⇩u" 55)
notation tensor_update (infixr "⊗⇩u" 70)

definition ‹complements F G ⟷ compatible F G ∧ iso_register (F;G)›

lemma complementsI: ‹compatible F G ⟹ iso_register (F;G) ⟹ complements F G›
using complements_def by blast

lemma complements_sym: ‹complements G F› if ‹complements F G›
proof (rule complementsI)
show [simp]: ‹compatible G F›
using compatible_sym complements_def that by blast
from that have ‹iso_register (F;G)›
by (meson complements_def)
then obtain I where [simp]: ‹register I› and ‹(F;G) o I = id› and ‹I o (F;G) = id›
using iso_register_def by blast
have ‹register (swap o I)›
using ‹register I› register_comp register_swap by blast
moreover have ‹(G;F) o (swap o I) = id›
by (simp add: ‹(F;G) ∘ I = id› rewriteL_comp_comp)
moreover have ‹(swap o I) o (G;F) = id›
by (metis (no_types, opaque_lifting) swap_swap ‹I ∘ (F;G) = id› calculation(2) comp_def eq_id_iff)
ultimately show ‹iso_register (G;F)›
using ‹compatible G F› iso_register_def pair_is_register by blast
qed

definition complement :: ‹('a::domain update ⇒ 'b::domain update) ⇒ (('a,'b) complement_domain update ⇒ 'b update)› where
‹complement F = (SOME G :: ('a, 'b) complement_domain update ⇒ 'b update. compatible F G ∧ iso_register (F;G))›

lemma register_complement[simp]: ‹register (complement F)› if ‹register F›
using complement_exists[OF that]
by (metis (no_types, lifting) compatible_def complement_def some_eq_imp)

lemma complement_is_complement:
assumes ‹register F›
shows ‹complements F (complement F)›
using complement_exists[OF assms] unfolding complements_def
by (metis (mono_tags, lifting) complement_def some_eq_imp)

lemma complement_unique:
assumes ‹complements F G›
shows ‹equivalent_registers G (complement F)›
apply (rule complement_unique[where F=F])
using assms unfolding complements_def using compatible_register1 complement_is_complement complements_def by blast+

lemma compatible_complement[simp]: ‹register F ⟹ compatible F (complement F)›
using complement_is_complement complements_def by blast

lemma complements_register_tensor:
assumes [simp]: ‹register F› ‹register G›
shows ‹complements (F ⊗⇩r G) (complement F ⊗⇩r complement G)›
proof (rule complementsI)
have sep4: ‹separating TYPE('z::domain) {(a ⊗⇩u b) ⊗⇩u (c ⊗⇩u d) |a b c d. True}›
apply (rule separating_tensor'[where A=‹{(a ⊗⇩u b) |a b. True}› and B=‹{(c ⊗⇩u d) |c d. True}›])
apply (rule separating_tensor'[where A=UNIV and B=UNIV]) apply auto[3]
apply (rule separating_tensor'[where A=UNIV and B=UNIV]) apply auto[3]
by auto
show compat: ‹compatible (F ⊗⇩r G) (complement F ⊗⇩r complement G)›
by (metis assms(1) assms(2) compatible_register_tensor complement_is_complement complements_def)
let ?reorder = ‹((Fst o Fst; Snd o Fst); (Fst o Snd; Snd o Snd))›
have [simp]: ‹register ?reorder›
by auto
have [simp]: ‹?reorder ((a ⊗⇩u b) ⊗⇩u (c ⊗⇩u d)) = ((a ⊗⇩u c) ⊗⇩u (b ⊗⇩u d))›
for a::‹'t::domain update› and b::‹'u::domain update› and c::‹'v::domain update› and d::‹'w::domain update›
by (simp add: register_pair_apply Fst_def Snd_def tensor_update_mult)
have [simp]: ‹iso_register ?reorder›
apply (rule iso_registerI[of _ ?reorder]) apply auto[2]
apply (rule register_eqI[OF sep4]) apply auto[3]
apply (rule register_eqI[OF sep4]) by auto
have ‹(F ⊗⇩r G; complement F ⊗⇩r complement G) = ((F; complement F) ⊗⇩r (G; complement G)) o ?reorder›
apply (rule register_eqI[OF sep4])
by (auto intro!: register_preregister register_comp register_tensor_is_register pair_is_register
simp: compat register_pair_apply tensor_update_mult)
moreover have ‹iso_register …›
apply (auto intro!: iso_register_comp iso_register_tensor_is_iso_register)
using assms complement_is_complement complements_def by blast+
ultimately show ‹iso_register (F ⊗⇩r G;complement F ⊗⇩r complement G)›
by simp
qed

definition is_unit_register where
‹is_unit_register U ⟷ complements U id›

lemma register_unit_register[simp]: ‹is_unit_register U ⟹ register U›
by (simp add: compatible_def complements_def is_unit_register_def)

lemma unit_register_compatible[simp]: ‹compatible U X› if ‹is_unit_register U› ‹register X›
by (metis compatible_comp_right complements_def id_comp is_unit_register_def that(1) that(2))

lemma unit_register_compatible'[simp]: ‹compatible X U› if ‹is_unit_register U› ‹register X›
using compatible_sym that(1) that(2) unit_register_compatible by blast

lemma compatible_complement_left[simp]: ‹register X ⟹ compatible (complement X) X›
using compatible_sym complement_is_complement complements_def by blast

lemma compatible_complement_right[simp]: ‹register X ⟹ compatible X (complement X)›
using complement_is_complement complements_def by blast

lemma unit_register_pair[simp]: ‹equivalent_registers X (U; X)› if [simp]: ‹is_unit_register U› ‹register X›
proof -
have ‹equivalent_registers id (U; id)›
using complements_def is_unit_register_def iso_register_equivalent_id that(1) by blast
also have ‹equivalent_registers … (U; (X; complement X))›
apply (rule equivalent_registers_pair_right)
apply (auto intro!: unit_register_compatible)
using complement_is_complement complements_def equivalent_registersI id_comp register_id that(2) by blast
also have ‹equivalent_registers … ((U; X); complement X)›
apply (rule equivalent_registers_assoc)
by auto
finally have ‹complements (U; X) (complement X)›
by (auto simp: equivalent_registers_def complements_def)
moreover have ‹equivalent_registers (X; complement X) id›
by (metis complement_is_complement complements_def equivalent_registers_def iso_register_def that)
ultimately show ?thesis
by (meson complement_unique complement_is_complement complements_sym equivalent_registers_sym equivalent_registers_trans that)
qed

lemma unit_register_compose_left:
assumes [simp]: ‹is_unit_register U›
assumes [simp]: ‹register A›
shows ‹is_unit_register (A o U)›
proof -
have ‹compatible (A o U) (A; complement A)›
apply (auto intro!: compatible3')
by (metis assms(1) assms(2) comp_id compatible_comp_inner complements_def is_unit_register_def)
then have compat[simp]: ‹compatible (A o U) id›
by (metis assms(2) compatible_comp_right complement_is_complement complements_def iso_register_def)
have ‹equivalent_registers (A o U; id) (A o U; (A; complement A))›
apply (auto intro!: equivalent_registers_pair_right)
using assms(2) complement_is_complement complements_def equivalent_registers_def id_comp register_id by blast
also have ‹equivalent_registers … ((A o U; A o id); complement A)›
apply auto
by (metis (no_types, opaque_lifting) compat assms(1) assms(2) compatible_comp_left compatible_def compatible_register1 complement_is_complement complements_def equivalent_registers_assoc id_apply register_unit_register)
also have ‹equivalent_registers … (A o (U; id); complement A)›
by (metis (no_types, opaque_lifting) assms(1) assms(2) calculation complements_def equivalent_registers_sym equivalent_registers_trans is_unit_register_def register_comp_pair)
also have ‹equivalent_registers … (A o id; complement A)›
apply (intro equivalent_registers_pair_left equivalent_registers_comp)
apply (auto simp: assms)
using assms(1) equivalent_registers_sym register_id unit_register_pair by blast
also have ‹equivalent_registers … id›
by (metis assms(2) comp_id complement_is_complement complements_def equivalent_registers_def iso_register_inv iso_register_inv_comp2 pair_is_register)
finally show ?thesis
using compat complementsI equivalent_registers_sym is_unit_register_def iso_register_equivalent_id by blast
qed

lemma unit_register_compose_right:
assumes [simp]: ‹is_unit_register U›
assumes [simp]: ‹iso_register A›
shows ‹is_unit_register (U o A)›
proof (unfold is_unit_register_def, rule complementsI)
show ‹compatible (U ∘ A) id›
have 1: ‹iso_register ((U;id) ∘ A ⊗⇩r id)›
by (meson assms(1) assms(2) complements_def is_unit_register_def iso_register_comp iso_register_id iso_register_tensor_is_iso_register)
have 2: ‹id ∘ ((U;id) ∘ A ⊗⇩r id) = (U ∘ A;id)›
by (metis assms(1) assms(2) complements_def fun.map_id is_unit_register_def iso_register_id iso_register_is_register pair_o_tensor)
show ‹iso_register (U ∘ A;id)›
using 1 2 by auto
qed

lemma unit_register_unique:
assumes ‹is_unit_register F›
assumes ‹is_unit_register G›
shows ‹equivalent_registers F G›
proof -
have ‹complements F id› ‹complements G id›
using assms by (metis complements_def equivalent_registers_def id_comp is_unit_register_def)+
then show ?thesis
by (meson complement_unique complements_sym equivalent_registers_sym equivalent_registers_trans)
qed

lemma unit_register_domains_isomorphic:
fixes F :: ‹'a::domain update ⇒ 'c::domain update›
fixes G :: ‹'b::domain update ⇒ 'd::domain update›
assumes ‹is_unit_register F›
assumes ‹is_unit_register G›
shows ‹∃I :: 'a update ⇒ 'b update. iso_register I›
proof -
have ‹is_unit_register ((λd. tensor_update id_update d) o G)›
moreover have ‹is_unit_register ((λc. tensor_update c id_update) o F)›
using assms(1) register_tensor_left unit_register_compose_left by blast
ultimately have ‹equivalent_registers ((λd. tensor_update id_update d) o G) ((λc. tensor_update c id_update) o F)›
using unit_register_unique by blast
then show ?thesis
unfolding equivalent_registers_def by auto
qed

lemma id_complement_is_unit_register[simp]: ‹is_unit_register (complement id)›
by (metis is_unit_register_def complement_is_complement complements_def complements_sym equivalent_registers_def id_comp register_id)

type_synonym unit_register_domain = ‹(some_domain, some_domain) complement_domain›
definition unit_register :: ‹unit_register_domain update ⇒ 'a::domain update› where ‹unit_register = (SOME U. is_unit_register U)›

lemma unit_register_is_unit_register[simp]: ‹is_unit_register (unit_register :: unit_register_domain update ⇒ 'a::domain update)›
proof -
let ?U0 = ‹complement id :: unit_register_domain update ⇒ some_domain update›
let ?U1 = ‹complement id :: ('a, 'a) complement_domain update ⇒ 'a update›
have ‹is_unit_register ?U0› ‹is_unit_register ?U1›
by auto
then obtain I :: ‹unit_register_domain update ⇒ ('a, 'a) complement_domain update› where ‹iso_register I›
apply atomize_elim by (rule unit_register_domains_isomorphic)
with ‹is_unit_register ?U1› have ‹is_unit_register (?U1 o I)›
by (rule unit_register_compose_right)
then show ?thesis
by (metis someI_ex unit_register_def)
qed

lemma unit_register_domain_tensor_unit:
fixes U :: ‹'a::domain update ⇒ _›
assumes ‹is_unit_register U›
shows ‹∃I :: 'b::domain update ⇒ ('a*'b) update. iso_register I›
(* Can we show that I = (λx. tensor_update id_update x) ? It would be nice but I do not see how to prove it. *)
proof -
have ‹equivalent_registers (id :: 'b update ⇒ _) (complement id; id)›
using id_complement_is_unit_register iso_register_equivalent_id register_id unit_register_pair by blast
then obtain J :: ‹'b update ⇒ ((('b, 'b) complement_domain * 'b) update)› where ‹iso_register J›
using equivalent_registers_def iso_register_inv by blast
moreover obtain K :: ‹('b, 'b) complement_domain update ⇒ 'a update› where ‹iso_register K›
using assms id_complement_is_unit_register unit_register_domains_isomorphic by blast
ultimately have ‹iso_register ((K ⊗⇩r id) o J)›
by auto
then show ?thesis
by auto
qed

lemma compatible_complement_pair1:
assumes ‹compatible F G›
shows ‹compatible F (complement (F;G))›
by (metis assms compatible_comp_left compatible_complement_right pair_is_register register_Fst register_pair_Fst)

lemma compatible_complement_pair2:
assumes [simp]: ‹compatible F G›
shows ‹compatible G (complement (F;G))›
proof -
have ‹compatible (F;G) (complement (F;G))›
by simp
then have ‹compatible ((F;G) o Snd) (complement (F;G))›
by auto
then show ?thesis
by (auto simp: register_pair_Snd)
qed

lemma equivalent_complements:
assumes ‹complements F G›
assumes ‹equivalent_registers G G'›
shows ‹complements F G'›
apply (rule complementsI)
apply (metis assms(1) assms(2) compatible_comp_right complements_def equivalent_registers_def iso_register_is_register)
by (metis assms(1) assms(2) complements_def equivalent_registers_def equivalent_registers_pair_right iso_register_comp)

lemma complements_complement_pair:
assumes [simp]: ‹compatible F G›
shows ‹complements F (G; complement (F;G))›
proof (rule complementsI)
have ‹equivalent_registers (F; (G; complement (F;G))) ((F;G); complement (F;G))›
apply (rule equivalent_registers_assoc)
by (auto simp add: compatible_complement_pair1 compatible_complement_pair2)
also have ‹equivalent_registers … id›
by (meson assms complement_is_complement complements_def equivalent_registers_sym iso_register_equivalent_id pair_is_register)
finally show ‹iso_register (F;(G;complement (F;G)))›
using equivalent_registers_sym iso_register_equivalent_id by blast
show ‹compatible F (G;complement (F;G))›
using assms compatible3' compatible_complement_pair1 compatible_complement_pair2 by blast
qed

lemma equivalent_registers_complement:
assumes ‹equivalent_registers F G›
shows ‹equivalent_registers (complement F) (complement G)›
proof -
have ‹complements F (complement F)›
using assms complement_is_complement equivalent_registers_register_left by blast
with assms have ‹complements G (complement F)›
by (meson complements_sym equivalent_complements)
then show ?thesis
by (rule complement_unique)
qed

lemma complements_complement_pair':
assumes [simp]: ‹compatible F G›
shows ‹complements G (F; complement (F;G))›
proof -
have ‹equivalent_registers (F;G) (G;F)›
apply (rule equivalent_registersI[where I=swap])
by auto
then have ‹equivalent_registers (complement (F;G)) (complement (G;F))›
by (rule equivalent_registers_complement)
then have ‹equivalent_registers (F; (complement (F;G))) (F; (complement (G;F)))›
apply (rule equivalent_registers_pair_right[rotated])
using assms compatible_complement_pair1 by blast
moreover have ‹complements G (F; complement (G;F))›
apply (rule complements_complement_pair)
using assms compatible_sym by blast
ultimately show ?thesis
by (meson equivalent_complements equivalent_registers_sym)
qed

lemma complements_chain:
assumes [simp]: ‹register F› ‹register G›
shows ‹complements (F o G) (complement F; F o complement G)›
proof (rule complementsI)
show ‹compatible (F o G) (complement F; F o complement G)›
by auto
have ‹equivalent_registers (F ∘ G;(complement F;F ∘ complement G)) (F ∘ G;(F ∘ complement G;complement F))›
apply (rule equivalent_registersI[where I=‹id ⊗⇩r swap›])
by (auto intro!: iso_register_tensor_is_iso_register simp: pair_o_tensor)
also have ‹equivalent_registers … ((F ∘ G;F ∘ complement G);complement F)›
apply (rule equivalent_registersI[where I=assoc])
by (auto intro!: iso_register_tensor_is_iso_register simp: pair_o_tensor)
also have ‹equivalent_registers … (F o (G; complement G);complement F)›
by (metis (no_types, lifting) assms(1) assms(2) calculation compatible_complement_right
equivalent_registers_sym equivalent_registers_trans register_comp_pair)
also have ‹equivalent_registers … (F o id;complement F)›
apply (rule equivalent_registers_pair_left, simp)
apply (rule equivalent_registers_comp, simp)
by (metis assms(2) complement_is_complement complements_def equivalent_registers_def iso_register_def)
also have ‹equivalent_registers … id›
by (metis assms(1) comp_id complement_is_complement complements_def equivalent_registers_def iso_register_def)
finally show ‹iso_register (F ∘ G;(complement F;F ∘ complement G))›
using equivalent_registers_sym iso_register_equivalent_id by blast
qed

lemma complements_Fst_Snd[simp]: ‹complements Fst Snd›
by (auto intro!: complementsI simp: pair_Fst_Snd)

lemma complements_Snd_Fst[simp]: ‹complements Snd Fst›
by (auto intro!: complementsI simp flip: swap_def)

lemma compatible_unit_register[simp]: ‹register F ⟹ compatible F unit_register›
using compatible_sym unit_register_compatible unit_register_is_unit_register by blast

lemma complements_id_unit_register[simp]: ‹complements id unit_register›
using complements_sym is_unit_register_def unit_register_is_unit_register by blast

lemma complements_iso_unit_register: ‹iso_register I ⟹ is_unit_register U ⟹ complements I U›
using complements_sym equivalent_complements is_unit_register_def iso_register_equivalent_id by blast

lemma iso_register_complement_is_unit_register[simp]:
assumes ‹iso_register F›
shows ‹is_unit_register (complement F)›
by (meson assms complement_is_complement complements_sym equivalent_complements equivalent_registers_sym is_unit_register_def iso_register_equivalent_id iso_register_is_register)

text ‹Adding support for \<^term>‹is_unit_register F› and \<^term>‹complements F G› to the [@{attribute register}] attribute›
lemmas [register_attribute_rule] = is_unit_register_def[THEN iffD1] complements_def[THEN iffD1]
lemmas [register_attribute_rule_immediate] = asm_rl[of ‹is_unit_register _›]

no_notation comp_update (infixl "*⇩u" 55)
no_notation tensor_update (infixr "⊗⇩u" 70)

end


# Theory Axioms_Classical

section ‹Classical instantiation of registerss›

(* AXIOM INSTANTIATION (use instantiate_laws.py to generate Laws_Classical.thy)

domain → type
comp_update → map_comp
id_update → Some

*)

theory Axioms_Classical
imports Main
begin

type_synonym 'a update = ‹'a ⇀ 'a›

lemma id_update_left: "Some ∘⇩m a = a"
by (auto intro!: ext simp add: map_comp_def option.case_eq_if)
lemma id_update_right: "a ∘⇩m Some = a"
by auto

lemma comp_update_assoc: "(a ∘⇩m b) ∘⇩m c = a ∘⇩m (b ∘⇩m c)"
by (auto intro!: ext simp add: map_comp_def option.case_eq_if)

type_synonym ('a,'b) preregister = ‹'a update ⇒ 'b update›
definition preregister :: ‹('a,'b) preregister ⇒ bool› where
‹preregister F ⟷ (∃g s. ∀a m. F a m = (case a (g m) of None ⇒ None | Some x ⇒ s x m))›

lemma id_preregister: ‹preregister id›
unfolding preregister_def
apply (rule exI[of _ ‹λm. m›])
apply (rule exI[of _ ‹λa m. Some a›])

lemma preregister_mult_right: ‹preregister (λa. a ∘⇩m z)›
unfolding preregister_def
apply (rule exI[of _ ‹λm. the (z m)›])
apply (rule exI[of _ ‹λx m. case z m of None ⇒ None | _ ⇒ Some x›])

lemma preregister_mult_left: ‹preregister (λa. z ∘⇩m a)›
unfolding preregister_def
apply (rule exI[of _ ‹λm. m›])
apply (rule exI[of _ ‹λx m. z x›])

lemma comp_preregister: "preregister (G ∘ F)" if "preregister F" and ‹preregister G›
proof -
from ‹preregister F›
obtain sF gF where F: ‹F a m = (case a (gF m) of None ⇒ None | Some x ⇒ sF x m)› for a m
using preregister_def by blast
from ‹preregister G›
obtain sG gG where G: ‹G a m = (case a (gG m) of None ⇒ None | Some x ⇒ sG x m)› for a m
using preregister_def by blast
define s g where ‹s a m = (case sF a (gG m) of None ⇒ None | Some x ⇒ sG x m)›
and ‹g m = gF (gG m)› for a m
have ‹(G ∘ F) a m = (case a (g m) of None ⇒ None | Some x ⇒ s x m)› for a m
unfolding F G s_def g_def
then show "preregister (G ∘ F)"
using preregister_def by blast
qed

definition tensor_update :: ‹'a update ⇒ 'b update ⇒ ('a×'b) update› where
‹tensor_update a b m = (case a (fst m) of None ⇒ None | Some x ⇒ (case b (snd m) of None ⇒ None | Some y ⇒ Some (x,y)))›

lemma tensor_update_mult: ‹tensor_update a c ∘⇩m tensor_update b d = tensor_update (a ∘⇩m b) (c ∘⇩m d)›
by (auto intro!: ext simp add: map_comp_def option.case_eq_if tensor_update_def)

definition update1 :: ‹'a ⇒ 'a ⇒ 'a update› where
‹update1 x y m = (if m=x then Some y else None)›

lemma update1_extensionality:
assumes ‹preregister F›
assumes ‹preregister G›
assumes FGeq: ‹⋀x y. F (update1 x y) = G (update1 x y)›
shows "F = G"
proof (rule ccontr)
assume neq: ‹F ≠ G›
then obtain z m where neq': ‹F z m ≠ G z m›
apply atomize_elim by auto
obtain gF sF where gsF: ‹F z m = (case z (gF m) of None ⇒ None | Some x ⇒ sF x m)› for z m
using ‹preregister F› preregister_def by blast
obtain gG sG where gsG: ‹G z m = (case z (gG m) of None ⇒ None | Some x ⇒ sG x m)› for z m
using ‹preregister G› preregister_def by blast
consider (abeq) x where ‹z (gF m) = Some x› ‹z (gG m) = Some x› ‹gF m = gG m›
| (abnone) ‹z (gG m) = None› ‹z (gF m) = None›
| (neqF) x where ‹gF m ≠ gG m› ‹F z m = Some x›
| (neqG) y where ‹gF m ≠ gG m› ‹G z m = Some y›
| (neqNone) ‹gF m ≠ gG m› ‹F z m = None› ‹G z m = None›
apply atomize_elim by (metis option.exhaust_sel)
then show False
proof cases
case (abeq x)
then have ‹F z m = sF x m› and ‹G z m = sG x m›
moreover have ‹F (update1 (gF m) x) m = sF x m›
moreover have ‹G (update1 (gF m) x) m = sG x m›
by (simp add: abeq gsG update1_def)
ultimately show False
using FGeq neq' by force
next
case abnone
then show False
using gsF gsG neq' by force
next
case neqF
moreover
have ‹F (update1 (gF m) (the (z (gF m)))) m = F z m›
by (metis gsF neqF(2) option.case_eq_if option.simps(3) option.simps(5) update1_def)
moreover have ‹G (update1 (gF m) (the (z (gF m)))) m = None›
by (metis gsG neqF(1) option.case_eq_if update1_def)
ultimately show False
using FGeq by force
next
case neqG
moreover
have ‹G (update1 (gG m) (the (z (gG m)))) m = G z m›
by (metis gsG neqG(2) option.case_eq_if option.distinct(1) option.simps(5) update1_def)
moreover have ‹F (update1 (gG m) (the (z (gG m)))) m = None›
by (simp add: gsF neqG(1) update1_def)
ultimately show False
using FGeq by force
next
case neqNone
with neq' show False
by fastforce
qed
qed

lemma tensor_extensionality:
assumes ‹preregister F›
assumes ‹preregister G›
assumes FGeq: ‹⋀a b. F (tensor_update a b) = G (tensor_update a b)›
shows "F = G"
proof -
have ‹F (update1 x y) = G (update1 x y)› for x y
using FGeq[of ‹update1 (fst x) (fst y)› ‹update1 (snd x) (snd y)›]
apply (auto intro!:ext simp: tensor_update_def[abs_def] update1_def[abs_def])
by (smt (z3) assms(1) assms(2) option.case(2) option.case_eq_if preregister_def prod.collapse)
with assms(1,2) show "F = G"
by (rule update1_extensionality)
qed

definition "valid_getter_setter g s ⟷
(∀b. b = s (g b) b) ∧ (∀a b. g (s a b) = a) ∧ (∀a a' b. s a (s a' b) = s a b)"

definition ‹register_from_getter_setter g s a m = (case a (g m) of None ⇒ None | Some x ⇒ Some (s x m))›
definition ‹register_apply F a = the o F (Some o a)›
definition ‹setter F a m = register_apply F (λ_. a) m› for F :: ‹'a update ⇒ 'b update›
definition ‹getter F m = (THE x. setter F x m = m)› for F :: ‹'a update ⇒ 'b update›

lemma
assumes ‹valid_getter_setter g s›
shows getter_of_register_from_getter_setter[simp]: ‹getter (register_from_getter_setter g s) = g›
and setter_of_register_from_getter_setter[simp]: ‹setter (register_from_getter_setter g s) = s›
proof -
define g' s' where ‹g' = getter (register_from_getter_setter g s)›
and ‹s' = setter (register_from_getter_setter g s)›
show ‹s' = s›
by (auto intro!:ext simp: s'_def setter_def register_apply_def register_from_getter_setter_def)
moreover show ‹g' = g›
proof (rule ext, rename_tac m)
fix m
have ‹g' m = (THE x. s x m = m)›
by (auto intro!:ext simp: g'_def s'_def[symmetric] ‹s'=s› getter_def register_apply_def register_from_getter_setter_def)
moreover have ‹s (g m) m = m›
by (metis assms valid_getter_setter_def)
moreover have ‹x = x'› if ‹s x m = m› ‹s x' m = m› for x x'
by (metis assms that(1) that(2) valid_getter_setter_def)
ultimately show ‹g' m = g m›
qed
qed

definition register :: ‹('a,'b) preregister ⇒ bool› where
‹register F ⟷ (∃g s. F = register_from_getter_setter g s ∧ valid_getter_setter g s)›

lemma register_of_id: ‹register F ⟹ F Some = Some›
by (auto simp add: register_def valid_getter_setter_def register_from_getter_setter_def)

lemma register_id: ‹register id›
unfolding register_def
apply (rule exI[of _ id], rule exI[of _ ‹λa m. a›])
by (auto intro!: ext simp: option.case_eq_if register_from_getter_setter_def valid_getter_setter_def)

lemma register_tensor_left: ‹register (λa. tensor_update a Some)›
apply (auto simp: register_def)
apply (rule exI[of _ fst])
apply (rule exI[of _ ‹λx' (x,y). (x',y)›])
by (auto intro!: ext simp add: tensor_update_def valid_getter_setter_def register_from_getter_setter_def option.case_eq_if)

lemma register_tensor_right: ‹register (λa. tensor_update Some a)›
apply (auto simp: register_def)
apply (rule exI[of _ snd])
apply (rule exI[of _ ‹λy' (x,y). (x,y')›])
by (auto intro!: ext simp add: tensor_update_def valid_getter_setter_def register_from_getter_setter_def option.case_eq_if)

lemma register_preregister: "preregister F" if ‹register F›
proof -
from ‹register F›
obtain s g where F: ‹F a m = (case a (g m) of None ⇒ None | Some x ⇒ Some (s x m))› for a m
unfolding register_from_getter_setter_def register_def by blast
show ?thesis
unfolding preregister_def
apply (rule exI[of _ g])
apply (rule exI[of _ ‹λx m. Some (s x m)›])
using F by simp
qed

lemma register_comp: "register (G ∘ F)" if ‹register F› and ‹register G›
for F :: "('a,'b) preregister" and G :: "('b,'c) preregister"
proof -
from ‹register F›
obtain sF gF where F: ‹F a m = (case a (gF m) of None ⇒ None | Some x ⇒ Some (sF x m))›
and validF: ‹valid_getter_setter gF sF› for a m
unfolding register_def register_from_getter_setter_def by blast
from ‹register G›
obtain sG gG where G: ‹G a m = (case a (gG m) of None ⇒ None | Some x ⇒ Some (sG x m))›
and validG: ‹valid_getter_setter gG sG› for a m
unfolding register_def register_from_getter_setter_def by blast
define s g where ‹s a m = sG (sF a (gG m)) m› and ‹g m = gF (gG m)› for a m
have ‹(G ∘ F) a m = (case a (g m) of None ⇒ None | Some x ⇒ Some (s x m))› for a m
by (auto simp add: option.case_eq_if F G s_def g_def)
moreover have ‹valid_getter_setter g s›
using validF validG by (auto simp: valid_getter_setter_def s_def g_def)
ultimately show "register (G ∘ F)"
unfolding register_def register_from_getter_setter_def by blast
qed

lemma register_mult: "register F ⟹ F a ∘⇩m F b = F (a ∘⇩m b)"
by (auto intro!: ext simp: register_def register_from_getter_setter_def[abs_def] valid_getter_setter_def map_comp_def option.case_eq_if)

definition register_pair ::
‹('a update ⇒ 'c update) ⇒ ('b update ⇒ 'c update) ⇒ (('a×'b) update ⇒ 'c update)› where
‹register_pair F G =
register_from_getter_setter (λm. (getter F m, getter G m)) (λ(a