src/HOL/Bali/Trans.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (20 months ago)
changeset 67022 49309fe530fd
parent 62390 842917225d56
child 67443 3abf6a722518
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
wenzelm@12857
     1
(*  Title:      HOL/Bali/Trans.thy
schirmer@13688
     2
    Author:     David von Oheimb and Norbert Schirmer
schirmer@12854
     3
schirmer@12854
     4
Operational transition (small-step) semantics of the 
schirmer@12854
     5
execution of Java expressions and statements
schirmer@12854
     6
schirmer@12854
     7
PRELIMINARY!!!!!!!!
schirmer@12854
     8
*)
schirmer@12854
     9
haftmann@16417
    10
theory Trans imports Evaln begin
schirmer@13337
    11
wenzelm@37956
    12
definition
wenzelm@37956
    13
  groundVar :: "var \<Rightarrow> bool" where
wenzelm@37956
    14
  "groundVar v \<longleftrightarrow> (case v of
wenzelm@37956
    15
                     LVar ln \<Rightarrow> True
wenzelm@37956
    16
                   | {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a
wenzelm@37956
    17
                   | e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i
wenzelm@37956
    18
                   | InsInitV c v \<Rightarrow> False)"
schirmer@13337
    19
wenzelm@47176
    20
lemma groundVar_cases:
wenzelm@47176
    21
  assumes ground: "groundVar v"
wenzelm@47176
    22
  obtains (LVar) ln where "v=LVar ln"
wenzelm@47176
    23
    | (FVar) accC statDeclC stat a fn where "v={accC,statDeclC,stat}(Lit a)..fn"
wenzelm@47176
    24
    | (AVar) a i where "v=(Lit a).[Lit i]"
wenzelm@47176
    25
  using ground LVar FVar AVar
nipkow@56073
    26
  by (cases v) (auto simp add: groundVar_def)
schirmer@13337
    27
wenzelm@37956
    28
definition
wenzelm@37956
    29
  groundExprs :: "expr list \<Rightarrow> bool"
wenzelm@37956
    30
  where "groundExprs es \<longleftrightarrow> (\<forall>e \<in> set es. \<exists>v. e = Lit v)"
schirmer@13337
    31
  
wenzelm@37956
    32
primrec the_val:: "expr \<Rightarrow> val"
wenzelm@37956
    33
  where "the_val (Lit v) = v"
schirmer@13337
    34
haftmann@37597
    35
primrec the_var:: "prog \<Rightarrow> state \<Rightarrow> var \<Rightarrow> (vvar \<times> state)" where
wenzelm@37956
    36
  "the_var G s (LVar ln) = (lvar ln (store s),s)"
haftmann@37597
    37
| the_var_FVar_def: "the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s"
haftmann@37597
    38
| the_var_AVar_def: "the_var G s(a.[i])                       =avar G (the_val i) (the_val a) s"
schirmer@13337
    39
schirmer@13337
    40
lemma the_var_FVar_simp[simp]:
schirmer@13337
    41
"the_var G s ({accC,statDeclC,stat}(Lit a)..fn) = fvar statDeclC stat fn a s"
schirmer@13337
    42
by (simp)
schirmer@13337
    43
declare the_var_FVar_def [simp del]
schirmer@13337
    44
schirmer@13337
    45
lemma the_var_AVar_simp:
schirmer@13337
    46
"the_var G s ((Lit a).[Lit i]) = avar G i a s"
schirmer@13337
    47
by (simp)
schirmer@13337
    48
declare the_var_AVar_def [simp del]
schirmer@12854
    49
wenzelm@35067
    50
abbreviation
wenzelm@35067
    51
  Ref :: "loc \<Rightarrow> expr"
wenzelm@35067
    52
  where "Ref a == Lit (Addr a)"
schirmer@12854
    53
wenzelm@35067
    54
abbreviation
wenzelm@35067
    55
  SKIP :: "expr"
wenzelm@35067
    56
  where "SKIP == Lit Unit"
schirmer@12854
    57
berghofe@23747
    58
inductive
berghofe@21765
    59
  step :: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>1 _"[61,82,82] 81)
berghofe@21765
    60
  for G :: prog
berghofe@21765
    61
