src/HOL/MicroJava/BV/LBVJVM.thy
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 23467 d1b97708d5eb
child 26450 158b924b5153
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{LBV for the JVM}\label{sec:JVM} *}
     8 
     9 theory LBVJVM
    10 imports LBVCorrect LBVComplete Typing_Framework_JVM
    11 begin
    12 
    13 types prog_cert = "cname \<Rightarrow> sig \<Rightarrow> state list"
    14 
    15 constdefs
    16   check_cert :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state list \<Rightarrow> bool"
    17   "check_cert G mxs mxr n cert \<equiv> check_types G mxs mxr cert \<and> length cert = n+1 \<and>
    18                                  (\<forall>i<n. cert!i \<noteq> Err) \<and> cert!n = OK None"
    19 
    20   lbvjvm :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> 
    21              state list \<Rightarrow> instr list \<Rightarrow> state \<Rightarrow> state"
    22   "lbvjvm G maxs maxr rT et cert bs \<equiv>
    23   wtl_inst_list bs cert  (JVMType.sup G maxs maxr) (JVMType.le G maxs maxr) Err (OK None) (exec G maxs rT et bs) 0"
    24 
    25   wt_lbv :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 
    26              exception_table \<Rightarrow> state list \<Rightarrow> instr list \<Rightarrow> bool"
    27   "wt_lbv G C pTs rT mxs mxl et cert ins \<equiv>
    28    check_bounded ins et \<and> 
    29    check_cert G mxs (1+size pTs+mxl) (length ins) cert \<and>
    30    0 < size ins \<and> 
    31    (let start  = Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err));
    32         result = lbvjvm G mxs (1+size pTs+mxl) rT et cert ins (OK start)
    33     in result \<noteq> Err)"
    34 
    35   wt_jvm_prog_lbv :: "jvm_prog \<Rightarrow> prog_cert \<Rightarrow> bool"
    36   "wt_jvm_prog_lbv G cert \<equiv>
    37   wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)). wt_lbv G C (snd sig) rT maxs maxl et (cert C sig) b) G"
    38 
    39   mk_cert :: "jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> instr list 
    40               \<Rightarrow> method_type \<Rightarrow> state list"
    41   "mk_cert G maxs rT et bs phi \<equiv> make_cert (exec G maxs rT et bs) (map OK phi) (OK None)"
    42 
    43   prg_cert :: "jvm_prog \<Rightarrow> prog_type \<Rightarrow> prog_cert"
    44   "prg_cert G phi C sig \<equiv> let (C,rT,(maxs,maxl,ins,et)) = the (method (G,C) sig) in 
    45                            mk_cert G maxs rT et ins (phi C sig)"
    46  
    47   
    48 lemma wt_method_def2:
    49   fixes pTs and mxl and G and mxs and rT and et and bs and phi 
    50   defines [simp]: "mxr   \<equiv> 1 + length pTs + mxl"
    51   defines [simp]: "r     \<equiv> sup_state_opt G"
    52   defines [simp]: "app0  \<equiv> \<lambda>pc. app (bs!pc) G mxs rT pc et"
    53   defines [simp]: "step0 \<equiv> \<lambda>pc. eff (bs!pc) G pc et"
    54 
    55   shows
    56   "wt_method G C pTs rT mxs mxl bs et phi = 
    57   (bs \<noteq> [] \<and> 
    58    length phi = length bs \<and>
    59    check_bounded bs et \<and> 
    60    check_types G mxs mxr (map OK phi) \<and>   
    61    wt_start G C pTs mxl phi \<and> 
    62    wt_app_eff r app0 step0 phi)"
    63   by (auto simp add: wt_method_def wt_app_eff_def wt_instr_def lesub_def
    64            dest: check_bounded_is_bounded boundedD)
    65 
    66 
    67 lemma check_certD:
    68   "check_cert G mxs mxr n cert \<Longrightarrow> cert_ok cert n Err (OK None) (states G mxs mxr)"
    69   apply (unfold cert_ok_def check_cert_def check_types_def)
    70   apply (auto simp add: list_all_iff)
    71   done
    72 
    73 
    74 lemma wt_lbv_wt_step:
    75   assumes wf:  "wf_prog wf_mb G"
    76   assumes lbv: "wt_lbv G C pTs rT mxs mxl et cert ins"
    77   assumes C:   "is_class G C" 
    78   assumes pTs: "set pTs \<subseteq> types G"
    79   
    80   defines [simp]: "mxr \<equiv> 1+length pTs+mxl"
    81 
    82   shows "\<exists>ts \<in> list (size ins) (states G mxs mxr). 
    83             wt_step (JVMType.le G mxs mxr) Err (exec G mxs rT et ins) ts
    84           \<and> OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err))) <=_(JVMType.le G mxs mxr) ts!0"
    85 proof -
    86   let ?step = "exec G mxs rT et ins"
    87   let ?r    = "JVMType.le G mxs mxr"
    88   let ?f    = "JVMType.sup G mxs mxr"
    89   let ?A    = "states G mxs mxr"
    90 
    91   have "semilat (JVMType.sl G mxs mxr)" 
    92     by (rule semilat_JVM_slI, rule wf_prog_ws_prog, rule wf)
    93   hence "semilat (?A, ?r, ?f)" by (unfold sl_triple_conv)
    94   moreover
    95   have "top ?r Err"  by (simp add: JVM_le_unfold)
    96   moreover
    97   have "Err \<in> ?A" by (simp add: JVM_states_unfold)
    98   moreover
    99   have "bottom ?r (OK None)" 
   100     by (simp add: JVM_le_unfold bottom_def)
   101   moreover
   102   have "OK None \<in> ?A" by (simp add: JVM_states_unfold)
   103   moreover
   104   from lbv
   105   have "bounded ?step (length ins)" 
   106     by (clarsimp simp add: wt_lbv_def exec_def) 
   107        (intro bounded_lift check_bounded_is_bounded) 
   108   moreover
   109   from lbv
   110   have "cert_ok cert (length ins) Err (OK None) ?A" 
   111     by (unfold wt_lbv_def) (auto dest: check_certD)
   112   moreover
   113   from wf have "pres_type ?step (length ins) ?A" by (rule exec_pres_type)
   114   moreover
   115   let ?start = "OK (Some ([],(OK (Class C))#(map OK pTs)@(replicate mxl Err)))"
   116   from lbv
   117   have "wtl_inst_list ins cert ?f ?r Err (OK None) ?step 0 ?start \<noteq> Err"
   118     by (simp add: wt_lbv_def lbvjvm_def)    
   119   moreover
   120   from C pTs have "?start \<in> ?A"
   121     by (unfold JVM_states_unfold) (auto intro: list_appendI, force)
   122   moreover
   123   from lbv have "0 < length ins" by (simp add: wt_lbv_def)
   124   ultimately
   125   show ?thesis by (rule lbvs.wtl_sound_strong)
   126 qed
   127   
   128 lemma wt_lbv_wt_method:
   129   assumes wf:  "wf_prog wf_mb G"
   130   assumes lbv: "wt_lbv G C pTs rT mxs mxl et cert ins"
   131   assumes C:   "is_class G C" 
   132   assumes pTs: "set pTs \<subseteq> types G"
   133   
   134   shows "\<exists>phi. wt_method G C pTs rT mxs mxl ins et phi"
   135 proof -
   136   let ?mxr   = "1 + length pTs + mxl"
   137   let ?step  = "exec G mxs rT et ins"
   138   let ?r     = "JVMType.le G mxs ?mxr"
   139   let ?f     = "JVMType.sup G mxs ?mxr"
   140   let ?A     = "states G mxs ?mxr"
   141   let ?start = "OK (Some ([],(OK (Class C))#(map OK pTs)@(replicate mxl Err)))"
   142   
   143   from lbv have l: "ins \<noteq> []" by (simp add: wt_lbv_def)
   144   moreover
   145   from wf lbv C pTs
   146   obtain phi where 
   147     list:  "phi \<in> list (length ins) ?A" and
   148     step:  "wt_step ?r Err ?step phi" and    
   149     start: "?start <=_?r phi!0" 
   150     by (blast dest: wt_lbv_wt_step)
   151   from list have [simp]: "length phi = length ins" by simp
   152   have "length (map ok_val phi) = length ins" by simp  
   153   moreover
   154   from l have 0: "0 < length phi" by simp
   155   with step obtain phi0 where "phi!0 = OK phi0"
   156     by (unfold wt_step_def) blast
   157   with start 0
   158   have "wt_start G C pTs mxl (map ok_val phi)"
   159     by (simp add: wt_start_def JVM_le_Err_conv lesub_def)
   160   moreover
   161   from lbv  have chk_bounded: "check_bounded ins et"
   162     by (simp add: wt_lbv_def)
   163   moreover {
   164     from list
   165     have "check_types G mxs ?mxr phi"
   166       by (simp add: check_types_def)
   167     also from step
   168     have [symmetric]: "map OK (map ok_val phi) = phi" 
   169       by (auto intro!: map_id simp add: wt_step_def)
   170     finally have "check_types G mxs ?mxr (map OK (map ok_val phi))" .
   171   }
   172   moreover {  
   173     let ?app = "\<lambda>pc. app (ins!pc) G mxs rT pc et"
   174     let ?eff = "\<lambda>pc. eff (ins!pc) G pc et"
   175 
   176     from chk_bounded
   177     have "bounded (err_step (length ins) ?app ?eff) (length ins)"
   178       by (blast dest: check_bounded_is_bounded boundedD intro: bounded_err_stepI)
   179     moreover
   180     from step
   181     have "wt_err_step (sup_state_opt G) ?step phi"
   182       by (simp add: wt_err_step_def JVM_le_Err_conv)
   183     ultimately
   184     have "wt_app_eff (sup_state_opt G) ?app ?eff (map ok_val phi)"
   185       by (auto intro: wt_err_imp_wt_app_eff simp add: exec_def)
   186   }    
   187   ultimately
   188   have "wt_method G C pTs rT mxs mxl ins et (map ok_val phi)"
   189     by - (rule wt_method_def2 [THEN iffD2], simp)
   190   thus ?thesis ..
   191 qed
   192 
   193 
   194 lemma wt_method_wt_lbv:
   195   assumes wf:  "wf_prog wf_mb G"
   196   assumes wt:  "wt_method G C pTs rT mxs mxl ins et phi"
   197   assumes C:   "is_class G C" 
   198   assumes pTs: "set pTs \<subseteq> types G"
   199   
   200   defines [simp]: "cert \<equiv> mk_cert G mxs rT et ins phi"
   201 
   202   shows "wt_lbv G C pTs rT mxs mxl et cert ins"
   203 proof -
   204   let ?mxr  = "1 + length pTs + mxl"
   205   let ?step = "exec G mxs rT et ins"
   206   let ?app  = "\<lambda>pc. app (ins!pc) G mxs rT pc et"
   207   let ?eff  = "\<lambda>pc. eff (ins!pc) G pc et"
   208   let ?r    = "JVMType.le G mxs ?mxr"
   209   let ?f    = "JVMType.sup G mxs ?mxr"
   210   let ?A    = "states G mxs ?mxr"
   211   let ?phi  = "map OK phi"
   212   let ?cert = "make_cert ?step ?phi (OK None)"
   213 
   214   from wt obtain 
   215     0:          "0 < length ins" and
   216     length:     "length ins = length ?phi" and
   217     ck_bounded: "check_bounded ins et" and
   218     ck_types:   "check_types G mxs ?mxr ?phi" and
   219     wt_start:   "wt_start G C pTs mxl phi" and
   220     app_eff:    "wt_app_eff (sup_state_opt G) ?app ?eff phi"
   221     by (simp (asm_lr) add: wt_method_def2)
   222   
   223   have "semilat (JVMType.sl G mxs ?mxr)" 
   224     by (rule semilat_JVM_slI) (rule wf_prog_ws_prog [OF wf])
   225   hence "semilat (?A, ?r, ?f)" by (unfold sl_triple_conv)
   226   moreover
   227   have "top ?r Err"  by (simp add: JVM_le_unfold)
   228   moreover
   229   have "Err \<in> ?A" by (simp add: JVM_states_unfold)
   230   moreover
   231   have "bottom ?r (OK None)" 
   232     by (simp add: JVM_le_unfold bottom_def)
   233   moreover
   234   have "OK None \<in> ?A" by (simp add: JVM_states_unfold)
   235   moreover
   236   from ck_bounded
   237   have bounded: "bounded ?step (length ins)" 
   238     by (clarsimp simp add: exec_def) 
   239        (intro bounded_lift check_bounded_is_bounded)
   240   with wf
   241   have "mono ?r ?step (length ins) ?A"
   242     by (rule wf_prog_ws_prog [THEN exec_mono])
   243   hence "mono ?r ?step (length ?phi) ?A" by (simp add: length)
   244   moreover
   245   from wf have "pres_type ?step (length ins) ?A" by (rule exec_pres_type)
   246   hence "pres_type ?step (length ?phi) ?A" by (simp add: length)
   247   moreover
   248   from ck_types
   249   have "set ?phi \<subseteq> ?A" by (simp add: check_types_def) 
   250   hence "\<forall>pc. pc < length ?phi \<longrightarrow> ?phi!pc \<in> ?A \<and> ?phi!pc \<noteq> Err" by auto
   251   moreover 
   252   from bounded 
   253   have "bounded (exec G mxs rT et ins) (length ?phi)" by (simp add: length)
   254   moreover
   255   have "OK None \<noteq> Err" by simp
   256   moreover
   257   from bounded length app_eff
   258   have "wt_err_step (sup_state_opt G) ?step ?phi"
   259     by (auto intro: wt_app_eff_imp_wt_err simp add: exec_def)
   260   hence "wt_step ?r Err ?step ?phi"
   261     by (simp add: wt_err_step_def JVM_le_Err_conv)
   262   moreover 
   263   let ?start = "OK (Some ([],(OK (Class C))#(map OK pTs)@(replicate mxl Err)))"  
   264   from 0 length have "0 < length phi" by auto
   265   hence "?phi!0 = OK (phi!0)" by simp
   266   with wt_start have "?start <=_?r ?phi!0"
   267     by (clarsimp simp add: wt_start_def lesub_def JVM_le_Err_conv)
   268   moreover
   269   from C pTs have "?start \<in> ?A"
   270     by (unfold JVM_states_unfold) (auto intro: list_appendI, force)
   271   moreover
   272   have "?start \<noteq> Err" by simp
   273   moreover
   274   note length 
   275   ultimately
   276   have "wtl_inst_list ins ?cert ?f ?r Err (OK None) ?step 0 ?start \<noteq> Err"
   277     by (rule lbvc.wtl_complete)
   278   moreover
   279   from 0 length have "phi \<noteq> []" by auto
   280   moreover
   281   from ck_types
   282   have "check_types G mxs ?mxr ?cert"
   283     by (auto simp add: make_cert_def check_types_def JVM_states_unfold)
   284   moreover
   285   note ck_bounded 0 length
   286   ultimately 
   287   show ?thesis 
   288     by (simp add: wt_lbv_def lbvjvm_def mk_cert_def 
   289       check_cert_def make_cert_def nth_append)
   290 qed  
   291 
   292 
   293 
   294 theorem jvm_lbv_correct:
   295   "wt_jvm_prog_lbv G Cert \<Longrightarrow> \<exists>Phi. wt_jvm_prog G Phi"
   296 proof -  
   297   let ?Phi = "\<lambda>C sig. let (C,rT,(maxs,maxl,ins,et)) = the (method (G,C) sig) in 
   298               SOME phi. wt_method G C (snd sig) rT maxs maxl ins et phi"
   299     
   300   assume "wt_jvm_prog_lbv G Cert"
   301   hence "wt_jvm_prog G ?Phi"
   302     apply (unfold wt_jvm_prog_def wt_jvm_prog_lbv_def)
   303     apply (erule jvm_prog_lift)
   304     apply (auto dest: wt_lbv_wt_method intro: someI)
   305     done
   306   thus ?thesis by blast
   307 qed
   308 
   309 theorem jvm_lbv_complete:
   310   "wt_jvm_prog G Phi \<Longrightarrow> wt_jvm_prog_lbv G (prg_cert G Phi)"
   311   apply (unfold wt_jvm_prog_def wt_jvm_prog_lbv_def)
   312   apply (erule jvm_prog_lift)
   313   apply (auto simp add: prg_cert_def intro: wt_method_wt_lbv)
   314   done  
   315 
   316 end