src/HOL/MicroJava/BV/Typing_Framework_JVM.thy
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 17090 603f23d71ada
child 26289 9d2c375e242b
permissions -rw-r--r--
Name.uu, Name.aT;
     1 (*  Title:      HOL/MicroJava/BV/JVM.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow, Gerwin Klein
     4     Copyright   2000 TUM
     5 *)
     6 
     7 header {* \isaheader{The Typing Framework for the JVM}\label{sec:JVM} *}
     8 
     9 theory Typing_Framework_JVM imports Typing_Framework_err JVMType EffectMono BVSpec begin
    10 
    11 
    12 constdefs
    13   exec :: "jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> instr list \<Rightarrow> state step_type"
    14   "exec G maxs rT et bs == 
    15   err_step (size bs) (\<lambda>pc. app (bs!pc) G maxs rT pc et) (\<lambda>pc. eff (bs!pc) G pc et)"
    16 
    17 constdefs
    18   opt_states :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> (ty list \<times> ty err list) option set"
    19   "opt_states G maxs maxr \<equiv> opt (\<Union>{list n (types G) |n. n \<le> maxs} \<times> list maxr (err (types G)))"
    20 
    21 
    22 section {*  Executability of @{term check_bounded} *}
    23 consts
    24   list_all'_rec :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> bool"
    25 primrec
    26   "list_all'_rec P n []     = True"
    27   "list_all'_rec P n (x#xs) = (P x n \<and> list_all'_rec P (Suc n) xs)"
    28 
    29 constdefs
    30   list_all' :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
    31   "list_all' P xs \<equiv> list_all'_rec P 0 xs"
    32 
    33 lemma list_all'_rec:
    34   "\<And>n. list_all'_rec P n xs = (\<forall>p < size xs. P (xs!p) (p+n))"
    35   apply (induct xs)
    36   apply auto
    37   apply (case_tac p)
    38   apply auto
    39   done
    40 
    41 lemma list_all' [iff]:
    42   "list_all' P xs = (\<forall>n < size xs. P (xs!n) n)"
    43   by (unfold list_all'_def) (simp add: list_all'_rec)
    44 
    45 lemma [code]:
    46   "check_bounded ins et = 
    47   (list_all' (\<lambda>i pc. list_all (\<lambda>pc'. pc' < length ins) (succs i pc)) ins \<and> 
    48    list_all (\<lambda>e. fst (snd (snd e)) < length ins) et)"
    49   by (simp add: list_all_iff check_bounded_def)
    50   
    51 
    52 section {* Connecting JVM and Framework *}
    53 
    54 lemma check_bounded_is_bounded:
    55   "check_bounded ins et \<Longrightarrow> bounded (\<lambda>pc. eff (ins!pc) G pc et) (length ins)"  
    56   by (unfold bounded_def) (blast dest: check_boundedD)
    57 
    58 lemma special_ex_swap_lemma [iff]: 
    59   "(? X. (? n. X = A n & P n) & Q X) = (? n. Q(A n) & P n)"
    60   by blast
    61 
    62 lemmas [iff del] = not_None_eq
    63 
    64 theorem exec_pres_type:
    65   "wf_prog wf_mb S \<Longrightarrow> 
    66   pres_type (exec S maxs rT et bs) (size bs) (states S maxs maxr)"
    67   apply (unfold exec_def JVM_states_unfold)
    68   apply (rule pres_type_lift)
    69   apply clarify
    70   apply (case_tac s)
    71    apply simp
    72    apply (drule effNone)
    73    apply simp  
    74   apply (simp add: eff_def xcpt_eff_def norm_eff_def)
    75   apply (case_tac "bs!p")
    76 
    77   apply (clarsimp simp add: not_Err_eq)
    78   apply (drule listE_nth_in, assumption)
    79   apply fastsimp
    80 
    81   apply (fastsimp simp add: not_None_eq)
    82 
    83   apply (fastsimp simp add: not_None_eq typeof_empty_is_type)
    84 
    85   apply clarsimp
    86   apply (erule disjE)
    87    apply fastsimp
    88   apply clarsimp
    89   apply (rule_tac x="1" in exI)
    90   apply fastsimp
    91 
    92   apply clarsimp
    93   apply (erule disjE)
    94    apply (fastsimp dest: field_fields fields_is_type)
    95   apply (simp add: match_some_entry split: split_if_asm)
    96   apply (rule_tac x=1 in exI)
    97   apply fastsimp
    98 
    99   apply clarsimp
   100   apply (erule disjE)
   101    apply fastsimp
   102   apply (simp add: match_some_entry split: split_if_asm)
   103   apply (rule_tac x=1 in exI)
   104   apply fastsimp
   105 
   106   apply clarsimp
   107   apply (erule disjE)
   108    apply fastsimp
   109   apply clarsimp
   110   apply (rule_tac x=1 in exI)
   111   apply fastsimp
   112 
   113   defer 
   114 
   115   apply fastsimp
   116   apply fastsimp
   117 
   118   apply clarsimp
   119   apply (rule_tac x="n'+2" in exI)  
   120   apply simp
   121 
   122   apply clarsimp
   123   apply (rule_tac x="Suc (Suc (Suc (length ST)))" in exI)  
   124   apply simp
   125 
   126   apply clarsimp
   127   apply (rule_tac x="Suc (Suc (Suc (Suc (length ST))))" in exI)  
   128   apply simp
   129 
   130   apply fastsimp
   131   apply fastsimp
   132   apply fastsimp
   133   apply fastsimp
   134 
   135   apply clarsimp
   136   apply (erule disjE)
   137    apply fastsimp
   138   apply clarsimp
   139   apply (rule_tac x=1 in exI)
   140   apply fastsimp
   141   
   142   apply (erule disjE)
   143    apply (clarsimp simp add: Un_subset_iff)  
   144    apply (drule method_wf_mdecl, assumption+)
   145    apply (clarsimp simp add: wf_mdecl_def wf_mhead_def)
   146    apply fastsimp
   147   apply clarsimp
   148   apply (rule_tac x=1 in exI)
   149   apply fastsimp
   150   done
   151 
   152 lemmas [iff] = not_None_eq
   153 
   154 lemma sup_state_opt_unfold:
   155   "sup_state_opt G \<equiv> Opt.le (Product.le (Listn.le (subtype G)) (Listn.le (Err.le (subtype G))))"
   156   by (simp add: sup_state_opt_def sup_state_def sup_loc_def sup_ty_opt_def)
   157 
   158 
   159 lemma app_mono:
   160   "app_mono (sup_state_opt G) (\<lambda>pc. app (bs!pc) G maxs rT pc et) (length bs) (opt_states G maxs maxr)"
   161   by (unfold app_mono_def lesub_def) (blast intro: EffectMono.app_mono)
   162   
   163 
   164 lemma list_appendI:
   165   "\<lbrakk>a \<in> list x A; b \<in> list y A\<rbrakk> \<Longrightarrow> a @ b \<in> list (x+y) A"
   166   apply (unfold list_def)
   167   apply (simp (no_asm))
   168   apply blast
   169   done
   170 
   171 lemma list_map [simp]:
   172   "(map f xs \<in> list (length xs) A) = (f ` set xs \<subseteq> A)"
   173   apply (unfold list_def)
   174   apply simp
   175   done
   176 
   177 lemma [iff]:
   178   "(OK ` A \<subseteq> err B) = (A \<subseteq> B)"
   179   apply (unfold err_def)
   180   apply blast
   181   done
   182 
   183 lemma [intro]:
   184   "x \<in> A \<Longrightarrow> replicate n x \<in> list n A"
   185   by (induct n, auto)
   186 
   187 lemma lesubstep_type_simple:
   188   "a <=[Product.le (op =) r] b \<Longrightarrow> a <=|r| b"
   189   apply (unfold lesubstep_type_def)
   190   apply clarify
   191   apply (simp add: set_conv_nth)
   192   apply clarify
   193   apply (drule le_listD, assumption)
   194   apply (clarsimp simp add: lesub_def Product.le_def)
   195   apply (rule exI)
   196   apply (rule conjI)
   197    apply (rule exI)
   198    apply (rule conjI)
   199     apply (rule sym)
   200     apply assumption
   201    apply assumption
   202   apply assumption
   203   done
   204   
   205 
   206 lemma eff_mono:
   207   "\<lbrakk>p < length bs; s <=_(sup_state_opt G) t; app (bs!p) G maxs rT pc et t\<rbrakk>
   208   \<Longrightarrow> eff (bs!p) G p et s <=|sup_state_opt G| eff (bs!p) G p et t"
   209   apply (unfold eff_def)
   210   apply (rule lesubstep_type_simple)
   211   apply (rule le_list_appendI)
   212    apply (simp add: norm_eff_def)
   213    apply (rule le_listI)
   214     apply simp
   215    apply simp
   216    apply (simp add: lesub_def)
   217    apply (case_tac s)
   218     apply simp
   219    apply (simp del: split_paired_All split_paired_Ex)
   220    apply (elim exE conjE)
   221    apply simp
   222    apply (drule eff'_mono, assumption)
   223    apply assumption
   224   apply (simp add: xcpt_eff_def)
   225   apply (rule le_listI)
   226     apply simp
   227   apply simp
   228   apply (simp add: lesub_def)
   229   apply (case_tac s)
   230    apply simp
   231   apply simp
   232   apply (case_tac t)
   233    apply simp
   234   apply (clarsimp simp add: sup_state_conv)
   235   done
   236 
   237 lemma order_sup_state_opt:
   238   "ws_prog G \<Longrightarrow> order (sup_state_opt G)"
   239   by (unfold sup_state_opt_unfold) (blast dest: acyclic_subcls1 order_widen)
   240 
   241 theorem exec_mono:
   242   "ws_prog G \<Longrightarrow> bounded (exec G maxs rT et bs) (size bs) \<Longrightarrow>
   243   mono (JVMType.le G maxs maxr) (exec G maxs rT et bs) (size bs) (states G maxs maxr)"  
   244   apply (unfold exec_def JVM_le_unfold JVM_states_unfold)  
   245   apply (rule mono_lift)
   246      apply (fold sup_state_opt_unfold opt_states_def)
   247      apply (erule order_sup_state_opt)
   248     apply (rule app_mono)
   249    apply assumption
   250   apply clarify
   251   apply (rule eff_mono)
   252   apply assumption+
   253   done
   254 
   255 theorem semilat_JVM_slI:
   256   "ws_prog G \<Longrightarrow> semilat (JVMType.sl G maxs maxr)"
   257   apply (unfold JVMType.sl_def stk_esl_def reg_sl_def)
   258   apply (rule semilat_opt)
   259   apply (rule err_semilat_Product_esl)
   260   apply (rule err_semilat_upto_esl)
   261   apply (rule err_semilat_JType_esl, assumption+)
   262   apply (rule err_semilat_eslI)
   263   apply (rule Listn_sl)
   264   apply (rule err_semilat_JType_esl, assumption+)
   265   done
   266 
   267 lemma sl_triple_conv:
   268   "JVMType.sl G maxs maxr == 
   269   (states G maxs maxr, JVMType.le G maxs maxr, JVMType.sup G maxs maxr)"
   270   by (simp (no_asm) add: states_def JVMType.le_def JVMType.sup_def)
   271 
   272 
   273 lemma map_id [rule_format]:
   274   "(\<forall>n < length xs. f (g (xs!n)) = xs!n) \<longrightarrow> map f (map g xs) = xs"
   275   by (induct xs, auto)
   276 
   277 
   278 lemma is_type_pTs:
   279   "\<lbrakk> wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; ((mn,pTs),rT,code) \<in> set mdecls \<rbrakk>
   280   \<Longrightarrow> set pTs \<subseteq> types G"
   281 proof 
   282   assume "wf_prog wf_mb G" 
   283          "(C,S,fs,mdecls) \<in> set G"
   284          "((mn,pTs),rT,code) \<in> set mdecls"
   285   hence "wf_mdecl wf_mb G C ((mn,pTs),rT,code)"
   286     by (rule wf_prog_wf_mdecl)
   287   hence "\<forall>t \<in> set pTs. is_type G t" 
   288     by (unfold wf_mdecl_def wf_mhead_def) auto
   289   moreover
   290   fix t assume "t \<in> set pTs"
   291   ultimately
   292   have "is_type G t" by blast
   293   thus "t \<in> types G" ..
   294 qed
   295 
   296 
   297 lemma jvm_prog_lift:  
   298   assumes wf: 
   299   "wf_prog (\<lambda>G C bd. P G C bd) G"
   300 
   301   assumes rule:
   302   "\<And>wf_mb C mn pTs C rT maxs maxl b et bd.
   303    wf_prog wf_mb G \<Longrightarrow>
   304    method (G,C) (mn,pTs) = Some (C,rT,maxs,maxl,b,et) \<Longrightarrow>
   305    is_class G C \<Longrightarrow>
   306    set pTs \<subseteq> types G \<Longrightarrow>
   307    bd = ((mn,pTs),rT,maxs,maxl,b,et) \<Longrightarrow>
   308    P G C bd \<Longrightarrow>
   309    Q G C bd"
   310  
   311   shows 
   312   "wf_prog (\<lambda>G C bd. Q G C bd) G"
   313 proof -
   314   from wf show ?thesis
   315     apply (unfold wf_prog_def wf_cdecl_def)
   316     apply clarsimp
   317     apply (drule bspec, assumption)
   318     apply (unfold wf_cdecl_mdecl_def)
   319     apply clarsimp
   320     apply (drule bspec, assumption)
   321     apply (frule methd [OF wf [THEN wf_prog_ws_prog]], assumption+)
   322     apply (frule is_type_pTs [OF wf], assumption+)
   323     apply clarify
   324     apply (drule rule [OF wf], assumption+)
   325     apply (rule refl)
   326     apply assumption+
   327     done
   328 qed
   329 
   330 end