Theory Multirelations

(*
Title: Binary Multirelations
Author: Hitoshi Furusawa, Georg Struth
Maintainer: <g.struth at sheffield.ac.uk>
*)

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,›

interpretation mrel_proto_trioid: proto_trioid "1⇩σ" "(⋅)" "1⇩π" "(∥)" "(∪)" "(⊆)" "(⊂)" "{}"
proof 
  show "⋀x. 1⇩σ ⋅ x = x"
    by (auto simp: mr_simp)
  show "⋀x. x ⋅ 1⇩σ = x"
    by (auto simp add: mr_simp) (metis UN_singleton)
  show "⋀x. 1⇩π ∥ x = x"
    by (simp add: mr_simp)
  show "⋀x y z. x ∥ y ∥ z = x ∥ (y ∥ z)"
    apply (rule antisym)
    apply (clarsimp simp: mr_simp Un_assoc, metis) 
    by (clarsimp simp: mr_simp, metis (no_types) Un_assoc)
  show "⋀x y. x ∥ y = y ∥ x"
    by  (auto simp: mr_simp)
  show "⋀x y. (x ⊆ y) = (x ∪ y = y)"
    by blast
  show "⋀x y. (x ⊂ y) = (x ⊆ y ∧ x ≠ y)"
    by (simp add: psubset_eq)
  show "⋀x y z. x ∪ y ∪ z = x ∪ (y ∪ z)"
    by (simp add: Un_assoc)
  show "⋀x y. x ∪ y = y ∪ x"
    by blast
  show "⋀x. x ∪ x = x"
    by auto
  show "⋀x. {} ∪ x = x"
    by blast
  show "⋀x y z. (x ∪ y) ⋅ z = x ⋅ z ∪ y ⋅ z"
    by (auto simp: mr_simp)
  show "⋀x y z. x ⋅ y ∪ x ⋅ z ⊆ x ⋅ (y ∪ z)"
    by (auto simp: mr_simp)
  show "⋀x. {} ⋅ x = {}"
    by (auto simp: mr_simp)
  show "⋀x y z. x ∥ (y ∪ z) = x ∥ y ∪ x ∥ z"
    by (auto simp: mr_simp)
  show "⋀x. x ∥ {} = {}"
    by (simp add: mr_simp)
qed

subsection ‹Simple Properties›

text‹This covers all the identities in the display before Lemma 2.1  except the two following ones.›

lemma s_prod_assoc1: "(R ⋅ S ) ⋅ T ⊆ R ⋅ (S ⋅ T)"
  by (clarsimp simp: mr_simp, metis)

lemma seq_conc_subdistr: "(R ∥ S) ⋅ T ⊆ (R ⋅ T) ∥ (S ⋅ T)"
  by (clarsimp simp: mr_simp UnI1 UnI2, blast)

text ‹Next we provide some counterexamples. These do not feature in~\<^cite>‹"FurusawaS15a"›.›

lemma  "R ⋅ {} = {}"
  nitpick 
  oops

lemma "R ⋅ (S ∪ T) = R ⋅ S ∪ R ⋅ T"
  apply (auto simp: s_prod_im)
  nitpick
  oops

lemma "R ⋅ (S ⋅ T) ⊆ (R ⋅ S) ⋅ T"
  apply (auto simp: s_prod_im)
  nitpick
  oops

lemma "(R ∥ R) ⋅ T = (R ⋅ T) ∥ (R ⋅ T)"
  quickcheck 
  oops

text ‹Next we prove the distributivity and associativity laws for sequential subidentities 
mentioned before Lemma 2.1›   

lemma subid_aux2: 
assumes "R ⊆ 1⇩σ"and "(a,A) ∈ R"
shows "A = {a}"
  using assms by (auto simp: mr_simp)

lemma s_prod_test_aux1: 
assumes "S ⊆ 1⇩σ"
and  "(a,A) ∈ R ⋅ S"
shows "((a,A) ∈ R ∧ (∀a ∈ A. (a,{a}) ∈ S))" 
  using assms apply (clarsimp simp: s_prod_im)
  by (metis assms(2) mrel_proto_trioid.s_prod_idr mrel_proto_trioid.s_prod_isol singletonD subid_aux2 subset_eq)

lemma s_prod_test_aux2: 
assumes "(a,A) ∈ R"
and "∀a ∈ A. (a,{a}) ∈ S"
shows "(a,A) ∈ R ⋅ S"
  using assms by (auto simp: mr_simp, fastforce)

lemma s_prod_test: 
assumes "P ⊆ 1⇩σ"
shows "(a,A) ∈ R ⋅ P ⟷ (a,A) ∈ R ∧ (∀a ∈ A. (a,{a}) ∈ P)"
  by (meson assms s_prod_test_aux1 s_prod_test_aux2) 

lemma test_s_prod_aux1: 
assumes "P ⊆  1⇩σ" 
and "(a,A) ∈ P ⋅ R"
shows "(a,{a}) ∈ P ∧ (a,A) ∈ R" 
  by (metis assms mrel_proto_trioid.s_prod_idl s_id_iff s_prod_iff subid_aux2)
  
lemma test_s_prod_aux2: 
assumes "(a,A) ∈ R" 
and "(a,{a}) ∈ P"
shows "(a,A) ∈ P ⋅ R"
  using assms s_prod_iff by fastforce

lemma test_s_prod: 
assumes "P ⊆ 1⇩σ"
shows "(a,A) ∈ P ⋅ R ⟷ (a,{a}) ∈ P ∧ (a,A) ∈ R"
  by (meson assms test_s_prod_aux1 test_s_prod_aux2)

lemma test_assoc1: 
assumes "P ⊆ 1⇩σ"
shows "(R ⋅ P) ⋅ S = R ⋅ (P ⋅ S)"
proof (rule antisym)
  show  "(R ⋅ P) ⋅ S ⊆ R ⋅ (P ⋅ S)"
    by (metis s_prod_assoc1)
