# HG changeset patch
# User kleing
# Date 1016975181 -3600
# Node ID b57d926d1de26320ea0e73e8fec7084cc8cd5283
# Parent  d6585b32412bab4ee97602671d1578d3dc93fc57
cleanup + simpler monotonicity

diff -r d6585b32412b -r b57d926d1de2 src/HOL/MicroJava/BV/Effect.thy
--- a/src/HOL/MicroJava/BV/Effect.thy	Sun Mar 24 14:05:53 2002 +0100
+++ b/src/HOL/MicroJava/BV/Effect.thy	Sun Mar 24 14:06:21 2002 +0100
@@ -184,6 +184,32 @@
   "app i G maxs rT pc et s == case s of None \<Rightarrow> True | Some t \<Rightarrow> app' (i,G,pc,maxs,rT,t) \<and> xcpt_app i G pc et"
 
 
+lemma match_any_match_table:
+  "C \<in> set (match_any G pc et) \<Longrightarrow> match_exception_table G C pc et \<noteq> None"
+  apply (induct et)
+   apply simp
+  apply simp
+  apply clarify
+  apply (simp split: split_if_asm)
+  apply (auto simp add: match_exception_entry_def)
+  done
+
+lemma match_X_match_table:
+  "C \<in> set (match G X pc et) \<Longrightarrow> match_exception_table G C pc et \<noteq> None"
+  apply (induct et)
+   apply simp
+  apply (simp split: split_if_asm)
+  done
+
+lemma xcpt_names_in_et:
+  "C \<in> set (xcpt_names (i,G,pc,et)) \<Longrightarrow> 
+  \<exists>e \<in> set et. the (match_exception_table G C pc et) = fst (snd (snd e))"
+  apply (cases i)
+  apply (auto dest!: match_any_match_table match_X_match_table 
+              dest: match_exception_table_in_et)
+  done
+
+
 lemma 1: "2 < length a \<Longrightarrow> (\<exists>l l' l'' ls. a = l#l'#l''#ls)"
 proof (cases a)
   fix x xs assume "a = x#xs" "2 < length a"
diff -r d6585b32412b -r b57d926d1de2 src/HOL/MicroJava/BV/JVM.thy
--- a/src/HOL/MicroJava/BV/JVM.thy	Sun Mar 24 14:05:53 2002 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy	Sun Mar 24 14:06:21 2002 +0100
@@ -6,13 +6,17 @@
 
 header {* \isaheader{Kildall for the JVM}\label{sec:JVM} *}
 
-theory JVM = Kildall_Lift + JVMType + Opt + Product + Typing_Framework_err +
-             EffectMono + BVSpec:
+theory JVM = Kildall_Lift + JVMType + EffectMono + BVSpec:
+
 
 constdefs
+  check_bounded :: "instr list \<Rightarrow> exception_table \<Rightarrow> bool"
+  "check_bounded ins et \<equiv> (\<forall>pc < length ins. \<forall>pc' \<in> set (succs (ins!pc) pc). pc' < length ins) \<and>
+                          (\<forall>e \<in> set et. fst (snd (snd e)) < length ins)"
+
   exec :: "jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> instr list \<Rightarrow> state step_type"
   "exec G maxs rT et bs == 
-  err_step (\<lambda>pc. app (bs!pc) G maxs rT pc et) (\<lambda>pc. eff (bs!pc) G pc et)"
+  err_step (size bs) (\<lambda>pc. app (bs!pc) G maxs rT pc et) (\<lambda>pc. eff (bs!pc) G pc et)"
 
   kiljvm :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> 
              instr list \<Rightarrow> state list \<Rightarrow> state list"
@@ -22,7 +26,7 @@
   wt_kil :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 
              exception_table \<Rightarrow> instr list \<Rightarrow> bool"
   "wt_kil G C pTs rT mxs mxl et ins ==
-   bounded (exec G mxs rT et ins) (size ins) \<and> 0 < size ins \<and> 
+   check_bounded ins et \<and> 0 < size ins \<and> 
    (let first  = Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err));
         start  = OK first#(replicate (size ins - 1) (OK None));
         result = kiljvm G mxs (1+size pTs+mxl) rT et ins start
@@ -33,6 +37,65 @@
   wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)). wt_kil G C (snd sig) rT maxs maxl et b) G"
 
 
+
+text {*
+  Executability of @{term check_bounded}:
+*}
+consts
+  list_all'_rec :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> bool"
+primrec
+  "list_all'_rec P n []     = True"
+  "list_all'_rec P n (x#xs) = (P x n \<and> list_all'_rec P (Suc n) xs)"
+
+constdefs
+  list_all' :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
+  "list_all' P xs \<equiv> list_all'_rec P 0 xs"
+
+lemma list_all'_rec:
+  "\<And>n. list_all'_rec P n xs = (\<forall>p < size xs. P (xs!p) (p+n))"
+  apply (induct xs)
+  apply auto
+  apply (case_tac p)
+  apply auto
+  done
+
+lemma list_all' [iff]:
+  "list_all' P xs = (\<forall>n < size xs. P (xs!n) n)"
+  by (unfold list_all'_def) (simp add: list_all'_rec)
+
+lemma list_all_ball:
+  "list_all P xs = (\<forall>x \<in> set xs. P x)"
+  by (induct xs) auto
+
+lemma [code]:
+  "check_bounded ins et = 
+  (list_all' (\<lambda>i pc. list_all (\<lambda>pc'. pc' < length ins) (succs i pc)) ins \<and> 
+   list_all (\<lambda>e. fst (snd (snd e)) < length ins) et)"
+  by (simp add: list_all_ball check_bounded_def)
+  
+text {*
+  Lemmas for Kildall instantiation
+*}
+
+lemma check_bounded_is_bounded:
+  "check_bounded ins et \<Longrightarrow> bounded (\<lambda>pc. eff (ins!pc) G pc et) (length ins)"
+  apply (unfold bounded_def eff_def)
+  apply clarify
+  apply simp
+  apply (unfold check_bounded_def)
+  apply clarify
+  apply (erule disjE)
+   apply blast
+  apply (erule allE, erule impE, assumption)
+  apply (unfold xcpt_eff_def)
+  apply clarsimp    
+  apply (drule xcpt_names_in_et)
+  apply clarify
+  apply (drule bspec, assumption)
+  apply simp
+  done
+   
+
 lemma special_ex_swap_lemma [iff]: 
   "(? X. (? n. X = A n & P n) & Q X) = (? n. Q(A n) & P n)"
   by blast
