133 |
133 |
134 lemma (in Semilat) trans_r [trans, intro?]: "\<lbrakk>x \<sqsubseteq>\<^sub>r y; y \<sqsubseteq>\<^sub>r z\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^sub>r z" |
134 lemma (in Semilat) trans_r [trans, intro?]: "\<lbrakk>x \<sqsubseteq>\<^sub>r y; y \<sqsubseteq>\<^sub>r z\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^sub>r z" |
135 (*<*) by (auto intro: order_trans) (*>*) |
135 (*<*) by (auto intro: order_trans) (*>*) |
136 |
136 |
137 lemma (in Semilat) ub1 [simp, intro?]: "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^sub>r x \<squnion>\<^sub>f y" |
137 lemma (in Semilat) ub1 [simp, intro?]: "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^sub>r x \<squnion>\<^sub>f y" |
138 (*<*) by (insert semilat) (unfold semilat_Def, simp) (*>*) |
138 (*<*) using semilat by (simp add: semilat_Def) (*>*) |
139 |
139 |
140 lemma (in Semilat) ub2 [simp, intro?]: "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> y \<sqsubseteq>\<^sub>r x \<squnion>\<^sub>f y" |
140 lemma (in Semilat) ub2 [simp, intro?]: "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> y \<sqsubseteq>\<^sub>r x \<squnion>\<^sub>f y" |
141 (*<*) by (insert semilat) (unfold semilat_Def, simp) (*>*) |
141 (*<*) using semilat by (simp add: semilat_Def) (*>*) |
142 |
142 |
143 lemma (in Semilat) lub [simp, intro?]: |
143 lemma (in Semilat) lub [simp, intro?]: |
144 "\<lbrakk> x \<sqsubseteq>\<^sub>r z; y \<sqsubseteq>\<^sub>r z; x \<in> A; y \<in> A; z \<in> A \<rbrakk> \<Longrightarrow> x \<squnion>\<^sub>f y \<sqsubseteq>\<^sub>r z" |
144 "\<lbrakk> x \<sqsubseteq>\<^sub>r z; y \<sqsubseteq>\<^sub>r z; x \<in> A; y \<in> A; z \<in> A \<rbrakk> \<Longrightarrow> x \<squnion>\<^sub>f y \<sqsubseteq>\<^sub>r z" |
145 (*<*) by (insert semilat) (unfold semilat_Def, simp) (*>*) |
145 (*<*) using semilat by (simp add: semilat_Def) (*>*) |
146 |
146 |
147 lemma (in Semilat) plus_le_conv [simp]: |
147 lemma (in Semilat) plus_le_conv [simp]: |
148 "\<lbrakk> x \<in> A; y \<in> A; z \<in> A \<rbrakk> \<Longrightarrow> (x \<squnion>\<^sub>f y \<sqsubseteq>\<^sub>r z) = (x \<sqsubseteq>\<^sub>r z \<and> y \<sqsubseteq>\<^sub>r z)" |
148 "\<lbrakk> x \<in> A; y \<in> A; z \<in> A \<rbrakk> \<Longrightarrow> (x \<squnion>\<^sub>f y \<sqsubseteq>\<^sub>r z) = (x \<sqsubseteq>\<^sub>r z \<and> y \<sqsubseteq>\<^sub>r z)" |
149 (*<*) by (blast intro: ub1 ub2 lub order_trans) (*>*) |
149 (*<*) by (blast intro: ub1 ub2 lub order_trans) (*>*) |
150 |
150 |