Theory Grover

section ‹Grover's algorithm›

theory Grover
  imports Partial_State Gates Quantum_Hoare
begin

subsection ‹Basic definitions›

locale grover_state =
  fixes n :: nat  (* number of qubits *)
    and f :: "nat ⇒ bool"  (* characteristic function, only need values in [0,N). *)
  assumes n: "n > 1"
    and dimM: "card {i. i < (2::nat) ^ n ∧ f i} > 0"
              "card {i. i < (2::nat) ^ n ∧ f i} < (2::nat) ^ n"
begin

definition N where
  "N = (2::nat) ^ n"

definition M where
  "M = card {i. i < N ∧ f i}"

lemma N_ge_0 [simp]: "0 < N" by (simp add: N_def)

lemma M_ge_0 [simp]: "0 < M" by (simp add: M_def dimM N_def)

lemma M_neq_0 [simp]: "M ≠ 0" by simp

lemma M_le_N [simp]: "M < N" by (simp add: M_def dimM N_def)

lemma M_not_ge_N [simp]: "¬ M ≥ N" using M_le_N by arith

definition ψ :: "complex vec" where
  "ψ = Matrix.vec N (λi. 1 / sqrt N)"

lemma ψ_dim [simp]:
  "ψ ∈ carrier_vec N"
  "dim_vec ψ = N"
  by (simp add: ψ_def)+

lemma ψ_eval:
  "i < N ⟹ ψ $ i = 1 / sqrt N"
  by (simp add: ψ_def)

lemma ψ_inner:
  "inner_prod ψ ψ = 1"
  apply (simp add: ψ_eval scalar_prod_def)
  by (smt of_nat_less_0_iff of_real_mult of_real_of_nat_eq real_sqrt_mult_self)
 
lemma ψ_norm:
  "vec_norm ψ = 1"
  by (simp add: ψ_eval vec_norm_def scalar_prod_def)

definition α :: "complex vec" where
  "α = Matrix.vec N (λi. if f i then 0 else 1 / sqrt (N - M))"

lemma α_dim [simp]:
  "α ∈ carrier_vec N"
  "dim_vec α = N"
  by (simp add: α_def)+

lemma α_eval:
  "i < N ⟹ α $ i = (if f i then 0 else 1 / sqrt (N - M))"
  by (simp add: α_def)

lemma α_inner:
  "inner_prod α α = 1"
  apply (simp add: scalar_prod_def α_eval)
  apply (subst sum.mono_neutral_cong_right[of "{0..<N}" "{0..<N}-{i. i < N ∧ f i}"])
   apply auto
  apply (subgoal_tac "card ({0..<N} - {i. i < N ∧ f i}) = N - M")
  subgoal by (metis of_nat_0_le_iff of_real_of_nat_eq of_real_power power2_eq_square real_sqrt_pow2)
  unfolding N_def M_def 
  by (metis (no_types, lifting) atLeastLessThan_iff card.infinite card_Diff_subset card_atLeastLessThan diff_zero dimM(1) mem_Collect_eq neq0_conv subsetI zero_order(1))

definition β :: "complex vec" where
  "β = Matrix.vec N (λi. if f i then 1 / sqrt M else 0)"

lemma β_dim [simp]:
  "β ∈ carrier_vec N"
  "dim_vec β = N"
  by (simp add: β_def)+

lemma β_eval:
  "i < N ⟹ β $ i = (if f i then 1 / sqrt M else 0)"
  by (simp add: β_def)

lemma β_inner:
  "inner_prod β β = 1"  
  apply (simp add: scalar_prod_def β_eval)
  apply (subst sum.mono_neutral_cong_right[of "{0..<N}" "{i. i < N ∧ f i}"])
   apply auto
  apply (fold M_def)
  by (metis of_nat_0_le_iff of_real_of_nat_eq of_real_power power2_eq_square real_sqrt_pow2)

lemma alpha_beta_orth:
  "inner_prod α β = 0"
  unfolding α_def β_def by (simp add: scalar_prod_def)

lemma beta_alpha_orth:
  "inner_prod β α = 0"
  unfolding α_def β_def by (simp add: scalar_prod_def)

definition θ :: real where
  "θ = 2 * arccos (sqrt ((N - M) / N))"

lemma cos_theta_div_2:
  "cos (θ / 2) = sqrt ((N - M) / N)"
proof -
  have "θ / 2 = arccos (sqrt ((N - M) / N))" using θ_def by simp
  then show "cos (θ / 2) = sqrt ((N - M) / N)" 
    by (simp add: cos_arccos_abs)
qed

lemma sin_theta_div_2:
  "sin (θ / 2) = sqrt (M / N)"
proof -
  have a: "θ / 2 = arccos (sqrt ((N - M) / N))" using θ_def by simp
  have N: "N > 0" using N_def by auto
  have M: "M < N" using M_def dimM N_def by auto
  then show "sin (θ / 2) = sqrt (M / N)"
    unfolding a
    apply (simp add: sin_arccos_abs)
  proof -
    have eq: "real (N - M) = real N - real M" using N M 
      using M_not_ge_N nat_le_linear of_nat_diff by blast
    have "1 - real (N - M) / real N = (real N - (real N - real M)) / real N" 
      unfolding eq using N 
      by (metis diff_divide_distrib divide_self_if eq gr_implies_not0 of_nat_0_eq_iff)
    then show "1 - real (N - M) / real N = real M / real N" by auto
  qed
qed

lemma θ_neq_0:
  "θ ≠ 0"
proof -
  {
  assume "θ = 0"
  then have "θ / 2 = 0" by auto
  then have "sin (θ / 2) = 0" by auto
  }
  note z = this
  have "sin (θ / 2) = sqrt (M / N)" using sin_theta_div_2 by auto
  moreover have "M > 0" unfolding M_def N_def using dimM by auto
  ultimately have "sin (θ / 2) > 0" by auto
  with z show ?thesis by auto
qed

abbreviation ccos where "ccos φ ≡ complex_of_real (cos φ)"
abbreviation csin where "csin φ ≡ complex_of_real (sin φ)"

lemma ψ_eq:
  "ψ = ccos (θ / 2) ⋅⇩v α + csin (θ / 2) ⋅⇩v β"
  apply (simp add: cos_theta_div_2 sin_theta_div_2)
  apply (rule eq_vecI)
  by (auto simp add: α_def β_def ψ_def real_sqrt_divide)

lemma psi_inner_alpha:
  "inner_prod ψ α = ccos (θ / 2)"
  unfolding ψ_eq
proof -
  have "inner_prod (ccos (θ / 2) ⋅⇩v α) α = ccos (θ / 2)"
    apply (subst inner_prod_smult_right[of _ N])
    using α_dim α_inner by auto
  moreover have "inner_prod (csin (θ / 2) ⋅⇩v β) α = 0"
    apply (subst inner_prod_smult_right[of _ N])
    using α_dim β_dim beta_alpha_orth by auto
  ultimately show "inner_prod (ccos (θ / 2) ⋅⇩v α + csin (θ / 2) ⋅⇩v β) α = ccos (θ / 2)"
    apply (subst inner_prod_distrib_left[of _ N])
    using α_dim β_dim by auto
qed

lemma psi_inner_beta:
  "inner_prod ψ β = csin (θ / 2)"
  unfolding ψ_eq
proof -
  have "inner_prod (ccos (θ / 2) ⋅⇩v α) β = 0"
    apply (subst inner_prod_smult_right[of _ N])
    using α_dim β_dim alpha_beta_orth by auto
  moreover have "inner_prod (csin (θ / 2) ⋅⇩v β) β = csin (θ / 2)"
    apply (subst inner_prod_smult_right[of _ N])
    using β_dim β_inner by auto
  ultimately show "inner_prod (ccos (θ / 2) ⋅⇩v α + csin (θ / 2) ⋅⇩v β) β = csin (θ / 2)"
    apply (subst inner_prod_distrib_left[of _ N])
    using α_dim β_dim by auto
qed

definition alpha_l :: "nat ⇒ complex" where
  "alpha_l l = ccos ((l + 1 / 2) * θ)"

lemma alpha_l_real:
  "alpha_l l ∈ Reals"
  unfolding alpha_l_def by auto

lemma cnj_alpha_l:
  "conjugate (alpha_l l) = alpha_l l"
  using alpha_l_real Reals_cnj_iff by auto

definition beta_l :: "nat ⇒ complex" where
  "beta_l l = csin ((l + 1 / 2) * θ)"

lemma beta_l_real:
  "beta_l l ∈ Reals"
  unfolding beta_l_def by auto

lemma cnj_beta_l:
  "conjugate (beta_l l) = beta_l l"
  using beta_l_real Reals_cnj_iff by auto

lemma csin_ccos_squared_add:
  "ccos (a::real) * ccos a + csin a * csin a = 1"
  by (smt cos_diff cos_zero of_real_add of_real_hom.hom_one of_real_mult)

lemma alpha_l_beta_l_add_norm:
  "alpha_l l * alpha_l l + beta_l l * beta_l l = 1"
  using alpha_l_def beta_l_def csin_ccos_squared_add by auto

definition psi_l where
  "psi_l l = (alpha_l l) ⋅⇩v α + (beta_l l) ⋅⇩v β"

lemma psi_l_dim:
  "psi_l l ∈ carrier_vec N"
  unfolding psi_l_def α_def β_def by auto

lemma inner_psi_l:
  "inner_prod (psi_l l) (psi_l l) = 1"
proof -
  have eq0: "inner_prod (psi_l l) (psi_l l) 
    = inner_prod ((alpha_l l) ⋅⇩v α) (psi_l l) + inner_prod ((beta_l l) ⋅⇩v β) (psi_l l)"
    unfolding psi_l_def
    apply (subst inner_prod_distrib_left)
    using α_def β_def by auto
  have "inner_prod ((alpha_l l) ⋅⇩v α) (psi_l l) 
    = inner_prod ((alpha_l l) ⋅⇩v α) ((alpha_l l) ⋅⇩v α) + inner_prod ((alpha_l l) ⋅⇩v α) ((beta_l l) ⋅⇩v β)"
    unfolding psi_l_def
    apply (subst inner_prod_distrib_right)
    using α_def β_def by auto
  also have "… = (conjugate (alpha_l l)) * (alpha_l l) * inner_prod α α 
                + (conjugate (alpha_l l)) * (beta_l l) * inner_prod α β"
    apply (subst (1 2) inner_prod_smult_left_right) using α_def β_def by auto
  also have "… = conjugate (alpha_l l) * (alpha_l l) "
    by (simp add: alpha_beta_orth α_inner)
  also have "… = (alpha_l l) * (alpha_l l)" using cnj_alpha_l by simp
  finally have eq1: "inner_prod (alpha_l l ⋅⇩v α) (psi_l l) = alpha_l l * alpha_l l".

  have "inner_prod ((beta_l l) ⋅⇩v β) (psi_l l) 
    = inner_prod ((beta_l l) ⋅⇩v β) ((alpha_l l) ⋅⇩v α) + inner_prod ((beta_l l) ⋅⇩v β) ((beta_l l) ⋅⇩v β)"
    unfolding psi_l_def
    apply (subst inner_prod_distrib_right)
    using α_def β_def by auto
  also have "… = (conjugate (beta_l l)) * (alpha_l l) * inner_prod β α 
                + (conjugate (beta_l l)) * (beta_l l) * inner_prod β β"
    apply (subst (1 2) inner_prod_smult_left_right) using α_def β_def by auto
  also have "… = (conjugate (beta_l l)) * (beta_l l)"  using β_inner beta_alpha_orth by auto
  also have "… = (beta_l l) * (beta_l l)" using cnj_beta_l by auto
  finally have eq2: "inner_prod (beta_l l ⋅⇩v β) (psi_l l) = beta_l l * beta_l l".

  show ?thesis unfolding eq0 eq1 eq2 using alpha_l_beta_l_add_norm by auto
qed

abbreviation proj :: "complex vec ⇒ complex mat" where
  "proj v ≡ outer_prod v v"

definition psi'_l where
  "psi'_l l = (alpha_l l) ⋅⇩v α - (beta_l l) ⋅⇩v β"

lemma psi'_l_dim:
  "psi'_l l ∈ carrier_vec N"
  unfolding psi'_l_def α_def β_def by auto

definition proj_psi'_l where
  "proj_psi'_l l = proj (psi'_l l)"

lemma proj_psi'_dim:
  "proj_psi'_l l ∈ carrier_mat N N"
  unfolding proj_psi'_l_def using psi'_l_dim by auto

lemma psi_inner_psi'_l:
  "inner_prod ψ (psi'_l l) = (alpha_l l * ccos (θ / 2) - beta_l l * csin (θ / 2))"
proof -
  have "inner_prod ψ (psi'_l l) = inner_prod ψ (alpha_l l ⋅⇩v α) - inner_prod ψ (beta_l l ⋅⇩v β)"
    unfolding psi'_l_def apply (subst inner_prod_minus_distrib_right[of _ N]) by auto
  also have "… = alpha_l l * (inner_prod ψ α) - beta_l l * (inner_prod ψ β)"
    using ψ_dim α_dim β_dim by auto
  also have "… = alpha_l l * (ccos (θ / 2)) - beta_l l * (csin (θ / 2))"
    using psi_inner_alpha psi_inner_beta by auto
  finally show ?thesis by auto
qed

lemma double_ccos_square:
  "2 * ccos (a::real) * ccos a = ccos (2 * a) + 1"
proof -
  have eq: "ccos (2 * a) = ccos a * ccos a - csin a * csin a"
    using cos_add[of a a] by auto
  have "csin a * csin a = 1 - ccos a * ccos a"
    using csin_ccos_squared_add[of a]
    by (metis add_diff_cancel_left')
  then have "ccos a * ccos a - csin a * csin a = 2 * ccos a * ccos a - 1"
    by simp
  with eq show ?thesis by simp 
qed

lemma double_csin_square:
  "2 * csin (a::real) * csin a = 1 - ccos (2 * a)"
proof -
  have eq: "ccos (2 * a) = ccos a * ccos a - csin a * csin a"
    using cos_add[of a a] by auto
  have "ccos a * ccos a = 1 - csin a * csin a"
    using csin_ccos_squared_add[of a]
      by (auto intro: add_implies_diff)
  then have "ccos a * ccos a - csin a * csin a = 1 - 2 * csin (a::real) * csin a"
    by simp
  with eq show ?thesis by simp
qed

lemma csin_double:
  "2 * csin (a::real) * ccos a = csin(2 * a)"
  using sin_add[of a a] by simp

lemma ccos_add:
  "ccos (x + y) = ccos x * ccos y - csin x * csin y"
  using cos_add[of x y] by simp

lemma alpha_l_Suc_l_derive:
  "2 * (alpha_l l * ccos (θ / 2) - beta_l l * csin (θ / 2)) * ccos (θ / 2) - alpha_l l = alpha_l (l + 1)"
  (is "?lhs = ?rhs")
proof -
  have "2 * ((alpha_l l) * ccos (θ / 2) - (beta_l l) * csin (θ / 2)) * ccos (θ / 2)
    = (alpha_l l) * (2 * ccos (θ / 2)* ccos (θ / 2)) - (beta_l l) * (2 * csin (θ / 2) * ccos (θ / 2))" 
    by (simp add: left_diff_distrib)

  also have "… = (alpha_l l) * (ccos (θ) + 1) - (beta_l l) * csin θ"
    using double_ccos_square csin_double by auto
  finally have "2 * ((alpha_l l) * ccos (θ / 2) - (beta_l l) * csin (θ / 2)) * ccos (θ / 2) 
    = (alpha_l l) * (ccos (θ) + 1) - (beta_l l) * csin θ".
  then have "?lhs = (alpha_l l) * ccos (θ) - (beta_l l) * csin θ" by (simp add: algebra_simps)
  also have "… = (alpha_l (l + 1))"
    unfolding alpha_l_def beta_l_def 
    apply (subst ccos_add[of "(real l + 1 / 2) * θ" "θ", symmetric])
    by (simp add: algebra_simps)
  finally show ?thesis by auto
qed

lemma csin_add:
  "csin (x + y) = ccos x * csin y + csin x * ccos y"
  using sin_add[of x y] by simp

lemma beta_l_Suc_l_derive:
  "2 * (alpha_l l * ccos (θ / 2) - (beta_l l) * csin (θ / 2)) * csin (θ / 2) + beta_l l = beta_l (l + 1)"
  (is "?lhs = ?rhs")
proof -
  have "2 * ((alpha_l l) * ccos (θ / 2) - (beta_l l) * csin (θ / 2)) * csin (θ / 2)
    = (alpha_l l) * (2 * csin (θ / 2)* ccos (θ / 2)) - (beta_l l) * (2 * csin (θ / 2) * csin (θ / 2))" 
    by (simp add: left_diff_distrib)
  also have "… = (alpha_l l) * (csin θ) - (beta_l l) * (1 - ccos (θ))"
    using double_csin_square csin_double by auto
  finally have "2 * ((alpha_l l) * ccos (θ / 2) - (beta_l l) * csin (θ / 2)) * csin (θ / 2)
    = (alpha_l l) * (csin θ) - (beta_l l) * (1 - ccos (θ))".
  then have "?lhs = (alpha_l l) * (csin θ) + (beta_l l) * ccos θ" by (simp add: algebra_simps)
  also have "… = (beta_l (l + 1))"
    unfolding alpha_l_def beta_l_def 
    apply (subst csin_add[of "(real l + 1 / 2) * θ" "θ", symmetric])
    by (simp add: algebra_simps)
  finally show ?thesis by auto
qed

lemma psi_l_Suc_l_derive:
  "2 * (alpha_l l * ccos (θ / 2) - beta_l l * csin (θ / 2)) ⋅⇩v ψ - psi'_l l = psi_l (l + 1)"
  (is "?lhs = ?rhs")
proof -
  let ?l = "2 * ((alpha_l l) * ccos (θ / 2) - (beta_l l) * csin (θ / 2))"
  have "?l ⋅⇩v ψ = ?l ⋅⇩v (ccos (θ / 2) ⋅⇩v α + csin (θ / 2) ⋅⇩v β)" unfolding ψ_eq by auto
  also have "… = ?l ⋅⇩v (ccos (θ / 2) ⋅⇩v α) + ?l ⋅⇩v (csin (θ / 2) ⋅⇩v β)" 
    apply (subst smult_add_distrib_vec[of _ N]) using α_dim β_dim by auto
  also have "… = (?l * ccos (θ / 2)) ⋅⇩v α + (?l * csin (θ / 2)) ⋅⇩v β" by auto
  finally have "?l ⋅⇩v ψ  = (?l * ccos (θ / 2)) ⋅⇩v α + (?l * csin (θ / 2)) ⋅⇩v β".
  then have "?l ⋅⇩v ψ - (psi'_l l) = ((?l * ccos (θ / 2)) ⋅⇩v α - (alpha_l l) ⋅⇩v α) + ((?l * csin (θ / 2)) ⋅⇩v β + (beta_l l) ⋅⇩v β)"
    unfolding psi'_l_def by auto
  also have "… = (?l * ccos (θ / 2) - alpha_l l) ⋅⇩v α + (?l * csin (θ / 2) + beta_l l) ⋅⇩v β"
    apply (subst minus_smult_vec_distrib) apply (subst add_smult_distrib_vec) by auto
  also have "… = (alpha_l (l + 1)) ⋅⇩v α + (beta_l (l + 1)) ⋅⇩v β"
    using alpha_l_Suc_l_derive beta_l_Suc_l_derive by auto
  finally have "?l ⋅⇩v ψ - (psi'_l l) = (alpha_l (l + 1)) ⋅⇩v α + (beta_l (l + 1)) ⋅⇩v β".
  then show ?thesis unfolding psi_l_def by auto
qed

subsection ‹Grover operator›

text ‹Oracle O›

definition proj_O :: "complex mat" where
  "proj_O = mat N N (λ(i, j). if i = j then (if f i then 1 else 0) else 0)"

lemma proj_O_dim:
  "proj_O ∈ carrier_mat N N"
  unfolding proj_O_def by auto

lemma proj_O_mult_alpha:
  "proj_O *⇩v α = zero_vec N"
  by (auto simp add: proj_O_def α_def scalar_prod_def)

lemma proj_O_mult_beta:
  "proj_O *⇩v β = β"
  by (auto simp add: proj_O_def β_def scalar_prod_def sum_only_one_neq_0)

definition mat_O :: "complex mat" where
  "mat_O = mat N N (λ(i,j). if i = j then (if f i then -1 else 1) else 0)"

lemma mat_O_dim:
  "mat_O ∈ carrier_mat N N"
  unfolding mat_O_def by auto

lemma mat_O_mult_alpha:
  "mat_O *⇩v α = α"
  by (auto simp add: mat_O_def α_def scalar_prod_def sum_only_one_neq_0)

lemma mat_O_mult_beta:
  "mat_O *⇩v β = - β"
  by (auto simp add: mat_O_def β_def scalar_prod_def sum_only_one_neq_0)

lemma hermitian_mat_O:
  "hermitian mat_O"
  by (auto simp add: hermitian_def mat_O_def adjoint_eval)

lemma unitary_mat_O:
  "unitary mat_O"
proof -
  have "mat_O ∈ carrier_mat N N" unfolding mat_O_def by auto
  moreover have "mat_O * adjoint mat_O = mat_O * mat_O" using hermitian_mat_O unfolding hermitian_def by auto
  moreover have "mat_O * mat_O = 1⇩m N"
    apply (rule eq_matI)
    unfolding mat_O_def
      apply (simp add: scalar_prod_def)
    subgoal for i j apply (rule)
      subgoal apply (subst sum_only_one_neq_0[of "{0..<N}" "j"]) by auto
        apply (subst sum_only_one_neq_0[of "{0..<N}" "j"]) by auto
    by auto
  ultimately show ?thesis unfolding unitary_def inverts_mat_def by auto
qed

definition mat_Ph :: "complex mat" where
  "mat_Ph = mat N N (λ(i,j). if i = j then if i = 0 then 1 else -1 else 0)"

lemma hermitian_mat_Ph:
  "hermitian mat_Ph"
  unfolding hermitian_def mat_Ph_def
  apply (rule eq_matI)
  by (auto simp add: adjoint_eval)

lemma unitary_mat_Ph:
  "unitary mat_Ph"
proof -
  have "mat_Ph ∈ carrier_mat N N" unfolding mat_Ph_def by auto
  moreover have "mat_Ph * adjoint mat_Ph = mat_Ph * mat_Ph" using hermitian_mat_Ph unfolding hermitian_def by auto
  moreover have "mat_Ph * mat_Ph = 1⇩m N"
    apply (rule eq_matI)
    unfolding mat_Ph_def
      apply (simp add: scalar_prod_def)
    subgoal for i j apply (rule)
      subgoal apply (subst sum_only_one_neq_0[of "{0..<N}" "0"]) by auto
        apply (subst sum_only_one_neq_0[of "{0..<N}" "j"]) by auto
    by auto
  ultimately show ?thesis unfolding unitary_def inverts_mat_def by auto
qed

definition mat_G' :: "complex mat" where
  "mat_G' = mat N N (λ(i,j). if i = j then 2 / N - 1 else 2 / N)"

text ‹Geometrically, the Grover operator G is a rotation›
definition mat_G :: "complex mat" where
  "mat_G = mat_G' * mat_O"

end

subsection ‹State of Grover's algorithm›

text ‹The dimensions are [2, 2, ..., 2, n]. We work with a very special
  case as in the paper›
locale grover_state_sig = grover_state + state_sig +
  fixes R :: nat
  fixes K :: nat
  assumes dims_def: "dims = replicate n 2 @ [K]"
  assumes R: "R = pi / (2 * θ) - 1 / 2"
  assumes K: "K > R"

begin

lemma K_gt_0:
  "K > 0"
  using K by auto

text ‹Bits q0 to q\_(n-1)›
definition vars1 :: "nat set" where
  "vars1 = {0 ..< n}"

text ‹Bit r›
definition vars2 :: "nat set" where
  "vars2 = {n}"

lemma length_dims:
  "length dims = n + 1"
  unfolding dims_def by auto

lemma dims_nth_lt_n:
  "l < n ⟹ nth dims l = 2" 
  unfolding dims_def by (simp add: nth_append)

lemma nths_Suc_n_dims:
  "nths dims {0..<(Suc n)} = dims" 
  using length_dims nths_upt_eq_take
  by (metis add_Suc_right add_Suc_shift lessThan_atLeast0 less_add_eq_less less_numeral_extra(4)
            not_less plus_1_eq_Suc take_all)

interpretation ps2_P: partial_state2 dims vars1 vars2
   apply unfold_locales unfolding vars1_def vars2_def by auto

interpretation ps_P: partial_state ps2_P.dims0 ps2_P.vars1'.

abbreviation tensor_P where
"tensor_P A B ≡ ps2_P.ptensor_mat A B"

lemma tensor_P_dim:
  "tensor_P A B ∈ carrier_mat d d"
proof -
  have "ps2_P.d0 = prod_list (nths dims ({0..<n} ∪ {n}))" unfolding ps2_P.d0_def ps2_P.dims0_def ps2_P.vars0_def 
    by (simp add: vars1_def vars2_def)
  also have "… = prod_list (nths dims ({0..<Suc n}))"
    apply (subgoal_tac "{0..<n} ∪ {n} = {0..<(Suc n)}") by auto
  also have "… = prod_list dims" using nths_Suc_n_dims by auto
  also have "… = d" unfolding d_def by auto
  finally show ?thesis  using ps2_P.ptensor_mat_carrier by auto
qed

lemma dims_nths_le_n:
  assumes "l ≤ n"
  shows "nths dims {0..<l} = replicate l 2"
proof (rule nth_equalityI, auto)
  have "l ≤ n ⟹ (i < Suc n ∧ i < l) = (i < l)" for i
    using less_trans by fastforce
  then show l: "length (nths dims {0..<l}) = l" using assms
    by (auto simp add: length_nths length_dims)

  have llt: "l < length dims" using length_dims assms by auto
  have v1: "⋀i. i < l ⟹ {a. a < i ∧ a ∈ {0..<l}} = {0..<i}" unfolding vars1_def by auto
  then have "⋀i. i < l ⟹ card {j. j < i ∧ j ∈ {0..<l}} = i" by auto 
  then have "nths dims {0..<l} ! i = dims ! i" if "i < l" for i
    using nth_nths_card[of i dims "{0..<l}"] that llt by auto
  moreover have "dims ! i = replicate n 2 ! i" if "i < n" for i unfolding dims_def 
    by (auto simp add: nth_append that)
  moreover have "replicate n 2 ! i = replicate l 2 ! i" if "i < l" for i using assms that by auto
  ultimately show "nths dims {0..<l} ! i = replicate l 2 ! i" if "i < length (nths dims {0..<l})" for i
    using l that assms by auto 
qed

lemma dims_nths_one_lt_n: 
  assumes "l < n"
  shows "nths dims {l} = [2]"
proof -
  have "{i. i < length dims ∧ i ∈ {l}} = {l}" using assms length_dims by auto
  then have "nths dims {l} = [dims ! l]" using nths_only_one[of dims "{l}" l] by auto
  moreover have "dims ! l = 2" unfolding dims_def using assms by (simp add: nth_append)
  ultimately show ?thesis by auto
qed

lemma dims_vars1:
  "nths dims vars1 = replicate n 2"
proof (rule nth_equalityI, auto)
  show l: "length (nths dims vars1) = n"
    apply (auto simp add: length_nths vars1_def length_dims)
    by (metis (no_types, lifting) Collect_cong Suc_lessD card_Collect_less_nat not_less_eq)

  have v1: "⋀i. i < n ⟹ {a. a < i ∧ a ∈ vars1} = {0..<i}" unfolding vars1_def by auto
  then have "⋀i. i < n ⟹ card {j. j < i ∧ j ∈ vars1} = i" by auto 
  then have "nths dims vars1 ! i = dims ! i" if "i < n" for i
    using nth_nths_card[of i dims vars1] that length_dims vars1_def by auto
  moreover have "dims ! i = replicate n 2 ! i" if "i < n" for i unfolding dims_def 
    by (simp add: nth_append that)
  ultimately show "nths dims vars1 ! i = replicate n 2 ! i" if "i < length (nths dims vars1)" for i
    using l that by auto 
qed

lemma nths_rep_2_n:
  "nths (replicate n 2) {n} = []"
  by (metis (no_types, lifting) Collect_empty_eq card.empty length_0_conv length_replicate less_Suc_eq not_less_eq nths_replicate singletonD)

lemma dims_vars2:
  "nths dims vars2 = [K]"
  unfolding dims_def vars2_def
  apply (subst nths_append)
  apply (subst nths_rep_2_n)
  by simp

lemma d_vars1:
  "prod_list (nths dims vars1) = N"
proof -
  have eq: "{0..<n} = {..<n}"  by auto
  have "nths (replicate n 2 @ [K]) {0..<n} = (replicate n 2)"
    apply (subst eq)
    using nths_upt_eq_take by simp
  then show ?thesis unfolding dims_def vars1_def N_def by auto
qed

lemma ps2_P_dims0:
  "ps2_P.dims0 = dims"
proof -
  have "vars1 ∪ vars2 = {0..<Suc n}" unfolding vars1_def vars2_def by auto
  then have dims: "nths dims (vars1 ∪ vars2) = dims" unfolding vars1_def vars2_def using nths_Suc_n_dims by auto
  then show ?thesis unfolding ps2_P.dims0_def ps2_P.vars0_def apply (subst dims) by auto
qed

lemma ps2_P_vars1':
  "ps2_P.vars1' = vars1"
  unfolding ps2_P.vars1'_def ps2_P.vars0_def  
proof -
  have eq: "vars1 ∪ vars2 = {0..<(Suc n)}" unfolding vars1_def vars2_def by auto
  have "x < Suc n ⟹ {i ∈ {0..<Suc n}. i < x} = {i. i < x}" for x by auto
  then have "x < Suc n ⟹ ind_in_set {0..<(Suc n)} x = x" for x unfolding ind_in_set_def by auto
  then have "x ∈ vars1 ⟹ ind_in_set {0..<(Suc n)} x = x" for x unfolding vars1_def by auto
  then have "ind_in_set {0..<(Suc n)} ` vars1 = vars1" by force
  with eq show "ind_in_set (vars1 ∪ vars2) ` vars1 = vars1" by auto
qed

lemma ps2_P_d0:
  "ps2_P.d0 = d"
  unfolding ps2_P.d0_def using ps2_P_dims0 d_def by auto

lemma ps2_P_d1:
  "ps2_P.d1 = N"
  unfolding ps2_P.d1_def ps2_P.dims1_def by (simp add: dims_vars1 N_def)

lemma ps2_P_d2:
  "ps2_P.d2 = K"
  unfolding ps2_P.d2_def ps2_P.dims2_def by (simp add: dims_vars2)

lemma ps_P_d:
  "ps_P.d = d"
  unfolding ps_P.d_def ps2_P_dims0 by auto

lemma ps_P_d1:
  "ps_P.d1 = N"
  unfolding ps_P.d1_def ps_P.dims1_def ps2_P.nths_vars1' using ps2_P_d1 unfolding ps2_P.d1_def by auto

lemma ps_P_d2:
  "ps_P.d2 = K"
  unfolding ps_P.d2_def ps_P.dims2_def ps2_P.nths_vars2' using ps2_P_d2 unfolding ps2_P.d2_def by auto

lemma nths_uminus_vars1:
  "nths dims (- vars1) = nths dims vars2"
  using ps2_P.nths_vars2' unfolding ps2_P_dims0 ps2_P_vars1' ps2_P.dims2_def by auto

lemma tensor_P_mult:
  assumes "m1 ∈ carrier_mat (2^n) (2^n)"
    and "m2 ∈ carrier_mat (2^n) (2^n)"
    and "m3 ∈ carrier_mat K K"
    and "m4 ∈ carrier_mat K K"
  shows "(tensor_P m1 m3) * (tensor_P m2 m4) = tensor_P (m1 * m2) (m3 * m4)"
proof -
  have eq:"{0..<n} = {..<n}" by auto
  have "(nths dims vars1) = replicate n 2"
    unfolding dims_def vars1_def apply (subst eq)
    by (simp add: nths_upt_eq_take[of "(replicate n 2 @ [K])" n]) 

  have "ps2_P.d1 = 2^n" unfolding ps2_P.d1_def ps2_P.dims1_def using d_vars1 N_def by auto
  moreover have "ps2_P.d2 = K" unfolding ps2_P.d2_def ps2_P.dims2_def using dims_vars2 by auto

  ultimately show ?thesis apply (subst ps2_P.ptensor_mat_mult) using assms by auto
qed

lemma mat_ext_vars1:
  shows "mat_extension dims vars1 A = tensor_P A (1⇩m K)"
  unfolding Utrans_P_def ps2_P.ptensor_mat_def partial_state.mat_extension_def
    partial_state.d2_def partial_state.dims2_def ps2_P.nths_vars2'[simplified ps2_P_dims0 ps2_P_vars1'] 
  using ps2_P_d2 unfolding ps2_P.d2_def using ps2_P_dims0 ps2_P_vars1' by auto

