Stream: Isabelle/ML

Topic: Understanding local theories

Johannes Neubrand (Jan 19 2022 at 17:10):

Hi all, I'm trying to create a function (with termination that should hopefully be proved by fun's default methods) and hit a bit of a roadblock trying to understand local theories. I'm experimenting with something like this:

ML ‹
val a_binding = @{binding a}
;
Function_Fun.add_fun
  [(a_binding, NONE, NoSyn)]
  [
    (((a_binding, []), @{term "HOL.Trueprop (a n = 3)"})
    , []
    , [])
  ]
  Function_Fun.fun_config
  @{context}
›

This leads to a "Missing local theory context" error. In general, how do I turn my @{context} into a local theory context? I found the cookbook section 4.3, but it doesn't really help me understand what's going on.

Lukas Stevens (Jan 19 2022 at 17:21):

local_setup ‹
let
  val a_binding = @{binding a}
in
  Function_Fun.add_fun
    [(a_binding, NONE, NoSyn)]
    [
      (((a_binding, []), @{term "HOL.Trueprop (a n = 3)"})
      , []
      , [])
    ]
    Function_Fun.fun_config
end
›

Lukas Stevens (Jan 19 2022 at 17:24):

add_fun transforms the local theory. Using local_setup, the local theory context will be passed to your function.

Last updated: Dec 21 2024 at 16:20 UTC