Theory Quantum_Program

section ‹Quantum programs›

theory Quantum_Program
  imports Matrix_Limit
begin

subsection ‹Syntax›

text ‹Datatype for quantum programs›
datatype com = 
  SKIP
| Utrans "complex mat"
| Seq com com  ("_;;/ _" [60, 61] 60)
| Measure nat "nat  complex mat" "com list" 
| While "nat  complex mat" com 

text ‹A state corresponds to the density operator›
type_synonym state = "complex mat"

text ‹List of dimensions of quantum states›
locale state_sig =
  fixes dims :: "nat list"
begin

definition d :: nat where
  "d = prod_list dims"

text ‹Wellformedness of commands›

fun well_com :: "com  bool" where
  "well_com SKIP = True"
| "well_com (Utrans U) = (U  carrier_mat d d  unitary U)"
| "well_com (Seq S1 S2) = (well_com S1  well_com S2)"
| "well_com (Measure n M S) = 
    (measurement d n M  length S = n  list_all well_com S)"
| "well_com (While M S) =
    (measurement d 2 M  well_com S)"

subsection ‹Denotational semantics›

text ‹Denotation of going through the while loop n times›
fun denote_while_n_iter :: "complex mat  complex mat  (state  state)  nat  state  state" where
  "denote_while_n_iter M0 M1 DS 0 ρ = ρ"
| "denote_while_n_iter M0 M1 DS (Suc n) ρ = denote_while_n_iter M0 M1 DS n (DS (M1 * ρ * adjoint M1))"

fun denote_while_n :: "complex mat  complex mat  (state  state)  nat  state  state" where
  "denote_while_n M0 M1 DS n ρ = M0 * denote_while_n_iter M0 M1 DS n ρ * adjoint M0"

fun denote_while_n_comp :: "complex mat  complex mat  (state  state)  nat  state  state" where
  "denote_while_n_comp M0 M1 DS n ρ = M1 * denote_while_n_iter M0 M1 DS n ρ * adjoint M1"

lemma denote_while_n_iter_assoc:
  "denote_while_n_iter M0 M1 DS (Suc n) ρ = DS (M1 * (denote_while_n_iter M0 M1 DS n ρ) * adjoint M1)"
proof (induct n arbitrary: ρ)
  case 0
  show ?case by auto
next
  case (Suc n)
  show ?case
    apply (subst denote_while_n_iter.simps)
    apply (subst Suc, auto)
    done
qed

lemma denote_while_n_iter_dim:
  "ρ  carrier_mat m m  partial_density_operator ρ  M1  carrier_mat m m  adjoint M1 * M1 L 1m m
   (ρ. ρ  carrier_mat m m  partial_density_operator ρ  DS ρ  carrier_mat m m  partial_density_operator (DS ρ))
   denote_while_n_iter M0 M1 DS n ρ  carrier_mat m m  partial_density_operator (denote_while_n_iter M0 M1 DS n ρ)"
proof (induct n arbitrary: ρ)
  case 0
  then show ?case unfolding denote_while_n_iter.simps by auto
next
  case (Suc n)
  then have dr: "ρ  carrier_mat m m" and dM1: "M1  carrier_mat m m" by auto
  have dMr: "M1 * ρ * adjoint M1  carrier_mat m m" using dr dM1 by fastforce
  have pdoMr: "partial_density_operator (M1 * ρ * adjoint M1)" using pdo_close_under_measurement Suc by auto
  from Suc dMr pdoMr have d: "DS (M1 * ρ * adjoint M1)  carrier_mat m m" and "partial_density_operator (DS (M1 * ρ * adjoint M1))" by auto
  then show ?case unfolding denote_while_n_iter.simps
    using Suc by auto
qed

lemma pdo_denote_while_n_iter:
  "ρ  carrier_mat m m  partial_density_operator ρ  M1  carrier_mat m m  adjoint M1 * M1 L 1m m
   (ρ. ρ  carrier_mat m m  partial_density_operator ρ  partial_density_operator (DS ρ))
   (ρ. ρ  carrier_mat m m  partial_density_operator ρ  DS ρ  carrier_mat m m)
   partial_density_operator (denote_while_n_iter M0 M1 DS n ρ)"
proof (induct n arbitrary: ρ)
  case 0
  then show ?case unfolding denote_while_n_iter.simps by auto
next
  case (Suc n)
  have "partial_density_operator (M1 * ρ * adjoint M1)" using Suc pdo_close_under_measurement by auto
  moreover have "M1 * ρ * adjoint M1  carrier_mat m m" using Suc by auto
  ultimately have p: "partial_density_operator (DS (M1 * ρ * adjoint M1))" and d: "DS (M1 * ρ * adjoint M1)  carrier_mat m m "using Suc by auto
  show ?case unfolding denote_while_n_iter.simps using Suc(1)[OF d p Suc(4) Suc(5)] Suc by auto
qed


text ‹Denotation of while is simply the infinite sum of denote\_while\_n›
definition denote_while :: "complex mat  complex mat  (state  state)  state  state" where
  "denote_while M0 M1 DS ρ = matrix_inf_sum d (λn. denote_while_n M0 M1 DS n ρ)"

lemma denote_while_n_dim:
  assumes "ρ  carrier_mat d d"
    "M0  carrier_mat d d"
    "M1  carrier_mat d d"
    "partial_density_operator ρ"
    "ρ'. ρ'  carrier_mat d d  partial_density_operator ρ'   positive (DS ρ')  trace (DS ρ')  trace ρ'  DS ρ'  carrier_mat d d"
   shows "denote_while_n M0 M1 DS n ρ   carrier_mat d d"
proof (induction n arbitrary: ρ)
  case 0
  then show ?case 
  proof -
    have "M0 * ρ * adjoint M0  carrier_mat d d"
      using assms assoc_mult_mat by auto
    then show ?thesis by auto
  qed
next
  case (Suc n)
  then show ?case 
  proof -
    have "denote_while_n M0 M1 DS n (DS (M1 * ρ * adjoint M1))  carrier_mat d d"
      using Suc assms by auto
    then show ?thesis by auto
  qed
qed
 
lemma denote_while_n_sum_dim:
  assumes "ρ  carrier_mat d d"
    "M0  carrier_mat d d"
    "M1  carrier_mat d d"
    "partial_density_operator ρ"
    "ρ'. ρ'  carrier_mat d d  partial_density_operator ρ'   positive (DS ρ')  trace (DS ρ')  trace ρ'  DS ρ'  carrier_mat d d"
  shows "matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) n  carrier_mat d d"
proof (induct n)
  case 0
  then show ?case by auto
next
  case (Suc n)
  then show ?case
  proof -
    have " denote_while_n M0 M1 DS n ρ  carrier_mat d d"
      using denote_while_n_dim assms by auto
    then have "matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) (Suc n)  carrier_mat d d"
      using Suc by auto
    then show ?thesis by auto
  qed
qed

lemma trace_decrease_mul_adj:
  assumes pdo: "partial_density_operator ρ" and dimr: "ρ  carrier_mat d d" 
    and dimx: "x  carrier_mat d d" and un: "adjoint x * x L   1m d "
  shows "trace (x * ρ * adjoint x)  trace ρ"
proof -
  have ad: "adjoint x * x  carrier_mat d d" using adjoint_dim index_mult_mat dimx by auto
  have "trace (x * ρ * adjoint x) = trace ((adjoint x * x) * ρ)" using dimx dimr by (mat_assoc d)
  also have "  trace (1m d * ρ)" using lowner_le_trace un ad dimr pdo by auto
  also have " = trace ρ" using dimr by auto
  ultimately show ?thesis by auto
qed

