theory SepLog_Misc
imports "SepLogicTime_RBTreeBasic.SepAuto"
begin
lemma inst_ex_assn: "A ⟹⇩A B x ⟹ A ⟹⇩A (∃⇩Ax. B x)"
using entails_ex_post by blast
lemma ent_iffI:
assumes "A⟹⇩AB"
assumes "B⟹⇩AA"
shows "A=B"
apply(rule assn_ext)
using assms
using entails_def by blast
lemma [simp]: "pHeap h {} 0 ⊨ emp" by(simp add: one_assn_rule)
lemma mod_star_trueI: "h⊨P ⟹ h⊨P*true"
by (metis assn_times_comm entailsD' entails_true mult.left_neutral)
lemma pure_true[simp]: "↑True = emp"
by (auto intro: assn_ext simp: one_assn_rule pure_assn_rule)
lemma merge_true_star[simp]: "true*true = true"
using top_assn_reduce by auto
lemma mod_false[simp]: "¬ h⊨false"
by (simp add: pure_assn_rule)
lemma mod_pure_star_dist[simp]: "h⊨P*↑b ⟷ h⊨P ∧ b"
by (simp add: mod_pure_star_dist)
lemma mod_pure_star_dist'[simp]: "h⊨↑b*P ⟷ h⊨P ∧ b"
using mod_pure_star_dist
by (simp add: mult.commute)
lemma pure_assn_eq_conv[simp]: "↑P = ↑Q ⟷ P=Q"
by (metis (full_types) assn_times_comm empty_iff in_range.simps mod_false' mod_pure_star_dist top_assn_rule)
thm entailsD
lemma ent_true[simp]: "P ⟹⇩A true"
by (simp add: entails_true)
lemma ent_star_mono: "⟦ P ⟹⇩A P'; Q ⟹⇩A Q'⟧ ⟹ P*Q ⟹⇩A P'*Q'"
using entails_trans2 entails_frame by blast
lemma merge_true_star_ctx: "true * (true * P) = true * P"
by (metis assn_times_assoc top_assn_reduce)
lemma pf: "(a::assn) * b = b * a"
using assn_times_comm by auto
lemma ent_true_drop:
"P⟹⇩AQ*true ⟹ P*R⟹⇩AQ*true"
"P⟹⇩AQ ⟹ P⟹⇩AQ*true"
apply (metis assn_times_comm ent_star_mono ent_true merge_true_star_ctx)
apply (metis assn_one_left ent_star_mono ent_true pf)
done
lemma ent_true_drop_fst:
"R⟹⇩AQ*true ⟹ P*R⟹⇩AQ*true"
apply (metis assn_times_comm ent_star_mono ent_true merge_true_star_ctx)
done
lemma ent_true_drop_fstf:
"R⟹⇩Atrue*Q ⟹ P*R⟹⇩Atrue*Q"
apply (metis assn_times_comm ent_star_mono ent_true merge_true_star_ctx)
done
lemma entailsI:
assumes "⋀h. h⊨P ⟹ h⊨Q"
shows "P ⟹⇩A Q"
using assms unfolding entails_def by auto
lemma entt_refl': "P⟹⇩A P * true"
by (simp add: entailsI mod_star_trueI)
subsection "for relH"
text "Transitivity"
lemma relH_trans[trans]: "⟦relH as h1 h2; relH as h2 h3⟧ ⟹ relH as h1 h3"
unfolding relH_def
by auto
lemma in_range_subset:
"⟦as ⊆ as'; in_range (h,as')⟧ ⟹ in_range (h,as)"
by (auto simp: in_range.simps)
lemma relH_subset:
assumes "relH bs h h'"
assumes "as ⊆ bs"
shows "relH as h h'"
using assms unfolding relH_def by (auto intro: in_range_subset)
subsection "new_addrs"
lemma new_addrs_id[simp]: "(new_addrs h as h) = as" unfolding new_addrs_def by auto
subsection "entailst"
definition entailst :: "assn ⇒ assn ⇒ bool" (infix "⟹⇩t" 10)
where "entailst A B ≡ A ⟹⇩A B * true"
lemma enttI: "A⟹⇩AB*true ⟹ A⟹⇩tB" unfolding entailst_def .
lemma enttD: "A⟹⇩tB ⟹ A⟹⇩AB*true" unfolding entailst_def .
lemma ent_trans[trans]: "⟦ P ⟹⇩A Q; Q ⟹⇩AR ⟧ ⟹ P ⟹⇩A R"
by (auto intro: entailsI dest: entailsD)
lemma entt_fr_drop: "F⟹⇩tF' ⟹ F*A ⟹⇩t F'"
using ent_true_drop(1) enttD enttI by blast
lemma entt_trans:
"entailst A B ⟹ entailst B C ⟹ entailst A C"
unfolding entailst_def
apply (erule ent_trans)
by (metis assn_times_assoc ent_star_mono ent_true merge_true_star)
lemma ent_imp_entt: "P⟹⇩AQ ⟹ P⟹⇩tQ"
apply (rule enttI)
apply (erule ent_trans)
by (simp add: entailsI mod_star_trueI)
lemma entt_refl[simp, intro!]: "P⟹⇩t P "
by (simp add: entailst_def entailsI mod_star_trueI)
subsection "Heap Or"
declare or_assn_conv [simp]
lemma ex_distrib_or: "(∃⇩Ax. Q x) ∨⇩A P = (∃⇩Ax. Q x ∨⇩A P)"
by (auto intro!: assn_ext simp: mod_ex_dist)
lemma sup_commute: "P ∨⇩A Q = Q ∨⇩A P"
by (meson assn_ext or_assn_conv)
lemma ent_disjI1:
assumes "P ∨⇩A Q ⟹⇩A R"
shows "P ⟹⇩A R" using assms unfolding entails_def by simp
lemma ent_disjI2:
assumes "P ∨⇩A Q ⟹⇩A R"
shows "Q ⟹⇩A R" using assms unfolding entails_def by simp
lemma ent_disjI1_direct[simp]: "A ⟹⇩A A ∨⇩A B"
by (simp add: entailsI or_assn_conv)
lemma ent_disjI2_direct[simp]: "B ⟹⇩A A ∨⇩A B"
by (simp add: entailsI or_assn_conv)
lemma entt_disjI1_direct[simp]: "A ⟹⇩t A ∨⇩A B"
by (rule ent_imp_entt[OF ent_disjI1_direct])
lemma entt_disjI2_direct[simp]: "B ⟹⇩t A ∨⇩A B"
by (rule ent_imp_entt[OF ent_disjI2_direct])
lemma entt_disjI1': "A⟹⇩tB ⟹ A⟹⇩tB∨⇩AC"
using entt_disjI1_direct entt_trans by blast
lemma entt_disjI2': "A⟹⇩tC ⟹ A⟹⇩tB∨⇩AC"
using entt_disjI2_direct entt_trans by blast
lemma ent_disjE: "⟦ A⟹⇩AC; B⟹⇩AC ⟧ ⟹ A∨⇩AB ⟹⇩AC"
by (simp add: entails_def or_assn_conv)
lemma entt_disjD1: "A∨⇩AB⟹⇩tC ⟹ A⟹⇩tC"
using entt_disjI1_direct entt_trans by blast
lemma entt_disjD2: "A∨⇩AB⟹⇩tC ⟹ B⟹⇩tC"
using entt_disjI2_direct entt_trans by blast
lemma mod_star_conv: "h⊨A*B
⟷ (∃hr as1 as2 n1 n2. h=pHeap hr (as1∪as2) (n1+n2) ∧ as1∩as2={} ∧ pHeap hr as1 n1⊨A ∧ pHeap hr as2 n2⊨B)"
apply (cases h)
apply rule
by(auto dest!: mod_star_convE intro!: mod_star_convI)
lemma star_or_dist1:
"(A ∨⇩A B)*C = (A*C ∨⇩A B*C)"
apply (rule ent_iffI)
unfolding entails_def
by (fastforce simp: mod_star_conv )+
lemma star_or_dist2:
"C*(A ∨⇩A B) = (C*A ∨⇩A C*B)"
apply (rule ent_iffI)
unfolding entails_def
by (fastforce simp: mod_star_conv )+
lemmas star_or_dist = star_or_dist1 star_or_dist2
lemma ent_disjI1': "A⟹⇩AB ⟹ A⟹⇩AB∨⇩AC"
by (auto simp: entails_def star_or_dist)
lemma ent_disjI2': "A⟹⇩AC ⟹ A⟹⇩AB∨⇩AC"
by (auto simp: entails_def star_or_dist)
subsection ‹New command ureturn›
definition ureturn :: "'a ⇒ 'a Heap" where
[code del]: "ureturn x = Heap_Monad.heap (λh. (x,h,0))"
lemma execute_ureturn [execute_simps]:
"execute (ureturn x) = Some ∘ (λh. (x,h,0))"
by (simp add: ureturn_def execute_simps)
lemma success_ureturnI [success_intros]:
"success (ureturn x) h"
by (rule successI) (simp add: execute_simps)
lemma effect_ureturnI [effect_intros]:
"h = h' ⟹ effect (ureturn x) h h' x 0"
by (rule effectI) (simp add: execute_simps)
lemma effect_ureturnE [effect_elims]:
assumes "effect (ureturn x) h h' r n"
obtains "r = x" "h' = h" "n=0"
using assms by (rule effectE) (simp add: execute_simps)
thm execute_return'
lemma timeFrame0[simp]: "timeFrame 0 f = f" apply(cases f) by auto
lemma ureturn_bind [simp]: "ureturn x ⤜ f = f x"
apply (rule Heap_eqI)
by (auto simp add: execute_simps )
lemma bind_ureturn [simp]: "f ⤜ ureturn = f"
by (rule Heap_eqI) (simp add: bind_def execute_simps split: option.splits)
lemma execute_ureturn' [rewrite]: "execute (ureturn x) h = Some (x, h, 0)" by (metis comp_eq_dest_lhs execute_ureturn)
lemma run_ureturnD: "run (ureturn x) (Some h) σ r t ⟹ σ = Some h ∧ r = x ∧ t = 0"
by (auto simp add: execute_ureturn' run.simps)
lemma return_rule:
"<$0> ureturn x <λr. ↑(r = x)>"
unfolding hoare_triple_def by (auto dest!: run_ureturnD simp: relH_def timeCredit_assn_rule)
subsection "Heap And"
lemma mod_and_dist: "h⊨P∧⇩AQ ⟷ h⊨P ∧ h⊨Q"
by (rule and_assn_conv)
lemma [simp]: "false∧⇩AQ = false"
apply(rule assn_ext)
by(simp add: mod_and_dist)
lemma [simp]: "Q∧⇩Afalse = false"
apply(rule assn_ext)
by(simp add: mod_and_dist)
lemma ent_conjI: "⟦ A⟹⇩AB; A⟹⇩AC ⟧ ⟹ A ⟹⇩A B ∧⇩A C"
unfolding entails_def by (auto simp: mod_and_dist)
lemma ent_conjE1: "⟦A⟹⇩AC⟧ ⟹ A∧⇩AB⟹⇩AC"
unfolding entails_def by (auto simp: mod_and_dist)
lemma ent_conjE2: "⟦B⟹⇩AC⟧ ⟹ A∧⇩AB⟹⇩AC"
unfolding entails_def by (auto simp: mod_and_dist)
subsection {* Precision *}
text {*
Precision rules describe that parts of an assertion may depend only on the
underlying heap. For example, the data where a pointer points to is the same
for the same heap.
*}
text {* Precision rules should have the form:
@{text [display] "∀x y. (h⊨(P x * F1) ∧⇩A (P y * F2)) ⟶ x=y"}*}
definition "precise R ≡ ∀a a' h p F F'.
h ⊨ R a p * F ∧⇩A R a' p * F' ⟶ a = a'"
lemma preciseI[intro?]:
assumes "⋀a a' h p F F'. h ⊨ R a p * F ∧⇩A R a' p * F' ⟹ a = a'"
shows "precise R"
using assms unfolding precise_def by blast
lemma preciseD:
assumes "precise R"
assumes "h ⊨ R a p * F ∧⇩A R a' p * F'"
shows "a=a'"
using assms unfolding precise_def by blast
lemma preciseD':
assumes "precise R"
assumes "h ⊨ R a p * F"
assumes "h ⊨ R a' p * F'"
shows "a=a'"
apply (rule preciseD)
apply (rule assms)
apply (simp only: mod_and_dist)
apply (blast intro: assms)
done
lemma false_absorb[simp]: "false * R = false"
by (simp add: assn_ext mod_false')
lemma star_false_right[simp]: "P * false = false"
using false_absorb by (simp add: assn_times_comm)
lemma precise_extr_pure[simp]:
"precise (λx y. ↑P * R x y) ⟷ (P ⟶ precise R)"
"precise (λx y. R x y * ↑P) ⟷ (P ⟶ precise R)"
subgoal apply (cases P) by (auto intro!: preciseI simp: false_absorb pure_true and_assn_conv)
subgoal apply (cases P) by (auto intro!: preciseI simp: false_absorb assn_times_comm and_assn_conv)
done
lemma sngr_prec: "precise (λx p. p↦⇩rx)"
apply rule
apply (clarsimp simp: mod_and_dist)
subgoal for a a' h
apply(cases h)
by(auto dest!: mod_star_convE simp: sngr_assn_rule)
done
lemma snga_prec: "precise (λx p. p↦⇩ax)"
apply rule
apply (clarsimp simp: mod_and_dist)
subgoal for a a' h
apply(cases h)
by(auto dest!: mod_star_convE simp: snga_assn_rule)
done
lemma ex_distrib_star': "Q * (∃⇩Ax. P x ) = (∃⇩Ax. Q * P x)"
proof -
have "Q * (∃⇩Ax. P x ) = (∃⇩Ax. P x ) * Q"
by (simp add: assn_times_comm)
also have "… = (∃⇩Ax. P x * Q )"
unfolding ex_distrib_star by simp
also have "… = (∃⇩Ax. Q * P x )"
by (simp add: assn_times_comm)
finally show ?thesis .
qed
definition "is_pure_assn a ≡ ∃P. a=↑P"
lemma is_pure_assnE: assumes "is_pure_assn a" obtains P where "a=↑P"
using assms
by (auto simp: is_pure_assn_def)
lemma is_pure_assn_pure[simp, intro!]: "is_pure_assn (↑P)"
by (auto simp add: is_pure_assn_def)
lemma is_pure_assn_basic_simps[simp]:
"is_pure_assn false"
"is_pure_assn emp"
proof -
have "is_pure_assn (↑False)" by rule thus "is_pure_assn false" by simp
have "is_pure_assn (↑True)" by rule thus "is_pure_assn emp" by simp
qed
lemma is_pure_assn_starI[simp,intro!]:
"⟦is_pure_assn a; is_pure_assn b⟧ ⟹ is_pure_assn (a*b)"
by (auto simp: pure_conj[symmetric] elim!: is_pure_assnE)
subsection "some automation"
text {* Move existential quantifiers to the front of assertions *}
lemma ex_assn_move_out[simp]:
"⋀Q R. (∃⇩Ax. Q x) * R = (∃⇩Ax. (Q x * R))"
"⋀Q R. R * (∃⇩Ax. Q x) = (∃⇩Ax. (R * Q x))"
"⋀P Q. (∃⇩Ax. Q x) ∨⇩A P = (∃⇩Ax. (Q x ∨⇩A P))"
"⋀P Q. Q ∨⇩A (∃⇩Ax. P x) = (∃⇩Ax. (Q ∨⇩A P x))"
apply -
apply (simp add: ex_distrib_star)
apply (subst mult.commute)
apply (subst (2) mult.commute)
apply (simp add: ex_distrib_star)
apply (simp add: ex_distrib_or)
apply (subst sup_commute)
apply (subst (2) sup_commute)
apply (simp add: ex_distrib_or)
done
thm merge_true_star
lemma merge_pure_or[simp]:
"↑a ∨⇩A ↑b = ↑(a∨b)"
by(auto intro!: assn_ext simp add: and_assn_conv pure_assn_rule)
thm mod_pure_star_dist
lemmas star_aci =
mult.assoc[where 'a=assn] mult.commute[where 'a=assn] mult.left_commute[where 'a=assn]
assn_one_left mult_1_right[where 'a=assn]
merge_true_star merge_true_star_ctx
lemma entt_star_mono: "⟦entailst A B; entailst C D⟧ ⟹ entailst (A*C) (B*D)"
unfolding entailst_def
proof -
assume a1: "A ⟹⇩A B * true"
assume "C ⟹⇩A D * true"
then have "A * C ⟹⇩A true * B * (true * D)"
using a1 assn_times_comm ent_star_mono by force
then show "A * C ⟹⇩A B * D * true"
by (simp add: ab_semigroup_mult_class.mult.left_commute assn_times_comm)
qed
lemma entt_emp[simp, intro!]:
"entailst A emp"
unfolding entailst_def by simp
declare entails_triv [simp]
lemma entt_star_true_simp[simp]:
"entailst A (B*true) ⟷ entailst A B"
"entailst (A*true) B ⟷ entailst A B"
unfolding entailst_def
subgoal by (auto simp: assn_times_assoc)
subgoal
apply (intro iffI)
subgoal using entails_def mod_star_trueI by blast
subgoal by (metis assn_times_assoc entails_triv ent_star_mono merge_true_star)
done
done
lemma entt_def_true: "(P⟹⇩tQ) ≡ (P*true ⟹⇩A Q*true)"
unfolding entailst_def
apply (rule eq_reflection)
using entailst_def entt_star_true_simp(2) by auto
lemma mod_starD: "h⊨A*B ⟹ ∃h1 h2. h1⊨A ∧ h2⊨B"
by (metis assn_ext mod_star_convE)
lemma ent_ex_preI: "(⋀x. P x ⟹⇩A Q) ⟹ ∃⇩Ax. P x ⟹⇩A Q"
by (meson entails_ex)
lemma ent_ex_postI: "Q ⟹⇩A P x ⟹ Q ⟹⇩A ∃⇩Ax. P x "
using entails_ex_post by blast
lemma entt_frame_fwd:
assumes "entailst P Q"
assumes "entailst A (P*F)"
assumes "entailst (Q*F) B"
shows "entailst A B"
using assms
by (metis entt_refl entt_star_mono entt_trans)
lemma ent_frame_fwd:
assumes R: "P ⟹⇩A R"
assumes F: "Ps ⟹⇩A P*F"
assumes I: "R*F ⟹⇩A Q"
shows "Ps ⟹⇩A Q"
using assms
by (metis entails_triv ent_star_mono ent_trans)
end