*To*: RF Todd <R.F.Todd at sms.ed.ac.uk>*Subject*: Re: [isabelle] Help with code*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Tue, 13 Nov 2007 09:31:45 +0100*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <20071112205014.gumlz6rekgs0okwo@www.sms.ed.ac.uk>*References*: <20071112205014.gumlz6rekgs0okwo@www.sms.ed.ac.uk>*User-agent*: Thunderbird 2.0.0.0 (Macintosh/20070326)

Looks like the justification for the previous line is missing. Tobias RF Todd schrieb:

Hi all,I am trying to get the following code2run but it comes up with anIllegal Command error at the 'hence' in the lemma double_sum_aux: and iwonder if you know why? I am new to Isabelle/Isar so not too sure how tomake it work.Rachel theory CauchySchwarz imports Complex_Main begin lemma real_sq: "(a::real)*a = a^2" proof - have "2 = Suc 1" by simp hence "a^2 = a^(Suc 1)" apply - apply (erule subst) by simp also have "\<dots> = a*(a^1)" by simp also have "\<dots> = a*a" by simp finally have "a^2 = a*a" by auto thus ?thesis by simp qed lemma real_mult_wkorder: fixes x::real assumes xge0: "0 \<le> x" and yge0: "0 \<le> y" shows "0 \<le> x*y" proof cases assume "x = 0" thus ?thesis by simp next assume "x \<noteq> 0" with xge0 have xgt0: "x > 0" by simp show ?thesis proof cases assume "y = 0" thus ?thesis by simp next assume "y \<noteq> 0" with yge0 have "y > 0" by simp with xgt0 have "x*y > 0" by (rule real_mult_order) thus ?thesis by simp qed qed lemma real_mult_order2: fixes c::real assumes c0: "0 \<le> c" and xy: "x \<le> y" shows "c*x \<le> c*y" proof cases assume "0 = c" thus ?thesis by auto next assume "0 \<noteq> c" with c0 have "0 < c" by simp with xy show ?thesis by simp qed lemma real_sq_order: fixes x::real assumes xgt0: "0 \<le> x" and ygt0: "0 \<le> y" and sq: "x^2 \<le> y^2" shows "x \<le> y" proof (rule ccontr) assume "\<not>(x \<le> y)" then have ylx: "y < x" by simp hence "y \<le> x" by simp with xgt0 have "x*y \<le> x*x" by (rule real_mult_order2) moreover have "\<not>(y = 0)" proof assume "y = 0" with ylx have xg0: "0 < x" by simp from xg0 xg0 have "0 < x*x" by (rule real_mult_order) moreover have "y*y = 0" by simp ultimately show False using sq by auto qed with ygt0 have "0 < y" by simp with ylx have "y*y < x*y" by auto ultimately have "y*y < x*x" by simp with sq show False by (auto simp add: real_sq) qed lemma real_add_mult_distrib2: fixes x::real shows "x*(y+z) = x*y + x*z" proof - have "x*(y+z) = (y+z)*x" by simp also have "\<dots> = y*x + z*x" by (rule real_add_mult_distrib) also have "\<dots> = x*y + x*z" by simp finally show ?thesis . qed lemma real_add_mult_distrib_ex: fixes x::real shows "(x+y)*(z+w) = x*z + x*w + y*z + y*w" proof - have "(x+y)*(z+w) = x*(z+w) + y*(z+w)" by (rule real_add_mult_distrib)also have "\<dots> = x*z + x*w + y*z + y*w" by (simp add:real_add_mult_distrib2)finally show ?thesis by simp qed lemma real_sub_mult_distrib_ex: fixes x::real shows "(x-y)*(z-w) = x*z - x*w - y*z + y*w" proof - have zw: "(z-w) = (z+ -w)" by simp have "(x-y)*(z-w) = (x+ -y)*(z-w)" by simp also have "\<dots> = x*(z-w) + -y*(z-w)" by (rule real_add_mult_distrib) also from zw have "\<dots> = x*(z+ -w) + -y*(z+ -w)" apply - apply (erule subst) by simpalso have "\<dots> = x*z + x*-w + -y*z + -y*-w" by (simp add:real_add_mult_distrib2)finally show ?thesis by simp qed lemma double_sum_expand: fixes f::"nat \<Rightarrow> real"shows "(\<Sum>j\<in>{1..n}. f j)*(\<Sum>j\<in>{1..n}. g j) =(\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}.f k*g j))"proof (induct n) case 0 show ?case by simp next case (Suc n) { assume nz: "n = 0" then have"(\<Sum>j\<in>{1..Suc n}. f j)*(\<Sum>j\<in>{1..Suc n}. g j) = f 1* g 1" by simpmoreover from nz have"(\<Sum>k\<in>{1..Suc n}.(\<Sum>j\<in>{1..Suc n}.(f k)*(g j))) = f1 * g 1" by autoultimately have ?case by simp } moreover { assume "\<not>(n = 0)" then have nge1: "n \<ge> 1" by simp hence sn: "Suc n > 1" by simp let ?f = "\<Sum>j\<in>{1..n}. f j" and ?g = "\<Sum>j\<in>{1..n}. g j"from sn setsum_cl_ivl_Suc have "(\<Sum>j\<in>{1..Suc n}. f j) = ?f + f(Suc n)" by automoreoverfrom sn setsum_cl_ivl_Suc have "(\<Sum>j\<in>{1..Suc n}. g j) = ?g + g(Suc n)" by autoultimately have"(\<Sum>j\<in>{1..Suc n}. f j)*(\<Sum>j\<in>{1..Suc n}. g j) = (?f +f (Suc n))*(?g + g (Suc n))" by simpalso have"\<dots> = ?f * ?g + ?f*(g (Suc n)) + (f (Suc n))*?g + (f (Sucn))*(g (Suc n))"by (auto simp add: real_add_mult_distrib_ex) also have"\<dots> = (\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}.(f k)*(g j))) +?f*(g (Suc n)) + (f (Suc n))*?g + (f (Suc n))*(g (Suc n))" using Suc bysimpalso have"\<dots> = (\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}.(f k)*(g j))) +(\<Sum>j\<in>{1..n}. f j * g (Suc n)) + ?g * (f (Suc n)) + (f (Sucn))*(g (Suc n))" by (auto simp add: setsum_mult real_mult_commute)also have"\<dots> = (\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}.(f k)*(g j)) + (fk * g (Suc n))) + (?g * f (Suc n)) + (f (Suc n))*(g (Suc n))" by (autosimp add: setsum_addf [symmetric])also have"\<dots> = (\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..(Suc n)}.(f k)*(gj))) + (\<Sum>j\<in>{1..n}. g j)*(f (Suc n)) + g(Suc n)*(f (Suc n))" bysimpalso have"\<dots> = (\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..(Suc n)}.(f k)*(gj))) + (\<Sum>j\<in>{1..n}.g j * f (Suc n)) + g(Suc n)*(f (Suc n))" by(auto simp add: setsum_mult real_mult_commute)also from sn setsum_cl_ivl_Suc have"\<dots> = (\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..(Suc n)}.(f k)*(gj))) + (\<Sum>j\<in>{1..Suc n}.(g j)*(f (Suc n)))" by autoalso from sn setsum_cl_ivl_Suc have"\<dots> = (\<Sum>k\<in>{1..Suc n}.(\<Sum>j\<in>{1..(Suc n)}.(fk)*(g j)))" by (auto simp add: real_mult_commute)finally have ?case . } ultimately show ?case by (rule case_split_thm) qed lemma real_sq_exp: fixes x::real shows "(x*y)^2 = x^2 * y^2" proof - have "(x*y)^2 = (x*y)*(x*y)" by (simp add: real_sq) also have "\<dots> = (x*x)*(y*y)" by simp also have "\<dots> = x^2 * y^2" by (simp add: real_sq) finally show ?thesis . qed lemma real_diff_exp: fixes x::real shows "(x-y)^2 = x^2 + y^2 - 2*x*y" proof - have "(x-y)^2 = (x-y)*(x-y)" by (simp only: real_sq)also from real_sub_mult_distrib_ex have "\<dots> = x*x - x*y - y*x +y*y" by simpfinally show ?thesis by (auto simp add: real_sq) qed lemma double_sum_equiv: fixes f::"nat \<Rightarrow> real"shows "(\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}. f k * g j)) =(\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}. f j * g k))"proof -have "(\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}. (f k)*(g j))) =(\<Sum>j\<in>{1..n}.f j)*(\<Sum>j\<in>{1..n}.g j)" by (simp only:double_sum_expand)also have "\<dots> = (\<Sum>j\<in>{1..n}. g j)*(\<Sum>j\<in>{1..n}. fj)" by simpalso have "\<dots> = (\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}. g k * fj))" by (simp only: double_sum_expand)finally show ?thesis by (simp add: real_mult_commute) qedtext {* Theorem: Take $V$ to be some vector space possessing a norm andinner product, then for all $a,b \in V$ the following inequality holds:@{text "|a.b| \<le> \<parallel>a\<parallel> * \<parallel>b\<parallel>"}.Specifically, in the Real case, the norm is in the Euclidean length andthe inner product is the standard dot product. *}types vector = "(nat \<Rightarrow> real)*nat"; constdefs ith :: "vector \<Rightarrow> nat \<Rightarrow> real" "ith v i \<equiv> (fst v) i" vlen :: "vector \<Rightarrow> nat" "vlen v \<equiv> (snd v)" constdefs dot :: "vector \<Rightarrow> vector \<Rightarrow> real" "dot a b \<equiv> (\<Sum>j\<in>{1..(vlen a)}.(ith a j)*(ith b j))" norm :: "vector \<Rightarrow> real" "norm v \<equiv> sqrt (\<Sum>j\<in>{1..(vlen v)}.(ith v j)^2)" syntax(HTML output) "norm" :: "vector \<Rightarrow> real" lemma norm_dot: "norm(v)=sqrt(dot v v)" proof -have "sqrt(dot v v) = sqrt(\<Sum>j\<in>{1..(vlen v)}. (ith v j)*(ith vj))" by (unfold dot_def, simp)also with real_sq have "\<dots> = sqrt(\<Sum>j\<in>{1..(vlen v)}.(ithv j)^2)" by simpalso have "\<dots> = norm v" by (unfold norm_def, simp) finally show ?thesis .. qed lemma norm_pos: "norm v \<ge> 0" proof - have "\<forall>j. (ith v j)^2 \<ge> 0" by (unfold ith_def, auto) hence "\<forall>j\<in>{1..(vlen v)}. (ith v j)^2 \<ge> 0" by simpwith setsum_nonneg have "(\<Sum>j\<in>{1..(vlen v)}. (ith v j)^2)\<ge> 0" .with real_sqrt_ge_zero have "sqrt(\<Sum>j\<in>{1..(vlen v)}. (ith vj)^2) \<ge> 0" .thus ?thesis by (unfold norm_def) qed lemma double_sum_aux: fixes f::"nat \<Rightarrow> real"shows "(\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}. f k * g j)) =(\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}.(f k * g j + f j * g k)/2))"proof -have "2 * (\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}. f k * g j)) =(\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}. f k * g j)) +(\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}. f k * g j))" by simpalso have "\<dots> = (\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}. f k * gj)) + (\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}. f j * g k))" by (simponly: double_sum_equiv)also have "\<dots> = (\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}. f k * gj + f j * g k))" by (auto simp add: setsum_addf)finally have "2 * (\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}. f k * g j))= (\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}. f k * g j + f j * g k))"hence "(\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}. f k * g j)) =(\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}.(f k * g j + f j * g k)))*(1/2)"by autoalso have "\<dots> = (\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}.(f k * gj + f j* g k)*(1/2)))" by (simp add: setsum_mult real_mult_commute)finally show ?thesis by (auto simp add: inverse_eq_divide) qed theorem CauchySchwarzReal: fixes x::vector assumes "vlen x = vlen y" shows "|dot x y| \<le> (norm x)*(norm y)" proof - have "0 \<le> |dot x y|" by simpmoreover have "0 \<le> (norm x)*(norm y)" by (auto simp add: norm_posintro: mult_nonneg_nonneg)moreover have "|dot x y|^2 \<le> ((norm x)*(norm y))^2" proof - txt {* We can rewrite the goal in the following form \<dots> *} have "((norm x)*(norm y))^2 - |dot x y|^2 \<ge> 0" proof - obtain n where nx: "n = vlen x" by simp hence ny: "n = vlen y" by simp { txt {* Some preliminary simplification rules. *} have "\<forall>j\<in>{1..n}. (ith x j)^2 \<ge> 0" by simphence "(\<Sum>j\<in>{1..n}. (ith x j)^2) \<ge> 0" by (rulesetseum_nonneg)hence xp: "sqrt (\<Sum>j\<in>{1..n}.(ith x j)^2 =(\<Sum>j\<in>{1..n}.(ith x j)^2)" by (rule real_sqrt_pow2)have "\<forall>j\<in>{1..n}.(ith y j)^2 \<ge> 0" by simphence "(\<Sum>j\<in>{1..n}.(ith y j)^2) \<ge> 0" by (rulesetsum_nonneg)hence yp: "(sqrt (\<Sum>j\<in>{1..n}.(ith y j)^2))^2 =(\<Sum>j\<in>{1..n}.(ith y j)^2)" by (rule real_sqrt_pow2)txt {* The main result of this section is that @{text"(\<parallel>x\<parallel>*\<parallel>y\<parallel>)^2"} can be written asa double sum. *}have "((norm x)*(norm y))^2 = (norm x)^2 * (norm y)^2" by (simpadd: real_sq_exp)also from nx ny have "\<dots> = (sqrt (\<Sum>j\<in>{1..n}.(ith xj)^2))^2 * (sqrt (\<Sum>j\<in>{1..n}.(ith y j)^2))^2" by (unfoldnorm_def, auto)also from xp yp have "\<dots> = (\<Sum>j\<in>{1..n}.(ith xj)^2)*(\<Sum>j\<in>{1..n}.(ith y j)^2)" by simpalso from double_sum_expand have "\<dots> =(\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}.(ith x k)^2)*(ith y j)^2)))" .finally have "((norm x)*(norm y))^2 =(\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}.(ith x k)^2)*(ith y j)^2)))"} moreover {txt {* We also show that @{text "|x.y|^2"} can be expressed as adouble sum. *}have "|dot x y|^2 = (dot x y)^2" by simpalso from nx have "\<dots> = (\<Sum>j\<in>{1..n}.(ith x j)*(ith yj))^2" by (unfold dot_def, simp)also from real_sq have "\<dots> = (\<Sum>j\<in>{1..n}. (ith xj)*(ith y j))*(\<Sum>j\<in>{1..n}. (ith x j)*(ith y j))" by simpalso from double_sum_expand have "\<dots> = (\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}. ((ith x k)*(ith y k))*((ith x j)*(ith y j))))" by simpfinally have "|dot x y|^2 = (\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}. ((ith x k)*(ith y k))*((ith x j)*(ith y j))))" .}txt {* We now manipulate the double sum expressions to get therequired inequality. *}ultimately have "((norm x)*(norm y))^2 - |x.y|^2 =(\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}. ((ith x k)^2)*((ith y j)^2))) -(\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}.((ith x k)*(ith y k))*((ith xj)*(ith y j))))" by simpalso have "\<dots> = (\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}. (((ithx k)^2*(ith y j)^2) + ((ith x j)^2*(ith y k)^2))/2)) -(\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}. ((ith x k)*(ith y k))*((ith xj)*(ith y j))))" by (simp only: double_sum_aux)also have "\<dots> = (\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}. (((ithx k)^2*(ith y j)^2) + ((ith x j)^2*(ith y k)^2))/2 - ((ith x k)*(ith yk))*((ith x j)*(ith y j))))" by (auto simp add: setsum_subtractf)also have "\<dots> =(\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}.(inverse 2)*2*( (((ith xk)^2*(ith y j)^2) + ((ith x j)^2*(ith y k)^2))*(1/2) - ((ith x k)*(ith yk))*((ith x j)*(ith y j)))))" by autoalso have "\<dots> =(\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}.(inverse 2)*(2*( (((ith xk)^2*(ith y j)^2) + ((ith x j)^2*(ith y k)^2))*(1/2) - ((ith x k)*(ith yk))*((ith x j)*(ith y j)))))))" by (simp only: real-mult_assoc)also have "\<dots> =(\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}.(inverse 2)*(( (((ith xk)^2*(ith y j)^2) + ((ith x j)^2*(ith y k)^2))*2*(inverse 2) - 2*((ith xk)*(ith y k))*((ith x j)*(ith y j))))))" by (auto simp add:real_add_mult_distrib real_mult_assoc mult_ac)also have "\<dots> =(\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}.(inverse 2)*((( (((ith xk)^2*(ith y j)^2) + ((ith x j)^2*(ith y k)^2))) - 2*((ith x k)*(ith yk))*((ith x j)*(ith y j)))))))" by (simp only: real_mult_assoc, simp)also have "\<dots> = (inverse2)*(\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}.((((ith x k)^2*(ith y j)^2) +((ith x j)^2*(ith y k)^2)) - 2*((ith x k)*(ith y k))*((ith x j)*(ith yj)))))" by (simp only: setseum_mult)also have "\<dots> = (inverse2)*(\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}.((ith x k)*(ith y j) - (ith xj)*(ith y k))^2))" by (simp only: real_diff_exp real_sq_exp, auto simpadd: mult_ac)also have "\<dots> \<ge> 0" proof - { fix k::nathave "\<forall>j\<in>{1..n}.((ith x k)*(ith y j) - (ith x j)*(ith yk))^2 \<ge> 0" by simphence "(\<Sum>j\<in>{1..n}.((ith x k)*(ith y j) - (ith x j)*(ith yk))^2 \<ge> 0" by (rule setsum_nonneg)}hence "\<forall>k\<in>{1..n}.(\<Sum>j\<in>{1..n}.((ith x k)*(ith yj) - (ith x j)*(ith y k))^2 \<ge> 0" by simphence "(\<Sum>k\<in>{1..n}.(\<Sum>j\<in>{1..n}.((ith x k)*(ith yj) - (ith x j)*(ith y k))^2)) \<ge> 0" by (rule setsum_nonneg)thus ?thesis by simp qed finally show "((norm x)*(norm y))^2 - |dot x y|^2 \<ge> 0" . qed thus ?thesis by simp qed ultimately show ?thesis by (rule real_sq_order) qed end

**References**:**[isabelle] Help with code***From:*RF Todd

- Previous by Date: [isabelle] Help with code
- Next by Date: [isabelle] Problems installing Isabelle
- Previous by Thread: [isabelle] Help with code
- Next by Thread: [isabelle] Problems installing Isabelle
- Cl-isabelle-users November 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list