--- 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