lemma denote_while_n_positive: 
  assumes dim0: "M0  carrier_mat d d" and dim1: "M1  carrier_mat d d" and un: "adjoint M1 * M1 L   1m d"
      and DS: "ρ. ρ  carrier_mat d d  partial_density_operator ρ  positive (DS ρ)  trace (DS ρ)  trace ρ  DS ρ  carrier_mat d d"
  shows "partial_density_operator ρ  ρ  carrier_mat d d  positive (denote_while_n M0 M1 DS n ρ)"
proof (induction n arbitrary: ρ)
  case 0
  then show ?case using positive_close_under_left_right_mult_adjoint dim0 unfolding partial_density_operator_def by auto
next
  case (Suc n)
  then show ?case 
  proof -
    have pdoM: "partial_density_operator (M1 * ρ * adjoint M1)" using pdo_close_under_measurement Suc dim1 un by auto
    moreover have cM: "M1 * ρ * adjoint M1  carrier_mat d d" using Suc dim1 adjoint_dim index_mult_mat by auto
    ultimately have DSM1: "positive (DS (M1 * ρ * adjoint M1))  trace (DS (M1 * ρ * adjoint M1))  trace (M1 * ρ * adjoint M1)  DS (M1 * ρ * adjoint M1)  carrier_mat d d"
      using DS by auto
    moreover have "trace (M1 * ρ * adjoint M1)  trace ρ" using trace_decrease_mul_adj Suc dim1 un by auto
    ultimately have "partial_density_operator (DS (M1 * ρ * adjoint M1))" using Suc unfolding partial_density_operator_def by auto
    then have "positive (M0 * denote_while_n_iter M0 M1 DS n (DS (M1 * ρ * adjoint M1)) * adjoint M0)" using Suc DSM1 by auto
    then have "positive (denote_while_n M0 M1 DS (Suc n) ρ)" by auto
    then show ?thesis by auto      
  qed
qed

lemma denote_while_n_sum_positive:
  assumes dim0: "M0  carrier_mat d d" and dim1: "M1  carrier_mat d d" and un: "adjoint M1 * M1 L   1m d" 
      and DS: "ρ. ρ  carrier_mat d d  partial_density_operator ρ  positive (DS ρ)  trace (DS ρ)  trace ρ  DS ρ  carrier_mat d d"
      and pdo: "partial_density_operator ρ" and r: " ρ  carrier_mat d d" 
    shows "positive (matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) n)"
proof -
  have "k. k < n  positive (denote_while_n M0 M1 DS k ρ)"  using assms denote_while_n_positive by auto
  moreover have "k. k < n  denote_while_n M0 M1 DS k ρ  carrier_mat d d" using denote_while_n_dim assms by auto
  ultimately show ?thesis using matrix_sum_positive by auto
qed

lemma trace_measure2_id:
  assumes dM0: "M0  carrier_mat n n" and dM1: "M1  carrier_mat n n" 
    and id: "adjoint M0 * M0 + adjoint M1 * M1 = 1m n"
    and dA: "A  carrier_mat n n"
  shows "trace (M0 * A * adjoint M0) + trace (M1 * A * adjoint M1) = trace A"
proof -
  have "trace (M0 * A * adjoint M0) + trace (M1 * A * adjoint M1) = trace ((adjoint M0 * M0 + adjoint M1 * M1) * A)"
    using assms by (mat_assoc n)
  also have " = trace (1m n * A)" using id by auto
  also have " = trace A" using dA by auto
  finally show ?thesis.
qed

lemma measurement_lowner_le_one1:
  assumes dim0: "M0  carrier_mat d d" and dim1: "M1  carrier_mat d d" and id: "adjoint M0 * M0 + adjoint M1 * M1 = 1m d"
  shows "adjoint M1 * M1 L 1m d"
proof -
  have paM0: "positive (adjoint M0 * M0)"
    apply (subgoal_tac "adjoint M0 * adjoint (adjoint M0) = adjoint M0 * M0")
    subgoal using positive_if_decomp[of "adjoint M0 * M0"] dim0 adjoint_dim[OF dim0] by fastforce
    using adjoint_adjoint[of M0] by auto
  have le1: "adjoint M0 * M0 + adjoint M1 * M1 L 1m d" using id lowner_le_refl[of "1m d"] by fastforce
  show "adjoint M1 * M1 L 1m d" 
    using add_positive_le_reduce2[OF _ _ _ paM0 le1] dim0 dim1 by fastforce
qed

lemma denote_while_n_sum_trace:
  assumes dim0: "M0  carrier_mat d d" and dim1: "M1  carrier_mat d d" and id: "adjoint M0 * M0 + adjoint M1 * M1 = 1m d" 
      and DS: "ρ. ρ  carrier_mat d d  partial_density_operator ρ  positive (DS ρ)  trace (DS ρ)  trace ρ  DS ρ  carrier_mat d d"
      and r: " ρ  carrier_mat d d"
      and pdor: "partial_density_operator ρ"
    shows "trace (matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) n)  trace ρ"
proof -
  have un: "adjoint M1 * M1 L 1m d" using measurement_lowner_le_one1 using dim0 dim1 id by auto
  have DS': "(DS ρ  carrier_mat d d)  partial_density_operator (DS ρ)" if "ρ  carrier_mat d d" and "partial_density_operator ρ" for ρ
  proof -
    have res: "positive (DS ρ)  trace (DS ρ)  trace ρ  DS ρ  carrier_mat d d" using DS that by auto
    moreover have "trace ρ  1" using that partial_density_operator_def by auto
    ultimately have "trace (DS ρ)  1" by auto
    with res show ?thesis unfolding partial_density_operator_def by auto
  qed
  have dWk: "denote_while_n_iter M0 M1 DS k ρ  carrier_mat d d" for k 
    using denote_while_n_iter_dim[OF r pdor dim1 un] DS' dim0 dim1 by auto
  have pdoWk: "partial_density_operator (denote_while_n_iter M0 M1 DS k ρ)" for k 
    using pdo_denote_while_n_iter[OF r pdor dim1 un] DS' dim0 dim1 by auto
  have dW0k: "denote_while_n M0 M1 DS k ρ  carrier_mat d d" for k using denote_while_n_dim r dim0 dim1 pdor by auto
  then have dsW0k: "matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) k  carrier_mat d d" for k
    using matrix_sum_dim[of k "λk. denote_while_n M0 M1 DS k ρ"] by auto

  have "(denote_while_n_comp M0 M1 DS n ρ)  carrier_mat d d" for n unfolding denote_while_n_comp.simps using dim1 dWk by auto
  moreover have 
    pdoW1k: "partial_density_operator (denote_while_n_comp M0 M1 DS n ρ)" for n unfolding denote_while_n_comp.simps
    using pdo_close_under_measurement[OF dim1 dWk pdoWk un] by auto
  ultimately have "trace (DS (denote_while_n_comp M0 M1 DS n ρ))  trace (denote_while_n_comp M0 M1 DS n ρ)" for n
    using DS by auto
  moreover have "trace (denote_while_n_iter M0 M1 DS (Suc n) ρ) = trace (DS (denote_while_n_comp M0 M1 DS n ρ))" for n
    using denote_while_n_iter_assoc[folded denote_while_n_comp.simps] by auto
  ultimately have leq3: "trace (denote_while_n_iter M0 M1 DS (Suc n) ρ)  trace (denote_while_n_comp M0 M1 DS n ρ)" for n by auto

  have mainleq: "trace (matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) (Suc n)) + trace (denote_while_n_comp M0 M1 DS n ρ)  trace ρ" for n
  proof (induct n)
    case 0
    then show ?case unfolding matrix_sum.simps denote_while_n.simps denote_while_n_comp.simps denote_while_n_iter.simps 
      apply (subgoal_tac "M0 * ρ * adjoint M0 + 0m d d = M0 * ρ * adjoint M0")
      using trace_measure2_id[OF dim0 dim1 id r] dim0 apply simp
      using dim0 by auto
  next
    case (Suc n)

    have eq1: "trace (matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) (Suc (Suc n))) 
      = trace (denote_while_n M0 M1 DS (Suc n) ρ) + trace (matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) (Suc n))"
      unfolding matrix_sum.simps
      using trace_add_linear dW0k[of "Suc n"] dsW0k[of "Suc n"] by auto

    have eq2: "trace (denote_while_n M0 M1 DS (Suc n) ρ) + trace (denote_while_n_comp M0 M1 DS (Suc n) ρ) 
      = trace (denote_while_n_iter M0 M1 DS (Suc n) ρ)"
      unfolding denote_while_n.simps denote_while_n_comp.simps using trace_measure2_id[OF dim0 dim1 id dWk[of "Suc n"]] by auto

    have "trace (matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) (Suc (Suc n))) + trace (denote_while_n_comp M0 M1 DS (Suc n) ρ)
    = trace (matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) (Suc n)) + trace (denote_while_n M0 M1 DS (Suc n) ρ) + trace (denote_while_n_comp M0 M1 DS (Suc n) ρ)"
      using eq1 by auto
    also have " = trace (matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) (Suc n)) + trace (denote_while_n_iter M0 M1 DS (Suc n) ρ)"
      using eq2 by auto
    also have "  trace (matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) (Suc n)) + trace (denote_while_n_comp M0 M1 DS n ρ)"
      using leq3 by auto
    also have "  trace ρ" using Suc by auto
    finally show ?case.
  qed

  have reduce_le_complex: "(b::complex)  0  a + b  c  a  c" for a b c
    by (simp add: less_eq_complex_def)
  have "positive (denote_while_n_comp M0 M1 DS n ρ)" for n using pdoW1k unfolding partial_density_operator_def by auto
  then have "trace (denote_while_n_comp M0 M1 DS n ρ)  0" for n using positive_trace
    using n. denote_while_n_comp M0 M1 DS n ρ  carrier_mat d d by blast
  then have "trace (matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) (Suc n))  trace ρ" for n 
    using mainleq reduce_le_complex[of "trace (denote_while_n_comp M0 M1 DS n ρ)"] by auto
  moreover have "trace (matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) 0)  trace ρ"
    unfolding matrix_sum.simps
    using trace_zero positive_trace pdor unfolding partial_density_operator_def
    using r by auto
  ultimately show "trace (matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) n)  trace ρ" for n 
    apply (induct n) by auto
