# HG changeset patch
# User kleing
# Date 1024483181 -7200
# Node ID 6f0928a942d152c71fd2cafad4302cfd82f3a25c
# Parent  45be08fbdcff364d0ca753e7ff42be2b88b12369
LBV instantiantion refactored, streamlined

diff -r 45be08fbdcff -r 6f0928a942d1 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Jun 19 11:48:01 2002 +0200
+++ b/src/HOL/IsaMakefile	Wed Jun 19 12:39:41 2002 +0200
@@ -495,7 +495,9 @@
   MicroJava/BV/Product.thy MicroJava/BV/Semilat.thy \
   MicroJava/BV/Effect.thy MicroJava/BV/EffectMono.thy \
   MicroJava/BV/Typing_Framework.thy MicroJava/BV/Typing_Framework_err.thy \
-  MicroJava/BV/Kildall_Lift.thy MicroJava/BV/BVExample.thy \
+  MicroJava/BV/Typing_Framework_JVM.thy MicroJava/BV/BVExample.thy \
+  MicroJava/BV/LBVSpec.thy MicroJava/BV/LBVCorrect.thy \
+  MicroJava/BV/LBVComplete.thy MicroJava/BV/LBVJVM.thy \
   MicroJava/document/root.bib MicroJava/document/root.tex \
   MicroJava/document/introduction.tex
 	@$(ISATOOL) usedir -g true $(OUT)/HOL MicroJava
diff -r 45be08fbdcff -r 6f0928a942d1 src/HOL/MicroJava/BV/JVM.thy
--- a/src/HOL/MicroJava/BV/JVM.thy	Wed Jun 19 11:48:01 2002 +0200
+++ b/src/HOL/MicroJava/BV/JVM.thy	Wed Jun 19 12:39:41 2002 +0200
@@ -6,14 +6,10 @@
 
 header {* \isaheader{Kildall for the JVM}\label{sec:JVM} *}
 
-theory JVM = Kildall_Lift + JVMType + EffectMono + BVSpec:
+theory JVM = Kildall + Typing_Framework_JVM:
 
 
 constdefs
