src/HOL/MicroJava/J/Eval.ML
changeset 10042 7164dc0d24d8
parent 9346 297dcbf64526
child 10613 78b1d6c3ee9c
     1.1 --- a/src/HOL/MicroJava/J/Eval.ML	Wed Sep 20 21:20:41 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/J/Eval.ML	Thu Sep 21 10:42:49 2000 +0200
     1.3 @@ -4,44 +4,44 @@
     1.4      Copyright   1999 Technische Universitaet Muenchen
     1.5  *)
     1.6  
     1.7 -Goal "\\<lbrakk>new_Addr (heap s) = (a,x); \
     1.8 -\      s' = c_hupd (heap s(a\\<mapsto>(C,init_vars (fields (G,C))))) (x,s)\\<rbrakk> \\<Longrightarrow> \
     1.9 -\      G\\<turnstile>Norm s -NewC C\\<succ>Addr a\\<rightarrow> s'";
    1.10 +Goal "[|new_Addr (heap s) = (a,x); \
    1.11 +\      s' = c_hupd (heap s(a\\<mapsto>(C,init_vars (fields (G,C))))) (x,s)|] ==> \
    1.12 +\      G\\<turnstile>Norm s -NewC C\\<succ>Addr a-> s'";
    1.13  by (hyp_subst_tac 1);
    1.14  br eval_evals_exec.NewC 1;
    1.15  by Auto_tac;
    1.16  qed "NewCI";
    1.17  
    1.18 -Goal "\\<And>s s'. (G\\<turnstile>(x,s) -e \\<succ>  v \\<rightarrow> (x',s') \\<longrightarrow> x'=None \\<longrightarrow> x=None) \\<and> \
    1.19 -\             (G\\<turnstile>(x,s) -es[\\<succ>]vs\\<rightarrow> (x',s') \\<longrightarrow> x'=None \\<longrightarrow> x=None) \\<and> \
    1.20 -\             (G\\<turnstile>(x,s) -c       \\<rightarrow> (x',s') \\<longrightarrow> x'=None \\<longrightarrow> x=None)";
    1.21 +Goal "!!s s'. (G\\<turnstile>(x,s) -e \\<succ>  v -> (x',s') --> x'=None --> x=None) \\<and> \
    1.22 +\             (G\\<turnstile>(x,s) -es[\\<succ>]vs-> (x',s') --> x'=None --> x=None) \\<and> \
    1.23 +\             (G\\<turnstile>(x,s) -c       -> (x',s') --> x'=None --> x=None)";
    1.24  by(split_all_tac 1);
    1.25  by(rtac eval_evals_exec.induct 1);
    1.26  by(rewtac c_hupd_def);
    1.27  by(ALLGOALS Asm_full_simp_tac);
    1.28  qed "eval_evals_exec_no_xcpt";
    1.29  
    1.30 -val eval_no_xcpt = prove_goal thy "\\<And>X. G\\<turnstile>(x,s) -e\\<succ>v\\<rightarrow> (None,s') \\<Longrightarrow> x=None" (K [
    1.31 +val eval_no_xcpt = prove_goal thy "!!X. G\\<turnstile>(x,s) -e\\<succ>v-> (None,s') ==> x=None" (K [
    1.32  	dtac (eval_evals_exec_no_xcpt RS conjunct1 RS mp) 1,
    1.33  	Fast_tac 1]);
    1.34 -val evals_no_xcpt = prove_goal thy "\\<And>X. G\\<turnstile>(x,s) -e[\\<succ>]v\\<rightarrow> (None,s') \\<Longrightarrow> x=None" (K [
    1.35 +val evals_no_xcpt = prove_goal thy "!!X. G\\<turnstile>(x,s) -e[\\<succ>]v-> (None,s') ==> x=None" (K [
    1.36  	dtac (eval_evals_exec_no_xcpt RS conjunct2 RS conjunct1 RS mp) 1,
    1.37  	Fast_tac 1]);
    1.38  
    1.39  val eval_evals_exec_xcpt = prove_goal thy 
    1.40 -"\\<And>s s'. (G\\<turnstile>(x,s) -e \\<succ>  v \\<rightarrow> (x',s') \\<longrightarrow> x=Some xc \\<longrightarrow> x'=Some xc \\<and> s'=s) \\<and> \
    1.41 -\        (G\\<turnstile>(x,s) -es[\\<succ>]vs\\<rightarrow> (x',s') \\<longrightarrow> x=Some xc \\<longrightarrow> x'=Some xc \\<and> s'=s) \\<and> \
    1.42 -\        (G\\<turnstile>(x,s) -c       \\<rightarrow> (x',s') \\<longrightarrow> x=Some xc \\<longrightarrow> x'=Some xc \\<and> s'=s)"
    1.43 +"!!s s'. (G\\<turnstile>(x,s) -e \\<succ>  v -> (x',s') --> x=Some xc --> x'=Some xc \\<and> s'=s) \\<and> \
    1.44 +\        (G\\<turnstile>(x,s) -es[\\<succ>]vs-> (x',s') --> x=Some xc --> x'=Some xc \\<and> s'=s) \\<and> \
    1.45 +\        (G\\<turnstile>(x,s) -c       -> (x',s') --> x=Some xc --> x'=Some xc \\<and> s'=s)"
    1.46   (K [
    1.47  	split_all_tac 1,
    1.48  	rtac eval_evals_exec.induct 1,
    1.49  	rewtac c_hupd_def,
    1.50  	ALLGOALS Asm_full_simp_tac]);
    1.51  val eval_xcpt = prove_goal thy 
    1.52 -"\\<And>X. G\\<turnstile>(Some xc,s) -e\\<succ>v\\<rightarrow> (x',s') \\<Longrightarrow> x'=Some xc \\<and>  s'=s" (K [
    1.53 +"!!X. G\\<turnstile>(Some xc,s) -e\\<succ>v-> (x',s') ==> x'=Some xc \\<and>  s'=s" (K [
    1.54  	dtac (eval_evals_exec_xcpt RS conjunct1 RS mp) 1,
    1.55  	Fast_tac 1]);
    1.56  val exec_xcpt = prove_goal thy 
    1.57 -"\\<And>X. G\\<turnstile>(Some xc,s) -s0\\<rightarrow> (x',s') \\<Longrightarrow> x'=Some xc \\<and>  s'=s" (K [
    1.58 +"!!X. G\\<turnstile>(Some xc,s) -s0-> (x',s') ==> x'=Some xc \\<and>  s'=s" (K [
    1.59  	dtac (eval_evals_exec_xcpt RS conjunct2 RS conjunct2 RS mp) 1,
    1.60  	Fast_tac 1]);