equal
deleted
inserted
replaced
50 obtains "ord x y" | "ord y x" |
50 obtains "ord x y" | "ord y x" |
51 using assms unfolding chain_def by fast |
51 using assms unfolding chain_def by fast |
52 |
52 |
53 lemma chain_empty: "chain ord {}" |
53 lemma chain_empty: "chain ord {}" |
54 by(simp add: chain_def) |
54 by(simp add: chain_def) |
|
55 |
|
56 lemma chain_equality: "chain op = A \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. x = y)" |
|
57 by(auto simp add: chain_def) |
55 |
58 |
56 subsection {* Chain-complete partial orders *} |
59 subsection {* Chain-complete partial orders *} |
57 |
60 |
58 text {* |
61 text {* |
59 A ccpo has a least upper bound for any chain. In particular, the |
62 A ccpo has a least upper bound for any chain. In particular, the |