*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Automatic simplification of lambda terms of tuples*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Sat, 27 Jun 2015 19:19:42 +0200*In-reply-to*: <558D6512.5080604@aalto.fi>*References*: <558D6512.5080604@aalto.fi>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:31.0) Gecko/20100101 Thunderbird/31.7.0

On 26/06/2015 16:43, Iulia Dragomir wrote:

Dear all, I have the following lemma within a theory: theory Test imports Main begin lemma lambda_true_top: "f (Î x . True) = F top" by (simp add: top_fun_def)

lemma lambda_pair_true_top: "f (Î (x,y) . True) = f top" by (simp add: split_def top_fun_def)

Tobias

end which I would like to use for lambda terms having different variables, like: lemma "F (Î (x,y) . True) = F top" or lemma "F (Î (x,y, (z, t), a, (b, c, d)) . True) = F top"

Now, if I use it as substitution rule, the goal is identical to the lemmas to be proved and if I try to add it as simplification rule, a failed application of proof method is raised. How can I use lambda_true_top in this proof? Or how can I write my original lemma such that it can be used to simplify a term like F (Î (x,y, (z, t), a, (b, c, d)) . True) to F top in general? In my case F is always a constant function. Thanks. Best regards, Iulia Dragomir

**Attachment:
smime.p7s**

**References**:**[isabelle] Automatic simplification of lambda terms of tuples***From:*Iulia Dragomir

- Previous by Date: Re: [isabelle] Datatype + cardinality + polymorphismus?
- Next by Date: Re: [isabelle] Datatype + cardinality + polymorphismus?
- Previous by Thread: [isabelle] Automatic simplification of lambda terms of tuples
- Next by Thread: [isabelle] of/where with dummy-patterns
- Cl-isabelle-users June 2015 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