Email Gateway (Aug 22 2022 at 12:42): Email Gateway (Aug 22 2022 at 12:42):From: Peter Lammich <lammich@in.tum.de>
Consider:
datatype 'a::order undef = Undefined | Defined "'a"
datatype 'a::order node = Node "'a node undef"
The second command raises:
Tactic failed
The error(s) above occurred for the goal statement⌂:
⋀f g. size_node f ∘ map_node g = size_node (f ∘ g)
This does not occur if one removes the sort constraint on undef. The
sort constraint on Node seems to be unrelated.
This behaviour is present in Isabelle2015, and also in 2016-RC3.
(Partial) workaround: The well-known Imperative-HOL hack gives you back
some of the sort contraints:
datatype 'a undef = Undefined | Defined "'a"
setup {* Sign.add_const_constraint
(@{const_name Defined}, SOME @{typ "'a::order ⇒ 'a undef"}) *}
setup {* Sign.add_const_constraint
(@{const_name Undefined}, SOME @{typ "'a::order undef"}) *}
Best,
Peter
Email Gateway (Aug 22 2022 at 12:44):From: Dmitriy Traytel <traytel@inf.ethz.ch>
Hi Peter,
it is a bit too much to expect the datatype package to instantiate the order type class while defining node. I’m actually quite surprised that this works that well: it fails only in the size plugin (which might be fixable by Jasmin), and works if you add a (plugins del: size) annotation to node (you will need to add the size instance for node yourself). This is actually quite better than the old package’s behavior ;-)
theory Scratch imports
"~~/src/HOL/Library/Old_Datatype"
begin
old_datatype 'a::order undef = Undefined | Defined "'a"
old_datatype 'a::order node = Node "'a node undef”
end
Cheers,
Dmitriy
Email Gateway (Aug 22 2022 at 12:44):From: Dmitriy Traytel <traytel@inf.ethz.ch>
I should add: Why this works at all with the new package is, because the bnf structure that constitutes the abstract interface to nested recursion is mostly type-class agnostic, see e.g.
term map_undef
which has no class constraints on the parameters. In contrast the constructors and high-level theorems, such as
thm undef.map
are constrained.
Dmitriy
Email Gateway (Aug 22 2022 at 14:28):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Peter,
Coming back to an old thread:
Another workaround would be to pass (plugins del: size) right after the "datatype" keyword. Then you can define the size function manually.
In any case, I have just pushed a change to Testboard to address this. The change will likely not be part of the next release, but of Isabelle2017, since there are many workarounds.
Cheers,
Jasmin
Last updated: Apr 25 2024 at 12:23 UTC