src/HOL/Bali/Trans.thy
author schirmer
Wed Jul 10 15:07:02 2002 +0200 (2002-07-10)
changeset 13337 f75dfc606ac7
parent 12925 99131847fb93
child 13354 8c8eafb63746
permissions -rw-r--r--
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
wenzelm@12857
     1
(*  Title:      HOL/Bali/Trans.thy
schirmer@12854
     2
    ID:         $Id$
schirmer@12854
     3
    Author:     David von Oheimb
wenzelm@12858
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
schirmer@12854
     5
schirmer@12854
     6
Operational transition (small-step) semantics of the 
schirmer@12854
     7
execution of Java expressions and statements
schirmer@12854
     8
schirmer@12854
     9
PRELIMINARY!!!!!!!!
schirmer@12854
    10
*)
schirmer@12854
    11
schirmer@13337
    12
theory Trans = Evaln:
schirmer@13337
    13
(*
schirmer@13337
    14
constdefs inj_stmt:: "stmt \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>s" 83)
schirmer@13337
    15
    "\<langle>s\<rangle>\<^sub>s \<equiv> In1r s"
schirmer@13337
    16
schirmer@13337
    17
constdefs inj_expr:: "expr \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>e" 83)
schirmer@13337
    18
    "\<langle>e\<rangle>\<^sub>e \<equiv> In1l e"
schirmer@13337
    19
*)
schirmer@13337
    20
axclass inj_term < "type"
schirmer@13337
    21
consts inj_term:: "'a::inj_term \<Rightarrow> term" ("\<langle>_\<rangle>" 83)
schirmer@13337
    22
schirmer@13337
    23
instance stmt::inj_term ..
schirmer@13337
    24
schirmer@13337
    25
defs (overloaded)
schirmer@13337
    26
stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c"
schirmer@13337
    27
schirmer@13337
    28
lemma stmt_inj_term_simp: "\<langle>c::stmt\<rangle> = In1r c"
schirmer@13337
    29
by (simp add: stmt_inj_term_def)
schirmer@13337
    30
schirmer@13337
    31
instance expr::inj_term ..
schirmer@13337
    32
schirmer@13337
    33
defs (overloaded)
schirmer@13337
    34
expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e"
schirmer@13337
    35
schirmer@13337
    36
lemma expr_inj_term_simp: "\<langle>e::expr\<rangle> = In1l e"
schirmer@13337
    37
by (simp add: expr_inj_term_def)
schirmer@13337
    38
schirmer@13337
    39
instance var::inj_term ..
schirmer@13337
    40
schirmer@13337
    41
defs (overloaded)
schirmer@13337
    42
var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v"
schirmer@13337
    43
schirmer@13337
    44
lemma var_inj_term_simp: "\<langle>v::var\<rangle> = In2 v"
schirmer@13337
    45
by (simp add: var_inj_term_def)
schirmer@13337
    46
schirmer@13337
    47
instance "list":: (type) inj_term ..
schirmer@13337
    48
schirmer@13337
    49
defs (overloaded)
schirmer@13337
    50
expr_list_inj_term_def: "\<langle>es::expr list\<rangle> \<equiv> In3 es"
schirmer@13337
    51
schirmer@13337
    52
lemma expr_list_inj_term_simp: "\<langle>es::expr list\<rangle> = In3 es"
schirmer@13337
    53
by (simp add: expr_list_inj_term_def)
schirmer@13337
    54
schirmer@13337
    55
constdefs groundVar:: "var \<Rightarrow> bool"
schirmer@13337
    56
"groundVar v \<equiv> (case v of
schirmer@13337
    57
                   LVar ln \<Rightarrow> True
schirmer@13337
    58
                 | {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a
schirmer@13337
    59
                 | e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i
schirmer@13337
    60
                 | InsInitV c v \<Rightarrow> False)"
schirmer@13337
    61
schirmer@13337
    62
lemma groundVar_cases [consumes 1, case_names LVar FVar AVar]:
schirmer@13337
    63
  assumes ground: "groundVar v" and
schirmer@13337
    64
          LVar: "\<And> ln. \<lbrakk>v=LVar ln\<rbrakk> \<Longrightarrow> P" and
schirmer@13337
    65
          FVar: "\<And> accC statDeclC stat a fn. 
schirmer@13337
    66
                    \<lbrakk>v={accC,statDeclC,stat}(Lit a)..fn\<rbrakk> \<Longrightarrow> P" and
schirmer@13337
    67
          AVar: "\<And> a i. \<lbrakk>v=(Lit a).[Lit i]\<rbrakk> \<Longrightarrow> P"
schirmer@13337
    68
  shows "P"
schirmer@13337
    69
proof -
schirmer@13337
    70
  from ground LVar FVar AVar