qed
 
lemma denote_while_n_sum_partial_density:
  assumes dim0: "M0  carrier_mat d d" and dim1: "M1  carrier_mat d d" and id: "adjoint M0 * M0 + adjoint M1 * M1 = 1m d"
      and DS: "ρ. ρ  carrier_mat d d  partial_density_operator ρ  positive (DS ρ)  trace (DS ρ)  trace ρ  DS ρ  carrier_mat d d"
      and pdo: "partial_density_operator ρ" and r: " ρ  carrier_mat d d" 
  shows "(partial_density_operator (matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) n))"
proof -
  have "trace (matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) n)  trace ρ" 
    using denote_while_n_sum_trace assms by auto
  then have "trace (matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) n)  1" 
    using pdo unfolding partial_density_operator_def  by auto
  moreover have "positive (matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) n)" 
    using assms DS denote_while_n_sum_positive measurement_lowner_le_one1[OF dim0 dim1 id] by auto
  ultimately show ?thesis unfolding partial_density_operator_def by auto
qed

lemma denote_while_n_sum_lowner_le:
  assumes dim0: "M0  carrier_mat d d" and dim1: "M1  carrier_mat d d" and id: "adjoint M0 * M0 + adjoint M1 * M1 = 1m d"
      and DS: "ρ. ρ  carrier_mat d d  partial_density_operator ρ  positive (DS ρ)  trace (DS ρ)  trace ρ  DS ρ  carrier_mat d d"
      and pdo: "partial_density_operator ρ" and dimr: " ρ  carrier_mat d d" 
  shows "(matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) n L matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) (Suc n))"
proof auto
  have whilenc: "denote_while_n M0 M1 DS n ρ  carrier_mat d d" using denote_while_n_dim assms by auto
  have sumc: "matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) n  carrier_mat d d"
    using denote_while_n_sum_dim assms by auto
  have "denote_while_n M0 M1 DS n ρ + matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) n - matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) n
         = denote_while_n M0 M1 DS n ρ  + matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) n + (- matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) n)" 
    using  minus_add_uminus_mat[of "matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) n" d d "matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) n"] by auto
  also have " = denote_while_n M0 M1 DS n ρ  + 0m d d" 
    by (smt assoc_add_mat minus_add_uminus_mat minus_r_inv_mat sumc uminus_carrier_mat whilenc)
  also have " = denote_while_n M0 M1 DS n ρ" using whilenc by auto
  finally have simp: "denote_while_n M0 M1 DS n ρ + matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) n -  matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) n =
                denote_while_n M0 M1 DS n ρ " by auto
  have "positive (denote_while_n M0 M1 DS n ρ)" using denote_while_n_positive assms measurement_lowner_le_one1[OF dim0 dim1 id] by auto
  then have "matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) n L (denote_while_n M0 M1 DS n ρ + matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) n)"
    unfolding lowner_le_def using simp by auto
  then show "matrix_sum d (λn. M0 * denote_while_n_iter M0 M1 DS n ρ * adjoint M0) n L
             (M0 * denote_while_n_iter M0 M1 DS n ρ * adjoint M0 + matrix_sum d (λn. M0 * denote_while_n_iter M0 M1 DS n ρ * adjoint M0) n)" by auto
qed

lemma lowner_is_lub_matrix_sum: 
  assumes dim0: "M0  carrier_mat d d" and dim1: "M1  carrier_mat d d" and id: "adjoint M0 * M0 + adjoint M1 * M1 = 1m d"
      and DS: "ρ. ρ  carrier_mat d d  partial_density_operator ρ  positive (DS ρ)  trace (DS ρ)  trace ρ  DS ρ  carrier_mat d d"
      and pdo: "partial_density_operator ρ" and dimr: " ρ  carrier_mat d d" 
  shows  "matrix_seq.lowner_is_lub (matrix_sum d (λn. denote_while_n M0 M1 DS n ρ)) (matrix_seq.lowner_lub (matrix_sum d (λn. denote_while_n M0 M1 DS n ρ)))"
proof-
  have sumdd: "n. matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) n  carrier_mat d d"
    using  denote_while_n_sum_dim assms by auto
  have sumtr: "n. trace (matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) n)  trace ρ"
    using denote_while_n_sum_trace assms by auto
  have sumpar: "n. partial_density_operator (matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) n)"
    using denote_while_n_sum_partial_density assms by auto
  have sumle:"n. matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) n L matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) (Suc n)"
    using denote_while_n_sum_lowner_le assms by auto
  have seqd: "matrix_seq d (matrix_sum d (λn. denote_while_n M0 M1 DS n ρ))"
    using matrix_seq_def sumdd sumpar sumle by auto
  then show ?thesis  using matrix_seq.lowner_lub_prop[of d "(matrix_sum d (λn. denote_while_n M0 M1 DS n ρ))"] by auto
qed
  
lemma denote_while_dim_positive:
  assumes dim0: "M0  carrier_mat d d" and dim1: "M1  carrier_mat d d" and id: "adjoint M0 * M0 + adjoint M1 * M1 = 1m d"
      and DS: "ρ. ρ  carrier_mat d d  partial_density_operator ρ  positive (DS ρ)  trace (DS ρ)  trace ρ  DS ρ  carrier_mat d d"
      and pdo: "partial_density_operator ρ" and dimr: " ρ  carrier_mat d d" 
  shows
    "denote_while M0 M1 DS ρ  carrier_mat d d  positive (denote_while M0 M1 DS ρ)  trace (denote_while M0 M1 DS ρ)  trace ρ"
