10 |
10 |
11 consts |
11 consts |
12 exec :: "(state \<times> stmt \<times> nat \<times> state) set" |
12 exec :: "(state \<times> stmt \<times> nat \<times> state) set" |
13 eval :: "(state \<times> expr \<times> val \<times> nat \<times> state) set" |
13 eval :: "(state \<times> expr \<times> val \<times> nat \<times> state) set" |
14 syntax (xsymbols) |
14 syntax (xsymbols) |
15 exec :: "[state,stmt, nat,state] => bool" ("_ -_-_\<rightarrow> _" [98,90, 99,98] 89) |
15 exec :: "[state,stmt, nat,state] => bool" ("_ -_-_\<rightarrow> _" [98,90, 65,98] 89) |
16 eval :: "[state,expr,val,nat,state] => bool" ("_ -_\<succ>_-_\<rightarrow> _"[98,95,99,99,98] 89) |
16 eval :: "[state,expr,val,nat,state] => bool" ("_ -_\<succ>_-_\<rightarrow> _"[98,95,99,65,98] 89) |
17 syntax |
17 syntax |
18 exec :: "[state,stmt, nat,state] => bool" ("_ -_-_-> _" [98,90, 99,98]89) |
18 exec :: "[state,stmt, nat,state] => bool" ("_ -_-_-> _" [98,90, 65,98]89) |
19 eval :: "[state,expr,val,nat,state] => bool" ("_ -_>_-_-> _"[98,95,99,99,98]89) |
19 eval :: "[state,expr,val,nat,state] => bool" ("_ -_>_-_-> _"[98,95,99,65,98]89) |
20 translations |
20 translations |
21 "s -c -n-> s'" == "(s, c, n, s') \<in> exec" |
21 "s -c -n-> s'" == "(s, c, n, s') \<in> exec" |
22 "s -e>v-n-> s'" == "(s, e, v, n, s') \<in> eval" |
22 "s -e>v-n-> s'" == "(s, e, v, n, s') \<in> eval" |
23 |
23 |
24 inductive exec eval intros |
24 inductive exec eval intros |
59 |
59 |
60 Meth: "[| s<This> = Addr a; D = obj_class s a; D\<preceq>C C; |
60 Meth: "[| s<This> = Addr a; D = obj_class s a; D\<preceq>C C; |
61 init_locs D m s -Impl (D,m)-n-> s' |] ==> |
61 init_locs D m s -Impl (D,m)-n-> s' |] ==> |
62 s -Meth (C,m)-n-> s'" |
62 s -Meth (C,m)-n-> s'" |
63 |
63 |
64 Impl: " s -body M-n-> s' ==> |
64 Impl: " s -body Cm- n-> s' ==> |
65 s -Impl M-Suc n-> s'" |
65 s -Impl Cm-Suc n-> s'" |
66 |
66 |
67 |
67 |
68 inductive_cases exec_elim_cases': |
68 inductive_cases exec_elim_cases': |
69 "s -Skip -n\<rightarrow> t" |
69 "s -Skip -n\<rightarrow> t" |
70 "s -c1;; c2 -n\<rightarrow> t" |
70 "s -c1;; c2 -n\<rightarrow> t" |
71 "s -If(e) c1 Else c2-n\<rightarrow> t" |
71 "s -If(e) c1 Else c2-n\<rightarrow> t" |
72 "s -While(x) c -n\<rightarrow> t" |
72 "s -While(x) c -n\<rightarrow> t" |
73 "s -x:==e -n\<rightarrow> t" |
73 "s -x:==e -n\<rightarrow> t" |
74 "s -e1..f:==e2 -n\<rightarrow> t" |
74 "s -e1..f:==e2 -n\<rightarrow> t" |
75 inductive_cases Meth_elim_cases: "s -Meth Cm-n\<rightarrow> t" |
75 inductive_cases Meth_elim_cases: "s -Meth Cm -n\<rightarrow> t" |
76 inductive_cases Impl_elim_cases: "s -Impl Cm-n\<rightarrow> t" |
76 inductive_cases Impl_elim_cases: "s -Impl Cm -n\<rightarrow> t" |
77 lemmas exec_elim_cases = exec_elim_cases' Meth_elim_cases Impl_elim_cases |
77 lemmas exec_elim_cases = exec_elim_cases' Meth_elim_cases Impl_elim_cases |
78 inductive_cases eval_elim_cases: |
78 inductive_cases eval_elim_cases: |
79 "s -new C \<succ>v-n\<rightarrow> t" |
79 "s -new C \<succ>v-n\<rightarrow> t" |
80 "s -Cast C e \<succ>v-n\<rightarrow> t" |
80 "s -Cast C e \<succ>v-n\<rightarrow> t" |
81 "s -LAcc x \<succ>v-n\<rightarrow> t" |
81 "s -LAcc x \<succ>v-n\<rightarrow> t" |
88 apply (rule exec_eval.induct) |
88 apply (rule exec_eval.induct) |
89 prefer 14 (* Impl *) |
89 prefer 14 (* Impl *) |
90 apply clarify |
90 apply clarify |
91 apply (rename_tac n) |
91 apply (rename_tac n) |
92 apply (case_tac n) |
92 apply (case_tac n) |
93 apply (blast intro:exec_eval.intros)+ |
93 apply (blast intro:exec_eval.intros)+ |
94 done |
94 done |
95 lemmas exec_mono = exec_eval_mono [THEN conjunct1, rule_format] |
95 lemmas exec_mono = exec_eval_mono [THEN conjunct1, rule_format] |
96 lemmas eval_mono = exec_eval_mono [THEN conjunct2, rule_format] |
96 lemmas eval_mono = exec_eval_mono [THEN conjunct2, rule_format] |
97 |
97 |
98 lemma exec_exec_max: "\<lbrakk>s1 -c1- n1 \<rightarrow> t1 ; s2 -c2- n2\<rightarrow> t2\<rbrakk> \<Longrightarrow> |
98 lemma exec_exec_max: "\<lbrakk>s1 -c1- n1 \<rightarrow> t1 ; s2 -c2- n2\<rightarrow> t2\<rbrakk> \<Longrightarrow> |