Theory Deutsch

(*
Authors: 

  Hanna Lachnitt, TU Wien, lachnitt@student.tuwien.ac.at
  Anthony Bordg, University of Cambridge, apdb3@cam.ac.uk
*)

section ‹The Deutsch Algorithm›

theory Deutsch
imports
  More_Tensor
  Measurement
begin


text ‹
Given a function $f:{0,1}\mapsto {0,1}$, Deutsch's algorithm decides if this function is constant
or balanced with a single $f(x)$ circuit to evaluate the function for multiple values of $x$ 
simultaneously. The algorithm makes use of quantum parallelism and quantum interference.
›
                                   
text ‹
A constant function with values in {0,1} returns either always 0 or always 1. 
A balanced function is 0 for half of the inputs and 1 for the other half. 
›

locale deutsch =
  fixes f:: "nat ⇒ nat" 
  assumes dom: "f ∈ ({0,1} →⇩E {0,1})"

context deutsch
begin

definition is_swap:: bool where
"is_swap = (∀x ∈ {0,1}. f x = 1 - x)"

lemma is_swap_values:
  assumes "is_swap"
  shows "f 0 = 1" and "f 1 = 0" 
  using assms is_swap_def by auto

lemma is_swap_sum_mod_2:
  assumes "is_swap"
  shows "(f 0 + f 1) mod 2 = 1"
  using assms is_swap_def by simp

definition const:: "nat ⇒ bool" where 
"const n = (∀x ∈ {0,1}.(f x = n))"

definition is_const:: "bool" where 
"is_const ≡ const 0 ∨ const 1"

definition is_balanced:: "bool" where
"is_balanced ≡ (∀x ∈ {0,1}.(f x = x)) ∨ is_swap"

lemma f_values: "(f 0 = 0 ∨ f 0 = 1) ∧ (f 1 = 0 ∨ f 1 = 1)" 
  using dom by auto
 
lemma f_cases:
  shows "is_const ∨ is_balanced"   
  using dom is_balanced_def const_def is_const_def is_swap_def f_values by auto

lemma const_0_sum_mod_2:
  assumes "const 0"
  shows "(f 0 + f 1) mod 2 = 0"
  using assms const_def by simp

lemma const_1_sum_mod_2:
  assumes "const 1"
  shows "(f 0 + f 1) mod 2 = 0"
  using assms const_def by simp

lemma is_const_sum_mod_2:
  assumes "is_const"
  shows "(f 0 + f 1) mod 2 = 0"
  using assms is_const_def const_0_sum_mod_2 const_1_sum_mod_2 by auto

lemma id_sum_mod_2:
  assumes "f = id"
  shows "(f 0 + f 1) mod 2 = 1"
  using assms by simp

lemma is_balanced_sum_mod_2:
  assumes "is_balanced"
  shows "(f 0 + f 1) mod 2 = 1"
  using assms is_balanced_def id_sum_mod_2 is_swap_sum_mod_2 by auto

lemma f_ge_0: "∀ x. (f x ≥ 0)" by simp

end (* context deutsch *)

text ‹The Deutsch's Transform @{text U⇩f}.›

definition (in deutsch) deutsch_transform:: "complex Matrix.mat" ("U⇩f") where 
"U⇩f ≡ mat_of_cols_list 4 [[1 - f(0), f(0), 0, 0],
                          [f(0), 1 - f(0), 0, 0],
                          [0, 0, 1 - f(1), f(1)],
                          [0, 0, f(1), 1 - f(1)]]"

lemma (in deutsch) deutsch_transform_dim [simp]: 
  shows "dim_row U⇩f = 4" and "dim_col U⇩f = 4" 
  by (auto simp add: deutsch_transform_def mat_of_cols_list_def)

lemma (in deutsch) deutsch_transform_coeff_is_zero [simp]: 
  shows "U⇩f $$ (0,2) = 0" and "U⇩f $$ (0,3) = 0"
    and "U⇩f $$ (1,2) = 0" and "U⇩f $$(1,3) = 0"
    and "U⇩f $$ (2,0) = 0" and "U⇩f $$(2,1) = 0"
    and "U⇩f $$ (3,0) = 0" and "U⇩f $$ (3,1) = 0"
  using deutsch_transform_def by auto