@@ -46,36 +109,6 @@
   "non_empty (\<lambda>pc. eff (bs!pc) G pc et)" 
   by (simp add: non_empty_def eff_def non_empty_succs)
 
-lemma listn_Cons_Suc [elim!]:
-  "l#xs \<in> list n A \<Longrightarrow> (\<And>n'. n = Suc n' \<Longrightarrow> l \<in> A \<Longrightarrow> xs \<in> list n' A \<Longrightarrow> P) \<Longrightarrow> P"
-  by (cases n) auto
-
-lemma listn_appendE [elim!]:
-  "a@b \<in> list n A \<Longrightarrow> (\<And>n1 n2. n=n1+n2 \<Longrightarrow> a \<in> list n1 A \<Longrightarrow> b \<in> list n2 A \<Longrightarrow> P) \<Longrightarrow> P" 
-proof -
-  have "\<And>n. a@b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n=n1+n2 \<and> a \<in> list n1 A \<and> b \<in> list n2 A"
-    (is "\<And>n. ?list a n \<Longrightarrow> \<exists>n1 n2. ?P a n n1 n2")
-  proof (induct a)
-    fix n assume "?list [] n"
-    hence "?P [] n 0 n" by simp
-    thus "\<exists>n1 n2. ?P [] n n1 n2" by fast
-  next
-    fix n l ls
-    assume "?list (l#ls) n"
-    then obtain n' where n: "n = Suc n'" "l \<in> A" and "ls@b \<in> list n' A" by fastsimp
-    assume "\<And>n. ls @ b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> ls \<in> list n1 A \<and> b \<in> list n2 A"
-    hence "\<exists>n1 n2. n' = n1 + n2 \<and> ls \<in> list n1 A \<and> b \<in> list n2 A" .
-    then obtain n1 n2 where "n' = n1 + n2" "ls \<in> list n1 A" "b \<in> list n2 A" by fast
-    with n have "?P (l#ls) n (n1+1) n2" by simp
-    thus "\<exists>n1 n2. ?P (l#ls) n n1 n2" by fastsimp
-  qed
-  moreover
-  assume "a@b \<in> list n A" "\<And>n1 n2. n=n1+n2 \<Longrightarrow> a \<in> list n1 A \<Longrightarrow> b \<in> list n2 A \<Longrightarrow> P"
-  ultimately
-  show ?thesis by blast
-qed
-
-
 theorem exec_pres_type:
   "wf_prog wf_mb S \<Longrightarrow> 
   pres_type (exec S maxs rT et bs) (size bs) (states S maxs maxr)"
@@ -172,15 +205,6 @@
 
 lemmas [iff] = not_None_eq
 
-lemma map_fst_eq:
-  "map fst (map (\<lambda>z. (f z, x z)) a) = map fst (map (\<lambda>z. (f z, y z)) a)"
-  by (induct a) auto
-
-lemma succs_stable_eff:
-  "succs_stable (sup_state_opt G) (\<lambda>pc. eff (bs!pc) G pc et)"
-  apply (unfold succs_stable_def eff_def xcpt_eff_def)
-  apply (simp add: map_fst_eq)
-  done
 
 lemma sup_state_opt_unfold:
   "sup_state_opt G \<equiv> Opt.le (Product.le (Listn.le (subtype G)) (Listn.le (Err.le (subtype G))))"
@@ -193,25 +217,32 @@
 lemma app_mono:
   "app_mono (sup_state_opt G) (\<lambda>pc. app (bs!pc) G maxs rT pc et) (length bs) (opt_states G maxs maxr)"
   by (unfold app_mono_def lesub_def) (blast intro: EffectMono.app_mono)
+  
 
-lemma le_list_appendI:
-  "\<And>b c d. a <=[r] b \<Longrightarrow> c <=[r] d \<Longrightarrow> a@c <=[r] b@d"
-apply (induct a)
- apply simp
-apply (case_tac b)
-apply auto
-done
-
-lemma le_listI:
-  "length a = length b \<Longrightarrow> (\<And>n. n < length a \<Longrightarrow> a!n <=_r b!n) \<Longrightarrow> a <=[r] b"
-  apply (unfold lesub_def Listn.le_def)
-  apply (simp add: list_all2_conv_all_nth)
+lemma lesubstep_type_simple:
+  "a <=[Product.le (op =) r] b \<Longrightarrow> a <=|r| b"
+  apply (unfold lesubstep_type_def)
+  apply clarify
+  apply (simp add: set_conv_nth)
+  apply clarify
+  apply (drule le_listD, assumption)
+  apply (clarsimp simp add: lesub_def Product.le_def)
+  apply (rule exI)
+  apply (rule conjI)
+   apply (rule exI)
+   apply (rule conjI)
+    apply (rule sym)
+    apply assumption
+   apply assumption
+  apply assumption
   done
   
+
 lemma eff_mono:
   "\<lbrakk>p < length bs; s <=_(sup_state_opt G) t; app (bs!p) G maxs rT pc et t\<rbrakk>
   \<Longrightarrow> eff (bs!p) G p et s <=|sup_state_opt G| eff (bs!p) G p et t"
   apply (unfold eff_def)
+  apply (rule lesubstep_type_simple)
   apply (rule le_list_appendI)
    apply (simp add: norm_eff_def)
    apply (rule le_listI)
@@ -243,14 +274,14 @@
   by (unfold sup_state_opt_unfold) (blast dest: acyclic_subcls1 order_widen)
 
 theorem exec_mono:
-  "wf_prog wf_mb G \<Longrightarrow>
+  "wf_prog wf_mb G \<Longrightarrow> bounded (exec G maxs rT et bs) (size bs) \<Longrightarrow>
   mono (JVMType.le G maxs maxr) (exec G maxs rT et bs) (size bs) (states G maxs maxr)"  
   apply (unfold exec_def JVM_le_unfold JVM_states_unfold)  
   apply (rule mono_lift)
      apply (fold sup_state_opt_unfold opt_states_def)
      apply (erule order_sup_state_opt)
-    apply (rule succs_stable_eff)
-   apply (rule app_mono)
+    apply (rule app_mono)
+   apply assumption
   apply clarify
   apply (rule eff_mono)
   apply assumption+
@@ -275,7 +306,7 @@
 
 
 theorem is_bcv_kiljvm:
-  "\<lbrakk> wf_prog wf_mb G; bounded (exec G maxs rT et bs) (size bs) \<rbrakk> \<Longrightarrow> 
+  "\<lbrakk> wf_prog wf_mb G; bounded (exec G maxs rT et bs) (size bs) \<rbrakk> \<Longrightarrow>
       is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT et bs)
              (size bs) (states G maxs maxr) (kiljvm G maxs maxr rT et bs)"
   apply (unfold kiljvm_def sl_triple_conv)
