equal
deleted
inserted
replaced
36 |
36 |
37 text {* minimal fixes least element *} |
37 text {* minimal fixes least element *} |
38 |
38 |
39 lemma minimal2UU[OF allI] : "\<forall>x. uu \<sqsubseteq> x \<Longrightarrow> uu = (THE u. \<forall>y. u \<sqsubseteq> y)" |
39 lemma minimal2UU[OF allI] : "\<forall>x. uu \<sqsubseteq> x \<Longrightarrow> uu = (THE u. \<forall>y. u \<sqsubseteq> y)" |
40 by (blast intro: theI2 below_antisym) |
40 by (blast intro: theI2 below_antisym) |
|
41 |
|
42 lemma eq_imp_below: "x = y \<Longrightarrow> x \<sqsubseteq> y" |
|
43 by simp |
41 |
44 |
42 text {* the reverse law of anti-symmetry of @{term "op <<"} *} |
45 text {* the reverse law of anti-symmetry of @{term "op <<"} *} |
43 (* Is this rule ever useful? *) |
46 (* Is this rule ever useful? *) |
44 lemma below_antisym_inverse: "x = y \<Longrightarrow> x \<sqsubseteq> y \<and> y \<sqsubseteq> x" |
47 lemma below_antisym_inverse: "x = y \<Longrightarrow> x \<sqsubseteq> y \<and> y \<sqsubseteq> x" |
45 by simp |
48 by simp |