# HG changeset patch
# User bulwahn
# Date 1324399217 -3600
# Node ID e0305e4f02c9c4fb7a8cec0def7e205944f07cc2
# Parent  f4f22d87e364094fafe96751d12829b07f5f93b9
adding quickcheck generator for distinct lists; adding examples

diff -r f4f22d87e364 -r e0305e4f02c9 src/HOL/Library/Dlist.thy
--- a/src/HOL/Library/Dlist.thy	Tue Dec 20 17:40:15 2011 +0100
+++ b/src/HOL/Library/Dlist.thy	Tue Dec 20 17:40:17 2011 +0100
@@ -180,6 +180,9 @@
 enriched_type map: map
   by (simp_all add: List.map.id remdups_map_remdups fun_eq_iff dlist_eq_iff)
 
+subsection {* Quickcheck generators *}
+
+quickcheck_generator dlist constructors: empty, insert
 
 hide_const (open) member fold foldr empty insert remove map filter null member length fold
 
diff -r f4f22d87e364 -r e0305e4f02c9 src/HOL/ex/Quickcheck_Examples.thy
--- a/src/HOL/ex/Quickcheck_Examples.thy	Tue Dec 20 17:40:15 2011 +0100
+++ b/src/HOL/ex/Quickcheck_Examples.thy	Tue Dec 20 17:40:17 2011 +0100
@@ -6,7 +6,7 @@
 header {* Examples for the 'quickcheck' command *}
 
 theory Quickcheck_Examples
-imports Complex_Main
+imports Complex_Main "~~/src/HOL/Library/Dlist"
 begin
 
 text {*
@@ -342,6 +342,17 @@
 quickcheck[expect = counterexample]
 oops
 
+subsection {* Examples with abstract types *}
+
+lemma
+  "Dlist.length (Dlist.remove x xs) = Dlist.length xs - 1"
+quickcheck[exhaustive]
+oops
+
+lemma
+  "Dlist.length (Dlist.insert x xs) = Dlist.length xs + 1"
+quickcheck[exhaustive]
+oops
 
 subsection {* Examples with Records *}