src/HOL/NanoJava/OpSem.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 32960 69916a850301
child 54863 82acc20ded73
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11376
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
     1
(*  Title:      HOL/NanoJava/OpSem.thy
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
     2
    Author:     David von Oheimb
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
     3
    Copyright   2001 Technische Universitaet Muenchen
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
     4
*)
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
     5
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
     6
header "Operational Evaluation Semantics"
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
     7
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 11772
diff changeset
     8
theory OpSem imports State begin
11376
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
     9
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    10
inductive
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    11
  exec :: "[state,stmt,    nat,state] => bool" ("_ -_-_\<rightarrow> _"  [98,90,   65,98] 89)
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    12
  and eval :: "[state,expr,val,nat,state] => bool" ("_ -_\<succ>_-_\<rightarrow> _"[98,95,99,65,98] 89)
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    13
where
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    14
  Skip: "   s -Skip-n\<rightarrow> s"
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    15
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    16
| Comp: "[| s0 -c1-n\<rightarrow> s1; s1 -c2-n\<rightarrow> s2 |] ==>
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    17
            s0 -c1;; c2-n\<rightarrow> s2"
11376
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
    18
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    19
| Cond: "[| s0 -e\<succ>v-n\<rightarrow> s1; s1 -(if v\<noteq>Null then c1 else c2)-n\<rightarrow> s2 |] ==>
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    20
            s0 -If(e) c1 Else c2-n\<rightarrow> s2"
11376
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
    21
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    22
| LoopF:"   s0<x> = Null ==>
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    23
            s0 -While(x) c-n\<rightarrow> s0"
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    24
| LoopT:"[| s0<x> \<noteq> Null; s0 -c-n\<rightarrow> s1; s1 -While(x) c-n\<rightarrow> s2 |] ==>
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    25
            s0 -While(x) c-n\<rightarrow> s2"
11476
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
    26
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    27
| LAcc: "   s -LAcc x\<succ>s<x>-n\<rightarrow> s"
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    28
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    29
| LAss: "   s -e\<succ>v-n\<rightarrow> s' ==>
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    30
            s -x:==e-n\<rightarrow> lupd(x\<mapsto>v) s'"
11376
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
    31
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    32
| FAcc: "   s -e\<succ>Addr a-n\<rightarrow> s' ==>
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    33
            s -e..f\<succ>get_field s' a f-n\<rightarrow> s'"
11476
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
    34
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    35
| FAss: "[| s0 -e1\<succ>Addr a-n\<rightarrow> s1;  s1 -e2\<succ>v-n\<rightarrow> s2 |] ==>
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    36
            s0 -e1..f:==e2-n\<rightarrow> upd_obj a f v s2"
11476
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
    37
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    38
| NewC: "   new_Addr s = Addr a ==>
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    39
            s -new C\<succ>Addr a-n\<rightarrow> new_obj a C s"
11376
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
    40
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    41
| Cast: "[| s -e\<succ>v-n\<rightarrow> s';
11476
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
    42
            case v of Null => True | Addr a => obj_class s' a \<preceq>C C |] ==>
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    43
            s -Cast C e\<succ>v-n\<rightarrow> s'"
11376
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
    44
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    45
| Call: "[| s0 -e1\<succ>a-n\<rightarrow> s1; s1 -e2\<succ>p-n\<rightarrow> s2; 
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    46
            lupd(This\<mapsto>a)(lupd(Par\<mapsto>p)(del_locs s2)) -Meth (C,m)-n\<rightarrow> s3
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    47
     |] ==> s0 -{C}e1..m(e2)\<succ>s3<Res>-n\<rightarrow> set_locs s2 s3"
11376
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
    48
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    49
| Meth: "[| s<This> = Addr a; D = obj_class s a; D\<preceq>C C;
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    50
            init_locs D m s -Impl (D,m)-n\<rightarrow> s' |] ==>
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    51
            s -Meth (C,m)-n\<rightarrow> s'"
11376
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
    52
23755
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    53
| Impl: "   s -body Cm-    n\<rightarrow> s' ==>
1c4672d130b1 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    54
            s -Impl Cm-Suc n\<rightarrow> s'"
11376
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
    55
11476
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
    56
11376
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
    57
inductive_cases exec_elim_cases':
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23755
diff changeset
    58
                                  "s -Skip            -n\<rightarrow> t"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23755
diff changeset
    59
                                  "s -c1;; c2         -n\<rightarrow> t"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23755
diff changeset
    60
                                  "s -If(e) c1 Else c2-n\<rightarrow> t"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23755
diff changeset
    61
                                  "s -While(x) c      -n\<rightarrow> t"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23755
diff changeset
    62
                                  "s -x:==e           -n\<rightarrow> t"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23755
diff changeset
    63
                                  "s -e1..f:==e2      -n\<rightarrow> t"
11508
168dbdaedb71 cosmetics
oheimb
parents: 11507
diff changeset
    64