lemma Utrans_P_is_tensor_P1:
  "Utrans_P vars1 A = Utrans (tensor_P A (1⇩m K))"
  unfolding Utrans_P_def ps2_P.ptensor_mat_def partial_state.mat_extension_def
    partial_state.d2_def partial_state.dims2_def ps2_P.nths_vars2'[simplified ps2_P_dims0 ps2_P_vars1'] 
  using ps2_P_d2 unfolding ps2_P.d2_def using ps2_P_dims0 ps2_P_vars1' by auto

lemma nths_dims_uminus_vars2:
  "nths dims (-vars2) = nths dims vars1"
proof -
  have "nths dims (-vars2) = nths dims ({0..<length dims} - vars2)"
    using nths_minus_eq by auto
  also have "… = nths dims vars1" unfolding vars1_def vars2_def length_dims
    apply (subgoal_tac "{0..<n + 1} - {n} = {0..<n}") by auto
  finally show ?thesis by auto
qed

lemma mat_ext_vars2:
  assumes "A ∈ carrier_mat K K"
  shows "mat_extension dims vars2 A = tensor_P (1⇩m N) A"
proof -
  have "mat_extension dims vars2 A = tensor_mat dims vars2 A (1⇩m N)"
    unfolding Utrans_P_def partial_state.mat_extension_def
      partial_state.d2_def partial_state.dims2_def
      nths_dims_uminus_vars2 dims_vars1 N_def by auto
  also have "… = tensor_mat dims vars1 (1⇩m N) A" 
    apply (subst tensor_mat_comm[of vars1 vars2])
    subgoal unfolding vars1_def vars2_def by auto
    subgoal unfolding length_dims vars1_def vars2_def by auto
    subgoal unfolding dims_vars1 N_def by auto
    unfolding dims_vars2 using assms by auto
  finally show "mat_extension dims vars2 A = tensor_P (1⇩m N) A"
    unfolding ps2_P.ptensor_mat_def ps2_P_dims0 ps2_P_vars1' by auto
qed

lemma Utrans_P_is_tensor_P2:
  assumes "A ∈ carrier_mat K K"
  shows "Utrans_P vars2 A = Utrans (tensor_P (1⇩m N) A)"
  unfolding Utrans_P_def using mat_ext_vars2 assms by auto


subsection ‹Grover's algorithm›

text ‹Apply hadamard operator to first n variables›
definition hadamard_on_i :: "nat ⇒ complex mat" where
  "hadamard_on_i i = pmat_extension dims {i} (vars1 - {i}) hadamard"
declare hadamard_on_i_def [simp]

fun hadamard_n :: "nat ⇒ com" where
  "hadamard_n 0 = SKIP"
| "hadamard_n (Suc i) = hadamard_n i ;; Utrans (tensor_P (hadamard_on_i i) (1⇩m K))"

text ‹Body of the loop›
definition D :: com where
  "D = Utrans_P vars1 mat_O ;;
       hadamard_n n ;;
       Utrans_P vars1 mat_Ph ;;
       hadamard_n n ;;
       Utrans_P vars2 (mat_incr K)"

lemma unitary_ex_mat_O:
  "unitary (tensor_P mat_O (1⇩m K))"
  unfolding ps2_P.ptensor_mat_def
  apply (subst ps_P.tensor_mat_unitary)
  subgoal using ps_P_d1 mat_O_def by auto
  subgoal using ps_P_d2 by auto
  subgoal using unitary_mat_O by auto
  using unitary_one by auto

lemma unitary_ex_mat_Ph:
  "unitary (tensor_P mat_Ph (1⇩m K))"
  unfolding ps2_P.ptensor_mat_def
  apply (subst ps_P.tensor_mat_unitary)
  subgoal using ps_P_d1 mat_Ph_def by auto
  subgoal using ps_P_d2 by auto
  subgoal using unitary_mat_Ph by auto
  using unitary_one by auto

lemma unitary_hadamard_on_i:
  assumes "k < n"
  shows "unitary (hadamard_on_i k)"
proof -
  interpret st2: partial_state2 dims "{k}" "vars1 - {k}"
    apply unfold_locales by auto
  show ?thesis unfolding hadamard_on_i_def st2.pmat_extension_def st2.ptensor_mat_def
    apply (rule partial_state.tensor_mat_unitary)
    subgoal unfolding partial_state.d1_def partial_state.dims1_def st2.nths_vars1' st2.dims1_def
      using dims_nths_one_lt_n assms hadamard_dim by auto
    subgoal unfolding st2.d2_def st2.dims2_def partial_state.d2_def partial_state.dims2_def st2.nths_vars2' st2.dims1_def
      by auto
    subgoal using unitary_hadamard by auto
    subgoal using unitary_one by auto
    done
qed

lemma unitary_exhadamard_on_i:
  assumes "k < n"
  shows "unitary (tensor_P (hadamard_on_i k) (1⇩m K))"
proof -
  interpret st2: partial_state2 dims "{k}" "vars1 - {k}"
    apply unfold_locales by auto
  have d1: "st2.d0 = partial_state.d1 ps2_P.dims0 ps2_P.vars1'"
    unfolding partial_state.d1_def partial_state.dims1_def ps2_P.nths_vars1' ps2_P.dims1_def
      st2.d0_def st2.dims0_def st2.vars0_def using assms
    apply (subgoal_tac "{k} ∪ (vars1 - {k}) = vars1") apply simp
    unfolding vars1_def by auto
  show ?thesis
  unfolding ps2_P.ptensor_mat_def
  apply (rule partial_state.tensor_mat_unitary)
  subgoal unfolding hadamard_on_i_def st2.pmat_extension_def 
    using st2.ptensor_mat_carrier[of hadamard "1⇩m st2.d2"]
    using d1 by auto
  subgoal unfolding partial_state.d2_def partial_state.dims2_def ps2_P.nths_vars2' ps2_P.dims2_def dims_vars2 by auto
  using unitary_hadamard_on_i unitary_one assms by auto
qed

lemma hadamard_on_i_dim:
  assumes "k < n"
  shows "hadamard_on_i k ∈ carrier_mat N N"
proof -
  interpret st: partial_state2 dims "{k}" "(vars1 - {k})"
    apply unfold_locales by auto
  have vars1: "{k} ∪ (vars1 - {k}) = vars1" unfolding vars1_def using assms by auto
  show ?thesis unfolding hadamard_on_i_def N_def using st.pmat_extension_carrier unfolding st.d0_def st.dims0_def st.vars0_def
    using vars1 dims_vars1 by auto
qed

lemma well_com_hadamard_k:
  "k ≤ n ⟹ well_com (hadamard_n k)"
proof (induct k)
  case 0
  then show ?case by auto
next
  case (Suc n)
  then have "well_com (hadamard_n n)" by auto
  then show ?case unfolding hadamard_n.simps well_com.simps using tensor_P_dim unitary_exhadamard_on_i Suc by auto
qed

lemma well_com_hadamard_n:
  "well_com (hadamard_n n)"
  using well_com_hadamard_k by auto

lemma well_com_mat_O:
  "well_com (Utrans_P vars1 mat_O)"
  apply (subst Utrans_P_is_tensor_P1)
  apply simp using tensor_P_dim unitary_ex_mat_O by auto

lemma well_com_mat_Ph:
  "well_com (Utrans_P vars1 mat_Ph)"
  apply (subst Utrans_P_is_tensor_P1)
  apply simp using tensor_P_dim unitary_ex_mat_Ph by auto

lemma unitary_exmat_incr:
  "unitary (tensor_P (1⇩m N) (mat_incr K))"
  unfolding ps2_P.ptensor_mat_def
  apply (subst ps_P.tensor_mat_unitary)
  using  unitary_mat_incr K unitary_one by (auto simp add: ps_P_d1 ps_P_d2 mat_incr_def)

lemma well_com_mat_incr:
  "well_com (Utrans_P vars2 (mat_incr K))"
  apply (subst Utrans_P_is_tensor_P2)
  apply (simp add: mat_incr_def) using tensor_P_dim unitary_exmat_incr by auto

lemma well_com_D: "well_com D"
  unfolding D_def apply auto
  using well_com_hadamard_n well_com_mat_incr well_com_mat_O well_com_mat_Ph 
  by auto

text ‹Test at while loop›

definition M0 :: "complex mat" where
  "M0 = mat K K (λ(i,j). if i = j ∧ i ≥ R then 1 else 0)"

lemma hermitian_M0:
  "hermitian M0"
  by (auto simp add: hermitian_def M0_def adjoint_eval)

lemma M0_dim:
  "M0 ∈ carrier_mat K K"
  unfolding M0_def by auto

lemma M0_mult_M0:
  "M0 * M0 = M0"
  by (auto simp add: M0_def scalar_prod_def sum_only_one_neq_0)

definition M1 :: "complex mat" where
  "M1 = mat K K (λ(i,j). if i = j ∧ i < R then 1 else 0)"

lemma M1_dim:
  "M1 ∈ carrier_mat K K"
  unfolding M1_def by auto

lemma hermitian_M1:
  "hermitian M1"
  by (auto simp add: hermitian_def M1_def adjoint_eval)

lemma M1_mult_M1:
  "M1 * M1 = M1"
  by (auto simp add: M1_def scalar_prod_def sum_only_one_neq_0)

lemma M1_add_M0:
  "M1 + M0 = 1⇩m K"
  unfolding M0_def M1_def by auto

text ‹Test at the end›

definition testN :: "nat ⇒ complex mat" where
  "testN k = mat N N (λ(i,j). if i = k ∧ j = k then 1 else 0)"

lemma hermitian_testN:
  "hermitian (testN k)"
  unfolding hermitian_def testN_def
  by (auto simp add: scalar_prod_def adjoint_eval)

lemma testN_mult_testN:
  "testN k * testN k = testN k"
  unfolding testN_def
  by (auto simp add: scalar_prod_def sum_only_one_neq_0)

lemma testN_dim:
  "testN k ∈ carrier_mat N N"
  unfolding testN_def by auto

definition test_fst_k :: "nat ⇒ complex mat" where
  "test_fst_k k = mat N N (λ(i, j). if (i = j ∧ i < k) then 1 else 0)"

lemma sum_test_k:
  assumes "m ≤ N"
  shows "matrix_sum N (λk. testN k) m = test_fst_k m"
