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. (bB. (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. (bB. (b,f b)  S  (af b. (a,{a})  P))  A = ((λx. f x) ` B))"
      by (simp add: s_prod_test assms)
    hence "B. (a,B)  R  (f. (bB. (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. (bB. (b,f b)  S)  (aA. (a,{a})  P)  A = ((λx. f x) ` B))"
      by auto blast
    hence "(a,A)  R  S  (aA. (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. (bB. (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. (bB. f b  {})  b = (xB. 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. (bBB. (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. (bBa. f b = {})  B = (bBa. 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. (v3x1. (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