proof -
  have sumdd: "n. matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) n  carrier_mat d d"
    using denote_while_n_sum_dim assms by auto
  have sumtr: "n. trace (matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) n)  trace ρ"
    using denote_while_n_sum_trace assms by auto
  have sumpar: "n. partial_density_operator (matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) n)"
    using denote_while_n_sum_partial_density assms by auto
  have sumle:"n. matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) n L matrix_sum d (λn. denote_while_n M0 M1 DS n ρ) (Suc n)"
    using denote_while_n_sum_lowner_le assms by auto
  have seqd: "matrix_seq d (matrix_sum d (λn. denote_while_n M0 M1 DS n ρ))"
    using matrix_seq_def sumdd sumpar sumle by auto
  have "matrix_seq.lowner_is_lub (matrix_sum d (λn. denote_while_n M0 M1 DS n ρ)) (matrix_seq.lowner_lub (matrix_sum d (λn. denote_while_n M0 M1 DS n ρ)))"
    using lowner_is_lub_matrix_sum assms by auto
  then have "matrix_seq.lowner_lub (matrix_sum d (λn. denote_while_n M0 M1 DS n ρ))  carrier_mat d d
             positive (matrix_seq.lowner_lub (matrix_sum d (λn. denote_while_n M0 M1 DS n ρ)))
             trace (matrix_seq.lowner_lub (matrix_sum d (λn. denote_while_n M0 M1 DS n ρ)))  trace ρ"
    using matrix_seq.lowner_is_lub_dim seqd matrix_seq.lowner_lub_is_positive matrix_seq.lowner_lub_trace sumtr by auto
  then show ?thesis unfolding denote_while_def matrix_inf_sum_def by auto 
qed 

definition denote_measure :: "nat  (nat  complex mat)  ((state  state) list)  state  state" where
  "denote_measure n M DS ρ = matrix_sum d (λk. (DS!k) ((M k) * ρ * adjoint (M k))) n"

lemma denote_measure_dim:
  assumes "ρ  carrier_mat d d"
    "measurement d n M"
    "ρ' k. ρ'  carrier_mat d d  k < n  (DS!k) ρ'  carrier_mat d d"
  shows
    "denote_measure n M DS ρ  carrier_mat d d"
proof -
  have dMk: "k < n  M k  carrier_mat d d" for k using assms measurement_def by auto
  have d: "k < n  (M k) * ρ * adjoint (M k)  carrier_mat d d" for k 
    using mult_carrier_mat[OF mult_carrier_mat[OF dMk assms(1)] adjoint_dim[OF dMk]] by auto
  then have "k < n  (DS!k) ((M k) * ρ * adjoint (M k))  carrier_mat d d" for k using assms(3) by auto
  then show ?thesis unfolding denote_measure_def using matrix_sum_dim[of n "λk. (DS!k) ((M k) * ρ * adjoint (M k))"] by auto
qed

lemma measure_well_com:
  assumes "well_com (Measure n M S)"
  shows "k. k < n  well_com (S ! k)"
  using assms unfolding well_com.simps using list_all_length by auto


text ‹Semantics of commands›
fun denote :: "com  state  state" where
  "denote SKIP ρ = ρ"
| "denote (Utrans U) ρ = U * ρ * adjoint U"
| "denote (Seq S1 S2) ρ = denote S2 (denote S1 ρ)"
| "denote (Measure n M S) ρ = denote_measure n M (map denote S) ρ"
| "denote (While M S) ρ = denote_while (M 0) (M 1) (denote S) ρ"


lemma denote_measure_expand:
  assumes m: "m  n" and wc: "well_com (Measure n M S)"  
  shows "denote (Measure m M S) ρ = matrix_sum d (λk. denote (S!k) ((M k) * ρ * adjoint (M k))) m"
  unfolding denote.simps denote_measure_def
proof -
  have "k < m  map denote S ! k = denote (S!k)" for k using wc m by auto
  then have "k < m  (map denote S ! k) (M k * ρ * adjoint (M k)) = denote (S!k) ((M k) * ρ * adjoint (M k))" for k by auto
  then show "matrix_sum d (λk. (map denote S ! k) (M k * ρ * adjoint (M k))) m
    = matrix_sum d (λk. denote (S ! k) (M k * ρ * adjoint (M k))) m" 
    using matrix_sum_cong[of m "λk. (map denote S ! k) (M k * ρ * adjoint (M k))" "λk. denote (S ! k) (M k * ρ * adjoint (M k))"] by auto
qed

lemma matrix_sum_trace_le:
  fixes f :: "nat  complex mat" and g :: "nat  complex mat"
  assumes "(k. k < n  f k  carrier_mat d d)" 
    "(k. k < n  g k  carrier_mat d d)"
    "(k. k < n  trace (f k)  trace (g k))"
  shows "trace (matrix_sum d f n)  trace (matrix_sum d g n)"
proof -
  have "sum (λk. trace (f k)) {0..<n}   sum (λk. trace (g k)) {0..<n}"
    using assms by (meson atLeastLessThan_iff sum_mono)
  then show ?thesis using trace_matrix_sum_linear assms by auto
qed

lemma map_denote_positive_trace_dim:
  assumes "well_com (Measure x1 x2a x3a)"
    "x4  carrier_mat d d"
    "partial_density_operator x4"
    "x3aa ρ. x3aa  set x3a  well_com x3aa  ρ  carrier_mat d d  partial_density_operator ρ 
       positive (denote x3aa ρ)  trace (denote x3aa ρ)  trace ρ  denote x3aa ρ  carrier_mat d d"
  shows "k < x1. positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) 
                ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)))  carrier_mat d d
                trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)))  trace (x2a k * x4 * adjoint (x2a k))"
proof -
  have x2ak: " k < x1. x2a k  carrier_mat d d" using assms(1) measurement_dim by auto
  then have x2aa:" k < x1. (x2a k * x4 * adjoint (x2a k))  carrier_mat d d" using assms(2) by fastforce
  have posct: "positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) 
                ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)))  carrier_mat d d
                trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)))  trace (x2a k * x4 * adjoint (x2a k))"
    if k: "k < x1" for k
  proof -
    have lea: "adjoint (x2a k) * x2a k L 1m d" using measurement_le_one_mat assms(1) k by auto
    have "(x2a k * x4 * adjoint (x2a k))  carrier_mat d d" using k x2aa assms(2) by fastforce
    moreover have "(x3a ! k)  set x3a" using k assms(1) by simp
    moreover have "well_com (x3a ! k)"  using k assms(1) using measure_well_com by blast
    moreover have "partial_density_operator (x2a k * x4 * adjoint (x2a k))" 
      using pdo_close_under_measurement x2ak assms(2,3) lea  k by blast 
    ultimately have "positive (denote (x3a ! k) (x2a k * x4 * adjoint (x2a k)))
          (denote (x3a ! k) (x2a k * x4 * adjoint (x2a k)))  carrier_mat d d
          trace (denote (x3a ! k) (x2a k * x4 * adjoint (x2a k)))  trace (x2a k * x4 * adjoint (x2a k))" 
      using assms(4) by auto
    then show ?thesis using assms(1) k by auto          
  qed
  then show ?thesis by auto
qed

lemma denote_measure_positive_trace_dim:
  assumes "well_com (Measure x1 x2a x3a)"
    "x4  carrier_mat d d"
    "partial_density_operator x4"
    "x3aa ρ. x3aa  set x3a  well_com x3aa  ρ  carrier_mat d d  partial_density_operator ρ 
       positive (denote x3aa ρ)  trace (denote x3aa ρ)  trace ρ  denote x3aa ρ  carrier_mat d d"
  shows "positive (denote (Measure x1 x2a x3a) x4)  trace (denote (Measure x1 x2a x3a) x4)  trace x4
         (denote (Measure x1 x2a x3a) x4)  carrier_mat d d"
