Theory Multirelations_Basics

section ‹Basic Properties of Multirelations›

theory Multirelations_Basics

imports Power_Allegories_Properties

begin

text ‹This theory extends a previous AFP entry for multirelations with one single objects to
proper multirelations in Rel.›

subsection ‹Peleg composition, parallel composition (inner union) and units›

type_synonym ('a,'b) mrel = "('a,'b set) rel"

definition s_prod :: "('a,'b) mrel ⇒ ('b,'c) mrel ⇒ ('a,'c) mrel" (infixl ‹⋅› 75) where
  "R ⋅ S = {(a,A). (∃B. (a,B) ∈ R ∧ (∃f. (∀b ∈ B. (b,f b) ∈ S) ∧ A = ⋃(f ` B)))}"

definition s_id :: "('a,'a) mrel" (‹1⇩σ›) where
  "1⇩σ = (⋃a. {(a,{a})})"

definition p_prod :: "('a,'b) mrel ⇒ ('a,'b) mrel ⇒ ('a,'b) mrel" (infixl ‹∥› 70) where
  "R ∥ S = {(a,A). (∃B C. A = B ∪ C ∧ (a,B) ∈ R ∧ (a,C) ∈ S)}"

definition p_id :: "('a,'b) mrel" (‹1⇩π›) where
  "1⇩π = (⋃a. {(a,{})})"

definition U :: "('a,'b) mrel" where
  "U = {(a,A) |a A. True}"

abbreviation "NC ≡ U - 1⇩π"

named_theorems mr_simp
declare s_prod_def [mr_simp] p_prod_def [mr_simp] s_id_def [mr_simp] p_id_def [mr_simp] U_def [mr_simp]

lemma s_prod_idl [simp]: "1⇩σ ⋅ R = R"
  by (auto simp: mr_simp)

lemma s_prod_idr [simp]: "R ⋅ 1⇩σ = R"
  by (auto simp: mr_simp) (metis UN_singleton)

lemma p_prod_ild [simp]: "1⇩π ∥ R = R"
  by (simp add: mr_simp)

lemma c_prod_idr [simp]: "R ∥ 1⇩π = R"
  by (simp add: mr_simp)

lemma cl7 [simp]: "1⇩σ ∥ 1⇩σ = 1⇩σ"
  by (auto simp: mr_simp)

lemma p_prod_assoc: "R ∥ S ∥ T = R ∥ (S ∥ T)"
  apply (rule set_eqI, clarsimp simp: mr_simp)
  by (metis (no_types, lifting) sup_assoc)

lemma p_prod_comm: "R ∥ S = S ∥ R"
  by (auto simp: mr_simp)

lemma subidem_par: "R ⊆ R ∥ R"
  by (auto simp: mr_simp)

lemma meet_le_par: "R ∩ S ⊆ R ∥ S"
  by (auto simp: mr_simp)

lemma s_prod_distr: "(R ∪ S) ⋅ T = R ⋅ T ∪ S ⋅ T"
  by (auto simp: mr_simp)

lemma s_prod_sup_distr: "(⋃X) ⋅ S = (⋃R ∈ X. R ⋅ S)"
  by (auto simp: mr_simp)

lemma s_prod_subdistl: "R ⋅ S ∪ R ⋅ T ⊆ R ⋅ (S ∪ T)"
  by (auto simp: mr_simp)

lemma s_prod_sup_subdistl: "X ≠ {} ⟹ (⋃S ∈ X. R ⋅ S) ⊆ R ⋅ ⋃X"
  by (simp add: mr_simp) blast

lemma s_prod_isol: "R ⊆ S ⟹ R ⋅ T ⊆ S ⋅ T"
  by (metis s_prod_distr sup.order_iff)

lemma s_prod_isor: "R ⊆ S ⟹ T ⋅ R ⊆ T ⋅ S"
  by (metis le_supE s_prod_subdistl sup.absorb_iff1)

lemma s_prod_zerol [simp]: "{} ⋅ R = {}"
  by (force simp: mr_simp)

lemma s_prod_wzeror: "R ⋅ {} ⊆ R"
  by (force simp: mr_simp)

lemma p_prod_zeror [simp]: "R ∥ {} = {}"
  by (simp add: mr_simp)

lemma s_prod_p_idl [simp]: "1⇩π ⋅ R = 1⇩π"
  by (force simp: mr_simp)

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

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

lemma p_prod_distl: "R ∥ (S ∪ T) = R ∥ S ∪ R ∥ T"
  by (fastforce simp: mr_simp)

lemma p_prod_sup_distl: "R ∥ (⋃X) = (⋃S ∈ X. R ∥ S)"
  by (fastforce simp: mr_simp)

lemma p_prod_isol: "R ⊆ S ⟹ R ∥ T ⊆ S ∥ T"
  by (metis p_prod_comm p_prod_distl sup.orderE sup.orderI)

lemma p_prod_isor: "R ⊆ S ⟹ T ∥ R ⊆ T ∥ S"
  by (simp add: p_prod_comm p_prod_isol)

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

lemma U_U [simp]: "U ⋅ U = U"
  by (simp add: mr_simp) blast

lemma U_par_idem [simp]: "U ∥ U = U"
  by (simp add: U_def equalityI subidem_par)

lemma p_id_NC: "R - 1⇩π = R ∩ NC"
  by (simp add: Diff_eq U_def)

lemma NC_NC [simp]: "NC ⋅ NC = NC"
  by (rule set_eqI, clarsimp simp: mr_simp, metis SUP_bot_conv(2) UN_constant insert_not_empty)

