Theory Measurement

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

section ‹Measurement›

theory Measurement
imports
  Quantum
begin


text ‹
Given an element v  such that @{text "state n v"}, its components @{text "v $ i"} (when v is seen as 
a vector, v being a matrix column) for @{text "0 ≤ i < n"} have to be understood as the coefficients 
of the representation of v in the basis given by the unit vectors of dimension $2^n$, unless stated otherwise. 
Such a vector v is a state for a quantum system of n qubits.
In the literature on quantum computing, for $n = 1$, i.e. for a quantum system of 1 qubit, the elements
of the so-called computational basis are denoted $|0\rangle$,$|1\rangle$, and these last elements might be understood
for instance as $(1,0)$,$(0,1)$, i.e. as the zeroth and the first elements of a given basis ; for $n = 2$, 
i.e. for a quantum system of 2 qubits, the elements of the computational basis are denoted $|00\rangle$,
$|01\rangle$, $|10\rangle$,$|11\rangle$, and they might be understood for instance as $(1,0,0,0)$,
$(0,1,0,0)$, $(0,0,1,0)$, $(0,0,0,1)$; and so on for higher values of $n$. 
The idea behind these standard notations is that the labels on the vectors of the 
computational basis are the binary expressions of the natural numbers indexing the elements
in a given ordered basis interpreting the computational basis in a specific context, another point of
view is that the order of the basis corresponds to the lexicographic order for the labels. 
Those labels also represent the possible outcomes of a measurement of the $n$ qubits of the system, 
while the squared modules of the corresponding coefficients represent the probabilities for those 
outcomes. The fact that the vector v has to be normalized expresses precisely the fact that the squared 
modules of the coefficients represent some probabilities and hence their sum should be $1$.
Note that in the case of a system with multiple qubits, i.e. $n \geq 2$, one can model the simultaneous 
measurement of multiple qubits by sequential measurements of single qubits. Indeed, this last process
leads to the same probabilities for the various possible outcomes.
Given a system with n-qubits and i the index of one qubit among the $n$ qubits of the system, where
$0 \leq i \leq n-1$ (i.e. we start the indexing from $0$), we want to find the indices of the states of the
computational basis whose labels have a $1$ at the ith spot (counting from $0$). For instance, 
if $n=3$ and $i=2$ then $1$,$3$,$5$,$7$ are the indices of the elements of the computational basis 
with a $1$ at the 2nd spot, namely $|001\rangle$,$|011\rangle$,$|101\rangle$,$|111\rangle$. To achieve that we define the 
predicate @{term "select_index"} below.
›

definition select_index ::"nat ⇒ nat ⇒ nat ⇒ bool" where
"select_index n i j ≡ (i≤n-1) ∧ (j≤2^n - 1) ∧ (j mod 2^(n-i) ≥ 2^(n-1-i))"

lemma select_index_union:
  "{k| k::nat. select_index n i k} ∪ {k| k::nat. (k<2^n) ∧ ¬ select_index n i k} = {0..<2^n::nat}"
proof
  have "{k |k. select_index n i k} ⊆ {0..<2 ^ n}"
  proof
    fix x::nat assume "x ∈ {k |k. select_index n i k}"
    then show "x ∈ {0..<2^n}" 
      using select_index_def
      by (metis (no_types, lifting) atLeastLessThan_iff diff_diff_cancel diff_is_0_eq' diff_le_mono2 
le_less_linear le_numeral_extra(2) mem_Collect_eq one_le_numeral one_le_power select_index_def zero_order(1))
  qed
  moreover have "{k |k. k<2 ^ n ∧ ¬ select_index n i k} ⊆ {0..<2 ^ n}" by auto
  ultimately show "{k |k. select_index n i k} ∪ {k |k. k<2 ^ n ∧ ¬ select_index n i k} ⊆ {0..<2 ^ n}" by simp
next
  show "{0..<2 ^ n} ⊆ {k |k. select_index n i k} ∪ {k |k. k<2 ^ n ∧ ¬ select_index n i k}" by auto
qed

lemma select_index_inter:
  "{k| k::nat. select_index n i k} ∩ {k| k::nat. (k<2^n) ∧ ¬ select_index n i k} = {}" by auto

lemma outcomes_sum [simp]:
  fixes f :: "nat ⇒ real"
  shows
  "(∑j∈{k| k::nat. select_index n i k}. (f j)) + 
   (∑j∈{k| k::nat. (k<2^n) ∧ ¬ select_index n i k}. (f j)) = 
   (∑j∈{0..<2^n::nat}. (f j))"
proof -
  have "{k| k::nat. select_index n i k} ⊆ {0..<2^n::nat}"
    using select_index_union by blast
  then have "finite {k| k::nat. select_index n i k}"
    using rev_finite_subset by blast
  moreover have "{k| k::nat. (k<2^n) ∧ ¬ select_index n i k} ⊆ {0..<2^n::nat}"
    using select_index_union by blast
  then have "finite {k| k::nat. (k<2^n) ∧ ¬ select_index n i k}"
    using rev_finite_subset by blast
  ultimately have "(∑j∈{k| k::nat. select_index n i k}∪{k| k::nat. (k<2^n) ∧ ¬ select_index n i k}. (f j)) = 
           (∑j∈{k| k::nat. select_index n i k}. (f j)) + 
           (∑j∈{k| k::nat. (k<2^n) ∧ ¬ select_index n i k}. (f j)) -
           (∑j∈{k| k::nat. select_index n i k}∩{k| k::nat. (k<2^n) ∧ ¬ select_index n i k}. (f j))"
    using sum_Un by blast
  then have "(∑j∈{0..<2^n::nat}. (f j)) = 
                (∑j∈{k| k::nat. select_index n i k}. (f j)) + 
                (∑j∈{k| k::nat. (k<2^n) ∧ ¬ select_index n i k}. (f j)) -
                (∑j∈{}. (f j))"
    using select_index_union select_index_inter by simp
  thus ?thesis by simp
qed

text ‹
Given a state v of a n-qbit system, we compute the probability that a measure 
of qubit i has the outcome 1.
›

definition prob1 ::"nat ⇒ complex mat ⇒ nat ⇒ real" where
"prob1 n v i ≡ ∑j∈{k| k::nat. select_index n i k}. (cmod(v $$ (j,0)))⇧2"

definition prob0 ::"nat ⇒ complex mat ⇒ nat ⇒ real" where
"prob0 n v i ≡ ∑j∈{k| k::nat. (k<2^n) ∧ ¬ select_index n i k}. (cmod(v $$ (j,0)))⇧2"

lemma
  shows prob1_geq_zero:"prob1 n v i ≥ 0" and prob0_geq_zero:"prob0 n v i ≥ 0" 
proof -
  have "(∑j∈{k| k::nat. select_index n i k}. (cmod(v $$ (j,0)))⇧2) ≥ 
           (∑j∈{k| k::nat. select_index n i k}. (0::real))"
    by (simp add: sum_nonneg)
  then have "(∑j∈{k| k::nat. select_index n i k}. (cmod(v $$ (j,0)))⇧2) ≥ 0" by simp
  thus "prob1 n v i ≥ 0"
    using prob1_def by simp
next
  have "(∑j∈{k| k::nat. (k < 2 ^ n) ∧ ¬ select_index n i k}. (cmod(v $$ (j,0)))⇧2) ≥ 
           (∑j∈{k| k::nat. (k < 2 ^ n) ∧ ¬ select_index n i k}. (0::real))"
    by (simp add: sum_nonneg)
  then have "(∑j∈{k| k::nat. (k < 2 ^ n) ∧ ¬ select_index n i k}. (cmod(v $$ (j,0)))⇧2) ≥ 0" by simp
  thus "prob0 n v i ≥ 0"
    using prob0_def by simp
qed

lemma prob_sum_is_one [simp]:
  assumes "state n v"
  shows "prob1 n v i + prob0 n v i = 1"
proof-
  have "prob1 n v i + prob0 n v i = (∑j∈{0..<2^n::nat}. (cmod(v $$ (j,0)))⇧2)"
    using prob1_def prob0_def outcomes_sum by simp
  also have "… = ∥col v 0∥⇧2"
    using cpx_vec_length_def assms state_def atLeast0LessThan by fastforce
  finally show ?thesis 
    using assms state_def by simp
qed

lemma
  assumes "state n v"
  shows prob1_leq_one:"prob1 n v i ≤ 1" and prob0_leq_one:"prob0 n v i ≤ 1"
   apply(metis assms le_add_same_cancel1 prob0_geq_zero prob_sum_is_one)
  apply(metis assms le_add_same_cancel2 prob1_geq_zero prob_sum_is_one)
  done

lemma prob0_is_prob: 
  assumes "state n v"
  shows "prob0 n v i ≥ 0 ∧ prob0 n v i ≤ 1"
  by (simp add: assms prob0_geq_zero prob0_leq_one)

lemma prob1_is_prob: 
  assumes "state n v"
  shows "prob1 n v i ≥ 0 ∧ prob1 n v i ≤ 1"
  by (simp add: assms prob1_geq_zero prob1_leq_one)

text ‹Below we give the new state of a n-qubits system after a measurement of the ith qubit gave 0.›

definition post_meas0 ::"nat ⇒ complex mat ⇒ nat ⇒ complex mat" where
"post_meas0 n v i ≡ 
  of_real(1/sqrt(prob0 n v i)) ⋅⇩m |vec (2^n) (λj. if ¬ select_index n i j then v $$ (j,0) else 0)⟩"
 
text ‹
Note that a division by 0 never occurs. Indeed, if @{text "sqrt(prob0 n v i)"} would be 0 then 
@{text "prob0 n v i"} would be 0 and it would mean that the measurement of the ith qubit gave 1.
›

lemma post_meas0_is_state [simp]:
  assumes "state n v" and "prob0 n v i ≠ 0"
  shows "state n (post_meas0 n v i)" 
