Email Gateway (Aug 19 2022 at 15:06): Email Gateway (Aug 19 2022 at 15:06):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear BNF developers,
I just want to let you know that in Isabelle2014-RC1, the datatype definition below fails
with "Proof failed".
Best,
Andreas
typedef ('a, 'b) f = "UNIV :: ('a + 'b) set" by auto
consts map_f :: "('a ⇒ 'b) ⇒ ('a, 'c) f ⇒ ('b, 'c) f"
consts set_f :: "('a, 'b) f ⇒ 'a set"
consts rel_f :: "('a ⇒ 'b ⇒ bool) ⇒ ('a, 'c) f ⇒ ('b, 'c) f ⇒ bool"
bnf
"('a, 'b) f"
map: map_f
sets: set_f
bd: "BNF_Cardinal_Arithmetic.csum natLeq (card_of (UNIV :: 'b set))"
wits: "Abs_f ∘ Inl"
rel: rel_f
sorry
datatype_new 'a foo = Foo int | Bar "('a foo, 'a) f" "('a foo, 'a) f"
Email Gateway (Aug 19 2022 at 15:06):From: Dmitriy Traytel <traytel@in.tum.de>
Hi Andreas,
using certain ubiquitous constants (like ∘ or Inl) in terms for the BNF
constants always used to be a little bit fragile (since internal tactics
treat those constants specially). We continuously try to improve the
situation here.
However this is not critical for the release: the easy workaround is to
define a constant for the witness:
definition "wit_f = Abs_f ∘ Inl"
and use wit_f in the bnf command.
Dmitriy
Email Gateway (Aug 19 2022 at 15:07):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Dmitriy,
Thanks for the quick reply and the solution.
Andreas
Last updated: May 06 2024 at 12:29 UTC