# Theory Typing_Framework_JVM

Up to index of Isabelle/HOL/MicroJava

theory Typing_Framework_JVM
imports Typing_Framework_err JVMType EffectMono BVSpec
begin

    (*  Title:      HOL/MicroJava/BV/JVM.thy
        ID:         $Id: Typing_Framework_JVM.thy,v 1.5 2005/08/17 09:44:10 nipkow Exp $
        Author:     Tobias Nipkow, Gerwin Klein
        Copyright   2000 TUM
    *)

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

    theory Typing_Framework_JVM imports Typing_Framework_err JVMType EffectMono BVSpec begin

    constdefs
      exec :: "jvm_prog => nat => ty => exception_table => instr list => state step_type"
      "exec G maxs rT et bs ==
      err_step (size bs) (λpc. app (bs!pc) G maxs rT pc et) (λpc. eff (bs!pc) G pc et)"

    constdefs
      opt_states :: "'c prog => nat => nat => (ty list × ty err list) option set"
      "opt_states G maxs maxr ≡ opt (\<Union>{list n (types G) |n. n ≤ maxs} × list maxr (err (types G)))"

    section {*  Executability of @{term check_bounded} *}
    consts
      list_all'_rec :: "('a => nat => bool) => nat => 'a list => bool"
    primrec
      "list_all'_rec P n []     = True"
      "list_all'_rec P n (x#xs) = (P x n ∧ list_all'_rec P (Suc n) xs)"

    constdefs
      list_all' :: "('a => nat => bool) => 'a list => bool"
      "list_all' P xs ≡ list_all'_rec P 0 xs"

    lemma list_all'_rec:
      "!!n. list_all'_rec P n xs = (∀p < size xs. P (xs!p) (p+n))"
      apply (induct xs)
      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 (λe. fst (snd (snd e)) < length ins) et)"
      by (simp add: list_all_iff check_bounded_def)

    section {* Connecting JVM and Framework *}

    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 simp add: not_Err_eq)
      apply (drule listE_nth_in, assumption)
      apply fastsimp

      apply (fastsimp simp add: not_None_eq)

      apply (fastsimp simp add: not_None_eq typeof_empty_is_type)

      apply clarsimp
      apply (erule disjE)
       apply fastsimp
      apply clarsimp
      apply (rule_tac x="1" in exI)
      apply fastsimp

      apply clarsimp
      apply (erule disjE)
       apply (fastsimp dest: field_fields fields_is_type)
      apply (simp add: match_some_entry split: split_if_asm)
      apply (rule_tac x=1 in exI)
      apply fastsimp

      apply clarsimp
      apply (erule disjE)
       apply fastsimp
      apply (simp add: match_some_entry split: split_if_asm)
      apply (rule_tac x=1 in exI)
      apply fastsimp

      apply clarsimp
      apply (erule disjE)
       apply fastsimp
      apply clarsimp
      apply (rule_tac x=1 in exI)
      apply fastsimp

      defer

      apply fastsimp
      apply fastsimp

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

      apply clarsimp
      apply (erule disjE)
       apply fastsimp
      apply clarsimp
      apply (rule_tac x=1 in exI)
      apply fastsimp

      apply (erule disjE)
       apply (clarsimp simp add: Un_subset_iff)
       apply (drule method_wf_mdecl, assumption+)
       apply (clarsimp simp add: wf_mdecl_def wf_mhead_def)
       apply fastsimp
      apply clarsimp
      apply (rule_tac x=1 in exI)
      apply fastsimp
      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 (op =) 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|]
      ==> eff (bs!p) G p et s <=|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 map_id [rule_format]:
      "(∀n < length xs. f (g (xs!n)) = xs!n) --> map f (map g xs) = xs"
      by (induct xs, auto)

    lemma is_type_pTs:
      "[| wf_prog wf_mb G; (C,S,fs,mdecls) ∈ set G; ((mn,pTs),rT,code) ∈ set mdecls |]
      ==> set pTs ⊆ 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 ==>
       method (G,C) (mn,pTs) = Some (C,rT,maxs,maxl,b,et) ==>
       is_class G C ==>
       set pTs ⊆ types G ==>
       bd = ((mn,pTs),rT,maxs,maxl,b,et) ==>
       P G C bd ==>
       Q G C bd"

      shows
      "wf_prog (λG C bd. Q G C bd) G"
    proof -
      from wf show ?thesis
        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 refl)
        apply assumption+
        done
    qed

    end

