1.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy	Fri Aug 08 14:54:37 2003 +0200
     1.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Fri Aug 08 14:57:46 2003 +0200
     1.3 @@ -373,27 +373,27 @@
     1.4  Unify.trace_bound  := 20
     1.5  *}
     1.6  
     1.7 +
     1.8  lemma eval_type_sound: "!!E s s'.  
     1.9 -  [| G=prg E; wf_java_prog G; G\<turnstile>(x,s) -e\<succ>v -> (x',s'); (x,s)::\<preceq>E; E\<turnstile>e::T |]  
    1.10 -  ==> (x',s')::\<preceq>E \<and> (x'=None --> G,heap s'\<turnstile>v::\<preceq>T)"
    1.11 -apply( simp (no_asm_simp) only: split_tupled_all)
    1.12 -apply (drule eval_evals_exec_type_sound 
    1.13 -             [THEN conjunct1, THEN mp, THEN spec, THEN mp])
    1.14 +  [| wf_java_prog G; G\<turnstile>(x,s) -e\<succ>v -> (x',s'); (x,s)::\<preceq>E; E\<turnstile>e::T; G=prg E |]  
    1.15 +  ==> (x',s')::\<preceq>E \<and> (x'=None --> G,heap s'\<turnstile>v::\<preceq>T) \<and> heap s \<le>| heap s'"
    1.16 +apply (simp (no_asm_simp) only: split_tupled_all)
    1.17 +apply (drule eval_evals_exec_type_sound [THEN conjunct1, THEN mp, THEN spec, THEN mp])
    1.18  apply auto
    1.19  done
    1.20  
    1.21 +
    1.22  lemma evals_type_sound: "!!E s s'.  
    1.23 -  [| G\<turnstile>(x,s) -es[\<succ>]vs -> (x',s'); G=prg E; wf_java_prog G; (x,s)::\<preceq>E; E\<turnstile>es[::]Ts |]  
    1.24 -  ==> (x',s')::\<preceq>E \<and> (x'=None --> list_all2 (conf G (heap s')) vs Ts)"
    1.25 -apply( simp (no_asm_simp) only: split_tupled_all)
    1.26 -apply (drule eval_evals_exec_type_sound 
    1.27 -             [THEN conjunct2, THEN conjunct1, THEN mp, THEN spec, THEN mp])
    1.28 +  [| wf_java_prog G; G\<turnstile>(x,s) -es[\<succ>]vs -> (x',s'); (x,s)::\<preceq>E; E\<turnstile>es[::]Ts; G=prg E |]  
    1.29 +  ==> (x',s')::\<preceq>E \<and> (x'=None --> (list_all2 (\<lambda>v T. G,heap s'\<turnstile>v::\<preceq>T) vs Ts)) \<and> heap s \<le>| heap s'"
    1.30 +apply (simp (no_asm_simp) only: split_tupled_all)
    1.31 +apply (drule eval_evals_exec_type_sound [THEN conjunct2, THEN conjunct1, THEN mp, THEN spec, THEN mp])
    1.32  apply auto
    1.33  done
    1.34  
    1.35  lemma exec_type_sound: "!!E s s'.  
    1.36 -  [| G=prg E; wf_java_prog G; G\<turnstile>(x,s) -s0-> (x',s'); (x,s)::\<preceq>E; E\<turnstile>s0\<surd> |]  
    1.37 -  ==> (x',s')::\<preceq>E"
    1.38 +  \<lbrakk> wf_java_prog G; G\<turnstile>(x,s) -s0-> (x',s'); (x,s)::\<preceq>E; E\<turnstile>s0\<surd>; G=prg E \<rbrakk>
    1.39 +  \<Longrightarrow> (x',s')::\<preceq>E \<and> heap s \<le>| heap s'"
    1.40  apply( simp (no_asm_simp) only: split_tupled_all)
    1.41  apply (drule eval_evals_exec_type_sound 
    1.42               [THEN conjunct2, THEN conjunct2, THEN mp, THEN spec, THEN mp])
    1.43 @@ -404,10 +404,10 @@
    1.44  "[|G=prg E; wf_java_prog G; G\<turnstile>(x,s) -e\<succ>a'-> Norm s'; a' \<noteq> Null; 
    1.45            (x,s)::\<preceq>E; E\<turnstile>e::Class C; method (G,C) sig \<noteq> None|] ==>  
    1.46    method (G,fst (the (heap s' (the_Addr a')))) sig \<noteq> None"
    1.47 -apply( drule (4) eval_type_sound)
    1.48 +apply (frule eval_type_sound, assumption+)
    1.49  apply(clarsimp)
    1.50  apply( frule widen_methd)
    1.51 -apply(   assumption)
    1.52 +apply assumption
    1.53  prefer 2
    1.54  apply(  fast)
    1.55  apply( drule non_npD)