Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] 回复: about ring_simps

Email Gateway (Aug 18 2022 at 15:36):

From: Tobias Nipkow <nipkow@in.tum.de>
许庆国 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 + 2ab" 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

Email Gateway (Aug 18 2022 at 15:41):

From: 许庆国 <qgxu@mail.shu.edu.cn>
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.

2010-07-01
Q.g., Xu

Last updated: Apr 27 2024 at 01:05 UTC