where
schirmer@12854
    62
schirmer@12854
    63
(* evaluation of expression *)
schirmer@12854
    64
  (* cf. 15.5 *)
berghofe@21765
    65
  Abrupt:       "\<lbrakk>\<forall>v. t \<noteq> \<langle>Lit v\<rangle>;
schirmer@13337
    66
                  \<forall> t. t \<noteq> \<langle>l\<bullet> Skip\<rangle>;
schirmer@13337
    67
                  \<forall> C vn c.  t \<noteq> \<langle>Try Skip Catch(C vn) c\<rangle>;
schirmer@13337
    68
                  \<forall> x c. t \<noteq> \<langle>Skip Finally c\<rangle> \<and> xc \<noteq> Xcpt x;
schirmer@13337
    69
                  \<forall> a c. t \<noteq> \<langle>FinA a c\<rangle>\<rbrakk> 
schirmer@13337
    70
                \<Longrightarrow> 
haftmann@28524
    71
                  G\<turnstile>(t,Some xc,s) \<mapsto>1 (\<langle>Lit undefined\<rangle>,Some xc,s)"
schirmer@12854
    72
berghofe@21765
    73
| InsInitE: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>, s')\<rbrakk>
berghofe@21765
    74
             \<Longrightarrow> 
berghofe@21765
    75
             G\<turnstile>(\<langle>InsInitE c e\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE c' e\<rangle>, s')"
schirmer@12854
    76
schirmer@13337
    77
(* SeqE: "G\<turnstile>(\<langle>Seq Skip e\<rangle>,Norm s) \<mapsto>1 (\<langle>e\<rangle>, Norm s)" *)
schirmer@13337
    78
(* Specialised rules to evaluate: 
schirmer@13337
    79
   InsInitE Skip (NewC C), InisInitE Skip (NewA T[e]) *)
schirmer@13337
    80
 
schirmer@13337
    81
  (* cf. 15.8.1 *)
berghofe@21765
    82
| NewC: "G\<turnstile>(\<langle>NewC C\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (Init C) (NewC C)\<rangle>, Norm s)"
berghofe@21765
    83
| NewCInited: "\<lbrakk>G\<turnstile> Norm s \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s'\<rbrakk> 
berghofe@21765
    84
               \<Longrightarrow> 
