Re: [isabelle] schematic variables and antiquotations



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.