# Theory Deutsch_Jozsa

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

section ‹The Deutsch-Jozsa Algorithm›

theory Deutsch_Jozsa
imports
Deutsch
More_Tensor
Binary_Nat
begin

text ‹
Given a function $f:{0,1}^n \mapsto {0,1}$, the Deutsch-Jozsa 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.

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 bob_fun =
fixes f:: "nat ⇒ nat" and n:: "nat"
assumes dom: "f ∈ ({(i::nat). i < 2^n} →⇩E {0,1})"
assumes dim: "n ≥ 1"

context bob_fun
begin

definition const:: "nat ⇒ bool" where
"const c = (∀x∈{i::nat. i<2^n}. f x = c)"

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

definition is_balanced:: bool where
"is_balanced ≡ ∃A B ::nat set. A ⊆ {i::nat. i < 2^n} ∧ B ⊆ {i::nat. i < 2^n}
∧ card A = 2^(n-1) ∧ card B = 2^(n-1)
∧ (∀x∈A. f x = 0)  ∧ (∀x∈B. f x = 1)"

lemma is_balanced_inter:
fixes A B:: "nat set"
assumes "∀x ∈ A. f x = 0" and "∀x ∈ B. f x = 1"
shows "A ∩ B = {}"
using assms by auto

lemma is_balanced_union:
fixes A B:: "nat set"
assumes "A ⊆ {i::nat. i < 2^n}" and "B ⊆ {i::nat. i < 2^n}"
and "card A = 2^(n-1)" and "card B = 2^(n-1)"
and "A ∩ B = {}"
shows "A ∪ B = {i::nat. i < 2^n}"
proof-
have "finite A" and "finite B"
then have "card(A ∪ B) = 2 * 2^(n-1)"
using assms(3-5) by (simp add: card_Un_disjoint)
then have "card(A ∪ B) = 2^n"
by (metis Nat.nat.simps(3) One_nat_def dim le_0_eq power_eq_if)
moreover have "… = card({i::nat. i < 2^n})" by simp
moreover have "A ∪ B ⊆ {i::nat. i < 2^n}"
using assms(1,2) by simp
moreover have "finite ({i::nat. i < 2^n})" by simp
ultimately show ?thesis
using card_subset_eq[of "{i::nat. i < 2^n}" "A ∪ B"] by simp
qed

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

lemma f_dom_not_zero:
shows "f ∈ ({i::nat. n ≥ 1 ∧ i < 2^n} →⇩E {0,1})"
using dim dom by simp

lemma f_values: "∀x ∈ {(i::nat). i < 2^n} . f x = 0 ∨ f x = 1"
using dom by auto

end (* bob_fun *)

text ‹The input function has to be constant or balanced.›

locale jozsa = bob_fun +
assumes const_or_balanced: "is_const ∨ is_balanced "

text ‹
Introduce two customised rules: disjunctions with four disjuncts and induction starting from one
›

(* To deal with Uf it is often necessary to do a case distinction with four different cases.*)
lemma disj_four_cases:
assumes "A ∨ B ∨ C ∨ D" and "A ⟹ P" and "B ⟹ P" and "C ⟹ P" and "D ⟹ P"
shows "P"
using assms by auto

text ‹The unitary transform @{term U⇩f}.›

definition (in jozsa) jozsa_transform:: "complex Matrix.mat" ("U⇩f") where
"U⇩f ≡ Matrix.mat (2^(n+1)) (2^(n+1)) (λ(i,j).
if i = j then (1-f(i div 2)) else
if i = j + 1 ∧ odd i then f(i div 2) else
if i = j - 1 ∧ even i ∧ j≥1 then f(i div 2) else 0)"

lemma (in jozsa) jozsa_transform_dim [simp]:
shows "dim_row U⇩f = 2^(n+1)" and "dim_col U⇩f = 2^(n+1)"

lemma (in jozsa) jozsa_transform_coeff_is_zero [simp]:
assumes "i < dim_row U⇩f ∧ j < dim_col U⇩f"
shows "(i≠j ∧ ¬(i=j+1 ∧ odd i) ∧ ¬ (i=j-1 ∧ even i ∧ j≥1)) ⟶ U⇩f $$(i,j) = 0" using jozsa_transform_def assms by auto lemma (in jozsa) jozsa_transform_coeff [simp]: assumes "i < dim_row U⇩f ∧ j < dim_col U⇩f" shows "i = j ⟶ U⇩f$$ (i,j) = 1 - f (i div 2)"
and "i = j + 1 ∧ odd i ⟶ U⇩f $$(i,j) = f (i div 2)" and "j ≥ 1 ∧ i = j - 1 ∧ even i ⟶ U⇩f$$ (i,j) = f (i div 2)"
using jozsa_transform_def assms by auto

lemma (in jozsa) U⇩f_mult_without_empty_summands_sum_even:
fixes i j A
assumes "i < dim_row U⇩f" and "j < dim_col A" and "even i" and "dim_col U⇩f = dim_row A"
shows "(∑k∈{0..< dim_row A}. U⇩f $$(i,k) * A$$ (k,j)) =(∑k∈{i,i+1}. U⇩f $$(i,k) * A$$ (k,j))"
proof-
have "(∑k ∈ {0..< 2^(n+1)}. U⇩f $$(i,k) * A$$ (k,j)) =
(∑k ∈ {0..<i}. U⇩f $$(i,k) * A$$ (k,j)) +
(∑k ∈ {i,i+1}. U⇩f $$(i,k) * A$$ (k,j)) +
(∑k ∈ {(i+2)..< 2^(n+1)}. U⇩f $$(i,k) * A$$ (k,j))"
proof-
have "{0..< 2^(n+1)} = {0..<i} ∪ {i..< 2^(n+1)}
∧ {i..< 2^(n+1)} = {i,i+1} ∪ {(i+2)..<2^(n+1)}" using assms(1-3) by auto
moreover have "{0..<i} ∩ {i,i+1} = {}
∧ {i,i+1} ∩ {(i+2)..< 2^(n+1)} = {}
∧ {0..<i} ∩ {(i+2)..< 2^(n+1)} = {}" using assms by simp
ultimately show ?thesis
using sum.union_disjoint
by (metis (no_types, lifting) finite_Un finite_atLeastLessThan is_num_normalize(1) ivl_disj_int_two(3))
qed
moreover have "(∑k ∈ {0..<i}. U⇩f $$(i,k) * A$$ (k,j)) = 0"
proof-
have "k ∈ {0..<i} ⟶ (i≠k ∧ ¬(i=k+1 ∧ odd i) ∧ ¬ (i=k-1 ∧ even i ∧ k≥1))" for k
using assms by auto
then have "k ∈ {0..<i} ⟶ U⇩f $$(i,k) = 0" for k using assms(1) by auto then show ?thesis by simp qed moreover have "(∑k ∈ {(i+2)..< 2^(n+1)}. U⇩f$$ (i,k) * A $$(k,j)) = 0" proof- have "k∈{(i+2)..< 2^(n+1)} ⟶ (i≠k ∧ ¬(i=k+1 ∧ odd i) ∧ ¬ (i=k-1 ∧ even i ∧ k≥1))" for k by auto then have "k ∈ {(i+2)..< 2^(n+1)}⟶ U⇩f$$ (i,k) = 0" for k
using assms(1) by auto
then show ?thesis by simp
qed
moreover have  "dim_row A = 2^(n+1)" using assms(4) by simp
qed

