# HG changeset patch
# User kleing
# Date 1017931680 -7200
# Node ID 1dd711c6b93c1c67b112ca36077f43a9e45f1e8b
# Parent  c2e4d99901626e17ebc09350faf6de91dcf39b4c
flattened, uses locales

diff -r c2e4d9990162 -r 1dd711c6b93c src/HOL/MicroJava/BV/LBVComplete.thy
--- a/src/HOL/MicroJava/BV/LBVComplete.thy	Thu Apr 04 16:47:44 2002 +0200
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Thu Apr 04 16:48:00 2002 +0200
@@ -9,508 +9,366 @@
 theory LBVComplete = LBVSpec + Typing_Framework:
 
 constdefs
-  contains_targets :: "['s steptype, 's certificate, 's option list, nat] \<Rightarrow> bool"
-  "contains_targets step cert phi pc \<equiv>
-  \<forall>(pc',s') \<in> set (step pc (OK (phi!pc))). pc' \<noteq> pc+1 \<and> pc' < length phi \<longrightarrow> cert!pc' = phi!pc'"
+  is_target :: "['s step_type, 's list, nat] \<Rightarrow> bool" 
+  "is_target step phi pc' \<equiv>
+     \<exists>pc s'. pc' \<noteq> pc+1 \<and> pc < length phi \<and> (pc',s') \<in> set (step pc (phi!pc))"
 