-  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 (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"
   "kiljvm G maxs maxr rT et bs ==
@@ -34,251 +30,6 @@
 
 
 
-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)"  
-  by (unfold bounded_def) (blast dest: check_boundedD)
-
-lemma special_ex_swap_lemma [iff]: 
-  "(? X. (? n. X = A n & P n) & Q X) = (? n. Q(A n) & P n)"
-  by blast
-
-lemmas [iff del] = not_None_eq
-
-theorem exec_pres_type:
-  "wf_prog wf_mb S \<Longrightarrow> 
-  pres_type (exec S maxs rT et bs) (size bs) (states S maxs maxr)"
-  apply (unfold exec_def JVM_states_unfold)
-  apply (rule pres_type_lift)
-  apply clarify
-  apply (case_tac s)
-   apply simp
-   apply (drule effNone)
-   apply simp  
-  apply (simp add: eff_def xcpt_eff_def norm_eff_def)
-  apply (case_tac "bs!p")
-
-  apply (clarsimp simp add: not_Err_eq)
-  apply (drule listE_nth_in, assumption)
-  apply fastsimp
-
-  apply (fastsimp simp add: not_None_eq)
-
-  apply (fastsimp simp add: not_None_eq typeof_empty_is_type)
-
-  apply clarsimp
-  apply (erule disjE)
-   apply fastsimp
-  apply clarsimp
-  apply (rule_tac x="1" in exI)
-  apply fastsimp
-
-  apply clarsimp
-  apply (erule disjE)
-   apply (fastsimp dest: field_fields fields_is_type)
-  apply (simp add: match_some_entry split: split_if_asm)
-  apply (rule_tac x=1 in exI)
-  apply fastsimp
-
-  apply clarsimp
-  apply (erule disjE)
-   apply fastsimp
-  apply (simp add: match_some_entry split: split_if_asm)
-  apply (rule_tac x=1 in exI)
-  apply fastsimp
-
-  apply clarsimp
-  apply (erule disjE)
-   apply fastsimp
-  apply clarsimp
-  apply (rule_tac x=1 in exI)
-  apply fastsimp
-
-  defer 
-
-  apply fastsimp
-  apply fastsimp
-
-  apply clarsimp
-  apply (rule_tac x="n'+2" in exI)  
-  apply simp
-  apply (drule listE_length)+
-  apply fastsimp
-
-  apply clarsimp
-  apply (rule_tac x="Suc (Suc (Suc (length ST)))" in exI)  
-  apply simp
-  apply (drule listE_length)+
-  apply fastsimp
-
-  apply clarsimp
-  apply (rule_tac x="Suc (Suc (Suc (Suc (length ST))))" in exI)  
-  apply simp
-  apply (drule listE_length)+
-  apply fastsimp
-
-  apply fastsimp
-  apply fastsimp
-  apply fastsimp
-  apply fastsimp
-
-  apply clarsimp
-  apply (erule disjE)
-   apply fastsimp
-  apply clarsimp
-  apply (rule_tac x=1 in exI)
-  apply fastsimp
-  
-  apply (erule disjE)
-   apply (clarsimp simp add: Un_subset_iff)  
-   apply (drule method_wf_mdecl, assumption+)
-   apply (clarsimp simp add: wf_mdecl_def wf_mhead_def)
-   apply fastsimp
-  apply clarsimp
-  apply (rule_tac x=1 in exI)
-  apply fastsimp
-  done
-
-lemmas [iff] = not_None_eq
-
-
-lemma sup_state_opt_unfold:
-  "sup_state_opt G \<equiv> Opt.le (Product.le (Listn.le (subtype G)) (Listn.le (Err.le (subtype G))))"
-  by (simp add: sup_state_opt_def sup_state_def sup_loc_def sup_ty_opt_def)
-
-constdefs
-  opt_states :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> (ty list \<times> ty err list) option set"
-  "opt_states G maxs maxr \<equiv> opt (\<Union>{list n (types G) |n. n \<le> maxs} \<times> list maxr (err (types G)))"
-
-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 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)
-    apply simp
-   apply simp
-   apply (simp add: lesub_def)
-   apply (case_tac s)
-    apply simp
-   apply (simp del: split_paired_All split_paired_Ex)
-   apply (elim exE conjE)
-   apply simp
-   apply (drule eff'_mono, assumption)
-   apply assumption
-  apply (simp add: xcpt_eff_def)
-  apply (rule le_listI)
-    apply simp
-  apply simp
-  apply (simp add: lesub_def)
-  apply (case_tac s)
-   apply simp
-  apply simp
-  apply (case_tac t)
-   apply simp
-  apply (clarsimp simp add: sup_state_conv)
-  done
-
-lemma order_sup_state_opt:
-  "wf_prog wf_mb G \<Longrightarrow> order (sup_state_opt G)"
-  by (unfold sup_state_opt_unfold) (blast dest: acyclic_subcls1 order_widen)
-
-theorem exec_mono:
-  "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 app_mono)
-   apply assumption
-  apply clarify
-  apply (rule eff_mono)
-  apply assumption+
-  done
-
-theorem semilat_JVM_slI:
-  "wf_prog wf_mb G \<Longrightarrow> semilat (JVMType.sl G maxs maxr)"
-  apply (unfold JVMType.sl_def stk_esl_def reg_sl_def)
-  apply (rule semilat_opt)
-  apply (rule err_semilat_Product_esl)
-  apply (rule err_semilat_upto_esl)
-  apply (rule err_semilat_JType_esl, assumption+)
-  apply (rule err_semilat_eslI)
-  apply (rule Listn_sl)
-  apply (rule err_semilat_JType_esl, assumption+)
-  done
-
-lemma sl_triple_conv:
-  "JVMType.sl G maxs maxr == 
-  (states G maxs maxr, JVMType.le G maxs maxr, JVMType.sup G maxs maxr)"
-  by (simp (no_asm) add: states_def JVMType.le_def JVMType.sup_def)
-
-
 theorem is_bcv_kiljvm:
   "\<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)
@@ -296,23 +47,31 @@
   apply (erule exec_mono, assumption)  
   done
 
-lemma map_id: "\<forall>x \<in> set xs. f (g x) = x \<Longrightarrow> map f (map g xs) = xs"
-  by (induct xs) auto
+lemma subset_replicate: "set (replicate n x) \<subseteq> {x}"
+  by (induct n) auto
+
+lemma in_set_replicate:
+  "x \<in> set (replicate n y) \<Longrightarrow> x = y"
+proof -
+  assume "x \<in> set (replicate n y)"
+  also have "set (replicate n y) \<subseteq> {y}" by (rule subset_replicate)
+  finally have "x \<in> {y}" .
+  thus ?thesis by simp
+qed
 
 theorem wt_kil_correct:
-  "\<lbrakk> wt_kil G C pTs rT maxs mxl et bs; wf_prog wf_mb G; 
-      is_class G C; \<forall>x \<in> set pTs. is_type G x \<rbrakk>
-  \<Longrightarrow> \<exists>phi. wt_method G C pTs rT maxs mxl bs et phi"
+  assumes wf:  "wf_prog wf_mb G"
+  assumes C:   "is_class G C"
+  assumes pTs: "set pTs \<subseteq> types G"
+  
+  assumes wtk: "wt_kil G C pTs rT maxs mxl et bs"
+  
+  shows "\<exists>phi. wt_method G C pTs rT maxs mxl bs et phi"
 proof -
   let ?start = "OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)))
                 #(replicate (size bs - 1) (OK None))"
 
-  assume wf:      "wf_prog wf_mb G"
-  assume isclass: "is_class G C"
-  assume istype:  "\<forall>x \<in> set pTs. is_type G x"
-
-  assume "wt_kil G C pTs rT maxs mxl et bs"
-  then obtain maxr r where    
+  from wtk obtain maxr r where    
     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
@@ -327,23 +86,14 @@
     (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
-  hence "OK ` set pTs \<subseteq> err (types G)" by auto
-  with instrs maxr isclass 
+  from C pTs instrs maxr
   have "?start \<in> list (length bs) (states G maxs maxr)"
-    apply (unfold list_def JVM_states_unfold)
-    apply simp
-    apply (rule conjI)
-     apply (simp add: Un_subset_iff)
-     apply (rule_tac B = "{Err}" in subset_trans)
-      apply (simp add: subset_replicate)
-     apply simp
-    apply (rule_tac B = "{OK None}" in subset_trans)
-     apply (simp add: subset_replicate)
-    apply simp
-    done
+    apply (unfold JVM_states_unfold)
+    apply (rule listI)
+    apply (auto intro: list_appendI dest!: in_set_replicate)
+    apply force
+    done    
+
   with bcv success result have 
     "\<exists>ts\<in>list (length bs) (states G maxs maxr).
          ?start <=[JVMType.le G maxs maxr] ts \<and>
@@ -368,11 +118,10 @@
 
   from phi' have "check_types G maxs maxr phi'" by(simp add: check_types_def)
   also from w have "phi' = map OK (map ok_val phi')" 
-    apply (clarsimp simp add: wt_step_def)
+    apply (clarsimp simp add: wt_step_def not_Err_eq) 
     apply (rule map_id [symmetric])
-    apply (clarsimp simp add: in_set_conv_decomp)
-    apply (erule_tac x = "length ys" in allE)
-    apply (clarsimp simp add: nth_append not_Err_eq)
+    apply (erule allE, erule impE, assumption)
+    apply clarsimp
     done    
   finally 
   have check_types:
@@ -409,19 +158,17 @@
 
 
 theorem wt_kil_complete:
-  "\<lbrakk> wt_method G C pTs rT maxs mxl bs et phi; wf_prog wf_mb G; 
-      is_class G C; 
-      \<forall>x \<in> set pTs. is_type G x \<rbrakk>
-  \<Longrightarrow> wt_kil G C pTs rT maxs mxl et bs"
+  assumes wf:  "wf_prog wf_mb G"  
+  assumes C:   "is_class G C"
+  assumes pTs: "set pTs \<subseteq> types G"
+
+  assumes wtm: "wt_method G C pTs rT maxs mxl bs et phi"
+
+  shows "wt_kil G C pTs rT maxs mxl et bs"
 proof -
-  assume wf: "wf_prog wf_mb G"  
-  assume isclass: "is_class G C"
-  assume istype: "\<forall>x \<in> set pTs. is_type G x"
-  
   let ?mxr = "1+size pTs+mxl"
   
-  assume "wt_method G C pTs rT maxs mxl bs et phi"
-  then obtain
+  from wtm obtain
     instrs:   "0 < length bs" and
     len:      "length phi = length bs" and
     bounded:  "check_bounded bs et" and
@@ -456,37 +203,25 @@
     "wt_err_step (sup_state_opt G) (exec G maxs rT et bs) (map OK phi)"
     by (unfold exec_def) (simp add: len)
  
-  let ?maxr = "1+size pTs+mxl"
   from wf bounded_exec
   have is_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)"
+    "is_bcv (JVMType.le G maxs ?mxr) Err (exec G maxs rT et bs) 
+            (size bs) (states G maxs ?mxr) (kiljvm G maxs ?mxr rT et bs)"
     by (rule is_bcv_kiljvm)
 
   let ?start = "OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)))
                 #(replicate (size bs - 1) (OK None))"
 
-  { 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
-  hence "OK ` set pTs \<subseteq> err (types G)" by auto
-  with instrs isclass have start:
-    "?start \<in> list (length bs) (states G maxs ?maxr)"
-    apply (unfold list_def JVM_states_unfold)
-    apply simp
-    apply (rule conjI)
-     apply (simp add: Un_subset_iff)
-     apply (rule_tac B = "{Err}" in subset_trans)
-      apply (simp add: subset_replicate)
-     apply simp
-    apply (rule_tac B = "{OK None}" in subset_trans)
-     apply (simp add: subset_replicate)
-    apply simp
-    done
+  from C pTs instrs
+  have start: "?start \<in> list (length bs) (states G maxs ?mxr)"
+    apply (unfold JVM_states_unfold)
+    apply (rule listI)
+    apply (auto intro!: list_appendI dest!: in_set_replicate)
+    apply force
+    done    
 
   let ?phi = "map OK phi"  
-  have less_phi: "?start <=[JVMType.le G maxs ?maxr] ?phi"
+  have less_phi: "?start <=[JVMType.le G maxs ?mxr] ?phi"
   proof -
     from len instrs
     have "length ?start = length (map OK phi)" by simp
@@ -499,112 +234,55 @@
       from instrs len
       have "0 < length phi" by simp
       ultimately
-      have "JVMType.le G maxs ?maxr (?start!0) (?phi!0)"
+      have "JVMType.le G maxs ?mxr (?start!0) (?phi!0)"
         by (simp add: JVM_le_Err_conv Err.le_def lesub_def)
       moreover
       { fix n'
-        have "JVMType.le G maxs ?maxr (OK None) (?phi!n)"
+        have "JVMType.le G maxs ?mxr (OK None) (?phi!n)"
           by (auto simp add: JVM_le_Err_conv Err.le_def lesub_def 
             split: err.splits)        
         hence "\<lbrakk> n = Suc n'; n < length ?start \<rbrakk> 
-          \<Longrightarrow> JVMType.le G maxs ?maxr (?start!n) (?phi!n)"
+          \<Longrightarrow> JVMType.le G maxs ?mxr (?start!n) (?phi!n)"
           by simp
       }
       ultimately
-      have "n < length ?start \<Longrightarrow> (?start!n) <=_(JVMType.le G maxs ?maxr) (?phi!n)"
+      have "n < length ?start \<Longrightarrow> (?start!n) <=_(JVMType.le G maxs ?mxr) (?phi!n)"
         by (unfold lesub_def) (cases n, blast+)
     } 
     ultimately show ?thesis by (rule le_listI)
   qed         
 
   from wt_err
-  have "wt_step (JVMType.le G maxs ?maxr) Err (exec G maxs rT et bs) ?phi"
+  have "wt_step (JVMType.le G maxs ?mxr) Err (exec G maxs rT et bs) ?phi"
     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"
+  have "\<forall>p. p < length bs \<longrightarrow> kiljvm G maxs ?mxr rT et bs ?start ! p \<noteq> Err"
     by (unfold is_bcv_def) auto
   with bounded instrs
   show "wt_kil G C pTs rT maxs mxl et bs" by (unfold wt_kil_def) simp
 qed
 
-lemma is_type_pTs:
-  "\<lbrakk> wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; (sig,rT,code) \<in> set mdecls; 
-      t \<in> set (snd sig) \<rbrakk>
-  \<Longrightarrow> is_type G t"
-proof -
-  assume "wf_prog wf_mb G" 
-         "(C,S,fs,mdecls) \<in> set G"
-         "(sig,rT,code) \<in> set mdecls"
-  hence "wf_mdecl wf_mb G C (sig,rT,code)"
-    by (unfold wf_prog_def wf_cdecl_def) auto
-  hence "\<forall>t \<in> set (snd sig). is_type G t" 
-    by (unfold wf_mdecl_def wf_mhead_def) auto
-  moreover
-  assume "t \<in> set (snd sig)"
-  ultimately
-  show ?thesis by blast
-qed
-
 
 theorem jvm_kildall_sound_complete:
   "wt_jvm_prog_kildall G = (\<exists>Phi. wt_jvm_prog G Phi)"
 proof 
-  assume wtk: "wt_jvm_prog_kildall G"
-
-  then obtain wf_mb where
-    wf: "wf_prog wf_mb G"
-    by (auto simp add: wt_jvm_prog_kildall_def)
-
   let ?Phi = "\<lambda>C sig. let (C,rT,(maxs,maxl,ins,et)) = the (method (G,C) sig) in 
               SOME phi. wt_method G C (snd sig) rT maxs maxl ins et phi"
-   
-  { fix C S fs mdecls sig rT code
-    assume "(C,S,fs,mdecls) \<in> set G" "(sig,rT,code) \<in> set mdecls"
-    with wf
-    have "method (G,C) sig = Some (C,rT,code) \<and> is_class G C \<and> (\<forall>t \<in> set (snd sig). is_type G t)"
-      by (simp add: methd is_type_pTs)
-  } note this [simp]
- 
-  from wtk
-  have "wt_jvm_prog G ?Phi"
-    apply (unfold wt_jvm_prog_def wt_jvm_prog_kildall_def wf_prog_def wf_cdecl_def)
-    apply clarsimp
-    apply (drule bspec, assumption)
-    apply (unfold wf_mdecl_def)
-    apply clarsimp
-    apply (drule bspec, assumption)
-    apply clarsimp
-    apply (drule wt_kil_correct [OF _ wf])
-    apply (auto intro: someI)
+  
+  assume "wt_jvm_prog_kildall G"
+  hence "wt_jvm_prog G ?Phi"
+    apply (unfold wt_jvm_prog_def wt_jvm_prog_kildall_def)
+    apply (erule jvm_prog_lift)
+    apply (auto dest!: wt_kil_correct intro: someI)
     done
-
-  thus "\<exists>Phi. wt_jvm_prog G Phi" by blast
+  thus "\<exists>Phi. wt_jvm_prog G Phi" by fast
 next
   assume "\<exists>Phi. wt_jvm_prog G Phi"
-  then obtain Phi where wt: "wt_jvm_prog G Phi" ..
-
-  then obtain wf_mb where
-    wf: "wf_prog wf_mb G"
-    by (auto simp add: wt_jvm_prog_def)
-
-  { fix C S fs mdecls sig rT code
-    assume "(C,S,fs,mdecls) \<in> set G" "(sig,rT,code) \<in> set mdecls"
-    with wf
-    have "method (G,C) sig = Some (C,rT,code) \<and> is_class G C \<and> (\<forall>t \<in> set (snd sig). is_type G t)"
-      by (simp add: methd is_type_pTs)
-  } note this [simp]
- 
-  from wt
-  show "wt_jvm_prog_kildall G"
-    apply (unfold wt_jvm_prog_def wt_jvm_prog_kildall_def wf_prog_def wf_cdecl_def)
-    apply clarsimp
-    apply (drule bspec, assumption)
-    apply (unfold wf_mdecl_def)
-    apply clarsimp
-    apply (drule bspec, assumption)
-    apply clarsimp
-    apply (drule wt_kil_complete [OF _ wf])
-    apply (auto intro: someI)
+  thus "wt_jvm_prog_kildall G"
+    apply (clarify)
+    apply (unfold wt_jvm_prog_def wt_jvm_prog_kildall_def)
+    apply (erule jvm_prog_lift)
+    apply (auto intro: wt_kil_complete)
     done
 qed
 
diff -r 45be08fbdcff -r 6f0928a942d1 src/HOL/MicroJava/BV/Kildall_Lift.thy
--- a/src/HOL/MicroJava/BV/Kildall_Lift.thy	Wed Jun 19 11:48:01 2002 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,105 +0,0 @@
-(*  Title:      HOL/MicroJava/BV/Kildall_Lift.thy
-    ID:         $Id$
-    Author:     Gerwin Klein
-    Copyright   2001 TUM
-*)
-
-theory Kildall_Lift = Kildall + Typing_Framework_err:
-
-constdefs
- app_mono :: "'s ord \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool"
-"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"
-
-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 le_list_map_OK [simp]:
-  "\<And>b. map OK a <=[Err.le r] map OK b = (a <=[r] b)"
-  apply (induct a)
-   apply simp
-  apply simp
-  apply (case_tac b)
-   apply simp
-  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> 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 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 simp
-apply (case_tac t)
- apply simp
- apply clarify
- apply (simp add: lesubstep_type_def error_def)
- apply clarify
- apply (drule in_map_sndD)
- apply clarify
- apply (drule bounded_err_stepD, 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 (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: lesubstep_type_def error_def)
-apply clarify
-apply (drule in_map_sndD)
-apply clarify
-apply (drule bounded_err_stepD, assumption+)
-apply (rule exI [of _ Err])
-apply simp
-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 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
- apply (drule in_errorD)
- apply simp
-apply (simp add: map_snd_def split: split_if_asm)
- apply fast
-apply (drule in_errorD)
-apply simp
-done
-
-end
diff -r 45be08fbdcff -r 6f0928a942d1 src/HOL/MicroJava/BV/LBVJVM.thy
--- a/src/HOL/MicroJava/BV/LBVJVM.thy	Wed Jun 19 11:48:01 2002 +0200
+++ b/src/HOL/MicroJava/BV/LBVJVM.thy	Wed Jun 19 12:39:41 2002 +0200
@@ -6,7 +6,7 @@
 
 header {* \isaheader{LBV for the JVM}\label{sec:JVM} *}
 
-theory LBVJVM = LBVCorrect + LBVComplete + EffectMono + BVSpec + Kildall_Lift:
+theory LBVJVM = LBVCorrect + LBVComplete + Typing_Framework_JVM:
 
 types prog_cert = "cname \<Rightarrow> sig \<Rightarrow> state list"
 
@@ -15,10 +15,6 @@
   "check_cert G mxs mxr n cert \<equiv> check_types G mxs mxr cert \<and> length cert = n+1 \<and>
                                  (\<forall>i<n. cert!i \<noteq> Err) \<and> cert!n = OK None"
 
-  exec :: "jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> instr list \<Rightarrow> state step_type"
-  "exec G maxs rT et bs \<equiv>
-  err_step (size bs) (\<lambda>pc. app (bs!pc) G maxs rT pc et) (\<lambda>pc. eff (bs!pc) G pc et)"
-
   lbvjvm :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> 
              state list \<Rightarrow> instr list \<Rightarrow> state \<Rightarrow> state"
   "lbvjvm G maxs maxr rT et cert bs \<equiv>
@@ -46,282 +42,7 @@
   "prg_cert G phi C sig \<equiv> let (C,rT,(maxs,maxl,ins,et)) = the (method (G,C) sig) in 
                            mk_cert G maxs rT et ins (phi C sig)"
  
-
-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 LBV instantiation
-*}
-
-lemma check_bounded_is_bounded:
-  "check_bounded ins et \<Longrightarrow> bounded (\<lambda>pc. eff (ins!pc) G pc et) (length ins)"
-  by (unfold bounded_def) (auto dest: check_boundedD)
-
-lemma check_certD:
-  "check_cert G mxs mxr n cert \<Longrightarrow> cert_ok cert n Err (OK None) (states G mxs mxr)"
-  apply (unfold cert_ok_def check_cert_def check_types_def)
-  apply (auto simp add: list_all_ball)
-  done
-
-lemma special_ex_swap_lemma [iff]: 
-  "(? X. (? n. X = A n & P n) & Q X) = (? n. Q(A n) & P n)"
-  by blast
-
-lemmas [iff del] = not_None_eq
-
-theorem exec_pres_type [intro]:
-  "wf_prog wf_mb S \<Longrightarrow> 
-  pres_type (exec S maxs rT et bs) (size bs) (states S maxs maxr)"
-  apply (unfold exec_def JVM_states_unfold)
-  apply (rule pres_type_lift)
-  apply clarify
-  apply (case_tac s)
-   apply simp
-   apply (drule effNone)
-   apply simp  
-  apply (simp add: eff_def xcpt_eff_def norm_eff_def)
-  apply (case_tac "bs!p")
-
-  apply (clarsimp simp add: not_Err_eq)
-  apply (drule listE_nth_in, assumption)
-  apply fastsimp
-
-  apply (fastsimp simp add: not_None_eq)
-
-  apply (fastsimp simp add: not_None_eq typeof_empty_is_type)
-
-  apply clarsimp
-  apply (erule disjE)
-   apply fastsimp
-  apply clarsimp
-  apply (rule_tac x="1" in exI)
-  apply fastsimp
-
-  apply clarsimp
-  apply (erule disjE)
-   apply (fastsimp dest: field_fields fields_is_type)
-  apply (simp add: match_some_entry split: split_if_asm)
-  apply (rule_tac x=1 in exI)
-  apply fastsimp
-
-  apply clarsimp
-  apply (erule disjE)
-   apply fastsimp
-  apply (simp add: match_some_entry split: split_if_asm)
-  apply (rule_tac x=1 in exI)
-  apply fastsimp
-
-  apply clarsimp
-  apply (erule disjE)
-   apply fastsimp
-  apply clarsimp
-  apply (rule_tac x=1 in exI)
-  apply fastsimp
-
-  defer 
-
-  apply fastsimp
-  apply fastsimp
-
-  apply clarsimp
-  apply (rule_tac x="n'+2" in exI)  
-  apply simp
-  apply (drule listE_length)+
-  apply fastsimp
-
-  apply clarsimp
-  apply (rule_tac x="Suc (Suc (Suc (length ST)))" in exI)  
-  apply simp
-  apply (drule listE_length)+
-  apply fastsimp
-
-  apply clarsimp
-  apply (rule_tac x="Suc (Suc (Suc (Suc (length ST))))" in exI)  
-  apply simp
-  apply (drule listE_length)+
-  apply fastsimp
-
-  apply fastsimp
-  apply fastsimp
-  apply fastsimp
-  apply fastsimp
-
-  apply clarsimp
-  apply (erule disjE)
-   apply fastsimp
-  apply clarsimp
-  apply (rule_tac x=1 in exI)
-  apply fastsimp
-  
-  apply (erule disjE)
-   apply (clarsimp simp add: Un_subset_iff)  
-   apply (drule method_wf_mdecl, assumption+)
-   apply (clarsimp simp add: wf_mdecl_def wf_mhead_def)
-   apply fastsimp
-  apply clarsimp
-  apply (rule_tac x=1 in exI)
-  apply fastsimp
-  done
-
-lemmas [iff] = not_None_eq
-
-
-lemma sup_state_opt_unfold:
-  "sup_state_opt G \<equiv> Opt.le (Product.le (Listn.le (subtype G)) (Listn.le (Err.le (subtype G))))"
-  by (simp add: sup_state_opt_def sup_state_def sup_loc_def sup_ty_opt_def)
-
-constdefs
-  opt_states :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> (ty list \<times> ty err list) option set"
-  "opt_states G maxs maxr \<equiv> opt (\<Union>{list n (types G) |n. n \<le> maxs} \<times> list maxr (err (types G)))"
-
-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 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)
-    apply simp
-   apply simp
-   apply (simp add: lesub_def)
-   apply (case_tac s)
-    apply simp
-   apply (simp del: split_paired_All split_paired_Ex)
-   apply (elim exE conjE)
-   apply simp
-   apply (drule eff'_mono, assumption)
-   apply assumption
-  apply (simp add: xcpt_eff_def)
-  apply (rule le_listI)
-    apply simp
-  apply simp
-  apply (simp add: lesub_def)
-  apply (case_tac s)
-   apply simp
-  apply simp
-  apply (case_tac t)
-   apply simp
-  apply (clarsimp simp add: sup_state_conv)
-  done
-
-lemma order_sup_state_opt:
-  "wf_prog wf_mb G \<Longrightarrow> order (sup_state_opt G)"
-  by (unfold sup_state_opt_unfold) (blast dest: acyclic_subcls1 order_widen)
-
-theorem exec_mono:
-  "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 app_mono)
-   apply assumption
-  apply clarify
-  apply (rule eff_mono)
-  apply assumption+
-  done
-
-theorem semilat_JVM_slI [intro]:
-  "wf_prog wf_mb G \<Longrightarrow> semilat (JVMType.sl G maxs maxr)"
-  apply (unfold JVMType.sl_def stk_esl_def reg_sl_def)
-  apply (rule semilat_opt)
-  apply (rule err_semilat_Product_esl)
-  apply (rule err_semilat_upto_esl)
-  apply (rule err_semilat_JType_esl, assumption+)
-  apply (rule err_semilat_eslI)
-  apply (rule Listn_sl)
-  apply (rule err_semilat_JType_esl, assumption+)
-  done
-
-lemma sl_triple_conv:
-  "JVMType.sl G maxs maxr == 
-  (states G maxs maxr, JVMType.le G maxs maxr, JVMType.sup G maxs maxr)"
-  by (simp (no_asm) add: states_def JVMType.le_def JVMType.sup_def)
-
-
-lemma list_appendI:
-  "\<lbrakk>a \<in> list x A; b \<in> list y A\<rbrakk> \<Longrightarrow> a @ b \<in> list (x+y) A"
-  apply (unfold list_def)
-  apply (simp (no_asm))
-  apply blast
-  done
-
-lemma list_map [simp]:
-  "(map f xs \<in> list (length xs) A) = (f ` set xs \<subseteq> A)"
-  apply (unfold list_def)
-  apply simp
-  done
-
-lemma [iff]:
-  "(OK ` A \<subseteq> err B) = (A \<subseteq> B)"
-  apply (unfold err_def)
-  apply blast
-  done
-
-lemma [intro]:
-  "x \<in> A \<Longrightarrow> replicate n x \<in> list n A"
-  by (induct n, auto)
-
-
 lemma wt_method_def2:
   fixes pTs and mxl and G and mxs and rT and et and bs and phi 
   defines [simp]: "mxr   \<equiv> 1 + length pTs + mxl"
@@ -341,6 +62,12 @@
            dest: check_bounded_is_bounded boundedD)
 
 
