src/HOL/MicroJava/BV/BVSpec.thy
changeset 10629 d790faef9c07
parent 10612 779af7c58743
child 10638 17063aee1d86
equal deleted inserted replaced
10628:4ea7f3e8e471 10629:d790faef9c07
    36 
    36 
    37 lemma wt_jvm_progD:
    37 lemma wt_jvm_progD:
    38 "wt_jvm_prog G phi ==> (\<exists>wt. wf_prog wt G)"
    38 "wt_jvm_prog G phi ==> (\<exists>wt. wf_prog wt G)"
    39 by (unfold wt_jvm_prog_def, blast)
    39 by (unfold wt_jvm_prog_def, blast)
    40 
    40 
    41 lemma wt_jvm_prog_impl_wt_instr: (* DvO: is_class G C eingefügt *)
    41 lemma wt_jvm_prog_impl_wt_instr:
    42 "[| wt_jvm_prog G phi; is_class G C;
    42 "[| wt_jvm_prog G phi; is_class G C;
    43     method (G,C) sig = Some (C,rT,maxs,maxl,ins); pc < length ins |] 
    43     method (G,C) sig = Some (C,rT,maxs,maxl,ins); pc < length ins |] 
    44  ==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc";
    44  ==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc";
    45 by (unfold wt_jvm_prog_def, drule method_wf_mdecl, 
    45 by (unfold wt_jvm_prog_def, drule method_wf_mdecl, 
    46     simp, simp, simp add: wf_mdecl_def wt_method_def)
    46     simp, simp, simp add: wf_mdecl_def wt_method_def)
    47 
    47 
    48 lemma wt_jvm_prog_impl_wt_start: (* DvO: is_class G C eingefügt *)
    48 lemma wt_jvm_prog_impl_wt_start:
    49 "[| wt_jvm_prog G phi; is_class G C;
    49 "[| wt_jvm_prog G phi; is_class G C;
    50     method (G,C) sig = Some (C,rT,maxs,maxl,ins) |] ==> 
    50     method (G,C) sig = Some (C,rT,maxs,maxl,ins) |] ==> 
    51  0 < (length ins) \<and> wt_start G C (snd sig) maxl (phi C sig)"
    51  0 < (length ins) \<and> wt_start G C (snd sig) maxl (phi C sig)"
    52 by (unfold wt_jvm_prog_def, drule method_wf_mdecl, 
    52 by (unfold wt_jvm_prog_def, drule method_wf_mdecl, 
    53     simp, simp, simp add: wf_mdecl_def wt_method_def)
    53     simp, simp, simp add: wf_mdecl_def wt_method_def)