src/HOL/ex/Quickcheck_Examples.thy
changeset 46337 54227223a8d4
parent 46169 321abd584588
child 46344 b6fbdd3d0915
equal deleted inserted replaced
46336:39fe503602fb 46337:54227223a8d4
   277 lemma
   277 lemma
   278   "(x, z) : rtrancl (R Un S) ==> \<exists> y. (x, y) : rtrancl R & (y, z) : rtrancl S"
   278   "(x, z) : rtrancl (R Un S) ==> \<exists> y. (x, y) : rtrancl R & (y, z) : rtrancl S"
   279 (* FIXME: missing instance for narrowing -- quickcheck[expect = counterexample] *)
   279 (* FIXME: missing instance for narrowing -- quickcheck[expect = counterexample] *)
   280 oops
   280 oops
   281 
   281 
       
   282 subsection {* Examples with the descriptive operator *}
       
   283 
       
   284 lemma
       
   285   "(THE x. x = a) = b"
       
   286 quickcheck[random, expect = counterexample]
       
   287 quickcheck[exhaustive, expect = counterexample]
       
   288 oops
       
   289 
   282 subsection {* Examples with Multisets *}
   290 subsection {* Examples with Multisets *}
   283 
   291 
   284 lemma
   292 lemma
   285   "X + Y = Y + (Z :: 'a multiset)"
   293   "X + Y = Y + (Z :: 'a multiset)"
   286 quickcheck[random, expect = counterexample]
   294 quickcheck[random, expect = counterexample]