[isabelle] [Fwd: Re: Help with let expressions]

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

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"

lemma [elim]:
  "k +' length'(xs) = 0' \<Longrightarrow> P"

lemma [elim]:
  "0' = 1' \<Longrightarrow> P"

lemma plus_inject_l:
  "(a::X_Int) +' b = a +' c \<Longrightarrow> b = c"

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
  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)

fn:Florian Haftmann
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: =

Attachment: signature.asc
Description: OpenPGP digital signature

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