Theory Quantum_Teleportation

(* 
Authors: 

  Anthony Bordg, University of Cambridge, apdb3@cam.ac.uk;
  Yijun He, University of Cambridge, yh403@cam.ac.uk
*)

section ‹Quantum Teleportation›

theory Quantum_Teleportation
imports 
  More_Tensor
  Basics
  Measurement
begin


definition alice:: "complex Matrix.mat  complex Matrix.mat" where
"alice φ  (H  Id 2) * ((CNOT  Id 1) * (φ  00))"

abbreviation M1:: "complex Matrix.mat" where
"M1  mat_of_cols_list 8 [[1, 0, 0, 0, 0, 0, 0, 0],
                          [0, 1, 0, 0, 0, 0, 0, 0],
                          [0, 0, 1, 0, 0, 0, 0, 0],
                          [0, 0, 0, 1, 0, 0, 0, 0],
                          [0, 0, 0, 0, 0, 0, 1, 0],
                          [0, 0, 0, 0, 0, 0, 0, 1],
                          [0, 0, 0, 0, 1, 0, 0, 0],
                          [0, 0, 0, 0, 0, 1, 0, 0]]"

lemma tensor_prod_of_cnot_id_1: 
  shows "(CNOT  Id 1) = M1"
proof
  show "dim_col (CNOT  Id 1) = dim_col M1" 
    by(simp add: CNOT_def Id_def mat_of_cols_list_def)
  show "dim_row (CNOT  Id 1) = dim_row M1"
    by(simp add: CNOT_def Id_def  mat_of_cols_list_def)
  fix i j::nat assume "i < dim_row M1" and "j < dim_col M1"
  then have "i  {0..<8}  j  {0..<8}"
    by (auto simp add:  mat_of_cols_list_def)
  then show "(CNOT  Id 1) $$ (i, j) = M1 $$ (i, j)"
    by (auto simp add: Id_def CNOT_def mat_of_cols_list_def)
qed

abbreviation M2:: "complex Matrix.mat" where
"M2  mat_of_cols_list 8 [[1/sqrt(2), 0, 0, 0, 1/sqrt(2), 0, 0, 0],
                          [0, 1/sqrt(2), 0, 0, 0, 1/sqrt(2), 0, 0],
                          [0, 0, 1/sqrt(2), 0, 0, 0, 1/sqrt(2), 0],
                          [0, 0, 0, 1/sqrt(2), 0, 0, 0, 1/sqrt(2)],
                          [1/sqrt(2), 0, 0, 0, -1/sqrt(2), 0, 0, 0],
                          [0, 1/sqrt(2), 0, 0, 0, -1/sqrt(2), 0, 0],
                          [0, 0, 1/sqrt(2), 0, 0, 0, -1/sqrt(2), 0],
                          [0, 0, 0, 1/sqrt(2), 0, 0, 0, -1/sqrt(2)]]"

lemma tensor_prod_of_h_id_2: 
  shows "(H  Id 2) = M2"
proof
  show "dim_col (H  Id 2) = dim_col M2"
    by(simp add: H_def Id_def mat_of_cols_list_def)
  show "dim_row (H  Id 2) = dim_row M2"
    by(simp add: H_def Id_def mat_of_cols_list_def)
  fix i j::nat assume "i < dim_row M2" and "j < dim_col M2"
  then have "i  {0..<8}  j  {0..<8}"
    by (auto simp add:  mat_of_cols_list_def)
  then show "(H  Id 2) $$ (i, j) = M2 $$ (i, j)"
    by (auto simp add: Id_def H_def mat_of_cols_list_def)
qed

lemma alice_step_1_state [simp]:
  assumes "state 1 φ"
  shows "state 3 (φ  00)"
  using assms bell00_is_state tensor_state by(metis One_nat_def Suc_1 numeral_3_eq_3 plus_1_eq_Suc)

lemma alice_step_2_state:
  assumes "state 1 φ"
  shows "state 3 ((CNOT  Id 1) * (φ  00))"
proof-
  have "gate 3 (CNOT  Id 1)"
    using CNOT_is_gate id_is_gate tensor_gate by (metis numeral_plus_one semiring_norm(5))
  then show "state 3 ((CNOT  Id 1) * (φ  00))" using assms by simp
qed

lemma alice_state [simp]:
  assumes "state 1 φ"
  shows "state 3 (alice φ) "
proof-
  have "gate 3 (H  Id 2)"
    using tensor_gate id_is_gate H_is_gate by(metis eval_nat_numeral(3) plus_1_eq_Suc)
  then show ?thesis 
    using assms alice_step_2_state by(simp add: alice_def)
qed

lemma alice_step_1:
  assumes "state 1 φ" and "α = φ $$ (0,0)" and "β = φ $$ (1,0)"
  shows "(φ  00) = mat_of_cols_list 8 [[α/sqrt(2),0,0,α/sqrt(2),β/sqrt(2),0,0,β/sqrt(2)]]"
proof
  define v where asm:"v = mat_of_cols_list 8 [[α/sqrt(2),0,0,α/sqrt(2),β/sqrt(2),0,0,β/sqrt(2)]]"
  then show "dim_row (φ  00) = dim_row v"
    using assms(1) alice_step_1_state state.dim_row mat_of_cols_list_def by fastforce
  show "dim_col (φ  00) = dim_col v"
    using assms(1) alice_step_1_state state.is_column asm mat_of_cols_list_def by fastforce
  show "i j. i < dim_row v  j < dim_col v  (φ  00) $$ (i,j) = v $$ (i,j)"
  proof-
    fix i j assume "i < dim_row v" and "j < dim_col v"
    then have "i  {0..<8}  j = 0"
      using asm by (auto simp add: mat_of_cols_list_def)
    moreover have "dim_row 00 = 4"
      using bell00_is_state state_def by simp
    moreover have "dim_col 00 = 1"
      using bell00_is_state state_def by simp
    ultimately show "(φ  00) $$ (i, j) = v $$ (i,j)"
      using state_def assms asm by (auto simp add: bell00_def)
  qed
qed

lemma alice_step_2:
  assumes "state 1 φ" and "α = φ $$ (0,0)" and "β = φ $$ (1,0)"
  shows "(CNOT  Id 1) * (φ  00) = mat_of_cols_list 8 [[α/sqrt(2),0,0,α/sqrt(2),0,β/sqrt(2),β/sqrt(2),0]]"