lemma (in deutsch) deutsch_transform_coeff [simp]: 
  shows "U⇩f $$ (0,1) = f(0)" and "U⇩f $$ (1,0) = f(0)"
    and "U⇩f $$(2,3) = f(1)" and "U⇩f $$ (3,2) = f(1)"
    and "U⇩f $$ (0,0) = 1 - f(0)" and "U⇩f $$(1,1) = 1 - f(0)"
    and "U⇩f $$ (2,2) = 1 - f(1)" and "U⇩f $$ (3,3) = 1 - f(1)"
  using deutsch_transform_def by auto

abbreviation (in deutsch) V⇩f:: "complex Matrix.mat" where
"V⇩f ≡ Matrix.mat 4 4 (λ(i,j). 
                if i=0 ∧ j=0 then 1 - f(0) else
                  (if i=0 ∧ j=1 then f(0) else
                    (if i=1 ∧ j=0 then f(0) else
                      (if i=1 ∧ j=1 then 1 - f(0) else
                        (if i=2 ∧ j=2 then 1 - f(1) else
                          (if i=2 ∧ j=3 then f(1) else
                            (if i=3 ∧ j=2 then f(1) else
                              (if i=3 ∧ j=3 then 1 - f(1) else 0))))))))"

lemma (in deutsch) deutsch_transform_alt_rep_coeff_is_zero [simp]:
  shows "V⇩f $$ (0,2) = 0" and "V⇩f $$ (0,3) = 0"
    and "V⇩f $$ (1,2) = 0" and "V⇩f $$(1,3) = 0"
    and "V⇩f $$ (2,0) = 0" and "V⇩f $$(2,1) = 0"
    and "V⇩f $$ (3,0) = 0" and "V⇩f $$ (3,1) = 0"
  by auto

lemma (in deutsch) deutsch_transform_alt_rep_coeff [simp]:
  shows "V⇩f $$ (0,1) = f(0)" and "V⇩f $$ (1,0) = f(0)"
    and "V⇩f $$(2,3) = f(1)" and "V⇩f $$ (3,2) = f(1)"
    and "V⇩f $$ (0,0) = 1 - f(0)" and "V⇩f $$(1,1) = 1 - f(0)"
    and "V⇩f $$ (2,2) = 1 - f(1)" and "V⇩f $$ (3,3) = 1 - f(1)"
  by auto

lemma (in deutsch) deutsch_transform_alt_rep:
  shows "U⇩f = V⇩f"
proof
  show c0:"dim_row U⇩f = dim_row V⇩f" by simp
  show c1:"dim_col U⇩f = dim_col V⇩f" by simp
  fix i j:: nat
  assume "i < dim_row V⇩f" and "j < dim_col V⇩f"
  then have "i < 4" and "j < 4" by auto
  thus "U⇩f $$ (i,j) = V⇩f $$ (i,j)"
    by (smt deutsch_transform_alt_rep_coeff deutsch_transform_alt_rep_coeff_is_zero deutsch_transform_coeff
 deutsch_transform_coeff_is_zero set_4_disj)
qed

text ‹@{text U⇩f} is a gate.›

lemma (in deutsch) transpose_of_deutsch_transform:
  shows "(U⇩f)⇧t = U⇩f"
proof
  show "dim_row (U⇩f⇧t) = dim_row U⇩f" by simp
  show "dim_col (U⇩f⇧t) = dim_col U⇩f" by simp
  fix i j:: nat
  assume "i < dim_row U⇩f" and "j < dim_col U⇩f"
  thus "U⇩f⇧t $$ (i, j) = U⇩f $$ (i, j)"
    by (auto simp add: transpose_mat_def)
      (metis deutsch_transform_coeff(1-4) deutsch_transform_coeff_is_zero set_4_disj)
qed

lemma (in deutsch) adjoint_of_deutsch_transform: 
  shows "(U⇩f)⇧† = U⇩f"
