src/HOL/Limits.thy
changeset 37767 a2b7a20d6ea3
parent 36822 38a480e0346f
child 39198 f967a16dfcdd
     1.1 --- a/src/HOL/Limits.thy	Mon Jul 12 08:58:27 2010 +0200
     1.2 +++ b/src/HOL/Limits.thy	Mon Jul 12 10:48:37 2010 +0200
     1.3 @@ -37,9 +37,8 @@
     1.4  
     1.5  subsection {* Eventually *}
     1.6  
     1.7 -definition
     1.8 -  eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a net \<Rightarrow> bool" where
     1.9 -  [code del]: "eventually P net \<longleftrightarrow> Rep_net net P"
    1.10 +definition eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a net \<Rightarrow> bool" where
    1.11 +  "eventually P net \<longleftrightarrow> Rep_net net P"
    1.12  
    1.13  lemma eventually_Abs_net:
    1.14    assumes "is_filter net" shows "eventually P (Abs_net net) = net P"
    1.15 @@ -114,37 +113,29 @@
    1.16  begin
    1.17  
    1.18  definition
    1.19 -  le_net_def [code del]:
    1.20 -    "net \<le> net' \<longleftrightarrow> (\<forall>P. eventually P net' \<longrightarrow> eventually P net)"
    1.21 +  le_net_def: "net \<le> net' \<longleftrightarrow> (\<forall>P. eventually P net' \<longrightarrow> eventually P net)"
    1.22  
    1.23  definition
    1.24 -  less_net_def [code del]:
    1.25 -    "(net :: 'a net) < net' \<longleftrightarrow> net \<le> net' \<and> \<not> net' \<le> net"
    1.26 +  less_net_def: "(net :: 'a net) < net' \<longleftrightarrow> net \<le> net' \<and> \<not> net' \<le> net"
    1.27  
    1.28  definition
    1.29 -  top_net_def [code del]:
    1.30 -    "top = Abs_net (\<lambda>P. \<forall>x. P x)"
    1.31 +  top_net_def: "top = Abs_net (\<lambda>P. \<forall>x. P x)"
    1.32  
    1.33  definition
    1.34 -  bot_net_def [code del]:
    1.35 -    "bot = Abs_net (\<lambda>P. True)"
    1.36 +  bot_net_def: "bot = Abs_net (\<lambda>P. True)"
    1.37  
    1.38  definition
    1.39 -  sup_net_def [code del]:
    1.40 -    "sup net net' = Abs_net (\<lambda>P. eventually P net \<and> eventually P net')"
    1.41 +  sup_net_def: "sup net net' = Abs_net (\<lambda>P. eventually P net \<and> eventually P net')"
    1.42  
    1.43  definition
    1.44 -  inf_net_def [code del]:
    1.45 -    "inf a b = Abs_net
    1.46 +  inf_net_def: "inf a b = Abs_net
    1.47        (\<lambda>P. \<exists>Q R. eventually Q a \<and> eventually R b \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
    1.48  
    1.49  definition
    1.50 -  Sup_net_def [code del]:
    1.51 -    "Sup A = Abs_net (\<lambda>P. \<forall>net\<in>A. eventually P net)"
    1.52 +  Sup_net_def: "Sup A = Abs_net (\<lambda>P. \<forall>net\<in>A. eventually P net)"
    1.53  
    1.54  definition
    1.55 -  Inf_net_def [code del]:
    1.56 -    "Inf A = Sup {x::'a net. \<forall>y\<in>A. x \<le> y}"
    1.57 +  Inf_net_def: "Inf A = Sup {x::'a net. \<forall>y\<in>A. x \<le> y}"
    1.58  
    1.59  lemma eventually_top [simp]: "eventually P top \<longleftrightarrow> (\<forall>x. P x)"
    1.60  unfolding top_net_def
    1.61 @@ -243,9 +234,7 @@
    1.62  
    1.63  subsection {* Map function for nets *}
    1.64  
    1.65 -definition
    1.66 -  netmap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a net \<Rightarrow> 'b net"
    1.67 -where [code del]:
    1.68 +definition netmap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a net \<Rightarrow> 'b net" where
    1.69    "netmap f net = Abs_net (\<lambda>P. eventually (\<lambda>x. P (f x)) net)"
    1.70  
    1.71  lemma eventually_netmap:
    1.72 @@ -271,9 +260,7 @@
    1.73  
    1.74  subsection {* Sequentially *}
    1.75  
    1.76 -definition
    1.77 -  sequentially :: "nat net"
    1.78 -where [code del]:
    1.79 +definition sequentially :: "nat net" where
    1.80    "sequentially = Abs_net (\<lambda>P. \<exists>k. \<forall>n\<ge>k. P n)"
    1.81  
    1.82  lemma eventually_sequentially:
    1.83 @@ -302,19 +289,13 @@
    1.84  
    1.85  subsection {* Standard Nets *}
    1.86  
    1.87 -definition
    1.88 -  within :: "'a net \<Rightarrow> 'a set \<Rightarrow> 'a net" (infixr "within" 70)
    1.89 -where [code del]:
    1.90 +definition within :: "'a net \<Rightarrow> 'a set \<Rightarrow> 'a net" (infixr "within" 70) where
    1.91    "net within S = Abs_net (\<lambda>P. eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) net)"
    1.92  
    1.93 -definition
    1.94 -  nhds :: "'a::topological_space \<Rightarrow> 'a net"
    1.95 -where [code del]:
    1.96 +definition nhds :: "'a::topological_space \<Rightarrow> 'a net" where
    1.97    "nhds a = Abs_net (\<lambda>P. \<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
    1.98  
    1.99 -definition
   1.100 -  at :: "'a::topological_space \<Rightarrow> 'a net"
   1.101 -where [code del]:
   1.102 +definition at :: "'a::topological_space \<Rightarrow> 'a net" where
   1.103    "at a = nhds a within - {a}"
   1.104  
   1.105  lemma eventually_within:
   1.106 @@ -368,9 +349,8 @@
   1.107  
   1.108  subsection {* Boundedness *}
   1.109  
   1.110 -definition
   1.111 -  Bfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a net \<Rightarrow> bool" where
   1.112 -  [code del]: "Bfun f net = (\<exists>K>0. eventually (\<lambda>x. norm (f x) \<le> K) net)"
   1.113 +definition Bfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a net \<Rightarrow> bool" where
   1.114 +  "Bfun f net = (\<exists>K>0. eventually (\<lambda>x. norm (f x) \<le> K) net)"
   1.115  
   1.116  lemma BfunI:
   1.117    assumes K: "eventually (\<lambda>x. norm (f x) \<le> K) net" shows "Bfun f net"
   1.118 @@ -390,9 +370,8 @@
   1.119  
   1.120  subsection {* Convergence to Zero *}
   1.121  
   1.122 -definition
   1.123 -  Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a net \<Rightarrow> bool" where
   1.124 -  [code del]: "Zfun f net = (\<forall>r>0. eventually (\<lambda>x. norm (f x) < r) net)"
   1.125 +definition Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a net \<Rightarrow> bool" where
   1.126 +  "Zfun f net = (\<forall>r>0. eventually (\<lambda>x. norm (f x) < r) net)"
   1.127  
   1.128  lemma ZfunI:
   1.129    "(\<And>r. 0 < r \<Longrightarrow> eventually (\<lambda>x. norm (f x) < r) net) \<Longrightarrow> Zfun f net"
   1.130 @@ -547,10 +526,8 @@
   1.131  
   1.132  subsection {* Limits *}
   1.133  
   1.134 -definition
   1.135 -  tendsto :: "('a \<Rightarrow> 'b::topological_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool"
   1.136 -    (infixr "--->" 55)
   1.137 -where [code del]:
   1.138 +definition tendsto :: "('a \<Rightarrow> 'b::topological_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool"
   1.139 +    (infixr "--->" 55) where
   1.140    "(f ---> l) net \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)"
   1.141  
   1.142  ML {*