lemma (in jozsa) U⇩f_mult_without_empty_summands_even:
fixes i j A
assumes "i < dim_row U⇩f" and "j < dim_col A" and "even i" and "dim_col U⇩f = dim_row A"
shows "(U⇩f * A) $$(i,j) = (∑k ∈ {i,i+1}. U⇩f$$ (i,k) * A $$(k,j))" proof- have "(U⇩f * A)$$ (i,j) = (∑ k∈{0..< dim_row A}. (U⇩f $$(i,k)) * (A$$ (k,j)))"
using assms(1,2,4) index_matrix_prod by (simp add: atLeast0LessThan)
then show ?thesis
using assms U⇩f_mult_without_empty_summands_sum_even by simp
qed

lemma (in jozsa) U⇩f_mult_without_empty_summands_sum_odd:
fixes i j A
assumes "i < dim_row U⇩f" and "j < dim_col A" and "odd i" and "dim_col U⇩f = dim_row A"
shows "(∑k∈{0..< dim_row A}. U⇩f $$(i,k) * A$$ (k,j)) =(∑k∈{i-1,i}. U⇩f $$(i,k) * A$$ (k,j))"
proof-
have "(∑k∈{0..< 2^(n+1)}. U⇩f $$(i,k) * A$$ (k,j)) =
(∑k ∈ {0..<i-1}. U⇩f $$(i,k) * A$$ (k,j)) +
(∑k ∈ {i-1,i}. U⇩f $$(i,k) * A$$ (k,j)) +
(∑k ∈ {i+1..< 2^(n+1)}. U⇩f $$(i,k) * A$$ (k,j))"
proof-
have "{0..< 2^(n+1)} = {0..<i-1} ∪ {i-1..< 2^(n+1)}
∧ {i-1..< 2^(n+1)} = {i-1,i} ∪ {i+1..<2^(n+1)}" using assms(1-3) by auto
moreover have "{0..<i-1} ∩ {i-1,i} = {}
∧ {i-1,i} ∩ {i+1..< 2^(n+1)} = {}
∧ {0..<i-1} ∩ {i+1..< 2^(n+1)} = {}" using assms by simp
ultimately show ?thesis
using sum.union_disjoint
by(metis (no_types, lifting) finite_Un finite_atLeastLessThan is_num_normalize(1) ivl_disj_int_two(3))
qed
moreover have "(∑k ∈ {0..<i-1}. U⇩f $$(i,k) * A$$ (k,j)) = 0"
proof-
have "k ∈ {0..<i-1} ⟶ (i≠k ∧ ¬(i=k+1 ∧ odd i) ∧ ¬ (i=k-1 ∧ even i ∧ k≥1))" for k by auto
then have "k ∈ {0..<i-1} ⟶ U⇩f $$(i,k) = 0" for k using assms(1) by auto then show ?thesis by simp qed moreover have "(∑k ∈ {i+1..< 2^(n+1)}. U⇩f$$ (i,k) * A $$(k,j)) = 0" using assms(3) by auto moreover have "dim_row A = 2^(n+1)" using assms(4) by simp ultimately show "?thesis" by(metis (no_types, lifting) add.left_neutral add.right_neutral) qed lemma (in jozsa) U⇩f_mult_without_empty_summands_odd: fixes i j A assumes "i < dim_row U⇩f" and "j < dim_col A" and "odd i" and "dim_col U⇩f = dim_row A" shows "(U⇩f * A)$$ (i,j) = (∑k ∈ {i-1,i}. U⇩f $$(i,k) * A$$ (k,j)) "
proof-
have "(U⇩f * A) $$(i,j) = (∑k ∈ {0 ..< dim_row A}. (U⇩f$$ (i,k)) * (A $$(k,j)))" using assms(1,2,4) index_matrix_prod by (simp add: atLeast0LessThan) then show "?thesis" using assms U⇩f_mult_without_empty_summands_sum_odd by auto qed text ‹@{term U⇩f} is a gate.› lemma (in jozsa) transpose_of_jozsa_transform: shows "(U⇩f)⇧t = U⇩f" proof show "dim_row (U⇩f⇧t) = dim_row U⇩f" by simp next show "dim_col (U⇩f⇧t) = dim_col U⇩f" by simp next fix i j:: nat assume a0: "i < dim_row U⇩f" and a1: "j < dim_col U⇩f" then show "U⇩f⇧t$$ (i, j) = U⇩f $$(i, j)" proof (induct rule: disj_four_cases) show "i=j ∨ (i=j+1 ∧ odd i) ∨ (i=j-1 ∧ even i ∧ j≥1) ∨ (i≠j ∧ ¬(i=j+1 ∧ odd i) ∧ ¬ (i=j-1 ∧ even i ∧ j≥1))" by linarith next assume "i = j" then show "U⇩f⇧t$$ (i,j) = U⇩f $$(i,j)" using a0 by simp next assume "(i=j+1 ∧ odd i)" then show "U⇩f⇧t$$ (i,j) = U⇩f $$(i,j)" using transpose_mat_def a0 a1 by auto next assume a2:"(i=j-1 ∧ even i ∧ j≥1)" then have "U⇩f$$ (i,j) = f (i div 2)"
using a0 a1 jozsa_transform_coeff by auto
moreover have "U⇩f $$(j,i) = f (i div 2)" using a0 a1 a2 jozsa_transform_coeff by (metis add_diff_assoc2 diff_add_inverse2 even_plus_one_iff even_succ_div_two jozsa_transform_dim) ultimately show "?thesis" using transpose_mat_def a0 a1 by simp next assume a2:"(i≠j ∧ ¬(i=j+1 ∧ odd i) ∧ ¬ (i=j-1 ∧ even i ∧ j≥1))" then have "(j≠i ∧ ¬(j=i+1 ∧ odd j) ∧ ¬ (j=i-1 ∧ even j ∧ i≥1))" by (metis le_imp_diff_is_add diff_add_inverse even_plus_one_iff le_add1) then have "U⇩f$$ (j,i) = 0"
using jozsa_transform_coeff_is_zero a0 a1 by auto
moreover have "U⇩f $$(i,j) = 0" using jozsa_transform_coeff_is_zero a0 a1 a2 by auto ultimately show "U⇩f⇧t$$ (i,j) = U⇩f $$(i,j)" using transpose_mat_def a0 a1 by simp qed qed lemma (in jozsa) adjoint_of_jozsa_transform: shows "(U⇩f)⇧† = U⇩f" proof show "dim_row (U⇩f⇧†) = dim_row U⇩f" by simp next show "dim_col (U⇩f⇧†) = dim_col U⇩f" by simp next fix i j:: nat assume a0: "i < dim_row U⇩f" and a1: "j < dim_col U⇩f" then show "U⇩f⇧†$$ (i,j) = U⇩f $$(i,j)" proof (induct rule: disj_four_cases) show "i=j ∨ (i=j+1 ∧ odd i) ∨ (i=j-1 ∧ even i ∧ j≥1) ∨ (i≠j ∧ ¬(i=j+1 ∧ odd i) ∧ ¬ (i=j-1 ∧ even i ∧ j≥1))" by linarith next assume "i=j" then show "U⇩f⇧†$$ (i,j) = U⇩f $$(i,j)" using a0 dagger_def by simp next assume "(i=j+1 ∧ odd i)" then show "U⇩f⇧†$$ (i,j) = U⇩f $$(i,j)" using a0 dagger_def by auto next assume a2:"(i=j-1 ∧ even i ∧ j≥1)" then have "U⇩f$$ (i,j) = f (i div 2)"
using a0 a1 jozsa_transform_coeff by auto
moreover have "U⇩f⇧†  $$(j,i) = f (i div 2)" using a1 a2 jozsa_transform_coeff dagger_def by auto ultimately show "U⇩f⇧†$$ (i,j) = U⇩f $$(i,j)" by(metis a0 a1 cnj_transpose_is_dagger dim_row_of_dagger index_transpose_mat dagger_of_transpose_is_cnj transpose_of_jozsa_transform) next assume a2: "(i≠j ∧ ¬(i=j+1 ∧ odd i) ∧ ¬ (i=j-1 ∧ even i ∧ j≥1))" then have f0:"(i≠j ∧ ¬(j=i+1 ∧ odd j) ∧ ¬ (j=i-1 ∧ even j ∧ i≥1))" by (metis le_imp_diff_is_add diff_add_inverse even_plus_one_iff le_add1) then have "U⇩f$$ (j,i) = 0" and "cnj 0 = 0"
using jozsa_transform_coeff_is_zero a0 a1 a2 by auto
then have "U⇩f⇧† $$(i,j) = 0" using a0 a1 dagger_def by simp then show "U⇩f⇧†$$ (i, j) = U⇩f $$(i, j)" using a0 a1 a2 jozsa_transform_coeff_is_zero by auto qed qed lemma (in jozsa) jozsa_transform_is_unitary_index_even: fixes i j:: nat assumes "i < dim_row U⇩f" and "j < dim_col U⇩f" and "even i" shows "(U⇩f * U⇩f)$$ (i,j) = 1⇩m (dim_col U⇩f) $$(i,j)" proof- have "(U⇩f * U⇩f)$$ (i,j) = (∑k ∈ {i,i+1}. U⇩f $$(i,k) * U⇩f$$ (k,j)) "
using U⇩f_mult_without_empty_summands_even[of i j U⇩f ] assms by simp
moreover have "U⇩f $$(i,i) * U⇩f$$ (i,j) = (1-f(i div 2)) * U⇩f $$(i,j)" using assms(1,3) by simp moreover have f0: "U⇩f$$ (i,i+1) * U⇩f $$(i+1,j) = f(i div 2) * U⇩f$$ (i+1,j)"
ultimately have f1: "(U⇩f * U⇩f) $$(i,j) = (1-f(i div 2)) * U⇩f$$ (i,j) +  f(i div 2) * U⇩f $$(i+1,j)" by auto thus ?thesis proof (induct rule: disj_four_cases) show "j=i ∨ (j=i+1 ∧ odd j) ∨ (j=i-1 ∧ even j ∧ i≥1) ∨ (j≠i ∧ ¬(j=i+1 ∧ odd j) ∧ ¬ (j=i-1 ∧ even j ∧ i≥1))" by linarith next assume a0:"j=i" then have "U⇩f$$ (i,j) = (1-f(i div 2))"
using assms(1,2) a0 by simp
moreover have "U⇩f $$(i+1,j) = f(i div 2)" using assms(1,3) a0 by auto ultimately have "(U⇩f * U⇩f)$$ (i,j) = (1-f(i div 2)) * (1-f(i div 2)) +  f(i div 2) * f(i div 2)"
using f1 by simp
moreover have "(1-f(i div 2)) * (1-f(i div 2)) + f(i div 2) * f(i div 2) = 1"
using f_values assms(1)
less_power_add_imp_div_less mem_Collect_eq mult_eq_if one_power2 power2_eq_square power_one_right)
ultimately show "(U⇩f * U⇩f) $$(i,j) = 1⇩m (dim_col U⇩f)$$ (i,j)"  by(metis assms(2) a0 index_one_mat(1) of_nat_1)
next
assume a0: "(j=i+1 ∧ odd j)"
then have "U⇩f $$(i,j) = f(i div 2)" using assms(1,2) a0 by simp moreover have "U⇩f$$ (i+1,j) = (1-f(i div 2))"
using assms(2,3) a0 by simp
ultimately have "(U⇩f * U⇩f) $$(i,j) = (1-f(i div 2)) * f(i div 2) + f(i div 2) * (1-f(i div 2))" using f0 f1 assms by simp then show "(U⇩f * U⇩f)$$ (i,j) = 1⇩m (dim_col U⇩f) $$(i,j)" using assms(1,2) a0 by auto next assume "(j=i-1 ∧ even j ∧ i≥1)" then show "(U⇩f * U⇩f)$$ (i,j) = 1⇩m (dim_col U⇩f) $$(i,j)" using assms(3) dvd_diffD1 odd_one by blast next assume a0:"(j≠i ∧ ¬(j=i+1 ∧ odd j) ∧ ¬ (j=i-1 ∧ even j ∧ i≥1))" then have "U⇩f$$ (i,j) = 0"
using assms(1,2) by(metis index_transpose_mat(1) jozsa_transform_coeff_is_zero jozsa_transform_dim transpose_of_jozsa_transform)
moreover have "U⇩f $$(i+1,j) = 0" using assms a0 by auto ultimately have "(U⇩f * U⇩f)$$ (i,j) = (1-f(i div 2)) * 0 +  f(i div 2) * 0"
then show "(U⇩f * U⇩f) $$(i,j) = 1⇩m (dim_col U⇩f)$$ (i,j)"
using a0 assms(1,2) by(metis add.left_neutral index_one_mat(1) jozsa_transform_dim mult_0_right of_nat_0)
qed
qed

