[isabelle] Infinitely recursive lambda expression or not?



My ashamed apologizes if this looks as weird as I'm afraid it may looks, however, this question really tickles me.

I came to something like this after some simplifications, so I wanted to test it with a lemma:

    lemma "f = (λa. a ∨ f a) ⟹ (f a = a)"

Isabelle tells me it found a counter example with “a = False” and “f a = True” . It does not seems to see there is an infinite recursion, or else I don't understand how it can believe “f a” may differs from “a” (how so?).

To me, it can only be “a”, an infinite never ending sequence of disjunctions of the same term may be nothing else if it's ever something, than this term.

I guess this case looks weird, but I would like to know, first if Isabelle sees it as an infinitely recursive lambda expression or not, then if if it do, if there exists some trusted axioms which are able to deal with this?


--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University





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