Session Registers

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
    by (simp add: o_def tensor_update_mult)
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
    by (simp add: o_def tensor_update_mult)
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)
  by (simp_all add: tensor_update_mult)

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 
  by (simp_all add: assms tensor_update_mult)

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
  by (simp add: separating_tensor)

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)
  by (auto simp add: register_tensor_is_register)

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"
  by (simp add: compatible_def)

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"
  by (simp add: compatible_def)

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

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›
  by (simp add: compatible_def)
lemma compatible_register2: ‹compatible F G ⟹ register G›
  by (simp add: compatible_def)

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›
  by (simp add: swap_def)

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›
  by (simp add: pointfree_idE)

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')›
    by (auto simp add: register_tensor_def)
  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
    apply (simp add: reorder_def register_pair_apply)
    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›
  by (simp add: pointfree_idE)

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

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

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›
  by (simp add: inv_equality)

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›
  by (simp add: iso_register_def)

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›
  by (simp add: equivalent_registers_def)

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" ^
                            "Please add assumption/fact  [simp]: ‹" ^ Lazy.force str ^ 
                            "›  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" ^
                    "Please add assumption/fact  [simp]: ‹" ^ Lazy.force str ^ "›  somewhere.")
      | _ => ()
  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
  added to this attribute.›

setup ‹
let
fun add thm results = 
  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›
    by (simp add: iso_register_is_register)
  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)›
    by (simp add: assms(2) unit_register_compose_left)
  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

   Generic laws about registers → Generic laws about registers, instantiated classically
*)

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›])
  by (simp add: option.case_eq_if)

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›])
  by (auto simp add: option.case_eq_if)

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›])
  by (auto simp add: option.case_eq_if)

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
    by (auto simp add: option.case_eq_if)
  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›
      by (simp_all add: gsF gsG)
    moreover have ‹F (update1 (gF m) x) m = sF x m›
      by (simp add: gsF update1_def)
    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›
      by (simp add: Uniq_def the1_equality')
  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