From b9400f08599fa8c36ecf06ac347e966c42db72fc Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 8 Apr 2010 17:49:30 +0000 Subject: [PATCH] ... From: tassi --- helm/software/matita/nlibrary/TPTP.ma | 24 +++ helm/software/matita/nlibrary/depends | 40 ++--- helm/software/matita/nlibrary/depends.dot | 171 +++++++++++++++------- 3 files changed, 163 insertions(+), 72 deletions(-) create mode 100644 helm/software/matita/nlibrary/TPTP.ma diff --git a/helm/software/matita/nlibrary/TPTP.ma b/helm/software/matita/nlibrary/TPTP.ma new file mode 100644 index 000000000..1254f577c --- /dev/null +++ b/helm/software/matita/nlibrary/TPTP.ma @@ -0,0 +1,24 @@ + +universe constraint Type[0] < Type[1]. + +ndefinition o ≝ Prop. +naxiom i : Type[0]. + +ninductive And (A,B:Prop) : Prop ≝ conj : A → B → And A B. +ninductive Exists (A : Type[0]) (P : A → Prop) : Prop ≝ exin : ∀a:A.P a → Exists A P. +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). + +interpretation "eq" 'eq T A B = (Eq A B). +interpretation "exteq1" 'eq T A B = (eq1 T A B). + +notation > "'Eq' term 90 A term 90 B" +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). diff --git a/helm/software/matita/nlibrary/depends b/helm/software/matita/nlibrary/depends index 47d897290..8ef3e1dbd 100644 --- a/helm/software/matita/nlibrary/depends +++ b/helm/software/matita/nlibrary/depends @@ -1,50 +1,52 @@ -overlap/o-algebra.ma sets/categories2.ma +arithmetics/R.ma arithmetics/nat.ma datatypes/pairs.ma datatypes/sums.ma topology/igft.ma algebra/bool.ma logic/connectives.ma +overlap/o-algebra.ma sets/categories2.ma algebra/abelian_magmas.ma algebra/magmas.ma basics/functions.ma Plogic/connectives.ma Plogic/equality.ma Plogic/connectives.ma Plogic/equality.ma arithmetics/nat.ma basics/bool.ma basics/eq.ma basics/functions.ma hints_declaration.ma -datatypes/bool.ma logic/pts.ma datatypes/sums.ma datatypes/pairs.ma logic/destruct_bb.ma logic/equality.ma +datatypes/bool.ma logic/pts.ma logic/equality.ma logic/connectives.ma properties/relations.ma sets/partitions.ma datatypes/pairs.ma nat/compare.ma nat/minus.ma nat/plus.ma sets/sets.ma logic/cprop.ma hints_declaration.ma sets/setoids1.ma -basics/bool.ma basics/eq.ma basics/functions.ma topology/igft.ma logic/equality.ma sets/sets.ma -nat/minus.ma nat/order.ma +basics/bool.ma basics/eq.ma basics/functions.ma algebra/magmas.ma sets/sets.ma +nat/minus.ma nat/order.ma hints_declaration.ma logic/pts.ma arithmetics/Z.ma arithmetics/nat.ma -Plogic/equality.ma logic/pts.ma properties/relations1.ma logic/pts.ma -PTS/gpts.ma PTS/subst.ma -datatypes/list.ma arithmetics/nat.ma -nat/compare.ma datatypes/bool.ma nat/order.ma -algebra/unital_magmas.ma algebra/magmas.ma +arithmetics/compare.ma arithmetics/nat.ma +Plogic/equality.ma logic/pts.ma +TPTP.ma sets/categories.ma sets/sets.ma properties/relations2.ma logic/pts.ma +PTS/gpts.ma PTS/subst.ma +algebra/unital_magmas.ma algebra/magmas.ma +nat/compare.ma datatypes/bool.ma nat/order.ma +datatypes/list.ma arithmetics/nat.ma nat/nat.ma hints_declaration.ma logic/equality.ma sets/setoids.ma logic/connectives.ma logic/pts.ma basics/relations.ma Plogic/connectives.ma basics/list.ma basics/bool.ma basics/eq.ma -basics/list2.ma arithmetics/nat.ma basics/list.ma -topology/igft-setoid.ma sets/sets.ma sets/categories2.ma sets/categories.ma sets/setoids2.ma sets/sets.ma +topology/igft-setoid.ma sets/sets.ma +basics/list2.ma arithmetics/nat.ma basics/list.ma sets/sets.ma hints_declaration.ma logic/connectives.ma logic/cprop.ma properties/relations1.ma sets/setoids1.ma -datatypes/pairs.ma logic/pts.ma -nat/plus.ma algebra/abelian_magmas.ma algebra/unital_magmas.ma nat/big_ops.ma -nat/order.ma nat/nat.ma sets/sets.ma logic/pts.ma -topology/cantor.ma nat/nat.ma topology/igft.ma +nat/order.ma nat/nat.ma sets/sets.ma +nat/plus.ma algebra/abelian_magmas.ma algebra/unital_magmas.ma nat/big_ops.ma +datatypes/pairs.ma logic/pts.ma sets/setoids1.ma hints_declaration.ma properties/relations1.ma sets/setoids.ma -nat/big_ops.ma algebra/magmas.ma nat/order.ma +topology/cantor.ma nat/nat.ma topology/igft.ma sets/setoids2.ma properties/relations2.ma sets/setoids1.ma +nat/big_ops.ma algebra/magmas.ma nat/order.ma topology/igft2.ma arithmetics/nat.ma topology/igft.ma +properties/relations.ma logic/pts.ma PTS/subst.ma basics/list2.ma topology/igft3.ma arithmetics/nat.ma datatypes/bool.ma topology/igft.ma -properties/relations.ma logic/pts.ma -basics/eq.ma basics/relations.ma topology/igft4.ma arithmetics/nat.ma datatypes/bool.ma topology/igft.ma +basics/eq.ma basics/relations.ma sets/setoids.ma hints_declaration.ma logic/connectives.ma properties/relations.ma -topology/igft5.ma arithmetics/nat.ma datatypes/bool.ma topology/igft.ma diff --git a/helm/software/matita/nlibrary/depends.dot b/helm/software/matita/nlibrary/depends.dot index a26055a4e..04e41a5e0 100644 --- a/helm/software/matita/nlibrary/depends.dot +++ b/helm/software/matita/nlibrary/depends.dot @@ -1,81 +1,146 @@ 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 []; "algebra/bool.ma" []; - "algebra/bool.ma" -> "logic/equality.ma" []; + algebra/bool.ma -> logic/connectives.ma []; + "overlap/o-algebra.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 []; + "Plogic/connectives.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 []; + "datatypes/sums.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" []; - "nat/minus.ma" []; - "nat/minus.ma" -> "nat/order.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 []; "algebra/magmas.ma" []; - "algebra/magmas.ma" -> "sets/sets.ma" []; + algebra/magmas.ma -> sets/sets.ma []; + "nat/minus.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 []; "properties/relations1.ma" []; - "properties/relations1.ma" -> "logic/pts.ma" []; + properties/relations1.ma -> logic/pts.ma []; + "arithmetics/compare.ma" []; + arithmetics/compare.ma -> arithmetics/nat.ma []; + "Plogic/equality.ma" []; + Plogic/equality.ma -> logic/pts.ma []; + "TPTP.ma" []; + "sets/categories.ma" []; + sets/categories.ma -> sets/sets.ma []; + "properties/relations2.ma" []; + properties/relations2.ma -> logic/pts.ma []; + "PTS/gpts.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" []; - "logic/connectives.ma" []; - "logic/connectives.ma" -> "logic/pts.ma" []; + nat/compare.ma -> datatypes/bool.ma []; + nat/compare.ma -> nat/order.ma []; + "datatypes/list.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 []; + "basics/relations.ma" []; + basics/relations.ma -> Plogic/connectives.ma []; + "basics/list.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 []; "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 []; "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" []; - "topology/cantor.ma" []; - "topology/cantor.ma" -> "nat/nat.ma" []; - "topology/cantor.ma" -> "topology/igft.ma" []; + datatypes/pairs.ma -> logic/pts.ma []; "sets/setoids1.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 []; + "sets/setoids2.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" -> "topology/igft.ma" []; - "logic/markov.ma" []; - "logic/markov.ma" -> "nat/order.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 []; + "topology/igft3.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 []; + "basics/eq.ma" []; + basics/eq.ma -> basics/relations.ma []; "sets/setoids.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 -- 2.39.2