# HG changeset patch
# User nipkow
# Date 1017748021 -7200
# Node ID 96bf406fd3e5485368f7e0552669c7cd9cf037c2
# Parent  cc9d7f403a4b2a2b19e91dfef7ca0e64f284a0aa
Started to convert to locales

diff -r cc9d7f403a4b -r 96bf406fd3e5 src/HOL/MicroJava/BV/Err.thy
--- a/src/HOL/MicroJava/BV/Err.thy	Thu Mar 28 16:28:12 2002 +0100
+++ b/src/HOL/MicroJava/BV/Err.thy	Tue Apr 02 13:47:01 2002 +0200
@@ -135,20 +135,24 @@
   "~(Err <_(le r) x)"
   by (simp add: lesssub_def lesub_def le_def split: err.split)
 
-lemma semilat_errI [intro]:
-  "semilat(A,r,f) \<Longrightarrow> semilat(err A, Err.le r, lift2(%x y. OK(f x y)))"
+lemma semilat_errI [intro]: includes semilat
+shows "semilat(err A, Err.le r, lift2(%x y. OK(f x y)))"
+apply(insert semilat)
 apply (unfold semilat_Def closed_def plussub_def lesub_def 
               lift2_def Err.le_def err_def)
 apply (simp split: err.split)
 done
 
-lemma err_semilat_eslI [intro, simp]: 
-  "\<And>L. semilat L \<Longrightarrow> err_semilat(esl L)"
+lemma err_semilat_eslI_aux:
+includes semilat shows "err_semilat(esl(A,r,f))"
 apply (unfold sl_def esl_def)
-apply (simp (no_asm_simp) only: split_tupled_all)
-apply (simp add: semilat_errI)
+apply (simp add: semilat_errI[OF semilat])
 done
 
+lemma err_semilat_eslI [intro, simp]:
+ "\<And>L. semilat L \<Longrightarrow> err_semilat(esl L)"
+by(simp add: err_semilat_eslI_aux split_tupled_all)
+
 lemma acc_err [simp, intro!]:  "acc r \<Longrightarrow> acc(le r)"
 apply (unfold acc_def lesub_def le_def lesssub_def)
 apply (simp add: wf_eq_minimal split: err.split)
@@ -222,27 +226,29 @@
 
 lemma semilat_le_err_Err_plus [simp]:
   "\<lbrakk> x: err A; semilat(err A, le r, f) \<rbrakk> \<Longrightarrow> Err +_f x = Err"
-  by (blast intro: le_iff_plus_unchanged [THEN iffD1] le_iff_plus_unchanged2 [THEN iffD1])
+  by (blast intro: semilat.le_iff_plus_unchanged [THEN iffD1]
+                   semilat.le_iff_plus_unchanged2 [THEN iffD1])
 
 lemma semilat_le_err_plus_Err [simp]:
   "\<lbrakk> x: err A; semilat(err A, le r, f) \<rbrakk> \<Longrightarrow> x +_f Err = Err"
-  by (blast intro: le_iff_plus_unchanged [THEN iffD1] le_iff_plus_unchanged2 [THEN iffD1])
+  by (blast intro: semilat.le_iff_plus_unchanged [THEN iffD1]
+                   semilat.le_iff_plus_unchanged2 [THEN iffD1])
 
 lemma semilat_le_err_OK1:
   "\<lbrakk> x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z \<rbrakk> 
   \<Longrightarrow> x <=_r z";
 apply (rule OK_le_err_OK [THEN iffD1])
 apply (erule subst)
-apply simp
-done 
+apply (simp add:semilat.ub1)
+done
 
 lemma semilat_le_err_OK2:
   "\<lbrakk> x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z \<rbrakk> 
   \<Longrightarrow> y <=_r z"
 apply (rule OK_le_err_OK [THEN iffD1])
 apply (erule subst)
-apply simp
-done 
+apply (simp add:semilat.ub2)
+done
 
 lemma eq_order_le:
   "\<lbrakk> x=y; order r \<rbrakk> \<Longrightarrow> x <=_r y"
@@ -257,14 +263,14 @@
   have plus_le_conv3: "\<And>A x y z f r. 
     \<lbrakk> semilat (A,r,f); x +_f y <=_r z; x:A; y:A; z:A \<rbrakk> 
     \<Longrightarrow> x <=_r z \<and> y <=_r z"
-    by (rule plus_le_conv [THEN iffD1])
+    by (rule semilat.plus_le_conv [THEN iffD1])
   case rule_context
   thus ?thesis
   apply (rule_tac iffI)
    apply clarify
    apply (drule OK_le_err_OK [THEN iffD2])
    apply (drule OK_le_err_OK [THEN iffD2])
-   apply (drule semilat_lub)
+   apply (drule semilat.lub[of _ _ _ "OK x" _ "OK y"])
         apply assumption
        apply assumption
       apply simp
@@ -276,10 +282,10 @@
   apply (rename_tac z)
   apply (subgoal_tac "OK z: err A")
   apply (drule eq_order_le)
-    apply blast
+    apply (erule semilat.orderI)
    apply (blast dest: plus_le_conv3) 
   apply (erule subst)
-  apply (blast intro: closedD)
+  apply (blast intro: semilat.closedI closedD)
   done 
 qed
 
diff -r cc9d7f403a4b -r 96bf406fd3e5 src/HOL/MicroJava/BV/JType.thy
--- a/src/HOL/MicroJava/BV/JType.thy	Thu Mar 28 16:28:12 2002 +0100
+++ b/src/HOL/MicroJava/BV/JType.thy	Tue Apr 02 13:47:01 2002 +0200
@@ -279,15 +279,15 @@
   have
     "(\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). x <=_(le (subtype G)) x +_(lift2 (sup G)) y) \<and> 
      (\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). y <=_(le (subtype G)) x +_(lift2 (sup G)) y)"
-    by (auto simp add: lesub_def plussub_def le_def lift2_def sup_subtype_greater split: err.split)
+    by (auto simp add: lesub_def plussub_def Err.le_def lift2_def sup_subtype_greater split: err.split)
 
-  moreover    
+  moreover
 
   from wf_prog single_valued acyclic 
   have
     "\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). \<forall>z\<in>err (types G). 
     x <=_(le (subtype G)) z \<and> y <=_(le (subtype G)) z \<longrightarrow> x +_(lift2 (sup G)) y <=_(le (subtype G)) z"
