Re: [isabelle] Isabelle2014-RC1: datatype_new fails at recursion through custom bnf
Thanks for the quick reply and the solution.
On 29/07/14 17:52, Dmitriy Traytel wrote:
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.
On 29.07.2014 17:13, Andreas Lochbihler wrote:
Dear BNF developers,
I just want to let you know that in Isabelle2014-RC1, the datatype definition below
fails with "Proof failed".
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"
"('a, 'b) f"
bd: "BNF_Cardinal_Arithmetic.csum natLeq (card_of (UNIV :: 'b set))"
wits: "Abs_f ∘ Inl"
datatype_new 'a foo = Foo int | Bar "('a foo, 'a) f" "('a foo, 'a) f"
This archive was generated by a fusion of
Pipermail (Mailman edition) and