Theory Choose_Component

(* Title:      An Operation to Select Components
   Author:     Nicolas Robinson-O'Brien, Walter Guttmann
   Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

section ‹An Operation to Select Components›

text ‹
In this theory we axiomatise an operation to select components of a graph.
This is joint work with Nicolas Robinson-O'Brien.
›

theory Choose_Component

imports
  Relation_Algebras

begin

context stone_relation_algebra
begin

text ‹
A ‹vector_classes› corresponds to one or more equivalence classes and a ‹unique_vector_class› corresponds to a single equivalence class.
›

definition vector_classes        :: "'a ⇒ 'a ⇒ bool" where "vector_classes x v ≡ regular x ∧ regular v ∧ equivalence x ∧ vector v ∧ x * v ≤ v ∧ v ≠ bot"
definition unique_vector_class   :: "'a ⇒ 'a ⇒ bool" where "unique_vector_class x v ≡ vector_classes x v ∧ v * v⇧T ≤ x"

end

text ‹
We introduce the operation ‹choose_component›.
\begin{itemize}
  \item Axiom ‹component_in_v› expresses that the result of ‹choose_component› is contained in the set of vertices, $v$, we are selecting from, ignoring the weights.
  \item Axiom ‹component_is_vector› states that the result of ‹choose_component› is a vector.
  \item Axiom ‹component_is_regular› states that the result of ‹choose_component› is regular.
  \item Axiom ‹component_is_connected› states that any two vertices from the result of ‹choose_component› are connected in $e$.
  \item Axiom ‹component_single› states that the result of ‹choose_component› is closed under being connected in $e$.
  \item Finally, axiom ‹component_not_bot_when_v_bot_bot› expresses that the operation ‹choose_component› returns a non-empty component if the input satisfies the given criteria.
\end{itemize}
›

class choose_component =
  fixes choose_component :: "'a ⇒ 'a ⇒ 'a"

class choose_component_algebra = choose_component + stone_relation_algebra +
  assumes component_is_vector:              "vector (choose_component e v)"
  assumes component_is_regular:             "regular (choose_component e v)"
  assumes component_in_v:                   "choose_component e v ≤ --v"
  assumes component_is_connected:           "choose_component e v * (choose_component e v)⇧T ≤ e"
  assumes component_single:                 "e * choose_component e v ≤ choose_component e v"
  assumes component_not_bot_when_v_bot_bot: "vector_classes e v ⟶ choose_component e v ≠ bot"
begin

lemma component_single_eq:
  assumes "equivalence x"
  shows "choose_component x v = x * choose_component x v"
proof -
  have "choose_component x v ≤ x * choose_component x v"
    by (meson component_is_connected ex231c mult_isotone order_lesseq_imp)
  thus ?thesis
    by (simp add: component_single order.antisym)
qed

end

class choose_component_algebra_tarski = choose_component_algebra + stone_relation_algebra_tarski
begin

definition "choose_component_point x ≡ choose_component 1 (--x)"

lemma choose_component_point_point:
  assumes "vector x"
      and "x ≠ bot"
    shows "point (choose_component_point x)"
proof (intro conjI)
  show 1: "vector (choose_component_point x)"
    by (simp add: choose_component_point_def component_is_vector)
  show "injective (choose_component_point x)"
    by (simp add: choose_component_point_def component_is_connected)
  have "vector_classes 1 (--x)"
    by (metis assms comp_inf.semiring.mult_zero_left coreflexive_symmetric inf.eq_refl mult_1_left pp_one regular_closed_p selection_closed_id vector_classes_def vector_complement_closed)
  hence "choose_component_point x ≠ bot"
    by (simp add: choose_component_point_def component_not_bot_when_v_bot_bot)
  thus "surjective (choose_component_point x)"
    using 1 choose_component_point_def component_is_regular tarski vector_mult_closed by fastforce
qed

lemma choose_component_point_decreasing:
  "choose_component_point x ≤ --x"
  by (metis choose_component_point_def component_in_v regular_closed_p)

end

end