proof
  have f0:"(φ  00) = mat_of_cols_list 8 [[α/sqrt(2),0,0,α/sqrt(2),β/sqrt(2),0,0,β/sqrt(2)]]"
    using assms alice_step_1 by simp
  define v where asm:"v = mat_of_cols_list 8 [[α/sqrt(2),0,0,α/sqrt(2),0,β/sqrt(2),β/sqrt(2),0]]"
  then show "dim_row ((CNOT  Id 1) * (φ  00)) = dim_row v"
    using assms(1) alice_step_2_state state.dim_row mat_of_cols_list_def by fastforce
  show "dim_col ((CNOT  Id 1) * (φ  00)) = dim_col v"
    using assms(1) alice_step_2_state state.is_column asm mat_of_cols_list_def by fastforce
  show "i j. i<dim_row v  j<dim_col v  ((CNOT  Id 1) * (φ  00)) $$ (i,j) = v $$ (i,j)"
  proof-
    fix i j assume "i < dim_row v" and "j < dim_col v"
    then have "i  {0..<8::nat}  j = 0"
      using asm by (auto simp add: mat_of_cols_list_def)
    then have "(M1 * (φ  00)) $$ (i,j) = v $$ (i,j)"
      by (auto simp add: f0 asm mat_of_cols_list_def times_mat_def scalar_prod_def)
    then show "((CNOT  Id 1) * (φ  00)) $$ (i,j) = v $$ (i,j)"
      using tensor_prod_of_cnot_id_1 by simp
  qed
qed

lemma alice_result:
  assumes "state 1 φ" and "α = φ $$ (0,0)" and "β = φ $$ (1,0)"
  shows "alice φ = mat_of_cols_list 8 [[α/2, β/2, β/2, α/2, α/2, -β/2, -β/2, α/2]]"
proof
  define v where a0:"v = mat_of_cols_list 8 [[α/2, β/2, β/2, α/2, α/2, -β/2, -β/2, α/2]]"
  define w where a1:"w = (CNOT  Id 1) * (φ  00)"
  then have f0:"w = mat_of_cols_list 8 [[α/sqrt(2), 0, 0, α/sqrt(2), 0, β/sqrt(2), β/sqrt(2), 0]]"
    using assms alice_step_2 by simp
  show "dim_row (alice φ) = dim_row v"
    using assms(1) alice_state state_def a0 by (simp add: mat_of_cols_list_def)
  show "dim_col (alice φ) = dim_col v"
    using assms(1) alice_state state_def a0 by (simp add: mat_of_cols_list_def)
  show "i j. i < dim_row v  j < dim_col v  alice φ $$ (i,j) = v $$ (i,j)"
  proof-
    fix i j assume "i < dim_row v" and "j < dim_col v"
    then have "i  {0..<8}  j = 0"
      using a0 by (auto simp add: Tensor.mat_of_cols_list_def)
    then have "(M2 * w) $$ (i,j) = v $$ (i,j)"
      by (auto simp add: f0 a0 mat_of_cols_list_def times_mat_def scalar_prod_def)
    then show "alice φ $$ (i,j) = v $$ (i,j)"
      by (simp add: tensor_prod_of_h_id_2 alice_def a1)
  qed
qed

text ‹
An application of function @{term "alice"} to a state @{term "φ"} of a 1-qubit system results in the following cases.
›

definition alice_meas:: "complex Matrix.mat  _list" where
"alice_meas φ = [
  ((prob0 3 (alice φ) 0) * (prob0 3 (post_meas0 3 (alice φ) 0) 1), post_meas0 3 (post_meas0 3 (alice φ) 0) 1)
, ((prob0 3 (alice φ) 0) * (prob1 3 (post_meas0 3 (alice φ) 0) 1), post_meas1 3 (post_meas0 3 (alice φ) 0) 1)
, ((prob1 3 (alice φ) 0) * (prob0 3 (post_meas1 3 (alice φ) 0) 1), post_meas0 3 (post_meas1 3 (alice φ) 0) 1)
, ((prob1 3 (alice φ) 0) * (prob1 3 (post_meas1 3 (alice φ) 0) 1), post_meas1 3 (post_meas1 3 (alice φ) 0) 1)
]"

definition alice_pos:: "complex Matrix.mat  complex Matrix.mat  bool" where
"alice_pos φ q   q = mat_of_cols_list 8 [[φ $$ (0,0), φ $$ (1,0), 0, 0, 0, 0, 0, 0]] 
                  q = mat_of_cols_list 8 [[0, 0, φ $$ (1,0), φ $$ (0,0), 0, 0, 0, 0]] 
                  q = mat_of_cols_list 8 [[0, 0, 0, 0, φ $$ (0,0), - φ $$ (1,0), 0, 0]] 
                  q = mat_of_cols_list 8 [[0, 0, 0, 0, 0, 0, - φ $$ (1,0), φ $$ (0,0)]]"

lemma phi_vec_length:
  assumes "state 1 φ"
  shows "cmod(φ $$ (0,0))^2 + cmod(φ $$ (Suc 0,0))^2 = 1"
  using set_2 assms state_def Matrix.col_def cpx_vec_length_def by(auto simp add: atLeast0LessThan)

lemma select_index_3_subsets [simp]: 
  shows "{j::nat. select_index 3 0 j} = {4,5,6,7} 
         {j::nat. j < 8  ¬ select_index 3 0 j} = {0,1,2,3} 
         {j::nat. select_index 3 1 j} = {2,3,6,7} 
         {j::nat. j < 8  ¬ select_index 3 1 j} = {0,1,4,5}"
proof-
  have "{j::nat. select_index 3 0 j} = {4,5,6,7}" by (auto simp add: select_index_def)
  moreover have "{j::nat. j < 8  ¬ select_index 3 0 j} = {0,1,2,3}" by(auto simp add: select_index_def)
  moreover have f1:"{j::nat. select_index 3 1 j} = {2,3,6,7}"
  proof
    show "{j. select_index 3 1 j}  {2,3,6,7}"
    proof
      fix j::nat assume "j  {j. select_index 3 1 j}"
      then have "j  {0..<8}  j mod 4  {2,3}" by (auto simp add: select_index_def)
      then show "j  {2,3,6,7}" by auto
    qed
    show "{2,3,6,7}  {j. select_index 3 1 j}" by (auto simp add: select_index_def)
  qed
  moreover have "{j::nat. j < 8  ¬ select_index 3 1 j} = {0,1,4,5}"
  proof-
    have "{j::nat. j < 8  j  {2,3,6,7}} = {0,1,4,5}"  by auto
    then show ?thesis using f1 by blast
  qed
  ultimately show ?thesis by simp
qed

lemma prob_index_0_alice:
  assumes "state 1 φ"
  shows "prob0 3 (alice φ) 0 = 1/2  prob1 3 (alice φ) 0 = 1/2"