-    by (unfold lift2_def plussub_def lesub_def le_def)
+    by (unfold lift2_def plussub_def lesub_def Err.le_def)
        (auto intro: sup_subtype_smallest sup_exists split: err.split)
 
   ultimately
diff -r cc9d7f403a4b -r 96bf406fd3e5 src/HOL/MicroJava/BV/JVM.thy
--- a/src/HOL/MicroJava/BV/JVM.thy	Thu Mar 28 16:28:12 2002 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy	Tue Apr 02 13:47:01 2002 +0200
@@ -288,8 +288,8 @@
   apply (rule err_semilat_upto_esl)
   apply (rule err_semilat_JType_esl, assumption+)
   apply (rule err_semilat_eslI)
-  apply (rule semilat_Listn_sl)
-  apply (rule err_semilat_JType_esl, assumption+)  
+  apply (rule Listn_sl)
+  apply (rule err_semilat_JType_esl, assumption+)
   done
 
 lemma sl_triple_conv:
diff -r cc9d7f403a4b -r 96bf406fd3e5 src/HOL/MicroJava/BV/Kildall.thy
--- a/src/HOL/MicroJava/BV/Kildall.thy	Thu Mar 28 16:28:12 2002 +0100
+++ b/src/HOL/MicroJava/BV/Kildall.thy	Tue Apr 02 13:47:01 2002 +0200
@@ -43,36 +43,34 @@
 "merges f (p'#ps) ss = (let (p,s) = p' in merges f ps (ss[p := s +_f ss!p]))"
 
 
-lemmas [simp] = Let_def le_iff_plus_unchanged [symmetric]
+lemmas [simp] = Let_def semilat.le_iff_plus_unchanged [symmetric]
 
 
-lemma nth_merges:
-  "\<And>ss. \<lbrakk> semilat (A, r, f); p < length ss; ss \<in> list n A; 
-            \<forall>(p,t)\<in>set ps. p<n \<and> t\<in>A \<rbrakk> \<Longrightarrow>
+lemma (in semilat) nth_merges:
+ "\<And>ss. \<lbrakk>p < length ss; ss \<in> list n A; \<forall>(p,t)\<in>set ps. p<n \<and> t\<in>A \<rbrakk> \<Longrightarrow>
   (merges f ps ss)!p = map snd [(p',t') \<in> ps. p'=p] ++_f ss!p"
-  (is "\<And>ss. _ \<Longrightarrow> _ \<Longrightarrow> _ \<Longrightarrow> ?steptype ps \<Longrightarrow> ?P ss ps")
+  (is "\<And>ss. \<lbrakk>_; _; ?steptype ps\<rbrakk> \<Longrightarrow> ?P ss ps")
 proof (induct ps)
   show "\<And>ss. ?P ss []" by simp
 
   fix ss p' ps'
-  assume sl: "semilat (A, r, f)"
   assume ss: "ss \<in> list n A"
   assume l:  "p < length ss"
   assume "?steptype (p'#ps')"
   then obtain a b where
     p': "p'=(a,b)" and ab: "a<n" "b\<in>A" and "?steptype ps'"
     by (cases p', auto)
-  assume "\<And>ss. semilat (A,r,f) \<Longrightarrow> p < length ss \<Longrightarrow> ss \<in> list n A \<Longrightarrow> ?steptype ps' \<Longrightarrow> ?P ss ps'"
+  assume "\<And>ss. p< length ss \<Longrightarrow> ss \<in> list n A \<Longrightarrow> ?steptype ps' \<Longrightarrow> ?P ss ps'"
   hence IH: "\<And>ss. ss \<in> list n A \<Longrightarrow> p < length ss \<Longrightarrow> ?P ss ps'" .
 
-  from sl ss ab
+  from ss ab
   have "ss[a := b +_f ss!a] \<in> list n A" by (simp add: closedD)
   moreover
   from calculation
   have "p < length (ss[a := b +_f ss!a])" by simp
   ultimately
   have "?P (ss[a := b +_f ss!a]) ps'" by (rule IH)
-  with p' l 
+  with p' l
   show "?P ss (p'#ps')" by simp
 qed
 
@@ -84,47 +82,43 @@
   by (induct_tac ps, auto)
 
 
-lemma merges_preserves_type_lemma: 
-  "semilat(A,r,f) \<Longrightarrow>
-     \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A)
-          \<longrightarrow> merges f ps xs \<in> list n A" 
-  apply (frule semilatDclosedI) 
-  apply (unfold closed_def) 
-  apply (induct_tac ps)
-   apply simp
-  apply clarsimp
-  done
+lemma (in semilat) merges_preserves_type_lemma:
+shows "\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A)
+          \<longrightarrow> merges f ps xs \<in> list n A"
+apply (insert closedI)
+apply (unfold closed_def)
+apply (induct_tac ps)
+ apply simp
+apply clarsimp
+done
 
-lemma merges_preserves_type [simp]:
-  "\<lbrakk> semilat(A,r,f); xs \<in> list n A; \<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A \<rbrakk>
+lemma (in semilat) merges_preserves_type [simp]:
+ "\<lbrakk> xs \<in> list n A; \<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A \<rbrakk>
   \<Longrightarrow> merges f ps xs \<in> list n A"
-  by (simp add: merges_preserves_type_lemma)
-  
-lemma merges_incr_lemma:
-  "semilat(A,r,f) \<Longrightarrow> 
-     \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A) \<longrightarrow> xs <=[r] merges f ps xs"
-  apply (induct_tac ps)
-   apply simp
+by (simp add: merges_preserves_type_lemma)
+
+lemma (in semilat) merges_incr_lemma:
+ "\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A) \<longrightarrow> xs <=[r] merges f ps xs"
+apply (induct_tac ps)
+ apply simp
+apply simp
+apply clarify
+apply (rule order_trans)
   apply simp
-  apply clarify
-  apply (rule order_trans)
-    apply simp
-   apply (erule list_update_incr)
-     apply assumption
-    apply simp
-   apply simp
-  apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in])
-  done
+ apply (erule list_update_incr)
+  apply simp
+ apply simp
+apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in])
+done
 