next
  show "R ⋅ (P ⋅ S) ⊆ (R ⋅ P) ⋅ S" using assms
  proof clarify
    fix a A
    assume "(a,A) ∈ R ⋅ (P ⋅ S)"
    hence "∃B.(a,B) ∈ R ∧ (∃f. (∀b ∈ B. (b,f b) ∈ P ⋅ S) ∧ A = ⋃((λx. f x) ` B))" 
      by (clarsimp simp: mr_simp)
    hence "∃B.(a,B) ∈ R ∧ (∃f. (∀b ∈ B. (b,{b}) ∈ P ∧ (b,f b) ∈ S) ∧ A = ⋃((λx. f x) ` B))" 
      by (metis assms test_s_prod)
    hence "∃B.(a,B) ∈ R ∧ (∀b ∈ B. (b,{b}) ∈ P) ∧ (∃f. (∀b ∈ B. (b,f b) ∈ S) ∧ A = ⋃((λx. f x) ` B))"  
      by auto
    hence "∃B. (a,B) ∈ R ⋅ P ∧ (∃f. (∀b ∈ B. (b,f b) ∈ S) ∧ A = ⋃((λx. f x) ` B))"
      by (metis assms s_prod_test)
    thus "(a,A) ∈ (R ⋅ P) ⋅ S"
      by (clarsimp simp: mr_simp)
  qed
qed

lemma test_assoc2: 
assumes "P ⊆ 1⇩σ"
shows "(P ⋅ R) ⋅ S = P ⋅ (R ⋅ S)"
proof (rule antisym)
  show "(P ⋅ R) ⋅ S ⊆  P ⋅ (R ⋅ S)"
    by (metis s_prod_assoc1)
  show "P ⋅ (R ⋅ S) ⊆ (P ⋅ R) ⋅ S" using assms
  proof clarify
    fix a A
    assume "(a,A) ∈ P ⋅ (R ⋅ S)"
    hence "(a,{a}) ∈ P ∧ (a,A) ∈ R ⋅ S"
      by (metis assms test_s_prod)
    hence "(a,{a}) ∈ P ∧ (∃B. (a,B) ∈ R ∧ (∃f. (∀b ∈ B. (b,f b) ∈ S) ∧ A = ⋃((λx. f x) ` B)))" 
      by (clarsimp simp: mr_simp)
    hence "∃B.(a,{a}) ∈ P ∧ (a,B) ∈ R ∧ (∃f. (∀b ∈ B. (b,f b) ∈ S) ∧ A = ⋃((λx. f x) ` B))" 
      by (clarsimp simp: mr_simp)
    hence "∃B. (a,B) ∈ P ⋅ R ∧ (∃f. (∀b ∈ B. (b,f b) ∈ S) ∧ A = ⋃((λx. f x) ` B))"
      by (metis assms test_s_prod)
    thus "(a,A) ∈ (P ⋅ R) ⋅ S"
      by (clarsimp simp: mr_simp)
  qed
qed

lemma test_assoc3: 
assumes "P ⊆ 1⇩σ"
shows "(R ⋅ S) ⋅ P = R ⋅ (S ⋅ P)"
proof (rule antisym)
  show "(R ⋅ S) ⋅ P ⊆ R ⋅ (S ⋅ P)"
    by (metis s_prod_assoc1)
  show "R ⋅ (S ⋅ P) ⊆ (R ⋅ S) ⋅ P" using assms
    proof clarify
    fix a A
    assume hyp1: "(a, A) ∈ R ⋅ (S ⋅ P)"
    hence "∃B. (a,B) ∈ R ∧ (∃f. (∀b∈B. (b,f b) ∈ S ⋅ P) ∧ A = ⋃((λx. f x) ` B))"
      by (simp add: s_prod_test s_prod_im)
    hence "∃B. (a,B) ∈ R ∧ (∃f. (∀b∈B. (b,f b) ∈ S ∧ (∀a∈f b. (a,{a}) ∈ P)) ∧ A = ⋃((λx. f x) ` B))"
      by (simp add: s_prod_test assms)
    hence "∃B. (a,B) ∈ R ∧ (∃f. (∀b∈B. (b,f b) ∈ S) ∧ (∀a∈⋃((λx. f x) ` B). (a,{a}) ∈ P) ∧ A = ⋃((λx. f x) ` B))"
      by auto
    hence "∃B. (a,B) ∈ R ∧ (∃f. (∀b∈B. (b,f b) ∈ S) ∧ (∀a∈A. (a,{a}) ∈ P) ∧ A = ⋃((λx. f x) ` B))"
      by auto blast
    hence "(a,A) ∈ R ⋅ S ∧ (∀a∈A. (a,{a}) ∈ P)"
      by (auto simp: mr_simp)
    thus "(a,A) ∈ (R ⋅ S) ⋅ P"
      by (simp add: s_prod_test assms)
  qed
qed

lemma s_distl_test: 
assumes "R ⊆ 1⇩σ"
shows "R ⋅ (S ∪ T) = R ⋅ S ∪ R ⋅ T" 
  apply (clarsimp simp: mr_simp) using assms subid_aux2 by fastforce 

text ‹Next we verify Lemma 2.1.›

lemma subid_par_idem: 
assumes "R ⊆ 1⇩σ"
shows "R ∥ R = R"
  by (rule set_eqI, clarsimp simp: mr_simp, metis Un_absorb assms subid_aux2) 

lemma term_par_idem: 
assumes "R ⊆ 1⇩π" 
shows "R ∥ R = R"
  using assms by (auto simp: mr_simp)

lemma U_par_idem: "U ∥ U = U"
  by (auto simp: mr_simp)

lemma nc_par_idem: "NC ∥ NC = NC"
  by (auto simp: mr_simp)

text ‹Next we prove the properties of Lemma 2.2 and 3.2. First we prepare to show that multirelations form c-lattices.›

text ‹We define the domain operation on multirelations and verify the explicit definition from Section 3.›

