Theory Multirelations

theory Multirelations

imports Power_Allegories_Multirelations

begin

lemma nonempty_set_card:
  assumes "finite S"
  shows "S  {}  card S  1"
  using assms card_0_eq by fastforce

no_notation one_class.one ("1")
no_notation times_class.times (infixl "*" 70)

no_notation rel_fdia ("(|__)" [61,81] 82)
no_notation rel_bdia ("(_|_)" [61,81] 82)
no_notation rel_fbox ("(|_]_)" [61,81] 82)
no_notation rel_bbox ("([_|_)" [61,81] 82)

declare s_prod_pa_def [mr_simp]

notation s_prod (infixl "*" 70)
notation s_id ("1")

lemma sp_oi_subdist:
  "(P  Q) * (R  S)  P * R"
  unfolding s_prod_def by blast

lemma sp_oi_subdist_2:
  "(P  Q) * (R  S)  (P * R)  (Q * S)"
  unfolding s_prod_def by blast

section ‹Inner Structure›

subsection ‹Inner union, inner intersection and inner complement›

abbreviation "inner_union" (infixl "∪∪" 65)
  where "inner_union  p_prod"

definition inner_intersection :: "('a,'b) mrel  ('a,'b) mrel  ('a,'b) mrel" (infixl "∩∩" 65) where
  "R ∩∩ S  { (a,B) . C D . B = C  D  (a,C)  R  (a,D)  S }"

definition inner_complement :: "('a,'b) mrel  ('a,'b) mrel" (" _" [80] 80) where
  "R  { (a,B) . (a,-B)  R }"

abbreviation "iu_unit" ("1")
  where "1  p_id"

definition ii_unit :: "('a,'a) mrel" ("1")
  where "1  { (a,UNIV) | a . True }"

declare inner_intersection_def [mr_simp] inner_complement_def [mr_simp] ii_unit_def [mr_simp]

lemma iu_assoc:
  "(R ∪∪ S) ∪∪ T = R ∪∪ (S ∪∪ T)"
  by (simp add: p_prod_assoc)

lemma iu_commute:
  "R ∪∪ S = S ∪∪ R"
  by (simp add: p_prod_comm)

lemma iu_unit:
  "R ∪∪ 1 = R"
  by simp

lemma ii_assoc:
  "(R ∩∩ S) ∩∩ T = R ∩∩ (S ∩∩ T)"
  apply (clarsimp simp: mr_simp)
  by (metis (no_types, opaque_lifting) semilattice_inf_class.inf_assoc)

lemma ii_commute:
  "R ∩∩ S = S ∩∩ R"
  by (auto simp: mr_simp)

lemma ii_unit [simp]:
  "R ∩∩ 1 = R"
  by (simp add: mr_simp)

lemma pa_ic:
  "(R  S) = R  S"
  by (clarsimp simp: mr_simp)

lemma ic_involutive [simp]:
  "R = R"
  by (simp add: mr_simp)

lemma ic_injective:
  "R = S  R = S"
  by (metis ic_involutive)

lemma ic_antidist_iu:
  "(R ∪∪ S) = R ∩∩ S"
  apply (clarsimp simp: mr_simp)
  by (metis (no_types, opaque_lifting) compl_sup double_compl)

lemma ic_antidist_ii:
  "(R ∩∩ S) = R ∪∪ S"
  by (metis ic_antidist_iu ic_involutive)

lemma ic_iu_unit [simp]:
  "1 = 1"
  unfolding ii_unit_def p_id_def inner_complement_def by force

lemma ic_ii_unit [simp]:
  "1 = 1"
  by (metis ic_involutive ic_iu_unit)

lemma ii_unit_split_iu [simp]:
  "1 ∪∪ 1 = 1"
  by (force simp: mr_simp)

lemma aux_1:
  "B = {a}  D  -D = {a}  B = {}"
  by auto

lemma iu_unit_split_ii [simp]:
  "1 ∩∩ 1 = 1"
  by (metis ic_antidist_iu ic_ii_unit ic_involutive ii_commute ii_unit_split_iu)

lemma iu_right_dist_ou:
  "(R  S) ∪∪ T = (R ∪∪ T)  (S ∪∪ T)"
  unfolding p_prod_def by auto

lemma ii_right_dist_ou:
  "(R  S) ∩∩ T = (R ∩∩ T)  (S ∩∩ T)"
  by (auto simp: mr_simp)

lemma iu_left_isotone:
  "R  S  R ∪∪ T  S ∪∪ T"
  by (metis iu_right_dist_ou subset_Un_eq)

lemma iu_right_isotone:
  "R  S  T ∪∪ R  T ∪∪ S"
  by (simp add: iu_commute iu_left_isotone)

lemma iu_isotone:
  "R  S  P  Q  R ∪∪ P  S ∪∪ Q"
  by (meson dual_order.trans iu_left_isotone iu_right_isotone)

lemma ii_left_isotone:
  "R  S  R ∩∩ T  S ∩∩ T"
  by (metis ii_right_dist_ou subset_Un_eq)

lemma ii_right_isotone:
  "R  S  T ∩∩ R  T ∩∩ S"
  by (simp add: ii_commute ii_left_isotone)

lemma ii_isotone:
  "R  S  P  Q  R ∩∩ P  S ∩∩ Q"
  by (meson ii_left_isotone ii_right_isotone order_trans)

lemma iu_right_subdist_ii:
  "(R ∩∩ S) ∪∪ T  (R ∪∪ T) ∩∩ (S ∪∪ T)"
  apply (clarsimp simp: mr_simp)
  by (metis sup_inf_distrib2)

lemma ii_right_subdist_iu:
  "(R ∪∪ S) ∩∩ T  (R ∩∩ T) ∪∪ (S ∩∩ T)"
  apply (clarsimp simp: mr_simp)
  by (metis inf_sup_distrib2)

lemma ic_isotone:
  "R  S  R  S"
  by (simp add: inner_complement_def subset_eq)

lemma ic_bot [simp]:
  "{} = {}"
  by (simp add: mr_simp)

lemma ic_top [simp]:
  "U = U"
  by (auto simp: mr_simp)

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

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

lemma ic_dist_oc:
  "-R = -(R)"
  by (auto simp: mr_simp)

lemma ii_sub_idempotent:
  "R  R ∩∩ R"
  unfolding inner_intersection_def by force

definition inner_Union :: "('i  ('a,'b) mrel)  'i set  ('a,'b) mrel" ("⋃⋃_|_" [80,80] 80) where
  "⋃⋃X|I  { (a,B) . f . B = (iI . f i)  (iI . (a,f i)  X i) }"

definition inner_Intersection :: "('i  ('a,'b) mrel)  'i set  ('a,'b) mrel" ("⋂⋂_|_" [80,80] 80) where
  "⋂⋂X|I  { (a,B) . f . B = (iI . f i)  (iI . (a,f i)  X i) }"

declare inner_Union_def [mr_simp] inner_Intersection_def [mr_simp]

lemma iU_empty:
  "⋃⋃X|{} = 1"
  by (auto simp: mr_simp)

lemma iI_empty:
  "⋂⋂X|{} = 1"
  by (auto simp: mr_simp)

lemma ic_antidist_iU:
  "⋃⋃X|I = ⋂⋂(inner_complement o X)|I"
  apply (rule antisym)
   apply (clarsimp simp: mr_simp)
   apply (metis (mono_tags, lifting) Compl_UN double_compl)
  by (clarsimp simp: mr_simp) blast

lemma ic_antidist_iI:
  "⋂⋂X|I = ⋃⋃(inner_complement o X)|I"
  apply (rule antisym)
   apply (clarsimp simp: mr_simp)
   apply (metis Compl_INT double_complement)
  by (clarsimp simp: mr_simp) blast

lemma iu_right_dist_oU:
  "X ∪∪ T = (RX . R ∪∪ T)"
  by (clarsimp simp: mr_simp) blast

lemma ii_right_dist_oU:
  "X ∩∩ T = (RX . R ∩∩ T)"
  by (clarsimp simp: mr_simp) blast

lemma iu_right_subdist_iI:
  "⋂⋂X|I ∪∪ T  ⋂⋂(λi . X i ∪∪ T)|I"
  apply (clarsimp simp: mr_simp)
  by (metis INT_simps(6))

lemma ii_right_subdist_iU:
  "⋃⋃X|I ∩∩ T  ⋃⋃(λi . X i ∩∩ T)|I"
  by (clarsimp simp: mr_simp, metis UN_extend_simps(4))

lemma ic_dist_oU:
  "X = (inner_complement ` X)"
  by (auto simp: mr_simp)

lemma ic_dist_oI:
  "X = (inner_complement ` X)"
  by (auto simp: mr_simp)

lemma sp_left_subdist_iU:
  "R * (⋃⋃X|I)  ⋃⋃(λi . R * X i)|I"
  apply (clarsimp simp: mr_simp)
  subgoal for a B f proof -
    assume 1: "(a,B)  R"
    assume "bB . g . f b = (g ` I)  (iI . (b,g i)  X i)"
    from this obtain g where 2: "bB . f b = (g b ` I)  (iI . (b,g b i)  X i)"
      by metis
    hence 3: "(f ` B) = (bB . (g b ` I))"
      by (meson SUP_cong)
    let ?h = "λi . bB . g b i"
    have "(f ` B) = (?h ` I)  (iI . B . (a,B)  R  (f . (bB . (b,f b)  X i)  ?h i = (f ` B)))"
      using 1 2 3 by (metis SUP_commute)
    thus ?thesis
      by auto
  qed
  done

lemma sp_right_subdist_iU:
  "(⋃⋃X|I) * R  ⋃⋃(λi . X i * R)|I"
  by (clarsimp simp: mr_simp, blast)

lemma sp_right_dist_iU:
  assumes "J::'a set . J  {}  (⋃⋃(λj . R)|J)  R"
  shows "(⋃⋃X|I) * R = ⋃⋃(λi . X i * R)|(I::'a set)"
  apply (rule antisym)
  using sp_right_subdist_iU apply blast
  apply (clarsimp simp: mr_simp)
  subgoal for a f proof -
    assume "iI . B . (a,B)  X i  (g . (bB . (b,g b)  R)  f i = (g ` B))"
    from this obtain B g where 1: "iI . (a,B i)  X i  (bB i . (b,g i b)  R)  f i = (g i ` B i)"
      by metis
    let ?B = "(B ` I)"
    let ?g = "λb . { g i b | i . iI  b  B i }"
    have "b?B . (b,?g b)  R"
    proof (rule ballI)
      fix b
      let ?I = "{ i | i . iI  b  B i }"
      assume 2: "b  (B ` I)"
      have "(b,?g b)  ⋃⋃(λj . R)|?I"
        apply (clarsimp simp: mr_simp)
        apply (rule exI[of _ "λi . g i b"])
        using 1 by blast
      thus "(b,?g b)  R"
        using 2 by (smt (verit) assms UN_E empty_Collect_eq subset_iff)
    qed
    hence "?B = (B ` I)  (iI . (a,B i)  X i)  (b?B . (b,?g b)  R)  (f ` I) = (?g ` ?B)"
      using 1 by auto
    thus "B . (f . B = (f ` I)  (iI . (a,f i)  X i))  (g . (bB . (b,g b)  R)  (f ` I) = (g ` B))"
      by (metis (no_types, lifting))
  qed
  done

subsection ‹Dual›

abbreviation dual :: "('a,'b) mrel  ('a,'b) mrel" ("_d" [100] 100)
  where "Rd  -R"

lemma dual:
  "Rd = { (a,B) . (a,-B)  R }"
  by (simp add: inner_complement_def)

declare dual [mr_simp]

lemma dual_antitone:
  "R  S  Sd  Rd"
  by (simp add: ic_isotone)

lemma ic_oc_dual:
  "R = -Rd"
  by (simp add: ic_dist_oc)

lemma dual_involutive [simp]:
  "Rdd = R"
  by (simp add: ic_dist_oc)

lemma dual_antidist_ou:
  "(R  S)d = Rd  Sd"
  by (simp add: ic_dist_oi)

lemma dual_antidist_oi:
  "(R  S)d = Rd  Sd"
  by (simp add: ic_dist_ou)

lemma dual_dist_oc:
  "(-R)d = -Rd"
  by (fact ic_dist_oc)

lemma dual_dist_ic:
  "(R)d = Rd"
  by (simp add: ic_dist_oc)

lemma dual_antidist_oU:
  "(X)d = (dual ` X)"
  by (simp add: ic_dist_oI uminus_Sup)

lemma dual_antidist_oI:
  "(X)d = (dual ` X)"
  by (simp add: ic_dist_oU uminus_Inf)

subsection ‹Co-composition›

definition co_prod :: "('a,'b) mrel  ('b,'c) mrel  ('a,'c) mrel" (infixl "" 70) where
  "R  S  { (a,C) . B . (a,B)  R  (f . (b  B . (b,f b)  S)  C = { f b | b . b  B }) }"

lemma co_prod_im:
  "R  S = { (a,C) . B . (a,B)  R  (f . (b  B . (b,f b)  S)  C = ((λx . f x) ` B)) }"
  by (auto simp: co_prod_def)

lemma co_prod_iff:
  "(a,C)  (R  S)  (B . (a,B)  R  (f . (b  B . (b,f b)  S)  C = { f b | b . b  B }))"
  by (unfold co_prod_im, auto)

declare co_prod_im [mr_simp]

lemma co_prod:
  "R  S = (R * S)"
  apply (clarsimp simp: mr_simp)
  by (smt (verit) Collect_cong Compl_INT Compl_UN case_prodI2 double_complement old.prod.case)

lemma cp_left_isotone:
  "R  S  R  T  S  T"
  by (simp add: co_prod ic_isotone s_prod_isol)

lemma cp_right_isotone:
  "R  S  T  R  T  S"
  by (smt (verit) co_prod_iff in_mono subrelI)

lemma cp_isotone:
  "R  S  P  Q  R  P  S  Q"
  by (meson cp_left_isotone cp_right_isotone order_trans)

lemma ic_dist_cp:
  "(R  S) = R * S"
  by (simp add: co_prod)

lemma ic_dist_sp:
  "(R * S) = R  S"
  by (simp add: co_prod)

lemma ic_cp_ic_unit:
  "R = R  1"
  by (simp add: co_prod)

lemma cp_left_zero [simp]:
  "{}  R = {}"
  by (simp add: co_prod_im)

lemma cp_left_unit [simp]:
  "1  R = R"
  by (simp add: co_prod)

lemma cp_ic_unit [simp]:
  "1  1 = 1"
  using ic_cp_ic_unit ic_involutive by blast

lemma cp_right_dist_ou:
  "(R  S)  T = (R  T)  (S  T)"
  by (simp add: co_prod ic_dist_ou s_prod_distr)

lemma cp_left_iu_unit [simp]:
  "1  R = 1"
  by (simp add: co_prod)

lemma cp_right_ii_unit:
  "R  1  R ∪∪ R"
  apply (clarsimp simp: mr_simp)
  by (metis double_compl sup_compl_top)

lemma sp_right_iu_unit:
  "R * 1  R ∩∩ R"
  apply (clarsimp simp: mr_simp)
  by (metis Compl_disjoint double_complement)

lemma cp_left_subdist_ii:
  "R  (S ∩∩ T)  (R  S) ∩∩ (R  T)"
  by (metis cl3 co_prod ic_antidist_ii ic_antidist_iu ic_isotone)

lemma cp_right_subantidist_iu:
  "(R ∪∪ S)  T  (R  T) ∩∩ (S  T)"
  by (metis co_prod ic_antidist_iu ic_isotone seq_conc_subdistr)

lemma cp_right_antidist_iu:
  assumes "T ∩∩ T  T"
  shows "(R ∪∪ S)  T = (R  T) ∩∩ (S  T)"
  by (smt (verit) assms cl4 co_prod cp_right_subantidist_iu ic_antidist_ii ic_involutive ic_isotone subset_antisym)

lemma cp_right_dist_oU:
  "X  T = (RX . R  T)"
  by (auto simp: mr_simp)

lemma cp_left_subdist_iI:
  "R  (⋂⋂X|I)  ⋂⋂(λi . R  X i)|I"
proof -
  have "R  (⋂⋂X|I) = (R * (⋃⋃(inner_complement o X)|I))"
    by (simp add: co_prod ic_antidist_iI)
  also have "...  (⋃⋃(λi . R * (X i))|I)"
    apply (rule ic_isotone)
    using sp_left_subdist_iU by force
  also have "... = ⋂⋂(λi . R  X i)|I"
    apply (subst ic_antidist_iU)
    by (metis co_prod comp_apply)
  finally show ?thesis
    .
qed

lemma cp_right_subantidist_iU:
  "(⋃⋃X|I)  R  ⋂⋂(λi . X i  R)|I"
proof -
  have "(⋃⋃X|I)  R = ((⋃⋃X|I) * R)"
    by (simp add: co_prod)
  also have "...  ((⋃⋃(λi . X i * R)|I))"
    by (simp add: ic_isotone sp_right_subdist_iU)
  also have "... = ⋂⋂(λi . X i  R)|I"
    apply (subst ic_antidist_iU)
    by (metis co_prod comp_apply)
  finally show ?thesis
    .
qed

lemma cp_right_antidist_iU:
  assumes "J::'a set . J  {}  (⋂⋂(λj . R)|J)  R"
  shows "(⋃⋃X|I)  R = ⋂⋂(λi . X i  R)|(I::'a set)"
proof -
  have 1: "J . ⋃⋃(λj.  R)|J = ⋂⋂(λj . R)|J"
    apply (subst ic_antidist_iI)
    by (metis comp_apply)
  have "(⋃⋃X|I)  R = ((⋃⋃X|I) * R)"
    by (simp add: co_prod)
  also have "... = ((⋃⋃(λi . X i * R)|I))"
    by (simp add: 1 assms sp_right_dist_iU ic_isotone)
  also have "... = ⋂⋂(λi . X i  R)|I"
    apply (subst ic_antidist_iU)
    by (metis co_prod comp_apply)
  finally show ?thesis
    .
qed

subsection ‹Inner order›

definition inner_order_iu :: "'a × 'b set  'a × 'b set  bool" (infix "" 50) where
  "x  y  fst x = fst y  snd x  snd y"

definition inner_order_ii :: "'a × 'b set  'a × 'b set  bool" (infix "" 50) where
  "x  y  fst x = fst y  snd x  snd y"

lemma inner_order_dual:
  "x  y  y  x"
  by (metis inner_order_ii_def inner_order_iu_def)

interpretation inner_order_iu: order "(≼)" "λx y . x  y  x  y"
  by (unfold_locales, auto simp add: inner_order_iu_def)

subsection ‹Up-closure, down-closure and convex-closure›

abbreviation up :: "('a,'b) mrel  ('a,'b) mrel" ("_" [100] 100)
  where "R  R ∪∪ U"

abbreviation down :: "('a,'b) mrel  ('a,'b) mrel" ("_" [100] 100)
  where "R  R ∩∩ U"

abbreviation convex :: "('a,'b) mrel  ('a,'b) mrel" ("_" [100] 100)
  where "R  R  R"

lemma up:
  "R = { (a,B) . C . (a,C)  R  C  B }"
  by (simp add: p_id_U)

lemma down:
  "R = { (a,B) . C . (a,C)  R  B  C }"
  by (auto simp: mr_simp)

lemma convex:
  "R = { (a,B) . C D . (a,C)  R  (a,D)  R  C  B  B  D }"
  by (auto simp: mr_simp)

declare up [mr_simp] down [mr_simp] convex [mr_simp]

lemma ic_up:
  "(R) = (R)"
  by (simp add: ic_antidist_iu)

lemma ic_down:
  "(R) = (R)"
  by (simp add: ic_antidist_ii)

lemma ic_convex:
  "(R) = (R)"
  by (simp add: ic_dist_oi ic_down ic_up inf_commute)

lemma up_isotone:
  "R  S  R  S"
  by (fact iu_left_isotone)

lemma up_increasing:
  "R  R"
  by (simp add: upclosed_ext)

lemma up_idempotent [simp]:
  "R = R"
  by (simp add: iu_assoc)

lemma up_dist_ou:
  "(R  S) = R  S"
  by (simp add: iu_right_dist_ou)

lemma up_dist_iu:
  "(R ∪∪ S) = R ∪∪ S"
  using cv_hom_par p_prod_assoc by blast

lemma up_dist_ii:
  "(R ∩∩ S) = R ∩∩ S"
proof (rule antisym)
  show "(R ∩∩ S)  R ∩∩ S"
    by (simp add: iu_right_subdist_ii)
next
  have "a B C D E . (a,B)  R  (a,C)  S  F . (G . (B  D)  (C  E) = F  G)  (H I . F = H  I  (a,H)  R  (a,I)  S)"
  proof -
    fix a B C D E
    assume 1: "(a,B)  R"
    assume 2: "(a,C)  S"
    let ?F = "B  C"
    let ?G = "(B  E)  (D  C)  (D  E)"
    have "(B  D)  (C  E) = ?F  ?G"
      by auto
    thus "F . (G . (B  D)  (C  E) = F  G)  (H I . F = H  I  (a,H)  R  (a,I)  S)"
      using 1 2 by auto
  qed
  thus "R ∩∩ S  (R ∩∩ S)"
    by (clarsimp simp: mr_simp)
qed

lemma down_isotone:
  "R  S  R  S"
  by (fact ii_left_isotone)

lemma down_increasing:
  "R  R"
  by (metis ic_involutive ic_isotone ic_up up_increasing)

lemma down_idempotent [simp]:
  "R = R"
  by (simp add: ic_down ic_injective)

lemma down_dist_ou:
  "(R  S) = R  S"
  by (fact ii_right_dist_ou)

lemma down_dist_iu:
  "(R ∪∪ S) = R ∪∪ S"
  by (simp add: ic_antidist_ii ic_antidist_iu ic_injective up_dist_ii)

lemma down_dist_ii:
  "(R ∩∩ S) = R ∩∩ S"
  by (metis down_idempotent ii_assoc ii_commute)

lemma convex_isotone:
  "R  S  R  S"
  by (meson Int_mono down_isotone up_isotone)

lemma convex_increasing:
  "R  R"
  by (simp add: down_increasing up_increasing)

lemma convex_idempotent [simp]:
  "R = R"
  by (smt (verit, ccfv_threshold) U_par_idem convex_increasing convex_isotone ic_top ic_up ii_assoc iu_assoc le_inf_iff subsetI subset_antisym)

lemma down_sp:
  "R = R * (1  1)"
proof -
  have "a B . (C . (D . B = C  D)  (a,C)  R)  (C . (a,C)  R  (f . (cC . f c = {}  f c = {c})  B = (cC . f c)))"
  proof (intro allI, rule iffI)
    fix a B
    assume "C . (D . B = C  D)  (a,C)  R"
    from this obtain C where 1: "D . B = C  D" and 2: "(a,C)  R"
      by auto
    let ?f = "λc . if c  B then {c} else {}"
    have "(cC . ?f c) = (cB . ?f c)  (cC-B . ?f c)"
      using 1 by blast
    hence 3: "B = (cC . ?f c)"
      by auto
    have "cC . ?f c = {}  ?f c = {c}"
      by auto
    thus "C . (a,C)  R  (f . (cC . f c = {}  f c = {c})  B = (cC . f c))"
      using 2 3 by smt
  next
    fix a B
    assume "C . (a,C)  R  (f . (cC . f c = {}  f c = {c})  B = (cC . f c))"
    from this obtain C where 4: "(a,C)  R" and "f . (cC . f c = {}  f c = {c})  B = (cC . f c)"
      by auto
    hence "B  C"
      by auto
    thus "C . (D . B = C  D)  (a,C)  R"
      using 4 by auto
  qed
  thus ?thesis
    by (clarsimp simp: mr_simp)
qed

lemma up_cp:
  "R = R  (1  1)"
  by (metis co_prod down_sp ic_dist_ou ic_ii_unit ic_involutive ic_up)

lemma down_dist_sp:
  "(R * S) = R * S"
proof (rule antisym)
  show "(R * S)  R * S"
    by (simp add: down_sp s_prod_assoc1)
next
  have "a B f . (a,B)  R  bB . C . (D . f b = C  D)  (b,C)  S  E . (F . (bB . f b) = E  F)  (B . (a,B)  R  (g . (bB . (b,g b)  S)  E = (bB . g b)))"
  proof -
    fix a B f
    assume 1: "(a,B)  R"
    assume "bB . C . (D . f b = C  D)  (b,C)  S"
    hence "g . bB . (D . f b = g b  D)  (b,g b)  S"
      by metis
    from this obtain g where 2: "bB . (D . f b = g b  D)  (b,g b)  S"
      by auto
    hence "(bB . f b)  (bB . g b)"
      by blast
    thus "E . (F . (bB . f b) = E  F)  (B . (a,B)  R  (g . (bB . (b,g b)  S)  E = (bB . g b)))"
      using 1 2 by (metis semilattice_inf_class.inf.absorb_iff2)
  qed
  thus "R * S  (R * S)"
    by (clarsimp simp: mr_simp)
qed

lemma up_dist_cp:
  "(R  S) = R  S"
  by (metis co_prod down_dist_sp ic_down ic_up)

lemma iu_up_oi:
  "R ∪∪ S = R  S"
  by (fact up_closed_par_is_meet)

lemma ii_down_oi:
  "R ∩∩ S = R  S"
  by (metis ic_antidist_ii ic_dist_oi ic_down ic_involutive up_closed_par_is_meet)

lemma down_dist_ii_oi:
  "R  S = (R ∩∩ S)"
  by (simp add: down_dist_ii ii_down_oi)

lemma up_dist_iu_oi:
  "R  S = (R ∪∪ S)"
  by (simp add: up_closed_par_is_meet up_dist_iu)

lemma oi_down_sub_up:
  "R  S  (R  S)"
  by (auto simp: mr_simp)

lemma oi_down_up:
  "R  S = {}  R  S = {}"
  by (metis (no_types, lifting) cp_left_zero down_increasing ic_bot inf.orderE inf_assoc inf_bot_right oi_down_sub_up up_cp)

lemma oi_down_up_iff:
  "R  S = {}  R  S = {}"
proof (rule iffI)
  show "R  S = {}  R  S = {}"
    by (simp add: oi_down_up)
next
  assume 1: "R  S = {}"
  have "(S) = (S)"
    by (metis (no_types) ic_down ic_involutive)
  hence "(R  S) = {}"
    using 1 by (metis Int_commute ic_bot ic_dist_oi ic_down oi_down_up)
  thus "R  S = {}"
    by (metis (no_types) ic_bot ic_involutive)
qed

lemma down_double_complement_up:
  "R  S  R  -((-S))"
  by (metis disjoint_eq_subset_Compl double_compl oi_down_up_iff)

lemma up_double_complement_down:
  "R  S  R  -((-S))"
  by (metis Compl_subset_Compl_iff double_compl down_double_complement_up)

lemma below_up_oi_down:
  "R  R  R"
  by (fact convex_increasing)

lemma cp_pa_sim:
  "(R  S) = R  S"
  by (metis co_prod ic_involutive ic_up pa_ic pe_pa_sim)

lemma domain_up_down_conjugate:
  "(R  S) * 1 = (R  S) * 1"
  apply (rule set_eqI, clarsimp simp: mr_simp)
  by (smt (verit, del_insts) Int_Un_eq(1) SUP_bot SUP_bot_conv(1) Un_Int_eq(1))

lemma down_below_sp_top:
  "R  R * U"
  apply (clarsimp simp: mr_simp)
  by (metis Int_Union UN_constant image_empty inf_commute)

lemma down_oi_up_closed:
  assumes "Q = Q"
  shows "R  Q  (R  Q)"
  using assms apply (clarsimp simp: mr_simp)
  by (metis (no_types, lifting) assms inf.cobounded1 ucl_iff)

lemma up_dist_oU:
  "(X) = (up ` X)"
  by (simp add: iu_right_dist_oU)

lemma up_dist_iU:
  assumes "I  {}"
  shows "(⋃⋃X|I) = ⋃⋃(up o X)|I"
  apply (rule antisym)
   apply (clarsimp simp: mr_simp)
   apply (metis UN_simps(2) assms)
  apply (clarsimp simp: mr_simp)
  subgoal for a f
  proof -
    fix a f
    assume "iI . B . (C . f i = B  C)  (a,B)  X i"
    from this obtain g where "iI . (C . f i = g i  C)  (a,g i)  X i"
      by metis
    hence "(C . (f ` I) = (g ` I)  C)  ((g ` I) = (g ` I)  (iI . (a,g i)  X i))"
      by auto
    thus "B . (C . (f ` I) = B  C)  (f . B = (f ` I)  (iI . (a,f i)  X i))"
      by auto
  qed
  done

lemma up_dist_iI:
  "(⋂⋂X|I) = ⋂⋂(up o X)|I"
  apply (rule antisym)
   apply (clarsimp simp: mr_simp)
   apply (smt (z3) INT_simps(10) sup_Inf sup_commute)
  apply (clarsimp simp: mr_simp)
  subgoal for a f
  proof -
    assume "iI . B . (C . f i = B  C)  (a,B)  X i"
    from this obtain g where "iI . (C . f i = g i  C)  (a,g i)  X i"
      by metis
    hence "(C . (f ` I) = (g ` I)  C)  ((g ` I) = (g ` I)  (iI . (a,g i)  X i))"
      by auto
    thus "B . (C . (f ` I) = B  C)  (f . B = (f ` I)  (iI . (a,f i)  X i))"
      by auto
  qed
  done

lemma down_dist_oU:
  "(X) = (down ` X)"
  by (simp add: ii_right_dist_oU)

lemma down_dist_iU:
  "(⋃⋃X|I) = ⋃⋃(down o X)|I"
  apply (rule antisym)
   apply (clarsimp simp: mr_simp)
   apply (metis UN_extend_simps(4))
  apply (clarsimp simp: mr_simp)
  subgoal for a f
  proof -
    assume "iI . B . (C . f i = B  C)  (a,B)  X i"
    from this obtain g where "iI . (C . f i = g i  C)  (a,g i)  X i"
      by metis
    hence "(C . (f ` I) = (g ` I)  C)  ((g ` I) = (g ` I)  (iI . (a,g i)  X i))"
      by auto
    thus "B . (C . (f ` I) = B  C)  (f . B = (f ` I)  (iI . (a,f i)  X i))"
      by auto
  qed
  done

lemma down_dist_iI:
  assumes "I  {}"
  shows "(⋂⋂X|I) = ⋂⋂(down o X)|I"
  apply (rule antisym)
   apply (clarsimp simp: mr_simp)
   apply (smt (verit, del_insts) INF_const INT_absorb Int_commute assms semilattice_inf_class.inf_left_commute)
  apply (clarsimp simp: mr_simp)
  subgoal for a f
  proof -
    assume "iI . B . (C . f i = B  C)  (a,B)  X i"
    from this obtain g where "iI . (C . f i = g i  C)  (a,g i)  X i"
      by metis
    hence "(C . (f ` I) = (g ` I)  C)  ((g ` I) = (g ` I)  (iI . (a,g i)  X i))"
      by auto
    thus "B . (C . (f ` I) = B  C)  (f . B = (f ` I)  (iI . (a,f i)  X i))"
      by auto
  qed
  done


lemma iU_up_oI:
  assumes "I  {}"
  shows "⋃⋃(up o X)|I = (up ` X ` I)"
  apply (rule antisym)
   apply (clarsimp simp: mr_simp)
   apply (metis UN_absorb sup_assoc)
  apply (clarsimp simp: mr_simp)
  by (metis UN_constant assms)