lemma nc_par_idem [simp]: "NC ∥ NC = NC"
  by (force 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
    subgoal for D E f g
      apply (rule exI[of _ D])
      apply (rule exI[of _ E])
      apply clarify
      apply (rule exI[of _ f])
      apply (rule exI[of _ g])
      using assms by (auto simp: p_prod_def, blast)
    done
  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
    subgoal for D E f g 
      apply (rule exI[of _ D])
      apply (rule exI[of _ E])
      apply clarify
      apply (rule exI[of _ "λx. if x ∈ (D - E) then f x else (if x ∈ D ∩ E then (f x ∪ g x) else g x)"])
      by auto
    done
  hence "(∃B. (a,B) ∈ R ∥ S ∧ (∃h. (∀b∈B. (b,h b) ∈ T) ∧ A = ⋃((λx. h x) ` B)))"
    by clarsimp 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 p_id_assoc1: "(1⇩π ⋅ R) ⋅ S = 1⇩π ⋅ (R ⋅ S)"
  by simp

lemma p_id_assoc2: "(R ⋅ 1⇩π) ⋅ T = R ⋅ (1⇩π ⋅ T)"
  by (rule set_eqI, clarsimp simp: mr_simp) fastforce

lemma cl1 [simp]: "R ⋅ 1⇩π ∪ R ⋅ NC = R ⋅ U"
  by (rule set_eqI, clarsimp simp: mr_simp, metis UN_constant UN_empty)

lemma tarski_aux:
  assumes "R - 1⇩π ≠ {}"
  and "(a,A) ∈ NC"
  shows "(a,A) ∈ NC ⋅ ((R - 1⇩π) ⋅ NC)"
  using assms apply (clarsimp simp: mr_simp)
  by (metis UN_constant insert_not_empty singletonD)

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

lemma tarski_var:
  assumes "R ∩ NC ≠ {}"
  shows "NC ⋅ ((R ∩ NC) ⋅ NC) = NC"
  by (metis assms p_id_NC tarski)

lemma s_le_nc: "1⇩σ ⊆ NC"
  by (auto simp: mr_simp)

lemma U_nc [simp]: "U ⋅ NC = U"
  by (metis NC_NC cl1 s_prod_distr s_prod_idl s_prod_p_idl)

lemma x_y_split [simp]: "(R ∩ NC) ⋅ S ∪ R ⋅ {} = R ⋅ S"
  by (auto simp: mr_simp)

lemma c_nc_comp1 [simp]: "1⇩π ∪ NC = U"
  using cl1 s_prod_idl by blast

subsection ‹Tests›

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

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

lemma s_prod_test_aux1:
  assumes "(a,A) ∈ R ⋅ (P ∩ 1⇩σ)"
  shows "((a,A) ∈ R ∧ (∀a ∈ A. (a,{a}) ∈ (P ∩ 1⇩σ)))"
  using assms by (auto simp: mr_simp)

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

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

lemma s_prod_test_var: "R ⋅ (P ∩ 1⇩σ) = {(a,A). (a,A) ∈ R ∧ (∀a ∈ A. (a,{a}) ∈ (P ∩ 1⇩σ))}"
  apply (rule antisym)
  by (fastforce simp: mr_simp)+

lemma test_s_prod_aux1:
  assumes "(a,A) ∈ (P ∩ 1⇩σ) ⋅ R"
  shows "(a,{a}) ∈ (P ∩ 1⇩σ) ∧ (a,A) ∈ R"
  using assms by (auto simp: mr_simp)

lemma test_s_prod_aux2:
  assumes "(a,A) ∈ R"
  and "(a,{a}) ∈ P"
  shows "(a,A) ∈ P ⋅ R"
  using assms s_prod_def by fastforce

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

lemma test_s_prod_var: "(P ∩ 1⇩σ) ⋅ R = {(a,A). (a,{a}) ∈ (P ∩ 1⇩σ) ∧ (a,A) ∈ R}"
  by (simp add: set_eq_iff test_s_prod)

lemma test_assoc1: "(R ⋅ (P ∩ 1⇩σ)) ⋅ S = R ⋅ ((P ∩ 1⇩σ) ⋅ S)"
  apply (rule antisym)
  apply (simp add: s_prod_assoc1)
  apply (clarsimp simp: mr_simp)
  by (metis UN_singleton)

lemma test_assoc2: "((P ∩ 1⇩σ) ⋅ R) ⋅ S = (P ∩ 1⇩σ) ⋅ (R ⋅ S)"
  apply (rule antisym)
  apply (simp add: s_prod_assoc1)
  by (fastforce simp: mr_simp s_prod_assoc1)

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

lemma s_distl_test: "(P ∩ 1⇩σ) ⋅ (S ∪ T) = (P ∩ 1⇩σ) ⋅ S ∪ (P ∩ 1⇩σ) ⋅ T"
  by (fastforce simp: mr_simp)

lemma s_distl_sup_test: "(P ∩ 1⇩σ) ⋅ ⋃X = (⋃S ∈ X. (P ∩ 1⇩σ) ⋅ S)"
  by (auto simp: mr_simp)

lemma subid_par_idem [simp]: "(P ∩ 1⇩σ) ∥ (P ∩ 1⇩σ) = (P ∩ 1⇩σ)"
  by (auto simp: mr_simp)

lemma seq_conc_subdistrl: "(P ∩ 1⇩σ) ⋅ (S ∥ T) = ((P ∩ 1⇩σ) ⋅ S) ∥ ((P ∩ 1⇩σ) ⋅ T)"
  apply (rule antisym)
  apply (simp add: cl3)
  by (fastforce simp: mr_simp)

lemma test_s_prod_is_meet [simp]: "(P ∩ 1⇩σ) ⋅ (Q ∩ 1⇩σ) = P ∩ Q ∩ 1⇩σ"
  by (auto simp: mr_simp)

lemma test_p_prod_is_meet [simp]: "(P ∩ 1⇩σ) ∥ (Q ∩ 1⇩σ) = (P ∩ 1⇩σ) ∩ (Q ∩ 1⇩σ)"
  by (auto simp: mr_simp)

lemma test_multipliciativer: "(P ∩ Q ∩ 1⇩σ) ⋅ T = ((P ∩ 1⇩σ) ⋅ T) ∩ ((Q ∩ 1⇩σ) ⋅ T)"
  by (auto simp: mr_simp)

lemma cl9 [simp]: "(R ∩ 1⇩σ) ⋅ 1⇩π ∥ 1⇩σ = R ∩ 1⇩σ"
  by (auto simp: mr_simp)

lemma s_subid_closed [simp]: "R ∩ NC ∩ 1⇩σ = R ∩ 1⇩σ"
  using s_le_nc by auto

lemma sub_id_le_nc: "R ∩ 1⇩σ ⊆ NC"
  by (simp add: le_infI2 s_le_nc)

lemma x_y_prop: "1⇩σ ∩ ((R ∩ NC) ⋅ S) = 1⇩σ ∩ R ⋅ S"
  by (auto simp: mr_simp)

lemma s_nc_U: "1⇩σ ∩ R ⋅ NC = 1⇩σ ∩ R ⋅ U"
  by (rule set_eqI, clarsimp simp: mr_simp, metis SUP_constant UN_empty insert_not_empty)

lemma sid_le_nc_var: "1⇩σ ∩ R ⊆ 1⇩σ ∩ (R ∥ NC)"
  using meet_le_par s_le_nc by fastforce

lemma s_nc_par_U: "1⇩σ ∩ (R ∥ NC) = 1⇩σ ∩ (R ∥ U)"
  by (metis c_nc_comp1 c_prod_idr inf_sup_distrib1 le_iff_sup p_prod_distl sid_le_nc_var)

lemma s_id_par_s_prod: "(P ∩ 1⇩σ) ∥ (Q ∩ 1⇩σ) = (P ∩ 1⇩σ) ⋅ (Q ∩ 1⇩σ)"
  by force

subsection ‹Parallel subidentities›

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

lemma p_subid_iff: "R ⊆ 1⇩π ⟷ R ⋅ 1⇩π = R"
  by (clarsimp simp: mr_simp, safe, simp_all) blast+

lemma p_subid_iff_var: "R ⊆ 1⇩π ⟷ R ⋅ {} = R"
  by (clarsimp simp: mr_simp, safe, simp_all) blast+

lemma term_par_idem [simp]: "(R ∩ 1⇩π) ∥ (R ∩ 1⇩π) = (R ∩ 1⇩π)"
  by (metis Int_Un_eq(4) c_prod_idr p_prod_distl subidem_par subset_Un_eq)

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

lemma p_id_zero: "R ∩ 1⇩π = R ⋅ {}"
  by (auto simp: mr_simp)

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" and A::"'f set"
    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 fastforce
    hence "∃B. (a,B) ∈ R ∧ (∃f. (∀b ∈ B. (b,f b) ∈ S ∧ (∀x ∈ f b. (x,{}) ∈ T ⋅ {}))) ∧ A = {}"
      by (metis (mono_tags))
    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

lemma c4: "(R ⋅ S) ⋅ 1⇩π = R ⋅ (S ⋅ 1⇩π)"
proof -
  have "(R ⋅ S) ⋅ 1⇩π = {(a,{}) | a. ∃B. (a,B) ∈ R ⋅ S}"
    by (simp add: p_id_st)
  also have "… = R ⋅ {(a,{}) | a. ∃B. (a,B) ∈ S}"
    apply (clarsimp simp: mr_simp)
    apply safe
    apply blast
    apply clarsimp
    by metis
  also have "… = R ⋅ (S ⋅ 1⇩π)"
    by (simp add: p_id_st)
  finally show ?thesis.
qed

lemma c3: "(R ∥ S) ⋅ 1⇩π = R ⋅ 1⇩π ∥ S ⋅ 1⇩π"
  by (simp add: Orderings.order_eq_iff cl4 seq_conc_subdistr)

lemma p_id_idem [simp]: "(R ⋅ 1⇩π) ⋅ 1⇩π = R ⋅ 1⇩π"
  by (simp add: c4)

lemma x_c_par_idem [simp]: "R ⋅ 1⇩π ∥ R ⋅ 1⇩π = R ⋅ 1⇩π"
  by (metis c1 p_id_idem)

lemma x_zero_le_c: "R ⋅ {} ⊆ 1⇩π"
  by (simp add: c4 p_subid_iff)

lemma p_subid_lb1: "R ⋅ {} ∥ S ⋅ {} ⊆ R ⋅ {}"
  by (metis c_prod_idr p_prod_isor x_zero_le_c)

lemma p_subid_lb2: "R ⋅ {} ∥ S ⋅ {} ⊆ S ⋅ {}"
  using p_prod_comm p_subid_lb1 by blast

lemma p_subid_idem [simp]: "R ⋅ {} ∥ R ⋅ {} = R ⋅ {}"
  by (simp add: p_subid_lb1 subidem_par subset_antisym)

lemma p_subid_glb: "T ⋅ {} ⊆ R ⋅ {} ⟹ T ⋅ {} ⊆ S ⋅ {} ⟹ T ⋅ {} ⊆ (R ⋅ {}) ∥ (S ⋅ {})"
  by (auto simp: mr_simp)

lemma p_subid_glb_iff: "T ⋅ {} ⊆ R ⋅ {} ∧ T ⋅ {} ⊆ S ⋅ {} ⟷ T ⋅ {} ⊆ (R ⋅ {}) ∥ (S ⋅ {})"
  by (auto simp: mr_simp)

lemma x_c_glb: "(T::('a,'b) mrel) ⋅ 1⇩π ⊆ (R::('a,'b) mrel) ⋅ 1⇩π ⟹ T ⋅ 1⇩π ⊆ (S::('a,'b) mrel) ⋅ 1⇩π ⟹ T ⋅ 1⇩π ⊆ (R ⋅ 1⇩π) ∥ (S ⋅ 1⇩π)"
  by (smt (verit, best) order_subst1 p_id_idem p_prod_isol p_prod_isor s_prod_isol x_c_par_idem)

lemma x_c_lb1: "R ⋅ 1⇩π ∥ S ⋅ 1⇩π ⊆ R ⋅ 1⇩π"
  by (metis c6 c_prod_idr p_prod_isor)

lemma x_c_lb2: "R ⋅ 1⇩π ∥ S ⋅ 1⇩π ⊆ S ⋅ 1⇩π"
  using p_prod_comm x_c_lb1 by blast

lemma x_c_glb_iff: "(T::('a,'b) mrel) ⋅ 1⇩π ⊆ (R::('a,'b) mrel) ⋅ 1⇩π ∧ T ⋅ 1⇩π ⊆ (S::('a,'b) mrel) ⋅ 1⇩π ⟷ T ⋅ 1⇩π ⊆ (R ⋅ 1⇩π) ∥ (S ⋅ 1⇩π)"
  by (meson subset_trans x_c_glb x_c_lb1 x_c_lb2)

lemma nc_iff1: "R ⊆ NC ⟷ R ∩ 1⇩π = {}"
  by (metis (no_types, lifting) Diff_Diff_Int Int_Diff Int_absorb diff_shunt_var p_id_NC)

lemma nc_iff2: "R ⊆ NC ⟷ R ⋅ {} = {}"
  by (metis c4 nc_iff1 p_id_zero s_prod_zerol)

lemma zero_assoc3: "(R ⋅ S) ⋅ {} = R ⋅ (S ⋅ {})"
  by (metis cl5 s_prod_zerol)

lemma x_zero_interr: "R ⋅ {} ∥ S ⋅ {} = (R ∥ S) ⋅ {}"
  by (clarsimp simp: mr_simp) blast

lemma p_subid_interr: "R ⋅ T ⋅ 1⇩π ∥ S ⋅ T ⋅ 1⇩π = (R ∥ S) ⋅ T ⋅ 1⇩π"
proof -
  have "R ⋅ T ⋅ 1⇩π ∥ S ⋅ T ⋅ 1⇩π = (R ⋅ {(a,{}) |a. ∃B. (a,B) ∈ T}) ∥ (S ⋅ {(a,{}) |a. ∃B. (a,B) ∈ T})"
    by (metis c4 p_id_st)
  also have "… = (R ∥ S) ⋅ {(a,{}) |a. ∃B. (a,B) ∈ T}"
    apply (rule antisym)
    apply (metis cl4 dual_order.refl p_id_st x_c_par_idem)
    by (simp add: seq_conc_subdistr)
  also have "… = (R ∥ S) ⋅ T ⋅ 1⇩π"
    by (metis c4 p_id_st)
  finally show ?thesis.
qed

lemma cl2 [simp]: "1⇩π ∩ (R ∪ NC) = R ⋅ {}"
  by (metis Diff_disjoint Int_Un_distrib inf_commute p_id_zero sup_bot.right_neutral)

lemma cl6 [simp]: "R ⋅ {} ⋅ S = R ⋅ {}"
  by (metis c4 p_id_assoc2 s_prod_p_idl s_prod_zerol)

lemma cl11 [simp]: "(R ∩ NC) ⋅ 1⇩π ∥ NC = (R ∩ NC) ⋅ NC"
  apply (rule antisym)
  apply (clarsimp simp: mr_simp)
  apply (metis UN_constant)
  apply (clarsimp simp: mr_simp)
  by (metis UN_empty2 UN_insert Un_empty_left equals0I insert_absorb sup_bot_right)

lemma x_split [simp]: "(R ∩ NC) ∪ (R ∩ 1⇩π) = R"
  by (metis Un_Diff_Int p_id_NC)

lemma x_split_var [simp]: "(R ∩ NC) ∪ R ⋅ {} = R"
  by (metis p_id_zero x_split)

lemma s_x_c [simp]: "1⇩σ ∩ R ⋅ 1⇩π = {}"
  using c6 s_le_nc by fastforce

lemma s_x_zero [simp]: "1⇩σ ∩ R ⋅ {} = {}"
  using cl6 s_x_c by blast

lemma c_nc [simp]: "R ⋅ 1⇩π ∩ NC = {}"
  using c6 by blast

lemma zero_nc [simp]: "R ⋅ {} ∩ NC = {}"
  using x_zero_le_c by fastforce

lemma nc_zero [simp]: "(R ∩ NC) ⋅ {} = {}"
  using nc_iff2 by auto

lemma c_def [simp]: "U ⋅ {} = 1⇩π"
  by (metis c_nc_comp1 cl2 cl6 inf_commute p_id_zero s_prod_p_idl)

lemma U_c [simp]: "U ⋅ 1⇩π = 1⇩π"
  by (metis U_U c_def zero_assoc3)

lemma nc_c [simp]: "NC ⋅ 1⇩π = 1⇩π"
  by (auto simp: mr_simp)

lemma nc_U [simp]: "NC ⋅ U = U"
  using NC_NC c_nc_comp1 cl1 nc_c by blast

lemma x_c_nc_split [simp]: "((R ∩ NC) ⋅ NC) ∪ (R ⋅ {} ∥ NC) = (R ⋅ 1⇩π) ∥ NC"
  by (metis cl11 p_prod_comm p_prod_distl x_y_split)

lemma x_c_U_split [simp]: "R ⋅ U ∪ (R ⋅ {} ∥ U) = R ⋅ 1⇩π ∥ U"
  apply (rule set_eqI, clarsimp simp: mr_simp)
  by (metis SUP_constant UN_extend_simps(2))

lemma p_subid_par_eq_meet [simp]: "R ⋅ {} ∥ S ⋅ {} = R ⋅ {} ∩ S ⋅ {}"
  by (auto simp: mr_simp)

lemma p_subid_par_eq_meet_var [simp]: "R ⋅ 1⇩π ∥ S ⋅ 1⇩π = R ⋅ 1⇩π ∩ S ⋅ 1⇩π"
  by (metis c_def p_subid_par_eq_meet zero_assoc3)

lemma x_zero_add_closed: "R ⋅ {} ∪ S ⋅ {} = (R ∪ S) ⋅ {}"
  by (simp add: s_prod_distr)

lemma x_zero_meet_closed: "R ⋅ {} ∩ S ⋅ {} = (R ∩ S) ⋅ {}"
  by (force simp: mr_simp)

lemma scomp_univalent_pres: "univalent R ⟹ univalent S ⟹ univalent (R ⋅ S)"
  unfolding univalent_set s_prod_def
  apply clarsimp
  by (metis Sup.SUP_cong)

lemma "univalent s_id"
  unfolding univalent_set s_id_def by simp

lemma det_peleg: "deterministic R ⟹ deterministic S ⟹ deterministic (R ⋅ S)"
  unfolding deterministic_set s_prod_def
  apply clarsimp
  apply safe
  apply metis
  apply (metis UN_I)
  by (metis UN_I)

lemma deterministic_sid: "deterministic 1⇩σ"
  unfolding deterministic_set s_id_def by simp


subsection ‹Domain›

definition Dom :: "('a,'b) mrel ⇒ ('a,'a) mrel" where
  "Dom R = {(a,{a}) |a. ∃B. (a,B) ∈ R}"

named_theorems mrd_simp
declare mr_simp [mrd_simp] Dom_def [mrd_simp]

lemma d_def_expl: "Dom R = R ⋅ 1⇩π ∥ 1⇩σ"
  by (force simp: mrd_simp set_eqI)

lemma s_subid_iff2: "(R ∩ 1⇩σ = R) = (Dom R = R)"
  by (metis c6 cl9 d_def_expl inf.order_iff p_prod_comm p_prod_ild p_prod_isor)

lemma cl8_var: "Dom R ⋅ S = R ⋅ 1⇩π ∥ S"
  apply (rule antisym)
  apply (metis d_def_expl p_id_assoc2 s_prod_idl s_prod_p_idl seq_conc_subdistr)
  by (force simp: mrd_simp)

lemma cl8 [simp]: "R ⋅ 1⇩π ∥ 1⇩σ ⋅ S = R ⋅ 1⇩π ∥ S"
  by simp

lemma cl10_var: "Dom (R - 1⇩π) = 1⇩σ ∩ ((R - 1⇩π) ⋅ NC)"
  apply (rule set_eqI, clarsimp simp: mrd_simp)
  apply safe
  apply (metis SUP_constant insert_not_empty)
  by blast

lemma c10: "(R ∩ NC) ⋅ 1⇩π ∥ 1⇩σ = 1⇩σ ∩ ((R ∩ NC) ⋅ NC)"
  by (metis Int_Diff cl10_var d_def_expl)

lemma cl9_var [simp]: "Dom (R ∩ 1⇩σ) = R ∩ 1⇩σ"
  by (simp add: d_def_expl)

lemma d_s_id [simp]: "Dom R ∩ 1⇩σ = Dom R"
  by (metis cl8_var d_def_expl p_prod_comm p_prod_ild s_subid_iff2)

lemma d_s_id_ax: "Dom R ⊆ 1⇩σ"
  by (simp add: le_iff_inf)

lemma d_assoc1: "Dom R ⋅ (S ⋅ T) = (Dom R ⋅ S) ⋅ T"
  by (metis d_s_id test_assoc2)

lemma d_meet_distr_var: "(Dom R ∩ Dom S) ⋅ T = Dom R ⋅ T ∩ Dom S ⋅ T"
  by (metis (no_types, lifting) d_s_id inf_assoc test_multipliciativer)

lemma d_idem [simp]: "Dom (Dom R) = Dom R"
  by (meson d_s_id s_subid_iff2)

lemma cd_2_var: "Dom (R ⋅ 1⇩π) ⋅ S = R ⋅ 1⇩π ∥ S"
  by (simp add: cl8_var p_id_assoc2)

lemma dc_prop1 [simp]: "Dom R ⋅ 1⇩π = R ⋅ 1⇩π"
  by (simp add: cl8_var)

lemma dc_prop2 [simp]: "Dom (R ⋅ 1⇩π) = Dom R"
  by (simp add: d_def_expl p_id_assoc2)

lemma ds_prop [simp]: "Dom R ∥ 1⇩σ = Dom R"
  by (simp add: p_prod_assoc d_def_expl)

lemma dc [simp]: "Dom 1⇩π = 1⇩σ"
  by (simp add: d_def_expl)

lemma cd_iso [simp]: "Dom (R ⋅ 1⇩π) ⋅ 1⇩π = R ⋅ 1⇩π"
  by simp

lemma dc_iso [simp]: "Dom (Dom R ⋅ 1⇩π) = Dom R"
  by simp

lemma d_s_id_inter [simp]: "Dom R ⋅ Dom S = Dom R ∩ Dom S"
  by (metis d_s_id inf_assoc test_s_prod_is_meet)

lemma d_conc6: "Dom (R ∥ S) = Dom R ∥ Dom S"
  by (metis (no_types, lifting) c3 d_def_expl ds_prop p_prod_assoc p_prod_comm)

lemma d_conc_inter [simp]: "Dom R ∥ Dom S = Dom R ∩ Dom S"
  by (metis d_s_id test_p_prod_is_meet)

lemma d_conc_s_prod_ax: "Dom R ∥ Dom S = Dom R ⋅ Dom S"
  by simp

lemma d_rest_ax [simp]: "Dom R ⋅ R = R"
  by (simp add: cl8_var)

lemma d_loc_ax [simp]: "Dom (R ⋅ Dom S) = Dom (R ⋅ S)"
  by (metis c4 dc_prop1 dc_prop2)

lemma assoc_p_subid: "(R ⋅ S) ⋅ (T ⋅ 1⇩π) = R ⋅ (S ⋅ (T ⋅ 1⇩π))"
  by (smt (verit, del_insts) c4 cd_iso d_idem d_loc_ax p_id_idem s_subid_iff2 test_assoc3)

lemma d_exp_ax [simp]: "Dom (Dom R ⋅ S) = Dom R ⋅ Dom S"
  by (metis d_conc6 d_conc_s_prod_ax d_idem d_loc_ax)

lemma d_comm_ax: "Dom R ⋅ Dom S = Dom S ⋅ Dom R"
  by force

lemma d_s_id_prop [simp]: "Dom 1⇩σ = 1⇩σ"
  by (simp add: d_def_expl)

lemma d_s_prod_closed [simp]: "Dom (Dom R ⋅ Dom S) = Dom R ⋅ Dom S"
  using d_exp_ax d_loc_ax by blast

lemma d_p_prod_closed [simp]: "Dom (Dom R ∥ Dom S) = Dom R ∥ Dom S"
  using d_s_prod_closed by auto

lemma d_idem2 [simp]: "Dom R ⋅ Dom R = Dom R"
  by (metis d_exp_ax d_rest_ax)

lemma d_assoc: "(Dom R ⋅ Dom S) ⋅ Dom T = Dom R ⋅ (Dom S ⋅ Dom T)"
  using d_assoc1 by blast

lemma iso_1 [simp]: "Dom R ⋅ 1⇩π ∥ 1⇩σ = Dom R"
  using d_def_expl by force

lemma d_idem_par [simp]: "Dom R ∥ Dom R = Dom R"
  by (simp add: d_conc_s_prod_ax)

lemma d_inter_r: "Dom R ⋅ (S ∥ T) = Dom R ⋅ S ∥ Dom R ⋅ T"
  by (metis d_s_id seq_conc_subdistrl)

lemma d_add_ax: "Dom (R ∪ S) = Dom R ∪ Dom S"
  by (simp add: d_def_expl p_prod_comm p_prod_distl s_prod_distr)

lemma d_sup_add: "Dom (⋃X) = (⋃R ∈ X. Dom R)"
  by (auto simp: mrd_simp)

lemma d_distl: "Dom R ⋅ (S ∪ T) = Dom R ⋅ S ∪ Dom R ⋅ T"
  by (metis d_s_id s_distl_test)

lemma d_sup_distl: "Dom R ⋅ ⋃X = (⋃S ∈ X. Dom R ⋅ S)"
  by (metis d_s_id s_distl_sup_test)

lemma d_zero_ax [simp]: "Dom {} = {}"
  by (simp add: d_def_expl p_prod_comm)

lemma d_absorb1 [simp]: "Dom R ∪ Dom R ⋅ Dom S = Dom R"
  by simp

lemma d_absorb2 [simp]: "Dom R ⋅ (Dom R ∪ Dom S) = Dom R"
  by (metis d_absorb1 d_idem2 d_s_id s_distl_test)

lemma d_dist1: "Dom R ⋅ (Dom S ∪ Dom T) = Dom R ⋅ Dom S ∪ Dom R ⋅ Dom T"
  by (simp add: cl8_var p_prod_distl)

lemma d_dist2: "Dom R ∪ (Dom S ⋅ Dom T) = (Dom R ∪ Dom S) ⋅ (Dom R ∪ Dom T)"
  by (smt (verit) boolean_algebra.disj_conj_distrib d_add_ax d_s_id_inter dc_prop2)

lemma d_add_prod_closed [simp]: "Dom (Dom R ∪ Dom S) = Dom R ∪ Dom S"
  by (simp add: d_add_ax)

lemma x_zero_prop: "R ⋅ {} ∥ S = Dom (R ⋅ {}) ⋅ S"
  by (simp add: cl8_var)

lemma cda_add_ax: "Dom ((R ∪ S) ⋅ T) = Dom (R ⋅ T) ∪ Dom (S ⋅ T)"
  by (simp add: d_add_ax s_prod_distr)

lemma d_x_zero: "Dom (R ⋅ {}) = R ⋅ {} ∥ 1⇩σ"
  by (simp add: d_def_expl)

lemma cda_ax2:
  assumes "(R ∥ S) ⋅ Dom T = R ⋅ Dom T ∥ S ⋅ Dom T"
  shows "Dom ((R ∥ S) ⋅ T) = Dom (R ⋅ T) ⋅ Dom (S ⋅ T)"
  by (metis assms d_conc6 d_conc_s_prod_ax d_loc_ax)

lemma d_lb1: "Dom R ⋅ Dom S ⊆ Dom R"
  using d_absorb1 by blast

lemma d_lb2: "Dom R ⋅ Dom S ⊆ Dom S"
  using d_comm_ax d_lb1 by blast

lemma d_glb: "Dom T ⊆ Dom R ∧ Dom T ⊆ Dom S ⟹ Dom T ⊆ Dom R ⋅ Dom S"
  by simp

lemma d_glb_iff: "Dom T ⊆ Dom R ∧ Dom T ⊆ Dom S ⟷ Dom T ⊆ Dom R ⋅ Dom S"
  by force

lemma d_interr: "R ⋅ Dom P ∥ S ⋅ Dom P = (R ∥ S) ⋅ Dom P"
  by (simp add: cl4 seq_conc_subdistr subset_antisym)

lemma cl10_d: "Dom (R ∩ NC) = 1⇩σ ∩ (R ∩ NC) ⋅ NC"
  by (simp add: c10 d_def_expl)

lemma cl11_d [simp]: "Dom (R ∩ NC) ⋅ NC = (R ∩ NC) ⋅ NC"
  by (simp add: cl8_var)

lemma cl10_d_var1: "Dom (R ∩ NC) = 1⇩σ ∩ R ⋅ NC"
  by (simp add: cl10_d x_y_prop)

lemma cl10_d_var2: "Dom (R ∩ NC) = 1⇩σ ∩ (R ∩ NC) ⋅ U"
  by (simp add: cl10_d_var1 s_nc_U x_y_prop)

lemma cl10_d_var3: "Dom (R ∩ NC) = 1⇩σ ∩ R ⋅ U"
  by (simp add: cl10_d_var1 s_nc_U)

lemma d_U [simp]: "Dom U = 1⇩σ"
  by (metis U_c dc dc_prop2)

lemma d_nc [simp]: "Dom NC = 1⇩σ"
  by (metis dc dc_prop2 nc_c)

lemma alt_d_def_nc_nc: "Dom (R ∩ NC) = 1⇩σ ∩ (((R ∩ NC) ⋅ 1⇩π) ∥ NC)"
  using c10 cl11_d cl8_var d_def_expl by blast

lemma alt_d_def_nc_U: "Dom (R ∩ NC) = 1⇩σ ∩ (((R ∩ NC) ⋅ 1⇩π) ∥ U)"
  using alt_d_def_nc_nc s_nc_par_U by blast

lemma d_def_split [simp]: "Dom (R ∩ NC) ∪ Dom (R ⋅ {}) = Dom R"
  by (metis d_add_ax d_loc_ax d_zero_ax p_id_zero x_split)

lemma d_def_split_var [simp]: "Dom (R ∩ NC) ∪ ((R ⋅ {}) ∥ 1⇩σ) = Dom R"
  using d_def_split d_x_zero by blast

lemma ax7 [simp]: "(1⇩σ ∩ R ⋅ U) ∪ (R ⋅ {} ∥ 1⇩σ) = Dom R"
  using cl10_d_var3 d_def_split d_x_zero by blast

lemma dom12_d: "Dom R = 1⇩σ ∩ (R ⋅ 1⇩π ∥ NC)"
  by (metis cl10_d_var3 cl8_var d_idem d_s_id inf.orderE s_nc_par_U sub_id_le_nc)

lemma dom12_d_U: "Dom R = 1⇩σ ∩ (R ⋅ 1⇩π ∥ U)"
  by (simp add: dom12_d s_nc_par_U)

lemma dom_def_var: "Dom R = (R ⋅ U ∩ 1⇩π) ∥ 1⇩σ"
  by (simp add: d_def_expl p_id_zero zero_assoc3)

lemma ax5_d [simp]: "Dom (R ∩ NC) ⋅ U = (R ∩ NC) ⋅ U"
  by (metis cl1 cl11_d dc_prop1)

lemma ax5_0 [simp]: "Dom (R ⋅ {}) ⋅ U = R ⋅ {} ∥ U"
  using x_zero_prop by auto

lemma x_c_U_split2: "Dom R ⋅ NC = (R ∩ NC) ⋅ NC ∪ (R ⋅ {} ∥ NC)"
  by (simp add: cl8_var)

lemma x_c_U_split3: "Dom R ⋅ U = (R ∩ NC) ⋅ U ∪ (R ⋅ {} ∥ U)"
  by (metis ax5_0 ax5_d d_def_split s_prod_distr)

lemma x_c_U_split_d: "Dom R ⋅ U = R ⋅ U ∪ (R ⋅ {} ∥ U)"
  by (simp add: cl8_var)

lemma x_U_prop2: "R ⋅ NC = Dom (R ∩ NC) ⋅ NC ∪ R ⋅ {}"
  by simp

lemma x_U_prop3: "R ⋅ U = Dom (R ∩ NC) ⋅ U ∪ R ⋅ {}"
  by (metis ax5_d x_y_split)

lemma d_x_nc [simp]: "Dom (R ⋅ NC) = Dom R"
  by (metis d_loc_ax d_nc dc dc_prop2)

lemma d_x_U [simp]: "Dom (R ⋅ U) = Dom R"
  by (metis d_U d_loc_ax dc dc_prop2)

lemma d_llp1: "Dom R ⊆ Dom S ⟹ R ⊆ Dom S ⋅ R"
  by (metis d_rest_ax s_prod_isol)

lemma d_llp2: "R ⊆ Dom S ⋅ R ⟹ Dom R ⊆ Dom S"
  by (metis d_assoc1 d_exp_ax d_meet_distr_var d_rest_ax d_s_id_inter inf.absorb_iff2)

lemma demod1: "Dom (R ⋅ S) ⊆ Dom T ⟹ R ⋅ Dom S ⊆ Dom T ⋅ R"
proof -
  assume h: "Dom (R ⋅ S) ⊆ Dom T"
  have "R ⋅ Dom S = Dom (R ⋅ Dom S) ⋅ (R ⋅ Dom S)"
    using d_rest_ax by blast
  also have "… ⊆ Dom T ⋅ (R ⋅ Dom S)"
    by (metis d_loc_ax h s_prod_distr subset_Un_eq)
  also have "… ⊆ Dom T ⋅ R"
    by (metis d_s_id_ax s_prod_idr s_prod_isor)
  finally show "R ⋅ Dom S ⊆ Dom T ⋅ R".
qed

lemma demod2: "R ⋅ Dom S ⊆ Dom T ⋅ R ⟹ Dom (R ⋅ S) ⊆ Dom T"
proof -
  assume h: "R ⋅ Dom S ⊆ Dom T ⋅ R"
  have "Dom (R ⋅ S) = Dom (R ⋅ Dom S)"
    by auto
  also have "… ⊆ Dom (Dom T ⋅ R)"
    by (metis d_add_ax h subset_Un_eq)
  also have "… = Dom T ⋅ Dom R"
    by simp
  also have "… ⊆ Dom T"
    by (simp add: d_lb1)
  finally show "Dom (R ⋅ S) ⊆ Dom T".
qed

lemma d_meet_closed [simp]: "Dom (Dom x ∩ Dom y) = Dom x ∩ Dom y"
  by (metis d_s_id inf_assoc s_subid_iff2)

lemma d_add_var: "Dom P ⋅ R ∪ Dom Q ⋅ R = Dom (P ∪ Q) ⋅ R"
  by (simp add: d_add_ax s_prod_distr)

lemma d_interr_U: "Dom x ⋅ U ∥ Dom y ⋅ U = Dom (x ∥ y) ⋅ U"
  by (metis U_nc U_par_idem cl4 d_conc6 seq_conc_subdistr subset_antisym)

lemma d_meet: "Dom x ⋅ z ∩ Dom y ⋅ z = (Dom x ∩ Dom y) ⋅ z"
  by (simp add: d_meet_distr_var)

lemma cs_hom_meet: "Dom (x ⋅ 1⇩π ∩ y ⋅ 1⇩π) = Dom (x ⋅ 1⇩π) ∩ Dom (y ⋅ 1⇩π)"
  by (metis d_conc6 d_conc_inter dc_prop2 p_subid_par_eq_meet_var)

lemma iso3 [simp]: "Dom (Dom x ⋅ U) = Dom x "
  by simp

lemma iso4 [simp]: "Dom (x ⋅ 1⇩π ∥ U) ⋅ U = x ⋅ 1⇩π ∥ U"
  by (metis cl8_var iso3)

lemma iso3_sharp [simp]: "Dom (Dom (x ∩ NC) ⋅ NC) = Dom (x ∩ NC)"
  by simp

lemma iso4_sharp [simp]: "Dom ((x ∩ NC) ⋅ NC) ⋅ NC = (x ∩ NC) ⋅ NC"
  by simp

subsection ‹Vectors›

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)
  by (smt (z3) SUP_bot case_prod_conv mem_Collect_eq sup_bot_left)

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

