Up to index of Isabelle/HOL/jsr
theory Typing_Framework_JVM = Typing_Framework_err + JVMType + EffectMono + BVSpec:(* Title: HOL/MicroJava/BV/JVM.thy
ID: $Id: Typing_Framework_JVM.html,v 1.1 2002/11/28 14:17:20 kleing Exp $
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> cname \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> bool \<Rightarrow> exception_table \<Rightarrow> instr list \<Rightarrow>
state step_type"
"exec G C maxs rT ini et bs ==
err_step (size bs) (\<lambda>pc. app (bs!pc) G C pc maxs (size bs) rT ini et) (\<lambda>pc. eff (bs!pc) G pc et)"
locale (open) JVM_sl =
fixes wf_mb and G and C and mxs and mxl
fixes pTs :: "ty list" and mn and bs and et and rT
fixes mxr and A and r and app and eff and step
defines [simp]: "mxr \<equiv> 1+length pTs+mxl"
defines [simp]: "A \<equiv> states G mxs mxr (length bs)"
defines [simp]: "r \<equiv> JVMType.le"
defines [simp]: "app \<equiv> \<lambda>pc. Effect.app (bs!pc) G C pc mxs (size bs) rT (mn=init) et"
defines [simp]: "eff \<equiv> \<lambda>pc. Effect.eff (bs!pc) G pc et"
defines [simp]: "step \<equiv> exec G C mxs rT (mn=init) et bs"
locale (open) start_context = JVM_sl +
assumes wf: "wf_prog wf_mb G"
assumes C: "is_class G C"
assumes pTs: "Init ` set pTs \<subseteq> init_tys G (size bs)"
fixes this and first :: state_bool and start
defines [simp]:
"this \<equiv> OK (if mn=init \<and> C \<noteq> Object then PartInit C else Init (Class C))"
defines [simp]:
"first \<equiv> (([],this#(map (OK\<circ>Init) pTs)@(replicate mxl Err)), C=Object)"
defines [simp]:
"start \<equiv> OK {first}#(replicate (size bs - 1) (OK {}))"
section {* Connecting JVM and Framework *}
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
lemma replace_in_setI:
"\<And>n. ls \<in> list n A \<Longrightarrow> b \<in> A \<Longrightarrow> replace a b ls \<in> list n A"
by (induct ls) (auto simp add: replace_def)
lemma in_list_Ex [iff]:
"(\<exists>n. xs \<in> list n A \<and> P xs n) = (set xs \<subseteq> A \<and> P xs (length xs))"
apply (unfold list_def)
apply auto
done
lemma boundedRAI1:
"¬is_RA T \<Longrightarrow> boundedRA (n,T)"
apply (cases T)
apply auto
apply (case_tac prim_ty)
apply auto
done
lemma eff_pres_type:
"\<lbrakk>wf_prog wf_mb S; s \<subseteq> address_types S maxs maxr (length bs);
p < length bs; app (bs!p) S C p maxs (length bs) rT ini et s;
(a, b) \<in> set (eff (bs ! p) S p et s)\<rbrakk>
\<Longrightarrow> \<forall>x \<in> b. x \<in> address_types S maxs maxr (length bs)"
apply clarify
apply (unfold eff_def xcpt_eff_def norm_eff_def eff_bool_def)
apply (case_tac "bs!p")
-- load
apply (clarsimp simp add: not_Err_eq address_types_def)
apply (drule bspec, assumption)
apply (drule subsetD, assumption)
apply (rotate_tac -1)
apply clarsimp
apply (drule listE_nth_in, assumption)
apply fastsimp
-- store
apply (clarsimp simp add: address_types_def)
apply (drule bspec, assumption)
apply (drule subsetD, assumption)
apply fastsimp
-- litpush
apply (clarsimp simp add: address_types_def)
apply (drule bspec, assumption)
apply (drule subsetD, assumption)
apply clarsimp
apply (rotate_tac -3) -- "for n = length ab"
apply (fastsimp simp add: init_tys_def)
-- new
apply clarsimp
apply (erule disjE)
apply (clarsimp simp add: address_types_def)
apply (drule bspec, assumption)
apply (drule subsetD, assumption)
apply (fastsimp simp add: replace_in_setI init_tys_def)
apply (clarsimp simp add: address_types_def)
apply (drule bspec, assumption)
apply (drule subsetD, assumption)
apply clarsimp
apply (rule_tac x=1 in exI)
apply (fastsimp simp add: init_tys_def)
-- getfield
apply clarsimp
apply (erule disjE)
apply (clarsimp simp add: address_types_def)
apply (drule bspec, assumption)
apply (drule subsetD, assumption)
apply clarsimp
apply (rule_tac x="Suc n'" in exI)
apply (drule field_fields)
apply simp
apply (frule fields_is_type, assumption, assumption)
apply (frule fields_no_RA, assumption, assumption)
apply (simp (no_asm) add: init_tys_def)
apply simp
apply (rule boundedRAI1, assumption)
apply (clarsimp simp add: address_types_def)
apply (drule bspec, assumption)
apply (drule subsetD, assumption)
apply (clarsimp simp add: init_tys_def)
apply (simp add: match_some_entry split: split_if_asm)
apply (rule_tac x=1 in exI)
apply fastsimp
-- putfield
apply clarsimp
apply (erule disjE)
apply (clarsimp simp add: address_types_def)
apply (drule bspec, assumption)
apply (drule subsetD, assumption)
apply (clarsimp simp add: init_tys_def)
apply fastsimp
apply (clarsimp simp add: address_types_def)
apply (drule bspec, assumption)
apply (drule subsetD, assumption)
apply (clarsimp simp add: init_tys_def)
apply (simp add: match_some_entry split: split_if_asm)
apply (rule_tac x=1 in exI)
apply fastsimp
-- checkcast
apply clarsimp
apply (erule disjE)
apply (clarsimp simp add: address_types_def)
apply (drule bspec, assumption)
apply (drule subsetD, assumption)
apply (clarsimp simp add: init_tys_def)
apply fastsimp
apply (clarsimp simp add: address_types_def)
apply (drule bspec, assumption)
apply (drule subsetD, assumption)
apply (clarsimp simp add: init_tys_def)
apply (rule_tac x=1 in exI)
apply fastsimp
-- invoke
apply clarsimp
apply (erule disjE)
apply (clarsimp simp add: address_types_def)
apply (drule bspec, assumption)
apply (drule subsetD, assumption)
apply (clarsimp simp add: init_tys_def)
apply (drule method_wf_mdecl, assumption+)
apply (clarsimp simp add: wf_mdecl_def wf_mhead_def)
apply (rule in_list_Ex [THEN iffD2])
apply (simp add: boundedRAI1)
apply (clarsimp simp add: address_types_def)
apply (drule bspec, assumption)
apply (drule subsetD, assumption)
apply (clarsimp simp add: init_tys_def)
apply (rule_tac x=1 in exI)
apply fastsimp
-- "@{text invoke_special}"
apply clarsimp
apply (erule disjE)
apply (clarsimp simp add: address_types_def)
apply (drule bspec, assumption)
apply (drule subsetD, assumption)
apply (clarsimp simp add: init_tys_def)
apply (drule method_wf_mdecl, assumption+)
apply (clarsimp simp add: wf_mdecl_def wf_mhead_def)
apply (rule conjI)
apply (rule_tac x="Suc (length ST)" in exI)
apply (fastsimp intro: replace_in_setI subcls_is_class boundedRAI1)
apply (fastsimp intro: replace_in_setI subcls_is_class boundedRAI1)
apply (clarsimp simp add: address_types_def)
apply (drule bspec, assumption)
apply (drule subsetD, assumption)
apply (clarsimp simp add: init_tys_def)
apply (rule_tac x=1 in exI)
apply fastsimp
-- return
apply fastsimp
-- pop
apply (clarsimp simp add: address_types_def)
apply (drule bspec, assumption)
apply (drule subsetD, assumption)
apply (clarsimp simp add: init_tys_def)
apply fastsimp
-- dup
apply (clarsimp simp add: address_types_def)
apply (drule bspec, assumption)
apply (drule subsetD, assumption)
apply (clarsimp simp add: init_tys_def)
apply (rule_tac x="n'+2" in exI)
apply simp
-- "@{text dup_x1}"
apply (clarsimp simp add: address_types_def)
apply (drule bspec, assumption)
apply (drule subsetD, assumption)
apply (clarsimp simp add: init_tys_def)
apply (rule_tac x="Suc (Suc (Suc (length ST)))" in exI)
apply simp
-- "@{text dup_x2}"
apply (clarsimp simp add: address_types_def)
apply (drule bspec, assumption)
apply (drule subsetD, assumption)
apply (clarsimp simp add: init_tys_def)
apply (rule_tac x="Suc (Suc (Suc (Suc (length ST))))" in exI)
apply simp
-- swap
apply (clarsimp simp add: address_types_def)
apply (drule bspec, assumption)
apply (drule subsetD, assumption)
apply (clarsimp simp add: init_tys_def)
apply fastsimp
-- iadd
apply (clarsimp simp add: address_types_def)
apply (drule bspec, assumption)
apply (drule subsetD, assumption)
apply (clarsimp simp add: init_tys_def)
apply fastsimp
-- goto
apply fastsimp
-- icmpeq
apply (clarsimp simp add: address_types_def)
apply fastsimp
-- throw
apply (clarsimp simp add: address_types_def init_tys_def)
apply (drule bspec, assumption)
apply (drule subsetD, assumption)
apply clarsimp
apply (rule_tac x=1 in exI)
apply fastsimp
-- jsr
apply (clarsimp simp add: address_types_def)
apply (drule bspec, assumption)
apply (drule subsetD, assumption)
apply (clarsimp simp add: init_tys_def)
apply fastsimp
-- ret
apply fastsimp
done
lemmas [iff] = not_None_eq
lemma app_mono:
"app_mono (op \<subseteq>) (\<lambda>pc. app (bs!pc) G C pc maxs (size bs) rT ini et) (length bs) (Pow (address_types G mxs mxr mpc))"
apply (unfold app_mono_def lesub_def)
apply clarify
apply (drule in_address_types_finite)+
apply (blast intro: EffectMono.app_mono)
done
theorem exec_pres_type:
"wf_prog wf_mb S \<Longrightarrow>
pres_type (exec S C maxs rT ini et bs) (size bs) (states S maxs maxr (length bs))"
apply (unfold exec_def states_def)
apply (rule pres_type_lift)
apply clarify
apply (blast dest: eff_pres_type)
done
declare split_paired_All [simp del]
declare eff_defs [simp del]
lemma eff_mono:
"\<lbrakk>wf_prog wf_mb G; t \<subseteq> address_types G maxs maxr (length bs); p < length bs; s \<subseteq> t; app (bs!p) G C p maxs (size bs) rT ini et t\<rbrakk>
\<Longrightarrow> eff (bs ! p) G p et s <=|op \<subseteq>| eff (bs ! p) G p et t"
apply (unfold lesubstep_type_def lesub_def)
apply clarify
apply (frule in_address_types_finite)
apply (frule EffectMono.app_mono, assumption, assumption)
apply (frule subset_trans, assumption)
apply (drule eff_pres_type, assumption, assumption, assumption, assumption)
apply (frule finite_subset, assumption)
apply (unfold eff_def)
apply clarsimp
apply (erule disjE)
defer
apply (unfold xcpt_eff_def)
apply clarsimp
apply blast
apply clarsimp
apply (rule exI)
apply (rule conjI)
apply (rule disjI1)
apply (rule imageI)
apply (rule subsetD [OF succs_mono], assumption+)
apply (unfold norm_eff_def)
apply clarsimp
apply (rule conjI)
apply clarsimp
apply (simp add: set_SOME_lists finite_imageI)
apply (rule imageI)
apply clarsimp
apply (rule subsetD, assumption+)
apply clarsimp
apply (rule imageI)
apply (rule subsetD, assumption+)
done
lemma bounded_exec:
"bounded (exec G C maxs rT ini et bs) (size bs) (states G maxs maxr (size bs))"
apply (unfold bounded_def exec_def err_step_def app_def)
apply (auto simp add: error_def map_snd_def split: err.splits split_if_asm)
done
theorem exec_mono:
"wf_prog wf_mb G \<Longrightarrow>
mono JVMType.le (exec G C maxs rT ini et bs) (size bs) (states G maxs maxr (size bs))"
apply (insert bounded_exec [of G C maxs rT ini et bs maxr])
apply (unfold exec_def JVMType.le_def JVMType.states_def)
apply (rule mono_lift)
apply (unfold order_def lesub_def)
apply blast
apply (rule app_mono)
apply assumption
apply clarify
apply (rule eff_mono)
apply assumption+
done
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> Init`set pTs \<subseteq> init_tys G mpc"
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 \<and> ¬is_RA t"
by (unfold wf_mdecl_def wf_mhead_def) auto
moreover
fix t assume "t \<in> Init`set pTs"
then obtain t' where t': "t = Init t'" and "t' \<in> set pTs" by auto
ultimately
have "is_type G t' \<and> ¬is_RA t'" by blast
with t' show "t \<in> init_tys G mpc" by (auto simp add: init_tys_def boundedRAI1)
qed
lemma (in JVM_sl) wt_method_def2:
"wt_method G C mn pTs rT mxs mxl bs et phi =
(bs \<noteq> [] \<and>
length phi = length bs \<and>
check_types G mxs mxr (size bs) (map OK phi) \<and>
wt_start G C mn pTs mxl phi \<and>
wt_app_eff (op \<subseteq>) app eff phi)"
apply (unfold wt_method_def wt_app_eff_def wt_instr_def lesub_def)
apply rule
apply fastsimp
apply clarsimp
apply (rule conjI)
defer
apply fastsimp
apply (insert bounded_exec [of G C mxs rT "mn=init" et bs "Suc (length pTs + mxl)"])
apply (unfold exec_def bounded_def err_step_def)
apply (erule allE, erule impE, assumption)+
apply clarsimp
apply (drule_tac x = "OK (phi!pc)" in bspec)
apply (fastsimp simp add: check_types_def)
apply (fastsimp simp add: map_snd_def)
done
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>
Init`set pTs \<subseteq> init_tys G (length b) \<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
lemma special_ex_swap_lemma:
(EX X. (EX n. X = A n & P n) & Q X) = (EX n. Q (A n) & P n)
lemmas
(x ~= None) = (EX y. x = Some y)
lemma replace_in_setI:
[| ls : list n A; b : A |] ==> replace a b ls : list n A
lemma in_list_Ex:
(EX n. xs : list n A & P xs n) = (set xs <= A & P xs (length xs))
lemma boundedRAI1:
¬ is_RA T ==> boundedRA (n, T)
lemma eff_pres_type:
[| wf_prog wf_mb S; s <= address_types S maxs maxr (length bs); p < length bs;
app (bs ! p) S C p maxs (length bs) rT ini et s;
(a, b) : set (eff (bs ! p) S p et s) |]
==> ALL x:b. x : address_types S maxs maxr (length bs)
lemmas
(x ~= None) = (EX y. x = Some y)
lemma app_mono:
app_mono op <= (%pc. app (bs ! pc) G C pc maxs (length bs) rT ini et) (length bs) (Pow (address_types G mxs mxr mpc))
theorem exec_pres_type:
wf_prog wf_mb S
==> pres_type (Typing_Framework_JVM.exec S C maxs rT ini et bs) (length bs)
(states S maxs maxr (length bs))
lemma eff_mono:
[| wf_prog wf_mb G; t <= address_types G maxs maxr (length bs); p < length bs;
s <= t; app (bs ! p) G C p maxs (length bs) rT ini et t |]
==> eff (bs ! p) G p et s <=|op <=| eff (bs ! p) G p et t
lemma bounded_exec:
bounded (Typing_Framework_JVM.exec G C maxs rT ini et bs) (length bs) (states G maxs maxr (length bs))
theorem exec_mono:
wf_prog wf_mb G
==> SemilatAlg.mono JVMType.le (Typing_Framework_JVM.exec G C maxs rT ini et bs)
(length bs) (states G maxs maxr (length bs))
lemma map_id:
(!!n. n < length xs ==> f (g (xs ! n)) = xs ! n) ==> map f (map g xs) = xs
lemma is_type_pTs:
[| wf_prog wf_mb G; (C, S, fs, mdecls) : set G;
((mn, pTs), rT, code) : set mdecls |]
==> Init ` set pTs <= init_tys G mpc
lemma wt_method_def2:
wt_method G C mn pTs rT mxs mxl bs et phi =
(bs ~= [] &
length phi = length bs &
check_types G mxs (1 + length pTs + mxl) (length bs) (map OK phi) &
wt_start G C mn pTs mxl phi &
wt_app_eff op <= (%pc. app (bs ! pc) G C pc mxs (length bs) rT (mn = init) et)
(%pc. eff (bs ! pc) G pc et) phi)
lemma
[| wf_prog P G;
!!wf_mb C mn pTs Ca rT maxs maxl b et bd.
[| wf_prog wf_mb G;
method (G, Ca) (mn, pTs) = Some (Ca, rT, maxs, maxl, b, et);
is_class G Ca; Init ` set pTs <= init_tys G (length b);
bd = ((mn, pTs), rT, maxs, maxl, b, et); P G Ca bd |]
==> Q G Ca bd |]
==> wf_prog Q G