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