proof
  show "prob0 3 (alice φ) 0 = 1/2"
    using alice_result assms prob0_def alice_state
    apply auto by (metis (no_types, opaque_lifting) One_nat_def phi_vec_length four_x_squared mult.commute 
nonzero_mult_div_cancel_right times_divide_eq_right zero_neq_numeral)
  then show"prob1 3 (alice φ) 0 = 1/2"
    using prob_sum_is_one[of "3" "alice φ" "0"] alice_state[of "φ"] assms by linarith
qed

lemma post_meas0_index_0_alice:
  assumes "state 1 φ" and "α = φ $$ (0,0)" and "β = φ $$ (1,0)"
  shows "post_meas0 3 (alice φ) 0 = 
mat_of_cols_list 8 [[α/sqrt(2), β/sqrt(2), β/sqrt(2), α/sqrt(2), 0, 0, 0, 0]]"
proof
  define v where asm:"v = mat_of_cols_list 8 [[α/sqrt(2),β/sqrt(2),β/sqrt(2),α/sqrt(2),0,0,0,0]]"
  then show "dim_row (post_meas0 3 (alice φ) 0) = dim_row v"
    using mat_of_cols_list_def post_meas0_def assms(1) alice_state ket_vec_def by simp
  show "dim_col (post_meas0 3 (alice φ) 0) = dim_col v"
    using mat_of_cols_list_def post_meas0_def assms(1) alice_state ket_vec_def asm by simp
  show "i j. i<dim_row v  j<dim_col v  post_meas0 3 (alice φ) 0 $$ (i,j) = v $$ (i,j)"
  proof-
    fix i j assume "i < dim_row v" and "j < dim_col v"
    then have "i  {0..<8}  j = 0"
      using asm set_8_atLeast0 mat_of_cols_list_def by auto
    then show "post_meas0 3 (alice φ) 0 $$ (i, j) = v $$ (i, j)"
      using post_meas0_def assms asm mat_of_cols_list_def ket_vec_def
      apply (auto simp add: prob_index_0_alice)
      using assms(1) alice_result select_index_def by auto
  qed
qed

lemma post_meas1_index_0_alice:
  assumes "state 1 φ" and "α = φ $$ (0,0)" and "β = φ $$ (1,0)"
  shows "post_meas1 3 (alice φ) 0 = mat_of_cols_list 8 [[0,0,0,0,α/sqrt(2),-β/sqrt(2),-β/sqrt(2),α/sqrt(2)]]"
proof
  define v where asm:"v = mat_of_cols_list 8 [[0,0,0,0,α/sqrt(2),-β/sqrt(2),-β/sqrt(2),α/sqrt(2)]]"
  then show "dim_row (post_meas1 3 (alice φ) 0) = dim_row v"
    using mat_of_cols_list_def post_meas1_def assms(1) alice_state ket_vec_def by simp
  show "dim_col (post_meas1 3 (alice φ) 0) = dim_col v"
    using mat_of_cols_list_def post_meas1_def assms(1) alice_state ket_vec_def asm by simp
  show "i j. i<dim_row v  j<dim_col v  post_meas1 3 (alice φ) 0 $$ (i,j) = v $$ (i,j)"
  proof-
    fix i j assume "i < dim_row v" and "j < dim_col v"
    then have "i  {0..<8}  j = 0"
      using asm set_8_atLeast0 mat_of_cols_list_def by auto
    then show "post_meas1 3 (alice φ) 0 $$ (i,j) = v $$ (i,j)"
      using post_meas1_def assms asm mat_of_cols_list_def ket_vec_def
      apply (auto simp add: prob_index_0_alice)
      using assms(1) alice_result select_index_def by auto
  qed
qed

lemma post_meas0_index_0_alice_state [simp]:
  assumes "state 1 φ"
  shows "state 3 (post_meas0 3 (alice φ) 0)"
  using assms by (simp add: prob_index_0_alice)

lemma post_meas1_index_0_alice_state [simp]:
  assumes "state 1 φ"
  shows "state 3 (post_meas1 3 (alice φ) 0)"
  using assms by (simp add: prob_index_0_alice)

lemma Alice_case [simp]:
  assumes "state 1 φ" and "state 3 q" and "List.member (alice_meas φ) (p, q)"
  shows "alice_pos φ q"
proof-
  define α β where a0:"α = φ $$ (0,0)" and a1:"β = φ $$ (1,0)"
  have f0:"prob0 3 (Matrix.mat 8 (Suc 0) (λ(i,j). [[φ $$ (0,0)/sqrt 2, φ $$ (Suc 0,0)/sqrt 2, 
                    φ $$ (Suc 0,0)/sqrt 2, φ $$ (0,0)/sqrt 2,0,0,0,0]]!j!i)) (Suc 0) = 1/2"
    using post_meas0_index_0_alice prob0_def mat_of_cols_list_def post_meas0_index_0_alice_state 
assms(1) a0 a1 select_index_3_subsets by (auto simp add: norm_divide power_divide phi_vec_length)
  have f1:"prob1 3 (Matrix.mat 8 (Suc 0) (λ(i,j). [[φ $$ (0,0)/sqrt 2, φ $$ (Suc 0,0)/sqrt 2, 
                    φ $$ (Suc 0,0)/sqrt 2, φ $$ (0,0)/sqrt 2, 0, 0, 0, 0]] ! j ! i)) (Suc 0) = 1/2"
    using post_meas0_index_0_alice prob1_def mat_of_cols_list_def post_meas0_index_0_alice_state 
assms(1) a0 a1 select_index_3_subsets by(auto simp add: norm_divide power_divide phi_vec_length algebra_simps)
  have f2:"prob0 3 (Matrix.mat 8 (Suc 0) 
          (λ(i,j). [[0,0,0,0,φ $$ (0,0)/complex_of_real (sqrt 2),-(φ $$ (Suc 0,0)/complex_of_real (sqrt 2)), 
-(φ $$ (Suc 0,0)/complex_of_real (sqrt 2)),φ $$ (0,0)/complex_of_real (sqrt 2)]] ! j ! i)) (Suc 0) = 1/2"
    using post_meas1_index_0_alice prob0_def mat_of_cols_list_def post_meas1_index_0_alice_state 
      assms(1) a0 a1 select_index_3_subsets by(auto simp add: norm_divide power_divide phi_vec_length)
  have f3:"prob1 3 (Matrix.mat 8 (Suc 0) 
          (λ(i,j). [[0,0,0,0,φ $$ (0,0)/complex_of_real (sqrt 2),-(φ $$ (Suc 0,0)/complex_of_real (sqrt 2)), 
-(φ $$ (Suc 0,0)/complex_of_real (sqrt 2)), φ $$ (0,0)/complex_of_real (sqrt 2)]] ! j ! i)) (Suc 0) = 1/2"
    using post_meas1_index_0_alice prob1_def mat_of_cols_list_def post_meas1_index_0_alice_state 
