File Eval.ML

(*  Title:      HOL/MicroJava/J/Eval.ML
    ID:         $Id: Eval.ML,v 1.3 2000/09/21 08:42:57 kleing Exp $
    Author:     David von Oheimb
    Copyright   1999 Technische Universitaet Muenchen
*)

Goal "[|new_Addr (heap s) = (a,x); \
\      s' = c_hupd (heap s(a\<mapsto>(C,init_vars (fields (G,C))))) (x,s)|] ==> \
\      G\<turnstile>Norm s -NewC C\<succ>Addr a-> s'";
by (hyp_subst_tac 1);
br eval_evals_exec.NewC 1;
by Auto_tac;
qed "NewCI";

Goal "!!s s'. (G\<turnstile>(x,s) -e \<succ>  v -> (x',s') --> x'=None --> x=None) \<and> \
\             (G\<turnstile>(x,s) -es[\<succ>]vs-> (x',s') --> x'=None --> x=None) \<and> \
\             (G\<turnstile>(x,s) -c       -> (x',s') --> x'=None --> x=None)";
by(split_all_tac 1);
by(rtac eval_evals_exec.induct 1);
by(rewtac c_hupd_def);
by(ALLGOALS Asm_full_simp_tac);
qed "eval_evals_exec_no_xcpt";

val eval_no_xcpt = prove_goal thy "!!X. G\<turnstile>(x,s) -e\<succ>v-> (None,s') ==> x=None" (K [
	dtac (eval_evals_exec_no_xcpt RS conjunct1 RS mp) 1,
	Fast_tac 1]);
val evals_no_xcpt = prove_goal thy "!!X. G\<turnstile>(x,s) -e[\<succ>]v-> (None,s') ==> x=None" (K [
	dtac (eval_evals_exec_no_xcpt RS conjunct2 RS conjunct1 RS mp) 1,
	Fast_tac 1]);

val eval_evals_exec_xcpt = prove_goal thy 
"!!s s'. (G\<turnstile>(x,s) -e \<succ>  v -> (x',s') --> x=Some xc --> x'=Some xc \<and> s'=s) \<and> \
\        (G\<turnstile>(x,s) -es[\<succ>]vs-> (x',s') --> x=Some xc --> x'=Some xc \<and> s'=s) \<and> \
\        (G\<turnstile>(x,s) -c       -> (x',s') --> x=Some xc --> x'=Some xc \<and> s'=s)"
 (K [
	split_all_tac 1,
	rtac eval_evals_exec.induct 1,
	rewtac c_hupd_def,
	ALLGOALS Asm_full_simp_tac]);
val eval_xcpt = prove_goal thy 
"!!X. G\<turnstile>(Some xc,s) -e\<succ>v-> (x',s') ==> x'=Some xc \<and>  s'=s" (K [
	dtac (eval_evals_exec_xcpt RS conjunct1 RS mp) 1,
	Fast_tac 1]);
val exec_xcpt = prove_goal thy 
"!!X. G\<turnstile>(Some xc,s) -s0-> (x',s') ==> x'=Some xc \<and>  s'=s" (K [
	dtac (eval_evals_exec_xcpt RS conjunct2 RS conjunct2 RS mp) 1,
	Fast_tac 1]);