author wenzelm Sun, 11 Mar 2012 13:39:16 +0100 changeset 46867 0883804b67bb parent 46866 b190913c3c41 child 46868 6c250adbe101
modernized locale expression, with some fluctuation of arguments;
 src/HOL/Hahn_Banach/Function_Norm.thy file | annotate | diff | comparison | revisions src/HOL/Hahn_Banach/Hahn_Banach.thy file | annotate | diff | comparison | revisions src/HOL/Hahn_Banach/Normed_Space.thy file | annotate | diff | comparison | revisions src/HOL/Hahn_Banach/Vector_Space.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Hahn_Banach/Function_Norm.thy	Sat Mar 10 23:45:47 2012 +0100
+++ b/src/HOL/Hahn_Banach/Function_Norm.thy	Sun Mar 11 13:39:16 2012 +0100
@@ -21,7 +21,8 @@
linear forms:
*}

-locale continuous = var_V + norm_syntax + linearform +
+locale continuous = linearform +
+  fixes norm :: "_ \<Rightarrow> real"    ("\<parallel>_\<parallel>")
assumes bounded: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"

declare continuous.intro [intro?] continuous_axioms.intro [intro?]
@@ -30,11 +31,11 @@
fixes norm :: "_ \<Rightarrow> real"  ("\<parallel>_\<parallel>")
assumes "linearform V f"
assumes r: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
-  shows "continuous V norm f"
+  shows "continuous V f norm"
proof
show "linearform V f" by fact
from r have "\<exists>c. \<forall>x\<in>V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" by blast
-  then show "continuous_axioms V norm f" ..
+  then show "continuous_axioms V f norm" ..
qed

@@ -71,7 +72,8 @@
supremum exists (otherwise it is undefined).
*}

-locale fn_norm = norm_syntax +
+locale fn_norm =
+  fixes norm :: "_ \<Rightarrow> real"    ("\<parallel>_\<parallel>")
fixes B defines "B V f \<equiv> {0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel> | x. x \<noteq> 0 \<and> x \<in> V}"
fixes fn_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999)
defines "\<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)"
@@ -87,10 +89,10 @@
*}

lemma (in normed_vectorspace_with_fn_norm) fn_norm_works:
-  assumes "continuous V norm f"
+  assumes "continuous V f norm"
shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
proof -
-  interpret continuous V norm f by fact
+  interpret continuous V f norm by fact
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. *}
@@ -154,39 +156,39 @@
qed

lemma (in normed_vectorspace_with_fn_norm) fn_norm_ub [iff?]:
-  assumes "continuous V norm f"
+  assumes "continuous V f norm"
assumes b: "b \<in> B V f"
shows "b \<le> \<parallel>f\<parallel>\<hyphen>V"
proof -
-  interpret continuous V norm f by fact
+  interpret continuous V f norm by fact
have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
-    using `continuous V norm f` by (rule fn_norm_works)
+    using `continuous V f norm` by (rule fn_norm_works)
from this and b show ?thesis ..
qed

lemma (in normed_vectorspace_with_fn_norm) fn_norm_leastB:
-  assumes "continuous V norm f"
+  assumes "continuous V f norm"
assumes b: "\<And>b. b \<in> B V f \<Longrightarrow> b \<le> y"
shows "\<parallel>f\<parallel>\<hyphen>V \<le> y"
proof -
-  interpret continuous V norm f by fact
+  interpret continuous V f norm by fact
have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
-    using `continuous V norm f` by (rule fn_norm_works)
+    using `continuous V f norm` by (rule fn_norm_works)
from this and b show ?thesis ..
qed

text {* The norm of a continuous function is always @{text "\<ge> 0"}. *}

lemma (in normed_vectorspace_with_fn_norm) fn_norm_ge_zero [iff]:
-  assumes "continuous V norm f"
+  assumes "continuous V f norm"
shows "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
proof -
-  interpret continuous V norm f by fact
+  interpret continuous V f norm by fact
txt {* The function norm is defined as the supremum of @{text B}.
So it is @{text "\<ge> 0"} if all elements in @{text B} are @{text "\<ge>
0"}, provided the supremum exists and @{text B} is not empty. *}
have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
-    using `continuous V norm f` by (rule fn_norm_works)
+    using `continuous V f norm` by (rule fn_norm_works)
moreover have "0 \<in> B V f" ..
ultimately show ?thesis ..
qed
@@ -199,11 +201,11 @@
*}

lemma (in normed_vectorspace_with_fn_norm) fn_norm_le_cong:
-  assumes "continuous V norm f" "linearform V f"
+  assumes "continuous V f norm" "linearform V f"
assumes x: "x \<in> V"
shows "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
proof -
-  interpret continuous V norm f by fact
+  interpret continuous V f norm by fact
interpret linearform V f by fact
show ?thesis
proof cases
@@ -212,7 +214,7 @@
also have "f 0 = 0" by rule unfold_locales
also have "\<bar>\<dots>\<bar> = 0" by simp
also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
-      using `continuous V norm f` by (rule fn_norm_ge_zero)
+      using `continuous V f norm` by (rule fn_norm_ge_zero)
from x have "0 \<le> norm x" ..
with a have "0 \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" by (simp add: zero_le_mult_iff)
finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" .
@@ -225,7 +227,7 @@
from x show "0 \<le> \<parallel>x\<parallel>" ..
from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f"
by (auto simp add: B_def divide_inverse)
-      with `continuous V norm f` show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
+      with `continuous V f norm` show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
by (rule fn_norm_ub)
qed
finally show ?thesis .
@@ -241,11 +243,11 @@
*}

