Stream: Isabelle/ML

Topic: Do not note function theorems

Jan van Brügge (Sep 14 2022 at 16:55):

Is it possible to prevent Function.add_function from noting the theorems about the function? I define one that is purely internal and only want to give the user some higher level theorems, not what is generated. (ie the function is an implementation detail that should not leak)

Dmitriy Traytel (Sep 17 2022 at 12:55):

I don't think you can completely hide it. I see this code in bnf_gfp_grec_sugar

fun add_function binding parsed_eq lthy =
  let
    fun pat_completeness_auto ctxt =
      Pat_Completeness.pat_completeness_tac ctxt 1 THEN auto_tac ctxt;

    val ({defname, pelims = [[pelim]], pinducts = [pinduct], psimps = [psimp], ...}, lthy') =
      Function.add_function [(Binding.concealed binding, NONE, NoSyn)]
        [(((Binding.concealed Binding.empty, []), parsed_eq), [], [])]
        Function_Common.default_config pat_completeness_auto lthy;
  in
    ((defname, (pelim, pinduct, psimp)), lthy')
  end;

Making the bindings "concealed" should hide them from end users (e.g., via find_theorems) and from ATPs (via Sledgehammer). But I guess, if you know the function name you can still find its simps.

Last updated: Apr 26 2024 at 16:20 UTC