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 1⇩m 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 1⇩m 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   1⇩m 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 (1⇩m 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   1⇩m 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   1⇩m 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 = 1⇩m 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 (1⇩m 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 = 1⇩m d"
  shows "adjoint M1 * M1 ≤⇩L 1⇩m 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 1⇩m d" using id lowner_le_refl[of "1⇩m d"] by fastforce
  show "adjoint M1 * M1 ≤⇩L 1⇩m 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 = 1⇩m 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 1⇩m 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 + 0⇩m 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 = 1⇩m 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 = 1⇩m 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 ρ  + 0⇩m 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 = 1⇩m 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 = 1⇩m 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 1⇩m 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 (1⇩m 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) = 1⇩m 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 = 1⇩m 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 1⇩m 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 = 1⇩m 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 1⇩m 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 "c≥0" "a ≤ b"
  shows "c * a ≤ c * b"
  using assms mult_le_cancel_iff2 unfolding less_eq_complex_def by force

lemma denote_while_n_scale:
  fixes c:: real
  assumes "c≥0"
    "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 1⇩m 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 * ρ * adjoint (x1 1))"
      using pdo_close_under_measurement assms  Suc lo1 measurement_dim 
      by (metis One_nat_def lessI numeral_2_eq_2)
    ultimately have dimr: "denote x2 (x1 1 * ρ * adjoint (x1 1)) ∈ carrier_mat d d"
      using dx2 by auto
    have pdor: "partial_density_operator (denote x2 (x1 1 * ρ * adjoint (x1 1)))"
      using denote_partial_density_operator assms dim1 pdo1 by auto
    have "trace (denote x2 (x1 1 * ρ * adjoint (x1 1))) ≤ trace (x1 1 * ρ * adjoint (x1 1))"
      using dx2 dim1 pdo1 by auto
    also have trr1: "… ≤ trace ρ" using trace_decrease_mul_adj assms Suc lo1 measurement_dim by auto
    finally have trr: "trace (denote x2 (x1 1 * ρ * adjoint (x1 1))) ≤ trace ρ" by auto
    moreover have "trace (c ⋅⇩m denote x2 (x1 1 * ρ * adjoint (x1 1))) = c * trace (denote x2 (x1 1 * ρ * adjoint (x1 1)))"
      using trace_smult dimr by auto
    moreover have trcr: "trace (c ⋅⇩m ρ) = c * trace ρ" using trace_smult Suc by auto
    ultimately have "trace (c ⋅⇩m denote x2 (x1 1 * ρ * adjoint (x1 1))) ≤ trace (c ⋅⇩m ρ)"
      using assms(1) state_sig.mulfact by auto
    then have trrc: "trace (c ⋅⇩m denote x2 (x1 1 * ρ * adjoint (x1 1))) ≤  1" using Suc by auto
    have "trace (c ⋅⇩m (x1 1 * ρ * adjoint (x1 1))) = c * trace (x1 1 * ρ * adjoint (x1 1))"
      using trace_smult dim1 by auto
    then have "trace (c ⋅⇩m (x1 1 * ρ * adjoint (x1 1))) ≤ trace (c ⋅⇩m ρ)"  using trcr trr1 assms(1) 
      using state_sig.mulfact by auto
    then have trrle: "trace (c ⋅⇩m (x1 1 * ρ * adjoint (x1 1))) ≤ 1" using Suc by auto
    have "x1 1 * (complex_of_real c ⋅⇩m ρ) * adjoint (x1 1) = complex_of_real c ⋅⇩m (x1 1 * ρ * adjoint (x1 1))"
      apply (mat_assoc d) using Suc.prems(1) assms measurement_dim by auto
    then have "denote x2 (x1 1 * (complex_of_real c ⋅⇩m ρ) * adjoint (x1 1)) =  (denote x2 (c ⋅⇩m (x1 1 * (ρ) * adjoint (x1 1))))"
      by auto
    moreover have "denote x2 (c ⋅⇩m (x1 1 * ρ * adjoint (x1 1))) = c ⋅⇩m denote x2 (x1 1 * ρ * adjoint (x1 1))"
      using assms(4) dim1 pdo1 trrle by auto
    ultimately have "denote x2 (x1 1 * (complex_of_real c ⋅⇩m ρ) * adjoint (x1 1)) = c ⋅⇩m denote x2 (x1 1 * ρ * adjoint (x1 1))"
      using assms by auto
    then show ?thesis using Suc dimr pdor trrc by auto
  qed
qed
  
lemma denote_while_scale:
  fixes c:: real
  assumes "ρ ∈ carrier_mat d d"
    "partial_density_operator ρ"
    "trace (c ⋅⇩m ρ) ≤ 1" "c ≥ 0"
    "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 "denote_while (x1 0) (x1 1) (denote x2) (c ⋅⇩m ρ) = c ⋅⇩m denote_while (x1 0) (x1 1) (denote x2) ρ"
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 ?A * ?A + adjoint ?B * ?B = 1⇩m d" using measurement_id2 assms by auto
  have ms: "matrix_seq d (matrix_sum d (λn. denote_while_n ?A ?B (denote x2) n ρ))"   
    using denote_while_n_sum_mat_seq assms measurement_dim by auto

  have trcless: "trace (c ⋅⇩m matrix_sum d (λn. denote_while_n (x1 0) (x1 1) (denote x2) n ρ) n) ≤ 1" for n
  proof -
    have dimr: "matrix_sum d (λn. denote_while_n (x1 0) (x1 1) (denote x2) n ρ) n ∈ carrier_mat d d"   
      using assms dx2 denote_while_n_dim matrix_sum_dim 
      using matrix_seq.dim ms by auto 
    have "trace (matrix_sum d (λn. denote_while_n ?A ?B (denote x2) n ρ) n) ≤ trace ρ"
      using denote_while_n_sum_trace dx2 lo1 assms measurement_dim by auto
    moreover have "trace (c ⋅⇩m matrix_sum d (λn. denote_while_n (x1 0) (x1 1) (denote x2) n ρ) n) = c * trace (matrix_sum d (λn. denote_while_n (x1 0) (x1 1) (denote x2) n ρ) n)"
      using trace_smult dimr by auto
    moreover have "trace (c ⋅⇩m ρ) =  c * trace ρ"  using trace_smult assms by auto        
    ultimately have "trace (c ⋅⇩m matrix_sum d (λn. denote_while_n (x1 0) (x1 1) (denote x2) n ρ) n) ≤ trace (c ⋅⇩m ρ)"
      using  assms(4) by (simp add: ordered_comm_semiring_class.comm_mult_left_mono less_eq_complex_def)
    then show ?thesis
      using assms by auto
  qed

  have llscale: "matrix_seq.lowner_lub  (λn. c ⋅⇩m (matrix_sum d (λn. denote_while_n ?A ?B (denote x2) n ρ)) n) 
    = c ⋅⇩m matrix_seq.lowner_lub (matrix_sum d (λn. denote_while_n ?A ?B (denote x2) n ρ))"
    using lowner_lub_scale[of d "(matrix_sum d (λn. denote_while_n (x1 0) (x1 1) (denote x2) n ρ))" c] ms trcless assms(4) by auto
  have "matrix_sum d (λn. denote_while_n (x1 0) (x1 1) (denote x2) n (complex_of_real c ⋅⇩m ρ)) m 
    = c ⋅⇩m (matrix_sum d (λn. denote_while_n ?A ?B (denote x2) n ρ)) m"
    for m
  proof -
    have  dim:"(⋀k. k < m ⟹ denote_while_n (x1 0) (x1 1) (denote x2) k ρ ∈ carrier_mat d d)" 
      using denote_while_n_dim dx2  assms measurement_dim by auto
    then have dimr: "(⋀k. k < m ⟹ c ⋅⇩m denote_while_n (x1 0) (x1 1) (denote x2) k ρ ∈ carrier_mat d d)"
      using smult_carrier_mat by auto
    have "∀ n<m. 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 ρ)"
      using denote_while_n_scale assms by auto
    then have "(matrix_sum d (λn. c ⋅⇩m denote_while_n ?A ?B (denote x2) n ρ)) m = 
      matrix_sum d (λn. denote_while_n (x1 0) (x1 1) (denote x2) n (complex_of_real c ⋅⇩m ρ)) m "
      using matrix_sum_cong[of m "λn. complex_of_real c ⋅⇩m denote_while_n (x1 0) (x1 1) (denote x2) n ρ"] dimr 
      by fastforce
    moreover have "(matrix_sum d (λn. c ⋅⇩m denote_while_n ?A ?B (denote x2) n ρ)) m = c ⋅⇩m (matrix_sum d (λn. denote_while_n ?A ?B (denote x2) n ρ)) m"
      using matrix_sum_smult[of m "(λn. denote_while_n (x1 0) (x1 1) (denote x2) n ρ)" d c] dim by auto
    ultimately show ?thesis by auto
  qed
  then have "matrix_seq.lowner_lub (matrix_sum d (λn. denote_while_n (x1 0) (x1 1) (denote x2) n (complex_of_real c ⋅⇩m ρ))) =
    matrix_seq.lowner_lub (λn. c ⋅⇩m (matrix_sum d (λn. denote_while_n ?A ?B (denote x2) n ρ)) n)"
    by meson
  then show ?thesis
    unfolding denote_while_def matrix_inf_sum_def using llscale by auto
qed
 
lemma denote_scale:
  fixes c :: real
  assumes "c≥0"
  shows "well_com S ⟹ ρ ∈ carrier_mat d d ⟹ partial_density_operator ρ ⟹
         trace (c  ⋅⇩m ρ) ≤ 1 ⟹ denote S (c  ⋅⇩m ρ) = c  ⋅⇩m denote S ρ"
proof (induction arbitrary: ρ)
  case SKIP
  then show ?case by auto
next
  case (Utrans x)
  then show ?case
    unfolding denote.simps apply (mat_assoc d) using Utrans by auto
next
  case (Seq x1 x2a)
  then show ?case
  proof -
    have cd: "denote x1 (c ⋅⇩m ρ) = c ⋅⇩m denote x1 ρ" using Seq by auto
    have x1: "denote x1 ρ ∈ carrier_mat d d ∧ partial_density_operator (denote x1 ρ) ∧ trace (denote x1 ρ) ≤ trace ρ" 
      using denote_positive_trace_dim Seq denote_partial_density_operator by auto
    have "trace (c ⋅⇩m denote x1 ρ) = c * trace (denote x1 ρ)" using trace_smult x1 by auto
    also have "… ≤ c * trace ρ" using x1 assms 
      by (metis Seq.prems cd denote_positive_trace_dim partial_density_operator_def positive_scale smult_carrier_mat trace_smult well_com.simps(3))
    also have "… ≤ 1" using Seq(6) trace_smult Seq(4) 
      by (simp add: trace_smult)
    finally have "trace (c ⋅⇩m denote x1 ρ) ≤1" by auto
    then have "denote x2a (c ⋅⇩m denote x1 ρ) = c ⋅⇩m denote x2a ( denote x1 ρ)" using x1 Seq by auto
    then show ?thesis using denote.simps(4) cd 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
    have cad: "x2a k * (c ⋅⇩m ρ) * adjoint (x2a k) = c ⋅⇩m (x2a k * ρ * adjoint (x2a k))"
      if k: "k < x1" for k
      apply (mat_assoc d) using well_com.simps Measure measurement_dim k by auto
    have "∀k<x1. x2a k * ρ * adjoint (x2a k) ∈ carrier_mat d d"
      using Measure(2) measurement_dim Measure(3) by fastforce
    have lea: "∀k<x1. adjoint (x2a k) * x2a k ≤⇩L 1⇩m d" using measurement_le_one_mat Measure(2) by auto
    then have pdox: "∀ k<x1. partial_density_operator (x2a k * ρ * adjoint (x2a k))"
      using pdo_close_under_measurement Measure(2,3,4) measurement_dim  
      by (meson state_sig.well_com.simps(4))
    have x2aa:"∀ k < x1. (x2a k * ρ * adjoint (x2a k)) ∈ carrier_mat d d" using Measure(2,3) measurement_dim by fastforce
    have dimm: "(⋀k. k < x1 ⟹ (map denote x3a ! k) (x2a k * ρ * adjoint (x2a k)) ∈ carrier_mat d d)"
      using map_denote_positive_trace_dim Measure(2,3,4) ptc by auto
    then have dimcm: "(⋀k. k < x1 ⟹ c ⋅⇩m (map denote x3a ! k) (x2a k * ρ * adjoint (x2a k)) ∈ carrier_mat d d)"
      using smult_carrier_mat by auto
    
    have tra: "∀ k < x1. trace ((x2a k * ρ * adjoint (x2a k))) ≤ trace ρ"
      using trace_decrease_mul_adj Measure lea measurement_dim by auto

    have tra1: "trace (c ⋅⇩m (x2a k * ρ * adjoint (x2a k))) ≤ 1" if k: "k < x1" for k
    proof -
      have trle: "trace (x2a k * ρ * adjoint (x2a k)) ≤ trace ρ" using tra k by auto
      have "trace (c ⋅⇩m (x2a k * ρ * adjoint (x2a k))) = c * trace ((x2a k * ρ * adjoint (x2a k)))"
        using trace_smult x2aa k by auto
      also have "… ≤ c * trace ρ" 
        using trle assms mulfact  by auto
      also have "… ≤ 1" using Measure(3,5) trace_smult  by metis
      finally show ?thesis by auto
    qed

    have "(map denote x3a ! k) (x2a k * (c ⋅⇩m ρ) * adjoint (x2a k)) 
        = c ⋅⇩m (map denote x3a ! k) (x2a k * ρ * adjoint (x2a k))" if k: "k < x1" for k
    proof -
      have "denote (x3a ! k) (x2a k * (c ⋅⇩m ρ) * adjoint (x2a k)) = denote (x3a ! k) (c ⋅⇩m (x2a k * ρ * adjoint (x2a k)))"
        using cad k by auto
      also have "… = c ⋅⇩m denote (x3a ! k) ( (x2a k * ρ * adjoint (x2a k)))"
        using Measure(1,2) pdox x2aa tra1 k using measure_well_com by auto
      finally have "denote (x3a ! k) (x2a k * (complex_of_real c ⋅⇩m ρ) * adjoint (x2a k)) = complex_of_real c ⋅⇩m denote (x3a ! k) (x2a k * ρ * adjoint (x2a k))"
        by auto
      then show ?thesis using Measure.prems(1) k by auto
    qed

    then have "matrix_sum d (λk. c ⋅⇩m (map denote x3a ! k) (x2a k * ρ * adjoint (x2a k))) x1 =
      matrix_sum d (λk. (map denote x3a ! k) (x2a k * (c ⋅⇩m ρ) * adjoint (x2a k))) x1"
      using matrix_sum_cong[of x1 "(λk. complex_of_real c ⋅⇩m (map denote x3a ! k) (x2a k * ρ * adjoint (x2a k)))" 
        "(λk. (map denote x3a ! k) (x2a k * (complex_of_real c ⋅⇩m ρ) * adjoint (x2a k)))"] dimcm by auto
    then have "matrix_sum d (λk. (map denote x3a ! k) (x2a k * (c ⋅⇩m ρ) * adjoint (x2a k))) x1 =
       c ⋅⇩m matrix_sum d (λk. (map denote x3a ! k) (x2a k * ρ * adjoint (x2a k))) x1"
      using matrix_sum_smult[of x1 "(λk. (map denote x3a ! k) (x2a k * ρ * adjoint (x2a k)))" d c] dimm by auto
    then have "denote (Measure x1 x2a x3a) (c ⋅⇩m ρ) = c ⋅⇩m denote (Measure x1 x2a x3a) ρ"
    using denote.simps(4)[of x1 x2a x3a "c ⋅⇩m ρ"] 
    using denote.simps(4)[of x1 x2a x3a "ρ"] unfolding denote_measure_def by auto
  then show ?thesis by auto
qed     
next
  case (While x1 x2a)
  then show ?case
    apply auto
    using denote_while_scale assms by auto
qed

lemma limit_mat_denote_while_n:
  assumes wc: "well_com (While M S)" and dr: "ρ ∈ carrier_mat d d" and pdor: "partial_density_operator ρ"
  shows "limit_mat (matrix_sum d (λk. denote_while_n (M 0) (M 1) (denote S) k ρ)) (denote (While M S) ρ) d"
proof -
  have m: "measurement d 2 M" using wc by auto
  then have dM0: "M 0 ∈ carrier_mat d d" and dM1: "M 1 ∈ carrier_mat d d" and id: "adjoint (M 0) * (M 0) + adjoint (M 1) * (M 1) = 1⇩m d" 
    using measurement_id2 m measurement_def by auto
  have wcs: "well_com S" using wc by auto
  have DS: "positive (denote S ρ) ∧ trace (denote S ρ) ≤ trace ρ ∧ denote S ρ ∈ carrier_mat d d" 
    if "ρ ∈ carrier_mat d d" and "partial_density_operator ρ" for ρ
    using wcs that denote_positive_trace_dim by auto

  have sumdd: "(∀n. matrix_sum d (λn. denote_while_n (M 0) (M 1) (denote S) n ρ) n ∈ carrier_mat d d)" 
    if "ρ ∈ carrier_mat d d" and "partial_density_operator ρ" for ρ
    using denote_while_n_sum_dim dM0 dM1 DS that by auto
  have sumtr: "∀ n. trace (matrix_sum d (λn. denote_while_n (M 0) (M 1) (denote S) n ρ) n) ≤ trace ρ"
    if "ρ ∈ carrier_mat d d" and "partial_density_operator ρ" for ρ
    using denote_while_n_sum_trace[OF dM0 dM1 id DS] that by auto
  have sumpar: "(∀n. partial_density_operator (matrix_sum d (λn. denote_while_n (M 0) (M 1) (denote S) n ρ) n))"
    if "ρ ∈ carrier_mat d d" and "partial_density_operator ρ" for ρ
    using denote_while_n_sum_partial_density[OF dM0 dM1 id DS] that by auto
  have sumle:"(∀n. matrix_sum d (λn. denote_while_n (M 0) (M 1) (denote S) n ρ) n ≤⇩L matrix_sum d (λn. denote_while_n (M 0) (M 1) (denote S) n ρ) (Suc n))"
    if "ρ ∈ carrier_mat d d" and "partial_density_operator ρ" for ρ
    using denote_while_n_sum_lowner_le[OF dM0 dM1 id DS] that by auto
  have seqd: "matrix_seq d (matrix_sum d (λn. denote_while_n (M 0) (M 1) (denote S) n ρ))"
    if "ρ ∈ carrier_mat d d" and "partial_density_operator ρ" for ρ
    using matrix_seq_def sumdd sumpar sumle that by auto

  have "matrix_seq.lowner_is_lub (matrix_sum d (λn. denote_while_n (M 0) (M 1) (denote S) n ρ))
    (matrix_seq.lowner_lub (matrix_sum d (λn. denote_while_n (M 0) (M 1) (denote S) n ρ)))"
    using DS lowner_is_lub_matrix_sum dM0 dM1 id pdor dr by auto
  then show "limit_mat (matrix_sum d (λk. denote_while_n (M 0) (M 1) (denote S) k ρ)) (denote (While M S) ρ) d"
    unfolding denote.simps denote_while_def matrix_inf_sum_def using matrix_seq.lowner_lub_is_limit[OF seqd[OF dr pdor]]  by auto
qed

end

end