# HG changeset patch
# User bulwahn
# Date 1323348808 -3600
# Node ID 3355c27c93a474bf27acdeb6d9e708c9e01bf615
# Parent  36ea69266e61535e6cf541f447e907ad6768d29a
adding examples for quickcheck narrowing about partial functions

diff -r 36ea69266e61 -r 3355c27c93a4 src/HOL/ex/Quickcheck_Narrowing_Examples.thy
--- a/src/HOL/ex/Quickcheck_Narrowing_Examples.thy	Thu Dec 08 13:53:27 2011 +0100
+++ b/src/HOL/ex/Quickcheck_Narrowing_Examples.thy	Thu Dec 08 13:53:28 2011 +0100
@@ -229,5 +229,42 @@
 quickcheck[tester = narrowing, finite_types = false, default_type = nat, size = 6, expect = counterexample]
 oops
 
+subsection {* Examples with hd and last *}
+
+lemma
+  "hd (xs @ ys) = hd ys"
+quickcheck[narrowing, expect = counterexample]
+oops
+
+lemma
+  "last(xs @ ys) = last xs"
+quickcheck[narrowing, expect = counterexample]
+oops
+
+subsection {* Examples with underspecified/partial functions *}
+
+lemma
+  "xs = [] ==> hd xs \<noteq> x"
+quickcheck[narrowing, expect = no_counterexample]
+oops
+
+lemma
+  "xs = [] ==> hd xs = x"
+quickcheck[narrowing, expect = no_counterexample]
+oops
+
+lemma "xs = [] ==> hd xs = x ==> x = y"
+quickcheck[narrowing, expect = no_counterexample]
+oops
+
+lemma
+  "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)"
+quickcheck[narrowing, expect = no_counterexample]
+oops
+
+lemma
+  "hd (map f xs) = f (hd xs)"
+quickcheck[narrowing, expect = no_counterexample]
+oops
 
 end