equal
deleted
inserted
replaced
74 "top = \<Sqinter>{}" |
74 "top = \<Sqinter>{}" |
75 by (auto intro: antisym Inf_greatest) |
75 by (auto intro: antisym Inf_greatest) |
76 |
76 |
77 lemma sup_bot [simp]: |
77 lemma sup_bot [simp]: |
78 "x \<squnion> bot = x" |
78 "x \<squnion> bot = x" |
79 using bot_least [of x] by (simp add: le_iff_sup sup_commute) |
79 using bot_least [of x] by (simp add: sup_commute) |
80 |
80 |
81 lemma inf_top [simp]: |
81 lemma inf_top [simp]: |
82 "x \<sqinter> top = x" |
82 "x \<sqinter> top = x" |
83 using top_greatest [of x] by (simp add: le_iff_inf inf_commute) |
83 using top_greatest [of x] by (simp add: inf_commute) |
84 |
84 |
85 definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where |
85 definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where |
86 "SUPR A f = \<Squnion> (f ` A)" |
86 "SUPR A f = \<Squnion> (f ` A)" |
87 |
87 |
88 definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where |
88 definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where |