adding a quickcheck example about functions and sets
authorbulwahn
Sun, 05 Feb 2012 08:57:03 +0100
changeset 46421 5ab496224729
parent 46420 92b629f568c4
child 46422 23936fa78841
child 46423 51259911b9fa
adding a quickcheck example about functions and sets
src/HOL/ex/Quickcheck_Examples.thy
--- a/src/HOL/ex/Quickcheck_Examples.thy	Sun Feb 05 08:47:13 2012 +0100
+++ b/src/HOL/ex/Quickcheck_Examples.thy	Sun Feb 05 08:57:03 2012 +0100
@@ -274,6 +274,11 @@
 quickcheck[exhaustive, expect = counterexample]
 oops
 
+lemma
+  "[| bij_betw f A B; bij_betw f C D |] ==> bij_betw f (A Un C) (B Un D)"
+quickcheck[exhaustive, expect = counterexample]
+oops
+
 
 subsection {* Examples with relations *}