Theory Shallow_Separation_Logic.Assertion_Triple

(* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
   SPDX-License-Identifier: MIT *)

(*<*)
theory Assertion_Triple
  imports Shallow_Micro_Rust.Eval Assertion_Language Precision Locality "HOL-Library.Rewrite"
begin

context sepalg begin
(*>*)

subsubsection‹Assertion triples›

text‹The following relation expresses that two states \<^term>‹σ› and \<^term>‹σ'› are related by
'swapping out' a sub-state satisfying assertion \<^term>‹φ› for a sub-state satisfying \<^term>‹ψ›:›
definition atriple :: ‹'a assert ⇒ 'a ⇒ 'a ⇒ 'a assert ⇒ bool›
      ("(_) ⊩/ '(_,_')/ ⊣⇩w⇩e⇩a⇩k (_)" [50,50,50]50) where
  ‹φ ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ ≡ ∀π. ucincl π ⟶ σ ⊨ φ ⋆ π ⟶ σ' ⊨ ψ ⋆ π›

lemma atripleI:
  assumes ‹⋀π. ucincl π ⟹ σ ⊨ (φ ⋆ π) ⟹ σ' ⊨ (ψ ⋆ π)›
    shows ‹φ ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ›
using assms by (auto simp add: atriple_def)

lemma atripleE:
  assumes ‹φ ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ›
      and ‹(⋀π. ucincl π ⟹ σ ⊨ (φ ⋆ π) ⟹ σ' ⊨ (ψ ⋆ π)) ⟹ R›
    shows R
using assms by (auto simp add: atriple_def)

lemma atriple_refl:
  shows ‹φ ⊩ (σ, σ) ⊣⇩w⇩e⇩a⇩k φ›
by (simp add: atriple_def)

lemma atriple_refl':
  shows ‹φ ⊩ (σ, σ) ⊣⇩w⇩e⇩a⇩k ⊤ ⋆ φ›
by (simp add: atriple_def) (metis local.asepconj_assoc local.asepconj_ident local.asepconj_swap_top)

lemma atriple_pre_false:
  shows ‹{} ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ›
by (simp add: atriple_def local.asepconj_bot_zero)

lemma atriple_post_true:
  shows ‹φ  ⊩ (σ, σ) ⊣⇩w⇩e⇩a⇩k ⊤›
by (metis aentails_def atripleI local.aentails_cancel_l local.asepconj_ident)

lemma atriple_consequence:
  assumes ‹φ' ⤏ φ›
     and ‹ψ ⤏ ψ'›
     and ‹φ ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ›
   shows ‹φ' ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ'›
using assms by (auto elim!: atripleE intro!: atripleI) (meson aentailsE local.asepconj_mono2)

lemma atriple_trans:
  assumes ‹φ ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ›
      and ‹ψ ⊩ (σ', σ'') ⊣⇩w⇩e⇩a⇩k ξ›
    shows ‹φ ⊩ (σ, σ'') ⊣⇩w⇩e⇩a⇩k ξ›
using assms by (auto simp add: atriple_def)

lemma atriple_union:
  shows ‹((⋃Φ) ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ) = (∀φ∈Φ. (φ ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ))›
    and ‹((⨆x. φ x) ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ) = (∀x. (φ x ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ))›
    and ‹((⨆x∈S. φ x) ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ) = (∀x∈S. (φ x ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ))›
by (auto simp add: atriple_def asepconj_simp)

lemma atriple_frame_rule:
  assumes ‹φ ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ›
    shows ‹φ ⋆ ξ ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ ⋆ ξ›
using assms by (simp add: atriple_def local.asepconj_assoc local.ucincl_asepconjR)

lemma atriple_complement:
  assumes ‹φ ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ›
      and ‹is_splitting σ σ0 σc›
      and ‹σ0 ⊨ φ›
  obtains σ0' where ‹σ0' ⊨ ψ ⋆ ⊤› and ‹σ0' ♯ σc› and ‹σ' = σ0' + σc›
proof -
  let ?π = ‹↑⇩s σc›
  have ‹ucincl ?π›
    by (simp add: uc_state_ucincl)
  moreover have ‹σ ⊨ ?π ⋆ φ›
    by (metis asat_def assms(2) assms(3) local.asepconjI local.asepconj_comm local.derived_order_refl
      local.is_splitting_def local.uc_state_def mem_Collect_eq)
  moreover from this have ‹σ' ⊨ ?π ⋆ ψ›
    using assms(1) atriple_def calculation local.asepconj_comm by auto
  moreover from this obtain σ0' σc' where ‹is_splitting σ' σ0' σc'› and ‹σ0' ⊨ ψ› and ‹σc' ⊨ ↑⇩s σc›
    by (metis local.asepconjE local.disjoint_sym local.is_splitting_def local.sepalg_comm)
  moreover from this obtain σcc where ‹σc' = σc + σcc› and ‹σc ♯ σcc›
    by (metis asat_def local.derived_order_def local.uc_state_def mem_Collect_eq)
  moreover from calculation obtain ‹σ0' ♯ σcc› and ‹(σ0' + σcc) ⊨ ψ ⋆ ⊤›
    by (meson asat_connectives_characterisation(1) local.asepconjI local.disjoint_sym local.is_splitting_def
        local.sepalg_apart_plus)
  ultimately show ?thesis
    by (metis local.disjoint_sym local.is_splitting_def local.sepalg_apart_plus2
      local.sepalg_apart_plus_distrib local.sepalg_assoc local.sepalg_comm that)
qed

lemma atriple_hoist_pure:
  shows ‹(φ ⋆ ⟨P⟩ ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ) ⟷ (P ⟶ (φ ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ))›
    and ‹(⟨P⟩ ⋆ φ ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ) ⟷ (P ⟶ (φ ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ))› (is ?g2)
proof -
  show ‹(φ ⋆ ⟨P⟩ ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ) ⟷ (P ⟶ (φ ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ))›
    by (clarsimp simp add: atriple_def apure_def asepconj_simp)
  from this show ‹(⟨P⟩ ⋆ φ ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ) ⟷ (P ⟶ (φ ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ))›
    by (simp add: asepconj_comm)
qed

lemma atriple_direct:
  assumes ‹ucincl α›
      and ‹ucincl β›
      and ‹α ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k β›
      and ‹σ ⊨ α›
    shows ‹σ' ⊨ β›
by (metis assms atripleE ucincl_UNIV ucincl_alt)

text‹For minimal states, the atriple can be characterized in simpler terms:›

lemma atriple_minimal:
  assumes ‹is_minimal ξ σ›
      and ‹σ' ⊨ ψ›
    shows ‹ξ ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ›
using assms by (clarsimp simp add: is_minimal_def asat_def atriple_def) (metis asat_def asepconjE
  asepconj_weakenI derived_order_def disjoint_sym reflE sepalg_apart_plus2 sepalg_comm)

text‹The assertion triple is invariant under passage to upward closure:›
lemma atriple_upwards_closure:
  shows ‹((φ ⋆ ⊤) ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k (ψ ⋆ ⊤)) ⟷ (φ ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ)›
    and ‹((⊤ ⋆ φ) ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k (⊤ ⋆ ψ)) ⟷ (φ ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ)›
    and ‹((φ ⋆ ⊤) ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k (⊤ ⋆ ψ)) ⟷ (φ ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ)›
    and ‹((⊤ ⋆ φ) ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k (ψ ⋆ ⊤)) ⟷ (φ ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ)›
    and ‹(φ ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k (ψ ⋆ ⊤)) ⟷ (φ ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ)›
    and ‹(φ ⋆ ⊤ ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ) ⟷ (φ ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ)›
    and ‹(φ ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k (⊤ ⋆ ψ)) ⟷ (φ ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ)›
    and ‹(⊤ ⋆ φ ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ) ⟷ (φ ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ)›
by (simp add: atriple_def local.asepconj_assoc local.asepconj_ident local.ucincl_asepconjR)+

(*<*)
end

context cancellative_sepalg begin
(*>*)

lemma atriple_minimal':
    notes sepalg_simps [simp del]
  assumes ‹is_minimal ξ σ›
      and ‹has_minimal_splittings ξ›
      and ‹σ' ⊨ ψ›
      and ‹σ ♯ σC›
      and ‹σ' ♯ σC›
      and ‹ξ ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ›
    shows ‹ξ ⊩ (σ + σC, σ' + σC) ⊣⇩w⇩e⇩a⇩k ψ›
proof -
  have ‹precise (minimal_states ξ)› and ‹ξ = (minimal_states ξ) ⋆ ⊤›
    using assms(2) local.has_minimal_splittings_via_minimal_states by blast+
  {
       fix π
    assume ‹ucincl π›
       and ‹σ + σC ⊨ π ⋆ ξ›
    moreover from this obtain τ0 τ1 where ‹τ0 ♯ τ1› and ‹τ0 ⊨ ξ› ‹τ1 ⊨ π› and ‹σ + σC = τ0 + τ1›
      by (metis local.asepconjE local.asepconj_comm)
    moreover from this obtain τ0' τ0'' where ‹is_minimal_splitting τ0 τ0' τ0'' ξ›
      by (meson assms(2) local.has_minimal_splittingsE)
    moreover from this have ‹τ0' ⊨ minimal_states ξ›
      by (simp add: asat_def local.is_minimal_splitting_is_minimal local.minimal_states_def)
    moreover from calculation have ‹σ + σC = τ0' + (τ0'' + τ1)›
      using local.is_minimal_splitting_def local.is_splitting_def local.sepalg_assoc
        local.sepalg_pairwise by force
    moreover from calculation and ‹precise (minimal_states ξ)› have ‹σ = τ0'›
      by (metis asat_def assms(1) assms(4) local.derived_orderI is_minimal_splitting_def
        is_splitting_def minimal_states_def preciseE local.sepalg_apart_assoc mem_Collect_eq)
    moreover from calculation have ‹τ0'' + τ1 = σC›
      by (metis assms(4) local.disjoint_sym local.is_minimal_splitting_def local.is_splitting_def
        local.sepalg_apart_assoc local.sepalg_cancel local.sepalg_comm)
    ultimately have ‹(σ' + σC) ⊨ π ⋆ ψ›
      by (metis assms(3) assms(5) local.asat_weaken local.asepconjI local.disjoint_sym
        local.is_minimal_splitting_def local.is_splitting_def local.sepalg_comm local.sepalg_pairwise2)
  }
  from this show ?thesis
    by (simp add: local.asepconj_comm local.atriple_def)
qed

(*<*)
end
(*>*)

context
    fixes α  :: ‹'a::{cancellative_sepalg} assert›
      and α' :: ‹'a assert›
      and β  :: ‹'a assert›
      and β' :: ‹'a assert›
  assumes preciseA:  ‹has_minimal_splittings α›
      and preciseA': ‹has_minimal_splittings α'›
      and preciseB:  ‹has_minimal_splittings β›
      and preciseB': ‹has_minimal_splittings β'›
    notes local_assms = preciseA preciseA' preciseB preciseB'
begin

lemma is_splitting_refine:
    notes sepalg_simps [simp del]
    fixes σ :: ‹'a::{cancellative_sepalg}›
  assumes ‹is_splitting σ σ0 σ1›
      and ‹is_splitting σ0 σ00 σ01›
      and ‹is_splitting σ1 σ10 σ11›
    shows ‹σ00 ♯ σ10›
      and ‹σ01 ♯ σ11›
      and ‹is_splitting σ (σ00 + σ10) (σ01 + σ11)›
proof -
  have ‹σ = σ0 + σ1› and ‹σ0 = σ00 + σ01› and ‹σ1 = σ10 + σ11›
    using assms is_splitting_def by auto
  moreover have ‹σ00 ♯ σ01› and ‹σ10 ♯ σ11›
    using assms is_splitting_def by blast+
  moreover show ‹σ00 ♯ σ10› and ‹σ01 ♯ σ11›
    using sepalg_apart_plus2 sepalg_apart_plus by (metis assms disjoint_sym is_splitting_def)+
  moreover have ‹σ00 ♯ σ11› and ‹σ01 ♯ σ10›
    using sepalg_apart_plus sepalg_apart_plus2 by (metis assms disjoint_sym is_splitting_def)+
  moreover from calculation have ‹σ00 + σ10 ♯ σ01 + σ11›
    by (meson disjoint_sym sepalg_pairwise_apart)
  ultimately show ‹is_splitting σ (σ00 + σ10) (σ01 + σ11)›
    by (clarsimp simp add: is_splitting_def; safe) (metis (no_types, opaque_lifting) disjoint_sym
      sepalg_assoc sepalg_comm sepalg_pairwise)
qed

lemma atriple_frame_rev:
    notes sepalg_simps [simp del]
  assumes ‹assert_strong_disj α' β›
      and ‹α ⋆ β ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k α' ⋆ β'›
      and ‹σ ⊨ α ⋆ β›
  obtains σ'' where ‹α ⊩ (σ, σ'') ⊣⇩w⇩e⇩a⇩k α'› and ‹β ⊩ (σ'', σ') ⊣⇩w⇩e⇩a⇩k β'›
proof -
  from local_assms and assms have ‹σ' ⊨ α' ⋆ β'›
    by (meson atriple_direct has_minimal_splittingsE ucincl_asepconjL)
  moreover from this and assms obtain σA σB where ‹is_splitting σ σA σB› and ‹σA ⊨ α› and ‹σB ⊨ β›
    by (metis asepconjE is_splitting_def)
  moreover from this obtain σA0 σAc σB0 σBc where ‹is_minimal_splitting σA σA0 σAc α› and
          ‹is_minimal_splitting σB σB0 σBc β›
    by (meson has_minimal_splittings_def preciseA preciseB)
  moreover from this have ‹is_minimal α σA0› and ‹is_minimal β σB0›
    by (simp add: is_minimal_splitting_is_minimal)+
  moreover from calculation have ‹σAc ♯ σBc›
    by (metis disjoint_sym is_minimal_splitting_def is_splitting_def sepalg_apart_plus)
  moreover from calculation have ‹is_splitting σ (σA0 + σB0) (σAc + σBc)›
    by (simp add: is_minimal_splitting_def is_splitting_refine(3))
  moreover from calculation have ‹σA0 + σB0 ⊨ α ⋆ β›
    by (meson asepconjI is_minimal_splitting_def is_splitting_refine(1))
  moreover from calculation and assms obtain σAB0' where ‹σAB0' ⊨ (α' ⋆ β') ⋆ ⊤› and ‹σAB0' ♯ (σAc + σBc)›
        and ‹σ' = σAB0' + (σAc + σBc)›
    using atriple_complement by blast
  moreover from this obtain σA0' and σB0' where ‹σA0' ♯ σB0'› and ‹σAB0' = σA0' + σB0'› and ‹σA0' ⊨ α'›
        and ‹σB0' ⊨ β'›
    by (metis asepconjE asepconj_strengthenE has_minimal_splittings_def preciseB' ucincl_UNIV ucincl_asepconjR)
  moreover from assms calculation obtain σA0'' and C C' where ‹σA0' = σA0'' + C› and ‹σA0'' ♯ C› and ‹σA0'' ⊨ α'›
            and ‹C' ≼ σB0› and ‹C' ⊨ β› and ‹σA0'' ♯ C'›
    using assert_strong_disj_def by (metis asat_def calculation(17) calculation(6) derived_orderE
      is_minimal_splitting_def)
  moreover from this and ‹is_minimal β σB0› have ‹C' = σB0›
    using is_minimal_def by blast
  moreover from calculation have ‹σA0'' ♯ σB0'› and ‹C ♯ σB0'›
    using sepalg_pairwise by metis+
  moreover from calculation have ‹σB0' + C ⊨ β'›
    by (meson asat_weaken disjoint_sym has_minimal_splittings_ucincl preciseB')
  moreover have ‹α ⊩ (σA0, σA0'') ⊣⇩w⇩e⇩a⇩k α'› and ‹β ⊩ (σB0, σB0' + C) ⊣⇩w⇩e⇩a⇩k β'›
    by (auto simp add: atriple_minimal calculation)
  moreover from calculation have ‹α ⊩ (σA0 + (σB0 + σAc + σBc), σA0'' + (σB0 + σAc + σBc)) ⊣⇩w⇩e⇩a⇩k α'›
    using preciseA by (auto intro!: atriple_minimal' simp add: is_minimal_splitting_def
      is_splitting_def sepalg_pairwise2)
  moreover have ‹σB0 ♯ (σA0'' + σAc + σBc)›
    using calculation by (metis (no_types, opaque_lifting) disjoint_sym is_minimal_splitting_def
      is_splitting_def sepalg_pairwise2)
  moreover from calculation have ‹σB0' + C ♯ (σA0'' + σAc + σBc)›
    by (metis (no_types, opaque_lifting) disjoint_sym sepalg_pairwise)
  moreover from calculation have ‹β ⊩ (σB0 + (σA0'' + σAc + σBc), σB0' + C + (σA0'' + σAc + σBc)) ⊣⇩w⇩e⇩a⇩k β'›
    using preciseA by (auto simp add: preciseB is_minimal_splitting_def is_splitting_def
      sepalg_pairwise sepalg_pairwise2 intro!: atriple_minimal')
  moreover from calculation have ‹σB0' + C + (σA0'' + σAc + σBc) = σ'›
    by (metis (no_types, lifting) disjoint_sym sepalg_apart_plus sepalg_assoc sepalg_comm)
  moreover from calculation have ‹σA0'' + (σB0 + σAc + σBc) = σB0 + (σA0'' + σAc + σBc)› (is ‹?a = ?b›)
  proof -
    have ‹?a = (σA0'' + σB0) + (σAc + σBc)›
      using calculation by (metis disjoint_sym sepalg_assoc sepalg_pairwise2)
    also have ‹... = (σB0 + σA0'') + (σAc + σBc)›
      using ‹C' = σB0› ‹σA0'' ♯ C'› sepalg_comm by fastforce
    also from calculation have ‹... = ?b›
      by (metis (no_types, lifting) ‹C ♯ σB0'› ‹σA0' = σA0'' + C› ‹σA0'' ♯ C› ‹σA0'' ♯ σB0'›
        ‹σAB0' = σA0' + σB0'› ‹σAB0' ♯ σAc + σBc› ‹σAc ♯ σBc› ‹σB0 ♯ σA0'' + σAc + σBc›
        sepalg_assoc sepalg_pairwise sepalg_pairwise2)
    finally show ?thesis
      by auto
  qed
  moreover from calculation have ‹σA0 + (σB0 + σAc + σBc) = σ›
    by (simp add: is_minimal_splitting_def is_splitting_def sepalg_assoc sepalg_pairwise2)
  moreover from calculation have ‹α ⊩ (σ, σA0'' + (σB0 + σAc + σBc)) ⊣⇩w⇩e⇩a⇩k α'› and
          ‹β ⊩ (σA0'' + (σB0 + σAc + σBc), σ') ⊣⇩w⇩e⇩a⇩k β'›
    by fastforce+
  ultimately show ?thesis
    using that by blast
qed

(*<*)
end

context sepalg
begin
(*>*)

definition atriple_rel :: ‹'a assert ⇒ ('a ⇒ ('t × 'a) ⇒ bool) ⇒ ('t ⇒ 'a assert) ⇒ bool›
      ("(_) ⊢/ _/ ⊣⇩R (_)" [50,50,50]50) where
  ‹φ ⊢ R ⊣⇩R ψ ≡ is_local R φ ∧ (∀σ σ' v. R σ (v, σ') ⟶ σ ⊨ φ ⟶ σ' ⊨ ψ v ⋆ ⊤)›

definition atriple_rel_id :: ‹'a assert ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool› ("_∼_") where
  ‹ξ∼P ≡ is_local0 P ξ ∧ (∀σ σ'. σ ⊨ ξ ⟶ P σ σ' ⟶ σ' ⊨ ξ)›

definition atriple_rel_ind :: ‹'a assert ⇒ ('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ ('t × 'a) ⇒ bool) ⇒
      ('t ⇒ 'a assert) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool› ("(_:_) ⊩⇩i/ _/ ⊣ (_:_)" [50,50,50]50) where
  ‹(φ:P ⊩⇩i R ⊣ ψ:Q) ≡ (φ ⊢ R ⊣⇩R ψ) ∧ (φ∼P) ∧ (∀v. ((ψ v)∼Q))
      ∧ (∀σ0 σ1 σ0' σ1' v0 v1.
            P σ0 σ1 ⟶ R σ0 (v0, σ0') ⟶ R σ1 (v1, σ1') ⟶ v0 = v1 ∧ Q σ0' σ1')›

lemma atriple_local:
  assumes ‹is_local R φ›
      and  ‹⋀σ σ' v. R σ (v, σ') ⟹ σ ⊨ φ ⟹ σ' ⊨ ψ v›
      and ‹R σ (v, σ')›
    shows ‹φ ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ v›
using assms by (clarsimp simp add: is_local_def atriple_def asat_def asepconj_def) (metis local.disjoint_sym)

lemma atriple_local':
  assumes ‹is_local R φ›
      and  ‹⋀σ σ' v. R σ (v, σ') ⟹ σ ⊨ φ ⟹ σ' ⊨ ψ v ⋆ ⊤›
      and ‹R σ (v, σ')›
    shows ‹φ ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k ψ v›
proof -
  from assms have ‹φ ⊩ (σ, σ') ⊣⇩w⇩e⇩a⇩k (λv. ψ v ⋆ ⊤) v›
    by (intro atriple_local[where R=R]; simp)
  from this show ?thesis
    using atriple_upwards_closure(5) by blast
qed

lemma atriple_rel_upwards_closure:
  shows ‹(φ ⊢ R ⊣⇩R ψ) ⟷ (φ ⋆ ⊤ ⊢ R ⊣⇩R (λv. ψ v ⋆ ⊤))›
proof
  assume ‹φ ⊢ R ⊣⇩R ψ›
  moreover {
       fix σ v σ'
    assume ‹is_local R φ›
       and ‹∀σ σ' v. R σ (v, σ') ⟶ σ ⊨ φ ⟶ σ' ⊨ ψ v ⋆ UNIV›
       and ‹R σ (v, σ')›
       and ‹σ ⊨ φ ⋆ UNIV›
    from this calculation have ‹σ' ⊨ ψ v ⋆ UNIV›
      by (metis atriple_local' local.atripleE local.ucincl_UNIV)
  }
  ultimately show ‹φ ⋆ ⊤ ⊢ R ⊣⇩R (λv. ψ v ⋆ ⊤)›
    by (auto simp add: atriple_rel_def is_local_upwards_closure asepconj_simp)
next
  assume ‹φ ⋆ UNIV ⊢ R ⊣⇩R (λv. ψ v ⋆ UNIV)›
  moreover {
       fix σ σ' v
    assume ‹is_local R φ›
       and ‹∀σ σ' v. R σ (v, σ') ⟶ σ ⊨ φ ⋆ UNIV ⟶ σ' ⊨ ψ v ⋆ UNIV›
       and ‹R σ (v, σ')›
       and ‹σ ⊨ φ›
    from this have ‹σ' ⊨ ψ v ⋆ UNIV›
      by (simp add: local.asepconj_weakenI)
  }
  ultimately show ‹φ ⊢ R ⊣⇩R ψ›
    by (clarsimp simp add: atriple_rel_def is_local_upwards_closure asepconj_simp)
qed

lemma atriple_rel_hoist_pure:
  shows ‹(φ ⋆ ⟨P⟩ ⊢ R ⊣⇩R ψ) ⟷ (P ⟶ (φ ⊢ R ⊣⇩R ψ))›
    and ‹(⟨P⟩ ⋆ φ ⊢ R ⊣⇩R ψ) ⟷ (P ⟶ (φ ⊢ R ⊣⇩R ψ))›
proof -
  {
    assume ‹φ ⋆ ⟨P⟩ ⊢ R ⊣⇩R ψ›
       and ‹P›
    from this have ‹φ ⊢ R ⊣⇩R ψ›
      by (simp add: atriple_rel_def local.asepconj_False_True(2) local.asepconj_comm
        local.asepconj_weaken2I local.is_local_upwards_closure(2))
  } moreover {
    assume ‹¬ P›
    from this have ‹φ ⋆ ⟨P⟩ ⊢ R ⊣⇩R ψ›
      by (simp add: atriple_rel_def local.asat_apure_distrib'(1) local.is_local_hoist_pure)
  } moreover {
    assume ‹φ ⊢ R ⊣⇩R ψ›
    from this have ‹φ ⋆ ⟨P⟩ ⊢ R ⊣⇩R ψ›
      by (clarsimp simp add: atriple_rel_def apure_def asepconj_simp)
        (metis atriple_local' local.atripleE local.is_local_empty local.is_local_frame local.ucincl_UNIV)
  }
  ultimately show ‹(φ ⋆ ⟨P⟩ ⊢ R ⊣⇩R ψ) = (P ⟶ φ ⊢ R ⊣⇩R ψ)›
    by auto
  from this show ‹(⟨P⟩ ⋆ φ ⊢ R ⊣⇩R ψ) ⟷ (P ⟶ (φ ⊢ R ⊣⇩R ψ))›
    by (simp add: asepconj_comm)
qed

lemma atriple_rel_upwards_closure':
  shows ‹((φ ⋆ ⊤) ⊢ R ⊣⇩R (λv. ψ v ⋆ ⊤)) ⟷ (φ ⊢ R ⊣⇩R ψ)›
    and ‹((⊤ ⋆ φ) ⊢ R ⊣⇩R (λv. ⊤ ⋆ ψ v)) ⟷ (φ ⊢ R ⊣⇩R ψ)›
    and ‹((φ ⋆ ⊤) ⊢ R ⊣⇩R (λv. ⊤ ⋆ ψ v)) ⟷ (φ ⊢ R ⊣⇩R ψ)›
    and ‹((⊤ ⋆ φ) ⊢ R ⊣⇩R (λv. ψ v ⋆ ⊤)) ⟷ (φ ⊢ R ⊣⇩R ψ)›
    and ‹(φ ⊢ R ⊣⇩R (λv. ψ v ⋆ ⊤)) ⟷ (φ ⊢ R ⊣⇩R ψ)›
    and ‹(φ ⋆ ⊤ ⊢ R ⊣⇩R ψ) ⟷ (φ ⊢ R ⊣⇩R ψ)›
    and ‹(φ ⊢ R ⊣⇩R (λv. ⊤ ⋆ ψ v)) ⟷ (φ ⊢ R ⊣⇩R ψ)›
    and ‹(⊤ ⋆ φ ⊢ R ⊣⇩R ψ) ⟷ (φ ⊢ R ⊣⇩R ψ)›
by (rewrite at "⌑ ⟷ _" atriple_rel_upwards_closure, rewrite at "_ ⟷  ⌑"
  atriple_rel_upwards_closure, simp add: asepconj_simp asepconj_comm asepconj_UNIV_collapse_top)+

lemma atriple_rel_bind:
    fixes φ :: ‹'a assert›
      and ψ :: ‹'v ⇒ 'a assert›
      and R :: ‹'a ⇒ ('v × 'a) ⇒ bool›
      and S :: ‹'v ⇒ 'a ⇒ ('w × 'a) ⇒ bool›
  assumes A: ‹φ ⊢ R ⊣⇩R ψ›
      and B: ‹⋀v. (ψ v ⊢ S v ⊣⇩R τ)›
    shows ‹φ ⊢ R ◊ S ⊣⇩R τ›
proof -
  from assms have ‹⋀v. (ψ v ⋆ ⊤ ⊢ S v ⊣⇩R τ)›
    by (metis atriple_rel_upwards_closure local.asepconj_UNIV_idempotent local.asepconj_assoc)
  moreover {
    assume §: ‹(⋀v. is_local (S v) (ψ v ⋆ UNIV) ∧ (∀σ σ' va. S v σ (va, σ') ⟶ σ ∈ ψ v ⋆ UNIV ⟶ σ' ∈ τ va ⋆ UNIV))›
        and ‹is_local R φ›
        and ‹∀σ σ' v. R σ (v, σ') ⟶ σ ∈ φ ⟶ σ' ∈ ψ v ⋆ UNIV›
    moreover {
         fix σ_0 σ_1 σ_0' v
      assume ‹σ_0 ♯ σ_1›
         and ‹σ_0 ⊨ φ›
         and ‹(R ◊ S) σ_0 (v, σ_0')›
      with assms § have ‹σ_0' ♯ σ_1› 
        unfolding rel_compose_def atriple_rel_def is_local_def by meson
    } moreover {
         fix σ_0 σ_1 v σ'
      assume ‹σ_0 ♯ σ_1›
         and ‹σ_0 ⊨ φ›
         and ‹(R ◊ S) (σ_0 + σ_1) (v, σ')›
      with assms § have ‹∃σ_0'. (R ◊ S) σ_0 (v, σ_0') ∧ σ' = σ_0' + σ_1›
        unfolding rel_compose_def atriple_rel_def is_local_def by (smt (verit, best))
    } moreover {
         fix σ_0 σ_1 v σ_0' σ'
      assume ‹σ_0 ♯ σ_1›
         and ‹σ_0 ⊨ φ›
         and ‹(R ◊ S) σ_0 (v, σ_0') ∧ σ' = σ_0' + σ_1›
      with assms § have ‹(R ◊ S) (σ_0 + σ_1) (v, σ')›
        unfolding rel_compose_def atriple_rel_def is_local_def  by (smt (verit, best))
    }
    ultimately have ‹is_local (R ◊ S) φ›
      by (intro is_localI) 
  } moreover {
       fix σ σ' v
    assume ‹⋀v. is_local (S v) (ψ v) ∧ (∀σ σ' va. S v σ (va, σ') ⟶ σ ∈ ψ v ⟶ σ' ∈ τ va ⋆ UNIV)›
       and ‹is_local R φ›
       and ‹∀σ σ' v. R σ (v, σ') ⟶ σ ∈ φ ⟶ σ' ∈ ψ v ⋆ UNIV›
       and ‹(R ◊ S) σ (v, σ')›
       and ‹σ ∈ φ›
    from this calculation have ‹σ' ∈ τ v ⋆ UNIV›
      by (metis asat_def atriple_rel_def rel_compose_def)
  }
  ultimately show ?thesis
    using assms by (auto simp add: atriple_rel_def asat_def)
qed

lemma atriple_rel_disj:
  assumes ‹φ ⊢ R ⊣⇩R ψ›
      and ‹φ ⊢ S ⊣⇩R ψ›
    shows ‹φ ⊢ (λa b. R a b ∨ S a b) ⊣⇩R ψ›
using assms by (clarsimp simp add: atriple_rel_def is_local_disj)

(*<*)
end

end
(*>*)