theory PtrTypeQuickcheck
imports "~~/src/HOL/Word/Word"
begin

datatype 'a ptr = Ptr "32 word"

(* Setup "word" and "ptr" types to work with quickcheck. *)

quickcheck_generator word
  constructors:
    "zero_class.zero :: ('a::len) word",
    "numeral :: num \<Rightarrow> ('a::len) word",
    "uminus :: ('a::len) word \<Rightarrow> ('a::len) word"

quickcheck_generator ptr constructors: Ptr

(* This works fine... *)
lemma "(a :: nat ptr \<Rightarrow> nat) = b"
  quickcheck
  oops

(* ...but when we move it into a record... *)
record lifted_globals =
  foo :: "nat ptr \<Rightarrow> nat"

(* This produces an error complaining about the lack of the "enum" class of ptr. *)
lemma "(a :: lifted_globals) = b"
  quickcheck
  oops

(* We can try instantiating "ptr" into the enum class... *)
instantiation ptr :: (type) enum
begin
  definition "enum_ptr \<equiv> map (Ptr o of_nat) [0 ..< 2 ^ 32]"
  definition "enum_all_ptr (P :: 'a ptr \<Rightarrow> bool) \<equiv> Ball UNIV P"
  definition "enum_ex_ptr (P :: 'a ptr \<Rightarrow> bool) \<equiv> Bex UNIV P"
  instance sorry
end

(* ...but not we get the error: "Type 'a ptr list includes a free type variable" *)
lemma "(a :: lifted_globals) = b"
  quickcheck
  oops

end