Re: [isabelle] export_code doesn't define Trueprop for False
This is my last email on this, unless someone wants to straighten me out
on anything, but in about 2 to 3 months from now, I'm going to start
trying to use the concept that I outlined in last email, where I made an
attempt to fix the exception problem, unless someone wants to explain
why I'm off track.
Its taken me a while to get to the code generator, where I specifically
learned about "export_code" from a tip given to me here several weeks
ago by Florian. It pays to ask questions, and get a tip here and there
for some of them.
There are "huge" parts of Isabelle, and I'll now put the code generator
in with those huge parts, like Isar as a high-level language, the
meta-logic of Pure, the object logic of HOL, Sledgehammer, the PIDE
interface, and other auto tools.
Complements from a mere user are now out of the way.
Here, I'm thinking about whether "prop" and "==>" are supposed to get
their meaning from their use with "value" or from their use with
"theorem". I guess I'm stating the obvious in saying that Isabelle/Pure
can't be exported as about 10 lines of Scala or Haskell code, and so
something has to be lost.
Essentially, "value", which I understand is related to the code
generator, doesn't return a "prop" value of "so-called-meta-true" or
"so-called-meta-false", as shown by these examples:
value "True ==> False" (* returns (Trueprop False)::prop *)
value "False ==> True" (* returns (Trueprop True)::prop *)
value "!!P. PROP P" (* returns (!!u::prop. PROP u)::prop *)
The short story is that the Haskell line of code "data prop Holds" is my
guiding principle, and that the meaning of "prop" and "==>" should come
from "theorem" and not "value", otherwise, the meta-logic, when
exported, will be no different from the object logic (which may be
inescapable). That's the way it appears to me.
I look to the software to teach me logic. I look to it to give me, as an
enforcer, the years of knowledge the programmers have, who have written
When the software doesn't give me strict guidance, I'm willing to get
creative, but I'd rather waste less of of my time than more of it by
going off track.
This archive was generated by a fusion of
Pipermail (Mailman edition) and