Theory AutoCorres2.Separation_UMM

(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 * Copyright (c) 2022 Apple Inc. All rights reserved.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)


theory Separation_UMM
imports TypHeap
begin

(* The store is not captured explicitly, variable values may appear in
   predicates and do not require special treatment *)
type_synonym ('a,'b) map_assert = "('a  'b)  bool"
type_synonym heap_assert = "(addr × s_heap_index,s_heap_value) map_assert"

definition sep_emp :: "('a,'b) map_assert" ("") where
  "sep_emp  (=) Map.empty"

definition sep_true :: "('a,'b) map_assert" where
  "sep_true  λs. True"

definition sep_false :: "('a,'b) map_assert" where
  "sep_false  λs. False"

definition
  sep_conj :: "('a,'b) map_assert  ('a,'b) map_assert  ('a,'b) map_assert" (infixr "*" 35)
where
  "P * Q  λs. s0 s1. s0  s1  s = s1 ++ s0  P s0  Q s1"

definition
  sep_impl :: "('a,'b) map_assert  ('a,'b) map_assert  ('a,'b) map_assert" (infixr "*" 25)
where
  "x * y  λs. s'. s  s'  x s'  y (s ++ s')"


definition
  singleton :: "'a::c_type ptr  'a  heap_mem  heap_typ_desc  heap_state"
where
  "singleton p v h d  lift_state (heap_update p v h,d) |` s_footprint p"

text ‹
  Like in Separation.thy, these arrows are defined using bsub and esub but
  have an \emph{input} syntax abbreviation with just sub.
  Why? Because if sub is the only way, people write things like
  @{text "p ↦i(f x y) v"} instead of @{text "p ↦i(f x y) v"}. We preserve
  the sub syntax though, because esub and bsub are a pain to type.
›

definition
  sep_map :: "'a::c_type ptr  'a ptr_guard  'a  heap_assert" ("_ ↦⇘_ _" [56,0,51] 56)
where
  "p ↦⇘gv  λs. lift_typ_heap g s p = Some v  dom s = s_footprint p  wf_heap_val s"

notation (input)
  sep_map ("_ ↦⇩_ _" [56,1000,51] 56)

definition
  sep_map_any :: "'a ::c_type ptr  'a ptr_guard  heap_assert" ("_ ↦⇘_ -" [56,0] 56)
where
  "p ↦⇘g-  λs. v. (p ↦⇩g v) s"

notation (input)
  sep_map_any ("_ ↦⇩_ -" [56,0] 56)

definition
  sep_map' :: "'a::c_type ptr  'a ptr_guard  'a  heap_assert" ("_ ↪⇘_ _" [56,0,51] 56)
where
  "p ↪⇘gv  (p ↦⇘gv) * sep_true"

notation (input)
  sep_map' ("_ ↪⇩_ _" [56,1000,51] 56)

definition
  sep_map'_any :: "'a ::c_type ptr  'a ptr_guard   heap_assert" ("_ ↪⇘_ -" [56,0] 56)
where
  "p ↪⇘g-  λs. x. (p ↪⇩g x) s"

notation (input)
  sep_map'_any ("_ ↪⇩_ -" [56,0] 56)

syntax
  "_sep_assert" :: "bool  heap_state  bool" ("'(_')sep" [0] 100)


text ‹----›

lemma sep_empD:
  " s  s = Map.empty"
  by (simp add: sep_emp_def)

lemma sep_emp_empty [simp]:
  " Map.empty"
  by (simp add: sep_emp_def)

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

lemma sep_false [simp]:
  "¬ sep_false s"
  by (simp add: sep_false_def)

declare sep_false_def [symmetric, simp add]

lemma singleton_dom':
  "dom (singleton p (v::'a::mem_type) h d) = dom (lift_state (h,d))  s_footprint p"
  by (auto simp: singleton_def lift_state_def
           split: if_split_asm s_heap_index.splits)

lemma lift_state_dom:
  "d,g t p  s_footprint (p::'a::mem_type ptr)  dom (lift_state (h,d))"
  supply unsigned_of_nat [simp del]
  apply(clarsimp simp: h_t_valid_def valid_footprint_def Let_def)
  apply(clarsimp simp: lift_state_def split: s_heap_index.splits option.splits)
  apply(rule conjI; clarsimp)
   apply(fastforce dest: s_footprintD intvlD simp: size_of_def)
  apply(frule s_footprintD2)
  apply(drule s_footprintD)
  apply(drule intvlD, clarsimp)
  apply(rename_tac k)
  apply(drule_tac x=k in spec)
  apply(erule impE)
   apply(simp add: size_of_def)
  apply(subst (asm) word_unat.eq_norm)
  apply(subst (asm) mod_less)
   apply(subst len_of_addr_card)
   apply(erule less_trans)
   apply(rule max_size)
  apply(force simp: map_le_def)
  done

