(*  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

PRELIMINARY!!!!!!!!
*)

theory Trans imports Evaln begin

definition
  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)

definition
  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]

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

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

inductive
  step :: "[prog,term × state,term × state] → bool" (‹_⊨_ ↦1 _›[61,82,82] 81)
  for G :: prog
where

(* 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\<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⊨(⟨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: "\<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⊨(⟨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: 
   "[G⊨abupd (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,s⊨v 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 = (v≠Null ∧ G,s⊨v fits RefT T)]
          ==>
          G⊨(⟨(Lit v) InstOf T⟩,Norm s) ↦1 (⟨Lit (Bool b)⟩,s')"

  (* cf. 15.7.1 *)
(*Lit                           "G\<turnstile>(Lit v,None,s) \<mapsto>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\<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:  "[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}e⋅mn({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 a⋅mn({pTs}args)⟩,Norm s)
                ↦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⊨(⟨{accC,statT,mode}Lit a⋅mn({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\<turnstile>(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›.
  rules for accessing variables (‹Acc›) and assigning to variables
 ‹Ass›), test this with the predicate ‹groundVar›. After
  is done and the ‹FVar› is evaluated, we can't just
  away the ‹InsInitFVar› term and return a literal value, as in the
  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: \<langle>(Lit a).[Lit i]\<rangle> 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 l∙c;; 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:   "[G⊨s ←-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 (a≠None) 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)"

abbreviation
  stepn:: "[prog, term × state,nat,term × state] → bool" (‹_⊨_ ↦_ _›[61,82,82] 81)
  where "G⊨p ↦n p' ≡ (p,p') ∈ {(x, y). step G x y}^^n"

abbreviation
  steptr:: "[prog,term × state,term × state] → bool" (‹_⊨_ ↦* _›[61,82,82] 81)
  where "G⊨p ↦* 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 ,\<dots>
*)

(*
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