# Theory Axioms_Quantum

```section ‹Quantum instantiation of registers›

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

# Type classes
domain → finite

# Types
some_domain → unit

# Constants
comp_update → cblinfun_compose
id_update → id_cblinfun
preregister → clinear
tensor_update → tensor_op

# Lemmas
id_update_left → cblinfun_compose_id_left
id_update_right → cblinfun_compose_id_right
comp_update_assoc → cblinfun_compose_assoc
id_preregister → complex_vector.linear_id
comp_preregister → clinear_compose
tensor_update_mult → comp_tensor_op
# preregister_tensor_left → clinear_tensor_right
# preregister_tensor_right → clinear_tensor_left

# Chapter name
*)

theory Axioms_Quantum
imports Jordan_Normal_Form.Matrix_Impl "HOL-Library.Rewrite"
Complex_Bounded_Operators.Complex_L2
Finite_Tensor_Product
begin

unbundle cblinfun_notation
no_notation m_inv ("invı _" [81] 80)

type_synonym 'a update = ‹('a ell2, 'a ell2) cblinfun›

lemma preregister_mult_right: ‹clinear (λa. a o⇩C⇩L z)›
lemma preregister_mult_left: ‹clinear (λa. z o⇩C⇩L a)›
by (meson cbilinear_cblinfun_compose cbilinear_def)

definition register :: ‹('a::finite update ⇒ 'b::finite update) ⇒ bool› where
"register F ⟷
clinear F
∧ F id_cblinfun = id_cblinfun
∧ (∀a b. F(a o⇩C⇩L b) = F a o⇩C⇩L F b)
∧ (∀a. F (a*) = (F a)*)"

lemma register_of_id: ‹register F ⟹ F id_cblinfun = id_cblinfun›

lemma register_id: ‹register id›

lemma register_preregister: "register F ⟹ clinear F"
unfolding register_def by simp

lemma register_comp: "register F ⟹ register G ⟹ register (G ∘ F)"
unfolding register_def
apply auto
using clinear_compose by blast

lemma register_mult: "register F ⟹ cblinfun_compose (F a) (F b) = F (cblinfun_compose a b)"
unfolding register_def
by auto

lemma register_tensor_left: ‹register (λa. tensor_op a id_cblinfun)›

lemma register_tensor_right: ‹register (λa. tensor_op id_cblinfun a)›

definition register_pair ::
‹('a::finite update ⇒ 'c::finite update) ⇒ ('b::finite update ⇒ 'c update)
⇒ (('a×'b) update ⇒ 'c update)› where
‹register_pair F G = (if register F ∧ register G ∧ (∀a b. F a o⇩C⇩L G b = G b o⇩C⇩L F a) then
tensor_lift (λa b. F a o⇩C⇩L G b) else (λ_. 0))›

lemma cbilinear_F_comp_G[simp]: ‹clinear F ⟹ clinear G ⟹ cbilinear (λa b. F a o⇩C⇩L G b)›
unfolding cbilinear_def

lemma register_pair_apply:
assumes [simp]: ‹register F› ‹register G›
assumes ‹⋀a b. F a o⇩C⇩L G b = G b o⇩C⇩L F a›
shows ‹(register_pair F G) (tensor_op a b) = F a o⇩C⇩L G b›
unfolding register_pair_def
apply (simp flip: assms(3))
by (metis assms(1) assms(2) cbilinear_F_comp_G register_preregister tensor_lift_correct)

lemma register_pair_is_register:
fixes F :: ‹'a::finite update ⇒ 'c::finite update› and G
assumes [simp]: ‹register F› and [simp]: ‹register G›
assumes ‹⋀a b. F a o⇩C⇩L G b = G b o⇩C⇩L F a›
shows ‹register (register_pair F G)›
proof (unfold register_def, intro conjI allI)
have [simp]: ‹clinear F› ‹clinear G›
using assms register_def by blast+
have [simp]: ‹F id_cblinfun = id_cblinfun› ‹G id_cblinfun = id_cblinfun›
using assms(1,2) register_def by blast+
show [simp]: ‹clinear (register_pair F G)›
unfolding register_pair_def
using assms apply auto
apply (rule tensor_lift_clinear)
by (simp flip: assms(3))
show ‹register_pair F G id_cblinfun = id_cblinfun›
apply (simp flip: tensor_id)
apply (subst register_pair_apply)
using assms by simp_all
have [simp]: ‹clinear (λy. register_pair F G (x o⇩C⇩L y))› for x :: ‹('a×'b) update›
apply (rule clinear_compose[unfolded o_def, where g=‹register_pair F G›])
have [simp]: ‹clinear (λy. x o⇩C⇩L register_pair F G y)› for x :: ‹'c update›
apply (rule clinear_compose[unfolded o_def, where f=‹register_pair F G›])
have [simp]: ‹clinear (λx. register_pair F G (x o⇩C⇩L y))› for y :: ‹('a×'b) update›
apply (rule clinear_compose[unfolded o_def, where g=‹register_pair F G›])
have [simp]: ‹clinear (λx. register_pair F G x o⇩C⇩L y)› for y :: ‹'c update›
apply (rule clinear_compose[unfolded o_def, where f=‹register_pair F G›])
have [simp]: ‹F (x o⇩C⇩L y) = F x o⇩C⇩L F y› for x y
have [simp]: ‹G (x o⇩C⇩L y) = G x o⇩C⇩L G y› for x y
have [simp]: ‹clinear (λa. (register_pair F G (a*))*)›
apply (rule antilinear_o_antilinear[unfolded o_def, where f=‹adj›])
apply simp
apply (rule antilinear_o_clinear[unfolded o_def, where g=‹adj›])
by (simp_all)
have [simp]: ‹F (a*) = (F a)*› for a
using assms(1) register_def by blast
have [simp]: ‹G (b*) = (G b)*› for b
using assms(2) register_def by blast

fix a b
show ‹register_pair F G (a o⇩C⇩L b) = register_pair F G a o⇩C⇩L register_pair F G b›
apply (rule tensor_extensionality[THEN fun_cong, where x=b], simp_all)
apply (rule tensor_extensionality[THEN fun_cong, where x=a], simp_all)
apply (simp_all add: comp_tensor_op register_pair_apply assms(3))
using assms(3)
by (metis cblinfun_compose_assoc)
have ‹(register_pair F G (a*))* = register_pair F G a›
apply (rule tensor_extensionality[THEN fun_cong, where x=a])