# HG changeset patch
# User bulwahn
# Date 1322641269 -3600
# Node ID 3d6ee9c7d7ef89e4fec0c3868f68490798c2e378
# Parent  805a2acf47fdb96a30a3eb30d2a183c4f0ab9447
adding a exception-safe term reification step in quickcheck; adding examples

diff -r 805a2acf47fd -r 3d6ee9c7d7ef src/HOL/Quickcheck_Exhaustive.thy
--- 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 *}
diff -r 805a2acf47fd -r 3d6ee9c7d7ef src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- 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)
diff -r 805a2acf47fd -r 3d6ee9c7d7ef src/HOL/ex/Quickcheck_Examples.thy
--- 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