[isabelle] Code generator setup for lazy lists

Dear all,

I am wondering how I can efficiently implement a conversion function list_of between the subset of finite lists from the type of possibly infinite lists (as defined in AFP-Coinductive) and ordinary lists from the HOL image.

At present, the code equations for list_of are as follows in the AFP:

list_of LNil = []
list_of (LCons x xs) = (if lfinite xs then x # list_of xs else undefined)

This way, the finiteness test is executed once for every element of the list, which makes conversion quadratic in the length of the list. Now, I would like to execute the finiteness test at most a constant number of times by exploiting that finiteness is preserved through all recursive calls. I hope that I can do this with the code generator's support for invariants. So far, I came up with the following:

(* Identify the subset of the type that is of interest *)
typedef (open) 'a llist_fin = "{xs :: 'a llist. lfinite xs}"
  morphisms llist_of_fin Abs_llist_fin
  show "LNil : ?llist_fin" by simp

(* Setup the abstype *)
lemma llist_of_fin_Abs_llist_fin [simp, code abstype]:
  "Abs_llist_fin (llist_of_fin xs) = xs"
by(rule llist_fin.llist_of_fin_inverse)

(* Define the abstract operation *)
definition list_of2 :: "'a llist_fin => 'a list"
where "list_of2 xs = list_of (llist_of_fin xs)"

(* Prove a new code equation for list_of that uses the abstract operation *)
lemma list_of_code [code]:
  "list_of xs = (if lfinite xs then list_of2 (Abs_llist_fin xs) else undefined)"
by(simp add: list_of2_def Abs_llist_fin_inverse list_of_def Abs_llist_fin2_def)

Now, I am stuck at two problems:
1. list_of_code uses the abstraction function Abs_llist_fin, which the code generator does not allow. But from the calling context, I know that all assumptions are satisfied.

2. I have no idea how to state the code equations for list_of2. I would imagine something like

"list_of2 (Abs_llist_fin LNil) = []"
"lfinite xs ==> list_of2 (Abs_llist_fin (LCons x xs)) = x # llist_of2 (Abs_llist_fin xs)"

I have been going in circles here for quite some time. Can someone point me in the right direction how to do this? Do I have the right approach? Or is it impossible in general?

Thanks in advance,

Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 031
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft

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