src/HOL/MicroJava/BV/LBVComplete.thy
author wenzelm
Tue Sep 12 22:13:23 2000 +0200 (2000-09-12)
changeset 9941 fe05af7ec816
parent 9906 5c027cca6262
child 10042 7164dc0d24d8
permissions -rw-r--r--
renamed atts: rulify to rule_format, elimify to elim_format;
     1 (*  Title:      HOL/MicroJava/BV/LBVComplete.thy
     2     ID:         $Id$
     3     Author:     Gerwin Klein
     4     Copyright   2000 Technische Universitaet Muenchen
     5 *)
     6 
     7 header {* Completeness of the LBV *}
     8 
     9 theory LBVComplete = BVSpec + LBVSpec + StepMono:
    10 
    11 constdefs
    12   contains_targets :: "[instr list, certificate, method_type, p_count] \<Rightarrow> bool"
    13   "contains_targets ins cert phi pc \<equiv> 
    14      \<forall>pc' \<in> set (succs (ins!pc) pc). 
    15       pc' \<noteq> pc+1 \<and> pc' < length ins \<longrightarrow> cert!pc' = phi!pc'"
    16 
    17   fits :: "[instr list, certificate, method_type] \<Rightarrow> bool"
    18   "fits ins cert phi \<equiv> \<forall>pc. pc < length ins \<longrightarrow> 
    19                        contains_targets ins cert phi pc \<and>
    20                        (cert!pc = None \<or> cert!pc = phi!pc)"
    21 
    22   is_target :: "[instr list, p_count] \<Rightarrow> bool" 
    23   "is_target ins pc \<equiv> 
    24      \<exists>pc'. pc \<noteq> pc'+1 \<and> pc' < length ins \<and> pc \<in> set (succs (ins!pc') pc')"
    25 
    26 
    27 constdefs 
    28   make_cert :: "[instr list, method_type] \<Rightarrow> certificate"
    29   "make_cert ins phi \<equiv> 
    30      map (\<lambda>pc. if is_target ins pc then phi!pc else None) [0..length ins(]"
    31 
    32   make_Cert :: "[jvm_prog, prog_type] \<Rightarrow> prog_certificate"
    33   "make_Cert G Phi \<equiv>  \<lambda> C sig.
    34      let (C,x,y,mdecls)  = \<epsilon> (Cl,x,y,mdecls). (Cl,x,y,mdecls) \<in> set G \<and> Cl = C;
    35          (sig,rT,maxl,b) = \<epsilon> (sg,rT,maxl,b). (sg,rT,maxl,b) \<in> set mdecls \<and> sg = sig
    36      in make_cert b (Phi C sig)"
    37   
    38 
    39 lemmas [simp del] = split_paired_Ex
    40 
    41 lemma make_cert_target:
    42   "[| pc < length ins; is_target ins pc |] ==> make_cert ins phi ! pc = phi!pc"
    43   by (simp add: make_cert_def)
    44 
    45 lemma make_cert_approx:
    46   "[| pc < length ins; make_cert ins phi ! pc \<noteq> phi ! pc |] ==> 
    47    make_cert ins phi ! pc = None"
    48   by (auto simp add: make_cert_def)
    49 
    50 lemma make_cert_contains_targets:
    51   "pc < length ins ==> contains_targets ins (make_cert ins phi) phi pc"
    52 proof (unfold contains_targets_def, intro strip, elim conjE)
    53  
    54   fix pc'
    55   assume "pc < length ins" 
    56          "pc' \<in> set (succs (ins ! pc) pc)" 
    57          "pc' \<noteq> pc+1" and
    58     pc': "pc' < length ins"
    59 
    60   hence "is_target ins pc'" 
    61     by (auto simp add: is_target_def)
    62 
    63   with pc'
    64   show "make_cert ins phi ! pc' = phi ! pc'" 
    65     by (auto intro: make_cert_target)
    66 qed
    67 
    68 theorem fits_make_cert:
    69   "fits ins (make_cert ins phi) phi"
    70   by (auto dest: make_cert_approx simp add: fits_def make_cert_contains_targets)
    71 
    72 
    73 lemma fitsD: 
    74   "[| fits ins cert phi; pc' \<in> set (succs (ins!pc) pc); 
    75       pc' \<noteq> Suc pc; pc < length ins; pc' < length ins |]
    76   ==> cert!pc' = phi!pc'"
    77   by (clarsimp simp add: fits_def contains_targets_def)
    78 
    79 lemma fitsD2:
    80    "[| fits ins cert phi; pc < length ins; cert!pc = Some s |]
    81   ==> cert!pc = phi!pc"
    82   by (auto simp add: fits_def)
    83                            
    84 
    85 lemma wtl_inst_mono:
    86   "[| wtl_inst i G rT s1 cert mpc pc = Ok s1'; fits ins cert phi; 
    87       pc < length ins;  G \<turnstile> s2 <=' s1; i = ins!pc |] ==>
    88   \<exists> s2'. wtl_inst (ins!pc) G rT s2 cert mpc pc = Ok s2' \<and> (G \<turnstile> s2' <=' s1')"
    89 proof -
    90   assume pc:   "pc < length ins" "i = ins!pc"
    91   assume wtl:  "wtl_inst i G rT s1 cert mpc pc = Ok s1'"
    92   assume fits: "fits ins cert phi"
    93   assume G:    "G \<turnstile> s2 <=' s1"
    94   
    95   let "?step s" = "step i G s"
    96 
    97   from wtl G
    98   have app: "app i G rT s2" by (auto simp add: wtl_inst_Ok app_mono)
    99   
   100   from wtl G
   101   have step: "succs i pc \<noteq> [] ==> G \<turnstile> ?step s2 <=' ?step s1" 
   102     by - (drule step_mono, auto simp add: wtl_inst_Ok)
   103 
   104   {
   105     fix pc'
   106     assume 0: "pc' \<in> set (succs i pc)" "pc' \<noteq> pc+1"
   107     hence "succs i pc \<noteq> []" by auto
   108     hence "G \<turnstile> ?step s2 <=' ?step s1" by (rule step)
   109     also 
   110     from wtl 0
   111     have "G \<turnstile> ?step s1 <=' cert!pc'"
   112       by (auto simp add: wtl_inst_Ok) 
   113     finally
   114     have "G\<turnstile> ?step s2 <=' cert!pc'" .
   115   } note cert = this
   116     
   117   have "\<exists>s2'. wtl_inst i G rT s2 cert mpc pc = Ok s2' \<and> G \<turnstile> s2' <=' s1'"
   118   proof (cases "pc+1 \<in> set (succs i pc)")
   119     case True
   120     with wtl
   121     have s1': "s1' = ?step s1" by (simp add: wtl_inst_Ok)
   122 
   123     have "wtl_inst i G rT s2 cert mpc pc = Ok (?step s2) \<and> G \<turnstile> ?step s2 <=' s1'" 
   124       (is "?wtl \<and> ?G")
   125     proof
   126       from True s1'
   127       show ?G by (auto intro: step)
   128 
   129       from True app wtl
   130       show ?wtl
   131         by (clarsimp intro!: cert simp add: wtl_inst_Ok)
   132     qed
   133     thus ?thesis by blast
   134   next
   135     case False
   136     with wtl
   137     have "s1' = cert ! Suc pc" by (simp add: wtl_inst_Ok)
   138 
   139     with False app wtl
   140     have "wtl_inst i G rT s2 cert mpc pc = Ok s1' \<and> G \<turnstile> s1' <=' s1'"
   141       by (clarsimp intro!: cert simp add: wtl_inst_Ok)
   142 
   143     thus ?thesis by blast
   144   qed
   145   
   146   with pc show ?thesis by simp
   147 qed
   148 
   149 
   150 lemma wtl_cert_mono:
   151   "[| wtl_cert i G rT s1 cert mpc pc = Ok s1'; fits ins cert phi; 
   152       pc < length ins; G \<turnstile> s2 <=' s1; i = ins!pc |] ==>
   153   \<exists> s2'. wtl_cert (ins!pc) G rT s2 cert mpc pc = Ok s2' \<and> (G \<turnstile> s2' <=' s1')"
   154 proof -
   155   assume wtl:  "wtl_cert i G rT s1 cert mpc pc = Ok s1'" and
   156          fits: "fits ins cert phi" "pc < length ins"
   157                "G \<turnstile> s2 <=' s1" "i = ins!pc"
   158 
   159   show ?thesis
   160   proof (cases (open) "cert!pc")
   161     case None
   162     with wtl fits
   163     show ?thesis 
   164       by - (rule wtl_inst_mono [elim_format], (simp add: wtl_cert_def)+)
   165   next
   166     case Some
   167     with wtl fits
   168 
   169     have G: "G \<turnstile> s2 <=' (Some a)"
   170       by - (rule sup_state_opt_trans, auto simp add: wtl_cert_def split: if_splits)
   171 
   172     from Some wtl
   173     have "wtl_inst i G rT (Some a) cert mpc pc = Ok s1'" 
   174       by (simp add: wtl_cert_def split: if_splits)
   175 
   176     with G fits
   177     have "\<exists> s2'. wtl_inst (ins!pc) G rT (Some a) cert mpc pc = Ok s2' \<and> 
   178                  (G \<turnstile> s2' <=' s1')"
   179       by - (rule wtl_inst_mono, (simp add: wtl_cert_def)+)
   180     
   181     with Some G
   182     show ?thesis by (simp add: wtl_cert_def)
   183   qed
   184 qed
   185 
   186  
   187 lemma wt_instr_imp_wtl_inst:
   188   "[| wt_instr (ins!pc) G rT phi max_pc pc; fits ins cert phi;
   189       pc < length ins; length ins = max_pc |] ==> 
   190   wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc \<noteq> Err"
   191  proof -
   192   assume wt:   "wt_instr (ins!pc) G rT phi max_pc pc" 
   193   assume fits: "fits ins cert phi"
   194   assume pc:   "pc < length ins" "length ins = max_pc"
   195 
   196   from wt 
   197   have app: "app (ins!pc) G rT (phi!pc)" by (simp add: wt_instr_def)
   198 
   199   from wt pc
   200   have pc': "\<And>pc'. pc' \<in> set (succs (ins!pc) pc) ==> pc' < length ins"
   201     by (simp add: wt_instr_def)
   202 
   203   let ?s' = "step (ins!pc) G (phi!pc)"
   204 
   205   from wt fits pc
   206   have cert: "!!pc'. \<lbrakk>pc' \<in> set (succs (ins!pc) pc); pc' < max_pc; pc' \<noteq> pc+1\<rbrakk> 
   207     \<Longrightarrow> G \<turnstile> ?s' <=' cert!pc'"
   208     by (auto dest: fitsD simp add: wt_instr_def)     
   209 
   210   from app pc cert pc'
   211   show ?thesis
   212     by (auto simp add: wtl_inst_Ok)
   213 qed
   214 
   215 lemma wt_less_wtl:
   216   "[| wt_instr (ins!pc) G rT phi max_pc pc; 
   217       wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = Ok s;
   218       fits ins cert phi; Suc pc < length ins; length ins = max_pc |] ==> 
   219   G \<turnstile> s <=' phi ! Suc pc"
   220 proof -
   221   assume wt:   "wt_instr (ins!pc) G rT phi max_pc pc" 
   222   assume wtl:  "wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = Ok s"
   223   assume fits: "fits ins cert phi"
   224   assume pc:   "Suc pc < length ins" "length ins = max_pc"
   225 
   226   { assume suc: "Suc pc \<in> set (succs (ins ! pc) pc)"
   227     with wtl         have "s = step (ins!pc) G (phi!pc)"
   228       by (simp add: wtl_inst_Ok)
   229     also from suc wt have "G \<turnstile> ... <=' phi!Suc pc"
   230       by (simp add: wt_instr_def)
   231     finally have ?thesis .
   232   }
   233 
   234   moreover
   235   { assume "Suc pc \<notin> set (succs (ins ! pc) pc)"
   236     
   237     with wtl
   238     have "s = cert!Suc pc" 
   239       by (simp add: wtl_inst_Ok)
   240     with fits pc
   241     have ?thesis
   242       by - (cases "cert!Suc pc", simp, drule fitsD2, assumption+, simp)
   243   }
   244 
   245   ultimately
   246   show ?thesis by blast
   247 qed
   248   
   249 
   250 lemma wt_instr_imp_wtl_cert:
   251   "[| wt_instr (ins!pc) G rT phi max_pc pc; fits ins cert phi;
   252       pc < length ins; length ins = max_pc |] ==> 
   253   wtl_cert (ins!pc) G rT (phi!pc) cert max_pc pc \<noteq> Err"
   254 proof -
   255   assume "wt_instr (ins!pc) G rT phi max_pc pc" and 
   256    fits: "fits ins cert phi" and
   257      pc: "pc < length ins" and
   258          "length ins = max_pc"
   259   
   260   hence wtl: "wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc \<noteq> Err"
   261     by (rule wt_instr_imp_wtl_inst)
   262 
   263   hence "cert!pc = None ==> ?thesis"
   264     by (simp add: wtl_cert_def)
   265 
   266   moreover
   267   { fix s
   268     assume c: "cert!pc = Some s"
   269     with fits pc
   270     have "cert!pc = phi!pc"
   271       by (rule fitsD2)
   272     from this c wtl
   273     have ?thesis
   274       by (clarsimp simp add: wtl_cert_def)
   275   }
   276 
   277   ultimately
   278   show ?thesis by blast
   279 qed
   280   
   281 
   282 lemma wt_less_wtl_cert:
   283   "[| wt_instr (ins!pc) G rT phi max_pc pc; 
   284       wtl_cert (ins!pc) G rT (phi!pc) cert max_pc pc = Ok s;
   285       fits ins cert phi; Suc pc < length ins; length ins = max_pc |] ==> 
   286   G \<turnstile> s <=' phi ! Suc pc"
   287 proof -
   288   assume wtl: "wtl_cert (ins!pc) G rT (phi!pc) cert max_pc pc = Ok s"
   289 
   290   assume wti: "wt_instr (ins!pc) G rT phi max_pc pc"
   291               "fits ins cert phi" 
   292               "Suc pc < length ins" "length ins = max_pc"
   293   
   294   { assume "cert!pc = None"
   295     with wtl
   296     have "wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = Ok s"
   297       by (simp add: wtl_cert_def)
   298     with wti
   299     have ?thesis
   300       by - (rule wt_less_wtl)
   301   }
   302   moreover
   303   { fix t
   304     assume c: "cert!pc = Some t"
   305     with wti
   306     have "cert!pc = phi!pc"
   307       by - (rule fitsD2, simp+)
   308     with c wtl
   309     have "wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = Ok s"
   310       by (simp add: wtl_cert_def)
   311     with wti
   312     have ?thesis
   313       by - (rule wt_less_wtl)
   314   }   
   315     
   316   ultimately
   317   show ?thesis by blast
   318 qed
   319 
   320 
   321 text {*
   322   \medskip
   323   Main induction over the instruction list.
   324 *}
   325 
   326 theorem wt_imp_wtl_inst_list:
   327 "\<forall> pc. (\<forall>pc'. pc' < length all_ins \<longrightarrow> 
   328         wt_instr (all_ins ! pc') G rT phi (length all_ins) pc') \<longrightarrow>
   329        fits all_ins cert phi \<longrightarrow> 
   330        (\<exists>l. pc = length l \<and> all_ins = l@ins) \<longrightarrow>  
   331        pc < length all_ins \<longrightarrow>      
   332        (\<forall> s. (G \<turnstile> s <=' (phi!pc)) \<longrightarrow> 
   333              wtl_inst_list ins G rT cert (length all_ins) pc s \<noteq> Err)" 
   334 (is "\<forall>pc. ?wt \<longrightarrow> ?fits \<longrightarrow> ?l pc ins \<longrightarrow> ?len pc \<longrightarrow> ?wtl pc ins"  
   335  is "\<forall>pc. ?C pc ins" is "?P ins") 
   336 proof (induct "?P" "ins")
   337   case Nil
   338   show "?P []" by simp
   339 next
   340   fix i ins'
   341   assume Cons: "?P ins'"
   342 
   343   show "?P (i#ins')" 
   344   proof (intro allI impI, elim exE conjE)
   345     fix pc s l
   346     assume wt  : "\<forall>pc'. pc' < length all_ins \<longrightarrow> 
   347                         wt_instr (all_ins ! pc') G rT phi (length all_ins) pc'"
   348     assume fits: "fits all_ins cert phi"
   349     assume l   : "pc < length all_ins"
   350     assume G   : "G \<turnstile> s <=' phi ! pc"
   351     assume pc  : "all_ins = l@i#ins'" "pc = length l"
   352     hence  i   : "all_ins ! pc = i"
   353       by (simp add: nth_append)
   354 
   355     from l wt
   356     have wti: "wt_instr (all_ins!pc) G rT phi (length all_ins) pc" by blast
   357 
   358     with fits l 
   359     have c: "wtl_cert (all_ins!pc) G rT (phi!pc) cert (length all_ins) pc \<noteq> Err"
   360       by - (drule wt_instr_imp_wtl_cert, auto)
   361     
   362     from Cons
   363     have "?C (Suc pc) ins'" by blast
   364     with wt fits pc
   365     have IH: "?len (Suc pc) \<longrightarrow> ?wtl (Suc pc) ins'" by auto
   366 
   367     show "wtl_inst_list (i#ins') G rT cert (length all_ins) pc s \<noteq> Err" 
   368     proof (cases "?len (Suc pc)")
   369       case False
   370       with pc
   371       have "ins' = []" by simp
   372       with G i c fits l
   373       show ?thesis by (auto dest: wtl_cert_mono)
   374     next
   375       case True
   376       with IH
   377       have wtl: "?wtl (Suc pc) ins'" by blast
   378 
   379       from c wti fits l True
   380       obtain s'' where
   381         "wtl_cert (all_ins!pc) G rT (phi!pc) cert (length all_ins) pc = Ok s''"
   382         "G \<turnstile> s'' <=' phi ! Suc pc"
   383         by clarsimp (drule wt_less_wtl_cert, auto)
   384       moreover
   385       from calculation fits G l
   386       obtain s' where
   387         c': "wtl_cert (all_ins!pc) G rT s cert (length all_ins) pc = Ok s'" and
   388         "G \<turnstile> s' <=' s''"
   389         by - (drule wtl_cert_mono, auto)
   390       ultimately
   391       have G': "G \<turnstile> s' <=' phi ! Suc pc" 
   392         by - (rule sup_state_opt_trans)
   393 
   394       with wtl
   395       have "wtl_inst_list ins' G rT cert (length all_ins) (Suc pc) s' \<noteq> Err"
   396         by auto
   397 
   398       with i c'
   399       show ?thesis by auto
   400     qed
   401   qed
   402 qed
   403   
   404 
   405 lemma fits_imp_wtl_method_complete:
   406   "[| wt_method G C pTs rT mxl ins phi; fits ins cert phi |] ==> 
   407   wtl_method G C pTs rT mxl ins cert"
   408 by (simp add: wt_method_def wtl_method_def)
   409    (rule wt_imp_wtl_inst_list [rule_format, elim_format], auto simp add: wt_start_def) 
   410 
   411 
   412 lemma wtl_method_complete:
   413   "wt_method G C pTs rT mxl ins phi ==> 
   414   wtl_method G C pTs rT mxl ins (make_cert ins phi)"
   415 proof -
   416   assume "wt_method G C pTs rT mxl ins phi" 
   417   moreover
   418   have "fits ins (make_cert ins phi) phi"
   419     by (rule fits_make_cert)
   420   ultimately
   421   show ?thesis 
   422     by (rule fits_imp_wtl_method_complete)
   423 qed
   424 
   425 lemma unique_set:
   426 "(a,b,c,d)\<in>set l \<longrightarrow> unique l \<longrightarrow> (a',b',c',d') \<in> set l \<longrightarrow> 
   427   a = a' \<longrightarrow> b=b' \<and> c=c' \<and> d=d'"
   428   by (induct "l") auto
   429 
   430 lemma unique_epsilon:
   431   "(a,b,c,d)\<in>set l \<longrightarrow> unique l \<longrightarrow> 
   432   (\<epsilon> (a',b',c',d'). (a',b',c',d') \<in> set l \<and> a'=a) = (a,b,c,d)"
   433   by (auto simp add: unique_set)
   434 
   435 
   436 theorem wtl_complete: 
   437   "wt_jvm_prog G Phi ==> wtl_jvm_prog G (make_Cert G Phi)"
   438 proof (simp only: wt_jvm_prog_def)
   439 
   440   assume wfprog: 
   441     "wf_prog (\<lambda>G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) G"
   442 
   443   thus ?thesis 
   444   proof (simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def wf_mdecl_def, auto)
   445     fix a aa ab b ac ba ad ae bb 
   446     assume 1 : "\<forall>(C,sc,fs,ms)\<in>set G.
   447              Ball (set fs) (wf_fdecl G) \<and>
   448              unique fs \<and>
   449              (\<forall>(sig,rT,mb)\<in>set ms. wf_mhead G sig rT \<and> 
   450                (\<lambda>(maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) mb) \<and>
   451              unique ms \<and>
   452              (case sc of None \<Rightarrow> C = Object
   453               | Some D \<Rightarrow>
   454                   is_class G D \<and>
   455                   (D, C) \<notin> (subcls1 G)^* \<and>
   456                   (\<forall>(sig,rT,b)\<in>set ms. 
   457                    \<forall>D' rT' b'. method (G, D) sig = Some (D', rT', b') \<longrightarrow> G\<turnstile>rT\<preceq>rT'))"
   458              "(a, aa, ab, b) \<in> set G"
   459   
   460     assume uG : "unique G" 
   461     assume b  : "((ac, ba), ad, ae, bb) \<in> set b"
   462 
   463     from 1
   464     show "wtl_method G a ba ad ae bb (make_Cert G Phi a (ac, ba))"
   465     proof (rule bspec [elim_format], clarsimp)
   466       assume ub : "unique b"
   467       assume m: "\<forall>(sig,rT,mb)\<in>set b. wf_mhead G sig rT \<and> 
   468                   (\<lambda>(maxl,b). wt_method G a (snd sig) rT maxl b (Phi a sig)) mb" 
   469       from m b
   470       show ?thesis
   471       proof (rule bspec [elim_format], clarsimp)
   472         assume "wt_method G a ba ad ae bb (Phi a (ac, ba))"         
   473         with wfprog uG ub b 1
   474         show ?thesis
   475           by - (rule wtl_method_complete [elim_format], assumption+, 
   476                 simp add: make_Cert_def unique_epsilon)
   477       qed 
   478     qed
   479   qed
   480 qed
   481 
   482 lemmas [simp] = split_paired_Ex
   483 
   484 end