[isabelle] Code-Generator/Nitpick for HOLCF Datatype



Hi,
I am using a datatype defined by the "domain" keyword from HOLCF. There seems to be no "out of the box" support for nitpick/quickcheck and "value".

What is the best way to make them work?


The use case is streams (also called lazy-lists):

theory DomainTest
imports HOLCF begin

default_sort countable
domain 'a stream = lscons "'a discr u" (lazy "'a stream") (infixr "&&" 40)

value "⊥::(nat stream)"         (* Error *)
value "((Iup (Discr 1)) && ⊥)"  (* Error *)

lemma "someStream = (otherStream :: (nat stream))"
  quickcheck    (* Error *)
  nitpick       (*Timeout *)

fixrec makeOnes ::"'a stream → nat stream" where
"x≠⊥ ⟹ makeOnes⋅(x&&xs) = ((Iup (Discr 1)) && (makeOnes⋅xs))"

lemma "makeOnes⋅someValue = ((Iup (Discr 1)) && ⊥)"
  quickcheck  (* Error *)

value "makeOnes⋅((Iup (Discr 2)) && ⊥)"  (* Error *)

end


Thank you for the help.
Sincerely,

Sebastian





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