Email Gateway (Aug 22 2022 at 11:31): Email Gateway (Aug 22 2022 at 11:31):From: Rustom Mody <rustompmody@gmail.com>
Thanks Harry
On Wed, Oct 21, 2015 at 2:11 PM, Harry Butterworth <heb1001@gmail.com>
wrote:
Your star is the wrong star character. Maybe you have cut and pasted from
a pdf document. That doesn't work.Yeah I started with
https://www.lri.fr/~wenzel/Isabelle_Paris_2014/slides.pdf
And was looking for a source/thy version of that...
With the version below...
theory sum
imports Main
begintheorem
fixes n::nat
shows "(∑ i =0.. n . i ) = n * ( n + 1) div 2"...I get the output
proof (prove): depth 0
goal (1 subgoal):
1. ∑{0..n} = n * (n + 1) div 2Harry
My current thy file is attached.
It has about a dozen 'red-marks' :-)
sum.thy
Email Gateway (Aug 22 2022 at 11:31):From: Harry Butterworth <heb1001@gmail.com>
Here you go...
theory sum
imports Main
begin
theorem
fixes n :: nat
shows "(\<Sum> i =0.. n . i ) = n * ( n + 1) div 2"
proof ( induct n )
case 0
have "(\<Sum> i =0..0. i ) = (0:: nat )" by simp
also have "… = 0 * (0 + 1) div 2" by simp
finally show ?case .
next
case ( Suc n )
have "(\<Sum> i =0.. Suc n . i ) = (\<Sum> i =0.. n . i ) + ( n + 1)" by
simp
also have "… = n * ( n + 1) div 2 + ( n + 1)" by ( simp add : Suc.hyps )
also have "… = ( n * ( n + 1) + 2 * ( n + 1)) div 2" by simp
also have "… = ( Suc n * ( Suc n + 1)) div 2" by simp
finally show ?case .
qed
Email Gateway (Aug 22 2022 at 11:32):From: Rustom Mody <rustompmody@gmail.com>
Thanks Harry!
Email Gateway (Aug 22 2022 at 11:32):From: Rustom Mody <rustompmody@gmail.com>
On Wed, Oct 21, 2015 at 3:50 PM, Rustom Mody <rustompmody@gmail.com> wrote:
On Wed, Oct 21, 2015 at 3:01 PM, Harry Butterworth <heb1001@gmail.com>
wrote:Here you go...
Thanks Harry!
Tried another small example
From http://www4.in.tum.de/~wenzelm/papers/Calculations-Isar.pdf
I managed to copy-paste and remove all red-marks :-)
[thy file below]
So now a more basic question
How do I know that the proof is done?
In more detail
Cursor on "finally", output window shows:
proof (chain): depth 0
picking this:
⋃{X, Y, {}} = ⋃{X, Y}
calculation: ⋃{X, Y, {}} = ⋃{X, Y}
Cursor on "qed" output window shows:
theorem ⋃{?X, ?Y, {}} = ⋃{?X, ?Y}
Looks quite arcane to me and nothing quite says "Proved!"
So where/how do I know this proof is successful?
----------------------- union.thy --------------
theory union
imports Main
begin
theorem "\<Union>{X , Y , {}} = \<Union>{X , Y }"
proof -
have "\<Union>{X , Y , {}} = \<Union>({X , Y } \<union> {{}})" by auto
also have "... = \<Union>{X , Y } \<union> \<Union>{{}}" by auto
also have "... = \<Union>{X , Y } \<union> {}" by auto
also have "... = \<Union>{X , Y }" by auto
finally show "\<Union>{X , Y , {}} = \<Union>{X , Y }" .
qed
Email Gateway (Aug 22 2022 at 11:32):From: Lars Hupel <hupel@in.tum.de>
So now a more basic question
How do I know that the proof is done?
You know that if the system is done processing and doesn't complain
(i.e. nothing is highlighted in whatever color or underlined in red).
There's also the possibility to check a theory in "batch mode" outside
of the editor. In Isabelle terminology, this is called "building a
session". Refer to §2 in the system manual for details. A simple example
for your theory would be to create a file "ROOT" with the following
contents:
session Your_Session_Name = HOL +
theories
Your_Theory_Name
... and then invoking "isabelle build -v -D ." in that directory.
Cheers
Lars
Email Gateway (Aug 22 2022 at 11:32):From: Peter Lammich <lammich@in.tum.de>
A theorem is proved, if you finish its proof (by qed or done).
Isabelle outputting "theorem" means that it is a proved theorem.
If you give the theorem a name, you can also use the command
thm name
to display the theorem later.
However, be careful with the asynchronous processing of the prover IDE:
Only if there are no errors in the theories before your theory (check
the "Theories"-panel), you have really proven the theorem. Otherwise, it
might depend on unproven stuff! E.g.
lemma f: False by simp -- "There will be an error here, but False
will be registered by name f anyway!"
theorem "1=2" using f by simp
-- "This outputs: theorem 1=2, and, locally, you cannot distinguish
that from a valid proof"
To be sure that a theory is valid, without having to inspect the open
theories for errors (which gets cumbersome for large developments, even
using the theories panel), you have to use the batch-build mode of
Isabelle.
So, summarized, to develop your own theories, you use the IDE. To verify
theories of others, you should use batch-build, which also excludes
cheating by the sorry-command.
Email Gateway (Aug 22 2022 at 11:48):From: Rustom Mody <rustompmody@gmail.com>
In paper https://www.lri.fr/~wenzel/Isabelle_Paris_2014/slides.pdf
there is the example of sum of first n integers.
Quite stuck at 'outer/inner' syntax errors.
Is there somewhere I can find the full example so that I can study it?
Also:
Spent some hours figuring out what is 'sorry'
Which manual answers such questions?
Finally if there is a more noob-list than this one please let me know!
Email Gateway (Aug 22 2022 at 11:48):From: Lars Noschinski <noschinl@in.tum.de>
On 21.10.2015 06:06, Rustom Mody wrote:
In paper https://www.lri.fr/~wenzel/Isabelle_Paris_2014/slides.pdf
there is the example of sum of first n integers.Quite stuck at 'outer/inner' syntax errors.
Is there somewhere I can find the full example so that I can study it?
It is customary to omit the quotation marks ("), when type-setting
Isabelle theories -- these need to surround every (non-atomic)
expression of the inner syntax.
Refering to slide 24 of the above document, "inner syntax" is everything
printed in cursive, except the proofs (which are proceeded by "by").
For starting, I would recommend to look at "Programming and Proving in
Isabelle/HOL".
Also:
Spent some hours figuring out what is 'sorry'
Which manual answers such questions?
The Isabelle/Isar Reference Manual (look at the index at the end of the
document). Be warned that this is a reference manual -- if you do not
already understand how the system works, many explanations are hard to
understand.
Finally if there is a more noob-list than this one please let me know!
No, this is the right list.
-- Lars
Email Gateway (Aug 22 2022 at 11:48):From: Rustom Mody <rustompmody@gmail.com>
Thanks Lars!
On Wed, Oct 21, 2015 at 11:14 AM, Lars Noschinski <noschinl@in.tum.de>
wrote:
On 21.10.2015 06:06, Rustom Mody wrote:
In paper https://www.lri.fr/~wenzel/Isabelle_Paris_2014/slides.pdf
there is the example of sum of first n integers.Quite stuck at 'outer/inner' syntax errors.
Is there somewhere I can find the full example so that I can study it?It is customary to omit the quotation marks ("), when type-setting
Isabelle theories -- these need to surround every (non-atomic)
expression of the inner syntax.
Maybe so
But I think I am stuck on something much more preliminary
The example starts with
theorem
fixes "n :: nat"
shows "(∑ i =0.. n . i ) = n ∗ ( n + 1) div 2"
etc
[assuming that's how the quotes should be put
But it looks that Isabelle (or should I be saying Isar?) wants some prefix
like
theory sum
imports Main
begin
which gives the following at theorem
Outer syntax error⌂: proposition expected,
but keyword (⌂ was found
Refering to slide 24 of the above document, "inner syntax" is everything
printed in cursive, except the proofs (which are proceeded by "by").For starting, I would recommend to look at "Programming and Proving in
Isabelle/HOL".Also:
Spent some hours figuring out what is 'sorry'
Which manual answers such questions?The Isabelle/Isar Reference Manual (look at the index at the end of the
document). Be warned that this is a reference manual -- if you do not
already understand how the system works, many explanations are hard to
understand.Finally if there is a more noob-list than this one please let me know!
No, this is the right list.
Good to know!
Email Gateway (Aug 22 2022 at 11:48):From: Harry Butterworth <heb1001@gmail.com>
Your star is the wrong star character. Maybe you have cut and pasted from
a pdf document. That doesn't work.
With the version below...
theory sum
imports Main
begin
theorem
fixes n::nat
shows "(∑ i =0.. n . i ) = n * ( n + 1) div 2"
...I get the output
proof (prove): depth 0
goal (1 subgoal):
Harry
Last updated: Nov 21 2024 at 12:39 UTC