# Theory OpSem

Up to index of Isabelle/HOL/NanoJava

theory OpSem
imports State
begin

    (*  Title:      HOL/NanoJava/OpSem.thy
        ID:         $Id: OpSem.thy,v 1.10 2005/06/17 14:13:09 haftmann Exp $
        Author:     David von Oheimb
        Copyright   2001 Technische Universitaet Muenchen
    *)

    header "Operational Evaluation Semantics"

    theory OpSem imports State begin

    consts
     exec :: "(state × stmt       × nat × state) set"
     eval :: "(state × expr × val × nat × state) set"
    syntax (xsymbols)
     exec :: "[state,stmt,    nat,state] => bool" ("_ -_-_-> _"  [98,90,   65,98] 89)
     eval :: "[state,expr,val,nat,state] => bool" ("_ -_\<succ>_-_-> _"[98,95,99,65,98] 89)
    syntax
     exec :: "[state,stmt,    nat,state] => bool" ("_ -_-_-> _"  [98,90,   65,98]89)
     eval :: "[state,expr,val,nat,state] => bool" ("_ -_>_-_-> _"[98,95,99,65,98]89)
    translations
     "s -c  -n-> s'" == "(s, c,    n, s') ∈ exec"
     "s -e>v-n-> s'" == "(s, e, v, n, s') ∈ eval"

    inductive exec eval intros
      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\<mapsto>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 \<preceq>C C |] ==>
                s -Cast C e>v-n-> s'"

      Call: "[| s0 -e1>a-n-> s1; s1 -e2>p-n-> s2;
                lupd(This\<mapsto>a)(lupd(Par\<mapsto>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\<preceq>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         \<succ>v-n-> t"
                                      "s -Cast C e      \<succ>v-n-> t"
                                      "s -LAcc x        \<succ>v-n-> t"
                                      "s -e..f          \<succ>v-n-> t"
                                      "s -{C}e1..m(e2)  \<succ>v-n-> t"

    lemma exec_eval_mono [rule_format]:
      "(s -c  -n-> t --> (∀m. n ≤ m --> s -c  -m-> t)) ∧
       (s -e\<succ>v-n-> t --> (∀m. n ≤ m --> s -e\<succ>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 le_maxI1 le_maxI2)

    lemma eval_exec_max: "[|s1 -c-    n1   -> t1 ; s2 -e\<succ>v-       n2-> t2|] ==>
                           s1 -c-max n1 n2-> t1 ∧ s2 -e\<succ>v-max n1 n2-> t2"
    by (fast intro: eval_mono exec_mono le_maxI1 le_maxI2)

    lemma eval_eval_max: "[|s1 -e1\<succ>v1-    n1   -> t1 ; s2 -e2\<succ>v2-       n2-> t2|] ==>
                           s1 -e1\<succ>v1-max n1 n2-> t1 ∧ s2 -e2\<succ>v2-max n1 n2-> t2"
    by (fast intro: eval_mono le_maxI1 le_maxI2)

    lemma eval_eval_exec_max:
     "[|s1 -e1\<succ>v1-n1-> t1; s2 -e2\<succ>v2-n2-> t2; s3 -c-n3-> t3|] ==>
       s1 -e1\<succ>v1-max (max n1 n2) n3-> t1 ∧
       s2 -e2\<succ>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 le_maxI1 le_maxI2)

    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

lemmas exec_elim_cases':

      [| s -Skip-n-> t; t = s ==> P |] ==> P

      [| s -c1.0;; c2.0-n-> t; !!s1. [| s -c1.0-n-> s1; s1 -c2.0-n-> t |] ==> P |]
      ==> P

      [| s -If (e) c1.0 Else c2.0-n-> t;
         !!s1 v.
            [| s -e>v-n-> s1; s1 -(if v ≠ Null then c1.0 else c2.0)-n-> t |] ==> P |]
      ==> P

      [| s -While (x) c-n-> t; [| s<x> = Null; t = s |] ==> P;
         !!s1. [| s<x> ≠ Null; s -c-n-> s1; s1 -While (x) c-n-> t |] ==> P |]
      ==> P

      [| s -x :== e-n-> t; !!s' v. [| s -e>v-n-> s'; t = lupd(x|->v) s' |] ==> P |]
      ==> P

      [| s -e1.0..f:==e2.0-n-> t;
         !!a s1 s2 v.
            [| s -e1.0>Addr a-n-> s1; s1 -e2.0>v-n-> s2; t = upd_obj a f v s2 |]
            ==> P |]
      ==> P

lemmas Meth_elim_cases:

      [| s -Meth Cm-n-> t;
         !!C a m.
            [| s<This> = Addr a; obj_class s a <=C C;
               init_locs (obj_class s a) m s -Impl (obj_class s a, m)-n-> t;
               Cm = (C, m) |]
            ==> P |]
      ==> P

lemmas Impl_elim_cases:

      [| s -Impl Cm-n-> t; !!n. [| s -body Cm-n-> t; n = Suc n |] ==> P |] ==> P

lemmas exec_elim_cases:

      [| s -Skip-n-> t; t = s ==> P |] ==> P

      [| s -c1.0;; c2.0-n-> t; !!s1. [| s -c1.0-n-> s1; s1 -c2.0-n-> t |] ==> P |]
      ==> P

      [| s -If (e) c1.0 Else c2.0-n-> t;
         !!s1 v.
            [| s -e>v-n-> s1; s1 -(if v ≠ Null then c1.0 else c2.0)-n-> t |] ==> P |]
      ==> P

      [| s -While (x) c-n-> t; [| s<x> = Null; t = s |] ==> P;
         !!s1. [| s<x> ≠ Null; s -c-n-> s1; s1 -While (x) c-n-> t |] ==> P |]
      ==> P

      [| s -x :== e-n-> t; !!s' v. [| s -e>v-n-> s'; t = lupd(x|->v) s' |] ==> P |]
      ==> P

      [| s -e1.0..f:==e2.0-n-> t;
         !!a s1 s2 v.
            [| s -e1.0>Addr a-n-> s1; s1 -e2.0>v-n-> s2; t = upd_obj a f v s2 |]
            ==> P |]
      ==> P

      [| s -Meth Cm-n-> t;
         !!C a m.
            [| s<This> = Addr a; obj_class s a <=C C;
               init_locs (obj_class s a) m s -Impl (obj_class s a, m)-n-> t;
               Cm = (C, m) |]
            ==> P |]
      ==> P

      [| s -Impl Cm-n-> t; !!n. [| s -body Cm-n-> t; n = Suc n |] ==> P |] ==> P

lemmas exec_elim_cases:

      [| s -Skip-n-> t; t = s ==> P |] ==> P

      [| s -c1.0;; c2.0-n-> t; !!s1. [| s -c1.0-n-> s1; s1 -c2.0-n-> t |] ==> P |]
      ==> P

      [| s -If (e) c1.0 Else c2.0-n-> t;
         !!s1 v.
            [| s -e>v-n-> s1; s1 -(if v ≠ Null then c1.0 else c2.0)-n-> t |] ==> P |]
      ==> P

      [| s -While (x) c-n-> t; [| s<x> = Null; t = s |] ==> P;
         !!s1. [| s<x> ≠ Null; s -c-n-> s1; s1 -While (x) c-n-> t |] ==> P |]
      ==> P

      [| s -x :== e-n-> t; !!s' v. [| s -e>v-n-> s'; t = lupd(x|->v) s' |] ==> P |]
      ==> P

      [| s -e1.0..f:==e2.0-n-> t;
         !!a s1 s2 v.
            [| s -e1.0>Addr a-n-> s1; s1 -e2.0>v-n-> s2; t = upd_obj a f v s2 |]
            ==> P |]
      ==> P

      [| s -Meth Cm-n-> t;
         !!C a m.
            [| s<This> = Addr a; obj_class s a <=C C;
               init_locs (obj_class s a) m s -Impl (obj_class s a, m)-n-> t;
               Cm = (C, m) |]
            ==> P |]
      ==> P

      [| s -Impl Cm-n-> t; !!n. [| s -body Cm-n-> t; n = Suc n |] ==> P |] ==> P

lemmas eval_elim_cases:

      [| s -new C>v-n-> t;
         !!a. [| new_Addr s = Addr a; v = Addr a; t = new_obj a C s |] ==> P |]
      ==> P

      [| s -Cast C e>v-n-> t;
         [| s -e>v-n-> t; case v of Null => True | Addr a => obj_class t a <=C C |]
         ==> P |]
      ==> P

      [| s -LAcc x>v-n-> t; [| v = s<x>; t = s |] ==> P |] ==> P

      [| s -e..f>v-n-> t; !!a. [| s -e>Addr a-n-> t; v = get_field t a f |] ==> P |]
      ==> P

      [| s -{C}e1.0..m(e2.0)>v-n-> t;
         !!a p s1 s2 s3.
            [| s -e1.0>a-n-> s1; s1 -e2.0>p-n-> s2;
               lupd(This|->a) (lupd(Par|->p) (del_locs s2)) -Meth (C, m)-n-> s3;
               v = s3<Res>; t = set_locs s2 s3 |]
            ==> P |]
      ==> P

lemma exec_eval_mono:

      (s -c-n-> t --> (∀m≥n. s -c-m-> t)) ∧ (s -e>v-n-> t --> (∀m≥n. s -e>v-m-> t))

lemmas exec_mono:

      [| s -c-n-> t; n ≤ m |] ==> s -c-m-> t

lemmas exec_mono:

      [| s -c-n-> t; n ≤ m |] ==> s -c-m-> t

lemmas eval_mono:

      [| s -e>v-n-> t; n ≤ m |] ==> s -e>v-m-> t

lemmas eval_mono:

      [| s -e>v-n-> t; n ≤ m |] ==> s -e>v-m-> t

lemma exec_exec_max:

      [| s1.0 -c1.0-n1.0-> t1.0; s2.0 -c2.0-n2.0-> t2.0 |]
      ==> s1.0 -c1.0-max n1.0 n2.0-> t1.0 ∧ s2.0 -c2.0-max n1.0 n2.0-> t2.0

lemma eval_exec_max:

      [| s1.0 -c-n1.0-> t1.0; s2.0 -e>v-n2.0-> t2.0 |]
      ==> s1.0 -c-max n1.0 n2.0-> t1.0 ∧ s2.0 -e>v-max n1.0 n2.0-> t2.0

lemma eval_eval_max:

      [| s1.0 -e1.0>v1.0-n1.0-> t1.0; s2.0 -e2.0>v2.0-n2.0-> t2.0 |]
      ==> s1.0 -e1.0>v1.0-max n1.0 n2.0-> t1.0 ∧ s2.0 -e2.0>v2.0-max n1.0 n2.0-> t2.0

lemma eval_eval_exec_max:

      [| s1.0 -e1.0>v1.0-n1.0-> t1.0; s2.0 -e2.0>v2.0-n2.0-> t2.0;
         s3.0 -c-n3.0-> t3.0 |]
      ==> s1.0 -e1.0>v1.0-max (max n1.0 n2.0) n3.0-> t1.0 ∧
          s2.0 -e2.0>v2.0-max (max n1.0 n2.0) n3.0-> t2.0 ∧
          s3.0 -c-max (max n1.0 n2.0) n3.0-> t3.0

lemma Impl_body_eq:

      (%t. ∃n. Z -Impl M-n-> t) = (%t. ∃n. Z -body M-n-> t)