*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Infinitely recursive lambda expression or not?*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Sat, 14 Dec 2013 06:22:31 -0600*In-reply-to*: <C743CBFE-029F-4E49-9A56-3695338394B8@cantab.net>*References*: <op.w72usxweule2fv@cardamome> <C743CBFE-029F-4E49-9A56-3695338394B8@cantab.net>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

Yannick,

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

Then lemma "(%x. True) = (%x. x | (%x. True) x) ==> ((%x. True) False ~= False)" by(simp) Regards, GB On 12/14/2013 4:29 AM, John Wickerson wrote:

Hi Yannick, 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? john On 14 Dec 2013, at 10:15, Yannick Duchêne (Hibou57)<yannick_duchene at yahoo.fr> wrote: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

**Follow-Ups**:**Re: [isabelle] Infinitely recursive lambda expression or not?***From:*Yannick Duchêne (Hibou57)

**References**:**[isabelle] Infinitely recursive lambda expression or not?***From:*Yannick Duchêne (Hibou57)

**Re: [isabelle] Infinitely recursive lambda expression or not?***From:*John Wickerson

- Previous by Date: Re: [isabelle] Infinitely recursive lambda expression or not?
- Next by Date: Re: [isabelle] Infinitely recursive lambda expression or not?
- Previous by Thread: Re: [isabelle] Infinitely recursive lambda expression or not?
- Next by Thread: Re: [isabelle] Infinitely recursive lambda expression or not?
- Cl-isabelle-users December 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list