lemma iI_down_oI:
  assumes "I  {}"
  shows "⋂⋂(down o X)|I = (down ` X ` I)"
  apply (rule antisym)
   apply (clarsimp simp: mr_simp)
   apply (metis INF_absorb Int_assoc)
  apply (clarsimp simp: mr_simp)
  using INF_eq_const assms by auto

lemma down_dist_iI_oI:
  "(down ` X ` I) = (⋂⋂X|I)"
  apply (rule antisym)
   apply (clarsimp simp: mr_simp)
   apply (metis INF_const INF_greatest INT_absorb empty_iff semilattice_inf_class.inf.absorb_iff2 semilattice_inf_class.le_inf_iff)
  apply (clarsimp simp: mr_simp)
  by blast

lemma up_dist_iU_oI:
  "(up ` X ` I) = (⋃⋃X|I)"
  apply (rule antisym)
   apply (clarsimp simp: mr_simp)
  subgoal for a D proof -
    assume "iI . B . (C . D = B  C)  (a,B)  X i"
    from this obtain f where 1: "iI . (C . D = f i  C)  (a,f i)  X i"
      by metis
    hence "C . D = (f ` I)  C"
      by auto
    thus ?thesis
      using 1 by auto
  qed
  apply (clarsimp simp: mr_simp)
  by blast

lemma iu_up:
  "(R ∪∪ R) = R"
  using up_dist_iu_oi by auto

lemma ii_down:
  "(R ∩∩ R) = R"
  using down_dist_ii_oi by blast

lemma iU_up:
  assumes "I  {}"
  shows "(⋃⋃(λj . R)|I) = R"
  apply (rule antisym)
   apply (clarsimp simp: mr_simp)
  using assms apply blast
  apply (clarsimp simp: mr_simp)
  by (metis UN_constant assms)

lemma iI_down:
  assumes "I  {}"
  shows "(⋂⋂(λj . R)|I) = R"
  apply (rule antisym)
   apply (clarsimp simp: mr_simp)
  using assms apply blast
  apply (clarsimp simp: mr_simp)
  by (metis INF_const assms)

lemma iu_unit_up:
  "1 = U"
  by (simp add: iu_commute)

lemma iu_unit_down:
  "1 = 1"
  by (simp add: down_sp)

lemma iu_unit_convex:
  "1 = 1"
  by (simp add: iu_unit_down p_id_zero)

lemma ii_unit_up:
  "1 = 1"
  by (simp add: up_cp)

lemma ii_unit_down:
  "1 = U"
  using ii_commute ii_unit by blast

lemma ii_unit_convex:
  "1 = 1"
  using down_increasing ii_unit_up by blast

lemma sp_unit_down:
  "1 = 1  1"
  by (simp add: down_sp inf_sup_aci(5))

lemma sp_unit_convex:
  "1 = 1"
  unfolding convex s_id_def by force

lemma top_up:
  "U = U"
  by simp

lemma top_down:
  "U = U"
  by (metis U_par_idem ic_top ic_up)

lemma top_convex:
  "U = U"
  by (simp add: top_down)

lemma bot_up:
  "{} = {}"
  by (simp add: p_prod_comm)

lemma bot_down:
  "{} = {}"
  using oi_down_up_iff by fastforce

lemma bot_convex:
  "{} = {}"
  by (simp add: bot_down)

lemma down_oi_up_convex:
  "(R  S) = R  S"
  unfolding up down convex by blast

lemma convex_iff_down_oi_up:
  "Q = Q  (R S . Q = R  S)"
  using down_oi_up_convex by blast

lemma convex_closed_oI:
  "(RX . R) = (RX . R)"
  apply (rule antisym)
   apply (clarsimp simp: mr_simp)
   apply (smt (verit, best) semilattice_inf_class.inf_commute semilattice_inf_class.inf_left_commute sup_commute sup_left_commute)
  by (meson convex_increasing)

lemma convex_closed_oi:
  "(R  S) = R  S"
  using convex_closed_oI[of "{R,S}"] by simp

lemma
  "(R ∪∪ S) = R ∪∪ S"
  nitpick[expect=genuine,card=1,3]
  oops

section ‹Powerdomain Preorders›

abbreviation lower_less_eq :: "('a,'b) mrel  ('a,'b) mrel  bool" (infixl "⊑↓" 50) where
  "R ⊑↓ S  R  S"

abbreviation upper_less_eq :: "('a,'b) mrel  ('a,'b) mrel  bool" (infixl "⊑↑" 50) where
  "R ⊑↑ S  S  R"

abbreviation convex_less_eq :: "('a,'b) mrel  ('a,'b) mrel  bool" (infixl "⊑↕" 50) where
  "R ⊑↕ S  R ⊑↓ S  R ⊑↑ S"

abbreviation Convex_less_eq :: "('a,'b) mrel  ('a,'b) mrel  bool" (infixl "⊑⇕" 50) where
  "R ⊑⇕ S  R  S"

lemma lower_less_eq:
  "R ⊑↓ S  (a B . (a,B)  R  (C . (a,C)  S  B  C))"
  apply (clarsimp simp: mr_simp)
  apply safe
   apply blast
  by (metis inf.absorb_iff2)

lemma upper_less_eq:
  "R ⊑↑ S  (a C . (a,C)  S  (B . (a,B)  R  B  C))"
  by (meson U_par_st subrelI subsetD)

lemma Convex_less_eq:
  "R ⊑⇕ S  (a C . (a,C)  R  (B D . (a,B)  S  (a,D)  S  B  C  C  D))"
  by (meson lower_less_eq semilattice_inf_class.le_inf_iff upper_less_eq)

lemma Convex_lower_upper:
  "R ⊑⇕ S  R ⊑↓ S  S ⊑↑ R"
  by auto

lemma lower_reflexive:
  "R ⊑↓ R"
  by (fact down_increasing)

lemma upper_reflexive:
  "R ⊑↑ R"
  by (fact up_increasing)

lemma convex_reflexive:
  "R ⊑↕ R"
  by (simp add: lower_reflexive upper_reflexive)

lemma Convex_reflexive:
  "R ⊑⇕ R"
  by (fact convex_increasing)

lemma lower_transitive:
  "R ⊑↓ S  S ⊑↓ T  R ⊑↓ T"
  using down_idempotent down_isotone by blast

lemma upper_transitive:
  "R ⊑↑ S  S ⊑↑ T  R ⊑↑ T"
  using up_idempotent up_isotone by blast

lemma convex_transitive:
  "R ⊑↕ S  S ⊑↕ T  R ⊑↕ T"
  by (meson lower_transitive upper_transitive)

lemma Convex_transitive:
  "R ⊑⇕ S  S ⊑⇕ T  R ⊑⇕ T"
  by (metis le_inf_iff lower_transitive upper_transitive)

lemma bot_lower_least:
  "{} ⊑↓ R"
  by simp

lemma top_upper_least:
  "U ⊑↑ R"
  by (metis U_par_idem iu_assoc le_inf_iff up_dist_iu_oi upper_reflexive)

lemma bot_Convex_least:
  "{} ⊑⇕ R"
  by simp

lemma top_lower_greatest:
  "R ⊑↓ U"
  using U_par_idem top_down top_upper_least by blast

lemma bot_upper_greatest:
  "R ⊑↑ {}"
  by simp

lemma top_Convex_greatest:
  "R ⊑⇕ U"
  using U_par_idem top_down top_upper_least by auto

lemma lower_iu_increasing:
  "R ⊑↓ R ∪∪ R"
  by (meson dual_order.trans lower_reflexive subidem_par)

lemma upper_iu_increasing:
  "R ⊑↑ R ∪∪ S"
  using p_prod_isor top_upper_least by auto

lemma convex_iu_increasing:
  "R ⊑↕ R ∪∪ R"
  by (simp add: lower_iu_increasing upper_iu_increasing)

lemma Convex_iu_increasing:
  "R ⊑⇕ R ∪∪ R"
  by (simp add: iu_up lower_iu_increasing upper_reflexive)

lemma lower_ii_decreasing:
  "R ∩∩ S ⊑↓ R"
  by (metis ii_right_isotone top_down top_lower_greatest)

lemma upper_ii_decreasing:
  "R ∩∩ R ⊑↑ R"
  using convex_reflexive ii_sub_idempotent by fastforce

lemma convex_ii_decreasing:
  "R ∩∩ R ⊑↕ R"
  by (simp add: lower_ii_decreasing upper_ii_decreasing)

lemma Convex_ii_increasing:
  "R ⊑⇕ R ∩∩ R"
  by (simp add: ii_down lower_reflexive upper_ii_decreasing)

lemma iu_lower_left_isotone:
  "R ⊑↓ S  R ∪∪ T ⊑↓ S ∪∪ T"
  by (simp add: down_dist_iu iu_isotone lower_reflexive)

lemma iu_upper_left_isotone:
  "R ⊑↑ S  R ∪∪ T ⊑↑ S ∪∪ T"
  by (metis (no_types, lifting) iu_assoc iu_commute iu_left_isotone)

lemma iu_convex_left_isotone:
  "R ⊑↕ S  R ∪∪ T ⊑↕ S ∪∪ T"
  by (simp add: iu_lower_left_isotone iu_upper_left_isotone)

lemma iu_Convex_left_isotone:
  "R ⊑⇕ S  R ∪∪ T ⊑⇕ S ∪∪ T"
  by (simp add: iu_lower_left_isotone iu_upper_left_isotone)

lemma iu_lower_right_isotone:
  "R ⊑↓ S  T ∪∪ R ⊑↓ T ∪∪ S"
  by (simp add: iu_commute iu_lower_left_isotone)

lemma iu_upper_right_isotone:
  "R ⊑↑ S  T ∪∪ R ⊑↑ T ∪∪ S"
  by (simp add: iu_assoc iu_right_isotone)

lemma iu_convex_right_isotone:
  "R ⊑↕ S  T ∪∪ R ⊑↕ T ∪∪ S"
  by (simp add: iu_lower_right_isotone iu_upper_right_isotone)

lemma iu_Convex_right_isotone:
  "R ⊑⇕ S  T ∪∪ R ⊑⇕ T ∪∪ S"
  by (simp add: iu_lower_right_isotone iu_upper_right_isotone)

lemma iu_lower_isotone:
  "R ⊑↓ S  P ⊑↓ Q  R ∪∪ P ⊑↓ S ∪∪ Q"
  by (simp add: down_dist_iu iu_isotone)

lemma iu_upper_isotone:
  "R ⊑↑ S  P ⊑↑ Q  R ∪∪ P ⊑↑ S ∪∪ Q"
  by (simp add: iu_isotone up_dist_iu)

lemma iu_convex_isotone:
  "R ⊑↕ S  P ⊑↕ Q  R ∪∪ P ⊑↕ S ∪∪ Q"
  by (simp add: iu_lower_isotone iu_upper_isotone)

lemma iu_Convex_isotone:
  "R ⊑⇕ S  P ⊑⇕ Q  R ∪∪ P ⊑⇕ S ∪∪ Q"
  by (simp add: down_dist_iu iu_isotone up_dist_iu)

lemma ii_lower_left_isotone:
  "R ⊑↓ S  R ∩∩ T ⊑↓ S ∩∩ T"
  by (simp add: down_dist_ii ii_isotone lower_reflexive)

lemma ii_upper_left_isotone:
  "R ⊑↑ S  R ∩∩ T ⊑↑ S ∩∩ T"
  by (simp add: ii_isotone up_dist_ii upper_reflexive)

lemma ii_convex_left_isotone:
  "R ⊑↕ S  R ∩∩ T ⊑↕ S ∩∩ T"
  by (simp add: ii_lower_left_isotone ii_upper_left_isotone)

lemma ii_Convex_left_isotone:
  "R ⊑⇕ S  R ∩∩ T ⊑⇕ S ∩∩ T"
  by (simp add: ii_lower_left_isotone ii_upper_left_isotone)

lemma ii_lower_right_isotone:
  "R ⊑↓ S  T ∩∩ R ⊑↓ T ∩∩ S"
  by (simp add: ii_assoc ii_right_isotone)

lemma ii_upper_right_isotone:
  "R ⊑↑ S  T ∩∩ R ⊑↑ T ∩∩ S"
  by (simp add: ii_commute ii_upper_left_isotone)

lemma ii_convex_right_isotone:
  "R ⊑↕ S  T ∩∩ R ⊑↕ T ∩∩ S"
  by (simp add: ii_lower_right_isotone ii_upper_right_isotone)

lemma ii_Convex_right_isotone:
  "R ⊑⇕ S  T ∩∩ R ⊑⇕ T ∩∩ S"
  by (simp add: ii_lower_right_isotone ii_upper_right_isotone)

lemma ii_lower_isotone:
  "R ⊑↓ S  P ⊑↓ Q  R ∩∩ P ⊑↓ S ∩∩ Q"
  by (simp add: down_dist_ii ii_isotone)

lemma ii_upper_isotone:
  "R ⊑↑ S  P ⊑↑ Q  R ∩∩ P ⊑↑ S ∩∩ Q"
  by (simp add: ii_isotone up_dist_ii)

lemma ii_convex_isotone:
  "R ⊑↕ S  P ⊑↕ Q  R ∩∩ P ⊑↕ S ∩∩ Q"
  by (simp add: ii_lower_isotone ii_upper_isotone)

lemma ii_Convex_isotone:
  "R ⊑⇕ S  P ⊑⇕ Q  R ∩∩ P ⊑⇕ S ∩∩ Q"
  by (simp add: ii_lower_isotone ii_upper_isotone)

lemma ou_lower_left_isotone:
  "R ⊑↓ S  R  T ⊑↓ S  T"
  by (meson le_sup_iff lower_reflexive lower_transitive)

lemma ou_upper_left_isotone:
  "R ⊑↑ S  R  T ⊑↑ S  T"
  by (metis Un_subset_iff sup.coboundedI1 up_dist_ou upclosed_ext)

lemma ou_convex_left_isotone:
  "R ⊑↕ S  R  T ⊑↕ S  T"
  by (meson ou_lower_left_isotone ou_upper_left_isotone)

lemma ou_Convex_left_isotone:
  "R ⊑⇕ S  R  T ⊑⇕ S  T"
  by (meson le_inf_iff ou_lower_left_isotone ou_upper_left_isotone)

lemma ou_lower_right_isotone:
  "R ⊑↓ S  T  R ⊑↓ T  S"
  by (metis Un_commute ou_lower_left_isotone)

lemma ou_upper_right_isotone:
  "R ⊑↑ S  T  R ⊑↑ T  S"
  by (metis Un_commute ou_upper_left_isotone)

lemma ou_convex_right_isotone:
  "R ⊑↕ S  T  R ⊑↕ T  S"
  by (meson ou_lower_right_isotone ou_upper_right_isotone)

lemma ou_Convex_right_isotone:
  "R ⊑⇕ S  T  R ⊑⇕ T  S"
  by (metis Un_commute ou_Convex_left_isotone)

lemma ou_lower_isotone:
  "R ⊑↓ S  P ⊑↓ Q  R  P ⊑↓ S  Q"
  using down_dist_ou by blast

lemma ou_upper_isotone:
  "R ⊑↑ S  P ⊑↑ Q  R  P ⊑↑ S  Q"
  by (simp add: iu_right_dist_ou sup.coboundedI1 sup.coboundedI2)

lemma ou_convex_isotone:
  "R ⊑↕ S  P ⊑↕ Q  R  P ⊑↕ S  Q"
  by (meson ou_lower_isotone ou_upper_isotone)

lemma ou_Convex_isotone:
  "R ⊑⇕ S  P ⊑⇕ Q  R  P ⊑⇕ S  Q"
  by (metis le_inf_iff ou_lower_isotone ou_upper_isotone)

lemma sp_lower_left_isotone:
  "R ⊑↓ S  T * R ⊑↓ T * S"
  by (simp add: down_dist_sp s_prod_isor)

lemma sp_upper_left_isotone:
  "R ⊑↑ S  T * R ⊑↑ T * S"
  by (meson cl3 dual_order.trans s_prod_isor upper_iu_increasing)

lemma sp_convex_left_isotone:
  "R ⊑↕ S  T * R ⊑↕ T * S"
  by (simp add: sp_lower_left_isotone sp_upper_left_isotone)

lemma sp_Convex_left_isotone:
  "R ⊑⇕ S  T * R ⊑⇕ T * S"
  by (simp add: sp_lower_left_isotone sp_upper_left_isotone)

lemma cp_lower_left_isotone:
  "R ⊑↓ S  T  R ⊑↓ T  S"
  by (smt (verit) co_prod ic_antidist_ii ic_antidist_iu ic_isotone ic_top sp_upper_left_isotone)

lemma cp_upper_left_isotone:
  "R ⊑↑ S  T  R ⊑↑ T  S"
  by (simp add: cp_right_isotone up_dist_cp)

lemma cp_convex_left_isotone:
  "R ⊑↕ S  T  R ⊑↕ T  S"
  by (simp add: cp_lower_left_isotone cp_upper_left_isotone)

lemma cp_Convex_left_isotone:
  "R ⊑⇕ S  T  R ⊑⇕ T  S"
  by (simp add: cp_lower_left_isotone cp_upper_left_isotone)

lemma lower_ic_upper:
  "R ⊑↓ S  S ⊑↑ R"
  by (metis ic_down ic_involutive ic_isotone)

lemma upper_ic_lower:
  "R ⊑↑ S  S ⊑↓ R"
  by (simp add: lower_ic_upper)

lemma convex_ic:
  "R ⊑↕ S  S ⊑↕ R"
  by (meson lower_ic_upper upper_ic_lower)

lemma Convex_ic:
  "R ⊑⇕ S  R ⊑⇕ S"
  by (metis le_inf_iff lower_ic_upper upper_ic_lower)

lemma up_lower_isotone:
  "R ⊑↓ S  R ⊑↓ S"
  by (fact iu_lower_left_isotone)

lemma up_upper_isotone:
  "R ⊑↑ S  R ⊑↑ S"
  by (fact iu_left_isotone)

lemma up_convex_isotone:
  "R ⊑↕ S  R ⊑↕ S"
  by (fact iu_convex_left_isotone)

lemma up_Convex_isotone:
  "R ⊑⇕ S  R ⊑⇕ S"
  by (fact iu_Convex_left_isotone)

lemma down_lower_isotone:
  "R ⊑↓ S  R ⊑↓ S"
  by (fact down_isotone)

lemma down_upper_isotone:
  "R ⊑↑ S  R ⊑↑ S"
  by (fact ii_upper_left_isotone)

lemma down_convex_isotone:
  "R ⊑↕ S  R ⊑↕ S"
  by (fact ii_convex_left_isotone)

lemma down_Convex_isotone:
  "R ⊑⇕ S  R ⊑⇕ S"
  by (fact ii_Convex_left_isotone)

lemma convex_lower_isotone:
  "R ⊑↓ S  R ⊑↓ S"
  by (metis convex_idempotent convex_increasing le_inf_iff lower_transitive)

lemma convex_upper_isotone:
  "R ⊑↑ S  R ⊑↑ S"
  by (simp add: convex_lower_isotone ic_convex upper_ic_lower)

lemma convex_convex_isotone:
  "R ⊑↕ S  R ⊑↕ S"
  by (simp add: convex_lower_isotone convex_upper_isotone)

lemma convex_Convex_isotone:
  "R ⊑⇕ S  R ⊑⇕ S"
  by (fact convex_isotone)

lemma subset_lower:
  "R  S  R ⊑↓ S"
  using lower_reflexive by auto

lemma subset_upper:
  "R  S  S ⊑↑ R"
  using upper_reflexive by blast

lemma subset_Convex:
  "R  S  R ⊑⇕ S"
  by (simp add: subset_lower subset_upper)

lemma oi_subset_lower_left_isotone:
  "R  S  R  T ⊑↓ S  T"
  using lower_reflexive by fastforce

lemma oi_subset_upper_left_antitone:
  "R  S  S  T ⊑↑ R  T"
  using upper_reflexive by force

lemma oi_subset_Convex_left_isotone:
  "R  S  R  T ⊑⇕ S  T"
  by (simp add: oi_subset_lower_left_isotone oi_subset_upper_left_antitone)

lemma oi_subset_lower_right_isotone:
  "R  S  T  R ⊑↓ T  S"
  by (simp add: oi_subset_lower_left_isotone semilattice_inf_class.inf_commute)

lemma oi_subset_upper_right_antitone:
  "R  S  T  S ⊑↑ T  R"
  by (simp add: oi_subset_upper_left_antitone semilattice_inf_class.inf_commute)

lemma oi_subset_Convex_right_isotone:
  "R  S  T  R ⊑⇕ T  S"
  using oi_subset_Convex_left_isotone by blast

lemma oi_subset_lower_isotone:
  "R  S  P  Q  R  P ⊑↓ S  Q"
  by (meson Int_mono subset_lower)

lemma oi_subset_upper_antitone:
  "R  S  P  Q  S  Q ⊑↑ R  P"
  by (meson Int_mono subset_upper)

lemma oi_subset_Convex_isotone:
  "R  S  P  Q  R  P ⊑⇕ S  Q"
  by (simp add: oi_subset_lower_isotone oi_subset_upper_antitone)

lemma sp_iu_unit_lower:
  "R * 1 ⊑↓ R"
  using lower_ii_decreasing sp_right_iu_unit by blast

lemma cp_ii_unit_upper:
  "R ⊑↑ R  1"
  by (meson cp_right_ii_unit in_mono subsetI upper_iu_increasing)

lemma lower_ii_down:
  "R ⊑↓ S  R = (R ∩∩ S)"
  apply safe
    apply (metis down_dist_ii_oi inf.orderE lower_ii_decreasing lower_transitive)
  using ii_assoc lower_ii_decreasing apply blast
  by (metis IntE down_dist_ii_oi lower_reflexive subset_eq)

lemma lower_ii_lower_bound:
  "R ⊑↓ S  R  R ∩∩ S"
  by (clarsimp simp: mr_simp) blast

lemma upper_ii_up:
  "R ⊑↑ S  S = (R ∪∪ S)"
  by (metis inf.absorb_iff2 up_dist_iu_oi upclosed_ext upper_iu_increasing upper_transitive)

lemma upper_ii_upper_bound:
  "R ⊑↑ S  S  R ∪∪ S"
  by (clarsimp simp: mr_simp) blast

lemma
  "R ⊑↓ S  R = R ∩∩ S"
  nitpick[expect=genuine,card=1]
  oops

lemma
  "R ⊑↑ S  S = R ∪∪ S"
  nitpick[expect=genuine,card=1]
  oops

lemma convex_oi_Convex_iu:
  "R  S ⊑⇕ R ∪∪ S"
  by (meson inf_le1 inf_le2 iu_Convex_isotone order_trans subidem_par)

lemma convex_oi_Convex_ii:
  "R  S ⊑⇕ R ∩∩ S"
  by (meson ii_Convex_isotone ii_sub_idempotent inf_le1 inf_le2 order_trans)

lemma convex_oi_iu_ii:
  "R  S = (R ∪∪ S)  (R ∩∩ S)"
  by (metis down_dist_ii_oi inf_assoc inf_left_commute up_dist_iu_oi)

lemma ii_lower_iu:
  "R ∩∩ S ⊑↓ R ∪∪ S"
  apply (clarsimp simp: mr_simp)
  by (metis Un_Int_eq(2) inf_left_commute)

lemma ii_upper_iu:
  "R ∩∩ S ⊑↑ R ∪∪ S"
  by (simp add: ic_antidist_ii ic_antidist_iu ii_lower_iu upper_ic_lower)

lemma ii_convex_iu:
  "R ∩∩ S ⊑↕ R ∪∪ S"
  by (simp add: ii_lower_iu ii_upper_iu)

lemma convex_oi_iu_ii_convex:
  "R  S = (R ∪∪ S)  (R ∩∩ S)"
  by (metis convex_oi_iu_ii ii_lower_iu ii_upper_iu inf.commute lower_ii_down upper_ii_up)

subsection ‹Functional properties of multirelations›

lemma id_one_converse:
  "Id = 1 ; 1"
  unfolding Id_def converse_def relcomp_unfold s_id_def by force

lemma dom_explicit:
  "Dom R = R ; U  1"
  by (clarsimp simp: mr_simp Dom_def) blast

lemma dom_explicit_2:
  "Dom R = R ; top  1"
  apply (clarsimp simp: mr_simp Dom_def)
  apply safe
    apply (simp add: relcomp.relcompI top_def)
   apply blast
  by blast

lemma total_dom:
  "total R  Dom R = 1"
  unfolding total_def dom_explicit_2
  apply (rule iffI)
  using top_def apply fastforce
  by (metis Int_subset_iff dom_def dom_gla_top dom_top id_one_converse inf.idem inf_le1)

lemma total_eq:
  "total R  1 = R * 1"
  by (metis total_dom U_c cd_iso dc dc_prop2)

lemma domain_pointwise:
  "x  R * 1  (a B . (a,B)  R  x = (a,{}))"
  by (smt mem_Collect_eq p_id_st)

text card› only works for finite sets›

lemma univalent_2:
  "univalent R  (a . finite { B . (a,B)  R }  card { B . (a,B)  R }  one_class.one)"
proof
  assume 1: "univalent R"
  show "a . finite { B . (a,B)  R }  card { B . (a,B)  R }  one_class.one"
  proof
    fix a
    let ?B = "{ B . (a,B)  R }"
    show "finite ?B  card ?B  one_class.one"
    proof (rule conjI)
      show 2: "finite ?B"
      proof (rule ccontr)
        assume 3: "infinite ?B"
        from this obtain B where 4: "(a,B)  R"
          using not_finite_existsD by auto
        have "?B = {B}"
        proof
          show "?B  {B}"
            using 1 4 by (metis (no_types, lifting) univalent_set insertCI mem_Collect_eq subsetI)
        next
          show "{B}  ?B"
            using 4 by simp
        qed
        thus False
          using 3 by auto
      qed
      show "card ?B  one_class.one"
      proof (rule ccontr)
        assume 5: "¬ card ?B  one_class.one"
        from this obtain B where 6: "(a,B)  R"
          by fastforce
        hence "card (?B - {B})  one_class.one"
          using 2 5 by auto
        from this obtain C where "(a,C)  R  B  C"
          using 5 by (metis (no_types, lifting) CollectD One_nat_def card.insert_remove card_Diff_singleton_if card.empty card_mono empty_iff finite.emptyI finite.insertI insert_iff subsetI)
        thus False
          using 1 6 by (meson univalent_set)
      qed
    qed
  qed
next
  assume 5: "a . finite { B . (a,B)  R }  card { B . (a,B)  R }  one_class.one"
  have "a B C . (a,B)  R  (a,C)  R  B = C"
  proof (intro allI, rule impI)
    fix a B C
    let ?B = "{ B . (a,B)  R }"
    have 6: "finite ?B"
      using 5 by simp
    assume "(a,B)  R  (a,C)  R"
    hence "{B,C}  ?B"
      by simp
    hence "card {B,C}  one_class.one"
      using 5 6 by (meson card_mono le_trans)
    thus "B = C"
      by (metis One_nat_def card.empty card_insert_disjoint empty_iff finite.emptyI finite.insertI insert_absorb lessI not_le singleton_insert_inj_eq)
  qed
  thus "univalent R"
    by (simp add: univalent_set)
qed

lemma univalent_3:
  "univalent R  (S . R * 1 = S * 1  S  R  S = R)"
proof
  assume 1: "S . R * 1 = S * 1  S  R  S = R"
  have "a B C . (a,B)  R  (a,C)  R  B = C"
  proof (intro allI, rule impI)
    fix a B C
    assume 2: "(a,B)  R  (a,C)  R"
    show "B = C"
    proof (rule ccontr)
      assume 3: "B  C"
      let ?S = "R - { (a,C) }"
      have 4: "R * 1 = ?S * 1"
      proof
        show "R * 1  ?S * 1"
        proof
          fix x::"'a × 'f set"
          assume "x  R * 1"
          from this obtain b D where "(b,D)  R  x = (b,{})"
            by (meson domain_pointwise)
          thus "x  ?S * 1"
            using 2 3 by (metis domain_pointwise Pair_inject insertE insert_Diff)
        qed
      next
        show "?S * 1  R * 1"
          by (simp add: s_prod_isol)
      qed
      have "?S  R"
        using 2 by blast
      thus False
        using 1 4 by blast
    qed
  qed
  thus "univalent R"
    by (simp add: univalent_set)
next
  assume 5: "univalent R"
  show "S . R * 1 = S * 1  S  R  S = R"
  proof
    fix S
    show "R * 1 = S * 1  S  R  S = R"
    proof
      assume 6: "R * 1 = S * 1  S  R"
      have "R  S"
      proof
        fix x
        assume 7: "x  R"
        from this obtain a B where 8: "x = (a,B)"
          by fastforce
        show "x  S"
        proof (cases "C . C  B  (a,C)  S")
          case True
          thus ?thesis
            using 5 6 7 8 by (metis subsetD univalent_set)
        next
          case False
          thus ?thesis
            using 6 7 8 by (metis (no_types, lifting) domain_pointwise prod.inject)
        qed
      qed
      thus "S = R"
        using 6 by simp
    qed
  qed
qed

lemma total_2:
  "total R  (a . { B . (a,B)  R }  {})"
  by (simp add: total_set)

lemma total_3:
  "total R  (a . finite { B . (a,B)  R }  card { B . (a,B)  R }  one_class.one)"
  by (metis finite.emptyI nonempty_set_card total_2)

lemma total_4: "total R  1  R * 1"
  by (simp add: c6 order_antisym_conv total_eq)

lemma deterministic_2:
  "deterministic R  (a . card { B . (a,B)  R } = one_class.one)"
  apply (rule iffI)
   apply (metis One_nat_def bot_nat_0.extremum_unique deterministic_def le_simps(2) less_Suc_eq nonempty_set_card total_2 univalent_2)
  by (metis card_1_singletonE deterministic_def finite.emptyI finite_insert order.refl total_3 univalent_2)

lemma univalent_convex:
  assumes "univalent S"
  shows "S = S"
  apply (rule antisym)
   apply (simp add: lower_reflexive upper_reflexive)
  apply (clarsimp simp: mr_simp)
  by (metis assms lattice_class.sup_inf_absorb sup_left_idem univalent_set)

lemma univalent_iu_idempotent:
  assumes "univalent S"
  shows "S = S ∪∪ S"
  apply (rule antisym)
   apply (meson convex_reflexive upper_ii_upper_bound)
  apply (clarsimp simp: mr_simp)
  by (metis assms sup.idem univalent_set)

lemma univalent_ii_idempotent:
  assumes "univalent S"
  shows "S = S ∩∩ S"
  apply (rule antisym)
   apply (simp add: ii_sub_idempotent)
  apply (clarsimp simp: mr_simp)
  by (metis assms semilattice_inf_class.inf.idem univalent_set)

lemma univalent_down_iu_idempotent:
  assumes "univalent S"
  shows "S = S ∪∪ S"
  apply (rule antisym)
   apply (meson convex_reflexive subset_upper upper_ii_upper_bound)
  apply (clarsimp simp: mr_simp)
  by (metis assms lattice_class.sup_inf_absorb sup_commute univalent_set)

lemma univalent_up_ii_idempotent:
  assumes "univalent S"
  shows "S = S ∩∩ S"
  apply (rule antisym)
   apply (metis assms ii_left_isotone univalent_ii_idempotent upclosed_ext)
  apply (clarsimp simp: mr_simp)
  by (metis Int_commute assms lattice_class.inf_sup_absorb univalent_set)