definition d :: "'a mrel ⇒ 'a mrel" where
  "d R ≡ {(a,{a}) |a. ∃B. (a,B) ∈ R}"

named_theorems mrd_simp
declare mr_simp [mrd_simp] d_def [mrd_simp]

lemma d_def_expl: "d R = (R ⋅ 1⇩π) ∥ 1⇩σ"
  apply (simp add: mrd_simp) using set_eqI by force

interpretation mrel_pbdl_monoid: pbdl_monoid "1⇩σ" "(⋅)" "1⇩π" "(∥)" "(∪)" "(⊆)" "(⊂)" "{}" "U" "(∩)"
  by (unfold_locales, auto simp: mrd_simp)

text ‹Here come the properties of Lemma 2.2.›

lemma c1: "(R ⋅ 1⇩π) ∥ R = R"
  apply (rule set_eqI) 
  apply (clarsimp simp: mr_simp)
  by (metis (no_types, lifting) SUP_bot SUP_bot_conv(2) sup_bot.left_neutral) 

lemma t_aux: "T ∥ T ⊆ T ⟹ (∀a B C. (a,B) ∈ T ∧ (a,C) ∈ T ⟹ (a,B ∪ C) ∈ T)"
  by (clarsimp simp: mr_simp)

lemma cl4:
assumes "T ∥ T ⊆ T"
shows "(R ⋅ T) ∥ (S ⋅ T) ⊆ (R ∥ S) ⋅ T" 
proof clarify
fix a A   
  assume  "(a,A) ∈ (R ⋅ T) ∥ (S ⋅ T)"
  hence "∃B C. A = B ∪ C ∧ (∃D. (a,D) ∈ R ∧ (∃f. (∀d ∈ D. (d,f d) ∈ T) ∧ B = ⋃ ((λx. f x) ` D))) ∧ (∃E. (a,E) ∈ S ∧ (∃g. (∀e ∈ E. (e,g e) ∈ T) ∧ C = ⋃ ((λx. g x)` E)))"
    by (simp add: mr_simp)
  hence "∃D E. (a,D ∪ E) ∈ R ∥ S ∧ (∃f g. (∀d ∈ D. (d,f d) ∈ T) ∧ (∀e ∈ E. (e,g e) ∈ T) ∧ A = (⋃ ((λx. f x) ` D)) ∪ (⋃ ((λx. g x)` E)))"
    by (auto simp: mr_simp)
  hence "∃D E. (a,D ∪ E) ∈ R ∥ S ∧ (∃f g. (∀d ∈ D-E. (d,f d) ∈ T) ∧ (∀e ∈ E-D. (e,g e) ∈ T) ∧ (∀x ∈ D ∩ E. (x,f x) ∈ T ∧ (x,g x) ∈ T) ∧ A = (⋃ ((λx. f x) ` (D-E))) ∪ (⋃ ((λx. g x) ` (E-D)) ∪ (⋃ ((λy. f y ∪ g y) ` (D ∩ E)))))"
    by auto blast
  hence "∃D E. (a,D ∪ E) ∈ R ∥ S ∧ (∃f g. (∀d ∈ D-E. (d,f d) ∈ T) ∧ (∀e ∈ E-D. (e,g e) ∈ T) ∧ (∀x ∈ D ∩ E. (x,f x ∪ g x) ∈ T) ∧ A = (⋃ ((λx. f x) ` (D-E))) ∪ (⋃ ((λx. g x) ` (E-D)) ∪ (⋃ ((λy. f y ∪ g y) ` (D ∩ E)))))"
    apply clarify
    apply (rule_tac x = D in exI)
    apply (rule_tac x = E in exI)
    apply clarify
    apply (rule_tac x = f in exI)
    apply (rule_tac x = g in exI)
    using assms by (auto simp: p_prod_def p_prod_iff, blast)
  hence "∃D E. (a,D ∪ E) ∈ R ∥ S ∧ (∃h. (∀d ∈ D-E. (d,h d) ∈ T) ∧ (∀e ∈ E-D. (e, h e) ∈ T) ∧ (∀x ∈ D ∩ E. (x, h x) ∈ T) ∧ A = (⋃ ((λx. h x) ` (D-E))) ∪ (⋃ ((λx. h x) ` (E-D)) ∪ (⋃ ((λy. h y) ` (D ∩ E)))))"
    apply clarify
    apply (rule_tac x = D in exI)
    apply (rule_tac x = E in exI)
    apply clarify
    apply (rule_tac x = "λx. if x ∈ (D - E) then f x else (if x ∈ D ∩ E then (f x ∪ g x) else g x)" in exI)
    by auto
  hence " (∃B. (a,B) ∈ R ∥ S ∧ (∃h. (∀b∈B. (b,h b) ∈ T) ∧ A = ⋃((λx. h x) ` B)))"
    by auto blast
  thus "(a,A) ∈ (R ∥ S) ⋅ T"
    by (simp add: mr_simp)
qed

lemma cl3: "R ⋅ (S ∥ T) ⊆ (R ⋅ S) ∥ (R ⋅ T)"
proof clarify
fix a A
assume "(a,A) ∈ R ⋅ (S ∥ T)"
  hence "∃B. (a,B) ∈ R ∧ (∃f. (∀b ∈ B. ∃C D. f b = C ∪ D ∧ (b,C) ∈ S ∧ (b,D) ∈ T) ∧ A = ⋃((λx. f x) ` B))"
    by (clarsimp simp: mr_simp)
  hence "∃B. (a,B) ∈ R ∧ (∃f g h. (∀b ∈ B. f b = g b ∪ h b ∧ (b,g b) ∈ S ∧ (b,h b) ∈ T) ∧ A = ⋃((λx. f x) ` B))"
    by (clarsimp simp: bchoice, metis)
  hence "∃B. (a,B) ∈ R ∧ (∃g h. (∀b ∈ B. (b,g b) ∈ S ∧ (b,h b) ∈ T) ∧ A = (⋃ ((λx. g x) ` B)) ∪ (⋃ ((λx. h x) ` B)))"
    by  blast
  hence "∃C D. (∃B. (a,B) ∈ R ∧ (∃g. (∀b ∈ B. (b,g b) ∈ S) ∧  C = ⋃ ((λx. g x) ` B))) ∧ (∃B. (a,B) ∈ R ∧ (∃h. (∀b ∈ B. (b,h b) ∈ T) ∧  D = ⋃ ((λx. h x)` B))) ∧ A = C ∪ D"
    by blast
  thus "(a,A) ∈ (R ⋅ S) ∥ (R ⋅ T)"
    by (auto simp: mr_simp)