lemma U_par_zero [simp]: "{} ⋅ R ∥ U = {}"
  by (simp add: p_prod_comm)

lemma U_par_s_id [simp]: "1⇩σ ⋅ 1⇩π ∥ U = U"
  by auto

lemma U_par_p_id [simp]: "1⇩π ⋅ 1⇩π ∥ U = U"
  by auto

lemma U_par_nc [simp]: "NC ⋅ 1⇩π ∥ U = U"
  by auto


subsection ‹Up-closure and Parikh composition›

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

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

lemma p_id_U: "R ∥ U = {(a,B). ∃A. (a,A) ∈ R ∧ A ⊆ B}"
  by (clarsimp simp: mr_simp) blast

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

lemma upclosed_ext: "R ⊆ R ∥ U"
  by (clarsimp simp: mr_simp) blast

lemma onelem: "R ⋅ S ∥ U ⊆ R ⊗ (S ∥ U)"
  by (auto simp: s_prod_def 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 (clarsimp simp: mr_simp) blast
  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 (clarsimp simp: mr_simp) blast
  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)"
  apply (rule order.antisym)
  by (simp add: p_prod_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)

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

lemma U_nc_par [simp]: "NC ∥ U = NC"
  by (metis c_nc_comp1 c_prod_idr nc_par_idem p_prod_distl sup_idem)

