(* Time-stamp: <Sat Nov 29 2008 00:35:55 Stardate: [-28]0409.91 hwloidl>

   The Grail Hume Processor, formalised as Isabelle theory file.
   This version is used in D17 as program logic
   Variant:
   - quantifying over function names, not arbitrary expressions, in CallVar
   - collecting pre-conds for CallVar in preUnderApp and preExactApp
   - using an undefined tickExp function (see ResAlg), param over syntax and ResConst
   Major change:
   . redefined PConInd and CostrInd, so that aux lemmas env_env_notin and ConstrInd_h_same
     can be proven (see VdmDerived.thy)
*)

header {* GRUMPY *}

(*<*)
theory GRUMPY = Basics + Grail + ResAlg:
(*>*)

text {* 
 GRUMPY is a VM at a higher level than HAM, more akin to the JVM-subset used
 in Grail without the method/o-o stuff. The point of this VM is to have a
 more convenient basis for doing reasoning, while still being able to prove
 exact resource bounds. The semantics for Hume could be phrased directly in 
 terms of GRUMPY, then showing equivalence btw HAM and GRUMPY or as translation
 function as used in Trans.thy (not finished, yet).
*}

subsection {* Function parameters, arguments and frames *}

text {* Formal parameters of functions and actual arguments 
        of functions are bound via these 2 relations *}

types ParamType = "VarName list"
types ArgType = "VarName list"

text {* In the paper I just use function update over vectors; check if we can use
 this in the Isabelle theory, too. *}

