complete_lattice instance for net type
authorhuffman
Sat May 01 11:46:47 2010 -0700 (2010-05-01)
changeset 36630aa1f8acdcc1c
parent 36629 de62713aec6e
child 36631 4c1f119fadb9
complete_lattice instance for net type
src/HOL/Limits.thy
     1.1 --- a/src/HOL/Limits.thy	Sat May 01 09:43:40 2010 -0700
     1.2 +++ b/src/HOL/Limits.thy	Sat May 01 11:46:47 2010 -0700
     1.3 @@ -11,7 +11,7 @@
     1.4  subsection {* Nets *}
     1.5  
     1.6  text {*
     1.7 -  A net is now defined simply as a filter.
     1.8 +  A net is now defined simply as a filter on a set.
     1.9    The definition also allows non-proper filters.
    1.10  *}
    1.11  
    1.12 @@ -53,6 +53,12 @@
    1.13  unfolding eventually_def
    1.14  by (rule is_filter.True [OF is_filter_Rep_net])
    1.15  
    1.16 +lemma always_eventually: "\<forall>x. P x \<Longrightarrow> eventually P net"
    1.17 +proof -
    1.18 +  assume "\<forall>x. P x" hence "P = (\<lambda>x. True)" by (simp add: ext)
    1.19 +  thus "eventually P net" by simp
    1.20 +qed
    1.21 +
    1.22  lemma eventually_mono:
    1.23    "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P net \<Longrightarrow> eventually Q net"
    1.24  unfolding eventually_def
    1.25 @@ -104,7 +110,7 @@
    1.26  text {* @{term "net \<le> net'"} means that @{term net} is finer than
    1.27  @{term net'}. *}
    1.28  
    1.29 -instantiation net :: (type) "{order,bot}"
    1.30 +instantiation net :: (type) complete_lattice
    1.31  begin
    1.32  
    1.33  definition
    1.34 @@ -116,13 +122,65 @@
    1.35      "(net :: 'a net) < net' \<longleftrightarrow> net \<le> net' \<and> \<not> net' \<le> net"
    1.36  
    1.37  definition
    1.38 +  top_net_def [code del]:
    1.39 +    "top = Abs_net (\<lambda>P. \<forall>x. P x)"
    1.40 +
    1.41 +definition
    1.42    bot_net_def [code del]:
    1.43      "bot = Abs_net (\<lambda>P. True)"
    1.44  
    1.45 +definition
    1.46 +  sup_net_def [code del]:
    1.47 +    "sup net net' = Abs_net (\<lambda>P. eventually P net \<and> eventually P net')"
    1.48 +
    1.49 +definition
    1.50 +  inf_net_def [code del]:
    1.51 +    "inf a b = Abs_net
    1.52 +      (\<lambda>P. \<exists>Q R. eventually Q a \<and> eventually R b \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
    1.53 +
    1.54 +definition
    1.55 +  Sup_net_def [code del]:
    1.56 +    "Sup A = Abs_net (\<lambda>P. \<forall>net\<in>A. eventually P net)"
    1.57 +
    1.58 +definition
    1.59 +  Inf_net_def [code del]:
    1.60 +    "Inf A = Sup {x::'a net. \<forall>y\<in>A. x \<le> y}"
    1.61 +
    1.62 +lemma eventually_top [simp]: "eventually P top \<longleftrightarrow> (\<forall>x. P x)"
    1.63 +unfolding top_net_def
    1.64 +by (rule eventually_Abs_net, rule is_filter.intro, auto)
    1.65 +
    1.66  lemma eventually_bot [simp]: "eventually P bot"
    1.67  unfolding bot_net_def
    1.68  by (subst eventually_Abs_net, rule is_filter.intro, auto)
    1.69  
    1.70 +lemma eventually_sup:
    1.71 +  "eventually P (sup net net') \<longleftrightarrow> eventually P net \<and> eventually P net'"
    1.72 +unfolding sup_net_def
    1.73 +by (rule eventually_Abs_net, rule is_filter.intro)
    1.74 +   (auto elim!: eventually_rev_mp)
    1.75 +
    1.76 +lemma eventually_inf:
    1.77 +  "eventually P (inf a b) \<longleftrightarrow>
    1.78 +   (\<exists>Q R. eventually Q a \<and> eventually R b \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
    1.79 +unfolding inf_net_def
    1.80 +apply (rule eventually_Abs_net, rule is_filter.intro)
    1.81 +apply (fast intro: eventually_True)
    1.82 +apply clarify
    1.83 +apply (intro exI conjI)
    1.84 +apply (erule (1) eventually_conj)
    1.85 +apply (erule (1) eventually_conj)
    1.86 +apply simp
    1.87 +apply auto
    1.88 +done
    1.89 +
    1.90 +lemma eventually_Sup:
    1.91 +  "eventually P (Sup A) \<longleftrightarrow> (\<forall>net\<in>A. eventually P net)"
    1.92 +unfolding Sup_net_def
    1.93 +apply (rule eventually_Abs_net, rule is_filter.intro)
    1.94 +apply (auto intro: eventually_conj elim!: eventually_rev_mp)
    1.95 +done
    1.96 +
    1.97  instance proof
    1.98    fix x y :: "'a net" show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
    1.99      by (rule less_net_def)
   1.100 @@ -136,8 +194,36 @@
   1.101    fix x y :: "'a net" assume "x \<le> y" and "y \<le> x" thus "x = y"
   1.102      unfolding le_net_def expand_net_eq by fast
   1.103  next
   1.104 +  fix x :: "'a net" show "x \<le> top"
   1.105 +    unfolding le_net_def eventually_top by (simp add: always_eventually)
   1.106 +next
   1.107    fix x :: "'a net" show "bot \<le> x"
   1.108      unfolding le_net_def by simp
   1.109 +next
   1.110 +  fix x y :: "'a net" show "x \<le> sup x y" and "y \<le> sup x y"
   1.111 +    unfolding le_net_def eventually_sup by simp_all
   1.112 +next
   1.113 +  fix x y z :: "'a net" assume "x \<le> z" and "y \<le> z" thus "sup x y \<le> z"
   1.114 +    unfolding le_net_def eventually_sup by simp
   1.115 +next
   1.116 +  fix x y :: "'a net" show "inf x y \<le> x" and "inf x y \<le> y"
   1.117 +    unfolding le_net_def eventually_inf by (auto intro: eventually_True)
   1.118 +next
   1.119 +  fix x y z :: "'a net" assume "x \<le> y" and "x \<le> z" thus "x \<le> inf y z"
   1.120 +    unfolding le_net_def eventually_inf
   1.121 +    by (auto elim!: eventually_mono intro: eventually_conj)
   1.122 +next
   1.123 +  fix x :: "'a net" and A assume "x \<in> A" thus "x \<le> Sup A"
   1.124 +    unfolding le_net_def eventually_Sup by simp
   1.125 +next
   1.126 +  fix A and y :: "'a net" assume "\<And>x. x \<in> A \<Longrightarrow> x \<le> y" thus "Sup A \<le> y"
   1.127 +    unfolding le_net_def eventually_Sup by simp
   1.128 +next
   1.129 +  fix z :: "'a net" and A assume "z \<in> A" thus "Inf A \<le> z"
   1.130 +    unfolding le_net_def Inf_net_def eventually_Sup Ball_def by simp
   1.131 +next
   1.132 +  fix A and x :: "'a net" assume "\<And>y. y \<in> A \<Longrightarrow> x \<le> y" thus "x \<le> Inf A"
   1.133 +    unfolding le_net_def Inf_net_def eventually_Sup Ball_def by simp
   1.134  qed
   1.135  
   1.136  end