Email Gateway (Aug 18 2022 at 12:26): Email Gateway (Aug 18 2022 at 12:26):From: Glauber Cabral <glauber.sp@gmail.com>
Dear Isabelle users.
I've been using Isabelle as the theorem prover of Hets environment to prove
HasCASL specifications to my master thesis and I'm still a starter in this
field.
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.
Thank you in advance,
Glauber.
PS: The files the .thy file imports are attached and they should work OK
from the same folder. The 3 files are also compressed as I don't know if
this list accept zip or not. Sorry by this duplication.
email.zip
MainHCPairs.thy
prelude.ML
Prelude_List_E2.thy
Email Gateway (Aug 18 2022 at 12:27):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Glauber,
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
ExampleProof.thy
florian.haftmann.vcf
signature.asc
Last updated: May 03 2024 at 01:09 UTC