lemma uc_par_meet: "(R ∥ U) ∩ (S ∥ U) = R ∥ U ∥ S ∥ U"
  using p_prod_assoc up_closed_par_is_meet by blast

lemma uc_unc [simp]: "R ∥ U ∥ R ∥ U = R ∥ U"
  using uc_par_meet by auto

lemma uc_interr: "(R ∥ S) ⋅ (T ∥ U) = R ⋅ (T ∥ U) ∥ S ⋅ (T ∥ U)"
  by (simp add: Orderings.order_eq_iff cl4 seq_conc_subdistr up_closed_par_is_meet)

lemma iso5 [simp]: "(R ⋅ 1⇩π ∥ U) ⋅ 1⇩π = R ⋅ 1⇩π"
  by (simp add: c3)

lemma iso6 [simp]: "(R ⋅ 1⇩π ∥ U) ⋅ 1⇩π ∥ U = R ⋅ 1⇩π ∥ U"
  by simp

lemma sv_hom_par: "(R ∥ S) ⋅ U = R ⋅ U ∥ S ⋅ U"
  by (metis U_par_idem uc_interr)

lemma vs_hom_meet: "Dom ((R ⋅ 1⇩π ∥ U) ∩ (S ⋅ 1⇩π ∥ U)) = Dom (R ⋅ 1⇩π ∥ U) ∩ Dom (S ⋅ 1⇩π ∥ U)"
  by (metis d_conc6 d_conc_inter dc_prop2 iso5 up_closed_par_is_meet)