-lemma merges_incr:
-  "\<lbrakk> semilat(A,r,f); xs \<in> list n A; \<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A \<rbrakk> 
+lemma (in semilat) merges_incr:
+ "\<lbrakk> xs \<in> list n A; \<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A \<rbrakk> 
   \<Longrightarrow> xs <=[r] merges f ps xs"
   by (simp add: merges_incr_lemma)
 
 
-lemma merges_same_conv [rule_format]:
-  "semilat(A,r,f) \<Longrightarrow> 
-     (\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x\<in>A) \<longrightarrow> 
+lemma (in semilat) merges_same_conv [rule_format]:
+ "(\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x\<in>A) \<longrightarrow> 
      (merges f ps xs = xs) = (\<forall>(p,x)\<in>set ps. x <=_r xs!p))"
   apply (induct_tac ps)
    apply simp
@@ -135,7 +129,6 @@
     apply (subgoal_tac "xs[p := x +_f xs!p] <=[r] xs")
      apply (force dest!: le_listD simp add: nth_list_update)
     apply (erule subst, rule merges_incr)
-        apply assumption
        apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in])
       apply clarify
       apply (rule conjI)
@@ -158,24 +151,22 @@
   done
 
 
-lemma list_update_le_listI [rule_format]:
+lemma (in semilat) list_update_le_listI [rule_format]:
   "set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> xs <=[r] ys \<longrightarrow> p < size xs \<longrightarrow>  
-   x <=_r ys!p \<longrightarrow> semilat(A,r,f) \<longrightarrow> x\<in>A \<longrightarrow> 
-   xs[p := x +_f xs!p] <=[r] ys"
+   x <=_r ys!p \<longrightarrow> x\<in>A \<longrightarrow> xs[p := x +_f xs!p] <=[r] ys"
+  apply(insert semilat)
   apply (unfold Listn.le_def lesub_def semilat_def)
   apply (simp add: list_all2_conv_all_nth nth_list_update)
   done
 
-lemma merges_pres_le_ub:
-  "\<lbrakk> semilat(A,r,f); set ts <= A; set ss <= A; 
-     \<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p < size ts; 
-     ss <=[r] ts \<rbrakk> 
+lemma (in semilat) merges_pres_le_ub:
+shows "\<lbrakk> set ts <= A; set ss <= A;
+         \<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p < size ts; ss <=[r] ts \<rbrakk>
   \<Longrightarrow> merges f ps ss <=[r] ts"
 proof -
