# HG changeset patch
# User bulwahn
# Date 1326187088 -3600
# Node ID 321abd5845888eca0198a4f9aef3822cb86425e9
# Parent  bef8c811df20746e4d9e68687bd7723adaa80809
adding quickcheck examples with multisets

diff -r bef8c811df20 -r 321abd584588 src/HOL/ex/Quickcheck_Examples.thy
--- a/src/HOL/ex/Quickcheck_Examples.thy	Tue Jan 10 10:17:09 2012 +0100
+++ b/src/HOL/ex/Quickcheck_Examples.thy	Tue Jan 10 10:18:08 2012 +0100
@@ -6,7 +6,7 @@
 header {* Examples for the 'quickcheck' command *}
 
 theory Quickcheck_Examples
-imports Complex_Main "~~/src/HOL/Library/Dlist"
+imports Complex_Main "~~/src/HOL/Library/Dlist" "~~/src/HOL/Library/Multiset"
 begin
 
 text {*
@@ -279,6 +279,25 @@
 (* FIXME: missing instance for narrowing -- quickcheck[expect = counterexample] *)
 oops
 
+subsection {* Examples with Multisets *}
+
+lemma
+  "X + Y = Y + (Z :: 'a multiset)"
+quickcheck[random, expect = counterexample]
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+lemma
+  "X - Y = Y - (Z :: 'a multiset)"
+quickcheck[random, expect = counterexample]
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+lemma
+  "N + M - N = (N::'a multiset)"
+quickcheck[random, expect = counterexample]
+quickcheck[exhaustive, expect = counterexample]
+oops
 
 subsection {* Examples with numerical types *}