[isabelle] Dealing with lets in Isar



Dear All,

We have a question about how to deal conveniently with 
Lets in Isar proofs. Some of our definitions contain many 
nested lets, as in

definition 
   "foo f e1 e2 e3 == let (x, y) = e1; (u, v) = e2; (w, k) = e3 in f x y u v w k"


The problem is that we have foo unfolded in our premises, say
  
  lemma
    assumes "P (let (x, y) = e1; (u, v) = e2; (w, k) = e3 in f x y u v w k)"
    shows "thesis"

We could prove such lemmas with 

  lemma
    assumes "P (let (x, y) = e1; (u, v) = e2; (w, k) = e3 in f x y u v w k)"
    shows "thesis"
  proof -
    from assms
    obtain x y u v w k
    where "P (f x y u v w k)" and 
          "(x, y) = e1" and "(u, v) = e2" and "(w, k) = e3" by ...

but we are wondering whether there is a simpler way. Essentially,
we want to avoid having to fix the variables and to avoid to write 
the equations explicitly. We rather prefer the way how the cases-construction
works, which automatically fixes variables and puts such equations
into the context, for example

  lemma 
    assumes "P (n:: nat)"
    shows "thesis"
  proof (cases n)

In this example you have "n = 0" in the "first" case and fix nat/n = Suc nat 
in the "second" case. Is there something similar for many nested lets?

If not, how would we have to go about implementing (presumably in ML)
such a construction?

Best wishes,
Christian




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