lemma cv_hom_meet: "(R ⋅ 1⇩π ∩ S ⋅ 1⇩π) ∥ U = (R ⋅ 1⇩π ∥ U) ∩ (S ⋅ 1⇩π ∥ U)"
  by (metis U_par_idem p_prod_assoc p_prod_comm p_subid_par_eq_meet_var uc_par_meet)

lemma cv_hom_par [simp]: " R ∥ U ∥ S ∥ U = (R ∥ S) ∥ U"
  by (metis U_par_idem p_prod_assoc p_prod_comm)

lemma vc_hom_meet: "((R ⋅ 1⇩π ∥ U) ∩ (S ⋅ 1⇩π ∥ U)) ⋅ 1⇩π = ((R ⋅ 1⇩π ∥ U) ⋅ 1⇩π) ∩ ((S ⋅ 1⇩π ∥ U) ⋅ 1⇩π)"
  by (metis c4 cl8_var cv_hom_meet iso5 p_subid_par_eq_meet_var)

lemma vc_hom_seq: "((R ⋅ 1⇩π ∥ U) ⋅ (S ⋅ 1⇩π ∥ U)) ⋅ 1⇩π = ((R ⋅ 1⇩π ∥ U) ⋅ 1⇩π) ⋅ ((S ⋅ 1⇩π ∥ U) ⋅ 1⇩π)"
proof -
  have "((R ⋅ 1⇩π ∥ U) ⋅ (S ⋅ 1⇩π ∥ U)) ⋅ 1⇩π = (R ⋅ 1⇩π ∥ U) ⋅ (S ⋅ 1⇩π)"
    by (metis c4 iso5)
  also have "... = R ⋅ 1⇩π ∥ U ⋅ (S ⋅ 1⇩π)"
    by (metis cl8_var d_assoc1)
  also have "... = R ⋅ 1⇩π ∥ (NC ⋅ (S ⋅ 1⇩π) ∪ 1⇩π ⋅ (S ⋅ 1⇩π))"
    by (metis c_nc_comp1 s_prod_distr sup_commute)
  also have "... = R ⋅ 1⇩π ∥ 1⇩π"
    by (metis Un_absorb1 c4 c6 s_prod_p_idl)
  thus ?thesis
    by (simp add: assoc_p_subid calculation)
qed


subsection ‹Nonterminal and terminal multirelations›

definition tau :: "('a,'b) mrel ⇒ ('a,'b) mrel" (‹τ›) where
  "τ R = R ⋅ {}"

definition nu :: "('a,'b) mrel ⇒ ('a,'b) mrel" (‹ν›) where
  "ν R = R ∩ NC"

lemma nc_s [simp]: "ν 1⇩σ = 1⇩σ"
  using nu_def s_le_nc by auto

lemma nc_scomp_closed: "ν R ⋅ ν S ⊆ NC"
  by (simp add: nu_def nc_iff1 p_id_zero zero_assoc3)

lemma nc_scomp_closed_alt [simp]: "ν (ν R ⋅ ν S) = ν R ⋅ ν S"
  by (metis inf.orderE nc_scomp_closed nu_def)

