Retrieving Symbol Definition in Isabelle - Stack Overflow

admin管理员组

文章数量:1346196

I'm interested in simulating the effect of going to the definition of a constant (ctrl + click) in Isabelle. So given a symbol, for example AExp.plus in ~~/src/HOL/IMP/AExp, I want to recover the definition:

fun plus :: "aexp ⇒ aexp ⇒ aexp" where
"plus (N i⇩1) (N i⇩2) = N(i⇩1+i⇩2)" |
"plus (N i) a = (if i=0 then a else Plus (N i) a)" |
"plus a (N i) = (if i=0 then a else Plus a (N i))" |
"plus a⇩1 a⇩2 = Plus a⇩1 a⇩2"

My first attempt at doing this was extracting transitions and constants and trying to do some string matching in Python. This works for simple cases but doesn't generalize without getting very messy.

It seems like like this should be doable with an ML block. One approach I'm exploring is using:

theory Scratch
            imports Main "~~/src/HOL/IMP/AExp" begin
ML‹
val def = Defs.specifications_of (Theory.defs_of @{theory}) (Defs.Const, "AExp.plus")  ;
›
end

This outputs:

val def =
   [{def = SOME "AExp.plus_def", description = "AExp.plus_def", lhs = [], pos =
     {offset=1, end_offset=4, label=command.fun, id=17644}, rhs =
     [((Const, "Product_Type.Pair"), ["AExp.aexp", "AExp.aexp"]),
      ((Const, "AExp.plus_sumC"), []),
      ((Type, "fun"), ["AExp.aexp", "AExp.aexp × AExp.aexp"]),
      ((Type, "fun"), ["AExp.aexp", "AExp.aexp ⇒ AExp.aexp × AExp.aexp"]),
      ((Type, "Product_Type.prod"), ["AExp.aexp", "AExp.aexp"]),
      ((Type, "fun"), ["AExp.aexp × AExp.aexp", "AExp.aexp"]),
      ((Type, "AExp.aexp"), [])]}]:
   Defs.spec list

Is this information sufficient to recover the definition as it appears in the source code? Or can I recover the definition using a different approach? Any guidance is highly appreciated!

本文标签： Retrieving Symbol Definition in IsabelleStack Overflow