Re: [isabelle] Isabelle2014-RC1: datatype_new fails at recursion through custom bnf



Hi Dmitriy,

Thanks for the quick reply and the solution.

Andreas

On 29/07/14 17:52, Dmitriy Traytel wrote:
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

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".

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"






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.