lstar removed from list.ma and placed in its own file

[helm.git] / matita / matita / contribs / lambda / preamble.ma

diff --git a/matita/matita/contribs/lambda/preamble.ma b/matita/matita/contribs/lambda/preamble.ma
index f3884b229489f7bbe58cd0bde50e28c7086b6833..c272595a2831f306ed7c12961cda21e2fa35bbf6 100644 (file)
--- a/matita/matita/contribs/lambda/preamble.ma
+++ b/matita/matita/contribs/lambda/preamble.ma
@@ -19,10 +19,7 @@ include "arithmetics/exp.ma".
 include "xoa_notation.ma".
 include "xoa.ma".
 
-(* Note: notation for nil not involving brackets *)
-notation > "◊"
-  non associative with precedence 90
-  for @{'nil}.
+(* logic *)
 
 (* Note: For some reason this cannot be in the standard library *) 
 interpretation "logical false" 'false = False.
@@ -31,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-.
@@ -75,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}.