-  { fix A r f t ts ps
+  { fix t ts ps
     have
-    "\<And>qs. \<lbrakk> semilat(A,r,f); set ts <= A; 
-              \<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p < size ts \<rbrakk> \<Longrightarrow> 
+    "\<And>qs. \<lbrakk>set ts <= A; \<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p< size ts \<rbrakk> \<Longrightarrow>
     set qs <= set ps  \<longrightarrow> 
     (\<forall>ss. set ss <= A \<longrightarrow> ss <=[r] ts \<longrightarrow> merges f qs ss <=[r] ts)"
     apply (induct_tac qs)
@@ -218,8 +209,8 @@
 
 (** iter **)
 
-lemma stable_pres_lemma:
-  "\<lbrakk> semilat (A,r,f); pres_type step n A; bounded step n; 
+lemma (in semilat) stable_pres_lemma:
+shows "\<lbrakk>pres_type step n A; bounded step n; 
      ss \<in> list n A; p \<in> w; \<forall>q\<in>w. q < n; 
      \<forall>q. q < n \<longrightarrow> q \<notin> w \<longrightarrow> stable r step ss q; q < n; 
      \<forall>s'. (q,s') \<in> set (step p (ss ! p)) \<longrightarrow> s' +_f ss ! q = ss ! q; 
@@ -237,8 +228,7 @@
    apply simp
   apply simp
   apply clarify
-  apply (subst nth_merges) 
-        apply assumption
+  apply (subst nth_merges)
        apply simp
        apply (blast dest: boundedD)
       apply assumption
@@ -248,10 +238,11 @@
      apply (erule pres_typeD)
        prefer 3 apply assumption
       apply simp
-     apply simp 
-  apply (frule nth_merges [of _ _ _ q _ _ "step p (ss!p)"]) (* fixme: why does method subst not work?? *)
-    prefer 2 apply assumption
-   apply simp
+     apply simp
+apply(subgoal_tac "q < length ss")
+prefer 2 apply simp
+  apply (frule nth_merges [of q _ _ "step p (ss!p)"]) (* fixme: why does method subst not work?? *)
+apply assumption
   apply clarify
   apply (rule conjI)
    apply (blast dest: boundedD)
@@ -281,8 +272,8 @@
  apply (rule order_trans)
    apply simp
   defer
- apply (rule ub2)
-    apply assumption
+ apply (rule pp_ub2)(*
+    apply assumption*)
    apply simp
    apply clarify
    apply simp
@@ -294,16 +285,15 @@
   apply (blast intro: listE_nth_in dest: boundedD)
  apply blast
  done
- 
-  
-lemma merges_bounded_lemma:
-  "\<lbrakk> semilat (A,r,f); mono r step n A; bounded step n; 
-     \<forall>(p',s') \<in> set (step p (ss!p)). s' \<in> A; ss \<in> list n A; ts \<in> list n A; p < n; 
-     ss <=[r] ts; \<forall>p. p < n \<longrightarrow> stable r step ts p \<rbrakk> 
+
+
+lemma (in semilat) merges_bounded_lemma:
+ "\<lbrakk> mono r step n A; bounded step n; 
+    \<forall>(p',s') \<in> set (step p (ss!p)). s' \<in> A; ss \<in> list n A; ts \<in> list n A; p < n; 
+    ss <=[r] ts; \<forall>p. p < n \<longrightarrow> stable r step ts p \<rbrakk> 
   \<Longrightarrow> merges f (step p (ss!p)) ss <=[r] ts" 
   apply (unfold stable_def)
   apply (rule merges_pres_le_ub)
-      apply assumption
      apply simp
     apply simp
    prefer 2 apply assumption
@@ -326,10 +316,11 @@
   apply (blast intro: order_trans)
   done
 
-lemma termination_lemma:  
-  "\<lbrakk> semilat(A,r,f); ss \<in> list n A; \<forall>(q,t)\<in>set qs. q<n \<and> t\<in>A; p\<in>w \<rbrakk> \<Longrightarrow> 
+lemma termination_lemma: includes semilat
+shows "\<lbrakk> ss \<in> list n A; \<forall>(q,t)\<in>set qs. q<n \<and> t\<in>A; p\<in>w \<rbrakk> \<Longrightarrow> 
       ss <[r] merges f qs ss \<or> 
   merges f qs ss = ss \<and> {q. \<exists>t. (q,t)\<in>set qs \<and> t +_f ss!q \<noteq> ss!q} Un (w-{p}) < w"
+apply(insert semilat)
   apply (unfold lesssub_def)
   apply (simp (no_asm_simp) add: merges_incr)
   apply (rule impI)
@@ -346,14 +337,15 @@
    apply clarsimp
   done 
 
-lemma iter_properties[rule_format]:
-  "\<lbrakk> semilat(A,r,f); acc r ; pres_type step n A; mono r step n A;
+lemma iter_properties[rule_format]: includes semilat
+shows "\<lbrakk> acc r ; pres_type step n A; mono r step n A;
      bounded step n; \<forall>p\<in>w0. p < n; ss0 \<in> list n A;
      \<forall>p<n. p \<notin> w0 \<longrightarrow> stable r step ss0 p \<rbrakk> \<Longrightarrow>
    iter f step ss0 w0 = (ss',w')
    \<longrightarrow>
    ss' \<in> list n A \<and> stables r step ss' \<and> ss0 <=[r] ss' \<and>
    (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow> ss' <=[r] ts)"
+apply(insert semilat)
 apply (unfold iter_def stables_def)
 apply (rule_tac P = "%(ss,w).
  ss \<in> list n A \<and> (\<forall>p<n. p \<notin> w \<longrightarrow> stable r step ss p) \<and> ss0 <=[r] ss \<and>
@@ -363,7 +355,7 @@
        in while_rule)
 
 -- "Invariant holds initially:"
-apply (simp add:stables_def) 
+apply (simp add:stables_def)
 
 -- "Invariant is preserved:"
 apply(simp add: stables_def split_paired_all)
@@ -385,8 +377,8 @@
  apply blast
 apply simp
 apply (rule conjI)
- apply (erule merges_preserves_type)
- apply blast 
+ apply (rule merges_preserves_type)
+ apply blast
  apply clarify
  apply (rule conjI)
   apply(clarsimp, blast dest!: boundedD)
@@ -396,10 +388,10 @@
   apply (erule listE_nth_in)
   apply blast
  apply blast
-apply (rule conjI) 
- apply clarify 
+apply (rule conjI)
+ apply clarify
  apply (blast intro!: stable_pres_lemma)
-apply (rule conjI) 
+apply (rule conjI)
  apply (blast intro!: merges_incr intro: le_list_trans)
 apply (rule conjI)
  apply clarsimp
@@ -408,11 +400,11 @@
 
 
 -- "Postcondition holds upon termination:"
-apply(clarsimp simp add: stables_def split_paired_all) 
+apply(clarsimp simp add: stables_def split_paired_all)
 
 -- "Well-foundedness of the termination relation:"
 apply (rule wf_lex_prod)
- apply (drule (1) semilatDorderI [THEN acc_le_listI])
+ apply (insert orderI [THEN acc_le_listI])
  apply (simp only: acc_def lesssub_def)
 apply (rule wf_finite_psubset) 
 
@@ -434,7 +426,7 @@
  apply blast
 apply (subst decomp_propa)
  apply blast
-apply clarify 
+apply clarify
 apply (simp del: listE_length
     add: lex_prod_def finite_psubset_def 
          bounded_nat_set_is_finite)
@@ -444,11 +436,11 @@
 apply assumption
 apply clarsimp
 apply (blast dest!: boundedD)
-done   
+done
 
 
-lemma kildall_properties:
-  "\<lbrakk> semilat(A,r,f); acc r; pres_type step n A; mono r step n A;
+lemma kildall_properties: includes semilat
+shows "\<lbrakk> acc r; pres_type step n A; mono r step n A;
      bounded step n; ss0 \<in> list n A \<rbrakk> \<Longrightarrow>
   kildall r f step ss0 \<in> list n A \<and>
   stables r step (kildall r f step ss0) \<and>
@@ -459,16 +451,14 @@
 apply(case_tac "iter f step ss0 (unstables r step ss0)")
 apply(simp)
 apply (rule iter_properties)
-apply (simp_all add: unstables_def stable_def)
-done
+by (simp_all add: unstables_def stable_def)
+
 
-lemma is_bcv_kildall:
-  "\<lbrakk> semilat(A,r,f); acc r; top r T; 
-      pres_type step n A; bounded step n; 
-      mono r step n A \<rbrakk>
+lemma is_bcv_kildall: includes semilat
+shows "\<lbrakk> acc r; top r T; pres_type step n A; bounded step n; mono r step n A \<rbrakk>
   \<Longrightarrow> is_bcv r T step n A (kildall r f step)"
 apply(unfold is_bcv_def wt_step_def)
-apply(insert kildall_properties[of A])
+apply(insert semilat kildall_properties[of A])
 apply(simp add:stables_def)
 apply clarify
 apply(subgoal_tac "kildall r f step ss \<in> list n A")
@@ -476,9 +466,9 @@
 apply (rule iffI)
  apply (rule_tac x = "kildall r f step ss" in bexI) 
   apply (rule conjI)
-   apply blast
+   apply (blast)
   apply (simp  (no_asm_simp))
- apply assumption
+ apply(assumption)
 apply clarify
 apply(subgoal_tac "kildall r f step ss!p <=_r ts!p")
  apply simp
diff -r cc9d7f403a4b -r 96bf406fd3e5 src/HOL/MicroJava/BV/LBVComplete.thy
--- a/src/HOL/MicroJava/BV/LBVComplete.thy	Thu Mar 28 16:28:12 2002 +0100
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Tue Apr 02 13:47:01 2002 +0200
@@ -110,8 +110,8 @@
     moreover    
     have mapD: "\<And>x ss. x \<in> set (?map ss) \<Longrightarrow> \<exists>p. (p,x) \<in> set ss \<and> p=pc+1" by auto
     from eosl x map1 
-    have "\<forall>x \<in> set (?map ss1). x \<le>|r (?sum ss1)" 
-      by clarify (rule ub1, simp add: Err.sl_def)
+    have "\<forall>x \<in> set (?map ss1). x \<le>|r (?sum ss1)"
+      by clarify (rule semilat.pp_ub1, simp add: Err.sl_def)
     with sum have "\<forall>x \<in> set (?map ss1). x \<le>|r (OK s1)" by simp
     with less have "\<forall>x \<in> set (?map ss2). x \<le>|r (OK s1)"
       apply clarify
@@ -127,7 +127,7 @@
       done
     moreover 
     from eosl map1 x have "x \<le>|r (?sum ss1)" 
-      by - (rule ub2, simp add: Err.sl_def)
+      by - (rule semilat.pp_ub2, simp add: Err.sl_def)
     with sum have "x \<le>|r (OK s1)" by simp
     moreover {
       have "set (?map ss2) \<subseteq> snd`(set ss2)" by auto
@@ -135,7 +135,7 @@
       finally have "set (?map ss2) \<subseteq> err (opt A)" . }
     ultimately
     have "?sum ss2 \<le>|r (OK s1)" using eosl x
-      by - (rule lub, simp add: Err.sl_def)
+      by - (rule semilat.pp_lub, simp add: Err.sl_def)
     also obtain s2 where sum2: "?sum ss2 = s2" by blast
     finally have "s2 \<le>|r (OK s1)" . 
     with sum2 have "\<exists>s2. ?sum ss2 = s2 \<and> s2 \<le>|r (OK s1)" by blast
@@ -295,7 +295,8 @@
     have "OK (cert!Suc pc) \<le>|r OK (phi!Suc pc)"     
       by (cases "cert!Suc pc") (simp, blast dest: fitsD2) 
     ultimately
-    have "?map ++|f OK (cert!Suc pc) \<le>|r OK (phi!Suc pc)" by (rule lub)
+    have "?map ++|f OK (cert!Suc pc) \<le>|r OK (phi!Suc pc)"
+      by (rule semilat.pp_lub)
     thus ?thesis by auto
   qed
   ultimately
@@ -386,7 +387,7 @@
     have "OK (cert!Suc pc) \<le>|r OK (phi!Suc pc)"     
       by (cases "cert!Suc pc") (simp, blast dest: fitsD2) 
     ultimately
-    have "?sum \<le>|r OK (phi!Suc pc)" by (rule lub)
+    have "?sum \<le>|r OK (phi!Suc pc)" by (rule semilat.pp_lub)
   }
   finally show ?thesis .
 qed
diff -r cc9d7f403a4b -r 96bf406fd3e5 src/HOL/MicroJava/BV/LBVSpec.thy
--- a/src/HOL/MicroJava/BV/LBVSpec.thy	Thu Mar 28 16:28:12 2002 +0100
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy	Tue Apr 02 13:47:01 2002 +0200
@@ -105,7 +105,7 @@
   "err_semilat (A,r,f) \<Longrightarrow> order r"
   apply (simp add: Err.sl_def)
   apply (rule order_le_err [THEN iffD1])
-  apply (rule semilatDorderI)
+  apply (rule semilat.orderI)
   apply assumption
   done
 
@@ -175,7 +175,8 @@
   also have "\<dots> = ?if ls ?if'" 
   proof -
     from l have "s' \<in> err (opt A)" by simp
-    with x semi have "(s' +|f x) \<in> err (opt A)" by (fast intro: closedD)
+    with x semi have "(s' +|f x) \<in> err (opt A)"
+      by (fast intro: semilat.closedI closedD)
     with x have "?if' \<in> err (opt A)" by auto
     hence "?P ls ?if'" by (rule IH) thus ?thesis by simp
   qed
diff -r cc9d7f403a4b -r 96bf406fd3e5 src/HOL/MicroJava/BV/Listn.thy
--- a/src/HOL/MicroJava/BV/Listn.thy	Thu Mar 28 16:28:12 2002 +0100
+++ b/src/HOL/MicroJava/BV/Listn.thy	Tue Apr 02 13:47:01 2002 +0200
@@ -283,30 +283,30 @@
 done
 
 
-lemma plus_list_ub1 [rule_format]:
-  "\<lbrakk> semilat(A,r,f); set xs <= A; set ys <= A; size xs = size ys \<rbrakk> 
+lemma (in semilat) plus_list_ub1 [rule_format]:
+ "\<lbrakk> set xs <= A; set ys <= A; size xs = size ys \<rbrakk> 
   \<Longrightarrow> xs <=[r] xs +[f] ys"
 apply (unfold unfold_lesub_list)
 apply (simp add: Listn.le_def list_all2_conv_all_nth)
 done
 
-lemma plus_list_ub2:
-  "\<lbrakk> semilat(A,r,f); set xs <= A; set ys <= A; size xs = size ys \<rbrakk>
+lemma (in semilat) plus_list_ub2:
+ "\<lbrakk>set xs <= A; set ys <= A; size xs = size ys \<rbrakk>
   \<Longrightarrow> ys <=[r] xs +[f] ys"
 apply (unfold unfold_lesub_list)
 apply (simp add: Listn.le_def list_all2_conv_all_nth)
-done 
+done
 
-lemma plus_list_lub [rule_format]:
-  "semilat(A,r,f) \<Longrightarrow> !xs ys zs. set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> set zs <= A 
+lemma (in semilat) plus_list_lub [rule_format]:
+shows "!xs ys zs. set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> set zs <= A 
   \<longrightarrow> size xs = n & size ys = n \<longrightarrow> 
   xs <=[r] zs & ys <=[r] zs \<longrightarrow> xs +[f] ys <=[r] zs"
 apply (unfold unfold_lesub_list)
 apply (simp add: Listn.le_def list_all2_conv_all_nth)
-done 
+done
 
-lemma list_update_incr [rule_format]:
-  "\<lbrakk> semilat(A,r,f); x:A \<rbrakk> \<Longrightarrow> set xs <= A \<longrightarrow> 
+lemma (in semilat) list_update_incr [rule_format]:
+ "x:A \<Longrightarrow> set xs <= A \<longrightarrow> 
   (!i. i<size xs \<longrightarrow> xs <=[r] xs[i := x +_f xs!i])"
 apply (unfold unfold_lesub_list)
 apply (simp add: Listn.le_def list_all2_conv_all_nth)
@@ -315,7 +315,7 @@
 apply (simp add: in_list_Suc_iff)
 apply clarify
 apply (simp add: nth_Cons split: nat.split)
-done 
+done
 
 lemma acc_le_listI [intro!]:
   "\<lbrakk> order r; acc r \<rbrakk> \<Longrightarrow> acc(Listn.le r)"
@@ -376,22 +376,23 @@
 apply (simp add: in_list_Suc_iff)
 apply clarify
 apply simp
-done 
+done
 
 
-lemma semilat_Listn_sl:
-  "\<And>L. semilat L \<Longrightarrow> semilat (Listn.sl n L)"
+lemma Listn_sl_aux:
+includes semilat shows "semilat (Listn.sl n (A,r,f))"
 apply (unfold Listn.sl_def)
-apply (simp (no_asm_simp) only: split_tupled_all)
 apply (simp (no_asm) only: semilat_Def split_conv)
 apply (rule conjI)
  apply simp
 apply (rule conjI)
- apply (simp only: semilatDclosedI closed_listI)
+ apply (simp only: closedI closed_listI)
 apply (simp (no_asm) only: list_def)
 apply (simp (no_asm_simp) add: plus_list_ub1 plus_list_ub2 plus_list_lub)
-done  
+done
 
+lemma Listn_sl: "\<And>L. semilat L \<Longrightarrow> semilat (Listn.sl n L)"
+ by(simp add: Listn_sl_aux split_tupled_all)
 
 lemma coalesce_in_err_list [rule_format]:
   "!xes. xes : list n (err A) \<longrightarrow> coalesce xes : err(list n A)"
@@ -443,7 +444,7 @@
 apply (erule thin_rl)
 apply (erule thin_rl)
 apply force
-done 
+done
 
 lemma coalesce_eq_OK_ub_D [rule_format]:
   "semilat(err A, Err.le r, lift2 f) \<Longrightarrow> 
@@ -500,7 +501,7 @@
 apply (simp add: in_list_Suc_iff)
 apply clarify
 apply (simp add: plussub_def closed_err_lift2_conv)
-done 
+done
 
 lemma closed_lift2_sup:
   "closed (err A) (lift2 f) \<Longrightarrow> 
@@ -515,9 +516,9 @@
 apply (unfold Err.sl_def)
 apply (simp only: split_conv)
 apply (simp (no_asm) only: semilat_Def plussub_def)
-apply (simp (no_asm_simp) only: semilatDclosedI closed_lift2_sup)
+apply (simp (no_asm_simp) only: semilat.closedI closed_lift2_sup)
 apply (rule conjI)
- apply (drule semilatDorderI)
+ apply (drule semilat.orderI)
  apply simp
 apply (simp (no_asm) only: unfold_lesub_err Err.le_def err_def sup_def lift2_def)
 apply (simp (no_asm_simp) add: coalesce_eq_OK1_D coalesce_eq_OK2_D split: err.split)
diff -r cc9d7f403a4b -r 96bf406fd3e5 src/HOL/MicroJava/BV/Product.thy
--- a/src/HOL/MicroJava/BV/Product.thy	Thu Mar 28 16:28:12 2002 +0100
+++ b/src/HOL/MicroJava/BV/Product.thy	Tue Apr 02 13:47:01 2002 +0200
@@ -78,14 +78,14 @@
   have plus_le_conv2:
     "\<And>r f z. \<lbrakk> z : err A; semilat (err A, r, f); OK x : err A; OK y : err A;
                  OK x +_f OK y <=_r z\<rbrakk> \<Longrightarrow> OK x <=_r z \<and> OK y <=_r z"
-    by (rule plus_le_conv [THEN iffD1])
+    by (rule semilat.plus_le_conv [THEN iffD1])
   case rule_context
   thus ?thesis
   apply (rule_tac iffI)
    apply clarify
    apply (drule OK_le_err_OK [THEN iffD2])
    apply (drule OK_le_err_OK [THEN iffD2])
-   apply (drule semilat_lub)
+   apply (drule semilat.lub[of _ _ _ "OK x" _ "OK y"])
         apply assumption
        apply assumption
       apply simp
@@ -101,7 +101,7 @@
       apply simp
       apply blast
      apply simp
-    apply (blast dest: semilatDorderI order_refl)
+    apply (blast dest: semilat.orderI order_refl)
    apply blast
   apply (erule subst)
   apply (unfold semilat_def err_def closed_def)
@@ -115,15 +115,15 @@
 apply (simp (no_asm_simp) only: split_tupled_all)
 apply simp
 apply (simp (no_asm) only: semilat_Def)
-apply (simp (no_asm_simp) only: semilatDclosedI closed_lift2_sup)
+apply (simp (no_asm_simp) only: semilat.closedI closed_lift2_sup)
 apply (simp (no_asm) only: unfold_lesub_err Err.le_def unfold_plussub_lift2 sup_def)
 apply (auto elim: semilat_le_err_OK1 semilat_le_err_OK2
             simp add: lift2_def  split: err.split)
-apply (blast dest: semilatDorderI)
-apply (blast dest: semilatDorderI)
+apply (blast dest: semilat.orderI)
+apply (blast dest: semilat.orderI)
 
 apply (rule OK_le_err_OK [THEN iffD1])
-apply (erule subst, subst OK_lift2_OK [symmetric], rule semilat_lub)
+apply (erule subst, subst OK_lift2_OK [symmetric], rule semilat.lub)
 apply simp
 apply simp
 apply simp
@@ -132,7 +132,7 @@
 apply simp
 
 apply (rule OK_le_err_OK [THEN iffD1])
-apply (erule subst, subst OK_lift2_OK [symmetric], rule semilat_lub)
+apply (erule subst, subst OK_lift2_OK [symmetric], rule semilat.lub)
 apply simp
 apply simp
 apply simp
diff -r cc9d7f403a4b -r 96bf406fd3e5 src/HOL/MicroJava/BV/Semilat.thy
--- a/src/HOL/MicroJava/BV/Semilat.thy	Thu Mar 28 16:28:12 2002 +0100
+++ b/src/HOL/MicroJava/BV/Semilat.thy	Tue Apr 02 13:47:01 2002 +0200
@@ -61,8 +61,13 @@
 "is_lub r x y u == is_ub r x y u & (!z. is_ub r x y z \<longrightarrow> (u,z):r)"
 
  some_lub :: "('a*'a)set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
-"some_lub r x y == SOME z. is_lub r x y z"
+"some_lub r x y == SOME z. is_lub r x y z";
 
+locale semilat =
+  fixes A :: "'a set"
+    and r :: "'a ord"
+    and f :: "'a binop"
+  assumes semilat: "semilat(A,r,f)"
 
 lemma order_refl [simp, intro]:
   "order r \<Longrightarrow> x <=_r x";
@@ -71,7 +76,7 @@
 lemma order_antisym:
   "\<lbrakk> order r; x <=_r y; y <=_r x \<rbrakk> \<Longrightarrow> x = y"
 apply (unfold order_def)
-apply (simp (no_asm_simp))  
+apply (simp (no_asm_simp))
 done
 
 lemma order_trans:
@@ -109,48 +114,44 @@
 apply (rule refl [THEN eq_reflection])
 done
 
-lemma semilatDorderI [simp, intro]:
-  "semilat(A,r,f) \<Longrightarrow> order r"
-  by (simp add: semilat_Def)
+lemma (in semilat) orderI [simp, intro]:
+  "order r"
+  by (insert semilat) (simp add: semilat_Def)
+
+lemma (in semilat) closedI [simp, intro]:
+  "closed A f"
+  by (insert semilat) (simp add: semilat_Def)
+
+lemma (in semilat) ub1 [simp]:
+  "\<lbrakk> x:A; y:A \<rbrakk> \<Longrightarrow> x <=_r x +_f y"
+  by (insert semilat) (unfold semilat_Def, simp)
+
+lemma (in semilat) ub2 [simp]:
+  "\<lbrakk> x:A; y:A \<rbrakk> \<Longrightarrow> y <=_r x +_f y"
+  by (insert semilat) (unfold semilat_Def, simp)
 
-lemma semilatDclosedI [simp, intro]:
-  "semilat(A,r,f) \<Longrightarrow> closed A f"
-apply (unfold semilat_Def)
+lemma (in semilat) lub [simp]:
+ "\<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
+
+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 (erule subst)
 apply simp
 done
 
-lemma semilat_ub1 [simp]:
-  "\<lbrakk> semilat(A,r,f); x:A; y:A \<rbrakk> \<Longrightarrow> x <=_r x +_f y"
-  by (unfold semilat_Def, simp)
-
-lemma semilat_ub2 [simp]:
-  "\<lbrakk> semilat(A,r,f); x:A; y:A \<rbrakk> \<Longrightarrow> y <=_r x +_f y"
-  by (unfold semilat_Def, simp)
-
-lemma semilat_lub [simp]:
- "\<lbrakk> x <=_r z; y <=_r z; semilat(A,r,f); x:A; y:A; z:A \<rbrakk> \<Longrightarrow> x +_f y <=_r z";
-  by (unfold semilat_Def, simp)
-
-
-lemma plus_le_conv [simp]:
-  "\<lbrakk> x:A; y:A; z:A; semilat(A,r,f) \<rbrakk> 
-  \<Longrightarrow> (x +_f y <=_r z) = (x <=_r z & y <=_r z)"
-apply (unfold semilat_Def)
-apply (blast intro: semilat_ub1 semilat_ub2 semilat_lub order_trans)
-done
-
-lemma le_iff_plus_unchanged:
-  "\<lbrakk> x:A; y:A; semilat(A,r,f) \<rbrakk> \<Longrightarrow> (x <=_r y) = (x +_f y = y)"
+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 (intro semilatDorderI order_antisym semilat_lub order_refl semilat_ub2, assumption+)
-apply (erule subst)
-apply simp
-done 
-
-lemma le_iff_plus_unchanged2:
-  "\<lbrakk> x:A; y:A; semilat(A,r,f) \<rbrakk> \<Longrightarrow> (x <=_r y) = (y +_f x = y)"
-apply (rule iffI)
- apply (intro semilatDorderI order_antisym semilat_lub order_refl semilat_ub1, assumption+)
+ apply (blast intro: order_antisym lub order_refl ub1)
 apply (erule subst)
 apply simp
 done 
@@ -160,23 +161,22 @@
   "\<lbrakk> closed A f; x:A; y:A \<rbrakk> \<Longrightarrow> x +_f y : A"
 apply (unfold closed_def)
 apply blast
-done 
+done
 
 lemma closed_UNIV [simp]: "closed UNIV f"
   by (simp add: closed_def)
 
 
-lemma plus_assoc [simp]:
-  assumes semi: "semilat (A,r,f)"
+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 semilatDclosedI [OF semi], intro]
-  note semilat_ub1 [OF semi, intro]
-  note semilat_ub2 [OF semi, intro]
-  note semilat_lub [OF _ _ semi, intro]
+  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" ..
@@ -186,7 +186,7 @@
   from order show ?thesis
   proof (rule order_antisym)
     show "a +_f (b +_f c) <=_r (a +_f b) +_f c"