lemma nc_ccomp_closed: "ν R ∥ ν S ⊆ NC"
  unfolding nu_def by (clarsimp simp: mr_simp)

lemma nc_ccomp_closed_alt [simp]: "ν (R ∥ ν S) = R ∥ ν S"
  unfolding nu_def by (clarsimp simp: mr_simp) blast

lemma tarski_prod: "(ν R ⋅ NC) ⋅ (ν S ⋅ NC) = (if ν S = {} then {} else ν R ⋅ NC)"
proof (cases "ν S = {}")
  case True
  show ?thesis
    by (metis True nc_zero nu_def p_id_NC s_prod_zerol zero_assoc3)
next
  case False
  hence a: "NC ⋅ (ν S ⋅ NC) = NC"
    unfolding nu_def by (metis p_id_NC tarski)
  have "(ν R ⋅ NC) ⋅ (ν S ⋅ NC) = (Dom (ν R) ⋅ NC) ⋅ (ν S ⋅ NC)"
    by (simp add: nu_def)
  also have "... = Dom (ν R) ⋅ (NC ⋅ (ν S ⋅ NC))"
    using d_assoc1 by blast
  also have "... = Dom (ν R) ⋅ NC"
    by (simp add: a)
  also have "... = ν R ⋅ NC"
    by (simp add: nu_def)
  finally have "(ν R ⋅ NC) ⋅ (ν S ⋅ NC) = ν R ⋅ NC".
  thus ?thesis
    using False by auto
qed

lemma nc_prod_aux [simp]: "(ν R ⋅ NC) ⋅ NC = ν R ⋅ NC"
  apply (clarsimp simp: mr_simp)
  apply safe
  apply clarsimp
  apply (smt (verit) SUP_bot_conv(1) ex_in_conv)
  apply clarsimp
  by (smt (verit, best) SUP_bot_conv(2) UNIV_I UN_constant)

lemma nc_vec_add_closed: "(ν R ⋅ NC ∪ ν S ⋅ NC) ⋅ NC = ν R ⋅ NC ∪ ν S ⋅ NC"
  by (simp add: s_prod_distr)

lemma nc_vec_par_is_meet: "ν R ⋅ NC ∥ ν S ⋅ NC = ν R ⋅ NC ∩ ν S ⋅ NC"
  by (metis (no_types, lifting) U_nc_par cl11 nu_def p_prod_assoc up_closed_par_is_meet)

lemma nc_vec_meet_closed: "(ν R ⋅ NC ∩ ν S ⋅ NC) ⋅ NC = ν R ⋅ NC ∩ ν S ⋅ NC"
  apply (clarsimp simp: nu_def mr_simp)
  apply safe
  apply (metis SUP_const UN_I ex_in_conv)
  apply (clarsimp, smt (verit) SUP_bot_conv(2) ex_in_conv)
  by (clarsimp, smt (verit, ccfv_threshold) SUP_bot_conv(1) SUP_const UNIV_I all_not_in_conv)

lemma nc_vec_par_closed: "(ν R ⋅ NC ∥ ν S ⋅ NC) ⋅ NC = ν R ⋅ NC ∥ ν S ⋅ NC"
  by (metis U_nc_par nc_prod_aux uc_interr)

lemma nc_vec_seq_closed: "((ν R ⋅ NC) ⋅ (ν S ⋅ NC)) ⋅ NC = (ν R ⋅ NC) ⋅ (ν S ⋅ NC)"
proof (cases "ν S = {}")
  case True thus ?thesis
    by simp
next
  case False thus ?thesis
    by (simp add: tarski_prod)
qed

lemma iso5_sharp [simp]: "(ν R ⋅ 1⇩π ∥ NC) ⋅ 1⇩π = ν R ⋅ 1⇩π"
  by (simp add: c3)

lemma iso6_sharp [simp]: "(ν R ⋅ NC ⋅ 1⇩π) ∥ NC = ν R ⋅ NC"
  by (simp add: c4 nu_def)

lemma nsv_hom_par: "(R ∥ S) ⋅ NC = R ⋅ NC ∥ S ⋅ NC"
  by (simp add: cl4 seq_conc_subdistr subset_antisym)

lemma nvs_hom_meet: "Dom (ν R ⋅ NC ∩ ν S ⋅ NC) = Dom (ν R ⋅ NC) ∩ Dom (ν S ⋅ NC)"
  by (rule antisym) (fastforce simp: nu_def mrd_simp)+

lemma ncv_hom_meet: "R ⋅ 1⇩π ∩ S ⋅ 1⇩π ∥ NC = (R ⋅ 1⇩π ∥ NC) ∩ (S ⋅ 1⇩π ∥ NC)"
  by (metis c4 cl8_var d_exp_ax d_meet d_s_id_inter p_subid_par_eq_meet_var)

lemma ncv_hom_par: "(R ∥ S) ∥ NC = R ∥ NC ∥ S ∥ NC"
  by (metis nc_par_idem p_prod_assoc p_prod_comm)

lemma nvc_hom_meet: "(ν R ⋅ NC ∩ ν S ⋅ NC) ⋅ 1⇩π = (ν R ⋅ NC) ⋅ 1⇩π ∩ (ν S ⋅ NC) ⋅ 1⇩π"
  by (rule antisym) (fastforce simp: nu_def mr_simp)+

lemma tau_int: "τ R ≤ R"
  using p_id_zero tau_def by auto

lemma nu_int: "ν R ≤ R"
  by (simp add: nu_def)

lemma tau_ret [simp]: "τ (τ R) = τ R"
  by (simp add: tau_def)

lemma nu_ret [simp]: "ν (ν R) = ν R"
  by (simp add: nu_def)

lemma tau_iso: "R ≤ S ⟹ τ R ≤ τ S"
  by (simp add: inf.order_iff tau_def x_zero_meet_closed)

lemma nu_iso: "R ≤ S ⟹ ν R ≤ ν S"
  by (metis Int_mono nu_def order_refl)

lemma tau_zero [simp]: "τ {} = {}"
  by (simp add: tau_def)

lemma nu_zero [simp]: "ν {} = {}"
  using nu_def by auto

lemma tau_s [simp]: "τ 1⇩σ = {}"
  by (simp add: tau_def)

lemma tau_c [simp]: "τ 1⇩π = 1⇩π"
  by (simp add: tau_def)

lemma nu_c [simp]: "ν 1⇩π = {}"
  by (simp add: nu_def)

lemma tau_nc [simp]: "τ NC = {}"
  by (metis nc_iff2 order_refl tau_def)

lemma nu_nc [simp]: "ν NC = NC"
  using nu_def by auto

lemma tau_U [simp]: "τ U = 1⇩π"
  by (simp add: tau_def)

lemma nu_U [simp]: "ν U = NC"
  by (simp add: Diff_eq nu_def)

lemma tau_add [simp]: "τ (R ∪ S) = τ R ∪ τ S"
  by (simp add: tau_def x_zero_add_closed)

lemma nu_add [simp]: "ν (R ∪ S) = ν R ∪ ν S"
  by (simp add: Int_Un_distrib2 nu_def)

lemma tau_meet [simp]: "τ (R ∩ S) = τ R ∩ τ S"
  by (simp add: tau_def x_zero_meet_closed)

lemma nu_meet [simp]: "ν (R ∩ S) = ν R ∩ ν S"
  by (simp add: inf_commute inf_left_commute nu_def)

lemma tau_seq: "τ (R ⋅ S) = τ R ∪ ν R ⋅ τ S"
  unfolding nu_def tau_def
  by (metis sup_commute x_y_split zero_assoc3)

lemma tau_par [simp]: "τ (R ∥ S) = τ R ∥ τ S"
  by (metis U_par_zero tau_def uc_interr)

lemma nu_par_aux1: "R ∥ τ S = Dom (τ S) ⋅ R"
  by (metis p_prod_comm tau_def x_zero_prop)

lemma nu_par_aux3 [simp]: "ν (ν R ∥ τ S) = ν R ∥ τ S"
  by (metis nc_ccomp_closed_alt p_prod_comm)

lemma nu_par_aux4 [simp]: "ν (τ R ∥ τ S) = {}"
  by (metis nu_def tau_def tau_par zero_nc)

lemma nu_par: "ν (R ∥ S) = Dom (τ R) ⋅ ν S ∪ Dom (τ S) ⋅ ν R ∪ (ν R ∥ ν S)"
  apply (rule antisym)
  apply (fastforce simp: mrd_simp nu_def tau_def)
  by (auto simp: mrd_simp nu_def tau_def)

lemma sprod_tau_nu: "R ⋅ S = τ R ∪ ν R ⋅ S"
  by (metis nu_def sup_commute tau_def x_y_split)

lemma pprod_tau_nu: "R ∥ S = (ν R ∥ ν S) ∪ Dom (τ R) ⋅ ν S ∪ Dom (τ S) ⋅ ν R ∪ (τ R ∥ τ S)"
  by (smt (verit) nu_def nu_par sup_assoc sup_left_commute tau_def tau_par x_split_var)

lemma tau_idem [simp]: "τ R ⋅ τ R = τ R"
  by (simp add: tau_def)

lemma tau_interr: "(R ∥ S) ⋅ τ T = R ⋅ τ T ∥ S ⋅ τ T"
  by (simp add: tau_def cl4 seq_conc_subdistr subset_antisym)

lemma tau_le_c: "τ R ≤ 1⇩π"
  by (simp add: tau_def x_zero_le_c)

lemma c_le_tauc: "1⇩π ≤ τ 1⇩π"
  by simp

lemma x_alpha_tau [simp]: "ν R ∪ τ R = R"
  by (simp add: nu_def tau_def)

