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

Am 10.06.2014 21:56, schrieb Dmitriy Traytel:
Am 10.06.2014 19:59, schrieb Lars Hupel:
Hi Jasmin,

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

     instance ..

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
  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.
If I understand it correctly, here really the same trick as for the size function can be done: one uses two versions of the function:

* eval :: "rule set => term => 'a :: evaluate list => bool"
* eval_list :: "rule set => (term => 'a => bool) => term => 'a list => bool"

s.t. "eval rs = eval_list rs (eval rs :: term => 'a :: evaluate => bool)"

For lists eval_list would be defined by:

primrec eval_list where
"eval_list rs ev t [] ⟷ rs ⊢ t ⟶* Const ''List.list.Nil''" |
"eval_list rs ev t (x # xs) ⟷ (∃t1 t2. ev t1 x ∧ eval_list rs ev t2 xs ∧ rs ⊢ t ⟶* Const ''List.list.Cons'' $ t1 $ t2)"

Then for rose trees:

datatype_new 'a tree = Node 'a "'a tree list"

primrec eval_tree where
  "eval_tree rs ev u (Node a us) = (∃t ts. ev t a ∧
     eval_list rs (λt f. f t) ts (map (λu t. eval_tree rs ev t u) us) ∧
     rs ⊢ u ⟶* Const ''Scratch.tree.Node'' $ t $ ts)"

And the class instantiation again via

  "eval rs = eval_tree rs (eval rs :: term => 'a :: evaluate => bool)"


BTW: hopefully something like "eval_list rs (λt f. f t) ts (map (λu t. eval_tree rs ev t u) us) = eval_list rs (eval_tree rs ev) ts us" will be provable, such that one can get nice equations (similarly to what you tried after Florian's suggestion hitting the syntactic restriction of primrec).


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