-    proof -      
+    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" .
@@ -212,28 +212,24 @@
   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"
+lemma (in semilat) plus_com_lemma:
+  "\<lbrakk>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)
+  assume a: "a \<in> A" and b: "b \<in> A"  
+  from b a have "a <=_r b +_f a" by (rule ub2)
   moreover
-  from semi b a have "b <=_r b +_f a" by (rule semilat_ub1)
+  from b a have "b <=_r b +_f a" by (rule ub1)
   moreover
-  note semi a b
+  note a b
   moreover
-  from semi b a have "b +_f a \<in> A" by (rule closedD [OF semilatDclosedI])
+  from b a have "b +_f a \<in> A" by (rule closedD [OF closedI])
   ultimately
-  show ?thesis by (rule semilat_lub)
+  show ?thesis by (rule 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 (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> (u,z):r)"
diff -r cc9d7f403a4b -r 96bf406fd3e5 src/HOL/MicroJava/BV/SemilatAlg.thy
--- a/src/HOL/MicroJava/BV/SemilatAlg.thy	Thu Mar 28 16:28:12 2002 +0100
+++ b/src/HOL/MicroJava/BV/SemilatAlg.thy	Tue Apr 02 13:47:01 2002 +0200
@@ -62,79 +62,71 @@
   done
 
 
-lemma plusplus_closed: 
-  "\<And>y. \<lbrakk>semilat (A, r, f); set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> x ++_f y \<in> A"
+lemma plusplus_closed: includes semilat shows
+  "\<And>y. \<lbrakk> set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> x ++_f y \<in> A"
 proof (induct x)
   show "\<And>y. y \<in> A \<Longrightarrow> [] ++_f y \<in> A" by simp
   fix y x xs
-  assume sl: "semilat (A, r, f)" and y: "y \<in> A" and xs: "set (x#xs) \<subseteq> A"
-  assume IH: "\<And>y. \<lbrakk>semilat (A, r, f); 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 sl x y have "(x +_f y) \<in> A" by (simp add: closedD)
-  with sl xs have "xs ++_f (x +_f y) \<in> A" by - (rule IH)
+  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)
   thus "(x#xs) ++_f y \<in> A" by simp
 qed
 
