Commit f4093dce authored by Rene Thiemann's avatar Rene Thiemann
Browse files

new entry Isabelle marries Dirac

parent cace3e947231
section \<open>Basic Results\<close>
theory Basics
imports
HOL.Set_Interval
HOL.Semiring_Normalization
HOL.Real_Vector_Spaces
HOL.Power
HOL.Complex
Jordan_Normal_Form.Jordan_Normal_Form
begin
subsection \<open>Basic Set-Theoretic Results\<close>
lemma set_2_atLeast0 [simp]: "{0..<2::nat} = {0,1}" by auto
lemma set_2: "{..<2::nat} = {0,1}" by auto
lemma set_4_atLeast0 [simp]:"{0..<4::nat} = {0,1,2,3}" by auto
lemma set_4: "{..<4::nat} = {0,1,2,3}" by auto
lemma set_4_disj [simp]:
fixes i:: nat
assumes "i < 4"
shows "i = 0 \<or> i = 1 \<or> i = 2 \<or> i = 3"
using assms by auto
lemma set_8_atLeast0 [simp]: "{0..<8::nat} = {0,1,2,3,4,5,6,7}" by auto
lemma index_is_2 [simp]: "\<forall>i::nat. i \<noteq> Suc 0 \<longrightarrow> i \<noteq> 3 \<longrightarrow> 0 < i \<longrightarrow> i < 4 \<longrightarrow> i = 2" by simp
lemma index_sl_four [simp]: "\<forall>i::nat. i < 4 \<longrightarrow> i = 0 \<or> i = 1 \<or> i = 2 \<or> i = 3" by auto
subsection \<open>Basic Arithmetic Results\<close>
lemma index_div_eq [simp]:
fixes i::nat
shows "i\<in>{a*b..<(a+1)*b} \<Longrightarrow> i div b = a"
proof-
fix i::nat
assume a:"i\<in>{a*b..<(a+1)*b}"
then have "i div b \<ge> a"
by (metis Suc_eq_plus1 atLeastLessThan_iff le_refl semiring_normalization_rules(7) split_div')
moreover have "i div b < a+1"
using a by (simp add: less_mult_imp_div_less)
ultimately show "i div b = a" by simp
qed
lemma index_mod_eq [simp]:
fixes i::nat
shows "i\<in>{a*b..<(a+1)*b} \<Longrightarrow> i mod b = i-a*b"
by (simp add: modulo_nat_def)
lemma sqr_of_cmod_of_prod:
shows "(cmod (z1 * z2))\<^sup>2 = (cmod z1)\<^sup>2 * (cmod z2)\<^sup>2"
by (simp add: norm_mult power_mult_distrib)
lemma less_power_add_imp_div_less [simp]:
fixes i m n:: nat
assumes "i < 2^(m+n)"
shows "i div 2^n < 2^m"
using assms by (simp add: less_mult_imp_div_less power_add)
lemma div_mult_mod_eq_minus:
fixes i j:: nat
shows "(i div 2^n) * 2^n + i mod 2^n - (j div 2^n) * 2^n - j mod 2^n = i - j"
by (simp add: div_mult_mod_eq algebra_simps)
lemma neq_imp_neq_div_or_mod:
fixes i j:: nat
assumes "i \<noteq> j"
shows "i div 2^n \<noteq> j div 2^n \<or> i mod 2^n \<noteq> j mod 2^n"
using assms div_mult_mod_eq_minus
by (metis add.right_neutral cancel_div_mod_rules(2))
lemma index_one_mat_div_mod:
assumes "i < 2^(m+n)" and "j < 2^(m+n)"
shows "((1\<^sub>m(2^m) $$ (i div 2^n, j div 2^n))::complex) * 1\<^sub>m(2^n) $$ (i mod 2^n, j mod 2^n) = 1\<^sub>m(2^(m+n)) $$ (i, j)"
proof (cases "i = j")
case True
then show ?thesis by(simp add: assms)
next
case c1:False
have "i div 2^n \<noteq> j div 2^n \<or> i mod 2^n \<noteq> j mod 2^n"
using c1 neq_imp_neq_div_or_mod by simp
then have "1\<^sub>m (2^m) $$ (i div 2^n, j div 2^n) = 0 \<or> 1\<^sub>m (2^n) $$ (i mod 2^n, j mod 2^n) = 0"
using assms by simp
then show ?thesis
using assms by (simp add: c1)
qed
lemma sqr_of_sqrt_2 [simp]:
fixes z:: "complex"
shows "z * 2 / (complex_of_real (sqrt 2) * complex_of_real (sqrt 2)) = z"
by(metis nonzero_mult_div_cancel_right norm_numeral of_real_numeral of_real_power power2_eq_square
real_norm_def real_sqrt_abs real_sqrt_power zero_neq_numeral)
lemma two_div_sqrt_two [simp]:
shows "2 * complex_of_real (sqrt (1/2)) = complex_of_real (sqrt 2)"
apply(auto simp add: real_sqrt_divide algebra_simps)
by (metis divide_eq_0_iff nonzero_mult_div_cancel_left sqr_of_sqrt_2)
lemma two_div_sqr_of_cmd_sqrt_two [simp]:
shows "2 * (cmod (1 / complex_of_real (sqrt 2)))\<^sup>2 = 1"
using cmod_def by (simp add: power_divide)
lemma two_div_two [simp]:
shows "2 div Suc (Suc 0) = 1" by simp
lemma two_mod_two [simp]:
shows "2 mod Suc (Suc 0) = 0" by (simp add: numeral_2_eq_2)
lemma three_div_two [simp]:
shows "3 div Suc (Suc 0) = 1" by (simp add: numeral_3_eq_3)
lemma three_mod_two [simp]:
shows "3 mod Suc (Suc 0) = 1" by (simp add: mod_Suc numeral_3_eq_3)
subsection \<open>Basic Results on Matrices\<close>
lemma index_matrix_prod [simp]:
assumes "i < dim_row A" and "j < dim_col B" and "dim_col A = dim_row B"
shows "(A * B) $$ (i,j) = (\<Sum>k<dim_row B. (A $$ (i,k)) * (B $$ (k,j)))"
using assms
apply(simp add: scalar_prod_def atLeast0LessThan).
subsection \<open>Basic Results on Sums\<close>
lemma sum_insert [simp]:
assumes "x \<notin> F" and "finite F"
shows "(\<Sum>y\<in>insert x F. P y) = (\<Sum>y\<in>F. P y) + P x"
using assms insert_def by(simp add: add.commute)
lemma sum_of_index_diff [simp]:
fixes f:: "nat \<Rightarrow> 'a::comm_monoid_add"
shows "(\<Sum>i\<in>{a..<a+b}. f(i-a)) = (\<Sum>i\<in>{..<b}. f(i))"
proof (induction b)
case 0
then show ?case by simp
next
case (Suc b)
then show ?case by simp
qed
subsection \<open>Basic Results Involving the Exponential Function.\<close>
lemma exp_of_real_cnj:
fixes x ::real
shows "cnj (exp (\<i> * x)) = exp (-(\<i> * x))"
proof
show "Re (cnj (exp (\<i> * x))) = Re (exp (-(\<i> * x)))"
using Re_exp by simp
show "Im (cnj (exp (\<i> * x))) = Im (exp (-(\<i> * x)))"
using Im_exp by simp
qed
lemma exp_of_real_cnj2:
fixes x ::real
shows "cnj (exp (-(\<i> * x))) = exp (\<i> * x)"
proof
show "Re (cnj (exp (-(\<i> * x)))) = Re (exp (\<i> * x))"
using Re_exp by simp
show "Im (cnj (exp (-(\<i> * x)))) = Im (exp (\<i> * x))"
using Im_exp by simp
qed
lemma exp_of_half_pi:
fixes x:: real
assumes "x = pi/2"
shows "exp (\<i> * complex_of_real x) = \<i>"
using assms cis_conv_exp cis_pi_half by fastforce
lemma exp_of_minus_half_pi:
fixes x:: real
assumes "x = pi/2"
shows "exp (-(\<i> * complex_of_real x)) = -\<i>"
using assms cis_conv_exp cis_minus_pi_half by fastforce
lemma exp_of_real:
fixes x:: real
shows "exp (\<i> * x) = cos x + \<i> * (sin x)"
proof
show "Re (exp (\<i> * x)) = Re ((cos x) + \<i> * (sin x))"
using Re_exp by simp
show "Im (exp (\<i> * x)) = Im ((cos x) + \<i> * (sin x))"
using Im_exp by simp
qed
lemma exp_of_real_inv:
fixes x:: real
shows "exp (-(\<i> * x)) = cos x - \<i> * (sin x)"
proof
show "Re (exp (-(\<i> * x))) = Re ((cos x) - \<i> * (sin x))"
using Re_exp by simp
show "Im (exp (-(\<i> * x))) = Im ((cos x) - \<i> * (sin x))"
using Im_exp by simp
qed
subsection \<open>Basic Results with Trigonometric Functions.\<close>
subsubsection \<open>Basic Inequalities\<close>
lemma sin_squared_le_one:
fixes x:: real
shows "(sin x)\<^sup>2 \<le> 1"
using abs_sin_le_one abs_square_le_1 by blast
lemma cos_squared_le_one:
fixes x:: real
shows "(cos x)\<^sup>2 \<le> 1"
using abs_cos_le_one abs_square_le_1 by blast
subsubsection \<open>Basic Equalities\<close>
lemma sin_of_quarter_pi:
fixes x:: real
assumes "x = pi/2"
shows "sin (x/2) = (sqrt 2)/2"
by (auto simp add: assms sin_45)
lemma cos_of_quarter_pi:
fixes x:: real
assumes "x = pi/2"
shows "cos (x/2) = (sqrt 2)/2"
by (auto simp add: assms cos_45)
end
\ No newline at end of file
(*
Authors:
Anthony Bordg, University of Cambridge, apdb3@cam.ac.uk
Hanna Lachnitt, TU Wien, lachnitt@student.tuwien.ac.at
*)
section \<open>Binary Representation of Natural Numbers\<close>
theory Binary_Nat
imports
HOL.Nat
HOL.List
Basics
begin
primrec bin_rep_aux:: "nat \<Rightarrow> nat \<Rightarrow> nat list" where
"bin_rep_aux 0 m = [m]"
| "bin_rep_aux (Suc n) m = m div 2^n # bin_rep_aux n (m mod 2^n)"
lemma length_of_bin_rep_aux:
fixes n m:: nat
assumes "m < 2^n"
shows "length (bin_rep_aux n m) = n+1"
using assms
proof(induction n arbitrary: m)
case 0
then show "length (bin_rep_aux 0 m) = 0 + 1" by simp
next
case (Suc n)
assume a0:"\<And>m. m < 2^n \<Longrightarrow> length (bin_rep_aux n m) = n + 1" and "m < 2^(Suc n)"
then show "length (bin_rep_aux (Suc n) m) = Suc n + 1"
using a0 by simp
qed
lemma bin_rep_aux_neq_nil:
fixes n m:: nat
shows "bin_rep_aux n m \<noteq> []"
using bin_rep_aux.simps by (metis list.distinct(1) old.nat.exhaust)
lemma last_of_bin_rep_aux:
fixes n m:: nat
assumes "m < 2^n" and "m \<ge> 0"
shows "last (bin_rep_aux n m) = 0"
using assms
proof(induction n arbitrary: m)
case 0
assume "m < 2^0" and "m \<ge> 0"
then show "last (bin_rep_aux 0 m) = 0" by simp
next
case (Suc n)
assume a0:"\<And>m. m < 2^n \<Longrightarrow> m \<ge> 0 \<Longrightarrow> last (bin_rep_aux n m) = 0" and "m < 2^(Suc n)"
and "m \<ge> 0"
then show "last (bin_rep_aux (Suc n) m) = 0"
using bin_rep_aux_neq_nil by simp
qed
lemma mod_mod_power_cancel:
fixes m n p:: nat
assumes "m \<le> n"
shows "p mod 2^n mod 2^m = p mod 2^m"
using assms by (simp add: dvd_power_le mod_mod_cancel)
lemma bin_rep_aux_index:
fixes n m i:: nat
assumes "n \<ge> 1" and "m < 2^n" and "m \<ge> 0" and "i \<le> n"
shows "bin_rep_aux n m ! i = (m mod 2^(n-i)) div 2^(n-1-i)"
using assms
proof(induction n arbitrary: m i rule: nat_induct_at_least)
case base
assume "m < 2^1" and "i \<le> 1"
then show "bin_rep_aux 1 m ! i = m mod 2^(1-i) div 2^(1-1-i)"
using bin_rep_aux.simps
by (metis One_nat_def base.prems(2) diff_is_0_eq' diff_zero div_by_1 le_Suc_eq le_numeral_extra(3)
nth_Cons' power_0 unique_euclidean_semiring_numeral_class.mod_less)
next
case (Suc n)
assume a0:"\<And>m i. m < 2^n \<Longrightarrow> m \<ge> 0 \<Longrightarrow> i \<le> n \<Longrightarrow> bin_rep_aux n m ! i = m mod 2 ^ (n-i) div 2^(n-1-i)"
and a1:"m < 2^(Suc n)" and a2:"i \<le> Suc n" and a3:"m \<ge> 0"
then show "bin_rep_aux (Suc n) m ! i = m mod 2^(Suc n - i) div 2^(Suc n - 1 - i)"
proof-
have "bin_rep_aux (Suc n) m = m div 2^n # bin_rep_aux n (m mod 2^n)" by simp
then have f0:"bin_rep_aux (Suc n) m ! i = (m div 2^n # bin_rep_aux n (m mod 2^n)) ! i" by simp
then have "bin_rep_aux (Suc n) m ! i = m div 2^n" if "i = 0" using that by simp
then have f1:"bin_rep_aux (Suc n) m ! i = m mod 2^(Suc n - i) div 2^(Suc n - 1 - i)" if "i = 0"
proof-
have "m mod 2^(Suc n - i) = m"
using that a1 by (simp add: Suc.prems(2))
then have "m mod 2^(Suc n - i) div 2^(Suc n - 1 - i) = m div 2^n"
using that by simp
thus ?thesis by (simp add: that)
qed
then have "bin_rep_aux (Suc n) m ! i = bin_rep_aux n (m mod 2^n) ! (i-1)" if "i \<ge> 1"
using that f0 by simp
then have f2:"bin_rep_aux (Suc n) m ! i = ((m mod 2^n) mod 2^(n - (i - 1))) div 2^(n - 1 - (i - 1))" if "i \<ge> 1"
using that a0 a1 a2 a3 Suc.prems(2) by simp
then have f3:"bin_rep_aux (Suc n) m ! i = ((m mod 2^n) mod 2^(Suc n - i)) div 2^(Suc n - 1 - i)" if "i \<ge> 1"
using that by simp
then have "bin_rep_aux (Suc n) m ! i = m mod 2^(Suc n - i) div 2^(Suc n - 1 - i)" if "i \<ge> 1"
proof-
have "Suc n - i \<le> n" using that by simp
then have "m mod 2^n mod 2^(Suc n - i) = m mod 2^(Suc n - i)"
using mod_mod_power_cancel[of "Suc n - i" "n" "m"] by simp
thus ?thesis
using that f3 by simp
qed
thus ?thesis using f1 f2
using linorder_not_less by blast
qed
qed
lemma bin_rep_aux_coeff:
fixes n m i:: nat
assumes "m < 2^n" and "i \<le> n" and "m \<ge> 0"
shows "bin_rep_aux n m ! i = 0 \<or> bin_rep_aux n m ! i = 1"
using assms
proof(induction n arbitrary: m i)
case 0
assume "m < 2^0" and "i \<le> 0" and "m \<ge> 0"
then show "bin_rep_aux 0 m ! i = 0 \<or> bin_rep_aux 0 m ! i = 1" by simp
next
case (Suc n)
assume a0:"\<And>m i. m < 2 ^ n \<Longrightarrow> i \<le> n \<Longrightarrow> m \<ge> 0 \<Longrightarrow> bin_rep_aux n m ! i = 0 \<or> bin_rep_aux n m ! i = 1"
and a1:"m < 2^Suc n" and a2:"i \<le> Suc n" and a3:"m \<ge> 0"
then show "bin_rep_aux (Suc n) m ! i = 0 \<or> bin_rep_aux (Suc n) m ! i = 1"
proof-
have "bin_rep_aux (Suc n) m ! i = (m div 2^n # bin_rep_aux n (m mod 2^n)) ! i" by simp
moreover have "\<dots> = bin_rep_aux n (m mod 2^n) ! (i - 1)" if "i \<ge> 1"
using that by simp
moreover have "m mod 2^n < 2^n" by simp
ultimately have "bin_rep_aux (Suc n) m ! i = 0 \<or> bin_rep_aux (Suc n) m ! i = 1" if "i\<ge>1"
using that a0[of "m mod 2^n" "i-1"] a2 by simp
moreover have "m div 2^n = 0 \<or> m div 2^n = 1"
using a1 a3 less_mult_imp_div_less by(simp add: less_2_cases)
ultimately show ?thesis by (simp add: nth_Cons')
qed
qed
definition bin_rep:: "nat \<Rightarrow> nat \<Rightarrow> nat list" where
"bin_rep n m = butlast (bin_rep_aux n m)"
lemma length_of_bin_rep:
fixes n m:: nat
assumes "m < 2^n"
shows "length (bin_rep n m) = n"
using assms length_of_bin_rep_aux bin_rep_def by simp
lemma bin_rep_coeff:
fixes n m i:: nat
assumes "m < 2^n" and "i < n" and "m \<ge> 0"
shows "bin_rep n m ! i = 0 \<or> bin_rep n m ! i = 1"
using assms bin_rep_def bin_rep_aux_coeff length_of_bin_rep by(simp add: nth_butlast)
lemma bin_rep_index:
fixes n m i:: nat
assumes "n \<ge> 1" and "m < 2^n" and "i < n" and "m \<ge> 0"
shows "bin_rep n m ! i = (m mod 2^(n-i)) div 2^(n-1-i)"
proof-
have "bin_rep n m ! i = bin_rep_aux n m ! i"
using bin_rep_def length_of_bin_rep nth_butlast assms(3)
by (simp add: nth_butlast assms(2))
thus ?thesis
using assms bin_rep_aux_index by simp
qed
lemma bin_rep_eq:
fixes n m:: nat
assumes "n \<ge> 1" and "m \<ge> 0" and "m < 2^n" and "m \<ge> 0"
shows "m = (\<Sum>i<n. bin_rep n m ! i * 2^(n-1-i))"
proof-
{
fix i:: nat
assume "i < n"
then have "bin_rep n m ! i * 2^(n-1-i) = (m mod 2^(n-i)) div 2^(n-1-i) * 2^(n-1-i)"
using assms bin_rep_index by simp
moreover have "\<dots> = m mod 2^(n-i) - m mod 2^(n-i) mod 2^(n-1-i)"
by (simp add: minus_mod_eq_div_mult)
moreover have "\<dots> = int(m mod 2^(n-i)) - m mod 2^(n-i) mod 2^(n-1-i)"
using mod_less_eq_dividend of_nat_diff by blast
moreover have "\<dots> = int(m mod 2^(n-i)) - m mod 2^(n-1-i)"
using mod_mod_power_cancel[of "n-1-i" "n-i"] by (simp add: dvd_power_le mod_mod_cancel)
ultimately have "bin_rep n m ! i * 2^(n-1-i) = int (m mod 2^(n-i)) - m mod 2^(n-1-i)"
by presburger
}
then have f0:"(\<Sum>i<n. bin_rep n m ! i * 2^(n-1-i)) = (\<Sum>i<n. int (m mod 2^(n-i)) - m mod 2^(n-1-i))"
by auto
thus ?thesis
proof-
have "(\<Sum>i<n. int ((m::nat) mod 2^(n - i)) - (m mod 2^(n - 1 - i))) =
(\<Sum>i<n. ( m mod 2^(n - i))) - (\<Sum>i<n. int (m mod 2^(n - 1 - i)))"
using sum_subtractf[of "(\<lambda>i. (m mod 2^(n-i)))::nat\<Rightarrow>nat" "(\<lambda>i. (m mod 2^(n-1-i)))::nat\<Rightarrow>nat" "{..<(n::nat)}"]
by auto
moreover have "\<dots> = m mod 2^n + (\<Sum>i\<in>{1..<n}. (m mod 2^(n-i))) - (\<Sum>i<n-1. int (m mod 2^(n-1-i)))- m mod 2^0"
using sum.atLeast_Suc_atMost sum.lessThan_Suc assms(1)
by (smt One_nat_def Suc_le_eq diff_self_eq_0 le_add_diff_inverse lessThan_atLeast0 minus_nat.diff_0
plus_1_eq_Suc sum.atLeast_Suc_lessThan)
moreover have "\<dots> = m mod 2^n + (\<Sum>i<n-1. m mod 2^(n-i-1)) - (\<Sum>i<n-1. int ( m mod 2^(n-1-i))) - m mod 2^0"
apply (auto simp add: sum_of_index_diff[of "\<lambda>i. m mod 2 ^ (n - 1 - i)" "1" "n-1"])
by (smt One_nat_def assms(1) le_add_diff_inverse lessThan_atLeast0 plus_1_eq_Suc sum.cong sum.shift_bounds_Suc_ivl)
moreover have "\<dots> = m mod 2^n - m mod 2^0" by simp
moreover have "\<dots> = m" using assms by auto
ultimately show "m = (\<Sum>i<n. bin_rep n m ! i * 2^(n-1-i))"
using assms f0 by linarith
qed
qed
lemma bin_rep_index_0:
fixes n m:: nat
assumes "m < 2^n" and "k > n"
shows "(bin_rep k m) ! 0 = 0"
proof-
have "m < 2^(k-1)"
using assms by(smt Suc_diff_1 Suc_leI gr0I le_trans less_or_eq_imp_le linorder_neqE_nat not_less
one_less_numeral_iff power_strict_increasing semiring_norm(76))
then have f:"m div 2^(k-1) = 0"
by auto
have "k \<ge> 1"
using assms(2) by simp
moreover have "bin_rep_aux k m = (m div 2^(k-1)) # (bin_rep_aux (k-1) (m mod 2^(k-1)))"
using bin_rep_aux.simps(2) by(metis Suc_diff_1 assms(2) diff_0_eq_0 neq0_conv zero_less_diff)
moreover have "bin_rep k m = butlast ((m div 2^(k-1)) # (bin_rep_aux (k-1) (m mod 2^(k-1))))"
using bin_rep_def by (simp add: calculation(2))
moreover have "\<dots> = butlast (0 # (bin_rep_aux (k-1) (m mod 2^(k-1))))"
using f by simp
moreover have "\<dots> = 0 # butlast (bin_rep_aux (k-1) (m mod 2^(k-1)))"
by(simp add: bin_rep_aux_neq_nil)
ultimately show ?thesis
by simp
qed
lemma bin_rep_index_0_geq:
fixes n m:: nat
assumes "m \<ge> 2^n" and "m < 2^(n+1)"
shows "bin_rep (n+1) m ! 0 = 1"
proof-
have "bin_rep (Suc n) m = butlast (bin_rep_aux (Suc n) m)"
using bin_rep_def by simp
moreover have "\<dots> = butlast (1 # (bin_rep_aux n (m mod 2^n)))"
using assms bin_rep_aux_def by simp
moreover have "\<dots> = 1 # butlast (bin_rep_aux n (m mod 2^n))"
by (simp add: bin_rep_aux_neq_nil)
ultimately show ?thesis
by (simp add: bin_rep_aux_neq_nil)
qed
end
\ No newline at end of file
(* Author: Anthony Bordg, University of Cambridge, apdb3@cam.ac.uk *)
section \<open>Complex Vectors\<close>
theory Complex_Vectors
imports
Quantum
VectorSpace.VectorSpace
begin
subsection \<open>The Vector Space of Complex Vectors of Dimension n\<close>
definition module_cpx_vec:: "nat \<Rightarrow> (complex, complex vec) module" where
"module_cpx_vec n \<equiv> module_vec TYPE(complex) n"
definition cpx_rng:: "complex ring" where
"cpx_rng \<equiv> \<lparr>carrier = UNIV, mult = (*), one = 1, zero = 0, add = (+)\<rparr>"
lemma cpx_cring_is_field [simp]:
"field cpx_rng"
apply unfold_locales
apply (auto intro: right_inverse simp: cpx_rng_def Units_def field_simps)
by (metis add.right_neutral add_diff_cancel_left' add_uminus_conv_diff)
lemma cpx_abelian_monoid [simp]:
"abelian_monoid cpx_rng"
using cpx_cring_is_field
by (simp add: field_def abelian_group_def cring_def domain_def ring_def)
lemma vecspace_cpx_vec [simp]:
"vectorspace cpx_rng (module_cpx_vec n)"
apply unfold_locales
apply (auto simp: cpx_rng_def module_cpx_vec_def module_vec_def Units_def field_simps)
apply (auto intro: right_inverse add_inv_exists_vec)
by (metis add.right_neutral add_diff_cancel_left' add_uminus_conv_diff)
lemma module_cpx_vec [simp]:
"Module.module cpx_rng (module_cpx_vec n)"
using vecspace_cpx_vec by (simp add: vectorspace_def)
definition state_basis:: "nat \<Rightarrow> nat \<Rightarrow> complex vec" where
"state_basis n i \<equiv> unit_vec (2^n) i"
definition unit_vectors:: "nat \<Rightarrow> (complex vec) set" where
"unit_vectors n \<equiv> {unit_vec n i | i::nat. 0 \<le> i \<and> i < n}"
lemma unit_vectors_carrier_vec [simp]:
"unit_vectors n \<subseteq> carrier_vec n"
using unit_vectors_def by auto
lemma (in Module.module) finsum_over_singleton [simp]:
assumes "f x \<in> carrier M"
shows "finsum M f {x} = f x"
using assms by simp
lemma lincomb_over_singleton [simp]:
assumes "x \<in> carrier_vec n" and "f \<in> {x} \<rightarrow> UNIV"
shows "module.lincomb (module_cpx_vec n) f {x} = f x \<cdot>\<^sub>v x"
using assms module.lincomb_def module_cpx_vec module_cpx_vec_def module.finsum_over_singleton
by (smt module_vec_simps(3) module_vec_simps(4) smult_carrier_vec)
lemma dim_vec_lincomb [simp]:
assumes "finite F" and "f: F \<rightarrow> UNIV" and "F \<subseteq> carrier_vec n"
shows "dim_vec (module.lincomb (module_cpx_vec n) f F) = n"
using assms
proof(induct F)
case empty
show "dim_vec (module.lincomb (module_cpx_vec n) f {}) = n"
proof -
have "module.lincomb (module_cpx_vec n) f {} = 0\<^sub>v n"
using module.lincomb_def abelian_monoid.finsum_empty module_cpx_vec_def vecspace_cpx_vec vectorspace_def
by (smt abelian_group_def Module.module_def module_vec_simps(2))
thus ?thesis by simp
qed
next
case (insert x F)
hence "module.lincomb (module_cpx_vec n) f (insert x F) =
(f x \<cdot>\<^sub>v x) \<oplus>\<^bsub>module_cpx_vec n\<^esub> module.lincomb (module_cpx_vec n) f F"
using module_cpx_vec_def module_vec_def module_cpx_vec module.lincomb_insert cpx_rng_def insert_subset
by (smt Pi_I' UNIV_I Un_insert_right module_vec_simps(4) partial_object.select_convs(1) sup_bot.comm_neutral)
hence "dim_vec (module.lincomb (module_cpx_vec n) f (insert x F)) =
dim_vec (module.lincomb (module_cpx_vec n) f F)"
using index_add_vec by (simp add: module_cpx_vec_def module_vec_simps(1))
thus "dim_vec (module.lincomb (module_cpx_vec n) f (insert x F)) = n"
using insert.hyps(3) insert.prems(2) by simp
qed
lemma lincomb_vec_index [simp]:
assumes "finite F" and a2:"i < n" and "F \<subseteq> carrier_vec n" and "f: F \<rightarrow> UNIV"
shows "module.lincomb (module_cpx_vec n) f F $ i = (\<Sum>v\<in>F. f v * (v $ i))"
using assms
proof(induct F)
case empty
then show "module.lincomb (module_cpx_vec n) f {} $ i = (\<Sum>v\<in>{}. f v * v $ i)"
apply auto
using a2 module.lincomb_def abelian_monoid.finsum_empty module_cpx_vec_def
by (metis (mono_tags) abelian_group_def index_zero_vec(1) module_cpx_vec Module.module_def module_vec_simps(2))
next
case(insert x F)
have "module.lincomb (module_cpx_vec n) f (insert x F) =
f x \<cdot>\<^sub>v x \<oplus>\<^bsub>module_cpx_vec n\<^esub> module.lincomb (module_cpx_vec n) f F"
using module.lincomb_insert module_cpx_vec insert.hyps(1) module_cpx_vec_def module_vec_def
insert.prems(2) insert.hyps(2) insert.prems(3) insert_def
by (smt Pi_I' UNIV_I Un_insert_right cpx_rng_def insert_subset module_vec_simps(4)
partial_object.select_convs(1) sup_bot.comm_neutral)
then have "module.lincomb (module_cpx_vec n) f (insert x F) $ i =
(f x \<cdot>\<^sub>v x) $ i + module.lincomb (module_cpx_vec n) f F $ i"
using index_add_vec(1) a2 dim_vec_lincomb
by (metis Pi_split_insert_domain insert.hyps(1) insert.prems(2) insert.prems(3) insert_subset
module_cpx_vec_def module_vec_simps(1))
hence "module.lincomb (module_cpx_vec n) f (insert x F) $ i = f x * x $ i + (\<Sum>v\<in>F. f v * v $ i)"
using index_smult_vec a2 insert.prems(2) insert_def insert.hyps(3) by auto
with insert show "module.lincomb (module_cpx_vec n) f (insert x F) $ i = (\<Sum>v\<in>insert x F. f v * v $ i)"
by auto
qed
lemma unit_vectors_is_lin_indpt [simp]:
"module.lin_indpt cpx_rng (module_cpx_vec n) (unit_vectors n)"
proof
assume "module.lin_dep cpx_rng (module_cpx_vec n) (unit_vectors n)"
hence "\<exists>A a v. (finite A \<and> A \<subseteq> (unit_vectors n) \<and> (a \<in> A \<rightarrow> UNIV) \<and>
(module.lincomb (module_cpx_vec n) a A = \<zero>\<^bsub>module_cpx_vec n\<^esub>) \<and> (v \<in> A) \<and> (a v \<noteq> \<zero>\<^bsub>cpx_rng\<^esub>))"
using module.lin_dep_def cpx_rng_def module_cpx_vec by (smt Pi_UNIV UNIV_I)
moreover obtain A and a and v where f1:"finite A" and f2:"A \<subseteq> (unit_vectors n)" and "a \<in> A \<rightarrow> UNIV"
and f4:"module.lincomb (module_cpx_vec n) a A = \<zero>\<^bsub>module_cpx_vec n\<^esub>" and f5:"v \<in> A" and
f6:"a v \<noteq> \<zero>\<^bsub>cpx_rng\<^esub>"
using calculation by blast
moreover obtain i where f7:"v = unit_vec n i" and f8:"i < n"
using unit_vectors_def calculation by auto
ultimately have f9:"module.lincomb (module_cpx_vec n) a A $ i = (\<Sum>u\<in>A. a u * (u $ i))"
using lincomb_vec_index
by (smt carrier_dim_vec index_unit_vec(3) mem_Collect_eq subset_iff sum.cong unit_vectors_def)
moreover have "\<forall>u\<in>A.\<forall>j<n. u = unit_vec n j \<longrightarrow> j \<noteq> i \<longrightarrow> a u * (u $ i) = 0"
using unit_vectors_def index_unit_vec by (simp add: f8)
then have "(\<Sum>u\<in>A. a u * (u $ i)) = (\<Sum>u\<in>A. if u=v then a v * v $ i else 0)"
using f2 unit_vectors_def f7 by (smt mem_Collect_eq subsetCE sum.cong)
also have "\<dots> = a v * (v $ i)"
using abelian_monoid.finsum_singleton[of cpx_rng v A "\<lambda>u\<in>A. a u * (u $ i)"] cpx_abelian_monoid
f5 f1 cpx_rng_def by simp
also have "\<dots> = a v"
using f7 index_unit_vec f8 by simp
also have "\<dots> \<noteq> 0"
using f6 by (simp add: cpx_rng_def)
finally show False
using f4 module_cpx_vec_def module_vec_def index_zero_vec f8 f9 by (simp add: module_vec_simps(2))
qed