src/HOL/MicroJava/BV/Semilat.thy

 "is_lub r x y u == is_ub r x y u & (!z. is_ub r x y z \<longrightarrow> r u z)"
 
  some_lub :: "'a ord \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
 "some_lub r x y == SOME z. is_lub r x y z";
 
-locale (open) semilat =
+locale Semilat =
   fixes A :: "'a set"
     and r :: "'a ord"
     and f :: "'a binop"
   assumes semilat: "semilat(A,r,f)"
 

                  (!x:A. !y:A. !z:A. x <=_r z & y <=_r z \<longrightarrow> x +_f y <=_r z)"
 apply (unfold semilat_def split_conv [THEN eq_reflection])
 apply (rule refl [THEN eq_reflection])
 done
 
-lemma (in semilat) orderI [simp, intro]:
+lemma (in Semilat) orderI [simp, intro]:
   "order r"
   by (insert semilat) (simp add: semilat_Def)
 
-lemma (in semilat) closedI [simp, intro]:
+lemma (in Semilat) closedI [simp, intro]:
   "closed A f"
   by (insert semilat) (simp add: semilat_Def)
 
 lemma closedD:
   "\<lbrakk> closed A f; x:A; y:A \<rbrakk> \<Longrightarrow> x +_f y : A"

 
 lemma closed_UNIV [simp]: "closed UNIV f"
   by (simp add: closed_def)
 
 
-lemma (in semilat) closed_f [simp, intro]:
+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]:
+lemma (in Semilat) refl_r [intro, simp]:
   "x <=_r x"
   by simp
 
-lemma (in semilat) antisym_r [intro?]:
+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?]:
+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?]:
+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, intro?]:
+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, intro?]:
+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]:
+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)"
   by (blast intro: ub1 ub2 lub order_trans)
 
-lemma (in semilat) le_iff_plus_unchanged:
+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: antisym_r refl_r lub ub2)
 apply (erule subst)
 apply simp
 done
 
-lemma (in semilat) le_iff_plus_unchanged2:
+lemma (in Semilat) le_iff_plus_unchanged2:
   "\<lbrakk> x:A; y:A \<rbrakk> \<Longrightarrow> (x <=_r y) = (y +_f x = y)"
 apply (rule iffI)
  apply (blast intro: order_antisym lub order_refl ub1)
 apply (erule subst)
 apply simp
 done 
 
 
-lemma (in semilat) plus_assoc [simp]:
+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 -
   from a b have ab: "a +_f b \<in> A" ..
   from this c have abc: "(a +_f b) +_f c \<in> A" ..

       from this "c<" ab c abc' show ?thesis ..
     qed
   qed
 qed
 
-lemma (in semilat) plus_com_lemma:
+lemma (in Semilat) plus_com_lemma:
   "\<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" .. 
   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:
+lemma (in Semilat) plus_commutative:
   "\<lbrakk>a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> a +_f b = b +_f a"
 by(blast intro: order_antisym plus_com_lemma)
 
 lemma is_lubD:
   "is_lub r x y u \<Longrightarrow> is_ub r x y u & (!z. is_ub r x y z \<longrightarrow> r u z)"