Theory Relation_Algebra_Models

(* Title:      Relation Algebra
   Author:     Alasdair Armstrong, Simon Foster, Georg Struth, Tjark Weber
   Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
               Tjark Weber <tjark.weber at it.uu.se>
*)

section ‹Models of Relation Algebra›

theory Relation_Algebra_Models
  imports Relation_Algebra Kleene_Algebra.Inf_Matrix
begin

text ‹We formalise two models. First we show the obvious: binary relations
form a relation algebra. Then we show that infinite matrices (which we
formalised originally for Kleene algebras) form models of relation algebra if
we restrict their element type to @{typ bool}.›

subsection ‹Binary Relations›

text ‹Since Isabelle's libraries for binary relations are very well
developed, the proof for this model is entirely trivial.›

interpretation rel_relation_algebra: relation_algebra "(-)" uminus "(∩)" "(⊆)" "(⊂)" "(∪)" "{}" UNIV "(O)" Relation.converse Id
by unfold_locales auto

subsection ‹Infinite Boolean Matrices›

text ‹Next we consider infinite Boolean matrices. We define the maximal
Boolean matrix (all of its entries are @{const True}), the converse or
transpose of a matrix, the intersection of two Boolean matrices and the
complement of a Boolean matrix.›

definition mat_top :: "('a, 'b, bool) matrix" ("τ")
  where "τ i j ≡ True"

definition mat_transpose :: "('a, 'b, 'c) matrix ⇒ ('b, 'a, 'c) matrix" ("_⇧†" [101] 100)
  where "f⇧† ≡ (λi j. f j i)"

definition mat_inter :: "('a, 'b, bool) matrix ⇒ ('a, 'b, bool) matrix ⇒ ('a, 'b, bool) matrix" (infixl "⊓" 70)
  where "f ⊓ g ≡ (λi j. f i j ⋅ g i j)"

definition mat_complement :: "('a, 'b, bool) matrix ⇒ ('a, 'b, bool) matrix" ("_⇧c" [101] 100)
  where "f⇧c = (λi j. - f i j)"

text ‹Next we show that the Booleans form a dioid. We state this as an
\emph{instantiation} result. The Kleene algebra files contain an
\emph{interpretation} proof, which is not sufficient for our purposes.›

instantiation bool :: dioid_one_zero
begin

  definition zero_bool_def:
    "zero_bool ≡ False"

  definition one_bool_def:
    "one_bool ≡ True"

  definition times_bool_def:
    "times_bool ≡ (∧)"

  definition plus_bool_def:
    "plus_bool ≡ (∨)"

  instance
  by standard (auto simp: plus_bool_def times_bool_def one_bool_def zero_bool_def)

end

text ‹We now show that infinite Boolean matrices form a Boolean algebra.›

lemma le_funI2: "(⋀i j. f i j ≤ g i j) ⟹ f ≤ g"
by (metis le_funI)

interpretation matrix_ba: boolean_algebra "λf g. f ⊓ g⇧c" mat_complement "(⊓)" "(≤)" "(<)" mat_add mat_zero mat_top
by standard (force intro!: le_funI simp: mat_inter_def plus_bool_def mat_add_def mat_zero_def zero_bool_def mat_top_def mat_complement_def)+

text ‹We continue working towards the main result of this section, that
infinite Boolean matrices form a relation algebra.›

lemma mat_mult_var: "(f ⊗ g) = (λi j. ∑ {(f i k) * (g k j) | k. k ∈ UNIV})"
by (rule ext)+ (simp add: mat_mult_def)

text ‹The following fact is related to proving the last relation algebra
axiom in the matrix model. It is more complicated than necessary since finite
infima are not well developed in Isabelle. Instead we translate properties of
finite infima into properties of finite suprema by using Boolean algebra. For
finite suprema we have developed special-purpose theorems in the Kleene algebra
files.›