schirmer@13337
    71
  show ?thesis
schirmer@13337
    72
    apply (cases v)
schirmer@13337
    73
    apply (simp add: groundVar_def)
schirmer@13337
    74
    apply (simp add: groundVar_def,blast)
schirmer@13337
    75
    apply (simp add: groundVar_def,blast)
schirmer@13337
    76
    apply (simp add: groundVar_def)
schirmer@13337
    77
    done
schirmer@13337
    78
qed
schirmer@13337
    79
schirmer@13337
    80
constdefs groundExprs:: "expr list \<Rightarrow> bool"
schirmer@13337
    81
"groundExprs es \<equiv> list_all (\<lambda> e. \<exists> v. e=Lit v) es"
schirmer@13337
    82
  
schirmer@13337
    83
consts the_val:: "expr \<Rightarrow> val"
schirmer@13337
    84
primrec
schirmer@13337
    85
"the_val (Lit v) = v"
schirmer@13337
    86
schirmer@13337
    87
consts the_var:: "prog \<Rightarrow> state \<Rightarrow> var \<Rightarrow> (vvar \<times> state)"
schirmer@13337
    88
primrec
schirmer@13337
    89
"the_var G s (LVar ln)                    =(lvar ln (store s),s)"
schirmer@13337
    90
the_var_FVar_def:
schirmer@13337
    91
"the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s"
schirmer@13337
    92
the_var_AVar_def:
schirmer@13337
    93
"the_var G s(a.[i])                       =avar G (the_val i) (the_val a) s"
schirmer@13337
    94
schirmer@13337
    95
lemma the_var_FVar_simp[simp]:
schirmer@13337
    96
"the_var G s ({accC,statDeclC,stat}(Lit a)..fn) = fvar statDeclC stat fn a s"
schirmer@13337
    97
by (simp)
schirmer@13337
    98
declare the_var_FVar_def [simp del]
schirmer@13337
    99
schirmer@13337
   100
lemma the_var_AVar_simp:
schirmer@13337
   101
"the_var G s ((Lit a).[Lit i]) = avar G i a s"
schirmer@13337
   102
by (simp)
schirmer@13337
   103
declare the_var_AVar_def [simp del]
schirmer@12854
   104
schirmer@12854
   105
consts
schirmer@13337
   106
  step	:: "prog \<Rightarrow> ((term \<times> state) \<times> (term \<times> state)) set"
schirmer@12854
   107
schirmer@12854
   108
syntax (symbols)
schirmer@13337
   109
  step :: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>1 _"[61,82,82] 81)
schirmer@13337
   110
  stepn:: "[prog, term \<times> state,nat,term \<times> state] \<Rightarrow> bool" 
schirmer@13337
   111
                                                  ("_\<turnstile>_ \<mapsto>_ _"[61,82,82] 81)
schirmer@13337
   112
"step*":: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>* _"[61,82,82] 81)
schirmer@13337
   113
  Ref  :: "loc \<Rightarrow> expr"
schirmer@13337
   114
  SKIP :: "expr"
schirmer@12854
   115
schirmer@12854
   116
translations
schirmer@13337
   117
  "G\<turnstile>p \<mapsto>1 p' " == "(p,p') \<in> step G"
schirmer@13337
   118
  "G\<turnstile>p \<mapsto>n p' " == "(p,p') \<in> (step G)^n"
schirmer@13337
   119
  "G\<turnstile>p \<mapsto>* p' " == "(p,p') \<in> (step G)\<^sup>*"
schirmer@12854
   120
  "Ref a" == "Lit (Addr a)"
schirmer@13337
   121
  "SKIP"  == "Lit Unit"
schirmer@12854
   122
schirmer@13337
   123
inductive "step G" intros 
schirmer@12854
   124
schirmer@12854
   125
(* evaluation of expression *)
schirmer@12854
   126
  (* cf. 15.5 *)
schirmer@13337
   127
Abrupt:	         "\<lbrakk>\<forall>v. t \<noteq> \<langle>Lit v\<rangle>;
schirmer@13337
   128
                  \<forall> t. t \<noteq> \<langle>l\<bullet> Skip\<rangle>;
schirmer@13337
   129
                  \<forall> C vn c.  t \<noteq> \<langle>Try Skip Catch(C vn) c\<rangle>;
schirmer@13337
   130
                  \<forall> x c. t \<noteq> \<langle>Skip Finally c\<rangle> \<and> xc \<noteq> Xcpt x;
schirmer@13337
   131
                  \<forall> a c. t \<noteq> \<langle>FinA a c\<rangle>\<rbrakk> 
schirmer@13337
   132
                \<Longrightarrow> 
