Theory Resource_Space

text ‹The idea of the locale-based modular semantics framework is using Virtual Datatype~\cite{VDT}
to formalize types and values modularly and using an improved Statespace~\cite{Statespace} to
formalize resources.›

section ‹Framework for Modular Formalization of Resources \& Fictional Resources›

text ‹Algebras used in the formalization are given in~\cite{Algebras}.›

theory Resource_Space
  imports "Phi_BI.Phi_Fiction" "Phi_Statespace.StateFun" Phi_BI.Phi_Algebra_Set
begin



subsection ‹Kind›

text ‹
The section presents the improved Statespace, ∗‹resource space›, which is specialized for
  resource models in separation algebra.
In addition, the section also presents a similar construct, ∗‹fiction space›,
  for formalize modularly fictions used in fictional separation (i.e., Fictional
  Separation Logic~\cite{FSL}).›

declare [[typedef_overloaded]]

datatype ('CONS_NAME,'REP,'ABS) kind =
  kind (name: 'CONS_NAME) (project: "'REP ⇒ 'ABS") (inject: "'ABS ⇒ 'REP") (domain: ‹'ABS sep_homo_set›)

hide_const (open) name project inject domain

declare [[typedef_overloaded=false]]

syntax
  "_entry_updbind" :: "'a ⇒ 'a ⇒ updbind"     ("(2_ #=/ _)")
  "_fine_Update"  :: "'a ⇒ updbinds ⇒ 'a"  ("_/'((_)')⇩?" [1000, 0] 900)

translations
  "f(x#=y)" => "f(CONST kind.name x := CONST kind.inject x y)"



subsection ‹Resource Space›

text ‹The section gives a locale-based approach for modelling modularly compound resource states
  that combine different kinds of resources modelled by different types.
It is in essence a modified Statespace ~\cite{Statespace} with the sort constraint of ‹sep_algebra›.

Different kinds of resources can use different types for modelling, and the compound is represented
by a uniform deep representation, a finite partial map of type
  \<^typ>‹'NAME ⇒ ('REP::sep_algebra)›
where ‹'NAME› is the type of the names of resource kinds that identify each resource kind;
type ‹'REP› is the deep representation of states of resources.

