Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Code-Generator/Nitpick for HOLCF Datatype

Email Gateway (Aug 22 2022 at 19:41):

From: Sebastian Stüber <sebastian.stueber@t-online.de>
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

Last updated: Apr 24 2024 at 08:20 UTC