Email Gateway (Aug 19 2022 at 16:24): Email Gateway (Aug 19 2022 at 16:24):From: Tobias Nipkow <nipkow@in.tum.de>
One reason I sometimes use HOL connectives in premises is that it is more
convenient for forward reasoning: you can write closed_Inter[OF ...]. I don't
know how to do this as compactly if the premise is not atomic.
Tobias
smime.p7s
Email Gateway (Aug 19 2022 at 16:24):From: Joachim Breitner <breitner@kit.edu>
Hi,
good point. I also often want a non-atomic OF.
I might be wrong, butmaybe this is what COMP was about?
New in Isabelle2013 (February 2013)
Discontinued obsolete attribute "COMP". Potential
INCOMPATIBILITY,
use regular rule composition via "OF" / "THEN", or explicit
proof
structure instead.
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 16:24):From: Lawrence Paulson <lp15@cam.ac.uk>
I would guess that in many cases the format of these theorems has been copied from HOL4, where the distinction does not exist. I agree, it is unfortunate. Generally it’s best to express your theorem in the form that is most convenient in its applications (of which there will probably be many) rather than in the proof of the theorem itself (of which there is only one).
Larry Paulson
Email Gateway (Aug 19 2022 at 16:25):From: Johannes Hölzl <hoelzl@in.tum.de>
Yes, this looks like it got lost (missed) in translation from HOL4 or
HOL Light. I try to state theorems using meta-quantifiers, especially
intro rules like closed_Inter.
@Joachim: In your specific case you can also use intro:
lemma "closed (⋂K)"
proof (intro continuous_intros ballI)
fix S assume "S : K" shows "closed S"
...
qed
Email Gateway (Aug 19 2022 at 16:25):From: Peter Lammich <lammich@in.tum.de>
As Johannes already pointed out, you could use intro.
I usually use something like the following in those cases:
proof rule safe
fix S
assume ...
Email Gateway (Aug 19 2022 at 16:25):From: Joachim Breitner <breitner@kit.edu>
Hi,
I guess you mean "proof (rule, safe)". That is even nicer, as in my case
K is a "range f", so this gets resolved as well. Although this seems to
be just a small step from
proof auto
which I believe is frowned upon.
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 16:25):From: Lawrence Paulson <lp15@cam.ac.uk>
I would frown or all of these abbreviations. I see the point of relying on the implicit choice of a rule when you are making various attempts to find a proof. But once you find it, you should invest a little effort in making your proof comprehensible to others and more robust against changes, including the precise change to continuous_intros suggested here. At least “safe" and "clarify" are very controlled in what they do, but “rule” could do almost anything.
Larry Paulson
Email Gateway (Aug 19 2022 at 16:26):From: Makarius <makarius@sketis.net>
COMP was one of these historical relics that are better forgotten, and not
unearthed again. The topic occasionally showed up on the mailing list in
the past decades, just in case you want to know more about its distant
past.
As a rule of thumb, uses of COMP are either very old tools, or based on
general misunderstandings how the system works, or very special
applications somewhere in the system infrastructure itself.
Makarius
http://stop-ttip.org 925,360 people so far
Email Gateway (Aug 19 2022 at 16:42):From: Joachim Breitner <breitner@kit.edu>
Hi,
sometimes I stumble over rules like
lemma closed_Inter [continuous_intros, intro]: "∀S∈K. closed S ⟹ closed (⋂ K)"
that use HOL quantifiers, despite being declared as intros. This is
probably no problem in uses in auto, and may even be required for
whatever continuous_intros is used, but it is certainly inconvenient for
use in Isar:
lemma "closed (⋂K)"
proof
-- Now I have to write
show "∀S∈K. closed S"
-- when I instead want to write
fix S
assume "X ∈ K"
Is that just an historic artifact from when Isar was not there yet, or
is there a deeper reason behind this?
(I’ll be giving an introductory talk on Isabelle next week, and without
this the proofs would be a bit more elegant.)
Greetings,
Joachim
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC