X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdemo%2Fpower_derivative.ma;h=4f1b44000889a1df1b765d98a29977b8a3b2a432;hb=5649890273cf8e660bba744e84ce5fee1e5efe69;hp=e910c8b6a715c4b89beee7fb220659bd0aea9ec5;hpb=b2a190e3c2d5b594d409db937e88f9f4f7d22b8c;p=helm.git

diff --git a/helm/software/matita/library/demo/power_derivative.ma b/helm/software/matita/library/demo/power_derivative.ma
index e910c8b6a..4f1b44000 100644
--- a/helm/software/matita/library/demo/power_derivative.ma
+++ b/helm/software/matita/library/demo/power_derivative.ma
@@ -277,13 +277,12 @@ theorem derivative_power: ∀n:nat. D[x \sup n] = n·x \sup (pred n).
       suppose (0=m) (m_zero). by _ done.
   conclude
      (D[x \sup (1+m)])
-   = (D[x · x \sup m]) by _.
-   = (D[x] · x \sup m + x · D[x \sup m]) by _.
-   = (x \sup m + x · (m · x \sup (pred m))) by _.
-clear H.
-   = (x \sup m + m · (x \sup (1 + pred m))) by _.
-   = (x \sup m + m · x \sup m) by _.
-   = ((1+m) · x \sup m) by _ (timeout=120)
+   = (D[x · x \sup m]).
+   = (D[x] · x \sup m + x · D[x \sup m]).
+   = (x \sup m + x · (m · x \sup (pred m))).
+   = (x \sup m + m · (x \sup (1 + pred m))).
+   = (x \sup m + m · x \sup m).
+   = ((1+m) · x \sup m) by Fmult_one_f Fmult_commutative Fmult_Fplus_distr costante_sum
   done.
 qed.
 
@@ -320,11 +319,79 @@ theorem derivative_power': ∀n:nat. D[x \sup (1+n)] = (1+n) · x \sup n.
    (D[x \sup (2+m)] = (2+m) · x \sup (1+m)).
   conclude
      (D[x \sup (2+m)])
-   = (D[x · x \sup (1+m)]) by _.
-   = (D[x] · x \sup (1+m) + x · D[x \sup (1+m)]) by _.
-   = (x \sup (1+m) + x · (costante (1+m) · x \sup m)) by _.
-clear H.
-   = (x \sup (1+m) + costante (1+m) · x \sup (1+m)) by _.
-   = (x \sup (1+m) · (costante (2 + m))) by _
-  done.
+   = (D[x · x \sup (1+m)]).
+   = (D[x] · x \sup (1+m) + x · D[x \sup (1+m)]).
+   = (x \sup (1+m) + x · (costante (1+m) · x \sup m)).
+   = (x \sup (1+m) + costante (1+m) · x \sup (1+m)).
+
+
+
+  conclude (x \sup (1+m) + costante (1+m) · x \sup (1+m))
+  = (costante 1 · x \sup (1+m) + costante (1+m) ·(x) \sup (1+m)) proof.
+   by (Fmult_one_f ((x)\sup(1+m)))
+   we proved (costante 1·(x)\sup(1+m)=(x)\sup(1+m)) (previous).
+   by (eq_OF_eq ? ? (λfoo:(R→R).foo+costante (1+m)·(x)\sup(1+m)) (costante 1
+                                                                                                                                                                                                                                       ·(x)\sup(1
+                                                                                                                                                                                                                                                    +m)) ((x)\sup(1
+                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             +m)) previous)
+   done.
+  = ((x)\sup(1+m)·costante 1+costante (1+m)·(x)\sup(1+m)) proof.
+   by (Fmult_commutative (costante 1) ((x)\sup(1+m)))
+   we proved (costante 1·(x)\sup(1+m)=(x)\sup(1+m)·costante 1) (previous).
+   by (eq_f ? ? (λfoo:(R→R).foo+costante (1+m)·(x)\sup(1+m)) (costante 1
+                                                                                                                                                                                                       ·(x)\sup(1+m)) ((x)\sup(1
+                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         +m)
+                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              ·costante
+                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                1) previous)
+   done.
+  = ((x)\sup(1+m)·costante 1+(x)\sup(1+m)·costante (1+m)) proof.
+   by (Fmult_commutative ((x)\sup(1+m)) (costante (1+m)))
+   we proved ((x)\sup(1+m)·costante (1+m)=costante (1+m)·(x)\sup(1+m))
+    
+   (previous)
+   .
+   by (eq_OF_eq ? ? (λfoo:(R→R).(x)\sup(1+m)·costante 1+foo) ((x)\sup(1+m)
+                                                                                                                                                                                                                               ·costante
+                                                                                                                                                                                                                                 (1+m)) (costante
+                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        (1
+                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         +m)
+                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        ·(x)\sup(1
+                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     +m)) previous)
+   done.
+  = ((x)\sup(1+m)·(costante 1+costante (1+m))) proof.
+   by (Fmult_Fplus_distr ((x)\sup(1+m)) (costante 1) (costante (1+m)))
+   we proved
+   ((x)\sup(1+m)·(costante 1+costante (1+m))
+    =(x)\sup(1+m)·costante 1+(x)\sup(1+m)·costante (1+m))
+    
+   (previous)
+   .
+   by (sym_eq ? ((x)\sup(1+m)·(costante 1+costante (1+m))) ((x)\sup(1+m)
+                                                                                                                                                                            ·costante 1
+                                                                                                                                                                            +(x)\sup(1+m)
+                                                                                                                                                                             ·costante (1+m)) previous)
+   done.
+  = ((costante 1+costante (1+m))·(x)\sup(1+m)) 
+  exact (Fmult_commutative ((x)\sup(1+m)) (costante 1+costante (1+m))).
+  = (costante (1+(1+m))·(x)\sup(1+m)) proof.
+   by (costante_sum 1 (1+m))
+   we proved (costante 1+costante (1+m)=costante (1+(1+m))) (previous).
+   by (eq_f ? ? (λfoo:(R→R).foo·(x)\sup(1+m)) (costante 1+costante (1+m)) (costante
+                                                                                                                                                                                                                                                                                                                              (1
+                                                                                                                                                                                                                                                                                                                               +(1
+                                                                                                                                                                                                                                                                                                                                 +m))) previous)
+   done.
+  = (costante (1+1+m)·(x)\sup(1+m)) proof.
+   by (assoc_plus 1 1 m)
+   we proved (1+1+m=1+(1+m)) (previous).
+   by (eq_OF_eq ? ? (λfoo:nat.costante foo·(x)\sup(1+m)) ? ? previous)
+   done.
+  = (costante (2+m)·(x)\sup(1+m)) proof done.
+   by (plus_n_SO 1)
+   we proved (2=1+1) (previous).
+   by (eq_OF_eq ? ? (λfoo:nat.costante (foo+m)·(x)\sup(1+m)) ? ? previous)
+   done.
+  
+ 
+(* end auto($Revision: 8206 $) proof: TIME=0.06 SIZE=100 DEPTH=100 *)  done.
 qed.