[isabelle] 回复: Re: about ring_simps

Hi Katovsky,

   thanks for your reply and giving a good solution.
As to  Emacs command "proof-find-theorems" you have mentioned, I have tried the pattern  (_+_)^2
the following message answers me.
*** Outer syntax error: keyword ")" expected,
*** but symbolic identifier _+_ was found
 the pattern "(_+_)^2" works fine.

what's the play about the quotation marks  "" ?

thank you again.

Q.g., Xu

From:  Alex Katovsky 
Date:  2010-07-01  15:54:19 
To:  许庆国 
Cc:  isabelle-users 
Subject:  Re: [isabelle] about ring_simps 
Hi Xu,

If you replace "ring_simps" by "power2_sum power2_diff" then it works.  There are a few more problems with the file (I have attached one that compiles).  In general, if you are looking for a theorem, you can search for it by using the Emacs command "proof-find-theorems", which is bound to the key sequence "C-c C-f".  In this case, you would search for 

Find theorems containing: "(_+_)^2"

And the search returns what we are looking for in this case.


On 07/01/2010 02:42 AM, 许庆国 wrote: 
Hello everyone:

    I am learning Isabelle through the the website: http://isabelle.in.tum.de/coursematerial/PSV2009-1/index.html  
  When I am tring to check the file thttp://isabelle.in.tum.de/coursematerial/PSV2009-1/session78/Demo2.thy.
  the following message shows:
    *** Unknown fact "ring_simps"
	*** At command "by".
in the process of proving              
  lemma fixes a :: int shows "(a+b)2 <= 2*(a2 + b2)" 
  also have "(a+b)2 £ a2 + b2 + 2*a*b"  by(simp add:numeral_2_eq_2 ring_simps

Now my Isabells's version is Isabelle 2009-2.

How to correct this error? 
thanks a lot in advance!

q.g. Xu

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.