lemma (in jozsa) jozsa_transform_is_unitary_index_odd:
fixes i j:: nat
assumes "i < dim_row U⇩f" and "j < dim_col U⇩f" and "odd i"
shows "(U⇩f * U⇩f) $$(i,j) = 1⇩m (dim_col U⇩f)$$ (i,j)"
proof-
have f0: "i ≥ 1"
using linorder_not_less assms(3) by auto
have "(U⇩f * U⇩f) $$(i,j) = (∑k ∈ {i-1,i}. U⇩f$$ (i,k) * U⇩f $$(k,j)) " using U⇩f_mult_without_empty_summands_odd[of i j U⇩f ] assms by simp moreover have "(∑k ∈ {i-1,i}. U⇩f$$ (i,k) * U⇩f $$(k,j)) = U⇩f$$ (i,i-1) * U⇩f $$(i-1,j) + U⇩f$$ (i,i) * U⇩f $$(i,j)" using f0 by simp moreover have "U⇩f$$ (i,i) * U⇩f $$(i,j) = (1-f(i div 2)) * U⇩f$$ (i,j)"
using assms(1,2) by simp
moreover have f1: "U⇩f $$(i,i-1) * U⇩f$$ (i-1,j) = f(i div 2) * U⇩f $$(i-1,j)" using assms(1) assms(3) by simp ultimately have f2: "(U⇩f * U⇩f)$$ (i,j) = f(i div 2) * U⇩f $$(i-1,j) + (1-f(i div 2)) * U⇩f$$ (i,j)" by simp
then show "?thesis"
proof (induct rule: disj_four_cases)
show "j=i ∨ (j=i+1 ∧ odd j) ∨ (j=i-1 ∧ even j ∧ i≥1) ∨ (j≠i ∧ ¬(j=i+1 ∧ odd j) ∧ ¬ (j=i-1 ∧ even j ∧ i≥1))"
by linarith
next
assume a0:"j=i"
then have "U⇩f $$(i,j) = (1-f(i div 2))" using assms(1,2) by simp moreover have "U⇩f$$ (i-1,j) = f(i div 2)"
using a0 assms
by (metis index_transpose_mat(1) jozsa_transform_coeff(2) less_imp_diff_less odd_two_times_div_two_nat
odd_two_times_div_two_succ transpose_of_jozsa_transform)
ultimately have "(U⇩f * U⇩f) $$(i,j) = f(i div 2) * f(i div 2) + (1-f(i div 2)) * (1-f(i div 2))" using f2 by simp moreover have "f(i div 2) * f(i div 2) + (1-f(i div 2)) * (1-f(i div 2)) = 1" using f_values assms(1) by (metis (no_types, lifting) Nat.minus_nat.diff_0 diff_add_0 diff_add_inverse jozsa_transform_dim(1) less_power_add_imp_div_less mem_Collect_eq mult_eq_if one_power2 power2_eq_square power_one_right) ultimately show "(U⇩f * U⇩f)$$ (i,j) = 1⇩m (dim_col U⇩f) $$(i,j)" by(metis assms(2) a0 index_one_mat(1) of_nat_1) next assume a0:"(j=i+1 ∧ odd j)" then show "(U⇩f * U⇩f)$$ (i,j) = 1⇩m (dim_col U⇩f) $$(i,j)" using assms(3) dvd_diffD1 odd_one even_plus_one_iff by blast next assume a0:"(j=i-1 ∧ even j ∧ i≥1)" then have "(U⇩f * U⇩f)$$ (i,j) = f(i div 2) * (1-f(i div 2)) + (1-f(i div 2)) * f(i div 2)"
using f0 f1 f2 assms
by (metis jozsa_transform_coeff(1) Groups.ab_semigroup_mult_class.mult.commute even_succ_div_two f2
then show "(U⇩f * U⇩f) $$(i,j) = 1⇩m (dim_col U⇩f)$$ (i,j)"
using assms(1) a0 by auto
next
assume a0:"j≠i ∧ ¬(j=i+1 ∧ odd j) ∧ ¬ (j=i-1 ∧ even j ∧ i≥1)"
then have "U⇩f $$(i,j) = 0" by (metis assms(1,2) index_transpose_mat(1) jozsa_transform_coeff_is_zero jozsa_transform_dim transpose_of_jozsa_transform) moreover have "U⇩f$$ (i-1,j) = 0"
using assms a0 f0
jozsa_transform_coeff_is_zero jozsa_axioms less_imp_le less_le_trans less_one odd_one)
ultimately have "(U⇩f * U⇩f) $$(i,j) = (1-f(i div 2)) * 0 + f(i div 2) * 0" using f2 by simp then show "(U⇩f * U⇩f)$$ (i,j) = 1⇩m (dim_col U⇩f) $$(i,j)" using a0 assms by (metis add.left_neutral index_one_mat(1) jozsa_transform_dim mult_0_right of_nat_0) qed qed lemma (in jozsa) jozsa_transform_is_gate: shows "gate (n+1) U⇩f" proof show "dim_row U⇩f = 2^(n+1)" by simp next show "square_mat U⇩f" by simp next 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 show "dim_col (U⇩f * U⇩f) = dim_col (1⇩m (dim_col U⇩f))" by simp 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 have "i < dim_row U⇩f" and "j < dim_col U⇩f" by auto then show "(U⇩f * U⇩f)$$ (i,j) = 1⇩m (dim_col U⇩f) $$(i,j)" using jozsa_transform_is_unitary_index_odd jozsa_transform_is_unitary_index_even by blast qed thus ?thesis by (simp add: adjoint_of_jozsa_transform unitary_def) qed qed text ‹N-fold application of the tensor product› fun iter_tensor:: "complex Matrix.mat ⇒ nat ⇒ complex Matrix.mat" ("_ ⊗⇗_⇖" 75) where "A ⊗⇗(Suc 0)⇖ = A" | "A ⊗⇗(Suc k)⇖ = A ⨂ (A ⊗⇗k⇖)" lemma one_tensor_is_id [simp]: fixes A shows "A ⊗⇗1⇖ = A" using one_mat_def by simp lemma iter_tensor_suc: fixes n assumes "n ≥ 1" shows " A ⊗⇗(Suc n)⇖ = A ⨂ (A ⊗⇗n⇖)" using assms by (metis Deutsch_Jozsa.iter_tensor.simps(2) One_nat_def Suc_le_D) lemma dim_row_of_iter_tensor [simp]: fixes A n assumes "n ≥ 1" shows "dim_row(A ⊗⇗n⇖) = (dim_row A)^n" using assms proof (rule nat_induct_at_least) show "dim_row (A ⊗⇗1⇖) = (dim_row A)^1" using one_tensor_is_id by simp fix n:: nat assume "n ≥ 1" and "dim_row (A ⊗⇗n⇖) = (dim_row A)^n" then show "dim_row (A ⊗⇗Suc n⇖) = (dim_row A)^Suc n" using iter_tensor_suc assms dim_row_tensor_mat by simp qed lemma dim_col_of_iter_tensor [simp]: fixes A n assumes "n ≥ 1" shows "dim_col(A ⊗⇗n⇖) = (dim_col A)^n" using assms proof (rule nat_induct_at_least) show "dim_col (A ⊗⇗1⇖) = (dim_col A)^1" using one_tensor_is_id by simp fix n:: nat assume "n ≥ 1" and "dim_col (A ⊗⇗n⇖) = (dim_col A)^n" then show "dim_col (A ⊗⇗Suc n⇖) = (dim_col A)^Suc n" using iter_tensor_suc assms dim_col_tensor_mat by simp qed lemma iter_tensor_values: fixes A n i j assumes "n ≥ 1" and "i < dim_row (A ⨂ (A ⊗⇗n⇖))" and "j < dim_col (A ⨂ (A ⊗⇗n⇖))" shows "(A ⊗⇗(Suc n)⇖)$$ (i,j) = (A ⨂ (A ⊗⇗n⇖)) $$(i,j)" using assms by (metis One_nat_def le_0_eq not0_implies_Suc iter_tensor.simps(2)) lemma iter_tensor_mult_distr: assumes "n ≥ 1" and "dim_col A = dim_row B" and "dim_col A > 0" and "dim_col B > 0" shows "(A ⊗⇗(Suc n)⇖) * (B ⊗⇗(Suc n)⇖) = (A * B) ⨂ ((A ⊗⇗n⇖) * (B ⊗⇗n⇖))" proof- have "(A ⊗⇗(Suc n)⇖) * (B ⊗⇗(Suc n)⇖) = (A ⨂ (A ⊗⇗n⇖)) * (B ⨂ (B ⊗⇗n⇖))" using Suc_le_D assms(1) by fastforce then show "?thesis" using mult_distr_tensor[of "A" "B" "(iter_tensor A n)" "(iter_tensor B n)"] assms by simp qed lemma index_tensor_mat_with_vec2_row_cond: fixes A B:: "complex Matrix.mat" and i:: "nat" assumes "i < 2 * (dim_row B)" and "i ≥ dim_row B" and "dim_col B > 0" and "dim_row A = 2" and "dim_col A = 1" shows "(A ⨂ B)$$ (i,0) = (A $$(1,0)) * (B$$ (i-dim_row B,0))"
proof-
have "(A ⨂ B) $$(i,0) = A$$ (i div (dim_row B),0) * B $$(i mod (dim_row B),0)" using assms index_tensor_mat[of A "dim_row A" "dim_col A" B "dim_row B" "dim_col B" i 0] by simp moreover have "i div (dim_row B) = 1" using assms(1,2,4) by simp then have "i mod (dim_row B) = i - (dim_row B)" by (simp add: modulo_nat_def) ultimately show "(A ⨂ B)$$ (i,0) = (A $$(1,0)) * (B$$ (i-dim_row B,0))"
by (simp add: ‹i div dim_row B = 1›)
qed

lemma iter_tensor_of_gate_is_gate:
fixes A:: "complex Matrix.mat" and n m:: "nat"
assumes "gate m A" and "n ≥ 1"
shows "gate (m*n) (A ⊗⇗n⇖)"
using assms(2)
proof(rule nat_induct_at_least)
show "gate (m * 1) (A ⊗⇗1⇖)" using assms(1) by simp
fix n:: nat
assume "n ≥ 1" and IH:"gate (m * n) (A ⊗⇗n⇖)"
then have "A ⊗⇗(Suc n)⇖ = A ⨂ (A ⊗⇗n⇖)"
moreover have "gate (m*n + m) (A ⊗⇗(Suc n)⇖)"
then show "gate (m*(Suc n)) (A ⊗⇗(Suc n)⇖)"
qed

lemma iter_tensor_of_state_is_state:
fixes A:: "complex Matrix.mat" and n m:: "nat"
assumes "state m A" and "n≥1"
shows "state (m*n) (A ⊗⇗n⇖)"
using assms(2)
proof(rule nat_induct_at_least)
show "state (m * 1) (A ⊗⇗1⇖)"
using one_tensor_is_id assms(1) by simp
fix n:: nat
assume "n ≥ 1" and IH:"state (m * n) (A ⊗⇗n⇖)"
then have "A ⊗⇗(Suc n)⇖ = A ⨂ (A ⊗⇗n⇖)"
moreover have "state (m*n + m) (A ⊗⇗(Suc n)⇖)"
then show "state (m*(Suc n)) (A ⊗⇗(Suc n)⇖)"
qed