lemma (in normed_vectorspace_with_fn_norm) fn_norm_least [intro?]:
-  assumes "continuous V norm f"
+  assumes "continuous V f norm"
assumes ineq: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c"
shows "\<parallel>f\<parallel>\<hyphen>V \<le> c"
proof -
-  interpret continuous V norm f by fact
+  interpret continuous V f norm by fact
show ?thesis
proof (rule fn_norm_leastB [folded B_def fn_norm_def])
fix b assume b: "b \<in> B V f"
@@ -272,7 +274,7 @@
qed
finally show ?thesis .
qed
-  qed (insert `continuous V norm f`, simp_all add: continuous_def)
+  qed (insert `continuous V f norm`, simp_all add: continuous_def)
qed

end```
```--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy	Sat Mar 10 23:45:47 2012 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy	Sun Mar 11 13:39:16 2012 +0100
@@ -356,9 +356,9 @@
fixes fn_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999)
defines "\<And>V f. \<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)"
assumes E_norm: "normed_vectorspace E norm" and FE: "subspace F E"
-    and linearform: "linearform F f" and "continuous F norm f"
+    and linearform: "linearform F f" and "continuous F f norm"
shows "\<exists>g. linearform E g
-     \<and> continuous E norm g
+     \<and> continuous E g norm
\<and> (\<forall>x \<in> F. g x = f x)
\<and> \<parallel>g\<parallel>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>F"
proof -
@@ -367,7 +367,7 @@
by (auto simp: B_def fn_norm_def) intro_locales
interpret subspace F E by fact
interpret linearform F f by fact
-  interpret continuous F norm f by fact
+  interpret continuous F f norm by fact
have E: "vectorspace E" by intro_locales
have F: "vectorspace F" by rule intro_locales
have F_norm: "normed_vectorspace F norm"
@@ -375,7 +375,7 @@
have ge_zero: "0 \<le> \<parallel>f\<parallel>\<hyphen>F"
by (rule normed_vectorspace_with_fn_norm.fn_norm_ge_zero
[OF normed_vectorspace_with_fn_norm.intro,
-       OF F_norm `continuous F norm f` , folded B_def fn_norm_def])
+       OF F_norm `continuous F f norm` , folded B_def fn_norm_def])
txt {* We define a function @{text p} on @{text E} as follows:
@{text "p x = \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"} *}
def p \<equiv> "\<lambda>x. \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
@@ -422,7 +422,7 @@
have "\<forall>x \<in> F. \<bar>f x\<bar> \<le> p x"
proof
fix x assume "x \<in> F"
-    with `continuous F norm f` and linearform
+    with `continuous F f norm` and linearform
show "\<bar>f x\<bar> \<le> p x"
unfolding p_def by (rule normed_vectorspace_with_fn_norm.fn_norm_le_cong
[OF normed_vectorspace_with_fn_norm.intro,
@@ -442,7 +442,7 @@

txt {* We furthermore have to show that @{text g} is also continuous: *}

-  have g_cont: "continuous E norm g" using linearformE
+  have g_cont: "continuous E g norm" using linearformE
proof
fix x assume "x \<in> E"
with b show "\<bar>g x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
@@ -500,7 +500,7 @@
show "0 \<le> \<parallel>g\<parallel>\<hyphen>E"
using g_cont
by (rule fn_norm_ge_zero [of g, folded B_def fn_norm_def])
-      show "continuous F norm f" by fact
+      show "continuous F f norm" by fact
qed
qed
with linearformE a g_cont show ?thesis by blast```
```--- a/src/HOL/Hahn_Banach/Normed_Space.thy	Sat Mar 10 23:45:47 2012 +0100
+++ b/src/HOL/Hahn_Banach/Normed_Space.thy	Sun Mar 11 13:39:16 2012 +0100
@@ -16,11 +16,9 @@
*}

-locale norm_syntax =
+locale seminorm =
+  fixes V :: "'a\<Colon>{minus, plus, zero, uminus} set"
fixes norm :: "'a \<Rightarrow> real"    ("\<parallel>_\<parallel>")
-
-locale seminorm = var_V + norm_syntax +
-  constrains V :: "'a\<Colon>{minus, plus, zero, uminus} set"
assumes ge_zero [iff?]: "x \<in> V \<Longrightarrow> 0 \<le> \<parallel>x\<parallel>"
and abs_homogenous [iff?]: "x \<in> V \<Longrightarrow> \<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>"
and subadditive [iff?]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"```
```--- a/src/HOL/Hahn_Banach/Vector_Space.thy	Sat Mar 10 23:45:47 2012 +0100
+++ b/src/HOL/Hahn_Banach/Vector_Space.thy	Sun Mar 11 13:39:16 2012 +0100
@@ -38,9 +38,8 @@
the neutral element of scalar multiplication.
*}

-locale var_V = fixes V
-
-locale vectorspace = var_V +
+locale vectorspace =
+  fixes V
assumes non_empty [iff, intro?]: "V \<noteq> {}"
and add_closed [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y \<in> V"
and mult_closed [iff]: "x \<in> V \<Longrightarrow> a \<cdot> x \<in> V"```