*To*: Christian Sternagel <c-sterna at jaist.ac.jp>*Subject*: Re: [isabelle] Lazy Lists*From*: Andreas Lochbihler <andreas.lochbihler at kit.edu>*Date*: Mon, 25 Jun 2012 08:43:52 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4FE7D8D3.2070104@jaist.ac.jp>*References*: <4FE7D8D3.2070104@jaist.ac.jp>*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.27) Gecko/20120216 Thunderbird/3.1.19

Dear Christian,

However, using standard HOL types and functions within HOLCF may need some work.

Lets consider we use "'a llist" (from AFP/Coinductive) for lazy lists and "'a list" for finite lists.

If I'm correct, the new transfer package should be able (after appropriate setup) to transfer facts from "'a list" to "'a llist" with additional "lfinite ..." assumptions (and also the other way round?). But how this setup is actually done, I did not find out.

Another issue is that Haskell functions (on lazy lists) are defined using notation like "fun" of Isabelle/HOL despite not being based on well-founded recursion, whereas for function definitions on "'a llist" in Isabelle/HOL this does not work (at least I don't know how). That is, there is a gap between what is used in Haskell programming and how this can be "simulated" in Isabelle/HOL.

Unfortunately, there is currently no support for corecursive definitions.

So, here is a wish-list: - in contexts where we have "lfinite", reuse facts on "'a list" functions

- provide a command that allows to define functions on "'a llist" using the same notation as "fun" (is this already possible?)

- for Haskell code generation Nil and LNil as well as Cons and LCons should be unified and mapped to [] and (:) of Haskell - moreover, would it be possible to unify "equivalent" (modulo infiniteness) functions like "map" and "lmap", "filter" and "lfilter" ..., for code generation?

Hope this helps, Andreas -- Karlsruher Institut für Technologie IPD Snelting Andreas Lochbihler wissenschaftlicher Mitarbeiter Am Fasanengarten 5, Geb. 50.34, Raum 025 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

theory Transfer_List imports Quotient_Coinductive_List begin lemma transfer_list_llist: "type_definition llist_of list_of {xs. lfinite xs}" by unfold_locales simp_all setup_lifting transfer_list_llist lemma [transfer_rule]: "cr_list LNil []" by(simp add: cr_list_def) lemma [transfer_rule]: "(op = ===> cr_list ===> cr_list) LCons op #" by(rule fun_relI)+(simp add: cr_list_def) lemma [transfer_rule]: "(cr_list ===> cr_list ===> cr_list) lappend op @" by(rule fun_relI)+(simp add: cr_list_def) lemma "xs @ [] = xs" by transfer simp lemma "lfinite xs \<Longrightarrow> lappend xs LNil = xs" oops end

**Follow-Ups**:**Re: [isabelle] Lazy Lists***From:*Lawrence Paulson

**Re: [isabelle] Lazy Lists***From:*Brian Huffman

**References**:**[isabelle] Lazy Lists***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] Trying to rename Lattices.thy
- Next by Date: Re: [isabelle] Trying to rename Lattices.thy
- Previous by Thread: Re: [isabelle] Lazy Lists
- Next by Thread: Re: [isabelle] Lazy Lists
- Cl-isabelle-users June 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list