author haftmann Fri Mar 16 21:32:08 2007 +0100 (2007-03-16) changeset 22452 8a86fd2a1bf0 parent 22451 989182f660e0 child 22453 530db8c36f53
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
 src/HOL/FixedPoint.thy file | annotate | diff | revisions src/HOL/Hyperreal/StarClasses.thy file | annotate | diff | revisions src/HOL/Library/Continuity.thy file | annotate | diff | revisions src/HOL/Library/Graphs.thy file | annotate | diff | revisions src/HOL/Matrix/Matrix.thy file | annotate | diff | revisions src/HOL/Matrix/SparseMatrix.thy file | annotate | diff | revisions src/HOL/OrderedGroup.thy file | annotate | diff | revisions src/HOL/Ring_and_Field.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/FixedPoint.thy	Fri Mar 16 21:32:07 2007 +0100
1.2 +++ b/src/HOL/FixedPoint.thy	Fri Mar 16 21:32:08 2007 +0100
1.3 @@ -5,37 +5,35 @@
1.4      Copyright   1992  University of Cambridge
1.5  *)
1.6
1.7 -header{* Fixed Points and the Knaster-Tarski Theorem*}
1.8 +header {* Fixed Points and the Knaster-Tarski Theorem*}
1.9
1.10  theory FixedPoint
1.11 -imports Product_Type LOrder
1.12 +imports Product_Type
1.13  begin
1.14
1.15  subsection {* Complete lattices *}
1.16
1.17 -consts
1.18 -  Inf :: "'a::order set \<Rightarrow> 'a"
1.19 -
1.20 -definition
1.21 -  Sup :: "'a::order set \<Rightarrow> 'a" where
1.22 -  "Sup A = Inf {b. \<forall>a \<in> A. a \<le> b}"
1.23 -
1.24 -class comp_lat = order +
1.25 +class complete_lattice = lattice +
1.26 +  fixes Inf :: "'a set \<Rightarrow> 'a"
1.27    assumes Inf_lower: "x \<in> A \<Longrightarrow> Inf A \<sqsubseteq> x"
1.28    assumes Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> Inf A"
1.29
1.30 -theorem Sup_upper: "(x::'a::comp_lat) \<in> A \<Longrightarrow> x <= Sup A"
1.31 +definition
1.32 +  Sup :: "'a\<Colon>complete_lattice set \<Rightarrow> 'a" where
1.33 +  "Sup A = Inf {b. \<forall>a \<in> A. a \<le> b}"
1.34 +
1.35 +theorem Sup_upper: "(x::'a::complete_lattice) \<in> A \<Longrightarrow> x <= Sup A"
1.36    by (auto simp: Sup_def intro: Inf_greatest)
1.37
1.38 -theorem Sup_least: "(\<And>x::'a::comp_lat. x \<in> A \<Longrightarrow> x <= z) \<Longrightarrow> Sup A <= z"
1.39 +theorem Sup_least: "(\<And>x::'a::complete_lattice. x \<in> A \<Longrightarrow> x <= z) \<Longrightarrow> Sup A <= z"
1.40    by (auto simp: Sup_def intro: Inf_lower)
1.41
1.42  definition
1.43 -  SUPR :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::comp_lat) \<Rightarrow> 'b" where
1.44 +  SUPR :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::complete_lattice) \<Rightarrow> 'b" where
1.45    "SUPR A f == Sup (f ` A)"
1.46
1.47  definition
1.48 -  INFI :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::comp_lat) \<Rightarrow> 'b" where
1.49 +  INFI :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::complete_lattice) \<Rightarrow> 'b" where
1.50    "INFI A f == Inf (f ` A)"
1.51
1.52  syntax
1.53 @@ -80,17 +78,6 @@
1.54
1.55  text {* A complete lattice is a lattice *}
1.56
1.57 -lemma is_meet_Inf: "is_meet (\<lambda>(x::'a::comp_lat) y. Inf {x, y})"
1.58 -  by (auto simp: is_meet_def intro: Inf_lower Inf_greatest)
1.59 -
1.60 -lemma is_join_Sup: "is_join (\<lambda>(x::'a::comp_lat) y. Sup {x, y})"
1.61 -  by (auto simp: is_join_def intro: Sup_upper Sup_least)
1.62 -
1.63 -instance comp_lat < lorder
1.64 -proof
1.65 -  from is_meet_Inf show "\<exists>m::'a\<Rightarrow>'a\<Rightarrow>'a. is_meet m" by iprover
1.66 -  from is_join_Sup show "\<exists>j::'a\<Rightarrow>'a\<Rightarrow>'a. is_join j" by iprover
1.67 -qed
1.68
1.69  subsubsection {* Properties *}
1.70
1.71 @@ -100,7 +87,7 @@
1.72  lemma mono_sup: "mono f \<Longrightarrow> sup (f A) (f B) <= f (sup A B)"
1.73    by (auto simp add: mono_def)
1.74
1.75 -lemma Sup_insert[simp]: "Sup (insert (a::'a::comp_lat) A) = sup a (Sup A)"
1.76 +lemma Sup_insert[simp]: "Sup (insert (a::'a::complete_lattice) A) = sup a (Sup A)"
1.77    apply (rule order_antisym)
1.78    apply (rule Sup_least)
1.79    apply (erule insertE)
1.80 @@ -116,7 +103,7 @@
1.81    apply simp
1.82    done
1.83
1.84 -lemma Inf_insert[simp]: "Inf (insert (a::'a::comp_lat) A) = inf a (Inf A)"
1.85 +lemma Inf_insert[simp]: "Inf (insert (a::'a::complete_lattice) A) = inf a (Inf A)"
1.86    apply (rule order_antisym)
1.87    apply (rule le_infI)
1.88    apply (rule Inf_lower)
1.89 @@ -132,10 +119,10 @@
1.90    apply (erule Inf_lower)
1.91    done
1.92
1.93 -lemma bot_least[simp]: "Sup{} \<le> (x::'a::comp_lat)"
1.94 +lemma bot_least[simp]: "Sup{} \<le> (x::'a::complete_lattice)"
1.95    by (rule Sup_least) simp
1.96
1.97 -lemma top_greatest[simp]: "(x::'a::comp_lat) \<le> Inf{}"
1.98 +lemma top_greatest[simp]: "(x::'a::complete_lattice) \<le> Inf{}"
1.99    by (rule Inf_greatest) simp
1.100
1.101  lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M"
1.102 @@ -149,51 +136,15 @@
1.103
1.104  subsubsection {* Booleans *}
1.105
1.106 -defs
1.107 -  Inf_bool_def: "Inf A == ALL x:A. x"
1.108 -
1.109 -instance bool :: comp_lat
1.110 +instance bool :: complete_lattice
1.111 +  Inf_bool_def: "Inf A \<equiv> \<forall>x\<in>A. x"
1.112    apply intro_classes
1.113    apply (unfold Inf_bool_def)
1.114    apply (iprover intro!: le_boolI elim: ballE)
1.115    apply (iprover intro!: ballI le_boolI elim: ballE le_boolE)
1.116    done
1.117
1.118 -theorem inf_bool_eq: "inf P Q \<longleftrightarrow> P \<and> Q"
1.119 -  apply (rule order_antisym)
1.120 -  apply (rule le_boolI)
1.121 -  apply (rule conjI)
1.122 -  apply (rule le_boolE)
1.123 -  apply (rule inf_le1)
1.124 -  apply assumption+
1.125 -  apply (rule le_boolE)
1.126 -  apply (rule inf_le2)
1.127 -  apply assumption+
1.128 -  apply (rule le_infI)
1.129 -  apply (rule le_boolI)
1.130 -  apply (erule conjunct1)
1.131 -  apply (rule le_boolI)
1.132 -  apply (erule conjunct2)
1.133 -  done
1.134 -
1.135 -theorem sup_bool_eq: "sup P Q \<longleftrightarrow> P \<or> Q"
1.136 -  apply (rule order_antisym)
1.137 -  apply (rule le_supI)
1.138 -  apply (rule le_boolI)
1.139 -  apply (erule disjI1)
1.140 -  apply (rule le_boolI)
1.141 -  apply (erule disjI2)
1.142 -  apply (rule le_boolI)
1.143 -  apply (erule disjE)
1.144 -  apply (rule le_boolE)
1.145 -  apply (rule sup_ge1)
1.146 -  apply assumption+
1.147 -  apply (rule le_boolE)
1.148 -  apply (rule sup_ge2)
1.149 -  apply assumption+
1.150 -  done
1.151 -
1.152 -theorem Sup_bool_eq: "Sup A \<longleftrightarrow> (\<exists>x \<in> A. x)"
1.153 +theorem Sup_bool_eq: "Sup A \<longleftrightarrow> (\<exists>x\<in>A. x)"
1.154    apply (rule order_antisym)
1.155    apply (rule Sup_least)
1.156    apply (rule le_boolI)
1.157 @@ -208,51 +159,8 @@
1.158
1.159  subsubsection {* Functions *}
1.160
1.161 -text {*
1.162 -  Handy introduction and elimination rules for @{text "\<le>"}
1.163 -  on unary and binary predicates
1.164 -*}
1.165 -
1.166 -lemma predicate1I [Pure.intro!, intro!]:
1.167 -  assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
1.168 -  shows "P \<le> Q"
1.169 -  apply (rule le_funI)
1.170 -  apply (rule le_boolI)
1.171 -  apply (rule PQ)
1.172 -  apply assumption
1.173 -  done
1.174 -
1.175 -lemma predicate1D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
1.176 -  apply (erule le_funE)
1.177 -  apply (erule le_boolE)
1.178 -  apply assumption+
1.179 -  done
1.180 -
1.181 -lemma predicate2I [Pure.intro!, intro!]:
1.182 -  assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y"
1.183 -  shows "P \<le> Q"
1.184 -  apply (rule le_funI)+
1.185 -  apply (rule le_boolI)
1.186 -  apply (rule PQ)
1.187 -  apply assumption
1.188 -  done
1.189 -
1.190 -lemma predicate2D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
1.191 -  apply (erule le_funE)+
1.192 -  apply (erule le_boolE)
1.193 -  apply assumption+
1.194 -  done
1.195 -
1.196 -lemma rev_predicate1D: "P x ==> P <= Q ==> Q x"
1.197 -  by (rule predicate1D)
1.198 -
1.199 -lemma rev_predicate2D: "P x y ==> P <= Q ==> Q x y"
1.200 -  by (rule predicate2D)
1.201 -
1.202 -defs
1.203 -  Inf_fun_def: "Inf A == (\<lambda>x. Inf {y. EX f:A. y = f x})"
1.204 -
1.205 -instance "fun" :: (type, comp_lat) comp_lat
1.206 +instance "fun" :: (type, complete_lattice) complete_lattice
1.207 +  Inf_fun_def: "Inf A \<equiv> (\<lambda>x. Inf {y. \<exists>f\<in>A. y = f x})"
1.208    apply intro_classes
1.209    apply (unfold Inf_fun_def)
1.210    apply (rule le_funI)
1.211 @@ -268,33 +176,7 @@
1.212    apply (iprover elim: le_funE)
1.213    done
1.214
1.215 -theorem inf_fun_eq: "inf f g = (\<lambda>x. inf (f x) (g x))"
1.216 -  apply (rule order_antisym)
1.217 -  apply (rule le_funI)
1.218 -  apply (rule le_infI)
1.219 -  apply (rule le_funD [OF inf_le1])
1.220 -  apply (rule le_funD [OF inf_le2])
1.221 -  apply (rule le_infI)
1.222 -  apply (rule le_funI)
1.223 -  apply (rule inf_le1)
1.224 -  apply (rule le_funI)
1.225 -  apply (rule inf_le2)
1.226 -  done
1.227 -
1.228 -theorem sup_fun_eq: "sup f g = (\<lambda>x. sup (f x) (g x))"
1.229 -  apply (rule order_antisym)
1.230 -  apply (rule le_supI)
1.231 -  apply (rule le_funI)
1.232 -  apply (rule sup_ge1)
1.233 -  apply (rule le_funI)
1.234 -  apply (rule sup_ge2)
1.235 -  apply (rule le_funI)
1.236 -  apply (rule le_supI)
1.237 -  apply (rule le_funD [OF sup_ge1])
1.238 -  apply (rule le_funD [OF sup_ge2])
1.239 -  done
1.240 -
1.241 -theorem Sup_fun_eq: "Sup A = (\<lambda>x. Sup {y::'a::comp_lat. EX f:A. y = f x})"
1.242 +theorem Sup_fun_eq: "Sup A = (\<lambda>x. Sup {y. \<exists>f\<in>A. y = f x})"
1.243    apply (rule order_antisym)
1.244    apply (rule Sup_least)
1.245    apply (rule le_funI)
1.246 @@ -308,34 +190,13 @@
1.247    apply simp
1.248    done
1.249
1.250 +
1.251  subsubsection {* Sets *}
1.252
1.253 -defs
1.254 -  Inf_set_def: "Inf S == \<Inter>S"
1.255 -
1.256 -instance set :: (type) comp_lat
1.257 +instance set :: (type) complete_lattice
1.258 +  Inf_set_def: "Inf S \<equiv> \<Inter>S"
1.259    by intro_classes (auto simp add: Inf_set_def)
1.260
1.261 -theorem inf_set_eq: "inf A B = A \<inter> B"
1.262 -  apply (rule subset_antisym)
1.263 -  apply (rule Int_greatest)
1.264 -  apply (rule inf_le1)
1.265 -  apply (rule inf_le2)
1.266 -  apply (rule le_infI)
1.267 -  apply (rule Int_lower1)
1.268 -  apply (rule Int_lower2)
1.269 -  done
1.270 -
1.271 -theorem sup_set_eq: "sup A B = A \<union> B"
1.272 -  apply (rule subset_antisym)
1.273 -  apply (rule le_supI)
1.274 -  apply (rule Un_upper1)
1.275 -  apply (rule Un_upper2)
1.276 -  apply (rule Un_least)
1.277 -  apply (rule sup_ge1)
1.278 -  apply (rule sup_ge2)
1.279 -  done
1.280 -
1.281  theorem Sup_set_eq: "Sup S = \<Union>S"
1.282    apply (rule subset_antisym)
1.283    apply (rule Sup_least)
1.284 @@ -348,11 +209,11 @@
1.285  subsection {* Least and greatest fixed points *}
1.286
1.287  definition
1.288 -  lfp :: "('a\<Colon>comp_lat \<Rightarrow> 'a) \<Rightarrow> 'a" where
1.289 +  lfp :: "('a\<Colon>complete_lattice \<Rightarrow> 'a) \<Rightarrow> 'a" where
1.290    "lfp f = Inf {u. f u \<le> u}"    --{*least fixed point*}
1.291
1.292  definition
1.293 -  gfp :: "('a\<Colon>comp_lat \<Rightarrow> 'a) \<Rightarrow> 'a" where
1.294 +  gfp :: "('a\<Colon>complete_lattice \<Rightarrow> 'a) \<Rightarrow> 'a" where
1.295    "gfp f = Sup {u. u \<le> f u}"    --{*greatest fixed point*}
1.296
1.297
1.298 @@ -403,10 +264,8 @@
1.299    by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp])
1.300      (auto simp: inf_set_eq intro: indhyp)
1.301
1.302 -
1.303 -text{*Version of induction for binary relations*}
1.304 -lemmas lfp_induct2 =  lfp_induct_set [of "(a,b)", split_format (complete)]
1.305 -
1.306 +text {* Version of induction for binary relations *}
1.307 +lemmas lfp_induct2 =  lfp_induct_set [of "(a, b)", split_format (complete)]
1.308
1.309  lemma lfp_ordinal_induct:
1.310    assumes mono: "mono f"
1.311 @@ -563,8 +422,6 @@
1.312  lemma gfp_mono: "(!!Z. f Z \<le> g Z) ==> gfp f \<le> gfp g"
1.313    by (rule gfp_upperbound [THEN gfp_least], blast intro: order_trans)
1.314
1.315 -
1.316 -
1.317  ML
1.318  {*
1.319  val lfp_def = thm "lfp_def";
```
```     2.1 --- a/src/HOL/Hyperreal/StarClasses.thy	Fri Mar 16 21:32:07 2007 +0100
2.2 +++ b/src/HOL/Hyperreal/StarClasses.thy	Fri Mar 16 21:32:08 2007 +0100
2.3 @@ -11,10 +11,6 @@
2.4
2.5  subsection {* Syntactic classes *}
2.6
2.7 -instance star :: (ord) ord
2.8 -  star_le_def:      "(op \<le>) \<equiv> *p2* (op \<le>)"
2.9 -  star_less_def:    "(op <) \<equiv> *p2* (op <)" ..
2.10 -
2.11  instance star :: (zero) zero
2.12    star_zero_def:    "0 \<equiv> star_of 0" ..
2.13
2.14 @@ -24,7 +20,6 @@
2.15  instance star :: (plus) plus
2.16    star_add_def:     "(op +) \<equiv> *f2* (op +)" ..
2.17
2.18 -
2.19  instance star :: (times) times
2.20    star_mult_def:    "(op *) \<equiv> *f2* (op *)" ..
2.21
2.22 @@ -47,6 +42,10 @@
2.23  instance star :: (power) power
2.24    star_power_def:   "(op ^) \<equiv> \<lambda>x n. ( *f* (\<lambda>x. x ^ n)) x" ..
2.25
2.26 +instance star :: (ord) ord
2.27 +  star_le_def:      "(op \<le>) \<equiv> *p2* (op \<le>)"
2.28 +  star_less_def:    "(op <) \<equiv> *p2* (op <)" ..
2.29 +
2.30  lemmas star_class_defs [transfer_unfold] =
2.31    star_zero_def     star_one_def      star_number_def
2.33 @@ -206,7 +205,7 @@
2.34    star_of_number_less star_of_number_le star_of_number_eq
2.35    star_of_less_number star_of_le_number star_of_eq_number
2.36
2.37 -subsection {* Ordering classes *}
2.38 +subsection {* Ordering and lattice classes *}
2.39
2.40  instance star :: (order) order
2.41  apply (intro_classes)
2.42 @@ -216,6 +215,33 @@
2.43  apply (transfer, erule (1) order_antisym)
2.44  done
2.45
2.46 +instance star :: (lower_semilattice) lower_semilattice
2.47 +  star_inf_def [transfer_unfold]: "inf \<equiv> *f2* inf"
2.48 +  by default (transfer star_inf_def, auto)+
2.49 +
2.50 +instance star :: (upper_semilattice) upper_semilattice
2.51 +  star_sup_def [transfer_unfold]: "sup \<equiv> *f2* sup"
2.52 +  by default (transfer star_sup_def, auto)+
2.53 +
2.54 +instance star :: (lattice) lattice ..
2.55 +
2.56 +instance star :: (distrib_lattice) distrib_lattice
2.57 +  by default (transfer, auto simp add: sup_inf_distrib1)
2.58 +
2.59 +lemma Standard_inf [simp]:
2.60 +  "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> inf x y \<in> Standard"
2.62 +
2.63 +lemma Standard_sup [simp]:
2.64 +  "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> sup x y \<in> Standard"
2.66 +
2.67 +lemma star_of_inf [simp]: "star_of (inf x y) = inf (star_of x) (star_of y)"
2.68 +by transfer (rule refl)
2.69 +
2.70 +lemma star_of_sup [simp]: "star_of (sup x y) = sup (star_of x) (star_of y)"
2.71 +by transfer (rule refl)
2.72 +
2.73  instance star :: (linorder) linorder
2.74  by (intro_classes, transfer, rule linorder_linear)
2.75
2.76 @@ -245,63 +271,6 @@
2.77  lemma star_of_min [simp]: "star_of (min x y) = min (star_of x) (star_of y)"
2.78  by transfer (rule refl)
2.79
2.80 -subsection {* Lattice ordering classes *}
2.81 -
2.82 -text {*
2.83 -  Some extra trouble is necessary because the class axioms
2.84 -  for @{term inf} and @{term sup} use quantification over
2.85 -  function spaces.
2.86 -*}
2.87 -
2.88 -lemma ex_star_fun:
2.89 -  "\<exists>f::('a \<Rightarrow> 'b) star. P (\<lambda>x. f \<star> x)
2.90 -   \<Longrightarrow> \<exists>f::'a star \<Rightarrow> 'b star. P f"
2.91 -by (erule exE, erule exI)
2.92 -
2.93 -lemma ex_star_fun2:
2.94 -  "\<exists>f::('a \<Rightarrow> 'b \<Rightarrow> 'c) star. P (\<lambda>x y. f \<star> x \<star> y)
2.95 -   \<Longrightarrow> \<exists>f::'a star \<Rightarrow> 'b star \<Rightarrow> 'c star. P f"
2.96 -by (erule exE, erule exI)
2.97 -
2.98 -instance star :: (join_semilorder) join_semilorder
2.99 -apply (intro_classes)
2.100 -apply (rule ex_star_fun2)
2.101 -apply (transfer is_join_def)
2.102 -apply (rule join_exists)
2.103 -done
2.104 -
2.105 -instance star :: (meet_semilorder) meet_semilorder
2.106 -apply (intro_classes)
2.107 -apply (rule ex_star_fun2)
2.108 -apply (transfer is_meet_def)
2.109 -apply (rule meet_exists)
2.110 -done
2.111 -
2.112 -instance star :: (lorder) lorder ..
2.113 -
2.114 -lemma star_inf_def [transfer_unfold]: "inf = *f2* inf"
2.115 -apply (rule is_meet_unique [OF is_meet_meet])
2.116 -apply (transfer is_meet_def, rule is_meet_meet)
2.117 -done
2.118 -
2.119 -lemma star_sup_def [transfer_unfold]: "sup = *f2* sup"
2.120 -apply (rule is_join_unique [OF is_join_join])
2.121 -apply (transfer is_join_def, rule is_join_join)
2.122 -done
2.123 -
2.124 -lemma Standard_inf [simp]:
2.125 -  "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> inf x y \<in> Standard"
2.127 -
2.128 -lemma Standard_sup [simp]:
2.129 -  "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> sup x y \<in> Standard"
2.131 -
2.132 -lemma star_of_inf [simp]: "star_of (inf x y) = inf (star_of x) (star_of y)"
2.133 -by transfer (rule refl)
2.134 -
2.135 -lemma star_of_sup [simp]: "star_of (sup x y) = sup (star_of x) (star_of y)"
2.136 -by transfer (rule refl)
2.137
2.138  subsection {* Ordered group classes *}
2.139
```
```     3.1 --- a/src/HOL/Library/Continuity.thy	Fri Mar 16 21:32:07 2007 +0100
3.2 +++ b/src/HOL/Library/Continuity.thy	Fri Mar 16 21:32:08 2007 +0100
3.3 @@ -12,15 +12,15 @@
3.4  subsection {* Continuity for complete lattices *}
3.5
3.6  definition
3.7 -  chain :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
3.8 +  chain :: "(nat \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
3.9    "chain M \<longleftrightarrow> (\<forall>i. M i \<le> M (Suc i))"
3.10
3.11  definition
3.12 -  continuous :: "('a::comp_lat \<Rightarrow> 'a::comp_lat) \<Rightarrow> bool" where
3.13 +  continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
3.14    "continuous F \<longleftrightarrow> (\<forall>M. chain M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
3.15
3.16  abbreviation
3.17 -  bot :: "'a::order" where
3.18 +  bot :: "'a::complete_lattice" where
3.19    "bot \<equiv> Sup {}"
3.20
3.21  lemma SUP_nat_conv:
3.22 @@ -34,7 +34,7 @@
3.23  apply (blast intro:SUP_leI le_SUPI)
3.24  done
3.25
3.26 -lemma continuous_mono: fixes F :: "'a::comp_lat \<Rightarrow> 'a::comp_lat"
3.27 +lemma continuous_mono: fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
3.28    assumes "continuous F" shows "mono F"
3.29  proof
3.30    fix A B :: "'a" assume "A <= B"
```
```     4.1 --- a/src/HOL/Library/Graphs.thy	Fri Mar 16 21:32:07 2007 +0100
4.2 +++ b/src/HOL/Library/Graphs.thy	Fri Mar 16 21:32:08 2007 +0100
4.3 @@ -20,6 +20,19 @@
4.4    "Graph (dest_graph G) = G"
4.5    by (cases G) simp
4.6
4.7 +lemma split_graph_all:
4.8 +  "(\<And>gr. PROP P gr) \<equiv> (\<And>set. PROP P (Graph set))"
4.9 +proof
4.10 +  fix set
4.11 +  assume "\<And>gr. PROP P gr"
4.12 +  then show "PROP P (Graph set)" .
4.13 +next
4.14 +  fix gr
4.15 +  assume "\<And>set. PROP P (Graph set)"
4.16 +  then have "PROP P (Graph (dest_graph gr))" .
4.17 +  then show "PROP P gr" by simp
4.18 +qed
4.19 +
4.20  definition
4.21    has_edge :: "('n,'e) graph \<Rightarrow> 'n \<Rightarrow> 'e \<Rightarrow> 'n \<Rightarrow> bool"
4.22  ("_ \<turnstile> _ \<leadsto>\<^bsup>_\<^esup> _")
4.23 @@ -132,11 +145,9 @@
4.24
4.25  subsection {* Order on Graphs *}
4.26
4.27 -instance graph :: (type, type) ord
4.28 -  graph_leq_def: "G \<le> H == dest_graph G \<subseteq> dest_graph H"
4.29 -  graph_less_def: "G < H == dest_graph G \<subset> dest_graph H" ..
4.30 -
4.31  instance graph :: (type, type) order
4.32 +  graph_leq_def: "G \<le> H \<equiv> dest_graph G \<subseteq> dest_graph H"
4.33 +  graph_less_def: "G < H \<equiv> dest_graph G \<subset> dest_graph H"
4.34  proof
4.35    fix x y z :: "('a,'b) graph"
4.36
4.37 @@ -153,27 +164,14 @@
4.38      by (cases x, cases y) auto
4.39  qed
4.40
4.41 -
4.43 -  Inf_graph_def: "Inf == \<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs))"
4.44 -
4.45 -instance graph :: (type, type) comp_lat
4.46 -  by default (auto simp: Inf_graph_def is_join_def graph_leq_def le_fun_def le_bool_def in_grplus has_edge_def)
4.47 +instance graph :: (type, type) distrib_lattice
4.48 +  "inf G H \<equiv> Graph (dest_graph G \<inter> dest_graph H)"
4.49 +  "sup G H \<equiv> G + H"
4.50 +  by default (auto simp add: split_graph_all graph_plus_def inf_graph_def sup_graph_def graph_leq_def graph_less_def)
4.51
4.52 -lemma plus_graph_is_join: "is_join ((op +)::('a::type, 'b::monoid_mult) graph \<Rightarrow> ('a,'b) graph \<Rightarrow> ('a,'b) graph)"
4.53 -  unfolding is_join_def
4.54 -proof (intro allI conjI impI)
4.55 -  fix a b x :: "('a, 'b) graph"
4.56 -
4.57 -  show "a \<le> a + b" "b \<le> a + b" "a \<le> x \<and> b \<le> x \<Longrightarrow> a + b \<le> x"
4.58 -    unfolding graph_leq_def graph_plus_def
4.59 -    by (cases a, cases b) auto
4.60 -qed
4.61 -
4.62 -lemma plus_is_join:
4.63 -  "(op +) =
4.64 -  (sup :: ('a::type, 'b::monoid_mult) graph \<Rightarrow> ('a,'b) graph \<Rightarrow> ('a,'b) graph)"
4.65 -  using plus_graph_is_join by (simp add:join_unique)
4.66 +instance graph :: (type, type) complete_lattice
4.67 +  Inf_graph_def: "Inf == \<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs))"
4.68 +  by default (auto simp: Inf_graph_def graph_leq_def le_fun_def le_bool_def in_grplus has_edge_def)
4.69
4.70  instance graph :: (type, monoid_mult) semiring_1
4.71  proof
4.72 @@ -199,11 +197,10 @@
4.73      by simp
4.74  qed
4.75
4.76 -
4.77  instance graph :: (type, monoid_mult) idem_add
4.78  proof
4.79    fix a :: "('a, 'b) graph"
4.80 -  show "a + a = a" unfolding plus_is_join by simp
4.81 +  show "a + a = a" unfolding graph_plus_def by simp
4.82  qed
4.83
4.84
4.85 @@ -270,7 +267,7 @@
4.86    unfolding Sup_graph_eq2 has_edge_leq graph_leq_def
4.87    by simp
4.88
4.89 -instance graph :: (type, monoid_mult) kleene_by_comp_lat
4.90 +instance graph :: (type, monoid_mult) kleene_by_complete_lattice
4.91  proof
4.92    fix a b c :: "('a, 'b) graph"
4.93
```
```     5.1 --- a/src/HOL/Matrix/Matrix.thy	Fri Mar 16 21:32:07 2007 +0100
5.2 +++ b/src/HOL/Matrix/Matrix.thy	Fri Mar 16 21:32:08 2007 +0100
5.3 @@ -7,6 +7,11 @@
5.4  imports MatrixGeneral
5.5  begin
5.6
5.7 +instance matrix :: ("{zero, lattice}") lattice
5.8 +  "inf \<equiv> combine_matrix inf"
5.9 +  "sup \<equiv> combine_matrix sup"
5.10 +  by default (auto simp add: inf_le1 inf_le2 le_infI le_matrix_def inf_matrix_def sup_matrix_def)
5.11 +
5.12  instance matrix :: ("{plus, zero}") plus
5.13    plus_matrix_def: "A + B \<equiv> combine_matrix (op +) A B" ..
5.14
5.15 @@ -17,13 +22,8 @@
5.16  instance matrix :: ("{plus, times, zero}") times
5.17    times_matrix_def: "A * B \<equiv> mult_matrix (op *) (op +) A B" ..
5.18
5.19 -lemma is_meet_combine_matrix_meet: "is_meet (combine_matrix inf)"
5.20 -  by (simp_all add: is_meet_def le_matrix_def inf_le1 inf_le2 le_infI)
5.21 -
5.22 -lemma is_join_combine_matrix_join: "is_join (combine_matrix sup)"
5.23 -  by (simp_all add: is_join_def le_matrix_def sup_ge1 sup_ge2 le_supI)
5.24 -
5.25  instance matrix :: (lordered_ab_group) lordered_ab_group_meet
5.26 +  abs_matrix_def: "abs (A::('a::lordered_ab_group) matrix) == sup A (- A)"
5.27  proof
5.28    fix A B C :: "('a::lordered_ab_group) matrix"
5.29    show "A + B + C = A + (B + C)"
5.30 @@ -45,8 +45,6 @@
5.31      by (simp add: plus_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)
5.32    show "A - B = A + - B"
5.33      by (simp add: plus_matrix_def diff_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)
5.34 -  show "\<exists>m\<Colon>'a matrix \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix. is_meet m"
5.35 -    by (auto intro: is_meet_combine_matrix_meet)
5.36    assume "A <= B"
5.37    then show "C + A <= C + B"
5.39 @@ -55,9 +53,6 @@
5.40      done
5.41  qed
5.42
5.44 -  abs_matrix_def: "abs (A::('a::lordered_ab_group) matrix) == sup A (- A)"
5.45 -
5.46  instance matrix :: (lordered_ring) lordered_ring
5.47  proof
5.48    fix A B C :: "('a :: lordered_ring) matrix"
5.49 @@ -90,7 +85,7 @@
5.50      apply (rule le_right_mult)
5.52      done
5.53 -qed
5.54 +qed
5.55
5.56  lemma Rep_matrix_add[simp]: "Rep_matrix ((a::('a::lordered_ab_group)matrix)+b) j i  = (Rep_matrix a j i) + (Rep_matrix b j i)"
5.58 @@ -286,17 +281,7 @@
5.59  lemma Rep_minus[simp]: "Rep_matrix (-(A::_::lordered_ab_group)) x y = - (Rep_matrix A x y)"
5.61
5.62 -lemma join_matrix: "sup (A::('a::lordered_ring) matrix) B = combine_matrix sup A B"
5.63 -  apply (insert join_unique[of "(combine_matrix sup)::('a matrix \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix)", simplified is_join_combine_matrix_join])
5.64 -  apply (simp)
5.65 -  done
5.66 -
5.67 -lemma meet_matrix: "inf (A::('a::lordered_ring) matrix) B = combine_matrix inf A B"
5.68 -  apply (insert meet_unique[of "(combine_matrix inf)::('a matrix \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix)", simplified is_meet_combine_matrix_meet])
5.69 -  apply (simp)
5.70 -  done
5.71 -
5.72  lemma Rep_abs[simp]: "Rep_matrix (abs (A::_::lordered_ring)) x y = abs (Rep_matrix A x y)"
5.73 -  by (simp add: abs_lattice join_matrix)
5.74 +  by (simp add: abs_lattice sup_matrix_def)
5.75
5.76  end
```
```     6.1 --- a/src/HOL/Matrix/SparseMatrix.thy	Fri Mar 16 21:32:07 2007 +0100
6.2 +++ b/src/HOL/Matrix/SparseMatrix.thy	Fri Mar 16 21:32:08 2007 +0100
6.3 @@ -922,7 +922,7 @@
6.4
6.5
6.6  lemma pprt_add: "disj_matrices A (B::(_::lordered_ring) matrix) \<Longrightarrow> pprt (A+B) = pprt A + pprt B"
6.7 -  apply (simp add: pprt_def join_matrix)
6.8 +  apply (simp add: pprt_def sup_matrix_def)
6.10    apply (rule ext)+
6.11    apply simp
6.12 @@ -931,7 +931,7 @@
6.13    done
6.14
6.15  lemma nprt_add: "disj_matrices A (B::(_::lordered_ring) matrix) \<Longrightarrow> nprt (A+B) = nprt A + nprt B"
6.16 -  apply (simp add: nprt_def meet_matrix)
6.17 +  apply (simp add: nprt_def inf_matrix_def)
6.19    apply (rule ext)+
6.20    apply simp
6.21 @@ -940,14 +940,14 @@
6.22    done
6.23
6.24  lemma pprt_singleton[simp]: "pprt (singleton_matrix j i (x::_::lordered_ring)) = singleton_matrix j i (pprt x)"
6.25 -  apply (simp add: pprt_def join_matrix)
6.26 +  apply (simp add: pprt_def sup_matrix_def)
6.28    apply (rule ext)+
6.29    apply simp
6.30    done
6.31
6.32  lemma nprt_singleton[simp]: "nprt (singleton_matrix j i (x::_::lordered_ring)) = singleton_matrix j i (nprt x)"
6.33 -  apply (simp add: nprt_def meet_matrix)
6.34 +  apply (simp add: nprt_def inf_matrix_def)
6.36    apply (rule ext)+
6.37    apply simp
6.38 @@ -978,7 +978,7 @@
6.39
6.40  lemma pprt_move_matrix: "pprt (move_matrix (A::('a::lordered_ring) matrix) j i) = move_matrix (pprt A) j i"
6.42 -  apply (simp add: join_matrix)
6.43 +  apply (simp add: sup_matrix_def)
6.45    apply (rule ext)+
6.46    apply (simp)
6.47 @@ -986,7 +986,7 @@
6.48
6.49  lemma nprt_move_matrix: "nprt (move_matrix (A::('a::lordered_ring) matrix) j i) = move_matrix (nprt A) j i"
6.51 -  apply (simp add: meet_matrix)
6.52 +  apply (simp add: inf_matrix_def)
6.54    apply (rule ext)+
6.55    apply (simp)
```
```     7.1 --- a/src/HOL/OrderedGroup.thy	Fri Mar 16 21:32:07 2007 +0100
7.2 +++ b/src/HOL/OrderedGroup.thy	Fri Mar 16 21:32:08 2007 +0100
7.3 @@ -1,4 +1,3 @@
7.4 -
7.5  (*  Title:   HOL/OrderedGroup.thy
7.6      ID:      \$Id\$
7.7      Author:  Gertrud Bauer, Steven Obua, Lawrence C Paulson, and Markus Wenzel,
7.8 @@ -8,7 +7,7 @@
7.9  header {* Ordered Groups *}
7.10
7.11  theory OrderedGroup
7.12 -imports LOrder
7.13 +imports Lattices
7.14  uses "~~/src/Provers/Arith/abel_cancel.ML"
7.15  begin
7.16
7.17 @@ -204,7 +203,7 @@
7.19
7.21 -  assumes add_le_imp_le_left: "c \<^loc>+ a \<sqsubseteq> c + b \<Longrightarrow> a \<sqsubseteq> b"
7.22 +  assumes add_le_imp_le_left: "c \<^loc>+ a \<sqsubseteq> c \<^loc>+ b \<Longrightarrow> a \<sqsubseteq> b"
7.23
7.25
7.26 @@ -565,13 +564,19 @@
7.27  lemma le_iff_diff_le_0: "(a \<le> b) = (a-b \<le> (0::'a::pordered_ab_group_add))"
7.29
7.30 +
7.31  subsection {* Lattice Ordered (Abelian) Groups *}
7.32
7.33 -axclass lordered_ab_group_meet < pordered_ab_group_add, meet_semilorder
7.34 +class lordered_ab_group_meet = pordered_ab_group_add + lower_semilattice
7.35 +
7.36 +class lordered_ab_group_join = pordered_ab_group_add + upper_semilattice
7.37
7.38 -axclass lordered_ab_group_join < pordered_ab_group_add, join_semilorder
7.39 +class lordered_ab_group = pordered_ab_group_add + lattice
7.40
7.41 -lemma add_inf_distrib_left: "a + (inf b c) = inf (a + b) (a + (c::'a::{pordered_ab_group_add, meet_semilorder}))"
7.42 +instance lordered_ab_group \<subseteq> lordered_ab_group_meet by default
7.43 +instance lordered_ab_group \<subseteq> lordered_ab_group_join by default
7.44 +
7.45 +lemma add_inf_distrib_left: "a + inf b c = inf (a + b) (a + (c::'a::{pordered_ab_group_add, lower_semilattice}))"
7.46  apply (rule order_antisym)
7.48  apply (rule add_le_imp_le_left [of "-a"])
7.49 @@ -580,7 +585,7 @@
7.51  done
7.52
7.53 -lemma add_sup_distrib_left: "a + (sup b c) = sup (a + b) (a+ (c::'a::{pordered_ab_group_add, join_semilorder}))"
7.54 +lemma add_sup_distrib_left: "a + sup b c = sup (a + b) (a+ (c::'a::{pordered_ab_group_add, upper_semilattice}))"
7.55  apply (rule order_antisym)
7.56  apply (rule add_le_imp_le_left [of "-a"])
7.57  apply (simp only: add_assoc[symmetric], simp)
7.58 @@ -590,55 +595,53 @@
7.59  apply (simp_all)
7.60  done
7.61
7.62 -lemma is_join_neg_inf: "is_join (% (a::'a::{pordered_ab_group_add, meet_semilorder}) b. - (inf (-a) (-b)))"
7.63 -apply (auto simp add: is_join_def)
7.66 -apply (subst neg_le_iff_le[symmetric])
7.68 -done
7.69 -
7.70 -lemma is_meet_neg_sup: "is_meet (% (a::'a::{pordered_ab_group_add, join_semilorder}) b. - (sup (-a) (-b)))"
7.71 -apply (auto simp add: is_meet_def)
7.74 -apply (subst neg_le_iff_le[symmetric])
7.76 -done
7.77 -
7.78 -axclass lordered_ab_group \<subseteq> pordered_ab_group_add, lorder
7.79 -
7.80 -instance lordered_ab_group_join \<subseteq> lordered_ab_group
7.81 -proof
7.82 -  show "? m. is_meet (m::'a\<Rightarrow>'a\<Rightarrow>('a::lordered_ab_group_join))" by (blast intro: is_meet_neg_sup)
7.83 -qed
7.84 -
7.85 -instance lordered_ab_group_meet \<subseteq> lordered_ab_group
7.86 -proof
7.87 -  show "? j. is_join (j::'a\<Rightarrow>'a\<Rightarrow>('a::lordered_ab_group_meet))" by (blast intro: is_join_neg_inf)
7.88 -qed
7.89 -
7.90 -lemma add_inf_distrib_right: "(inf a b) + (c::'a::lordered_ab_group) = inf (a+c) (b+c)"
7.91 +lemma add_inf_distrib_right: "inf a b + (c::'a::lordered_ab_group) = inf (a+c) (b+c)"
7.92  proof -
7.93 -  have "c + (inf a b) = inf (c+a) (c+b)" by (simp add: add_inf_distrib_left)
7.94 +  have "c + inf a b = inf (c+a) (c+b)" by (simp add: add_inf_distrib_left)
7.96  qed
7.97
7.98 -lemma add_sup_distrib_right: "(sup a b) + (c::'a::lordered_ab_group) = sup (a+c) (b+c)"
7.99 +lemma add_sup_distrib_right: "sup a b + (c::'a::lordered_ab_group) = sup (a+c) (b+c)"
7.100  proof -
7.101 -  have "c + (sup a b) = sup (c+a) (c+b)" by (simp add: add_sup_distrib_left)
7.102 +  have "c + sup a b = sup (c+a) (c+b)" by (simp add: add_sup_distrib_left)
7.104  qed
7.105
7.107
7.108 -lemma sup_eq_neg_inf: "sup a (b::'a::lordered_ab_group) = - inf (-a) (-b)"
7.109 -by (simp add: is_join_unique[OF is_join_join is_join_neg_inf])
7.110 +lemma inf_eq_neg_sup: "inf a (b\<Colon>'a\<Colon>lordered_ab_group) = - sup (-a) (-b)"
7.111 +proof (rule inf_unique)
7.112 +  fix a b :: 'a
7.113 +  show "- sup (-a) (-b) \<le> a" by (rule add_le_imp_le_right [of _ "sup (-a) (-b)"])
7.115 +next
7.116 +  fix a b :: 'a
7.117 +  show "- sup (-a) (-b) \<le> b" by (rule add_le_imp_le_right [of _ "sup (-a) (-b)"])
7.119 +next
7.120 +  fix a b c :: 'a
7.121 +  assume "a \<le> b" "a \<le> c"
7.122 +  then show "a \<le> - sup (-b) (-c)" by (subst neg_le_iff_le [symmetric])
7.124 +qed
7.125 +
7.126 +lemma sup_eq_neg_inf: "sup a (b\<Colon>'a\<Colon>lordered_ab_group) = - inf (-a) (-b)"
7.127 +proof (rule sup_unique)
7.128 +  fix a b :: 'a
7.129 +  show "a \<le> - inf (-a) (-b)" by (rule add_le_imp_le_right [of _ "inf (-a) (-b)"])
7.131 +next
7.132 +  fix a b :: 'a
7.133 +  show "b \<le> - inf (-a) (-b)" by (rule add_le_imp_le_right [of _ "inf (-a) (-b)"])
7.135 +next
7.136 +  fix a b c :: 'a
7.137 +  assume "a \<le> c" "b \<le> c"
7.138 +  then show "- inf (-a) (-b) \<le> c" by (subst neg_le_iff_le [symmetric])
7.140 +qed
7.141
7.142 -lemma inf_eq_neg_sup: "inf a (b::'a::lordered_ab_group) = - sup (-a) (-b)"
7.143 -by (simp add: is_meet_unique[OF is_meet_meet is_meet_neg_sup])
7.144 -
7.145 -lemma add_eq_inf_sup: "a + b = (sup a b) + (inf a (b::'a::lordered_ab_group))"
7.146 +lemma add_eq_inf_sup: "a + b = sup a b + inf a (b\<Colon>'a\<Colon>lordered_ab_group)"
7.147  proof -
7.148    have "0 = - inf 0 (a-b) + inf (a-b) 0" by (simp add: inf_commute)
7.149    hence "0 = sup 0 (b-a) + inf (a-b) 0" by (simp add: inf_eq_neg_sup)
7.150 @@ -761,8 +764,8 @@
7.151    with a show ?thesis by simp
7.152  qed
7.153
7.154 -axclass lordered_ab_group_abs \<subseteq> lordered_ab_group
7.155 -  abs_lattice: "abs x = sup x (-x)"
7.156 +class lordered_ab_group_abs = lordered_ab_group +
7.157 +  assumes abs_lattice: "abs x = sup x (uminus x)"
7.158
7.159  lemma abs_zero[simp]: "abs 0 = (0::'a::lordered_ab_group_abs)"
7.161 @@ -786,7 +789,7 @@
7.162  proof -
7.163    note b = add_le_cancel_right[of a a "-a",symmetric,simplified]
7.164    have c: "a + a = 0 \<Longrightarrow> -a = a" by (rule add_right_imp_eq[of _ a], simp)
7.165 -  show ?thesis by (auto simp add: max_def b linorder_not_less join_max)
7.166 +  show ?thesis by (auto simp add: max_def b linorder_not_less sup_max)
7.167  qed
7.168
7.169  lemma abs_if_lattice: "\<bar>a\<bar> = (if a < 0 then -a else (a::'a::{lordered_ab_group_abs, linorder}))"
7.170 @@ -1131,8 +1134,6 @@
7.171  val le_iff_diff_le_0 = thm "le_iff_diff_le_0";
7.174 -val is_join_neg_inf = thm "is_join_neg_inf";
7.175 -val is_meet_neg_sup = thm "is_meet_neg_sup";
```
```     8.1 --- a/src/HOL/Ring_and_Field.thy	Fri Mar 16 21:32:07 2007 +0100
8.2 +++ b/src/HOL/Ring_and_Field.thy	Fri Mar 16 21:32:08 2007 +0100
8.3 @@ -265,7 +265,7 @@
8.4
8.5  instance pordered_ring \<subseteq> pordered_ab_group_add ..
8.6
8.7 -axclass lordered_ring \<subseteq> pordered_ring, lordered_ab_group_abs
8.8 +class lordered_ring = pordered_ring + lordered_ab_group_abs
8.9
8.10  instance lordered_ring \<subseteq> lordered_ab_group_meet ..
8.11
8.12 @@ -274,9 +274,7 @@
8.13  class abs_if = minus + ord + zero +
8.14    assumes abs_if: "abs a = (if a \<sqsubset> 0 then (uminus a) else a)"
8.15
8.16 -class ordered_ring_strict = ring + ordered_semiring_strict + abs_if
8.17 -
8.18 -instance ordered_ring_strict \<subseteq> lordered_ab_group ..
8.19 +class ordered_ring_strict = ring + ordered_semiring_strict + abs_if + lordered_ab_group
8.20
8.21  instance ordered_ring_strict \<subseteq> lordered_ring
8.22    by intro_classes (simp add: abs_if sup_eq_if)
8.23 @@ -287,7 +285,7 @@
8.24    (*previously ordered_semiring*)
8.25    assumes zero_less_one [simp]: "\<^loc>0 \<sqsubset> \<^loc>1"
8.26
8.27 -class ordered_idom = comm_ring_1 + ordered_comm_semiring_strict + abs_if
8.28 +class ordered_idom = comm_ring_1 + ordered_comm_semiring_strict + abs_if + lordered_ab_group
8.29    (*previously ordered_ring*)
8.30
8.31  instance ordered_idom \<subseteq> ordered_ring_strict ..
```