# Theory Multirelations

section ‹Multirelations›
theory Multirelations
imports C_Algebras
begin
subsection ‹Basic Definitions›
text ‹We define a type synonym for multirelations.›
type_synonym 'a mrel = "('a * ('a set)) set"
no_notation s_prod (infixl "⋅" 80)
no_notation s_id ("1⇩_{σ}")
no_notation c_prod (infixl "∥" 80)
no_notation c_id ("1⇩_{π}")
text ‹Now we start with formalising the multirelational model. First
we define sequential composition and paraellel composition of multirelations, their units and
the universal multirelation as in Section 2 of the article.›
definition s_prod :: "'a mrel ⇒ 'a mrel ⇒ 'a mrel" (infixl "⋅" 70) where
"R ⋅ S = {(a,A). (∃B. (a,B) ∈ R ∧ (∃f. (∀b ∈ B. (b,f b) ∈ S) ∧ A = ⋃{f b |b. b ∈ B}))}"
definition s_id :: "'a mrel" ("1⇩_{σ}") where
"1⇩_{σ} ≡ ⋃a. {(a,{a})}"
definition p_prod :: "'a mrel ⇒ 'a mrel ⇒ 'a mrel" (infixl "∥" 70) where
"R ∥ S = {(a,A). (∃B C. A = B ∪ C ∧ (a,B) ∈ R ∧ (a,C) ∈ S)}"
definition p_id :: "'a mrel" ("1⇩_{π}") where
"1⇩_{π} ≡ ⋃a. {(a,{})}"
definition U :: "'a mrel" where
"U ≡ {(a,A) |a A. a ∈ UNIV ∧ A ⊆ UNIV}"
abbreviation "NC ≡ U - 1⇩_{π}"
text ‹We write NC where $\overline{1_\pi}$ is written in~\cite{FurusawaS15a}.›
text ‹Next we prove some basic set-theoretic properties.›
lemma s_prod_im: "R ⋅ S = {(a,A). (∃B. (a,B) ∈ R ∧ (∃f. (∀b ∈ B. (b,f b) ∈ S) ∧ A = ⋃((λx. f x) ` B)))}"
by (auto simp: s_prod_def)
lemma s_prod_iff: "(a,A) ∈ (R ⋅ S) ⟷ (∃B. (a,B) ∈ R ∧ (∃f. (∀b ∈ B. (b,f b) ∈ S) ∧ A = ⋃((λx. f x) ` B)))"
by (unfold s_prod_im, auto)
lemma s_id_iff: "(a,A) ∈ 1⇩_{σ} ⟷ A = {a}"
by (simp add: s_id_def)
lemma p_prod_iff: "(a,A) ∈ R ∥ S ⟷ (∃B C. A = B ∪ C ∧ (a,B) ∈ R ∧ (a,C) ∈ S)"
by (clarsimp simp add: p_prod_def)
named_theorems mr_simp
declare s_prod_im [mr_simp] p_prod_def [mr_simp] s_id_def [mr_simp] p_id_def [mr_simp] U_def [mr_simp]
subsection‹Multirelations and Proto-Dioids›
text ‹We can now show that multirelations form proto-trioids.
This is Proposition 5.1, and it subsumes Proposition 4.1,›