equal
deleted
inserted
replaced
105 fix a assume "a \<in> A" |
105 fix a assume "a \<in> A" |
106 with assms obtain b where "b \<in> B" and "a \<sqsubseteq> b" by blast |
106 with assms obtain b where "b \<in> B" and "a \<sqsubseteq> b" by blast |
107 from `b \<in> B` have "b \<sqsubseteq> \<Squnion>B" by (rule Sup_upper) |
107 from `b \<in> B` have "b \<sqsubseteq> \<Squnion>B" by (rule Sup_upper) |
108 with `a \<sqsubseteq> b` show "a \<sqsubseteq> \<Squnion>B" by auto |
108 with `a \<sqsubseteq> b` show "a \<sqsubseteq> \<Squnion>B" by auto |
109 qed |
109 qed |
110 |
|
111 lemma top_le: |
|
112 "\<top> \<sqsubseteq> x \<Longrightarrow> x = \<top>" |
|
113 by (rule antisym) auto |
|
114 |
|
115 lemma le_bot: |
|
116 "x \<sqsubseteq> \<bottom> \<Longrightarrow> x = \<bottom>" |
|
117 by (rule antisym) auto |
|
118 |
|
119 lemma not_less_bot [simp]: "\<not> (x \<sqsubset> \<bottom>)" |
|
120 using bot_least [of x] by (auto simp: le_less) |
|
121 |
|
122 lemma not_top_less [simp]: "\<not> (\<top> \<sqsubset> x)" |
|
123 using top_greatest [of x] by (auto simp: le_less) |
|
124 |
110 |
125 lemma Sup_upper2: "u \<in> A \<Longrightarrow> v \<sqsubseteq> u \<Longrightarrow> v \<sqsubseteq> \<Squnion>A" |
111 lemma Sup_upper2: "u \<in> A \<Longrightarrow> v \<sqsubseteq> u \<Longrightarrow> v \<sqsubseteq> \<Squnion>A" |
126 using Sup_upper[of u A] by auto |
112 using Sup_upper[of u A] by auto |
127 |
113 |
128 lemma Inf_lower2: "u \<in> A \<Longrightarrow> u \<sqsubseteq> v \<Longrightarrow> \<Sqinter>A \<sqsubseteq> v" |
114 lemma Inf_lower2: "u \<in> A \<Longrightarrow> u \<sqsubseteq> v \<Longrightarrow> \<Sqinter>A \<sqsubseteq> v" |