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



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.