src/HOL/MicroJava/BV/LBVComplete.thy
changeset 10042 7164dc0d24d8
parent 9941 fe05af7ec816
child 10496 f2d304bdf3cc
     1.1 --- a/src/HOL/MicroJava/BV/LBVComplete.thy	Wed Sep 20 21:20:41 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Thu Sep 21 10:42:49 2000 +0200
     1.3 @@ -9,30 +9,30 @@
     1.4  theory LBVComplete = BVSpec + LBVSpec + StepMono:
     1.5  
     1.6  constdefs
     1.7 -  contains_targets :: "[instr list, certificate, method_type, p_count] \<Rightarrow> bool"
     1.8 -  "contains_targets ins cert phi pc \<equiv> 
     1.9 +  contains_targets :: "[instr list, certificate, method_type, p_count] => bool"
    1.10 +  "contains_targets ins cert phi pc == 
    1.11       \<forall>pc' \<in> set (succs (ins!pc) pc). 
    1.12 -      pc' \<noteq> pc+1 \<and> pc' < length ins \<longrightarrow> cert!pc' = phi!pc'"
    1.13 +      pc' \<noteq> pc+1 \<and> pc' < length ins --> cert!pc' = phi!pc'"
    1.14  
    1.15 -  fits :: "[instr list, certificate, method_type] \<Rightarrow> bool"
    1.16 -  "fits ins cert phi \<equiv> \<forall>pc. pc < length ins \<longrightarrow> 
    1.17 +  fits :: "[instr list, certificate, method_type] => bool"
    1.18 +  "fits ins cert phi == \<forall>pc. pc < length ins --> 
    1.19                         contains_targets ins cert phi pc \<and>
    1.20                         (cert!pc = None \<or> cert!pc = phi!pc)"
    1.21  
    1.22 -  is_target :: "[instr list, p_count] \<Rightarrow> bool" 
    1.23 -  "is_target ins pc \<equiv> 
    1.24 +  is_target :: "[instr list, p_count] => bool" 
    1.25 +  "is_target ins pc == 
    1.26       \<exists>pc'. pc \<noteq> pc'+1 \<and> pc' < length ins \<and> pc \<in> set (succs (ins!pc') pc')"
    1.27  
    1.28  
    1.29  constdefs 
    1.30 -  make_cert :: "[instr list, method_type] \<Rightarrow> certificate"
    1.31 -  "make_cert ins phi \<equiv> 
    1.32 +  make_cert :: "[instr list, method_type] => certificate"
    1.33 +  "make_cert ins phi == 
    1.34       map (\<lambda>pc. if is_target ins pc then phi!pc else None) [0..length ins(]"
    1.35  
    1.36 -  make_Cert :: "[jvm_prog, prog_type] \<Rightarrow> prog_certificate"
    1.37 -  "make_Cert G Phi \<equiv>  \<lambda> C sig.
    1.38 -     let (C,x,y,mdecls)  = \<epsilon> (Cl,x,y,mdecls). (Cl,x,y,mdecls) \<in> set G \<and> Cl = C;
    1.39 -         (sig,rT,maxl,b) = \<epsilon> (sg,rT,maxl,b). (sg,rT,maxl,b) \<in> set mdecls \<and> sg = sig
    1.40 +  make_Cert :: "[jvm_prog, prog_type] => prog_certificate"
    1.41 +  "make_Cert G Phi ==  \<lambda> C sig.
    1.42 +     let (C,x,y,mdecls)  = SOME (Cl,x,y,mdecls). (Cl,x,y,mdecls) \<in> set G \<and> Cl = C;
    1.43 +         (sig,rT,maxl,b) = SOME (sg,rT,maxl,b). (sg,rT,maxl,b) \<in> set mdecls \<and> sg = sig
    1.44       in make_cert b (Phi C sig)"
    1.45    
    1.46  
    1.47 @@ -197,14 +197,14 @@
    1.48    have app: "app (ins!pc) G rT (phi!pc)" by (simp add: wt_instr_def)
    1.49  
    1.50    from wt pc
    1.51 -  have pc': "\<And>pc'. pc' \<in> set (succs (ins!pc) pc) ==> pc' < length ins"
    1.52 +  have pc': "!!pc'. pc' \<in> set (succs (ins!pc) pc) ==> pc' < length ins"
    1.53      by (simp add: wt_instr_def)
    1.54  
    1.55    let ?s' = "step (ins!pc) G (phi!pc)"
    1.56  
    1.57    from wt fits pc
    1.58 -  have cert: "!!pc'. \<lbrakk>pc' \<in> set (succs (ins!pc) pc); pc' < max_pc; pc' \<noteq> pc+1\<rbrakk> 
    1.59 -    \<Longrightarrow> G \<turnstile> ?s' <=' cert!pc'"
    1.60 +  have cert: "!!pc'. [|pc' \<in> set (succs (ins!pc) pc); pc' < max_pc; pc' \<noteq> pc+1|] 
    1.61 +    ==> G \<turnstile> ?s' <=' cert!pc'"
    1.62      by (auto dest: fitsD simp add: wt_instr_def)     
    1.63  
    1.64    from app pc cert pc'
    1.65 @@ -324,14 +324,14 @@
    1.66  *}
    1.67  
    1.68  theorem wt_imp_wtl_inst_list:
    1.69 -"\<forall> pc. (\<forall>pc'. pc' < length all_ins \<longrightarrow> 
    1.70 -        wt_instr (all_ins ! pc') G rT phi (length all_ins) pc') \<longrightarrow>
    1.71 -       fits all_ins cert phi \<longrightarrow> 
    1.72 -       (\<exists>l. pc = length l \<and> all_ins = l@ins) \<longrightarrow>  
    1.73 -       pc < length all_ins \<longrightarrow>      
    1.74 -       (\<forall> s. (G \<turnstile> s <=' (phi!pc)) \<longrightarrow> 
    1.75 +"\<forall> pc. (\<forall>pc'. pc' < length all_ins --> 
    1.76 +        wt_instr (all_ins ! pc') G rT phi (length all_ins) pc') -->
    1.77 +       fits all_ins cert phi --> 
    1.78 +       (\<exists>l. pc = length l \<and> all_ins = l@ins) -->  
    1.79 +       pc < length all_ins -->      
    1.80 +       (\<forall> s. (G \<turnstile> s <=' (phi!pc)) --> 
    1.81               wtl_inst_list ins G rT cert (length all_ins) pc s \<noteq> Err)" 
    1.82 -(is "\<forall>pc. ?wt \<longrightarrow> ?fits \<longrightarrow> ?l pc ins \<longrightarrow> ?len pc \<longrightarrow> ?wtl pc ins"  
    1.83 +(is "\<forall>pc. ?wt --> ?fits --> ?l pc ins --> ?len pc --> ?wtl pc ins"  
    1.84   is "\<forall>pc. ?C pc ins" is "?P ins") 
    1.85  proof (induct "?P" "ins")
    1.86    case Nil
    1.87 @@ -343,7 +343,7 @@
    1.88    show "?P (i#ins')" 
    1.89    proof (intro allI impI, elim exE conjE)
    1.90      fix pc s l
    1.91 -    assume wt  : "\<forall>pc'. pc' < length all_ins \<longrightarrow> 
    1.92 +    assume wt  : "\<forall>pc'. pc' < length all_ins --> 
    1.93                          wt_instr (all_ins ! pc') G rT phi (length all_ins) pc'"
    1.94      assume fits: "fits all_ins cert phi"
    1.95      assume l   : "pc < length all_ins"
    1.96 @@ -362,7 +362,7 @@
    1.97      from Cons
    1.98      have "?C (Suc pc) ins'" by blast
    1.99      with wt fits pc
   1.100 -    have IH: "?len (Suc pc) \<longrightarrow> ?wtl (Suc pc) ins'" by auto
   1.101 +    have IH: "?len (Suc pc) --> ?wtl (Suc pc) ins'" by auto
   1.102  
   1.103      show "wtl_inst_list (i#ins') G rT cert (length all_ins) pc s \<noteq> Err" 
   1.104      proof (cases "?len (Suc pc)")
   1.105 @@ -422,20 +422,10 @@
   1.106      by (rule fits_imp_wtl_method_complete)
   1.107  qed
   1.108  
   1.109 -lemma unique_set:
   1.110 -"(a,b,c,d)\<in>set l \<longrightarrow> unique l \<longrightarrow> (a',b',c',d') \<in> set l \<longrightarrow> 
   1.111 -  a = a' \<longrightarrow> b=b' \<and> c=c' \<and> d=d'"
   1.112 -  by (induct "l") auto
   1.113 -
   1.114 -lemma unique_epsilon:
   1.115 -  "(a,b,c,d)\<in>set l \<longrightarrow> unique l \<longrightarrow> 
   1.116 -  (\<epsilon> (a',b',c',d'). (a',b',c',d') \<in> set l \<and> a'=a) = (a,b,c,d)"
   1.117 -  by (auto simp add: unique_set)
   1.118 -
   1.119  
   1.120  theorem wtl_complete: 
   1.121    "wt_jvm_prog G Phi ==> wtl_jvm_prog G (make_Cert G Phi)"
   1.122 -proof (simp only: wt_jvm_prog_def)
   1.123 +proof (unfold wt_jvm_prog_def)
   1.124  
   1.125    assume wfprog: 
   1.126      "wf_prog (\<lambda>G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) G"
   1.127 @@ -449,12 +439,12 @@
   1.128               (\<forall>(sig,rT,mb)\<in>set ms. wf_mhead G sig rT \<and> 
   1.129                 (\<lambda>(maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) mb) \<and>
   1.130               unique ms \<and>
   1.131 -             (case sc of None \<Rightarrow> C = Object
   1.132 -              | Some D \<Rightarrow>
   1.133 +             (case sc of None => C = Object
   1.134 +              | Some D =>
   1.135                    is_class G D \<and>
   1.136                    (D, C) \<notin> (subcls1 G)^* \<and>
   1.137                    (\<forall>(sig,rT,b)\<in>set ms. 
   1.138 -                   \<forall>D' rT' b'. method (G, D) sig = Some (D', rT', b') \<longrightarrow> G\<turnstile>rT\<preceq>rT'))"
   1.139 +                   \<forall>D' rT' b'. method (G, D) sig = Some (D', rT', b') --> G\<turnstile>rT\<preceq>rT'))"
   1.140               "(a, aa, ab, b) \<in> set G"
   1.141    
   1.142      assume uG : "unique G"