Email Gateway (Jan 28 2021 at 17:55): Email Gateway (Jan 28 2021 at 17:55):From: Daniel Kirchner <daniel@ekpyron.org>
Dear all,
First some background information:
I'm working at embedding a non-classical logic with non-classical
syntax into the Isabelle/HOL logic using a shallow semantical embedding.
I.e. I have a custom proposition type o and a custom grammar starting
at a nonterminal my_prop to parse propositions of that type written in
the target theory's "native" syntax (which is quite different from
Isabelle's usual term/prop syntax, so this involves some non-trivial
parse translations on the grammar tree starting at my_prop).
This proposition type is connected to the HOL logic using a semantic
validity function is_valid_in semanticContext proposition (using
some complex HOL semantics for the target theory's logic).
Now I do define syntax for is_valid_in that parses its
proposition part starting from the nonterminal my_prop. But to
make life easier and lower entry barriers for people used to the target
theory's syntax, but not to Isabelle's term syntax, I'm also
introducing copies of outer theory commands to directly act on
my_prop-propositions and among other things hide the semantic
context in the proof state. I.e. my_theorem accepts both short and
long theorem specifications, but parses propositions starting from
my_prop as grammar root. It internally sets up a fixed
"semanticContext" and can thereby transparently translate these
"my_prop"-propositions to regular "prop"-propositions. Furthermore,
that semanticContext is stored in the Proof_Context and I define
further outer syntax commands like my_assume, my_have,
my_show (and some custom ones specific to reasoning mechanisms in
the target logic) that again directly parse my_prop syntax and can
transparently pick up (or sometimes manipulate) the semanticContext in
the proof context, etc.
Independently, I set up different "printing modes" (i.e. configurable
sets of print translations), s.t. it's possible to either view the proof
state relative to the custom commands and "my_prop" or to view the
translation to Isabelle's native logic and to easily switch between
those viewing mode, s.t. people familiar with either syntax can easily
get used to the other and in order to be transparent about the
transformations automatically done by the custom commands.
Now all of this is working quite nicely and most of the complexity of
this nicely lives in the grammar and parse and print translations for
my_prop.
However, currently, I also have to parse full long statement and theorem
outer syntax in the custom commands, replacing reading propositions by
custom logic that reads my_prop terms (by constructing a temporary
proof context with Syntax.root replaced by my_prop and parsing
them as terms instead of propositions), which involves quite some
additional complexity that I am not particularly happy with (I'm
basically roughly reimplementing parts of Expression.read_statement to
read the theorem specification to then pass it on to
Specification.theorem with some additional postprocessing, but the
process is quite complex and I would like to avoid this as much as
possible to keep things maintainable in the long run).
So now to the actual question:
In the situation described above I think I could avoid almost all
complexity in the custom outer syntax commands, if I could replace the
grammar root symbol used to parse propositions in a Proof_Context.
While there is Syntax.root that can be used to replace the grammar
root symbol for parsing terms, there currently seems to be no way to do
the same for "prop" when parsing propositions (looking at the
implementation of parse_term in the syntax phases, "prop" is
hard-coded, whereas the term root is read from the Syntax.root config
option in the respective proof context; I see no obvious reason why
the proposition root could not symmetrically be a config option as
well).
So to cut a long story short: is there any particular reason why the
proposition root grammar symbol "prop" cannot or should not be a config
option in the proof context, similarly to the term root symbol? Or is
there an entirely different, simpler approach to achieving the same
thing without having the proposition root symbol configurable, but also
without having to replicate major parts of the logic used to parse long
statement/theorem outer syntax for the custom commands I want to define?
Also how "abusive" of Isabelle's internals does my current approach
(e.g. temporarily changing Syntax.root for parsing the
custom propositions as terms) sound in general ;-)? (It does seem to
work quite perfectly, but I may be missing good reasons for not doing
things like this in general).
I do realize that I could probably avoid a good part of the complexity,
if I just wrapped all propositions in some special bracket syntax
everywhere and only had parse translations do the work e.g. of
extracting a stored semantic context, but ideally I would generally
like to avoid that and keep syntactic overhead for statements in the
target logic's syntax at an absolute minimum (although I'm not sure how
sane of a desire that is ;-)) and I still need custom outer syntax
commands anyways to properly "initialize"/create and manipulate the
implicit semantic context in some cases, plus I e.g. also intend to
automatically post-process theorems and potentially extract "rulified"
versions of them to be used for improved automated reasoning, etc.
Thank you very much for your time and your replies!
Best wishes,
Daniel Kirchner
Last updated: Apr 19 2024 at 01:05 UTC