proof
  show "dim_row (U⇩f⇧†) = dim_row U⇩f" by simp
  show "dim_col (U⇩f⇧†) = dim_col U⇩f" by simp
  fix i j:: nat
  assume "i < dim_row U⇩f" and "j < dim_col U⇩f"
  thus "U⇩f⇧† $$ (i, j) = U⇩f $$ (i, j)"
    by (auto simp add: dagger_def)
      (metis complex_cnj_of_nat complex_cnj_zero deutsch_transform_coeff 
        deutsch_transform_coeff_is_zero set_4_disj)
qed

lemma (in deutsch) deutsch_transform_is_gate:
  shows "gate 2 U⇩f"
proof
  show "dim_row U⇩f = 2⇧2" by simp
  show "square_mat U⇩f" by simp
  show "unitary U⇩f"
  proof-
    have "U⇩f * U⇩f = 1⇩m (dim_col U⇩f)"
    proof
      show "dim_row (U⇩f * U⇩f) = dim_row (1⇩m (dim_col U⇩f))" by simp
    next
      show "dim_col (U⇩f * U⇩f) = dim_col (1⇩m (dim_col U⇩f))" by simp
    next
      fix i j:: nat
      assume "i < dim_row (1⇩m (dim_col U⇩f))" and "j < dim_col (1⇩m (dim_col U⇩f))"
      then show "(U⇩f * U⇩f) $$ (i,j) = 1⇩m (dim_col U⇩f) $$ (i, j)"
        apply (auto simp add: deutsch_transform_alt_rep one_mat_def times_mat_def)
         apply (auto simp: scalar_prod_def) 
        using f_values by auto
    qed
    thus ?thesis by (simp add: adjoint_of_deutsch_transform unitary_def)
  qed
qed

text ‹
Two qubits are prepared. 
The first one in the state $|0\rangle$, the second one in the state $|1\rangle$.
›

abbreviation zero where "zero ≡ unit_vec 2 0"
abbreviation one where "one ≡ unit_vec 2 1" 

lemma ket_zero_is_state: 
  shows "state 1 |zero⟩"
  by (simp add: state_def ket_vec_def cpx_vec_length_def numerals(2))

lemma ket_one_is_state:
  shows "state 1 |one⟩" 
  by (simp add: state_def ket_vec_def cpx_vec_length_def numerals(2))

lemma ket_zero_to_mat_of_cols_list [simp]: "|zero⟩ = mat_of_cols_list 2 [[1, 0]]"
  by (auto simp add: ket_vec_def mat_of_cols_list_def)

lemma ket_one_to_mat_of_cols_list [simp]: "|one⟩ = mat_of_cols_list 2 [[0, 1]]"
  apply (auto simp add: ket_vec_def unit_vec_def mat_of_cols_list_def)
  using less_2_cases by fastforce

text ‹
Applying the Hadamard gate to the state $|0\rangle$ results in the new state 
@{term "ψ⇩0⇩0"} = $\dfrac {(|0\rangle + |1\rangle)} {\sqrt 2 }$
›

abbreviation ψ⇩0⇩0:: "complex Matrix.mat" where
"ψ⇩0⇩0 ≡ mat_of_cols_list 2 [[1/sqrt(2), 1/sqrt(2)]]"

lemma H_on_ket_zero: 
  shows "(H * |zero⟩) = ψ⇩0⇩0"
proof 
  fix i j:: nat
  assume "i < dim_row ψ⇩0⇩0" and "j < dim_col ψ⇩0⇩0"
  then have "i ∈ {0,1} ∧ j = 0" by (simp add: mat_of_cols_list_def less_2_cases)
  then show "(H * |zero⟩) $$ (i,j) = ψ⇩0⇩0 $$ (i,j)"
    by (auto simp add: mat_of_cols_list_def times_mat_def scalar_prod_def H_def)
next
  show "dim_row (H * |zero⟩) = dim_row ψ⇩0⇩0"  by (simp add: H_def mat_of_cols_list_def)
  show "dim_col (H * |zero⟩) = dim_col ψ⇩0⇩0" by (simp add: H_def mat_of_cols_list_def)
qed

lemma H_on_ket_zero_is_state: 
  shows "state 1 (H * |zero⟩)"
