From: Enrico Tassi Date: Tue, 13 Apr 2010 19:51:39 +0000 (+0000) Subject: fixed support file for TPTP X-Git-Tag: make_still_working~2931 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=130d99d356c82501fecb5f3aa1eb708b4d4c8b24;p=helm.git fixed support file for TPTP From: tassi --- diff --git a/helm/software/matita/nlibrary/TPTP.ma b/helm/software/matita/nlibrary/TPTP.ma index 1254f577c..326b673fc 100644 --- a/helm/software/matita/nlibrary/TPTP.ma +++ b/helm/software/matita/nlibrary/TPTP.ma @@ -1,4 +1,4 @@ - +(* universe constraint Type[0] < Type[1]. ndefinition o ≝ Prop. @@ -10,6 +10,7 @@ ninductive Or (A,B:Prop) : Prop ≝ orl : A → Or A B | orr : B → Or A B. ninductive True : Prop ≝ I : True. ninductive False : Prop ≝ . ninductive Not (A : Prop) : Prop ≝ abs : (A → False) → Not A. + ninductive Eq (a:i) : i → Prop ≝ refl : Eq a a. ndefinition eq1 ≝ λT:Type[0].λp1,p2 : T → Prop. ∀x:T.And (p1 x → p2 x) (p2 x → p1 x). @@ -22,3 +23,16 @@ non associative with precedence 40 for @{'eq ? $A $B}. interpretation "TPTP and" 'and A B = (And A B). interpretation "TPTP not" 'not B = (Not B). interpretation "TPTP ex" 'exists f = (Exists ? f). +*) +include "basics/eq.ma". + +ndefinition o ≝ Prop. +naxiom i : Type[0]. + +interpretation "myeq" 'myeq T A B = (eq T A B). + +notation > "'Eq' term 90 A term 90 B" +non associative with precedence 40 for @{'myeq ? $A $B}. + +naxiom bool_ext : ∀P,Q: Prop. (P → Q) → (Q → P) → P = Q. +naxiom f_ext_1 : ∀a,b:Type[0].∀f,g: a → b. (∀x.f x = g x) → f = g. diff --git a/helm/software/matita/nlibrary/depends b/helm/software/matita/nlibrary/depends index 8ef3e1dbd..9c8a7b1c6 100644 --- a/helm/software/matita/nlibrary/depends +++ b/helm/software/matita/nlibrary/depends @@ -1,4 +1,5 @@ arithmetics/R.ma arithmetics/nat.ma datatypes/pairs.ma datatypes/sums.ma topology/igft.ma +SET171^3.ma TPTP.ma algebra/bool.ma logic/connectives.ma overlap/o-algebra.ma sets/categories2.ma algebra/abelian_magmas.ma algebra/magmas.ma @@ -20,7 +21,7 @@ arithmetics/Z.ma arithmetics/nat.ma properties/relations1.ma logic/pts.ma arithmetics/compare.ma arithmetics/nat.ma Plogic/equality.ma logic/pts.ma -TPTP.ma +TPTP.ma basics/eq.ma sets/categories.ma sets/sets.ma properties/relations2.ma logic/pts.ma PTS/gpts.ma PTS/subst.ma diff --git a/helm/software/matita/nlibrary/depends.dot b/helm/software/matita/nlibrary/depends.dot index 04e41a5e0..ebdc8fd34 100644 --- a/helm/software/matita/nlibrary/depends.dot +++ b/helm/software/matita/nlibrary/depends.dot @@ -1,146 +1,149 @@ digraph g { "arithmetics/R.ma" []; - arithmetics/R.ma -> arithmetics/nat.ma []; - arithmetics/R.ma -> datatypes/pairs.ma []; - arithmetics/R.ma -> datatypes/sums.ma []; - arithmetics/R.ma -> topology/igft.ma []; + "arithmetics/R.ma" -> "arithmetics/nat.ma" []; + "arithmetics/R.ma" -> "datatypes/pairs.ma" []; + "arithmetics/R.ma" -> "datatypes/sums.ma" []; + "arithmetics/R.ma" -> "topology/igft.ma" []; + "SET171^3.ma" []; + "SET171^3.ma" -> "TPTP.ma" []; "algebra/bool.ma" []; - algebra/bool.ma -> logic/connectives.ma []; + "algebra/bool.ma" -> "logic/connectives.ma" []; "overlap/o-algebra.ma" []; - overlap/o-algebra.ma -> sets/categories2.ma []; + "overlap/o-algebra.ma" -> "sets/categories2.ma" []; "algebra/abelian_magmas.ma" []; - algebra/abelian_magmas.ma -> algebra/magmas.ma []; + "algebra/abelian_magmas.ma" -> "algebra/magmas.ma" []; "basics/functions.ma" []; - basics/functions.ma -> Plogic/connectives.ma []; - basics/functions.ma -> Plogic/equality.ma []; + "basics/functions.ma" -> "Plogic/connectives.ma" []; + "basics/functions.ma" -> "Plogic/equality.ma" []; "Plogic/connectives.ma" []; - Plogic/connectives.ma -> Plogic/equality.ma []; + "Plogic/connectives.ma" -> "Plogic/equality.ma" []; "arithmetics/nat.ma" []; - arithmetics/nat.ma -> basics/bool.ma []; - arithmetics/nat.ma -> basics/eq.ma []; - arithmetics/nat.ma -> basics/functions.ma []; - arithmetics/nat.ma -> hints_declaration.ma []; + "arithmetics/nat.ma" -> "basics/bool.ma" []; + "arithmetics/nat.ma" -> "basics/eq.ma" []; + "arithmetics/nat.ma" -> "basics/functions.ma" []; + "arithmetics/nat.ma" -> "hints_declaration.ma" []; "datatypes/sums.ma" []; - datatypes/sums.ma -> datatypes/pairs.ma []; + "datatypes/sums.ma" -> "datatypes/pairs.ma" []; "logic/destruct_bb.ma" []; - logic/destruct_bb.ma -> logic/equality.ma []; + "logic/destruct_bb.ma" -> "logic/equality.ma" []; "datatypes/bool.ma" []; - datatypes/bool.ma -> logic/pts.ma []; + "datatypes/bool.ma" -> "logic/pts.ma" []; "logic/equality.ma" []; - logic/equality.ma -> logic/connectives.ma []; - logic/equality.ma -> properties/relations.ma []; + "logic/equality.ma" -> "logic/connectives.ma" []; + "logic/equality.ma" -> "properties/relations.ma" []; "sets/partitions.ma" []; - sets/partitions.ma -> datatypes/pairs.ma []; - sets/partitions.ma -> nat/compare.ma []; - sets/partitions.ma -> nat/minus.ma []; - sets/partitions.ma -> nat/plus.ma []; - sets/partitions.ma -> sets/sets.ma []; + "sets/partitions.ma" -> "datatypes/pairs.ma" []; + "sets/partitions.ma" -> "nat/compare.ma" []; + "sets/partitions.ma" -> "nat/minus.ma" []; + "sets/partitions.ma" -> "nat/plus.ma" []; + "sets/partitions.ma" -> "sets/sets.ma" []; "logic/cprop.ma" []; - logic/cprop.ma -> hints_declaration.ma []; - logic/cprop.ma -> sets/setoids1.ma []; + "logic/cprop.ma" -> "hints_declaration.ma" []; + "logic/cprop.ma" -> "sets/setoids1.ma" []; "topology/igft.ma" []; - topology/igft.ma -> logic/equality.ma []; - topology/igft.ma -> sets/sets.ma []; + "topology/igft.ma" -> "logic/equality.ma" []; + "topology/igft.ma" -> "sets/sets.ma" []; "basics/bool.ma" []; - basics/bool.ma -> basics/eq.ma []; - basics/bool.ma -> basics/functions.ma []; + "basics/bool.ma" -> "basics/eq.ma" []; + "basics/bool.ma" -> "basics/functions.ma" []; "algebra/magmas.ma" []; - algebra/magmas.ma -> sets/sets.ma []; + "algebra/magmas.ma" -> "sets/sets.ma" []; "nat/minus.ma" []; - nat/minus.ma -> nat/order.ma []; + "nat/minus.ma" -> "nat/order.ma" []; "hints_declaration.ma" []; - hints_declaration.ma -> logic/pts.ma []; + "hints_declaration.ma" -> "logic/pts.ma" []; "arithmetics/Z.ma" []; - arithmetics/Z.ma -> arithmetics/nat.ma []; + "arithmetics/Z.ma" -> "arithmetics/nat.ma" []; "properties/relations1.ma" []; - properties/relations1.ma -> logic/pts.ma []; + "properties/relations1.ma" -> "logic/pts.ma" []; "arithmetics/compare.ma" []; - arithmetics/compare.ma -> arithmetics/nat.ma []; + "arithmetics/compare.ma" -> "arithmetics/nat.ma" []; "Plogic/equality.ma" []; - Plogic/equality.ma -> logic/pts.ma []; + "Plogic/equality.ma" -> "logic/pts.ma" []; "TPTP.ma" []; + "TPTP.ma" -> "basics/eq.ma" []; "sets/categories.ma" []; - sets/categories.ma -> sets/sets.ma []; + "sets/categories.ma" -> "sets/sets.ma" []; "properties/relations2.ma" []; - properties/relations2.ma -> logic/pts.ma []; + "properties/relations2.ma" -> "logic/pts.ma" []; "PTS/gpts.ma" []; - PTS/gpts.ma -> PTS/subst.ma []; + "PTS/gpts.ma" -> "PTS/subst.ma" []; "algebra/unital_magmas.ma" []; - algebra/unital_magmas.ma -> algebra/magmas.ma []; + "algebra/unital_magmas.ma" -> "algebra/magmas.ma" []; "nat/compare.ma" []; - nat/compare.ma -> datatypes/bool.ma []; - nat/compare.ma -> nat/order.ma []; + "nat/compare.ma" -> "datatypes/bool.ma" []; + "nat/compare.ma" -> "nat/order.ma" []; "datatypes/list.ma" []; - datatypes/list.ma -> arithmetics/nat.ma []; + "datatypes/list.ma" -> "arithmetics/nat.ma" []; "nat/nat.ma" []; - nat/nat.ma -> hints_declaration.ma []; - nat/nat.ma -> logic/equality.ma []; - nat/nat.ma -> sets/setoids.ma []; + "nat/nat.ma" -> "hints_declaration.ma" []; + "nat/nat.ma" -> "logic/equality.ma" []; + "nat/nat.ma" -> "sets/setoids.ma" []; "logic/connectives.ma" []; - logic/connectives.ma -> logic/pts.ma []; + "logic/connectives.ma" -> "logic/pts.ma" []; "basics/relations.ma" []; - basics/relations.ma -> Plogic/connectives.ma []; + "basics/relations.ma" -> "Plogic/connectives.ma" []; "basics/list.ma" []; - basics/list.ma -> basics/bool.ma []; - basics/list.ma -> basics/eq.ma []; + "basics/list.ma" -> "basics/bool.ma" []; + "basics/list.ma" -> "basics/eq.ma" []; "sets/categories2.ma" []; - sets/categories2.ma -> sets/categories.ma []; - sets/categories2.ma -> sets/setoids2.ma []; - sets/categories2.ma -> sets/sets.ma []; + "sets/categories2.ma" -> "sets/categories.ma" []; + "sets/categories2.ma" -> "sets/setoids2.ma" []; + "sets/categories2.ma" -> "sets/sets.ma" []; "topology/igft-setoid.ma" []; - topology/igft-setoid.ma -> sets/sets.ma []; + "topology/igft-setoid.ma" -> "sets/sets.ma" []; "basics/list2.ma" []; - basics/list2.ma -> arithmetics/nat.ma []; - basics/list2.ma -> basics/list.ma []; + "basics/list2.ma" -> "arithmetics/nat.ma" []; + "basics/list2.ma" -> "basics/list.ma" []; "sets/sets.ma" []; - sets/sets.ma -> hints_declaration.ma []; - sets/sets.ma -> logic/connectives.ma []; - sets/sets.ma -> logic/cprop.ma []; - sets/sets.ma -> properties/relations1.ma []; - sets/sets.ma -> sets/setoids1.ma []; + "sets/sets.ma" -> "hints_declaration.ma" []; + "sets/sets.ma" -> "logic/connectives.ma" []; + "sets/sets.ma" -> "logic/cprop.ma" []; + "sets/sets.ma" -> "properties/relations1.ma" []; + "sets/sets.ma" -> "sets/setoids1.ma" []; "logic/pts.ma" []; "nat/order.ma" []; - nat/order.ma -> nat/nat.ma []; - nat/order.ma -> sets/sets.ma []; + "nat/order.ma" -> "nat/nat.ma" []; + "nat/order.ma" -> "sets/sets.ma" []; "nat/plus.ma" []; - nat/plus.ma -> algebra/abelian_magmas.ma []; - nat/plus.ma -> algebra/unital_magmas.ma []; - nat/plus.ma -> nat/big_ops.ma []; + "nat/plus.ma" -> "algebra/abelian_magmas.ma" []; + "nat/plus.ma" -> "algebra/unital_magmas.ma" []; + "nat/plus.ma" -> "nat/big_ops.ma" []; "datatypes/pairs.ma" []; - datatypes/pairs.ma -> logic/pts.ma []; + "datatypes/pairs.ma" -> "logic/pts.ma" []; "sets/setoids1.ma" []; - sets/setoids1.ma -> hints_declaration.ma []; - sets/setoids1.ma -> properties/relations1.ma []; - sets/setoids1.ma -> sets/setoids.ma []; + "sets/setoids1.ma" -> "hints_declaration.ma" []; + "sets/setoids1.ma" -> "properties/relations1.ma" []; + "sets/setoids1.ma" -> "sets/setoids.ma" []; "topology/cantor.ma" []; - topology/cantor.ma -> nat/nat.ma []; - topology/cantor.ma -> topology/igft.ma []; + "topology/cantor.ma" -> "nat/nat.ma" []; + "topology/cantor.ma" -> "topology/igft.ma" []; "sets/setoids2.ma" []; - sets/setoids2.ma -> properties/relations2.ma []; - sets/setoids2.ma -> sets/setoids1.ma []; + "sets/setoids2.ma" -> "properties/relations2.ma" []; + "sets/setoids2.ma" -> "sets/setoids1.ma" []; "nat/big_ops.ma" []; - nat/big_ops.ma -> algebra/magmas.ma []; - nat/big_ops.ma -> nat/order.ma []; + "nat/big_ops.ma" -> "algebra/magmas.ma" []; + "nat/big_ops.ma" -> "nat/order.ma" []; "topology/igft2.ma" []; - topology/igft2.ma -> arithmetics/nat.ma []; - topology/igft2.ma -> topology/igft.ma []; + "topology/igft2.ma" -> "arithmetics/nat.ma" []; + "topology/igft2.ma" -> "topology/igft.ma" []; "properties/relations.ma" []; - properties/relations.ma -> logic/pts.ma []; + "properties/relations.ma" -> "logic/pts.ma" []; "PTS/subst.ma" []; - PTS/subst.ma -> basics/list2.ma []; + "PTS/subst.ma" -> "basics/list2.ma" []; "topology/igft3.ma" []; - topology/igft3.ma -> arithmetics/nat.ma []; - topology/igft3.ma -> datatypes/bool.ma []; - topology/igft3.ma -> topology/igft.ma []; + "topology/igft3.ma" -> "arithmetics/nat.ma" []; + "topology/igft3.ma" -> "datatypes/bool.ma" []; + "topology/igft3.ma" -> "topology/igft.ma" []; "topology/igft4.ma" []; - topology/igft4.ma -> arithmetics/nat.ma []; - topology/igft4.ma -> datatypes/bool.ma []; - topology/igft4.ma -> topology/igft.ma []; + "topology/igft4.ma" -> "arithmetics/nat.ma" []; + "topology/igft4.ma" -> "datatypes/bool.ma" []; + "topology/igft4.ma" -> "topology/igft.ma" []; "basics/eq.ma" []; - basics/eq.ma -> basics/relations.ma []; + "basics/eq.ma" -> "basics/relations.ma" []; "sets/setoids.ma" []; - sets/setoids.ma -> hints_declaration.ma []; - sets/setoids.ma -> logic/connectives.ma []; - sets/setoids.ma -> properties/relations.ma []; + "sets/setoids.ma" -> "hints_declaration.ma" []; + "sets/setoids.ma" -> "logic/connectives.ma" []; + "sets/setoids.ma" -> "properties/relations.ma" []; } \ No newline at end of file diff --git a/helm/software/matita/nlibrary/depends.png b/helm/software/matita/nlibrary/depends.png index d70a17341..1f81825a8 100644 Binary files a/helm/software/matita/nlibrary/depends.png and b/helm/software/matita/nlibrary/depends.png differ