qed

lemma cl5: "(R ⋅ S) ⋅ (T ⋅ {}) = R ⋅ (S ⋅ (T ⋅ {}))"
  proof (rule antisym)
  show "(R ⋅ S) ⋅ (T ⋅ {}) ⊆ R ⋅ (S ⋅ (T ⋅ {}))"
    by (metis s_prod_assoc1)
  show " R ⋅ (S ⋅ (T ⋅ {})) ⊆ (R ⋅ S) ⋅ (T ⋅ {})"
  proof clarify
  fix a A
  assume "(a,A) ∈  R ⋅ (S ⋅ (T ⋅ {}))"
    hence "∃B. (a,B) ∈ R ∧ (∃f. (∀b ∈ B. (∃ C. (b,C) ∈ S ∧ (∃g. (∀x ∈ C. (x,g x) ∈ T ⋅ {}) ∧ f b = ⋃((λx. g x) ` C)))) ∧ A = ⋃((λx. f x) ` B))"
      by (clarsimp simp: mr_simp)
    hence "∃B. (a,B) ∈ R ∧ (∃f. (∀b ∈ B. (∃ C. (b,C) ∈ S ∧ (∀x ∈ C. (x,{}) ∈ T ⋅ {}) ∧ f b = {})) ∧ A = ⋃((λx. f x) ` B))"
      by (clarsimp simp: mr_simp) fastforce
    hence "∃B. (a,B) ∈ R ∧ (∀b ∈ B. (∃ C. (b,C) ∈ S ∧ (∀x ∈ C. (x,{}) ∈ T ⋅ {}))) ∧ A = {}"
      by (metis (erased, opaque_lifting) SUP_bot_conv(2))
    hence "∃B. (a,B) ∈ R ∧ (∃f. (∀b ∈ B. (b,f b) ∈ S ∧ (∀x ∈ f b. (x,{}) ∈ T ⋅ {}))) ∧ A = {}" 
      by metis
    hence "∃B. (a,B) ∈ R ∧ (∃f. (∀b ∈ B. (b,f b) ∈ S) ∧ (∀x ∈ ⋃((λx. f x) ` B). (x,{}) ∈ T ⋅ {})) ∧ A = {}"
      by (metis UN_E) 
    hence "∃C B. (a,B) ∈ R ∧ (∃f. (∀b ∈ B. (b, f b) ∈ S) ∧ C =  ⋃((λx. f x) ` B) ∧ (∀x ∈ C. (x,{}) ∈ T ⋅ {})) ∧ A = {}"
      by metis
    hence "∃C. (a,C) ∈ R ⋅ S ∧ (∀x ∈ C. (x,{}) ∈ T ⋅ {}) ∧ A = {}"
      by (auto simp: mr_simp)
    thus "(a,A) ∈ (R ⋅ S) ⋅ (T ⋅ {})"
      by (clarsimp simp: mr_simp) blast
  qed
qed

text ‹We continue verifying other c-lattice axioms›

lemma cl8_var: "d R ⋅ S = (R ⋅ 1⇩π) ∥ S"
  apply (rule set_eqI)
  apply (clarsimp simp: mrd_simp)
  apply standard
  apply (metis SUP_bot sup.commute sup_bot.right_neutral)
  by auto

lemma cl9_var: "d (R ∩ 1⇩σ) = R ∩ 1⇩σ"
  by (auto simp: mrd_simp)

lemma cl10_var: "d (R - 1⇩π) = 1⇩σ ∩ ((R - 1⇩π) ⋅ NC)"
  apply (rule set_eqI)
  apply (clarsimp simp: d_def p_id_def s_id_def U_def s_prod_im)
  by (metis UN_constant insert_not_empty)

subsection ‹Multirelations and C-Lattices›

text ‹Next we show that multirelations form c-lattices (Proposition 7.3) and prove further facts in this setting.›

