src/HOL/Lattices.thy
changeset 28685 275122631271
parent 28562 4e74209f113e
child 28692 a2bc5ce0c9fc
     1.1 --- a/src/HOL/Lattices.thy	Fri Oct 24 17:48:36 2008 +0200
     1.2 +++ b/src/HOL/Lattices.thy	Fri Oct 24 17:48:37 2008 +0200
     1.3 @@ -332,7 +332,7 @@
     1.4  
     1.5  subsection {* Complete lattices *}
     1.6  
     1.7 -class complete_lattice = lattice +
     1.8 +class complete_lattice = lattice + top + bot +
     1.9    fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
    1.10      and Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
    1.11    assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
    1.12 @@ -383,19 +383,13 @@
    1.13    "\<Squnion>{a, b} = a \<squnion> b"
    1.14    by (simp add: Sup_insert_simp)
    1.15  
    1.16 -definition
    1.17 -  top :: 'a where
    1.18 +lemma top_def:
    1.19    "top = \<Sqinter>{}"
    1.20 +  by (auto intro: antisym Inf_greatest)
    1.21  
    1.22 -definition
    1.23 -  bot :: 'a where
    1.24 +lemma bot_def:
    1.25    "bot = \<Squnion>{}"
    1.26 -
    1.27 -lemma top_greatest [simp]: "x \<le> top"
    1.28 -  by (unfold top_def, rule Inf_greatest, simp)
    1.29 -
    1.30 -lemma bot_least [simp]: "bot \<le> x"
    1.31 -  by (unfold bot_def, rule Sup_least, simp)
    1.32 +  by (auto intro: antisym Sup_least)
    1.33  
    1.34  definition
    1.35    SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
    1.36 @@ -499,12 +493,6 @@
    1.37    "\<not> Sup {}"
    1.38    unfolding Sup_bool_def by auto
    1.39  
    1.40 -lemma top_bool_eq: "top = True"
    1.41 -  by (iprover intro!: order_antisym le_boolI top_greatest)
    1.42 -
    1.43 -lemma bot_bool_eq: "bot = False"
    1.44 -  by (iprover intro!: order_antisym le_boolI bot_least)
    1.45 -
    1.46  
    1.47  subsection {* Fun as lattice *}
    1.48  
    1.49 @@ -556,12 +544,6 @@
    1.50    "\<Squnion>{} = (\<lambda>_. \<Squnion>{})"
    1.51    by rule (auto simp add: Sup_fun_def)
    1.52  
    1.53 -lemma top_fun_eq: "top = (\<lambda>x. top)"
    1.54 -  by (iprover intro!: order_antisym le_funI top_greatest)
    1.55 -
    1.56 -lemma bot_fun_eq: "bot = (\<lambda>x. bot)"
    1.57 -  by (iprover intro!: order_antisym le_funI bot_least)
    1.58 -
    1.59  
    1.60  subsection {* Set as lattice *}
    1.61