author | nipkow |
Fri, 20 Nov 2015 12:22:41 +0100 | |
changeset 61709 | 47f7263870a0 |
parent 58889 | 5b7a9633cfa8 |
child 62390 | 842917225d56 |
permissions | -rw-r--r-- |
11376 | 1 |
(* Title: HOL/NanoJava/OpSem.thy |
2 |
Author: David von Oheimb |
|
3 |
Copyright 2001 Technische Universitaet Muenchen |
|
4 |
*) |
|
5 |
||
58889 | 6 |
section "Operational Evaluation Semantics" |
11376 | 7 |
|
16417 | 8 |
theory OpSem imports State begin |
11376 | 9 |
|
23755 | 10 |
inductive |
11 |
exec :: "[state,stmt, nat,state] => bool" ("_ -_-_\<rightarrow> _" [98,90, 65,98] 89) |
|
12 |
and eval :: "[state,expr,val,nat,state] => bool" ("_ -_\<succ>_-_\<rightarrow> _"[98,95,99,65,98] 89) |
|
13 |
where |
|
14 |
Skip: " s -Skip-n\<rightarrow> s" |
|
15 |
||
16 |
| Comp: "[| s0 -c1-n\<rightarrow> s1; s1 -c2-n\<rightarrow> s2 |] ==> |
|
17 |
s0 -c1;; c2-n\<rightarrow> s2" |
|
11376 | 18 |
|
23755 | 19 |
| Cond: "[| s0 -e\<succ>v-n\<rightarrow> s1; s1 -(if v\<noteq>Null then c1 else c2)-n\<rightarrow> s2 |] ==> |
20 |
s0 -If(e) c1 Else c2-n\<rightarrow> s2" |
|
11376 | 21 |
|
23755 | 22 |
| LoopF:" s0<x> = Null ==> |
23 |
s0 -While(x) c-n\<rightarrow> s0" |
|
24 |
| LoopT:"[| s0<x> \<noteq> Null; s0 -c-n\<rightarrow> s1; s1 -While(x) c-n\<rightarrow> s2 |] ==> |
|
25 |
s0 -While(x) c-n\<rightarrow> s2" |
|
11476 | 26 |
|
23755 | 27 |
| LAcc: " s -LAcc x\<succ>s<x>-n\<rightarrow> s" |
28 |
||
29 |
| LAss: " s -e\<succ>v-n\<rightarrow> s' ==> |
|
30 |
s -x:==e-n\<rightarrow> lupd(x\<mapsto>v) s'" |
|
11376 | 31 |
|
23755 | 32 |
| FAcc: " s -e\<succ>Addr a-n\<rightarrow> s' ==> |
33 |
s -e..f\<succ>get_field s' a f-n\<rightarrow> s'" |
|
11476 | 34 |
|
23755 | 35 |
| FAss: "[| s0 -e1\<succ>Addr a-n\<rightarrow> s1; s1 -e2\<succ>v-n\<rightarrow> s2 |] ==> |
36 |
s0 -e1..f:==e2-n\<rightarrow> upd_obj a f v s2" |
|
11476 | 37 |
|
23755 | 38 |
| NewC: " new_Addr s = Addr a ==> |
39 |
s -new C\<succ>Addr a-n\<rightarrow> new_obj a C s" |
|
11376 | 40 |
|
23755 | 41 |
| Cast: "[| s -e\<succ>v-n\<rightarrow> s'; |
11476 | 42 |
case v of Null => True | Addr a => obj_class s' a \<preceq>C C |] ==> |
23755 | 43 |
s -Cast C e\<succ>v-n\<rightarrow> s'" |
11376 | 44 |
|
23755 | 45 |
| Call: "[| s0 -e1\<succ>a-n\<rightarrow> s1; s1 -e2\<succ>p-n\<rightarrow> s2; |
46 |
lupd(This\<mapsto>a)(lupd(Par\<mapsto>p)(del_locs s2)) -Meth (C,m)-n\<rightarrow> s3 |
|
47 |
|] ==> s0 -{C}e1..m(e2)\<succ>s3<Res>-n\<rightarrow> set_locs s2 s3" |
|
11376 | 48 |
|
23755 | 49 |
| Meth: "[| s<This> = Addr a; D = obj_class s a; D\<preceq>C C; |
50 |
init_locs D m s -Impl (D,m)-n\<rightarrow> s' |] ==> |
|
51 |
s -Meth (C,m)-n\<rightarrow> s'" |
|
11376 | 52 |
|
23755 | 53 |
| Impl: " s -body Cm- n\<rightarrow> s' ==> |
54 |
s -Impl Cm-Suc n\<rightarrow> s'" |
|
11376 | 55 |
|
11476 | 56 |
|
11376 | 57 |
inductive_cases exec_elim_cases': |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
23755
diff
changeset
|
58 |
"s -Skip -n\<rightarrow> t" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
23755
diff
changeset
|
59 |
"s -c1;; c2 -n\<rightarrow> t" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
23755
diff
changeset
|
60 |
"s -If(e) c1 Else c2-n\<rightarrow> t" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
23755
diff
changeset
|
61 |
"s -While(x) c -n\<rightarrow> t" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
23755
diff
changeset
|
62 |
"s -x:==e -n\<rightarrow> t" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
23755
diff
changeset
|
63 |
"s -e1..f:==e2 -n\<rightarrow> t" |
11508 | 64 |
inductive_cases Meth_elim_cases: "s -Meth Cm -n\<rightarrow> t" |
65 |
inductive_cases Impl_elim_cases: "s -Impl Cm -n\<rightarrow> t" |
|
11376 | 66 |
lemmas exec_elim_cases = exec_elim_cases' Meth_elim_cases Impl_elim_cases |
11476 | 67 |
inductive_cases eval_elim_cases: |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
23755
diff
changeset
|
68 |
"s -new C \<succ>v-n\<rightarrow> t" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
23755
diff
changeset
|
69 |
"s -Cast C e \<succ>v-n\<rightarrow> t" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
23755
diff
changeset
|
70 |
"s -LAcc x \<succ>v-n\<rightarrow> t" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
23755
diff
changeset
|
71 |
"s -e..f \<succ>v-n\<rightarrow> t" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
23755
diff
changeset
|
72 |
"s -{C}e1..m(e2) \<succ>v-n\<rightarrow> t" |
11376 | 73 |
|
11476 | 74 |
lemma exec_eval_mono [rule_format]: |
75 |
"(s -c -n\<rightarrow> t \<longrightarrow> (\<forall>m. n \<le> m \<longrightarrow> s -c -m\<rightarrow> t)) \<and> |
|
76 |
(s -e\<succ>v-n\<rightarrow> t \<longrightarrow> (\<forall>m. n \<le> m \<longrightarrow> s -e\<succ>v-m\<rightarrow> t))" |
|
77 |
apply (rule exec_eval.induct) |
|
78 |
prefer 14 (* Impl *) |
|
11376 | 79 |
apply clarify |
80 |
apply (rename_tac n) |
|
81 |
apply (case_tac n) |
|
11508 | 82 |
apply (blast intro:exec_eval.intros)+ |
11376 | 83 |
done |
11476 | 84 |
lemmas exec_mono = exec_eval_mono [THEN conjunct1, rule_format] |
85 |
lemmas eval_mono = exec_eval_mono [THEN conjunct2, rule_format] |
|
86 |
||
87 |
lemma exec_exec_max: "\<lbrakk>s1 -c1- n1 \<rightarrow> t1 ; s2 -c2- n2\<rightarrow> t2\<rbrakk> \<Longrightarrow> |
|
88 |
s1 -c1-max n1 n2\<rightarrow> t1 \<and> s2 -c2-max n1 n2\<rightarrow> t2" |
|
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
32960
diff
changeset
|
89 |
by (fast intro: exec_mono max.cobounded1 max.cobounded2) |
11376 | 90 |
|
11476 | 91 |
lemma eval_exec_max: "\<lbrakk>s1 -c- n1 \<rightarrow> t1 ; s2 -e\<succ>v- n2\<rightarrow> t2\<rbrakk> \<Longrightarrow> |
92 |
s1 -c-max n1 n2\<rightarrow> t1 \<and> s2 -e\<succ>v-max n1 n2\<rightarrow> t2" |
|
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
32960
diff
changeset
|
93 |
by (fast intro: eval_mono exec_mono max.cobounded1 max.cobounded2) |
11476 | 94 |
|
95 |
lemma eval_eval_max: "\<lbrakk>s1 -e1\<succ>v1- n1 \<rightarrow> t1 ; s2 -e2\<succ>v2- n2\<rightarrow> t2\<rbrakk> \<Longrightarrow> |
|
96 |
s1 -e1\<succ>v1-max n1 n2\<rightarrow> t1 \<and> s2 -e2\<succ>v2-max n1 n2\<rightarrow> t2" |
|
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
32960
diff
changeset
|
97 |
by (fast intro: eval_mono max.cobounded1 max.cobounded2) |
11476 | 98 |
|
99 |
lemma eval_eval_exec_max: |
|
100 |
"\<lbrakk>s1 -e1\<succ>v1-n1\<rightarrow> t1; s2 -e2\<succ>v2-n2\<rightarrow> t2; s3 -c-n3\<rightarrow> t3\<rbrakk> \<Longrightarrow> |
|
101 |
s1 -e1\<succ>v1-max (max n1 n2) n3\<rightarrow> t1 \<and> |
|
102 |
s2 -e2\<succ>v2-max (max n1 n2) n3\<rightarrow> t2 \<and> |
|
103 |
s3 -c -max (max n1 n2) n3\<rightarrow> t3" |
|
104 |
apply (drule (1) eval_eval_max, erule thin_rl) |
|
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
32960
diff
changeset
|
105 |
by (fast intro: exec_mono eval_mono max.cobounded1 max.cobounded2) |
11376 | 106 |
|
11565 | 107 |
lemma Impl_body_eq: "(\<lambda>t. \<exists>n. Z -Impl M-n\<rightarrow> t) = (\<lambda>t. \<exists>n. Z -body M-n\<rightarrow> t)" |
11376 | 108 |
apply (rule ext) |
11476 | 109 |
apply (fast elim: exec_elim_cases intro: exec_eval.Impl) |
11376 | 110 |
done |
111 |
||
112 |
end |