src/HOL/Real_Vector_Spaces.thy
changeset 60758 d8d85a8172b5
parent 60307 75e1aa7a450e
child 60762 bf0c76ccee8d
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Sat Jul 18 21:44:18 2015 +0200
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Sat Jul 18 22:58:50 2015 +0200
     1.3 @@ -3,13 +3,13 @@
     1.4      Author:     Johannes Hölzl
     1.5  *)
     1.6  
     1.7 -section {* Vector Spaces and Algebras over the Reals *}
     1.8 +section \<open>Vector Spaces and Algebras over the Reals\<close>
     1.9  
    1.10  theory Real_Vector_Spaces
    1.11  imports Real Topological_Spaces
    1.12  begin
    1.13  
    1.14 -subsection {* Locale for additive functions *}
    1.15 +subsection \<open>Locale for additive functions\<close>
    1.16  
    1.17  locale additive =
    1.18    fixes f :: "'a::ab_group_add \<Rightarrow> 'b::ab_group_add"
    1.19 @@ -43,7 +43,7 @@
    1.20  
    1.21  end
    1.22  
    1.23 -subsection {* Vector spaces *}
    1.24 +subsection \<open>Vector spaces\<close>
    1.25  
    1.26  locale vector_space =
    1.27    fixes scale :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b"
    1.28 @@ -131,7 +131,7 @@
    1.29  
    1.30  end
    1.31  
    1.32 -subsection {* Real vector spaces *}
    1.33 +subsection \<open>Real vector spaces\<close>
    1.34  
    1.35  class scaleR =
    1.36    fixes scaleR :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "*\<^sub>R" 75)
    1.37 @@ -159,7 +159,7 @@
    1.38  apply (rule scaleR_one)
    1.39  done
    1.40  
    1.41 -text {* Recover original theorem names *}
    1.42 +text \<open>Recover original theorem names\<close>
    1.43  
    1.44  lemmas scaleR_left_commute = real_vector.scale_left_commute
    1.45  lemmas scaleR_zero_left = real_vector.scale_zero_left
    1.46 @@ -176,7 +176,7 @@
    1.47  lemmas scaleR_cancel_left = real_vector.scale_cancel_left
    1.48  lemmas scaleR_cancel_right = real_vector.scale_cancel_right
    1.49  
    1.50 -text {* Legacy names *}
    1.51 +text \<open>Legacy names\<close>
    1.52  
    1.53  lemmas scaleR_left_distrib = scaleR_add_left
    1.54  lemmas scaleR_right_distrib = scaleR_add_right
    1.55 @@ -229,8 +229,8 @@
    1.56  done
    1.57  
    1.58  
    1.59 -subsection {* Embedding of the Reals into any @{text real_algebra_1}:
    1.60 -@{term of_real} *}
    1.61 +subsection \<open>Embedding of the Reals into any @{text real_algebra_1}:
    1.62 +@{term of_real}\<close>
    1.63  
    1.64  definition
    1.65    of_real :: "real \<Rightarrow> 'a::real_algebra_1" where
    1.66 @@ -303,7 +303,7 @@
    1.67      by (simp add: of_real_def)
    1.68  qed
    1.69  
    1.70 -text{*Collapse nested embeddings*}
    1.71 +text\<open>Collapse nested embeddings\<close>
    1.72  lemma of_real_of_nat_eq [simp]: "of_real (of_nat n) = of_nat n"
    1.73  by (induct n) auto
    1.74  
    1.75 @@ -322,7 +322,7 @@
    1.76  lemma of_real_neg_numeral [simp]: "of_real (- numeral w) = - numeral w"
    1.77  using of_real_of_int_eq [of "- numeral w"] by simp
    1.78  
    1.79 -text{*Every real algebra has characteristic zero*}
    1.80 +text\<open>Every real algebra has characteristic zero\<close>
    1.81  
    1.82  instance real_algebra_1 < ring_char_0
    1.83  proof
    1.84 @@ -333,7 +333,7 @@
    1.85  instance real_field < field_char_0 ..
    1.86  
    1.87  
    1.88 -subsection {* The Set of Real Numbers *}
    1.89 +subsection \<open>The Set of Real Numbers\<close>
    1.90  
    1.91  definition Reals :: "'a::real_algebra_1 set" where
    1.92    "Reals = range of_real"
    1.93 @@ -439,7 +439,7 @@
    1.94    obtains (of_real) r where "q = of_real r"
    1.95    unfolding Reals_def
    1.96  proof -
    1.97 -  from `q \<in> \<real>` have "q \<in> range of_real" unfolding Reals_def .
    1.98 +  from \<open>q \<in> \<real>\<close> have "q \<in> range of_real" unfolding Reals_def .
    1.99    then obtain r where "q = of_real r" ..
   1.100    then show thesis ..
   1.101  qed
   1.102 @@ -468,7 +468,7 @@
   1.103    "q \<in> \<real> \<Longrightarrow> (\<And>r. P (of_real r)) \<Longrightarrow> P q"
   1.104    by (rule Reals_cases) auto
   1.105  
   1.106 -subsection {* Ordered real vector spaces *}
   1.107 +subsection \<open>Ordered real vector spaces\<close>
   1.108  
   1.109  class ordered_real_vector = real_vector + ordered_ab_group_add +
   1.110    assumes scaleR_left_mono: "x \<le> y \<Longrightarrow> 0 \<le> a \<Longrightarrow> a *\<^sub>R x \<le> a *\<^sub>R y"
   1.111 @@ -583,16 +583,16 @@
   1.112        assume "0 < a"
   1.113        with lhs have "inverse a *\<^sub>R 0 \<le> inverse a *\<^sub>R (a *\<^sub>R b)"
   1.114          by (intro scaleR_mono) auto
   1.115 -      hence ?rhs using `0 < a`
   1.116 +      hence ?rhs using \<open>0 < a\<close>
   1.117          by simp
   1.118      } moreover {
   1.119        assume "0 > a"
   1.120        with lhs have "- inverse a *\<^sub>R 0 \<le> - inverse a *\<^sub>R (a *\<^sub>R b)"
   1.121          by (intro scaleR_mono) auto
   1.122 -      hence ?rhs using `0 > a`
   1.123 +      hence ?rhs using \<open>0 > a\<close>
   1.124          by simp
   1.125 -    } ultimately show ?rhs using `a \<noteq> 0` by arith
   1.126 -  qed (auto simp: not_le `a \<noteq> 0` intro!: split_scaleR_pos_le)
   1.127 +    } ultimately show ?rhs using \<open>a \<noteq> 0\<close> by arith
   1.128 +  qed (auto simp: not_le \<open>a \<noteq> 0\<close> intro!: split_scaleR_pos_le)
   1.129  qed simp
   1.130  
   1.131  lemma scaleR_le_0_iff:
   1.132 @@ -622,7 +622,7 @@
   1.133    using scaleR_right_mono[of a 1 x] by simp
   1.134  
   1.135  
   1.136 -subsection {* Real normed vector spaces *}
   1.137 +subsection \<open>Real normed vector spaces\<close>
   1.138  
   1.139  class dist =
   1.140    fixes dist :: "'a \<Rightarrow> 'a \<Rightarrow> real"
   1.141 @@ -862,7 +862,7 @@
   1.142    shows "norm (x ^ n) = norm x ^ n"
   1.143  by (induct n) (simp_all add: norm_mult)
   1.144  
   1.145 -text{*Despite a superficial resemblance, @{text norm_eq_1} is not relevant.*}
   1.146 +text\<open>Despite a superficial resemblance, @{text norm_eq_1} is not relevant.\<close>
   1.147  lemma square_norm_one:
   1.148    fixes x :: "'a::real_normed_div_algebra"
   1.149    assumes "x^2 = 1" shows "norm x = 1"
   1.150 @@ -939,7 +939,7 @@
   1.151    finally show ?thesis .
   1.152  qed
   1.153  
   1.154 -subsection {* Metric spaces *}
   1.155 +subsection \<open>Metric spaces\<close>
   1.156  
   1.157  class metric_space = open_dist +
   1.158    assumes dist_eq_0_iff [simp]: "dist x y = 0 \<longleftrightarrow> x = y"
   1.159 @@ -1065,7 +1065,7 @@
   1.160      by blast
   1.161  qed
   1.162  
   1.163 -text {* Every normed vector space is a metric space. *}
   1.164 +text \<open>Every normed vector space is a metric space.\<close>
   1.165  
   1.166  instance real_normed_vector < metric_space
   1.167  proof
   1.168 @@ -1077,7 +1077,7 @@
   1.169      using norm_triangle_ineq4 [of "x - z" "y - z"] by simp
   1.170  qed
   1.171  
   1.172 -subsection {* Class instances for real numbers *}
   1.173 +subsection \<open>Class instances for real numbers\<close>
   1.174  
   1.175  instantiation real :: real_normed_field
   1.176  begin
   1.177 @@ -1150,24 +1150,24 @@
   1.178  lemmas closed_real_atLeast = closed_atLeast[where 'a=real]
   1.179  lemmas closed_real_atLeastAtMost = closed_atLeastAtMost[where 'a=real]
   1.180  
   1.181 -subsection {* Extra type constraints *}
   1.182 +subsection \<open>Extra type constraints\<close>
   1.183  
   1.184 -text {* Only allow @{term "open"} in class @{text topological_space}. *}
   1.185 +text \<open>Only allow @{term "open"} in class @{text topological_space}.\<close>
   1.186  
   1.187 -setup {* Sign.add_const_constraint
   1.188 -  (@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"}) *}
   1.189 +setup \<open>Sign.add_const_constraint
   1.190 +  (@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"})\<close>
   1.191  
   1.192 -text {* Only allow @{term dist} in class @{text metric_space}. *}
   1.193 +text \<open>Only allow @{term dist} in class @{text metric_space}.\<close>
   1.194  
   1.195 -setup {* Sign.add_const_constraint
   1.196 -  (@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"}) *}
   1.197 +setup \<open>Sign.add_const_constraint
   1.198 +  (@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"})\<close>
   1.199  
   1.200 -text {* Only allow @{term norm} in class @{text real_normed_vector}. *}
   1.201 +text \<open>Only allow @{term norm} in class @{text real_normed_vector}.\<close>
   1.202  
   1.203 -setup {* Sign.add_const_constraint
   1.204 -  (@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"}) *}
   1.205 +setup \<open>Sign.add_const_constraint
   1.206 +  (@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"})\<close>
   1.207  
   1.208 -subsection {* Sign function *}
   1.209 +subsection \<open>Sign function\<close>
   1.210  
   1.211  lemma norm_sgn:
   1.212    "norm (sgn(x::'a::real_normed_vector)) = (if x = 0 then 0 else 1)"
   1.213 @@ -1225,7 +1225,7 @@
   1.214  lemma dist_diff [simp]: "dist a (a - b) = norm b"  "dist (a - b) a = norm b"
   1.215    by (simp_all add: dist_norm)
   1.216    
   1.217 -subsection {* Bounded Linear and Bilinear Operators *}
   1.218 +subsection \<open>Bounded Linear and Bilinear Operators\<close>
   1.219  
   1.220  locale linear = additive f for f :: "'a::real_vector \<Rightarrow> 'b::real_vector" +
   1.221    assumes scaleR: "f (scaleR r x) = scaleR r (f x)"
   1.222 @@ -1492,7 +1492,7 @@
   1.223      by (clarsimp, rule_tac x="x + of_real (e/2)" in exI, simp)
   1.224  qed
   1.225  
   1.226 -subsection {* Filters and Limits on Metric Space *}
   1.227 +subsection \<open>Filters and Limits on Metric Space\<close>
   1.228  
   1.229  lemma (in metric_space) nhds_metric: "nhds x = (INF e:{0 <..}. principal {y. dist y x < e})"
   1.230    unfolding nhds_def
   1.231 @@ -1552,7 +1552,7 @@
   1.232    apply (rule_tac c="nat(ceiling (Z + 1))" in eventually_sequentiallyI)
   1.233    by linarith
   1.234  
   1.235 -subsubsection {* Limits of Sequences *}
   1.236 +subsubsection \<open>Limits of Sequences\<close>
   1.237  
   1.238  lemma lim_sequentially: "X ----> (L::'a::metric_space) \<longleftrightarrow> (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. dist (X n) L < r)"
   1.239    unfolding tendsto_iff eventually_sequentially ..
   1.240 @@ -1571,7 +1571,7 @@
   1.241  by (simp add: lim_sequentially)
   1.242  
   1.243  
   1.244 -subsubsection {* Limits of Functions *}
   1.245 +subsubsection \<open>Limits of Functions\<close>
   1.246  
   1.247  lemma LIM_def: "f -- (a::'a::metric_space) --> (L::'b::metric_space) =
   1.248       (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & dist x a < s
   1.249 @@ -1622,14 +1622,14 @@
   1.250    shows "(\<lambda>x. g (f x)) -- a --> l"
   1.251  by (rule metric_LIM_compose2 [OF f g inj])
   1.252  
   1.253 -subsection {* Complete metric spaces *}
   1.254 +subsection \<open>Complete metric spaces\<close>
   1.255  
   1.256 -subsection {* Cauchy sequences *}
   1.257 +subsection \<open>Cauchy sequences\<close>
   1.258  
   1.259  definition (in metric_space) Cauchy :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
   1.260    "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < e)"
   1.261  
   1.262 -subsection {* Cauchy Sequences *}
   1.263 +subsection \<open>Cauchy Sequences\<close>
   1.264  
   1.265  lemma metric_CauchyI:
   1.266    "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X"
   1.267 @@ -1685,7 +1685,7 @@
   1.268  unfolding convergent_def
   1.269  by (erule exE, erule LIMSEQ_imp_Cauchy)
   1.270  
   1.271 -subsubsection {* Cauchy Sequences are Convergent *}
   1.272 +subsubsection \<open>Cauchy Sequences are Convergent\<close>
   1.273  
   1.274  class complete_space = metric_space +
   1.275    assumes Cauchy_convergent: "Cauchy X \<Longrightarrow> convergent X"
   1.276 @@ -1695,17 +1695,17 @@
   1.277    shows "Cauchy X = convergent X"
   1.278  by (fast intro: Cauchy_convergent convergent_Cauchy)
   1.279  
   1.280 -subsection {* The set of real numbers is a complete metric space *}
   1.281 +subsection \<open>The set of real numbers is a complete metric space\<close>
   1.282  
   1.283 -text {*
   1.284 +text \<open>
   1.285  Proof that Cauchy sequences converge based on the one from
   1.286  @{url "http://pirate.shu.edu/~wachsmut/ira/numseq/proofs/cauconv.html"}
   1.287 -*}
   1.288 +\<close>
   1.289  
   1.290 -text {*
   1.291 +text \<open>
   1.292    If sequence @{term "X"} is Cauchy, then its limit is the lub of
   1.293    @{term "{r::real. \<exists>N. \<forall>n\<ge>N. r < X n}"}
   1.294 -*}
   1.295 +\<close>
   1.296  
   1.297  lemma increasing_LIMSEQ:
   1.298    fixes f :: "nat \<Rightarrow> real"
   1.299 @@ -1717,9 +1717,9 @@
   1.300    fix x assume "x < l"
   1.301    with dense[of 0 "l - x"] obtain e where "0 < e" "e < l - x"
   1.302      by auto
   1.303 -  from en[OF `0 < e`] obtain n where "l - e \<le> f n"
   1.304 +  from en[OF \<open>0 < e\<close>] obtain n where "l - e \<le> f n"
   1.305      by (auto simp: field_simps)
   1.306 -  with `e < l - x` `0 < e` have "x < f n" by simp
   1.307 +  with \<open>e < l - x\<close> \<open>0 < e\<close> have "x < f n" by simp
   1.308    with incseq_SucI[of f, OF inc] show "eventually (\<lambda>n. x < f n) sequentially"
   1.309      by (auto simp: eventually_sequentially incseq_def intro: less_le_trans)
   1.310  qed (insert bdd, auto)