Re: [isabelle] Hiding facts from find_theorems



On 29/03/18 15:18, Manuel Eberl wrote:
> 
> I have a large theory that defines a lot of very technical internal
> theorems that are designed to be easily composable from ML and that are
> of no interest to an Isabelle user.
> 
> I currently mark them as "qualified" to avoid namespace pollution, but
> still allow using them from outside e.g. if another theory wants to
> extend the tool I'm building. However, there seems to be no way (not
> through "private" nor through "hide_fact") to actually stop the theorem
> from showing up in "find_theorems".

This is controlled by a somewhat older layer in name space management:
Binding.concealed or Name_Space.concealed (in Isabelle/ML).

The included Scratch.thy provides an example for global theory
specifications.


I can't say on the spot if the "concealed" flag should or could become a
qualifier like 'private' / 'qualified'. There is a lot of accumulated
complexity here.


	Makarius
theory Scratch
  imports Main
begin

ML \<open>val theory_naming = Sign.naming_of @{theory}\<close>
setup \<open>Sign.map_naming Name_Space.concealed\<close>

definition "foo x = x"

lemma aaa: "foo (foo x) = x"
  by (simp add: foo_def)

find_theorems name: aaa

setup \<open>Sign.map_naming (K theory_naming)\<close>

lemma bbb: "foo (foo (foo x)) = x"
  by (simp add: foo_def)

find_theorems name: bbb

end


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