Isabelle's Code generation: Abstraction lemmas for containers?

Question

I am experimenting with the Code generator. My theory contains a datatype that encodes an invariant:

typedef small = "{x::nat. x < 10}" morphisms to_nat small
  by (rule exI[where x = 0], simp)

definition "is_one x ⟷ x = small 1"

Now I want to export code for is_one. It seems that I first have to set up the data type for the code generator as follows:

code_datatype small

instantiation small :: equal
begin
  definition "HOL.equal a b ⟷ to_nat a = to_nat b" 
  instance
  apply default
  unfolding equal_small_def
  apply (rule to_nat_inject)
  done
end

lemma [code abstype]: "small (to_nat x) = x" by (rule to_nat_inverse)

And now I am able to define a code equation for is_one that does not violate the abstraction:

definition [code del]:"small_one = small 1"
declare is_one_def[code del]
lemma [code]: "is_one x ⟷ x = small_one" unfolding is_one_def small_one_def..
lemma [code abstract]: "to_nat small_one = 1"
  unfolding small_one_def by (rule small_inverse, simp)

export_code is_one in Haskell file -

Question 1: Can I avoid pulling the definition of small_one out of is_one?

Now I have a compound value of small items:

definition foo :: "small set list" where "foo = [ {small (10-i), small i} . i <- [2,3,4] ]"

In that form, I cannot export code using it (“Abstraction violation in code equation foo...”).

Question 2: How do I define an [code abstract] lemma for such a value? It seems that the code generator does not accept lemmas of the form map to_nat foo = ....

Answer 1

For types with invariants declared by code_abstract such as small, no code equation may contain the abstraction function small. Consequently, if you want the equality test in is_one to be expressed on type small, you have to define a constant for small 1 and prove the corresponding code equation with to_nat first. This is what you have done. However, it would be easier to use equality on the representation type nat, i.e., inline the implementation equal_class.equal; then, you do not need to instantiate equal for small either.

lemma is_one_code [code]: "is_one x ⟷ to_nat x = 1"
by(cases x)(simp add: is_one_def small_inject small_inverse)

The lifting package does most of this for you automatically:

setup_lifting type_definition_small
lift_definition is_one :: "small => bool" is "%x. x = 1" ..
export_code is_one in SML file -

Unfortunately, the code generator does not support compound return types that involve abstract types like in small set list. As described in Data Refinement in Isabelle/HOL, sect. 3.2, you have to wrap the type small set list as a type constructor small_set_list of its own and define foo with type small_set_list. The type small_set_list is then represented as nat set list with the invariant list_all (%A. ALL x:A. x < 10).

Answer 2

Besides Andreas' explanation and comprehensive solution, I found a work-around that avoids introducing a new type. Assume foo is not used in many places, say, only in

definition "in_foo x = (∀s ∈ set foo. x ∈ s)"

Trying to export code for in_foo gives the "Abstraction violation" error. But using program refinement, I can avoid the problematic code:

I use code_thms to find out how foo is used and find that it is used as list_all (op ∈ ?x) foo. Now I rewrite this particular use of foo without mentioning small:

lemma [code_unfold]:
  "list_all (op ∈ x) foo ⟷
    list_all (op ∈ (to_nat x))  [ {(10-i), i} . i <- [2, 3, 4] ]"
  unfolding foo_def by (auto simp add: small_inverse small_inject)

(Had I defined foo using lift_definition, the proof after apply transfer would be even simpler.)

After this transformation, which essentially captures that all members of foo fulfill the invariant of small, the code export works as intended:

export_code in_foo in Haskell file -