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_notation
no_notation m_inv ("invı _" [81] 80)

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

lemma preregister_mult_right: clinear (λa. a oCL z)
  by (simp add: bounded_cbilinear.add_left bounded_cbilinear_cblinfun_compose clinearI)
lemma preregister_mult_left: clinear (λa. z oCL 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 oCL b) = F a oCL 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 oCL G b = G b oCL F a) then 
                        tensor_lift (λa b. F a oCL G b) else (λ_. 0))

lemma cbilinear_F_comp_G[simp]: clinear F  clinear G  cbilinear (λa b. F a oCL 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 oCL G b = G b oCL F a
  shows (register_pair F G) (tensor_op a b) = F a oCL 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 oCL G b = G b oCL 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 oCL 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 oCL 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 oCL 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 oCL 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 oCL y) = F x oCL F y for x y
    by (simp add: register_mult)
  have [simp]: G (x oCL y) = G x oCL 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 oCL b) = register_pair F G a oCL 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