proof
  show "gate 1 H" 
    using H_is_gate by simp
  show "state 1 |zero⟩" 
    using ket_zero_is_state by simp
qed

text ‹
Applying the Hadamard gate to the state $|0\rangle$ results in the new state 
@{text ψ⇩0⇩1} = $\dfrac {(|0\rangle - |1\rangle)} {\sqrt 2}$.
›

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

lemma H_on_ket_one: 
  shows "(H * |one⟩) = ψ⇩0⇩1"
proof 
  fix i j:: nat
  assume "i < dim_row ψ⇩0⇩1" and "j < dim_col ψ⇩0⇩1"
  then have "i ∈ {0,1} ∧ j = 0" by (simp add: mat_of_cols_list_def less_2_cases)
  then show "(H * |one⟩) $$ (i,j) = ψ⇩0⇩1 $$ (i,j)"
    by (auto simp add: mat_of_cols_list_def times_mat_def scalar_prod_def H_def ket_vec_def)
next
  show "dim_row (H * |one⟩) = dim_row ψ⇩0⇩1" by (simp add: H_def mat_of_cols_list_def)
  show "dim_col (H * |one⟩) = dim_col ψ⇩0⇩1" by (simp add: H_def mat_of_cols_list_def ket_vec_def)
qed

lemma H_on_ket_one_is_state: 
  shows "state 1 (H * |one⟩)"
  using H_is_gate ket_one_is_state by simp

text‹
Then, the state @{text ψ⇩1} = $\dfrac {(|00\rangle - |01\rangle + |10\rangle - |11\rangle)} {2} $
is obtained by taking the tensor product of the states 
@{text ψ⇩0⇩0} = $\dfrac {(|0\rangle + |1\rangle)} {\sqrt 2} $  and  
@{text ψ⇩0⇩1} = $\dfrac {(|0\rangle - |1\rangle)} {\sqrt 2} $.
›

abbreviation ψ⇩1:: "complex Matrix.mat" where
"ψ⇩1 ≡ mat_of_cols_list 4 [[1/2, -1/2, 1/2, -1/2]]"

lemma ψ⇩0_to_ψ⇩1: 
  shows "(ψ⇩0⇩0 ⨂ ψ⇩0⇩1) = ψ⇩1"
proof 
  fix i j:: nat
  assume "i < dim_row ψ⇩1" and "j < dim_col ψ⇩1"
  then have "i ∈ {0,1,2,3}" and "j = 0" using mat_of_cols_list_def by auto  
  moreover have "complex_of_real (sqrt 2) * complex_of_real (sqrt 2) = 2"
    by (metis mult_2_right numeral_Bit0 of_real_mult of_real_numeral real_sqrt_four real_sqrt_mult)
  ultimately show "(ψ⇩0⇩0 ⨂ ψ⇩0⇩1) $$ (i,j) = ψ⇩1 $$ (i,j)" using mat_of_cols_list_def by auto
next 
  show "dim_row (ψ⇩0⇩0 ⨂ ψ⇩0⇩1) = dim_row ψ⇩1" by (simp add: mat_of_cols_list_def)
  show "dim_col (ψ⇩0⇩0 ⨂ ψ⇩0⇩1) = dim_col ψ⇩1" by (simp add: mat_of_cols_list_def)
qed

lemma ψ⇩1_is_state: 
  shows "state 2 ψ⇩1"
proof 
  show  "dim_col ψ⇩1 = 1" 
    by (simp add: Tensor.mat_of_cols_list_def)
  show "dim_row ψ⇩1 = 2⇧2" 
    by (simp add: Tensor.mat_of_cols_list_def)
  show "∥Matrix.col ψ⇩1 0∥ = 1"
    using H_on_ket_one_is_state H_on_ket_zero_is_state state.is_normal tensor_state2 ψ⇩0_to_ψ⇩1
    H_on_ket_one H_on_ket_zero by force
qed

