--- a/src/HOL/Bali/Evaln.thy Mon Dec 11 12:28:16 2006 +0100
+++ b/src/HOL/Bali/Evaln.thy Mon Dec 11 16:06:14 2006 +0100
@@ -28,68 +28,40 @@
for welltyped, and definitely assigned terms.
*}
-consts
-
- evaln :: "prog \<Rightarrow> (state \<times> term \<times> nat \<times> vals \<times> state) set"
-
-syntax
-
- evaln :: "[prog, state, term, nat, vals * state] => bool"
- ("_|-_ -_>-_-> _" [61,61,80, 61,61] 60)
- evarn :: "[prog, state, var , vvar , nat, state] => bool"
- ("_|-_ -_=>_-_-> _" [61,61,90,61,61,61] 60)
- eval_n:: "[prog, state, expr , val , nat, state] => bool"
- ("_|-_ -_->_-_-> _" [61,61,80,61,61,61] 60)
- evalsn:: "[prog, state, expr list, val list, nat, state] => bool"
- ("_|-_ -_#>_-_-> _" [61,61,61,61,61,61] 60)
- execn :: "[prog, state, stmt , nat, state] => bool"
- ("_|-_ -_-_-> _" [61,61,65, 61,61] 60)
-
-syntax (xsymbols)
+inductive2
+ evaln :: "[prog, state, term, nat, vals, state] \<Rightarrow> bool"
+ ("_\<turnstile>_ \<midarrow>_\<succ>\<midarrow>_\<rightarrow> '(_, _')" [61,61,80,61,0,0] 60)
+ and evarn :: "[prog, state, var, vvar, nat, state] \<Rightarrow> bool"
+ ("_\<turnstile>_ \<midarrow>_=\<succ>_\<midarrow>_\<rightarrow> _" [61,61,90,61,61,61] 60)
+ and eval_n:: "[prog, state, expr, val, nat, state] \<Rightarrow> bool"
+ ("_\<turnstile>_ \<midarrow>_-\<succ>_\<midarrow>_\<rightarrow> _" [61,61,80,61,61,61] 60)
+ and evalsn :: "[prog, state, expr list, val list, nat, state] \<Rightarrow> bool"
+ ("_\<turnstile>_ \<midarrow>_\<doteq>\<succ>_\<midarrow>_\<rightarrow> _" [61,61,61,61,61,61] 60)
+ and execn :: "[prog, state, stmt, nat, state] \<Rightarrow> bool"
+ ("_\<turnstile>_ \<midarrow>_\<midarrow>_\<rightarrow> _" [61,61,65, 61,61] 60)
+ for G :: prog
+where
- evaln :: "[prog, state, term, nat, vals \<times> state] \<Rightarrow> bool"
- ("_\<turnstile>_ \<midarrow>_\<succ>\<midarrow>_\<rightarrow> _" [61,61,80, 61,61] 60)
- evarn :: "[prog, state, var , vvar , nat, state] \<Rightarrow> bool"
- ("_\<turnstile>_ \<midarrow>_=\<succ>_\<midarrow>_\<rightarrow> _" [61,61,90,61,61,61] 60)
- eval_n:: "[prog, state, expr , val , nat, state] \<Rightarrow> bool"
- ("_\<turnstile>_ \<midarrow>_-\<succ>_\<midarrow>_\<rightarrow> _" [61,61,80,61,61,61] 60)
- evalsn:: "[prog, state, expr list, val list, nat, state] \<Rightarrow> bool"
- ("_\<turnstile>_ \<midarrow>_\<doteq>\<succ>_\<midarrow>_\<rightarrow> _" [61,61,61,61,61,61] 60)
- execn :: "[prog, state, stmt , nat, state] \<Rightarrow> bool"
- ("_\<turnstile>_ \<midarrow>_\<midarrow>_\<rightarrow> _" [61,61,65, 61,61] 60)
-
-translations
-
- "G\<turnstile>s \<midarrow>t \<succ>\<midarrow>n\<rightarrow> w___s' " == "(s,t,n,w___s') \<in> evaln G"
- "G\<turnstile>s \<midarrow>t \<succ>\<midarrow>n\<rightarrow> (w, s')" <= "(s,t,n,w, s') \<in> evaln G"
- "G\<turnstile>s \<midarrow>t \<succ>\<midarrow>n\<rightarrow> (w,x,s')" <= "(s,t,n,w,x,s') \<in> evaln G"
- "G\<turnstile>s \<midarrow>c \<midarrow>n\<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In1r c\<succ>\<midarrow>n\<rightarrow> (\<diamondsuit> ,x,s')"
- "G\<turnstile>s \<midarrow>c \<midarrow>n\<rightarrow> s' " == "G\<turnstile>s \<midarrow>In1r c\<succ>\<midarrow>n\<rightarrow> (\<diamondsuit> , s')"
- "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')"
- "G\<turnstile>s \<midarrow>e-\<succ>v \<midarrow>n\<rightarrow> s' " == "G\<turnstile>s \<midarrow>In1l e\<succ>\<midarrow>n\<rightarrow> (In1 v , s')"
- "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')"
- "G\<turnstile>s \<midarrow>e=\<succ>vf \<midarrow>n\<rightarrow> s' " == "G\<turnstile>s \<midarrow>In2 e\<succ>\<midarrow>n\<rightarrow> (In2 vf, s')"
- "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')"
- "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')"
-
-
-inductive "evaln G" intros
+ "G\<turnstile>s \<midarrow>c \<midarrow>n\<rightarrow> s' \<equiv> G\<turnstile>s \<midarrow>In1r c\<succ>\<midarrow>n\<rightarrow> (\<diamondsuit> , s')"
+| "G\<turnstile>s \<midarrow>e-\<succ>v \<midarrow>n\<rightarrow> s' \<equiv> G\<turnstile>s \<midarrow>In1l e\<succ>\<midarrow>n\<rightarrow> (In1 v , s')"
+| "G\<turnstile>s \<midarrow>e=\<succ>vf \<midarrow>n\<rightarrow> s' \<equiv> G\<turnstile>s \<midarrow>In2 e\<succ>\<midarrow>n\<rightarrow> (In2 vf, s')"
+| "G\<turnstile>s \<midarrow>e\<doteq>\<succ>v \<midarrow>n\<rightarrow> s' \<equiv> G\<turnstile>s \<midarrow>In3 e\<succ>\<midarrow>n\<rightarrow> (In3 v , s')"
--{* propagation of abrupt completion *}
- Abrupt: "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t,(Some xc,s))"
+| Abrupt: "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t,(Some xc,s))"
--{* evaluation of variables *}
- LVar: "G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
+| LVar: "G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
- FVar: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s2;
+| FVar: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s2;
(v,s2') = fvar statDeclC stat fn a s2;
s3 = check_field_access G accC statDeclC fn stat a s2'\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>n\<rightarrow> s3"
- 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;
+| 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;
(v,s2') = avar G i a s2\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<midarrow>n\<rightarrow> s2'"
@@ -98,46 +70,46 @@
--{* evaluation of expressions *}
- NewC: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1;
+| NewC: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1;
G\<turnstile> s1 \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s2\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<midarrow>n\<rightarrow> s2"
- 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;
+| 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;
G\<turnstile>abupd (check_neg i') s2 \<midarrow>halloc (Arr T (the_Intg i'))\<succ>a\<rightarrow> s3\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<midarrow>n\<rightarrow> s3"
- Cast: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1;
+| Cast: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1;
s2 = abupd (raise_if (\<not>G,snd s1\<turnstile>v fits T) ClassCast) s1\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>Cast T e-\<succ>v\<midarrow>n\<rightarrow> s2"
- Inst: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1;
+| Inst: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1;
b = (v\<noteq>Null \<and> G,store s1\<turnstile>v fits RefT T)\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<midarrow>n\<rightarrow> s1"
- Lit: "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
+| Lit: "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
- UnOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk>
+| UnOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk>
\<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>(eval_unop unop v)\<midarrow>n\<rightarrow> s1"
- BinOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n\<rightarrow> s1;
+| BinOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n\<rightarrow> s1;
G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then (In1l e2) else (In1r Skip))
\<succ>\<midarrow>n\<rightarrow> (In1 v2,s2)\<rbrakk>
\<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>n\<rightarrow> s2"
- Super: "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
+| Super: "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
- Acc: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
+| Acc: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<midarrow>n\<rightarrow> s1"
- Ass: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w,f)\<midarrow>n\<rightarrow> s1;
+| Ass: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w,f)\<midarrow>n\<rightarrow> s1;
G\<turnstile> s1 \<midarrow>e-\<succ>v \<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>va:=e-\<succ>v\<midarrow>n\<rightarrow> assign f v s2"
- Cond: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n\<rightarrow> s1;
+| Cond: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e0-\<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>
G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<midarrow>n\<rightarrow> s2"
- Call:
+| Call:
"\<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;
D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>;
s3=init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs s2;
@@ -147,10 +119,10 @@
\<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}args)-\<succ>v\<midarrow>n\<rightarrow> (restore_lvars s2 s4)"
- Methd:"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
+| Methd:"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
- Body: "\<lbrakk>G\<turnstile>Norm s0\<midarrow>Init D\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2;
+| Body: "\<lbrakk>G\<turnstile>Norm s0\<midarrow>Init D\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2;
s3 = (if (\<exists> l. abrupt s2 = Some (Jump (Break l)) \<or>
abrupt s2 = Some (Jump (Cont l)))
then abupd (\<lambda> x. Some (Error CrossMethodJump)) s2
@@ -160,57 +132,57 @@
--{* evaluation of expression lists *}
- Nil:
+| Nil:
"G\<turnstile>Norm s0 \<midarrow>[]\<doteq>\<succ>[]\<midarrow>n\<rightarrow> Norm s0"
- Cons: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e -\<succ> v \<midarrow>n\<rightarrow> s1;
+| Cons: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e -\<succ> v \<midarrow>n\<rightarrow> s1;
G\<turnstile> s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<midarrow>n\<rightarrow> s2"
--{* execution of statements *}
- Skip: "G\<turnstile>Norm s \<midarrow>Skip\<midarrow>n\<rightarrow> Norm s"
+| Skip: "G\<turnstile>Norm s \<midarrow>Skip\<midarrow>n\<rightarrow> Norm s"
- Expr: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
+| Expr: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1"
- Lab: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
+| Lab: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb l) s1"
- Comp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<midarrow>n\<rightarrow> s1;
+| Comp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<midarrow>n\<rightarrow> s1;
G\<turnstile> s1 \<midarrow>c2 \<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>c1;; c2\<midarrow>n\<rightarrow> s2"
- If: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1;
+| If: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1;
G\<turnstile> s1\<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2 \<midarrow>n\<rightarrow> s2"
- Loop: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1;
+| Loop: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1;
if the_Bool b
then (G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2 \<and>
G\<turnstile>(abupd (absorb (Cont l)) s2) \<midarrow>l\<bullet> While(e) c\<midarrow>n\<rightarrow> s3)
else s3 = s1\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>n\<rightarrow> s3"
- Jmp: "G\<turnstile>Norm s \<midarrow>Jmp j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
+| Jmp: "G\<turnstile>Norm s \<midarrow>Jmp j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
- Throw:"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
+| Throw:"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> abupd (throw a') s1"
- Try: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2;
+| Try: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2;
if G,s2\<turnstile>catch tn then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n\<rightarrow> s3 else s3 = s2\<rbrakk>
\<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(tn vn) c2\<midarrow>n\<rightarrow> s3"
- Fin: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n\<rightarrow> (x1,s1);
+| Fin: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n\<rightarrow> (x1,s1);
G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n\<rightarrow> s2;
s3=(if (\<exists> err. x1=Some (Error err))
then (x1,s1)
else abupd (abrupt_if (x1\<noteq>None) x1) s2)\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>n\<rightarrow> s3"
- Init: "\<lbrakk>the (class G C) = c;
+| Init: "\<lbrakk>the (class G C) = c;
if inited C (globs s0) then s3 = Norm s0
else (G\<turnstile>Norm (init_class_obj G C s0)
\<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n\<rightarrow> s1 \<and>
@@ -229,41 +201,41 @@
ML_setup {*
change_simpset (fn ss => ss delloop "split_all_tac");
*}
-inductive_cases evaln_cases: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> vs'"
+inductive_cases2 evaln_cases: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v, s')"
-inductive_cases evaln_elim_cases:
- "G\<turnstile>(Some xc, s) \<midarrow>t \<succ>\<midarrow>n\<rightarrow> vs'"
- "G\<turnstile>Norm s \<midarrow>In1r Skip \<succ>\<midarrow>n\<rightarrow> xs'"
- "G\<turnstile>Norm s \<midarrow>In1r (Jmp j) \<succ>\<midarrow>n\<rightarrow> xs'"
- "G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> c) \<succ>\<midarrow>n\<rightarrow> xs'"
- "G\<turnstile>Norm s \<midarrow>In3 ([]) \<succ>\<midarrow>n\<rightarrow> vs'"
- "G\<turnstile>Norm s \<midarrow>In3 (e#es) \<succ>\<midarrow>n\<rightarrow> vs'"
- "G\<turnstile>Norm s \<midarrow>In1l (Lit w) \<succ>\<midarrow>n\<rightarrow> vs'"
- "G\<turnstile>Norm s \<midarrow>In1l (UnOp unop e) \<succ>\<midarrow>n\<rightarrow> vs'"
- "G\<turnstile>Norm s \<midarrow>In1l (BinOp binop e1 e2) \<succ>\<midarrow>n\<rightarrow> vs'"
- "G\<turnstile>Norm s \<midarrow>In2 (LVar vn) \<succ>\<midarrow>n\<rightarrow> vs'"
- "G\<turnstile>Norm s \<midarrow>In1l (Cast T e) \<succ>\<midarrow>n\<rightarrow> vs'"
- "G\<turnstile>Norm s \<midarrow>In1l (e InstOf T) \<succ>\<midarrow>n\<rightarrow> vs'"
- "G\<turnstile>Norm s \<midarrow>In1l (Super) \<succ>\<midarrow>n\<rightarrow> vs'"
- "G\<turnstile>Norm s \<midarrow>In1l (Acc va) \<succ>\<midarrow>n\<rightarrow> vs'"
- "G\<turnstile>Norm s \<midarrow>In1r (Expr e) \<succ>\<midarrow>n\<rightarrow> xs'"
- "G\<turnstile>Norm s \<midarrow>In1r (c1;; c2) \<succ>\<midarrow>n\<rightarrow> xs'"
- "G\<turnstile>Norm s \<midarrow>In1l (Methd C sig) \<succ>\<midarrow>n\<rightarrow> xs'"
- "G\<turnstile>Norm s \<midarrow>In1l (Body D c) \<succ>\<midarrow>n\<rightarrow> xs'"
- "G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2) \<succ>\<midarrow>n\<rightarrow> vs'"
- "G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2) \<succ>\<midarrow>n\<rightarrow> xs'"
- "G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> While(e) c) \<succ>\<midarrow>n\<rightarrow> xs'"
- "G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2) \<succ>\<midarrow>n\<rightarrow> xs'"
- "G\<turnstile>Norm s \<midarrow>In1r (Throw e) \<succ>\<midarrow>n\<rightarrow> xs'"
- "G\<turnstile>Norm s \<midarrow>In1l (NewC C) \<succ>\<midarrow>n\<rightarrow> vs'"
- "G\<turnstile>Norm s \<midarrow>In1l (New T[e]) \<succ>\<midarrow>n\<rightarrow> vs'"
- "G\<turnstile>Norm s \<midarrow>In1l (Ass va e) \<succ>\<midarrow>n\<rightarrow> vs'"
- "G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2) \<succ>\<midarrow>n\<rightarrow> xs'"
- "G\<turnstile>Norm s \<midarrow>In2 ({accC,statDeclC,stat}e..fn) \<succ>\<midarrow>n\<rightarrow> vs'"
- "G\<turnstile>Norm s \<midarrow>In2 (e1.[e2]) \<succ>\<midarrow>n\<rightarrow> vs'"
- "G\<turnstile>Norm s \<midarrow>In1l ({accC,statT,mode}e\<cdot>mn({pT}p)) \<succ>\<midarrow>n\<rightarrow> vs'"
- "G\<turnstile>Norm s \<midarrow>In1r (Init C) \<succ>\<midarrow>n\<rightarrow> xs'"
- "G\<turnstile>Norm s \<midarrow>In1r (Init C) \<succ>\<midarrow>n\<rightarrow> xs'"
+inductive_cases2 evaln_elim_cases:
+ "G\<turnstile>(Some xc, s) \<midarrow>t \<succ>\<midarrow>n\<rightarrow> (v, s')"
+ "G\<turnstile>Norm s \<midarrow>In1r Skip \<succ>\<midarrow>n\<rightarrow> (x, s')"
+ "G\<turnstile>Norm s \<midarrow>In1r (Jmp j) \<succ>\<midarrow>n\<rightarrow> (x, s')"
+ "G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> c) \<succ>\<midarrow>n\<rightarrow> (x, s')"
+ "G\<turnstile>Norm s \<midarrow>In3 ([]) \<succ>\<midarrow>n\<rightarrow> (v, s')"
+ "G\<turnstile>Norm s \<midarrow>In3 (e#es) \<succ>\<midarrow>n\<rightarrow> (v, s')"
+ "G\<turnstile>Norm s \<midarrow>In1l (Lit w) \<succ>\<midarrow>n\<rightarrow> (v, s')"
+ "G\<turnstile>Norm s \<midarrow>In1l (UnOp unop e) \<succ>\<midarrow>n\<rightarrow> (v, s')"
+ "G\<turnstile>Norm s \<midarrow>In1l (BinOp binop e1 e2) \<succ>\<midarrow>n\<rightarrow> (v, s')"
+ "G\<turnstile>Norm s \<midarrow>In2 (LVar vn) \<succ>\<midarrow>n\<rightarrow> (v, s')"
+ "G\<turnstile>Norm s \<midarrow>In1l (Cast T e) \<succ>\<midarrow>n\<rightarrow> (v, s')"
+ "G\<turnstile>Norm s \<midarrow>In1l (e InstOf T) \<succ>\<midarrow>n\<rightarrow> (v, s')"
+ "G\<turnstile>Norm s \<midarrow>In1l (Super) \<succ>\<midarrow>n\<rightarrow> (v, s')"
+ "G\<turnstile>Norm s \<midarrow>In1l (Acc va) \<succ>\<midarrow>n\<rightarrow> (v, s')"
+ "G\<turnstile>Norm s \<midarrow>In1r (Expr e) \<succ>\<midarrow>n\<rightarrow> (x, s')"
+ "G\<turnstile>Norm s \<midarrow>In1r (c1;; c2) \<succ>\<midarrow>n\<rightarrow> (x, s')"
+ "G\<turnstile>Norm s \<midarrow>In1l (Methd C sig) \<succ>\<midarrow>n\<rightarrow> (x, s')"
+ "G\<turnstile>Norm s \<midarrow>In1l (Body D c) \<succ>\<midarrow>n\<rightarrow> (x, s')"
+ "G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2) \<succ>\<midarrow>n\<rightarrow> (v, s')"
+ "G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2) \<succ>\<midarrow>n\<rightarrow> (x, s')"
+ "G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> While(e) c) \<succ>\<midarrow>n\<rightarrow> (x, s')"
+ "G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2) \<succ>\<midarrow>n\<rightarrow> (x, s')"
+ "G\<turnstile>Norm s \<midarrow>In1r (Throw e) \<succ>\<midarrow>n\<rightarrow> (x, s')"
+ "G\<turnstile>Norm s \<midarrow>In1l (NewC C) \<succ>\<midarrow>n\<rightarrow> (v, s')"
+ "G\<turnstile>Norm s \<midarrow>In1l (New T[e]) \<succ>\<midarrow>n\<rightarrow> (v, s')"
+ "G\<turnstile>Norm s \<midarrow>In1l (Ass va e) \<succ>\<midarrow>n\<rightarrow> (v, s')"
+ "G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2) \<succ>\<midarrow>n\<rightarrow> (x, s')"
+ "G\<turnstile>Norm s \<midarrow>In2 ({accC,statDeclC,stat}e..fn) \<succ>\<midarrow>n\<rightarrow> (v, s')"
+ "G\<turnstile>Norm s \<midarrow>In2 (e1.[e2]) \<succ>\<midarrow>n\<rightarrow> (v, s')"
+ "G\<turnstile>Norm s \<midarrow>In1l ({accC,statT,mode}e\<cdot>mn({pT}p)) \<succ>\<midarrow>n\<rightarrow> (v, s')"
+ "G\<turnstile>Norm s \<midarrow>In1r (Init C) \<succ>\<midarrow>n\<rightarrow> (x, s')"
+ "G\<turnstile>Norm s \<midarrow>In1r (Init C) \<succ>\<midarrow>n\<rightarrow> (x, s')"
declare split_if [split] split_if_asm [split]
option.split [split] option.split_asm [split]
@@ -288,25 +260,32 @@
(injection @{term In1} into generalised values @{term vals}).
*}
+lemma evaln_expr_eq: "G\<turnstile>s \<midarrow>In1l t\<succ>\<midarrow>n\<rightarrow> (w, s') = (\<exists>v. w=In1 v \<and> G\<turnstile>s \<midarrow>t-\<succ>v \<midarrow>n\<rightarrow> s')"
+ by (auto, frule evaln_Inj_elim, auto)
+
+lemma evaln_var_eq: "G\<turnstile>s \<midarrow>In2 t\<succ>\<midarrow>n\<rightarrow> (w, s') = (\<exists>vf. w=In2 vf \<and> G\<turnstile>s \<midarrow>t=\<succ>vf\<midarrow>n\<rightarrow> s')"
+ by (auto, frule evaln_Inj_elim, auto)
+
+lemma evaln_exprs_eq: "G\<turnstile>s \<midarrow>In3 t\<succ>\<midarrow>n\<rightarrow> (w, s') = (\<exists>vs. w=In3 vs \<and> G\<turnstile>s \<midarrow>t\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s')"
+ by (auto, frule evaln_Inj_elim, auto)
+
+lemma evaln_stmt_eq: "G\<turnstile>s \<midarrow>In1r t\<succ>\<midarrow>n\<rightarrow> (w, s') = (w=\<diamondsuit> \<and> G\<turnstile>s \<midarrow>t \<midarrow>n\<rightarrow> s')"
+ by (auto, frule evaln_Inj_elim, auto, frule evaln_Inj_elim, auto)
+
ML_setup {*
-fun enf nam inj rhs =
+fun enf name lhs =
let
- val name = "evaln_" ^ nam ^ "_eq"
- val lhs = "G\<turnstile>s \<midarrow>" ^ inj ^ " t\<succ>\<midarrow>n\<rightarrow> (w, s')"
- val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")")
- (K [Auto_tac, ALLGOALS (ftac (thm "evaln_Inj_elim")) THEN Auto_tac])
fun is_Inj (Const (inj,_) $ _) = true
| is_Inj _ = false
- fun pred (_ $ (Const ("Pair",_) $ _ $ (Const ("Pair", _) $ _ $
- (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ x $ _ )))) $ _ ) = is_Inj x
+ fun pred (_ $ _ $ _ $ _ $ _ $ x $ _) = is_Inj x
in
cond_simproc name lhs pred (thm name)
end;
-val evaln_expr_proc = enf "expr" "In1l" "\<exists>v. w=In1 v \<and> G\<turnstile>s \<midarrow>t-\<succ>v \<midarrow>n\<rightarrow> s'";
-val evaln_var_proc = enf "var" "In2" "\<exists>vf. w=In2 vf \<and> G\<turnstile>s \<midarrow>t=\<succ>vf\<midarrow>n\<rightarrow> s'";
-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'";
-val evaln_stmt_proc = enf "stmt" "In1r" " w=\<diamondsuit> \<and> G\<turnstile>s \<midarrow>t \<midarrow>n\<rightarrow> s'";
+val evaln_expr_proc = enf "evaln_expr_eq" "G\<turnstile>s \<midarrow>In1l t\<succ>\<midarrow>n\<rightarrow> (w, s')";
+val evaln_var_proc = enf "evaln_var_eq" "G\<turnstile>s \<midarrow>In2 t\<succ>\<midarrow>n\<rightarrow> (w, s')";
+val evaln_exprs_proc = enf "evaln_exprs_eq" "G\<turnstile>s \<midarrow>In3 t\<succ>\<midarrow>n\<rightarrow> (w, s')";
+val evaln_stmt_proc = enf "evaln_stmt_eq" "G\<turnstile>s \<midarrow>In1r t\<succ>\<midarrow>n\<rightarrow> (w, s')";
Addsimprocs [evaln_expr_proc,evaln_var_proc,evaln_exprs_proc,evaln_stmt_proc];
bind_thms ("evaln_AbruptIs", sum3_instantiate (thm "evaln.Abrupt"))
@@ -319,9 +298,7 @@
assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
normal: "normal s" and
callee: "t=In1l (Callee l e)"
- then have "False"
- proof (induct)
- qed (auto)
+ then have "False" by induct auto
}
then show ?thesis
by (cases s') fastsimp
@@ -333,9 +310,7 @@
assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
normal: "normal s" and
callee: "t=In1l (InsInitE c e)"
- then have "False"
- proof (induct)
- qed (auto)
+ then have "False" by induct auto
}
then show ?thesis
by (cases s') fastsimp
@@ -347,9 +322,7 @@
assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
normal: "normal s" and
callee: "t=In2 (InsInitV c w)"
- then have "False"
- proof (induct)
- qed (auto)
+ then have "False" by induct auto
}
then show ?thesis
by (cases s') fastsimp
@@ -361,9 +334,7 @@
assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
normal: "normal s" and
callee: "t=In1r (FinA a c)"
- then have "False"
- proof (induct)
- qed (auto)
+ then have "False" by induct auto
}
then show ?thesis
by (cases s') fastsimp
@@ -385,9 +356,7 @@
local
fun is_Some (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _) =true
| is_Some _ = false
- fun pred (_ $ (Const ("Pair",_) $
- _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
- (Const ("Pair", _) $ _ $ x)))) $ _ ) = is_Some x
+ fun pred (_ $ _ $ _ $ _ $ _ $ _ $ x) = is_Some x
in
val evaln_abrupt_proc =
cond_simproc "evaln_abrupt" "G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s')" pred (thm "evaln_abrupt")
@@ -440,7 +409,7 @@
shows "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
using evaln
proof (induct)
- case (Loop b c e l n s0 s1 s2 s3)
+ case (Loop s0 e n b s1 c s2 l s3)
have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1".
moreover
have "if the_Bool b
@@ -450,7 +419,7 @@
using Loop.hyps by simp
ultimately show ?case by (rule eval.Loop)
next
- case (Try c1 c2 n s0 s1 s2 s3 C vn)
+ case (Try s0 c1 n s1 s2 C vn c2 s3)
have "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1".
moreover
have "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2".
@@ -459,7 +428,7 @@
using Try.hyps by simp
ultimately show ?case by (rule eval.Try)
next
- case (Init C c n s0 s1 s2 s3)
+ case (Init C c s0 s3 n s1 s2)
have "the (class G C) = c".
moreover
have "if inited C (globs s0)
@@ -478,8 +447,7 @@
done
lemma evaln_nonstrict [rule_format (no_asm), elim]:
- "\<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"
-apply (simp (no_asm_simp) only: split_tupled_all)
+ "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w, s') \<Longrightarrow> \<forall>m. n\<le>m \<longrightarrow> G\<turnstile>s \<midarrow>t\<succ>\<midarrow>m\<rightarrow> (w, s')"
apply (erule evaln.induct)
apply (tactic {* ALLGOALS (EVERY'[strip_tac, TRY o etac (thm "Suc_le_D_lemma"),
REPEAT o smp_tac 1,
@@ -490,30 +458,30 @@
lemmas evaln_nonstrict_Suc = evaln_nonstrict [OF _ le_refl [THEN le_SucI]]
-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>
- 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"
+lemma evaln_max2: "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> (w1, s1'); G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> (w2, s2')\<rbrakk> \<Longrightarrow>
+ G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max n1 n2\<rightarrow> (w1, s1') \<and> G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max n1 n2\<rightarrow> (w2, s2')"
by (fast intro: le_maxI1 le_maxI2)
corollary evaln_max2E [consumes 2]:
- "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> ws1; G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> ws2;
- \<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max n1 n2\<rightarrow> ws1;G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max n1 n2\<rightarrow> ws2 \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
+ "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> (w1, s1'); G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> (w2, s2');
+ \<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max n1 n2\<rightarrow> (w1, s1');G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max n1 n2\<rightarrow> (w2, s2') \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
by (drule (1) evaln_max2) simp
lemma evaln_max3:
-"\<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>
- G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws1 \<and>
- G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws2 \<and>
- G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws3"
+"\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> (w1, s1'); G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> (w2, s2'); G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>n3\<rightarrow> (w3, s3')\<rbrakk> \<Longrightarrow>
+ G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w1, s1') \<and>
+ G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w2, s2') \<and>
+ G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w3, s3')"
apply (drule (1) evaln_max2, erule thin_rl)
apply (fast intro!: le_maxI1 le_maxI2)
done
corollary evaln_max3E:
-"\<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;
- \<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws1;
- G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws2;
- G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws3
+"\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> (w1, s1'); G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> (w2, s2'); G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>n3\<rightarrow> (w3, s3');
+ \<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w1, s1');
+ G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w2, s2');
+ G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w3, s3')
\<rbrakk> \<Longrightarrow> P
\<rbrakk> \<Longrightarrow> P"
by (drule (2) evaln_max3) simp
@@ -551,16 +519,16 @@
shows "\<exists>n. G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)"
using eval
proof (induct)
- case (Abrupt s t xc)
+ case (Abrupt xc s t)
obtain n where
- "G\<turnstile>(Some xc, s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t, Some xc, s)"
+ "G\<turnstile>(Some xc, s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t, (Some xc, s))"
by (iprover intro: evaln.Abrupt)
then show ?case ..
next
case Skip
show ?case by (blast intro: evaln.Skip)
next
- case (Expr e s0 s1 v)
+ case (Expr s0 e v s1)
then obtain n where
"G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
by (iprover)
@@ -568,7 +536,7 @@
by (rule evaln.Expr)
then show ?case ..
next
- case (Lab c l s0 s1)
+ case (Lab s0 c s1 l)
then obtain n where
"G\<turnstile>Norm s0 \<midarrow>c\<midarrow>n\<rightarrow> s1"
by (iprover)
@@ -576,7 +544,7 @@
by (rule evaln.Lab)
then show ?case ..
next
- case (Comp c1 c2 s0 s1 s2)
+ case (Comp s0 c1 s1 c2 s2)
then obtain n1 n2 where
"G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
"G\<turnstile>s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
@@ -585,7 +553,7 @@
by (blast intro: evaln.Comp dest: evaln_max2 )
then show ?case ..
next
- case (If b c1 c2 e s0 s1 s2)
+ case (If s0 e b s1 c1 c2 s2)
then obtain n1 n2 where
"G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
"G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n2\<rightarrow> s2"
@@ -594,7 +562,7 @@
by (blast intro: evaln.If dest: evaln_max2)
then show ?case ..
next
- case (Loop b c e l s0 s1 s2 s3)
+ case (Loop s0 e b s1 c s2 l s3)
from Loop.hyps obtain n1 where
"G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
by (iprover)
@@ -614,12 +582,12 @@
done
then show ?case ..
next
- case (Jmp j s)
+ case (Jmp s j)
have "G\<turnstile>Norm s \<midarrow>Jmp j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
by (rule evaln.Jmp)
then show ?case ..
next
- case (Throw a e s0 s1)
+ case (Throw s0 e a s1)
then obtain n where
"G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s1"
by (iprover)
@@ -627,7 +595,7 @@
by (rule evaln.Throw)
then show ?case ..
next
- case (Try catchC c1 c2 s0 s1 s2 s3 vn)
+ case (Try s0 c1 s1 s2 catchC vn c2 s3)
from Try.hyps obtain n1 where
"G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
by (iprover)
@@ -642,7 +610,7 @@
by (auto intro!: evaln.Try le_maxI1 le_maxI2)
then show ?case ..
next
- case (Fin c1 c2 s0 s1 s2 s3 x1)
+ case (Fin s0 c1 x1 s1 c2 s2 s3)
from Fin obtain n1 n2 where
"G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> (x1, s1)"
"G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
@@ -657,7 +625,7 @@
by (blast intro: evaln.Fin dest: evaln_max2)
then show ?case ..
next
- case (Init C c s0 s1 s2 s3)
+ case (Init C c s0 s3 s1 s2)
have cls: "the (class G C) = c" .
moreover from Init.hyps obtain n where
"if inited C (globs s0) then s3 = Norm s0
@@ -670,7 +638,7 @@
by (rule evaln.Init)
then show ?case ..
next
- case (NewC C a s0 s1 s2)
+ case (NewC s0 C s1 a s2)
then obtain n where
"G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1"
by (iprover)
@@ -679,7 +647,7 @@
by (iprover intro: evaln.NewC)
then show ?case ..
next
- case (NewA T a e i s0 s1 s2 s3)
+ case (NewA s0 T s1 e i s2 a s3)
then obtain n1 n2 where
"G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<midarrow>n1\<rightarrow> s1"
"G\<turnstile>s1 \<midarrow>e-\<succ>i\<midarrow>n2\<rightarrow> s2"
@@ -691,7 +659,7 @@
by (blast intro: evaln.NewA dest: evaln_max2)
then show ?case ..
next
- case (Cast castT e s0 s1 s2 v)
+ case (Cast s0 e v s1 s2 castT)
then obtain n where
"G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
by (iprover)
@@ -702,7 +670,7 @@
by (rule evaln.Cast)
then show ?case ..
next
- case (Inst T b e s0 s1 v)
+ case (Inst s0 e v s1 b T)
then obtain n where
"G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
by (iprover)
@@ -718,7 +686,7 @@
by (rule evaln.Lit)
then show ?case ..
next
- case (UnOp e s0 s1 unop v )
+ case (UnOp s0 e v s1 unop)
then obtain n where
"G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
by (iprover)
@@ -726,7 +694,7 @@
by (rule evaln.UnOp)
then show ?case ..
next
- case (BinOp binop e1 e2 s0 s1 s2 v1 v2)
+ case (BinOp s0 e1 v1 s1 binop e2 v2 s2)
then obtain n1 n2 where
"G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n1\<rightarrow> s1"
"G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
@@ -742,7 +710,7 @@
by (rule evaln.Super)
then show ?case ..
next
- case (Acc f s0 s1 v va)
+ case (Acc s0 va v f s1)
then obtain n where
"G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<midarrow>n\<rightarrow> s1"
by (iprover)
@@ -751,7 +719,7 @@
by (rule evaln.Acc)
then show ?case ..
next
- case (Ass e f s0 s1 s2 v var w)
+ case (Ass s0 var w f s1 e v s2)
then obtain n1 n2 where
"G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, f)\<midarrow>n1\<rightarrow> s1"
"G\<turnstile>s1 \<midarrow>e-\<succ>v\<midarrow>n2\<rightarrow> s2"
@@ -761,7 +729,7 @@
by (blast intro: evaln.Ass dest: evaln_max2)
then show ?case ..
next
- case (Cond b e0 e1 e2 s0 s1 s2 v)
+ case (Cond s0 e0 b s1 e1 e2 v s2)
then obtain n1 n2 where
"G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n1\<rightarrow> s1"
"G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n2\<rightarrow> s2"
@@ -771,8 +739,7 @@
by (blast intro: evaln.Cond dest: evaln_max2)
then show ?case ..
next
- case (Call invDeclC a' accC' args e mn mode pTs' s0 s1 s2 s3 s3' s4 statT
- v vs)
+ case (Call s0 e a' s1 args vs s2 invDeclC mode statT mn pTs' s3 s3' accC' v s4)
then obtain n1 n2 where
"G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n1\<rightarrow> s1"
"G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"
@@ -795,7 +762,7 @@
by (auto intro!: evaln.Call le_maxI1 le_max3I1 le_max3I2)
thus ?case ..
next
- case (Methd D s0 s1 sig v )
+ case (Methd s0 D sig v s1)
then obtain n where
"G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n\<rightarrow> s1"
by iprover
@@ -803,7 +770,7 @@
by (rule evaln.Methd)
then show ?case ..
next
- case (Body D c s0 s1 s2 s3 )
+ case (Body s0 D s1 c s2 s3)
from Body.hyps obtain n1 n2 where
evaln_init: "G\<turnstile>Norm s0 \<midarrow>Init D\<midarrow>n1\<rightarrow> s1" and
evaln_c: "G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2"
@@ -826,7 +793,7 @@
by (iprover intro: evaln.LVar)
then show ?case ..
next
- case (FVar a accC e fn s0 s1 s2 s2' s3 stat statDeclC v)
+ case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC)
then obtain n1 n2 where
"G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n1\<rightarrow> s1"
"G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n2\<rightarrow> s2"
@@ -839,7 +806,7 @@
by (iprover intro: evaln.FVar dest: evaln_max2)
then show ?case ..
next
- case (AVar a e1 e2 i s0 s1 s2 s2' v )
+ case (AVar s0 e1 a s1 e2 i s2 v s2')
then obtain n1 n2 where
"G\<turnstile>Norm s0 \<midarrow>e1-\<succ>a\<midarrow>n1\<rightarrow> s1"
"G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n2\<rightarrow> s2"
@@ -854,7 +821,7 @@
case (Nil s0)
show ?case by (iprover intro: evaln.Nil)
next
- case (Cons e es s0 s1 s2 v vs)
+ case (Cons s0 e v s1 es vs s2)
then obtain n1 n2 where
"G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n1\<rightarrow> s1"
"G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"