Theory Sep_Algebra_Add
section ‹Additions to Separation Algebra Library›
theory Sep_Algebra_Add
imports "Separation_Algebra.Sep_Tactics"
"HOL-Library.Function_Algebras" "HOL-Library.Product_Plus"
begin
no_notation pred_K ("⟨_⟩")
hide_const (open) Separation_Algebra.pure
subsection ‹Simp-Lemmas for Separation Algebra›
named_theorems sep_algebra_simps ‹Advanced simplification lemmas for separation algebra›
lemmas [sep_algebra_simps] = sep_conj_exists sep_add_ac
lemmas [simp] = sep_conj_assoc
lemmas sep_conj_c = sep_conj_commute sep_conj_left_commute
lemmas sep_conj_aci = sep_conj_ac sep_conj_empty sep_conj_empty'
subsection ‹Separation Algebra with a Unique Zero›
class unique_zero_sep_algebra = stronger_sep_algebra +
assumes unique_zero: "x##x ⟹ x=0"
begin
lemma unique_zero_simps[simp]:
"a##a ⟷ a=0"
"a##b ⟹ a+b = a ⟷ b=0"
"a##b ⟹ a+b = b ⟷ a=0"
"a##b ⟹ a + b = 0 ⟷ a=0 ∧ b=0"
apply -
using local.sep_disj_zero local.unique_zero apply blast
apply (metis local.sep_add_disjD local.sep_add_zero local.unique_zero)
apply (metis local.sep_add_disjD local.sep_add_zero_sym local.sep_disj_commute local.unique_zero)
by (metis local.sep_add_disjD local.sep_add_zero local.sep_disj_zero local.unique_zero)
end
subsection ‹Standard Instantiations›
thm plus_fun_def
thm zero_fun_def
instantiation "fun" :: (type,stronger_sep_algebra) stronger_sep_algebra
begin
definition "f1 ## f2 ⟷ (∀x. f1 x ## f2 x)"
instance
apply standard
unfolding sep_disj_fun_def plus_fun_def zero_fun_def
apply (auto)
subgoal
by (simp add: sep_disj_commute)
subgoal
using sep_add_commute by auto
subgoal
by (simp add: sep_add_assoc)
done
end
lemma plus_fun_alt[simp]: "(f1 + f2) x = (f1 x + f2 x)"
by auto
lemma zero_fun_alt[simp]: "0 x ≡ 0"
by auto
instance "fun" :: (type,unique_zero_sep_algebra) unique_zero_sep_algebra
apply standard
unfolding sep_disj_fun_def plus_fun_def zero_fun_def
by (metis unique_zero)
lemma disj_fun_upd_iff[simp]:
"⟦f a = 0; g a = 0⟧ ⟹ (f(a:=x) ## g(a:=y)) ⟷ (f ## g ∧ x ## y)"
unfolding sep_disj_fun_def by force
lemma fun_upd_Z_Z[simp]: "fun_upd 0 i 0 = 0" by auto
lemma sep_disj_fun_updI[sep_algebra_simps, intro]: "⟦f##g; a##b⟧ ⟹ f(x:=a) ## g(x:=b)"
by (simp add: sep_disj_fun_def)
lemma sep_disj_fun_Zupd_eq[sep_algebra_simps]:
"f##0(x:=y) ⟷ f x ## y"
"0(x:=y) ## f ⟷ y ## f x"
by (auto simp add: sep_disj_fun_def)
lemma sep_disj_funD: "f##g ⟹ f x ## g x" by (auto simp: sep_disj_fun_def)
lemma merge_fun_singleton: "fun_upd 0 i (a::'c::pre_sep_algebra) + fun_upd 0 i b = fun_upd 0 i (a+b)"
by auto
lemma split_fun_upd_0: "fun_upd (a+b) i (0::'c::pre_sep_algebra) = fun_upd a i 0 + fun_upd b i 0"
by auto
instantiation option :: (stronger_sep_algebra) stronger_sep_algebra begin
fun sep_disj_option :: "'a option ⇒ 'a option ⇒ bool" where
"sep_disj None None ⟷ True"
| "sep_disj None (Some _) ⟷ True"
| "sep_disj (Some _) None ⟷ True"
| "sep_disj (Some x) (Some y) ⟷ x##y"
lemma sep_disj_option_add_simps[simp]:
"sep_disj None x"
"sep_disj x None"
by (cases x; simp)+
fun plus_option :: "'a option ⇒ 'a option ⇒ 'a option" where
"plus None None = None"
| "plus None (Some x) = Some x"
| "plus (Some x) None = Some x"
| "plus (Some x) (Some y) = Some (x+y)"
lemma plus_option_add_simps[simp]: "plus None x = x" "plus x None = x"
by (cases x; simp)+
definition "0 = None"
instance
apply standard
apply (simp_all add: zero_option_def)
apply (case_tac x; case_tac y; simp add: sep_disj_commute)
apply (case_tac x; case_tac y; auto simp add: sep_disj_commute sep_add_commute)
apply (case_tac x; case_tac y; case_tac z; simp add: sep_add_assoc)
apply (case_tac x; case_tac y; case_tac z; auto dest: sep_disj_addD1)
done
end
instantiation prod :: (stronger_sep_algebra, stronger_sep_algebra) stronger_sep_algebra
begin
definition "a##b ⟷ fst a ## fst b ∧ snd a ## snd b"
instance
apply standard
unfolding sep_disj_prod_def plus_prod_def zero_prod_def
by (auto
simp: sep_add_ac
intro: sep_disj_commuteI sep_disj_addD1 sep_disj_addI1)
end
lemma sep_disj_prod_lower[sep_algebra_simps]: "(a,b) ## (c,d) ⟷ a##c ∧ b##d"
by (simp add: sep_disj_prod_def)
lemma plus_prod_lower[sep_algebra_simps]: "(a,b) + (c,d) = (a+c,b+d)"
by (simp add: plus_prod_def)
instance prod :: (unique_zero_sep_algebra,unique_zero_sep_algebra) unique_zero_sep_algebra
by standard (auto simp: zero_prod_def sep_algebra_simps)
lemma prod_Z_lower[sep_algebra_simps]:
"(a,b) = 0 ⟷ a=0 ∧ b=0"
"0 = (a,b) ⟷ a=0 ∧ b=0"
by (auto simp: zero_prod_def)
lemma plus_prod_eqI: "(a+b,c+d) = (a,c) + (b,d)" by (simp add: sep_algebra_simps)
lemma fst_Z[simp]: "fst 0 = 0" by (simp add: zero_prod_def)
lemma snd_Z[simp]: "snd 0 = 0" by (simp add: zero_prod_def)
lemma fst_plus[sep_algebra_simps]: "fst (a+b) = fst a + fst b" by (auto simp: plus_prod_def)
lemma snd_plus[sep_algebra_simps]: "snd (a+b) = snd a + snd b" by (auto simp: plus_prod_def)
lemma disj_fstI[sep_algebra_simps]: "a##b ⟹ fst a ## fst b" by (auto simp: sep_disj_prod_def)
lemma disj_sndI[sep_algebra_simps]: "a##b ⟹ snd a ## snd b" by (auto simp: sep_disj_prod_def)
datatype 'a tsa_opt = ZERO | TRIV (the_tsa: 'a)
instantiation tsa_opt :: (type) unique_zero_sep_algebra begin
definition sep_disj_tsa_opt :: "'a tsa_opt ⇒ 'a tsa_opt ⇒ bool"
where "a##b ⟷ a=ZERO ∨ b=ZERO"
definition "a+b ≡ (case (a,b) of (ZERO,x) ⇒ x | (x,ZERO) ⇒ x)"
definition "0 = ZERO"
instance
apply standard
by (auto simp: zero_tsa_opt_def sep_disj_tsa_opt_def plus_tsa_opt_def split: tsa_opt.splits)
end
instance tsa_opt :: (type) cancellative_sep_algebra
apply standard
by (auto simp: zero_tsa_opt_def sep_disj_tsa_opt_def plus_tsa_opt_def split: tsa_opt.splits)
lemma TRIV_not_zero[simp]: "TRIV x ≠ 0" "0≠TRIV x" by (auto simp: zero_tsa_opt_def)
lemma TRIV_Z_lower[intro!]:
"ZERO = 0"
"0 = ZERO"
by (auto simp: zero_tsa_opt_def)
lemma triv_Z_lower2[sep_algebra_simps]:
"x + ZERO = x"
"ZERO + x = x"
by (auto simp: zero_tsa_opt_def plus_tsa_opt_def split: tsa_opt.splits)
lemma TRIV_disj_simps[sep_algebra_simps]:
"TRIV a ## b ⟷ b=ZERO"
"b ## TRIV a ⟷ b=ZERO"
by (auto simp: sep_disj_tsa_opt_def)
subsection ‹Additional Simplifier Setup›
lemma sep_empty_app[sep_algebra_simps]: "□ h ⟷ h=0"
by (simp add: sep_empty_def)
lemma sep_empty_I[sep_algebra_simps]: "(λh. h=0) = □"
by (simp add: sep_empty_def)
lemma sep_triv_ineqs[simp]:
"□ ≠ sep_false"
"sep_true ≠ sep_false"
"sep_false ≠ □"
"sep_false ≠ sep_true"
by (auto dest: fun_cong)
lemma sep_true_not_empty:
assumes "(a::'a::sep_algebra) ≠ (b::'a)"
shows "(□::'a⇒bool) ≠ sep_true"
by (metis (mono_tags, lifting) assms sep_empty_I)
subsection ‹Pure Assertions›
text ‹The Separation Algebra entry only defines @{term "pred_K Φ"}, which
makes no constraint on the heap. We define ‹↑Φ›, which requires an empty heap,
and is more natural when using separation logic with deallocation.
›
definition pred_lift :: "bool ⇒ 'a::sep_algebra ⇒ bool" ("↑_" [100] 100)
where "(↑Φ) s ≡ Φ ∧ □ s"
text ‹Relation between ‹pred_lift› and ‹pred_K›. Warning, do not use
as simp-lemma, as ‹sep_true› is an abbreviation for ‹⟨True⟩››
lemma "pred_K Φ = (↑Φ ** sep_true)" by (auto simp: pred_lift_def sep_conj_def sep_algebra_simps)
lemma pred_lift_merge_simps[sep_algebra_simps]:
"(↑Φ ** ↑Ψ) = (↑(Φ∧Ψ))"
"(↑Φ ** ↑Ψ ** B) = (↑(Φ∧Ψ) ** B)"
by (auto simp: pred_lift_def sep_conj_def sep_algebra_simps)
lemma pred_lift_move_front_simps[sep_algebra_simps]:
"NO_MATCH (↑X) A ⟹ (A ** ↑Φ ** B) = (↑Φ ** A ** B)"
"NO_MATCH (↑X) A ⟹ (A ** ↑Φ) = (↑Φ ** A)"
by (auto simp: pred_lift_def sep_conj_def sep_algebra_simps)
lemmas pred_lift_move_merge_simps = pred_lift_merge_simps pred_lift_move_front_simps
lemma pred_lift_extract_simps:
"(↑Φ) h ⟷ Φ ∧ h=0"
"(↑Φ ** A) h ⟷ Φ ∧ A h"
by (auto simp: pred_lift_def sep_conj_def sep_algebra_simps)
lemma pure_true_conv[sep_algebra_simps]: "↑True = □" by (auto simp: sep_algebra_simps pred_lift_extract_simps)
lemma pred_lift_false_conv[simp]: "↑False = sep_false" by (auto simp: sep_algebra_simps pred_lift_extract_simps)
lemma pure_assn_eq_conv[simp]: "(↑Φ) = (↑Ψ) ⟷ Φ=Ψ"
by (smt pred_lift_extract_simps(1))
lemmas sep_conj_false_simps =
pred_lift_false_conv
sep_conj_false_left sep_conj_false_right
definition sep_is_pure_assn :: "('a::sep_algebra ⇒ bool) ⇒ bool" where
"sep_is_pure_assn A ≡ ∀s. A s ⟶ s=0"
definition pure_part :: "('a::sep_algebra ⇒ bool) ⇒ bool" where
"pure_part A ≡ Ex A"
lemma pure_partI: "A s ⟹ pure_part A" by (auto simp: pure_part_def)
lemma pure_part_pure_eq[simp]: "sep_is_pure_assn A ⟹ ↑pure_part A = A"
apply (rule ext)
by (auto simp: sep_is_pure_assn_def pure_part_def pred_lift_def sep_algebra_simps)
lemma pure_part_triv_simps[simp]:
"¬pure_part sep_false"
"pure_part □"
by (auto simp: pure_part_def)
lemma pure_part_pure[simp]: "pure_part (↑Φ) = Φ"
by (auto simp: pure_part_def sep_algebra_simps pred_lift_def)
lemma pure_part_split_conj: "pure_part (A**B) ⟹ pure_part A ∧ pure_part B"
by (auto simp: pure_part_def sep_conj_def)
lemma sep_is_pure_lift_pred[simp]: "sep_is_pure_assn (↑Φ)"
by (auto simp: sep_is_pure_assn_def pred_lift_def sep_algebra_simps)
lemma sep_is_pure_assn_false[simp]: "sep_is_pure_assn sep_false" by (auto simp: sep_is_pure_assn_def)
lemma sep_is_pure_assn_empty[simp]: "sep_is_pure_assn □" by (auto simp: sep_is_pure_assn_def sep_algebra_simps)
lemma sep_is_pure_assn_conjI: "sep_is_pure_assn A ⟹ sep_is_pure_assn B ⟹ sep_is_pure_assn (A**B)"
by (auto simp: sep_is_pure_assn_def sep_conj_def)
lemma pure_part_pure_conj_eq: "pure_part (↑P ** Q) ⟷ P ∧ pure_part Q"
unfolding pure_part_def by (auto simp: sep_algebra_simps pred_lift_extract_simps)
lemma and_pure_true: "((A ** F) and ((↑Φ ** sep_true) ** F)) s ⟶ ((↑Φ ** A) ** F) s"
unfolding sep_conj_def pred_lift_def
by (auto simp: sep_algebra_simps)
subsection ‹Exact Assertion›
definition EXACT :: "'a::sep_algebra ⇒ 'a ⇒ bool" where [simp]: "EXACT h h' ≡ h'=h"
lemma strictly_exact_EXACT[simp]: "strictly_exact (EXACT h)"
unfolding EXACT_def by (auto intro: strictly_exactI)
lemma EXACT_split: "a##b ⟹ EXACT (a+b) = (EXACT a ** EXACT b)"
unfolding EXACT_def sep_conj_def by auto
lemma EXACT_zero[simp]: "EXACT 0 = □" by (auto simp: sep_algebra_simps)
lemma EXACT_eq_iff[simp]: "EXACT a = EXACT b ⟷ a=b"
unfolding EXACT_def by metis
subsection ‹List-Sum over Separation Algebra›
definition "sepsum_list l ≡ foldr (+) l (0::_::stronger_sep_algebra)"
lemma sepsum_list_simps[simp]:
"sepsum_list [] = 0"
"sepsum_list (x#xs) = x + sepsum_list xs"
by (auto simp: sepsum_list_def)
context begin
private named_theorems ss
private definition "sep_ldisj1 x ys ≡ ∀y∈List.set ys. x##y"
private lemma sep_ldisj1_simps[ss]:
"sep_ldisj1 x []"
"sep_ldisj1 x (y#ys) ⟷ x##y ∧ sep_ldisj1 x ys"
by (auto simp: sep_ldisj1_def)
private lemma sep_ldisj1_append[ss]: "sep_ldisj1 x (ys⇩1@ys⇩2) ⟷ sep_ldisj1 x ys⇩1 ∧ sep_ldisj1 x ys⇩2"
by (induction ys⇩1) (auto simp: ss)
private definition "sep_ldisj xs ys ≡ ∀x∈List.set xs. sep_ldisj1 x ys"
private lemma sep_ldisj_simps[ss]:
"sep_ldisj [] ys"
"sep_ldisj xs []"
"sep_ldisj (x#xs) ys ⟷ sep_ldisj1 x ys ∧ sep_ldisj xs ys"
"sep_ldisj xs (y#ys) ⟷ sep_ldisj1 y xs ∧ sep_ldisj xs ys"
by (auto simp: sep_ldisj_def sep_ldisj1_def sep_algebra_simps)
private lemma sep_ldisj_append1[ss]: "sep_ldisj (xs⇩1@xs⇩2) ys ⟷ sep_ldisj xs⇩1 ys ∧ sep_ldisj xs⇩2 ys"
by (induction xs⇩1) (auto simp: ss)
private lemma sep_ldisj_append2[ss]: "sep_ldisj xs (ys⇩1@ys⇩2) ⟷ sep_ldisj xs ys⇩1 ∧ sep_ldisj xs ys⇩2"
by (induction ys⇩1) (auto simp: ss)
private lemma sep_ldisj_commute[sep_algebra_simps]: "sep_ldisj xs ys ⟷ sep_ldisj ys xs"
by (force simp: sep_ldisj_def sep_ldisj1_def sep_algebra_simps)
fun sep_distinct :: "_::stronger_sep_algebra list ⇒ bool" where
"sep_distinct [] ⟷ True"
| "sep_distinct (x#xs) ⟷ sep_ldisj1 x xs ∧ sep_distinct xs"
declare sep_distinct.simps[simp del, ss add]
private lemma sep_distinct_append_aux[ss]:
"sep_distinct (xs@ys) ⟷ sep_distinct xs ∧ sep_distinct ys ∧ sep_ldisj xs ys"
by (induction xs) (auto simp: ss)
private lemma norm_ldisj1[ss]: "sep_distinct ys ⟹ sep_ldisj1 x ys ⟷ x ## sepsum_list ys"
by (induction ys arbitrary: x) (auto simp: ss)
private lemma norm_ldisj[ss]: "sep_distinct xs ⟹ sep_distinct ys ⟹ sep_ldisj xs ys ⟷ sepsum_list xs ## sepsum_list ys"
by (induction xs) (auto simp: ss)
lemma sep_distinct_append[simp]:
"sep_distinct (xs@ys) ⟷ sep_distinct xs ∧ sep_distinct ys ∧ sepsum_list xs ## sepsum_list ys"
by (auto simp: ss)
lemma sepsum_append[simp]: "sep_distinct (xs@ys) ⟹ sepsum_list (xs@ys) = sepsum_list xs + sepsum_list ys"
by (induction xs) (auto simp: sep_algebra_simps ss)
lemma sep_distinct_simps[simp]:
"sep_distinct []"
"sep_distinct (x#xs) ⟷ x ## sepsum_list xs ∧ sep_distinct xs"
by (auto simp: ss)
end
subsection ‹Finite Assertion Families›
interpretation sep_folding: folding "λi Q. P i ** Q" □ for P
apply unfold_locales
apply (intro ext)
apply (simp add: sep.add_ac)
done
definition "sep_set_img S P ≡ ↑(finite S) ** sep_folding.F P S"
syntax
"_SEP_SET_IMG" :: "pttrn => 'a set => ('b ⇒ bool) => ('b ⇒ bool)" ("(3⋃*_∈_./ _)" [0, 0, 10] 10)
translations
"⋃*x∈A. B" ⇌ "CONST sep_set_img A (λx. B)"
print_translation ‹
[Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax sep_set_img} @{syntax_const "_SEP_SET_IMG"}]
›
lemma sep_set_img_infinite[simp]: "infinite I ⟹ sep_set_img I P = sep_false"
unfolding sep_set_img_def by auto
lemma sep_set_img_empty[simp]: "sep_set_img {} P = □"
and sep_set_img_insert_remove: "sep_set_img (insert x S) P = (P x ** sep_set_img (S-{x}) P)"
and sep_set_img_insert[simp]: "x∉S ⟹ sep_set_img (insert x S) P = (P x ** sep_set_img S P)"
and sep_set_img_remove: "x∈S ⟹ sep_set_img S P = (P x ** sep_set_img (S-{x}) P)"
by (auto
simp: sep_set_img_def sep_algebra_simps pred_lift_extract_simps sep_folding.insert_remove sep_folding.remove
del: ext intro!: ext)
lemma sep_set_img_cong:
assumes [simp]: "I=I'"
assumes P: "⋀x. finite I' ⟹ x∈I' ⟹ P x = P' x"
shows "sep_set_img I P = sep_set_img I' P'"
proof -
{
assume "finite I'"
then have "sep_set_img I' P = sep_set_img I' P'" using P
by induction auto
}
then show ?thesis by (cases "finite I'") auto
qed
lemma sep_set_img_cong_strong[cong]:
assumes [simp]: "I=I'"
assumes P: "⋀x. finite I' =simp=> x∈I' =simp=> P x = P' x"
shows "sep_set_img I P = sep_set_img I' P'"
using assms
unfolding simp_implies_def
by (rule sep_set_img_cong)
lemma sep_set_img_union[simp]:
assumes "S⇩1∩S⇩2={}"
shows "sep_set_img (S⇩1∪S⇩2) P = (sep_set_img S⇩1 P ** sep_set_img S⇩2 P)"
proof -
{
assume "finite S⇩1"
then have ?thesis using assms
by (induction S⇩1) auto
}
then show ?thesis by (cases "finite S⇩1") auto
qed
lemmas sep_set_img_ins[simp] = sep_set_img_union[where S⇩1="{i}", simplified] for i
lemma sep_set_img_map:
assumes "inj_on f I"
shows "(⋃*i∈f`I. A i) = (⋃*i∈I. A (f i))"
proof (cases "finite I")
case True
thus ?thesis using assms apply (induction I)
by (auto simp: sep_algebra_simps)
next
case False thus ?thesis
using assms
apply simp
using finite_image_iff sep_set_img_infinite by blast
qed
lemma sep_set_img_unionI':
assumes NDUP: "⋀x. ⟦x∈S⇩2 ⟧ ⟹ (P x ** P x) = sep_false"
assumes P: "(sep_set_img S⇩1 P ** sep_set_img S⇩2 P) s"
shows "sep_set_img (S⇩1∪S⇩2) P s"
proof -
have A: "(P x ** P x ** F) = sep_false" if "x∈S⇩2" for x F
using assms
by (simp add: sep.mult_commute sep_conj_left_commute that)
{
assume "finite S⇩1"
then have "?thesis" using P
proof (induction S⇩1 arbitrary: s)
case empty
then show ?case by simp
next
case (insert x S⇩1)
then show ?case
apply (cases "x∉S⇩2")
apply (auto simp: sep_set_img_remove sep_set_img_insert_remove sep_algebra_simps sep_conj_impl)
by (simp add: A sep_conj_left_commute)
qed
}
then show ?thesis using P by (cases "finite S⇩1") auto
qed
lemma sep_set_img_pull_EXS: "(⋃*x∈I. EXS y. f x y) = (EXS Y. ⋃*x∈I. f x (Y x))"
proof -
{
assume "finite I"
then have ?thesis
apply (induction I)
apply simp
apply (rule ext)
apply (clarsimp simp: sep_algebra_simps; safe)
subgoal for x F s xa xb
apply (rule exI[where x="xb(x:=xa)"])
apply auto
by (smt sep_set_img_cong)
subgoal by auto
done
}
then show ?thesis by (cases "finite I") auto
qed
lemma list_conj_eq_sep_set_img: "distinct xs ⟹ (⋀*map P xs) = sep_set_img (List.set xs) P"
by (induction xs) auto
lemma sep_is_pure_assn_imgI:
assumes "⋀i. i∈I ⟹ sep_is_pure_assn (f i)"
shows "sep_is_pure_assn (⋃*i∈I. f i)"
proof (cases "finite I")
assume "finite I"
then show ?thesis using assms
by (induction I) (auto simp: sep_is_pure_assn_conjI)
qed simp
end