diff --git a/thys/Multirelations_Heterogeneous/Multirelations.thy b/thys/Multirelations_Heterogeneous/Multirelations.thy --- a/thys/Multirelations_Heterogeneous/Multirelations.thy +++ b/thys/Multirelations_Heterogeneous/Multirelations.thy @@ -1,6215 +1,6310 @@ 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\<^sub>\\<^sub>\") where "1\<^sub>\\<^sub>\ \ p_id" definition ii_unit :: "('a,'a) mrel" ("1\<^sub>\\<^sub>\") where "1\<^sub>\\<^sub>\ \ { (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\<^sub>\\<^sub>\ = 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\<^sub>\\<^sub>\ = 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\<^sub>\\<^sub>\ = 1\<^sub>\\<^sub>\" unfolding ii_unit_def p_id_def inner_complement_def by force lemma ic_ii_unit [simp]: "\1\<^sub>\\<^sub>\ = 1\<^sub>\\<^sub>\" by (metis ic_involutive ic_iu_unit) lemma ii_unit_split_iu [simp]: "1 \\ \1 = 1\<^sub>\\<^sub>\" 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\<^sub>\\<^sub>\" 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 = (\i\I . f i) \ (\i\I . (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 = (\i\I . f i) \ (\i\I . (a,f i) \ X i) }" declare inner_Union_def [mr_simp] inner_Intersection_def [mr_simp] lemma iU_empty: "\\X|{} = 1\<^sub>\\<^sub>\" by (auto simp: mr_simp) lemma iI_empty: "\\X|{} = 1\<^sub>\\<^sub>\" 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 = (\R\X . R \\ T)" by (clarsimp simp: mr_simp) blast lemma ii_right_dist_oU: "\X \\ T = (\R\X . 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 "\b\B . \g . f b = \(g ` I) \ (\i\I . (b,g i) \ X i)" from this obtain g where 2: "\b\B . f b = \(g b ` I) \ (\i\I . (b,g b i) \ X i)" by metis hence 3: "\(f ` B) = (\b\B . \(g b ` I))" by (meson SUP_cong) let ?h = "\i . \b\B . g b i" have "\(f ` B) = \(?h ` I) \ (\i\I . \B . (a,B) \ R \ (\f . (\b\B . (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 "\i\I . \B . (a,B) \ X i \ (\g . (\b\B . (b,g b) \ R) \ f i = \(g ` B))" from this obtain B g where 1: "\i\I . (a,B i) \ X i \ (\b\B 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 . i\I \ b \ B i }" have "\b\?B . (b,?g b) \ R" proof (rule ballI) fix b let ?I = "{ i | i . i\I \ 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) \ (\i\I . (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) \ (\i\I . (a,f i) \ X i)) \ (\g . (\b\B . (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" ("_\<^sup>d" [100] 100) where "R\<^sup>d \ \-R" lemma dual: "R\<^sup>d = { (a,B) . (a,-B) \ R }" by (simp add: inner_complement_def) declare dual [mr_simp] lemma dual_antitone: "R \ S \ S\<^sup>d \ R\<^sup>d" by (simp add: ic_isotone) lemma ic_oc_dual: "\R = -R\<^sup>d" by (simp add: ic_dist_oc) lemma dual_involutive [simp]: "R\<^sup>d\<^sup>d = R" by (simp add: ic_dist_oc) lemma dual_antidist_ou: "(R \ S)\<^sup>d = R\<^sup>d \ S\<^sup>d" by (simp add: ic_dist_oi) lemma dual_antidist_oi: "(R \ S)\<^sup>d = R\<^sup>d \ S\<^sup>d" by (simp add: ic_dist_ou) lemma dual_dist_oc: "(-R)\<^sup>d = -R\<^sup>d" by (fact ic_dist_oc) lemma dual_dist_ic: "(\R)\<^sup>d = \R\<^sup>d" by (simp add: ic_dist_oc) lemma dual_antidist_oU: "(\X)\<^sup>d = \(dual ` X)" by (simp add: ic_dist_oI uminus_Sup) lemma dual_antidist_oI: "(\X)\<^sup>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\<^sub>\\<^sub>\ \ R = 1\<^sub>\\<^sub>\" by (simp add: co_prod) lemma cp_right_ii_unit: "R \ 1\<^sub>\\<^sub>\ \ R \\ \R" apply (clarsimp simp: mr_simp) by (metis double_compl sup_compl_top) lemma sp_right_iu_unit: "R * 1\<^sub>\\<^sub>\ \ 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 = (\R\X . 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 "\\<^sub>\\<^sub>\" 50) where "x \\<^sub>\\<^sub>\ y \ fst x = fst y \ snd x \ snd y" definition inner_order_ii :: "'a \ 'b set \ 'a \ 'b set \ bool" (infix "\\<^sub>\\<^sub>\" 50) where "x \\<^sub>\\<^sub>\ y \ fst x = fst y \ snd x \ snd y" lemma inner_order_dual: "x \\<^sub>\\<^sub>\ y \ y \\<^sub>\\<^sub>\ x" by (metis inner_order_ii_def inner_order_iu_def) interpretation inner_order_iu: order "(\\<^sub>\\<^sub>\)" "\x y . x \\<^sub>\\<^sub>\ 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\<^sub>\\<^sub>\ \ 1)" proof - have "\a B . (\C . (\D . B = C \ D) \ (a,C) \ R) \ (\C . (a,C) \ R \ (\f . (\c\C . f c = {} \ f c = {c}) \ B = (\c\C . 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 "(\c\C . ?f c) = (\c\B . ?f c) \ (\c\C\-B . ?f c)" using 1 by blast hence 3: "B = (\c\C . ?f c)" by auto have "\c\C . ?f c = {} \ ?f c = {c}" by auto thus "\C . (a,C) \ R \ (\f . (\c\C . f c = {} \ f c = {c}) \ B = (\c\C . f c))" using 2 3 by smt next fix a B assume "\C . (a,C) \ R \ (\f . (\c\C . f c = {} \ f c = {c}) \ B = (\c\C . f c))" from this obtain C where 4: "(a,C) \ R" and "\f . (\c\C . f c = {} \ f c = {c}) \ B = (\c\C . 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\<^sub>\\<^sub>\ \ \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 \ \b\B . \C . (\D . f b = C \ D) \ (b,C) \ S \ \E . (\F . (\b\B . f b) = E \ F) \ (\B . (a,B) \ R \ (\g . (\b\B . (b,g b) \ S) \ E = (\b\B . g b)))" proof - fix a B f assume 1: "(a,B) \ R" assume "\b\B . \C . (\D . f b = C \ D) \ (b,C) \ S" hence "\g . \b\B . (\D . f b = g b \ D) \ (b,g b) \ S" by metis from this obtain g where 2: "\b\B . (\D . f b = g b \ D) \ (b,g b) \ S" by auto hence "(\b\B . f b) \ (\b\B . g b)" by blast thus "\E . (\F . (\b\B . f b) = E \ F) \ (\B . (a,B) \ R \ (\g . (\b\B . (b,g b) \ S) \ E = (\b\B . 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\<^sub>\\<^sub>\ = (R \ S\) * 1\<^sub>\\<^sub>\" 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 "\i\I . \B . (\C . f i = B \ C) \ (a,B) \ X i" from this obtain g where "\i\I . (\C . f i = g i \ C) \ (a,g i) \ X i" by metis hence "(\C . \(f ` I) = \(g ` I) \ C) \ (\(g ` I) = \(g ` I) \ (\i\I . (a,g i) \ X i))" by auto thus "\B . (\C . \(f ` I) = B \ C) \ (\f . B = \(f ` I) \ (\i\I . (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 "\i\I . \B . (\C . f i = B \ C) \ (a,B) \ X i" from this obtain g where "\i\I . (\C . f i = g i \ C) \ (a,g i) \ X i" by metis hence "(\C . \(f ` I) = \(g ` I) \ C) \ (\(g ` I) = \(g ` I) \ (\i\I . (a,g i) \ X i))" by auto thus "\B . (\C . \(f ` I) = B \ C) \ (\f . B = \(f ` I) \ (\i\I . (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 "\i\I . \B . (\C . f i = B \ C) \ (a,B) \ X i" from this obtain g where "\i\I . (\C . f i = g i \ C) \ (a,g i) \ X i" by metis hence "(\C . \(f ` I) = \(g ` I) \ C) \ (\(g ` I) = \(g ` I) \ (\i\I . (a,g i) \ X i))" by auto thus "\B . (\C . \(f ` I) = B \ C) \ (\f . B = \(f ` I) \ (\i\I . (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 "\i\I . \B . (\C . f i = B \ C) \ (a,B) \ X i" from this obtain g where "\i\I . (\C . f i = g i \ C) \ (a,g i) \ X i" by metis hence "(\C . \(f ` I) = \(g ` I) \ C) \ (\(g ` I) = \(g ` I) \ (\i\I . (a,g i) \ X i))" by auto thus "\B . (\C . \(f ` I) = B \ C) \ (\f . B = \(f ` I) \ (\i\I . (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 "\i\I . \B . (\C . D = B \ C) \ (a,B) \ X i" from this obtain f where 1: "\i\I . (\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\<^sub>\\<^sub>\\ = U" by (simp add: iu_commute) lemma iu_unit_down: "1\<^sub>\\<^sub>\\ = 1\<^sub>\\<^sub>\" by (simp add: down_sp) lemma iu_unit_convex: "1\<^sub>\\<^sub>\\ = 1\<^sub>\\<^sub>\" by (simp add: iu_unit_down p_id_zero) lemma ii_unit_up: "1\<^sub>\\<^sub>\\ = 1\<^sub>\\<^sub>\" by (simp add: up_cp) lemma ii_unit_down: "1\<^sub>\\<^sub>\\ = U" using ii_commute ii_unit by blast lemma ii_unit_convex: "1\<^sub>\\<^sub>\\ = 1\<^sub>\\<^sub>\" using down_increasing ii_unit_up by blast lemma sp_unit_down: "1\ = 1 \ 1\<^sub>\\<^sub>\" 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: "(\R\X . R\)\ = (\R\X . 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\<^sub>\\<^sub>\ \\ R" using lower_ii_decreasing sp_right_iu_unit by blast lemma cp_ii_unit_upper: "R \\ R \ 1\<^sub>\\<^sub>\" 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\<^sup>\" 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\<^sub>\\<^sub>\ = R * 1\<^sub>\\<^sub>\" by (metis total_dom U_c cd_iso dc dc_prop2) lemma domain_pointwise: "x \ R * 1\<^sub>\\<^sub>\ \ (\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\<^sub>\\<^sub>\ = S * 1\<^sub>\\<^sub>\ \ S \ R \ S = R)" proof assume 1: "\S . R * 1\<^sub>\\<^sub>\ = S * 1\<^sub>\\<^sub>\ \ 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\<^sub>\\<^sub>\ = ?S * 1\<^sub>\\<^sub>\" proof show "R * 1\<^sub>\\<^sub>\ \ ?S * 1\<^sub>\\<^sub>\" proof fix x::"'a \ 'f set" assume "x \ R * 1\<^sub>\\<^sub>\" from this obtain b D where "(b,D) \ R \ x = (b,{})" by (meson domain_pointwise) thus "x \ ?S * 1\<^sub>\\<^sub>\" using 2 3 by (metis domain_pointwise Pair_inject insertE insert_Diff) qed next show "?S * 1\<^sub>\\<^sub>\ \ R * 1\<^sub>\\<^sub>\" 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\<^sub>\\<^sub>\ = S * 1\<^sub>\\<^sub>\ \ S \ R \ S = R" proof fix S show "R * 1\<^sub>\\<^sub>\ = S * 1\<^sub>\\<^sub>\ \ S \ R \ S = R" proof assume 6: "R * 1\<^sub>\\<^sub>\ = S * 1\<^sub>\\<^sub>\ \ 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\<^sub>\\<^sub>\ \ R * 1\<^sub>\\<^sub>\" 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\<^sub>\\<^sub>\ \\ R" unfolding lower_less_eq by (simp add: p_id_def total_set) lemma total_upper: "total R \ R \\ 1\<^sub>\\<^sub>\" 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\<^sub>\\<^sub>\ \ 1) * T)" by (simp add: down_sp s_prod_assoc1) also have "... = R * (1\<^sub>\\<^sub>\ \ T * 1)" by (simp add: s_prod_distr) also have "... = R * (T * 1\<^sub>\\<^sub>\ \ T * 1)" by (metis assms c6 order_antisym_conv total_4) also have "... \ R * (T * (1\<^sub>\\<^sub>\ \ 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\<^sub>\\<^sub>\)" by (metis Lambda_empty det_lambda) lemma ii_unit_deterministic: "deterministic (1\<^sub>\\<^sub>\)" 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: "(\R\X . R\) =\ \X" by (metis down_dist_oU lower_eq_down_closed) lemma oI_down_lower_eq_iI: "(\i\I . 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: "(\R\X . R\) =\ \X" by (metis up_dist_oU upper_eq_up_closed) lemma oI_up_upper_eq_iI: "(\i\I . 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 "\R\X . R\ = R" shows "(\X)\ = \X" by (meson Inter_iff assms ucl_iff) lemma oI_down_closed: assumes "\R\X . 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 "\R\X . 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\<^sub>\\<^sub>\ = 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\<^sub>\\<^sub>\ = 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 "\R\X . 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 "\R\X . 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 "\R\X . 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 "\R\X . 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\<^sub>\\<^sub>\") where "A\<^sub>\\<^sub>\ \ { (a,{b}) | a b . True }" definition co_atoms :: "('a,'b) mrel" ("A\<^sub>\\<^sub>\") where "A\<^sub>\\<^sub>\ \ { (a,UNIV - {b}) | a b . True }" declare atoms_def [mr_simp] co_atoms_def [mr_simp] lemma atoms_solution: "A\<^sub>\\<^sub>\\ = -1\<^sub>\\<^sub>\" 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\<^sub>\\<^sub>\" shows "A\<^sub>\\<^sub>\ \ R" proof fix x :: "'a \ 'b set" assume 1: "x \ A\<^sub>\\<^sub>\" 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\<^sub>\\<^sub>\ = A\<^sub>\\<^sub>\" apply (clarsimp simp: mr_simp) by fastforce lemma ic_co_atoms: "\A\<^sub>\\<^sub>\ = A\<^sub>\\<^sub>\" by (metis ic_atoms ic_involutive) lemma co_atoms_solution: "A\<^sub>\\<^sub>\\ = -1\<^sub>\\<^sub>\" by (metis atoms_solution ic_atoms ic_dist_oc ic_iu_unit ic_up) lemma co_atoms_least_solution: assumes "R\ = -1\<^sub>\\<^sub>\" shows "A\<^sub>\\<^sub>\ \ 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\<^sub>\\<^sub>\ \ A\<^sub>\\<^sub>\ = {}" by (metis Compl_disjoint atoms_solution iu_unit_down oi_down_up_iff) lemma ii_unit_co_atoms_disjoint: "1\<^sub>\\<^sub>\ \ A\<^sub>\\<^sub>\ = {}" using co_atoms_solution lower_reflexive by fastforce lemma atoms_sp_idempotent: "A\<^sub>\\<^sub>\ * A\<^sub>\\<^sub>\ = A\<^sub>\\<^sub>\" by (auto simp: mr_simp) lemma atoms_sp_cp: "(R \ A\<^sub>\\<^sub>\) * S = (R \ A\<^sub>\\<^sub>\) \ S" by (auto simp: mr_simp) subsection \Inner-functional properties\ abbreviation inner_univalent :: "('a,'b) mrel \ bool" where "inner_univalent R \ R \ 1\<^sub>\\<^sub>\ \ A\<^sub>\\<^sub>\" abbreviation inner_total :: "('a,'b) mrel \ bool" where "inner_total R \ R \ -1\<^sub>\\<^sub>\" 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\<^sub>\\<^sub>\" 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\<^sub>\\<^sub>\" 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\<^sub>\\<^sub>\)\)" proof show "(fus R)\ \ -((-(R\) \ A\<^sub>\\<^sub>\)\)" apply (clarsimp simp: mr_simp) by blast next show "-((-(R\) \ A\<^sub>\\<^sub>\)\) \ (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\<^sub>\\<^sub>\)\)" proof show "(fus R)\ \ -((\(R\) \ A\<^sub>\\<^sub>\)\)" apply (clarsimp simp: mr_simp) by blast next show "-((\(R\) \ A\<^sub>\\<^sub>\)\) \ (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\<^sub>\\<^sub>\) * \1)\)" by (simp add: atoms_sp_cp co_prod fusion_up_char ic_atoms ic_dist_oi) lemma fusion_char: "fus R = -((-(R\) \ A\<^sub>\\<^sub>\)\) \ -((\(R\) \ A\<^sub>\\<^sub>\)\)" by (metis deterministic_def fusion_deterministic fusion_down_char fusion_up_char inf_commute univalent_convex) lemma fusion_char_2: "fus R = -((-(R\) \ A\<^sub>\\<^sub>\)\) \ -(((R\ \ A\<^sub>\\<^sub>\) * \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\<^sub>\\<^sub>\" 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\<^sub>\\<^sub>\" 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 "\b\B . \C . f b = insert b C" hence "B \ (\x\B . f x)" by blast thus "\D . (\C . (\x\B . 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: "\b\C\D . (b,f b) \ S" and 3: "f x \ {}" and 4: "x \ C" and 5: "x \ D" let ?B = "{ b\C\D . 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 "(\x\C\D . f x) = (\x\?B . f x)" by auto thus "\B . (\C . (\D . B = C \ D) \ (a,C) \ R) \ B \ {} \ (\g . (\b\B . (b,g b) \ S \ g b \ {}) \ (\x\C\D . f x) = (\x\B . 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\<^sub>\\<^sub>\" 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\<^sub>\\<^sub>\" 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\<^sub>\\<^sub>\) = {}" 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\<^sub>\\<^sub>\)\)" proof show "(\\R)\ \ -((-(R\) \ A\<^sub>\\<^sub>\)\)" apply (clarsimp simp: mr_simp) by blast next show "-((-(R\) \ A\<^sub>\\<^sub>\)\) \ (\\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\<^sub>\\<^sub>\)\)" proof show "(\\R)\ \ -((\(R\) \ A\<^sub>\\<^sub>\)\)" apply (clarsimp simp: mr_simp) by blast next show "-((\(R\) \ A\<^sub>\\<^sub>\)\) \ (\\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\<^sub>\\<^sub>\) \ \1)\)" by (metis co_fusion_down_char ic_co_atoms ic_cp_ic_unit ic_dist_oi) lemma co_fusion_char: "\\R = -((-(R\) \ A\<^sub>\\<^sub>\)\) \ -((\(R\) \ A\<^sub>\\<^sub>\)\)" 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\<^sub>\\<^sub>\)\) \ -(((R\ \ A\<^sub>\\<^sub>\) \ \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\<^sub>\\<^sub>\ _" [80] 80) where "at\<^sub>\\<^sub>\ R \ R\ \ A\<^sub>\\<^sub>\" lemma co_fission: "at\<^sub>\\<^sub>\ 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\<^sub>\\<^sub>\ R" by (fact semilattice_inf_class.inf_le1) lemma co_fission_ic_inner_deterministic: "inner_deterministic (\at\<^sub>\\<^sub>\ 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\<^sub>\\<^sub>\ 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\<^sub>\\<^sub>\ 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\<^sub>\\<^sub>\ R \\ at\<^sub>\\<^sub>\ S" by (simp add: oi_subset_upper_left_antitone upper_transitive) lemma co_fission_idempotent: "at\<^sub>\\<^sub>\ (at\<^sub>\\<^sub>\ R) = at\<^sub>\\<^sub>\ 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\<^sub>\\<^sub>\ U = A\<^sub>\\<^sub>\" using top_lower_greatest U_par_idem top_down by blast lemma co_fission_up: "at\<^sub>\\<^sub>\ R = at\<^sub>\\<^sub>\ (R\)" by simp lemma co_fission_ic_inner_deterministic_fixpoint: "inner_deterministic (\R) \ R = at\<^sub>\\<^sub>\ 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\<^sub>\\<^sub>\ 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\<^sub>\\<^sub>\ (\\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\<^sub>\\<^sub>\ 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\<^sub>\\<^sub>\ (\\R) = at\<^sub>\\<^sub>\ 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\<^sub>\\<^sub>\ 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\<^sub>\\<^sub>\ 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\<^sub>\ = 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\<^sub>\ = 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 \ (\b\B . (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) \ (\b\B . (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\<^sub>\\<^sub>\ * \ 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\<^sub>\\<^sub>\" 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\<^sub>\\<^sub>\ * \ 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\<^sub>\\<^sub>\ * \ 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 "\b\B . (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\<^sub>\\<^sub>\" 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\<^sub>\\<^sub>\" 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\<^sub>\\<^sub>\" 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\<^sub>\\<^sub>\" proof assume "R\ \ U * p" thus "R\ * \ p \ 1\<^sub>\\<^sub>\" using assms top_sp_test_shunt by blast next assume 1: "R\ * \ p \ 1\<^sub>\\<^sub>\" 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 "\b\B . (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\<^sub>\\<^sub>\ \ 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\<^sub>\\<^sub>\ \ R\ \ 1\<^sub>\\<^sub>\ \ (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\<^sub>\\<^sub>\ \ (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\<^sub>\\<^sub>\" 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\<^sub>\\<^sub>\ \ (\p q . p \ 1 \ q \ 1\<^sub>\\<^sub>\ \ t = p \ q)" by (meson subset_UnE sup.mono) lemma test_iu_test_sp_assoc_1: "t \ 1 \ 1\<^sub>\\<^sub>\ \ 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\<^sub>\\<^sub>\ \ R * (t * S) = (R * t) * S" proof - assume 1: "t \ 1\<^sub>\\<^sub>\" 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\<^sub>\\<^sub>\" 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 \ (\b\B . (b,f b) \ t * S) \ C = \{ f b | b . b\B }" by (simp add: mr_simp) blast hence "\b\B . \D . (b,D) \ t \ (\g . (\e\D . (e,g e) \ S) \ f b = \{ g e | e . e \ D })" by (simp add: mr_simp Setcompr_eq_image) hence "\Db . \b\B . (b,Db b) \ t \ (\g . (\e\Db b . (e,g e) \ S) \ f b = \{ g e | e . e \ Db b })" by (rule bchoice) from this obtain Db where 2: "\b\B . (b,Db b) \ t \ (\g . (\e\Db b . (e,g e) \ S) \ f b = \{ g e | e . e \ Db b })" by auto let ?D = "\{ Db b | b . b \ B }" have "\b\B . (b,Db b) \ t" using 2 by auto hence 3: "\b\B . 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\<^sub>\\<^sub>\ \ 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\<^sub>\\<^sub>\" 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 \ (\b\B . (b,f b) \ S * t) \ C = \{ f b | b . b\B }" by (clarsimp simp: mr_simp) blast hence "\b\B . \D . (b,D) \ S \ (\g . (\e\D . (e,g e) \ t) \ f b = \{ g e | e . e \ D })" by (clarsimp simp: mr_simp Setcompr_eq_image) hence "\Db . \b\B . (b,Db b) \ S \ (\g . (\e\Db b . (e,g e) \ t) \ f b = \{ g e | e . e \ Db b })" by (rule bchoice) from this obtain Db where 2: "\b\B . (b,Db b) \ S \ (\g . (\e\Db b . (e,g e) \ t) \ f b = \{ g e | e . e \ Db b })" by auto hence "\gb . \b\B . (\e\Db 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: "\b\B . (\e\Db 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: "\b\B . \e\Db 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 \ (\b\B . (b,f b) \ R * S) \ D = \{ f b | b . b\B }" by (simp add: mr_simp) blast have "(a,D) \ (t * R) * S" proof (cases "(a,B) \ 1\<^sub>\\<^sub>\") 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\<^sub>\\<^sub>\" 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 \ (\c\C . (c,g c) \ S) \ D = \{ g c | c . c\C }" 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\<^sub>\\<^sub>\ \ 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: "\p\X . test p \ test (\X)" by blast lemma test_oI_closed: "\p\X . test p \ test (\X)" by blast lemma sp_test_dist_oI: assumes "test p" and "X \ {}" shows "(\X) * p = (\R\X . R * p)" apply (rule antisym) apply (clarsimp simp: mr_simp) apply blast apply (clarsimp simp: mr_simp) subgoal for a C proof - assume 1: "\R\X . \B . (a,B) \ R \ (\f . (\b\B . (b,f b) \ p) \ C = \(f ` B))" have 2: "(\R\X . (a,C) \ R \ (\b\C . (b,{b}) \ p))" proof fix R assume "R \ X" from this obtain B where 3: "(a,B) \ R \ (\f . (\b\B . (b,f b) \ p) \ C = \(f ` B))" using 1 by force from this obtain f where 4: "\b\B . (b,f b) \ p" and 5: "C = \(f ` B)" by auto hence 6: "\b\B . 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 \ (\b\C . (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 "\i\I . 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: "\i\I . (a,f i) \ X i" hence "\i\I . f i = {a}" using assms(1) by (meson test) hence "\(f ` I) = \(f ` I) \ (\i\I . (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 "\i\I . 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\<^sub>\\<^sub>\) \\ 1) \ 1" by (simp add: d_def_expl) lemma ad_expl_2: "aDom (R::('a,'b) mrel) = -((R * (1\<^sub>\\<^sub>\::('b,'a) mrel))\) \ (1::('a,'a) mrel)" proof have "-((R * 1\<^sub>\\<^sub>\)\) \ 1 = -((R * 1\<^sub>\\<^sub>\) \\ U) \ 1" by simp also have "\ \ -((R * 1\<^sub>\\<^sub>\) \\ 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\<^sub>\\<^sub>\)\) \ 1 \ aDom R" using \\ ((R::('a::type \ 'b::type set) set) * 1\<^sub>\\<^sub>\)\ \ \ (R * 1\<^sub>\\<^sub>\ \\ 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\<^sub>\\<^sub>\::('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\<^sub>\\<^sub>\ \ R \ U * aDom (ne S)" proof - have "R\ * S \ 1\<^sub>\\<^sub>\ \ 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\<^sub>\\<^sub>\)\ = 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 . (\c\C . (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\<^sub>\\<^sub>\ \ S)" proof - have "R\ * S = R * (1\<^sub>\\<^sub>\ \ 1) * S" by (simp add: down_sp) also have "... = R * ((1\<^sub>\\<^sub>\ \ 1) * S)" by (simp add: test_iu_test_sp_assoc_3) also have "... = R * (1\<^sub>\\<^sub>\ \ 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\<^sub>\\<^sub>\ \ (1\<^sub>\\<^sub>\ \ 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\<^sub>\\<^sub>\ \ R)" using down_sp_sp by blast also have "... = (((U * p) \ R) \ 1) * 1\<^sub>\\<^sub>\ \ (((U * p) \ R) \ 1) * R" by (simp add: s_distl_test) also have "... \ 1\<^sub>\\<^sub>\ \ (((U * p) \ R) \ 1) * R" using c6 by auto also have "... \ 1\<^sub>\\<^sub>\ \ ((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\<^sub>\\<^sub>\ \ 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\<^sub>\\<^sub>\ \ \ p)" using down_sp_sp by blast also have "... = R * ((p \ q) * 1\<^sub>\\<^sub>\ \ (p \ q) * \ p)" by (smt (verit) assms inf.orderE s_distl_test test_assoc1 test_ou_closed) also have "... \ R * (1\<^sub>\\<^sub>\ \ (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) . (\b\B . (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 "\b\B . \g . f b = \(g ` I) \ (\i\I . (b,g i) \ X i)" from this obtain g where 3: "f a = \(g ` I) \ (\i\I . (a,g i) \ X i)" using 2 by auto have "\(f ` B) = \(g ` I) \ (\i\I . \B . (a,B) \ p \ (\f . (\b\B . (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: "\i\I . \B . (a,B) \ p \ (\g . (\b\B . (b,g b) \ X i) \ f i = \(g ` B))" have "(a,{a}) \ p \ (\g . (\b\{a} . \f . g b = \(f ` I) \ (\i\I . (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 "|R\p \ { (a,{a}) | a . \B . (a,B) \ R \ (\b\B . (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 \ (\b\B . (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 \ (\b\B . (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 \ (\b\B . (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 "|R\p = Dom (R * p)" proof show "|R\p \ Dom (R * p)" proof fix x assume "x \ |R\p" from this obtain a B where 1: "x = (a,{a}) \ (a,B) \ R \ (\b\B . (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) \ |R\p" 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 \ (\b\B . (b,f b) \ p) \ A = \{ f b | b . b \ B }" by (simp add: mr_simp) blast hence "\b\B . (b,{b}) \ p" using assms subid_aux2 by fastforce thus "x \ |R\p" 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 \ (\b\B . (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 \ (\b\B . (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 "\b\B . (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 \ (\b\B . (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 \ (\b\B . (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 "\b\B . (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 "|R\p = |R\\p" proof - have "|R\\p = 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 "... = |R\p" 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 "|R\p = \ |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 \ |R\p \ |S\p" by (metis adia d_isotone inf.absorb_iff1 sp_test_dist_oi) lemma adia_right_isotone: "test p \ test q \ p \ q \ |R\p \ |R\q" 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 "|R\p = |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 = |R\p" proof show "|R]p \ |R\p" proof fix x assume "x \ |R]p" from this obtain a where 1: "x = (a,{a}) \ (\B . (a,B) \ R \ (\b\B . (b,{b}) \ p))" using abox_def by force from assms(2) obtain B where "(a,B) \ R" by (meson deterministic_set) thus "x \ |R\p" using 1 adia_def by fastforce qed next show "|R\p \ |R]p" proof fix x assume "x \ |R\p" from this obtain a B where 2: "x = (a,{a}) \ (a,B) \ R \ (\b\B . (b,{b}) \ p)" by (smt adia_def mem_Collect_eq) have "\C . (a,C) \ R \ (\b\C . (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 "\b\C . (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 R\p" 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 R\p" 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 \ |R\1 = 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 * R\q = p * |R\q" 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\<^sub>\\<^sub>\)" by (auto simp: mr_simp) hence "fis (R * S) = fis (R * Dom S * (S \ aDom S * 1\<^sub>\\<^sub>\))" by (metis d_s_id_ax sp_test_sp_oi_right test_sp) also have "... = fis (R * Dom S) * fis (S \ aDom S * 1\<^sub>\\<^sub>\)" 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\<^sub>\\<^sub>\))" 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 ( |R\p )" 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) \ |R\p \ |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 \ |R\q" 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 "|R\p * |R](p \ q) \ |R\q" proof - have "p \ p \ q \ q" using assms(1) by blast hence "|R\p \ |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) \ |R\p \ |R\q" 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 \ |R\q \ |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 \ S\p = |R\p \ |S\p" 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 = ( |R\1 \ |S]p ) * ( |S\1 \ |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]|S\1 = { (a,{a}) | a . \B . (a,B) \ R \ (\b\B . \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 . (\b\B . (b,C) \ S) \ (\c\C . (c,{c}) \ p)) }" by (auto simp: abox_def) lemma sp_abox_set: "|R * S]p = { (a,{a}) | a . \B . (a,B) \ R \ (\C . (\f . (\b\B . (b,f b) \ S) \ C = \{ f b | b . b \ B }) \ (\c\C . (c,{c}) \ p)) }" apply (unfold abox_def s_prod_def) by blast lemma abox_sp_1: assumes "test p" shows "|R]|S\1 * |R * S]p \ |R]|S]p" proof - have "|R]|S\1 * |R * S]p = |R]|S\1 \ |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]|S\1 \ |R * S]p" from this obtain a where 1: "x = (a,{a}) \ x \ |R]|S\1 \ 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 \ (\b\B . \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 . (\b\B . (b,f b) \ S) \ C = \{ f b | b . b \ B }) \ (\c\C . (c,{c}) \ p))" using 1 by (smt sp_abox_set mem_Collect_eq old.prod.inject) have "\B . (a,B) \ R \ (\C . (\b\B . (b,C) \ S) \ (\c\C . (c,{c}) \ p))" proof (rule allI, rule impI) fix B assume 4: "(a,B) \ R" hence "\DD . \b\B . (b,DD b) \ S" using 2 by (auto intro: bchoice) from this obtain DD where 5: "\b\B . (b,DD b) \ S" by auto show "\C . (\b\B . (b,C) \ S) \ (\c\C . (c,{c}) \ p)" proof (rule allI, rule impI) fix C assume "\b\B . (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 . (\b\B . (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 "\c\C . (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]|S\1 \ |R]|S]p" proof - have "|R]|S\1 * |R * S]p \ |R]|S]p" by (auto simp: assms abox_sp_1) hence "|R]|S\1 \ |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]|S\1 * |R * S]p = |R]|S\1 * |R]|S]p" proof (rule antisym) have "|R * S]p \ |R]|S\1 \ |R]|S]p" by (simp add: abox_sp_4 assms) hence "|R]|S\1 \ |R * S]p \ |R]|S]p" by blast hence "|R]|S\1 \ |R * S]p \ |R]|S\1 \ |R]|S]p" by blast thus "|R]|S\1 * |R * S]p \ |R]|S\1 * |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]|S\1 * |R]|S]p \ |R]|S\1 * |R * S]p" by (simp add: abox_sp_3 assms s_prod_isor) qed lemma abox_sp_6: assumes "test p" shows "|R]|S\1 \ |R * S]p = |R]|S\1 \ |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) * S\p" proof - have "|Q * (R * S)\p = |Q\( |R\( |S\p))" by (metis (no_types, lifting) adia adia_test assms d_loc_ax inf.orderE test_assoc3) also have "\ = |(Q * R) * S\p" by (smt (verit, best) adia adia_test assms d_loc test_assoc3 test_double_complement) finally show "|Q * (R * S)\p = |(Q * R) * S\p" . 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 = (\p\X . |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 = (\R\X . |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 = (\R\X . |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: "|\X\p = (\R\X . |R\p)" apply (clarsimp simp: mr_simp) by blast lemma edia_left_dist_oU: "|\X\\p = (\R\X . |R\\p)" apply (clarsimp simp: mr_simp) by blast subsection \Goldblatt's axioms with star\ no_notation rtrancl ("(_\<^sup>*)" [1000] 999) notation star ("_\<^sup>*" [1000] 999) lemma star_induct_1: assumes "1 \ X" and "R * X \ X" shows "R\<^sup>* \ X" apply (unfold star_def) apply (rule lfp_lowerbound) by (simp add: assms) lemma star_induct: assumes "S \ 1 \ 1\<^sub>\\<^sub>\" and "S \ X" and "R * X \ X" shows "R\<^sup>* * S \ X" proof - have "R\<^sup>* \ 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\<^sup>*)" by (metis s_prod_idl s_prod_isol star_refl total_4) lemma star_down: "R\<^sup>*\ = (R\)\<^sup>* \ 1\<^sub>\\<^sub>\" proof have "R\<^sup>* * (1 \ 1\<^sub>\\<^sub>\) \ (R\)\<^sup>* \ 1\<^sub>\\<^sub>\" proof (rule star_induct) show "1 \ 1\<^sub>\\<^sub>\ \ 1 \ 1\<^sub>\\<^sub>\" by simp next show "1 \ 1\<^sub>\\<^sub>\ \ (R\)\<^sup>* \ 1\<^sub>\\<^sub>\" using star_refl by auto next have "ne (R * ((R\)\<^sup>* \ 1\<^sub>\\<^sub>\)) \ ne (R\ * ((R\)\<^sup>* \ 1\<^sub>\\<^sub>\))" by (simp add: down_sp_sp sup_commute) also have "... = ne (R\) * ne ((R\)\<^sup>* \ 1\<^sub>\\<^sub>\)" by (simp add: ne_dist_down_sp) also have "... = ne (R\) * ne ((R\)\<^sup>*)" by (metis down_idempotent down_sp_sp ne_dist_down_sp sup_commute) also have "... \ R\ * (R\)\<^sup>*" using sp_oi_subdist by blast also have "... \ (R\)\<^sup>*" using star_unfold_eq by blast finally show "R * ((R\)\<^sup>* \ 1\<^sub>\\<^sub>\) \ (R\)\<^sup>* \ 1\<^sub>\\<^sub>\" by blast qed thus "R\<^sup>*\ \ (R\)\<^sup>* \ 1\<^sub>\\<^sub>\" by (simp add: down_sp sup_commute) next have "(R\)\<^sup>* \ R\<^sup>*\" proof (rule star_induct_1) show "1 \ R\<^sup>*\" by (simp add: star_refl subset_lower) next show "R\ * R\<^sup>*\ \ R\<^sup>*\" 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\)\<^sup>* \ 1\<^sub>\\<^sub>\ \ R\<^sup>*\" using star_total total_lower by blast qed lemma ne_star_down: "ne (R\<^sup>*\) = ne ((R\)\<^sup>*)" by (simp add: ne_dist_ou star_down) lemma ne_down_star: "ne ((R\)\<^sup>*) = (ne (R\))\<^sup>*" proof have "(R\)\<^sup>* \ (ne (R\))\<^sup>* \ 1\<^sub>\\<^sub>\" proof (rule star_induct_1) show "1 \ (ne (R\))\<^sup>* \ 1\<^sub>\\<^sub>\" by (simp add: le_supI1 star_refl) next have "ne (R\ * ((ne (R\))\<^sup>* \ 1\<^sub>\\<^sub>\)) = ne (R\) * ne ((ne (R\))\<^sup>*)" by (metis down_idempotent down_sp_sp ne_dist_down_sp sup_commute) also have "... \ (ne (R\))\<^sup>*" by (metis (no_types, lifting) IntE UnCI inf.absorb_iff2 sp_oi_subdist star_unfold_eq subsetI) finally show "R\ * ((ne (R\))\<^sup>* \ 1\<^sub>\\<^sub>\) \ ((ne (R\))\<^sup>* \ 1\<^sub>\\<^sub>\)" by blast qed thus "ne ((R\)\<^sup>*) \ (ne (R\))\<^sup>*" 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\))\<^sup>* \ ne ((R\)\<^sup>*)" proof (rule star_induct_1) show "1 \ ne ((R\)\<^sup>*)" using star_refl test_ne by auto next show "ne (R\) * ne ((R\)\<^sup>*) \ ne ((R\)\<^sup>*)" by (metis IntE IntI UnCI ne_dist_down_sp star_unfold_eq subsetI) qed qed lemma abox_star_unfold: "test p \ |R\<^sup>*]p = p * |R]|R\<^sup>*]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\<^sub>\\<^sub>\" and "Q * S \ S * R" shows "Q\<^sup>* * S \ S * R\<^sup>*" proof (rule star_induct) show "S \ 1 \ 1\<^sub>\\<^sub>\" by (simp add: assms(1)) next show "S \ S * R\<^sup>*" by (metis s_prod_idr s_prod_isor star_refl) next have "Q * (S * R\<^sup>*) \ S * R * R\<^sup>*" by (metis (no_types, lifting) assms s_prod_distr subset_Un_eq test_iu_test_sp_assoc_3) thus "Q * (S * R\<^sup>*) \ S * R\<^sup>*" 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 "|R\p \ p \ |R\<^sup>*\p \ p" proof assume "|R\p \ 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\<^sup>* * p \ p * R\<^sup>*" by (simp add: assms le_supI1 star_sp_test_commute) hence "R\<^sup>* * p \ p * (R\<^sup>* * p)" by (metis assms inf.absorb_iff2 inf.orderE sp_oi_subdist test_assoc3 test_sp_idempotent) hence "\ p * (R\<^sup>* * p) = {}" by (meson assms subset_empty test_sp_shunting) hence "\ p * Dom (R\<^sup>* * p) = {}" using d_sp_strict by blast thus "|R\<^sup>*\p \ p" by (metis adia assms d_test empty_subsetI semilattice_inf_class.le_inf_iff sp_test test_sp_shunting) next assume "|R\<^sup>*\p \ p" thus "|R\p \ 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\<^sup>*]]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\<^sup>*]p" proof - have "p \ |ne (R\)]]p \ p \ |ne (R\<^sup>*\)]]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\<^sup>*\\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\<^sup>*]p" proof - have "q \ p \ q \ |R\<^sup>*]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 \ |R\q \ q" shows "|R\<^sup>*\p \ q" by (meson adia_right_isotone adia_star_induct assms order.trans sup.bounded_iff) lemma abox_segerberg: assumes "test p" shows "|R\<^sup>*](p \ |R]p) \ p \ |R\<^sup>*]p" proof - have "p * |R\<^sup>*](p \ |R]p) \ |R\<^sup>*]p" proof (rule abox_star_induct_1) show "test p" by (simp add: assms) next show "test (p * |R\<^sup>*](p \ |R]p))" by (simp add: abox_test assms test_galois_1) next have "p * |R\<^sup>*](p \ |R]p) = p * (p \ |R]p) * |R]|R\<^sup>*](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\<^sup>*](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\<^sup>*](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\<^sup>*](p \ |R]p) \ p * |R](p * |R\<^sup>*](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\<^sup>*]( |R\p \ p ) \ |R\<^sup>*\p \ p" proof - let ?q = "|R\<^sup>*]( |R\p \ p )" have "|R\<^sup>*\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 * ( |R\p \ p ) \ |R\p * ( |R\p \ 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) \ ( |R\p \ 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_id \ p_id) * R = R \ p_id" +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 "p\R\q \ 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)\<^sup>* * \ p" + +lemma hoare_skip: + assumes "test p" + shows "p\1\p" + by (simp add: assms sp_unit_abox) + +lemma hoare_cons: + assumes "test s" + and "r \ p" + and "q \ s" + and "p\R\q" + shows "r\R\s" + by (meson abox_right_isotone assms order_trans) + +lemma hoare_seq: + assumes "test q" + and "test r" + and "p\R\q" + and "q\S\r" + shows "p\R*S\r" +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)\R\r" + and "((\ p)*q)\S\r" + shows "q\if_then_else p R S\r" + 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)\R\q" + shows "q\while_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)\<^sup>*]q" + by (meson abox_star_induct assms(2)) + also have "... \ |(p*R)\<^sup>*](q \ p)" + by (simp add: abox_right_isotone assms(1,2)) + also have "... = |(p*R)\<^sup>*](\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)\<^sup>*]|\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 "p\R\q" + and "p\S\q" + shows "p\R \\ S\q" +proof - + have 1: "p \ |R\1 \ |S]q" + by (simp add: assms(3) le_supI2) + have "p \ |S\1 \ |R]q" + by (simp add: assms(2) le_supI2) + hence "p \ ( |R\1 \ |S]q) \ ( |S\1 \ |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.a\<^sub>1" 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\<^sub>\\<^sub>\ = R * (-(p * U) \ 1\<^sub>\\<^sub>\))" 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.a\<^sub>1" abbreviation "b_2 \ finite_2.a\<^sub>2" 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 \ |R\p = |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.a\<^sub>1" abbreviation "c_2 \ finite_3.a\<^sub>2" abbreviation "c_3 \ finite_3.a\<^sub>3" 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\<^sub>\\<^sub>\ \ S = 1\<^sub>\\<^sub>\)" 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