# HG changeset patch
# User ballarin
# Date 1064927459 -7200
# Node ID 5369d671f1009b48d660d5c73c8f6e973413d612
# Parent  7bf882b0a51e69ce330b50f08d9e900352e25b27
Improvements to Isar/Locales:  premises generated by "includes" elements
changed.

diff -r 7bf882b0a51e -r 5369d671f100 src/HOL/Real/HahnBanach/FunctionNorm.thy
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Tue Sep 30 15:10:26 2003 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Tue Sep 30 15:10:59 2003 +0200
@@ -151,7 +151,7 @@
   shows "b \<le> \<parallel>f\<parallel>\<hyphen>V"
 proof -
   have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
-    by (unfold B_def fn_norm_def) (rule fn_norm_works)
+    by (unfold B_def fn_norm_def) (rule fn_norm_works [OF _ continuous.intro])
   from this and b show ?thesis ..
 qed
 
@@ -161,7 +161,7 @@
   shows "\<parallel>f\<parallel>\<hyphen>V \<le> y"
 proof -
   have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
-    by (unfold B_def fn_norm_def) (rule fn_norm_works)
+    by (unfold B_def fn_norm_def) (rule fn_norm_works [OF _ continuous.intro])
   from this and b show ?thesis ..
 qed
 
@@ -175,7 +175,7 @@
     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)"
-    by (unfold B_def fn_norm_def) (rule fn_norm_works)
+    by (unfold B_def fn_norm_def) (rule fn_norm_works [OF _ continuous.intro])
   moreover have "0 \<in> B V f" ..
   ultimately show ?thesis ..
 qed
@@ -198,7 +198,9 @@
   also have "\<bar>\<dots>\<bar> = 0" by simp
   also have "\<dots> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
   proof (rule real_le_mult_order1a)
-    show "0 \<le> \<parallel>f\<parallel>\<hyphen>V" by (unfold B_def fn_norm_def) rule
+    show "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
+      by (unfold B_def fn_norm_def)
+        (rule fn_norm_ge_zero [OF _ continuous.intro])
     show "0 \<le> norm x" ..
   qed
   finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" .
@@ -212,7 +214,7 @@
     from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f"
       by (auto simp add: B_def real_divide_def)
     then show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
-      by (unfold B_def fn_norm_def) (rule fn_norm_ub)
+      by (unfold B_def fn_norm_def) (rule fn_norm_ub [OF _ continuous.intro])
   qed
   finally show ?thesis .
 qed
@@ -254,6 +256,6 @@
     qed
     finally show ?thesis .
   qed
-qed
+qed (simp_all! add: continuous_def)
 
 end
diff -r 7bf882b0a51e -r 5369d671f100 src/HOL/Real/HahnBanach/HahnBanach.thy
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Tue Sep 30 15:10:26 2003 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Tue Sep 30 15:10:59 2003 +0200
@@ -339,10 +339,11 @@
   have FE: "F \<unlhd> E" .
   have F: "vectorspace F" ..
   have linearform: "linearform F f" .
-  have F_norm: "normed_vectorspace F norm" ..
+  have F_norm: "normed_vectorspace F norm"
+    by (rule subspace_normed_vs [OF _ _ _ norm.intro])
   have ge_zero: "0 \<le> \<parallel>f\<parallel>\<hyphen>F"
     by (rule normed_vectorspace.fn_norm_ge_zero
-      [OF F_norm, folded B_def fn_norm_def])
+      [OF F_norm _ continuous.intro, 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>"} *}
@@ -394,7 +395,7 @@
     fix x assume "x \<in> F"
     show "\<bar>f x\<bar> \<le> p x"
       by (unfold p_def) (rule normed_vectorspace.fn_norm_le_cong
-        [OF F_norm, folded B_def fn_norm_def])
+        [OF F_norm _ continuous.intro, folded B_def fn_norm_def])
   qed
 
   txt {* Using the fact that @{text p} is a seminorm and @{text f} is bounded
@@ -443,7 +444,7 @@
       with b show "\<bar>g x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
         by (simp only: p_def)
     qed
-    from continuous.axioms [OF g_cont] this ge_zero
+    from linearformE g_cont this ge_zero
     show "\<parallel>g\<parallel>\<hyphen>E \<le> \<parallel>f\<parallel>\<hyphen>F"
       by (rule fn_norm_least [of g, folded B_def fn_norm_def])
 
@@ -456,7 +457,7 @@
 	fix x assume x: "x \<in> F"
 	from a have "g x = f x" ..
 	hence "\<bar>f x\<bar> = \<bar>g x\<bar>" by (simp only:)
-	also from continuous.axioms [OF g_cont]
+	also from linearformE g_cont
 	have "\<dots> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
 	proof (rule fn_norm_le_cong [of g, folded B_def fn_norm_def])
 	  from FE x show "x \<in> E" ..
@@ -464,8 +465,10 @@
 	finally show "\<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>" .
       qed
       show "0 \<le> \<parallel>g\<parallel>\<hyphen>E"
-	using continuous.axioms [OF g_cont]
+	using linearformE g_cont
 	by (rule fn_norm_ge_zero [of g, folded B_def fn_norm_def])
+    next
+      show "continuous F norm f" by (rule continuous.intro)
     qed
   qed
   with linearformE a g_cont show ?thesis by blast