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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
