Theory Separation_UMM
theory Separation_UMM
imports TypHeap
begin
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. ∃s⇩0 s⇩1. s⇩0 ⊥ s⇩1 ∧ s = s⇩1 ++ s⇩0 ∧ P s⇩0 ∧ Q s⇩1"
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"
(‹(‹open_block notation=‹mixfix sep_map››_ ↦⇘_⇙ _)› [56,0,51] 56)
where
"p ↦⇘g⇙ v ≡ λs. lift_typ_heap g s p = Some v ∧ dom s = s_footprint p ∧ wf_heap_val s"
notation (input)
sep_map (‹(‹open_block notation=‹mixfix sep_map››_ ↦⇩_ _)› [56,1000,51] 56)
definition
sep_map_any :: "'a ::c_type ptr ⇒ 'a ptr_guard ⇒ heap_assert"
(‹(‹open_block notation=‹mixfix sep_map_any››_ ↦⇘_⇙ -)› [56,0] 56)
where
"p ↦⇘g⇙ - ≡ λs. ∃v. (p ↦⇩g v) s"
notation (input)
sep_map_any (‹(‹open_block notation=‹mixfix sep_map_any››_ ↦⇩_ -)› [56,0] 56)
definition
sep_map' :: "'a::c_type ptr ⇒ 'a ptr_guard ⇒ 'a ⇒ heap_assert"
(‹(‹open_block notation=‹mixfix sep_map'››_ ↪⇘_⇙ _)› [56,0,51] 56)
where
"p ↪⇘g⇙ v ≡ (p ↦⇘g⇙ v) ∧⇧* sep_true"
notation (input)
sep_map' (‹(‹open_block notation=‹mixfix sep_map'››_ ↪⇩_ _)› [56,1000,51] 56)
definition
sep_map'_any :: "'a ::c_type ptr ⇒ 'a ptr_guard ⇒ heap_assert"
(‹(‹open_block notation=‹mixfix sep_map'_any››_ ↪⇘_⇙ -)› [56,0] 56)
where
"p ↪⇘g⇙ - ≡ λs. ∃x. (p ↪⇩g x) s"
notation (input)
sep_map'_any (‹(‹open_block notation=‹mixfix sep_map'_any››_ ↪⇩_ -)› [56,0] 56)
syntax
"_sep_assert" :: "bool ⇒ heap_state ⇒ bool"
(‹(‹open_block notation=‹mixfix assertion››'(_')⇗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:
"s⇩1,g ⊨⇩s p ⟹ s⇩0 ++ s⇩1,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:
"⟦ s⇩0 ++ s⇩1,g ⊨⇩s p; s_footprint p ⊆ dom s⇩1 ⟧ ⟹ s⇩1,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':
"⟦ s⇩1,g ⊨⇩s (p::'a::c_type ptr); n ≤ size_of TYPE('a) ⟧ ⟹
heap_list_s (s⇩0 ++ s⇩1) n (ptr_val p + of_nat (size_of TYPE('a) - n))
= heap_list_s s⇩1 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 s⇩1"
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:
"s⇩1,g ⊨⇩s ((Ptr p)::'a::c_type ptr) ⟹
heap_list_s (s⇩0 ++ s⇩1) (size_of TYPE('a)) p = heap_list_s s⇩1 (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 s⇩1 p = Some v ⟹ lift_typ_heap g (s⇩0 ++ s⇩1) (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) s⇩1 ⟹ lift_typ_heap g (s⇩0 ++ s⇩1) p = Some (v::'a::c_type)"
by (drule sep_map_lift_typ_heapD, erule lift_typ_heap_heap_merge_right)
lemma sep_conjI:
"⟦ P s⇩0; Q s⇩1; s⇩0 ⊥ s⇩1; s = s⇩1 ++ s⇩0 ⟧ ⟹ (P ∧⇧* Q) s"
by (force simp: sep_conj_def)
lemma sep_conjD:
"(P ∧⇧* Q) s ⟹ ∃s⇩0 s⇩1. s⇩0 ⊥ s⇩1 ∧ s = s⇩1 ++ s⇩0 ∧ P s⇩0 ∧ Q s⇩1"
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 s⇩1=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 s⇩0=x and s⇩1=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' s⇩2 where disj_o: "s' ⊥ s⇩2" and merge_o: "s = s⇩2 ++ s'" and
l_o: "(P ∧⇧* Q) s'" and r_o: "R s⇩2" by (force dest: sep_conjD)
then obtain s⇩0 s⇩1 where disj_i: "s⇩0 ⊥ s⇩1" and merge_i: "s' = s⇩1 ++ s⇩0" and
l_i: "P s⇩0" and r_i: "Q s⇩1" by (force dest: sep_conjD)
from disj_o disj_i merge_i have disj_i': "s⇩1 ⊥ s⇩2"
by (force simp: map_ac_simps)
with r_i and r_o have r_o': "(Q ∧⇧* R) (s⇩2 ++ s⇩1)" by (fast intro: sep_conjI)
from disj_o merge_i disj_i disj_i' have "s⇩0 ⊥ s⇩2 ++ s⇩1"
by (force simp: map_ac_simps)
with r_o' l_i have "(P ∧⇧* (Q ∧⇧* R)) ((s⇩2 ++ s⇩1) ++ s⇩0)"
by (force intro: sep_conjI)
moreover from merge_o merge_i disj_i disj_i' have "s = ((s⇩2 ++ s⇩1) ++ s⇩0)"
by (simp add: map_add_assoc [symmetric])
ultimately show ?thesis by simp
qed
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)
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
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 s⇩0 s⇩1 where "s⇩0 ⊥ s⇩1" and "s = s⇩1 ++ s⇩0" and "P s⇩0 ∨ Q s⇩0" and
"R s⇩1"
by - (drule sep_conjD, auto)
moreover from this have "¬ ?z ⟹ ¬ Q s⇩0"
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=s⇩0 in spec)
apply(erule impE)
apply(clarsimp simp: map_disj_def, fast)
apply(drule sep_implD)
apply(drule_tac x=s⇩1 in spec)
apply(erule impE)
apply(clarsimp simp: map_disj_def, fast)
apply(subst map_add_com [where h⇩0=s⇩1])
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 s⇩0 s⇩1 s⇩0' s⇩1' where pv_m: "(p ↦⇩g v) s⇩1" and
pv'_m: "(p ↦⇩h v') s⇩1'" and "s⇩0 ++ s⇩1 = s⇩0' ++ s⇩1'"
by (force simp: sep_map'_def map_ac_simps dest!: sep_conjD)
hence "s⇩1 = s⇩1'" 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 "s⇩1 (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 "s⇩1 (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) s⇩0 ∨ (p ↪⇩g v) s⇩1" and disj: "s⇩0 ⊥ s⇩1"
shows "(p ↪⇩g v) (s⇩0 ++ s⇩1)" (is "?x")
proof cases
assume "(p ↪⇩g v) s⇩0"
with disj show ?x
apply (clarsimp simp: sep_map'_def sep_conj_ac dest!: sep_conjD)
subgoal for s⇩0' s⇩1'
apply (rule sep_conjI [where s⇩1="s⇩1'" and s⇩0="s⇩0' ++ s⇩1"])
apply (auto simp: map_ac_simps)
done
done
next
assume "¬ (p ↪⇩g v) s⇩0"
with map'_v have "(p ↪⇩g v) s⇩1" by simp
with disj show ?x
apply (clarsimp simp: sep_map'_def sep_conj_ac dest!: sep_conjD)
subgoal for s⇩0' s⇩1'
apply (rule sep_conjI [where s⇩1="s⇩1'" and s⇩0="s⇩0 ++ s⇩0'"])
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 s⇩0 ∧ (ptr_val p,SIndexVal) ∈ dom s⇩1")
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="s⇩0" in spec)
apply(clarsimp simp: map_disj_com)
done
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)
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 s⇩0 s⇩1 where "(p ↦⇩g v) s⇩0" and s: "s = s⇩1 ++ s⇩0"
by (force dest!: sep_conjD sep_map'D)
moreover assume "s ⊆⇩m s'"
with s have "s' = s' |` (UNIV - dom s⇩0) ++ s⇩0"
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 s⇩1="s'|`(dom s' - dom s⇩0)" 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' s⇩0 s⇩1
assume le: "s⇩1 ++ s⇩0 ⊆⇩m s'" and disj: "s⇩0 ⊥ (s⇩1::'a ⇀ 'b)"
hence le_restrict: "s⇩0 ⊆⇩m s' |` (dom s' - dom s⇩1)"
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 s⇩0"
ultimately have "P (s' |` (dom s' - dom s⇩1))"
by - (erule (2) intuitionisticD)
moreover from le_restrict have "s' |` (dom s' - dom s⇩1) ⊥ s⇩1"
by (force simp: map_disj_def dest: map_le_implies_dom_le)
moreover from le disj have "s⇩1 ⊆⇩m s'"
by (subst (asm) map_add_comm, force simp: map_disj_def)
(erule map_add_le_mapE)
hence "s' = s⇩1 ++ s' |` (dom s' - dom s⇩1)"
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 s⇩1"
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)
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 s⇩0; P s⇩1 ⟧ ⟹ dom s⇩0 = dom s⇩1"
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 s⇩0; s⇩0 ⊥ s⇩1 ⟧ ⟹ (s⇩1 |` 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; s⇩0 ⊥ s⇩1; P s⇩1 ⟧ ⟹ (s⇩1 ++ s⇩0) |` (dom_eps P) = s⇩1"
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; s⇩0 ⊥ s⇩1; P s⇩0 ⟧ ⟹ (s⇩1 ++ s⇩0) |` (UNIV - dom_eps P) = s⇩1"
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 s⇩0="s |` (UNIV - dom_eps Q)" and s⇩1="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)
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 s⇩0; P s⇩1 ⟧ ⟹ s⇩0 = s⇩1"
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
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 s⇩0=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
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