@@ -287,8 +318,8 @@
                    dest: wf_subcls1 wf_acyclic) 
      apply (simp add: JVM_le_unfold)
     apply (erule exec_pres_type)
-    apply assumption
-  apply (erule exec_mono)
+   apply assumption
+  apply (erule exec_mono, assumption)  
   done
 
 
@@ -306,19 +337,20 @@
 
   assume "wt_kil G C pTs rT maxs mxl et bs"
   then obtain maxr r where    
-    bounded: "bounded (exec G maxs rT et bs) (size bs)" and
+    bounded: "check_bounded bs et" and
     result:  "r = kiljvm G maxs maxr rT et bs ?start" and
     success: "\<forall>n < size bs. r!n \<noteq> Err" and
     instrs:  "0 < size bs" and
     maxr:    "maxr = Suc (length pTs + mxl)" 
     by (unfold wt_kil_def) simp
 
-  from wf bounded
-  have bcv:
+  from bounded have "bounded (exec G maxs rT et bs) (size bs)"
+    by (unfold exec_def) (intro bounded_lift check_bounded_is_bounded)
+  with wf have bcv:
     "is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT et bs) 
-            (size bs) (states G maxs maxr) (kiljvm G maxs maxr rT et bs)"
+    (size bs) (states G maxs maxr) (kiljvm G maxs maxr rT et bs)"
     by (rule is_bcv_kiljvm)
-
+    
   { fix l x have "set (replicate l x) \<subseteq> {x}" by (cases "0 < l") simp+
   } note subset_replicate = this
   from istype have "set pTs \<subseteq> types G" by auto
@@ -346,9 +378,9 @@
     s: "?start <=[JVMType.le G maxs maxr] phi'" and
     w: "wt_step (JVMType.le G maxs maxr) Err (exec G maxs rT et bs) phi'"
     by blast
-  hence dynamic:
-    "dynamic_wt (sup_state_opt G) (exec G maxs rT et bs) phi'"
-    by (simp add: dynamic_wt_def exec_def JVM_le_Err_conv)
+  hence wt_err_step:
+    "wt_err_step (sup_state_opt G) (exec G maxs rT et bs) phi'"
+    by (simp add: wt_err_step_def exec_def JVM_le_Err_conv)
 
   from s have le: "JVMType.le G maxs maxr (?start ! 0) (phi'!0)"
     by (drule_tac p=0 in le_listD) (simp add: lesub_def)+
@@ -360,14 +392,14 @@
 
   from l bounded 
   have bounded': "bounded (\<lambda>pc. eff (bs!pc) G pc et) (length phi')"
