[isabelle-dev] Problems with datatype-new

[René Thiemann]

Dear all,

I have an unexpected problem when defining a datatype using datatype_new.

theory Test
imports  
  "$AFP/Collections/ICF/impl/RBTSetImpl"
begin
datatype_new ('a,'b) bar = Foo 'a "'b option" "'b rs"

(*
Proof failed.
 1. ⋀g ga h.
       local.bar.ctor_rec_bar
        (λx. case local.bar.Rep_bar_pre_bar x of (l, la, xa) ⇒ h (g l) (map_option (λx. x) la) xa) =
       local.bar.ctor_rec_bar (λx. case local.bar.Rep_bar_pre_bar x of (x1, xa, xb) ⇒ h (g x1) xa xb)
The error(s) above occurred for the goal statement⌂:
⋀g ga h. local.bar.rec_bar h ∘ local.bar.map_bar g = local.bar.rec_bar (λx. h (g x))*)
end

The problem vanishes if I make the datatype slightly more easier, e.g., if
- I declare 'a or 'b as dead
- 'b option or 'b rs is changed to pure 'b
- 'a is dropped

Just wanting to report this,
René

Isabelle: 52dfde98be4a
AFP: 23c1c5591d9f