Up to index of Isabelle/HOL/Jinja
theory TF_JVM(* Title: HOL/MicroJava/BV/JVM.thy
Author: Tobias Nipkow, Gerwin Klein
Copyright 2000 TUM
*)
header {* \isaheader{The Typing Framework for the JVM}\label{sec:JVM} *}
theory TF_JVM
imports "../DFA/Typing_Framework_err" EffectMono BVSpec
begin
definition exec :: "jvm_prog => nat => ty => ex_table => instr list => ty⇣i' err step_type"
where
"exec G maxs rT et bs ≡
err_step (size bs) (λpc. app (bs!pc) G maxs rT pc (size bs) et)
(λpc. eff (bs!pc) G pc et)"
locale JVM_sl =
fixes P :: jvm_prog and mxs and mxl⇣0
fixes Ts :: "ty list" and "is" and xt and T⇣r
fixes mxl and A and r and f and app and eff and step
defines [simp]: "mxl ≡ 1+size Ts+mxl⇣0"
defines [simp]: "A ≡ states P mxs mxl"
defines [simp]: "r ≡ JVM_SemiType.le P mxs mxl"
defines [simp]: "f ≡ JVM_SemiType.sup P mxs mxl"
defines [simp]: "app ≡ λpc. Effect.app (is!pc) P mxs T⇣r pc (size is) xt"
defines [simp]: "eff ≡ λpc. Effect.eff (is!pc) P pc xt"
defines [simp]: "step ≡ err_step (size is) app eff"
locale start_context = JVM_sl +
fixes p and C
assumes wf: "wf_prog p P"
assumes C: "is_class P C"
assumes Ts: "set Ts ⊆ types P"
fixes first :: ty⇣i' and start
defines [simp]:
"first ≡ Some ([],OK (Class C) # map OK Ts @ replicate mxl⇣0 Err)"
defines [simp]:
"start ≡ OK first # replicate (size is - 1) (OK None)"
section {* Connecting JVM and Framework *}
lemma (in JVM_sl) step_def_exec: "step ≡ exec P mxs T⇣r xt is"
by (simp add: exec_def)
lemma special_ex_swap_lemma [iff]:
"(? X. (? n. X = A n & P n) & Q X) = (? n. Q(A n) & P n)"
by blast
lemma ex_in_list [iff]:
"(∃n. ST ∈ list n A ∧ n ≤ mxs) = (set ST ⊆ A ∧ size ST ≤ mxs)"
by (unfold list_def) auto
lemma singleton_list:
"(∃n. [Class C] ∈ list n (types P) ∧ n ≤ mxs) = (is_class P C ∧ 0 < mxs)"
by auto
lemma set_drop_subset:
"set xs ⊆ A ==> set (drop n xs) ⊆ A"
by (auto dest: in_set_dropD)
lemma Suc_minus_minus_le:
"n < mxs ==> Suc (n - (n - b)) ≤ mxs"
by arith
lemma in_listE:
"[| xs ∈ list n A; [|size xs = n; set xs ⊆ A|] ==> P |] ==> P"
by (unfold list_def) blast
declare is_relevant_entry_def [simp]
declare set_drop_subset [simp]
theorem (in start_context) exec_pres_type:
"pres_type step (size is) A"
(*<*)
apply (insert wf)
apply simp
apply (unfold JVM_states_unfold)
apply (rule pres_type_lift)
apply clarify
apply (rename_tac s pc pc' s')
apply (case_tac s)
apply simp
apply (drule effNone)
apply simp
apply (simp add: Effect.app_def xcpt_app_def Effect.eff_def
xcpt_eff_def norm_eff_def relevant_entries_def)
apply (case_tac "is!pc")
-- Load
apply clarsimp
apply (frule listE_nth_in, assumption)
apply fastforce
-- Store
apply fastforce
-- Push
apply (fastforce simp add: typeof_lit_is_type)
-- New
apply fastforce
-- Getfield
apply (fastforce dest: sees_field_is_type)
-- Putfield
apply fastforce
-- Checkcast
apply fastforce
defer
-- Return
apply fastforce
-- Pop
apply fastforce
-- IAdd
apply fastforce
-- Goto
apply fastforce
-- CmpEq
apply fastforce
-- IfFalse
apply fastforce
-- Throw
apply fastforce
-- Invoke
apply (clarsimp split: split_if_asm)
apply fastforce
apply (erule disjE)
prefer 2
apply fastforce
apply clarsimp
apply (rule conjI)
apply (drule (1) sees_wf_mdecl)
apply (clarsimp simp add: wf_mdecl_def)
apply arith
done
(*>*)
declare is_relevant_entry_def [simp del]
declare set_drop_subset [simp del]
lemma lesubstep_type_simple:
"xs [\<sqsubseteq>⇘Product.le (op =) r⇙] ys ==> set xs {\<sqsubseteq>⇘r⇙} set ys"
(*<*)
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
(*>*)
declare is_relevant_entry_def [simp del]
lemma conjI2: "[| A; A ==> B |] ==> A ∧ B" by blast
lemma (in JVM_sl) eff_mono:
"[|wf_prog p P; pc < length is; s \<sqsubseteq>⇘sup_state_opt P⇙ t; app pc t|]
==> set (eff pc s) {\<sqsubseteq>⇘sup_state_opt P⇙} set (eff pc t)"
(*<*)
apply simp
apply (unfold Effect.eff_def)
apply (cases t)
apply (simp add: lesub_def)
apply (rename_tac a)
apply (cases s)
apply simp
apply (rename_tac b)
apply simp
apply (rule lesubstep_union)
prefer 2
apply (rule lesubstep_type_simple)
apply (simp add: xcpt_eff_def)
apply (rule le_listI)
apply (simp add: split_beta)
apply (simp add: split_beta)
apply (simp add: lesub_def fun_of_def)
apply (case_tac a)
apply (case_tac b)
apply simp
apply (subgoal_tac "size ab = size aa")
prefer 2
apply (clarsimp simp add: list_all2_lengthD)
apply simp
apply (clarsimp simp add: norm_eff_def lesubstep_type_def lesub_def iff del: sup_state_conv)
apply (rule exI)
apply (rule conjI2)
apply (rule imageI)
apply (clarsimp simp add: Effect.app_def iff del: sup_state_conv)
apply (drule (2) succs_mono)
apply blast
apply simp
apply (erule eff⇣i_mono)
apply simp
apply assumption
apply clarsimp
apply clarsimp
done
(*>*)
lemma (in JVM_sl) bounded_step: "bounded step (size is)"
(*<*)
apply simp
apply (unfold bounded_def err_step_def Effect.app_def Effect.eff_def)
apply (auto simp add: error_def map_snd_def split: err.splits option.splits)
done
(*>*)
theorem (in JVM_sl) step_mono:
"wf_prog wf_mb P ==> mono r step (size is) A"
(*<*)
apply (simp add: JVM_le_Err_conv)
apply (insert bounded_step)
apply (unfold JVM_states_unfold)
apply (rule mono_lift)
apply blast
apply (unfold app_mono_def lesub_def)
apply clarsimp
apply (erule (2) app_mono)
apply simp
apply clarify
apply (drule eff_mono)
apply (auto simp add: lesub_def)
done
(*>*)
lemma (in start_context) first_in_A [iff]: "OK first ∈ A"
using Ts C by (force intro!: list_appendI simp add: JVM_states_unfold)
lemma (in JVM_sl) wt_method_def2:
"wt_method P C' Ts T⇣r mxs mxl⇣0 is xt τs =
(is ≠ [] ∧
size τs = size is ∧
OK ` set τs ⊆ states P mxs mxl ∧
wt_start P C' Ts mxl⇣0 τs ∧
wt_app_eff (sup_state_opt P) app eff τs)"
(*<*)
apply (unfold wt_method_def wt_app_eff_def wt_instr_def lesub_def check_types_def)
apply auto
done
(*>*)
end