lemma univalent_convex_iu_idempotent:
  assumes "univalent S"
  shows "S = S ∪∪ S"
  by (metis assms univalent_convex univalent_iu_idempotent)

lemma univalent_convex_ii_idempotent:
  assumes "univalent S"
  shows "S = S ∩∩ S"
  by (metis assms univalent_convex univalent_ii_idempotent)

lemma univalent_iu_closed:
  "univalent R  univalent S  univalent (R ∪∪ S)"
  by (smt (verit, best) case_prodD mem_Collect_eq p_prod_def univalent_set)

lemma univalent_ii_closed:
  "univalent R  univalent S  univalent (R ∩∩ S)"
  by (smt (verit, ccfv_SIG) CollectD Pair_inject case_prodE inner_intersection_def univalent_set)

lemma total_lower:
  "total R  1 ⊑↓ R"
  unfolding lower_less_eq
  by (simp add: p_id_def total_set)

lemma total_upper:
  "total R  R ⊑↑ 1"
  unfolding upper_less_eq
  by (simp add: ii_unit_def total_set)

lemma total_lower_iu:
  assumes "total T"
  shows "R ⊑↓ R ∪∪ T"
  by (metis assms iu_lower_right_isotone iu_unit total_lower)

lemma total_upper_ii:
  assumes "total T"
  shows "R ∩∩ T ⊑↑ R"
  by (smt (verit, ccfv_threshold) U_par_idem assms iu_assoc iu_commute lower_ii_lower_bound total_lower_iu up_dist_ii upper_ii_up)

lemma total_univalent_lower_iu:
  assumes "total T"
    and "univalent S"
    and "T ⊑↓ S"
  shows "T ∪∪ S = S"
proof -
  have 1: "a. B. (a, B)  T"
    by (meson assms(1) total_set)
  have 2: "a B C. (a, B)  S  (a, C)  S  B = C"
    by (meson assms(2) univalent_set)
  hence 3: "T ∪∪ S  S"
    by (metis assms(2,3) iu_left_isotone univalent_down_iu_idempotent)
  hence "S  T ∪∪ S"
    apply (clarsimp simp: mr_simp)
    using 1 2 by (metis (mono_tags, lifting) CollectI Un_iff case_prodI subset_Un_eq)
  thus ?thesis
    using 3 by (simp add: subset_antisym)
qed

lemma total_iu_closed:
  "total R  total S  total (R ∪∪ S)"
  by (meson lower_transitive total_lower total_lower_iu)

lemma total_ii_closed:
  "total R  total S  total (R ∩∩ S)"
  by (metis down_dist_ii_oi le_inf_iff total_lower)

lemma deterministic_lower:
  assumes "deterministic V"
  shows "R ⊑↓ V  (a B C . (a,B)  R  (a,C)  V  B  C)"
proof -
  have "R ⊑↓ V  (a B . (a,B)  R  (C . (a,C)  V  B  C))"
    by (simp add: lower_less_eq)
  also have "...  (a B . (a,B)  R  (C . (a,C)  V  B  C))"
    by (metis assms deterministic_set)
  finally show ?thesis
    by blast
qed

lemma deterministic_upper:
  assumes "deterministic V"
  shows "V ⊑↑ R  (a B C . (a,B)  R  (a,C)  V  C  B)"
proof -
  have "V ⊑↑ R  (a C . (a,C)  R  (B . (a,B)  V  B  C))"
    by (simp add: upper_less_eq)
  also have "...  (a C . (a,C)  R  (B . (a,B)  V  B  C))"
    by (metis assms deterministic_set)
  finally show ?thesis
    by blast
qed

lemma deterministic_iu_closed:
  "deterministic R  deterministic S  deterministic (R ∪∪ S)"
  by (simp add: deterministic_def univalent_iu_closed total_iu_closed)

lemma deterministic_ii_closed:
  "deterministic R  deterministic S  deterministic (R ∩∩ S)"
  by (simp add: deterministic_def univalent_ii_closed total_ii_closed)

lemma total_univalent_lower_implies_upper:
  assumes "total T"
    and "univalent S"
    and "T ⊑↓ S"
  shows "T ⊑↑ S"
  by (simp add: assms total_univalent_lower_iu upper_ii_upper_bound)

lemma total_univalent_lower_implies_convex:
  assumes "total T"
    and "univalent S"
    and "T ⊑↓ S"
  shows "T ⊑↕ S"
  by (simp add: assms total_univalent_lower_implies_upper)

lemma total_univalent_upper_implies_lower:
  assumes "total T"
    and "univalent S"
    and "S ⊑↑ T"
  shows "S ⊑↓ T"
proof (clarsimp simp: mr_simp)
  fix a B
  assume 1: "(a,B)  S"
  from this obtain C where 2: "(a,C)  T"
    by (meson assms(1) total_set)
  hence "(a,C)  S"
    using assms(3) by auto
  from this obtain D where 3: "(a,D)  S  D  C"
    using 2 by (meson assms(3) upper_less_eq)
  hence "D = B"
    using 1 by (meson assms(2) univalent_set)
  thus "C . (D . B = C  D)  (a,C)  T"
    using 2 3 by (metis Int_absorb1)
qed

lemma total_univalent_upper_implies_convex:
  assumes "total T"
    and "univalent S"
    and "S ⊑↑ T"
  shows "S ⊑↕ T"
  by (simp add: assms total_univalent_upper_implies_lower)

lemma deterministic_lower_upper:
  assumes "deterministic T"
    and "deterministic S"
  shows "S ⊑↓ T  S ⊑↑ T"
  by (meson assms deterministic_def total_univalent_lower_implies_convex total_univalent_upper_implies_lower)

lemma deterministic_lower_convex:
  assumes "deterministic T"
    and "deterministic S"
  shows "S ⊑↓ T  S ⊑↕ T"
  by (simp add: assms deterministic_lower_upper)

lemma deterministic_upper_convex:
  assumes "deterministic T"
    and "deterministic S"
  shows "S ⊑↑ T  S ⊑↕ T"
  by (simp add: assms deterministic_lower_upper)

lemma total_down_sp_sp_down:
  assumes "total T"
  shows "R * T  R * T"
proof -
  have "R * T  R * ((1  1) * T)"
    by (simp add: down_sp s_prod_assoc1)
  also have "... = R * (1  T * 1)"
    by (simp add: s_prod_distr)
  also have "... = R * (T * 1  T * 1)"
    by (metis assms c6 order_antisym_conv total_4)
  also have "...  R * (T * (1  1))"
    by (metis down_sp le_supI s_prod_isor sp_iu_unit_lower sup_ge2)
  also have "... = R * T"
    by (simp add: down_sp)
  finally show ?thesis
    by simp
qed

lemma total_down_sp_semi_commute:
  "total T  R * T  (R * T)"
  by (simp add: down_dist_sp total_down_sp_sp_down)

lemma total_down_dist_sp:
  "total T  (R * T) = R * T"
  by (smt (verit, best) down_dist_sp equalityI ii_assoc ii_isotone lower_reflexive s_prod_isol top_down total_down_sp_semi_commute)

lemma univalent_ic_closed:
  "univalent R  univalent (R)"
  apply (unfold univalent_set)
  apply (clarsimp simp: mr_simp)
  by (metis double_compl)

lemma total_ic_closed:
  "total R  total (R)"
  by (metis total_dom d_def_expl domain_up_down_conjugate equalityI ic_down ic_top ic_up ii_commute inf.orderE lower_ic_upper top_down top_lower_greatest total_lower total_upper_ii)

lemma deterministic_ic_closed:
  "deterministic R  deterministic (R)"
  by (meson deterministic_def total_ic_closed univalent_ic_closed)

lemma iu_unit_deterministic:
  "deterministic (1)"
  by (metis Lambda_empty det_lambda)

lemma ii_unit_deterministic:
  "deterministic (1)"
  using deterministic_ic_closed iu_unit_deterministic by force

lemma univalent_upper_iu:
  assumes "univalent R"
  shows "(R ⊑↑ S)  (R ∪∪ S = S)"
proof -
  have 1: "R ∪∪ S = S  R ⊑↑ S"
    using upper_iu_increasing by blast
  have 2: "R ⊑↑ S  S  R ∪∪ S"
    by (simp add: upper_ii_upper_bound)
  have "R ⊑↑ S  R ∪∪ S  S"
    apply (clarsimp simp: mr_simp)
    by (smt (verit) Ball_Collect assms case_prodD le_iff_sup subset_refl sup.bounded_iff univalent_set)
  thus ?thesis
    using 1 2 by blast
qed

lemma univalent_lower_ii:
  assumes "univalent S"
  shows "(R ⊑↓ S) = (R ∩∩ S = R)"
  apply (clarsimp simp: mr_simp)
  apply safe
    apply (smt (z3) CollectD CollectI Collect_cong Int_iff assms case_prodD inf_set_def subsetD univalent_set)
   apply blast
  by (smt (verit, ccfv_threshold) CollectD Pair_inject case_prodE inf_commute)

subsection ‹Equivalences induced by powerdomain preorders›

abbreviation lower_eq :: "('a,'b) mrel  ('a,'b) mrel  bool" (infixl "=↓" 50) where
  "R =↓ S  R ⊑↓ S  S ⊑↓ R"

abbreviation upper_eq :: "('a,'b) mrel  ('a,'b) mrel  bool" (infixl "=↑" 50) where
  "R =↑ S  R ⊑↑ S  S ⊑↑ R"

abbreviation convex_eq :: "('a,'b) mrel  ('a,'b) mrel  bool" (infixl "=↕" 50) where
  "R =↕ S  R ⊑↕ S  S ⊑↕ R"

lemma Convex_eq:
  "R =↕ S  R ⊑⇕ S  S ⊑⇕ R"
  by (smt (z3) semilattice_inf_class.le_inf_iff)

lemma convex_lower_upper:
  "R =↕ S  R =↓ S  R =↑ S"
  by auto

lemma lower_eq_down:
  "R =↓ S  R = S"
  using down_idempotent down_lower_isotone lower_reflexive by blast

lemma upper_eq_up:
  "R =↑ S  R = S"
  by (metis p_prod_comm upclosed_ext upper_ii_up)

lemma convex_eq_convex:
  "R =↕ S  R = S"
  by (metis Convex_lower_upper lower_eq_down upper_eq_up)

lemma lower_eq:
  "R =↓ S  (a B . (C . (a,C)  R  B  C)  (C . (a,C)  S  B  C))"
  by (meson lower_less_eq order_refl order_trans)

lemma upper_eq:
  "R =↑ S  (a C . (B . (a,B)  R  B  C)  (B . (a,B)  S  B  C))"
  by (meson order_refl order_trans upper_less_eq)

lemma lower_eq_reflexive:
  "R =↓ R"
  by (simp add: lower_reflexive)

lemma upper_eq_reflexive:
  "R =↑ R"
  by (simp add: upper_reflexive)

lemma convex_eq_reflexive:
  "R =↕ R"
  by (simp add: lower_reflexive upper_reflexive)

lemma lower_eq_symmetric:
  "R =↓ S  S =↓ R"
  by simp

lemma upper_eq_symmetric:
  "R =↑ S  S =↑ R"
  by simp

lemma convex_eq_symmetric:
  "R =↕ S  S =↕ R"
  by simp

lemma lower_eq_transitive:
  "R =↓ S  S =↓ T  R =↓ T"
  using lower_transitive by auto

lemma upper_eq_transitive:
  "R =↑ S  S =↑ T  R =↑ T"
  using upper_transitive by auto

lemma convex_eq_transitive:
  "R =↕ S  S =↕ T  R =↕ T"
  by (meson lower_transitive upper_transitive)

lemma ou_lower_eq_left_congruence:
  "R =↓ S  R  T =↓ S  T"
  using ou_lower_left_isotone by blast

lemma ou_upper_eq_left_congruence:
  "R =↑ S  R  T =↑ S  T"
  using ou_upper_left_isotone by blast

lemma ou_convex_eq_left_congruence:
  "R =↕ S  R  T =↕ S  T"
  by (meson ou_lower_left_isotone ou_upper_left_isotone)

lemma ou_lower_eq_right_congruence:
  "R =↓ S  T  R =↓ T  S"
  using ou_lower_right_isotone by blast

lemma ou_upper_eq_right_congruence:
  "R =↑ S  T  R =↑ T  S"
  using ou_upper_right_isotone by blast

lemma ou_convex_eq_right_congruence:
  "R =↕ S  T  R =↕ T  S"
  by (meson ou_lower_right_isotone ou_upper_right_isotone)

lemma ou_lower_eq_congruence:
  "R =↓ S  P =↓ Q  R  P =↓ S  Q"
  using ou_lower_isotone by blast

lemma ou_upper_eq_congruence:
  "R =↑ S  P =↑ Q  R  P =↑ S  Q"
  using ou_upper_isotone by blast

lemma ou_convex_eq_congruence:
  "R =↕ S  P =↕ Q  R  P =↕ S  Q"
  by (meson ou_lower_isotone ou_upper_isotone)

lemma iu_lower_eq_left_congruence:
  "R =↓ S  R ∪∪ T =↓ S ∪∪ T"
  using iu_lower_left_isotone by blast

lemma iu_upper_eq_left_congruence:
  "R =↑ S  R ∪∪ T =↑ S ∪∪ T"
  using iu_upper_left_isotone by blast

lemma iu_convex_eq_left_congruence:
  "R =↕ S  R ∪∪ T =↕ S ∪∪ T"
  by (simp add: iu_lower_left_isotone iu_upper_left_isotone)

lemma iu_lower_eq_right_congruence:
  "R =↓ S  T ∪∪ R =↓ T ∪∪ S"
  using iu_lower_right_isotone by blast

lemma iu_upper_eq_right_congruence:
  "R =↑ S  T ∪∪ R =↑ T ∪∪ S"
  using iu_upper_right_isotone by blast

lemma iu_convex_eq_right_congruence:
  "R =↕ S  T ∪∪ R =↕ T ∪∪ S"
  by (simp add: iu_lower_right_isotone iu_upper_right_isotone)

lemma iu_lower_eq_congruence:
  "R =↓ S  P =↓ Q  R ∪∪ P =↓ S ∪∪ Q"
  using iu_lower_isotone by blast

lemma iu_upper_eq_congruence:
  "R =↑ S  P =↑ Q  R ∪∪ P =↑ S ∪∪ Q"
  using iu_upper_isotone by blast

lemma iu_convex_eq_congruence:
  "R =↕ S  P =↕ Q  R ∪∪ P =↕ S ∪∪ Q"
  by (simp add: iu_lower_isotone iu_upper_isotone)

lemma ii_lower_eq_left_congruence:
  "R =↓ S  R ∩∩ T =↓ S ∩∩ T"
  using ii_lower_left_isotone by blast

lemma ii_upper_eq_left_congruence:
  "R =↑ S  R ∩∩ T =↑ S ∩∩ T"
  using ii_upper_left_isotone by blast

lemma ii_convex_eq_left_congruence:
  "R =↕ S  R ∩∩ T =↕ S ∩∩ T"
  by (simp add: ii_lower_left_isotone ii_upper_left_isotone)

lemma ii_lower_eq_right_congruence:
  "R =↓ S  T ∩∩ R =↓ T ∩∩ S"
  using ii_lower_right_isotone by blast

lemma ii_upper_eq_right_congruence:
  "R =↑ S  T ∩∩ R =↑ T ∩∩ S"
  using ii_upper_right_isotone by blast

lemma ii_convex_eq_right_congruence:
  "R =↕ S  T ∩∩ R =↕ T ∩∩ S"
  by (simp add: ii_lower_right_isotone ii_upper_right_isotone)

lemma ii_lower_eq_congruence:
  "R =↓ S  P =↓ Q  R ∩∩ P =↓ S ∩∩ Q"
  using ii_lower_isotone by blast

lemma ii_upper_eq_congruence:
  "R =↑ S  P =↑ Q  R ∩∩ P =↑ S ∩∩ Q"
  using ii_upper_isotone by blast

lemma ii_convex_eq_congruence:
  "R =↕ S  P =↕ Q  R ∩∩ P =↕ S ∩∩ Q"
  by (simp add: ii_lower_isotone ii_upper_isotone)

lemma sp_lower_eq_left_congruence:
  "R =↓ S  T * R =↓ T * S"
  by (simp add: sp_lower_left_isotone)

lemma sp_upper_eq_left_congruence:
  "R =↑ S  T * R =↑ T * S"
  by (simp add: sp_upper_left_isotone)

lemma sp_convex_eq_left_congruence:
  "R =↕ S  T * R =↕ T * S"
  by (simp add: sp_lower_left_isotone sp_upper_left_isotone)

lemma cp_lower_eq_left_congruence:
  "R =↓ S  T  R =↓ T  S"
  by (simp add: cp_lower_left_isotone)

lemma cp_upper_eq_left_congruence:
  "R =↑ S  T  R =↑ T  S"
  by (simp add: cp_upper_left_isotone)

lemma cp_convex_eq_left_congruence:
  "R =↕ S  T  R =↕ T  S"
  by (simp add: cp_lower_left_isotone cp_upper_left_isotone)

lemma lower_eq_ic_upper:
  "R =↓ S  R =↑ S"
  using lower_ic_upper by auto

lemma upper_eq_ic_lower:
  "R =↑ S  R =↓ S"
  using upper_ic_lower by auto

lemma convex_eq_ic_lower:
  "R =↕ S  R =↕ S"
  by (meson lower_ic_upper upper_ic_lower)

lemma up_lower_eq_congruence:
  "R =↓ S  R =↓ S"
  by (fact iu_lower_eq_left_congruence)

lemma up_upper_eq_congruence:
  "R =↑ S  R =↑ S"
  by (fact iu_upper_eq_left_congruence)

lemma up_convex_eq_congruence:
  "R =↕ S  R =↕ S"
  by (fact iu_convex_eq_left_congruence)

lemma down_lower_eq_congruence:
  "R =↓ S  R =↓ S"
  by (fact ii_lower_eq_left_congruence)

lemma down_upper_eq_congruence:
  "R =↑ S  R =↑ S"
  by (fact ii_upper_eq_left_congruence)

lemma down_convex_eq_congruence:
  "R =↕ S  R =↕ S"
  by (fact ii_convex_eq_left_congruence)

lemma convex_lower_eq_congruence:
  "R =↓ S  R =↓ S"
  by (simp add: convex_lower_isotone)

lemma convex_upper_eq_congruence:
  "R =↑ S  R =↑ S"
  by (simp add: convex_upper_isotone)

lemma convex_convex_eq_congruence:
  "R =↕ S  R =↕ S"
  by (simp add: convex_lower_isotone convex_upper_isotone)

lemma univalent_lower_eq_subset:
  assumes "univalent S"
    and "S =↓ R"
  shows "S  R"
proof -
  have 1: "a B C. (a, B)  S  (a, C)  S  B = C"
    using assms(1) by (simp add: univalent_set)
  have "a B. (A. (a,A)  S  B  A) = (A. (a,A)  R  B  A)"
    by (meson assms(2) lower_eq)
  hence "a B. (a,B)  S  (a,B)  R"
    using 1 by (smt (verit, del_insts) assms(2) lower_less_eq subset_antisym)
  thus ?thesis
    by (simp add: subset_iff)
qed

lemma univalent_lower_eq:
  assumes "univalent R"
    and "univalent S"
    and "R =↓ S"
  shows "R = S"
  by (meson assms subset_antisym univalent_lower_eq_subset)

lemma univalent_lower_eq_iff:
  assumes "univalent R"
    and "univalent S"
  shows "(R =↓ S)  (R = S)"
  using assms lower_reflexive univalent_lower_eq by auto

lemma univalent_upper_eq_subset:
  assumes "univalent S"
    and "S =↑ R"
  shows "S  R"
proof -
  have 1: "a B C. (a, B)  S  (a, C)  S  B = C"
    using assms(1) by (simp add: univalent_set)
  have "a B. (A. (a,A)  S  A  B) = (A. (a,A)  R  A  B)"
    by (meson assms(2) upper_eq)
  hence "a B. (a,B)  S  (a,B)  R"
    using 1 by (smt (verit) order_refl subset_antisym)
  thus ?thesis
    by (simp add: subset_iff)
qed

lemma univalent_upper_eq:
  assumes "univalent R"
    and "univalent S"
    and "R =↑ S"
  shows "R = S"
  by (meson assms subset_antisym univalent_upper_eq_subset)

lemma univalent_upper_eq_iff:
  assumes "univalent R"
    and "univalent S"
  shows "(R =↑ S)  (R = S)"
  using assms univalent_upper_eq upclosed_ext by blast

lemma univalent_convex_eq_iff:
  assumes "univalent R"
    and "univalent S"
  shows "(R =↕ S)  (R = S)"
  by (metis assms univalent_lower_eq_iff univalent_upper_eq_iff)

lemma total_univalent_upper_ii:
  assumes "total T"
    and "univalent S"
    and "S ⊑↑ T"
  shows "T ∩∩ S = S"
  apply (rule antisym)
   apply (metis assms(2,3) ii_left_isotone univalent_up_ii_idempotent)
  by (metis assms ii_commute lower_ii_lower_bound total_univalent_upper_implies_lower)

lemma lower_eq_down_closed:
  "R =↓ R"
  by (simp add: subset_lower)

lemma upper_eq_up_closed:
  "R =↑ R"
  by (simp add: subset_upper)

lemma convex_eq_up_closed:
  "R =↕ R"
  by (simp add: subset_lower subset_upper)

lemma lower_join:
  "(P . Q ⊑↓ P  R ⊑↓ P  S ⊑↓ P)  Q =↓ R  S"
  by (meson Un_subset_iff lower_reflexive lower_transitive)

lemma lower_meet:
  "(P . P ⊑↓ Q  P ⊑↓ R  P ⊑↓ S)  Q =↓ R ∩∩ S"
  by (metis (no_types, lifting) down_dist_ii_oi le_inf_iff lower_eq_down lower_reflexive)

lemma upper_join:
  "(P . Q ⊑↑ P  R ⊑↑ P  S ⊑↑ P)  Q =↑ R ∪∪ S"
  by (metis (no_types, lifting) convex_increasing le_inf_iff up_dist_iu_oi upper_eq_up)

lemma upper_meet:
  "(P . P ⊑↑ Q  P ⊑↑ R  P ⊑↑ S)  Q =↑ R  S"
  by (meson Un_subset_iff upper_reflexive upper_transitive)

lemma lower_ii_idempotent:
  "R ∩∩ R =↓ R"
  using ii_down lower_reflexive by blast

lemma upper_iu_idempotent:
  "R ∪∪ R =↑ R"
  using iu_up upper_reflexive by auto

lemma lower_iI_idempotent:
  "I  {}  (⋂⋂(λj . R)|I) =↓ R"
  by (metis iI_down lower_eq_down)

lemma upper_iU_idempotent:
  "I  {}  (⋃⋃(λj . R)|I) =↑ R"
  by (metis iU_up upper_eq_up)

lemma down_closed_intersection_closed:
  "R = R  I . I  {}  (⋂⋂(λj . R)|I)  R"
  by (metis lower_iI_idempotent)

lemma up_closed_union_closed:
  "R = R  I . I  {}  (⋃⋃(λj . R)|I)  R"
  by (metis upper_iU_idempotent)

lemma ou_down_lower_eq_ou:
  "R  S =↓ R  S"
  using down_dist_ou lower_eq_down_closed by blast

lemma oi_down_lower_eq_ii:
  "R  S =↓ R ∩∩ S"
  by (simp add: down_dist_ii_oi lower_reflexive)

lemma ou_up_upper_eq_ou:
  "R  S =↑ R  S"
  by (metis ou_upper_isotone up_idempotent upper_reflexive)

lemma oi_up_upper_eq_iu:
  "R  S =↑ R ∪∪ S"
  by (simp add: up_dist_iu_oi upper_reflexive)

lemma oU_down_lower_eq_oU:
  "(RX . R) =↓ X"
  by (metis down_dist_oU lower_eq_down_closed)

lemma oI_down_lower_eq_iI:
  "(iI . X i) =↓ ⋂⋂X|I"
  apply safe
  using down_dist_iI_oI apply fastforce
  by (metis (no_types, lifting) down_dist_iI_oI image_cong image_image lower_eq_down subsetD)

lemma oU_up_upper_eq_oU:
  "(RX . R) =↑ X"
  by (metis up_dist_oU upper_eq_up_closed)

lemma oI_up_upper_eq_iI:
  "(iI . X i) =↑ ⋃⋃X|I"
  by (smt (z3) INT_extend_simps(10) Sup.SUP_cong U_par_idem p_prod_assoc p_prod_comm top_upper_least up_dist_iU_oI upper_ii_upper_bound)

lemma down_order_lower:
  "R  S  R ⊑↓ S"
  by (meson lower_eq_down_closed lower_transitive)

lemma up_order_upper:
  "R  S  S ⊑↑ R"
  by (meson upper_eq_up_closed upper_transitive)

lemma convex_order_lower_upper:
  "R  S  R ⊑↓ S  S ⊑↑ R"
  by (meson convex_eq_up_closed le_inf_iff lower_transitive upper_transitive)

lemma convex_order_Convex:
  "R  S  R ⊑⇕ S"
  by (meson Convex_lower_upper convex_order_lower_upper)

subsection ‹Further results for convex-closure›

lemma convex_down:
  "R = R"
  by (meson convex_eq_up_closed lower_eq_down)

lemma convex_up:
  "R = R"
  by (meson convex_eq_up_closed upper_eq_up)

lemma iu_dist_oi_convex:
  assumes "R = R"
      and "S = S"
      and "T = T"
    shows "(R  S) ∪∪ T = (R ∪∪ T)  (S ∪∪ T)"
  nitpick[expect=genuine,card=1]
  oops

lemma ii_dist_oi_convex:
  assumes "R = R"
      and "S = S"
      and "T = T"
    shows "(R  S) ∩∩ T = (R ∩∩ T)  (S ∩∩ T)"
  nitpick[expect=genuine,card=1]
  oops

lemma oI_up_closed:
  assumes "RX . R = R"
    shows "(X) = X"
  by (meson Inter_iff assms ucl_iff)

lemma oI_down_closed:
  assumes "RX . R = R"
    shows "(X) = X"
  by (metis (no_types, opaque_lifting) antisym assms down_isotone dual_order.refl le_Inf_iff lower_reflexive)

lemma oI_convex_closed:
  assumes "RX . R = R"
    shows "(X) = X"
  by (metis (no_types, lifting) Inf_lower Inter_greatest antisym assms convex_increasing convex_isotone)

lemma up_dist_Union:
  "(X) = { R | R . R  X }"
  by (simp add: Setcompr_eq_image up_dist_oU)

lemma down_dist_Union:
  "(X) = { R | R . R  X }"
  by (simp add: Setcompr_eq_image down_dist_oU)

lemma convex_dist_Union:
  "(X) = { R | R . R  X }"
  nitpick[expect=genuine,card=1,2]
  oops

lemma up_dist_Inter:
  "(X) = { R | R . R  X }"
  nitpick[expect=genuine,card=1]
  oops

lemma down_dist_Inter:
  "(X) = { R | R . R  X }"
  nitpick[expect=genuine,card=1]
  oops

lemma convex_dist_Inter:
  "(X) = { R | R . R  X }"
  nitpick[expect=genuine,card=1,2]
  oops

lemma Inter_convex_closed:
  "(X) = X"
  nitpick[expect=genuine,card=1,2]
  oops

abbreviation "convex_iu" (infixl "∪∪↕" 70)
  where "R ∪∪↕ S  (R ∪∪ S)"

lemma convex_iu:
  "R ∪∪↕ S = (R ∪∪ S)  R  S"
  by (metis Int_assoc Int_commute down_dist_iu up_dist_iu_oi)

lemma convex_iu_sub:
  "R ∪∪ S  R ∪∪↕ S"
  by (meson equalityE iu_Convex_left_isotone)

lemma convex_iu_convex_left:
  "R ∪∪↕ S = R ∪∪↕ S"
  by (simp add: convex_down convex_iu convex_up)

lemma convex_iu_convex_right:
  "R ∪∪↕ S = R ∪∪↕ S"
  by (simp add: convex_down convex_iu convex_up)

lemma convex_iu_convex:
  "R ∪∪↕ S = R ∪∪↕ S"
  by (simp add: convex_down convex_iu convex_up)

lemma convex_iu_assoc:
  "(R ∪∪↕ S) ∪∪↕ T = R ∪∪↕ (S ∪∪↕ T)"
  by (smt convex_iu_convex_left convex_iu_convex_right p_prod_assoc)

lemma convex_iu_comm:
  "R ∪∪↕ S = S ∪∪↕ R"
  by (simp add: p_prod_comm)

lemma convex_iu_unit:
  "R = R  R ∪∪↕ 1 = R"
  by simp

abbreviation "convex_ii" (infixl "∩∩↕" 70)
  where "R ∩∩↕ S  (R ∩∩ S)"

lemma convex_ii:
  "R ∩∩↕ S = (R ∩∩ S)  R  S"
  by (simp add: down_dist_ii_oi inf_assoc up_dist_ii)

lemma convex_ii_sub:
  "R ∩∩ S  R ∩∩↕ S"
  by (meson equalityE ii_Convex_left_isotone)

lemma convex_ii_convex_left:
  "R ∩∩↕ S = R ∩∩↕ S"
  by (simp add: convex_down convex_ii convex_up)

lemma convex_ii_convex_right:
  "R ∩∩↕ S = R ∩∩↕ S"
  by (simp add: convex_down convex_ii convex_up)

lemma convex_ii_convex:
  "R ∩∩↕ S = R ∩∩↕ S"
  by (simp add: convex_down convex_ii convex_up)

lemma convex_ii_assoc:
  "(R ∩∩↕ S) ∩∩↕ T = R ∩∩↕ (S ∩∩↕ T)"
  by (smt convex_ii_convex_left convex_ii_convex_right ii_assoc)

lemma convex_ii_comm:
  "R ∩∩↕ S = S ∩∩↕ R"
  by (simp add: ii_commute)

lemma convex_ii_unit:
  "R = R  R ∩∩↕ 1 = R"
  by simp

lemma convex_iu_ic:
  "(R ∪∪↕ S) = R ∩∩↕ S"
  by (simp add: ic_antidist_iu ic_convex)

lemma convex_ii_ic:
  "(R ∩∩↕ S) = R ∪∪↕ S"
  by (simp add: ic_antidist_ii ic_convex)

abbreviation convex_sup :: "('a,'b) mrel set  ('a,'b) mrel" ("⋃↕") where
  "⋃↕X  (X)"

lemma convex_sup_convex:
  "⋃↕X = (⋃↕X)"
  by simp

lemma convex_sup_inter:
  "⋃↕X = { Y . Y = Y  X  Y }"
  apply (rule antisym)
  apply (smt (verit) Inf_greatest convex_isotone mem_Collect_eq)
  by (smt (verit, del_insts) Inter_lower convex_down convex_increasing convex_up mem_Collect_eq)

lemma convex_iu_dist_convex_sup:
  "⋃↕X ∪∪↕ S = ⋃↕{ R ∪∪↕ S | R . R  X }"