lemma singleton_dom:
  "d,g t p  dom (singleton p (v::'a::mem_type) h d) = s_footprint p"
  apply(subst singleton_dom')
  apply(fastforce dest: lift_state_dom)
  done

lemma wf_heap_val_restrict [simp]:
  "wf_heap_val s  wf_heap_val (s |` X)"
  unfolding wf_heap_val_def by (auto simp: restrict_map_def)

lemma singleton_wf_heap_val [simp]:
  "wf_heap_val (singleton p v h d)"
  unfolding singleton_def by simp

lemma h_t_valid_restrict_proj_d:
  " proj_d s,g t p; x. x  s_footprint p  s x = s' x  
      proj_d s',g t p"
  apply(clarsimp simp: h_t_valid_def valid_footprint_def Let_def)
  apply(rule conjI)
   apply(drule_tac x=y in spec)
   apply simp
   apply(clarsimp simp: proj_d_def map_le_def)
   apply(drule_tac x="ptr_val p + of_nat y" in spec)
   apply(drule_tac x="SIndexTyp a" in spec)
   apply(erule impE)
    apply(erule s_footprintI)
    apply(simp add: size_of_def)
   apply simp
  apply(clarsimp simp: proj_d_def)
  apply(drule_tac x=y in spec)
  apply clarsimp
  apply(drule_tac x="ptr_val p + of_nat y" in spec)
  apply(drule_tac x="SIndexVal" in spec)
  apply(erule impE)
   apply(rule s_footprintI2)
   apply(simp add: size_of_def)
  apply force
  done

lemma s_valid_restrict [simp]:
  "s |` s_footprint p,g s p = s,g s p"
  by (fastforce simp: s_valid_def elim: h_t_valid_restrict_proj_d)

lemma proj_h_restrict:
  "(x,SIndexVal)  X  proj_h (s |` X) x = proj_h s x"
  by (auto simp: proj_h_def)

lemma heap_list_s_restrict:
  "(λx. (x,SIndexVal)) ` {p..+n}  X  heap_list_s (s |` X) n p = heap_list_s s n p"
  apply(induct n arbitrary: p)
   apply(simp add: heap_list_s_def)
  apply(clarsimp simp: heap_list_s_def)
  apply(rule conjI)
   apply(fastforce intro: proj_h_restrict intvl_self)
  apply(fastforce intro: intvl_plus_sub_Suc)
  done

lemma lift_typ_heap_restrict [simp]:
  "lift_typ_heap g (s |` s_footprint p) p = lift_typ_heap g s p"
  apply(clarsimp simp: lift_typ_heap_if)
  apply(subst heap_list_s_restrict)
   apply clarsimp
   apply(drule intvlD, clarsimp)
   apply(erule s_footprintI2)
  apply simp
  done

lemma singleton_s_valid:
  "d,g t p  singleton p (v::'a::mem_type) h d,g s p"
  by (simp add: singleton_def h_t_s_valid)

lemma singleton_lift_typ_heap_Some:
  "d,g t p  lift_typ_heap g (singleton p v h d) p = Some (v::'a::mem_type)"
  by (simp add: singleton_def lift_t lift_t_heap_update h_t_valid_restrict)

lemma sep_map_g:
  "(p ↦⇩g v) s  g p"
  by (force simp: sep_map_def dest: lift_typ_heap_g)

lemma sep_map_g_sep_false:
  "¬ g p  (p ↦⇩g v) = sep_false"
  by (simp add: sep_map_def lift_typ_heap_if s_valid_def h_t_valid_def)

lemma sep_map_singleton:
  "d,g t p  ((p::'a::mem_type ptr) ↦⇩g v) (singleton p v h d)"
  by (simp add: sep_map_def singleton_lift_typ_heap_Some singleton_dom)

lemma sep_mapD:
  "(p ↦⇩g v) s  lift_typ_heap g s p = Some v 
      dom s = s_footprint p  wf_heap_val s"
  by (simp add: sep_map_def)

lemma sep_map_lift_typ_heapD:
  "(p ↦⇩g v) s  lift_typ_heap g s p = Some (v::'a::c_type)"
  by (simp add: sep_map_def)

lemma sep_map_dom_exc:
  "(p ↦⇩g (v::'a::c_type)) s  dom s = s_footprint p"
  by (simp add: sep_map_def)

lemma sep_map_inj:
  " (p ↦⇩g (v::'a::c_type)) s; (p ↦⇩h v') s   v = v'"
  by (clarsimp simp: sep_map_def lift_typ_heap_if split: if_split_asm)

lemma sep_map_anyI_exc [simp]:
  "(p ↦⇩g v) s  (p ↦⇩g -) s"
  by (force simp: sep_map_any_def)

lemma sep_map_anyD_exc:
  "(p ↦⇩g -) s  v. (p ↦⇩g v) s"
  by (force simp: sep_map_any_def)

lemma sep_map_any_singleton:
  "d,g t i  (i ↦⇩g -) (singleton i (v::'a::mem_type) h d)"
  by (unfold sep_map_any_def, rule exI [where x=v], erule sep_map_singleton)

lemma proj_h_heap_merge:
  "proj_h (s ++ t) = (λx. if (x,SIndexVal)   dom t then proj_h t x else proj_h s x)"
  by (force simp: proj_h_def split: option.splits)

lemma s_valid_heap_merge_right:
  "s1,g s p  s0 ++ s1,g s p"
  apply (clarsimp simp: s_valid_def h_t_valid_def valid_footprint_def Let_def)
  apply (rule conjI)
   apply(drule_tac x=y in spec, simp)
   apply clarsimp
   apply(erule map_le_trans)
   apply(clarsimp simp: proj_d_def map_le_def split: option.splits)
  apply(drule_tac x=y in spec, simp)
  apply(clarsimp simp: proj_d_def map_le_def split: option.splits)
  done

lemma proj_d_map_add_fst:
  "fst (proj_d (s ++ t) x) = (if (x,SIndexVal)  dom t then fst (proj_d t x) else
      fst (proj_d s x))"
  by (auto simp: proj_d_def split: option.splits)

lemma proj_d_map_add_snd:
  "snd (proj_d (s ++ t) x) n = (if (x,SIndexTyp n)  dom t then snd (proj_d t x) n else
      snd (proj_d s x) n)"
  by (auto simp: proj_d_def split: option.splits)

lemma proj_d_restrict_map_fst:
  "(x,SIndexVal)  X  fst (proj_d (s |` X) x) = fst (proj_d s x)"
  by (auto simp: proj_d_def)

lemma proj_d_restrict_map_snd:
  "(x,SIndexTyp n)  X  snd (proj_d (s |` X) x) n = snd (proj_d s x) n"
  by (auto simp: proj_d_def)

lemma s_valid_heap_merge_right2:
  " s0 ++ s1,g s p; s_footprint p  dom s1   s1,g s p"
  apply(clarsimp simp: s_valid_def h_t_valid_def valid_footprint_def Let_def)
  apply(rule conjI)
   apply(clarsimp simp: map_le_def)
   apply(subst proj_d_map_add_snd)
   apply(clarsimp split: if_split_asm)
   apply(subgoal_tac "(ptr_val p + of_nat y,SIndexTyp a)  s_footprint p")
    apply fast
   apply(erule s_footprintI)
   apply(simp add: size_of_def)
  apply(subgoal_tac "(ptr_val p + of_nat y,SIndexVal)  s_footprint p")
   apply(drule (1) subsetD)
   apply clarsimp
   apply(subst (asm) proj_d_map_add_fst)
   apply(drule_tac x=y in spec)
   apply(clarsimp split: if_split_asm)
  apply(rule s_footprintI2)
  apply(simp add: size_of_def)
  done

