theory BlahSep imports Word begin

text {* Trivial setup for a typed heap and separating conjunction *}

definition 
  map_disj :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> bool" (infix "\<bottom>" 51) where
  "h\<^isub>0 \<bottom> h\<^isub>1 \<equiv> dom h\<^isub>0 \<inter> dom h\<^isub>1 = {}"

types heap_assert = "(32 word \<rightharpoonup> 8 word) \<Rightarrow> bool"

constdefs sep_true :: "heap_assert"
  "sep_true \<equiv> \<lambda>s. True"

constdefs sep_false :: "heap_assert"
  "sep_false \<equiv> \<lambda>s. False"

constdefs sep_empty :: "heap_assert" ("\<box>")
  "\<box> \<equiv> \<lambda>h. h = empty"

constdefs sep_conj :: "heap_assert \<Rightarrow> heap_assert \<Rightarrow> heap_assert" 
  (infixr "\<and>\<^sup>*" 35)
  "P \<and>\<^sup>* Q \<equiv> \<lambda>h. \<exists>h\<^isub>0 h\<^isub>1. h\<^isub>0 \<bottom> h\<^isub>1 \<and> h = h\<^isub>0 ++ h\<^isub>1 \<and> P h\<^isub>0 \<and> Q h\<^isub>1"

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

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

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

text {* 
  First example: used to be able to use intro: ext without the exclamation
*}
lemma sep_conj_false_right:
  "(P \<and>\<^sup>* sep_false) = sep_false"
  by (force dest: sep_conjD intro!: ext)
  (* NOTE: (auto dest: sep_conjD intro!: ext) also works, but needed
       the exclamation in the past, so that hasn't changed, only force has *)

text {*
  Second example: didn't need any exclamation marks
*}
lemma sep_conj_exists2:
  "(P \<and>\<^sup>* (\<lambda>s. \<exists>x. Q x s)) = (\<lambda>s. (\<exists>x. (P \<and>\<^sup>* Q x) s))"
  by (force intro!: sep_conjI ext dest!: sep_conjD)
  (* NOTE: same as above, auto can be used, but needs exclamations and also
       did in the past, probably why we used force here *)


text {*
  Third example: fact chaining and extra "-"
*}
consts
  delete :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"

lemma sep_conj_foldl_extract:
  assumes fold: "foldl op \<and>\<^sup>* \<box> Ps s"
  assumes inP: "P \<in> set Ps"
  shows "(P \<and>\<^sup>* sep_true) s"
proof -
  let ?rest = "foldl op \<and>\<^sup>* \<box> (delete P Ps)"

  have notnil: "Ps \<noteq> []" using inP by auto

  have rewrite:
    "(foldl op \<and>\<^sup>* \<box> Ps) = (P \<and>\<^sup>* ?rest)" using notnil inP
  proof (induct Ps arbitrary: P)
    case Nil thus ?case by simp
  next
    case (Cons x xs)
    hence IH: "\<lbrakk> xs \<noteq> [] ; P \<in> set xs \<rbrakk> \<Longrightarrow> (foldl op \<and>\<^sup>* \<box> xs) = (P \<and>\<^sup>* foldl op \<and>\<^sup>* \<box> (delete P xs))" 
      and in': "P \<in> set (x # xs)"

    (* These work, and work in slightly-pre-2009:
      by - assumption
      by - simp
      by - blast
      by auto      
    *)
    (* And these do not work, but used to:
      by simp
      by blast
    *)
    (* However, in the old version I'm getting "Legacy feature! Implicit use of prems in assumption proof", so I guess there's my answer. 
       Not sure what's the proper way to write these now.
    *)
 
    by - assumption
  oops