-    by (simp add: exec_def bounded_lift)  
-  with dynamic
-  have "static_wt (sup_state_opt G) (\<lambda>pc. app (bs!pc) G maxs rT pc et) 
-                  (\<lambda>pc. eff (bs!pc) G pc et) (map ok_val phi')"
-    by (auto intro: dynamic_imp_static simp add: exec_def non_empty)
+    by (simp add: exec_def check_bounded_is_bounded)  
+  with wt_err_step
+  have "wt_app_eff (sup_state_opt G) (\<lambda>pc. app (bs!pc) G maxs rT pc et) 
+                   (\<lambda>pc. eff (bs!pc) G pc et) (map ok_val phi')"
+    by (auto intro: wt_err_imp_wt_app_eff simp add: l exec_def non_empty)
   with instrs l le bounded'
   have "wt_method G C pTs rT maxs mxl bs et (map ok_val phi')"
-    apply (unfold wt_method_def static_wt_def)
+    apply (unfold wt_method_def wt_app_eff_def)
     apply simp
     apply (rule conjI)
      apply (unfold wt_start_def)
@@ -387,7 +419,8 @@
 
 theorem wt_kil_complete:
   "\<lbrakk> wt_method G C pTs rT maxs mxl bs et phi; wf_prog wf_mb G; 
-      length phi = length bs; is_class G C; \<forall>x \<in> set pTs. is_type G x;
+     check_bounded bs et; length phi = length bs; is_class G C; 
+      \<forall>x \<in> set pTs. is_type G x;
       map OK phi \<in> list (length bs) (states G maxs (1+size pTs+mxl)) \<rbrakk>
   \<Longrightarrow> wt_kil G C pTs rT maxs mxl et bs"
 proof -
@@ -396,6 +429,7 @@
   assume istype: "\<forall>x \<in> set pTs. is_type G x"
   assume length: "length phi = length bs"
   assume istype_phi: "map OK phi \<in> list (length bs) (states G maxs (1+size pTs+mxl))"
+  assume bounded: "check_bounded bs et"
 
   assume "wt_method G C pTs rT maxs mxl bs et phi"
   then obtain
@@ -408,37 +442,22 @@
   let ?eff  = "\<lambda>pc. eff (bs!pc) G pc et"
   let ?app   = "\<lambda>pc. app (bs!pc) G maxs rT pc et"
 
-  have bounded_eff: "bounded ?eff (size bs)"
-  proof (unfold bounded_def, clarify)
-    fix pc pc' s s' assume "pc < length bs"
-    with wt_ins have "wt_instr (bs!pc) G rT phi maxs (length bs) et pc" by fast
-    then obtain "\<forall>(pc',s') \<in> set (?eff pc (phi!pc)). pc' < length bs"
-      by (unfold wt_instr_def) fast
-    hence "\<forall>pc' \<in> set (map fst (?eff pc (phi!pc))). pc' < length bs" by auto
-    also 
-    note succs_stable_eff 
-    hence "map fst (?eff pc (phi!pc)) = map fst (?eff pc s)" 
-      by (rule succs_stableD)
-    finally have "\<forall>(pc',s') \<in> set (?eff pc s). pc' < length bs" by auto
-    moreover assume "(pc',s') \<in> set (?eff pc s)"
-    ultimately show "pc' < length bs" by blast
-  qed
-  hence bounded_exec: "bounded (exec G maxs rT et bs) (size bs)" 
-    by (simp add: exec_def bounded_lift)
+  from bounded
+  have bounded_exec: "bounded (exec G maxs rT et bs) (size bs)"
+    by (unfold exec_def) (intro bounded_lift check_bounded_is_bounded)
  
   from wt_ins
-  have "static_wt (sup_state_opt G) ?app ?eff phi"
-    apply (unfold static_wt_def wt_instr_def lesub_def)
+  have "wt_app_eff (sup_state_opt G) ?app ?eff phi"
+    apply (unfold wt_app_eff_def wt_instr_def lesub_def)
     apply (simp (no_asm) only: length)
     apply blast
     done
-
-  with bounded_eff
-  have "dynamic_wt (sup_state_opt G) (err_step ?app ?eff) (map OK phi)"
-    by - (erule static_imp_dynamic, simp add: length)
-  hence dynamic:
-    "dynamic_wt (sup_state_opt G) (exec G maxs rT et bs) (map OK phi)"
-    by (unfold exec_def)
+  with bounded_exec
+  have "wt_err_step (sup_state_opt G) (err_step (size phi) ?app ?eff) (map OK phi)"
+    by - (erule wt_app_eff_imp_wt_err,simp add: exec_def length)
+  hence wt_err:
+    "wt_err_step (sup_state_opt G) (exec G maxs rT et bs) (map OK phi)"
+    by (unfold exec_def) (simp add: length)
  
   let ?maxr = "1+size pTs+mxl"
   from wf bounded_exec
@@ -501,13 +520,13 @@
     ultimately show ?thesis by (rule le_listI)
   qed         
 
-  from dynamic
+  from wt_err
   have "wt_step (JVMType.le G maxs ?maxr) Err (exec G maxs rT et bs) ?phi"
-    by (simp add: dynamic_wt_def JVM_le_Err_conv)  
+    by (simp add: wt_err_step_def JVM_le_Err_conv)  
   with start istype_phi less_phi is_bcv
   have "\<forall>p. p < length bs \<longrightarrow> kiljvm G maxs ?maxr rT et bs ?start ! p \<noteq> Err"
     by (unfold is_bcv_def) auto
-  with bounded_exec instrs
+  with bounded instrs
   show "wt_kil G C pTs rT maxs mxl et bs" by (unfold wt_kil_def) simp
 qed
 text {*
@@ -593,4 +612,5 @@
   thus ?thesis by blast
 qed
 
+
 end
diff -r d6585b32412b -r b57d926d1de2 src/HOL/MicroJava/BV/Kildall.thy
--- a/src/HOL/MicroJava/BV/Kildall.thy	Sun Mar 24 14:05:53 2002 +0100
+++ b/src/HOL/MicroJava/BV/Kildall.thy	Sun Mar 24 14:06:21 2002 +0100
@@ -299,8 +299,8 @@
 lemma merges_bounded_lemma:
   "\<lbrakk> semilat (A,r,f); mono r step n A; bounded step n; 
      \<forall>(p',s') \<in> set (step p (ss!p)). s' \<in> A; ss \<in> list n A; ts \<in> list n A; p < n; 
-     ss <=[r] ts; ! p. p < n \<longrightarrow> stable r step ts p \<rbrakk> 
-  \<Longrightarrow> merges f (step p (ss!p)) ss <=[r] ts"
+     ss <=[r] ts; \<forall>p. p < n \<longrightarrow> stable r step ts p \<rbrakk> 
+  \<Longrightarrow> merges f (step p (ss!p)) ss <=[r] ts" 
   apply (unfold stable_def)
   apply (rule merges_pres_le_ub)
       apply assumption
@@ -319,7 +319,7 @@
     apply simp
    apply (simp add: le_listD)
   
-  apply (drule lesub_step_type, assumption) 
+  apply (drule lesub_step_typeD, assumption) 
   apply clarify
   apply (drule bspec, assumption)
   apply simp
diff -r d6585b32412b -r b57d926d1de2 src/HOL/MicroJava/BV/Kildall_Lift.thy
--- a/src/HOL/MicroJava/BV/Kildall_Lift.thy	Sun Mar 24 14:05:53 2002 +0100
+++ b/src/HOL/MicroJava/BV/Kildall_Lift.thy	Sun Mar 24 14:06:21 2002 +0100
@@ -11,84 +11,32 @@
 "app_mono r app n A ==
  \<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> app p t \<longrightarrow> app p s"
 
- succs_stable :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> bool"
-"succs_stable r step == \<forall>p t t'. map fst (step p t') = map fst (step p t)"
 
-lemma succs_stableD:
-  "succs_stable r step \<Longrightarrow> map fst (step p t) = map fst (step p t')"
-  by (unfold succs_stable_def) blast
-
-lemma eqsub_def [simp]: "a <=_(op =) b = (a = b)" by (simp add: lesub_def)
-
-lemma list_le_eq [simp]: "\<And>b. a <=[op =] b = (a = b)"
-apply (induct a) 
- apply simp
- apply rule
-  apply simp
- apply simp
-apply (case_tac b)
- apply simp
-apply simp
-done
-
-lemma map_err: "map_err a = zip (map fst a) (map (\<lambda>x. Err) (map snd a))"
-apply (induct a)
-apply (auto simp add: map_err_def map_snd_def)
-done
-
-lemma map_snd: "map_snd f a = zip (map fst a) (map f (map snd a))"
-apply (induct a)
-apply (auto simp add: map_snd_def)
-done
+lemma in_map_sndD: "(a,b) \<in> set (map_snd f xs) \<Longrightarrow> \<exists>b'. (a,b') \<in> set xs"
+  apply (induct xs)
+  apply (auto simp add: map_snd_def)
+  done
 
-lemma zipI: 
-  "\<And>b c d. a <=[r1] c \<Longrightarrow> b <=[r2] d \<Longrightarrow> zip a b <=[Product.le r1 r2] zip c d"
-apply (induct a)
- apply simp
-apply (case_tac c)
- apply simp
-apply (case_tac b)
- apply simp
-apply (case_tac d)
- apply simp
-apply simp
-done
-
-lemma step_type_ord: 
-  "\<And>b. a <=|r| b \<Longrightarrow> map snd a <=[r] map snd b \<and> map fst a = map fst b"
-apply (induct a)
- apply simp
-apply (case_tac b)
- apply simp
-apply simp
-apply (auto simp add: Product.le_def lesub_def)
-done
+lemma bounded_lift:
+  "bounded step n \<Longrightarrow> bounded (err_step n app step) n"
+  apply (unfold bounded_def err_step_def error_def)
+  apply clarify
+  apply (erule allE, erule impE, assumption)
+  apply (case_tac s)
+  apply (auto simp add: map_snd_def split: split_if_asm)
+  done
 
-lemma map_OK_Err: 
-  "\<And>y. length y = length x \<Longrightarrow> map OK x <=[Err.le r] map (\<lambda>x. Err) y"
-apply (induct x)
- apply simp
-apply simp
-apply (case_tac y)
-apply auto
-done
-
-lemma map_Err_Err:
-  "\<And>b. length a = length b \<Longrightarrow> map (\<lambda>x. Err) a <=[Err.le r] map (\<lambda>x. Err) b"
-apply (induct a)
- apply simp
-apply (case_tac b)
-apply auto
-done
-
-lemma succs_stable_length: 
-  "succs_stable r step \<Longrightarrow> length (step p t) = length (step p t')"
-proof -
-  assume "succs_stable r step"  
-  hence "map fst (step p t) = map fst (step p t')" by (rule succs_stableD)
-  hence "length (map fst (step p t)) = length (map fst (step p t'))" by simp
-  thus ?thesis by simp
-qed
+lemma boundedD2:
+  "bounded (err_step n app step) n \<Longrightarrow> 
+  p < n \<Longrightarrow>  app p a \<Longrightarrow> (q,b) \<in> set (step p a) \<Longrightarrow> 
+  q < n"
+  apply (simp add: bounded_def err_step_def)
+  apply (erule allE, erule impE, assumption)
+  apply (erule_tac x = "OK a" in allE, drule bspec)
+   apply (simp add: map_snd_def)
+   apply fast
+  apply simp
+  done
 
 lemma le_list_map_OK [simp]:
   "\<And>b. map OK a <=[Err.le r] map OK b = (a <=[r] b)"
@@ -100,126 +48,76 @@
   apply simp
   done
 
+
+lemma map_snd_lessI:
+  "x <=|r| y \<Longrightarrow> map_snd OK x <=|Err.le r| map_snd OK y"
+  apply (induct x)
+  apply (unfold lesubstep_type_def map_snd_def)
+  apply auto
+  done
+
+
 lemma mono_lift:
-  "order r \<Longrightarrow> succs_stable r step \<Longrightarrow> app_mono r app n A \<Longrightarrow> 
+  "order r \<Longrightarrow> app_mono r app n A \<Longrightarrow> bounded (err_step n app step) n \<Longrightarrow>
   \<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> app p t \<longrightarrow> step p s <=|r| step p t \<Longrightarrow>
-  mono (Err.le r) (err_step app step) n (err A)"
+  mono (Err.le r) (err_step n app step) n (err A)"
 apply (unfold app_mono_def mono_def err_step_def)
 apply clarify
 apply (case_tac s)
- apply simp
- apply (rule le_list_refl)
- apply simp
+ apply simp 
 apply simp
-apply (subgoal_tac "map fst (step p arbitrary) = map fst (step p a)")
- prefer 2
- apply (erule succs_stableD)
 apply (case_tac t)
  apply simp
- apply (rule conjI)
-  apply clarify
-  apply (simp add: map_err map_snd)
-  apply (rule zipI)
-   apply simp
-  apply (rule map_OK_Err)
-  apply (subgoal_tac "length (step p arbitrary) = length (step p a)")
-   prefer 2
-   apply (erule succs_stable_length)
-  apply simp
  apply clarify
- apply (simp add: map_err)
- apply (rule zipI)
-  apply simp
- apply (rule map_Err_Err)
- apply simp
- apply (erule succs_stable_length)
-apply simp
-apply (elim allE)
-apply (erule impE, blast)+
-apply (rule conjI)
+ apply (simp add: lesubstep_type_def error_def)
+ apply clarify
+ apply (drule in_map_sndD)
  apply clarify
- apply (simp add: map_snd)
- apply (rule zipI)
-  apply simp
-  apply (erule succs_stableD)
- apply (simp add: step_type_ord)
-apply clarify
+ apply (drule boundedD2, assumption+)
+ apply (rule exI [of _ Err])
+ apply simp
+apply simp
+apply (erule allE, erule allE, erule allE, erule impE)
+ apply (rule conjI, assumption)
+ apply (rule conjI, assumption)
+ apply assumption
 apply (rule conjI)
- apply clarify
- apply (simp add: map_snd map_err)
- apply (rule zipI)
-  apply simp
-  apply (erule succs_stableD)
- apply (rule map_OK_Err)
- apply (simp add: succs_stable_length)
+apply clarify
+apply (erule allE, erule allE, erule allE, erule impE)
+ apply (rule conjI, assumption)
+ apply (rule conjI, assumption)
+ apply assumption
+apply (erule impE, assumption)
+apply (rule map_snd_lessI, assumption)
 apply clarify
-apply (simp add: map_err)
-apply (rule zipI)
- apply simp
- apply (erule succs_stableD)
-apply (rule map_Err_Err)
-apply (simp add: succs_stable_length)
+apply (simp add: lesubstep_type_def error_def)
+apply clarify
+apply (drule in_map_sndD)
+apply clarify
+apply (drule boundedD2, assumption+)
+apply (rule exI [of _ Err])
+apply simp
 done
  
-lemma in_map_sndD: "(a,b) \<in> set (map_snd f xs) \<Longrightarrow> \<exists>b'. (a,b') \<in> set xs"
-apply (induct xs)
-apply (auto simp add: map_snd_def)
-done
-
-lemma bounded_lift:
-  "bounded (err_step app step) n = bounded step n"
-apply (unfold bounded_def err_step_def)
-apply rule
-apply clarify
- apply (erule allE, erule impE, assumption)
- apply (erule_tac x = "OK s" in allE)
- apply simp
- apply (case_tac "app p s")
-  apply (simp add: map_snd_def)
-  apply (drule bspec, assumption)
-  apply simp
- apply (simp add: map_err_def map_snd_def)
- apply (drule bspec, assumption)
- apply simp
-apply clarify
-apply (case_tac s)
- apply simp
- apply (simp add: map_err_def)
- apply (blast dest: in_map_sndD)
-apply (simp split: split_if_asm)
- apply (blast dest: in_map_sndD)
-apply (simp add: map_err_def)
-apply (blast dest: in_map_sndD)
-done
-
-lemma set_zipD: "\<And>y. (a,b) \<in> set (zip x y) \<Longrightarrow> (a \<in> set x \<and> b \<in> set y)"
-apply (induct x)
- apply simp
-apply (case_tac y)
- apply simp
-apply simp
-apply blast
-done
+lemma in_errorD:
+  "(x,y) \<in> set (error n) \<Longrightarrow> y = Err"
+  by (auto simp add: error_def)
 
 lemma pres_type_lift:
   "\<forall>s\<in>A. \<forall>p. p < n \<longrightarrow> app p s \<longrightarrow> (\<forall>(q, s')\<in>set (step p s). s' \<in> A) 
-  \<Longrightarrow> pres_type (err_step app step) n (err A)"  
+  \<Longrightarrow> pres_type (err_step n app step) n (err A)"  
 apply (unfold pres_type_def err_step_def)
 apply clarify
 apply (case_tac b)
  apply simp
 apply (case_tac s)
- apply (simp add: map_err)
- apply (drule set_zipD)
- apply clarify
+ apply simp
+ apply (drule in_errorD)
  apply simp
- apply blast
-apply (simp add: map_err split: split_if_asm)
- apply (simp add: map_snd_def)
- apply fastsimp
-apply (drule set_zipD)
+apply (simp add: map_snd_def split: split_if_asm)
+ apply fast
+apply (drule in_errorD)
 apply simp
-apply blast
 done
 
 end
diff -r d6585b32412b -r b57d926d1de2 src/HOL/MicroJava/BV/LBVComplete.thy
--- a/src/HOL/MicroJava/BV/LBVComplete.thy	Sun Mar 24 14:05:53 2002 +0100
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Sun Mar 24 14:06:21 2002 +0100
@@ -9,60 +9,60 @@
 theory LBVComplete = LBVSpec + Typing_Framework:
 
 constdefs
-  contains_targets :: "['s steptype, 's certificate, 's option list, nat, nat] \<Rightarrow> bool"
-  "contains_targets step cert phi pc n \<equiv>
-  \<forall>(pc',s') \<in> set (step pc (OK (phi!pc))). pc' \<noteq> pc+1 \<and> pc' < n \<longrightarrow> cert!pc' = phi!pc'"
+  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'"
 
-  fits :: "['s steptype, 's certificate, 's option list, nat] \<Rightarrow> bool"
-  "fits step cert phi n \<equiv> \<forall>pc. pc < n \<longrightarrow> 
-                               contains_targets step cert phi pc n \<and>
-                               (cert!pc = None \<or> cert!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)"
 
-  is_target :: "['s steptype, 's option list, nat, nat] \<Rightarrow> bool" 
-  "is_target step phi pc' n \<equiv>
-     \<exists>pc s'. pc' \<noteq> pc+1 \<and> pc < n \<and> (pc',s') \<in> set (step pc (OK (phi!pc)))"
+  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)))"
 
