# HG changeset patch
# User kleing
# Date 1016626867 -3600
# Node ID 4b1edf2f6bd261690bf40db60f0520299efb6143
# Parent  75b2edff1af329500fe84e1946854857bfe7e34e
small refactoring for lbv with semilattices

diff -r 75b2edff1af3 -r 4b1edf2f6bd2 src/HOL/MicroJava/BV/Err.thy
--- a/src/HOL/MicroJava/BV/Err.thy	Mon Mar 18 11:47:03 2002 +0100
+++ b/src/HOL/MicroJava/BV/Err.thy	Wed Mar 20 13:21:07 2002 +0100
@@ -135,14 +135,14 @@
   "~(Err <_(le r) x)"
   by (simp add: lesssub_def lesub_def le_def split: err.split)
 
-lemma semilat_errI:
+lemma semilat_errI [intro]:
   "semilat(A,r,f) \<Longrightarrow> semilat(err A, Err.le r, lift2(%x y. OK(f x y)))"
 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: 
+lemma err_semilat_eslI [intro, simp]: 
   "\<And>L. semilat L \<Longrightarrow> err_semilat(esl L)"
 apply (unfold sl_def esl_def)
 apply (simp (no_asm_simp) only: split_tupled_all)
diff -r 75b2edff1af3 -r 4b1edf2f6bd2 src/HOL/MicroJava/BV/Kildall.thy
--- a/src/HOL/MicroJava/BV/Kildall.thy	Mon Mar 18 11:47:03 2002 +0100
+++ b/src/HOL/MicroJava/BV/Kildall.thy	Wed Mar 20 13:21:07 2002 +0100
@@ -8,22 +8,8 @@
 
 header {* \isaheader{Kildall's Algorithm}\label{sec:Kildall} *}
 
-theory Kildall = Typing_Framework + While_Combinator + Product:
-
+theory Kildall = SemilatAlg + While_Combinator:
 
-syntax "@lesubstep_type" :: "(nat \<times> 's) list \<Rightarrow> 's ord \<Rightarrow> (nat \<times> 's) list \<Rightarrow> bool"
-       ("(_ /<=|_| _)" [50, 0, 51] 50)
-translations
- "x <=|r| y" == "x <=[(Product.le (op =) r)] y"
- 
-
-constdefs
- pres_type :: "'s step_type \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool"
-"pres_type step n A == \<forall>s\<in>A. \<forall>p<n. \<forall>(q,s')\<in>set (step p s). s' \<in> A"
-
- mono :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool"
-"mono r step n A ==
- \<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> step p s <=|r| step p t"
 
 consts
  iter :: "'s binop \<Rightarrow> 's step_type \<Rightarrow>
@@ -60,12 +46,6 @@
 lemmas [simp] = Let_def le_iff_plus_unchanged [symmetric]
 
 
-consts
- "@plusplussub" :: "'a list \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" ("(_ /++'__ _)" [65, 1000, 66] 65)
-primrec
-  "[] ++_f y = y"
-  "(x#xs) ++_f y = xs ++_f (x +_f y)"
-
 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>
@@ -97,18 +77,6 @@
 qed
 
 
-lemma pres_typeD:
-  "\<lbrakk> pres_type step n A; s\<in>A; p<n; (q,s')\<in>set (step p s) \<rbrakk> \<Longrightarrow> s' \<in> A"
-  by (unfold pres_type_def, blast)
-
-lemma boundedD: 
-  "\<lbrakk> bounded step n; p < n; (q,t) : set (step p xs) \<rbrakk> \<Longrightarrow> q < n" 
-  by (unfold bounded_def, blast)
-
-lemma monoD:
-  "\<lbrakk> mono r step n A; p < n; s\<in>A; s <=_r t \<rbrakk> \<Longrightarrow> step p s <=|r| step p t"
-  by (unfold mono_def, blast)
-
 (** merges **)
 
 lemma length_merges [rule_format, simp]:
@@ -250,113 +218,6 @@
 
 (** iter **)
 
-lemma plusplus_closed: 
-  "\<And>y. \<lbrakk>semilat (A, r, f); 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)
-  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"
-proof (induct x)
-  show "\<And>y. semilat(A, r, f) \<Longrightarrow> 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"
-  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)
-  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
-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"
-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]
-  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"
-  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)" .
-    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)" .
-  }
-  ultimately 
-  have "x <=_r ls ++_f (s +_f y)" by blast
-  thus "x <=_r (s#ls) ++_f y" 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" 
-proof -
-  let "b <=_r ?map ++_f y" = ?thesis
-
-  assume "semilat (A, r, f)" "y \<in> A"
-  moreover
-  assume "\<forall>(p,s) \<in> set S. s \<in> A"
-  hence "set ?map \<subseteq> A" by auto
-  moreover
-  assume "(a,b) \<in> set S"
-  hence "b \<in> set ?map" by (induct S, auto)
-  ultimately
-  show ?thesis by - (rule ub1)
-qed
-    
- 
-
-lemma plusplus_empty:  
-  "\<forall>s'. (q, s') \<in> set S \<longrightarrow> s' +_f ss ! q = ss ! q \<Longrightarrow>
-   (map snd [(p', t')\<in> S. p' = q] ++_f ss ! q) = ss ! q"
-apply (induct S)
-apply auto 
-done
-
-
 lemma stable_pres_lemma:
   "\<lbrakk> semilat (A,r,f); pres_type step n A; bounded step n; 
      ss \<in> list n A; p \<in> w; \<forall>q\<in>w. q < n; 
@@ -435,23 +296,6 @@
  done
  
   
-lemma lesub_step_type:
-  "\<And>b x y. a <=|r| b \<Longrightarrow> (x,y) \<in> set a \<Longrightarrow> \<exists>y'. (x, y') \<in> set b \<and> y <=_r y'"
-apply (induct a)
- apply simp
-apply simp
-apply (case_tac b)
- apply simp
-apply simp
-apply (erule disjE)
- apply clarify
- apply (simp add: lesub_def)
- apply blast   
-apply clarify
-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; 
diff -r 75b2edff1af3 -r 4b1edf2f6bd2 src/HOL/MicroJava/BV/LBVCorrect.thy
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy	Mon Mar 18 11:47:03 2002 +0100
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy	Wed Mar 20 13:21:07 2002 +0100
@@ -6,288 +6,224 @@
 
 header {* \isaheader{Correctness of the LBV} *}
 
-(* This theory is currently broken. The port to exceptions
-  didn't make it into the Isabelle 2001 release. It is included for 
-  documentation only. See Isabelle 99-2 for a working copy of this
-  theory. *)
-
-
-theory LBVCorrect = BVSpec + LBVSpec:
-
-lemmas [simp del] = split_paired_Ex split_paired_All
+theory LBVCorrect = LBVSpec + Typing_Framework:
 
 constdefs
-fits :: "[method_type,instr list,jvm_prog,ty,state_type option,nat,nat,exception_table,certificate] \<Rightarrow> bool"
-"fits phi is G rT s0 maxs maxr et cert == 
-  (\<forall>pc s1. pc < length is \<longrightarrow>
-    (wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s0 = OK s1 \<longrightarrow>
-    (case cert!pc of None   \<Rightarrow> phi!pc = s1
-                   | Some t \<Rightarrow> phi!pc = Some t)))"
+fits :: "'s option list \<Rightarrow> 's certificate \<Rightarrow> 's ebinop \<Rightarrow> 's ord \<Rightarrow> 
+         's steptype \<Rightarrow> 's option \<Rightarrow> 'a list \<Rightarrow> bool"
+"fits phi cert f r step s0 is \<equiv>
+  length phi = length is \<and>
+  (\<forall>pc s. pc < length is -->
+    (wtl_inst_list (take pc is) cert f r step 0 s0 = OK s \<longrightarrow>
+    (case cert!pc of None   => phi!pc = s
+                   | Some t => phi!pc = Some t)))"
 
-constdefs
-make_phi :: "[instr list,jvm_prog,ty,state_type option,nat,nat,exception_table,certificate] \<Rightarrow> method_type"
-"make_phi is G rT s0 maxs maxr et cert == 
+make_phi :: "'s certificate \<Rightarrow> 's ebinop \<Rightarrow> 's ord \<Rightarrow> 
+             's steptype \<Rightarrow> 's option \<Rightarrow> 'a list \<Rightarrow> 's option list"
+"make_phi cert f r step s0 is \<equiv> 
    map (\<lambda>pc. case cert!pc of 
-               None   \<Rightarrow> ok_val (wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s0) 
-             | Some t \<Rightarrow> Some t) [0..length is(]"
-
+               None   => ok_val (wtl_inst_list (take pc is) cert f r step 0 s0)
+             | Some t => Some t) [0..length is(]"
 
-lemma fitsD_None:
-  "\<lbrakk>fits phi is G rT s0 mxs mxr et cert; pc < length is;
-    wtl_inst_list (take pc is) G rT cert mxs mxr (length is) et 0 s0 = OK s1; 
-    cert ! pc = None\<rbrakk> \<Longrightarrow> phi!pc = s1"
+lemma fitsD_None [intro?]:
+  "\<lbrakk> fits phi cert f r step s0 is; pc < length is;
+     wtl_inst_list (take pc is) cert f r step 0 s0 = OK s; 
+     cert!pc = None \<rbrakk> \<Longrightarrow> phi!pc = s"
   by (auto simp add: fits_def)
 
-lemma fitsD_Some:
-  "\<lbrakk>fits phi is G rT s0 mxs mxr et cert; pc < length is;
-    wtl_inst_list (take pc is) G rT cert mxs mxr (length is) et 0 s0 = OK s1; 
-    cert ! pc = Some t\<rbrakk> \<Longrightarrow> phi!pc = Some t"
+lemma fitsD_Some [intro?]:
+  "\<lbrakk> fits phi cert f r step s0 is; pc < length is;
+     wtl_inst_list (take pc is) cert f r step 0 s0 = OK s; 
+     cert!pc = Some t \<rbrakk> \<Longrightarrow> phi!pc = Some t"
   by (auto simp add: fits_def)
 
 lemma make_phi_Some:
-  "\<lbrakk> pc < length is; cert!pc = Some t \<rbrakk> \<Longrightarrow> 
-  make_phi is G rT s0 mxs mxr et cert ! pc = Some t"
+  "pc < length is \<Longrightarrow> cert!pc = Some t \<Longrightarrow>
+  make_phi cert f r step s0 is ! pc = Some t"
   by (simp add: make_phi_def)
 
 lemma make_phi_None:
-  "\<lbrakk> pc < length is; cert!pc = None \<rbrakk> \<Longrightarrow> 
-  make_phi is G rT s0 mxs mxr et cert ! pc = 
-  ok_val (wtl_inst_list (take pc is) G rT cert mxs mxr (length is) et 0 s0)"
+  "pc < length is \<Longrightarrow> cert!pc = None \<Longrightarrow>
+  make_phi cert f r step s0 is ! pc = 
+  ok_val (wtl_inst_list (take pc is) cert f r step 0 s0)"
+  by (simp add: make_phi_def)
+
+lemma make_phi_len:
+  "length (make_phi cert f r step s0 is) = length is"
   by (simp add: make_phi_def)
 
 lemma exists_phi:
-  "\<exists>phi. fits phi is G rT s0 mxs mxr et cert"  
+  "\<exists>phi. fits phi cert f r step s0 is"
 proof - 
-  have "fits (make_phi is G rT s0 mxs mxr et cert) is G rT s0 mxs mxr et cert"
-    by (auto simp add: fits_def make_phi_Some make_phi_None 
+  have "fits (make_phi cert f r step s0 is) cert f r step s0 is"
+    by (auto simp add: fits_def make_phi_Some make_phi_None make_phi_len
              split: option.splits) 
   thus ?thesis by fast
 qed
   
-lemma fits_lemma1:
-  "\<lbrakk> wtl_inst_list is G rT cert mxs mxr (length is) et 0 s = OK s'; fits phi is G rT s mxs mxr et cert \<rbrakk>
+lemma fits_lemma1 [intro?]:
+  "\<lbrakk>wtl_inst_list is cert f r step 0 s \<noteq> Err; fits phi cert f r step s is\<rbrakk>
   \<Longrightarrow> \<forall>pc t. pc < length is \<longrightarrow> cert!pc = Some t \<longrightarrow> phi!pc = Some t"
 proof (intro strip)
   fix pc t 
-  assume "wtl_inst_list is G rT cert mxs mxr (length is) et 0 s = OK s'"
+  assume "wtl_inst_list is cert f r step 0 s \<noteq> Err"
   then obtain s'' where
-    "wtl_inst_list (take pc is) G rT cert mxs mxr (length is) et 0 s = OK s''"
+    "wtl_inst_list (take pc is) cert f r step 0 s = OK s''" 
     by (blast dest: wtl_take)
   moreover
-  assume "fits phi is G rT s mxs mxr et cert" 
-         "pc < length is" 
-         "cert ! pc = Some t"
+  assume "fits phi cert f r step s is"
+         "pc < length is" "cert ! pc = Some t"
   ultimately
   show "phi!pc = Some t" by (auto dest: fitsD_Some)
 qed
 
 
 lemma wtl_suc_pc:
- "\<lbrakk> wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err;
-     wtl_inst_list (take pc is) G rT cert mxs mxr (length is) et 0 s = OK s';
-     wtl_cert (is!pc) G rT s' cert mxs mxr (length is) et pc = OK s'';
-     fits phi is G rT s mxs mxr et cert; Suc pc < length is \<rbrakk> \<Longrightarrow>
-  G \<turnstile> s'' <=' phi ! Suc pc"
+  assumes
+    semi: "err_semilat (A,r,f)" and
+    all:  "wtl_inst_list is cert f r step 0 s0 \<noteq> Err" and
+    wtl:  "wtl_inst_list (take pc is) cert f r step 0 s0 = OK s'" and
+    cert: "wtl_cert cert f r step pc s' = OK s''" and
+    fits: "fits phi cert f r step s0 is" and
+    pc:   "pc+1 < length is"
+  shows "OK s'' \<le>|r OK (phi!(pc+1))"
 proof -
-  
-  assume all:  "wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err"
-  assume fits: "fits phi is G rT s mxs mxr et cert"
+  from wtl cert pc
+  have wts: "wtl_inst_list (take (pc+1) is) cert f r step 0 s0 = OK s''"
+    by (rule wtl_Suc)
+  moreover
+  from all pc
+  have "\<exists>s' s''. wtl_inst_list (take (pc+1) is) cert f r step 0 s0 = OK s' \<and> 
+                 wtl_cert cert f r step (pc+1) s' = OK s''"
+    by (rule wtl_all)
+  ultimately
+  obtain x where "wtl_cert cert f r step (pc+1) s'' = OK x" by auto
+  hence "\<And>t. cert!(pc+1) = Some t \<Longrightarrow> OK s'' \<le>|r OK (cert!(pc+1))"
+    by (simp add: wtl_cert_def split: split_if_asm)
+  also from fits pc wts
+  have "\<And>t. cert!(pc+1) = Some t \<Longrightarrow> cert!(pc+1) = phi!(pc+1)"
+    by (auto dest!: fitsD_Some)
+  finally have "\<And>t. cert!(pc+1) = Some t \<Longrightarrow> OK s'' \<le>|r OK (phi!(pc+1))" .
+  moreover
+  from fits pc wts have "cert!(pc+1) = None \<Longrightarrow> s'' = phi!(pc+1)"
+    by (rule fitsD_None [symmetric])
+  with semi have "cert!(pc+1) = None \<Longrightarrow> OK s'' \<le>|r OK (phi!(pc+1))" by simp
+  ultimately
+  show "OK s'' \<le>|r OK (phi!(pc+1))" by (cases "cert!(pc+1)", blast+)
+qed    
 
-  assume wtl:  "wtl_inst_list (take pc is) G rT cert mxs mxr (length is) et 0 s = OK s'" and
-         wtc:  "wtl_cert (is!pc) G rT s' cert mxs mxr (length is) et pc = OK s''" and
-         pc:   "Suc pc < length is"
-
-  hence wts: 
-    "wtl_inst_list (take (Suc pc) is) G rT cert mxs mxr (length is) et 0 s = OK s''"
-    by (rule wtl_Suc)
-
-  from all
-  have app: 
-  "wtl_inst_list (take (Suc pc) is@drop (Suc pc) is) G rT cert mxs mxr (length is) et 0 s \<noteq> Err"
-    by simp
+lemma wtl_stable:
+  assumes
+    semi:    "err_semilat (A,r,f)" and
+    pres:    "pres_type step (length is) (err (opt A))" and
+    s0_in_A: "s0 \<in> opt A" and
+    cert_ok: "cert_ok cert (length is) A" and
+    fits:    "fits phi cert f r step s0 is"  and
+    wtl:     "wtl_inst_list is cert f r step 0 s0 \<noteq> Err" and
+    pc:      "pc < length is" and
+    bounded: "bounded step (length is)"
+  shows "stable (Err.le (Opt.le r)) step (map OK phi) pc"
+proof (unfold stable_def, clarify)
+  fix pc' s' assume step: "(pc',s') \<in> set (step pc ((map OK phi) ! pc))" 
+                      (is "(pc',s') \<in> set (?step pc)")
+  
+  from step pc bounded have pc': "pc' < length is"
+    by (unfold bounded_def) blast
+  
+  from wtl pc obtain s1 s2 where
+    tkpc: "wtl_inst_list (take pc is) cert f r step 0 s0 = OK s1" and
+    cert: "wtl_cert cert f r step pc s1 = OK s2" 
+    by - (drule wtl_all, auto)
 
-  from pc 
-  have "0 < length (drop (Suc pc) is)" 
-    by simp
-  then obtain l ls where
-    "drop (Suc pc) is = l#ls"
-    by (auto simp add: neq_Nil_conv simp del: length_drop)
-  with app wts pc
-  obtain x where 
-    "wtl_cert l G rT s'' cert mxs mxr (length is) et (Suc pc) = OK x"
-    by (auto simp add: wtl_append min_def simp del: append_take_drop_id)
+  have c_Some: "\<forall>pc t. pc < length is \<longrightarrow> cert!pc = Some t \<longrightarrow> phi!pc = Some t" ..
+  have c_None: "cert!pc = None \<Longrightarrow> phi!pc = s1" ..
+
+  from cert pc c_None c_Some 
+  have inst: "wtl_inst cert f r step pc (phi!pc) = OK s2"
+    by (simp add: wtl_cert_def split: option.splits split_if_asm)
+  
+  from semi have "order (Err.le (Opt.le r))" by simp note order_trans [OF this, trans]
+  
+  from pc fits have [simp]: "map OK phi!pc = OK (phi!pc)" by (simp add: fits_def)
+  from pc' fits have [simp]: "map OK phi!pc' = OK (phi!pc')" by (simp add: fits_def)
+
+  have "s1 \<in> opt A" by (rule wtl_inst_list_pres)
+  with pc c_Some cert_ok c_None
+  have "phi!pc \<in> opt A" by (cases "cert!pc") (auto dest: cert_okD)
+  with pc pres
+  have step_in_A: "\<forall>(pc',s') \<in> set (?step pc). s' \<in> err (opt A)" 
+    by (auto dest: pres_typeD)
 
-  hence c1: "\<And>t. cert!Suc pc = Some t \<Longrightarrow> G \<turnstile> s'' <=' cert!Suc pc"
-    by (simp add: wtl_cert_def split: split_if_asm)
-  moreover
-  from fits pc wts
-  have c2: "\<And>t. cert!Suc pc = Some t \<Longrightarrow> phi!Suc pc = cert!Suc pc"
-    by - (drule fitsD_Some, auto)
-  moreover
-  from fits pc wts
-  have c3: "cert!Suc pc = None \<Longrightarrow> phi!Suc pc = s''"
-    by (rule fitsD_None)
-  ultimately
-  show ?thesis by (cases "cert!Suc pc", auto)
+  show "s' \<le>|r (map OK phi) ! pc'"
+  proof (cases "pc' = pc+1")
+    case True
+    with pc' cert_ok
+    have cert_in_A: "OK (cert!(pc+1)) \<in> err (opt A)" by (auto dest: cert_okD)
+    from inst 
+    have ok: "OK s2 = merge cert f r pc (?step pc) (OK (cert!(pc+1)))" 
+      by (simp add: wtl_inst_def)
+    also    
+    have "\<dots> = (map snd [(p',t')\<in>?step pc. p'=pc+1] ++|f (OK (cert!(pc+1))))"
+      using cert_in_A step_in_A semi ok
+      by - (drule merge_def, auto split: split_if_asm)
+    finally
+    have "s' \<le>|r OK s2" 
+      using semi step_in_A cert_in_A True step by (auto intro: ub1')
+    also 
+    from True pc' have "pc+1 < length is" by simp
+    with semi wtl tkpc cert fits
+    have "OK s2 \<le>|r (OK (phi ! (pc+1)))" by (rule wtl_suc_pc)
+    also note True [symmetric]
+    finally show ?thesis by simp
+  next
+    case False
+    from inst 
+    have "\<forall>(pc', s')\<in>set (?step pc). pc'\<noteq>pc+1 \<longrightarrow> s' \<le>|r OK (cert!pc')"
+      by (unfold wtl_inst_def) (rule merge_ok, simp)
+    with step False 
+    have ok: "s' \<le>|r (OK (cert!pc'))" by blast
+    moreover
+    from ok
+    have "cert!pc' = None \<longrightarrow> s' = OK None" by auto
+    moreover
+    from c_Some pc'
+    have "cert!pc' \<noteq> None \<longrightarrow> phi!pc' = cert!pc'" by auto
+    ultimately
+    show ?thesis by auto
+  qed
 qed
 
 
-lemma wtl_fits_wt:
-  "\<lbrakk> wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err; 
-      fits phi is G rT s mxs mxr et cert; pc < length is \<rbrakk> \<Longrightarrow>
-   wt_instr (is!pc) G rT phi mxs (length is) et pc"
-proof -
-  assume fits: "fits phi is G rT s mxs mxr et cert"
-  assume pc:  "pc < length is" and
-         wtl: "wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err"        
-  then obtain s' s'' where
-    w: "wtl_inst_list (take pc is) G rT cert mxs mxr (length is) et 0 s = OK s'" and
-    c: "wtl_cert (is!pc) G rT s' cert mxs mxr (length is) et pc = OK s''"
-    by - (drule wtl_all, auto)
-
-  from fits wtl pc have cert_Some: 
-    "\<And>t pc. \<lbrakk> pc < length is; cert!pc = Some t \<rbrakk> \<Longrightarrow> phi!pc = Some t"
-    by (auto dest: fits_lemma1)
-  
-  from fits wtl pc have cert_None: "cert!pc = None \<Longrightarrow> phi!pc = s'"
-    by - (drule fitsD_None)
-  
-  from pc c cert_None cert_Some
-  have wti: "wtl_inst (is ! pc) G rT (phi!pc) cert mxs mxr (length is) et pc = OK s''"
-    by (auto simp add: wtl_cert_def split: split_if_asm option.splits)
-
-  -- "we now must show that @{text wt_instr} holds; the definition 
-      of @{text wt_instr} is: @{thm [display] wt_instr_def[no_vars]}"
-
-  { fix pc' r
-    assume pc': "(pc',r) \<in> set (eff (is!pc) G pc et (phi!pc))"
+lemma wtl_fits:
+  "wtl_inst_list is cert f r step 0 s0 \<noteq> Err \<Longrightarrow>
+  fits phi cert f r step s0 is \<Longrightarrow>
+  err_semilat (A,r,f) \<Longrightarrow>
+  bounded step (length is) \<Longrightarrow>
+  pres_type step (length is) (err (opt A)) \<Longrightarrow>
+  s0 \<in> opt A \<Longrightarrow>
+  cert_ok cert (length is) A \<Longrightarrow>
+  wt_step (Err.le (Opt.le r)) Err step (map OK phi)"
+  apply (unfold wt_step_def)
+  apply (intro strip)
+  apply (rule conjI, simp)
+  apply (rule wtl_stable)
+  apply assumption+
+  apply (simp add: fits_def)
+  apply assumption
+  done
 
-    with wti have less: "pc' < length is" by (simp add: wtl_inst_OK) blast
-
-    have "G \<turnstile> r <=' phi ! pc'" 
-    proof (cases "pc' = Suc pc")
-      case False          
-      with wti pc'
-      have G: "G \<turnstile> r <=' cert ! pc'" by (simp add: wtl_inst_OK) blast
-      hence "cert!pc' = None \<Longrightarrow> r = None" by simp
-      hence "cert!pc' = None \<Longrightarrow> ?thesis" by simp
-      moreover {
-        fix t assume "cert!pc' = Some t"
-        with less have "phi!pc' = cert!pc'" by (simp add: cert_Some)
-        with G have ?thesis by simp
-      }
-      ultimately show ?thesis by blast      
-    next
-      case True
-      with pc' wti
-      have "G \<turnstile> r <=' s''"  sorry
-      also
-      from wtl w fits c pc 
-      have "Suc pc < length is \<Longrightarrow> G \<turnstile> s'' <=' phi ! Suc pc" 
-        by - (rule wtl_suc_pc)
-      with True less
-      have "G \<turnstile> s'' <=' phi ! Suc pc" by blast
-      finally show ?thesis by (simp add: True)
-    qed
-  }  
-  with wti show ?thesis
-    by (auto simp add: wtl_inst_OK wt_instr_def)
+  
+theorem wtl_sound:
+  assumes "wtl_inst_list is cert f r step 0 s0 \<noteq> Err" 
+  assumes "err_semilat (A,r,f)" and "bounded step (length is)"
+  assumes "s0 \<in> opt A" and "cert_ok cert (length is) A"
+  assumes "pres_type step (length is) (err (opt A))"
+  shows "\<exists>ts. wt_step (Err.le (Opt.le r)) Err step ts"
+proof -
+  obtain phi where "fits phi cert f r step s0 is" by (insert exists_phi) fast
+  have "wt_step (Err.le (Opt.le r)) Err step (map OK phi)" by (rule wtl_fits)
+  thus ?thesis ..
 qed
 
 
-    
-lemma fits_first:
-  "\<lbrakk> 0 < length is; wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err; 
-      fits phi is G rT s mxs mxr et cert \<rbrakk> \<Longrightarrow> 
-  G \<turnstile> s <=' phi ! 0"
-proof -
-  assume wtl:  "wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err"
-  assume fits: "fits phi is G rT s mxs mxr et cert"
-  assume pc:   "0 < length is"
-
-  from wtl
-  have wt0: "wtl_inst_list (take 0 is) G rT cert mxs mxr (length is) et 0 s = OK s"
-    by simp
-  
-  with fits pc
-  have "cert!0 = None \<Longrightarrow> phi!0 = s"
-    by (rule fitsD_None)
-  moreover    
-  from fits pc wt0
-  have "\<And>t. cert!0 = Some t \<Longrightarrow> phi!0 = cert!0"
-    by - (drule fitsD_Some, auto)
-  moreover
-  from pc
-  obtain x xs where "is = x#xs" 
-    by (auto simp add: neq_Nil_conv)
-  with wtl
-  obtain s' where
-    "wtl_cert x G rT s cert mxs mxr (length is) et 0 = OK s'"
-    by auto
-  hence 
-    "\<And>t. cert!0 = Some t \<Longrightarrow> G \<turnstile> s <=' cert!0"
-    by (simp add: wtl_cert_def split: split_if_asm)
-
-  ultimately
-  show ?thesis
-    by (cases "cert!0") auto
-qed
-
-  
-lemma wtl_method_correct:
-"wtl_method G C pTs rT mxs mxl et ins cert \<Longrightarrow> \<exists> phi. wt_method G C pTs rT mxs mxl ins et phi"
-proof (unfold wtl_method_def, simp only: Let_def, elim conjE)
-  let "?s0" = "Some ([], OK (Class C) # map OK pTs @ replicate mxl Err)"
-  assume pc:  "0 < length ins"
-  assume wtl: "wtl_inst_list ins G rT cert mxs mxl (length ins) et 0 ?s0 \<noteq> Err"
-
-  obtain phi where fits: "fits phi ins G rT ?s0 mxs mxl et cert"    
-    by (rule exists_phi [elim_format]) blast
-
-  with wtl
-  have allpc:
-    "\<forall>pc. pc < length ins \<longrightarrow> wt_instr (ins ! pc) G rT phi mxs (length ins) et pc"
-    by (blast intro: wtl_fits_wt)
-
-  from pc wtl fits
-  have "wt_start G C pTs mxl phi"
-    by (unfold wt_start_def) (rule fits_first)
-
-  with pc allpc 
-  show ?thesis by (auto simp add: wt_method_def)
-qed
-
-
-theorem wtl_correct:
-  "wtl_jvm_prog G cert \<Longrightarrow> \<exists> Phi. wt_jvm_prog G Phi"
-proof -  
-  assume wtl: "wtl_jvm_prog G cert"
-
-  let ?Phi = "\<lambda>C sig. let (C,rT,(maxs,maxl,ins,et)) = the (method (G,C) sig) in 
-              SOME phi. wt_method G C (snd sig) rT maxs maxl ins et phi"
-   
-  { fix C S fs mdecls sig rT code
-    assume "(C,S,fs,mdecls) \<in> set G" "(sig,rT,code) \<in> set mdecls"
-    moreover
-    from wtl obtain wf_mb where "wf_prog wf_mb G" 
-      by (auto simp add: wtl_jvm_prog_def)
-    ultimately
-    have "method (G,C) sig = Some (C,rT,code)"
-      by (simp add: methd)
-  } note this [simp]
- 
-  from wtl
-  have "wt_jvm_prog G ?Phi"
-    apply (clarsimp simp add: wt_jvm_prog_def wtl_jvm_prog_def wf_prog_def wf_cdecl_def)
-    apply (drule bspec, assumption)
-    apply (clarsimp simp add: wf_mdecl_def)
-    apply (drule bspec, assumption)
-    apply (clarsimp dest!: wtl_method_correct)
-    apply (rule someI, assumption)
-    done
-
-  thus ?thesis
-    by blast
-qed   
-      
 end
diff -r 75b2edff1af3 -r 4b1edf2f6bd2 src/HOL/MicroJava/BV/LBVSpec.thy
--- a/src/HOL/MicroJava/BV/LBVSpec.thy	Mon Mar 18 11:47:03 2002 +0100
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy	Wed Mar 20 13:21:07 2002 +0100
@@ -6,154 +6,215 @@
 
 header {* \isaheader{The Lightweight Bytecode Verifier} *}
 
-theory LBVSpec = Effect + Kildall:
+theory LBVSpec = SemilatAlg + Opt:
+
+
+syntax
+  "@lesuberropt" :: "'a option err \<Rightarrow> 'a ord \<Rightarrow> 'a option err \<Rightarrow> 'a option err ord"
+  ("_ \<le>|_ _" [50,50,51] 50) 
 
-text {* 
-  The Lightweight Bytecode Verifier with exceptions has not 
-  made it completely into the Isabelle 2001 release. Currently 
-  there is only the specification itself available. The proofs of
-  soundness and completeness are broken (they still need to be
-  ported to the exception version). Both theories are included
-  for documentation (but they don't work for this specification), 
-  please see the Isabelle 99-2 release for a working copy, or
-  \url{http://isabelle.in.tum.de/verificard} for the most recent
-  development of \mJava.
-*}
+  "@superropt" :: "'a option err \<Rightarrow> 'a ebinop \<Rightarrow> 'a option err \<Rightarrow> 'a option err binop"
+  ("_ +|_ _" [50,50,51] 50)
+  
+  "@supsuperropt" :: "'a option err list \<Rightarrow> 'a ebinop \<Rightarrow> 'a option err \<Rightarrow> 'a option err binop"
+  ("_ ++|_ _" [50,50,51] 50)
+
+translations
+  "a \<le>|r b" == "a <=_(Err.le (Opt.le r)) b"  
+  "a +|f b" == "a +_(Err.lift2 (Opt.sup f)) b"
+  "a ++|f b" == "a ++_(Err.lift2 (Opt.sup f)) b"
+
 
 types
-  certificate       = "state_type option list" 
-  class_certificate = "sig \<Rightarrow> certificate"
-  prog_certificate  = "cname \<Rightarrow> class_certificate"
+  's certificate = "'s option list"   
+  's steptype    = "'s option err step_type"
 
 consts
-  merge :: "[jvm_prog, p_count, nat, nat, p_count, certificate, (nat \<times> (state_type option)) list, state] \<Rightarrow> state"
+merge :: "'s certificate \<Rightarrow> 's ebinop \<Rightarrow> 's ord \<Rightarrow> nat \<Rightarrow> 
+          (nat \<times> 's option err) list \<Rightarrow> 's option err \<Rightarrow> 's option err"
 primrec
-  "merge G pc mxs mxr max_pc cert []     x = x"
-  "merge G pc mxs mxr max_pc cert (s#ss) x = (let (pc',s') = s in 
-                                       if pc' < max_pc \<and> pc' = pc+1 then 
-                                         merge G pc mxs mxr max_pc cert ss (OK s' +_(sup G mxs mxr) x) 
-                                       else if pc' < max_pc \<and> G \<turnstile> s' <=' cert!pc' then 
-                                         merge G pc mxs mxr max_pc cert ss x
-                                       else Err)"
+"merge cert f r pc []     x = x"
+"merge cert f r pc (s#ss) x = (let (pc',s') = s in
+                               merge cert f r pc ss (if pc'=pc+1 then (s' +|f x)
+                                                     else if s' \<le>|r (OK (cert!pc')) then x
+                                                     else Err))"
 
-constdefs 
-  wtl_inst :: "[instr,jvm_prog,ty,state_type option,certificate,nat,nat,p_count,exception_table,p_count] 
-               \<Rightarrow> state_type option err" 
-  "wtl_inst i G rT s cert maxs maxr max_pc et pc == 
-     if app i G maxs rT pc et s then 
-       merge G pc maxs maxr max_pc cert (eff i G pc et s) (OK (cert!(pc+1)))
-     else Err"
+constdefs
+wtl_inst :: "'s certificate \<Rightarrow> 's ebinop \<Rightarrow> 's ord \<Rightarrow> 
+             's steptype \<Rightarrow> nat \<Rightarrow> 's option \<Rightarrow> 's option err"
+"wtl_inst cert f r step pc s \<equiv> merge cert f r pc (step pc (OK s)) (OK (cert!(pc+1)))"
 
-  wtl_cert :: "[instr,jvm_prog,ty,state_type option,certificate,nat,nat,p_count,exception_table,p_count] 
-               \<Rightarrow> state_type option err"  
-  "wtl_cert i G rT s cert maxs maxr max_pc et pc ==
-     case cert!pc of
-        None    \<Rightarrow> wtl_inst i G rT s cert maxs maxr max_pc et pc
-      | Some s' \<Rightarrow> if G \<turnstile> s <=' (Some s') then 
-                    wtl_inst i G rT (Some s') cert maxs maxr max_pc et pc 
-                  else Err"
+wtl_cert :: "'s certificate \<Rightarrow> 's ebinop \<Rightarrow> 's ord \<Rightarrow> 
+             's steptype \<Rightarrow> nat \<Rightarrow> 's option \<Rightarrow> 's option err"
+"wtl_cert cert f r step pc s \<equiv>
+  case cert!pc of 
+    None    \<Rightarrow> wtl_inst cert f r step pc s
+  | Some s' \<Rightarrow> if OK s \<le>|r (OK (Some s')) then wtl_inst cert f r step pc (Some s') else Err"
 
 consts 
-  wtl_inst_list :: "[instr list,jvm_prog,ty,certificate,nat,nat,p_count,exception_table,p_count,
-                     state_type option] \<Rightarrow> state_type option err"
+wtl_inst_list :: "'a list \<Rightarrow> 's certificate \<Rightarrow> 's ebinop \<Rightarrow> 's ord \<Rightarrow> 
+                  's steptype \<Rightarrow> nat \<Rightarrow> 's option \<Rightarrow> 's option err"
 primrec
-  "wtl_inst_list []     G rT cert maxs maxr max_pc et pc s = OK s"
-  "wtl_inst_list (i#is) G rT cert maxs maxr max_pc et pc s = 
-    (let s' = wtl_cert i G rT s cert maxs maxr max_pc et pc in
-     strict (wtl_inst_list is G rT cert maxs maxr max_pc et (pc+1)) s')"
-              
+"wtl_inst_list []      cert f r step pc s = OK s"
+"wtl_inst_list (i#ins) cert f r step pc s = 
+  (let s' = wtl_cert cert f r step pc s in
+   strict (wtl_inst_list ins cert f r step (pc+1)) s')"
+
+
 
 constdefs
- wtl_method :: "[jvm_prog,cname,ty list,ty,nat,nat,exception_table,instr list,certificate] \<Rightarrow> bool"  
- "wtl_method G C pTs rT mxs mxl et ins cert ==  
-	let max_pc = length ins  
-  in 
-  0 < max_pc \<and>   
-  wtl_inst_list ins G rT cert mxs mxl max_pc et 0 
-                (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err))) \<noteq> Err"
+  cert_ok :: "'s certificate \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool"
+  "cert_ok cert n A \<equiv> \<forall>i < n. cert!i \<in> opt A"
+
+lemma cert_okD:
+  "cert_ok cert n A \<Longrightarrow> pc < n \<Longrightarrow> cert!pc \<in> opt A"
+  by (unfold cert_ok_def) fast
+
+
+declare Let_def [simp]
+
+section "more semilattice lemmas"
+
+(*
+lemma sup_top [simp]:
+  assumes sl:  "semilat (A,r,f)" 
+  assumes set: "x \<in> A"  "t \<in> A"  
+  assumes top: "top r t" 
+  shows "x +_f t = t"
+proof -
+  from sl have "order r" ..
+  moreover from top have "x +_f t <=_r t" ..
+  moreover from sl set have "t <=_r x +_f t" by simp 
+  ultimately show ?thesis by (rule order_antisym)
+qed
+  
+lemma plusplussup_top:
+  "semilat (A,r,f) \<Longrightarrow> top r Err \<Longrightarrow> set xs \<subseteq> A \<Longrightarrow> Err \<in> A \<Longrightarrow> xs ++_f Err = Err"
+  by (induct xs) auto
+*)
+
+lemma err_semilatDorderI [simp, intro]:
+  "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 assumption
+  done
+
+lemma err_opt_semilat [simp,elim]:
+  "err_semilat (A,r,f) \<Longrightarrow> semilat (err (opt A), Err.le (Opt.le r), lift2 (Opt.sup f))"
+proof -
+  assume "err_semilat (A,r,f)"
+  hence "err_semilat (Opt.esl (A,r,f))" ..
+  thus ?thesis by (simp add: Err.sl_def Opt.esl_def)
+qed
+
+lemma plusplus_erropt_Err [simp]:
+  "xs ++|f Err = Err"
+  by (induct xs) auto
+
+
+section "merge"
+
+lemma merge_Err [simp]:
+  "merge cert f r pc ss Err = Err"
+  by (induct ss) auto
 
- wtl_jvm_prog :: "[jvm_prog,prog_certificate] \<Rightarrow> bool" 
- "wtl_jvm_prog G cert ==  
-  wf_prog (\<lambda>G C (sig,rT,maxs,maxl,b,et). wtl_method G C (snd sig) rT maxs maxl et b (cert C sig)) G"
+lemma merge_ok:
+  "\<And>x. merge cert f r pc ss x = OK s \<Longrightarrow> 
+  \<forall>(pc',s') \<in> set ss. (pc' \<noteq> pc+1 \<longrightarrow> s' \<le>|r (OK (cert!pc')))"
+  (is "\<And>x. ?merge ss x \<Longrightarrow> ?P ss")
+proof (induct ss)
+  show "?P []" by simp
+next
+  fix x l ls assume merge: "?merge (l#ls) x"
+  moreover
+  obtain pc' s' where [simp]: "l = (pc',s')" by (cases l)
+  ultimately
+  obtain x' where "?merge ls x'" by simp  
+  assume "\<And>x. ?merge ls x \<Longrightarrow> ?P ls" hence "?P ls" .
+  moreover
+  from merge
+  have "pc' \<noteq> pc+1 \<longrightarrow> s' \<le>|r (OK (cert!pc'))" by (simp split: split_if_asm)
+  ultimately
+  show "?P (l#ls)" by simp
+qed
+
 
+lemma merge_def:
+  assumes semi: "err_semilat (A,r,f)" 
+  shows 
+  "\<And>x. x \<in> err (opt A) \<Longrightarrow> \<forall>(pc', s') \<in> set ss. s' \<in> err (opt A) \<Longrightarrow>
+  merge cert f r pc ss x = 
+  (if \<forall>(pc',s') \<in> set ss. (pc' \<noteq> pc+1 \<longrightarrow> s' \<le>|r (OK (cert!pc'))) then
+    map snd [(p',t') \<in> ss. p'=pc+1] ++|f x
+  else Err)" 
+  (is "\<And>x. _ \<Longrightarrow> _ \<Longrightarrow> ?merge ss x = ?if ss x" is "\<And>x. _ \<Longrightarrow> _ \<Longrightarrow> ?P ss x")
+proof (induct ss)
+  fix x show "?P [] x" by simp
+next 
+  fix x assume x: "x \<in> err (opt A)" 
+  fix l::"nat \<times> 'a option err" and ls  
+  assume "\<forall>(pc', s') \<in> set (l#ls). s' \<in> err (opt A)"
+  then obtain l: "snd l \<in> err (opt A)" and ls: "\<forall>(pc', s') \<in> set ls. s' \<in> err (opt A)" by auto
+  assume "\<And>x. x \<in> err (opt A) \<Longrightarrow> \<forall>(pc',s') \<in> set ls. s' \<in> err (opt A) \<Longrightarrow> ?P ls x" 
+  hence IH: "\<And>x. x \<in> err (opt A) \<Longrightarrow> ?P ls x" .
+  obtain pc' s' where [simp]: "l = (pc',s')" by (cases l)
+  hence "?merge (l#ls) x = ?merge ls 
+    (if pc'=pc+1 then s' +|f x else if s' \<le>|r (OK (cert!pc')) then x else Err)"
+    (is "?merge (l#ls) x = ?merge ls ?if'")
+    by simp 
+  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 have "?if' \<in> err (opt A)" by auto
+    hence "?P ls ?if'" by (rule IH) thus ?thesis by simp
+  qed
+  also have "\<dots> = ?if (l#ls) x"
+    proof (cases "\<forall>(pc', s')\<in>set (l#ls). pc' \<noteq> pc + 1 \<longrightarrow> s' \<le>|r OK (cert ! pc')")
+      case True
+      hence "\<forall>(pc', s')\<in>set ls. pc' \<noteq> pc + 1 \<longrightarrow> s' \<le>|r (OK (cert ! pc'))" by auto
+      moreover
+      from True have 
+        "map snd [(p',t')\<in>ls . p'=pc+1] ++|f ?if' = 
+        (map snd [(p',t')\<in>l#ls . p'=pc+1] ++|f x)"
+        by simp
+      ultimately
+      show ?thesis using True by simp
+    next
+      case False thus ?thesis by auto
+    qed
+  finally show "?P (l#ls) x" .
+qed
+
+lemma merge_ok_s:
+  assumes sl: "err_semilat (A,r,f)" 
+  assumes x:  "x \<in> err (opt A)"
+  assumes ss: "\<forall>(pc', s') \<in> set ss. s' \<in> err (opt A)"
+  assumes m:  "merge cert f r pc ss x = OK s"
+  shows "merge cert f r pc ss x = (map snd [(p',t') \<in> ss. p'=pc+1] ++|f x)"
+proof -
+  from m have "\<forall>(pc',s') \<in> set ss. (pc' \<noteq> pc+1 \<longrightarrow> s' \<le>|r (OK (cert!pc')))" 
+    by (rule merge_ok)
+  with sl x ss m show ?thesis by - (drule merge_def, auto split: split_if_asm)
+qed
+
+section "wtl-inst-list"
 
 lemmas [iff] = not_Err_eq
 
-lemma if_eq_cases:
-  "(P \<Longrightarrow> x = z) \<Longrightarrow> (\<not>P \<Longrightarrow> y = z) \<Longrightarrow> (if P then x else y) = z"
-  by simp
-
-lemma merge_def:
-  "\<And>x. merge G pc mxs mxr max_pc cert ss x = 
-  (if \<forall>(pc',s') \<in> set ss. pc' < max_pc \<and> (pc' \<noteq> pc+1 \<longrightarrow> G \<turnstile> s' <=' cert!pc') then
-    map (OK \<circ> snd) [(p',t') \<in> ss. p'=pc+1] ++_(sup G mxs mxr) x
-  else Err)" (is "\<And>x. ?merge ss x = ?if ss x" is "\<And>x. ?P ss x")
-proof (induct ss)
-  show "\<And>x. ?P [] x" by simp
-next
-  have OK_snd: "(\<lambda>u. OK (snd u)) = OK \<circ> snd" by (rule ext) auto
-  fix x ss and s::"nat \<times> (state_type option)"
-  assume IH: "\<And>x. ?P ss x"
-  obtain pc' s' where s: "s = (pc',s')" by (cases s)  
-  hence "?merge (s#ss) x = ?merge ((pc',s')#ss) x" by hypsubst (rule refl)
-  also
-  have "\<dots> = (if pc' < max_pc \<and> pc' = pc+1 then 
-               ?merge ss (OK s' +_(sup G mxs mxr) x)
-             else if pc' < max_pc \<and> G \<turnstile> s' <=' cert!pc' then 
-               ?merge ss x
-             else Err)" 
-    (is "_ = (if ?pc' then ?merge ss (_ +_?f _) else if ?G then _ else _)")
-    by simp 
-  also 
-  let "if ?all ss then _ else _" = "?if ss x"    
-  have "\<dots> = ?if ((pc',s')#ss) x"
-  proof (cases "?pc'")    
-    case True
-    hence "?all (((pc',s')#ss)) = (pc+1 < max_pc \<and> ?all ss)" by simp
-    with True
-    have "?if ss (OK s' +_?f x) = ?if ((pc',s')#ss) x" by (auto simp add: OK_snd)
-    hence "?merge ss (OK s' +_?f x) = ?if ((pc',s')#ss) x" by (simp only: IH)
-    with True show ?thesis by (fast intro: if_eq_cases)
-  next
-    case False
-    have "(if ?G then ?merge ss x else Err) = ?if ((pc',s')#ss) x" 
-    proof (cases ?G)
-      assume G: ?G with False
-      have "?if ss x = ?if ((pc',s')#ss) x" by (auto simp add: OK_snd)
-      hence "?merge ss x = ?if ((pc',s')#ss) x" by (simp only: IH)
-      with G show ?thesis by (fast intro: if_eq_cases)
-    next
-      assume G: "\<not>?G"
-      with False have "Err = ?if ((pc',s')#ss) x" by auto
-      with G show ?thesis by (fast intro: if_eq_cases)
-    qed
-    with False show ?thesis by (fast intro: if_eq_cases)
-  qed
-  also from s have "\<dots> = ?if (s#ss) x" by hypsubst (rule refl)
-  finally show "?P (s#ss) x" .
-qed
-  
-
-lemma wtl_inst_OK:
-"(wtl_inst i G rT s cert mxs mxr max_pc et pc = OK s') = (
- app i G mxs rT pc et s \<and> 
-  (\<forall>(pc',r) \<in> set (eff i G pc et s). 
-  pc' < max_pc \<and> (pc' \<noteq> pc+1 \<longrightarrow> G \<turnstile> r <=' cert!pc')) \<and> 
-  map (OK \<circ> snd) [(p',t') \<in> (eff i G pc et s). p'=pc+1] 
-  ++_(sup G mxs mxr) (OK (cert!(pc+1))) = OK s')"
-  by (auto simp add: wtl_inst_def merge_def split: split_if_asm)
-
 lemma wtl_Cons:
-  "wtl_inst_list (i#is) G rT cert maxs maxr max_pc et pc s \<noteq> Err = 
-  (\<exists>s'. wtl_cert i G rT s cert maxs maxr max_pc et pc = OK s' \<and> 
-        wtl_inst_list is G rT cert maxs maxr max_pc et (pc+1) s' \<noteq> Err)"
+  "wtl_inst_list (i#is) cert f r step pc s \<noteq> Err = 
+  (\<exists>s'. wtl_cert cert f r step pc s = OK s' \<and> 
+        wtl_inst_list is cert f r step (pc+1) s' \<noteq> Err)"
   by (auto simp del: split_paired_Ex)
 
 lemma wtl_append:
-"\<forall> s pc. (wtl_inst_list (a@b) G rT cert mxs mxr mpc et pc s = OK s') =
-   (\<exists>s''. wtl_inst_list a G rT cert mxs mxr mpc et pc s = OK s'' \<and> 
-          wtl_inst_list b G rT cert mxs mxr mpc et (pc+length a) s'' = OK s')" 
-  (is "\<forall> s pc. ?C s pc a" is "?P a")
+"\<forall>s pc. (wtl_inst_list (a@b) cert f r step pc s = OK s') =
+   (\<exists>s''. wtl_inst_list a cert f r step pc s = OK s'' \<and> 
+          wtl_inst_list b cert f r step (pc+length a) s'' = OK s')" 
+  (is "\<forall>s pc. ?C s pc a" is "?P a")
 proof (induct ?P a)
   show "?P []" by simp
 next
@@ -162,28 +223,28 @@
   proof (intro allI)
     fix s pc 
     show "?C s pc (x#xs)"
-    proof (cases "wtl_cert x G rT s cert mxs mxr mpc et pc")
+    proof (cases "wtl_cert cert f r step pc s")
       case Err thus ?thesis by simp
     next
-      fix s0 assume "wtl_cert x G rT s cert mxs mxr mpc et pc = OK s0"      
-      with IH have "?C s0 (Suc pc) xs" by blast
+      case (OK s0)
+      with IH have "?C s0 (pc+1) xs" by blast
       thus ?thesis by (simp!)
     qed
   qed
 qed
 
 lemma wtl_take:
-  "wtl_inst_list is G rT cert mxs mxr mpc et pc s = OK s'' \<Longrightarrow>
-   \<exists>s'. wtl_inst_list (take pc' is) G rT cert mxs mxr mpc et pc s = OK s'"
+  "wtl_inst_list is cert f r step pc s = OK s'' \<Longrightarrow>
+   \<exists>s'. wtl_inst_list (take pc' is) cert f r step pc s = OK s'"
+  (is "?wtl is = _ \<Longrightarrow> _")
 proof -
-  assume "wtl_inst_list is G rT cert mxs mxr mpc et pc s = OK s''"
-  hence "wtl_inst_list (take pc' is @ drop pc' is) G rT cert mxs mxr mpc et pc s = OK s''"
-    by simp
+  assume "?wtl is = OK s''"
+  hence "?wtl (take pc' is @ drop pc' is) = OK s''" by simp
   thus ?thesis by (auto simp add: wtl_append simp del: append_take_drop_id)
 qed
 
 lemma take_Suc:
-  "\<forall>n. n < length l \<longrightarrow> take (Suc n) l = (take n l)@[l!n]" (is "?P l")
+  "\<forall>n. n < length l --> take (Suc n) l = (take n l)@[l!n]" (is "?P l")
 proof (induct l)
   show "?P []" by simp
 next
@@ -197,39 +258,137 @@
 qed
 
 lemma wtl_Suc:
- "\<lbrakk> wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s = OK s'; 
-     wtl_cert (is!pc) G rT s' cert maxs maxr (length is) et pc = OK s'';
-     Suc pc < length is \<rbrakk> \<Longrightarrow>
-  wtl_inst_list (take (Suc pc) is) G rT cert maxs maxr (length is) et 0 s = OK s''" 
+  assumes "wtl_inst_list (take pc is) cert f r step 0 s = OK s'"
+           "wtl_cert cert f r step pc s' = OK s''" and
+      suc: "pc+1 < length is"
+  shows "wtl_inst_list (take (pc+1) is) cert f r step 0 s = OK s''"    
 proof -
-  assume "wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s = OK s'"
-         "wtl_cert (is!pc) G rT s' cert maxs maxr (length is) et pc = OK s''"
-         "Suc pc < length is"
-  hence "take (Suc pc) is = (take pc is)@[is!pc]" by (simp add: take_Suc)
+  from suc have "take (pc+1) is=(take pc is)@[is!pc]" by (simp add: take_Suc)
   thus ?thesis by (simp! add: wtl_append min_def)
 qed
 
 lemma wtl_all:
-  "\<lbrakk> wtl_inst_list is G rT cert maxs maxr (length is) et 0 s \<noteq> Err;
-      pc < length is \<rbrakk> \<Longrightarrow> 
-   \<exists>s' s''. wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s = OK s' \<and> 
-            wtl_cert (is!pc) G rT s' cert maxs maxr (length is) et pc = OK s''"
+  assumes
+  all: "wtl_inst_list is cert f r step 0 s \<noteq> Err" (is "?wtl is \<noteq> _") and
+  pc:  "pc < length is"
+  shows
+  "\<exists>s' s''. wtl_inst_list (take pc is) cert f r step 0 s = OK s' \<and> 
+            wtl_cert cert f r step pc s' = OK s''"
 proof -
-  assume all: "wtl_inst_list is G rT cert maxs maxr (length is) et 0 s \<noteq> Err"
-
-  assume pc: "pc < length is"
-  hence  "0 < length (drop pc is)" by simp
+  from pc have "0 < length (drop pc is)" by simp
   then  obtain i r where Cons: "drop pc is = i#r" 
     by (auto simp add: neq_Nil_conv simp del: length_drop)
   hence "i#r = drop pc is" ..
-  with all have take: 
-    "wtl_inst_list (take pc is@i#r) G rT cert maxs maxr (length is) et 0 s \<noteq> Err"
-    by simp
- 
+  with all have take: "?wtl (take pc is@i#r) \<noteq> Err" by simp 
   from pc have "is!pc = drop pc is ! 0" by simp
   with Cons have "is!pc = i" by simp
   with take pc show ?thesis by (auto simp add: wtl_append min_def)
 qed
 
+section "preserves-type"
+
+lemma merge_pres:
+  assumes semi: "err_semilat (A,r,f)"
+  assumes s0_A: "\<forall>(pc', s')\<in>set ss. s' \<in> err (opt A)"
+  assumes x_A:  "x \<in> err (opt A)"
+  assumes merge:"merge cert f r pc ss x = OK s'"
+  shows "s' \<in> opt A"
+proof -
+  from s0_A
+  have "set (map snd [(p', t')\<in>ss . p'=pc+1]) \<subseteq> err (opt A)" by auto
+  with semi x_A
+  have "(map snd [(p', t')\<in>ss . p'=pc+1] ++|f x) \<in> err (opt A)"
+    by (auto intro!: plusplus_closed)
+  also {
+    note merge
+    also from semi x_A s0_A
+    have "merge cert f r pc ss x = 
+      (if \<forall>(pc', s')\<in>set ss. pc' \<noteq> pc + 1 \<longrightarrow> s' \<le>|r (OK (cert!pc'))
+      then map snd [(p', t')\<in>ss . p'=pc+1] ++|f x else Err)"
+      by (rule merge_def)
+    finally have "(map snd [(p', t')\<in>ss . p'=pc+1] ++|f x) = OK s'" 
+      by (simp split: split_if_asm)
+  } 
+  finally show ?thesis by simp
+qed
+  
+
+
+lemma wtl_inst_pres [intro?]:
+  assumes semi: "err_semilat (A,r,f)"
+  assumes pres: "pres_type step n (err (opt A))" 
+  assumes cert: "cert!(pc+1) \<in> opt A"
+  assumes s_A:  "s \<in> opt A"
+  assumes pc:   "pc < n"
+  assumes wtl:  "wtl_inst cert f r step pc s = OK s'"
+  shows "s' \<in> opt A"
+proof -
+  from pres pc s_A
+  have "\<forall>(q, s')\<in>set (step pc (OK s)). s' \<in> err (opt A)"
+    by (unfold pres_type_def) blast
+  moreover
+  from cert have "OK (cert!(pc+1)) \<in> err (opt A)" by simp
+  moreover
+  from wtl
+  have "merge cert f r pc (step pc (OK s)) (OK (cert!(pc+1))) = OK s'"  
+    by (unfold wtl_inst_def) simp
+  ultimately
+  show "s' \<in> opt A" using semi by - (rule merge_pres)
+qed
+
+
+lemma wtl_cert_pres:
+  assumes "err_semilat (A,r,f)"
+  assumes "pres_type step n (err (opt A))"
+  assumes "cert!pc \<in> opt A" and "cert!(pc+1) \<in> opt A"
+  assumes "s \<in> opt A" and "pc < n"
+  assumes wtc: "wtl_cert cert f r step pc s = OK s'"
+  shows "s' \<in> opt A"            
+proof -
+  have "wtl_inst cert f r step pc s = OK s' \<Longrightarrow> s' \<in> opt A" ..
+  moreover
+  have "wtl_inst cert f r step pc (cert!pc) = OK s' \<Longrightarrow> s' \<in> opt A" ..
+  ultimately
+  show ?thesis using wtc
+    by (unfold wtl_cert_def) (simp split: option.splits split_if_asm)
+qed
+
+lemma wtl_inst_list_pres:
+  assumes semi: "err_semilat (A,r,f)"
+  assumes pres: "pres_type step (length is) (err (opt A))"
+  assumes cert: "cert_ok cert (length is) A"
+  assumes s:    "s \<in> opt A" 
+  assumes all:  "wtl_inst_list is cert f r step 0 s \<noteq> Err"
+  shows "\<And>s'. pc < length is \<Longrightarrow> wtl_inst_list (take pc is) cert f r step 0 s = OK s'
+         \<Longrightarrow> s' \<in> opt A" (is "\<And>s'. ?len pc \<Longrightarrow> ?wtl pc s' \<Longrightarrow> ?A s'")
+proof (induct pc)
+  from s show "\<And>s'. ?wtl 0 s' \<Longrightarrow> ?A s'" by simp
+next
+  fix s' n
+  assume "Suc n < length is" 
+  then obtain "n < length is" by simp  
+  with all obtain s1 s2 where
+    "wtl_inst_list (take n is) cert f r step 0 s = OK s1" 
+    "wtl_cert cert f r step n s1 = OK s2"
+    by - (drule wtl_all, auto)
+    
+  assume "?wtl (Suc n) s'"
+  moreover
+  have n1: "n+1 < length is" by simp
+  hence "?wtl (n+1) s2" by - (rule wtl_Suc)
+  ultimately
+  have [simp]: "s2 = s'" by simp
+  
+  assume IH: "\<And>s'. n < length is \<Longrightarrow> ?wtl n s' \<Longrightarrow> s' \<in> opt A"
+  hence "s1 \<in> opt A" .
+  moreover
+  from cert have "cert!n \<in> opt A" by (rule cert_okD)
+  moreover
+  from cert n1 have "cert!(n+1) \<in> opt A" by (rule cert_okD)
+  ultimately
+  have "s2 \<in> opt A" using semi pres by - (rule wtl_cert_pres)
+  thus "s' \<in> opt A" by simp
+qed
+
 
 end
diff -r 75b2edff1af3 -r 4b1edf2f6bd2 src/HOL/MicroJava/BV/Opt.thy
--- a/src/HOL/MicroJava/BV/Opt.thy	Mon Mar 18 11:47:03 2002 +0100
+++ b/src/HOL/MicroJava/BV/Opt.thy	Wed Mar 20 13:21:07 2002 +0100
@@ -101,7 +101,7 @@
 done 
 
 
-lemma semilat_opt:
+lemma semilat_opt [intro, simp]:
   "\<And>L. err_semilat L \<Longrightarrow> err_semilat (Opt.esl L)"
 proof (unfold Opt.esl_def Err.sl_def, simp add: split_tupled_all)
   
diff -r 75b2edff1af3 -r 4b1edf2f6bd2 src/HOL/MicroJava/BV/SemilatAlg.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/SemilatAlg.thy	Wed Mar 20 13:21:07 2002 +0100
@@ -0,0 +1,181 @@
+(*  Title:      HOL/MicroJava/BV/SemilatAlg.thy
+    ID:         $Id$
+    Author:     Gerwin Klein
+    Copyright   2002 Technische Universitaet Muenchen
+*)
+
+header {* \isaheader{More on Semilattices} *}
+
+theory SemilatAlg = Typing_Framework + Product:
+
+
+syntax "@lesubstep_type" :: "(nat \<times> 's) list \<Rightarrow> 's ord \<Rightarrow> (nat \<times> 's) list \<Rightarrow> bool"
+       ("(_ /<=|_| _)" [50, 0, 51] 50)
+translations
+ "x <=|r| y" == "x <=[(Product.le (op =) r)] y"
+ 
+consts
+ "@plusplussub" :: "'a list \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" ("(_ /++'__ _)" [65, 1000, 66] 65)
+primrec
+  "[] ++_f y = y"
+  "(x#xs) ++_f y = xs ++_f (x +_f y)"
+
+
+constdefs
+ bounded :: "'s step_type \<Rightarrow> nat \<Rightarrow> bool"
+"bounded step n == !p<n. !s. !(q,t):set(step p s). q<n"  
+
+ pres_type :: "'s step_type \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool"
+"pres_type step n A == \<forall>s\<in>A. \<forall>p<n. \<forall>(q,s')\<in>set (step p s). s' \<in> A"
+
+ mono :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool"
+"mono r step n A ==
+ \<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> step p s <=|r| step p t"
+
+
+lemma pres_typeD:
+  "\<lbrakk> pres_type step n A; s\<in>A; p<n; (q,s')\<in>set (step p s) \<rbrakk> \<Longrightarrow> s' \<in> A"
+  by (unfold pres_type_def, blast)
+
+lemma monoD:
+  "\<lbrakk> mono r step n A; p < n; s\<in>A; s <=_r t \<rbrakk> \<Longrightarrow> step p s <=|r| step p t"
+  by (unfold mono_def, blast)
+
+lemma boundedD: 
+  "\<lbrakk> bounded step n; p < n; (q,t) : set (step p xs) \<rbrakk> \<Longrightarrow> q < n" 
+  by (unfold bounded_def, blast)
+
+
+lemma 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"
+  apply (unfold Listn.le_def lesub_def semilat_def)
+  apply (simp add: list_all2_conv_all_nth nth_list_update)
+  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"
+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)
+  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"
+proof (induct x)
+  show "\<And>y. semilat(A, r, f) \<Longrightarrow> 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"
+  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)
+  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
+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"
+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]
+  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"
+  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)" .
+    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)" .
+  }
+  ultimately 
+  have "x <=_r ls ++_f (s +_f y)" by blast
+  thus "x <=_r (s#ls) ++_f y" 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" 
+proof -
+  let "b <=_r ?map ++_f y" = ?thesis
+
+  assume "semilat (A, r, f)" "y \<in> A"
+  moreover
+  assume "\<forall>(p,s) \<in> set S. s \<in> A"
+  hence "set ?map \<subseteq> A" by auto
+  moreover
+  assume "(a,b) \<in> set S"
+  hence "b \<in> set ?map" by (induct S, auto)
+  ultimately
+  show ?thesis by - (rule ub1)
+qed
+    
+ 
+
+lemma plusplus_empty:  
+  "\<forall>s'. (q, s') \<in> set S \<longrightarrow> s' +_f ss ! q = ss ! q \<Longrightarrow>
+   (map snd [(p', t')\<in> S. p' = q] ++_f ss ! q) = ss ! q"
+apply (induct S)
+apply auto 
+done
+
+
+lemma lesub_step_type:
+  "\<And>b x y. a <=|r| b \<Longrightarrow> (x,y) \<in> set a \<Longrightarrow> \<exists>y'. (x, y') \<in> set b \<and> y <=_r y'"
+apply (induct a)
+ apply simp
+apply simp
+apply (case_tac b)
+ apply simp
+apply simp
+apply (erule disjE)
+ apply clarify
+ apply (simp add: lesub_def)
+ apply blast   
+apply clarify
+apply blast
+done
+
+end
diff -r 75b2edff1af3 -r 4b1edf2f6bd2 src/HOL/MicroJava/BV/Typing_Framework.thy
--- a/src/HOL/MicroJava/BV/Typing_Framework.thy	Mon Mar 18 11:47:03 2002 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework.thy	Wed Mar 20 13:21:07 2002 +0100
@@ -15,9 +15,6 @@
   's step_type = "nat \<Rightarrow> 's \<Rightarrow> (nat \<times> 's) list"
 
 constdefs
- bounded :: "'s step_type \<Rightarrow> nat \<Rightarrow> bool"
-"bounded step n == !p<n. !s. !(q,t):set(step p s). q<n"  
-
  stable :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> nat \<Rightarrow> bool"
 "stable r step ss p == !(q,s'):set(step p (ss!p)). s' <=_r ss!q"
 
diff -r 75b2edff1af3 -r 4b1edf2f6bd2 src/HOL/MicroJava/BV/Typing_Framework_err.thy
--- a/src/HOL/MicroJava/BV/Typing_Framework_err.thy	Mon Mar 18 11:47:03 2002 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework_err.thy	Wed Mar 20 13:21:07 2002 +0100
@@ -7,7 +7,7 @@
 
 header {* \isaheader{Static and Dynamic Welltyping} *}
 
-theory Typing_Framework_err = Typing_Framework:
+theory Typing_Framework_err = Typing_Framework + SemilatAlg:
 
 constdefs
 
diff -r 75b2edff1af3 -r 4b1edf2f6bd2 src/HOL/MicroJava/ROOT.ML
--- a/src/HOL/MicroJava/ROOT.ML	Mon Mar 18 11:47:03 2002 +0100
+++ b/src/HOL/MicroJava/ROOT.ML	Wed Mar 20 13:21:07 2002 +0100
@@ -13,9 +13,8 @@
 use_thy "JVM";
 use_thy "BVSpecTypeSafe";
 use_thy "BVExample";
-use_thy "LBVSpec"; 
+use_thy "LBVCorrect";
 
 (* momentarily broken:
-use_thy "LBVCorrect";
 use_thy "LBVComplete";
 *)