# 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\(x,s) -e\v -> (x',s'); (x,s)::\E; E\e::T |] - ==> (x',s')::\E \ (x'=None --> G,heap s'\v::\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\(x,s) -e\v -> (x',s'); (x,s)::\E; E\e::T; G=prg E |] + ==> (x',s')::\E \ (x'=None --> G,heap s'\v::\T) \ heap s \| 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\(x,s) -es[\]vs -> (x',s'); G=prg E; wf_java_prog G; (x,s)::\E; E\es[::]Ts |] - ==> (x',s')::\E \ (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\(x,s) -es[\]vs -> (x',s'); (x,s)::\E; E\es[::]Ts; G=prg E |] + ==> (x',s')::\E \ (x'=None --> (list_all2 (\v T. G,heap s'\v::\T) vs Ts)) \ heap s \| 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\(x,s) -s0-> (x',s'); (x,s)::\E; E\s0\ |] - ==> (x',s')::\E" + \ wf_java_prog G; G\(x,s) -s0-> (x',s'); (x,s)::\E; E\s0\; G=prg E \ + \ (x',s')::\E \ heap s \| 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\(x,s) -e\a'-> Norm s'; a' \ Null; (x,s)::\E; E\e::Class C; method (G,C) sig \ None|] ==> method (G,fst (the (heap s' (the_Addr a')))) sig \ 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)