Email Gateway (Aug 18 2022 at 18:53): Email Gateway (Aug 18 2022 at 18:53):From: Lars Noschinski <noschinl@in.tum.de>
Apart from adhoc-mechanisms on the ML level, there is no such thing in
Isabelle. There have been occasional requests for support of concepts
like 'proof by analogy' or 'without loss of generality'. But to my
knowledge, there haven't been any efforts to implement such a thing.
Support for the really simple cases (like your example, just replace
HeadMap by TailMap everwhere) would probably be just a technical
problem, but often the mathematical notion of "similarly" is quite a bit
wider ...
-- Lars
Email Gateway (Aug 18 2022 at 18:53):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
John Wickerson wrote:
John,
Where what varies is the choice of theorem you could get something like
(and this sort of thing is absolutely routine in my work):
fun mtacs XMap = [ ... ] : tactic list ;
Then use, one time, (EVERY (mtacs HeadMapThm))
and the other time (EVERY (mtacs TailMapThm)).
In your case what differs between the two cases is the choice of the
constant (?)
HeadMap or TailMap, to plug into a particular spot. You could no doubt
work something out involving a variable ?XMap (in place of HeadMap or
TailMap), a subgoal ?XMap = ?XMap, and resolve this with theorems such as
HeadMap = HeadMap (in one instance), or TailMap = TailMap (in the other).
Alternatively, what I have also done on occasions is to create different
strings for use in subgoal_tac or similar
fun string1 XMapstr = .... ^ XMapstr ^ ....
and use
string1 "HeadMap" or string1 "TailMap"
You have to be using the ML interface to Isabelle to do this - which, I
understand, is what ML was originally designed for - and so is
particularly well suited for.
Cheers,
Jeremy
Email Gateway (Aug 18 2022 at 19:03):From: John Wickerson <jpw48@cam.ac.uk>
Hello,
Is there a feature in Isabelle that corresponds to writing "and similarly" in an informal pen-and-paper proof? Specifically, here is a fragment of my proof script:
The two blocks here are identical, except one uses "HeadMap" where the other uses "TailMap". (HeadMap and TailMap are both record constructors.) Is there a neat way to remove the duplication here?
Thanks very much,
John
Email Gateway (Aug 18 2022 at 19:03):From: Steven Obua <steven.obua@googlemail.com>
This question made my day :-)
Cheers,
Steven
Email Gateway (Aug 18 2022 at 19:03):From: Ramana Kumar <rk436@cam.ac.uk>
If you were writing tactics (i.e. using "apply-style" proofs), you could
use function abstraction. For example:
fun foo m = ...
then in the proof:
apply foo HeadMap
next
apply foo TailMap
But this is not very robust, and I don't know if there's anything
equivalent in "proper" (structured) Isar.
Email Gateway (Aug 18 2022 at 19:03):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi John,
the proofs look to me as if they are completely independent of HeadMap and
TailMap. Hence, Isar allows you to abstract over them and prove both goals in
one go:
next
fix HeadOrTailMap
assume "opt1 fN \<circ> HeadOrTailMap g1 = HeadOrTailMap g2 \<circ> fA"
and "opt1 fN' \<circ> HeadOrTailMap g2 = HeadOrTailMap g3 \<circ> fA'"
hence "opt1 fN' \<circ> opt1 fN \<circ> HeadOrTailMap g1 =
HeadOrTailMap g3 \<circ> fA' \<circ> fA"
using o_assoc[of "opt1 fN'" "opt1 fN" "HeadOrTailMap g1"]
and o_assoc[of "opt1 fN'" "HeadOrTailMap g2" "fA"] by auto
hence "opt1 (fN' \<circ> fN) \<circ> HeadOrTailMap g1 =
HeadOrTailMap g3 \<circ> (fA' \<circ> fA)" (is ?thesis)
using opt1_o[of "fN'" "fN"] by auto
thus ?thesis and ?thesis by -
qed
In order to solve both goals, you still must state the "show" or "thus" part
twice, which is why I introduced the ?thesis abbreviation.
Problems with distinct types might cause this approach to fail. In that case,
you can state the above proof as a separate lemma X and then use
qed(erule (2) X)+
instead.
Hope this helps,
Andreas
Email Gateway (Aug 18 2022 at 19:08):From: Makarius <makarius@sketis.net>
Contemporary Isabelle does not really have anything that could be called
"ML interface". There is Isabelle/ML and Isabelle/Isar, and both are
intertwined in a certain way: ML is used for the implementation of Isar,
and Isar embeds ML into its formal context later on in the bootstrapping.
The primary "interface" to the user is the Isar source language (by
definition). It can refer to ML in better ways than ever before in the
history of LCF-style theorem proving. The current Prover IDE
(Isabelle/jEdit) even provides hyperlinks for ML entities and inferred
types. The TTY loop is a bit more awkward here, and in fact close to
being useless.
Taking Isabelle/Isar and Isabelle/ML together, it is possible to define
your own proof methods, say to automate certain standard proof schemes.
This transfers the old LCF idea of user-defined tactics into the world of
Isabelle/Isar, but not much more.
What is conceptually missing is a systematic way to define proof patterns
in a more structured language. Ltac of Coq marks some success in that
respect: it allows users to define tactics quickly without embarking on
details about ML.
Nonetheless, instead of adding a "proof programming language" to Isar, I
conceptually prefer to keep the language as is, and instead empower the
Prover IDE around it. With serious "proof refactoring", which is a
non-trivial thing to provide, one could imaging certain "and similarly
..." operations on the source.
Makarius
Last updated: Apr 16 2024 at 12:28 UTC