text ‹
We prepare n+1 qubits. The first n qubits in the state $|0\rangle$, the last one in the state
$|1\rangle$.
›

abbreviation ψ⇩1⇩0:: "nat ⇒ complex Matrix.mat" where
"ψ⇩1⇩0 n ≡ Matrix.mat (2^n) 1 (λ(i,j). 1/(sqrt 2)^n)"

lemma ψ⇩1⇩0_values:
fixes i j n
assumes "i < dim_row (ψ⇩1⇩0 n)" and "j < dim_col (ψ⇩1⇩0 n)"
shows "(ψ⇩1⇩0 n) $$(i,j) = 1/(sqrt 2)^n" using assms case_prod_conv by simp text ‹H^{\otimes n} is applied to |0\rangle^{\otimes n}.› lemma H_on_ket_zero: shows "(H * |zero⟩) = ψ⇩1⇩0 1" proof fix i j:: nat assume "i < dim_row (ψ⇩1⇩0 1)" and "j < dim_col (ψ⇩1⇩0 1)" then have f1: "i ∈ {0,1} ∧ j = 0" by (simp add: less_2_cases) then show "(H * |zero⟩)$$ (i,j) = (ψ⇩1⇩0 1) $$(i,j)" by (auto simp add: times_mat_def scalar_prod_def H_def ket_vec_def) next show "dim_row (H * |zero⟩) = dim_row (ψ⇩1⇩0 1)" by (simp add: H_def) show "dim_col (H * |zero⟩) = dim_col (ψ⇩1⇩0 1)" using H_def by (simp add: ket_vec_def) qed lemma ψ⇩1⇩0_tensor: assumes "n ≥ 1" shows "(ψ⇩1⇩0 1) ⨂ (ψ⇩1⇩0 n) = (ψ⇩1⇩0 (Suc n))" proof have "dim_row (ψ⇩1⇩0 1) * dim_row (ψ⇩1⇩0 n) = 2^(Suc n)" by simp then show "dim_row ((ψ⇩1⇩0 1) ⨂ (ψ⇩1⇩0 n)) = dim_row (ψ⇩1⇩0 (Suc n))" by simp have "dim_col (ψ⇩1⇩0 1) * dim_col (ψ⇩1⇩0 n) = 1" by simp then show "dim_col ((ψ⇩1⇩0 1) ⨂ (ψ⇩1⇩0 n)) = dim_col (ψ⇩1⇩0 (Suc n))" by simp next fix i j:: nat assume a0: "i < dim_row (ψ⇩1⇩0 (Suc n))" and a1: "j < dim_col (ψ⇩1⇩0 (Suc n))" then have f0: "j = 0" and f1: "i < 2^(Suc n)" by auto then have f2:"(ψ⇩1⇩0 (Suc n))$$ (i,j) = 1/(sqrt 2)^(Suc n)"
using ψ⇩1⇩0_values[of "i" "(Suc n)" "j"] a0 a1 by simp
show "((ψ⇩1⇩0 1) ⨂ (ψ⇩1⇩0 n)) $$(i,j) = (ψ⇩1⇩0 (Suc n))$$ (i,j)"
proof (rule disjE) (*case distinction*)
show "i < dim_row (ψ⇩1⇩0 n) ∨ i ≥ dim_row (ψ⇩1⇩0 n)" by linarith
next (* case i < dim_row (ψ⇩1⇩0 n) *)
assume a2: "i < dim_row (ψ⇩1⇩0 n)"
then have "((ψ⇩1⇩0 1) ⨂ (ψ⇩1⇩0 n)) $$(i,j) = (ψ⇩1⇩0 1)$$ (0,0) * (ψ⇩1⇩0 n) $$(i,0)" using index_tensor_mat f0 assms by simp also have "... = 1/sqrt(2) * 1/(sqrt(2)^n)" using ψ⇩1⇩0_values a2 assms by simp finally show "((ψ⇩1⇩0 1) ⨂ (ψ⇩1⇩0 n))$$ (i,j) = (ψ⇩1⇩0 (Suc n)) $$(i,j)" using f2 divide_divide_eq_left power_Suc by simp next (* case i ≥ dim_row (ψ⇩1⇩0 n) *) assume "i ≥ dim_row (ψ⇩1⇩0 n)" then have "((ψ⇩1⇩0 1) ⨂ (ψ⇩1⇩0 n))$$ (i,0) = ((ψ⇩1⇩0 1) $$(1, 0)) * ((ψ⇩1⇩0 n)$$ ( i -dim_row (ψ⇩1⇩0 n),0))"
using index_tensor_mat_with_vec2_row_cond[of i "(ψ⇩1⇩0 1)" "(ψ⇩1⇩0 n)" ] a0 a1 f0
by (metis dim_col_mat(1) dim_row_mat(1) index_tensor_mat_with_vec2_row_cond power_Suc power_one_right)
then have "((ψ⇩1⇩0 1) ⨂ (ψ⇩1⇩0 n)) $$(i,0) = 1/sqrt(2) * 1/(sqrt 2)^n" using ψ⇩1⇩0_values[of "i -dim_row (ψ⇩1⇩0 n)" "n" "j"] a0 a1 by simp then show "((ψ⇩1⇩0 1) ⨂ (ψ⇩1⇩0 n))$$ (i,j) = (ψ⇩1⇩0 (Suc n)) $$(i,j)" using f0 f1 divide_divide_eq_left power_Suc by simp qed qed lemma ψ⇩1⇩0_tensor_is_state: assumes "n ≥ 1" shows "state n ( |zero⟩ ⊗⇗n⇖)" using iter_tensor_of_state_is_state ket_zero_is_state assms by fastforce lemma iter_tensor_of_H_is_gate: assumes "n ≥ 1" shows "gate n (H ⊗⇗n⇖)" using iter_tensor_of_gate_is_gate H_is_gate assms by fastforce lemma iter_tensor_of_H_on_zero_tensor: assumes "n ≥ 1" shows "(H ⊗⇗n⇖) * ( |zero⟩ ⊗⇗n⇖) = ψ⇩1⇩0 n" using assms proof(rule nat_induct_at_least) show "(H ⊗⇗1⇖) * ( |zero⟩ ⊗⇗1⇖) = ψ⇩1⇩0 1" using H_on_ket_zero by simp next fix n:: nat assume a0: "n ≥ 1" and IH: "(H ⊗⇗n⇖) * ( |zero⟩ ⊗⇗n⇖) = ψ⇩1⇩0 n" then have "(H ⊗⇗(Suc n)⇖) * ( |zero⟩ ⊗⇗(Suc n)⇖) = (H * |zero⟩) ⨂ ((H ⊗⇗n⇖) * ( |zero⟩ ⊗⇗n⇖))" using iter_tensor_mult_distr[of "n" "H" "|zero⟩"] a0 ket_vec_def H_def by(simp add: H_def) also have "... = (H * |zero⟩) ⨂ (ψ⇩1⇩0 n)" using IH by simp also have "... = (ψ⇩1⇩0 1) ⨂ (ψ⇩1⇩0 n)" using H_on_ket_zero by simp also have "... = (ψ⇩1⇩0 (Suc n))" using ψ⇩1⇩0_tensor a0 by simp finally show "(H ⊗⇗(Suc n)⇖) * ( |zero⟩ ⊗⇗(Suc n)⇖) = (ψ⇩1⇩0 (Suc n))" by simp qed lemma ψ⇩1⇩0_is_state: assumes "n ≥ 1" shows "state n (ψ⇩1⇩0 n)" using iter_tensor_of_H_is_gate ψ⇩1⇩0_tensor_is_state assms gate_on_state_is_state iter_tensor_of_H_on_zero_tensor assms by metis abbreviation ψ⇩1⇩1:: "complex Matrix.mat" where "ψ⇩1⇩1 ≡ Matrix.mat 2 1 (λ(i,j). if i=0 then 1/sqrt(2) else -1/sqrt(2))" lemma H_on_ket_one_is_ψ⇩1⇩1: shows "(H * |one⟩) = ψ⇩1⇩1" proof fix i j:: nat assume "i < dim_row ψ⇩1⇩1" and "j < dim_col ψ⇩1⇩1" then have "i ∈ {0,1} ∧ j = 0" by (simp add: less_2_cases) then show "(H * |one⟩)$$ (i,j) = ψ⇩1⇩1 $$(i,j)" by (auto simp add: times_mat_def scalar_prod_def H_def ket_vec_def) next show "dim_row (H * |one⟩) = dim_row ψ⇩1⇩1" by (simp add: H_def) next show "dim_col (H * |one⟩) = dim_col ψ⇩1⇩1" by (simp add: H_def ket_vec_def) qed abbreviation ψ⇩1:: "nat ⇒ complex Matrix.mat" where "ψ⇩1 n ≡ Matrix.mat (2^(n+1)) 1 (λ(i,j). if even i then 1/(sqrt 2)^(n+1) else -1/(sqrt 2)^(n+1))" lemma ψ⇩1_values_even[simp]: fixes i j n assumes "i < dim_row (ψ⇩1 n)" and "j < dim_col (ψ⇩1 n)" and "even i" shows "(ψ⇩1 n)$$ (i,j) = 1/(sqrt 2)^(n+1)"
using assms case_prod_conv by simp