interpretation mrel_c_lattice: c_lattice "1⇩σ" "(⋅)" "1⇩π" "(∥)" "(∪)" "(⊆)" "(⊂)" "{}" "U" "(∩)" "NC"
proof
  fix x y z :: "('b × 'b set) set"
  show "x ⋅ 1⇩π ∪ x ⋅ NC = x ⋅ U"
    apply (rule set_eqI) 
    apply (clarsimp simp:  mr_simp)
    using UN_constant all_not_in_conv by metis
  show "1⇩π ∩ (x ∪ NC) = x ⋅ {}"
    by (auto simp: mr_simp)
  show "x ⋅ (y ∥ z) ⊆ x ⋅ y ∥ (x ⋅ z)"
    by (rule cl3)
  show "z ∥ z ⊆ z ⟹ x ∥ y ⋅ z = x ⋅ z ∥ (y ⋅ z)"
    by (metis cl4 seq_conc_subdistr subset_antisym)
  show "x ⋅ (y ⋅ (z ⋅ {})) = x ⋅ y ⋅ (z ⋅ {})"
    by (metis cl5)
  show "x ⋅ {} ⋅ z = x ⋅ {}"
    by (clarsimp simp: mr_simp)
  show "1⇩σ ∥ 1⇩σ = 1⇩σ"
    by (auto simp: mr_simp)
  show "x ⋅ 1⇩π ∥ 1⇩σ ⋅ y = x ⋅ 1⇩π ∥ y"
    by (metis cl8_var d_def_expl)
  show "x ∩ 1⇩σ ⋅ 1⇩π ∥ 1⇩σ = x ∩ 1⇩σ"
    by (auto simp: mr_simp)
  show "x ∩ NC ⋅ 1⇩π ∥ 1⇩σ = 1⇩σ ∩ (x ∩ NC ⋅ NC)"
    by (metis Int_Diff cl10_var d_def_expl)
  show "x ∩ NC ⋅ 1⇩π ∥ NC = x ∩ NC ⋅ NC"
    apply (rule set_eqI)
    apply (clarsimp simp: d_def U_def p_id_def p_prod_def s_prod_im)
    apply standard
    apply (metis (no_types, lifting) UN_extend_simps(2) Un_empty)
  proof -
    fix a :: 'b and b :: "'b set"
    assume a1: "∃B. (a, B) ∈ x ∧ B ≠ {} ∧ (∃f. (∀b∈B. f b ≠ {}) ∧ b = (⋃x∈B. f x))"
    { fix bb :: "'b set ⇒ 'b set ⇒ 'b set ⇒ ('b ⇒ 'b set) ⇒ 'b"
      obtain BB :: "'b set" and BBa :: "'b ⇒ 'b set" where
        ff1: "(a, BB) ∈ x ∧ {} ≠ BB ∧ (∀b. b ∉ BB ∨ {} ≠ BBa b) ∧ ⋃(BBa ` BB) = b"
        by (metis (full_types) a1)
      hence "∀B. (⋃b∈BB. (B::'b set)) = B"
        by force
      hence "∃B Ba. B ∪ Ba = b ∧ (∃Bb. (a, Bb) ∈ x ∧ {} ≠ Bb ∧ (∃f. (bb B Ba Bb f ∉ Bb ∨ {} = f (bb B Ba Bb f)) ∧ ⋃(f ` Bb) = B)) ∧ {} ≠ Ba"
        by (metis ff1 SUP_bot_conv(2) sup_bot.left_neutral) }
    thus "∃B Ba. b = B ∪ Ba ∧ (∃Ba. (a, Ba) ∈ x ∧ Ba ≠ {} ∧ (∃f. (∀b∈Ba. f b = {}) ∧ B = (⋃b∈Ba. f b))) ∧ Ba ≠ {}"
      by metis
  qed
qed

text ‹The following facts from Lemma 2.2 remain to be shown.›

lemma p_id_assoc1: "(1⇩π ⋅ R) ⋅ S = 1⇩π ⋅ (R ⋅ S)"
  by (clarsimp simp: mr_simp)

lemma p_id_assoc2: "(R ⋅ 1⇩π) ⋅ T = R ⋅ (1⇩π ⋅ T)"
  by (auto simp add: mr_simp cong del: SUP_cong_simp, blast+)

lemma seq_conc_subdistrl: 
assumes "P ⊆ 1⇩σ"
shows "P ⋅ (S ∥ T) = (P ⋅ S) ∥ (P ⋅ T)"
  by (metis assms mrel_c_lattice.d_inter_r mrel_c_lattice.d_s_subid)

lemma test_s_prod_is_meet [simp]: 
assumes "R ⊆ 1⇩σ" 
and "S ⊆ 1⇩σ"
shows "R ⋅ S = R ∩ S"
  using assms by (auto simp: mr_simp, force+)

lemma test_p_prod_is_meet: 
assumes "R ⊆ 1⇩σ"
and "S ⊆ 1⇩σ"
shows "R ∥ S = R ∩ S"
  apply standard
  using assms
  apply (auto simp: mr_simp, force+)
  done

lemma test_multipliciativer:
assumes "R ⊆ 1⇩σ"
and "S ⊆ 1⇩σ"
shows "(R ∩ S) ⋅ T = (R ⋅ T) ∩ (S ⋅ T)"
  using assms by (clarsimp simp: set_eqI mr_simp subid_aux2, force)

text ‹Next we verify the remaining fact from Lemma 2.2; in fact it follows from the corresponding theorem of c-lattices.›

lemma c6: "R ⋅ 1⇩π ⊆ 1⇩π"
 by (clarsimp simp: mr_simp)

text ‹Next we verify Lemma 3.1.›

lemma p_id_st: "R ⋅ 1⇩π = {(a,{}) |a.  ∃B. (a,B) ∈ R}"
  by (auto simp: mr_simp)
 
lemma p_id_zero: "R ∩ 1⇩π = R ⋅ {}"
  by (auto simp: mr_simp)

lemma p_id_zero_st: "R ∩ 1⇩π = {(a,{}) |a. (a,{}) ∈ R}"
  by (auto simp: mr_simp)

lemma s_id_st: "R ∩ 1⇩σ = {(a,{a}) |a. (a,{a}) ∈ R}"
  by (auto simp: mr_simp)

lemma U_seq_st: "(a,A) ∈ R ⋅ U ⟷ (A = {} ∧ (a,{}) ∈ R) ∨ (∃B. B ≠ {} ∧ (a,B) ∈ R)"
  by (clarsimp simp: s_prod_im U_def, metis SUP_constant SUP_empty) 

lemma U_par_st: "(a,A) ∈ R ∥ U ⟷ (∃B. B ⊆ A ∧ (a,B) ∈ R)"
  by (auto simp: mr_simp)

text ‹Next we verify the relationships after Lemma 3.1.›

lemma s_subid_iff1: "R ⊆ 1⇩σ ⟷ R ∩ 1⇩σ = R"
  by blast

lemma s_subid_iff2: "R ⊆ 1⇩σ ⟷ d R = R"
  by (auto simp: mrd_simp)

lemma p_subid_iff: "R ⊆ 1⇩π ⟷ R ⋅ 1⇩π = R"
  by (simp add: mrel_c_lattice.term_p_subid)

lemma vec_iff1: 
assumes "∀a. (∃A. (a,A) ∈ R) ⟶ (∀A. (a,A) ∈ R)"
shows "(R ⋅ 1⇩π) ∥ U = R"
  using assms by (auto simp: mr_simp)

