Re: [isabelle] Infinitely recursive lambda expression or not?
On Sat, 14 Dec 2013 11:29:47 +0100, John Wickerson
<johnwickerson at cantab.net> wrote:
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
∀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).
This archive was generated by a fusion of
Pipermail (Mailman edition) and