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