We reuse \<^typ>‹('NAME, 'REP::sep_algebra, 'T::sep_algebra) kind› to represent resource kinds.
A resource kind is a triple of ‹name::'NAME› and ‹project :: 'REP ⇒ 'T, inject :: 'T ⇒ 'REP› between
  the deep representation ‹'REP› of the states and the model ‹'T› of this kind of resource.

The model ‹'T› is required to be a separation algebra, albeit
it does not require the physical resource to be separable because any structure can be
  lifted to a a discrete separable because by introducing a unit element standing for
 none resource or no specification.
›

locale sep_inj_proj =
  inj: closed_homo_sep inject + inj: homo_one inject +
  prj: homo_sep project + prj: homo_one project
  for inject :: ‹'T::sep_algebra ⇒ 'REP::sep_algebra›
  and project:: ‹'REP::sep_algebra ⇒ 'T::sep_algebra›
    ― ‹the project' cannot be arbitrarily any inverse function of the inject',
      but must be the one itself is also a separation homomorphism.›
+ assumes proj_inj[simp]: "project (inject x) = x"
    and   mult_in_dom:    ‹a ## b ⟹
              a * b = inject c ⟷ (∃a' b'. a = inject a' ∧ b = inject b' ∧ a' * b' = c)›
begin

sublocale inj: sep_orthogonal_monoid inject UNIV
  by (standard; simp; metis mult_in_dom prj.sep_disj_homo_semi proj_inj)

lemma inject_inj[iff]:
  ‹inject a = inject b ⟷ a = b›
  by (metis proj_inj)

lemma inject_assoc_homo[simp]:
  "inject y ## R ∧ inject x ## inject y * R
⟹ inject x * inject y * R = inject (x * y) * R"
  by (metis mult_in_dom sep_disj_multD1)

lemma inj_Sep_Homo:
  ‹Homo_Sep_Homo inject›
  unfolding Sep_Closed_def Homo_Sep_Homo_def
  apply (auto simp add: Sep_Homo_def)
  using mult_in_dom apply auto[1]
  using mult_in_dom apply auto[1]
  by (metis imageI inj.homo_mult)

end

lemma sep_inj_proj_id: ‹sep_inj_proj id id› by (standard; simp)

lemma sep_inj_proj_comp:
  ‹ sep_inj_proj f1 g1
⟹ sep_inj_proj f2 g2
⟹ sep_inj_proj (f2 o f1) (g1 o g2)›
  unfolding sep_inj_proj_def sep_inj_proj_axioms_def homo_one_def closed_homo_sep_def
  by (clarsimp, insert closed_homo_sep_disj.sep_disj_homo, blast)


locale sep_space_entry =
  sep_inj_proj inject' project'
  for name'   :: 'NAME
  and inject' :: ‹'T::sep_algebra ⇒ 'REP::sep_algebra›
  and project':: ‹'REP::sep_algebra ⇒ 'T::sep_algebra›
begin


abbreviation "name ≡ name'"
abbreviation "inject ≡ inject'"
abbreviation "project ≡ project'"

abbreviation "clean r ≡ r(name := 1)"
  ― ‹‹clean r› removes all resources of kind ‹K› from the compound resource ‹r›.
      ‹1› is the unit element of the separation algebra which represents empty resource or
      none specification.›

abbreviation "get r ≡ project (r name)"
  ― ‹‹get r› retrieves the model of resource kind ‹K› from the compound resource ‹r››

abbreviation "updt g r ≡ r(name := inject (g (get r)))"
  ― ‹‹updt g r› updates the model of resource kind ‹k› by using function ‹g››

abbreviation "updts g r ≡ {r(name := inject v) |v. v ∈ g (get r)}"

abbreviation "mk x ≡ 1(name := inject x)"
  ― ‹‹mk x› makes a compound resource that only has the resource modelled by ‹x› of kind ‹K››

subsubsection ‹Lemmas for Automation and Analysis›

lemma sep_disj_mk[iff]:
  ‹mk x ## mk y ⟷ x ## y›
  by force

lemma sep_disj_mk_name[simp]:
  ‹mk x ## r ⟹ inject x ## r name›
  by (metis fun_upd_same sep_disj_fun)

lemma sep_disj_get_name:
  ‹mk x ## r ⟶ x ## get r›
  by (metis prj.sep_disj_homo_semi proj_inj sep_disj_mk_name)

lemma get_homo_mult:
  ‹a ## b ⟹ get (a * b) = get a * get b›
  by (simp add: prj.homo_mult times_fun)

lemma mk_homo_one[iff]: ‹mk x = 1 ⟷ x = 1›
  by (metis fun_1upd1 fun_upd_eqD inj.homo_one proj_inj)

lemma mk_homo_mult: ‹a ## b ⟹ mk (a * b) = mk a * mk b›
  by (simp add: fun_1upd_homo inj.homo_mult)

lemma mk_inj[iff]: ‹mk a = mk b ⟷ a = b›
  unfolding fun_eq_iff by simp
(* 
lemmas split = fun_split_1[where ?k = name and ?'a = 'NAME and ?'b = 'REP]

lemma inject_wand_homo: ‹
  NO_MATCH (inject a'') a'
⟹ a' ## inject b
⟹ a' * inject b = inject c ⟷ (∃a. a' = inject a ∧ a * b = c ∧ a ## b)›
  ― ‹split the deep representation of the kind ‹K›.
      This lemma is useful in fictional separation especially view shifts.›
  using mult_in_dom by force

lemma sep_disj_clean[simp]:
  ‹clean r ## mk any›
  by simp *)

lemma times_fun_upd:
  ‹(mk x * R)(name := inject y) = (mk y * clean R)›
  unfolding times_fun_def fun_upd_def fun_eq_iff by simp

end

locale "resource_space" =
  fixes DOMAIN :: ‹'NAME ⇒ 'REP::sep_algebra sep_homo_set›
begin

definition SPACE :: ‹('NAME ⇒ 'REP) set›
  where ‹SPACE = {R. finite (dom1 R) ∧ (∀N. R N ∈⇩S⇩H DOMAIN N) }›

lemma SPACE_1[iff]:
  ‹1 ∈ SPACE›
  unfolding SPACE_def by simp

lemma SPACE_mult_homo:
  ‹A ## B ⟹ A * B ∈ SPACE ⟷ A ∈ SPACE ∧ B ∈ SPACE›
  unfolding SPACE_def
  by (simp add: times_fun sep_disj_fun_def dom1_sep_mult_disjoint; blast)

(* lemma
  ‹Sep_Closed {R. ∀N. R N ∈⇩S DOMAIN N }›
  unfolding Sep_Closed_def by (simp add: times_fun sep_disj_fun_def; blast) *)

end


locale resource_kind =
  "resource_space" DOMAIN
+ sep_space_entry ‹kind.name K› ‹kind.inject K› ‹kind.project K›
for DOMAIN :: ‹'NAME ⇒ 'REP::sep_algebra sep_homo_set›
and K :: "('NAME, 'REP::sep_algebra, 'T::sep_algebra) kind"
+ assumes raw_domain: "DOMAIN (kind.name K) = kind.inject K `⇩S⇩H kind.domain K"

begin

subsubsection ‹Methods and Sugars of a Resource Kind›

abbreviation "domain ≡ kind.domain K"

lemma in_DOMAIN[simp]:
  ‹rep ∈⇩S⇩H DOMAIN name ⟷ (∃x. rep = inject x ∧ x ∈⇩S⇩H domain)›
  by (simp add: inj_Sep_Homo raw_domain)

lemma 𝗋_valid_split:
  ‹res ∈ SPACE ⟷
  clean res ∈ SPACE ∧ (∃m. res name = inject m ∧ m ∈⇩S⇩H domain)›
  apply (subst fun_split_1[where ?k = name and ?'a = 'NAME and ?'b = 'REP];
         simp add: times_fun image_iff SPACE_def)
  using inj_Sep_Homo raw_domain by auto

lemma 𝗋_valid_split': ‹
  NO_MATCH (clean res') res
⟹ res ∈ SPACE ⟷ clean res ∈ SPACE ∧ (∃m. res name = inject m ∧ m ∈⇩S⇩H domain)›
  using 𝗋_valid_split .

lemma inj_prj_in_SPACE[simp]:
  ‹f ∈ SPACE ⟹ inject (project (f name)) = f name›
  by (metis 𝗋_valid_split proj_inj)

end

locale resource_kind' =
  resource_kind DOMAIN K
for DOMAIN :: ‹'NAME ⇒ 'REP::sep_algebra sep_homo_set›
and K :: "('NAME, 'REP::sep_algebra, 'T::sep_algebra) kind"
and DOM :: ‹'T::sep_algebra sep_homo_set›
+ assumes domain[simp]: "kind.domain K = DOM"

ML_file ‹resource_space.ML›


subsection ‹Fiction Space›

text ‹The section presents a modular implementation of fictional separation~\cite{FSL}, using
fictional interpretations given in~\cite{Algebras}.
Readers should read \cite{FSL,Algebras} first before beginning this section.

Akin to resource space, fiction space is a locale-based approach that combines fictions on
different models. Specifically, parameterized by resource type ‹'RES› (which can be typically
the deep representation ‹'NAME ⇒ 'REP› of a resource space discussed above),
a fiction space is a resource space ‹'FNAME ⇒ 'FREP› at fictional level, where every kind of
fictional resource ‹(i::'FNAME, inj⇩i :: 'T⇩i ⇒ 'FREP, prj⇩i :: 'FREP ⇒ 'T⇩i)›
is equipped with an interpretation ‹I⇩i :: 'T⇩i ⇒ 'RES set› that interprets fictional resources to
concrete resources. This fictional resource is named fiction simply.

Fiction space is therefore a collection of interpretations ‹{I⇩i}› from their own
fiction models ‹'T⇩i› to resources ‹'RES›.
The fiction space then converts this collection of fictions and interpretations to
a union fiction of type ‹'FNAME ⇒ 'FREP› and the interpretation from the fiction ‹'FNAME ⇒ 'FREP›
to resources ‹'RES›.

Recalling resource space, ‹'FNAME› is a type of names that identify each interpretation;
‹'FREP› is a representation type in which each fiction ‹'T⇩i› can be embedded, viz.,
every fiction ‹'T⇩i› for each ‹i› is injective to ‹'FREP›.
By the ‹prj⇩i› each interpretation ‹I⇩i› is convertible to representational interpretation
‹I'⇩i ≜ I⇩i ∘ prj⇩i› of type ‹'FREP ⇒ 'RES set›, which interprets the representation of fiction ‹'T⇩i›
to the concrete resources.
The union interpretation is then the finite product of all representational interpretation ‹I'⇩i›
\[ ‹INTERP ≜ λf. Πi. I'⇩i(f i)› \]
where lambda variable ‹f::'FNAME ⇒ 'FREP› denotes the fictional resource to be interpreted,
and ‹f i› gets the representation of fictional resource ‹i›.
›

locale fictional_space =
  resource_space DOMAIN
  for DOMAIN :: ‹'FNAME ⇒ 'FREP::sep_algebra sep_homo_set›
  and INTERPRET :: "'FNAME ⇒ ('FREP::sep_algebra,'RES::sep_algebra) unital_homo_interp"
    ― ‹\<^term>‹INTERPRET i› gives the interpretation of fiction kind ‹i›, i.e., ‹I⇩i› above.›
begin

definition "INTERP = ℱ_FP_homo INTERPRET"

end


locale fiction_kind =
  fictional_space DOMAIN INTERPRET
+ resource_kind DOMAIN FK
  for DOMAIN :: ‹'FNAME ⇒ 'FREP::sep_algebra sep_homo_set›
  and INTERPRET :: "'FNAME ⇒ ('FREP::sep_algebra,'RES::sep_algebra) unital_homo_interp"
  and FK :: "('FNAME,'FREP,'T::sep_algebra) kind"
+ fixes I :: "('RES, 'T) φ"
assumes interpret_reduct: "INTERPRET (kind.name FK) = Unital_Homo (I o kind.project FK)"
  and   univ_domain[simp]: "kind.domain FK = sep_homo_set UNIV"
begin

(*lemma 𝗋_valid_split:
  ‹res ∈ SPACE ⟷
  clean res ∈ SPACE ∧ (∃m. res name = inject m)›
  by (subst split; simp add: times_fun image_iff SPACE_def; blast)

lemma 𝗋_valid_split': ‹
  NO_MATCH (clean res') res
⟹ res ∈ SPACE ⟷ clean res ∈ SPACE ∧ (∃m. res name = inject m)›
  using 𝗋_valid_split . *)

  (* by (metis 𝗋_valid_split proj_inj) *)

lemma Fic_Space_m[simp]: "mk x ∈ SPACE"
  unfolding SPACE_def by simp

lemma interp_m[simp]: "homo_one I ⟹ INTERP (mk x) = I x"
  unfolding INTERP_def
  by (simp add: sep_disj_commute sep_mult_commute interpret_reduct prj.homo_one_axioms,
      metis homo_one.homo_one prj.homo_one_axioms proj_inj)

lemma sep_disj_get_name_eq[simp]:
  ‹r ∈ SPACE ⟹ x ## get r ⟷ mk x ## r›
  by (metis fun_sep_disj_1_fupdt(2) fun_upd_triv inj.sep_disj_homo_semi inj_prj_in_SPACE sep_disj_get_name)

lemma interp_split:
  " NO_MATCH (clean f') f
⟹ homo_one I
⟹ f ∈ SPACE ⟹
    INTERP f = I (project (f name)) * INTERP (clean f)
  ∧ I (project (f name)) ## INTERP (clean f) "
  unfolding INTERP_def SPACE_def
  by (simp_all add: interpret_reduct,
      smt (verit, del_insts) Diff_empty Diff_insert0 comp_def dom1_def homo_one.homo_one homo_one_comp interpret_reduct mem_Collect_eq mult_1_class.mult_1_left prj.homo_one_axioms prod.remove unital_homo_inverse)

lemma Fic_Space_mm[simp]: "mk x ## f ⟹ mk x * f ∈ SPACE ⟷ f ∈ SPACE"
  unfolding SPACE_def finite_dom1_mult1
  by (clarsimp,
      smt (verit, ccfv_threshold) Fic_Space_m SPACE_def SPACE_mult_homo finite_dom1_mult1 mem_Collect_eq)

end

hide_type (open) kind
hide_const (open) kind


end