# Theory Trans

Up to index of Isabelle/HOL/Bali

theory Trans
imports Evaln
begin

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