Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] schematic variables and antiquotations

Email Gateway (Aug 18 2022 at 13:46):

From: Lucas Dixon <ldixon@inf.ed.ac.uk>
Hello,

I'm trying to do some experiments with Isabelle 2009 - I'm writing a
function to "zip-to" a particular subterm. I would like specify the
subterm in a way that can involve schematic variables, much like the
find feature which lets schematic variables be used to find theorems
matching a pattern.

So here's what I'm doing...

( START )
theory norm
imports Main
uses "tools.ML"
begin

local_setup {* ProofContext.set_mode ProofContext.mode_schematic *}

ML {*
val x = zip_to_matching_subterm @{context} [] @{term "?x + ?y"} 0 @{term
"1 + 2 + 3 + 4"};
*}
( END )

but here I get:

*** Unbound schematic variable: ?x
*** At command "ML".

Can I get the antiquotation to read schematic terms? Should I create a
new kind of antiquotation? (is that easy?) Suggestions very welcome,

cheers,
lucas

Email Gateway (Aug 18 2022 at 13:47):

From: Makarius <makarius@sketis.net>
On Fri, 10 Jul 2009, Lucas Dixon wrote:

I'm trying to do some experiments with Isabelle 2009 - I'm writing a
function to "zip-to" a particular subterm. I would like specify the
subterm in a way that can involve schematic variables, much like the
find feature which lets schematic variables be used to find theorems
matching a pattern.

So here's what I'm doing...

( START )
theory norm
imports Main
uses "tools.ML"
begin

local_setup {* ProofContext.set_mode ProofContext.mode_schematic *}

ML {*
val x = zip_to_matching_subterm @{context} [] @{term "?x + ?y"} 0 @{term "1 +
2 + 3 + 4"};
*}
( END )

but here I get:

*** Unbound schematic variable: ?x
*** At command "ML".

Note that regular Isar text is always fully determined, and variables with
question marks refer to bindings introduced via is/let abbreviations.

While the ProofContext.mode_schematic indeed switches to a special mode
where "term patterns" can be processed instead (with slightly different
rules for type-inference), it is a rather bad idea to enable it globally.

Luckly the 'local_setup' did work out, indicating that this is the wrong
approach anyway. (Incidently, the reason for that is that a local theory
operation merely sees the "auxiliary context", essentially a sandbox to
produce specifications to go into the "target context". After finishing
the 'local_setup' command, the toplevel resets the state to the
(unchanged) target context. A permanent change of the local theory target
would require proper LocalTheory operations, not ProofContext ones.)

Since you have mentioned patterns in 'find_theorems' already, a brief look
at the sources reveals that it uses ProofContext.read_term_pattern to
process its input, and a check of its implementation shows the usual way
of changing these modes temporarily.

Can I get the antiquotation to read schematic terms? Should I create a
new kind of antiquotation? (is that easy?)

Yes, defining antiquotation is a regular user-space operation, just like
defining methods or attributes. For Isabelle2009 I have cleaned up all
these interfaces, to regain the clarity lost in 1999 when I was in a hurry
implementing syntax for attributes and methods "somehow".

OK, so let's go to src/Pure/ML/ml_antiquote.ML and study examples such as
@{term} or simular for 10-15 minutes. This is the outcome:

ML {*
ML_Antiquote.inline "term_pat"
(Args.context -- Scan.lift Args.name_source >>
(fn (ctxt, s) =>
let val t = ProofContext.read_term_pattern ctxt s
in ML_Syntax.atomic (ML_Syntax.print_term t) end))
*}

ML {* @{term_pat "?x + ?y"} *}

Note that we provide predefined antiquotations in Isabelle/Pure very
sparingly, because they essentially affect the Isabelle/ML language
itself. So one needs to be 120% sure about it; any later changes will
hurt existing applications more than the usual fine-tuning and renaming of
library functions.

Makarius

Last updated: May 03 2024 at 12:27 UTC