proof -
  have x2ak: " k < x1. x2a k  carrier_mat d d" using assms(1) measurement_dim by auto
  then have x2aa:" k < x1. (x2a k * x4 * adjoint (x2a k))  carrier_mat d d" using assms(2) by fastforce
  have posct:" k < x1. positive ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) 
                ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)))  carrier_mat d d
                trace ((map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)))  trace (x2a k * x4 * adjoint (x2a k))"
    using map_denote_positive_trace_dim assms by auto
  
  have "trace (matrix_sum d (λk. (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) x1)
        trace (matrix_sum d (λk. (x2a k * x4 * adjoint (x2a k))) x1)"
    using posct matrix_sum_trace_le[of x1 "(λk. (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k)))" "(λk. x2a k * x4 * adjoint (x2a k)) "]
         x2aa by auto
  also have " = trace x4"  using trace_measurement[of d "x1" "x2a" x4] assms(1,2) by auto
  finally have " trace (matrix_sum d (λk. (map denote x3a ! k) (x2a k * x4 * adjoint (x2a k))) x1)  trace x4" by auto
  then have "trace (denote_measure x1 x2a (map denote x3a) x4)  trace x4"
    unfolding denote_measure_def by auto
  then have "trace (denote (Measure x1 x2a x3a) x4)  trace x4" by auto
  moreover from posct have "positive (denote (Measure x1 x2a x3a) x4)"
    apply auto
    unfolding denote_measure_def using matrix_sum_positive by auto
  moreover have "(denote (Measure x1 x2a x3a) x4)  carrier_mat d d" 
    apply auto  
    unfolding denote_measure_def using matrix_sum_dim posct 
    by (simp add: matrix_sum_dim)
  ultimately show ?thesis by auto
qed
  
lemma denote_positive_trace_dim:
  "well_com S  ρ  carrier_mat d d  partial_density_operator ρ 
    (positive (denote S ρ)  trace (denote S ρ)  trace ρ  denote S ρ  carrier_mat d d)"
proof (induction arbitrary: ρ)
  case SKIP
then show ?case unfolding partial_density_operator_def by auto
next
case (Utrans x)
  then show ?case  
  proof -
    assume wc: "well_com (Utrans x)" and r: "ρ  carrier_mat d d" and pdo: "partial_density_operator ρ"
    show "positive (denote (Utrans x) ρ)  trace (denote (Utrans x) ρ)  trace ρ  denote (Utrans x) ρ  carrier_mat d d"
    proof -
     have "trace (x * ρ * adjoint x) = trace ((adjoint x * x) * ρ)"
       using r apply (mat_assoc d) using wc by auto
     also have " = trace (1m d * ρ)" using wc inverts_mat_def inverts_mat_symm adjoint_dim by auto
     also have " = trace ρ"  using r by auto
     finally have fst: "trace (x * ρ * adjoint x) = trace ρ" by auto
     moreover have "positive (x * ρ * adjoint x)" using positive_close_under_left_right_mult_adjoint r pdo wc unfolding partial_density_operator_def by auto
     moreover have "x * ρ * adjoint x  carrier_mat d d" using r wc adjoint_dim index_mult_mat by auto
     ultimately show ?thesis by auto
    qed
  qed
next
  case (Seq x1 x2a)
  then show ?case
  proof -
    assume dx1: "(ρ. well_com x1  ρ  carrier_mat d d  partial_density_operator ρ  positive (denote x1 ρ)  trace (denote x1 ρ)  trace ρ  denote x1 ρ  carrier_mat d d)"
       and dx2a: "(ρ. well_com x2a  ρ  carrier_mat d d  partial_density_operator ρ  positive (denote x2a ρ)  trace (denote x2a ρ)  trace ρ  denote x2a ρ  carrier_mat d d)"
       and wc: "well_com (Seq x1 x2a)" and r: "ρ  carrier_mat d d" and pdo: "partial_density_operator ρ"
    show "positive (denote (Seq x1 x2a) ρ)  trace (denote (Seq x1 x2a) ρ)  trace ρ  denote (Seq x1 x2a) ρ  carrier_mat d d"
    proof -
      have ptc: "positive (denote x1 ρ)  trace (denote x1 ρ)  trace ρ  denote x1 ρ  carrier_mat d d"
        using wc r pdo dx1 by auto
      then have "partial_density_operator (denote x1 ρ)" using pdo unfolding partial_density_operator_def by auto
      then show ?thesis using ptc dx2a wc  dual_order.trans by auto
    qed
  qed
next
  case (Measure x1 x2a x3a)
  then show ?case using denote_measure_positive_trace_dim by auto
next
  case (While x1 x2a)
  then show ?case
  proof -
    have "adjoint (x1 0) * (x1 0) + adjoint (x1 1) * (x1 1) = 1m d"
      using measurement_id2 While by auto
    moreover have "(ρ. ρ  carrier_mat d d  partial_density_operator ρ  
      positive (denote x2a ρ)  trace (denote x2a ρ)  trace ρ  denote x2a ρ  carrier_mat d d)"
      using While by fastforce
    moreover have "x1 0  carrier_mat d d  x1 1  carrier_mat d d"
      using measurement_dim While by fastforce
    ultimately have "denote_while (x1 0) (x1 1) (denote x2a) ρ  carrier_mat d d  
               positive (denote_while (x1 0) (x1 1) (denote x2a) ρ)  
               trace (denote_while (x1 0) (x1 1) (denote x2a) ρ)  trace ρ"
      using denote_while_dim_positive[of "x1 0" "x1 1" "denote x2a" "ρ"] While by fastforce
    then show ?thesis by auto
  qed 
qed

lemma denote_dim_pdo:
  "well_com S  ρ  carrier_mat d d  partial_density_operator ρ 
    (denote S ρ  carrier_mat d d)  (partial_density_operator (denote S ρ))"
  using denote_positive_trace_dim unfolding partial_density_operator_def by fastforce

lemma denote_dim:
  "well_com S  ρ  carrier_mat d d  partial_density_operator ρ 
    (denote S ρ  carrier_mat d d)"
  using denote_positive_trace_dim by auto

lemma denote_trace:
  "well_com S  ρ  carrier_mat d d  partial_density_operator ρ 
    trace (denote S ρ)  trace ρ"
  using denote_positive_trace_dim by auto

lemma denote_partial_density_operator:
  assumes "well_com S" "partial_density_operator ρ" "ρ  carrier_mat d d"
  shows "partial_density_operator (denote S ρ)"
  using assms denote_positive_trace_dim unfolding partial_density_operator_def
  using dual_order.trans by blast


lemma denote_while_n_sum_mat_seq:
  assumes "ρ  carrier_mat d d" and
    "x1 0  carrier_mat d d" and
    "x1 1  carrier_mat d d" and
    "partial_density_operator ρ" and
    wc: "well_com x2" and mea: "measurement d 2 x1"  
  shows "matrix_seq d (matrix_sum d (λn. denote_while_n (x1 0) (x1 1) (denote x2) n ρ))"   
