Theory Laws_Quantum

(*
 * This is an autogenerated file. Do not edit.
 * The original is Laws.thy. It was converted using instantiate_laws.py.
 *)

section ‹Generic laws about registers, instantiated quantumly›

theory Laws_Quantum
  imports Axioms_Quantum
begin

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

subsection ‹Elementary facts›

declare complex_vector.linear_id[simp]
declare cblinfun_compose_id_left[simp]
declare cblinfun_compose_id_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]: clinear (λb::'b::finite update. tensor_op a b)
  for a :: 'a::finite update
proof -
  have clinear ((λb1::('a×'b) update. (a u id_cblinfun) *u b1) o (λb. tensor_op id_cblinfun b))
    by (rule clinear_compose; simp)
  then show ?thesis
    by (simp add: o_def comp_tensor_op)
qed

lemma preregister_tensor_right[simp]: clinear (λa::'a::finite update. tensor_op a b)  
  for b :: 'b::finite update
proof -
  have clinear ((λa1::('a×'b) update. (id_cblinfun u b) *u a1) o (λa. tensor_op a id_cblinfun))
    by (rule clinear_compose, simp_all)
  then show ?thesis
    by (simp add: o_def comp_tensor_op)
qed

subsection ‹Registers›

lemma id_update_tensor_register[simp]:
  assumes register F
  shows register (λa::'a::finite update. id_cblinfun 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::finite update. F a u id_cblinfun)
  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_op (F a) id_cblinfun) (λb. tensor_op id_cblinfun (G b))"

lemma register_tensor_is_register: 
  fixes F :: "'a::finite update  'b::finite update" and G :: "'c::finite update  'd::finite update"
  shows "register F  register G  register (F r G)"
  unfolding register_tensor_def
  apply (rule register_pair_is_register)
  by (simp_all add: comp_tensor_op)

lemma register_tensor_apply[simp]:
  fixes F :: "'a::finite update  'b::finite update" and G :: "'c::finite update  'd::finite 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 comp_tensor_op)

definition "separating (_::'b::finite itself) A  
  (F G :: 'a::finite update  'b update. clinear F  clinear G  (xA. 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::finite) A  separating TYPE('a) B
  unfolding separating_def by (meson in_mono) 

lemma register_eqI: separating TYPE('b::finite) A  clinear F  clinear G  (x. xA  F x = G x)  F = (G::_  'b update)
  unfolding separating_def by auto

lemma separating_tensor:
  fixes A :: 'a::finite update set and B :: 'b::finite update set
  assumes [simp]: separating TYPE('c::finite) A
  assumes [simp]: separating TYPE('c) B
  shows separating TYPE('c) {a u b | a b. aA  bB}
proof (unfold separating_def, intro allI impI)
  fix F G :: ('a×'b) update  'c update
  assume [simp]: clinear F clinear G
  have [simp]: clinear (λx. F (a u x)) for a
    using _ clinear F apply (rule clinear_compose[unfolded o_def])
    by simp
  have [simp]: clinear (λx. G (a u x)) for a
    using _ clinear G apply (rule clinear_compose[unfolded o_def])
    by simp
  have [simp]: clinear (λx. F (x u b)) for b
    using _ clinear F apply (rule clinear_compose[unfolded o_def])
    by simp
  have [simp]: clinear (λx. G (x u b)) for b
    using _ clinear G apply (rule clinear_compose[unfolded o_def])
    by simp

  assume x{a u b |a b. aA  bB}. 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::finite update set and B :: 'b::finite update set
  assumes separating TYPE('c::finite) A
  assumes separating TYPE('c) B
  assumes C = {a u b | a b. aA  bB}
  shows separating TYPE('c) C
  using assms
  by (simp add: separating_tensor)

lemma tensor_extensionality3: 
  fixes F G :: ('a::finite×'b::finite×'c::finite) update  'd::finite 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={aubuc| 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={buc| b c. True}])
    by auto
  show clinear F clinear 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::finite×'b::finite)×'c::finite) update  'd::finite 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={(aub)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={aub| a b. True}])
    by auto
  show clinear F clinear 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::finite update  'c::finite update)
                        ('b::finite 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 clinear_compose)

lemma compatible_tensor_id_update_left[simp]:
  fixes F :: "'a::finite update  'c::finite update" and G :: "'b::finite update  'c::finite update"
  assumes "compatible F G"
  shows "compatible (λa. id_cblinfun u F a) (λa. id_cblinfun 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::finite update  'c::finite update" and G :: "'b::finite update  'c::finite update"
  assumes "compatible F G"
  shows "compatible (λa. F a u id_cblinfun) (λa. G a u id_cblinfun)"
  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_cblinfun) (λa. id_cblinfun u G a)"
  apply (rule compatibleI)
  using assms by (auto simp: comp_tensor_op)

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

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 clinear (F  G;F  H) and clinear (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 comp_tensor_op)
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 cblinfun_compose_assoc compatible_def)

lemmas compatible_ac_rules = swap_registers cblinfun_compose_assoc[symmetric] swap_registers_right

subsection ‹Fst and Snd›

definition Fst where Fst a = a u id_cblinfun
definition Snd where Snd a = id_cblinfun 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 comp_tensor_op)

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_Quantum.register_pair_apply Fst_def Snd_def comp_tensor_op) 

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 comp_tensor_op)

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 comp_tensor_op)

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 comp_tensor_op)


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]: clinear F clinear G clinear H
    using register_preregister by blast+
  have [simp]: clinear (λa. (F;G) a *u z) for z
    apply (rule clinear_compose[unfolded o_def, of (F;G)])
    by simp_all
  have [simp]: clinear (λa. z *u (F;G) a) for z
    apply (rule clinear_compose[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 cblinfun_compose_assoc)
    also have  = H h *u (F; G) (f u g)
      using compatible F G by (subst register_pair_apply, auto simp: cblinfun_compose_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]: "clinear A" "clinear B"
     apply (metis (no_types, opaque_lifting) assms compatible_register1 register_preregister)
    by (metis (full_types) assms compatible_register2 register_preregister)
  then show clinear ((A; B)  swap)
    by simp
  show clinear (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::finite update  'e::finite update and G :: 'b::finite update  'f::finite update
    and F' :: 'c::finite update  'e update and G' :: 'd::finite update  'f update
  assumes [simp]: compatible F F'
  assumes [simp]: compatible G G'
  shows compatible (F r G) (F' r G')
proof -
  note [intro!] = 
    clinear_compose[OF _ preregister_mult_right, unfolded o_def]
    clinear_compose[OF _ preregister_mult_left, unfolded o_def]
    clinear_compose
    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]: clinear 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 comp_tensor_op)
  define Φ where Φ c d = ((F;F') r (G;G')) o reorder o (λσ. σ u (c u d)) for c d
  have [simp]: clinear (Φ 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 comp_tensor_op)
  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 comp_tensor_op)
  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::finite×'b::finite)×'c::finite) update  ('a×('b×'c)) update where 
  assoc = ((Fst; Snd o Fst); Snd o Snd)

lemma assoc_is_hom[simp]: clinear 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 comp_tensor_op)