assms(1) a0 a1 select_index_3_subsets by(auto simp add: norm_divide power_divide phi_vec_length algebra_simps)
  have "(p, q) = ((prob0 3 (alice φ) 0) * (prob0 3 (post_meas0 3 (alice φ) 0) 1), post_meas0 3 (post_meas0 3 (alice φ) 0) 1) 
        (p, q) = ((prob0 3 (alice φ) 0) * (prob1 3 (post_meas0 3 (alice φ) 0) 1), post_meas1 3 (post_meas0 3 (alice φ) 0) 1) 
        (p, q) = ((prob1 3 (alice φ) 0) * (prob0 3 (post_meas1 3 (alice φ) 0) 1), post_meas0 3 (post_meas1 3 (alice φ) 0) 1) 
        (p, q) = ((prob1 3 (alice φ) 0) * (prob1 3 (post_meas1 3 (alice φ) 0) 1), post_meas1 3 (post_meas1 3 (alice φ) 0) 1)"
    using assms(3) alice_meas_def List.member_def by(smt (verit) list.distinct(1) list.exhaust list.inject member_rec(1) member_rec(2))
  then have "q = post_meas0 3 (post_meas0 3 (alice φ) 0) 1  q = post_meas1 3 (post_meas0 3 (alice φ) 0) 1 
             q = post_meas0 3 (post_meas1 3 (alice φ) 0) 1  q = post_meas1 3 (post_meas1 3 (alice φ) 0) 1"
    by auto
  moreover have "post_meas0 3 (post_meas0 3 (alice φ) 0) 1 = mat_of_cols_list 8 [[α,β,0,0,0,0,0,0]]"
  proof
    define v where asm:"v = mat_of_cols_list 8 [[α, β, 0, 0, 0, 0, 0, 0]]"
    then show "dim_row (post_meas0 3 (post_meas0 3 (alice φ) 0) 1) = dim_row v"
      using mat_of_cols_list_def post_meas0_def ket_vec_def by simp
    show "dim_col (post_meas0 3 (post_meas0 3 (alice φ) 0) 1) = dim_col v"
      using mat_of_cols_list_def post_meas0_def ket_vec_def asm by simp
    show "i j. i<dim_row v  j<dim_col v  post_meas0 3 (post_meas0 3 (alice φ) 0) 1 $$ (i,j) = v $$ (i,j)"
    proof-
      fix i j assume "i < dim_row v" and "j < dim_col v"
      then have "i  {0..<8}  j = 0"
        using asm mat_of_cols_list_def by auto
      then show "post_meas0 3 (post_meas0 3 (alice φ) 0) 1 $$ (i,j) = v $$ (i,j)"
        using post_meas0_index_0_alice assms(1) a0 a1
        apply (auto)
        using post_meas0_def asm mat_of_cols_list_def ket_vec_def select_index_def
        by (auto simp add: f0 real_sqrt_divide)
    qed
  qed
  moreover have "post_meas1 3 (post_meas0 3 (alice φ) 0) 1 = mat_of_cols_list 8 [[0,0,β,α,0,0,0,0]]"
  proof
    define v where asm:"v = mat_of_cols_list 8 [[0,0,β,α,0,0,0,0]]"
    then show "dim_row (post_meas1 3 (post_meas0 3 (alice φ) 0) 1) = dim_row v"
      using mat_of_cols_list_def post_meas1_def ket_vec_def asm by auto
    show "dim_col (post_meas1 3 (post_meas0 3 (alice φ) 0) 1) = dim_col v"
      using mat_of_cols_list_def post_meas1_def ket_vec_def asm by auto
    show "i j. i<dim_row v  j<dim_col v  post_meas1 3 (post_meas0 3 (alice φ) 0) 1 $$ (i,j) = v $$ (i,j)"
    proof-
      fix i j assume "i < dim_row v" and "j < dim_col v"
      then have "i  {0..<8}  j = 0"
        using asm mat_of_cols_list_def by auto
      then show "post_meas1 3 (post_meas0 3 (alice φ) 0) 1 $$ (i,j) = v $$ (i,j)"
        using post_meas0_index_0_alice assms(1) a0 a1
        apply (auto)
        using post_meas1_def asm mat_of_cols_list_def ket_vec_def select_index_def
        by (auto simp add: f1 real_sqrt_divide)
    qed
  qed
  moreover have "post_meas0 3 (post_meas1 3 (alice φ) 0) 1 = mat_of_cols_list 8 [[0,0,0,0,α,-β,0,0]]"
  proof
    define v where asm:"v = mat_of_cols_list 8 [[0, 0, 0, 0, α, -β, 0, 0]]"
    then show "dim_row (post_meas0 3 (post_meas1 3 (alice φ) 0) 1) = dim_row v"
      using mat_of_cols_list_def post_meas0_def ket_vec_def by simp
    show "dim_col (post_meas0 3 (post_meas1 3 (alice φ) 0) 1) = dim_col v"
      using mat_of_cols_list_def post_meas0_def ket_vec_def asm by simp
    show "i j. i<dim_row v  j<dim_col v  post_meas0 3 (post_meas1 3 (alice φ) 0) 1 $$ (i,j) = v $$ (i,j)"
    proof-
      fix i j assume "i < dim_row v" and "j < dim_col v"
      then have "i  {0..<8}  j = 0"
        using asm mat_of_cols_list_def by auto
      then show "post_meas0 3 (post_meas1 3 (alice φ) 0) 1 $$ (i,j) = v $$ (i,j)"
        using post_meas1_index_0_alice assms(1) a0 a1
        apply (auto)
        using post_meas0_def asm mat_of_cols_list_def ket_vec_def select_index_def
        by (auto simp add: f2 real_sqrt_divide)
    qed
  qed
  moreover have "post_meas1 3 (post_meas1 3 (alice φ) 0) 1 = mat_of_cols_list 8 [[0,0,0,0,0,0,-β,α]]"
  proof
    define v where asm:"v = mat_of_cols_list 8 [[0,0,0,0,0,0,-β,α]]"
    then show "dim_row (post_meas1 3 (post_meas1 3 (alice φ) 0) 1) = dim_row v"
      using mat_of_cols_list_def post_meas1_def ket_vec_def by simp
    show "dim_col (post_meas1 3 (post_meas1 3 (alice φ) 0) 1) = dim_col v"
      using mat_of_cols_list_def post_meas1_def ket_vec_def asm by simp
    show "i j. i<dim_row v  j<dim_col v  post_meas1 3 (post_meas1 3 (alice φ) 0) 1 $$ (i,j) = v $$ (i,j)"
    proof-
      fix i j assume "i < dim_row v" and "j < dim_col v"
      then have "i  {0..<8}  j = 0"
        using asm mat_of_cols_list_def by auto
      then show "post_meas1 3 (post_meas1 3 (alice φ) 0) 1 $$ (i,j) = v $$ (i,j)"
        using post_meas1_index_0_alice assms(1) a0 a1
        apply (auto)
        using post_meas1_def asm mat_of_cols_list_def ket_vec_def select_index_def
        by (auto simp add: f3 real_sqrt_divide)
    qed
  qed
  ultimately show ?thesis using alice_pos_def a0 a1 by simp