proof -
  let ?A = "x1 0" and ?B = "x1 1"
  have dx2:"ρ. ρ  carrier_mat d d  partial_density_operator ρ 
            positive ((denote x2) ρ)  trace ((denote x2) ρ)  trace ρ  (denote x2) ρ  carrier_mat d d"
    using denote_positive_trace_dim wc by auto
  have lo1: "adjoint ?A * ?A + adjoint ?B * ?B = 1m d" using measurement_id2 assms by auto
  have "n. matrix_sum d (λn. denote_while_n (x1 0) (x1 1) (denote x2) n ρ) n  carrier_mat d d"
    using assms dx2 
    by (metis denote_while_n_dim matrix_sum_dim)
  moreover have "(n. partial_density_operator (matrix_sum d (λn. denote_while_n (x1 0) (x1 1) (denote x2) n ρ) n))"
    using assms dx2 lo1
    by (metis denote_while_n_sum_partial_density)
  moreover have "(n. matrix_sum d (λn. denote_while_n (x1 0) (x1 1) (denote x2) n ρ) n L matrix_sum d (λn. denote_while_n (x1 0) (x1 1) (denote x2) n ρ) (Suc n))"
    using assms dx2 lo1
    by (metis denote_while_n_sum_lowner_le)
  ultimately show ?thesis
    unfolding matrix_seq_def by auto
qed 

lemma denote_while_n_add:
  assumes M0: "x1 0  carrier_mat d d" and
    M1: "x1 1  carrier_mat d d" and
    wc: "well_com x2" and mea: "measurement d 2 x1" and
    DS: "(ρ1 ρ2. ρ1  carrier_mat d d  ρ2  carrier_mat d d  partial_density_operator ρ1  
      partial_density_operator ρ2  trace (ρ1 + ρ2)  1  denote x2 (ρ1 + ρ2) = denote x2 ρ1 + denote x2 ρ2)"
  shows "ρ1  carrier_mat d d  ρ2  carrier_mat d d  partial_density_operator ρ1  partial_density_operator ρ2  trace (ρ1 + ρ2)  1  
    denote_while_n (x1 0) (x1 1) (denote x2) k (ρ1 + ρ2) = denote_while_n (x1 0) (x1 1) (denote x2) k ρ1 + denote_while_n (x1 0) (x1 1) (denote x2) k ρ2"
proof (auto, induct k arbitrary: ρ1 ρ2)
  case 0
  then show ?case
    apply auto using M0 by (mat_assoc d)
next
  case (Suc k)
  then show ?case 
  proof -
    let ?A = "x1 0" and ?B = "x1 1"
    have dx2:"(ρ. ρ  carrier_mat d d  partial_density_operator ρ  positive ((denote x2) ρ)  trace ((denote x2) ρ)  trace ρ  (denote x2) ρ  carrier_mat d d) "
      using denote_positive_trace_dim wc by auto
    have lo1: "adjoint ?B * ?B L 1m d" using measurement_le_one_mat assms by auto
    have dim1: "x1 1 * ρ1 * adjoint (x1 1)  carrier_mat d d" using assms Suc 
      by (metis adjoint_dim mult_carrier_mat)
    moreover have pdo1: "partial_density_operator (x1 1 * ρ1 * adjoint (x1 1))"
      using pdo_close_under_measurement assms(2) Suc(2,4) lo1 by auto
    ultimately have dimr1: "denote x2 (x1 1 * ρ1 * adjoint (x1 1))  carrier_mat d d"
      using dx2 by auto
    have dim2: "x1 1 * ρ2 * adjoint (x1 1)  carrier_mat d d" using assms Suc 
      by (metis adjoint_dim mult_carrier_mat)
    moreover have pdo2: "partial_density_operator (x1 1 * ρ2 * adjoint (x1 1))"
      using pdo_close_under_measurement assms(2) Suc lo1 by auto
    ultimately have dimr2: "denote x2 (x1 1 * ρ2 * adjoint (x1 1))  carrier_mat d d"
      using dx2 by auto
    have pdor1: "partial_density_operator (denote x2 (x1 1 * ρ1 * adjoint (x1 1)))"
      using denote_partial_density_operator assms dim1 pdo1 by auto
    have pdor2: "partial_density_operator (denote x2 (x1 1 * ρ2 * adjoint (x1 1)))"
      using denote_partial_density_operator assms dim2 pdo2 by auto
    have "trace (denote x2 (x1 1 * ρ1 * adjoint (x1 1)))  trace (x1 1 * ρ1 * adjoint (x1 1))"
      using dx2 dim1 pdo1 by auto
    also have tr1: "  trace ρ1" using trace_decrease_mul_adj assms Suc lo1 by auto
    finally have trr1:" trace (denote x2 (x1 1 * ρ1 * adjoint (x1 1)))  trace ρ1" by auto
    have "trace (denote x2 (x1 1 * ρ2 * adjoint (x1 1)))  trace (x1 1 * ρ2 * adjoint (x1 1))"
      using dx2 dim2 pdo2 by auto
    also have tr2: "  trace ρ2" using trace_decrease_mul_adj assms Suc lo1 by auto
    finally have trr2:" trace (denote x2 (x1 1 * ρ2 * adjoint (x1 1)))  trace ρ2" by auto
    from tr1 tr2 Suc have "trace ( (x1 1 * ρ1 * adjoint (x1 1)) +  (x1 1 * ρ2 * adjoint (x1 1)))  trace (ρ1 + ρ2)"
      using trace_add_linear trace_add_linear[of "(x1 1 * ρ1 * adjoint (x1 1))" d "(x1 1 * ρ2 * adjoint (x1 1))"]
            trace_add_linear[of ρ1 d ρ2]
      using dim1 dim2 by (auto simp: less_eq_complex_def)
    then have trless1: "trace ( (x1 1 * ρ1 * adjoint (x1 1)) +  (x1 1 * ρ2 * adjoint (x1 1)))  1" using Suc by auto
    from trr1 trr2 Suc have "trace (denote x2 (x1 1 * ρ1 * adjoint (x1 1)) + denote x2 (x1 1 * ρ2 * adjoint (x1 1)))  trace (ρ1 + ρ2)"
      using trace_add_linear[of "denote x2 (x1 1 * ρ1 * adjoint (x1 1))" d "denote x2 (x1 1 * ρ2 * adjoint (x1 1))"]
            trace_add_linear[of ρ1 d ρ2]
      using dimr1 dimr2 by (auto simp: less_eq_complex_def)
    then have trless2: "trace (denote x2 (x1 1 * ρ1 * adjoint (x1 1)) + denote x2 (x1 1 * ρ2 * adjoint (x1 1)))  1"
      using Suc by auto
    have "x1 1 * (ρ1 + ρ2) * adjoint (x1 1) = (x1 1 * ρ1 * adjoint (x1 1)) + (x1 1 * ρ2 * adjoint (x1 1))"
      using M1 Suc by (mat_assoc d)
    then have deadd: "denote x2 (x1 1 * (ρ1 + ρ2) * adjoint (x1 1)) =
        denote x2 (x1 1 * ρ1 * adjoint (x1 1)) + denote x2 (x1 1 * ρ2 * adjoint (x1 1))"
      using assms(5) dim1 dim2 pdo1 pdo2 trless1 by auto
    from dimr1 dimr2 pdor1 pdor2 trless2 Suc(1) deadd show ?thesis by auto
  qed
qed

lemma denote_while_add:
  assumes r1: "ρ1  carrier_mat d d" and
    r2: "ρ2  carrier_mat d d" and
    M0: "x1 0  carrier_mat d d" and
    M1: "x1 1  carrier_mat d d" and
    pdo1: "partial_density_operator ρ1" and
    pdo2: "partial_density_operator ρ2" and tr12: "trace (ρ1 + ρ2)  1" and
    wc: "well_com x2" and mea: "measurement d 2 x1" and
    DS: "(ρ1 ρ2. ρ1  carrier_mat d d  ρ2  carrier_mat d d  partial_density_operator ρ1  
      partial_density_operator ρ2  trace (ρ1 + ρ2)  1  denote x2 (ρ1 + ρ2) = denote x2 ρ1 + denote x2 ρ2)"
    shows
    "denote_while (x1 0) (x1 1) (denote x2) (ρ1 + ρ2) = denote_while (x1 0) (x1 1) (denote x2) ρ1 + denote_while (x1 0) (x1 1) (denote x2) ρ2"