## Executability of @{term check_bounded}

lemma list_all'_rec:

      list_all'_rec P n xs = (∀p<length xs. P (xs ! p) (p + n))

lemma list_all':

      list_all' P xs = (∀n<length xs. P (xs ! n) n)

lemma

      check_bounded ins et =
      (list_all' (%i pc. list_all (%pc'. pc' < length ins) (succs i pc)) ins ∧
       list_all (%e. fst (snd (snd e)) < length ins) et)

## Connecting JVM and Framework

lemma check_bounded_is_bounded:

      check_bounded ins et ==> bounded (%pc. eff (ins ! pc) G pc et) (length ins)

lemma special_ex_swap_lemma:

      (∃X. (∃n. X = A n ∧ P n) ∧ Q X) = (∃n. Q (A n) ∧ P n)

lemmas

      (x ≠ None) = (∃y. x = Some y)

lemmas

      (x ≠ None) = (∃y. x = Some y)

theorem exec_pres_type:

      wf_prog wf_mb S
      ==> pres_type (exec S maxs rT et bs) (length bs) (states S maxs maxr)

lemmas

      (x ≠ None) = (∃y. x = Some y)

lemmas

      (x ≠ None) = (∃y. x = Some y)

lemma sup_state_opt_unfold:

      sup_state_opt G ==
      Opt.le (Product.le (Listn.le (subtype G)) (Listn.le (Err.le (subtype G))))

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)

lemma list_appendI:

      [| a ∈ list x A; b ∈ list y A |] ==> a @ b ∈ list (x + y) A

lemma list_map:

      (map f xs ∈ list (length xs) A) = (f ` set xs ⊆ A)

lemma

      (OK ` A ⊆ err B) = (A ⊆ B)

lemma

      x ∈ A ==> replicate n x ∈ list n A

lemma lesubstep_type_simple:

      a <=[Product.le op = r] b ==> a <=|r| b

lemma eff_mono:

      [| p < length bs; s <=_(sup_state_opt G) t; app (bs ! p) G maxs rT pc et t |]
      ==> eff (bs ! p) G p et s <=|sup_state_opt G| eff (bs ! p) G p et t

lemma order_sup_state_opt:

      ws_prog G ==> order (sup_state_opt G)

theorem exec_mono:

      [| ws_prog G; bounded (exec G maxs rT et bs) (length bs) |]
      ==> SemilatAlg.mono (JVMType.le G maxs maxr) (exec G maxs rT et bs) (length bs)
           (states G maxs maxr)

theorem semilat_JVM_slI:

      ws_prog G ==> semilat (JVMType.sl G maxs maxr)

lemma sl_triple_conv:

      JVMType.sl G maxs maxr ==
      (states G maxs maxr, JVMType.le G maxs maxr, JVMType.sup G maxs maxr)

lemma map_id:

      (!!n. n < length xs ==> f (g (xs ! n)) = xs ! n) ==> map f (map g xs) = xs

lemma is_type_pTs:

      [| wf_prog wf_mb G; (C, S, fs, mdecls) ∈ set G;
         ((mn, pTs), rT, code) ∈ set mdecls |]
      ==> set pTs ⊆ types G

lemma jvm_prog_lift:

      [| wf_prog P G;
         !!wf_mb C mn pTs Ca rT maxs maxl b et bd.
            [| wf_prog wf_mb G;
               method (G, Ca) (mn, pTs) = Some (Ca, rT, maxs, maxl, b, et);
               is_class G Ca; set pTs ⊆ types G;
               bd = ((mn, pTs), rT, maxs, maxl, b, et); P G Ca bd |]
            ==> Q G Ca bd |]
      ==> wf_prog Q G