proof -
  have "⋃↕X ∪∪↕ S = X ∪∪↕ S"
    using convex_iu_convex_left by blast
  also have "... = ⋃↕{ R ∪∪ S | R . R  X }"
    by (simp add: Setcompr_eq_image iu_right_dist_oU)
  also have "... = ⋃↕{ R ∪∪↕ S | R . R  X }"
  proof (rule antisym)
    show "⋃↕{ R ∪∪ S | R . R  X }  ⋃↕{ R ∪∪↕ S | R . R  X }"
      by (smt (verit, ccfv_SIG) Convex_transitive Sup_mono dual_order.refl mem_Collect_eq subset_Convex)
    have "RX . R ∪∪↕ S  ⋃↕{ R ∪∪ S | R . R  X }"
      by (smt (verit, ccfv_SIG) Union_upper convex_isotone mem_Collect_eq)
    thus "⋃↕{ R ∪∪↕ S | R . R  X }  ⋃↕{ R ∪∪ S | R . R  X }"
      apply (subst convex_order_Convex)
      apply (rule Union_least)
      by blast
  qed
  finally show ?thesis
    .
qed

lemma convex_ii_dist_convex_sup:
  "⋃↕X ∩∩↕ S = ⋃↕{ R ∩∩↕ S | R . R  X }"
proof -
  have "⋃↕X ∩∩↕ S = X ∩∩↕ S"
    using convex_ii_convex_left by blast
  also have "... = ⋃↕{ R ∩∩ S | R . R  X }"
    by (simp add: Setcompr_eq_image ii_right_dist_oU)
  also have "... = ⋃↕{ R ∩∩↕ S | R . R  X }"
  proof (rule antisym)
    show "⋃↕{ R ∩∩ S | R . R  X }  ⋃↕{ R ∩∩↕ S | R . R  X }"
      by (smt (verit, ccfv_SIG) Convex_transitive Sup_mono dual_order.refl mem_Collect_eq subset_Convex)
    have "RX . R ∩∩↕ S  ⋃↕{ R ∩∩ S | R . R  X }"
      by (smt (verit, ccfv_SIG) Union_upper convex_isotone mem_Collect_eq)
    thus "⋃↕{ R ∩∩↕ S | R . R  X }  ⋃↕{ R ∩∩ S | R . R  X }"
      apply (subst convex_order_Convex)
      apply (rule Union_least)
      by blast
  qed
  finally show ?thesis
    .
qed

lemma convex_dist_sup:
  "(X) = ⋃↕{ R | R . R  X }"
proof (rule antisym)
  have "RX . R  ⋃↕{ R | R . R  X }"
    by (metis (mono_tags, lifting) Sup_upper2 convex_increasing mem_Collect_eq subset_Convex)
  thus "(X)  ⋃↕{ R | R . R  X }"
    by (meson Sup_least convex_order_Convex)
  have "RX . R  (X)"
    by (meson Union_upper convex_isotone)
  thus "⋃↕{ R | R . R  X }  (X)"
    apply (subst convex_order_Convex)
    apply (rule Union_least)
    by blast
qed

section ‹Fusion and Fission›

subsection ‹Atoms and co-atoms›

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

definition co_atoms :: "('a,'b) mrel" ("A")
  where "A  { (a,UNIV - {b}) | a b . True }"

declare atoms_def [mr_simp] co_atoms_def [mr_simp]

lemma atoms_solution:
  "A = -1"
  apply (rule antisym)
   apply (clarsimp simp: mr_simp)
  apply (clarsimp simp: mr_simp)
  by (metis equals0I insert_is_Un mk_disjoint_insert)

lemma atoms_least_solution:
  assumes "R = -1"
  shows "A  R"
proof
  fix x :: "'a × 'b set"
  assume 1: "x  A"
  from this obtain a b where 2: "x = (a,{b})"
    by (smt CollectD atoms_def)
  have 3: "x  R"
    using 1 assms atoms_solution upper_reflexive by fastforce
  have "(a,{})  R"
    by (metis ComplD IntE U_c U_par_idem assms domain_pointwise p_prod_assoc up_dist_iu_oi)
  thus "x  R"
    using 2 3 by (smt (verit) U_par_st subsetD subset_singletonD upclosed_ext)
qed

lemma ic_atoms:
  "A = A"
  apply (clarsimp simp: mr_simp)
  by fastforce

lemma ic_co_atoms:
  "A = A"
  by (metis ic_atoms ic_involutive)

lemma co_atoms_solution:
  "A = -1"
  by (metis atoms_solution ic_atoms ic_dist_oc ic_iu_unit ic_up)

lemma co_atoms_least_solution:
  assumes "R = -1"
  shows "A  R"
  by (metis assms atoms_least_solution ic_atoms ic_dist_oc ic_down ic_ii_unit ic_involutive ic_isotone)

lemma iu_unit_atoms_disjoint:
  "1  A = {}"
  by (metis Compl_disjoint atoms_solution iu_unit_down oi_down_up_iff)

lemma ii_unit_co_atoms_disjoint:
  "1  A = {}"
  using co_atoms_solution lower_reflexive by fastforce

lemma atoms_sp_idempotent:
  "A * A = A"
  by (auto simp: mr_simp)

lemma atoms_sp_cp:
  "(R  A) * S = (R  A)  S"
  by (auto simp: mr_simp)

subsection ‹Inner-functional properties›

abbreviation inner_univalent :: "('a,'b) mrel  bool" where
  "inner_univalent R  R  1  A"

abbreviation inner_total :: "('a,'b) mrel  bool" where
  "inner_total R  R  -1"

abbreviation inner_deterministic :: "('a,'b) mrel  bool" where
  "inner_deterministic R  inner_total R  inner_univalent R"

lemma inner_deterministic_atoms:
  "inner_deterministic R  R  A"
  using atoms_solution upper_reflexive by fastforce

