[isabelle-dev] Problems with datatype-new

[Dmitriy Traytel]

Hi René,

this is a tactic failure in the recent size extension (the interface 
with fun). We will work on it.

Thanks for the report,
Dmitriy

On 25.06.2014 13:49, René Thiemann wrote:
> 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev