Theory Trans

(*  Title:      HOL/Bali/Trans.thy
    Author:     David von Oheimb and Norbert Schirmer

Operational transition (small-step) semantics of the 
execution of Java expressions and statements


theory Trans imports Evaln begin

  groundVar :: "var  bool" where
  "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:
  assumes ground: "groundVar v"
  obtains (LVar) ln where "v=LVar ln"
    | (FVar) accC statDeclC stat a fn where "v={accC,statDeclC,stat}(Lit a)..fn"
    | (AVar) a i where "v=(Lit a).[Lit i]"
  using ground LVar FVar AVar
  by (cases v) (auto simp add: groundVar_def)

  groundExprs :: "expr list  bool"
  where "groundExprs es  (e  set es. v. e = Lit v)"
primrec the_val:: "expr  val"
  where "the_val (Lit v) = v"

primrec the_var:: "prog  state  var  (vvar × state)" where
  "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]

  Ref :: "loc  expr"
  where "Ref a == Lit (Addr a)"

  SKIP :: "expr"
  where "SKIP == Lit Unit"

  step :: "[prog,term × state,term × state]  bool" ("__ ↦1 _"[61,82,82] 81)
  for G :: prog

(* 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(t,Some xc,s) ↦1 (Lit undefined,Some xc,s)"

| InsInitE: "G(c,Norm s) ↦1 (c', s')
             G(InsInitE c e,Norm s) ↦1 (InsInitE c' e, s')"

(* SeqE: "G⊢(⟨Seq Skip e⟩,Norm s) ↦1 (⟨e⟩, Norm s)" *)
(* Specialised rules to evaluate: 
   InsInitE Skip (NewC C), InisInitE Skip (NewA T[e]) *)
  (* cf. 15.8.1 *)
| NewC: "G(NewC C,Norm s) ↦1 (InsInitE (Init C) (NewC C), Norm s)"
| NewCInited: "G Norm s ─halloc (CInst C)a s' 
               G(InsInitE Skip (NewC C),Norm s) ↦1 (Ref a, s')"

(* Alternative when rule SeqE is present 
NewCInited: "⟦inited C (globs s); 
              G⊢ Norm s ─halloc (CInst C)≻a→ s'⟧ 
              G⊢(⟨NewC C⟩,Norm s) ↦1 (⟨Ref a⟩, s')"

     "⟦¬ inited C (globs s)⟧ 
      G⊢(⟨NewC C⟩,Norm s) ↦1 (⟨Seq (Init C) (NewC C)⟩, Norm s)"

  (* cf. 15.9.1 *)
| NewA: 
   "G(New T[e],Norm s) ↦1 (InsInitE (init_comp_ty T) (New T[e]),Norm s)"
| InsInitNewAIdx: 
   "G(e,Norm s) ↦1 (e', s')
    G(InsInitE Skip (New T[e]),Norm s) ↦1 (InsInitE Skip (New T[e']),s')"
| InsInitNewA: 
   "Gabupd (check_neg i) (Norm s) ─halloc (Arr T (the_Intg i))a s' 
    G(InsInitE Skip (New T[Lit i]),Norm s) ↦1 (Ref a,s')"
  (* cf. 15.15 *)
| CastE:
   "G(e,Norm s) ↦1 (e',s') 
    G(Cast T e,None,s) ↦1 (Cast T e',s')" 
| Cast:
   "s' = abupd (raise_if (¬G,sv fits T)  ClassCast) (Norm s) 
    G(Cast T (Lit v),Norm s) ↦1 (Lit v,s')"
  (* can be written without abupd, since we know Norm s *)

| InstE: "G(e,Norm s) ↦1 (e'::expr,s') 
        G(e InstOf T,Norm s) ↦1 (e',s')" 
| Inst:  "b = (vNull  G,sv fits RefT T) 
          G((Lit v) InstOf T,Norm s) ↦1 (Lit (Bool b),s')"

  (* cf. 15.7.1 *)
(*Lit                           "G⊢(Lit v,None,s) ↦1 (Lit v,None,s)"*)

| UnOpE:  "G(e,Norm s) ↦1 (e',s') 
           G(UnOp unop e,Norm s) ↦1 (UnOp unop e',s')"
| UnOp:   "G(UnOp unop (Lit v),Norm s) ↦1 (Lit (eval_unop unop v),Norm s)"

| BinOpE1:  "G(e1,Norm s) ↦1 (e1',s') 
             G(BinOp binop e1 e2,Norm s) ↦1 (BinOp binop e1' e2,s')"
| BinOpE2:  "need_second_arg binop v1; G(e2,Norm s) ↦1 (e2',s') 
             G(BinOp binop (Lit v1) e2,Norm s) 
              ↦1 (BinOp binop (Lit v1) e2',s')"
| BinOpTerm:  "¬ need_second_arg binop v1
               G(BinOp binop (Lit v1) e2,Norm s) 
                ↦1 (Lit v1,Norm s)"
| BinOp:    "G(BinOp binop (Lit v1) (Lit v2),Norm s) 
              ↦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(Super,Norm s) ↦1 (Lit (val_this s),Norm s)"

| AccVA: "G(va,Norm s) ↦1 (va',s') 
          G(Acc va,Norm s) ↦1 (Acc va',s')"
| Acc:  "groundVar va; ((v,vf),s') = the_var G (Norm s) va
         G(Acc va,Norm s) ↦1 (Lit v,s')"

AccLVar: "G⊢(⟨Acc (LVar vn)⟩,Norm s) ↦1 (⟨Lit (fst (lvar vn s))⟩,Norm s)"
AccFVar: "⟦((v,vf),s') = fvar statDeclC stat fn a (Norm s)⟧
          G⊢(⟨Acc ({accC,statDeclC,stat}(Lit a)..fn)⟩,Norm s) 
           ↦1 (⟨Lit v⟩,s')"
AccAVar: "⟦((v,vf),s') = avar G i a (Norm s)⟧
          G⊢(⟨Acc ((Lit a).[Lit i])⟩,Norm s) ↦1 (⟨Lit v⟩,s')"
| AssVA:  "G(va,Norm s) ↦1 (va',s') 
           G(va:=e,Norm s) ↦1 (va':=e,s')"
| AssE:   "groundVar va; G(e,Norm s) ↦1 (e',s') 
           G(va:=e,Norm s) ↦1 (va:=e',s')"
| Ass:    "groundVar va; ((w,f),s') = the_var G (Norm s) va 
           G(va:=(Lit v),Norm s) ↦1 (Lit v,assign f v s')"

| CondC: "G(e0,Norm s) ↦1 (e0',s') 
          G(e0? e1:e2,Norm s) ↦1 (e0'? e1:e2,s')"
| Cond:  "G(Lit b? e1:e2,Norm s) ↦1 (if the_Bool b then e1 else e2,Norm s)"

| CallTarget: "G(e,Norm s) ↦1 (e',s') 
               G({accC,statT,mode}emn({pTs}args),Norm s) 
                ↦1 ({accC,statT,mode}e'mn({pTs}args),s')"
| CallArgs:   "G(args,Norm s) ↦1 (args',s') 
               G({accC,statT,mode}Lit amn({pTs}args),Norm s) 
                ↦1 ({accC,statT,mode}Lit amn({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({accC,statT,mode}Lit amn({pTs}args),Norm s) 
                ↦1 (Callee (locals s) (Methd D name=mn,parTs=pTs),s')"
| Callee:     "G(e,Norm s) ↦1 (e'::expr,s')
               G(Callee lcls_caller e,Norm s) ↦1 (e',s')"

| CalleeRet:   "G(Callee lcls_caller (Lit v),Norm s) 
                 ↦1 (Lit v,(set_lvars lcls_caller (Norm s)))"

| Methd: "G(Methd D sig,Norm s) ↦1 (body G D sig,Norm s)"

| Body: "G(Body D c,Norm s) ↦1 (InsInitE (Init D) (Body D c),Norm s)"

| InsInitBody: 
    "G(c,Norm s) ↦1 (c',s')
     G(InsInitE Skip (Body D c),Norm s) ↦1(InsInitE Skip (Body D c'),s')"
| InsInitBodyRet: 
     "G(InsInitE Skip (Body D Skip),Norm s)
       ↦1 (Lit (the ((locals s) Result)),abupd (absorb Ret) (Norm s))"

(*   LVar: "G⊢(LVar vn,Norm s)" is already evaluated *)
| FVar: "¬ inited statDeclC (globs s)
         G({accC,statDeclC,stat}e..fn,Norm s) 
          ↦1 (InsInitV (Init statDeclC) ({accC,statDeclC,stat}e..fn),Norm s)"
| InsInitFVarE:
      "G(e,Norm s) ↦1 (e',s')
       G(InsInitV Skip ({accC,statDeclC,stat}e..fn),Norm s) 
        ↦1 (InsInitV Skip ({accC,statDeclC,stat}e'..fn),s')"
| InsInitFVar:
      "G(InsInitV Skip ({accC,statDeclC,stat}Lit a..fn),Norm s) 
        ↦1 ({accC,statDeclC,stat}Lit a..fn,Norm s)"
― ‹Notice, that we do not have literal values for vars›. 
The rules for accessing variables (Acc›) and assigning to variables 
(Ass›), test this with the predicate groundVar›.  After 
initialisation is done and the FVar› is evaluated, we can't just 
throw away the InsInitFVar› term and return a literal value, as in the 
cases of New›  or NewC›. Instead we just return the evaluated 
FVar› and test for initialisation in the rule FVar›.›

| AVarE1: "G(e1,Norm s) ↦1 (e1',s') 
           G(e1.[e2],Norm s) ↦1 (e1'.[e2],s')"

| AVarE2: "G(e2,Norm s) ↦1 (e2',s') 
           G(Lit a.[e2],Norm s) ↦1 (Lit a.[e2'],s')"

(* AVar: ⟨(Lit a).[Lit i]⟩ is fully evaluated *)

(* evaluation of expression lists *)

  ― ‹Nil›  is fully evaluated›

| ConsHd: "G(e::expr,Norm s) ↦1 (e'::expr,s') 
           G(e#es,Norm s) ↦1 (e'#es,s')"
| ConsTl: "G(es,Norm s) ↦1 (es',s') 
           G((Lit v)#es,Norm s) ↦1 ((Lit v)#es',s')"

(* execution of statements *)

  (* cf. 14.5 *)
| Skip: "G(Skip,Norm s) ↦1 (SKIP,Norm s)"

| ExprE: "G(e,Norm s) ↦1 (e',s') 
          G(Expr e,Norm s) ↦1 (Expr e',s')"
| Expr:  "G(Expr (Lit v),Norm s) ↦1 (Skip,Norm s)"

| LabC: "G(c,Norm s) ↦1 (c',s') 
         G(l c,Norm s) ↦1 (l c',s')"
| Lab:  "G(l Skip,s) ↦1 (Skip, abupd (absorb l) s)"

  (* cf. 14.2 *)
| CompC1: "G(c1,Norm s) ↦1 (c1',s') 
           G(c1;; c2,Norm s) ↦1 (c1';; c2,s')"

| Comp:   "G(Skip;; c2,Norm s) ↦1 (c2,Norm s)"

  (* cf. 14.8.2 *)
| IfE: "G(e ,Norm s) ↦1 (e',s') 
        G(If(e) s1 Else s2,Norm s) ↦1 (If(e') s1 Else s2,s')"
| If:  "G(If(Lit v) s1 Else s2,Norm s) 
         ↦1 (if the_Bool v then s1 else s2,Norm s)"

  (* cf. 14.10, 14.10.1 *)
| Loop: "G(l While(e) c,Norm s) 
          ↦1 (If(e) (Cont lc;; l While(e) c) Else Skip,Norm s)"

| Jmp: "G(Jmp j,Norm s) ↦1 (Skip,(Some (Jump j), s))"

| ThrowE: "G(e,Norm s) ↦1 (e',s') 
           G(Throw e,Norm s) ↦1 (Throw e',s')"
| Throw:  "G(Throw (Lit a),Norm s) ↦1 (Skip,abupd (throw a) (Norm s))"

| TryC1: "G(c1,Norm s) ↦1 (c1',s') 
          G(Try c1 Catch(C vn) c2, Norm s) ↦1 (Try c1' Catch(C vn) c2,s')"
| Try:   "Gs ─sxalloc→ s'
          G(Try Skip Catch(C vn) c2, s) 
           ↦1 (if G,s'⊢catch C then (c2,new_xcpt_var vn s')
                                else (Skip,s'))"

| FinC1: "G(c1,Norm s) ↦1 (c1',s') 
          G(c1 Finally c2,Norm s) ↦1 (c1' Finally c2,s')"

| Fin:    "G(Skip Finally c2,(a,s)) ↦1 (FinA a c2,Norm s)"

| FinAC: "G(c,s) ↦1 (c',s')
          G(FinA a c,s) ↦1 (FinA a c',s')"
| FinA: "G(FinA a Skip,s) ↦1 (Skip,abupd (abrupt_if (aNone) a) s)"

| Init1: "inited C (globs s) 
          G(Init C,Norm s) ↦1 (Skip,Norm s)"
| Init: "the (class G C)=c; ¬ inited C (globs s)  
         G(Init C,Norm s) 
          ↦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))"
― ‹InsInitE› is just used as trick to embed the statement 
init c› into an expression› 
| InsInitESKIP:
    "G(InsInitE Skip SKIP,Norm s) ↦1 (SKIP,Norm s)"

  stepn:: "[prog, term × state,nat,term × state]  bool" ("__ _ _"[61,82,82] 81)
  where "Gp n p'  (p,p')  {(x, y). step G x y}^^n"

  steptr:: "[prog,term × state,term × state]  bool" ("__ ↦* _"[61,82,82] 81)
  where "Gp ↦* p'  (p,p')  {(x, y). step G x y}*"
(* Equivalenzen:
  Bigstep zu Smallstep komplett.
  Smallstep zu Bigstep, nur wenn nicht die Ausdrücke Callee, FinA ,…

lemma imp_eval_trans:
  assumes eval: "G⊢s0 ─t≻→ (v,s1)" 
    shows trans: "G⊢(t,s0) ↦* (⟨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⊢(t,s0) ↦* (t',s1) ∧ the_vals t' = v