[isabelle] Fwd: Code generation for typedefs with an invariant


I have a typedef of the form

typedef good_nat = "{n::nat. good n}"

and I have an executable function that produces a "nat list" where I have proven that all entries are good.

How can I lift that to an *executable* function that produces a "good_nat list" instead?

The way I see it, the usual approach of doing a "code abstype" and specifying the code equation in terms of some projection out of the "type with invariant" to "type without invariant" doesn't work here because I have lists of these things.

I do have a workaround involving a second typedef for intermediate results, but it is very boilerplatey and I'd be happy to know if there is something easier.

See attachment for all the details.


theory Test
  imports Main

(* Imagine that this is either difficult to compute or good not computable *)
consts good :: "nat \<Rightarrow> bool"

axiomatization where good_42 [simp]: "good 42" and good_23 [simp]: "good 23"

(* I define a type of good numbers *)
typedef (overloaded) good_nat = "{n::nat. good n}"
  by (rule exI[of _ 23]) auto

lemma [code abstype]: "Abs_good_nat (Rep_good_nat x) = x"
  by (simp add: Rep_good_nat_inverse)

setup_lifting type_definition_good_nat

  Suppose I have some very complicated computation here, but I know it only produces good numbers.
definition my_complicated_computation :: "nat \<Rightarrow> nat list" where
  "my_complicated_computation n = [23, 42] \<comment> \<open>placeholder\<close>"

lemma my_complicated_computation_good: "\<forall>x\<in>set (my_complicated_computation n). good x"
  by (auto simp: my_complicated_computation_def)

  I can now lift that computation such that the goodness information is present in the type:
lift_definition my_complicated_computation' :: "nat \<Rightarrow> good_nat list" is my_complicated_computation
  using my_complicated_computation_good by (auto simp: list.pred_set)

(* But it*s not executable :( *)
value "my_complicated_computation' 13"

(* My workaround: *)

typedef (overloaded) good_nat_list = "{ns::nat list. \<forall>n\<in>set ns. good n}"
  by (rule exI[of _ "[]"]) auto

lemma [code abstype]: "Abs_good_nat_list (Rep_good_nat_list x) = x"
  by (simp add: Rep_good_nat_list_inverse)

setup_lifting type_definition_good_nat_list

lift_definition my_complicated_computation'' :: "nat \<Rightarrow> good_nat_list" is my_complicated_computation
  using my_complicated_computation_good by (auto simp: list.pred_set)

lemma [code]: "Rep_good_nat_list (my_complicated_computation'' x) = my_complicated_computation x"
  by transfer auto

  Now this is executable, but I still have to turn the "good_nat_list" into 
  a "good_nat list" somehow
value "my_complicated_computation'' 13"

lift_definition list_of_good_nat_list :: "good_nat_list \<Rightarrow> good_nat list" is "\<lambda>xs. xs"
  by (auto simp: list.pred_set)

lemma [code]:
  "my_complicated_computation' x = list_of_good_nat_list (my_complicated_computation'' x)"
  by transfer auto

(* Still not executable *)
value "list_of_good_nat_list (my_complicated_computation' 13)"

(* So let's take a brute force approach *)
lift_definition hd_good_nat_list :: "good_nat_list \<Rightarrow> good_nat" is
  "\<lambda>xs. if xs = [] then 23 else hd xs"
  by auto

lift_definition tl_good_nat_list :: "good_nat_list \<Rightarrow> good_nat_list" is tl
  by (auto simp: tl_def)

lift_definition null_good_nat_list :: "good_nat_list \<Rightarrow> bool" is
  "\<lambda>xs. xs = []" .

lemma [code]:
  "list_of_good_nat_list xs =
     (if null_good_nat_list xs then []
      else hd_good_nat_list xs # list_of_good_nat_list (tl_good_nat_list xs))"
  by transfer auto

(* And now it works *)
value "my_complicated_computation' 13"


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