lemma ψ⇩1_values_odd [simp]:
fixes i j n
assumes "i < dim_row (ψ⇩1 n)" and "j < dim_col (ψ⇩1 n)" and "odd i"
shows "(ψ⇩1 n) $$(i,j) = -1/(sqrt 2)^(n+1)" using assms case_prod_conv by simp lemma "ψ⇩1⇩0_tensor_ψ⇩1⇩1_is_ψ⇩1": assumes "n ≥ 1" shows "(ψ⇩1⇩0 n) ⨂ ψ⇩1⇩1 = ψ⇩1 n" proof show "dim_col ((ψ⇩1⇩0 n) ⨂ ψ⇩1⇩1) = dim_col (ψ⇩1 n)" by simp next show "dim_row ((ψ⇩1⇩0 n) ⨂ ψ⇩1⇩1) = dim_row (ψ⇩1 n)" by simp next fix i j:: nat assume a0: "i < dim_row (ψ⇩1 n)" and a1: "j < dim_col (ψ⇩1 n)" then have "i < 2^(n+1)" and "j = 0" by auto then have f0: "((ψ⇩1⇩0 n) ⨂ ψ⇩1⇩1)$$ (i,j) = 1/(sqrt 2)^n * ψ⇩1⇩1 $$(i mod 2, j)" using ψ⇩1⇩0_values[of "i div 2" n "j div 1"] a0 a1 by simp show "((ψ⇩1⇩0 n) ⨂ ψ⇩1⇩1)$$ (i,j) = (ψ⇩1 n) $$(i,j)" using f0 ψ⇩1_values_even ψ⇩1_values_odd a0 a1 by auto qed lemma ψ⇩1_is_state: assumes "n ≥ 1" shows "state (n+1) (ψ⇩1 n)" using assms ψ⇩1⇩0_tensor_ψ⇩1⇩1_is_ψ⇩1 ψ⇩1⇩0_is_state H_on_ket_one_is_state H_on_ket_one_is_ψ⇩1⇩1 tensor_state by metis abbreviation (in jozsa) ψ⇩2:: "complex Matrix.mat" where "ψ⇩2 ≡ Matrix.mat (2^(n+1)) 1 (λ(i,j). if even i then (-1)^f(i div 2)/(sqrt 2)^(n+1) else (-1)^(f(i div 2)+1)/(sqrt 2)^(n+1))" lemma (in jozsa) ψ⇩2_values_even [simp]: fixes i j assumes "i < dim_row ψ⇩2 " and "j < dim_col ψ⇩2" and "even i" shows "ψ⇩2$$ (i,j) = (-1)^f(i div 2)/(sqrt 2)^(n+1)"
using assms case_prod_conv by simp

lemma (in jozsa) ψ⇩2_values_odd [simp]:
fixes i j
assumes "i < dim_row ψ⇩2" and "j < dim_col ψ⇩2" and "odd i"
shows "ψ⇩2 $$(i,j) = (-1)^(f(i div 2)+1)/(sqrt 2)^(n+1)" using assms case_prod_conv by simp lemma (in jozsa) ψ⇩2_values_odd_hidden [simp]: assumes "2*k+1 < dim_row ψ⇩2" and "j < dim_col ψ⇩2" shows "ψ⇩2$$ (2*k+1,j) = ((-1)^(f((2*k+1) div 2)+1))/(sqrt 2)^(n+1)"
using assms by simp

lemma (in jozsa) snd_rep_of_ψ⇩2:
assumes "i < dim_row ψ⇩2"
shows "((1-f(i div 2)) + -f(i div 2)) * 1/(sqrt 2)^(n+1) = (-1)^f(i div 2)/(sqrt 2)^(n+1)"
and "(-(1-f(i div 2))+(f(i div 2)))* 1/(sqrt 2)^(n+1) = (-1)^(f(i div 2)+1)/(sqrt 2)^(n+1)"
proof-
have "i div 2 ∈ {i. i < 2 ^ n}"
using assms by auto
then have "real (Suc 0 - f (i div 2)) - real (f (i div 2)) = (- 1) ^ f (i div 2)"
using assms f_values by auto
thus "((1-f(i div 2)) + -f(i div 2)) * 1/(sqrt 2)^(n+1) = (-1)^f(i div 2)/(sqrt 2)^(n+1)" by auto
next
have "i div 2 ∈ {i. i < 2^n}"
using assms by simp
then have "(real (f (i div 2)) - real (Suc 0 - f (i div 2))) / (sqrt 2 ^ (n+1)) =
- ((- 1) ^ f (i div 2) / (sqrt 2 ^ (n+1)))"
using assms f_values by fastforce
then show "(-(1-f(i div 2))+(f(i div 2)))* 1/(sqrt 2)^(n+1) = (-1)^(f(i div 2)+1)/(sqrt 2)^(n+1)" by simp
qed

