theory DummyExpr
imports GRUMPY
begin

section {* Dummy expressions *}

text {*
Several wee examples showing how to use the expression-level logic
to prove properties about boxes. This serves to settle the interface
between the box-level and the expression-level logic for Hume.
*}

subsection {* A specification of a box as used on box-level *}

text {* GG's version *}

consts
  incbox_GG :: "nat option \<Rightarrow> bool \<times> (nat option)"

primrec
 "incbox_GG None = (False,None)"
 "incbox_GG (Some a) = (True,Some (a+1))"


(* Integration using operational semantics directly!!! *)


consts exe :: "Env \<Rightarrow> Heap \<Rightarrow> Exp \<Rightarrow> (HoVal \<times> Heap \<times> Rescomp)"

axioms
 exe: "(exe E h e = (v,h',p)) = (E, h \<turnstile> e \<Down> (v,h',p))"

lemma vdmexe: "\<lbrakk>(v,h',p) = exe E h e; {} \<rhd> e : P\<rbrakk> 
  \<Longrightarrow> P E h h' v p"
proof -
  assume a1: "{} \<rhd> e : P"
    and  a2: "(v,h',p) = exe E h e"
  have "{} \<rhd> e : P \<Longrightarrow> {} \<Turnstile> e : P" by (rule soundness)
  with a1 have g1: "{} \<Turnstile> e : P" by simp
  have g1': "|\<Turnstile> {}" by (auto simp add: ctxt_valid_def)
  with g1 g1' have g1'': "\<Turnstile> e:P" 
    by (auto simp add: valid_in_ctxt_def)
   hence G: "(\<forall> E h h' v p . ((E, h \<turnstile> e \<Down> (v,h',p)) \<longrightarrow> P E h h' v p))"
     by (unfold valid_def)
  from a2 exe[symmetric] have g2: "E, h \<turnstile> e \<Down> (v,h',p)"
    by auto
  with G show ?thesis by auto
qed

subsection {* The body of the box *}

syntax 
 x1  :: "VarName"
 x2  :: "VarName"
 x3  :: "VarName"
 xin :: "VarName"
translations
"x1" == "(VN ''x1'')"
"x2" == "(VN ''x2'')"
"x3" == "(VN ''x3'')"
"xin" == "(VN ''xin'')"

constdefs iplus :: "HoVal => HoVal => HoVal"
"iplus x y == I ((theInt x)+(theInt y))"
constdefs iinc :: "HoVal => HoVal => HoVal"
"iinc x y == I ((theInt x)+(1::int))"

text {* Just the RHS of the body *}

constdefs incbody0 :: "Exp"
"incbody0 == (PrimBin iinc xin xin)"

(*
lemma "{} \<rhd> VarExp xin : (\<lambda> E h hh v p. (\<forall> i r . (E xin = (R (Ref r))  \<longrightarrow> v = (R (Ref r)))))"
apply (rule vdmConseq)
prefer 2
apply (rule vdmVar)
apply clarsimp
done
*)

text {* Prove specification, in form of an Assertion, for the body of incbox *}

lemma ib0: "{} \<rhd> incbody0 : (\<lambda> E h hh v p. (\<forall> i r . (E xin = (I i))  \<longrightarrow> v = (I (i+1))))"
apply (simp add: incbody0_def)
thm vdmConseq
apply (rule vdmConseq)
prefer 2
apply (rule vdmPrimBin)
apply clarsimp
apply (simp add: iinc_def)
done

lemma assumes a1: "(v,h',p) = exe E h incbody0"
  shows "(\<forall> i r . (E xin = (I i))  \<longrightarrow> v = (I (i+1)))"
using a1 ib0 by (rule vdmexe)

text {* HWL's version of the specification; input hardwired to xin; phps use funTab to capture binding of input to variable *}

constdefs
  incbox_HWL :: "HoVal option \<Rightarrow> bool \<times> Assertion"
 "incbox_HWL v0 == (case v0 of
                      None \<Rightarrow> (False,\<lambda> E h hh v p. False)
                    | (Some (a::HoVal)) \<Rightarrow> (True, (\<lambda> E h hh v p. (\<forall> i r . (E xin = (R (Ref r)) \<and> (fmap_lookup h r = Some a) \<and> a = (I i))  \<longrightarrow> v = (I (i+1))))))"



text {* Full body, including a pattern match against a variable *}

constdefs incbody :: "Exp"
"incbody == CaseOneExp xin (PVar x1) (RPrimBin iinc x1 x1) (ValueExp BOTTOM)"

theorem incbody_spec: "{} \<rhd> incbody : (\<lambda> E h hh v p. 
  (\<forall> i r . (E xin = (R (Ref r)) \<and> (fmap_lookup h r = Some (I i)))  \<longrightarrow> v = (I (i+1))))"
apply (simp add: incbody_def)
apply (rule vdmConseq)
prefer 2
apply (rule vdmCaseOne)
apply (rule vdmRPrimBin)
apply (rule vdmValue)
apply clarsimp
apply (erule_tac x="E(x1:=(R (Ref r)))" in allE)
apply (erule_tac x="R (Ref r)" in allE)
apply clarsimp
apply (erule impE)
apply (rule semPVar)
apply (simp add: iinc_def)
done

consts va :: "HoVal"

lemma "{} \<rhd> incbody : (snd (incbox_HWL (Some va)))"
apply (simp add: incbox_HWL_def)
apply (rule vdmConseq)
prefer 2
apply (insert  incbody_spec)
apply simp
apply clarsimp
done

text {* Function call version *}

syntax inc_fct :: "FunName"
translations
 "inc_fct" == "(FN ''inc_fct'')"

axioms fff:
 "funTab inc_fct = ((xin#[]), incbody)"
(*                   params    body of the fct *)

theorem inccall_spec: "{} \<rhd> (CallFunExp inc_fct (x2#[])) : (\<lambda> E h hh v p. (\<forall> i r . (E x2 = (R (Ref r)) \<and> (fmap_lookup h r = Some (I i)))  \<longrightarrow> v = (I (i+1))))"
apply (rule vdmConseq)
prefer 2
apply (rule vdmCallFun)
apply (simp add: fff)
(* todo: parameter passing, then use theorem above  *)
oops

text {* This version uses an unary evaluation function over ints; otw same as above *}

constdefs mkAss :: "VarName \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> Assertion"
"mkAss x f == \<lambda> E h hh v p. (\<forall> i r . (E x = (R (Ref r)) \<and> (fmap_lookup h r = Some (I i)))  \<longrightarrow> v = (I (f i)))"

lemma "{} \<rhd> incbody : mkAss xin (\<lambda> i . i+1)"
apply (insert  incbody_spec)
apply (simp add: mkAss_def)
done

end