X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fexp.ma;h=11d84f74ca7deb3b676007693f72b585c0547435;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=a80a0cee362fc3fd4024dd565faec8df6d6f4373;hpb=5a702cea95883f7095c16b450e065ccb1714fc5a;p=helm.git

diff --git a/helm/matita/library/nat/exp.ma b/helm/matita/library/nat/exp.ma
index a80a0cee3..11d84f74c 100644
--- a/helm/matita/library/nat/exp.ma
+++ b/helm/matita/library/nat/exp.ma
@@ -21,40 +21,42 @@ let rec exp n m on m\def
  [ O \Rightarrow (S O)
  | (S p) \Rightarrow (times n (exp n p)) ].
 
+interpretation "natural exponent" 'exp a b = (cic:/matita/nat/exp/exp.con a b).
+
 theorem exp_plus_times : \forall n,p,q:nat. 
-eq nat (exp n (plus p q)) (times (exp n p) (exp n q)).
+n \sup (p + q) = (n \sup p) * (n \sup q).
 intros.elim p.
 simplify.rewrite < plus_n_O.reflexivity.
 simplify.rewrite > H.symmetry.
 apply assoc_times.
 qed.
 
-theorem exp_n_O : \forall n:nat. eq nat (S O) (exp n O).
+theorem exp_n_O : \forall n:nat. S O = n \sup O.
 intro.simplify.reflexivity.
 qed.
 
-theorem exp_n_SO : \forall n:nat. eq nat n (exp n (S O)).
+theorem exp_n_SO : \forall n:nat. n = n \sup (S O).
 intro.simplify.rewrite < times_n_SO.reflexivity.
 qed.
 
 theorem exp_exp_times : \forall n,p,q:nat. 
-eq nat (exp (exp n p) q) (exp n (times p q)).
+(n \sup p) \sup q = n \sup (p * q).
 intros.
 elim q.simplify.rewrite < times_n_O.simplify.reflexivity.
 simplify.rewrite > H.rewrite < exp_plus_times.
 rewrite < times_n_Sm.reflexivity.
 qed.
 
-theorem lt_O_exp: \forall n,m:nat. O < n \to O < exp n m. 
-intros.elim m.simplify.apply le_n.
-simplify.rewrite > times_n_SO.
+theorem lt_O_exp: \forall n,m:nat. O < n \to O < n \sup m. 
+intros.elim m.simplify.unfold lt.apply le_n.
+simplify.unfold lt.rewrite > times_n_SO.
 apply le_times.assumption.assumption.
 qed.
 
-theorem lt_m_exp_nm: \forall n,m:nat. (S O) < n \to m < exp n m.
-intros.elim m.simplify.reflexivity.
-simplify.
-apply trans_le ? ((S(S O))*(S n1)).
+theorem lt_m_exp_nm: \forall n,m:nat. (S O) < n \to m < n \sup m.
+intros.elim m.simplify.unfold lt.reflexivity.
+simplify.unfold lt.
+apply (trans_le ? ((S(S O))*(S n1))).
 simplify.
 rewrite < plus_n_Sm.apply le_S_S.apply le_S_S.
 rewrite < sym_plus.
@@ -63,33 +65,33 @@ apply le_times.assumption.assumption.
 qed.
 
 theorem exp_to_eq_O: \forall n,m:nat. (S O) < n 
-\to exp n m = (S O) \to m = O.
+\to n \sup m = (S O) \to m = O.
 intros.apply antisym_le.apply le_S_S_to_le.
-rewrite < H1.change with m < exp n m.
+rewrite < H1.change with (m < n \sup m).
 apply lt_m_exp_nm.assumption.
 apply le_O_n.
 qed.
 
 theorem injective_exp_r: \forall n:nat. (S O) < n \to 
-injective nat nat (\lambda m:nat. exp n m).
+injective nat nat (\lambda m:nat. n \sup m).
 simplify.intros 4.
-apply nat_elim2 (\lambda x,y.exp n x = exp n y \to x = y).
-intros.apply sym_eq.apply exp_to_eq_O n.assumption.
+apply (nat_elim2 (\lambda x,y.n \sup x = n \sup y \to x = y)).
+intros.apply sym_eq.apply (exp_to_eq_O n).assumption.
 rewrite < H1.reflexivity.
-intros.apply exp_to_eq_O n.assumption.assumption.
+intros.apply (exp_to_eq_O n).assumption.assumption.
 intros.apply eq_f.
 apply H1.
 (* esprimere inj_times senza S *)
-cut \forall a,b:nat.O < n \to n*a=n*b \to a=b.
-apply Hcut.simplify. apply le_S_S_to_le. apply le_S. assumption.
+cut (\forall a,b:nat.O < n \to n*a=n*b \to a=b).
+apply Hcut.simplify.unfold lt.apply le_S_S_to_le. apply le_S. assumption.
 assumption.
 intros 2.
-apply nat_case n.
-intros.apply False_ind.apply not_le_Sn_O O H3.
+apply (nat_case n).
+intros.apply False_ind.apply (not_le_Sn_O O H3).
 intros.
-apply inj_times_r m1.assumption.
+apply (inj_times_r m1).assumption.
 qed.
 
 variant inj_exp_r: \forall p:nat. (S O) < p \to \forall n,m:nat.
-(exp p n) = (exp p m) \to n = m \def
-injective_exp_r.
\ No newline at end of file
+p \sup n = p \sup m \to n = m \def
+injective_exp_r.