(* Title: HOL/Bali/Trans.thy ID: $Id: Trans.thy,v 1.10 2005/06/17 14:13:06 haftmann Exp $ Author: David von Oheimb and Norbert Schirmer Operational transition (small-step) semantics of the execution of Java expressions and statements PRELIMINARY!!!!!!!! *) theory Trans imports Evaln begin constdefs groundVar:: "var => bool" "groundVar v ≡ (case v of LVar ln => True | {accC,statDeclC,stat}e..fn => ∃ a. e=Lit a | e1.[e2] => ∃ a i. e1= Lit a ∧ e2 = Lit i | InsInitV c v => False)" lemma groundVar_cases [consumes 1, case_names LVar FVar AVar]: assumes ground: "groundVar v" and LVar: "!! ln. [|v=LVar ln|] ==> P" and FVar: "!! accC statDeclC stat a fn. [|v={accC,statDeclC,stat}(Lit a)..fn|] ==> P" and AVar: "!! a i. [|v=(Lit a).[Lit i]|] ==> 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 => bool" "groundExprs es ≡ list_all (λ e. ∃ v. e=Lit v) es" consts the_val:: "expr => val" primrec "the_val (Lit v) = v" consts the_var:: "prog => state => var => (vvar × 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 => ((term × state) × (term × state)) set" syntax (symbols) step :: "[prog,term × state,term × state] => bool" ("_\<turnstile>_ \<mapsto>1 _"[61,82,82] 81) stepn:: "[prog, term × state,nat,term × state] => bool" ("_\<turnstile>_ \<mapsto>_ _"[61,82,82] 81) "step*":: "[prog,term × state,term × state] => bool" ("_\<turnstile>_ \<mapsto>* _"[61,82,82] 81) Ref :: "loc => expr" SKIP :: "expr" translations "G\<turnstile>p \<mapsto>1 p' " == "(p,p') ∈ step G" "G\<turnstile>p \<mapsto>n p' " == "(p,p') ∈ (step G)^n" "G\<turnstile>p \<mapsto>* p' " == "(p,p') ∈ (step G)*" "Ref a" == "Lit (Addr a)" "SKIP" == "Lit Unit" inductive "step G" intros (* evaluation of expression *) (* cf. 15.5 *) Abrupt: "[|∀v. t ≠ 〈Lit v〉; ∀ t. t ≠ 〈l• Skip〉; ∀ C vn c. t ≠ 〈Try Skip Catch(C vn) c〉; ∀ x c. t ≠ 〈Skip Finally c〉 ∧ xc ≠ Xcpt x; ∀ a c. t ≠ 〈FinA a c〉|] ==> G\<turnstile>(t,Some xc,s) \<mapsto>1 (〈Lit arbitrary〉,Some xc,s)" InsInitE: "[|G\<turnstile>(〈c〉,Norm s) \<mapsto>1 (〈c'〉, s')|] ==> G\<turnstile>(〈InsInitE c e〉,Norm s) \<mapsto>1 (〈InsInitE c' e〉, s')" (* SeqE: "G\<turnstile>(〈Seq Skip e〉,Norm s) \<mapsto>1 (〈e〉, Norm s)" *) (* Specialised rules to evaluate: InsInitE Skip (NewC C), InisInitE Skip (NewA T[e]) *) (* cf. 15.8.1 *) NewC: "G\<turnstile>(〈NewC C〉,Norm s) \<mapsto>1 (〈InsInitE (Init C) (NewC C)〉, Norm s)" NewCInited: "[|G\<turnstile> Norm s \<midarrow>halloc (CInst C)\<succ>a-> s'|] ==> G\<turnstile>(〈InsInitE Skip (NewC C)〉,Norm s) \<mapsto>1 (〈Ref a〉, s')" (* Alternative when rule SeqE is present NewCInited: "[|inited C (globs s); G\<turnstile> Norm s \<midarrow>halloc (CInst C)\<succ>a-> s'|] ==> G\<turnstile>(〈NewC C〉,Norm s) \<mapsto>1 (〈Ref a〉, s')" NewC: "[|¬ inited C (globs s)|] ==> G\<turnstile>(〈NewC C〉,Norm s) \<mapsto>1 (〈Seq (Init C) (NewC C)〉, Norm s)" *) (* cf. 15.9.1 *) NewA: "G\<turnstile>(〈New T[e]〉,Norm s) \<mapsto>1 (〈InsInitE (init_comp_ty T) (New T[e])〉,Norm s)" InsInitNewAIdx: "[|G\<turnstile>(〈e〉,Norm s) \<mapsto>1 (〈e'〉, s')|] ==> G\<turnstile>(〈InsInitE Skip (New T[e])〉,Norm s) \<mapsto>1 (〈InsInitE Skip (New T[e'])〉,s')" InsInitNewA: "[|G\<turnstile>abupd (check_neg i) (Norm s) \<midarrow>halloc (Arr T (the_Intg i))\<succ>a-> s' |] ==> G\<turnstile>(〈InsInitE Skip (New T[Lit i])〉,Norm s) \<mapsto>1 (〈Ref a〉,s')" (* cf. 15.15 *) CastE: "[|G\<turnstile>(〈e〉,Norm s) \<mapsto>1 (〈e'〉,s')|] ==> G\<turnstile>(〈Cast T e〉,None,s) \<mapsto>1 (〈Cast T e'〉,s')" Cast: "[|s' = abupd (raise_if (¬G,s\<turnstile>v fits T) ClassCast) (Norm s)|] ==> G\<turnstile>(〈Cast T (Lit v)〉,Norm s) \<mapsto>1 (〈Lit v〉,s')" (* can be written without abupd, since we know Norm s *) InstE: "[|G\<turnstile>(〈e〉,Norm s) \<mapsto>1 (〈e'::expr〉,s')|] ==> G\<turnstile>(〈e InstOf T〉,Norm s) \<mapsto>1 (〈e'〉,s')" Inst: "[|b = (v≠Null ∧ G,s\<turnstile>v fits RefT T)|] ==> G\<turnstile>(〈(Lit v) InstOf T〉,Norm s) \<mapsto>1 (〈Lit (Bool b)〉,s')" (* cf. 15.7.1 *) (*Lit "G\<turnstile>(Lit v,None,s) \<mapsto>1 (Lit v,None,s)"*) UnOpE: "[|G\<turnstile>(〈e〉,Norm s) \<mapsto>1 (〈e'〉,s') |] ==> G\<turnstile>(〈UnOp unop e〉,Norm s) \<mapsto>1 (〈UnOp unop e'〉,s')" UnOp: "G\<turnstile>(〈UnOp unop (Lit v)〉,Norm s) \<mapsto>1 (〈Lit (eval_unop unop v)〉,Norm s)" BinOpE1: "[|G\<turnstile>(〈e1〉,Norm s) \<mapsto>1 (〈e1'〉,s') |] ==> G\<turnstile>(〈BinOp binop e1 e2〉,Norm s) \<mapsto>1 (〈BinOp binop e1' e2〉,s')" BinOpE2: "[|need_second_arg binop v1; G\<turnstile>(〈e2〉,Norm s) \<mapsto>1 (〈e2'〉,s') |] ==> G\<turnstile>(〈BinOp binop (Lit v1) e2〉,Norm s) \<mapsto>1 (〈BinOp binop (Lit v1) e2'〉,s')" BinOpTerm: "[|¬ need_second_arg binop v1|] ==> G\<turnstile>(〈BinOp binop (Lit v1) e2〉,Norm s) \<mapsto>1 (〈Lit v1〉,Norm s)" BinOp: "G\<turnstile>(〈BinOp binop (Lit v1) (Lit v2)〉,Norm s) \<mapsto>1 (〈Lit (eval_binop binop v1 v2)〉,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>(〈Super〉,Norm s) \<mapsto>1 (〈Lit (val_this s)〉,Norm s)" AccVA: "[|G\<turnstile>(〈va〉,Norm s) \<mapsto>1 (〈va'〉,s') |] ==> G\<turnstile>(〈Acc va〉,Norm s) \<mapsto>1 (〈Acc va'〉,s')" Acc: "[|groundVar va; ((v,vf),s') = the_var G (Norm s) va|] ==> G\<turnstile>(〈Acc va〉,Norm s) \<mapsto>1 (〈Lit v〉,s')" (* AccLVar: "G\<turnstile>(〈Acc (LVar vn)〉,Norm s) \<mapsto>1 (〈Lit (fst (lvar vn s))〉,Norm s)" AccFVar: "[|((v,vf),s') = fvar statDeclC stat fn a (Norm s)|] ==> G\<turnstile>(〈Acc ({accC,statDeclC,stat}(Lit a)..fn)〉,Norm s) \<mapsto>1 (〈Lit v〉,s')" AccAVar: "[|((v,vf),s') = avar G i a (Norm s)|] ==> G\<turnstile>(〈Acc ((Lit a).[Lit i])〉,Norm s) \<mapsto>1 (〈Lit v〉,s')" *) AssVA: "[|G\<turnstile>(〈va〉,Norm s) \<mapsto>1 (〈va'〉,s')|] ==> G\<turnstile>(〈va:=e〉,Norm s) \<mapsto>1 (〈va':=e〉,s')" AssE: "[|groundVar va; G\<turnstile>(〈e〉,Norm s) \<mapsto>1 (〈e'〉,s')|] ==> G\<turnstile>(〈va:=e〉,Norm s) \<mapsto>1 (〈va:=e'〉,s')" Ass: "[|groundVar va; ((w,f),s') = the_var G (Norm s) va|] ==> G\<turnstile>(〈va:=(Lit v)〉,Norm s) \<mapsto>1 (〈Lit v〉,assign f v s')" CondC: "[|G\<turnstile>(〈e0〉,Norm s) \<mapsto>1 (〈e0'〉,s')|] ==> G\<turnstile>(〈e0? e1:e2〉,Norm s) \<mapsto>1 (〈e0'? e1:e2〉,s')" Cond: "G\<turnstile>(〈Lit b? e1:e2〉,Norm s) \<mapsto>1 (〈if the_Bool b then e1 else e2〉,Norm s)" CallTarget: "[|G\<turnstile>(〈e〉,Norm s) \<mapsto>1 (〈e'〉,s')|] ==> G\<turnstile>(〈{accC,statT,mode}e·mn({pTs}args)〉,Norm s) \<mapsto>1 (〈{accC,statT,mode}e'·mn({pTs}args)〉,s')" CallArgs: "[|G\<turnstile>(〈args〉,Norm s) \<mapsto>1 (〈args'〉,s')|] ==> G\<turnstile>(〈{accC,statT,mode}Lit a·mn({pTs}args)〉,Norm s) \<mapsto>1 (〈{accC,statT,mode}Lit a·mn({pTs}args')〉,s')" Call: "[|groundExprs args; vs = map the_val args; D = invocation_declclass G mode s a statT (|name=mn,parTs=pTs|)),; s'=init_lvars G D (|name=mn,parTs=pTs|)), mode a' vs (Norm s)|] ==> G\<turnstile>(〈{accC,statT,mode}Lit a·mn({pTs}args)〉,Norm s) \<mapsto>1 (〈Callee (locals s) (Methd D (|name=mn,parTs=pTs|)),)〉,s')" Callee: "[|G\<turnstile>(〈e〉,Norm s) \<mapsto>1 (〈e'::expr〉,s')|] ==> G\<turnstile>(〈Callee lcls_caller e〉,Norm s) \<mapsto>1 (〈e'〉,s')" CalleeRet: "G\<turnstile>(〈Callee lcls_caller (Lit v)〉,Norm s) \<mapsto>1 (〈Lit v〉,(set_lvars lcls_caller (Norm s)))" Methd: "G\<turnstile>(〈Methd D sig〉,Norm s) \<mapsto>1 (〈body G D sig〉,Norm s)" Body: "G\<turnstile>(〈Body D c〉,Norm s) \<mapsto>1 (〈InsInitE (Init D) (Body D c)〉,Norm s)" InsInitBody: "[|G\<turnstile>(〈c〉,Norm s) \<mapsto>1 (〈c'〉,s')|] ==> G\<turnstile>(〈InsInitE Skip (Body D c)〉,Norm s) \<mapsto>1(〈InsInitE Skip (Body D c')〉,s')" InsInitBodyRet: "G\<turnstile>(〈InsInitE Skip (Body D Skip)〉,Norm s) \<mapsto>1 (〈Lit (the ((locals s) Result))〉,abupd (absorb Ret) (Norm s))" (* LVar: "G\<turnstile>(LVar vn,Norm s)" is already evaluated *) FVar: "[|¬ inited statDeclC (globs s)|] ==> G\<turnstile>(〈{accC,statDeclC,stat}e..fn〉,Norm s) \<mapsto>1 (〈InsInitV (Init statDeclC) ({accC,statDeclC,stat}e..fn)〉,Norm s)" InsInitFVarE: "[|G\<turnstile>(〈e〉,Norm s) \<mapsto>1 (〈e'〉,s')|] ==> G\<turnstile>(〈InsInitV Skip ({accC,statDeclC,stat}e..fn)〉,Norm s) \<mapsto>1 (〈InsInitV Skip ({accC,statDeclC,stat}e'..fn)〉,s')" InsInitFVar: "G\<turnstile>(〈InsInitV Skip ({accC,statDeclC,stat}Lit a..fn)〉,Norm s) \<mapsto>1 (〈{accC,statDeclC,stat}Lit a..fn〉,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: "[|G\<turnstile>(〈e1〉,Norm s) \<mapsto>1 (〈e1'〉,s')|] ==> G\<turnstile>(〈e1.[e2]〉,Norm s) \<mapsto>1 (〈e1'.[e2]〉,s')" AVarE2: "G\<turnstile>(〈e2〉,Norm s) \<mapsto>1 (〈e2'〉,s') ==> G\<turnstile>(〈Lit a.[e2]〉,Norm s) \<mapsto>1 (〈Lit a.[e2']〉,s')" (* AVar: 〈(Lit a).[Lit i]〉 is fully evaluated *) (* evaluation of expression lists *) -- {* @{text Nil} is fully evaluated *} ConsHd: "[|G\<turnstile>(〈e::expr〉,Norm s) \<mapsto>1 (〈e'::expr〉,s')|] ==> G\<turnstile>(〈e#es〉,Norm s) \<mapsto>1 (〈e'#es〉,s')" ConsTl: "[|G\<turnstile>(〈es〉,Norm s) \<mapsto>1 (〈es'〉,s')|] ==> G\<turnstile>(〈(Lit v)#es〉,Norm s) \<mapsto>1 (〈(Lit v)#es'〉,s')" (* execution of statements *) (* cf. 14.5 *) Skip: "G\<turnstile>(〈Skip〉,Norm s) \<mapsto>1 (〈SKIP〉,Norm s)" ExprE: "[|G\<turnstile>(〈e〉,Norm s) \<mapsto>1 (〈e'〉,s')|] ==> G\<turnstile>(〈Expr e〉,Norm s) \<mapsto>1 (〈Expr e'〉,s')" Expr: "G\<turnstile>(〈Expr (Lit v)〉,Norm s) \<mapsto>1 (〈Skip〉,Norm s)" LabC: "[|G\<turnstile>(〈c〉,Norm s) \<mapsto>1 (〈c'〉,s')|] ==> G\<turnstile>(〈l• c〉,Norm s) \<mapsto>1 (〈l• c'〉,s')" Lab: "G\<turnstile>(〈l• Skip〉,s) \<mapsto>1 (〈Skip〉, abupd (absorb l) s)" (* cf. 14.2 *) CompC1: "[|G\<turnstile>(〈c1〉,Norm s) \<mapsto>1 (〈c1'〉,s')|] ==> G\<turnstile>(〈c1;; c2〉,Norm s) \<mapsto>1 (〈c1';; c2〉,s')" Comp: "G\<turnstile>(〈Skip;; c2〉,Norm s) \<mapsto>1 (〈c2〉,Norm s)" (* cf. 14.8.2 *) IfE: "[|G\<turnstile>(〈e〉 ,Norm s) \<mapsto>1 (〈e'〉,s')|] ==> G\<turnstile>(〈If(e) s1 Else s2〉,Norm s) \<mapsto>1 (〈If(e') s1 Else s2〉,s')" If: "G\<turnstile>(〈If(Lit v) s1 Else s2〉,Norm s) \<mapsto>1 (〈if the_Bool v then s1 else s2〉,Norm s)" (* cf. 14.10, 14.10.1 *) Loop: "G\<turnstile>(〈l• While(e) c〉,Norm s) \<mapsto>1 (〈If(e) (Cont l•c;; l• While(e) c) Else Skip〉,Norm s)" Jmp: "G\<turnstile>(〈Jmp j〉,Norm s) \<mapsto>1 (〈Skip〉,(Some (Jump j), s))" ThrowE: "[|G\<turnstile>(〈e〉,Norm s) \<mapsto>1 (〈e'〉,s')|] ==> G\<turnstile>(〈Throw e〉,Norm s) \<mapsto>1 (〈Throw e'〉,s')" Throw: "G\<turnstile>(〈Throw (Lit a)〉,Norm s) \<mapsto>1 (〈Skip〉,abupd (throw a) (Norm s))" TryC1: "[|G\<turnstile>(〈c1〉,Norm s) \<mapsto>1 (〈c1'〉,s')|] ==> G\<turnstile>(〈Try c1 Catch(C vn) c2〉, Norm s) \<mapsto>1 (〈Try c1' Catch(C vn) c2〉,s')" Try: "[|G\<turnstile>s \<midarrow>sxalloc-> s'|] ==> G\<turnstile>(〈Try Skip Catch(C vn) c2〉, s) \<mapsto>1 (if G,s'\<turnstile>catch C then (〈c2〉,new_xcpt_var vn s') else (〈Skip〉,s'))" FinC1: "[|G\<turnstile>(〈c1〉,Norm s) \<mapsto>1 (〈c1'〉,s')|] ==> G\<turnstile>(〈c1 Finally c2〉,Norm s) \<mapsto>1 (〈c1' Finally c2〉,s')" Fin: "G\<turnstile>(〈Skip Finally c2〉,(a,s)) \<mapsto>1 (〈FinA a c2〉,Norm s)" FinAC: "[|G\<turnstile>(〈c〉,s) \<mapsto>1 (〈c'〉,s')|] ==> G\<turnstile>(〈FinA a c〉,s) \<mapsto>1 (〈FinA a c'〉,s')" FinA: "G\<turnstile>(〈FinA a Skip〉,s) \<mapsto>1 (〈Skip〉,abupd (abrupt_if (a≠None) a) s)" Init1: "[|inited C (globs s)|] ==> G\<turnstile>(〈Init C〉,Norm s) \<mapsto>1 (〈Skip〉,Norm s)" Init: "[|the (class G C)=c; ¬ inited C (globs s)|] ==> G\<turnstile>(〈Init C〉,Norm s) \<mapsto>1 (〈(if C = Object then Skip else (Init (super c)));; Expr (Callee (locals s) (InsInitE (init c) SKIP))〉 ,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>(〈InsInitE Skip SKIP〉,Norm s) \<mapsto>1 (〈SKIP〉,Norm s)" (* Equivalenzen: Bigstep zu Smallstep komplett. Smallstep zu Bigstep, nur wenn nicht die Ausdrücke Callee, FinA ,… *) lemma rtrancl_imp_rel_pow: "p ∈ R^* ==> ∃n. p ∈ R^n" proof - assume "p ∈ R*" moreover obtain x y where p: "p = (x,y)" by (cases p) ultimately have "(x,y) ∈ R*" by hypsubst hence "∃n. (x,y) ∈ R^n" proof induct fix a have "(a,a) ∈ R^0" by simp thus "∃n. (a,a) ∈ R ^ n" .. next fix a b c assume "∃n. (a,b) ∈ R ^ n" then obtain n where "(a,b) ∈ R^n" .. moreover assume "(b,c) ∈ R" ultimately have "(a,c) ∈ R^(Suc n)" by auto thus "∃n. (a,c) ∈ R^n" .. qed with p show ?thesis by hypsubst qed (* lemma imp_eval_trans: assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>-> (v,s1)" shows trans: "G\<turnstile>(t,s0) \<mapsto>* (〈Lit v〉,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… G\<turnstile>(t,s0) \<mapsto>* (t',s1) ∧ the_vals t' = v *) end
lemma groundVar_cases:
[| groundVar v; !!ln. v = LVar ln ==> P; !!accC statDeclC stat a fn. v = {accC,statDeclC,stat}Lit a..fn ==> P; !!a i. v = Lit a.[Lit i] ==> P |] ==> P
lemma the_var_FVar_simp:
the_var G s ({accC,statDeclC,stat}Lit a..fn) = fvar statDeclC stat fn a s
lemma the_var_AVar_simp:
the_var G s (Lit a.[Lit i]) = avar G i a s
lemma rtrancl_imp_rel_pow:
p ∈ R* ==> ∃n. p ∈ R ^ n