[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.