# Theory Forests

(* Title:      Orientations and Undirected Forests
Author:     Walter Guttmann
Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

section ‹Orientations and Undirected Forests›

text ‹
In this theory we study orientations and various second-order specifications of undirected forests.
The results are structured by the classes in which they can be proved, which correspond to algebraic structures.
Most classes are generalisations of Kleene relation algebras.
None of the classes except ‹kleene_relation_algebra› assumes the double-complement law ‹--x = x› available in Boolean algebras.
The corresponding paper does not elaborate these fine distinctions, so some results take a different form in this theory.
They usually specialise to Kleene relation algebras after simplification using ‹--x = x›.
›

theory Forests

imports Stone_Kleene_Relation_Algebras.Kleene_Relation_Algebras

begin

subsection ‹Orientability›

(* move to Relation_Algebras *)
context bounded_distrib_allegory_signature
begin

abbreviation irreflexive_inf :: "'a ⇒ bool" where "irreflexive_inf x ≡ x ⊓ 1 = bot"

end

context bounded_distrib_allegory
begin

(* move to Relation_Algebras *)
lemma irreflexive_inf_arc_asymmetric:
"irreflexive_inf x ⟹ arc x ⟹ asymmetric x"
proof -
assume "irreflexive_inf x" "arc x"
hence "bot = (x * top)⇧T ⊓ x"
by (metis arc_top_arc comp_right_one schroeder_1)
thus ?thesis
by (metis comp_inf.semiring.mult_zero_right conv_inf_bot_iff inf.sup_relative_same_increasing top_right_mult_increasing)
qed

lemma asymmetric_inf:
"asymmetric x ⟷ irreflexive_inf (x * x)"
using inf.sup_monoid.add_commute schroeder_2 by force

lemma asymmetric_irreflexive_inf:
"asymmetric x ⟹ irreflexive_inf x"
by (metis asymmetric_inf_closed coreflexive_symmetric inf.idem inf_le2)

lemma transitive_asymmetric_irreflexive_inf:
"transitive x ⟹ asymmetric x ⟷ irreflexive_inf x"
by (smt asymmetric_inf asymmetric_irreflexive_inf inf.absorb2 inf.cobounded1 inf.sup_monoid.add_commute inf_assoc le_bot)

abbreviation "orientation x y ≡ y ⊔ y⇧T = x ∧ asymmetric y"
abbreviation "loop_orientation x y ≡ y ⊔ y⇧T = x ∧ antisymmetric y"
abbreviation "super_orientation x y ≡ x ≤ y ⊔ y⇧T ∧ asymmetric y"
abbreviation "loop_super_orientation x y ≡ x ≤ y ⊔ y⇧T ∧ antisymmetric y"

lemma orientation_symmetric:
"orientation x y ⟹ symmetric x"
using conv_dist_sup sup_commute by auto

lemma orientation_irreflexive_inf:
"orientation x y ⟹ irreflexive_inf x"
using asymmetric_irreflexive_inf asymmetric_conv_closed inf_sup_distrib2 by auto

lemma loop_orientation_symmetric:
"loop_orientation x y ⟹ symmetric x"
using conv_dist_sup sup_commute by auto

lemma loop_orientation_diagonal:
"loop_orientation x y ⟹ y ⊓ y⇧T = x ⊓ 1"
by (metis inf.sup_monoid.add_commute inf.sup_same_context inf_le2 inf_sup_distrib1 one_inf_conv sup.idem)

lemma super_orientation_irreflexive_inf:
"super_orientation x y ⟹ irreflexive_inf x"
using coreflexive_bot_closed inf.sup_monoid.add_assoc inf.sup_right_divisibility inf_bot_right loop_orientation_diagonal by fastforce

lemma loop_super_orientation_diagonal:
"loop_super_orientation x y ⟹ x ⊓ 1 ≤ y ⊓ y⇧T"
using inf.sup_right_divisibility inf_assoc loop_orientation_diagonal by fastforce

definition "orientable x ≡ ∃y . orientation x y"
definition "loop_orientable x ≡ ∃y . loop_orientation x y"
definition "super_orientable x ≡ ∃y . super_orientation x y"
definition "loop_super_orientable x ≡ ∃y . loop_super_orientation x y"

lemma orientable_symmetric:
"orientable x ⟹ symmetric x"
using orientable_def orientation_symmetric by blast

lemma orientable_irreflexive_inf:
"orientable x ⟹ irreflexive_inf x"
using orientable_def orientation_irreflexive_inf by blast

lemma loop_orientable_symmetric:
"loop_orientable x ⟹ symmetric x"
using loop_orientable_def loop_orientation_symmetric by blast

lemma super_orientable_irreflexive_inf:
"super_orientable x ⟹ irreflexive_inf x"
using super_orientable_def super_orientation_irreflexive_inf by blast

lemma orientable_down_closed:
assumes "symmetric x"
and "x ≤ y"
and "orientable y"
shows "orientable x"
proof -
from assms(3) obtain z where 1: "z ⊔ z⇧T = y ∧ asymmetric z"
using orientable_def by blast
let ?z = "x ⊓ z"
have "orientation x ?z"
proof (rule conjI)
show "asymmetric ?z"
using 1 by (simp add: conv_dist_inf inf.left_commute inf.sup_monoid.add_assoc)
thus "?z ⊔ ?z⇧T = x"
using 1 by (metis assms(1,2) conv_dist_inf inf.orderE inf_sup_distrib1)
qed
thus ?thesis
using orientable_def by blast
qed

lemma loop_orientable_down_closed:
assumes "symmetric x"
and "x ≤ y"
and "loop_orientable y"
shows "loop_orientable x"
proof -
from assms(3) obtain z where 1: "z ⊔ z⇧T = y ∧ antisymmetric z"
using loop_orientable_def by blast
let ?z = "x ⊓ z"
have "loop_orientation x ?z"
proof (rule conjI)
show "antisymmetric ?z"
using 1 antisymmetric_inf_closed inf_commute by fastforce
thus "?z ⊔ ?z⇧T = x"
using 1 by (metis assms(1,2) conv_dist_inf inf.orderE inf_sup_distrib1)
qed
thus ?thesis
using loop_orientable_def by blast
qed

lemma super_orientable_down_closed:
assumes "x ≤ y"
and "super_orientable y"
shows "super_orientable x"
using assms order_lesseq_imp super_orientable_def by auto

lemma loop_super_orientable_down_closed:
assumes "x ≤ y"
and "loop_super_orientable y"
shows "loop_super_orientable x"
using assms order_lesseq_imp loop_super_orientable_def by auto

abbreviation "orientable_1 x ≡ loop_super_orientable x"
abbreviation "orientable_2 x ≡ ∃y . x ≤ y ⊔ y⇧T ∧ y ⊓ y⇧T ≤ x ⊓ 1"
abbreviation "orientable_3 x ≡ ∃y . x ≤ y ⊔ y⇧T ∧ y ⊓ y⇧T = x ⊓ 1"
abbreviation "orientable_4 x ≡ irreflexive_inf x ⟶ super_orientable x"
abbreviation "orientable_5 x ≡ symmetric x ⟶ loop_orientable x"
abbreviation "orientable_6 x ≡ symmetric x ⟶ (∃y . y ⊔ y⇧T = x ∧ y ⊓ y⇧T ≤ x ⊓ 1)"
abbreviation "orientable_7 x ≡ symmetric x ⟶ (∃y . y ⊔ y⇧T = x ∧ y ⊓ y⇧T = x ⊓ 1)"
abbreviation "orientable_8 x ≡ symmetric x ∧ irreflexive_inf x ⟶ orientable x"

lemma super_orientation_diagonal:
"x ≤ y ⊔ y⇧T ⟹ y ⊓ y⇧T ≤ x ⊓ 1 ⟹ y ⊓ y⇧T = x ⊓ 1"
using inf.antisym loop_super_orientation_diagonal by auto

lemma orientable_2_implies_1:
"orientable_2 x ⟹ orientable_1 x"
using loop_super_orientable_def by auto

lemma orientable_2_3:
"orientable_2 x ⟷ orientable_3 x"
using eq_refl super_orientation_diagonal by blast

lemma orientable_5_6:
"orientable_5 x ⟷ orientable_6 x"
using loop_orientable_def loop_orientation_diagonal by fastforce

lemma orientable_6_7:
"orientable_6 x ⟷ orientable_7 x"
using super_orientation_diagonal by fastforce

lemma orientable_7_implies_8:
"orientable_7 x ⟹ orientable_8 x"
using orientable_def by blast

lemma orientable_5_implies_1:
"orientable_5 (x ⊔ x⇧T) ⟹ orientable_1 x"
using conv_dist_sup loop_orientable_def loop_super_orientable_def sup_commute by fastforce

text ‹ternary predicate S called ‹split› here›

abbreviation "split x y z ≡ y ⊓ y⇧T = x ∧ y ⊔ y⇧T = z"

text ‹Theorem 3.1›

lemma orientation_split:
"orientation x y ⟷ split bot y x"
by auto

text ‹Theorem 3.2›

lemma split_1_loop_orientation:
"split 1 y x ⟹ loop_orientation x y"
by simp

text ‹Theorem 3.3›

lemma loop_orientation_split:
"loop_orientation x y ⟷ split (x ⊓ 1) y x"
by (metis inf.cobounded2 loop_orientation_diagonal)

text ‹Theorem 3.4›

lemma loop_orientation_split_inf_1:
"loop_orientation x y ⟷ split (y ⊓ 1) y x"
by (metis inf.sup_monoid.add_commute inf.sup_same_context inf_le2 one_inf_conv)

lemma loop_orientation_top_split:
"loop_orientation top y ⟷ split 1 y top"
by (simp add: loop_orientation_split)

text ‹injective and transitive orientations›

definition "injectively_orientable x ≡ ∃y . orientation x y ∧ injective y"

lemma injectively_orientable_orientable:
"injectively_orientable x ⟹ orientable x"
using injectively_orientable_def orientable_def by auto

lemma orientable_orientable_1:
"orientable x ⟹ orientable_1 x"
by (metis bot_least order_refl loop_super_orientable_def orientable_def)

lemma injectively_orientable_down_closed:
assumes "symmetric x"
and "x ≤ y"
and "injectively_orientable y"
shows "injectively_orientable x"
proof -
from assms(3) obtain z where 1: "z ⊔ z⇧T = y ∧ asymmetric z ∧ injective z"
using injectively_orientable_def by blast
let ?z = "x ⊓ z"
have 2: "injective ?z"
using 1 inf_commute injective_inf_closed by fastforce
have "orientation x ?z"
proof (rule conjI)
show "asymmetric ?z"
using 1 by (simp add: conv_dist_inf inf.left_commute inf.sup_monoid.add_assoc)
thus "?z ⊔ ?z⇧T = x"
using 1 by (metis assms(1,2) conv_dist_inf inf.orderE inf_sup_distrib1)
qed
thus ?thesis
using 2 injectively_orientable_def by blast
qed

definition "transitively_orientable x ≡ ∃y . orientation x y ∧ transitive y"

lemma transitively_orientable_orientable:
"transitively_orientable x ⟹ orientable x"
using transitively_orientable_def orientable_def by auto

lemma irreflexive_transitive_orientation_asymmetric:
assumes "irreflexive_inf x"
and "transitive y"
and "y ⊔ y⇧T = x"
shows "asymmetric y"
using assms comp_inf.mult_right_dist_sup transitive_asymmetric_irreflexive_inf by auto

text ‹Theorem 12›

lemma transitively_orientable_2:
"transitively_orientable x ⟷ irreflexive_inf x ∧ (∃y . y ⊔ y⇧T = x ∧ transitive y)"
by (metis irreflexive_transitive_orientation_asymmetric coreflexive_bot_closed loop_orientation_split transitively_orientable_def)

end

context relation_algebra_signature
begin

abbreviation asymmetric_var :: "'a ⇒ bool" where "asymmetric_var x ≡ irreflexive (x * x)"

end

context pd_allegory
begin

text ‹Theorem 1.4›

lemma asymmetric_var:
"asymmetric x ⟷ asymmetric_var x"
using asymmetric_inf pseudo_complement by auto

text ‹Theorem 1.3›
text ‹(Theorem 1.2 is ‹asymmetric_irreflexive› in ‹Relation_Algebras›)›

lemma transitive_asymmetric_irreflexive:
"transitive x ⟹ asymmetric x ⟷ irreflexive x"
using strict_order_var by blast

lemma orientable_irreflexive:
"orientable x ⟹ irreflexive x"
using orientable_irreflexive_inf pseudo_complement by blast

lemma super_orientable_irreflexive:
"super_orientable x ⟹ irreflexive x"
using pseudo_complement super_orientable_irreflexive_inf by blast

lemma orientation_diversity_split:
"orientation (-1) y ⟷ split bot y (-1)"
by auto

abbreviation "linear_orderable_1 x ≡ linear_order x"
abbreviation "linear_orderable_2 x ≡ linear_strict_order x"
abbreviation "linear_orderable_3 x ≡ transitive x ∧ asymmetric x ∧ strict_linear x"
abbreviation "linear_orderable_3a x ≡ transitive x ∧ strict_linear x"

abbreviation "orientable_11 x ≡ split 1 x top"
abbreviation "orientable_12 x ≡ split bot x (-1)"

lemma linear_strict_order_split:
"linear_strict_order x ⟷ transitive x ∧ split bot x (-1)"
using strict_order_var by blast

text ‹Theorem 1.6›

lemma linear_strict_order_without_irreflexive:
"linear_strict_order x ⟷ transitive x ∧ strict_linear x"
using strict_linear_irreflexive by auto

lemma linear_order_without_reflexive:
"linear_order x ⟷ antisymmetric x ∧ transitive x ∧ linear x"
using linear_reflexive by blast

lemma linear_orderable_1_implies_2:
"linear_orderable_1 x ⟹ linear_orderable_2 (x ⊓ -1)"
using linear_order_strict_order by blast

lemma linear_orderable_2_3:
"linear_orderable_2 x ⟷ linear_orderable_3 x"
using linear_strict_order_split by auto

lemma linear_orderable_3_3a:
"linear_orderable_3 x ⟷ linear_orderable_3a x"
using strict_linear_irreflexive strict_order_var by blast

lemma linear_orderable_3_implies_orientable_12:
"linear_orderable_3 x ⟹ orientable_12 x"
by simp

lemma orientable_11_implies_12:
"orientable_11 x ⟹ orientable_12 (x ⊓ -1)"
by (smt inf_sup_distrib2 conv_complement conv_dist_inf conv_involutive inf_import_p inf_top.left_neutral linear_asymmetric maddux_3_13 p_inf symmetric_one_closed)

end

context stone_relation_algebra
begin

text ‹Theorem 3.5›

lemma split_symmetric_asymmetric:
assumes "regular x"
shows "split x y z ⟷ y ⊓ y⇧T = x ∧ (y ⊓ -y⇧T) ⊔ (y ⊓ -y⇧T)⇧T = z ⊓ -x ∧ x ≤ z"
proof
assume "split x y z"
thus "y ⊓ y⇧T = x ∧ (y ⊓ -y⇧T) ⊔ (y ⊓ -y⇧T)⇧T = z ⊓ -x ∧ x ≤ z"
by (metis conv_complement conv_dist_inf conv_involutive inf.cobounded1 inf.sup_monoid.add_commute inf_import_p inf_sup_distrib2 le_supI1)
next
assume "y ⊓ y⇧T = x ∧ (y ⊓ -y⇧T) ⊔ (y ⊓ -y⇧T)⇧T = z ⊓ -x ∧ x ≤ z"
thus "split x y z"
by (smt (z3) assms conv_dist_sup conv_involutive inf.absorb2 inf.boundedE inf.cobounded1 inf.idem inf.sup_monoid.add_commute inf_import_p maddux_3_11_pp sup.left_commute sup_commute sup_inf_absorb)
qed

lemma orientable_1_2:
"orientable_1 x ⟷ orientable_2 x"
proof
assume "orientable_1 x"
from this obtain y where 1: "x ≤ y ⊔ y⇧T ∧ y ⊓ y⇧T ≤ 1"
using loop_super_orientable_def by blast
let ?y = "(x ⊓ 1) ⊔ (y ⊓ -1)"
have "x ≤ ?y ⊔ ?y⇧T ∧ ?y ⊓ ?y⇧T ≤ x ⊓ 1"
proof
have "x ⊓ -1 ≤ (y ⊓ -1) ⊔ (y⇧T ⊓ -1)"
using 1 inf.sup_right_divisibility inf_commute inf_left_commute inf_sup_distrib2 by auto
also have "... ≤ ?y ⊔ ?y⇧T"
by (metis comp_inf.semiring.add_mono conv_complement conv_dist_inf conv_isotone sup.cobounded2 symmetric_one_closed)
finally show "x ≤ ?y ⊔ ?y⇧T"
by (metis comp_inf.semiring.add_mono maddux_3_11_pp regular_one_closed sup.cobounded1 sup.left_idem)
have "x = (x ⊓ 1) ⊔ (x ⊓ -1)"
by (metis maddux_3_11_pp regular_one_closed)
have "?y ⊓ ?y⇧T = (x ⊓ 1) ⊔ ((y ⊓ -1) ⊓ (y⇧T ⊓ -1))"
by (metis comp_inf.semiring.distrib_left conv_complement conv_dist_inf conv_dist_sup coreflexive_symmetric distrib_imp1 inf_le2 symmetric_one_closed)
also have "... = x ⊓ 1"
by (metis 1 inf_assoc inf_commute pseudo_complement regular_one_closed selection_closed_id inf.cobounded2 maddux_3_11_pp)
finally show "?y ⊓ ?y⇧T ≤ x ⊓ 1"
by simp
qed
thus "orientable_2 x"
by blast
next
assume "orientable_2 x"
thus "orientable_1 x"
using loop_super_orientable_def by auto
qed

lemma orientable_8_implies_5:
assumes "orientable_8 (x ⊓ -1)"
shows "orientable_5 x"
proof
assume 1: "symmetric x"
hence "symmetric (x ⊓ -1)"
by (simp add: conv_complement symmetric_inf_closed)
hence "orientable (x ⊓ -1)"
by (simp add: assms pseudo_complement)
from this obtain y where 2: "y ⊔ y⇧T = x ⊓ -1 ∧ asymmetric y"
using orientable_def by blast
let ?y = "y ⊔ (x ⊓ 1)"
have "loop_orientation x ?y"
proof
have "?y ⊔ ?y⇧T = y ⊔ y⇧T ⊔ (x ⊓ 1)"
using 1 conv_dist_inf conv_dist_sup sup_assoc sup_commute by auto
thus "?y ⊔ ?y⇧T = x"
by (metis 2 maddux_3_11_pp regular_one_closed)
have "?y ⊓ ?y⇧T = (y ⊓ y⇧T) ⊔ (x ⊓ 1)"
by (simp add: 1 conv_dist_sup sup_inf_distrib2 symmetric_inf_closed)
thus "antisymmetric ?y"
by (simp add: 2)
qed
thus "loop_orientable x"
using loop_orientable_def by blast
qed

lemma orientable_4_implies_1:
assumes "orientable_4 (x ⊓ -1)"
shows "orientable_1 x"
proof -
obtain y where 1: "x ⊓ -1 ≤ y ⊔ y⇧T ∧ asymmetric y"
using assms pseudo_complement super_orientable_def by auto
let ?y = "y ⊔ 1"
have "loop_super_orientation x ?y"
proof
show "x ≤ ?y ⊔ ?y⇧T"
by (smt 1 comp_inf.semiring.add_mono conv_dist_sup inf_le2 maddux_3_11_pp reflexive_one_closed regular_one_closed sup.absorb1 sup.left_commute sup_assoc symmetric_one_closed)
show "antisymmetric ?y"
using 1 conv_dist_sup distrib_imp1 inf_sup_distrib1 sup_monoid.add_commute by auto
qed
thus ?thesis
using loop_super_orientable_def by blast
qed

lemma orientable_1_implies_4:
assumes "orientable_1 (x ⊔ 1)"
shows "orientable_4 x"
proof
assume 1: "irreflexive_inf x"
obtain y where 2: "x ⊔ 1 ≤ y ⊔ y⇧T ∧ antisymmetric y"
using assms loop_super_orientable_def by blast
let ?y = "y ⊓ -1"
have "super_orientation x ?y"
proof
have "x ≤ (y ⊔ y⇧T) ⊓ -1"
using 1 2 pseudo_complement by auto
thus "x ≤ ?y ⊔ ?y⇧T"
by (simp add: conv_complement conv_dist_inf inf_sup_distrib2)
have "?y ⊓ ?y⇧T = y ⊓ y⇧T ⊓ -1"
using conv_complement conv_dist_inf inf_commute inf_left_commute by auto
thus "asymmetric ?y"
using 2 pseudo_complement by auto
qed
thus "super_orientable x"
using super_orientable_def by blast
qed

lemma orientable_1_implies_5:
assumes "orientable_1 x"
shows "orientable_5 x"
proof
assume 1: "symmetric x"
obtain y where 2: "x ≤ y ⊔ y⇧T ∧ antisymmetric y"
using assms loop_super_orientable_def by blast
let ?y = "(x ⊓ 1) ⊔ (y ⊓ x ⊓ -1)"
have "loop_orientation x ?y"
proof
have "?y ⊔ ?y⇧T = ((y ⊔ y⇧T) ⊓ x ⊓ -1) ⊔ (x ⊓ 1)"
by (simp add: 1 conv_complement conv_dist_inf conv_dist_sup inf_sup_distrib2 sup.left_commute sup_commute)
thus "?y ⊔ ?y⇧T = x"
by (metis 2 inf_absorb2 maddux_3_11_pp regular_one_closed)
have "?y ⊓ ?y⇧T = (x ⊓ 1) ⊔ ((y ⊓ x ⊓ -1) ⊓ (y⇧T ⊓ x⇧T ⊓ -1))"
by (simp add: 1 conv_complement conv_dist_inf conv_dist_sup sup_inf_distrib1)
thus "antisymmetric ?y"
by (metis 2 antisymmetric_inf_closed conv_complement conv_dist_inf inf_le2 le_supI symmetric_one_closed)
qed
thus "loop_orientable x"
using loop_orientable_def by blast
qed

text ‹Theorem 2›

lemma all_orientable_characterisations:
shows "(∀x . orientable_1 x) ⟷ (∀x . orientable_2 x)"
and "(∀x . orientable_1 x) ⟷ (∀x . orientable_3 x)"
and "(∀x . orientable_1 x) ⟷ (∀x . orientable_4 x)"
and "(∀x . orientable_1 x) ⟷ (∀x . orientable_5 x)"
and "(∀x . orientable_1 x) ⟷ (∀x . orientable_6 x)"
and "(∀x . orientable_1 x) ⟷ (∀x . orientable_7 x)"
and "(∀x . orientable_1 x) ⟷ (∀x . orientable_8 x)"
subgoal using orientable_1_2 by simp
subgoal using orientable_1_2 orientable_2_3 by simp
subgoal using orientable_1_implies_4 orientable_4_implies_1 by blast
subgoal using orientable_5_implies_1 orientable_1_implies_5 by blast
subgoal using orientable_5_6 orientable_5_implies_1 orientable_1_implies_5 by blast
subgoal using orientable_5_6 orientable_5_implies_1 orientable_6_7 orientable_1_implies_5 by force
subgoal using orientable_5_6 orientable_5_implies_1 orientable_6_7 orientable_7_implies_8 orientable_1_implies_5 orientable_8_implies_5 by auto
done

lemma orientable_12_implies_11:
"orientable_12 x ⟹ orientable_11 (x ⊔ 1)"
by (smt inf_top.right_neutral conv_complement conv_dist_sup conv_involutive inf_import_p maddux_3_13 p_bot p_dist_inf p_dist_sup regular_one_closed symmetric_one_closed)

(* The following lemma might go into Relation_Algebras. *)
lemma linear_strict_order_order:
"linear_strict_order x ⟹ linear_order (x ⊔ 1)"
by (simp add: strict_order_order transitive_asymmetric_irreflexive orientable_12_implies_11)

lemma linear_orderable_2_implies_1:
"linear_orderable_2 x ⟹ linear_orderable_1 (x ⊔ 1)"
using linear_strict_order_order by simp

text ‹Theorem 4›
text ‹Theorem 12›
text ‹Theorem 13›

lemma exists_split_characterisations:
shows "(∃x . linear_orderable_1 x) ⟷ (∃x . linear_orderable_2 x)"
and "(∃x . linear_orderable_1 x) ⟷ (∃x . linear_orderable_3 x)"
and "(∃x . linear_orderable_1 x) ⟷ (∃x . linear_orderable_3a x)"
and "(∃x . linear_orderable_1 x) ⟷ transitively_orientable (-1)"
and "(∃x . linear_orderable_1 x) ⟹ (∃x . orientable_11 x)"
and "(∃x . orientable_11 x) ⟷ (∃x . orientable_12 x)"
subgoal 1 using linear_strict_order_order linear_order_strict_order by blast
subgoal 2 using 1 strict_order_var by blast
subgoal using 1 linear_strict_order_without_irreflexive by auto
subgoal using 2 transitively_orientable_def by auto
subgoal using loop_orientation_top_split by blast
subgoal using orientable_11_implies_12 orientable_12_implies_11 by blast
done

text ‹Theorem 4›
text ‹Theorem 12›

lemma exists_all_orientable:
shows "(∃x . orientable_11 x) ⟷ (∀x . orientable_1 x)"
and "transitively_orientable (-1) ⟹ (∀x . orientable_8 x)"
subgoal apply (rule iffI)
subgoal using loop_super_orientable_def top_greatest by blast
subgoal using loop_orientation_top_split loop_super_orientable_def top_le by blast
done
subgoal using orientable_down_closed pseudo_complement transitively_orientable_orientable by blast
done

end

subsection ‹Undirected forests›

text ‹
We start with a few general results in Kleene algebras and a few basic properties of directed acyclic graphs.
›

(* move to Kleene_Algebras *)
context kleene_algebra
begin

text ‹Theorem 1.9›

lemma plus_separate_comp_bot:
assumes "x * y = bot"
shows "(x ⊔ y)⇧+ = x⇧+ ⊔ y⇧+ ⊔ y⇧+ * x⇧+"
proof -
have "(x ⊔ y)⇧+ = x * y⇧⋆ * x⇧⋆ ⊔ y⇧+ * x⇧⋆"
using assms cancel_separate_1 semiring.distrib_right mult_assoc by auto
also have "... = x⇧+ ⊔ y⇧+ * x⇧⋆"
by (simp add: assms star_absorb)
finally show ?thesis
by (metis star.circ_back_loop_fixpoint star.circ_plus_same sup_assoc sup_commute mult_assoc)
qed

end

(* move to Kleene_Relation_Algebras *)
context bounded_distrib_kleene_allegory
begin

lemma reflexive_inf_plus_star:
assumes "reflexive x"
shows "x ⊓ y⇧+ ≤ 1 ⟷ x ⊓ y⇧⋆ = 1"
using assms reflexive_inf_star sup.absorb_iff1 by auto

end

context pd_kleene_allegory
begin

(* move to Kleene_Relation_Algebras *)
lemma acyclic_star_inf_conv_iff:
assumes "irreflexive w"
shows "acyclic w ⟷ w⇧⋆ ⊓ w⇧T⇧⋆ = 1"
by (metis assms acyclic_star_below_complement_1 acyclic_star_inf_conv conv_complement conv_order equivalence_one_closed inf.absorb1 inf.left_commute pseudo_complement star.circ_increasing)

text ‹Theorem 1.7›

(* move to Kleene_Relation_Algebras *)
lemma acyclic_irreflexive_star_antisymmetric:
"acyclic x ⟷ irreflexive x ∧ antisymmetric (x⇧⋆)"
by (metis acyclic_star_inf_conv_iff conv_star_commute dual_order.trans eq_iff reflexive_inf_closed star.circ_mult_increasing star.circ_reflexive)

text ‹Theorem 1.8›

(* move to Kleene_Relation_Algebras *)
lemma acyclic_plus_asymmetric:
"acyclic x ⟷ asymmetric (x⇧+)"
using acyclic_asymmetric asymmetric_irreflexive star.circ_transitive_equal star.left_plus_circ mult_assoc by auto

text ‹Theorem 1.3›
text ‹(Theorem 1.1 is ‹acyclic_asymmetric› in ‹Kleene_Relation_Algebras›)›

lemma transitive_acyclic_irreflexive:
"transitive x ⟹ acyclic x ⟷ irreflexive x"
using antisym star.circ_mult_increasing star_right_induct_mult by fastforce

lemma transitive_acyclic_asymmetric:
"transitive x ⟹ acyclic x ⟷ asymmetric x"
using strict_order_var transitive_acyclic_irreflexive by blast

text ‹Theorem 1.5›

lemma strict_order_transitive_acyclic:
"strict_order x ⟷ transitive x ∧ acyclic x"
using transitive_acyclic_irreflexive by auto

lemma linear_strict_order_transitive_acyclic:
"linear_strict_order x ⟷ transitive x ∧ acyclic x ∧ strict_linear x"
using transitive_acyclic_irreflexive by auto

text ‹
The following are various specifications of an undirected graph being acyclic.
›

definition "acyclic_1 x ≡ ∀y . orientation x y ⟶ acyclic y"
definition "acyclic_1b x ≡ ∀y . orientation x y ⟶ y⇧⋆ ⊓ y⇧T⇧⋆ = 1"
definition "acyclic_2 x ≡ ∀y . y ≤ x ∧ asymmetric y ⟶ acyclic y"
definition "acyclic_2a x ≡ ∀y . y ⊔ y⇧T ≤ x ∧ asymmetric y ⟶ acyclic y"
definition "acyclic_2b x ≡ ∀y . y ⊔ y⇧T ≤ x ∧ asymmetric y ⟶ y⇧⋆ ⊓ y⇧T⇧⋆ = 1"
definition "acyclic_3a x ≡ ∀y . y ≤ x ∧ x ≤ y⇧⋆ ⟶ y = x"
definition "acyclic_3b x ≡ ∀y . y ≤ x ∧ y⇧⋆ = x⇧⋆ ⟶ y = x"
definition "acyclic_3c x ≡ ∀y . y ≤ x ∧ x ≤ y⇧+ ⟶ y = x"
definition "acyclic_3d x ≡ ∀y . y ≤ x ∧ y⇧+ = x⇧+ ⟶ y = x"
definition "acyclic_4 x ≡ ∀y . y ≤ x ⟶ x ⊓ y⇧⋆ ≤ --y"
definition "acyclic_4a x ≡ ∀y . y ≤ x ⟶ x ⊓ y⇧⋆ ≤ y"
definition "acyclic_4b x ≡ ∀y . y ≤ x ⟶ x ⊓ y⇧⋆ = y"
definition "acyclic_4c x ≡ ∀y . y ≤ x ⟶ y ⊓ (x ⊓ -y)⇧⋆ = bot"
definition "acyclic_5a x ≡ ∀y . y ≤ x ⟶ y⇧⋆ ⊓ (x ⊓ -y)⇧⋆ = 1"
definition "acyclic_5b x ≡ ∀y . y ≤ x ⟶ y⇧⋆ ⊓ (x ⊓ -y)⇧+ ≤ 1"
definition "acyclic_5c x ≡ ∀y . y ≤ x ⟶ y⇧+ ⊓ (x ⊓ -y)⇧⋆ ≤ 1"
definition "acyclic_5d x ≡ ∀y . y ≤ x ⟶ y⇧+ ⊓ (x ⊓ -y)⇧+ ≤ 1"
definition "acyclic_5e x ≡ ∀y z . y ≤ x ∧ z ≤ x ∧ y ⊓ z = bot ⟶ y⇧⋆ ⊓ z⇧⋆ = 1"
definition "acyclic_5f x ≡ ∀y z . y ⊔ z ≤ x ∧ y ⊓ z = bot ⟶ y⇧⋆ ⊓ z⇧⋆ = 1"
definition "acyclic_5g x ≡ ∀y z . y ⊔ z = x ∧ y ⊓ z = bot ⟶ y⇧⋆ ⊓ z⇧⋆ = 1"
definition "acyclic_6 x ≡ ∃y . y ⊔ y⇧T = x ∧ acyclic y ∧ injective y"

text ‹Theorem 6›

lemma acyclic_2_2a:
assumes "symmetric x"
shows "acyclic_2 x ⟷ acyclic_2a x"
proof -
have "⋀y . y ≤ x ⟷ y ⊔ y⇧T ≤ x"
using assms conv_isotone by force
thus ?thesis
by (simp add: acyclic_2_def acyclic_2a_def)
qed

text ‹Theorem 6›

lemma acyclic_2a_2b:
shows "acyclic_2a x ⟷ acyclic_2b x"
by (simp add: acyclic_2a_def acyclic_2b_def acyclic_star_inf_conv_iff asymmetric_irreflexive)

text ‹Theorem 5›

lemma acyclic_1_1b:
shows "acyclic_1 x ⟷ acyclic_1b x"
by (simp add: acyclic_1_def acyclic_1b_def acyclic_star_inf_conv_iff asymmetric_irreflexive)

text ‹Theorem 10›

lemma acyclic_6_1_injectively_orientable:
"acyclic_6 x ⟷ acyclic_1 x ∧ injectively_orientable x"
proof
assume "acyclic_6 x"
from this obtain y where 1: "y ⊔ y⇧T = x ∧ acyclic y ∧ injective y"
using acyclic_6_def by blast
have "acyclic_1 x"
proof (unfold acyclic_1_def, rule allI, rule impI)
fix z
assume 2: "orientation x z"
hence 3: "z = (z ⊓ y) ⊔ (z ⊓ y⇧T)"
by (metis 1 inf_sup_absorb inf_sup_distrib1)
have "(z ⊓ y) * (z ⊓ y⇧T) ≤ z * z ⊓ y * y⇧T"
by (simp add: comp_isotone)
also have "... ≤ -1 ⊓ 1"
using 1 2 asymmetric_var comp_inf.mult_isotone by blast
finally have 4: "(z ⊓ y) * (z ⊓ y⇧T) = bot"
by (simp add: le_bot)
have "z⇧+ = (z ⊓ y)⇧+ ⊔ (z ⊓ y⇧T)⇧+ ⊔ (z ⊓ y⇧T)⇧+ * (z ⊓ y)⇧+"
using 3 4 plus_separate_comp_bot by fastforce
also have "... ≤ y⇧+ ⊔ (z ⊓ y⇧T)⇧+ ⊔ (z ⊓ y⇧T)⇧+ * (z ⊓ y)⇧+"
using comp_isotone semiring.add_right_mono star_isotone by auto
also have "... ≤ y⇧+ ⊔ y⇧T⇧+ ⊔ (z ⊓ y⇧T)⇧+ * (z ⊓ y)⇧+"
using comp_isotone semiring.add_left_mono semiring.add_right_mono star_isotone by auto
also have "... ≤ -1 ⊔ (z ⊓ y⇧T)⇧+ * (z ⊓ y)⇧+"
by (smt 1 conv_complement conv_isotone conv_plus_commute inf.absorb2 inf.orderE order_conv_closed order_one_closed semiring.add_right_mono sup.absorb1)
also have "... = -1"
proof -
have "(z ⊓ y⇧T)⇧+ * (z ⊓ y)⇧+ ≤ (z ⊓ y⇧T) * top * (z ⊓ y)⇧+"
using comp_isotone by auto
also have "... ≤ (z ⊓ y⇧T) * top * (z ⊓ y)"
by (metis inf.eq_refl star.circ_left_top star_plus mult_assoc)
also have "... ≤ -1"
by (metis 4 bot_least comp_commute_below_diversity inf.absorb2 pseudo_complement schroeder_1 mult_assoc)
finally show ?thesis
using sup.absorb1 by blast
qed
finally show "acyclic z"
by simp
qed
thus "acyclic_1 x ∧ injectively_orientable x"
using 1 injectively_orientable_def acyclic_asymmetric by blast
next
assume "acyclic_1 x ∧ injectively_orientable x"
thus "acyclic_6 x"
using acyclic_6_def acyclic_1_def injectively_orientable_def by auto
qed

lemma acyclic_6_symmetric:
"acyclic_6 x ⟹ symmetric x"
by (simp add: acyclic_6_1_injectively_orientable injectively_orientable_orientable orientable_symmetric)

lemma acyclic_6_irreflexive:
"acyclic_6 x ⟹ irreflexive x"
by (simp add: acyclic_6_1_injectively_orientable injectively_orientable_orientable orientable_irreflexive)

lemma acyclic_4_irreflexive:
"acyclic_4 x ⟹ irreflexive x"
by (metis acyclic_4_def bot_least inf.absorb2 inf.sup_monoid.add_assoc p_bot pseudo_complement star.circ_reflexive)

text ‹Theorem 6.4›

lemma acyclic_2_implies_1:
"acyclic_2 x ⟹ acyclic_1 x"
using acyclic_2_def acyclic_1_def by auto

text ‹Theorem 8›

lemma acyclic_4a_4b:
"acyclic_4a x ⟷ acyclic_4b x"
using acyclic_4a_def acyclic_4b_def eq_iff star.circ_increasing by auto

text ‹Theorem 7›

lemma acyclic_3a_3b:
"acyclic_3a x ⟷ acyclic_3b x"
by (metis acyclic_3a_def acyclic_3b_def antisym star.circ_increasing star_involutive star_isotone)

text ‹Theorem 7›

lemma acyclic_3a_3c:
assumes "irreflexive x"
shows "acyclic_3a x ⟷ acyclic_3c x"
proof
assume "acyclic_3a x"
thus "acyclic_3c x"
by (meson acyclic_3a_def acyclic_3c_def order_lesseq_imp star.left_plus_below_circ)
next
assume 1: "acyclic_3c x"
show "acyclic_3a x"
proof (unfold acyclic_3a_def, rule allI, rule impI)
fix y
assume "y ≤ x ∧ x ≤ y⇧⋆"
hence "y ≤ x ∧ x ≤ y⇧+"
by (metis assms inf.order_lesseq_imp le_infI p_inf_sup_below star_left_unfold_equal)
thus "y = x"
using 1 acyclic_3c_def by blast
qed
qed

text ‹Theorem 7›

lemma acyclic_3c_3d:
shows "acyclic_3c x ⟷ acyclic_3d x"
proof -
have "⋀y z . y ≤ z ∧ z ≤ y⇧+ ⟷ y ≤ z ∧ y⇧+ = z⇧+"
apply (rule iffI)
apply (smt comp_associative plus_sup star.circ_transitive_equal star.left_plus_circ sup_absorb1 sup_absorb2)
by (simp add: star.circ_mult_increasing)
thus ?thesis
by (simp add: acyclic_3c_def acyclic_3d_def)
qed

text ‹Theorem 8›

lemma acyclic_4a_implies_3a:
"acyclic_4a x ⟹ acyclic_3a x"
using acyclic_4a_def acyclic_3a_def inf.absorb1 by auto

lemma acyclic_4a_implies_4:
"acyclic_4a x ⟹ acyclic_4 x"
by (simp add: acyclic_4_def acyclic_4a_4b acyclic_4b_def pp_increasing)

lemma acyclic_4b_implies_4c:
"acyclic_4b x ⟹ acyclic_4c x"
by (simp add: acyclic_4b_def acyclic_4c_def inf.sup_relative_same_increasing)

text ‹Theorem 8.5›

lemma acyclic_4_implies_2:
assumes "symmetric x"
shows "acyclic_4 x ⟹ acyclic_2 x"
proof -
assume 1: "acyclic_4 x"
show "acyclic_2 x"
proof (unfold acyclic_2_def, rule allI, rule impI)
fix y
assume 2: "y ≤ x ∧ asymmetric y"
hence "y⇧T ≤ x ⊓ -y"
using assms conv_inf_bot_iff conv_isotone pseudo_complement by force
hence "y⇧⋆ ⊓ y⇧T ≤ y⇧⋆ ⊓ x ⊓ -y"
using dual_order.trans by auto
also have "... ≤ --y ⊓ -y"
using 1 2 by (metis inf.commute acyclic_4_def comp_inf.mult_left_isotone)
finally show "acyclic y"
by (simp add: acyclic_star_below_complement_1 le_bot)
qed
qed

text ‹Theorem 10.3›

lemma acyclic_6_implies_4a:
"acyclic_6 x ⟹ acyclic_4a x"
proof -
assume "acyclic_6 x"
from this obtain y where 1: "y ⊔ y⇧T = x ∧ acyclic y ∧ injective y"
using acyclic_6_def by auto
show "acyclic_4a x"
proof (unfold acyclic_4a_def, rule allI, rule impI)
fix z
assume "z ≤ x"
hence "z = (z ⊓ y) ⊔ (z ⊓ y⇧T)"
using 1 by (metis inf.orderE inf_sup_distrib1)
hence 2: "z⇧⋆ = (z ⊓ y⇧T)⇧⋆ * (z ⊓ y)⇧⋆"
using 1 by (metis cancel_separate_2)
hence "x ⊓ z⇧⋆ = (y ⊓ (z ⊓ y⇧T)⇧⋆ * (z ⊓ y)⇧⋆) ⊔ (y⇧T ⊓ (z ⊓ y⇧T)⇧⋆ * (z ⊓ y)⇧⋆)"
using 1 inf_sup_distrib2 by auto
also have "... ≤ z"
proof (rule sup_least)
have "y ⊓ (z ⊓ y⇧T)⇧⋆ * (z ⊓ y)⇧⋆ = (y ⊓ (z ⊓ y⇧T)⇧⋆) ⊔ (y ⊓ z⇧⋆ * (z ⊓ y))"
using 2 by (metis inf_sup_distrib1 star.circ_back_loop_fixpoint sup_commute)
also have "... ≤ (y ⊓ y⇧T⇧⋆) ⊔ (y ⊓ z⇧⋆ * (z ⊓ y))"
using inf.sup_right_isotone semiring.add_right_mono star_isotone by auto
also have "... = y ⊓ z⇧⋆ * (z ⊓ y)"
using 1 by (metis acyclic_star_below_complement bot_least inf.sup_monoid.add_commute pseudo_complement sup.absorb2)
also have "... ≤ (z⇧⋆ ⊓ y * (z ⊓ y)⇧T) * (z ⊓ y)"
using dedekind_2 inf_commute by auto
also have "... ≤ y * y⇧T * z"
by (simp add: conv_isotone inf.coboundedI2 mult_isotone)
also have "... ≤ z"
using 1 mult_left_isotone by fastforce
finally show "y ⊓ (z ⊓ y⇧T)⇧⋆ * (z ⊓ y)⇧⋆ ≤ z"
.
have "y⇧T ⊓ (z ⊓ y⇧T)⇧⋆ * (z ⊓ y)⇧⋆ = (y⇧T ⊓ (z ⊓ y)⇧⋆) ⊔ (y⇧T ⊓ (z ⊓ y⇧T) * z⇧⋆)"
using 2 by (metis inf_sup_distrib1 star.circ_loop_fixpoint sup_commute)
also have "... ≤ (y⇧T ⊓ y⇧⋆) ⊔ (y⇧T ⊓ (z ⊓ y⇧T) * z⇧⋆)"
using inf.sup_right_isotone semiring.add_right_mono star_isotone by auto
also have "... = y⇧T ⊓ (z ⊓ y⇧T) * z⇧⋆"
using 1 acyclic_star_below_complement_1 inf_commute by auto
also have "... ≤ (z ⊓ y⇧T) * (z⇧⋆ ⊓ (z ⊓ y⇧T)⇧T * y⇧T)"
using dedekind_1 inf_commute by auto
also have "... ≤ z * y * y⇧T"
by (simp add: comp_associative comp_isotone conv_dist_inf inf.coboundedI2)
also have "... ≤ z"
using 1 mult_right_isotone mult_assoc by fastforce
finally show "y⇧T ⊓ (z ⊓ y⇧T)⇧⋆ * (z ⊓ y)⇧⋆ ≤ z"
.
qed
finally show "x ⊓ z⇧⋆ ≤ z"
.
qed
qed

text ‹Theorem 1.10›

lemma top_injective_inf_complement:
assumes "injective x"
shows "top * (x ⊓ y) ⊓ top * (x ⊓ -y) = bot"
proof -
have "(x ⊓ -y) * (x⇧T ⊓ y⇧T) ≤ -1"
by (metis conv_dist_inf inf.cobounded2 inf_left_idem mult_left_one p_shunting_swap schroeder_4_p)
hence "(x ⊓ -y) * (x⇧T ⊓ y⇧T) = bot"
by (smt assms comp_isotone coreflexive_comp_inf coreflexive_idempotent coreflexive_symmetric dual_order.trans inf.cobounded1 strict_order_var)
thus ?thesis
by (simp add: conv_dist_inf schroeder_2 mult_assoc)
qed

lemma top_injective_inf_complement_2:
assumes "injective x"
shows "(x⇧T ⊓ y) * top ⊓ (x⇧T ⊓ -y) * top = bot"
by (smt assms top_injective_inf_complement conv_dist_comp conv_dist_inf conv_involutive conv_complement conv_top conv_bot)

text ‹Theorem 10.3›

lemma acyclic_6_implies_5a:
"acyclic_6 x ⟹ acyclic_5a x"
proof -
assume "acyclic_6 x"
from this obtain y where 1: "y ⊔ y⇧T = x ∧ acyclic y ∧ injective y"
using acyclic_6_def by auto
show "acyclic_5a x"
proof (unfold acyclic_5a_def, rule allI, rule impI)
fix z
assume "z ≤ x"
hence 2: "z = (z ⊓ y) ⊔ (z ⊓ y⇧T)"
by (metis 1 inf.orderE inf_sup_distrib1)
hence 3: "z⇧⋆ = (z ⊓ y⇧T)⇧⋆ * (z ⊓ y)⇧⋆"
by (metis 1 cancel_separate_2)
have "(x ⊓ -z)⇧⋆ = ((y ⊓ -z) ⊔ (y⇧T ⊓ -z))⇧⋆"
using 1 inf_sup_distrib2 by auto
also have "... = (y⇧T ⊓ -z)⇧⋆ * (y ⊓ -z)⇧⋆"
using 1 cancel_separate_2 inf_commute by auto
finally have "z⇧⋆ ⊓ (x ⊓ -z)⇧⋆ = (y⇧T ⊓ z)⇧⋆ * (y ⊓ z)⇧⋆ ⊓ (y⇧T ⊓ -z)⇧⋆ * (y ⊓ -z)⇧⋆"
using 3 inf_commute by simp
also have "... = ((y ⊓ z)⇧⋆ ⊓ (y⇧T ⊓ -z)⇧⋆ * (y ⊓ -z)⇧⋆) ⊔ ((y⇧T ⊓ z)⇧+ * (y ⊓ z)⇧⋆ ⊓ (y⇧T ⊓ -z)⇧⋆ * (y ⊓ -z)⇧⋆)"
by (smt inf.sup_monoid.add_commute inf_sup_distrib1 star.circ_loop_fixpoint sup_commute mult_assoc)
also have "... = (1 ⊓ (y⇧T ⊓ -z)⇧⋆ * (y ⊓ -z)⇧⋆) ⊔ ((y ⊓ z)⇧+ ⊓ (y⇧T ⊓ -z)⇧⋆ * (y ⊓ -z)⇧⋆) ⊔ ((y⇧T ⊓ z)⇧+ * (y ⊓ z)⇧⋆ ⊓ (y⇧T ⊓ -z)⇧⋆ * (y ⊓ -z)⇧⋆)"
by (metis inf_sup_distrib2 star_left_unfold_equal)
also have "... ≤ 1"
proof (intro sup_least)
show "1 ⊓ (y⇧T ⊓ -z)⇧⋆ * (y ⊓ -z)⇧⋆ ≤ 1"
by simp
have "(y ⊓ z)⇧+ ⊓ (y⇧T ⊓ -z)⇧⋆ * (y ⊓ -z)⇧⋆ = ((y ⊓ z)⇧+ ⊓ (y⇧T ⊓ -z)⇧⋆) ⊔ ((y ⊓ z)⇧+ ⊓ (y⇧T ⊓ -z)⇧⋆ * (y ⊓ -z)⇧+)"
by (metis inf_sup_distrib1 star.circ_back_loop_fixpoint star.circ_plus_same sup_commute mult_assoc)
also have "... ≤ bot"
proof (rule sup_least)
have "(y ⊓ z)⇧+ ⊓ (y⇧T ⊓ -z)⇧⋆ ≤ y⇧+ ⊓ y⇧T⇧⋆"
by (meson comp_inf.mult_isotone comp_isotone inf.cobounded1 star_isotone)
also have "... = bot"
using 1 by (smt acyclic_star_inf_conv inf.orderE inf.sup_monoid.add_assoc pseudo_complement star.left_plus_below_circ)
finally show "(y ⊓ z)⇧+ ⊓ (y⇧T ⊓ -z)⇧⋆ ≤ bot"
.
have "(y ⊓ z)⇧+ ⊓ (y⇧T ⊓ -z)⇧⋆ * (y ⊓ -z)⇧+ ≤ top * (y ⊓ z) ⊓ top * (y ⊓ -z)"
by (metis comp_associative comp_inf.mult_isotone star.circ_left_top star.circ_plus_same top_left_mult_increasing)
also have "... = bot"
using 1 by (simp add: top_injective_inf_complement)
finally show "(y ⊓ z)⇧+ ⊓ (y⇧T ⊓ -z)⇧⋆ * (y ⊓ -z)⇧+ ≤ bot"
.
qed
finally show "(y ⊓ z)⇧+ ⊓ (y⇧T ⊓ -z)⇧⋆ * (y ⊓ -z)⇧⋆ ≤ 1"
using bot_least le_bot by blast
have "(y⇧T ⊓ z)⇧+ * (y ⊓ z)⇧⋆ ⊓ (y⇧T ⊓ -z)⇧⋆ * (y ⊓ -z)⇧⋆ = ((y⇧T ⊓ z)⇧+ * (y ⊓ z)⇧⋆ ⊓ (y ⊓ -z)⇧⋆) ⊔ ((y⇧T ⊓ z)⇧+ * (y ⊓ z)⇧⋆ ⊓ (y⇧T ⊓ -z)⇧+ * (y ⊓ -z)⇧⋆)"
by (metis inf_sup_distrib1 star.circ_loop_fixpoint sup_commute mult_assoc)
also have "... = ((y⇧T ⊓ z)⇧+ * (y ⊓ z)⇧⋆ ⊓ 1) ⊔ ((y⇧T ⊓ z)⇧+ * (y ⊓ z)⇧⋆ ⊓ (y ⊓ -z)⇧+) ⊔ ((y⇧T ⊓ z)⇧+ * (y ⊓ z)⇧⋆ ⊓ (y⇧T ⊓ -z)⇧+ * (y ⊓ -z)⇧⋆)"
by (metis inf_sup_distrib1 star_left_unfold_equal)
also have "... ≤ 1"
proof (intro sup_least)
show "(y⇧T ⊓ z)⇧+ * (y ⊓ z)⇧⋆ ⊓ 1 ≤ 1"
by simp
have "(y⇧T ⊓ z)⇧+ * (y ⊓ z)⇧⋆ ⊓ (y ⊓ -z)⇧+ = ((y⇧T ⊓ z)⇧+ ⊓ (y ⊓ -z)⇧+) ⊔ ((y⇧T ⊓ z)⇧+ * (y ⊓ z)⇧+ ⊓ (y ⊓ -z)⇧+)"
by (smt inf.sup_monoid.add_commute inf_sup_distrib1 star.circ_back_loop_fixpoint star.circ_plus_same sup_commute mult_assoc)
also have "... ≤ bot"
proof (rule sup_least)
have "(y⇧T ⊓ z)⇧+ ⊓ (y ⊓ -z)⇧+ ≤ y⇧T⇧+ ⊓ y⇧+"
by (meson comp_inf.mult_isotone comp_isotone inf.cobounded1 star_isotone)
also have "... = bot"
using 1 by (metis acyclic_asymmetric conv_inf_bot_iff conv_plus_commute star_sup_1 sup.idem mult_assoc)
finally show "(y⇧T ⊓ z)⇧+ ⊓ (y ⊓ -z)⇧+ ≤ bot"
.
have "(y⇧T ⊓ z)⇧+ * (y ⊓ z)⇧+ ⊓ (y ⊓ -z)⇧+ ≤ top * (y ⊓ z) ⊓ top * (y ⊓ -z)"
by (smt comp_inf.mult_isotone comp_isotone inf.cobounded1 inf.orderE star.circ_plus_same top.extremum mult_assoc)
also have "... = bot"
using 1 by (simp add: top_injective_inf_complement)
finally show "(y⇧T ⊓ z)⇧+ * (y ⊓ z)⇧+ ⊓ (y ⊓ -z)⇧+ ≤ bot"
.
qed
finally show "(y⇧T ⊓ z)⇧+ * (y ⊓ z)⇧⋆ ⊓ (y ⊓ -z)⇧+ ≤ 1"
using bot_least le_bot by blast
have "(y⇧T ⊓ z)⇧+ * (y ⊓ z)⇧⋆ ⊓ (y⇧T ⊓ -z)⇧+ * (y ⊓ -z)⇧⋆ ≤ (y⇧T ⊓ z) * top ⊓ (y⇧T ⊓ -z) * top"
by (smt comp_inf.mult_isotone comp_isotone eq_iff top.extremum mult_assoc)
also have "... = bot"
using 1 by (simp add: top_injective_inf_complement_2)
finally show "(y⇧T ⊓ z)⇧+ * (y ⊓ z)⇧⋆ ⊓ (y⇧T ⊓ -z)⇧+ * (y ⊓ -z)⇧⋆ ≤ 1"
using bot_least le_bot by blast
qed
finally show "(y⇧T ⊓ z)⇧+ * (y ⊓ z)⇧⋆ ⊓ (y⇧T ⊓ -z)⇧⋆ * (y ⊓ -z)⇧⋆ ≤ 1"
.
qed
finally show "z⇧⋆ ⊓ (x ⊓ -z)⇧⋆ = 1"
by (simp add: antisym star.circ_reflexive)
qed
qed

text ‹Theorem 9.7›

lemma acyclic_5b_implies_4:
assumes "irreflexive x"
and "acyclic_5b x"
shows "acyclic_4 x"
proof (unfold acyclic_4_def, rule allI, rule impI)
fix y
assume "y ≤ x"
hence "y⇧⋆ ⊓ (x ⊓ -y)⇧+ ≤ 1"
using acyclic_5b_def assms(2) by blast
hence "y⇧⋆ ⊓ x ⊓ -y ≤ 1"
by (smt inf.sup_left_divisibility inf.sup_monoid.add_assoc star.circ_mult_increasing)
hence "y⇧⋆ ⊓ x ⊓ -y = bot"
by (smt assms(1) comp_inf.semiring.mult_zero_left inf.orderE inf.sup_monoid.add_assoc inf.sup_monoid.add_commute pseudo_complement)
thus "x ⊓ y⇧⋆ ≤ --y"
using inf.sup_monoid.add_commute pseudo_complement by fastforce
qed

text ‹Theorem 9›

lemma acyclic_5a_5b:
"acyclic_5a x ⟷ acyclic_5b x"
by (simp add: acyclic_5a_def acyclic_5b_def star.circ_reflexive reflexive_inf_plus_star)

text ‹Theorem 9›

lemma acyclic_5a_5c:
"acyclic_5a x ⟷ acyclic_5c x"
by (metis acyclic_5a_def acyclic_5c_def inf_commute star.circ_reflexive reflexive_inf_plus_star)

text ‹Theorem 9›

lemma acyclic_5b_5d:
"acyclic_5b x ⟷ acyclic_5d x"
proof -
have "acyclic_5b x ⟷ (∀y . y ≤ x ⟶ (y⇧+ ⊔ 1) ⊓ (x ⊓ -y)⇧+ ≤ 1)"
by (simp add: acyclic_5b_def star_left_unfold_equal sup_commute)
also have "... ⟷ acyclic_5d x"
by (simp add: inf_sup_distrib2 acyclic_5d_def)
finally show ?thesis
.
qed

lemma acyclic_5a_5e:
"acyclic_5a x ⟷ acyclic_5e x"
proof
assume 1: "acyclic_5a x"
show "acyclic_5e x"
proof (unfold acyclic_5e_def, intro allI, rule impI)
fix y z
assume 2: "y ≤ x ∧ z ≤ x ∧ y ⊓ z = bot"
hence "z ≤ x ⊓ -y"
using p_antitone_iff pseudo_complement by auto
hence "y⇧⋆ ⊓ z⇧⋆ ≤ 1"
using 1 2 by (metis acyclic_5a_def comp_inf.mult_isotone inf.cobounded1 inf.right_idem star_isotone)
thus "y⇧⋆ ⊓ z⇧⋆ = 1"
by (simp add: antisym star.circ_reflexive)
qed
next
assume 1: "acyclic_5e x"
show "acyclic_5a x"
proof (unfold acyclic_5a_def, rule allI, rule impI)
fix y
let ?z = "x ⊓ -y"
assume 2: "y ≤ x"
have "y ⊓ ?z = bot"
by (simp add: inf.left_commute)
thus "y⇧⋆ ⊓ ?z⇧⋆ = 1"
using 1 2 by (simp add: acyclic_5e_def)
qed
qed

text ‹Theorem 9›

lemma acyclic_5e_5f:
"acyclic_5e x ⟷ acyclic_5f x"
by (simp add: acyclic_5e_def acyclic_5f_def)

lemma acyclic_5e_down_closed:
assumes "x ≤ y"
and "acyclic_5e y"
shows "acyclic_5e x"
using assms acyclic_5e_def order.trans by blast

lemma acyclic_5a_down_closed:
assumes "x ≤ y"
and "acyclic_5a y"
shows "acyclic_5a x"
using acyclic_5e_down_closed assms acyclic_5a_5e by blast

text ‹further variants of the existence of a linear order›

abbreviation "linear_orderable_4 x ≡ transitive x ∧ acyclic x ∧ strict_linear x"
abbreviation "linear_orderable_5 x ≡ transitive x ∧ acyclic x ∧ linear (x⇧⋆)"
abbreviation "linear_orderable_6 x ≡ acyclic x ∧ linear (x⇧⋆)"
abbreviation "linear_orderable_7 x ≡ split 1 (x⇧⋆) top"
abbreviation "linear_orderable_8 x ≡ split bot (x⇧+) (-1)"

lemma linear_orderable_3_4:
"linear_orderable_3 x ⟷ linear_orderable_4 x"
using transitive_acyclic_asymmetric by blast

lemma linear_orderable_5_implies_6:
"linear_orderable_5 x ⟹ linear_orderable_6 x"
by simp

lemma linear_orderable_6_implies_3:
assumes "linear_orderable_6 x"
shows "linear_orderable_3 (x⇧+)"
proof -
have 1: "transitive (x⇧+)"
by (simp add: comp_associative mult_isotone star.circ_mult_upper_bound star.left_plus_below_circ)
have 2: "asymmetric (x⇧+)"
by (simp add: assms acyclic_asymmetric star.circ_transitive_equal star.left_plus_circ mult_assoc)
have 3: "strict_linear (x⇧+)"
by (smt assms acyclic_star_inf_conv conv_star_commute inf.sup_monoid.add_commute inf_absorb2 maddux_3_13 orientable_11_implies_12 star_left_unfold_equal)
show ?thesis
using 1 2 3 by simp
qed

lemma linear_orderable_7_implies_1:
"linear_orderable_7 x ⟹ linear_orderable_1 (x⇧⋆)"
using star.circ_transitive_equal by auto

lemma linear_orderable_6_implies_8:
"linear_orderable_6 x ⟹ linear_orderable_8 x"
by (simp add: linear_orderable_6_implies_3)

abbreviation "path_orderable x ≡ univalent x ∧ injective x ∧ acyclic x ∧ linear (x⇧⋆)"

lemma path_orderable_implies_linear_orderable_6:
"path_orderable x ⟹ linear_orderable_6 x"
by simp

definition "simple_paths x ≡ ∃y . y ⊔ y⇧T = x ∧ acyclic y ∧ injective y ∧ univalent y"

text ‹Theorem 14.1›

lemma simple_paths_acyclic_6:
"simple_paths x ⟹ acyclic_6 x"
using simple_paths_def acyclic_6_def by blast

text ‹Theorem 14.2›

lemma simple_paths_transitively_orientable:
assumes "simple_paths x"
shows "transitively_orientable (x⇧+ ⊓ -1)"
proof -
from assms obtain y where 1: "y ⊔ y⇧T = x ∧ acyclic y ∧ injective y ∧ univalent y"
using simple_paths_def by auto
let ?y = "y⇧+"
have 2: "transitive ?y"
by (simp add: comp_associative mult_right_isotone star.circ_mult_upper_bound star.left_plus_below_circ)
have 3: "asymmetric ?y"
using 1 acyclic_plus_asymmetric by auto
have "?y ⊔ ?y⇧T = x⇧+ ⊓ -1"
proof (rule antisym)
have 4: "?y ≤ x⇧+"
using 1 comp_isotone star_isotone by auto
hence "?y⇧T ≤ x⇧+"
using 1 by (metis conv_dist_sup conv_involutive conv_order conv_plus_commute sup_commute)
thus "?y ⊔ ?y⇧T ≤ x⇧+ ⊓ -1"
using 1 4 by (simp add: irreflexive_conv_closed)
have "x⇧+ ≤ y⇧⋆ ⊔ y⇧⋆⇧T"
using 1 by (metis cancel_separate_1_sup conv_star_commute star.left_plus_below_circ)
also have "... = ?y ⊔ ?y⇧T ⊔ 1"
by (smt conv_plus_commute conv_star_commute star.circ_reflexive star_left_unfold_equal sup.absorb1 sup_assoc sup_monoid.add_commute)
finally show "x⇧+ ⊓ -1 ≤ ?y ⊔ ?y⇧T"
by (metis inf.order_lesseq_imp inf.sup_monoid.add_commute inf.sup_right_isotone p_inf_sup_below sup_commute)
qed
thus ?thesis
using 2 3 transitively_orientable_def by auto
qed

abbreviation "spanning x y ≡ y ≤ x ∧ x ≤ (y ⊔ y⇧T)⇧⋆ ∧ acyclic y ∧ injective y"
definition "spannable x ≡ ∃y . spanning x y"

lemma acyclic_6_implies_spannable:
"acyclic_6 x ⟹ spannable x"
by (metis acyclic_6_def star.circ_increasing sup.cobounded1 spannable_def)

lemma acyclic_3a_spannable_implies_6:
assumes "acyclic_3a x"
and "spannable x"
and "symmetric x"
shows "acyclic_6 x"
by (smt acyclic_6_def acyclic_3a_def assms conv_isotone le_supI spannable_def)

text ‹Theorem 10.3›

lemma acyclic_6_implies_3a:
"acyclic_6 x ⟹ acyclic_3a x"
by (simp add: acyclic_6_implies_4a acyclic_4a_implies_3a)

text ‹Theorem 10.3›

lemma acyclic_6_implies_2:
"acyclic_6 x ⟹ acyclic_2 x"
by (simp add: acyclic_6_implies_4a acyclic_6_symmetric acyclic_4_implies_2 acyclic_4a_implies_4)

text ‹Theorem 11›

lemma acyclic_6_3a_spannable:
"acyclic_6 x ⟷ symmetric x ∧ spannable x ∧ acyclic_3a x"
using acyclic_6_implies_3a acyclic_3a_spannable_implies_6 acyclic_6_implies_spannable acyclic_6_symmetric by blast

end

context stone_kleene_relation_algebra
begin

text ‹Theorem 11.3›

lemma point_spanning:
assumes "point p"
shows "spanning (-1) (p ⊓ -1)"
"spannable (-1)"
proof -
let ?y = "p ⊓ -1"
have 1: "injective ?y"
by (simp add: assms injective_inf_closed)
have "?y * ?y ≤ -1"
using assms cancel_separate_5 inf.sup_monoid.add_commute vector_inf_comp by auto
hence 2: "transitive ?y"
by (simp add: assms vector_inf_comp)
hence 3: "acyclic ?y"
by (simp add: transitive_acyclic_irreflexive)
have 4: "p ≤ ?y ⊔ 1"
by (simp add: regular_complement_top sup_commute sup_inf_distrib1)
have "top = p⇧T * p"
using assms inf.eq_iff shunt_bijective top_greatest vector_conv_covector by blast
also have "... ≤ (?y ⊔ 1)⇧T * (?y ⊔ 1)"
using 4 by (simp add: conv_isotone mult_isotone)
also have "... = (?y ⊔ ?y⇧T)⇧⋆"
using 1 2 by (smt antisym cancel_separate_1 conv_star_commute star.circ_mult_1 star.circ_mult_increasing star.right_plus_circ star_right_induct_mult sup_commute)
finally have "-1 ≤ (?y ⊔ ?y⇧T)⇧⋆"
using top.extremum top_le by blast
thus "spanning (-1) (p ⊓ -1)"
using 1 3 inf.cobounded2 by blast
thus "spannable (-1)"
using spannable_def by blast
qed

(* move to Kleene_Relation_Algebras *)
lemma irreflexive_star:
"(x ⊓ -1)⇧⋆ = x⇧⋆"
proof -
have 1: "x ⊓ 1 ≤ (x ⊓ -1)⇧⋆"
by (simp add: le_infI2 star.circ_reflexive)
have "x ⊓ -1 ≤ (x ⊓ -1)⇧⋆"
by (simp add: star.circ_increasing)
hence "x ≤ (x ⊓ -1)⇧⋆"
using 1 by (smt maddux_3_11_pp regular_one_closed sup.absorb_iff1 sup_assoc)
thus ?thesis
by (metis antisym inf.cobounded1 star_involutive star_isotone)
qed

text ‹Theorem 6.5›

lemma acyclic_2_1:
assumes "orientable x"
shows "acyclic_2 x ⟷ acyclic_1 x"
proof
assume "acyclic_2 x"
thus "acyclic_1 x"
using acyclic_2_implies_1 by blast
next
assume 1: "acyclic_1 x"
obtain y where 2: "orientation x y ∧ symmetric x"
using assms orientable_def orientable_symmetric by blast
show "acyclic_2 x"
proof (unfold acyclic_2_def, rule allI, rule impI)
fix z
assume 3: "z ≤ x ∧ asymmetric z"
let ?z = "(--z ⊓ x) ⊔ (-(z ⊔ z⇧T) ⊓ y)"
have "orientation x ?z"
proof
have "?z ⊔ ?z⇧T = ((--z ⊔ --z⇧T) ⊓ x) ⊔ (-(z ⊔ z⇧T) ⊓ (y ⊔ y⇧T))"
by (smt 2 3 comp_inf.semiring.combine_common_factor conv_complement conv_dist_inf conv_dist_sup inf_sup_distrib1 orientation_symmetric sup.left_commute sup_assoc)
also have "... = x"
by (metis 2 inf_commute maddux_3_11_pp pp_dist_sup sup_monoid.add_commute)
finally show "?z ⊔ ?z⇧T = x"
.
have "?z ⊓ ?z⇧T = ((--z ⊓ x) ⊔ (-(z ⊔ z⇧T) ⊓ y)) ⊓ ((--z⇧T ⊓ x) ⊔ (-(z ⊔ z⇧T) ⊓ y⇧T))"
by (simp add: 2 conv_complement conv_dist_inf conv_dist_sup inf.sup_monoid.add_commute)
also have "... = ((--z ⊓ x) ⊓ (--z⇧T ⊓ x)) ⊔ ((--z ⊓ x) ⊓ (-(z ⊔ z⇧T) ⊓ y⇧T)) ⊔ ((-(z ⊔ z⇧T) ⊓ y) ⊓ (--z⇧T ⊓ x)) ⊔ ((-(z ⊔ z⇧T) ⊓ y) ⊓ (-(z ⊔ z⇧T) ⊓ y⇧T))"
by (smt comp_inf.semiring.distrib_left inf_sup_distrib2 sup_assoc)
also have "... = bot"
by (smt 2 3 inf.cobounded1 inf.left_commute inf.orderE p_dist_sup pseudo_complement sup.absorb_iff1)
finally show "?z ⊓ ?z⇧T = bot"
.
qed
hence 4: "acyclic ?z"
using 1 acyclic_1_def by auto
have "z ≤ ?z"
by (simp add: 3 le_supI1 pp_increasing)
thus "acyclic z"
using 4 comp_isotone star_isotone by fastforce
qed
qed

text ‹Theorem 8›

lemma acyclic_4_4c:
"acyclic_4 x ⟷ acyclic_4c x"
proof
assume 1: "acyclic_4 x"
show "acyclic_4c x"
proof (unfold acyclic_4c_def, rule allI, rule impI)
fix y
assume 2: "y ≤ x"
have "x ⊓ (x ⊓ -y)⇧⋆ ≤ --(x ⊓ -y)"
using 1 acyclic_4_def inf.cobounded1 by blast
also have "... ≤ -y"
by simp
finally have "x ⊓ y ⊓ (x ⊓ -y)⇧⋆ = bot"
by (simp add: p_shunting_swap pseudo_complement)
thus "y ⊓ (x ⊓ -y)⇧⋆ = bot"
using 2 inf_absorb2 by auto
qed
next
assume 3: "acyclic_4c x"
show "acyclic_4 x"
proof (unfold acyclic_4_def, rule allI, rule impI)
fix y
assume 4: "y ≤ x"
have "x ⊓ -y ⊓ (x ⊓ -(x ⊓ -y))⇧⋆ = bot"
using 3 acyclic_4c_def inf_le1 by blast
hence "x ⊓ -y ⊓ (x ⊓ --y)⇧⋆ = bot"
using inf_import_p by auto
hence "x ⊓ -y ⊓ (x ⊓ y)⇧⋆ = bot"
by (smt p_inf_pp pp_dist_star pp_pp_inf_bot_iff)
hence "x ⊓ -y ⊓ y⇧⋆ = bot"
using 4 inf_absorb2 by auto
thus "x ⊓ y⇧⋆ ≤ --y"
using p_shunting_swap pseudo_complement by auto
qed
qed

text ‹Theorem 9›

lemma acyclic_5f_5g:
"acyclic_5f x ⟷ acyclic_5g x"
proof
assume "acyclic_5f x"
thus "acyclic_5g x"
using acyclic_5f_def acyclic_5g_def by auto
next
assume 1: "acyclic_5g x"
show "acyclic_5f x"
proof (unfold acyclic_5f_def, intro allI, rule impI)
fix y z
let ?y = "x ⊓ --y"
let ?z = "x ⊓ -y"
assume "y ⊔ z ≤ x ∧ y ⊓ z = bot"
hence "y ≤ ?y ∧ z ≤ ?z"
using inf.sup_monoid.add_commute pseudo_complement by fastforce
hence "y⇧⋆ ⊓ z⇧⋆ ≤ ?y⇧⋆ ⊓ ?z⇧⋆"
using comp_inf.mult_isotone star_isotone by blast
also have "... = 1"
finally show "y⇧⋆ ⊓ z⇧⋆ = 1"
by (simp add: antisym star.circ_reflexive)
qed
qed

lemma linear_orderable_3_implies_5:
assumes "linear_orderable_3 x"
shows "linear_orderable_5 x"
proof -
have "top = x ⊔ x⇧T ⊔ 1"
using assms conv_dist_sup orientable_12_implies_11 sup_assoc sup_commute by fastforce
also have "... ≤ x⇧⋆ ⊔ x⇧⋆⇧T"
by (smt conv_star_commute star.circ_increasing star_sup_one sup_assoc sup_commute sup_mono)
finally show ?thesis
by (simp add: assms top_le transitive_acyclic_asymmetric)
qed

lemma linear_orderable_8_implies_7:
"linear_orderable_8 x ⟹ linear_orderable_7 x"
using orientable_12_implies_11 star_left_unfold_equal sup_commute by fastforce

text ‹Theorem 13›

lemma exists_split_characterisations_2:
shows "(∃x . linear_orderable_1 x) ⟷ (∃x . linear_orderable_4 x)"
and "(∃x . linear_orderable_1 x) ⟷ (∃x . linear_orderable_5 x)"
and "(∃x . linear_orderable_1 x) ⟷ (∃x . linear_orderable_6 x)"
and "(∃x . linear_orderable_1 x) ⟷ (∃x . linear_orderable_7 x)"
and "(∃x . linear_orderable_1 x) ⟷ (∃x . linear_orderable_8 x)"
subgoal 1 using exists_split_characterisations(1) strict_order_transitive_acyclic by auto
subgoal 2 using 1 linear_orderable_3_implies_5 linear_orderable_6_implies_3 transitive_acyclic_asymmetric by auto
subgoal 3 using 2 exists_split_characterisations(1) linear_orderable_6_implies_3 by auto
subgoal using 2 linear_orderable_8_implies_7 linear_orderable_6_implies_3 linear_orderable_7_implies_1 by blast
subgoal using 3 linear_orderable_8_implies_7 asymmetric_irreflexive linear_orderable_6_implies_3 by blast
done

end

subsection ‹Arc axiom›

class stone_kleene_relation_algebra_arc = stone_kleene_relation_algebra +
assumes arc_axiom: "x ≠ bot ⟹ ∃y . arc y ∧ y ≤ --x"
begin

subclass stone_relation_algebra_tarski
proof unfold_locales
fix x
assume 1: "regular x" and 2: "x ≠ bot"
from 2 obtain y where "arc y ∧ y ≤ --x"
using arc_axiom by auto
thus "top * x * top = top"
using 1 by (metis mult_assoc le_iff_sup mult_left_isotone semiring.distrib_left sup.orderE top.extremum)
qed

context
assumes orientable_path: "arc x ⟹ x ≤ --y⇧⋆ ⟹ ∃z . z ≤ y ∧ asymmetric z ∧ x ≤ --z⇧⋆"
begin

text ‹Theorem 8.6›

lemma acyclic_2_4:
assumes "irreflexive x"
and "symmetric x"
shows "acyclic_2 x ⟷ acyclic_4 x"
proof
show "acyclic_2 x ⟹ acyclic_4 x"
proof (unfold acyclic_4_def, intro allI, intro impI, rule ccontr)
fix y
assume 1: "acyclic_2 x" and 2: "y ≤ x" and 3: "¬ x ⊓ y⇧⋆ ≤ --y"
hence "x ⊓ y⇧⋆ ⊓ -y ≠ bot"
by (simp add: pseudo_complement)
from this obtain z where 4: "arc z ∧ z ≤ --(x ⊓ y⇧⋆ ⊓ -y)"
using arc_axiom by blast
from this obtain w where 5: "w ≤ y ∧ asymmetric w ∧ z ≤ --w⇧⋆"
using orientable_path by auto
let ?y = "w ⊔ (z⇧T ⊓ x)"
have 6: "?y ≤ x"
using 2 5 by auto
have "?y ⊓ ?y⇧T = (w ⊓ w⇧T) ⊔ (w ⊓ z ⊓ x⇧T) ⊔ (z⇧T ⊓ x ⊓ w⇧T) ⊔ (z⇧T ⊓ x ⊓ z ⊓ x⇧T)"
by (simp add: inf.commute sup.commute inf.left_commute sup.left_commute conv_dist_inf conv_dist_sup inf_sup_distrib1)
also have "... ≤ bot"
proof (intro sup_least)
show "w ⊓ w⇧T ≤ bot"
by (simp add: 5)
have "w ⊓ z ⊓ x⇧T ≤ y ⊓ z"
by (simp add: 5 inf.coboundedI1)
also have "... ≤ y ⊓ -y"
using 4 by (metis eq_refl inf.cobounded1 inf.left_commute inf.sup_monoid.add_commute inf_p order_trans pseudo_complement)
finally show "w ⊓ z ⊓ x⇧T ≤ bot"
by simp
thus "z⇧T ⊓ x ⊓ w⇧T ≤ bot"
by (smt conv_dist_inf conv_inf_bot_iff inf.left_commute inf.sup_monoid.add_commute le_bot)
have "irreflexive z"
by (meson 4 assms(1) dual_order.trans irreflexive_complement_reflexive irreflexive_inf_closed reflexive_complement_irreflexive)
hence "asymmetric z"
using 4 by (simp add: pseudo_complement irreflexive_inf_arc_asymmetric)
thus "z⇧T ⊓ x ⊓ z ⊓ x⇧T ≤ bot"
qed
finally have "acyclic ?y"
using 1 6 by (simp add: le_bot acyclic_2_def)
hence "?y⇧⋆ ⊓ ?y⇧T = bot"
using acyclic_star_below_complement_1 by blast
hence "w⇧⋆ ⊓ ?y⇧T = bot"
using dual_order.trans pseudo_complement star.circ_sub_dist by blast
hence "w⇧⋆ ⊓ z ⊓ x⇧T = bot"
by (simp add: comp_inf.semiring.distrib_left conv_dist_inf conv_dist_sup inf.sup_monoid.add_assoc)
hence "z ⊓ x⇧T = bot"
using 5 by (metis comp_inf.p_pp_comp inf.absorb2 pp_pp_inf_bot_iff)
hence "z ⊓ --x = bot"
using assms(2) pseudo_complement by auto
hence "z = bot"
using 4 inf.orderE by auto
thus "False"
using 3 4 comp_inf.coreflexive_pseudo_complement inf_bot_right by auto
qed
next
show "acyclic_4 x ⟹ acyclic_2 x"
by (simp add: assms(2) acyclic_4_implies_2)
qed

end

end

context kleene_relation_algebra
begin

text ‹Theorem 8›

lemma acyclic_3a_implies_4b:
assumes "acyclic_3a x"
shows "acyclic_4b x"
proof (unfold acyclic_4b_def, rule allI, rule impI)
fix y
let ?y = "(x ⊓ -y⇧⋆) ⊔ y"
assume 1: "y ≤ x"
have "x = (x ⊓ -y⇧⋆) ⊔ (x ⊓ y⇧⋆)"
by simp
also have "... ≤ ?y ⊔ y⇧⋆"
using shunting_var by fastforce
also have "... ≤ ?y⇧⋆"
by (simp add: star.circ_increasing star.circ_sub_dist sup_commute)
finally have "?y = x"
using 1 assms acyclic_3a_def by simp
hence "x ⊓ y⇧⋆ = y ⊓ y⇧⋆"
by (smt (z3) inf.sup_monoid.add_commute inf_sup_absorb inf_sup_distrib2 maddux_3_13 sup_commute sup_inf_absorb)
thus "x ⊓ y⇧⋆ = y"
by (simp add: inf_absorb1 star.circ_increasing)
qed

lemma acyclic_3a_4b:
"acyclic_3a x ⟷ acyclic_4b x"
using acyclic_3a_implies_4b acyclic_4a_4b acyclic_4a_implies_3a by blast

lemma acyclic_4_4a:
"acyclic_4 x ⟷ acyclic_4a x"
by (simp add: acyclic_4_def acyclic_4a_def)

subsection ‹Counterexamples›

text ‹
Calls to nitpick have been put into comments to save processing time.
›

text ‹independence of (0)›

lemma "symmetric x ⟹ irreflexive_inf x ⟹ orientable x"
text ‹nitpick[expect=genuine,card=4,timeout=600]›
oops

lemma "linear_orderable_6 x ⟹ path_orderable x"
text ‹nitpick[expect=genuine,card=8,timeout=600]›
oops

text ‹(5) does not imply (6)›

lemma "symmetric x ⟹ irreflexive x ⟹ acyclic_5a x ⟹ acyclic_6 x"
text ‹nitpick[expect=genuine,card=4,timeout=600]›
oops

text ‹(2) does not imply (4)›

lemma "symmetric x ⟹ irreflexive x ⟹ acyclic_2 x ⟹ acyclic_4 x"
text ‹nitpick[expect=genuine,card=8,timeout=600]›
oops

end

end



# Theory Algorithms

(* Title:      Axioms and Algorithmic Proofs
Author:     Walter Guttmann
Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

section ‹Axioms and Algorithmic Proofs›

text ‹
In this theory we verify the correctness of three basic graph algorithms.
We use them to constructively prove a number of graph properties.
›

theory Algorithms

imports "HOL-Hoare.Hoare_Logic" Forests

begin

context stone_kleene_relation_algebra_arc
begin

text ‹
Assuming the arc axiom we can define the function ‹choose_arc› that selects an arc in a non-empty graph.
›

definition "choose_arc x ≡ if x = bot then bot else SOME y . arc y ∧ y ≤ --x"

lemma choose_arc_below:
"choose_arc x ≤ --x"
proof (cases "x = bot")
case True
thus ?thesis
using choose_arc_def by auto
next
let ?P = "λy . arc y ∧ y ≤ --x"
case False
have "?P (SOME y . ?P y)"
apply (rule someI_ex)
using someI_ex False arc_axiom by auto
thus ?thesis
using False choose_arc_def by auto
qed

lemma choose_arc_arc:
assumes "x ≠ bot"
shows "arc (choose_arc x)"
proof -
let ?P = "λy . arc y ∧ y ≤ --x"
have "?P (SOME y . ?P y)"
apply (rule someI_ex)
using someI_ex assms arc_axiom by auto
thus ?thesis
using assms choose_arc_def by auto
qed

lemma choose_arc_bot:
"choose_arc bot = bot"
by (metis bot_unique choose_arc_below regular_closed_bot)

lemma choose_arc_bot_iff:
"choose_arc x = bot ⟷ x = bot"
using covector_bot_closed inf_bot_right choose_arc_arc vector_bot_closed choose_arc_bot by fastforce

lemma choose_arc_regular:
"regular (choose_arc x)"
proof (cases "x = bot")
assume "x = bot"
thus ?thesis
by (simp add: choose_arc_bot)
next
assume "x ≠ bot"
thus ?thesis
by (simp add: arc_regular choose_arc_arc)
qed

subsection ‹Constructing a spanning tree›

definition "spanning_forest f g ≡ forest f ∧ f ≤ --g ∧ components g ≤ forest_components f ∧ regular f"
definition "kruskal_spanning_invariant f g h ≡ symmetric g ∧ h = h⇧T ∧ g ⊓ --h = h ∧ spanning_forest f (-h ⊓ g)"

lemma spanning_forest_spanning:
"spanning_forest f g ⟹ spanning (--g) f"
by (smt (z3) cancel_separate_1 order_trans star.circ_increasing spanning_forest_def)

lemma spanning_forest_spanning_regular:
assumes "regular f"
and "regular g"
shows "spanning_forest f g ⟷ spanning g f"
by (smt (z3) assms cancel_separate_1 components_increasing dual_order.trans forest_components_star star_isotone spanning_forest_def)

text ‹
We prove total correctness of Kruskal's spanning tree algorithm (ignoring edge weights) \cite{Kruskal1956}.
The algorithm and proof are adapted from the AFP theory ‹Relational_Minimum_Spanning_Trees.Kruskal› to work in Stone-Kleene relation algebras \cite{Guttmann2017c,Guttmann2018c}.
›

lemma kruskal_vc_1:
assumes "symmetric g"
shows "kruskal_spanning_invariant bot g g"
proof (unfold kruskal_spanning_invariant_def, intro conjI)
show "symmetric g"
using assms by simp
next
show "g = g⇧T"
using assms by simp
next
show "g ⊓ --g = g"
using inf.sup_monoid.add_commute selection_closed_id by simp
next
show "spanning_forest bot (-g ⊓ g)"
using star.circ_transitive_equal spanning_forest_def by simp
qed

text ‹
For the remainder of this theory we assume there are finitely many regular elements.
This means that the graphs are finite and is needed for proving termination of the algorithms.
›

context
assumes finite_regular: "finite { x . regular x }"
begin

lemma kruskal_vc_2:
assumes "kruskal_spanning_invariant f g h"
and "h ≠ bot"
shows "(choose_arc h ≤ -forest_components f ⟶ kruskal_spanning_invariant ((f ⊓ -(top * choose_arc h * f⇧T⇧⋆)) ⊔ (f ⊓ top * choose_arc h * f⇧T⇧⋆)⇧T ⊔ choose_arc h) g (h ⊓ -choose_arc h ⊓ -choose_arc h⇧T)
∧ card { x . regular x ∧ x ≤ --h ∧ x ≤ -choose_arc h ∧ x ≤ -choose_arc h⇧T } < card { x . regular x ∧ x ≤ --h }) ∧
(¬ choose_arc h ≤ -forest_components f ⟶ kruskal_spanning_invariant f g (h ⊓ -choose_arc h ⊓ -choose_arc h⇧T)
∧ card { x . regular x ∧ x ≤ --h ∧ x ≤ -choose_arc h ∧ x ≤ -choose_arc h⇧T } < card { x . regular x ∧ x ≤ --h })"
proof -
let ?e = "choose_arc h"
let ?f = "(f ⊓ -(top * ?e * f⇧T⇧⋆)) ⊔ (f ⊓ top * ?e * f⇧T⇧⋆)⇧T ⊔ ?e"
let ?h = "h ⊓ -?e ⊓ -?e⇧T"
let ?F = "forest_components f"
let ?n1 = "card { x . regular x ∧ x ≤ --h }"
let ?n2 = "card { x . regular x ∧ x ≤ --h ∧ x ≤ -?e ∧ x ≤ -?e⇧T }"
have 1: "regular f ∧ regular ?e"
by (metis assms(1) kruskal_spanning_invariant_def spanning_forest_def choose_arc_regular)
hence 2: "regular ?f ∧ regular ?F ∧ regular (?e⇧T)"
using regular_closed_star regular_conv_closed regular_mult_closed by simp
have 3: "¬ ?e ≤ -?e"
using assms(2) inf.orderE choose_arc_bot_iff by fastforce
have 4: "?n2 < ?n1"
apply (rule psubset_card_mono)
using finite_regular apply simp
using 1 3 kruskal_spanning_invariant_def choose_arc_below by auto
show "(?e ≤ -?F ⟶ kruskal_spanning_invariant ?f g ?h ∧ ?n2 < ?n1) ∧ (¬ ?e ≤ -?F ⟶ kruskal_spanning_invariant f g ?h ∧ ?n2 < ?n1)"
proof (rule conjI)
have 5: "injective ?f"
apply (rule kruskal_injective_inv)
using assms(1) kruskal_spanning_invariant_def spanning_forest_def apply simp
apply (simp add: covector_mult_closed)
apply (simp add: comp_associative comp_isotone star.right_plus_below_circ)
apply (meson mult_left_isotone order_lesseq_imp star_outer_increasing top.extremum)
using assms(1,2) kruskal_spanning_invariant_def kruskal_injective_inv_2 choose_arc_arc spanning_forest_def apply simp
using assms(2) arc_injective choose_arc_arc apply blast
using assms(1,2) kruskal_spanning_invariant_def kruskal_injective_inv_3 choose_arc_arc spanning_forest_def by simp
show "?e ≤ -?F ⟶ kruskal_spanning_invariant ?f g ?h ∧ ?n2 < ?n1"
proof
assume 6: "?e ≤ -?F"
have 7: "equivalence ?F"
using assms(1) kruskal_spanning_invariant_def forest_components_equivalence spanning_forest_def by simp
have "?e⇧T * top * ?e⇧T = ?e⇧T"
using assms(2) by (simp add: arc_top_arc choose_arc_arc)
hence "?e⇧T * top * ?e⇧T ≤ -?F"
using 6 7 conv_complement conv_isotone by fastforce
hence 8: "?e * ?F * ?e = bot"
using le_bot triple_schroeder_p by simp
show "kruskal_spanning_invariant ?f g ?h ∧ ?n2 < ?n1"
proof (unfold kruskal_spanning_invariant_def, intro conjI)
show "symmetric g"
using assms(1) kruskal_spanning_invariant_def by simp
next
show "?h = ?h⇧T"
using assms(1) by (simp add: conv_complement conv_dist_inf inf_commute inf_left_commute kruskal_spanning_invariant_def)
next
show "g ⊓ --?h = ?h"
using 1 2 by (metis (hide_lams) assms(1) kruskal_spanning_invariant_def inf_assoc pp_dist_inf)
next
show "spanning_forest ?f (-?h ⊓ g)"
proof (unfold spanning_forest_def, intro conjI)
show "injective ?f"
using 5 by simp
next
show "acyclic ?f"
apply (rule kruskal_acyclic_inv)
using assms(1) kruskal_spanning_invariant_def spanning_forest_def apply simp
apply (simp add: covector_mult_closed)
using 8 assms(1) kruskal_spanning_invariant_def spanning_forest_def kruskal_acyclic_inv_1 apply simp
using 8 apply (metis comp_associative mult_left_sub_dist_sup_left star.circ_loop_fixpoint sup_commute le_bot)
using 6 by (simp add: p_antitone_iff)
next
show "?f ≤ --(-?h ⊓ g)"
apply (rule kruskal_subgraph_inv)
using assms(1) kruskal_spanning_invariant_def spanning_forest_def apply simp
using assms(1) apply (metis kruskal_spanning_invariant_def choose_arc_below order.trans pp_isotone_inf)
using assms(1) kruskal_spanning_invariant_def apply simp
using assms(1) kruskal_spanning_invariant_def by simp
next
show "components (-?h ⊓ g) ≤ forest_components ?f"
apply (rule kruskal_spanning_inv)
using 5 apply simp
using 1 regular_closed_star regular_conv_closed regular_mult_closed apply simp
using 1 apply simp
using assms(1) kruskal_spanning_invariant_def spanning_forest_def by simp
next
show "regular ?f"
using 2 by simp
qed
next
show "?n2 < ?n1"
using 4 by simp
qed
qed
next
show "¬ ?e ≤ -?F ⟶ kruskal_spanning_invariant f g ?h ∧ ?n2 < ?n1"
proof
assume "¬ ?e ≤ -?F"
hence 9: "?e ≤ ?F"
using 2 assms(2) arc_in_partition choose_arc_arc by fastforce
show "kruskal_spanning_invariant f g ?h ∧ ?n2 < ?n1"
proof (unfold kruskal_spanning_invariant_def, intro conjI)
show "symmetric g"
using assms(1) kruskal_spanning_invariant_def by simp
next
show "?h = ?h⇧T"
using assms(1) by (simp add: conv_complement conv_dist_inf inf_commute inf_left_commute kruskal_spanning_invariant_def)
next
show "g ⊓ --?h = ?h"
using 1 2 by (metis (hide_lams) assms(1) kruskal_spanning_invariant_def inf_assoc pp_dist_inf)
next
show "spanning_forest f (-?h ⊓ g)"
proof (unfold spanning_forest_def, intro conjI)
show "injective f"
using assms(1) kruskal_spanning_invariant_def spanning_forest_def by simp
next
show "acyclic f"
using assms(1) kruskal_spanning_invariant_def spanning_forest_def by simp
next
have "f ≤ --(-h ⊓ g)"
using assms(1) kruskal_spanning_invariant_def spanning_forest_def by simp
also have "... ≤ --(-?h ⊓ g)"
using comp_inf.mult_right_isotone inf.sup_monoid.add_commute inf_left_commute p_antitone_inf pp_isotone by auto
finally show "f ≤ --(-?h ⊓ g)"
by simp
next
show "components (-?h ⊓ g) ≤ ?F"
apply (rule kruskal_spanning_inv_1)
using 9 apply simp
using 1 apply simp
using assms(1) kruskal_spanning_invariant_def spanning_forest_def apply simp
using assms(1) kruskal_spanning_invariant_def forest_components_equivalence spanning_forest_def by simp
next
show "regular f"
using 1 by simp
qed
next
show "?n2 < ?n1"
using 4 by simp
qed
qed
qed
qed

theorem kruskal_spanning:
"VARS e f h
[ symmetric g ]
f := bot;
h := g;
WHILE h ≠ bot
INV { kruskal_spanning_invariant f g h }
VAR { card { x . regular x ∧ x ≤ --h } }
DO e := choose_arc h;
IF e ≤ -forest_components f THEN
f := (f ⊓ -(top * e * f⇧T⇧⋆)) ⊔ (f ⊓ top * e * f⇧T⇧⋆)⇧T ⊔ e
ELSE
SKIP
FI;
h := h ⊓ -e ⊓ -e⇧T
OD
[ spanning_forest f g ]"
apply vcg_tc_simp
using kruskal_vc_1 apply simp
using kruskal_vc_2 apply simp
using kruskal_spanning_invariant_def by auto

lemma kruskal_exists_spanning:
"symmetric g ⟹ ∃f . spanning_forest f g"
using tc_extract_function kruskal_spanning by blast

text ‹Theorem 16›

lemma symmetric_spannable:
"symmetric g ⟹ spannable (--g)"
using kruskal_exists_spanning spanning_forest_spanning spannable_def by blast

text ‹
We prove total correctness of a simple breadth-first search algorithm.
It is a variant of an algorithm discussed in \cite{Berghammer1999}.
›

theorem bfs_reachability:
"VARS p q t
[ regular r ∧ regular s ∧ vector s ]
t := bot;
q := s;
p := -s ⊓ r⇧T * s;
WHILE p ≠ bot
INV { regular r ∧ regular q ∧ vector q ∧ asymmetric t ∧ t ≤ r ∧ t ≤ q ∧ q = t⇧T⇧⋆ * s ∧ p = -q ⊓ r⇧T * q }
VAR { card { x . regular x ∧ x ≤ --(-q ⊓ r⇧T⇧⋆ * s) } }
DO t := t ⊔ (r ⊓ q * p⇧T);
q := q ⊔ p;
p := -q ⊓ r⇧T * p
OD
[ asymmetric t ∧ t ≤ r ∧ q = t⇧T⇧⋆ * s ∧ q = r⇧T⇧⋆ * s ]"
proof vcg_tc
fix p q t
assume "regular r ∧ regular s ∧ vector s"
thus "regular r ∧ regular s ∧ vector s ∧ asymmetric bot ∧ bot ≤ r ∧ bot ≤ s ∧ s = bot⇧T⇧⋆ * s ∧ -s ⊓ r⇧T * s = -s ⊓ r⇧T * s"
by (simp add: star.circ_zero)
next
fix p q t
assume 1: "(regular r ∧ regular q ∧ vector q ∧ asymmetric t ∧ t ≤ r ∧ t ≤ q ∧ q = t⇧T⇧⋆ * s ∧ p = -q ⊓ r⇧T * q) ∧ ¬ p ≠ bot"
have "q = r⇧T⇧⋆ * s"
apply (rule antisym)
using 1 conv_order mult_left_isotone star_isotone apply simp
using 1 by (metis inf.sup_monoid.add_commute mult_1_left mult_left_isotone mult_right_isotone order_lesseq_imp pseudo_complement star.circ_reflexive star_left_induct_mult)
thus "asymmetric t ∧ t ≤ r ∧ q = t⇧T⇧⋆ * s ∧ q = r⇧T⇧⋆ * s"
using 1 by simp
next
fix n p q t
assume 2: "((regular r ∧ regular q ∧ vector q ∧ asymmetric t ∧ t ≤ r ∧ t ≤ q ∧ q = t⇧T⇧⋆ * s ∧ p = -q ⊓ r⇧T * q) ∧ p ≠ bot) ∧ card { x . regular x ∧ x ≤ --(-q ⊓ r⇧T⇧⋆ * s) } = n"
hence 3: "vector p"
using vector_complement_closed vector_inf_closed vector_mult_closed by blast
show "(-(q ⊔ p) ⊓ r⇧T * p, q ⊔ p, t ⊔ (r ⊓ q * p⇧T))
∈ { trip . (case trip of (p, q, t) ⇒ regular r ∧ regular q ∧ vector q ∧ asymmetric t ∧ t ≤ r ∧ t ≤ q ∧ q = t⇧T⇧⋆ * s ∧ p = -q ⊓ r⇧T * q) ∧
(case trip of (p, q, t) ⇒ card { x . regular x ∧ x ≤ --(-q ⊓ r⇧T⇧⋆ * s) }) < n }"
apply (rule CollectI, rule conjI)
subgoal proof (intro case_prodI, intro conjI)
show "regular r"
using 2 by blast
show "regular (q ⊔ p)"
using 2 regular_conv_closed regular_mult_closed by force
show "vector (q ⊔ p)"
using 2 vector_complement_closed vector_inf_closed vector_mult_closed vector_sup_closed by force
show "asymmetric (t ⊔ (r ⊓ q * p⇧T))"
proof -
have "t ⊓ (r ⊓ q * p⇧T)⇧T ≤ t ⊓ p * q⇧T"
by (metis comp_inf.mult_right_isotone conv_dist_comp conv_involutive conv_order inf.cobounded2)
also have "... ≤ t ⊓ p"
using 3 by (metis comp_inf.mult_right_isotone comp_inf.star.circ_sup_sub_sup_one_1 inf.boundedE le_sup_iff mult_right_isotone)
finally have 4: "t ⊓ (r ⊓ q * p⇧T)⇧T = bot"
using 2 by (metis antisym bot_least inf.sup_monoid.add_assoc pseudo_complement)
hence 5: "r ⊓ q * p⇧T ⊓ t⇧T = bot"
using conv_inf_bot_iff inf_commute by force
have "r ⊓ q * p⇧T ⊓ (r ⊓ q * p⇧T)⇧T ≤ q * p⇧T ⊓ p * q⇧T"
by (metis comp_inf.comp_isotone conv_dist_comp conv_involutive conv_order inf.cobounded2)
also have "... ≤ q ⊓ p"
using 2 3 by (metis comp_inf.comp_isotone inf.cobounded1 vector_covector)
finally have 6: "r ⊓ q * p⇧T ⊓ (r ⊓ q * p⇧T)⇧T = bot"
using 2 by (metis inf.cobounded1 inf.sup_monoid.add_commute le_bot pseudo_complement)
have "(t ⊔ (r ⊓ q * p⇧T)) ⊓ (t ⊔ (r ⊓ q * p⇧T))⇧T = (t ⊓ t⇧T) ⊔ (t ⊓ (r ⊓ q * p⇧T)⇧T) ⊔ (r ⊓ q * p⇧T ⊓ t⇧T) ⊔ (r ⊓ q * p⇧T ⊓ (r ⊓ q * p⇧T)⇧T)"
by (simp add: sup.commute sup.left_commute conv_dist_sup inf_sup_distrib1 inf_sup_distrib2)
also have "... = bot"
using 2 4 5 6 by auto
finally show ?thesis
.
qed
show "t ⊔ (r ⊓ q * p⇧T) ≤ r"
using 2 by (meson inf.cobounded1 le_supI)
show "t ⊔ (r ⊓ q * p⇧T) ≤ q ⊔ p"
using 2 by (metis comp_inf.star.circ_sup_sub_sup_one_1 inf.absorb2 inf.coboundedI2 inf.sup_monoid.add_commute le_sup_iff mult_right_isotone sup_left_divisibility)
show "q ⊔ p = (t ⊔ (r ⊓ q * p⇧T))⇧T⇧⋆ * s"
proof (rule antisym)
have 7: "q ≤ (t ⊔ (r ⊓ q * p⇧T))⇧T⇧⋆ * s"
using 2 by (metis conv_order mult_left_isotone star_isotone sup_left_divisibility)
have "-q ⊓ (r ⊓ q * p⇧T)⇧T * q ≤ (t ⊔ (r ⊓ q * p⇧T))⇧T * t⇧T⇧⋆ * s"
using 2 comp_associative conv_dist_sup inf.coboundedI2 mult_right_sub_dist_sup_right by auto
also have "... ≤ (t ⊔ (r ⊓ q * p⇧T))⇧T⇧⋆ * s"
by (simp add: conv_dist_sup mult_left_isotone star.circ_increasing star.circ_mult_upper_bound star.circ_sub_dist)
finally have 8: "-q ⊓ (r ⊓ q * p⇧T)⇧T * q ≤ (t ⊔ (r ⊓ q * p⇧T))⇧T⇧⋆ * s"
.
have 9: "(r ⊓ -q)⇧T * q = bot"
using 2 by (metis conv_dist_inf covector_inf_comp_3 pp_inf_p semiring.mult_not_zero vector_complement_closed)
have "-q ⊓ (r ⊓ -(q * p⇧T))⇧T * q = -q ⊓ (r ⊓ (-q ⊔ -p⇧T))⇧T * q"
using 2 3 by (metis p_dist_inf vector_covector)
also have "... = (-q ⊓ (r ⊓ -q)⇧T * q) ⊔ (-q ⊓ (r ⊓ -p⇧T)⇧T * q)"
by (simp add: conv_dist_sup inf_sup_distrib1 mult_right_dist_sup)
also have "... = -q ⊓ (r ⊓ -p⇧T)⇧T * q"
using 9 by simp
also have "... = -q ⊓ -p ⊓ r⇧T * q"
using 3 by (metis conv_complement conv_dist_inf conv_involutive inf.sup_monoid.add_assoc inf_vector_comp vector_complement_closed)
finally have 10: "-q ⊓ (r ⊓ -(q * p⇧T))⇧T * q = bot"
using 2 inf_import_p pseudo_complement by auto
have "r = (r ⊓ q * p⇧T) ⊔ (r ⊓ -(q * p⇧T))"
using 2 by (smt (z3) maddux_3_11_pp pp_dist_comp regular_closed_inf regular_conv_closed)
hence "p = -q ⊓ ((r ⊓ q * p⇧T) ⊔ (r ⊓ -(q * p⇧T)))⇧T * q"
using 2 by auto
also have "... = (-q ⊓ (r ⊓ q * p⇧T)⇧T * q) ⊔ (-q ⊓ (r ⊓ -(q * p⇧T))⇧T * q)"
by (simp add: conv_dist_sup inf_sup_distrib1 semiring.distrib_right)
also have "... ≤ (t ⊔ (r ⊓ q * p⇧T))⇧T⇧⋆ * s"
using 8 10 le_sup_iff bot_least by blast
finally show "q ⊔ p ≤ (t ⊔ (r ⊓ q * p⇧T))⇧T⇧⋆ * s"
using 7 by simp
have 11: "t⇧T * q ≤ r⇧T * q"
using 2 conv_order mult_left_isotone by auto
have "t⇧T * p ≤ t⇧T * top"
by (simp add: mult_right_isotone)
also have "... = t⇧T * q ⊔ t⇧T * -q"
using 2 regular_complement_top semiring.distrib_left by force
also have "... = t⇧T * q"
proof -
have "t⇧T * -q = bot"
using 2 by (metis bot_least conv_complement_sub conv_dist_comp conv_involutive mult_right_isotone regular_closed_bot stone sup.absorb2 sup_commute)
thus ?thesis
by simp
qed
finally have 12: "t⇧T * p ≤ r⇧T * q"
using 11 order.trans by blast
have 13: "(r ⊓ q * p⇧T)⇧T * q ≤ r⇧T * q"
by (simp add: conv_dist_inf mult_left_isotone)
have "(r ⊓ q * p⇧T)⇧T * p ≤ p"
using 3 by (metis conv_dist_comp conv_dist_inf conv_involutive inf.coboundedI2 mult_isotone mult_right_isotone top.extremum)
hence 14: "(r ⊓ q * p⇧T)⇧T * p ≤ r⇧T * q"
using 2 le_infE by blast
have "(t ⊔ (r ⊓ q * p⇧T))⇧T * (q ⊔ p) = t⇧T * q ⊔ t⇧T * p ⊔ (r ⊓ q * p⇧T)⇧T * q ⊔ (r ⊓ q * p⇧T)⇧T * p"
by (metis conv_dist_sup semiring.distrib_left semiring.distrib_right sup_assoc)
also have "... ≤ r⇧T * q"
using 11 12 13 14 by simp
finally have "(t ⊔ (r ⊓ q * p⇧T))⇧T * (q ⊔ p) ≤ q ⊔ p"
using 2 by (metis maddux_3_21_pp sup.boundedE sup_right_divisibility)
thus "(t ⊔ (r ⊓ q * p⇧T))⇧T⇧⋆ * s ≤ q ⊔ p"
using 2 by (smt (verit, ccfv_SIG) star.circ_loop_fixpoint star_left_induct sup.bounded_iff sup_left_divisibility)
qed
show "-(q ⊔ p) ⊓ r⇧T * p = -(q ⊔ p) ⊓ r⇧T * (q ⊔ p)"
proof (rule antisym)
show "-(q ⊔ p) ⊓ r⇧T * p ≤ -(q ⊔ p) ⊓ r⇧T * (q ⊔ p)"
using inf.sup_right_isotone mult_left_sub_dist_sup_right by blast
have 15: "- (q ⊔ p) ⊓ r⇧T * (q ⊔ p) = - (q ⊔ p) ⊓ r⇧T * q ⊔ - (q ⊔ p) ⊓ r⇧T * p"
by (simp add: comp_inf.semiring.distrib_left mult_left_dist_sup)
have "- (q ⊔ p) ⊓ r⇧T * q ≤ - (q ⊔ p) ⊓ r⇧T * p"
using 2 by (metis bot_least p_dist_inf p_dist_sup p_inf_sup_below pseudo_complement)
thus "- (q ⊔ p) ⊓ r⇧T * (q ⊔ p) ≤ - (q ⊔ p) ⊓ r⇧T * p"
using 15 sup.absorb2 by force
qed
qed
subgoal proof clarsimp
have "card { x . regular x ∧ x ≤ -q ∧ x ≤ -p ∧ x ≤ --(r⇧T⇧⋆ * s) } < card { x . regular x ∧ x ≤ --(-q ⊓ r⇧T⇧⋆ * s) }"
proof (rule psubset_card_mono)
show "finite { x . regular x ∧ x ≤ --(-q ⊓ r⇧T⇧⋆ * s) }"
using finite_regular by simp
show "{ x . regular x ∧ x ≤ -q ∧ x ≤ -p ∧ x ≤ --(r⇧T⇧⋆ * s) } ⊂ { x . regular x ∧ x ≤ --(-q ⊓ r⇧T⇧⋆ * s) }"
proof -
have "∀x . x ≤ -q ∧ x ≤ --(r⇧T⇧⋆ * s) ⟶ x ≤ --(-q ⊓ r⇧T⇧⋆ * s)"
by auto
hence 16: "{ x . regular x ∧ x ≤ -q ∧ x ≤ -p ∧ x ≤ --(r⇧T⇧⋆ * s) } ⊆ { x . regular x ∧ x ≤ --(-q ⊓ r⇧T⇧⋆ * s) }"
by blast
have 17: "regular p"
using 2 regular_conv_closed regular_mult_closed by force
hence 18: "¬ p ≤ -p"
using 2 by (metis inf.absorb1 pp_inf_p)
have 19: "p ≤ -q"
using 2 by simp
have "r⇧T * q ≤ r⇧T⇧⋆ * s"
using 2 by (metis (no_types, lifting) comp_associative conv_dist_sup mult_left_isotone star.circ_increasing star.circ_mult_upper_bound star.circ_sub_dist sup_left_divisibility)
hence 20: "p ≤ --(r⇧T⇧⋆ * s)"
using 2 le_infI2 order_lesseq_imp pp_increasing by blast
hence 21: "p ≤ --(-q ⊓ r⇧T⇧⋆ * s)"
using 2 by simp
show ?thesis
using 16 17 18 19 20 21 by blast
qed
qed
thus "card { x . regular x ∧ x ≤ -q ∧ x ≤ -p ∧ x ≤ --(r⇧T⇧⋆ * s) } < n"
using 2 by auto
qed
done
qed

text ‹Theorem 18›

lemma bfs_reachability_exists:
"regular r ∧ regular s ∧ vector s ⟹ ∃t . asymmetric t ∧ t ≤ r ∧ t⇧T⇧⋆ * s = r⇧T⇧⋆ * s"
using tc_extract_function bfs_reachability by blast

text ‹Theorem 17›

lemma orientable_path:
"arc x ⟹ x ≤ --y⇧⋆ ⟹ ∃z . z ≤ y ∧ asymmetric z ∧ x ≤ --z⇧⋆"
proof -
assume 1: "arc x" and 2: "x ≤ --y⇧⋆"
hence "regular (--y) ∧ regular (x * top) ∧ vector (x * top)"
using bijective_regular mult_assoc by auto
from this obtain t where 3: "asymmetric t ∧ t ≤ --y ∧ t⇧T⇧⋆ * (x * top) = (--y)⇧T⇧⋆ * (x * top)"
using bfs_reachability_exists by blast
let ?z = "t ⊓ y"
have "x⇧T * top * x⇧T ≤ (--y)⇧T⇧⋆"
using 1 2 by (metis arc_top_arc conv_complement conv_isotone conv_star_commute arc_conv_closed pp_dist_star)
hence "x⇧T ≤ (--y)⇧T⇧⋆ * x * top"
using 1 comp_associative conv_dist_comp shunt_bijective by force
also have "... = t⇧T⇧⋆ * x * top"
using 3 mult_assoc by force
finally have "x⇧T * top * x⇧T ≤ t⇧T⇧⋆"
using 1 comp_associative conv_dist_comp shunt_bijective by force
hence "x⇧T ≤ t⇧T⇧⋆"
using 1 by (metis arc_top_arc arc_conv_closed)
also have "... ≤ (--?z)⇧T⇧⋆"
using 3 by (metis conv_order inf.orderE inf_pp_semi_commute star_isotone)
finally have "x ≤ --?z⇧⋆"
using conv_order conv_star_commute pp_dist_star by fastforce
thus "∃z . z ≤ y ∧ asymmetric z ∧ x ≤ --z⇧⋆"
using 3 asymmetric_inf_closed inf.cobounded2 by blast
qed

subsection ‹Extending partial orders to linear orders›

text ‹
We prove total correctness of Szpilrajn's algorithm \cite{Szpilrajn1930}.
A partial-correctness proof using Prover9 is given in \cite{BerghammerStruth2010}.
›

theorem szpilrajn:
"VARS e t
[ order p ∧ regular p ]
t := p;
WHILE t ⊔ t⇧T ≠ top
INV { order t ∧ regular t ∧ p ≤ t }
VAR { card { x . regular x ∧ x ≤ -(t ⊔ t⇧T) } }
DO e := choose_arc (-(t ⊔ t⇧T));
t := t ⊔ t * e * t
OD
[ linear_order t ∧ p ≤ t ]"
proof vcg_tc_simp
fix t
let ?e = "choose_arc (-t ⊓ -t⇧T)"
let ?tet = "t * ?e * t"
let ?t = "t ⊔ ?tet"
let ?s1 = "{ x . regular x ∧ x ≤ -t ∧ x ≤ -?tet ∧ x ≤ -?t⇧T }"
let ?s2 = "{ x . regular x ∧ x ≤ -t ∧ x ≤ -t⇧T }"
assume 1: "reflexive t ∧ transitive t ∧ antisymmetric t ∧ regular t ∧ p ≤ t ∧ ¬ linear t"
show "reflexive ?t ∧
transitive ?t ∧
antisymmetric ?t ∧
?t = t ⊔ --?tet ∧
p ≤ ?t ∧
card ?s1 < card ?s2"
proof (intro conjI)
show "reflexive ?t"
using 1 by (simp add: sup.coboundedI1)
have "-t ⊓ -t⇧T ≠ bot"
using 1 regular_closed_top regular_conv_closed by force
hence 2: "arc ?e"
using choose_arc_arc by blast
have "?t * ?t = t * t ⊔ t * ?tet ⊔ ?tet * t ⊔ ?tet * ?tet"
by (smt (z3) mult_left_dist_sup mult_right_dist_sup sup_assoc)
also have "... ≤ ?t"
proof (intro sup_least)
show "t * t ≤ ?t"
using 1 sup.coboundedI1 by blast
show "t * ?tet ≤ ?t"
using 1 by (metis le_supI2 mult_left_isotone mult_assoc)
show "?tet * t ≤ ?t"
using 1 mult_right_isotone sup.coboundedI2 mult_assoc by auto
have "?e * t * t * ?e ≤ ?e"
using 2 by (smt arc_top_arc mult_assoc mult_right_isotone mult_left_isotone top_greatest)
hence "transitive ?tet"
by (smt mult_assoc mult_right_isotone mult_left_isotone)
thus "?tet * ?tet ≤ ?t"
using le_supI2 by auto
qed
finally show "transitive ?t"
.
have 3: "?e ≤ -t⇧T"
by (metis choose_arc_below inf.cobounded2 order_lesseq_imp p_dist_sup regular_closed_p)
have 4: "?e ≤ -t"
by (metis choose_arc_below inf.cobounded1 order_trans regular_closed_inf regular_closed_p)
have "?t ⊓ ?t⇧T = (t ⊓ t⇧T) ⊔ (t ⊓ ?tet⇧T) ⊔ (?tet ⊓ t⇧T) ⊔ (?tet ⊓ ?tet⇧T)"
by (smt (z3) conv_dist_sup inf_sup_distrib1 inf_sup_distrib2 sup_monoid.add_assoc)
also have "... ≤ 1"
proof (intro sup_least)
show "antisymmetric t"
using 1 by simp
have "t * t * t = t"
using 1 preorder_idempotent by fastforce
also have "... ≤ -?e⇧T"
using 3 by (metis p_antitone_iff conv_complement conv_order conv_involutive)
finally have "t⇧T * ?e⇧T * t⇧T ≤ -t"
using triple_schroeder_p by blast
hence "t ⊓ ?tet⇧T = bot"
by (simp add: comp_associative conv_dist_comp p_antitone pseudo_complement_pp)
thus "t ⊓ ?tet⇧T ≤ 1"
by simp
thus "?tet ⊓ t⇧T ≤ 1"
by (smt conv_isotone inf_commute conv_one conv_dist_inf conv_involutive)
have "?e * t * ?e ≤ ?e"
using 2 by (smt arc_top_arc mult_assoc mult_right_isotone mult_left_isotone top_greatest)
also have "... ≤ -t⇧T"
using 3 by simp
finally have "?tet ≤ -?e⇧T"
by (metis conv_dist_comp schroeder_3_p triple_schroeder_p)
hence "t * t * ?e * t * t ≤ -?e⇧T"
using 1 by (metis preorder_idempotent mult_assoc)
hence "t⇧T * ?e⇧T * t⇧T ≤ -?tet"
using triple_schroeder_p mult_assoc by auto
hence "?tet ⊓ ?tet⇧T = bot"
by (simp add: conv_dist_comp p_antitone pseudo_complement_pp mult_assoc)
thus "antisymmetric ?tet"
by simp
qed
finally show "antisymmetric ?t"
.
show "?t = t ⊔ --?tet"
using 1 choose_arc_regular regular_mult_closed by auto
show "p ≤ ?t"
using 1 by (simp add: le_supI1)
show "card ?s1 < card ?s2"
proof (rule psubset_card_mono)
show "finite { x . regular x ∧ x ≤ -t ∧ x ≤ -t⇧T }"
using finite_regular by simp
show "{ x . regular x ∧ x ≤ -t ∧ x ≤ -?tet ∧ x ≤ -?t⇧T } ⊂ { x . regular x ∧ x ≤ -t ∧ x ≤ -t⇧T }"
proof -
have "∀x . regular x ∧ x ≤ -t ∧ x ≤ -?tet ∧ x ≤ -?t⇧T ⟶ regular x ∧ x ≤ -t ∧ x ≤ -t⇧T"
using conv_dist_sup by auto
hence 5: "{ x . regular x ∧ x ≤ -t ∧ x ≤ -?tet ∧ x ≤ -?t⇧T } ⊆ { x . regular x ∧ x ≤ -t ∧ x ≤ -t⇧T }"
by blast
have 6: "regular ?e ∧ ?e ≤ -t ∧ ?e ≤ -t⇧T"
using 2 3 4 choose_arc_regular by blast
have "¬ ?e ≤ -?tet"
proof
assume 7: "?e ≤ -?tet"
have "?e ≤ ?e * t"
using 1 by (meson mult_right_isotone mult_sub_right_one order.trans)
also have "?e * t ≤ -(t⇧T * ?e)"
using 7 p_antitone_iff schroeder_3_p mult_assoc by auto
also have "... ≤ -(1⇧T * ?e)"
using 1 conv_isotone mult_left_isotone p_antitone by blast
also have "... = -?e"
by simp
finally show False
using 1 2 by (smt (z3) bot_least eq_refl inf.absorb1 pseudo_complement semiring.mult_not_zero top_le)
qed
thus ?thesis
using 5 6 by blast
qed
qed
qed
qed

text ‹Theorem 15›

lemma szpilrajn_exists:
"order p ∧ regular p ⟹ ∃t . linear_order t ∧ p ≤ t"
using tc_extract_function szpilrajn by blast

lemma complement_one_transitively_orientable:
"transitively_orientable (-1)"
proof -
have "∃t . linear_order t"
using szpilrajn_exists bijective_one_closed bijective_regular order_one_closed by blast
thus ?thesis
using exists_split_characterisations(4) by blast
qed

end

end

end