# HG changeset patch
# User kleing
# Date 1017173416 -3600
# Node ID 472b1c91b09f0227403be4943dd5054debbefd8b
# Parent  a59af3a83c613f5a535988b8a6b535ca37054776
+_f is associative and commutative

diff -r a59af3a83c61 -r 472b1c91b09f src/HOL/MicroJava/BV/Semilat.thy
--- a/src/HOL/MicroJava/BV/Semilat.thy	Sun Mar 24 19:16:51 2002 +0100
+++ b/src/HOL/MicroJava/BV/Semilat.thy	Tue Mar 26 21:10:16 2002 +0100
@@ -166,6 +166,75 @@
   by (simp add: closed_def)
 
 
+lemma plus_assoc [simp]:
+  assumes semi: "semilat (A,r,f)"
+  assumes a: "a \<in> A" and b: "b \<in> A" and c: "c \<in> A"
+  shows "a +_f (b +_f c) = a +_f b +_f c"
+proof -
+  have order: "order r" ..
+  note order_trans [OF order,trans]
+  note closedD [OF semilatDclosedI [OF semi], intro]
+  note semilat_ub1 [OF semi, intro]
+  note semilat_ub2 [OF semi, intro]
+  note semilat_lub [OF _ _ semi, intro]
+
+  from a b have ab: "a +_f b \<in> A" ..
+  from this c have abc: "(a +_f b) +_f c \<in> A" ..
+  from b c have bc: "b +_f c \<in> A" ..
+  from a this have abc': "a +_f (b +_f c) \<in> A" ..
+
+  from order show ?thesis
+  proof (rule order_antisym)
+    show "a +_f (b +_f c) <=_r (a +_f b) +_f c"
+    proof -      
+      from a b have "a <=_r a +_f b" .. 
+      also from ab c have "\<dots> <=_r \<dots> +_f c" ..
+      finally have "a<": "a <=_r (a +_f b) +_f c" .
+      from a b have "b <=_r a +_f b" ..
+      also from ab c have "\<dots> <=_r \<dots> +_f c" ..
+      finally have "b<": "b <=_r (a +_f b) +_f c" .
+      from ab c have "c<": "c <=_r (a +_f b) +_f c" ..    
+      from "b<" "c<" b c abc have "b +_f c <=_r (a +_f b) +_f c" ..
+      from "a<" this a bc abc show ?thesis ..
+    qed
+    show "(a +_f b) +_f c <=_r a +_f (b +_f c)" 
+    proof -
+      from b c have "b <=_r b +_f c" .. 
+      also from a bc have "\<dots> <=_r a +_f \<dots>" ..
+      finally have "b<": "b <=_r a +_f (b +_f c)" .
+      from b c have "c <=_r b +_f c" ..
+      also from a bc have "\<dots> <=_r a +_f \<dots>" ..
+      finally have "c<": "c <=_r a +_f (b +_f c)" .
+      from a bc have "a<": "a <=_r a +_f (b +_f c)" ..
+      from "a<" "b<" a b abc' have "a +_f b <=_r a +_f (b +_f c)" ..
+      from this "c<" ab c abc' show ?thesis ..
+    qed
+  qed
+qed
+
+lemma plus_com_lemma:
+  "\<lbrakk>semilat (A,r,f); a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> a +_f b <=_r b +_f a"
+proof -
+  assume semi: "semilat (A,r,f)" and a: "a \<in> A" and b: "b \<in> A"  
+  from semi b a have "a <=_r b +_f a" by (rule semilat_ub2)
+  moreover
+  from semi b a have "b <=_r b +_f a" by (rule semilat_ub1)
+  moreover
+  note semi a b
+  moreover
+  from semi b a have "b +_f a \<in> A" by (rule closedD [OF semilatDclosedI])
+  ultimately
+  show ?thesis by (rule semilat_lub)
+qed
+
+lemma plus_commutative:
+  "\<lbrakk>semilat (A,r,f); a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> a +_f b = b +_f a"
+  apply (frule semilatDorderI)
+  apply (erule order_antisym)
+  apply (rule plus_com_lemma, assumption+)
+  apply (rule plus_com_lemma, assumption+)
+  done
+
 lemma is_lubD:
   "is_lub r x y u \<Longrightarrow> is_ub r x y u & (!z. is_ub r x y z \<longrightarrow> (u,z):r)"
   by (simp add: is_lub_def)