lemma mat_res_pointwise:
  fixes i j :: "'a::finite"
    and x :: "('a, 'a, bool) matrix"
  shows "(x⇧† ⊗ (x ⊗ y)⇧c) i j ≤ (y⇧c) i j"
proof -
  have "∑{(x⇧†) i k ∧ ((x ⊗ y)⇧c) k j |k. k ∈ UNIV} ≤ (y⇧c) i j ⟷ (∀k. ((x⇧†) i k ∧ ((x ⊗ y)⇧c) k j) ≤ (y⇧c) i j)"
    by (subst sum_sup) auto
  also have "… ⟷ (∀k. ((x⇧†) i k ∧ - (x ⊗ y) k j) ≤ (y⇧c) i j)"
    by (simp only: mat_complement_def)
  also have "… ⟷ (∀k. (x⇧†) i k ≤ ((y⇧c) i j ∨ (x ⊗ y) k j))"
    by auto
  also have "… ⟷ (∀k. (x⇧†) i k ≤ (- y i j ∨ (x ⊗ y) k j))"
    by (simp only: mat_complement_def)
  also have "… ⟷ (∀k. ((x⇧†) i k ∧ y i j) ≤ (x ⊗ y) k j)"
    by auto
  also have "… ⟷ (∀k. (x k i ∧ y i j) ≤ (x ⊗ y) k j)"
    by (simp add: mat_transpose_def)
  also have "… ⟷ (∀k. (x k i ∧ y i j) ≤ ∑{x k l ∧ y l j |l. l ∈ UNIV})"
    by (simp add: mat_mult_def times_bool_def)
  also have "… ⟷ (∀k. ∑{x k i ∧ y i j} ≤ ∑{x k l ∧ y l j |l. l ∈ UNIV})"
    by simp
  also have "… ⟷ True"
    by (intro iffI TrueI allI sum_intro[rule_format]) auto
  moreover have "(x⇧† ⊗ (x ⊗ y)⇧c) i j = ∑{(x⇧†) i k ∧ ((x ⊗ y)⇧c) k j |k. k ∈ UNIV}"
    by (subst mat_mult_def) (simp add: times_bool_def)
  ultimately show ?thesis
    by auto
qed

text ‹Finally the main result of this section.›

interpretation matrix_ra: relation_algebra "λf g. f ⊓ g⇧c" mat_complement "(⊓)" "(≤)" "(<)" "(⊕)" "λi j. False" τ "(⊗)" mat_transpose ε
proof
  fix x y z :: "'a::finite ⇒ 'a ⇒ bool"
  show "(λ(i::'a) j::'a. False) ≤ x"
    by (metis predicate2I)
  show "x ⊓ x⇧c = (λi j. False)"
    by (metis matrix_ba.bot.extremum matrix_ba.inf_compl_bot rev_predicate2D)
  show "x ⊕ x⇧c = τ"
    by (fact matrix_ba.sup_compl_top)
  show "x ⊓ y⇧c = x ⊓ y⇧c"
    by (fact refl)
  show "x ⊗ y ⊗ z = x ⊗ (y ⊗ z)"
    by (metis mat_mult_assoc)
  show "x ⊗ ε = x"
    by (fact mat_oner)
  show "x ⊕ y ⊗ z = (x ⊗ z) ⊕ (y ⊗ z)"
    by (fact mat_distr)
  show "(x⇧†)⇧† = x"
    by (simp add: mat_transpose_def)
  show "(x ⊕ y)⇧† = x⇧† ⊕ y⇧†"
    by (simp add: mat_transpose_def mat_add_def)
  show "(x ⊗ y)⇧† = y⇧† ⊗ x⇧†"
    by (simp add: mat_transpose_def mat_mult_var times_bool_def conj_commute)
  show "x⇧† ⊗ (x ⊗ y)⇧c ≤ y⇧c"
    by (metis le_funI2 mat_res_pointwise)
qed

end