Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Automatic simplification of lambda terms of tu...

Email Gateway (Aug 22 2022 at 10:24):

From: Iulia Dragomir <iulia.dragomir@aalto.fi>
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

Email Gateway (Aug 22 2022 at 10:25):

From: Tobias Nipkow <nipkow@in.tum.de>
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)

I assume you mean the same f/F on both sides. This does not cover abstraction
over tuples, which is syntactic sugar for the combinator split :: "('a ⇒ 'b ⇒
'c) ⇒ 'a × 'b ⇒ 'c". You also need

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

However, the simplifier will not be able to use such rules, unless you
instantiate the f with a concrete term.

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

smime.p7s

Last updated: Nov 21 2024 at 12:39 UTC