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