+lemma check_certD:
+  "check_cert G mxs mxr n cert \<Longrightarrow> cert_ok cert n Err (OK None) (states G mxs mxr)"
+  apply (unfold cert_ok_def check_cert_def check_types_def)
+  apply (auto simp add: list_all_ball)
+  done
+
 
 lemma wt_lbv_wt_step:
   assumes wf:  "wf_prog wf_mb G"
@@ -359,7 +86,7 @@
   let ?f    = "JVMType.sup G mxs mxr"
   let ?A    = "states G mxs mxr"
 
-  have "semilat (JVMType.sl G mxs mxr)" ..
+  have "semilat (JVMType.sl G mxs mxr)" by (rule semilat_JVM_slI)
   hence "semilat (?A, ?r, ?f)" by (unfold sl_triple_conv)
   moreover
   have "top ?r Err"  by (simp add: JVM_le_unfold)
@@ -380,7 +107,7 @@
   have "cert_ok cert (length ins) Err (OK None) ?A" 
     by (unfold wt_lbv_def) (auto dest: check_certD)
   moreover
-  have "pres_type ?step (length ins) ?A" ..
+  have "pres_type ?step (length ins) ?A" by (rule exec_pres_type)
   moreover
   let ?start = "OK (Some ([],(OK (Class C))#(map OK pTs)@(replicate mxl Err)))"
   from lbv
