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

`Le Sat, 14 Dec 2013 13:22:31 +0100, Gottfried Barrow
``<gottfried.barrow at gmx.com> a écrit:
`

Yannick,

`I just make more explicit what John says with regards to the constant
``function, and also, explicitly, for any free variables in a lemma, there
``is implicit universal quantification of those free variables, something
``which Christian Sternagel made explicit enough with explicit examples to
``conclusively show, for me, the connection between free variables and
``universal quantification.
`
There can be lots of implicit action working underneath.
You're stating this:
lemma "!!f. !!a. f = (%a. a | f a) ==> (f a = a)"
oops

`So, let "f = (%a. True)", and for the quantified variable "a", let "a =
``False".
`
Then

`lemma "(%x. True) = (%x. x | (%x. True) x) ==> ((%x. True) False ~=
``False)"
`by(simp)
Regards,
GB

`I wanted to check if had an issue with binding (indeed, I did had issues
``with implicit operations in some cases), so tried this:
`
lemma "f = (λa. False ∨ f False) ⟹ (f False = False)"

`It still says it find a counter example, with “f False = True”. Precisely,
``what I don't understand, is why it suppose this may be True. “a” is not
``used, and the only constant used in f is False.
`

`I must be missing something important, or else it's just Auto Quickcheck
``which is not made for this kind of infinite expression.
`
I won't go with an axiom, looks unsafe if I am missing something.
--
“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.*