Email Gateway (Aug 18 2022 at 15:36): Email Gateway (Aug 18 2022 at 15:36):From: Peter Gammie <peteg42@gmail.com>
Peter,
I like this approach - thanks for sharing it.
However it seems a bit limited: locale-fixed functions ("choice") are monomorphic, right? In other words, I would need to instantiate this locale at every type I wanted to apply "choice" to. I guess I'm asking for the locale equivalent of the polymorphic SOME.
In any case I think the amount of proof-pain of eliminating choice is pretty much constant whatever the scaffolding is, having tried out a few approaches recently.
cheers
peter
Email Gateway (Aug 18 2022 at 15:36):From: Peter Lammich <peter.lammich@uni-muenster.de>
Peter Gammie wrote:
Unfortunately, that is true. And we also have problems with this limitation.
Best,
Peter
Email Gateway (Aug 18 2022 at 15:39):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Peter,
Anyway, I wanted to follow up your suggestion about using lists. Given the advice in Executable_Set and what you've said to Tjark, would you now suggest Fset instead? If so, can you perhaps sketch for me how Fset is used (there aren't any examples in the distribution)?
a small sketch using a contrived example:
Suppose we have the following operation on sets which shall be implemented:
definition foo :: "nat ⇒ nat set ⇒ nat set" where
"foo n A = insert n {n ∈ A. n mod 2 = 0}"
To turn this executable, we formally define a lifted counterpart
operating on fsets:
definition foo' :: "nat ⇒ nat fset ⇒ nat fset" where
[simp]: "foo' n A = Fset (foo n (member A))"
Note that this should be done as thumb as possible, using the Fset and
member conversions. The more stylized the lifted definition is, the
easier the proofs are. Using [simp] yields reasonable ad-hoc automation.
This definition is immediately followed by its dual, expressing foo in
terms of foo':
lemma [code]:
"foo n A = member (foo' n (Fset A))"
by simp
The final step is to transfer the code equation of foo to a similar code
equation for foo':
lemma [code]:
"foo' n A = Fset.insert n (Fset.filter (\<lambda>n. n mod 2 = 0) A)"
by (simp add: foo_def)
This lifting must be done for all operations involving sets in their
type signature.
I hope to provide automation for this one day.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 15:39):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Peter,
executing choice is a difficult issue. It largely depends on the
scenario. Here a cursory sketch of approaches which I have thought of
until now how to resolve it:
a) Make choice irrelevant for generated code
c.f. src/HOL/ex/Execute_Choice.thy
b) Turn choice into definite choice
e.g. Min { ... } instead of SOME x \<in> { ... }
c) Turn specification non-deterministic using a set-monad
e.g. the pred type defined in src/HOL/Predicate.thy. This means that
instead of using choice in an operation, the operation shall operate on
all suitable elements of a set, returning a set of results. (I have
no example at hand because this is a fresh thought which has not yet
been explored further).
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 15:39):From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi
executing choice is a difficult issue. It largely depends on the
scenario. Here a cursory sketch of approaches which I have thought of
until now how to resolve it:a) Make choice irrelevant for generated code
c.f. src/HOL/ex/Execute_Choice.thy
b) Turn choice into definite choice
e.g. Min { ... } instead of SOME x \<in> { ... }
c) Turn specification non-deterministic using a set-monad
What's about
d) Parameterize over choice-function (e.g. using a locale, fixing
choice and assuming: "s~={} ==> choice s : s"), do your definition
inside this locale
and then instantiate to concrete set implementation ?
Best,
Peter
e.g. the pred type defined in src/HOL/Predicate.thy. This means that
instead of using choice in an operation, the operation shall operate on
all suitable elements of a set, returning a set of results. (I have
no example at hand because this is a fresh thought which has not yet
been explored further).Hope this helps,
Florian
Email Gateway (Aug 18 2022 at 15:39):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Peter,
yes, that is also a possibility. (I had the already the strong
impression that I missed something).
Thanks for pointing this out.
Florian
signature.asc
Last updated: Apr 23 2024 at 20:15 UTC