lemma inner_univalent:
  "inner_univalent R  (a b c B . (a,B)  R  b  B  c  B  b = c)"
  apply (clarsimp simp: mr_simp, safe)
   apply blast
  by (smt (z3) UNIV_I UN_iff equals0I insertI1 insert_absorb singleton_insert_inj_eq' subsetI)

lemma inner_univalent_2:
  "inner_univalent R  (a B . (a,B)  R  finite B  card B  one_class.one)"
  apply (rule iffI)
   apply (metis card_eq_0_iff finite.emptyI inner_univalent is_singletonI' is_singleton_altdef linear nonempty_set_card)
  by (metis all_not_in_conv card_1_singletonE eq_iff inner_univalent nonempty_set_card singletonD)

lemma inner_total:
  "inner_total R  (a B . (a,B)  R  (b . b  B))"
  apply (rule iffI)
   apply (smt (verit, del_insts) Collect_empty_eq all_not_in_conv disjoint_eq_subset_Compl p_id_zero_st)
  by (smt (verit) Collect_empty_eq disjoint_eq_subset_Compl ex_in_conv p_id_zero_st)

lemma inner_total_2:
  "inner_total R  (a B . (a,B)  R  B  {})"
  by (meson all_not_in_conv inner_total)

lemma inner_total_3:
  "inner_total R  (a B . (a,B)  R  finite B  card B  one_class.one)"
  by (metis finite.emptyI inner_total_2 nonempty_set_card)

lemma inner_deterministic:
  "inner_deterministic R  (a B . (a,B)  R  (∃!b . b  B))"
  by (metis (no_types, lifting) inner_total inner_univalent)

lemma inner_deterministic_2:
  "inner_deterministic R  (a B . (a,B)  R  card B = one_class.one)"
  by (metis card_1_singletonE eq_iff finite.emptyI finite_insert inner_total_3 inner_univalent_2)

lemma inner_deterministic_sp_unit:
  "inner_deterministic 1"
  by (simp add: inner_deterministic s_id_def)

lemma inner_univalent_down:
  assumes "inner_univalent S"
  shows "S  S  1"
  using assms by (auto simp: mr_simp)

lemma inner_deterministic_lower_eq:
  assumes "inner_deterministic V"
    and "inner_deterministic W"
    and "V =↓ W"
  shows "V = W"
  using assms inner_univalent_down by blast

lemma inner_total_down_closed:
  "inner_total T  R  T  inner_total R"
  by simp

lemma inner_univalent_down_closed:
  "inner_univalent T  R  T  inner_univalent R"
  by simp

lemma inner_deterministic_down_closed:
  "inner_deterministic T  R  T  inner_deterministic R"
  by blast

lemma inner_univalent_convex:
  assumes "inner_univalent R"
  shows "R = R"
  apply (rule antisym)
  using convex_increasing apply blast
  apply (clarsimp simp: mr_simp)
  by (smt (verit) Un_Int_eq(2) Un_Int_eq(3) assms boolean_algebra_cancel.sup0 disjoint_iff inner_univalent semilattice_inf_class.inf.orderE subsetI)

lemma inner_deterministic_alt_closure:
  "inner_deterministic R = (R O converse 1 O 1 = R)"
  apply (clarsimp simp: mr_simp)
  apply safe
    apply force
  by blast+

lemma inner_deterministic_s_id_conv_epsiloff:
  "inner_deterministic R  R O converse s_id = R O epsiloff"
  apply (clarsimp simp: mr_simp)
  unfolding epsiloff_def
  by blast

lemma inner_deterministic_lower_iff:
  assumes "inner_deterministic R"
    and "inner_deterministic S"
  shows "(R ⊑↓ S)  (R  S)"
  apply standard
   apply (smt (verit, ccfv_threshold) Un_commute assms disjoint_eq_subset_Compl inf.orderE inf.orderI inf_commute inf_sup_distrib2 inner_univalent_down sup.orderE sup_bot_left)
  by (simp add: subset_lower)

lemma inner_deterministic_upper_iff:
  assumes "inner_deterministic R"
    and "inner_deterministic S"
  shows "(R ⊑↑ S)  (S  R)"
  apply standard
   apply (clarsimp simp: mr_simp)
  using inner_deterministic apply (smt (verit, del_insts) Ball_Collect Un_subset_iff assms case_prodD subsetD subsetI subset_antisym)
  by (simp add: subset_upper)

lemma inner_deterministic_lower_eq_iff:
  assumes "inner_deterministic R"
    and "inner_deterministic S"
  shows "(R =↓ S)  (R = S)"
  by (meson assms inner_deterministic_lower_eq lower_reflexive)

lemma inner_deterministic_upper_eq_iff:
  assumes "inner_deterministic R"
    and "inner_deterministic S"
  shows "(R =↑ S)  (R = S)"
  by (simp add: antisym assms inner_deterministic_upper_iff)

lemma inner_deterministic_convex_eq_iff:
  assumes "inner_deterministic R"
    and "inner_deterministic S"
  shows "(R =↕ S)  (R = S)"
  by (metis assms inner_deterministic_lower_eq_iff inner_deterministic_upper_eq_iff)

lemma
  "inner_univalent R  inner_univalent S  inner_univalent (R ∪∪ S)"
  nitpick[expect=genuine,card=1,2]
  oops

lemma inner_univalent_ii_closed:
  "inner_univalent R  inner_univalent S  inner_univalent (R ∩∩ S)"
  by (metis (no_types, lifting) Un_subset_iff convex_reflexive down_dist_ii_oi inner_univalent_down inner_univalent_down_closed le_inf_iff subsetI)

lemma inner_total_iu_closed:
  "inner_total R  inner_total S  inner_total (R ∪∪ S)"
  by (metis U_par_idem U_par_p_id atoms_solution c_prod_idr iu_upper_isotone s_prod_p_idl top_upper_least)

lemma
  "inner_total R  inner_total S  inner_total (R ∩∩ S)"
  nitpick[expect=genuine,card=1,2]
  oops

  subsection ‹Fusion›

lemma fusion_set:
  "fus R  { (a,B) . B = { C . (a,C)  R } }"
  unfolding fus_set Image_singleton
  by (smt (verit) Collect_cong Pair_inject case_prodE case_prodI2)

declare fusion_set [mr_simp]

lemma fusion_lower_increasing:
  "R ⊑↓ fus R"
  apply (clarsimp simp: mr_simp)
  by blast

lemma fusion_deterministic:
  "deterministic (fus R)"
  by (simp add: deterministic_set fusion_set)

lemma fusion_least:
  assumes "R ⊑↓ S"
    and "deterministic S"
  shows "fus R ⊑↓ S"
proof (clarsimp simp: mr_simp)
  fix a::'a
  from assms(2) obtain C::"'b set" where 1: "(a,C)  S"
    by (meson deterministic_set)
  hence "{ B . (a,B)  R }  C"
    using assms deterministic_lower by (smt (verit, del_insts) Sup_le_iff mem_Collect_eq)
  thus "C . (D . { B . (a,B)  R } = C  D)  (a,C)  S"
    using 1 by blast
qed

lemma fusion_unique:
  assumes "R . R ⊑↓ f R"
    and "R . deterministic (f R)"
    and "R S . R ⊑↓ S  deterministic S  f R ⊑↓ S"
  shows "f T = fus T"
  apply (rule univalent_lower_eq)
  using assms(2) deterministic_def apply blast
  using deterministic_def fusion_deterministic apply blast
  by (simp add: assms fusion_deterministic fusion_least fusion_lower_increasing)

lemma fusion_down_char:
  "(fus R) = -((-(R)  A))"
proof
  show "(fus R)  -((-(R)  A))"
    apply (clarsimp simp: mr_simp)
    by blast
next
  show "-((-(R)  A))  (fus R)"
  proof (clarsimp simp: mr_simp)
    fix a A
    assume 1: "B . (C . A  B  C)  (C . (D . B = C  D)  (a,C)  R)  (b . B  {b})"
    have "A  { C . (a,C)  R }"
    proof
      fix x
      assume "x  A"
      from this obtain C where "x  C  (a,C)  R"
        using 1 by (metis IntD1 insert_Diff insert_is_Un singletonI)
      thus "x  { C . (a,C)  R }"
        by blast
    qed
    thus "D . A = { C . (a,C)  R }  D"
      by auto
  qed
qed

lemma fusion_up_char:
  "(fus R) = -(((R)  A))"
proof
  show "(fus R)  -(((R)  A))"
    apply (clarsimp simp: mr_simp)
    by blast
next
  show "-(((R)  A))  (fus R)"
  proof (clarsimp simp: mr_simp)
    fix a A
    assume 1: "C . (D . A  C  D)  (B . (D . - C  B  D)  (a,B)  R)  (b . C  UNIV - {b})"
    have "{ C . (a,C)  R }  A"
    proof
      fix x
      assume "x  { C . (a,C)  R }"
      from this obtain C where "x  C  (a,C)  R"
        by blast
      thus "x  A"
        using 1 by (metis Compl_eq_Diff_UNIV Diff_Diff_Int Diff_cancel Diff_eq Diff_insert_absorb Int_commute double_complement insert_Diff insert_inter_insert)
    qed
    thus "C . A = { C . (a,C)  R }  C"
      by auto
  qed
qed

lemma fusion_up_char_2:
  "(fus R) = -(((R  A) * 1))"
  by (simp add: atoms_sp_cp co_prod fusion_up_char ic_atoms ic_dist_oi)

lemma fusion_char:
  "fus R = -((-(R)  A))  -(((R)  A))"
  by (metis deterministic_def fusion_deterministic fusion_down_char fusion_up_char inf_commute univalent_convex)

lemma fusion_char_2:
  "fus R = -((-(R)  A))  -(((R  A) * 1))"
  using fusion_char fusion_up_char fusion_up_char_2 by blast

lemma fusion_lower_isotone:
  "R ⊑↓ S  fus R ⊑↓ fus S"
  by (meson fusion_deterministic fusion_least fusion_lower_increasing lower_transitive)

lemma fusion_iu_idempotent:
  "fus R ∪∪ fus R = fus R"
  using deterministic_def fusion_deterministic univalent_iu_idempotent by blast

lemma fusion_down:
  "fus R = fus (R)"
  by (simp add: fusion_char)

lemma fusion_iu_total:
  "total T  T ∪∪ fus T = fus T"
  by (meson deterministic_def fusion_deterministic fusion_lower_increasing total_univalent_lower_iu)

lemma fusion_deterministic_fixpoint:
  "deterministic R  R = fus R"
  by (metis deterministic_def fusion_deterministic fusion_iu_total fusion_least lower_reflexive p_prod_comm total_univalent_lower_iu)

abbreviation non_empty :: "('a,'b) mrel  ('a,'b) mrel" ("ne _" [100] 100)
  where "ne R  R  -1"

lemma non_empty:
  "ne R = { (a,B) | a B . (a,B)  R  B  {} }"
  by (auto simp: mr_simp)

lemma ne_equality:
  "ne R = R  R  -1"
  by blast

lemma ne_dist_ou:
  "ne (R  S) = ne R  ne S"
  by (fact inf_sup_distrib2)

lemma ne_down_idempotent:
  "ne ((ne (R))) = ne (R)"
  by (auto simp: mr_simp)

lemma ne_up:
  "(ne R) = ne R * 1"
proof
  show "(ne R)  ne R * 1"
    apply (clarsimp simp: mr_simp)
    by (metis UN_constant Un_insert_left insert_absorb)
next
  show "ne R * 1  (ne R)"
  proof (clarsimp simp: mr_simp)
    fix a B f
    assume 1: "(a,B)  R" and 2: "B  {}" and "bB . C . f b = insert b C"
    hence "B  (xB . f x)"
      by blast
    thus "D . (C . (xB . f x) = D  C)  (a,D)  R  D  {}"
      using 1 2 by blast
  qed
qed

lemma ne_dist_down_sp:
  "ne (R * S) = ne (R) * ne S"
proof (rule antisym)
  show "ne (R * S)  ne (R) * ne S"
  proof (clarsimp simp: mr_simp)
    fix a C f D x
    assume 1: "(a,C)  R" and 2: "bCD . (b,f b)  S" and 3: "f x  {}" and 4: "x  C" and 5: "x  D"
    let ?B = "{ bCD . f b  {} }"
    have 6: "C . (D . ?B = C  D)  (a,C)  R"
      using 1 by auto
    have 7: "?B  {}"
      using 3 4 5 by auto
    have 8: "b?B . (b,f b)  S  f b  {}"
      using 2 by auto
    have "(xCD . f x) = (x?B . f x)"
      by auto
    thus "B . (C . (D . B = C  D)  (a,C)  R)  B  {}  (g . (bB . (b,g b)  S  g b  {})  (xCD . f x) = (xB . g x))"
      using 6 7 8 by blast
  qed
next
  show "ne (R) * ne S  ne (R * S)"
    by (clarsimp simp: mr_simp) blast
qed

lemma total_ne_down_dist_sp:
  "total T  ne ((R * T)) = ne (R) * ne (T)"
  by (simp add: ne_dist_down_sp total_down_dist_sp)

lemma inner_univalent_char:
  "inner_univalent S  (R . fus R = fus S  R ⊑↓ S  ne R = ne S)"
proof
  assume 1: "inner_univalent S"
  show "R . fus R = fus S  R ⊑↓ S  ne R = ne S"
  proof (rule allI, rule impI)
    fix R
    assume 2: "fus R = fus S  R ⊑↓ S"
    show "ne R = ne S"
    proof (rule antisym)
      show "ne R  ne S"
      proof
        fix x
        assume 3: "x  ne R"
        from this obtain a B where 4: "x = (a,B)  x  R  B  {}"
          by (metis Int_iff Int_lower2 inner_total_2 surj_pair)
        from this obtain C where 5: "B  C  (a,C)  S"
          using 2 by (meson lower_less_eq)
        from this obtain b where "C = {b}"
          using 1 4 by (metis Un_empty inner_univalent is_singletonI' is_singleton_the_elem subset_Un_eq)
        hence "B = C"
          using 4 5 by blast
        thus "x  ne S"
          using 3 4 5 by blast
      qed
    next
      show "ne S  ne R"
      proof
        fix x
        assume 6: "x  ne S"
        from this obtain a B where 7: "x = (a,B)  x  S  B  {}"
          by (metis Int_absorb Int_iff inner_total_2 semilattice_inf_class.inf.absorb_iff2 surj_pair)
        from this obtain b where 8: "B = {b}"
          using 1 by (meson antisym card_1_singletonE inner_univalent_2 nonempty_set_card)
        from this obtain C where 9: "b  C  (a,C)  fus S"
          using 7 by (meson fusion_lower_increasing insert_subset lower_less_eq)
        hence "(a,C)  fus R"
          using 2 by simp
        hence "C = { D . (a,D)  R }"
          by (clarsimp simp: mr_simp)
        from this obtain D where 10: "b  D  (a,D)  R"
          using 9 by blast
        from this obtain E where 11: "D  E  (a,E)  S"
          using 2 by (meson lower_less_eq)
        from this obtain c where "E = {c}"
          using 1 10 by (metis antisym card_1_singletonE empty_iff inner_univalent_2 nonempty_set_card subsetI)
        hence "D = {b}"
          using 10 11 by blast
        thus "x  ne R"
          using 6 7 8 10 by blast
      qed
    qed
  qed
next
  assume 12: "R . fus R = fus S  R ⊑↓ S  ne R = ne S"
  show "inner_univalent S"
  proof (unfold inner_univalent, intro allI, rule impI)
    fix a b c B
    assume 13: "(a,B)  S  b  B  c  B"
    let ?R = "{ (f,{e}) | f e . C . (f,C)  S  e  C }"
    have 14: "fus ?R = fus S"
      apply (clarsimp simp: mr_simp)
      by blast
    have "?R ⊑↓ S"
      using lower_less_eq by fastforce
    hence "ne ?R = ne S"
      using 12 14 by simp
    hence "(a,B)  ?R"
      using 13 by (smt (verit, del_insts) empty_iff mem_Collect_eq non_empty)
    thus "b = c"
      using 13 by blast
  qed
qed

lemma ne_dist_oU:
  "ne (X) = (non_empty ` X)"
  by blast

subsection ‹Fission›

lemma fission_set:
  "fis R = { (a,{b}) | a b . B . (a,B)  R  b  B }"
  unfolding fis_set Image_singleton
  by simp

declare fission_set [mr_simp]

lemma fission_var:
  "fis R = R  A"
  apply (clarsimp simp: mr_simp)
  by blast

lemma fission_lower_decreasing:
  "fis R ⊑↓ R"
  by (simp add: fission_var)

lemma fission_inner_deterministic:
  "inner_deterministic (fis R)"
  by (simp add: fission_var inner_deterministic_atoms)

lemma fission_greatest:
  assumes "S ⊑↓ R"
    and "inner_deterministic S"
  shows "S ⊑↓ fis R"
proof (clarsimp simp: mr_simp)
  fix a B
  assume 1: "(a,B)  S"
  from this obtain b where 2: "B = {b}"
    using assms(2) by (meson card_1_singletonE inner_deterministic_2)
  from 1 obtain C where "B  C  (a,C)  R"
    using assms(1) by (meson lower_less_eq)
  thus "C . (D . B = C  D)  (b . C = {b}  (E . (a,E)  R  b  E))"
    using 2 by auto
qed

lemma fission_unique:
  assumes "R . f R ⊑↓ R"
    and "R . inner_deterministic (f R)"
    and "R S . S ⊑↓ R  inner_deterministic S  S ⊑↓ f R"
  shows "f T = fis T"
  apply (rule inner_deterministic_lower_eq)
    apply (simp add: assms(2))
   apply (simp add: fission_inner_deterministic)
  by (simp add: assms fission_greatest fission_inner_deterministic fission_lower_decreasing)

lemma fission_lower_isotone:
  "R ⊑↓ S  fis R ⊑↓ fis S"
  by (meson fission_greatest fission_inner_deterministic fission_lower_decreasing lower_transitive)

lemma fission_idempotent:
  "fis (fis R) = fis R"
  by (metis comp_apply fis_fis)

lemma fission_top:
  "fis U = A"
  using fission_var top_down top_upper_least by fastforce

lemma fission_down:
  "fis R = fis (R)"
  by (simp add: fission_var)

lemma fission_ne_fixpoint:
  "fis R = ne (fis R)"
  using fission_inner_deterministic by blast

lemma fission_down_ne_fixpoint:
  "fis R = ne ((fis R))"
  by (metis fission_inner_deterministic fission_ne_fixpoint fusion_down inner_univalent_char lower_ii_decreasing)

lemma fission_inner_deterministic_fixpoint:
  "inner_deterministic R  R = fis R"
  apply (rule iffI)
   apply (metis comp_eq_dest_lhs fission_lower_decreasing fission_ne_fixpoint fus_fis inner_univalent_char le_iff_inf)
  using fission_inner_deterministic by auto

lemma fission_sp_subdist:
  "fis (R * S)  fis R * fis S"
proof
  fix x
  assume "x  fis (R * S)"
  from this obtain a b B where 1: "x = (a,{b})  (a,B)  R * S  b  B"
    by (smt CollectD fission_set)
  from this obtain C f where 2: "(a,C)  R  (c  C . (c,f c)  S)  B = { f c | c . c  C }"
    by (simp add: mr_simp) blast
  from this obtain c where 3: "b  f c  c  C"
    using 1 by blast
  let ?B = "{c}"
  let ?f = "λx . {b}"
  have 4: "(a,?B)  fis R"
    using 2 3 fission_set by blast
  have 5: "b?B . (b,?f b)  fis S"
    using 2 3 fission_set by blast
  have "{b} = { ?f b | b . b  ?B }"
    by simp
  hence "f . (b?B . (b,f b)  fis S)  {b} = { f b | b . b  ?B }"
    using 5 by auto
  hence "(a,{b})  fis R * fis S"
    apply (unfold s_prod_def)
    using 4 by auto
  thus "x  fis R * fis S"
    using 1 by simp
qed

lemma fission_sp_total_dist:
  assumes "total T"
  shows "fis (R * T) = fis R * fis T"
  by (metis assms atoms_sp_idempotent fis_lax fission_var sp_oi_subdist_2 subset_antisym total_down_dist_sp)

lemma fission_dist_ou:
  "fis (R  S) = fis R  fis S"
  by (simp add: down_dist_ou fission_var inf_sup_distrib2)

lemma fission_sp_iu_unit:
  "fis (R * 1) = {}"
  by (metis c_nc down_sp fission_lower_decreasing nu_def nu_fis nu_fis_var s_prod_zerol subset_empty)

lemma fission_fusion_lower_decreasing:
  "fis (fus R) ⊑↓ R"
  apply (clarsimp simp: mr_simp)
  by blast

lemma fusion_fission_lower_increasing:
  "R ⊑↓ fus (fis R)"
  apply (clarsimp simp: mr_simp)
  by blast

lemma fission_fusion_galois:
  "fis R ⊑↓ S  R ⊑↓ fus S"
  apply (rule iffI)
   apply (meson fusion_fission_lower_increasing fusion_lower_isotone lower_transitive)
  by (meson fission_fusion_lower_decreasing fission_lower_isotone lower_transitive)

lemma fission_fusion:
  "fis (fus R) = fis R"
  by (metis fission_fusion_lower_decreasing fission_idempotent fission_inner_deterministic fission_lower_isotone fusion_lower_increasing inner_deterministic_lower_eq)

lemma fusion_fission:
  "fus (fis R) = fus R"
  by (metis comp_def fus_fis)

lemma same_fusion_fission_lower:
  "fus R = fus S  fis R ⊑↓ S"
  by (metis fission_fusion_galois fusion_lower_increasing)

lemma fission_below_ne_down_fusion:
  "fis R  ne ((fus R))"
  using fission_fusion fission_inner_deterministic fission_lower_decreasing by blast

lemma ne_fusion_fission:
  "(ne ((fus R))) = (fis R)"
  by (metis (mono_tags, lifting) atoms_solution fission_below_ne_down_fusion fission_fusion oi_down_sub_up subset_trans upper_eq_up upper_reflexive fission_var)

lemma fission_up_ne_down_up:
  "(fis R) = (ne (R))"
  by (metis (mono_tags, lifting) atoms_solution fission_ne_fixpoint fission_top oi_down_sub_up semilattice_inf_class.inf_le2 semilattice_inf_class.inf_left_commute subset_trans upper_eq_up fission_var)

lemma fusion_idempotent:
  "fus (fus R) = fus R"
  by (metis fission_fusion fusion_fission)

lemma fission_dist_oU:
  "fis (X) = (fis ` X)"
  by (metis (no_types, lifting) SUP_cong UN_simps(4) fission_var ii_right_dist_oU)

subsection ‹Co-fusion and co-fission›

definition co_fusion :: "('a,'b) mrel  ('a,'b) mrel" ("⨅⨅ _" [80] 80) where
  "⨅⨅R  { (a,B) . B = { C . (a,C)  R } }"

declare co_fusion_def [mr_simp]

lemma co_fusion_upper_decreasing:
  "⨅⨅R ⊑↑ R"
  apply (clarsimp simp: mr_simp)
  by blast

lemma co_fusion_deterministic:
  "deterministic (⨅⨅R)"
  by (simp add: deterministic_set co_fusion_def)

lemma co_fusion_greatest:
  assumes "S ⊑↑ R"
    and "deterministic S"
  shows "S ⊑↑ ⨅⨅R"
proof (clarsimp simp: mr_simp)
  fix a
  from assms(2) obtain B where 1: "(a,B)  S"
    by (meson deterministic_set)
  hence "B  { C . (a,C)  R }"
    using assms deterministic_upper by (smt (verit, ccfv_threshold) Inter_greatest mem_Collect_eq)
  thus "B . (D . { C . (a,C)  R } = B  D)  (a,B)  S"
    using 1 by blast
qed

lemma co_fusion_unique:
  assumes "R . f R ⊑↑ R"
    and "R . deterministic (f R)"
    and "R S . S ⊑↑ R  deterministic S  S ⊑↑ f R"
  shows "f T = ⨅⨅T"
  apply (rule univalent_upper_eq)
  using assms(2) deterministic_def apply blast
  using co_fusion_deterministic deterministic_def apply blast
  by (simp add: assms co_fusion_deterministic co_fusion_greatest co_fusion_upper_decreasing)

lemma co_fusion_up_char:
  "(⨅⨅R) = -((-(R)  A))"
proof
  show "(⨅⨅R)  -((-(R)  A))"
    apply (clarsimp simp: mr_simp)
    by blast
next
  show "-((-(R)  A))  (⨅⨅R)"
  proof (clarsimp simp: mr_simp)
    fix a A
    assume 1: "B . (C . A  B  C)  (C . (D . B = C  D)  (a,C)  R)  (b . B  UNIV - {b})"
    have "{ C . (a,C)  R }  A"
    proof
      fix x
      assume "x  { C . (a,C)  R }"
      hence "C . A  (UNIV - {x})  C"
        using 1 by blast
      thus "x  A"
        by blast
    qed
    thus "D . A = { C . (a,C)  R }  D"
      by auto
  qed
qed

lemma co_fusion_down_char:
  "(⨅⨅R) = -(((R)  A))"
proof
  show "(⨅⨅R)  -(((R)  A))"
    apply (clarsimp simp: mr_simp)
    by blast
next
  show "-(((R)  A))  (⨅⨅R)"
  proof (clarsimp simp: mr_simp)
    fix a A
    assume 1: "C . (D . A  C  D)  (B . (D . - C  B  D)  (a,B)  R)  (b . C  {b})"
    have "A  { C . (a,C)  R }"
    proof
      fix x
      assume "x  A"
      hence "B . (D . - {x}  B  D)  (a,B)  R"
        using 1 by blast
      thus "x  { C . (a,C)  R }"
        by blast
    qed
    thus "C . A = { C . (a,C)  R }  C"
      by auto
  qed
qed

lemma co_fusion_down_char_2:
  "(⨅⨅R) = -(((R  A)  1))"
  by (metis co_fusion_down_char ic_co_atoms ic_cp_ic_unit ic_dist_oi)

lemma co_fusion_char:
  "⨅⨅R = -((-(R)  A))  -(((R)  A))"
  by (metis deterministic_def co_fusion_deterministic co_fusion_down_char co_fusion_up_char univalent_convex)

lemma co_fusion_char_2:
  "⨅⨅R = -((-(R)  A))  -(((R  A)  1))"
  using co_fusion_char co_fusion_down_char co_fusion_down_char_2 by blast

lemma co_fusion_upper_isotone:
  "R ⊑↑ S  ⨅⨅R ⊑↑ ⨅⨅S"
  by (meson co_fusion_deterministic co_fusion_greatest co_fusion_upper_decreasing upper_transitive)

lemma co_fusion_ii_idempotent:
  "⨅⨅R ∩∩ ⨅⨅R = ⨅⨅R"
  by (metis deterministic_def co_fusion_deterministic univalent_ii_idempotent)

lemma co_fusion_up:
  "⨅⨅R = ⨅⨅(R)"
  by (simp add: co_fusion_char)

lemma co_fusion_ii_total:
  "total T  T ∩∩ ⨅⨅T = ⨅⨅T"
  by (meson co_fusion_deterministic co_fusion_upper_decreasing deterministic_def total_univalent_upper_ii)

lemma co_fusion_deterministic_fixpoint:
  "deterministic R  R = ⨅⨅R"
  apply (rule iffI)
   apply (metis deterministic_def co_fusion_deterministic co_fusion_greatest co_fusion_ii_total ii_commute total_univalent_upper_ii upper_reflexive)
  by (metis co_fusion_deterministic)

abbreviation co_fission :: "('a,'b) mrel  ('a,'b) mrel" ("at _" [80] 80) where
  "at R  R  A"

lemma co_fission:
  "at R = { (a,B) | a B . (b . -B = {b})  (C . (a,C)  R  C  B) }"
  apply (clarsimp simp: mr_simp)
  by blast

declare co_fission [mr_simp]

lemma co_fission_upper_increasing:
  "R ⊑↑ at R"
  by (fact semilattice_inf_class.inf_le1)

lemma co_fission_ic_inner_deterministic:
  "inner_deterministic (at R)"
  by (simp add: ic_co_atoms ic_dist_oi inner_deterministic_atoms)

lemma co_fission_least:
  assumes "R ⊑↑ S"
    and "inner_deterministic (S)"
  shows "at R ⊑↑ S"
proof (clarsimp simp: mr_simp)
  fix a B
  assume 1: "(a,B)  S"
  hence "(a,-B)  S"
    by (simp add: inner_complement_def)
  from this obtain b where 2: "-B = {b}"
    using assms(2) by (meson card_1_singletonE inner_deterministic_2)
  from 1 obtain C where "C  B  (a,C)  R"
    using assms(1) by (meson upper_less_eq)
  thus "C . (D . B = C  D)  (E . (D . C = E  D)  (a,E)  R)  (b . C = UNIV - {b})"
    using 2 by (metis Compl_eq_Diff_UNIV double_compl subset_Un_eq sup.idem)
qed

lemma co_fission_unique:
  assumes "R . R ⊑↑ f R"
    and "R . inner_deterministic (f R)"
    and "R S . R ⊑↑ S  inner_deterministic (S)  f R ⊑↑ S"
  shows "f T = at T"
  apply (rule ic_injective)
  apply (rule inner_deterministic_lower_eq)
    apply (simp add: assms(2))
   apply (simp add: co_fission_ic_inner_deterministic)
  by (meson assms co_fission_ic_inner_deterministic co_fission_least semilattice_inf_class.inf_le1 upper_ic_lower)

lemma co_fission_upper_isotone:
  "R ⊑↑ S  at R ⊑↑ at S"
  by (simp add: oi_subset_upper_left_antitone upper_transitive)

lemma co_fission_idempotent:
  "at (at R) = at R"
  by (meson equalityI semilattice_inf_class.inf_le1 semilattice_inf_class.inf_le2 semilattice_inf_class.le_inf_iff upper_reflexive upper_transitive)

lemma co_fission_top:
  "at U = A"
  using top_lower_greatest U_par_idem top_down by blast

lemma co_fission_up:
  "at R = at (R)"
  by simp

lemma co_fission_ic_inner_deterministic_fixpoint:
  "inner_deterministic (R)  R = at R"
  apply (rule iffI)
   apply (simp add: fission_var fission_inner_deterministic_fixpoint ic_antidist_iu ic_co_atoms ic_dist_oi ic_injective ic_up)
  by (metis co_fission_ic_inner_deterministic)

lemma co_fusion_co_fission_upper_decreasing:
  "⨅⨅(at R) ⊑↑ R"
proof (clarsimp simp: mr_simp)
  fix a B
  assume 1: "(a,B)  R"
  have "{ D . (E . (F . D = E  F)  (a,E)  R)  (b . D = UNIV - {b}) }  B"
  proof
    fix x
    assume 2: "x  { D . (E . (F . D = E  F)  (a,E)  R)  (b . D = UNIV - {b}) }"
    show "x  B"
    proof (rule ccontr)
      let ?D = "-{x}"
      assume 3: "x  B"
      hence "B  ?D"
        by simp
      hence "{ D . (E . (F . D = E  F)  (a,E)  R)  (b . D = UNIV - {b}) }  ?D"
        using 1 by (smt CollectI Compl_eq_Diff_UNIV Inf_lower subset_Un_eq)
      thus False
        using 2 by auto
    qed
  qed
  thus "C . B = { D . (E . (F . D = E  F)  (a,E)  R)  (b . D = UNIV - {b}) }  C"
    by auto
qed

lemma co_fission_co_fusion_upper_increasing:
  "R ⊑↑ at (⨅⨅R)"
proof (clarsimp simp: mr_simp)
  fix a b B
  assume "{ C . (a,C)  R }  B = UNIV - {b}"
  hence "b  { C . (a,C)  R }"
    by blast
  hence "C . b  C  (a,C)  R"
    by blast
  thus "C . (D . UNIV - {b} = C  D)  (a,C)  R"
    by blast
qed

lemma co_fusion_co_fission_galois:
  "⨅⨅R ⊑↑ S  R ⊑↑ at S"
  apply (rule iffI)
   apply (meson co_fission_co_fusion_upper_increasing co_fission_upper_isotone upper_transitive)
  by (meson co_fusion_co_fission_upper_decreasing co_fusion_upper_isotone upper_transitive)

lemma co_fission_co_fusion:
  "at (⨅⨅R) = at R"
  using co_fission_co_fusion_upper_increasing co_fission_idempotent co_fission_upper_isotone co_fusion_upper_decreasing by blast

lemma co_fusion_co_fission:
  "⨅⨅(at R) = ⨅⨅R"
  apply (rule antisym)
   apply (metis deterministic_def co_fission_co_fusion co_fission_co_fusion_upper_increasing co_fusion_co_fission_upper_decreasing co_fusion_deterministic co_fusion_upper_isotone univalent_upper_eq_subset)
  by (metis deterministic_def co_fission_co_fusion co_fission_co_fusion_upper_increasing co_fusion_co_fission_upper_decreasing co_fusion_deterministic co_fusion_upper_isotone univalent_upper_eq_subset)

lemma same_co_fusion_co_fission_upper:
  "⨅⨅R = ⨅⨅S  S ⊑↑ at R"
  by (metis co_fusion_co_fission_galois co_fusion_upper_decreasing)

lemma co_fusion_idempotent:
  "⨅⨅(⨅⨅R) = ⨅⨅R"
  by (metis co_fission_co_fusion co_fusion_co_fission)

section ‹Modalities›

subsection ‹Tests›

abbreviation test :: "('a,'a) mrel  bool" where
  "test R  R  1"

lemma test:
  "test R  (a B . (a,B)  R  B = {a})"
  by (force simp: s_id_def)

lemma test_fix: "test R  R  1σ = R"
  by (simp add: le_iff_inf)

lemma test_ou_closed:
  "test p  test q  test (p  q)"
  by (fact sup_least)

lemma test_oi_closed:
  "test p  test (p  q)"
  by blast

abbreviation test_complement :: "('a,'a) mrel  ('a,'a) mrel" (" _" [80] 80) where
  " R  -R  1"

lemma test_complement_closed:
  "test ( p)"
  by simp

lemma test_double_complement:
  "test p  p =   p"
  by blast

lemma test_complement:
  "(a,{a})   p  ¬ (a,{a})  p"
  by (simp add: s_id_def)

declare test_complement [mr_simp]

lemma test_complement_antitone:
  assumes "test p"
  shows "p  q   q   p"
  using assms(1) by blast

lemma test_complement_huntington:
  "test p  p =  ( p   q)   ( p  q)"
  by blast

abbreviation test_implication :: "('a,'a) mrel  ('a,'a) mrel  ('a,'a) mrel" (infixl "" 65) where
  "p  q   p  q"

lemma test_implication_closed:
  "test q  test (p  q)"
  by simp

lemma test_implication:
  "(a,{a})  p  q  ((a,{a})  p  (a,{a})  q)"
  by (simp add: s_id_def)

declare test_implication [mr_simp]

lemma test_implication_left_antitone:
  assumes "test p"
  shows "p  r  r  q  p  q"
  by blast

lemma test_implication_right_isotone:
  assumes "test p"
  shows "q  r  p  q  p  r"
  by blast

lemma test_sp_idempotent:
  "test p  p * p = p"
  by (metis d_rest_ax inf.order_iff s_subid_iff2)

lemma test_sp:
  assumes "test p"
  shows "p * R = (p * U)  R"
  apply (clarsimp simp: mr_simp)
  apply safe
    apply blast
  using assms subid_aux2 by fastforce+

lemma sp_test:
  "test p  R * p = R  (U * p)"
  apply (rule antisym)
   apply (metis (no_types, lifting) U_par_idem inf.absorb_iff2 inf.idem le_inf_iff s_prod_idr sp_oi_subdist top_upper_least)
  using test_fix by (smt IntE s_prod_test_aux1 s_prod_test_aux2 subrelI)

lemma sp_test_dist_oi:
  "test p  (R  S) * p = (R * p)  (S * p)"
  by (smt Int_left_commute semilattice_inf_class.inf.assoc semilattice_inf_class.inf.right_idem sp_test)

lemma sp_test_dist_oi_left:
  "test p  (R  S) * p = (R * p)  S"
  by (smt Int_commute semilattice_inf_class.inf.left_commute sp_test)

lemma sp_test_dist_oi_right:
  "test p  (R  S) * p = R  (S * p)"
  by (metis semilattice_inf_class.inf.commute sp_test_dist_oi_left)

lemma sp_test_sp_oi_left:
  "test p  (R  (U * p)) * T = R * p * T"
  by (metis sp_test)

lemma sp_test_sp_oi_right:
  "test p  R * ((p * U)  T) = R * p * T"
  by (metis inf.orderE test_assoc1 test_sp)

lemma test_sp_ne:
  "test p  p * ne R = ne (p * R)"
  by (smt lattice_class.inf_sup_aci(1) lattice_class.inf_sup_aci(3) test_sp)

lemma ne_sp_test:
  "test p  ne R * p = ne (R * p)"
  by (fact sp_test_dist_oi_left)

lemma top_sp_test_down_closed:
  assumes "test p"
  shows "U * p = (U * p)"
proof -
  have 1: "p  1σ = p"
    using assms by blast
  hence "(U * p) = {(a,A). (a,A)  U  (a  A. (a,{a})  p)} ∩∩ U"
    by (smt (verit) Collect_cong case_prodI2 case_prod_conv s_prod_test_var)
  also have " = {(a,A). a  A. (a,{a})  p} ∩∩ U"
    by (smt (verit) Collect_cong ii_assoc lower_ii_down mem_Collect_eq split_cong subsetD top_down)
  also have " = {(a,A). (a,A)  U  (a  A. (a,{a})  p)}"
    by (auto simp: mr_simp)
  also have " = U * p"
    using 1 by (smt (verit) Collect_cong case_prodI2 case_prod_conv s_prod_test_var)
  finally show ?thesis
    by blast
qed

lemma oc_top_sp_test_up_closed:
  "test p  -(U * p) = (-(U * p))"
  by (metis antisym convex_reflexive disjoint_eq_subset_Compl inf_compl_bot oi_down_up_iff semilattice_inf_class.inf.commute top_sp_test_down_closed)

lemma top_sp_test:
  "test p  (a,B)  U * p  (bB . (b,{b})  p)"
  using test_fix by (metis IntE UNIV_I s_prod_test sp_test)

lemma oc_top_sp_test:
  "test p  (a,B)  -(U * p)  (bB . (b,{b})  p)"
  by (simp add: top_sp_test)

declare top_sp_test [mr_simp] oc_top_sp_test [mr_simp]

lemma oc_top_sp_test_0:
  "-1 *  p = ne (U *  p)"
  by (metis Int_lower1 semilattice_inf_class.inf.commute sp_test)

lemma oc_top_sp_test_1:
  assumes "test p"
  shows "-(U * p) = (ne (U *  p))"
proof (rule antisym)
  show "-(U * p)  (ne (U *  p))"
  proof
    fix x::"'c × 'a set"
    assume 1: "x  -(U * p)"
    from this obtain a B where 2: "x = (a,B)"
      by force
    from this obtain c where 3: "c  B  (c,{c})  p"
      using 1 by (meson assms oc_top_sp_test)
    hence 4: "(a,{c})  U *  p"
      by (metis singletonD test_complement test_complement_closed top_sp_test)
    have "(a,{c})  -1"
      using oc_top_sp_test by (smt (verit, del_insts) ComplI Int_iff assms boolean_algebra.conj_cancel_left inf.coboundedI2 p_id_zero s_prod_test_aux1 singleton_iff)
    hence "(a,{c})  ne (U *  p)"
      using 4 by simp
    thus "x  (ne (U *  p))"
      using 2 3 by (metis (no_types, lifting) U_par_st singletonD subset_eq)
  qed
next
  have "(U * p) = U * p"
    using assms top_sp_test_down_closed by auto
  also have "...  -(-1 *  p)"
    by (smt (verit) Compl_disjoint assms disjoint_eq_subset_Compl inf_commute oc_top_sp_test_0 p_id_zero s_prod_idl sp_test_dist_oi_right test_assoc1 test_double_complement)
  also have "... = -ne (U *  p)"
    by (simp add: oc_top_sp_test_0)
  finally have "U * p  -((ne (U *  p)))"
    by (simp add: down_double_complement_up)
  thus "(ne (U *  p))  -(U * p)"
    by auto
qed

lemma oc_top_sp_test_2:
  "test p  -(U * p) = (-1 *  p)"
  by (simp add: oc_top_sp_test_1 oc_top_sp_test_0)

lemma split_sp_test:
  assumes "test p"
  shows "R = (R * p)  (ne R  (ne (R *  p)))"
proof (rule antisym)
  show "R  (R * p)  (ne R  (ne (R *  p)))"
  proof
    fix x
    assume 1: "x  R"
    from this obtain a B where 2: "x = (a,B)"
      by force
    show "x  (R * p)  (ne R  (ne (R *  p)))"
    proof (cases "bB . (b,{b})  p")
      case True
      hence "(a,B)  U * p"
        by (simp add: assms top_sp_test)
      thus ?thesis
        using 1 2 by (metis Int_iff UnCI assms sp_test)
    next
      case False
      from this obtain b where 3: "{b}  B  (b,{b})  p"
        by auto
      hence "(a,{b})  R"
        using 1 2 down by fastforce
      hence "(a,{b})  R *  p"
        using 3 by (metis s_prod_test_aux2 singletonD test_complement)
      hence "(a,{b})  ne (R *  p)"
        by (simp add: non_empty)
      hence "(a,B)  (ne (R *  p))"
        using 3 by (meson U_par_st)
      thus ?thesis
        using 1 2 3 non_empty by auto
    qed
  qed
next
  show "(R * p)  (ne R  (ne (R *  p)))  R"
    using assms sp_test by auto
qed

lemma top_sp_test_down_iff_1:
  assumes "test p"
  shows "R  U * p  R  U * p"
  by (smt (verit, del_insts) assms down_order_lower top_sp_test_down_closed)

lemma test_ne:
  "test p  ne p = p"
  using inner_deterministic_sp_unit by blast

lemma ne_test_up:
  "test p  ne (p) = p"
  by (metis atoms_solution ne_equality test_ne up_idempotent up_isotone)

lemma ne_sp_test_up:
  "test p  (ne (R * p)) = ne R * p"
  using test_fix by (smt ne_up sp_test_dist_oi_left test_assoc1 test_ne)

lemma ne_down_sp_test_up:
  "test p  ne (R * p) = ne (R) * p"
  by (simp add: ne_dist_down_sp ne_test_up)

lemma test_up_sp:
  "test p  p = p * 1"
  by (metis ne_up test_ne)

lemma top_test_oi_top_complement:
  "test p  (U * p)  (U *  p) = 1"
  by (smt (verit) Compl_disjoint U_par_idem inf.absorb_iff2 inf_commute p_id_zero s_prod_idl sp_test_dist_oi_right test_assoc1 top_upper_least)

lemma sp_test_oi_complement:
  "test p  (R * p)  (R *  p) = R  1"
  by (smt semilattice_inf_class.inf_idem sp_test sp_test_dist_oi_left sp_test_dist_oi_right test_complement_closed top_test_oi_top_complement)

lemma ne_top_sp_test_complement:
  assumes "test p"
  shows "ne (U * p) *  p = {}"
  by (metis Compl_disjoint Int_assoc assms oc_top_sp_test_0 semilattice_inf_class.inf_le2 sp_test_dist_oi_right top_test_oi_top_complement)

lemma complement_test_sp_top:
  assumes "test p"
  shows "-(p * U) =  p * U"
proof -
  have "-(p * U) = -{(a,A). (a,{a})  p  (a,A)  U}"
    by (metis (no_types, lifting) Collect_cong assms inf.orderE split_cong test_s_prod_var)
  also have " = -{(a,A). (a,{a})  p}"
    using top_upper_least by auto
  also have " = {(a,A). (a,{a})  p}"
    by force
  also have " = {(a,A). (a,{a})   p}"
    by (meson test_complement)
  also have " = {(a,A). (a,{a})   p  (a,A)  U}"
    using U_par_idem top_upper_least by auto
  also have " =   p * U"
    by (simp add: test_s_prod_var)
  finally show ?thesis
    .
qed

lemma top_sp_test_shunt:
  assumes "test p"
  shows "R  U * p  R *  p  1"
  by (metis assms inf.absorb_iff1 sp_test sp_test_dist_oi test_complement_closed top_test_oi_top_complement)

lemma top_sp_test_down_iff_2:
  assumes "test p"
  shows "R  U * p  R *  p  1"
proof
  assume "R  U * p"
  thus "R *  p  1"
    using assms top_sp_test_shunt by blast
next
  assume 1: "R *  p  1"
  have "R  U * p"
  proof
    fix x
    assume "x  R"
    from this obtain a B where 2: "x = (a,B)  x  R"
      by force
    have "bB . (b,{b})  p"
    proof
      fix b
      assume 3: "b  B"
      have "(b,{b})   p"
      proof
        assume 4: "(b,{b})   p"
        have "(a,{b})  R"
          using 2 3 down by fastforce
        hence "(a,{b})  R *  p"
          using 4 by (simp add: s_prod_test)
        thus False
          using 1 by (metis Pair_inject domain_pointwise insert_not_empty p_subid_iff)
      qed
      thus "(b,{b})  p"
        by (meson test_complement)
    qed
    thus "x  U * p"
      using 2 by (simp add: assms top_sp_test)
  qed
  thus "R  U * p"
    using assms top_sp_test_down_iff_1 by blast
qed

lemma top_sp_test_down_iff_3:
  "R *  p  1  ne (R) *  p  {}"
  by (simp add: disjoint_eq_subset_Compl ne_sp_test)

lemma top_sp_test_down_iff_4:
  assumes "test p"
  shows "R  (U *  p)  1  R  1  (U * p)"
  by (metis assms lattice_class.sup_inf_absorb semilattice_inf_class.inf_le2 sp_test sup_commute top_sp_test_down_iff_2 top_test_oi_top_complement)

lemma top_sp_test_down_iff_5:
  assumes "test p"
  shows "R  U * p  R  1  (U * p)"
  by (metis assms semilattice_inf_class.inf_le1 sup.absorb2 top_test_oi_top_complement)

lemma iu_test_sp_left_zero:
  assumes "q  1"
  shows "q * R = q"
  by (metis assms p_id_assoc2 p_subid_iff s_prod_p_idl)

lemma test_iu_test_split:
  "t  1  1  (p q . p  1  q  1  t = p  q)"
  by (meson subset_UnE sup.mono)

lemma test_iu_test_sp_assoc_1:
  "t  1  1  t * (R * S) = (t * R) * S"
  unfolding test_iu_test_split
  by (smt (verit, ccfv_threshold) inf.orderE p_id_assoc2 p_subid_iff s_prod_distr s_prod_p_idl test_assoc2)

lemma test_iu_test_sp_assoc_2:
  "t  1  R * (t * S) = (R * t) * S"
proof -
  assume 1: "t  1"
  have "R * (t * S) = R * (t * {})"
    using 1 by (metis iu_test_sp_left_zero p_id_assoc2 s_prod_p_idl)
  also have " = (R * t) * {}"
    by (metis cl5 s_prod_idl)
  also have "  (R * t) * S"
    by (simp add: s_prod_isor)
  finally have "R * (t * S)  (R * t) * S"
    .
  thus ?thesis
    by (simp add: s_prod_assoc1 set_eq_subset)
qed

lemma test_iu_test_sp_assoc_3:
  assumes "t  1  1"
  shows "R * (t * S) = (R * t) * S"
proof
  let ?g = "λb . if (b,{b})  t  (b,{})  t then {b} else {}"
  show "R * (t * S)  (R * t) * S"
  proof
    fix x
    assume "x  R * (t * S)"
    from this obtain a B C f where 1: "x = (a,C)  (a,B)  R  (bB . (b,f b)  t * S)  C = { f b | b . bB }"
      by (simp add: mr_simp) blast
    hence "bB . D . (b,D)  t  (g . (eD . (e,g e)  S)  f b = { g e | e . e  D })"
      by (simp add: mr_simp Setcompr_eq_image)
    hence "Db . bB . (b,Db b)  t  (g . (eDb b . (e,g e)  S)  f b = { g e | e . e  Db b })"
      by (rule bchoice)
    from this obtain Db where 2: "bB . (b,Db b)  t  (g . (eDb b . (e,g e)  S)  f b = { g e | e . e  Db b })"
      by auto
    let ?D = "{ Db b | b . b  B }"
    have "bB . (b,Db b)  t"
      using 2 by auto
    hence 3: "bB . Db b = {b}  Db b = {}"
      using assms by (metis Pair_inject Un_iff domain_pointwise inf.orderE p_subid_iff subid_aux2 test_iu_test_split)
    have 4: "(a,?D)  R * t"
      apply (simp add: mr_simp)
      apply (rule exI[where ?x="B"])
      apply (rule conjI)
      using 1 apply simp
      apply (rule exI[where ?x="Db"])
      using 2 by auto
    have 5: "b?D . (b,f b)  S"
    proof
      fix b
      assume "b  ?D"
      hence "b  B  Db b = {b}"
        using 3 by auto
      thus "(b,f b)  S"
        using 2 by force
    qed
    have 6: "C = { f b | b . b  ?D }"
    proof
      show "C  { f b | b . b  ?D }"
      proof
        fix y
        assume "y  C"
        from this 1 obtain b where 7: "b  B  y  f b"
          by auto
        hence "Db b = {b}"
          using 2 3 by blast
        thus "y  { f b | b . b  ?D }"
          using 7 by blast
      qed
    next
      show "{ f b | b . b  ?D }  C"
      proof
        fix y
        assume "y  { f b | b . b  ?D }"
        from this obtain b where 8: "b  ?D  y  f b"
          by auto
        hence "b  B"
          using 3 by auto
        thus "y  C"
          using 1 8 by auto
      qed
    qed
    have "(a,C)  (R * t) * S"
      using 4 5 6 apply (clarsimp simp: mr_simp) by blast
    thus "x  (R * t) * S"
      using 1 by simp
  qed
next
  show "(R * t) * S  R * (t * S)"
    using s_prod_assoc1 by blast
qed

lemma test_iu_test_sp_assoc_4:
  "t  1  R * (S * t) = (R * S) * t"
  by (metis cl5 iu_test_sp_left_zero)

lemma test_iu_test_sp_assoc_5:
  assumes "t  1  1"
  shows "R * (S * t) = (R * S) * t"
proof
  show "R * (S * t)  (R * S) * t"
  proof
    fix x
    assume "x  R * (S * t)"
    from this obtain a B C f where 1: "x = (a,C)  (a,B)  R  (bB . (b,f b)  S * t)  C = { f b | b . bB }"
      by (clarsimp simp: mr_simp) blast
    hence "bB . D . (b,D)  S  (g . (eD . (e,g e)  t)  f b = { g e | e . e  D })"
      by (clarsimp simp: mr_simp Setcompr_eq_image)
    hence "Db . bB . (b,Db b)  S  (g . (eDb b . (e,g e)  t)  f b = { g e | e . e  Db b })"
      by (rule bchoice)
    from this obtain Db where 2: "bB . (b,Db b)  S  (g . (eDb b . (e,g e)  t)  f b = { g e | e . e  Db b })"
      by auto
    hence "gb . bB . (eDb b . (e,gb b e)  t)  f b = { gb b e | e . e  Db b }"
      by (auto intro: bchoice)
    from this obtain gb where 3: "bB . (eDb b . (e,gb b e)  t)  f b = { gb b e | e . e  Db b }"
      by auto
    let ?g = "λx . { gb b x | b . b  B  x  Db b }"
    have 4: "bB . eDb b . gb b e = {}  gb b e = {e}"
    proof (intro ballI)
      fix b e
      assume "b  B" "e  Db b"
      hence "(e,gb b e)  t"
        using 3 by simp
      thus "gb b e = {}  gb b e = {e}"
        by (metis Un_iff assms domain_pointwise inf.orderE p_subid_iff prod.inject subid_aux2 test_iu_test_split)
    qed
    hence "e . ?g e  {e}"
      by auto
    hence 5: "e . ?g e = {}  ?g e = {e}"
      by auto
    let ?D = "{ Db b | b . b  B }"
    have 6: "(a,?D)  R * S"
      apply (unfold s_prod_def)
      using 1 2 by blast
    have 7: "b?D . (b,?g b)  t"
    proof
      fix e
      assume "e  ?D"
      from this obtain b where 8: "b  B  e  Db b"
        by auto
      show "(e,?g e)  t"
      proof (cases "?g e = {}")
        case True
        hence "gb b e = {}"
          using 8 by auto
        thus ?thesis
          using 3 8 True by metis
      next
        case False
        hence 9: "?g e = {e}"
          using 5 by auto
        from this obtain bb where 10: "bb  B  e  Db bb  e  gb bb e"
          by auto
        hence "gb bb e = {e}"
          using 4 by auto
        thus ?thesis
          using 3 9 10 by force
      qed
    qed
    have 11: "C = { ?g e | e . e  ?D }"
    proof
      show "C  { ?g e | e . e  ?D }"
      proof
        fix y
        assume "y  C"
        from this obtain b where 12: "b  B  y  f b"
          using 1 by auto
        from this 3 obtain e where "e  Db b  y  gb b e"
          by auto
        thus "y  { ?g e | e . e  ?D }"
          using 4 12 by auto
      qed
    next
      show "{ ?g e | e . e  ?D }  C"
      proof
        fix y
        assume "y  { ?g e | e . e  ?D }"
        from this obtain b e where 13: "b  B  e  Db b  y  gb b e"
          by auto
        hence "y  f b"
          using 3 by auto
        thus "y  C"
          using 1 13 by auto
      qed
    qed
    have "(a,C)  (R * S) * t"
      apply (simp add: mr_simp)
      apply (rule exI[where ?x="?D"])
      apply (rule conjI)
      using 6 apply (simp add: mr_simp)
      apply (rule exI[where ?x="?g"])
      using 7 11 by auto
    thus "x  (R * S) * t"
      using 1 by simp
  qed
next
  show "(R * S) * t  R * (S * t)"
    using s_prod_assoc1 by blast
qed

lemma inner_deterministic_sp_assoc:
  assumes "inner_univalent t"
  shows "t * (R * S) = (t * R) * S"
proof (rule antisym)
  show "t * (R * S)  (t * R) * S"
  proof
    fix x
    assume "x  t * (R * S)"
    from this obtain a B D f where 1: "x = (a,D)  (a,B)  t  (bB . (b,f b)  R * S)  D = { f b | b . bB }"
      by (simp add: mr_simp) blast
    have "(a,D)  (t * R) * S"
    proof (cases "(a,B)  1")
      case True
      hence "B = {}"
        by (metis Pair_inject domain_pointwise iu_test_sp_left_zero order_refl)
      hence "D = {}"
        using 1 by fastforce
      hence "(a,D)  t * (R * {})"
        using 1 (B::'b::type set) = {} s_prod_def by fastforce
      hence "(a,D)  (t * R) * {}"
        by (metis cl5 s_prod_idl)
      thus ?thesis
        using s_prod_isor by auto
    next
      case False
      hence "(a,B)  A"
        using 1 assms by blast
      from this obtain b where 2: "B = {b}"
        by (smt atoms_def Pair_inject mem_Collect_eq)
      hence "D = f b  (b,f b)  R * S"
        using 1 by auto
      from this obtain C g where 3: "(b,C)  R  (cC . (c,g c)  S)  D = { g c | c . cC }"
        by (clarsimp simp: mr_simp) blast
      have "(a,C)  t * R"
        apply (simp add: mr_simp)
        apply (rule exI[where ?x="B"])
        using 1 2 3 by auto
      thus ?thesis
        using 3 s_prod_def by blast
    qed
    thus "x  (t * R) * S"
      using 1 by auto
  qed
next
  show "(t * R) * S  t * (R * S)"
    using s_prod_assoc1 by blast
qed

lemma iu_unit_below_top_sp_test:
  "1  U * R"
  by (clarsimp simp: mr_simp) force

lemma ne_oi_complement_top_sp_test_1:
  "ne (R  -(U * S)) = R  -(U * S)"
  using iu_unit_below_top_sp_test by auto

lemma ne_oi_complement_top_sp_test_2:
  "ne R  -(U * S) = R  -(U * S)"
  using iu_unit_below_top_sp_test by auto

lemma schroeder_test:
  assumes "test p"
  shows "R * p  S  -S * p  -R"
  by (metis assms disjoint_eq_subset_Compl double_compl semilattice_inf_class.inf_commute sp_test_dist_oi_right)

lemma complement_test_sp_test:
  "test p  -p * p  -1"
  by (simp add: schroeder_test)

lemma test_sp_commute:
  "test p  test q  p * q = q * p"
  by (metis s_prod_idl sp_test_dist_oi_left sp_test_dist_oi_right test_fix)

lemma test_shunting:
  assumes "test p"
    and "test q"
    and "test r"
  shows "p * q  r  p  r   q"
proof
  assume 1: "p * q  r"
  have "p = p * q  p *  q"
    by (smt (verit, del_insts) Int_Un_distrib assms(1,2) inf_sup_aci(1) inf_sup_ord(2) le_iff_inf s_distl_test s_prod_idr sup_neg_inf)
  also have "...  r   q"
    using 1 by (metis assms(1) inf_le2 sup.mono test_sp)
  finally show "p  r   q"
    .
next
  assume "p  r   q"
  hence "p * q  p * r"
    by (smt (verit) assms boolean_algebra_class.boolean_algebra.double_compl inf.orderE inf_le1 le_inf_iff schroeder_test sup_neg_inf test_double_complement test_s_prod_is_meet test_sp_commute)
  also have "...  r"
    using assms(1) test_sp by auto
  finally show "p * q  r"
    .
qed

lemma test_sp_is_iu:
  "test p  test q  p * q = p ∪∪ q"
  by (metis Int_assoc inf.right_idem p_prod_comm s_prod_idr test_p_prod_is_meet test_sp)

lemma test_set:
  "test p  p = { (a,{a}) | a . (a,{a})  p }"
  using s_id_st by blast

lemma test_sp_is_ii:
  assumes "test p"
    and "test q"
  shows "p * q = p ∩∩ q"
proof -
  have "p  q = { (a,{a}) | a . (a,{a})  p }  { (a,{a}) | a . (a,{a})  q }"
    using assms test_set by blast
  also have "... = { (a,{a}) | a . (a,{a})  p } ∩∩ { (a,{a}) | a . (a,{a})  q }"
    apply (rule antisym)
     apply (clarsimp simp: mr_simp)
    apply (rule Int_greatest)
     apply (clarsimp simp: mr_simp)
    by (clarsimp simp: mr_simp)
  also have "... = p ∩∩ q"
    using test_set[symmetric, OF assms(1)] test_set[symmetric, OF assms(2)] by simp
  finally show "p * q = p ∩∩ q"
    by (metis assms inf.orderE test_oi_closed test_s_prod_is_meet)
qed

lemma test_galois_1:
  assumes "test p"
    and "test q"
  shows "p * q  r  q  p  r"
  by (metis (no_types, lifting) Int_Un_eq(2) assms inf.orderE sup_neg_inf test_double_complement test_s_prod_is_meet test_sp_commute)

lemma test_sp_shunting:
  assumes "test p"
  shows " p * R  {}  R  p * R"
  apply (rule iffI)
   apply (metis (no_types, opaque_lifting) assms complement_test_sp_top disjoint_eq_subset_Compl double_compl semilattice_inf_class.inf.absorb_iff2 semilattice_inf_class.inf_commute semilattice_inf_class.inf_right_idem test_sp)
  by (metis (no_types, opaque_lifting) assms complement_test_sp_top disjoint_eq_subset_Compl double_compl semilattice_inf_class.inf_commute semilattice_inf_class.inf_le1 subset_antisym test_sp)

lemma test_oU_closed:
  "pX . test p  test (X)"
  by blast

lemma test_oI_closed:
  "pX . test p  test (X)"
  by blast

lemma sp_test_dist_oI:
  assumes "test p"
    and "X  {}"
  shows "(X) * p = (RX . R * p)"
  apply (rule antisym)
   apply (clarsimp simp: mr_simp)
   apply blast
  apply (clarsimp simp: mr_simp)
  subgoal for a C proof -
    assume 1: "RX . B . (a,B)  R  (f . (bB . (b,f b)  p)  C = (f ` B))"
    have 2: "(RX . (a,C)  R  (bC . (b,{b})  p))"
    proof
      fix R
      assume "R  X"
      from this obtain B where 3: "(a,B)  R  (f . (bB . (b,f b)  p)  C = (f ` B))"
        using 1 by force
      from this obtain f where 4: "bB . (b,f b)  p" and 5: "C = (f ` B)"
        by auto
      hence 6: "bB . f b = {b}"
        using assms(1) test by blast
      hence 7: "C = B"
        using 5 by auto
      hence "(a,C)  R"
        using 3 by auto
      thus "(a,C)  R  (bC . (b,{b})  p)"
        using 4 6 7 by fastforce
    qed
    show ?thesis
      apply (rule exI[of _ C])
      apply (rule conjI)
      using 2 apply simp
      apply (rule exI[of _ "λx . {x}"])
      apply (rule conjI)
      using 2 assms(2) apply blast
      by simp
  qed
  done

lemma test_iU_is_iI:
  assumes "iI . test (X i)"
    and "I  {}"
  shows "⋃⋃X|I = ⋂⋂X|I"
  apply (rule antisym)
   apply (clarsimp simp: mr_simp)
  subgoal for a f proof -
    assume 1: "iI . (a,f i)  X i"
    hence "iI . f i = {a}"
      using assms(1) by (meson test)
    hence "(f ` I) = (f ` I)  (iI . (a,f i)  X i)"
      using 1 assms(2) by auto
    thus ?thesis
      by meson
  qed
  apply (clarsimp simp: mr_simp)
  by (metis (no_types, opaque_lifting) INF_eq_const SUP_eq_const assms test)

lemma test_iU_is_oI:
  assumes "iI . test (X i)"
    and "I  {}"
  shows "⋃⋃X|I = (X ` I)"
  apply (rule antisym)
   apply (clarsimp simp: mr_simp)
   apply (metis (no_types, opaque_lifting) SUP_eq_const assms test)
  apply (clarsimp simp: mr_simp)
  by (metis UN_constant assms(2))

subsection ‹Domain and antidomain›

declare Dom_def [mr_simp]

abbreviation aDom :: "('a,'b) mrel  ('a,'a) mrel" where
  "aDom R   Dom R"

lemma ad_set: "aDom R = {(a,{a})| a. ¬(A. (a,A)  R)}"
  by (clarsimp simp: mr_simp) force

lemma d_test:
  "test (Dom R)"
  unfolding Dom_def using s_id_def by fastforce

lemma ad_test:
  "test (aDom R)"
  by simp

lemma ad_expl:
  "aDom R = -((R * 1) ∪∪ 1)  1"
  by (simp add: d_def_expl)

lemma ad_expl_2:
  "aDom (R::('a,'b) mrel) = -((R * (1::('b,'a) mrel)))  (1::('a,'a) mrel)"
proof
  have "-((R * 1))  1 = -((R * 1) ∪∪ U)  1"
    by simp
  also have "  -((R * 1) ∪∪ 1)  1"
    by (metis c6 convex_increasing iu_commute iu_isotone iu_unit sp_unit_convex test_complement_antitone upper_iu_increasing)
  also have " = aDom R"
    by (simp add: d_def_expl)
  finally show "-((R * 1))  1  aDom R"
    using  ((R::('a::type × 'b::type set) set) * 1)   (R * 1 ∪∪ 1) by blast
  have "aDom R = {(a,{a}) |a. ¬(B. (a,B)  R)}"
    by (simp add: ad_set)
  also have "  {(a,{a}) |a. (a,{a})  (R * (p_id::('b,'a) mrel))}"
    by (simp add: U_par_st domain_pointwise)
  also have " = {(a,{a}) |a. (a,{a})  -(R * (p_id::('b,'a) mrel))  1}"
    using test_complement by fastforce
  finally show "aDom R  -((R * (1::('b,'a) mrel)))  (1::('a,'a) mrel)"
    by blast
qed

lemma aDom:
  "aDom R = { (a,{a}) | a . ¬(B . (a,B)  R) }"
  by (simp add: ad_set)

declare aDom [mr_simp]

lemma d_down_oi_up_1:
  "Dom (R  S) = Dom (R  S)"
  by (metis Int_commute d_def_expl domain_up_down_conjugate)

lemma d_down_oi_up_2:
  "Dom (R  S) = Dom (R  S)"
  by (simp add: d_down_oi_up_1)

lemma d_ne_down_dp_complement_test:
  assumes "test p"
  shows "Dom (R  -(U * p)) = Dom (ne (R) *  p)"
  by (simp add: assms d_down_oi_up_1 oc_top_sp_test_0 oc_top_sp_test_1 sp_test_dist_oi_right)

lemma d_strict:
  "R = {}  Dom R = {}"
  using Dom_def by fastforce

lemma d_sp_strict:
  "R * S = {}  R * Dom S = {}"
  apply (clarsimp simp: mr_simp)
  apply safe
   apply metis
  by (metis UN_singleton)

lemma d_complement_ad:
  "Dom R =  aDom R"
  using d_test by blast

lemma down_sp_below_iu_unit:
  "R * S  1  R  U * aDom (ne S)"
proof -
  have "R * S  1  ne (R * S) = {}"
    by (simp add: disjoint_eq_subset_Compl)
  also have "...  ne (R) * ne S = {}"
    by (simp add: ne_dist_down_sp)
  also have "...  ne (R) * Dom (ne S) = {}"
    using d_sp_strict by auto
  also have "...  ne (R) *  aDom (ne S) = {}"
    by (metis d_complement_ad)
  also have "...  R  U * aDom (ne S)"
    by (metis top_sp_test_down_iff_1 top_sp_test_down_iff_2 top_sp_test_down_iff_3 ad_test subset_empty)
  finally show ?thesis
    .
qed

lemma ad_sp_bot:
  "aDom R * R = {}"
  by (simp add: d_s_id_ax d_sp_strict inf_sup_aci(1) sp_test_dist_oi_left)

lemma sp_top_d:
  "R * U  Dom R * U"
  by (simp add: cl8_var iu_unit_up sp_upper_left_isotone)

lemma d_sp_top:
  "Dom (R * U) = Dom R"
  by (clarsimp simp: mr_simp) blast

lemma d_down:
  "Dom (R) = Dom R"
  by (metis U_par_idem d_down_oi_up_1 inf.orderE top_down top_lower_greatest)

lemma d_up:
  "Dom (R) = Dom R"
  by (metis Int_absorb1 U_par_idem d_down_oi_up_1 top_down top_upper_least)

lemma d_isotone:
  "R  S  Dom R  Dom S"
  unfolding Dom_def by blast

lemma ad_antitone:
  "R  S  aDom S  aDom R"
  by (simp add: Int_commute d_isotone semilattice_inf_class.le_infI2)

lemma d_dist_ou:
  "Dom (R  S) = Dom R  Dom S"
  unfolding Dom_def by blast

lemma d_dist_iu:
  "Dom (R ∪∪ S) = Dom R * Dom S"
  by (clarsimp simp: mr_simp) auto

lemma d_dist_ii:
  "Dom (R ∩∩ S) = Dom R * Dom S"
  by (metis antisym_conv d_U d_dist_iu d_down d_isotone ii_convex_iu s_prod_idr)

lemma d_loc:
  "Dom (R * Dom S) = Dom (R * S)"
  apply (clarsimp simp: mr_simp)
  apply safe
   apply metis
  by (metis UN_singleton)

lemma ad_loc:
  "aDom (R * Dom S) = aDom (R * S)"
  by simp

lemma d_ne_down:
  "Dom (ne (R)) = Dom (ne R)"
  by (metis atoms_solution d_down_oi_up_1 d_down_oi_up_2)

lemma ne_sp_iu_unit_up:
  "ne R = R  (R * 1) = R * U"
  apply (clarsimp simp: mr_simp)
  apply safe
   apply (metis (no_types, lifting) Compl_iff IntE Inter_iff UNIV_I UN_simps(2) image_eqI singletonI)
  apply clarsimp
  by (metis SUP_bot sup_bot_left)

lemma ne_d_expl:
  "ne R = R  Dom R = R * U  1"
  by (metis cl8_var d_def_expl d_test ne_sp_iu_unit_up test_sp)

lemma ne_a_expl:
  "ne R = R  aDom R = -(R * U)  1"
  by (simp add: ad_expl_2 ne_sp_iu_unit_up)

lemma d_dist_oU:
  "Dom (X) = (Dom ` X)"
  apply (clarsimp simp: mr_simp)
  by blast

lemma d_dist_iU_iI:
  "Dom (⋃⋃X|I) = Dom (⋂⋂X|I)"
  by (clarsimp simp: mr_simp)

lemma d_dist_iU_oI:
  assumes "I  {}"
  shows "Dom (⋃⋃X|I) = (Dom ` X ` I)"
  apply (rule antisym)
   apply (clarsimp simp: mr_simp)
   apply blast
  apply (clarsimp simp: mr_simp)
  by (meson all_not_in_conv assms)

subsection ‹Left residual›

definition sp_lres :: "('a,'c) mrel  ('b,'c) mrel  ('a,'b) mrel" (infixl "" 65) where
  "Q  R  { (a,B) . f . (b  B . (b,f b)  R)  (a,{ f b | b . b  B })  Q }"

declare sp_lres_def [mr_simp]

lemma sp_lres_galois:
  "S * R  Q  S  Q  R"
proof
  assume 1: "S * R  Q"
  show "S  Q  R"
  proof
    fix x
    assume "x  S"
    from this obtain a B where 2: "x = (a,B)  (a,B)  S"
      by (metis surj_pair)
    have "f . (b  B . (b,f b)  R)  (a,{ f b | b . b  B })  Q"
    proof (rule allI, rule impI)
      fix f
      assume "b  B . (b,f b)  R"
      hence "(a,{ f b | b . b  B })  S * R"
        apply (unfold s_prod_def)
        using 2 by auto
      thus "(a,{ f b | b . b  B })  Q"
        using 1 by auto
    qed
    thus "x  Q  R"
      using 2 sp_lres_def by auto
  qed
next
  assume 3: "S  Q  R"
  have "(Q  R) * R  Q"
  proof
    fix x
    assume "x  (Q  R) * R"
    from this obtain a D where 4: "x = (a,D)  (a,D)  (Q  R) * R"
      by (metis surj_pair)
    from this obtain C where "(a,C)  Q  R  (g . (cC . (c,g c)  R)  D = { g c | c . c  C })"
      by (simp add: mr_simp) blast
    thus "x  Q"
      apply (unfold sp_lres_def)
      using 4 by auto
  qed
  thus "S * R  Q"
    using 3 by (meson dual_order.trans s_prod_isol)
qed

lemma sp_lres_expl:
  "Q  R = { S . S * R  Q }"
  using sp_lres_galois by blast

lemma bot_sp_lres_d:
  "{}  R = {}  Dom R"
  by (metis d_sp_strict order_refl sp_lres_galois subset_antisym subset_empty)

lemma bot_sp_lres_expl:
  "{}  R = -(U * Dom R)"
  apply (rule antisym)
   apply (metis d_sp_strict d_test disjoint_eq_subset_Compl order_refl sp_lres_galois sp_test subset_empty)
  by (metis Compl_disjoint2 bot_sp_lres_d d_test sp_lres_galois sp_test subset_empty)

lemma sp_lres_sp_below:
  "(Q  R) * R  Q"
  by (simp add: sp_lres_galois)

lemma sp_lres_left_isotone:
  "Q  S  Q  R  S  R"
  by (meson dual_order.refl sp_lres_galois subset_trans)

lemma sp_lres_right_antitone:
  "S  R  Q  R  Q  S"
  by (meson dual_order.trans s_prod_isor sp_lres_galois sp_lres_sp_below)

lemma sp_lres_down_closed_1:
  "Q  R = Q  R"
proof
  show "Q  R  Q  R"
    by (metis down_dist_sp down_idempotent down_isotone sp_lres_galois sp_lres_sp_below)
next
  show "Q  R  Q  R"
    by (simp add: lower_reflexive sp_lres_right_antitone)
qed

lemma sp_lres_down_closed_2:
  assumes "R = R"
    and "total T"
  shows "(R  T) = R  T"
proof -
  have "(R  T)  R  T"
    by (metis assms lower_transitive sp_lres_galois sp_lres_sp_below total_down_sp_semi_commute)
  thus ?thesis
    by (simp add: lower_reflexive subset_antisym)
qed

lemma down_sp_sp:
  "R * S = R * (1  S)"
proof -
  have "R * S = R * (1  1) * S"
    by (simp add: down_sp)
  also have "... = R * ((1  1) * S)"
    by (simp add: test_iu_test_sp_assoc_3)
  also have "... = R * (1  S)"
    apply (clarsimp simp: mr_simp)
    apply safe
     apply (smt (z3) Sup_empty ccpo_Sup_singleton image_empty image_insert singletonI)
    by (smt (verit, del_insts) Sup_empty all_not_in_conv ccpo_Sup_singleton image_insert image_is_empty singletonD)
  finally show ?thesis
    .
qed

lemma iu_unit_sp_lres_iu_unit_ou:
  "U * aDom (ne R) = 1  (1  R)"
  apply (rule antisym)
   apply (metis down_sp_sp sp_lres_galois down_sp_below_iu_unit order_refl)
  by (metis down_sp_sp sp_lres_galois down_sp_below_iu_unit order_refl)

lemma bot_sl_below_complement_d:
  "{}  R  - Dom R"
  by (metis Compl_anti_mono bot_sp_lres_expl d_test dual_order.refl inf.order_iff sp_test test_s_prod_is_meet)

lemma sp_unit_oi_bot_sp_lres:
  "1  - Dom R = 1  ({}  R)"
  by (smt (verit, ccfv_SIG) ad_sp_bot boolean_algebra_cancel.inf1 bot_sl_below_complement_d inf.orderE inf_bot_right inf_commute inf_le2 sp_lres_galois)

lemma ad_explicit_d:
  "aDom R = -(U * Dom R)  1"
  by (simp add: bot_sp_lres_expl lattice_class.inf_sup_aci(1) sp_unit_oi_bot_sp_lres)

lemma top_test_sp_lres_total_expl_1:
  assumes "test p"
  shows "S . S  (U * p)  R  S  U * aDom (R  -(U * p))"
proof
  fix S::"('b,'c) mrel"
  have "S  U * aDom (R  -(U * p))  ne (S) * Dom (R  -(U * p)) = {}"
    by (metis (no_types, lifting) d_complement_ad inf_le2 subset_empty top_sp_test_down_iff_1 top_sp_test_down_iff_2 top_sp_test_down_iff_3)
  also have "...  ne (S) * Dom (ne (R) *  p) = {}"
    by (simp add: assms d_ne_down_dp_complement_test)
  also have "...  ne (S) * (ne (R) *  p) = {}"
    using d_sp_strict by auto
  also have "...  ne (S) * ne (R) *  p = {}"
    by (simp add: test_assoc3)
  also have "...  ne ((S * R)) *  p = {}"
    by (simp add: down_dist_sp ne_dist_down_sp)
  also have "...  S * R  U * p"
    by (metis assms top_sp_test_down_iff_1 top_sp_test_down_iff_2 top_sp_test_down_iff_3 subset_empty)
  also have "...  S  (U * p)  R"
    by (simp add: sp_lres_galois)
  finally show "S  (U * p)  R  S  U * aDom (R  -(U * p))"
    by simp
qed

lemma top_test_sp_lres_total_expl_2:
  assumes "test p"
    and "total T"
  shows "(U * p)  T = U * aDom (T  -(U * p))"
proof -
  have "S . S  (U * p)  T  S  U * aDom (T  -(U * p))"
    by (smt assms lower_reflexive sp_lres_down_closed_2 subset_trans top_sp_test_down_closed top_test_sp_lres_total_expl_1)
  thus ?thesis
    by blast
qed

lemma top_test_sp_lres_total_expl_3:
  assumes "test p"
  shows "((U * p)  R)  1 = aDom (R  -(U * p))"
proof
  have "(((U * p)  R)  1) * R = (((U * p)  R)  1) * (1  R)"
    using down_sp_sp by blast
  also have "... = (((U * p)  R)  1) * 1  (((U * p)  R)  1) * R"
    by (simp add: s_distl_test)
  also have "...  1  (((U * p)  R)  1) * R"
    using c6 by auto
  also have "...  1  ((U * p)  R) * R"
    by (metis Un_Int_eq(4) inf_le2 iu_unit_convex iu_unit_down sp_oi_subdist sup.mono)
  also have "...  1  U * p"
    using sp_lres_sp_below by auto
  also have "... = U * p"
    by (simp add: iu_unit_below_top_sp_test sup.absorb2)
  finally have "(((U * p)  R)  1)  (U * p)  R"
    by (simp add: sp_lres_galois)
  hence "((U * p)  R)  1  U * aDom (R  -(U * p))"
    by (metis assms top_test_sp_lres_total_expl_1)
  thus "((U * p)  R)  1  aDom (R  -(U * p))"
    by (metis (no_types, lifting) inf.idem inf.orderE inf_commute sp_oi_subdist sp_test test_s_prod_is_meet)
next
  have "aDom (R  -(U * p)) = U * aDom (R  -(U * p))  1"
    by (metis (no_types, lifting) inf.absorb_iff2 inf.idem inf_commute inf_le2 sp_test test_s_prod_is_meet)
  thus "aDom (R  -(U * p))  ((U * p)  R)  1"
    by (metis Int_mono ad_test assms order_refl top_sp_test_down_closed top_test_sp_lres_total_expl_1)
qed

lemma top_test_sp_lres_total_expl_4:
  assumes "test p"
  shows "aDom (ne (R) *  p) = ((U * p)  R)  1"
  by (simp add: assms d_ne_down_dp_complement_test top_test_sp_lres_total_expl_3)

lemma oi_complement_top_sp_test_top_1:
  assumes "test p"
  shows "(R  -(U * p)) * U = (R  -(U * p)) * U"
proof (rule antisym)
  show "(R  -(U * p)) * U  (R  -(U * p)) * U"
    by (metis (no_types, lifting) assms cl8_var d_down_oi_up_1 equalityD2 ne_oi_complement_top_sp_test_1 ne_sp_iu_unit_up oc_top_sp_test_up_closed)
next
  have "R  -(U * p)  (R  -(U * p))"
    by (metis oc_top_sp_test_up_closed down_oi_up_closed assms)
  also have "...  (R  -(U * p)) * U"
    by (simp add: down_below_sp_top)
  finally show "(R  -(U * p)) * U  (R  -(U * p)) * U"
    by (metis assms domain_up_down_conjugate inf_commute ne_oi_complement_top_sp_test_1 ne_sp_iu_unit_up oc_top_sp_test_up_closed set_eq_subset)
qed

lemma oi_complement_top_sp_test_top_2:
  assumes "test p"
  shows "(R  -(U * p)) * U = ne (R) *  p * U"
proof (rule antisym)
  have "R  -(U * p) * U  Dom (R  -(U * p)) * U"
    using sp_top_d by blast
  also have "... = Dom (ne (R) *  p) * U"
    by (simp add: assms d_ne_down_dp_complement_test)
  also have "... = Dom (ne (R *  p)) * U"
    by (simp add: ne_sp_test)
  also have "... = ne (R *  p) * U"
    by (simp add: cl8_var ne_sp_iu_unit_up)
  also have "... = ne (R) *  p * U"
    by (simp add: ne_sp_test)
  finally show "(R  -(U * p)) * U  ne (R) *  p * U"
    .
next
  have "ne (R) *  p  -(U * p)"
    by (metis assms disjoint_eq_subset_Compl double_complement inf_compl_bot_right schroeder_test sp_test test_complement_closed top_test_oi_top_complement)
  thus "ne (R) *  p * U  (R  -(U * p)) * U"
    by (metis (no_types) assms cl8_var d_down_oi_up_1 d_ne_down_dp_complement_test ne_oi_complement_top_sp_test_1 ne_sp_iu_unit_up oc_top_sp_test_up_closed sp_top_d)
qed

lemma oi_complement_top_sp_test_top_3:
  assumes "test p"
  shows "(R  -(U * p)) * U = ne (R) * -(p * U)"
  by (simp add: assms complement_test_sp_top oi_complement_top_sp_test_top_2 test_assoc1)

lemma split_sp_test_2:
  "test p  R  R * p  ne (R) * ( p)"
proof -
  assume "test p"
  hence "R  R * p  (ne (R *  p))"
    by (smt (verit, best) IntE UnCI UnE split_sp_test subsetI)
  thus "R  R * p  ne (R) * ( p)"
    by (simp add: ne_sp_test_up)
qed

lemma split_sp_test_3:
  "test p  R  R * p  R * ( p)"
  by (smt IntE UnCI UnE ne_dist_down_sp ne_sp_test_up ne_test_up split_sp_test subsetI)

lemma split_sp_test_4:
  assumes "test p"
    and "test q"
  shows "R * (p  q)  R * p  ne (R) * q"
proof -
  have 1: "(p  q) * p = p"
    by (metis Un_Int_eq(1) assms sp_test_dist_oi_left test_ou_closed test_sp_commute test_sp_idempotent)
  have "(R * (p  q)) *  p  R * q"
  proof -
    have "(R * (p  q)) *  p = R * (p  q) * (1   p)"
      using down_sp_sp by blast
    also have "... = R * ((p  q) * 1  (p  q) *  p)"
      by (smt (verit) assms inf.orderE s_distl_test test_assoc1 test_ou_closed)
    also have "...  R * (1  (p  q) *  p)"
      by (meson c6 s_prod_isor subset_refl sup.mono)
    also have "... = R * ((p  q) *  p)"
      using down_sp_sp by blast
    also have "... = R * (p *  p  q *  p)"
      by (metis assms ii_right_dist_ou inf_commute inf_le1 test_ou_closed test_sp_is_ii)
    also have "... = R * (q *  p)"
      by (metis Compl_disjoint assms(1) inf_commute inf_le1 s_prod_idl sp_test_dist_oi_left subset_Un_eq test_sp_commute)
    also have "...  R * q"
      by (metis inf_le1 inf_le2 s_prod_isor sp_test)
    finally show ?thesis
      .
  qed
  hence 2: "ne ((R * (p  q))) *  p  ne (R) * q"
    by (metis assms(2) inf_le2 ne_dist_ou ne_sp_test subset_Un_eq)
  have "R * (p  q)  R * (p  q) * p  ne ((R * (p  q))) * ( p)"
    by (simp add: assms split_sp_test_2)
  also have "... = R * p  ne ((R * (p  q))) * ( p)"
    using 1 by (metis assms(1) inf.orderE test_assoc3)
  also have "...  R * p  ne (R) * q"
    using 2 by (metis (no_types, lifting) Un_Int_eq(1) assms(2) inf_le2 iu_isotone ne_sp_test ne_sp_test_up sup.mono)
  finally show ?thesis
    .
qed

lemma split_sp_test_5:
  assumes "test p"
    and "test q"
  shows "R * (p  q)  R * p  R * q"
proof -
  have "R * (p  q)  R * p  ne (R) * q"
    by (simp add: assms split_sp_test_4)
  thus ?thesis
    by (metis (no_types, lifting) assms(2) le_inf_iff ne_dist_down_sp ne_test_up sup_neg_inf)
qed

lemma split_sp_test_6:
  assumes "test p"
    and "test q"
  shows "Dom (R * (p  q))  Dom (R * p  ne (R) * q)"
proof -
  have "Dom (R * (p  q))  Dom (R * p  ne (R) * q)"
    by (simp add: assms d_isotone split_sp_test_4)
  also have "... = Dom (R * p  (ne (R) * q))"
    by (simp add: assms(2) ne_sp_test ne_sp_test_up)
  also have "...  Dom (R * p  ne (R) * q)"
    by (metis d_up subsetI up_dist_ou up_idempotent)
  finally show ?thesis
    .
qed

lemma split_sp_test_7:
  assumes "test p"
    and "test q"
  shows "Dom (ne (R) * (p  q)) = Dom (ne (R) * p  ne (R) * q)"
  apply (rule antisym)
   apply (metis assms ne_down_idempotent split_sp_test_6)
  by (smt (verit, ccfv_SIG) Un_Int_eq(1) Un_subset_iff assms(2) d_isotone inf.orderE inf_le1 le_inf_iff lower_eq_down ne_dist_ou sp_oi_subdist_2 subset_Un_eq sup.mono)

lemma test_sp_left_dist_iu_1:
  "test p  p * (R ∪∪ S) = p * R ∪∪ S"
  by (metis cl8_var inf.orderE p_prod_assoc s_subid_iff2)

lemma test_sp_left_dist_iu_2:
  "test p  p * (R ∪∪ S) = R ∪∪ p * S"
  by (metis iu_commute test_sp_left_dist_iu_1)

lemma d_sp_below_iu_down:
  "Dom R * S  (R ∪∪ S)"
  by (simp add: cl8_var iu_lower_left_isotone sp_iu_unit_lower)

lemma d_sp_ne_down_below_ne_iu_down:
  "Dom R * ne (S)  ne ((R ∪∪ S))"
proof -
  have "Dom R * S  (R ∪∪ S)"
    by (simp add: cl8_var iu_lower_isotone sp_iu_unit_lower)
  hence "ne (Dom R * S)  ne ((R ∪∪ S))"
    by blast
  thus ?thesis
    by (smt d_test test_sp_ne)
qed

lemma top_test:
  "test p  U * p = { (a,B) . (bB . (b,{b})  p) }"
  apply (unfold test)
  apply (clarsimp simp: mr_simp)
  by fastforce

lemma iu_oi_complement_top_test_ou_up:
  "test p  (R ∪∪ S)  -(U * p)  ((R  S)  -(U * p))"
  apply (unfold top_test)
  apply (clarsimp simp: mr_simp)
  by blast

lemma d_ne_iu_down_sp_test_ou:
  assumes "test p"
  shows "Dom (ne ((R ∪∪ S)) * p)  Dom ((ne (R)  ne (S)) * p)"
proof -
  have "Dom (ne ((R ∪∪ S)) * p) = Dom ((R ∪∪ S)  -(U *  p))"
    by (metis assms d_ne_down_dp_complement_test test_double_complement)
  also have "...  Dom ((R  S)  -(U *  p))"
    by (metis iu_oi_complement_top_test_ou_up d_isotone d_up semilattice_inf_class.inf_le2)
  also have "... = Dom (ne ((R  S)) * p)"
    by (metis assms d_ne_down_dp_complement_test test_double_complement)
  finally show ?thesis
    by (simp add: down_dist_ou ne_dist_ou)
qed

lemma test_sp_left_dist_iU:
  assumes "test p"
    and "I  {}"
  shows "p * (⋃⋃X|I) = ⋃⋃(λi . p * X i)|I"
  apply (rule antisym)
   apply (clarsimp simp: mr_simp)
  subgoal for a B f proof -
    assume 1: "(a,B)  p"
    hence 2: "B = {a}"
      by (metis assms(1) test)
    assume "bB . g . f b = (g ` I)  (iI . (b,g i)  X i)"
    from this obtain g where 3: "f a = (g ` I)  (iI . (a,g i)  X i)"
      using 2 by auto
    have "(f ` B) = (g ` I)  (iI . B . (a,B)  p  (f . (bB . (b,f b)  X i)  g i = (f ` B)))"
      apply (rule conjI)
      using 2 3 apply blast
      apply (rule ballI)
      apply (rule exI[of _ B])
      apply (rule conjI)
      using 1 apply simp
      subgoal for i
        apply (rule exI[of _ "λb . g i"])
        using 2 3 by blast
      done
    thus ?thesis
      by auto
  qed
  apply (clarsimp simp: mr_simp)
  subgoal for a f proof -
    assume 4: "iI . B . (a,B)  p  (g . (bB . (b,g b)  X i)  f i = (g ` B))"
    have "(a,{a})  p  (g . (b{a} . f . g b = (f ` I)  (iI . (b,f i)  X i))  (f ` I) = (g ` {a}))"
      apply (rule conjI)
      using 4 apply (metis assms equals0I test)
      apply (rule exI[of _ "λa . (f ` I)"])
      apply clarsimp
      apply (rule exI[of _ f])
      using 4 assms(1) test by fastforce
    thus ?thesis
      by auto
  qed
  done

subsection ‹Modal operations›

definition adia :: "('a,'b) mrel  ('b,'b) mrel  ('a,'a) mrel" ("| _  _" [50,90] 95) where
  "|Rp  { (a,{a}) | a . B . (a,B)  R  (bB . (b,{b})  p) }"

definition abox :: "('a,'b) mrel  ('b,'b) mrel  ('a,'a) mrel" ("| _ ] _" [50,90] 95) where
  "|R]p  { (a,{a}) | a . B . (a,B)  R  (bB . (b,{b})  p) }"

definition edia :: "('a,'b) mrel  ('b,'b) mrel  ('a,'a) mrel" ("| _ ⟩⟩ _" [50,90] 95) where
  "|R⟩⟩p  { (a,{a}) | a . B . (a,B)  R  (bB . (b,{b})  p) }"

definition ebox :: "('a,'b) mrel  ('b,'b) mrel  ('a,'a) mrel" ("| _ ]] _" [50,90] 95) where
  "|R]]p  { (a,{a}) | a . B . (a,B)  R  (bB . (b,{b})  p) }"

declare adia_def [mr_simp] abox_def [mr_simp] edia_def [mr_simp] ebox_def [mr_simp]

lemma adia:
  assumes "test p"
  shows "|Rp = Dom (R * p)"
proof
  show "|Rp  Dom (R * p)"
  proof
    fix x
    assume "x  |Rp"
    from this obtain a B where 1: "x = (a,{a})  (a,B)  R  (bB . (b,{b})  p)"
      by (smt adia_def surj_pair mem_Collect_eq)
    have "(a,B)  R * p"
      apply (clarsimp simp: s_prod_def)
      apply (rule exI[where ?x="B"])
      apply (rule conjI)
      using 1 apply simp
      apply (rule exI[where ?x="λx . {x}"])
      using 1 by auto
    thus "x  Dom (R * p)"
      using 1 Dom_def by auto
  qed
next
  show "Dom (R * p)  |Rp"
  proof
    fix x
    assume "x  Dom (R * p)"
    from this obtain a A where 2: "x = (a,{a})  (a,A)  R * p"
      by (smt Dom_def surj_pair mem_Collect_eq)
    from this obtain B f where 3: "(a,B)  R  (bB . (b,f b)  p)  A = { f b | b . b  B }"
      by (simp add: mr_simp) blast
    hence "bB . (b,{b})  p"
      using assms subid_aux2 by fastforce
    thus "x  |Rp"
      using 2 3 adia_def by blast
  qed
qed

lemma abox_1:
  assumes "test p"
  shows "|R]p = aDom (R  -(U * p))"
proof
  show "|R]p  aDom (R  -(U * p))"
  proof
    fix x
    assume "x  |R]p"
    from this obtain a where 1: "x = (a,{a})  (B . (a,B)  R  (bB . (b,{b})  p))"
      by (smt abox_def surj_pair mem_Collect_eq)
    have "¬(B . (a,B)  R  -(U * p))"
    proof
      assume "B . (a,B)  R  -(U * p)"
      from this obtain B where "(a,B)  R  (a,B)  U * p"
        by auto
      thus False
        using 1 by (metis (no_types, lifting) assms top_sp_test)
    qed
    thus "x  aDom (R  -(U * p))"
      using 1 aDom by blast
  qed
next
  show "aDom (R  -(U * p))  |R]p"
  proof
    fix x
    assume "x  aDom (R  -(U * p))"
    from this obtain a where 2: "x = (a,{a})  ¬(B . (a,B)  R  -(U * p))"
      by (smt aDom surj_pair mem_Collect_eq)
    hence "B . (a,B)  R  (bB . (b,{b})  p)"
      using assms by (metis (no_types, lifting) IntI oc_top_sp_test)
    thus "x  |R]p"
      using 2 abox_def by blast
  qed
qed

lemma abox:
  assumes "test p"
  shows "|R]p = aDom (ne (R) *  p)"
  by (simp add: abox_1 assms d_ne_down_dp_complement_test)

lemma edia_1:
  assumes "test p"
  shows "|R⟩⟩p = Dom (R  -(U *  p))"
proof
  show "|R⟩⟩p  Dom (R  -(U *  p))"
  proof
    fix x
    assume "x  |R⟩⟩p"
    from this obtain a b B where 1: "x = (a,{a})  (a,B)  R  b  B  (b,{b})  p"
      by (smt edia_def surj_pair mem_Collect_eq)
    hence "(a,B)  -(U *  p)"
      by (metis (no_types, lifting) lattice_class.inf_sup_ord(2) oc_top_sp_test test_complement)
    thus "x  Dom (R  -(U *  p))"
      using 1 Dom_def by auto
  qed
next
  show "Dom (R  -(U *  p))  |R⟩⟩p"
  proof
    fix x
    assume "x  Dom (R  -(U *  p))"
    from this obtain a B where 2: "x = (a,{a})  (a,B)  R  (a,B)  -(U *  p)"
      by (smt Dom_def surj_pair mem_Collect_eq IntE)
    hence "bB . (b,{b})  p"
      by (meson oc_top_sp_test test_complement test_complement_closed)
    thus "x  |R⟩⟩p"
      using 2 edia_def by blast
  qed
qed

lemma edia:
  assumes "test p"
  shows "|R⟩⟩p = Dom (ne (R) * p)"
  by (metis assms d_ne_down_dp_complement_test edia_1 test_double_complement)

lemma ebox:
  assumes "test p"
  shows "|R]]p = aDom (R *  p)"
proof
  show "|R]]p  aDom (R *  p)"
  proof
    fix x
    assume "x  |R]]p"
    from this obtain a where 1: "x = (a,{a})  (B . (a,B)  R  (bB . (b,{b})  p))"
      by (smt ebox_def surj_pair mem_Collect_eq)
    hence "¬(B . (a,B)  R *  p)"
      by (metis (no_types, lifting) s_prod_test test_complement)
    thus "x  aDom (R *  p)"
      using 1 aDom by blast
  qed
next
  show "aDom (R *  p)  |R]]p"
  proof
    fix x
    assume "x  aDom (R *  p)"
    from this obtain a where 2: "x = (a,{a})  ¬(B . (a,B)  R *  p)"
      by (smt aDom surj_pair mem_Collect_eq)
    have "B . (a,B)  R  (bB . (b,{b})  p)"
    proof (rule allI, rule impI)
      fix B
      assume "(a,B)  R"
      hence "(a,B)  U *  p"
        using 2 by (metis Int_iff Int_lower2 sp_test)
      thus "bB . (b,{b})  p"
        by (meson test_complement test_complement_closed top_sp_test)
    qed
    thus "x  |R]]p"
      using 2 ebox_def by blast
  qed
qed

lemma abox_2:
  assumes "test p"
  shows "|R]p = -((R  -(U * p)) * U)  1"
  by (simp add: abox_1 assms ne_a_expl ne_oi_complement_top_sp_test_1)

lemma abox_3:
  assumes "test p"
  shows "|R]p = -(ne (R) *  p * U)  1"
  by (simp add: abox assms ne_a_expl ne_sp_test)

lemma abox_4:
  assumes "test p"
  shows "|R]p = ((U * p)  R)  1"
  by (simp add: abox_1 assms top_test_sp_lres_total_expl_3)

lemma abox_ebox:
  assumes "test p"
  shows "|R]p = |ne (R)]]p"
  by (simp add: abox assms ebox)

lemma abox_edia:
  assumes "test p"
  shows "|R]p =  |R⟩⟩( p)"
  by (simp add: abox assms edia)

lemma abox_adia:
  assumes "test p"
  shows "|R]p =  |ne (R)( p)"
  by (simp add: abox adia assms)

lemma edia_adia:
  assumes "test p"
  shows "|R⟩⟩p = |ne (R)p"
  by (simp add: adia assms edia)

lemma edia_abox:
  assumes "test p"
  shows "|R⟩⟩p =  |R]( p)"
  by (metis abox_1 assms d_complement_ad edia_1 semilattice_inf_class.inf.cobounded2)

lemma edia_ebox:
  assumes "test p"
  shows "|R⟩⟩p =  |ne (R)]]( p)"
  by (simp add: abox assms ebox edia_abox)

lemma abox_ne_down:
  assumes "test p"
  shows "|R]p = |ne (R)]p"
  by (simp add: abox assms ne_down_idempotent)

lemma edia_ne_down:
  assumes "test p"
  shows "|R⟩⟩p = |ne (R)⟩⟩p"
  by (simp add: assms edia ne_down_idempotent)

lemma adia_up:
  assumes "test p"
  shows "|Rp = |Rp"
proof -
  have "|Rp = Dom (R  U * p)"
    by (metis adia assms iu_assoc iu_unit_up up_dist_iu_oi)
  also have "... = Dom (R  U * p)"
    by (metis assms d_def_expl domain_up_down_conjugate sp_test_dist_oi_right top_sp_test_down_closed)
  also have "... = |Rp"
    by (metis adia assms inf.absorb_iff2 inf_commute top_down top_lower_greatest)
  finally show ?thesis
    by simp
qed

lemma ebox_up:
  assumes "test p"
  shows "|R]]p = |R]]p"
  by (metis Int_commute adia adia_up assms ebox semilattice_inf_class.inf_le1)

lemma adia_ebox:
  assumes "test p"
  shows "|Rp =  |R]]( p)"
  by (metis (no_types, lifting) adia assms d_complement_ad ebox test_double_complement)

lemma ebox_adia:
  assumes "test p"
  shows "|R]]p =  |R( p)"
  by (simp add: adia assms ebox)

lemma abox_down:
  assumes "test p"
  shows "|R]p = |R]p"
  by (simp add: abox assms)

lemma edia_down:
  assumes "test p"
  shows "|R⟩⟩p = |R⟩⟩p"
  by (simp add: assms edia)

lemma fusion_oi_complement_top_test_up:
  "test p  fus R  -(U * p)  (R  -(U * p))"
  apply (unfold top_test)
  apply (clarsimp simp: mr_simp)
  by blast

lemma adia_left_isotone:
  "test p  R  S  |Rp  |Sp"
  by (metis adia d_isotone inf.absorb_iff1 sp_test_dist_oi)

lemma adia_right_isotone:
  "test p  test q  p  q  |Rp  |Rq"
  by (metis (no_types, opaque_lifting) adia d_isotone inf.orderE inf_commute inf_le1 sp_test test_assoc3 test_s_prod_is_meet)

lemma abox_left_antitone:
  "test p  R  S  |S]p  |R]p"
  apply (clarsimp simp: mr_simp) by force

lemma abox_right_isotone:
  "test p  test q  p  q  |R]p  |R]q"
  by (smt (verit, ccfv_threshold) IntE abox_def inf.orderE mem_Collect_eq subsetI)

lemma edia_left_isotone:
  "test p  R  S  |R⟩⟩p  |S⟩⟩p"
  by (metis Int_mono adia_left_isotone down_isotone edia_adia order_refl)

lemma edia_right_isotone:
  "test p  test q  p  q  |R⟩⟩p  |R⟩⟩q"
  by (simp add: adia_right_isotone edia_adia)

lemma ebox_left_antitone:
  "test p  R  S  |S]]p  |R]]p"
  by (metis (no_types, lifting) adia_ebox adia_left_isotone ebox_adia test_complement_antitone test_double_complement)

lemma ebox_right_isotone:
  "test p  test q  p  q  |R]]p  |R]]q"
  by (smt (verit, ccfv_SIG) adia_ebox adia_right_isotone ebox inf_le2 test_complement_antitone test_double_complement)

lemma edia_fusion:
  assumes "test p"
  shows "|R⟩⟩p = |fus R⟩⟩p"
proof
  have "|fus R⟩⟩p = Dom (fus R  -(U *  p))"
    using assms edia_1 by blast
  also have "...  Dom (R  -(U *  p))"
    by (metis fusion_oi_complement_top_test_up d_isotone d_up semilattice_inf_class.inf_le2)
  also have "... = |R⟩⟩p"
    using assms edia_1 by blast
  finally show "|fus R⟩⟩p  |R⟩⟩p"
    .
next
  have "|R⟩⟩p  |(fus R)⟩⟩p"
    by (simp add: assms edia_left_isotone fusion_lower_increasing)
  thus "|R⟩⟩p  |fus R⟩⟩p"
    using assms edia_down by blast
qed

lemma abox_fusion:
  assumes "test p"
  shows "|R]p = |fus R]p"
  by (metis Int_lower2 abox_edia assms edia_fusion)

lemma abox_fission:
  assumes "test p"
  shows "|R]p = |fis R]p"
  by (metis assms abox_fusion fusion_fission)

lemma edia_fission:
  assumes "test p"
  shows "|R⟩⟩p = |fis R⟩⟩p"
  by (metis assms edia_fusion fusion_fission)

lemma fission_below:
  "fis R  S  (a b B . (a,B)  R  b  B  (a,{b})  S)"
  apply standard
   apply (simp add: basic_trans_rules(31) fission_set)
  apply (clarsimp simp: mr_simp)
  by blast

lemma below_fission_up:
  "S  (fis R)  (a B . (a,B)  S  (C . (a,C)  R  C  B  {}))"
proof
  assume "S  (fis R)"
  thus "a B . (a,B)  S  (C . (a,C)  R  C  B  {})"
    apply (clarsimp simp: mr_simp)
    by fastforce
next
  assume 1: "a B . (a,B)  S  (C . (a,C)  R  C  B  {})"
  show "S  (fis R)"
  proof
    fix x
    assume "x  S"
    from this obtain a B where 2: "x = (a,B)  (a,B)  S"
      by (metis surj_pair)
    hence "C . (a,C)  R  C  B  {}"
      using 1 by simp
    from this obtain C b where 3: "(a,C)  R  b  C  b  B"
      by auto
    hence "(a,{b})  fis R"
      using fission_set by blast
    thus "x  (fis R)"
      using 2 3 U_par_st by fastforce
  qed
qed

lemma ebox_below_abox:
  assumes "test p"
    and "fis R  S"
  shows "|S]]p  |R]p"
  by (metis abox_ebox abox_fission assms ebox_left_antitone fission_down_ne_fixpoint)

lemma abox_below_ebox:
  assumes "test p"
    and "S  (fis R)"
  shows "|R]p  |S]]p"
  by (metis abox_ebox abox_fission assms ebox_left_antitone ebox_up fission_down_ne_fixpoint)

lemma abox_eq_ebox:
  assumes "test p"
    and "fis R  S"
    and "S  (fis R)"
  shows "|R]p = |S]]p"
  by (simp add: abox_below_ebox assms ebox_below_abox subset_antisym)

lemma abox_eq_ebox_sufficient:
  "S = fis R  S = ne (R)  S = (ne (R))  fis R  S  S  (fis R)"
  apply (unfold imp_disjL)
  apply (intro conjI)
    apply (simp add: convex_reflexive)
   apply (simp add: fission_inner_deterministic fission_up_ne_down_up oi_subset_upper_right_antitone same_fusion_fission_lower)
  by (metis convex_reflexive fission_up_ne_down_up order_refl)

lemma ebox_fission_abox:
  "test p  |R]p = |fis R]]p"
  by (metis abox abox_fission ebox fission_down_ne_fixpoint)

lemma ebox_down_ne_up_abox:
  "test p  |R]p = |(ne (R))]]p"
  using abox_ebox ebox_up by blast

lemma same_fusion:
  assumes "fis R ⊑↓ S"
    and "S ⊑↓ fus R"
  shows "fis R = fis S"
  by (metis assms fission_down fission_fusion fission_fusion_galois subset_antisym)

lemma same_abox:
  assumes "fis R ⊑↓ S"
    and "S ⊑↓ fus R"
    and "test p"
  shows "|R]p = |S]p"
  by (metis assms ebox_fission_abox same_fusion)

lemma abox_ebox_inner_deterministic:
  assumes "test p"
    and "inner_deterministic R"
  shows "|R]p = |R]]p"
  apply (rule abox_eq_ebox)
    apply (simp add: assms(1))
  using assms(2) fission_inner_deterministic_fixpoint apply blast
  by (metis assms(2) convex_reflexive fission_inner_deterministic_fixpoint)

lemma adia_edia_inner_deterministic:
  assumes "test p"
    and "inner_deterministic R"
  shows "|Rp = |R⟩⟩p"
  by (metis assms edia_adia fission_down_ne_fixpoint fission_inner_deterministic_fixpoint)

lemma abox_adia_deterministic:
  assumes "test p"
    and "deterministic R"
  shows "|R]p = |Rp"
proof
  show "|R]p  |Rp"
  proof
    fix x
    assume "x  |R]p"
    from this obtain a where 1: "x = (a,{a})  (B . (a,B)  R  (bB . (b,{b})  p))"
      using abox_def by force
    from assms(2) obtain B where "(a,B)  R"
      by (meson deterministic_set)
    thus "x  |Rp"
      using 1 adia_def by fastforce
  qed
next
  show "|Rp  |R]p"
  proof
    fix x
    assume "x  |Rp"
    from this obtain a B where 2: "x = (a,{a})  (a,B)  R  (bB . (b,{b})  p)"
      by (smt adia_def mem_Collect_eq)
    have "C . (a,C)  R  (bC . (b,{b})  p)"
    proof (rule allI, rule impI)
      fix C
      assume "(a,C)  R"
      hence "B = C"
        using 2 by (metis assms(2) deterministic_set)
      thus "bC . (b,{b})  p"
        using 2 by simp
    qed
    thus "x  |R]p"
      using 2 abox_def by blast
  qed
qed

lemma ebox_edia_deterministic:
  assumes "test p"
    and "deterministic R"
  shows "|R]]p = |R⟩⟩p"
  by (simp add: assms abox_adia_deterministic ebox_adia edia_abox)

lemma abox_ebox_fusion:
  assumes "test p"
  shows "|fis R]p = |fis R]]p"
  by (metis abox_fission assms ebox_fission_abox)

lemma abox_fission_edia_fusion:
  assumes "test p"
  shows "|fis R]p = |fus Rp"
  by (simp add: abox_adia_deterministic abox_fusion assms fusion_deterministic fusion_fission)

lemma abox_adia_fusion:
  assumes "test p"
  shows "|fus R]p = |fus Rp"
  by (simp add: abox_adia_deterministic assms fusion_deterministic)

subsection ‹Goldblatt's axioms without star›

lemma abox_sp_unit:
  "|R]1 = 1"
  apply (clarsimp simp: mr_simp) by force

lemma ou_unit_abox:
  "test p  |{}]p = 1"
  by (metis abox_1 abox_sp_unit disjoint_eq_subset_Compl empty_subsetI inf.absorb_iff2 test_complement_closed)

lemma ou_unit_test_implication:
  "test p  {}  p = 1"
  by blast

lemma sp_unit_abox:
  "test p  |1]p = p"
  by (smt (verit) Int_left_commute abox_1 c1 cl8_var convex_reflexive d_ne_down_dp_complement_test fission_down_ne_fixpoint fission_inner_deterministic_fixpoint inf.absorb_iff2 inf_commute inner_deterministic_sp_unit s_subid_iff2 test_double_complement test_sp)

lemma sp_unit_test_implication:
  "test p  1  p = p"
  by simp

lemma test_abox_ebox:
  "test p  test q  |q]p = |q]]p"
  apply (rule antisym)
   apply (metis abox_ebox_inner_deterministic dual_order.trans inner_deterministic_sp_unit subset_refl)
  by (metis abox_ebox_inner_deterministic dual_order.eq_iff inner_deterministic_sp_unit inner_univalent_down_closed ne_equality test_ne)

lemma test_abox:
  "test p  test q  |q]p = q  p"
  by (smt Int_commute Int_lower2 abox cl9_var compl_sup d_complement_ad d_ne_down_dp_complement_test lattice_class.inf_sup_aci(2) sp_unit_abox test_ou_closed)

lemma abox_ou_adia_sp_unit:
  assumes "test p"
  shows "|R]p  |R1 = 1"
  apply (rule antisym)
   apply (simp add: assms abox adia_ebox)
  by (clarsimp simp: mr_simp)

lemma d_test_sp:
  "test p  Dom (p * R) = p * Dom R"
  by (simp add: c4 d_def_expl test_sp_left_dist_iu_1)

lemma ad_test_sp:
  "test p  aDom (p * R) =  p  aDom R"
  by (metis (no_types, opaque_lifting) Int_commute boolean_algebra.conj_disj_distrib boolean_algebra.de_Morgan_conj d_s_id_inter d_test_sp s_subid_iff2 test_fix)

lemma adia_test_sp:
  "test p  test q  |p * Rq = p * |Rq"
  by (metis (no_types, lifting) adia d_test_sp test_assoc3 test_double_complement)

lemma ebox_test_sp:
  "test p  test q  |p * R]]q =  p  |R]]q"
  by (simp add: ad_test_sp ebox test_assoc3)

lemma abox_test_sp:
  assumes "test p"
    and "test q"
  shows "|p * R]q =  p  |R]q"
proof -
  have "|p * R]q = aDom ((p * R)  -(U * q))"
    by (simp add: abox_1 assms(2))
  also have "... = aDom (p * (R  -(U * q)))"
    by (metis Int_assoc assms(1) test_sp)
  also have "... =  p  |R]q"
    by (simp add: abox_1 ad_test_sp assms)
  finally show ?thesis
    .
qed

lemma abox_test_sp_2:
  "test p  test q  p  |R]q = | p * R]q"
  by (simp add: abox_test_sp test_double_complement)

lemma abox_test_sp_3:
  "test p  test q  p  |R]q = |p * R]q"
  by (simp add: abox_test_sp)

lemma fission_sp_dist:
  "fis (R * S) = fis (R * Dom S) * fis S"
proof -
  have "S = Dom S * (S  aDom S * 1)"
    by (auto simp: mr_simp)
  hence "fis (R * S) = fis (R * Dom S * (S  aDom S * 1))"
    by (metis d_s_id_ax sp_test_sp_oi_right test_sp)
  also have "... = fis (R * Dom S) * fis (S  aDom S * 1)"
    apply (rule fission_sp_total_dist)
    by (smt (verit) total_dom Compl_disjoint ad_sp_bot ad_test_sp c6 compl_inf_bot d_complement_ad d_dist_ou inf_le2 iu_unit_down subset_Un_eq sup_ge2 sup_inf_absorb total_lower)
  also have "... = fis (R * Dom S) * (fis S  fis (aDom S * 1))"
    by (simp add: fission_dist_ou)
  also have "... = fis (R * Dom S) * fis S"
    by (simp add: fission_sp_iu_unit)
  finally show ?thesis
    .
qed

lemma abox_test:
  "test p  test ( |R]p )"
  by (simp add: abox)

lemma adia_test:
  "test p  test ( |Rp )"
  by (simp add: adia d_test)

lemma ebox_test:
  "test p  test ( |R]]p )"
  by (simp add: ebox)

lemma edia_test:
  "test p  test ( |R⟩⟩p )"
  by (simp add: edia d_test)

lemma abox_sp:
  assumes "test p"
    and "test q"
  shows "|R](p * q) = |R]p * |R]q"
proof -
  have "|R](p * q) = aDom (ne (R) * ( p   q))"
    by (metis (no_types, lifting) abox_1 ad_test_sp assms cl9_var d_ne_down_dp_complement_test sp_test test_double_complement test_oi_closed)
  also have "... = aDom (ne (R) *  p) * aDom (ne (R) *  q)"
    by (smt ad_test_sp cl9_var d_complement_ad d_dist_ou d_test_sp semilattice_inf_class.inf_le2 split_sp_test_7)
  also have "... = |R]p * |R]q"
    by (simp add: abox assms)
  finally show ?thesis
    .
qed

lemma adia_ou_below_ne_down:
  assumes "test p"
  shows "|R(p   q)  |Rp  |ne (R)( q)"
  by (metis adia assms d_dist_ou split_sp_test_6 test_complement_closed test_ou_closed)

lemma abox_adia_mp:
  assumes "test p"
    and "test q"
  shows "|R(p  q) * |R]p  |Rq"
  by (smt adia_ou_below_ne_down test_shunting abox adia assms d_complement_ad sup_commute test_complement_closed test_implication_closed)

lemma adia_abox_mp:
  assumes "test p"
    and "test q"
  shows "|Rp * |R](p  q)  |Rq"
proof -
  have "p  p  q  q"
    using assms(1) by blast
  hence "|Rp  |R((p  q)  q)"
    by (simp add: adia_right_isotone assms)
  thus ?thesis
    by (smt abox_adia_mp abox_test adia_test assms(2) semilattice_inf_class.inf.orderE semilattice_inf_class.le_infI2 test_implication_closed test_shunting)
qed

lemma abox_implication_adia:
  assumes "test p"
    and "test q"
  shows "|R](p  q)  |Rp  |Rq"
  by (metis adia_abox_mp test_shunting test_sp_commute Int_lower2 Un_commute abox_test adia_test assms test_ou_closed)

lemma abox_adia_implication:
  assumes "test p"
    and "test q"
  shows "|R]p  |Rq  |R(p * q)"
proof -
  have "p  q  p * q"
    by (metis assms subset_refl test_galois_1 test_sp_commute)
  hence "|R]p  |R](q  p * q)"
    by (simp add: abox_right_isotone assms test_galois_1)
  thus ?thesis
    by (metis (no_types, lifting) Int_Un_eq(2) abox_implication_adia assms le_sup_iff subset_Un_eq test_galois_1)
qed

lemma abox_mp:
  assumes "test p"
    and "test q"
  shows "|R]p * |R](p  q)  |R]q"
  by (metis (no_types, lifting) abox_right_isotone abox_sp assms semilattice_inf_class.inf.absorb_iff1 sp_test_dist_oi_left subset_refl sup_commute test_implication_closed test_shunting test_sp_commute)

lemma abox_implication:
  assumes "test p"
    and "test q"
  shows "|R](p  q)  |R]p  |R]q"
  by (metis abox_mp test_shunting test_sp_commute abox_test assms sup_commute test_implication_closed)

lemma ebox_left_dist_ou:
  assumes "test p"
  shows "|R  S]]p = |R]]p * |S]]p"
  by (auto simp: mr_simp)

lemma abox_left_dist_ou:
  assumes "test p"
  shows "|R  S]p = |R]p * |S]p"
  by (simp add: abox_ebox assms ebox_left_dist_ou ii_right_dist_ou ne_dist_ou)

lemma adia_left_dist_ou:
  assumes "test p"
  shows "|R  Sp = |Rp  |Sp"
  by (auto simp: mr_simp)

lemma edia_left_dist_ou:
  assumes "test p"
  shows "|R  S⟩⟩p = |R⟩⟩p  |S⟩⟩p"
  by (simp add: assms boolean_algebra.conj_disj_distrib2 d_dist_ou edia_1)

lemma abox_dist_iu_1:
  assumes "test p"
  shows "|R ∪∪ S]p = |Dom R * ne (S)]]p * |Dom S * ne (R)]]p"
proof
  have 1: "|R ∪∪ S]p  |Dom R * ne (S)]]p"
    by (metis abox_ebox assms d_sp_ne_down_below_ne_iu_down ebox_left_antitone)
  have "|R ∪∪ S]p  |Dom S * ne (R)]]p"
    by (metis abox_ebox assms d_sp_ne_down_below_ne_iu_down ebox_left_antitone iu_commute)
  thus "|R ∪∪ S]p  |Dom R * ne (S)]]p * |Dom S * ne (R)]]p"
    using 1 by (simp add: assms ebox)
next
  have "|Dom R * ne (S)]]p * |Dom S * ne (R)]]p  |Dom R * Dom S * ne (S)]]p * |Dom S * ne (R)]]p"
    apply (clarsimp simp: mr_simp)
    by (metis UN_I singletonI)
  also have "...  |Dom R * Dom S * ne (S)]]p * |Dom R * Dom S * ne (R)]]p"
    by (simp add: assms d_lb2 ebox_left_antitone s_prod_isol s_prod_isor)
  also have "... = |Dom R * Dom S * ne (S)  Dom R * Dom S * ne (R)]]p"
    using assms ebox_left_dist_ou by blast
  also have "... = |ne (Dom R * Dom S * S)  ne (Dom R * Dom S * R)]]p"
    by (metis d_dist_ii d_test test_sp_ne)
  also have "... = |ne ((Dom R * Dom S * S))  ne ((Dom R * Dom S * R))]]p"
    by (simp add: down_dist_sp)
  also have "... = aDom ((ne ((Dom R * Dom S * S))  ne ((Dom R * Dom S * R))) *  p)"
    using assms ebox by blast
  also have "...  aDom ((ne ((Dom R * Dom S * S ∪∪ Dom R * Dom S * R))) *  p)"
    using d_ne_iu_down_sp_test_ou by blast
  also have "... = |Dom R * Dom S * S ∪∪ Dom R * Dom S * R]p"
    using abox assms by blast
  also have "... = |Dom R * Dom S * (R ∪∪ S)]p"
    by (metis d_assoc1 d_inter_r p_prod_comm)
  also have "... = |R ∪∪ S]p"
    by (metis c1 cl8_var d_dist_iu)
  finally show "|Dom R * ne (S)]]p * |Dom S * ne (R)]]p  |R ∪∪ S]p"
    .
qed

lemma abox_dist_iu_2:
  assumes "test p"
  shows "|R ∪∪ S]p = |Dom R * S]p * |Dom S * R]p"
proof -
  have "|Dom R * ne (S)]]p * |Dom S * ne (R)]]p = |ne ((Dom R * S))]]p * |ne ((Dom S * R))]]p"
    by (simp add: d_test down_dist_sp test_sp_ne)
  also have "... = |Dom R * S]p * |Dom S * R]p"
    by (simp add: abox_ebox assms)
  finally show ?thesis
    using assms abox_dist_iu_1 by blast
qed

lemma abox_dist_iu_3:
  assumes "test p"
  shows "|R ∪∪ S]p = ( |R1  |S]p ) * ( |S1  |R]p )"
  by (metis abox_dist_iu_2 adia assms abox_test_sp d_test s_prod_idr subset_refl)

lemma abox_adia_sp_one_set:
  "|R]|S1 = { (a,{a}) | a . B . (a,B)  R  (bB . D . (b,D)  S) }"
  by (auto simp: abox_def Dom_def adia)

lemma abox_abox_set:
  "|R]|S]p = { (a,{a}) | a . B . (a,B)  R  (C . (bB . (b,C)  S)  (cC . (c,{c})  p)) }"
  by (auto simp: abox_def)

lemma sp_abox_set:
  "|R * S]p = { (a,{a}) | a . B . (a,B)  R  (C . (f . (bB . (b,f b)  S)  C = { f b | b . b  B })  (cC . (c,{c})  p)) }"
  apply (unfold abox_def s_prod_def)
  by blast

lemma abox_sp_1:
  assumes "test p"
  shows "|R]|S1 * |R * S]p  |R]|S]p"
proof -
  have "|R]|S1 * |R * S]p = |R]|S1  |R * S]p"
    by (smt (verit, ccfv_SIG) abox_test adia_test assms convex_increasing inf.orderE inf_assoc sp_unit_convex test_s_prod_is_meet)
  also have "...  |R]|S]p"
  proof
    fix x
    assume "x  |R]|S1  |R * S]p"
    from this obtain a where 1: "x = (a,{a})  x  |R]|S1  x  |R * S]p"
      by (metis Int_iff abox_test adia_test order_refl subid_aux2 subsetD surj_pair)
    hence 2: "B . (a,B)  R  (bB . D . (b,D)  S)"
      by (smt abox_adia_sp_one_set mem_Collect_eq old.prod.inject)
    have 3: "B . (a,B)  R  (C . (f . (bB . (b,f b)  S)  C = { f b | b . b  B })  (cC . (c,{c})  p))"
      using 1 by (smt sp_abox_set mem_Collect_eq old.prod.inject)
    have "B . (a,B)  R  (C . (bB . (b,C)  S)  (cC . (c,{c})  p))"
    proof (rule allI, rule impI)
      fix B
      assume 4: "(a,B)  R"
      hence "DD . bB . (b,DD b)  S"
        using 2 by (auto intro: bchoice)
      from this obtain DD where 5: "bB . (b,DD b)  S"
        by auto
      show "C . (bB . (b,C)  S)  (cC . (c,{c})  p)"
      proof (rule allI, rule impI)
        fix C
        assume "bB . (b,C)  S"
        from this obtain b where 6: "b  B  (b,C)  S"
          by auto
        let ?f = "λx . if x = b then C else DD x"
        let ?C = "C  { ?f x | x . x  B  x  b }"
        have "f . (bB . (b,f b)  S)  ?C = { f b | b . b  B }"
          apply (rule exI[where ?x="?f"])
          using 5 6 by auto
        hence "c?C . (c,{c})  p"
          using 3 4 by auto
        thus "cC . (c,{c})  p"
          by blast
      qed
    qed
    thus "x  |R]|S]p"
      using 1 abox_abox_set by blast
  qed
  finally show ?thesis
    .
qed

lemma abox_sp_2:
  assumes "test p"
  shows "|R]|S]p = |R * S]p"
proof -
  have "|R]|S]p = aDom (ne (R) * Dom (ne (S) *  p))"
    by (metis abox abox_test assms d_complement_ad)
  also have "... = aDom (ne (R) * ne (S) *  p)"
    by (simp add: test_assoc3)
  also have "... = aDom (ne ((R * S)) *  p)"
    by (simp add: down_dist_sp ne_dist_down_sp)
  also have "... = |R * S]p"
    by (simp add: abox assms)
  finally show ?thesis
    .
qed

lemma abox_sp_3:
  assumes "test p"
  shows "|R]|S]p  |R * S]p"
  by (clarsimp simp: mr_simp) auto

lemma abox_sp_4:
  assumes "test p"
  shows "|R * S]p  |R]|S1  |R]|S]p"
proof -
  have "|R]|S1 * |R * S]p  |R]|S]p"
    by (auto simp: assms abox_sp_1)
  hence "|R]|S1  |R * S]p  |R]|S]p"
    by (smt (verit) abox_test adia_test assms convex_increasing inf.orderE sp_unit_convex test_oi_closed test_s_prod_is_meet)
  thus ?thesis
    using abox_test assms by blast
qed

lemma abox_sp_5:
  assumes "test p"
  shows "|R]|S1 * |R * S]p = |R]|S1 * |R]|S]p"
proof (rule antisym)
  have "|R * S]p  |R]|S1  |R]|S]p"
    by (simp add: abox_sp_4 assms)
  hence "|R]|S1  |R * S]p  |R]|S]p"
    by blast
  hence "|R]|S1  |R * S]p  |R]|S1  |R]|S]p"
    by blast
  thus "|R]|S1 * |R * S]p  |R]|S1 * |R]|S]p"
    by (smt (verit, del_insts) abox_test adia_test assms convex_increasing inf.orderE sp_unit_convex test_oi_closed test_s_prod_is_meet)
  show "|R]|S1 * |R]|S]p  |R]|S1 * |R * S]p"
    by (simp add: abox_sp_3 assms s_prod_isor)
qed

lemma abox_sp_6:
  assumes "test p"
  shows "|R]|S1  |R * S]p = |R]|S1  |R]|S]p"
  by (smt Int_commute abox_sp_3 abox_sp_4 assms inf_sup_distrib2 lattice_class.inf_sup_absorb semilattice_inf_class.inf.absorb_iff2 sup_commute)

lemma abox_sp_7:
  assumes "test p"
    and "total S"
  shows "|R * S]p = |R]|S]p"
  by (metis (no_types, lifting) abox_ebox abox_sp_2 assms down_dist_sp total_down_dist_sp)

lemma adia_sp_associative:
  assumes "test p"
  shows "|Q * (R * S)p = |(Q * R) * Sp"
proof -
  have "|Q * (R * S)p = |Q( |R( |Sp))"
    by (metis (no_types, lifting) adia adia_test assms d_loc_ax inf.orderE test_assoc3)
  also have " = |(Q * R) * Sp"
    by (smt (verit, best) adia adia_test assms d_loc test_assoc3 test_double_complement)
  finally show "|Q * (R * S)p = |(Q * R) * Sp"
    .
qed

lemma ebox_sp_associative:
  assumes "test p"
  shows "|Q * (R * S)]]p = |(Q * R) * S]]p"
  by (simp add: adia_sp_associative assms ebox_adia)

lemma edia_sp_associative:
  assumes "test p"
  shows "|Q * (R * S)⟩⟩p = |(Q * R) * S⟩⟩p"
proof -
  have "|fis (Q * (R * S))⟩⟩p = |fis (Q * Dom (R * S)) * (fis (R * Dom S) * fis S)⟩⟩p"
    by (metis fission_sp_dist)
  also have "... = |(fis (Q * Dom (R * S)) * fis (R * Dom S)) * fis S⟩⟩p"
    by (simp add: inner_deterministic_sp_assoc semilattice_inf_class.inf_commute semilattice_inf_class.le_infI1 fission_var)
  also have "... = |fis (Q * Dom (R * Dom S)) * fis (R * Dom S) * fis S⟩⟩p"
    by simp
  also have "... = |fis (Q * (R * Dom S)) * fis S⟩⟩p"
    by (metis fission_sp_dist)
  also have "... = |fis ((Q * R) * Dom S) * fis S⟩⟩p"
    by (metis d_complement_ad test_assoc3)
  also have "... = |fis ((Q * R) * S)⟩⟩p"
    by (metis fission_sp_dist)
  finally show ?thesis
    using assms edia_fission by blast
qed

lemma abox_sp_associative:
  assumes "test p"
  shows "|Q * (R * S)]p = |(Q * R) * S]p"
  by (simp add: edia_sp_associative assms abox_edia)

lemma abox_oI:
  assumes "X  {}"
  shows "|R]X = (pX . |R]p)"
  apply (rule antisym)
   apply (clarsimp simp: mr_simp)
  apply (clarsimp simp: mr_simp)
  using assms by blast

lemma ebox_left_dist_oU:
  assumes "X  {}"
  shows "|X]]p = (RX . |R]]p)"
  apply (rule antisym)
   apply (clarsimp simp: mr_simp)
   apply blast
  apply (clarsimp simp: mr_simp)
  using assms by blast

lemma abox_left_dist_oU:
  assumes "X  {}"
  shows "|X]p = (RX . |R]p)"
  apply (rule antisym)
   apply (clarsimp simp: mr_simp)
   apply blast
  apply (clarsimp simp: mr_simp)
  using assms by blast

lemma adia_left_dist_oU:
  "|Xp = (RX . |Rp)"
  apply (clarsimp simp: mr_simp)
  by blast

lemma edia_left_dist_oU:
  "|X⟩⟩p = (RX . |R⟩⟩p)"
  apply (clarsimp simp: mr_simp)
  by blast

subsection ‹Goldblatt's axioms with star›

no_notation rtrancl ("(_*)" [1000] 999)
notation star ("_*" [1000] 999)

lemma star_induct_1:
  assumes "1  X"
    and "R * X  X"
  shows "R*  X"
  apply (unfold star_def)
  apply (rule lfp_lowerbound)
  by (simp add: assms)

lemma star_induct:
  assumes "S  1  1"
    and "S  X"
    and "R * X  X"
  shows "R* * S  X"
proof -
  have "R*  X  S"
  proof (rule star_induct_1)
    show "1  X  S"
      by (metis (no_types, opaque_lifting) Int_subset_iff assms(2) dual_order.eq_iff sp_lres_galois test_sp)
  next
    have "(X  S) * S  X"
      by (simp add: sp_lres_sp_below)
    hence "R * (X  S) * S  R * X"
      by (metis assms(1) s_prod_isor test_iu_test_sp_assoc_5)
    also have "...  X"
      by (simp add: assms(3))
    finally show "R * (X  S)  X  S"
      by (simp add: sp_lres_galois)
  qed
  thus ?thesis
    by (simp add: sp_lres_galois)
qed

lemma star_total:
  "total (R*)"
  by (metis s_prod_idl s_prod_isol star_refl total_4)

lemma star_down:
  "R* = (R)*  1"
proof
  have "R* * (1  1)  (R)*  1"
  proof (rule star_induct)
    show "1  1  1  1"
      by simp
  next
    show "1  1  (R)*  1"
      using star_refl by auto
  next
    have "ne (R * ((R)*  1))  ne (R * ((R)*  1))"
      by (simp add: down_sp_sp sup_commute)
    also have "... = ne (R) * ne ((R)*  1)"
      by (simp add: ne_dist_down_sp)
    also have "... = ne (R) * ne ((R)*)"
      by (metis down_idempotent down_sp_sp ne_dist_down_sp sup_commute)
    also have "...  R * (R)*"
      using sp_oi_subdist by blast
    also have "...  (R)*"
      using star_unfold_eq by blast
    finally show "R * ((R)*  1)  (R)*  1"
      by blast
  qed
  thus "R*  (R)*  1"
    by (simp add: down_sp sup_commute)
next
  have "(R)*  R*"
  proof (rule star_induct_1)
    show "1  R*"
      by (simp add: star_refl subset_lower)
  next
    show "R * R*  R*"
      by (metis total_dom Un_Int_eq(1) d_isotone d_test ii_right_dist_ou inf_le2 le_sup_iff s_subid_iff2 star_unfold_eq subset_antisym total_down_dist_sp)
  qed
  thus "(R)*  1  R*"
    using star_total total_lower by blast
qed

lemma ne_star_down:
  "ne (R*) = ne ((R)*)"
  by (simp add: ne_dist_ou star_down)

lemma ne_down_star:
  "ne ((R)*) = (ne (R))*"
proof
  have "(R)*  (ne (R))*  1"
  proof (rule star_induct_1)
    show "1  (ne (R))*  1"
      by (simp add: le_supI1 star_refl)
  next
    have "ne (R * ((ne (R))*  1)) = ne (R) * ne ((ne (R))*)"
      by (metis down_idempotent down_sp_sp ne_dist_down_sp sup_commute)
    also have "...  (ne (R))*"
      by (metis (no_types, lifting) IntE UnCI inf.absorb_iff2 sp_oi_subdist star_unfold_eq subsetI)
    finally show "R * ((ne (R))*  1)  ((ne (R))*  1)"
      by blast
  qed
  thus "ne ((R)*)  (ne (R))*"
    by (smt Compl_disjoint2 Int_commute Int_left_commute ne_dist_ou semilattice_inf_class.le_iff_inf sup_bot.right_neutral)
next
  show "(ne (R))*  ne ((R)*)"
  proof (rule star_induct_1)
    show "1  ne ((R)*)"
      using star_refl test_ne by auto
  next
    show "ne (R) * ne ((R)*)  ne ((R)*)"
      by (metis IntE IntI UnCI ne_dist_down_sp star_unfold_eq subsetI)
  qed
qed

lemma abox_star_unfold:
  "test p  |R*]p = p * |R]|R*]p"
  by (metis abox_left_dist_ou abox_sp_7 sp_unit_abox star_total star_unfold_eq)

lemma star_sp_test_commute:
  assumes "S  1  1"
    and "Q * S  S * R"
  shows "Q* * S  S * R*"
proof (rule star_induct)
  show "S  1  1"
    by (simp add: assms(1))
next
  show "S  S * R*"
    by (metis s_prod_idr s_prod_isor star_refl)
next
  have "Q * (S * R*)  S * R * R*"
    by (metis (no_types, lifting) assms s_prod_distr subset_Un_eq test_iu_test_sp_assoc_3)
  thus "Q * (S * R*)  S * R*"
    by (metis (no_types, lifting) UnCI dual_order.trans s_prod_assoc1 s_prod_isor star_unfold subset_eq)
qed

lemma adia_star_induct:
  assumes "test p"
  shows "|Rp  p  |R*p  p"
proof
  assume "|Rp  p"
  hence " p * Dom (R * p) = {}"
    by (metis adia assms d_idem2 s_prod_isol subset_empty test_sp_shunting)
  hence "R * p  p * (R * p)"
    by (metis assms d_sp_strict subset_refl test_sp_shunting)
  hence "R * p  p * R"
    by (metis assms inf.absorb_iff2 inf_commute sp_test_dist_oi_right test_assoc3 test_sp_idempotent)
  hence "R* * p  p * R*"
    by (simp add: assms le_supI1 star_sp_test_commute)
  hence "R* * p  p * (R* * p)"
    by (metis assms inf.absorb_iff2 inf.orderE sp_oi_subdist test_assoc3 test_sp_idempotent)
  hence " p * (R* * p) = {}"
    by (meson assms subset_empty test_sp_shunting)
  hence " p * Dom (R* * p) = {}"
    using d_sp_strict by blast
  thus "|R*p  p"
    by (metis adia assms d_test empty_subsetI semilattice_inf_class.le_inf_iff sp_test test_sp_shunting)
next
  assume "|R*p  p"
  thus "|Rp  p"
    by (metis adia_left_isotone assms dual_order.trans s_prod_idr s_prod_isor star_refl star_unfold sup.coboundedI2)
qed

lemma ebox_star_induct:
  assumes "test p"
  shows "p  |R]]p  p  |R*]]p"
  by (smt (verit, best) adia adia_star_induct assms d_complement_ad ebox_adia test_complement_antitone test_double_complement)

lemma abox_star_induct:
  assumes "test p"
  shows "p  |R]p  p  |R*]p"
proof -
  have "p  |ne (R)]]p  p  |ne (R*)]]p"
    by (metis assms ebox_star_induct ne_down_star ne_star_down)
  thus ?thesis
    by (metis abox_ebox assms)
qed

lemma edia_star_induct:
  assumes "test p"
  shows "|R⟩⟩p  p  |R*⟩⟩p  p"
  by (metis adia_star_induct assms edia_adia ne_down_star ne_star_down)

lemma abox_star_induct_1:
  assumes "test p"
    and "test q"
    and "q  p * |R]q"
  shows "q  |R*]p"
proof -
  have "q  p  q  |R*]q"
    by (metis Int_subset_iff abox_star_induct abox_test assms test_sp test_sp_commute)
  thus ?thesis
    using abox_right_isotone assms(1,2) by blast
qed

lemma adia_star_induct_1:
  assumes "test p"
    and "test q"
    and "p  |Rq  q"
  shows "|R*p  q"
  by (meson adia_right_isotone adia_star_induct assms order.trans sup.bounded_iff)

lemma abox_segerberg:
  assumes "test p"
  shows "|R*](p  |R]p)  p  |R*]p"
proof -
  have "p * |R*](p  |R]p)  |R*]p"
  proof (rule abox_star_induct_1)
    show "test p"
      by (simp add: assms)
  next
    show "test (p * |R*](p  |R]p))"
      by (simp add: abox_test assms test_galois_1)
  next
    have "p * |R*](p  |R]p) = p * (p  |R]p) * |R]|R*](p  |R]p)"
      by (metis abox_star_unfold abox_test assms inf_le2 le_infE sp_unit_convex sp_unit_down test_iu_test_sp_assoc_1 test_ou_closed)
    also have "... = p * |R]p * |R]|R*](p  |R]p)"
      by (smt (verit, best) Un_Int_eq(4) abox_left_dist_ou abox_test assms equalityD1 le_infE s_prod_isol sp_unit_abox sp_unit_convex sp_unit_down subset_Un_eq subset_antisym test_galois_1 test_iu_test_sp_assoc_1 test_ou_closed test_sp_commute)
    also have "... = p * |R](p * |R*](p  |R]p))"
      by (metis (no_types, lifting) abox_sp abox_test abox_test_sp_3 assms test_assoc2 test_double_complement)
    finally show "p * |R*](p  |R]p)  p * |R](p * |R*](p  |R]p))"
      by simp
  qed
  thus ?thesis
    by (meson abox_test assms test_galois_1 test_implication_closed)
qed

lemma abox_segerberg_adia:
  assumes "test p"
  shows "|R*]( |Rp  p )  |R*p  p"
proof -
  let ?q = "|R*]( |Rp  p )"
  have "|R*p  ?q  p"
  proof (rule adia_star_induct_1)
    show "test p"
      by (simp add: assms)
  next
    show "test ( ?q  p )"
      by (simp add: assms)
  next
    have "|R(?q  p) * |R]?q * ( |Rp  p )  |Rp * ( |Rp  p )"
      by (metis (no_types, lifting) abox_adia_mp abox_test assms inf.absorb_iff2 sp_test_dist_oi test_implication_closed)
    also have "...  p"
      by (meson adia_test assms equalityD2 test_galois_1 test_implication_closed)
    finally have "|R(?q  p)  ( |Rp  p ) * |R]?q  p"
      by (smt (verit) abox_star_unfold abox_test adia assms d_complement_ad test_assoc3 test_double_complement test_galois_1 test_implication_closed test_sp_commute)
    also have "... = ?q  p"
      by (metis abox_star_unfold assms test_implication_closed)
    finally show "p  |R( ?q  p )  ?q  p"
      by (metis le_sup_iff order_refl)
  qed
  thus ?thesis
    by (smt abox_test adia_test assms sup_commute test_galois_1 test_implication_closed test_shunting)
qed

lemma s_p_id_sp:
  "(s_id  p_id) * R = R  p_id"
  by (simp add: s_prod_distr)

subsection ‹Propositional Hoare logic›

abbreviation hoare :: "('a,'a) mrel  ('a,'b) mrel  ('b,'b) mrel  bool" ("___" [50,60,50] 95)
  where "pRq  p  |R]q"

abbreviation if_then_else :: "('a,'a) mrel  ('a,'b) mrel  ('a,'b) mrel  ('a,'b) mrel"
  where "if_then_else p R S  p * R   p * S"

abbreviation while_do :: "('a,'a) mrel  ('a,'a) mrel  ('a,'a) mrel"
  where "while_do p R  (p * R)* *  p"

lemma hoare_skip:
  assumes "test p"
    shows "p1p"
  by (simp add: assms sp_unit_abox)

lemma hoare_cons:
  assumes "test s"
      and "r  p"
      and "q  s"
      and "pRq"
    shows "rRs"
  by (meson abox_right_isotone assms order_trans)

lemma hoare_seq:
  assumes "test q"
      and "test r"
      and "pRq"
      and "qSr"
    shows "pR*Sr"
proof -
  have "p  |R]q"
    by (simp add: assms(3))
  also have "...  |R]|S]r"
    by (simp add: abox_right_isotone abox_test assms(1,2,4))
  also have "...  |R*S]r"
    by (simp add: abox_sp_3 assms(2))
  finally show ?thesis
    by simp
qed

lemma hoare_if:
  assumes "test p"
      and "test q"
      and "test r"
      and "(p*q)Rr"
      and "(( p)*q)Sr"
  shows "qif_then_else p R Sr"
  by (smt (verit, ccfv_threshold) abox_left_dist_ou abox_test_sp assms inf.absorb_iff2 inf_le2 sp_oi_subdist test_galois_1 test_sp_idempotent)

lemma hoare_while:
  assumes "test p"
      and "test q"
      and "(p*q)Rq"
    shows "qwhile_do p R(q*( p))"
proof -
  have "q  p  |R]q"
    by (meson assms test_galois_1)
  also have "... = |p]|R]q"
    by (simp add: abox_test assms(1,2) test_abox)
  also have "...  |p*R]q"
    by (simp add: abox_sp_3 assms(2))
  finally have "q  |(p*R)*]q"
    by (meson abox_star_induct assms(2))
  also have "...  |(p*R)*](q  p)"
    by (simp add: abox_right_isotone assms(1,2))
  also have "... = |(p*R)*](p  (q*( p)))"
    by (smt (verit, best) Un_assoc Un_upper1 assms(1,2) inf_commute sup.commute sup.order_iff test_double_complement test_galois_1 test_s_prod_is_meet)
  also have "... = |(p*R)*]|p](q*( p))"
    by (simp add: assms(2) test_abox test_shunting)
  also have "...  |while_do p R](q*( p))"
    by (simp add: abox_sp_3 assms(2) test_galois_1)
  finally show ?thesis
    by simp
qed

lemma hoare_par:
  assumes "test q"
      and "pRq"
      and "pSq"
    shows "pR ∪∪ Sq"
proof -
  have 1: "p  |R1  |S]q"
    by (simp add: assms(3) le_supI2)
  have "p  |S1  |R]q"
    by (simp add: assms(2) le_supI2)
  hence "p  ( |R1  |S]q)  ( |S1  |R]q)"
    using 1 by simp
  also have "... = |R ∪∪ S]q"
    by (smt (verit) abox_dist_iu_3 abox_test assms(1) inf.orderE test_implication_closed test_oi_closed test_s_prod_is_meet)
  finally show ?thesis
    by simp
qed

section ‹Counterexamples›

locale counterexamples 
begin

lemma counter_01:
  "¬ ((U::('a,'b) mrel) * -((U::('b,'c) mrel) * (R::('c,'d) mrel))  -(U * R))"
  by (metis UNIV_I U_par_zero disjoint_eq_subset_Compl emptyE iu_unit_below_top_sp_test iu_unit_up le_inf_iff s_prod_zerol subset_empty top_upper_least)

abbreviation "a_1  finite_1.a1"

lemma counter_02:
  "R::(Enum.finite_1,Enum.finite_1) mrel . p . ¬ (test p  (R  -(U * p)) * U = R * -(p * U))"
  apply (rule exI[where ?x="{(a_1,{})}"])
  apply (rule exI[where ?x="{}"])
  apply (clarsimp simp: s_id_def)
  by (smt (verit, ccfv_SIG) Compl_empty_eq Diff_eq Int_insert_left_if0 U_par_p_id cl8_var complement_test_sp_top d_U d_sp_strict dc empty_subsetI inf_le2 inf_top_left inner_total_2 insert_not_empty s_prod_zerol x_split_var x_y_split zero_nc)

lemma counter_03:
  "R::(Enum.finite_1,Enum.finite_1) mrel . p . ¬ (test p  (R  -(U * p)) * 1 = R * (-(p * U)  1))"
  apply (rule exI[where ?x="{(a_1,{})}"])
  apply (rule exI[where ?x="{}"])
  apply (clarsimp simp: s_id_def)
  by (smt (z3) Int_Un_eq(3) Int_absorb2 U_c ad_sp_bot cd_iso dc_prop1 disjoint_eq_subset_Compl inf_compl_bot_right inner_total_2 insertI1 p_id_zero singleton_Un_iff sp_oi_subdist)

abbreviation "b_1  finite_2.a1"
abbreviation "b_2  finite_2.a2"
abbreviation "b_1_0  (b_1,{})"
abbreviation "b_1_1  (b_1,{b_1})"
abbreviation "b_1_2  (b_1,{b_2})"
abbreviation "b_1_3  (b_1,{b_1,b_2})"
abbreviation "b_2_0  (b_2,{})"
abbreviation "b_2_1  (b_2,{b_1})"
abbreviation "b_2_2  (b_2,{b_2})"
abbreviation "b_2_3  (b_2,{b_1,b_2})"

lemma counter_04:
  "R::(Enum.finite_2,Enum.finite_2) mrel . p q . ¬ (test p  test q  |R * p]q = |R]|p]q)"
  apply (rule exI[where ?x="{b_1_3}"])
  apply (rule exI[where ?x="{b_1_1}"])
  apply (rule exI[where ?x="{}"])
  apply (subst sp_test)
   apply (clarsimp simp: s_id_def)
  apply (subst top_test)
   apply (clarsimp simp: s_id_def)
  apply (unfold abox_def)
  apply (clarsimp simp: s_id_def)
  by blast

lemma counter_05:
  "¬ (f . R p . test p  |Rp = |f R]p)"
  by (smt (verit, ccfv_threshold) Int_lower1 Int_lower2 abox_sp_unit adia_test_sp counter_01 iu_test_sp_left_zero s_prod_idl subset_refl)

lemma counter_06:
  "¬ (f . R p . test p  |R]]p = |f R]p)"
  by (metis abox_adia_fusion abox_fusion abox_sp_unit adia counter_05 d_complement_ad disjoint_eq_subset_Compl ebox_adia empty_subsetI s_prod_idr order_refl)

lemma counter_07:
  "¬ (f . mono f  (R . fus R = lfp (λX . f R X)))"
proof
  assume "f::('a,'b) mrel  ('a,'b) mrel  ('a,'b) mrel . mono f  (R . fus R = lfp (λX . f R X))"
  from this obtain f :: "('a,'b) mrel  ('a,'b) mrel  ('a,'b) mrel" where "mono f  (R . fus R = lfp (λX . f R X))"
    by auto
  hence "fus {}  fus (U::('a,'b) mrel)"
    by (simp add: le_fun_def mono_def lfp_mono)
  thus False
    by (auto simp: mr_simp)
qed

abbreviation "c_1  finite_3.a1"
abbreviation "c_2  finite_3.a2"
abbreviation "c_3  finite_3.a3"

lemma counter_08:
  "¬ ((1::(Enum.finite_3,Enum.finite_3) mrel) * 1  {1, 1})"
proof -
  let ?c = "(c_1,{c_1,c_2,c_3})"
  have 1: "?c  1 * 1"
    apply (clarsimp simp: mr_simp)
    apply (rule exI[where ?x="{c_2,c_3}"])
    using UNIV_finite_3 by auto
  have "?c  1  ?c  1"
    by (auto simp: mr_simp)
  thus ?thesis
    using 1 by auto
qed

lemma counter_09:
  "¬ ((1::(Enum.finite_3,Enum.finite_3) mrel)  1  {1, 1})"
  by (metis counter_08 co_prod empty_iff ic_involutive insert_iff)

lemma ex_2_cases:
  "b. b = b_1  b = b_2"
  by auto

lemma all_2_cases:
  "(b. b = b_2  b = b_1) = False"
  by auto

lemma impl_2_cases:
  "{ X . b. (b = b_1  X = Y)  (b = b_2  X = Z)} = Y  Z"
  by auto

lemma ex_2_set_cases:
  "(B::Enum.finite_2 set . P B)  P {}  P {b_1}  P {b_2}  P {b_1,b_2}"
proof -
  let ?U = "UNIV::Enum.finite_2 set set"
  have "?U  {{},{b_1},{b_2},{b_1,b_2}}"
  proof
    fix x
    have "x  {b_1,b_2}"
      by auto
    thus "x  {{},{b_1},{b_2},{b_1,b_2}}"
      by auto
  qed
  hence "?U = {{},{b_1},{b_2},{b_1,b_2}}"
    by auto
  thus ?thesis
    by (metis UNIV_I empty_iff insertE)
qed

abbreviation "B_0  {}::Enum.finite_2 set"
abbreviation "B_1  {b_1}"
abbreviation "B_2  {b_2}"
abbreviation "B_3  {b_1,b_2}"
abbreviation "mkf x y  λz . if z = b_1 then x else y"

lemma mkf:
  "f = mkf (f b_1) (f b_2)"
  by auto

lemma mkf2:
  "f b_1 = X  f b_2 = Y  f = mkf X Y"
  by auto

lemma ex_2_mrel_cases:
  "(f::Enum.finite_2  Enum.finite_2 set . P f) 
    P (mkf B_0 B_0)  P (mkf B_0 B_1)  P (mkf B_0 B_2)  P (mkf B_0 B_3) 
    P (mkf B_1 B_0)  P (mkf B_1 B_1)  P (mkf B_1 B_2)  P (mkf B_1 B_3) 
    P (mkf B_2 B_0)  P (mkf B_2 B_1)  P (mkf B_2 B_2)  P (mkf B_2 B_3) 
    P (mkf B_3 B_0)  P (mkf B_3 B_1)  P (mkf B_3 B_2)  P (mkf B_3 B_3)"
proof
  assume "f::Enum.finite_2  Enum.finite_2 set . P f"
  from this obtain f where 1: "P f"
    by auto
  have "x . f x  B_3"
    by auto
  hence 2: "x . f x = B_0  f x = B_1  f x = B_2  f x = B_3"
    by auto
  have "f = mkf B_0 B_0  f = mkf B_0 B_1  f = mkf B_0 B_2  f = mkf B_0 B_3 
        f = mkf B_1 B_0  f = mkf B_1 B_1  f = mkf B_1 B_2  f = mkf B_1 B_3 
        f = mkf B_2 B_0  f = mkf B_2 B_1  f = mkf B_2 B_2  f = mkf B_2 B_3 
        f = mkf B_3 B_0  f = mkf B_3 B_1  f = mkf B_3 B_2  f = mkf B_3 B_3"
    using 2[of b_1] 2[of b_2] mkf2[of f] by blast
  thus "P (mkf B_0 B_0)  P (mkf B_0 B_1)  P (mkf B_0 B_2)  P (mkf B_0 B_3) 
        P (mkf B_1 B_0)  P (mkf B_1 B_1)  P (mkf B_1 B_2)  P (mkf B_1 B_3) 
        P (mkf B_2 B_0)  P (mkf B_2 B_1)  P (mkf B_2 B_2)  P (mkf B_2 B_3) 
        P (mkf B_3 B_0)  P (mkf B_3 B_1)  P (mkf B_3 B_2)  P (mkf B_3 B_3)"
    using 1 by auto
next
  assume "P (mkf B_0 B_0)  P (mkf B_0 B_1)  P (mkf B_0 B_2)  P (mkf B_0 B_3) 
          P (mkf B_1 B_0)  P (mkf B_1 B_1)  P (mkf B_1 B_2)  P (mkf B_1 B_3) 
          P (mkf B_2 B_0)  P (mkf B_2 B_1)  P (mkf B_2 B_2)  P (mkf B_2 B_3) 
          P (mkf B_3 B_0)  P (mkf B_3 B_1)  P (mkf B_3 B_2)  P (mkf B_3 B_3)"
  thus "f::Enum.finite_2  Enum.finite_2 set . P f"
    by auto
qed

lemma counter_10:
  "R::(Enum.finite_2,Enum.finite_2) mrel . ¬ (U::(Enum.finite_2,Enum.finite_2) mrel) * (U * R)  U * R"
  apply (rule exI[where ?x="{b_1_1,b_1_2}"])
  apply (unfold s_prod_def)
  apply (unfold ex_2_set_cases)
  apply (unfold ex_2_mrel_cases)
  apply (clarsimp simp: mr_simp ex_2_cases all_2_cases impl_2_cases)
  by auto

lemma counter_11:
  "(R::(Enum.finite_2,Enum.finite_2) mrel) (s::(Enum.finite_2,Enum.finite_2) mrel) (t::(Enum.finite_2,Enum.finite_2) mrel) . ¬ (inner_univalent s  inner_univalent t  R * (s * t) = (R * s) * t)"
  apply (rule exI[where ?x="{b_1_3}"])
  apply (rule exI[where ?x="{b_1_1,b_2_1}"])
  apply (rule exI[where ?x="{b_1_1,b_1_2}"])
  apply (unfold s_prod_def)
  apply (unfold ex_2_set_cases)
  apply (unfold ex_2_mrel_cases)
  apply (clarsimp simp: mr_simp ex_2_cases all_2_cases impl_2_cases)
  by (auto simp: times_eq_iff)

lemma counter_12:
  "¬(S . 1  S = 1)"
  by (metis Int_absorb2 UNIV_I U_U cl9 co_prod cp_ii_unit_upper disjoint_iff_not_equal ic_antidist_ii ic_iu_unit ic_top iu_unit_down p_prod_comm p_prod_ild s_prod_idl s_prod_p_idl)

lemma counter_13:
  "¬(S . R . R  S = R)"
  by (meson counter_12)
end

end