qed


datatype bit = zero | one

definition alice_out:: "complex Matrix.mat => complex Matrix.mat => bit × bit" where
"alice_out φ q  
if q = mat_of_cols_list 8 [[φ $$ (0,0), φ $$ (1,0), 0, 0, 0, 0, 0, 0]] then (zero, zero) else
  if q = mat_of_cols_list 8 [[0, 0, φ $$ (1,0), φ $$ (0,0), 0, 0, 0, 0]] then (zero, one) else
    if q = mat_of_cols_list 8 [[0, 0, 0, 0, φ $$ (0,0), - φ $$ (1,0), 0, 0]] then (one, zero) else
      if q = mat_of_cols_list 8 [[0, 0, 0, 0, 0, 0, - φ $$ (1,0), φ $$ (0,0)]] then (one, one) else 
        undefined"

definition bob:: "complex Matrix.mat => bit × bit  complex Matrix.mat" where
"bob q b  
if (fst b, snd b) = (zero, zero) then q else 
  if (fst b, snd b) = (zero, one) then (Id 2  X) * q else
    if (fst b, snd b) = (one, zero) then (Id 2  Z) * q else
      if (fst b, snd b) = (one, one) then (Id 2  Z * X) * q else 
        undefined"

lemma alice_out_unique [simp]:
  assumes "state 1 φ"
  shows "Matrix.mat 8 (Suc 0) (λ(i,j). [[0, 0, φ $$ (Suc 0, 0), φ $$ (0, 0), 0, 0, 0, 0]]!j!i) 
         Matrix.mat 8 (Suc 0) (λ(i,j). [[φ $$ (0, 0), φ $$ (Suc 0, 0), 0, 0, 0, 0, 0, 0]]!j!i)  
         Matrix.mat 8 (Suc 0) (λ(i,j). [[0, 0, 0, 0, φ $$ (0, 0), -φ $$ (Suc 0, 0), 0, 0]]!j!i) 
         Matrix.mat 8 (Suc 0) (λ(i,j). [[φ $$ (0, 0), φ $$ (Suc 0, 0), 0, 0, 0, 0, 0, 0]]!j!i)  
         Matrix.mat 8 (Suc 0) (λ(i,j). [[0, 0, 0, 0, 0, 0, -φ $$ (Suc 0, 0), φ $$ (0, 0)]]!j!i) 
         Matrix.mat 8 (Suc 0) (λ(i,j). [[φ $$ (0, 0), φ $$ (Suc 0, 0), 0, 0, 0, 0, 0, 0]]!j!i)  
         Matrix.mat 8 (Suc 0) (λ(i,j). [[0, 0, 0, 0, φ $$ (0, 0), -φ $$ (Suc 0, 0), 0, 0]]!j!i) 
         Matrix.mat 8 (Suc 0) (λ(i,j). [[0, 0, φ $$ (Suc 0, 0), φ $$ (0, 0), 0, 0, 0, 0]]!j!i)  
         Matrix.mat 8 (Suc 0) (λ(i,j). [[0, 0, 0, 0, 0, 0, -φ $$ (Suc 0, 0), φ $$ (0, 0)]]!j!i) 
         Matrix.mat 8 (Suc 0) (λ(i,j). [[0, 0, φ $$ (Suc 0, 0), φ $$ (0, 0), 0, 0, 0, 0]]!j!i)  
         Matrix.mat 8 (Suc 0) (λ(i,j). [[0, 0, 0, 0, 0, 0, -φ $$ (Suc 0, 0), φ $$ (0, 0)]]!j!i) 
         Matrix.mat 8 (Suc 0) (λ(i,j). [[0, 0, 0, 0, φ $$ (0, 0), -φ $$ (Suc 0, 0), 0, 0]]!j!i)"
proof-
  have f0:"φ $$ (0,0)  0  φ $$ (1,0)  0"
    using assms state_def Matrix.col_def cpx_vec_length_def set_2 by(auto simp add: atLeast0LessThan)
  define v1 v2 v3 v4 where d0:"v1 = Matrix.mat 8 1 (λ(i,j). [[φ $$ (0,0),φ $$ (1,0),0,0,0,0,0,0]]!j!i)"
                       and d1:"v2 = Matrix.mat 8 1 (λ(i,j). [[0,0,φ $$ (1,0), φ $$ (0,0),0,0,0,0]]!j!i)"
                       and d2:"v3 = Matrix.mat 8 1 (λ(i,j). [[0,0,0,0,φ $$ (0,0),-φ $$ (1,0),0,0]]!j!i)"
                       and d3:"v4 = Matrix.mat 8 1 (λ(i,j). [[0,0,0,0,0,0,-φ $$ (1,0),φ $$ (0,0)]]!j!i)"
  then have "(v1 $$ (0,0)  v2 $$ (0,0)  v1 $$ (1,0)  v2 $$ (1,0))  
             (v1 $$ (0,0)  v3 $$ (0,0)  v1 $$ (1,0)  v3 $$ (1,0))   
             (v1 $$ (0,0)  v4 $$ (0,0)  v1 $$ (1,0)  v4 $$ (1,0))   
             (v2 $$ (2,0)  v3 $$ (2,0)  v2 $$ (3,0)  v3 $$ (3,0))   
             (v2 $$ (2,0)  v4 $$ (2,0)  v2 $$ (3,0)  v4 $$ (3,0))   
             (v3 $$ (4,0)  v4 $$ (4,0)  v3 $$ (5,0)  v4 $$ (5,0))" using f0 by auto
  then have "v1  v2  v1  v3  v1  v4  v2  v3  v2  v4  v3  v4" by auto
  thus ?thesis by (auto simp add: d0 d1 d2 d3)
qed

