[isabelle] Help with let expressions



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
Description: Zip archive

Attachment: MainHCPairs.thy
Description: Binary data

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
Description: Binary data



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