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

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.


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"
  map: map_f
  sets: set_f
  bd: "BNF_Cardinal_Arithmetic.csum natLeq (card_of (UNIV :: 'b set))"
  wits: "Abs_f ∘ Inl"
  rel: rel_f

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.