src/HOL/NanoJava/OpSem.thy
author oheimb
Wed Aug 08 12:36:48 2001 +0200 (2001-08-08)
changeset 11476 06c1998340a8
parent 11376 bf98ad1c22c6
child 11486 8f32860eac3a
permissions -rw-r--r--
changed to full expressions with side effects
oheimb@11376
     1
(*  Title:      HOL/NanoJava/OpSem.thy
oheimb@11376
     2
    ID:         $Id$
oheimb@11376
     3
    Author:     David von Oheimb
oheimb@11376
     4
    Copyright   2001 Technische Universitaet Muenchen
oheimb@11376
     5
*)
oheimb@11376
     6
oheimb@11376
     7
header "Operational Evaluation Semantics"
oheimb@11376
     8
oheimb@11376
     9
theory OpSem = State:
oheimb@11376
    10
oheimb@11376
    11
consts
oheimb@11476
    12
 exec :: "(state \<times> stmt       \<times> nat \<times> state) set"
oheimb@11476
    13
 eval :: "(state \<times> expr \<times> val \<times> nat \<times> state) set"
oheimb@11376
    14
syntax (xsymbols)
oheimb@11476
    15
 exec :: "[state,stmt,    nat,state] => bool" ("_ -_-_\<rightarrow> _"  [98,90,   99,98] 89)
oheimb@11476
    16
 eval :: "[state,expr,val,nat,state] => bool" ("_ -_\<succ>_-_\<rightarrow> _"[98,95,99,99,98] 89)
oheimb@11376
    17
syntax
oheimb@11476
    18
 exec :: "[state,stmt,    nat,state] => bool" ("_ -_-_-> _"  [98,90,   99,98]89)
oheimb@11476
    19
 eval :: "[state,expr,val,nat,state] => bool" ("_ -_>_-_-> _"[98,95,99,99,98]89)
oheimb@11376
    20
translations
oheimb@11476
    21
 "s -c  -n-> s'" == "(s, c,    n, s') \<in> exec"
oheimb@11476
    22
 "s -e>v-n-> s'" == "(s, e, v, n, s') \<in> eval"
oheimb@11376
    23
oheimb@11476
    24
inductive exec eval intros
oheimb@11376
    25
oheimb@11376
    26
  Skip: "   s -Skip-n-> s"
oheimb@11376
    27
oheimb@11376
    28
  Comp: "[| s0 -c1-n-> s1; s1 -c2-n-> s2 |] ==>
oheimb@11376
    29
            s0 -c1;; c2-n-> s2"
oheimb@11376
    30
oheimb@11476
    31
  Cond: "[| s0 -e>v-n-> s1; s1 -(if v\<noteq>Null then c1 else c2)-n-> s2 |] ==>
oheimb@11476
    32
            s0 -If(e) c1 Else c2-n-> s2"
oheimb@11476
    33
oheimb@11476
    34
  LoopF:"   s0<x> = Null ==>
oheimb@11476
    35
            s0 -While(x) c-n-> s0"
oheimb@11476
    36
  LoopT:"[| s0<x> \<noteq> Null; s0 -c-n-> s1; s1 -While(x) c-n-> s2 |] ==>
oheimb@11476
    37
            s0 -While(x) c-n-> s2"
oheimb@11376
    38
oheimb@11476
    39
  LAcc: "   s -LAcc x>s<x>-n-> s"
oheimb@11476
    40
oheimb@11476
    41
  LAss: "   s -e>v-n-> s' ==>
oheimb@11476
    42
            s -x:==e-n-> lupd(x\<mapsto>v) s'"
oheimb@11476
    43
oheimb@11476
    44
  FAcc: "   s -e>Addr a-n-> s' ==>
oheimb@11476
    45
            s -e..f>get_field s' a f-n-> s'"
oheimb@11476
    46
oheimb@11476
    47
  FAss: "[| s0 -e1>Addr a-n-> s1;  s1 -e2>v-n-> s2 |] ==>
oheimb@11476
    48
            s0 -e1..f:==e2-n-> upd_obj a f v s2"
oheimb@11376
    49
oheimb@11376
    50
  NewC: "   new_Addr s = Addr a ==>
oheimb@11476
    51
            s -new C>Addr a-n-> new_obj a C s"
oheimb@11376
    52
oheimb@11476
    53
  Cast: "[| s -e>v-n-> s';
oheimb@11476
    54
            case v of Null => True | Addr a => obj_class s' a \<preceq>C C |] ==>
oheimb@11476
    55
            s -Cast C e>v-n-> s'"
oheimb@11376
    56
oheimb@11476
    57
  Call: "[| s0 -e1>a-n-> s1; s1 -e2>p-n-> s2; 
oheimb@11476
    58
            lupd(This\<mapsto>a)(lupd(Param\<mapsto>p)(init_locs C m s2)) -Meth C m-n-> s3
oheimb@11476
    59
     |] ==> s0 -{C}e1..m(e2)>s3<Res>-n-> set_locs s2 s3"
oheimb@11376
    60
oheimb@11376
    61
  Meth: "[| s<This> = Addr a; obj_class s a\<preceq>C C;
oheimb@11376
    62
            s -Impl (obj_class s a) m-n-> s' |] ==>
oheimb@11376
    63
            s -Meth C m-n-> s'"
oheimb@11376
    64
oheimb@11476
    65
  Impl: "   s -body C m-n-> s' ==>
oheimb@11376
    66
            s -Impl C m-Suc n-> s'"
oheimb@11376
    67
oheimb@11476
    68
oheimb@11376
    69
inductive_cases exec_elim_cases':
oheimb@11476
    70
	"s -Skip            -n\<rightarrow> t"
oheimb@11476
    71
	"s -c1;; c2         -n\<rightarrow> t"
oheimb@11476
    72
	"s -If(e) c1 Else c2-n\<rightarrow> t"
oheimb@11476
    73
	"s -While(x) c      -n\<rightarrow> t"
oheimb@11476
    74
	"s -x:==e           -n\<rightarrow> t"
oheimb@11476
    75
	"s -e1..f:==e2      -n\<rightarrow> t"
oheimb@11476
    76
inductive_cases Meth_elim_cases: "s -Meth C m-n\<rightarrow> t"
oheimb@11476
    77
inductive_cases Impl_elim_cases: "s -Impl C m-n\<rightarrow> t"
oheimb@11376
    78
lemmas exec_elim_cases = exec_elim_cases' Meth_elim_cases Impl_elim_cases
oheimb@11476
    79
inductive_cases eval_elim_cases:
oheimb@11476
    80
	"s -new C         \<succ>v-n\<rightarrow> t"
oheimb@11476
    81
	"s -Cast C e      \<succ>v-n\<rightarrow> t"
oheimb@11476
    82
	"s -LAcc x        \<succ>v-n\<rightarrow> t"
oheimb@11476
    83
	"s -e..f          \<succ>v-n\<rightarrow> t"
oheimb@11476
    84
	"s -{C}e1..m(e2)  \<succ>v-n\<rightarrow> t"
oheimb@11376
    85
oheimb@11476
    86
lemma exec_eval_mono [rule_format]: 
oheimb@11476
    87
  "(s -c  -n\<rightarrow> t \<longrightarrow> (\<forall>m. n \<le> m \<longrightarrow> s -c  -m\<rightarrow> t)) \<and>
oheimb@11476
    88
   (s -e\<succ>v-n\<rightarrow> t \<longrightarrow> (\<forall>m. n \<le> m \<longrightarrow> s -e\<succ>v-m\<rightarrow> t))"
oheimb@11476
    89
apply (rule exec_eval.induct)
oheimb@11476
    90
prefer 14 (* Impl *)
oheimb@11376
    91
apply clarify
oheimb@11376
    92
apply (rename_tac n)
oheimb@11376
    93
apply (case_tac n)
oheimb@11476
    94
apply  (blast intro:exec_eval.intros)+
oheimb@11376
    95
done
oheimb@11476
    96
lemmas exec_mono = exec_eval_mono [THEN conjunct1, rule_format]
oheimb@11476
    97
lemmas eval_mono = exec_eval_mono [THEN conjunct2, rule_format]
oheimb@11476
    98
oheimb@11476
    99
lemma exec_exec_max: "\<lbrakk>s1 -c1-    n1   \<rightarrow> t1 ; s2 -c2-       n2\<rightarrow> t2\<rbrakk> \<Longrightarrow> 
oheimb@11476
   100
                       s1 -c1-max n1 n2\<rightarrow> t1 \<and> s2 -c2-max n1 n2\<rightarrow> t2"
oheimb@11476
   101
by (fast intro: exec_mono le_maxI1 le_maxI2)
oheimb@11376
   102
oheimb@11476
   103
lemma eval_exec_max: "\<lbrakk>s1 -c-    n1   \<rightarrow> t1 ; s2 -e\<succ>v-       n2\<rightarrow> t2\<rbrakk> \<Longrightarrow> 
oheimb@11476
   104
                       s1 -c-max n1 n2\<rightarrow> t1 \<and> s2 -e\<succ>v-max n1 n2\<rightarrow> t2"
oheimb@11476
   105
by (fast intro: eval_mono exec_mono le_maxI1 le_maxI2)
oheimb@11476
   106
oheimb@11476
   107
lemma eval_eval_max: "\<lbrakk>s1 -e1\<succ>v1-    n1   \<rightarrow> t1 ; s2 -e2\<succ>v2-       n2\<rightarrow> t2\<rbrakk> \<Longrightarrow> 
oheimb@11476
   108
                       s1 -e1\<succ>v1-max n1 n2\<rightarrow> t1 \<and> s2 -e2\<succ>v2-max n1 n2\<rightarrow> t2"
oheimb@11476
   109
by (fast intro: eval_mono le_maxI1 le_maxI2)
oheimb@11476
   110
oheimb@11476
   111
lemma eval_eval_exec_max: 
oheimb@11476
   112
 "\<lbrakk>s1 -e1\<succ>v1-n1\<rightarrow> t1; s2 -e2\<succ>v2-n2\<rightarrow> t2; s3 -c-n3\<rightarrow> t3\<rbrakk> \<Longrightarrow> 
oheimb@11476
   113
   s1 -e1\<succ>v1-max (max n1 n2) n3\<rightarrow> t1 \<and> 
oheimb@11476
   114
   s2 -e2\<succ>v2-max (max n1 n2) n3\<rightarrow> t2 \<and> 
oheimb@11476
   115
   s3 -c    -max (max n1 n2) n3\<rightarrow> t3"
oheimb@11476
   116
apply (drule (1) eval_eval_max, erule thin_rl)
oheimb@11476
   117
by (fast intro: exec_mono eval_mono le_maxI1 le_maxI2)
oheimb@11376
   118
oheimb@11376
   119
lemma Impl_body_eq: "(\<lambda>t. \<exists>n. z -Impl C m-n\<rightarrow> t) = (\<lambda>t. \<exists>n. z -body C m-n\<rightarrow> t)"
oheimb@11376
   120
apply (rule ext)
oheimb@11476
   121
apply (fast elim: exec_elim_cases intro: exec_eval.Impl)
oheimb@11376
   122
done
oheimb@11376
   123
oheimb@11376
   124
end