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 |
25 |
|
26 Skip: " s -Skip-n-> s" |
25 Skip: " s -Skip-n-> s" |
27 |
26 |
28 Comp: "[| s0 -c1-n-> s1; s1 -c2-n-> s2 |] ==> |
27 Comp: "[| s0 -c1-n-> s1; s1 -c2-n-> s2 |] ==> |
29 s0 -c1;; c2-n-> s2" |
28 s0 -c1;; c2-n-> s2" |
30 |
29 |
65 Impl: " s -body C m-n-> s' ==> |
64 Impl: " s -body C m-n-> s' ==> |
66 s -Impl C m-Suc n-> s'" |
65 s -Impl C m-Suc n-> s'" |
67 |
66 |
68 |
67 |
69 inductive_cases exec_elim_cases': |
68 inductive_cases exec_elim_cases': |
70 "s -Skip -n\<rightarrow> t" |
69 "s -Skip -n\<rightarrow> t" |
71 "s -c1;; c2 -n\<rightarrow> t" |
70 "s -c1;; c2 -n\<rightarrow> t" |
72 "s -If(e) c1 Else c2-n\<rightarrow> t" |
71 "s -If(e) c1 Else c2-n\<rightarrow> t" |
73 "s -While(x) c -n\<rightarrow> t" |
72 "s -While(x) c -n\<rightarrow> t" |
74 "s -x:==e -n\<rightarrow> t" |
73 "s -x:==e -n\<rightarrow> t" |
75 "s -e1..f:==e2 -n\<rightarrow> t" |
74 "s -e1..f:==e2 -n\<rightarrow> t" |
76 inductive_cases Meth_elim_cases: "s -Meth C m-n\<rightarrow> t" |
75 inductive_cases Meth_elim_cases: "s -Meth C m-n\<rightarrow> t" |
77 inductive_cases Impl_elim_cases: "s -Impl C m-n\<rightarrow> t" |
76 inductive_cases Impl_elim_cases: "s -Impl C m-n\<rightarrow> t" |
78 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 |
79 inductive_cases eval_elim_cases: |
78 inductive_cases eval_elim_cases: |
80 "s -new C \<succ>v-n\<rightarrow> t" |
79 "s -new C \<succ>v-n\<rightarrow> t" |
81 "s -Cast C e \<succ>v-n\<rightarrow> t" |
80 "s -Cast C e \<succ>v-n\<rightarrow> t" |
82 "s -LAcc x \<succ>v-n\<rightarrow> t" |
81 "s -LAcc x \<succ>v-n\<rightarrow> t" |
83 "s -e..f \<succ>v-n\<rightarrow> t" |
82 "s -e..f \<succ>v-n\<rightarrow> t" |
84 "s -{C}e1..m(e2) \<succ>v-n\<rightarrow> t" |
83 "s -{C}e1..m(e2) \<succ>v-n\<rightarrow> t" |
85 |
84 |
86 lemma exec_eval_mono [rule_format]: |
85 lemma exec_eval_mono [rule_format]: |
87 "(s -c -n\<rightarrow> t \<longrightarrow> (\<forall>m. n \<le> m \<longrightarrow> s -c -m\<rightarrow> t)) \<and> |
86 "(s -c -n\<rightarrow> t \<longrightarrow> (\<forall>m. n \<le> m \<longrightarrow> s -c -m\<rightarrow> t)) \<and> |
88 (s -e\<succ>v-n\<rightarrow> t \<longrightarrow> (\<forall>m. n \<le> m \<longrightarrow> s -e\<succ>v-m\<rightarrow> t))" |
87 (s -e\<succ>v-n\<rightarrow> t \<longrightarrow> (\<forall>m. n \<le> m \<longrightarrow> s -e\<succ>v-m\<rightarrow> t))" |
89 apply (rule exec_eval.induct) |
88 apply (rule exec_eval.induct) |