lemma vec_iff2: 
assumes "(R ⋅ 1⇩π) ∥ U = R"
shows "(∀a. (∃A. (a,A) ∈ R) ⟶ (∀A. (a,A) ∈ R))"
  using assms apply (clarsimp simp: mr_simp)
  proof -
    fix a :: 'a and A :: "'a set" and Aa :: "'a set"
    assume a1: "(a, A) ∈ R"
    obtain AA :: "('a × 'a set) set ⇒ 'a set ⇒ 'a ⇒ 'a set" where
    "∀x0 x1 x2. (∃v3⊆x1. (x2, v3) ∈ x0) = (AA x0 x1 x2 ⊆ x1 ∧ (x2, AA x0 x1 x2) ∈ x0)"
      by moura
    hence f2: "AA (R ⋅ 1⇩π) A a ⊆ A ∧ (a, AA (R ⋅ 1⇩π) A a) ∈ R ⋅ 1⇩π"
      by (metis a1 U_par_st assms)
    hence "∃aa. (a, AA (R ⋅ 1⇩π) A a) = (aa, {}) ∧ (∃A. (aa, A) ∈ R)"
      by (simp add: p_id_st)
    hence "AA (R ⋅ 1⇩π) A a ⊆ Aa"
      by blast
   thus "(a, Aa) ∈ R"
      using f2 by (metis (no_types) U_par_st assms)
qed

lemma vec_iff: "(∀a. (∃A. (a,A) ∈ R) ⟶ (∀A. (a,A) ∈ R)) ⟷ (R ⋅ 1⇩π) ∥ U = R"
  by (metis vec_iff1 vec_iff2)

lemma ucl_iff: "(∀a A B. (a,A) ∈ R ∧ A ⊆ B ⟶ (a,B) ∈ R) ⟷ R ∥ U = R" 
  by (clarsimp simp: mr_simp, blast)

lemma nt_iff: "R ⊆ NC ⟷ R ∩ NC = R"
  by blast

text‹Next we provide a counterexample for the final paragraph of Section 3.›

lemma "1⇩σ ∩ R ⋅ U = R"
  nitpick
  oops

text‹Next we present a counterexample for vectors mentioned before Lemma 9.3.›

lemma "d (d R ⋅ U) ⋅ (d S ⋅ U) ⋅ U = (d R ⋅ U) ⋅ (d S ⋅ U)"
  nitpick
  oops

text‹Next we prove Tarski' rule (Lemma 9.3).›

lemma tarski_aux: 
assumes "R - 1⇩π ≠ {}"
and "(a,A) ∈  NC"
shows "(a,A) ∈ NC ⋅ ((R - 1⇩π) ⋅ NC)"
proof -
  have "(∃B. B ≠ {} ∧ (∀x ∈ B. (x,{x}) ∈ d (R - 1⇩π)))" 
    using assms(1) by (auto simp: mrd_simp)
  hence "(∃B. B ≠ {} ∧ (∀x ∈ B. (x,{x}) ∈ d (R - 1⇩π))) ∧ A ≠ {}" 
    using assms(2) by (clarsimp simp: mr_simp)
  hence "(∃B. B ≠ {} ∧ (∃f. (∀x ∈ B. (x,{x}) ∈ d (R - 1⇩π) ∧ f x ≠ {}) ∧ A = ⋃ ((λx. (f x)) ` B)))"
    by (metis UN_constant)
  hence "(a,A) ∈ NC ⋅ (d (R - 1⇩π) ⋅ NC)"
    by (clarsimp simp: mrd_simp) metis
  thus ?thesis
   by (clarsimp simp: mrd_simp, metis UN_constant)
qed

lemma tarski: 
assumes "R - 1⇩π ≠ {}"
shows "NC ⋅ ((R - 1⇩π) ⋅ NC) = NC"
  by standard (simp add: U_def p_id_def s_prod_im, force, metis assms tarski_aux subrelI)

text ‹Next we verify the assumptions of Proposition 9.8.›

lemma d_assoc1: "d R ⋅ (S ⋅ T) = (d R ⋅ S) ⋅ T"
  by (metis d_def_expl mrel_c_lattice.d_def mrel_c_lattice.d_sub_id_ax test_assoc2)

lemma d_meet_distr_var: "(d R ∩ d S) ⋅ T = (d R ⋅ T) ∩ (d S ⋅ T)"
  by (auto simp: mrd_simp)

text ‹Lemma 10.5.›

lemma "((R ∩ 1⇩σ) ⋅ (S ∩ 1⇩σ)) ⋅ 1⇩π = ((R ∩ 1⇩σ) ⋅ 1⇩π) ⋅ ((S ∩ 1⇩σ) ⋅ 1⇩π)" 
  nitpick
  oops

lemma "d ((R ⋅ 1⇩π) ⋅ (S ⋅ 1⇩π)) = d (R ⋅ 1⇩π) ⋅ d (S ⋅ 1⇩π)"
  nitpick
  oops

lemma "((R ∩ 1⇩σ) ⋅ (S ∩ 1⇩σ)) ⋅ U = ((R ∩ 1⇩σ) ⋅ U) ⋅ ((S ∩ 1⇩σ) ⋅ U)" 
  nitpick
  oops

lemma "d (((R ⋅ 1⇩π) ∥ U) ⋅ ((S ⋅ 1⇩π) ∥ U)) = d ((R ⋅ 1⇩π) ∥ U) ⋅ d ((S ⋅ 1⇩π) ∥ U)"
  nitpick
  oops

lemma "((R ⋅ 1⇩π) ⋅ (S ⋅ 1⇩π)) ∥ U = ((R ⋅ 1⇩π) ∥ U) ⋅ ((S ⋅ 1⇩π) ∥ U)"
  nitpick
  oops

