theory Sep imports HoareAbort MapExtra 
begin

text {* Define the heap *}

types heap = "(nat \<Rightarrow> nat option)"

text {* The semantic definition of a few connectives: *}

constdefs
  sep_emp :: "heap \<Rightarrow> bool" ("\<box>")
  "sep_emp h == h = empty"
constdefs
  singl :: "nat \<Rightarrow> nat \<Rightarrow> heap \<Rightarrow> bool" ("_ \<mapsto> _" [56] 56)
  "singl x y h == dom h = {x} & h x = Some y"
constdefs
  sep_conj :: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)" 
    (infixr "\<and>\<^sup>*" 35)
  "sep_conj P Q == \<lambda>h. \<exists>h1 h2. h = h1 ++ h2 \<and> h1 \<bottom> h2 \<and> P h1 \<and> Q h2"
constdefs
  sep_impl :: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)" (infixr "\<longrightarrow>\<^sup>*" 25)
  "sep_impl P Q == \<lambda>h. \<forall>h'. h' \<bottom> h \<and> P h' \<longrightarrow> Q(h++h')"
constdefs 
  "sep_true \<equiv> \<lambda>s. True"
constdefs 
  "sep_false \<equiv> \<lambda>s. False"


text {* Simple test *}

lemma "VARS x y z w h
  {sep_conj (singl x y) (singl z w) h}
   SKIP
  {x \<noteq> z}"
  apply vcg
  apply(auto simp:sep_conj_def map_disj_def singl_def)
  done

lemma "VARS H x y z w
 {(x \<mapsto> y \<and>\<^sup>* z \<mapsto> w) H}
 y := w
 {x \<noteq> z}"
apply vcg
apply (unfold sep_conj_def)
apply clarsimp
apply (clarsimp simp: map_disj_def singl_def)
done

lemma "VARS H x y z w
 {(x \<mapsto> 3) H}
 H := H(x \<mapsto> 4)
 {(x \<mapsto> 4) H}"
apply vcg
apply (unfold singl_def)
apply simp
done

text {* Rules of separation logic *}

lemma sep_empD:
  "\<box> s \<Longrightarrow> s = empty"
  by (simp add: sep_emp_def)

lemma sep_emp_empty [simp]:
  "\<box> empty"
  by (simp add: sep_emp_def)

lemma sep_true [simp]:
  "sep_true s"
  by (simp add: sep_true_def)

lemma sep_false [simp]:
  "\<not> sep_false s"
  by (simp add: sep_false_def)

declare sep_false_def [symmetric, simp add]

lemma sep_conjI:
  "\<lbrakk> P s\<^isub>0; Q s\<^isub>1; s\<^isub>0 \<bottom> s\<^isub>1; s = s\<^isub>1 ++ s\<^isub>0 \<rbrakk> \<Longrightarrow> (P \<and>\<^sup>* Q) s"
  by (force simp: sep_conj_def map_add_ac)

lemma sep_conjD:
  "(P \<and>\<^sup>* Q) s \<Longrightarrow> \<exists>s\<^isub>0 s\<^isub>1. s\<^isub>0 \<bottom> s\<^isub>1 \<and> s = s\<^isub>1 ++ s\<^isub>0 \<and> P s\<^isub>0 \<and> Q s\<^isub>1"
  by (force simp: sep_conj_def map_add_ac)

(* a law of separation logic *)
lemma star_comm: "(P \<and>\<^sup>* Q) = (Q \<and>\<^sup>* P)"
  apply (rule ext)
  apply (rule iffI)
   apply (drule sep_conjD)
   apply clarsimp
   apply (rule sep_conjI)
      apply assumption
     apply assumption
    apply (simp add: map_disj_com)
   apply (simp add: map_add_ac)
  apply (drule sep_conjD)
  apply clarsimp
  apply (rule sep_conjI)
    apply assumption
    apply assumption
   apply (simp add: map_disj_com)
  apply (simp add: map_add_ac)
  done

lemma "VARS H x y z w
 {(P \<and>\<^sup>* Q) H}
 SKIP
 {(Q \<and>\<^sup>* P) H}"
apply (simp add: star_comm)
apply vcg
done

end