proof -
  have "(∑j∈{0..<2^n::nat}. (cmod (if ¬ select_index n i j then v $$ (j,0) else 0))⇧2) = 
           (∑j∈{k| k::nat. select_index n i k}. (cmod (if ¬ select_index n i j then v $$ (j,0) else 0))⇧2) +
           (∑j∈{k| k::nat. (k<2^n) ∧ ¬ select_index n i k}. (cmod (if ¬ select_index n i j then v $$ (j,0) else 0))⇧2)"
    using outcomes_sum[of "λj. (cmod (if ¬ select_index n i j then v $$ (j,0) else 0))⇧2" n i] by simp
  moreover have "(∑j∈{k| k::nat. (k<2^n) ∧ ¬ select_index n i k}. (cmod (if ¬ select_index n i j then v $$ (j,0) else 0))⇧2) = 
           prob0 n v i"
    by(simp add: prob0_def)
  ultimately have "∥vec (2 ^ n) (λj. if ¬ select_index n i j then v $$ (j,0) else 0)∥ = sqrt(prob0 n v i)"
    using lessThan_atLeast0 by (simp add: cpx_vec_length_def)
  moreover have "∥col (complex_of_real (1/sqrt (prob0 n v i)) ⋅⇩m |vec (2^n) (λj. if ¬ select_index n i j then v $$ (j,0) else 0)⟩) 0∥ = 
           (1/sqrt (prob0 n v i)) * ∥vec (2^n) (λj. if ¬ select_index n i j then v $$ (j,0) else 0)∥"
    using prob0_geq_zero smult_vec_length_bis by(metis (no_types, lifting) real_sqrt_ge_0_iff zero_le_divide_1_iff)
  ultimately show ?thesis
    using state_def post_meas0_def by (simp add: ket_vec_def post_meas0_def assms(2))
qed

text ‹Below we give the new state of a n-qubits system after a measurement of the ith qubit gave 1.›

definition post_meas1 ::"nat ⇒ complex mat ⇒ nat ⇒ complex mat" where
"post_meas1 n v i ≡ 
  of_real(1/sqrt(prob1 n v i)) ⋅⇩m |vec (2^n) (λj. if select_index n i j then v $$ (j,0) else 0)⟩"
 
text ‹
Note that a division by 0 never occurs. Indeed, if @{text "sqrt(prob1 n v i)"} would be 0 then 
@{text "prob1 n v i"} would be 0 and it would mean that the measurement of the ith qubit gave 0.
› 

lemma post_meas_1_is_state [simp]:
  assumes "state n v" and "prob1 n v i ≠ 0"
  shows "state n (post_meas1 n v i)"
proof -
  have "(∑j∈{0..<2^n::nat}. (cmod (if select_index n i j then v $$ (j,0) else 0))⇧2) = 
           (∑j∈{k| k::nat. select_index n i k}. (cmod (if select_index n i j then v $$ (j,0) else 0))⇧2) +
           (∑j∈{k| k::nat. (k<2^n) ∧ ¬ select_index n i k}. (cmod (if select_index n i j then v $$ (j,0) else 0))⇧2)"
    using outcomes_sum[of "λj. (cmod (if select_index n i j then v $$ (j,0) else 0))⇧2" n i] by simp
  then have "∥vec (2^n) (λj. if select_index n i j then v $$ (j,0) else 0)∥ = sqrt(prob1 n v i)"
    using lessThan_atLeast0 by (simp add: cpx_vec_length_def prob1_def)
  moreover have "∥col(complex_of_real (1/sqrt (prob1 n v i)) ⋅⇩m |vec (2^n) (λj. if select_index n i j then v $$ (j,0) else 0)⟩) 0∥ = 
           (1/sqrt(prob1 n v i)) * ∥vec (2^n) (λj. if select_index n i j then v $$ (j,0) else 0)∥"
    using prob1_geq_zero smult_vec_length_bis
    by (metis (no_types, lifting) real_sqrt_ge_0_iff zero_le_divide_1_iff)
  ultimately have "∥col(complex_of_real (1/sqrt (prob1 n v i)) ⋅⇩m |vec (2^n) (λj. if select_index n i j then v $$ (j,0) else 0)⟩) 0∥
= (1/sqrt(prob1 n v i)) * sqrt(prob1 n v i)" by simp
  thus ?thesis
    using state_def post_meas1_def by (simp add: ket_vec_def post_meas1_def assms(2))
qed

text ‹
The measurement operator below takes a number of qubits n, a state v of a n-qubits system, a number
i corresponding to the index (starting from 0) of one qubit among the n-qubits, and it computes a list 
whose first (resp. second) element is the pair made of the probability that the outcome of the measurement
of the ith qubit is 0 (resp. 1) and the corresponding post-measurement state of the system.
Of course, note that i should be strictly less than n and v should be a state of dimension n, i.e. 
state n v should hold".
›

definition meas ::"nat ⇒ complex mat ⇒ nat ⇒ _list" where
"meas n v i ≡ [(prob0 n v i, post_meas0 n v i), (prob1 n v i, post_meas1 n v i)]"

text ‹
We want to determine the probability that the first n qubits of an n+1 qubit system are 0. 
For this we need to find the indices of the states of the computational basis whose labels do 
not have a 1 at spot $i=0,...,n$.
›

definition prob0_fst_qubits:: "nat ⇒ complex Matrix.mat ⇒ real" where
"prob0_fst_qubits n v ≡ 
∑j∈{k| k::nat. (k<2^(n+1)) ∧ (∀i∈{0..<n}. ¬ select_index (n+1) i k)}. (cmod(v $$ (j,0)))⇧2"

lemma select_index_div_2:
  fixes n i j::"nat"
  assumes "i < 2^(n+1)" and "j<n"
  shows "select_index n j (i div 2) = select_index (n+1) j i"
proof-
  have "2^(n-Suc j) ≤ i div 2 mod 2^(n-j) ⟹ 2^(n-j) ≤ i mod 2^(n+1-j)"
  proof-
    define a::nat where a0:"a = i div 2 mod 2^(n-j)"
    assume "2^(n-Suc j) ≤ a"
    then have "2*a + i mod 2 ≥ 2^(n-(Suc j)+1)" by simp
    then have f0:"2*a + i mod 2 ≥ 2^(n-j)"
      by (metis Suc_diff_Suc Suc_eq_plus1 assms(2))
    have "a < 2^(n-j)" using a0 by simp
    then have "2*a + i mod 2 < 2*2^(n-j)" by linarith
    then have "2*a + i mod 2 < 2^(n-j+1)" by simp
    then have f1:"2*a + i mod 2 < 2^(n+1-j)"
      by (metis Nat.add_diff_assoc2 Suc_leD Suc_leI assms(2))
    have "i = 2*(a + 2^(n-j)*(i div 2 div 2^(n-j))) + i mod 2" using a0 by simp
    then have "i = 2*a + i mod 2 + 2^(n-j+1)*(i div 2 div 2^(n-j))" by simp
    then have "i = 2*a + i mod 2 + 2^(n+1-j)*(i div 2 div 2^(n-j))"
      by (metis Nat.add_diff_assoc2 Suc_leD Suc_leI assms(2))
    then have "i mod 2^(n+1-j) = 2*a + i mod 2"
      using f1 by (metis mod_if mod_mult_self2)
    then show "2^(n-j) ≤ i mod 2^(n+1-j)"
      using f0 by simp
  qed
  moreover have "2^(n-j) ≤ i mod 2^(n+1-j) ⟹ 2^(n-Suc j) ≤ i div 2 mod 2^(n-j)"
  proof-
    define a::nat where a0:"a = i div 2 mod 2^(n-j)"
    assume a1:"2^(n-j) ≤ i mod 2^(n+1-j)"
    have f0:"2^(n-j) = 2^(n-Suc j+1)"
      by (metis Suc_diff_Suc Suc_eq_plus1 assms(2))
    have "a < 2^(n-j)" using a0 by simp
    then have "2*a + i mod 2 < 2*2^(n-j)" by linarith
    then have "2*a + i mod 2 < 2^(n-j+1)" by simp
    then have f1:"2*a + i mod 2 < 2^(n+1-j)"
      by (metis Nat.add_diff_assoc2 Suc_leD Suc_leI assms(2))
    have "i = 2*(a + 2^(n-j)*(i div 2 div 2^(n-j))) + i mod 2" using a0 by simp
    then have "i = 2*a + i mod 2 + 2^(n-j+1)*(i div 2 div 2^(n-j))" by simp
    then have "i = 2*a + i mod 2 + 2^(n+1-j)*(i div 2 div 2^(n-j))"
      by (metis Nat.add_diff_assoc2 Suc_leD Suc_leI assms(2))
    then have "i mod 2^(n+1-j) = 2*a + i mod 2"
      using f1 by (metis mod_if mod_mult_self2)
    then have "2*a + i mod 2 ≥ 2^(n-j)"
      using a1 by simp
    then have "(2*a + i mod 2) div 2 ≥ (2^(n-j)) div 2"
      using div_le_mono by blast
    then show "2^(n-Suc j) ≤ a" by (simp add: f0)
  qed
  ultimately show ?thesis
    using select_index_def assms by auto
qed

lemma select_index_suc_even:
  fixes n k i:: nat
  assumes "k < 2^n" and "select_index n i k"
  shows "select_index (Suc n) i (2*k)"
proof-
  have "select_index n i k = select_index n i (2*k div 2)" by simp
  moreover have "… = select_index (Suc n) i (2*k)"
  proof-
    have "i < n" using assms(2) select_index_def
      by (metis (no_types, opaque_lifting) Suc_eq_plus1 assms(1) calculation diff_diff_left diff_le_self 
diff_self_eq_0 div_by_1 le_0_eq le_eq_less_or_eq less_imp_diff_less mod_div_trivial mult.left_neutral mult_eq_0_iff mult_le_mono1 not_less plus_1_eq_Suc power_0 semiring_normalization_rules(7))
    thus ?thesis
      using select_index_div_2 assms(1) select_index_def by(metis Suc_1 Suc_eq_plus1 Suc_mult_less_cancel1 power_Suc)
  qed
  ultimately show "select_index (Suc n) i (2*k)" 
    using assms(2) by simp
qed

lemma select_index_suc_odd:
  fixes n k i:: nat
  assumes "k ≤ 2^n -1" and "select_index n i k"
  shows "select_index (Suc n) i (2*k+1)"
proof-
  have "((2*k+1) mod 2^(Suc n - i) ≥ 2^(n - i)) =  
