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



Am 10.06.2014 19:59, schrieb Lars Hupel:
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.
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)"

Dmitriy




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