src/HOL/Bali/Evaln.thy
author schirmer
Fri, 22 Feb 2002 11:26:44 +0100
changeset 12925 99131847fb93
parent 12919 d6a0d168291e
child 12937 0c4fd7529467
permissions -rw-r--r--
Added check for field/method access to operational semantics and proved the acesses valid.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12857
a4386cc9b1c3 tuned header;
wenzelm
parents: 12854
diff changeset
     1
(*  Title:      HOL/Bali/Evaln.thy
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     2
    ID:         $Id$
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
     3
    Author:     David von Oheimb and Norbert Schirmer
12859
wenzelm
parents: 12857
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
12854
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
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
    10
theory Evaln = Eval + TypeSafe:
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    11
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    12
text {*
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
    13
Variant of eval relation with counter for bounded recursive depth.
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
    14
Evaln omits the technical accessibility tests @{term check_field_access}
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
    15
and @{term check_method_access}, since we proved the absence of errors for
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
    16
wellformed programs.
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    17
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    18
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    19
consts
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    20
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    21
  evaln	:: "prog \<Rightarrow> (state \<times> term \<times> nat \<times> vals \<times> state) set"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    22
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    23
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    24
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    25
  evaln	:: "[prog, state, term,        nat, vals * state] => bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    26
				("_|-_ -_>-_-> _"   [61,61,80,   61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    27
  evarn	:: "[prog, state, var  , vvar        , nat, state] => bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    28
				("_|-_ -_=>_-_-> _" [61,61,90,61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    29
  eval_n:: "[prog, state, expr , val         , nat, state] => bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    30
				("_|-_ -_->_-_-> _" [61,61,80,61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    31
  evalsn:: "[prog, state, expr list, val list, nat, state] => bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    32
				("_|-_ -_#>_-_-> _" [61,61,61,61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    33
  execn	:: "[prog, state, stmt ,               nat, state] => bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    34
				("_|-_ -_-_-> _"    [61,61,65,   61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    35
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    36
syntax (xsymbols)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    37
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    38
  evaln	:: "[prog, state, term,         nat, vals \<times> state] \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    39
				("_\<turnstile>_ \<midarrow>_\<succ>\<midarrow>_\<rightarrow> _"   [61,61,80,   61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    40
  evarn	:: "[prog, state, var  , vvar         , nat, state] \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    41
				("_\<turnstile>_ \<midarrow>_=\<succ>_\<midarrow>_\<rightarrow> _" [61,61,90,61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    42
  eval_n:: "[prog, state, expr , val ,          nat, state] \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    43
				("_\<turnstile>_ \<midarrow>_-\<succ>_\<midarrow>_\<rightarrow> _" [61,61,80,61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    44
  evalsn:: "[prog, state, expr list, val  list, nat, state] \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    45
				("_\<turnstile>_ \<midarrow>_\<doteq>\<succ>_\<midarrow>_\<rightarrow> _" [61,61,61,61,61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    46
  execn	:: "[prog, state, stmt ,                nat, state] \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    47
				("_\<turnstile>_ \<midarrow>_\<midarrow>_\<rightarrow> _"     [61,61,65,   61,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    48
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    49
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    50
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    51
  "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
    52
  "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
    53
  "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
    54
  "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
    55
  "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
    56
  "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
    57
  "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
    58
  "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
    59
  "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
    60
  "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
    61
  "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
    62
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    63
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    64
inductive "evaln G" intros
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    65
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    66
(* propagation of abrupt completion *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    67
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    68
  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
    69
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    70
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    71
(* evaluation of variables *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    72
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    73
  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
    74
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
    75
  FVar:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s2;
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
    76
	  (v,s2') = fvar statDeclC stat fn a' s2\<rbrakk> \<Longrightarrow>
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
    77
	  G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>n\<rightarrow> s2'"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    78
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    79
  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
    80
	  (v,s2') = avar G i a s2\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    81
	              G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<midarrow>n\<rightarrow> s2'"
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
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    85
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    86
(* evaluation of expressions *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    87
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    88
  NewC:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    89
	  G\<turnstile>     s1 \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s2\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    90
	                          G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<midarrow>n\<rightarrow> s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    91
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    92
  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
    93
	  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
    94
	                        G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<midarrow>n\<rightarrow> s3"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    95
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    96
  Cast:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    97
	  s2 = abupd (raise_if (\<not>G,snd s1\<turnstile>v fits T) ClassCast) s1\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    98
			        G\<turnstile>Norm s0 \<midarrow>Cast T e-\<succ>v\<midarrow>n\<rightarrow> s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    99
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   100
  Inst:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   101
	  b = (v\<noteq>Null \<and> G,store s1\<turnstile>v fits RefT T)\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   102
			      G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<midarrow>n\<rightarrow> s1"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   103
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   104
  Lit:			   "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   105
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   106
  Super:		   "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   107
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   108
  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
   109
	                          G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<midarrow>n\<rightarrow> s1"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   110
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   111
  Ass:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w,f)\<midarrow>n\<rightarrow> s1;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   112
          G\<turnstile>     s1 \<midarrow>e-\<succ>v     \<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   113
				   G\<turnstile>Norm s0 \<midarrow>va:=e-\<succ>v\<midarrow>n\<rightarrow> assign f v s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   114
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   115
  Cond:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n\<rightarrow> s1;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   116
          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
   117
			    G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<midarrow>n\<rightarrow> s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   118
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   119
  Call:	
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   120
  "\<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
   121
    D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   122
    G\<turnstile>init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs s2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   123
            \<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ>v\<midarrow>n\<rightarrow> s3\<rbrakk>
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   124
   \<Longrightarrow> 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   125
    G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}args)-\<succ>v\<midarrow>n\<rightarrow> (restore_lvars s2 s3)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   126
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   127
  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
   128
				G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   129
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   130
  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
   131
 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
   132
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   133
(* evaluation of expression lists *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   134
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   135
  Nil:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   136
				"G\<turnstile>Norm s0 \<midarrow>[]\<doteq>\<succ>[]\<midarrow>n\<rightarrow> Norm s0"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   137
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   138
  Cons:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e -\<succ> v \<midarrow>n\<rightarrow> s1;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   139
          G\<turnstile>     s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   140
			     G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<midarrow>n\<rightarrow> s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   141
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   142
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   143
(* execution of statements *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   144
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   145
  Skip:	 			    "G\<turnstile>Norm s \<midarrow>Skip\<midarrow>n\<rightarrow> Norm s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   146
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   147
  Expr:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   148
				  G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   149
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   150
  Lab:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   151
                             G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb (Break l)) s1"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   152
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   153
  Comp:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<midarrow>n\<rightarrow> s1;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   154
	  G\<turnstile>     s1 \<midarrow>c2 \<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   155
				 G\<turnstile>Norm s0 \<midarrow>c1;; c2\<midarrow>n\<rightarrow> s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   156
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   157
  If:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   158
	  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
   159
		       G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2 \<midarrow>n\<rightarrow> s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   160
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   161
  Loop:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   162
	  if normal s1 \<and> the_Bool b 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   163
             then (G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2 \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   164
                   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
   165
	     else s3 = s1\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   166
			      G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>n\<rightarrow> s3"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   167
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   168
  Do: "G\<turnstile>Norm s \<midarrow>Do j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   169
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   170
  Throw:"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   171
				 G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> abupd (throw a') s1"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   172
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   173
  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
   174
	  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
   175
          \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   176
		  G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(tn vn) c2\<midarrow>n\<rightarrow> s3"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   177
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   178
  Fin:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n\<rightarrow> (x1,s1);
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   179
	  G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   180
              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
   181
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   182
  Init:	"\<lbrakk>the (class G C) = c;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   183
	  if inited C (globs s0) then s3 = Norm s0
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   184
	  else (G\<turnstile>Norm (init_class_obj G C s0)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   185
	          \<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n\<rightarrow> s1 \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   186
	        G\<turnstile>set_lvars empty s1 \<midarrow>init c\<midarrow>n\<rightarrow> s2 \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   187
                s3 = restore_lvars s1 s2)\<rbrakk>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   188
          \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   189
		 G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   190
monos
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   191
  if_def2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   192
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   193
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   194
declare split_if     [split del] split_if_asm     [split del]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   195
        option.split [split del] option.split_asm [split del]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   196
inductive_cases evaln_cases: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   197
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   198
inductive_cases evaln_elim_cases:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   199
	"G\<turnstile>(Some xc, s) \<midarrow>t                        \<succ>\<midarrow>n\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   200
	"G\<turnstile>Norm s \<midarrow>In1r Skip                      \<succ>\<midarrow>n\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   201
        "G\<turnstile>Norm s \<midarrow>In1r (Do j)                    \<succ>\<midarrow>n\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   202
        "G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> c)                    \<succ>\<midarrow>n\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   203
	"G\<turnstile>Norm s \<midarrow>In3  ([])                      \<succ>\<midarrow>n\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   204
	"G\<turnstile>Norm s \<midarrow>In3  (e#es)                    \<succ>\<midarrow>n\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   205
	"G\<turnstile>Norm s \<midarrow>In1l (Lit w)                   \<succ>\<midarrow>n\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   206
	"G\<turnstile>Norm s \<midarrow>In2  (LVar vn)                 \<succ>\<midarrow>n\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   207
	"G\<turnstile>Norm s \<midarrow>In1l (Cast T e)                \<succ>\<midarrow>n\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   208
	"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T)              \<succ>\<midarrow>n\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   209
	"G\<turnstile>Norm s \<midarrow>In1l (Super)                   \<succ>\<midarrow>n\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   210
	"G\<turnstile>Norm s \<midarrow>In1l (Acc va)                  \<succ>\<midarrow>n\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   211
	"G\<turnstile>Norm s \<midarrow>In1r (Expr e)                  \<succ>\<midarrow>n\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   212
	"G\<turnstile>Norm s \<midarrow>In1r (c1;; c2)                 \<succ>\<midarrow>n\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   213
	"G\<turnstile>Norm s \<midarrow>In1l (Methd C sig)             \<succ>\<midarrow>n\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   214
	"G\<turnstile>Norm s \<midarrow>In1l (Body D c)                \<succ>\<midarrow>n\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   215
	"G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2)            \<succ>\<midarrow>n\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   216
	"G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2)        \<succ>\<midarrow>n\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   217
	"G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> While(e) c)           \<succ>\<midarrow>n\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   218
	"G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2)           \<succ>\<midarrow>n\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   219
	"G\<turnstile>Norm s \<midarrow>In1r (Throw e)                 \<succ>\<midarrow>n\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   220
	"G\<turnstile>Norm s \<midarrow>In1l (NewC C)                  \<succ>\<midarrow>n\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   221
	"G\<turnstile>Norm s \<midarrow>In1l (New T[e])                \<succ>\<midarrow>n\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   222
	"G\<turnstile>Norm s \<midarrow>In1l (Ass va e)                \<succ>\<midarrow>n\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   223
	"G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2)  \<succ>\<midarrow>n\<rightarrow> xs'"
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   224
	"G\<turnstile>Norm s \<midarrow>In2  ({accC,statDeclC,stat}e..fn) \<succ>\<midarrow>n\<rightarrow> vs'"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   225
	"G\<turnstile>Norm s \<midarrow>In2  (e1.[e2])                 \<succ>\<midarrow>n\<rightarrow> vs'"
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   226
	"G\<turnstile>Norm s \<midarrow>In1l ({accC,statT,mode}e\<cdot>mn({pT}p)) \<succ>\<midarrow>n\<rightarrow> vs'"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   227
	"G\<turnstile>Norm s \<midarrow>In1r (Init C)                  \<succ>\<midarrow>n\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   228
declare split_if     [split] split_if_asm     [split] 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   229
        option.split [split] option.split_asm [split]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   230
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   231
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
   232
  (case ec of Inl e \<Rightarrow> (\<exists>v. w = In1 v) | Inr c \<Rightarrow> w = \<diamondsuit>)  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   233
  | In2 e \<Rightarrow> (\<exists>v. w = In2 v) | In3 e \<Rightarrow> (\<exists>v. w = In3 v)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   234
apply (erule evaln_cases , auto)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   235
apply (induct_tac "t")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   236
apply   (induct_tac "a")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   237
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   238
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   239
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   240
ML_setup {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   241
fun enf nam inj rhs =
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   242
let
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   243
  val name = "evaln_" ^ nam ^ "_eq"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   244
  val lhs = "G\<turnstile>s \<midarrow>" ^ inj ^ " t\<succ>\<midarrow>n\<rightarrow> (w, s')"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   245
  val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")") 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   246
	(K [Auto_tac, ALLGOALS (ftac (thm "evaln_Inj_elim")) THEN Auto_tac])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   247
  fun is_Inj (Const (inj,_) $ _) = true
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   248
    | is_Inj _                   = false
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   249
  fun pred (_ $ (Const ("Pair",_) $ _ $ (Const ("Pair", _) $ _ $ 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   250
    (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ x $ _ )))) $ _ ) = is_Inj x
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   251
in
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   252
  make_simproc name lhs pred (thm name)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   253
end;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   254
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   255
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
   256
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
   257
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
   258
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
   259
Addsimprocs [evaln_expr_proc,evaln_var_proc,evaln_exprs_proc,evaln_stmt_proc];
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   260
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   261
bind_thms ("evaln_AbruptIs", sum3_instantiate (thm "evaln.Abrupt"))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   262
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   263
declare evaln_AbruptIs [intro!]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   264
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   265
lemma evaln_abrupt_lemma: "G\<turnstile>s \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (v,s') \<Longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   266
 fst s = Some xc \<longrightarrow> s' = s \<and> v = arbitrary3 e"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   267
apply (erule evaln_cases , auto)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   268
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   269
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   270
lemma evaln_abrupt: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   271
 "\<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
   272
  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
   273
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   274
apply (frule evaln_abrupt_lemma, auto)+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   275
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   276
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   277
ML {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   278
local
12919
d6a0d168291e removed theory Option;
wenzelm
parents: 12859
diff changeset
   279
  fun is_Some (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _) =true
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   280
    | is_Some _ = false
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   281
  fun pred (_ $ (Const ("Pair",_) $
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   282
     _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   283
       (Const ("Pair", _) $ _ $ x)))) $ _ ) = is_Some x
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   284
in
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   285
  val evaln_abrupt_proc = 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   286
 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
   287
end;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   288
Addsimprocs [evaln_abrupt_proc]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   289
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   290
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   291
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
   292
apply (case_tac "s", case_tac "a = None")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   293
by (auto intro!: evaln.Lit)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   294
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   295
lemma CondI: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   296
 "\<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
   297
  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
   298
apply (case_tac "s", case_tac "a = None")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   299
by (auto intro!: evaln.Cond)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   300
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   301
lemma evaln_SkipI [intro!]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   302
apply (case_tac "s", case_tac "a = None")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   303
by (auto intro!: evaln.Skip)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   304
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   305
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
   306
apply (case_tac "s", case_tac "a = None")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   307
by (auto intro!: evaln.Expr)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   308
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   309
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
   310
apply (case_tac "s", case_tac "a = None")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   311
by (auto intro!: evaln.Comp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   312
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   313
lemma evaln_IfI: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   314
 "\<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
   315
  G\<turnstile>s \<midarrow>If(e) c1 Else c2\<midarrow>n\<rightarrow> s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   316
apply (case_tac "s", case_tac "a = None")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   317
by (auto intro!: evaln.If)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   318
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   319
lemma evaln_SkipD [dest!]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s' \<Longrightarrow> s' = s" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   320
by (erule evaln_cases, auto)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   321
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   322
lemma evaln_Skip_eq [simp]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s' = (s = s')"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   323
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   324
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   325
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   326
lemma evaln_eval:  
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   327
 (assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   328
             wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and  
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   329
        conf_s0: "s0\<Colon>\<preceq>(G, L)" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   330
             wf: "wf_prog G" 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   331
       
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   332
 )  "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   333
proof -
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   334
  from evaln 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   335
  show "\<And> L accC T. \<lbrakk>s0\<Colon>\<preceq>(G, L);\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T\<rbrakk>
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   336
                    \<Longrightarrow> G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   337
       (is "PROP ?EqEval s0 s1 t v")
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   338
  proof (induct)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   339
    case Abrupt
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   340
    show ?case by (rule eval.Abrupt)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   341
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   342
    case LVar
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   343
    show ?case by (rule eval.LVar)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   344
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   345
    case (FVar a accC' e fn n s0 s1 s2 s2' stat statDeclC v L accC T)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   346
    have eval_initn: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n\<rightarrow> s1" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   347
    have eval_en: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s2" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   348
    have hyp_init: "PROP ?EqEval (Norm s0) s1 (In1r (Init statDeclC)) \<diamondsuit>" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   349
    have hyp_e: "PROP ?EqEval s1 s2 (In1l e) (In1 a)" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   350
    have fvar: "(v, s2') = fvar statDeclC stat fn a s2" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   351
    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   352
    have wt: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>In2 ({accC',statDeclC,stat}e..fn)\<Colon>T" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   353
    then obtain statC f where
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   354
                wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   355
            accfield: "accfield G accC statC fn = Some (statDeclC,f)" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   356
                stat: "stat=is_static f" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   357
               accC': "accC'=accC" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   358
	           T: "T=(Inl (type f))"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   359
       by (rule wt_elim_cases) (auto simp add: member_is_static_simp)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   360
    from wf wt_e 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   361
    have iscls_statC: "is_class G statC"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   362
      by (auto dest: ty_expr_is_type type_is_class)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   363
    with wf accfield 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   364
    have iscls_statDeclC: "is_class G statDeclC"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   365
      by (auto dest!: accfield_fields dest: fields_declC)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   366
    then 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   367
    have wt_init: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>(Init statDeclC)\<Colon>\<surd>"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   368
      by simp
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   369
    from conf_s0 wt_init
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   370
    have eval_init: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   371
      by (rule hyp_init)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   372
    with wt_init conf_s0 wf 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   373
    have conf_s1: "s1\<Colon>\<preceq>(G, L)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   374
      by (blast dest: exec_ts)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   375
    with hyp_e wt_e
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   376
    have eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   377
      by blast
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   378
    with wf conf_s1 wt_e
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   379
    obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   380
            conf_a: "normal s2 \<longrightarrow> G,store s2\<turnstile>a\<Colon>\<preceq>Class statC"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   381
      by (auto dest!: eval_type_sound)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   382
    obtain s3 where
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   383
      check: "s3 = check_field_access G accC statDeclC fn stat a s2'"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   384
      by simp
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   385
    from accfield wt_e eval_init eval_e conf_s2 conf_a fvar stat check  wf
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   386
    have eq_s3_s2': "s3=s2'"  
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   387
      by (auto dest!: error_free_field_access)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   388
    with eval_init eval_e fvar check accC'
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   389
    show "G\<turnstile>Norm s0 \<midarrow>{accC',statDeclC,stat}e..fn=\<succ>v\<rightarrow> s2'"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   390
      by (auto intro: eval.FVar)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   391
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   392
    case AVar
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   393
    with wf show ?case
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   394
      apply -
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   395
      apply (erule wt_elim_cases)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   396
      apply (blast intro!: eval.AVar dest: eval_type_sound)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   397
      done
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   398
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   399
    case NewC
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   400
    with wf show ?case
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   401
      apply - 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   402
      apply (erule wt_elim_cases)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   403
      apply (blast intro!: eval.NewC dest: eval_type_sound is_acc_classD)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   404
      done
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   405
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   406
    case (NewA T a e i n s0 s1 s2 s3 L accC Ta) 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   407
    have hyp_init: "PROP ?EqEval (Norm s0) s1 (In1r (init_comp_ty T)) \<diamondsuit>" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   408
    have hyp_size: "PROP ?EqEval s1 s2 (In1l e) (In1 i)" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   409
    have "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (New T[e])\<Colon>Ta" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   410
    then obtain
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   411
       wt_init: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>init_comp_ty T\<Colon>\<surd>" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   412
       wt_size: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Integer"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   413
      by (rule wt_elim_cases) (auto intro: wt_init_comp_ty dest: is_acc_typeD)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   414
    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   415
    from this wt_init 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   416
    have eval_init: "G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<rightarrow> s1"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   417
      by (rule hyp_init)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   418
    moreover
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   419
    from eval_init wt_init wf conf_s0
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   420
    have "s1\<Colon>\<preceq>(G, L)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   421
      by (auto dest: eval_type_sound)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   422
    from this wt_size 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   423
    have "G\<turnstile>s1 \<midarrow>e-\<succ>i\<rightarrow> s2"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   424
      by (rule hyp_size)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   425
    moreover note NewA
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   426
    ultimately show ?case
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   427
      by (blast intro!: eval.NewA)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   428
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   429
    case Cast
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   430
    with wf show ?case
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   431
      by - (erule wt_elim_cases, rule eval.Cast,auto dest: eval_type_sound)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   432
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   433
    case Inst
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   434
    with wf show ?case
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   435
      by - (erule wt_elim_cases, rule eval.Inst,auto dest: eval_type_sound)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   436
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   437
    case Lit
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   438
    show ?case by (rule eval.Lit)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   439
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   440
    case Super
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   441
    show ?case by (rule eval.Super)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   442
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   443
    case Acc
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   444
    then show ?case
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   445
      by - (erule wt_elim_cases, rule eval.Acc,auto dest: eval_type_sound)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   446
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   447
    case Ass
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   448
    with wf show ?case
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   449
      by - (erule wt_elim_cases, blast intro!: eval.Ass dest: eval_type_sound) 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   450
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   451
    case (Cond b e0 e1 e2 n s0 s1 s2 v L accC T)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   452
    have hyp_e0: "PROP ?EqEval (Norm s0) s1 (In1l e0) (In1 b)" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   453
    have hyp_if: "PROP ?EqEval s1 s2 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   454
                              (In1l (if the_Bool b then e1 else e2)) (In1 v)" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   455
    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   456
    have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (e0 ? e1 : e2)\<Colon>T" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   457
    then obtain T1 T2 statT where
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   458
       wt_e0: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e0\<Colon>-PrimT Boolean" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   459
       wt_e1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e1\<Colon>-T1" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   460
       wt_e2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e2\<Colon>-T2" and 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   461
       statT: "G\<turnstile>T1\<preceq>T2 \<and> statT = T2  \<or>  G\<turnstile>T2\<preceq>T1 \<and> statT =  T1" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   462
       T    : "T=Inl statT"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   463
      by (rule wt_elim_cases) auto
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   464
    from conf_s0 wt_e0
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   465
    have eval_e0: "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   466
      by (rule hyp_e0)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   467
    moreover
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   468
    from eval_e0 conf_s0 wf wt_e0
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   469
    have "s1\<Colon>\<preceq>(G, L)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   470
      by (blast dest: eval_type_sound)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   471
    with wt_e1 wt_e2 statT hyp_if
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   472
    have "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   473
      by (cases "the_Bool b") auto
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   474
    ultimately
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   475
    show ?case
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   476
      by (rule eval.Cond)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   477
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   478
    case (Call invDeclC a' accC' args e mn mode n pTs' s0 s1 s2 s4 statT 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   479
           v vs L accC T)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   480
    (* Repeats large parts of the type soundness proof. One should factor
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   481
       out some lemmata about the relations and conformance of s2, s3 and s3'*)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   482
    have evaln_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s1" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   483
    have evaln_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s2" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   484
    have invDeclC: "invDeclC 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   485
                      = invocation_declclass G mode (store s2) a' statT 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   486
                           \<lparr>name = mn, parTs = pTs'\<rparr>" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   487
    let ?InitLvars 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   488
         = "init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> mode a' vs s2"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   489
    obtain s3 s3' where 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   490
      init_lvars: "s3 = 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   491
             init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> mode a' vs s2" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   492
      check: "s3' =
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   493
         check_method_access G accC' statT mode \<lparr>name = mn, parTs = pTs'\<rparr> a' s3"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   494
      by simp
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   495
    have evaln_methd: 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   496
           "G\<turnstile>?InitLvars \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<midarrow>n\<rightarrow> s4" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   497
    have     hyp_e: "PROP ?EqEval (Norm s0) s1 (In1l e) (In1 a')" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   498
    have  hyp_args: "PROP ?EqEval s1 s2 (In3 args) (In3 vs)" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   499
    have hyp_methd: "PROP ?EqEval ?InitLvars s4 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   500
                     (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)".
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   501
    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   502
    have      wt: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   503
                    \<turnstile>In1l ({accC',statT,mode}e\<cdot>mn( {pTs'}args))\<Colon>T" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   504
    from wt obtain pTs statDeclT statM where
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   505
                 wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   506
              wt_args: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>args\<Colon>\<doteq>pTs" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   507
                statM: "max_spec G accC statT \<lparr>name=mn,parTs=pTs\<rparr> 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   508
                         = {((statDeclT,statM),pTs')}" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   509
                 mode: "mode = invmode statM e" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   510
                    T: "T =Inl (resTy statM)" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   511
        eq_accC_accC': "accC=accC'"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   512
      by (rule wt_elim_cases) auto
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   513
    from conf_s0 wt_e hyp_e
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   514
    have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   515
      by blast
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   516
    with wf conf_s0 wt_e
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   517
    obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   518
           conf_a': "normal s1 \<Longrightarrow> G, store s1\<turnstile>a'\<Colon>\<preceq>RefT statT" 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   519
      by (auto dest!: eval_type_sound)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   520
    from conf_s1 wt_args hyp_args
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   521
    have eval_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   522
      by blast
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   523
    with wt_args conf_s1 wf 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   524
    obtain    conf_s2: "s2\<Colon>\<preceq>(G, L)" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   525
            conf_args: "normal s2 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   526
                         \<Longrightarrow>  list_all2 (conf G (store s2)) vs pTs" 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   527
      by (auto dest!: eval_type_sound)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   528
    from statM 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   529
    obtain
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   530
       statM': "(statDeclT,statM)\<in>mheads G accC statT \<lparr>name=mn,parTs=pTs'\<rparr>" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   531
       pTs_widen: "G\<turnstile>pTs[\<preceq>]pTs'"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   532
      by (blast dest: max_spec2mheads)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   533
    from check
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   534
    have eq_store_s3'_s3: "store s3'=store s3"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   535
      by (cases s3) (simp add: check_method_access_def Let_def)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   536
    obtain invC
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   537
      where invC: "invC = invocation_class mode (store s2) a' statT"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   538
      by simp
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   539
    with init_lvars
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   540
    have invC': "invC = (invocation_class mode (store s3) a' statT)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   541
      by (cases s2,cases mode) (auto simp add: init_lvars_def2 )
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   542
    show "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   543
             -\<succ>v\<rightarrow> (set_lvars (locals (store s2))) s4"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   544
    proof (cases "normal s2")
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   545
      case False
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   546
      with init_lvars 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   547
      obtain keep_abrupt: "abrupt s3 = abrupt s2" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   548
             "store s3 = store (init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   549
                                            mode a' vs s2)" 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   550
	by (auto simp add: init_lvars_def2)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   551
      moreover
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   552
      from keep_abrupt False check
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   553
      have eq_s3'_s3: "s3'=s3" 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   554
	by (auto simp add: check_method_access_def Let_def)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   555
      moreover
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   556
      from eq_s3'_s3 False keep_abrupt evaln_methd init_lvars
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   557
      obtain "s4=s3'"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   558
	 "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   559
	by auto
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   560
      moreover note False
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   561
      ultimately have
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   562
	"G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<rightarrow> s4"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   563
	by (auto)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   564
      from eval_e eval_args invDeclC init_lvars check this
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   565
      show ?thesis
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   566
	by (rule eval.Call)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   567
    next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   568
      case True
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   569
      note normal_s2 = True
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   570
      with eval_args
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   571
      have normal_s1: "normal s1"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   572
	by (cases "normal s1") auto
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   573
      with conf_a' eval_args 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   574
      have conf_a'_s2: "G, store s2\<turnstile>a'\<Colon>\<preceq>RefT statT"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   575
	by (auto dest: eval_gext intro: conf_gext)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   576
      show ?thesis
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   577
      proof (cases "a'=Null \<longrightarrow> is_static statM")
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   578
	case False
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   579
	then obtain not_static: "\<not> is_static statM" and Null: "a'=Null" 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   580
	  by blast
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   581
	with normal_s2 init_lvars mode
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   582
	obtain np: "abrupt s3 = Some (Xcpt (Std NullPointer))" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   583
                   "store s3 = store (init_lvars G invDeclC 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   584
                                       \<lparr>name = mn, parTs = pTs'\<rparr> mode a' vs s2)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   585
	  by (auto simp add: init_lvars_def2)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   586
	moreover
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   587
	from np check
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   588
	have eq_s3'_s3: "s3'=s3" 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   589
	  by (auto simp add: check_method_access_def Let_def)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   590
	moreover
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   591
	from eq_s3'_s3 np evaln_methd init_lvars
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   592
	obtain "s4=s3'"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   593
	  "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   594
	  by auto
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   595
	moreover note np 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   596
	ultimately have
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   597
	  "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<rightarrow> s4"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   598
	  by (auto)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   599
	from eval_e eval_args invDeclC init_lvars check this
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   600
	show ?thesis
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   601
	  by (rule eval.Call)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   602
      next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   603
	case True
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   604
	with mode have notNull: "mode = IntVir \<longrightarrow> a' \<noteq> Null"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   605
	  by (auto dest!: Null_staticD)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   606
	with conf_s2 conf_a'_s2 wf invC 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   607
	have dynT_prop: "G\<turnstile>mode\<rightarrow>invC\<preceq>statT"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   608
	  by (cases s2) (auto intro: DynT_propI)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   609
	with wt_e statM' invC mode wf 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   610
	obtain dynM where 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   611
           dynM: "dynlookup G statT invC  \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   612
           acc_dynM: "G \<turnstile>Methd  \<lparr>name=mn,parTs=pTs'\<rparr> dynM 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   613
                          in invC dyn_accessible_from accC"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   614
	  by (force dest!: call_access_ok)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   615
	with invC' check eq_accC_accC'
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   616
	have eq_s3'_s3: "s3'=s3"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   617
	  by (auto simp add: check_method_access_def Let_def)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   618
	from dynT_prop wf wt_e statM' mode invC invDeclC dynM 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   619
	obtain 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   620
	   wf_dynM: "wf_mdecl G invDeclC (\<lparr>name=mn,parTs=pTs'\<rparr>,mthd dynM)" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   621
	     dynM': "methd G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   622
           iscls_invDeclC: "is_class G invDeclC" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   623
	        invDeclC': "invDeclC = declclass dynM" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   624
	     invC_widen: "G\<turnstile>invC\<preceq>\<^sub>C invDeclC" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   625
	   is_static_eq: "is_static dynM = is_static statM" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   626
	   involved_classes_prop:
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   627
             "(if invmode statM e = IntVir
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   628
               then \<forall>statC. statT = ClassT statC \<longrightarrow> G\<turnstile>invC\<preceq>\<^sub>C statC
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   629
               else ((\<exists>statC. statT = ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C invDeclC) \<or>
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   630
                     (\<forall>statC. statT \<noteq> ClassT statC \<and> invDeclC = Object)) \<and>
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   631
                      statDeclT = ClassT invDeclC)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   632
	  by (auto dest: DynT_mheadsD)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   633
	obtain L' where 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   634
	   L':"L'=(\<lambda> k. 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   635
                 (case k of
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   636
                    EName e
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   637
                    \<Rightarrow> (case e of 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   638
                          VNam v 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   639
                          \<Rightarrow>(table_of (lcls (mbody (mthd dynM)))
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   640
                             (pars (mthd dynM)[\<mapsto>]pTs')) v
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   641
                        | Res \<Rightarrow> Some (resTy dynM))
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   642
                  | This \<Rightarrow> if is_static statM 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   643
                            then None else Some (Class invDeclC)))"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   644
	  by simp
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   645
	from wf_dynM [THEN wf_mdeclD1, THEN conjunct1] normal_s2 conf_s2 wt_e
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   646
              wf eval_args conf_a' mode notNull wf_dynM involved_classes_prop
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   647
	have conf_s3: "s3\<Colon>\<preceq>(G,L')"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   648
	   apply - 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   649
          (*FIXME confomrs_init_lvars should be 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   650
                adjusted to be more directy applicable *)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   651
	   apply (drule conforms_init_lvars [of G invDeclC 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   652
                  "\<lparr>name=mn,parTs=pTs'\<rparr>" dynM "store s2" vs pTs "abrupt s2" 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   653
                  L statT invC a' "(statDeclT,statM)" e])
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   654
	     apply (rule wf)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   655
	     apply (rule conf_args,assumption)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   656
	     apply (simp add: pTs_widen)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   657
	     apply (cases s2,simp)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   658
	     apply (rule dynM')
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   659
	     apply (force dest: ty_expr_is_type)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   660
	     apply (rule invC_widen)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   661
	     apply (force intro: conf_gext dest: eval_gext)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   662
	     apply simp
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   663
	     apply simp
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   664
	     apply (simp add: invC)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   665
	     apply (simp add: invDeclC)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   666
	     apply (force dest: wf_mdeclD1 is_acc_typeD)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   667
	     apply (cases s2, simp add: L' init_lvars
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   668
	                      cong add: lname.case_cong ename.case_cong)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   669
	   done
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   670
	from is_static_eq wf_dynM L'
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   671
	obtain mthdT where
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   672
	   "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   673
            \<turnstile>Body invDeclC (stmt (mbody (mthd dynM)))\<Colon>-mthdT" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   674
	   mthdT_widen: "G\<turnstile>mthdT\<preceq>resTy dynM"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   675
	  by - (drule wf_mdecl_bodyD,
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   676
                simp cong add: lname.case_cong ename.case_cong)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   677
	with dynM' iscls_invDeclC invDeclC'
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   678
	have
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   679
	   "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   680
            \<turnstile>(Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)\<Colon>-mthdT"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   681
	  by (auto intro: wt.Methd)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   682
	with conf_s3 hyp_methd init_lvars eq_s3'_s3
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   683
	have "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<rightarrow> s4"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   684
	  by auto
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   685
	from eval_e eval_args invDeclC init_lvars check this
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   686
	show ?thesis
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   687
	  by (rule eval.Call)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   688
      qed
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   689
    qed
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   690
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   691
    case Methd
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   692
    with wf show ?case
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   693
      by - (erule wt_elim_cases, rule eval.Methd, 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   694
            auto dest: eval_type_sound simp add: body_def2)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   695
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   696
    case Body
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   697
    with wf show ?case
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   698
       by - (erule wt_elim_cases, blast intro!: eval.Body dest: eval_type_sound)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   699
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   700
    case Nil
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   701
    show ?case by (rule eval.Nil)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   702
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   703
    case Cons
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   704
    with wf show ?case
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   705
      by - (erule wt_elim_cases, blast intro!: eval.Cons dest: eval_type_sound)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   706
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   707
    case Skip
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   708
    show ?case by (rule eval.Skip)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   709
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   710
    case Expr
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   711
    with wf show ?case
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   712
      by - (erule wt_elim_cases, rule eval.Expr,auto dest: eval_type_sound)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   713
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   714
    case Lab
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   715
    with wf show ?case
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   716
      by - (erule wt_elim_cases, rule eval.Lab,auto dest: eval_type_sound)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   717
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   718
    case Comp
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   719
    with wf show ?case
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   720
      by - (erule wt_elim_cases, blast intro!: eval.Comp dest: eval_type_sound)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   721
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   722
    case (If b c1 c2 e n s0 s1 s2 L accC T)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   723
    have hyp_e: "PROP ?EqEval (Norm s0) s1 (In1l e) (In1 b)" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   724
    have hyp_then_else: 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   725
      "PROP ?EqEval s1 s2 (In1r (if the_Bool b then c1 else c2)) \<diamondsuit>" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   726
    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   727
    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (If(e) c1 Else c2)\<Colon>T" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   728
    then obtain 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   729
              wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   730
      wt_then_else: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   731
      by (rule wt_elim_cases) (auto split add: split_if)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   732
    from conf_s0 wt_e
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   733
    have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   734
      by (rule hyp_e)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   735
    moreover
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   736
    from eval_e wt_e conf_s0 wf
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   737
    have "s1\<Colon>\<preceq>(G, L)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   738
      by (blast dest: eval_type_sound)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   739
    from this wt_then_else
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   740
    have "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   741
      by (rule hyp_then_else)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   742
    ultimately
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   743
    show ?case
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   744
      by (rule eval.If)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   745
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   746
    case (Loop b c e l n s0 s1 s2 s3 L accC T)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   747
    have hyp_e: "PROP ?EqEval (Norm s0) s1 (In1l e) (In1 b)" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   748
    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   749
    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   750
    then obtain wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   751
                wt_c: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   752
      by (rule wt_elim_cases) (blast)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   753
    from conf_s0 wt_e 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   754
    have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   755
      by (rule hyp_e)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   756
    moreover
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   757
    from eval_e wt_e conf_s0 wf
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   758
    have conf_s1: "s1\<Colon>\<preceq>(G, L)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   759
      by (blast dest: eval_type_sound)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   760
    have "if normal s1 \<and> the_Bool b 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   761
             then (G\<turnstile>s1 \<midarrow>c\<rightarrow> s2 \<and> 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   762
                   G\<turnstile>(abupd (absorb (Cont l)) s2) \<midarrow>l\<bullet> While(e) c\<rightarrow> s3)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   763
	     else s3 = s1"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   764
    proof (cases "normal s1 \<and> the_Bool b")
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   765
      case True 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   766
      from Loop True have hyp_c: "PROP ?EqEval s1 s2 (In1r c) \<diamondsuit>"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   767
	by (auto)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   768
      from Loop True have hyp_w: "PROP ?EqEval (abupd (absorb (Cont l)) s2)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   769
                                        s3 (In1r (l\<bullet> While(e) c)) \<diamondsuit>"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   770
	by (auto)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   771
      from conf_s1 wt_c
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   772
      have eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   773
	by (rule hyp_c)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   774
      moreover
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   775
      from eval_c conf_s1 wt_c wf
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   776
      have "s2\<Colon>\<preceq>(G, L)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   777
	by (blast dest: eval_type_sound)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   778
      then
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   779
      have "abupd (absorb (Cont l)) s2 \<Colon>\<preceq>(G, L)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   780
	by (cases s2) (auto intro: conforms_absorb)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   781
      from this and wt
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   782
      have "G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   783
	by (rule hyp_w)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   784
      moreover note True
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   785
      ultimately
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   786
      show ?thesis
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   787
	by simp
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   788
    next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   789
      case False
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   790
      with Loop have "s3 = s1" by simp
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   791
      with False
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   792
      show ?thesis 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   793
	by auto
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   794
    qed
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   795
    ultimately
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   796
    show ?case
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   797
      by (rule eval.Loop)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   798
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   799
    case Do
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   800
    show ?case by (rule eval.Do)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   801
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   802
    case Throw
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   803
    with wf show ?case
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   804
      by - (erule wt_elim_cases, rule eval.Throw,auto dest: eval_type_sound)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   805
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   806
    case (Try c1 c2 n s0 s1 s2 s3 catchC vn L accC T)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   807
    have  hyp_c1: "PROP ?EqEval (Norm s0) s1 (In1r c1) \<diamondsuit>" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   808
    have conf_s0:"Norm s0\<Colon>\<preceq>(G, L)" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   809
    have      wt:"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>In1r (Try c1 Catch(catchC vn) c2)\<Colon>T" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   810
    then obtain 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   811
      wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   812
      wt_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<lparr>lcl := L(VName vn\<mapsto>Class catchC)\<rparr>\<turnstile>c2\<Colon>\<surd>"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   813
      by (rule wt_elim_cases) (auto)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   814
    from conf_s0 wt_c1
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   815
    have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   816
      by (rule hyp_c1)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   817
    moreover
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   818
    have sxalloc: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   819
    moreover
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   820
    from eval_c1 wt_c1 conf_s0 wf
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   821
    have "s1\<Colon>\<preceq>(G, L)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   822
      by (blast dest: eval_type_sound)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   823
    with sxalloc wf
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   824
    have conf_s2: "s2\<Colon>\<preceq>(G, L)" 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   825
      by (auto dest: sxalloc_type_sound split: option.splits)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   826
    have "if G,s2\<turnstile>catch catchC then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3 else s3 = s2"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   827
    proof (cases "G,s2\<turnstile>catch catchC")
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   828
      case True
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   829
      note Catch = this
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   830
      with Try have hyp_c2: "PROP ?EqEval (new_xcpt_var vn s2) s3 (In1r c2) \<diamondsuit>"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   831
	by auto
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   832
      show ?thesis
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   833
      proof (cases "normal s1")
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   834
	case True
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   835
	with sxalloc wf 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   836
	have eq_s2_s1: "s2=s1"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   837
	  by (auto dest: sxalloc_type_sound split: option.splits)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   838
	with True 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   839
	have "\<not>  G,s2\<turnstile>catch catchC"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   840
	  by (simp add: catch_def)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   841
	with Catch show ?thesis 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   842
	  by (contradiction)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   843
      next 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   844
	case False
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   845
	with sxalloc wf
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   846
	obtain a 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   847
	  where xcpt_s2: "abrupt s2 = Some (Xcpt (Loc a))"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   848
	  by (auto dest!: sxalloc_type_sound split: option.splits)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   849
	with Catch
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   850
	have "G\<turnstile>obj_ty (the (globs (store s2) (Heap a)))\<preceq>Class catchC"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   851
	  by (cases s2) simp
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   852
	with xcpt_s2 conf_s2 wf 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   853
	have "new_xcpt_var vn s2\<Colon>\<preceq>(G, L(VName vn\<mapsto>Class catchC))"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   854
	  by (auto dest: Try_lemma)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   855
	from this wt_c2
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   856
	have "G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   857
	  by (auto intro: hyp_c2)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   858
	with Catch 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   859
	show ?thesis
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   860
	  by simp
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   861
      qed
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   862
    next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   863
      case False
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   864
      with Try
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   865
      have "s3=s2"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   866
	by simp
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   867
      with False
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   868
      show ?thesis
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   869
	by simp
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   870
    qed
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   871
    ultimately
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   872
    show ?case
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   873
      by (rule eval.Try)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   874
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   875
    case Fin
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   876
    with wf show ?case
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   877
      by -(erule wt_elim_cases, blast intro!: eval.Fin
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   878
           dest: eval_type_sound intro: conforms_NormI)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   879
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   880
    case (Init C c n s0 s1 s2 s3 L accC T)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   881
    have     cls: "the (class G C) = c" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   882
    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   883
    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Init C)\<Colon>T" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   884
    with cls
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   885
    have cls_C: "class G C = Some c"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   886
      by - (erule wt_elim_cases,auto)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   887
    have "if inited C (globs s0) then s3 = Norm s0
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   888
	  else (G\<turnstile>Norm (init_class_obj G C s0) 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   889
		  \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1 \<and>
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   890
	       G\<turnstile>set_lvars empty s1 \<midarrow>init c\<rightarrow> s2 \<and> s3 = restore_lvars s1 s2)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   891
    proof (cases "inited C (globs s0)")
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   892
      case True
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   893
      with Init have "s3 = Norm s0"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   894
	by simp
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   895
      with True show ?thesis 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   896
	by simp
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   897
    next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   898
      case False
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   899
      with Init
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   900
      obtain 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   901
	hyp_init_super: 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   902
        "PROP ?EqEval (Norm ((init_class_obj G C) s0)) s1
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   903
	               (In1r (if C = Object then Skip else Init (super c))) \<diamondsuit>"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   904
	and 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   905
        hyp_init_c:
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   906
	   "PROP ?EqEval ((set_lvars empty) s1) s2 (In1r (init c)) \<diamondsuit>" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   907
	s3: "s3 = (set_lvars (locals (store s1))) s2"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   908
	by (simp only: if_False)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   909
      from conf_s0 wf cls_C False
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   910
      have conf_s0': "(Norm ((init_class_obj G C) s0))\<Colon>\<preceq>(G, L)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   911
	by (auto dest: conforms_init_class_obj)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   912
      moreover
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   913
      from wf cls_C 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   914
      have wt_init_super:
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   915
           "\<lparr>prg = G, cls = accC, lcl = L\<rparr>
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   916
                  \<turnstile>(if C = Object then Skip else Init (super c))\<Colon>\<surd>"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   917
	by (cases "C=Object")
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   918
           (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   919
      ultimately
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   920
      have eval_init_super: 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   921
	   "G\<turnstile>Norm ((init_class_obj G C) s0) 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   922
            \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   923
	by (rule hyp_init_super)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   924
      with conf_s0' wt_init_super wf
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   925
      have "s1\<Colon>\<preceq>(G, L)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   926
	by (blast dest: eval_type_sound)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   927
      then
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   928
      have "(set_lvars empty) s1\<Colon>\<preceq>(G, empty)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   929
	by (cases s1) (auto dest: conforms_set_locals )
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   930
      with wf cls_C 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   931
      have eval_init_c: "G\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<rightarrow> s2"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   932
	by (auto intro!: hyp_init_c dest: wf_prog_cdecl wf_cdecl_wt_init)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   933
      from False eval_init_super eval_init_c s3
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   934
      show ?thesis
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   935
	by simp
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   936
    qed
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   937
    from cls this
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   938
    show ?case
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   939
      by (rule eval.Init)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   940
  qed 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   941
qed
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   942
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   943
lemma Suc_le_D_lemma: "\<lbrakk>Suc n <= m'; (\<And>m. n <= m \<Longrightarrow> P (Suc m)) \<rbrakk> \<Longrightarrow> P m'"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   944
apply (frule Suc_le_D)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   945
apply fast
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   946
done
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   947
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   948
lemma evaln_nonstrict [rule_format (no_asm), elim]: 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   949
  "\<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"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   950
apply (simp (no_asm_simp) only: split_tupled_all)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   951
apply (erule evaln.induct)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   952
apply (tactic {* ALLGOALS (EVERY'[strip_tac, TRY o etac (thm "Suc_le_D_lemma"),
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   953
  REPEAT o smp_tac 1, 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   954
  resolve_tac (thms "evaln.intros") THEN_ALL_NEW TRY o atac]) *})
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   955
(* 3 subgoals *)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   956
apply (auto split del: split_if)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   957
done
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   958
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   959
lemmas evaln_nonstrict_Suc = evaln_nonstrict [OF _ le_refl [THEN le_SucI]]
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   960
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   961
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> 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   962
             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"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   963
apply (fast intro: le_maxI1 le_maxI2)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   964
done
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   965
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   966
lemma evaln_max3: 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   967
"\<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>
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   968
 G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws1 \<and>
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   969
 G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws2 \<and> 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   970
 G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws3"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   971
apply (drule (1) evaln_max2, erule thin_rl)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   972
apply (fast intro!: le_maxI1 le_maxI2)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   973
done
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   974
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   975
lemma le_max3I1: "(n2::nat) \<le> max n1 (max n2 n3)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   976
proof -
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   977
  have "n2 \<le> max n2 n3"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   978
    by (rule le_maxI1)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   979
  also
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   980
  have "max n2 n3 \<le> max n1 (max n2 n3)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   981
    by (rule le_maxI2)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   982
  finally
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   983
  show ?thesis .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   984
qed
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   985
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   986
lemma le_max3I2: "(n3::nat) \<le> max n1 (max n2 n3)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   987
proof -
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   988
  have "n3 \<le> max n2 n3"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   989
    by (rule le_maxI2)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   990
  also
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   991
  have "max n2 n3 \<le> max n1 (max n2 n3)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   992
    by (rule le_maxI2)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   993
  finally
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   994
  show ?thesis .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   995
qed
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   996
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   997
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   998
lemma eval_evaln: 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
   999
 (assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1000
          wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and  
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1001
     conf_s0: "s0\<Colon>\<preceq>(G, L)" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1002
          wf: "wf_prog G"  
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1003
 )  "\<exists>n. G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1004
proof -
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1005
  from eval 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1006
  show "\<And> L accC T. \<lbrakk>s0\<Colon>\<preceq>(G, L);\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T\<rbrakk>
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1007
                     \<Longrightarrow> \<exists> n. G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1008
       (is "PROP ?EqEval s0 s1 t v")
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1009
  proof (induct)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1010
    case (Abrupt s t xc L accC T)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1011
    obtain n where
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1012
      "G\<turnstile>(Some xc, s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t, Some xc, s)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1013
      by (rules intro: evaln.Abrupt)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1014
    then show ?case ..
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1015
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1016
    case Skip
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1017
    show ?case by (blast intro: evaln.Skip)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1018
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1019
    case (Expr e s0 s1 v L accC T)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1020
    then obtain n where
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1021
      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1022
      by (rules elim!: wt_elim_cases)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1023
    then have "G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1024
      by (rule evaln.Expr) 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1025
    then show ?case ..
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1026
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1027
    case (Lab c l s0 s1 L accC T)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1028
    then obtain n where
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1029
      "G\<turnstile>Norm s0 \<midarrow>c\<midarrow>n\<rightarrow> s1"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1030
      by (rules elim!: wt_elim_cases)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1031
    then have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb (Break l)) s1"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1032
      by (rule evaln.Lab)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1033
    then show ?case ..
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1034
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1035
    case (Comp c1 c2 s0 s1 s2 L accC T)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1036
    with wf obtain n1 n2 where
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1037
      "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1038
      "G\<turnstile>s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1039
      by (blast elim!: wt_elim_cases dest: eval_type_sound)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1040
    then have "G\<turnstile>Norm s0 \<midarrow>c1;; c2\<midarrow>max n1 n2\<rightarrow> s2"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1041
      by (blast intro: evaln.Comp dest: evaln_max2 )
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1042
    then show ?case ..
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1043
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1044
    case (If b c1 c2 e s0 s1 s2 L accC T)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1045
    with wf obtain
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1046
      "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1047
      "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1048
      by (cases "the_Bool b") (auto elim!: wt_elim_cases)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1049
    with If wf obtain n1 n2 where
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1050
      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1051
      "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n2\<rightarrow> s2"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1052
      by (blast dest: eval_type_sound)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1053
    then have "G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2\<midarrow>max n1 n2\<rightarrow> s2"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1054
      by (blast intro: evaln.If dest: evaln_max2)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1055
    then show ?case ..
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1056
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1057
    case (Loop b c e l s0 s1 s2 s3 L accC T)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1058
    have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1059
    have hyp_e: "PROP ?EqEval (Norm s0) s1 (In1l e) (In1 b)" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1060
    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1061
    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1062
    then obtain wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1063
                wt_c: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1064
      by (rule wt_elim_cases) (blast)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1065
    from conf_s0 wt_e 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1066
    obtain n1 where
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1067
      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1068
      by (rules dest: hyp_e)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1069
    moreover
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1070
    from eval_e wt_e conf_s0 wf
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1071
    have conf_s1: "s1\<Colon>\<preceq>(G, L)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1072
      by (rules dest: eval_type_sound)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1073
    obtain n2 where
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1074
      "if normal s1 \<and> the_Bool b 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1075
             then (G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2 \<and> 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1076
                   G\<turnstile>(abupd (absorb (Cont l)) s2)\<midarrow>l\<bullet> While(e) c\<midarrow>n2\<rightarrow> s3)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1077
	     else s3 = s1"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1078
    proof (cases "normal s1 \<and> the_Bool b")
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1079
      case True
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1080
      from Loop True have hyp_c: "PROP ?EqEval s1 s2 (In1r c) \<diamondsuit>"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1081
	by (auto)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1082
      from Loop True have hyp_w: "PROP ?EqEval (abupd (absorb (Cont l)) s2)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1083
                                        s3 (In1r (l\<bullet> While(e) c)) \<diamondsuit>"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1084
	by (auto)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1085
      from Loop True have eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1086
	by simp
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1087
      from conf_s1 wt_c
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1088
      obtain m1 where 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1089
	evaln_c: "G\<turnstile>s1 \<midarrow>c\<midarrow>m1\<rightarrow> s2"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1090
	by (rules dest: hyp_c)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1091
      moreover
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1092
      from eval_c conf_s1 wt_c wf
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1093
      have "s2\<Colon>\<preceq>(G, L)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1094
	by (rules dest: eval_type_sound)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1095
      then
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1096
      have "abupd (absorb (Cont l)) s2 \<Colon>\<preceq>(G, L)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1097
	by (cases s2) (auto intro: conforms_absorb)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1098
      from this and wt
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1099
      obtain m2 where 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1100
	"G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<midarrow>m2\<rightarrow> s3"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1101
	by (blast dest: hyp_w)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1102
      moreover note True and that
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1103
      ultimately show ?thesis
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1104
	by simp (rules intro: evaln_nonstrict le_maxI1 le_maxI2)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1105
    next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1106
      case False
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1107
      with Loop have "s3 = s1"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1108
	by simp
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1109
      with False that
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1110
      show ?thesis
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1111
	by auto 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1112
    qed
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1113
    ultimately
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1114
    have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>max n1 n2\<rightarrow> s3"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1115
      apply -
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1116
      apply (rule evaln.Loop)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1117
      apply   (rules intro: evaln_nonstrict intro: le_maxI1)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1118
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1119
      apply   (auto intro: evaln_nonstrict intro: le_maxI2)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1120
      done
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1121
    then show ?case ..
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1122
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1123
    case (Do j s L accC T)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1124
    have "G\<turnstile>Norm s \<midarrow>Do j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1125
      by (rule evaln.Do)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1126
    then show ?case ..
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1127
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1128
    case (Throw a e s0 s1 L accC T)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1129
    then obtain n where
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1130
      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s1"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1131
      by (rules elim!: wt_elim_cases)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1132
    then have "G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> abupd (throw a) s1"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1133
      by (rule evaln.Throw)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1134
    then show ?case ..
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1135
  next 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1136
    case (Try catchC c1 c2 s0 s1 s2 s3 vn L accC T)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1137
    have  hyp_c1: "PROP ?EqEval (Norm s0) s1 (In1r c1) \<diamondsuit>" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1138
    have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1139
    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1140
    have      wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>In1r (Try c1 Catch(catchC vn) c2)\<Colon>T" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1141
    then obtain 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1142
      wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1143
      wt_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<lparr>lcl := L(VName vn\<mapsto>Class catchC)\<rparr>\<turnstile>c2\<Colon>\<surd>"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1144
      by (rule wt_elim_cases) (auto)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1145
    from conf_s0 wt_c1
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1146
    obtain n1 where
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1147
      "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1148
      by (blast dest: hyp_c1)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1149
    moreover 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1150
    have sxalloc: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1151
    moreover
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1152
    from eval_c1 wt_c1 conf_s0 wf
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1153
    have "s1\<Colon>\<preceq>(G, L)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1154
      by (blast dest: eval_type_sound)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1155
    with sxalloc wf
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1156
    have conf_s2: "s2\<Colon>\<preceq>(G, L)" 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1157
      by (auto dest: sxalloc_type_sound split: option.splits)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1158
    obtain n2 where
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1159
      "if G,s2\<turnstile>catch catchC then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n2\<rightarrow> s3 else s3 = s2"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1160
    proof (cases "G,s2\<turnstile>catch catchC")
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1161
      case True
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1162
      note Catch = this
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1163
      with Try have hyp_c2: "PROP ?EqEval (new_xcpt_var vn s2) s3 (In1r c2) \<diamondsuit>"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1164
	by auto
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1165
      show ?thesis
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1166
      proof (cases "normal s1")
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1167
	case True
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1168
	with sxalloc wf 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1169
	have eq_s2_s1: "s2=s1"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1170
	  by (auto dest: sxalloc_type_sound split: option.splits)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1171
	with True 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1172
	have "\<not>  G,s2\<turnstile>catch catchC"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1173
	  by (simp add: catch_def)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1174
	with Catch show ?thesis 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1175
	  by (contradiction)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1176
      next 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1177
	case False
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1178
	with sxalloc wf
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1179
	obtain a 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1180
	  where xcpt_s2: "abrupt s2 = Some (Xcpt (Loc a))"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1181
	  by (auto dest!: sxalloc_type_sound split: option.splits)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1182
	with Catch
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1183
	have "G\<turnstile>obj_ty (the (globs (store s2) (Heap a)))\<preceq>Class catchC"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1184
	  by (cases s2) simp
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1185
	with xcpt_s2 conf_s2 wf 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1186
	have "new_xcpt_var vn s2\<Colon>\<preceq>(G, L(VName vn\<mapsto>Class catchC))"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1187
	  by (auto dest: Try_lemma)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1188
	(* FIXME extract lemma for this conformance, also usefull for
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1189
               eval_type_sound and evaln_eval *)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1190
	from this wt_c2
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1191
	obtain m where "G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>m\<rightarrow> s3"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1192
	  by (auto dest: hyp_c2)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1193
	with True that
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1194
	show ?thesis
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1195
	  by simp
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1196
      qed
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1197
    next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1198
      case False
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1199
      with Try
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1200
      have "s3=s2"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1201
	by simp
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1202
      with False and that
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1203
      show ?thesis
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1204
	by simp
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1205
    qed
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1206
    ultimately
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1207
    have "G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(catchC vn) c2\<midarrow>max n1 n2\<rightarrow> s3"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1208
      by (auto intro!: evaln.Try le_maxI1 le_maxI2)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1209
    then show ?case ..
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1210
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1211
    case (Fin c1 c2 s0 s1 s2 x1 L accC T)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1212
    with wf obtain n1 n2 where 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1213
      "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> (x1, s1)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1214
      "G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1215
      by (blast elim!: wt_elim_cases 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1216
	         dest: eval_type_sound intro: conforms_NormI)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1217
    then have 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1218
     "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>max n1 n2\<rightarrow> abupd (abrupt_if (x1 \<noteq> None) x1) s2"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1219
      by (blast intro: evaln.Fin dest: evaln_max2)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1220
    then show ?case ..
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1221
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1222
    case (Init C c s0 s1 s2 s3 L accC T)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1223
    have     cls: "the (class G C) = c" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1224
    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1225
    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Init C)\<Colon>T" .
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1226
    with cls
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1227
    have cls_C: "class G C = Some c"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1228
      by - (erule wt_elim_cases,auto)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1229
    obtain n where
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1230
      "if inited C (globs s0) then s3 = Norm s0
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1231
       else (G\<turnstile>Norm (init_class_obj G C s0)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1232
	      \<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n\<rightarrow> s1 \<and>
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1233
	           G\<turnstile>set_lvars empty s1 \<midarrow>init c\<midarrow>n\<rightarrow> s2 \<and> 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1234
                   s3 = restore_lvars s1 s2)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1235
    proof (cases "inited C (globs s0)")
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1236
      case True
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1237
      with Init have "s3 = Norm s0"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1238
	by simp
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1239
      with True that show ?thesis 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1240
	by simp
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1241
    next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1242
      case False
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1243
      with Init
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1244
      obtain 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1245
	hyp_init_super: 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1246
        "PROP ?EqEval (Norm ((init_class_obj G C) s0)) s1
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1247
	               (In1r (if C = Object then Skip else Init (super c))) \<diamondsuit>"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1248
	and 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1249
        hyp_init_c:
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1250
	   "PROP ?EqEval ((set_lvars empty) s1) s2 (In1r (init c)) \<diamondsuit>" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1251
	s3: "s3 = (set_lvars (locals (store s1))) s2" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1252
	eval_init_super: 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1253
	"G\<turnstile>Norm ((init_class_obj G C) s0) 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1254
           \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1255
	by (simp only: if_False)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1256
      from conf_s0 wf cls_C False
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1257
      have conf_s0': "(Norm ((init_class_obj G C) s0))\<Colon>\<preceq>(G, L)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1258
	by (auto dest: conforms_init_class_obj)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1259
      moreover
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1260
      from wf cls_C 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1261
      have wt_init_super:
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1262
           "\<lparr>prg = G, cls = accC, lcl = L\<rparr>
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1263
                  \<turnstile>(if C = Object then Skip else Init (super c))\<Colon>\<surd>"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1264
	by (cases "C=Object")
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1265
           (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1266
      ultimately
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1267
      obtain m1 where  
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1268
	   "G\<turnstile>Norm ((init_class_obj G C) s0) 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1269
            \<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>m1\<rightarrow> s1"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1270
	by (rules dest: hyp_init_super)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1271
      moreover
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1272
      from eval_init_super conf_s0' wt_init_super wf
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1273
      have "s1\<Colon>\<preceq>(G, L)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1274
	by (rules dest: eval_type_sound)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1275
      then
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1276
      have "(set_lvars empty) s1\<Colon>\<preceq>(G, empty)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset
  1277
	by (cases s1) (auto dest: conforms_set_locals )
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12919
diff changeset