# Theory Separation_Logic_Imperative_HOL.Assertions

```section "Assertions"

theory Assertions
imports
"Tools/Syntax_Match"
Automatic_Refinement.Misc
begin

subsection ‹Partial Heaps›
text ‹
A partial heap is modeled by a heap and a set of valid addresses, with the
side condition that the valid addresses have to be within the limit of the
heap. This modeling is somewhat strange for separation logic, however, it
allows us to solve some technical problems related to definition of
Hoare triples, that will be detailed later.
›
type_synonym pheap = "heap × addr set"

text ‹Predicate that expresses that the address set of a partial heap is
within the heap's limit.
›
fun in_range :: "(heap × addr set) ⇒ bool"
where "in_range (h,as) ⟷ (∀a∈as. a < lim h)"

declare in_range.simps[simp del]

lemma in_range_empty[simp, intro!]: "in_range (h,{})"
by (auto simp: in_range.simps)

lemma in_range_dist_union[simp]:
"in_range (h,as ∪ as') ⟷ in_range (h,as) ∧ in_range (h,as')"
by (auto simp: in_range.simps)

lemma in_range_subset:
"⟦as ⊆ as'; in_range (h,as')⟧ ⟹ in_range (h,as)"
by (auto simp: in_range.simps)

text ‹Relation that holds if two heaps are identical on a given
definition relH :: "addr set ⇒ heap ⇒ heap ⇒ bool"
where "relH as h h' ≡
in_range (h,as)
∧ in_range (h',as)
∧ (∀t. ∀a ∈ as.
refs h t a = refs h' t a
∧ arrays h t a = arrays h' t a
)"

lemma relH_in_rangeI:
assumes "relH as h h'"
shows "in_range (h,as)" and "in_range (h',as)"
using assms unfolding relH_def by auto

text "Reflexivity"
lemma relH_refl: "in_range (h,as) ⟹ relH as h h"
unfolding relH_def by simp

text "Symmetry"
lemma relH_sym: "relH as h h' ⟹ relH as h' h"
unfolding relH_def
by auto

text "Transitivity"
lemma relH_trans[trans]: "⟦relH as h1 h2; relH as h2 h3⟧ ⟹ relH as h1 h3"
unfolding relH_def
by auto

lemma relH_dist_union[simp]:
"relH (as∪as') h h' ⟷ relH as h h' ∧ relH as' h h'"
unfolding relH_def
by auto

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)

lemma relH_ref:
assumes "relH as h h'"
shows "Ref.get h r = Ref.get h' r"
using assms unfolding relH_def Ref.get_def by auto

lemma relH_array:
assumes "relH as h h'"
shows "Array.get h r = Array.get h' r"
using assms unfolding relH_def Array.get_def by auto

lemma relH_set_ref: "⟦ addr_of_ref r ∉ as; in_range (h,as)⟧
⟹ relH as h (Ref.set r x h)"
unfolding relH_def Ref.set_def
by (auto simp: in_range.simps)

lemma relH_set_array: "⟦addr_of_array r ∉ as; in_range (h,as)⟧
⟹ relH as h (Array.set r x h)"
unfolding relH_def Array.set_def
by (auto simp: in_range.simps)

subsection ‹Assertions›
text ‹
Assertions are predicates on partial heaps, that fulfill a well-formedness
condition called properness: They only depend on the part of the heap
by the address set, and must be false for partial heaps that are not in range.
›
type_synonym assn_raw = "pheap ⇒ bool"

definition proper :: "assn_raw ⇒ bool" where
"proper P ≡ ∀h h' as. (P (h,as) ⟶ in_range (h,as))
∧ (P (h,as) ∧ relH as h h' ∧ in_range (h',as) ⟶ P (h',as))"

lemma properI[intro?]:
assumes "⋀as h. P (h,as) ⟹ in_range (h,as)"
assumes "⋀as h h'.
⟦P (h,as); relH as h h'; in_range (h',as)⟧ ⟹ P (h',as)"
shows "proper P"
unfolding proper_def using assms by blast

lemma properD1:
assumes "proper P"
assumes "P (h,as)"
shows "in_range (h,as)"
using assms unfolding proper_def by blast

lemma properD2:
assumes "proper P"
assumes "P (h,as)"
assumes "relH as h h'"
assumes "in_range (h',as)"
shows "P (h',as)"
using assms unfolding proper_def by blast

lemmas properD = properD1 properD2

lemma proper_iff:
assumes "proper P"
assumes "relH as h h'"
assumes "in_range (h',as)"
shows "P (h,as) ⟷ P (h',as)"
using assms
by (metis properD2 relH_in_rangeI(1) relH_sym)

text ‹We encapsulate assertions in their own type›
typedef assn = "Collect proper"
apply simp
unfolding proper_def
by fastforce

lemmas [simp] = Rep_assn_inverse Rep_assn_inject
lemmas [simp, intro!] = Rep_assn[unfolded mem_Collect_eq]

lemma Abs_assn_eqI[intro?]:
"(⋀h. P h = Rep_assn Pr h) ⟹ Abs_assn P = Pr"
"(⋀h. P h = Rep_assn Pr h) ⟹ Pr = Abs_assn P"
by (metis Rep_assn_inverse predicate1I xt1(5))+

abbreviation models :: "pheap ⇒ assn ⇒ bool" (infix "⊨" 50)
where "h⊨P ≡ Rep_assn P h"

lemma models_in_range: "h⊨P ⟹ in_range h"
apply (cases h)
by (metis mem_Collect_eq Rep_assn properD1)

subsubsection ‹Empty Partial Heap›
text ‹The empty partial heap satisfies some special properties.
We set up a simplification that tries to rewrite it to the standard
empty partial heap ‹h⇩⊥››
abbreviation h_bot ("h⇩⊥") where "h⇩⊥ ≡ (undefined,{})"
lemma mod_h_bot_indep: "(h,{})⊨P ⟷ (h',{})⊨P"
by (metis mem_Collect_eq Rep_assn emptyE in_range_empty
proper_iff relH_def)

lemma mod_h_bot_normalize[simp]:
"syntax_fo_nomatch undefined h ⟹ (h,{})⊨P ⟷ h⇩⊥ ⊨ P"
using mod_h_bot_indep[where h'=undefined] by simp

text ‹Properness, lifted to the assertion type.›
lemma mod_relH: "relH as h h' ⟹ (h,as)⊨P ⟷ (h',as)⊨P"
by (metis mem_Collect_eq Rep_assn proper_iff relH_in_rangeI(2))

subsection ‹Connectives›
text ‹
We define several operations on assertions, and instantiate some type classes.
›

subsubsection ‹Empty Heap and Separation Conjunction›
text ‹The assertion that describes the empty heap, and the separation
conjunction form a commutative monoid:›
instantiation assn :: one begin
fun one_assn_raw :: "pheap ⇒ bool"
where "one_assn_raw (h,as) ⟷ as={}"

lemma one_assn_proper[intro!,simp]: "proper one_assn_raw"
by (auto intro!: properI)

definition one_assn :: assn where "1 ≡ Abs_assn one_assn_raw"
instance ..
end

abbreviation one_assn::assn ("emp") where "one_assn ≡ 1"

instantiation assn :: times begin
fun times_assn_raw :: "assn_raw ⇒ assn_raw ⇒ assn_raw" where
"times_assn_raw P Q (h,as)
= (∃as1 as2. as=as1∪as2 ∧ as1∩as2={}
∧ P (h,as1) ∧ Q (h,as2))"

lemma times_assn_proper[intro!,simp]:
"proper P ⟹ proper Q ⟹ proper (times_assn_raw P Q)"
apply (rule properI)
apply (auto dest: properD1) []
apply clarsimp
apply (drule (3) properD2)
apply (drule (3) properD2)
apply blast
done

definition times_assn where "P*Q ≡
Abs_assn (times_assn_raw (Rep_assn P) (Rep_assn Q))"

instance ..
end

lemma mod_star_conv: "h⊨A*B
⟷ (∃hr as1 as2. h=(hr,as1∪as2) ∧ as1∩as2={} ∧ (hr,as1)⊨A ∧ (hr,as2)⊨B)"
unfolding times_assn_def
apply (cases h)
by (auto simp: Abs_assn_inverse)

lemma mod_starD: "h⊨A*B ⟹ ∃h1 h2. h1⊨A ∧ h2⊨B"
by (auto simp: mod_star_conv)

lemma star_assnI:
assumes "(h,as)⊨P" and "(h,as')⊨Q" and "as∩as'={}"
shows "(h,as∪as')⊨P*Q"
using assms unfolding times_assn_def
by (auto simp: Abs_assn_inverse)

instantiation assn :: comm_monoid_mult begin
lemma assn_one_left: "1*P = (P::assn)"
unfolding one_assn_def times_assn_def
apply (rule)
apply (auto simp: Abs_assn_inverse)
done

lemma assn_times_comm: "P*Q = Q*(P::assn)"
unfolding times_assn_def
apply rule
apply (fastforce simp add: Abs_assn_inverse Un_ac)
done

lemma assn_times_assoc: "(P*Q)*R = P*(Q*(R::assn))"
unfolding times_assn_def
apply rule
apply (auto simp: Abs_assn_inverse)
apply (rule_tac x="as1∪as1a" in exI)
apply (rule_tac x="as2a" in exI)
apply (auto simp add: Un_ac) []

apply (rule_tac x="as1a" in exI)
apply (rule_tac x="as2a∪as2" in exI)
apply (fastforce simp add: Un_ac) []
done

instance
apply standard
apply (rule assn_times_assoc)
apply (rule assn_times_comm)
apply (rule assn_one_left)
done

end

subsubsection ‹Magic Wand›
fun wand_raw :: "assn_raw ⇒ assn_raw ⇒ assn_raw" where
"wand_raw P Q (h,as) ⟷ in_range (h,as)
∧ (∀h' as'. as∩as'={} ∧ relH as h h' ∧ in_range (h',as)
∧ P (h',as')
⟶ Q (h',as∪as'))"

lemma wand_proper[simp, intro!]: "proper (wand_raw P Q)"
apply (rule properI)
apply simp
apply (auto dest: relH_trans)
done

definition
wand_assn :: "assn ⇒ assn ⇒ assn" (infixl "-*" 56)
where "P-*Q ≡ Abs_assn (wand_raw (Rep_assn P) (Rep_assn Q))"

lemma wand_assnI:
assumes "in_range (h,as)"
assumes "⋀h' as'. ⟦
as ∩ as' = {};
relH as h h';
in_range (h',as);
(h',as')⊨Q
⟧ ⟹ (h',as∪as') ⊨ R"
shows "(h,as) ⊨ Q -* R"
using assms
unfolding wand_assn_def
apply (auto simp: Abs_assn_inverse)
done

subsubsection ‹Boolean Algebra on Assertions›
instantiation assn :: boolean_algebra begin
definition top_assn where "top ≡ Abs_assn in_range"
definition bot_assn where "bot ≡ Abs_assn (λ_. False)"
definition sup_assn where "sup P Q ≡ Abs_assn (λh. h⊨P ∨ h⊨Q)"
definition inf_assn where "inf P Q ≡ Abs_assn (λh. h⊨P ∧ h⊨Q)"
definition uminus_assn where
"-P ≡ Abs_assn (λh. in_range h ∧ ¬h⊨P)"

lemma bool_assn_proper[simp, intro!]:
"proper in_range"
"proper (λ_. False)"
"proper P ⟹ proper Q ⟹ proper (λh. P h ∨ Q h)"
"proper P ⟹ proper Q ⟹ proper (λh. P h ∧ Q h)"
"proper P ⟹ proper (λh. in_range h ∧ ¬P h)"
apply (auto
intro!: properI
intro: relH_in_rangeI
dest: properD1
simp: proper_iff)
done

text ‹(And, Or, True, False, Not) are a Boolean algebra.
Due to idiosyncrasies of the Isabelle/HOL class setup, we have to
also define a difference and an ordering:›
definition less_eq_assn where
[simp]: "(a::assn) ≤ b ≡ a = inf a b"

definition less_assn where
[simp]: "(a::assn) < b ≡ a ≤ b ∧ a≠b"

definition minus_assn where
[simp]: "(a::assn) - b ≡ inf a (-b)"

instance
apply standard
unfolding
top_assn_def bot_assn_def sup_assn_def inf_assn_def uminus_assn_def
less_eq_assn_def less_assn_def minus_assn_def
apply (auto
simp: Abs_assn_inverse conj_commute conj_ac
intro: Abs_assn_eqI models_in_range)
apply rule
apply (metis (mono_tags) Abs_assn_inverse[unfolded mem_Collect_eq]
Rep_assn[unfolded mem_Collect_eq] bool_assn_proper(4))
apply rule
apply (metis (mono_tags)
Abs_assn_inverse[unfolded mem_Collect_eq]
Rep_assn[unfolded mem_Collect_eq] bool_assn_proper(4))
apply rule
apply (metis (mono_tags)
Abs_assn_inverse[unfolded mem_Collect_eq]
Rep_assn[unfolded mem_Collect_eq] bool_assn_proper(4))
done

end

text ‹We give the operations some more standard names›
abbreviation top_assn::assn ("true") where "top_assn ≡ top"
abbreviation bot_assn::assn ("false") where "bot_assn ≡ bot"
abbreviation sup_assn::"assn⇒assn⇒assn" (infixr "∨⇩A" 61)
where "sup_assn ≡ sup"
abbreviation inf_assn::"assn⇒assn⇒assn" (infixr "∧⇩A" 62)
where "inf_assn ≡ inf"
abbreviation uminus_assn::"assn ⇒ assn" ("¬⇩A _" [81] 80)
where "uminus_assn ≡ uminus"

text ‹Now we prove some relations between the Boolean algebra operations
and the (empty heap,separation conjunction) monoid›

lemma star_false_left[simp]: "false * P = false"
unfolding times_assn_def bot_assn_def
apply rule
done

lemma star_false_right[simp]: "P * false = false"
using star_false_left by (simp add: assn_times_comm)

lemmas star_false = star_false_left star_false_right

lemma assn_basic_inequalities[simp, intro!]:
"true ≠ emp" "emp ≠ true"
"false ≠ emp" "emp ≠ false"
"true ≠ false" "false ≠ true"
subgoal
unfolding one_assn_def top_assn_def
proof (subst Abs_assn_inject; simp?)
have "in_range (⦇arrays = (λ_ _. []), refs = (λ_ _. 0), lim = 1⦈,{0})" (is "in_range ?h")
by (auto simp: in_range.simps)
moreover have "¬one_assn_raw ?h" by auto
ultimately show "in_range ≠ one_assn_raw" by auto
qed
subgoal
by (simp add: ‹true ≠ emp›)
subgoal
using star_false_left ‹true ≠ emp› by force
subgoal
by (simp add: ‹false ≠ emp›)
subgoal
by (metis inf_bot_right inf_top.right_neutral ‹true ≠ emp›)
subgoal
using ‹true ≠ false› by auto
done

subsubsection ‹Existential Quantification›
definition ex_assn :: "('a ⇒ assn) ⇒ assn" (binder "∃⇩A" 11)
where "(∃⇩Ax. P x) ≡ Abs_assn (λh. ∃x. h⊨P x)"

lemma ex_assn_proper[simp, intro!]:
"(⋀x. proper (P x)) ⟹ proper (λh. ∃x. P x h)"
by (auto intro!: properI dest: properD1 simp: proper_iff)

lemma ex_assn_const[simp]: "(∃⇩Ax. c) = c"
unfolding ex_assn_def by auto

lemma ex_one_point_gen:
"⟦⋀h x. h⊨P x ⟹ x=v⟧ ⟹ (∃⇩Ax. P x) = (P v)"
unfolding ex_assn_def
apply rule
apply auto
done

lemma ex_distrib_star: "(∃⇩Ax. P x * Q) = (∃⇩Ax. P x) * Q"
unfolding ex_assn_def times_assn_def
apply rule
apply fastforce
done

lemma ex_distrib_and: "(∃⇩Ax. P x ∧⇩A Q) = (∃⇩Ax. P x) ∧⇩A Q"
unfolding ex_assn_def inf_assn_def
apply rule
done

lemma ex_distrib_or: "(∃⇩Ax. P x ∨⇩A Q) = (∃⇩Ax. P x) ∨⇩A Q"
unfolding ex_assn_def sup_assn_def
apply rule
done

lemma ex_join_or: "(∃⇩Ax. P x ∨⇩A (∃⇩Ax. Q x)) = (∃⇩Ax. P x ∨⇩A Q x)"
unfolding ex_assn_def sup_assn_def
apply rule
done

subsubsection ‹Pure Assertions›
text ‹Pure assertions do not depend on any heap content.›
fun pure_assn_raw where "pure_assn_raw b (h,as) ⟷ as={} ∧ b"
definition pure_assn :: "bool ⇒ assn" ("↑") where
"↑b ≡ Abs_assn (pure_assn_raw b)"

lemma pure_assn_proper[simp, intro!]: "proper (pure_assn_raw b)"
by (auto intro!: properI intro: relH_in_rangeI)

lemma pure_true[simp]: "↑True = emp"
unfolding pure_assn_def one_assn_def
apply rule
apply (auto)
done

lemma pure_false[simp]: "↑False = false"
unfolding pure_assn_def bot_assn_def
apply rule
apply (auto simp: Abs_assn_inverse)
done

lemma pure_assn_eq_false_iff[simp]: "↑P = false ⟷ ¬P" by auto

lemma pure_assn_eq_emp_iff[simp]: "↑P = emp ⟷ P" by (cases P) auto

lemma merge_pure_star[simp]:
"↑a * ↑b = ↑(a∧b)"
unfolding times_assn_def
apply rule
unfolding pure_assn_def
apply fastforce
done

lemma merge_true_star[simp]: "true*true = true"
unfolding times_assn_def top_assn_def
apply rule
apply (fastforce simp: in_range.simps)
done

lemma merge_pure_and[simp]:
"↑a ∧⇩A ↑b = ↑(a∧b)"
unfolding inf_assn_def
apply rule
unfolding pure_assn_def
apply fastforce
done

lemma merge_pure_or[simp]:
"↑a ∨⇩A ↑b = ↑(a∨b)"
unfolding sup_assn_def
apply rule
unfolding pure_assn_def
apply fastforce
done

lemma pure_assn_eq_conv[simp]: "↑P = ↑Q ⟷ P=Q" by auto

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)"

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 elim!: is_pure_assnE)

subsubsection ‹Pointers›
text ‹In Imperative HOL, we have to distinguish between pointers to single
values and pointers to arrays. For both, we define assertions that
describe the part of the heap that a pointer points to.›
fun sngr_assn_raw :: "'a::heap ref ⇒ 'a ⇒ assn_raw" where
"sngr_assn_raw r x (h,as) ⟷ Ref.get h r = x ∧ as = {addr_of_ref r} ∧

lemma sngr_assn_proper[simp, intro!]: "proper (sngr_assn_raw r x)"
apply (auto intro!: properI simp: relH_ref)
apply (auto simp add: in_range.simps dest: relH_in_rangeI)
done

definition sngr_assn :: "'a::heap ref ⇒ 'a ⇒ assn" (infix "↦⇩r" 82)
where "r↦⇩rx ≡ Abs_assn (sngr_assn_raw r x)"

fun snga_assn_raw :: "'a::heap array ⇒ 'a list ⇒ assn_raw"
where "snga_assn_raw r x (h,as)
⟷ Array.get h r = x ∧ as = {addr_of_array r}
∧ addr_of_array r < lim h"

lemma snga_assn_proper[simp, intro!]: "proper (snga_assn_raw r x)"
apply (auto intro!: properI simp: relH_array)
apply (auto simp add: in_range.simps dest: relH_in_rangeI)
done

definition
snga_assn :: "'a::heap array ⇒ 'a list ⇒ assn" (infix "↦⇩a" 82)
where "r↦⇩aa ≡ Abs_assn (snga_assn_raw r a)"

text ‹Two disjoint parts of the heap cannot be pointed to by the
same pointer›
lemma sngr_same_false[simp]:
"p ↦⇩r x * p ↦⇩r y = false"
unfolding times_assn_def bot_assn_def sngr_assn_def
apply rule
apply (auto simp: Abs_assn_inverse)
done

lemma snga_same_false[simp]:
"p ↦⇩a x * p ↦⇩a y = false"
unfolding times_assn_def bot_assn_def snga_assn_def
apply rule
apply (auto simp: Abs_assn_inverse)
done

subsection ‹Properties of the Models-Predicate›
lemma mod_true[simp]: "h⊨true ⟷ in_range h"
unfolding top_assn_def by (simp add: Abs_assn_inverse)
lemma mod_false[simp]: "¬ h⊨false"
unfolding bot_assn_def by (simp add: Abs_assn_inverse)

lemma mod_emp: "h⊨emp ⟷ snd h = {}"
unfolding one_assn_def by (cases h) (simp add: Abs_assn_inverse)

lemma mod_emp_simp[simp]: "(h,{})⊨emp"

lemma mod_pure[simp]: "h⊨↑b ⟷ snd h = {} ∧ b"
unfolding pure_assn_def
apply (cases h)
done

lemma mod_ex_dist[simp]: "h⊨(∃⇩Ax. P x) ⟷ (∃x. h⊨P x)"
unfolding ex_assn_def by (auto simp: Abs_assn_inverse)

lemma mod_exI: "∃x. h⊨P x ⟹ h⊨(∃⇩Ax. P x)"
by (auto simp: mod_ex_dist)
lemma mod_exE: assumes "h⊨(∃⇩Ax. P x)" obtains x where "h⊨P x"
using assms by (auto simp: mod_ex_dist)

(* Not declared as simp, to not interfere with precision.
TODO: Perhaps define own connector for precision claims?
*)
lemma mod_and_dist: "h⊨P∧⇩AQ ⟷ h⊨P ∧ h⊨Q"
unfolding inf_assn_def by (simp add: Abs_assn_inverse)

lemma mod_or_dist[simp]: "h⊨P∨⇩AQ ⟷ h⊨P ∨ h⊨Q"
unfolding sup_assn_def by (simp add: Abs_assn_inverse)

lemma mod_not_dist[simp]: "h⊨(¬⇩AP) ⟷ in_range h ∧ ¬ h⊨P"
unfolding uminus_assn_def by (simp add: Abs_assn_inverse)

lemma mod_pure_star_dist[simp]: "h⊨P*↑b ⟷ h⊨P ∧ b"
by (metis (full_types) mod_false mult_1_right pure_false
pure_true star_false_right)

lemmas mod_dist = mod_pure mod_pure_star_dist mod_ex_dist mod_and_dist
mod_or_dist mod_not_dist

lemma mod_star_trueI: "h⊨P ⟹ h⊨P*true"
unfolding times_assn_def top_assn_def
apply (cases h)
apply auto
done

lemma mod_star_trueE': assumes "h⊨P*true" obtains h' where
"fst h' = fst h" and "snd h' ⊆ snd h" and "h'⊨P"
using assms
unfolding times_assn_def top_assn_def
apply (cases h)
done

lemma mod_star_trueE: assumes "h⊨P*true" obtains h' where "h'⊨P"
using assms by (blast elim: mod_star_trueE')

lemma mod_h_bot_iff[simp]:
"(h,{}) ⊨ ↑b ⟷ b"
"(h,{}) ⊨ true"
"(h,{}) ⊨ p↦⇩rx ⟷ False"
"(h,{}) ⊨ q↦⇩ay ⟷ False"
"(h,{}) ⊨ P*Q ⟷ ((h,{}) ⊨ P) ∧ ((h,{}) ⊨ Q)"
"(h,{}) ⊨ P∧⇩AQ ⟷ ((h,{}) ⊨ P) ∧ ((h,{}) ⊨ Q)"
"(h,{}) ⊨ P∨⇩AQ ⟷ ((h,{}) ⊨ P) ∨ ((h,{}) ⊨ Q)"
"(h,{}) ⊨ (∃⇩Ax. R x) ⟷ (∃x. (h,{}) ⊨ R x)"
apply simp
done

subsection ‹Entailment›
definition entails :: "assn ⇒ assn ⇒ bool" (infix "⟹⇩A" 10)
where "P ⟹⇩A Q ≡ ∀h. h⊨P ⟶ h⊨Q"

lemma entailsI:
assumes "⋀h. h⊨P ⟹ h⊨Q"
shows "P ⟹⇩A Q"
using assms unfolding entails_def by auto

lemma entailsD:
assumes "P ⟹⇩A Q"
assumes "h⊨P"
shows "h⊨Q"
using assms unfolding entails_def by blast

subsubsection ‹Properties›
lemma ent_fwd:
assumes "h⊨P"
assumes "P ⟹⇩A Q"
shows "h⊨Q" using assms(2,1) by (rule entailsD)

lemma ent_refl[simp]: "P ⟹⇩A P"
by (auto simp: entailsI)

lemma ent_trans[trans]: "⟦ P ⟹⇩A Q; Q ⟹⇩AR ⟧ ⟹ P ⟹⇩A R"
by (auto intro: entailsI dest: entailsD)

lemma ent_iffI:
assumes "A⟹⇩AB"
assumes "B⟹⇩AA"
shows "A=B"
apply (subst Rep_assn_inject[symmetric])
apply (rule ext)
using assms unfolding entails_def
by blast

lemma ent_false[simp]: "false ⟹⇩A P"
by (auto intro: entailsI)
lemma ent_true[simp]: "P ⟹⇩A true"
by (auto intro!: entailsI simp: models_in_range)

lemma ent_false_iff[simp]: "(P ⟹⇩A false) ⟷ (∀h. ¬h⊨P)"
unfolding entails_def
by auto

lemma ent_pure_pre_iff[simp]: "(P*↑b ⟹⇩A Q) ⟷ (b ⟶ (P ⟹⇩A Q))"
unfolding entails_def

lemma ent_pure_pre_iff_sng[simp]:
"(↑b ⟹⇩A Q) ⟷ (b ⟶ (emp ⟹⇩A Q))"
using ent_pure_pre_iff[where P=emp]
by simp

lemma ent_pure_post_iff[simp]:
"(P ⟹⇩A Q*↑b) ⟷ ((∀h. h⊨P ⟶ b) ∧ (P ⟹⇩A Q))"
unfolding entails_def

lemma ent_pure_post_iff_sng[simp]:
"(P ⟹⇩A ↑b) ⟷ ((∀h. h⊨P ⟶ b) ∧ (P ⟹⇩A emp))"
using ent_pure_post_iff[where Q=emp]
by simp

lemma ent_ex_preI: "(⋀x. P x ⟹⇩A Q) ⟹ ∃⇩Ax. P x ⟹⇩A Q"
unfolding entails_def ex_assn_def
by (auto simp: Abs_assn_inverse)

lemma ent_ex_postI: "(P ⟹⇩A Q x) ⟹ P ⟹⇩A ∃⇩Ax. Q x"
unfolding entails_def ex_assn_def
by (auto simp: Abs_assn_inverse)

lemma ent_mp: "(P * (P -* Q)) ⟹⇩A Q"
apply (rule entailsI)
unfolding times_assn_def wand_assn_def
apply (drule_tac x="a" in spec)
apply (drule_tac x="as1" in spec)
apply (auto simp: Un_ac relH_refl)
done

lemma ent_star_mono: "⟦ P ⟹⇩A P'; Q ⟹⇩A Q'⟧ ⟹ P*Q ⟹⇩A P'*Q'"
unfolding entails_def times_assn_def
apply metis
done

lemma ent_wandI:
assumes IMP: "Q*P ⟹⇩A R"
shows "P ⟹⇩A (Q -* R)"
unfolding entails_def
apply clarsimp
apply (rule wand_assnI)
apply (blast intro: models_in_range)
proof -
fix h as h' as'
assume "(h,as)⊨P"
and "as∩as'={}"
and "relH as h h'"
and "in_range (h',as)"
and "(h',as') ⊨ Q"

from ‹(h,as)⊨P› and ‹relH as h h'› have "(h',as)⊨P"
with ‹(h',as') ⊨ Q› and ‹as∩as'={}› have "(h',as∪as')⊨Q*P"
by (metis star_assnI Int_commute Un_commute)
with IMP show "(h',as∪as') ⊨ R" by (blast dest: ent_fwd)
qed

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"

lemma ent_disjI2_direct[simp]: "B ⟹⇩A A ∨⇩A B"

lemma ent_disjE: "⟦ A⟹⇩AC; B⟹⇩AC ⟧ ⟹ A∨⇩AB ⟹⇩AC"
unfolding entails_def by auto

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)

lemma star_or_dist1:
"(A ∨⇩A B)*C = (A*C ∨⇩A B*C)"
apply (rule ent_iffI)
unfolding entails_def

lemma star_or_dist2:
"C*(A ∨⇩A B) = (C*A ∨⇩A C*B)"
apply (rule ent_iffI)
unfolding entails_def

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)

lemma triv_exI[simp, intro!]: "Q x ⟹⇩A ∃⇩Ax. Q x"
by (meson ent_ex_postI ent_refl)

subsubsection ‹Weak Entails›
text ‹Weakening of entails to allow arbitrary unspecified memory in conclusion›
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 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 entt_refl[simp, intro!]: "entailst A A"
unfolding entailst_def

lemma entt_true[simp, intro!]:
"entailst A true"
unfolding entailst_def by simp

lemma entt_emp[simp, intro!]:
"entailst A emp"
unfolding entailst_def by 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 ent_refl ent_star_mono merge_true_star)
done
done

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"
qed

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 enttI_true: "P*true ⟹⇩A Q*true ⟹ P⟹⇩tQ"
by (drule enttI) simp

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 ent_imp_entt: "P⟹⇩AQ ⟹ P⟹⇩tQ"
apply (rule enttI)
apply (erule ent_trans)

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"
by (auto simp: entailst_def entails_def star_or_dist)

lemma entt_disjI2': "A⟹⇩tC ⟹ A⟹⇩tB∨⇩AC"
by (auto simp: entailst_def entails_def star_or_dist)

lemma entt_disjE: "⟦ A⟹⇩tM; B⟹⇩tM ⟧ ⟹ A∨⇩AB ⟹⇩t M"
using ent_disjE enttD enttI by blast

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

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 precise_extr_pure[simp]:
"precise (λx y. ↑P * R x y) ⟷ (P ⟶ precise R)"
"precise (λx y. R x y * ↑P) ⟷ (P ⟶ precise R)"
apply (cases P, (auto intro!: preciseI) [2])+
done

lemma sngr_prec: "precise (λx p. p↦⇩rx)"
apply rule
apply (clarsimp simp: mod_and_dist)
unfolding sngr_assn_def times_assn_def