140 have "x <=_r ls ++_f (s +_f y)" by blast |
140 have "x <=_r ls ++_f (s +_f y)" by blast |
141 thus "x <=_r (s#ls) ++_f y" by simp |
141 thus "x <=_r (s#ls) ++_f y" by simp |
142 qed |
142 qed |
143 |
143 |
144 |
144 |
|
145 lemma lub: |
|
146 assumes sl: "semilat (A, r, f)" and "z \<in> A" |
|
147 shows |
|
148 "\<And>y. y \<in> A \<Longrightarrow> set xs \<subseteq> A \<Longrightarrow> \<forall>x \<in> set xs. x <=_r z \<Longrightarrow> y <=_r z \<Longrightarrow> xs ++_f y <=_r z" |
|
149 proof (induct xs) |
|
150 fix y assume "y <=_r z" thus "[] ++_f y <=_r z" by simp |
|
151 next |
|
152 fix y l ls assume y: "y \<in> A" and "set (l#ls) \<subseteq> A" |
|
153 then obtain l: "l \<in> A" and ls: "set ls \<subseteq> A" by auto |
|
154 assume "\<forall>x \<in> set (l#ls). x <=_r z" |
|
155 then obtain "l <=_r z" and lsz: "\<forall>x \<in> set ls. x <=_r z" by auto |
|
156 assume "y <=_r z" have "l +_f y <=_r z" by (rule semilat_lub) |
|
157 moreover |
|
158 from sl l y have "l +_f y \<in> A" by (fast intro: closedD) |
|
159 moreover |
|
160 assume "\<And>y. y \<in> A \<Longrightarrow> set ls \<subseteq> A \<Longrightarrow> \<forall>x \<in> set ls. x <=_r z \<Longrightarrow> y <=_r z |
|
161 \<Longrightarrow> ls ++_f y <=_r z" |
|
162 ultimately |
|
163 have "ls ++_f (l +_f y) <=_r z" using ls lsz by - assumption |
|
164 thus "(l#ls) ++_f y <=_r z" by simp |
|
165 qed |
|
166 |
|
167 |
145 lemma ub1': |
168 lemma ub1': |
146 "\<lbrakk>semilat (A, r, f); \<forall>(p,s) \<in> set S. s \<in> A; y \<in> A; (a,b) \<in> set S\<rbrakk> |
169 "\<lbrakk>semilat (A, r, f); \<forall>(p,s) \<in> set S. s \<in> A; y \<in> A; (a,b) \<in> set S\<rbrakk> |
147 \<Longrightarrow> b <=_r map snd [(p', t')\<in>S. p' = a] ++_f y" |
170 \<Longrightarrow> b <=_r map snd [(p', t')\<in>S. p' = a] ++_f y" |
148 proof - |
171 proof - |
149 let "b <=_r ?map ++_f y" = ?thesis |
172 let "b <=_r ?map ++_f y" = ?thesis |