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