lemma "(((R - 1⇩π) ∩ 1⇩σ) ⋅ ((S - 1⇩π) ∩ 1⇩σ)) ⋅ 1⇩π = (((R - 1⇩π) ∩ 1⇩σ) ⋅ 1⇩π) ⋅ (((S - 1⇩π) ∩ 1⇩σ) ⋅ 1⇩π)" 
  nitpick
  oops

lemma "d (((R - 1⇩π) ⋅ 1⇩π) ⋅ ((S - 1⇩π) ⋅ 1⇩π)) = d ((R - 1⇩π) ⋅ 1⇩π) ⋅ d ((S - 1⇩π) ⋅ 1⇩π)"
  nitpick
  oops

lemma "(((R - 1⇩π) ∩ 1⇩σ) ⋅ ((S - 1⇩π) ∩ 1⇩σ)) ⋅ NC = (((R - 1⇩π) ∩ 1⇩σ) ⋅ NC) ⋅ (((S - 1⇩π) ∩ 1⇩σ) ⋅ NC)" 
  apply (auto simp: U_def p_id_def s_id_def s_prod_im)
  defer
  nitpick
  oops

lemma "d ((((R - 1⇩π) ⋅ 1⇩π) ∥ NC) ⋅ (((S - 1⇩π) ⋅ 1⇩π) ∥ NC)) = d (((R - 1⇩π) ⋅ 1⇩π) ∥ NC) ⋅ d (((S - 1⇩π) ⋅ 1⇩π) ∥ NC)"
  apply (simp add: U_def p_id_def s_prod_im p_prod_def d_def)
  nitpick
  oops

lemma "(((R - 1⇩π) ⋅ 1⇩π) ⋅ ((S - 1⇩π) ⋅ 1⇩π)) ∥ NC = (((R - 1⇩π) ⋅ 1⇩π) ∥ NC) ⋅ (((S - 1⇩π) ⋅ 1⇩π) ∥ NC)"
  nitpick
  oops

lemma "((((R - 1⇩π) ⋅ 1⇩π) ∥ NC) ⋅ (((S - 1⇩π) ⋅ 1⇩π) ∥ NC)) ⋅ 1⇩π  = ((((R - 1⇩π) ⋅ 1⇩π) ∥ NC) ⋅ 1⇩π) ⋅ ((((S - 1⇩π) ⋅ 1⇩π) ∥ NC) ⋅ 1⇩π)"
  nitpick
  oops

subsection ‹Terminal and Nonterminal Elements›

text ‹Lemma 11.4›

lemma "(R ⋅ S) ⋅ {} = (R ⋅ {}) ⋅ (S ⋅ {})"
  nitpick
  oops

lemma "(R ⋅ S) - 1⇩π = (R - 1⇩π) ⋅ (S - 1⇩π)"
  apply (auto simp: s_prod_im p_id_def)
  nitpick
  oops

lemma "(R ∥ S) - 1⇩π = (R - 1⇩π) ∥ (S - 1⇩π)"
  nitpick
  oops

text ‹Lemma 11.8.›

lemma "((R ⋅ 1⇩π) ⋅ (S - 1⇩π)) - 1⇩π = (R ⋅ 1⇩π) ⋅ (S - 1⇩π)"
  nitpick 
  oops

lemma "((S - 1⇩π) ⋅ (R ⋅ 1⇩π)) - 1⇩π = (S - 1⇩π) ⋅ (R ⋅ 1⇩π)"
  nitpick 
  oops

lemma "((R ⋅ 1⇩π) ∥ (S - 1⇩π)) ⋅ 1⇩π = (R ⋅ 1⇩π) ∥ (S - 1⇩π)"
  nitpick
  oops

text ‹Lemma 11.10.›

lemma "R ⋅ {} ⊆ S ⋅ {} ⟹ (R ⋅ T) ⋅ {} ⊆ (S ⋅ T) ⋅ {}"
  nitpick
  oops

lemma "R - 1⇩π ⊆ S - 1⇩π ⟹ (R ∥ T) - 1⇩π ⊆ (S ∥ T) - 1⇩π"
  nitpick
  oops

lemma "R - 1⇩π ⊆ S - 1⇩π ⟹ (T ⋅ R) - 1⇩π ⊆ (T ⋅ S) - 1⇩π"
  apply (auto simp: p_id_def s_prod_im)
  nitpick
  oops

text ‹Corollary 11.12›

lemma "R ⋅ {} = S ⋅ {} ⟹ (R ⋅ T) ⋅ {} = (S ⋅ T) ⋅ {}"
  nitpick
  oops

lemma "R - 1⇩π = S - 1⇩π ⟹ (R ∥ T) - 1⇩π = (S ∥ T) - 1⇩π"
  nitpick
  oops

lemma "R - 1⇩π = S - 1⇩π ⟹ (T ⋅ R) - 1⇩π = (T ⋅ S) - 1⇩π"
  apply (auto simp: p_id_def s_prod_im)
  nitpick
  oops

subsection ‹Multirelations, Proto-Quantales and Iteration›

interpretation mrel_proto_quantale: proto_quantale "1⇩σ" "(⋅)" Inter Union "(∩)" "(⊆)" "(⊂)" "(∪)" "{}" "U"
  by (unfold_locales, auto simp: mr_simp)

text ‹We reprove Corollary 13.2. because Isabelle does not pick it up from the quantale level.›

lemma iso_prop: "mono (λX. S ∪ R ⋅ X)"
  by (rule monoI, (clarsimp simp: mr_simp), blast)

lemma gfp_lfp_prop: "gfp (λX. R ⋅ X) ∪ lfp (λX. S ∪ R ⋅ X) ⊆ gfp (λX. S ∪ R ⋅ X)"
  by (simp add: lfp_le_gfp gfp_mono iso_prop)

subsection ‹Further Counterexamples›

text ‹Lemma 14,1. and 14.2› 

lemma  "R ∥ R ⊆ R" 
   nitpick
   oops 

lemma "R ⊆ R ∥ S"
   nitpick
   oops

