src/HOL/MicroJava/BV/LBVCorrect.thy
author wenzelm
Tue Sep 12 22:13:23 2000 +0200 (2000-09-12)
changeset 9941 fe05af7ec816
parent 9906 5c027cca6262
child 9970 dfe4747c8318
permissions -rw-r--r--
renamed atts: rulify to rule_format, elimify to elim_format;
     1 (*  Title:      HOL/MicroJava/BV/BVLCorrect.thy
     2     ID:         $Id$
     3     Author:     Gerwin Klein
     4     Copyright   1999 Technische Universitaet Muenchen
     5 *)
     6 
     7 header {* Correctness of the LBV *}
     8 
     9 theory LBVCorrect = BVSpec + LBVSpec:
    10 
    11 lemmas [simp del] = split_paired_Ex split_paired_All
    12 
    13 constdefs
    14 fits :: "[method_type,instr list,jvm_prog,ty,state_type option,certificate] \<Rightarrow> bool"
    15 "fits phi is G rT s0 cert \<equiv> 
    16   (\<forall>pc s1. pc < length is \<longrightarrow>
    17     (wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1 \<longrightarrow>
    18     (case cert!pc of None   \<Rightarrow> phi!pc = s1
    19                    | Some t \<Rightarrow> phi!pc = Some t)))"
    20 
    21 constdefs
    22 make_phi :: "[instr list,jvm_prog,ty,state_type option,certificate] \<Rightarrow> method_type"
    23 "make_phi is G rT s0 cert \<equiv> 
    24    map (\<lambda>pc. case cert!pc of 
    25                None   \<Rightarrow> val (wtl_inst_list (take pc is) G rT cert (length is) 0 s0) 
    26              | Some t \<Rightarrow> Some t) [0..length is(]"
    27 
    28 
    29 lemma fitsD_None:
    30   "\<lbrakk>fits phi is G rT s0 cert; pc < length is;
    31     wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1; 
    32     cert ! pc = None\<rbrakk> \<Longrightarrow> phi!pc = s1"
    33   by (auto simp add: fits_def)
    34 
    35 lemma fitsD_Some:
    36   "\<lbrakk>fits phi is G rT s0 cert; pc < length is;
    37     wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1; 
    38     cert ! pc = Some t\<rbrakk> \<Longrightarrow> phi!pc = Some t"
    39   by (auto simp add: fits_def)
    40 
    41 lemma make_phi_Some:
    42   "[| pc < length is; cert!pc = Some t |] ==> 
    43   make_phi is G rT s0 cert ! pc = Some t"
    44   by (simp add: make_phi_def)
    45 
    46 lemma make_phi_None:
    47   "[| pc < length is; cert!pc = None |] ==> 
    48   make_phi is G rT s0 cert ! pc = 
    49   val (wtl_inst_list (take pc is) G rT cert (length is) 0 s0)"
    50   by (simp add: make_phi_def)
    51 
    52 lemma exists_phi:
    53   "\<exists>phi. fits phi is G rT s0 cert"  
    54 proof - 
    55   have "fits (make_phi is G rT s0 cert) is G rT s0 cert"
    56     by (auto simp add: fits_def make_phi_Some make_phi_None 
    57              split: option.splits) 
    58 
    59   thus ?thesis
    60     by blast
    61 qed
    62   
    63 lemma fits_lemma1:
    64   "[| wtl_inst_list is G rT cert (length is) 0 s = Ok s'; fits phi is G rT s cert |]
    65   ==> \<forall>pc t. pc < length is \<longrightarrow> cert!pc = Some t \<longrightarrow> phi!pc = Some t"
    66 proof (intro strip)
    67   fix pc t 
    68   assume "wtl_inst_list is G rT cert (length is) 0 s = Ok s'"
    69   then 
    70   obtain s'' where
    71     "wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s''"
    72     by (blast dest: wtl_take)
    73   moreover
    74   assume "fits phi is G rT s cert" 
    75          "pc < length is" 
    76          "cert ! pc = Some t"
    77   ultimately
    78   show "phi!pc = Some t" by (auto dest: fitsD_Some)
    79 qed
    80 
    81 
    82 lemma wtl_suc_pc:
    83  "[| wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err;
    84      wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s';
    85      wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s'';
    86      fits phi is G rT s cert; Suc pc < length is |] ==>
    87   G \<turnstile> s'' <=' phi ! Suc pc"
    88 proof -
    89   
    90   assume all:  "wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err"
    91   assume fits: "fits phi is G rT s cert"
    92 
    93   assume wtl:  "wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s'" and
    94          wtc:  "wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s''" and
    95          pc:   "Suc pc < length is"
    96 
    97   hence wts: "wtl_inst_list (take (Suc pc) is) G rT cert (length is) 0 s = Ok s''"
    98     by (rule wtl_Suc)
    99 
   100   from all
   101   have app: 
   102   "wtl_inst_list (take (Suc pc) is@drop (Suc pc) is) G rT cert (length is) 0 s \<noteq> Err"
   103     by simp
   104 
   105   from pc 
   106   have "0 < length (drop (Suc pc) is)" 
   107     by simp
   108   then 
   109   obtain l ls where
   110     "drop (Suc pc) is = l#ls"
   111     by (auto simp add: neq_Nil_conv simp del: length_drop)
   112   with app wts pc
   113   obtain x where 
   114     "wtl_cert l G rT s'' cert (length is) (Suc pc) = Ok x"
   115     by (auto simp add: wtl_append min_def simp del: append_take_drop_id)
   116 
   117   hence c1: "\<And>t. cert!Suc pc = Some t ==> G \<turnstile> s'' <=' cert!Suc pc"
   118     by (simp add: wtl_cert_def split: if_splits)
   119   moreover
   120   from fits pc wts
   121   have c2: "\<And>t. cert!Suc pc = Some t ==> phi!Suc pc = cert!Suc pc"
   122     by - (drule fitsD_Some, auto)
   123   moreover
   124   from fits pc wts
   125   have c3: "cert!Suc pc = None ==> phi!Suc pc = s''"
   126     by (rule fitsD_None)
   127   ultimately
   128 
   129   show ?thesis 
   130     by - (cases "cert ! Suc pc", auto)
   131 qed
   132 
   133 
   134 lemma wtl_fits_wt:
   135   "[| wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err; 
   136       fits phi is G rT s cert; pc < length is |] ==>
   137    wt_instr (is!pc) G rT phi (length is) pc"
   138 proof -
   139 
   140   assume fits: "fits phi is G rT s cert"
   141 
   142   assume pc:  "pc < length is" and
   143          wtl: "wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err"
   144         
   145   then
   146   obtain s' s'' where
   147     w: "wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s'" and
   148     c: "wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s''"
   149     by - (drule wtl_all, auto)
   150 
   151   from fits wtl pc
   152   have cert_Some: 
   153     "\<And>t pc. [| pc < length is; cert!pc = Some t |] ==> phi!pc = Some t"
   154     by (auto dest: fits_lemma1)
   155   
   156   from fits wtl pc
   157   have cert_None: "cert!pc = None ==> phi!pc = s'"
   158     by - (drule fitsD_None)
   159   
   160   from pc c cert_None cert_Some
   161   have wti: "wtl_inst (is ! pc) G rT (phi!pc) cert (length is) pc = Ok s''"
   162     by (auto simp add: wtl_cert_def split: if_splits option.splits)
   163 
   164   { fix pc'
   165     assume pc': "pc' \<in> set (succs (is!pc) pc)"
   166 
   167     with wti
   168     have less: "pc' < length is"  
   169       by (simp add: wtl_inst_Ok)
   170 
   171     have "G \<turnstile> step (is!pc) G (phi!pc) <=' phi ! pc'" 
   172     proof (cases "pc' = Suc pc")
   173       case False          
   174       with wti pc'
   175       have G: "G \<turnstile> step (is ! pc) G (phi ! pc) <=' cert ! pc'" 
   176         by (simp add: wtl_inst_Ok)
   177 
   178       hence "cert!pc' = None ==> step (is ! pc) G (phi ! pc) = None"
   179         by simp
   180       hence "cert!pc' = None ==> ?thesis"
   181         by simp
   182 
   183       moreover
   184       { fix t
   185         assume "cert!pc' = Some t"
   186         with less
   187         have "phi!pc' = cert!pc'"
   188           by (simp add: cert_Some)
   189         with G
   190         have ?thesis
   191           by simp
   192       }
   193 
   194       ultimately
   195       show ?thesis by blast      
   196     next
   197       case True
   198       with pc' wti
   199       have "step (is ! pc) G (phi ! pc) = s''"  
   200         by (simp add: wtl_inst_Ok)
   201       also
   202       from w c fits pc wtl 
   203       have "Suc pc < length is ==> G \<turnstile> s'' <=' phi ! Suc pc"
   204         by - (drule wtl_suc_pc)
   205       with True less
   206       have "G \<turnstile> s'' <=' phi ! Suc pc" 
   207         by blast
   208       finally
   209       show ?thesis 
   210         by (simp add: True)
   211     qed
   212   }
   213   
   214   with wti
   215   show ?thesis
   216     by (auto simp add: wtl_inst_Ok wt_instr_def)
   217 qed
   218 
   219 
   220     
   221 lemma fits_first:
   222   "[| 0 < length is; wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err; 
   223       fits phi is G rT s cert |] ==> 
   224   G \<turnstile> s <=' phi ! 0"
   225 proof -
   226   assume wtl:  "wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err"
   227   assume fits: "fits phi is G rT s cert"
   228   assume pc:   "0 < length is"
   229 
   230   from wtl
   231   have wt0: "wtl_inst_list (take 0 is) G rT cert (length is) 0 s = Ok s"
   232     by simp
   233   
   234   with fits pc
   235   have "cert!0 = None ==> phi!0 = s"
   236     by (rule fitsD_None)
   237   moreover    
   238   from fits pc wt0
   239   have "\<And>t. cert!0 = Some t ==> phi!0 = cert!0"
   240     by - (drule fitsD_Some, auto)
   241   moreover
   242   from pc
   243   obtain x xs where "is = x#xs" 
   244     by (simp add: neq_Nil_conv) (elim, rule that)
   245   with wtl
   246   obtain s' where
   247     "wtl_cert x G rT s cert (length is) 0 = Ok s'"
   248     by simp (elim, rule that, simp)
   249   hence 
   250     "\<And>t. cert!0 = Some t ==> G \<turnstile> s <=' cert!0"
   251     by (simp add: wtl_cert_def split: if_splits)
   252 
   253   ultimately
   254   show ?thesis
   255     by - (cases "cert!0", auto)
   256 qed
   257 
   258   
   259 lemma wtl_method_correct:
   260 "wtl_method G C pTs rT mxl ins cert ==> \<exists> phi. wt_method G C pTs rT mxl ins phi"
   261 proof (unfold wtl_method_def, simp only: Let_def, elim conjE)
   262   let "?s0" = "Some ([], Ok (Class C) # map Ok pTs @ replicate mxl Err)"
   263   assume pc:  "0 < length ins"
   264   assume wtl: "wtl_inst_list ins G rT cert (length ins) 0 ?s0 \<noteq> Err"
   265 
   266   obtain phi where fits: "fits phi ins G rT ?s0 cert"    
   267     by (rule exists_phi [elim_format]) blast
   268 
   269   with wtl
   270   have allpc:
   271     "\<forall>pc. pc < length ins \<longrightarrow> wt_instr (ins ! pc) G rT phi (length ins) pc"
   272     by (blast intro: wtl_fits_wt)
   273 
   274   from pc wtl fits
   275   have "wt_start G C pTs mxl phi"
   276     by (unfold wt_start_def) (rule fits_first)
   277 
   278   with pc allpc 
   279   show ?thesis by (auto simp add: wt_method_def)
   280 qed
   281 
   282 lemma unique_set:
   283   "(a,b,c,d)\<in>set l \<longrightarrow> unique l \<longrightarrow> (a',b',c',d') \<in> set l \<longrightarrow> 
   284    a = a' \<longrightarrow> b=b' \<and> c=c' \<and> d=d'"
   285   by (induct "l") auto
   286 
   287 lemma unique_epsilon:
   288   "(a,b,c,d)\<in>set l \<longrightarrow> unique l \<longrightarrow> 
   289    (\<epsilon> (a',b',c',d'). (a',b',c',d') \<in> set l \<and> a'=a) = (a,b,c,d)"
   290   by (auto simp add: unique_set)
   291 
   292 theorem wtl_correct:
   293 "wtl_jvm_prog G cert ==> \<exists> Phi. wt_jvm_prog G Phi"
   294 proof (clarsimp simp add: wt_jvm_prog_def wf_prog_def, intro conjI)
   295 
   296   assume wtl_prog: "wtl_jvm_prog G cert"
   297   thus "ObjectC \<in> set G" by (simp add: wtl_jvm_prog_def wf_prog_def)
   298 
   299   from wtl_prog 
   300   show uniqueG: "unique G" by (simp add: wtl_jvm_prog_def wf_prog_def)
   301 
   302   show "\<exists>Phi. Ball (set G) (wf_cdecl (\<lambda>G C (sig,rT,maxl,b). 
   303               wt_method G C (snd sig) rT maxl b (Phi C sig)) G)"
   304     (is "\<exists>Phi. ?Q Phi")
   305   proof (intro exI)
   306     let "?Phi" = "\<lambda> C sig. 
   307       let (C,x,y,mdecls) = \<epsilon> (Cl,x,y,mdecls). (Cl,x,y,mdecls) \<in> set G \<and> Cl = C;
   308           (sig,rT,maxl,b) = \<epsilon> (sg,rT,maxl,b). (sg,rT,maxl,b) \<in> set mdecls \<and> sg = sig
   309       in \<epsilon> phi. wt_method G C (snd sig) rT maxl b phi"
   310     from wtl_prog
   311     show "?Q ?Phi"
   312     proof (unfold wf_cdecl_def, intro)
   313       fix x a b aa ba ab bb m
   314       assume 1: "x \<in> set G" "x = (a, b)" "b = (aa, ba)" "ba = (ab, bb)" "m \<in> set bb"
   315       with wtl_prog
   316       show "wf_mdecl (\<lambda>G C (sig,rT,maxl,b). 
   317             wt_method G C (snd sig) rT maxl b (?Phi C sig)) G a m"
   318       proof (simp add: wf_mdecl_def wtl_jvm_prog_def wf_prog_def wf_cdecl_def, 
   319              elim conjE)
   320         apply_end (drule bspec, assumption, simp, elim conjE)
   321         assume "\<forall>(sig,rT,mb)\<in>set bb. wf_mhead G sig rT \<and> 
   322                  (\<lambda>(maxl,b). wtl_method G a (snd sig) rT maxl b (cert a sig)) mb"
   323                "unique bb"
   324         with 1 uniqueG
   325         show "(\<lambda>(sig,rT,mb).
   326           wf_mhead G sig rT \<and>
   327           (\<lambda>(maxl,b).
   328               wt_method G a (snd sig) rT maxl b 
   329                ((\<lambda>(C,x,y,mdecls).
   330                     (\<lambda>(sig,rT,maxl,b). Eps (wt_method G C (snd sig) rT maxl b))
   331                      (\<epsilon>(sg,rT,maxl,b). (sg, rT, maxl, b) \<in> set mdecls \<and> sg = sig))
   332                  (\<epsilon>(Cl,x,y,mdecls). (Cl, x, y, mdecls) \<in> set G \<and> Cl = a))) mb) m"
   333           by - (drule bspec, assumption, 
   334                 clarsimp dest!: wtl_method_correct,
   335                 clarsimp intro!: selectI simp add: unique_epsilon) 
   336       qed
   337     qed (auto simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def)
   338   qed
   339 qed
   340     
   341 
   342 end