Quelle  Separata.thy

(*
 * Copyright 2016, NTU
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * Author: Zhe Hou, David Sanan.
 *)

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 (* This section contains invertible rules. Apply as often as possible. *)
          |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 (* This section contains structural rules. *)
        |try_lspasl_e
        |try_lspasl_a)+
      |(try_lspasl_starr (* This section contains *R and -*L. *)
        |try_lspasl_magicl)
        )+
    |try_lspasl_u_form+ (* This rule is rarely used. *)
    |try_lspasl_cs (* Cross-split adds too much complication. Try not to use it. *)
      )+

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