lemma "R ∥ S ∩ R ∥ T ⊆ R ∥ (S ∩ T)"
  nitpick
  oops

lemma "R ⋅ (S ∥ T) = (R ⋅ S) ∥ (R ⋅ T)"
  nitpick
  oops

lemma "R ⋅ (S ⋅ T) ⊆ (R ⋅ S) ⋅ T"
  apply (auto simp: s_prod_im)
  nitpick
  oops

lemma "⟦R ∥ R = R; S ∥ S = S; T ∥ T = T⟧ ⟹ R ⋅ (S ∥ T) = (R ⋅ S) ∥ (R ⋅ T)"
  nitpick
  oops

lemma "⟦R ≠ {}; S ≠ {}; ∀a. (a,{}) ∉ R ∪ S⟧ ⟹ R ⋅ S ⊆ R ∥ S"
  quickcheck
  oops

lemma "⟦R ≠ {}; S ≠ {}; ∀a. (a,{}) ∉ R ∪ S⟧ ⟹ R ∥ S ⊆ R ⋅ S"
  quickcheck
  oops

lemma "⟦R ≠ {}; S ≠ {}; T ≠ {}; ∀a. (a,{}) ∉ R ∪ S ∪ T⟧ ⟹ (R ∥ S) ⋅ T ⊆ R ∥ (S ⋅ T)"
  quickcheck
  oops

lemma "⟦R ≠ {}; S ≠ {}; T ≠ {}; ∀a. (a,{}) ∉ R ∪ S ∪ T⟧ ⟹ R ∥ (S ⋅ T) ⊆ (R ∥ S) ⋅ T" 
  quickcheck
  oops

lemma "⟦R ≠ {}; S ≠ {}; T ≠ {}; ∀a. (a,{}) ∉ R ∪ S ∪ T⟧ ⟹ R ⋅ (S ∥ T) ⊆ (R ⋅ S) ∥ T"
  quickcheck
  oops

lemma "⟦R ≠ {}; S ≠ {}; T ≠ {}; ∀a. (a,{}) ∉ R ∪ S ∪ T⟧ ⟹ (R ⋅ S) ∥ T ⊆ R ⋅ (S ∥ T)"
  quickcheck
  oops

lemma "⟦R ≠ {}; S ≠ {}; ∀a. (a,{}) ∉ R ∪ S⟧ ⟹ (R ∥ S) ⋅ (R ∥ S) ⊆ (R ⋅ R) ∥ (S ⋅ S)"
  quickcheck
  oops

lemma "⟦R ≠ {}; S ≠ {}; ∀a. (a,{}) ∉ R ∪ S⟧ ⟹ (R ⋅ R) ∥ (S ⋅ S) ⊆ (R ∥ S) ⋅ (R ∥ S)"
  quickcheck
  oops

subsection ‹Relationship with Up-Closed Multirelations›

text ‹We now define Parikh's sequential composition.›

definition s_prod_pa :: "'a mrel ⇒ 'a mrel ⇒ 'a mrel" (infixl ‹⊗› 70) where
  "R ⊗ S = {(a,A). (∃B. (a,B) ∈ R ∧ (∀b ∈ B. (b,A) ∈ S))}"

text ‹We show that Parikh's definition doesn't preserve up-closure.›

lemma up_closed_prop: "((R ∥ U) ⋅ (S ∥ U)) ∥ U = (R ∥ U) ⋅ (S ∥ U)"
  apply (auto simp: p_prod_def s_prod_pa_def U_def)
  nitpick
  oops

text ‹Lemma 15.1.›

lemma onelem: "(R ⋅ S) ∥ U ⊆ R ⊗ (S ∥ U)"
  by (auto simp: s_prod_im p_prod_def U_def s_prod_pa_def)

lemma twolem: "R ⊗ (S ∥ U)  ⊆ (R ⋅ S) ∥ U"
proof clarify
  fix a A
  assume "(a,A) ∈ R ⊗ (S ∥ U)"
  hence "∃B. (a,B) ∈ R ∧ (∀b ∈ B. (b,A) ∈ S ∥ U)"
    by (auto simp: s_prod_pa_def)
  hence "∃B. (a,B) ∈ R ∧ (∀b ∈ B. ∃C. C ⊆ A ∧ (b,C) ∈ S)"
    by (metis U_par_st)
  hence "∃B. (a,B) ∈ R ∧ (∃f. (∀b ∈ B. f b ⊆ A ∧ (b,f b) ∈ S))"
    by metis
  hence "∃C. C ⊆ A ∧ (∃B. (a,B) ∈ R ∧ (∃f. (∀b ∈ B. (b,f b) ∈ S) ∧ C = ⋃ ((λx. f x) ` B)))"
    by clarsimp blast
  hence "∃C. C ⊆ A ∧ (a,C) ∈ R ⋅ S"     
    by (clarsimp simp: mr_simp)
  thus "(a,A) ∈ (R ⋅ S) ∥ U"
    by (simp add: U_par_st)
qed

lemma pe_pa_sim: "(R ⋅ S) ∥ U = R ⊗ (S ∥ U)"
  by (metis antisym onelem twolem)

lemma pe_pa_sim_var: "((R ∥ U) ⋅ (S ∥ U)) ∥ U = (R ∥ U) ⊗ (S ∥ U)"
  by (simp add: mrel_proto_trioid.mult_assoc pe_pa_sim)

lemma pa_assoc1: "((R ∥ U) ⊗ (S ∥ U)) ⊗ (T ∥ U) ⊆ (R ∥ U) ⊗ ((S ∥ U) ⊗ (T ∥ U))"
  by (clarsimp simp: p_prod_def s_prod_pa_def U_def, metis)

text ‹The converse direction of associativity remains to be proved.›

text ‹Corollary 15.3.›

lemma up_closed_par_is_meet: "(R ∥ U) ∥ (S ∥ U) = (R ∥ U) ∩ (S ∥ U)"
  by (auto simp: mr_simp)

end