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

Hi David,

Now I see that ML's value restriction causes the error. One of the parameters of the enum type class (namely enum) is not of function type. Since its definition 'a ptr does not depend on other type classes' parameters for 'a, the code generator produces a declaration of the form

val enum_ptr = ...

which of course should be polymorphic in the element type, but this is not allowed for val declarations in ML. If you restrict the element type to a type class with type parameters, then the code generator will produce a fun declaration, which may be polymorphic. You can define your own type class such as

class dummy = fixes DUMMY :: "'a itself"

and declare a corresponding code equation:

lemma enum_ptr_code [code]:
  "Enum.enum = (map (Ptr o of_nat) [0 ..< 2 ^ 32] :: 'a :: dummy ptr list)"
by(simp add: enum_ptr_def)

Of course, you have to instantiate this class for all your type constructors that you want to store in a ptr.

instantiation "fun" :: (type, type) dummy begin
definition "DUMMY = TYPE('a ⇒ 'b)"
instance ..

instantiation nat :: dummy begin
definition "DUMMY = TYPE(nat)"
instance ..

Alternatively, you can reuse one of Isabelle/HOL's type classes, e.g. typerep (of which almost every type is an instance of):

lemma enum_ptr_code [code]:
  "Enum.enum = (map (Ptr o of_nat) [0 ..< 2 ^ 32] :: 'a :: typerep ptr list)"
by(simp add: enum_ptr_def)

With this setup, the code generator outputs valid ML code.


On 05/11/14 23:17, David Greenaway wrote:
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

In particular:

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

seems to work fine, but:

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

     lemma "(a :: lifted_globals) = b"

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


     Error: Type 'a ptr list includes a free type variable
        enum_ptra : 'a ptr list =
           map (Ptr o ... ...) (upt Zero_nat (... ... (... ...)))
     At (line 1331 of "generated code")
     Error: Type mismatch in type constraint.
           {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,


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.

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