# HG changeset patch
# User kleing
# Date 1017931664 -7200
# Node ID c2e4d99901626e17ebc09350faf6de91dcf39b4c
# Parent  70704dd48bd54afa16b7d3a6ae08f2ee65ffece3
tuned

diff -r 70704dd48bd5 -r c2e4d9990162 src/HOL/MicroJava/BV/Semilat.thy
--- a/src/HOL/MicroJava/BV/Semilat.thy	Wed Apr 03 10:21:13 2002 +0200
+++ b/src/HOL/MicroJava/BV/Semilat.thy	Thu Apr 04 16:47:44 2002 +0200
@@ -122,28 +122,52 @@
   "closed A f"
   by (insert semilat) (simp add: semilat_Def)
 
-lemma (in semilat) ub1 [simp]:
+lemma closedD:
+  "\<lbrakk> closed A f; x:A; y:A \<rbrakk> \<Longrightarrow> x +_f y : A"
+  by (unfold closed_def) blast
+
+lemma closed_UNIV [simp]: "closed UNIV f"
+  by (simp add: closed_def)
+
+
+lemma (in semilat) closed_f [simp, intro]:
+  "\<lbrakk>x:A; y:A\<rbrakk>  \<Longrightarrow> x +_f y : A"
+  by (simp add: closedD [OF closedI])
+
+lemma (in semilat) refl_r [intro, simp]:
+  "x <=_r x"
+  by simp
+
+lemma (in semilat) antisym_r [intro?]:
+  "\<lbrakk> x <=_r y; y <=_r x \<rbrakk> \<Longrightarrow> x = y"
+  by (rule order_antisym) auto
+  
+lemma (in semilat) trans_r [trans, intro?]:
+  "\<lbrakk>x <=_r y; y <=_r z\<rbrakk> \<Longrightarrow> x <=_r z"
+  by (auto intro: order_trans)    
+  
+
+lemma (in semilat) ub1 [simp, intro?]:
   "\<lbrakk> x:A; y:A \<rbrakk> \<Longrightarrow> x <=_r x +_f y"
   by (insert semilat) (unfold semilat_Def, simp)
 
-lemma (in semilat) ub2 [simp]:
+lemma (in semilat) ub2 [simp, intro?]:
   "\<lbrakk> x:A; y:A \<rbrakk> \<Longrightarrow> y <=_r x +_f y"
   by (insert semilat) (unfold semilat_Def, simp)
 
-lemma (in semilat) lub [simp]:
+lemma (in semilat) lub [simp, intro?]:
  "\<lbrakk> x <=_r z; y <=_r z; x:A; y:A; z:A \<rbrakk> \<Longrightarrow> x +_f y <=_r z";
   by (insert semilat) (unfold semilat_Def, simp)
 
 
 lemma (in semilat) plus_le_conv [simp]:
   "\<lbrakk> x:A; y:A; z:A \<rbrakk> \<Longrightarrow> (x +_f y <=_r z) = (x <=_r z & y <=_r z)"
-apply (blast intro: ub1 ub2 lub order_trans)
-done
+  by (blast intro: ub1 ub2 lub order_trans)
 
 lemma (in semilat) le_iff_plus_unchanged:
   "\<lbrakk> x:A; y:A \<rbrakk> \<Longrightarrow> (x <=_r y) = (x +_f y = y)"
 apply (rule iffI)
- apply (blast intro: order_antisym lub order_refl ub2);
+ apply (blast intro: antisym_r refl_r lub ub2)
 apply (erule subst)
 apply simp
 done
@@ -157,34 +181,17 @@
 done 
 
 
-lemma closedD:
-  "\<lbrakk> closed A f; x:A; y:A \<rbrakk> \<Longrightarrow> x +_f y : A"
-apply (unfold closed_def)
-apply blast
-done
-
-lemma closed_UNIV [simp]: "closed UNIV f"
-  by (simp add: closed_def)
-
-
 lemma (in semilat) plus_assoc [simp]:
   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 closedI, intro]
