Email Gateway (Aug 18 2022 at 15:35): Email Gateway (Aug 18 2022 at 15:35):From: 许庆国 <qgxu@mail.shu.edu.cn>
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:37):From: Tobias Nipkow <nipkow@in.tum.de>
Please use algebra_simps now; ring_simps and a number of other special
sets of algebraic simplification rules have been combined into
algebra_simps.
I will update the slides, thanks.
Tobias
许庆国 wrote:
Email Gateway (Aug 18 2022 at 15:39):From: Alex Katovsky <apk32@cam.ac.uk>
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.
Demo2.thy
Last updated: Apr 18 2024 at 16:19 UTC