--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Mon Jul 17 15:06:08 2000 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Mon Jul 17 18:17:54 2000 +0200
@@ -20,14 +20,14 @@
is_continuous ::
"['a::{plus, minus, zero} set, 'a => real, 'a => real] => bool"
"is_continuous V norm f ==
- is_linearform V f \<and> (\<exists>c. \<forall>x \<in> V. |f x| <= c * norm x)"
+ is_linearform V f \\<and> (\\<exists>c. \\<forall>x \\<in> V. |f x| <= c * norm x)"
lemma continuousI [intro]:
- "[| is_linearform V f; !! x. x \<in> V ==> |f x| <= c * norm x |]
+ "[| is_linearform V f; !! x. x \\<in> V ==> |f x| <= c * norm x |]
==> is_continuous V norm f"
proof (unfold is_continuous_def, intro exI conjI ballI)
- assume r: "!! x. x \<in> V ==> |f x| <= c * norm x"
- fix x assume "x \<in> V" show "|f x| <= c * norm x" by (rule r)
+ assume r: "!! x. x \\<in> V ==> |f x| <= c * norm x"
+ fix x assume "x \\<in> V" show "|f x| <= c * norm x" by (rule r)
qed
lemma continuous_linearform [intro??]:
@@ -36,7 +36,7 @@
lemma continuous_bounded [intro??]:
"is_continuous V norm f
- ==> \<exists>c. \<forall>x \<in> V. |f x| <= c * norm x"
+ ==> \\<exists>c. \\<forall>x \\<in> V. |f x| <= c * norm x"
by (unfold is_continuous_def) force
subsection{* The norm of a linear form *}
@@ -66,7 +66,7 @@
constdefs
B :: "[ 'a set, 'a => real, 'a::{plus, minus, zero} => real ] => real set"
"B V norm f ==
- {#0} \<union> {|f x| * rinv (norm x) | x. x \<noteq> 0 \<and> x \<in> V}"
+ {#0} \\<union> {|f x| * rinv (norm x) | x. x \\<noteq> 0 \\<and> x \\<in> V}"
text{* $n$ is the function norm of $f$, iff
$n$ is the supremum of $B$.
@@ -85,9 +85,9 @@
"function_norm f V norm == Sup UNIV (B V norm f)"
syntax
- function_norm :: " ['a => real, 'a set, 'a => real] => real" ("\<parallel>_\<parallel>_,_")
+ function_norm :: " ['a => real, 'a set, 'a => real] => real" ("\\<parallel>_\\<parallel>_,_")
-lemma B_not_empty: "#0 \<in> B V norm f"
+lemma B_not_empty: "#0 \\<in> B V norm f"
by (unfold B_def, force)
text {* The following lemma states that every continuous linear form
@@ -95,35 +95,35 @@
lemma ex_fnorm [intro??]:
"[| is_normed_vectorspace V norm; is_continuous V norm f|]
- ==> is_function_norm f V norm \<parallel>f\<parallel>V,norm"
+ ==> is_function_norm f V norm \\<parallel>f\\<parallel>V,norm"
proof (unfold function_norm_def is_function_norm_def
is_continuous_def Sup_def, elim conjE, rule selectI2EX)
assume "is_normed_vectorspace V norm"
assume "is_linearform V f"
- and e: "\<exists>c. \<forall>x \<in> V. |f x| <= c * norm x"
+ and e: "\\<exists>c. \\<forall>x \\<in> V. |f x| <= c * norm x"
txt {* The existence of the supremum is shown using the
completeness of the reals. Completeness means, that
every non-empty bounded set of reals has a
supremum. *}
- show "\<exists>a. is_Sup UNIV (B V norm f) a"
+ show "\\<exists>a. is_Sup UNIV (B V norm f) a"
proof (unfold is_Sup_def, rule reals_complete)
txt {* First we have to show that $B$ is non-empty: *}
- show "\<exists>X. X \<in> B V norm f"
+ show "\\<exists>X. X \\<in> B V norm f"
proof (intro exI)
- show "#0 \<in> (B V norm f)" by (unfold B_def, force)
+ show "#0 \\<in> (B V norm f)" by (unfold B_def, force)
qed
txt {* Then we have to show that $B$ is bounded: *}
- from e show "\<exists>Y. isUb UNIV (B V norm f) Y"
+ from e show "\\<exists>Y. isUb UNIV (B V norm f) Y"
proof
txt {* We know that $f$ is bounded by some value $c$. *}
- fix c assume a: "\<forall>x \<in> V. |f x| <= c * norm x"
+ fix c assume a: "\\<forall>x \\<in> V. |f x| <= c * norm x"
def b == "max c #0"
show "?thesis"
@@ -133,7 +133,7 @@
txt{* To proof the thesis, we have to show that there is
some constant $b$, such that $y \leq b$ for all $y\in B$.
Due to the definition of $B$ there are two cases for
- $y\in B$. If $y = 0$ then $y \leq idt{max}\ap c\ap 0$: *}
+ $y\in B$. If $y = 0$ then $y \leq \idt{max}\ap c\ap 0$: *}
fix y assume "y = (#0::real)"
show "y <= b" by (simp! add: le_max2)
@@ -144,7 +144,7 @@
next
fix x y
- assume "x \<in> V" "x \<noteq> 0" (***
+ assume "x \\<in> V" "x \\<noteq> 0" (***
have ge: "#0 <= rinv (norm x)";
by (rule real_less_imp_le, rule real_rinv_gt_zero,
@@ -155,11 +155,11 @@
show "#0 < norm x"; ..;
qed;
qed; *** )
- have nz: "norm x \<noteq> #0"
+ have nz: "norm x \\<noteq> #0"
by (rule not_sym, rule lt_imp_not_eq,
rule normed_vs_norm_gt_zero) (***
proof (rule not_sym);
- show "#0 \<noteq> norm x";
+ show "#0 \\<noteq> norm x";
proof (rule lt_imp_not_eq);
show "#0 < norm x"; ..;
qed;
@@ -180,7 +180,7 @@
by (rule real_mult_assoc)
also have "(norm x * rinv (norm x)) = (#1::real)"
proof (rule real_mult_inv_right1)
- show nz: "norm x \<noteq> #0"
+ show nz: "norm x \\<noteq> #0"
by (rule not_sym, rule lt_imp_not_eq,
rule normed_vs_norm_gt_zero)
qed
@@ -195,7 +195,7 @@
lemma fnorm_ge_zero [intro??]:
"[| is_continuous V norm f; is_normed_vectorspace V norm |]
- ==> #0 <= \<parallel>f\<parallel>V,norm"
+ ==> #0 <= \\<parallel>f\\<parallel>V,norm"
proof -
assume c: "is_continuous V norm f"
and n: "is_normed_vectorspace V norm"
@@ -206,11 +206,11 @@
show ?thesis
proof (unfold function_norm_def, rule sup_ub1)
- show "\<forall>x \<in> (B V norm f). #0 <= x"
+ show "\\<forall>x \\<in> (B V norm f). #0 <= x"
proof (intro ballI, unfold B_def,
elim UnE singletonE CollectE exE conjE)
fix x r
- assume "x \<in> V" "x \<noteq> 0"
+ assume "x \\<in> V" "x \\<noteq> 0"
and r: "r = |f x| * rinv (norm x)"
have ge: "#0 <= |f x|" by (simp! only: abs_ge_zero)
@@ -228,13 +228,13 @@
txt {* Since $f$ is continuous the function norm exists: *}
- have "is_function_norm f V norm \<parallel>f\<parallel>V,norm" ..
+ have "is_function_norm f V norm \\<parallel>f\\<parallel>V,norm" ..
thus "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"
by (unfold is_function_norm_def function_norm_def)
txt {* $B$ is non-empty by construction: *}
- show "#0 \<in> B V norm f" by (rule B_not_empty)
+ show "#0 \\<in> B V norm f" by (rule B_not_empty)
qed
qed
@@ -245,10 +245,10 @@
*}
lemma norm_fx_le_norm_f_norm_x:
- "[| is_continuous V norm f; is_normed_vectorspace V norm; x \<in> V |]
- ==> |f x| <= \<parallel>f\<parallel>V,norm * norm x"
+ "[| is_continuous V norm f; is_normed_vectorspace V norm; x \\<in> V |]
+ ==> |f x| <= \\<parallel>f\\<parallel>V,norm * norm x"
proof -
- assume "is_normed_vectorspace V norm" "x \<in> V"
+ assume "is_normed_vectorspace V norm" "x \\<in> V"
and c: "is_continuous V norm f"
have v: "is_vectorspace V" ..
@@ -265,31 +265,29 @@
have "|f x| = |f 0|" by (simp!)
also from v continuous_linearform have "f 0 = #0" ..
also note abs_zero
- also have "#0 <= \<parallel>f\<parallel>V,norm * norm x"
+ also have "#0 <= \\<parallel>f\\<parallel>V,norm * norm x"
proof (rule real_le_mult_order1a)
- show "#0 <= \<parallel>f\<parallel>V,norm" ..
+ show "#0 <= \\<parallel>f\\<parallel>V,norm" ..
show "#0 <= norm x" ..
qed
finally
- show "|f x| <= \<parallel>f\<parallel>V,norm * norm x" .
+ show "|f x| <= \\<parallel>f\\<parallel>V,norm * norm x" .
next
- assume "x \<noteq> 0"
- have n: "#0 <= norm x" ..
- have nz: "norm x \<noteq> #0"
- proof (rule lt_imp_not_eq [RS not_sym])
- show "#0 < norm x" ..
- qed
+ assume "x \\<noteq> 0"
+ have n: "#0 < norm x" ..
+ hence nz: "norm x \\<noteq> #0"
+ by (simp only: lt_imp_not_eq)
txt {* For the case $x\neq \zero$ we derive the following
fact from the definition of the function norm:*}
- have l: "|f x| * rinv (norm x) <= \<parallel>f\<parallel>V,norm"
+ have l: "|f x| * rinv (norm x) <= \\<parallel>f\\<parallel>V,norm"
proof (unfold function_norm_def, rule sup_ub)
from ex_fnorm [OF _ c]
show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"
by (simp! add: is_function_norm_def function_norm_def)
- show "|f x| * rinv (norm x) \<in> B V norm f"
+ show "|f x| * rinv (norm x) \\<in> B V norm f"
by (unfold B_def, intro UnI2 CollectI exI [of _ x]
conjI, simp)
qed
@@ -298,14 +296,12 @@
have "|f x| = |f x| * #1" by (simp!)
also from nz have "#1 = rinv (norm x) * norm x"
- by (rule real_mult_inv_left1 [RS sym])
- also
- have "|f x| * ... = |f x| * rinv (norm x) * norm x"
+ by (simp add: real_mult_inv_left1)
+ also have "|f x| * ... = |f x| * rinv (norm x) * norm x"
by (simp! add: real_mult_assoc)
- also have "... <= \<parallel>f\<parallel>V,norm * norm x"
- by (rule real_mult_le_le_mono2 [OF n l])
- finally
- show "|f x| <= \<parallel>f\<parallel>V,norm * norm x" .
+ also from n l have "... <= \\<parallel>f\\<parallel>V,norm * norm x"
+ by (simp add: real_mult_le_le_mono2)
+ finally show "|f x| <= \\<parallel>f\\<parallel>V,norm * norm x" .
qed
qed
@@ -318,13 +314,13 @@
lemma fnorm_le_ub:
"[| is_continuous V norm f; is_normed_vectorspace V norm;
- \<forall>x \<in> V. |f x| <= c * norm x; #0 <= c |]
- ==> \<parallel>f\<parallel>V,norm <= c"
+ \\<forall>x \\<in> V. |f x| <= c * norm x; #0 <= c |]
+ ==> \\<parallel>f\\<parallel>V,norm <= c"
proof (unfold function_norm_def)
assume "is_normed_vectorspace V norm"
assume c: "is_continuous V norm f"
- assume fb: "\<forall>x \<in> V. |f x| <= c * norm x"
- and "#0 <= c"
+ assume fb: "\\<forall>x \\<in> V. |f x| <= c * norm x"
+ and "#0 <= c"
txt {* Suppose the inequation holds for some $c\geq 0$.
If $c$ is an upper bound of $B$, then $c$ is greater
@@ -343,7 +339,7 @@
show "isUb UNIV (B V norm f) c"
proof (intro isUbI setleI ballI)
- fix y assume "y \<in> B V norm f"
+ fix y assume "y \\<in> B V norm f"
thus le: "y <= c"
proof (unfold B_def, elim UnE CollectE exE conjE singletonE)
@@ -358,14 +354,14 @@
next
fix x
- assume "x \<in> V" "x \<noteq> 0"
+ assume "x \\<in> V" "x \\<noteq> 0"
have lz: "#0 < norm x"
by (simp! add: normed_vs_norm_gt_zero)
- have nz: "norm x \<noteq> #0"
+ have nz: "norm x \\<noteq> #0"
proof (rule not_sym)
- from lz show "#0 \<noteq> norm x"
+ from lz show "#0 \\<noteq> norm x"
by (simp! add: order_less_imp_not_eq)
qed