Theory Algorithms
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" and "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 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 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
subsection ‹Breadth-first search›
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 order.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 order.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 order.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 order.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