Re: [isabelle] I want to print axiomatization info



On 11.07.2012 18:49, Gottfried Barrow wrote:

074: consts
082:   All::"('a => bool) => bool" (binder "ALL " 10)

153: notation (HOL)
154:   All  (binder "! " 10)

178: defs
180:   All_def:      "All(P)    == (P = (%x. True))"

I put this in jEdit, and it shows R::bool:

   lemma "!R. (P-->Q-->R) --> R"

So, you're right, though I thought you had to be wrong, until the goal
for the proof step told me you're right. This is where things like
declare[[show_types=true]] save us a bunch of time.

It appeared to me, by line 82, that "All" takes a "('a => bool)" and
returns a bool. It could be that "All(P)" is not the same thing as "All P".

If you resolve the binder syntax,

  !R. (P --> Q --> R) --> R

is the same as

  All (%R. (P --> Q -->R) --> R)

where the lambda abstraction has type bool => bool.





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