Email Gateway (Aug 22 2022 at 10:36): Email Gateway (Aug 22 2022 at 10:36):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Jasmin,
Another application of the Ctr_Sugar/BNF machinery would be generating selector equations
from a record specification or specifying a record via its selectors. Here is an example
of what I have in mind:
record point =
x :: nat
y :: nat
definition my_point :: point where "my_point = (| x = 5, y = 7 |)"
Now, I have to manually state and derive
lemma point_sel:
"x my_point = 5"
"y my_point = 7"
by(simp_all add: my_point_def)
Conversely, it seems sensible to specify records by their fields, as in
record_definition my_point :: point where "x my_point = 5" | "y my_point = 7"
which could internally derive
my_point_ctr: "my_point = (| x = 5; y = 7 |)"
Johannes Hölzl has changed the definition of the complex numbers to a codatatype to be
able to use primcorec which does these conversions already internally. Is there already
something similar for extensible records which I have missed?
Best,
Andreas
Email Gateway (Aug 22 2022 at 10:36):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Andreas,
Another application of the Ctr_Sugar/BNF machinery would be generating selector equations from a record specification or specifying a record via its selectors. Here is an example of what I have in mind:
…
Johannes Hölzl has changed the definition of the complex numbers to a codatatype to be able to use primcorec which does these conversions already internally. Is there already something similar for extensible records which I have missed?
No, there is nothing like that. I think the key would be to extend “primcorec” to work with arbitrary “ctr_sugar”s that have selectors, by building a degenerate corecursor (term) from the case constant. This would be fairly easy. I might even have a student to work on this.
Cheers,
Jasmin
Last updated: Apr 24 2024 at 08:20 UTC