Re: [isabelle] Modular definition of type class constants for datatypes with nested recursion



Hi Jasmin,

    instantiation rose :: (foo) foo
    begin
     primrec count_rose where
     "count (Fork a as) = count a + count (map count as)"

     instance ..
    end

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" ("_/ ⊢/ (_ ↓/ _)" [50,0,50] 50)
  assumes ...

Instantiations typically look like this:

instantiation list :: (evaluate) evaluate
begin
  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)"

...

end

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

    thm list.size
    thm rose.size

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 "size"
systematically for all BNF-based datatypes might still serve as an
inspiration.

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 version.

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 happening :-)

Cheers
Lars




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