# Re: [isabelle] Infinitely recursive lambda expression or not?

`On Sat, 14 Dec 2013 11:29:47 +0100, John Wickerson
``<johnwickerson at cantab.net> wrote:
`

Hi Yannick,

Hello John, and thanks for your interest in the question.

`The counterexample involves having f as the constant "True" function,
``and then picking "a" to be False. The assumption in your lemma can be
``rewritten as
`
∀x. (f(x) = x ∨ f(x))

`and this certainly holds when f is the constant "True" function, since
``both sides of the =-operator are True. But the conclusion of your lemma
``doesn't hold since f(False) is not False.
`
Does that help?

`I don't know so far, will see if I understand. At least you seem to
``confirm Isabelle really understand it as a recursive function application
``(I had a doubt on this for a moment).
`

`Why is f(False) not False ? If it's built with False only and only
``disjunctions, where could True comes from?
`

`Or else may be my interpretation is wrong: I see it as an infinite
``sequence like “x ∨ x ∨ x ∨ x ∨ x ∨ …”.
`

`For the longer story, what I was attempting with this lemma, is to get a
``rule for elimination of this particular kind of infinite recursion. A more
``general case could be (in my interpretation which may be erroneous, I
``don't know so far): let “+” be an operator, let the proposition “a + b =
``a” be previously proved to holds, then an infinite sequence like “a + b +
``b + b + b + …” may be substituted to “a”; that was the meaning I expected.
`

`May be there is a way to prove it with something like a list induction and
``proving the function recursion is like the list recursion on an infinite
``list. May be with a list I could say “what ever the length of a + b + b +
``b + b + … it will always be a when a + b = a” so the infinite length list
``produce the same if it's interpreted as producing anything (already hardly
``provable I believe). Just that it's not a list, it's a recursive function
``instead. Then I wondered if there exist an axiom for this in any kind of
``theory (either that of Isabelle or from foreign theories) or else if it
``would be safe to create one, and I'm afraid of creating an axiom which I'm
``not able to prove (so a pure axiom, not a theorem).
`
--
Yannick Duchêne

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