# [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
proof
show "LNil : ?llist_fin" by simp
qed
(* 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,
Andreas
--
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
http://pp.info.uni-karlsruhe.de

`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.*