-  fits :: "['s steptype, 's certificate, 's option list] \<Rightarrow> bool"
-  "fits step cert phi \<equiv> \<forall>pc. pc < length phi \<longrightarrow> 
-                             contains_targets step cert phi pc \<and>
-                             (cert!pc = None \<or> cert!pc = phi!pc)"
+  make_cert :: "['s step_type, 's list, 's] \<Rightarrow> 's certificate"
+  "make_cert step phi B \<equiv> 
+     map (\<lambda>pc. if is_target step phi pc then phi!pc else B) [0..length phi(] @ [B]"
+
+locale lbvc = lbv + 
+  fixes phi :: "'a list" ("\<phi>")
+  fixes c   :: "'a list" 
+  defines cert_def: "c \<equiv> make_cert step \<phi> \<bottom>"
 
-  is_target :: "['s steptype, 's option list, nat] \<Rightarrow> bool" 
-  "is_target step phi pc' \<equiv>
-     \<exists>pc s'. pc' \<noteq> pc+1 \<and> pc < length phi \<and> (pc',s') \<in> set (step pc (OK (phi!pc)))"
+  assumes mono: "mono r step (length \<phi>) A"
+  assumes pres: "pres_type step (length \<phi>) A" 
+  assumes phi:  "\<forall>pc < length \<phi>. \<phi>!pc \<in> A \<and> \<phi>!pc \<noteq> \<top>"
+  assumes bounded: "bounded step (length \<phi>)"
+
+  assumes B_neq_T: "\<bottom> \<noteq> \<top>" 
+
 
-  make_cert :: "['s steptype, 's option list] \<Rightarrow> 's certificate"
-  "make_cert step phi \<equiv> 
-     map (\<lambda>pc. if is_target step phi pc then phi!pc else None) [0..length phi(] @ [None]"
+lemma (in lbvc) cert: "cert_ok c (length \<phi>) \<top> \<bottom> A"
+proof (unfold cert_ok_def, intro strip conjI)  
+  note [simp] = make_cert_def cert_def nth_append 
+
+  show "c!length \<phi> = \<bottom>" by simp
 
-  
+  fix pc assume pc: "pc < length \<phi>" 
+  from pc phi B_A show "c!pc \<in> A" by simp
+  from pc phi B_neq_T show "c!pc \<noteq> \<top>" by simp
+qed
+
 lemmas [simp del] = split_paired_Ex
 
-lemma make_cert_target:
-  "\<lbrakk> pc < length phi; is_target step phi pc \<rbrakk> \<Longrightarrow> make_cert step phi ! pc = phi!pc"
-  by (simp add: make_cert_def nth_append)
-
-lemma make_cert_approx:
-  "\<lbrakk> pc < length phi; make_cert step phi ! pc \<noteq> phi!pc \<rbrakk> \<Longrightarrow> 
-   make_cert step phi ! pc = None"
-  by (auto simp add: make_cert_def nth_append)
 
-lemma make_cert_contains_targets:
-  "pc < length phi \<Longrightarrow> contains_targets step (make_cert step phi) phi pc"
-proof (unfold contains_targets_def, clarify)
-  fix pc' s'
-  assume "pc < length phi"
-         "(pc',s') \<in> set (step pc (OK (phi ! pc)))"
-         "pc' \<noteq> pc+1" and
-    pc': "pc' < length phi"
-  hence "is_target step phi pc'"  by (auto simp add: is_target_def)
-  with pc' show "make_cert step phi ! pc' = phi!pc'" 
-    by (auto intro: make_cert_target)
-qed
+lemma (in lbvc) cert_target [intro?]:
+  "\<lbrakk> (pc',s') \<in> set (step pc (\<phi>!pc));
+      pc' \<noteq> pc+1; pc < length \<phi>; pc' < length \<phi> \<rbrakk>
+  \<Longrightarrow> c!pc' = \<phi>!pc'"
+  by (auto simp add: cert_def make_cert_def nth_append is_target_def)
 
-theorem fits_make_cert:
-  "fits step (make_cert step phi) phi"
-  by (auto dest: make_cert_approx simp add: fits_def make_cert_contains_targets)
 
-lemma fitsD: 
-  "\<lbrakk> fits step cert phi; (pc',s') \<in> set (step pc (OK (phi!pc)));
-      pc' \<noteq> pc+1; pc < length phi; pc' < length phi \<rbrakk>
-  \<Longrightarrow> cert!pc' = phi!pc'"
-  by (auto simp add: fits_def contains_targets_def)
-
-lemma fitsD2:
-   "\<lbrakk> fits step cert phi; pc < length phi; cert!pc = Some s \<rbrakk>
-  \<Longrightarrow> cert!pc = phi!pc"
-  by (auto simp add: fits_def)
+lemma (in lbvc) cert_approx [intro?]:
+  "\<lbrakk> pc < length \<phi>; c!pc \<noteq> \<bottom> \<rbrakk>
+  \<Longrightarrow> c!pc = \<phi>!pc"
+  by (auto simp add: cert_def make_cert_def nth_append)
 
 
-lemma merge_mono:
-  assumes merge: "merge cert f r pc ss1 x = OK s1"
-  assumes less:  "ss2 <=|Err.le (Opt.le r)| ss1"
-  assumes esl:   "err_semilat (A, r, f)"
-  assumes x:     "x \<in> err (opt A)"
-  assumes ss1:   "\<forall>(pc', s')\<in>set ss1. s' \<in> err (opt A)"
-  assumes ss2:   "\<forall>(pc', s')\<in>set ss2. s' \<in> err (opt A)"
-  shows "\<exists>s2. merge cert f r pc ss2 x = s2 \<and> s2 \<le>|r (OK s1)"
+lemma (in lbv) le_top [simp, intro]:
+  "x <=_r \<top>"
+  by (insert top) simp
+  
+
+lemma (in lbv) merge_mono:
+  assumes less:  "ss2 <=|r| ss1"
+  assumes x:     "x \<in> A"
+  assumes ss1:   "snd`set ss1 \<subseteq> A"
+  assumes ss2:   "snd`set ss2 \<subseteq> A"
+  shows "merge c pc ss2 x <=_r merge c pc ss1 x" (is "?s2 <=_r ?s1")
 proof-
-  from esl have eosl: "err_semilat (opt A, Opt.le r, Opt.sup f)" 
-    by - (drule semilat_opt, simp add: Opt.esl_def)
-  hence order: "order (Opt.le r)" ..
-  from esl x ss1 have "merge cert f r pc ss1 x =
-    (if \<forall>(pc', s')\<in>set ss1. pc' \<noteq> pc + 1 \<longrightarrow> s' \<le>|r (OK (cert!pc'))
-    then (map snd [(p', t')\<in>ss1 . p'=pc+1]) ++|f x
-    else Err)" 
-    by (rule merge_def)
-  with merge obtain
-    app: "\<forall>(pc',s')\<in>set ss1. pc' \<noteq> pc+1 \<longrightarrow> s' \<le>|r (OK (cert!pc'))" 
-         (is "?app ss1") and
-    sum: "(map snd [(p',t')\<in>ss1 . p' = pc+1] ++|f x) = OK s1" 
-         (is "?map ss1 ++|f x = _" is "?sum ss1 = _")
-    by (simp split: split_if_asm)
-  from app less
-  have "?app ss2" 
-    apply clarify 
-    apply (drule lesub_step_typeD, assumption) 
-    apply clarify
-    apply (drule bspec, assumption)
-    apply clarify
-    apply (drule order_trans [OF order], assumption)
-    apply blast
-    done
+  have "?s1 = \<top> \<Longrightarrow> ?thesis" by simp
   moreover {
-    have "set (?map ss1) \<subseteq> snd`(set ss1)" by auto
-    also from ss1 have "snd`(set ss1) \<subseteq> err (opt A)" by auto
-    finally have map1: "set (?map ss1) \<subseteq> err (opt A)" . 
-    with eosl x have "?sum ss1 \<in> err (opt A)" 
-      by (auto intro!: plusplus_closed simp add: Err.sl_def)
-    with sum have "OK s1 \<in> err (opt A)" by simp
-    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 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
-      apply (drule mapD)
-      apply clarify
-      apply (drule lesub_step_typeD, assumption)
-      apply clarify
-      apply simp
-      apply (erule allE, erule impE, assumption)
-      apply clarify
-      apply simp
-      apply (rule order_trans [OF order],assumption+)
-      done
-    moreover 
-    from eosl map1 x have "x \<le>|r (?sum ss1)" 
-      by - (rule semilat.pp_ub2, simp add: Err.sl_def)
-    with sum have "x \<le>|r (OK s1)" by simp
+    assume merge: "?s1 \<noteq> T" 
+    from x ss1 have "?s1 =
+      (if \<forall>(pc', s')\<in>set ss1. pc' \<noteq> pc + 1 \<longrightarrow> s' <=_r c!pc'
+      then (map snd [(p', t')\<in>ss1 . p'=pc+1]) ++_f x
+      else \<top>)" 
+      by (rule merge_def)  
+    with merge obtain
+      app: "\<forall>(pc',s')\<in>set ss1. pc' \<noteq> pc+1 \<longrightarrow> s' <=_r c!pc'" 
+           (is "?app ss1") and
+      sum: "(map snd [(p',t')\<in>ss1 . p' = pc+1] ++_f x) = ?s1" 
+           (is "?map ss1 ++_f x = _" is "?sum ss1 = _")
+      by (simp split: split_if_asm)
+    from app less 
+    have "?app ss2" by (blast dest: trans_r lesub_step_typeD)
     moreover {
-      have "set (?map ss2) \<subseteq> snd`(set ss2)" by auto
-      also from ss2 have "snd`(set ss2) \<subseteq> err (opt A)" by auto
-      finally have "set (?map ss2) \<subseteq> err (opt A)" . }
-    ultimately
-    have "?sum ss2 \<le>|r (OK s1)" using eosl x
-      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
+      from ss1 have map1: "set (?map ss1) \<subseteq> A" by auto
+      with x have "?sum ss1 \<in> A" by (auto intro!: plusplus_closed)
+      with sum have "?s1 \<in> A" by simp
+      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 x map1 
+      have "\<forall>x \<in> set (?map ss1). x <=_r ?sum ss1"
+        by clarify (rule pp_ub1)
+      with sum have "\<forall>x \<in> set (?map ss1). x <=_r ?s1" by simp
+      with less have "\<forall>x \<in> set (?map ss2). x <=_r ?s1"
+        by (fastsimp dest!: mapD lesub_step_typeD intro: trans_r)
+      moreover 
+      from map1 x have "x <=_r (?sum ss1)" by (rule pp_ub2)
+      with sum have "x <=_r ?s1" by simp
+      moreover 
+      from ss2 have "set (?map ss2) \<subseteq> A" by auto
+      ultimately
+      have "?sum ss2 <=_r ?s1" using x by - (rule pp_lub)
+    }
+    moreover
+    from x ss2 have 
+      "?s2 =
+      (if \<forall>(pc', s')\<in>set ss2. pc' \<noteq> pc + 1 \<longrightarrow> s' <=_r c!pc'
+      then map snd [(p', t')\<in>ss2 . p' = pc + 1] ++_f x
+      else \<top>)" 
+      by (rule merge_def)
+    ultimately have ?thesis by simp
   }
-  moreover
-  from esl x ss2 have 
-    "merge cert f r pc ss2 x =
-    (if \<forall>(pc', s')\<in>set ss2. pc' \<noteq> pc + 1 \<longrightarrow> s' \<le>|r (OK (cert!pc'))
-    then map snd [(p', t')\<in>ss2 . p' = pc + 1] ++|f x
-    else Err)" 
-    by (rule merge_def)
-  ultimately show ?thesis by simp
+  ultimately show ?thesis by (cases "?s1 = \<top>") auto
 qed
 
 
-lemma wtl_inst_mono:
-  assumes wtl:  "wtl_inst cert f r step pc s1 = OK s1'"
-  assumes less: "OK s2 \<le>|r (OK s1)"
-  assumes pc:   "pc < n" 
-  assumes s1:   "s1 \<in> opt A"
-  assumes s2:   "s2 \<in> opt A"
-  assumes esl:  "err_semilat (A,r,f)"
-  assumes cert: "cert_ok cert n A"
-  assumes mono: "mono (Err.le (Opt.le r)) step n (err (opt A))"
-  assumes pres: "pres_type step n (err (opt A))" 
-  shows "\<exists>s2'. wtl_inst cert f r step pc s2 = OK s2' \<and> OK s2' \<le>|r (OK s1')"
+lemma (in lbvc) wti_mono:
+  assumes less: "s2 <=_r s1"
+  assumes pc:   "pc < length \<phi>" 
+  assumes s1:   "s1 \<in> A"
+  assumes s2:   "s2 \<in> A"
+  shows "wti c pc s2 <=_r wti c pc s1" (is "?s2' <=_r ?s1'")
 proof -
-  let "?step s1" = "step pc (OK s1)"
-  let ?cert = "OK (cert!Suc pc)"
-  from wtl 
-  have "merge cert f r pc (?step s1) ?cert = OK s1'" by (simp add: wtl_inst_def)
+  from mono s2 have "step pc s2 <=|r| step pc s1" by - (rule monoD)
   moreover
-  have s2: "OK s2 \<in> err (opt A)" by simp
-  with mono have "?step s2 <=|Err.le (Opt.le r)| ?step s1" by - (rule monoD)
-  moreover note esl
-  moreover
-  from pc cert have "?cert \<in> err (opt A)" by (simp add: cert_okD3)
-  moreover
-  have s1: "OK s1 \<in> err (opt A)" by simp
-  with pres pc
-  have "\<forall>(pc', s')\<in>set (?step s1). s' \<in> err (opt A)"
-    by (blast intro: pres_typeD)  
+  from pc cert have "c!Suc pc \<in> A" by - (rule cert_okD3)
+  moreover 
+  from pres s1 pc
+  have "snd`set (step pc s1) \<subseteq> A" by (rule pres_typeD2)
   moreover
   from pres s2 pc
-  have "\<forall>(pc', s')\<in>set (?step s2). s' \<in> err (opt A)" 
-    by (blast intro: pres_typeD)  
+  have "snd`set (step pc s2) \<subseteq> A" by (rule pres_typeD2)
   ultimately
-  obtain s2' where "merge cert f r pc (?step s2) ?cert = s2' \<and> s2' \<le>|r (OK s1')"
-    by (blast dest: merge_mono)
-  thus ?thesis by (simp add: wtl_inst_def)
+  show ?thesis by (simp add: wti merge_mono)
 qed 
 
-lemma wtl_cert_mono:
-  assumes wtl:  "wtl_cert cert f r step pc s1 = OK s1'"
-  assumes less: "OK s2 \<le>|r (OK s1)"
-  assumes pc:   "pc < n" 
-  assumes s1:   "s1 \<in> opt A"
-  assumes s2:   "s2 \<in> opt A"
-  assumes esl:  "err_semilat (A,r,f)"
-  assumes cert: "cert_ok cert n A"
-  assumes mono: "mono (Err.le (Opt.le r)) step n (err (opt A))"
-  assumes pres: "pres_type step n (err (opt A))" 
-  shows "\<exists>s2'. wtl_cert cert f r step pc s2 = OK s2' \<and> OK s2' \<le>|r (OK s1')"
-proof (cases "cert!pc")
-  case None
-  with wtl have "wtl_inst cert f r step pc s1 = OK s1'" 
-    by (simp add: wtl_cert_def)
-  hence "\<exists>s2'. wtl_inst cert f r step pc s2 = OK s2' \<and> OK s2' \<le>|r (OK s1')"
-    by - (rule wtl_inst_mono)
-  with None show ?thesis by (simp add: wtl_cert_def)
+lemma (in lbvc) wtc_mono:
+  assumes less: "s2 <=_r s1"
+  assumes pc:   "pc < length \<phi>" 
+  assumes s1:   "s1 \<in> A"
+  assumes s2:   "s2 \<in> A"
+  shows "wtc c pc s2 <=_r wtc c pc s1" (is "?s2' <=_r ?s1'")
+proof (cases "c!pc = \<bottom>")
+  case True 
+  moreover have "wti c pc s2 <=_r wti c pc s1" by (rule wti_mono)
+  ultimately show ?thesis by (simp add: wtc)
 next
-  case (Some s')
-  with wtl obtain 
-    wti: "wtl_inst cert f r step pc (Some s') = OK s1'" and
-    s':  "OK s1 \<le>|r OK (Some s')"
-    by (auto simp add: wtl_cert_def split: split_if_asm)
-  from esl have order: "order (Opt.le r)" by simp
-  hence "order (Err.le (Opt.le r))" by simp
-  with less s' have "OK s2 \<le>|r OK (Some s')" by - (drule order_trans)
-  with Some wti order show ?thesis by (simp add: wtl_cert_def)
+  case False
+  have "?s1' = \<top> \<Longrightarrow> ?thesis" by simp
+  moreover {
+    assume "?s1' \<noteq> \<top>" 
+    with False have c: "s1 <=_r c!pc" by (simp add: wtc split: split_if_asm)
+    with less have "s2 <=_r c!pc" ..
+    with False c have ?thesis by (simp add: wtc)
+  }
+  ultimately show ?thesis by (cases "?s1' = \<top>") auto
 qed
 
 
-lemma stable_wtl:
-  assumes stable:  "stable (Err.le (Opt.le r)) step (map OK phi) pc"
-  assumes fits:    "fits step cert phi"  
-  assumes pc:      "pc < length phi"
-  assumes bounded: "bounded step (length phi)"
-  assumes esl:     "err_semilat (A, r, f)"
-  assumes cert_ok: "cert_ok cert (length phi) A"
-  assumes phi_ok:  "\<forall>pc < length phi. phi!pc \<in> opt A"
-  assumes pres:    "pres_type step (length phi) (err (opt A))" 
-  shows "wtl_inst cert f r step pc (phi!pc) \<noteq> Err"
+lemma (in lbv) top_le_conv [simp]:
+  "\<top> <=_r x = (x = \<top>)"
+  by (insert semilat) (simp add: top top_le_conv) 
+
+lemma (in lbv) neq_top [simp, elim]:
+  "\<lbrakk> x <=_r y; y \<noteq> \<top> \<rbrakk> \<Longrightarrow> x \<noteq> \<top>"
+  by (cases "x = T") auto
+
+
+lemma (in lbvc) stable_wti:
+  assumes stable:  "stable r step \<phi> pc"
+  assumes pc:      "pc < length \<phi>"
+  shows "wti c pc (\<phi>!pc) \<noteq> \<top>"
 proof -
-  from esl have order: "order (Opt.le r)" by simp
-
-  let ?step = "step pc (OK (phi!pc))"
-  from pc have [simp]: "map OK phi ! pc = OK (phi!pc)" by simp
+  let ?step = "step pc (\<phi>!pc)"
   from stable 
-  have less: "\<forall>(q,s')\<in>set ?step. s' \<le>|r (map OK phi!q)" 
-    by (simp add: stable_def)
+  have less: "\<forall>(q,s')\<in>set ?step. s' <=_r \<phi>!q" by (simp add: stable_def)
   
-  from cert_ok pc
-  have cert_suc: "OK (cert!Suc pc) \<in> err (opt A)" by (auto dest: cert_okD3)
+  from cert pc 
+  have cert_suc: "c!Suc pc \<in> A" by - (rule cert_okD3)
   moreover  
-  from phi_ok pc
-  have "OK (phi!pc) \<in> err (opt A)" by simp
+  from phi pc have "\<phi>!pc \<in> A" by simp
   with pres pc 
-  have stepA: "\<forall>(pc',s') \<in> set ?step. s' \<in> err (opt A)" 
-    by (blast dest: pres_typeD)
+  have stepA: "snd`set ?step \<subseteq> A" by - (rule pres_typeD2)  
   ultimately
-  have "merge cert f r pc ?step (OK (cert!Suc pc)) =
-    (if \<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' \<le>|r (OK (cert!pc'))
-    then map snd [(p',t')\<in>?step.p'=pc+1] ++|f (OK (cert!Suc pc))
-    else Err)" using esl by - (rule merge_def)
+  have "merge c pc ?step (c!Suc pc) =
+    (if \<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'
+    then map snd [(p',t')\<in>?step.p'=pc+1] ++_f c!Suc pc
+    else \<top>)" by (rule merge_def)
   moreover {
     fix pc' s' assume s': "(pc', s') \<in> set ?step" and suc_pc: "pc' \<noteq> pc+1"
-    from bounded pc s' have pc': "pc' < length phi" by (rule boundedD)
-    hence [simp]: "map OK phi ! pc' = OK (phi!pc')" by simp
-    with s' less have "s' \<le>|r OK (phi!pc')" by auto
-    also from fits s' suc_pc pc pc' 
-    have "cert!pc' = phi!pc'" by (rule fitsD)
-    hence "phi!pc' = cert!pc'" ..
-    finally have "s' \<le>|r (OK (cert!pc'))" .
-  } hence "\<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' \<le>|r (OK (cert!pc'))" by auto
+    with less have "s' <=_r \<phi>!pc'" by auto
+    also 
+    from bounded pc s' have "pc' < length \<phi>" by (rule boundedD)
+    with s' suc_pc pc have "c!pc' = \<phi>!pc'" ..
+    hence "\<phi>!pc' = c!pc'" ..
+    finally have "s' <=_r c!pc'" .
+  } hence "\<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'" by auto
   moreover
-  from pc have "Suc pc = length phi \<or> Suc pc < length phi" by auto
-  hence "(map snd [(p',t')\<in>?step.p'=pc+1] ++|f (OK (cert!Suc pc))) \<noteq> Err" 
-         (is "(?map ++|f _) \<noteq> _")
+  from pc have "Suc pc = length \<phi> \<or> Suc pc < length \<phi>" by auto
+  hence "map snd [(p',t')\<in>?step.p'=pc+1] ++_f c!Suc pc \<noteq> \<top>" 
+         (is "?map ++_f _ \<noteq> _")
   proof (rule disjE)
-    assume pc': "Suc pc = length phi"
-    with cert_ok have "cert!Suc pc = None" by (simp add: cert_okD2)
+    assume pc': "Suc pc = length \<phi>"
+    with cert have "c!Suc pc = \<bottom>" by (simp add: cert_okD2)
     moreover 
-    from pc' bounded pc
+    from pc' bounded pc 
     have "\<forall>(p',t')\<in>set ?step. p'\<noteq>pc+1" by clarify (drule boundedD, auto)
     hence "[(p',t')\<in>?step.p'=pc+1] = []" by (blast intro: filter_False) 
     hence "?map = []" by simp
-    ultimately show ?thesis by simp
+    ultimately show ?thesis by (simp add: B_neq_T)  
   next
-    assume pc': "Suc pc < length phi"
-    hence [simp]: "map OK phi ! Suc pc = OK (phi!Suc pc)" by simp
-    from esl
-    have "semilat (err (opt A), Err.le (Opt.le r), lift2 (Opt.sup f))"
-      by (simp add: Err.sl_def)
-    moreover
-    from pc' phi_ok 
-    have "OK (phi!Suc pc) \<in> err (opt A)" by simp
+    assume pc': "Suc pc < length \<phi>"
+    from pc' phi have "\<phi>!Suc pc \<in> A" by simp
     moreover note cert_suc
     moreover from stepA 
-    have "snd`(set ?step) \<subseteq> err (opt A)" by auto
-    hence "set ?map \<subseteq> err (opt A)" by auto
+    have "set ?map \<subseteq> A" by auto
     moreover
     have "\<And>s. s \<in> set ?map \<Longrightarrow> \<exists>t. (Suc pc, t) \<in> set ?step" by auto
-    with less have "\<forall>s' \<in> set ?map. s' \<le>|r OK (phi!Suc pc)" by auto
+    with less have "\<forall>s' \<in> set ?map. s' <=_r \<phi>!Suc pc" by auto
     moreover
-    from order fits pc' 
-    have "OK (cert!Suc pc) \<le>|r OK (phi!Suc pc)"     
-      by (cases "cert!Suc pc") (simp, blast dest: fitsD2) 
+    from pc' have "c!Suc pc <=_r \<phi>!Suc pc" 
+      by (cases "c!Suc pc = \<bottom>") (auto dest: cert_approx)
     ultimately
-    have "?map ++|f OK (cert!Suc pc) \<le>|r OK (phi!Suc pc)"
-      by (rule semilat.pp_lub)
-    thus ?thesis by auto
+    have "?map ++_f c!Suc pc <=_r \<phi>!Suc pc" by (rule pp_lub)
+    moreover
+    from pc' phi have "\<phi>!Suc pc \<noteq> \<top>" by simp
+    ultimately
+    show ?thesis by auto
   qed
   ultimately
-  have "merge cert f r pc ?step (OK (cert!Suc pc)) \<noteq> Err" by simp
-  thus ?thesis by (simp add: wtl_inst_def)  
+  have "merge c pc ?step (c!Suc pc) \<noteq> \<top>" by simp
+  thus ?thesis by (simp add: wti)  
 qed
 
-lemma stable_cert:
-  assumes stable:  "stable (Err.le (Opt.le r)) step (map OK phi) pc"
-  assumes fits:    "fits step cert phi"  
-  assumes pc:      "pc < length phi"
-  assumes bounded: "bounded step (length phi)"
-  assumes esl:     "err_semilat (A, r, f)"
-  assumes cert_ok: "cert_ok cert (length phi) A"
-  assumes phi_ok:  "\<forall>pc < length phi. phi!pc \<in> opt A"
-  assumes pres:    "pres_type step (length phi) (err (opt A))" 
-  shows "wtl_cert cert f r step pc (phi!pc) \<noteq> Err"
+lemma (in lbvc) wti_less:
+  assumes stable:  "stable r step \<phi> pc"
+  assumes suc_pc:   "Suc pc < length \<phi>"
+  shows "wti c pc (\<phi>!pc) <=_r \<phi>!Suc pc" (is "?wti <=_r _")
 proof -
-  have wtl: "wtl_inst cert f r step pc (phi!pc) \<noteq> Err" by (rule stable_wtl)   
-  show ?thesis
-  proof (cases "cert!pc")
-    case None with wtl show ?thesis by (simp add: wtl_cert_def)
-  next
-    case (Some s)
-    with pc fits have "cert!pc = phi!pc" by - (rule fitsD2)
-    with Some have "phi!pc = Some s" by simp
-    with Some wtl esl show ?thesis by (simp add: wtl_cert_def)
-  qed
-qed
-  
-
-lemma wtl_less:
-  assumes stable:  "stable (Err.le (Opt.le r)) step (map OK phi) pc"
-  assumes wtl:     "wtl_inst cert f r step pc (phi!pc) = OK s"
-  assumes fits:    "fits step cert phi"  
-  assumes suc_pc:   "Suc pc < length phi"
-  assumes bounded: "bounded step (length phi)"
-  assumes esl:     "err_semilat (A, r, f)"
-  assumes cert_ok: "cert_ok cert (length phi) A"
-  assumes phi_ok:  "\<forall>pc < length phi. phi!pc \<in> opt A"
-  assumes pres:    "pres_type step (length phi) (err (opt A))" 
-  shows "OK s \<le>|r OK (phi!Suc pc)"
-proof -
-  from esl have order: "order (Opt.le r)" by simp
+  let ?step = "step pc (\<phi>!pc)"
 
-  let ?step = "step pc (OK (phi!pc))"
-  from suc_pc have [simp]: "map OK phi ! pc = OK (phi!pc)" by simp
-  from suc_pc have [simp]: "map OK phi ! Suc pc = OK (phi!Suc pc)" by simp
-  from suc_pc have pc: "pc < length phi" by simp
-
-  from stable
-  have less: "\<forall>(q,s')\<in>set ?step. s' \<le>|r (map OK phi!q)" 
-    by (simp add: stable_def)
-  
-  from cert_ok pc
-  have cert_suc: "OK (cert!Suc pc) \<in> err (opt A)" by (auto dest: cert_okD3)
+  from stable 
+  have less: "\<forall>(q,s')\<in>set ?step. s' <=_r \<phi>!q" by (simp add: stable_def)
+   
+  from suc_pc have pc: "pc < length \<phi>" by simp
+  with cert have cert_suc: "c!Suc pc \<in> A" by - (rule cert_okD3)
   moreover  
-  from phi_ok pc
-  have "OK (phi!pc) \<in> err (opt A)" by simp
-  with pres pc 
-  have stepA: "\<forall>(pc',s') \<in> set ?step. s' \<in> err (opt A)" 
-    by (blast dest: pres_typeD)
+  from phi pc have "\<phi>!pc \<in> A" by simp
+  with pres pc have stepA: "snd`set ?step \<subseteq> A" by - (rule pres_typeD2)
+  moreover
+  from stable pc have "?wti \<noteq> \<top>" by (rule stable_wti)
+  hence "merge c pc ?step (c!Suc pc) \<noteq> \<top>" by (simp add: wti)
   ultimately
-  have "merge cert f r pc ?step (OK (cert!Suc pc)) =
-    (if \<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' \<le>|r (OK (cert!pc'))
-    then map snd [(p',t')\<in>?step.p'=pc+1] ++|f (OK (cert!Suc pc))
-    else Err)" using esl by - (rule merge_def)
-  with wtl have
-    "OK s = (map snd [(p',t')\<in>?step.p'=pc+1] ++|f (OK (cert!Suc pc)))" 
-    (is "_ = (?map ++|f _)" is "_ = ?sum")
-    by (simp add: wtl_inst_def split: split_if_asm)
+  have "merge c pc ?step (c!Suc pc) =
+    map snd [(p',t')\<in>?step.p'=pc+1] ++_f c!Suc pc" by (rule merge_not_top_s) 
+  hence "?wti = \<dots>" (is "_ = (?map ++_f _)" is "_ = ?sum") by (simp add: wti)
   also {
-    from esl
-    have "semilat (err (opt A), Err.le (Opt.le r), lift2 (Opt.sup f))"
-      by (simp add: Err.sl_def)
-    moreover
-    from suc_pc phi_ok 
-    have "OK (phi!Suc pc) \<in> err (opt A)" by simp
+    from suc_pc phi have "\<phi>!Suc pc \<in> A" by simp
     moreover note cert_suc
-    moreover from stepA 
-    have "snd`(set ?step) \<subseteq> err (opt A)" by auto
-    hence "set ?map \<subseteq> err (opt A)" by auto
+    moreover from stepA have "set ?map \<subseteq> A" by auto
     moreover
     have "\<And>s. s \<in> set ?map \<Longrightarrow> \<exists>t. (Suc pc, t) \<in> set ?step" by auto
-    with less have "\<forall>s' \<in> set ?map. s' \<le>|r OK (phi!Suc pc)" by auto
+    with less have "\<forall>s' \<in> set ?map. s' <=_r \<phi>!Suc pc" by auto
     moreover
-    from order fits suc_pc
-    have "OK (cert!Suc pc) \<le>|r OK (phi!Suc pc)"     
-      by (cases "cert!Suc pc") (simp, blast dest: fitsD2) 
+    from suc_pc have "c!Suc pc <=_r \<phi>!Suc pc"
+      by (cases "c!Suc pc = \<bottom>") (auto dest: cert_approx)
     ultimately
-    have "?sum \<le>|r OK (phi!Suc pc)" by (rule semilat.pp_lub)
+    have "?sum <=_r \<phi>!Suc pc" by (rule pp_lub)
   }
   finally show ?thesis .
 qed
 
+lemma (in lbvc) stable_wtc:
+  assumes stable:  "stable r step phi pc"
+  assumes pc:      "pc < length \<phi>"
+  shows "wtc c pc (\<phi>!pc) \<noteq> \<top>"
+proof -
+  have wti: "wti c pc (\<phi>!pc) \<noteq> \<top>" by (rule stable_wti)   
+  show ?thesis
+  proof (cases "c!pc = \<bottom>")
+    case True with wti show ?thesis by (simp add: wtc)
+  next
+    case False
+    with pc have "c!pc = \<phi>!pc" ..    
+    with False wti show ?thesis by (simp add: wtc)
+  qed
+qed
 
-lemma cert_less:
-  assumes stable:  "stable (Err.le (Opt.le r)) step (map OK phi) pc"
-  assumes cert:    "wtl_cert cert f r step pc (phi!pc) = OK s"
-  assumes fits:    "fits step cert phi"  
-  assumes suc_pc:   "Suc pc < length phi"
-  assumes bounded: "bounded step (length phi)"
-  assumes esl:     "err_semilat (A, r, f)"
-  assumes cert_ok: "cert_ok cert (length phi) A"
-  assumes phi_ok:  "\<forall>pc < length phi. phi!pc \<in> opt A"
-  assumes pres:    "pres_type step (length phi) (err (opt A))" 
-  shows "OK s \<le>|r OK (phi!Suc pc)"
-proof (cases "cert!pc")
-  case None with cert 
-  have "wtl_inst cert f r step pc (phi!pc) = OK s" by (simp add: wtl_cert_def)
-  thus ?thesis by - (rule wtl_less)
+lemma (in lbvc) wtc_less:
+  assumes stable: "stable r step \<phi> pc"
+  assumes suc_pc: "Suc pc < length \<phi>"
+  shows "wtc c pc (\<phi>!pc) <=_r \<phi>!Suc pc" (is "?wtc <=_r _")
+proof (cases "c!pc = \<bottom>")
+  case True
+  moreover have "wti c pc (\<phi>!pc) <=_r \<phi>!Suc pc" by (rule wti_less)
+  ultimately show ?thesis by (simp add: wtc)
 next
-  case (Some s') with cert 
-  have "wtl_inst cert f r step pc (Some s') = OK s" 
-    by (simp add: wtl_cert_def split: split_if_asm)
-  also
-  from suc_pc have "pc < length phi" by simp
-  with fits Some have "cert!pc = phi!pc" by - (rule fitsD2)
-  with Some have "Some s' = phi!pc" by simp
-  finally
-  have "wtl_inst cert f r step pc (phi!pc) = OK s" .
-  thus ?thesis by - (rule wtl_less)
+  case False
+  from suc_pc have pc: "pc < length \<phi>" by simp
+  hence "?wtc \<noteq> \<top>" by - (rule stable_wtc)
+  with False have "?wtc = wti c pc (c!pc)" 
+    by (unfold wtc) (simp split: split_if_asm)
+  also from pc False have "c!pc = \<phi>!pc" .. 
+  finally have "?wtc = wti c pc (\<phi>!pc)" .
+  also have "wti c pc (\<phi>!pc) <=_r \<phi>!Suc pc" by (rule wti_less)
+  finally show ?thesis .
 qed
 
 
-  
-lemma wt_step_wtl_lemma:
-  assumes wt_step: "wt_step (Err.le (Opt.le r)) Err step (map OK phi)"
-  assumes fits:    "fits step cert phi"  
-  assumes bounded: "bounded step (length phi)"
-  assumes esl:     "err_semilat (A, r, f)"
-  assumes cert_ok: "cert_ok cert (length phi) A"
-  assumes phi_ok:  "\<forall>pc < length phi. phi!pc \<in> opt A"
-  assumes pres:    "pres_type step (length phi) (err (opt A))" 
-  assumes mono:    "mono (Err.le (Opt.le r)) step (length phi) (err (opt A))"
-  shows "\<And>pc s. pc+length ins = length phi \<Longrightarrow> OK s \<le>|r OK (phi!pc) \<Longrightarrow> s \<in> opt A \<Longrightarrow>
-                wtl_inst_list ins cert f r step pc s \<noteq> Err"
-  (is "\<And>pc s. _ \<Longrightarrow> _ \<Longrightarrow> _ \<Longrightarrow> ?wtl ins pc s \<noteq> Err")
-proof (induct ins)
-  fix pc s show "?wtl [] pc s \<noteq> Err" by simp
+lemma (in lbvc) wt_step_wtl_lemma:
+  assumes wt_step: "wt_step r \<top> step \<phi>"
+  shows "\<And>pc s. pc+length ls = length \<phi> \<Longrightarrow> s <=_r \<phi>!pc \<Longrightarrow> s \<in> A \<Longrightarrow> s\<noteq>\<top> \<Longrightarrow>
+                wtl ls c pc s \<noteq> \<top>"
+  (is "\<And>pc s. _ \<Longrightarrow> _ \<Longrightarrow> _ \<Longrightarrow> _ \<Longrightarrow> ?wtl ls pc s \<noteq> _")
+proof (induct ls)
+  fix pc s assume "s\<noteq>\<top>" thus "?wtl [] pc s \<noteq> \<top>" by simp
 next
-  fix pc s i ins
-  assume "\<And>pc s. pc+length ins=length phi \<Longrightarrow> OK s \<le>|r OK (phi!pc) \<Longrightarrow> s \<in> opt A \<Longrightarrow>
-                 ?wtl ins pc s \<noteq> Err"
+  fix pc s i ls
+  assume "\<And>pc s. pc+length ls=length \<phi> \<Longrightarrow> s <=_r \<phi>!pc \<Longrightarrow> s \<in> A \<Longrightarrow> s\<noteq>\<top> \<Longrightarrow> 
+                  ?wtl ls pc s \<noteq> \<top>"
   moreover
-  assume pc_l: "pc + length (i#ins) = length phi"
-  hence suc_pc_l: "Suc pc + length ins = length phi" by simp
+  assume pc_l: "pc + length (i#ls) = length \<phi>"
+  hence suc_pc_l: "Suc pc + length ls = length \<phi>" by simp
   ultimately
-  have IH: 
-    "\<And>s. OK s \<le>|r OK (phi!Suc pc) \<Longrightarrow> s \<in> opt A \<Longrightarrow> ?wtl ins (Suc pc) s \<noteq> Err" .
+  have IH: "\<And>s. s <=_r \<phi>!Suc pc \<Longrightarrow> s \<in> A \<Longrightarrow> s \<noteq> \<top> \<Longrightarrow> ?wtl ls (Suc pc) s \<noteq> \<top>" .
 
-  from pc_l obtain pc: "pc < length phi" by simp
-  with wt_step 
-  have stable: "stable (Err.le (Opt.le r)) step (map OK phi) pc" 
-    by (simp add: wt_step_def)
+  from pc_l obtain pc: "pc < length \<phi>" by simp
+  with wt_step have stable: "stable r step \<phi> pc" by (simp add: wt_step_def)
   moreover
-  assume s_phi: "OK s \<le>|r OK (phi!pc)"
+  assume s_phi: "s <=_r \<phi>!pc"
   ultimately 
-  have "wtl_cert cert f r step pc (phi!pc) \<noteq> Err" by - (rule stable_cert)
-  then obtain s'' where s'': "wtl_cert cert f r step pc (phi!pc) = OK s''" by fast
+  have wt_phi: "wtc c pc (\<phi>!pc) \<noteq> \<top>" by - (rule stable_wtc)
+
+  from phi pc have phi_pc: "\<phi>!pc \<in> A" by simp
   moreover 
-  from phi_ok pc 
-  have phi_pc: "phi!pc \<in> opt A" by simp
-  moreover 
-  assume s: "s \<in> opt A"
+  assume s: "s \<in> A"
   ultimately
-  obtain s' where "wtl_cert cert f r step pc s = OK s'"
-    by - (drule wtl_cert_mono, assumption+, blast)
-  hence "ins = [] \<Longrightarrow> ?wtl (i#ins) pc s \<noteq> Err" by simp
+  have wt_s_phi: "wtc c pc s <=_r wtc c pc (\<phi>!pc)" using s_phi by - (rule wtc_mono)
+  with wt_phi have wt_s: "wtc c pc s \<noteq> \<top>" by simp
+  moreover
+  assume s: "s \<noteq> \<top>" 
+  ultimately
+  have "ls = [] \<Longrightarrow> ?wtl (i#ls) pc s \<noteq> \<top>" by simp
   moreover {
-    assume "ins \<noteq> []" 
-    with pc_l have suc_pc: "Suc pc < length phi" by (auto simp add: neq_Nil_conv)
-    with stable s'' have "OK s'' \<le>|r OK (phi!Suc pc)" by - (rule cert_less)
+    assume "ls \<noteq> []" 
+    with pc_l have suc_pc: "Suc pc < length \<phi>" by (auto simp add: neq_Nil_conv)
+    with stable have "wtc c pc (phi!pc) <=_r \<phi>!Suc pc" by (rule wtc_less)
+    with wt_s_phi have "wtc c pc s <=_r \<phi>!Suc pc" by (rule trans_r)      
     moreover
-    from s'' s_phi obtain s' where 
-      cert: "wtl_cert cert f r step pc s = OK s'" and
-      "OK s' \<le>|r OK s''"
-      using phi_pc
-      by - (drule wtl_cert_mono, assumption+, blast)
-    moreover from esl have "order (Err.le (Opt.le r))" by simp
-    ultimately have less: "OK s' \<le>|r OK (phi!Suc pc)" by - (rule order_trans)
-
-    from cert_ok suc_pc have "cert!pc \<in> opt A" and "cert!(pc+1) \<in> opt A" 
+    from cert suc_pc have "c!pc \<in> A" "c!(pc+1) \<in> A" 
       by (auto simp add: cert_ok_def)
-    with s cert pres have "s' \<in> opt A" by - (rule wtl_cert_pres) 
-
-    with less IH have "?wtl ins (Suc pc) s' \<noteq> Err" by blast
-    with cert have "?wtl (i#ins) pc s \<noteq> Err" by simp 
+    with pres have "wtc c pc s \<in> A" by (rule wtc_pres)
+    ultimately
+    have "?wtl ls (Suc pc) (wtc c pc s) \<noteq> \<top>" using IH wt_s by blast
+    with s wt_s have "?wtl (i#ls) pc s \<noteq> \<top>" by simp 
   }
-  ultimately show "?wtl (i#ins) pc s \<noteq> Err" by (cases ins) auto 
+  ultimately show "?wtl (i#ls) pc s \<noteq> \<top>" by (cases ls) blast+
 qed
 
-
-theorem wtl_complete:
-  assumes "wt_step (Err.le (Opt.le r)) Err step (map OK phi)"
-  assumes "OK s \<le>|r OK (phi!0)" and "s \<in> opt A"
-  defines cert:  "cert \<equiv> make_cert step phi"
-
-  assumes "bounded step (length phi)" and "err_semilat (A, r, f)"
-  assumes "pres_type step (length phi) (err (opt A))" 
-  assumes "mono (Err.le (Opt.le r)) step (length phi) (err (opt A))"
-  assumes "length ins = length phi"
-  assumes phi_ok:  "\<forall>pc < length phi. phi!pc \<in> opt A"
-
-  shows "wtl_inst_list ins cert f r step 0 s \<noteq> Err"
-proof -
+  
+theorem (in lbvc) wtl_complete:
+  assumes "wt_step r \<top> step \<phi>"
+  assumes "s <=_r \<phi>!0" and "s \<in> A" and "s \<noteq> \<top>" and "length ins = length phi"
+  shows "wtl ins c 0 s \<noteq> \<top>"
+proof -  
   have "0+length ins = length phi" by simp
-  moreover
-  have "fits step cert phi" by (unfold cert) (rule fits_make_cert)
-  moreover
-  from phi_ok have "cert_ok cert (length phi) A"
-    by (simp add: cert make_cert_def cert_ok_def nth_append)
-  ultimately
-  show ?thesis by - (rule wt_step_wtl_lemma)
+  thus ?thesis by - (rule wt_step_wtl_lemma)
 qed
 
 
diff -r c2e4d9990162 -r 1dd711c6b93c src/HOL/MicroJava/BV/LBVCorrect.thy
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy	Thu Apr 04 16:47:44 2002 +0200
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy	Thu Apr 04 16:48:00 2002 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/MicroJava/BV/BVLCorrect.thy
+(*
     ID:         $Id$
     Author:     Gerwin Klein
     Copyright   1999 Technische Universitaet Muenchen
@@ -8,222 +8,150 @@
 
 theory LBVCorrect = LBVSpec + Typing_Framework:
 
-constdefs
-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)))"
-
-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   => ok_val (wtl_inst_list (take pc is) cert f r step 0 s0)
-             | Some t => Some t) [0..length is(]"
+locale lbvc = lbv +
+  fixes s0  :: 'a
+  fixes c   :: "'a list"
+  fixes ins :: "'b list"
+  fixes phi :: "'a list" ("\<phi>")
+  defines phi_def:
+  "\<phi> \<equiv>  map (\<lambda>pc. if c!pc = \<bottom> then wtl (take pc ins) c 0 s0 else c!pc) 
+        [0..length ins(]"
 
-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 [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:
-  "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 (in lbvc) phi_None [intro?]:
+  "\<lbrakk> pc < length ins; c!pc = \<bottom> \<rbrakk> \<Longrightarrow> \<phi> ! pc = wtl (take pc ins) c 0 s0"
+  by (simp add: phi_def)
 
-lemma make_phi_None:
-  "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 (in lbvc) phi_Some [intro?]:
+  "\<lbrakk> pc < length ins; c!pc \<noteq> \<bottom> \<rbrakk> \<Longrightarrow> \<phi> ! pc = c ! pc"
+  by (simp add: phi_def)
 
-lemma make_phi_len:
-  "length (make_phi cert f r step s0 is) = length is"
-  by (simp add: make_phi_def)
+lemma (in lbvc) phi_len [simp]:
+  "length \<phi> = length ins"
+  by (simp add: phi_def)
+
 
-lemma exists_phi:
-  "\<exists>phi. fits phi cert f r step s0 is"
-proof - 
-  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 [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 cert f r step 0 s \<noteq> Err"
-  then obtain s'' where
-    "wtl_inst_list (take pc is) cert f r step 0 s = OK s''" 
-    by (blast dest: wtl_take)
-  moreover
-  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)
+lemma (in lbvc) wtl_suc_pc:
+  assumes all: "wtl ins c 0 s0 \<noteq> \<top>" 
+  assumes pc:  "pc+1 < length ins"
+  shows "wtl (take (pc+1) ins) c 0 s0 <=_r \<phi>!(pc+1)"
+proof -
+  from all pc
+  have "wtc c (pc+1) (wtl (take (pc+1) ins) c 0 s0) \<noteq> T" by (rule wtl_all)
+  with pc show ?thesis by (simp add: phi_def wtc split: split_if_asm)
 qed
 
 
-lemma wtl_suc_pc:
+lemma (in lbvc) wtl_stable:
   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 -
-  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    
-
-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"
+    pres:    "pres_type step (length ins) A" and
+    s0_in_A: "s0 \<in> A" and
+    cert_ok: "cert_ok c (length ins) \<top> \<bottom> A" and
+    wtl:     "wtl ins c 0 s0 \<noteq> \<top>" and
+    pc:      "pc < length ins" and
+    bounded: "bounded step (length ins)"
+  shows "stable r step \<phi> pc"
 proof (unfold stable_def, clarify)
-  fix pc' s' assume step: "(pc',s') \<in> set (step pc ((map OK phi) ! pc))" 
+  fix pc' s' assume step: "(pc',s') \<in> set (step pc (\<phi> ! pc))" 
                       (is "(pc',s') \<in> set (?step pc)")
   
-  from step pc bounded have pc': "pc' < length is"
+  from step pc bounded have pc': "pc' < length ins"
     by (unfold bounded_def) blast
+
+  have tkpc: "wtl (take pc ins) c 0 s0 \<noteq> \<top>" (is "?s1 \<noteq> _") by (rule wtl_take)
+  have s2: "wtl (take (pc+1) ins) c 0 s0 \<noteq> \<top>" (is "?s2 \<noteq> _") by (rule wtl_take)
   
-  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 wtl pc have cert: "wtc c pc ?s1 \<noteq> \<top>" by (rule wtl_all)
 
-  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" ..
+  have c_Some: "\<forall>pc t. pc < length ins \<longrightarrow> c!pc \<noteq> \<bottom> \<longrightarrow> \<phi>!pc = c!pc" 
+    by (simp add: phi_def)
+  have c_None: "c!pc = \<bottom> \<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)
+  from cert pc c_None c_Some
+  have inst: "wtc c pc ?s1  = wti c pc (\<phi>!pc)"
+    by (simp add: wtc split: split_if_asm)
 
-  have "s1 \<in> opt A" by (rule wtl_inst_list_pres)
+  have "?s1 \<in> A" by (rule wtl_pres) 
   with pc c_Some cert_ok c_None
-  have "phi!pc \<in> opt A" by (cases "cert!pc") (auto dest: cert_okD1)
+  have "\<phi>!pc \<in> A" by (cases "c!pc = \<bottom>") (auto dest: cert_okD1)
   with pc pres
-  have step_in_A: "\<forall>(pc',s') \<in> set (?step pc). s' \<in> err (opt A)" 
-    by (auto dest: pres_typeD)
+  have step_in_A: "snd`set (?step pc) \<subseteq> A" by (auto dest: pres_typeD2)
 
-  show "s' \<le>|r (map OK phi) ! pc'"
+  show "s' <=_r \<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_okD1)
-    from inst 
-    have ok: "OK s2 = merge cert f r pc (?step pc) (OK (cert!(pc+1)))" 
-      by (simp add: wtl_inst_def)
+    have cert_in_A: "c!(pc+1) \<in> A" by (auto dest: cert_okD1)
+    from True pc' have pc1: "pc+1 < length ins" by simp
+    with tkpc have "?s2 = wtc c pc ?s1" by - (rule wtl_Suc)
+    with inst 
+    have merge: "?s2 = merge c pc (?step pc) (c!(pc+1))" by (simp add: wti)
     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)
+    from s2 merge have "\<dots> \<noteq> \<top>" (is "?merge \<noteq> _") by simp
+    with cert_in_A step_in_A
+    have "?merge = (map snd [(p',t')\<in>?step pc. p'=pc+1] ++_f (c!(pc+1)))"
+      by (rule merge_not_top_s) 
     finally
-    have "s' \<le>|r OK s2" 
-      using semi step_in_A cert_in_A True step by (auto intro: ub1')
+    have "s' <=_r ?s2" using step_in_A cert_in_A True step 
+      by (auto intro: pp_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)
+    from wtl pc1 have "?s2 <=_r \<phi>!(pc+1)" by (rule wtl_suc_pc)
     also note True [symmetric]
-    finally show ?thesis by simp
+    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)
+    from cert inst
+    have "merge c pc (?step pc) (c!(pc+1)) \<noteq> \<top>" by (simp add: wti)
+    with step_in_A
+    have "\<forall>(pc', s')\<in>set (?step pc). pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'" 
+      by - (rule merge_not_top)
     with step False 
-    have ok: "s' \<le>|r (OK (cert!pc'))" by blast
+    have ok: "s' <=_r c!pc'" by blast
     moreover
     from ok
-    have "cert!pc' = None \<longrightarrow> s' = OK None" by auto
+    have "c!pc' = \<bottom> \<Longrightarrow> s' = \<bottom>" by simp
     moreover
     from c_Some pc'
-    have "cert!pc' \<noteq> None \<longrightarrow> phi!pc' = cert!pc'" by auto
+    have "c!pc' \<noteq> \<bottom> \<Longrightarrow> \<phi>!pc' = c!pc'" by auto
     ultimately
-    show ?thesis by auto
+    show ?thesis by (cases "c!pc' = \<bottom>") auto 
   qed
 qed
 
+  
+lemma (in lbvc) phi_not_top:
+  assumes wtl: "wtl ins c 0 s0 \<noteq> \<top>"
+  assumes crt: "cert_ok c (length ins) \<top> \<bottom> A"
+  assumes pc: "pc < length ins"
+  shows "\<phi>!pc \<noteq> \<top>"
+proof (cases "c!pc = \<bottom>")
+  case False with pc
+  have "\<phi>!pc = c!pc" ..
+  also from crt pc have "\<dots> \<noteq> \<top>" by (rule cert_okD4)
+  finally show ?thesis .
+next
+  case True with pc
+  have "\<phi>!pc = wtl (take pc ins) c 0 s0" ..
+  also from wtl have "\<dots> \<noteq> \<top>" by (rule wtl_take)
+  finally show ?thesis .
+qed
+    
 
-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
-
-  
-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 ..
+theorem (in lbvc) wtl_sound:
+  assumes "wtl ins c 0 s0 \<noteq> \<top>" 
+  assumes "bounded step (length ins)"
+  assumes "s0 \<in> A" and "cert_ok c (length ins) \<top> \<bottom> A"
+  assumes "pres_type step (length ins) A"
+  shows "\<exists>ts. wt_step r \<top> step ts"
+proof -  
+  have "wt_step r \<top> step \<phi>"
+  proof (unfold wt_step_def, intro strip conjI)
+    fix pc assume "pc < length \<phi>"
+    then obtain "pc < length ins" by simp
+    show "\<phi>!pc \<noteq> \<top>" by (rule phi_not_top)
+    show "stable r step \<phi> pc" by (rule wtl_stable)
+  qed    
+  thus ?thesis .. 
 qed
 
-
-end
+end
\ No newline at end of file
diff -r c2e4d9990162 -r 1dd711c6b93c src/HOL/MicroJava/BV/LBVSpec.thy
--- a/src/HOL/MicroJava/BV/LBVSpec.thy	Thu Apr 04 16:47:44 2002 +0200
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy	Thu Apr 04 16:48:00 2002 +0200
@@ -8,252 +8,272 @@
 
 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) 
-
-  "@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
-  's certificate = "'s option list"   
-  's steptype    = "'s option err step_type"
+  's certificate = "'s list"   
 
 consts
-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"
+merge :: "'s certificate \<Rightarrow> 's binop \<Rightarrow> 's ord \<Rightarrow> 's \<Rightarrow> nat \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's \<Rightarrow> 's"
 primrec
-"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))"
+"merge cert f r T pc []     x = x"
+"merge cert f r T pc (s#ss) x = merge cert f r T pc ss (let (pc',s') = s in 
+                                  if pc'=pc+1 then s' +_f x
+                                  else if s' <=_r (cert!pc') then x
+                                  else T)"
 
 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_inst :: "'s certificate \<Rightarrow> 's binop \<Rightarrow> 's ord \<Rightarrow> 's \<Rightarrow>
+             's step_type \<Rightarrow> nat \<Rightarrow> 's \<Rightarrow> 's"
+"wtl_inst cert f r T step pc s \<equiv> merge cert f r T pc (step pc s) (cert!(pc+1))"
 
-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"
+wtl_cert :: "'s certificate \<Rightarrow> 's binop \<Rightarrow> 's ord \<Rightarrow> 's \<Rightarrow> 's \<Rightarrow>
+             's step_type \<Rightarrow> nat \<Rightarrow> 's \<Rightarrow> 's"
+"wtl_cert cert f r T B step pc s \<equiv>
+  if cert!pc = B then 
+    wtl_inst cert f r T step pc s
+  else
+    if s <=_r (cert!pc) then wtl_inst cert f r T step pc (cert!pc) else T"
 
 consts 
-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"
+wtl_inst_list :: "'a list \<Rightarrow> 's certificate \<Rightarrow> 's binop \<Rightarrow> 's ord \<Rightarrow> 's \<Rightarrow> 's \<Rightarrow>
+                  's step_type \<Rightarrow> nat \<Rightarrow> 's \<Rightarrow> 's"
 primrec
-"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')"
-
+"wtl_inst_list []      cert f r T B step pc s = s"
+"wtl_inst_list (i#ins) cert f r T B step pc s = 
+    (let s' = wtl_cert cert f r T B step pc s in
+      if s' = T \<or> s = T then T else wtl_inst_list ins cert f r T B step (pc+1) s')"
 
 
 constdefs
-  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) \<and> (cert!n = None)"
+  cert_ok :: "'s certificate \<Rightarrow> nat \<Rightarrow> 's \<Rightarrow> 's \<Rightarrow> 's set \<Rightarrow> bool"
+  "cert_ok cert n T B A \<equiv> (\<forall>i < n. cert!i \<in> A \<and> cert!i \<noteq> T) \<and> (cert!n = B)"
+
+constdefs
+  bottom :: "'a ord \<Rightarrow> 'a \<Rightarrow> bool"
+  "bottom r B \<equiv> \<forall>x. B <=_r x"
+
+
+locale lbv = semilat +
+  fixes T :: "'a" ("\<top>") 
+  fixes B :: "'a" ("\<bottom>") 
+  fixes step :: "'a step_type" 
+  assumes top: "top r \<top>"
+  assumes T_A: "\<top> \<in> A"
+  assumes bot: "bottom r \<bottom>" 
+  assumes B_A: "\<bottom> \<in> A"
+
+  fixes merge :: "'a certificate \<Rightarrow> nat \<Rightarrow> (nat \<times> 'a) list \<Rightarrow> 'a \<Rightarrow> 'a"
+  defines mrg_def: "merge cert \<equiv> LBVSpec.merge cert f r \<top>"
 
-lemma cert_okD1:
-  "cert_ok cert n A \<Longrightarrow> pc < n \<Longrightarrow> cert!pc \<in> opt A"
+  fixes wti :: "'a certificate \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"
+  defines wti_def: "wti cert \<equiv> wtl_inst cert f r \<top> step"
+ 
+  fixes wtc :: "'a certificate \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"
+  defines wtc_def: "wtc cert \<equiv> wtl_cert cert f r \<top> \<bottom> step"
+
+  fixes wtl :: "'b list \<Rightarrow> 'a certificate \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"
+  defines wtl_def: "wtl ins cert \<equiv> wtl_inst_list ins cert f r \<top> \<bottom> step"
+
+
+lemma (in lbv) wti:
+  "wti c pc s \<equiv> merge c pc (step pc s) (c!(pc+1))"
+  by (simp add: wti_def mrg_def wtl_inst_def)
+
+lemma (in lbv) wtc: 
+  "wtc c pc s \<equiv> if c!pc = \<bottom> then wti c pc s else if s <=_r c!pc then wti c pc (c!pc) else \<top>"
+  by (unfold wtc_def wti_def wtl_cert_def)
+
+
+lemma cert_okD1 [intro?]:
+  "cert_ok c n T B A \<Longrightarrow> pc < n \<Longrightarrow> c!pc \<in> A"
   by (unfold cert_ok_def) fast
 
-lemma cert_okD2:
-  "cert_ok cert n A \<Longrightarrow> cert!n = None"
+lemma cert_okD2 [intro?]:
+  "cert_ok c n T B A \<Longrightarrow> c!n = B"
   by (simp add: cert_ok_def)
 
-lemma cert_okD3:
-  "cert_ok cert n A \<Longrightarrow> pc < n \<Longrightarrow> cert!Suc pc \<in> opt A"
+lemma cert_okD3 [intro?]:
+  "cert_ok c n T B A \<Longrightarrow> B \<in> A \<Longrightarrow> pc < n \<Longrightarrow> c!Suc pc \<in> A"
   by (drule Suc_leI) (auto simp add: le_eq_less_or_eq dest: cert_okD1 cert_okD2)
 
+lemma cert_okD4 [intro?]:
+  "cert_ok c n T B A \<Longrightarrow> pc < n \<Longrightarrow> c!pc \<noteq> T"
+  by (simp add: cert_ok_def)
 
 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"
+
+lemma (in lbv) sup_top [simp, elim]:
+  assumes x: "x \<in> A" 
+  shows "x +_f \<top> = \<top>"
 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)
+  from top have "x +_f \<top> <=_r \<top>" ..
+  moreover from x have "\<top> <=_r x +_f \<top>" ..
+  ultimately show ?thesis ..
 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"
+lemma (in lbv) plusplussup_top [simp, elim]:
+  "set xs \<subseteq> A \<Longrightarrow> xs ++_f \<top> = \<top>"
   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 semilat.orderI)
-  apply assumption
-  done
+lemma (in semilat) pp_ub1':
+  assumes S: "snd`set S \<subseteq> A" 
+  assumes y: "y \<in> A" and ab: "(a, b) \<in> set S" 
+  shows "b <=_r map snd [(p', t')\<in>S . p' = a] ++_f y"
+proof -
+  from S have "\<forall>(x,y) \<in> set S. y \<in> A" by auto
+  with semilat y ab show ?thesis by - (rule ub1')
+qed 
 
-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 (in lbv) bottom_le [simp, intro]:
+  "\<bottom> <=_r x"
+  by (insert bot) (simp add: bottom_def)
 
-lemma plusplus_erropt_Err [simp]:
-  "xs ++|f Err = Err"
-  by (induct xs) auto
+lemma (in lbv) le_bottom [simp]:
+  "x <=_r \<bottom> = (x = \<bottom>)"
+  by (blast intro: antisym_r)
+
 
 
 section "merge"
 
-lemma merge_Err [simp]:
-  "merge cert f r pc ss Err = Err"
+lemma (in lbv) merge_Nil [simp]:
+  "merge c pc [] x = x" by (simp add: mrg_def)
+
+lemma (in lbv) merge_Cons [simp]:
+  "merge c pc (l#ls) x = merge c pc ls (if fst l=pc+1 then snd l +_f x
+                                        else if snd l <=_r (c!fst l) then x
+                                        else \<top>)"
+  by (simp add: mrg_def split_beta)
+
+lemma (in lbv) merge_Err [simp]:
+  "snd`set ss \<subseteq> A \<Longrightarrow> merge c pc ss \<top> = \<top>"
   by (induct ss) auto
 
-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")
+lemma (in lbv) merge_not_top:
+  "\<And>x. snd`set ss \<subseteq> A \<Longrightarrow> merge c pc ss x \<noteq> \<top> \<Longrightarrow> 
+  \<forall>(pc',s') \<in> set ss. (pc' \<noteq> pc+1 \<longrightarrow> s' <=_r (c!pc'))"
+  (is "\<And>x. ?set ss \<Longrightarrow> ?merge ss x \<Longrightarrow> ?P ss")
 proof (induct ss)
   show "?P []" by simp
 next
-  fix x l ls assume merge: "?merge (l#ls) x"
+  fix x ls l
+  assume "?set (l#ls)" then obtain set: "snd`set ls \<subseteq> A" by simp
+  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" .
+  obtain x' where "?merge ls x'" by simp 
+  assume "\<And>x. ?set ls \<Longrightarrow> ?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)
+  from merge set
+  have "pc' \<noteq> pc+1 \<longrightarrow> s' <=_r (c!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)" 
+lemma (in lbv) merge_def:
   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)" 
+  "\<And>x. x \<in> A \<Longrightarrow> snd`set ss \<subseteq> A \<Longrightarrow>
+  merge c pc ss x = 
+  (if \<forall>(pc',s') \<in> set ss. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc' then
+    map snd [(p',t') \<in> ss. p'=pc+1] ++_f x
+  else \<top>)" 
   (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" .
+  fix x assume x: "x \<in> A" 
+  fix l::"nat \<times> 'a" and ls  
+  assume "snd`set (l#ls) \<subseteq> A"
+  then obtain l: "snd l \<in> A" and ls: "snd`set ls \<subseteq> A" by auto
+  assume "\<And>x. x \<in> A \<Longrightarrow> snd`set ls \<subseteq> A \<Longrightarrow> ?P ls x" 
+  hence IH: "\<And>x. x \<in> 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)"
+    (if pc'=pc+1 then s' +_f x else if s' <=_r c!pc' then x else \<top>)"
     (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: semilat.closedI closedD)
-    with x have "?if' \<in> err (opt A)" by auto
+    from l have "s' \<in> A" by simp
+    with x have "s' +_f x \<in> A" by simp
+    with x have "?if' \<in> 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')")
+    proof (cases "\<forall>(pc', s')\<in>set (l#ls). pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'")
       case True
-      hence "\<forall>(pc', s')\<in>set ls. pc' \<noteq> pc + 1 \<longrightarrow> s' \<le>|r (OK (cert ! pc'))" by auto
+      hence "\<forall>(pc', s')\<in>set ls. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!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)"
+        "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
+      case False 
+      moreover
+      from ls have "set (map snd [(p', t')\<in>ls . p' = Suc pc]) \<subseteq> A" by auto
+      ultimately show ?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)"
+lemma (in lbv) merge_not_top_s:
+  assumes x:  "x \<in> A" and ss: "snd`set ss \<subseteq> A"
+  assumes m:  "merge c pc ss x \<noteq> \<top>"
+  shows "merge c 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)
+  from ss m have "\<forall>(pc',s') \<in> set ss. (pc' \<noteq> pc+1 \<longrightarrow> s' <=_r c!pc')" 
+    by (rule merge_not_top)
+  with 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 wtl_Cons:
-  "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)"
+lemma (in lbv) wtl_Nil [simp]: "wtl [] c pc s = s" 
+  by (simp add: wtl_def)
+
+lemma (in lbv) wtl_Cons [simp]: 
+  "wtl (i#is) c pc s = 
+  (let s' = wtc c pc s in if s' = \<top> \<or> s = \<top> then \<top> else wtl is c (pc+1) s')"
+  by (simp add: wtl_def wtc_def)
+
+lemma (in lbv) wtl_Cons_not_top:
+  "wtl (i#is) c pc s \<noteq> \<top> = 
+  (wtc c pc s \<noteq> \<top> \<and> s \<noteq> T \<and> wtl is c (pc+1) (wtc c pc s) \<noteq> \<top>)"
   by (auto simp del: split_paired_Ex)
 
-lemma wtl_append:
-"\<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
-  fix x xs  assume IH: "?P xs"
-  show "?P (x#xs)"
-  proof (intro allI)
-    fix s pc 
-    show "?C s pc (x#xs)"
-    proof (cases "wtl_cert cert f r step pc s")
-      case Err thus ?thesis by simp
-    next
-      case (OK s0)
-      with IH have "?C s0 (pc+1) xs" by blast
-      thus ?thesis by (simp!)
-    qed
-  qed
-qed
+lemma (in lbv) wtl_top [simp]:  "wtl ls c pc \<top> = \<top>"
+  by (cases ls) auto
+
+lemma (in lbv) wtl_not_top:
+  "wtl ls c pc s \<noteq> \<top> \<Longrightarrow> s \<noteq> \<top>"
+  by (cases "s=\<top>") auto
 
-lemma wtl_take:
-  "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> _")
+lemma (in lbv) wtl_append [simp]:
+  "\<And>pc s. wtl (a@b) c pc s = wtl b c (pc+length a) (wtl a c pc s)"
+  by (induct a) auto
+
+lemma (in lbv) wtl_take:
+  "wtl is c pc s \<noteq> \<top> \<Longrightarrow> wtl (take pc' is) c pc s \<noteq> \<top>"
+  (is "?wtl is \<noteq> _ \<Longrightarrow> _")
 proof -
-  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)
+  assume "?wtl is \<noteq> \<top>"
+  hence "?wtl (take pc' is @ drop pc' is) \<noteq> \<top>" by simp  
+  thus ?thesis by (auto dest!: wtl_not_top simp del: append_take_drop_id)
 qed
 
 lemma take_Suc:
-  "\<forall>n. n < length l --> take (Suc n) l = (take n l)@[l!n]" (is "?P l")
+  "\<forall>n. n < length l \<longrightarrow> take (Suc n) l = (take n l)@[l!n]" (is "?P l")
 proof (induct l)
   show "?P []" by simp
 next
@@ -266,137 +286,96 @@
   qed
 qed
 
-lemma wtl_Suc:
-  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''"    
+lemma (in lbv) wtl_Suc:
+  assumes suc: "pc+1 < length is"
+  assumes wtl: "wtl (take pc is) c 0 s \<noteq> \<top>"
+  shows "wtl (take (pc+1) is) c 0 s = wtc c pc (wtl (take pc is) c 0 s)"
 proof -
   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)
+  with suc wtl show ?thesis by (simp add: min_def)
 qed
 
-lemma wtl_all:
-  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''"
+lemma (in lbv) wtl_all:
+  assumes all: "wtl is c 0 s \<noteq> \<top>" (is "?wtl is \<noteq> _") 
+  assumes pc:  "pc < length is"
+  shows  "wtc c pc (wtl (take pc is) c 0 s) \<noteq> \<top>"
 proof -
   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 (take pc is@i#r) \<noteq> Err" by simp 
+  with all have take: "?wtl (take pc is@i#r) \<noteq> \<top>" 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)
+  with take pc show ?thesis by (auto simp add: min_def split: split_if_asm)
 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"
+lemma (in lbv) merge_pres:
+  assumes s0: "snd`set ss \<subseteq> A" and x: "x \<in> A"
+  shows "merge c pc ss x \<in> 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)"
+  from s0 have "set (map snd [(p', t')\<in>ss . p'=pc+1]) \<subseteq> A" by auto
+  with x  have "(map snd [(p', t')\<in>ss . p'=pc+1] ++_f x) \<in> 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
+  with s0 x show ?thesis by (simp add: merge_def T_A)
 qed
   
 
+lemma pres_typeD2:
+  "pres_type step n A \<Longrightarrow> s \<in> A \<Longrightarrow> p < n \<Longrightarrow> snd`set (step p s) \<subseteq> A"
+  by auto (drule pres_typeD)
 
-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"
+
+lemma (in lbv) wti_pres [intro?]:
+  assumes pres: "pres_type step n A" 
+  assumes cert: "c!(pc+1) \<in> A"
+  assumes s_pc: "s \<in> A" "pc < n"
+  shows "wti c pc s \<in> 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)
+  from pres s_pc have "snd`set (step pc s) \<subseteq> A" by (rule pres_typeD2)
+  with cert show ?thesis by (simp add: wti 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"            
+lemma (in lbv) wtc_pres:
+  assumes "pres_type step n A"
+  assumes "c!pc \<in> A" and "c!(pc+1) \<in> A"
+  assumes "s \<in> A" and "pc < n"
+  shows "wtc c pc s \<in> 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)
+  have "wti c pc s \<in> A" ..
+  moreover have "wti c pc (c!pc) \<in> A" ..
+  ultimately show ?thesis using T_A by (simp add: wtc) 
 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'")
+
+lemma (in lbv) wtl_pres:
+  assumes pres: "pres_type step (length is) A"
+  assumes cert: "cert_ok c (length is) \<top> \<bottom> A"
+  assumes s:    "s \<in> A" 
+  assumes all:  "wtl is c 0 s \<noteq> \<top>"
+  shows "pc < length is \<Longrightarrow> wtl (take pc is) c 0 s \<in> A"
+  (is "?len pc \<Longrightarrow> ?wtl pc \<in> A")
 proof (induct pc)
-  from s show "\<And>s'. ?wtl 0 s' \<Longrightarrow> ?A s'" by simp
+  from s show "?wtl 0 \<in> A" 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'"
+  fix n assume "Suc n < length is"
+  then obtain n: "n < length is" by simp  
+  assume "n < length is \<Longrightarrow> ?wtl n \<in> A"
+  hence "?wtl n \<in> A" .
+  moreover
+  from cert have "c!n \<in> A" by (rule cert_okD1)
   moreover
   have n1: "n+1 < length is" by simp
-  hence "?wtl (n+1) s2" by - (rule wtl_Suc)
+  with cert have "c!(n+1) \<in> A" by (rule cert_okD1)
   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_okD1)
-  moreover
-  from cert n1 have "cert!(n+1) \<in> opt A" by (rule cert_okD1)
-  ultimately
-  have "s2 \<in> opt A" using semi pres by - (rule wtl_cert_pres)
-  thus "s' \<in> opt A" by simp
+  have "wtc c n (?wtl n) \<in> A" by - (rule wtc_pres)
+  also
+  from all n have "?wtl n \<noteq> \<top>" by - (rule wtl_take)
+  with n1 have "wtc c n (?wtl n) = ?wtl (n+1)" by (rule wtl_Suc [symmetric])
+  finally  show "?wtl (Suc n) \<in> A" by simp
 qed