src/HOL/Lattices.thy
changeset 24749 151b3758f576
parent 24640 85a6c200ecd3
child 25062 af5ef0d4d655
     1.1 --- a/src/HOL/Lattices.thy	Sat Sep 29 08:58:51 2007 +0200
     1.2 +++ b/src/HOL/Lattices.thy	Sat Sep 29 08:58:54 2007 +0200
     1.3 @@ -401,34 +401,34 @@
     1.4    "\<Squnion>{a, b} = a \<squnion> b"
     1.5    by (simp add: Sup_insert_simp)
     1.6  
     1.7 -end
     1.8 -
     1.9  definition
    1.10 -  top :: "'a::complete_lattice"
    1.11 +  top :: 'a
    1.12  where
    1.13    "top = Inf {}"
    1.14  
    1.15  definition
    1.16 -  bot :: "'a::complete_lattice"
    1.17 +  bot :: 'a
    1.18  where
    1.19    "bot = Sup {}"
    1.20  
    1.21 -lemma top_greatest [simp]: "x \<le> top"
    1.22 +lemma top_greatest [simp]: "x \<^loc>\<le> top"
    1.23    by (unfold top_def, rule Inf_greatest, simp)
    1.24  
    1.25 -lemma bot_least [simp]: "bot \<le> x"
    1.26 +lemma bot_least [simp]: "bot \<^loc>\<le> x"
    1.27    by (unfold bot_def, rule Sup_least, simp)
    1.28  
    1.29  definition
    1.30 -  SUPR :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::complete_lattice) \<Rightarrow> 'b"
    1.31 +  SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
    1.32  where
    1.33    "SUPR A f == Sup (f ` A)"
    1.34  
    1.35  definition
    1.36 -  INFI :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::complete_lattice) \<Rightarrow> 'b"
    1.37 +  INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
    1.38  where
    1.39    "INFI A f == Inf (f ` A)"
    1.40  
    1.41 +end
    1.42 +
    1.43  syntax
    1.44    "_SUP1"     :: "pttrns => 'b => 'b"           ("(3SUP _./ _)" [0, 10] 10)
    1.45    "_SUP"      :: "pttrn => 'a set => 'b => 'b"  ("(3SUP _:_./ _)" [0, 10] 10)