Working with Isabelle's code generator: Data refinement and higher order functions

Question

This is a follow-up on Isabelle's Code generation: Abstraction lemmas for containers?:

I want to generate code for the_question in the following theory:

theory Scratch imports Main begin

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

definition a_pred :: "small ⇒ bool"
  where "a_pred = undefined"

definition "smaller j = [small i . i <- [0 ..< to_nat j]]" 

definition "the_question j = (∀i ∈ set (smaller j). a_pred j)"

The problem is that the equation for smaller is not suitable for code generation, as it mentions the abstraction function small.

Now according to Andreas’ answer to my last question and the paper on data refinement, the next step is to introduce a type for sets of small numbers, and create a definition for smaller in that type:

typedef small_list = "{l. ∀x∈ set l. (x::nat) < 10}" by (rule exI[where x = "[]"], auto)
code_datatype Abs_small_list
lemma [code abstype]: "Abs_small_list (Rep_small_list x) = x" by (rule Rep_small_list_inverse)

definition "smaller' j = Abs_small_list [ i . i <- [0 ..< to_nat j]]"
lemma smaller'_code[code abstract]: "Rep_small_list (smaller' j) = [ i . i <- [0 ..< to_nat j]]"
  unfolding smaller'_def
  by (rule Abs_small_list_inverse, cases j, auto elim: less_trans simp add: small_inverse)

Now smaller' is executable. From what I understand I need to redefine operations on small list as operations on small_list:

definition "small_list_all P l = list_all P (map small (Rep_small_list l))"

lemma[code]: "the_question j = small_list_all a_pred (smaller' j)"
  unfolding small_list_all_def the_question_def smaller'_code smaller_def Ball_set by simp

I can define a good looking code equation for the_question. But the definition of small_list_all is not suitable for code generation, as it mentions the abstraction morphismsmall. How do I make small_list_all executable?

(Note that I cannot unfold the code equation of a_pred, as the problem actually occurs in the code equation of the actually recursive a_pred. Also, I’d like to avoid hacks that involve re-checking the invariant at runtime.)

Answer 1

The short answer is no, it does not work.

The long answer is that there are often workarounds possible. One is shown by Brian in his answer. The general idea seems to be

Separate the function that has the abstract type in covariant positions besides the final return value (i.e. higher order functions or functions returning containers of abstract values) into multiple helper functions so that abstract values are only constructed as a single return value of one of the helper function.

In Brian’s example, this function is predecessor. Or, as another simple example, assume a function

definition smallPrime :: "nat ⇒ small option"
  where "smallPrime n = (if n ∈ {2,3,5,7} then Some (small n) else None)"

This definition is not a valid code equation, due to the occurrence of small. But this derives one:

definition smallPrimeHelper :: "nat ⇒ small"
  where "smallPrimeHelper n = (if n ∈ {2,3,5,7} then small n else small 0)"
lemma [code abstract]: "to_nat (smallPrimeHelper n) = (if n ∈ {2,3,5,7} then n else 0)"
  by (auto simp add: smallPrimeHelper_def intro: small_inverse)
lemma [code_unfold]: "smallPrime n = (if n ∈ {2,3,5,7} then Some (smallPrimeHelper n) else None)"
  unfolding smallPrime_def smallPrimeHelper_def by simp

If one wants to avoid the redundant calculation of the predicate (which might be more complex than just ∈ {2,3,5,7}, one can make the return type of the helper smarter by introducing an abstract view, i.e. a type that contains both the result of the computation, and the information needed to construct the abstract type from it:

typedef smallPrime_view = "{(x::nat, b::bool). x < 10 ∧ b = (x ∈ {2,3,5,7})}"
  by (rule exI[where x = "(2, True)"], auto)
setup_lifting type_definition_small
setup_lifting type_definition_smallPrime_view

For the view we have a function building it and accessors that take the result apart, with some lemmas about them:

lift_definition smallPrimeHelper' :: "nat ⇒ smallPrime_view"
  is "λ n. if n ∈ {2,3,5,7} then (n, True) else (0, False)" by simp
lift_definition smallPrimeView_pred :: "smallPrime_view ⇒ bool"
  is "λ spv :: (nat × bool) . snd spv" by auto
lift_definition smallPrimeView_small :: "smallPrime_view ⇒ small"
  is "λ spv :: (nat × bool) . fst spv" by auto
lemma [simp]: "smallPrimeView_pred (smallPrimeHelper' n) ⟷ (n ∈ {2,3,5,7})"
  by transfer simp
lemma [simp]: "n ∈ {2,3,5,7} ⟹ to_nat (smallPrimeView_small (smallPrimeHelper' n)) = n"
  by transfer auto
lemma [simp]: "n ∈ {2,3,5,7} ⟹ smallPrimeView_small (smallPrimeHelper' n) = small n"
  by (auto intro: iffD1[OF to_nat_inject] simp add: small_inverse)

With that we can derive a code equation that does the check only once:

lemma [code]: "smallPrime n = 
  (let spv = smallPrimeHelper' n in
   (if smallPrimeView_pred spv
    then Some (smallPrimeView_small spv)
    else None))"
   by (auto simp add: smallPrime_def Let_def)

Answer 2

I don't have a good solution to the general problem, but here's an idea that will let you generate code for the_question in this particular case.

First, define a function predecessor :: "small ⇒ small with an abstract code equation (possibly using lift_definition from λn::nat. n - 1).

Now you can prove a new code equation for smaller whose rhs uses if-then-else, predecessor and normal list operations:

lemma smaller_code [code]:
  "smaller j = (if to_nat j = 0 then []
    else let k = predecessor j in smaller k @ [k])"

(More efficient implementations are of course possible if you're willing to define an auxiliary function.)

Code generation should now work for smaller, since this code equation doesn't use function small.