|
1 (* Title: HOL/MicroJava/J/Eval.ML |
|
2 ID: $Id$ |
|
3 Author: David von Oheimb |
|
4 Copyright 1999 Technische Universitaet Muenchen |
|
5 *) |
|
6 |
|
7 Goal "\\<And>s s'. (G\\<turnstile>(x,s) -e \\<succ> v \\<rightarrow> (x',s') \\<longrightarrow> x'=None \\<longrightarrow> x=None) \\<and> \ |
|
8 \ (G\\<turnstile>(x,s) -es[\\<succ>]vs\\<rightarrow> (x',s') \\<longrightarrow> x'=None \\<longrightarrow> x=None) \\<and> \ |
|
9 \ (G\\<turnstile>(x,s) -c \\<rightarrow> (x',s') \\<longrightarrow> x'=None \\<longrightarrow> x=None)"; |
|
10 by(split_all_tac 1); |
|
11 by(rtac eval_evals_exec.induct 1); |
|
12 by(rewtac c_hupd_def); |
|
13 by(ALLGOALS Asm_full_simp_tac); |
|
14 qed "eval_evals_exec_no_xcpt"; |
|
15 |
|
16 val eval_no_xcpt = prove_goal thy "\\<And>X. G\\<turnstile>(x,s) -e\\<succ>v\\<rightarrow> (None,s') \\<Longrightarrow> x=None" (K [ |
|
17 dtac (eval_evals_exec_no_xcpt RS conjunct1 RS mp) 1, |
|
18 Fast_tac 1]); |
|
19 val evals_no_xcpt = prove_goal thy "\\<And>X. G\\<turnstile>(x,s) -e[\\<succ>]v\\<rightarrow> (None,s') \\<Longrightarrow> x=None" (K [ |
|
20 dtac (eval_evals_exec_no_xcpt RS conjunct2 RS conjunct1 RS mp) 1, |
|
21 Fast_tac 1]); |
|
22 |
|
23 val eval_evals_exec_xcpt = prove_goal thy |
|
24 "\\<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> \ |
|
25 \ (G\\<turnstile>(x,s) -es[\\<succ>]vs\\<rightarrow> (x',s') \\<longrightarrow> x=Some xc \\<longrightarrow> x'=Some xc \\<and> s'=s) \\<and> \ |
|
26 \ (G\\<turnstile>(x,s) -c \\<rightarrow> (x',s') \\<longrightarrow> x=Some xc \\<longrightarrow> x'=Some xc \\<and> s'=s)" |
|
27 (K [ |
|
28 split_all_tac 1, |
|
29 rtac eval_evals_exec.induct 1, |
|
30 rewtac c_hupd_def, |
|
31 ALLGOALS Asm_full_simp_tac]); |
|
32 val eval_xcpt = prove_goal thy |
|
33 "\\<And>X. G\\<turnstile>(Some xc,s) -e\\<succ>v\\<rightarrow> (x',s') \\<Longrightarrow> x'=Some xc \\<and> s'=s" (K [ |
|
34 dtac (eval_evals_exec_xcpt RS conjunct1 RS mp) 1, |
|
35 Fast_tac 1]); |
|
36 val exec_xcpt = prove_goal thy |
|
37 "\\<And>X. G\\<turnstile>(Some xc,s) -s0\\<rightarrow> (x',s') \\<Longrightarrow> x'=Some xc \\<and> s'=s" (K [ |
|
38 dtac (eval_evals_exec_xcpt RS conjunct2 RS conjunct2 RS mp) 1, |
|
39 Fast_tac 1]); |