X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Ftests%2Fmatch.ma;h=bc8caa22332b5c4a18bb65e7a941def31f2e47c8;hb=c0f06261e5626228e4681de9973b6412524f09a2;hp=9494d9cc8a3b37a9fa375330dd26ca8828f4c570;hpb=f2f6b3b567d556e732a8ae861ea633b0804840fb;p=helm.git

diff --git a/helm/matita/tests/match.ma b/helm/matita/tests/match.ma
index 9494d9cc8..bc8caa223 100644
--- a/helm/matita/tests/match.ma
+++ b/helm/matita/tests/match.ma
@@ -1,13 +1,28 @@
+(**************************************************************************)
+(*       ___	                                                            *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+
 inductive True: Prop \def
 I : True.
 
 inductive False: Prop \def .
 
 definition Not: Prop \to Prop \def
-\lambda A:Prop. (A \to False).
+\lambda A. (A \to False).
 
 theorem absurd : \forall A,C:Prop. A \to Not A \to C.
-intros.cut False.elim Hcut.apply H1.assumption.
+intros. elim (H1 H).
 qed.
 
 inductive And (A,B:Prop) : Prop \def
@@ -97,13 +112,10 @@ intros.elim n.apply O_S.apply not_eq_S.assumption.
 qed.
 
 
-definition plus : nat \to nat \to nat \def
 let rec plus n m \def 
  match n with 
  [ O \Rightarrow m
- | (S p) \Rightarrow S (plus p m) ]
-in
-plus.
+ | (S p) \Rightarrow S (plus p m) ].
 
 theorem plus_n_O: \forall n:nat. eq nat n (plus n O).
 intros.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption.
@@ -123,13 +135,10 @@ theorem assoc_plus:
 intros.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption.
 qed.
 
-definition times : nat \to nat \to nat \def
 let rec times n m \def 
  match n with 
  [ O \Rightarrow O
- | (S p) \Rightarrow (plus m (times p m)) ]
-in
-times.
+ | (S p) \Rightarrow (plus m (times p m)) ].
 
 theorem times_n_O: \forall n:nat. eq nat O (times n O).
 intros.elim n.simplify.apply refl_equal.simplify.assumption.
@@ -151,16 +160,13 @@ intros.elim n.simplify.apply times_n_O.
 simplify.elim (sym_eq ? ? ? H).apply times_n_Sm.
 qed.
 
-definition minus : nat \to nat \to nat \def
 let rec minus n m \def 
- [\lambda n:nat.nat] match n with 
+ match n with 
  [ O \Rightarrow O
  | (S p) \Rightarrow 
-	[\lambda n:nat.nat] match m with
+	match m with
 	[O \Rightarrow (S p)
-        | (S q) \Rightarrow minus p q ]]
-in
-minus.
+        | (S q) \Rightarrow minus p q ]].
 
 theorem nat_case :
 \forall n:nat.\forall P:nat \to Prop. 
@@ -270,15 +276,13 @@ apply le_S_n.assumption.
 apply le_S_n.assumption.
 qed.
 
-definition leb : nat \to nat \to bool \def
 let rec leb n m \def 
-   [\lambda n:nat.bool] match n with 
+    match n with 
     [ O \Rightarrow true
     | (S p) \Rightarrow
-	[\lambda n:nat.bool] match m with 
+	match m with 
         [ O \Rightarrow false
-	| (S q) \Rightarrow leb p q]]
-in leb.
+	| (S q) \Rightarrow leb p q]].
 
 theorem le_dec: \forall n,m:nat. if_then_else (leb n m) (le n m) (Not (le n m)).
 intros.
@@ -291,6 +295,7 @@ simplify.apply le_n_S.apply H.
 simplify.intros.apply H.apply le_S_n.assumption.
 qed.
 
+(*CSC: this requires too much time
 theorem prova :
 let three \def (S (S (S O))) in
 let nine \def (times three three) in
@@ -300,6 +305,5 @@ let square \def (times eightyone eightyone) in
 intro.
 intro.
 intro.intro.
-STOP normalize goal at (? ? % ?).
-
-
+normalize goal at (? ? % ?).
+*)
\ No newline at end of file