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