text ‹
Next, the gate @{text U⇩f} is applied to the state 
@{text ψ⇩1} = $\dfrac {(|00\rangle - |01\rangle + |10\rangle - |11\rangle)} {2}$ and 
@{text ψ⇩2}= $\dfrac {(|0f(0)\oplus 0\rangle - |0 f(0) \oplus 1\rangle + |1 f(1)\oplus 0\rangle - |1f(1)\oplus 1\rangle)} {2}$ 
is obtained. This simplifies to 
@{text ψ⇩2}= $\dfrac {(|0f(0)\rangle - |0 \overline{f(0)} \rangle + |1 f(1)\rangle - |1\overline{f(1)}\rangle)} {2}$ 
›

abbreviation (in deutsch) ψ⇩2:: "complex Matrix.mat" where
"ψ⇩2 ≡  mat_of_cols_list 4 [[(1 - f(0))/2 - f(0)/2,
                            f(0)/2 - (1 - f(0))/2,
                            (1 - f(1))/2 - f(1)/2,
                            f(1)/2 - (1- f(1))/2]]"

lemma (in deutsch) ψ⇩1_to_ψ⇩2: 
  shows "U⇩f * ψ⇩1 = ψ⇩2"
proof 
  fix i j:: nat
  assume "i < dim_row ψ⇩2 " and "j < dim_col ψ⇩2"
  then have asm:"i ∈ {0,1,2,3} ∧ j = 0 " by (auto simp add: mat_of_cols_list_def)
  then have "i < dim_row U⇩f ∧ j < dim_col ψ⇩1" 
    using deutsch_transform_def mat_of_cols_list_def by auto
  then have "(U⇩f * ψ⇩1) $$ (i, j) 
        = (∑ k ∈ {0 ..< dim_vec ψ⇩1}. (Matrix.row U⇩f i) $ k * (Matrix.col ψ⇩1 j) $ k)"
    apply (auto simp add: times_mat_def scalar_prod_def).
  thus "(U⇩f * ψ⇩1) $$ (i, j) = ψ⇩2 $$ (i, j)"
    using  mat_of_cols_list_def deutsch_transform_def asm by auto
next
  show "dim_row (U⇩f * ψ⇩1) = dim_row ψ⇩2" by (simp add: mat_of_cols_list_def)
  show "dim_col (U⇩f * ψ⇩1) = dim_col ψ⇩2" by (simp add: mat_of_cols_list_def)
qed

lemma (in deutsch) ψ⇩2_is_state:
  shows "state 2 ψ⇩2" 
proof
  show  "dim_col ψ⇩2 = 1" 
    by (simp add: Tensor.mat_of_cols_list_def)
  show "dim_row ψ⇩2 = 2⇧2" 
    by (simp add: Tensor.mat_of_cols_list_def)
  show "∥Matrix.col ψ⇩2 0∥ = 1"
    using gate_on_state_is_state ψ⇩1_is_state deutsch_transform_is_gate ψ⇩1_to_ψ⇩2 state_def
    by (metis (no_types, lifting))
qed

lemma H_tensor_Id_1: 
  defines d:"v ≡  mat_of_cols_list 4 [[1/sqrt(2), 0, 1/sqrt(2), 0],
                                  [0, 1/sqrt(2), 0, 1/sqrt(2)],
                                  [1/sqrt(2), 0, -1/sqrt(2), 0],
                                  [0, 1/sqrt(2), 0, -1/sqrt(2)]]"
  shows "(H ⨂ Id 1) = v"
proof
  show "dim_col (H ⨂ Id 1) = dim_col v"  
    by (simp add: d H_def Id_def mat_of_cols_list_def)
  show "dim_row (H ⨂ Id 1) = dim_row v"
    by (simp add: d H_def Id_def mat_of_cols_list_def)
  fix i j:: nat assume "i < dim_row v" and "j < dim_col v"
  then have "i ∈ {0..<4} ∧ j ∈ {0..<4}" 
    by (auto simp add: d mat_of_cols_list_def)
  thus "(H ⨂ Id 1) $$ (i, j) = v $$ (i, j)"
    by (auto simp add: d Id_def H_def mat_of_cols_list_def)
qed

lemma H_tensor_Id_1_is_gate: 
  shows "gate 2 (H ⨂ Id 1)"
