src/HOL/MicroJava/BV/LBVCorrect.thy
changeset 10042 7164dc0d24d8
parent 9970 dfe4747c8318
child 10496 f2d304bdf3cc
     1.1 --- a/src/HOL/MicroJava/BV/LBVCorrect.thy	Wed Sep 20 21:20:41 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/LBVCorrect.thy	Thu Sep 21 10:42:49 2000 +0200
     1.3 @@ -11,31 +11,31 @@
     1.4  lemmas [simp del] = split_paired_Ex split_paired_All
     1.5  
     1.6  constdefs
     1.7 -fits :: "[method_type,instr list,jvm_prog,ty,state_type option,certificate] \<Rightarrow> bool"
     1.8 -"fits phi is G rT s0 cert \<equiv> 
     1.9 -  (\<forall>pc s1. pc < length is \<longrightarrow>
    1.10 -    (wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1 \<longrightarrow>
    1.11 -    (case cert!pc of None   \<Rightarrow> phi!pc = s1
    1.12 -                   | Some t \<Rightarrow> phi!pc = Some t)))"
    1.13 +fits :: "[method_type,instr list,jvm_prog,ty,state_type option,certificate] => bool"
    1.14 +"fits phi is G rT s0 cert == 
    1.15 +  (\<forall>pc s1. pc < length is -->
    1.16 +    (wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1 -->
    1.17 +    (case cert!pc of None   => phi!pc = s1
    1.18 +                   | Some t => phi!pc = Some t)))"
    1.19  
    1.20  constdefs
    1.21 -make_phi :: "[instr list,jvm_prog,ty,state_type option,certificate] \<Rightarrow> method_type"
    1.22 -"make_phi is G rT s0 cert \<equiv> 
    1.23 +make_phi :: "[instr list,jvm_prog,ty,state_type option,certificate] => method_type"
    1.24 +"make_phi is G rT s0 cert == 
    1.25     map (\<lambda>pc. case cert!pc of 
    1.26 -               None   \<Rightarrow> val (wtl_inst_list (take pc is) G rT cert (length is) 0 s0) 
    1.27 -             | Some t \<Rightarrow> Some t) [0..length is(]"
    1.28 +               None   => val (wtl_inst_list (take pc is) G rT cert (length is) 0 s0) 
    1.29 +             | Some t => Some t) [0..length is(]"
    1.30  
    1.31  
    1.32  lemma fitsD_None:
    1.33 -  "\<lbrakk>fits phi is G rT s0 cert; pc < length is;
    1.34 +  "[|fits phi is G rT s0 cert; pc < length is;
    1.35      wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1; 
    1.36 -    cert ! pc = None\<rbrakk> \<Longrightarrow> phi!pc = s1"
    1.37 +    cert ! pc = None|] ==> phi!pc = s1"
    1.38    by (auto simp add: fits_def)
    1.39  
    1.40  lemma fitsD_Some:
    1.41 -  "\<lbrakk>fits phi is G rT s0 cert; pc < length is;
    1.42 +  "[|fits phi is G rT s0 cert; pc < length is;
    1.43      wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1; 
    1.44 -    cert ! pc = Some t\<rbrakk> \<Longrightarrow> phi!pc = Some t"
    1.45 +    cert ! pc = Some t|] ==> phi!pc = Some t"
    1.46    by (auto simp add: fits_def)
    1.47  
    1.48  lemma make_phi_Some:
    1.49 @@ -62,7 +62,7 @@
    1.50    
    1.51  lemma fits_lemma1:
    1.52    "[| wtl_inst_list is G rT cert (length is) 0 s = Ok s'; fits phi is G rT s cert |]
    1.53 -  ==> \<forall>pc t. pc < length is \<longrightarrow> cert!pc = Some t \<longrightarrow> phi!pc = Some t"
    1.54 +  ==> \<forall>pc t. pc < length is --> cert!pc = Some t --> phi!pc = Some t"
    1.55  proof (intro strip)
    1.56    fix pc t 
    1.57    assume "wtl_inst_list is G rT cert (length is) 0 s = Ok s'"
    1.58 @@ -114,11 +114,11 @@
    1.59      "wtl_cert l G rT s'' cert (length is) (Suc pc) = Ok x"
    1.60      by (auto simp add: wtl_append min_def simp del: append_take_drop_id)
    1.61  
    1.62 -  hence c1: "\<And>t. cert!Suc pc = Some t ==> G \<turnstile> s'' <=' cert!Suc pc"
    1.63 +  hence c1: "!!t. cert!Suc pc = Some t ==> G \<turnstile> s'' <=' cert!Suc pc"
    1.64      by (simp add: wtl_cert_def split: if_splits)
    1.65    moreover
    1.66    from fits pc wts
    1.67 -  have c2: "\<And>t. cert!Suc pc = Some t ==> phi!Suc pc = cert!Suc pc"
    1.68 +  have c2: "!!t. cert!Suc pc = Some t ==> phi!Suc pc = cert!Suc pc"
    1.69      by - (drule fitsD_Some, auto)
    1.70    moreover
    1.71    from fits pc wts
    1.72 @@ -150,7 +150,7 @@
    1.73  
    1.74    from fits wtl pc
    1.75    have cert_Some: 
    1.76 -    "\<And>t pc. [| pc < length is; cert!pc = Some t |] ==> phi!pc = Some t"
    1.77 +    "!!t pc. [| pc < length is; cert!pc = Some t |] ==> phi!pc = Some t"
    1.78      by (auto dest: fits_lemma1)
    1.79    
    1.80    from fits wtl pc
    1.81 @@ -236,7 +236,7 @@
    1.82      by (rule fitsD_None)
    1.83    moreover    
    1.84    from fits pc wt0
    1.85 -  have "\<And>t. cert!0 = Some t ==> phi!0 = cert!0"
    1.86 +  have "!!t. cert!0 = Some t ==> phi!0 = cert!0"
    1.87      by - (drule fitsD_Some, auto)
    1.88    moreover
    1.89    from pc
    1.90 @@ -247,7 +247,7 @@
    1.91      "wtl_cert x G rT s cert (length is) 0 = Ok s'"
    1.92      by simp (elim, rule that, simp)
    1.93    hence 
    1.94 -    "\<And>t. cert!0 = Some t ==> G \<turnstile> s <=' cert!0"
    1.95 +    "!!t. cert!0 = Some t ==> G \<turnstile> s <=' cert!0"
    1.96      by (simp add: wtl_cert_def split: if_splits)
    1.97  
    1.98    ultimately
    1.99 @@ -268,7 +268,7 @@
   1.100  
   1.101    with wtl
   1.102    have allpc:
   1.103 -    "\<forall>pc. pc < length ins \<longrightarrow> wt_instr (ins ! pc) G rT phi (length ins) pc"
   1.104 +    "\<forall>pc. pc < length ins --> wt_instr (ins ! pc) G rT phi (length ins) pc"
   1.105      by (blast intro: wtl_fits_wt)
   1.106  
   1.107    from pc wtl fits
   1.108 @@ -279,15 +279,6 @@
   1.109    show ?thesis by (auto simp add: wt_method_def)
   1.110  qed
   1.111  
   1.112 -lemma unique_set:
   1.113 -  "(a,b,c,d)\<in>set l \<longrightarrow> unique l \<longrightarrow> (a',b',c',d') \<in> set l \<longrightarrow> 
   1.114 -   a = a' \<longrightarrow> b=b' \<and> c=c' \<and> d=d'"
   1.115 -  by (induct "l") auto
   1.116 -
   1.117 -lemma unique_epsilon:
   1.118 -  "(a,b,c,d)\<in>set l \<longrightarrow> unique l \<longrightarrow> 
   1.119 -   (\<epsilon> (a',b',c',d'). (a',b',c',d') \<in> set l \<and> a'=a) = (a,b,c,d)"
   1.120 -  by (auto simp add: unique_set)
   1.121  
   1.122  theorem wtl_correct:
   1.123  "wtl_jvm_prog G cert ==> \<exists> Phi. wt_jvm_prog G Phi"
   1.124 @@ -304,9 +295,9 @@
   1.125      (is "\<exists>Phi. ?Q Phi")
   1.126    proof (intro exI)
   1.127      let "?Phi" = "\<lambda> C sig. 
   1.128 -      let (C,x,y,mdecls) = \<epsilon> (Cl,x,y,mdecls). (Cl,x,y,mdecls) \<in> set G \<and> Cl = C;
   1.129 -          (sig,rT,maxl,b) = \<epsilon> (sg,rT,maxl,b). (sg,rT,maxl,b) \<in> set mdecls \<and> sg = sig
   1.130 -      in \<epsilon> phi. wt_method G C (snd sig) rT maxl b phi"
   1.131 +      let (C,x,y,mdecls) = SOME (Cl,x,y,mdecls). (Cl,x,y,mdecls) \<in> set G \<and> Cl = C;
   1.132 +          (sig,rT,maxl,b) = SOME (sg,rT,maxl,b). (sg,rT,maxl,b) \<in> set mdecls \<and> sg = sig
   1.133 +      in SOME phi. wt_method G C (snd sig) rT maxl b phi"
   1.134      from wtl_prog
   1.135      show "?Q ?Phi"
   1.136      proof (unfold wf_cdecl_def, intro)
   1.137 @@ -328,8 +319,8 @@
   1.138                wt_method G a (snd sig) rT maxl b 
   1.139                 ((\<lambda>(C,x,y,mdecls).
   1.140                      (\<lambda>(sig,rT,maxl,b). Eps (wt_method G C (snd sig) rT maxl b))
   1.141 -                     (\<epsilon>(sg,rT,maxl,b). (sg, rT, maxl, b) \<in> set mdecls \<and> sg = sig))
   1.142 -                 (\<epsilon>(Cl,x,y,mdecls). (Cl, x, y, mdecls) \<in> set G \<and> Cl = a))) mb) m"
   1.143 +                     (SOME (sg,rT,maxl,b). (sg, rT, maxl, b) \<in> set mdecls \<and> sg = sig))
   1.144 +                 (SOME (Cl,x,y,mdecls). (Cl, x, y, mdecls) \<in> set G \<and> Cl = a))) mb) m"
   1.145            by - (drule bspec, assumption, 
   1.146                  clarsimp dest!: wtl_method_correct,
   1.147                  clarsimp intro!: someI simp add: unique_epsilon)