Theory Partial_State
section ‹Partial state›
theory Partial_State
imports Quantum_Program Deep_Learning.Tensor_Matricization
begin
lemma nths_intersection_eq:
assumes "{0..<length xs} ⊆ A"
shows "nths xs B = nths xs (A ∩ B)"
proof -
have "⋀x. x ∈ set (zip xs [0..<length xs]) ⟹ snd x < length xs"
by (metis atLeastLessThan_iff atLeastLessThan_upt in_set_zip nth_mem)
then have "⋀x. x ∈ set (zip xs [0..<length xs]) ⟹ snd x ∈ A" using assms by auto
then have eqp: "⋀x. x ∈ set (zip xs [0..<length xs]) ⟹ snd x ∈ B = (snd x ∈ (A ∩ B))" by simp
then have "filter (λp. snd p ∈ B) (zip xs [0..<length xs]) = filter (λp. snd p ∈ (A ∩ B)) (zip xs [0..<length xs])"
using filter_cong[of "(zip xs [0..<length xs])" "(zip xs [0..<length xs])", OF _ eqp] by auto
then show "nths xs B = nths xs (A ∩ B)" unfolding nths_def by auto
qed
lemma nths_minus_eq:
assumes "{0..<length xs} ⊆ A"
shows "nths xs (-B) = nths xs (A - B)"
proof -
have "⋀x. x ∈ set (zip xs [0..<length xs]) ⟹ snd x < length xs"
by (metis atLeastLessThan_iff atLeastLessThan_upt in_set_zip nth_mem)
then have "⋀x. x ∈ set (zip xs [0..<length xs]) ⟹ snd x ∈ A" using assms by auto
then have eqp: "⋀x. x ∈ set (zip xs [0..<length xs]) ⟹ snd x ∈ (-B) = (snd x ∈ (A - B))" by simp
then have "filter (λp. snd p ∈ (-B)) (zip xs [0..<length xs]) = filter (λp. snd p ∈ (A-B)) (zip xs [0..<length xs])"
using filter_cong[of "(zip xs [0..<length xs])" "(zip xs [0..<length xs])", OF _ eqp] by auto
then show "nths xs (-B) = nths xs (A - B)" unfolding nths_def by auto
qed
lemma nths_split_complement_eq:
assumes "A ∩ B = {}"
and "{0..<length xs} ⊆ A ∪ B"
shows "nths xs A = nths xs (-B)"
proof -
have "nths xs (-B) = nths xs (A ∪ B - B)" using nths_minus_eq assms by auto
moreover have "A ∪ B - B = A" using assms by auto
ultimately show ?thesis by auto
qed
lemma lt_set_card_lt:
fixes A :: "nat set"
assumes "finite A" and "x ∈ A"
shows "card {y. y ∈ A ∧ y < x} < card A"
proof -
have "x ∉ {y. y ∈ A ∧ y < x}" by auto
then have "{y. y ∈ A ∧ y < x} ⊆ A - {x}" by auto
then have "card {y. y ∈ A ∧ y < x} ≤ card (A - {x})"
using card_mono finite_Diff[OF assms(1)] by auto
also have "… < card A" using card_Diff1_less[OF assms] by auto
finally show ?thesis by auto
qed
definition ind_in_set where
"ind_in_set A x = card {i. i ∈ A ∧ i < x}"
lemma bij_ind_in_set_bound:
fixes M :: "nat" and v0 :: "nat set"
assumes "⋀x. f x = card {y. y ∈ v0 ∧ y < x}"
shows "bij_betw f ({0..<M} ∩ v0) {0..<card ({0..<M} ∩ v0)}"
unfolding bij_betw_def
proof
let ?dom = "{0..<M} ∩ v0"
let ?ran = "{0..<card ({0..<M} ∩ v0)}"
{
fix x1 x2 :: nat assume x1: "x1 ∈ ?dom" and x2: "x2 ∈ ?dom" and "f x1 = f x2"
then have "card {y. y ∈ v0 ∧ y < x1} = card {y. y ∈ v0 ∧ y < x2}" using assms by auto
then have "pick v0 (card {y. y ∈ v0 ∧ y < x1}) = pick v0 (card {y. y ∈ v0 ∧ y < x2})" by auto
moreover have "pick v0 (card {y. y ∈ v0 ∧ y < x1}) = x1" using pick_card_in_set x1 by auto
moreover have "pick v0 (card {y. y ∈ v0 ∧ y < x2}) = x2" using pick_card_in_set x2 by auto
ultimately have "x1 = x2" by auto
}
then show "inj_on f ?dom" unfolding inj_on_def by auto
{
fix x assume x: "x ∈ ?dom"
then have "(y ∈ v0 ∧ y < x) = (y ∈ ?dom ∧ y < x)" for y using x by auto
then have "card {y. y ∈ v0 ∧ y < x} = card {y. y ∈ ?dom ∧ y < x}" by auto
moreover have "card {y. y ∈ ?dom ∧ y < x} < card ?dom" using x lt_set_card_lt[of ?dom] by auto
ultimately have "f x ∈ ?ran" using assms by auto
}
then have sub: "(f ` ?dom) ⊆ ?ran" by auto
{
fix y assume y: "y ∈ ?ran"
then have yle: "y < card ?dom" by auto
then have pyindom: "pick ?dom y ∈ ?dom" using pick_in_set_le[of y ?dom] by auto
then have "pick ?dom y < M" by auto
then have "⋀z. (z < pick ?dom y ⟹ z ∈ v0 = (z ∈ ?dom))" by auto
then have "{z. z ∈ v0 ∧ z < pick ?dom y} = {z. z ∈ ?dom ∧ z < pick ?dom y}" by auto
then have "card {z. z ∈ v0 ∧ z < pick ?dom y} = card {z. z ∈ ?dom ∧ z < pick ?dom y}" by auto
then have "f (pick ?dom y) = y" using card_pick_le[OF yle] assms by auto
with pyindom have "∃x∈?dom. f x = y" by auto
}
then have sup: "?ran ⊆ (f ` ?dom)" by fastforce
show "(f ` ?dom) = ?ran" using sub sup by auto
qed
lemma ind_in_set_bound:
fixes A :: "nat set" and M N :: "nat"
assumes "N ≥ M"
shows "ind_in_set A N ∉ (ind_in_set A ` ({0..<M} ∩ A))"
proof -
have "{0..<M}∩A ⊆ {i. i ∈ A ∧ i < N}" using assms by auto
then have "card ({0..<M}∩A) ≤ card {i. i ∈ A ∧ i < N}"
using card_mono[of "{i. i ∈ A ∧ i < N}"] by auto
moreover have "ind_in_set A N = card {i. i ∈ A ∧ i < N}" unfolding ind_in_set_def by auto
ultimately have "ind_in_set A N ≥ card ({0..<M}∩A)" by auto
moreover have "y ∈ ind_in_set A ` (A ∩ {0..<M}) ⟹ y < card ({0..<M}∩A)" for y
proof -
let ?dom = "{0..<M} ∩ A"
assume "y ∈ ind_in_set A ` (A ∩ {0..<M})"
then obtain x where x: "x ∈ ?dom" and y: "ind_in_set A x = y" by auto
then have "(y ∈ A ∧ y < x) = (y ∈ ?dom ∧ y < x)" for y using x by auto
then have "card {y. y ∈ A ∧ y < x} = card {y. y ∈ ?dom ∧ y < x}" by auto
moreover have "card {y. y ∈ ?dom ∧ y < x} < card ?dom" using x lt_set_card_lt[of ?dom] by auto
ultimately show "y < card ({0..<M}∩A)" using y unfolding ind_in_set_def by auto
qed
ultimately show ?thesis by fastforce
qed
lemma bij_minus_subset:
"bij_betw f A B ⟹ C ⊆ A ⟹ (f ` A) - (f ` C) = f ` (A - C)"
by (metis Diff_subset bij_betw_imp_inj_on bij_betw_imp_surj_on inj_on_image_set_diff)
lemma ind_in_set_minus_subset_bound:
fixes A B :: "nat set" and M :: "nat"
assumes "B ⊆ A"
shows "(ind_in_set A ` ({0..<M} ∩ A)) - (ind_in_set A ` B) = (ind_in_set A ` ({0..<M} ∩ A)) ∩ (ind_in_set A ` (A - B))"
proof -
let ?dom = "{0..<M} ∩ A"
let ?ran = "{0..<card ({0..<M} ∩ A)}"
let ?f = "ind_in_set A"
let ?C = "A - B"
have bij: "bij_betw ?f ?dom ?ran"
using bij_ind_in_set_bound[of "?f" A M] unfolding ind_in_set_def by auto
then have eq: "?f ` ?dom = ?ran" using bij_betw_imp_surj_on by fastforce
have "(?f ` B) = (?f ` ({0..<M} ∩ B)) ∪ (?f ` ({n. n ≥ M} ∩ B))"
by fastforce
then have "(?f ` ?dom) - (?f ` B)
= (?f ` ?dom) - (?f ` ({n. n ≥ M} ∩ B)) - (?f ` ({0..<M} ∩ B))"
by fastforce
moreover have "(?f ` ({n. n ≥ M} ∩ B)) ∩ (?f ` ?dom) = {}" using ind_in_set_bound[of M _ A] by auto
ultimately have eq1: "(?f ` ?dom) - (?f ` B) = (?f ` ?dom) - (?f ` ({0..<M} ∩ B))" by auto
have "{0..<M} ∩ B ⊆ ?dom" using assms by auto
then have "(?f ` ?dom) - (?f ` ({0..<M} ∩ B)) = ?f ` (?dom - ({0..<M} ∩ B))"
using bij bij_minus_subset[of "?f"] by auto
also have "… = ?f ` ({0..<M} ∩ ?C)" by auto
finally have eq2: "(?f ` ?dom) - (?f ` B) = ?f ` ({0..<M} ∩ ?C)" using eq1 by auto
have "(?f ` ?C) = (?f ` ({0..<M} ∩ ?C)) ∪ (?f ` ({n. n ≥ M} ∩ ?C))" by fastforce
moreover have "(?f ` ({n. n ≥ M} ∩ ?C)) ∩ (?f ` ?dom) = {}" using ind_in_set_bound[of M _ A] by auto
ultimately have eq3:"(ind_in_set A ` ?dom) ∩ (?f ` ?C) = (ind_in_set A ` ?dom) ∩ (?f ` ({0..<M} ∩ ?C))" by auto
have "{0..<M} ∩ ?C ⊆ ?dom" using assms by auto
then have "(ind_in_set A ` ?dom) ∩ (?f ` ({0..<M} ∩ ?C)) = (?f ` ({0..<M} ∩ ?C))" using bij by fastforce
then show ?thesis using eq2 eq3 by auto
qed
lemma ind_in_set_iff:
fixes A B :: "nat set"
assumes "x ∈ A" and "B ⊆ A"
shows "ind_in_set A x ∈ (ind_in_set A ` B) = (x ∈ B)"
proof
have lemm: "card {i. i ∈ A ∧ i < (x::nat) } = card {i. i ∈ A ∧ i < (y::nat) } ⟹ x ∈ A ⟹ y ∈ A ⟹ x = y" for A x y
by (metis (full_types) pick_card_in_set)
{
assume "ind_in_set A x ∈ (ind_in_set A ` B)"
then have "∃y ∈ B. card {i ∈ A. i < x} = card {i ∈ A. i < y}" unfolding ind_in_set_def by auto
then obtain y where y1: "y ∈ B" and ceq: "card {i ∈ A. i < x} = card {i ∈ A. i < y}" by auto
with y1 assms have y0: "y ∈ A" by auto
then have "x = y" using lemm[OF ceq] y0 assms by auto
then show "x ∈ B" using y1 by auto
}
qed (simp add: ind_in_set_def)
lemma nths_reencode_eq:
assumes "B ⊆ A"
shows "nths (nths xs A) (ind_in_set A ` B) = nths xs B"
proof (induction xs rule: rev_induct)
case Nil
then show ?case by auto
next
case (snoc x xs)
have seteq: "{i. i < length xs ∧ i ∈ A} = {i. i ∈ A ∧ i < length xs}" by auto
show ?case
proof (cases "length xs ∈ B")
case True
have "nths (xs @ [x]) B = nths xs B @ nths [x] {l. l + length xs ∈ B}" using nths_append[of xs] by auto
moreover have "nths [x] {l. l + length xs ∈ B} = [x]" using nths_singleton True by auto
ultimately have eqT1: "nths (xs @ [x]) B = nths xs B @ [x]" by auto
then have "length xs ∈ A" using True assms by auto
then have "nths [x] {l. l + length xs ∈ A} = [x]" using nths_singleton by auto
moreover have "nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs ∈ A}" using nths_append[of xs] by auto
ultimately have "nths (xs @ [x]) A = nths xs A @ [x]" by auto
then have eqT2: "nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (nths xs A @ [x]) (ind_in_set A ` B)" by auto
have eqT3: "nths (nths xs A @ [x]) (ind_in_set A ` B)
= nths xs B @ (nths [x] {l. l + length (nths xs A) ∈ (ind_in_set A ` B)})"
using nths_append[of "nths xs A"] snoc by auto
have "ind_in_set A (length xs) = card {i. i < length xs ∧ i ∈ A}" using ind_in_set_def seteq by auto
moreover have "length (nths xs A) = card {i. i < length xs ∧ i ∈ A}" using length_nths by auto
ultimately have "length (nths xs A) = ind_in_set A (length xs)" by auto
moreover have "ind_in_set A (length xs) ∈ ind_in_set A ` B" using True by auto
ultimately have "length (nths xs A) ∈ ind_in_set A ` B" by auto
then have "(nths [x] {l. l + length (nths xs A) ∈ (ind_in_set A ` B)}) = [x]" using nths_singleton by auto
then have "nths (nths xs A @ [x]) (ind_in_set A ` B) = nths xs B @ [x]" using eqT3 by auto
then show ?thesis using eqT1 eqT2 by auto
next
case False
have "nths (xs @ [x]) B = nths xs B @ nths [x] {l. l + length xs ∈ B}" using nths_append[of xs] by auto
moreover have "nths [x] {l. l + length xs ∈ B} = []" using nths_singleton False by auto
ultimately have eqT1: "nths (xs @ [x]) B = nths xs B" by auto
have "nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B"
proof (cases "length xs ∈ A")
case True
then have "nths [x] {l. l + length xs ∈ A} = [x]" using nths_singleton by auto
moreover have "nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs ∈ A}" using nths_append[of xs] by auto
ultimately have "nths (xs @ [x]) A = nths xs A @ [x]" by auto
then have "nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths (nths xs A @ [x]) (ind_in_set A ` B)" by auto
then have eqT2: "nths (nths (xs @ [x]) A) (ind_in_set A ` B)
= nths xs B @ (nths [x] {l. l + length (nths xs A) ∈ (ind_in_set A ` B)})"
using nths_append[of "nths xs A"] snoc by auto
have "length (nths xs A) ∈ (ind_in_set A ` B) ⟹ length xs ∈ B"
proof -
assume "length (nths xs A) ∈ (ind_in_set A ` B)"
moreover have "length (nths xs A) = card {i. i ∈ A ∧ i < length xs}"
using length_nths[of xs] seteq by auto
ultimately have "card {i. i ∈ A ∧ i < length xs} ∈ (ind_in_set A ` B)" unfolding ind_in_set_def by auto
then show "length xs ∈ B" using ind_in_set_iff True assms unfolding ind_in_set_def by auto
qed
then have "length (nths xs A) ∉ (ind_in_set A ` B)" using False by auto
then have "nths [x] {l. l + length (nths xs A) ∈ (ind_in_set A ` B)} = []" using nths_singleton by auto
then show "nths (nths (xs @ [x]) A) (ind_in_set A ` B) = nths xs B" using eqT2 by auto
next
case False
then have "nths [x] {l. l + length xs ∈ A} = []" using nths_singleton by auto
moreover have "nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs ∈ A}" using nths_append[of xs] by auto
ultimately have "nths (xs @ [x]) A = nths xs A" by auto
then show ?thesis using snoc by auto
qed
with eqT1 show ?thesis by auto
qed
qed
lemma nths_reencode_eq_comp:
assumes "B ⊆ A"
shows "nths (nths xs A) (- ind_in_set A ` B) = nths xs (A - B)"
proof (induction xs rule: rev_induct)
case Nil
then show ?case by auto
next
case (snoc x xs)
have sub20: "A - B ⊆ A" using assms by auto
have seteq: "{i. i < length xs ∧ i ∈ A} = {i. i ∈ A ∧ i < length xs}" by auto
show ?case
proof (cases "length xs ∈ (A - B)")
case True
have "nths (xs @ [x]) (A - B) = nths xs (A - B) @ nths [x] {l. l + length xs ∈ (A - B)}" using nths_append[of xs] by auto
moreover have "nths [x] {l. l + length xs ∈ (A - B)} = [x]" using nths_singleton True by auto
ultimately have eqT1: "nths (xs @ [x]) (A - B) = nths xs (A - B) @ [x]" by auto
then have "length xs ∈ A" using True sub20 by auto
then have "nths [x] {l. l + length xs ∈ A} = [x]" using nths_singleton by auto
moreover have "nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs ∈ A}" using nths_append[of xs] by auto
ultimately have "nths (xs @ [x]) A = nths xs A @ [x]" by auto
then have "nths (nths (xs @ [x]) A) (- (ind_in_set A) ` B) = nths (nths xs A @ [x]) (- (ind_in_set A) ` B)" by auto
then have eqT2: "nths (nths (xs @ [x]) A) (- (ind_in_set A) ` B)
= nths xs (A - B) @ (nths [x] {l. l + length (nths xs A) ∈ (- (ind_in_set A) ` B)})"
using nths_append[of "nths xs A"] snoc by auto
have "length (nths xs A) ∈ ((ind_in_set A) ` B) ⟹ length xs ∈ B"
proof -
assume "length (nths xs A) ∈ ((ind_in_set A) ` B)"
moreover have "length (nths xs A) = card {i. i ∈ A ∧ i < length xs}"
using length_nths[of xs] seteq by auto
ultimately have "ind_in_set A (length xs) ∈ (ind_in_set A ` B)" unfolding ind_in_set_def by auto
then show "length xs ∈ B" using ind_in_set_iff True assms by auto
qed
moreover have "length xs ∉ B" using True by auto
ultimately have "length (nths xs A) ∈ (- (ind_in_set A) ` B)" by auto
then have "nths [x] {l. l + length (nths xs A) ∈ (- (ind_in_set A) ` B)} = [x]"
using nths_singleton by auto
then have "nths (nths (xs @ [x]) A) (- (ind_in_set A) ` B) = nths xs (A - B) @ [x]" using eqT2 by auto
then show ?thesis using eqT1 by auto
next
case False
have "nths (xs @ [x]) (A - B) = nths xs (A - B) @ nths [x] {l. l + length xs ∈ (A - B)}" using nths_append[of xs] by auto
moreover have "nths [x] {l. l + length xs ∈ (A - B)} = []" using nths_singleton False by auto
ultimately have eqT1: "nths (xs @ [x]) (A - B) = nths xs (A - B)" by auto
have "nths (nths (xs @ [x]) A) (- (ind_in_set A) ` B) = nths xs (A - B)"
proof (cases "length xs ∈ A")
case True
then have True1: "length xs ∈ B" using False by auto
then have "nths [x] {l. l + length xs ∈ A} = [x]" using nths_singleton True by auto
moreover have "nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs ∈ A}" using nths_append[of xs] by auto
ultimately have "nths (xs @ [x]) A = nths xs A @ [x]" by auto
then have "nths (nths (xs @ [x]) A) (- (ind_in_set A) ` B) = nths (nths xs A @ [x]) (- (ind_in_set A) ` B)" by auto
then have eqT2: "nths (nths (xs @ [x]) A) (- (ind_in_set A) ` B)
= nths xs (A - B) @ (nths [x] {l. l + length (nths xs A) ∈ (- (ind_in_set A) ` B)})"
using nths_append[of "nths xs A"] snoc by auto
have "length (nths xs A) ∈ ((ind_in_set A) ` B)"
proof -
have "length (nths xs A) = card {i. i ∈ A ∧ i < length xs}"
using length_nths[of xs] seteq by auto
moreover have "card {i. i ∈ A ∧ i < length xs} ∈ (ind_in_set A ` B)"
unfolding ind_in_set_def using True ind_in_set_iff[of "length xs"] True1 by auto
ultimately show "length (nths xs A) ∈ (ind_in_set A) ` B" by auto
qed
then have "nths [x] {l. l + length (nths xs A) ∈ (- (ind_in_set A) ` B)} = []" using nths_singleton by auto
then show "nths (nths (xs @ [x]) A) (- (ind_in_set A) ` B) = nths xs (A - B)" using eqT2 by auto
next
case False
then have "nths [x] {l. l + length xs ∈ A} = []" using nths_singleton by auto
moreover have "nths (xs @ [x]) A = nths xs A @ nths [x] {l. l + length xs ∈ A}" using nths_append[of xs] by auto
ultimately have "nths (xs @ [x]) A = nths xs A" by auto
then show ?thesis using snoc by auto
qed
with eqT1 show ?thesis by auto
qed
qed
lemma nths_prod_list_split:
fixes A :: "nat set" and xs :: "nat list"
assumes "B ⊆ A"
shows "prod_list (nths xs A) = (prod_list (nths xs B)) * (prod_list (nths xs (A - B)))"
proof (induction xs rule: rev_induct)
case Nil
then show ?case by auto
next
let ?C = "A - B"
case (snoc x xs)
have SA: "nths (xs @ [x]) A = nths xs A @ nths [x] {j. j + length xs ∈ A}" using nths_append[of xs] by auto
have SB: "nths (xs @ [x]) B = nths xs B @ nths [x] {j. j + length xs ∈ B}" using nths_append[of xs] by auto
have SC: "nths (xs @ [x]) ?C = nths xs ?C @ nths [x] {j. j + length xs ∈ ?C}" using nths_append[of xs] by auto
show ?case
proof (cases "length xs ∈ A")
case True
then have "nths (xs @ [x]) A = nths xs A @ [x]" using SA by auto
then have eqA: "prod_list (nths (xs @ [x]) A) = prod_list (nths xs A) * x" by auto
show ?thesis
proof (cases "length xs ∈ B")
case True
then have "nths (xs @ [x]) B = nths xs B @ [x]" using SB by auto
then have eqB: "prod_list (nths (xs @ [x]) B) = prod_list (nths xs B) * x" by auto
have "length xs ∉ ?C" using True assms by auto
then have "nths (xs @ [x]) ?C = nths xs ?C" using SC by auto
then have eqC: "prod_list (nths (xs @ [x]) ?C) = prod_list (nths xs ?C)" by auto
then show ?thesis using snoc eqA eqB eqC by auto
next
case False
then have "nths (xs @ [x]) B = nths xs B" using SB by auto
then have eqB: "prod_list (nths (xs @ [x]) B) = prod_list (nths xs B)" by auto
then have "length xs ∈ ?C" using True False assms by auto
then have "nths (xs @ [x]) ?C = nths xs ?C @ [x]" using SC by auto
then have eqC: "prod_list (nths (xs @ [x]) ?C) = prod_list (nths xs ?C) * x" by auto
then show ?thesis using snoc eqA eqB eqC by auto
qed
next
case False
then have ninB: "length xs ∉ B" and ninC: "length xs ∉ ?C" using assms by auto
have "nths (xs @ [x]) A = nths xs A" using SA False nths_singleton by auto
then have eqA: "prod_list (nths (xs @ [x]) A) = prod_list (nths xs A)" by auto
have "nths (xs @ [x]) B = nths xs B" using SB ninB nths_singleton by auto
then have eqB: "prod_list (nths (xs @ [x]) B) = prod_list (nths xs B)" by auto
have "nths (xs @ [x]) ?C = nths xs ?C" using SC ninC nths_singleton by auto
then have eqC: "prod_list (nths (xs @ [x]) ?C) = prod_list (nths xs ?C)" by auto
then show ?thesis using eqA eqB eqC snoc by auto
qed
qed
subsection ‹Encodings›
lemma digit_encode_take:
"take n (digit_encode ds a) = digit_encode (take n ds) a"
proof (induct n arbitrary: ds a)
case 0
then show ?case by auto
next
case (Suc n)
then show ?case
proof (cases ds)
case Nil
then show ?thesis by auto
next
case (Cons d ds')
then show ?thesis by (auto simp add: Suc)
qed
qed
lemma nths_minus_upt_eq_drop:
"nths l (-{..<n}) = drop n l"
apply (induct l rule: rev_induct)
by (auto simp add: nths_append)
lemma digit_encode_drop:
"drop n (digit_encode ds a) = digit_encode (drop n ds) (a div (prod_list (take n ds)))"
proof (induct n arbitrary: ds a)
case 0
then show ?case by auto
next
case (Suc n)
then show ?case
proof (cases ds)
case Nil
then show ?thesis by auto
next
case (Cons d ds')
then show ?thesis by (auto simp add: Suc div_mult2_eq)
qed
qed
text ‹List of active variables in the partial state›
locale partial_state = state_sig +
fixes vars :: "nat set"
context partial_state
begin
text ‹Dimensions of active variables›
abbreviation avars :: "nat set" where
"avars ≡ {0..<length dims}"
definition dims1 :: "nat list" where
"dims1 = nths dims vars"
definition dims2 :: "nat list" where
"dims2 = nths dims (-vars)"
lemma dims1_alter:
assumes "avars ⊆ A"
shows "dims1 = nths dims (A ∩ vars)"
using nths_intersection_eq assms unfolding dims1_def by auto
lemma dims2_alter:
assumes "avars ⊆ A"
shows "dims2 = nths dims (A-vars)"
using nths_minus_eq assms unfolding dims2_def by auto
text ‹Total dimension for the active variables›
definition d1 :: nat where
"d1 = prod_list dims1"
text ‹Total dimension for the non-active variables›
definition d2 :: nat where
"d2 = prod_list dims2"
text ‹Translating dimension in d to dimension in d1›
definition encode1 :: "nat ⇒ nat" where
"encode1 i = digit_decode dims1 (nths (digit_encode dims i) vars)"
lemma encode1_alter:
assumes "avars ⊆ A"
shows "encode1 i = digit_decode dims1 (nths (digit_encode dims i) (A ∩ vars))"
using length_digit_encode[of dims i] nths_intersection_eq[of "digit_encode dims i" A vars] assms unfolding encode1_def
by (subgoal_tac "nths (digit_encode dims i) (vars) = nths (digit_encode dims i) (A ∩ vars)", auto)
text ‹Translating dimension in d to dimension in d2›
definition encode2 :: "nat ⇒ nat" where
"encode2 i = digit_decode dims2 (nths (digit_encode dims i) (-vars))"
lemma encode2_alter:
assumes "avars ⊆ A"
shows "encode2 i = digit_decode dims2 (nths (digit_encode dims i) (A-vars))"
using length_digit_encode[of dims i] nths_minus_eq[of "digit_encode dims i" A] assms unfolding encode2_def
by (subgoal_tac "nths (digit_encode dims i) (- vars) = nths (digit_encode dims i) (A - vars)", auto)
lemma encode1_lt [simp]:
assumes "i < d"
shows "encode1 i < d1"
unfolding d1_def encode1_def apply (rule digit_decode_lt)
using dims1_def assms d_def digit_encode_valid_index valid_index_nths by auto
lemma encode2_lt [simp]:
assumes "i < d"
shows "encode2 i < d2"
unfolding d2_def encode2_def apply (rule digit_decode_lt)
using dims2_def assms d_def digit_encode_valid_index valid_index_nths by auto
text ‹Given dimensions in d1 and d2, form dimension in d›
fun encode12 :: "nat × nat ⇒ nat" where
"encode12 (i, j) = digit_decode dims (weave vars (digit_encode dims1 i) (digit_encode dims2 j))"
declare encode12.simps [simp del]
lemma encode12_inv:
assumes "k < d"
shows "encode12 (encode1 k, encode2 k) = k"
unfolding encode12.simps encode1_def encode2_def
using assms d_def digit_encode_valid_index dims1_def dims2_def valid_index_nths by auto
lemma encode12_inv1:
assumes "i < d1" "j < d2"
shows "encode1 (encode12 (i, j)) = i"
unfolding encode12.simps encode1_def
using assms unfolding d1_def d2_def dims1_def dims2_def
by (metis digit_decode_encode_lt digit_encode_decode digit_encode_valid_index valid_index_weave(1,2))
lemma encode12_inv2:
assumes "i < d1" "j < d2"
shows "encode2 (encode12 (i, j)) = j"
unfolding encode12.simps encode2_def
using assms unfolding d1_def d2_def dims1_def dims2_def
by (metis digit_decode_encode_lt digit_encode_decode digit_encode_valid_index valid_index_weave(1,3))
lemma encode12_lt:
assumes "i < d1" "j < d2"
shows "encode12 (i, j) < d"
using assms unfolding encode12.simps d_def d1_def d2_def dims1_def dims2_def
by (simp add: digit_decode_lt digit_encode_valid_index valid_index_weave(1))
lemma sum_encode: "(∑i = 0..<d1. ∑j = 0..<d2. f i j) = sum (λk. f (encode1 k) (encode2 k)) {0..<d}"
apply (subst sum.cartesian_product)
apply (rule sum.reindex_bij_witness[where i="λk. (encode1 k, encode2 k)" and j=encode12])
by (auto simp: encode12_inv1 encode12_inv2 encode12_inv encode12_lt)
subsection ‹Tensor product of vectors and matrices›
text ‹Given vector v1 of dimension d1, and vector v2 of dimension d2, form
the tensor vector of dimension d1 * d2 = d›
definition tensor_vec :: "'a::times vec ⇒ 'a vec ⇒ 'a vec" where
"tensor_vec v1 v2 = Matrix.vec d (λi. v1 $ encode1 i * v2 $ encode2 i)"
lemma tensor_vec_dim [simp]:
"dim_vec (tensor_vec v1 v2) = d"
unfolding tensor_vec_def by auto
lemma tensor_vec_carrier:
"tensor_vec v1 v2 ∈ carrier_vec d"
unfolding tensor_vec_def by auto
lemma tensor_vec_eval:
assumes "i < d"
shows "tensor_vec v1 v2 $ i = v1 $ encode1 i * v2 $ encode2 i"
unfolding tensor_vec_def using assms by simp
lemma tensor_vec_add1:
fixes v1 v2 v3 :: "'a::comm_ring vec"
assumes "v1 ∈ carrier_vec d1"
and "v2 ∈ carrier_vec d1"
and "v3 ∈ carrier_vec d2"
shows "tensor_vec (v1 + v2) v3 = tensor_vec v1 v3 + tensor_vec v2 v3"
apply (rule eq_vecI, auto)
unfolding tensor_vec_eval
using assms(2) comm_semiring_class.distrib by force
lemma tensor_vec_add2:
fixes v1 v2 v3 :: "'a::comm_ring vec"
assumes "v1 ∈ carrier_vec d1"
and "v2 ∈ carrier_vec d2"
and "v3 ∈ carrier_vec d2"
shows "tensor_vec v1 (v2 + v3) = tensor_vec v1 v2 + tensor_vec v1 v3"
apply (rule eq_vecI, auto)
unfolding tensor_vec_eval
using assms(3) semiring_class.distrib_left by force
text ‹Given d1-by-d1 matrix m1, and d2-by-d2 matrix m2, form d-by-d matrix›
definition tensor_mat :: "'a::comm_ring_1 mat ⇒ 'a mat ⇒ 'a mat" where
"tensor_mat m1 m2 = Matrix.mat d d (λ(i,j).
m1 $$ (encode1 i, encode1 j) * m2 $$ (encode2 i, encode2 j))"
lemma tensor_mat_dim_row [simp]:
"dim_row (tensor_mat m1 m2) = d"
unfolding tensor_mat_def by auto
lemma tensor_mat_dim_col [simp]:
"dim_col (tensor_mat m1 m2) = d"
unfolding tensor_mat_def by auto
lemma tensor_mat_carrier:
"tensor_mat m1 m2 ∈ carrier_mat d d"
unfolding tensor_mat_def by auto
lemma tensor_mat_eval:
assumes "i < d" "j < d"
shows "tensor_mat m1 m2 $$ (i, j) = m1 $$ (encode1 i, encode1 j) * m2 $$ (encode2 i, encode2 j)"
unfolding tensor_mat_def using assms by simp
lemma tensor_mat_zero1:
shows "tensor_mat (0⇩m d1 d1) m1 = 0⇩m d d"
apply (rule eq_matI)
by (auto simp add: tensor_mat_eval)
lemma tensor_mat_zero2:
shows "tensor_mat m1 (0⇩m d2 d2) = 0⇩m d d"
apply (rule eq_matI)
by (auto simp add: tensor_mat_eval)
lemma tensor_mat_add1:
assumes "m1 ∈ carrier_mat d1 d1"
and "m2 ∈ carrier_mat d1 d1"
and "m3 ∈ carrier_mat d2 d2"
shows "tensor_mat (m1 + m2) m3 = tensor_mat m1 m3 + tensor_mat m2 m3"
apply (rule eq_matI, auto)
unfolding tensor_mat_eval
using assms(2) comm_semiring_class.distrib by force
lemma tensor_mat_add2:
assumes "m1 ∈ carrier_mat d1 d1"
and "m2 ∈ carrier_mat d2 d2"
and "m3 ∈ carrier_mat d2 d2"
shows "tensor_mat m1 (m2 + m3) = tensor_mat m1 m2 + tensor_mat m1 m3"
apply (rule eq_matI, auto)
unfolding tensor_mat_eval
using assms(3) semiring_class.distrib_left by force
lemma tensor_mat_minus1:
assumes "m1 ∈ carrier_mat d1 d1"
and "m2 ∈ carrier_mat d1 d1"
and "m3 ∈ carrier_mat d2 d2"
shows "tensor_mat (m1 - m2) m3 = tensor_mat m1 m3 - tensor_mat m2 m3"
apply (rule eq_matI, auto)
unfolding tensor_mat_eval
apply (subst index_minus_mat)
subgoal using assms by auto
subgoal using assms by auto
using assms(2) ring_class.left_diff_distrib by force
lemma tensor_mat_matrix_sum2:
assumes "m1 ∈ carrier_mat d1 d1"
shows "(⋀k. k < n ⟹ f k ∈ carrier_mat d2 d2)
⟹ matrix_sum d (λk. tensor_mat m1 (f k)) n = tensor_mat m1 (matrix_sum d2 f n)"
proof (induct n)
case 0
then show ?case apply simp using tensor_mat_zero2[of m1] by auto
next
case (Suc n)
then have "k < n ⟹ f k ∈ carrier_mat d2 d2" for k by auto
then have ds: "matrix_sum d2 f n ∈ carrier_mat d2 d2" using matrix_sum_dim by auto
have dn: "f n ∈ carrier_mat d2 d2" using Suc by auto
have "matrix_sum d2 f (Suc n) = f n + matrix_sum d2 f n" by simp
then have eq: "tensor_mat m1 (matrix_sum d2 f (Suc n))
= tensor_mat m1 (f n) + tensor_mat m1 (matrix_sum d2 f n)"
using tensor_mat_add2 dn ds assms by auto
have "matrix_sum d (λk. tensor_mat m1 (f k)) (Suc n)
= tensor_mat m1 (f n) + matrix_sum d (λk. tensor_mat m1 (f k)) n" by simp
also have "… = tensor_mat m1 (f n) + tensor_mat m1 (matrix_sum d2 f n)"
using Suc by auto
finally show ?case using eq by auto
qed
lemma tensor_mat_scale1:
assumes "m1 ∈ carrier_mat d1 d1"
and "m2 ∈ carrier_mat d2 d2"
shows "tensor_mat (a ⋅⇩m m1) m2 = a ⋅⇩m tensor_mat m1 m2"
apply (rule eq_matI, auto)
unfolding tensor_mat_eval
using assms comm_semiring_class.distrib by force
lemma tensor_mat_scale2:
assumes "m1 ∈ carrier_mat d1 d1"
and "m2 ∈ carrier_mat d2 d2"
shows "tensor_mat m1 (a ⋅⇩m m2) = a ⋅⇩m tensor_mat m1 m2"
apply (rule eq_matI, auto)
unfolding tensor_mat_eval
using assms comm_semiring_class.distrib by force
lemma tensor_mat_trace:
assumes "m1 ∈ carrier_mat d1 d1"
and "m2 ∈ carrier_mat d2 d2"
shows "trace (tensor_mat m1 m2) = trace m1 * trace m2"
apply (auto simp add: tensor_mat_carrier trace_def tensor_mat_eval)
apply (subst Groups_Big.sum_product)
apply (subst sum_encode[symmetric])
using assms by auto
lemma tensor_mat_id:
"tensor_mat (1⇩m d1) (1⇩m d2) = 1⇩m d"
proof (rule eq_matI, auto)
show "tensor_mat (1⇩m d1) (1⇩m d2) $$ (i, i) = 1" if "i < d" for i
using that by (simp add: tensor_mat_eval)
next
show "tensor_mat (1⇩m d1) (1⇩m d2) $$ (i, j) = 0" if "i < d" "j < d" "i ≠ j" for i j
using that apply (simp add: tensor_mat_eval)
by (metis encode12_inv)
qed
lemma tensor_mat_mult_vec:
assumes "m1 ∈ carrier_mat d1 d1"
and "m2 ∈ carrier_mat d2 d2"
and "v1 ∈ carrier_vec d1"
and "v2 ∈ carrier_vec d2"
shows "tensor_vec (m1 *⇩v v1) (m2 *⇩v v2) = tensor_mat m1 m2 *⇩v tensor_vec v1 v2"
proof (rule eq_vecI, auto)
fix i j :: nat
assume i: "i < d"
let ?i1 = "encode1 i" and ?i2 = "encode2 i"
have "tensor_vec (m1 *⇩v v1) (m2 *⇩v v2) $ i = (m1 *⇩v v1) $ ?i1 * (m2 *⇩v v2) $ ?i2"
using i by (simp add: tensor_vec_eval)
also have "… = (row m1 ?i1 ∙ v1) * (row m2 ?i2 ∙ v2)"
using assms i by auto
also have "… = (∑i = 0..<d1. m1 $$ (?i1, i) * v1 $ i) * (∑j = 0..<d2. m2 $$ (?i2, j) * v2 $ j)"
using assms i by (simp add: scalar_prod_def)
also have "… = (∑i = 0..<d1. ∑j = 0..<d2. (m1 $$ (?i1, i) * v1 $ i) * (m2 $$ (?i2, j) * v2 $ j))"
by (rule Groups_Big.sum_product)
also have "… = (∑i = 0..<d. (m1 $$ (?i1, encode1 i) * v1 $ (encode1 i)) * (m2 $$ (?i2, encode2 i) * v2 $ (encode2 i)))"
by (rule sum_encode)
also have "… = row (tensor_mat m1 m2) i ∙ tensor_vec v1 v2"
apply (simp add: scalar_prod_def tensor_mat_eval tensor_vec_eval i)
by (rule sum.cong, auto)
finally show "tensor_vec (m1 *⇩v v1) (m2 *⇩v v2) $ i = row (tensor_mat m1 m2) i ∙ tensor_vec v1 v2" by auto
qed
lemma tensor_mat_mult:
assumes "m1 ∈ carrier_mat d1 d1"
and "m2 ∈ carrier_mat d1 d1"
and "m3 ∈ carrier_mat d2 d2"
and "m4 ∈ carrier_mat d2 d2"
shows "tensor_mat (m1 * m2) (m3 * m4) = tensor_mat m1 m3 * tensor_mat m2 m4"
proof (rule eq_matI, auto)
fix i j :: nat
assume i: "i < d" and j: "j < d"
let ?i1 = "encode1 i" and ?i2 = "encode2 i" and ?j1 = "encode1 j" and ?j2 = "encode2 j"
have "tensor_mat (m1 * m2) (m3 * m4) $$ (i, j) = (m1 * m2) $$ (?i1, ?j1) * (m3 * m4) $$ (?i2, ?j2)"
using i j by (simp add: tensor_mat_eval)
also have "… = (row m1 ?i1 ∙ col m2 ?j1) * (row m3 ?i2 ∙ col m4 ?j2)"
using assms i j by auto
also have "… = (∑i = 0..<d1. m1 $$ (?i1, i) * m2 $$ (i, ?j1)) * (∑j = 0..<d2. m3 $$ (?i2, j) * m4 $$ (j, ?j2))"
using assms i j by (simp add: scalar_prod_def)
also have "… = (∑i = 0..<d1. ∑j = 0..<d2. (m1 $$ (?i1, i) * m2 $$ (i, ?j1)) * (m3 $$ (?i2, j) * m4 $$ (j, ?j2)))"
by (rule Groups_Big.sum_product)
also have "… = (∑i = 0..<d. (m1 $$ (?i1, encode1 i) * m2 $$ (encode1 i, ?j1)) * (m3 $$ (?i2, encode2 i) * m4 $$ (encode2 i, ?j2)))"
by (rule sum_encode)
also have "… = row (tensor_mat m1 m3) i ∙ col (tensor_mat m2 m4) j"
apply (simp add: scalar_prod_def tensor_mat_eval i j)
by (rule sum.cong, auto)
finally show "tensor_mat (m1 * m2) (m3 * m4) $$ (i, j) = row (tensor_mat m1 m3) i ∙ col (tensor_mat m2 m4) j" .
qed
lemma tensor_mat_adjoint:
assumes "m1 ∈ carrier_mat d1 d1"
and "m2 ∈ carrier_mat d2 d2"
shows "adjoint (tensor_mat m1 m2) = tensor_mat (adjoint m1) (adjoint m2)"
apply (rule eq_matI, auto)
unfolding tensor_mat_def adjoint_def
using assms by (simp add: conjugate_dist_mul)
lemma tensor_mat_hermitian:
assumes "m1 ∈ carrier_mat d1 d1"
and "m2 ∈ carrier_mat d2 d2"
and "hermitian m1"
and "hermitian m2"
shows "hermitian (tensor_mat m1 m2)"
using assms by (metis hermitian_def tensor_mat_adjoint)
lemma tensor_mat_unitary:
assumes "m1 ∈ carrier_mat d1 d1"
and "m2 ∈ carrier_mat d2 d2"
and "unitary m1"
and "unitary m2"
shows "unitary (tensor_mat m1 m2)"
using assms apply (auto simp add: unitary_def tensor_mat_adjoint)
using assms unfolding inverts_mat_def
apply (subst tensor_mat_mult[symmetric], auto)
by (rule tensor_mat_id)
lemma tensor_mat_positive:
assumes "m1 ∈ carrier_mat d1 d1"
and "m2 ∈ carrier_mat d2 d2"
and "positive m1"
and "positive m2"
shows "positive (tensor_mat m1 m2)"
proof -
obtain M1 where M1: "m1 = M1 * adjoint M1" and dM1:"M1 ∈ carrier_mat d1 d1" using positive_only_if_decomp assms by auto
obtain M2 where M2: "m2 = M2 * adjoint M2" and dM2:"M2 ∈ carrier_mat d2 d2" using positive_only_if_decomp assms by auto
have "(adjoint (tensor_mat M1 M2)) = tensor_mat (adjoint M1) (adjoint M2)" using tensor_mat_adjoint dM1 dM2 by auto
then have "tensor_mat M1 M2 * (adjoint (tensor_mat M1 M2)) = tensor_mat (M1 * adjoint M1) (M2 * adjoint M2)"
using dM1 dM2 adjoint_dim[OF dM1] adjoint_dim[OF dM2] by (auto simp add: tensor_mat_mult)
also have "… = tensor_mat m1 m2" using M1 M2 by auto
finally have "tensor_mat m1 m2 = tensor_mat M1 M2 * (adjoint (tensor_mat M1 M2))"..
then have "∃M. M * adjoint M = tensor_mat m1 m2" by auto
moreover have "tensor_mat m1 m2 ∈ carrier_mat d d" using tensor_mat_carrier by auto
ultimately show ?thesis using positive_if_decomp[of "tensor_mat m1 m2"] by auto
qed
lemma tensor_mat_positive_le:
assumes "m1 ∈ carrier_mat d1 d1"
and "m2 ∈ carrier_mat d2 d2"
and "positive m1"
and "positive m2"
and "m1 ≤⇩L A"
and "m2 ≤⇩L B"
shows "tensor_mat m1 m2 ≤⇩L tensor_mat A B"
proof -
have dA: "A ∈ carrier_mat d1 d1" using assms lowner_le_def by auto
have pA: "positive A" using assms dA lowner_le_trans_positiveI[of m1] by auto
have dB: "B ∈ carrier_mat d2 d2" using assms lowner_le_def by auto
have pB: "positive B" using assms dB lowner_le_trans_positiveI[of m2] by auto
have "A - m1 = A + (- m1)" using assms by (auto simp add: minus_add_uminus_mat)
then have "positive (A + (- m1))" using assms unfolding lowner_le_def by auto
then have p1: "positive (tensor_mat (A + (- m1)) m2)" using assms tensor_mat_positive by auto
moreover have "tensor_mat (- m1) m2 = - tensor_mat m1 m2" using assms apply (subgoal_tac "- m1 = -1 ⋅⇩m m1")
by (auto simp add: tensor_mat_scale1)
moreover have "tensor_mat (A + (- m1)) m2 = tensor_mat A m2 + (tensor_mat (- m1) m2)" using
assms by (auto simp add: tensor_mat_add1 dA)
ultimately have "tensor_mat (A + (- m1)) m2 = tensor_mat A m2 - (tensor_mat m1 m2)" by auto
with p1 have le1: "tensor_mat m1 m2 ≤⇩L tensor_mat A m2" unfolding lowner_le_def by auto
have "B - m2 = B + (- m2)" using assms by (auto simp add: minus_add_uminus_mat)
then have "positive (B + (- m2))" using assms unfolding lowner_le_def by auto
then have p2: "positive (tensor_mat A (B + (- m2)))"
using assms tensor_mat_positive positive_one dA dB pA by auto
moreover have "tensor_mat A (-m2) = - tensor_mat A m2"
using assms apply (subgoal_tac "- m2 = -1 ⋅⇩m m2")
by (auto simp add: tensor_mat_scale2 dA)
moreover have "tensor_mat A (B + (- m2)) = tensor_mat A B + tensor_mat A (- m2)"
using assms by (auto simp add: tensor_mat_add2 dA dB)
ultimately have "tensor_mat A (B + (- m2)) = tensor_mat A B - tensor_mat A m2" by auto
with p2 have le20: "tensor_mat A m2 ≤⇩L tensor_mat A B" unfolding lowner_le_def by auto
show ?thesis apply (subst lowner_le_trans[of _ d "tensor_mat (A) m2"])
subgoal using tensor_mat_carrier by auto
subgoal using tensor_mat_carrier by auto
using le1 le20 by auto
qed
lemma tensor_mat_le_one:
assumes "m1 ∈ carrier_mat d1 d1"
and "m2 ∈ carrier_mat d2 d2"
and "positive m1"
and "positive m2"
and "m1 ≤⇩L 1⇩m d1"
and "m2 ≤⇩L 1⇩m d2"
shows "tensor_mat m1 m2 ≤⇩L 1⇩m d"
proof -
have "1⇩m d1 - m1 = 1⇩m d1 + (- m1)" using assms by (auto simp add: minus_add_uminus_mat)
then have "positive (1⇩m d1 + (- m1))" using assms unfolding lowner_le_def by auto
then have p1: "positive (tensor_mat (1⇩m d1 + (- m1)) m2)" using assms tensor_mat_positive by auto
moreover have "tensor_mat (- m1) m2 = - tensor_mat m1 m2" using assms apply (subgoal_tac "- m1 = -1 ⋅⇩m m1")
by (auto simp add: tensor_mat_scale1)
moreover have "tensor_mat (1⇩m d1 + (- m1)) m2 = tensor_mat (1⇩m d1) m2 + (tensor_mat (- m1) m2)" using
assms by (auto simp add: tensor_mat_add1)
ultimately have "tensor_mat (1⇩m d1 + (- m1)) m2 = tensor_mat (1⇩m d1) m2 - (tensor_mat m1 m2)" by auto
with p1 have le1: "(tensor_mat m1 m2) ≤⇩L tensor_mat (1⇩m d1) m2" unfolding lowner_le_def by auto
have "1⇩m d2 - m2 = 1⇩m d2 + (- m2)" using assms by (auto simp add: minus_add_uminus_mat)
then have "positive (1⇩m d2 + (- m2))" using assms unfolding lowner_le_def by auto
then have p2: "positive (tensor_mat (1⇩m d1) (1⇩m d2 + (- m2)))" using assms tensor_mat_positive positive_one by auto
moreover have "tensor_mat (1⇩m d1) (-m2) = - tensor_mat (1⇩m d1) m2" using assms apply (subgoal_tac "- m2 = -1 ⋅⇩m m2")
by (auto simp add: tensor_mat_scale2)
moreover have "tensor_mat (1⇩m d1) (1⇩m d2 + (- m2)) = tensor_mat (1⇩m d1) (1⇩m d2) + (tensor_mat (1⇩m d1) (- m2))" using
assms by (auto simp add: tensor_mat_add2)
ultimately have "tensor_mat (1⇩m d1) (1⇩m d2 + (- m2)) = tensor_mat (1⇩m d1) (1⇩m d2) - (tensor_mat (1⇩m d1) m2)" by auto
with p2 have le20: "tensor_mat (1⇩m d1) m2 ≤⇩L tensor_mat (1⇩m d1) (1⇩m d2)" unfolding lowner_le_def by auto
then have le2: "tensor_mat (1⇩m d1) m2 ≤⇩L 1⇩m d" apply (subst tensor_mat_id[symmetric]) by auto
have "tensor_mat (1⇩m d1) (1⇩m d2) = 1⇩m d" using tensor_mat_id by auto
show ?thesis apply (subst lowner_le_trans[of _ d "tensor_mat (1⇩m d1) m2"])
subgoal using tensor_mat_carrier by auto
subgoal using tensor_mat_carrier by auto
using le1 le2 by auto
qed
subsection ‹Extension of matrices›
definition mat_extension :: "'a::comm_ring_1 mat ⇒ 'a mat" where
"mat_extension m = tensor_mat m (1⇩m d2)"
lemma mat_extension_carrier:
"mat_extension m ∈ carrier_mat d d"
by (simp add: mat_extension_def tensor_mat_carrier)
lemma mat_extension_add:
assumes "m1 ∈ carrier_mat d1 d1"
and "m2 ∈ carrier_mat d1 d1"
shows "mat_extension (m1 + m2) = mat_extension m1 + mat_extension m2"
using assms by (simp add: mat_extension_def tensor_mat_add1)
lemma mat_extension_trace:
assumes "m ∈ carrier_mat d1 d1"
shows "trace (mat_extension m) = d2 * trace m"
unfolding mat_extension_def
using assms by (simp add: tensor_mat_trace)
lemma mat_extension_id:
"mat_extension (1⇩m d1) = 1⇩m d"
unfolding mat_extension_def by (rule tensor_mat_id)
lemma mat_extension_mult:
assumes "m1 ∈ carrier_mat d1 d1"
and "m2 ∈ carrier_mat d1 d1"
shows "mat_extension (m1 * m2) = mat_extension m1 * mat_extension m2"
using assms by (simp add: mat_extension_def tensor_mat_mult[symmetric])
lemma mat_extension_hermitian:
assumes "m ∈ carrier_mat d1 d1"
and "hermitian m"
shows "hermitian (mat_extension m)"
using assms by (simp add: hermitian_one mat_extension_def tensor_mat_hermitian)
lemma mat_extension_unitary:
assumes "m ∈ carrier_mat d1 d1"
and "unitary m"
shows "unitary (mat_extension m)"
using assms by (simp add: mat_extension_def tensor_mat_unitary unitary_one)
end
abbreviation "tensor_mat ≡ partial_state.tensor_mat"
abbreviation "mat_extension ≡ partial_state.mat_extension"
context state_sig
begin
text ‹Swapping the order of matrices, as well as switching vars, should have no effect›
lemma tensor_mat_comm:
assumes "vars1 ∩ vars2 = {}"
and "{0..<length dims} ⊆ vars1 ∪ vars2"
and "m1 ∈ carrier_mat (prod_list (nths dims vars1)) (prod_list (nths dims vars1))"
and "m2 ∈ carrier_mat (prod_list (nths dims vars2)) (prod_list (nths dims vars2))"
shows "tensor_mat dims vars1 m1 m2 = tensor_mat dims vars2 m2 m1"
proof -
{
fix i
have "nths dims (- vars2) = nths dims vars1" using nths_split_complement_eq[symmetric] assms by auto
then have eq2211: "partial_state.dims2 dims vars2 = partial_state.dims1 dims vars1"
unfolding partial_state.dims2_def partial_state.dims1_def by auto
have "nths dims (- vars1) = nths dims vars2" using nths_split_complement_eq[symmetric, of vars2] assms by auto
then have eq2112: "partial_state.dims2 dims vars1 = partial_state.dims1 dims vars2"
unfolding partial_state.dims2_def partial_state.dims1_def by auto
have "vars1 ∪ vars2 - vars2 = vars1" using assms by auto
then have e1:"partial_state.encode2 dims vars2 i = partial_state.encode1 dims (vars1) i"
using assms(2) partial_state.encode2_alter[of dims "vars1 ∪ vars2" vars2]
unfolding partial_state.encode2_def partial_state.encode1_def apply (subst eq2211[symmetric]) by auto
have "vars1 ∪ vars2 - vars1 = vars2" using assms by auto
then have e2:"partial_state.encode2 dims vars1 i = partial_state.encode1 dims (vars2) i"
using assms(2) partial_state.encode2_alter[of dims "vars1 ∪ vars2" vars1]
unfolding partial_state.encode2_def partial_state.encode1_def apply (subst eq2112[symmetric]) by auto
note e1 e2
}
note e = this
show ?thesis
unfolding partial_state.tensor_mat_def apply (rule cong_mat, simp_all)
unfolding partial_state.dims1_def partial_state.dims2_def
using e by auto
qed
end
subsection ‹Partial tensor product›
text ‹In this context, we assume two disjoint sets of variables, and define
the tensor product of two matrices on these variables›
locale partial_state2 = state_sig +
fixes vars1 :: "nat set"
and vars2 :: "nat set"
assumes disjoint: "vars1 ∩ vars2 = {}"
begin
definition vars0 :: "nat set" where
"vars0 = vars1 ∪ vars2"
definition dims0 :: "nat list" where
"dims0 = nths dims vars0"
definition dims1 :: "nat list" where
"dims1 = nths dims vars1"
definition dims2 :: "nat list" where
"dims2 = nths dims vars2"
definition d0 :: nat where
"d0 = prod_list dims0"
definition d1 :: nat where
"d1 = prod_list dims1"
definition d2 :: nat where
"d2 = prod_list dims2"
lemma dims_product:
"d0 = d1 * d2"
unfolding d0_def d1_def d2_def dims0_def dims1_def dims2_def vars0_def
using disjoint nths_prod_list_split[of vars1 "vars1 ∪ vars2" dims]
apply (subgoal_tac "vars1 ∪ vars2 - vars1 = vars2")
by auto
text ‹Locations of variables in vars1 relative to vars0.
For example: if vars0 = {0,1,2,4,5,6,9} and vars1 = {1,4,6,9}, then
vars1' should be {1,3,5,6}.›
definition vars1' :: "nat set" where
"vars1' = (ind_in_set vars0) ` vars1"
definition vars2' :: "nat set" where
"vars2' = (ind_in_set vars0) ` vars2"
lemma vars1'I:
"x ∈ vars1 ⟹ card {y∈vars0. y < x} ∈ vars1'"
unfolding vars1'_def ind_in_set_def by auto
lemma vars1'D:
"i ∈ vars1' ⟹ ∃x∈vars1. card {y∈vars0. y < x} = i"
unfolding vars1'_def ind_in_set_def by auto
text ‹Main property of vars1'›
lemma ind_in_set_bij:
"bij_betw (ind_in_set vars0) ({0..<length dims} ∩ vars0) {0..<card ({0..<length dims} ∩ vars0)}"
using bij_ind_in_set_bound unfolding ind_in_set_def by auto
lemma length_dims0:
"length dims0 = card ({0..<length dims} ∩ vars0)"
unfolding dims0_def using length_nths[of dims vars0]
apply (subgoal_tac "{i. i < length dims ∧ i ∈ vars0}= {0..<length dims} ∩ vars0")
by auto
lemma length_dims0_minus_vars2'_is_vars1':
"{0..<length dims0} - vars2' = {0..<length dims0} ∩ vars1'"
proof -
have sub20: "vars2 ⊆ vars0" unfolding vars0_def by auto
have sub1: "vars1 = vars0 - vars2" unfolding vars0_def using disjoint by auto
have eq: "{0..<length dims0} = ind_in_set vars0 ` ({0..<length dims} ∩ vars0)"
using ind_in_set_bij length_dims0 bij_betw_imp_surj_on[of "ind_in_set vars0"] by auto
show ?thesis unfolding vars2'_def vars1'_def eq using ind_in_set_minus_subset_bound[OF sub20] sub1 by auto
qed
lemma length_dims0_minus_vars1'_is_vars2':
"{0..<length dims0} - vars1' = {0..<length dims0} ∩ vars2'"
proof -
have sub10: "vars1 ⊆ vars0" unfolding vars0_def by auto
have sub2: "vars2 = vars0 - vars1" unfolding vars0_def using disjoint by auto
have eq: "{0..<length dims0} = ind_in_set vars0 ` ({0..<length dims} ∩ vars0)"
using ind_in_set_bij length_dims0 bij_betw_imp_surj_on[of "ind_in_set vars0"] by auto
show ?thesis unfolding vars2'_def vars1'_def eq using ind_in_set_minus_subset_bound[OF sub10] sub2 by auto
qed
lemma nths_vars1':
"nths dims0 vars1' = dims1"
using nths_reencode_eq[of vars1 vars0 dims]
using nths_reencode_eq_comp[of vars1 vars0 dims]
unfolding vars0_def ind_in_set_def vars1'_def dims1_def dims0_def by auto
lemma nths_vars1'_comp:
"nths dims0 (-vars2') = dims1"
using nths_reencode_eq_comp[of vars2 vars0 dims] disjoint
unfolding vars0_def ind_in_set_def vars2'_def dims1_def dims0_def
apply (subgoal_tac "(vars1 ∪ vars2 - vars2) = vars1") by auto
lemma nths_vars2':
"nths dims0 (-vars1') = dims2"
using nths_reencode_eq_comp[of vars1 vars0 dims] disjoint
unfolding vars0_def ind_in_set_def vars1'_def dims2_def dims0_def
apply (subgoal_tac "(vars1 ∪ vars2 - vars1) = vars2") by auto
lemma nths_vars2'_comp:
"nths dims0 (vars2') = dims2"
using nths_reencode_eq[of vars2 vars0 dims]
unfolding vars0_def ind_in_set_def vars2'_def dims2_def dims0_def
by auto
lemma ptensor_encode1_encode2:
"partial_state.encode1 dims0 vars1' = partial_state.encode2 dims0 vars2'"
proof -
have "partial_state.encode1 dims0 vars1' i
= digit_decode (partial_state.dims1 dims0 vars1') (nths (digit_encode dims0 i) ({0..<length dims0} ∩ vars1'))" for i
using partial_state.encode1_alter by auto
moreover have "partial_state.encode2 dims0 vars2' i
= digit_decode (partial_state.dims2 dims0 vars2') (nths (digit_encode dims0 i) ({0..<length dims0} - vars2'))" for i
using partial_state.encode2_alter by auto
moreover have "partial_state.dims1 dims0 vars1' = partial_state.dims2 dims0 vars2'"
unfolding partial_state.dims1_def partial_state.dims2_def using nths_vars1' nths_vars1'_comp by auto
ultimately show ?thesis using length_dims0_minus_vars2'_is_vars1' by auto
qed
lemma ptensor_encode2_encode1:
"partial_state.encode1 dims0 vars2' = partial_state.encode2 dims0 vars1'"
proof -
have "partial_state.encode1 dims0 vars2' i
= digit_decode (partial_state.dims1 dims0 vars2') (nths (digit_encode dims0 i) ({0..<length dims0} ∩ vars2'))" for i
using partial_state.encode1_alter by auto
moreover have "partial_state.encode2 dims0 vars1' i
= digit_decode (partial_state.dims2 dims0 vars1') (nths (digit_encode dims0 i) ({0..<length dims0} - vars1'))" for i
using partial_state.encode2_alter by auto
moreover have "partial_state.dims1 dims0 vars2' = partial_state.dims2 dims0 vars1'"
unfolding partial_state.dims1_def partial_state.dims2_def using nths_vars2' nths_vars2'_comp by auto
ultimately show ?thesis using length_dims0_minus_vars1'_is_vars2' by auto
qed
text ‹Given vector v1 of dimension d1, and vector v2 of dimension d2, form
the tensor vector of dimension d1 * d2 = d0›
definition ptensor_vec :: "'a::times vec ⇒ 'a vec ⇒ 'a vec" where
"ptensor_vec v1 v2 = partial_state.tensor_vec dims0 vars1' v1 v2"
lemma ptensor_vec_dim [simp]:
"dim_vec (ptensor_vec v1 v2) = d0"
by (simp add: ptensor_vec_def partial_state.tensor_vec_dim state_sig.d_def d0_def)
lemma ptensor_vec_carrier:
"ptensor_vec v1 v2 ∈ carrier_vec d0"
by (simp add: carrier_dim_vec)
lemma ptensor_vec_add:
fixes v1 v2 v3 :: "'a::comm_ring vec"
assumes "v1 ∈ carrier_vec d1"
and "v2 ∈ carrier_vec d1"
and "v3 ∈ carrier_vec d2"
shows "ptensor_vec (v1 + v2) v3 = ptensor_vec v1 v3 + ptensor_vec v2 v3"
unfolding ptensor_vec_def
apply (rule partial_state.tensor_vec_add1)
unfolding partial_state.d1_def partial_state.d2_def
partial_state.dims1_def partial_state.dims2_def nths_vars1' nths_vars2'
using assms unfolding d1_def d2_def by auto
definition ptensor_mat :: "'a::comm_ring_1 mat ⇒ 'a mat ⇒ 'a mat" where
"ptensor_mat m1 m2 = partial_state.tensor_mat dims0 vars1' m1 m2"
lemma ptensor_mat_dim_row [simp]:
"dim_row (ptensor_mat m1 m2) = d0"
by (simp add: ptensor_mat_def partial_state.tensor_mat_dim_row d0_def state_sig.d_def)
lemma ptensor_mat_dim_col [simp]:
"dim_col (ptensor_mat m1 m2) = d0"
by (simp add: ptensor_mat_def partial_state.tensor_mat_dim_col d0_def state_sig.d_def)
lemma ptensor_mat_carrier:
"ptensor_mat m1 m2 ∈ carrier_mat d0 d0"
by (simp add: carrier_matI)
lemma ptensor_mat_add:
assumes "m1 ∈ carrier_mat d1 d1"
and "m2 ∈ carrier_mat d1 d1"
and "m3 ∈ carrier_mat d2 d2"
shows "ptensor_mat (m1 + m2) m3 = ptensor_mat m1 m3 + ptensor_mat m2 m3"
unfolding ptensor_mat_def
apply (rule partial_state.tensor_mat_add1)
unfolding partial_state.d1_def partial_state.d2_def
partial_state.dims1_def partial_state.dims2_def nths_vars1'
nths_vars2'
using assms unfolding d1_def d2_def by auto
lemma ptensor_mat_trace:
assumes "m1 ∈ carrier_mat d1 d1"
and "m2 ∈ carrier_mat d2 d2"
shows "trace (ptensor_mat m1 m2) = trace m1 * trace m2"
unfolding ptensor_mat_def
apply (rule partial_state.tensor_mat_trace)
unfolding partial_state.d1_def partial_state.d2_def
partial_state.dims1_def partial_state.dims2_def nths_vars1' nths_vars2'
using assms unfolding d1_def d2_def by auto
lemma ptensor_mat_id:
"ptensor_mat (1⇩m d1) (1⇩m d2) = 1⇩m d0"
unfolding ptensor_mat_def
by (metis d0_def d1_def d2_def nths_vars1' nths_vars2'
partial_state.d1_def partial_state.d2_def partial_state.dims1_def
partial_state.dims2_def partial_state.tensor_mat_id state_sig.d_def)
lemma ptensor_mat_mult:
assumes "m1 ∈ carrier_mat d1 d1"
and "m2 ∈ carrier_mat d1 d1"
and "m3 ∈ carrier_mat d2 d2"
and "m4 ∈ carrier_mat d2 d2"
shows "ptensor_mat (m1 * m2) (m3 * m4) = ptensor_mat m1 m3 * ptensor_mat m2 m4"
proof -
interpret st: partial_state dims0 vars1'.
have "st.d1 = d1" unfolding st.d1_def st.dims1_def d1_def nths_vars1' by auto
moreover have "st.d2 = d2" unfolding st.d2_def