--- a/src/HOL/Quickcheck_Exhaustive.thy Wed Nov 30 09:21:07 2011 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy Wed Nov 30 09:21:09 2011 +0100
@@ -530,6 +530,15 @@
code_const catch_match
(Quickcheck "(_) handle Match => _")
+definition catch_match' :: "term => term => term"
+where
+ [code del]: "catch_match' t1 t2 = (SOME t. t = t1 \<or> t = t2)"
+
+code_const catch_match'
+ (Quickcheck "(_) handle Match => _")
+
+consts unknown :: "'a" ("?")
+
use "Tools/Quickcheck/exhaustive_generators.ML"
setup {* Exhaustive_Generators.setup *}
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Wed Nov 30 09:21:07 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Wed Nov 30 09:21:09 2011 +0100
@@ -349,6 +349,8 @@
val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_safe_if none_t return ctxt
in lambda depth (mk_test_term t) end
+fun mk_unknown_term T = HOLogic.reflect_term (Const ("Quickcheck_Exhaustive.unknown", T))
+
fun mk_full_generator_expr ctxt (t, eval_terms) =
let
val thy = Proof_Context.theory_of ctxt
@@ -361,9 +363,11 @@
val term_vars = map (fn n => Free (n, @{typ "unit => term"})) term_names
fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v)
val terms = HOLogic.mk_list @{typ term} (map (fn v => v $ @{term "()"}) term_vars)
- val appendC = @{term "List.append :: term list => term list => term list"}
+ fun mk_safe_term t = @{term "Quickcheck_Exhaustive.catch_match' :: term => term => term"}
+ $ (HOLogic.mk_term_of (fastype_of t) t) $ mk_unknown_term (fastype_of t)
+ val appendC = @{term "List.append :: term list => term list => term list"}
val return = @{term "Some :: term list => term list option"} $ (appendC $ terms $
- (HOLogic.mk_list @{typ "term"} (map (fn t => HOLogic.mk_term_of (fastype_of t) t) eval_terms)))
+ (HOLogic.mk_list @{typ "term"} (map mk_safe_term eval_terms)))
fun mk_exhaustive_closure (free as Free (_, T), term_var) t =
if Sign.of_sort thy (T, @{sort enum}) then
Const (@{const_name "Quickcheck_Exhaustive.check_all_class.check_all"}, check_allT T)
--- a/src/HOL/ex/Quickcheck_Examples.thy Wed Nov 30 09:21:07 2011 +0100
+++ b/src/HOL/ex/Quickcheck_Examples.thy Wed Nov 30 09:21:09 2011 +0100
@@ -407,5 +407,24 @@
quickcheck[exhaustive, expect = counterexample]
oops
+subsection {* Examples with underspecified/partial functions *}
+
+lemma
+ "xs = [] ==> hd xs \<noteq> x"
+quickcheck[exhaustive, potential = false, expect = no_counterexample]
+quickcheck[exhaustive, potential = true, expect = counterexample]
+oops
+
+lemma
+ "xs = [] ==> hd xs = x"
+quickcheck[exhaustive, potential = false, expect = no_counterexample]
+quickcheck[exhaustive, potential = true, expect = counterexample]
+oops
+
+lemma "xs = [] ==> hd xs = x ==> x = y"
+quickcheck[exhaustive, potential = false, expect = no_counterexample]
+quickcheck[exhaustive, potential = true, expect = counterexample]
+oops
+
end