# HG changeset patch
# User kleing
# Date 1017173433 -3600
# Node ID 3ccbd3a97bcb6993a6cbd1865e1da19d3ee7c0a9
# Parent  472b1c91b09f0227403be4943dd5054debbefd8b
lub property of ++_f

diff -r 472b1c91b09f -r 3ccbd3a97bcb src/HOL/MicroJava/BV/SemilatAlg.thy
--- 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"