schirmer@13337
   133
                  G\<turnstile>(t,Some xc,s) \<mapsto>1 (\<langle>Lit arbitrary\<rangle>,Some xc,s)"
schirmer@12854
   134
schirmer@13337
   135
InsInitE: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>, s')\<rbrakk>
schirmer@13337
   136
           \<Longrightarrow> 
schirmer@13337
   137
           G\<turnstile>(\<langle>InsInitE c e\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE c' e\<rangle>, s')"
schirmer@12854
   138
schirmer@13337
   139
(* SeqE: "G\<turnstile>(\<langle>Seq Skip e\<rangle>,Norm s) \<mapsto>1 (\<langle>e\<rangle>, Norm s)" *)
schirmer@13337
   140
(* Specialised rules to evaluate: 
schirmer@13337
   141
   InsInitE Skip (NewC C), InisInitE Skip (NewA T[e]) *)
schirmer@13337
   142
 
schirmer@13337
   143
  (* cf. 15.8.1 *)
schirmer@13337
   144
NewC: "G\<turnstile>(\<langle>NewC C\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (Init C) (NewC C)\<rangle>, Norm s)"
schirmer@13337
   145
NewCInited: "\<lbrakk>G\<turnstile> Norm s \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s'\<rbrakk> 
schirmer@13337
   146
             \<Longrightarrow> 