proof -
  let ?A = "x1 0" and ?B = "x1 1"
  have dx2:"(ρ. ρ  carrier_mat d d  partial_density_operator ρ  positive ((denote x2) ρ)  trace ((denote x2) ρ)  trace ρ  (denote x2) ρ  carrier_mat d d) "
    using denote_positive_trace_dim wc by auto
  have lo1: "adjoint ?A * ?A + adjoint ?B * ?B = 1m d" using measurement_id2 assms by auto
  have pdo12: "partial_density_operator (ρ1 + ρ2)" using pdo1 pdo2 unfolding partial_density_operator_def using tr12 positive_add assms by auto
  have ms1: "matrix_seq d (matrix_sum d (λn. denote_while_n ?A ?B (denote x2) n ρ1))"   
    using denote_while_n_sum_mat_seq assms by auto
  have ms2: "matrix_seq d (matrix_sum d (λn. denote_while_n ?A ?B (denote x2) n ρ2))"   
    using denote_while_n_sum_mat_seq assms by auto
  have dim1: "(n. matrix_sum d (λn. denote_while_n (x1 0) (x1 1) (denote x2) n ρ1) n  carrier_mat d d)"   
    using assms dx2 
    by (metis denote_while_n_dim matrix_sum_dim)
  have dim2: "(n. matrix_sum d (λn. denote_while_n (x1 0) (x1 1) (denote x2) n ρ2) n  carrier_mat d d)"   
    using assms dx2 
    by (metis denote_while_n_dim matrix_sum_dim)
  have "trace (matrix_sum d (λn. denote_while_n ?A ?B (denote x2) n ρ1) n +
               matrix_sum d (λn. denote_while_n ?A ?B (denote x2) n ρ2) n)  trace (ρ1 + ρ2)"
    for n
  proof -
    have "trace (matrix_sum d (λn. denote_while_n ?A ?B (denote x2) n ρ1) n)  trace ρ1"
      using denote_while_n_sum_trace dx2 lo1 assms by auto
    moreover have "trace (matrix_sum d (λn. denote_while_n ?A ?B (denote x2) n ρ2) n)  trace ρ2"
      using denote_while_n_sum_trace dx2 lo1 assms by auto
    ultimately show ?thesis
      using trace_add_linear dim1 dim2
      by (metis add_mono_thms_linordered_semiring(1) r1 r2)
  qed
  then have "n. trace (matrix_sum d (λn. denote_while_n ?A ?B (denote x2) n ρ1) n + matrix_sum d (λn. denote_while_n ?A ?B (denote x2) n ρ2) n)  1"
    using assms(7) dual_order.trans by blast
  then have lladd: "matrix_seq.lowner_lub  (λn. (matrix_sum d (λn. denote_while_n ?A ?B (denote x2) n ρ1)) n + (matrix_sum d (λn. denote_while_n ?A ?B (denote x2) n ρ2)) n) = matrix_seq.lowner_lub (matrix_sum d (λn. denote_while_n ?A ?B (denote x2) n ρ1))
    + matrix_seq.lowner_lub (matrix_sum d (λn. denote_while_n ?A ?B (denote x2) n ρ2))"
    using lowner_lub_add ms1 ms2 by auto
 
  have "matrix_sum d (λn. denote_while_n (x1 0) (x1 1) (denote x2) n (ρ1 + ρ2)) m =
    matrix_sum d (λn. denote_while_n ?A ?B (denote x2) n ρ1) m + matrix_sum d (λn. denote_while_n ?A ?B (denote x2) n ρ2) m"
    for m
  proof -
    have "(k. k < m  denote_while_n (x1 0) (x1 1) (denote x2) k (ρ1 + ρ2)  carrier_mat d d)"
      using denote_while_n_dim dx2 pdo12 assms measurement_dim by auto
    moreover have "(k. k < m  denote_while_n (x1 0) (x1 1) (denote x2) k ρ1  carrier_mat d d)" 
      using denote_while_n_dim dx2  assms measurement_dim by auto
    moreover have "(k. k < m  denote_while_n (x1 0) (x1 1) (denote x2) k ρ2  carrier_mat d d)"
      using denote_while_n_dim dx2  assms measurement_dim by auto
    moreover have "(  k < m.
      denote_while_n (x1 0) (x1 1) (denote x2) k (ρ1 + ρ2) = denote_while_n (x1 0) (x1 1) (denote x2) k ρ1 + denote_while_n (x1 0) (x1 1) (denote x2) k ρ2)"
      using denote_while_n_add assms by auto
    ultimately show ?thesis
      using matrix_sum_add[of m "(λn. denote_while_n (x1 0) (x1 1) (denote x2) n (ρ1 + ρ2))" d "(λn. denote_while_n (x1 0) (x1 1) (denote x2) n ρ1)"
        "(λn. denote_while_n (x1 0) (x1 1) (denote x2) n ρ2)"] by auto
  qed
  then have "matrix_seq.lowner_lub (matrix_sum d (λn. denote_while_n (x1 0) (x1 1) (denote x2) n (ρ1 + ρ2))) = 
    matrix_seq.lowner_lub (λn. (matrix_sum d (λn. denote_while_n ?A ?B (denote x2) n ρ1)) n + (matrix_sum d (λn. denote_while_n ?A ?B (denote x2) n ρ2)) n)"
    using lladd by presburger
  then show ?thesis unfolding denote_while_def matrix_inf_sum_def using lladd by auto
qed

lemma denote_add:
  "well_com S  ρ1  carrier_mat d d  ρ2  carrier_mat d d 
   partial_density_operator ρ1  partial_density_operator ρ2  trace (ρ1 + ρ2)  1 
   denote S (ρ1 + ρ2) = denote S ρ1 + denote S ρ2"
proof (induction arbitrary: ρ1 ρ2)
  case SKIP
  then show ?case by auto
next
  case (Utrans U)
  then show ?case by (clarsimp, mat_assoc d)
next
  case (Seq x1 x2a)
  then show ?case
  proof -
    have dim1: "denote x1 ρ1  carrier_mat d d" using denote_positive_trace_dim Seq by auto
    have dim2: "denote x1 ρ2  carrier_mat d d" using denote_positive_trace_dim Seq by auto
    have "trace (denote x1  ρ1)  trace ρ1" using denote_positive_trace_dim Seq by auto
    moreover have "trace (denote x1 ρ2)  trace ρ2" using denote_positive_trace_dim Seq by auto
    ultimately have tr: "trace (denote x1 ρ1 + denote x1 ρ2)  1" using Seq(4,5,8) trace_add_linear dim1 dim2
      by (smt add_mono order_trans)

    have "denote (Seq x1 x2a) (ρ1 + ρ2) = denote x2a (denote x1 (ρ1 + ρ2))" by auto
    moreover have "denote x1 (ρ1 + ρ2) = denote x1 ρ1 + denote x1 ρ2" using Seq by auto
    moreover have "partial_density_operator (denote x1 ρ1)" using denote_partial_density_operator Seq by auto
    moreover have "partial_density_operator (denote x1 ρ2)" using denote_partial_density_operator Seq by auto
    ultimately show ?thesis using Seq dim1 dim2 tr by auto
  qed
