# HG changeset patch
# User streckem
# Date 1060347466 -7200
# Node ID 0b04f6587e679f10366e545822718b12242c0af7
# Parent  d3916d9183d2bfd58bf822a0c9c1a3c2e1406f30
Changed lemmas .._type_sound

diff -r d3916d9183d2 -r 0b04f6587e67 src/HOL/MicroJava/J/JTypeSafe.thy
--- a/src/HOL/MicroJava/J/JTypeSafe.thy	Fri Aug 08 14:54:37 2003 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Fri Aug 08 14:57:46 2003 +0200
@@ -373,27 +373,27 @@
 Unify.trace_bound  := 20
 *}
 
+
 lemma eval_type_sound: "!!E s s'.  
-  [| G=prg E; wf_java_prog G; G\<turnstile>(x,s) -e\<succ>v -> (x',s'); (x,s)::\<preceq>E; E\<turnstile>e::T |]  
-  ==> (x',s')::\<preceq>E \<and> (x'=None --> G,heap s'\<turnstile>v::\<preceq>T)"
-apply( simp (no_asm_simp) only: split_tupled_all)
-apply (drule eval_evals_exec_type_sound 
-             [THEN conjunct1, THEN mp, THEN spec, THEN mp])
+  [| wf_java_prog G; G\<turnstile>(x,s) -e\<succ>v -> (x',s'); (x,s)::\<preceq>E; E\<turnstile>e::T; G=prg E |]  
+  ==> (x',s')::\<preceq>E \<and> (x'=None --> G,heap s'\<turnstile>v::\<preceq>T) \<and> heap s \<le>| heap s'"
+apply (simp (no_asm_simp) only: split_tupled_all)
+apply (drule eval_evals_exec_type_sound [THEN conjunct1, THEN mp, THEN spec, THEN mp])
 apply auto
 done
 
+
 lemma evals_type_sound: "!!E s s'.  
-  [| G\<turnstile>(x,s) -es[\<succ>]vs -> (x',s'); G=prg E; wf_java_prog G; (x,s)::\<preceq>E; E\<turnstile>es[::]Ts |]  
-  ==> (x',s')::\<preceq>E \<and> (x'=None --> list_all2 (conf G (heap s')) vs Ts)"
-apply( simp (no_asm_simp) only: split_tupled_all)
-apply (drule eval_evals_exec_type_sound 
-             [THEN conjunct2, THEN conjunct1, THEN mp, THEN spec, THEN mp])
+  [| wf_java_prog G; G\<turnstile>(x,s) -es[\<succ>]vs -> (x',s'); (x,s)::\<preceq>E; E\<turnstile>es[::]Ts; G=prg E |]  
+  ==> (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'"
+apply (simp (no_asm_simp) only: split_tupled_all)
+apply (drule eval_evals_exec_type_sound [THEN conjunct2, THEN conjunct1, THEN mp, THEN spec, THEN mp])
 apply auto
 done
 
 lemma exec_type_sound: "!!E s s'.  
-  [| G=prg E; wf_java_prog G; G\<turnstile>(x,s) -s0-> (x',s'); (x,s)::\<preceq>E; E\<turnstile>s0\<surd> |]  
-  ==> (x',s')::\<preceq>E"
+  \<lbrakk> wf_java_prog G; G\<turnstile>(x,s) -s0-> (x',s'); (x,s)::\<preceq>E; E\<turnstile>s0\<surd>; G=prg E \<rbrakk>
+  \<Longrightarrow> (x',s')::\<preceq>E \<and> heap s \<le>| heap s'"
 apply( simp (no_asm_simp) only: split_tupled_all)
 apply (drule eval_evals_exec_type_sound 
              [THEN conjunct2, THEN conjunct2, THEN mp, THEN spec, THEN mp])
@@ -404,10 +404,10 @@
 "[|G=prg E; wf_java_prog G; G\<turnstile>(x,s) -e\<succ>a'-> Norm s'; a' \<noteq> Null; 
           (x,s)::\<preceq>E; E\<turnstile>e::Class C; method (G,C) sig \<noteq> None|] ==>  
   method (G,fst (the (heap s' (the_Addr a')))) sig \<noteq> None"
-apply( drule (4) eval_type_sound)
+apply (frule eval_type_sound, assumption+)
 apply(clarsimp)
 apply( frule widen_methd)
-apply(   assumption)
+apply assumption
 prefer 2
 apply(  fast)
 apply( drule non_npD)