src/HOL/Bali/Trans.thy
author haftmann
Mon, 28 Jun 2010 15:32:13 +0200
changeset 37597 a02ea93e88c6
parent 35416 d8d7d1b785af
child 37956 ee939247b2fb
permissions -rw-r--r--
modernized specifications
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
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35069
diff changeset
    12
definition groundVar :: "var \<Rightarrow> bool" where
37597
a02ea93e88c6 modernized specifications
haftmann
parents: 35416
diff changeset
    13
"groundVar v \<longleftrightarrow> (case v of
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    14
                   LVar ln \<Rightarrow> True
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    15
                 | {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    16
                 | e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    17
                 | InsInitV c v \<Rightarrow> False)"
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    18
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    19
lemma groundVar_cases [consumes 1, case_names LVar FVar AVar]:
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    20
  assumes ground: "groundVar v" and
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    21
          LVar: "\<And> ln. \<lbrakk>v=LVar ln\<rbrakk> \<Longrightarrow> P" and
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    22
          FVar: "\<And> accC statDeclC stat a fn. 
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    23
                    \<lbrakk>v={accC,statDeclC,stat}(Lit a)..fn\<rbrakk> \<Longrightarrow> P" and
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    24
          AVar: "\<And> a i. \<lbrakk>v=(Lit a).[Lit i]\<rbrakk> \<Longrightarrow> P"
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    25
  shows "P"
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    26
proof -
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    27
  from ground LVar FVar AVar
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    28
  show ?thesis
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    29
    apply (cases v)
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    30
    apply (simp add: groundVar_def)
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    31
    apply (simp add: groundVar_def,blast)
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    32
    apply (simp add: groundVar_def,blast)
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    33
    apply (simp add: groundVar_def)
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    34
    done
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    35
qed
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    36
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 35069
diff changeset
    37
definition groundExprs :: "expr list \<Rightarrow> bool" where
37597
a02ea93e88c6 modernized specifications
haftmann
parents: 35416
diff changeset
    38
  "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
    39
  
37597
a02ea93e88c6 modernized specifications
haftmann
parents: 35416
diff changeset
    40
primrec the_val:: "expr \<Rightarrow> val" where
a02ea93e88c6 modernized specifications
haftmann
parents: 35416
diff changeset
    41
  "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
    42
37597
a02ea93e88c6 modernized specifications
haftmann
parents: 35416
diff changeset
    43
primrec the_var:: "prog \<Rightarrow> state \<Rightarrow> var \<Rightarrow> (vvar \<times> state)" where
a02ea93e88c6 modernized specifications
haftmann
parents: 35416
diff changeset
    44
  "the_var G s (LVar ln)                    =(lvar ln (store s),s)"
a02ea93e88c6 modernized specifications
haftmann
parents: 35416
diff changeset
    45
| 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
    46
| 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
    47
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    48
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
    49
"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
    50
by (simp)
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    51
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
    52
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    53
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
    54
"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
    55
by (simp)
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    56
declare the_var_AVar_def [simp del]
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    57
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
    58
abbreviation
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
    59
  Ref :: "loc \<Rightarrow> expr"
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
    60
  where "Ref a == Lit (Addr a)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    61
35067
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
    62
abbreviation
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
    63
  SKIP :: "expr"
af4c18c30593 modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents: 32960
diff changeset
    64
  where "SKIP == Lit Unit"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    65
23747
b07cff284683 Renamed inductive2 to inductive.
berghofe
parents: 21765
diff changeset
    66
inductive
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    67
  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
    68
  for G :: prog
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    69
where
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    70
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    71
(* evaluation of expression *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    72
  (* cf. 15.5 *)
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    73
  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
    74
                  \<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
    75
                  \<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
    76
                  \<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
    77
                  \<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
    78
                \<Longrightarrow> 
28524
644b62cf678f arbitrary is undefined
haftmann
parents: 23747
diff changeset
    79
                  G\<turnstile>(t,Some xc,s) \<mapsto>1 (\<langle>Lit undefined\<rangle>,Some xc,s)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    80
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    81
| 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
    82
             \<Longrightarrow> 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    83
             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
    84
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    85
(* 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
    86
(* Specialised rules to evaluate: 
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    87
   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
    88
 
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    89
  (* cf. 15.8.1 *)
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    90
| 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
    91
| 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
    92
               \<Longrightarrow> 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
    93
               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
    94
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    95
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    96
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
    97
(* 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
    98
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
    99
              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
   100
             \<Longrightarrow> 
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   101
              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
   102
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   103
NewC:
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   104
     "\<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
   105
     \<Longrightarrow> 
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   106
      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
   107
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   108
*)
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   109
  (* cf. 15.9.1 *)
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   110
| NewA: 
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   111
   "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
   112
| InsInitNewAIdx: 
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   113
   "\<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
   114
    \<Longrightarrow>  
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   115
    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
   116
| InsInitNewA: 
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   117
   "\<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
   118
    \<Longrightarrow>
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   119
    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
   120
 
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   121
  (* cf. 15.15 *)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30952
diff changeset
   122
| CastE:
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   123
   "\<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
   124
    \<Longrightarrow>
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   125
    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
   126
| Cast:
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   127
   "\<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
   128
    \<Longrightarrow> 
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   129
    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
   130
  (* can be written without abupd, since we know Norm s *)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   131
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   132
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   133
| 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
   134
        \<Longrightarrow> 
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   135
        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
   136
| 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
   137
          \<Longrightarrow> 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   138
          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
   139
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   140
  (* cf. 15.7.1 *)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30952
diff changeset
   141
(*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
   142
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   143
| 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
   144
           \<Longrightarrow> 
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   145
           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
   146
| 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
   147
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   148
| 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
   149
             \<Longrightarrow> 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   150
             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
   151
| 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
   152
             \<Longrightarrow> 
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13354
diff changeset
   153
             G\<turnstile>(\<langle>BinOp binop (Lit v1) e2\<rangle>,Norm s) 
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   154
              \<mapsto>1 (\<langle>BinOp binop (Lit v1) e2'\<rangle>,s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   155
| BinOpTerm:  "\<lbrakk>\<not> need_second_arg binop v1\<rbrakk>
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   156
               \<Longrightarrow> 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   157
               G\<turnstile>(\<langle>BinOp binop (Lit v1) e2\<rangle>,Norm s) 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   158
                \<mapsto>1 (\<langle>Lit v1\<rangle>,Norm s)"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   159
| 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
   160
              \<mapsto>1 (\<langle>Lit (eval_binop binop v1 v2)\<rangle>,Norm s)"
13384
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13354
diff changeset
   161
(* Maybe its more convenient to add: need_second_arg as precondition to BinOp 
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13354
diff changeset
   162
   to make the choice between BinOpTerm and BinOp deterministic *)
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13354
diff changeset
   163
   
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   164
| 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
   165
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   166
| 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
   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>Acc va'\<rangle>,s')"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   169
| 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
   170
         \<Longrightarrow>  
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   171
         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
   172
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   173
(*
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   174
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
   175
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
   176
          \<Longrightarrow>  
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   177
          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
   178
           \<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
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
   180
          \<Longrightarrow>  
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   181
          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
   182
*) 
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   183
| 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
   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
| 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
   187
           \<Longrightarrow> 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   188
           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
   189
| 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
   190
           \<Longrightarrow> 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   191
           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
   192
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   193
| 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
   194
          \<Longrightarrow> 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   195
          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
   196
| 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
   197
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   198
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   199
| 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
   200
               \<Longrightarrow>
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   201
               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
   202
                \<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
   203
| 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
   204
               \<Longrightarrow>
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   205
               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
   206
                \<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
   207
| Call:       "\<lbrakk>groundExprs args; vs = map the_val args;
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   208
                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
   209
                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
   210
               \<Longrightarrow> 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   211
               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
   212
                \<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
   213
           
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   214
| 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
   215
               \<Longrightarrow> 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   216
               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
   217
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   218
| CalleeRet:   "G\<turnstile>(\<langle>Callee lcls_caller (Lit v)\<rangle>,Norm s) 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   219
                 \<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
   220
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   221
| 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
   222
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   223
| 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
   224
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   225
| InsInitBody: 
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   226
    "\<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
   227
     \<Longrightarrow> 
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   228
     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
   229
| InsInitBodyRet: 
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   230
     "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
   231
       \<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
   232
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   233
(*   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
   234
  
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   235
| FVar: "\<lbrakk>\<not> inited statDeclC (globs s)\<rbrakk>
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   236
         \<Longrightarrow> 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   237
         G\<turnstile>(\<langle>{accC,statDeclC,stat}e..fn\<rangle>,Norm s) 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   238
          \<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
   239
| InsInitFVarE:
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   240
      "\<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
   241
       \<Longrightarrow>
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}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
   243
        \<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
   244
| InsInitFVar:
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   245
      "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
   246
        \<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
   247
--  {* 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
   248
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
   249
(@{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
   250
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
   251
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
   252
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
   253
@{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
   254
*}
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   255
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   256
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   257
| 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
   258
           \<Longrightarrow> 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   259
           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
   260
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   261
| 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
   262
           \<Longrightarrow> 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   263
           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
   264
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   265
(* 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
   266
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   267
(* evaluation of expression lists *)
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   268
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   269
  -- {* @{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
   270
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   271
| 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
   272
           \<Longrightarrow>
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   273
           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
   274
  
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   275
| 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
   276
           \<Longrightarrow>
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   277
           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
   278
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   279
(* execution of statements *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   280
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   281
  (* cf. 14.5 *)
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   282
| Skip: "G\<turnstile>(\<langle>Skip\<rangle>,Norm s) \<mapsto>1 (\<langle>SKIP\<rangle>,Norm s)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   283
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   284
| 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
   285
          \<Longrightarrow> 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   286
          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
   287
| 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
   288
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   289
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   290
| 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
   291
         \<Longrightarrow>  
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   292
         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
   293
| 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
   294
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   295
  (* cf. 14.2 *)
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   296
| 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
   297
           \<Longrightarrow> 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   298
           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
   299
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   300
| 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
   301
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   302
  (* cf. 14.8.2 *)
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   303
| 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
   304
        \<Longrightarrow>
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   305
        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
   306
| 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
   307
         \<mapsto>1 (\<langle>if the_Bool v then s1 else s2\<rangle>,Norm s)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   308
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   309
  (* cf. 14.10, 14.10.1 *)
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   310
| Loop: "G\<turnstile>(\<langle>l\<bullet> While(e) c\<rangle>,Norm s) 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   311
          \<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
   312
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   313
| 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
   314
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   315
| 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
   316
           \<Longrightarrow>
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   317
           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
   318
| 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
   319
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   320
| 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
   321
          \<Longrightarrow>
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   322
          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
   323
| Try:   "\<lbrakk>G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'\<rbrakk>
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   324
          \<Longrightarrow>
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   325
          G\<turnstile>(\<langle>Try Skip Catch(C vn) c2\<rangle>, s) 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   326
           \<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
   327
                                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
   328
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   329
| 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
   330
          \<Longrightarrow>
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   331
          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
   332
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   333
| 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
   334
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   335
| 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
   336
          \<Longrightarrow>
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   337
          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
   338
| 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
   339
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   340
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   341
| Init1: "\<lbrakk>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) \<mapsto>1 (\<langle>Skip\<rangle>,Norm s)"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   344
| 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
   345
         \<Longrightarrow> 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   346
         G\<turnstile>(\<langle>Init C\<rangle>,Norm s) 
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   347
          \<mapsto>1 (\<langle>(if C = Object then Skip else (Init (super c)));;
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   348
                Expr (Callee (locals s) (InsInitE (init c) SKIP))\<rangle>
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   349
               ,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
   350
-- {* @{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
   351
@{text "init c"} into an expression*} 
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   352
| InsInitESKIP:
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   353
    "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
   354
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   355
abbreviation
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   356
  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
   357
  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
   358
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   359
abbreviation
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   360
  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
   361
  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
   362
         
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   363
(* Equivalenzen:
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   364
  Bigstep zu Smallstep komplett.
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   365
  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
   366
*)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   367
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   368
(*
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   369
lemma imp_eval_trans:
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   370
  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
   371
    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
   372
*)
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   373
(* Jetzt muss man bei trans natürlich wieder unterscheiden: Stmt, Expr, Var!
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   374
   Sowas blödes:
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   375
   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
   376
   the_vals definieren\<dots>
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   377
  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
   378
*)
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   379
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   380
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   381
end