Email Gateway (Aug 18 2022 at 18:15): Email Gateway (Aug 18 2022 at 18:15):From: Makarius <makarius@sketis.net>
On Fri, 26 Aug 2011, Steve Wong wrote:
I'm trying to generate a proof goal from string using the following:
I am answering this on isabelle-users, because it is a perfectly normal
user question. (Using ML alone does not mean it is relevant for
isabelle-dev.)
fun generate x lthy =
let
val thy = Local_Theory.exit_global lthy
val ctxt = ProofContext.init_global thy
in
This is a bit odd. You can use lthy, which is called "auxiliary context"
in local theory parlance directly as your context for the subsequent
operations. A lthy: local_theory is a semantic subtype of ctxt:
Proof.context, and the lthy naming convention is used whenever actual
local theory operations follow, like the subsequent
Specification.theorem_cmd.
(Specification.theorem_cmd
Thm.lemmaK NONE (K I)
(Binding.name "", []) [](Element.Shows [(Attrib.empty_binding,
[(Syntax.string_of_term ctxt @{term "F"} ^ " =
" ^
Syntax.string_of_term ctxt @{term "G"}, [])])]) x lthy)
end
*** Malformed YXML encoding: multiple results
*** At command "verify_with"
Syntax.string_of_term turns internal formal entities (terms) into external
text representation for user-consumption. For historic reasons the string
type is used here, but it is in fact some kind of quasi-abstract datatype
for marked-up document content. In general it is not allowed either to
split text input that is passed in or paste together text that is passed
out of the formal environment.
Working with string interfaces for formal entities was never robust, even
20 years ago, but now the fragility has become immediately apparent.
When "generating" things, you should always use the regular non-text
versions of tools and packages. (Sometines people forget to provide them,
but for almost everything in the regular Isabelle distribution there is
such a proper non-text version, taking directly typ and term values etc.)
Anyway, instead of Specification.theorem it is probably easier to use
Proof.theorem, although you need to store the result yourself in the
"after_qed" continuation.
Makarius
Email Gateway (Aug 18 2022 at 18:15):From: Steve Wong <s.wong.731@gmail.com>
On Fri, Aug 26, 2011 at 12:26 PM, Makarius <makarius@sketis.net> wrote:
On Fri, 26 Aug 2011, Steve Wong wrote:
Syntax.string_of_term turns internal formal entities (terms) into external
text representation for user-consumption. For historic reasons the string
type is used here, but it is in fact some kind of quasi-abstract datatype
for marked-up document content. In general it is not allowed either to
split text input that is passed in or paste together text that is passed out
of the formal environment.Working with string interfaces for formal entities was never robust, even
20 years ago, but now the fragility has become immediately apparent. When
"generating" things, you should always use the regular non-text versions of
tools and packages. (Sometines people forget to provide them, but for
almost everything in the regular Isabelle distribution there is such a
proper non-text version, taking directly typ and term values etc.)Anyway, instead of Specification.theorem it is probably easier to use
Proof.theorem, although you need to store the result yourself in the
"after_qed" continuation.Thanks a lot for that. So, which are the tools recommended for constructing
new terms (based on some existing terms)? Are you referring to functions
like dest_Free in term.ML, i.e. destruct a term into parts and then create a
new term from ground up?
Thanks again.
Steve
Makarius
Email Gateway (Aug 18 2022 at 18:17):From: Makarius <makarius@sketis.net>
Either using directly the datype constructors of typ/term (e.g. in pattern
matching) or some derived functions from src/Pure/term.ML,
src/Pure/logic.ML, src/HOL/Tools/hologic.ML.
The "tools and packages" that I mentioned above are more complex things
like Function_Fun.add_fun (the regular ML version) instead of the
add_fun_cmd as string version for end-users.
Makarius
Last updated: May 06 2024 at 16:21 UTC