[isabelle] Correct handling of fixed and free variables



Dear list,

I'm currently working on enhanced tracing capabilities in the
simplifier, and as such implement a capability to set "term
breakpoints". The idea is that the user can specify a term pattern, and
if that pattern occurs in a simplification step, certain actions are
triggered.

To declare a breakpoint, I'd like to have a command (could also be an
attribute, but that is not important at this point) which works in proof
mode and parses a specified term and adds it to an internal data
structure. The usual use case could be something like

  have "...."
    using [[break_term "?x > 0"]]

The problem is how to parse the term. A naive use of `Syntax.read_term`
fails because `?x` is an unknown schematic variable. On the other hand,
the @{cpat} antiquotation which seems like a good fit handles already
existing schematic variables not quite correctly:

notepad
begin
  let ?x = 0
  ML_prf{*
    @{cpat "?x > ?y"}
    (* produces:   `val it = "?y < ?x": cterm` *)
    (* instead of: `val it = "?y < 0": cterm`  *)
  *}
end

To summarize the constraints: I'd like to have a `Proof.context`-aware
term parsing, which works correctly for existing schematic and locally
fixed variables. Lars Noschinski also pointed out that care needs to be
taken of these two different kinds of fixed variables:

notepad begin
   { have P sorry } note A = this
   { fix P have P sorry } note B = this
end

Regards
Lars





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