Email Gateway (Aug 18 2022 at 13:25): Email Gateway (Aug 18 2022 at 13:25):From: Peter Lammich <peter.lammich@uni-muenster.de>
I'm currently converting theories from 2008 -> 2009:
I'm using the following definition of conc:
RegSet.conc_def: conc ?A ?B = {xs @ ys |xs ys. xs \<in> ?A \<and> ys
\<in> ?B}
Then I do:
interpretation lc_monoid: monoid_mult "{[]}" conc [...]
text {* Languages with concatenation (*) and union (+) form a semiring
with 1-element @{term "{[]}"} and 0-element @{term "{}"}: *}
interpretation regset_semiring: semiring_1 "{[]}" conc "{}" "op \<union>"
apply (unfold_locales)
apply (auto simp add: conc_def)
done
And get the following error upon the "done" command, i.e. after (!) it
told me "No subgoals".
*** Partially applied constant on left hand side of equation
*** "semiring_1.of_nat {[]} {} op \<union> ?n \<equiv>
semiring_1.of_nat_aux (\<lambda>i. i \<union> {[]}) ?n {}"
*** At command "done".
I do not know what this error message means, nor can I find any
documentation.
In Isabelle2008, the proof worked well.
Many thanks for any hints,
Peter
Email Gateway (Aug 18 2022 at 13:25):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Peter,
The fundamental problem is that interpretation still does not work as
expected with definitions relative to locales. In your case, the
definitions of of_nat and Nats relative to locale semiring_1 make
problems. There is a workaround pattern:
definition
"conc A B = {xs @ ys | xs ys. xs \<in> A \<and> ys \<in> B}"
interpretation lc_monoid: monoid_mult "{[]}" conc
apply unfold_locales
sorry
-- {* define explicit constants for the interpretation results of of_nat
and Nats *}
definition
"regset_of_nat = semiring_1.of_nat {[]} {} (op \<union>)"
definition
"regset_Nats = semiring_1.Nats {[]} {} (op \<union>)"
interpretation regset_semiring: semiring_1 "{[]}" conc "{}" "op
\<union>" where
-- {* fold interpretation results of of_nat and Nats to the
corresponding global constants *}
"semiring_1.of_nat {[]} {} (op \<union>) = regset_of_nat"
and "semiring_1.Nats {[]} {} (op \<union>) = regset_Nats"
proof -
show "semiring_1 {[]} conc {} (op \<union>)"
by unfold_locales (auto simp add: conc_def)
qed (simp_all add: regset_of_nat_def regset_Nats_def)
Ugly, but working; we hope to repair this problem once and forall in
the next Isabelle release.
Hope this helps
Florian
signature.asc
Email Gateway (Aug 18 2022 at 13:26):From: Makarius <makarius@sketis.net>
This is essentially an instance of the problem of "tool compliance" of
morphisms, see also the hints about that in the paper by Chaieb & Wenzel
http://www4.in.tum.de/~wenzelm/papers/context-methods.pdf
Arbitrary data declarations that are included in a locale body (or class
or whatever) are subject to arbitrary transformations performed by other
means later (here locale interpretation). While the primitive logic is
stable under such morphisms (theorems are mapped to theorems etc.),
arbitrary tools are not.
"Tool compliance" means that the transformation by a given morphism
"works" -- what exactly is meant by that depends on the particular tool
(here the code generator).
The usual strategy to prevent breakdowns like above is as follows:
* Internal declarations of tool data (via certain attributes) should be
tolerant against illformed input, i.e. not insist on a certain form,
but give in and ignore the declaration. (This should be
done in way that does not cause too much surprise to the user, maybe
via a suitable warning.)
* The user should be able to modify the environment that results from an
interpretation etc. by adding new declarations of replacement data.
Makarius
Last updated: May 03 2024 at 08:18 UTC