Theory TF_JVM

(*  Title:      JinjaThreads/BV/TF_JVM.thy
    Author:     Tobias Nipkow, Gerwin Klein, Andreas Lochbihler
*)

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

theory TF_JVM
imports "../../Jinja/DFA/Typing_Framework_err" EffectMono BVSpec
begin

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 ⊆ is_type 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 (is_type P) ∧ n ≤ mxs) = (is_class P C ∧ 0 < mxs)"
  by(auto)(auto simp add: mem_def)

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]

lemma [simp]: "x ∈ is_type P <-> is_type P x"
by(simp add: mem_def)

lemma (in start_context) [simp, intro!]: "is_class P Throwable"
apply(rule converse_subcls_is_class[OF wf])
 apply(rule xcpt_subcls_Throwable[OF _ wf])
 prefer 2
 apply(rule is_class_xcpt[OF _ wf])
apply(fastsimp simp add: sys_xcpts_def)+
done

declare option.splits[split del]
declare option.case_cong[cong]

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 split: option.splits)
  apply (frule listE_nth_in, assumption)
  apply(fastsimp split: option.splits)

  -- Store
  apply clarsimp
  apply(erule disjE)
   apply clarsimp
  apply(fastsimp split: option.splits)

  -- Push
  apply(fastsimp simp add: typeof_lit_is_type split: option.splits)

  -- New
  apply (clarsimp)
  apply (erule disjE)
   apply clarsimp
  apply (clarsimp)
  apply(rule conjI)
   apply(force split: option.splits)
  apply fastsimp

  -- NewArray
  apply clarsimp
  apply (erule disjE)
   apply clarsimp
  apply (clarsimp)
  apply (erule allE)+
  apply(erule impE, blast)
  apply(erule impE, blast)
  apply(force split: option.splits)

  -- ALoad
  apply(clarsimp split: split_if_asm)
   apply(rule conjI)
    apply(fastsimp split: option.splits)
   apply(erule allE)+
   apply(erule impE, blast)
   apply(erule impE, blast)
   apply arith
  apply(erule disjE)
   apply(fastsimp)
  apply(clarsimp)
  apply(rule conjI)
   apply(fastsimp split: option.splits)
  apply(erule allE)+
  apply(erule impE, blast)
  apply(erule impE, blast)
  apply arith

  -- AStore
  apply(clarsimp split: split_if_asm)
   apply(rule conjI)
    apply(fastsimp split: option.splits)
   apply(erule allE)+
   apply(erule impE, blast)
   apply(erule impE, blast)
   apply arith
  apply(erule disjE)
   apply(fastsimp)
  apply clarsimp
  apply(rule conjI)
   apply(fastsimp split: option.splits)
  apply(erule allE)+
  apply(erule impE, blast)
  apply(erule impE, blast)
  apply arith

  -- ALength
  apply(clarsimp split: split_if_asm)
   apply(rule conjI)
    apply(fastsimp split: option.splits)
   apply(erule allE)+
   apply(erule impE, blast)
   apply(erule impE, blast)
   apply arith
  apply(erule disjE)
   apply(fastsimp)
  apply clarsimp
  apply(rule conjI)
   apply(fastsimp split: option.splits)
  apply(erule allE)+
  apply(erule impE, blast)
  apply(erule impE, blast)
  apply arith


  -- Getfield
  apply(clarsimp)
  apply(erule disjE)
   apply(fastsimp dest: sees_field_is_type)
  apply clarsimp
  apply(rule conjI)
   apply(fastsimp split: option.splits)
  apply fastsimp

  -- Putfield
  apply(clarsimp)
  apply(erule disjE)
   apply(fastsimp)
  apply clarsimp
  apply(rule conjI)
   apply(fastsimp split: option.splits)
  apply fastsimp

  -- Checkcast
  apply(clarsimp)
  apply(erule disjE)
   apply(fastsimp)
  apply clarsimp
  apply(rule conjI)
   apply(fastsimp split: option.splits)
  apply fastsimp

  defer 
  
  -- Return
  apply(fastsimp split: option.splits)

  -- Pop
  apply(clarsimp)
  apply(erule disjE)
   apply(fastsimp)
  apply clarsimp
  apply(rule conjI)
   apply(fastsimp split: option.splits)
  apply fastsimp

  -- BinOpInstr
  apply(clarsimp)
  apply(erule disjE)
   apply(fastsimp intro: WTrt_binop_is_type)
  apply clarsimp
  apply(rule conjI)
   apply(fastsimp split: option.splits)
  apply fastsimp
  
  -- Goto
  apply(fastsimp split: option.splits)

  -- IfFalse
  apply(clarsimp)
  apply(erule disjE)
   apply(fastsimp)
  apply(erule disjE)
   apply fastsimp
  apply clarsimp
  apply(rule conjI)
   apply(fastsimp split: option.splits)
  apply fastsimp

  -- ThrowExc
  apply(clarsimp)
  apply(rule conjI)
   apply(erule allE)+
   apply(erule impE, blast)
   apply(erule impE, blast)
   apply(clarsimp split: option.splits)
  apply fastsimp

  -- MEnter
  apply(clarsimp)
  apply(erule disjE)
   apply(fastsimp)
  apply clarsimp
  apply(rule conjI)
   apply(fastsimp split: option.splits)
  apply fastsimp

  -- MExit
  apply(clarsimp)
  apply(erule disjE)
   apply(fastsimp)
  apply clarsimp
  apply(rule conjI)
   apply(fastsimp split: option.splits)
  apply fastsimp

  -- Invoke
  apply(rename_tac the_s M n)
  apply (clarsimp split: split_if_asm)
    apply(rule conjI)
     apply(fastsimp split: option.splits)
    apply fastsimp
   apply (erule disjE)
    apply(clarsimp simp add: external_WT_The_conv)
    apply(rule conjI)
     apply(erule in_listE)+
     apply(erule WT_external_is_type)
      apply simp
      apply(drule_tac c="a!n" in subsetD, simp)
      apply simp
     apply simp
     apply(blast intro: set_take_subset subset_trans del: subsetI)
    apply simp
   apply clarsimp
   apply(rule conjI)
    apply(fastsimp split: option.splits)
   apply fastsimp
  apply clarsimp
  apply(erule disjE)
   apply clarsimp
   apply(rule conjI)
    apply(drule (1) sees_wf_mdecl)
    apply(clarsimp simp add: wf_mdecl_def)
   apply(arith)
  apply(clarsimp)
  apply(erule allE)+
  apply(rotate_tac -2)
  apply(erule impE, blast)
  apply(erule impE, blast)
  apply(clarsimp split: option.splits)
  done
(*>*)

declare option.weak_case_cong[cong]
declare option.splits[split]

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 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