Theory Separata
theory Separata
imports Main Separation_Algebra.Separation_Algebra "HOL-Eisbach.Eisbach_Tools"
"HOL-Library.Multiset"
begin
text ‹The tactics in this file are a simple proof search procedure based on
the labelled sequent calculus LS\_PASL for Propositional Abstract Separation Logic
in Zhe's PhD thesis.›
text ‹We define a class which is an extension to cancellative\_sep\_algebra
with other useful properties in separation algebra, including:
indivisible unit, disjointness, and cross-split.
We also add a property about the (reverse) distributivity of the disjointness.›
class heap_sep_algebra = cancellative_sep_algebra +
assumes sep_add_ind_unit: "⟦x + y = 0; x ## y⟧ ⟹ x = 0"
assumes sep_add_disj: "x##x ⟹x= 0 "
assumes sep_add_cross_split:
"⟦a + b = w; c + d = w; a ## b; c ## d⟧ ⟹
∃ e f g h. e + f = a ∧ g + h = b ∧ e + g = c ∧ f + h = d ∧
e ## f ∧ g ## h ∧ e ## g ∧ f ## h"
assumes disj_dstri: "⟦x ## y; y ## z; x ## z⟧ ⟹ x ## (y + z)"
begin
section ‹Lemmas about the labelled sequent calculus.›
text ‹An abbreviation of the + and \#\# operators in Separation\_Algebra.thy.
This notion is closer to the ternary relational atoms used in the literature.
This will be the main data structure which our labelled sequent calculus works on.›
definition tern_rel:: "'a ⇒ 'a ⇒ 'a ⇒ bool" ("(_,_▹_)" 25) where
"tern_rel a b c ≡ a ## b ∧ a + b = c"
lemma exist_comb: "x ## y ⟹ ∃z. (x,y▹z)"
by (simp add: tern_rel_def)
lemma disj_comb:
assumes a1: "(x,y▹z)"
assumes a2: "x ## w"
assumes a3: "y ## w"
shows "z ## w"
proof -
from a1 have f1: "x ## y ∧ x + y = z"
by (simp add: tern_rel_def)
then show ?thesis using a2 a3
using local.disj_dstri local.sep_disj_commuteI by blast
qed
text ‹The following lemmas corresponds to inference rules in LS\_PASL.
Thus these lemmas prove the soundness of LS\_PASL.
We also show the invertibility of those rules.›
lemma (in -) lspasl_id:
"Gamma ∧ (A h) ⟹ (A h) ∨ Delta"
by simp
lemma (in -) lspasl_botl:
"Gamma ∧ (sep_false h) ⟹ Delta"
by simp
lemma (in -) lspasl_topr:
"gamma ⟹ (sep_true h) ∨ Delta"
by simp
lemma lspasl_empl:
"Gamma ∧ (h = 0) ⟶ Delta ⟹
Gamma ∧ (sep_empty h) ⟶ Delta"
by (simp add: local.sep_empty_def)
lemma lspasl_empl_inv:
"Gamma ∧ (sep_empty h) ⟶ Delta ⟹
Gamma ∧ (h = 0) ⟶ Delta"
by simp
text ‹The following two lemmas are the same as applying
simp add: sep\_empty\_def.›
lemma lspasl_empl_der: "sep_empty h ⟹ h = 0"
by (simp add: local.sep_empty_def)
lemma lspasl_empl_eq: "(sep_empty h) = (h = 0)"
by (simp add: local.sep_empty_def)
lemma lspasl_empr:
"Gamma ⟶ (sep_empty 0) ∨ Delta"
by simp
end
lemma lspasl_notl:
"Gamma ⟶ (A h) ∨ Delta ⟹
Gamma ∧ ((not A) h) ⟶ Delta"
by auto
lemma lspasl_notl_inv:
"Gamma ∧ ((not A) h) ⟶ Delta ⟹
Gamma ⟶ (A h) ∨ Delta"
by auto
lemma lspasl_notr:
"Gamma ∧ (A h) ⟶ Delta ⟹
Gamma ⟶ ((not A) h) ∨ Delta"
by simp
lemma lspasl_notr_inv:
"Gamma ⟶ ((not A) h) ∨ Delta ⟹
Gamma ∧ (A h) ⟶ Delta"
by simp
lemma lspasl_andl:
"Gamma ∧ (A h) ∧ (B h) ⟶ Delta ⟹
Gamma ∧ ((A and B) h) ⟶ Delta"
by simp
lemma lspasl_andl_inv:
"Gamma ∧ ((A and B) h) ⟶ Delta ⟹
Gamma ∧ (A h) ∧ (B h) ⟶ Delta"
by simp
lemma lspasl_andr:
"⟦Gamma ⟶ (A h) ∨ Delta; Gamma ⟶ (B h) ∨ Delta⟧ ⟹
Gamma ⟶ ((A and B) h) ∨ Delta"
by auto
lemma lspasl_andr_inv:
"Gamma ⟶ ((A and B) h) ∨ Delta ⟹
(Gamma ⟶ (A h) ∨ Delta) ∧ (Gamma ⟶ (B h) ∨ Delta)"
by auto
lemma lspasl_orl:
"⟦Gamma ∧ (A h) ⟶ Delta; Gamma ∧ (B h) ⟶ Delta⟧ ⟹
Gamma ∧ (A or B) h ⟶ Delta"
by auto
lemma lspasl_orl_inv:
"Gamma ∧ (A or B) h ⟶ Delta ⟹
(Gamma ∧ (A h) ⟶ Delta) ∧ (Gamma ∧ (B h) ⟶ Delta)"
by simp
lemma lspasl_orr:
"Gamma ⟶ (A h) ∨ (B h) ∨ Delta ⟹
Gamma ⟶ ((A or B) h) ∨ Delta"
by simp
lemma lspasl_orr_inv:
"Gamma ⟶ ((A or B) h) ∨ Delta ⟹
Gamma ⟶ (A h) ∨ (B h) ∨ Delta"
by simp
lemma lspasl_impl:
"⟦Gamma ⟶ (A h) ∨ Delta; Gamma ∧ (B h) ⟶ Delta⟧ ⟹
Gamma ∧ ((A imp B) h) ⟶ Delta"
by auto
lemma lspasl_impl_inv:
"Gamma ∧ ((A imp B) h) ⟶ Delta ⟹
(Gamma ⟶ (A h) ∨ Delta) ∧ (Gamma ∧ (B h) ⟶ Delta)"
by auto
lemma lspasl_impr:
"Gamma ∧ (A h) ⟶ (B h) ∨ Delta ⟹
Gamma ⟶ ((A imp B) h) ∨ Delta"
by simp
lemma lspasl_impr_inv:
"Gamma ⟶ ((A imp B) h) ∨ Delta ⟹
Gamma ∧ (A h) ⟶ (B h) ∨ Delta"
by simp
context heap_sep_algebra
begin
text ‹We don't provide lemmas for derivations for the classical connectives,
as Isabelle proof methods can easily deal with them.›
lemma lspasl_starl:
"(∃h1 h2. (Gamma ∧ (h1,h2▹h0) ∧ (A h1) ∧ (B h2))) ⟶ Delta ⟹
Gamma ∧ ((A ** B) h0) ⟶ Delta"
using local.sep_conj_def by (auto simp add: tern_rel_def)
lemma lspasl_starl_inv:
"Gamma ∧ ((A ** B) h0) ⟶ Delta ⟹
(∃h1 h2. (Gamma ∧ (h1,h2▹h0) ∧ (A h1) ∧ (B h2))) ⟶ Delta"
using local.sep_conjI by (auto simp add: tern_rel_def)
lemma lspasl_starl_der:
"((A ** B) h0) ⟹ (∃h1 h2. (h1,h2▹h0) ∧ (A h1) ∧ (B h2))"
by (metis lspasl_starl)
lemma lspasl_starl_eq:
"((A ** B) h0) = (∃h1 h2. (h1,h2▹h0) ∧ (A h1) ∧ (B h2))"
by (metis lspasl_starl lspasl_starl_inv)
lemma lspasl_starr:
"⟦Gamma ∧ (h1,h2▹h0) ⟶ (A h1) ∨ ((A ** B) h0) ∨ Delta;
Gamma ∧ (h1,h2▹h0) ⟶ (B h2) ∨ ((A ** B) h0) ∨ Delta⟧ ⟹
Gamma ∧ (h1,h2▹h0) ⟶ ((A ** B) h0) ∨ Delta"
using local.sep_conjI by (auto simp add: tern_rel_def)
lemma lspasl_starr_inv:
"Gamma ∧ (h1,h2▹h0) ⟶ ((A ** B) h0) ∨ Delta ⟹
(Gamma ∧ (h1,h2▹h0) ⟶ (A h1) ∨ ((A ** B) h0) ∨ Delta) ∧
(Gamma ∧ (h1,h2▹h0) ⟶ (B h2) ∨ ((A ** B) h0) ∨ Delta)"
by simp
text ‹For efficiency we only apply *R on a pair of a ternary relational atom
and a formula ONCE. To achieve this, we create a special predicate to indicate that
a pair of a ternary relational atom and a formula has already been used in
a *R application.
Note that the predicate is true even if the *R rule hasn't been applied.
We will not infer the truth of this predicate in proof search, but only
check its syntactical appearance, which is only generated by the lemma lspasl\_starr\_der.
We need to ensure that this predicate is not generated elsewhere
in the proof search.›
definition starr_applied:: "'a ⇒ 'a ⇒ 'a ⇒ ('a ⇒ bool) ⇒ bool" where
"starr_applied h1 h2 h0 F ≡ (h1,h2▹h0) ∧ ¬(F h0)"
lemma lspasl_starr_der:
"(h1,h2▹h0) ⟹ ¬ ((A ** B) h0) ⟹
((h1,h2▹h0) ∧ ¬ ((A h1) ∨ ((A ** B) h0)) ∧ (starr_applied h1 h2 h0 (A ** B))) ∨
((h1,h2▹h0) ∧ ¬ ((B h2) ∨ ((A ** B) h0)) ∧ (starr_applied h1 h2 h0 (A ** B)))"
by (simp add: lspasl_starl_eq starr_applied_def)
lemma lspasl_starr_eq:
"((h1,h2▹h0) ∧ ¬ ((A ** B) h0)) =
(((h1,h2▹h0) ∧ ¬ ((A h1) ∨ ((A ** B) h0))) ∨ ((h1,h2▹h0) ∧ ¬ ((B h2) ∨ ((A ** B) h0))))"
using lspasl_starr_der by blast
lemma lspasl_magicl:
"⟦Gamma ∧ (h1,h2▹h0) ∧ ((A ⟶* B) h2) ⟶ (A h1) ∨ Delta;
Gamma ∧ (h1,h2▹h0) ∧ ((A ⟶* B) h2) ∧ (B h0) ⟶ Delta⟧ ⟹
Gamma ∧ (h1,h2▹h0) ∧ ((A ⟶* B) h2) ⟶ Delta"
using local.sep_add_commute local.sep_disj_commuteI local.sep_implD tern_rel_def
by fastforce
lemma lspasl_magicl_inv:
"Gamma ∧ (h1,h2▹h0) ∧ ((A ⟶* B) h2) ⟶ Delta ⟹
(Gamma ∧ (h1,h2▹h0) ∧ ((A ⟶* B) h2) ⟶ (A h1) ∨ Delta) ∧
(Gamma ∧ (h1,h2▹h0) ∧ ((A ⟶* B) h2) ∧ (B h0) ⟶ Delta)"
by simp
text ‹For efficiency we only apply -*L on a pair of a ternary relational atom
and a formula ONCE. To achieve this, we create a special predicate to indicate that
a pair of a ternary relational atom and a formula has already been used in
a *R application.
Note that the predicate is true even if the *R rule hasn't been applied.
We will not infer the truth of this predicate in proof search, but only
check its syntactical appearance, which is only generated by the lemma lspasl\_magicl\_der.
We need to ensure that in the proof search of Separata, this predicate is
not generated elsewhere.›
definition magicl_applied:: "'a ⇒ 'a ⇒ 'a ⇒ ('a ⇒ bool) ⇒ bool" where
"magicl_applied h1 h2 h0 F ≡ (h1,h2▹h0) ∧ (F h2)"
lemma lspasl_magicl_der:
"(h1,h2▹h0) ⟹ ((A ⟶* B) h2) ⟹
((h1,h2▹h0) ∧ ¬(A h1) ∧ ((A ⟶* B) h2) ∧ (magicl_applied h1 h2 h0 (A ⟶* B))) ∨
((h1,h2▹h0) ∧ (B h0) ∧ ((A ⟶* B) h2) ∧ (magicl_applied h1 h2 h0 (A ⟶* B)))"
by (metis lspasl_magicl magicl_applied_def)
lemma lspasl_magicl_eq:
"((h1,h2▹h0) ∧ ((A ⟶* B) h2)) =
(((h1,h2▹h0) ∧ ¬(A h1) ∧ ((A ⟶* B) h2)) ∨ ((h1,h2▹h0) ∧ (B h0) ∧ ((A ⟶* B) h2)))"
using lspasl_magicl_der by blast
lemma lspasl_magicr:
"(∃h1 h0. Gamma ∧ (h1,h2▹h0) ∧ (A h1) ∧ ((not B) h0)) ⟶ Delta ⟹
Gamma ⟶ ((A ⟶* B) h2) ∨ Delta"
using local.sep_add_commute local.sep_disj_commute local.sep_impl_def tern_rel_def
by auto
lemma lspasl_magicr_inv:
"Gamma ⟶ ((A ⟶* B) h2) ∨ Delta ⟹
(∃h1 h0. Gamma ∧ (h1,h2▹h0) ∧ (A h1) ∧ ((not B) h0)) ⟶ Delta"
by (metis lspasl_magicl)
lemma lspasl_magicr_der:
"¬ ((A ⟶* B) h2) ⟹
(∃h1 h0. (h1,h2▹h0) ∧ (A h1) ∧ ((not B) h0))"
by (metis lspasl_magicr)
lemma lspasl_magicr_eq:
"(¬ ((A ⟶* B) h2)) =
((∃h1 h0. (h1,h2▹h0) ∧ (A h1) ∧ ((not B) h0)))"
by (metis lspasl_magicl lspasl_magicr)
lemma lspasl_eq:
"Gamma ∧ (0,h2▹h2) ∧ h1 = h2 ⟶ Delta ⟹
Gamma ∧ (0,h1▹h2) ⟶ Delta"
by (simp add: tern_rel_def)
lemma lspasl_eq_inv:
"Gamma ∧ (0,h1▹h2) ⟶ Delta ⟹
Gamma ∧ (0,h2▹h2) ∧ h1 = h2 ⟶ Delta"
by simp
lemma lspasl_eq_der: "(0,h1▹h2) ⟹ ((0,h1▹h1) ∧ h1 = h2)"
using lspasl_eq by auto
lemma lspasl_eq_eq: "(0,h1▹h2) = ((0,h1▹h1) ∧ (h1 = h2))"
by (simp add: tern_rel_def)
lemma lspasl_u:
"Gamma ∧ (h,0▹h) ⟶ Delta ⟹
Gamma ⟶ Delta"
by (simp add: tern_rel_def)
lemma lspasl_u_inv:
"Gamma ⟶ Delta ⟹
Gamma ∧ (h,0▹h) ⟶ Delta"
by simp
lemma lspasl_u_der: "(h,0▹h)"
using lspasl_u by auto
lemma lspasl_e:
"Gamma ∧ (h1,h2▹h0) ∧ (h2,h1▹h0) ⟶ Delta ⟹
Gamma ∧ (h1,h2▹h0) ⟶ Delta"
by (simp add: local.sep_add_commute local.sep_disj_commute tern_rel_def)
lemma lspasl_e_inv:
"Gamma ∧ (h1,h2▹h0) ⟶ Delta ⟹
Gamma ∧ (h1,h2▹h0) ∧ (h2,h1▹h0) ⟶ Delta"
by simp
lemma lspasl_e_der: "(h1,h2▹h0) ⟹ (h1,h2▹h0) ∧ (h2,h1▹h0)"
using lspasl_e by blast
lemma lspasl_e_eq: "(h1,h2▹h0) = ((h1,h2▹h0) ∧ (h2,h1▹h0))"
using lspasl_e by blast
lemma lspasl_a_der:
assumes a1: "(h1,h2▹h0)"
and a2: "(h3,h4▹h1)"
shows "(∃h5. (h3,h5▹h0) ∧ (h2,h4▹h5) ∧ (h1,h2▹h0) ∧ (h3,h4▹h1))"
proof -
have f1: "h1 ## h2"
using a1 by (simp add: tern_rel_def)
have f2: "h3 ## h4"
using a2 by (simp add: tern_rel_def)
have f3: "h3 + h4 = h1"
using a2 by (simp add: tern_rel_def)
then have "h3 ## h2"
using f2 f1 by (metis local.sep_disj_addD1 local.sep_disj_commute)
then have f4: "h2 ## h3"
by (metis local.sep_disj_commute)
then have f5: "h2 + h4 ## h3"
using f3 f2 f1 by (metis (no_types) local.sep_add_commute local.sep_add_disjI1)
have "h4 ## h2"
using f3 f2 f1 by (metis local.sep_add_commute local.sep_disj_addD1 local.sep_disj_commute)
then show ?thesis
using f5 f4 by (metis (no_types) assms tern_rel_def local.sep_add_assoc local.sep_add_commute local.sep_disj_commute)
qed
lemma lspasl_a:
"(∃h5. Gamma ∧ (h3,h5▹h0) ∧ (h2,h4▹h5) ∧ (h1,h2▹h0) ∧ (h3,h4▹h1)) ⟶ Delta ⟹
Gamma ∧ (h1,h2▹h0) ∧ (h3,h4▹h1) ⟶ Delta"
using lspasl_a_der by blast
lemma lspasl_a_inv:
"Gamma ∧ (h1,h2▹h0) ∧ (h3,h4▹h1) ⟶ Delta ⟹
(∃h5. Gamma ∧ (h3,h5▹h0) ∧ (h2,h4▹h5) ∧ (h1,h2▹h0) ∧ (h3,h4▹h1)) ⟶ Delta"
by auto
lemma lspasl_a_eq:
"((h1,h2▹h0) ∧ (h3,h4▹h1)) =
(∃h5. (h3,h5▹h0) ∧ (h2,h4▹h5) ∧ (h1,h2▹h0) ∧ (h3,h4▹h1))"
using lspasl_a_der by blast
lemma lspasl_p:
"Gamma ∧ (h1,h2▹h0) ∧ h0 = h3 ⟶ Delta ⟹
Gamma ∧ (h1,h2▹h0) ∧ (h1,h2▹h3) ⟶ Delta"
by (auto simp add: tern_rel_def)
lemma lspasl_p_inv:
"Gamma ∧ (h1,h2▹h0) ∧ (h1,h2▹h3) ⟶ Delta ⟹
Gamma ∧ (h1,h2▹h0) ∧ h0 = h3 ⟶ Delta"
by auto
lemma lspasl_p_der:
"(h1,h2▹h0) ⟹ (h1,h2▹h3) ⟹ (h1,h2▹h0) ∧ h0 = h3"
by (simp add: tern_rel_def)
lemma lspasl_p_eq:
"((h1,h2▹h0) ∧ (h1,h2▹h3)) = ((h1,h2▹h0) ∧ h0 = h3)"
using lspasl_p_der by auto
lemma lspasl_c:
"Gamma ∧ (h1,h2▹h0) ∧ h2 = h3 ⟶ Delta ⟹
Gamma ∧ (h1,h2▹h0) ∧ (h1,h3▹h0) ⟶ Delta"
by (metis local.sep_add_cancelD local.sep_add_commute tern_rel_def
local.sep_disj_commuteI)
lemma lspasl_c_inv:
"Gamma ∧ (h1,h2▹h0) ∧ (h1,h3▹h0) ⟶ Delta ⟹
Gamma ∧ (h1,h2▹h0) ∧ h2 = h3 ⟶ Delta"
by auto
lemma lspasl_c_der:
"(h1,h2▹h0) ⟹ (h1,h3▹h0) ⟹ (h1,h2▹h0) ∧ h2 = h3"
using lspasl_c by blast
lemma lspasl_c_eq:
"((h1,h2▹h0) ∧ (h1,h3▹h0)) = ((h1,h2▹h0) ∧ h2 = h3)"
using lspasl_c_der by auto
lemma lspasl_iu:
"Gamma ∧ (0,h2▹0) ∧ h1 = 0 ⟶ Delta ⟹
Gamma ∧ (h1,h2▹0) ⟶ Delta"
using local.sep_add_ind_unit tern_rel_def by blast
lemma lspasl_iu_inv:
"Gamma ∧ (h1,h2▹0) ⟶ Delta ⟹
Gamma ∧ (0,h2▹0) ∧ h1 = 0 ⟶ Delta"
by simp
lemma lspasl_iu_der:
"(h1,h2▹0) ⟹ ((0,0▹0) ∧ h1 = 0 ∧ h2 = 0)"
using lspasl_eq_der lspasl_iu by (auto simp add: tern_rel_def)
lemma lspasl_iu_eq:
"(h1,h2▹0) = ((0,0▹0) ∧ h1 = 0 ∧ h2 = 0)"
using lspasl_iu_der by blast
lemma lspasl_d:
"Gamma ∧ (0,0▹h2) ∧ h1 = 0 ⟶ Delta ⟹
Gamma ∧ (h1,h1▹h2) ⟶ Delta"
using local.sep_add_disj tern_rel_def by fastforce
lemma lspasl_d_inv:
"Gamma ∧ (h1,h1▹h2) ⟶ Delta ⟹
Gamma ∧ (0,0▹h2) ∧ h1 = 0 ⟶ Delta"
by blast
lemma lspasl_d_der:
"(h1,h1▹h2) ⟹ (0,0▹0) ∧ h1 = 0 ∧ h2 = 0"
using lspasl_d lspasl_eq_der by blast
lemma lspasl_d_eq:
"(h1,h1▹h2) = ((0,0▹0) ∧ h1 = 0 ∧ h2 = 0)"
using lspasl_d_der by blast
lemma lspasl_cs_der:
assumes a1: "(h1,h2▹h0)"
and a2: "(h3,h4▹h0)"
shows "(∃h5 h6 h7 h8. (h5,h6▹h1) ∧ (h7,h8▹h2) ∧(h5,h7▹h3) ∧ (h6,h8▹h4)
∧ (h1,h2▹h0) ∧ (h3,h4▹h0))"
proof -
from a1 a2 have "h1 + h2 = h0 ∧ h3 + h4 = h0 ∧ h1 ## h2 ∧ h3 ## h4"
by (simp add: tern_rel_def)
then have "∃h5 h6 h7 h8. h5 + h6 = h1 ∧ h7 + h8 = h2 ∧
h5 + h7 = h3 ∧ h6 + h8 = h4 ∧ h5 ## h6 ∧ h7 ## h8 ∧
h5 ## h7 ∧ h6 ## h8"
using local.sep_add_cross_split by auto
then have "∃h5 h6 h7 h8. (h5,h6▹h1) ∧ h7 + h8 = h2 ∧
h5 + h7 = h3 ∧ h6 + h8 = h4 ∧ h7 ## h8 ∧
h5 ## h7 ∧ h6 ## h8"
by (auto simp add: tern_rel_def)
then have "∃h5 h6 h7 h8. (h5,h6▹h1) ∧ (h7,h8▹h2) ∧
h5 + h7 = h3 ∧ h6 + h8 = h4 ∧ h5 ## h7 ∧ h6 ## h8"
by (auto simp add: tern_rel_def)
then have "∃h5 h6 h7 h8. (h5,h6▹h1) ∧ (h7,h8▹h2) ∧
(h5,h7▹h3) ∧ h6 + h8 = h4 ∧ h6 ## h8"
by (auto simp add: tern_rel_def)
then show ?thesis using a1 a2 tern_rel_def by blast
qed
lemma lspasl_cs:
"(∃h5 h6 h7 h8. Gamma ∧ (h5,h6▹h1) ∧ (h7,h8▹h2) ∧(h5,h7▹h3) ∧ (h6,h8▹h4) ∧ (h1,h2▹h0) ∧ (h3,h4▹h0)) ⟶ Delta ⟹
Gamma ∧ (h1,h2▹h0) ∧ (h3,h4▹h0) ⟶ Delta"
using lspasl_cs_der by auto
lemma lspasl_cs_inv:
"Gamma ∧ (h1,h2▹h0) ∧ (h3,h4▹h0) ⟶ Delta ⟹
(∃h5 h6 h7 h8. Gamma ∧ (h5,h6▹h1) ∧ (h7,h8▹h2) ∧(h5,h7▹h3) ∧ (h6,h8▹h4) ∧ (h1,h2▹h0) ∧ (h3,h4▹h0)) ⟶ Delta"
by auto
lemma lspasl_cs_eq:
"((h1,h2▹h0) ∧ (h3,h4▹h0)) =
(∃h5 h6 h7 h8. (h5,h6▹h1) ∧ (h7,h8▹h2) ∧(h5,h7▹h3) ∧ (h6,h8▹h4) ∧
(h1,h2▹h0) ∧ (h3,h4▹h0))"
using lspasl_cs_der by auto
end
text ‹The above proves the soundness and invertibility of LS\_PASL.›
section ‹Lemmas David proved for separation algebra.›
lemma sep_substate_tran:
"x ≼ y ∧ y ≼ z ⟹ x ≼ z"
unfolding sep_substate_def
proof -
assume "(∃z. x ## z ∧ x + z = y) ∧ (∃za. y ## za ∧ y + za = z)"
then obtain x' y' where fixed:"(x ## x' ∧ x + x' = y) ∧ (y ## y' ∧ y + y' = z)"
by auto
then have disj_x:"x ## y' ∧ x' ## y'"
using sep_disj_addD sep_disj_commute by blast
then have p1:"x ## (x' + y')" using fixed sep_disj_commute sep_disj_addI3
by blast
then have "x + (x' + y') = z" using disj_x by (metis (no_types) fixed sep_add_assoc)
thus "∃za. x ## za ∧ x + za = z" using p1 by auto
qed
lemma precise_sep_conj:
assumes a1:"precise I" and
a2:"precise I'"
shows "precise (I ∧* I')"
proof (clarsimp simp: precise_def)
fix hp hp' h
assume hp:"hp ≼ h" and hp': "hp' ≼ h" and ihp: "(I ∧* I') hp" and ihp': "(I ∧* I') hp'"
obtain hp1 hp2 where ihpex: "hp1 ## hp2 ∧ hp = hp1 + hp2 ∧ I hp1 ∧ I' hp2" using ihp sep_conjD by blast
obtain hp1' hp2' where ihpex': "hp1' ## hp2' ∧ hp' = hp1' + hp2' ∧ I hp1' ∧ I' hp2'" using ihp' sep_conjD by blast
have f3: "hp2' ## hp1'"
by (simp add: ihpex' sep_disj_commute)
have f4: "hp2 ## hp1"
using ihpex sep_disj_commute by blast
have f5:"⋀a. ¬ a ≼ hp ∨ a ≼ h"
using hp sep_substate_tran by blast
have f6:"⋀a. ¬ a ≼ hp' ∨ a ≼ h"
using hp' sep_substate_tran by blast
thus "hp = hp'"
using f4 f3 f5 a2 a1 a1 a2 ihpex ihpex'
unfolding precise_def by (metis sep_add_commute sep_substate_disj_add')
qed
lemma unique_subheap:
"(σ1,σ2▹σ) ⟹ ∃!σ2'.(σ1,σ2'▹σ)"
using lspasl_c_der by blast
lemma sep_split_substate:
"(σ1, σ2▹ σ) ⟹
(σ1 ≼ σ) ∧ (σ2 ≼ σ)"
proof-
assume a1:"(σ1, σ2▹ σ)"
thus "(σ1 ≼ σ) ∧ (σ2 ≼ σ)"
by (auto simp add: sep_disj_commute
tern_rel_def
sep_substate_disj_add
sep_substate_disj_add')
qed
abbreviation sep_septraction :: "(('a::sep_algebra) ⇒ bool) ⇒ ('a ⇒ bool) ⇒ ('a ⇒ bool)" (infixr "⟶⊕" 25)
where
"P ⟶⊕ Q ≡ not (P ⟶* not Q)"
section ‹Below we integrate the inference rules in proof search.›
method try_lspasl_empl = (
match premises in P[thin]:"sep_empty ?h" ⇒
‹insert lspasl_empl_der[OF P]›,
simp?
)
method try_lspasl_starl = (
match premises in P[thin]:"(?A ** ?B) ?h" ⇒
‹insert lspasl_starl_der[OF P], auto›,
simp?
)
method try_lspasl_magicr = (
match premises in P[thin]:"¬(?A ⟶* ?B) ?h" ⇒
‹insert lspasl_magicr_der[OF P], auto›,
simp?
)
text ‹Only apply the rule Eq on (0,h1,h2) where h1 and h2
are not syntactically the same.›
method try_lspasl_eq = (
match premises in P[thin]:"(0,?h1▹?h2)" ⇒
‹match P in
"(0,h▹h)" for h ⇒ ‹fail›
¦_ ⇒ ‹insert lspasl_eq_der[OF P], auto››,
simp?
)
text ‹We restrict that the rule IU can't be applied
on (0,0,0).›
method try_lspasl_iu = (
match premises in P[thin]:"(?h1,?h2▹0)" ⇒
‹match P in
"(0,0▹0)" ⇒ ‹fail›
¦_ ⇒ ‹insert lspasl_iu_der[OF P], auto››,
simp?
)
text ‹We restrict that the rule D can't be applied
on (0,0,0).›
method try_lspasl_d = (
match premises in P[thin]:"(h1,h1▹h2)" for h1 h2 ⇒
‹match P in
"(0,0▹0)" ⇒ ‹fail›
¦_ ⇒ ‹insert lspasl_d_der[OF P], auto››,
simp?
)
text ‹We restrict that the rule P can't be applied to
two syntactically identical ternary relational atoms.›
method try_lspasl_p = (
match premises in P[thin]:"(h1,h2▹h0)" for h0 h1 h2 ⇒
‹match premises in "(h1,h2▹h0)" ⇒ ‹fail›
¦P'[thin]:"(h1,h2▹?h3)" ⇒ ‹insert lspasl_p_der[OF P P'], auto››,
simp?
)
text ‹We restrict that the rule C can't be applied to
two syntactically identical ternary relational atoms.›
method try_lspasl_c = (
match premises in P[thin]:"(h1,h2▹h0)" for h0 h1 h2 ⇒
‹match premises in "(h1,h2▹h0)" ⇒ ‹fail›
¦P'[thin]:"(h1,?h3▹h0)" ⇒ ‹insert lspasl_c_der[OF P P'], auto››,
simp?
)
text ‹We restrict that *R only applies to a pair of
a ternary relational and a formula once.
Here, we need to first try simp to unify heaps.
In the end, we try simp\_all to simplify all branches.
A similar strategy is used in -*L.›
method try_lspasl_starr = (
simp?,
match premises in P:"(h1,h2▹h)" and P':"¬(A ** B) (h::'a::heap_sep_algebra)" for h1 h2 h A B ⇒
‹match premises in "starr_applied h1 h2 h (A ** B)" ⇒ ‹fail›
¦_ ⇒ ‹insert lspasl_starr_der[OF P P'], auto››,
simp_all?
)
text ‹We restrict that -*L only applies to a pair of
a ternary relational and a formula once.›
method try_lspasl_magicl = (
simp?,
match premises in P: "(h1,h▹h2)" and P':"(A ⟶* B) (h::'a::heap_sep_algebra)" for h1 h2 h A B ⇒
‹match premises in "magicl_applied h1 h h2 (A ⟶* B)" ⇒ ‹fail›
¦_ ⇒ ‹insert lspasl_magicl_der[OF P P'], auto››,
simp_all?
)
text ‹We restrict that the U rule is only applicable to a world h
when (h,0,h) is not in the premises. There are two cases:
(1) We pick a ternary relational atom (h1,h2,h0),
and check if (h1,0,h1) occurs in the premises, if not,
apply U on h1. Otherwise, check other ternary relational atoms.
(2) We pick a labelled formula (A h),
and check if (h,0,h) occurs in the premises, if not,
apply U on h. Otherwise, check other labelled formulae.›
method try_lspasl_u_tern = (
match premises in
P:"(h1,h2▹(h0::'a::heap_sep_algebra))" for h1 h2 h0 ⇒
‹match premises in
"(h1,0▹h1)" ⇒ ‹match premises in
"(h2,0▹h2)" ⇒ ‹match premises in
I1:"(h0,0▹h0)" ⇒ ‹fail›
¦_ ⇒ ‹insert lspasl_u_der[of h0]››
¦_ ⇒ ‹insert lspasl_u_der[of h2]››
¦_ ⇒ ‹insert lspasl_u_der[of h1]››,
simp?
)
method try_lspasl_u_form = (
match premises in
P':"_ (h::'a::heap_sep_algebra)" for h ⇒
‹match premises in "(h,0▹h)" ⇒ ‹fail›
¦"(0,0▹0)" and "h = 0" ⇒ ‹fail›
¦"(0,0▹0)" and "0 = h" ⇒ ‹fail›
¦_ ⇒ ‹insert lspasl_u_der[of h]››,
simp?
)
text ‹We restrict that the E rule is only applicable to
(h1,h2,h0) when (h2,h1,h0) is not in the premises.›
method try_lspasl_e = (
match premises in P:"(h1,h2▹h0)" for h1 h2 h0 ⇒
‹match premises in "(h2,h1▹h0)" ⇒ ‹fail›
¦_ ⇒ ‹insert lspasl_e_der[OF P], auto››,
simp?
)
text ‹We restrict that the A rule is only applicable to
(h1,h2,h0) and (h3,h4,h1) when (h3,h,h0) and (h2,h4,h)
or any commutative variants of the two
do not occur in the premises, for some h.
Additionally, we do not allow A to be applied to two identical
ternary relational atoms.
We further restrict that the leaves must not be 0,
because otherwise this application does not gain anything.›
method try_lspasl_a = (
match premises in "(h1,h2▹h0)" for h0 h1 h2 ⇒
‹match premises in
"(0,h2▹h0)" ⇒ ‹fail›
¦"(h1,0▹h0)" ⇒ ‹fail›
¦"(h1,h2▹0)" ⇒ ‹fail›
¦P[thin]:"(h1,h2▹h0)" ⇒
‹match premises in
P':"(h3,h4▹h1)" for h3 h4 ⇒ ‹match premises in
"(0,h4▹h1)" ⇒ ‹fail›
¦"(h3,0▹h1)" ⇒ ‹fail›
¦"(_,h3▹h0)" ⇒ ‹fail›
¦"(h3,_▹h0)" ⇒ ‹fail›
¦"(h2,h4▹_)" ⇒ ‹fail›
¦"(h4,h2▹_)" ⇒ ‹fail›
¦_ ⇒ ‹insert P P', drule lspasl_a_der, auto››››,
simp?
)
text ‹I don't have a good heuristics for CS right now.
I simply forbid CS to be applied on the same pair twice.›
method try_lspasl_cs = (
match premises in P[thin]:"(h1,h2▹h0)" for h0 h1 h2 ⇒
‹match premises in "(h1,h2▹h0)" ⇒ ‹fail›
¦"(h2,h1▹h0)" ⇒ ‹fail›
¦P':"(h3,h4▹h0)" for h3 h4 ⇒ ‹match premises in
"(h5,h6▹h1)" and "(h7,h8▹h2)" and "(h5,h7▹h3)" and "(h6,h8▹h4)" for h5 h6 h7 h8 ⇒ ‹fail›
¦"(i5,i6▹h2)" and "(i7,i8▹h1)" and "(i5,i7▹h3)" and "(i6,i8▹h4)" for i5 i6 i7 i8 ⇒ ‹fail›
¦"(j5,j6▹h1)" and "(j7,j8▹h2)" and "(j5,j7▹h4)" and "(j6,j8▹h3)" for j5 j6 j7 j8 ⇒ ‹fail›
¦"(k5,k6▹h2)" and "(k7,k8▹h1)" and "(k5,k7▹h4)" and "(k6,k8▹h3)" for k5 k6 k7 k8 ⇒ ‹fail›
¦_ ⇒ ‹insert lspasl_cs_der[OF P P'], auto›››,
simp
)
method try_lspasl_starr_guided = (
simp?,
match premises in P:"(h1,h2▹h)" and P':"¬(A ** B) (h::'a::heap_sep_algebra)" for h1 h2 h A B ⇒
‹match premises in "starr_applied h1 h2 h (A ** B)" ⇒ ‹fail›
¦"A h1" ⇒ ‹insert lspasl_starr_der[OF P P'], auto›
¦"B h2" ⇒ ‹insert lspasl_starr_der[OF P P'], auto››,
simp_all?
)
method try_lspasl_magicl_guided = (
simp?,
match premises in P: "(h1,h▹h2)" and P':"(A ⟶* B) (h::'a::heap_sep_algebra)" for h1 h2 h A B ⇒
‹match premises in "magicl_applied h1 h h2 (A ⟶* B)" ⇒ ‹fail›
¦"A h1" ⇒ ‹insert lspasl_magicl_der[OF P P'], auto›
¦"¬(B h2)" ⇒ ‹insert lspasl_magicl_der[OF P P'], auto››,
simp_all?
)
text ‹In case the conclusion is not False, we normalise the goal as below.›
method norm_goal = (
match conclusion in "False" ⇒ ‹fail›
¦_ ⇒ ‹rule ccontr›,
simp?
)
text ‹The tactic for separata. We first try to simplify the problem
with auto simp add: sep\_conj\_ac, which ought to solve many problems.
Then we apply the "true" invertible rules and structural rules
which unify worlds as much as possible, followed by auto to simplify the goals.
Then we apply *R and -*L and other structural rules.
The rule CS is only applied when nothing else is applicable. We try not
to use it.›
text ‹
*****
Note, (try\_lspasl\_u
|try\_lspasl\_e)
|try\_lspasl\_a)+
may cause infinite loops.
*****
›
method separata =
((auto simp add: sep_conj_ac)
|(norm_goal?,
((try_lspasl_empl
|try_lspasl_starl
|try_lspasl_magicr
|try_lspasl_iu
|try_lspasl_d
|try_lspasl_eq
|try_lspasl_p
|try_lspasl_c
|try_lspasl_starr_guided
|try_lspasl_magicl_guided)+,
auto?)
|(try_lspasl_u_tern
|try_lspasl_e
|try_lspasl_a)+
|(try_lspasl_starr
|try_lspasl_magicl)
)+
|try_lspasl_u_form+
|try_lspasl_cs
)+
section ‹Some examples.›
text ‹Let's prove something that abstract separation logic provers struggle to prove.
This can be proved easily in Isabelle, proof found by Sledgehammer.›
lemma fm_hard: "((sep_empty imp (p0 ⟶* (((p0 ** (p0 ⟶* p1)) ** (not p1)) ⟶*
(p0 ** (p0 ** ((p0 ⟶* p1) ** (not p1))))))) imp ((((sep_empty ** p0) **
(p0 ** ((p0 ⟶* p1) ** (not p1)))) imp (((p0 ** p0) ** (p0 ⟶* p1)) **
(not p1))) ** sep_empty)) h"
by separata
text ‹The following formula can only be proved in partial-deterministic
separation algebras.
Sledgehammer took a rather long time to find a proof.›
lemma fm_partial: "(((not (sep_true ⟶* (not sep_empty))) **
(not (sep_true ⟶* (not sep_empty)))) imp
(not (sep_true ⟶* (not sep_empty))))
(h::'a::heap_sep_algebra)"
by separata
text ‹The following is the axiom of indivisible unit.
Sledgehammer finds a proof easily.›
lemma ax_iu: "((sep_empty and (A ** B)) imp A)
(h::'a::heap_sep_algebra)"
by separata
text ‹Sledgehammer fails to find a proof in 300s for this one.›
lemma "(not (((A ** (C ⟶* (not ((not (A ⟶* B)) ** C)))) and (not B)) ** C))
(h::'a::heap_sep_algebra)"
by separata
text ‹Sledgehammer finds a proof easily.›
lemma "((sep_empty ⟶* (not ((not A) ** sep_empty))) imp A)
(h::'a::heap_sep_algebra)"
by separata
text ‹Sledgehammer finds a proof in 46 seconds.›
lemma "(A imp (not ((not (A ** B)) and (not (A ** (not B))))))
(h::'a::heap_sep_algebra)"
by separata
text ‹Sledgehammer easily finds a proof.›
lemma "((sep_empty and A) imp (A ** A))
(h::'a::heap_sep_algebra)"
by separata
text ‹Sledgehammer fails to find a proof in 300s.›
lemma "(not (((A ** (C ⟶* (not ((not (A ⟶* B)) ** C)))) and (not B)) ** C))
(h::'a::heap_sep_algebra)"
by separata
text ‹Sledgehammer finds a proof easily.›
lemma "((sep_empty ⟶* (not ((not A) ** sep_empty))) imp A)
(h::'a::heap_sep_algebra)"
by separata
text ‹Sledgehammer finds a proof easily.›
lemma "(sep_empty imp ((A ** B) ⟶* (B ** A)))
(h::'a::heap_sep_algebra)"
by separata
text ‹Sledgehammer takes a while to find a proof, although the proof is by smt and is fast.›
lemma "(sep_empty imp ((A ** (B and C)) ⟶* ((A ** B) and (A ** C))))
(h::'a::heap_sep_algebra)"
by separata
text ‹Sledgehammer takes a long time to find a smt proof, but the smt proves it quickly.›
lemma "(sep_empty imp ((A ⟶* (B imp C)) ⟶* ((A ⟶* B) imp (A ⟶* C))))
(h::'a::heap_sep_algebra)"
by separata
text ‹Sledgehammer finds a proof quickly.›
lemma "(sep_empty imp (((A imp B) ⟶* ((A ⟶* A) imp A)) imp (A ⟶* A)))
(h::'a::heap_sep_algebra)"
by separata
text ‹Sledgehammer finds proofs in a while.›
lemma "((A ⟶* B) and (sep_true ** (sep_empty and A)) imp B)
(h::'a::heap_sep_algebra)"
by separata
text ‹Sledgehammer finds proofs easily.›
lemma "((sep_empty ⟶* (not ((not A) ** sep_true))) imp A)
(h::'a::heap_sep_algebra)"
by separata
text ‹Sledgehammer takes a while to find a proof.›
lemma "(not ((A ⟶* (not (A ** B))) and (((not A) ⟶* (not B)) and B)))
(h::'a::heap_sep_algebra)"
by separata
text ‹Sledgehammer takes a long time to find a smt proof, although smt proves it quickly.›
lemma "(sep_empty imp ((A ⟶* (B ⟶* C)) ⟶* ((A ** B) ⟶* C)))
(h::'a::heap_sep_algebra)"
by separata
text ‹Sledgehammer finds proofs easily.›
lemma "(sep_empty imp ((A ** (B ** C)) ⟶* ((A ** B) ** C)))
(h::'a::heap_sep_algebra)"
by separata
text ‹Sledgehammer finds proofs in a few seconds.›
lemma "(sep_empty imp ((A ** ((B ⟶* D) ** C)) ⟶* ((A ** (B ⟶* D)) ** C)))
(h::'a::heap_sep_algebra)"
by separata
text ‹Sledgehammer fails to find a proof in 300s.›
lemma "(not (((A ⟶* (not ((not (D ⟶* (not (A ** (C ** B))))) ** A))) and C) ** (D and (A ** B))))
(h::'a::heap_sep_algebra)"
by separata
text ‹Sledgehammer takes a while to find a proof.›
lemma "(not ((C ** (D ** E)) and ((A ⟶* (not (not (B ⟶* not (D ** (E ** C))) ** A))) **
(B and (A ** sep_true)))))
(h::'a::heap_sep_algebra)"
by separata
text ‹Sledgehammer fails to find a proof in 300s.›
lemma "(not (((A ⟶* (not ((not (D ⟶* (not ((C ** E) ** (B ** A))))) ** A))) and C) ** (D and (A ** (B ** E)))))
(h::'a::heap_sep_algebra)"
by separata
text ‹Sledgehammer finds a proof easily.›
lemma "((A ** (B ** (C ** (D ** E)))) imp (E ** (B ** (A ** (C ** D)))))
(h::'a::heap_sep_algebra)"
by separata
lemma "((A ** (B ** (C ** (D ** (E ** (F ** G)))))) imp (G ** (E ** (B ** (A ** (C ** (D ** F)))))))
(h::'a::heap_sep_algebra)"
by separata
text ‹Sledgehammer finds a proof in a few seconds.›
lemma "(sep_empty imp ((A ** ((B ⟶* E) ** (C ** D))) ⟶* ((A ** D) ** (C ** (B ⟶* E)))))
(h::'a::heap_sep_algebra)"
by separata
text ‹This is the odd BBI formula that I personally can't
prove using any other methods. I only know of a derivation in
my labelled sequent calculus for BBI.
Sledgehammer takes a while to find a proof.›
lemma "(not (sep_empty and A and (B ** (not (C ⟶* (sep_empty imp A))))))
(h::'a::heap_sep_algebra)"
by separata
text ‹Sledgehammer finds a proof easily.›
lemma "((((sep_true imp p0) imp ((p0 ** p0) ⟶* ((sep_true imp p0) ** (p0 ** p0)))) imp
(p1 ⟶* (((sep_true imp p0) imp ((p0 ** p0) ⟶* (((sep_true imp p0) ** p0) ** p0))) ** p1))))
(h::'a::heap_sep_algebra)"
by separata
text ‹The following are some randomly generated BBI formulae.›
text ‹Sledgehammer finds a proof easily.›
lemma "((((p1 ⟶* p3) ⟶* (p5 ⟶* p2)) imp ((((p7 ** p4) and (p3 ⟶* p2)) imp
((p7 ** p4) and (p3 ⟶* p2))) ⟶* (((p1 ⟶* p3) ⟶* (p5 ⟶* p2)) **
(((p4 ** p7) and (p3 ⟶* p2)) imp ((p4 ** p7) and (p3 ⟶* p2)))))))
(h::'a::heap_sep_algebra)"
by separata
text ‹Sledgehammer finds a proof easily.›
lemma "(((((p1 ⟶* (p0 imp sep_false )) imp sep_false ) imp (((p1 imp sep_false ) imp
((p0 ** ((p1 imp sep_false ) ⟶* (p4 ⟶* p1))) ⟶* ((p1 imp sep_false ) **
(p0 ** ((p1 imp sep_false ) ⟶* (p4 ⟶* p1)))))) imp sep_false )) imp
(((p1 imp sep_false ) imp ((p0 ** ((p1 imp sep_false ) ⟶* (p4 ⟶* p1))) ⟶*
((p0 ** (p1 imp sep_false )) ** ((p1 imp sep_false ) ⟶* (p4 ⟶* p1))))) imp
(p1 ⟶* (p0 imp sep_false )))))
(h::'a::heap_sep_algebra)"
by separata
text ‹Sledgehammer finds a proof easily.›
lemma "(((p0 imp sep_false ) imp ((p1 ** p0) ⟶* (p1 ** ((p0 imp sep_false ) **
p0)))) imp ((p0 imp sep_false ) imp ((p1 ** p0) ⟶* ((p1 ** p0) ** (p0 imp
sep_false )))))
(h::'a::heap_sep_algebra)"
by separata
text ‹Sledgehammer finds a proof in a while.›
lemma "(sep_empty imp ((((p4 ** p1) ⟶* ((p8 ** sep_empty ) ⟶* p0)) imp
(p1 ⟶* (p1 ** ((p4 ** p1) ⟶* ((p8 ** sep_empty ) ⟶* p0))))) ⟶*
(((p4 ** p1) ⟶* ((p8 ** sep_empty ) ⟶* p0)) imp (p1 ⟶* (((p1 ** p4) ⟶*
((p8 ** sep_empty ) ⟶* p0)) ** p1)))))
(h::'a::heap_sep_algebra)"
by separata
text ‹Sledgehammer finds a proof easily.›
lemma "((((p3 imp (p0 ⟶* (p3 ** p0))) imp sep_false ) imp (p1 imp sep_false )) imp
(p1 imp (p3 imp (p0 ⟶* (p0 ** p3)))))
(h::'a::heap_sep_algebra)"
by separata
text ‹Sledgehammer finds a proof in a few seconds.›
lemma "((p7 ⟶* (p4 ** (p6 ⟶* p1))) imp ((p4 imp (p1 ⟶* ((sep_empty **
p1) ** p4))) ⟶* ((p1 imp (p4 ⟶* (p4 ** (sep_empty ** p1)))) ** (p7 ⟶*
((p6 ⟶* p1) ** p4)))))
(h::'a::heap_sep_algebra)"
by separata
text ‹Sledgehammer finds a proof easily.›
lemma "(((p2 imp p0) imp ((p0 ** sep_true ) ⟶* (p0 ** (sep_true **
(p2 imp p0))))) imp ((p2 imp p0) imp ((sep_true ** p0) ⟶*
(p0 ** ((p2 imp p0) ** sep_true )))))
(h::'a::heap_sep_algebra)"
by separata
text ‹Sledgehammer finds a proof easily.›
lemma "((sep_empty imp ((p1 ⟶* (((p2 imp sep_false ) ** p0) ** p8)) ⟶*
(p1 ⟶* ((p2 imp sep_false ) ** (p0 ** p8))))) imp ((p0 ** sep_empty ) ⟶*
((sep_empty imp ((p1 ⟶* ((p0 ** (p2 imp sep_false )) ** p8)) ⟶* (p1 ⟶*
((p2 imp sep_false ) ** (p0 ** p8))))) ** (p0 ** sep_empty ))))
(h::'a::heap_sep_algebra)"
by separata
text ‹Sledgehammer finds a proof in a while.›
lemma "((p0 ⟶* sep_empty ) imp ((sep_empty imp ((sep_empty ** ((((p8 ** p7) **
(p8 imp p4)) ⟶* p8) ** (p2 ** p1))) ⟶* (p2 ** (((p7 ** ((p8 imp p4) **
p8)) ⟶* p8) ** p1)))) ⟶* ((sep_empty imp (((((p7 ** (p8 ** (p8 imp p4))) ⟶*
p8) ** sep_empty ) ** (p1 ** p2)) ⟶* (((p7 ** ((p8 imp p4) ** p8)) ⟶* p8) **
(p1 ** p2)))) ** (p0 ⟶* sep_empty ))))
(h::'a::heap_sep_algebra)"
by separata
end