Theory Oracle_Programs

section ‹‹Oracle_Programs› -- Oracle programs and their execution›

theory Oracle_Programs imports
  CO_Operations
  Invariant_Preservation
  Compressed_Oracle_Is_RO
begin

subsection ‹Oracle programs›

datatype ('mem, 'x, 'y) program_step = ProgramStep ‹'mem update› | QueryStep ‹'x update ⇒ 'mem update› ‹'y update ⇒ 'mem update›
type_synonym ('mem, 'x, 'y) program = ‹('mem, 'x, 'y) program_step list›


inductive is_QueryStep :: ‹('mem,'x,'y::ab_group_add) program_step ⇒ bool› where is_QueryStep_QueryStep[iff]: ‹is_QueryStep (QueryStep X Y)›
inductive is_ProgramStep :: ‹('mem,'x,'y::ab_group_add) program_step ⇒ bool› where is_ProgramStep_ProgramStep[iff]: ‹is_ProgramStep (ProgramStep U)›

lemma is_QueryStep_ProgramStep[iff]: ‹¬ is_QueryStep (ProgramStep U)›
  using is_QueryStep.cases by blast

lemma is_ProgramStep_QueryStep[iff]: ‹¬ is_ProgramStep (QueryStep X Y)›
  by (simp add: is_ProgramStep.simps)

fun valid_program_step where ‹valid_program_step (QueryStep X Y) = compatible X Y› | ‹valid_program_step (ProgramStep U) = isometry U›
definition valid_program where ‹valid_program prog = list_all valid_program_step prog›

lemma valid_program_cons[simp]: ‹valid_program (p # ps) ⟷ valid_program_step p ∧ valid_program ps›
  by (simp add: valid_program_def)

lemma valid_program_append: ‹valid_program (p @ q) ⟷ valid_program p ∧ valid_program q›
  by (simp add: valid_program_def)

lemma valid_program_empty[iff]: ‹valid_program []›
  by (simp add: valid_program_def)

fun exec_program_step :: ‹('x ⇒ 'y) ⇒ ('mem,'x,'y::ab_group_add) program_step ⇒ 'mem ell2 ⇒ 'mem ell2› where
  ‹exec_program_step h (ProgramStep U) ψ = U *⇩V ψ›
| ‹exec_program_step h (QueryStep X Y) ψ = (X;Y) (function_oracle h) *⇩V ψ›

fun exec_program_step_with :: ‹('x × 'y × 'o) update ⇒ ('mem,'x,'y) program_step ⇒ ('mem × 'o) ell2 ⇒ ('mem × 'o) ell2› where
  ‹exec_program_step_with Q (ProgramStep U) ψ = Fst U *⇩V ψ›
| ‹exec_program_step_with Q (QueryStep X Y) ψ = (Fst o X; (Fst o Y; Snd)) Q ψ›

definition exec_program :: ‹('x ⇒ 'y::ab_group_add) ⇒ ('mem,'x,'y) program ⇒ 'mem ell2 ⇒ 'mem ell2› where
  ‹exec_program h program ψ = fold (exec_program_step h) program ψ›
definition exec_program_with :: ‹('x × 'y × 'o) update ⇒ ('mem,'x,'y) program ⇒ ('mem×'o) ell2 ⇒ ('mem×'o) ell2› where
  ‹exec_program_with Q program ψ = fold (exec_program_step_with Q) program ψ›

lemma bounded_clinear_exec_program_step_with[bounded_clinear]: ‹bounded_clinear (exec_program_step_with Q step)›
  apply (cases step)
  by (auto intro!: cblinfun.bounded_clinear_right simp add: exec_program_step_with.simps[abs_def])

lemma exec_program_empty[simp]: ‹exec_program h [] ψ = ψ›
  by (simp add: exec_program_def)
lemma exec_program_with_empty[simp]: ‹exec_program_with Q [] ψ = ψ›
  by (simp add: exec_program_with_def)
lemma exec_program_append: ‹exec_program h (p @ q) ψ = exec_program h q (exec_program h p ψ)›
  by (simp add: exec_program_def)
lemma exec_program_with_append: ‹exec_program_with Q (p @ q) ψ = exec_program_with Q q (exec_program_with Q p ψ)›
  by (simp add: exec_program_with_def)
lemma exec_program_cons[simp]: ‹exec_program h (step#prog) ψ = exec_program h prog (exec_program_step h step ψ)›
  by (simp add: exec_program_def)
lemma exec_program_with_cons[simp]: ‹exec_program_with Q (step#prog) ψ = exec_program_with Q prog (exec_program_step_with Q step ψ)›
  by (simp add: exec_program_with_def)


lemma norm_exec_program_step_with: ‹norm (exec_program_step_with oracle program_step ψ) ≤ norm ψ› if ‹valid_program_step program_step› and ‹norm oracle ≤ 1›
proof (cases program_step)
  case (ProgramStep U)
  with that have ‹isometry U›
    by simp
  then have ‹norm (Fst U) = 1›
    by (simp add: register_norm norm_isometry)
  then show ?thesis
    apply (simp add: ProgramStep)
    by (smt (verit, del_insts) ‹norm (Fst U) = 1› mult_cancel_right1 norm_cblinfun)
next
  case (QueryStep X Y)
  with that
  have [register]: ‹compatible X Y›
    using valid_program_step.simps by blast
  have [register]: ‹register (Fst ∘ X;(Fst ∘ Y;Snd))›
    by simp
  have ‹norm ((Fst ∘ X;(Fst ∘ Y;Snd)) oracle *⇩V ψ) ≤ norm ((Fst ∘ X;(Fst ∘ Y;Snd)) oracle) * norm ψ›
    using norm_cblinfun by blast
  also have ‹… = norm oracle * norm ψ›
    by (simp add: register_norm)
  also have ‹… ≤ norm ψ›
  by (simp add: mult_left_le_one_le that(2))
  finally show ?thesis
    by (simp add: QueryStep)
qed

lemma norm_exec_program_with: 
  ‹norm (exec_program_with oracle program ψ) ≤ norm ψ› if ‹norm oracle ≤ 1› and ‹valid_program program› for program
proof (insert that(2), induction program rule: rev_induct)
  case Nil
  then show ?case
    by simp
next
  case (snoc program_step program)
  then have ‹valid_program_step program_step› and ‹valid_program program›
    by (auto simp: valid_program_append)
  have ‹norm (exec_program_step_with oracle program_step (exec_program_with oracle program ψ)) ≤ norm (exec_program_with oracle program ψ)›
    by (smt (verit, del_insts) ‹valid_program_step program_step› mult_left_le_one_le norm_exec_program_step_with norm_ge_zero that(1))
  also have ‹… ≤ norm ψ›
    using ‹valid_program program› snoc.IH by force
  finally show ?case
    by (simp add: exec_program_with_append)
qed

lemma norm_exec_program_step_with_isometry:
  assumes ‹valid_program_step program_step›
  assumes ‹isometry query›
  shows ‹norm (exec_program_step_with query program_step ψ) = norm ψ›
proof (cases program_step)
  case (ProgramStep U)
  with assms have ‹isometry U›
    by simp
  with ProgramStep show ?thesis
    by (simp add: isometry_preserves_norm register_isometry)
next
  case (QueryStep X Y)
  with assms have [register]: ‹compatible X Y›
    by simp
  have ‹register (Fst ∘ X;(Fst ∘ Y;Snd))›
    by simp
  with assms have ‹isometry ((Fst ∘ X;(Fst ∘ Y;Snd)) query)›
    using register_isometry by blast
  then show ?thesis
    by (simp add: QueryStep isometry_preserves_norm)
qed

(* (* TODO move *)
lemma norm_exec_program_step_with:
  assumes ‹norm Q ≤ 1›
  assumes ‹valid_program_step step›
  assumes ‹norm ψ ≤ 1›
  shows ‹norm (exec_program_step_with Q step ψ) ≤ 1›
proof -
  have aux: ‹norm (X *⇩V ψ) ≤ 1› if ‹norm X ≤ 1› and ‹norm ψ ≤ 1› for X ψ
    by (smt (verit) mult_le_one norm_cblinfun norm_ge_zero that(1,2))
  show ?thesis
  proof (cases step)
    case (ProgramStep U)
    then show ?thesis
    using assms
    by (auto intro!: aux simp: register_norm norm_isometry)
  next
    case (QueryStep X Y)
    with assms have [register]: ‹compatible X Y›
      by simp
    then have reg: ‹register (Fst ∘ X;(Fst ∘ Y;Snd))›
      by simp
    then show ?thesis
      by (auto intro!: aux assms simp: register_norm[OF ] norm_isometry QueryStep)
  qed
qed

(* TODO move *)
lemma norm_exec_program_with:
  assumes ‹norm U ≤ 1›
  assumes ‹valid_program program›
  assumes ‹norm ψ ≤ 1›
  shows ‹norm (exec_program_with U program ψ) ≤ 1›
  using ‹valid_program program›
  apply (induction program rule:rev_induct)
   apply (simp add: assms)
  by (simp add: assms exec_program_with_append valid_program_append norm_exec_program_step_with) *)


subsection ‹Lifting›

fun lift_program_step :: ‹('a update ⇒ 'mem update) ⇒ ('a,'x,'y::ab_group_add) program_step ⇒ ('mem,'x,'y) program_step› where
  ‹lift_program_step Q (ProgramStep U) = ProgramStep (Q U)›
| ‹lift_program_step Q (QueryStep X Y) = QueryStep (Q o X) (Q o Y)›

definition lift_program :: ‹('a update ⇒ 'mem update) ⇒ ('a,'x,'y::ab_group_add) program_step list ⇒ ('mem,'x,'y) program› where
  ‹lift_program Q p = map (lift_program_step Q) p›

lemma valid_program_step_lift:
  assumes ‹register Q› and ‹valid_program_step p›
  shows ‹valid_program_step (lift_program_step Q p)›
proof (cases p)
  case (ProgramStep U)
  then have ‹isometry (Q U)›
    using assms register_isometry valid_program_step.simps(2) by blast
  then show ?thesis
    using ProgramStep by auto
next
  case (QueryStep X Y)
  with assms show ?thesis
    by simp
qed

lemma valid_program_lift:
  assumes ‹register Q› and ‹valid_program p›
  shows ‹valid_program (lift_program Q p)›
  using assms(2)
  by (auto simp add: valid_program_def lift_program_def list.pred_map list_all_length valid_program_step_lift assms(1))

lemma lift_program_empty[simp]: ‹lift_program Q [] = []›
  by (simp add: lift_program_def)

lemma lift_program_cons: ‹lift_program Q (program_step # program) = lift_program_step Q program_step # lift_program Q program›
  by (simp add: lift_program_def)

lemma lift_program_append: ‹lift_program Q (program1 @ program2) = lift_program Q program1 @ lift_program Q program2›
  by (simp add: lift_program_def)

lemma is_QueryStep_lift_program_step[simp]: ‹is_QueryStep (lift_program_step Q program_step) ⟷ is_QueryStep program_step›
  apply (cases program_step)
  by simp_all

lemma filter_is_QueryStep_lift_program: ‹filter is_QueryStep (lift_program Q program) = lift_program Q (filter is_QueryStep program)›
  apply (induction program)
  by (auto simp: lift_program_def)

lemma length_lift_program[simp]: ‹length (lift_program Q program) = length program›
  apply (induction program)
  by (auto simp: lift_program_def)

definition ‹query_count program = length (filter is_QueryStep program)›

lemma query_count_append[simp]: ‹query_count (p @ q) = query_count p + query_count q›
  by (simp add: query_count_def)
lemma query_count_nil[simp]: ‹query_count [] = 0›
  by (simp add: query_count_def)
lemma query_count_cons_QueryStep[simp]: ‹query_count (QueryStep X Y # p) = query_count p + 1›
  by (simp add: query_count_def)
lemma query_count_cons_ProgramStep[simp]: ‹query_count (ProgramStep U # p) = query_count p›
  by (simp add: query_count_def)
lemma query_count_lift_program[simp]: ‹query_count (lift_program Q p) = query_count p›
  by (simp add: query_count_def filter_is_QueryStep_lift_program)

lemma exec_lift_program_step_Fst:
  assumes ‹valid_program_step program_step›
  shows ‹exec_program_step h (lift_program_step Fst program_step) (ψ ⊗⇩s φ) = exec_program_step h program_step ψ ⊗⇩s φ›
proof (cases program_step)
  case (ProgramStep U)
  then show ?thesis
    by (simp add: Fst_def tensor_op_ell2)
next
  case (QueryStep X Y)
  with assms have [register]: ‹compatible X Y›
    using valid_program_step.simps(1) by blast
  have ‹(Fst ∘ (X;Y)) (function_oracle h) *⇩V ψ ⊗⇩s φ = ((X;Y) (function_oracle h) *⇩V ψ) ⊗⇩s φ›
    by (simp add: Fst_def tensor_op_ell2)
  then show ?thesis
    by (simp add: QueryStep register_comp_pair)
qed

lemma exec_lift_program_Fst:
  assumes ‹valid_program program›
  shows ‹exec_program h (lift_program Fst program) (ψ ⊗⇩s φ) = exec_program h program ψ ⊗⇩s φ›
  apply (insert assms, induction program rule:rev_induct)
  by (simp_all add: lift_program_append exec_program_append lift_program_cons valid_program_append exec_lift_program_step_Fst)

subsection ‹Final measurement›

definition measurement_probability :: ‹('a update ⇒ 'mem update) ⇒ 'mem ell2 ⇒ 'a ⇒ real› where 
  ‹measurement_probability Q ψ x = (norm (Q (proj (ket x)) ψ))⇧2›

lemma measurement_probability_nonneg: ‹measurement_probability Q ψ x ≥ 0›
  by (simp add: measurement_probability_def)

lemma norm_register_Proj_ket_invariant_union:
  ― ‹Helper lemma›
  assumes ‹register Q› and ‹A ∩ B = {}›
  shows ‹(norm (Q (Proj (ket_invariant (A ∪ B))) ψ))⇧2 = (norm (Q (Proj (ket_invariant A)) ψ))⇧2 + (norm (Q (Proj (ket_invariant B)) ψ))⇧2›
proof -
  have ortho1: ‹orthogonal_spaces (ket_invariant A) (ket_invariant B)›
    using assms(2) by force
  have ortho2: ‹is_orthogonal (Q (Proj (ket_invariant A)) *⇩V ψ) (Q (Proj (ket_invariant B)) *⇩V ψ)›
  proof -
    from ortho1 have ‹orthogonal_spaces (lift_invariant Q (ket_invariant A)) (lift_invariant Q (ket_invariant B))›
      by (simp add: orthogonal_spaces_lift_invariant assms)
    then have ‹is_orthogonal (Proj (lift_invariant Q (ket_invariant A)) ψ) (Proj (lift_invariant Q (ket_invariant B)) ψ)›
      by (metis Proj_lift_invariant assms(1) cblinfun_apply_in_image lift_invariant_def orthogonal_spaces_def)
    moreover have ‹Proj (lift_invariant Q (ket_invariant A)) = Q (Proj (ket_invariant A))›
      by (simp add: Proj_ket_invariant_butterfly Proj_lift_invariant assms(1) butterfly_eq_proj)
    moreover have ‹Proj (lift_invariant Q (ket_invariant B)) = Q (Proj (ket_invariant B))›
      by (simp add: Proj_lift_invariant assms(1) ket_invariant_def)
    ultimately show ?thesis
      by simp
  qed    
  have ‹(norm (Q (Proj (ket_invariant (A ∪ B))) ψ))⇧2 = (norm (Q (Proj (ket_invariant A ⊔ ket_invariant B)) ψ))⇧2›
    by (simp add: ket_invariant_union)
  also have ‹… = (norm (Q (Proj (ket_invariant A) + (Proj (ket_invariant B))) ψ))⇧2›
    by (metis Proj_sup ortho1) 
  also have ‹… = (norm (Q (Proj (ket_invariant A)) ψ + Q (Proj (ket_invariant B)) ψ))⇧2›
    by (simp add: complex_vector.linear_add clinear_register ‹register Q› cblinfun.add_left)
  also have ‹… = (norm (Q (Proj (ket_invariant A)) ψ))⇧2 + (norm (Q (Proj (ket_invariant B)) ψ))⇧2›
    by (simp add: pythagorean_theorem ortho2)
  finally show ?thesis
    by -
qed



lemma measurement_probability_sum:
  assumes ‹register Q› and ‹finite F›
  shows ‹(∑x∈F. measurement_probability Q ψ x) = (norm (Q (Proj (ket_invariant F)) ψ))⇧2›
proof (use ‹finite F› in induction)
  case empty
  show ?case
    apply simp
    by (metis (no_types, lifting) assms(1) cancel_comm_monoid_add_class.diff_cancel cblinfun.zero_left register_minus)
next
  case (insert x F)
  have ‹(norm (Q (Proj (ket_invariant (insert x F))) *⇩V ψ))⇧2 = (norm (Q (Proj (ket_invariant F)) *⇩V ψ))⇧2 + (norm (Q (Proj (ket_invariant {x})) *⇩V ψ))⇧2›
    apply (rewrite at ‹insert x F› to ‹F ∪ {x}› DEADID.rel_mono_strong)
     apply simp
    apply (subst norm_register_Proj_ket_invariant_union)
    by (simp_all add: assms insert.hyps)
  also have ‹… = (norm (Q (proj (ket x)) ψ))⇧2 + (norm (Q (Proj (ccspan (ket ` F))) ψ))⇧2›
    by (simp add: ket_invariant_def)
  also have ‹… = (norm (Q (proj (ket x)) ψ))⇧2 + sum (measurement_probability Q ψ) F›
    by (simp add: insert.IH ket_invariant_def)
  also have ‹… = sum (measurement_probability Q ψ) (insert x F)›
    by (simp add: insert.hyps measurement_probability_def)
  finally show ?case
    by simp
qed

lemma
  assumes ‹register Q›
  shows measurement_probability_summable: ‹measurement_probability Q ψ summable_on A›
    and measurement_probability_infsum_leq: ‹(∑⇩∞x∈A. measurement_probability Q ψ x) ≤ (norm (Q (Proj (ket_invariant A)) ψ))⇧2›
proof -
  define m s where ‹m x = measurement_probability Q ψ x› and ‹s A = (norm (Q (Proj (ket_invariant A)) ψ))⇧2› for A x
  have sum_m_fin: ‹sum m F = s F› if ‹finite F› for F
    by (simp add: measurement_probability_sum m_def s_def that assms)
  have s_mono: ‹s A ≤ s B› if ‹A ⊆ B› for A B
  proof -
    have [simp]: ‹A ∪ B = B›
      using that by blast
    have ‹s A ≤ s A + s (B-A)›
      by (simp add: s_def)
    also have ‹… = s B›
      apply (simp add: s_def)
      apply (subst norm_register_Proj_ket_invariant_union[symmetric])
      using that
      by (auto simp: assms)
    finally show ?thesis
      by -
  qed
  have m_pos: ‹m x ≥ 0› for x
    by (simp add: m_def measurement_probability_nonneg)
  show summable: ‹m summable_on A› for A
    apply (rule nonneg_bounded_partial_sums_imp_summable_on[where C=‹s UNIV›])
    using s_mono[of _ UNIV] sum_m_fin
    by (auto intro!: eventually_finite_subsets_at_top_weakI simp: m_pos)
  then show ‹infsum m A ≤ s A›
    apply (rule infsum_le_finite_sums)
    using s_mono[of _ A] sum_m_fin
    by auto
qed

lemma dist_inv_measurement_probability:
  fixes I :: ‹'i::finite set›
  assumes [register]: ‹register Q›
  shows ‹(∑x∈I. measurement_probability Q ψ x) = (dist_inv Q (ket_invariant (-I)) ψ)⇧2›
proof -
  have ‹(∑x∈I. measurement_probability Q ψ x) = (norm (Q (Proj (ket_invariant I)) *⇩V ψ))⇧2›
    by (simp add: measurement_probability_sum)
  then show ?thesis
    by (simp add: dist_inv_def ket_invariant_compl)
qed

lemma dist_inv_avg_measurement_probability:
  fixes I :: ‹'h::finite ⇒ 'i::finite set›
  assumes [register]: ‹register Q›
  shows ‹(∑h∈UNIV. ∑x∈I h. measurement_probability Q (ψ h) x) / CARD('h)
             = (dist_inv_avg Q (λh. ket_invariant (- I h)) ψ)⇧2›
  by (simp add: dist_inv_avg_def real_sqrt_pow2 divide_nonneg_pos
      sum_nonneg dist_inv_measurement_probability)



subsection ‹Preservation›



lemma dist_inv_avg_exec_compatible:
  fixes prog
  assumes ‹valid_program prog›
  assumes [register]: ‹compatible Q R›
  shows ‹dist_inv_avg Q I (λh::'x::finite⇒'y::{finite,ab_group_add}. exec_program h (lift_program R prog) (ψ h))
       ≤ dist_inv_avg Q I ψ›
proof (insert ‹valid_program prog›, induction prog rule:rev_induct)
  case Nil
  with assms show ?case
    by simp
next
  case (snoc program_step prog)
  show ?case
  proof (cases program_step)
    case (ProgramStep U)
    have ‹dist_inv_avg Q I (λh. exec_program h (lift_program R (prog @ [program_step])) (ψ h))
         ≤ (MAX h::'x⇒'y. norm U) * dist_inv_avg Q I (λh. exec_program h (lift_program R prog) (ψ h))›
      apply (simp add: lift_program_append lift_program_cons exec_program_append ProgramStep del: range_constant Max_const)
      apply (rule dist_inv_avg_apply_compatible[where R=‹λ_. R›])
      by simp
    also have ‹… ≤ dist_inv_avg Q I ψ›
      using snoc
      by (simp_all add: ProgramStep norm_isometry valid_program_append)
    finally show ?thesis
      by -
  next
    case (QueryStep X Y)
    with snoc have [register]: ‹compatible X Y› by (simp add: valid_program_append)
    have ‹dist_inv_avg Q I (λh. exec_program h (lift_program R (prog @ [program_step])) (ψ h)) 
      ≤ (MAX h::'x⇒'y. norm (function_oracle h)) * dist_inv_avg Q I (λh. exec_program h (lift_program R prog) (ψ h))›
      apply (simp add: lift_program_append lift_program_cons exec_program_append QueryStep 
          del: range_constant Max_const norm_function_oracle)
       apply (rule dist_inv_avg_apply_compatible[where R=‹λ_. (R ∘ X;R ∘ Y)›])
      by simp
    also have ‹… ≤ dist_inv_avg Q I ψ›
      using snoc
      by (simp_all add: QueryStep valid_program_append)
    finally show ?thesis
      by -
  qed
qed

lemma dist_inv_exec'_compatible:
  fixes prog
  assumes ‹valid_program prog›
  assumes normU: ‹norm U ≤ 1›
  assumes [register]: ‹register R›
  assumes compatQ1[register]: ‹compatible Q (Fst o R)›
  assumes compatQ2[register]: ‹compatible Q Snd›
  shows ‹dist_inv Q I (exec_program_with U (lift_program R prog) ψ) ≤ dist_inv Q I ψ›
proof (insert ‹valid_program prog›, induction prog rule:rev_induct)
  case Nil
  with assms show ?case
    by simp
next
  case (snoc program_step prog)
  show ?case
  proof (cases program_step)
    case (ProgramStep V)
    have ‹dist_inv Q I (exec_program_with U (lift_program R (prog @ [program_step])) ψ)
      ≤ norm V * dist_inv Q I (exec_program_with U (lift_program R prog) ψ)›
      apply (simp add: lift_program_append exec_program_with_append lift_program_cons ProgramStep)
      using dist_inv_apply_compatible[OF compatQ1]
      by simp
    also have ‹… ≤ dist_inv Q I ψ›
      using ProgramStep norm_isometry snoc(1) snoc.prems valid_program_append exec_program_with_append by fastforce
    finally show ?thesis
      by -
  next
    case (QueryStep X Y)
    with snoc have [register]: ‹compatible X Y› by (simp add: valid_program_append)
    then have compat[register]: ‹compatible Q (Fst ∘ (R ∘ X);(Fst ∘ (R ∘ Y);Snd))›
      by (auto intro!: compatible3' compatible_comp_inner simp flip: comp_assoc)
    have ‹dist_inv Q I (exec_program_with U (lift_program R (prog @ [program_step])) ψ)
      ≤ norm U * dist_inv Q I (exec_program_with U (lift_program R prog) ψ)›
      apply (simp add: lift_program_append lift_program_cons QueryStep exec_program_with_append)
      by (rule dist_inv_apply_compatible[OF compat])
    also have ‹… ≤ dist_inv Q I ψ›
      by (smt (verit, ccfv_SIG) assms(2) dist_inv_pos mult_cancel_right1
          mult_left_le_one_le snoc(1) snoc.prems valid_program_append zero_le_mult_iff)
    finally show ?thesis
      by -
  qed
qed




subsection ‹Misc›

(* TODO sort me *)

lemma dist_inv_induct:
  fixes "oracle" :: ‹('x × 'y::ab_group_add × ('x ⇒ 'y option)) update›
  assumes ‹compatible R Fst›
  assumes ‹(∑i<query_count program. g i) ≤ ε›
  assumes init: ‹ψ0 ∈ space_as_set (lift_invariant R (J 0))›
  assumes ‹J (query_count program) ≤ I›
  assumes ‹valid_program program›
  assumes ‹⋀X Y i. compatible X Y ⟹ preserves ((Fst ∘ X;(Fst ∘ Y;Snd)) oracle :: ('m × _) update) (lift_invariant R (J i))
           (lift_invariant R (J (Suc i))) (g i)›
  assumes ‹norm oracle ≤ 1›
  assumes ‹norm ψ0 ≤ 1›
  shows ‹dist_inv R I (exec_program_with oracle program ψ0) ≤ ε›
proof -
  note [[simproc del: Laws_Quantum.compatibility_warn]]
  define f where ‹f n = (∑i<n. g i)› for n
  from ‹compatible R Fst› have [register]: ‹register R›
    using compatible_register1 by blast
  have ‹dist_inv R (J (query_count program)) (exec_program_with oracle program ψ0) ≤ f (query_count program)›
  proof (insert ‹valid_program program›, induction program rule:rev_induct)
    case Nil
    from init
    have ‹dist_inv R (J 0) ψ0 = 0›
      by (simp add: dist_inv_0_iff)
    then show ?case
      by (simp add: assms(2) query_count_def f_def)
  next
    case (snoc program_step program)
    from snoc.prems have ‹valid_program program›
      using valid_program_append by blast
    from snoc.prems have ‹valid_program_step program_step›
      by (simp add: valid_program_append)
    define i where ‹i = query_count program›
    show ?case
    proof (cases program_step)
      case (ProgramStep U)
      with ‹valid_program_step program_step›
      have [iff]: ‹isometry U›
        by simp
      have ‹preserves (Fst U) (lift_invariant R (J i)) (lift_invariant R (J i)) 0›
        apply (rule_tac preserves_compatible[where F=Fst])
        using ‹compatible R Fst› compatible_register_invariant_compatible_register compatible_sym apply blast
        by simp
      then have ‹dist_inv R (J i) (Fst U *⇩V exec_program_with oracle program ψ0) ≤ f i›
        apply (rule dist_inv_leq_if_preserves[THEN order_trans])
        using snoc.IH[OF ‹valid_program program›]
        by (simp_all add: norm_isometry register_isometry query_count_def i_def)
      then show ?thesis
        by (simp add: ProgramStep exec_program_with_append i_def query_count_def)
    next
      case (QueryStep X Y)
      with ‹valid_program_step program_step›
      have [register]: ‹compatible X Y›
        by simp
      with assms have pres: ‹preserves ((Fst ∘ X;(Fst ∘ Y;Snd)) oracle) (lift_invariant R (J i))
           (lift_invariant R (J (Suc i))) (g i)›
        by fast
      have fg': ‹norm ((Fst ∘ X;(Fst ∘ Y;Snd)) oracle) * f i + g i * norm (exec_program_with oracle program ψ0) ≤ f (Suc i)›
      proof -
        have ‹norm ((Fst ∘ X;(Fst ∘ Y;Snd)) oracle) ≤ 1›
          apply (subst register_norm[where a="oracle"])
          by (simp_all add: assms)
        moreover have ‹norm (exec_program_with oracle program ψ0) ≤ 1›
          apply (rule norm_exec_program_with[THEN order_trans])
          using ‹valid_program program› assms by simp_all
        moreover have ‹f i + g i ≤ f (Suc i)›
          by (simp add: f_def)
        moreover have gpos: ‹g i ≥ 0› for i
          using ‹compatible X Y› assms(6) preserves_def by blast
        moreover have ‹f i ≥ 0›
          by (auto intro!: sum_nonneg gpos simp: f_def)
        ultimately  
        show ?thesis
          by (smt (verit) mult_left_le mult_left_le_one_le norm_ge_zero)
      qed
      show ?thesis
        apply (simp add: QueryStep exec_program_with_append flip: i_def)
        using pres apply (rule dist_inv_leq_if_preserves[THEN order_trans])
          apply (simp, simp)
        using snoc.IH[OF ‹valid_program program›, folded i_def]
        by (smt (verit, ccfv_SIG) fg' mult_left_mono norm_ge_zero)
    qed
  qed
  with assms show ?thesis
    using ‹register R›
    by (smt (verit, best) dist_inv_mono f_def)
qed

subsection ‹Random Oracles›

lemma standard_query_for_fixed_function_generic:
  fixes standard_query
  assumes ‹⋀H x y z. H x = Some z ⟹ standard_query *⇩V (ket (x,y,H)) = ket (x, y + z, H)› (* e.g. standard_query_ket_full_Some *)
  assumes ‹valid_program program›
  shows ‹exec_program h program initial_state ⊗⇩s ket (Some o h) 
       = exec_program_with standard_query program (initial_state ⊗⇩s ket (Some ∘ h))›
proof (insert ‹valid_program program›, induction program rule: rev_induct)
  case Nil
  then show ?case
    by simp
next
  case (snoc program_step prog)
  then have [simp]: ‹valid_program prog›
    using list_all_append valid_program_def by blast
  show ?case
  proof (cases program_step)
    case (ProgramStep U)
    have ‹exec_program h (prog @ [program_step]) initial_state ⊗⇩s ket (Some ∘ h) = (U *⇩V exec_program h prog initial_state) ⊗⇩s ket (Some ∘ h)›
      by (simp add: ProgramStep exec_program_append)
    also have ‹… = Fst U *⇩V exec_program h prog initial_state ⊗⇩s ket (Some ∘ h)›
      by (simp add: Fst_def tensor_op_ell2)
    also have ‹… = Fst U *⇩V exec_program_with standard_query prog (initial_state ⊗⇩s ket (Some ∘ h))›
      by (subst snoc.IH, simp_all)
    also have ‹… = exec_program_with standard_query (prog @ [program_step]) (initial_state ⊗⇩s ket (Some ∘ h))›
      by (simp add: ProgramStep exec_program_with_append)
    finally show ?thesis
      by -
  next
    case (QueryStep X Y)
    then have [register]: ‹compatible X Y›
      using snoc.prems valid_program_def by force
    have ‹exec_program h (prog @ [program_step]) initial_state ⊗⇩s ket (Some ∘ h) = ((X;Y) (function_oracle h) *⇩V exec_program h prog initial_state) ⊗⇩s ket (Some ∘ h)›
      by (simp add: QueryStep exec_program_append)
    also have ‹… = Fst ((X;Y) (function_oracle h)) *⇩V (exec_program h prog initial_state ⊗⇩s ket (Some ∘ h))›
      by (simp add: Fst_def tensor_op_ell2)
    also have ‹… = (Fst o X; (Fst o Y; Snd)) standard_query *⇩V (exec_program h prog initial_state ⊗⇩s ket (Some ∘ h))›
      by (simp add: standard_query_for_fixed_func_generic assms)
    also have ‹… = (Fst o X; (Fst o Y; Snd)) standard_query *⇩V exec_program_with standard_query prog (initial_state ⊗⇩s ket (Some ∘ h))›
      by (subst snoc.IH, simp_all)
    also have ‹… = exec_program_with standard_query (prog @ [program_step]) (initial_state ⊗⇩s ket (Some ∘ h))›
      by (simp add: QueryStep exec_program_with_append)
    finally show ?thesis
      by -
  qed
qed

lemma standard_query_for_fixed_function_dist_inv_generic:
  assumes ‹⋀H x y z. H x = Some z ⟹ standard_query *⇩V (ket (x,y,H)) = ket (x, y + z, H)› (* e.g. standard_query_ket_full_Some *)
  assumes ‹valid_program program›
  assumes compat: ‹compatible_invariants (⊤ ⊗⇩S ccspan {ket (Some ∘ h)}) J›
  assumes IJ: ‹J ⊓ (⊤ ⊗⇩S ccspan{ket (Some o h)}) = I ⊗⇩S ccspan{ket (Some o h)}›
  assumes [register]: ‹register Q›
  shows ‹dist_inv Q I (exec_program h program initial_state) =
    dist_inv (Fst o Q; Snd) J (exec_program_with standard_query program (initial_state ⊗⇩s ket (Some ∘ h)))›
proof -
  define e1 e2 where ‹e1 = exec_program h program initial_state› and ‹e2 = exec_program_with standard_query program (initial_state ⊗⇩s ket (Some ∘ h))›
  define keth where ‹keth = ket (Some o h)›
  have e2e1: ‹e2 = e1 ⊗⇩s keth›
    unfolding e1_def e2_def keth_def
    using standard_query_for_fixed_function_generic assms
    by fastforce
  have ‹dist_inv Q I e1 = norm ((id_cblinfun - Q (Proj I)) *⇩V e1)›
    by (simp add: dist_inv_def Proj_ortho_compl register_minus)
  also have ‹… = norm (e1 ⊗⇩s keth - (Q (Proj I) *⇩V e1) ⊗⇩s keth)›
    by (simp add: norm_tensor_ell2 keth_def cblinfun.diff_left flip: tensor_ell2_diff1)
  also have ‹… = norm ((id_cblinfun - Fst (Q (Proj I)) o⇩C⇩L Snd (proj keth)) *⇩V e1 ⊗⇩s keth)›
    by (simp add: Fst_def Snd_def comp_tensor_op tensor_op_ell2 cblinfun.diff_left)
  also have ‹… = dist_inv (Fst o Q; Snd) (I ⊗⇩S ccspan{keth}) (e1 ⊗⇩s keth)›
    by (simp add: dist_inv_def Proj_ortho_compl register_minus tensor_ccsubspace_via_Proj
        Proj_on_own_range is_Proj_tensor_op register_pair_apply)
  also have ‹… = dist_inv (Fst o Q; Snd) (J ⊓ (⊤ ⊗⇩S ccspan{ket (Some o h)})) (e1 ⊗⇩s keth)›
    by (simp add: IJ keth_def)
  also have ‹… = dist_inv (Fst o Q; Snd) J (e1 ⊗⇩s keth)›
    using compat apply (rule dist_inv_intersect_onesided)
     apply simp
    by (simp add: dist_inv_def Proj_ortho_compl register_minus tensor_ccsubspace_via_Proj
        Proj_on_own_range is_Proj_tensor_op register_pair_apply cblinfun.diff_left keth_def)
  also have ‹… = dist_inv (Fst o Q; Snd) J e2›
    by (simp add: e2e1)
  finally show ‹dist_inv Q I e1 = …›
    by -
qed



lemma standard_query_is_ro_generic:
  fixes standard_query
  assumes ‹⋀H x y z. H x = Some z ⟹ standard_query *⇩V (ket (x,y,H)) = ket (x, y + z, H)› (* e.g. standard_query_ket_full_Some *)
  assumes ‹valid_program program›
  shows ‹exec_program_with standard_query program (initial_state ⊗⇩s (superpos_total :: ('x::finite ⇒ 'y::{finite,ab_group_add} option) ell2))
      = (∑h∈UNIV. (exec_program h program initial_state ⊗⇩s ket (Some o h)) /⇩R sqrt CARD('x ⇒ 'y))›
proof (insert assms(2), induction program rule: rev_induct)
  case Nil
  have ‹sum ket (total_functions :: ('x ⇒ 'y option) set) = (∑h∈UNIV. ket (λa. Some (h a)))›
    apply (simp add: total_functions_def2 sum.reindex fun.inj_map)
    by (simp add: o_def)
  then show ?case
    by (simp add: uniform_superpos_def2 scaleR_scaleC card_fun card_total_functions tensor_ell2_scaleC2
        flip: scaleC_sum_right tensor_ell2_sum_right)
next
  case (snoc step prog)
  then have ‹valid_program_step step› and [iff]: ‹valid_program prog›
    by (simp_all add: valid_program_append)
  have ‹exec_program_step_with standard_query step (ψ ⊗⇩s ket (Some o h)) =
        exec_program_step h step ψ ⊗⇩s ket (Some o h)› for h ψ
  proof (cases step)
    case (ProgramStep U)
    then show ?thesis
      by (simp add: Fst_def tensor_op_ell2)
  next
    case (QueryStep X Y)
    with ‹valid_program_step step› have [register]: ‹compatible X Y›
      by simp
    have ‹exec_program_step_with standard_query step (ψ ⊗⇩s ket (Some ∘ h))
        = (Fst ∘ X;(Fst ∘ Y;Snd)) standard_query *⇩V (ψ ⊗⇩s ket (Some ∘ h))›
      by (simp add: QueryStep)
    also have ‹… = ((Fst ∘ X;(Fst ∘ Y;Snd)) standard_query o⇩C⇩L Snd (selfbutter (ket (Some o h)))) *⇩V (ψ ⊗⇩s ket (Some ∘ h))›
      by simp
    also have ‹… = (Fst ∘ X;(Fst ∘ Y;Snd)) (standard_query o⇩C⇩L (Snd o Snd) (selfbutter (ket (Some o h)))) *⇩V (ψ ⊗⇩s ket (Some ∘ h))›
      by (simp add: register_mult[symmetric, where F=‹(_;_)›] register_pair_Snd[unfolded o_def, THEN fun_cong])
    also have ‹… = (Fst ∘ X;(Fst ∘ Y;Snd)) ((Fst; Snd o Fst) (function_oracle h) o⇩C⇩L (Snd o Snd) (selfbutter (ket (Some o h)))) *⇩V (ψ ⊗⇩s ket (Some ∘ h))›
      apply (rewrite at ‹(Fst;Snd ∘ Fst) (function_oracle h)› to ‹assoc (function_oracle h ⊗⇩o id_cblinfun)› DEADID.rel_mono_strong)
       apply (simp add: assoc_def register_pair_Fst[unfolded o_def, THEN fun_cong] flip: Fst_def)
      apply (rule arg_cong[where f=‹λx. (_;_) x *⇩V _›])
      by (auto intro!: equal_ket simp: Snd_def tensor_op_ket cinner_ket tensor_ell2_ket assms
          assoc_ell2_sandwich sandwich_apply function_oracle_apply)
    also have ‹… = ((Fst ∘ X;(Fst ∘ Y;Snd)) ((Fst; Snd o Fst) (function_oracle h)) o⇩C⇩L Snd (selfbutter (ket (Some o h)))) *⇩V (ψ ⊗⇩s ket (Some ∘ h))›
      by (simp add: register_mult[symmetric, where F=‹(_;_)›] register_pair_Snd[unfolded o_def, THEN fun_cong])
    also have ‹… = (Fst ∘ X;(Fst ∘ Y;Snd)) ((Fst; Snd o Fst) (function_oracle h)) *⇩V (ψ ⊗⇩s ket (Some ∘ h))›
      by simp
    also have ‹… = Fst ((X;Y) (function_oracle h)) *⇩V (ψ ⊗⇩s ket (Some ∘ h))›
      apply (rewrite at ‹(Fst ∘ X;(Fst ∘ Y;Snd)) ((Fst;Snd ∘ Fst) _)› to ‹((Fst ∘ X;(Fst ∘ Y;Snd)) o (Fst;Snd ∘ Fst)) _› DEADID.rel_mono_strong)
       apply simp
      apply (subst register_comp_pair[symmetric])
        apply (simp, simp)
      by (simp add: register_pair_Snd register_pair_Fst register_comp_pair flip: comp_assoc)
    also have ‹… = ((X;Y) (function_oracle h) *⇩V ψ) ⊗⇩s ket (Some ∘ h)›
      by (simp add: Fst_def tensor_op_ell2)
    also have ‹… = exec_program_step h step ψ ⊗⇩s ket (Some ∘ h)›
      by (simp add: QueryStep)
    finally show ?thesis
      by -
  qed
  then show ?case
    by (simp add: exec_program_with_append exec_program_append snoc.IH o_def
        complex_vector.linear_sum[where f=‹exec_program_step_with standard_query step›]
        bounded_clinear.clinear bounded_clinear_exec_program_step_with scaleR_scaleC
        clinear.scaleC)
qed



lemma standard_query_is_ro_dist_inv_generic:
  fixes standard_query :: ‹('x::finite × 'y::{finite,ab_group_add} × ('x ⇀ 'y)) ell2 ⇒⇩C⇩L _›
  assumes ‹⋀H x y z. H x = Some z ⟹ standard_query *⇩V (ket (x,y,H)) = ket (x, y + z, H)› (* e.g. standard_query_ket_full_Some *)
  assumes ‹valid_program program›
  assumes [register]: ‹register Q›
  shows ‹dist_inv_avg Q (λ_. I) (λh. exec_program h program initial_state) =
    dist_inv (Fst o Q) I (exec_program_with standard_query program (initial_state ⊗⇩s superpos_total))› (is ‹?lhs = ?rhs›)
proof -
  have ‹?rhs⇧2 = (dist_inv (Fst ∘ Q) I (∑h∈UNIV. (exec_program h program initial_state ⊗⇩s ket (Some ∘ h)) /⇩R sqrt (real CARD('x ⇒ 'y))))⇧2›
    apply (subst standard_query_is_ro_generic)
    using assms by simp_all
  also have ‹… = (norm (∑i∈UNIV. ((Q (Proj (- I)) *⇩V exec_program i program initial_state) ⊗⇩s ket (Some ∘ i)) /⇩R sqrt (real CARD('x ⇒ 'y))))⇧2›
    by (simp add: dist_inv_def cblinfun.sum_right Fst_def tensor_op_ell2 cblinfun.scaleR_right)
  also have ‹… = (∑a∈UNIV. (norm (((Q (Proj (- I)) *⇩V exec_program a program initial_state) ⊗⇩s ket (Some ∘ a)) /⇩R sqrt (real CARD('x ⇒ 'y))))⇧2)›
    apply (subst pythagorean_theorem_sum)
      apply (simp, metis fun.inj_map_strong option.inject)
     apply simp
    by simp
  also have ‹… = (∑a∈UNIV. (dist_inv (Fst o Q) I (exec_program a program initial_state ⊗⇩s ket (Some ∘ a)))⇧2 /⇩R real CARD('x ⇒ 'y))›
    by (auto intro!: sum.cong simp: dist_inv_def Fst_def tensor_op_ell2 power_mult_distrib real_inv_sqrt_pow2)
  also have ‹… = (∑x∈UNIV. (dist_inv Q I (exec_program x program initial_state))⇧2) /⇩R real CARD('x ⇒ 'y)›
    by (metis (no_types, lifting) dist_inv_Fst_tensor norm_ket scaleR_right.sum sum.cong)
  also have ‹… = ?lhs⇧2›
    by (simp add: dist_inv_avg_def real_sqrt_pow2 sum_nonneg divide_inverse flip: sum_distrib_left)
  finally show ?thesis
    by simp
qed

lemma (in compressed_oracle) standard_query_is_ro_dist_inv:
  assumes ‹valid_program program›
  assumes [register]: ‹register Q›
  shows ‹dist_inv_avg Q (λ_. I) (λh. exec_program h program initial_state) =
    dist_inv (Fst o Q) I (exec_program_with standard_query program (initial_state ⊗⇩s superpos_total))› (is ‹?lhs = ?rhs›)
  using standard_query_ket_full_Some assms by (rule standard_query_is_ro_dist_inv_generic)

lemma (in compressed_oracle) standard_query'_is_ro_dist_inv:
  assumes ‹valid_program program›
  assumes [register]: ‹register Q›
  shows ‹dist_inv_avg Q (λ_. I) (λh. exec_program h program initial_state) =
    dist_inv (Fst o Q) I (exec_program_with standard_query' program (initial_state ⊗⇩s superpos_total))› (is ‹?lhs = ?rhs›)
  using standard_query'_ket_full_Some assms by (rule standard_query_is_ro_dist_inv_generic)



lemma (in compressed_oracle) compress_query_is_standard_query_generic:
  fixes query standard_query
  assumes ‹valid_program program›
  assumes ‹standard_query o⇩C⇩L reg_3_3 compress = reg_3_3 compress o⇩C⇩L query›
  shows ‹exec_program_with standard_query program (initial_state ⊗⇩s superpos_total)
      =  Snd compress *⇩V exec_program_with query program (initial_state ⊗⇩s ket (λx. None))›
proof (insert ‹valid_program program›, induction program rule: rev_induct)
  case Nil
  then show ?case
    by (simp add: compress_empty)
next
  case (snoc program_step prog)
  then have [simp]: ‹valid_program prog›
    by (simp add: valid_program_def)
  show ?case
  proof (cases program_step)
    case (ProgramStep U)
    have ‹exec_program_with standard_query (prog @ [program_step]) (initial_state ⊗⇩s superpos_total)
         = Fst U *⇩V Snd compress *⇩V exec_program_with query prog (initial_state ⊗⇩s ket Map.empty)›
      by (simp add: ProgramStep snoc.IH exec_program_with_append)
    also have ‹… = Snd compress *⇩V Fst U *⇩V exec_program_with query prog (initial_state ⊗⇩s ket Map.empty)›
      by (simp flip: cblinfun_apply_cblinfun_compose swap_registers)
    also have ‹… = Snd compress *⇩V exec_program_with query (prog @ [program_step]) (initial_state ⊗⇩s ket Map.empty)›
      by (simp add: ProgramStep exec_program_with_append)
    finally show ?thesis
      by -
  next
    case (QueryStep X Y)
    with snoc.prems have [register]: ‹compatible X Y›
      by (simp add: valid_program_def)
    have aux: ‹(Fst ∘ X;(Fst ∘ Y;Snd)) (reg_3_3 compress) = Snd compress›
      by (simp add: reg_3_3_def register_pair_Snd[unfolded o_def, THEN fun_cong])
    have ‹exec_program_with standard_query (prog @ [program_step]) (initial_state ⊗⇩s superpos_total)
          = (Fst ∘ X;(Fst ∘ Y;Snd)) standard_query *⇩V Snd compress *⇩V exec_program_with query prog (initial_state ⊗⇩s ket Map.empty)›
      by (simp add: QueryStep snoc.IH exec_program_with_append)
    also have ‹… = (Fst ∘ X;(Fst ∘ Y;Snd)) (standard_query o⇩C⇩L reg_3_3 compress) *⇩V exec_program_with query prog (initial_state ⊗⇩s ket Map.empty)›
      by (simp_all add: aux flip: register_mult)
    also have ‹… = (Fst ∘ X;(Fst ∘ Y;Snd)) (reg_3_3 compress o⇩C⇩L query) *⇩V exec_program_with query prog (initial_state ⊗⇩s ket Map.empty)›
      by (simp add: assms)
    also have ‹… = Snd compress *⇩V (Fst ∘ X;(Fst ∘ Y;Snd)) query *⇩V (exec_program_with query) prog (initial_state ⊗⇩s ket Map.empty)›
      by (simp_all add: aux flip: register_mult)
    also have ‹… = Snd compress *⇩V (exec_program_with query) (prog @ [program_step]) (initial_state ⊗⇩s ket (λx. None))›
      by (simp add: QueryStep Cons exec_program_with_append)
    finally show ?thesis
      by -
  qed
qed



lemma (in compressed_oracle) query_is_standard_query_generic:
  fixes query standard_query
  assumes ‹valid_program program›
  assumes ‹standard_query o⇩C⇩L reg_3_3 compress = reg_3_3 compress o⇩C⇩L query›
  shows ‹dist_inv Fst I (exec_program_with standard_query program (initial_state ⊗⇩s superpos_total))
       = dist_inv Fst I (exec_program_with query program (initial_state ⊗⇩s ket (λx. None)))›
proof -
  have ‹dist_inv Fst I (exec_program_with standard_query program (initial_state ⊗⇩s superpos_total))
       = norm (Fst (Proj (- I)) *⇩V Snd compress *⇩V exec_program_with query program (initial_state ⊗⇩s ket (λx. None)))›
    by (simp add: compress_query_is_standard_query_generic assms dist_inv_def Proj_on_own_range register_projector)
  also have ‹… = norm (Snd compress *⇩V Fst (Proj (- I)) *⇩V exec_program_with query program (initial_state ⊗⇩s ket (λx. None)))›
    by (simp flip: cblinfun_apply_cblinfun_compose swap_registers)
  also have ‹… = norm (Fst (Proj (- I)) *⇩V exec_program_with query program (initial_state ⊗⇩s ket (λx. None)))›
    by (simp add: isometry_preserves_norm register_isometry[where F=Snd])
  also have ‹… = dist_inv Fst I (exec_program_with query program (initial_state ⊗⇩s ket (λx. None)))›
    by (simp add: dist_inv_def Proj_on_own_range register_projector)
  finally show ?thesis
    by -
qed



lemma (in compressed_oracle) query_is_standard_query:
  assumes ‹valid_program program›
  shows
  ‹dist_inv Fst I (exec_program_with standard_query program (initial_state ⊗⇩s superpos_total)) =
   dist_inv Fst I (exec_program_with query program (initial_state ⊗⇩s ket (λx. None)))›
  using query_is_standard_query_generic standard_query_compress assms by blast

lemma (in compressed_oracle) query'_is_standard_query:
  assumes ‹valid_program program›
  shows
  ‹dist_inv Fst I (exec_program_with standard_query' program (initial_state ⊗⇩s superpos_total)) =
   dist_inv Fst I (exec_program_with query' program (initial_state ⊗⇩s ket (λx. None)))›
  using query_is_standard_query_generic standard_query'_compress assms by blast

lemma (in compressed_oracle) query_is_random_oracle:
  assumes ‹valid_program program›
  shows ‹dist_inv_avg id (λ_. I) (λh. exec_program h program initial_state) =
         dist_inv Fst I (exec_program_with query program (initial_state ⊗⇩s ket (λ_. None)))›
  by (simp add: standard_query_is_ro_dist_inv assms query_is_standard_query)


lemma (in compressed_oracle) query'_is_random_oracle:
  assumes ‹valid_program program›
  shows ‹dist_inv_avg id (λ_. I) (λh. exec_program h program initial_state) =
         dist_inv Fst I (exec_program_with query' program (initial_state ⊗⇩s ket (λ_. None)))›
  by (simp add: standard_query'_is_ro_dist_inv assms query'_is_standard_query)


lemma (in compressed_oracle) dist_inv_exec_query_exec_fixed:
  fixes program :: ‹('mem, 'x::finite, 'y::{finite,ab_group_add}) program_step list›
  fixes Q :: ‹'a ell2 ⇒⇩C⇩L 'a ell2 ⇒ 'mem ell2 ⇒⇩C⇩L 'mem ell2›
  assumes ‹valid_program program›
  assumes [register]: ‹register Q›
  shows ‹dist_inv (Fst ∘ Q) I (exec_program_with query program (ψ ⊗⇩s ket (λ_. None)))
       = dist_inv_avg Q (λ_. I) (λh. exec_program h program ψ)›
proof -
  have ‹dist_inv (Fst ∘ Q) I (exec_program_with query program (ψ ⊗⇩s ket (λ_. None)))
      = dist_inv Fst (lift_invariant Q I) (exec_program_with query program (ψ ⊗⇩s ket (λ_. None)))›
    by (metis (no_types, lifting) Proj_lift_invariant assms(2) dist_inv_def lift_invariant_compl o_apply)
  also have ‹… = dist_inv_avg id (λh. lift_invariant Q I) (λh. exec_program h program ψ)›
    by (simp add: query_is_random_oracle assms)
  also have ‹… = dist_inv_avg Q (λ_. I) (λh. exec_program h program ψ)›
    by (simp add: dist_inv_avg_register_rewrite)
  finally show ?thesis
    by -
qed

lemma (in compressed_oracle) dist_inv_exec_query'_exec_fixed:
  fixes program :: ‹('mem, 'x::finite, 'y::{finite,ab_group_add}) program_step list›
  fixes Q :: ‹'a ell2 ⇒⇩C⇩L 'a ell2 ⇒ 'mem ell2 ⇒⇩C⇩L 'mem ell2›
  assumes ‹valid_program program›
  assumes [register]: ‹register Q›
  shows ‹dist_inv (Fst ∘ Q) I (exec_program_with query' program (ψ ⊗⇩s ket (λ_. None)))
       = dist_inv_avg Q (λ_. I) (λh. exec_program h program ψ)›
proof -
  have ‹dist_inv (Fst ∘ Q) I (exec_program_with query' program (ψ ⊗⇩s ket (λ_. None)))
      = dist_inv Fst (lift_invariant Q I) (exec_program_with query' program (ψ ⊗⇩s ket (λ_. None)))›
    by (metis (no_types, lifting) Proj_lift_invariant assms(2) dist_inv_def lift_invariant_compl o_apply)
  also have ‹… = dist_inv_avg id (λh. lift_invariant Q I) (λh. exec_program h program ψ)›
    by (simp add: query'_is_random_oracle assms)
  also have ‹… = dist_inv_avg Q (λ_. I) (λh. exec_program h program ψ)›
    by (simp add: dist_inv_avg_register_rewrite)
  finally show ?thesis
    by -
qed


end