Re: [isabelle] 回复: Re: about ring_simps



许庆国 wrote:
> 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  "" ?

You need them. As usual in Isabelle, formulas need to be enclosed in "".
Note that you can ask for more than formula patterns with the Find
command, eg

"_+_" name: induct

which finds all thms with a + in them whose name contains the string induct.

Tobias

> thank you again.
> 
> 2010-07-01 
> 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.
> 
> Alexander.
> 
> 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!
> 
> 
> 2010-07-01 
> q.g. Xu
>   







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