Email Gateway (Aug 22 2022 at 10:53): Email Gateway (Aug 22 2022 at 10:53):From: Julian Brunner <julianbrunner@gmail.com>
Dear all,
I would like to inductively define a set as follows:
locale transition_system =
fixes en :: "'state => 'transition set"
fixes ex :: "'transition => 'state => 'state"
begin
inductive_set paths :: "'state => 'transition list set" where
"[] : paths p" | "a : en p ==> w : paths (ex a p) ==> a # w : paths p"
end
I get the error "Argument types ['state] of paths do not agree with types
[] of declared parameters" (added brackets for clarity). However, I cannot
declare this parameter using a for clause, since it is not fixed ("ex a p"
vs. "p").
I was under the impression that the inductive_set command simply uses
inductive to define a predicate and then composes this predicate with
Collect to obtain the set representation. However, it seems that
inductive_set is strictly weaker than inductive.
As of now, I am working around this by doing what I thought inductive_set
was doing by hand. However, this results in quite a lot of boilerplate
since all the introduction, elimination and induction rules have to be
transferred by hand. Is there a reason why the inductive_set command cannot
do this for me?
Julian
Email Gateway (Aug 22 2022 at 10:54):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Julian,
This restriction is well-known and just a matter of not having ever been implemented.
Historically, inductive_set existed before inductive and at that time, the implementation
could not handle non-fixed parameters. Later, the more general inductive has been
implemented and inductive_set was replaced with a wrapper around inductive. The wrapper
was designed just to support whatever the old inductive_set could do. However, there is no
reason for inductive_set not being able to handle changing parameters. It is just a matter
of generalising the implementation. If you have time to attack this, I guess many people
will be happy (including me).
I've mentioned the restriction in
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2015-February/msg00038.html and
gave a few examples in
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2015-May/msg00084.html. The latter
post also contains an example how to emulate the behaviour of inductive_set without too
much trouble. A preliminary version of this can be found in one of my posts on stackoverflow
http://stackoverflow.com/a/16604803
Best,
Andreas
Last updated: Nov 21 2024 at 12:39 UTC