# HG changeset patch
# User bulwahn
# Date 1300468782 -3600
# Node ID 1bd4b6d1c482470dda00a2f8e99f635fb0fa26aa
# Parent  101ce92333f49baf55d08e46de370c25f67f0e91
adding minimalistic setup and transformation to handle functions as data to enable naive function generation for Quickcheck_Narrowing

diff -r 101ce92333f4 -r 1bd4b6d1c482 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 18 18:19:42 2011 +0100
@@ -9,12 +9,19 @@
   val compile_generator_expr:
     Proof.context -> term -> int -> term list option * Quickcheck.report option
   val put_counterexample: (unit -> term list option) -> Proof.context -> Proof.context
+  val finite_functions : bool Config.T
   val setup: theory -> theory
 end;
 
 structure Narrowing_Generators : NARROWING_GENERATORS =
 struct
 
+(* configurations *)
+
+val (finite_functions, setup_finite_functions) =
+  Attrib.config_bool "quickcheck_finite_functions" (K true)
+
+
 fun mk_undefined T = Const(@{const_name undefined}, T)
 
 (* narrowing specific names and types *)
@@ -178,23 +185,27 @@
 )
 
 val put_counterexample =  Counterexample.put
-  
+
+fun finitize_functions t = t
+
 fun compile_generator_expr ctxt t size =
   let
     val thy = ProofContext.theory_of ctxt
+    val t' = if Config.get ctxt finite_functions then finitize_functions t else t
     fun ensure_testable t =
       Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
-    val t = dynamic_value_strict
+    val result = dynamic_value_strict
       (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
-      thy (Option.map o map) (ensure_testable t) [] size
+      thy (Option.map o map) (ensure_testable t') [] size
   in
-    (t, NONE)
+    (result, NONE)
   end;
 
 
 val setup =
   Datatype.interpretation
     (Quickcheck_Common.ensure_sort_datatype (@{sort narrowing}, instantiate_narrowing_datatype))
+  #> setup_finite_functions
   #> Context.theory_map
     (Quickcheck.add_generator ("narrowing", compile_generator_expr))
     
diff -r 101ce92333f4 -r 1bd4b6d1c482 src/HOL/ex/Quickcheck_Narrowing_Examples.thy
--- a/src/HOL/ex/Quickcheck_Narrowing_Examples.thy	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/ex/Quickcheck_Narrowing_Examples.thy	Fri Mar 18 18:19:42 2011 +0100
@@ -30,13 +30,24 @@
 oops
 
 lemma "rev xs = xs"
-  quickcheck[tester = narrowing, finite_types = false, default_type = int]
+  quickcheck[tester = narrowing, finite_types = false, default_type = int, expect = counterexample]
 oops
 
 lemma "rev xs = xs"
+  quickcheck[tester = narrowing, finite_types = true, expect = counterexample]
+oops
+
+subsection {* Simple examples with functions *}
+
+declare [[quickcheck_finite_functions]]
+
+lemma "map f xs = map g xs"
   quickcheck[tester = narrowing, finite_types = true]
 oops
 
+lemma "map f xs = map f ys ==> xs = ys"
+  quickcheck[tester = narrowing, finite_types = true]
+oops
 
 subsection {* AVL Trees *}