Theory Forests
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›
context bounded_distrib_allegory_signature
begin
abbreviation irreflexive_inf :: "'a ⇒ bool" where "irreflexive_inf x ≡ x ⊓ 1 = bot"
end
context bounded_distrib_allegory
begin
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 order.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)
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.
›
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
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
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›
lemma acyclic_irreflexive_star_antisymmetric:
"acyclic x ⟷ irreflexive x ∧ antisymmetric (x⇧⋆)"
by (metis acyclic_star_inf_conv_iff conv_star_commute order.trans reflexive_inf_closed star.circ_mult_increasing star.circ_reflexive order.antisym)
text ‹Theorem 1.8›
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 order.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›
thm eq_iff order.eq_iff
lemma acyclic_4a_4b:
"acyclic_4a x ⟷ acyclic_4b x"
using acyclic_4a_def acyclic_4b_def order.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 order.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"
using comp_associative inf.sup_mono mult_right_isotone top.extremum by presburger
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: order.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: order.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 order.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 order.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 order.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
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 order.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"
using 1 by (simp add: acyclic_5g_def inf.left_commute inf.sup_monoid.add_commute maddux_3_11_pp)
finally show "y⇧⋆ ⊓ z⇧⋆ = 1"
by (simp add: order.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"
by (simp add: inf.left_commute inf.sup_monoid.add_commute)
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