Theory TF_JVM

Up to index of Isabelle/HOL/Jinja

theory TF_JVM = Typing_Framework_err + EffectMono + BVSpec: 
(*  Title:      HOL/MicroJava/BV/JVM.thy
    ID:         $Id: TF_JVM.html 1910 2004-05-19 04:46:04Z kleing $
    Author:     Tobias Nipkow, Gerwin Klein
    Copyright   2000 TUM
*)

header {* \isaheader{The Typing Framework for the JVM}\label{sec:JVM} *}

theory TF_JVM = Typing_Framework_err + EffectMono + BVSpec:

constdefs
  exec :: "jvm_prog => nat => ty => ex_table => instr list => tyi' err step_type"
  "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 mxl0
  fixes Ts :: "ty list" and "is" and xt and Tr

  fixes mxl and A and r and f and app and eff and step
  defines [simp]: "mxl ≡ 1+size Ts+mxl0"
  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 Tr 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 :: tyi' and start
  defines [simp]: 
  "first ≡ Some ([],OK (Class C) # map OK Ts @ replicate mxl0 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 Tr 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 fastsimp

  -- Store
  apply fastsimp

  -- Push
  apply (fastsimp simp add: typeof_lit_is_type)

  -- New
  apply clarsimp
  apply (erule disjE)
   apply clarsimp
  apply clarsimp
  apply (erule allE)+
  apply (erule impE, blast)
  apply (erule impE, blast)
  apply fastsimp

  -- Getfield
  apply (fastsimp dest: sees_field_is_type)

  -- Putfield
  apply fastsimp

  -- Checkcast
  apply fastsimp

  defer 
  
  -- Return
  apply fastsimp

  -- Pop
  apply fastsimp

  -- IAdd
  apply fastsimp
  
  -- Goto
  apply fastsimp

  -- CmpEq
  apply fastsimp

  -- IfFalse
  apply fastsimp

  -- Throw
  apply fastsimp

  -- Invoke
  apply (clarsimp split: split_if_asm)
   apply fastsimp
  apply (erule disjE)
   prefer 2
   apply fastsimp
  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 (rule list_all2_dropI)
   apply (simp add: fun_of_def)
  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 effi_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 Tr mxs mxl0 is xt τs =
  (is ≠ [] ∧ 
   size τs = size is ∧
   OK ` set τs ⊆ states P mxs mxl ∧
   wt_start P C' Ts mxl0 τ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

Connecting JVM and Framework

lemma step_def_exec: 

  err_step (length is) (%pc. app (is ! pc) P mxs Tr pc (length is) xt)
   (%pc. eff (is ! pc) P pc xt) ==
  exec P mxs Tr xt is

lemma special_ex_swap_lemma: 

  (EX X. (EX n. X = A n & P n) & Q X) = (EX n. Q (A n) & P n)

lemma ex_in_list: 

  (EX n. ST : list n A & n <= mxs) = (set ST <= A & length ST <= mxs)

lemma singleton_list: 

  (EX n. [Class C] : list n (types P) & n <= mxs) = (is_class P C & 0 < mxs)

lemma set_drop_subset: 

  set xs <= A ==> set (drop n xs) <= A

lemma Suc_minus_minus_le: 

  n < mxs ==> Suc (n - (n - b)) <= mxs

lemma in_listE: 

  [| xs : list n A; [| length xs = n; set xs <= A |] ==> P |] ==> P

theorem exec_pres_type: 

  start_context P Ts p C
  ==> pres_type
       (err_step (length is) (%pc. app (is ! pc) P mxs Tr pc (length is) xt)
         (%pc. eff (is ! pc) P pc xt))
       (length is) (states P mxs (1 + length Ts + mxl0))

lemma lesubstep_type_simple: 

  xs [<=Product.le op = r] ys ==> set xs {<=_r} set ys

lemma conjI2: 

  [| A; A ==> B |] ==> A & B

lemma eff_mono: 

  [| wf_prog p P; pc < length is; s <=_(sup_state_opt P) t;
     app (is ! pc) P mxs Tr pc (length is) xt t |]
  ==> set (eff (is ! pc) P pc xt s) 
      {<=_sup_state_opt P} set (eff (is ! pc) P pc xt t)

lemma bounded_step: 

  bounded
   (err_step (length is) (%pc. app (is ! pc) P mxs Tr pc (length is) xt)
     (%pc. eff (is ! pc) P pc xt))
   (length is)

theorem step_mono: 

  wf_prog wf_mb P
  ==> SemilatAlg.mono (JVM_SemiType.le P mxs (1 + length Ts + mxl0))
       (err_step (length is) (%pc. app (is ! pc) P mxs Tr pc (length is) xt)
         (%pc. eff (is ! pc) P pc xt))
       (length is) (states P mxs (1 + length Ts + mxl0))

lemma first_in_A: 

  start_context P Ts p C
  ==> OK ⌊([], OK (Class C) # map OK Ts @ replicate mxl0 Err)⌋
      : states P mxs (1 + length Ts + mxl0)

lemma wt_method_def2: 

  wt_method P C' Ts Tr mxs mxl0 is xt τs =
  (is ~= [] &
   length τs = length is &
   OK ` set τs <= states P mxs (1 + length Ts + mxl0) &
   wt_start P C' Ts mxl0 τs &
   wt_app_eff (sup_state_opt P) (%pc. app (is ! pc) P mxs Tr pc (length is) xt)
    (%pc. eff (is ! pc) P pc xt) τs)