berghofe@21765
    85
               G\<turnstile>(\<langle>InsInitE Skip (NewC C)\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>, s')"
schirmer@12854
    86
schirmer@12854
    87
schirmer@12854
    88
schirmer@13337
    89
(* Alternative when rule SeqE is present 
schirmer@13337
    90
NewCInited: "\<lbrakk>inited C (globs s); 
schirmer@13337
    91
              G\<turnstile> Norm s \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s'\<rbrakk> 
schirmer@13337
    92
             \<Longrightarrow> 
schirmer@13337
    93
              G\<turnstile>(\<langle>NewC C\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>, s')"
schirmer@13337
    94
schirmer@13337
    95
NewC:
schirmer@13337
    96
     "\<lbrakk>\<not> inited C (globs s)\<rbrakk> 
schirmer@13337
    97
     \<Longrightarrow> 
schirmer@13337
    98
      G\<turnstile>(\<langle>NewC C\<rangle>,Norm s) \<mapsto>1 (\<langle>Seq (Init C) (NewC C)\<rangle>, Norm s)"
schirmer@13337
    99
schirmer@13337
   100
*)
schirmer@13337
   101
  (* cf. 15.9.1 *)
berghofe@21765
   102
| NewA: 
schirmer@13337
   103
   "G\<turnstile>(\<langle>New T[e]\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (init_comp_ty T) (New T[e])\<rangle>,Norm s)"
berghofe@21765
   104
| InsInitNewAIdx: 
schirmer@13337
   105
   "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>, s')\<rbrakk>
schirmer@13337
   106
    \<Longrightarrow>  
schirmer@13337
   107
    G\<turnstile>(\<langle>InsInitE Skip (New T[e])\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE Skip (New T[e'])\<rangle>,s')"
berghofe@21765
   108
| InsInitNewA: 
schirmer@13337
   109
   "\<lbrakk>G\<turnstile>abupd (check_neg i) (Norm s) \<midarrow>halloc (Arr T (the_Intg i))\<succ>a\<rightarrow> s' \<rbrakk>
schirmer@13337
   110
    \<Longrightarrow>
schirmer@13337
   111
    G\<turnstile>(\<langle>InsInitE Skip (New T[Lit i])\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>,s')"
schirmer@13337
   112
 
schirmer@13337
   113
  (* cf. 15.15 *)
wenzelm@32960
   114
| CastE:
schirmer@13337
   115
   "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
schirmer@13337
   116
    \<Longrightarrow>
schirmer@13337
   117
    G\<turnstile>(\<langle>Cast T e\<rangle>,None,s) \<mapsto>1 (\<langle>Cast T e'\<rangle>,s')" 
wenzelm@32960
   118
| Cast:
schirmer@13337
   119
   "\<lbrakk>s' = abupd (raise_if (\<not>G,s\<turnstile>v fits T)  ClassCast) (Norm s)\<rbrakk> 
schirmer@13337
   120
    \<Longrightarrow> 
schirmer@13337
   121
    G\<turnstile>(\<langle>Cast T (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
schirmer@13337
   122
  (* can be written without abupd, since we know Norm s *)
schirmer@12854
   123
schirmer@12854
   124
berghofe@21765
   125
| InstE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk> 
schirmer@13337
   126
        \<Longrightarrow> 
schirmer@13337
   127
        G\<turnstile>(\<langle>e InstOf T\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')" 
berghofe@21765
   128
| Inst:  "\<lbrakk>b = (v\<noteq>Null \<and> G,s\<turnstile>v fits RefT T)\<rbrakk> 
berghofe@21765
   129
          \<Longrightarrow> 
berghofe@21765
   130
          G\<turnstile>(\<langle>(Lit v) InstOf T\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (Bool b)\<rangle>,s')"
schirmer@13337
   131
schirmer@13337
   132
  (* cf. 15.7.1 *)
wenzelm@32960
   133
(*Lit                           "G\<turnstile>(Lit v,None,s) \<mapsto>1 (Lit v,None,s)"*)
schirmer@13337
   134
berghofe@21765
   135
| UnOpE:  "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s') \<rbrakk>
schirmer@13337
   136
           \<Longrightarrow> 
berghofe@21765
   137
           G\<turnstile>(\<langle>UnOp unop e\<rangle>,Norm s) \<mapsto>1 (\<langle>UnOp unop e'\<rangle>,s')"
berghofe@21765
   138
| UnOp:   "G\<turnstile>(\<langle>UnOp unop (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (eval_unop unop v)\<rangle>,Norm s)"
berghofe@21765
   139
berghofe@21765
   140
| BinOpE1:  "\<lbrakk>G\<turnstile>(\<langle>e1\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'\<rangle>,s') \<rbrakk>
berghofe@21765
   141
             \<Longrightarrow> 
berghofe@21765
   142
             G\<turnstile>(\<langle>BinOp binop e1 e2\<rangle>,Norm s) \<mapsto>1 (\<langle>BinOp binop e1' e2\<rangle>,s')"
berghofe@21765
   143
| BinOpE2:  "\<lbrakk>need_second_arg binop v1; G\<turnstile>(\<langle>e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e2'\<rangle>,s') \<rbrakk>
schirmer@13384
   144
             \<Longrightarrow> 
schirmer@13384
   145
             G\<turnstile>(\<langle>BinOp binop (Lit v1) e2\<rangle>,Norm s) 
berghofe@21765
   146
              \<mapsto>1 (\<langle>BinOp binop (Lit v1) e2'\<rangle>,s')"
berghofe@21765
   147
| BinOpTerm:  "\<lbrakk>\<not> need_second_arg binop v1\<rbrakk>
berghofe@21765
   148
               \<Longrightarrow> 
berghofe@21765
   149
               G\<turnstile>(\<langle>BinOp binop (Lit v1) e2\<rangle>,Norm s) 
berghofe@21765
   150
                \<mapsto>1 (\<langle>Lit v1\<rangle>,Norm s)"
berghofe@21765
   151
| BinOp:    "G\<turnstile>(\<langle>BinOp binop (Lit v1) (Lit v2)\<rangle>,Norm s) 
berghofe@21765
   152
              \<mapsto>1 (\<langle>Lit (eval_binop binop v1 v2)\<rangle>,Norm s)"
schirmer@13384
   153
(* Maybe its more convenient to add: need_second_arg as precondition to BinOp 
schirmer@13384
   154
   to make the choice between BinOpTerm and BinOp deterministic *)
schirmer@13384
   155
   
berghofe@21765
   156
| Super: "G\<turnstile>(\<langle>Super\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (val_this s)\<rangle>,Norm s)"
schirmer@13337
   157
berghofe@21765
   158
| AccVA: "\<lbrakk>G\<turnstile>(\<langle>va\<rangle>,Norm s) \<mapsto>1 (\<langle>va'\<rangle>,s') \<rbrakk>
berghofe@21765
   159
          \<Longrightarrow> 
berghofe@21765
   160
          G\<turnstile>(\<langle>Acc va\<rangle>,Norm s) \<mapsto>1 (\<langle>Acc va'\<rangle>,s')"
berghofe@21765
   161
| Acc:  "\<lbrakk>groundVar va; ((v,vf),s') = the_var G (Norm s) va\<rbrakk>
berghofe@21765
   162
         \<Longrightarrow>  
berghofe@21765
   163
         G\<turnstile>(\<langle>Acc va\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
schirmer@13337
   164
schirmer@13337
   165
(*
schirmer@13337
   166
AccLVar: "G\<turnstile>(\<langle>Acc (LVar vn)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (fst (lvar vn s))\<rangle>,Norm s)"
schirmer@13337
   167
AccFVar: "\<lbrakk>((v,vf),s') = fvar statDeclC stat fn a (Norm s)\<rbrakk>
schirmer@13337
   168
          \<Longrightarrow>  
schirmer@13337
   169
          G\<turnstile>(\<langle>Acc ({accC,statDeclC,stat}(Lit a)..fn)\<rangle>,Norm s) 
schirmer@13337
   170
           \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
schirmer@13337
   171
AccAVar: "\<lbrakk>((v,vf),s') = avar G i a (Norm s)\<rbrakk>
schirmer@13337
   172
          \<Longrightarrow>  
schirmer@13337
   173
          G\<turnstile>(\<langle>Acc ((Lit a).[Lit i])\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
schirmer@13337
   174
*) 
berghofe@21765
   175
| AssVA:  "\<lbrakk>G\<turnstile>(\<langle>va\<rangle>,Norm s) \<mapsto>1 (\<langle>va'\<rangle>,s')\<rbrakk> 
berghofe@21765
   176
           \<Longrightarrow> 
berghofe@21765
   177
           G\<turnstile>(\<langle>va:=e\<rangle>,Norm s) \<mapsto>1 (\<langle>va':=e\<rangle>,s')"
berghofe@21765
   178
| AssE:   "\<lbrakk>groundVar va; G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
berghofe@21765
   179
           \<Longrightarrow> 
berghofe@21765
   180
           G\<turnstile>(\<langle>va:=e\<rangle>,Norm s) \<mapsto>1 (\<langle>va:=e'\<rangle>,s')"
berghofe@21765
   181
| Ass:    "\<lbrakk>groundVar va; ((w,f),s') = the_var G (Norm s) va\<rbrakk> 
berghofe@21765
   182
           \<Longrightarrow> 
berghofe@21765
   183
           G\<turnstile>(\<langle>va:=(Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,assign f v s')"
schirmer@13337
   184
berghofe@21765
   185
| CondC: "\<lbrakk>G\<turnstile>(\<langle>e0\<rangle>,Norm s) \<mapsto>1 (\<langle>e0'\<rangle>,s')\<rbrakk> 
berghofe@21765
   186
          \<Longrightarrow> 
berghofe@21765
   187
          G\<turnstile>(\<langle>e0? e1:e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e0'? e1:e2\<rangle>,s')"
berghofe@21765
   188
| 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
   189
schirmer@13337
   190
berghofe@21765
   191
| CallTarget: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
berghofe@21765
   192
               \<Longrightarrow>
berghofe@21765
   193
               G\<turnstile>(\<langle>{accC,statT,mode}e\<cdot>mn({pTs}args)\<rangle>,Norm s) 
berghofe@21765
   194
                \<mapsto>1 (\<langle>{accC,statT,mode}e'\<cdot>mn({pTs}args)\<rangle>,s')"
berghofe@21765
   195
| CallArgs:   "\<lbrakk>G\<turnstile>(\<langle>args\<rangle>,Norm s) \<mapsto>1 (\<langle>args'\<rangle>,s')\<rbrakk> 
berghofe@21765
   196
               \<Longrightarrow>
berghofe@21765
   197
               G\<turnstile>(\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args)\<rangle>,Norm s) 
berghofe@21765
   198
                \<mapsto>1 (\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args')\<rangle>,s')"
berghofe@21765
   199
| Call:       "\<lbrakk>groundExprs args; vs = map the_val args;
berghofe@21765
   200
                D = invocation_declclass G mode s a statT \<lparr>name=mn,parTs=pTs\<rparr>;
berghofe@21765
   201
                s'=init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs (Norm s)\<rbrakk> 
berghofe@21765
   202
               \<Longrightarrow> 
berghofe@21765
   203
               G\<turnstile>(\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args)\<rangle>,Norm s) 
berghofe@21765
   204
                \<mapsto>1 (\<langle>Callee (locals s) (Methd D \<lparr>name=mn,parTs=pTs\<rparr>)\<rangle>,s')"
schirmer@13337
   205
           
berghofe@21765
   206
| Callee:     "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk>
berghofe@21765
   207
               \<Longrightarrow> 
berghofe@21765
   208
               G\<turnstile>(\<langle>Callee lcls_caller e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')"
schirmer@13337
   209
berghofe@21765
   210
| CalleeRet:   "G\<turnstile>(\<langle>Callee lcls_caller (Lit v)\<rangle>,Norm s) 
berghofe@21765
   211
                 \<mapsto>1 (\<langle>Lit v\<rangle>,(set_lvars lcls_caller (Norm s)))"
schirmer@13337
   212
berghofe@21765
   213
| Methd: "G\<turnstile>(\<langle>Methd D sig\<rangle>,Norm s) \<mapsto>1 (\<langle>body G D sig\<rangle>,Norm s)"
schirmer@13337
   214
berghofe@21765
   215
| Body: "G\<turnstile>(\<langle>Body D c\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (Init D) (Body D c)\<rangle>,Norm s)"
schirmer@13337
   216
berghofe@21765
   217
| InsInitBody: 
schirmer@13337
   218
    "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk>
schirmer@13337
   219
     \<Longrightarrow> 
schirmer@13337
   220
     G\<turnstile>(\<langle>InsInitE Skip (Body D c)\<rangle>,Norm s) \<mapsto>1(\<langle>InsInitE Skip (Body D c')\<rangle>,s')"
berghofe@21765
   221
| InsInitBodyRet: 
schirmer@13337
   222
     "G\<turnstile>(\<langle>InsInitE Skip (Body D Skip)\<rangle>,Norm s)
schirmer@13337
   223
       \<mapsto>1 (\<langle>Lit (the ((locals s) Result))\<rangle>,abupd (absorb Ret) (Norm s))"
schirmer@13337
   224
schirmer@13337
   225
(*   LVar: "G\<turnstile>(LVar vn,Norm s)" is already evaluated *)
schirmer@13337
   226
  
berghofe@21765
   227
| FVar: "\<lbrakk>\<not> inited statDeclC (globs s)\<rbrakk>
berghofe@21765
   228
         \<Longrightarrow> 
berghofe@21765
   229
         G\<turnstile>(\<langle>{accC,statDeclC,stat}e..fn\<rangle>,Norm s) 
berghofe@21765
   230
          \<mapsto>1 (\<langle>InsInitV (Init statDeclC) ({accC,statDeclC,stat}e..fn)\<rangle>,Norm s)"
berghofe@21765
   231
| InsInitFVarE:
schirmer@13337
   232
      "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk>
schirmer@13337
   233
       \<Longrightarrow>
schirmer@13337
   234
       G\<turnstile>(\<langle>InsInitV Skip ({accC,statDeclC,stat}e..fn)\<rangle>,Norm s) 
schirmer@13337
   235
        \<mapsto>1 (\<langle>InsInitV Skip ({accC,statDeclC,stat}e'..fn)\<rangle>,s')"
berghofe@21765
   236
| InsInitFVar:
schirmer@13337
   237
      "G\<turnstile>(\<langle>InsInitV Skip ({accC,statDeclC,stat}Lit a..fn)\<rangle>,Norm s) 
schirmer@13337
   238
        \<mapsto>1 (\<langle>{accC,statDeclC,stat}Lit a..fn\<rangle>,Norm s)"
wenzelm@62042
   239
\<comment>  \<open>Notice, that we do not have literal values for \<open>vars\<close>. 
wenzelm@62042
   240
The rules for accessing variables (\<open>Acc\<close>) and assigning to variables 
wenzelm@62042
   241
(\<open>Ass\<close>), test this with the predicate \<open>groundVar\<close>.  After 
wenzelm@62042
   242
initialisation is done and the \<open>FVar\<close> is evaluated, we can't just 
wenzelm@62042
   243
throw away the \<open>InsInitFVar\<close> term and return a literal value, as in the 
wenzelm@62042
   244
cases of \<open>New\<close>  or \<open>NewC\<close>. Instead we just return the evaluated 
wenzelm@62042
   245
\<open>FVar\<close> and test for initialisation in the rule \<open>FVar\<close>. 
wenzelm@62042
   246
\<close>
schirmer@13337
   247
schirmer@13337
   248
berghofe@21765
   249
| AVarE1: "\<lbrakk>G\<turnstile>(\<langle>e1\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'\<rangle>,s')\<rbrakk> 
berghofe@21765
   250
           \<Longrightarrow> 
berghofe@21765
   251
           G\<turnstile>(\<langle>e1.[e2]\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'.[e2]\<rangle>,s')"
schirmer@13337
   252
berghofe@21765
   253
| AVarE2: "G\<turnstile>(\<langle>e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e2'\<rangle>,s') 
berghofe@21765
   254
           \<Longrightarrow> 
berghofe@21765
   255
           G\<turnstile>(\<langle>Lit a.[e2]\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit a.[e2']\<rangle>,s')"
schirmer@13337
   256
schirmer@13337
   257
(* AVar: \<langle>(Lit a).[Lit i]\<rangle> is fully evaluated *)
schirmer@13337
   258
schirmer@13337
   259
(* evaluation of expression lists *)
schirmer@13337
   260
wenzelm@62042
   261
  \<comment> \<open>\<open>Nil\<close>  is fully evaluated\<close>
schirmer@13337
   262
berghofe@21765
   263
| ConsHd: "\<lbrakk>G\<turnstile>(\<langle>e::expr\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk> 
berghofe@21765
   264
           \<Longrightarrow>
berghofe@21765
   265
           G\<turnstile>(\<langle>e#es\<rangle>,Norm s) \<mapsto>1 (\<langle>e'#es\<rangle>,s')"
schirmer@13337
   266
  
berghofe@21765
   267
| ConsTl: "\<lbrakk>G\<turnstile>(\<langle>es\<rangle>,Norm s) \<mapsto>1 (\<langle>es'\<rangle>,s')\<rbrakk> 
berghofe@21765
   268
           \<Longrightarrow>
berghofe@21765
   269
           G\<turnstile>(\<langle>(Lit v)#es\<rangle>,Norm s) \<mapsto>1 (\<langle>(Lit v)#es'\<rangle>,s')"
schirmer@12854
   270
schirmer@12854
   271
(* execution of statements *)
schirmer@12854
   272
schirmer@12854
   273
  (* cf. 14.5 *)
berghofe@21765
   274
| Skip: "G\<turnstile>(\<langle>Skip\<rangle>,Norm s) \<mapsto>1 (\<langle>SKIP\<rangle>,Norm s)"
schirmer@12854
   275
berghofe@21765
   276
| ExprE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
berghofe@21765
   277
          \<Longrightarrow> 
berghofe@21765
   278
          G\<turnstile>(\<langle>Expr e\<rangle>,Norm s) \<mapsto>1 (\<langle>Expr e'\<rangle>,s')"
berghofe@21765
   279
| Expr:  "G\<turnstile>(\<langle>Expr (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,Norm s)"
schirmer@12854
   280
schirmer@12854
   281
berghofe@21765
   282
| LabC: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk> 
berghofe@21765
   283
         \<Longrightarrow>  
berghofe@21765
   284
         G\<turnstile>(\<langle>l\<bullet> c\<rangle>,Norm s) \<mapsto>1 (\<langle>l\<bullet> c'\<rangle>,s')"
berghofe@21765
   285
| Lab:  "G\<turnstile>(\<langle>l\<bullet> Skip\<rangle>,s) \<mapsto>1 (\<langle>Skip\<rangle>, abupd (absorb l) s)"
schirmer@13337
   286
schirmer@13337
   287
  (* cf. 14.2 *)
berghofe@21765
   288
| CompC1: "\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk> 
berghofe@21765
   289
           \<Longrightarrow> 
berghofe@21765
   290
           G\<turnstile>(\<langle>c1;; c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c1';; c2\<rangle>,s')"
schirmer@13337
   291
berghofe@21765
   292
| Comp:   "G\<turnstile>(\<langle>Skip;; c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c2\<rangle>,Norm s)"
schirmer@12854
   293
schirmer@12854
   294
  (* cf. 14.8.2 *)
berghofe@21765
   295
| IfE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle> ,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
berghofe@21765
   296
        \<Longrightarrow>
berghofe@21765
   297
        G\<turnstile>(\<langle>If(e) s1 Else s2\<rangle>,Norm s) \<mapsto>1 (\<langle>If(e') s1 Else s2\<rangle>,s')"
berghofe@21765
   298
| If:  "G\<turnstile>(\<langle>If(Lit v) s1 Else s2\<rangle>,Norm s) 
berghofe@21765
   299
         \<mapsto>1 (\<langle>if the_Bool v then s1 else s2\<rangle>,Norm s)"
schirmer@12854
   300
schirmer@12854
   301
  (* cf. 14.10, 14.10.1 *)
berghofe@21765
   302
| Loop: "G\<turnstile>(\<langle>l\<bullet> While(e) c\<rangle>,Norm s) 
berghofe@21765
   303
          \<mapsto>1 (\<langle>If(e) (Cont l\<bullet>c;; l\<bullet> While(e) c) Else Skip\<rangle>,Norm s)"
schirmer@13337
   304
berghofe@21765
   305
| Jmp: "G\<turnstile>(\<langle>Jmp j\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,(Some (Jump j), s))"
schirmer@13337
   306
berghofe@21765
   307
| ThrowE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
berghofe@21765
   308
           \<Longrightarrow>
berghofe@21765
   309
           G\<turnstile>(\<langle>Throw e\<rangle>,Norm s) \<mapsto>1 (\<langle>Throw e'\<rangle>,s')"
berghofe@21765
   310
| Throw:  "G\<turnstile>(\<langle>Throw (Lit a)\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,abupd (throw a) (Norm s))"
schirmer@13337
   311
berghofe@21765
   312
| TryC1: "\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk> 
berghofe@21765
   313
          \<Longrightarrow>
berghofe@21765
   314
          G\<turnstile>(\<langle>Try c1 Catch(C vn) c2\<rangle>, Norm s) \<mapsto>1 (\<langle>Try c1' Catch(C vn) c2\<rangle>,s')"
berghofe@21765
   315
| Try:   "\<lbrakk>G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'\<rbrakk>
berghofe@21765
   316
          \<Longrightarrow>
berghofe@21765
   317
          G\<turnstile>(\<langle>Try Skip Catch(C vn) c2\<rangle>, s) 
berghofe@21765
   318
           \<mapsto>1 (if G,s'\<turnstile>catch C then (\<langle>c2\<rangle>,new_xcpt_var vn s')
berghofe@21765
   319
                                else (\<langle>Skip\<rangle>,s'))"
schirmer@13337
   320
berghofe@21765
   321
| FinC1: "\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk> 
berghofe@21765
   322
          \<Longrightarrow>
berghofe@21765
   323
          G\<turnstile>(\<langle>c1 Finally c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c1' Finally c2\<rangle>,s')"
schirmer@13337
   324
berghofe@21765
   325
| Fin:    "G\<turnstile>(\<langle>Skip Finally c2\<rangle>,(a,s)) \<mapsto>1 (\<langle>FinA a c2\<rangle>,Norm s)"
schirmer@13337
   326
berghofe@21765
   327
| FinAC: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk>
berghofe@21765
   328
          \<Longrightarrow>
berghofe@21765
   329
          G\<turnstile>(\<langle>FinA a c\<rangle>,s) \<mapsto>1 (\<langle>FinA a c'\<rangle>,s')"
berghofe@21765
   330
| FinA: "G\<turnstile>(\<langle>FinA a Skip\<rangle>,s) \<mapsto>1 (\<langle>Skip\<rangle>,abupd (abrupt_if (a\<noteq>None) a) s)"
schirmer@13337
   331
schirmer@13337
   332
berghofe@21765
   333
| Init1: "\<lbrakk>inited C (globs s)\<rbrakk> 
berghofe@21765
   334
          \<Longrightarrow> 
berghofe@21765
   335
          G\<turnstile>(\<langle>Init C\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,Norm s)"
berghofe@21765
   336
| Init: "\<lbrakk>the (class G C)=c; \<not> inited C (globs s)\<rbrakk>  
berghofe@21765
   337
         \<Longrightarrow> 
berghofe@21765
   338
         G\<turnstile>(\<langle>Init C\<rangle>,Norm s) 
berghofe@21765
   339
          \<mapsto>1 (\<langle>(if C = Object then Skip else (Init (super c)));;
berghofe@21765
   340
                Expr (Callee (locals s) (InsInitE (init c) SKIP))\<rangle>
berghofe@21765
   341
               ,Norm (init_class_obj G C s))"
wenzelm@62042
   342
\<comment> \<open>\<open>InsInitE\<close> is just used as trick to embed the statement 
wenzelm@62042
   343
\<open>init c\<close> into an expression\<close> 
berghofe@21765
   344
| InsInitESKIP:
berghofe@21765
   345
    "G\<turnstile>(\<langle>InsInitE Skip SKIP\<rangle>,Norm s) \<mapsto>1 (\<langle>SKIP\<rangle>,Norm s)"
berghofe@21765
   346
berghofe@21765
   347
abbreviation
berghofe@21765
   348
  stepn:: "[prog, term \<times> state,nat,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>_ _"[61,82,82] 81)
haftmann@30952
   349
  where "G\<turnstile>p \<mapsto>n p' \<equiv> (p,p') \<in> {(x, y). step G x y}^^n"
berghofe@21765
   350
berghofe@21765
   351
abbreviation
berghofe@21765
   352
  steptr:: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>* _"[61,82,82] 81)
berghofe@21765
   353
  where "G\<turnstile>p \<mapsto>* p' \<equiv> (p,p') \<in> {(x, y). step G x y}\<^sup>*"
schirmer@13337
   354
         
schirmer@13337
   355
(* Equivalenzen:
schirmer@13337
   356
  Bigstep zu Smallstep komplett.
wenzelm@40945
   357
  Smallstep zu Bigstep, nur wenn nicht die Ausdrücke Callee, FinA ,\<dots>
schirmer@12925
   358
*)
schirmer@12854
   359
schirmer@13337
   360
(*
schirmer@13337
   361
lemma imp_eval_trans:
schirmer@13337
   362
  assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" 
schirmer@13337
   363
    shows trans: "G\<turnstile>(t,s0) \<mapsto>* (\<langle>Lit v\<rangle>,s1)"
schirmer@13337
   364
*)
wenzelm@40945
   365
(* Jetzt muss man bei trans natürlich wieder unterscheiden: Stmt, Expr, Var!
wenzelm@40945
   366
   Sowas blödes:
schirmer@13337
   367
   Am besten den Terminus ground auf Var,Stmt,Expr hochziehen und dann
schirmer@13337
   368
   the_vals definieren\<dots>
schirmer@13337
   369
  G\<turnstile>(t,s0) \<mapsto>* (t',s1) \<and> the_vals t' = v
schirmer@13337
   370
*)
schirmer@13337
   371
schirmer@13337
   372
nipkow@62390
   373
end