next
  case (Measure x1 x2a x3a)
  then show ?case
  proof -
    have ptc: "x3aa ρ. x3aa  set x3a  well_com x3aa  ρ  carrier_mat d d  partial_density_operator ρ 
       positive (denote x3aa ρ)  trace (denote x3aa ρ)  trace ρ  denote x3aa ρ  carrier_mat d d"
      using denote_positive_trace_dim Measure by auto
    then have map:"ρ. ρ  carrier_mat d d  partial_density_operator ρ   k < x1. positive ((map denote x3a ! k) (x2a k * ρ * adjoint (x2a k))) 
                ((map denote x3a ! k) (x2a k * ρ * adjoint (x2a k)))  carrier_mat d d
                trace ((map denote x3a ! k) (x2a k * ρ * adjoint (x2a k)))  trace (x2a k * ρ * adjoint (x2a k))"
      using Measure map_denote_positive_trace_dim by auto

    from map have mapd1: "k. k < x1  (map denote x3a ! k) (x2a k * ρ1 * adjoint (x2a k))  carrier_mat d d"
      using Measure by auto
    from map have mapd2: "k. k < x1  (map denote x3a ! k) (x2a k * ρ2 * adjoint (x2a k))  carrier_mat d d"
      using Measure by auto
    have dim1:"k. k < x1  x2a k * ρ1 * adjoint (x2a k)  carrier_mat d d" 
      using well_com.simps(5) measurement_dim Measure by fastforce
    have dim2: "k. k < x1  x2a k * ρ2 * adjoint (x2a k)  carrier_mat d d"
      using well_com.simps(5) measurement_dim Measure by fastforce
    have "k. k < x1  (x2a k * (ρ1 + ρ2) * adjoint (x2a k))  carrier_mat d d"
      using well_com.simps(5) measurement_dim Measure by fastforce
    have lea: "k. k < x1  adjoint (x2a k) * x2a k L 1m d" using measurement_le_one_mat Measure by auto
    moreover have dimx: "k. k < x1  x2a k  carrier_mat d d" using Measure measurement_dim by auto
    ultimately have pdo12:"k. k < x1  partial_density_operator (x2a k * ρ1 * adjoint (x2a k))  partial_density_operator (x2a k * ρ2 * adjoint (x2a k))"
      using pdo_close_under_measurement Measure measurement_dim by blast

    have trless: "trace (x2a k * ρ1 * adjoint (x2a k) + x2a k * ρ2 * adjoint (x2a k))  1"
      if k: "k < x1" for k
    proof -
      have "trace (x2a k * ρ1 * adjoint (x2a k))  trace ρ1" using trace_decrease_mul_adj dimx Measure lea k by auto
      moreover have "trace (x2a k * ρ2 * adjoint (x2a k))  trace ρ2" using trace_decrease_mul_adj dimx Measure lea k by auto
      ultimately have "trace (x2a k * ρ1 * adjoint (x2a k) + x2a k * ρ2 * adjoint (x2a k))  trace (ρ1 + ρ2)"
        using trace_add_linear dim1 dim2 Measure k 
        by (metis add_mono_thms_linordered_semiring(1))
      then show ?thesis using Measure(7) by auto
    qed
 
    have dist: "(x2a k * (ρ1 + ρ2) * adjoint (x2a k)) = (x2a k * ρ1 * adjoint (x2a k)) + (x2a k * ρ2 * adjoint (x2a k))"
      if k: "k < x1" for k
    proof -
      have "(x2a k * (ρ1 + ρ2) * adjoint (x2a k)) = ((x2a k * ρ1 + x2a k * ρ2) * adjoint (x2a k))"
        using mult_add_distrib_mat Measure well_com.simps(4) measurement_dim by (metis k)
      also have " = (x2a k * ρ1 * adjoint (x2a k)) + (x2a k * ρ2 * adjoint (x2a k))"
        apply (mat_assoc d) using Measure k well_com.simps(4) measurement_dim by auto
      finally show ?thesis by auto
    qed

    have mapadd: "(map denote x3a ! k) (x2a k * (ρ1 + ρ2) * adjoint (x2a k)) =
        (map denote x3a ! k) (x2a k * ρ1 * adjoint (x2a k)) + (map denote x3a ! k) (x2a k * ρ2 * adjoint (x2a k))"
      if k: "k < x1" for k
    proof -
      have "(map denote x3a ! k) (x2a k * (ρ1 + ρ2) * adjoint (x2a k)) = denote (x3a ! k) (x2a k * (ρ1 + ρ2) * adjoint (x2a k))"
        using Measure.prems(1) k by auto
      then have mapx: "(map denote x3a ! k) (x2a k * (ρ1 + ρ2) * adjoint (x2a k)) =  denote (x3a ! k) ((x2a k * ρ1 * adjoint (x2a k)) + (x2a k * ρ2 * adjoint (x2a k)))"
        using dist k by auto
      have "denote (x3a ! k) ((x2a k * ρ1 * adjoint (x2a k)) + (x2a k * ρ2 * adjoint (x2a k))) 
           = denote (x3a ! k) (x2a k * ρ1 * adjoint (x2a k)) + denote (x3a ! k) (x2a k * ρ2  * adjoint (x2a k))"
        using Measure(1,2) dim1 dim2 pdo12 trless k
        by (simp add: list_all_length)
      then show ?thesis  
        using Measure.prems(1) mapx k by auto
    qed
    then have mapd12:"(k. k < x1  (map denote x3a ! k) (x2a k * (ρ1 + ρ2) * adjoint (x2a k))  carrier_mat d d)"
      using mapd1 mapd2 by auto

    have "matrix_sum d (λk. (map denote x3a ! k) (x2a k * (ρ1 + ρ2) * adjoint (x2a k))) x1 =
          matrix_sum d (λk. (map denote x3a ! k) (x2a k * ρ1 * adjoint (x2a k))) x1 + 
          matrix_sum d (λk. (map denote x3a ! k) (x2a k * ρ2 * adjoint (x2a k))) x1"
      using matrix_sum_add[of x1 "(λk. (map denote x3a ! k) (x2a k * (ρ1 + ρ2) * adjoint (x2a k)))" d "(λk. (map denote x3a ! k) (x2a k * ρ1 * adjoint (x2a k)))" "(λk. (map denote x3a ! k) (x2a k * ρ2 * adjoint (x2a k)))"]
      using mapd12 mapd1 mapd2 mapadd by auto
    then show ?thesis  using denote.simps(4) unfolding denote_measure_def by auto
  qed
next
  case (While x1 x2)
  then show ?case
    apply auto using denote_while_add measurement_dim by auto     
qed 


lemma mulfact:
  fixes c:: real and a:: complex and b:: complex
  assumes "c0" "a  b"
  shows "c * a  c * b"
  using assms mult_le_cancel_left_pos unfolding less_eq_complex_def by force

lemma denote_while_n_scale:
  fixes c:: real
  assumes "c0"
    "measurement d 2 x1" "well_com x2"
    "(ρ. ρ  carrier_mat d d  partial_density_operator ρ  trace (c m ρ)  1  
      denote x2 (c m ρ) =  c m denote x2 ρ)"
  shows "ρ  carrier_mat d d  partial_density_operator ρ  trace (c m ρ)  1  
    denote_while_n (x1 0) (x1 1) (denote x2) n (complex_of_real c m ρ) = c m (denote_while_n (x1 0) (x1 1) (denote x2) n ρ)"
proof (auto, induct n arbitrary: ρ)
  case 0
  then show ?case 
    apply auto apply (mat_assoc d) using assms measurement_dim by auto
next
  case (Suc n)
  then show ?case
  proof -
    let ?A = "x1 0" and ?B = "x1 1"
    have dx2:"(ρ. ρ  carrier_mat d d  partial_density_operator ρ  positive ((denote x2) ρ)  trace ((denote x2) ρ)  trace ρ  (denote x2) ρ  carrier_mat d d) "
      using denote_positive_trace_dim assms by auto
    have lo1: "adjoint ?B * ?B L 1m d" using measurement_le_one_mat assms by auto
    have dim1: "x1 1 * ρ * adjoint (x1 1)  carrier_mat d d" using assms(2) Suc(2) measurement_dim 
      by (meson adjoint_dim mult_carrier_mat one_less_numeral_iff semiring_norm(76))
    moreover have pdo1: "partial_density_operator (x1 1 * ρ