lemma (in jozsa) jozsa_transform_times_ψ⇩1_is_ψ⇩2:
shows "U⇩f * (ψ⇩1 n) = ψ⇩2"
proof
show "dim_row (U⇩f * (ψ⇩1 n)) = dim_row ψ⇩2" by simp
next
show "dim_col (U⇩f * (ψ⇩1 n)) = dim_col ψ⇩2" by simp
next
fix i j ::nat
assume a0: "i < dim_row ψ⇩2" and a1: "j < dim_col ψ⇩2"
then have f0:"i ∈ {0..2^(n+1)} ∧ j=0" by simp
then have f1: "i < dim_row U⇩f ∧ j < dim_col U⇩f " using a0 by simp
have f2: "i < dim_row (ψ⇩1 n) ∧ j < dim_col (ψ⇩1 n)" using a0 a1 by simp
show "(U⇩f * (ψ⇩1 n)) $$(i,j) = ψ⇩2$$ (i,j)"
proof (rule disjE)
show "even i ∨ odd i" by auto
next
assume a2: "even i"
then have "(U⇩f * (ψ⇩1 n)) $$(i,j) = (∑k ∈ {i,i+1}. U⇩f$$ (i,k) * (ψ⇩1 n) $$(k,j))" using f1 f2 U⇩f_mult_without_empty_summands_even[of i j "(ψ⇩1 n)"] by simp moreover have "U⇩f$$ (i,i) * (ψ⇩1 n) $$(i,j) = (1-f(i div 2))* 1/(sqrt 2)^(n+1)" using f0 f1 a2 by simp moreover have "U⇩f$$ (i,i+1) * (ψ⇩1 n) $$(i+1,j) = (-f(i div 2))* 1/(sqrt 2)^(n+1)" using f0 f1 a2 by auto ultimately have "(U⇩f * (ψ⇩1 n))$$ (i,j) = (1-f(i div 2))* 1/(sqrt 2)^(n+1) + (-f(i div 2))* 1/(sqrt 2)^(n+1)" by simp
also have "... = ((1-f(i div 2))+-f(i div 2)) * 1/(sqrt 2)^(n+1)"
by (metis (no_types, opaque_lifting) mult.right_neutral of_int_add of_int_of_nat_eq)
also have "... = ψ⇩2 $$(i,j)" using a0 a1 a2 snd_rep_of_ψ⇩2 by simp finally show "(U⇩f * (ψ⇩1 n))$$ (i,j) = ψ⇩2 $$(i,j)" by simp next assume a2: "odd i" then have f6: "i≥1" using linorder_not_less by auto have "(U⇩f * (ψ⇩1 n))$$ (i,j) = (∑k ∈ {i-1,i}. U⇩f $$(i,k) * (ψ⇩1 n)$$ (k,j))"
using f1 f2 a2 U⇩f_mult_without_empty_summands_odd[of i j "(ψ⇩1 n)"]
by (metis dim_row_mat(1) jozsa_transform_dim(2))
moreover have "(∑k ∈ {i-1,i}. U⇩f $$(i,k) * (ψ⇩1 n)$$ (k,j))
= U⇩f $$(i,i-1) * (ψ⇩1 n)$$ (i-1,j) +  U⇩f $$(i,i) * (ψ⇩1 n)$$ (i,j)"
using a2 f6 by simp
moreover have  "U⇩f $$(i,i) * (ψ⇩1 n)$$ (i,j) = (1-f(i div 2))* -1/(sqrt 2)^(n+1)"
using f1 f2 a2 by simp
moreover have "U⇩f $$(i,i-1) * (ψ⇩1 n)$$ (i-1,j) = f(i div 2)* 1/(sqrt 2)^(n+1)"
using a0 a1 a2 by simp
ultimately have "(U⇩f * (ψ⇩1 n)) $$(i,j) = (1-f(i div 2))* -1/(sqrt 2)^(n+1) +(f(i div 2))* 1/(sqrt 2)^(n+1)" using of_real_add by simp also have "... = (-(1-f(i div 2)) + (f(i div 2))) * 1/(sqrt 2)^(n+1)" by (metis (no_types, opaque_lifting) mult.right_neutral add_divide_distrib mult_minus1_right of_int_add of_int_of_nat_eq) also have "... = (-1)^(f(i div 2)+1)/(sqrt 2)^(n+1)" using a0 a1 a2 snd_rep_of_ψ⇩2 by simp finally show "(U⇩f * (ψ⇩1 n))$$ (i,j) = ψ⇩2 $$(i,j)" using a0 a1 a2 by simp qed qed lemma (in jozsa) ψ⇩2_is_state: shows "state (n+1) ψ⇩2" using jozsa_transform_times_ψ⇩1_is_ψ⇩2 jozsa_transform_is_gate ψ⇩1_is_state dim gate_on_state_is_state by fastforce text ‹@{text "H^⇩⊗ n"} is the result of taking the nth tensor product of H› abbreviation iter_tensor_of_H_rep:: "nat ⇒ complex Matrix.mat" ("H^⇩⊗ _") where "iter_tensor_of_H_rep n ≡ Matrix.mat (2^n) (2^n) (λ(i,j).(-1)^(i ⋅⇘n⇙ j)/(sqrt 2)^n)" lemma tensor_of_H_values [simp]: fixes n i j:: nat assumes "i < dim_row (H^⇩⊗ n)" and "j < dim_col (H^⇩⊗ n)" shows "(H^⇩⊗ n)$$ (i,j) = (-1)^(i ⋅⇘n⇙ j)/(sqrt 2)^n"
using assms by simp

lemma dim_row_of_iter_tensor_of_H [simp]:
assumes "n ≥ 1"
shows "1 < dim_row (H^⇩⊗ n)"
using assms by(metis One_nat_def Suc_1 dim_row_mat(1) le_trans lessI linorder_not_less one_less_power)

lemma iter_tensor_of_H_fst_pos:
fixes n i j:: nat
assumes "i < 2^n ∨ j < 2^n" and "i < 2^(n+1) ∧ j < 2^(n+1)"
shows "(H^⇩⊗ (Suc n)) $$(i,j) = 1/sqrt(2) * ((H^⇩⊗ n)$$ (i mod 2^n, j mod 2^n))"
proof-
have "(H^⇩⊗ (Suc n)) $$(i,j) = (-1)^(bip i (Suc n) j)/(sqrt 2)^(Suc n)" using assms by simp moreover have "bip i (Suc n) j = bip (i mod 2^n) n (j mod 2^n)" using bitwise_inner_prod_fst_el_0 assms(1) by simp ultimately show ?thesis using bitwise_inner_prod_def by simp qed lemma iter_tensor_of_H_fst_neg: fixes n i j:: nat assumes "i ≥ 2^n ∧ j ≥ 2^n" and "i < 2^(n+1) ∧ j < 2^(n+1)" shows "(H^⇩⊗ (Suc n))$$ (i,j) = -1/sqrt(2) * (H^⇩⊗ n) $$(i mod 2^n, j mod 2^n)" proof- have "(H^⇩⊗ (Suc n))$$ (i,j) = (-1)^(bip i (n+1) j)/(sqrt 2)^(n+1)"
using assms(2) by simp
moreover have "bip i (n+1) j = 1 + bip (i mod 2^n) n (j mod 2^n)"
using bitwise_inner_prod_fst_el_is_1 assms by simp
ultimately show ?thesis by simp
qed