proof 
  show "dim_row (H ⨂ Quantum.Id 1) = 2⇧2" 
    using H_tensor_Id_1 by (simp add: mat_of_cols_list_def)
  show "square_mat (H ⨂ Quantum.Id 1)" 
    using H_is_gate id_is_gate tensor_gate_sqr_mat by blast
  show "unitary (H ⨂ Quantum.Id 1)" 
    using H_is_gate gate_def id_is_gate tensor_gate by blast
qed

text ‹
Applying the Hadamard gate to the first qubit of @{text ψ⇩2} results in @{text ψ⇩3} = 
$\pm |f(0)\oplus f(1)\rangle \left[ \dfrac {(|0\rangle - |1\rangle)} {\sqrt 2}\right]$ 
›

abbreviation (in deutsch) ψ⇩3:: "complex Matrix.mat" where
"ψ⇩3 ≡ mat_of_cols_list 4 
[[(1-f(0))/(2*sqrt(2)) - f(0)/(2*sqrt(2)) + (1-f(1))/(2*sqrt(2)) - f(1)/(2*sqrt(2)),
  f(0)/(2*sqrt(2)) - (1-f(0))/(2*sqrt(2)) + (f(1)/(2*sqrt(2)) - (1-f(1))/(2*sqrt(2))),
  (1-f(0))/(2*sqrt(2)) - f(0)/(2*sqrt(2)) - (1-f(1))/(2*sqrt(2)) + f(1)/(2*sqrt(2)),
  f(0)/(2*sqrt(2)) - (1-f(0))/(2*sqrt(2)) - f(1)/(2*sqrt(2)) + (1-f(1))/(2*sqrt(2))]]"

lemma (in deutsch) ψ⇩2_to_ψ⇩3: 
 shows "(H ⨂ Id 1) * ψ⇩2 = ψ⇩3" 
proof
  fix i j:: nat
  assume "i < dim_row ψ⇩3" and "j < dim_col ψ⇩3"
  then have a0:"i ∈ {0,1,2,3} ∧ j = 0" by (auto simp add: mat_of_cols_list_def)
  then have "i < dim_row (H ⨂ Id 1) ∧ j < dim_col ψ⇩2"
    using mat_of_cols_list_def H_tensor_Id_1 by auto
  then have "((H ⨂ Id 1)*ψ⇩2) $$ (i,j)
        = (∑ k ∈ {0 ..< dim_vec ψ⇩2}. (Matrix.row (H ⨂ Id 1) i) $ k * (Matrix.col ψ⇩2 j) $ k)"
    by (auto simp: times_mat_def scalar_prod_def)
  thus "((H ⨂ Id 1) * ψ⇩2) $$ (i, j) = ψ⇩3 $$ (i, j)"
    using  mat_of_cols_list_def H_tensor_Id_1 a0 f_ge_0 
    by (auto simp: diff_divide_distrib)
next
  show "dim_row ((H ⨂ Id 1) * ψ⇩2) = dim_row ψ⇩3"
    using H_tensor_Id_1 mat_of_cols_list_def by simp
  show "dim_col ((H ⨂ Id 1) * ψ⇩2) = dim_col ψ⇩3"    
    using H_tensor_Id_1 mat_of_cols_list_def by simp
qed

lemma (in deutsch) ψ⇩3_is_state: 
  shows "state 2 ψ⇩3"
proof-
  have "gate 2 (H ⨂ Id 1)" 
    using H_tensor_Id_1_is_gate by simp
  thus "state 2 ψ⇩3" 
    using ψ⇩2_is_state ψ⇩2_to_ψ⇩3 by (metis gate_on_state_is_state)
qed

text ‹
Finally, all steps are put together. The result depends on the function f. If f is constant
the first qubit of $\pm |f(0)\oplus f(1)\rangle \left[ \dfrac {(|0\rangle - |1\rangle)} {\sqrt 2}\right]$
is 0, if it is is\_balanced it is 1. 
The algorithm only uses one evaluation of f(x) and will always succeed. 
›

definition (in deutsch) deutsch_algo:: "complex Matrix.mat" where 
"deutsch_algo ≡ (H ⨂ Id 1) * (U⇩f * ((H * |zero⟩) ⨂ (H * |one⟩)))"