schirmer@13337
   147
             G\<turnstile>(\<langle>InsInitE Skip (NewC C)\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>, s')"
schirmer@12854
   148
schirmer@12854
   149
schirmer@12854
   150
schirmer@13337
   151
(* Alternative when rule SeqE is present 
schirmer@13337
   152
NewCInited: "\<lbrakk>inited C (globs s); 
schirmer@13337
   153
              G\<turnstile> Norm s \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s'\<rbrakk> 
schirmer@13337
   154
             \<Longrightarrow> 
schirmer@13337
   155
              G\<turnstile>(\<langle>NewC C\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>, s')"
schirmer@13337
   156
schirmer@13337
   157
NewC:
schirmer@13337
   158
     "\<lbrakk>\<not> inited C (globs s)\<rbrakk> 
schirmer@13337
   159
     \<Longrightarrow> 
schirmer@13337
   160
      G\<turnstile>(\<langle>NewC C\<rangle>,Norm s) \<mapsto>1 (\<langle>Seq (Init C) (NewC C)\<rangle>, Norm s)"
schirmer@13337
   161
schirmer@13337
   162
*)
schirmer@13337
   163
  (* cf. 15.9.1 *)
schirmer@13337
   164
NewA: 
schirmer@13337
   165
   "G\<turnstile>(\<langle>New T[e]\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (init_comp_ty T) (New T[e])\<rangle>,Norm s)"
schirmer@13337
   166
InsInitNewAIdx: 
schirmer@13337
   167
   "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>, s')\<rbrakk>
schirmer@13337
   168
    \<Longrightarrow>  
schirmer@13337
   169
    G\<turnstile>(\<langle>InsInitE Skip (New T[e])\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE Skip (New T[e'])\<rangle>,s')"
schirmer@13337
   170
InsInitNewA: 
schirmer@13337
   171
   "\<lbrakk>G\<turnstile>abupd (check_neg i) (Norm s) \<midarrow>halloc (Arr T (the_Intg i))\<succ>a\<rightarrow> s' \<rbrakk>
schirmer@13337
   172
    \<Longrightarrow>
schirmer@13337
   173
    G\<turnstile>(\<langle>InsInitE Skip (New T[Lit i])\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>,s')"
schirmer@13337
   174
 
schirmer@13337
   175
  (* cf. 15.15 *)
schirmer@13337
   176
CastE:	
schirmer@13337
   177
   "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
schirmer@13337
   178
    \<Longrightarrow>
schirmer@13337
   179
    G\<turnstile>(\<langle>Cast T e\<rangle>,None,s) \<mapsto>1 (\<langle>Cast T e'\<rangle>,s')" 
schirmer@13337
   180
Cast:	
schirmer@13337
   181
   "\<lbrakk>s' = abupd (raise_if (\<not>G,s\<turnstile>v fits T)  ClassCast) (Norm s)\<rbrakk> 
schirmer@13337
   182
    \<Longrightarrow> 
schirmer@13337
   183
    G\<turnstile>(\<langle>Cast T (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
schirmer@13337
   184
  (* can be written without abupd, since we know Norm s *)
schirmer@12854
   185
schirmer@12854
   186
schirmer@13337
   187
InstE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk> 
schirmer@13337
   188
        \<Longrightarrow> 
schirmer@13337
   189
        G\<turnstile>(\<langle>e InstOf T\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')" 
schirmer@13337
   190
Inst:  "\<lbrakk>b = (v\<noteq>Null \<and> G,s\<turnstile>v fits RefT T)\<rbrakk> 
schirmer@13337
   191
        \<Longrightarrow> 
schirmer@13337
   192
        G\<turnstile>(\<langle>(Lit v) InstOf T\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (Bool b)\<rangle>,s')"
schirmer@13337
   193
schirmer@13337
   194
  (* cf. 15.7.1 *)
schirmer@13337
   195
(*Lit				"G\<turnstile>(Lit v,None,s) \<mapsto>1 (Lit v,None,s)"*)
schirmer@13337
   196
schirmer@13337
   197
UnOpE:  "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s') \<rbrakk>
schirmer@13337
   198
         \<Longrightarrow> 
schirmer@13337
   199
         G\<turnstile>(\<langle>UnOp unop e\<rangle>,Norm s) \<mapsto>1 (\<langle>UnOp unop e'\<rangle>,s')"
schirmer@13337
   200
UnOp:   "G\<turnstile>(\<langle>UnOp unop (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (eval_unop unop v)\<rangle>,Norm s)"
schirmer@13337
   201
schirmer@13337
   202
BinOpE1:  "\<lbrakk>G\<turnstile>(\<langle>e1\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'\<rangle>,s') \<rbrakk>
schirmer@13337
   203
           \<Longrightarrow> 
schirmer@13337
   204
           G\<turnstile>(\<langle>BinOp binop e1 e2\<rangle>,Norm s) \<mapsto>1 (\<langle>BinOp binop e1' e2\<rangle>,s')"
schirmer@13337
   205
BinOpE2:  "\<lbrakk>G\<turnstile>(\<langle>e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e2'\<rangle>,s') \<rbrakk>
schirmer@13337
   206
           \<Longrightarrow> 
schirmer@13337
   207
           G\<turnstile>(\<langle>BinOp binop (Lit v1) e2\<rangle>,Norm s) 
schirmer@13337
   208
            \<mapsto>1 (\<langle>BinOp binop (Lit v1) e2'\<rangle>,s')"
schirmer@13337
   209
BinOp:    "G\<turnstile>(\<langle>BinOp binop (Lit v1) (Lit v2)\<rangle>,Norm s) 
schirmer@13337
   210
            \<mapsto>1 (\<langle>Lit (eval_binop binop v1 v2)\<rangle>,Norm s)"
schirmer@13337
   211
schirmer@13337
   212
Super: "G\<turnstile>(\<langle>Super\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (val_this s)\<rangle>,Norm s)"
schirmer@13337
   213
schirmer@13337
   214
AccVA: "\<lbrakk>G\<turnstile>(\<langle>va\<rangle>,Norm s) \<mapsto>1 (\<langle>va'\<rangle>,s') \<rbrakk>
schirmer@13337
   215
        \<Longrightarrow> 
schirmer@13337
   216
        G\<turnstile>(\<langle>Acc va\<rangle>,Norm s) \<mapsto>1 (\<langle>Acc va'\<rangle>,s')"
schirmer@13337
   217
Acc:  "\<lbrakk>groundVar va; ((v,vf),s') = the_var G (Norm s) va\<rbrakk>
schirmer@13337
   218
       \<Longrightarrow>  
schirmer@13337
   219
       G\<turnstile>(\<langle>Acc va\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
schirmer@13337
   220
schirmer@13337
   221
(*
schirmer@13337
   222
AccLVar: "G\<turnstile>(\<langle>Acc (LVar vn)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (fst (lvar vn s))\<rangle>,Norm s)"
schirmer@13337
   223
AccFVar: "\<lbrakk>((v,vf),s') = fvar statDeclC stat fn a (Norm s)\<rbrakk>
schirmer@13337
   224
          \<Longrightarrow>  
schirmer@13337
   225
          G\<turnstile>(\<langle>Acc ({accC,statDeclC,stat}(Lit a)..fn)\<rangle>,Norm s) 
schirmer@13337
   226
           \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
schirmer@13337
   227
AccAVar: "\<lbrakk>((v,vf),s') = avar G i a (Norm s)\<rbrakk>
schirmer@13337
   228
          \<Longrightarrow>  
schirmer@13337
   229
          G\<turnstile>(\<langle>Acc ((Lit a).[Lit i])\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
schirmer@13337
   230
*) 
schirmer@13337
   231
AssVA:  "\<lbrakk>G\<turnstile>(\<langle>va\<rangle>,Norm s) \<mapsto>1 (\<langle>va'\<rangle>,s')\<rbrakk> 
schirmer@13337
   232
         \<Longrightarrow> 
schirmer@13337
   233
         G\<turnstile>(\<langle>va:=e\<rangle>,Norm s) \<mapsto>1 (\<langle>va':=e\<rangle>,s')"
schirmer@13337
   234
AssE:   "\<lbrakk>groundVar va; G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
schirmer@13337
   235
         \<Longrightarrow> 
schirmer@13337
   236
         G\<turnstile>(\<langle>va:=e\<rangle>,Norm s) \<mapsto>1 (\<langle>va:=e'\<rangle>,s')"
schirmer@13337
   237
Ass:    "\<lbrakk>groundVar va; ((w,f),s') = the_var G (Norm s) va\<rbrakk> 
schirmer@13337
   238
         \<Longrightarrow> 
schirmer@13337
   239
         G\<turnstile>(\<langle>va:=(Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,assign f v s')"
schirmer@13337
   240
schirmer@13337
   241
CondC: "\<lbrakk>G\<turnstile>(\<langle>e0\<rangle>,Norm s) \<mapsto>1 (\<langle>e0'\<rangle>,s')\<rbrakk> 
schirmer@13337
   242
        \<Longrightarrow> 
schirmer@13337
   243
        G\<turnstile>(\<langle>e0? e1:e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e0'? e1:e2\<rangle>,s')"
schirmer@13337
   244
Cond:  "G\<turnstile>(\<langle>Lit b? e1:e2\<rangle>,Norm s) \<mapsto>1 (\<langle>if the_Bool b then e1 else e2\<rangle>,Norm s)"
schirmer@13337
   245
schirmer@13337
   246
schirmer@13337
   247
CallTarget: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
schirmer@13337
   248
             \<Longrightarrow>
schirmer@13337
   249
	     G\<turnstile>(\<langle>{accC,statT,mode}e\<cdot>mn({pTs}args)\<rangle>,Norm s) 
schirmer@13337
   250
              \<mapsto>1 (\<langle>{accC,statT,mode}e'\<cdot>mn({pTs}args)\<rangle>,s')"
schirmer@13337
   251
CallArgs:   "\<lbrakk>G\<turnstile>(\<langle>args\<rangle>,Norm s) \<mapsto>1 (\<langle>args'\<rangle>,s')\<rbrakk> 
schirmer@13337
   252
             \<Longrightarrow>
schirmer@13337
   253
	     G\<turnstile>(\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args)\<rangle>,Norm s) 
schirmer@13337
   254
              \<mapsto>1 (\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args')\<rangle>,s')"
schirmer@13337
   255
Call:       "\<lbrakk>groundExprs args; vs = map the_val args;
schirmer@13337
   256
              D = invocation_declclass G mode s a statT \<lparr>name=mn,parTs=pTs\<rparr>;
schirmer@13337
   257
              s'=init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs (Norm s)\<rbrakk> 
schirmer@13337
   258
             \<Longrightarrow> 
schirmer@13337
   259
             G\<turnstile>(\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args)\<rangle>,Norm s) 
schirmer@13337
   260
              \<mapsto>1 (\<langle>Callee (locals s) (Methd D \<lparr>name=mn,parTs=pTs\<rparr>)\<rangle>,s')"
schirmer@13337
   261
           
schirmer@13337
   262
Callee:     "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk>
schirmer@13337
   263
             \<Longrightarrow> 
schirmer@13337
   264
             G\<turnstile>(\<langle>Callee lcls_caller e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')"
schirmer@13337
   265
schirmer@13337
   266
CalleeRet:   "G\<turnstile>(\<langle>Callee lcls_caller (Lit v)\<rangle>,Norm s) 
schirmer@13337
   267
               \<mapsto>1 (\<langle>Lit v\<rangle>,(set_lvars lcls_caller (Norm s)))"
schirmer@13337
   268
schirmer@13337
   269
Methd: "G\<turnstile>(\<langle>Methd D sig\<rangle>,Norm s) \<mapsto>1 (\<langle>body G D sig\<rangle>,Norm s)"
schirmer@13337
   270
schirmer@13337
   271
Body: "G\<turnstile>(\<langle>Body D c\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (Init D) (Body D c)\<rangle>,Norm s)"
schirmer@13337
   272
schirmer@13337
   273
InsInitBody: 
schirmer@13337
   274
    "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk>
schirmer@13337
   275
     \<Longrightarrow> 
schirmer@13337
   276
     G\<turnstile>(\<langle>InsInitE Skip (Body D c)\<rangle>,Norm s) \<mapsto>1(\<langle>InsInitE Skip (Body D c')\<rangle>,s')"
schirmer@13337
   277
InsInitBodyRet: 
schirmer@13337
   278
     "G\<turnstile>(\<langle>InsInitE Skip (Body D Skip)\<rangle>,Norm s)
schirmer@13337
   279
       \<mapsto>1 (\<langle>Lit (the ((locals s) Result))\<rangle>,abupd (absorb Ret) (Norm s))"
schirmer@13337
   280
schirmer@13337
   281
(*   LVar: "G\<turnstile>(LVar vn,Norm s)" is already evaluated *)
schirmer@13337
   282
  
schirmer@13337
   283
FVar: "\<lbrakk>\<not> inited statDeclC (globs s)\<rbrakk>
schirmer@13337
   284
       \<Longrightarrow> 
schirmer@13337
   285
       G\<turnstile>(\<langle>{accC,statDeclC,stat}e..fn\<rangle>,Norm s) 
schirmer@13337
   286
        \<mapsto>1 (\<langle>InsInitV (Init statDeclC) ({accC,statDeclC,stat}e..fn)\<rangle>,Norm s)"
schirmer@13337
   287
InsInitFVarE:
schirmer@13337
   288
      "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk>
schirmer@13337
   289
       \<Longrightarrow>
schirmer@13337
   290
       G\<turnstile>(\<langle>InsInitV Skip ({accC,statDeclC,stat}e..fn)\<rangle>,Norm s) 
schirmer@13337
   291
        \<mapsto>1 (\<langle>InsInitV Skip ({accC,statDeclC,stat}e'..fn)\<rangle>,s')"
schirmer@13337
   292
InsInitFVar:
schirmer@13337
   293
      "G\<turnstile>(\<langle>InsInitV Skip ({accC,statDeclC,stat}Lit a..fn)\<rangle>,Norm s) 
schirmer@13337
   294
        \<mapsto>1 (\<langle>{accC,statDeclC,stat}Lit a..fn\<rangle>,Norm s)"
schirmer@13337
   295
--  {* Notice, that we do not have literal values for @{text vars}. 
schirmer@13337
   296
The rules for accessing variables (@{text Acc}) and assigning to variables 
schirmer@13337
   297
(@{text Ass}), test this with the predicate @{text groundVar}.  After 
schirmer@13337
   298
initialisation is done and the @{text FVar} is evaluated, we can't just 
schirmer@13337
   299
throw away the @{text InsInitFVar} term and return a literal value, as in the 
schirmer@13337
   300
cases of @{text New}  or @{text NewC}. Instead we just return the evaluated 
schirmer@13337
   301
@{text FVar} and test for initialisation in the rule @{text FVar}. 
schirmer@13337
   302
*}
schirmer@13337
   303
schirmer@13337
   304
schirmer@13337
   305
AVarE1: "\<lbrakk>G\<turnstile>(\<langle>e1\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'\<rangle>,s')\<rbrakk> 
schirmer@13337
   306
         \<Longrightarrow> 
schirmer@13337
   307
         G\<turnstile>(\<langle>e1.[e2]\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'.[e2]\<rangle>,s')"
schirmer@13337
   308
schirmer@13337
   309
AVarE2: "G\<turnstile>(\<langle>e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e2'\<rangle>,s') 
schirmer@13337
   310
         \<Longrightarrow> 
schirmer@13337
   311
         G\<turnstile>(\<langle>Lit a.[e2]\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit a.[e2']\<rangle>,s')"
schirmer@13337
   312
schirmer@13337
   313
(* AVar: \<langle>(Lit a).[Lit i]\<rangle> is fully evaluated *)
schirmer@13337
   314
schirmer@13337
   315
(* evaluation of expression lists *)
schirmer@13337
   316
schirmer@13337
   317
  -- {* @{text Nil}  is fully evaluated *}
schirmer@13337
   318
schirmer@13337
   319
ConsHd: "\<lbrakk>G\<turnstile>(\<langle>e::expr\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk> 
schirmer@13337
   320
         \<Longrightarrow>
schirmer@13337
   321
         G\<turnstile>(\<langle>e#es\<rangle>,Norm s) \<mapsto>1 (\<langle>e'#es\<rangle>,s')"
schirmer@13337
   322
  
schirmer@13337
   323
ConsTl: "\<lbrakk>G\<turnstile>(\<langle>es\<rangle>,Norm s) \<mapsto>1 (\<langle>es'\<rangle>,s')\<rbrakk> 
schirmer@13337
   324
         \<Longrightarrow>
schirmer@13337
   325
         G\<turnstile>(\<langle>(Lit v)#es\<rangle>,Norm s) \<mapsto>1 (\<langle>(Lit v)#es'\<rangle>,s')"
schirmer@12854
   326
schirmer@12854
   327
(* execution of statements *)
schirmer@12854
   328
schirmer@12854
   329
  (* cf. 14.5 *)
schirmer@13337
   330
Skip: "G\<turnstile>(\<langle>Skip\<rangle>,Norm s) \<mapsto>1 (\<langle>SKIP\<rangle>,Norm s)"
schirmer@12854
   331
schirmer@13337
   332
ExprE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
schirmer@13337
   333
        \<Longrightarrow> 
schirmer@13337
   334
        G\<turnstile>(\<langle>Expr e\<rangle>,Norm s) \<mapsto>1 (\<langle>Expr e'\<rangle>,s')"
schirmer@13337
   335
Expr:  "G\<turnstile>(\<langle>Expr (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,Norm s)"
schirmer@12854
   336
schirmer@12854
   337
schirmer@13337
   338
LabC: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk> 
schirmer@13337
   339
       \<Longrightarrow>  
schirmer@13337
   340
       G\<turnstile>(\<langle>l\<bullet> c\<rangle>,Norm s) \<mapsto>1 (\<langle>l\<bullet> c'\<rangle>,s')"
schirmer@13337
   341
Lab:  "G\<turnstile>(\<langle>l\<bullet> Skip\<rangle>,s) \<mapsto>1 (\<langle>Skip\<rangle>, abupd (absorb l) s)"
schirmer@13337
   342
schirmer@13337
   343
  (* cf. 14.2 *)
schirmer@13337
   344
CompC1:	"\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk> 
schirmer@13337
   345
         \<Longrightarrow> 
schirmer@13337
   346
         G\<turnstile>(\<langle>c1;; c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c1';; c2\<rangle>,s')"
schirmer@13337
   347
schirmer@13337
   348
Comp:   "G\<turnstile>(\<langle>Skip;; c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c2\<rangle>,Norm s)"
schirmer@12854
   349
schirmer@12854
   350
  (* cf. 14.8.2 *)
schirmer@13337
   351
IfE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle> ,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
schirmer@13337
   352
      \<Longrightarrow>
schirmer@13337
   353
      G\<turnstile>(\<langle>If(e) s1 Else s2\<rangle>,Norm s) \<mapsto>1 (\<langle>If(e') s1 Else s2\<rangle>,s')"
schirmer@13337
   354
If:  "G\<turnstile>(\<langle>If(Lit v) s1 Else s2\<rangle>,Norm s) 
schirmer@13337
   355
       \<mapsto>1 (\<langle>if the_Bool v then s1 else s2\<rangle>,Norm s)"
schirmer@12854
   356
schirmer@12854
   357
  (* cf. 14.10, 14.10.1 *)
schirmer@13337
   358
Loop: "G\<turnstile>(\<langle>l\<bullet> While(e) c\<rangle>,Norm s) 
schirmer@13337
   359
        \<mapsto>1 (\<langle>If(e) (Cont l\<bullet>c;; l\<bullet> While(e) c) Else Skip\<rangle>,Norm s)"
schirmer@13337
   360
schirmer@13337
   361
Do: "G\<turnstile>(\<langle>Do j\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,(Some (Jump j), s))"
schirmer@13337
   362
schirmer@13337
   363
ThrowE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
schirmer@13337
   364
         \<Longrightarrow>
schirmer@13337
   365
         G\<turnstile>(\<langle>Throw e\<rangle>,Norm s) \<mapsto>1 (\<langle>Throw e'\<rangle>,s')"
schirmer@13337
   366
Throw:  "G\<turnstile>(\<langle>Throw (Lit a)\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,abupd (throw a) (Norm s))"
schirmer@13337
   367
schirmer@13337
   368
TryC1: "\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk> 
schirmer@13337
   369
        \<Longrightarrow>
schirmer@13337
   370
        G\<turnstile>(\<langle>Try c1 Catch(C vn) c2\<rangle>, Norm s) \<mapsto>1 (\<langle>Try c1' Catch(C vn) c2\<rangle>,s')"
schirmer@13337
   371
Try:   "\<lbrakk>G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'\<rbrakk>
schirmer@13337
   372
        \<Longrightarrow>
schirmer@13337
   373
        G\<turnstile>(\<langle>Try Skip Catch(C vn) c2\<rangle>, s) 
schirmer@13337
   374
         \<mapsto>1 (if G,s'\<turnstile>catch C then (\<langle>c2\<rangle>,new_xcpt_var vn s')
schirmer@13337
   375
                              else (\<langle>Skip\<rangle>,s'))"
schirmer@13337
   376
schirmer@13337
   377
FinC1: "\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk> 
schirmer@13337
   378
        \<Longrightarrow>
schirmer@13337
   379
        G\<turnstile>(\<langle>c1 Finally c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c1' Finally c2\<rangle>,s')"
schirmer@13337
   380
schirmer@13337
   381
Fin:    "G\<turnstile>(\<langle>Skip Finally c2\<rangle>,(a,s)) \<mapsto>1 (\<langle>FinA a c2\<rangle>,Norm s)"
schirmer@13337
   382
schirmer@13337
   383
FinAC: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk>
schirmer@13337
   384
        \<Longrightarrow>
schirmer@13337
   385
        G\<turnstile>(\<langle>FinA a c\<rangle>,s) \<mapsto>1 (\<langle>FinA a c'\<rangle>,s')"
schirmer@13337
   386
FinA: "G\<turnstile>(\<langle>FinA a Skip\<rangle>,s) \<mapsto>1 (\<langle>Skip\<rangle>,abupd (abrupt_if (a\<noteq>None) a) s)"
schirmer@13337
   387
schirmer@13337
   388
schirmer@13337
   389
Init1: "\<lbrakk>inited C (globs s)\<rbrakk> 
schirmer@13337
   390
        \<Longrightarrow> 
schirmer@13337
   391
        G\<turnstile>(\<langle>Init C\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,Norm s)"
schirmer@13337
   392
Init: "\<lbrakk>the (class G C)=c; \<not> inited C (globs s)\<rbrakk>  
schirmer@13337
   393
       \<Longrightarrow> 
schirmer@13337
   394
       G\<turnstile>(\<langle>Init C\<rangle>,Norm s) 
schirmer@13337
   395
        \<mapsto>1 (\<langle>(if C = Object then Skip else (Init (super c)));;
schirmer@13337
   396
              Expr (Callee (locals s) (InsInitE (init c) SKIP))\<rangle>
schirmer@13337
   397
             ,Norm (init_class_obj G C s))"
schirmer@13337
   398
-- {* @{text InsInitE} is just used as trick to embed the statement 
schirmer@13337
   399
@{text "init c"} into an expression*} 
schirmer@13337
   400
InsInitESKIP:
schirmer@13337
   401
  "G\<turnstile>(\<langle>InsInitE Skip SKIP\<rangle>,Norm s) \<mapsto>1 (\<langle>SKIP\<rangle>,Norm s)"
schirmer@13337
   402
         
schirmer@13337
   403
(* Equivalenzen:
schirmer@13337
   404
  Bigstep zu Smallstep komplett.
schirmer@13337
   405
  Smallstep zu Bigstep, nur wenn nicht die Ausdrücke Callee, FinA ,\<dots>
schirmer@12925
   406
*)
schirmer@12854
   407
schirmer@13337
   408
lemma rtrancl_imp_rel_pow: "p \<in> R^* \<Longrightarrow> \<exists>n. p \<in> R^n"
schirmer@13337
   409
proof -
schirmer@13337
   410
  assume "p \<in> R\<^sup>*"
schirmer@13337
   411
  moreover obtain x y where p: "p = (x,y)" by (cases p)
schirmer@13337
   412
  ultimately have "(x,y) \<in> R\<^sup>*" by hypsubst
schirmer@13337
   413
  hence "\<exists>n. (x,y) \<in> R^n"
schirmer@13337
   414
  proof induct
schirmer@13337
   415
    fix a have "(a,a) \<in> R^0" by simp
schirmer@13337
   416
    thus "\<exists>n. (a,a) \<in> R ^ n" ..
schirmer@13337
   417
  next
schirmer@13337
   418
    fix a b c assume "\<exists>n. (a,b) \<in> R ^ n"
schirmer@13337
   419
    then obtain n where "(a,b) \<in> R^n" ..
schirmer@13337
   420
    moreover assume "(b,c) \<in> R"
schirmer@13337
   421
    ultimately have "(a,c) \<in> R^(Suc n)" by auto
schirmer@13337
   422
    thus "\<exists>n. (a,c) \<in> R^n" ..
schirmer@13337
   423
  qed
schirmer@13337
   424
  with p show ?thesis by hypsubst
schirmer@13337
   425
qed  
schirmer@13337
   426
schirmer@13337
   427
(*
schirmer@13337
   428
lemma imp_eval_trans:
schirmer@13337
   429
  assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" 
schirmer@13337
   430
    shows trans: "G\<turnstile>(t,s0) \<mapsto>* (\<langle>Lit v\<rangle>,s1)"
schirmer@13337
   431
*)
schirmer@13337
   432
(* Jetzt muss man bei trans natürlich wieder unterscheiden: Stmt, Expr, Var!
schirmer@13337
   433
   Sowas blödes:
schirmer@13337
   434
   Am besten den Terminus ground auf Var,Stmt,Expr hochziehen und dann
schirmer@13337
   435
   the_vals definieren\<dots>
schirmer@13337
   436
  G\<turnstile>(t,s0) \<mapsto>* (t',s1) \<and> the_vals t' = v
schirmer@13337
   437
*)
schirmer@13337
   438
schirmer@13337
   439
schirmer@13337
   440
end