src/HOL/MicroJava/BV/BVNoTypeError.thy
changeset 59682 d662d096f72b
parent 58886 8a6cac7c7247
child 61361 8b5f00202e1a
     1.1 --- a/src/HOL/MicroJava/BV/BVNoTypeError.thy	Tue Mar 10 23:04:40 2015 +0100
     1.2 +++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy	Thu Mar 12 14:58:32 2015 +0100
     1.3 @@ -429,14 +429,14 @@
     1.4    fixes G ("\<Gamma>") and Phi ("\<Phi>")
     1.5    assumes wt: "wt_jvm_prog \<Gamma> \<Phi>"  
     1.6    assumes is_class: "is_class \<Gamma> C"
     1.7 -    and method: "method (\<Gamma>,C) (m,[]) = Some (C, b)"
     1.8 +    and "method": "method (\<Gamma>,C) (m,[]) = Some (C, b)"
     1.9      and m: "m \<noteq> init"
    1.10    defines start: "s \<equiv> start_state \<Gamma> C m"
    1.11  
    1.12    assumes s: "\<Gamma> \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> t" 
    1.13    shows "t \<noteq> TypeError"
    1.14  proof -
    1.15 -  from wt is_class method have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
    1.16 +  from wt is_class "method" have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
    1.17      unfolding start by (rule BV_correct_initial)
    1.18    from wt this s show ?thesis by (rule no_type_errors)
    1.19  qed
    1.20 @@ -461,12 +461,12 @@
    1.21    fixes G ("\<Gamma>") and Phi ("\<Phi>")
    1.22    assumes wt: "wt_jvm_prog \<Gamma> \<Phi>"  
    1.23    assumes is_class: "is_class \<Gamma> C"
    1.24 -    and method: "method (\<Gamma>,C) (m,[]) = Some (C, b)"
    1.25 +    and "method": "method (\<Gamma>,C) (m,[]) = Some (C, b)"
    1.26      and m: "m \<noteq> init"
    1.27    defines start: "s \<equiv> start_state \<Gamma> C m"
    1.28    shows "\<Gamma> \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> (Normal t) = \<Gamma> \<turnstile> s \<midarrow>jvm\<rightarrow> t"
    1.29  proof -
    1.30 -  from wt is_class method have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
    1.31 +  from wt is_class "method" have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
    1.32      unfolding start by (rule BV_correct_initial)
    1.33    with wt show ?thesis by (rule welltyped_commutes)
    1.34  qed