11376
|
1 |
(* Title: HOL/NanoJava/OpSem.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: David von Oheimb
|
|
4 |
Copyright 2001 Technische Universitaet Muenchen
|
|
5 |
*)
|
|
6 |
|
|
7 |
header "Operational Evaluation Semantics"
|
|
8 |
|
|
9 |
theory OpSem = State:
|
|
10 |
|
|
11 |
consts
|
|
12 |
exec :: "(state \<times> stmt \<times> nat \<times> state) set"
|
|
13 |
syntax (xsymbols)
|
|
14 |
exec :: "[state, stmt, nat, state] => bool" ("_ -_-_\<rightarrow> _" [98,90,99,98] 89)
|
|
15 |
syntax
|
|
16 |
exec :: "[state, stmt, nat, state] => bool" ("_ -_-_-> _" [98,90,99,98] 89)
|
|
17 |
translations
|
|
18 |
"s -c-n-> s'" == "(s, c, n, s') \<in> exec"
|
|
19 |
|
|
20 |
inductive exec intros
|
|
21 |
|
|
22 |
Skip: " s -Skip-n-> s"
|
|
23 |
|
|
24 |
Comp: "[| s0 -c1-n-> s1; s1 -c2-n-> s2 |] ==>
|
|
25 |
s0 -c1;; c2-n-> s2"
|
|
26 |
|
|
27 |
Cond: "[| s -(if s<e> \<noteq> Null then c1 else c2)-n-> s' |] ==>
|
|
28 |
s -If(e) c1 Else c2-n-> s'"
|
|
29 |
|
|
30 |
LoopF:" s0<e> = Null ==>
|
|
31 |
s0 -While(e) c-n-> s0"
|
|
32 |
LoopT:"[| s0<e> \<noteq> Null; s0 -c-n-> s1; s1 -While(e) c-n-> s2 |] ==>
|
|
33 |
s0 -While(e) c-n-> s2"
|
|
34 |
|
|
35 |
NewC: " new_Addr s = Addr a ==>
|
|
36 |
s -x:=new C-n-> lupd(x\<mapsto>Addr a)(new_obj a C s)"
|
|
37 |
|
|
38 |
Cast: " (case s<y> of Null => True | Addr a => obj_class s a \<preceq>C C) ==>
|
|
39 |
s -x:=(C)y-n-> lupd(x\<mapsto>s<y>) s"
|
|
40 |
|
|
41 |
FAcc: " s<y> = Addr a ==>
|
|
42 |
s -x:=y..f-n-> lupd(x\<mapsto>get_field s a f) s"
|
|
43 |
|
|
44 |
FAss: " s<y> = Addr a ==>
|
|
45 |
s -y..f:=x-n-> upd_obj a f (s<x>) s"
|
|
46 |
|
|
47 |
Call: "lupd(This\<mapsto>s<y>)(lupd(Param\<mapsto>s<p>)(init_locs C m s))-Meth C m -n-> s'==>
|
|
48 |
s -x:={C}y..m(p)-n-> lupd(x\<mapsto>s'<Res>)(set_locs s s')"
|
|
49 |
|
|
50 |
Meth: "[| s<This> = Addr a; obj_class s a\<preceq>C C;
|
|
51 |
s -Impl (obj_class s a) m-n-> s' |] ==>
|
|
52 |
s -Meth C m-n-> s'"
|
|
53 |
|
|
54 |
Impl: " s -body C m- n-> s' ==>
|
|
55 |
s -Impl C m-Suc n-> s'"
|
|
56 |
|
|
57 |
inductive_cases exec_elim_cases':
|
|
58 |
"s -Skip -n-> t"
|
|
59 |
"s -c1;; c2 -n-> t"
|
|
60 |
"s -If(e) c1 Else c2-n-> t"
|
|
61 |
"s -While(e) c -n-> t"
|
|
62 |
"s -x:=new C -n-> t"
|
|
63 |
"s -x:=(C)y -n-> t"
|
|
64 |
"s -x:=y..f -n-> t"
|
|
65 |
"s -y..f:=x -n-> t"
|
|
66 |
"s -x:={C}y..m(p) -n-> t"
|
|
67 |
inductive_cases Meth_elim_cases: "s -Meth C m -n-> t"
|
|
68 |
inductive_cases Impl_elim_cases: "s -Impl C m -n-> t"
|
|
69 |
lemmas exec_elim_cases = exec_elim_cases' Meth_elim_cases Impl_elim_cases
|
|
70 |
|
|
71 |
lemma exec_mono [rule_format]: "s -c-n\<rightarrow> t \<Longrightarrow> \<forall>m. n \<le> m \<longrightarrow> s -c-m\<rightarrow> t"
|
|
72 |
apply (erule exec.induct)
|
|
73 |
prefer 12 (* Impl *)
|
|
74 |
apply clarify
|
|
75 |
apply (rename_tac n)
|
|
76 |
apply (case_tac n)
|
|
77 |
apply (blast intro:exec.intros)+
|
|
78 |
done
|
|
79 |
|
|
80 |
lemma exec_max2: "\<lbrakk>s1 -c1- n1 \<rightarrow> t1 ; s2 -c2- n2\<rightarrow> t2\<rbrakk> \<Longrightarrow>
|
|
81 |
s1 -c1-max n1 n2\<rightarrow> t1 \<and> s2 -c2-max n1 n2\<rightarrow> t2"
|
|
82 |
by (fast intro: exec_mono le_maxI1 le_maxI2)
|
|
83 |
|
|
84 |
lemma Impl_body_eq: "(\<lambda>t. \<exists>n. z -Impl C m-n\<rightarrow> t) = (\<lambda>t. \<exists>n. z -body C m-n\<rightarrow> t)"
|
|
85 |
apply (rule ext)
|
|
86 |
apply (fast elim: exec_elim_cases intro: exec.Impl)
|
|
87 |
done
|
|
88 |
|
|
89 |
end |