Theory Run_Pure_B
theory Run_Pure_B
imports Definition_Pure_O2H
begin
unbundle cblinfun_syntax
unbundle lattice_syntax
unbundle register_syntax
context pure_o2h
begin
section ‹Defining and Representing the Adversary $B$›
text ‹For the proof of the O2H, the final adversary $B$ is restricted to information on the set $S$.
That means, $B$ takes note in a separate register of type ‹'l› weather a value in $S$ was
queried and in which step with a unitary ‹U_S›.
›
text ‹Given the initial state ‹init ⊗⇩s ket 0 :: 'mem × 'l›, we run the adversary with counting
by performing consecutive bit-flips.
‹run_B_upto n› is the function that allows the adversary ‹n› calls to the query oracle.
‹run_B› allows exactly ‹d› query calls.
The final state $\Psi_{right}$ as in the paper is then ‹run_B›.›
definition ‹run_B_upto n = run_pure_adv n (λi. UA i ⊗⇩o id_cblinfun) (US S) init_B X_for_B Y_for_B H›
definition ‹run_B = run_pure_adv d (λi. UA i ⊗⇩o id_cblinfun) (US S) init_B X_for_B Y_for_B H›
lemma run_B_altdef: "run_B = run_B_upto d"
unfolding run_B_def run_B_upto_def by auto
lemma run_B_upto_I:
"run_B_upto (Suc n) = (UA (Suc n) ⊗⇩o id_cblinfun) *⇩V (X_for_B;Y_for_B) (Uquery H) *⇩V
US S n *⇩V run_B_upto n"
unfolding run_B_upto_def by auto
text ‹This version of the O2H is only for pure states.
Therefore, the norm of states is always $1$.›
lemma norm_run_B_upto:
assumes "n<d+1"
shows "norm (run_B_upto n) ≤ 1"
using assms proof (induct n)
case 0
then show ?case unfolding run_B_upto_def init_B_def using norm_UA_0_init
by (auto simp add: tensor_op_ell2 norm_tensor_ell2 norm_init)
next
case (Suc n)
have "norm (run_B_upto (Suc n)) ≤ norm ((UA (Suc n) ⊗⇩o (id_cblinfun::'l update))) *
norm ((X_for_B;Y_for_B) (Uquery H) *⇩V US S n *⇩V
run_pure_adv n (λi. UA i ⊗⇩o id_cblinfun) (US S) init_B X_for_B Y_for_B H)"
unfolding run_B_upto_def run_pure_adv.simps using norm_cblinfun by blast
also have "… ≤ norm ((UA (Suc n) ⊗⇩o (id_cblinfun::'l update))) *
norm (run_pure_adv n (λi. UA i ⊗⇩o id_cblinfun) (US S) init_B X_for_B Y_for_B H)"
by (simp add: iso_H_B isometry_US isometry_preserves_norm norm_isometry)
also have "… ≤ 1" using norm_UA Suc by (simp add: mult_le_one run_B_upto_def tensor_op_norm)
finally show ?case by linarith
qed
lemma norm_run_B:
"norm run_B ≤ 1"
unfolding run_B_altdef using norm_run_B_upto by auto
subsection ‹Representing the run of Adversary $B$ as a finite sum›
text ‹How the state after the $n$-th query behaves with respect to projections.›
lemma run_B_upto_proj_not_valid:
assumes "n≤d"
shows "Proj_ket_set (- Collect blog) *⇩V run_B_upto n = 0"
using le0[of n] proof (induct rule: dec_induct)
case base
have "proj_classical_set (- Collect blog) *⇩V ket empty = 0"
by (intro proj_classical_set_not_elem)(auto simp add: blog_empty)
then show ?case unfolding run_B_upto_def init_B_def Proj_ket_set_def
by (auto simp add: tensor_op_ell2)
next
case (step m)
have 1: "Proj_ket_set (- Collect blog) *⇩V run_B_upto (Suc m) =
(UA (Suc m) ⊗⇩o id_cblinfun) *⇩V (X_for_B;Y_for_B) (Uquery H) *⇩V
Proj_ket_set (- Collect blog) *⇩V
US S m *⇩V run_B_upto m" unfolding Proj_ket_set_def
by (metis UqueryH_tensor_id_cblinfunB run_B_upto_I tensor_op_padding tensor_op_padding')
have "m<d" using step assms by auto
have "(S_embed S ⊗⇩o (proj_classical_set (- Collect blog) o⇩C⇩L Ub m)) *⇩V run_B_upto m = 0"
using step(3) unfolding Proj_ket_set_def by (subst tensor_op_padding,
subst proj_classical_set_not_blog_Ub[OF ‹m<d›])
(metis (no_types, lifting) cblinfun.zero_right cblinfun_apply_cblinfun_compose
cblinfun_compose_id_left comp_tensor_op)
moreover have "(not_S_embed S ⊗⇩o proj_classical_set (- Collect blog)) *⇩V run_B_upto m = 0"
using step(3) unfolding Proj_ket_set_def by (subst tensor_op_padding) auto
ultimately have 2: "Proj_ket_set (- Collect blog) *⇩V US S m *⇩V run_B_upto m =
(S_embed S ⊗⇩o Ub m) *⇩V Proj_ket_set (- Collect blog) *⇩V run_B_upto m +
(not_S_embed S ⊗⇩o id_cblinfun) *⇩V Proj_ket_set (- Collect blog) *⇩V run_B_upto m"
using proj_classical_set_not_blog_Ub[symmetric] step assms unfolding US_def Proj_ket_set_def
by (auto simp add: cblinfun.add_left cblinfun.add_right comp_tensor_op
cblinfun_apply_cblinfun_compose[symmetric] simp del: cblinfun_apply_cblinfun_compose)
show ?case by (subst 1, subst 2) (auto simp add: step(3))
qed
lemma orth_run_B_upto:
fixes C :: "'mem update"
assumes y: "y ∈ has_bits {Suc m..<d}" and m: "m<d"
shows "is_orthogonal ((C ⊗⇩o id_cblinfun) *⇩V run_B_upto m) (x ⊗⇩s ket (list_to_l y))"
using le0 y proof (induction m arbitrary: C y rule: Nat.dec_induct)
case base
have "empty ≠ list_to_l y" using base.prems has_bits_def has_bits_not_empty by fastforce
then show ?case unfolding run_B_upto_def init_B_def by (auto simp add: tensor_op_ell2)
next
case (step n)
define A where "A = C o⇩C⇩L UA (Suc n) o⇩C⇩L (X;Y) (Uquery H) o⇩C⇩L S_embed S"
define B where "B = C o⇩C⇩L UA (Suc n) o⇩C⇩L (X;Y) (Uquery H) o⇩C⇩L not_S_embed S"
then have Suc: "(C ⊗⇩o id_cblinfun) *⇩V run_B_upto (Suc n) =
(id_cblinfun ⊗⇩o Ub n) *⇩V (A ⊗⇩o id_cblinfun) *⇩V run_B_upto n +
(B ⊗⇩o id_cblinfun) *⇩V run_B_upto n"
apply (subst tensor_op_padding'[symmetric])
unfolding run_B_upto_I UqueryH_tensor_id_cblinfunB US_def A_def B_def
unfolding cblinfun.add_left cblinfun.add_right
by (metis (mono_tags, lifting) cblinfun_apply_cblinfun_compose
cblinfun_compose_id_left comp_tensor_op)
have iso: "isometry (id_cblinfun ⊗⇩o Ub n)" by (simp add: isometry_Ub)
have len_y: "length y = d" using step unfolding has_bits_def len_d_lists_def by auto
have blog_y: "blog (list_to_l y)" by (simp add: blog_list_to_l len_y)
have y_has_bits: "y ∈ has_bits {Suc n..<d}"
by (metis Set.basic_monos(7) Suc_n_not_le_n has_bits_incl ivl_subset step(4) nat_le_linear)
have range: "y[d-n-1:=¬y!(d-n-1)] ∈ has_bits {Suc n..<d}"
by (intro has_bits_not_elem) (use step y_has_bits m len_y len_d_lists_def in ‹auto›)
have no_flip: "((id_cblinfun ⊗⇩o Ub n) *⇩V (A ⊗⇩o id_cblinfun) *⇩V run_B_upto n) ∙⇩C
(x ⊗⇩s ket (list_to_l y)) = 0" (is "?left = 0")
proof -
have "n<d" using assms(2) step(2) by force
have "?left = ((id_cblinfun ⊗⇩o Ub n) *⇩V (A ⊗⇩o id_cblinfun) *⇩V run_B_upto n) ∙⇩C
((id_cblinfun ⊗⇩o Ub n) *⇩V (id_cblinfun ⊗⇩o Ub n) *⇩V (x ⊗⇩s ket (list_to_l y)))"
by (simp add: Ub_ket flip_flip[OF ‹n<d› blog_y] tensor_op_ell2)
also have "… = ((A ⊗⇩o id_cblinfun) *⇩V run_B_upto n) ∙⇩C
((id_cblinfun ⊗⇩o Ub n) *⇩V (x ⊗⇩s ket (list_to_l y)))"
using isometry_cinner_both_sides[OF iso] by auto
also have "… = ((A ⊗⇩o id_cblinfun) *⇩V run_B_upto n) ∙⇩C
(x ⊗⇩s ket (flip n (list_to_l y)))" by (simp add: Ub_ket tensor_op_ell2)
also have "… = ((A ⊗⇩o id_cblinfun) *⇩V run_B_upto n) ∙⇩C
(x ⊗⇩s ket (list_to_l (y[d-n-1:=¬y!(d-n-1)])))"
using ‹n < d› flip_list_to_l le_eq_less_or_eq len_y by presburger
also have "… = 0" by (intro step(3)) (rule range)
finally show ?thesis by auto
qed
show ?case using y_has_bits unfolding Suc cinner_add_left
by (subst no_flip, subst step(3))(use step in ‹auto›)
qed
lemma orth_run_B_upto_ket:
assumes y: "y ∈ has_bits {Suc m..<d}" and Sucm: "Suc m<d"
shows "is_orthogonal (run_B_upto m) (x ⊗⇩s ket (list_to_l y))"
proof -
have m: "m<d" using assms(2) by auto
have id: "run_B_upto m = (id_cblinfun ⊗⇩o id_cblinfun) *⇩V run_B_upto m" by auto
then show ?thesis
by (subst id, intro orth_run_B_upto[OF _ m]) (use assms in ‹auto›)
qed
lemma orth_run_B_upto_flip:
assumes y: "y ∈ has_bits {Suc m..<d}" and Sucm: "Suc m<d"
shows "is_orthogonal (run_B_upto m) (x ⊗⇩s ket (flip m (list_to_l y)))"
proof -
have len_d: "y ∈ len_d_lists" using y unfolding has_bits_def by auto
then have m: "m < length y" by (simp add: Suc_lessD Sucm len_d_lists_def)
have yd: "length y ≤ d" using y has_bits_def len_d_lists_def by auto
have id: "run_B_upto m = (id_cblinfun ⊗⇩o id_cblinfun) *⇩V run_B_upto m" by auto
have range: "y[d - m - 1 := ¬ y ! (d - m - 1)] ∈ has_bits {Suc m..<d}"
by (intro has_bits_not_elem) (use y Sucm len_d in ‹auto›)
then show ?thesis
by (subst flip_list_to_l[OF m yd], subst id, intro orth_run_B_upto)
(use len_d len_d_lists_def Sucm in ‹auto›)
qed
lemma run_B_upto_proj_over:
assumes "n≤d"
shows "Proj_ket_set (list_to_l ` has_bits {n..<d}) *⇩V run_B_upto n = 0"
proof (cases "n=d")
case True then show ?thesis unfolding ‹n=d› Proj_ket_set_def proj_classical_set_def by auto
next
case False
then have "n<d" using assms by auto
show ?thesis
using le0[of n] proof (induct rule: dec_induct)
case base
have "empty ∉ list_to_l ` has_bits {0..<d}" using has_bits_def has_bits_not_empty by fastforce
then have "proj_classical_set (list_to_l ` has_bits {0..<d}) *⇩V ket (empty) = 0"
by (intro proj_classical_set_not_elem) auto
then show ?case unfolding run_B_upto_def init_B_def Proj_ket_set_def
by (auto simp add: tensor_op_ell2)
next
case (step m)
then have "m<d" using assms by auto
then have "Suc m≤d" by auto
have "Suc m < d" using ‹n < d› step(2) by linarith
have 1: "Proj_ket_set (list_to_l ` has_bits {Suc m..<d}) *⇩V run_B_upto (Suc m) =
(UA (Suc m) ⊗⇩o id_cblinfun) *⇩V (X_for_B;Y_for_B) (Uquery H) *⇩V
Proj_ket_set (list_to_l ` has_bits {Suc m..<d}) *⇩V
US S m *⇩V run_B_upto m" unfolding Proj_ket_set_def
by (smt (verit, del_insts) UqueryH_tensor_id_cblinfunB cblinfun_apply_cblinfun_compose
cblinfun_compose_id_left cblinfun_compose_id_right comp_tensor_op run_B_upto_def
run_pure_adv.simps(2))
have 2: "Proj_ket_set (list_to_l ` has_bits {Suc m..<d}) *⇩V US S m *⇩V run_B_upto m =
(S_embed S ⊗⇩o Ub m) *⇩V Proj_ket_set (flip m ` list_to_l ` has_bits {Suc m..<d}) *⇩V run_B_upto m +
(not_S_embed S ⊗⇩o id_cblinfun) *⇩V Proj_ket_set (list_to_l ` has_bits {Suc m..<d}) *⇩V run_B_upto m"
using proj_classical_set_over_Ub[OF ‹Suc m≤d›, symmetric] step assms
unfolding US_def Proj_ket_set_def
by (auto simp add: cblinfun.add_left cblinfun.add_right comp_tensor_op
cblinfun_apply_cblinfun_compose[symmetric] simp del: cblinfun_apply_cblinfun_compose)
have "Proj_ket_set (flip m ` list_to_l ` has_bits {Suc m..<d}) *⇩V run_B_upto m = 0"
proof -
have "Proj_ket_set (flip m ` list_to_l ` has_bits {Suc m..<d}) *⇩V run_B_upto m =
Proj (⊤ ⊗⇩S ccspan (ket ` flip m ` list_to_l ` has_bits {Suc m..<d})) *⇩V run_B_upto m"
by (simp add: Proj_on_own_range is_Proj_tensor_op proj_classical_set_def
tensor_ccsubspace_via_Proj Proj_ket_set_def)
also have "… = 0" by (intro Proj_0_compl, unfold ccspan_UNIV[symmetric],
subst tensor_ccsubspace_ccspan,intro mem_ortho_ccspanI)
(auto intro!: orth_run_B_upto_flip simp add: ‹Suc m<d›)
finally show ?thesis by auto
qed
then have 3: "(S_embed S ⊗⇩o Ub m) *⇩V Proj_ket_set (flip m ` list_to_l ` has_bits {Suc m..<d})
*⇩V run_B_upto m = 0"
by (metis (no_types, lifting) cblinfun.real.zero_right cblinfun_apply_cblinfun_compose)
have "Proj_ket_set (list_to_l ` has_bits {Suc m..<d}) *⇩V run_B_upto m = 0"
proof -
have "Proj_ket_set (list_to_l ` has_bits {Suc m..<d}) *⇩V run_B_upto m =
Proj (⊤ ⊗⇩S ccspan (ket ` list_to_l ` has_bits {Suc m..<d})) *⇩V run_B_upto m"
by (simp add: Proj_on_own_range is_Proj_tensor_op proj_classical_set_def
tensor_ccsubspace_via_Proj Proj_ket_set_def)
also have "… = 0" by (intro Proj_0_compl, unfold ccspan_UNIV[symmetric],
subst tensor_ccsubspace_ccspan,intro mem_ortho_ccspanI)
(auto intro!: orth_run_B_upto_ket simp add: ‹Suc m<d›)
finally show ?thesis by auto
qed
then have 4: "(not_S_embed S ⊗⇩o id_cblinfun) *⇩V Proj_ket_set (list_to_l ` has_bits {Suc m..<d}) *⇩V
run_B_upto m = 0" by (subst tensor_op_padding) auto
show ?case by (subst 1, subst 2, subst 3, subst 4) auto
qed
qed
text ‹How ‹Ψs› relate to ‹run_B›. We can write ‹run_B› as a sum counting over all valid
ket states in the counting register.›
lemma not_empty_list_nth:
assumes "x∈len_d_lists"
shows "x ≠ empty_list ⟷ (∃i<d. x!i)"
using assms unfolding len_d_lists_def empty_list_def by (simp add: list_eq_iff_nth_eq)
text ‹First we show the mere existence of such a form.›
lemma run_B_upto_sum:
assumes "n<d"
shows "∃v. run_B_upto n = (∑i∈has_bits_upto n. v i ⊗⇩s ket (list_to_l i))"
using le0[of n] assms proof (induct n rule: Nat.dec_induct)
case base
have "∃xa∈{0..<d}. x ! (d - Suc xa)"
if "x ≠ empty_list" "x ∈ len_d_lists" for x :: "bool list"
using not_empty_list_nth[OF that(2)] that(1) by (metis Suc_pred atLeast0LessThan
diff_diff_cancel diff_less_Suc lessThan_iff less_or_eq_imp_le not_less_eq zero_less_diff)
then have rew: "has_bits_upto 0 = {empty_list}"
unfolding has_bits_upto_def has_bits_def len_d_lists_def empty_list_def by auto
show ?case by (subst rew, unfold run_B_upto_def init_B_def)
(auto simp add: empty_list_to_l tensor_op_ell2)
next
case (step n)
let ?upto_n = "has_bits_upto n"
let ?upto_Suc_n = "has_bits_upto (Suc n)"
let ?only_n = "has_bits {n} - has_bits{Suc n..<d}"
have [simp]: "n<d" by(rule Suc_lessD[OF step(4)])
from step obtain v where v: "run_B_upto n =
(∑i∈?upto_n. v i ⊗⇩s ket (list_to_l i))"
using Suc_lessD by presburger
define v1 where "v1 i = not_S_embed S *⇩V (v i)" for i
define v2 where "v2 i = S_embed S *⇩V (v i)" for i
have US_ket: "US S n *⇩V (v i) ⊗⇩s ket (list_to_l i) =
v1 i ⊗⇩s ket (list_to_l i) + v2 i ⊗⇩s ket (flip n (list_to_l i))"
if "i∈?upto_n" for i unfolding US_ket_only01
by (auto simp add: that v1_def v2_def)
define v' where "v' i = (if i ∈ ?upto_n
then ((UA (Suc n)) *⇩V (X;Y) (Uquery H) *⇩V v1 i)
else ((UA (Suc n)) *⇩V (X;Y) (Uquery H) *⇩V v2 (i[d-n-1:= ¬i!(d-n-1)])))" for i
have "(∑i∈?upto_n.
((UA (Suc n)) *⇩V (X;Y) (Uquery H) *⇩V v1 i) ⊗⇩s ket (list_to_l i) +
((UA (Suc n)) *⇩V (X;Y) (Uquery H) *⇩V v2 i) ⊗⇩s ket (flip n (list_to_l i))) =
(∑i∈?upto_Suc_n. v' i ⊗⇩s ket (list_to_l i))" (is "?l = ?r")
proof -
have left: "?l = (∑i∈?upto_n. ((UA (Suc n)) *⇩V (X;Y) (Uquery H) *⇩V v1 i) ⊗⇩s ket (list_to_l i)) +
(∑i∈?upto_n. (UA (Suc n) *⇩V (X;Y) (Uquery H) *⇩V v2 i) ⊗⇩s ket (flip n (list_to_l i)))"
(is "?l = ?fst + ?snd" )
by (subst sum.distrib)(auto intro!: sum.cong)
have fst: "?fst = (∑i∈?upto_n. v' i ⊗⇩s ket (list_to_l i))" unfolding v'_def by auto
let ?reindex = "(λk. k[d-n-1:= ¬k!(d-n-1)])"
have reindex_idem: "?reindex (?reindex l) = l" if "l∈len_d_lists" for l
by (smt (verit, best) list_update_id list_update_overwrite)
have snd': "?snd = (∑i∈?reindex` ?upto_n.
((UA (Suc n)) *⇩V (X;Y) (Uquery H) *⇩V v2 (?reindex i)) ⊗⇩s
ket (list_to_l i))"
proof (subst sum.reindex, goal_cases)
case 1
then show ?case unfolding has_bits_upto_def
by (metis (no_types, lifting) inj_on_def inj_on_diff reindex_idem)
next
case 2
then show ?case
proof (intro sum.cong, goal_cases)
case (2 x)
have one: "n < length x" using ‹n<d› 2 has_bits_upto_def len_d_lists_def by auto
have two: "length x ≤ d" using 2 len_d_lists_def has_bits_upto_def by auto
have three: "x ∈ len_d_lists" using 2 has_bits_upto_def by auto
show ?case by (subst flip_list_to_l[OF one two])
(use reindex_idem[OF three] three in ‹auto simp add: len_d_lists_def›)
qed simp
qed
have set_rew: "?reindex ` ?upto_n = ?only_n"
proof -
have "x∈?only_n" if "x∈?reindex ` ?upto_n" for x
proof -
have len_d_x: "x ∈ len_d_lists" using that unfolding len_d_lists_def has_bits_upto_def by auto
obtain x' where x':"x = ?reindex x' " "x'∈?upto_n" using ‹x ∈ ?reindex ` ?upto_n› by blast
then have len_x': "length x' = d" unfolding len_d_lists_def has_bits_upto_def by auto
have "¬ x'!(d-n-1)" by (intro has_bits_upto_elem [OF x'(2)]) auto
then have "x!(d-n-1)" unfolding x' by (subst nth_list_update_eq)(auto simp add: d_gr_0 len_x')
then have a: "x∈has_bits {n}" unfolding has_bits_def using len_d_x by auto
have "x' ∈ has_bits_upto (Suc n)" using has_bits_split_Suc has_bits_upto_def x'(2) by force
then have "¬ x'!(d-i-1)" if "i∈{Suc n..<d}" for i
by (intro has_bits_elem[of x' "{Suc n..<d}"], unfold has_bits_upto_def[symmetric])
(use that in ‹auto›)
then have "∀i∈{Suc n..<d}. ¬ x!(d-i-1)" using x'(1) by fastforce
then have b: "x∉has_bits {Suc n..<d}" by (simp add: has_bits_def)
show ?thesis using a b by auto
qed
moreover have"x∈?reindex ` ?upto_n" if "x∈?only_n" for x
proof -
have len_d_x: "x ∈ len_d_lists" using that unfolding has_bits_def len_d_lists_def by auto
define x' where x':"x' = ?reindex x "
then have "x'∈?reindex ` ?only_n" using ‹x ∈ ?only_n› reindex_idem by auto
then have len_d_x': "x' ∈ len_d_lists" using that
unfolding has_bits_def len_d_lists_def by auto
have "¬x'!(d-i-1)" if "i∈{n..<d}" for i
proof (cases "i = n")
case True
have ineq: "d - n - 1 < length x" using len_d_x len_d_lists_def by (simp add: d_gr_0)
have "x∈has_bits {n}" using ‹x ∈ ?only_n› by blast
then have "x ! (d-n-1)" unfolding has_bits_def by auto
then show ?thesis unfolding True x' by (subst nth_list_update_eq) (use ineq in ‹auto›)
next
case False
have set: "i∈{Suc n..<d}" using False ‹i∈{n..<d}› by auto
have "x∉has_bits {Suc n..<d}" using ‹x ∈ ?only_n› by auto
then have "¬x!(d-i-1)" using has_bits_def set using len_d_x by blast
moreover have "x!(d-i-1) = x'!(d-i-1)" using False ‹i∈{n..<d}› using x' by force
ultimately show ?thesis by auto
qed
then have "x'∉ has_bits {n..<d}" by (simp add: has_bits_def)
then have "x'∈?upto_n" using len_d_x' has_bits_upto_def by auto
then show ?thesis using x'
by (metis (no_types, lifting) image_iff len_d_x reindex_idem)
qed
ultimately show ?thesis by auto
qed
have snd: "?snd = (∑i∈?only_n. v' i ⊗⇩s ket (list_to_l i))"
unfolding v'_def snd' using set_rew
by (auto intro!: sum.cong simp add: has_bits_upto_def has_bits_split_Suc)
have incl: "?only_n ⊆ has_bits {n..<d}"
using has_bits_incl[of "{n}" "{n..<d}"] by (auto)
have union: "?upto_n ∪ ?only_n = ?upto_Suc_n"
unfolding has_bits_split_Suc[OF ‹n<d›] has_bits_upto_def
using has_bits_in_len_d_lists[of "{n}"] by blast
show ?thesis unfolding left fst snd
by (subst sum.union_disjoint[symmetric])(use incl union has_bits_upto_def in ‹auto›)
qed
then show ?case unfolding run_B_upto_def unfolding run_pure_adv.simps
by (fold run_B_upto_def, subst v)
(auto simp add: cblinfun.sum_right tensor_op_ell2 US_ket_only01
UqueryH_tensor_id_cblinfunB cblinfun.add_right US_ket nth_append v1_def v2_def)
qed
text ‹As a shorthand, we define ‹Proj_ket_upto›.›
lemma run_B_projection:
assumes "n<d"
shows "Proj_ket_upto (has_bits_upto n) *⇩V run_B_upto n = run_B_upto n"
proof -
obtain v where v: "run_B_upto n = (∑i∈has_bits_upto n. v i ⊗⇩s ket (list_to_l i))"
using run_B_upto_sum assms by auto
show ?thesis unfolding v by (subst cblinfun.sum_right, intro sum.cong, simp,
intro Proj_ket_upto_vec) fastforce
qed
text ‹How ‹Ψs› relate to ‹run_B›.›
lemma run_B_upto_split:
assumes "n≤d"
shows "run_B_upto n = (∑i∈has_bits_upto n. Ψs (list_to_l i) (run_B_upto n) ⊗⇩s ket (list_to_l i))"
proof -
have neg_set: "- list_to_l ` (has_bits_upto n) =
list_to_l ` has_bits {n..<d} ∪ - Collect blog" unfolding has_bits_upto_def
by (smt (verit, del_insts) Compl_Diff_eq Diff_subset Un_commute inj_list_to_l
inj_on_image_set_diff has_bits_in_len_d_lists surj_list_to_l)
have "run_B_upto n = id_cblinfun *⇩V run_B_upto n" by auto
also have "… = (∑i∈list_to_l ` has_bits_upto n.
(tensor_ell2_right (ket i)) o⇩C⇩L (tensor_ell2_right (ket i)*)) *⇩V run_B_upto n +
Proj_ket_set (- list_to_l ` has_bits_upto n) *⇩V run_B_upto n"
by (subst id_cblinfun_tensor_split_finite[of "list_to_l ` has_bits_upto n"])
(auto simp add: cblinfun.add_left)
also have "… = (∑i∈list_to_l ` has_bits_upto n.
(tensor_ell2_right (ket i)) o⇩C⇩L (tensor_ell2_right (ket i)*)) *⇩V run_B_upto n +
Proj_ket_set (list_to_l ` has_bits {n..<d}) *⇩V run_B_upto n"
proof -
have orth: "is_orthogonal x y"
if ass: "x ∈ ket ` list_to_l ` has_bits {n..<d}" "y ∈ ket ` (- Collect blog)" for x y
proof -
obtain j where j: "j∈has_bits {n..<d}" and x: "x = ket (list_to_l j)" using ass(1) by auto
then have valid: "blog (list_to_l j)"
by (metis Set.basic_monos(7) has_bits_in_len_d_lists imageI mem_Collect_eq surj_list_to_l)
obtain k where k: "¬ blog k" and y: "y = ket k" using ass(2) by auto
show "is_orthogonal x y" unfolding x y by (subst orthogonal_ket)(use k valid in ‹blast›)
qed
then show ?thesis using run_B_upto_proj_not_valid unfolding neg_set Proj_ket_set_def
by (subst proj_classical_set_union[OF orth])
(auto simp add: tensor_op_right_add cblinfun.add_left assms )
qed
also have "… = (∑i∈has_bits_upto n. (tensor_ell2_right (ket (list_to_l i))) o⇩C⇩L
(tensor_ell2_right (ket (list_to_l i))*)) *⇩V run_B_upto n"
unfolding run_B_upto_proj_over[OF ‹n≤d›] proof (subst sum.reindex, goal_cases)
case 1 show ?case using bij_betw_imp_inj_on[OF bij_betw_list_to_l]
by (simp add: has_bits_upto_def inj_on_diff)
qed (auto simp add: Proj_ket_set_def)
finally have *: "run_B_upto n =
(∑i∈has_bits_upto n. (tensor_ell2_right (ket (list_to_l i))* *⇩V run_B_upto n) ⊗⇩s ket (list_to_l i))"
by (smt (verit, ccfv_SIG) cblinfun.sum_left cblinfun_apply_cblinfun_compose sum.cong
tensor_ell2_right.rep_eq)
show ?thesis unfolding Ψs_def by (subst *)(use lessThan_Suc_atMost in ‹auto›)
qed
lemma run_B_split:
"run_B = (∑i∈len_d_lists. Ψs (list_to_l i) run_B ⊗⇩s (ket (list_to_l i)))"
unfolding run_B_altdef has_bits_upto_d[symmetric] by (subst run_B_upto_split[symmetric]) auto
end
unbundle no cblinfun_syntax
unbundle no lattice_syntax
unbundle no register_syntax
end