@@ -395,12 +122,6 @@
   show ?thesis by (rule lbvs.wtl_sound_strong)
 qed
   
-
-lemma map_ident [rule_format]:
-  "(\<forall>n < length xs. f (g (xs!n)) = xs!n) \<longrightarrow> map f (map g xs) = xs"
-  by (induct xs, auto)
-    
-
 lemma wt_lbv_wt_method:
   assumes wf:  "wf_prog wf_mb G"
   assumes lbv: "wt_lbv G C pTs rT mxs mxl et cert ins"
@@ -441,8 +162,8 @@
     have "check_types G mxs ?mxr phi"
       by (simp add: check_types_def)
     also from step
-    have [symmetric]: "map OK (map ok_val phi) = phi"
-      by (auto intro!: map_ident simp add: wt_step_def)
+    have [symmetric]: "map OK (map ok_val phi) = phi" 
+      by (auto intro!: map_id simp add: wt_step_def)
     finally have "check_types G mxs ?mxr (map OK (map ok_val phi))" .
   }
   moreover {  
@@ -467,52 +188,6 @@
 qed
 
 
-lemma is_type_pTs:
-  "\<lbrakk> wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; ((mn,pTs),rT,code) \<in> set mdecls \<rbrakk>
-  \<Longrightarrow> set pTs \<subseteq> types G"
-proof 
-  assume "wf_prog wf_mb G" 
-         "(C,S,fs,mdecls) \<in> set G"
-         "((mn,pTs),rT,code) \<in> set mdecls"
-  hence "wf_mdecl wf_mb G C ((mn,pTs),rT,code)"
-    by (unfold wf_prog_def wf_cdecl_def) auto  
-  hence "\<forall>t \<in> set pTs. is_type G t" 
-    by (unfold wf_mdecl_def wf_mhead_def) auto
-  moreover
-  fix t assume "t \<in> set pTs"
-  ultimately
-  have "is_type G t" by blast
-  thus "t \<in> types G" ..
-qed
-
-
-theorem jvm_lbv_correct:
-  "wt_jvm_prog_lbv G Cert \<Longrightarrow> \<exists>Phi. wt_jvm_prog G Phi"
-proof -  
-  assume wtk: "wt_jvm_prog_lbv G Cert"
-  then obtain wf_mb where wf: "wf_prog wf_mb G"
-    by (auto simp add: wt_jvm_prog_lbv_def)
-
-  let ?Phi = "\<lambda>C sig. let (C,rT,(maxs,maxl,ins,et)) = the (method (G,C) sig) in 
-              SOME phi. wt_method G C (snd sig) rT maxs maxl ins et phi"
-    
-  from wtk have "wt_jvm_prog G ?Phi"
-    apply (unfold wt_jvm_prog_def wt_jvm_prog_lbv_def wf_prog_def wf_cdecl_def)
-    apply clarsimp
-    apply (drule bspec, assumption)
-    apply (unfold wf_mdecl_def)
-    apply clarsimp
-    apply (drule bspec, assumption)
-    apply clarsimp
-    apply (frule methd [OF wf], assumption+)
-    apply (frule is_type_pTs [OF wf], assumption+)
-    apply (drule wt_lbv_wt_method [OF wf])
-    apply (auto intro: someI)
-    done
-  thus ?thesis by blast
-qed
-
-
 lemma wt_method_wt_lbv:
   assumes wf:  "wf_prog wf_mb G"
   assumes wt:  "wt_method G C pTs rT mxs mxl ins et phi"
@@ -542,8 +217,7 @@
     app_eff:    "wt_app_eff (sup_state_opt G) ?app ?eff phi"
     by (simp add: wt_method_def2)
   
-
-  have "semilat (JVMType.sl G mxs ?mxr)" ..
+  have "semilat (JVMType.sl G mxs ?mxr)" by (rule semilat_JVM_slI)
   hence "semilat (?A, ?r, ?f)" by (unfold sl_triple_conv)
   moreover
   have "top ?r Err"  by (simp add: JVM_le_unfold)
@@ -563,7 +237,7 @@
   have "mono ?r ?step (length ins) ?A" by (rule exec_mono)
   hence "mono ?r ?step (length ?phi) ?A" by (simp add: length)
   moreover
-  have "pres_type ?step (length ins) ?A" ..
+  have "pres_type ?step (length ins) ?A" by (rule exec_pres_type)
   hence "pres_type ?step (length ?phi) ?A" by (simp add: length)
   moreover
   from ck_types
@@ -611,29 +285,27 @@
 qed  
 
 
+
+theorem jvm_lbv_correct:
+  "wt_jvm_prog_lbv G Cert \<Longrightarrow> \<exists>Phi. wt_jvm_prog G Phi"
+proof -  
+  let ?Phi = "\<lambda>C sig. let (C,rT,(maxs,maxl,ins,et)) = the (method (G,C) sig) in 
+              SOME phi. wt_method G C (snd sig) rT maxs maxl ins et phi"
+    
+  assume "wt_jvm_prog_lbv G Cert"
+  hence "wt_jvm_prog G ?Phi"
+    apply (unfold wt_jvm_prog_def wt_jvm_prog_lbv_def)
+    apply (erule jvm_prog_lift)
+    apply (auto dest: wt_lbv_wt_method intro: someI)
+    done
+  thus ?thesis by blast
+qed
+
 theorem jvm_lbv_complete:
   "wt_jvm_prog G Phi \<Longrightarrow> wt_jvm_prog_lbv G (prg_cert G Phi)"
-proof -
-  assume wt: "wt_jvm_prog G Phi"
-
-  then obtain wf_mb where
-    wf: "wf_prog wf_mb G"
-    by (auto simp add: wt_jvm_prog_def)
-
-  from wt show ?thesis
-    apply (unfold wt_jvm_prog_def wt_jvm_prog_lbv_def wf_prog_def wf_cdecl_def)
-    apply clarsimp
-    apply (drule bspec, assumption)
-    apply (unfold wf_mdecl_def)
-    apply clarsimp
-    apply (drule bspec, assumption)
-    apply clarsimp
-    apply (frule methd [OF wf], assumption+)
-    apply clarify
-    apply (frule is_type_pTs [OF wf], assumption+)
-    apply (drule wt_method_wt_lbv [OF wf])
-    apply (auto simp add: prg_cert_def)
-    done  
-qed
+  apply (unfold wt_jvm_prog_def wt_jvm_prog_lbv_def)
+  apply (erule jvm_prog_lift)
+  apply (auto simp add: prg_cert_def intro wt_method_wt_lbv)
+  done  
 
 end
diff -r 45be08fbdcff -r 6f0928a942d1 src/HOL/MicroJava/BV/Typing_Framework.thy
--- a/src/HOL/MicroJava/BV/Typing_Framework.thy	Wed Jun 19 11:48:01 2002 +0200
+++ b/src/HOL/MicroJava/BV/Typing_Framework.thy	Wed Jun 19 12:39:41 2002 +0200
@@ -9,7 +9,7 @@
 theory Typing_Framework = Listn:
 
 text {* 
-  The relationship between dataflow analysis and a welltyped-insruction predicate. 
+  The relationship between dataflow analysis and a welltyped-instruction predicate. 
 *}
 types
   's step_type = "nat \<Rightarrow> 's \<Rightarrow> (nat \<times> 's) list"
diff -r 45be08fbdcff -r 6f0928a942d1 src/HOL/MicroJava/BV/Typing_Framework_JVM.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Wed Jun 19 12:39:41 2002 +0200
@@ -0,0 +1,341 @@
+(*  Title:      HOL/MicroJava/BV/JVM.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow, Gerwin Klein
+    Copyright   2000 TUM
+*)
+
+header {* \isaheader{The Typing Framework for the JVM}\label{sec:JVM} *}
+
+theory Typing_Framework_JVM = Typing_Framework_err + JVMType + EffectMono + BVSpec:
+
+
+constdefs
+  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 (size bs) (\<lambda>pc. app (bs!pc) G maxs rT pc et) (\<lambda>pc. eff (bs!pc) G pc et)"
+
+constdefs
+  opt_states :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> (ty list \<times> ty err list) option set"
+  "opt_states G maxs maxr \<equiv> opt (\<Union>{list n (types G) |n. n \<le> maxs} \<times> list maxr (err (types G)))"
+
+
+section {*  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)
+  
+
+section {* Connecting JVM and Framework *}
+
+lemma check_bounded_is_bounded:
+  "check_bounded ins et \<Longrightarrow> bounded (\<lambda>pc. eff (ins!pc) G pc et) (length ins)"  
+  by (unfold bounded_def) (blast dest: check_boundedD)
+
+lemma special_ex_swap_lemma [iff]: 
+  "(? X. (? n. X = A n & P n) & Q X) = (? n. Q(A n) & P n)"
+  by blast
+
+lemmas [iff del] = not_None_eq
+
+theorem exec_pres_type:
+  "wf_prog wf_mb S \<Longrightarrow> 
+  pres_type (exec S maxs rT et bs) (size bs) (states S maxs maxr)"
+  apply (unfold exec_def JVM_states_unfold)
+  apply (rule pres_type_lift)
+  apply clarify
+  apply (case_tac s)
+   apply simp
+   apply (drule effNone)
+   apply simp  
+  apply (simp add: eff_def xcpt_eff_def norm_eff_def)
+  apply (case_tac "bs!p")
+
+  apply (clarsimp simp add: not_Err_eq)
+  apply (drule listE_nth_in, assumption)
+  apply fastsimp
+
+  apply (fastsimp simp add: not_None_eq)
+
+  apply (fastsimp simp add: not_None_eq typeof_empty_is_type)
+
+  apply clarsimp
+  apply (erule disjE)
+   apply fastsimp
+  apply clarsimp
+  apply (rule_tac x="1" in exI)
+  apply fastsimp
+
+  apply clarsimp
+  apply (erule disjE)
+   apply (fastsimp dest: field_fields fields_is_type)
+  apply (simp add: match_some_entry split: split_if_asm)
+  apply (rule_tac x=1 in exI)
+  apply fastsimp
+
+  apply clarsimp
+  apply (erule disjE)
+   apply fastsimp
+  apply (simp add: match_some_entry split: split_if_asm)
+  apply (rule_tac x=1 in exI)
+  apply fastsimp
+
+  apply clarsimp
+  apply (erule disjE)
+   apply fastsimp
+  apply clarsimp
+  apply (rule_tac x=1 in exI)
+  apply fastsimp
+
+  defer 
+
+  apply fastsimp
+  apply fastsimp
+
+  apply clarsimp
+  apply (rule_tac x="n'+2" in exI)  
+  apply simp
+  apply (drule listE_length)+
+  apply fastsimp
+
+  apply clarsimp
+  apply (rule_tac x="Suc (Suc (Suc (length ST)))" in exI)  
+  apply simp
+  apply (drule listE_length)+
+  apply fastsimp
+
+  apply clarsimp
+  apply (rule_tac x="Suc (Suc (Suc (Suc (length ST))))" in exI)  
+  apply simp
+  apply (drule listE_length)+
+  apply fastsimp
+
+  apply fastsimp
+  apply fastsimp
+  apply fastsimp
+  apply fastsimp
+
+  apply clarsimp
+  apply (erule disjE)
+   apply fastsimp
+  apply clarsimp
+  apply (rule_tac x=1 in exI)
+  apply fastsimp
+  
+  apply (erule disjE)
+   apply (clarsimp simp add: Un_subset_iff)  
+   apply (drule method_wf_mdecl, assumption+)
+   apply (clarsimp simp add: wf_mdecl_def wf_mhead_def)
+   apply fastsimp
+  apply clarsimp
+  apply (rule_tac x=1 in exI)
+  apply fastsimp
+  done
+
+lemmas [iff] = not_None_eq
+
+lemma sup_state_opt_unfold:
+  "sup_state_opt G \<equiv> Opt.le (Product.le (Listn.le (subtype G)) (Listn.le (Err.le (subtype G))))"
+  by (simp add: sup_state_opt_def sup_state_def sup_loc_def sup_ty_opt_def)
+
+
+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 list_appendI:
+  "\<lbrakk>a \<in> list x A; b \<in> list y A\<rbrakk> \<Longrightarrow> a @ b \<in> list (x+y) A"
+  apply (unfold list_def)
+  apply (simp (no_asm))
+  apply blast
+  done
+
+lemma list_map [simp]:
+  "(map f xs \<in> list (length xs) A) = (f ` set xs \<subseteq> A)"
+  apply (unfold list_def)
+  apply simp
+  done
+
+lemma [iff]:
+  "(OK ` A \<subseteq> err B) = (A \<subseteq> B)"
+  apply (unfold err_def)
+  apply blast
+  done
+
+lemma [intro]:
+  "x \<in> A \<Longrightarrow> replicate n x \<in> list n A"
+  by (induct n, auto)
+
+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)
+    apply simp
+   apply simp
+   apply (simp add: lesub_def)
+   apply (case_tac s)
+    apply simp
+   apply (simp del: split_paired_All split_paired_Ex)
+   apply (elim exE conjE)
+   apply simp
+   apply (drule eff'_mono, assumption)
+   apply assumption
+  apply (simp add: xcpt_eff_def)
+  apply (rule le_listI)
+    apply simp
+  apply simp
+  apply (simp add: lesub_def)
+  apply (case_tac s)
+   apply simp
+  apply simp
+  apply (case_tac t)
+   apply simp
+  apply (clarsimp simp add: sup_state_conv)
+  done
+
+lemma order_sup_state_opt:
+  "wf_prog wf_mb G \<Longrightarrow> order (sup_state_opt G)"
+  by (unfold sup_state_opt_unfold) (blast dest: acyclic_subcls1 order_widen)
+
+theorem exec_mono:
+  "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 app_mono)
+   apply assumption
+  apply clarify
+  apply (rule eff_mono)
+  apply assumption+
+  done
+
+theorem semilat_JVM_slI:
+  "wf_prog wf_mb G \<Longrightarrow> semilat (JVMType.sl G maxs maxr)"
+  apply (unfold JVMType.sl_def stk_esl_def reg_sl_def)
+  apply (rule semilat_opt)
+  apply (rule err_semilat_Product_esl)
+  apply (rule err_semilat_upto_esl)
+  apply (rule err_semilat_JType_esl, assumption+)
+  apply (rule err_semilat_eslI)
+  apply (rule Listn_sl)
+  apply (rule err_semilat_JType_esl, assumption+)
+  done
+
+lemma sl_triple_conv:
+  "JVMType.sl G maxs maxr == 
+  (states G maxs maxr, JVMType.le G maxs maxr, JVMType.sup G maxs maxr)"
+  by (simp (no_asm) add: states_def JVMType.le_def JVMType.sup_def)
+
+
+lemma map_id [rule_format]:
+  "(\<forall>n < length xs. f (g (xs!n)) = xs!n) \<longrightarrow> map f (map g xs) = xs"
+  by (induct xs, auto)
+
+
+lemma is_type_pTs:
+  "\<lbrakk> wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; ((mn,pTs),rT,code) \<in> set mdecls \<rbrakk>
+  \<Longrightarrow> set pTs \<subseteq> types G"
+proof 
+  assume "wf_prog wf_mb G" 
+         "(C,S,fs,mdecls) \<in> set G"
+         "((mn,pTs),rT,code) \<in> set mdecls"
+  hence "wf_mdecl wf_mb G C ((mn,pTs),rT,code)"
+    by (unfold wf_prog_def wf_cdecl_def) auto  
+  hence "\<forall>t \<in> set pTs. is_type G t" 
+    by (unfold wf_mdecl_def wf_mhead_def) auto
+  moreover
+  fix t assume "t \<in> set pTs"
+  ultimately
+  have "is_type G t" by blast
+  thus "t \<in> types G" ..
+qed
+
+
+lemma jvm_prog_lift:  
+  assumes wf: 
+  "wf_prog (\<lambda>G C bd. P G C bd) G"
+
+  assumes rule:
+  "\<And>wf_mb C mn pTs C rT maxs maxl b et bd.
+   wf_prog wf_mb G \<Longrightarrow>
+   method (G,C) (mn,pTs) = Some (C,rT,maxs,maxl,b,et) \<Longrightarrow>
+   is_class G C \<Longrightarrow>
+   set pTs \<subseteq> types G \<Longrightarrow>
+   bd = ((mn,pTs),rT,maxs,maxl,b,et) \<Longrightarrow>
+   P G C bd \<Longrightarrow>
+   Q G C bd"
+ 
+  shows 
+  "wf_prog (\<lambda>G C bd. Q G C bd) G"
+proof -
+  from wf show ?thesis
+    apply (unfold wf_prog_def wf_cdecl_def)
+    apply clarsimp
+    apply (drule bspec, assumption)
+    apply (unfold wf_mdecl_def)
+    apply clarsimp
+    apply (drule bspec, assumption)
+    apply clarsimp
+    apply (frule methd [OF wf], assumption+)
+    apply (frule is_type_pTs [OF wf], assumption+)
+    apply clarify
+    apply (drule rule [OF wf], assumption+)
+    apply (rule refl)
+    apply assumption+
+    done
+qed
+
+end
diff -r 45be08fbdcff -r 6f0928a942d1 src/HOL/MicroJava/BV/Typing_Framework_err.thy
--- a/src/HOL/MicroJava/BV/Typing_Framework_err.thy	Wed Jun 19 11:48:01 2002 +0200
+++ b/src/HOL/MicroJava/BV/Typing_Framework_err.thy	Wed Jun 19 12:39:41 2002 +0200
@@ -5,7 +5,7 @@
 
 *)
 
-header {* \isaheader{Static and Dynamic Welltyping} *}
+header {* \isaheader{Lifting the Typing Framework to err, app, and eff} *}
 
 theory Typing_Framework_err = Typing_Framework + SemilatAlg:
 
@@ -18,22 +18,26 @@
 "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 \<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(]"
 
-
 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"
 
+app_mono :: "'s ord \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool"
+"app_mono r app n A \<equiv>
+ \<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> app p t \<longrightarrow> app p s"
+
+
 lemmas err_step_defs = err_step_def map_snd_def error_def
 
+
 lemma bounded_err_stepD:
   "bounded (err_step n app step) n \<Longrightarrow> 
   p < n \<Longrightarrow>  app p a \<Longrightarrow> (q,b) \<in> set (step p a) \<Longrightarrow> 
@@ -68,6 +72,100 @@
 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 le_list_map_OK [simp]:
+  "\<And>b. map OK a <=[Err.le r] map OK b = (a <=[r] b)"
+  apply (induct a)
+   apply simp
+  apply simp
+  apply (case_tac b)
+   apply simp
+  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> 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 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 simp
+apply (case_tac t)
+ apply simp
+ apply clarify
+ apply (simp add: lesubstep_type_def error_def)
+ apply clarify
+ apply (drule in_map_sndD)
+ apply clarify
+ apply (drule bounded_err_stepD, 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 (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: lesubstep_type_def error_def)
+apply clarify
+apply (drule in_map_sndD)
+apply clarify
+apply (drule bounded_err_stepD, assumption+)
+apply (rule exI [of _ Err])
+apply simp
+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 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
+ apply (drule in_errorD)
+ apply simp
+apply (simp add: map_snd_def split: split_if_asm)
+ apply fast
+apply (drule in_errorD)
+apply simp
+done
+
+
+
 text {*
   There used to be a condition here that each instruction must have a
   successor. This is not needed any more, because the definition of
@@ -158,3 +256,4 @@
 qed
 
 end
+