Quelle  TF_JVM.thy

(*  Title:      HOL/MicroJava/BV/JVM.thy

    Author:     Tobias Nipkow, Gerwin Klein
    Copyright   2000 TUM
*)

section ‹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₀ and n
  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₀"
  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"

  defines [simp]: "n ≡ size is"

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₀ Err)"
  defines [simp]:
  "start ≡ OK first # replicate (size is - 1) (OK None)"

subsection ‹Connecting JVM and Framework›
lemma (in start_context) semi: "semilat (A, r, f)"
  using semilat_JVM[OF wf]
  by (auto simp: JVM_SemiType.le_def JVM_SemiType.sup_def states_def)

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_nlists [iff]:
  "(∃n. ST ∈ nlists n A ∧ n ≤ mxs) = (set ST ⊆ A ∧ size ST ≤ mxs)"
  by (unfold nlists_def) auto

lemma singleton_nlists: 
  "(∃n. [Class C] ∈ nlists 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_nlistsE:
  "[ xs ∈ nlists n A; [size xs = n; set xs ⊆ A] ==> P ] ==> P"
  by (unfold nlists_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 nlistsE_nth_in, assumption)
  apply fastforce

  ― ‹Store›
  apply fastforce

  ― ‹Push›
  apply (fastforce simp add: typeof_lit_is_type)

  ― ‹New›
  apply clarsimp apply fastforce

  ― ‹Getfield›
  apply clarsimp apply (fastforce dest: sees_field_is_type)

  ― ‹Putfield›
  apply clarsimp apply fastforce

  ― ‹Checkcast›
  apply clarsimp apply fastforce

  defer 
  
  ― ‹Return›
  apply fastforce

  ― ‹Pop›
  apply fastforce

  ― ‹IAdd›
  apply fastforce
  
  ― ‹Goto›
  apply fastforce

  ― ‹CmpEq›
  apply fastforce

  ― ‹IfFalse›
  apply fastforce

  ― ‹Throw›
 apply clarsimp  apply fastforce

  ― ‹Invoke›
  apply (clarsimp split!: if_splits)
   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 [⊑_{.le (=) r}] ys ==> set xs {⊑} set ys"
(*<*)
  apply (simp add: lesubstep_type_def set_conv_nth)
  by (metis (full_types, opaque_lifting) le_listD le_prod_Pair_conv lesub_def
      surj_pair)
(*>*)

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 ⊑ _P t; app pc t]
  ==> set (eff pc s) {⊑ _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)
  using succs_mono eff_{i_mono}
  by (fastforce simp: Effect.app_def iff del: sup_state_conv)
(*>*)

lemma (in JVM_sl) bounded_step: "bounded step (size is)"
(*<*)
  by (auto simp add: error_def map_snd_def bounded_def err_step_def Effect.app_def Effect.eff_def split: err.splits option.splits)
(*>*)

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   ―‹ order_sup_state_opt' ›
    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!: nlists_appendI simp add: JVM_states_unfold)


lemma (in JVM_sl) wt_method_def2:
  "wt_method P C' Ts T_r mxs mxl₀ is xt τs =
  (is ≠ [] ∧
   size τs = size is ∧
   OK ` set τs ⊆ states P mxs mxl ∧
   wt_start P C' Ts mxl₀ τs ∧
   wt_app_eff (sup_state_opt P) app eff τs)"
(*<*)
  by (auto simp: wt_method_def wt_app_eff_def wt_instr_def lesub_def check_types_def)
(*>*)


end