Theory Phi_BI

section ‹An Implementation of φ-Bunched Implications›

text ‹It also contains a simplified BI specialized for only necessary constructs required
  by ∗‹Multi-Term Form›.

➧ ∗‹Multi-Term Form› is the canonical form in the reasoning of φ-System, which demonstrates
  abstractions directly and clearly in a localized way. It is characterized by form,
\[ ‹∃a. (x⇩₁ ⦂ T⇩₁ ∗ x⇩₂ ⦂ T⇩₂ ∗ ⋯ x⇩_n ⦂ T⇩_n) ∧ P› \]
where ‹P› is a pure proposition only containing free variables occurring in ‹x⇩₁,⋯,x⇩_n,a›.
It relates the concrete resource to a set of abstract objects ‹{(x⇩₁,⋯,x⇩_n) |a. P}› if
  ∗‹variables ‹a› are not free in ‹T⇩₁,⋯,T⇩_n››.
All specifications in φ-System are in Multi-Term Form. It is so pervasive that we use a set-like
notation to denote them,
\[ ‹(x⇩₁ ⦂ T⇩₁ ∗ x⇩₂ ⦂ T⇩₂ ∗ ⋯ x⇩_n ⦂ T⇩_n 𝗌𝗎𝖻𝗃 a. P)› \]
Readers may read it as a set,
\[ ‹{ x⇩₁ ⦂ T⇩₁ ∗ x⇩₂ ⦂ T⇩₂ ∗ ⋯ x⇩_n ⦂ T⇩_n |a. P }› \]

➧ ∗‹Simple Multi-Term Form› is a MTF where there is no existential quantification and the attached
  ‹P› is trivial ‹True›, viz., it is characterized by
  \[ ‹x⇩₁ ⦂ T⇩₁ ∗ ⋯ ∗ x⇩_n ⦂ T⇩_n› \]
›

text ‹
Specifically, in this minimal specialized BI:

  ▪ It does not have a general additive conjunction (‹∧›) that connects any BI assertions,
    but only the one (‹A 𝗌𝗎𝖻𝗃 P›) connects a BI assertion ‹A› and a pure assertion ‹P›,
    because it is exactly what at most the MTF requires.

  ▪ Implication does not occur in assertions (of φ-SL), but it represents transformations of
    abstraction so has a significant role in reasoning (rules).
    We emphasize this transformation by assigning the implication with notation
    ‹A 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 B 𝖺𝗇𝖽 P ≜ A ⟶ B ∧ P›, where ‹P› is a pure assertion.
    The ‹P› helps to capture the information (in abstract domain) lost in the
    weakening of this implication.
    Currying implications like ‹A ⟶ B ⟶ C› are never used in φ-BI.

  ▪ Optionally we have universal quantification. It can be used to quantify free variables
    if for any reason free variables are inadmissible. The universal quantifier is typically
    not necessary in φ-BI and φ-SL, where we use free variables directly. However, in some
    situation, like when we consider transitions of resource states and we want a transition
    relation for each procedure, we need a single universally quantified assertion,
    instead of a family of assertions indexed by free variables.

  ▪ The use of a implication represents a transformation of abstraction.
    Therefore, implications are never curried or nested, always in form ‹X ⟶ Y ∧ P›
    where ‹X, Y› are MTF and ‹P› is a pure proposition.
    We denote them by notation ‹X 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 Y 𝖺𝗇𝖽 P›.

  ▪ It only has multiplicative conjunctions, specialized additive conjunction described above,
    existential quantification, and optionally universal quantification,
    which are all the MTF requires,
    plus implications that only occur in reasoning rules.
    Any other things, should be some specific φ-Types expressing their meaning
    specifically and particularly.
›

theory Phi_BI
  imports "Phi_Logic_Programming_Reasoner.Phi_Logic_Programming_Reasoner" Phi_Preliminary
  abbrevs "<:>" = "⦂"
      and "<implies>" = "𝗂𝗆𝗉𝗅𝗂𝖾𝗌"
      and "<and>"  = "𝖺𝗇𝖽"
      and "<subj>" = "𝗌𝗎𝖻𝗃"
      and "<remains>" = "𝗋𝖾𝗆𝖺𝗂𝗇𝗌"
begin

subsection ‹Bottom›

