theory SepList imports Sep
begin

abbreviation
  NULL :: nat where
  "NULL \<equiv> 0"

consts
  List :: "nat list \<Rightarrow> nat \<Rightarrow> heap \<Rightarrow> bool"

primrec
  "List [] p h = (p = NULL \<and> sep_emp h)"
  "List (x#xs) p h = (p \<noteq> NULL \<and> p = x \<and> (\<exists>q. (p \<mapsto> q \<and>\<^sup>* List xs q) h))"

lemma list_empty [simp]:
  shows "List xs NULL = (\<lambda>s. xs = [] \<and> \<box> s)"
  apply (cases xs)
   apply (rule ext, clarsimp)
  apply clarsimp
  apply (rule ext)
  apply clarsimp
  done

text {* Prepending to a list *}
lemma "VARS H
  {p \<noteq> NULL \<and> (p \<mapsto> x \<and>\<^sup>* List qs q) H}
  H := H(p \<mapsto> q)
  {List (p#qs) p H}"
  apply vcg
  apply clarsimp
  apply (rule_tac x=q in exI)
  apply (drule sep_conjD)
  apply clarsimp
  apply (rule_tac s\<^isub>0="s\<^isub>0(p \<mapsto> q)" in sep_conjI)
     prefer 2
     apply assumption
    apply (simp add: singl_def)
   apply (simp add: map_disj_def singl_def)
  apply (simp add: map_add_ac)
  done

end