(* Title: HOL/MicroJava/BV/Typing_Framework_JVM.thy
Author: Tobias Nipkow, Gerwin Klein
Copyright 2000 TUM
*)
section \<open>The Typing Framework for the JVM \label{sec:JVM}\<close>
theory Typing_Framework_JVM
imports "../DFA/Abstract_BV" JVMType EffectMono BVSpec
begin
definition exec :: "jvm_prog \ nat \ ty \ exception_table \ instr list \ JVMType.state step_type" where
"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)"
definition opt_states :: "'c prog \ nat \ nat \ (ty list \ ty err list) option set" where
"opt_states G maxs maxr \ opt (\{list n (types G) |n. n \ maxs} \ list maxr (err (types G)))"
subsection \<open>Executability of \<^term>\<open>check_bounded\<close>\<close>
primrec list_all'_rec :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> bool"
where
"list_all'_rec P n [] = True"
| "list_all'_rec P n (x#xs) = (P x n \ list_all'_rec P (Suc n) xs)"
definition list_all' :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
"list_all' P xs \ list_all'_rec P 0 xs"
lemma list_all'_rec:
"list_all'_rec P n xs = (\p < size xs. P (xs!p) (p+n))"
apply (induct xs arbitrary: n)
apply auto
apply (case_tac p)
apply auto
done
lemma list_all' [iff]:
"list_all' P xs = (\n < size xs. P (xs!n) n)"
by (unfold list_all'_def) (simp add: list_all'_rec)
lemma [code]:
"check_bounded ins et =
(list_all' (\i pc. list_all (\pc'. pc' < length ins) (succs i pc)) ins \
list_all (\<lambda>e. fst (snd (snd e)) < length ins) et)"
by (simp add: list_all_iff check_bounded_def)
subsection \<open>Connecting JVM and Framework\<close>
lemma check_bounded_is_bounded:
"check_bounded ins et \ bounded (\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 \
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
apply (drule listE_nth_in, assumption)
apply fastforce
apply (fastforce simp add: not_None_eq)
apply (fastforce simp add: not_None_eq typeof_empty_is_type)
apply clarsimp
apply (erule disjE)
apply fastforce
apply clarsimp
apply (rule_tac x="1" in exI)
apply fastforce
apply clarsimp
apply (erule disjE)
apply (fastforce dest: field_fields fields_is_type)
apply (simp add: match_some_entry image_iff)
apply (rule_tac x=1 in exI)
apply fastforce
apply clarsimp
apply (erule disjE)
apply fastforce
apply (simp add: match_some_entry image_iff)
apply (rule_tac x=1 in exI)
apply fastforce
apply clarsimp
apply (erule disjE)
apply fastforce
apply clarsimp
apply (rule_tac x=1 in exI)
apply fastforce
defer
apply fastforce
apply fastforce
apply clarsimp
apply (rule_tac x="n'+2" in exI)
apply simp
apply clarsimp
apply (rule_tac x="Suc (Suc (Suc (length ST)))" in exI)
apply simp
apply clarsimp
apply (rule_tac x="Suc (Suc (Suc (Suc (length ST))))" in exI)
apply simp
apply fastforce
apply fastforce
apply fastforce
apply fastforce
apply clarsimp
apply (erule disjE)
apply fastforce
apply clarsimp
apply (rule_tac x=1 in exI)
apply fastforce
apply (erule disjE)
apply clarsimp
apply (drule method_wf_mdecl, assumption+)
apply (clarsimp simp add: wf_mdecl_def wf_mhead_def)
apply fastforce
apply clarsimp
apply (rule_tac x=1 in exI)
apply fastforce
done
lemmas [iff] = not_None_eq
lemma sup_state_opt_unfold:
"sup_state_opt G \ 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) (\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:
"\a \ list x A; b \ list y A\ \ a @ b \ list (x+y) A"
apply (unfold list_def)
apply (simp (no_asm))
apply blast
done
lemma list_map [simp]:
"(map f xs \ list (length xs) A) = (f ` set xs \ A)"
apply (unfold list_def)
apply simp
done
lemma [iff]:
"(OK ` A \ err B) = (A \ B)"
apply (unfold err_def)
apply blast
done
lemma [intro]:
"x \ A \ replicate n x \ list n A"
by (induct n, auto)
lemma lesubstep_type_simple:
"a <=[Product.le (=) r] b \ 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:
"\p < length bs; s <=_(sup_state_opt G) t; app (bs!p) G maxs rT pc et t\
\<Longrightarrow> eff (bs!p) G p et s \<le>|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:
"ws_prog G \ order (sup_state_opt G)"
by (unfold sup_state_opt_unfold) (blast dest: acyclic_subcls1 order_widen)
theorem exec_mono:
"ws_prog G \ bounded (exec G maxs rT et bs) (size bs) \
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:
"ws_prog G \ 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 is_type_pTs:
"\ wf_prog wf_mb G; (C,S,fs,mdecls) \ set G; ((mn,pTs),rT,code) \ set mdecls \
\<Longrightarrow> set pTs \<subseteq> types G"
proof
assume "wf_prog wf_mb G"
"(C,S,fs,mdecls) \ set G"
"((mn,pTs),rT,code) \ set mdecls"
hence "wf_mdecl wf_mb G C ((mn,pTs),rT,code)"
by (rule wf_prog_wf_mdecl)
hence "\t \ set pTs. is_type G t"
by (unfold wf_mdecl_def wf_mhead_def) auto
moreover
fix t assume "t \ set pTs"
ultimately
have "is_type G t" by blast
thus "t \ types G" ..
qed
lemma jvm_prog_lift:
assumes wf:
"wf_prog (\G C bd. P G C bd) G"
assumes rule:
"\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 (\G C bd. Q G C bd) G"
using wf
apply (unfold wf_prog_def wf_cdecl_def)
apply clarsimp
apply (drule bspec, assumption)
apply (unfold wf_cdecl_mdecl_def)
apply clarsimp
apply (drule bspec, assumption)
apply (frule methd [OF wf [THEN wf_prog_ws_prog]], assumption+)
apply (frule is_type_pTs [OF wf], assumption+)
apply clarify
apply (drule rule [OF wf], assumption+)
apply (rule HOL.refl)
apply assumption+
done
end
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