-  note ub1 [intro]
-  note ub2 [intro]
-  note lub [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 ?thesis
+  proof    
     show "a +_f (b +_f c) <=_r (a +_f b) +_f c"
     proof -
       from a b have "a <=_r a +_f b" .. 
@@ -216,15 +223,11 @@
   "\<lbrakk>a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> a +_f b <=_r b +_f a"
 proof -
   assume a: "a \<in> A" and b: "b \<in> A"  
-  from b a have "a <=_r b +_f a" by (rule ub2)
-  moreover
-  from b a have "b <=_r b +_f a" by (rule ub1)
-  moreover
-  note a b
-  moreover
-  from b a have "b +_f a \<in> A" by (rule closedD [OF closedI])
-  ultimately
-  show ?thesis by (rule lub)
+  from b a have "a <=_r b +_f a" .. 
+  moreover from b a have "b <=_r b +_f a" ..
+  moreover note a b
+  moreover from b a have "b +_f a \<in> A" ..
+  ultimately show ?thesis ..
 qed
 
 lemma (in semilat) plus_commutative:
diff -r 70704dd48bd5 -r c2e4d9990162 src/HOL/MicroJava/BV/SemilatAlg.thy
--- a/src/HOL/MicroJava/BV/SemilatAlg.thy	Wed Apr 03 10:21:13 2002 +0200
+++ b/src/HOL/MicroJava/BV/SemilatAlg.thy	Thu Apr 04 16:47:44 2002 +0200
@@ -70,8 +70,8 @@
   assume y: "y \<in> A" and xs: "set (x#xs) \<subseteq> A"
   assume IH: "\<And>y. \<lbrakk> set xs \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> xs ++_f y \<in> A"
   from xs obtain x: "x \<in> A" and "set xs \<subseteq> A" by simp
-  from semilat x y have "(x +_f y) \<in> A" by (simp add: closedD)
-  with semilat xs have "xs ++_f (x +_f y) \<in> A" by - (rule IH)
+  from x y have "(x +_f y) \<in> A" ..
+  with xs have "xs ++_f (x +_f y) \<in> A" by - (rule IH)
   thus "(x#xs) ++_f y \<in> A" by simp
 qed
 
@@ -87,10 +87,8 @@
   assume "\<And>y. \<lbrakk>set l \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> y <=_r l ++_f y"
   hence IH: "\<And>y. y \<in> A \<Longrightarrow> y <=_r l ++_f y" .
 
-  have "order r" .. note order_trans [OF this, trans]
-
-  from a y have "y <=_r a +_f y" by (rule ub2)
-  also from a y have "a +_f y \<in> A" by (simp add: closedD)
+  from a y have "y <=_r a +_f y" ..
+  also from a y have "a +_f y \<in> A" ..
   hence "(a +_f y) <=_r l ++_f (a +_f y)" by (rule IH)
   finally have "y <=_r l ++_f (a +_f y)" .
   thus "y <=_r (a#l) ++_f y" by simp
@@ -103,7 +101,6 @@
   show "\<And>y. x \<in> set [] \<Longrightarrow> x <=_r [] ++_f y" by simp
 
   fix y s ls
-  have "order r" .. note order_trans [OF this, trans]
   assume "set (s#ls) \<subseteq> A"
   then obtain s: "s \<in> A" and ls: "set ls \<subseteq> A" by simp
   assume y: "y \<in> A" 
@@ -116,8 +113,8 @@
   then obtain xls: "x = s \<or> x \<in> set ls" by simp
   moreover {
     assume xs: "x = s"
-    from s y have "s <=_r s +_f y" by (rule ub1)
-    also from s y have "s +_f y \<in> A" by (simp add: closedD)
+    from s y have "s <=_r s +_f y" ..
+    also from s y have "s +_f y \<in> A" ..
     with ls have "(s +_f y) <=_r ls ++_f (s +_f y)" by (rule pp_ub2)
     finally have "s <=_r ls ++_f (s +_f y)" .
     with xs have "x <=_r ls ++_f (s +_f y)" by simp
@@ -125,7 +122,7 @@
   moreover {
     assume "x \<in> set ls"
     hence "\<And>y. y \<in> A \<Longrightarrow> x <=_r ls ++_f y" by (rule IH)
-    moreover from s y have "s +_f y \<in> A" by (simp add: closedD)
+    moreover from s y have "s +_f y \<in> A" ..
     ultimately have "x <=_r ls ++_f (s +_f y)" .
   }
   ultimately 
@@ -145,14 +142,14 @@
   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 lub)
+  assume "y <=_r z" have "l +_f y <=_r z" ..  
   moreover
-  from l y have "l +_f y \<in> A" by (fast intro: closedD)
+  from l y have "l +_f y \<in> A" ..
   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" by - (insert ls lsz)
+  have "ls ++_f (l +_f y) <=_r z" using ls lsz by -
   thus "(l#ls) ++_f y <=_r z" by simp
 qed