[Maxima] factorials and binomials simplification - nusum less verbose

[giovanni gherdovich]

--0-1316448935-1152640638=:97215
Content-Type: text/plain; charset=iso-8859-1

Thankyou Richard and Robert, you answered completely to my questions.

>matchdeclare([a,b],true);
>defrule(h,binomial(a,b),(a+b)!/a!/b!);
>apply1(…, h);
>minfactorial(%);
    >will simplify the example you give, 

Just for the sake of understanding:

matchdeclare([a,b],true);

This command makes Maxima able to apply the following rule

defrule(h,binomial(a,b),(a+b)!/a!/b!);

wherever it finds something like "binomial(n,k)", whatever the domain of n and k is, isn't it?

>> I'd like to avoid the string "Dependent equations eliminated:  (1)".
>From looking at the code from which that message originates >(src/solve.lisp),
>it appears that linsolvewarn : false; should disable that message.
>I didn't try that.

Yes, the command 
linsolvewarn:false
makes the linear solver silent, and it's what I want.

>> I'm using Maxima within the theorem prover Hol Light, through an >>interface
>> written by John Harrison.

>Hmm, that sounds interesting. Maybe you can tell us more about this.

A theorem prover, like Hol Light, is (roughly speaking) a programming language in wich the code you write is a mathematical proof. If the code runs, the proof was correct and you get a theorem (if you agree with the Hol axioms!).
But it cannot find any result by itself, it can only check if a result is correct (producing a formal proof of it).
So it's very different from a Computer Algebra System, wich can find the answers, but without giving the proofs.
A very interesting mix is ask Maxima for the answers, and then check them by Hol to get formal theorems.
I was encouraged to this approach by the last chapter of the Hol Tutorial (page 206), http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial_220.pdf , were I found the interface I'm using.

Thankyou again.

Giovanni Gherdovich

 Chiacchiera con i tuoi amici in tempo reale! 
 http://it.yahoo.com/mail_it/foot/*http://it.messenger.yahoo.com 
--0-1316448935-1152640638=:97215
Content-Type: text/html; charset=iso-8859-1

Thankyou Richard and Robert, you answered completely to my questions.<br><br><div class="MsoNormal"><font color="navy" face="Arial" size="2"><span style="font-size: 10pt; font-family: Arial; color: navy;">&gt;matchdeclare([a,b],true);<o:p></o:p></span></font><br>&gt;defrule(h,binomial(a,b),(a+b)!/a!/b!);<o:p></o:p><br>&gt;apply1(…, h);<br>&gt;minfactorial(%);</div><font color="navy" face="Arial" size="2"><span style="font-size: 10pt; font-family: Arial; color: navy;"></span></font>    <font color="navy" face="Arial" size="2"><span style="font-size: 10pt; font-family: Arial; color: navy;">&gt;will simplify the example you give, </span></font><br><br>Just for the sake of understanding:<br><font color="navy" face="Arial" size="2"><span style="font-size: 10pt; font-family: Arial; color: navy;"><br><span style="color: rgb(0, 0, 0);">matchdeclare([a,b],true);</span><br style="color: rgb(0, 0, 0);"><br style="color: rgb(0, 0, 0);"><span style="color: rgb(0, 0, 0);">This command
 makes Maxima able to apply the following rule</span><br style="color: rgb(0, 0, 0);"><br style="color: rgb(0, 0, 0);"></span></font><font color="navy" face="Arial" size="2"><span style="font-size: 10pt; font-family: Arial; color: navy;"><span style="color: rgb(0, 0, 0);">defrule(h,binomial(a,b),(a+b)!/a!/b!);</span><br style="color: rgb(0, 0, 0);"><br style="color: rgb(0, 0, 0);"><span style="color: rgb(0, 0, 0);">wherever it finds something like "binomial(n,k)", whatever the domain of n and k is, isn't it?</span><br><br></span></font>&gt;&gt; I'd like to avoid the string "Dependent equations eliminated:  (1)".<br>&gt;From looking at the code from which that message originates &gt;(src/solve.lisp),<br>&gt;it appears that linsolvewarn : false; should disable that message.<br>&gt;I didn't try that.<br><font color="navy" face="Arial" size="2"><span style="font-size: 10pt; font-family: Arial; color: navy;"><br>Yes, the command <br>linsolvewarn:false<br></span></font>makes the
 linear solver silent, and it's what I want.<br><br>&gt;&gt; I'm using Maxima within the theorem prover Hol Light, through an &gt;&gt;interface<br>&gt;&gt; written by John Harrison.<br><br>&gt;Hmm, that sounds interesting. Maybe you can tell us more about this.<br><br>A theorem prover, like Hol Light, is (roughly speaking) a programming language in wich the code you write is a mathematical proof. If the code runs, the proof was correct and you get a theorem (if you agree with the Hol axioms!).<br>But it cannot find any result by itself, it can only check if a result is correct (producing a formal proof of it).<br>So it's very different from a Computer Algebra System, wich can find the answers, but without giving the proofs.<br>A very interesting mix is ask Maxima for the answers, and then check them by Hol to get formal theorems.<br>I was encouraged to this approach by the last chapter of the Hol Tutorial (page 206), http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial_220.pdf
 , were I found the interface I'm using.<br><br>Thankyou again.<br><br>Giovanni Gherdovich<br><p>&#32;Chiacchiera con i tuoi amici in tempo reale! <br> http://it.yahoo.com/mail_it/foot/*http://it.messenger.yahoo.com 
--0-1316448935-1152640638=:97215--