src/HOL/MicroJava/BV/LBVSpec.thy
changeset 10042 7164dc0d24d8
parent 9757 1024a2d80ac0
child 10496 f2d304bdf3cc
     1.1 --- a/src/HOL/MicroJava/BV/LBVSpec.thy	Wed Sep 20 21:20:41 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/LBVSpec.thy	Thu Sep 21 10:42:49 2000 +0200
     1.3 @@ -11,44 +11,36 @@
     1.4  
     1.5  types
     1.6    certificate       = "state_type option list" 
     1.7 -  class_certificate = "sig \<Rightarrow> certificate"
     1.8 -  prog_certificate  = "cname \<Rightarrow> class_certificate"
     1.9 +  class_certificate = "sig => certificate"
    1.10 +  prog_certificate  = "cname => class_certificate"
    1.11  
    1.12  
    1.13  constdefs
    1.14    check_cert :: "[instr, jvm_prog, state_type option, certificate, p_count, p_count]
    1.15 -                 \<Rightarrow> bool"
    1.16 -  "check_cert i G s cert pc max_pc \<equiv> \<forall>pc' \<in> set (succs i pc). pc' < max_pc \<and>  
    1.17 -                                     (pc' \<noteq> pc+1 \<longrightarrow> G \<turnstile> step i G s <=' cert!pc')"
    1.18 +                 => bool"
    1.19 +  "check_cert i G s cert pc max_pc == \<forall>pc' \<in> set (succs i pc). pc' < max_pc \<and>  
    1.20 +                                     (pc' \<noteq> pc+1 --> G \<turnstile> step i G s <=' cert!pc')"
    1.21  
    1.22    wtl_inst :: "[instr,jvm_prog,ty,state_type option,certificate,p_count,p_count] 
    1.23 -               \<Rightarrow> state_type option err" 
    1.24 -  "wtl_inst i G rT s cert max_pc pc \<equiv> 
    1.25 +               => state_type option err" 
    1.26 +  "wtl_inst i G rT s cert max_pc pc == 
    1.27       if app i G rT s \<and> check_cert i G s cert pc max_pc then 
    1.28         if pc+1 mem (succs i pc) then Ok (step i G s) else Ok (cert!(pc+1))
    1.29       else Err";
    1.30  
    1.31 -lemma wtl_inst_Ok:
    1.32 -"(wtl_inst i G rT s cert max_pc pc = Ok s') =
    1.33 - (app i G rT s \<and> (\<forall>pc' \<in> set (succs i pc). 
    1.34 -                   pc' < max_pc \<and> (pc' \<noteq> pc+1 \<longrightarrow> G \<turnstile> step i G s <=' cert!pc')) \<and> 
    1.35 - (if pc+1 \<in> set (succs i pc) then s' = step i G s else s' = cert!(pc+1)))"
    1.36 -  by (auto simp add: wtl_inst_def check_cert_def set_mem_eq);
    1.37 -
    1.38 -
    1.39  constdefs
    1.40    wtl_cert :: "[instr,jvm_prog,ty,state_type option,certificate,p_count,p_count] 
    1.41 -               \<Rightarrow> state_type option err"  
    1.42 -  "wtl_cert i G rT s cert max_pc pc \<equiv>
    1.43 +               => state_type option err"  
    1.44 +  "wtl_cert i G rT s cert max_pc pc ==
    1.45       case cert!pc of
    1.46 -        None    \<Rightarrow> wtl_inst i G rT s cert max_pc pc
    1.47 -      | Some s' \<Rightarrow> if G \<turnstile> s <=' (Some s') then 
    1.48 +        None    => wtl_inst i G rT s cert max_pc pc
    1.49 +      | Some s' => if G \<turnstile> s <=' (Some s') then 
    1.50                      wtl_inst i G rT (Some s') cert max_pc pc 
    1.51                    else Err"
    1.52  
    1.53  consts 
    1.54    wtl_inst_list :: "[instr list,jvm_prog,ty,certificate,p_count,p_count, 
    1.55 -                     state_type option] \<Rightarrow> state_type option err"
    1.56 +                     state_type option] => state_type option err"
    1.57  primrec
    1.58    "wtl_inst_list []     G rT cert max_pc pc s = Ok s"
    1.59    "wtl_inst_list (i#is) G rT cert max_pc pc s = 
    1.60 @@ -57,19 +49,26 @@
    1.61                
    1.62  
    1.63  constdefs
    1.64 - wtl_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,certificate] \<Rightarrow> bool"  
    1.65 - "wtl_method G C pTs rT mxl ins cert \<equiv>  
    1.66 + wtl_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,certificate] => bool"  
    1.67 + "wtl_method G C pTs rT mxl ins cert ==  
    1.68  	let max_pc = length ins  
    1.69    in 
    1.70    0 < max_pc \<and>   
    1.71    wtl_inst_list ins G rT cert max_pc 0 
    1.72                  (Some ([],(Ok (Class C))#((map Ok pTs))@(replicate mxl Err))) \<noteq> Err"
    1.73  
    1.74 - wtl_jvm_prog :: "[jvm_prog,prog_certificate] \<Rightarrow> bool" 
    1.75 - "wtl_jvm_prog G cert \<equiv>  
    1.76 + wtl_jvm_prog :: "[jvm_prog,prog_certificate] => bool" 
    1.77 + "wtl_jvm_prog G cert ==  
    1.78    wf_prog (\<lambda>G C (sig,rT,maxl,b). wtl_method G C (snd sig) rT maxl b (cert C sig)) G"
    1.79  
    1.80 -text {* \medskip *} 
    1.81 +
    1.82 +
    1.83 +lemma wtl_inst_Ok:
    1.84 +"(wtl_inst i G rT s cert max_pc pc = Ok s') =
    1.85 + (app i G rT s \<and> (\<forall>pc' \<in> set (succs i pc). 
    1.86 +                   pc' < max_pc \<and> (pc' \<noteq> pc+1 --> G \<turnstile> step i G s <=' cert!pc')) \<and> 
    1.87 + (if pc+1 \<in> set (succs i pc) then s' = step i G s else s' = cert!(pc+1)))"
    1.88 +  by (auto simp add: wtl_inst_def check_cert_def set_mem_eq);
    1.89  
    1.90  lemma strict_Some [simp]: 
    1.91  "(strict f x = Ok y) = (\<exists> z. x = Ok z \<and> f z = Ok y)"
    1.92 @@ -127,7 +126,7 @@
    1.93  qed
    1.94  
    1.95  lemma take_Suc:
    1.96 -  "\<forall>n. n < length l \<longrightarrow> take (Suc n) l = (take n l)@[l!n]" (is "?P l")
    1.97 +  "\<forall>n. n < length l --> take (Suc n) l = (take n l)@[l!n]" (is "?P l")
    1.98  proof (induct l)
    1.99    show "?P []" by simp
   1.100  
   1.101 @@ -191,4 +190,14 @@
   1.102      by (auto simp add: wtl_append min_def)
   1.103  qed
   1.104  
   1.105 +lemma unique_set:
   1.106 +"(a,b,c,d)\<in>set l --> unique l --> (a',b',c',d') \<in> set l --> 
   1.107 +  a = a' --> b=b' \<and> c=c' \<and> d=d'"
   1.108 +  by (induct "l") auto
   1.109 +
   1.110 +lemma unique_epsilon:
   1.111 +  "(a,b,c,d)\<in>set l --> unique l --> 
   1.112 +  (SOME (a',b',c',d'). (a',b',c',d') \<in> set l \<and> a'=a) = (a,b,c,d)"
   1.113 +  by (auto simp add: unique_set)
   1.114 +
   1.115  end