-lemma ub2: "\<And>y. \<lbrakk>semilat (A, r, f); set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> y <=_r x ++_f y"
+lemma (in semilat) pp_ub2:
+ "\<And>y. \<lbrakk> set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> y <=_r x ++_f y"
 proof (induct x)
-  show "\<And>y. semilat(A, r, f) \<Longrightarrow> y <=_r [] ++_f y" by simp 
+  from semilat show "\<And>y. y <=_r [] ++_f y" by simp
   
   fix y a l
-  assume sl: "semilat (A, r, f)"
   assume y:  "y \<in> A"
   assume "set (a#l) \<subseteq> A"
-  then obtain a: "a \<in> A" and x: "set l \<subseteq> A" by simp 
-  assume "\<And>y. \<lbrakk>semilat (A, r, f); set l \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> y <=_r l ++_f y"
+  then obtain a: "a \<in> A" and x: "set l \<subseteq> A" by simp
+  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" .
 
-  from sl have "order r" .. note order_trans [OF this, trans]  
-  
-  from sl a y have "y <=_r a +_f y" by (rule semilat_ub2)
-  also
-  from sl a y have "a +_f y \<in> A" by (simp add: closedD)
+  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)
   hence "(a +_f y) <=_r l ++_f (a +_f y)" by (rule IH)