abbreviation M3:: "complex Matrix.mat" where 
"M3  mat_of_cols_list 8 [[0, 1, 0, 0, 0, 0, 0, 0],
                          [1, 0, 0, 0, 0, 0, 0, 0],
                          [0, 0, 0, 1, 0, 0, 0, 0],
                          [0, 0, 1, 0, 0, 0, 0, 0],
                          [0, 0, 0, 0, 0, 1, 0, 0],
                          [0, 0, 0, 0, 1, 0, 0, 0],
                          [0, 0, 0, 0, 0, 0, 0, 1],
                          [0, 0, 0, 0, 0, 0, 1, 0]]"

lemma tensor_prod_of_id_2_x:
  shows "(Id 2  X) = M3"
proof
    have f0:"gate 3 (Id 2  X)"
      using X_is_gate tensor_gate[of "2" "Id 2" "1" "X"] by simp
    then show "dim_row (Id 2  X) = dim_row M3"
      using gate_def by (simp add: mat_of_cols_list_def)
    show "dim_col (Id 2  X) = dim_col M3"
      using f0 gate_def by (simp add: mat_of_cols_list_def)
    show "i j. i < dim_row M3  j < dim_col M3  (Id 2  X) $$ (i,j) = M3 $$ (i,j)"
    proof-
      fix i j assume "i < dim_row M3" and "j < dim_col M3"
      then have "i  {0..<8}  j  {0..<8}" by (auto simp add: mat_of_cols_list_def)
      then show "(Id 2  X) $$ (i,j) = M3 $$ (i,j)"
        using Id_def X_def index_tensor_mat[of "Id 2" "4" "4" "X" "2" "2" "i" "j"] gate_def X_is_gate 
id_is_gate Id_def by (auto simp add: mat_of_cols_list_def X_def)
    qed
qed

abbreviation M4:: "complex Matrix.mat" where 
"M4  mat_of_cols_list 8 [[0, -1, 0, 0, 0, 0, 0, 0],
                          [1, 0, 0, 0, 0, 0, 0, 0],
                          [0, 0, 0, -1, 0, 0, 0, 0],
                          [0, 0, 1, 0, 0, 0, 0, 0],
                          [0, 0, 0, 0, 0, -1, 0, 0],
                          [0, 0, 0, 0, 1, 0, 0, 0],
                          [0, 0, 0, 0, 0, 0, 0, -1],
                          [0, 0, 0, 0, 0, 0, 1, 0]]"

abbreviation ZX:: "complex Matrix.mat" where
"ZX  mat_of_cols_list 2 [[0, -1], [1, 0]]"

lemma l_inv_of_ZX:
  shows "ZX * ZX = 1m 2"
proof
  show "dim_row (ZX * ZX) = dim_row (1m 2)" using dagger_def mat_of_cols_list_def by simp
  show "dim_col (ZX * ZX) = dim_col (1m 2)" using dagger_def mat_of_cols_list_def by simp
  show "i j. i < dim_row (1m 2)  j < dim_col (1m 2)  (ZX * ZX) $$ (i, j) = 1m 2 $$ (i, j)"
  proof-
    fix i j assume "i < dim_row (1m 2)" and "j < dim_col (1m 2)"
    then have "i  {0..<2}  j  {0..<2}" by auto
    then show "(ZX * ZX) $$ (i, j) = 1m 2 $$ (i, j)"
      using mat_of_cols_list_def dagger_def by (auto simp add: set_2)
  qed
qed

lemma r_inv_of_ZX:
  shows "ZX * (ZX) = 1m 2"
proof
  show "dim_row (ZX * (ZX)) = dim_row (1m 2)" using dagger_def mat_of_cols_list_def by simp
  show "dim_col (ZX * (ZX)) = dim_col (1m 2)" using dagger_def mat_of_cols_list_def by simp
  show "i j. i < dim_row (1m 2)  j < dim_col (1m 2)  (ZX * (ZX)) $$ (i, j) = 1m 2 $$ (i, j)"
  proof-
    fix i j assume "i < dim_row (1m 2)" and "j < dim_col (1m 2)"
    then have "i  {0..<2}  j  {0..<2}" by auto
    then show "(ZX * (ZX)) $$ (i, j) = 1m 2 $$ (i, j)"
      using mat_of_cols_list_def dagger_def by (auto simp add: set_2)
  qed
qed

lemma ZX_is_gate [simp]:
  shows "gate 1 ZX"
proof
  show "dim_row ZX = 2 ^ 1" using mat_of_cols_list_def by simp
  show "square_mat ZX" using mat_of_cols_list_def by simp
  show "unitary ZX" using unitary_def l_inv_of_ZX r_inv_of_ZX mat_of_cols_list_def by auto
qed

lemma prod_of_ZX:
  shows "Z * X = ZX"
proof
  show "dim_row (Z * X) = dim_row ZX"
    using Z_is_gate mat_of_cols_list_def gate_def by auto
  show "dim_col (Z * X) = dim_col ZX"
    using X_is_gate mat_of_cols_list_def gate_def by auto
  show "i j. i < dim_row ZX  j < dim_col ZX  (Z * X) $$ (i, j) = ZX $$ (i, j)"
  proof-
    fix i j assume "i < dim_row ZX" and "j < dim_col ZX"
    then have "i  {0..<2}  j  {0..<2}" by (auto simp add: mat_of_cols_list_def)
    then show "(Z * X) $$ (i, j) = ZX $$ (i, j)" by (auto simp add: set_2 Z_def X_def)
  qed
qed

lemma tensor_prod_of_id_2_y:
  shows "(Id 2  Z * X) = M4"
proof
  have f0:"gate 3 (Id 2  Z * X)"
    using prod_of_ZX ZX_is_gate tensor_gate[of "2" "Id 2" "1" "Z * X"] by simp
  then show "dim_row (Id 2  Z * X) = dim_row M4"
      using gate_def by (simp add: mat_of_cols_list_def)
  show "dim_col (Id 2  Z * X) = dim_col M4"
    using f0 gate_def by (simp add: mat_of_cols_list_def)
  show "i j. i < dim_row M4  j < dim_col M4  (Id 2  Z * X) $$ (i,j) = M4 $$ (i,j)"
  proof-
    fix i j assume "i < dim_row M4" and "j < dim_col M4"
    then have "i  {0..<8}  j  {0..<8}" by (auto simp add: mat_of_cols_list_def)
    then have "(Id 2  ZX) $$ (i, j) = M4 $$ (i,j)"
      using Id_def mat_of_cols_list_def index_tensor_mat[of "Id 2" "4" "4" "ZX" "2" "2" "i" "j"] 
        gate_def ZX_is_gate id_is_gate
      by (auto simp add: mat_of_cols_list_def)
    then show "(Id 2  Z * X) $$ (i, j) = M4 $$ (i,j)"
      using prod_of_ZX by simp
    qed
