Theory Relation_Algebra_Vectors

(* 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 ‹Vectors›

theory Relation_Algebra_Vectors
  imports Relation_Algebra
begin

text ‹Vectors can be used for modelling sets of states. In this section we
follow Maddux's book to derive some of their most important properties.›

context relation_algebra
begin

definition is_vector :: "'a ⇒ bool"
  where "is_vector x ≡ x = x ; 1"

lemma vector_compl: "is_vector x ⟹ is_vector (-x)"
by (metis one_compl is_vector_def)

lemma vector_add: "⟦is_vector x; is_vector y⟧ ⟹ is_vector (x + y)"
by (metis comp_distr is_vector_def)

lemma vector_mult: "⟦is_vector x; is_vector y⟧ ⟹ is_vector (x ⋅ y)"
by (metis ra_1 is_vector_def)

lemma vector_comp: "⟦is_vector x; is_vector y⟧ ⟹ is_vector (x ; y)"
by (metis comp_assoc is_vector_def)

lemma vector_1: "is_vector x ⟹ (x ⋅ y) ; z = x ⋅ y ; z"
by (metis inf.commute ra_1 is_vector_def)

lemma vector_1_comm: "is_vector y ⟹ (x ⋅ y) ; z = x ; z ⋅ y"
by (metis ra_1 is_vector_def)

lemma vector_2: "is_vector y ⟹ (x ⋅ y⇧⌣) ; z = x ; (y ⋅ z)"
by (metis inf.commute ra_2 is_vector_def)

lemma vector_2_var: "is_vector y ⟹ (x ⋅ y⇧⌣) ; z = (x ⋅ y⇧⌣) ; (y ⋅ z)"
by (metis inf.left_idem vector_2)

lemma vector_idem [simp]: "is_vector x ⟹ x ; x = x"
by (metis inf_absorb2 inf_top_left maddux_21 vector_1_comm)

lemma vector_rectangle [simp]: "is_vector x ⟹ x ; 1 ; x = x"
by (metis vector_idem is_vector_def)

lemma vector_3 [simp]: "is_vector x ⟹ (x ⋅ 1') ; y = x ⋅ y"
by (metis inf.commute mult.left_neutral vector_1)

end (* relation_algebra *)

end