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 Uf}.›

definition (in deutsch) deutsch_transform:: "complex Matrix.mat" ("Uf") where 
"Uf  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 Uf = 4" and "dim_col Uf = 4" 
  by (auto simp add: deutsch_transform_def mat_of_cols_list_def)

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

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

abbreviation (in deutsch) Vf:: "complex Matrix.mat" where
"Vf  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 "Vf $$ (0,2) = 0" and "Vf $$ (0,3) = 0"
    and "Vf $$ (1,2) = 0" and "Vf $$(1,3) = 0"
    and "Vf $$ (2,0) = 0" and "Vf $$(2,1) = 0"
    and "Vf $$ (3,0) = 0" and "Vf $$ (3,1) = 0"
  by auto

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

lemma (in deutsch) deutsch_transform_alt_rep:
  shows "Uf = Vf"
proof
  show c0:"dim_row Uf = dim_row Vf" by simp
  show c1:"dim_col Uf = dim_col Vf" by simp
  fix i j:: nat
  assume "i < dim_row Vf" and "j < dim_col Vf"
  then have "i < 4" and "j < 4" by auto
  thus "Uf $$ (i,j) = Vf $$ (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 Uf} is a gate.›

lemma (in deutsch) transpose_of_deutsch_transform:
  shows "(Uf)t = Uf"
proof
  show "dim_row (Uft) = dim_row Uf" by simp
  show "dim_col (Uft) = dim_col Uf" by simp
  fix i j:: nat
  assume "i < dim_row Uf" and "j < dim_col Uf"
  thus "Uft $$ (i, j) = Uf $$ (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 "(Uf) = Uf"
proof
  show "dim_row (Uf) = dim_row Uf" by simp
  show "dim_col (Uf) = dim_col Uf" by simp
  fix i j:: nat
  assume "i < dim_row Uf" and "j < dim_col Uf"
  thus "Uf $$ (i, j) = Uf $$ (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 Uf"
proof
  show "dim_row Uf = 22" by simp
  show "square_mat Uf" by simp
  show "unitary Uf"
  proof-
    have "Uf * Uf = 1m (dim_col Uf)"
    proof
      show "dim_row (Uf * Uf) = dim_row (1m (dim_col Uf))" by simp
    next
      show "dim_col (Uf * Uf) = dim_col (1m (dim_col Uf))" by simp
    next
      fix i j:: nat
      assume "i < dim_row (1m (dim_col Uf))" and "j < dim_col (1m (dim_col Uf))"
      then show "(Uf * Uf) $$ (i,j) = 1m (dim_col Uf) $$ (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 "ψ00"} = $\dfrac {(|0\rangle + |1\rangle)} {\sqrt 2 }$
›

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

lemma H_on_ket_zero: 
  shows "(H * |zero) = ψ00"
proof 
  fix i j:: nat
  assume "i < dim_row ψ00" and "j < dim_col ψ00"
  then have "i  {0,1}  j = 0" by (simp add: mat_of_cols_list_def less_2_cases)
  then show "(H * |zero) $$ (i,j) = ψ00 $$ (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 ψ00"  by (simp add: H_def mat_of_cols_list_def)
  show "dim_col (H * |zero) = dim_col ψ00" 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 ψ01} = $\dfrac {(|0\rangle - |1\rangle)} {\sqrt 2}$.
›

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

lemma H_on_ket_one: 
  shows "(H * |one) = ψ01"
proof 
  fix i j:: nat
  assume "i < dim_row ψ01" and "j < dim_col ψ01"
  then have "i  {0,1}  j = 0" by (simp add: mat_of_cols_list_def less_2_cases)
  then show "(H * |one) $$ (i,j) = ψ01 $$ (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 ψ01" by (simp add: H_def mat_of_cols_list_def)
  show "dim_col (H * |one) = dim_col ψ01" 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 ψ00} = $\dfrac {(|0\rangle + |1\rangle)} {\sqrt 2} $  and  
@{text ψ01} = $\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 "(ψ00  ψ01) = ψ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 "(ψ00  ψ01) $$ (i,j) = ψ1 $$ (i,j)" using mat_of_cols_list_def by auto
next 
  show "dim_row (ψ00  ψ01) = dim_row ψ1" by (simp add: mat_of_cols_list_def)
  show "dim_col (ψ00  ψ01) = 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 = 22" 
    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 Uf} 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 "Uf * ψ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 Uf  j < dim_col ψ1" 
    using deutsch_transform_def mat_of_cols_list_def by auto
  then have "(Uf * ψ1) $$ (i, j) 
        = ( k  {0 ..< dim_vec ψ1}. (Matrix.row Uf i) $ k * (Matrix.col ψ1 j) $ k)"
    apply (auto simp add: times_mat_def scalar_prod_def).
  thus "(Uf * ψ1) $$ (i, j) = ψ2 $$ (i, j)"
    using  mat_of_cols_list_def deutsch_transform_def asm by auto
next
  show "dim_row (Uf * ψ1) = dim_row ψ2" by (simp add: mat_of_cols_list_def)
  show "dim_col (Uf * ψ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 = 22" 
    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) = 22" 
    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) * (Uf * ((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