cleanup + simpler monotonicity
authorkleing
Sun Mar 24 14:06:21 2002 +0100 (2002-03-24)
changeset 13066b57d926d1de2
parent 13065 d6585b32412b
child 13067 a59af3a83c61
cleanup + simpler monotonicity
src/HOL/MicroJava/BV/Effect.thy
src/HOL/MicroJava/BV/JVM.thy
src/HOL/MicroJava/BV/Kildall.thy
src/HOL/MicroJava/BV/Kildall_Lift.thy
src/HOL/MicroJava/BV/LBVComplete.thy
src/HOL/MicroJava/BV/Listn.thy
src/HOL/MicroJava/BV/SemilatAlg.thy
src/HOL/MicroJava/BV/Typing_Framework_err.thy
     1.1 --- a/src/HOL/MicroJava/BV/Effect.thy	Sun Mar 24 14:05:53 2002 +0100
     1.2 +++ b/src/HOL/MicroJava/BV/Effect.thy	Sun Mar 24 14:06:21 2002 +0100
     1.3 @@ -184,6 +184,32 @@
     1.4    "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"
     1.5  
     1.6  
     1.7 +lemma match_any_match_table:
     1.8 +  "C \<in> set (match_any G pc et) \<Longrightarrow> match_exception_table G C pc et \<noteq> None"
     1.9 +  apply (induct et)
    1.10 +   apply simp
    1.11 +  apply simp
    1.12 +  apply clarify
    1.13 +  apply (simp split: split_if_asm)
    1.14 +  apply (auto simp add: match_exception_entry_def)
    1.15 +  done
    1.16 +
    1.17 +lemma match_X_match_table:
    1.18 +  "C \<in> set (match G X pc et) \<Longrightarrow> match_exception_table G C pc et \<noteq> None"
    1.19 +  apply (induct et)
    1.20 +   apply simp
    1.21 +  apply (simp split: split_if_asm)
    1.22 +  done
    1.23 +
    1.24 +lemma xcpt_names_in_et:
    1.25 +  "C \<in> set (xcpt_names (i,G,pc,et)) \<Longrightarrow> 
    1.26 +  \<exists>e \<in> set et. the (match_exception_table G C pc et) = fst (snd (snd e))"
    1.27 +  apply (cases i)
    1.28 +  apply (auto dest!: match_any_match_table match_X_match_table 
    1.29 +              dest: match_exception_table_in_et)
    1.30 +  done
    1.31 +
    1.32 +
    1.33  lemma 1: "2 < length a \<Longrightarrow> (\<exists>l l' l'' ls. a = l#l'#l''#ls)"
    1.34  proof (cases a)
    1.35    fix x xs assume "a = x#xs" "2 < length a"
     2.1 --- a/src/HOL/MicroJava/BV/JVM.thy	Sun Mar 24 14:05:53 2002 +0100
     2.2 +++ b/src/HOL/MicroJava/BV/JVM.thy	Sun Mar 24 14:06:21 2002 +0100
     2.3 @@ -6,13 +6,17 @@
     2.4  
     2.5  header {* \isaheader{Kildall for the JVM}\label{sec:JVM} *}
     2.6  
     2.7 -theory JVM = Kildall_Lift + JVMType + Opt + Product + Typing_Framework_err +
     2.8 -             EffectMono + BVSpec:
     2.9 +theory JVM = Kildall_Lift + JVMType + EffectMono + BVSpec:
    2.10 +
    2.11  
    2.12  constdefs
    2.13 +  check_bounded :: "instr list \<Rightarrow> exception_table \<Rightarrow> bool"
    2.14 +  "check_bounded ins et \<equiv> (\<forall>pc < length ins. \<forall>pc' \<in> set (succs (ins!pc) pc). pc' < length ins) \<and>
    2.15 +                          (\<forall>e \<in> set et. fst (snd (snd e)) < length ins)"
    2.16 +
    2.17    exec :: "jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> instr list \<Rightarrow> state step_type"
    2.18    "exec G maxs rT et bs == 
    2.19 -  err_step (\<lambda>pc. app (bs!pc) G maxs rT pc et) (\<lambda>pc. eff (bs!pc) G pc et)"
    2.20 +  err_step (size bs) (\<lambda>pc. app (bs!pc) G maxs rT pc et) (\<lambda>pc. eff (bs!pc) G pc et)"
    2.21  
    2.22    kiljvm :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> 
    2.23               instr list \<Rightarrow> state list \<Rightarrow> state list"
    2.24 @@ -22,7 +26,7 @@
    2.25    wt_kil :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 
    2.26               exception_table \<Rightarrow> instr list \<Rightarrow> bool"
    2.27    "wt_kil G C pTs rT mxs mxl et ins ==
    2.28 -   bounded (exec G mxs rT et ins) (size ins) \<and> 0 < size ins \<and> 
    2.29 +   check_bounded ins et \<and> 0 < size ins \<and> 
    2.30     (let first  = Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err));
    2.31          start  = OK first#(replicate (size ins - 1) (OK None));
    2.32          result = kiljvm G mxs (1+size pTs+mxl) rT et ins start
    2.33 @@ -33,6 +37,65 @@
    2.34    wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)). wt_kil G C (snd sig) rT maxs maxl et b) G"
    2.35  
    2.36  
    2.37 +
    2.38 +text {*
    2.39 +  Executability of @{term check_bounded}:
    2.40 +*}
    2.41 +consts
    2.42 +  list_all'_rec :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> bool"
    2.43 +primrec
    2.44 +  "list_all'_rec P n []     = True"
    2.45 +  "list_all'_rec P n (x#xs) = (P x n \<and> list_all'_rec P (Suc n) xs)"
    2.46 +
    2.47 +constdefs
    2.48 +  list_all' :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
    2.49 +  "list_all' P xs \<equiv> list_all'_rec P 0 xs"
    2.50 +
    2.51 +lemma list_all'_rec:
    2.52 +  "\<And>n. list_all'_rec P n xs = (\<forall>p < size xs. P (xs!p) (p+n))"
    2.53 +  apply (induct xs)
    2.54 +  apply auto
    2.55 +  apply (case_tac p)
    2.56 +  apply auto
    2.57 +  done
    2.58 +
    2.59 +lemma list_all' [iff]:
    2.60 +  "list_all' P xs = (\<forall>n < size xs. P (xs!n) n)"
    2.61 +  by (unfold list_all'_def) (simp add: list_all'_rec)
    2.62 +
    2.63 +lemma list_all_ball:
    2.64 +  "list_all P xs = (\<forall>x \<in> set xs. P x)"
    2.65 +  by (induct xs) auto
    2.66 +
    2.67 +lemma [code]:
    2.68 +  "check_bounded ins et = 
    2.69 +  (list_all' (\<lambda>i pc. list_all (\<lambda>pc'. pc' < length ins) (succs i pc)) ins \<and> 
    2.70 +   list_all (\<lambda>e. fst (snd (snd e)) < length ins) et)"
    2.71 +  by (simp add: list_all_ball check_bounded_def)
    2.72 +  
    2.73 +text {*
    2.74 +  Lemmas for Kildall instantiation
    2.75 +*}
    2.76 +
    2.77 +lemma check_bounded_is_bounded:
    2.78 +  "check_bounded ins et \<Longrightarrow> bounded (\<lambda>pc. eff (ins!pc) G pc et) (length ins)"
    2.79 +  apply (unfold bounded_def eff_def)
    2.80 +  apply clarify
    2.81 +  apply simp
    2.82 +  apply (unfold check_bounded_def)
    2.83 +  apply clarify
    2.84 +  apply (erule disjE)
    2.85 +   apply blast
    2.86 +  apply (erule allE, erule impE, assumption)
    2.87 +  apply (unfold xcpt_eff_def)
    2.88 +  apply clarsimp    
    2.89 +  apply (drule xcpt_names_in_et)
    2.90 +  apply clarify
    2.91 +  apply (drule bspec, assumption)
    2.92 +  apply simp
    2.93 +  done
    2.94 +   
    2.95 +
    2.96  lemma special_ex_swap_lemma [iff]: 
    2.97    "(? X. (? n. X = A n & P n) & Q X) = (? n. Q(A n) & P n)"
    2.98    by blast
    2.99 @@ -46,36 +109,6 @@
   2.100    "non_empty (\<lambda>pc. eff (bs!pc) G pc et)" 
   2.101    by (simp add: non_empty_def eff_def non_empty_succs)
   2.102  
   2.103 -lemma listn_Cons_Suc [elim!]:
   2.104 -  "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"
   2.105 -  by (cases n) auto
   2.106 -
   2.107 -lemma listn_appendE [elim!]:
   2.108 -  "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" 
   2.109 -proof -
   2.110 -  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"
   2.111 -    (is "\<And>n. ?list a n \<Longrightarrow> \<exists>n1 n2. ?P a n n1 n2")
   2.112 -  proof (induct a)
   2.113 -    fix n assume "?list [] n"
   2.114 -    hence "?P [] n 0 n" by simp
   2.115 -    thus "\<exists>n1 n2. ?P [] n n1 n2" by fast
   2.116 -  next
   2.117 -    fix n l ls
   2.118 -    assume "?list (l#ls) n"
   2.119 -    then obtain n' where n: "n = Suc n'" "l \<in> A" and "ls@b \<in> list n' A" by fastsimp
   2.120 -    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"
   2.121 -    hence "\<exists>n1 n2. n' = n1 + n2 \<and> ls \<in> list n1 A \<and> b \<in> list n2 A" .
   2.122 -    then obtain n1 n2 where "n' = n1 + n2" "ls \<in> list n1 A" "b \<in> list n2 A" by fast
   2.123 -    with n have "?P (l#ls) n (n1+1) n2" by simp
   2.124 -    thus "\<exists>n1 n2. ?P (l#ls) n n1 n2" by fastsimp
   2.125 -  qed
   2.126 -  moreover
   2.127 -  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"
   2.128 -  ultimately
   2.129 -  show ?thesis by blast
   2.130 -qed
   2.131 -
   2.132 -
   2.133  theorem exec_pres_type:
   2.134    "wf_prog wf_mb S \<Longrightarrow> 
   2.135    pres_type (exec S maxs rT et bs) (size bs) (states S maxs maxr)"
   2.136 @@ -172,15 +205,6 @@
   2.137  
   2.138  lemmas [iff] = not_None_eq
   2.139  
   2.140 -lemma map_fst_eq:
   2.141 -  "map fst (map (\<lambda>z. (f z, x z)) a) = map fst (map (\<lambda>z. (f z, y z)) a)"
   2.142 -  by (induct a) auto
   2.143 -
   2.144 -lemma succs_stable_eff:
   2.145 -  "succs_stable (sup_state_opt G) (\<lambda>pc. eff (bs!pc) G pc et)"
   2.146 -  apply (unfold succs_stable_def eff_def xcpt_eff_def)
   2.147 -  apply (simp add: map_fst_eq)
   2.148 -  done
   2.149  
   2.150  lemma sup_state_opt_unfold:
   2.151    "sup_state_opt G \<equiv> Opt.le (Product.le (Listn.le (subtype G)) (Listn.le (Err.le (subtype G))))"
   2.152 @@ -193,25 +217,32 @@
   2.153  lemma app_mono:
   2.154    "app_mono (sup_state_opt G) (\<lambda>pc. app (bs!pc) G maxs rT pc et) (length bs) (opt_states G maxs maxr)"
   2.155    by (unfold app_mono_def lesub_def) (blast intro: EffectMono.app_mono)
   2.156 +  
   2.157  
   2.158 -lemma le_list_appendI:
   2.159 -  "\<And>b c d. a <=[r] b \<Longrightarrow> c <=[r] d \<Longrightarrow> a@c <=[r] b@d"
   2.160 -apply (induct a)
   2.161 - apply simp
   2.162 -apply (case_tac b)
   2.163 -apply auto
   2.164 -done
   2.165 -
   2.166 -lemma le_listI:
   2.167 -  "length a = length b \<Longrightarrow> (\<And>n. n < length a \<Longrightarrow> a!n <=_r b!n) \<Longrightarrow> a <=[r] b"
   2.168 -  apply (unfold lesub_def Listn.le_def)
   2.169 -  apply (simp add: list_all2_conv_all_nth)
   2.170 +lemma lesubstep_type_simple:
   2.171 +  "a <=[Product.le (op =) r] b \<Longrightarrow> a <=|r| b"
   2.172 +  apply (unfold lesubstep_type_def)
   2.173 +  apply clarify
   2.174 +  apply (simp add: set_conv_nth)
   2.175 +  apply clarify
   2.176 +  apply (drule le_listD, assumption)
   2.177 +  apply (clarsimp simp add: lesub_def Product.le_def)
   2.178 +  apply (rule exI)
   2.179 +  apply (rule conjI)
   2.180 +   apply (rule exI)
   2.181 +   apply (rule conjI)
   2.182 +    apply (rule sym)
   2.183 +    apply assumption
   2.184 +   apply assumption
   2.185 +  apply assumption
   2.186    done
   2.187    
   2.188 +
   2.189  lemma eff_mono:
   2.190    "\<lbrakk>p < length bs; s <=_(sup_state_opt G) t; app (bs!p) G maxs rT pc et t\<rbrakk>
   2.191    \<Longrightarrow> eff (bs!p) G p et s <=|sup_state_opt G| eff (bs!p) G p et t"
   2.192    apply (unfold eff_def)
   2.193 +  apply (rule lesubstep_type_simple)
   2.194    apply (rule le_list_appendI)
   2.195     apply (simp add: norm_eff_def)
   2.196     apply (rule le_listI)
   2.197 @@ -243,14 +274,14 @@
   2.198    by (unfold sup_state_opt_unfold) (blast dest: acyclic_subcls1 order_widen)
   2.199  
   2.200  theorem exec_mono:
   2.201 -  "wf_prog wf_mb G \<Longrightarrow>
   2.202 +  "wf_prog wf_mb G \<Longrightarrow> bounded (exec G maxs rT et bs) (size bs) \<Longrightarrow>
   2.203    mono (JVMType.le G maxs maxr) (exec G maxs rT et bs) (size bs) (states G maxs maxr)"  
   2.204    apply (unfold exec_def JVM_le_unfold JVM_states_unfold)  
   2.205    apply (rule mono_lift)
   2.206       apply (fold sup_state_opt_unfold opt_states_def)
   2.207       apply (erule order_sup_state_opt)
   2.208 -    apply (rule succs_stable_eff)
   2.209 -   apply (rule app_mono)
   2.210 +    apply (rule app_mono)
   2.211 +   apply assumption
   2.212    apply clarify
   2.213    apply (rule eff_mono)
   2.214    apply assumption+
   2.215 @@ -275,7 +306,7 @@
   2.216  
   2.217  
   2.218  theorem is_bcv_kiljvm:
   2.219 -  "\<lbrakk> wf_prog wf_mb G; bounded (exec G maxs rT et bs) (size bs) \<rbrakk> \<Longrightarrow> 
   2.220 +  "\<lbrakk> wf_prog wf_mb G; bounded (exec G maxs rT et bs) (size bs) \<rbrakk> \<Longrightarrow>
   2.221        is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT et bs)
   2.222               (size bs) (states G maxs maxr) (kiljvm G maxs maxr rT et bs)"
   2.223    apply (unfold kiljvm_def sl_triple_conv)
   2.224 @@ -287,8 +318,8 @@
   2.225                     dest: wf_subcls1 wf_acyclic) 
   2.226       apply (simp add: JVM_le_unfold)
   2.227      apply (erule exec_pres_type)
   2.228 -    apply assumption
   2.229 -  apply (erule exec_mono)
   2.230 +   apply assumption
   2.231 +  apply (erule exec_mono, assumption)  
   2.232    done
   2.233  
   2.234  
   2.235 @@ -306,19 +337,20 @@
   2.236  
   2.237    assume "wt_kil G C pTs rT maxs mxl et bs"
   2.238    then obtain maxr r where    
   2.239 -    bounded: "bounded (exec G maxs rT et bs) (size bs)" and
   2.240 +    bounded: "check_bounded bs et" and
   2.241      result:  "r = kiljvm G maxs maxr rT et bs ?start" and
   2.242      success: "\<forall>n < size bs. r!n \<noteq> Err" and
   2.243      instrs:  "0 < size bs" and
   2.244      maxr:    "maxr = Suc (length pTs + mxl)" 
   2.245      by (unfold wt_kil_def) simp
   2.246  
   2.247 -  from wf bounded
   2.248 -  have bcv:
   2.249 +  from bounded have "bounded (exec G maxs rT et bs) (size bs)"
   2.250 +    by (unfold exec_def) (intro bounded_lift check_bounded_is_bounded)
   2.251 +  with wf have bcv:
   2.252      "is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT et bs) 
   2.253 -            (size bs) (states G maxs maxr) (kiljvm G maxs maxr rT et bs)"
   2.254 +    (size bs) (states G maxs maxr) (kiljvm G maxs maxr rT et bs)"
   2.255      by (rule is_bcv_kiljvm)
   2.256 -
   2.257 +    
   2.258    { fix l x have "set (replicate l x) \<subseteq> {x}" by (cases "0 < l") simp+
   2.259    } note subset_replicate = this
   2.260    from istype have "set pTs \<subseteq> types G" by auto
   2.261 @@ -346,9 +378,9 @@
   2.262      s: "?start <=[JVMType.le G maxs maxr] phi'" and
   2.263      w: "wt_step (JVMType.le G maxs maxr) Err (exec G maxs rT et bs) phi'"
   2.264      by blast
   2.265 -  hence dynamic:
   2.266 -    "dynamic_wt (sup_state_opt G) (exec G maxs rT et bs) phi'"
   2.267 -    by (simp add: dynamic_wt_def exec_def JVM_le_Err_conv)
   2.268 +  hence wt_err_step:
   2.269 +    "wt_err_step (sup_state_opt G) (exec G maxs rT et bs) phi'"
   2.270 +    by (simp add: wt_err_step_def exec_def JVM_le_Err_conv)
   2.271  
   2.272    from s have le: "JVMType.le G maxs maxr (?start ! 0) (phi'!0)"
   2.273      by (drule_tac p=0 in le_listD) (simp add: lesub_def)+
   2.274 @@ -360,14 +392,14 @@
   2.275  
   2.276    from l bounded 
   2.277    have bounded': "bounded (\<lambda>pc. eff (bs!pc) G pc et) (length phi')"
   2.278 -    by (simp add: exec_def bounded_lift)  
   2.279 -  with dynamic
   2.280 -  have "static_wt (sup_state_opt G) (\<lambda>pc. app (bs!pc) G maxs rT pc et) 
   2.281 -                  (\<lambda>pc. eff (bs!pc) G pc et) (map ok_val phi')"
   2.282 -    by (auto intro: dynamic_imp_static simp add: exec_def non_empty)
   2.283 +    by (simp add: exec_def check_bounded_is_bounded)  
   2.284 +  with wt_err_step
   2.285 +  have "wt_app_eff (sup_state_opt G) (\<lambda>pc. app (bs!pc) G maxs rT pc et) 
   2.286 +                   (\<lambda>pc. eff (bs!pc) G pc et) (map ok_val phi')"
   2.287 +    by (auto intro: wt_err_imp_wt_app_eff simp add: l exec_def non_empty)
   2.288    with instrs l le bounded'
   2.289    have "wt_method G C pTs rT maxs mxl bs et (map ok_val phi')"
   2.290 -    apply (unfold wt_method_def static_wt_def)
   2.291 +    apply (unfold wt_method_def wt_app_eff_def)
   2.292      apply simp
   2.293      apply (rule conjI)
   2.294       apply (unfold wt_start_def)
   2.295 @@ -387,7 +419,8 @@
   2.296  
   2.297  theorem wt_kil_complete:
   2.298    "\<lbrakk> wt_method G C pTs rT maxs mxl bs et phi; wf_prog wf_mb G; 
   2.299 -      length phi = length bs; is_class G C; \<forall>x \<in> set pTs. is_type G x;
   2.300 +     check_bounded bs et; length phi = length bs; is_class G C; 
   2.301 +      \<forall>x \<in> set pTs. is_type G x;
   2.302        map OK phi \<in> list (length bs) (states G maxs (1+size pTs+mxl)) \<rbrakk>
   2.303    \<Longrightarrow> wt_kil G C pTs rT maxs mxl et bs"
   2.304  proof -
   2.305 @@ -396,6 +429,7 @@
   2.306    assume istype: "\<forall>x \<in> set pTs. is_type G x"
   2.307    assume length: "length phi = length bs"
   2.308    assume istype_phi: "map OK phi \<in> list (length bs) (states G maxs (1+size pTs+mxl))"
   2.309 +  assume bounded: "check_bounded bs et"
   2.310  
   2.311    assume "wt_method G C pTs rT maxs mxl bs et phi"
   2.312    then obtain
   2.313 @@ -408,37 +442,22 @@
   2.314    let ?eff  = "\<lambda>pc. eff (bs!pc) G pc et"
   2.315    let ?app   = "\<lambda>pc. app (bs!pc) G maxs rT pc et"
   2.316  
   2.317 -  have bounded_eff: "bounded ?eff (size bs)"
   2.318 -  proof (unfold bounded_def, clarify)
   2.319 -    fix pc pc' s s' assume "pc < length bs"
   2.320 -    with wt_ins have "wt_instr (bs!pc) G rT phi maxs (length bs) et pc" by fast
   2.321 -    then obtain "\<forall>(pc',s') \<in> set (?eff pc (phi!pc)). pc' < length bs"
   2.322 -      by (unfold wt_instr_def) fast
   2.323 -    hence "\<forall>pc' \<in> set (map fst (?eff pc (phi!pc))). pc' < length bs" by auto
   2.324 -    also 
   2.325 -    note succs_stable_eff 
   2.326 -    hence "map fst (?eff pc (phi!pc)) = map fst (?eff pc s)" 
   2.327 -      by (rule succs_stableD)
   2.328 -    finally have "\<forall>(pc',s') \<in> set (?eff pc s). pc' < length bs" by auto
   2.329 -    moreover assume "(pc',s') \<in> set (?eff pc s)"
   2.330 -    ultimately show "pc' < length bs" by blast
   2.331 -  qed
   2.332 -  hence bounded_exec: "bounded (exec G maxs rT et bs) (size bs)" 
   2.333 -    by (simp add: exec_def bounded_lift)
   2.334 +  from bounded
   2.335 +  have bounded_exec: "bounded (exec G maxs rT et bs) (size bs)"
   2.336 +    by (unfold exec_def) (intro bounded_lift check_bounded_is_bounded)
   2.337   
   2.338    from wt_ins
   2.339 -  have "static_wt (sup_state_opt G) ?app ?eff phi"
   2.340 -    apply (unfold static_wt_def wt_instr_def lesub_def)
   2.341 +  have "wt_app_eff (sup_state_opt G) ?app ?eff phi"
   2.342 +    apply (unfold wt_app_eff_def wt_instr_def lesub_def)
   2.343      apply (simp (no_asm) only: length)
   2.344      apply blast
   2.345      done
   2.346 -
   2.347 -  with bounded_eff
   2.348 -  have "dynamic_wt (sup_state_opt G) (err_step ?app ?eff) (map OK phi)"
   2.349 -    by - (erule static_imp_dynamic, simp add: length)
   2.350 -  hence dynamic:
   2.351 -    "dynamic_wt (sup_state_opt G) (exec G maxs rT et bs) (map OK phi)"
   2.352 -    by (unfold exec_def)
   2.353 +  with bounded_exec
   2.354 +  have "wt_err_step (sup_state_opt G) (err_step (size phi) ?app ?eff) (map OK phi)"
   2.355 +    by - (erule wt_app_eff_imp_wt_err,simp add: exec_def length)
   2.356 +  hence wt_err:
   2.357 +    "wt_err_step (sup_state_opt G) (exec G maxs rT et bs) (map OK phi)"
   2.358 +    by (unfold exec_def) (simp add: length)
   2.359   
   2.360    let ?maxr = "1+size pTs+mxl"
   2.361    from wf bounded_exec
   2.362 @@ -501,13 +520,13 @@
   2.363      ultimately show ?thesis by (rule le_listI)
   2.364    qed         
   2.365  
   2.366 -  from dynamic
   2.367 +  from wt_err
   2.368    have "wt_step (JVMType.le G maxs ?maxr) Err (exec G maxs rT et bs) ?phi"
   2.369 -    by (simp add: dynamic_wt_def JVM_le_Err_conv)  
   2.370 +    by (simp add: wt_err_step_def JVM_le_Err_conv)  
   2.371    with start istype_phi less_phi is_bcv
   2.372    have "\<forall>p. p < length bs \<longrightarrow> kiljvm G maxs ?maxr rT et bs ?start ! p \<noteq> Err"
   2.373      by (unfold is_bcv_def) auto
   2.374 -  with bounded_exec instrs
   2.375 +  with bounded instrs
   2.376    show "wt_kil G C pTs rT maxs mxl et bs" by (unfold wt_kil_def) simp
   2.377  qed
   2.378  text {*
   2.379 @@ -593,4 +612,5 @@
   2.380    thus ?thesis by blast
   2.381  qed
   2.382  
   2.383 +
   2.384  end
     3.1 --- a/src/HOL/MicroJava/BV/Kildall.thy	Sun Mar 24 14:05:53 2002 +0100
     3.2 +++ b/src/HOL/MicroJava/BV/Kildall.thy	Sun Mar 24 14:06:21 2002 +0100
     3.3 @@ -299,8 +299,8 @@
     3.4  lemma merges_bounded_lemma:
     3.5    "\<lbrakk> semilat (A,r,f); mono r step n A; bounded step n; 
     3.6       \<forall>(p',s') \<in> set (step p (ss!p)). s' \<in> A; ss \<in> list n A; ts \<in> list n A; p < n; 
     3.7 -     ss <=[r] ts; ! p. p < n \<longrightarrow> stable r step ts p \<rbrakk> 
     3.8 -  \<Longrightarrow> merges f (step p (ss!p)) ss <=[r] ts"
     3.9 +     ss <=[r] ts; \<forall>p. p < n \<longrightarrow> stable r step ts p \<rbrakk> 
    3.10 +  \<Longrightarrow> merges f (step p (ss!p)) ss <=[r] ts" 
    3.11    apply (unfold stable_def)
    3.12    apply (rule merges_pres_le_ub)
    3.13        apply assumption
    3.14 @@ -319,7 +319,7 @@
    3.15      apply simp
    3.16     apply (simp add: le_listD)
    3.17    
    3.18 -  apply (drule lesub_step_type, assumption) 
    3.19 +  apply (drule lesub_step_typeD, assumption) 
    3.20    apply clarify
    3.21    apply (drule bspec, assumption)
    3.22    apply simp
     4.1 --- a/src/HOL/MicroJava/BV/Kildall_Lift.thy	Sun Mar 24 14:05:53 2002 +0100
     4.2 +++ b/src/HOL/MicroJava/BV/Kildall_Lift.thy	Sun Mar 24 14:06:21 2002 +0100
     4.3 @@ -11,84 +11,32 @@
     4.4  "app_mono r app n A ==
     4.5   \<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> app p t \<longrightarrow> app p s"
     4.6  
     4.7 - succs_stable :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> bool"
     4.8 -"succs_stable r step == \<forall>p t t'. map fst (step p t') = map fst (step p t)"
     4.9  
    4.10 -lemma succs_stableD:
    4.11 -  "succs_stable r step \<Longrightarrow> map fst (step p t) = map fst (step p t')"
    4.12 -  by (unfold succs_stable_def) blast
    4.13 -
    4.14 -lemma eqsub_def [simp]: "a <=_(op =) b = (a = b)" by (simp add: lesub_def)
    4.15 -
    4.16 -lemma list_le_eq [simp]: "\<And>b. a <=[op =] b = (a = b)"
    4.17 -apply (induct a) 
    4.18 - apply simp
    4.19 - apply rule
    4.20 -  apply simp
    4.21 - apply simp
    4.22 -apply (case_tac b)
    4.23 - apply simp
    4.24 -apply simp
    4.25 -done
    4.26 -
    4.27 -lemma map_err: "map_err a = zip (map fst a) (map (\<lambda>x. Err) (map snd a))"
    4.28 -apply (induct a)
    4.29 -apply (auto simp add: map_err_def map_snd_def)
    4.30 -done
    4.31 -
    4.32 -lemma map_snd: "map_snd f a = zip (map fst a) (map f (map snd a))"
    4.33 -apply (induct a)
    4.34 -apply (auto simp add: map_snd_def)
    4.35 -done
    4.36 +lemma in_map_sndD: "(a,b) \<in> set (map_snd f xs) \<Longrightarrow> \<exists>b'. (a,b') \<in> set xs"
    4.37 +  apply (induct xs)
    4.38 +  apply (auto simp add: map_snd_def)
    4.39 +  done
    4.40  
    4.41 -lemma zipI: 
    4.42 -  "\<And>b c d. a <=[r1] c \<Longrightarrow> b <=[r2] d \<Longrightarrow> zip a b <=[Product.le r1 r2] zip c d"
    4.43 -apply (induct a)
    4.44 - apply simp
    4.45 -apply (case_tac c)
    4.46 - apply simp
    4.47 -apply (case_tac b)
    4.48 - apply simp
    4.49 -apply (case_tac d)
    4.50 - apply simp
    4.51 -apply simp
    4.52 -done
    4.53 -
    4.54 -lemma step_type_ord: 
    4.55 -  "\<And>b. a <=|r| b \<Longrightarrow> map snd a <=[r] map snd b \<and> map fst a = map fst b"
    4.56 -apply (induct a)
    4.57 - apply simp
    4.58 -apply (case_tac b)
    4.59 - apply simp
    4.60 -apply simp
    4.61 -apply (auto simp add: Product.le_def lesub_def)
    4.62 -done
    4.63 +lemma bounded_lift:
    4.64 +  "bounded step n \<Longrightarrow> bounded (err_step n app step) n"
    4.65 +  apply (unfold bounded_def err_step_def error_def)
    4.66 +  apply clarify
    4.67 +  apply (erule allE, erule impE, assumption)
    4.68 +  apply (case_tac s)
    4.69 +  apply (auto simp add: map_snd_def split: split_if_asm)
    4.70 +  done
    4.71  
    4.72 -lemma map_OK_Err: 
    4.73 -  "\<And>y. length y = length x \<Longrightarrow> map OK x <=[Err.le r] map (\<lambda>x. Err) y"
    4.74 -apply (induct x)
    4.75 - apply simp
    4.76 -apply simp
    4.77 -apply (case_tac y)
    4.78 -apply auto
    4.79 -done
    4.80 -
    4.81 -lemma map_Err_Err:
    4.82 -  "\<And>b. length a = length b \<Longrightarrow> map (\<lambda>x. Err) a <=[Err.le r] map (\<lambda>x. Err) b"
    4.83 -apply (induct a)
    4.84 - apply simp
    4.85 -apply (case_tac b)
    4.86 -apply auto
    4.87 -done
    4.88 -
    4.89 -lemma succs_stable_length: 
    4.90 -  "succs_stable r step \<Longrightarrow> length (step p t) = length (step p t')"
    4.91 -proof -
    4.92 -  assume "succs_stable r step"  
    4.93 -  hence "map fst (step p t) = map fst (step p t')" by (rule succs_stableD)
    4.94 -  hence "length (map fst (step p t)) = length (map fst (step p t'))" by simp
    4.95 -  thus ?thesis by simp
    4.96 -qed
    4.97 +lemma boundedD2:
    4.98 +  "bounded (err_step n app step) n \<Longrightarrow> 
    4.99 +  p < n \<Longrightarrow>  app p a \<Longrightarrow> (q,b) \<in> set (step p a) \<Longrightarrow> 
   4.100 +  q < n"
   4.101 +  apply (simp add: bounded_def err_step_def)
   4.102 +  apply (erule allE, erule impE, assumption)
   4.103 +  apply (erule_tac x = "OK a" in allE, drule bspec)
   4.104 +   apply (simp add: map_snd_def)
   4.105 +   apply fast
   4.106 +  apply simp
   4.107 +  done
   4.108  
   4.109  lemma le_list_map_OK [simp]:
   4.110    "\<And>b. map OK a <=[Err.le r] map OK b = (a <=[r] b)"
   4.111 @@ -100,126 +48,76 @@
   4.112    apply simp
   4.113    done
   4.114  
   4.115 +
   4.116 +lemma map_snd_lessI:
   4.117 +  "x <=|r| y \<Longrightarrow> map_snd OK x <=|Err.le r| map_snd OK y"
   4.118 +  apply (induct x)
   4.119 +  apply (unfold lesubstep_type_def map_snd_def)
   4.120 +  apply auto
   4.121 +  done
   4.122 +
   4.123 +
   4.124  lemma mono_lift:
   4.125 -  "order r \<Longrightarrow> succs_stable r step \<Longrightarrow> app_mono r app n A \<Longrightarrow> 
   4.126 +  "order r \<Longrightarrow> app_mono r app n A \<Longrightarrow> bounded (err_step n app step) n \<Longrightarrow>
   4.127    \<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>
   4.128 -  mono (Err.le r) (err_step app step) n (err A)"
   4.129 +  mono (Err.le r) (err_step n app step) n (err A)"
   4.130  apply (unfold app_mono_def mono_def err_step_def)
   4.131  apply clarify
   4.132  apply (case_tac s)
   4.133 - apply simp
   4.134 - apply (rule le_list_refl)
   4.135 - apply simp
   4.136 + apply simp 
   4.137  apply simp
   4.138 -apply (subgoal_tac "map fst (step p arbitrary) = map fst (step p a)")
   4.139 - prefer 2
   4.140 - apply (erule succs_stableD)
   4.141  apply (case_tac t)
   4.142   apply simp
   4.143 - apply (rule conjI)
   4.144 -  apply clarify
   4.145 -  apply (simp add: map_err map_snd)
   4.146 -  apply (rule zipI)
   4.147 -   apply simp
   4.148 -  apply (rule map_OK_Err)
   4.149 -  apply (subgoal_tac "length (step p arbitrary) = length (step p a)")
   4.150 -   prefer 2
   4.151 -   apply (erule succs_stable_length)
   4.152 -  apply simp
   4.153   apply clarify
   4.154 - apply (simp add: map_err)
   4.155 - apply (rule zipI)
   4.156 -  apply simp
   4.157 - apply (rule map_Err_Err)
   4.158 - apply simp
   4.159 - apply (erule succs_stable_length)
   4.160 -apply simp
   4.161 -apply (elim allE)
   4.162 -apply (erule impE, blast)+
   4.163 -apply (rule conjI)
   4.164 + apply (simp add: lesubstep_type_def error_def)
   4.165 + apply clarify
   4.166 + apply (drule in_map_sndD)
   4.167   apply clarify
   4.168 - apply (simp add: map_snd)
   4.169 - apply (rule zipI)
   4.170 -  apply simp
   4.171 -  apply (erule succs_stableD)
   4.172 - apply (simp add: step_type_ord)
   4.173 -apply clarify
   4.174 + apply (drule boundedD2, assumption+)
   4.175 + apply (rule exI [of _ Err])
   4.176 + apply simp
   4.177 +apply simp
   4.178 +apply (erule allE, erule allE, erule allE, erule impE)
   4.179 + apply (rule conjI, assumption)
   4.180 + apply (rule conjI, assumption)
   4.181 + apply assumption
   4.182  apply (rule conjI)
   4.183 - apply clarify
   4.184 - apply (simp add: map_snd map_err)
   4.185 - apply (rule zipI)
   4.186 -  apply simp
   4.187 -  apply (erule succs_stableD)
   4.188 - apply (rule map_OK_Err)
   4.189 - apply (simp add: succs_stable_length)
   4.190 +apply clarify
   4.191 +apply (erule allE, erule allE, erule allE, erule impE)
   4.192 + apply (rule conjI, assumption)
   4.193 + apply (rule conjI, assumption)
   4.194 + apply assumption
   4.195 +apply (erule impE, assumption)
   4.196 +apply (rule map_snd_lessI, assumption)
   4.197  apply clarify
   4.198 -apply (simp add: map_err)
   4.199 -apply (rule zipI)
   4.200 - apply simp
   4.201 - apply (erule succs_stableD)
   4.202 -apply (rule map_Err_Err)
   4.203 -apply (simp add: succs_stable_length)
   4.204 +apply (simp add: lesubstep_type_def error_def)
   4.205 +apply clarify
   4.206 +apply (drule in_map_sndD)
   4.207 +apply clarify
   4.208 +apply (drule boundedD2, assumption+)
   4.209 +apply (rule exI [of _ Err])
   4.210 +apply simp
   4.211  done
   4.212   
   4.213 -lemma in_map_sndD: "(a,b) \<in> set (map_snd f xs) \<Longrightarrow> \<exists>b'. (a,b') \<in> set xs"
   4.214 -apply (induct xs)
   4.215 -apply (auto simp add: map_snd_def)
   4.216 -done
   4.217 -
   4.218 -lemma bounded_lift:
   4.219 -  "bounded (err_step app step) n = bounded step n"
   4.220 -apply (unfold bounded_def err_step_def)
   4.221 -apply rule
   4.222 -apply clarify
   4.223 - apply (erule allE, erule impE, assumption)
   4.224 - apply (erule_tac x = "OK s" in allE)
   4.225 - apply simp
   4.226 - apply (case_tac "app p s")
   4.227 -  apply (simp add: map_snd_def)
   4.228 -  apply (drule bspec, assumption)
   4.229 -  apply simp
   4.230 - apply (simp add: map_err_def map_snd_def)
   4.231 - apply (drule bspec, assumption)
   4.232 - apply simp
   4.233 -apply clarify
   4.234 -apply (case_tac s)
   4.235 - apply simp
   4.236 - apply (simp add: map_err_def)
   4.237 - apply (blast dest: in_map_sndD)
   4.238 -apply (simp split: split_if_asm)
   4.239 - apply (blast dest: in_map_sndD)
   4.240 -apply (simp add: map_err_def)
   4.241 -apply (blast dest: in_map_sndD)
   4.242 -done
   4.243 -
   4.244 -lemma set_zipD: "\<And>y. (a,b) \<in> set (zip x y) \<Longrightarrow> (a \<in> set x \<and> b \<in> set y)"
   4.245 -apply (induct x)
   4.246 - apply simp
   4.247 -apply (case_tac y)
   4.248 - apply simp
   4.249 -apply simp
   4.250 -apply blast
   4.251 -done
   4.252 +lemma in_errorD:
   4.253 +  "(x,y) \<in> set (error n) \<Longrightarrow> y = Err"
   4.254 +  by (auto simp add: error_def)
   4.255  
   4.256  lemma pres_type_lift:
   4.257    "\<forall>s\<in>A. \<forall>p. p < n \<longrightarrow> app p s \<longrightarrow> (\<forall>(q, s')\<in>set (step p s). s' \<in> A) 
   4.258 -  \<Longrightarrow> pres_type (err_step app step) n (err A)"  
   4.259 +  \<Longrightarrow> pres_type (err_step n app step) n (err A)"  
   4.260  apply (unfold pres_type_def err_step_def)
   4.261  apply clarify
   4.262  apply (case_tac b)
   4.263   apply simp
   4.264  apply (case_tac s)
   4.265 - apply (simp add: map_err)
   4.266 - apply (drule set_zipD)
   4.267 - apply clarify
   4.268 + apply simp
   4.269 + apply (drule in_errorD)
   4.270   apply simp
   4.271 - apply blast
   4.272 -apply (simp add: map_err split: split_if_asm)
   4.273 - apply (simp add: map_snd_def)
   4.274 - apply fastsimp
   4.275 -apply (drule set_zipD)
   4.276 +apply (simp add: map_snd_def split: split_if_asm)
   4.277 + apply fast
   4.278 +apply (drule in_errorD)
   4.279  apply simp
   4.280 -apply blast
   4.281  done
   4.282  
   4.283  end
     5.1 --- a/src/HOL/MicroJava/BV/LBVComplete.thy	Sun Mar 24 14:05:53 2002 +0100
     5.2 +++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Sun Mar 24 14:06:21 2002 +0100
     5.3 @@ -9,60 +9,60 @@
     5.4  theory LBVComplete = LBVSpec + Typing_Framework:
     5.5  
     5.6  constdefs
     5.7 -  contains_targets :: "['s steptype, 's certificate, 's option list, nat, nat] \<Rightarrow> bool"
     5.8 -  "contains_targets step cert phi pc n \<equiv>
     5.9 -  \<forall>(pc',s') \<in> set (step pc (OK (phi!pc))). pc' \<noteq> pc+1 \<and> pc' < n \<longrightarrow> cert!pc' = phi!pc'"
    5.10 +  contains_targets :: "['s steptype, 's certificate, 's option list, nat] \<Rightarrow> bool"
    5.11 +  "contains_targets step cert phi pc \<equiv>
    5.12 +  \<forall>(pc',s') \<in> set (step pc (OK (phi!pc))). pc' \<noteq> pc+1 \<and> pc' < length phi \<longrightarrow> cert!pc' = phi!pc'"
    5.13  
    5.14 -  fits :: "['s steptype, 's certificate, 's option list, nat] \<Rightarrow> bool"
    5.15 -  "fits step cert phi n \<equiv> \<forall>pc. pc < n \<longrightarrow> 
    5.16 -                               contains_targets step cert phi pc n \<and>
    5.17 -                               (cert!pc = None \<or> cert!pc = phi!pc)"
    5.18 +  fits :: "['s steptype, 's certificate, 's option list] \<Rightarrow> bool"
    5.19 +  "fits step cert phi \<equiv> \<forall>pc. pc < length phi \<longrightarrow> 
    5.20 +                             contains_targets step cert phi pc \<and>
    5.21 +                             (cert!pc = None \<or> cert!pc = phi!pc)"
    5.22  
    5.23 -  is_target :: "['s steptype, 's option list, nat, nat] \<Rightarrow> bool" 
    5.24 -  "is_target step phi pc' n \<equiv>
    5.25 -     \<exists>pc s'. pc' \<noteq> pc+1 \<and> pc < n \<and> (pc',s') \<in> set (step pc (OK (phi!pc)))"
    5.26 +  is_target :: "['s steptype, 's option list, nat] \<Rightarrow> bool" 
    5.27 +  "is_target step phi pc' \<equiv>
    5.28 +     \<exists>pc s'. pc' \<noteq> pc+1 \<and> pc < length phi \<and> (pc',s') \<in> set (step pc (OK (phi!pc)))"
    5.29  
    5.30 -  make_cert :: "['s steptype, 's option list, nat] \<Rightarrow> 's certificate"
    5.31 -  "make_cert step phi n \<equiv> 
    5.32 -     map (\<lambda>pc. if is_target step phi pc n then phi!pc else None) [0..n(]"
    5.33 +  make_cert :: "['s steptype, 's option list] \<Rightarrow> 's certificate"
    5.34 +  "make_cert step phi \<equiv> 
    5.35 +     map (\<lambda>pc. if is_target step phi pc then phi!pc else None) [0..length phi(]"
    5.36  
    5.37    
    5.38  lemmas [simp del] = split_paired_Ex
    5.39  
    5.40  lemma make_cert_target:
    5.41 -  "\<lbrakk> pc < n; is_target step phi pc n \<rbrakk> \<Longrightarrow> make_cert step phi n ! pc = phi!pc"
    5.42 +  "\<lbrakk> pc < length phi; is_target step phi pc \<rbrakk> \<Longrightarrow> make_cert step phi ! pc = phi!pc"
    5.43    by (simp add: make_cert_def)
    5.44  
    5.45  lemma make_cert_approx:
    5.46 -  "\<lbrakk> pc < n; make_cert step phi n ! pc \<noteq> phi!pc \<rbrakk> \<Longrightarrow> 
    5.47 -   make_cert step phi n ! pc = None"
    5.48 +  "\<lbrakk> pc < length phi; make_cert step phi ! pc \<noteq> phi!pc \<rbrakk> \<Longrightarrow> 
    5.49 +   make_cert step phi ! pc = None"
    5.50    by (auto simp add: make_cert_def)
    5.51  
    5.52  lemma make_cert_contains_targets:
    5.53 -  "pc < n \<Longrightarrow> contains_targets step (make_cert step phi n) phi pc n"
    5.54 +  "pc < length phi \<Longrightarrow> contains_targets step (make_cert step phi) phi pc"
    5.55  proof (unfold contains_targets_def, clarify)
    5.56    fix pc' s'
    5.57 -  assume "pc < n"
    5.58 +  assume "pc < length phi"
    5.59           "(pc',s') \<in> set (step pc (OK (phi ! pc)))"
    5.60           "pc' \<noteq> pc+1" and
    5.61 -    pc': "pc' < n"
    5.62 -  hence "is_target step phi pc' n"  by (auto simp add: is_target_def)
    5.63 -  with pc' show "make_cert step phi n ! pc' = phi ! pc'" 
    5.64 +    pc': "pc' < length phi"
    5.65 +  hence "is_target step phi pc'"  by (auto simp add: is_target_def)
    5.66 +  with pc' show "make_cert step phi ! pc' = phi!pc'" 
    5.67      by (auto intro: make_cert_target)
    5.68  qed
    5.69  
    5.70  theorem fits_make_cert:
    5.71 -  "fits step (make_cert step phi n) phi n"
    5.72 +  "fits step (make_cert step phi) phi"
    5.73    by (auto dest: make_cert_approx simp add: fits_def make_cert_contains_targets)
    5.74  
    5.75  lemma fitsD: 
    5.76 -  "\<lbrakk> fits step cert phi n; (pc',s') \<in> set (step pc (OK (phi ! pc)));
    5.77 -      pc' \<noteq> Suc pc; pc < n; pc' < n \<rbrakk>
    5.78 +  "\<lbrakk> fits step cert phi; (pc',s') \<in> set (step pc (OK (phi ! pc)));
    5.79 +      pc' \<noteq> Suc pc; pc < length phi; pc' < length phi \<rbrakk>
    5.80    \<Longrightarrow> cert!pc' = phi!pc'"
    5.81    by (auto simp add: fits_def contains_targets_def)
    5.82  
    5.83  lemma fitsD2:
    5.84 -   "\<lbrakk> fits step cert phi n; pc < n; cert!pc = Some s \<rbrakk>
    5.85 +   "\<lbrakk> fits step cert phi; pc < length phi; cert!pc = Some s \<rbrakk>
    5.86    \<Longrightarrow> cert!pc = phi!pc"
    5.87    by (auto simp add: fits_def)
    5.88  
    5.89 @@ -82,8 +82,9 @@
    5.90    
    5.91  lemma stable_wtl:
    5.92    assumes stable: "stable (Err.le (Opt.le r)) step (map OK phi) pc"
    5.93 -  assumes fits:   "fits step cert phi n"
    5.94 +  assumes fits:   "fits step cert phi"  
    5.95    assumes pc:     "pc < length phi"
    5.96 +  assumes bounded:"bounded step (length phi)"
    5.97    shows "wtl_inst cert f r step pc (phi!pc) \<noteq> Err"
    5.98  proof -
    5.99    from pc have [simp]: "map OK phi ! pc = OK (phi!pc)" by simp
   5.100 @@ -91,7 +92,10 @@
   5.101    have "\<forall>(q,s')\<in>set (step pc (OK (phi!pc))). s' \<le>|r (map OK phi!q)"
   5.102      by (simp add: stable_def)
   5.103    
   5.104 -
   5.105 +  have "merge cert f r pc (step pc (OK (phi ! pc))) (OK (cert ! Suc pc)) \<noteq> Err"
   5.106 +    sorry
   5.107 +  thus ?thesis by (simp add: wtl_inst_def)  
   5.108 +qed
   5.109  
   5.110  
   5.111  lemma wtl_inst_mono:
     6.1 --- a/src/HOL/MicroJava/BV/Listn.thy	Sun Mar 24 14:05:53 2002 +0100
     6.2 +++ b/src/HOL/MicroJava/BV/Listn.thy	Sun Mar 24 14:06:21 2002 +0100
     6.3 @@ -142,6 +142,20 @@
     6.4  apply auto
     6.5  done  
     6.6  
     6.7 +lemma le_list_appendI:
     6.8 +  "\<And>b c d. a <=[r] b \<Longrightarrow> c <=[r] d \<Longrightarrow> a@c <=[r] b@d"
     6.9 +apply (induct a)
    6.10 + apply simp
    6.11 +apply (case_tac b)
    6.12 +apply auto
    6.13 +done
    6.14 +
    6.15 +lemma le_listI:
    6.16 +  "length a = length b \<Longrightarrow> (\<And>n. n < length a \<Longrightarrow> a!n <=_r b!n) \<Longrightarrow> a <=[r] b"
    6.17 +  apply (unfold lesub_def Listn.le_def)
    6.18 +  apply (simp add: list_all2_conv_all_nth)
    6.19 +  done
    6.20 +
    6.21  lemma listI:
    6.22    "\<lbrakk> length xs = n; set xs <= A \<rbrakk> \<Longrightarrow> xs : list n A"
    6.23  apply (unfold list_def)
    6.24 @@ -202,6 +216,37 @@
    6.25    "\<lbrakk> xs : list n A; i < n \<rbrakk> \<Longrightarrow> (xs!i) : A"
    6.26    by auto
    6.27  
    6.28 +
    6.29 +lemma listn_Cons_Suc [elim!]:
    6.30 +  "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"
    6.31 +  by (cases n) auto
    6.32 +
    6.33 +lemma listn_appendE [elim!]:
    6.34 +  "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" 
    6.35 +proof -
    6.36 +  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"
    6.37 +    (is "\<And>n. ?list a n \<Longrightarrow> \<exists>n1 n2. ?P a n n1 n2")
    6.38 +  proof (induct a)
    6.39 +    fix n assume "?list [] n"
    6.40 +    hence "?P [] n 0 n" by simp
    6.41 +    thus "\<exists>n1 n2. ?P [] n n1 n2" by fast
    6.42 +  next
    6.43 +    fix n l ls
    6.44 +    assume "?list (l#ls) n"
    6.45 +    then obtain n' where n: "n = Suc n'" "l \<in> A" and "ls@b \<in> list n' A" by fastsimp
    6.46 +    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"
    6.47 +    hence "\<exists>n1 n2. n' = n1 + n2 \<and> ls \<in> list n1 A \<and> b \<in> list n2 A" .
    6.48 +    then obtain n1 n2 where "n' = n1 + n2" "ls \<in> list n1 A" "b \<in> list n2 A" by fast
    6.49 +    with n have "?P (l#ls) n (n1+1) n2" by simp
    6.50 +    thus "\<exists>n1 n2. ?P (l#ls) n n1 n2" by fastsimp
    6.51 +  qed
    6.52 +  moreover
    6.53 +  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"
    6.54 +  ultimately
    6.55 +  show ?thesis by blast
    6.56 +qed
    6.57 +
    6.58 +
    6.59  lemma listt_update_in_list [simp, intro!]:
    6.60    "\<lbrakk> xs : list n A; x:A \<rbrakk> \<Longrightarrow> xs[i := x] : list n A"
    6.61  apply (unfold list_def)
     7.1 --- a/src/HOL/MicroJava/BV/SemilatAlg.thy	Sun Mar 24 14:05:53 2002 +0100
     7.2 +++ b/src/HOL/MicroJava/BV/SemilatAlg.thy	Sun Mar 24 14:06:21 2002 +0100
     7.3 @@ -9,18 +9,17 @@
     7.4  theory SemilatAlg = Typing_Framework + Product:
     7.5  
     7.6  
     7.7 -syntax "@lesubstep_type" :: "(nat \<times> 's) list \<Rightarrow> 's ord \<Rightarrow> (nat \<times> 's) list \<Rightarrow> bool"
     7.8 -       ("(_ /<=|_| _)" [50, 0, 51] 50)
     7.9 -translations
    7.10 - "x <=|r| y" == "x <=[(Product.le (op =) r)] y"
    7.11 - 
    7.12 +constdefs 
    7.13 +  lesubstep_type :: "(nat \<times> 's) list \<Rightarrow> 's ord \<Rightarrow> (nat \<times> 's) list \<Rightarrow> bool"
    7.14 +                    ("(_ /<=|_| _)" [50, 0, 51] 50)
    7.15 +  "x <=|r| y \<equiv> \<forall>(p,s) \<in> set x. \<exists>s'. (p,s') \<in> set y \<and> s <=_r s'"
    7.16 +
    7.17  consts
    7.18   "@plusplussub" :: "'a list \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" ("(_ /++'__ _)" [65, 1000, 66] 65)
    7.19  primrec
    7.20    "[] ++_f y = y"
    7.21    "(x#xs) ++_f y = xs ++_f (x +_f y)"
    7.22  
    7.23 -
    7.24  constdefs
    7.25   bounded :: "'s step_type \<Rightarrow> nat \<Rightarrow> bool"
    7.26  "bounded step n == !p<n. !s. !(q,t):set(step p s). q<n"  
    7.27 @@ -45,6 +44,14 @@
    7.28    "\<lbrakk> bounded step n; p < n; (q,t) : set (step p xs) \<rbrakk> \<Longrightarrow> q < n" 
    7.29    by (unfold bounded_def, blast)
    7.30  
    7.31 +lemma lesubstep_type_refl [simp, intro]:
    7.32 +  "(\<And>x. x <=_r x) \<Longrightarrow> x <=|r| x"
    7.33 +  by (unfold lesubstep_type_def) auto
    7.34 +
    7.35 +lemma lesub_step_typeD:
    7.36 +  "a <=|r| b \<Longrightarrow> (x,y) \<in> set a \<Longrightarrow> \<exists>y'. (x, y') \<in> set b \<and> y <=_r y'"
    7.37 +  by (unfold lesubstep_type_def) blast
    7.38 +
    7.39  
    7.40  lemma list_update_le_listI [rule_format]:
    7.41    "set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> xs <=[r] ys \<longrightarrow> p < size xs \<longrightarrow>  
    7.42 @@ -162,20 +169,4 @@
    7.43  done
    7.44  
    7.45  
    7.46 -lemma lesub_step_type:
    7.47 -  "\<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'"
    7.48 -apply (induct a)
    7.49 - apply simp
    7.50 -apply simp
    7.51 -apply (case_tac b)
    7.52 - apply simp
    7.53 -apply simp
    7.54 -apply (erule disjE)
    7.55 - apply clarify
    7.56 - apply (simp add: lesub_def)
    7.57 - apply blast   
    7.58 -apply clarify
    7.59 -apply blast
    7.60 -done
    7.61 -
    7.62  end
     8.1 --- a/src/HOL/MicroJava/BV/Typing_Framework_err.thy	Sun Mar 24 14:05:53 2002 +0100
     8.2 +++ b/src/HOL/MicroJava/BV/Typing_Framework_err.thy	Sun Mar 24 14:06:21 2002 +0100
     8.3 @@ -11,28 +11,30 @@
     8.4  
     8.5  constdefs
     8.6  
     8.7 -dynamic_wt :: "'s ord \<Rightarrow> 's err step_type \<Rightarrow> 's err list \<Rightarrow> bool"
     8.8 -"dynamic_wt r step ts == wt_step (Err.le r) Err step ts"
     8.9 +wt_err_step :: "'s ord \<Rightarrow> 's err step_type \<Rightarrow> 's err list \<Rightarrow> bool"
    8.10 +"wt_err_step r step ts \<equiv> wt_step (Err.le r) Err step ts"
    8.11  
    8.12 -static_wt :: "'s ord \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool"
    8.13 -"static_wt r app step ts == 
    8.14 +wt_app_eff :: "'s ord \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool"
    8.15 +"wt_app_eff r app step ts \<equiv>
    8.16    \<forall>p < size ts. app p (ts!p) \<and> (\<forall>(q,t) \<in> set (step p (ts!p)). t <=_r ts!q)"
    8.17  
    8.18  map_snd :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'c) list"
    8.19 -"map_snd f == map (\<lambda>(x,y). (x, f y))"
    8.20 +"map_snd f \<equiv> map (\<lambda>(x,y). (x, f y))"
    8.21 +
    8.22 +error :: "nat \<Rightarrow> (nat \<times> 'a err) list"
    8.23 +"error n \<equiv> map (\<lambda>x. (x,Err)) [0..n(]"
    8.24  
    8.25 -map_err :: "('a \<times> 'b) list \<Rightarrow> ('a \<times> 'b err) list"
    8.26 -"map_err == map_snd (\<lambda>y. Err)"
    8.27 -
    8.28 -err_step :: "(nat \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's step_type \<Rightarrow> 's err step_type"
    8.29 -"err_step app step p t == case t of Err \<Rightarrow> map_err (step p arbitrary) | OK t' \<Rightarrow> 
    8.30 -  if app p t' then map_snd OK (step p t') else map_err (step p t')"
    8.31 +err_step :: "nat \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's step_type \<Rightarrow> 's err step_type"
    8.32 +"err_step n app step p t \<equiv> 
    8.33 +  case t of 
    8.34 +    Err   \<Rightarrow> error n
    8.35 +  | OK t' \<Rightarrow> if app p t' then map_snd OK (step p t') else error n"
    8.36  
    8.37  non_empty :: "'s step_type \<Rightarrow> bool"
    8.38 -"non_empty step == \<forall>p t. step p t \<noteq> []"
    8.39 +"non_empty step \<equiv> \<forall>p t. step p t \<noteq> []"
    8.40  
    8.41  
    8.42 -lemmas err_step_defs = err_step_def map_snd_def map_err_def
    8.43 +lemmas err_step_defs = err_step_def map_snd_def error_def
    8.44  
    8.45  lemma non_emptyD:
    8.46    "non_empty step \<Longrightarrow> \<exists>q t'. (q,t') \<in> set(step p t)"
    8.47 @@ -46,44 +48,38 @@
    8.48  qed
    8.49  
    8.50  
    8.51 -lemma dynamic_imp_static:
    8.52 -  "\<lbrakk> bounded step (size ts); non_empty step;
    8.53 -      dynamic_wt r (err_step app step) ts \<rbrakk> 
    8.54 -  \<Longrightarrow> static_wt r app step (map ok_val ts)"
    8.55 -proof (unfold static_wt_def, intro strip, rule conjI)
    8.56 -
    8.57 -  assume b:  "bounded step (size ts)"
    8.58 -  assume n:  "non_empty step"
    8.59 -  assume wt: "dynamic_wt r (err_step app step) ts"
    8.60 -
    8.61 -  fix p 
    8.62 -  assume "p < length (map ok_val ts)"
    8.63 -  hence lp: "p < length ts" by simp
    8.64 +lemma wt_err_imp_wt_app_eff:
    8.65 +  assumes b:  "bounded step (size ts)"
    8.66 +  assumes n:  "non_empty step"
    8.67 +  assumes wt: "wt_err_step r (err_step (size ts) app step) ts"
    8.68 +  shows "wt_app_eff r app step (map ok_val ts)"
    8.69 +proof (unfold wt_app_eff_def, intro strip, rule conjI)
    8.70 +  fix p assume "p < size (map ok_val ts)"
    8.71 +  hence lp: "p < size ts" by simp
    8.72  
    8.73    from wt lp
    8.74 -  have [intro?]: "\<And>p. p < length ts \<Longrightarrow> ts ! p \<noteq> Err" 
    8.75 -    by (unfold dynamic_wt_def wt_step_def) simp
    8.76 +  have [intro?]: "\<And>p. p < size ts \<Longrightarrow> ts ! p \<noteq> Err" 
    8.77 +    by (unfold wt_err_step_def wt_step_def) simp
    8.78  
    8.79    show app: "app p (map ok_val ts ! p)"
    8.80    proof -
    8.81      from wt lp 
    8.82      obtain s where
    8.83        OKp:  "ts ! p = OK s" and
    8.84 -      less: "\<forall>(q,t) \<in> set (err_step app step p (ts!p)). t <=_(Err.le r) ts!q"
    8.85 -      by (unfold dynamic_wt_def wt_step_def stable_def) 
    8.86 +      less: "\<forall>(q,t) \<in> set (err_step (size ts) app step p (ts!p)). t <=_(Err.le r) ts!q"
    8.87 +      by (unfold wt_err_step_def wt_step_def stable_def) 
    8.88           (auto iff: not_Err_eq)
    8.89      
    8.90 -    from n
    8.91 -    obtain q t where q: "(q,t) \<in> set(step p s)"
    8.92 -      by (blast dest: non_emptyD)
    8.93 -
    8.94 +    from n obtain q t where q: "(q,t) \<in> set(step p s)"
    8.95 +      by (blast dest: non_emptyD) 
    8.96 +    
    8.97      from lp b q
    8.98 -    have lq: "q < length ts" by (unfold bounded_def) blast
    8.99 +    have lq: "q < size ts" by (unfold bounded_def) blast
   8.100      hence "ts!q \<noteq> Err" ..
   8.101      then obtain s' where OKq: "ts ! q = OK s'" by (auto iff: not_Err_eq)      
   8.102  
   8.103 -    with OKp less q have "app p s"
   8.104 -      by (auto simp add: err_step_defs split: err.split_asm split_if_asm)
   8.105 +    with OKp less q lp have "app p s"
   8.106 +      by (auto simp add: err_step_defs split: err.split_asm split_if_asm)      
   8.107  
   8.108      with lp OKp show ?thesis by simp
   8.109    qed
   8.110 @@ -95,12 +91,12 @@
   8.111      from wt lp q
   8.112      obtain s where
   8.113        OKp:  "ts ! p = OK s" and
   8.114 -      less: "\<forall>(q,t) \<in> set (err_step app step p (ts!p)). t <=_(Err.le r) ts!q"
   8.115 -      by (unfold dynamic_wt_def wt_step_def stable_def) 
   8.116 +      less: "\<forall>(q,t) \<in> set (err_step (size ts) app step p (ts!p)). t <=_(Err.le r) ts!q"
   8.117 +      by (unfold wt_err_step_def wt_step_def stable_def) 
   8.118           (auto iff: not_Err_eq)
   8.119  
   8.120      from lp b q
   8.121 -    have lq: "q < length ts" by (unfold bounded_def) blast
   8.122 +    have lq: "q < size ts" by (unfold bounded_def) blast
   8.123      hence "ts!q \<noteq> Err" ..
   8.124      then obtain s' where OKq: "ts ! q = OK s'" by (auto iff: not_Err_eq)
   8.125  
   8.126 @@ -111,24 +107,22 @@
   8.127  qed
   8.128  
   8.129  
   8.130 -lemma static_imp_dynamic:
   8.131 -  "\<lbrakk> static_wt r app step ts; bounded step (size ts) \<rbrakk> 
   8.132 -  \<Longrightarrow> dynamic_wt r (err_step app step) (map OK ts)"
   8.133 -proof (unfold dynamic_wt_def wt_step_def, intro strip, rule conjI)
   8.134 -  assume bounded: "bounded step (size ts)"
   8.135 -  assume static:  "static_wt r app step ts"
   8.136 -  fix p assume "p < length (map OK ts)" 
   8.137 -  hence p: "p < length ts" by simp
   8.138 +lemma wt_app_eff_imp_wt_err:
   8.139 +  assumes app_eff: "wt_app_eff r app step ts"
   8.140 +  assumes bounded: "bounded (err_step (size ts) app step) (size ts)"
   8.141 +  shows "wt_err_step r (err_step (size ts) app step) (map OK ts)"
   8.142 +proof (unfold wt_err_step_def wt_step_def, intro strip, rule conjI)
   8.143 +  fix p assume "p < size (map OK ts)" 
   8.144 +  hence p: "p < size ts" by simp
   8.145    thus "map OK ts ! p \<noteq> Err" by simp
   8.146    { fix q t
   8.147 -    assume q: "(q,t) \<in> set (err_step app step p (map OK ts ! p))" 
   8.148 -    with p static obtain 
   8.149 +    assume q: "(q,t) \<in> set (err_step (size ts) app step p (map OK ts ! p))" 
   8.150 +    with p app_eff obtain 
   8.151        "app p (ts ! p)" "\<forall>(q,t) \<in> set (step p (ts!p)). t <=_r ts!q"
   8.152 -      by (unfold static_wt_def) blast
   8.153 +      by (unfold wt_app_eff_def) blast
   8.154      moreover
   8.155 -    from q p bounded have "q < size ts" 
   8.156 -      by (clarsimp simp add: bounded_def err_step_defs 
   8.157 -          split: err.splits split_if_asm) blast+
   8.158 +    from q p bounded have "q < size ts"
   8.159 +      by - (rule boundedD)
   8.160      hence "map OK ts ! q = OK (ts!q)" by simp
   8.161      moreover
   8.162      have "p < size ts" by (rule p)
   8.163 @@ -137,7 +131,7 @@
   8.164      have "t <=_(Err.le r) map OK ts ! q" 
   8.165        by (auto simp add: err_step_def map_snd_def)
   8.166    }
   8.167 -  thus "stable (Err.le r) (err_step app step) (map OK ts) p"
   8.168 +  thus "stable (Err.le r) (err_step (size ts) app step) (map OK ts) p"
   8.169      by (unfold stable_def) blast
   8.170  qed
   8.171