*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Help with let expressions*From*: "Glauber Cabral" <glauber.sp at gmail.com>*Date*: Mon, 22 Sep 2008 17:45:40 -0300

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.

**Attachment:
email.zip**

**Attachment:
MainHCPairs.thy**

structure Header : sig (* val get_axioms : string -> string list *) val record : string -> unit val initialize : string list -> unit end = struct open Proofterm infix mem; val thmlist = ref [""]; val thyname = ref "" fun axname s = let val (_,an) = take_prefix (fn x => x <> ".") (explode s) in if null an then "" else implode (tl an) end fun get_axioms name = let val (l, r) = List.partition (fn s => s mem (!thmlist)) (filter (fn s => s <> name) (filter (fn s => length (filter (fn c => c = ".") (explode s)) < 2) (filter (String.isPrefix (!thyname)) (Symtab.keys (thms_of_proof (Thm.proof_of (thm name)) Symtab.empty))))) in if null r then l else l @ List.concat (map get_axioms r) end fun record1 name = let val thy = the_context () val thms = PureThy.thms_of thy in if name mem (map (axname o fst) thms) then let val axs = map axname (get_axioms (!thyname ^ "." ^ name)) val txt = foldl (fn (s, t) => s ^ "\n" ^ t) "" axs val filename = !thyname ^ "_" ^ name ^ ".deps" in File.write (Path.basic filename) txt end else () end fun record name = record1 name handle _ => () fun initialize l = let val thy = Context.theory_name (the_context ()) in thmlist := map (fn s => thy ^ "." ^ s) l; thyname := thy end end; proofs:=1;

**Attachment:
Prelude_List_E2.thy**

- Previous by Date: [isabelle] Partial definitions of datatypes
- Next by Date: Re: [isabelle] Question about locales
- Previous by Thread: Re: [isabelle] Partial definitions of datatypes
- Next by Thread: [isabelle] Syntax for theory definitions
- 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