Theory OpSem

(*  Title:      HOL/NanoJava/OpSem.thy
    Author:     David von Oheimb
    Copyright   2001 Technische Universitaet Muenchen
*)

section "Operational Evaluation Semantics"

theory OpSem imports State begin

inductive
  exec :: "[state,stmt,    nat,state] => bool" ("_ -_-_→ _"  [98,90,   65,98] 89)
  and eval :: "[state,expr,val,nat,state] => bool" ("_ -_≻_-_→ _"[98,95,99,65,98] 89)
where
  Skip: "   s -Skip-n→ s"

| Comp: "[| s0 -c1-n→ s1; s1 -c2-n→ s2 |] ==>
            s0 -c1;; c2-n→ s2"

| Cond: "[| s0 -e≻v-n→ s1; s1 -(if v≠Null then c1 else c2)-n→ s2 |] ==>
            s0 -If(e) c1 Else c2-n→ s2"

| LoopF:"   s0<x> = Null ==>
            s0 -While(x) c-n→ s0"
| LoopT:"[| s0<x> ≠ Null; s0 -c-n→ s1; s1 -While(x) c-n→ s2 |] ==>
            s0 -While(x) c-n→ s2"

| LAcc: "   s -LAcc x≻s<x>-n→ s"

| LAss: "   s -e≻v-n→ s' ==>
            s -x:==e-n→ lupd(x↦v) s'"

| FAcc: "   s -e≻Addr a-n→ s' ==>
            s -e..f≻get_field s' a f-n→ s'"

| FAss: "[| s0 -e1≻Addr a-n→ s1;  s1 -e2≻v-n→ s2 |] ==>
            s0 -e1..f:==e2-n→ upd_obj a f v s2"

| NewC: "   new_Addr s = Addr a ==>
            s -new C≻Addr a-n→ new_obj a C s"

| Cast: "[| s -e≻v-n→ s';
            case v of Null => True | Addr a => obj_class s' a ≼C C |] ==>
            s -Cast C e≻v-n→ s'"

| Call: "[| s0 -e1≻a-n→ s1; s1 -e2≻p-n→ s2; 
            lupd(This↦a)(lupd(Par↦p)(del_locs s2)) -Meth (C,m)-n→ s3
     |] ==> s0 -{C}e1..m(e2)≻s3<Res>-n→ set_locs s2 s3"

| Meth: "[| s<This> = Addr a; D = obj_class s a; D≼C C;
            init_locs D m s -Impl (D,m)-n→ s' |] ==>
            s -Meth (C,m)-n→ s'"

| Impl: "   s -body Cm-    n→ s' ==>
            s -Impl Cm-Suc n→ s'"


inductive_cases exec_elim_cases':
                                  "s -Skip            -n→ t"
                                  "s -c1;; c2         -n→ t"
                                  "s -If(e) c1 Else c2-n→ t"
                                  "s -While(x) c      -n→ t"
                                  "s -x:==e           -n→ t"
                                  "s -e1..f:==e2      -n→ t"
inductive_cases Meth_elim_cases:  "s -Meth Cm         -n→ t"
inductive_cases Impl_elim_cases:  "s -Impl Cm         -n→ t"
lemmas exec_elim_cases = exec_elim_cases' Meth_elim_cases Impl_elim_cases
inductive_cases eval_elim_cases:
                                  "s -new C         ≻v-n→ t"
                                  "s -Cast C e      ≻v-n→ t"
                                  "s -LAcc x        ≻v-n→ t"
                                  "s -e..f          ≻v-n→ t"
                                  "s -{C}e1..m(e2)  ≻v-n→ t"

lemma exec_eval_mono [rule_format]: 
  "(s -c  -n→ t ⟶ (∀m. n ≤ m ⟶ s -c  -m→ t)) ∧
   (s -e≻v-n→ t ⟶ (∀m. n ≤ m ⟶ s -e≻v-m→ t))"
apply (rule exec_eval.induct)
prefer 14 (* Impl *)
apply clarify
apply (rename_tac n)
apply (case_tac n)
apply (blast intro:exec_eval.intros)+
done
lemmas exec_mono = exec_eval_mono [THEN conjunct1, rule_format]
lemmas eval_mono = exec_eval_mono [THEN conjunct2, rule_format]

lemma exec_exec_max: "⟦s1 -c1-    n1   → t1 ; s2 -c2-       n2→ t2⟧ ⟹ 
                       s1 -c1-max n1 n2→ t1 ∧ s2 -c2-max n1 n2→ t2"
by (fast intro: exec_mono max.cobounded1 max.cobounded2)

lemma eval_exec_max: "⟦s1 -c-    n1   → t1 ; s2 -e≻v-       n2→ t2⟧ ⟹ 
                       s1 -c-max n1 n2→ t1 ∧ s2 -e≻v-max n1 n2→ t2"
by (fast intro: eval_mono exec_mono max.cobounded1 max.cobounded2)

lemma eval_eval_max: "⟦s1 -e1≻v1-    n1   → t1 ; s2 -e2≻v2-       n2→ t2⟧ ⟹ 
                       s1 -e1≻v1-max n1 n2→ t1 ∧ s2 -e2≻v2-max n1 n2→ t2"
by (fast intro: eval_mono max.cobounded1 max.cobounded2)

lemma eval_eval_exec_max: 
 "⟦s1 -e1≻v1-n1→ t1; s2 -e2≻v2-n2→ t2; s3 -c-n3→ t3⟧ ⟹ 
   s1 -e1≻v1-max (max n1 n2) n3→ t1 ∧ 
   s2 -e2≻v2-max (max n1 n2) n3→ t2 ∧ 
   s3 -c    -max (max n1 n2) n3→ t3"
apply (drule (1) eval_eval_max, erule thin_rl)
by (fast intro: exec_mono eval_mono max.cobounded1 max.cobounded2)

lemma Impl_body_eq: "(λt. ∃n. Z -Impl M-n→ t) = (λt. ∃n. Z -body M-n→ t)"
apply (rule ext)
apply (fast elim: exec_elim_cases intro: exec_eval.Impl)
done

end