proof -
  have "m ≤ N ⟹ matrix_sum N (λk. testN k) m = mat N N (λ(i, j). if (i = j ∧ i < m) then 1 else 0)" for m
  proof (induct m)
    case 0
    then show ?case apply simp apply (rule eq_matI) by auto
  next
    case (Suc m)
    then have m: "m < N" by auto
    then have m': "m ≤ N" by auto
    have "matrix_sum N testN (Suc m) = testN m + matrix_sum N testN m" by simp
    also have "… = mat N N (λ(i, j). if (i = j ∧ i < (Suc m)) then 1 else 0)"
      unfolding testN_def Suc(1)[OF m'] apply (rule eq_matI) by auto
    finally show ?case by auto
  qed
  then show ?thesis unfolding test_fst_k_def using assms by auto
qed

lemma test_fst_kN:
  "test_fst_k N = 1⇩m N"
  apply (rule eq_matI)
  unfolding test_fst_k_def by auto

lemma matrix_sum_tensor_P1:
  "(⋀k. k < m ⟹ g k ∈ carrier_mat N N) ⟹ (A ∈ carrier_mat K K) ⟹
   matrix_sum d (λk. tensor_P (g k) A) m = tensor_P (matrix_sum N g m) A"
proof (induct m)
  case 0
  show ?case apply (simp) unfolding ps2_P.ptensor_mat_def 
    using ps_P.tensor_mat_zero1[simplified ps_P_d ps_P_d1, of A] by auto
next
  case (Suc m)
  then have ind: "matrix_sum d (λk. tensor_P (g k) A) m = tensor_P (matrix_sum N g m) A" 
    and dk: "⋀k. k < m ⟹ g k ∈ carrier_mat N N" and "A ∈ carrier_mat K K" by auto
  have ds: "matrix_sum N g m ∈ carrier_mat N N" apply (subst matrix_sum_dim)
    using dk by auto
  show ?case apply simp
    apply (subst ind)
    unfolding ps2_P.ptensor_mat_def apply (subst ps_P.tensor_mat_add1)
    unfolding ps_P_d1 ps_P_d2 using Suc ds by auto
qed

text ‹Grover's algorithm. Assume we start in the zero state›
definition Grover :: com where
  "Grover = hadamard_n n ;;
            While_P vars2 M0 M1 D ;;
            Measure_P vars1 N testN (replicate N SKIP)"

lemma well_com_if:
  "well_com (Measure_P vars1 N testN (replicate N SKIP))"
  unfolding Measure_P_def apply auto
proof -
  have eq0: "⋀n. mat_extension dims vars1 (testN n) = tensor_P (testN n) (1⇩m K)"
    unfolding mat_ext_vars1 by auto 
  have eq1: "adjoint (tensor_P (testN j) (1⇩m K)) * tensor_P (testN j) (1⇩m K) = tensor_P (testN j) (1⇩m K)" for j
    unfolding ps2_P.ptensor_mat_def
    apply (subst ps_P.tensor_mat_adjoint)
      apply (auto simp add: ps_P_d1 ps_P_d2 testN_dim hermitian_testN[unfolded hermitian_def] hermitian_one[unfolded hermitian_def])
    apply (subst ps_P.tensor_mat_mult[symmetric])
    by (auto simp add: ps_P_d1 ps_P_d2 testN_dim testN_mult_testN)
  have "measurement d N (λn. tensor_P (testN n) (1⇩m K))"
    unfolding measurement_def
    apply (simp add: tensor_P_dim)
    apply (subst eq1)
    apply (subst matrix_sum_tensor_P1)
      apply (auto simp add: testN_dim)
    apply (subst sum_test_k, simp)
    apply (subst test_fst_kN)
    unfolding ps2_P.ptensor_mat_def
    using ps_P.tensor_mat_id ps_P_d ps_P_d1 ps_P_d2 by auto
  then show "measurement d N (λn. mat_extension dims vars1 (testN n))" using eq0 by auto

  show "list_all well_com (replicate N SKIP)" 
    apply (subst list_all_length) by simp
qed

lemma well_com_while:
  "well_com (While_P vars2 M0 M1 D)"
  unfolding While_P_def apply auto
   apply (subst (1 2) mat_ext_vars2)
  apply (auto simp add: M1_dim M0_dim)
proof -
  have 2: "2 = Suc (Suc 0)" by auto
  have ad0: "adjoint (tensor_P (1⇩m N) M0) = (tensor_P (1⇩m N) M0)"
    unfolding ps2_P.ptensor_mat_def apply (subst ps_P.tensor_mat_adjoint)
    unfolding ps_P_d1 ps_P_d2 by (auto simp add: M0_dim adjoint_one hermitian_M0[unfolded hermitian_def])
  have ad1: "adjoint (tensor_P (1⇩m N) M1) = (tensor_P (1⇩m N) M1)"
    unfolding ps2_P.ptensor_mat_def apply (subst ps_P.tensor_mat_adjoint)
    unfolding ps_P_d1 ps_P_d2 by (auto simp add: M1_dim adjoint_one hermitian_M1[unfolded hermitian_def])
  have m0: "tensor_P (1⇩m N) M0 * tensor_P (1⇩m N) M0 = tensor_P (1⇩m N) M0"
    unfolding ps2_P.ptensor_mat_def apply (subst ps_P.tensor_mat_mult[symmetric])
    unfolding ps_P_d1 ps_P_d2 using M0_dim M0_mult_M0 by auto
  have m1: "tensor_P (1⇩m N) M1 * tensor_P (1⇩m N) M1 = tensor_P (1⇩m N) M1"
    unfolding ps2_P.ptensor_mat_def apply (subst ps_P.tensor_mat_mult[symmetric])
    unfolding ps_P_d1 ps_P_d2 using M1_dim M1_mult_M1 by auto
  have s: "tensor_P (1⇩m N) M1 + tensor_P (1⇩m N) M0 = 1⇩m d"
    unfolding ps2_P.ptensor_mat_def apply (subst ps_P.tensor_mat_add2[symmetric])
    unfolding ps_P_d1 ps_P_d2 
    by (auto simp add: M1_dim M0_dim M1_add_M0 ps_P.tensor_mat_id[simplified ps_P_d1 ps_P_d2 ps_P_d])
  show "measurement d 2 (λn. if n = 0 then tensor_P (1⇩m N) M0 else if n = 1 then tensor_P (1⇩m N) M1 else undefined)"
    unfolding measurement_def apply (auto simp add: tensor_P_dim) apply (subst 2)
    apply (simp add: ad0 ad1 m0 m1)
    apply (subst assoc_add_mat[symmetric, of _ d d]) using tensor_P_dim s by auto
  show "well_com D" using well_com_D by auto
qed

lemma well_com_Grover:
  "well_com Grover"
  unfolding Grover_def apply auto
  using well_com_hadamard_n well_com_if well_com_while by auto

subsection ‹Correctness›

text ‹Pre-condition: assume in the zero state›

definition ket_pre :: "complex vec" where
  "ket_pre = Matrix.vec N (λk. if k = 0 then 1 else 0)"

lemma ket_pre_dim:
  "ket_pre ∈ carrier_vec N" using ket_pre_def by auto

definition pre :: "complex mat" where
  "pre = proj ket_pre"

lemma pre_dim:
  "pre ∈ carrier_mat N N"
  using pre_def ket_pre_def by auto

lemma norm_pre:
  "inner_prod ket_pre ket_pre = 1"
  unfolding ket_pre_def scalar_prod_def
  using sum_only_one_neq_0[of "{0..<N}" 0 "λi. (if i = 0 then 1 else 0) * cnj (if i = 0 then 1 else 0)"] by auto

lemma pre_trace:
  "trace pre = 1"
  unfolding pre_def
  apply (subst trace_outer_prod[of _ N])
  subgoal unfolding ket_pre_def by auto using norm_pre by auto

lemma positive_pre:
  "positive pre"
  using positive_same_outer_prod unfolding pre_def ket_pre_def by auto

lemma pre_le_one:
  "pre ≤⇩L 1⇩m N"
  unfolding pre_def using outer_prod_le_one norm_pre ket_pre_def by auto

text ‹Post-condition: should be in a state i with f i = 1›

definition post :: "complex mat" where
  "post = mat N N (λ(i, j). if (i = j ∧ f i) then 1 else 0)"

lemma post_dim:
  "post ∈ carrier_mat N N"
  unfolding post_def by auto

lemma hermitian_post:
  "hermitian post"
  unfolding hermitian_def post_def
  by (auto simp add: adjoint_eval)

text ‹Hoare triples of initialization›

definition ket_zero :: "complex vec" where
  "ket_zero = Matrix.vec 2 (λk. if k = 0 then 1 else 0)"

lemma ket_zero_dim:
  "ket_zero ∈ carrier_vec 2" unfolding ket_zero_def by auto

definition proj_zero where
  "proj_zero = proj ket_zero"

definition ket_one where
  "ket_one = Matrix.vec 2 (λk. if k = 1 then 1 else 0)"

definition proj_one where
  "proj_one = proj ket_one"

definition ket_plus where
  "ket_plus = Matrix.vec 2 (λk.1 / csqrt 2) "

lemma ket_plus_dim:
  "ket_plus ∈ carrier_vec 2" unfolding ket_plus_def by auto

lemma ket_plus_eval [simp]:
  "i < 2 ⟹ ket_plus $ i = 1 / csqrt 2"
  apply (simp only: ket_plus_def)
  using index_vec less_2_cases by force

lemma csqrt_2_sq [simp]:
  "complex_of_real (sqrt 2) * complex_of_real (sqrt 2) = 2"
  by (smt of_real_add of_real_hom.hom_one of_real_power one_add_one power2_eq_square real_sqrt_pow2)

lemma ket_plus_tensor_n:
  "partial_state.tensor_vec [2, 2] {0} ket_plus ket_plus = Matrix.vec 4 (λk. 1 / 2)"
  unfolding partial_state.tensor_vec_def state_sig.d_def
proof (rule eq_vecI, auto)
  fix i :: nat assume i: "i < 4"
  interpret st: partial_state "[2, 2]" "{0}" .
  have d1_eq: "st.d1 = 2"
    by (simp add: st.d1_def st.dims1_def nths_def)
  have "st.encode1 i < st.d1"
    by (simp add: st.d_def i)
  then have i1_lt: "st.encode1 i < 2"
    using d1_eq by auto
  have d2_eq: "st.d2 = 2"
    by (simp add: st.d2_def st.dims2_def nths_def)
  have "st.encode2 i < st.d2"
    by (simp add: st.d_def i)
  then have i2_lt: "st.encode2 i < 2"
    using d2_eq by auto
  show "ket_plus $ st.encode1 i * ket_plus $ st.encode2 i * 2 = 1"
    by (auto simp add: i1_lt i2_lt)
qed

definition proj_plus where
  "proj_plus = proj ket_plus"

lemma hadamard_on_zero:
  "hadamard *⇩v ket_zero = ket_plus"
  unfolding hadamard_def ket_zero_def ket_plus_def mat_of_rows_list_def  
  apply (rule eq_vecI, auto simp add: scalar_prod_def)
  subgoal for i
    apply (drule less_2_cases)
    apply (drule disjE, auto)
    by (subst sum_le_2, auto)+.

fun exH_k :: "nat ⇒ complex mat" where
  "exH_k 0 = hadamard_on_i 0"
| "exH_k (Suc k) = exH_k k * hadamard_on_i (Suc k)"

fun H_k :: "nat ⇒ complex mat" where
  "H_k 0 = hadamard"
| "H_k (Suc k) = ptensor_mat dims {0..<Suc k} {Suc k} (H_k k) hadamard"

lemma H_k_dim:
  "k < n ⟹ H_k k ∈ carrier_mat (2^(Suc k)) (2^(Suc k))"
proof (induct k)
  case 0
  then show ?case using hadamard_dim by auto
next
  case (Suc k)
  interpret st: partial_state2 dims "{0..<(Suc k)}" "{Suc k}"
    apply unfold_locales by auto
  have "Suc (Suc k) ≤ n" using Suc by auto
  then have "nths dims ({0..<Suc (Suc k)}) = replicate (Suc (Suc k)) 2" using dims_nths_le_n by auto
  moreover have "prod_list (replicate l 2) = 2^l" for l by simp
  moreover have "{0..<Suc k} ∪ {Suc k} = {0..<(Suc (Suc k))}" by auto
  ultimately have plssk: "prod_list (nths dims ({0..<Suc k} ∪ {Suc k})) = 2^(Suc (Suc k))" by auto
  have "dim_col (H_k (Suc k)) = 2^(Suc (Suc k))" using st.ptensor_mat_dim_col unfolding st.d0_def st.dims0_def st.vars0_def using plssk by auto
  moreover have "dim_row (H_k (Suc k)) = 2^(Suc (Suc k))" using st.ptensor_mat_dim_row unfolding st.d0_def st.dims0_def st.vars0_def using plssk by auto
  ultimately show ?case by auto
qed

lemma exH_k_eq_H_k:
  "k < n ⟹ exH_k k = pmat_extension dims {0..<(Suc k)} {(Suc k)..<n} (H_k k)"
proof(induct k)
  case 0
  have "{(Suc 0)..<n} = vars1 - {0..<(Suc 0)}" using vars1_def by fastforce
  then show ?case unfolding exH_k.simps using vars1_def by auto
next
  case (Suc k)
  interpret st: partial_state2 dims "{0..<Suc k}" "{(Suc k)..<n}"
    apply unfold_locales by auto
  interpret st1: partial_state2 dims "{Suc k}" "{(Suc (Suc k))..<n}"
    apply unfold_locales by auto
  interpret st2: partial_state2 dims "{Suc k}" "vars1 - {Suc k}"
    apply unfold_locales by auto
  interpret st3: partial_state2 dims "{0..<Suc k}" "{Suc (Suc k)..<n}"
    apply unfold_locales by auto
  interpret st4: partial_state2 dims "{0..<Suc (Suc k)}" "{Suc (Suc k)..<n}"
    apply unfold_locales by auto

  from Suc have eq0: "exH_k (Suc k) 
    = (st.pmat_extension (H_k k)) * (st2.pmat_extension hadamard)" by auto
  have "vars1 - {0..<Suc k} = {(Suc k)..<n}" using vars1_def by auto

  then have eql1: "st.pmat_extension (H_k k) = st.ptensor_mat (H_k k) (1⇩m st.d2)"
    using st.pmat_extension_def by auto

  from dims_nths_one_lt_n[OF Suc(2)] have st1d1: "st1.d1 = 2" unfolding st1.d1_def st1.dims1_def by fastforce
  have "{Suc k} ∪ {Suc (Suc k)..<n} = {Suc k..<n}" using Suc by auto
  then have "st1.d0 = st.d2" unfolding st1.d0_def st1.dims0_def st1.vars0_def st.d2_def st.dims2_def by fastforce
  then have eql2: "st1.ptensor_mat (1⇩m 2) (1⇩m st1.d2) = 1⇩m st.d2"
    using st1.ptensor_mat_id st1d1 by auto
  have eql3: "st.ptensor_mat (H_k k) (1⇩m st.d2) = st.ptensor_mat (H_k k) (st1.ptensor_mat (1⇩m 2) (1⇩m st1.d2))"
    apply (subst eql2[symmetric]) by auto

  have eqr1: "(st2.pmat_extension hadamard) = st2.ptensor_mat hadamard (1⇩m st2.d2)" using st2.pmat_extension_def by auto
  have splitset: "{0..<Suc k} ∪ {Suc (Suc k)..<n} = vars1 - {Suc k}" unfolding vars1_def using Suc(2) by auto

  have Sksplit: "{Suc k} ∪ {Suc (Suc k)..<n} = {Suc k..<n}" using Suc(2) by auto
  have Sksplit1: "{0..<Suc k}∪{Suc k} = {0..<Suc (Suc k)}" by auto
  have "st.ptensor_mat (H_k k) (st1.ptensor_mat (1⇩m 2) (1⇩m st1.d2)) 
    = ptensor_mat dims ({0..<Suc k}∪{Suc k}) {Suc (Suc k)..<n} (ptensor_mat dims {0..<Suc k} {Suc k} (H_k k) (1⇩m 2)) (1⇩m st1.d2)"
    apply (subst ptensor_mat_assoc[symmetric, of "{0..<Suc k}" "{Suc k}" "{Suc (Suc k)..<n}" "H_k k" "1⇩m 2" "1⇩m st1.d2", simplified Sksplit])
    using Suc length_dims by auto
  also have "… = ptensor_mat dims ({0..<Suc k}∪{Suc k}) {Suc (Suc k)..<n} (ptensor_mat dims {Suc k} {0..<Suc k} (1⇩m 2) (H_k k)) (1⇩m st1.d2)"
    using ptensor_mat_comm[of "{0..<Suc k}" "{Suc k}"] by auto
  also have "… = ptensor_mat dims {Suc k} ({0..<Suc k} ∪ {Suc (Suc k)..<n})
                  (1⇩m 2) 
                  (ptensor_mat dims {0..<Suc k} {Suc (Suc k)..<n} (H_k k) (1⇩m st1.d2))"
    apply (subst sup_commute)
    apply (subst ptensor_mat_assoc[of "{Suc k}" "{0..<Suc k}" "{Suc (Suc k)..<n}" "(1⇩m 2)" "H_k k" "1⇩m st1.d2"])
    using Suc length_dims by auto
  finally have eql4: "st.pmat_extension (H_k k) 
    = st2.ptensor_mat (1⇩m 2) (st3.ptensor_mat (H_k k) (1⇩m st3.d2))" using eql1 eql3 splitset by auto

  have "st2.ptensor_mat (1⇩m 2) (st3.ptensor_mat (H_k k) (1⇩m st3.d2)) * st2.ptensor_mat hadamard (1⇩m st2.d2)
        = st2.ptensor_mat ((1⇩m 2)*hadamard) ((st3.ptensor_mat (H_k k) (1⇩m st3.d2))*(1⇩m st2.d2))"
    apply (rule st2.ptensor_mat_mult[symmetric, of "1⇩m 2" "hadamard" "(st3.ptensor_mat (H_k k) (1⇩m st3.d2))" "(1⇩m st2.d2)"])
    subgoal unfolding st2.d1_def st2.dims1_def
      by (simp add: dims_nths_one_lt_n Suc(2))
    subgoal unfolding st2.d1_def st2.dims1_def
      apply (simp add: dims_nths_one_lt_n Suc(2)) using hadamard_dim by auto
    subgoal unfolding st2.d2_def[unfolded st2.dims2_def]
      using st3.ptensor_mat_dim_col[unfolded st3.d0_def st3.dims0_def st3.vars0_def, simplified splitset]
        st3.ptensor_mat_dim_row[unfolded st3.d0_def st3.dims0_def st3.vars0_def, simplified splitset] by auto
    by auto
  also have "… = st2.ptensor_mat (hadamard) (st3.ptensor_mat (H_k k) (1⇩m st3.d2))"
    unfolding st2.d2_def[unfolded st2.dims2_def]
    using hadamard_dim st3.ptensor_mat_dim_col[unfolded st3.d0_def st3.dims0_def st3.vars0_def, simplified splitset]
        st3.ptensor_mat_dim_row[unfolded st3.d0_def st3.dims0_def st3.vars0_def, simplified splitset] by auto
  also have "… = ptensor_mat dims ({0..<Suc k}∪{Suc k}) {Suc (Suc k)..<n} (ptensor_mat dims {Suc k} {0..<Suc k} hadamard (H_k k)) (1⇩m st3.d2)"
    apply (subst ptensor_mat_assoc[symmetric, of "{Suc k}" "{0..<Suc k}" "{Suc (Suc k)..<n}" "hadamard" "H_k k" "1⇩m st3.d2", simplified splitset]) 
    using Suc length_dims by auto
  also have "… = ptensor_mat dims ({0..<Suc k}∪{Suc k}) {Suc (Suc k)..<n} (H_k (Suc k)) (1⇩m st3.d2)"
    using ptensor_mat_comm[of "{Suc k}"] Sksplit1 by auto
  also have "… = ptensor_mat dims ({0..<Suc (Suc k)}) {Suc (Suc k)..<n} (H_k (Suc k)) (1⇩m st3.d2)" using Sksplit1 by auto
  also have "… = pmat_extension dims {0..<Suc (Suc k)} {Suc (Suc k)..<n} (H_k (Suc k))" 
    unfolding st4.pmat_extension_def by auto
  finally show ?case using eq0 eql4 eqr1 by auto
qed

lemma mult_exH_k_left:
  assumes "Suc k < n"
  shows "hadamard_on_i (Suc k) * exH_k k = exH_k (Suc k)"
proof -
  interpret st: partial_state2 dims "{0..<Suc k}" "{(Suc k)..<n}"
    apply unfold_locales by auto
  interpret st1: partial_state2 dims "{Suc k}" "{(Suc (Suc k))..<n}"
    apply unfold_locales by auto
  interpret st2: partial_state2 dims "{Suc k}" "vars1 - {Suc k}"
    apply unfold_locales by auto
  interpret st3: partial_state2 dims "{0..<Suc k}" "{Suc (Suc k)..<n}"
    apply unfold_locales by auto
  interpret st4: partial_state2 dims "{0..<Suc (Suc k)}" "{Suc (Suc k)..<n}"
    apply unfold_locales by auto

  from exH_k_eq_H_k assms have eq0: "exH_k (Suc k) 
    = (st.pmat_extension (H_k k)) * (st2.pmat_extension hadamard)" by auto
  have "vars1 - {0..<Suc k} = {(Suc k)..<n}" using vars1_def by auto

  then have eql1: "st.pmat_extension (H_k k) = st.ptensor_mat (H_k k) (1⇩m st.d2)"
    using st.pmat_extension_def by auto

  from dims_nths_one_lt_n[OF assms] have st1d1: "st1.d1 = 2" unfolding st1.d1_def st1.dims1_def by fastforce
  have "{Suc k} ∪ {Suc (Suc k)..<n} = {Suc k..<n}" using assms by auto
  then have "st1.d0 = st.d2" unfolding st1.d0_def st1.dims0_def st1.vars0_def st.d2_def st.dims2_def by fastforce
  then have eql2: "st1.ptensor_mat (1⇩m 2) (1⇩m st1.d2) = 1⇩m st.d2"
    using st1.ptensor_mat_id st1d1 by auto
  have eql3: "st.ptensor_mat (H_k k) (1⇩m st.d2) = st.ptensor_mat (H_k k) (st1.ptensor_mat (1⇩m 2) (1⇩m st1.d2))"
    apply (subst eql2[symmetric]) by auto

  have eqr1: "(st2.pmat_extension hadamard) = st2.ptensor_mat hadamard (1⇩m st2.d2)" using st2.pmat_extension_def by auto
  have splitset: "{0..<Suc k} ∪ {Suc (Suc k)..<n} = vars1 - {Suc k}" unfolding vars1_def using assms by auto

  have Sksplit: "{Suc k} ∪ {Suc (Suc k)..<n} = {Suc k..<n}" using assms by auto
  have Sksplit1: "{0..<Suc k}∪{Suc k} = {0..<Suc (Suc k)}" by auto
  have "st.ptensor_mat (H_k k) (st1.ptensor_mat (1⇩m 2) (1⇩m st1.d2)) 
    = ptensor_mat dims ({0..<Suc k}∪{Suc k}) {Suc (Suc k)..<n} (ptensor_mat dims {0..<Suc k} {Suc k} (H_k k) (1⇩m 2)) (1⇩m st1.d2)"
    apply (subst ptensor_mat_assoc[symmetric, of "{0..<Suc k}" "{Suc k}" "{Suc (Suc k)..<n}" "H_k k" "1⇩m 2" "1⇩m st1.d2", simplified Sksplit])
    using assms length_dims by auto
  also have "… = ptensor_mat dims ({0..<Suc k}∪{Suc k}) {Suc (Suc k)..<n} (ptensor_mat dims {Suc k} {0..<Suc k} (1⇩m 2) (H_k k)) (1⇩m st1.d2)"
    using ptensor_mat_comm[of "{0..<Suc k}" "{Suc k}"] by auto
  also have "… = ptensor_mat dims {Suc k} ({0..<Suc k} ∪ {Suc (Suc k)..<n})
                  (1⇩m 2) 
                  (ptensor_mat dims {0..<Suc k} {Suc (Suc k)..<n} (H_k k) (1⇩m st1.d2))"
    apply (subst sup_commute)
    apply (subst ptensor_mat_assoc[of "{Suc k}" "{0..<Suc k}" "{Suc (Suc k)..<n}" "(1⇩m 2)" "H_k k" "1⇩m st1.d2"]) using assms length_dims by auto
  finally have "st.pmat_extension (H_k k) 
    = st2.ptensor_mat (1⇩m 2) (st3.ptensor_mat (H_k k) (1⇩m st3.d2))" using eql1 eql3 splitset by auto
  moreover have "st.pmat_extension (H_k k) = exH_k k" using exH_k_eq_H_k assms by auto
  ultimately have eql4: "exH_k k = st2.ptensor_mat (1⇩m 2) (st3.ptensor_mat (H_k k) (1⇩m st3.d2))" by auto

  have "st2.ptensor_mat hadamard (1⇩m st2.d2) * st2.ptensor_mat (1⇩m 2) (st3.ptensor_mat (H_k k) (1⇩m st3.d2))
        = st2.ptensor_mat (hadamard*(1⇩m 2)) ((1⇩m st2.d2)* (st3.ptensor_mat (H_k k) (1⇩m st3.d2)))"
    apply (rule st2.ptensor_mat_mult[symmetric, of "hadamard" "1⇩m 2" "(1⇩m st2.d2)" "(st3.ptensor_mat (H_k k) (1⇩m st3.d2))"])
    subgoal unfolding st2.d1_def st2.dims1_def apply (simp add: dims_nths_one_lt_n assms) using hadamard_dim by auto
    subgoal unfolding st2.d1_def st2.dims1_def by (simp add: dims_nths_one_lt_n assms) 
    subgoal by auto
    subgoal unfolding st2.d2_def[unfolded st2.dims2_def] using st3.ptensor_mat_dim_col[unfolded st3.d0_def st3.dims0_def st3.vars0_def, simplified splitset]
        st3.ptensor_mat_dim_row[unfolded st3.d0_def st3.dims0_def st3.vars0_def, simplified splitset] by auto
    done
  also have "… = st2.ptensor_mat (hadamard) (st3.ptensor_mat (H_k k) (1⇩m st3.d2))"
    unfolding st2.d2_def[unfolded st2.dims2_def]
    using hadamard_dim st3.ptensor_mat_dim_col[unfolded st3.d0_def st3.dims0_def st3.vars0_def, simplified splitset]
        st3.ptensor_mat_dim_row[unfolded st3.d0_def st3.dims0_def st3.vars0_def, simplified splitset] by auto
  also have "… = ptensor_mat dims ({0..<Suc k}∪{Suc k}) {Suc (Suc k)..<n} (ptensor_mat dims {Suc k} {0..<Suc k} hadamard (H_k k)) (1⇩m st3.d2)"
    apply (subst ptensor_mat_assoc[symmetric, of "{Suc k}" "{0..<Suc k}" "{Suc (Suc k)..<n}" "hadamard" "H_k k" "1⇩m st3.d2", simplified splitset]) 
    using assms length_dims by auto
  also have "… = ptensor_mat dims ({0..<Suc k}∪{Suc k}) {Suc (Suc k)..<n} (H_k (Suc k)) (1⇩m st3.d2)"
    using ptensor_mat_comm[of "{Suc k}"] Sksplit1 by auto
  also have "… = ptensor_mat dims ({0..<Suc (Suc k)}) {Suc (Suc k)..<n} (H_k (Suc k)) (1⇩m st3.d2)" using Sksplit1 by auto
  also have "… = pmat_extension dims {0..<Suc (Suc k)} {Suc (Suc k)..<n} (H_k (Suc k))" 
    unfolding st4.pmat_extension_def by auto
  also have "… = exH_k (Suc k)" using exH_k_eq_H_k[of "Suc k"] assms by auto
  finally have "st2.ptensor_mat hadamard (1⇩m st2.d2) * st2.ptensor_mat (1⇩m 2) (st3.ptensor_mat (H_k k) (1⇩m st3.d2)) 
    =exH_k (Suc k)".
  then show ?thesis unfolding hadamard_on_i_def
    using eql4 eqr1 by auto 
qed

lemma exH_eq_H:
  "exH_k (n - 1) = H_k (n - 1)"
proof -
  have "∃m. n = Suc (Suc m)" using n by presburger
  then obtain m where m: "n = Suc (Suc m)" using n by auto
  then have "exH_k m = pmat_extension dims {0..<(Suc m)} {(Suc m)..<n} (H_k m)" using exH_k_eq_H_k by auto
  then have "exH_k (Suc m) = pmat_extension dims {0..<(Suc m)} {(Suc m)..<n} (H_k m) 
                            * (pmat_extension dims {Suc m} (vars1 - {Suc m}) hadamard)" by auto
  moreover have "{(Suc m)..<n} = {Suc m}" using m by auto
  moreover have "vars1 - {Suc m} = {0..<Suc m}" unfolding vars1_def using m by auto
  ultimately have eqSm: "exH_k (Suc m) = pmat_extension dims {0..<(Suc m)} {Suc m} (H_k m) 
                            * (pmat_extension dims {Suc m} {0..<Suc m} hadamard)" by auto

  interpret stm1: partial_state2 dims "{Suc m}" "{0..<Suc m}" 
    apply unfold_locales by auto
  interpret stm2: partial_state2 dims "{0..<Suc m}" "{Suc m}"
    apply unfold_locales by auto
  have "nths dims {0..<Suc m} = replicate (Suc m) 2" using dims_nths_le_n m by auto
  then have stm2d1: "stm2.d1 = 2^(Suc m)" unfolding stm2.d1_def stm2.dims1_def by auto
  have stm2d2: "stm2.d2 = 2" unfolding stm2.d2_def stm2.dims2_def using dims_nths_one_lt_n m by auto

  have "m < n" using m by auto
  then have "H_k m ∈ carrier_mat (2^(Suc m)) (2^(Suc m))" using H_k_dim by auto
  then have Hkm1: "(H_k m) * (1⇩m stm2.d1) = (H_k m)" unfolding stm2d1 by auto

  have eqd12: "stm1.d2 = stm2.d1" unfolding stm1.d2_def stm1.dims2_def stm2.d1_def stm2.dims1_def by auto
  have "pmat_extension dims {Suc m} {0..<Suc m} hadamard = stm1.ptensor_mat hadamard (1⇩m stm1.d2)" using stm1.pmat_extension_def by auto
  also have "… = stm2.ptensor_mat (1⇩m stm2.d1) hadamard" using ptensor_mat_comm eqd12 by auto
  finally have eqr: "(pmat_extension dims {Suc m} {0..<Suc m} hadamard) = stm2.ptensor_mat (1⇩m stm2.d1) hadamard".
  then have "exH_k (Suc m) = stm2.ptensor_mat (H_k m) (1⇩m stm2.d2) * stm2.ptensor_mat (1⇩m stm2.d1) hadamard" 
    using eqSm unfolding stm2.pmat_extension_def by auto
  also have "… = stm2.ptensor_mat ((H_k m) * (1⇩m stm2.d1)) (1⇩m stm2.d2 * hadamard)" 
    apply (rule stm2.ptensor_mat_mult[symmetric, of "H_k m" "1⇩m stm2.d1" "1⇩m stm2.d2" "hadamard"])
    unfolding stm2d1 stm2d2 using H_k_dim m hadamard_dim by auto
  also have "… = stm2.ptensor_mat (H_k m) (hadamard)" using H_k_dim hadamard_dim stm2d1 stm2d2 Hkm1 by auto
  also have "… = H_k (Suc m)" unfolding stm2.ptensor_mat_def H_k.simps by auto
  finally have  "exH_k (Suc m) = H_k (Suc m)" by auto
  moreover have "Suc m = n - 1" using m by auto
  ultimately show ?thesis by auto
qed

fun ket_zero_k :: "nat ⇒ complex vec" where
  "ket_zero_k 0 = ket_zero"
| "ket_zero_k (Suc k) = ptensor_vec dims {0..<(Suc k)} {Suc k} (ket_zero_k k) ket_zero"

lemma ket_zero_k_dim:
  assumes "k < n"
  shows "ket_zero_k k ∈ carrier_vec (2^(Suc k))"
proof (cases k)
  case 0
  show ?thesis using ket_zero_dim 0 by auto
next
  case (Suc k)
  interpret st: partial_state2 dims "{0..<(Suc k)}" "{Suc k}"
    apply unfold_locales by auto
  have "Suc (Suc k) ≤ n" using assms Suc by auto
  then have "nths dims ({0..<Suc (Suc k)}) = replicate (Suc (Suc k)) 2" using dims_nths_le_n by auto
  moreover have "prod_list (replicate l 2) = 2^l" for l by simp
  moreover have "{0..<Suc k} ∪ {Suc k} = {0..<(Suc (Suc k))}" by auto
  ultimately have plssk: "prod_list (nths dims ({0..<Suc k} ∪ {Suc k})) = 2^(Suc (Suc k))" by auto
  show ?thesis apply (rule carrier_vecI) unfolding ket_zero_k.simps Suc
    using st.ptensor_vec_dim[of "ket_zero_k k" ket_zero] plssk unfolding st.d0_def st.dims0_def st.vars0_def by auto
qed

fun ket_plus_k where
  "ket_plus_k 0 = ket_plus"
| "ket_plus_k (Suc k) = ptensor_vec dims {0..<(Suc k)} {Suc k} (ket_plus_k k) ket_plus"

lemma ket_plus_k_dim:
  assumes "k < n"
  shows "ket_plus_k k ∈ carrier_vec (2^(Suc k))"
proof (cases k)
  case 0
  show ?thesis using ket_plus_dim 0 by auto
next
  case (Suc k)
  interpret st: partial_state2 dims "{0..<(Suc k)}" "{Suc k}"
    apply unfold_locales by auto
  have "Suc (Suc k) ≤ n" using assms Suc by auto
  then have "nths dims ({0..<Suc (Suc k)}) = replicate (Suc (Suc k)) 2" using dims_nths_le_n by auto
  moreover have "prod_list (replicate l 2) = 2^l" for l by simp
  moreover have "{0..<Suc k} ∪ {Suc k} = {0..<(Suc (Suc k))}" by auto
  ultimately have plssk: "prod_list (nths dims ({0..<Suc k} ∪ {Suc k})) = 2^(Suc (Suc k))" by auto
  show ?thesis apply (rule carrier_vecI) unfolding ket_zero_k.simps Suc
    using st.ptensor_vec_dim plssk unfolding st.d0_def st.dims0_def st.vars0_def by auto
qed


lemma H_k_ket_zero_k:
  "k < n ⟹ (H_k k) *⇩v (ket_zero_k k) = (ket_plus_k k)"
proof (induct k)
  case 0
  show ?case using hadamard_on_zero unfolding H_k.simps ket_zero_k.simps ket_plus_k.simps by auto
next
  case (Suc k)
  then have k: "k < n" by auto
  interpret st: partial_state2 dims "{0..<(Suc k)}" "{Suc k}"
    apply unfold_locales by auto
  have "nths dims {0..<Suc k} = replicate (Suc k) 2" using dims_nths_le_n Suc by auto
  then have std1: "st.d1 = 2^(Suc k)" unfolding st.d1_def st.dims1_def by auto
  have std2: "st.d2 = 2" unfolding st.d2_def st.dims2_def using dims_nths_one_lt_n Suc by auto
  have "H_k (Suc k) *⇩v ket_zero_k (Suc k) = st.ptensor_mat (H_k k) hadamard *⇩v st.ptensor_vec (ket_zero_k k) ket_zero" by auto
  also have "… = st.ptensor_vec ((H_k k) *⇩v (ket_zero_k k)) (hadamard *⇩v ket_zero)" 
    using st.ptensor_mat_mult_vec[unfolded std1 std2, OF H_k_dim[OF k] ket_zero_k_dim[OF k] hadamard_dim ket_zero_dim] by auto
  also have "… = st.ptensor_vec (ket_plus_k k) ket_plus" using Suc hadamard_on_zero by auto
  finally show ?case by auto
qed


lemma encode1_replicate_2:
  "partial_state.encode1 (replicate (Suc k) 2) {0..<k} i = i mod (2 ^ k)"
proof -
  have take_Suc: "take k (replicate (Suc k) 2) = replicate k 2"
    apply (subst take_replicate) by auto
  have take_encode: "take k (digit_encode (replicate (Suc k) 2) i) = digit_encode (replicate k 2) i"
    apply (subst digit_encode_take) using take_Suc by metis
  show ?thesis
    unfolding partial_state.encode1_def partial_state.dims1_def
      nths_upt_eq_take[simplified lessThan_atLeast0] take_Suc take_encode
      digit_decode_encode prod_list_replicate ..
qed

lemma encode2_replicate_2:
  assumes "i < 2 ^ Suc k"
  shows "partial_state.encode2 (replicate (Suc k) 2) {0..<k} i = i div (2 ^ k)"
proof -
  have drop_Suc: "drop k (replicate (Suc k) 2) = [2]"
    apply (subst drop_replicate) by auto
  have drop_encode: "drop k (digit_encode (replicate (Suc k) 2) i) = digit_encode [2] (i div (2 ^ k))"
    unfolding digit_encode_drop drop_Suc take_replicate prod_list_replicate
    by (metis lessI min.strict_order_iff)
  have le2: "i div 2 ^ k < 2"
    using assms by (auto simp add: less_mult_imp_div_less)
  have prod_list_2: "prod_list [2] = 2" by simp
  show ?thesis
    unfolding partial_state.encode2_def partial_state.dims2_def
      nths_minus_upt_eq_drop[simplified lessThan_atLeast0] drop_Suc drop_encode
      digit_decode_encode prod_list_2
    using le2 by auto
qed

lemma ket_zero_k_decode:
  "k < n ⟹ ket_zero_k k = Matrix.vec (2^(Suc k)) (λk. if k = 0 then 1 else 0)"
proof (induct k)
  case 0                            
  show ?case apply (rule eq_vecI) by (auto simp add: ket_zero_def)
next
  case (Suc k)
  then have k: "k < n" by auto
  have kzkk: "ket_zero_k k = Matrix.vec (2 ^ Suc k) (λk. if (k = 0) then 1 else 0)" using Suc(1)[OF k] by auto

  have dSk: "ket_zero_k (Suc k) ∈ carrier_vec (2^(Suc (Suc k)))" using ket_zero_k_dim[OF Suc(2)] by auto

  interpret st: partial_state "replicate (Suc (Suc k)) 2" "{0..<Suc k}".
  interpret st2: partial_state2 dims "{0..<Suc k}" "{Suc k}" by (unfold_locales, auto)

  have splitset: "({0..<Suc k} ∪ {Suc k}) = {0..<Suc (Suc k)}" by auto
  then have st2dims0: "st2.dims0 = replicate (Suc (Suc k)) 2" unfolding st2.dims0_def st2.vars0_def 
    using dims_nths_le_n[of "Suc (Suc k)"] Suc by auto
  have "⋀x. (x ∈ {0..<Suc k} ⟹ {y ∈ {0..<Suc (Suc k)}. y < x} = {0..<x})" by auto
  then have cardeq: "⋀x. (x ∈ {0..<Suc k} ⟹ card {y ∈ {0..<Suc (Suc k)}. y < x} = card {0..<x})" by auto
  have setcong: "⋀g h I. (⋀x. (x ∈ I ⟹ g x = h x)) ⟹ {g x | x. x ∈ I} = {h x | x. x ∈ I}" by metis
  have "{card {y ∈ {0..<Suc (Suc k)}. y < x} |x. x ∈ {0..<Suc k}} = {card {0..<x} |x. x ∈ {0..<Suc k}} "
    using setcong[OF cardeq, of "{0..<Suc k}"] by auto
  also have "… = {0..<Suc k}" by auto
  finally have st2vars1': "st2.vars1' = {0..<Suc k}" unfolding st2.vars1'_def st2.vars0_def splitset ind_in_set_def by fastforce
  have st2pvsttv: "st2.ptensor_vec = st.tensor_vec" unfolding st2.ptensor_vec_def using st2dims0 st2vars1' by auto
  have "st.encode1 0 = 0" using encode1_replicate_2[of "Suc k" 0] by auto
  moreover have "st.encode2 0 = 0" using encode2_replicate_2[of 0 "Suc k"] by auto
  moreover have  std: "st.d = 2^(Suc (Suc k))" unfolding st.d_def by auto
  ultimately have kzkk0: "ket_zero_k (Suc k) $ 0 = 1" 
    unfolding ket_zero_k.simps st2pvsttv st.tensor_vec_def ket_zero_def using kzkk by auto

  have kzkki: "ket_zero_k (Suc k) $ i = 0" if ine0: "i ≠ 0" and ile: "i < 2^(Suc (Suc k))" for i
  proof (cases "i mod (2 ^ Suc k) ≠ 0")
    case True
    then have "ket_zero_k k $ st.encode1 i = 0" unfolding kzkk using encode1_replicate_2[of "Suc k" i] ile by auto
    then show ?thesis unfolding ket_zero_k.simps st2pvsttv st.tensor_vec_def ket_zero_def std using ile by auto
  next
    case False
    have "i div (2 ^ Suc k) ≠ 0 ∨ i mod (2 ^ Suc k) ≠ 0" using ine0 by fastforce
    then have "i div (2 ^ Suc k) ≠ 0" using False by auto
    moreover have "i div (2 ^ Suc k) < 2" using ile less_mult_imp_div_less by auto
    ultimately have "i div (2 ^ Suc k) = 1" by auto
    then have "st.encode2 i = 1" using encode2_replicate_2[of i "Suc k"] ile by auto
    then have "Matrix.vec 2 (λk. if k = 0 then 1 else 0) $ st.encode2 i = 0" 
      unfolding kzkk by fastforce
    then show ?thesis unfolding ket_zero_k.simps st2pvsttv st.tensor_vec_def ket_zero_def std using ile by auto
  qed

  show ?case apply (rule eq_vecI)
    subgoal for i using kzkk0 kzkki by auto
    using carrier_vecD[OF dSk] by auto
qed

lemma ket_plus_k_decode:
  "k < n ⟹ ket_plus_k k = Matrix.vec (2^(Suc k)) (λl. 1 / csqrt (2^(Suc k)))"
proof (induct k)
  case 0
  then show ?case unfolding ket_plus_k.simps ket_plus_def by auto
next
  case (Suc k)
  then have kpkk: "ket_plus_k k = Matrix.vec (2 ^ Suc k) (λl. 1 / csqrt (2 ^ Suc k))" by auto

  have dSk: "ket_plus_k (Suc k) ∈ carrier_vec (2^(Suc (Suc k)))" using ket_plus_k_dim[OF Suc(2)] by auto

  interpret st: partial_state "replicate (Suc (Suc k)) 2" "{0..<Suc k}".
  interpret st2: partial_state2 dims "{0..<Suc k}" "{Suc k}" by (unfold_locales, auto)

  have splitset: "({0..<Suc k} ∪ {Suc k}) = {0..<Suc (Suc k)}" by auto
  then have st2dims0: "st2.dims0 = replicate (Suc (Suc k)) 2" unfolding st2.dims0_def st2.vars0_def 
    using dims_nths_le_n[of "Suc (Suc k)"] Suc by auto
  have "⋀x. (x ∈ {0..<Suc k} ⟹ {y ∈ {0..<Suc (Suc k)}. y < x} = {0..<x})" by auto
  then have cardeq: "⋀x. (x ∈ {0..<Suc k} ⟹ card {y ∈ {0..<Suc (Suc k)}. y < x} = card {0..<x})" by auto
  have setcong: "⋀g h I. (⋀x. (x ∈ I ⟹ g x = h x)) ⟹ {g x | x. x ∈ I} = {h x | x. x ∈ I}" by metis
  have "{card {y ∈ {0..<Suc (Suc k)}. y < x} |x. x ∈ {0..<Suc k}} = {card {0..<x} |x. x ∈ {0..<Suc k}} "
    using setcong[OF cardeq, of "{0..<Suc k}"] by auto
  also have "… = {0..<Suc k}" by auto
  finally have st2vars1': "st2.vars1' = {0..<Suc k}" unfolding st2.vars1'_def st2.vars0_def splitset ind_in_set_def by blast
  have st2pvsttv: "st2.ptensor_vec = st.tensor_vec" unfolding st2.ptensor_vec_def using st2dims0 st2vars1' by auto

  have "csqrt (2 ^ (Suc k)) = complex_of_real (sqrt (2 ^ (Suc k)))" by simp
  moreover have "complex_of_real (sqrt (2 ^ (Suc k))) * complex_of_real (sqrt 2) = complex_of_real (sqrt (2 ^ (Suc (Suc k))))"
    by (metis of_real_mult power_Suc power_commutes real_sqrt_power)
  ultimately have "csqrt (2 ^ (Suc k)) * csqrt 2 = csqrt (2 ^ (Suc (Suc k)))" by auto
  moreover have "1 / csqrt (2 ^ Suc k) * 1 / csqrt 2 = 1 / (csqrt (2 ^ (Suc k)) * csqrt 2)" by simp
  ultimately have csqrt2p :"1 / csqrt (2 ^ Suc k) * 1 / csqrt 2 = 1 / (csqrt (2 ^ (Suc (Suc k))))" by simp

  have std: "st.d = 2^(Suc (Suc k))" unfolding st.d_def by auto

  have nthsSSk2: "nths (replicate (Suc (Suc k)) 2) {0..<Suc k} = replicate (Suc k) 2" 
    unfolding nths_replicate[of "Suc (Suc k)" 2 "{0..<Suc k}"]
    by (smt Collect_cong ‹{card {0..<x} |x. x ∈ {0..<Suc k}} = {0..<Suc k}› atLeastLessThan_iff card_atLeastLessThan diff_zero less_SucI)
  then have std1: "st.d1 = 2^(Suc k)" unfolding st.d1_def st.dims1_def nthsSSk2 by auto
  have "{i. i < Suc (Suc k) ∧ i ∈ {Suc k..}} = {Suc k}" by auto
  then have "nths (replicate (Suc (Suc k)) 2) ({Suc k..}) = replicate 1 2" unfolding nths_replicate by auto
  moreover have "(- {0..<Suc k}) = {Suc k..}" by auto
  ultimately have nthsSSk2c: "nths (replicate (Suc (Suc k)) 2) (- {0..<Suc k}) = replicate 1 2" by auto
  have std2: "st.d2 = 2" unfolding st.d2_def st.dims2_def apply (subst nthsSSk2c) by auto

  have "st.encode1 i < st.d1" if "i < st.d" for i using that st.encode1_lt[OF that] by auto
  then have kpkki: "ket_plus_k k $ st.encode1 i = 1 / csqrt (2^(Suc k))" if "i < st.d" for i unfolding kpkk std1 using that by auto
  have "st.encode2 i < st.d2" if "i < st.d" for i using that st.encode2_lt[OF that] by auto
  then have kpi: "ket_plus $ st.encode2 i = 1 / csqrt 2" if "i < st.d" for i unfolding ket_plus_def std2 using that by auto
  have kzkki: "ket_plus_k (Suc k) $ i = 1 / (csqrt (2 ^ (Suc (Suc k))))" if "i < st.d" for i
    unfolding ket_plus_k.simps st2pvsttv st.tensor_vec_def using csqrt2p kpkki kpi that  by auto
  show ?case apply (rule eq_vecI)
    subgoal for i using kzkki unfolding std by auto
    using carrier_vecD[OF dSk] by auto
qed

lemma exH_k_mult_pre_is_psi:
  "exH_k (n - 1) *⇩v ket_pre = ψ"
proof -
  have "exH_k (n - 1) = H_k (n - 1)" using exH_eq_H by auto
  moreover have "ket_zero_k (n - 1) = ket_pre" using ket_zero_k_decode[of "n - 1"] ket_pre_def N_def n by auto
  moreover have "ket_plus_k (n - 1) = ψ" using ket_plus_k_decode[of "n - 1"] ψ_def N_def n by auto
  moreover have "H_k (n - 1) *⇩v ket_zero_k (n - 1) = ket_plus_k (n - 1)" using H_k_ket_zero_k n by auto
  ultimately show ?thesis by auto
qed

definition ket_k :: "nat ⇒ complex vec" where
  "ket_k x = Matrix.vec K (λk. if k = x then 1 else 0)"

lemma ket_k_dim:
  "ket_k k ∈ carrier_vec K"
  unfolding ket_k_def by auto

lemma mat_incr_mult_ket_k:
  "k < K ⟹ (mat_incr K) *⇩v (ket_k k) = (ket_k ((k + 1) mod K))"
  apply (rule eq_vecI)
  unfolding mat_incr_def ket_k_def
   apply (simp add: scalar_prod_def)
   apply (case_tac "k = K - 1")
  subgoal for i apply auto by (simp add: sum_only_one_neq_0[of _ "K - 1"])
  subgoal for i apply auto by (simp add: sum_only_one_neq_0[of _ "i - 1"])
  by auto

definition proj_k where
  "proj_k x = proj (ket_k x)"

lemma proj_k_dim:
  "proj_k k ∈ carrier_mat K K"
  unfolding proj_k_def using ket_k_dim by auto

lemma norm_ket_k_lt_K:
  "k < K ⟹ inner_prod (ket_k k) (ket_k k) = 1"
  unfolding ket_k_def apply (simp add: scalar_prod_def)
  using sum_only_one_neq_0[of "{0..<K}" k "λi. (if i = k then 1 else 0) * cnj (if i = k then 1 else 0)"] by auto

lemma norm_ket_k_ge_K:
  "k ≥ K ⟹ inner_prod (ket_k k) (ket_k k) = 0"
  unfolding ket_k_def by (simp add: scalar_prod_def)

lemma norm_ket_k:
  "inner_prod (ket_k k) (ket_k k) ≤ 1"
  apply (case_tac "k < K")
  using norm_ket_k_lt_K norm_ket_k_ge_K by (auto simp: less_eq_complex_def)

lemma proj_k_mat:
  assumes "k < K"
  shows "proj_k k = mat K K (λ(i, j). if (i = j ∧ i = k) then 1 else 0)" 
  apply (rule eq_matI)
    apply (simp add: proj_k_def ket_k_def index_outer_prod) 
  using proj_k_dim by auto

lemma positive_proj_k:
  "positive (proj_k k)"
  using positive_same_outer_prod unfolding proj_k_def ket_k_def by auto 

lemma proj_k_le_one:
  "(proj_k k) ≤⇩L 1⇩m K"
  unfolding proj_k_def using outer_prod_le_one norm_ket_k ket_k_def by auto

definition proj_psi where
  "proj_psi = proj ψ"

lemma proj_psi_dim:
  "proj_psi ∈ carrier_mat N N"
  unfolding proj_psi_def ψ_def by auto

lemma norm_psi:
  "inner_prod ψ ψ = 1"
  apply (simp add: ψ_eval scalar_prod_def)
  by (metis norm_of_nat norm_of_real of_real_mult of_real_of_nat_eq real_sqrt_mult_self)

lemma proj_psi_mat:
  "proj_psi = mat N N (λk. 1 / N)"
  unfolding proj_psi_def
  apply (rule eq_matI, simp_all)
    apply (simp add: ψ_def index_outer_prod)
    apply (smt of_nat_less_0_iff of_real_of_nat_eq of_real_power power2_eq_square real_sqrt_pow2)
   by (auto simp add: carrier_matD[OF outer_prod_dim[OF ψ_dim(1) ψ_dim(1)]])

lemma hermitian_proj_psi:
  "hermitian proj_psi" 
  unfolding hermitian_def proj_psi_mat apply (rule eq_matI)
  by (auto simp add: adjoint_eval)

lemma hermitian_exproj_psi:
  "hermitian (tensor_P proj_psi (1⇩m K))"
  unfolding ps2_P.ptensor_mat_def
  apply (subst ps_P.tensor_mat_hermitian)
  using proj_psi_dim ps_P_d1 ps_P_d2 hermitian_proj_psi hermitian_one by auto

lemma proj_psi_is_projection:
  "proj_psi * proj_psi = proj_psi"
proof -
  have "proj_psi * proj_psi = inner_prod ψ ψ ⋅⇩m proj_psi"
    unfolding proj_psi_def 
    apply (subst outer_prod_mult_outer_prod) using  ψ_def by auto
  also have "… = proj_psi"
    using ψ_inner by auto
  finally show ?thesis.
qed

lemma proj_psi_trace:
  "trace (proj_psi) = 1"
  unfolding proj_psi_def
  apply (subst trace_outer_prod[of _ N]) 
  subgoal unfolding ψ_def by auto using norm_psi by auto

lemma positive_proj_psi:
  "positive (proj_psi)"
  using positive_same_outer_prod unfolding proj_psi_def ψ_def by auto 

lemma proj_psi_le_one:
  "(proj_psi) ≤⇩L 1⇩m N"
  unfolding proj_psi_def using outer_prod_le_one norm_psi ψ_def by auto

lemma hermitian_hadamard_on_k:
  assumes "k < n"
  shows "hermitian (hadamard_on_i k)"
proof -
  interpret st2: partial_state2 dims "{k}" "(vars1 - {k})"
    apply unfold_locales by auto
  have st2d1: "st2.dims1 = [2]" unfolding st2.dims1_def dims_def
    using assms dims_nths_one_lt_n local.dims_def st2.dims1_def by auto
  show "hermitian (hadamard_on_i k)" unfolding hadamard_on_i_def st2.pmat_extension_def st2.ptensor_mat_def
    apply (rule partial_state.tensor_mat_hermitian)
    subgoal unfolding partial_state.d1_def partial_state.dims1_def st2.nths_vars1' hadamard_def by (simp add: st2d1)
    subgoal unfolding partial_state.d2_def partial_state.dims2_def st2.nths_vars2' st2.d2_def by auto
    subgoal unfolding hermitian_def hadamard_def apply (rule eq_matI) by (auto simp add: adjoint_dim adjoint_eval)
    using hermitian_one by auto
qed

lemma hermitian_H_k:
  "k < n ⟹ hermitian (H_k k)"
proof (induct k)
  case 0
  show ?case unfolding H_k.simps hermitian_def hadamard_def apply (rule eq_matI) by (auto simp add: adjoint_dim adjoint_eval)
next
  case (Suc k)
  interpret st2: partial_state2 dims "{0..<Suc k}" "{Suc k}"
    apply unfold_locales by auto
  have st2d1: "prod_list st2.dims1 = (2^(Suc k))" unfolding st2.dims1_def dims_def using Suc(2)
    using dims_nths_le_n local.dims_def st2.dims1_def by auto
  have st2d2: "st2.dims2 = [2]" unfolding st2.dims2_def dims_def using Suc(2)
    using dims_nths_one_lt_n local.dims_def st2.dims2_def by auto
  show ?case unfolding H_k.simps st2.ptensor_mat_def
    apply (rule partial_state.tensor_mat_hermitian)
    subgoal unfolding partial_state.d1_def partial_state.dims1_def st2.nths_vars1' using st2d1 H_k_dim Suc by auto
    subgoal unfolding partial_state.d2_def partial_state.dims2_def st2.nths_vars2' st2.d2_def using st2d2 by (simp add: hadamard_def)
    subgoal using Suc by auto
    using hermitian_hadamard by auto
qed

lemma unitary_H_k:
  "k < n ⟹ unitary (H_k k)"
proof (induct k)
  case 0
  show ?case using unitary_hadamard by auto
next
  case (Suc k)
  then have k: "k < n" by auto
  interpret st2: partial_state2 dims "{0..<Suc k}" "{Suc k}" by (unfold_locales, auto)

  have st2d1: "prod_list st2.dims1 = (2^(Suc k))" unfolding st2.dims1_def dims_def using Suc(2)
    using dims_nths_le_n local.dims_def st2.dims1_def by auto
  have st2d2: "st2.dims2 = [2]" unfolding st2.dims2_def dims_def using Suc(2)
    using dims_nths_one_lt_n local.dims_def st2.dims2_def by auto
  show ?case unfolding H_k.simps st2.ptensor_mat_def
    apply (rule partial_state.tensor_mat_unitary[of "H_k k" st2.dims0 st2.vars1' hadamard]  )
    unfolding partial_state.d1_def partial_state.dims1_def st2.nths_vars1' partial_state.d2_def partial_state.dims2_def
      st2.nths_vars2'
       apply (auto simp add: st2d1 st2d2 )
    subgoal using H_k_dim[OF k] by auto
    subgoal using hadamard_dim by auto
    subgoal using Suc by auto
    using unitary_hadamard by auto
qed

lemma exH_k_dim:
  shows "k < n ⟹ exH_k k ∈ carrier_mat N N"
  apply (induct k)
  using hadamard_on_i_dim by auto

lemma exH_n_dim:
  shows "exH_k (n - 1) ∈ carrier_mat N N"
  using exH_k_dim n by auto

lemma unitary_exH_k:
  shows "k < n ⟹ unitary (exH_k k)" 
proof (induct k)
  case 0
  then show ?case unfolding exH_k.simps using unitary_hadamard_on_i 0 by auto 
next
  case (Suc k)
  show ?case unfolding exH_k.simps apply (subst unitary_times_unitary[of _ N])
    subgoal using exH_k_dim Suc by auto
    subgoal using hadamard_on_i_dim Suc by auto
    subgoal using Suc by auto
    using unitary_hadamard_on_i Suc by auto
qed

lemma hermitian_exH_n:
  "hermitian (exH_k (n - 1))"
  using hermitian_H_k exH_eq_H n by auto

lemma exH_k_mult_psi_is_pre:
  "exH_k (n - 1) *⇩v ψ = ket_pre"
proof -
  let ?H = "exH_k (n - 1)"
  have "hermitian ?H" using hermitian_H_k exH_eq_H n by auto
  then have eqad: "adjoint ?H = ?H" unfolding hermitian_def by auto
  have d: "?H ∈ carrier_mat N N" using exH_k_dim n by auto
  have "unitary ?H" using unitary_exH_k n by auto
  then have id: "?H * ?H = 1⇩m N"
    unfolding unitary_def inverts_mat_def
    using d apply (subst (2) eqad[symmetric]) by auto
  have "?H *⇩v ψ = ?H *⇩v (?H *⇩v ket_pre)"
    using exH_k_mult_pre_is_psi by auto
  also have "… = (?H * ?H) *⇩v ket_pre"
    using d ket_pre_def by auto
  also have "… = ket_pre"
    using id ket_pre_def by auto
  finally show ?thesis by auto
qed

fun exexH_k :: "nat ⇒ complex mat" where
  "exexH_k k = tensor_P (exH_k k) (1⇩m K)"

lemma unitary_exexH_k:
  "k < n ⟹ unitary (exexH_k k)" 
  unfolding exexH_k.simps ps2_P.ptensor_mat_def 
  apply (subst partial_state.tensor_mat_unitary)
  subgoal using exH_k_dim unfolding partial_state.d1_def partial_state.dims1_def ps2_P.nths_vars1' ps2_P.dims1_def dims_vars1 N_def by auto
  subgoal unfolding partial_state.d2_def partial_state.dims2_def ps2_P.nths_vars2' ps2_P.dims2_def dims_vars2 by auto
  using unitary_exH_k unitary_one by auto

lemma exexH_k_dim:
  "k < n ⟹ exexH_k k ∈ carrier_mat d d"
  unfolding exexH_k.simps using ps2_P.ptensor_mat_carrier ps2_P_d0 by auto

lemma hoare_seq_utrans:
  fixes P :: "complex mat"
  assumes "unitary U1" and "unitary U2" and "is_quantum_predicate P"
    and dU1: "U1 ∈ carrier_mat d d" and dU2: "U2 ∈ carrier_mat d d"
  shows "
   ⊢⇩p 
   {adjoint (U2 * U1) * P * (U2 * U1)} 
   Utrans U1;; Utrans U2
   {P}"
proof -
  have hp0: "⊢⇩p {adjoint (U2) * P * (U2)} Utrans U2 {P}"
    using assms hoare_partial.intros by auto
  have qp: "is_quantum_predicate (adjoint (U2) * P * (U2))"
    using qp_close_under_unitary_operator assms by auto
  then have hp1: "⊢⇩p {adjoint U1 * (adjoint (U2) * P * (U2)) * U1} Utrans U1 {adjoint (U2) * P * (U2)}"
    using hoare_partial.intros by auto
  have dP: "P ∈ carrier_mat d d" using assms is_quantum_predicate_def by auto
  have eq: "adjoint U1 * (adjoint U2 * P * U2) * U1 = adjoint (U2 * U1) * P * (U2 * U1)"
    using dU1 dU2 dP by (mat_assoc d)
  with hp1 have hp2: "⊢⇩p {adjoint (U2 * U1) * P * (U2 * U1)} Utrans U1 {adjoint (U2) * P * (U2)}" by auto

  have "is_quantum_predicate (adjoint U1 * (adjoint U2 * P * U2) * U1)" using qp qp_close_under_unitary_operator assms by auto
  then have "is_quantum_predicate (adjoint (U2 * U1) * P * (U2 * U1))" using eq by auto
  then show ?thesis using hoare_partial.intros(3)[OF _ qp assms(3)] hp0 hp2 by auto
qed

lemma qp_close_after_exexH_k:
  fixes P :: "complex mat"
  assumes "is_quantum_predicate P"
  shows "k < n ⟹ is_quantum_predicate (adjoint (exexH_k k) * P * exexH_k k)"
  apply (subst qp_close_under_unitary_operator)
  subgoal using exexH_k_dim by auto
  subgoal using unitary_exexH_k by auto
  using assms by auto

lemma hoare_hadamard_n:
  fixes P :: "complex mat"
  shows "is_quantum_predicate P ⟹ k < n ⟹ 
   ⊢⇩p 
   {adjoint (exexH_k k) * P * exexH_k k} 
   hadamard_n (Suc k)
   {P}"
proof (induct k arbitrary: P)
  case 0
  have qp: "is_quantum_predicate (adjoint (exexH_k 0) * P * exexH_k 0)"
    using qp_close_under_unitary_operator[OF _ unitary_exhadamard_on_i[of 0]] tensor_P_dim 0 by auto
  then have "⊢⇩p {adjoint (exexH_k 0) * P * exexH_k 0} SKIP {adjoint (exexH_k 0) * P * exexH_k 0}"
    using hoare_partial.intros(1) by auto
  moreover have "⊢⇩p {adjoint (exexH_k 0) * P * exexH_k 0} Utrans (tensor_P (hadamard_on_i 0) (1⇩m K)) {P}"
    using hoare_partial.intros(2) 0 by auto
  ultimately have "⊢⇩p {adjoint (exexH_k 0) * P * exexH_k 0} SKIP;; Utrans (tensor_P (hadamard_on_i 0) (1⇩m K)) {P}"
    using hoare_partial.intros(3) qp 0 by auto
  then show ?case using qp by auto
next
  case (Suc k)
  have h1: "⊢⇩p 
    {adjoint (tensor_P (hadamard_on_i (Suc k)) (1⇩m K)) * P * (tensor_P (hadamard_on_i (Suc k)) (1⇩m K))} 
    Utrans (tensor_P (hadamard_on_i (Suc k)) (1⇩m K)) 
    {P}"
    using hoare_partial.intros Suc by auto
  have qp: "is_quantum_predicate (adjoint (tensor_P (hadamard_on_i (Suc k)) (1⇩m K)) * P * (tensor_P (hadamard_on_i (Suc k)) (1⇩m K)))"
    apply (subst qp_close_under_unitary_operator)
    subgoal using ps2_P.ptensor_mat_carrier ps2_P_d0 by auto
    subgoal unfolding ps2_P.ptensor_mat_def apply (subst partial_state.tensor_mat_unitary ) 
      subgoal unfolding partial_state.d1_def partial_state.dims1_def ps2_P.nths_vars1' ps2_P.dims1_def d_vars1 using hadamard_on_i_dim Suc by auto
      subgoal unfolding partial_state.d2_def partial_state.dims2_def ps2_P.nths_vars2' ps2_P.dims2_def using dims_vars2 by auto
      using unitary_hadamard_on_i unitary_one Suc by auto
    using Suc by auto
  then have h2: "⊢⇩p 
    {adjoint (exexH_k k) * (adjoint (tensor_P (hadamard_on_i (Suc k)) (1⇩m K)) * P * (tensor_P (hadamard_on_i (Suc k)) (1⇩m K))) * exexH_k k} 
    hadamard_n (Suc k)
    {adjoint (tensor_P (hadamard_on_i (Suc k)) (1⇩m K)) * P * (tensor_P (hadamard_on_i (Suc k)) (1⇩m K))}"
    using Suc by auto
  have "(tensor_P (hadamard_on_i (Suc k)) (1⇩m K)) * exexH_k k
    = (tensor_P (hadamard_on_i (Suc k) * (exH_k k)) (1⇩m K * (1⇩m K)))"
    apply (subst ps2_P.ptensor_mat_mult)
    subgoal using hadamard_on_i_dim ps2_P_d1 Suc by auto
    subgoal using exH_k_dim ps2_P_d1 Suc by auto
    using ps2_P_d2 by auto
  also have "… = exexH_k (Suc k)" using mult_exH_k_left Suc by auto
  finally have eq1: "(tensor_P (hadamard_on_i (Suc k)) (1⇩m K)) * exexH_k k = exexH_k (Suc k)".
  then have eq2: "adjoint (exexH_k k) * adjoint (tensor_P (hadamard_on_i (Suc k)) (1⇩m K)) = adjoint (exexH_k (Suc k))"
    apply (subst adjoint_mult[symmetric, of _ d d _ d])
    subgoal using tensor_P_dim by auto
    using exexH_k_dim Suc by auto
  have dP: "P ∈ carrier_mat d d" using is_quantum_predicate_def Suc by auto
  moreover have dH: "exexH_k k ∈ carrier_mat d d" using exexH_k_dim Suc by auto
  moreover have dHi: "tensor_P (hadamard_on_i (Suc k)) (1⇩m K) ∈ carrier_mat d d" using tensor_P_dim by auto
  ultimately have eq3: "adjoint (exexH_k k) * (adjoint (tensor_P (hadamard_on_i (Suc k)) (1⇩m K)) * P * tensor_P (hadamard_on_i (Suc k)) (1⇩m K)) * exexH_k k
    = (adjoint (exexH_k k) * adjoint (tensor_P (hadamard_on_i (Suc k)) (1⇩m K))) * P * (tensor_P (hadamard_on_i (Suc k)) (1⇩m K) * exexH_k k)"
    by (mat_assoc d)
  show ?case apply (subst hadamard_n.simps) 
    apply (subst hoare_partial.intros(3)[of _ "adjoint (tensor_P (hadamard_on_i (Suc k)) (1⇩m K)) * P * (tensor_P (hadamard_on_i (Suc k)) (1⇩m K))"])
    subgoal using qp_close_after_exexH_k[of P "Suc k"] Suc by auto
    subgoal using qp by auto
    subgoal using Suc by auto
    subgoal using h2[simplified eq3 eq1 eq2] by auto
    using h1 by auto
qed

lemma qp_pre:
  "is_quantum_predicate (tensor_P pre (proj_k 0))"
  unfolding is_quantum_predicate_def
proof (intro conjI)
  show "tensor_P pre (proj_k 0) ∈ carrier_mat d d" using tensor_P_dim by auto
  interpret st: partial_state dims vars1 .
  have d1: "st.d1 = N" unfolding st.d1_def st.dims1_def using d_vars1 by auto
  have d2: "st.d2 = K" unfolding st.d2_def st.dims2_def nths_uminus_vars1 dims_vars2 by auto
  show "positive (tensor_P pre (proj_k 0))"
    unfolding ps2_P.ptensor_mat_def ps2_P_dims0  ps2_P_vars1' 
    apply (subst st.tensor_mat_positive)
    subgoal unfolding pre_def using outer_prod_dim ket_pre_def d1 by auto
    subgoal unfolding proj_k_def using outer_prod_dim ket_k_def d2 by auto
    subgoal using positive_pre by auto
    using positive_proj_k[of 0] K_gt_0 by auto
  show "tensor_P pre (proj_k 0) ≤⇩L 1⇩m d"
    unfolding ps2_P.ptensor_mat_def ps2_P_dims0  ps2_P_vars1' 
    apply (subst st.tensor_mat_le_one)
    subgoal using pre_def ket_pre_def outer_prod_dim d1 by auto
    subgoal using proj_k_def K_gt_0 ket_k_def outer_prod_dim d2 by auto
    using d1 d2  K_gt_0 outer_prod_dim positive_pre positive_proj_k pre_le_one proj_k_le_one by auto
qed

lemma qp_init_post:
  "is_quantum_predicate (tensor_P proj_psi (proj_k 0))"
  unfolding is_quantum_predicate_def
proof (intro conjI)
  show "tensor_P proj_psi (proj_k 0) ∈ carrier_mat d d" using tensor_P_dim by auto
  interpret st: partial_state dims vars1 .
  have d1: "st.d1 = N" unfolding st.d1_def st.dims1_def using d_vars1 by auto
  have d2: "st.d2 = K" unfolding st.d2_def st.dims2_def nths_uminus_vars1 dims_vars2 by auto
  show "positive (tensor_P proj_psi (proj_k 0))"
    unfolding ps2_P.ptensor_mat_def ps2_P_dims0  ps2_P_vars1' 
    apply (subst st.tensor_mat_positive)
    subgoal unfolding proj_psi_def using outer_prod_dim ψ_def d1 by auto
    subgoal unfolding proj_k_def using outer_prod_dim ket_k_def d2 by auto
    subgoal using positive_proj_psi by auto
    using positive_proj_k[of 0] K_gt_0 by auto
  show "tensor_P proj_psi (proj_k 0) ≤⇩L 1⇩m d"
    unfolding ps2_P.ptensor_mat_def ps2_P_dims0  ps2_P_vars1' 
    apply (subst st.tensor_mat_le_one)
    subgoal using proj_psi_def outer_prod_dim d1 by auto
    subgoal using proj_k_def K_gt_0 ket_k_def outer_prod_dim d2 by auto
    using d1 d2  K_gt_0 outer_prod_dim positive_proj_psi positive_proj_k proj_psi_le_one proj_k_le_one by auto
qed

lemma tensor_P_adjoint_left_right:
  assumes "m1 ∈ carrier_mat N N" and "m2 ∈ carrier_mat K K" and "m3 ∈ carrier_mat N N" and "m4 ∈ carrier_mat K K"
  shows "adjoint (tensor_P m1 m2) * tensor_P m3 m4 * tensor_P m1 m2 = tensor_P (adjoint m1 * m3 * m1) (adjoint m2 * m4 * m2)"
proof -
  have eq1: "adjoint (tensor_P m1 m2) = tensor_P (adjoint m1) (adjoint m2)"
    unfolding ps2_P.ptensor_mat_def
    apply (subst ps_P.tensor_mat_adjoint)
    using ps_P_d1 ps_P_d2 assms by auto
  have eq2: "adjoint (tensor_P m1 m2) * tensor_P m3 m4 = tensor_P (adjoint m1 * m3) (adjoint m2 * m4)"
    unfolding ps2_P.ptensor_mat_def
    apply (subst ps_P.tensor_mat_mult)
    using ps_P_d1 ps_P_d2 assms eq1 unfolding ps2_P.ptensor_mat_def by (auto simp add: adjoint_dim)
  have eq3: "tensor_P (adjoint m1 * m3) (adjoint m2 * m4) * (tensor_P m1 m2) = tensor_P (adjoint m1 * m3 * m1) (adjoint m2 * m4 * m2)"
    unfolding ps2_P.ptensor_mat_def
    apply (subst ps_P.tensor_mat_mult[of "adjoint m1 * m3"])
    using ps_P_d1 ps_P_d2 assms by (auto simp add: adjoint_dim)
  show ?thesis using eq1 eq2 eq3 by auto
qed

abbreviation exH_n where
  "exH_n ≡ exH_k (n - 1)"

lemma hoare_triple_init:
  "⊢⇩p 
   {tensor_P pre (proj_k 0)} 
   hadamard_n n
   {tensor_P proj_psi (proj_k 0)}"
proof -
  have h: "⊢⇩p 
   {adjoint (exexH_k (n - 1)) * (tensor_P proj_psi (proj_k 0)) * (exexH_k (n - 1))} 
   hadamard_n n
   {tensor_P proj_psi (proj_k 0)}"
    using hoare_hadamard_n[OF qp_init_post, of "n - 1"] qp_init_post n by auto
  have "adjoint (exexH_k (n - 1)) * tensor_P proj_psi (proj_k 0) * exexH_k (n - 1) =
        tensor_P (adjoint exH_n * proj_psi * exH_n) (adjoint (1⇩m K) * proj_k 0 * 1⇩m K)"
    unfolding exexH_k.simps
    apply (subst tensor_P_adjoint_left_right)
    using exH_k_dim proj_psi_def ψ_def  proj_k_def ket_k_def n by (auto)
  moreover have "adjoint exH_n * proj_psi * exH_n = pre"
    unfolding proj_psi_def pre_def
    apply (subst outer_prod_left_right_mat[of _ N _ N _ N _ N])
    subgoal using ψ_def by auto
    subgoal using exH_k_dim n by (simp add: adjoint_dim)
    subgoal using exH_k_dim n by simp
    apply (subst (1 2) hermitian_exH_n[simplified hermitian_def])
    apply (subst (1 2) exH_k_mult_psi_is_pre)
    by auto
  moreover have "adjoint (1⇩m K) * (proj_k 0) * (1⇩m K) = proj_k 0"
    apply (subst adjoint_one) using proj_k_dim[of 0] K_gt_0 by auto
  ultimately have "adjoint (exexH_k (n - 1)) * tensor_P proj_psi (proj_k 0) * exexH_k (n - 1) = tensor_P pre (proj_k 0)"
    by auto
  with h show ?thesis by auto
qed

text ‹Hoare triples of while loop›

definition proj_psi_l where
  "proj_psi_l l = proj (psi_l l)"

lemma positive_psi_l:
  "k < K ⟹ positive (proj_psi_l k)"
  unfolding proj_psi_l_def
  apply (subst positive_same_outer_prod)
  using psi_l_dim by auto

lemma hermitian_proj_psi_l:
  "k < K ⟹ hermitian (proj_psi_l k)"
  using positive_psi_l positive_is_hermitian by auto

definition P' where
  "P' = tensor_P (proj_psi_l R) (proj_k R)"

lemma proj_psi_l_dim:
  "proj_psi_l l ∈ carrier_mat N N"
  unfolding proj_psi_l_def using psi_l_def by auto

definition Q :: "complex mat" where
  "Q = matrix_sum d (λl. tensor_P (proj_psi_l l) (proj_k l)) R"

lemma psi_l_le_id:
  shows "proj_psi_l l ≤⇩L 1⇩m N"
proof -
  have "inner_prod (psi_l l) (psi_l l) = 1"
    using inner_psi_l by auto
  then show ?thesis using outer_prod_le_one psi_l_def proj_psi_l_def by auto
qed

lemma positive_proj_psi_l:
  shows "positive (proj_psi_l l)"
  using positive_same_outer_prod proj_psi_l_def psi_l_dim by auto

definition proj_fst_k :: "nat ⇒ complex mat" where
  "proj_fst_k k = mat K K (λ(i, j). if (i = j ∧ i < k) then 1 else 0)"

lemma hermitian_proj_fst_k:
  "adjoint (proj_fst_k k) = proj_fst_k k"
  by (auto simp add: proj_fst_k_def adjoint_eval)

lemma proj_fst_k_is_projection:
  "proj_fst_k k * proj_fst_k k = proj_fst_k k"
  by (auto simp add: proj_fst_k_def scalar_prod_def sum_only_one_neq_0)

lemma positive_proj_fst_k:
  "positive (proj_fst_k k)"
proof -
  have "(proj_fst_k k) * adjoint (proj_fst_k k) = (proj_fst_k k)"
    using hermitian_proj_fst_k proj_fst_k_is_projection by auto
  then have "∃M. M * adjoint M = (proj_fst_k k)" by auto
  then show ?thesis apply (subst positive_if_decomp) using proj_fst_k_def by auto
qed

lemma proj_fst_k_le_one:
  "proj_fst_k k ≤⇩L 1⇩m K"
proof -
  define M where "M l = mat K K (λ(i, j). if (i = j ∧ i ≥ l) then (1::complex) else 0)" for l
  have eq: "1⇩m K - proj_fst_k k = M k" unfolding M_def proj_fst_k_def
    apply (rule eq_matI) by auto
  have "M k * M k = M k" unfolding M_def
    apply (rule eq_matI) apply (simp add: scalar_prod_def)
      apply (subst sum_only_one_neq_0[of _ j]) by auto
  moreover have "adjoint (M k) = M k" unfolding M_def
    apply (rule eq_matI) by (auto simp add: adjoint_eval)
  ultimately have "M k * adjoint (M k) = M k" by auto
  then have "∃M. M * adjoint M = 1⇩m K - proj_fst_k k" using eq by auto
  then have "positive (1⇩m K - proj_fst_k k)" 
    apply (subst positive_if_decomp) using proj_fst_k_def by auto
  then show ?thesis unfolding lowner_le_def using proj_fst_k_def by auto
qed

lemma sum_proj_k:
  assumes "m ≤ K"
  shows "matrix_sum K (λk. proj_k k) m = proj_fst_k m"
proof -
  have "m ≤ K ⟹ matrix_sum K (λk. proj_k k) m = mat K K (λ(i, j). if (i = j ∧ i < m) then 1 else 0)" for m
  proof (induct m)
    case 0
    then show ?case apply simp apply (rule eq_matI) by auto
  next
    case (Suc m)
    then have m: "m < K" by auto
    then have m': "m ≤ K" by auto
    have "matrix_sum K proj_k (Suc m) = proj_k m + matrix_sum K proj_k m" by simp
    also have "… = mat K K (λ(i, j). if (i = j ∧ i < (Suc m)) then 1 else 0)"
      unfolding proj_k_mat[OF m] Suc(1)[OF m'] apply (rule eq_matI) by auto
    finally show ?case by auto
  qed
  then show ?thesis unfolding proj_fst_k_def using assms by auto
qed

lemma proj_psi_proj_k_le_exproj_k:
  shows "tensor_P (proj_psi_l k) (proj_k l) ≤⇩L tensor_P (1⇩m N) (proj_k l)"
  unfolding ps2_P.ptensor_mat_def
  apply (subst ps_P.tensor_mat_positive_le) 
  subgoal using proj_psi_l_def psi_l_dim ps_P_d1 by auto
  subgoal using proj_k_def ket_k_def ps_P_d2 by auto
  subgoal using positive_proj_psi_l by auto
  subgoal using positive_same_outer_prod proj_k_def ket_k_def by auto
  subgoal using psi_l_le_id by auto
  apply (subst lowner_le_refl[of _ K]) by (auto simp add: proj_k_def ket_k_def)

definition Q1 :: "complex mat" where
  "Q1 = matrix_sum d (λl. tensor_P (proj_psi'_l l) (proj_k l)) R"

lemma tensor_P_left_right_partial1:
  assumes "m1 ∈ carrier_mat N N" and "m2 ∈ carrier_mat N N" and "m3 ∈ carrier_mat K K" and "m4 ∈ carrier_mat N N"
  shows "tensor_P m1 (1⇩m K) * tensor_P m2 m3 * tensor_P m4 (1⇩m K) = tensor_P (m1 * m2 * m4) m3"
proof -
  have "tensor_P m1 (1⇩m K) * tensor_P m2 m3 = tensor_P (m1 * m2) m3"
    unfolding ps2_P.ptensor_mat_def 
    apply (subst ps_P.tensor_mat_mult[symmetric])
    using assms ps_P_d1 ps_P_d2 by auto
  moreover have "tensor_P (m1 * m2) m3 * tensor_P m4 (1⇩m K) = tensor_P (m1 * m2 * m4) m3"
    unfolding ps2_P.ptensor_mat_def 
    apply (subst ps_P.tensor_mat_mult[symmetric])
    using assms ps_P_d1 ps_P_d2 by auto
  ultimately show ?thesis by auto
qed

lemma tensor_P_left_right_partial2:
  assumes "m1 ∈ carrier_mat K K" and "m2 ∈ carrier_mat K K" and "m3 ∈ carrier_mat N N" and "m4 ∈ carrier_mat K K"
  shows "tensor_P (1⇩m N) m1 * tensor_P m3 m2 * tensor_P (1⇩m N) m4 = tensor_P m3 (m1 * m2 * m4)"
proof -
  have "tensor_P (1⇩m N) m1 * tensor_P m3 m2 = tensor_P m3 (m1 * m2)"
    unfolding ps2_P.ptensor_mat_def 
    apply (subst ps_P.tensor_mat_mult[symmetric])
    using assms ps_P_d1 ps_P_d2 by auto
  moreover have "tensor_P m3 (m1 * m2) * tensor_P (1⇩m N) m4 = tensor_P m3 (m1 * m2 * m4)"
    unfolding ps2_P.ptensor_mat_def 
    apply (subst ps_P.tensor_mat_mult[symmetric])
    using assms ps_P_d1 ps_P_d2 by auto
  ultimately show ?thesis by auto
qed

lemma matrix_sum_mult_left_right:
  fixes A B :: "complex mat"
  assumes dg: "(⋀k. k < l ⟹ g k ∈ carrier_mat m m) "
    and dA: "A ∈ carrier_mat m m" and dB: "B ∈ carrier_mat m m"
  shows "matrix_sum m (λk. A * g k * B) l = A * matrix_sum m g l * B"
proof -
  have eq: "A * matrix_sum m g l = matrix_sum m (λk. A * g k) l" 
    using matrix_sum_distrib_left assms by auto
  have "A * matrix_sum m g l * B = matrix_sum m (λk. A * g k * B) l"
    apply (subst eq)
    using matrix_sum_mult_right[of l "λk. A * g k"] assms by auto
  then show ?thesis by auto
qed

lemma mat_O_split:
  "mat_O = 1⇩m N - 2 ⋅⇩m proj_O"
  apply (rule eq_matI)
  unfolding mat_O_def proj_O_def by auto

lemma mat_O_mult_psi'_l:
  "mat_O *⇩v (psi'_l l) = psi_l l"
proof -
  have "mat_O *⇩v (psi'_l l) = mat_O *⇩v ((alpha_l l) ⋅⇩v α) - mat_O *⇩v ((beta_l l) ⋅⇩v β)"
    unfolding psi'_l_def apply (subst mult_minus_distrib_mat_vec)
    using mat_O_dim α_dim β_dim by auto
  also have "… = (alpha_l l) ⋅⇩v (mat_O *⇩v  α) - (beta_l l) ⋅⇩v (mat_O *⇩v β)"
    using mult_mat_vec_smult_vec_assoc[of mat_O N N] mat_O_dim α_dim β_dim by auto
  also have "… = (alpha_l l) ⋅⇩v α - (beta_l l) ⋅⇩v (- β)"
    using mat_O_mult_alpha mat_O_mult_beta by auto
  also have "… = (alpha_l l) ⋅⇩v α + (beta_l l) ⋅⇩v β"
    by auto
  finally show ?thesis unfolding psi_l_def by auto
qed

lemma mat_O_times_Q1:
  "adjoint (tensor_P mat_O (1⇩m K)) * Q1 * (tensor_P mat_O (1⇩m K)) = Q"
proof -
  let ?m1 = "tensor_P mat_O (1⇩m K)"
  have eq:"adjoint ?m1 = ?m1"
    unfolding ps2_P.ptensor_mat_def 
    apply (subst ps_P.tensor_mat_adjoint)
      apply (auto simp add: mat_O_dim ps_P_d1 ps_P_d2)
    by (simp add: hermitian_mat_O[unfolded hermitian_def] hermitian_one[unfolded hermitian_def])
  {
    fix l
    let ?m2 = "tensor_P (proj_psi'_l l) (proj_k l)"
    have "?m1 * ?m2 * ?m1 = tensor_P (mat_O * (proj_psi'_l l) * mat_O) (proj_k l)"
      apply (subst tensor_P_left_right_partial1)
      using mat_O_dim proj_psi'_dim proj_k_dim by auto
    moreover have "mat_O * (proj_psi'_l l) * mat_O = outer_prod (psi_l l) (psi_l l)"
      unfolding proj_psi'_l_def apply (subst outer_prod_left_right_mat[of _ N _ N  _ N _ N])
      using psi'_l_dim mat_O_dim mat_O_mult_psi'_l hermitian_mat_O[unfolded hermitian_def] by auto
    ultimately have "?m1 * ?m2 * ?m1 = tensor_P (proj_psi_l l) (proj_k l)" unfolding proj_psi_l_def by auto
  }
  note p1 = this
  have "adjoint (tensor_P mat_O (1⇩m K)) * Q1 * (tensor_P mat_O (1⇩m K)) = ?m1 * Q1 * ?m1"
    using eq by auto
  also have "… = matrix_sum d (λl. ?m1 * (tensor_P (proj_psi'_l l) (proj_k l)) * ?m1) R"
    unfolding Q1_def
    apply (subst matrix_sum_mult_left_right) using tensor_P_dim by auto
  also have "… = Q"
    unfolding Q_def using p1 by auto
  finally show ?thesis by auto
qed

definition Q2 where
  "Q2 = matrix_sum d (λl. tensor_P (proj_psi_l (l + 1)) (proj_k l)) R"

lemma Q2_dim:
  "Q2 ∈ carrier_mat d d"
  unfolding Q2_def apply (subst matrix_sum_dim) using tensor_P_dim by auto

lemma Q2_le_one:
  "Q2 ≤⇩L 1⇩m d" 
proof -
  have leq: "Q2 ≤⇩L matrix_sum d (λk. tensor_P (1⇩m N) (proj_k k)) R"
    unfolding Q2_def
    apply (subst lowner_le_matrix_sum)
    subgoal using tensor_P_dim by auto
    subgoal using tensor_P_dim by auto
    using proj_psi_proj_k_le_exproj_k by auto
  have "matrix_sum d (λk. tensor_P (1⇩m N) (proj_k k)) R
      = tensor_P (1⇩m N) (matrix_sum K proj_k R)"
    unfolding ps2_P.ptensor_mat_def
    apply (subst ps_P.tensor_mat_matrix_sum2[simplified ps_P_d ps_P_d2])
    subgoal using ps_P_d1 by auto
    using proj_k_dim by auto
  also have "… = tensor_P (1⇩m N) (proj_fst_k R)" using sum_proj_k K by auto
  also have "… ≤⇩L tensor_P (1⇩m N) (1⇩m K)" unfolding ps2_P.ptensor_mat_def
    apply (subst ps_P.tensor_mat_positive_le)
    subgoal using ps_P_d1 by auto
    subgoal using ps_P_d2 proj_fst_k_def by auto
    subgoal using positive_one by auto
    subgoal using positive_proj_fst_k  by auto
    subgoal using lowner_le_refl[of "1⇩m N" N] by auto
    using proj_fst_k_le_one by auto
  also have "… = 1⇩m d" unfolding ps2_P.ptensor_mat_def
    using ps_P.tensor_mat_id ps_P_d1 ps_P_d2 ps_P_d by auto
  finally have leq2: "matrix_sum d (λk. tensor_P (1⇩m N) (proj_k k)) R ≤⇩L 1⇩m d" by auto
  have ds: "matrix_sum d (λk. tensor_P (1⇩m N) (proj_k k)) R ∈ carrier_mat d d"
    apply (subst matrix_sum_dim) using tensor_P_dim by auto
  then show ?thesis using leq leq2 lowner_le_trans[OF Q2_dim ds, of "1⇩m d"] by auto
qed

lemma qp_Q2:
  "is_quantum_predicate Q2"
  unfolding is_quantum_predicate_def
proof (intro conjI)
  show "Q2 ∈ carrier_mat d d" unfolding Q2_def 
    apply (subst matrix_sum_dim) using tensor_P_dim by auto
next
  show "positive Q2" unfolding Q2_def
    apply (subst matrix_sum_positive)
    subgoal using tensor_P_dim by auto
    subgoal for k unfolding ps2_P.ptensor_mat_def 
      apply (subst ps_P.tensor_mat_positive)
      subgoal using proj_psi_l_def psi_l_dim ps_P_d1 by auto
      subgoal using proj_k_dim ps_P_d2 K by auto
      subgoal using positive_proj_psi_l by auto
       using positive_proj_k K by auto
    by auto
next
  show "Q2 ≤⇩L 1⇩m d" using Q2_le_one by auto
qed

lemma pre_mat:
  "pre = mat N N (λ(i, j). if i = j ∧ i = 0 then 1 else 0)"
  apply (rule eq_matI)
  subgoal for i j  unfolding pre_def apply (subst index_outer_prod[OF ket_pre_dim ket_pre_dim])
      apply simp_all
    unfolding ket_pre_def by auto
  using outer_prod_dim[OF ket_pre_dim ket_pre_dim, folded pre_def] by auto

lemma mat_Ph_split:
  "mat_Ph = 2 ⋅⇩m pre - 1⇩m N"
  unfolding mat_Ph_def pre_mat
  apply (rule eq_matI) by auto
  
lemma H_Ph_H:
  "exexH_k (n-1) * tensor_P mat_Ph (1⇩m K) * exexH_k (n - 1) = 2 ⋅⇩m tensor_P proj_psi (1⇩m K) - 1⇩m d"
  unfolding mat_Ph_split exexH_k.simps
  apply (subst tensor_P_left_right_partial1)
  subgoal using exH_k_dim[of "n - 1"] n by auto
  subgoal using pre_dim by auto
  subgoal by auto
proof -
  have eq1: "exH_n * exH_n = 1⇩m N"
    using unitary_exH_k[of "n - 1"]
    unfolding unitary_def inverts_mat_def
    using n hermitian_exH_n[simplified hermitian_def] exH_n_dim by auto
  have eq2: "exH_n * pre * exH_n = proj_psi"
    unfolding pre_def proj_psi_def
    apply (subst outer_prod_left_right_mat[of _ N _ N _ N _ N])
    subgoal using ket_pre_dim by auto
    subgoal using exH_n_dim by auto
    apply (subst hermitian_exH_n[simplified hermitian_def])
    using exH_k_mult_pre_is_psi by auto
  have eq3: "exH_n * (2 ⋅⇩m pre) * exH_n = 2 ⋅⇩m (exH_n * pre * exH_n)"
    using pre_dim exH_n_dim by (mat_assoc N)
  have "exH_n * (2 ⋅⇩m pre - 1⇩m N) * exH_n = exH_n * (2 ⋅⇩m pre) * exH_n - exH_n * exH_n"
    using pre_dim exH_n_dim apply (mat_assoc N) by auto
  also have "… = 2 ⋅⇩m (exH_n * pre * exH_n) - 1⇩m N"
    using eq1 eq3 by auto
  finally have eq4: "exH_n * (2 ⋅⇩m pre - 1⇩m N) * exH_n = 2 ⋅⇩m proj_psi - 1⇩m N" using eq2 by auto
  show "tensor_P (exH_n * (2 ⋅⇩m pre - 1⇩m N) * exH_n) (1⇩m K) = 2 ⋅⇩m tensor_P proj_psi (1⇩m K) - 1⇩m d"
    unfolding eq4 unfolding ps2_P.ptensor_mat_def 
    apply (subst ps_P.tensor_mat_minus1)
    unfolding ps_P_d1 ps_P_d2 apply (auto simp add: proj_psi_dim)
    apply (subst ps_P.tensor_mat_scale1)
    unfolding ps_P_d1 ps_P_d2 apply (auto simp add: proj_psi_dim)
    apply (subst ps_P.tensor_mat_id[simplified ps_P_d1 ps_P_d2 ps_P_d]) by auto
qed

lemma hermitian_proj_psi_minus_1:
  "hermitian (2 ⋅⇩m proj_psi - 1⇩m N)"
  unfolding hermitian_def
  apply (subst adjoint_minus[of _ N N])
    apply (auto simp add: proj_psi_dim)
  apply (subst adjoint_scale)
  using hermitian_proj_psi[simplified hermitian_def] hermitian_def adjoint_one by auto

lemma unitary_proj_psi_minus_1:
  "unitary (2 ⋅⇩m proj_psi - 1⇩m N)"
proof -
  have a: "adjoint (2 ⋅⇩m proj_psi) = 2 ⋅⇩m proj_psi" 
    apply (subst adjoint_scale) using hermitian_proj_psi[simplified hermitian_def] by simp
  have eq: "adjoint (2 ⋅⇩m proj_psi - 1⇩m N) = 2 ⋅⇩m proj_psi - 1⇩m N"
    apply (subst adjoint_minus) using proj_psi_dim a adjoint_one by auto
  have "(2 ⋅⇩m proj_psi) * (2 ⋅⇩m proj_psi) = 4 ⋅⇩m (proj_psi * proj_psi)"
    using proj_psi_dim by auto
  also have "… = 4 ⋅⇩m proj_psi" using proj_psi_is_projection by auto
  finally have sq: "(2 ⋅⇩m proj_psi) * (2 ⋅⇩m proj_psi) = 4 ⋅⇩m proj_psi".
  have l: "(2 ⋅⇩m proj_psi) * (2 ⋅⇩m proj_psi - 1⇩m N) = 4 ⋅⇩m proj_psi - (2 ⋅⇩m proj_psi)"
    apply (subst mult_minus_distrib_mat) using proj_psi_dim sq by auto

  have "(2 ⋅⇩m proj_psi - 1⇩m N) * adjoint (2 ⋅⇩m proj_psi - 1⇩m N)
    = (2 ⋅⇩m proj_psi - 1⇩m N) * (2 ⋅⇩m proj_psi - 1⇩m N)" using eq by auto
  also have "… = (2 ⋅⇩m proj_psi) * (2 ⋅⇩m proj_psi - 1⇩m N) - 2 ⋅⇩m proj_psi + 1⇩m N"
    apply (subst minus_mult_distrib_mat[of _ N N]) using proj_psi_dim by auto
  also have "… = 4 ⋅⇩m proj_psi - (2 ⋅⇩m proj_psi) - 2 ⋅⇩m proj_psi + 1⇩m N"
    using l by auto
  also have "… = 1⇩m N" using proj_psi_dim by auto
  finally have "(2 ⋅⇩m proj_psi - 1⇩m N) * adjoint (2 ⋅⇩m proj_psi - 1⇩m N) = 1⇩m N".
  then show ?thesis unfolding unitary_def inverts_mat_def using proj_psi_dim by auto
qed

lemma proj_psi_minus_1_mult_psi'_l:
  "(2 ⋅⇩m proj_psi - 1⇩m N) *⇩v psi'_l l = psi_l (l + 1)"
proof -
  have eq1: "(2 ⋅⇩m proj_psi - 1⇩m N) *⇩v psi'_l l = 2 ⋅⇩m proj_psi *⇩v psi'_l l - psi'_l l"
    apply (subst minus_mult_distrib_mat_vec)
    using psi'_l_dim proj_psi'_dim proj_psi_dim by auto
  have eq2: "2 ⋅⇩m proj_psi *⇩v (psi'_l l) = 2 ⋅⇩v (proj_psi *⇩v (psi'_l l))"
    apply (subst smult_mat_mult_mat_vec_assoc) 
    using proj_psi_dim psi'_l_dim by auto
  have "proj_psi *⇩v (psi'_l l) = inner_prod ψ (psi'_l l) ⋅⇩v ψ"
    unfolding proj_psi_def
    apply (subst outer_prod_mult_vec[of _ N _ N])
    using ψ_dim psi'_l_dim  by auto
  also have "… = ((alpha_l l) * ccos (θ / 2) - (beta_l l) * csin (θ / 2)) ⋅⇩v ψ"
    using psi_inner_psi'_l by auto
  finally have "proj_psi *⇩v (psi'_l l) = ((alpha_l l) * ccos (θ / 2) - (beta_l l) * csin (θ / 2)) ⋅⇩v ψ" by auto
  then have eq3: "2 ⋅⇩v (proj_psi *⇩v (psi'_l l)) = 2 * ((alpha_l l) * ccos (θ / 2) - (beta_l l) * csin (θ / 2)) ⋅⇩v ψ" by auto
  then show "(2 ⋅⇩m proj_psi - (1⇩m N)) *⇩v (psi'_l l) = psi_l (l + 1)"
    using eq1 eq2 eq3 psi_l_Suc_l_derive by simp
qed

lemma proj_psi_minus_1_mult_psi_Suc_l:
  "(2 ⋅⇩m proj_psi - 1⇩m N) *⇩v psi_l (l + 1) = psi'_l l"
proof -
  have id: "(2 ⋅⇩m proj_psi - 1⇩m N) * (2 ⋅⇩m proj_psi - 1⇩m N) = 1⇩m N"
    using unitary_proj_psi_minus_1 unfolding unitary_def hermitian_proj_psi_minus_1[simplified hermitian_def]
    unfolding inverts_mat_def by auto
  have "(2 ⋅⇩m proj_psi - 1⇩m N) *⇩v psi_l (l + 1) = (2 ⋅⇩m proj_psi - 1⇩m N) *⇩v ((2 ⋅⇩m proj_psi - 1⇩m N) *⇩v psi'_l l)"
    using proj_psi_minus_1_mult_psi'_l by auto
  also have "… = ((2 ⋅⇩m proj_psi - 1⇩m N) * (2 ⋅⇩m proj_psi - 1⇩m N) *⇩v psi'_l l)"
    apply (subst assoc_mult_mat_vec) using proj_psi_dim psi'_l_dim by auto
  also have "… = psi'_l l" using psi'_l_dim id by auto
  finally show ?thesis by auto
qed

lemma exproj_psi_minus_1_tensor:
  "(2 ⋅⇩m tensor_P proj_psi (1⇩m K)) - 1⇩m d = tensor_P (2 ⋅⇩m proj_psi - (1⇩m N)) (1⇩m K)"
  unfolding ps2_P.ptensor_mat_def
  apply (subst ps_P.tensor_mat_id[symmetric, simplified ps_P_d])
  apply (auto simp add: ps_P_d1 ps_P_d2)
  apply (subst ps_P.tensor_mat_scale1[symmetric])
    apply (auto simp add: ps_P_d1 ps_P_d2 proj_psi_dim)
  apply (subst ps_P.tensor_mat_minus1)
  by (auto simp add: ps_P_d1 ps_P_d2 proj_psi_dim)

lemma unitary_exproj_psi_minus_1:
  "unitary (2 ⋅⇩m tensor_P proj_psi (1⇩m K) - 1⇩m d)"
  unfolding exproj_psi_minus_1_tensor
  unfolding ps2_P.ptensor_mat_def 
  apply (subst ps_P.tensor_mat_unitary)
  using ps_P_d1 ps_P_d2 unitary_proj_psi_minus_1 unitary_one by auto

lemma proj_psi_minus_1_Q2:
  "adjoint (2 ⋅⇩m tensor_P proj_psi (1⇩m K) - 1⇩m d) * Q2 * (2 ⋅⇩m tensor_P proj_psi (1⇩m K) - 1⇩m d) = Q1"
proof -
  have eq1: "adjoint (2 ⋅⇩m tensor_P proj_psi (1⇩m K) - 1⇩m d) = 2 ⋅⇩m tensor_P proj_psi (1⇩m K) - 1⇩m d"
    apply (subst adjoint_minus[of _ d d])
    subgoal using tensor_P_dim[of proj_psi] by auto
    subgoal by auto
    apply (subst adjoint_one) apply (subst adjoint_scale) 
    using hermitian_exproj_psi[simplified hermitian_def] by auto
  let ?m1 = "tensor_P (2 ⋅⇩m proj_psi - (1⇩m N)) (1⇩m K)"
  {
    fix l
    let ?m2 = "tensor_P (proj_psi_l (l + 1)) (proj_k l)"
    have 121: "?m1 * ?m2 * ?m1 
        = tensor_P ((2 ⋅⇩m proj_psi - (1⇩m N)) * (proj_psi_l (l + 1)) * (2 ⋅⇩m proj_psi - (1⇩m N)))
            (proj_k l)"
      apply (subst tensor_P_left_right_partial1)
      using proj_psi_dim proj_psi_l_dim proj_k_dim by auto
    have "(2 ⋅⇩m proj_psi - (1⇩m N)) * (proj_psi_l (l + 1)) * (2 ⋅⇩m proj_psi - (1⇩m N))
      = outer_prod ((2 ⋅⇩m proj_psi - (1⇩m N)) *⇩v (psi_l (l + 1))) ((2 ⋅⇩m proj_psi - (1⇩m N)) *⇩v (psi_l (l + 1)))"
      unfolding proj_psi_l_def apply (subst outer_prod_left_right_mat[of _ N _ N _ N _ N])
      using proj_psi_dim psi_l_dim hermitian_proj_psi_minus_1[simplified hermitian_def] by auto
    also have "… = outer_prod (psi'_l l) (psi'_l l)"
      using proj_psi_minus_1_mult_psi_Suc_l by auto
    finally have "(2 ⋅⇩m proj_psi - (1⇩m N)) * (proj_psi_l (l + 1)) * (2 ⋅⇩m proj_psi - (1⇩m N)) 
      = outer_prod (psi'_l l) (psi'_l l)".
    then have "?m1 * ?m2 * ?m1 = tensor_P (proj_psi'_l l) (proj_k l)"
      using 121 proj_psi'_l_def by auto
  }
  note p1 = this
  have "adjoint (2 ⋅⇩m tensor_P proj_psi (1⇩m K) - 1⇩m d) * Q2 * (2 ⋅⇩m tensor_P proj_psi (1⇩m K) - 1⇩m d)
    = (2 ⋅⇩m tensor_P proj_psi (1⇩m K) - 1⇩m d) * Q2 * (2 ⋅⇩m tensor_P proj_psi (1⇩m K) - 1⇩m d)"
    using eq1 by auto
  also have "… = matrix_sum d
    (λl. (2 ⋅⇩m tensor_P proj_psi (1⇩m K) - 1⇩m d) * tensor_P (proj_psi_l (l + 1)) (proj_k l) * (2 ⋅⇩m tensor_P proj_psi (1⇩m K) - 1⇩m d))
    R" unfolding Q2_def apply (subst matrix_sum_mult_left_right)
    using tensor_P_dim by auto
  also have "… = matrix_sum d (λl. tensor_P (proj_psi'_l l) (proj_k l)) R"
    using p1 exproj_psi_minus_1_tensor by auto
  also have "… = Q1" unfolding Q1_def by auto
  finally show ?thesis using eq1 by auto
qed

lemma qp_Q1:
  "is_quantum_predicate Q1"
  unfolding proj_psi_minus_1_Q2[symmetric]
  apply (subst qp_close_under_unitary_operator)
  using tensor_P_dim unitary_exproj_psi_minus_1 qp_Q2 by auto

lemma qp_Q:
  "is_quantum_predicate Q"
proof -
  have u: "unitary (tensor_P mat_O (1⇩m K))"
    unfolding ps2_P.ptensor_mat_def
    apply (subst ps_P.tensor_mat_unitary)
    subgoal unfolding ps_P_d1 mat_O_def by auto
    subgoal unfolding ps_P_d2 by auto
    subgoal using unitary_mat_O by auto
    using unitary_one by auto
  then show ?thesis using tensor_P_dim qp_Q1 
    using qp_close_under_unitary_operator[OF tensor_P_dim u qp_Q1]
    by (simp add: mat_O_times_Q1 )
qed

lemma hoare_triple_D1:
  "⊢⇩p 
   {Q} 
   Utrans_P vars1 mat_O
   {Q1}"
  unfolding Utrans_P_is_tensor_P1
    mat_O_times_Q1[symmetric]
  apply (subst hoare_partial.intros(2))
  using qp_Q1 by auto

lemma hoare_triple_D2:
  "⊢⇩p 
   {Q1}
   hadamard_n n ;;
   Utrans_P vars1 mat_Ph ;;
   hadamard_n n 
   {Q2}"
proof -
  let ?H = "exexH_k (n - 1)"
  let ?Ph = "tensor_P mat_Ph (1⇩m K)"
  let ?O = "tensor_P mat_O (1⇩m K)"
  have h1: "⊢⇩p 
    {adjoint ?H * Q2 * ?H} 
    hadamard_n n 
    {Q2}"
    using hoare_hadamard_n[OF qp_Q2, of "n - 1"] n by auto
  have qp1: "is_quantum_predicate ((adjoint ?H) * Q2 * ?H)"
    using qp_close_under_unitary_operator unitary_exexH_k n exexH_k_dim qp_Q2 by auto
  then have h2: "⊢⇩p 
    {adjoint ?Ph * (adjoint ?H * Q2 * ?H) * ?Ph} 
    Utrans_P vars1 mat_Ph 
    {adjoint ?H * Q2 * ?H}"
    using qp1 Utrans_P_is_tensor_P1 hoare_partial.intros by auto
  have qp2: "is_quantum_predicate (adjoint ?Ph * (adjoint ?H * Q2 * ?H) * ?Ph)"
    using qp_close_under_unitary_operator[of "tensor_P mat_Ph (1⇩m K)"] ps2_P.ptensor_mat_carrier ps2_P_d0 unitary_ex_mat_Ph qp1 by auto
  then have  h3: "⊢⇩p 
    {adjoint ?H * (adjoint ?Ph * (adjoint ?H * Q2 * ?H) * ?Ph) * ?H} 
    hadamard_n n 
    {adjoint ?Ph * (adjoint ?H * Q2 * ?H) * ?Ph}"
    using hoare_hadamard_n[OF qp2, of "n - 1"] n by auto
  have qp3: "is_quantum_predicate (adjoint ?H * (adjoint ?Ph * (adjoint ?H * Q2 * ?H) * ?Ph) * ?H)"
    using qp_close_under_unitary_operator[of "?H"] exexH_k_dim unitary_exexH_k qp2 n by auto
  have h4: "⊢⇩p 
    {adjoint ?H * (adjoint ?Ph * (adjoint ?H * Q2 * ?H) * ?Ph) * ?H} 
    hadamard_n n ;;
    Utrans_P vars1 mat_Ph
    {adjoint ?H * Q2 * ?H}"
    using h2 h3 qp1 qp2 qp3 hoare_partial.intros by auto
  then have h5: "⊢⇩p 
   {adjoint ?H * (adjoint ?Ph * (adjoint ?H * Q2 * ?H) * ?Ph) * ?H}
   hadamard_n n ;;
   Utrans_P vars1 mat_Ph ;;
   hadamard_n n 
   {Q2}"
    using h1 qp_Q2 qp3 qp1 hoare_partial.intros(3)[OF qp3 qp1 qp_Q2 h4 h1] by auto

  have "adjoint ?H * (adjoint ?Ph * (adjoint ?H * Q2 * ?H) * ?Ph) * ?H =
        adjoint (?H * ?Ph * ?H) * Q2 * (?H * ?Ph * ?H)"
    apply (mat_assoc d) using exexH_k_dim n tensor_P_dim Q2_dim by auto
  also have "… = Q1" using H_Ph_H proj_psi_minus_1_Q2 by auto
  finally show ?thesis using h5 by auto 
qed

definition exM0 where
  "exM0 = tensor_P (1⇩m N) M0"

lemma M0_mult_ket_k_R:
  "M0 *⇩v ket_k R = ket_k R"
  apply (rule eq_vecI)
  unfolding M0_def ket_k_def
  by (auto simp add: scalar_prod_def sum_only_one_neq_0)

lemma exP0_P':
  "adjoint exM0 * P' * exM0 = P'"
proof -
  have eq: "adjoint exM0 = exM0"
    unfolding exM0_def ps2_P.ptensor_mat_def 
    apply (subst ps_P.tensor_mat_adjoint)
    unfolding ps_P_d1 ps_P_d2 using M0_dim adjoint_one hermitian_M0[unfolded hermitian_def] by auto
  have eq2: "M0 * (proj_k R) * M0 = (proj_k R)"
    unfolding proj_k_def
    apply (subst outer_prod_left_right_mat[of _ K _ K _ K _ K])
    unfolding hermitian_M0[unfolded hermitian_def] M0_mult_ket_k_R
    using ket_k_dim M0_dim by auto
  show ?thesis unfolding eq unfolding exM0_def P'_def
    apply (subst tensor_P_left_right_partial2)
    using M0_dim proj_k_dim eq2 proj_psi_l_dim by auto
qed
 
definition exM1 where
  "exM1 = tensor_P (1⇩m N) M1"

lemma M1_mult_ket_k:
  assumes "k < R"
  shows "M1 *⇩v ket_k k = ket_k k"
  apply (rule eq_vecI)
  unfolding M1_def ket_k_def
  by (auto simp add: scalar_prod_def assms R sum_only_one_neq_0)

lemma exP1_Q:
  "adjoint exM1 * Q * exM1 = Q"
proof -
  have eq: "adjoint exM1 = exM1"
    unfolding exM1_def ps2_P.ptensor_mat_def 
    apply (subst ps_P.tensor_mat_adjoint)
    unfolding ps_P_d1 ps_P_d2 using M1_dim adjoint_one hermitian_M1[unfolded hermitian_def] by auto
  {
    fix k assume k: "k < R"
    let ?m = "tensor_P (proj_psi_l k) (proj_k k)"
    have "exM1 * ?m * exM1 = tensor_P (proj_psi_l k) (M1 * (proj_k k) * M1)"
      unfolding exM1_def apply (subst tensor_P_left_right_partial2)
      using M1_dim proj_k_dim proj_psi_l_dim by auto
    also have "… = tensor_P (proj_psi_l k) (outer_prod (M1 *⇩v ket_k k) (M1 *⇩v ket_k k))"
      unfolding proj_k_def apply (subst outer_prod_left_right_mat[of _ K _ K _ K _ K])
      unfolding hermitian_M1[unfolded hermitian_def]
      using ket_k_dim M1_dim by auto
    finally have "exM1 * ?m * exM1 = ?m" unfolding proj_k_def using k M1_mult_ket_k by auto
  }
  note p1 = this
  have "adjoint exM1 * Q * exM1 = exM1 * Q * exM1" using eq by auto
  also have "… = matrix_sum d (λk. exM1 * (tensor_P (proj_psi_l k) (proj_k k)) * exM1) R"
    unfolding Q_def
    apply (subst matrix_sum_mult_left_right)
    using tensor_P_dim exM1_def by auto
  also have "… = matrix_sum d (λk. tensor_P (proj_psi_l k) (proj_k k)) R"
    apply (subst matrix_sum_cong)
    using p1 by auto
  finally show ?thesis using Q_def by auto
qed
         
lemma qp_P':
  "is_quantum_predicate P'"
  unfolding is_quantum_predicate_def
proof (intro conjI)
  show "P' ∈ carrier_mat d d" unfolding P'_def using tensor_P_dim by auto
  show "positive P'" unfolding P'_def ps2_P.ptensor_mat_def
    apply (subst ps_P.tensor_mat_positive)
        apply (auto simp add: ps_P_d1 ps_P_d2 proj_O_dim proj_k_dim)
    using proj_psi_l_dim positive_proj_psi_l positive_proj_k K by auto
  show "P' ≤⇩L 1⇩m d" unfolding P'_def ps2_P.ptensor_mat_def
    apply (subst ps_P.tensor_mat_le_one[simplified ps_P_d])
    by (auto simp add: ps_P_d1 ps_P_d2 proj_psi_l_dim K proj_k_dim positive_proj_psi_l positive_proj_k proj_k_le_one psi_l_le_id)
qed

lemma P'_add_Q:
  "P' + Q = matrix_sum d (λl. tensor_P (proj_psi_l l) (proj_k l)) (R + 1)"
  apply simp unfolding P'_def Q_def by auto

lemma positive_Qk:
  "positive (tensor_P (proj_psi_l l) (proj_k l))"
  unfolding ps2_P.ptensor_mat_def 
  apply (subst ps_P.tensor_mat_positive)
  unfolding ps_P_d1 ps_P_d2
  using proj_psi_l_dim proj_k_dim positive_proj_psi_l positive_proj_k by auto

lemma P'_Q_dim:
  "P' + Q ∈ carrier_mat d d"
  unfolding P'_add_Q
  apply (subst matrix_sum_dim)
  using tensor_P_dim by auto

lemma P'_add_Q_le_one:
  "P' + Q ≤⇩L 1⇩m d" 
proof -
  have leq: "matrix_sum d (λl. tensor_P (proj_psi_l l) (proj_k l)) (R + 1) 
      ≤⇩L matrix_sum d (λk. tensor_P (1⇩m N) (proj_k k)) (R + 1)"
    unfolding Q2_def
    apply (subst lowner_le_matrix_sum)
    subgoal using tensor_P_dim by auto
    subgoal using tensor_P_dim by auto
    using proj_psi_proj_k_le_exproj_k by auto
  have "matrix_sum d (λk. tensor_P (1⇩m N) (proj_k k)) (R + 1)
      = tensor_P (1⇩m N) (matrix_sum K proj_k (R + 1))"
    unfolding ps2_P.ptensor_mat_def
    apply (subst ps_P.tensor_mat_matrix_sum2[simplified ps_P_d ps_P_d2])
    subgoal using ps_P_d1 by auto
    using proj_k_dim by auto
  also have "… = tensor_P (1⇩m N) (proj_fst_k (R + 1))" using sum_proj_k[of "R + 1"] K by auto
  also have "… ≤⇩L tensor_P (1⇩m N) (1⇩m K)" unfolding ps2_P.ptensor_mat_def
    apply (subst ps_P.tensor_mat_positive_le)
    subgoal using ps_P_d1 by auto
    subgoal using ps_P_d2 proj_fst_k_def by auto
    subgoal using positive_one by auto
    subgoal using positive_proj_fst_k  by auto
    subgoal using lowner_le_refl[of "1⇩m N" N] by auto
    using proj_fst_k_le_one by auto
  also have "… = 1⇩m d" unfolding ps2_P.ptensor_mat_def
    using ps_P.tensor_mat_id ps_P_d1 ps_P_d2 ps_P_d by auto
  finally have leq2: "matrix_sum d (λk. tensor_P (1⇩m N) (proj_k k)) (R + 1) ≤⇩L 1⇩m d" by auto
  have ds: "matrix_sum d (λk. tensor_P (1⇩m N) (proj_k k)) (R + 1) ∈ carrier_mat d d"
    apply (subst matrix_sum_dim) using tensor_P_dim by auto
  then show ?thesis 
   using leq leq2 lowner_le_trans[OF P'_Q_dim ds, of "1⇩m d"] unfolding P'_add_Q by auto
qed

lemma qp_P'_Q:
  "is_quantum_predicate (P' + Q)"
  unfolding is_quantum_predicate_def
proof (intro conjI)
  show "P' + Q ∈ carrier_mat d d"
    unfolding P'_add_Q apply (subst matrix_sum_dim)
    using tensor_P_dim by auto
  show "positive (P' + Q)" unfolding P'_add_Q
    apply (subst matrix_sum_positive)
    using tensor_P_dim positive_Qk by auto
  show " P' + Q ≤⇩L 1⇩m d" using P'_add_Q_le_one by auto
qed

lemma Q2_leq_lemma:
  "tensor_P (1⇩m N) (mat_incr K) * Q2 * adjoint (tensor_P (1⇩m N) (mat_incr K)) ≤⇩L P' + Q"
proof -
  have ad: "adjoint (tensor_P (1⇩m N) (mat_incr K)) = tensor_P (1⇩m N) (adjoint (mat_incr K))"
    unfolding ps2_P.ptensor_mat_def apply (subst ps_P.tensor_mat_adjoint)
    using ps_P_d1 ps_P_d2 mat_incr_dim adjoint_one by auto
  let ?m1 = "tensor_P (1⇩m N) (mat_incr K)"
  let ?m3 = "tensor_P (1⇩m N) (adjoint (mat_incr K))"
  {
    fix l assume "l < R"
    then have "l < K - 1" using K by auto
    then have m: "(mat_incr K) *⇩v (ket_k l) = (ket_k (l + 1))"
      using mat_incr_mult_ket_k by auto
    let ?m2 = "tensor_P (proj_psi_l (l + 1)) (proj_k l)"
    have eq: "?m1 * ?m2 * ?m3 = tensor_P (proj_psi_l (l + 1)) ((mat_incr K) * (proj_k l) * adjoint (mat_incr K))"
      apply (subst tensor_P_left_right_partial2)
      using proj_k_dim proj_psi_l_dim mat_incr_dim adjoint_dim[OF mat_incr_dim] by auto
    have "(mat_incr K) * (proj_k l) * adjoint (mat_incr K) = outer_prod ((mat_incr K) *⇩v (ket_k l)) ((mat_incr K) *⇩v (ket_k l))"
      unfolding proj_k_def apply (subst outer_prod_left_right_mat[of _ K _ K _ K _ K])
      using ket_k_dim mat_incr_dim adjoint_dim[OF mat_incr_dim] adjoint_adjoint[of "mat_incr K"] by auto
    also have "… = proj_k (l + 1)" unfolding proj_k_def using m by auto
    finally have "?m1 * ?m2 * ?m3 = tensor_P (proj_psi_l (l + 1)) (proj_k (l + 1))" using eq by auto
  }
  note p1 = this
  have "?m1 * Q2 * ?m3
    = matrix_sum d (λl. ?m1 * (tensor_P (proj_psi_l (l + 1)) (proj_k l)) * ?m3) R"
    unfolding Q2_def apply(subst matrix_sum_mult_left_right)
    using tensor_P_dim by auto
  also have "… = matrix_sum d (λl. tensor_P (proj_psi_l (l + 1)) (proj_k (l + 1))) R"
    apply (subst matrix_sum_cong) using p1 by auto
  finally have eq1: "?m1 * Q2 * ?m3 = matrix_sum d (λl. tensor_P (proj_psi_l (l + 1)) (proj_k (l + 1))) R" (is "_=?r") . 
  have eq2: "P' + Q = tensor_P (proj_psi_l 0) (proj_k 0) + ?r"
    unfolding P'_add_Q
    apply (subst matrix_sum_Suc_remove_head) using tensor_P_dim by auto
  have "tensor_P (proj_psi_l 0) (proj_k 0) + ?r ≤⇩L P' + Q"
    unfolding eq2[symmetric] apply (subst lowner_le_refl) using P'_Q_dim by auto
  moreover have "positive (tensor_P (proj_psi_l 0) (proj_k 0))"
    unfolding ps2_P.ptensor_mat_def apply (subst ps_P.tensor_mat_positive)
    unfolding ps_P_d1 ps_P_d2 using proj_psi_l_dim proj_k_dim positive_proj_psi_l positive_proj_k by auto
  moreover have "matrix_sum d (λl. tensor_P (proj_psi_l (l + 1)) (proj_k (l + 1))) R ∈ carrier_mat d d"
    apply (subst matrix_sum_dim) using tensor_P_dim by auto
  ultimately have "?r ≤⇩L P' + Q"
    apply (subst add_positive_le_reduce2[of ?r d "tensor_P (proj_psi_l 0) (proj_k 0)" "P' + Q"])
    using tensor_P_dim P'_Q_dim by auto
  then show ?thesis using eq1 ad by auto
qed

lemma Q2_leq:
  "Q2 ≤⇩L adjoint (tensor_P (1⇩m N) (mat_incr K)) * (P' + Q) * tensor_P (1⇩m N) (mat_incr K)"
proof -
  let ?m1 = "tensor_P (1⇩m N) (mat_incr K)"
  let ?m2 = "adjoint (tensor_P (1⇩m N) (mat_incr K))"
  have "?m1 * ?m2 = 1⇩m d"
    unfolding ps2_P.ptensor_mat_def
    apply (subst ps_P.tensor_mat_adjoint)
    unfolding ps_P_d1 ps_P_d2 apply (auto simp add: mat_incr_dim adjoint_one)
    apply (subst ps_P.tensor_mat_mult[symmetric])
    unfolding ps_P_d1 ps_P_d2 apply (auto simp add: mat_incr_dim adjoint_dim mat_incr_mult_adjoint_mat_incr)
    using ps_P.tensor_mat_id ps_P_d ps_P_d1 ps_P_d2 by auto
  then have inv: "?m2 * ?m1 = 1⇩m d"
    using mat_mult_left_right_inverse[of ?m1 d ?m2] 
        tensor_P_dim adjoint_dim by auto
  have d: "?m1 * Q2 * ?m2 ∈ carrier_mat d d" using tensor_P_dim adjoint_dim[OF tensor_P_dim] Q2_dim by fastforce
  have le: "?m2 * (?m1 * Q2 * ?m2) * ?m1 ≤⇩L ?m2 * (P' + Q) * ?m1" (is "lowner_le ?l ?r")
    apply (subst lowner_le_keep_under_measurement[of _ d])
    using Q2_leq_lemma tensor_P_dim P'_Q_dim d by auto
  have "?l = (?m2 * ?m1) * Q2 * (?m2 * ?m1)"
    apply (mat_assoc d) using tensor_P_dim Q2_dim by auto
  also have "… = 1⇩m d * Q2 * 1⇩m d" using inv by auto
  also have "… = Q2" using Q2_dim by auto
  finally have eq: "?l = Q2".
  show ?thesis using eq le by auto
qed

lemma hoare_triple_D3:
  "⊢⇩p 
   {Q2}
   Utrans_P vars2 (mat_incr K)
   {adjoint exM0 * P' * exM0 + adjoint exM1 * Q * exM1}"
  unfolding exP0_P' exP1_Q 
proof -
  let ?m = "tensor_P (1⇩m N) (mat_incr K)"
  have h1: "⊢⇩p 
    {adjoint ?m * (P' + Q) * ?m} 
    Utrans ?m
    {P' + Q}"
    using qp_P'_Q hoare_partial.intros by auto
  have qp: "is_quantum_predicate (adjoint ?m * (P' + Q) * ?m)"
    using qp_close_under_unitary_operator tensor_P_dim qp_P'_Q unitary_exmat_incr by auto
  then have "⊢⇩p 
    {Q2} 
    Utrans ?m
    {P' + Q}"
    using hoare_partial.intros(6)[OF qp_Q2 qp_P'_Q qp qp_P'_Q] Q2_leq h1 lowner_le_refl[OF P'_Q_dim] by auto
  moreover have "Utrans ?m = Utrans_P vars2 (mat_incr K)"
    apply (subst Utrans_P_is_tensor_P2) unfolding mat_incr_def by auto
  ultimately show "⊢⇩p {Q2} Utrans_P vars2 (mat_incr K) {P' + Q}" by auto
qed

lemma qp_D3_post:
  "is_quantum_predicate (adjoint exM0 * P' * exM0 + adjoint exM1 * Q * exM1)"
  unfolding exP0_P' exP1_Q using qp_P'_Q by auto

lemma hoare_triple_D:
  "⊢⇩p 
   {Q} 
   D
   {adjoint exM0 * P' * exM0 + adjoint exM1 * Q * exM1}"
proof -
  have "⊢⇩p {Q1} hadamard_n n;; (Utrans_P vars1 mat_Ph;; hadamard_n n) {Q2}"
    using  well_com_hadamard_n well_com_mat_Ph hoare_triple_D2 qp_Q1 qp_Q2 by (auto simp add: hoare_patial_seq_assoc)
  then have "⊢⇩p {Q} Utrans_P vars1 mat_O;; (hadamard_n n;; (Utrans_P vars1 mat_Ph;; hadamard_n n)) {Q2}"
    using hoare_triple_D1 qp_Q qp_Q1 qp_Q2 hoare_partial.intros(3) by auto
  moreover have "well_com (Utrans_P vars1 mat_Ph;; hadamard_n n)" using well_com_hadamard_n well_com_mat_Ph by auto
  ultimately have "⊢⇩p {Q} (Utrans_P vars1 mat_O;; hadamard_n n);; (Utrans_P vars1 mat_Ph;; hadamard_n n) {Q2}"
    using well_com_hadamard_n well_com_mat_O qp_Q qp_Q2 by (auto simp add: hoare_patial_seq_assoc)
  moreover have "well_com (Utrans_P vars1 mat_O;; hadamard_n n)"
    using well_com_mat_O well_com_hadamard_n by auto
  ultimately have "⊢⇩p {Q} Utrans_P vars1 mat_O;; hadamard_n n;; Utrans_P vars1 mat_Ph;; hadamard_n n {Q2}"
    using well_com_hadamard_n well_com_mat_Ph qp_Q qp_Q2 by (auto simp add: hoare_patial_seq_assoc)
  with qp_Q qp_Q2 qp_D3_post hoare_triple_D3 show "⊢⇩p 
   {Q} 
   D
   {adjoint exM0 * P' * exM0 + adjoint exM1 * Q * exM1}"
    unfolding D_def using hoare_partial.intros(3) by auto
qed

lemma psi_is_psi_l0:
  "ψ = psi_l 0"
  unfolding ψ_eq psi_l_def alpha_l_def beta_l_def by auto

lemma proj_psi_is_proj_psi_l0:
  "proj_psi = proj_psi_l 0"
  unfolding proj_psi_def psi_is_psi_l0 proj_psi_l_def by auto

lemma lowner_le_Q:
  "tensor_P proj_psi (proj_k 0) ≤⇩L adjoint exM0 * P' * exM0 + adjoint exM1 * Q * exM1"
proof -
  let ?r = "matrix_sum d (λl. tensor_P (proj_psi_l l) (proj_k l)) (R + 1)"
  let ?l = "tensor_P (proj_psi_l 0) (proj_k 0)"
  have eq: "?r = ?l + matrix_sum d (λl. tensor_P (proj_psi_l (l + 1)) (proj_k (l + 1))) R" (is "_ = _ + ?s")
    apply (subst matrix_sum_Suc_remove_head)
    using tensor_P_dim by auto
  have d: "?s ∈ carrier_mat d d"
    apply (subst matrix_sum_dim) using tensor_P_dim by auto
  have pt: "positive (tensor_P (proj_psi_l l) (proj_k l))" for l
    unfolding ps2_P.ptensor_mat_def apply (subst ps_P.tensor_mat_positive)
    unfolding ps_P_d1 ps_P_d2 using proj_psi_l_dim proj_k_dim positive_proj_psi_l positive_proj_k by auto
  have ps: "positive ?s"
    apply (subst matrix_sum_positive) 
    subgoal using tensor_P_dim by auto
    using pt by auto
  have "?l ≤⇩L ?r"
    unfolding eq
    apply (subst add_positive_le_reduce1[of ?l d ?s])
    subgoal using tensor_P_dim by auto
    subgoal using d by auto
    subgoal using tensor_P_dim d by auto
    subgoal using ps by auto
     apply (subst lowner_le_refl[of _ d])
    using tensor_P_dim d by auto
  then show ?thesis unfolding exP0_P' exP1_Q P'_add_Q proj_psi_is_proj_psi_l0  by auto
qed

lemma hoare_triple_while:
  "⊢⇩p 
   {adjoint exM0 * P' * exM0 + adjoint exM1 * Q * exM1} 
   While_P vars2 M0 M1 D
   {P'}"
proof -
  let ?m = "λ(n::nat). if n = 0 then mat_extension dims vars2 M0 else
                       if n = 1 then mat_extension dims vars2 M1 else undefined"
  have dM0: "M0 ∈ carrier_mat K K" unfolding M0_def by auto
  have dM1: "M1 ∈ carrier_mat K K" unfolding M1_def by auto
  have m0: "?m 0 = exM0" apply (simp) unfolding exM0_def ps2_P.ptensor_mat_def mat_ext_vars2[OF dM0] by auto
  have m1: "?m 1 = exM1" unfolding exM1_def ps2_P.ptensor_mat_def mat_ext_vars2[OF dM1] by auto
  have "⊢⇩p {Q} D {adjoint (?m 0) * P' * (?m 0) + adjoint (?m 1) * Q * (?m 1)}"
    using hoare_triple_D m0 m1 by auto
  then show ?thesis unfolding While_P_def using qp_D3_post qp_P' hoare_partial.intros(5)[OF qp_P' qp_Q, of D ?m] m0 m1 by auto
qed

lemma R_and_a_half_θ:
  "(R + 1/2) * θ = pi / 2"
  using R θ_neq_0 by auto

lemma psi_lR_is_beta:
  "psi_l R = β"
  unfolding psi_l_def alpha_l_def beta_l_def R_and_a_half_θ by auto

lemma post_mult_beta:
  "post *⇩v β = β"
  by (auto simp add: post_def β_def scalar_prod_def sum_only_one_neq_0)

lemma post_mult_post:
  "post * post = post"
  by (auto simp add: post_def scalar_prod_def sum_only_one_neq_0)

lemma post_mult_proj_psi_lR:
  "post * proj_psi_l R = proj_psi_l R"
proof -
  let ?R = "proj_psi_l R"
  have "post * ?R = post * ?R * 1⇩m N"
    using post_dim proj_psi_l_dim[of R] by auto
  also have "… = outer_prod (post *⇩v psi_l R) ((1⇩m N) *⇩v psi_l R)"
    unfolding proj_psi_l_def
    apply (subst outer_prod_left_right_mat[of _ N _ N _ N _ N])
    by (auto simp add: psi_l_dim post_dim adjoint_one)
  also have "… = ?R" unfolding proj_psi_l_def unfolding psi_lR_is_beta unfolding post_mult_beta
    using β_dim by auto
  finally show "post * ?R = ?R".
qed

lemma proj_psi_lR_mult_post:
  "proj_psi_l R * post = proj_psi_l R"
proof -
  let ?R = "proj_psi_l R"
  have "?R * post = 1⇩m N * ?R * post"
    using post_dim proj_psi_l_dim[of R] by auto
  also have "… = outer_prod ((1⇩m N) *⇩v psi_l R) (post *⇩v psi_l R)"
    unfolding proj_psi_l_def
    apply (subst outer_prod_left_right_mat[of _ N _ N _ N _ N])
    by (auto simp add: psi_l_dim post_dim hermitian_post[unfolded hermitian_def])
  also have "… = ?R" unfolding proj_psi_l_def unfolding psi_lR_is_beta unfolding post_mult_beta
    using β_dim by auto
  finally show "?R * post = ?R".
qed

lemma proj_psi_lR_mult_proj_psi_lR:
  "proj_psi_l R * proj_psi_l R = proj_psi_l R"
  unfolding proj_psi_l_def psi_lR_is_beta
  apply (subst outer_prod_mult_outer_prod[of _ N _ N _ _ N])
  by (auto simp add: β_inner)

lemma proj_psi_lR_le_post:
  "proj_psi_l R ≤⇩L post"
proof -
  let ?R = "proj_psi_l R"
  let ?s = "post - ?R"
  have eq1: "post * (post - ?R) = post - ?R"
    apply (subst mult_minus_distrib_mat[of _ N N _ N])
      apply (auto simp add: post_dim proj_psi_l_dim[of R])
    using post_mult_post post_mult_proj_psi_lR by auto
  have eq2: "?R * (post - ?R) = 0⇩m N N"
    apply (subst mult_minus_distrib_mat[of _ N N _ N])
      apply (auto simp add: post_dim proj_psi_l_dim[of R])
    unfolding proj_psi_lR_mult_post proj_psi_lR_mult_proj_psi_lR 
    using proj_psi_l_dim[of R] by auto
  have "adjoint ?s = ?s"
    apply (subst adjoint_minus[of _ N N])
    using post_dim proj_psi_l_dim hermitian_post hermitian_proj_psi_l K by (auto simp add: hermitian_def)
  then have "?s * adjoint ?s = ?s * ?s" by auto
  also have "… = post * (post - ?R) - ?R * (post - ?R)"
    using post_dim proj_psi_l_dim[of R] by (mat_assoc N)
  also have "… = post - ?R"
    unfolding eq1 eq2 using post_dim proj_psi_l_dim[of R] by auto
  finally have "?s * adjoint ?s = ?s". 
  then have "∃M. M * adjoint M = ?s" by auto
  then have "positive ?s" apply (subst positive_if_decomp[of ?s N]) using post_dim proj_psi_l_dim[of R] by auto
  then show ?thesis unfolding lowner_le_def using post_dim proj_psi_l_dim[of R] by auto
qed

lemma P'_le_post_R:
  "P' ≤⇩L (tensor_P post (proj_k R))"
proof -
  let ?r = "tensor_P post (proj_k R)"
  have "?r - P' = tensor_P (post - proj_psi_l R) (proj_k R)"
    unfolding P'_def ps2_P.ptensor_mat_def
    apply (subst ps_P.tensor_mat_minus1)
    unfolding ps_P_d1 ps_P_d2
    using post_dim proj_psi_l_dim proj_k_dim by auto
  moreover have "positive (tensor_P (post - proj_psi_l R) (proj_k R))"
    unfolding ps2_P.ptensor_mat_def
    apply (subst ps_P.tensor_mat_positive)
    unfolding ps_P_d1 ps_P_d2 
    using proj_psi_lR_le_post[unfolded lowner_le_def]
      post_dim proj_psi_l_dim[of R] proj_k_dim positive_proj_k
    by auto
  ultimately show "P' ≤⇩L ?r"
    unfolding lowner_le_def P'_def
    using tensor_P_dim by auto
qed

lemma positive_post:
  "positive post"
proof -
  have ad: "adjoint post = post" using hermitian_post[unfolded hermitian_def] by auto
  then have "post * adjoint post = post"
    unfolding ad post_mult_post by auto
  then have "∃M. M * adjoint M = post" by auto
  then show ?thesis using positive_if_decomp post_dim by auto
qed

lemma lowner_le_P':
  "P' ≤⇩L tensor_P post (1⇩m K)"
proof -
  let ?r = "tensor_P post (1⇩m K)"
  let ?m = "tensor_P post (proj_k R)"
  have "?m ≤⇩L ?r"
    unfolding ps2_P.ptensor_mat_def
    apply (subst ps_P.tensor_mat_positive_le)
    unfolding ps_P_d1 ps_P_d2
    using post_dim proj_k_dim positive_post positive_proj_k
      lowner_le_refl[of post] proj_k_le_one by auto
  then show "P' ≤⇩L ?r"
    using lowner_le_trans[of P' d ?m ?r] P'_le_post_R
    unfolding P'_def using tensor_P_dim by auto
qed

lemma post_mult_testNk:
  assumes "f k"
  shows "post * (testN k) = testN k"
  using assms by (auto simp add: post_def testN_def scalar_prod_def sum_only_one_neq_0)

lemma post_mult_testNk_neg:
  assumes "¬ f k"
  shows "post * testN k = 0⇩m N N"
  using assms by (auto simp add: post_def testN_def scalar_prod_def sum_only_one_neq_0)

lemma testN_post1:
  "f k ⟹ adjoint (testN k) * post * testN k = testN k"
  apply (subst assoc_mult_mat[of _ N N _ N _ N])
     apply (auto simp add: adjoint_dim testN_dim post_dim)
  apply (subst post_mult_testNk, simp)
  unfolding hermitian_testN[unfolded hermitian_def]
  using testN_mult_testN by auto

lemma testN_post2:
  "¬ f k ⟹ adjoint (testN k) * post * testN k = 0⇩m N N"
  apply (subst assoc_mult_mat[of _ N N _ N _ N])
     apply (auto simp add: adjoint_dim testN_dim post_dim)
  apply (subst post_mult_testNk_neg, simp)
  unfolding hermitian_testN[unfolded hermitian_def]
  using testN_dim[of k] by auto

definition post_fst_k :: "nat ⇒ complex mat" where
  "post_fst_k k = mat N N (λ(i, j). if (i = j ∧ f i ∧ i < k) then 1 else 0)"

lemma post_fst_kN:
  "post_fst_k N = post"
  unfolding post_fst_k_def post_def by auto

lemma post_fst_k_Suc:
  "f i ⟹ post_fst_k (Suc i) = testN i + post_fst_k i"
  apply (rule eq_matI)
  unfolding post_fst_k_def testN_def by auto

lemma post_fst_k_Suc_neg:
  "¬ f i ⟹ post_fst_k (Suc i) = post_fst_k i"
  apply (rule eq_matI)
  unfolding post_fst_k_def
    apply auto
  using less_antisym by fastforce

lemma testN_sum:
  "matrix_sum N (λk. adjoint (testN k) * post * testN k) N = post"
proof -
  have "m ≤ N ⟹ matrix_sum N (λk. adjoint (testN k) * post * testN k) m = post_fst_k m" for m
  proof (induct m)
    case 0
    then show ?case apply simp unfolding post_fst_k_def by auto
  next
    case (Suc m) 
    then have m: "m ≤ N" by auto
    show ?case
    proof (cases "f m")
      case True
      show ?thesis apply simp
        apply (subst testN_post1[OF True])
        apply (subst Suc(1)[OF m])
        using post_fst_k_Suc True by auto
    next
      case False
      show ?thesis apply simp
        apply (subst testN_post2[OF False])
        apply (subst Suc(1)[OF m])
        using post_fst_k_Suc_neg False post_fst_k_def by auto
    qed
  qed
  then show ?thesis using post_fst_kN by auto
qed

lemma tensor_P_testN_sum:
  "matrix_sum d (λk. adjoint (tensor_P (testN k) (1⇩m K)) * tensor_P post (1⇩m K) * tensor_P (testN k) (1⇩m K)) N =
   tensor_P post (1⇩m K)"
proof -
  have eq: "adjoint (tensor_P (testN k) (1⇩m K)) * tensor_P post (1⇩m K) * tensor_P (testN k) (1⇩m K) =
            tensor_P (adjoint (testN k) * post * (testN k)) (1⇩m K)" for k
    apply (subst tensor_P_adjoint_left_right)
    subgoal unfolding testN_def by auto
    subgoal by auto
    subgoal using post_dim by auto
    using adjoint_one by auto
  moreover have "matrix_sum N (λk. adjoint (testN k) * post * testN k) N = post"
    using testN_sum by auto
  show ?thesis unfolding eq
    apply (subst matrix_sum_tensor_P1)
    subgoal unfolding testN_def by auto
    subgoal by auto
    using testN_sum by auto
qed

lemma post_le_one:
  "post ≤⇩L 1⇩m N"
proof -
  let ?s = "1⇩m N - post"
  have eq1: "1⇩m N * (1⇩m N - post) = 1⇩m N - post"
    apply (mat_assoc N) using post_dim by auto
  have eq2: "post * (1⇩m N - post) = 0⇩m N N"
    apply (subst mult_minus_distrib_mat[of _ N N])
    using post_dim by (auto simp add: post_mult_post)

  have "adjoint ?s = ?s" 
    apply (subst adjoint_minus)
      apply (auto simp add: post_dim adjoint_dim)
    using adjoint_one hermitian_post[unfolded hermitian_def] by auto
  then have "?s * adjoint ?s = ?s * ?s" by auto
  also have "… = 1⇩m N * (1⇩m N - post) - post * (1⇩m N - post)"
    apply (mat_assoc N) using post_dim by auto
  also have "… = ?s" unfolding eq1 eq2 using post_dim by auto
  finally have "?s * adjoint ?s = ?s".
  then have "∃M. M * adjoint M = ?s" by auto
  then have "positive ?s" apply (subst positive_if_decomp[of ?s N]) using post_dim by auto
  then show ?thesis unfolding lowner_le_def using post_dim by auto
qed

lemma qp_post:
  "is_quantum_predicate (tensor_P post (1⇩m K))"
  unfolding is_quantum_predicate_def
proof (intro conjI)
  show "tensor_P post (1⇩m K) ∈ carrier_mat d d"
    using tensor_P_dim by auto
  show "positive (tensor_P post (1⇩m K))"
    unfolding ps2_P.ptensor_mat_def
    apply (subst ps_P.tensor_mat_positive)
    by (auto simp add: ps_P_d1 ps_P_d2 post_dim positive_post positive_one)
  show "tensor_P post (1⇩m K) ≤⇩L 1⇩m d"
    unfolding ps_P.tensor_mat_id[symmetric, unfolded ps_P_d ps_P_d1 ps_P_d2]
    unfolding ps2_P.ptensor_mat_def
    apply (subst ps_P.tensor_mat_positive_le)
    unfolding ps_P_d1 ps_P_d2 using post_dim positive_post positive_one post_le_one lowner_le_refl[of "1⇩m K" K]
    by auto
qed

lemma hoare_triple_if:
  "⊢⇩p 
   {tensor_P post (1⇩m K)} 
   Measure_P vars1 N testN (replicate N SKIP)
   {tensor_P post (1⇩m K)}"
proof -
  define M where "M = (λn. mat_extension dims vars1 (testN n))"
  define Post where "Post = (λ(k::nat). tensor_P post (1⇩m K))"
  have M: "M = (λn. tensor_P (testN n) (1⇩m K))"
    unfolding M_def using mat_ext_vars1 by auto
  have skip: "⋀k. k < N ⟹ (replicate N SKIP) ! k = SKIP" by simp
  have h: "⋀k. k < N ⟹ ⊢⇩p {Post k} replicate N SKIP ! k {tensor_P post (1⇩m K)}"
    unfolding Post_def skip using qp_post hoare_partial.intros by auto
  moreover have "⋀k. k < N ⟹ is_quantum_predicate (Post k)" unfolding Post_def using qp_post by auto
  ultimately show ?thesis
    unfolding Measure_P_def apply (fold M_def) 
    using hoare_partial.intros(4)[of N Post "tensor_P post (1⇩m K)" "replicate N SKIP" M]
    unfolding M Post_def using tensor_P_testN_sum qp_post by auto
qed

theorem grover_partial_deduct:
  "⊢⇩p
   {tensor_P pre (proj_k 0)}
    Grover
   {tensor_P post (1⇩m K)}"
  unfolding Grover_def
proof -
  have "⊢⇩p
   {tensor_P pre (proj_k 0)}
    hadamard_n n
   {adjoint exM0 * P' * exM0 + adjoint exM1 * Q * exM1}"
    using hoare_partial.intros(6)[OF qp_pre qp_D3_post qp_pre qp_init_post]
    hoare_triple_init lowner_le_refl[OF tensor_P_dim] lowner_le_Q by auto
  then have "⊢⇩p
   {tensor_P pre (proj_k 0)}
    hadamard_n n;;
    While_P vars2 M0 M1 D
   {P'}"
    using hoare_triple_while hoare_partial.intros(3) qp_pre qp_D3_post qp_P' by auto
  then have "⊢⇩p
   {tensor_P pre (proj_k 0)}
    hadamard_n n;;
    While_P vars2 M0 M1 D
   {tensor_P post (1⇩m K)}"
    using lowner_le_P' hoare_partial.intros(6)[OF qp_pre qp_post qp_pre qp_P'] 
      lowner_le_P' lowner_le_refl[OF tensor_P_dim] by auto
  then show " ⊢⇩p
   {tensor_P pre (proj_k 0)}
    hadamard_n n;;
    While_P vars2 M0 M1 D;;
    Measure_P vars1 N testN (replicate N SKIP)
   {tensor_P post (1⇩m K)}"
    using hoare_triple_if qp_pre qp_post hoare_partial.intros(3) by auto
qed

theorem grover_partial_correct:
  "⊨⇩p
   {tensor_P pre (proj_k 0)}
    Grover
   {tensor_P post (1⇩m K)}"
  using grover_partial_deduct well_com_Grover qp_pre qp_post hoare_partial_sound by auto
end

end