definition assoc' :: ('a×('b×'c)) update  (('a::finite×'b::finite)×'c::finite) update where 
  assoc' = (Fst o Fst; (Fst o Snd; Snd))

lemma assoc'_is_hom[simp]: clinear 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 comp_tensor_op)

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 cblinfun_compose_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 cblinfun_compose_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 :: _::finite update  _::finite 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 :: _::finite update  _::finite 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
   termcompatible x y that are probably unsolvable due to missing declarations of 
   variable compatibility facts. Same for subgoals of the form termregister x.›
simproc_setup "compatibility_warn" ("compatible x y" | "register x") = let val thy_string = Markup.markup (Theory.get_markup theory) (Context.theory_base_name theory)
in
fn m => fn ctxt => fn ct => let
  val (x,y) = case Thm.term_of ct of
                 Const(const_namecompatible,_ ) $ x $ y => (x, SOME y)
               | Const(const_nameregister,_ ) $ 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 termregister F, termiso_register F, termcompatible F G or a conjunction of these,
  then those facts are added to the simplifier together with some derived theorems
  (e.g., termcompatible F G also adds termregister F).

  In theory Laws_Complement›, support for termis_unit_register F and termcomplements 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 bindingregister
 (Scan.succeed (Thm.declaration_attribute declare))
  "Add register-related rules to the simplifier"
end

subsection ‹Notation›

no_notation cblinfun_compose (infixl "*u" 55)
no_notation tensor_op (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