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:
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
There can be lots of implicit action working underneath.
You're stating this:
lemma "!!f. !!a. f = (%a. a | f a) ==> (f a = a)"
So, let "f = (%a. True)", and for the quantified variable "a", let "a =
lemma "(%x. True) = (%x. x | (%x. True) x) ==> ((%x. True) False ~=
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.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and