(* Title: Relational Characterisation of Paths Author: Walter Guttmann, Peter Hoefner Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz> Peter Hoefner <peter at hoefner-online.de> *) section ‹Relational Characterisation of Paths› text ‹ This theory provides the relation-algebraic characterisations of paths, as defined in Sections 3--5 of \<^cite>‹"BerghammerFurusawaGuttmannHoefner2020"›. › theory Paths imports More_Relation_Algebra begin context relation_algebra_tarski begin lemma path_concat_aux_0: assumes "is_vector v" and "v ≠ 0" and "w;v⇧^{T}≤ x" and "v;z ≤ y" shows "w;1;z ≤ x;y" proof - from tarski assms(1,2) have "1 = 1;v⇧^{T};v;1" by (metis conv_contrav conv_one eq_refl inf_absorb1 inf_top_left is_vector_def ra_2) hence "w;1;z = w;1;v⇧^{T};v;1;z" by (simp add: mult_isor mult_isol mult_assoc) also from assms(1) have "... = w;v⇧^{T};v;z" by (metis is_vector_def comp_assoc conv_contrav conv_one) also from assms(3) have "... ≤ x;v;z" by (simp add: mult_isor) also from assms(4) have "... ≤ x;y" by (simp add: mult_isol mult_assoc) finally show ?thesis . qed end (* context relation_algebra_tarski *) subsection ‹Consequences without the Tarski rule› context relation_algebra_rtc begin text ‹Definitions for path classifications› abbreviation connected where "connected x ≡ x;1;x ≤ x⇧^{⋆}+ x⇧^{T}⇧^{⋆}" abbreviation many_strongly_connected where "many_strongly_connected x ≡ x⇧^{⋆}= x⇧^{T}⇧^{⋆}" abbreviation one_strongly_connected where "one_strongly_connected x ≡ x⇧^{T};1;x⇧^{T}≤ x⇧^{⋆}" definition path where "path x ≡ connected x ∧ is_p_fun x ∧ is_inj x" abbreviation cycle where "cycle x ≡ path x ∧ many_strongly_connected x" abbreviation start_points where "start_points x ≡ x;1 ⋅ -(x⇧^{T};1)" abbreviation end_points where "end_points x ≡ x⇧^{T};1 ⋅ -(x;1)" abbreviation no_start_points where "no_start_points x ≡ x;1 ≤ x⇧^{T};1" abbreviation no_end_points where "no_end_points x ≡ x⇧^{T};1 ≤ x;1" abbreviation no_start_end_points where "no_start_end_points x ≡ x;1 = x⇧^{T};1" abbreviation has_start_points where "has_start_points x ≡ 1 = -(1;x);x;1" abbreviation has_end_points where "has_end_points x ≡ 1 = 1;x;-(x;1)" abbreviation has_start_end_points where "has_start_end_points x ≡ 1 = -(1;x);x;1 ⋅ 1;x;-(x;1)" abbreviation backward_terminating where "backward_terminating x ≡ x ≤ -(1;x);x;1" abbreviation forward_terminating where "forward_terminating x ≡ x ≤ 1;x;-(x;1)" abbreviation terminating where "terminating x ≡ x ≤ -(1;x);x;1 ⋅ 1;x;-(x;1)" abbreviation backward_finite where "backward_finite x ≡ x ≤ x⇧^{T}⇧^{⋆}+ -(1;x);x;1" abbreviation forward_finite where "forward_finite x ≡ x ≤ x⇧^{T}⇧^{⋆}+ 1;x;-(x;1)" abbreviation finite where "finite x ≡ x ≤ x⇧^{T}⇧^{⋆}+ (-(1;x);x;1 ⋅ 1;x;-(x;1))" abbreviation no_start_points_path where "no_start_points_path x ≡ path x ∧ no_start_points x" abbreviation no_end_points_path where "no_end_points_path x ≡ path x ∧ no_end_points x" abbreviation no_start_end_points_path where "no_start_end_points_path x ≡ path x ∧ no_start_end_points x" abbreviation has_start_points_path where "has_start_points_path x ≡ path x ∧ has_start_points x" abbreviation has_end_points_path where "has_end_points_path x ≡ path x ∧ has_end_points x" abbreviation has_start_end_points_path where "has_start_end_points_path x ≡ path x ∧ has_start_end_points x" abbreviation backward_terminating_path where "backward_terminating_path x ≡ path x ∧ backward_terminating x" abbreviation forward_terminating_path where "forward_terminating_path x ≡ path x ∧ forward_terminating x" abbreviation terminating_path where "terminating_path x ≡ path x ∧ terminating x" abbreviation backward_finite_path where "backward_finite_path x ≡ path x ∧ backward_finite x" abbreviation forward_finite_path where "forward_finite_path x ≡ path x ∧ forward_finite x" abbreviation finite_path where "finite_path x ≡ path x ∧ finite x" text ‹General properties› lemma reachability_from_z_in_y: assumes "x ≤ y⇧^{⋆};z" and "x ⋅ z = 0" shows "x ≤ y⇧^{+};z" by (metis assms conway.dagger_unfoldl_distr galois_1 galois_aux inf.orderE) lemma reachable_imp: assumes "point p" and "point q" and "p⇧^{⋆};q ≤ p⇧^{T}⇧^{⋆};p" shows "p ≤ p⇧^{⋆};q" by (metis assms conway.dagger_unfoldr_distr le_supE point_swap star_conv) text ‹Basic equivalences› lemma no_start_end_points_iff: "no_start_end_points x ⟷ no_start_points x ∧ no_end_points x" by fastforce lemma has_start_end_points_iff: "has_start_end_points x ⟷ has_start_points x ∧ has_end_points x" by (metis inf_eq_top_iff) lemma terminating_iff: "terminating x ⟷ backward_terminating x ∧ forward_terminating x" by simp lemma finite_iff: "finite x ⟷ backward_finite x ∧ forward_finite x" by (simp add: sup_inf_distrib1 inf.boundedI) lemma no_start_end_points_path_iff: "no_start_end_points_path x ⟷ no_start_points_path x ∧ no_end_points_path x" by fastforce lemma has_start_end_points_path_iff: "has_start_end_points_path x ⟷ has_start_points_path x ∧ has_end_points_path x" using has_start_end_points_iff by blast lemma terminating_path_iff: "terminating_path x ⟷ backward_terminating_path x ∧ forward_terminating_path x" by fastforce lemma finite_path_iff: "finite_path x ⟷ backward_finite_path x ∧ forward_finite_path x" using finite_iff by fastforce text ‹Closure under converse› lemma connected_conv: "connected x ⟷ connected (x⇧^{T})" by (metis comp_assoc conv_add conv_contrav conv_iso conv_one star_conv) lemma conv_many_strongly_connected: "many_strongly_connected x ⟷ many_strongly_connected (x⇧^{T})" by fastforce lemma conv_one_strongly_connected: "one_strongly_connected x ⟷ one_strongly_connected (x⇧^{T})" by (metis comp_assoc conv_contrav conv_iso conv_one star_conv) lemma conv_path: "path x ⟷ path (x⇧^{T})" using connected_conv inj_p_fun path_def by fastforce lemma conv_cycle: "cycle x ⟷ cycle (x⇧^{T})" using conv_path by fastforce lemma conv_no_start_points: "no_start_points x ⟷ no_end_points (x⇧^{T})" by simp lemma conv_no_start_end_points: "no_start_end_points x ⟷ no_start_end_points (x⇧^{T})" by fastforce lemma conv_has_start_points: "has_start_points x ⟷ has_end_points (x⇧^{T})" by (metis comp_assoc conv_compl conv_contrav conv_invol conv_one) lemma conv_has_start_end_points: "has_start_end_points x ⟷ has_start_end_points (x⇧^{T})" by (metis comp_assoc conv_compl conv_contrav conv_invol conv_one inf_eq_top_iff) lemma conv_backward_terminating: "backward_terminating x ⟷ forward_terminating (x⇧^{T})" by (metis comp_assoc conv_compl conv_contrav conv_iso conv_one) lemma conv_terminating: "terminating x ⟷ terminating (x⇧^{T})" apply (rule iffI) apply (metis conv_compl conv_contrav conv_one conv_times inf.commute le_iff_inf mult_assoc) by (metis conv_compl conv_contrav conv_invol conv_one conv_times inf.commute le_iff_inf mult_assoc) lemma conv_backward_finite: "backward_finite x ⟷ forward_finite (x⇧^{T})" by (metis comp_assoc conv_add conv_compl conv_contrav conv_iso conv_one star_conv) lemma conv_finite: "finite x ⟷ finite (x⇧^{T})" by (metis finite_iff conv_backward_finite conv_invol) lemma conv_no_start_points_path: "no_start_points_path x ⟷ no_end_points_path (x⇧^{T})" using conv_path by fastforce lemma conv_no_start_end_points_path: "no_start_end_points_path x ⟷ no_start_end_points_path (x⇧^{T})" using conv_path by fastforce lemma conv_has_start_points_path: "has_start_points_path x ⟷ has_end_points_path (x⇧^{T})" using conv_has_start_points conv_path by fastforce lemma conv_has_start_end_points_path: "has_start_end_points_path x ⟷ has_start_end_points_path (x⇧^{T})" using conv_has_start_end_points conv_path by fastforce lemma conv_backward_terminating_path: "backward_terminating_path x ⟷ forward_terminating_path (x⇧^{T})" using conv_backward_terminating conv_path by fastforce lemma conv_terminating_path: "terminating_path x ⟷ terminating_path (x⇧^{T})" using conv_path conv_terminating by fastforce lemma conv_backward_finite_path: "backward_finite_path x ⟷ forward_finite_path (x⇧^{T})" using conv_backward_finite conv_path by fastforce lemma conv_finite_path: "finite_path x ⟷ finite_path (x⇧^{T})" using conv_finite conv_path by blast text ‹Equivalences for ‹connected›› lemma connected_iff2: assumes "is_inj x" and "is_p_fun x" shows "connected x ⟷ x;1;x⇧^{T}≤ x⇧^{⋆}+ x⇧^{T}⇧^{⋆}" proof assume 1: "connected x" have "x;1;x⇧^{T}≤ x;1;x;x⇧^{T}" by (metis conv_invol modular_var_3 vector_meet_comp_x') also have "... ≤ (x⇧^{+}+ x⇧^{T}⇧^{⋆});x⇧^{T}" using 1 mult_isor star_star_plus by fastforce also have "... ≤ x⇧^{⋆};x;x⇧^{T}+ x⇧^{T}⇧^{⋆}" using join_isol star_slide_var by simp also from assms(1) have "... ≤ x⇧^{⋆}+ x⇧^{T}⇧^{⋆}" by (metis is_inj_def comp_assoc join_iso mult_1_right mult_isol) finally show "x;1;x⇧^{T}≤ x⇧^{⋆}+ x⇧^{T}⇧^{⋆}" . next assume 2: "x;1;x⇧^{T}≤ x⇧^{⋆}+ x⇧^{T}⇧^{⋆}" have "x;1;x ≤ x;1;x⇧^{T};x" by (simp add: modular_var_3 vector_meet_comp_x) also have "... ≤ (x⇧^{⋆}+ x⇧^{T}⇧^{+});x" using 2 by (metis mult_isor star_star_plus sup_commute) also have "... ≤ x⇧^{⋆}+ x⇧^{T}⇧^{⋆};x⇧^{T};x" using join_iso star_slide_var by simp also from assms(2) have "... ≤ x⇧^{⋆}+ x⇧^{T}⇧^{⋆}" by (metis comp_assoc is_p_fun_def join_isol mult_1_right mult_isol) finally show "connected x" . qed lemma connected_iff3: assumes "is_inj x" and "is_p_fun x" shows "connected x ⟷ x⇧^{T};1;x ≤ x⇧^{⋆}+ x⇧^{T}⇧^{⋆}" by (metis assms connected_conv connected_iff2 inj_p_fun p_fun_inj conv_invol add_commute) lemma connected_iff4: "connected x ⟷ x⇧^{T};1;x⇧^{T}≤ x⇧^{⋆}+ x⇧^{T}⇧^{⋆}" by (metis connected_conv conv_invol add_commute) lemma connected_iff5: "connected x ⟷ x⇧^{+};1;x⇧^{+}≤ x⇧^{⋆}+ x⇧^{T}⇧^{⋆}" using comp_assoc plus_top top_plus by fastforce lemma connected_iff6: assumes "is_inj x" and "is_p_fun x" shows "connected x ⟷ x⇧^{+};1;(x⇧^{+})⇧^{T}≤ x⇧^{⋆}+ x⇧^{T}⇧^{⋆}" using assms connected_iff2 comp_assoc plus_conv plus_top top_plus by fastforce lemma connected_iff7: assumes "is_inj x" and "is_p_fun x" shows "connected x ⟷ (x⇧^{+})⇧^{T};1;x⇧^{+}≤ x⇧^{⋆}+ x⇧^{T}⇧^{⋆}" by (metis assms connected_iff3 conv_contrav conv_invol conv_one top_plus vector_meet_comp_x) lemma connected_iff8: "connected x ⟷ (x⇧^{+})⇧^{T};1;(x⇧^{+})⇧^{T}≤ x⇧^{⋆}+ x⇧^{T}⇧^{⋆}" by (metis connected_iff4 comp_assoc conv_contrav conv_invol conv_one plus_conv star_conv top_plus) text ‹Equivalences and implications for ‹many_strongly_connected›› lemma many_strongly_connected_iff_1: "many_strongly_connected x ⟷ x⇧^{T}≤ x⇧^{⋆}" apply (rule iffI,simp) by (metis conv_invol conv_iso order.eq_iff star_conv star_invol star_iso) lemma many_strongly_connected_iff_2: "many_strongly_connected x ⟷ x⇧^{T}≤ x⇧^{+}" proof assume as: "many_strongly_connected x" hence "x⇧^{T}≤ x⇧^{⋆}⋅ (-(1') + x)" by (metis many_strongly_connected_iff_1 loop_backward_forward inf_greatest) also have "... ≤ (x⇧^{⋆}⋅ -(1')) + (x⇧^{⋆}⋅ x)" by (simp add: inf_sup_distrib1) also have "... ≤ x⇧^{+}" by (metis as order.eq_iff mult_1_right mult_isol star_ref sup.absorb1 conv_invol eq_refl galois_1 inf.absorb_iff1 inf.commute star_unfoldl_eq sup_mono many_strongly_connected_iff_1) finally show "x⇧^{T}≤ x⇧^{+}" . next show "x⇧^{T}≤ x⇧^{+}⟹ many_strongly_connected x" using order_trans star_1l many_strongly_connected_iff_1 by blast qed lemma many_strongly_connected_iff_3: "many_strongly_connected x ⟷ x ≤ x⇧^{T}⇧^{⋆}" by (metis conv_invol many_strongly_connected_iff_1) lemma many_strongly_connected_iff_4: "many_strongly_connected x ⟷ x ≤ x⇧^{T}⇧^{+}" by (metis conv_invol many_strongly_connected_iff_2) lemma many_strongly_connected_iff_5: "many_strongly_connected x ⟷ x⇧^{⋆};x⇧^{T}≤ x⇧^{+}" by (metis comp_assoc conv_contrav conway.dagger_unfoldr_distr star_conv star_denest_var_2 star_invol star_trans_eq star_unfoldl_eq sup.boundedE many_strongly_connected_iff_2) lemma many_strongly_connected_iff_6: "many_strongly_connected x ⟷ x⇧^{T};x⇧^{⋆}≤ x⇧^{+}" by (metis dual_order.trans star_1l star_conv star_inductl_star star_invol star_slide_var many_strongly_connected_iff_1 many_strongly_connected_iff_5) lemma many_strongly_connected_iff_7: "many_strongly_connected x ⟷ x⇧^{T}⇧^{+}= x⇧^{+}" by (metis order.antisym conv_invol star_slide_var star_unfoldl_eq many_strongly_connected_iff_5) lemma many_strongly_connected_iff_5_eq: "many_strongly_connected x ⟷ x⇧^{⋆};x⇧^{T}= x⇧^{+}" by (metis order.refl star_slide_var many_strongly_connected_iff_5 many_strongly_connected_iff_7) lemma many_strongly_connected_iff_6_eq: "many_strongly_connected x ⟷ x⇧^{T};x⇧^{⋆}= x⇧^{+}" using many_strongly_connected_iff_6 many_strongly_connected_iff_7 by force lemma many_strongly_connected_implies_no_start_end_points: assumes "many_strongly_connected x" shows "no_start_end_points x" by (metis assms conway.dagger_unfoldl_distr mult_assoc sup_top_left conv_invol many_strongly_connected_iff_7) lemma many_strongly_connected_implies_8: assumes "many_strongly_connected x" shows "x;x⇧^{T}≤ x⇧^{+}" by (simp add: assms mult_isol) lemma many_strongly_connected_implies_9: assumes "many_strongly_connected x" shows "x⇧^{T};x ≤ x⇧^{+}" by (metis assms eq_refl phl_cons1 star_ext star_slide_var) lemma many_strongly_connected_implies_10: assumes "many_strongly_connected x" shows "x;x⇧^{T};x⇧^{⋆}≤ x⇧^{+}" by (simp add: assms comp_assoc mult_isol) lemma many_strongly_connected_implies_10_eq: assumes "many_strongly_connected x" shows "x;x⇧^{T};x⇧^{⋆}= x⇧^{+}" proof (rule order.antisym) show "x;x⇧^{T};x⇧^{⋆}≤ x⇧^{+}" by (simp add: assms comp_assoc mult_isol) next have "x⇧^{+}≤ x;x⇧^{T};x;x⇧^{⋆}" using mult_isor x_leq_triple_x by blast thus "x⇧^{+}≤ x;x⇧^{T};x⇧^{⋆}" by (simp add: comp_assoc mult_isol order_trans) qed lemma many_strongly_connected_implies_11: assumes "many_strongly_connected x" shows "x⇧^{⋆};x⇧^{T};x ≤ x⇧^{+}" by (metis assms conv_contrav conv_iso mult_isol star_1l star_slide_var) lemma many_strongly_connected_implies_11_eq: assumes "many_strongly_connected x" shows "x⇧^{⋆};x⇧^{T};x = x⇧^{+}" by (metis assms comp_assoc conv_invol many_strongly_connected_iff_5_eq many_strongly_connected_implies_10_eq) lemma many_strongly_connected_implies_12: assumes "many_strongly_connected x" shows "x⇧^{⋆};x;x⇧^{T}≤ x⇧^{+}" by (metis assms comp_assoc mult_isol star_1l star_slide_var) lemma many_strongly_connected_implies_12_eq: assumes "many_strongly_connected x" shows "x⇧^{⋆};x;x⇧^{T}= x⇧^{+}" by (metis assms comp_assoc star_slide_var many_strongly_connected_implies_10_eq) lemma many_strongly_connected_implies_13: assumes "many_strongly_connected x" shows "x⇧^{T};x;x⇧^{⋆}≤ x⇧^{+}" by (metis assms star_slide_var many_strongly_connected_implies_11 mult.assoc) lemma many_strongly_connected_implies_13_eq: assumes "many_strongly_connected x" shows "x⇧^{T};x;x⇧^{⋆}= x⇧^{+}" by (metis assms conv_invol many_strongly_connected_iff_7 many_strongly_connected_implies_10_eq) lemma many_strongly_connected_iff_8: assumes "is_p_fun x" shows "many_strongly_connected x ⟷ x;x⇧^{T}≤ x⇧^{+}" apply (rule iffI) apply (simp add: mult_isol) apply (simp add: many_strongly_connected_iff_1) by (metis comp_assoc conv_invol dual_order.trans mult_isol x_leq_triple_x assms comp_assoc dual_order.trans is_p_fun_def order.refl prod_star_closure star_ref) lemma many_strongly_connected_iff_9: assumes "is_inj x" shows "many_strongly_connected x ⟷ x⇧^{T};x ≤ x⇧^{+}" by (metis assms conv_contrav conv_iso inj_p_fun star_conv star_slide_var many_strongly_connected_iff_1 many_strongly_connected_iff_8) lemma many_strongly_connected_iff_10: assumes "is_p_fun x" shows "many_strongly_connected x ⟷ x;x⇧^{T};x⇧^{⋆}≤ x⇧^{+}" apply (rule iffI) apply (simp add: comp_assoc mult_isol) by (metis assms mult_isol mult_oner order_trans star_ref many_strongly_connected_iff_8) lemma many_strongly_connected_iff_10_eq: assumes "is_p_fun x" shows "many_strongly_connected x ⟷ x;x⇧^{T};x⇧^{⋆}= x⇧^{+}" using assms many_strongly_connected_iff_10 many_strongly_connected_implies_10_eq by fastforce lemma many_strongly_connected_iff_11: assumes "is_inj x" shows "many_strongly_connected x ⟷ x⇧^{⋆};x⇧^{T};x ≤ x⇧^{+}" by (metis assms comp_assoc conv_contrav conv_iso inj_p_fun plus_conv star_conv many_strongly_connected_iff_10 many_strongly_connected_iff_2) lemma many_strongly_connected_iff_11_eq: assumes "is_inj x" shows "many_strongly_connected x ⟷ x⇧^{⋆};x⇧^{T};x = x⇧^{+}" using assms many_strongly_connected_iff_11 many_strongly_connected_implies_11_eq by fastforce lemma many_strongly_connected_iff_12: assumes "is_p_fun x" shows "many_strongly_connected x ⟷ x⇧^{⋆};x;x⇧^{T}≤ x⇧^{+}" by (metis assms dual_order.trans mult_double_iso mult_oner star_ref star_slide_var many_strongly_connected_iff_8 many_strongly_connected_implies_12) lemma many_strongly_connected_iff_12_eq: assumes "is_p_fun x" shows "many_strongly_connected x ⟷ x⇧^{⋆};x;x⇧^{T}= x⇧^{+}" using assms many_strongly_connected_iff_12 many_strongly_connected_implies_12_eq by fastforce lemma many_strongly_connected_iff_13: assumes "is_inj x" shows "many_strongly_connected x ⟷ x⇧^{T};x;x⇧^{⋆}≤ x⇧^{+}" by (metis assms comp_assoc conv_contrav conv_iso inj_p_fun star_conv star_slide_var many_strongly_connected_iff_1 many_strongly_connected_iff_12) lemma many_strongly_connected_iff_13_eq: assumes "is_inj x" shows "many_strongly_connected x ⟷ x⇧^{T};x;x⇧^{⋆}= x⇧^{+}" using assms many_strongly_connected_iff_13 many_strongly_connected_implies_13_eq by fastforce text ‹Equivalences and implications for ‹one_strongly_connected›› lemma one_strongly_connected_iff: "one_strongly_connected x ⟷ connected x ∧ many_strongly_connected x" apply (rule iffI) apply (metis top_greatest x_leq_triple_x mult_double_iso top_greatest dual_order.trans many_strongly_connected_iff_1 comp_assoc conv_contrav conv_invol conv_iso le_supI2 star_conv) by (metis comp_assoc conv_contrav conv_iso conv_one conway.dagger_denest star_conv star_invol star_sum_unfold star_trans_eq) lemma one_strongly_connected_iff_1: "one_strongly_connected x ⟷ x⇧^{T};1;x⇧^{T}≤ x⇧^{+}" proof assume 1: "one_strongly_connected x" have "x⇧^{T};1;x⇧^{T}≤ x⇧^{T};x;x⇧^{T};1;x⇧^{T}" by (metis conv_invol mult_isor x_leq_triple_x) also from 1 have "... ≤ x⇧^{T};x;x⇧^{⋆}" by (metis distrib_left mult_assoc sup.absorb_iff1) also from 1 have "... ≤ x⇧^{+}" using many_strongly_connected_implies_13 one_strongly_connected_iff by blast finally show "x⇧^{T};1;x⇧^{T}≤ x⇧^{+}" . next assume "x⇧^{T};1;x⇧^{T}≤ x⇧^{+}" thus "one_strongly_connected x" using dual_order.trans star_1l by blast qed lemma one_strongly_connected_iff_1_eq: "one_strongly_connected x ⟷ x⇧^{T};1;x⇧^{T}= x⇧^{+}" apply (rule iffI, simp_all) by (metis comp_assoc conv_contrav conv_invol mult_double_iso plus_conv star_slide_var top_greatest top_plus many_strongly_connected_implies_10_eq one_strongly_connected_iff order.eq_iff one_strongly_connected_iff_1) lemma one_strongly_connected_iff_2: "one_strongly_connected x ⟷ x;1;x ≤ x⇧^{T}⇧^{⋆}" by (metis conv_invol eq_refl less_eq_def one_strongly_connected_iff) lemma one_strongly_connected_iff_3: "one_strongly_connected x ⟷ x;1;x ≤ x⇧^{T}⇧^{+}" by (metis comp_assoc conv_contrav conv_invol conv_iso conv_one star_conv one_strongly_connected_iff_1) lemma one_strongly_connected_iff_3_eq: "one_strongly_connected x ⟷ x;1;x = x⇧^{T}⇧^{+}" by (metis conv_invol one_strongly_connected_iff_1_eq one_strongly_connected_iff_2) lemma one_strongly_connected_iff_4_eq: "one_strongly_connected x ⟷ x⇧^{T};1;x = x⇧^{+}" apply (rule iffI) apply (metis comp_assoc top_plus many_strongly_connected_iff_7 one_strongly_connected_iff one_strongly_connected_iff_1_eq) by (metis comp_assoc conv_contrav conv_invol conv_one plus_conv top_plus one_strongly_connected_iff_1_eq) lemma one_strongly_connected_iff_5_eq: "one_strongly_connected x ⟷ x;1;x⇧^{T}= x⇧^{+}" using comp_assoc conv_contrav conv_invol conv_one plus_conv top_plus many_strongly_connected_iff_7 one_strongly_connected_iff one_strongly_connected_iff_3_eq by metis lemma one_strongly_connected_iff_6_aux: "x;x⇧^{+}≤ x;1;x" by (metis comp_assoc maddux_21 mult_isol top_plus) lemma one_strongly_connected_implies_6_eq: assumes "one_strongly_connected x" shows "x;1;x = x;x⇧^{+}" by (metis assms comp_assoc many_strongly_connected_iff_7 many_strongly_connected_implies_10_eq one_strongly_connected_iff one_strongly_connected_iff_3_eq) lemma one_strongly_connected_iff_7_aux: "x⇧^{+}≤ x;1;x" by (metis le_infI maddux_20 maddux_21 plus_top top_plus vector_meet_comp_x') lemma one_strongly_connected_implies_7_eq: assumes "one_strongly_connected x" shows "x;1;x = x⇧^{+}" using assms many_strongly_connected_iff_7 one_strongly_connected_iff one_strongly_connected_iff_3_eq by force lemma one_strongly_connected_implies_8: assumes "one_strongly_connected x" shows "x;1;x ≤ x⇧^{⋆}" using assms one_strongly_connected_iff by fastforce lemma one_strongly_connected_iff_4: assumes "is_inj x" shows "one_strongly_connected x ⟷ x⇧^{T};1;x ≤ x⇧^{+}" proof assume "one_strongly_connected x" thus "x⇧^{T};1;x ≤ x⇧^{+}" by (simp add: one_strongly_connected_iff_4_eq) next assume 1: "x⇧^{T};1;x ≤ x⇧^{+}" hence "x⇧^{T};1;x⇧^{T}≤ x⇧^{⋆};x;x⇧^{T}" by (metis mult_isor star_slide_var comp_assoc conv_invol modular_var_3 vector_meet_comp_x order.trans) also from assms have "... ≤ x⇧^{⋆}" using comp_assoc is_inj_def mult_isol mult_oner by fastforce finally show "one_strongly_connected x" using dual_order.trans star_1l by fastforce qed lemma one_strongly_connected_iff_5: assumes "is_p_fun x" shows "one_strongly_connected x ⟷ x;1;x⇧^{T}≤ x⇧^{+}" apply (rule iffI) using one_strongly_connected_iff_5_eq apply simp by (metis assms comp_assoc mult_double_iso order.trans star_slide_var top_greatest top_plus many_strongly_connected_iff_12 many_strongly_connected_iff_7 one_strongly_connected_iff_3) lemma one_strongly_connected_iff_6: assumes "is_p_fun x" and "is_inj x" shows "one_strongly_connected x ⟷ x;1;x ≤ x;x⇧^{+}" proof assume "one_strongly_connected x" thus "x;1;x ≤ x;x⇧^{+}" by (simp add: one_strongly_connected_implies_6_eq) next assume 1: "x;1;x ≤ x;x⇧^{+}" have "x⇧^{T};1;x ≤ x⇧^{T};x;x⇧^{T};1;x" by (metis conv_invol mult_isor x_leq_triple_x) also have "... ≤ x⇧^{T};x;1;x" by (metis comp_assoc mult_double_iso top_greatest) also from 1 have "... ≤ x⇧^{T};x;x⇧^{+}" by (simp add: comp_assoc mult_isol) also from assms(1) have "... ≤ x⇧^{+}" by (metis comp_assoc is_p_fun_def mult_isor mult_onel) finally show "one_strongly_connected x" using assms(2) one_strongly_connected_iff_4 by blast qed lemma one_strongly_connected_iff_6_eq: assumes "is_p_fun x" and "is_inj x" shows "one_strongly_connected x ⟷ x;1;x = x;x⇧^{+}" apply (rule iffI) using one_strongly_connected_implies_6_eq apply blast by (simp add: assms one_strongly_connected_iff_6) text ‹Start points and end points› lemma start_end_implies_terminating: assumes "has_start_points x" and "has_end_points x" shows "terminating x" using assms by simp lemma start_points_end_points_conv: "start_points x = end_points (x⇧^{T})" by simp lemma start_point_at_most_one: assumes "path x" shows "is_inj (start_points x)" proof - have isvec: "is_vector (x;1 ⋅ -(x⇧^{T};1))" by (simp add: comp_assoc is_vector_def one_compl vector_1) have "x;1 ⋅ 1;x⇧^{T}≤ x;1;x;x⇧^{T}" by (metis comp_assoc conv_contrav conv_one inf.cobounded2 mult_1_right mult_isol one_conv ra_2) also have "... ≤ (x⇧^{⋆}+ x⇧^{T}⇧^{⋆});x⇧^{T}" using ‹path x› by (metis path_def mult_isor) also have "... = x⇧^{T}+ x⇧^{+};x⇧^{T}+ x⇧^{T}⇧^{+}" by (simp add: star_slide_var) also have "... ≤ x⇧^{T}⇧^{+}+ x⇧^{+};x⇧^{T}+ x⇧^{T}⇧^{+}" by (metis add_iso mult_1_right star_unfoldl_eq subdistl) also have "... ≤ x⇧^{⋆};x;x⇧^{T}+ x⇧^{T}⇧^{+}" by (simp add: star_slide_var add_comm) also have "... ≤ x⇧^{⋆};1' + x⇧^{T}⇧^{+}" using ‹path x› by (metis path_def is_inj_def comp_assoc distrib_left join_iso less_eq_def) also have "... = 1' + x⇧^{⋆};x + x⇧^{T};x⇧^{T}⇧^{⋆}" by simp also have "... ≤ 1' + 1;x + x⇧^{T};1" by (metis join_isol mult_isol mult_isor sup.mono top_greatest) finally have aux: "x;1 ⋅ 1;x⇧^{T}≤ 1' + 1;x + x⇧^{T};1" . from aux have "x;1 ⋅ 1;x⇧^{T}⋅ -(x⇧^{T};1) ⋅ -(1;x) ≤ 1'" by (simp add: galois_1 sup_commute) hence "(x;1 ⋅ -(x⇧^{T};1)) ⋅ (x;1 ⋅ -(x⇧^{T};1))⇧^{T}≤ 1'" by (simp add: conv_compl inf.assoc inf.left_commute) with isvec have "(x;1 ⋅ -(x⇧^{T};1)) ; (x;1 ⋅ -(x⇧^{T};1))⇧^{T}≤ 1'" by (metis vector_meet_comp') thus "is_inj (start_points x)" by (simp add: conv_compl is_inj_def) qed lemma start_point_zero_point: assumes "path x" shows "start_points x = 0 ∨ is_point (start_points x)" using assms start_point_at_most_one comp_assoc is_point_def is_vector_def vector_compl vector_mult by simp lemma start_point_iff1: assumes "path x" shows "is_point (start_points x) ⟷ ¬(no_start_points x)" using assms start_point_zero_point galois_aux2 is_point_def by blast lemma end_point_at_most_one: assumes "path x" shows "is_inj (end_points x)" by (metis assms conv_path compl_bot_eq conv_invol inj_def_var1 is_point_def top_greatest start_point_zero_point) lemma end_point_zero_point: assumes "path x" shows "end_points x = 0 ∨ is_point (end_points x)" using assms conv_path start_point_zero_point by fastforce lemma end_point_iff1: assumes "path x" shows "is_point (end_points x) ⟷ ¬(no_end_points x)" using assms end_point_zero_point galois_aux2 is_point_def by blast lemma predecessor_point': assumes "path x" and "point s" and "point e" and "e;s⇧^{T}≤ x" shows "x;s = e" proof (rule order.antisym) show 1: "e ≤ x ; s" using assms(2,4) point_def ss423bij by blast show "x ; s ≤ e" proof - have "e⇧^{T}; (x ; s) = 1" using 1 by (metis assms(3) order.eq_iff is_vector_def point_def ss423conv top_greatest) thus ?thesis by (metis assms(1-3) comp_assoc conv_contrav conv_invol order.eq_iff inj_compose is_vector_def mult_isol path_def point_def ss423conv sur_def_var1 top_greatest) qed qed lemma predecessor_point: assumes "path x" and "point s" and "point e" and "e;s⇧^{T}≤ x" shows "point(x;s)" using predecessor_point' assms by blast lemma points_of_path_iff: shows "(x + x⇧^{T});1 = x⇧^{T};1 + start_points(x)" and "(x + x⇧^{T});1 = x;1 + end_points(x)" using aux9 inf.commute sup.commute by auto text ‹Path concatenation preliminaries› lemma path_concat_aux_1: assumes "x;1 ⋅ y;1 ⋅ y⇧^{T};1 = 0" and "end_points x = start_points y" shows "x;1 ⋅ y;1 = 0" proof - have "x;1 ⋅ y;1 = (x;1 ⋅ y;1 ⋅ y⇧^{T};1) + (x;1 ⋅ y;1 ⋅ -(y⇧^{T};1))" by simp also from assms(1) have "... = x;1 ⋅ y;1 ⋅ -(y⇧^{T};1)" by (metis aux6_var de_morgan_3 inf.left_commute inf_compl_bot inf_sup_absorb) also from assms(2) have "... = x;1 ⋅ x⇧^{T};1 ⋅ -(x;1)" by (simp add: inf.assoc) also have "... = 0" by (simp add: inf.commute inf.assoc) finally show ?thesis . qed lemma path_concat_aux_2: assumes "x;1 ⋅ x⇧^{T};1 ⋅ y⇧^{T};1 = 0" and "end_points x = start_points y" shows "x⇧^{T};1 ⋅ y⇧^{T};1 = 0" proof - have "y⇧^{T};1 ⋅ x⇧^{T};1 ⋅ (x⇧^{T})⇧^{T};1 = 0" using assms(1) inf.assoc inf.commute by force thus ?thesis by (metis assms(2) conv_invol inf.commute path_concat_aux_1) qed lemma path_concat_aux3_1: assumes "path x" shows "x;1;x⇧^{T}≤ x⇧^{⋆}+ x⇧^{T}⇧^{⋆}" proof - have "x;1;x⇧^{T}≤ x;1;x⇧^{T};x;x⇧^{T}" by (metis comp_assoc conv_invol mult_isol x_leq_triple_x) also have "... ≤ x;1;x;x⇧^{T}" by (metis mult_isol mult_isor mult_assoc top_greatest) also from assms have "... ≤ (x⇧^{⋆}+ x⇧^{T}⇧^{⋆});x⇧^{T}" using path_def comp_assoc mult_isor by blast also have "... = x⇧^{⋆};x;x⇧^{T}+ x⇧^{T}⇧^{⋆};x⇧^{T}" by (simp add: star_slide_var star_star_plus) also have "... ≤ x⇧^{⋆};1' + x⇧^{T}⇧^{⋆};x⇧^{T}" by (metis assms path_def is_inj_def join_iso mult_isol mult_assoc) also have "... ≤ x⇧^{⋆}+ x⇧^{T}⇧^{⋆}" using join_isol by simp finally show ?thesis . qed lemma path_concat_aux3_2: assumes "path x" shows "x⇧^{T};1;x ≤ x⇧^{⋆}+ x⇧^{T}⇧^{⋆}" proof - have "x⇧^{T};1;x ≤ x⇧^{T};x;x⇧^{T};1;x" by (metis comp_assoc conv_invol mult_isor x_leq_triple_x) also have "... ≤ x⇧^{T};x;1;x" by (metis mult_isol mult_isor mult_assoc top_greatest) also from assms have "... ≤ x⇧^{T};(x⇧^{⋆}+ x⇧^{T}⇧^{⋆})" by (simp add: comp_assoc mult_isol path_def) also have "... = x⇧^{T};x;x⇧^{⋆}+ x⇧^{T};x⇧^{T}⇧^{⋆}" by (simp add: comp_assoc distrib_left star_star_plus) also have "... ≤ 1';x⇧^{⋆}+ x⇧^{T};x⇧^{T}⇧^{⋆}" by (metis assms path_def is_p_fun_def join_iso mult_isor mult_assoc) also have "... ≤ x⇧^{⋆}+ x⇧^{T}⇧^{⋆}" using join_isol by simp finally show ?thesis . qed lemma path_concat_aux3_3: assumes "path x" shows "x⇧^{T};1;x⇧^{T}≤ x⇧^{⋆}+ x⇧^{T}⇧^{⋆}" proof - have "x⇧^{T};1;x⇧^{T}≤ x⇧^{T};x;x⇧^{T};1;x⇧^{T}" by (metis comp_assoc conv_invol mult_isor x_leq_triple_x) also have "... ≤ x⇧^{T};x;1;x⇧^{T}" by (metis mult_isol mult_isor mult_assoc top_greatest) also from assms have "... ≤ x⇧^{T};(x⇧^{⋆}+ x⇧^{T}⇧^{⋆})" using path_concat_aux3_1 by (simp add: mult_assoc mult_isol) also have "... = x⇧^{T};x;x⇧^{⋆}+ x⇧^{T};x⇧^{T}⇧^{⋆}" by (simp add: comp_assoc distrib_left star_star_plus) also have "... ≤ 1';x⇧^{⋆}+ x⇧^{T};x⇧^{T}⇧^{⋆}" by (metis assms path_def is_p_fun_def join_iso mult_isor mult_assoc) also have "... ≤ x⇧^{⋆}+ x⇧^{T}⇧^{⋆}" using join_isol by simp finally show ?thesis . qed lemma path_concat_aux_3: assumes "path x" and "y ≤ x⇧^{+}+ x⇧^{T}⇧^{+}" and "z ≤ x⇧^{+}+ x⇧^{T}⇧^{+}" shows "y;1;z ≤ x⇧^{⋆}+ x⇧^{T}⇧^{⋆}" proof - from assms(2,3) have "y;1;z ≤ (x⇧^{+}+ x⇧^{T}⇧^{+});1;(x⇧^{+}+ x⇧^{T}⇧^{+})" using mult_isol_var mult_isor by blast also have "... = x⇧^{+};1;x⇧^{+}+ x⇧^{+};1;x⇧^{T}⇧^{+}+ x⇧^{T}⇧^{+};1;x⇧^{+}+ x⇧^{T}⇧^{+};1;x⇧^{T}⇧^{+}" by (simp add: distrib_left sup_commute sup_left_commute) also have "... = x;x⇧^{⋆};1;x⇧^{⋆};x + x;x⇧^{⋆};1;x⇧^{T}⇧^{⋆};x⇧^{T}+ x⇧^{T};x⇧^{T}⇧^{⋆};1;x⇧^{⋆};x + x⇧^{T};x⇧^{T}⇧^{⋆};1;x⇧^{T}⇧^{⋆};x⇧^{T}" by (simp add: comp_assoc star_slide_var) also have "... ≤ x;1;x + x;x⇧^{⋆};1;x⇧^{T}⇧^{⋆};x⇧^{T}+ x⇧^{T};x⇧^{T}⇧^{⋆};1;x⇧^{⋆};x + x⇧^{T};x⇧^{T}⇧^{⋆};1;x⇧^{T}⇧^{⋆};x⇧^{T}" by (metis comp_assoc mult_double_iso top_greatest join_iso) also have "... ≤ x;1;x + x;1;x⇧^{T}+ x⇧^{T};x⇧^{T}⇧^{⋆};1;x⇧^{⋆};x + x⇧^{T};x⇧^{T}⇧^{⋆};1;x⇧^{T}⇧^{⋆};x⇧^{T}" by (metis comp_assoc mult_double_iso top_greatest join_iso join_isol) also have "... ≤ x;1;x + x;1;x⇧^{T}+ x⇧^{T};1;x + x⇧^{T};x⇧^{T}⇧^{⋆};1;x⇧^{T}⇧^{⋆};x⇧^{T}" by (metis comp_assoc mult_double_iso top_greatest join_iso join_isol) also have "... ≤ x;1;x + x;1;x⇧^{T}+ x⇧^{T};1;x + x⇧^{T};1;x⇧^{T}" by (metis comp_assoc mult_double_iso top_greatest join_isol) also have "... ≤ x⇧^{⋆}+ x⇧^{T}⇧^{⋆}" using assms(1) path_def path_concat_aux3_1 path_concat_aux3_2 path_concat_aux3_3 join_iso join_isol by simp finally show ?thesis . qed lemma path_concat_aux_4: "x⇧^{⋆}+ x⇧^{T}⇧^{⋆}≤ x⇧^{⋆}+ x⇧^{T};1" by (metis star_star_plus add_comm join_isol mult_isol top_greatest) lemma path_concat_aux_5: assumes "path x" and "y ≤ start_points x" and "z ≤ x + x⇧^{T}" shows "y;1;z ≤ x⇧^{⋆}" proof - from assms(1) have "x;1;x ≤ x⇧^{⋆}+ x⇧^{T};1" using path_def path_concat_aux_4 dual_order.trans by blast hence aux1: "x;1;x ⋅ -(x⇧^{T};1) ≤ x⇧^{⋆}" by (simp add: galois_1 sup_commute) from assms(1) have "x;1;x⇧^{T}≤ x⇧^{⋆}+ x⇧^{T};1" using dual_order.trans path_concat_aux3_1 path_concat_aux_4 by blast hence aux2: "x;1;x⇧^{T}⋅ -(x⇧^{T};1) ≤ x⇧^{⋆}" by (simp add: galois_1 sup_commute) from assms(2,3) have "y;1;z ≤ (x;1 ⋅ -(x⇧^{T};1));1;(x + x⇧^{T})" by (simp add: mult_isol_var mult_isor) also have "... = (x;1 ⋅ -(x⇧^{T};1));1;x + (x;1 ⋅ -(x⇧^{T};1));1;x⇧^{T}" using distrib_left by blast also have "... = (x;1 ⋅ -(x⇧^{T};1) ⋅ 1;x) + (x;1 ⋅ -(x⇧^{T};1));1;x⇧^{T}" by (metis comp_assoc inf_top_right is_vector_def one_idem_mult vector_1 vector_compl) also have "... = (x;1 ⋅ -(x⇧^{T};1) ⋅ 1;x) + (x;1 ⋅ -(x⇧^{T};1) ⋅ 1;x⇧^{T})" by (metis comp_assoc inf_top_right is_vector_def one_idem_mult vector_1 vector_compl) also have "... = (x;1;x ⋅ -(x⇧^{T};1)) + (x;1;x⇧^{T}-(x⇧^{T};1))" using vector_meet_comp_x vector_meet_comp_x' diff_eq inf.assoc inf.commute by simp also from aux1 aux2 have "... ≤ x⇧^{⋆}" by (simp add: diff_eq join_iso) finally show ?thesis . qed lemma path_conditions_disjoint_points_iff: "x;1 ⋅ (x⇧^{T};1 + y;1) ⋅ y⇧^{T};1 = 0 ∧ start_points x ⋅ end_points y = 0 ⟷ x;1 ⋅ y⇧^{T};1 = 0" proof assume 1: "x ; 1 ⋅ y⇧^{T}; 1 = 0" hence g1: "x ; 1 ⋅ (x⇧^{T}; 1 + y ; 1) ⋅ y⇧^{T}; 1 = 0" by (metis inf.left_commute inf_bot_right inf_commute) have g2: "start_points x ⋅ end_points y = 0" using 1 by (metis compl_inf_bot inf.assoc inf.commute inf.left_idem) show "x;1 ⋅ (x⇧^{T};1 + y;1) ⋅ y⇧^{T};1 = 0 ∧ start_points x ⋅ end_points y = 0" using g1 and g2 by simp next assume a: "x;1 ⋅ (x⇧^{T};1 + y;1) ⋅ y⇧^{T};1 = 0 ∧ start_points x ⋅ end_points y = 0" from a have a1: "x;1 ⋅ x⇧^{T};1 ⋅ y⇧^{T};1 = 0" by (simp add: inf.commute inf_sup_distrib1) from a have a2: "x;1 ⋅ y;1 ⋅ y⇧^{T};1 = 0" by (simp add: inf.commute inf_sup_distrib1) from a have a3: "start_points x ⋅ end_points y = 0" by blast have "x;1 ⋅ y⇧^{T};1 = x;1 ⋅ x⇧^{T};1 ⋅ y⇧^{T};1 + x;1 ⋅ -(x⇧^{T};1) ⋅ y⇧^{T};1" by (metis aux4 inf_sup_distrib2) also from a1 have "... = x;1 ⋅ -(x⇧^{T};1) ⋅ y⇧^{T};1" using sup_bot_left by blast also have "... = x;1 ⋅ -(x⇧^{T};1) ⋅ y;1 ⋅ y⇧^{T};1 + x;1 ⋅ -(x⇧^{T};1) ⋅ -(y;1) ⋅ y⇧^{T};1" by (metis aux4 inf_sup_distrib2) also have "... ≤ x;1 ⋅ y;1 ⋅ y⇧^{T};1 + x;1 ⋅ -(x⇧^{T};1) ⋅ -(y;1) ⋅ y⇧^{T};1" using join_iso meet_iso by simp also from a2 have "... = start_points x ⋅ end_points y" using sup_bot_left inf.commute inf.left_commute by simp also from a3 have "... = 0" by blast finally show "x;1 ⋅ y⇧^{T};1 = 0" using le_bot by blast qed end (* end relation_algebra_rtc *) subsection ‹Consequences with the Tarski rule› context relation_algebra_rtc_tarski begin text ‹General theorems› lemma reachable_implies_predecessor: assumes "p ≠ q" and "point p" and "point q" and "x⇧^{⋆};q ≤ x⇧^{T}⇧^{⋆};p" shows "x;q ≠ 0" proof assume contra: "x;q=0" with assms(4) have "q ≤ x⇧^{T}⇧^{⋆};p" by (simp add: independence1) hence "p ≤ x⇧^{⋆};q" by (metis assms(2,3) point_swap star_conv) with contra assms(2,3) have "p=q" by (simp add: independence1 is_point_def point_singleton point_is_point) with assms(1) show False by simp qed lemma acyclic_imp_one_step_different_points: assumes "is_acyclic x" and "point p" and "point q" and "p ≤ x;q" shows "p ≤ -q" and "p ≠ q" using acyclic_reachable_points assms point_is_point point_not_equal(1) by auto text ‹Start points and end points› lemma start_point_iff2: assumes "path x" shows "is_point (start_points x) ⟷ has_start_points x" proof - have "has_start_points x ⟷ 1 ≤ -(1;x);x;1" by (simp add: order.eq_iff) also have "... ⟷ 1 ≤ 1;x⇧^{T};-(x⇧^{T};1)" by (metis comp_assoc conv_compl conv_contrav conv_iso conv_one) also have "... ⟷ 1 ≤ 1;(x;1 ⋅ -(x⇧^{T};1))" by (metis (no_types) conv_contrav conv_one inf.commute is_vector_def one_idem_mult ra_2 vector_1 vector_meet_comp_x) also have "... ⟷ 1 = 1;(x;1 ⋅ -(x⇧^{T};1))" by (simp add: order.eq_iff) also have "... ⟷ x;1 ⋅ -(x⇧^{T};1) ≠ 0" by (metis tarski comp_assoc one_compl ra_1 ss_p18) also have "... ⟷ is_point (start_points x)" using assms is_point_def start_point_zero_point by blast finally show ?thesis .. qed lemma end_point_iff2: assumes "path x" shows "is_point (end_points x) ⟷ has_end_points x" by (metis assms conv_invol conv_has_start_points conv_path start_point_iff2) lemma edge_is_path: assumes "is_point p" and "is_point q" shows "path (p;q⇧^{T})" apply (unfold path_def; intro conjI) apply (metis assms comp_assoc is_point_def le_supI1 star_ext vector_rectangle point_equations(3)) apply (metis is_p_fun_def assms comp_assoc conv_contrav conv_invol is_inj_def is_point_def vector_2_var vector_meet_comp_x' point_equations) by (metis is_inj_def assms conv_invol conv_times is_point_def p_fun_mult_var vector_meet_comp) lemma edge_start: assumes "is_point p" and "is_point q" and "p ≠ q" shows "start_points (p;q⇧^{T}) = p" using assms by (simp add: comp_assoc point_equations(1,3) point_not_equal inf.absorb1) lemma edge_end: assumes "is_point p" and "is_point q" and "p ≠ q" shows "end_points (p;q⇧^{T}) = q" using assms edge_start by simp lemma loop_no_start: assumes "is_point p" shows "start_points (p;p⇧^{T}) = 0" by simp lemma loop_no_end: assumes "is_point p" shows "end_points (p;p⇧^{T}) = 0" by simp lemma start_point_no_predecessor: "x;start_points(x) = 0" by (metis inf_top.right_neutral modular_1_aux') lemma end_point_no_successor: "x⇧^{T};end_points(x) = 0" by (metis conv_invol start_point_no_predecessor) lemma start_to_end: assumes "path x" shows "start_points(x);end_points(x)⇧^{T}≤ x⇧^{⋆}" proof (cases "end_points(x) = 0") assume "end_points(x) = 0" thus ?thesis by simp next assume ass: "end_points(x) ≠ 0" hence nz: "x;end_points(x) ≠ 0" by (metis comp_res_aux compl_bot_eq inf.left_idem) have a: "x;end_points(x);end_points(x)⇧^{T}≤ x + x⇧^{T}" by (metis end_point_at_most_one assms(1) is_inj_def comp_assoc mult_isol mult_oner le_supI1) have "start_points(x);end_points(x)⇧^{T}= start_points(x);1;end_points(x)⇧^{T}" using ass by (simp add: comp_assoc is_vector_def one_compl vector_1) also have "... = start_points(x);1;x;end_points(x);1;end_points(x)⇧^{T}" using nz tarski by (simp add: comp_assoc) also have "... = start_points(x);1;x;end_points(x);end_points(x)⇧^{T}" using ass by (simp add: comp_assoc is_vector_def one_compl vector_1) also with a assms(1) have "... ≤ x⇧^{⋆}" using path_concat_aux_5 comp_assoc eq_refl by simp finally show ?thesis . qed lemma path_acyclic: assumes "has_start_points_path x" shows "is_acyclic x" proof - let ?r = "start_points(x)" have pt: "point(?r)" using assms point_is_point start_point_iff2 by blast have "x⇧^{+}⋅1' = (x⇧^{+})⇧^{T}⋅x⇧^{+}⋅1'" by (metis conv_e conv_times inf.assoc inf.left_idem inf_le2 many_strongly_connected_iff_7 mult_oner star_subid) also have "... ≤ x⇧^{T};1⋅x⇧^{+}⋅1'" by (metis conv_contrav inf.commute maddux_20 meet_double_iso plus_top star_conv star_slide_var) finally have "?r;(x⇧^{+}⋅1') ≤ ?r;(x⇧^{T};1⋅x⇧^{+}⋅1')" using mult_isol by blast also have "... = (?r⋅1;x);(x⇧^{+}⋅1')" by (metis (no_types, lifting) comp_assoc conv_contrav conv_invol conv_one inf.assoc is_vector_def one_idem_mult vector_2) also have "... = ?r;x;(x⇧^{+}⋅1')" by (metis comp_assoc inf_top.right_neutral is_vector_def one_compl one_idem_mult vector_1) also have "... ≤ (x⇧^{⋆}+ x⇧^{T}⇧^{⋆});(x⇧^{+}⋅1')" using assms(1) mult_isor by (meson connected_iff4 dual_order.trans mult_subdistr path_concat_aux3_3) also have "... = x⇧^{⋆};(x⇧^{+}⋅1') + x⇧^{T}⇧^{+};(x⇧^{+}⋅1')" by (metis distrib_right star_star_plus sup.commute) also have "... ≤ x⇧^{⋆};(x⇧^{+}⋅1') + x⇧^{T};1" by (metis join_isol mult_isol plus_top top_greatest) finally have "?r;(x⇧^{+}⋅1');1 ≤ x⇧^{⋆};(x⇧^{+}⋅1');1 + x⇧^{T};1" by (metis distrib_right inf_absorb2 mult_assoc mult_subdistr one_idem_mult) hence 1: "?r;(x⇧^{+}⋅1');1 ≤ x⇧^{T};1" using assms(1) path_def inj_implies_step_forwards_backwards sup_absorb2 by simp have "x⇧^{+}⋅1' ≤ (x⇧^{+}⋅1');1" by (simp add: maddux_20) also have "... ≤ ?r⇧^{T};?r;(x⇧^{+}⋅1');1" using pt comp_assoc point_def ss423conv by fastforce also have "... ≤ ?r⇧^{T};x⇧^{T};1" using 1 by (simp add: comp_assoc mult_isol) also have "... = 0" by (metis start_point_no_predecessor annil conv_contrav conv_zero) finally show ?thesis using galois_aux le_bot by blast qed text ‹Equivalences for ‹terminating›› lemma backward_terminating_iff1: assumes "path x" shows "backward_terminating x ⟷ has_start_points x ∨ x = 0" proof assume "backward_terminating x" hence "1;x;1 ≤ 1;-(1;x);x;1;1" by (metis mult_isor mult_isol comp_assoc) also have "... = -(1;x);x;1" by (metis conv_compl conv_contrav conv_invol conv_one mult_assoc one_compl one_idem_mult) finally have "1;x;1 ≤ -(1;x);x;1" . with tarski show "has_start_points x ∨ x = 0" by (metis top_le) next show "has_start_points x ∨ x = 0 ⟹ backward_terminating x" by fastforce qed lemma backward_terminating_iff2_aux: assumes "path x" shows "x;1 ⋅ 1;x⇧^{T}⋅ -(1;x) ≤ x⇧^{T}⇧^{⋆}" proof - have "x;1 ⋅ 1;x⇧^{T}≤ x;1;x;x⇧^{T}" by (metis conv_invol modular_var_3 vector_meet_comp_x vector_meet_comp_x') also from assms have "... ≤ (x⇧^{⋆}+ x⇧^{T}⇧^{⋆});x⇧^{T}" using path_def mult_isor by blast also have "... ≤ x⇧^{⋆};x;x⇧^{T}+ x⇧^{T}⇧^{⋆};x⇧^{T}" by (simp add: star_star_plus star_slide_var add_comm) also from assms have "... ≤ x⇧^{⋆};1' + x⇧^{T}⇧^{⋆};x⇧^{T}" by (metis path_def is_inj_def join_iso mult_assoc mult_isol) also have "... = x⇧^{+}+ x⇧^{T}⇧^{⋆}" by (metis mult_1_right star_slide_var star_star_plus sup.commute) also have "... ≤ x⇧^{T}⇧^{⋆}+ 1;x" by (metis join_iso mult_isor star_slide_var top_greatest add_comm) finally have "x;1 ⋅ 1;x⇧^{T}≤ x⇧^{T}⇧^{⋆}+ 1;x" . thus ?thesis by (simp add: galois_1 sup.commute) qed lemma backward_terminating_iff2: assumes "path x" shows "backward_terminating x ⟷ x ≤ x⇧^{T}⇧^{⋆};-(x⇧^{T};1)" proof assume "backward_terminating x" with assms have "has_start_points x ∨ x = 0" by (simp add: backward_terminating_iff1) thus "x ≤ x⇧^{T}⇧^{⋆};-(x⇧^{T};1)" proof assume "x = 0" thus ?thesis by simp next assume "has_start_points x" hence aux1: "1 = 1;x⇧^{T};-(x⇧^{T};1)" by (metis comp_assoc conv_compl conv_contrav conv_one) have "x = x ⋅ 1" by simp also have "... ≤ (x;-(1;x) ⋅ 1;x⇧^{T});-(x⇧^{T};1)" by (metis inf.commute aux1 conv_compl conv_contrav conv_invol conv_one modular_2_var) also have "... = (x;1 ⋅ -(1;x) ⋅ 1;x⇧^{T});-(x⇧^{T};1)" by (metis comp_assoc conv_compl conv_contrav conv_invol conv_one inf.commute inf_top_left one_compl ra_1) also from assms have "... ≤ x⇧^{T}⇧^{⋆};-(x⇧^{T};1)" using backward_terminating_iff2_aux inf.commute inf.assoc mult_isor by fastforce finally show "x ≤ x⇧^{T}⇧^{⋆};-(x⇧^{T};1)" . qed next assume "x ≤ x⇧^{T}⇧^{⋆};-(x⇧^{T};1)" hence"x ≤ x⇧^{T}⇧^{⋆};-(x⇧^{T};1) ⋅ x" by simp also have "... = (x⇧^{T}⇧^{⋆}⋅ -(1;x));1 ⋅ x" by (metis one_compl conv_compl conv_contrav conv_invol conv_one inf_top_left ra_2) also have "... ≤ (x⇧^{T}⇧^{⋆}⋅ -(1;x)) ; (1 ⋅ (x⇧^{⋆}⋅ -(1;x)⇧^{T});x)" by (metis (mono_tags) conv_compl conv_invol conv_times modular_1_var star_conv) also have "... ≤ -(1;x);x⇧^{⋆};x" by (simp add: mult_assoc mult_isol_var) also have "... ≤ -(1;x);x;1" by (simp add: mult_assoc mult_isol star_slide_var) finally show "backward_terminating x" . qed lemma backward_terminating_iff3_aux: assumes "path x" shows "x⇧^{T};1 ⋅ 1;x⇧^{T}⋅ -(1;x) ≤ x⇧^{T}⇧^{⋆}" proof - have "x⇧^{T};1 ⋅ 1;x⇧^{T}≤ x⇧^{T};1;x;x⇧^{T}" by (metis conv_invol modular_var_3 vector_meet_comp_x vector_meet_comp_x') also from assms have "... ≤ (x⇧^{⋆}+ x⇧^{T}⇧^{⋆});x⇧^{T}" using mult_isor path_concat_aux3_2 by blast also have "... ≤ x⇧^{⋆};x;x⇧^{T}+ x⇧^{T}⇧^{⋆};x⇧^{T}" by (simp add: star_star_plus star_slide_var add_comm) also from assms have "... ≤ x⇧^{⋆};1' + x⇧^{T}⇧^{⋆};x⇧^{T}" by (metis path_def is_inj_def join_iso mult_assoc mult_isol) also have "... = x⇧^{+}+ x⇧^{T}⇧^{⋆}" by (metis mult_1_right star_slide_var star_star_plus sup.commute) also have "... ≤ x⇧^{T}⇧^{⋆}+ 1;x" by (metis join_iso mult_isor star_slide_var top_greatest add_comm) finally have "x⇧^{T};1 ⋅ 1;x⇧^{T}≤ x⇧^{T}⇧^{⋆}+ 1;x" . thus ?thesis by (simp add: galois_1 sup.commute) qed lemma backward_terminating_iff3: assumes "path x" shows "backward_terminating x ⟷ x⇧^{T}≤ x⇧^{T}⇧^{⋆};-(x⇧^{T};1)" proof assume "backward_terminating x" with assms have "has_start_points x ∨ x = 0" by (simp add: backward_terminating_iff1) thus "x⇧^{T}≤ x⇧^{T}⇧^{⋆};-(x⇧^{T};1)" proof assume "x = 0" thus ?thesis by simp next assume "has_start_points x" hence aux1: "1 = 1;x⇧^{T};-(x⇧^{T};1)" by (metis comp_assoc conv_compl conv_contrav conv_one) have "x⇧^{T}= x⇧^{T}⋅ 1" by simp also have "... ≤ (x⇧^{T};-(1;x) ⋅ 1;x⇧^{T});-(x⇧^{T};1)" by (metis inf.commute aux1 conv_compl conv_contrav conv_invol conv_one modular_2_var) also have "... = (x⇧^{T};1 ⋅ -(1;x) ⋅ 1;x⇧^{T});-(x⇧^{T};1)" by (metis comp_assoc conv_compl conv_contrav conv_invol conv_one inf.commute inf_top_left one_compl ra_1) also from assms have "... ≤ x⇧^{T}⇧^{⋆};-(x⇧^{T};1)" using backward_terminating_iff3_aux inf.commute inf.assoc mult_isor by fastforce finally show "x⇧^{T}≤ x⇧^{T}⇧^{⋆};-(x⇧^{T};1)" . qed next have 1: "-(1;x) ⋅ x = 0" by (simp add: galois_aux2 inf.commute maddux_21) assume "x⇧^{T}≤ x⇧^{T}⇧^{⋆};-(x⇧^{T};1)" hence "x = -(1;x);x⇧^{⋆}⋅ x" by (metis (mono_tags, lifting) conv_compl conv_contrav conv_iso conv_one inf.absorb2 star_conv) also have "... = (-(1;x);x⇧^{+}+ -(1;x);1') ⋅ x" by (metis distrib_left star_unfoldl_eq sup_commute) also have "... = -(1;x);x⇧^{+}⋅ x + -(1;x) ⋅ x" by (simp add: inf_sup_distrib2) also have "... ≤ -(1;x);x⇧^{+}" using 1 by simp also have "... ≤ -(1;x);x;1" by (simp add: mult_assoc mult_isol star_slide_var) finally show "backward_terminating x" . qed lemma backward_terminating_iff4: assumes "path x" shows "backward_terminating x ⟷ x ≤ -(1;x);x⇧^{⋆}" apply (subst backward_terminating_iff3) apply (rule assms) by (metis (mono_tags, lifting) conv_compl conv_iso star_conv conv_contrav conv_one) lemma forward_terminating_iff1: assumes "path x" shows "forward_terminating x ⟷ has_end_points x ∨ x = 0" by (metis comp_assoc eq_refl le_bot one_compl tarski top_greatest) lemma forward_terminating_iff2: assumes "path x" shows "forward_terminating x ⟷ x⇧^{T}≤ x⇧^{⋆};-(x;1)" by (metis assms backward_terminating_iff1 backward_terminating_iff2 end_point_iff2 forward_terminating_iff1 compl_bot_eq conv_compl conv_invol conv_one conv_path double_compl start_point_iff2) lemma forward_terminating_iff3: assumes "path x" shows "forward_terminating x ⟷ x ≤ x⇧^{⋆};-(x;1)" by (metis assms backward_terminating_iff1 backward_terminating_iff3 end_point_iff2 forward_terminating_iff1 compl_bot_eq conv_compl conv_invol conv_one conv_path double_compl start_point_iff2) lemma forward_terminating_iff4: assumes "path x" shows "forward_terminating x ⟷ x ≤ -(1;x⇧^{T});x⇧^{T}⇧^{⋆}" using forward_terminating_iff2 conv_contrav conv_iso star_conv assms conv_compl by force lemma terminating_iff1: assumes "path x" shows "terminating x ⟷ has_start_end_points x ∨ x = 0" using assms backward_terminating_iff1 forward_terminating_iff1 by fastforce lemma terminating_iff2: assumes "path x" shows "terminating x ⟷ x ≤ x⇧^{T}⇧^{⋆};-(x⇧^{T};1) ⋅ -(1;x⇧^{T});x⇧^{T}⇧^{⋆}" using assms backward_terminating_iff2 forward_terminating_iff2 conv_compl conv_iso star_conv by force lemma terminating_iff3: assumes "path x" shows "terminating x ⟷ x ≤ x⇧^{⋆};-(x;1) ⋅ -(1;x);x⇧^{⋆}" using assms backward_terminating_iff4 forward_terminating_iff3 by fastforce lemma backward_terminating_path_irreflexive: assumes "backward_terminating_path x" shows "x ≤ -1'" proof - have 1: "x;x⇧^{T}≤ 1'" using assms is_inj_def path_def by blast have "x;(x⇧^{T}⋅ 1') ≤ x;x⇧^{T}⋅ x" by (metis inf.bounded_iff inf.commute mult_1_right mult_subdistl) also have "... ≤ 1' ⋅ x" using 1 meet_iso by blast also have "... = 1' ⋅ x⇧^{T}" by (metis conv_e conv_times inf.cobounded1 is_test_def test_eq_conv) finally have 2: "x⇧^{T};-(x⇧^{T}⋅ 1') ≤ -(x⇧^{T}⋅ 1')" by (metis compl_le_swap1 conv_galois_1 inf.commute) have "x⇧^{T}⋅ 1' ≤ x⇧^{T};1" by (simp add: le_infI1 maddux_20) hence "-(x⇧^{T};1) ≤ -(x⇧^{T}⋅ 1')" using compl_mono by blast hence "x⇧^{T};-(x⇧^{T}⋅ 1') + -(x⇧^{T};1) ≤ -(x⇧^{T}⋅ 1')" using 2 by (simp add: le_supI) hence "x⇧^{T}⇧^{⋆};-(x⇧^{T};1) ≤ -(x⇧^{T}⋅ 1')" by (simp add: rtc_inductl) hence "x⇧^{T}⋅ 1' ⋅ x⇧^{T}⇧^{⋆};-(x⇧^{T};1) = 0" by (simp add: compl_le_swap1 galois_aux) hence "x⇧^{T}⋅ 1' = 0" using assms backward_terminating_iff3 inf.order_iff le_infI1 by blast hence "x ⋅ 1' = 0" by (simp add: conv_self_conjugate) thus ?thesis by (simp add: galois_aux) qed lemma forward_terminating_path_end_points_1: assumes "forward_terminating_path x" shows "x ≤ x⇧^{+};end_points x" proof - have 1: "-(x;1) ⋅ x = 0" by (simp add: galois_aux maddux_20) have "x = x⇧^{⋆};-(x;1) ⋅ x" using assms forward_terminating_iff3 inf.absorb2 by fastforce also have "... = (x⇧^{+};-(x;1) + 1';-(x;1)) ⋅ x" by (simp add: sup.commute) also have "... =