-  finally
-  have "y <=_r l ++_f (a +_f y)" .
+  finally have "y <=_r l ++_f (a +_f y)" .
   thus "y <=_r (a#l) ++_f y" by simp
 qed
 
 
-lemma ub1: 
-  "\<And>y. \<lbrakk>semilat (A, r, f); set ls \<subseteq> A; y \<in> A; x \<in> set ls\<rbrakk> \<Longrightarrow> x <=_r ls ++_f y"
+lemma (in semilat) pp_ub1:
+shows "\<And>y. \<lbrakk>set ls \<subseteq> A; y \<in> A; x \<in> set ls\<rbrakk> \<Longrightarrow> x <=_r ls ++_f y"
 proof (induct ls)
   show "\<And>y. x \<in> set [] \<Longrightarrow> x <=_r [] ++_f y" by simp
-  
+
   fix y s ls
-  assume sl: "semilat (A, r, f)" 
-  hence "order r" .. note order_trans [OF this, trans]
+  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" 
 
   assume 
-    "\<And>y. \<lbrakk>semilat (A, r, f); set ls \<subseteq> A; y \<in> A; x \<in> set ls\<rbrakk> \<Longrightarrow> x <=_r ls ++_f y"
+    "\<And>y. \<lbrakk>set ls \<subseteq> A; y \<in> A; x \<in> set ls\<rbrakk> \<Longrightarrow> x <=_r ls ++_f y"
   hence IH: "\<And>y. x \<in> set ls \<Longrightarrow> y \<in> A \<Longrightarrow> x <=_r ls ++_f y" .
 
   assume "x \<in> set (s#ls)"
   then obtain xls: "x = s \<or> x \<in> set ls" by simp
   moreover {
     assume xs: "x = s"
-    from sl s y have "s <=_r s +_f y" by (rule semilat_ub1)
-    also
-    from sl s y have "s +_f y \<in> A" by (simp add: closedD)
-    with sl ls have "(s +_f y) <=_r ls ++_f (s +_f y)" by (rule ub2)
-    finally 
-    have "s <=_r ls ++_f (s +_f y)" .
+    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)
+    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
   } 
   moreover {
     assume "x \<in> set ls"
     hence "\<And>y. y \<in> A \<Longrightarrow> x <=_r ls ++_f y" by (rule IH)
-    moreover
-    from sl s y
-    have "s +_f y \<in> A" by (simp add: closedD)
-    ultimately 
-    have "x <=_r ls ++_f (s +_f y)" .
+    moreover from s y have "s +_f y \<in> A" by (simp add: closedD)
+    ultimately have "x <=_r ls ++_f (s +_f y)" .
   }
   ultimately 
   have "x <=_r ls ++_f (s +_f y)" by blast
@@ -142,8 +134,8 @@
 qed
 
 
-lemma lub:
-  assumes sl: "semilat (A, r, f)" and "z \<in> A"
+lemma (in semilat) pp_lub:
+  assumes "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)
@@ -153,25 +145,25 @@
   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) 
+  assume "y <=_r z" have "l +_f y <=_r z" by (rule lub)
   moreover
-  from sl l y have "l +_f y \<in> A" by (fast intro: closedD)
+  from 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
+  have "ls ++_f (l +_f y) <=_r z" by - (insert ls lsz)
   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> 
+lemma ub1': includes semilat
+shows "\<lbrakk>\<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" 
 proof -
   let "b <=_r ?map ++_f y" = ?thesis
 
-  assume "semilat (A, r, f)" "y \<in> A"
+  assume "y \<in> A"
   moreover
   assume "\<forall>(p,s) \<in> set S. s \<in> A"
   hence "set ?map \<subseteq> A" by auto
@@ -179,7 +171,7 @@
   assume "(a,b) \<in> set S"
   hence "b \<in> set ?map" by (induct S, auto)
   ultimately
-  show ?thesis by - (rule ub1)
+  show ?thesis by - (rule pp_ub1)
 qed