-  make_cert :: "['s steptype, 's option list, nat] \<Rightarrow> 's certificate"
-  "make_cert step phi n \<equiv> 
-     map (\<lambda>pc. if is_target step phi pc n then phi!pc else None) [0..n(]"
+  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(]"
 
   
 lemmas [simp del] = split_paired_Ex
 
 lemma make_cert_target:
-  "\<lbrakk> pc < n; is_target step phi pc n \<rbrakk> \<Longrightarrow> make_cert step phi n ! pc = phi!pc"
+  "\<lbrakk> pc < length phi; is_target step phi pc \<rbrakk> \<Longrightarrow> make_cert step phi ! pc = phi!pc"
   by (simp add: make_cert_def)
 
 lemma make_cert_approx:
-  "\<lbrakk> pc < n; make_cert step phi n ! pc \<noteq> phi!pc \<rbrakk> \<Longrightarrow> 
-   make_cert step phi n ! pc = None"
+  "\<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)
 
 lemma make_cert_contains_targets:
-  "pc < n \<Longrightarrow> contains_targets step (make_cert step phi n) phi pc n"
+  "pc < length phi \<Longrightarrow> contains_targets step (make_cert step phi) phi pc"
 proof (unfold contains_targets_def, clarify)
   fix pc' s'
-  assume "pc < n"
+  assume "pc < length phi"
          "(pc',s') \<in> set (step pc (OK (phi ! pc)))"
          "pc' \<noteq> pc+1" and
-    pc': "pc' < n"
-  hence "is_target step phi pc' n"  by (auto simp add: is_target_def)
-  with pc' show "make_cert step phi n ! pc' = phi ! pc'" 
+    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
 
 theorem fits_make_cert:
-  "fits step (make_cert step phi n) phi n"
+  "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 n; (pc',s') \<in> set (step pc (OK (phi ! pc)));
-      pc' \<noteq> Suc pc; pc < n; pc' < n \<rbrakk>
+  "\<lbrakk> fits step cert phi; (pc',s') \<in> set (step pc (OK (phi ! pc)));
+      pc' \<noteq> Suc pc; 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 n; pc < n; cert!pc = Some s \<rbrakk>
+   "\<lbrakk> fits step cert phi; pc < length phi; cert!pc = Some s \<rbrakk>
   \<Longrightarrow> cert!pc = phi!pc"
   by (auto simp add: fits_def)
 
@@ -82,8 +82,9 @@
   
 lemma stable_wtl:
   assumes stable: "stable (Err.le (Opt.le r)) step (map OK phi) pc"
-  assumes fits:   "fits step cert phi n"
+  assumes fits:   "fits step cert phi"  
   assumes pc:     "pc < length phi"
+  assumes bounded:"bounded step (length phi)"
   shows "wtl_inst cert f r step pc (phi!pc) \<noteq> Err"
 proof -
   from pc have [simp]: "map OK phi ! pc = OK (phi!pc)" by simp
@@ -91,7 +92,10 @@
   have "\<forall>(q,s')\<in>set (step pc (OK (phi!pc))). s' \<le>|r (map OK phi!q)"
     by (simp add: stable_def)
   
-
+  have "merge cert f r pc (step pc (OK (phi ! pc))) (OK (cert ! Suc pc)) \<noteq> Err"
+    sorry
+  thus ?thesis by (simp add: wtl_inst_def)  
+qed
 
 
 lemma wtl_inst_mono:
diff -r d6585b32412b -r b57d926d1de2 src/HOL/MicroJava/BV/Listn.thy
--- a/src/HOL/MicroJava/BV/Listn.thy	Sun Mar 24 14:05:53 2002 +0100
+++ b/src/HOL/MicroJava/BV/Listn.thy	Sun Mar 24 14:06:21 2002 +0100
@@ -142,6 +142,20 @@
 apply auto
 done  
 
+lemma le_list_appendI:
+  "\<And>b c d. a <=[r] b \<Longrightarrow> c <=[r] d \<Longrightarrow> a@c <=[r] b@d"
+apply (induct a)
+ apply simp
+apply (case_tac b)
+apply auto
+done
+
+lemma le_listI:
+  "length a = length b \<Longrightarrow> (\<And>n. n < length a \<Longrightarrow> a!n <=_r b!n) \<Longrightarrow> a <=[r] b"
+  apply (unfold lesub_def Listn.le_def)
+  apply (simp add: list_all2_conv_all_nth)
+  done
+
 lemma listI:
   "\<lbrakk> length xs = n; set xs <= A \<rbrakk> \<Longrightarrow> xs : list n A"
 apply (unfold list_def)
@@ -202,6 +216,37 @@
   "\<lbrakk> xs : list n A; i < n \<rbrakk> \<Longrightarrow> (xs!i) : A"
   by auto
 
+
+lemma listn_Cons_Suc [elim!]:
+  "l#xs \<in> list n A \<Longrightarrow> (\<And>n'. n = Suc n' \<Longrightarrow> l \<in> A \<Longrightarrow> xs \<in> list n' A \<Longrightarrow> P) \<Longrightarrow> P"
+  by (cases n) auto
+
+lemma listn_appendE [elim!]:
+  "a@b \<in> list n A \<Longrightarrow> (\<And>n1 n2. n=n1+n2 \<Longrightarrow> a \<in> list n1 A \<Longrightarrow> b \<in> list n2 A \<Longrightarrow> P) \<Longrightarrow> P" 
+proof -
+  have "\<And>n. a@b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n=n1+n2 \<and> a \<in> list n1 A \<and> b \<in> list n2 A"
+    (is "\<And>n. ?list a n \<Longrightarrow> \<exists>n1 n2. ?P a n n1 n2")
+  proof (induct a)
+    fix n assume "?list [] n"
+    hence "?P [] n 0 n" by simp
+    thus "\<exists>n1 n2. ?P [] n n1 n2" by fast
+  next
+    fix n l ls
+    assume "?list (l#ls) n"
+    then obtain n' where n: "n = Suc n'" "l \<in> A" and "ls@b \<in> list n' A" by fastsimp
+    assume "\<And>n. ls @ b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> ls \<in> list n1 A \<and> b \<in> list n2 A"
+    hence "\<exists>n1 n2. n' = n1 + n2 \<and> ls \<in> list n1 A \<and> b \<in> list n2 A" .
+    then obtain n1 n2 where "n' = n1 + n2" "ls \<in> list n1 A" "b \<in> list n2 A" by fast
+    with n have "?P (l#ls) n (n1+1) n2" by simp
+    thus "\<exists>n1 n2. ?P (l#ls) n n1 n2" by fastsimp
+  qed
+  moreover
+  assume "a@b \<in> list n A" "\<And>n1 n2. n=n1+n2 \<Longrightarrow> a \<in> list n1 A \<Longrightarrow> b \<in> list n2 A \<Longrightarrow> P"
+  ultimately
+  show ?thesis by blast
+qed
+
+
 lemma listt_update_in_list [simp, intro!]:
   "\<lbrakk> xs : list n A; x:A \<rbrakk> \<Longrightarrow> xs[i := x] : list n A"
 apply (unfold list_def)
diff -r d6585b32412b -r b57d926d1de2 src/HOL/MicroJava/BV/SemilatAlg.thy
--- a/src/HOL/MicroJava/BV/SemilatAlg.thy	Sun Mar 24 14:05:53 2002 +0100
+++ b/src/HOL/MicroJava/BV/SemilatAlg.thy	Sun Mar 24 14:06:21 2002 +0100
@@ -9,18 +9,17 @@
 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"
- 
+constdefs 
+  lesubstep_type :: "(nat \<times> 's) list \<Rightarrow> 's ord \<Rightarrow> (nat \<times> 's) list \<Rightarrow> bool"
+                    ("(_ /<=|_| _)" [50, 0, 51] 50)
+  "x <=|r| y \<equiv> \<forall>(p,s) \<in> set x. \<exists>s'. (p,s') \<in> set y \<and> s <=_r s'"
+
 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"  
@@ -45,6 +44,14 @@
   "\<lbrakk> bounded step n; p < n; (q,t) : set (step p xs) \<rbrakk> \<Longrightarrow> q < n" 
   by (unfold bounded_def, blast)
 
+lemma lesubstep_type_refl [simp, intro]:
+  "(\<And>x. x <=_r x) \<Longrightarrow> x <=|r| x"
+  by (unfold lesubstep_type_def) auto
+
+lemma lesub_step_typeD:
+  "a <=|r| b \<Longrightarrow> (x,y) \<in> set a \<Longrightarrow> \<exists>y'. (x, y') \<in> set b \<and> y <=_r y'"
+  by (unfold lesubstep_type_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>  
@@ -162,20 +169,4 @@
 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 d6585b32412b -r b57d926d1de2 src/HOL/MicroJava/BV/Typing_Framework_err.thy
--- a/src/HOL/MicroJava/BV/Typing_Framework_err.thy	Sun Mar 24 14:05:53 2002 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework_err.thy	Sun Mar 24 14:06:21 2002 +0100
@@ -11,28 +11,30 @@
 
 constdefs
 
-dynamic_wt :: "'s ord \<Rightarrow> 's err step_type \<Rightarrow> 's err list \<Rightarrow> bool"
-"dynamic_wt r step ts == wt_step (Err.le r) Err step ts"
+wt_err_step :: "'s ord \<Rightarrow> 's err step_type \<Rightarrow> 's err list \<Rightarrow> bool"
+"wt_err_step r step ts \<equiv> wt_step (Err.le r) Err step ts"
 
-static_wt :: "'s ord \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool"
-"static_wt r app step ts == 
+wt_app_eff :: "'s ord \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool"
+"wt_app_eff r app step ts \<equiv>
   \<forall>p < size ts. app p (ts!p) \<and> (\<forall>(q,t) \<in> set (step p (ts!p)). t <=_r ts!q)"
 
 map_snd :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'c) list"
-"map_snd f == map (\<lambda>(x,y). (x, f y))"
+"map_snd f \<equiv> map (\<lambda>(x,y). (x, f y))"
+
+error :: "nat \<Rightarrow> (nat \<times> 'a err) list"
+"error n \<equiv> map (\<lambda>x. (x,Err)) [0..n(]"
 
-map_err :: "('a \<times> 'b) list \<Rightarrow> ('a \<times> 'b err) list"
-"map_err == map_snd (\<lambda>y. Err)"
-
-err_step :: "(nat \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's step_type \<Rightarrow> 's err step_type"
-"err_step app step p t == case t of Err \<Rightarrow> map_err (step p arbitrary) | OK t' \<Rightarrow> 
-  if app p t' then map_snd OK (step p t') else map_err (step p t')"
+err_step :: "nat \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's step_type \<Rightarrow> 's err step_type"
+"err_step n app step p t \<equiv> 
+  case t of 
+    Err   \<Rightarrow> error n
+  | OK t' \<Rightarrow> if app p t' then map_snd OK (step p t') else error n"
 
 non_empty :: "'s step_type \<Rightarrow> bool"
-"non_empty step == \<forall>p t. step p t \<noteq> []"
+"non_empty step \<equiv> \<forall>p t. step p t \<noteq> []"
 
 
-lemmas err_step_defs = err_step_def map_snd_def map_err_def
+lemmas err_step_defs = err_step_def map_snd_def error_def
 
 lemma non_emptyD:
   "non_empty step \<Longrightarrow> \<exists>q t'. (q,t') \<in> set(step p t)"
@@ -46,44 +48,38 @@
 qed
 
 
-lemma dynamic_imp_static:
-  "\<lbrakk> bounded step (size ts); non_empty step;
-      dynamic_wt r (err_step app step) ts \<rbrakk> 
-  \<Longrightarrow> static_wt r app step (map ok_val ts)"
-proof (unfold static_wt_def, intro strip, rule conjI)
-
-  assume b:  "bounded step (size ts)"
-  assume n:  "non_empty step"
-  assume wt: "dynamic_wt r (err_step app step) ts"
-
-  fix p 
-  assume "p < length (map ok_val ts)"
-  hence lp: "p < length ts" by simp
+lemma wt_err_imp_wt_app_eff:
+  assumes b:  "bounded step (size ts)"
+  assumes n:  "non_empty step"
+  assumes wt: "wt_err_step r (err_step (size ts) app step) ts"
+  shows "wt_app_eff r app step (map ok_val ts)"
+proof (unfold wt_app_eff_def, intro strip, rule conjI)
+  fix p assume "p < size (map ok_val ts)"
+  hence lp: "p < size ts" by simp
 
   from wt lp
-  have [intro?]: "\<And>p. p < length ts \<Longrightarrow> ts ! p \<noteq> Err" 
-    by (unfold dynamic_wt_def wt_step_def) simp
+  have [intro?]: "\<And>p. p < size ts \<Longrightarrow> ts ! p \<noteq> Err" 
+    by (unfold wt_err_step_def wt_step_def) simp
 
   show app: "app p (map ok_val ts ! p)"
   proof -
     from wt lp 
     obtain s where
       OKp:  "ts ! p = OK s" and
-      less: "\<forall>(q,t) \<in> set (err_step app step p (ts!p)). t <=_(Err.le r) ts!q"
-      by (unfold dynamic_wt_def wt_step_def stable_def) 
+      less: "\<forall>(q,t) \<in> set (err_step (size ts) app step p (ts!p)). t <=_(Err.le r) ts!q"
+      by (unfold wt_err_step_def wt_step_def stable_def) 
          (auto iff: not_Err_eq)
     
-    from n
-    obtain q t where q: "(q,t) \<in> set(step p s)"
-      by (blast dest: non_emptyD)
-
+    from n obtain q t where q: "(q,t) \<in> set(step p s)"
+      by (blast dest: non_emptyD) 
+    
     from lp b q
-    have lq: "q < length ts" by (unfold bounded_def) blast
+    have lq: "q < size ts" by (unfold bounded_def) blast
     hence "ts!q \<noteq> Err" ..
     then obtain s' where OKq: "ts ! q = OK s'" by (auto iff: not_Err_eq)      
 
-    with OKp less q have "app p s"
-      by (auto simp add: err_step_defs split: err.split_asm split_if_asm)
+    with OKp less q lp have "app p s"
+      by (auto simp add: err_step_defs split: err.split_asm split_if_asm)      
 
     with lp OKp show ?thesis by simp
   qed
@@ -95,12 +91,12 @@
     from wt lp q
     obtain s where
       OKp:  "ts ! p = OK s" and
-      less: "\<forall>(q,t) \<in> set (err_step app step p (ts!p)). t <=_(Err.le r) ts!q"
-      by (unfold dynamic_wt_def wt_step_def stable_def) 
+      less: "\<forall>(q,t) \<in> set (err_step (size ts) app step p (ts!p)). t <=_(Err.le r) ts!q"
+      by (unfold wt_err_step_def wt_step_def stable_def) 
          (auto iff: not_Err_eq)
 
     from lp b q
-    have lq: "q < length ts" by (unfold bounded_def) blast
+    have lq: "q < size ts" by (unfold bounded_def) blast
     hence "ts!q \<noteq> Err" ..
     then obtain s' where OKq: "ts ! q = OK s'" by (auto iff: not_Err_eq)
 
@@ -111,24 +107,22 @@
 qed
 
 
-lemma static_imp_dynamic:
-  "\<lbrakk> static_wt r app step ts; bounded step (size ts) \<rbrakk> 
-  \<Longrightarrow> dynamic_wt r (err_step app step) (map OK ts)"
-proof (unfold dynamic_wt_def wt_step_def, intro strip, rule conjI)
-  assume bounded: "bounded step (size ts)"
-  assume static:  "static_wt r app step ts"
-  fix p assume "p < length (map OK ts)" 
-  hence p: "p < length ts" by simp
+lemma wt_app_eff_imp_wt_err:
+  assumes app_eff: "wt_app_eff r app step ts"
+  assumes bounded: "bounded (err_step (size ts) app step) (size ts)"
+  shows "wt_err_step r (err_step (size ts) app step) (map OK ts)"
+proof (unfold wt_err_step_def wt_step_def, intro strip, rule conjI)
+  fix p assume "p < size (map OK ts)" 
+  hence p: "p < size ts" by simp
   thus "map OK ts ! p \<noteq> Err" by simp
   { fix q t
-    assume q: "(q,t) \<in> set (err_step app step p (map OK ts ! p))" 
-    with p static obtain 
+    assume q: "(q,t) \<in> set (err_step (size ts) app step p (map OK ts ! p))" 
+    with p app_eff obtain 
       "app p (ts ! p)" "\<forall>(q,t) \<in> set (step p (ts!p)). t <=_r ts!q"
-      by (unfold static_wt_def) blast
+      by (unfold wt_app_eff_def) blast
     moreover
-    from q p bounded have "q < size ts" 
-      by (clarsimp simp add: bounded_def err_step_defs 
-          split: err.splits split_if_asm) blast+
+    from q p bounded have "q < size ts"
+      by - (rule boundedD)
     hence "map OK ts ! q = OK (ts!q)" by simp
     moreover
     have "p < size ts" by (rule p)
@@ -137,7 +131,7 @@
     have "t <=_(Err.le r) map OK ts ! q" 
       by (auto simp add: err_step_def map_snd_def)
   }
-  thus "stable (Err.le r) (err_step app step) (map OK ts) p"
+  thus "stable (Err.le r) (err_step (size ts) app step) (map OK ts) p"
     by (unfold stable_def) blast
 qed