author kleing Tue, 26 Mar 2002 21:10:33 +0100 changeset 13069 3ccbd3a97bcb parent 13068 472b1c91b09f child 13070 fcfdefa4617b
lub property of ++_f
```--- a/src/HOL/MicroJava/BV/SemilatAlg.thy	Tue Mar 26 21:10:16 2002 +0100
+++ b/src/HOL/MicroJava/BV/SemilatAlg.thy	Tue Mar 26 21:10:33 2002 +0100
@@ -142,6 +142,29 @@
qed

+lemma lub:
+  assumes sl: "semilat (A, r, f)" and "z \<in> A"
+  shows
+  "\<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"
+proof (induct xs)
+  fix y assume "y <=_r z" thus "[] ++_f y <=_r z" by simp
+next
+  fix y l ls assume y: "y \<in> A" and "set (l#ls) \<subseteq> A"
+  then obtain l: "l \<in> A" and ls: "set ls \<subseteq> A" by auto
+  assume "\<forall>x \<in> set (l#ls). x <=_r z"
+  then obtain "l <=_r z" and lsz: "\<forall>x \<in> set ls. x <=_r z" by auto
+  assume "y <=_r z" have "l +_f y <=_r z" by (rule semilat_lub)
+  moreover
+  from sl l y have "l +_f y \<in> A" by (fast intro: closedD)
+  moreover
+  assume "\<And>y. y \<in> A \<Longrightarrow> set ls \<subseteq> A \<Longrightarrow> \<forall>x \<in> set ls. x <=_r z \<Longrightarrow> y <=_r z
+          \<Longrightarrow> ls ++_f y <=_r z"
+  ultimately
+  have "ls ++_f (l +_f y) <=_r z" using ls lsz by - assumption
+  thus "(l#ls) ++_f y <=_r z" by simp
+qed
+
+
lemma ub1':
"\<lbrakk>semilat (A, r, f); \<forall>(p,s) \<in> set S. s \<in> A; y \<in> A; (a,b) \<in> set S\<rbrakk>
\<Longrightarrow> b <=_r map snd [(p', t')\<in>S. p' = a] ++_f y" ```