lemma alpha_tau_zero [simp]: "ν (τ R) = {}"
  by (simp add: nu_def tau_def)

lemma tau_alpha_zero [simp]: "τ (ν R) = {}"
  by (simp add: nu_def tau_def)

lemma sprod_tau_nu_var [simp]: "ν (ν R ⋅ S) = ν (R ⋅ S)"
  by (metis nu_add nu_def nu_ret x_y_split zero_nc)

lemma tau_s_prod [simp]: "τ (R ⋅ S) = R ⋅ τ S"
  by (simp add: tau_def zero_assoc3)

lemma alpha_fp: "ν R = R ⟷ R ⋅ {} = {}"
  by (metis inf.orderE nc_iff2 nc_zero nu_def)

lemma p_prod_tau_alpha: "R ∥ S = (R ∥ ν S) ∪ (ν R ∥ S) ∪ (τ R ∥ τ S)"
  by (smt (verit) p_prod_comm p_prod_distl sup.idem sup_assoc sup_commute x_alpha_tau)

lemma p_prod_tau_alpha_var: "R ∥ S = (R ∥ ν S) ∪ (ν R ∥ S) ∪ τ (R ∥ S)"
  using p_prod_tau_alpha tau_par by blast

lemma alpha_par: "ν (R ∥ S) = (ν R ∥ S) ∪ (R ∥ ν S)"
  by (metis alpha_tau_zero nc_ccomp_closed_alt nu_add p_prod_comm p_prod_tau_alpha sup_bot_right tau_par)

lemma alpha_tau [simp]: "ν (R ⋅ τ S) = {}"
  by (metis alpha_tau_zero tau_s_prod)

lemma nu_par_prop: "ν R = R ⟹ ν (R ∥ S) = R ∥ S"
  by (metis nc_ccomp_closed_alt p_prod_comm)

lemma tau_seq_prop: "τ R = R ⟹ R ⋅ S = R"
  by (metis cl6 tau_def)

lemma tau_seq_prop2: "τ R = R ⟹ τ (R ⋅ S) = R ⋅ S"
  by (metis cl6 tau_def)

lemma d_nu: "ν (Dom R ⋅ S) = Dom R ⋅ ν S"
  by (auto simp: nu_def mrd_simp)

lemma nu_ideal1: "ν R = R ⟹ S ≤ R ⟹ ν S = S"
  unfolding nu_def by blast

lemma tau_ideal1: "τ R = R ⟹ S ≤ R ⟹ τ S = S"
  by (metis dual_order.trans p_subid_iff_var tau_def)

lemma nu_ideal2: "ν R = R ⟹ ν S = S ⟹ ν (R ∪ S) = R ∪ S"
  by simp

lemma tau_ideal2: "τ R = R ⟹ τ S = S ⟹ τ (R ∪ S) = R ∪ S"
  by simp

lemma tau_add_precong: "τ R ≤ τ S ⟹ τ (R ∪ T) ≤ τ (S ∪ T)"
  by auto

lemma tau_meet_precong: "τ R ≤ τ S ⟹ τ (R ∩ T) ≤ τ (S ∩ T)"
  by force

lemma tau_par_precong: "τ R ≤ τ S ⟹ τ (R ∥ T) ≤ τ (S ∥ T)"
  by (simp add: p_prod_isol)

lemma tau_seq_precongl: "τ R ≤ τ S ⟹ τ (T ⋅ R) ≤ τ (T ⋅ S)"
  by (simp add: s_prod_isor)

lemma nu_add_precong: "ν R ≤ ν S ⟹ ν (R ∪ T) ≤ ν (S ∪ T)"
  by auto

lemma nu_meet_precong: "ν R ≤ ν S ⟹ ν (R ∩ T) ≤ ν (S ∩ T)"
  by force

lemma nu_seq_precongr: "ν R ≤ ν S ⟹ ν (R ⋅ T) ≤ ν (S ⋅ T)"
  by (metis nu_iso s_prod_isol sprod_tau_nu_var)

definition
  "tcg R S = (τ R ≤ τ S ∧ τ S ≤ τ R)"

definition
  "ncg R S = (ν R ≤ ν S ∧ ν S ≤ ν R)"

lemma tcg_refl: "tcg R R"
  by (simp add: tcg_def)

lemma tcg_trans: "tcg R S ⟹ tcg S T ⟹ tcg R T"
  by (meson subset_trans tcg_def)

lemma tcg_sym: "tcg R S ⟹ tcg S R"
  by (simp add: tcg_def)

lemma ncg_refl: "ncg R R"
  using ncg_def by blast

lemma ncg_trans: "ncg R S ⟹ ncg S T ⟹ ncg R T"
  by (meson ncg_def order_trans)

lemma ncg_sym: "ncg R S ⟹ ncg S R"
  by (simp add: ncg_def)

lemma tcg_alt: "tcg R S = (τ R = τ S)"
  using tcg_def by auto

lemma ncg_alt: "ncg R S = (ν R = ν S)"
  by (simp add: Orderings.order_eq_iff ncg_def)

lemma tcg_add: "τ R = τ S ⟹ τ (R ∪ T) = τ (S ∪ T)"
  by simp

lemma tcg_meet: "τ R = τ S ⟹ τ (R ∩ T) = τ (S ∩ T)"
  by simp

lemma tcg_par: "τ R = τ S ⟹ τ (R ∥ T) = τ (S ∥ T)"
  by simp

lemma tcg_seql: "τ R = τ S ⟹ τ (T ⋅ R) = τ (T ⋅ S)"
  by simp

lemma ncg_add: "ν R = ν S ⟹ ν (R ∪ T) = ν (S ∪ T)"
  by simp

lemma ncg_meet: "ν R = ν S ⟹ ν (R ∩ T) = ν (S ∩ T)"
  by simp

lemma ncg_seqr: "ν R = ν S ⟹ ν (R ⋅ T) = ν (S ⋅ T)"
  by (metis sprod_tau_nu_var)


subsection ‹Powers›

primrec p_power :: "('a,'a) mrel ⇒ nat ⇒ ('a,'a) mrel" where
  "p_power R 0       = 1⇩σ" |
  "p_power R (Suc n) = R ⋅ p_power R n"

primrec power_rd :: "('a,'a) mrel ⇒ nat ⇒ ('a,'a) mrel" where
  "power_rd R 0       = {}" |
  "power_rd R (Suc n) = 1⇩σ ∪ R ⋅ power_rd R n"

primrec power_sq :: "('a,'a) mrel ⇒ nat ⇒ ('a,'a) mrel" where
  "power_sq R 0       = 1⇩σ" |
  "power_sq R (Suc n) = 1⇩σ ∪ R ⋅ power_sq R n"

lemma power_rd_chain: "power_rd R n ≤ power_rd R (n + 1)"
  apply (induct n)
  apply simp
  by (smt (verit, best) Suc_eq_plus1 Un_subset_iff le_iff_sup power_rd.simps(2) s_prod_subdistl subsetI)

lemma power_sq_chain: "power_sq R n ≤ power_sq R (n + 1)"
  apply (induct n)
  apply clarsimp
  by (smt (verit, ccfv_SIG) UnCI Un_subset_iff add.commute le_iff_sup plus_1_eq_Suc power_sq.simps(2) s_prod_subdistl subsetI)

lemma pow_chain: "p_power (1⇩σ ∪ R) n ≤ p_power (1⇩σ ∪ R) (n + 1)"
  apply (induct n)
  apply simp
  by (simp add: s_prod_isor)

lemma pow_prop: "p_power (1⇩σ ∪ R) (n + 1) = 1⇩σ ∪ R ⋅ p_power (1⇩σ ∪ R) n"
  apply (induct n)
  apply simp
  by (smt (verit, best) add.commute p_power.simps(2) plus_1_eq_Suc s_prod_distr s_prod_idl s_prod_subdistl subset_antisym sup.commute sup.left_commute sup.right_idem sup_ge1)

lemma power_rd_le_sq: "power_rd R n ≤ power_sq R n"
  apply (induct n)
  apply simp
  by (smt (verit, best) UnCI UnE le_iff_sup power_rd.simps(2) power_sq.simps(2) s_prod_subdistl subsetI)

lemma power_sq_le_rd: "power_sq R n ≤ power_rd R (Suc n)"
  apply (induct n)
  apply simp
  by (smt (verit, del_insts) UnCI UnE power_rd.simps(2) power_sq.simps(2) s_prod_subdistl subsetI sup.absorb_iff1)

lemma power_sq_power: "power_sq R n = p_power (1⇩σ ∪ R) n"
  apply (induct n)
  apply simp
  using pow_prop by auto


subsection ‹Star›

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)

definition star :: "('a,'a) mrel ⇒ ('a,'a) mrel" where
  "star R = lfp (λX. s_id ∪ R ⋅ X)"

lemma star_unfold: "1⇩σ ∪ R ⋅ star R ≤ star R"
  unfolding star_def using iso_prop lfp_unfold by blast

lemma star_induct: "1⇩σ ∪ R ⋅ S ≤ S ⟹ star R ≤ S"
  unfolding star_def by (meson lfp_lowerbound)

lemma star_refl: "1⇩σ ≤ star R"
  using star_unfold by auto

lemma star_unfold_part: "R ⋅ star R ≤ star R"
  using star_unfold by auto

lemma star_ext_aux: "R ≤ R ⋅ star R"
  by (metis s_prod_idr s_prod_isor star_refl)

lemma star_ext: "R ≤ star R"
  using star_ext_aux star_unfold_part by blast

lemma star_co_trans: "star R ≤ star R ⋅ star R"
  by (metis s_prod_idr s_prod_isor star_refl)