inductive_cases Meth_elim_cases:  "s -Meth Cm         -n\<rightarrow> t"
168dbdaedb71 cosmetics
oheimb
parents: 11507
diff changeset
    65
inductive_cases Impl_elim_cases:  "s -Impl Cm         -n\<rightarrow> t"
11376
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
    66
lemmas exec_elim_cases = exec_elim_cases' Meth_elim_cases Impl_elim_cases
11476
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
    67
inductive_cases eval_elim_cases:
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23755
diff changeset
    68
                                  "s -new C         \<succ>v-n\<rightarrow> t"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23755
diff changeset
    69
                                  "s -Cast C e      \<succ>v-n\<rightarrow> t"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23755
diff changeset
    70
                                  "s -LAcc x        \<succ>v-n\<rightarrow> t"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23755
diff changeset
    71
                                  "s -e..f          \<succ>v-n\<rightarrow> t"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 23755
diff changeset
    72
                                  "s -{C}e1..m(e2)  \<succ>v-n\<rightarrow> t"
11376
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
    73
11476
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
    74
lemma exec_eval_mono [rule_format]: 
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
    75
  "(s -c  -n\<rightarrow> t \<longrightarrow> (\<forall>m. n \<le> m \<longrightarrow> s -c  -m\<rightarrow> t)) \<and>
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
    76
   (s -e\<succ>v-n\<rightarrow> t \<longrightarrow> (\<forall>m. n \<le> m \<longrightarrow> s -e\<succ>v-m\<rightarrow> t))"
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
    77
apply (rule exec_eval.induct)
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
    78
prefer 14 (* Impl *)
11376
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
    79
apply clarify
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
    80
apply (rename_tac n)
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
    81
apply (case_tac n)
11508
168dbdaedb71 cosmetics
oheimb
parents: 11507
diff changeset
    82
apply (blast intro:exec_eval.intros)+
11376
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
    83
done
11476
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
    84
lemmas exec_mono = exec_eval_mono [THEN conjunct1, rule_format]
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
    85
lemmas eval_mono = exec_eval_mono [THEN conjunct2, rule_format]
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
    86
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
    87
lemma exec_exec_max: "\<lbrakk>s1 -c1-    n1   \<rightarrow> t1 ; s2 -c2-       n2\<rightarrow> t2\<rbrakk> \<Longrightarrow> 
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
    88
                       s1 -c1-max n1 n2\<rightarrow> t1 \<and> s2 -c2-max n1 n2\<rightarrow> t2"
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
    89
by (fast intro: exec_mono le_maxI1 le_maxI2)
11376
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
    90
11476
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
    91
lemma eval_exec_max: "\<lbrakk>s1 -c-    n1   \<rightarrow> t1 ; s2 -e\<succ>v-       n2\<rightarrow> t2\<rbrakk> \<Longrightarrow> 
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
    92
                       s1 -c-max n1 n2\<rightarrow> t1 \<and> s2 -e\<succ>v-max n1 n2\<rightarrow> t2"
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
    93
by (fast intro: eval_mono exec_mono le_maxI1 le_maxI2)
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
    94
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
    95
lemma eval_eval_max: "\<lbrakk>s1 -e1\<succ>v1-    n1   \<rightarrow> t1 ; s2 -e2\<succ>v2-       n2\<rightarrow> t2\<rbrakk> \<Longrightarrow> 
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
    96
                       s1 -e1\<succ>v1-max n1 n2\<rightarrow> t1 \<and> s2 -e2\<succ>v2-max n1 n2\<rightarrow> t2"
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
    97
by (fast intro: eval_mono le_maxI1 le_maxI2)
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
    98
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
    99
lemma eval_eval_exec_max: 
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
   100
 "\<lbrakk>s1 -e1\<succ>v1-n1\<rightarrow> t1; s2 -e2\<succ>v2-n2\<rightarrow> t2; s3 -c-n3\<rightarrow> t3\<rbrakk> \<Longrightarrow> 
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
   101
   s1 -e1\<succ>v1-max (max n1 n2) n3\<rightarrow> t1 \<and> 
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
   102
   s2 -e2\<succ>v2-max (max n1 n2) n3\<rightarrow> t2 \<and> 
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
   103
   s3 -c    -max (max n1 n2) n3\<rightarrow> t3"
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
   104
apply (drule (1) eval_eval_max, erule thin_rl)
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
   105
by (fast intro: exec_mono eval_mono le_maxI1 le_maxI2)
11376
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
   106
11565
ab004c0ecc63 Minor improvements, added Example
oheimb
parents: 11558
diff changeset
   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)"
11376
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
   108
apply (rule ext)
11476
06c1998340a8 changed to full expressions with side effects
oheimb
parents: 11376
diff changeset
   109
apply (fast elim: exec_elim_cases intro: exec_eval.Impl)
11376
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
   110
done
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
   111
bf98ad1c22c6 added NanoJava
oheimb
parents:
diff changeset
   112
end