*To*: "Yannick Duchêne (Hibou57)" <yannick_duchene at yahoo.fr>*Subject*: Re: [isabelle] Infinitely recursive lambda expression or not?*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Sat, 14 Dec 2013 14:10:04 +0000*Cc*: "cl-isabelle-users at lists.cam.ac.uk List" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <op.w723lrn9ule2fv@cardamome>*References*: <op.w72usxweule2fv@cardamome> <C743CBFE-029F-4E49-9A56-3695338394B8@cantab.net> <52AC4D87.9030304@gmx.com> <op.w723lrn9ule2fv@cardamome>

It is simply that if f is the constant-True function, then f = (λa. False ∨ f False). I think that you are imagining some sort of execution model for HOL. But HOL doesn’t have an operational semantics. Larry Paulson On 14 Dec 2013, at 13:26, Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr> wrote: > 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.

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

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

**Re: [isabelle] Infinitely recursive lambda expression or not?***From:*Gottfried Barrow

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

- Previous by Date: Re: [isabelle] Hide all constructors of a datatype automatically
- Next by Date: Re: [isabelle] Hide all constructors of a datatype automatically
- 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