equal
deleted
inserted
replaced
147 text \<open>lubs are unique\<close> |
147 text \<open>lubs are unique\<close> |
148 |
148 |
149 lemma is_lub_unique: "S <<| x \<Longrightarrow> S <<| y \<Longrightarrow> x = y" |
149 lemma is_lub_unique: "S <<| x \<Longrightarrow> S <<| y \<Longrightarrow> x = y" |
150 unfolding is_lub_def is_ub_def by (blast intro: below_antisym) |
150 unfolding is_lub_def is_ub_def by (blast intro: below_antisym) |
151 |
151 |
152 text \<open>technical lemmas about @{term lub} and @{term is_lub}\<close> |
152 text \<open>technical lemmas about \<^term>\<open>lub\<close> and \<^term>\<open>is_lub\<close>\<close> |
153 |
153 |
154 lemma is_lub_lub: "M <<| x \<Longrightarrow> M <<| lub M" |
154 lemma is_lub_lub: "M <<| x \<Longrightarrow> M <<| lub M" |
155 unfolding lub_def by (rule theI [OF _ is_lub_unique]) |
155 unfolding lub_def by (rule theI [OF _ is_lub_unique]) |
156 |
156 |
157 lemma lub_eqI: "M <<| l \<Longrightarrow> lub M = l" |
157 lemma lub_eqI: "M <<| l \<Longrightarrow> lub M = l" |