src/HOL/MicroJava/BV/BVSpec.thy
changeset 10042 7164dc0d24d8
parent 9757 1024a2d80ac0
child 10496 f2d304bdf3cc
     1.1 --- a/src/HOL/MicroJava/BV/BVSpec.thy	Wed Sep 20 21:20:41 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/BVSpec.thy	Thu Sep 21 10:42:49 2000 +0200
     1.3 @@ -11,53 +11,53 @@
     1.4  
     1.5  types
     1.6   method_type = "state_type option list"
     1.7 - class_type	 = "sig \<Rightarrow> method_type"
     1.8 - prog_type	 = "cname \<Rightarrow> class_type"
     1.9 + class_type	 = "sig => method_type"
    1.10 + prog_type	 = "cname => class_type"
    1.11  
    1.12  constdefs
    1.13 -wt_instr :: "[instr,jvm_prog,ty,method_type,p_count,p_count] \<Rightarrow> bool"
    1.14 -"wt_instr i G rT phi max_pc pc \<equiv> 
    1.15 +wt_instr :: "[instr,jvm_prog,ty,method_type,p_count,p_count] => bool"
    1.16 +"wt_instr i G rT phi max_pc pc == 
    1.17      app i G rT (phi!pc) \<and>
    1.18     (\<forall> pc' \<in> set (succs i pc). pc' < max_pc \<and> (G \<turnstile> step i G (phi!pc) <=' phi!pc'))"
    1.19  
    1.20 -wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \<Rightarrow> bool"
    1.21 -"wt_start G C pTs mxl phi \<equiv> 
    1.22 +wt_start :: "[jvm_prog,cname,ty list,nat,method_type] => bool"
    1.23 +"wt_start G C pTs mxl phi == 
    1.24      G \<turnstile> Some ([],(Ok (Class C))#((map Ok pTs))@(replicate mxl Err)) <=' phi!0"
    1.25  
    1.26  
    1.27 -wt_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,method_type] \<Rightarrow> bool"
    1.28 -"wt_method G C pTs rT mxl ins phi \<equiv>
    1.29 +wt_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,method_type] => bool"
    1.30 +"wt_method G C pTs rT mxl ins phi ==
    1.31  	let max_pc = length ins
    1.32          in
    1.33  	0 < max_pc \<and> wt_start G C pTs mxl phi \<and> 
    1.34 -	(\<forall>pc. pc<max_pc \<longrightarrow> wt_instr (ins ! pc) G rT phi max_pc pc)"
    1.35 +	(\<forall>pc. pc<max_pc --> wt_instr (ins ! pc) G rT phi max_pc pc)"
    1.36  
    1.37 -wt_jvm_prog :: "[jvm_prog,prog_type] \<Rightarrow> bool"
    1.38 -"wt_jvm_prog G phi \<equiv>
    1.39 +wt_jvm_prog :: "[jvm_prog,prog_type] => bool"
    1.40 +"wt_jvm_prog G phi ==
    1.41     wf_prog (\<lambda>G C (sig,rT,maxl,b).
    1.42                wt_method G C (snd sig) rT maxl b (phi C sig)) G"
    1.43  
    1.44  
    1.45  
    1.46  lemma wt_jvm_progD:
    1.47 -"wt_jvm_prog G phi \<Longrightarrow> (\<exists>wt. wf_prog wt G)"
    1.48 +"wt_jvm_prog G phi ==> (\<exists>wt. wf_prog wt G)"
    1.49  by (unfold wt_jvm_prog_def, blast)
    1.50  
    1.51  lemma wt_jvm_prog_impl_wt_instr:
    1.52 -"\<lbrakk> wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins); pc < length ins \<rbrakk> 
    1.53 - \<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc";
    1.54 +"[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins); pc < length ins |] 
    1.55 + ==> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc";
    1.56  by (unfold wt_jvm_prog_def, drule method_wf_mdecl, 
    1.57      simp, simp add: wf_mdecl_def wt_method_def)
    1.58  
    1.59  lemma wt_jvm_prog_impl_wt_start:
    1.60 -"\<lbrakk> wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins) \<rbrakk> \<Longrightarrow> 
    1.61 +"[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins) |] ==> 
    1.62   0 < (length ins) \<and> wt_start G C (snd sig) maxl (phi C sig)"
    1.63  by (unfold wt_jvm_prog_def, drule method_wf_mdecl, 
    1.64      simp, simp add: wf_mdecl_def wt_method_def)
    1.65  
    1.66  (* for most instructions wt_instr collapses: *)
    1.67  lemma  
    1.68 -"succs i pc = [pc+1] \<Longrightarrow> wt_instr i G rT phi max_pc pc = 
    1.69 +"succs i pc = [pc+1] ==> wt_instr i G rT phi max_pc pc = 
    1.70   (app i G rT (phi!pc) \<and> pc+1 < max_pc \<and> (G \<turnstile> step i G (phi!pc) <=' phi!(pc+1)))"
    1.71  by (simp add: wt_instr_def) 
    1.72