equal
deleted
inserted
replaced
43 lemma po_eq_conv: "((x::'a::po) = y) = (x \<sqsubseteq> y \<and> y \<sqsubseteq> x)" |
43 lemma po_eq_conv: "((x::'a::po) = y) = (x \<sqsubseteq> y \<and> y \<sqsubseteq> x)" |
44 by (fast elim!: antisym_less_inverse intro!: antisym_less) |
44 by (fast elim!: antisym_less_inverse intro!: antisym_less) |
45 |
45 |
46 lemma rev_trans_less: "\<lbrakk>(y::'a::po) \<sqsubseteq> z; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z" |
46 lemma rev_trans_less: "\<lbrakk>(y::'a::po) \<sqsubseteq> z; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z" |
47 by (rule trans_less) |
47 by (rule trans_less) |
|
48 |
|
49 lemma sq_ord_less_eq_trans: "\<lbrakk>a \<sqsubseteq> b; b = c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c" |
|
50 by (rule subst) |
|
51 |
|
52 lemma sq_ord_eq_less_trans: "\<lbrakk>a = b; b \<sqsubseteq> c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c" |
|
53 by (rule ssubst) |
|
54 |
|
55 lemmas HOLCF_trans_rules [trans] = |
|
56 trans_less |
|
57 antisym_less |
|
58 sq_ord_less_eq_trans |
|
59 sq_ord_eq_less_trans |
48 |
60 |
49 subsection {* Chains and least upper bounds *} |
61 subsection {* Chains and least upper bounds *} |
50 |
62 |
51 constdefs |
63 constdefs |
52 |
64 |