# Re: [isabelle] Disproof methods with Word.thy and AutoCorres

Hi Andreas,

Thanks for your suggestions about writing some custom state generators.
I have some ideas about what might be useful testcases in practice.

Generating custom states by inspecting the precondition sounds fun, but
might be a longer-term project. :)

On 05/11/14 20:34, Andreas Lochbihler wrote:
[...]
> I was not able to look at problem 2, because I have not found a small
> example where the ptr causes an exception. If you provide one, I can
> have a look at this, too.

I have attached a small, self-contained example that demonstrates the
problem.

In particular:

lemma "(a :: nat ptr ⇒ nat) = b"
quickcheck

seems to work fine, but:

record lifted_globals =
foo :: "nat ptr ⇒ nat"

lemma "(a :: lifted_globals) = b"
quickcheck

raises one of the errors:

Wellsortedness error
(in code equation equal_lifted_globals_ext_inst.equal_lifted_globals_ext
⦇foo = ?fooa, … = ?morea⦈ ⦇foo = ?foo, … = ?more⦈ ≡
?fooa = ?foo ∧ ?morea = ?more,
with dependency "Pure.dummy_pattern" -> "equal_class.equal [lifted_globals_ext]"):
Type nat ptr ⇒ nat not of sort equal
No type arity ptr :: enum

or:

Error: Type 'a ptr list includes a free type variable
val
enum_ptra : 'a ptr list =
map (Ptr o ... ...) (upt Zero_nat (... ... (... ...)))
At (line 1331 of "generated code")
Error: Type mismatch in type constraint.
Value:
{finite_enum = finite_ptr, enum = enum_ptra, enum_all = enum_all_ptr,
enum_ex = enum_ex_ptr} :
{enum: 'a ptr list,
enum_all: ('b -> bool) -> bool,
enum_ex: ('c -> bool) -> bool, finite_enum: 'd ptr finite}
Constraint: 'a ptr enum
Reason: Can't unify 'a to 'a (Cannot unify with explicit type variable)
{finite_enum = finite_ptr, enum = enum_ptra, enum_all = enum_all_ptr,
enum_ex = ...} : 'a ptr enum
At (line 1351 of "generated code")
Exception- Fail "Static Errors" raised

Depending on whether "ptr" has been instantiated into the "enum" class
or not, respectively.

Thanks for your help,
David

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.