src/HOL/MicroJava/BV/LBVCorrect.thy
changeset 10496 f2d304bdf3cc
parent 10042 7164dc0d24d8
child 10592 fc0b575a2cf7
     1.1 --- a/src/HOL/MicroJava/BV/LBVCorrect.thy	Sat Nov 18 19:48:34 2000 +0100
     1.2 +++ b/src/HOL/MicroJava/BV/LBVCorrect.thy	Mon Nov 20 16:37:42 2000 +0100
     1.3 @@ -14,7 +14,7 @@
     1.4  fits :: "[method_type,instr list,jvm_prog,ty,state_type option,certificate] => bool"
     1.5  "fits phi is G rT s0 cert == 
     1.6    (\<forall>pc s1. pc < length is -->
     1.7 -    (wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1 -->
     1.8 +    (wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = OK s1 -->
     1.9      (case cert!pc of None   => phi!pc = s1
    1.10                     | Some t => phi!pc = Some t)))"
    1.11  
    1.12 @@ -22,19 +22,19 @@
    1.13  make_phi :: "[instr list,jvm_prog,ty,state_type option,certificate] => method_type"
    1.14  "make_phi is G rT s0 cert == 
    1.15     map (\<lambda>pc. case cert!pc of 
    1.16 -               None   => val (wtl_inst_list (take pc is) G rT cert (length is) 0 s0) 
    1.17 +               None   => ok_val (wtl_inst_list (take pc is) G rT cert (length is) 0 s0) 
    1.18               | Some t => Some t) [0..length is(]"
    1.19  
    1.20  
    1.21  lemma fitsD_None:
    1.22    "[|fits phi is G rT s0 cert; pc < length is;
    1.23 -    wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1; 
    1.24 +    wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = OK s1; 
    1.25      cert ! pc = None|] ==> phi!pc = s1"
    1.26    by (auto simp add: fits_def)
    1.27  
    1.28  lemma fitsD_Some:
    1.29    "[|fits phi is G rT s0 cert; pc < length is;
    1.30 -    wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1; 
    1.31 +    wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = OK s1; 
    1.32      cert ! pc = Some t|] ==> phi!pc = Some t"
    1.33    by (auto simp add: fits_def)
    1.34  
    1.35 @@ -46,7 +46,7 @@
    1.36  lemma make_phi_None:
    1.37    "[| pc < length is; cert!pc = None |] ==> 
    1.38    make_phi is G rT s0 cert ! pc = 
    1.39 -  val (wtl_inst_list (take pc is) G rT cert (length is) 0 s0)"
    1.40 +  ok_val (wtl_inst_list (take pc is) G rT cert (length is) 0 s0)"
    1.41    by (simp add: make_phi_def)
    1.42  
    1.43  lemma exists_phi:
    1.44 @@ -61,14 +61,14 @@
    1.45  qed
    1.46    
    1.47  lemma fits_lemma1:
    1.48 -  "[| wtl_inst_list is G rT cert (length is) 0 s = Ok s'; fits phi is G rT s cert |]
    1.49 +  "[| wtl_inst_list is G rT cert (length is) 0 s = OK s'; fits phi is G rT s cert |]
    1.50    ==> \<forall>pc t. pc < length is --> cert!pc = Some t --> phi!pc = Some t"
    1.51  proof (intro strip)
    1.52    fix pc t 
    1.53 -  assume "wtl_inst_list is G rT cert (length is) 0 s = Ok s'"
    1.54 +  assume "wtl_inst_list is G rT cert (length is) 0 s = OK s'"
    1.55    then 
    1.56    obtain s'' where
    1.57 -    "wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s''"
    1.58 +    "wtl_inst_list (take pc is) G rT cert (length is) 0 s = OK s''"
    1.59      by (blast dest: wtl_take)
    1.60    moreover
    1.61    assume "fits phi is G rT s cert" 
    1.62 @@ -81,8 +81,8 @@
    1.63  
    1.64  lemma wtl_suc_pc:
    1.65   "[| wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err;
    1.66 -     wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s';
    1.67 -     wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s'';
    1.68 +     wtl_inst_list (take pc is) G rT cert (length is) 0 s = OK s';
    1.69 +     wtl_cert (is!pc) G rT s' cert (length is) pc = OK s'';
    1.70       fits phi is G rT s cert; Suc pc < length is |] ==>
    1.71    G \<turnstile> s'' <=' phi ! Suc pc"
    1.72  proof -
    1.73 @@ -90,11 +90,11 @@
    1.74    assume all:  "wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err"
    1.75    assume fits: "fits phi is G rT s cert"
    1.76  
    1.77 -  assume wtl:  "wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s'" and
    1.78 -         wtc:  "wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s''" and
    1.79 +  assume wtl:  "wtl_inst_list (take pc is) G rT cert (length is) 0 s = OK s'" and
    1.80 +         wtc:  "wtl_cert (is!pc) G rT s' cert (length is) pc = OK s''" and
    1.81           pc:   "Suc pc < length is"
    1.82  
    1.83 -  hence wts: "wtl_inst_list (take (Suc pc) is) G rT cert (length is) 0 s = Ok s''"
    1.84 +  hence wts: "wtl_inst_list (take (Suc pc) is) G rT cert (length is) 0 s = OK s''"
    1.85      by (rule wtl_Suc)
    1.86  
    1.87    from all
    1.88 @@ -111,7 +111,7 @@
    1.89      by (auto simp add: neq_Nil_conv simp del: length_drop)
    1.90    with app wts pc
    1.91    obtain x where 
    1.92 -    "wtl_cert l G rT s'' cert (length is) (Suc pc) = Ok x"
    1.93 +    "wtl_cert l G rT s'' cert (length is) (Suc pc) = OK x"
    1.94      by (auto simp add: wtl_append min_def simp del: append_take_drop_id)
    1.95  
    1.96    hence c1: "!!t. cert!Suc pc = Some t ==> G \<turnstile> s'' <=' cert!Suc pc"
    1.97 @@ -144,8 +144,8 @@
    1.98          
    1.99    then
   1.100    obtain s' s'' where
   1.101 -    w: "wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s'" and
   1.102 -    c: "wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s''"
   1.103 +    w: "wtl_inst_list (take pc is) G rT cert (length is) 0 s = OK s'" and
   1.104 +    c: "wtl_cert (is!pc) G rT s' cert (length is) pc = OK s''"
   1.105      by - (drule wtl_all, auto)
   1.106  
   1.107    from fits wtl pc
   1.108 @@ -158,7 +158,7 @@
   1.109      by - (drule fitsD_None)
   1.110    
   1.111    from pc c cert_None cert_Some
   1.112 -  have wti: "wtl_inst (is ! pc) G rT (phi!pc) cert (length is) pc = Ok s''"
   1.113 +  have wti: "wtl_inst (is ! pc) G rT (phi!pc) cert (length is) pc = OK s''"
   1.114      by (auto simp add: wtl_cert_def split: if_splits option.splits)
   1.115  
   1.116    { fix pc'
   1.117 @@ -166,14 +166,14 @@
   1.118  
   1.119      with wti
   1.120      have less: "pc' < length is"  
   1.121 -      by (simp add: wtl_inst_Ok)
   1.122 +      by (simp add: wtl_inst_OK)
   1.123  
   1.124      have "G \<turnstile> step (is!pc) G (phi!pc) <=' phi ! pc'" 
   1.125      proof (cases "pc' = Suc pc")
   1.126        case False          
   1.127        with wti pc'
   1.128        have G: "G \<turnstile> step (is ! pc) G (phi ! pc) <=' cert ! pc'" 
   1.129 -        by (simp add: wtl_inst_Ok)
   1.130 +        by (simp add: wtl_inst_OK)
   1.131  
   1.132        hence "cert!pc' = None ==> step (is ! pc) G (phi ! pc) = None"
   1.133          by simp
   1.134 @@ -197,7 +197,7 @@
   1.135        case True
   1.136        with pc' wti
   1.137        have "step (is ! pc) G (phi ! pc) = s''"  
   1.138 -        by (simp add: wtl_inst_Ok)
   1.139 +        by (simp add: wtl_inst_OK)
   1.140        also
   1.141        from w c fits pc wtl 
   1.142        have "Suc pc < length is ==> G \<turnstile> s'' <=' phi ! Suc pc"
   1.143 @@ -213,7 +213,7 @@
   1.144    
   1.145    with wti
   1.146    show ?thesis
   1.147 -    by (auto simp add: wtl_inst_Ok wt_instr_def)
   1.148 +    by (auto simp add: wtl_inst_OK wt_instr_def)
   1.149  qed
   1.150  
   1.151  
   1.152 @@ -228,7 +228,7 @@
   1.153    assume pc:   "0 < length is"
   1.154  
   1.155    from wtl
   1.156 -  have wt0: "wtl_inst_list (take 0 is) G rT cert (length is) 0 s = Ok s"
   1.157 +  have wt0: "wtl_inst_list (take 0 is) G rT cert (length is) 0 s = OK s"
   1.158      by simp
   1.159    
   1.160    with fits pc
   1.161 @@ -244,7 +244,7 @@
   1.162      by (simp add: neq_Nil_conv) (elim, rule that)
   1.163    with wtl
   1.164    obtain s' where
   1.165 -    "wtl_cert x G rT s cert (length is) 0 = Ok s'"
   1.166 +    "wtl_cert x G rT s cert (length is) 0 = OK s'"
   1.167      by simp (elim, rule that, simp)
   1.168    hence 
   1.169      "!!t. cert!0 = Some t ==> G \<turnstile> s <=' cert!0"
   1.170 @@ -259,7 +259,7 @@
   1.171  lemma wtl_method_correct:
   1.172  "wtl_method G C pTs rT mxl ins cert ==> \<exists> phi. wt_method G C pTs rT mxl ins phi"
   1.173  proof (unfold wtl_method_def, simp only: Let_def, elim conjE)
   1.174 -  let "?s0" = "Some ([], Ok (Class C) # map Ok pTs @ replicate mxl Err)"
   1.175 +  let "?s0" = "Some ([], OK (Class C) # map OK pTs @ replicate mxl Err)"
   1.176    assume pc:  "0 < length ins"
   1.177    assume wtl: "wtl_inst_list ins G rT cert (length ins) 0 ?s0 \<noteq> Err"
   1.178