[isabelle-dev] NEWS: quickcheck with functions

[Stefan Berghofer]

Dear all,

quickcheck can now also display counterexamples involving functions (using
notation for function updates). For example,

   consts app: "('a => 'a) list => 'a => 'a"
   primrec
     "app [] x = x"
     "app (f # fs) x = app fs (f x)"

   lemma "app (fs @ gs) x = app fs (app gs x)"
     quickcheck
     oops

now yields something like

   Counterexample found:

   fs = [arbitrary(0 := -1)]
   gs = [arbitrary(0 := 0, -1 := 0)]
   x = 0

Greetings,
Stefan

-- 
Dr. Stefan Berghofer               E-Mail: berghofe at in.tum.de
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY            http://www.in.tum.de/~berghofe