Quelle  vect_3D_2D.pvs   Sprache: unbekannt

vect_3D_2D: THEORY
BEGIN

  IMPORTING vectors_2D, vectors_3D

  vect2(v:Vect3): Vect2 = (v`x,v`y)

  CONVERSION vect2

  v2   : VAR Vect2
  v,w  : VAR Vect3
  a,vz : VAR real
  
  vect2_add : LEMMA 
    vect2(v+w) = vect2(v) + vect2(w)

  vect2_sub   : LEMMA 
    vect2(v-w) = vect2(v) - vect2(w)

  vect2_scal : LEMMA 
    vect2(a*v) = a*vect2(v)
 
  vect2_neg : LEMMA 
    vect2(-v)  = -vect2(v) 

  vect2_zero  : LEMMA 
    vect2(zero) = zero

  vect2_eq : LEMMA
     vect2(v WITH [z := vz]) = vect2(v)

  vect2_eq_ext : LEMMA
     vect2(v2 WITH [z |-> vz]) = v2

  vect2_ext_id :LEMMA
    vect2(v) WITH [z |-> v`z] = v

  AUTO_REWRITE+ vect2_zero
  AUTO_REWRITE+ vect2_eq
  AUTO_REWRITE+ vect2_eq_ext
  AUTO_REWRITE+ vect2_ext_id

END vect_3D_2D