[isabelle] Derive shows with List



Hi,

when trying to derive a "show" class for a datatype, it fails with a
strange error if teh type has nested lists. Find attached a minimal
example.

Am I doing something wrong here?  

Thanks in advance for any help,
  Peter

Isabelle2017 with AFP:

theory Scratch
imports Main   "Show.Show_Instances"
begin

datatype 'a foo = C "'a list"

derive "show" foo

(*
deriving "show" instance for type "Scratch.foo"
generating show-function for type "Scratch.foo"
Proof failed.
 1. (λxa. shows_pl p (shows_string ''C'' (shows_space (pshowsp_list 1
(map (show⇩'⇩a 1) x) (shows_pr p xa))))) =
    (λxa. shows_pl p (shows_string ''C'' (shows_space (pshowsp_list 1
(map (show⇩'⇩a 0) x) (shows_pr p xa)))))
The error(s) above occurred for the goal statement⌂:
showsp_foo show⇩'⇩a p (C x) = shows_pl p ∘ shows_string ''C'' ∘
shows_space ∘ showsp_list show⇩'⇩a 1 x ∘ shows_pr p
*)




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.