src/HOL/Bali/Evaln.thy
author schirmer
Mon, 28 Jan 2002 17:00:19 +0100
changeset 12854 00d4a435777f
child 12857 a4386cc9b1c3
permissions -rw-r--r--
Isabelle/Bali sources;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     1
(*  Title:      isabelle/Bali/Evaln.thy
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     2
    ID:         $Id$
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     3
    Author:     David von Oheimb
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     4
    Copyright   1999 Technische Universitaet Muenchen
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     5
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     6
header {* Operational evaluation (big-step) semantics of Java expressions and 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     7
          statements
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     8
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     9
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    10
theory Evaln = Eval:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    11
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    12
text {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    13
Variant of eval relation with counter for bounded recursive depth
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    14
Evaln could completely replace Eval.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    15
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    16
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    17
consts
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    18
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    19
  evaln	:: "prog \<Rightarrow> (state \<times> term \<times> nat \<times> vals \<times> state) set"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    20
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    21
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    22
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    23
  evaln	:: "[prog, state, term,        nat, vals * state] => bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    24
				("_|-_ -_>-_-> _"   [61,61,80,   61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    25
  evarn	:: "[prog, state, var  , vvar        , nat, state] => bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    26
				("_|-_ -_=>_-_-> _" [61,61,90,61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    27
  eval_n:: "[prog, state, expr , val         , nat, state] => bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    28
				("_|-_ -_->_-_-> _" [61,61,80,61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    29
  evalsn:: "[prog, state, expr list, val list, nat, state] => bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    30
				("_|-_ -_#>_-_-> _" [61,61,61,61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    31
  execn	:: "[prog, state, stmt ,               nat, state] => bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    32
				("_|-_ -_-_-> _"    [61,61,65,   61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    33
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    34
syntax (xsymbols)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    35
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    36
  evaln	:: "[prog, state, term,         nat, vals \<times> state] \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    37
				("_\<turnstile>_ \<midarrow>_\<succ>\<midarrow>_\<rightarrow> _"   [61,61,80,   61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    38
  evarn	:: "[prog, state, var  , vvar         , nat, state] \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    39
				("_\<turnstile>_ \<midarrow>_=\<succ>_\<midarrow>_\<rightarrow> _" [61,61,90,61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    40
  eval_n:: "[prog, state, expr , val ,          nat, state] \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    41
				("_\<turnstile>_ \<midarrow>_-\<succ>_\<midarrow>_\<rightarrow> _" [61,61,80,61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    42
  evalsn:: "[prog, state, expr list, val  list, nat, state] \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    43
				("_\<turnstile>_ \<midarrow>_\<doteq>\<succ>_\<midarrow>_\<rightarrow> _" [61,61,61,61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    44
  execn	:: "[prog, state, stmt ,                nat, state] \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    45
				("_\<turnstile>_ \<midarrow>_\<midarrow>_\<rightarrow> _"     [61,61,65,   61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    46
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    47
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    48
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    49
  "G\<turnstile>s \<midarrow>t    \<succ>\<midarrow>n\<rightarrow>  w___s' " == "(s,t,n,w___s') \<in> evaln G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    50
  "G\<turnstile>s \<midarrow>t    \<succ>\<midarrow>n\<rightarrow> (w,  s')" <= "(s,t,n,w,  s') \<in> evaln G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    51
  "G\<turnstile>s \<midarrow>t    \<succ>\<midarrow>n\<rightarrow> (w,x,s')" <= "(s,t,n,w,x,s') \<in> evaln G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    52
  "G\<turnstile>s \<midarrow>c     \<midarrow>n\<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In1r  c\<succ>\<midarrow>n\<rightarrow> (\<diamondsuit>    ,x,s')"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    53
  "G\<turnstile>s \<midarrow>c     \<midarrow>n\<rightarrow>    s' " == "G\<turnstile>s \<midarrow>In1r  c\<succ>\<midarrow>n\<rightarrow> (\<diamondsuit>    ,  s')"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    54
  "G\<turnstile>s \<midarrow>e-\<succ>v  \<midarrow>n\<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In1l e\<succ>\<midarrow>n\<rightarrow> (In1 v ,x,s')"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    55
  "G\<turnstile>s \<midarrow>e-\<succ>v  \<midarrow>n\<rightarrow>    s' " == "G\<turnstile>s \<midarrow>In1l e\<succ>\<midarrow>n\<rightarrow> (In1 v ,  s')"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    56
  "G\<turnstile>s \<midarrow>e=\<succ>vf \<midarrow>n\<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In2  e\<succ>\<midarrow>n\<rightarrow> (In2 vf,x,s')"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    57
  "G\<turnstile>s \<midarrow>e=\<succ>vf \<midarrow>n\<rightarrow>    s' " == "G\<turnstile>s \<midarrow>In2  e\<succ>\<midarrow>n\<rightarrow> (In2 vf,  s')"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    58
  "G\<turnstile>s \<midarrow>e\<doteq>\<succ>v  \<midarrow>n\<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In3  e\<succ>\<midarrow>n\<rightarrow> (In3 v ,x,s')"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    59
  "G\<turnstile>s \<midarrow>e\<doteq>\<succ>v  \<midarrow>n\<rightarrow>    s' " == "G\<turnstile>s \<midarrow>In3  e\<succ>\<midarrow>n\<rightarrow> (In3 v ,  s')"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    60
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    61
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    62
inductive "evaln G" intros
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    63
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    64
(* propagation of abrupt completion *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    65
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    66
  Abrupt:   "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t,(Some xc,s))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    67
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    68
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    69
(* evaluation of variables *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    70
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    71
  LVar:	"G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    72
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    73
  FVar:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s2;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    74
	  (v,s2') = fvar C stat fn a' s2\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    75
	  G\<turnstile>Norm s0 \<midarrow>{C,stat}e..fn=\<succ>v\<midarrow>n\<rightarrow> s2'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    76
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    77
  AVar:	"\<lbrakk>G\<turnstile> Norm s0 \<midarrow>e1-\<succ>a\<midarrow>n\<rightarrow> s1 ; G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n\<rightarrow> s2; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    78
	  (v,s2') = avar G i a s2\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    79
	              G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<midarrow>n\<rightarrow> s2'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    80
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    81
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    82
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    83
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    84
(* evaluation of expressions *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    85
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    86
  NewC:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    87
	  G\<turnstile>     s1 \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s2\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    88
	                          G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<midarrow>n\<rightarrow> s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    89
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    90
  NewA:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>i'\<midarrow>n\<rightarrow> s2; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    91
	  G\<turnstile>abupd (check_neg i') s2 \<midarrow>halloc (Arr T (the_Intg i'))\<succ>a\<rightarrow> s3\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    92
	                        G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<midarrow>n\<rightarrow> s3"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    93
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    94
  Cast:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    95
	  s2 = abupd (raise_if (\<not>G,snd s1\<turnstile>v fits T) ClassCast) s1\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    96
			        G\<turnstile>Norm s0 \<midarrow>Cast T e-\<succ>v\<midarrow>n\<rightarrow> s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    97
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    98
  Inst:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    99
	  b = (v\<noteq>Null \<and> G,store s1\<turnstile>v fits RefT T)\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   100
			      G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<midarrow>n\<rightarrow> s1"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   101
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   102
  Lit:			   "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   103
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   104
  Super:		   "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   105
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   106
  Acc:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   107
	                          G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<midarrow>n\<rightarrow> s1"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   108
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   109
  Ass:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w,f)\<midarrow>n\<rightarrow> s1;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   110
          G\<turnstile>     s1 \<midarrow>e-\<succ>v     \<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   111
				   G\<turnstile>Norm s0 \<midarrow>va:=e-\<succ>v\<midarrow>n\<rightarrow> assign f v s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   112
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   113
  Cond:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n\<rightarrow> s1;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   114
          G\<turnstile>     s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   115
			    G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<midarrow>n\<rightarrow> s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   116
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   117
  Call:	
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   118
  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s2;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   119
    D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   120
    G\<turnstile>init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs s2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   121
            \<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ>v\<midarrow>n\<rightarrow> s3\<rbrakk>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   122
   \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>{statT,mode}e\<cdot>mn({pTs}args)-\<succ>v\<midarrow>n\<rightarrow> (restore_lvars s2 s3)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   123
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   124
  Methd:"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   125
				G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   126
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   127
  Body:	"\<lbrakk>G\<turnstile>Norm s0\<midarrow>Init D\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2\<rbrakk>\<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   128
 G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)\<midarrow>n\<rightarrow>abupd (absorb Ret) s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   129
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   130
(* evaluation of expression lists *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   131
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   132
  Nil:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   133
				"G\<turnstile>Norm s0 \<midarrow>[]\<doteq>\<succ>[]\<midarrow>n\<rightarrow> Norm s0"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   134
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   135
  Cons:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e -\<succ> v \<midarrow>n\<rightarrow> s1;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   136
          G\<turnstile>     s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   137
			     G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<midarrow>n\<rightarrow> s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   138
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   139
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   140
(* execution of statements *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   141
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   142
  Skip:	 			    "G\<turnstile>Norm s \<midarrow>Skip\<midarrow>n\<rightarrow> Norm s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   143
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   144
  Expr:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   145
				  G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   146
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   147
  Lab:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   148
                             G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb (Break l)) s1"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   149
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   150
  Comp:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<midarrow>n\<rightarrow> s1;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   151
	  G\<turnstile>     s1 \<midarrow>c2 \<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   152
				 G\<turnstile>Norm s0 \<midarrow>c1;; c2\<midarrow>n\<rightarrow> s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   153
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   154
  If:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   155
	  G\<turnstile>     s1\<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   156
		       G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2 \<midarrow>n\<rightarrow> s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   157
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   158
  Loop:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   159
	  if normal s1 \<and> the_Bool b 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   160
             then (G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2 \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   161
                   G\<turnstile>(abupd (absorb (Cont l)) s2) \<midarrow>l\<bullet> While(e) c\<midarrow>n\<rightarrow> s3)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   162
	     else s3 = s1\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   163
			      G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>n\<rightarrow> s3"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   164
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   165
  Do: "G\<turnstile>Norm s \<midarrow>Do j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   166
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   167
  Throw:"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   168
				 G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> abupd (throw a') s1"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   169
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   170
  Try:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   171
	  if G,s2\<turnstile>catch tn then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n\<rightarrow> s3 else s3 = s2\<rbrakk>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   172
          \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   173
		  G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(tn vn) c2\<midarrow>n\<rightarrow> s3"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   174
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   175
  Fin:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n\<rightarrow> (x1,s1);
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   176
	  G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   177
              G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>n\<rightarrow> abupd (abrupt_if (x1\<noteq>None) x1) s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   178
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   179
  Init:	"\<lbrakk>the (class G C) = c;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   180
	  if inited C (globs s0) then s3 = Norm s0
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   181
	  else (G\<turnstile>Norm (init_class_obj G C s0)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   182
	          \<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n\<rightarrow> s1 \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   183
	        G\<turnstile>set_lvars empty s1 \<midarrow>init c\<midarrow>n\<rightarrow> s2 \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   184
                s3 = restore_lvars s1 s2)\<rbrakk>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   185
          \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   186
		 G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   187
monos
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   188
  if_def2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   189
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   190
lemma evaln_eval: "\<And>ws. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> ws \<Longrightarrow> G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   191
apply (simp (no_asm_simp) only: split_tupled_all)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   192
apply (erule evaln.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   193
apply (rule eval.intros, (assumption+)?,(force split del: split_if)?)+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   194
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   195
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   196
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   197
lemma Suc_le_D_lemma: "\<lbrakk>Suc n <= m'; (\<And>m. n <= m \<Longrightarrow> P (Suc m)) \<rbrakk> \<Longrightarrow> P m'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   198
apply (frule Suc_le_D)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   199
apply fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   200
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   201
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   202
lemma evaln_nonstrict [rule_format (no_asm), elim]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   203
  "\<And>ws. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> ws \<Longrightarrow> \<forall>m. n\<le>m \<longrightarrow> G\<turnstile>s \<midarrow>t\<succ>\<midarrow>m\<rightarrow> ws"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   204
apply (simp (no_asm_simp) only: split_tupled_all)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   205
apply (erule evaln.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   206
apply (tactic {* ALLGOALS (EVERY'[strip_tac, TRY o etac (thm "Suc_le_D_lemma"),
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   207
  REPEAT o smp_tac 1, 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   208
  resolve_tac (thms "evaln.intros") THEN_ALL_NEW TRY o atac]) *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   209
(* 3 subgoals *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   210
apply (auto split del: split_if)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   211
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   212
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   213
lemmas evaln_nonstrict_Suc = evaln_nonstrict [OF _ le_refl [THEN le_SucI]]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   214
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   215
lemma evaln_max2: "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> ws1; G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> ws2\<rbrakk> \<Longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   216
             G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max n1 n2\<rightarrow> ws1 \<and> G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max n1 n2\<rightarrow> ws2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   217
apply (fast intro: le_maxI1 le_maxI2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   218
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   219
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   220
lemma evaln_max3: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   221
"\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> ws1; G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> ws2; G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>n3\<rightarrow> ws3\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   222
 G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws1 \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   223
 G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws2 \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   224
 G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws3"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   225
apply (drule (1) evaln_max2, erule thin_rl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   226
apply (fast intro!: le_maxI1 le_maxI2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   227
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   228
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   229
lemma eval_evaln: "\<And>ws. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws \<Longrightarrow> (\<exists>n. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> ws)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   230
apply (simp (no_asm_simp) only: split_tupled_all)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   231
apply (erule eval.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   232
apply (tactic {* ALLGOALS 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   233
         (asm_full_simp_tac (HOL_basic_ss addsplits [split_if_asm])) *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   234
apply (tactic {* ALLGOALS (EVERY'[
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   235
   REPEAT o eresolve_tac [exE, conjE], rtac exI,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   236
                     TRY o datac (thm "evaln_max3") 2, REPEAT o etac conjE,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   237
  resolve_tac (thms "evaln.intros") THEN_ALL_NEW 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   238
  force_tac (HOL_cs, HOL_ss)]) *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   239
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   240
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   241
declare split_if     [split del] split_if_asm     [split del]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   242
        option.split [split del] option.split_asm [split del]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   243
inductive_cases evaln_cases: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   244
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   245
inductive_cases evaln_elim_cases:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   246
	"G\<turnstile>(Some xc, s) \<midarrow>t                        \<succ>\<midarrow>n\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   247
	"G\<turnstile>Norm s \<midarrow>In1r Skip                      \<succ>\<midarrow>n\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   248
        "G\<turnstile>Norm s \<midarrow>In1r (Do j)                    \<succ>\<midarrow>n\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   249
        "G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> c)                    \<succ>\<midarrow>n\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   250
	"G\<turnstile>Norm s \<midarrow>In3  ([])                      \<succ>\<midarrow>n\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   251
	"G\<turnstile>Norm s \<midarrow>In3  (e#es)                    \<succ>\<midarrow>n\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   252
	"G\<turnstile>Norm s \<midarrow>In1l (Lit w)                   \<succ>\<midarrow>n\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   253
	"G\<turnstile>Norm s \<midarrow>In2  (LVar vn)                 \<succ>\<midarrow>n\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   254
	"G\<turnstile>Norm s \<midarrow>In1l (Cast T e)                \<succ>\<midarrow>n\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   255
	"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T)              \<succ>\<midarrow>n\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   256
	"G\<turnstile>Norm s \<midarrow>In1l (Super)                   \<succ>\<midarrow>n\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   257
	"G\<turnstile>Norm s \<midarrow>In1l (Acc va)                  \<succ>\<midarrow>n\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   258
	"G\<turnstile>Norm s \<midarrow>In1r (Expr e)                  \<succ>\<midarrow>n\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   259
	"G\<turnstile>Norm s \<midarrow>In1r (c1;; c2)                 \<succ>\<midarrow>n\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   260
	"G\<turnstile>Norm s \<midarrow>In1l (Methd C sig)             \<succ>\<midarrow>n\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   261
	"G\<turnstile>Norm s \<midarrow>In1l (Body D c)                \<succ>\<midarrow>n\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   262
	"G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2)            \<succ>\<midarrow>n\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   263
	"G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2)        \<succ>\<midarrow>n\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   264
	"G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> While(e) c)           \<succ>\<midarrow>n\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   265
	"G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2)           \<succ>\<midarrow>n\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   266
	"G\<turnstile>Norm s \<midarrow>In1r (Throw e)                 \<succ>\<midarrow>n\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   267
	"G\<turnstile>Norm s \<midarrow>In1l (NewC C)                  \<succ>\<midarrow>n\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   268
	"G\<turnstile>Norm s \<midarrow>In1l (New T[e])                \<succ>\<midarrow>n\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   269
	"G\<turnstile>Norm s \<midarrow>In1l (Ass va e)                \<succ>\<midarrow>n\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   270
	"G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2)  \<succ>\<midarrow>n\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   271
	"G\<turnstile>Norm s \<midarrow>In2  ({C,stat}e..fn)           \<succ>\<midarrow>n\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   272
	"G\<turnstile>Norm s \<midarrow>In2  (e1.[e2])                 \<succ>\<midarrow>n\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   273
	"G\<turnstile>Norm s \<midarrow>In1l ({statT,mode}e\<cdot>mn({pT}p)) \<succ>\<midarrow>n\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   274
	"G\<turnstile>Norm s \<midarrow>In1r (Init C)                  \<succ>\<midarrow>n\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   275
declare split_if     [split] split_if_asm     [split] 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   276
        option.split [split] option.split_asm [split]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   277
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   278
lemma evaln_Inj_elim: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w,s') \<Longrightarrow> case t of In1 ec \<Rightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   279
  (case ec of Inl e \<Rightarrow> (\<exists>v. w = In1 v) | Inr c \<Rightarrow> w = \<diamondsuit>)  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   280
  | In2 e \<Rightarrow> (\<exists>v. w = In2 v) | In3 e \<Rightarrow> (\<exists>v. w = In3 v)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   281
apply (erule evaln_cases , auto)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   282
apply (induct_tac "t")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   283
apply   (induct_tac "a")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   284
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   285
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   286
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   287
ML_setup {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   288
fun enf nam inj rhs =
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   289
let
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   290
  val name = "evaln_" ^ nam ^ "_eq"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   291
  val lhs = "G\<turnstile>s \<midarrow>" ^ inj ^ " t\<succ>\<midarrow>n\<rightarrow> (w, s')"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   292
  val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")") 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   293
	(K [Auto_tac, ALLGOALS (ftac (thm "evaln_Inj_elim")) THEN Auto_tac])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   294
  fun is_Inj (Const (inj,_) $ _) = true
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   295
    | is_Inj _                   = false
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   296
  fun pred (_ $ (Const ("Pair",_) $ _ $ (Const ("Pair", _) $ _ $ 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   297
    (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ x $ _ )))) $ _ ) = is_Inj x
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   298
in
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   299
  make_simproc name lhs pred (thm name)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   300
end;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   301
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   302
val evaln_expr_proc = enf "expr" "In1l" "\<exists>v.  w=In1 v  \<and> G\<turnstile>s \<midarrow>t-\<succ>v \<midarrow>n\<rightarrow> s'";
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   303
val evaln_var_proc  = enf "var"  "In2"  "\<exists>vf. w=In2 vf \<and> G\<turnstile>s \<midarrow>t=\<succ>vf\<midarrow>n\<rightarrow> s'";
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   304
val evaln_exprs_proc= enf "exprs""In3"  "\<exists>vs. w=In3 vs \<and> G\<turnstile>s \<midarrow>t\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s'";
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   305
val evaln_stmt_proc = enf "stmt" "In1r" "     w=\<diamondsuit>      \<and> G\<turnstile>s \<midarrow>t     \<midarrow>n\<rightarrow> s'";
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   306
Addsimprocs [evaln_expr_proc,evaln_var_proc,evaln_exprs_proc,evaln_stmt_proc];
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   307
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   308
bind_thms ("evaln_AbruptIs", sum3_instantiate (thm "evaln.Abrupt"))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   309
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   310
declare evaln_AbruptIs [intro!]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   311
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   312
lemma evaln_abrupt_lemma: "G\<turnstile>s \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (v,s') \<Longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   313
 fst s = Some xc \<longrightarrow> s' = s \<and> v = arbitrary3 e"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   314
apply (erule evaln_cases , auto)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   315
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   316
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   317
lemma evaln_abrupt: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   318
 "\<And>s'. G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s') = (s' = (Some xc,s) \<and>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   319
  w=arbitrary3 e \<and> G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (arbitrary3 e,(Some xc,s)))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   320
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   321
apply (frule evaln_abrupt_lemma, auto)+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   322
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   323
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   324
ML {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   325
local
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   326
  fun is_Some (Const ("Pair",_) $ (Const ("Option.option.Some",_) $ _)$ _) =true
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   327
    | is_Some _ = false
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   328
  fun pred (_ $ (Const ("Pair",_) $
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   329
     _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   330
       (Const ("Pair", _) $ _ $ x)))) $ _ ) = is_Some x
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   331
in
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   332
  val evaln_abrupt_proc = 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   333
 make_simproc "evaln_abrupt" "G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s')" pred (thm "evaln_abrupt")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   334
end;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   335
Addsimprocs [evaln_abrupt_proc]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   336
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   337
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   338
lemma evaln_LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else arbitrary)\<midarrow>n\<rightarrow> s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   339
apply (case_tac "s", case_tac "a = None")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   340
by (auto intro!: evaln.Lit)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   341
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   342
lemma CondI: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   343
 "\<And>s1. \<lbrakk>G\<turnstile>s \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   344
  G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else arbitrary)\<midarrow>n\<rightarrow> s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   345
apply (case_tac "s", case_tac "a = None")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   346
by (auto intro!: evaln.Cond)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   347
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   348
lemma evaln_SkipI [intro!]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   349
apply (case_tac "s", case_tac "a = None")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   350
by (auto intro!: evaln.Skip)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   351
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   352
lemma evaln_ExprI: "G\<turnstile>s \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>Expr e\<midarrow>n\<rightarrow> s'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   353
apply (case_tac "s", case_tac "a = None")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   354
by (auto intro!: evaln.Expr)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   355
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   356
lemma evaln_CompI: "\<lbrakk>G\<turnstile>s \<midarrow>c1\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c2\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow> G\<turnstile>s \<midarrow>c1;; c2\<midarrow>n\<rightarrow> s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   357
apply (case_tac "s", case_tac "a = None")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   358
by (auto intro!: evaln.Comp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   359
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   360
lemma evaln_IfI: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   361
 "\<lbrakk>G\<turnstile>s \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>(if the_Bool v then c1 else c2)\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   362
  G\<turnstile>s \<midarrow>If(e) c1 Else c2\<midarrow>n\<rightarrow> s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   363
apply (case_tac "s", case_tac "a = None")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   364
by (auto intro!: evaln.If)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   365
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   366
lemma evaln_SkipD [dest!]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s' \<Longrightarrow> s' = s" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   367
by (erule evaln_cases, auto)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   368
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   369
lemma evaln_Skip_eq [simp]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s' = (s = s')"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   370
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   371
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   372
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   373
end