# HG changeset patch
# User huffman
# Date 1215020143 -7200
# Node ID 22b6281d671927b029fe6a902302db519f33ab2b
# Parent  2d16f20adb4d6a48b2bc1820cd70d8232d9c0afc
use begin and end for proofs in locales

diff -r 2d16f20adb4d -r 22b6281d6719 src/HOL/Real/RealVector.thy
--- a/src/HOL/Real/RealVector.thy	Wed Jul 02 18:13:10 2008 +0200
+++ b/src/HOL/Real/RealVector.thy	Wed Jul 02 19:35:43 2008 +0200
@@ -14,25 +14,26 @@
 locale additive =
   fixes f :: "'a::ab_group_add \<Rightarrow> 'b::ab_group_add"
   assumes add: "f (x + y) = f x + f y"
+begin
 
-lemma (in additive) zero: "f 0 = 0"
+lemma zero: "f 0 = 0"
 proof -
   have "f 0 = f (0 + 0)" by simp
   also have "\<dots> = f 0 + f 0" by (rule add)
   finally show "f 0 = 0" by simp
 qed
 
-lemma (in additive) minus: "f (- x) = - f x"
+lemma minus: "f (- x) = - f x"
 proof -
   have "f (- x) + f x = f (- x + x)" by (rule add [symmetric])
   also have "\<dots> = - f x + f x" by (simp add: zero)
   finally show "f (- x) = - f x" by (rule add_right_imp_eq)
 qed
 
-lemma (in additive) diff: "f (x - y) = f x - f y"
+lemma diff: "f (x - y) = f x - f y"
 by (simp add: diff_def add minus)
 
-lemma (in additive) setsum: "f (setsum g A) = (\<Sum>x\<in>A. f (g x))"
+lemma setsum: "f (setsum g A) = (\<Sum>x\<in>A. f (g x))"
 apply (cases "finite A")
 apply (induct set: finite)
 apply (simp add: zero)
@@ -40,6 +41,7 @@
 apply (simp add: zero)
 done
 
+end
 
 subsection {* Real vector spaces *}
 
@@ -644,8 +646,9 @@
   constrains f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes scaleR: "f (scaleR r x) = scaleR r (f x)"
   assumes bounded: "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K"
+begin
 
-lemma (in bounded_linear) pos_bounded:
+lemma pos_bounded:
   "\<exists>K>0. \<forall>x. norm (f x) \<le> norm x * K"
 proof -
   obtain K where K: "\<And>x. norm (f x) \<le> norm x * K"
@@ -663,13 +666,15 @@
   qed
 qed
 
-lemma (in bounded_linear) nonneg_bounded:
+lemma nonneg_bounded:
   "\<exists>K\<ge>0. \<forall>x. norm (f x) \<le> norm x * K"
 proof -
   from pos_bounded
   show ?thesis by (auto intro: order_less_imp_le)
 qed
 
+end
+
 locale bounded_bilinear =
   fixes prod :: "['a::real_normed_vector, 'b::real_normed_vector]
                  \<Rightarrow> 'c::real_normed_vector"
@@ -679,8 +684,9 @@
   assumes scaleR_left: "prod (scaleR r a) b = scaleR r (prod a b)"
   assumes scaleR_right: "prod a (scaleR r b) = scaleR r (prod a b)"
   assumes bounded: "\<exists>K. \<forall>a b. norm (prod a b) \<le> norm a * norm b * K"
+begin
 
-lemma (in bounded_bilinear) pos_bounded:
+lemma pos_bounded:
   "\<exists>K>0. \<forall>a b. norm (a ** b) \<le> norm a * norm b * K"
 apply (cut_tac bounded, erule exE)
 apply (rule_tac x="max 1 K" in exI, safe)
@@ -690,40 +696,40 @@
 apply (intro mult_nonneg_nonneg norm_ge_zero)
 done
 
-lemma (in bounded_bilinear) nonneg_bounded:
+lemma nonneg_bounded:
   "\<exists>K\<ge>0. \<forall>a b. norm (a ** b) \<le> norm a * norm b * K"
 proof -
   from pos_bounded
   show ?thesis by (auto intro: order_less_imp_le)
 qed
 
-lemma (in bounded_bilinear) additive_right: "additive (\<lambda>b. prod a b)"
+lemma additive_right: "additive (\<lambda>b. prod a b)"
 by (rule additive.intro, rule add_right)
 
-lemma (in bounded_bilinear) additive_left: "additive (\<lambda>a. prod a b)"
+lemma additive_left: "additive (\<lambda>a. prod a b)"
 by (rule additive.intro, rule add_left)
 
-lemma (in bounded_bilinear) zero_left: "prod 0 b = 0"
+lemma zero_left: "prod 0 b = 0"
 by (rule additive.zero [OF additive_left])
 
-lemma (in bounded_bilinear) zero_right: "prod a 0 = 0"
+lemma zero_right: "prod a 0 = 0"
 by (rule additive.zero [OF additive_right])
 
-lemma (in bounded_bilinear) minus_left: "prod (- a) b = - prod a b"
+lemma minus_left: "prod (- a) b = - prod a b"
 by (rule additive.minus [OF additive_left])
 
-lemma (in bounded_bilinear) minus_right: "prod a (- b) = - prod a b"
+lemma minus_right: "prod a (- b) = - prod a b"
 by (rule additive.minus [OF additive_right])
 
-lemma (in bounded_bilinear) diff_left:
+lemma diff_left:
   "prod (a - a') b = prod a b - prod a' b"
 by (rule additive.diff [OF additive_left])
 
-lemma (in bounded_bilinear) diff_right:
+lemma diff_right:
   "prod a (b - b') = prod a b - prod a b'"
 by (rule additive.diff [OF additive_right])
 
-lemma (in bounded_bilinear) bounded_linear_left:
+lemma bounded_linear_left:
   "bounded_linear (\<lambda>a. a ** b)"
 apply (unfold_locales)
 apply (rule add_left)
@@ -733,7 +739,7 @@
 apply (simp add: mult_ac)
 done
 
-lemma (in bounded_bilinear) bounded_linear_right:
+lemma bounded_linear_right:
   "bounded_linear (\<lambda>b. a ** b)"
 apply (unfold_locales)
 apply (rule add_right)
@@ -743,10 +749,12 @@
 apply (simp add: mult_ac)
 done
 
-lemma (in bounded_bilinear) prod_diff_prod:
+lemma prod_diff_prod:
   "(x ** y - a ** b) = (x - a) ** (y - b) + (x - a) ** b + a ** (y - b)"
 by (simp add: diff_left diff_right)
 
+end
+
 interpretation mult:
   bounded_bilinear ["op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra"]
 apply (rule bounded_bilinear.intro)