qed

abbreviation M5:: "complex Matrix.mat" where 
"M5  mat_of_cols_list 8 [[1, 0, 0, 0, 0, 0, 0, 0],
                          [0, -1, 0, 0, 0, 0, 0, 0],
                          [0, 0, 1, 0, 0, 0, 0, 0],
                          [0, 0, 0, -1, 0, 0, 0, 0],
                          [0, 0, 0, 0, 1, 0, 0, 0],
                          [0, 0, 0, 0, 0, -1, 0, 0],
                          [0, 0, 0, 0, 0, 0, 1, 0],
                          [0, 0, 0, 0, 0, 0, 0, -1]]"

lemma tensor_prod_of_id_2_z:
  shows "(Id 2  Z) = M5"
proof
    have f0:"gate 3 (Id 2  Z)"
      using Z_is_gate tensor_gate[of "2" "Id 2" "1" "Z"] by simp
    then show "dim_row (Id 2  Z) = dim_row M5"
      using gate_def by (simp add:  mat_of_cols_list_def)
    show "dim_col (Id 2  Z) = dim_col M5"
      using f0 gate_def by (simp add:  mat_of_cols_list_def)
    show "i j. i < dim_row M5  j < dim_col M5  (Id 2  Z) $$ (i,j) = M5 $$ (i,j)"
    proof-
      fix i j assume "i < dim_row M5" and "j < dim_col M5"
      then have "i  {0..<8}  j  {0..<8}" by (auto simp add: mat_of_cols_list_def)
      then show "(Id 2  Z) $$ (i, j) = M5 $$ (i,j)"
        using Id_def Z_def index_tensor_mat[of "Id 2" "4" "4" "Z" "2" "2" "i" "j"] gate_def Z_is_gate 
id_is_gate Id_def by (auto simp add: mat_of_cols_list_def Z_def)
    qed
qed

lemma teleportation:
  assumes "state 1 φ" and "state 3 q" and "List.member (alice_meas φ) (p, q)"
  shows "r. state 2 r  bob q (alice_out φ q) = r  φ"
proof-
  define α β where a0:"α = φ $$ (0,0)" and a1:"β = φ $$ (1,0)"
  then have "q = mat_of_cols_list 8 [[α, β, 0, 0, 0, 0, 0, 0]] 
             q = mat_of_cols_list 8 [[0, 0, β, α, 0, 0, 0, 0]] 
             q = mat_of_cols_list 8 [[0, 0, 0, 0, α, -β, 0, 0]] 
             q = mat_of_cols_list 8 [[0, 0, 0, 0, 0, 0, -β, α]]"
    using assms Alice_case alice_pos_def by simp
  moreover have "q = mat_of_cols_list 8 [[α,β,0,0,0,0,0,0]]  bob q (alice_out φ q) = 
mat_of_cols_list 4 [[1, 0, 0, 0]]  φ"
  proof
    assume asm:"q = Tensor.mat_of_cols_list 8 [[α, β, 0, 0, 0, 0, 0, 0]]"
    show "dim_row (bob q (alice_out φ q)) = dim_row (Tensor.mat_of_cols_list 4 [[1,0,0,0]]  φ)"
      using mat_of_cols_list_def a0 a1 assms(1) state_def bob_def alice_out_def asm by simp
    show "dim_col (bob q (alice_out φ q)) = dim_col (Tensor.mat_of_cols_list 4 [[1,0,0,0]]  φ)"
      using mat_of_cols_list_def a0 a1 assms(1) state_def bob_def alice_out_def asm by simp
    show "i j. i < dim_row (Tensor.mat_of_cols_list 4 [[1,0,0,0]]  φ)  
                j < dim_col (Tensor.mat_of_cols_list 4 [[1,0,0,0]]  φ) 
           bob q (alice_out φ q) $$ (i, j) = (Tensor.mat_of_cols_list 4 [[1,0,0,0]]  φ) $$ (i,j)"
    proof-
      fix i j assume "i < dim_row (Tensor.mat_of_cols_list 4 [[1,0,0,0]]  φ)" and
                     "j < dim_col (Tensor.mat_of_cols_list 4 [[1,0,0,0]]  φ)"
      then have "i  {0..<8}  j = 0"
        using asm mat_of_cols_list_def assms state_def by auto
      then show "bob q (alice_out φ q) $$ (i,j) = (Tensor.mat_of_cols_list 4 [[1,0,0,0]]  φ) $$ (i,j)"
        using bob_def alice_out_def asm mat_of_cols_list_def a0 a1 assms state_def by auto
    qed
  qed
  moreover have "q = mat_of_cols_list 8 [[0,0,β,α,0,0,0,0]]  bob q (alice_out φ q) = 
mat_of_cols_list 4 [[0,1,0,0]]  φ"
  proof
    assume asm:"q = Tensor.mat_of_cols_list 8 [[0,0,β,α,0,0,0,0]]"
    show "dim_row (bob q (alice_out φ q)) = dim_row (Tensor.mat_of_cols_list 4 [[0,1,0,0]]  φ)"
      using mat_of_cols_list_def a0 a1 assms(1) state_def bob_def alice_out_def asm tensor_prod_of_id_2_x by simp
    show "dim_col (bob q (alice_out φ q)) = dim_col (Tensor.mat_of_cols_list 4 [[0,1,0,0]]  φ)"
      using mat_of_cols_list_def a0 a1 assms(1) state_def bob_def alice_out_def asm by simp    
    show "i j. i < dim_row (Tensor.mat_of_cols_list 4 [[0,1,0,0]]  φ)  
                j < dim_col (Tensor.mat_of_cols_list 4 [[0,1,0,0]]  φ) 
           bob q (alice_out φ q) $$ (i,j) = (Tensor.mat_of_cols_list 4 [[0,1,0,0]]  φ) $$ (i,j)"
    proof-
      fix i j assume "i < dim_row (Tensor.mat_of_cols_list 4 [[0,1,0,0]]  φ)" and
                     "j < dim_col (Tensor.mat_of_cols_list 4 [[0,1,0,0]]  φ)"
      then have c1:"i  {0..<8}  j = 0"
        using asm mat_of_cols_list_def assms(1) state_def by auto
      then have "(M3 * (Matrix.mat 8 1 (λ(i,j). [[0,0,φ $$ (1,0),φ $$ (0,0),0,0,0,0]]!j!i))) $$ (i,j) = 