consts FrameInd :: "(ParamType \<times> ArgType \<times> Env \<times> Env) set"
inductive FrameInd intros
FrameInd_NIL: "([],[],E,emptyEnv):FrameInd"
FrameInd_CONS: "\<lbrakk> (ps,as,E,E'):FrameInd; E''=fun_upd E' x (E y) \<rbrakk>
                \<Longrightarrow> (x # ps, y # as, E,E''):FrameInd"

consts FrameIndHO :: "(ParamType \<times> (Ref list) \<times> Env \<times> Env) set"
inductive FrameIndHO intros
FrameIndHO_NIL: "([],[],E,emptyEnv):FrameIndHO"
FrameIndHO_CONS: "\<lbrakk> (ps,rs,E,E'):FrameIndHO; E''=fun_upd E' x (R r) \<rbrakk>
                \<Longrightarrow> (x # ps, r # rs, E,E''):FrameIndHO"

syntax bindArgs_  :: "[ParamType, ArgType, Env, Env] \<Rightarrow> bool"   ("_ <=| _ . _ = _ ")

translations "ps <=| as . E = E'" == "(ps,as,E,E') : FrameInd"

consts PConInd :: "(VarName list \<times> Ref list \<times> Env \<times> Env) set"
inductive PConInd intros
PConInd_NIL:  "([], [], E, E):PConInd"
PConInd_CONS: "\<lbrakk> (xs,rs,E,E'):PConInd; E''=fun_upd E' x (R r) \<rbrakk>
               \<Longrightarrow> (x # xs, r # rs, E, E''):PConInd"

consts ConstrInd :: "(VarName list \<times> Ref list \<times> Env \<times> Heap \<times> Heap) set"
inductive ConstrInd intros
ConstrInd_NIL:  "([], [], E, h, h):ConstrInd"
ConstrInd_CONS: "\<lbrakk> (xs,rs,E,h,h):ConstrInd; (R r) = E x \<rbrakk>
               \<Longrightarrow> (x # xs, r # rs, E, h, h):ConstrInd"

text {* A table matching function name to list of parameter types and the body *}

types
 FunTable = "FunName \<Rightarrow> (ParamType \<times> Exp)"

consts
 funTab :: FunTable

subsection {* GRUMPY Semantics *}

text {* 
  Big-step operational semantics, for patterns and for expressions. 
  In a pattern, we have the location against which we are matching as additional argumetn.
*}

consts semmatch :: "(Env \<times> Heap \<times> Pattern \<times> Locn \<times> Env \<times> HoVal) set" -- {* operational semantics *}

syntax semmatch_  :: "[Env, Heap, Pattern, Locn, Env, HoVal] \<Rightarrow> bool"   ("MATCH _, _ \<turnstile> _ @ _ \<Down> '(_, _  ')")

translations "MATCH E, h \<turnstile> e @ l \<Down> (E',v)" == "(E,h,e,l,E',v) : semmatch"

consts semexpn :: "(Env \<times> Heap \<times> Exp \<times> nat \<times> HoVal \<times> Heap \<times> Rescomp) set" -- {* operational semantics *}

syntax semexpn_  :: "[Env, Heap, Exp, nat, HoVal, Heap, Rescomp] \<Rightarrow> bool"   (" _, _ \<turnstile> _ \<Down>_ '(_ , _, _ ')")

translations "E, h \<turnstile> e \<Down>n (v,h',p)" == "(E,h,e,n,v,h',p) : semexpn"

(* NB: Underapp only works on CallVar; need to assign the funid to a var first, if it's underapplied *)

inductive semmatch intros
 (* Patterns *)
 semPVal: "\<lbrakk> fmap_lookup h l = Some w \<rbrakk>
           \<Longrightarrow> MATCH E, h \<turnstile> (PVal w) @ l \<Down> (E,R (Ref l))"
 semPValFail: "\<lbrakk> \<not> (fmap_lookup h l = Some w) \<rbrakk>
           \<Longrightarrow> MATCH E, h \<turnstile> (PVal w) @ l \<Down> (E,\<bottom>)"
 semPVar: "MATCH E, h \<turnstile> (PVar x) @ l \<Down> (E(x:=(R (Ref l))),R (Ref l))"
 semPWild: "MATCH E, h \<turnstile> (PWild i) @ l \<Down> (E, R (Ref l))"
 semPCon: "\<lbrakk> \<exists> rs . fmap_lookup h l = Some (C c rs) \<and> (vs, rs, E, E'):PConInd \<rbrakk>
          \<Longrightarrow> MATCH E, h \<turnstile> (PCon c vs) @ l \<Down> (E',R (Ref l))"
 semPConFail: "\<lbrakk> \<not> ( \<exists> rs . fmap_lookup h l = Some (C c rs) ) \<rbrakk>
          \<Longrightarrow> MATCH E, h \<turnstile> (PCon c vs) @ l \<Down> (E,\<bottom>)"

inductive semexpn intros
 (* Expessions  *)
 semValue: "E, h \<turnstile> (ValueExp v) \<Down>1 (v, h, tickExp (ValueExp v) RCUndef)"
 semVar: "\<lbrakk> E x = v \<rbrakk> 
           \<Longrightarrow> E, h \<turnstile> (VarExp x) \<Down>1 (v,h,tickExp (VarExp x)  RCUndef)"
 semConstr: "\<lbrakk> l = freshloc (fmap_dom h) ; (xs,rs,E,h,h'):ConstrInd; h'' = fmap_upd h' l (C c rs) \<rbrakk> 
             \<Longrightarrow> E, h \<turnstile> (ConstrExp c xs) \<Down>1 (R (Ref l),h'',tickExp (ConstrExp c xs) RCUndef)"
 semPrimBin: "\<lbrakk> i = E x ; j = E y ; v = f i j \<rbrakk>
             \<Longrightarrow> E, h \<turnstile> (PrimBin f x y) \<Down>1 (v,h,tickExp (PrimBin f x y) RCUndef)"
 semRPrimBin: "\<lbrakk> R (Ref lx) = E x ; R (Ref ly) = E y ; fmap_lookup h lx = Some vx ; fmap_lookup h ly = Some vy ; v = f vx vy \<rbrakk>
              \<Longrightarrow> E, h \<turnstile> (RPrimBin f x y) \<Down>1 (v,h,tickExp (RPrimBin f x y) RCUndef)"
 semIfTrue: "\<lbrakk> E x = B True ; E, h \<turnstile> e1 \<Down>n (v, h',p')\<rbrakk>
               \<Longrightarrow> E, h \<turnstile> (IfExp x e1 e2) \<Down>(Suc n) (v, h', p'\<smile>tickExp (IfExp x e1 e2) RCUndef)"
 semIfFalse: "\<lbrakk> E x = B False ; E, h \<turnstile> e2 \<Down>n (v, h',p')\<rbrakk>
                \<Longrightarrow> E, h \<turnstile> (IfExp x e1 e2) \<Down>(Suc n) (v, h', p'\<smile>tickExp (IfExp x e1 e2) RCUndef)"
 semLet: "\<lbrakk> E, h \<turnstile> e1 \<Down>m (v,h',p'); E(x:=v), h' \<turnstile> e2 \<Down>n (v'', h'',p'') \<rbrakk>
          \<Longrightarrow> E, h \<turnstile> (LetExp x e1 e2) \<Down>(m+n) (v'', h'', p'\<smile>p''\<smile>tickExp (LetExp x e1 e2) RCUndef)"
 semCallFun: 
   "\<lbrakk> ((fst (funTab f)), xs, E, E'):FrameInd ; E', h \<turnstile> (snd (funTab f)) \<Down>n (v, h',p) \<rbrakk>
    \<Longrightarrow> E, h \<turnstile> (CallFunExp f xs) \<Down>(Suc n) (v, h', p\<smile>tickExp (CallFunExp f xs) RCUndef)"
 semCallVarExact: 
   "\<lbrakk> R (Ref (l::nat)) = E x ; Some (X f i rs) = fmap_lookup h l ; (as,e)=(funTab f); 
      i+(length xs)=(length (fst (funTab f))); 
      (fst (funTab f), rs@(map (\<lambda> x . theRef (E x)) xs), E, E'):FrameIndHO ; 
      E', h \<turnstile> snd (funTab f) \<Down>n (v, h',p) \<rbrakk>
    \<Longrightarrow> E, h \<turnstile> (CallVarExp x xs) \<Down>(Suc n) (v, h', p\<smile>tickExp (CallVarExp x xs) RCUndef)"
 semCallVarUnderApp: 
   "\<lbrakk> R (Ref (l::nat)) = E x ; Some (X f i rs) = fmap_lookup h l ; (as,e)=(funTab f);
      i+(length xs)<(length as); 
      l' = freshloc (fmap_dom h);
      h' = fmap_upd h l' (X f (i+(length xs)) (rs@map (\<lambda> x . theRef (E x)) xs)) \<rbrakk>
    \<Longrightarrow> E, h \<turnstile> (CallVarExp x xs) \<Down>1 (R (Ref l'), h', tickExp (CallVarExp x xs) RCUndef)"
 semCaseOneTrue: 
   "\<lbrakk> R (Ref (l::nat)) = E x ;  
      MATCH E, h \<turnstile> b @ l \<Down> (Ej, vj); vj\<noteq>\<bottom>  ;
      Ej, h \<turnstile> e \<Down>n (v, h',p') \<rbrakk>
    \<Longrightarrow> E, h \<turnstile> (CaseOneExp x b e e') \<Down>(n+1) (v, h', p'\<smile>tickExp (CaseOneExp x b e e') RCUndef)"
 semCaseOneFalse: 
   "\<lbrakk> R (Ref (l::nat)) = E x ;  
      MATCH E, h \<turnstile> b @ l \<Down> (Ej, vj); vj=\<bottom> ;  
      E, h \<turnstile> e' \<Down>n (v, h',p') \<rbrakk>
    \<Longrightarrow> E, h \<turnstile> (CaseOneExp x b e e') \<Down>(n+1) (v, h', p'\<smile>tickExp (CaseOneExp x b e e') RCUndef)"

(* tickExp (CaseOneExp x b e e') E h p')" *)

text {* Assumes 0-cost pattern matching; needs to be refined! *}

subsection {* Basic properties *}
text {*We also provide elimination lemmas for the inductively defined relation*}

inductive_cases semmatch_cases: 
 "MATCH E, h \<turnstile> PVal i     @ l \<Down> (E,v)"
 "MATCH E, h \<turnstile> PVar x     @ l \<Down> (E,v)"
 "MATCH E, h \<turnstile> PWild i    @ l \<Down> (E,v)"
 "MATCH E, h \<turnstile> PCon c vs  @ l \<Down> (E,v)"

inductive_cases semexpn_cases: 
 "E, h \<turnstile> (ValueExp i) \<Down>n (v,h',p')"
 "E, h \<turnstile> (VarExp x) \<Down>n (v,h',p')"
 "E, h \<turnstile> (PrimBin f x y) \<Down>n (v,h',p')"
 "E, h \<turnstile> (RPrimBin f x y) \<Down>n (v,h',p')"
 "E, h \<turnstile> (ConstrExp c x) \<Down>n (v,h',p')"
 "E, h \<turnstile> (IfExp x e2 e3) \<Down>n (v,h',p')"
 "E, h \<turnstile> (LetExp x e1 e2) \<Down>n (v,h',p')"
 "E, h \<turnstile> (CallFunExp f xs) \<Down>n (v,h',p')"
 "E, h \<turnstile> (CallVarExp x xs) \<Down>n (v,h',p')"
 "E, h \<turnstile> (CaseOneExp x b e e') \<Down>n (v,h',p')"

lemma no_zero_height_derivsAux: "\<forall> E h h' v p'. E, h \<turnstile> e \<Down>0 (v,h',p') \<longrightarrow> False"
apply (clarify)
apply (induct e)
apply (simp_all)?
apply (elim semexpn_cases, insert Zero_not_Suc, fastsimp)+
apply (insert Suc_not_Zero, fastsimp)
apply (elim semexpn_cases, insert Zero_not_Suc, fastsimp)+
apply (insert Zero_not_Suc, fastsimp)
apply (elim semexpn_cases)
apply simp
apply (erule semexpn.cases) apply simp_all
done

text {* Operational semantics without height index *}

constdefs
 semexp :: "[Env, Heap, Exp, HoVal, Heap, Rescomp] \<Rightarrow> bool"  (" _, _ \<turnstile> _ \<Down> '(_ , _, _ ')")
 "E, h \<turnstile> e \<Down> (v,h',p) \<equiv> (\<exists> n. (E, h \<turnstile> e \<Down>n (v,h',p)))"

text {* 
 The main rules, that show new language features, are semCallV.. and semCase.

 In semCallV we distinguish between exact-, under and over-app, and we need
 a closure as value for the function variable. Either a new closure with 
 the additional value is built (underapp) or the body is executed (exactapp).
 This doesn't reflect the closure-chains as used in the HAM. But maybe these
 can be accounted for just in the cost.
 
 In semCase we go over all branches, require that branches 1..j-1 do not match, 
 and execute the body of the j-th (ie. matching) branch. 
 Costs are more complicated here, but the Hume Op Sem D spells this out in mpre
 detail anyway.
*}

subsection {* Program Logic *}

text {*
 Again a VDM style program logic, using a shallow embedding into Isabelle/HOL.
 Partial correctness. 
 We could later adapt the termination logic and bring it into this project,
 since there is no stand-alone publication on this material so far. 

*}

types Assertion = "Env \<Rightarrow> Heap \<Rightarrow> Heap \<Rightarrow> HoVal \<Rightarrow> Rescomp \<Rightarrow> bool"

types Context = "(Exp \<times> Assertion) set"
(* types PattContext = "(Pattern \<times> VarName \<times> Assertion) set" *)

consts vdm :: "(Context \<times> Exp \<times> Assertion) set" -- {* VDM-style program logic *}

syntax vdm_  :: "[Context, Exp, Assertion] \<Rightarrow> bool"   (" _ \<rhd> _ : _")

translations "G \<rhd> e : P" == "(G,e,P) : vdm"

consts vdmpat :: "(Context \<times> Pattern \<times> VarName \<times> Assertion) set"

syntax vdmpat_  :: "[Context, Pattern, VarName, Assertion] \<Rightarrow> bool"   ("MATCH _ \<rhd> _ @ _ : _")

translations "MATCH G \<rhd> p @ x : A" == "(G,p,x,A) : vdmpat"

text {* Note: vdmpat is UNUSED;  the vdm rules sempat directly *}

inductive vdmpat intros
(* Patterns *)
vdmPVal: "MATCH G \<rhd> (PVal v) @ x : \<lambda> E h hh v p. (\<exists> l. R (Ref l) = E x  \<and> fmap_lookup h l = Some v)"
vdmPVar: "MATCH G \<rhd> (PVar y) @ x : \<lambda> E h hh v p. E x = E y"
vdmPWild: "MATCH G \<rhd> (PWild i) @ x : \<lambda> E h hh v p. h = hh"
vdmPCon: "MATCH G \<rhd> (PCon c ys) @ x : \<lambda> E h hh v p. (\<exists> l rs. R (Ref l) = E x \<and> fmap_lookup h l = Some (C c rs) \<and> (\<forall> (i::nat). i<(length rs) \<longrightarrow> E (nth ys i) = R (nth rs i)))"

text {* aux defs used in vdmCallVar *}

(* this is \<Phi> in the paper *)
constdefs preUnderApp :: "Env \<Rightarrow> Heap \<Rightarrow> Heap \<Rightarrow> HoVal \<Rightarrow> VarName \<Rightarrow> (VarName list) \<Rightarrow> bool"
"preUnderApp \<equiv> \<lambda> E h hh v x xs. (\<exists> l l' f i rs. ((E x)=(R (Ref l)) \<and> (fmap_lookup h l)=(Some (X f i rs)) \<and> i+(length xs)<(length (fst (funTab f))) \<and> l'=freshloc (fmap_dom h) \<and> v=R (Ref l') \<and> hh=fmap_upd h l' (X f (i+(length xs)) (rs@map (\<lambda> x . theRef (E x)) xs))))"

(* this is \<Psi> in the paper *)
constdefs preExactApp :: "Env \<Rightarrow> Heap \<Rightarrow> Heap \<Rightarrow> HoVal \<Rightarrow> FunName \<Rightarrow> (Ref list) \<Rightarrow> VarName \<Rightarrow> (VarName list) \<Rightarrow> bool"
"preExactApp \<equiv> \<lambda> E' h hh v f rs x xs. (\<exists> l i . ((E' x)=(R (Ref l)) \<and> (fmap_lookup h l)=(Some (X f i rs)) \<and> (i+(length xs)=length (fst (funTab f)))))"


inductive vdm intros
(* Expessions *)
vdmValue:   "G \<rhd> ValueExp w : \<lambda> E h hh v p. (v=w \<and> h=hh \<and> p=tickExp (ValueExp w) RCUndef)"
vdmVar:     "G \<rhd> VarExp x : \<lambda> E h hh v p. (v=E x \<and> h=hh \<and> p=tickExp (VarExp x) RCUndef)"
vdmConstr:  "G \<rhd> ConstrExp c xs : \<lambda> E h hh v p. (\<exists> l rs h'. l = freshloc (fmap_dom h) \<and> (xs,rs,E,h,h'):ConstrInd \<and> v=R (Ref l) \<and>  hh = fmap_upd h' l (C c rs) \<and> p=tickExp (ConstrExp c xs) RCUndef)"
vdmPrimBin: "G \<rhd> PrimBin f x y : \<lambda> E h hh v p. (\<exists> i j. E x = i \<and> E y = j \<and> v = f i j \<and> h=hh \<and> p=tickExp (PrimBin f x y) RCUndef)"
vdmRPrimBin: "G \<rhd> RPrimBin f x y : \<lambda> E h hh v p. (\<exists> lx ly vx vy. R (Ref lx) = E x \<and> R (Ref ly) = E y \<and> fmap_lookup h lx = Some vx \<and> fmap_lookup h ly = Some vy \<and> v = f vx vy \<and> h=hh \<and> p=tickExp (RPrimBin f x y) RCUndef)"
vdmIf: "\<lbrakk> G \<rhd> e1 : P1 ; G \<rhd> e2 : P2 \<rbrakk> \<Longrightarrow>
          G \<rhd> (IfExp x e1 e2) : \<lambda> E h hh v p. (((E x=B True \<longrightarrow> (\<exists> p'. P1 E h hh v p' \<and> p=(p'\<smile>tickExp (IfExp x e1 e2) RCUndef))) \<and> 
                                                (E x=B False \<longrightarrow> (\<exists> p'. P2 E h hh v p' \<and> p=(p'\<smile>tickExp (IfExp x e1 e2) RCUndef)))))"
vdmLet:  "\<lbrakk> G \<rhd> e1 : P1 ; G \<rhd> e2 : P2 \<rbrakk> \<Longrightarrow>
          G \<rhd> LetExp x e1 e2 : \<lambda> E h hh v p. \<exists> v' h' p' p''.
                  ((P1 E h h' v' p') \<and> (P2 (fun_upd E x v') h' hh v p'') \<and> (p=(p'\<smile>p''\<smile>tickExp (LetExp x e1 e2) RCUndef)))"
vdmCallFun: "\<lbrakk> insert (CallFunExp f xs , P) G \<rhd> snd (funTab f) : \<lambda> E h hh v p. (\<forall> E'. (fst (funTab f),xs,E',E):FrameInd \<longrightarrow> (P E' h hh v (p\<smile>tickExp (CallFunExp f xs) RCUndef))) \<rbrakk> \<Longrightarrow> 
           G \<rhd> CallFunExp f xs : P"
vdmCallVar: "\<lbrakk> (\<forall> E h hh v . preUnderApp E h hh v x xs \<longrightarrow> P E h hh v (tickExp (CallVarExp x xs) RCUndef));
               (\<forall> f.  insert (CallVarExp x xs, P) G \<rhd> snd (funTab f) : (\<lambda> E h hh v p. 
                       (\<forall> E'. (\<exists> rs. preExactApp E' h hh v f rs x xs \<and> (fst (funTab f), rs@(map (\<lambda> x . theRef (E' x)) xs), E', E):FrameIndHO) \<longrightarrow> P E' h hh v (p\<smile>tickExp (CallVarExp x xs) RCUndef)) 
                        )) \<rbrakk> \<Longrightarrow>
           G \<rhd> CallVarExp x xs : P"
vdmCaseOne: "\<lbrakk> G \<rhd> e : P ; G \<rhd> e' : P' \<rbrakk> \<Longrightarrow>
          G \<rhd> CaseOneExp x b e e' : (\<lambda> E h hh v p . 
             \<forall> (l::Locn). R (Ref l) = E x \<longrightarrow>
                (\<forall> E' v'.
                       MATCH E, h \<turnstile> b @ l \<Down> (E',v') \<longrightarrow> 
                         ((v'=\<bottom> \<longrightarrow> (\<exists> p'. P' E  h hh v p' \<and> p=(p'\<smile>tickExp (CaseOneExp x b e e') RCUndef))) \<and>
                          (v'\<noteq>\<bottom> \<longrightarrow> (\<exists> p'. P  E' h hh v p' \<and> p=(p'\<smile>tickExp (CaseOneExp x b e e') RCUndef))))))"
vdmAx:     "\<lbrakk> (e,P):G \<rbrakk> \<Longrightarrow> G \<rhd> e :P"
vdmConseq: "\<lbrakk> \<forall> E h h' v p. P E h h' v p \<longrightarrow> Q E h h' v p ; G \<rhd> e : P \<rbrakk> \<Longrightarrow> G \<rhd> e : Q"

(*
lemma bonzo_13: "\<forall> xs rs n E h h' . (xs,rs,n,E,h,h'):ConstrInd \<longrightarrow> (\<forall> (i::nat). i<n \<longrightarrow> E (nth xs i) = R (nth rs i))"
apply (rule allI)+
apply (rule impI)
apply (rule_tac ConstrInd.induct)
defer 1
apply clarsimp
apply clarify
apply (case_tac "i=na")
apply clarsimp
*)

(* UNUSED
 The judgement for patterns contains as rightmost element an assertion, induced by 
 the pattern, under which the rhs of the branch must be true (see Case).
*)
(*
lemmas "vdmCase": "\<lbrakk> \<And> (i::nat). (i < length bs) \<longrightarrow> (\<forall> Q. (MATCH G \<rhd> fst (nth bs i) @ x : Q) \<longrightarrow> ((G \<rhd> snd (nth bs i) : (\<lambda> E h hh v p . Q E h hh v p \<longrightarrow> P E h hh v p)))) \<rbrakk> \<Longrightarrow>
          G \<rhd> CaseExp x bs : P"
oops
*)
(*
vdmCase: "\<lbrakk> \<And> i . i<(length bs) \<longrightarrow> (\<exists> G' . MATCH G \<rhd> fst (nth bs i) @ x : G' \<and> G' \<rhd> snd (nth bs i) : P)  \<rbrakk>
          \<Longrightarrow>  G \<rhd> (CaseExp x bs) : P "
*)
(* \<Down>(n+m+1) (v', h'', tickExp (CaseExp x bs) E h p)" *)

(*
vdmCallV: "\<lbrakk> \<forall> as e . (G \<rhd> e : (\<lambda> E h hh v p. (\<forall> l f i vs E' p'.
              (((E x)=(R (Ref l)) \<and> (fmap_lookup h l)=(Some (X f i vs)) \<and> (as,e)=(funTab f) \<and>
              (as,vs@(map (\<lambda> x. theRef (E' x)) xs),E',E):FrameIndHO)
              \<longrightarrow> P E' h v p (tickExp (CallVarExp x xs) E h p))))) \<rbrakk> \<Longrightarrow>
           G \<rhd> CallVarExp x xs : P"
*)

text {* Validity *}

constdefs  validn :: "nat \<Rightarrow> Exp \<Rightarrow> Assertion \<Rightarrow> bool"  ("\<Turnstile>\<^sub>_ _ : _" 50)
"\<Turnstile>\<^sub>n e : P \<equiv> (\<forall> m . m \<le> n \<longrightarrow> (\<forall> E h h' v p . ((E, h \<turnstile> e \<Down>m (v,h',p)) \<longrightarrow> P E h h' v p)))"

constdefs  valid :: "Exp \<Rightarrow> Assertion \<Rightarrow> bool"  ("\<Turnstile> _ : _" 50)
"\<Turnstile> e : P \<equiv> (\<forall> E h h' v p . ((E, h \<turnstile> e \<Down> (v,h',p)) \<longrightarrow> P E h h' v p))"

constdefs ctxt_validn::"nat \<Rightarrow>  Context \<Rightarrow> bool"  ("|\<Turnstile>\<^sub>_ _" 60)
"|\<Turnstile>\<^sub>n G \<equiv> (\<forall> (e,P) \<in> G . \<Turnstile>\<^sub>n e : P)"

constdefs ctxt_valid::" Context \<Rightarrow> bool"  ("|\<Turnstile> _" 60)
"|\<Turnstile> G \<equiv> (\<forall> (e,P) \<in> G . \<Turnstile> e : P)"

constdefs valid_in_ctxt :: " Context \<Rightarrow>  Exp \<Rightarrow> Assertion \<Rightarrow> bool" ("_ \<Turnstile> _ : _" 75)
 "G \<Turnstile> e : P \<equiv>  ( |\<Turnstile> G ) \<longrightarrow> (\<Turnstile> e:P)"

constdefs valid_in_ctxt_n :: " Context \<Rightarrow> nat \<Rightarrow> Exp \<Rightarrow> Assertion \<Rightarrow> bool" ("_ \<Turnstile>\<^sub> _ _ : _" 75)
 "G \<Turnstile>\<^sub>n e : P \<equiv>  ( |\<Turnstile>\<^sub>n G ) \<longrightarrow> ( \<Turnstile>\<^sub>n e:P)"

(* top-level validity statement, used in the paper version of the soundness statement *)
constdefs testme :: " Context \<Rightarrow> Exp \<Rightarrow> Assertion \<Rightarrow> bool" ("TESTME _ \<Turnstile> _ : _" 75)
 "TESTME G \<Turnstile> e : P \<equiv> \<forall> n. ((\<forall> (e,P) \<in> G . \<Turnstile>\<^sub>n e : P) \<longrightarrow> ( \<Turnstile>\<^sub>n e:P))"

text {*
 Simple lemmas over variants of the validity statement.
*}

lemma valid_validn: "\<Turnstile> e : P \<Longrightarrow>  \<Turnstile>\<^sub>n e : P"
apply (simp add: valid_def validn_def semexp_def)
apply (fastsimp)
done

lemma validn_valid: "(\<forall> n . \<Turnstile>\<^sub>n e : P) \<Longrightarrow> \<Turnstile> e : P"
apply (simp add: valid_def validn_def semexp_def)
apply (fastsimp)
done

lemma ctxt_valid_validn: "( |\<Turnstile> G) \<Longrightarrow> (\<forall> n.( |\<Turnstile>\<^sub>n G))"
apply (simp add: ctxt_validn_def ctxt_valid_def)
apply clarsimp
apply (auto elim: valid_validn)
done

lemma emptyctxn [simp]: "|\<Turnstile>\<^sub>n {}"
apply (simp add: ctxt_validn_def)
done

lemma ctxt_projn[rule_format]: "(e,P) \<in> G \<and> |\<Turnstile>\<^sub>n G \<Longrightarrow> (\<Turnstile>\<^sub>n e : P)"
apply (simp add: ctxt_validn_def)
apply (fastsimp)
done

lemma ctxt_drop: "( |\<Turnstile> {(e,P)} \<union> G) \<Longrightarrow> |\<Turnstile> G"
apply (simp add: ctxt_valid_def)
done

lemma ctxt_ext[simp]: "( |\<Turnstile> {(e,P)} \<union> G) = ((\<Turnstile> e : P ) \<and> ( |\<Turnstile> G))"
apply (simp add: ctxt_valid_def)
done

lemma empty_ctxt [simp]: "|\<Turnstile> {}"
apply (simp add: ctxt_valid_def)
done

lemma ctxt_subn[rule_format]:  "H \<subseteq> G \<and> |\<Turnstile>\<^sub>n G \<Longrightarrow> |\<Turnstile>\<^sub>n H"
apply (simp add: ctxt_validn_def validn_def)
apply (fast)
done

lemma ctxt_cons: "\<lbrakk> |\<Turnstile> G; \<Turnstile> e : P\<rbrakk> \<Longrightarrow> |\<Turnstile> G \<union> {(e,P)}"
apply (simp add: ctxt_valid_def)
done

lemma ctxt_validn_valid[rule_format]: "(\<forall> n. |\<Turnstile>\<^sub>n G) \<Longrightarrow> |\<Turnstile> G"
apply (simp add: ctxt_validn_def ctxt_valid_def valid_def validn_def semexp_def)
apply (fastsimp)
done

lemma ctxt_valid_validn: "|\<Turnstile> G \<Longrightarrow> (\<forall> n. |\<Turnstile>\<^sub>n G)"
apply (simp add: ctxt_validn_def ctxt_valid_def valid_def validn_def semexp_def)
apply (fastsimp)
done

lemma lowerm: "\<lbrakk>  m < n; \<Turnstile>\<^sub>n e:P \<rbrakk> \<Longrightarrow> \<Turnstile>\<^sub>m e : P"
apply (simp add: validn_def)
apply clarsimp
apply (subgoal_tac "ma < n")
prefer 2 apply simp
apply (erule_tac thin_rl)
apply (erule_tac x="ma" in allE)
apply simp
done
 
lemma lowerm_suc: "\<lbrakk>  \<Turnstile>\<^sub>(Suc n) e:P \<rbrakk> \<Longrightarrow> \<Turnstile>\<^sub>n e : P"
(*<*)
apply (simp add: validn_def)
apply clarsimp
apply (erule_tac x="m" in allE)
apply simp
done
(*>*)

lemma ctxt_lower: "\<lbrakk> |\<Turnstile>\<^sub>n G; m<n \<rbrakk> \<Longrightarrow> |\<Turnstile>\<^sub>m G"
(*<*)
apply (simp add: ctxt_validn_def)
apply clarsimp
apply (rule lowerm)
apply fastsimp+
done
(*>*)

(* lemmas ctxt_lower_suc = ctxt_lower [of "Suc n" G n]; *)

lemma ctxt_lower_suc: "\<lbrakk> |\<Turnstile>\<^sub>(Suc n) G \<rbrakk> \<Longrightarrow> |\<Turnstile>\<^sub>n G"
(*<*)
apply (simp add: ctxt_validn_def)
apply clarsimp
apply (rule lowerm)
apply fastsimp+
done
(*>*)

lemma ctxt_consn: "\<lbrakk> |\<Turnstile>\<^sub>n G; \<Turnstile>\<^sub>n e:P \<rbrakk> \<Longrightarrow> ( |\<Turnstile>\<^sub>n {(e,P)} \<union> G)"
(*<*)by (simp add: ctxt_validn_def)(*>*)

lemma ctxt_insertn: "\<lbrakk> |\<Turnstile>\<^sub>n G; \<Turnstile>\<^sub>n e:P \<rbrakk> \<Longrightarrow> ( |\<Turnstile>\<^sub>n (insert (e,P) G))"
(*<*)by (simp add: ctxt_validn_def)(*>*)


(*
constdefs ctxt_validn :: "nat \<Rightarrow> Context \<Rightarrow> bool"  (" |\<Turnstile>\<^sub>_ _ " [900,900] 900)
"ctxt_validn n G == \<forall> e P. (e,P):G \<longrightarrow> \<Turnstile>\<^sub>n e : P"

"ctxt_validn n G == \<forall> eg Ag. (eg,Ag):G \<longrightarrow> (\<forall> E h h' v p . E, h \<turnstile> eg \<Down>n (v,h',p) \<longrightarrow> Ag E h hh v p \<longrightarrow> E, h \<turnstile> e \<Down>n (v,h',p) \<longrightarrow> P E h hh v p)"


constdefs valid_in_ctxt :: "Context \<Rightarrow> Exp \<Rightarrow> Assertion \<Rightarrow> bool"  ("_ \<Turnstile> _ : _")
"valid_in_ctxt G e P == \<exists> n. |\<Turnstile>\<^sub>n G \<longrightarrow> \<Turnstile>\<^sub>n e : P"

"valid G e P == \<forall> eg Ag. (eg,Ag):G \<longrightarrow> (\<forall> E h h' v p n . E, h \<turnstile> eg \<Down>n (v,h',p) \<longrightarrow> Ag E h hh v p \<longrightarrow> E, h \<turnstile> e \<Down>n (v,h',p) \<longrightarrow> P E h hh v p)"

syntax valid :: "Exp \<Rightarrow> Assertion \<Rightarrow> bool"  ("\<Turnstile> _ : _")
translations "\<Turnstile> e : P" == "valid e P"

constdefs valid :: "Exp \<Rightarrow> Assertion \<Rightarrow> bool"  ("\<Turnstile> _ : _")
"valid e P == (\<emptyset> \<Turnstile> e : P)"
*)

lemma bonzo_10[rule_format]: "\<forall> rs E E' E''. (xs,rs,E,E'):PConInd \<longrightarrow> (xs,rs,E,E''):PConInd \<longrightarrow> E'=E''"
apply (induct_tac xs)
apply clarsimp
apply (erule_tac PConInd.cases)
apply simp_all 
apply (erule_tac PConInd.cases)
apply simp_all 
apply clarsimp
apply (rotate_tac -1)
apply (erule_tac PConInd.cases) apply simp_all
apply (rotate_tac -4)
apply (erule_tac PConInd.cases) apply simp_all 
apply clarsimp
apply (erule_tac x="rsb" in allE)
apply (erule_tac x="Eb" in allE)
apply (erule_tac x="E'a" in allE)
apply (erule impE)
apply assumption
apply (erule_tac x="E'b" in allE)
apply clarsimp
done

lemma bonzo_11[rule_format]: "\<forall> E h l E' E'' v' v''. MATCH E, h \<turnstile> b @ l \<Down> (E', v') \<longrightarrow> MATCH E, h \<turnstile> b @ l \<Down> (E'', v'')  \<longrightarrow> E'=E'' \<and> v'=v''"
apply (case_tac b)
apply simp_all
apply clarsimp
apply (erule semmatch.cases)
apply simp_all
apply (erule semmatch.cases)
apply simp_all
(* PVal *)
apply clarsimp
apply (erule semmatch.cases)
apply simp_all
apply (erule semmatch.cases)
apply simp_all
apply clarsimp
apply (erule semmatch.cases)
apply simp_all
(* PCon *)
defer 1
(* PWild *)
apply clarsimp
apply (erule semmatch.cases)
apply simp_all
apply clarsimp
apply (erule semmatch.cases)
apply simp_all
apply clarsimp
(* PCon *)
apply clarsimp?
apply (erule semmatch.cases)
apply simp_all
apply clarsimp
apply (erule semmatch.cases)
apply simp_all
apply clarsimp
apply (drule bonzo_10)
apply fastsimp
apply assumption
apply clarsimp
apply (erule semmatch.cases)
apply simp_all
done

lemma bonzo_21[rule_format] :"\<forall> l l' E x . R (Ref l) = E x \<and> R (Ref l') = E x \<longrightarrow> l = l' "
apply clarsimp
apply (case_tac "E x = R (Ref l)")
apply fastsimp
apply fastsimp
done

subsection {* Soundness of the VDM-style logic *}

text {* 
  Aux lemmas for soundness theorem 
*}
(*
lemma callsound00: "\<forall> e P G. ((e, P) \<in> G \<longrightarrow>
                       ( \<forall>n. ( ( |\<Turnstile>\<^sub>n G) \<longrightarrow>
                         (\<forall>m. (m \<le> n \<longrightarrow>
                           (\<forall> E h h' v p. (E, h \<turnstile> e \<Down>m (v, h', p) \<longrightarrow> P E h h' v p)))))))"
apply (rule allI)+
apply (rule impI)
apply (rule allI)
apply (rule impI)
apply (subgoal_tac "\<Turnstile>\<^sub>n e : P")
apply (simp add: ctxt_validn_def validn_def) 
apply (simp add: ctxt_validn_def, fastsimp)
done


lemma callsound01: "\<forall> f xs e P G. ((e, P) \<in> G \<longrightarrow>
                      (\<forall>n. ( ( |\<Turnstile>\<^sub>n G) \<longrightarrow> 
                        (G \<rhd> CallFunExp f xs : P) \<longrightarrow>
                          (\<forall>m. m \<le> n \<longrightarrow> G \<Turnstile>\<^sub>m e : P) \<longrightarrow>
                            G  \<Turnstile>\<^sub>n CallFunExp f xs : P )))"
apply (rule allI)+
apply (rule impI)
apply (rule allI)
apply (induct_tac n)
apply clarsimp
apply (erule thin_rl)
apply (erule thin_rl)
apply (erule thin_rl)
apply (insert no_zero_height_derivsAux)
apply (simp add: valid_in_ctxt_def valid_in_ctxt_n_def ctxt_validn_def valid_def validn_def)
(* recursion case *)
apply (rotate_tac -1)
apply (erule thin_rl)
apply clarsimp
apply (simp add: valid_in_ctxt_def valid_in_ctxt_n_def ctxt_validn_def valid_def validn_def)
apply clarsimp
sorry

lemma callsound02: "\<forall> n. (\<forall>m. m \<le> n \<longrightarrow> (insert (CallFunExp f xs, P) G) \<Turnstile>\<^sub>m (snd (funTab f)) : \<lambda> E h hh v p. (\<forall> E'. ((fst (funTab f)),xs,E',E):FrameInd \<longrightarrow> (P E' h hh v (tickExp (CallFunExp f xs) E h p)))) 
                    \<longrightarrow> G  \<Turnstile>\<^sub>n CallFunExp f xs : P "
apply (simp add: valid_in_ctxt_def valid_in_ctxt_n_def ctxt_validn_def valid_def validn_def)
apply clarsimp
apply (erule semexpn.cases)
apply simp_all
apply clarsimp

oops
*)


lemma validn_valid_in_ctxt[rule_format]: "(\<forall> n. G \<Turnstile>\<^sub>n e : P) \<longrightarrow> G \<Turnstile> e : P"
apply clarsimp
apply (simp add: valid_in_ctxt_def)
apply clarsimp
apply (rule validn_valid)
apply (simp add: valid_in_ctxt_n_def)
apply clarsimp
apply (erule_tac x="n" in allE)
apply (erule impE)
apply (frule ctxt_valid_validn)
apply (erule_tac x="n" in allE)
apply assumption
apply assumption
done

(*
lemma valid_validn_in_ctxt[rule_format]: " G \<Turnstile> e : P  \<longrightarrow> (\<forall> n. G \<Turnstile>\<^sub>n e : P)"
apply (simp add: valid_in_ctxt_def valid_in_ctxt_n_def)
apply clarsimp
apply (rule valid_validn)
apply (erule impE)
defer 1
apply assumption
apply (simp only: ctxt_valid_def ctxt_validn_def)
apply clarify
oops
*)

(*
lemma CallFunSoundAux: "\<lbrakk> \<And> as e . (as, e)=(funTab f) \<longrightarrow>
        insert (CallFunExp f xs , P) G \<rhd> e : \<lambda> E h hh v p. (\<forall> E'. (as,xs,E',E):FrameInd \<longrightarrow> (P E' h hh v (tickExp (CallFunExp f xs) E h p))) ; G \<rhd> CallFunExp f xs : P \<rbrakk>
             \<Longrightarrow> 
      (\<forall> n . G \<Turnstile>\<^sub>n e : P)"
apply (rule allI)
apply (insert callsound00)
apply (induct_tac n)
apply (insert no_zero_height_derivsAux)
apply fast
(* recursion case *)
apply (rotate_tac -1)
apply (simp add: valid_in_ctxt_def ctxt_validn_def valid_def validn_def)
apply clarify
(* apply (simp add: semexp_def) *)
(* apply (erule exE) *)
apply (erule semexpn.cases)
apply simp_all
apply clarsimp
oops
*)


lemma soundnessAux: "G \<rhd> e : P \<Longrightarrow> (\<forall> n. G \<Turnstile>\<^sub>n e : P)" 
apply (erule  vdm.induct)
(* ValueExp *)
apply clarify
apply (simp add: valid_in_ctxt_def valid_in_ctxt_n_def ctxt_validn_def valid_def validn_def)
apply clarsimp
apply (erule semexpn.cases)
apply simp_all
(*
apply (simp add: valid_in_ctxt_def ctxt_validn_def valid_def validn_def)
apply clarsimp
apply (simp add: tickExp_def)
*)
(* done with ValueExp *)
(* VarExp *)
apply clarify
apply (simp add: valid_in_ctxt_def valid_in_ctxt_n_def ctxt_validn_def valid_def validn_def)
apply clarsimp
apply (erule semexpn.cases)
apply simp_all
(* done with VarExp *)
(* ConstrExp *)
apply clarify
apply (simp add: valid_in_ctxt_def valid_in_ctxt_n_def ctxt_validn_def valid_def validn_def)
apply clarsimp
apply (erule semexpn.cases)
apply simp_all
apply clarsimp
apply (rule_tac x="rs" in exI)
apply (rule_tac x="h'a" in exI)
apply clarsimp
(* done with ConstrExp *)
(* PrimBin *)
apply clarify
apply (simp add: valid_in_ctxt_def valid_in_ctxt_n_def ctxt_validn_def valid_def validn_def)
apply clarsimp
apply (erule semexpn.cases)
apply simp_all
(* done with PrimBin *)
(* RPrimBin *)
apply clarify
apply (simp add: valid_in_ctxt_def valid_in_ctxt_n_def ctxt_validn_def valid_def validn_def)
apply clarsimp
apply (erule semexpn.cases)
apply simp_all
apply (rule_tac x="lx" in exI)
apply clarsimp
apply (rule_tac x="ly" in exI)
apply clarsimp
(* done with RPrimBin *)
(* IfExp *)
apply clarify
apply (simp add: valid_in_ctxt_def valid_in_ctxt_n_def valid_def validn_def)
apply clarsimp
apply (erule semexpn.cases)
apply simp_all
apply (erule thin_rl)
apply (rule_tac x="p'" in exI)
apply (rule conjI)
apply clarify
apply (erule_tac x="n" in allE)  apply (rotate_tac -1)
apply (erule impE)
apply assumption
apply (erule thin_rl)
apply (erule thin_rl)
apply (erule thin_rl)
apply (rotate_tac -1)
apply (erule_tac x="na" in allE) apply (rotate_tac -1)
apply (erule impE)
apply simp
apply (rotate_tac -1)
apply (erule_tac x="Ea" in allE) apply (rotate_tac -1)
apply (erule_tac x="ha" in allE) apply (rotate_tac -1)
apply (erule_tac x="h'a" in allE) apply (rotate_tac -1)
apply (erule_tac x="va" in allE) apply (rotate_tac -1)
apply (erule_tac x="p'" in allE) apply (rotate_tac -1)
apply (erule impE)
apply assumption
apply assumption
apply simp
(* subcase: False *)
apply clarify
apply (simp add: valid_in_ctxt_def valid_in_ctxt_n_def valid_def validn_def)
apply clarsimp?
apply (rule_tac x="p'" in exI)
apply (rule conjI)
apply clarify?
apply (erule thin_rl)
apply (erule thin_rl)
apply (erule thin_rl)
apply (erule_tac x="n" in allE)  apply (rotate_tac -1)
apply (erule impE)
apply assumption
apply (erule_tac x="na" in allE) apply (rotate_tac -1)
apply (erule impE)
apply simp
apply (rotate_tac -1)
apply (erule_tac x="Ea" in allE) apply (rotate_tac -1)
apply (erule_tac x="ha" in allE) apply (rotate_tac -1)
apply (erule_tac x="h'a" in allE) apply (rotate_tac -1)
apply (erule_tac x="va" in allE) apply (rotate_tac -1)
apply (erule_tac x="p'" in allE) apply (rotate_tac -1)
apply (erule impE)
apply assumption
apply assumption
apply simp
(* done with IfExp *)
(* LetExp *)
apply clarify
apply (simp add: valid_in_ctxt_def valid_in_ctxt_n_def valid_def validn_def)
apply clarsimp
apply (erule semexpn.cases)
apply simp_all
apply (rule_tac x="va" in exI)
apply (rule_tac x="h'a" in exI)
apply (rule_tac x="p'" in exI)
apply (erule_tac x="n" in allE)  apply (rotate_tac -1)
apply (erule impE)
apply assumption
apply (rotate_tac -1)
apply (erule_tac x="ma" in allE)   apply (rotate_tac -1)
apply (erule impE)
apply simp
apply (rotate_tac -1)
apply (erule_tac x="Ea" in allE) apply (rotate_tac -1)
apply (erule_tac x="ha" in allE) apply (rotate_tac -1)
apply (erule_tac x="h'a" in allE) apply (rotate_tac -1)
apply (erule_tac x="va" in allE) apply (rotate_tac -1)
apply (erule_tac x="p'" in allE) apply (rotate_tac -1)
apply (erule impE)
apply assumption
apply (rule conjI)
apply assumption
apply (rule_tac x="p''" in exI)
apply (rule conjI)
apply (erule_tac x="n" in allE) apply (rotate_tac -1)
apply (erule impE) 
apply assumption
apply (rotate_tac -1)
apply (erule_tac x="na" in allE) apply (rotate_tac -1)
apply (erule impE) apply simp apply (rotate_tac -1)
apply (erule_tac x="Ea(xa := va)" in allE)  apply (rotate_tac -1)
apply (erule_tac x="h'a" in allE)           apply (rotate_tac -1)
apply (erule_tac x="h''" in allE)           apply (rotate_tac -1)
apply (erule_tac x="v''" in allE)           apply (rotate_tac -1)
apply (erule_tac x="p''" in allE)           apply (rotate_tac -1)
apply (erule impE)
apply assumption
apply assumption
apply clarsimp
(* done with LetExp *)
(* ToDos: CallFunExp, CallVarExp, CaseExp *)
(* CallFunExp *)
apply clarsimp
apply (erule thin_rl)
apply (induct_tac n)
apply (simp add: valid_in_ctxt_def valid_in_ctxt_n_def ctxt_validn_def valid_def validn_def)
apply (insert no_zero_height_derivsAux)
apply fast
(* recursion case *)
apply (rotate_tac -1) apply (erule thin_rl)
apply (simp (no_asm) add: valid_in_ctxt_def valid_in_ctxt_n_def)
apply clarsimp
apply (simp (no_asm) add: valid_def validn_def)
apply clarsimp
apply (erule semexpn.cases)  apply simp_all
apply clarsimp
apply (erule_tac x="na" in allE)
apply (simp add: valid_in_ctxt_def valid_in_ctxt_n_def)
apply (erule impE)
apply (rule ctxt_lower)
apply simp
apply simp
apply (erule impE)
apply (drule ctxt_lower_suc)
apply (erule thin_rl)
apply (erule thin_rl)
apply (erule thin_rl)
apply (drule ctxt_consn)
apply simp
apply simp
apply (simp only: valid_def validn_def) 
(* done with CallFunExp *)
(* TODOs: CallVarExp, CaseExp, structural rules *)
defer 1 
defer 1
(* vdmAx rule *)
apply clarify
apply (rotate_tac -1) apply (erule thin_rl)
apply (simp add: valid_in_ctxt_def valid_in_ctxt_n_def ctxt_validn_def valid_def validn_def)
apply fastsimp
(* vdmConseq rule *)
apply clarify
apply (rotate_tac -1) apply (erule thin_rl)
apply (simp add: valid_in_ctxt_def valid_in_ctxt_n_def ctxt_validn_def valid_def validn_def)
(* TODOs: CallVarExp, CaseExp *)
defer 1
(* CaseOneExp *)
apply (rotate_tac -1) apply (erule thin_rl)
apply clarify
apply (simp add: valid_in_ctxt_def valid_in_ctxt_n_def valid_def validn_def)
apply clarsimp
apply (case_tac b)
  apply simp_all
(* NB: all pattern-cases uses exactly the same proof script *)
(* PVar *)
  apply (erule semexpn.cases)
  apply simp_all
  apply clarsimp
  apply (subgoal_tac "l=la")
  apply clarsimp 
  apply (drule bonzo_11)
  apply fastsimp
  apply (erule_tac x="n" in allE) apply (rotate_tac -1)
  apply (erule impE)
  apply assumption
  apply (rotate_tac -1)
  apply (erule_tac x="na" in allE)  
  apply (rotate_tac -1)
  apply (erule impE)
  apply simp
  apply (rotate_tac -1)
  apply (erule_tac x="Ej" in allE) apply (rotate_tac -1)
  apply (erule_tac x="ha" in allE) apply (rotate_tac -1)
  apply (erule_tac x="h'a" in allE) apply (rotate_tac -1)
  apply (erule_tac x="va" in allE) apply (rotate_tac -1)
  apply (erule_tac x="p'" in allE) apply (rotate_tac -1)
  apply (erule impE)
  apply assumption
  apply simp
  (* instantiate intermediate p *)
  apply clarsimp
  apply (rule_tac x="p'" in exI)
  apply clarsimp
  apply (rule bonzo_21) (* l=la *)
  apply simp
  apply (subgoal_tac "l=la")
  apply clarsimp 
  apply (drule bonzo_11)
  apply fastsimp
  apply (erule thin_rl)
  apply (erule thin_rl)
  apply (erule_tac x="n" in allE) apply (rotate_tac -1)
  apply (erule impE)
  apply assumption
  apply (rotate_tac -1)
  apply (erule_tac x="na" in allE)  
  apply (rotate_tac -1)
  apply (erule impE)
  apply simp
  apply (rotate_tac -1)
  apply (erule_tac x="Ea" in allE) apply (rotate_tac -1)
  apply (erule_tac x="ha" in allE) apply (rotate_tac -1)
  apply (erule_tac x="h'a" in allE) apply (rotate_tac -1)
  apply (erule_tac x="va" in allE) apply (rotate_tac -1)
  apply (erule_tac x="p'" in allE) apply (rotate_tac -1)
  apply (erule impE)
  apply assumption
  apply simp
  (* instantiate intermediate p *)
  apply clarsimp
  apply (rule_tac x="p'" in exI)
  apply clarsimp
  apply (rule bonzo_21) (* l=la *)
  apply simp
(* PVal *)
  apply (erule semexpn.cases)
  apply simp_all
  apply clarsimp
  apply (subgoal_tac "l=la")
  apply clarsimp 
  apply (drule bonzo_11)
  apply fastsimp
  apply (erule_tac x="n" in allE) apply (rotate_tac -1)
  apply (erule impE)
  apply assumption
  apply (rotate_tac -1)
  apply (erule_tac x="na" in allE)  
  apply (rotate_tac -1)
  apply (erule impE)
  apply simp
  apply (rotate_tac -1)
  apply (erule_tac x="Ej" in allE) apply (rotate_tac -1)
  apply (erule_tac x="ha" in allE) apply (rotate_tac -1)
  apply (erule_tac x="h'a" in allE) apply (rotate_tac -1)
  apply (erule_tac x="va" in allE) apply (rotate_tac -1)
  apply (erule_tac x="p'" in allE) apply (rotate_tac -1)
  apply (erule impE)
  apply assumption
  apply simp
  (* instantiate intermediate p *)
  apply clarsimp
  apply (rule_tac x="p'" in exI)
  apply clarsimp
  apply (rule bonzo_21) (* l=la *)
  apply simp
  (* Fail *)
  apply (subgoal_tac "l=la")
  apply clarsimp 
  apply (drule bonzo_11)
  apply fastsimp
  apply (erule thin_rl)
  apply (erule thin_rl)
  apply (erule_tac x="n" in allE) apply (rotate_tac -1)
  apply (erule impE)
  apply assumption
  apply (rotate_tac -1)
  apply (erule_tac x="na" in allE)  
  apply (rotate_tac -1)
  apply (erule impE)
  apply simp
  apply (rotate_tac -1)
  apply (erule_tac x="Ea" in allE) apply (rotate_tac -1)
  apply (erule_tac x="ha" in allE) apply (rotate_tac -1)
  apply (erule_tac x="h'a" in allE) apply (rotate_tac -1)
  apply (erule_tac x="va" in allE) apply (rotate_tac -1)
  apply (erule_tac x="p'" in allE) apply (rotate_tac -1)
  apply (erule impE)
  apply assumption
  apply simp
  (* instantiate intermediate p *)
  apply clarsimp
  apply (rule_tac x="p'" in exI)
  apply clarsimp
  apply (rule bonzo_21) (* l=la *)
  apply simp
(* PCon *)
  apply (erule semexpn.cases)
  apply simp_all
  apply clarsimp
  apply (subgoal_tac "l=la")
  apply clarsimp 
  apply (drule bonzo_11)
  apply fastsimp
  apply (erule_tac x="n" in allE) apply (rotate_tac -1)
  apply (erule impE)
  apply assumption
  apply (rotate_tac -1)
  apply (erule_tac x="na" in allE)  
  apply (rotate_tac -1)
  apply (erule impE)
  apply simp
  apply (rotate_tac -1)
  apply (erule_tac x="Ej" in allE) apply (rotate_tac -1)
  apply (erule_tac x="ha" in allE) apply (rotate_tac -1)
  apply (erule_tac x="h'a" in allE) apply (rotate_tac -1)
  apply (erule_tac x="va" in allE) apply (rotate_tac -1)
  apply (erule_tac x="p'" in allE) apply (rotate_tac -1)
  apply (erule impE)
  apply assumption
  apply simp
  (* instantiate intermediate p *)
  apply clarsimp
  apply (rule_tac x="p'" in exI)
  apply clarsimp
  apply (rule bonzo_21) (* l=la *)
  apply simp
  (* Fail *)
  apply (subgoal_tac "l=la")
  apply clarsimp 
  apply (drule bonzo_11)
  apply fastsimp
  apply (erule thin_rl)
  apply (erule thin_rl)
  apply (erule_tac x="n" in allE) apply (rotate_tac -1)
  apply (erule impE)
  apply assumption
  apply (rotate_tac -1)
  apply (erule_tac x="na" in allE)  
  apply (rotate_tac -1)
  apply (erule impE)
  apply simp
  apply (rotate_tac -1)
  apply (erule_tac x="Ea" in allE) apply (rotate_tac -1)
  apply (erule_tac x="ha" in allE) apply (rotate_tac -1)
  apply (erule_tac x="h'a" in allE) apply (rotate_tac -1)
  apply (erule_tac x="va" in allE) apply (rotate_tac -1)
  apply (erule_tac x="p'" in allE) apply (rotate_tac -1)
  apply (erule impE)
  apply assumption
  apply simp
  (* instantiate intermediate p *)
  apply clarsimp
  apply (rule_tac x="p'" in exI)
  apply clarsimp
  apply (rule bonzo_21) (* l=la *)
  apply simp
(* PWild *)
  apply (erule semexpn.cases)
  apply simp_all
  apply clarsimp
  apply (subgoal_tac "l=la")
  apply clarsimp 
  apply (drule bonzo_11)
  apply fastsimp
  apply (erule_tac x="n" in allE) apply (rotate_tac -1)
  apply (erule impE)
  apply assumption
  apply (rotate_tac -1)
  apply (erule_tac x="na" in allE)  
  apply (rotate_tac -1)
  apply (erule impE)
  apply simp
  apply (rotate_tac -1)
  apply (erule_tac x="Ej" in allE) apply (rotate_tac -1)
  apply (erule_tac x="ha" in allE) apply (rotate_tac -1)
  apply (erule_tac x="h'a" in allE) apply (rotate_tac -1)
  apply (erule_tac x="va" in allE) apply (rotate_tac -1)
  apply (erule_tac x="p'" in allE) apply (rotate_tac -1)
  apply (erule impE)
  apply assumption
  apply simp
  (* instantiate intermediate p *)
  apply clarsimp
  apply (rule_tac x="p'" in exI)
  apply clarsimp
  apply (rule bonzo_21) (* l=la *)
  apply simp
  (* Fail *)
  apply (subgoal_tac "l=la")
  apply clarsimp 
  apply (drule bonzo_11)
  apply fastsimp
  apply (erule thin_rl)
  apply (erule thin_rl)
  apply (erule_tac x="n" in allE) apply (rotate_tac -1)
  apply (erule impE)
  apply assumption
  apply (rotate_tac -1)
  apply (erule_tac x="na" in allE)  
  apply (rotate_tac -1)
  apply (erule impE)
  apply simp
  apply (rotate_tac -1)
  apply (erule_tac x="Ea" in allE) apply (rotate_tac -1)
  apply (erule_tac x="ha" in allE) apply (rotate_tac -1)
  apply (erule_tac x="h'a" in allE) apply (rotate_tac -1)
  apply (erule_tac x="va" in allE) apply (rotate_tac -1)
  apply (erule_tac x="p'" in allE) apply (rotate_tac -1)
  apply (erule impE)
  apply assumption
  apply simp
  (* instantiate intermediate p *)
  apply clarsimp
  apply (rule_tac x="p'" in exI)
  apply clarsimp
  apply (rule bonzo_21) (* l=la *)
  apply simp
(* TODOs: CallVarExp *)
apply clarsimp
apply (induct_tac n)
apply (simp add: valid_in_ctxt_def valid_in_ctxt_n_def ctxt_validn_def valid_def validn_def)
(* recursion case *)
apply (rotate_tac -2) apply (erule thin_rl)
apply (simp (no_asm) add: valid_in_ctxt_def valid_in_ctxt_n_def)
apply clarsimp
apply (simp (no_asm) add: valid_def validn_def)
apply clarsimp
apply (erule semexpn.cases)  apply simp_all
(* subcase: ExactApp *)
apply clarsimp
(* apply (erule_tac x="snd (funTab f)" in allE) *)
apply (erule_tac x="f" in allE)
apply clarsimp
apply (rotate_tac -2) apply (erule thin_rl)
apply (erule_tac x="na" in allE)
apply (simp add: valid_in_ctxt_def valid_in_ctxt_n_def)
apply (erule impE)
apply (rule ctxt_lower)
apply simp
apply simp
apply (erule impE)
apply (drule ctxt_lower_suc)
apply (drule ctxt_consn)
apply simp
apply (subgoal_tac "{(CallVarExp xa xsa, P)} \<union> G = insert (CallVarExp xa xsa, P) G")
apply simp
apply simp
apply (erule thin_rl)
apply (simp add: valid_def validn_def)
apply (rotate_tac -1)
apply (erule_tac x="n" in allE)
apply (rotate_tac -1)
apply (erule impE) apply assumption
apply (erule_tac x="E'" in allE)
apply (erule_tac x="ha" in allE)
apply (erule_tac x="h'a" in allE)
apply (erule_tac x="va" in allE)
apply (erule_tac x="pa" in allE)
apply (erule impE) apply assumption
apply (rotate_tac -1)
apply (erule_tac x="Ea" in allE)
apply (rotate_tac -1)
apply (erule impE)
apply (rule_tac x="rs" in exI)
apply (rule conjI)
apply (simp only: preExactApp_def)
apply (rule_tac x="l" in exI)
apply (rule_tac x="i" in exI)
apply (rule conjI)
apply clarsimp
apply clarsimp
apply (assumption)
apply assumption
(* subcase: UnderApp *)
apply clarsimp
apply (erule thin_rl)
apply (rotate_tac 1)
apply (erule thin_rl)
apply (erule thin_rl)
apply (erule_tac x="Ea" in allE)
apply (erule_tac x="ha" in allE)
apply (erule_tac x="(ha(freshloc (fmap_dom ha)\<mapsto>\<^sub>fX f (i + length xsa) (rs @ map (\<lambda>x. theRef (Ea x)) xsa)))" in allE)
apply (erule_tac x="(R (Ref (freshloc (fmap_dom ha))))" in allE)
(* apply (erule_tac x="pa" in allE) *)
apply (erule impE)
apply (simp only: preUnderApp_def)
apply (rule_tac x="l" in exI)
apply (rule_tac x="freshloc (fmap_dom ha)" in exI)
apply (rule_tac x="f" in exI)
apply (rule_tac x="i" in exI)
apply (rule_tac x="rs" in exI)
apply clarsimp
apply (subgoal_tac "funTab f=(as,e)")
apply simp
apply fastsimp
apply assumption
done

text {* 
  Main Soundness theorem 
  Structure of the proof: induction over vdm rules, and induction over n in case of 
  function calls
  (same as for Grail, mapping all Call? cases of GRUMPY to Grail static methods.
*}

theorem "soundness": "G \<rhd> e : P \<Longrightarrow> G \<Turnstile> e : P" 
apply (drule soundnessAux)
apply (rule validn_valid_in_ctxt)
apply (erule_tac x="n" in allE)
apply assumption
done

text {* Finally, soundness in empty contexts. *}

theorem "soundness1": "{} \<rhd> e : P  \<Longrightarrow> {} \<Turnstile> e : P"
apply (insert soundness [of "{}"])
apply (simp add: valid_in_ctxt_def validn_def valid_def) (*  sem_def *)
apply fast
done

text {* Same result in a slightly different flavour, exactly as used in D17 *}

lemma t1: "TESTME G \<Turnstile> e : P \<Longrightarrow> \<forall> n. G \<Turnstile>\<^sub>n e : P"
apply (simp add: testme_def)
apply (simp add: valid_in_ctxt_def valid_in_ctxt_n_def ctxt_validn_def valid_def validn_def)
done

lemma t2: "\<forall> n. G \<Turnstile>\<^sub>n e : P \<Longrightarrow> TESTME G \<Turnstile> e : P"
apply (simp add: testme_def)
apply (simp add: valid_in_ctxt_def valid_in_ctxt_n_def ctxt_validn_def valid_def validn_def)
done

lemma s1: "G \<rhd> e : P \<Longrightarrow> TESTME G \<Turnstile> e : P"
apply (drule soundnessAux)
apply (rule t2)
apply simp
done

theorem "{} \<rhd> e : P  \<Longrightarrow> TESTME {} \<Turnstile> e : P"
apply (insert s1 [of "{}"])
apply (simp add: valid_in_ctxt_def validn_def valid_def testme_def) (*  sem_def *)
apply fast
done

(* collections of lemmas *)

lemmas vdm_basics = vdmValue vdmVar vdmConstr vdmPrimBin vdmIf vdmLet vdmCallFun vdmCallVar vdmCaseOne vdmAx vdmConseq
                    
lemmas vdm_structural = vdmAx vdmConseq

lemmas vdm_calls = vdmCallFun vdmCallVar 

lemmas vdm_pathetic = vdmValue vdmVar vdmConstr vdmPrimBin vdmRPrimBin

text {*
Next steps after proving soundness: design derived assertions, mapping 
resource info on stack, heap and time into this logic.

What we need for the first D is a description of the assertion language, ie.
motivate the usage of Isabelle/HOL and a shallow embedding.
Also, examples showing how resource info is mapped down would be useful.
And a discussion of how GRUMPY maps down to HAM. I started work on a translation
function in Isabelle, but that needs more work. A discussion of such a translation,
covering resources, too, should be sufficient for the D.
*}

text {*
Main things to check:
\begin{itemize}
\item Relationship to high-level types and defunctionalisation-based compilation?
\item Problems because of no distinction btw funame and varname?
\item Examples for: rec h-o. functions, resources
\item Type system for heap allocations
\end{itemize}
*}

end