Quelle  definitions_3D.pvs

%------------------------------------------------------------------------------
% definitions_3D.pvs
% ACCoRD v1.0
%------------------------------------------------------------------------------

definitions_3D : THEORY
BEGIN

  IMPORTING definitions,
            vectors@vect_3D_2D
 
  s,v,
  vo1,vo2 : VAR Vect3
  nzs     : VAR Nz_vect3

  Zv2_vect3  : TYPE = {v | zero_vect2?(v)}
  Nzv2_vect3 : TYPE = {v | nz_vect2?(v)}

  nzv : VAR Nzv2_vect3

  nzv2 : JUDGEMENT
    vect2(nzv) HAS_TYPE Nz_vect2

%%
%% Symmetry breaking
%%

  break_symmetry(s) : Sign = 
    IF s`z > 0 OR 
       s`z = 0 AND s`x > 0 OR
       s`z = 0 AND s`x = 0 AND s`y > 0 THEN 
       1
    ELSE
      -1
    ENDIF

  break_symmetry_neg : LEMMA
    break_symmetry(-nzs) = -break_symmetry(nzs)

%%
%% Kind of Resolutions 
%%

  horizontal_only?(vo1)(vo2) : MACRO bool =
    vo1`z = vo2`z

  gs_only_3D?(vo1)(vo2) : MACRO bool =
    gs_only?(vo1)(vo2) AND
    vo1`z = vo2`z
  
  gsho : JUDGEMENT
    (gs_only_3D?(v)) SUBTYPE_OF (horizontal_only?(v))

  trk_only_3D?(vo1)(vo2) : MACRO bool =
    trk_only?(vo1)(vo2) AND
    vo1`z = vo2`z

  trkho : JUDGEMENT
    (trk_only_3D?(v)) SUBTYPE_OF (horizontal_only?(v))

  vs(v) : real = v`z

  vs_only?(vo1)(vo2) : bool =
    vect2(vo1) = vect2(vo2)

  vs_only_symm : LEMMA
    vs_only?(vo1)(vo2) IFF vs_only?(vo2)(vo1)

END definitions_3D