(Tensor.mat_of_cols_list 4 [[0,1,0,0]]  φ) $$ (i,j)"
        using state_def assms(1) by(auto simp add:  a0 a1 mat_of_cols_list_def times_mat_def scalar_prod_def)
      then show "bob q (alice_out φ q) $$ (i,j) = (Tensor.mat_of_cols_list 4 [[0,1,0,0]]  φ) $$ (i,j)"
        using bob_def alice_out_def asm c1 a0 a1 mat_of_cols_list_def tensor_prod_of_id_2_x assms(1) by simp
    qed
  qed
  moreover have "q = mat_of_cols_list 8 [[0,0,0,0,α,-β,0,0]]  bob q (alice_out φ q) = 
mat_of_cols_list 4 [[0,0,1,0]]  φ"
  proof
    assume asm:"q = Tensor.mat_of_cols_list 8 [[0,0,0,0,α,-β,0,0]]"
    show "dim_row (bob q (alice_out φ q)) = dim_row (Tensor.mat_of_cols_list 4 [[0,0,1,0]]  φ)"
      using mat_of_cols_list_def a0 a1 assms(1) state_def bob_def alice_out_def asm tensor_prod_of_id_2_z by simp
    show "dim_col (bob q (alice_out φ q)) = dim_col (Tensor.mat_of_cols_list 4 [[0,0,1,0]]  φ)"
      using mat_of_cols_list_def a0 a1 assms(1) state_def bob_def alice_out_def asm by simp      
    show "i j. i < dim_row (Tensor.mat_of_cols_list 4 [[0,0,1,0]]  φ)  
                j < dim_col (Tensor.mat_of_cols_list 4 [[0,0,1,0]]  φ) 
           bob q (alice_out φ q) $$ (i,j) = (Tensor.mat_of_cols_list 4 [[0,0,1,0]]  φ) $$ (i,j)"
    proof-
      fix i j assume "i < dim_row (Tensor.mat_of_cols_list 4 [[0,0,1,0]]  φ)" and
                     "j < dim_col (Tensor.mat_of_cols_list 4 [[0,0,1,0]]  φ)"
      then have c1:"i  {0..<8}  j = 0"
        using asm mat_of_cols_list_def assms state_def by auto
      then have "(M5 * (Matrix.mat 8 (Suc 0) (λ(i,j). [[0,0,0,0,φ $$ (0,0),-φ $$ (Suc 0,0),0,0]]!j!i))) $$ (i,j) = 
(Tensor.mat_of_cols_list 4 [[0,0,1,0]]  φ) $$ (i,j)"
        using state_def assms(1) by(auto simp add: a0 a1 mat_of_cols_list_def times_mat_def scalar_prod_def)
      then show "bob q (alice_out φ q) $$ (i,j) = (Tensor.mat_of_cols_list 4 [[0,0,1,0]]  φ) $$ (i,j)"
        using bob_def alice_out_def asm c1 a0 a1 mat_of_cols_list_def tensor_prod_of_id_2_z assms(1) by simp
    qed
  qed
  moreover have "q = mat_of_cols_list 8 [[0, 0, 0, 0, 0, 0, -β, α]]  bob q (alice_out φ q) = 
mat_of_cols_list 4 [[0, 0, 0, 1]]  φ"
  proof
    assume asm:"q = Tensor.mat_of_cols_list 8 [[0, 0, 0, 0, 0, 0, -β, α]]"
    show "dim_row (bob q (alice_out φ q)) = dim_row (Tensor.mat_of_cols_list 4 [[0,0,0,1]]  φ)"
      using mat_of_cols_list_def a0 a1 assms(1) state_def bob_def alice_out_def asm tensor_prod_of_id_2_y by simp
    show "dim_col (bob q (alice_out φ q)) = dim_col (Tensor.mat_of_cols_list 4 [[0,0,0,1]]  φ)"
      using mat_of_cols_list_def a0 a1 assms(1) state_def bob_def alice_out_def asm by simp  
    show "i j. i < dim_row (Tensor.mat_of_cols_list 4 [[0,0,0,1]]  φ)  
                j < dim_col (Tensor.mat_of_cols_list 4 [[0,0,0,1]]  φ) 
           bob q (alice_out φ q) $$ (i,j) = (Tensor.mat_of_cols_list 4 [[0,0,0,1]]  φ) $$ (i,j)"
    proof-
      fix i j assume "i < dim_row (Tensor.mat_of_cols_list 4 [[0,0,0,1]]  φ)" and
                     "j < dim_col (Tensor.mat_of_cols_list 4 [[0,0,0,1]]  φ)"
      then have c1:"i  {0..<8}  j = 0"
        using asm mat_of_cols_list_def assms state_def by auto
      then have "(M4 * (Matrix.mat 8 (Suc 0) (λ(i, j). [[0,0,0,0,0,0,-φ $$ (Suc 0,0),φ $$ (0,0)]]!j!i))) $$ (i,j) = 
(Tensor.mat_of_cols_list 4 [[0,0,0,1]]  φ) $$ (i,j)"
        using state_def assms(1) by(auto simp add: a0 a1 mat_of_cols_list_def times_mat_def scalar_prod_def)
      then show "bob q (alice_out φ q) $$ (i,j) = (Tensor.mat_of_cols_list 4 [[0,0,0,1]]  φ) $$ (i,j)"
        using bob_def alice_out_def asm c1 a0 a1 mat_of_cols_list_def tensor_prod_of_id_2_y assms(1) by simp
    qed
  qed
  moreover have "state 2 (mat_of_cols_list 4 [[1, 0, 0, 0]])"
    using state_def mat_of_cols_list_def cpx_vec_length_def lessThan_atLeast0 by simp
  moreover have "state 2 (mat_of_cols_list 4 [[0, 1, 0, 0]])"
    using state_def mat_of_cols_list_def cpx_vec_length_def lessThan_atLeast0 by simp
  moreover have "state 2 (mat_of_cols_list 4 [[0, 0, 1, 0]])"
    using state_def mat_of_cols_list_def cpx_vec_length_def lessThan_atLeast0 by simp
  moreover have "state 2 (mat_of_cols_list 4 [[0, 0, 0, 1]])"
    using state_def mat_of_cols_list_def cpx_vec_length_def lessThan_atLeast0 by simp
  ultimately show ?thesis by auto
qed

(* 
Biblio:

@inproceedings{Boender2015FormalizationOQ,
  title={Formalization of Quantum Protocols using Coq},
  author={Jaap Boender and Florian Kamm{\"u}ller and Rajagopal Nagarajan},
  booktitle={QPL},
  year={2015}
}
*)

end