src/HOL/MicroJava/BV/Altern.thy
author haftmann
Tue Nov 24 14:37:23 2009 +0100 (2009-11-24)
changeset 33954 1bc3b688548c
parent 26450 158b924b5153
child 35416 d8d7d1b785af
permissions -rwxr-xr-x
backported parts of abstract byte code verifier from AFP/Jinja
     1 (*  Title:      HOL/MicroJava/BV/Altern.thy
     2     Author:     Martin Strecker
     3 *)
     4 
     5 header {* Alternative definition of well-typing of bytecode,  used in compiler type correctness proof *}
     6 
     7 theory Altern
     8 imports BVSpec
     9 begin
    10 
    11 constdefs
    12   check_type :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> JVMType.state \<Rightarrow> bool"
    13   "check_type G mxs mxr s \<equiv> s \<in> states G mxs mxr"
    14 
    15   wt_instr_altern :: "[instr,jvm_prog,ty,method_type,nat,nat,p_count,
    16                 exception_table,p_count] \<Rightarrow> bool"
    17   "wt_instr_altern i G rT phi mxs mxr max_pc et pc \<equiv>
    18   app i G mxs rT pc et (phi!pc) \<and>
    19   check_type G mxs mxr (OK (phi!pc)) \<and>
    20   (\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). pc' < max_pc \<and> G \<turnstile> s' <=' phi!pc')"
    21 
    22   wt_method_altern :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,
    23                  exception_table,method_type] \<Rightarrow> bool"
    24   "wt_method_altern G C pTs rT mxs mxl ins et phi \<equiv>
    25   let max_pc = length ins in
    26   0 < max_pc \<and> 
    27   length phi = length ins \<and>
    28   check_bounded ins et \<and> 
    29   wt_start G C pTs mxl phi \<and>
    30   (\<forall>pc. pc<max_pc \<longrightarrow> wt_instr_altern (ins!pc) G rT phi mxs (1+length pTs+mxl) max_pc et pc)"
    31 
    32 
    33 lemma wt_method_wt_method_altern : 
    34   "wt_method G C pTs rT mxs mxl ins et phi \<longrightarrow> wt_method_altern G C pTs rT mxs mxl ins et phi"
    35 apply (simp add: wt_method_def wt_method_altern_def)
    36 apply (intro strip)
    37 apply clarify
    38 apply (drule spec, drule mp, assumption)
    39 apply (simp add: check_types_def wt_instr_def wt_instr_altern_def check_type_def)
    40 apply (auto  intro: imageI)
    41 done
    42 
    43 
    44 lemma check_type_check_types [rule_format]: 
    45   "(\<forall>pc. pc < length phi \<longrightarrow> check_type G mxs mxr (OK (phi ! pc)))
    46   \<longrightarrow> check_types G mxs mxr (map OK phi)"
    47 apply (induct phi)
    48 apply (simp add: check_types_def)
    49 apply (simp add: check_types_def)
    50 apply clarify
    51 apply (frule_tac x=0 in spec)
    52 apply (simp add: check_type_def)
    53 apply auto
    54 done
    55 
    56 lemma wt_method_altern_wt_method [rule_format]: 
    57   "wt_method_altern G C pTs rT mxs mxl ins et phi \<longrightarrow> wt_method G C pTs rT mxs mxl ins et phi"
    58 apply (simp add: wt_method_def wt_method_altern_def)
    59 apply (intro strip)
    60 apply clarify
    61 apply (rule conjI)
    62   (* show check_types *)
    63 apply (rule check_type_check_types)
    64 apply (simp add: wt_instr_altern_def)
    65 
    66   (* show wt_instr *)
    67 apply (intro strip)
    68 apply (drule spec, drule mp, assumption)
    69 apply (simp add: wt_instr_def wt_instr_altern_def)
    70 done
    71 
    72 
    73 end