src/HOL/Library/Quickcheck_Narrowing.thy
changeset 42022 101ce92333f4
parent 42021 52551c0a3374
child 42024 51df23535105
--- 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