Email Gateway (Aug 19 2022 at 09:26): Email Gateway (Aug 19 2022 at 09:26):From: Alfio Martini <alfio.martini@acm.org>
Dear Isabelle Users,
I was playing with the exercise below, and I wanted to find the
theory where the indexed sum operator is defined.
I tried find_consts name: Sum, but this does not seem to
be the way.
Thanks for any help!
theorem sum02: "∑{0..n::nat} = n * (n+1) div 2" (is "?P n")
proof (induction n)
show "?P 0"
proof -
have "∑{0..0::nat} = 0" by simp
also have "...= 0 * 0" by simp
also have "... = 0 * (0 + 1)" by simp
also have "... = (0 * (0 + 1)) div 2" by simp
finally show ?thesis by this
qed
next
fix x0::nat
assume IH: "?P x0"
show "?P (Suc x0)"
proof -
have "∑{0..(Suc x0)} = ∑{0..x0} + Suc x0" by simp
also have "...= ∑{0..x0} + (x0 + 1)" by simp
also have "...= (x0 * (x0 + 1) div 2) + (x0 + 1)" by (simp
only: IH)
also have "...= (x0 * (x0 + 1) + 2 * x0 + 2) div 2" by simp
also have "...= (x0 * x0 + x0 + 2*x0 + 2) div 2" by simp
also have "...= (x0 * x0 + 3*x0 +2) div 2" by simp
also have "...= (x0 + 1) * (x0 + 2) div 2" by simp
also have "...= Suc x0 * (Suc x0 + 1) div 2" by simp
finally show ?thesis by this
qed
qed
Email Gateway (Aug 19 2022 at 09:26):From: Johannes Hölzl <hoelzl@in.tum.de>
Hi Alfio,
in this case the problem is that "∑ A" (named "Setsum") is a special
syntax for "∑x∈A. x" (named "setsum", note that symbol names are
case-sensitive). It is defined in src/HOL/Big_Operators.thy.
To find "Setsum" using find_consts or find_theorem is quiet hard as it
is just a syntax abbreviation and its more general form "∑x∈A. f x" is
not found when you just search "∑ A".
Luckily with the jEdit interface for Isabelle this gets much easier as
you can Ctrl-click on the constant and jump to its definition.
-Johannes
Email Gateway (Aug 19 2022 at 09:27):From: Makarius <makarius@sketis.net>
That is indeed the way and it is not just by luck, because that is an
important principle of the Prover IDE: what you see as formally checked
source is annotated by aspects of the logical content from the prover.
So you can explore it via tooltips or hyperlinks right in the text.
Sometimes these "aspects" are still missing or only approximative, but the
coverage is increasing over time. So the need for separate diagnostic
commands like find_consts is more and more diminished.
Makarius
Email Gateway (Aug 19 2022 at 09:27):From: Alfio Martini <alfio.martini@acm.org>
Thank you Makarius, Johannes and Lars.
It works fine, although if by chance you click first on the symbol and then
later
press the Control key and then click on the symbol (as I have done many
times)
it won´t work. You must press Control, then hover the cursor over the symbol
and THEN click on the symbol. It took me a while to get it right...:-)
Anyway, this functionality is already mentioned in Christian´s small (and
nice) tutorial on jEdit.
I finally read it.
As many others already mentioned here, jEdit is an awesome tool. It makes
using Isabelle a completely different experience.
It would be great to have a more solid and complete tutorial for the next
release.
I know that you all work very hard, but I still think that could be a
priority amongst
the many things that has to be done.
Best!
Email Gateway (Aug 19 2022 at 09:27):From: Tobias Nipkow <nipkow@in.tum.de>
The interesting part of the functionality of find_consts is search by a given
type (a bit like Hoogle, if you speak Haskell). How do you plan to replace that
by tooltips and hyperlinks?
Tobias
Email Gateway (Aug 19 2022 at 09:27):From: Makarius <makarius@sketis.net>
This is just a different category of application: search over a
"mathematical" library, and really good solutions to that are still
missing. (I am occasionally attending the MKM conference, where people
are discussing that.)
In contrast, the application sketched in this thread, you have your formal
(con)text where you presently work already.
In the past query tools like find_theorems were often re-used to explore
the local proof context, but this can be done more directly. Similarly
replacement of interactive diagnostics can be anticipated for print_cases,
print_facts, "thm calculation", "thm this" etc.
"Big" IDEs for Java do such things routinely. That is conceptually not
such a big deal, and no need to go back to TTY-style commands.
Makarius
Email Gateway (Aug 19 2022 at 09:27):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
On 05/12/2012, at 6:58 AM, Makarius <makarius@sketis.net> wrote:
On Tue, 4 Dec 2012, Tobias Nipkow wrote:
Sometimes these "aspects" are still missing or only approximative, but the coverage is increasing over time. So the need for separate diagnostic commands like find_consts is more and more diminished.
The interesting part of the functionality of find_consts is search by a given type (a bit like Hoogle, if you speak Haskell). How do you plan to replace that by tooltips and hyperlinks?
This is just a different category of application: search over a "mathematical" library, and really good solutions to that are still missing. (I am occasionally attending the MKM conference, where people are discussing that.)
I think that the combination of tooltips/hover links and the existing searches in find_theorems and find_consts is actually pretty good for searching our fact base (think back 10 years when grep was the power tool of choice).
Things can and should certainly be improved, but I wouldn't diminish one kind of tool over the other. Both have their place.
In contrast, the application sketched in this thread, you have your formal (con)text where you presently work already.
In the past query tools like find_theorems were often re-used to explore the local proof context, but this can be done more directly.
I don't agree, that's not how find_theorems gets used most often. It can be, and you're right that that part is better expressed by other methods in an IDE, but there is no way to express a context sensitive term pattern query mixed with negative naming constraints and further refinements in a simple click or tool tip.
We really want both tools. Simple diagnostic information should be easily and directly accessible, and more complex searches for type or term patterns need to be just as well supported. Maybe they can be integrated better (dialogs or similar, although I'm not a fan of these), but that's a different aspect.
Since we're on the IDE topic: one thing that we could make more use of from IDEs is intelligent context sensitive name completion (for constants, types, rules, proof methods, etc). Also, it would help if suggestions were sorted by frequency of use, e.g. "sledgehammer" should be suggested before "sledgehammer_params". Good IDEs excel at that.
I'm not suggesting to aim for any of this in the next release, but if we're looking to improve the user experience in the future, this might make a big difference.
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 19 2022 at 09:28):From: Tobias Nipkow <nipkow@in.tum.de>
Am 04/12/2012 20:58, schrieb Makarius:
On Tue, 4 Dec 2012, Tobias Nipkow wrote:
Sometimes these "aspects" are still missing or only approximative, but the
coverage is increasing over time. So the need for separate diagnostic
commands like find_consts is more and more diminished.The interesting part of the functionality of find_consts is search by a given
type (a bit like Hoogle, if you speak Haskell). How do you plan to replace
that by tooltips and hyperlinks?This is just a different category of application: search over a "mathematical"
library, and really good solutions to that are still missing. (I am
occasionally attending the MKM conference, where people are discussing that.)
I was not talking of the search facility itself (as Gerwin noted, we have a
number of nifty tools beside find_const) but how to invoke it without having to
type the command name. Command completion is already nice, but still crude.
Because the name can be nondescriptive and the parameters unclear. An example of
what I mean: Larry was not aware of the type-based search via find_consts.
Contrast this with the nice box that cmd-f gives you in many tools, eg jedit.
Tobias
In contrast, the application sketched in this thread, you have your formal
(con)text where you presently work already.In the past query tools like find_theorems were often re-used to explore the
local proof context, but this can be done more directly. Similarly replacement
of interactive diagnostics can be anticipated for print_cases, print_facts, "thm
calculation", "thm this" etc."Big" IDEs for Java do such things routinely. That is conceptually not such a
big deal, and no need to go back to TTY-style commands.Makarius
Email Gateway (Aug 19 2022 at 09:28):From: Makarius <makarius@sketis.net>
On Tue, 4 Dec 2012, Gerwin Klein wrote:
This is just a different category of application: search over a
"mathematical" library, and really good solutions to that are still
missing. (I am occasionally attending the MKM conference, where people
are discussing that.)I think that the combination of tooltips/hover links and the existing
searches in find_theorems and find_consts is actually pretty good for
searching our fact base (think back 10 years when grep was the power
tool of choice).
Grep would be "hypersearch" in jEdit, and I am using this a lot. It could
be improved to take the semantic markup into account: search for regular
expressions relative to some XML path context.
Things can and should certainly be improved, but I wouldn't diminish one
kind of tool over the other. Both have their place.
The start of the thread was a confusion about the right tool to use for
the job. What you see already formally in your bit of theory or an
example by someone else does not have to be queried again, it is already
there to be explored.
I have recently brushed up the "find" tools a bit to provide more
hyperlinks in their output for the coming release, such that they can
participate in the game better. Much more could and should be done there,
to get them to the state of the art of potential possibilities of the
present system.
Makarius
Last updated: Apr 25 2024 at 16:19 UTC