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
    Generic laws about registers → Generic laws about registers, instantiated quantumly
    Generic laws about complements → Generic laws about complements, instantiated quantumly
*)

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


unbundle cblinfun_syntax
unbundle no m_inv_syntax

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

lemma preregister_mult_right: ‹clinear (λa. a o⇩C⇩L z)›
  by (simp add: bounded_cbilinear.add_left bounded_cbilinear_cblinfun_compose clinearI)
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›
  by (simp add: register_def)

lemma register_id: ‹register id›
  by (simp add: register_def complex_vector.module_hom_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)›
  by (simp add: comp_tensor_op register_def tensor_op_cbilinear tensor_op_adjoint)

lemma register_tensor_right: ‹register (λa. tensor_op id_cblinfun a)›
  by (simp add: comp_tensor_op register_def tensor_op_cbilinear tensor_op_adjoint)

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
  by (auto simp add: clinear_iff bounded_cbilinear.add_left bounded_cbilinear_cblinfun_compose bounded_cbilinear.add_right)

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›])
    by (simp_all add: preregister_mult_left bounded_cbilinear.add_right clinearI)
  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›])
    by (simp_all add: preregister_mult_left bounded_cbilinear.add_right clinearI)
  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›])
    by (simp_all add: bounded_cbilinear.add_left bounded_cbilinear_cblinfun_compose clinearI)
  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›])
    by (simp_all add: bounded_cbilinear.add_left bounded_cbilinear_cblinfun_compose clinearI)
  have [simp]: ‹F (x o⇩C⇩L y) = F x o⇩C⇩L F y› for x y
    by (simp add: register_mult)
  have [simp]: ‹G (x o⇩C⇩L y) = G x o⇩C⇩L G y› for x y
    by (simp add: register_mult)
  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])
    by (simp_all add: tensor_op_adjoint register_pair_apply assms(3))
  then show ‹register_pair F G (a*) = register_pair F G a*›
    by (metis double_adj)
qed

end