lemma star_iso: "R ≤ S ⟹ star R ≤ star S"
  by (metis (no_types, lifting) le_sup_iff s_prod_distr star_induct star_refl star_unfold_part subset_Un_eq)

lemma star_unfold_eq [simp]: "1⇩σ ∪ R ⋅ star R = star R"
  by (metis iso_prop lfp_unfold star_def)

lemma nu_star1:
  assumes "⋀(R::('a,'a) mrel) (S::('a,'a) mrel) (T::('a,'a) mrel). R ⋅ (S ⋅ T) = (R ⋅ S) ⋅ T"
  shows "star (R::('a,'a) mrel) ≤ star (ν R) ⋅ (1⇩σ ∪ τ R)"
  by (smt (verit, ccfv_threshold) assms s_prod_distr s_prod_idl sprod_tau_nu star_induct star_unfold_eq subsetI sup_assoc)

lemma nu_star2:
  assumes "⋀(R::('a,'a) mrel). star R ⋅ star R ≤ star R"
  shows "star (ν (R::('a,'a) mrel)) ⋅ (1⇩σ ∪ τ R) ≤ star R"
  by (smt (verit) assms le_sup_iff nu_int s_prod_isol s_prod_isor star_ext star_refl star_iso subset_trans tau_int)

lemma nu_star:
  assumes "⋀(R::('a,'a) mrel). star R ⋅ star R ≤ star R"
  and "⋀(R::('a,'a) mrel) (S::('a,'a) mrel) (T::('a,'a) mrel). R ⋅ (S ⋅ T) = (R ⋅ S) ⋅ T"
  shows "star (ν (R::('a,'a) mrel)) ⋅ (1⇩σ ∪ τ R) = star R"
  using assms nu_star1 nu_star2 by blast

lemma tau_star: "star (τ R) = 1⇩σ ∪ τ R"
  by (metis cl6 tau_def star_unfold_eq)

lemma tau_star_var:
  assumes "⋀(R::('a,'a) mrel) (S::('a,'a) mrel) (T::('a,'a) mrel). R ⋅ (S ⋅ T) = (R ⋅ S) ⋅ T"
  and "⋀(R::('a,'a) mrel). star R ⋅ star R ≤ star R"
  shows "τ (star (R::('a,'a) mrel)) = star (ν R) ⋅ τ R"
  by (metis (mono_tags, lifting) assms nu_star s_prod_distr s_prod_zerol sup_bot_left tau_def tau_s)

lemma nu_star_sub: "star (ν R) ≤ ν (star R)"
proof -
  have a: "1⇩σ ⊆ star R"
    by (simp add: star_refl)
  have b: "(R ∩ NC) ⋅ (star R ∩ NC) ⊆ star R"
    by (metis nu_def nu_int s_prod_isol s_prod_isor star_unfold_part subset_trans)
  have c: "1⇩σ ⊆ NC"
    by (simp add: s_le_nc)
  have "(R ∩ NC) ⋅ (star R ∩ NC) ⊆ NC"
    by (metis nc_scomp_closed nu_def)
  thus ?thesis
    by (metis Un_least a b c le_infI nu_def star_induct)
qed

lemma nu_star_nu [simp]: "ν (star (ν R)) = star (ν R)"
  using nu_int nu_star_sub by fastforce

lemma nu_star_tau [simp]: "ν (star (τ R)) = 1⇩σ"
  using tau_star by (metis alpha_tau_zero nu_add tau_s x_alpha_tau)

lemma tau_star_tau [simp]: "τ (star (τ R)) = τ R"
  by (simp add: tau_star)

lemma tau_star_nu [simp]: "τ (star (ν R)) = {}"
  using alpha_fp tau_def nu_star_nu by metis

lemma d_star_unfold [simp]: "Dom S ∪ Dom (R ⋅ Dom (star R ⋅ S)) = Dom (star R ⋅ S)"
proof -
  have "Dom S ∪ Dom (R ⋅ Dom (star R ⋅ S)) = Dom S ∪ Dom (R ⋅ (star R ⋅ Dom S))"
    by (metis d_loc_ax)
  also have "... = Dom (1⇩σ ⋅ Dom S ∪ (R ⋅ (star R ⋅ Dom S)))"
    by (simp add: d_add_ax)
  also have "... = Dom (1⇩σ ⋅ Dom S ∪ (R ⋅ star R) ⋅ Dom S)"
    by (metis d_comm_ax d_s_id_inter d_s_id_prop s_prod_idl test_assoc3)
  moreover have "... = Dom ((1⇩σ ∪ R ⋅ star R) ⋅ Dom S)"
    using s_prod_distr by metis
  ultimately show ?thesis
    by simp
qed

lemma d_star_sim1:
  assumes "⋀R S T. Dom (T::('a,'b) mrel) ∪ (R::('a,'a) mrel) ⋅ (S::('a,'a) mrel) ≤ S ⟹ star R ⋅ Dom T ≤ S"
  shows "(R::('a,'a) mrel) ⋅ Dom (T::('a,'b) mrel) ≤ Dom T ⋅ (S::('a,'a) mrel) ⟹ star R ⋅ Dom T ≤ Dom T ⋅ star S"
proof -
  fix R S::"('a,'a) mrel" and T ::"('a,'b) mrel"
  assume a: "R ⋅ Dom T ≤ Dom T ⋅ S"
  hence "(R ⋅ Dom T) ⋅ star S ≤ (Dom T ⋅ S) ⋅ star S"
    by (simp add: s_prod_isol)
  hence b: "R ⋅ (Dom T ⋅ star S) ≤ Dom T ⋅ (S ⋅ star S)"
    by (metis d_assoc1 d_s_id_ax inf.order_iff test_assoc1)
  hence "R ⋅ (Dom T ⋅ star S) ≤ Dom T ⋅ star S"
    by (meson order_trans s_prod_isor star_unfold_part)
  hence "Dom T ∪ R ⋅ (Dom T ⋅ star S) ≤ Dom T ⋅ star S"
    by (metis le_supI s_prod_idr s_prod_isor star_refl)
  thus "star R ⋅ Dom T ≤ Dom T ⋅ star S"
    using assms by presburger
qed

lemma d_star_induct:
  assumes "⋀R S T. Dom (T::('a,'b) mrel) ∪ (R::('a,'a) mrel) ⋅ (S::('a,'a) mrel) ≤ S ⟹ star R ⋅ Dom T ≤ S"
  shows "Dom ((R::('a,'a) mrel) ⋅ (S::('a,'a) mrel)) ≤ Dom S ⟹ Dom (star R ⋅ S) ≤ Dom S"
  by (metis assms d_star_sim1 dc_prop2 demod1 demod2)


subsection ‹Omega›

definition omega :: "('a,'a) mrel ⇒ ('a,'a) mrel" where
  "omega R ≡ gfp (λX. R ⋅ X)"

lemma om_unfold: "omega R ≤ R ⋅ omega R"
  unfolding omega_def
  by (metis (no_types, lifting) gfp_least gfp_upperbound order_trans s_prod_isor)

lemma om_coinduct: "S ≤ R ⋅ S ⟹ S ≤ omega R"
  unfolding omega_def by (simp add: gfp_upperbound omega_def)

lemma om_unfold_eq [simp]: "R ⋅ omega R = omega R"
  by (rule antisym) (auto simp: om_coinduct om_unfold s_prod_isor)

lemma om_iso: "R ≤ S ⟹ omega R ≤ omega S"
  by (metis om_coinduct s_prod_isol om_unfold_eq)

lemma zero_om [simp]: "omega {} = {}"
  using om_unfold_eq s_prod_zerol by blast

lemma s_id_om [simp]: "omega 1⇩σ = U"
  by (simp add: U_def eq_iff om_coinduct)

lemma p_id_om [simp]: "omega 1⇩π = 1⇩π"
  using om_unfold_eq s_prod_p_idl by blast

lemma nc_om [simp]: "omega NC = U"
  by (metis dual_order.refl nc_U om_coinduct s_id_om s_prod_idl subset_antisym)

lemma U_om [simp]: "omega U = U"
  by (metis U_U dual_order.refl om_coinduct s_id_om s_prod_idl subset_antisym)

lemma tau_om1: "τ R ≤ τ (omega R)"
  by (metis om_unfold_eq order_refl sup.boundedE tau_seq)

lemma tau_om2 [simp]: "omega (τ R) = τ R"
  by (metis cl6 om_unfold_eq tau_def)

lemma tau_om3: "omega (τ R) ≤ τ (omega R)"
  by (simp add: tau_om1)

lemma om_nu_tau: "omega (ν R) ∪ star (ν R) ⋅ τ R ≤ omega R"
proof -
  have "omega (ν R) ∪ star (ν R) ⋅ τ R = omega (ν R) ∪ (1⇩σ ∪ ν R ⋅ star (ν R)) ⋅ τ R"
    by auto
  also have "... = omega (ν R) ∪ τ R ∪ ν R ⋅ star (ν R) ⋅ τ R"
    using s_prod_distr s_prod_idl by blast
  also have "... = τ R ∪ ν R ⋅ omega (ν R) ∪ ν R ⋅ (star (ν R) ⋅ τ R)"
    by (simp add: cl5 sup_commute tau_def)
  also have "... ≤ τ R ∪ ν R ⋅ (omega (ν R) ∪ star (ν R) ⋅ τ R)"
    by (smt (verit) Un_subset_iff s_prod_isor sup.cobounded2 sup.coboundedI2 sup_commute)
  also have "... = R ⋅ (omega (ν R) ∪ star (ν R) ⋅ τ R)"
    using sprod_tau_nu by blast
  finally show ?thesis
    using om_coinduct by blast
qed

end