X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda%2Fpreamble.ma;h=c272595a2831f306ed7c12961cda21e2fa35bbf6;hb=30961a10d1cdfd74c4a662082419b717b85d63a6;hp=fa36983af635ee6689a23bfcc09591c61db272d8;hpb=b6a8600c3c4381809f1ab8d3e28628e17d9c3d3d;p=helm.git

diff --git a/matita/matita/contribs/lambda/preamble.ma b/matita/matita/contribs/lambda/preamble.ma
index fa36983af..c272595a2 100644
--- a/matita/matita/contribs/lambda/preamble.ma
+++ b/matita/matita/contribs/lambda/preamble.ma
@@ -14,11 +14,13 @@
 
 include "basics/star.ma".
 include "basics/lists/list.ma".
-include "arithmetics/nat.ma".
+include "arithmetics/exp.ma".
 
 include "xoa_notation.ma".
 include "xoa.ma".
 
+(* logic *)
+
 (* Note: For some reason this cannot be in the standard library *) 
 interpretation "logical false" 'false = False.
 
@@ -26,6 +28,23 @@ notation "⊥"
   non associative with precedence 90
   for @{'false}.
 
+(* relations *)
+
+definition confluent1: ∀A. relation A → predicate A ≝ λA,R,a0.
+                       ∀a1. R a0 a1 → ∀a2. R a0 a2 →
+                       ∃∃a. R a1 a & R a2 a. 
+
+(* Note: confluent1 would be redundant if \Pi-reduction where enabled *)                       
+definition confluent: ∀A. predicate (relation A) ≝ λA,R.
+                      ∀a0. confluent1 … R a0.
+
+(* booleans *)
+
+definition is_false: predicate bool ≝ λb.
+                     false = b.
+
+(* arithmetics *)
+
 lemma lt_refl_false: ∀n. n < n → ⊥.
 #n #H elim (lt_to_not_eq … H) -H /2 width=1/
 qed-.
@@ -70,3 +89,10 @@ lemma tri_gt: ∀A,a1,a2,a3,n1,n2. n2 < n1 → tri A n1 n2 a1 a2 a3 = a3.
 | #n1 #IH #n2 elim n2 -n2 // /3 width=1/
 ]
 qed.
+
+(* lists *)
+
+(* Note: notation for nil not involving brackets *)
+notation > "◊"
+  non associative with precedence 90
+  for @{'nil}.