(((2*k+1) div 2) mod 2^(n - i) ≥ 2^(n-1-i))"
  proof-
    have "2*k+1 < 2^(n + 1)" 
      using assms(1)
      by (smt Suc_1 Suc_eq_plus1 Suc_le_lessD Suc_le_mono add_Suc_right distrib_left_numeral le_add_diff_inverse mult_le_mono2 nat_mult_1_right one_le_numeral one_le_power plus_1_eq_Suc power_add power_one_right)
    moreover have "i < n" 
      using assms(2) select_index_def
      by (metis (no_types, opaque_lifting) add_cancel_left_left add_diff_inverse_nat diff_le_self div_by_1 le_antisym less_le_trans less_one mod_div_trivial not_le power_0)
    ultimately show ?thesis
      using select_index_div_2[of "2*k+1" "n" i] select_index_def
      by (metis Nat.le_diff_conv2 Suc_eq_plus1 Suc_leI assms(2) diff_Suc_1 less_imp_le less_power_add_imp_div_less one_le_numeral one_le_power power_one_right)
  qed
  moreover have "… = (k mod 2^(n - i) ≥ 2^(n-1-i))" by simp
  ultimately show ?thesis
  proof-
    have "i ≤ Suc n -1" using assms(2) select_index_def by auto
    moreover have "2*k+1 ≤ 2^(Suc n)-1" 
      using assms(1) by (smt Suc_diff_1 Suc_eq_plus1 add_diff_cancel_right' diff_Suc_diff_eq2 diff_diff_left diff_is_0_eq diff_mult_distrib2 le_add2 mult_2 mult_Suc_right plus_1_eq_Suc pos2 power_Suc zero_less_power)
    ultimately show ?thesis
      using select_index_def
      by (metis ‹(2 ^ (n - 1 - i) ≤ (2 * k + 1) div 2 mod 2 ^ (n - i)) = (2 ^ (n - 1 - i) ≤ k mod 2 ^ (n - i))› ‹(2 ^ (n - i) ≤ (2 * k + 1) mod 2 ^ (Suc n - i)) = (2 ^ (n - 1 - i) ≤ (2 * k + 1) div 2 mod 2 ^ (n - i))› assms(2) diff_Suc_1)
  qed
qed

lemma aux_range:
  fixes k:: nat
  assumes "k < 2^(Suc n + 1)" and "k ≥ 2"
  shows "k = 2 ∨ k = 3 ∨ (∃l. l≥2 ∧ l≤2^(n+1)-1 ∧ (k = 2*l ∨ k = 2*l + 1))"
proof(rule disjCI)
  assume "¬ (k = 3 ∨ (∃l≥2. l ≤ 2^(n + 1) - 1 ∧ (k = 2 * l ∨ k = 2 * l + 1)))"
  have "k > 3 ⟶ (∃l≥2. l ≤ 2^(n + 1) - 1 ∧ (k = 2 * l ∨ k = 2 * l + 1))"
  proof
    assume asm:"k > 3"
    have "even k ∨ odd k" by simp
    then obtain l where "k = 2*l ∨ k = 2*l+1" by (meson evenE oddE)
    moreover have "l ≥ 2" 
      using asm calculation by linarith
    moreover have "l ≤ 2^(n+1) - 1" 
      using assms(1) by (metis Suc_diff_1 Suc_eq_plus1 calculation(1) dvd_triv_left even_Suc_div_two less_Suc_eq_le less_power_add_imp_div_less nonzero_mult_div_cancel_left pos2 power_one_right zero_less_power zero_neq_numeral)
    ultimately show "∃l≥2. l ≤ 2^(n + 1) - 1 ∧ (k = 2 * l ∨ k = 2 * l + 1)" by auto
  qed
  then have "k ≤ 2"
    using ‹¬ (k = 3 ∨ (∃l≥2. l ≤ 2 ^ (n + 1) - 1 ∧ (k = 2 * l ∨ k = 2 * l + 1)))› less_Suc_eq_le by auto
  thus "k = 2"
    using assms(2) by simp
qed

lemma select_index_with_1:
  fixes n:: nat
  assumes "n ≥ 1"
  shows "∀k. k < 2^(n+1) ⟶ k ≥ 2 ⟶ (∃i<n. select_index (n+1) i k)"
  using assms
proof(rule nat_induct_at_least)
  show "∀k< 2^(1+1). 2 ≤ k ⟶ (∃i<1. select_index (1+1) i k)"
  proof-
    have "select_index 2 0 2 = True" 
      using select_index_def by simp
    moreover have "select_index 2 0 3"
      using select_index_def by simp
    ultimately show ?thesis
      by (metis Suc_leI add_Suc_shift le_eq_less_or_eq mult_2 not_less one_add_one one_plus_numeral 
plus_1_eq_Suc power.simps(2) power_one_right semiring_norm(3) zero_less_one_class.zero_less_one)
  qed
next
  show "⋀n. 1 ≤ n ⟹
         ∀k < 2^(n+1). 2 ≤ k ⟶ (∃i<n. select_index (n+1) i k) ⟹
         ∀k < 2^(Suc n + 1). 2 ≤ k ⟶ (∃i<Suc n. select_index (Suc n +1) i k)"
  proof-
    fix n:: nat
    assume asm:"n ≥ 1" and IH:"∀k < 2^(n+1). 2 ≤ k ⟶ (∃i<n. select_index (n+1) i k)"
    have "select_index (Suc n + 1) n 2"
    proof-
      have "select_index (Suc n) n 1" 
        using select_index_def by(smt Suc_1 Suc_diff_Suc Suc_lessI add_diff_cancel_right' diff_Suc_1 
diff_commute diff_zero le_eq_less_or_eq less_Suc_eq_le nat.simps(3) nat_power_eq_Suc_0_iff 
one_mod_two_eq_one plus_1_eq_Suc power_one_right zero_less_power)
      thus ?thesis 
        using select_index_suc_even by (metis Suc_eq_plus1 less_numeral_extra(4) mult_2 not_less_less_Suc_eq one_add_one one_less_power zero_less_Suc)
    qed
    moreover have "select_index (Suc n + 1) n 3"
    proof-
      have "select_index (Suc n) n 1"
        using select_index_def by(smt Suc_1 Suc_diff_Suc Suc_lessI add_diff_cancel_right' diff_Suc_1 
diff_commute diff_zero le_eq_less_or_eq less_Suc_eq_le nat.simps(3) nat_power_eq_Suc_0_iff 
one_mod_two_eq_one plus_1_eq_Suc power_one_right zero_less_power)
      thus ?thesis 
        using select_index_suc_odd by (metis One_nat_def Suc_eq_plus1 mult_2 numeral_3_eq_3 select_index_def)
    qed
    moreover have "∃i<Suc n. select_index (Suc n +1) i (2*k)" if "k ≥ 2" and "k ≤ 2^(n + 1)-1" for k:: nat
    proof-
      obtain i where "i<n" and "select_index (n+1) i k" 
        using IH by(metis One_nat_def Suc_diff_Suc ‹2 ≤ k› ‹k ≤ 2 ^ (n + 1) - 1› diff_zero le_imp_less_Suc pos2 zero_less_power)
      then have "select_index (Suc n +1) i (2*k)"
        using select_index_suc_even
        by (metis One_nat_def Suc_diff_Suc add.commute diff_zero le_imp_less_Suc plus_1_eq_Suc pos2 that(2) zero_less_power)
      thus ?thesis
        using ‹i < n› less_SucI by blast
    qed
    moreover have "∃i<Suc n. select_index (Suc n +1) i (2*k +1)" if "k ≥ 2" and "k ≤ 2^(n + 1)-1" for k:: nat
    proof-
      obtain i where "i<n" and "select_index (n+1) i k" 
        using IH by(metis One_nat_def Suc_diff_Suc ‹2 ≤ k› ‹k ≤ 2 ^ (n + 1) - 1› diff_zero le_imp_less_Suc pos2 zero_less_power)
      then have "select_index (Suc n +1) i (2*k+1)"
        using select_index_suc_odd that(2) by simp
      thus ?thesis
        using ‹i < n› less_SucI by blast
    qed
    ultimately show "∀k< 2^(Suc n + 1). 2 ≤ k ⟶ (∃i<Suc n. select_index (Suc n +1) i k)"
      using aux_range by (metis lessI)
  qed
qed

lemma prob0_fst_qubits_index:
  fixes n:: nat and v:: "complex Matrix.mat"
  shows "{k| k::nat. (k<2^(n+1)) ∧ (∀i∈{0..<n}. ¬ select_index (n+1) i k)} = {0,1}"
proof(induct n)
  case 0
  show "{k |k. k < 2^(0+1) ∧ (∀i∈{0..<0}. ¬ select_index (0+1) i k)} = {0,1}" by auto
next
  case (Suc n)
  show "⋀n. {k |k. k < 2^(n+1) ∧ (∀i∈{0..<n}. ¬ select_index (n+1) i k)} = {0,1} ⟹
         {k |k. k < 2^(Suc n + 1) ∧ (∀i∈{0..<Suc n}. ¬ select_index (Suc n + 1) i k)} =
         {0, 1}"
  proof-
    fix n
    assume IH: "{k |k. k < 2^(n+1) ∧ (∀i∈{0..<n}. ¬ select_index (n+1) i k)} = {0,1}"
    then have "{0,1} ⊆ {k |k. k < 2^(Suc n + 1) ∧ (∀i∈{0..<Suc n}. ¬ select_index (Suc n + 1) i k)}"
    proof-
      have "k < 2^(n+1) ⟶ k < 2^(Suc n + 1)" for k::nat by simp
      moreover have "(∀i∈{0..<n}. ¬ select_index (n+1) i 0) ∧ (∀i∈{0..<n}. ¬ select_index (n+1) i 1)"
        using IH by auto
      then have "(∀i∈{0..<n}. ¬ select_index (Suc n +1) i 0) ∧ (∀i∈{0..<n}. ¬ select_index (Suc n +1) i 1)"
        using select_index_suc_odd[of 0 "n+1"] Suc_eq_plus1
        by (smt One_nat_def Suc_1 add_Suc_shift add_diff_cancel_right' atLeastLessThan_iff diff_diff_cancel 
le_eq_less_or_eq less_Suc_eq linorder_not_le mod_less nat_power_eq_Suc_0_iff select_index_def zero_less_power)
      moreover have "select_index (Suc n + 1) n 0 = False" using select_index_def by simp
      moreover have "select_index (Suc n + 1) n 1 = False" using select_index_def by simp
      ultimately show ?thesis
        by (smt One_nat_def Suc_1 Suc_eq_plus1 Suc_lessI atLeast0_lessThan_Suc empty_iff insertE 
mem_Collect_eq nat.simps(1) nat_power_eq_Suc_0_iff pos2 subsetI zero_less_power)
    qed
    moreover have "{k |k. k < 2^(Suc n + 1) ∧ (∀i∈{0..<Suc n}. ¬ select_index (Suc n + 1) i k)} ⊆ {0,1}"
    proof-
      have "∀k<2^(Suc n +1). k ≥ 2 ⟶ (∃i<Suc n. ¬ select_index (Suc n +1) i k = False)"
        using select_index_with_1[of "Suc n"] by (metis Suc_eq_plus1 add.commute le_add1)
      thus ?thesis by auto
    qed
    ultimately show "{k |k. k<2^(Suc n + 1) ∧ (∀i∈{0..<Suc n}. ¬ select_index (Suc n +1) i k)} = {0,1}" by auto
  qed
qed

lemma prob0_fst_qubits_eq:
  fixes n:: nat
  shows "prob0_fst_qubits n v = (cmod(v $$ (0,0)))⇧2 + (cmod(v $$ (1,0)))⇧2"
proof-
  have "prob0_fst_qubits n v = (∑j∈{k| k::nat. (k<2^(n+1)) ∧ (∀i∈{0..<n}. ¬ select_index (n+1) i k)}. (cmod(v $$ (j,0)))⇧2)"
    using prob0_fst_qubits_def by simp
  moreover have "… = (∑j∈{0,1}. (cmod(v $$ (j,0)))⇧2)"
    using prob0_fst_qubits_index by simp
  finally show ?thesis by simp
qed

(* Below in iter_post_meas0, the first argument n corresponds to the number of qubits of the system
, and the second argument m corresponds to the number of qubits that have been measured. *)
primrec iter_post_meas0:: "nat ⇒ nat ⇒ complex Matrix.mat ⇒ complex Matrix.mat" where
  "iter_post_meas0 n 0 v = v"
| "iter_post_meas0 n (Suc m) v = post_meas0 n (iter_post_meas0 n m v) m"

(* iter_prob0 outputs the probability that successive measurements of the first m qubits
(out of n qubits in the system) give m zeros. *)
definition iter_prob0:: "nat ⇒ nat ⇒ complex Matrix.mat ⇒ real" where 
  "iter_prob0 n m v = (∏i<m. prob0 n (iter_post_meas0 n i v) i)"

(* To do:
lemma iter_prob0_eq:
  fixes n:: nat and v:: "complex Matrix.mat"
  assumes "n ≥ 1"
  shows "iter_prob0 (Suc n) n v = prob0_fst_qubits n v"
*)

subsection ‹Measurements with Bell States›

text ‹
A Bell state is a remarkable state. Indeed, if one makes one measure, either of the first or the second 
qubit, then one gets either $0$ with probability $1/2$ or $1$ with probability $1/2$. Moreover, in the case of 
two successive measurements of the first and second qubit, the outcomes are correlated. 
Indeed, in the case of @{text "|β⇩0⇩0⟩"} or @{text "|β⇩1⇩0⟩"} (resp. @{text "|β⇩0⇩1⟩"} or @{text "|β⇩1⇩1⟩"}) if 
one measures the second qubit after a measurement of the first qubit (or the other way around) then 
one gets the same outcomes (resp. opposite outcomes), i.e. for instance the probability of measuring 
$0$ for the second qubit after a measure with outcome $0$ for the first qubit is $1$ (resp. $0$).
›

lemma prob0_bell_fst [simp]:
  assumes "v = |β⇩0⇩0⟩ ∨ v = |β⇩0⇩1⟩ ∨ v = |β⇩1⇩0⟩ ∨ v = |β⇩1⇩1⟩"
  shows "prob0 2 v 0 = 1/2" 
proof -
  have set_0 [simp]:"{k| k::nat. (k<4) ∧ ¬ select_index 2 0 k} = {0,1}"
    using select_index_def by auto
  have "v = |β⇩0⇩0⟩ ⟹ prob0 2 v 0 = 1/2"
  proof -
    fix v assume asm:"v = |β⇩0⇩0⟩"
    show "prob0 2 v 0 = 1/2"
    proof -
      have "prob0 2 v 0 = (∑j∈{k| k::nat. (k<4) ∧ ¬ select_index 2 0 k}. (cmod(bell00 $$ (j,0)))⇧2)"
        by (auto simp: prob0_def asm)
      also have "… = (∑j∈{0,1}. (cmod(bell00 $$ (j,0)))⇧2)"
        using set_0 by simp
      also have "… = (cmod(1/sqrt(2)))⇧2 + (cmod(0))⇧2"
        by (auto simp: bell00_def ket_vec_def)
      finally show  ?thesis by(simp add: cmod_def power_divide)
    qed
  qed
  moreover have "v = |β⇩0⇩1⟩ ⟹ prob0 2 v 0 = 1/2"
  proof -
    fix v assume asm:"v = |β⇩0⇩1⟩"
    show "prob0 2 v 0 = 1/2"
    proof -
      have "prob0 2 v 0 = (∑j∈{k| k::nat. (k<4) ∧ ¬ select_index 2 0 k}. (cmod(bell01 $$ (j,0)))⇧2)"
        by (auto simp: prob0_def asm)
      also have "… = (∑j∈{0,1}. (cmod(bell01 $$ (j,0)))⇧2)"
        using set_0 by simp
      also have "… = (cmod(0))⇧2 + (cmod(1/sqrt(2)))⇧2"
        by (auto simp: bell01_def ket_vec_def)
      finally show ?thesis by(simp add: cmod_def power_divide)
    qed
  qed
  moreover have "v = |β⇩1⇩0⟩ ⟹ prob0 2 v 0 = 1/2"
  proof -
    fix v assume asm:"v = |β⇩1⇩0⟩"
    show "prob0 2 v 0 = 1/2"
    proof -
      have "prob0 2 v 0 = (∑j∈{k| k::nat. (k<4) ∧ ¬ select_index 2 0 k}. (cmod(bell10 $$ (j,0)))⇧2)"
        by (auto simp: prob0_def asm)
      also have "… = (∑j∈{0,1}. (cmod(bell10 $$ (j,0)))⇧2)"
        using set_0 by simp
      also have "… = (cmod(1/sqrt(2)))⇧2 + (cmod(0))⇧2"
        by (auto simp: bell10_def ket_vec_def)
      finally show ?thesis by(simp add: cmod_def power_divide)
    qed
  qed
  moreover have "v = |β⇩1⇩1⟩ ⟹ prob0 2 v 0 = 1/2"
  proof -
    fix v assume asm:"v = |β⇩1⇩1⟩"
    show "prob0 2 v 0 = 1/2"
    proof -
      have "prob0 2 v 0 = (∑j∈{k| k::nat. (k<4) ∧ ¬ select_index 2 0 k}. (cmod(bell11 $$ (j,0)))⇧2)"
        by (auto simp: prob0_def asm)
      also have "… = (∑j∈{0,1}. (cmod(bell11 $$ (j,0)))⇧2)"
        using set_0 by simp
      also have "… = (cmod(0))⇧2 + (cmod(1/sqrt(2)))⇧2"
        by (auto simp: bell11_def ket_vec_def)
      finally show ?thesis by(simp add: cmod_def power_divide)
    qed
  qed
  ultimately show ?thesis using assms by auto
qed

lemma prob_1_bell_fst [simp]:
  assumes "v = |β⇩0⇩0⟩ ∨ v = |β⇩0⇩1⟩ ∨ v = |β⇩1⇩0⟩ ∨ v = |β⇩1⇩1⟩"
  shows "prob1 2 v 0 = 1/2" 
proof -
  have set_0 [simp]:"{k| k::nat. select_index 2 0 k} = {2,3}"
    using select_index_def by auto
  have "v = |β⇩0⇩0⟩ ⟹ prob1 2 v 0 = 1/2"
  proof -
    fix v assume asm:"v = |β⇩0⇩0⟩"
    show "prob1 2 v 0 = 1/2"
    proof -
      have "prob1 2 v 0 = (∑j∈{k| k::nat. select_index 2 0 k}. (cmod(bell00 $$ (j,0)))⇧2)"
        by (auto simp: prob1_def asm)
      also have "… = (∑j∈{2,3}. (cmod(bell00 $$ (j,0)))⇧2)"
        using set_0 by simp
      also have "… = (cmod(1/sqrt(2)))⇧2 + (cmod(0))⇧2"
        by (auto simp: bell00_def ket_vec_def)
      finally show ?thesis by(simp add: cmod_def power_divide)
    qed
  qed
  moreover have "v = |β⇩0⇩1⟩ ⟹ prob1 2 v 0 = 1/2"
  proof -
    fix v assume asm:"v = |β⇩0⇩1⟩"
    show "prob1 2 v 0 = 1/2"
    proof -
      have "prob1 2 v 0 = (∑j∈{k| k::nat. select_index 2 0 k}. (cmod(bell01 $$ (j,0)))⇧2)"
        by (auto simp: prob1_def asm)
      also have "… = (∑j∈{2,3}. (cmod(bell01 $$ (j,0)))⇧2)"
        using set_0 by simp
      also have "… = (cmod(0))⇧2 + (cmod(1/sqrt(2)))⇧2"
        by (auto simp: bell01_def ket_vec_def)
      finally show ?thesis by(simp add: cmod_def power_divide)
    qed
  qed
  moreover have "v = |β⇩1⇩0⟩ ⟹ prob1 2 v 0 = 1/2"
  proof -
    fix v assume asm:"v = |β⇩1⇩0⟩"
    show "prob1 2 v 0 = 1/2"
    proof -
      have "prob1 2 v 0 = (∑j∈{k| k::nat. select_index 2 0 k}. (cmod(bell10 $$ (j,0)))⇧2)"
        by (auto simp: prob1_def asm)
      also have "… = (∑j∈{2,3}. (cmod(bell10 $$ (j,0)))⇧2)"
        using set_0 by simp
      also have "… = (cmod(1/sqrt(2)))⇧2 + (cmod(0))⇧2"
        by (auto simp: bell10_def ket_vec_def)
      finally show ?thesis by(simp add: cmod_def power_divide)
    qed
  qed
  moreover have "v = |β⇩1⇩1⟩ ⟹ prob1 2 v 0 = 1/2"
  proof -
    fix v assume asm:"v = |β⇩1⇩1⟩"
    show "prob1 2 v 0 = 1/2"
    proof -
      have "prob1 2 v 0 = (∑j∈{k| k::nat. select_index 2 0 k}. (cmod(bell11 $$ (j,0)))⇧2)"
        by (auto simp: prob1_def asm)
      also have "… = (∑j∈{2,3}. (cmod(bell11 $$ (j,0)))⇧2)"
        using set_0 by simp
      also have "… = (cmod(0))⇧2 + (cmod(1/sqrt(2)))⇧2"
        by (auto simp: bell11_def ket_vec_def)
      finally show ?thesis by(simp add: cmod_def power_divide)
    qed
  qed
  ultimately show ?thesis using assms by auto
qed

lemma prob0_bell_snd [simp]:
  assumes "v = |β⇩0⇩0⟩ ∨ v = |β⇩0⇩1⟩ ∨ v = |β⇩1⇩0⟩ ∨ v = |β⇩1⇩1⟩"
  shows "prob0 2 v 1 = 1/2" 
proof -
  have set_0 [simp]:"{k| k::nat. (k<4) ∧ ¬ select_index 2 1 k} = {0,2}"
    by (auto simp: select_index_def)
      (metis Suc_le_mono add_Suc add_Suc_right le_numeral_extra(3) less_antisym mod_Suc_eq mod_less 
        neq0_conv not_mod2_eq_Suc_0_eq_0 numeral_2_eq_2 numeral_Bit0 one_add_one one_mod_two_eq_one one_neq_zero) 
  have "v = |β⇩0⇩0⟩ ⟹ prob0 2 v 1 = 1/2"
  proof -
    fix v assume asm:"v = |β⇩0⇩0⟩"
    show "prob0 2 v 1 = 1/2"
    proof -
      have "prob0 2 v 1 = (∑j∈{k| k::nat. (k<4) ∧ ¬ select_index 2 1 k}. (cmod(bell00 $$ (j,0)))⇧2)"
        by (auto simp: prob0_def asm)
      also have "… = (∑j∈{0,2}. (cmod(bell00 $$ (j,0)))⇧2)"
        using set_0 by simp
      also have "… = (cmod(1/sqrt(2)))⇧2 + (cmod(0))⇧2"
        by (auto simp: bell00_def ket_vec_def)
      finally show ?thesis by(simp add: cmod_def power_divide)
    qed
  qed
  moreover have "v = |β⇩0⇩1⟩ ⟹ prob0 2 v 1 = 1/2"
  proof -
    fix v assume asm:"v = |β⇩0⇩1⟩"
    show "prob0 2 v 1 = 1/2"
    proof -
      have "prob0 2 v 1 = (∑j∈{k| k::nat. (k<4) ∧ ¬ select_index 2 1 k}. (cmod(bell01 $$ (j,0)))⇧2)"
        by (auto simp: prob0_def asm)
      also have "… = (∑j∈{0,2}. (cmod(bell01 $$ (j,0)))⇧2)"
        using set_0 by simp
      also have "… = (cmod(0))⇧2 + (cmod(1/sqrt(2)))⇧2"
        by (auto simp: bell01_def ket_vec_def)
      finally show ?thesis by(simp add: cmod_def power_divide)
    qed
  qed
  moreover have "v = |β⇩1⇩0⟩ ⟹ prob0 2 v 1 = 1/2"
  proof -
    fix v assume asm:"v = |β⇩1⇩0⟩"
    show "prob0 2 v 1 = 1/2"
    proof -
      have "prob0 2 v 1 = (∑j∈{k| k::nat. (k<4) ∧ ¬ select_index 2 1 k}. (cmod(bell10 $$ (j,0)))⇧2)"
        by (auto simp: prob0_def asm)
      also have "… = (∑j∈{0,2}. (cmod(bell10 $$ (j,0)))⇧2)"
        using set_0 by simp
      also have "… = (cmod(1/sqrt(2)))⇧2 + (cmod(0))⇧2"
        by (auto simp: bell10_def ket_vec_def)
      finally show ?thesis by(simp add: cmod_def power_divide)
    qed
  qed
  moreover have "v = |β⇩1⇩1⟩ ⟹ prob0 2 v 1 = 1/2"
  proof -
    fix v assume asm:"v = |β⇩1⇩1⟩"
    show "prob0 2 v 1 = 1/2"
    proof -
      have "prob0 2 v 1 = (∑j∈{k| k::nat. (k<4) ∧ ¬ select_index 2 1 k}. (cmod(bell11 $$ (j,0)))⇧2)"
        by (auto simp: prob0_def asm)
      also have "… = (∑j∈{0,2}. (cmod(bell11 $$ (j,0)))⇧2)"
        using set_0 by simp
      also have "… = (cmod(0))⇧2 + (cmod(1/sqrt(2)))⇧2"
        by (auto simp: bell11_def ket_vec_def)
      finally show ?thesis by(simp add: cmod_def power_divide)
    qed
  qed
  ultimately show ?thesis using assms by auto
qed

lemma prob_1_bell_snd [simp]:
  assumes "v = |β⇩0⇩0⟩ ∨ v = |β⇩0⇩1⟩ ∨ v = |β⇩1⇩0⟩ ∨ v = |β⇩1⇩1⟩"
  shows "prob1 2 v 1 = 1/2" 
proof -
  have set_0:"{k| k::nat. select_index 2 1 k} = {1,3}"
    by (auto simp: select_index_def)
      (metis Suc_le_lessD le_SucE le_less mod2_gr_0 mod_less mod_self numeral_2_eq_2 numeral_3_eq_3)
  have "v = |β⇩0⇩0⟩ ⟹ prob1 2 v 1 = 1/2"
  proof -
    fix v assume asm:"v = |β⇩0⇩0⟩"
    show "prob1 2 v 1 = 1/2"
    proof -
      have "prob1 2 v 1 = (∑j∈{k| k::nat. select_index 2 1 k}. (cmod(bell00 $$ (j,0)))⇧2)"
        by (auto simp: prob1_def asm)
      also have "… = (∑j∈{1,3}. (cmod(bell00 $$ (j,0)))⇧2)"
        using set_0 by simp
      also have "… = (cmod(1/sqrt(2)))⇧2 + (cmod(0))⇧2"
        by (auto simp: bell00_def ket_vec_def)
      finally show ?thesis by(simp add: cmod_def power_divide)
    qed
  qed
  moreover have "v = |β⇩0⇩1⟩ ⟹ prob1 2 v 1 = 1/2"
  proof -
    fix v assume asm:"v = |β⇩0⇩1⟩"
    show "prob1 2 v 1 = 1/2"
    proof -
      have "prob1 2 v 1 = (∑j∈{k| k::nat. select_index 2 1 k}. (cmod(bell01 $$ (j,0)))⇧2)"
        by (auto simp: prob1_def asm)
      also have "… = (∑j∈{1,3}. (cmod(bell01 $$ (j,0)))⇧2)"
        using set_0 by simp
      also have "… = (cmod(0))⇧2 + (cmod(1/sqrt(2)))⇧2"
        by (auto simp: bell01_def ket_vec_def)
      finally show ?thesis by(simp add: cmod_def power_divide)
    qed
  qed
  moreover have "v = |β⇩1⇩0⟩ ⟹ prob1 2 v 1 = 1/2"
  proof -
    fix v assume asm:"v = |β⇩1⇩0⟩"
    show "prob1 2 v 1 = 1/2"
    proof -
      have "prob1 2 v 1 = (∑j∈{k| k::nat. select_index 2 1 k}. (cmod(bell10 $$ (j,0)))⇧2)"
        by (auto simp: prob1_def asm)
      also have "… = (∑j∈{1,3}. (cmod(bell10 $$ (j,0)))⇧2)"
        using set_0 by simp
      also have "… = (cmod(1/sqrt(2)))⇧2 + (cmod(0))⇧2"
        by (auto simp: bell10_def ket_vec_def)
      finally show ?thesis by(simp add: cmod_def power_divide)
    qed
  qed
  moreover have "v = |β⇩1⇩1⟩ ⟹ prob1 2 v 1 = 1/2"
  proof -
    fix v assume asm:"v = |β⇩1⇩1⟩"
    show "prob1 2 v 1 = 1/2"
    proof -
      have "prob1 2 v 1 = (∑j∈{k| k::nat. select_index 2 1 k}. (cmod(bell11 $$ (j,0)))⇧2)"
        by (auto simp: prob1_def asm)
      also have "… = (∑j∈{1,3}. (cmod(bell11 $$ (j,0)))⇧2)"
        using set_0 by simp
      also have "… = (cmod(0))⇧2 + (cmod(1/sqrt(2)))⇧2"
        by (auto simp: bell11_def ket_vec_def)
      finally show ?thesis by(simp add: cmod_def power_divide)
    qed
  qed
  ultimately show ?thesis using assms by auto
qed

lemma post_meas0_bell00_fst [simp]:
  "post_meas0 2 |β⇩0⇩0⟩ 0 = |unit_vec 4 0⟩"
proof
  fix i j::nat assume "i < dim_row |unit_vec 4 0⟩" and "j < dim_col |unit_vec 4 0⟩"
  then have "i ∈ {0,1,2,3}" and "j = 0"
    by(auto simp add: ket_vec_def)
  moreover have "post_meas0 2 |β⇩0⇩0⟩ 0 $$ (0,0) = |unit_vec 4 0⟩ $$ (0,0)"
    by(simp add: post_meas0_def unit_vec_def select_index_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas0 2 |β⇩0⇩0⟩ 0 $$ (1,0) = |unit_vec 4 0⟩ $$ (1,0)"
    by(simp add: post_meas0_def unit_vec_def select_index_def bell00_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas0 2 |β⇩0⇩0⟩ 0 $$ (2,0) = |unit_vec 4 0⟩ $$ (2,0)"
    by(simp add: post_meas0_def unit_vec_def select_index_def bell00_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas0 2 |β⇩0⇩0⟩ 0 $$ (3,0) = |unit_vec 4 0⟩ $$ (3,0)"
    by(simp add: post_meas0_def unit_vec_def select_index_def bell00_def ket_vec_def real_sqrt_divide) 
  ultimately show "post_meas0 2 |β⇩0⇩0⟩ 0 $$ (i,j) = |unit_vec 4 0⟩ $$ (i,j)" by auto
next
  show "dim_row (post_meas0 2 |β⇩0⇩0⟩ 0) = dim_row |unit_vec 4 0⟩"
    by(auto simp add: post_meas0_def ket_vec_def)
  show "dim_col (post_meas0 2 |β⇩0⇩0⟩ 0) = dim_col |unit_vec 4 0⟩"
    by(auto simp add: post_meas0_def ket_vec_def)
qed

lemma post_meas0_bell00_snd [simp]:
  "post_meas0 2 |β⇩0⇩0⟩ 1 = |unit_vec 4 0⟩"
proof
  fix i j::nat assume "i < dim_row |unit_vec 4 0⟩" and "j < dim_col |unit_vec 4 0⟩"
  then have "i ∈ {0,1,2,3}" and "j = 0" 
    by(auto simp add: ket_vec_def)
  moreover have "post_meas0 2 |β⇩0⇩0⟩ 1 $$ (0,0) = |unit_vec 4 0⟩ $$ (0,0)"
    by(simp add: post_meas0_def unit_vec_def select_index_def bell00_def ket_vec_def real_sqrt_divide del:One_nat_def)
  moreover have "post_meas0 2 |β⇩0⇩0⟩ 1 $$ (1,0) = |unit_vec 4 0⟩ $$ (1,0)"
    by(simp add: post_meas0_def unit_vec_def select_index_def bell00_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas0 2 |β⇩0⇩0⟩ 1 $$ (2,0) = |unit_vec 4 0⟩ $$ (2,0)"
    by(simp add: post_meas0_def unit_vec_def select_index_def bell00_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas0 2 |β⇩0⇩0⟩ 1 $$ (3,0) = |unit_vec 4 0⟩ $$ (3,0)"
    by(simp add: post_meas0_def unit_vec_def select_index_def bell00_def ket_vec_def real_sqrt_divide)
  ultimately show "post_meas0 2 |β⇩0⇩0⟩ 1 $$ (i,j) = |unit_vec 4 0⟩ $$ (i,j)" by auto
next
  show "dim_row (post_meas0 2 |β⇩0⇩0⟩ 1) = dim_row |unit_vec 4 0⟩"
    by(auto simp add: post_meas0_def ket_vec_def)
  show "dim_col (post_meas0 2 |β⇩0⇩0⟩ 1) = dim_col |unit_vec 4 0⟩"
    by(auto simp add: post_meas0_def ket_vec_def)
qed

lemma post_meas0_bell01_fst [simp]:
  "post_meas0 2 |β⇩0⇩1⟩ 0 = |unit_vec 4 1⟩"
proof
  fix i j::nat assume "i < dim_row |unit_vec 4 1⟩" and "j < dim_col |unit_vec 4 1⟩"
  then have "i ∈ {0,1,2,3}" and "j = 0" 
    by(auto simp add: ket_vec_def)
  moreover have "post_meas0 2 |β⇩0⇩1⟩ 0 $$ (0,0) = |unit_vec 4 1⟩ $$ (0,0)"
    by(simp add: post_meas0_def unit_vec_def select_index_def bell01_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas0 2 |β⇩0⇩1⟩ 0 $$ (1,0) = |unit_vec 4 1⟩ $$ (1,0)"
    by(simp add: post_meas0_def unit_vec_def select_index_def bell01_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas0 2 |β⇩0⇩1⟩ 0 $$ (2,0) = |unit_vec 4 1⟩ $$ (2,0)"
    by(simp add: post_meas0_def unit_vec_def select_index_def bell01_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas0 2 |β⇩0⇩1⟩ 0 $$ (3,0) = |unit_vec 4 1⟩ $$ (3,0)"
    by(simp add: post_meas0_def unit_vec_def select_index_def bell01_def ket_vec_def real_sqrt_divide)
  ultimately show "post_meas0 2 |β⇩0⇩1⟩ 0 $$ (i,j) = |unit_vec 4 1⟩ $$ (i,j)" by auto
next
  show "dim_row (post_meas0 2 |β⇩0⇩1⟩ 0) = dim_row |unit_vec 4 1⟩"
    by(auto simp add: post_meas0_def ket_vec_def)
  show "dim_col (post_meas0 2 |β⇩0⇩1⟩ 0) = dim_col |unit_vec 4 1⟩"
    by(auto simp add: post_meas0_def ket_vec_def)
qed

lemma post_meas0_bell01_snd [simp]:
  "post_meas0 2 |β⇩0⇩1⟩ 1 = |unit_vec 4 2⟩" 
proof
  fix i j::nat assume "i < dim_row |unit_vec 4 2⟩" and "j < dim_col |unit_vec 4 2⟩"
  then have "i ∈ {0,1,2,3}" and "j = 0" 
    by(auto simp add: ket_vec_def)
  moreover have "post_meas0 2 |β⇩0⇩1⟩ 1 $$ (0,0) = |unit_vec 4 2⟩ $$ (0,0)"
    by(simp add: post_meas0_def unit_vec_def select_index_def bell01_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas0 2 |β⇩0⇩1⟩ 1 $$ (1,0) = |unit_vec 4 2⟩ $$ (1,0)"
    by(simp add: post_meas0_def unit_vec_def select_index_def bell01_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas0 2 |β⇩0⇩1⟩ 1 $$ (2,0) = |unit_vec 4 2⟩ $$ (2,0)"
    by(simp add: post_meas0_def unit_vec_def select_index_def bell01_def ket_vec_def real_sqrt_divide del:One_nat_def)
  moreover have "post_meas0 2 |β⇩0⇩1⟩ 1 $$ (3,0) = |unit_vec 4 2⟩ $$ (3,0)"
    by(simp add: post_meas0_def unit_vec_def select_index_def bell01_def ket_vec_def real_sqrt_divide)
  ultimately show "post_meas0 2 |β⇩0⇩1⟩ 1 $$ (i,j) = |unit_vec 4 2⟩ $$ (i,j)" by auto
next
  show "dim_row (post_meas0 2 |β⇩0⇩1⟩ 1) = dim_row |unit_vec 4 2⟩"
    by(auto simp add: post_meas0_def ket_vec_def)
  show "dim_col (post_meas0 2 |β⇩0⇩1⟩ 1) = dim_col |unit_vec 4 2⟩"
    by(auto simp add: post_meas0_def ket_vec_def)
qed

lemma post_meas0_bell10_fst [simp]:
  "post_meas0 2 |β⇩1⇩0⟩ 0 = |unit_vec 4 0⟩" 
proof
  fix i j::nat assume "i < dim_row |unit_vec 4 0⟩" and "j < dim_col |unit_vec 4 0⟩"
  then have "i ∈ {0,1,2,3}" and "j = 0" 
    by(auto simp add: ket_vec_def)
  moreover have "post_meas0 2 |β⇩1⇩0⟩ 0 $$ (0,0) = |unit_vec 4 0⟩ $$ (0,0)"
    by(simp add: post_meas0_def unit_vec_def select_index_def bell10_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas0 2 |β⇩1⇩0⟩ 0 $$ (1,0) = |unit_vec 4 0⟩ $$ (1,0)"
    by(simp add: post_meas0_def unit_vec_def select_index_def bell10_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas0 2 |β⇩1⇩0⟩ 0 $$ (2,0) = |unit_vec 4 0⟩ $$ (2,0)"
    by(simp add: post_meas0_def unit_vec_def select_index_def bell10_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas0 2 |β⇩1⇩0⟩ 0 $$ (3,0) = |unit_vec 4 0⟩ $$ (3,0)"
    by(simp add: post_meas0_def unit_vec_def select_index_def bell10_def ket_vec_def real_sqrt_divide)
  ultimately show "post_meas0 2 |β⇩1⇩0⟩ 0 $$ (i,j) = |unit_vec 4 0⟩ $$ (i,j)" by auto
next
  show "dim_row (post_meas0 2 |β⇩1⇩0⟩ 0) = dim_row |unit_vec 4 0⟩"
    by(auto simp add: post_meas0_def ket_vec_def)
  show "dim_col (post_meas0 2 |β⇩1⇩0⟩ 0) = dim_col |unit_vec 4 0⟩"
    by(auto simp add: post_meas0_def ket_vec_def)
qed

lemma post_meas0_bell10_snd [simp]:
  "post_meas0 2 |β⇩1⇩0⟩ 1 = |unit_vec 4 0⟩" 
proof
  fix i j::nat assume "i < dim_row |unit_vec 4 0⟩" and "j < dim_col |unit_vec 4 0⟩"
  then have "i ∈ {0,1,2,3}" and "j = 0" 
    by(auto simp add: ket_vec_def)
  moreover have "post_meas0 2 |β⇩1⇩0⟩ 1 $$ (0,0) = |unit_vec 4 0⟩ $$ (0,0)"
    by(simp add: post_meas0_def unit_vec_def select_index_def bell10_def ket_vec_def real_sqrt_divide del:One_nat_def)
  moreover have "post_meas0 2 |β⇩1⇩0⟩ 1 $$ (1,0) = |unit_vec 4 0⟩ $$ (1,0)"
    by(simp add: post_meas0_def unit_vec_def select_index_def bell10_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas0 2 |β⇩1⇩0⟩ 1 $$ (2,0) = |unit_vec 4 0⟩ $$ (2,0)"
    by(simp add: post_meas0_def unit_vec_def select_index_def bell10_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas0 2 |β⇩1⇩0⟩ 1 $$ (3,0) = |unit_vec 4 0⟩ $$ (3,0)"
    by(simp add: post_meas0_def unit_vec_def select_index_def bell10_def ket_vec_def real_sqrt_divide)
  ultimately show "post_meas0 2 |β⇩1⇩0⟩ 1 $$ (i,j) = |unit_vec 4 0⟩ $$ (i,j)" by auto
next
  show "dim_row (post_meas0 2 |β⇩1⇩0⟩ 1) = dim_row |unit_vec 4 0⟩"
    by(auto simp add: post_meas0_def ket_vec_def)
  show "dim_col (post_meas0 2 |β⇩1⇩0⟩ 1) = dim_col |unit_vec 4 0⟩"
    by(auto simp add: post_meas0_def ket_vec_def)
qed

lemma post_meas0_bell11_fst [simp]:
  "post_meas0 2 |β⇩1⇩1⟩ 0 = |unit_vec 4 1⟩" 
proof
  fix i j::nat assume "i < dim_row |unit_vec 4 1⟩" and "j < dim_col |unit_vec 4 1⟩"
  then have "i ∈ {0,1,2,3}" and "j = 0"  
    by(auto simp add: ket_vec_def)
  moreover have "post_meas0 2 |β⇩1⇩1⟩ 0 $$ (0,0) = |unit_vec 4 1⟩ $$ (0,0)"
    by(simp add: post_meas0_def unit_vec_def select_index_def bell11_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas0 2 |β⇩1⇩1⟩ 0 $$ (1,0) = |unit_vec 4 1⟩ $$ (1,0)"
    by(simp add: post_meas0_def unit_vec_def select_index_def bell11_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas0 2 |β⇩1⇩1⟩ 0 $$ (2,0) = |unit_vec 4 1⟩ $$ (2,0)"
    by(simp add: post_meas0_def unit_vec_def select_index_def bell11_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas0 2 |β⇩1⇩1⟩ 0 $$ (3,0) = |unit_vec 4 1⟩ $$ (3,0)"
    by(simp add: post_meas0_def unit_vec_def select_index_def bell11_def ket_vec_def real_sqrt_divide)
  ultimately show "post_meas0 2 |β⇩1⇩1⟩ 0 $$ (i,j) = |unit_vec 4 1⟩ $$ (i,j)" by auto
next
  show "dim_row (post_meas0 2 |β⇩1⇩1⟩ 0) = dim_row |unit_vec 4 1⟩"
    by(auto simp add: post_meas0_def ket_vec_def)
  show "dim_col (post_meas0 2 |β⇩1⇩1⟩ 0) = dim_col |unit_vec 4 1⟩"
    by(auto simp add: post_meas0_def ket_vec_def)
qed

lemma post_meas0_bell11_snd [simp]:
  "post_meas0 2 |β⇩1⇩1⟩ 1 = - |unit_vec 4 2⟩" 
proof
  fix i j::nat assume "i < dim_row (- |unit_vec 4 2⟩)" and "j < dim_col (- |unit_vec 4 2⟩)"
  then have "i ∈ {0,1,2,3}" and "j = 0" 
    by(auto simp add: ket_vec_def)
  moreover have "post_meas0 2 |β⇩1⇩1⟩ 1 $$ (0,0) = (- |unit_vec 4 2⟩) $$ (0,0)"
    by(simp add: post_meas0_def unit_vec_def select_index_def bell11_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas0 2 |β⇩1⇩1⟩ 1 $$ (1,0) = (- |unit_vec 4 2⟩) $$ (1,0)"
    by(simp add: post_meas0_def unit_vec_def select_index_def bell11_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas0 2 |β⇩1⇩1⟩ 1 $$ (2,0) = (- |unit_vec 4 2⟩) $$ (2,0)"
    by(simp add: post_meas0_def unit_vec_def select_index_def bell11_def ket_vec_def real_sqrt_divide del:One_nat_def)
  moreover have "post_meas0 2 |β⇩1⇩1⟩ 1 $$ (3,0) = (- |unit_vec 4 2⟩) $$ (3,0)"
    by(simp add: post_meas0_def unit_vec_def select_index_def bell11_def ket_vec_def real_sqrt_divide)
  ultimately show "post_meas0 2 |β⇩1⇩1⟩ 1 $$ (i,j) = (- |unit_vec 4 2⟩) $$ (i,j)" by auto
next
  show "dim_row (post_meas0 2 |β⇩1⇩1⟩ 1) = dim_row (- |unit_vec 4 2⟩)"
    by(auto simp add: post_meas0_def ket_vec_def)
  show "dim_col (post_meas0 2 |β⇩1⇩1⟩ 1) = dim_col (- |unit_vec 4 2⟩)"
    by(auto simp add: post_meas0_def ket_vec_def)
qed

lemma post_meas1_bell00_fst [simp]:
  "post_meas1 2 |β⇩0⇩0⟩ 0 = |unit_vec 4 3⟩" 
proof
  fix i j::nat assume "i < dim_row |unit_vec 4 3⟩" and "j < dim_col |unit_vec 4 3⟩"
  then have "i ∈ {0,1,2,3}" and "j = 0"  
    by(auto simp add: ket_vec_def)
  moreover have "post_meas1 2 |β⇩0⇩0⟩ 0 $$ (0,0) = |unit_vec 4 3⟩ $$ (0,0)"
    by(simp add: post_meas1_def unit_vec_def select_index_def bell00_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas1 2 |β⇩0⇩0⟩ 0 $$ (1,0) = |unit_vec 4 3⟩ $$ (1,0)"
    by(simp add: post_meas1_def unit_vec_def select_index_def bell00_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas1 2 |β⇩0⇩0⟩ 0 $$ (2,0) = |unit_vec 4 3⟩ $$ (2,0)"
    by(simp add: post_meas1_def unit_vec_def select_index_def bell00_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas1 2 |β⇩0⇩0⟩ 0 $$ (3,0) = |unit_vec 4 3⟩ $$ (3,0)"
    by(simp add: post_meas1_def unit_vec_def select_index_def bell00_def ket_vec_def real_sqrt_divide)
  ultimately show "post_meas1 2 |β⇩0⇩0⟩ 0 $$ (i,j) = |unit_vec 4 3⟩ $$ (i,j)" by auto
next
  show "dim_row (post_meas1 2 |β⇩0⇩0⟩ 0) = dim_row |unit_vec 4 3⟩"
    by(auto simp add: post_meas1_def ket_vec_def)
  show "dim_col (post_meas1 2 |β⇩0⇩0⟩ 0) = dim_col |unit_vec 4 3⟩"
    by(auto simp add: post_meas1_def ket_vec_def)
qed

lemma post_meas1_bell00_snd [simp]:
  "post_meas1 2 |β⇩0⇩0⟩ 1 = |unit_vec 4 3⟩" 
proof
  fix i j::nat assume "i < dim_row |unit_vec 4 3⟩" and "j < dim_col |unit_vec 4 3⟩"
  then have "i ∈ {0,1,2,3}" and "j = 0" 
    by(auto simp add: ket_vec_def)
  moreover have "post_meas1 2 |β⇩0⇩0⟩ 1 $$ (0,0) = |unit_vec 4 3⟩ $$ (0,0)"
    by(simp add: post_meas1_def unit_vec_def select_index_def bell00_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas1 2 |β⇩0⇩0⟩ 1 $$ (1,0) = |unit_vec 4 3⟩ $$ (1,0)"
    by(simp add: post_meas1_def unit_vec_def select_index_def bell00_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas1 2 |β⇩0⇩0⟩ 1 $$ (2,0) = |unit_vec 4 3⟩ $$ (2,0)"
    by(simp add: post_meas1_def unit_vec_def select_index_def bell00_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas1 2 |β⇩0⇩0⟩ 1 $$ (3,0) = |unit_vec 4 3⟩ $$ (3,0)"
    by(simp add: post_meas1_def unit_vec_def select_index_def bell00_def ket_vec_def real_sqrt_divide del: One_nat_def)
  ultimately show "post_meas1 2 |β⇩0⇩0⟩ 1 $$ (i,j) = |unit_vec 4 3⟩ $$ (i,j)" by auto
next
  show "dim_row (post_meas1 2 |β⇩0⇩0⟩ 1) = dim_row |unit_vec 4 3⟩"
    by(auto simp add: post_meas1_def ket_vec_def)
  show "dim_col (post_meas1 2 |β⇩0⇩0⟩ 1) = dim_col |unit_vec 4 3⟩"
    by(auto simp add: post_meas1_def ket_vec_def)
qed

lemma post_meas1_bell01_fst [simp]:
  "post_meas1 2 |β⇩0⇩1⟩ 0 = |unit_vec 4 2⟩" 
proof
  fix i j::nat assume "i < dim_row |unit_vec 4 2⟩" and "j < dim_col |unit_vec 4 2⟩"
  then have "i ∈ {0,1,2,3}" and "j = 0" 
    by(auto simp add: ket_vec_def)
  moreover have "post_meas1 2 |β⇩0⇩1⟩ 0 $$ (0,0) = |unit_vec 4 2⟩ $$ (0,0)"
    by(simp add: post_meas1_def unit_vec_def select_index_def bell01_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas1 2 |β⇩0⇩1⟩ 0 $$ (1,0) = |unit_vec 4 2⟩ $$ (1,0)"
    by(simp add: post_meas1_def unit_vec_def select_index_def bell01_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas1 2 |β⇩0⇩1⟩ 0 $$ (2,0) = |unit_vec 4 2⟩ $$ (2,0)"
    by(simp add: post_meas1_def unit_vec_def select_index_def bell01_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas1 2 |β⇩0⇩1⟩ 0 $$ (3,0) = |unit_vec 4 2⟩ $$ (3,0)"
    by(simp add: post_meas1_def unit_vec_def select_index_def bell01_def ket_vec_def real_sqrt_divide)
  ultimately show "post_meas1 2 |β⇩0⇩1⟩ 0 $$ (i,j) = |unit_vec 4 2⟩ $$ (i,j)" by auto
next
  show "dim_row (post_meas1 2 |β⇩0⇩1⟩ 0) = dim_row |unit_vec 4 2⟩"
    by(auto simp add: post_meas1_def ket_vec_def)
  show "dim_col (post_meas1 2 |β⇩0⇩1⟩ 0) = dim_col |unit_vec 4 2⟩"
    by(auto simp add: post_meas1_def ket_vec_def)
qed

lemma post_meas1_bell01_snd [simp]:
  "post_meas1 2 |β⇩0⇩1⟩ 1 = |unit_vec 4 1⟩" 
proof
  fix i j::nat assume "i < dim_row |unit_vec 4 1⟩" and "j < dim_col |unit_vec 4 1⟩"
  then have "i ∈ {0,1,2,3}" and "j = 0" 
    by(auto simp add: ket_vec_def)
  moreover have "post_meas1 2 |β⇩0⇩1⟩ 1 $$ (0,0) = |unit_vec 4 1⟩ $$ (0,0)"
    by(simp add: post_meas1_def unit_vec_def select_index_def bell01_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas1 2 |β⇩0⇩1⟩ 1 $$ (1,0) = |unit_vec 4 1⟩ $$ (1,0)"
    by(simp add: post_meas1_def unit_vec_def select_index_def bell01_def ket_vec_def real_sqrt_divide del: One_nat_def)
  moreover have "post_meas1 2 |β⇩0⇩1⟩ 1 $$ (2,0) = |unit_vec 4 1⟩ $$ (2,0)"
    by(simp add: post_meas1_def unit_vec_def select_index_def bell01_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas1 2 |β⇩0⇩1⟩ 1 $$ (3,0) = |unit_vec 4 1⟩ $$ (3,0)"
    by(simp add: post_meas1_def unit_vec_def select_index_def bell01_def ket_vec_def real_sqrt_divide)
  ultimately show "post_meas1 2 |β⇩0⇩1⟩ 1 $$ (i,j) = |unit_vec 4 1⟩ $$ (i,j)" by auto
next
  show "dim_row (post_meas1 2 |β⇩0⇩1⟩ 1) = dim_row |unit_vec 4 1⟩"
    by(auto simp add: post_meas1_def ket_vec_def)
  show "dim_col (post_meas1 2 |β⇩0⇩1⟩ 1) = dim_col |unit_vec 4 1⟩"
    by(auto simp add: post_meas1_def ket_vec_def)
qed

lemma post_meas1_bell10_fst [simp]:
  "post_meas1 2 |β⇩1⇩0⟩ 0 = - |unit_vec 4 3⟩" 
proof
  fix i j::nat assume "i < dim_row (- |unit_vec 4 3⟩)" and "j < dim_col (- |unit_vec 4 3⟩)"
  then have "i ∈ {0,1,2,3}" and "j = 0" 
    by(auto simp add: ket_vec_def)
  moreover have "post_meas1 2 |β⇩1⇩0⟩ 0 $$ (0,0) = (- |unit_vec 4 3⟩) $$ (0,0)"
    by(simp add: post_meas1_def unit_vec_def select_index_def bell10_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas1 2 |β⇩1⇩0⟩ 0 $$ (1,0) = (- |unit_vec 4 3⟩) $$ (1,0)"
    by(simp add: post_meas1_def unit_vec_def select_index_def bell10_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas1 2 |β⇩1⇩0⟩ 0 $$ (2,0) = (- |unit_vec 4 3⟩) $$ (2,0)"
    by(simp add: post_meas1_def unit_vec_def select_index_def bell10_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas1 2 |β⇩1⇩0⟩ 0 $$ (3,0) = (- |unit_vec 4 3⟩) $$ (3,0)"
    by(simp add: post_meas1_def unit_vec_def select_index_def bell10_def ket_vec_def real_sqrt_divide)
  ultimately show "post_meas1 2 |β⇩1⇩0⟩ 0 $$ (i,j) = (- |unit_vec 4 3⟩) $$ (i,j)" by auto
next
  show "dim_row (post_meas1 2 |β⇩1⇩0⟩ 0) = dim_row (- |unit_vec 4 3⟩)"
    by(auto simp add: post_meas1_def ket_vec_def)
  show "dim_col (post_meas1 2 |β⇩1⇩0⟩ 0) = dim_col (- |unit_vec 4 3⟩)"
    by(auto simp add: post_meas1_def ket_vec_def)
qed

lemma post_meas1_bell10_snd [simp]:
  "post_meas1 2 |β⇩1⇩0⟩ 1 = - |unit_vec 4 3⟩" 
proof
  fix i j::nat assume "i < dim_row (- |unit_vec 4 3⟩)" and "j < dim_col (- |unit_vec 4 3⟩)"
  then have "i ∈ {0,1,2,3}" and "j = 0" 
    by(auto simp add: ket_vec_def)
  moreover have "post_meas1 2 |β⇩1⇩0⟩ 1 $$ (0,0) = (- |unit_vec 4 3⟩) $$ (0,0)"
    by(simp add: post_meas1_def unit_vec_def select_index_def bell10_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas1 2 |β⇩1⇩0⟩ 1 $$ (1,0) = (- |unit_vec 4 3⟩) $$ (1,0)"
    by(simp add: post_meas1_def unit_vec_def select_index_def bell10_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas1 2 |β⇩1⇩0⟩ 1 $$ (2,0) = (- |unit_vec 4 3⟩) $$ (2,0)"
    by(simp add: post_meas1_def unit_vec_def select_index_def bell10_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas1 2 |β⇩1⇩0⟩ 1 $$ (3,0) = (- |unit_vec 4 3⟩) $$ (3,0)"
    by(simp add: post_meas1_def unit_vec_def select_index_def bell10_def ket_vec_def real_sqrt_divide del: One_nat_def)
  ultimately show "post_meas1 2 |β⇩1⇩0⟩ 1 $$ (i,j) = (- |unit_vec 4 3⟩) $$ (i,j)" by auto    
next
  show "dim_row (post_meas1 2 |β⇩1⇩0⟩ 1) = dim_row (- |unit_vec 4 3⟩)"
    by(auto simp add: post_meas1_def ket_vec_def)
  show "dim_col (post_meas1 2 |β⇩1⇩0⟩ 1) = dim_col (- |unit_vec 4 3⟩)"
    by(auto simp add: post_meas1_def ket_vec_def)
qed

lemma post_meas1_bell11_fst [simp]:
  "post_meas1 2 |β⇩1⇩1⟩ 0 = - |unit_vec 4 2⟩" 
proof
  fix i j::nat assume "i < dim_row (- |unit_vec 4 2⟩)" and "j < dim_col (- |unit_vec 4 2⟩)"
  then have "i ∈ {0,1,2,3}" and "j = 0" 
    by(auto simp add: ket_vec_def)
  moreover have "post_meas1 2 |β⇩1⇩1⟩ 0 $$ (0,0) = (- |unit_vec 4 2⟩) $$ (0,0)"
    by(simp add: post_meas1_def unit_vec_def select_index_def bell11_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas1 2 |β⇩1⇩1⟩ 0 $$ (1,0) = (- |unit_vec 4 2⟩) $$ (1,0)"
    by(simp add: post_meas1_def unit_vec_def select_index_def bell11_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas1 2 |β⇩1⇩1⟩ 0 $$ (2,0) = (- |unit_vec 4 2⟩) $$ (2,0)"
    by(simp add: post_meas1_def unit_vec_def select_index_def bell11_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas1 2 |β⇩1⇩1⟩ 0 $$ (3,0) = (- |unit_vec 4 2⟩) $$ (3,0)"
    by(simp add: post_meas1_def unit_vec_def select_index_def bell11_def ket_vec_def real_sqrt_divide)
  ultimately show "post_meas1 2 |β⇩1⇩1⟩ 0 $$ (i,j) = (- |unit_vec 4 2⟩) $$ (i,j)" by auto    
next
  show "dim_row (post_meas1 2 |β⇩1⇩1⟩ 0) = dim_row (- |unit_vec 4 2⟩)"
    by(auto simp add: post_meas1_def ket_vec_def)
  show "dim_col (post_meas1 2 |β⇩1⇩1⟩ 0) = dim_col (- |unit_vec 4 2⟩)"
    by(auto simp add: post_meas1_def ket_vec_def)
qed

lemma post_meas1_bell11_snd [simp]:
  "post_meas1 2 |β⇩1⇩1⟩ 1 = |unit_vec 4 1⟩" 
proof
  fix i j::nat assume "i < dim_row |unit_vec 4 1⟩" and "j < dim_col |unit_vec 4 1⟩"
  then have "i ∈ {0,1,2,3}" and "j = 0"  
    by(auto simp add: ket_vec_def)
  moreover have "post_meas1 2 |β⇩1⇩1⟩ 1 $$ (0,0) = |unit_vec 4 1⟩ $$ (0,0)"
    by(simp add: post_meas1_def unit_vec_def select_index_def bell11_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas1 2 |β⇩1⇩1⟩ 1 $$ (1,0) = |unit_vec 4 1⟩ $$ (1,0)"
    by(simp add: post_meas1_def unit_vec_def select_index_def bell11_def ket_vec_def real_sqrt_divide del: One_nat_def)
  moreover have "post_meas1 2 |β⇩1⇩1⟩ 1 $$ (2,0) = |unit_vec 4 1⟩ $$ (2,0)"
    by(simp add: post_meas1_def unit_vec_def select_index_def bell11_def ket_vec_def real_sqrt_divide)
  moreover have "post_meas1 2 |β⇩1⇩1⟩ 1 $$ (3,0) = |unit_vec 4 1⟩ $$ (3,0)"
    by(simp add: post_meas1_def unit_vec_def select_index_def bell11_def ket_vec_def real_sqrt_divide)
  ultimately show "post_meas1 2 |β⇩1⇩1⟩ 1 $$ (i,j) = |unit_vec 4 1⟩ $$ (i,j)" by auto
next
  show "dim_row (post_meas1 2 |β⇩1⇩1⟩ 1) = dim_row |unit_vec 4 1⟩"
    by(auto simp add: post_meas1_def ket_vec_def)
  show "dim_col (post_meas1 2 |β⇩1⇩1⟩ 1) = dim_col |unit_vec 4 1⟩"
    by(auto simp add: post_meas1_def ket_vec_def)
qed

end