Email Gateway (Aug 18 2022 at 11:46): Email Gateway (Aug 18 2022 at 11:46):From: Cristiano Longo <cristiano.longo@tvblob.com>
Morning all, I have been away from Isabelle for a long time. Now I need
to define inductively a function that takes a set and returns a set of
sets, built inductively starting from the input one.
In the previous versions of Isabelle i used the "induct" construct to do
that, but with the later version its counterpart "induct_set" does not
allow this.
How can I do? The only way is to define a recursive function?
Thanks in advance,
Cristiano Longo
Email Gateway (Aug 18 2022 at 11:46):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear Cristiano,
I have no clear idea what your problem really is. In principial the
inductive_set command should do the job, as in the following (slightly
pointless) example:
inductive_set foo :: "'a set \<Rightarrow> 'a set set"
for A :: "'a set" where
"A \<in> foo A"
| "B \<in> foo A \<Longrightarrow> A \<union> B \<in> foo A"
Could you post a self-contained theory snippet which illustrates your
problem?
Cheers
Florian
signature.asc
Last updated: May 03 2024 at 04:19 UTC