# 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 (verit) 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)"
(metis deutsch_transform_coeff(1-4) deutsch_transform_coeff_is_zero set_4_disj)
qed

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)"
(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
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"
show "dim_row ψ⇩1 = 2⇧2"
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