]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/nlibrary/TPTP.ma
Progress
[helm.git] / matita / matita / nlibrary / TPTP.ma
1 (*
2 universe constraint Type[0] < Type[1].
3
4 ndefinition o ≝ Prop.
5 naxiom i : Type[0].
6
7 ninductive And (A,B:Prop) : Prop ≝ conj : A → B → And A B.
8 ninductive Exists (A : Type[0]) (P : A → Prop) : Prop ≝ exin : ∀a:A.P a → Exists A P.
9 ninductive Or (A,B:Prop) : Prop ≝ orl : A → Or A B | orr : B → Or A B.
10 ninductive True : Prop ≝ I : True.
11 ninductive False : Prop ≝ .
12 ninductive Not (A : Prop) : Prop ≝ abs : (A → False) → Not A.
13
14 ninductive Eq (a:i) : i → Prop ≝ refl : Eq a a.
15 ndefinition eq1 ≝ λT:Type[0].λp1,p2 : T → Prop. ∀x:T.And (p1 x → p2 x) (p2 x → p1 x).  
16
17 interpretation "eq" 'eq T A B = (Eq A B).
18 interpretation "exteq1" 'eq T A B = (eq1 T A B).
19
20 notation > "'Eq' term 90 A term 90 B" 
21 non associative with precedence 40 for @{'eq ? $A $B}.
22
23 interpretation "TPTP and" 'and A B = (And A B).
24 interpretation "TPTP not" 'not B = (Not B).
25 interpretation "TPTP ex"  'exists f = (Exists ? f).
26 *)
27 include "basics/eq.ma".
28
29 ndefinition o ≝ Prop.
30 naxiom i : Type[0].
31
32 interpretation "myeq" 'myeq T A B = (eq T A B).
33
34 notation > "'Eq' term 90 A term 90 B" 
35 non associative with precedence 40 for @{'myeq ? $A $B}.
36
37 naxiom bool_ext : ∀P,Q: o. (P → Q) → (Q → P) → P = Q.
38 naxiom f_ext_1 : ∀a,b:Type[0].∀f,g: a → b. (∀x.f x = g x) → f = g.