src/HOL/NanoJava/OpSem.thy
changeset 23755 1c4672d130b1
parent 16417 9bc16273c2d4
child 32960 69916a850301
     1.1 --- a/src/HOL/NanoJava/OpSem.thy	Wed Jul 11 11:27:46 2007 +0200
     1.2 +++ b/src/HOL/NanoJava/OpSem.thy	Wed Jul 11 11:28:13 2007 +0200
     1.3 @@ -8,61 +8,51 @@
     1.4  
     1.5  theory OpSem imports State begin
     1.6  
     1.7 -consts
     1.8 - exec :: "(state \<times> stmt       \<times> nat \<times> state) set"
     1.9 - eval :: "(state \<times> expr \<times> val \<times> nat \<times> state) set"
    1.10 -syntax (xsymbols)
    1.11 - exec :: "[state,stmt,    nat,state] => bool" ("_ -_-_\<rightarrow> _"  [98,90,   65,98] 89)
    1.12 - eval :: "[state,expr,val,nat,state] => bool" ("_ -_\<succ>_-_\<rightarrow> _"[98,95,99,65,98] 89)
    1.13 -syntax
    1.14 - exec :: "[state,stmt,    nat,state] => bool" ("_ -_-_-> _"  [98,90,   65,98]89)
    1.15 - eval :: "[state,expr,val,nat,state] => bool" ("_ -_>_-_-> _"[98,95,99,65,98]89)
    1.16 -translations
    1.17 - "s -c  -n-> s'" == "(s, c,    n, s') \<in> exec"
    1.18 - "s -e>v-n-> s'" == "(s, e, v, n, s') \<in> eval"
    1.19 +inductive
    1.20 +  exec :: "[state,stmt,    nat,state] => bool" ("_ -_-_\<rightarrow> _"  [98,90,   65,98] 89)
    1.21 +  and eval :: "[state,expr,val,nat,state] => bool" ("_ -_\<succ>_-_\<rightarrow> _"[98,95,99,65,98] 89)
    1.22 +where
    1.23 +  Skip: "   s -Skip-n\<rightarrow> s"
    1.24 +
    1.25 +| Comp: "[| s0 -c1-n\<rightarrow> s1; s1 -c2-n\<rightarrow> s2 |] ==>
    1.26 +            s0 -c1;; c2-n\<rightarrow> s2"
    1.27  
    1.28 -inductive exec eval intros
    1.29 -  Skip: "   s -Skip-n-> s"
    1.30 -
    1.31 -  Comp: "[| s0 -c1-n-> s1; s1 -c2-n-> s2 |] ==>
    1.32 -            s0 -c1;; c2-n-> s2"
    1.33 +| Cond: "[| s0 -e\<succ>v-n\<rightarrow> s1; s1 -(if v\<noteq>Null then c1 else c2)-n\<rightarrow> s2 |] ==>
    1.34 +            s0 -If(e) c1 Else c2-n\<rightarrow> s2"
    1.35  
    1.36 -  Cond: "[| s0 -e>v-n-> s1; s1 -(if v\<noteq>Null then c1 else c2)-n-> s2 |] ==>
    1.37 -            s0 -If(e) c1 Else c2-n-> s2"
    1.38 +| LoopF:"   s0<x> = Null ==>
    1.39 +            s0 -While(x) c-n\<rightarrow> s0"
    1.40 +| LoopT:"[| s0<x> \<noteq> Null; s0 -c-n\<rightarrow> s1; s1 -While(x) c-n\<rightarrow> s2 |] ==>
    1.41 +            s0 -While(x) c-n\<rightarrow> s2"
    1.42  
    1.43 -  LoopF:"   s0<x> = Null ==>
    1.44 -            s0 -While(x) c-n-> s0"
    1.45 -  LoopT:"[| s0<x> \<noteq> Null; s0 -c-n-> s1; s1 -While(x) c-n-> s2 |] ==>
    1.46 -            s0 -While(x) c-n-> s2"
    1.47 +| LAcc: "   s -LAcc x\<succ>s<x>-n\<rightarrow> s"
    1.48 +
    1.49 +| LAss: "   s -e\<succ>v-n\<rightarrow> s' ==>
    1.50 +            s -x:==e-n\<rightarrow> lupd(x\<mapsto>v) s'"
    1.51  
    1.52 -  LAcc: "   s -LAcc x>s<x>-n-> s"
    1.53 -
    1.54 -  LAss: "   s -e>v-n-> s' ==>
    1.55 -            s -x:==e-n-> lupd(x\<mapsto>v) s'"
    1.56 +| FAcc: "   s -e\<succ>Addr a-n\<rightarrow> s' ==>
    1.57 +            s -e..f\<succ>get_field s' a f-n\<rightarrow> s'"
    1.58  
    1.59 -  FAcc: "   s -e>Addr a-n-> s' ==>
    1.60 -            s -e..f>get_field s' a f-n-> s'"
    1.61 +| FAss: "[| s0 -e1\<succ>Addr a-n\<rightarrow> s1;  s1 -e2\<succ>v-n\<rightarrow> s2 |] ==>
    1.62 +            s0 -e1..f:==e2-n\<rightarrow> upd_obj a f v s2"
    1.63  
    1.64 -  FAss: "[| s0 -e1>Addr a-n-> s1;  s1 -e2>v-n-> s2 |] ==>
    1.65 -            s0 -e1..f:==e2-n-> upd_obj a f v s2"
    1.66 -
    1.67 -  NewC: "   new_Addr s = Addr a ==>
    1.68 -            s -new C>Addr a-n-> new_obj a C s"
    1.69 +| NewC: "   new_Addr s = Addr a ==>
    1.70 +            s -new C\<succ>Addr a-n\<rightarrow> new_obj a C s"
    1.71  
    1.72 -  Cast: "[| s -e>v-n-> s';
    1.73 +| Cast: "[| s -e\<succ>v-n\<rightarrow> s';
    1.74              case v of Null => True | Addr a => obj_class s' a \<preceq>C C |] ==>
    1.75 -            s -Cast C e>v-n-> s'"
    1.76 +            s -Cast C e\<succ>v-n\<rightarrow> s'"
    1.77  
    1.78 -  Call: "[| s0 -e1>a-n-> s1; s1 -e2>p-n-> s2; 
    1.79 -            lupd(This\<mapsto>a)(lupd(Par\<mapsto>p)(del_locs s2)) -Meth (C,m)-n-> s3
    1.80 -     |] ==> s0 -{C}e1..m(e2)>s3<Res>-n-> set_locs s2 s3"
    1.81 +| Call: "[| s0 -e1\<succ>a-n\<rightarrow> s1; s1 -e2\<succ>p-n\<rightarrow> s2; 
    1.82 +            lupd(This\<mapsto>a)(lupd(Par\<mapsto>p)(del_locs s2)) -Meth (C,m)-n\<rightarrow> s3
    1.83 +     |] ==> s0 -{C}e1..m(e2)\<succ>s3<Res>-n\<rightarrow> set_locs s2 s3"
    1.84  
    1.85 -  Meth: "[| s<This> = Addr a; D = obj_class s a; D\<preceq>C C;
    1.86 -            init_locs D m s -Impl (D,m)-n-> s' |] ==>
    1.87 -            s -Meth (C,m)-n-> s'"
    1.88 +| Meth: "[| s<This> = Addr a; D = obj_class s a; D\<preceq>C C;
    1.89 +            init_locs D m s -Impl (D,m)-n\<rightarrow> s' |] ==>
    1.90 +            s -Meth (C,m)-n\<rightarrow> s'"
    1.91  
    1.92 -  Impl: "   s -body Cm-    n-> s' ==>
    1.93 -            s -Impl Cm-Suc n-> s'"
    1.94 +| Impl: "   s -body Cm-    n\<rightarrow> s' ==>
    1.95 +            s -Impl Cm-Suc n\<rightarrow> s'"
    1.96  
    1.97  
    1.98  inductive_cases exec_elim_cases':