src/HOL/NanoJava/OpSem.thy
author wenzelm
Sat Oct 17 14:43:18 2009 +0200 (2009-10-17)
changeset 32960 69916a850301
parent 23755 1c4672d130b1
child 54863 82acc20ded73
permissions -rw-r--r--
eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;
     1 (*  Title:      HOL/NanoJava/OpSem.thy
     2     Author:     David von Oheimb
     3     Copyright   2001 Technische Universitaet Muenchen
     4 *)
     5 
     6 header "Operational Evaluation Semantics"
     7 
     8 theory OpSem imports State begin
     9 
    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"
    18 
    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"
    21 
    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"
    26 
    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'"
    31 
    32 | FAcc: "   s -e\<succ>Addr a-n\<rightarrow> s' ==>
    33             s -e..f\<succ>get_field s' a f-n\<rightarrow> s'"
    34 
    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"
    37 
    38 | NewC: "   new_Addr s = Addr a ==>
    39             s -new C\<succ>Addr a-n\<rightarrow> new_obj a C s"
    40 
    41 | Cast: "[| s -e\<succ>v-n\<rightarrow> s';
    42             case v of Null => True | Addr a => obj_class s' a \<preceq>C C |] ==>
    43             s -Cast C e\<succ>v-n\<rightarrow> s'"
    44 
    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"
    48 
    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'"
    52 
    53 | Impl: "   s -body Cm-    n\<rightarrow> s' ==>
    54             s -Impl Cm-Suc n\<rightarrow> s'"
    55 
    56 
    57 inductive_cases exec_elim_cases':
    58                                   "s -Skip            -n\<rightarrow> t"
    59                                   "s -c1;; c2         -n\<rightarrow> t"
    60                                   "s -If(e) c1 Else c2-n\<rightarrow> t"
    61                                   "s -While(x) c      -n\<rightarrow> t"
    62                                   "s -x:==e           -n\<rightarrow> t"
    63                                   "s -e1..f:==e2      -n\<rightarrow> t"
    64 inductive_cases Meth_elim_cases:  "s -Meth Cm         -n\<rightarrow> t"
    65 inductive_cases Impl_elim_cases:  "s -Impl Cm         -n\<rightarrow> t"
    66 lemmas exec_elim_cases = exec_elim_cases' Meth_elim_cases Impl_elim_cases
    67 inductive_cases eval_elim_cases:
    68                                   "s -new C         \<succ>v-n\<rightarrow> t"
    69                                   "s -Cast C e      \<succ>v-n\<rightarrow> t"
    70                                   "s -LAcc x        \<succ>v-n\<rightarrow> t"
    71                                   "s -e..f          \<succ>v-n\<rightarrow> t"
    72                                   "s -{C}e1..m(e2)  \<succ>v-n\<rightarrow> t"
    73 
    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 *)
    79 apply clarify
    80 apply (rename_tac n)
    81 apply (case_tac n)
    82 apply (blast intro:exec_eval.intros)+
    83 done
    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"
    89 by (fast intro: exec_mono le_maxI1 le_maxI2)
    90 
    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"
    93 by (fast intro: eval_mono exec_mono le_maxI1 le_maxI2)
    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"
    97 by (fast intro: eval_mono le_maxI1 le_maxI2)
    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)
   105 by (fast intro: exec_mono eval_mono le_maxI1 le_maxI2)
   106 
   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)"
   108 apply (rule ext)
   109 apply (fast elim: exec_elim_cases intro: exec_eval.Impl)
   110 done
   111 
   112 end