Definicja

start

Definicja zaczyna się od słowa kluczowego definition, a kończy się słowem end. Definicja zawiera deklarację locusów?, ewentualne złożenia i właściwą definicję lub redefinicję. Poza tym warunki poprawności i ewentualne własności.

definition
  let X be set;
  mode Element of X means
  it in X if X is non empty otherwise it is empty;
  existence by XBOOLE_0:def 1;
  consistency;
  sethood
  proof
   per cases;
   case X is non empty;
    take X;
    thus thesis;
   end;
   case X is empty;
    take {{}};
    let y be set;
    thus thesis by TARSKI:def 1;
   end;
  end;
end;

Definicja elementu zbioru jest przez przypadki: gdy zbiór jest niepusty oraz gdy jest pusty. Stąd warunek poprawności consistency -- jak przypadki się pokrywają, to odpowiadające im definiensy cząstkowe są równoważne. Warunek existence stwierdza istnienie zbioru spełniającego definiens. Udowodniona została własność sethood mówiąca o istnieniu uniwersum definiowanego typu.

definicja warunki poprawności
definition
  let x be Θ;
  attr x is ξ means Φ(x);
end;
nie ma warunków
definition
  let x be Θ;
  attr x is ξ means Φ1(x) if  α1(x),
          .......
         Φn(x) if  αn(x)
         otherwise Φn+1(x);
end;
consistency -- (α1(x) & α2(x) implies (Φ1(x) iff Φ2(x))) & .... & (αn(x) & not α1(x) & ... & not αn(x) implies (Φn(x) iff Φn+1(x)))
definition
  let x be Θ;
  redefine attr x is ξ means Φ'(x);
end;
compatybility -- x is ξ iff Φ'(x);
definition
  let x be Θ;
  mode Θ of x -> Θ' of x means Φ(x,it)
end;
existence -- ex y being Θ' of x st Φ(x,y)
definition
  let x be Θ;
  func ⊕ x -> Θ of x means Φ(x,it);
end;
existence -- ex y being Θ of x st Φ(x,y) ; uniqueness -- for y1,y2 being Θ of x st Φ(x,y1) & Φ(x,y2) holds y1 = y2
definition
  let x be Θ;
  func ⊕ x -> Θ of x equals τ(x);
end;
coherence -- τ is Θ of x
definition
  let x be Θ;
  redefine func ⊕ x -> Θ' of x;
end;
coherence -- ⊕ x is Θ' of x
definition
  let x be Θ;
  redefine func ⊕ x means Φ'(x);
end;
compatybility -- for y being Θ of x holds x = ρ x iff Φ'(x);
definition
  let x be Θ;
  pred ≈ x ->  means Φ(x);
end;
nie ma warunków
definition
  let x be Θ;
  pred ≈ x means Φ1(x) if  α1(x),
          .......
         Φn(x) if  αn(x)
         otherwise Φn+1(x);
end;
consistency -- (α1(x) & α2(x) implies (Φ1(x) iff Φ2(x))) & .... & (αn(x) & not α1(x) & ... & not αn(x) implies (Φn(x) iff Φn+1(x)))
definition
  let x be Θ;
  redefine pred ≈ x means Φ'(x);
end;
compatybility -- ≈ x iff Φ'(x);
WebForm
TopicClassification Select one...
ProjectGroup?

ImplementationDate? N/A
Topic revision: r5 - 2012-02-02 - 15:29:40 - GrzegorzBancerek
 
Mizar TWiki
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback