Email Gateway (Aug 22 2022 at 20:51): Email Gateway (Aug 22 2022 at 20:51):From: Manuel Eberl <eberlm@in.tum.de>
I don't think so. Is there a reason not to simply use "inductive" if you
want this?
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 20:52):From: Tobias Nipkow <nipkow@in.tum.de>
On 08/11/2019 08:57, Manuel Eberl wrote:
I don't think so. Is there a reason not to simply use "inductive" if you
want this?
Yes, you don't get the equality.
Tobias
Cheers,
Manuel
On 07/11/2019 23:22, mailing-list anonymous wrote:
Dear All,
I am curious whether anyone has ever thought about introducing a package
for generating sensible default intro/elim/dest rules from definitions. It
seems that a non-insignificant part of almost every Isabelle/HOL library is
dedicated to the statement and proof of these (often) trivial results.
After all, this has already been partially achieved for certain other
specification elements, e.g. inductive and fun/function. In my view, even
something that produces the desired result 'sufficiently often' would be
considerably better than nothing at all.In summary, I have the following questions:
1). Is the feature that I seek already available (I have encountered quite
a number of similar useful auxiliary features that seem to be
ignored/forgotten)?
2). Does anyone have plans to introduce such a feature in the foreseeable
future?Thank you
Email Gateway (Aug 22 2022 at 20:53):From: Manuel Eberl <eberlm@in.tum.de>
Yes you do. Albeit, admittedly, in a somewhat quirky form:
inductive foo where
"length xs = length ys ⟹ foo xs ys"
thm foo.simps
(* foo ?a1.0 ?a2.0 = (∃xs ys. ?a1.0 = xs ∧ ?a2.0 = ys ∧ length xs =
length ys) *)
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 20:54):From: Lawrence Paulson <lp15@cam.ac.uk>
I’m one of those who does this a lot, or did. I think however that a formulaic generation of intro/elim rules is not that useful. I’ve become more comfortable with beginning a proof with
unfolding blah_def
proof (intro exI conjI impI)
for example, especially when only a few proofs have to start this way. It’s normal to get bogged down in much harder proofs pretty quickly.
Larry Paulson
Email Gateway (Aug 22 2022 at 20:54):From: Tobias Nipkow <nipkow@in.tum.de>
On 08/11/2019 11:59, Manuel Eberl wrote:
Yes you do. Albeit, admittedly, in a somewhat quirky form:
That's why I wrote "the" equality and not "an".
Tobias
inductive foo where
"length xs = length ys ⟹ foo xs ys"thm foo.simps
(* foo ?a1.0 ?a2.0 = (∃xs ys. ?a1.0 = xs ∧ ?a2.0 = ys ∧ length xs =
length ys) *)Cheers,
Manuel
On 08/11/2019 11:51, Tobias Nipkow wrote:
>
>On 08/11/2019 08:57, Manuel Eberl wrote:
I don't think so. Is there a reason not to simply use "inductive" if you
want this?Yes, you don't get the equality.
Tobias
Cheers,
Manuel
On 07/11/2019 23:22, mailing-list anonymous wrote:
Dear All,
I am curious whether anyone has ever thought about introducing a package
for generating sensible default intro/elim/dest rules from
definitions. It
seems that a non-insignificant part of almost every Isabelle/HOL
library is
dedicated to the statement and proof of these (often) trivial results.
After all, this has already been partially achieved for certain other
specification elements, e.g. inductive and fun/function. In my view,
even
something that produces the desired result 'sufficiently often' would be
considerably better than nothing at all.In summary, I have the following questions:
1). Is the feature that I seek already available (I have encountered
quite
a number of similar useful auxiliary features that seem to be
ignored/forgotten)?
2). Does anyone have plans to introduce such a feature in the
foreseeable
future?Thank you
Email Gateway (Aug 22 2022 at 20:54):From: "lammich@in.tum.de" <lammich@in.tum.de>
To get intro rules, I sometimes use xxx_def[THEN iffD2]
Peter
Email Gateway (Aug 22 2022 at 20:54):From: Makarius <makarius@sketis.net>
Results are better if the arguments are treated as parameters, moreover
with fancy postfix notation for rules:
inductive foo for xs ys :: "'a list"
where "foo xs ys" if "length xs = length ys"
print_theorems
(*
theorems:
foo.cases: foo ?xs ?ys ⟹ (length ?xs = length ?ys ⟹ ?P) ⟹ ?P
foo.induct: foo ?xs ?ys ⟹ (length ?xs = length ?ys ⟹ ?Q) ⟹ ?Q
foo.inducts: foo ?xs ?ys ⟹ (length ?xs = length ?ys ⟹ ?Q) ⟹ ?Q
foo.intros: length ?xs = length ?ys ⟹ foo ?xs ?ys
foo.simps: foo ?xs ?ys = (length ?xs = length ?ys)
*)
Makarius
Email Gateway (Aug 22 2022 at 20:55):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear All,
Thank you for your replies: I will make an attempt to respond in a single
message to avoid pollution.
Thank you for your comment. Indeed, I have a tendency to overcomplicate
things from time to time. Nevertheless, I find that if such rules are
provided to the classical reasoning tools consistently and for every
predicate in a library (by specifying attributes intro/elim/dest), then the
Isar proofs can be expressed more concisely and proofs can be obtained
faster because one does not have to worry too much about a multitude of
folds/unfolds/intros/etc. For me, the benefit of having such theorems far
outweighs the disadvantage of having to type 10-20 extra lines of code for
each newly introduced predicate.
I guess, the main conclusion of this thread is that the functionality that
I seek is only available partially as part of the functionality associated
with the command "inductive". It is not unlikely that I will
"rapid-prototype" something that provides more of the functionality that I
seek. However, I doubt I would ever wish to make an attempt to develop it
into a universally applicable and robust framework.
Thank you
Email Gateway (Aug 22 2022 at 21:02):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear All,
I am curious whether anyone has ever thought about introducing a package
for generating sensible default intro/elim/dest rules from definitions. It
seems that a non-insignificant part of almost every Isabelle/HOL library is
dedicated to the statement and proof of these (often) trivial results.
After all, this has already been partially achieved for certain other
specification elements, e.g. inductive and fun/function. In my view, even
something that produces the desired result 'sufficiently often' would be
considerably better than nothing at all.
In summary, I have the following questions:
1). Is the feature that I seek already available (I have encountered quite
a number of similar useful auxiliary features that seem to be
ignored/forgotten)?
2). Does anyone have plans to introduce such a feature in the foreseeable
future?
Thank you
Last updated: Apr 25 2024 at 12:23 UTC