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 the software.

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 MHonArc.