# [isabelle] Automatic simplification of lambda terms of tuples

*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] Automatic simplification of lambda terms of tuples
*From*: Iulia Dragomir <iulia.dragomir at aalto.fi>
*Date*: Fri, 26 Jun 2015 17:43:30 +0300
*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.7.0

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)
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
--
Iulia Dragomir, Ph.D.
Aalto University School of Science
Department of Computer Science
PO Box 15400
FI-00076 Aalto
Finland
Email: iulia.dragomir at aalto.fi
Phone: +358 503 872710
Web: http://users.ics.aalto.fi/iulia

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