*To*: USR Isabelle <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] [Fwd: Re: Help with let expressions]*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Tue, 23 Sep 2008 17:38:35 +0200*Organization*: TU München, Lehrstuhl Software and Systems Engineering*User-agent*: Thunderbird 1.5 (X11/20060113)

Hi Glauber, > I'm trying to prove the ZipSpec theorem (attached file) that shows the > property of Haskell unzip/zip function. This is the first theorem that uses > let definitions and I've got problems with this. > I try do use Let_def and decompose let definitions, but I guess I'm going to > start a loop (the last apply command is again a let decomposition and it > suggests that induction should be used, I guess). Can anyone give any > suggestion or example of how to deal with let definition? The example in the > tutorial is trivial and I could not get much far from there. Attached I have a sketch how a proof using induction could work (the problem indeed has nothing to do with let). Note that there are some auxiliary lemmas involving X_Ints and length' which surely hold but I did not prove in detail. An alternative could be to provide a rule for simultaneous induction on two lists in the manner of the HOL theorem "list_induct2". I don't know the details of the project and to which extent the foundations are firm or can be changed, but after a look at the sources a few observations (in descending relevance): * You work with types X_Int and X_List which seem to be *copies* of the existing HOL ints and lists. It will be an *enormous* effort to provide enough lemmas to prove reasonable things with it (remember the auxiliary lemmas I have mentioned above). If it is in accordance with the aims of the projects, I would recommend to use HOL ints and lists. * The attribute [rule_format] is superfluous if you write down the propositions using meta connectives \<And> and ==> instead of ALL and -->. * Prelude_List_E2 does a lot in order to provide tupled syntax for the operations; if there is no reason for this, it could be left out easily. * constdefs/axioms are now (Isabelle2008) superseeded (though still present) by definition/axiomatization * You can incorporate ML code directly into theory files using ML {* ... *} sections. Feel free to ask further questions. Hope this helps Florian

lemma ZipConsCons' [simp]: "zip'(X_Cons x xs, X_Cons y ys) = X_Cons (x, y) (zip'(xs, ys))" by (rule ZipConsCons) rule lemma [elim]: "length' (X_Cons x xs) = 0' \<Longrightarrow> P" sorry lemma [elim]: "k +' length'(xs) = 0' \<Longrightarrow> P" sorry lemma [elim]: "0' = 1' \<Longrightarrow> P" sorry lemma plus_inject_l: "(a::X_Int) +' b = a +' c \<Longrightarrow> b = c" sorry theorem ZipSpec: assumes "length'(xs) = length'(ys)" shows "unzip (zip' (xs, ys)) = (xs, ys)" using assms proof (induct xs arbitrary: ys) case X_Nil then show ?case apply (simp_all add: UnzipNil LengthCons) apply (cases ys) apply simp_all apply (drule sym) apply auto done next case (X_Cons x xs) then show ?case apply (cases ys) apply (auto simp add: ZipConsNil UnzipNil LengthCons UnzipCons Let_def split_def) apply (drule plus_inject_l, auto) apply (drule plus_inject_l, auto) done qed

begin:vcard fn:Florian Haftmann n:Haftmann;Florian org;quoted-printable;quoted-printable:Technische Universit=C3=A4t M=C3=BCnchen ;Institut f=C3=BCr Informatik, Lehrstuhl Software and Systems Engineering adr;quoted-printable;quoted-printable:;;Boltzmannstra=C3=9Fe 3;M=C3=BCnchen;Bayern;85748;Deutschland email;internet:florian.haftmann at informatik.tu-muenchen.de title:M. Sc. tel;work:(++49 89) 289 - 17300 note;quoted-printable:PGP available: = =0D=0A= http://www4.informatik.tu-muenchen.de/~haftmann/pgp/florian_haftmann_at_i= nformatik_tu_muenchen_de.pgp=0D=0A= x-mozilla-html:FALSE url:http://isabelle.in.tum.de/~haftmann version:2.1 end:vcard

**Attachment:
signature.asc**

- Previous by Date: [isabelle] Syntax for theory definitions
- Next by Date: Re: [isabelle] Partial definitions of datatypes
- Previous by Thread: [isabelle] Incompatibilities between releases (Re: Syntax for theory definitions)
- Next by Thread: [isabelle] DAMP 2009 CFP
- Cl-isabelle-users September 2008 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