lemma heap_list_s_heap_merge_right':
  " s1,g s (p::'a::c_type ptr); n  size_of TYPE('a)  
      heap_list_s (s0 ++ s1) n (ptr_val p + of_nat (size_of TYPE('a) - n))
          = heap_list_s s1 n (ptr_val p + of_nat (size_of TYPE('a) - n))"
proof (induct n)
  case 0 thus ?case by (simp add: heap_list_s_def)
next
  case (Suc n)
  hence "(ptr_val p + (of_nat (size_of TYPE('a) - Suc n)),SIndexVal)  dom s1"
    by - (drule_tac x="size_of TYPE('a) - Suc n" in s_valid_Some, auto)
  with Suc show ?case
    by (simp add: heap_list_s_def proj_h_heap_merge algebra_simps)
qed

lemma heap_list_s_heap_merge_right:
  "s1,g s ((Ptr p)::'a::c_type ptr) 
   heap_list_s (s0 ++ s1) (size_of TYPE('a)) p = heap_list_s s1 (size_of TYPE('a)) p"
  by (force dest: heap_list_s_heap_merge_right')

lemma lift_typ_heap_heap_merge_right:
  "lift_typ_heap g s1 p = Some v  lift_typ_heap g (s0 ++ s1) (p::'a::c_type ptr) = Some v"
  by (force simp: lift_typ_heap_if s_valid_heap_merge_right heap_list_s_heap_merge_right
            split: if_split_asm)

lemma lift_typ_heap_heap_merge_sep_map:
  "(p ↦⇩g v) s1  lift_typ_heap g (s0 ++ s1) p = Some (v::'a::c_type)"
  by (drule sep_map_lift_typ_heapD, erule lift_typ_heap_heap_merge_right)

lemma sep_conjI:
  " P s0; Q s1; s0  s1; s = s1 ++ s0   (P * Q) s"
  by (force simp: sep_conj_def)

lemma sep_conjD:
  "(P * Q) s  s0 s1. s0  s1  s = s1 ++ s0  P s0  Q s1"
  by (force simp: sep_conj_def)

lemma sep_map'I:
  "((p ↦⇩g v) * sep_true) s  (p ↪⇩g v) s"
  by (simp add: sep_map'_def)

lemma sep_map'D:
  "(p ↪⇩g v) s  ((p ↦⇩g v) * sep_true) s"
  by (simp add: sep_map'_def)

lemma sep_map'_g_exc:
  "(p ↪⇩g v) s  g p"
  by (force simp add: sep_map'_def dest: sep_conjD sep_map_g)

lemma sep_conj_sep_true:
  "P s  (P * sep_true) s"
  by (erule_tac s1=Map.empty in sep_conjI, simp+)

lemma sep_map_sep_map'_exc [simp]:
  "(p ↦⇩g v) s  (p ↪⇩g v) s"
  by (unfold sep_map'_def, erule sep_conj_sep_true)

lemma sep_conj_true [simp]:
  "(sep_true * sep_true) = sep_true"
  apply (rule ext) 
  subgoal for x
    apply simp
    apply (rule sep_conjI [where s0=x and s1=Map.empty])
       apply auto
    done
  done

lemma sep_conj_assocD:
  assumes l: "((P * Q) * R) s"
  shows "(P * (Q * R)) s"
proof -
  from l obtain s' s2 where disj_o: "s'  s2" and merge_o: "s = s2 ++ s'" and
    l_o: "(P * Q) s'" and r_o: "R s2" by (force dest: sep_conjD)
  then obtain s0 s1 where disj_i: "s0  s1" and merge_i: "s' = s1 ++ s0" and
    l_i: "P s0" and r_i: "Q s1" by (force dest: sep_conjD)
  from disj_o disj_i merge_i have disj_i': "s1  s2"
    by (force simp: map_ac_simps)
  with r_i and r_o have r_o': "(Q * R) (s2 ++ s1)" by (fast intro: sep_conjI)
  from disj_o merge_i disj_i disj_i' have "s0  s2 ++ s1"
    by (force simp: map_ac_simps)
  with r_o' l_i have "(P * (Q * R)) ((s2 ++ s1) ++ s0)"
    by (force intro: sep_conjI)
  moreover from merge_o merge_i disj_i disj_i' have "s = ((s2 ++ s1) ++ s0)"
    by (simp add: map_add_assoc [symmetric])
  ultimately show ?thesis by simp
qed

(* Reynolds' properties from "Separation Logic: A Logic for Shared
   Mutable Data Structures", page 5-6.  *)

lemma sep_conj_com:
  "(P * Q) = (Q * P)"
  by (rule ext) (auto simp: map_ac_simps sep_conjI dest!: sep_conjD)

lemma sep_conj_false_right [simp]:
  "(P * sep_false) = sep_false"
  by (force dest: sep_conjD)

lemma sep_conj_false_left [simp]:
  "(sep_false * P) = sep_false"
  by (simp add: sep_conj_com)

lemma sep_conj_comD:
  "(P * Q) s  (Q * P) s"
  by (simp add: sep_conj_com)

(* fixme: the need for this kind of special case should disappear with
   generalised separation conjunction *)
lemma exists_left:
  "(Q * (λs. x. P x s)) = ((λs. x. P x s) * Q)" by (simp add: sep_conj_com)

lemma sep_conj_assoc:
  "((P * Q) * R) = (P * (Q * R))" (is "?x = ?y")
proof (rule ext, standard)
  fix s
  assume "?x s"
  thus "?y s" by - (erule sep_conj_assocD)
next
  fix s
  assume "?y s"
  hence "((R * Q) * P) s" by (simp add: sep_conj_com)
  hence "(R * (Q * P)) s" by - (erule sep_conj_assocD)
  thus "?x s" by (simp add: sep_conj_com)
qed

(* For permutative rewriting *)
lemma sep_conj_left_com:
  "(P * (Q * R)) = (Q * (P * R))" (is "?x = ?y")
proof -
  have "?x = ((Q * R) * P)" by (simp add: sep_conj_com)
  also have " = (Q * (R * P))" by (subst sep_conj_assoc, simp)
  finally show ?thesis by (simp add: sep_conj_com)
qed

lemmas sep_conj_ac = sep_conj_com sep_conj_assoc sep_conj_left_com

lemma sep_conj_empty:
  "(P * ) = P"
proof (rule ext, standard)
  fix x
  assume "(P * ) x"
  thus "P x" by (force simp: sep_emp_def dest: sep_conjD)
next
  fix x
  assume "P x"
  moreover have " Map.empty" by simp
  ultimately show "(P * ) x" by - (erule (1) sep_conjI, auto)
qed

lemma sep_conj_empty' [simp]:
  "( * P) = P"
 by (simp add: sep_conj_empty sep_conj_ac)

lemma sep_conj_true_P [simp]:
  "(sep_true * (sep_true * P)) = (sep_true * P)"
  by (simp add: sep_conj_ac)

lemma sep_map'_unfold_exc:
  "(p ↪⇩g v) = ((p ↪⇩g v) * sep_true)"
  by (simp add: sep_map'_def sep_conj_ac)

lemma sep_conj_disj:
  "((λs. P s  Q s) * R) s = ((P * R) s  (Q * R) s)" (is "?x = (?y  ?z)")
proof 
  assume ?x
  then obtain s0 s1 where "s0  s1" and "s = s1 ++ s0" and "P s0  Q s0" and
      "R s1"
    by - (drule sep_conjD, auto)
  moreover from this have "¬ ?z  ¬ Q s0"
    by - (clarsimp, erule notE, erule (2) sep_conjI, simp)
  ultimately show "?y  ?z" by (force intro: sep_conjI)
next
  have "?y  ?x"
    by (force simp: map_ac_simps intro: sep_conjI dest: sep_conjD)
  moreover have "?z  ?x"
    by (force simp: map_ac_simps intro: sep_conjI dest: sep_conjD)
  moreover assume "?y  ?z"
  ultimately show ?x by fast
qed

lemma sep_conj_conj:
  "((λs. P s  Q s) * R) s  (P * R) s  (Q * R) s"
  by (force intro: sep_conjI dest!: sep_conjD)

lemma sep_conj_exists1:
  "((λs. x. P x s) * Q) = (λs. (x. (P x * Q) s))"
  by (force intro: sep_conjI dest: sep_conjD)

lemma sep_conj_exists2:
  "(P * (λs. x. Q x s)) = (λs. (x. (P * Q x) s))"
  by (force intro: sep_conjI dest: sep_conjD)

lemmas sep_conj_exists = sep_conj_exists1 sep_conj_exists2

lemma sep_conj_forall:
  "((λs. x. P x s) * Q) s  (P x * Q) s"
  by (force intro: sep_conjI dest: sep_conjD)

lemma sep_conj_impl:
  " (P * Q) s; s. P s  P' s; s. Q s  Q' s   (P' * Q') s"
  by (force intro: sep_conjI dest: sep_conjD)

lemma sep_conj_sep_true_left:
  "(P * Q) s  (sep_true * Q) s"
  by (erule sep_conj_impl, simp+)

lemma sep_conj_sep_true_right:
  "(P * Q) s  (P * sep_true) s"
  by (subst (asm) sep_conj_com, drule sep_conj_sep_true_left,
      simp add: sep_conj_ac)

lemma sep_globalise:
  " (P * R) s; (s. P s  Q s)   (Q * R) s"
  by (fast elim: sep_conj_impl)

lemma sep_implI:
  "s'. s  s'  x s'  y (s ++ s')  (x * y) s"
  by (force simp: sep_impl_def)

lemma sep_implI':
  assumes x: "h'.  h  h'; x h'   y (h ++ h')"
  shows "(x * y) h"
  apply (simp add: sep_impl_def)
  apply (intro allI impI)
  apply (erule conjE)
  apply (erule (1) x)
  done

lemma sep_implD:
  "(x * y) s  s'. s  s'  x s'  y (s ++ s')"
  by (force simp: sep_impl_def)

lemma sep_emp_sep_impl [simp]:
  "( * P) = P"
  apply(rule ext)
  apply(clarsimp simp: sep_impl_def)
  apply(rule iffI; clarsimp?)
   apply(drule_tac x=Map.empty in spec)
   apply fastforce
  apply(fastforce dest: sep_empD)
  done

lemma sep_impl_sep_true [simp]:
  "(P * sep_true) = sep_true"
  by (force intro: sep_implI)

lemma sep_impl_sep_false [simp]:
  "(sep_false * P) = sep_true"
  by (force intro: sep_implI)

lemma sep_impl_sep_true_P:
  "(sep_true * P) s  P s"
  by (auto dest!: sep_implD, drule_tac x=Map.empty in spec, simp)

lemma sep_impl_sep_true_false [simp]:
  "(sep_true * sep_false) = sep_false"
  by (force dest: sep_impl_sep_true_P)

lemma sep_impl_impl:
  "(P * Q * R) = (P * Q * R)"
  apply(rule ext)
  apply(rule iffI)
   apply(rule sep_implI)
   apply clarsimp
   apply(drule sep_conjD, clarsimp)
   apply(drule sep_implD)
   apply(drule_tac x=s0 in spec)
   apply(erule impE)
    apply(clarsimp simp: map_disj_def, fast)
   apply(drule sep_implD)
   apply(drule_tac x=s1 in spec)
   apply(erule impE)
    apply(clarsimp simp: map_disj_def, fast)
   apply(subst map_add_com [where h0=s1])
    apply(clarsimp simp: map_disj_def, fast)
   apply(subst map_add_assoc)
   apply simp
  apply(rule sep_implI, clarsimp)
  apply(rule sep_implI, clarsimp)
  apply(drule sep_implD)
  apply(drule_tac x="s' ++ s'a" in spec)
  apply(erule impE)
   apply(rule conjI)
    apply(clarsimp simp: map_disj_def, fast)
   apply(erule (1) sep_conjI)
    apply(clarsimp simp: map_disj_def, fast)
   apply(subst map_add_com)
    apply(clarsimp simp: map_disj_def, fast)
   apply simp
  apply(simp add: map_add_assoc)
  done

lemma sep_conj_sep_impl:
  " P s; s. (P * Q) s  R s   (Q * R) s"
  apply (rule sep_implI, clarsimp)
proof -
  fix s'
  assume "P s" and "s  s'" and "Q s'"
  hence "(P * Q) (s ++ s')" by (force simp: map_ac_simps intro: sep_conjI)
  moreover assume "s. (P * Q) s  R s"
  ultimately show "R (s ++ s')" by simp
qed

lemma sep_conj_sep_impl2:
  " (P * Q) s; s. P s  (Q * R) s   R s"
  by (force simp: map_ac_simps dest: sep_implD sep_conjD)

lemma sep_map'_anyI_exc [simp]:
  "(p ↪⇩g v) s  (p ↪⇩g -) s"
  by (force simp: sep_map'_any_def)

lemma sep_map'_anyD_exc:
  "(p ↪⇩g -) s  v. (p ↪⇩g v) s"
  by (force simp: sep_map'_any_def)

lemma sep_map'_any_unfold_exc:
  "(i ↪⇩g -) = ((i ↪⇩g -) * sep_true)"
  by (rule ext, simp add: sep_map'_any_def)
     (subst sep_map'_unfold_exc, subst sep_conj_com, subst sep_conj_exists,
      simp add: sep_conj_ac)

lemma sep_map'_inj_exc:
  assumes pv: "(p ↪⇩g (v::'a::c_type)) s" and pv': "(p ↪⇩h v') s"
  shows "v = v'"
proof -
  from pv pv' obtain s0 s1 s0' s1' where pv_m: "(p ↦⇩g v) s1" and
      pv'_m: "(p ↦⇩h v') s1'" and "s0 ++ s1 = s0' ++ s1'"
    by (force simp: sep_map'_def map_ac_simps dest!: sep_conjD)
  hence "s1 = s1'" by (force dest!: map_add_right_dom_eq sep_map_dom_exc)
  with pv_m pv'_m show ?thesis by (force dest: sep_map_inj)
qed

lemma sep_map'_any_dom_exc:
  "((p::'a::mem_type ptr) ↪⇩g -) s  (ptr_val p,SIndexVal)  dom s"
  by (clarsimp simp: sep_map'_def sep_map'_any_def sep_conj_ac
               dest!: sep_conjD)
     (subgoal_tac "s1 (ptr_val p,SIndexVal)  None", force simp: map_ac_simps,
      force dest: sep_map_dom_exc)

lemma sep_map'_dom_exc:
  "(p ↪⇩g (v::'a::mem_type)) s  (ptr_val p,SIndexVal)  dom s"
  apply(clarsimp simp: sep_map'_def sep_conj_ac dest!: sep_conjD)
  apply(subgoal_tac "s1 (ptr_val p, SIndexVal)  None")
   apply(force simp: map_ac_simps)
  apply(drule sep_map_dom_exc)
  apply(subgoal_tac "(ptr_val p, SIndexVal)  s_footprint p")
   apply fast
  apply(rule s_footprintI2 [where x=0, simplified])
  apply simp
  done

lemma sep_map'_lift_typ_heapD:
  "(p ↪⇩g v) s 
      lift_typ_heap g s p = Some (v::'a::c_type)"
  by (force simp: sep_map'_def map_ac_simps dest: sep_conjD
                  lift_typ_heap_heap_merge_sep_map)

lemma sep_map'_merge:
  assumes map'_v: "(p ↪⇩g v) s0  (p ↪⇩g v) s1" and disj: "s0  s1"
  shows "(p ↪⇩g v) (s0 ++ s1)" (is "?x")
proof cases
  assume "(p ↪⇩g v) s0"
  with disj show ?x
    apply (clarsimp simp: sep_map'_def sep_conj_ac dest!: sep_conjD)
    subgoal for s0' s1'
      apply (rule sep_conjI [where s1="s1'" and s0="s0' ++ s1"])
      apply (auto simp: map_ac_simps)
      done
    done
next
  assume "¬ (p ↪⇩g v) s0"
  with map'_v have "(p ↪⇩g v) s1" by simp
  with disj show ?x
    apply (clarsimp simp: sep_map'_def sep_conj_ac dest!: sep_conjD)
    subgoal for s0' s1'
      apply (rule sep_conjI [where s1="s1'" and s0="s0 ++ s0'"])
      apply (auto simp: map_ac_simps)
      done
    done
qed

lemma sep_conj_overlapD:
  " (P * Q) s; s. P s  ((p::'a::mem_type ptr) ↪⇩g -) s;
      s. Q s  (p ↪⇩h -) s   False"
  apply(drule sep_conjD, clarsimp simp: map_disj_def)
  apply(subgoal_tac "(ptr_val p,SIndexVal)  dom s0  (ptr_val p,SIndexVal)  dom s1")
   apply fast
  apply(fast intro!: sep_map'_any_dom_exc)
  done

lemma sep_no_skew:
  "(λs. (p ↪⇩g v) s  (q ↪⇩h w) s) s 
      p=q  {ptr_val (p::'a::c_type ptr)..+size_of TYPE('a)} 
          {ptr_val q..+size_of TYPE('a)} = {}"
  apply clarsimp
  apply(drule sep_map'_lift_typ_heapD)+
  apply(clarsimp simp: lift_typ_heap_if s_valid_def split: if_split_asm)
  apply(rule ccontr)
  apply(drule (1) h_t_valid_neq_disjoint; simp?)
  apply(rule peer_typ_not_field_of; simp)
  done

lemma sep_no_skew2:
  " (λs. (p ↪⇩g v) s  (q ↪⇩h w) s) s; typ_uinfo_t TYPE('a) t typ_uinfo_t TYPE('b) 
       {ptr_val (p::'a::c_type ptr)..+size_of TYPE('a)} 
          {ptr_val (q::'b::c_type ptr)..+size_of TYPE('b)} = {}"
  apply clarsimp
  apply(drule sep_map'_lift_typ_heapD)+
  apply(clarsimp simp: lift_typ_heap_if s_valid_def split: if_split_asm)
  apply(frule (1) h_t_valid_neq_disjoint[where q=q])
    apply(clarsimp simp: tag_disj_def sub_typ_proper_def)
    apply(simp add: typ_tag_lt_def)
   apply(clarsimp simp: tag_disj_def typ_tag_le_def field_of_t_def field_of_def)
  apply assumption
  done

lemma sep_conj_impl_same:
  "(P * (P * Q)) s  Q s"
  apply(drule sep_conjD, clarsimp)
  apply(drule sep_implD)
  apply(drule_tac x="s0" in spec)
  apply(clarsimp simp: map_disj_com)
  done


(* Pure *)

definition pure :: "('a,'b) map_assert  bool" where
  "pure P  s s'. P s = P s'"

lemma pure_sep_true:
  "pure sep_true"
  by (simp add: pure_def)

lemma pure_sep_fasle:
  "pure sep_true"
  by (simp add: pure_def)

lemma pure_split:
  "pure P = (P = sep_true  P = sep_false)"
  by (force simp: pure_def)

lemma pure_sep_conj:
  " pure P; pure Q   pure (P * Q)"
  by (force simp: pure_split)

lemma pure_sep_impl:
  " pure P; pure Q   pure (P * Q)"
  by (force simp: pure_split)

lemma pure_conj_sep_conj:
  " (λs. P s  Q s) s; pure P  pure Q   (P * Q) s"
  by (force simp: pure_split sep_conj_ac intro: sep_conj_sep_true)

lemma pure_sep_conj_conj:
  " (P * Q) s; pure P; pure Q   (λs. P s  Q s) s"
  by (force simp: pure_split)

lemma pure_conj_sep_conj_assoc:
  "pure P  ((λs. P s  Q s) * R) = (λs. P s  (Q * R) s)"
  by (force simp: pure_split)

lemma pure_sep_impl_impl:
  " (P * Q) s; pure P   P s  Q s"
  by (force simp: pure_split dest: sep_impl_sep_true_P)

lemma pure_impl_sep_impl:
  " P s  Q s; pure P; pure Q   (P * Q) s"
  by (force simp: pure_split)

(* Intuitionistic *)

definition
  intuitionistic :: "('a,'b) map_assert  bool"
where
  "intuitionistic P  s s'. P s  s m s'  P s'"

lemma intuitionisticI:
  "(s s'.  P s; s m s'   P s')  intuitionistic P"
  by (unfold intuitionistic_def, fast)

lemma intuitionisticD:
  " intuitionistic P; P s; s m s'   P s'"
  by (unfold intuitionistic_def, fast)

lemma pure_intuitionistic:
  "pure P  intuitionistic P"
  by (clarsimp simp: intuitionistic_def pure_def, fast)

lemma intuitionistic_sep_map':
  "intuitionistic (p ↪⇩g v)"
proof (rule intuitionisticI)
  fix s s'
  assume "(p ↪⇩g v) s"
  then obtain s0 s1 where "(p ↦⇩g v) s0" and s: "s = s1 ++ s0"
    by (force dest!: sep_conjD sep_map'D)
  moreover assume "s m s'"
  with s have "s' = s' |` (UNIV - dom s0) ++ s0"
    apply simp
    apply (drule map_add_le_mapE)
    by (subst map_le_restrict) force+
  ultimately show "(p ↪⇩g v) s'" by (force intro: sep_map'I sep_conjI)
qed

lemma intuitionistic_sep_conj_sep_true:
  "intuitionistic (P * sep_true)"
  by (rule intuitionisticI, drule sep_conjD, clarsimp)
     (erule_tac s1="s'|`(dom s' - dom s0)" in sep_conjI, simp,
      force simp: map_disj_def,
      force intro: map_le_dom_restrict_sub_add map_add_le_mapE  sym)

lemma intuitionistic_sep_impl_sep_true:
  "intuitionistic (sep_true * P)"
  apply (rule intuitionisticI, rule sep_implI, clarsimp)
proof -
  fix s s' s'a
  assume "(sep_true * P) s" and le: "s m s'" and "s'  s'a"
  moreover from this have "P (s ++ (s' |` (dom s' - dom s) ++ s'a))"
    by - (drule sep_implD,
          drule_tac x="s'|`(dom s' - dom s) ++ s'a" in spec,
          force simp: map_disj_def dest: map_disj_map_le)
  moreover have "dom s  dom (s' |` (dom s' - dom s)) = {}" by force
  ultimately show "P (s' ++ s'a)"
    by (force simp: map_le_dom_restrict_sub_add map_add_assoc dest!: map_add_comm)
qed

lemma intuitionistic_conj:
  " intuitionistic P; intuitionistic Q   intuitionistic (λs. P s  Q s)"
  by (force intro: intuitionisticI dest: intuitionisticD)

lemma intuitionistic_disj:
  " intuitionistic P; intuitionistic Q   intuitionistic (λs. P s  Q s)"
  by (force intro: intuitionisticI dest: intuitionisticD)

lemma intuitionistic_forall:
  "(x. intuitionistic (P x))  intuitionistic (λs. x. P x s)"
  by (force intro: intuitionisticI dest: intuitionisticD)

lemma intuitionistic_exists:
  "(x. intuitionistic (P x))  intuitionistic (λs. x. P x s)"
  by (force intro: intuitionisticI dest: intuitionisticD)

lemma intuitionistic_sep_conj:
  "intuitionistic (P::('a,'b) map_assert)  intuitionistic (P * Q)"
  apply (rule intuitionisticI, drule sep_conjD, clarsimp)
proof -
  fix s' s0 s1
  assume le: "s1 ++ s0 m s'" and disj: "s0  (s1::'a  'b)"
  hence le_restrict: "s0 m s' |` (dom s' - dom s1)"
    by - (rule map_le_dom_subset_restrict, erule map_add_le_mapE,
          force simp: map_disj_def  dest: map_le_implies_dom_le
          map_add_le_mapE)
  moreover assume "intuitionistic P" and "P s0"
  ultimately have "P (s' |` (dom s' - dom s1))"
    by - (erule (2) intuitionisticD)
  moreover from le_restrict have "s' |` (dom s' - dom s1)  s1"
    by (force simp: map_disj_def dest: map_le_implies_dom_le)
  moreover from le disj have "s1 m s'"
    by (subst (asm) map_add_comm, force  simp: map_disj_def)
       (erule map_add_le_mapE)
  hence "s' = s1 ++ s' |` (dom s' - dom s1)"
    by (subst map_add_comm, force simp: map_disj_def,
        force simp: map_le_dom_restrict_sub_add map_add_comm map_disj_def)
  moreover assume "Q s1"
  ultimately show "(P * Q) s'"
    by - (erule (3) sep_conjI)
qed

lemma intuitionistic_sep_impl:
  "intuitionistic (Q::('a,'b) map_assert)  intuitionistic (P * Q)"
  apply (rule intuitionisticI, rule sep_implI, clarsimp)
proof -
  fix s s' s'a
  assume le: "s m s'" and disj: "s'  (s'a::'a  'b)"
  moreover from this have "s ++ s'a m s' ++ s'a"
  proof -
    from le disj have "s m s ++ s'a"
      by (subst map_add_com)
         (force simp: map_disj_def dest: map_le_implies_dom_le, simp)
    with le disj show ?thesis
      by - (rule map_add_le_mapI, subst map_add_com,
            auto elim: map_le_trans)
  qed
  moreover assume "(P * Q) s" and "intuitionistic Q" and "P s'a"
  ultimately show "Q (s' ++ s'a)"
    by (fast elim: map_disj_map_le intuitionisticD dest: sep_implD)
qed

lemma strongest_intuitionistic:
  "¬ (Q. (s. (Q s  (P * sep_true) s))  intuitionistic Q 
      Q  (P * sep_true)  (s. P s  Q s))"
  by (clarsimp, rule ext) (force dest!: sep_conjD intuitionisticD)

lemma weakest_intuitionistic:
  "¬ (Q. (s. ((sep_true * P) s  Q s))  intuitionistic Q 
      Q  (sep_true * P)  (s. Q s  P s))"
  apply (clarsimp, rule ext)
  apply (rename_tac Q x)
  apply (rule iffI; clarsimp?)
  apply (rule sep_implI')
  apply (rename_tac h')
  apply (drule_tac s=x and s'="x ++ h'" in intuitionisticD; clarsimp simp: map_ac_simps)
  done

lemma intuitionistic_sep_conj_sep_true_P:
  " (P * sep_true) s; intuitionistic P   P s"
  by (force dest: intuitionisticD sep_conjD)

lemma intuitionistic_sep_conj_sep_true_simp:
  "intuitionistic P  (P * sep_true) = P"
  by (fast intro: sep_conj_sep_true elim: intuitionistic_sep_conj_sep_true_P)

lemma intuitionistic_sep_impl_sep_true_P:
  " P s; intuitionistic P   (sep_true * P) s"
  by (force simp: map_add_com intro: sep_implI dest: intuitionisticD)

lemma intuitionistic_sep_impl_sep_true_simp:
  "intuitionistic P  (sep_true * P) = P"
  by (fast elim: sep_impl_sep_true_P intuitionistic_sep_impl_sep_true_P)

(* Domain exact *)

definition
  dom_exact :: "('a,'b) map_assert  bool"
where
  "dom_exact P  s s'. P s  P s'  dom s = dom s'"

lemma dom_exactI:
  "(s s'.  P s; P s'   dom s = dom s')  dom_exact P"
  by (unfold dom_exact_def, fast)

lemma dom_exactD:
  " dom_exact P; P s0; P s1   dom s0 = dom s1"
  by (unfold dom_exact_def, fast)

lemma dom_exact_sep_conj:
  " dom_exact P; dom_exact Q   dom_exact (P * Q)"
  by (rule dom_exactI, (drule sep_conjD)+, clarsimp)
     (drule (2) dom_exactD, drule (2) dom_exactD, simp)

lemma dom_exact_sep_conj_conj:
  " (P * R) s; (Q * R) s; dom_exact R   ((λs. P s  Q s) * R) s"
  apply ((drule sep_conjD)+)
  by (clarsimp simp: sep_conj_ac,
      rule sep_conjI, fast, rule conjI)
     (fast, drule (2) dom_exactD, drule (1) map_disj_add_eq_dom_right_eq,
      auto simp: map_ac_simps)

lemma sep_conj_conj_simp:
  "dom_exact R  ((λs. P s  Q s) * R) = (λs. (P * R) s  (Q * R) s)"
  by (fast intro!: sep_conj_conj dom_exact_sep_conj_conj)

definition dom_eps :: "('a,'b) map_assert  'a set" where
  "dom_eps P  THE x. s. P s  x = dom s"

lemma dom_epsI:
  " dom_exact P; P s; x  dom s   x  dom_eps P"
  by (unfold dom_eps_def, rule theI2 [where a="dom s"])
     (fastforce simp: dom_exact_def, clarsimp+)

lemma dom_epsD [rule_format]:
  " dom_exact P; P s   x  dom_eps P  x  dom s"
  by (unfold dom_eps_def, rule theI2 [where a="dom s"])
     (fastforce simp: dom_exact_def, clarsimp+)

lemma dom_eps:
  " dom_exact P; P s   dom s = dom_eps P"
  by (force intro: dom_epsI dest: dom_epsD)

lemma map_restrict_dom_exact:
  " dom_exact P; P s   s |` dom_eps P = s"
  by (force simp: restrict_map_def None_com intro: dom_epsI)

lemma map_restrict_dom_exact2:
  " dom_exact P; P s0; s0  s1   (s1 |` dom_eps P) = Map.empty"
  by (force simp: restrict_map_def map_disj_def dest: dom_epsD)

lemma map_restrict_dom_exact3:
  " dom_exact P; P s   s |` (UNIV - dom_eps P) = Map.empty"
  by (force simp: restrict_map_def dest: dom_epsI)

lemma map_add_restrict_dom_exact:
  " dom_exact P; s0  s1; P s1   (s1 ++ s0) |` (dom_eps P) = s1"
  by (simp add: map_add_restrict map_restrict_dom_exact)
     (subst map_restrict_dom_exact2, auto simp: map_disj_def)

lemma map_add_restrict_dom_exact2:
  " dom_exact P; s0  s1; P s0   (s1 ++ s0) |` (UNIV - dom_eps P) = s1"
  by (force simp: map_add_restrict map_disj_def dom_eps
            intro: restrict_map_subdom dest: map_restrict_dom_exact3 )

lemma dom_exact_sep_conj_forall:
  assumes sc: "x. (P x * Q) s" and de: "dom_exact Q"
  shows "((λs. x. P x s) * Q) s"
proof (rule sep_conjI [where s0="s |` (UNIV - dom_eps Q)" and  s1="s |` dom_eps Q"])
  from sc de show "x. P x (s |` (UNIV - dom_eps Q))"
    by (force simp: map_add_restrict_dom_exact2 sep_conj_ac dest: sep_conjD)
next
  from sc de show "Q (s |` dom_eps Q)"
    by (force simp: map_add_restrict_dom_exact dest!: sep_conjD spec)
next
  from sc de show "s |` (UNIV - dom_eps Q)  s |` dom_eps Q"
    by (force simp: map_add_restrict_dom_exact2 map_ac_simps
              dest: map_add_restrict_dom_exact dest!: sep_conjD spec)
next
  show "s = s |` dom_eps Q ++ s |` (UNIV - dom_eps Q)" by simp
qed

lemma sep_conj_forall_simp:
  "dom_exact Q  ((λs. x. P x s) * Q) = (λs. x. (P x * Q) s)"
  by (fast dest: sep_conj_forall dom_exact_sep_conj_forall)

lemma dom_exact_sep_map:
  "dom_exact (i ↦⇩g x)"
  by (clarsimp simp: dom_exact_def sep_map_def)

lemma dom_exact_P_emp:
  " dom_exact P; P Map.empty; P s   s = Map.empty"
  by (auto simp: dom_exact_def)


(* Strictly exact *)

definition
  strictly_exact :: "('a,'b) map_assert  bool"
where
  "strictly_exact P  s s'. P s  P s'  s = s'"

lemma strictly_exactD:
  " strictly_exact P; P s0; P s1   s0 = s1"
  by (unfold strictly_exact_def, fast)

lemma strictly_exactI:
  "(s s'.  P s; P s'   s = s')  strictly_exact P"
  by (unfold strictly_exact_def, fast)

lemma strictly_exact_dom_exact:
  "strictly_exact P  dom_exact P"
  by (force simp: strictly_exact_def dom_exact_def)

lemma strictly_exact_sep_emp:
  "strictly_exact "
  by (force simp: strictly_exact_def dest: sep_empD)

lemma strictly_exact_sep_conj:
  " strictly_exact P; strictly_exact Q   strictly_exact (P * Q)"
  by (force intro!: strictly_exactI dest: sep_conjD strictly_exactD)

lemma strictly_exact_conj_impl:
  " (Q * sep_true) s; P s; strictly_exact Q   (Q * (Q * P)) s"
  by (force intro: sep_conjI sep_implI dest: strictly_exactD dest!: sep_conjD)

lemma dom_eps_sep_emp [simp]:
  "dom_eps  = {}"
  apply(subst dom_eps [symmetric])
    apply(rule strictly_exact_dom_exact)
    apply(rule strictly_exact_sep_emp)
   apply(rule sep_emp_empty)
  apply simp
  done

lemma dom_eps_sep_map:
  "g p  dom_eps (p ↦⇩g (v::'a::mem_type)) = s_footprint p"
  apply(subst dom_eps [symmetric])
    apply(rule dom_exact_sep_map)
   apply(rule sep_map_singleton)
   apply(erule ptr_retyp_h_t_valid)
  apply(subst singleton_dom)
   apply(erule ptr_retyp_h_t_valid)
  apply simp
  done

(* Non-empty *)

definition non_empty :: "('a,'b) map_assert  bool" where
  "non_empty P  s. P s"

lemma non_emptyI:
  "P s  non_empty P"
  by (force simp: non_empty_def)

lemma non_emptyD:
  "non_empty P  s. P s"
  by (force simp: non_empty_def)

lemma non_empty_sep_true:
  "non_empty sep_true"
  by (simp add: non_empty_def)

lemma non_empty_sep_false:
  "¬ non_empty sep_false"
  by (simp add: non_empty_def)

lemma non_empty_sep_emp:
  "non_empty "
  unfolding non_empty_def by (rule exI, rule sep_emp_empty)

lemma non_empty_sep_map:
  "g p  non_empty (p ↦⇩g (v::'a::mem_type))"
  apply(unfold non_empty_def)
  apply(rule exI, rule sep_map_singleton)
  apply(erule ptr_retyp_h_t_valid)
  done

lemma non_empty_sep_conj:
  " non_empty P; non_empty Q; dom_exact P; dom_exact Q;
      dom_eps P  dom_eps Q = {}   non_empty (P * Q)"
  apply(clarsimp simp: non_empty_def)
  subgoal for s s'
    apply(rule exI [where x="s++s'"])
    apply(rule sep_conjI, assumption+)
     apply(clarsimp simp: map_disj_def dom_eps)
    apply(subst map_add_com)
     apply(clarsimp simp: map_disj_def dom_eps)
    apply simp
    done
  done

lemma non_empty_sep_map':
  "g p  non_empty (p ↪⇩g (v::'a::mem_type))"
  apply(unfold sep_map'_def)
  apply(clarsimp simp: non_empty_def sep_conj_ac)
  apply(rule exI [where x="singleton p v h (ptr_retyp p d)"])
  apply(rule sep_conjI [where s0=Map.empty])
     apply simp
    apply(rule sep_map_singleton)
    apply(erule ptr_retyp_h_t_valid)
   apply(simp add: map_disj_def)
  apply simp
  done

lemma non_empty_sep_impl:
  "¬ P Map.empty  non_empty (P * Q)"
  apply(clarsimp simp: non_empty_def)
  apply(rule exI [where x="λs. Some undefined"] )
  apply(rule sep_implI)
  apply(clarsimp simp: map_disj_def)
  done

(* Some useful lemmas *)

lemma pure_conj_right: "(Q * (λs. P'  Q' s)) = (λs. P'  (Q * Q') s)"
  by (rule ext, standard, standard, clarsimp dest!: sep_conjD)
     (erule sep_conj_impl, auto)

lemma pure_conj_right': "(Q * (λs. P' s  Q')) = (λs. Q'  (Q * P') s)"
  by (simp add: conj_comms pure_conj_right)

lemma pure_conj_left: "((λs. P'  Q' s) * Q) = (λs. P'  (Q' * Q) s)"
  by (simp add: pure_conj_right sep_conj_ac)

lemma pure_conj_left': "((λs. P' s  Q') * Q) = (λs. Q'  (P' * Q) s)"
  by (subst conj_comms, subst pure_conj_left, simp)

lemmas pure_conj = pure_conj_right pure_conj_right' pure_conj_left pure_conj_left'

declare pure_conj [simp add]

lemma sep_conj_sep_conj_sep_impl_sep_conj:
  "(P * R) s  (P * (Q * (Q * R))) s"
  by (erule (1) sep_conj_impl, erule sep_conj_sep_impl, simp add: sep_conj_ac)

lemma sep_map'_conjE1_exc:
  " (P * Q) s; s. P s  (i ↪⇩g v) s   (i ↪⇩g v) s"
  by (subst sep_map'_unfold_exc, erule sep_conj_impl, simp+)

lemma sep_map'_conjE2_exc:
  " (P * Q) s; s. Q s  (i ↪⇩g v) s   (i ↪⇩g v) s"
  by (subst (asm) sep_conj_com, erule sep_map'_conjE1_exc, simp)

lemma sep_map'_any_conjE1_exc:
  " (P * Q) s; s. P s  (i ↪⇩g -) s   (i ↪⇩g -) s"
  by (subst sep_map'_any_unfold_exc, erule sep_conj_impl, simp+)

lemma sep_map'_any_conjE2_exc:
  " (P * Q) s; s. Q s  (i ↪⇩g -) s   (i ↪⇩g -) s"
  by (subst (asm) sep_conj_com, erule sep_map'_any_conjE1_exc, simp)

lemma sep_conj_mapD_exc:
  "((i ↦⇩g v) * P) s  (i ↪⇩g v) s  ((i ↦⇩g -) * P) s"
  by (force simp: sep_conj_ac intro: sep_conj_impl sep_map'_conjE2_exc)

lemma sep_impl_conj_sameD:
  " (P * P * Q) s; dom_exact P; non_empty P; dom s  UNIV - dom_eps P 
       Q s"
  apply(drule sep_implD)
  apply(clarsimp simp: non_empty_def)
  apply(rename_tac s')
  apply(drule_tac x=s' in spec)
  apply(erule impE)
   apply(fastforce simp: map_disj_def dom_eps)
  apply(drule sep_conjD, clarsimp)
  apply(clarsimp simp: map_disj_def)
  apply(subst (asm) map_add_comm)
   apply(clarsimp simp: dom_eps)
   apply fast
  apply(subst (asm) map_add_comm, fast)
  apply(drule map_disj_add_eq_dom_right_eq)
     apply(simp add: dom_eps)
    apply(clarsimp simp: dom_eps map_disj_def)
    apply fast
   apply(simp add: map_disj_def)
  apply clarsimp
  done

lemma sep_impl_conj_sameI:
  "Q s   (P * P * Q) s"
  by (fastforce intro: sep_implI sep_conjI simp: map_disj_com)

end