equal
deleted
inserted
replaced
18 Sup :: "'a::order set \<Rightarrow> 'a" |
18 Sup :: "'a::order set \<Rightarrow> 'a" |
19 |
19 |
20 defs Sup_def: "Sup A == Meet {b. \<forall>a \<in> A. a <= b}" |
20 defs Sup_def: "Sup A == Meet {b. \<forall>a \<in> A. a <= b}" |
21 |
21 |
22 definition |
22 definition |
23 SUP :: "('a \<Rightarrow> 'b::order) \<Rightarrow> 'b" (binder "SUP " 10) |
23 SUP :: "('a \<Rightarrow> 'b::order) \<Rightarrow> 'b" (binder "SUP " 10) where |
24 "SUP x. f x == Sup (f ` UNIV)" |
24 "SUP x. f x == Sup (f ` UNIV)" |
|
25 |
25 (* |
26 (* |
26 abbreviation |
27 abbreviation |
27 bot :: "'a::order" |
28 bot :: "'a::order" where |
28 "bot == Sup {}" |
29 "bot == Sup {}" |
29 *) |
30 *) |
30 axclass comp_lat < order |
31 axclass comp_lat < order |
31 Meet_lower: "x \<in> A \<Longrightarrow> Meet A <= x" |
32 Meet_lower: "x \<in> A \<Longrightarrow> Meet A <= x" |
32 Meet_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z <= x) \<Longrightarrow> z <= Meet A" |
33 Meet_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z <= x) \<Longrightarrow> z <= Meet A" |
33 |
34 |