Re: [isabelle] Modular definition of type class constants for datatypes with nested recursion
instantiation rose :: (foo) foo
primrec count_rose where
"count (Fork a as) = count a + count (map count as)"
thanks, but my real type class is a little bit more complicated. I
guess I should've posted the real thing from the beginning ;-)
class evaluate =
fixes eval :: "rule set ⇒ term ⇒ 'a ⇒ bool" ("_/ ⊢/ (_ ↓/ _)"
Instantiations typically look like this:
instantiation list :: (evaluate) evaluate
primrec eval_list where
"eval_list rs t  ⟷ rs ⊢ t ⟶* Const ''List.list.Nil''" |
"eval_list rs t (x # xs) ⟷ (∃t⇩1 t⇩2. rs ⊢ t⇩1 ↓ x ∧ rs ⊢ t⇩2 ↓ xs ∧
rs ⊢ t ⟶* Const ''List.list.Cons'' $ t⇩1 $ t⇩2)"
Off the top of my head, I don't see any way I could make this cheat
work for this class, because every element of a data type needs to be
mapped with a different function.
You might want to take a look at the BNF-based size extension. Try
to see what it has to offer. I suspect that you could base "count" on
"size_xxx" (e.g. "size_list"). If not, the idiom used to derive
systematically for all BNF-based datatypes might still serve as an
Thanks, I'll have a look. This doesn't seem to be in the Isabelle
2013-2 release, but I have no problem with switching to a repository
The author of this entry is all in favor of porting it to the new
package, and it is, from what I understand, only a matter of time
until he gets to it. ;)
Well, in that case, here's one more person who'd like to see that
This archive was generated by a fusion of
Pipermail (Mailman edition) and