# HG changeset patch
# User bulwahn
# Date 1300468782 -3600
# Node ID 101ce92333f49baf55d08e46de370c25f67f0e91
# Parent  52551c0a337417eb9982e64f16a99541e06e0b8c
adding a simple datatype for representing functions in Quickcheck_Narrowing

diff -r 52551c0a3374 -r 101ce92333f4 src/HOL/Library/Quickcheck_Narrowing.thy
--- a/src/HOL/Library/Quickcheck_Narrowing.thy	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Library/Quickcheck_Narrowing.thy	Fri Mar 18 18:19:42 2011 +0100
@@ -468,4 +468,17 @@
 hide_const (open) int_of of_int nth error toEnum map_index split_At empty
   cons conv nonEmpty "apply" sum cons1 cons2 ensure_testable
 
+subsubsection {* Defining a simple datatype to represent functions in an incomplete and redundant way *}
+
+datatype ('a, 'b) ffun = Constant 'b | Update 'a 'b "('a, 'b) ffun"
+
+primrec eval_ffun :: "('a, 'b) ffun => 'a => 'b"
+where
+  "eval_ffun (Constant c) x = c"
+| "eval_ffun (Update x' y f) x = (if x = x' then y else eval_ffun f x)"
+
+hide_type (open) ffun
+hide_const (open) Constant Update eval_ffun
+
+
 end
\ No newline at end of file