Email Gateway (Aug 22 2022 at 19:07): Email Gateway (Aug 22 2022 at 19:07):From: Joshua Chen <joshua.chen@uibk.ac.at>
Dear all, is there a canonical way in Isabelle/ML to get the value of
the Isar fact "this"? I'm currently using
let
val fs = Proof_Context.facts_of @{context}
in
Facts.lookup (Context.Proof @{context}) fs "local.this"
end
but am unsure if there are more direct ways.
Thanks,
Josh
Email Gateway (Aug 22 2022 at 19:08):From: Makarius <makarius@sketis.net>
On 07/02/2019 16:55, Joshua Chen wrote:
Dear all, is there a canonical way in Isabelle/ML to get the value of
the Isar fact "this"?
It depends what you mean precisely, and what your application actually is.
I'm currently using
let
val fs = Proof_Context.facts_of @{context}
in
Facts.lookup (Context.Proof @{context}) fs "local.this"
endbut am unsure if there are more direct ways.
Since you are using the compile-time @{context}, i.e. a constant, the
example is equivalent to:
ML_val ‹
@{thm this}
›
So when experimenting with ML inside Isar, it is better to bind some
initial constants like this:
ML_val ‹
val ctxt = @{context};
...
›
Later on, ctxt can be abstracted as arguments of a function, while the
body "..." remains unchanged.
Moreover, string literals of guessed internal names should be avoided:
such names change routinely over the years of continued Isabelle
development. (In particular, the "local" prefix is an odd artifact that
should disappear eventually.)
So here is my version of your initial example, following these principles:
notepad
begin
assume a: A
ML_val ‹
val ctxt = @{context};
val this_name =
Name_Space.full_name (Proof_Context.naming_of ctxt) (Binding.name
Auto_Bind.thisN);
val this = #thms (the (Proof_Context.lookup_fact ctxt this_name));
›
end
Nonetheless, it is unlikely that you actually need that in the
application. The "this" entry in the facts space is merely for end-users
writing Isar proof texts. Tools normally access specifically the some
internal slots of the proof engine.
A proof method gets the used facts (formerly "this") in the proof as
main argument. Nothing special to do: merely need to omit the
SIMPLE_METHOD wrapper.
A proof command can access the full Proof.state and retrieve this
information from it via Proof.goal: the ML_val command includes some
special tricks to support this in experiments:
notepad
begin
assume A
from this have B
ML_val ‹
val using_this = #facts @{Isar.goal};
›
sorry
end
An example for this in production is the 'sledgehammer' command: it uses
Proof.goal to get to the "chained facts", i.e. the former "this" that is
relevant for the pending goal.
Makarius
Email Gateway (Aug 22 2022 at 19:08):From: Joshua Chen <joshua.chen@uibk.ac.at>
Since you are using the compile-time @{context}, i.e. a constant, the
example is equivalent to:ML_val ‹
@{thm this}
›So when experimenting with ML inside Isar, it is better to bind some
initial constants like this:ML_val ‹
val ctxt = @{context};...
›Later on, ctxt can be abstracted as arguments of a function, while the
body "..." remains unchanged.
I picked up on this soon after, but I do find I often forget this..
Thanks very much for the pointers! As a beginner, it's often unclear
which of the multiple similarly plausible-sounding functions I should
use to accomplish what I want, so I greatly appreciate the advice.
It depends what you mean precisely, and what your application actually is.
I'm implementing syntax parse rules for Isabelle/HoTT that should
automatically fill in object-level type information for terms, so that
end users can leave some type information implicit for the logic to
infer. For instance, given that one has proved/assumed facts "f: A -> B"
and "g: B -> C" visible in the current proof context, one should be able
to write 'show "g o f"' and have the logic fill in the domain type to
give "compose A g f".
It seems to me that I do need direct access to the fact space since this
is a translation issue, in particular one that occurs before any proof
methods/commands are called. Though again, I'm not 100% sure about this.
Best,
Josh
Email Gateway (Aug 22 2022 at 19:08):From: Makarius <makarius@sketis.net>
On 10/02/2019 18:53, Joshua Chen wrote:
As a beginner, it's often unclear
which of the multiple similarly plausible-sounding functions I should
use to accomplish what I want, so I greatly appreciate the advice.
The usual strategy is two-fold:
* look at the text of the definitions of things, using the Prover IDE
* look at the context of applications, and try to figure out typical uses
Moreover it is often helpful to study documentation or ask on the
mailing list.
I'm implementing syntax parse rules for Isabelle/HoTT that should
automatically fill in object-level type information for terms, so that
end users can leave some type information implicit for the logic to
infer. For instance, given that one has proved/assumed facts "f: A -> B"
and "g: B -> C" visible in the current proof context, one should be able
to write 'show "g o f"' and have the logic fill in the domain type to
give "compose A g f".It seems to me that I do need direct access to the fact space since this
is a translation issue, in particular one that occurs before any proof
methods/commands are called. Though again, I'm not 100% sure about this.
Tools normally do not look at the fact name space, it is mainly for
end-users and thus somewhat accidental what it contains and what it
omits (e.g. unnamed facts don't show up).
A more robust scheme works via declarations of facts to tool-specific
parts of the context.
For example, Isabelle/ZF has a "TC" declaration attribute, which
maintains context data as defined in $ISABELLE_HOME/src/ZF/Tools/typechk.ML
It is also possible to use the Isar command 'named_theorems' and thus
bypass the details of handwritten context-data. E.g. search
named_theorems and Named_Theorems.get in .thy and .ML files to get some
ideas.
Thus your language will require explicit hints in the text, e.g.
assume a[TC]: A
have b[TC]: B
This is more robust than magic operations on the fact name space, but
also a bit awkward. Several people who are building non-HOL object
logics have pointed this out in the past few months. There is some
concrete chance that something will happen soon, shortly before or after
the Isabelle2019 release.
Makarius
Email Gateway (Aug 22 2022 at 19:08):From: Joshua Chen <joshua.chen@uibk.ac.at>
The usual strategy is two-fold:
This is what I have been doing intermittently over the past year and a
half ;) I do think the contributors are doing a heroic job of
maintenance and development, but it is indeed a less-than-optimal state
of affairs that Isabelle/ML is not yet very well-documented (even the
incomplete Cookbook is already fairly out-of-date). I'd like to help out
with that at some point after I learn things better for myself.
For example, Isabelle/ZF has a "TC" declaration attribute, which
maintains context data as defined in $ISABELLE_HOME/src/ZF/Tools/typechk.MLIt is also possible to use the Isar command 'named_theorems' and thus
bypass the details of handwritten context-data. E.g. search
named_theorems and Named_Theorems.get in .thy and .ML files to get some
ideas.
Great, this is also an approach I considered and will look into!
Thus your language will require explicit hints in the text, e.g.
assume a[TC]: A
have b[TC]: BThis is more robust than magic operations on the fact name space, but
also a bit awkward. Several people who are building non-HOL object
logics have pointed this out in the past few months. There is some
concrete chance that something will happen soon, shortly before or after
the Isabelle2019 release.
Indeed this is a little annoying, I look forward to possible
developments on this!
Best,
Josh
Email Gateway (Aug 22 2022 at 19:08):From: Makarius <makarius@sketis.net>
As the Prover IDE supports more and more Isabelle/ML development, that
interactive environment becomes an important source of implicit
information. Just a few years ago, reading Isabelle/ML sources required
much more arcane knowledge.
E.g. you can open $ISABELLE_HOME/src/Pure/ROOT.ML and browse through (a
copy of) Isabelle/Pure within itself, with full annotations provided by
the Poly/ML compiler.
You can also browse through $ISABELLE_HOME/src/Doc/Implementation and
its chapters as theory sources.
Browsing through Isabelle/ML tools is more awkward: it requires to start
from Pure (e.g. "isabelle jedit -l Pure") and wait a long time until its
Main.thy material is loaded.
Makarius
Email Gateway (Aug 22 2022 at 19:09):From: Makarius <makarius@sketis.net>
The space of named facts is mainly for the end-user, by there is an
alternative view of all facts that are literally accessible in the
current context. This is used e.g. for the backquote/cartouche notation
of facts or the "fact" proof method.
Here is an example to access this "cloud" of literal facts of the context:
ML ‹
val literal_facts = Proof_Context.facts_of #> Facts.props;
›
notepad
begin
{
fix x y z :: nat
{
assume "x = y"
assume "y = z"
from ‹x = y› and ‹y = z› have "x = z" by (rule trans)
moreover from ‹x = z› have "z = x" by (rule sym)
print_facts
ML_val ‹literal_facts \<^context>›
moreover note calculation
}
print_facts
ML_val ‹literal_facts \<^context>›
}
print_facts
ML_val ‹literal_facts \<^context>›
end
You could try to use that by default, potentially with a declaration
attribute to suppress unwanted literal facts.
Makarius
Last updated: Apr 19 2024 at 08:19 UTC