Theory Sep_Algebra_Add

theory Sep_Algebra_Add
  imports "Separation_Algebra.Separation_Algebra" "Separation_Algebra.Sep_Heap_Instance"
    Product_Separation_Algebra
begin

definition puree :: "bool ⇒ 'h::sep_algebra ⇒ bool" (‹↑›) where "puree P ≡ λh. h=0 ∧ P"

lemma puree_alt: "↑Φ = (⟨Φ⟩ and □)"
  by (auto simp: puree_def sep_empty_def)

lemma pure_alt: "⟨Φ⟩ = (↑Φ ** sep_true)"
  apply (clarsimp simp: puree_def)
proof -
  { fix aa :: 'a
    obtain aaa :: "('a ⇒ bool) ⇒ ('a ⇒ bool) ⇒ 'a" where
      ff1: "⋀p pa a pb pc aa. (¬ (p ∧* pa) a ∨ p (aaa p pb) ∨ (pb ∧*
pa) a) ∧ (¬ pb (aaa p pb) ∨ ¬ (p ∧* pc) aa ∨ (pb ∧* pc) aa)"
      by (metis (no_types) sep_globalise)
    then have "∃p. ((λa. a = 0) ∧* p) aa"
      by (metis (full_types) sep_conj_commuteI sep_conj_sep_emptyE
sep_empty_def)
    then have "¬ Φ ∨ Φ ∧ ((λa. a = 0) ∧* (λa. True)) aa"
      using ff1 by (metis (no_types) sep_conj_commuteI) }
  then show "(λa. Φ) = (λa. Φ ∧ ((λa. (a::'a) = 0) ∧* (λa. True)) a)"
    by blast
qed
  
abbreviation NO_PURE :: "bool ⇒ ('h::sep_algebra ⇒ bool) ⇒ bool" 
  where "NO_PURE X Q ≡ (NO_MATCH (⟨X⟩::'h⇒bool) Q ∧ NO_MATCH ((↑X)::'h⇒bool) Q)"

named_theorems sep_simplify ‹Assertion simplifications›

lemma sep_reorder[sep_simplify]:  
  "((a ∧* b) ∧* c) = (a ∧* b ∧* c)"
  "(NO_PURE X a) ⟹ (a ** b) = (b ** a)"
  "(NO_PURE X b) ⟹ (b ∧* a ∧* c) = (a ∧* b ∧* c)"
  "(Q ** ⟨P⟩) = (⟨P⟩ ** Q)"
  "(Q ** ↑P) = (↑P ** Q)"
  "NO_PURE X Q ⟹ (Q ** ⟨P⟩ ** F) = (⟨P⟩ ** Q ** F)"
  "NO_PURE X Q ⟹ (Q ** ↑P ** F) = (↑P ** Q ** F)"
  by (simp_all add: sep.add_ac)

lemma sep_combine1[simp]:
  "(↑P ** ↑Q) = ↑(P∧Q)"
  "(⟨P⟩ ** ⟨Q⟩) = ⟨P∧Q⟩"
  "(↑P ** ⟨Q⟩) = ⟨P∧Q⟩"
  "(⟨P⟩ ** ↑Q) = ⟨P∧Q⟩"
  apply (auto simp add: sep_conj_def puree_def intro!: ext)
  apply (rule_tac x=0 in exI)
  apply simp
  done

lemma sep_combine2[simp]:
  "(↑P ** ↑Q ** F) = (↑(P∧Q) ** F)"
  "(⟨P⟩ ** ⟨Q⟩ ** F) = (⟨P∧Q⟩ ** F)"
  "(↑P ** ⟨Q⟩ ** F) = (⟨P∧Q⟩ ** F)"
  "(⟨P⟩ ** ↑Q ** F) = (⟨P∧Q⟩ ** F)"
  apply (subst sep.add_assoc[symmetric]; simp)+
  done

lemma sep_extract_pure[simp]:
  "NO_MATCH True P ⟹ (⟨P⟩ ** Q) h = (P ∧ (sep_true ** Q) h)"
  "(↑P ** Q) h = (P ∧ Q h)"
  "↑True = □"
  "↑False = sep_false"
  using sep_conj_sep_true_right apply fastforce
  by (auto simp: puree_def sep_empty_def[symmetric])

lemma sep_pure_front2[simp]: 
  "(↑P ** A ** ↑Q ** F) = (↑(P ∧ Q) ** F ** A)"
  apply (simp add: sep_reorder)
  done

lemma ex_h_simps[simp]: 
  "Ex (↑Φ) ⟷ Φ"
  "Ex (↑Φ ** P) ⟷ (Φ ∧ Ex P)"
  apply (cases Φ; auto)
  apply auto
  done
  
lemma
  fixes h :: "('a ⇒ 'b option) * nat"
  shows "(P ** Q ** H) h = (Q ** H ** P) h"
  by (simp add: sep_conj_ac)
    
(* map_le *)
lemma map_le_substate_conv: "map_le = sep_substate"
  unfolding map_le_def sep_substate_def sep_disj_fun_def plus_fun_def domain_def dom_def none_def apply (auto intro!: ext)
  subgoal for m1 m2 apply(rule exI[where x="%x. if (∃y. m1 x = Some y) then None else m2 x"])
    by auto
  by blast


end