lemma H_tensor_iter_tensor_of_H:
fixes n:: nat
shows  "(H ⨂ H^⇩⊗ n) = H^⇩⊗ (Suc n)"
proof
fix i j:: nat
assume a0: "i < dim_row (H^⇩⊗ (Suc n))" and a1: "j < dim_col (H^⇩⊗ (Suc n))"
then have f0: "i ∈ {0..<2^(n+1)} ∧ j ∈ {0..<2^(n+1)}" by simp
then have f1: "(H ⨂ H^⇩⊗ n) $$(i,j) = H$$ (i div (dim_row (H^⇩⊗ n)),j div (dim_col (H^⇩⊗ n)))
* (H^⇩⊗ n) $$(i mod (dim_row (H^⇩⊗ n)),j mod (dim_col (H^⇩⊗ n)))" by (simp add: H_without_scalar_prod) show "(H ⨂ H^⇩⊗ n)$$ (i,j) = (H^⇩⊗ (Suc n)) $$(i,j)" proof (rule disjE) show "(i < 2^n ∨ j < 2^n) ∨ ¬(i < 2^n ∨ j < 2^n)" by auto next assume a2: "(i < 2^n ∨ j < 2^n)" then have "(H^⇩⊗ (Suc n))$$ (i,j) = 1/sqrt(2) * ((H^⇩⊗ n) $$(i mod 2^n, j mod 2^n))" using a0 a1 f0 iter_tensor_of_H_fst_pos by (metis (mono_tags, lifting) atLeastLessThan_iff) moreover have "H$$ (i div (dim_row (H^⇩⊗ n)),j div (dim_col (H^⇩⊗ n))) = 1/sqrt 2"
using a0 a1 f0 H_without_scalar_prod H_values a2
by (metis (no_types, lifting) dim_col_mat(1) dim_row_mat(1) div_less le_eq_less_or_eq
ultimately show "(H ⨂ H^⇩⊗ n) $$(i,j) = (H^⇩⊗ (Suc n))$$ (i,j)"
using f1 by simp
next
assume a2: "¬(i < 2^n ∨ j < 2^n)"
then have "i ≥ 2^n ∧ j ≥ 2^n" by simp
then have f2:"(H^⇩⊗ (Suc n)) $$(i,j) = -1/sqrt(2) * ((H^⇩⊗ n)$$ (i mod 2^n, j mod 2^n))"
using a0 a1 f0 iter_tensor_of_H_fst_neg by simp
have "i div (dim_row (H^⇩⊗ n)) =1" and "j div (dim_row (H^⇩⊗ n)) = 1"
using a2 a0 a1 by auto
then have "H $$(i div (dim_row (H^⇩⊗ n)),j div (dim_col (H^⇩⊗ n))) = -1/sqrt 2" using a0 a1 f0 H_values_right_bottom[of "i div (dim_row (H^⇩⊗ n))" "j div (dim_col (H^⇩⊗ n))"] a2 by fastforce then show "(H ⨂ H^⇩⊗ n)$$ (i,j) = (H^⇩⊗ (Suc n)) $$(i,j)" using f1 f2 by simp qed next show "dim_row (H ⨂ H^⇩⊗ n) = dim_row (H^⇩⊗ (Suc n))" by (simp add: H_without_scalar_prod) next show "dim_col (H ⨂ H^⇩⊗ n) = dim_col (H^⇩⊗ (Suc n))" by (simp add: H_without_scalar_prod) qed text ‹ We prove that @{term "H^⇩⊗ n"} is indeed the matrix representation of @{term "H ⊗⇗n⇖"}, the iterated tensor product of the Hadamard gate H. › lemma one_tensor_of_H_is_H: shows "(H^⇩⊗ 1) = H" proof(rule eq_matI) show "dim_row (H^⇩⊗ 1) = dim_row H" by (simp add: H_without_scalar_prod) show "dim_col (H^⇩⊗ 1) = dim_col H" by (simp add: H_without_scalar_prod) next fix i j:: nat assume a0:"i < dim_row H" and a1:"j < dim_col H" then show "(H^⇩⊗ 1)$$ (i,j) = H $$(i,j)" proof- have "(H^⇩⊗ 1)$$ (0, 0) = 1/sqrt(2)"
using bitwise_inner_prod_def bin_rep_def by simp
moreover have "(H^⇩⊗ 1) $$(0,1) = 1/sqrt(2)" using bitwise_inner_prod_def bin_rep_def by simp moreover have "(H^⇩⊗ 1)$$ (1,0) = 1/sqrt(2)"
using bitwise_inner_prod_def bin_rep_def by simp
moreover have "(H^⇩⊗ 1) $$(1,1) = -1/sqrt(2)" using bitwise_inner_prod_def bin_rep_def by simp ultimately show "(H^⇩⊗ 1)$$ (i,j) = H $$(i,j)" using a0 a1 H_values H_values_right_bottom by (metis (no_types, lifting) H_without_scalar_prod One_nat_def dim_col_mat(1) dim_row_mat(1) divide_minus_left less_2_cases) qed qed lemma iter_tensor_of_H_rep_is_correct: fixes n:: nat assumes "n ≥ 1" shows "(H ⊗⇗n⇖) = H^⇩⊗ n" using assms proof(rule nat_induct_at_least) show "(H ⊗⇗1⇖) = H^⇩⊗ 1" using one_tensor_is_id one_tensor_of_H_is_H by simp next fix n:: nat assume a0:"n ≥ 1" and IH:"(H ⊗⇗n⇖) = H^⇩⊗ n" then have "(H ⊗⇗(Suc n)⇖) = H ⨂ (H ⊗⇗n⇖)" using iter_tensor_suc Nat.Suc_eq_plus1 by metis also have "... = H ⨂ (H^⇩⊗ n)" using IH by simp also have "... = H^⇩⊗ (Suc n)" using a0 H_tensor_iter_tensor_of_H by simp finally show "(H ⊗⇗(Suc n)⇖) = H^⇩⊗ (Suc n)" by simp qed text ‹@{text "HId^⇩⊗ 1"} is the result of taking the tensor product of the nth tensor of H and Id 1 › abbreviation tensor_of_H_tensor_Id:: "nat ⇒ complex Matrix.mat" ("HId^⇩⊗ _") where "tensor_of_H_tensor_Id n ≡ Matrix.mat (2^(n+1)) (2^(n+1)) (λ(i,j). if (i mod 2 = j mod 2) then (-1)^((i div 2) ⋅⇘n⇙ (j div 2))/(sqrt 2)^n else 0)" lemma mod_2_is_both_even_or_odd: "((even i ∧ even j) ∨ (odd i ∧ odd j)) ⟷ (i mod 2 = j mod 2)" by (metis even_iff_mod_2_eq_zero odd_iff_mod_2_eq_one) lemma HId_values [simp]: assumes "n ≥ 1" and "i < dim_row (HId^⇩⊗ n)" and "j < dim_col (HId^⇩⊗ n)" shows "even i ∧ even j ⟶ (HId^⇩⊗ n)$$ (i,j) = (-1)^((i div 2) ⋅⇘n⇙ (j div 2))/(sqrt 2)^n"
and "odd i ∧ odd j ⟶ (HId^⇩⊗ n) $$(i,j) = (-1)^((i div 2) ⋅⇘n⇙ (j div 2))/(sqrt 2)^n" and "(i mod 2 = j mod 2) ⟶ (HId^⇩⊗ n)$$ (i,j) = (-1)^((i div 2) ⋅⇘n⇙ (j div 2))/(sqrt 2)^n"
and "¬(i mod 2 = j mod 2) ⟶ (HId^⇩⊗ n)  (i,j) = 0"
using assms mod_2_is_both_even_or_odd by auto

lemma