lemma (in deutsch) deutsch_algo_result [simp]: 
  shows "deutsch_algo = ψ⇩3" 
  using deutsch_algo_def H_on_ket_zero H_on_ket_one ψ⇩0_to_ψ⇩1 ψ⇩1_to_ψ⇩2 ψ⇩2_to_ψ⇩3 by simp

lemma (in deutsch) deutsch_algo_result_is_state: 
  shows "state 2 deutsch_algo" 
  using ψ⇩3_is_state by simp


text ‹
If the function is constant then the measurement of the first qubit should result in the state 
$|0\rangle$ with probability 1. 
›

lemma (in deutsch) prob0_deutsch_algo_const:
  assumes "is_const" 
  shows "prob0 2 deutsch_algo 0 = 1" 
proof -
  have "{k| k::nat. (k < 4) ∧ ¬ select_index 2 0 k} = {0,1}"
    using select_index_def by auto
  then have "prob0 2 deutsch_algo 0 = (∑j∈{0,1}. (cmod(deutsch_algo $$ (j,0)))⇧2)"
    using deutsch_algo_result_is_state prob0_def by simp
  thus "prob0 2 deutsch_algo 0 = 1" 
    using assms is_const_def const_def by auto
qed

lemma (in deutsch) prob1_deutsch_algo_const: 
  assumes "is_const" 
  shows "prob1 2 deutsch_algo 0 = 0" 
  using assms prob0_deutsch_algo_const prob_sum_is_one[of "2" "deutsch_algo" "0"] 
deutsch_algo_result_is_state by simp

text ‹
If the function is balanced the measurement of the first qubit should result in the state $|1\rangle$ 
with probability 1. 
›

lemma (in deutsch) prob0_deutsch_algo_balanced:  
  assumes "is_balanced" 
  shows "prob0 2 deutsch_algo 0 = 0" 
proof-
  have "{k| k::nat. (k < 4) ∧ ¬ select_index 2 0 k} = {0,1}"
    using select_index_def by auto
  then have "prob0 2 deutsch_algo 0 = (∑j ∈ {0,1}. (cmod(deutsch_algo $$ (j,0)))⇧2)"
    using deutsch_algo_result_is_state prob0_def by simp
  thus "prob0 2 deutsch_algo 0 = 0" 
    using is_swap_values assms is_balanced_def by auto
qed

lemma (in deutsch) prob1_deutsch_algo_balanced:
  assumes "is_balanced" 
  shows "prob1 2 deutsch_algo 0 = 1" 
using assms prob0_deutsch_algo_balanced prob_sum_is_one[of "2" "deutsch_algo" "0"] 
deutsch_algo_result_is_state by simp
 
text ‹Eventually, the measurement of the first qubit results in $f(0)\oplus f(1)$. ›

definition (in deutsch) deutsch_algo_eval:: "real" where 
"deutsch_algo_eval ≡ prob1 2 deutsch_algo 0"

lemma (in deutsch) sum_mod_2_cases:
  shows "(f 0 + f 1) mod 2 = 0 ⟶ is_const" 
  and "(f 0 + f 1) mod 2 = 1 ⟶ is_balanced"
  using f_cases is_balanced_sum_mod_2 is_const_sum_mod_2 by auto 

lemma (in deutsch) deutsch_algo_eval_is_sum_mod_2:
  shows "deutsch_algo_eval = (f 0 + f 1) mod 2"
  using deutsch_algo_eval_def f_cases is_const_sum_mod_2 is_balanced_sum_mod_2 
prob1_deutsch_algo_const prob1_deutsch_algo_balanced by auto

text ‹
If the algorithm returns 0 then one concludes that the input function is constant and
if it returns 1 then the function is balanced.
›

theorem (in deutsch) deutsch_algo_is_correct:
  shows "deutsch_algo_eval = 0 ⟶ is_const" and "deutsch_algo_eval = 1 ⟶ is_balanced"
  using deutsch_algo_eval_is_sum_mod_2 sum_mod_2_cases by auto

end