Added conditional and (&&) and or (||).
(* Title: HOL/Bali/Trans.thy
ID: $Id$
Author: David von Oheimb
License: GPL (GNU GENERAL PUBLIC LICENSE)
Operational transition (small-step) semantics of the
execution of Java expressions and statements
PRELIMINARY!!!!!!!!
*)
theory Trans = Evaln:
constdefs groundVar:: "var \<Rightarrow> bool"
"groundVar v \<equiv> (case v of
LVar ln \<Rightarrow> True
| {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a
| e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i
| InsInitV c v \<Rightarrow> False)"
lemma groundVar_cases [consumes 1, case_names LVar FVar AVar]:
assumes ground: "groundVar v" and
LVar: "\<And> ln. \<lbrakk>v=LVar ln\<rbrakk> \<Longrightarrow> P" and
FVar: "\<And> accC statDeclC stat a fn.
\<lbrakk>v={accC,statDeclC,stat}(Lit a)..fn\<rbrakk> \<Longrightarrow> P" and
AVar: "\<And> a i. \<lbrakk>v=(Lit a).[Lit i]\<rbrakk> \<Longrightarrow> P"
shows "P"
proof -
from ground LVar FVar AVar
show ?thesis
apply (cases v)
apply (simp add: groundVar_def)
apply (simp add: groundVar_def,blast)
apply (simp add: groundVar_def,blast)
apply (simp add: groundVar_def)
done
qed
constdefs groundExprs:: "expr list \<Rightarrow> bool"
"groundExprs es \<equiv> list_all (\<lambda> e. \<exists> v. e=Lit v) es"
consts the_val:: "expr \<Rightarrow> val"
primrec
"the_val (Lit v) = v"
consts the_var:: "prog \<Rightarrow> state \<Rightarrow> var \<Rightarrow> (vvar \<times> state)"
primrec
"the_var G s (LVar ln) =(lvar ln (store s),s)"
the_var_FVar_def:
"the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s"
the_var_AVar_def:
"the_var G s(a.[i]) =avar G (the_val i) (the_val a) s"
lemma the_var_FVar_simp[simp]:
"the_var G s ({accC,statDeclC,stat}(Lit a)..fn) = fvar statDeclC stat fn a s"
by (simp)
declare the_var_FVar_def [simp del]
lemma the_var_AVar_simp:
"the_var G s ((Lit a).[Lit i]) = avar G i a s"
by (simp)
declare the_var_AVar_def [simp del]
consts
step :: "prog \<Rightarrow> ((term \<times> state) \<times> (term \<times> state)) set"
syntax (symbols)
step :: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>1 _"[61,82,82] 81)
stepn:: "[prog, term \<times> state,nat,term \<times> state] \<Rightarrow> bool"
("_\<turnstile>_ \<mapsto>_ _"[61,82,82] 81)
"step*":: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>* _"[61,82,82] 81)
Ref :: "loc \<Rightarrow> expr"
SKIP :: "expr"
translations
"G\<turnstile>p \<mapsto>1 p' " == "(p,p') \<in> step G"
"G\<turnstile>p \<mapsto>n p' " == "(p,p') \<in> (step G)^n"
"G\<turnstile>p \<mapsto>* p' " == "(p,p') \<in> (step G)\<^sup>*"
"Ref a" == "Lit (Addr a)"
"SKIP" == "Lit Unit"
inductive "step G" intros
(* evaluation of expression *)
(* cf. 15.5 *)
Abrupt: "\<lbrakk>\<forall>v. t \<noteq> \<langle>Lit v\<rangle>;
\<forall> t. t \<noteq> \<langle>l\<bullet> Skip\<rangle>;
\<forall> C vn c. t \<noteq> \<langle>Try Skip Catch(C vn) c\<rangle>;
\<forall> x c. t \<noteq> \<langle>Skip Finally c\<rangle> \<and> xc \<noteq> Xcpt x;
\<forall> a c. t \<noteq> \<langle>FinA a c\<rangle>\<rbrakk>
\<Longrightarrow>
G\<turnstile>(t,Some xc,s) \<mapsto>1 (\<langle>Lit arbitrary\<rangle>,Some xc,s)"
InsInitE: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>, s')\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>InsInitE c e\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE c' e\<rangle>, s')"
(* SeqE: "G\<turnstile>(\<langle>Seq Skip e\<rangle>,Norm s) \<mapsto>1 (\<langle>e\<rangle>, Norm s)" *)
(* Specialised rules to evaluate:
InsInitE Skip (NewC C), InisInitE Skip (NewA T[e]) *)
(* cf. 15.8.1 *)
NewC: "G\<turnstile>(\<langle>NewC C\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (Init C) (NewC C)\<rangle>, Norm s)"
NewCInited: "\<lbrakk>G\<turnstile> Norm s \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s'\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>InsInitE Skip (NewC C)\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>, s')"
(* Alternative when rule SeqE is present
NewCInited: "\<lbrakk>inited C (globs s);
G\<turnstile> Norm s \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s'\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>NewC C\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>, s')"
NewC:
"\<lbrakk>\<not> inited C (globs s)\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>NewC C\<rangle>,Norm s) \<mapsto>1 (\<langle>Seq (Init C) (NewC C)\<rangle>, Norm s)"
*)
(* cf. 15.9.1 *)
NewA:
"G\<turnstile>(\<langle>New T[e]\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (init_comp_ty T) (New T[e])\<rangle>,Norm s)"
InsInitNewAIdx:
"\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>, s')\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>InsInitE Skip (New T[e])\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE Skip (New T[e'])\<rangle>,s')"
InsInitNewA:
"\<lbrakk>G\<turnstile>abupd (check_neg i) (Norm s) \<midarrow>halloc (Arr T (the_Intg i))\<succ>a\<rightarrow> s' \<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>InsInitE Skip (New T[Lit i])\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>,s')"
(* cf. 15.15 *)
CastE:
"\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>Cast T e\<rangle>,None,s) \<mapsto>1 (\<langle>Cast T e'\<rangle>,s')"
Cast:
"\<lbrakk>s' = abupd (raise_if (\<not>G,s\<turnstile>v fits T) ClassCast) (Norm s)\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>Cast T (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
(* can be written without abupd, since we know Norm s *)
InstE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>e InstOf T\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')"
Inst: "\<lbrakk>b = (v\<noteq>Null \<and> G,s\<turnstile>v fits RefT T)\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>(Lit v) InstOf T\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (Bool b)\<rangle>,s')"
(* cf. 15.7.1 *)
(*Lit "G\<turnstile>(Lit v,None,s) \<mapsto>1 (Lit v,None,s)"*)
UnOpE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s') \<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>UnOp unop e\<rangle>,Norm s) \<mapsto>1 (\<langle>UnOp unop e'\<rangle>,s')"
UnOp: "G\<turnstile>(\<langle>UnOp unop (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (eval_unop unop v)\<rangle>,Norm s)"
BinOpE1: "\<lbrakk>G\<turnstile>(\<langle>e1\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'\<rangle>,s') \<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>BinOp binop e1 e2\<rangle>,Norm s) \<mapsto>1 (\<langle>BinOp binop e1' e2\<rangle>,s')"
BinOpE2: "\<lbrakk>need_second_arg binop v1; G\<turnstile>(\<langle>e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e2'\<rangle>,s') \<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>BinOp binop (Lit v1) e2\<rangle>,Norm s)
\<mapsto>1 (\<langle>BinOp binop (Lit v1) e2'\<rangle>,s')"
BinOpTerm: "\<lbrakk>\<not> need_second_arg binop v1\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>BinOp binop (Lit v1) e2\<rangle>,Norm s)
\<mapsto>1 (\<langle>Lit v1\<rangle>,Norm s)"
BinOp: "G\<turnstile>(\<langle>BinOp binop (Lit v1) (Lit v2)\<rangle>,Norm s)
\<mapsto>1 (\<langle>Lit (eval_binop binop v1 v2)\<rangle>,Norm s)"
(* Maybe its more convenient to add: need_second_arg as precondition to BinOp
to make the choice between BinOpTerm and BinOp deterministic *)
Super: "G\<turnstile>(\<langle>Super\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (val_this s)\<rangle>,Norm s)"
AccVA: "\<lbrakk>G\<turnstile>(\<langle>va\<rangle>,Norm s) \<mapsto>1 (\<langle>va'\<rangle>,s') \<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>Acc va\<rangle>,Norm s) \<mapsto>1 (\<langle>Acc va'\<rangle>,s')"
Acc: "\<lbrakk>groundVar va; ((v,vf),s') = the_var G (Norm s) va\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>Acc va\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
(*
AccLVar: "G\<turnstile>(\<langle>Acc (LVar vn)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (fst (lvar vn s))\<rangle>,Norm s)"
AccFVar: "\<lbrakk>((v,vf),s') = fvar statDeclC stat fn a (Norm s)\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>Acc ({accC,statDeclC,stat}(Lit a)..fn)\<rangle>,Norm s)
\<mapsto>1 (\<langle>Lit v\<rangle>,s')"
AccAVar: "\<lbrakk>((v,vf),s') = avar G i a (Norm s)\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>Acc ((Lit a).[Lit i])\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
*)
AssVA: "\<lbrakk>G\<turnstile>(\<langle>va\<rangle>,Norm s) \<mapsto>1 (\<langle>va'\<rangle>,s')\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>va:=e\<rangle>,Norm s) \<mapsto>1 (\<langle>va':=e\<rangle>,s')"
AssE: "\<lbrakk>groundVar va; G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>va:=e\<rangle>,Norm s) \<mapsto>1 (\<langle>va:=e'\<rangle>,s')"
Ass: "\<lbrakk>groundVar va; ((w,f),s') = the_var G (Norm s) va\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>va:=(Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,assign f v s')"
CondC: "\<lbrakk>G\<turnstile>(\<langle>e0\<rangle>,Norm s) \<mapsto>1 (\<langle>e0'\<rangle>,s')\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>e0? e1:e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e0'? e1:e2\<rangle>,s')"
Cond: "G\<turnstile>(\<langle>Lit b? e1:e2\<rangle>,Norm s) \<mapsto>1 (\<langle>if the_Bool b then e1 else e2\<rangle>,Norm s)"
CallTarget: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>{accC,statT,mode}e\<cdot>mn({pTs}args)\<rangle>,Norm s)
\<mapsto>1 (\<langle>{accC,statT,mode}e'\<cdot>mn({pTs}args)\<rangle>,s')"
CallArgs: "\<lbrakk>G\<turnstile>(\<langle>args\<rangle>,Norm s) \<mapsto>1 (\<langle>args'\<rangle>,s')\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args)\<rangle>,Norm s)
\<mapsto>1 (\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args')\<rangle>,s')"
Call: "\<lbrakk>groundExprs args; vs = map the_val args;
D = invocation_declclass G mode s a statT \<lparr>name=mn,parTs=pTs\<rparr>;
s'=init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs (Norm s)\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args)\<rangle>,Norm s)
\<mapsto>1 (\<langle>Callee (locals s) (Methd D \<lparr>name=mn,parTs=pTs\<rparr>)\<rangle>,s')"
Callee: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>Callee lcls_caller e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')"
CalleeRet: "G\<turnstile>(\<langle>Callee lcls_caller (Lit v)\<rangle>,Norm s)
\<mapsto>1 (\<langle>Lit v\<rangle>,(set_lvars lcls_caller (Norm s)))"
Methd: "G\<turnstile>(\<langle>Methd D sig\<rangle>,Norm s) \<mapsto>1 (\<langle>body G D sig\<rangle>,Norm s)"
Body: "G\<turnstile>(\<langle>Body D c\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (Init D) (Body D c)\<rangle>,Norm s)"
InsInitBody:
"\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>InsInitE Skip (Body D c)\<rangle>,Norm s) \<mapsto>1(\<langle>InsInitE Skip (Body D c')\<rangle>,s')"
InsInitBodyRet:
"G\<turnstile>(\<langle>InsInitE Skip (Body D Skip)\<rangle>,Norm s)
\<mapsto>1 (\<langle>Lit (the ((locals s) Result))\<rangle>,abupd (absorb Ret) (Norm s))"
(* LVar: "G\<turnstile>(LVar vn,Norm s)" is already evaluated *)
FVar: "\<lbrakk>\<not> inited statDeclC (globs s)\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>{accC,statDeclC,stat}e..fn\<rangle>,Norm s)
\<mapsto>1 (\<langle>InsInitV (Init statDeclC) ({accC,statDeclC,stat}e..fn)\<rangle>,Norm s)"
InsInitFVarE:
"\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>InsInitV Skip ({accC,statDeclC,stat}e..fn)\<rangle>,Norm s)
\<mapsto>1 (\<langle>InsInitV Skip ({accC,statDeclC,stat}e'..fn)\<rangle>,s')"
InsInitFVar:
"G\<turnstile>(\<langle>InsInitV Skip ({accC,statDeclC,stat}Lit a..fn)\<rangle>,Norm s)
\<mapsto>1 (\<langle>{accC,statDeclC,stat}Lit a..fn\<rangle>,Norm s)"
-- {* Notice, that we do not have literal values for @{text vars}.
The rules for accessing variables (@{text Acc}) and assigning to variables
(@{text Ass}), test this with the predicate @{text groundVar}. After
initialisation is done and the @{text FVar} is evaluated, we can't just
throw away the @{text InsInitFVar} term and return a literal value, as in the
cases of @{text New} or @{text NewC}. Instead we just return the evaluated
@{text FVar} and test for initialisation in the rule @{text FVar}.
*}
AVarE1: "\<lbrakk>G\<turnstile>(\<langle>e1\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'\<rangle>,s')\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>e1.[e2]\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'.[e2]\<rangle>,s')"
AVarE2: "G\<turnstile>(\<langle>e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e2'\<rangle>,s')
\<Longrightarrow>
G\<turnstile>(\<langle>Lit a.[e2]\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit a.[e2']\<rangle>,s')"
(* AVar: \<langle>(Lit a).[Lit i]\<rangle> is fully evaluated *)
(* evaluation of expression lists *)
-- {* @{text Nil} is fully evaluated *}
ConsHd: "\<lbrakk>G\<turnstile>(\<langle>e::expr\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>e#es\<rangle>,Norm s) \<mapsto>1 (\<langle>e'#es\<rangle>,s')"
ConsTl: "\<lbrakk>G\<turnstile>(\<langle>es\<rangle>,Norm s) \<mapsto>1 (\<langle>es'\<rangle>,s')\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>(Lit v)#es\<rangle>,Norm s) \<mapsto>1 (\<langle>(Lit v)#es'\<rangle>,s')"
(* execution of statements *)
(* cf. 14.5 *)
Skip: "G\<turnstile>(\<langle>Skip\<rangle>,Norm s) \<mapsto>1 (\<langle>SKIP\<rangle>,Norm s)"
ExprE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>Expr e\<rangle>,Norm s) \<mapsto>1 (\<langle>Expr e'\<rangle>,s')"
Expr: "G\<turnstile>(\<langle>Expr (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,Norm s)"
LabC: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>l\<bullet> c\<rangle>,Norm s) \<mapsto>1 (\<langle>l\<bullet> c'\<rangle>,s')"
Lab: "G\<turnstile>(\<langle>l\<bullet> Skip\<rangle>,s) \<mapsto>1 (\<langle>Skip\<rangle>, abupd (absorb l) s)"
(* cf. 14.2 *)
CompC1: "\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>c1;; c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c1';; c2\<rangle>,s')"
Comp: "G\<turnstile>(\<langle>Skip;; c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c2\<rangle>,Norm s)"
(* cf. 14.8.2 *)
IfE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle> ,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>If(e) s1 Else s2\<rangle>,Norm s) \<mapsto>1 (\<langle>If(e') s1 Else s2\<rangle>,s')"
If: "G\<turnstile>(\<langle>If(Lit v) s1 Else s2\<rangle>,Norm s)
\<mapsto>1 (\<langle>if the_Bool v then s1 else s2\<rangle>,Norm s)"
(* cf. 14.10, 14.10.1 *)
Loop: "G\<turnstile>(\<langle>l\<bullet> While(e) c\<rangle>,Norm s)
\<mapsto>1 (\<langle>If(e) (Cont l\<bullet>c;; l\<bullet> While(e) c) Else Skip\<rangle>,Norm s)"
Do: "G\<turnstile>(\<langle>Do j\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,(Some (Jump j), s))"
ThrowE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>Throw e\<rangle>,Norm s) \<mapsto>1 (\<langle>Throw e'\<rangle>,s')"
Throw: "G\<turnstile>(\<langle>Throw (Lit a)\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,abupd (throw a) (Norm s))"
TryC1: "\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>Try c1 Catch(C vn) c2\<rangle>, Norm s) \<mapsto>1 (\<langle>Try c1' Catch(C vn) c2\<rangle>,s')"
Try: "\<lbrakk>G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>Try Skip Catch(C vn) c2\<rangle>, s)
\<mapsto>1 (if G,s'\<turnstile>catch C then (\<langle>c2\<rangle>,new_xcpt_var vn s')
else (\<langle>Skip\<rangle>,s'))"
FinC1: "\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>c1 Finally c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c1' Finally c2\<rangle>,s')"
Fin: "G\<turnstile>(\<langle>Skip Finally c2\<rangle>,(a,s)) \<mapsto>1 (\<langle>FinA a c2\<rangle>,Norm s)"
FinAC: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>FinA a c\<rangle>,s) \<mapsto>1 (\<langle>FinA a c'\<rangle>,s')"
FinA: "G\<turnstile>(\<langle>FinA a Skip\<rangle>,s) \<mapsto>1 (\<langle>Skip\<rangle>,abupd (abrupt_if (a\<noteq>None) a) s)"
Init1: "\<lbrakk>inited C (globs s)\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>Init C\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,Norm s)"
Init: "\<lbrakk>the (class G C)=c; \<not> inited C (globs s)\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>Init C\<rangle>,Norm s)
\<mapsto>1 (\<langle>(if C = Object then Skip else (Init (super c)));;
Expr (Callee (locals s) (InsInitE (init c) SKIP))\<rangle>
,Norm (init_class_obj G C s))"
-- {* @{text InsInitE} is just used as trick to embed the statement
@{text "init c"} into an expression*}
InsInitESKIP:
"G\<turnstile>(\<langle>InsInitE Skip SKIP\<rangle>,Norm s) \<mapsto>1 (\<langle>SKIP\<rangle>,Norm s)"
(* Equivalenzen:
Bigstep zu Smallstep komplett.
Smallstep zu Bigstep, nur wenn nicht die Ausdrücke Callee, FinA ,\<dots>
*)
lemma rtrancl_imp_rel_pow: "p \<in> R^* \<Longrightarrow> \<exists>n. p \<in> R^n"
proof -
assume "p \<in> R\<^sup>*"
moreover obtain x y where p: "p = (x,y)" by (cases p)
ultimately have "(x,y) \<in> R\<^sup>*" by hypsubst
hence "\<exists>n. (x,y) \<in> R^n"
proof induct
fix a have "(a,a) \<in> R^0" by simp
thus "\<exists>n. (a,a) \<in> R ^ n" ..
next
fix a b c assume "\<exists>n. (a,b) \<in> R ^ n"
then obtain n where "(a,b) \<in> R^n" ..
moreover assume "(b,c) \<in> R"
ultimately have "(a,c) \<in> R^(Suc n)" by auto
thus "\<exists>n. (a,c) \<in> R^n" ..
qed
with p show ?thesis by hypsubst
qed
(*
lemma imp_eval_trans:
assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
shows trans: "G\<turnstile>(t,s0) \<mapsto>* (\<langle>Lit v\<rangle>,s1)"
*)
(* Jetzt muss man bei trans natürlich wieder unterscheiden: Stmt, Expr, Var!
Sowas blödes:
Am besten den Terminus ground auf Var,Stmt,Expr hochziehen und dann
the_vals definieren\<dots>
G\<turnstile>(t,s0) \<mapsto>* (t',s1) \<and> the_vals t' = v
*)
end