Re: [isabelle] Dealing with lets in Isar



You can implement a nice expansion of lets into equations with the simplifier as per Konrad Slimd's and my proof pearl paper in TPHOLs 2005

Michael

> On 30 Nov 2013, at 3:35, "Andreas Lochbihler" <andreas.lochbihler at inf.ethz.ch> wrote:
>
> Hi Christian,
>
> I don't completely understand why this is related to let. A let just introduces an abbreviation. However, in your example, you are more concerned with patterns such as tuples, but
>
>  let (x, y) = e in f x y
>
> is syntactic sugar for
>
>  Let e (prod_case (%x y. f x y))
>
> So, do you also want to introduce variables if there's no pattern-matching involved, such that "P (let x = e in f x)" gets transformed into "!!x. x = e ==> P (f x)"?
>
> In principle, you can use Isabelle's splitter:
>
> lemma Let_prod_split_asm:
>  "P (Let e (prod_case f)) = (~ (EX x y. (x, y) = e & ~ P (f x y)))"
> by(auto simp add: Let_def prod.split_asm)
>
> lemma Let_split_asm: "P (Let e f) = (~ (EX x. x = e & ~ P (f x)))"
> by(auto simp add: Let_def)
>
> lemma
>  assumes "P (let (x, y) = e1; (u, v) = e2; (w, k) = e3 in f x y u v w k)"
>  shows "thesis"
> using assms
> apply -
> proof(split Let_prod_split_asm Let_split_asm)+
>  case (goal1 x y u v w k)
>
> With some ML programming, it should be easy to make this more readable.
>
> Hope this helps,
> Andreas
>
>
>> On 29/11/13 16:55, Christian Urban wrote:
>>
>> 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
>

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




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