Email Gateway (Aug 19 2022 at 08:24): Email Gateway (Aug 19 2022 at 08:24):From: John Munroe <munddr@gmail.com>
Hi,
I have a question about Pure. Is
http://www.lri.fr/~wenzel/Isabelle2011-Paris/pure.pdf a reasonably
sufficient reference for summarising the primitives of Pure? If so,
suppose my function requires something richer than those presented on
page 2, e.g., theory manipulations, does that mean I'm actually
working in a separate meta-logic (one that sits between Pure and the
object-logic)? That is, I'm actually using Pure to encode theory
manipulations, so it's an object-logic when viewed from Pure's
perspective.
Thanks a lot for your time in advance.
John
Email Gateway (Aug 19 2022 at 08:24):From: Lawrence Paulson <lp15@cam.ac.uk>
I wonder whether these concepts are precisely enough defined for your question to be answered in any meaningful way.
Larry Paulson
Email Gateway (Aug 19 2022 at 08:25):From: John Munroe <munddr@gmail.com>
Sorry, I'll try to clarify clarify my question. For example, if the
transformation is to negate each axiom in a theory or the
transformation is to make some syntactic changes, e.g., rename certain
term to something else, then is it still expressible in Pure? I've
just found http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-130.pdf and
it seems that there isn't appropriate syntax at least for the latter.
If that's the case, does that mean these transformations would sit in
a separate meta-level in the logic hierarchy -- between Pure and the
object-logic?
Please let me know if more clarification is needed.
Thanks
John
Email Gateway (Aug 19 2022 at 08:25):From: Lawrence Paulson <lp15@cam.ac.uk>
I'm not aware of any such hierarchy. Honestly, I don't think there's any enlightenment to be had in this line of reasoning.
Larry Paulson
Email Gateway (Aug 19 2022 at 08:25):From: Makarius <makarius@sketis.net>
As the author of the above slides I am also a little confused about the
formulations of the questions. Only Larry or Randy can say if this a
"reasonably sufficient reference".
I made these slides for a 1-day Isabelle tutorial at Place d'Italie in
Paris, which is the core Coq development group. We had some interesting
discussions on that day, including the question why "fix" and "assume" are
not the same thing in Isabelle/Isar, and the underlying Pure framework.
(Nobody outside the type-theory group actually understood that question.)
Makarius
Last updated: Apr 25 2024 at 20:15 UTC