abbreviation Bottom ("⊥") where ‹Bottom ≡ (0::'a::sep_magma set)›
abbreviation Bottom_abs ("⊥⇩_λ") where ‹Bottom_abs ≡ (0 :: 'b ⇒ 'a::sep_magma set)›

subsection ‹φ-Type›

type_synonym ('concrete,'abstract) φ = " 'abstract ⇒ 'concrete set "

definition φType :: "'b ⇒ ('a,'b) φ ⇒ 'a set" (infix "⦂" 20) where " (x ⦂ T) = (T x)"

lemma typing_inhabited: "p ∈ (x ⦂ T) ⟹ Inhabited (x ⦂ T)"
  unfolding Inhabited_def φType_def by blast

lemma φType_eqI:
  ‹(∀x p. p ∈ (x ⦂ a) ⟷ p ∈ (x ⦂ b)) ⟹ a = b›
  unfolding φType_def by blast

ML_file ‹library/tools/simp_congruence.ML›

text ‹The implementation represents BI assertions by sets simply, in shallow embedding manner.›

subsection ‹Implication›

definition Imply :: " 'a set ⇒ 'a set ⇒ bool ⇒ bool " ("(2_)/ 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 (2_)/ 𝖺𝗇𝖽 (2_)" [13,13,13] 12)
  where "(A 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 B 𝖺𝗇𝖽 P) ⟷ (∀v. v ∈ A ⟶ v ∈ B ∧ P)"

abbreviation SimpleImply :: " 'a set ⇒ 'a set ⇒ bool " ("(2_)/ 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 (2_)" [13,13] 12)
  where ‹SimpleImply T U ≡ Imply T U True›

declare [[φreason_default_pattern ‹?X 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 ?Y 𝖺𝗇𝖽 _› ⇒ ‹?X 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 ?Y 𝖺𝗇𝖽 _› (10)]]

text ‹Semantics of antecedent \<^pattern_prop>‹X 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 Y 𝖺𝗇𝖽 ?P›:
  Given the source \<^term>‹X› and the target \<^term>‹Y›, find a reasoning way to do the transformation,
  which may bring in additional pure facts \<^pattern_term>‹?P› and generate proof obligations.›

definition FOCUS_TAG :: " 'a ⇒ 'a "  ("❬ _ ❭") where [iff]: "❬ x ❭ = x"

abbreviation Remains :: ‹ 'a::{sep_disj,times} set ⇒ 'a set ⇒ 'a set › (infix "𝗋𝖾𝗆𝖺𝗂𝗇𝗌" 13)
  where ‹(X 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R) ≡ R * ❬ X ❭›

declare [[φreason_default_pattern
    ‹?X 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 ?Y 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ 𝖺𝗇𝖽 _› ⇒ ‹?X 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 ?Y 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 _ 𝖺𝗇𝖽 _› (20)
]]

text ‹For antecedent \<^pattern_prop>‹X 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 Y 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 ?R 𝖺𝗇𝖽 _›, the semantics is slightly different
  where it specifies extracting given \<^term>‹Y› from given \<^term>‹X› and leaving some \<^schematic_term>‹?R›.›


subsubsection ‹Proof \& Reasoning Rules›

lemma zero_implies_any[φreason 2000, simp]:
  ‹0 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 X›
  unfolding Imply_def zero_set_def by simp

lemma implies_refl[simp,
    φreason 4000 for ‹?A 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 ?A 𝖺𝗇𝖽 ?P›,
    φreason 900 for ‹?A 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 ?B 𝖺𝗇𝖽 ?P› ― ‹Unification can be aggressive.›
]:
  "A 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 A" unfolding Imply_def by fast

lemma implies_refl_ty[φreason 800 for ‹?x ⦂ ?T 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 ?y ⦂ ?T' 𝖺𝗇𝖽 _›]:
  "𝗉𝗋𝖾𝗆𝗂𝗌𝖾 x = y ⟹ x ⦂ T 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 y ⦂ T" unfolding Imply_def by fast



lemma implies_union:
  ‹ A 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 X 𝖺𝗇𝖽 P
⟹ A 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 X + Y 𝖺𝗇𝖽 P›
  ‹ A 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 Y 𝖺𝗇𝖽 P
⟹ A 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 X + Y 𝖺𝗇𝖽 P›
  unfolding Imply_def by simp_all

(* abbreviation SimpleSubty :: " 'a set ⇒ 'a set ⇒ bool " ("(2_ 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 _)" [2,14] 13)
  where "(A ⟼ B) ≡ (❙s❙u❙b❙t❙y❙p❙e A 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 B 𝖺𝗇𝖽 True)" *)
(* lemma SubtyE[elim]: "A 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 B 𝖺𝗇𝖽 P ⟹ (¬ Inhabited A ⟹ C) ⟹ (Inhabited A ⟹ Inhabited B ⟹ A ⊆ B ⟹ P ⟹ C) ⟹ C"
   unfolding Imply_def Inhabited_def by (auto intro: Inhabited_subset)
lemma SubtyI[intro]: "Inhabited A ⟹ A ⊆ B ⟹ P ⟹ A 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 B 𝖺𝗇𝖽 P"
  and [intro]: "¬ Inhabited A ⟹ A 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 B 𝖺𝗇𝖽 P" unfolding Imply_def Inhabited_def by auto *)


lemma implies_trans:
  "A 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 B 𝖺𝗇𝖽 P
    ⟹ (P ⟹ B 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 C 𝖺𝗇𝖽 Q)
    ⟹ A 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 C 𝖺𝗇𝖽 P ∧ Q"
  unfolding Imply_def by auto

lemma implies_weaken:
  ‹ P ⟶ P'
⟹ A 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 B 𝖺𝗇𝖽 P
⟹ A 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 B 𝖺𝗇𝖽 P'›
  unfolding Imply_def by simp

lemma implies_left_prod:
  "U' 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 U 𝖺𝗇𝖽 P ⟹ R * U' 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 R * U 𝖺𝗇𝖽 P "
  unfolding Imply_def split_paired_All times_set_def by blast

lemma implies_right_prod:
  "U' 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 U 𝖺𝗇𝖽 P ⟹ U' * R 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 U * R 𝖺𝗇𝖽 P "
  unfolding Imply_def split_paired_All times_set_def by blast

lemma assertion_eq_intro:
  ‹ P 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 Q
⟹ Q 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 P
⟹ P = Q›
  unfolding Imply_def by blast

subsubsection ‹Inhabitance Reasoning - Part II›

lemma [φreason 1100]:
  ‹PROP Extract_Elimination_Rule (Trueprop (X 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 Y)) (Inhabited X) (Inhabited Y) ›
  unfolding Extract_Elimination_Rule_def Imply_def Inhabited_def by blast

lemma [φreason 1000]:
  ‹PROP Extract_Elimination_Rule (Trueprop (X 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 Y 𝖺𝗇𝖽 P)) (Inhabited X) (Inhabited Y ∧ P) ›
  unfolding Extract_Elimination_Rule_def Imply_def Inhabited_def by blast


subsection ‹Specialized Additive Conjunction›

definition Subjection :: " 'p set ⇒ bool ⇒ 'p set " (infixl "𝗌𝗎𝖻𝗃" 15)
  where " (T 𝗌𝗎𝖻𝗃 P) = {p. p ∈ T ∧ P}"

lemma Subjection_expn[φexpns]:
  "p ∈ (T 𝗌𝗎𝖻𝗃 P) ⟷ p ∈ T ∧ P"
  unfolding Subjection_def by simp

lemma Subjection_inhabited[elim!,φinhabitance_rule]:
  ‹Inhabited (S 𝗌𝗎𝖻𝗃 P) ⟹ (P ⟹ Inhabited S ⟹ C) ⟹ C›
  unfolding Inhabited_def by (simp add: Subjection_expn)

lemma Subjection_cong[cong]:
  ‹P ≡ P' ⟹ (P' ⟹ S ≡ S') ⟹ (S 𝗌𝗎𝖻𝗃 P) ≡ (S' 𝗌𝗎𝖻𝗃 P')›
  unfolding atomize_eq set_eq_iff by (simp add: Subjection_expn, blast)

(* lemma [φreason 1000]:
  " T 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 T' 𝖺𝗇𝖽 P
⟹ (P ⟹ 𝗉𝗋𝖾𝗆𝗂𝗌𝖾 Q)
⟹ T 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 T' 𝗌𝗎𝖻𝗃 Q 𝖺𝗇𝖽 P"
  unfolding Imply_def Premise_def by (simp add: Subjection_expn) *)

lemma Subjection_imp_I:
  ‹ P
⟹ S 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 S' 𝖺𝗇𝖽 Q
⟹ S 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 S' 𝗌𝗎𝖻𝗃 P 𝖺𝗇𝖽 Q›
  unfolding Imply_def by (simp add: Subjection_expn)

lemma Subjection_True [simp, φprogramming_safe_simps]: "(T 𝗌𝗎𝖻𝗃 True) = T"
  unfolding set_eq_iff by (simp add: Subjection_expn)

lemma Subjection_Flase[simp, φprogramming_safe_simps]: ‹(T 𝗌𝗎𝖻𝗃 False) = 0›
  unfolding set_eq_iff by (simp add: Subjection_expn zero_set_def)

lemma Subjection_Subjection:
  ‹(S 𝗌𝗎𝖻𝗃 P 𝗌𝗎𝖻𝗃 Q) = (S 𝗌𝗎𝖻𝗃 P ∧ Q)›
  unfolding set_eq_iff
  by (simp add: Subjection_expn)

lemma Subjection_Zero[simp]:
  ‹(0 𝗌𝗎𝖻𝗃 P) = 0›
  unfolding set_eq_iff
  by (simp add: Subjection_expn zero_set_def)

(* lemma (in φempty) [simp]: "(VAL (S 𝗌𝗎𝖻𝗃 P)) = (VAL S 𝗌𝗎𝖻𝗃 P)" by (simp add: φexpns set_eq_iff) blast
lemma (in φempty) [simp]: "(OBJ (S 𝗌𝗎𝖻𝗃 P)) = (OBJ S 𝗌𝗎𝖻𝗃 P)" by (simp add: φexpns set_eq_iff) *)

lemma Subjection_times[simp]:
  ‹(S 𝗌𝗎𝖻𝗃 P) * T = (S * T 𝗌𝗎𝖻𝗃 P)›
  ‹T * (S 𝗌𝗎𝖻𝗃 P) = (T * S 𝗌𝗎𝖻𝗃 P)›
  unfolding Subjection_def times_set_def set_eq_iff by blast+

lemma Subjection_plus:
  ‹(A + B 𝗌𝗎𝖻𝗃 P) = (A 𝗌𝗎𝖻𝗃 P) + (B 𝗌𝗎𝖻𝗃 P)›
  unfolding set_eq_iff by (simp add: φexpns) blast

subsection ‹Existential Quantification›

definition ExSet :: " ('c ⇒ 'a set) ⇒ 'a set" (binder "∃*" 14)
  where "ExSet S = {p. (∃c. p ∈ S c)}"
notation ExSet (binder "∃⇧^s" 14)

lemma ExSet_expn[φexpns]: "p ∈ ExSet S ⟷ (∃c. p ∈ S c)" unfolding ExSet_def by simp

lemma ExSet_inhabited[φinhabitance_rule, elim!]:
  ‹Inhabited (ExSet S) ⟹ (⋀x. Inhabited (S x) ⟹ C) ⟹ C›
  unfolding Inhabited_def by (simp add: φexpns; blast)

syntax
  "_SetcomprNu" :: "'a ⇒ idts ⇒ bool ⇒ 'a set"  ("_ 𝗌𝗎𝖻𝗃/ _./ _" [14,0,15] 14)

translations
  " X 𝗌𝗎𝖻𝗃 idts. P " ⇌ "∃* idts. X 𝗌𝗎𝖻𝗃 P"
  " X 𝗌𝗎𝖻𝗃 idts. CONST True " ⇌ "∃* idts. X"

text ‹Semantically, an existential quantification in BI actually represents union of resources
  matching the existentially quantified assertion, as shown by the following lemma.›

lemma " Union { S x |x. P x } = (S x 𝗌𝗎𝖻𝗃 x. P x) "
  by (simp add: set_eq_iff φexpns) blast


lemma ExSet_pair: "ExSet T = (∃*a b. T (a,b) )"
  unfolding set_eq_iff by (clarsimp simp add: φexpns)

(* lemma (in φempty_sem) [simp]: "p ∈ 𝒮  (ExSet T) ⟷ (∃z. p ∈ 𝒮  (T z) )" by (cases p, simp_all add: φexpns set_eq_iff)
lemma (in φempty_sem) [simp]: "p ∈ !𝒮 (ExSet T) ⟷ (∃z. p ∈ !𝒮 (T z) )" by (cases p, simp_all add: φexpns set_eq_iff) *)
(* lemma (in φempty) [simp]: "(VAL ExSet T) = (∃*c. VAL T c)" by (simp add: φexpns set_eq_iff) blast
lemma (in φempty) [simp]: "(OBJ ExSet T) = (∃*c. OBJ T c)" by (simp add: φexpns set_eq_iff) *)

lemma ExSet_times_left [simp]: "(ExSet T * R) = (∃* c. T c * R )" by (simp add: φexpns set_eq_iff, blast)
lemma ExSet_times_right[simp]: "(L * ExSet T) = (∃* c. L * T c)" by (simp add: φexpns set_eq_iff) blast

lemma ExSet_simps[simp]:
  ‹ExSet (λ_. T) = T›
  ‹(∃* x. F x 𝗌𝗎𝖻𝗃 x = y) = (F y)›
  ‹(∃* x. F x 𝗌𝗎𝖻𝗃 x = y ∧ P x) = (F y 𝗌𝗎𝖻𝗃 P y)›
  ‹(X b 𝗌𝗎𝖻𝗃 P b 𝗌𝗎𝖻𝗃 b. Q b) = (X b 𝗌𝗎𝖻𝗃 b. P b ∧ Q b)›
  ‹(X2 a b 𝗌𝗎𝖻𝗃 a. P2 a b 𝗌𝗎𝖻𝗃 b. Q b) = (X2 a b 𝗌𝗎𝖻𝗃 a b. P2 a b ∧ Q b)›
  ‹ExSet 0 = 0›
  unfolding set_eq_iff by (simp_all add: φexpns) blast

declare ExSet_simps(1)[φprogramming_safe_simps]

(*lemma [φreason 200]: (*depreciated*)
   "(⋀c. T c 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 T' 𝖺𝗇𝖽 P c)
⟹ (ExSet T) 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 T' 𝖺𝗇𝖽 (∃c. P c)"
  unfolding Imply_def by (simp add: φexpns) blast *)

(* lemma [φreason 300]:
  ‹(⋀c. S c 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 S' 𝖺𝗇𝖽 P)
⟹ (ExSet S) 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 S' 𝖺𝗇𝖽 P›
  unfolding Imply_def by (simp add: φexpns, blast) *)

lemma ExSet_imp_I:
  ‹ S 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 S' x 𝖺𝗇𝖽 P
⟹ S 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 (ExSet S') 𝖺𝗇𝖽 P›
  unfolding Imply_def by (clarsimp simp add: φexpns, blast)

(*lemma [φreason 100 for ‹?S 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 ?S' 𝖺𝗇𝖽 (Ex ?P)›]:
  ‹ S 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 S' 𝖺𝗇𝖽 P x
⟹ S 𝗂𝗆𝗉𝗅𝗂𝖾𝗌 S' 𝖺𝗇𝖽 (Ex P)›
  unfolding Imply_def by (clarsimp simp add: φexpns, blast) *)

lemma ExSet_plus:
  ‹(∃*x. A x + B x) = ExSet A + ExSet B›
  ‹ExSet (A + B) = ExSet A + ExSet B›
  unfolding set_eq_iff by (simp_all add: φexpns plus_fun) blast+

subsection ‹Universal Quantification›

definition AllSet :: ‹('a ⇒ 'b set) ⇒ 'b set› (binder "∀⇧^S" 10)
  where ‹AllSet X = {y. ∀x. y ∈ X x}›

lemma AllSet_expn[φexpns]:
  ‹p ∈ (∀⇧^Sx. B x) ⟷ (∀x. p ∈ B x)›
  unfolding AllSet_def by simp

lemma AllSet_subset:
  ‹A ⊆ (∀⇧^S x. B x) ⟷ (∀x. A ⊆ B x)›
  unfolding AllSet_def subset_iff by (rule; clarsimp; blast)

lemma AllSet_refl:
  ‹(⋀x. refl (B x))
⟹ refl (∀⇧^S x. B x)›
  unfolding AllSet_def
  by (simp add: refl_on_def)

lemma AllSet_trans:
  ‹(⋀x. trans (B x))
⟹ trans (∀⇧^S x. B x)›
  unfolding AllSet_def
  by (smt (verit) mem_Collect_eq transD transI)





end