Isabelle use Locale or Context outside of any locale

Question

I have defined locale and proved a few theorems. Now I need to use them outside of this locale/context. How can I do so? Can I obtain theorem with hypotheses extended by locale's assumptions? (Like it is done in Coq.)

locale mylocale =
  assumes H1:‹a ∈ A›
begin

theorem thm:‹a∈A›
  by (rule H1)

end

I need to obtain theorem "a∈A==>a∈A" from thm that is defined above. (I don't need exactly this theorem, it's just a simplest example of obtaining theorem with extended set of assumptions.(thm inside mylocale has zero hypotheses))

Andreas Lochbihler Andreas Lochbihler · Accepted Answer · 2020-04-10T07:28:42

Every definition and theorem in a locale context generates a global version. You can access this global version (generalized over the locale parameters and extended with the locale assumptions) using locale_name.constant_name or locale_name.theorem_name. In your example, mylocale.thm gives you what you want.

If you need several theorems without the generalization of the locale parameters, you can interpret the locale in an unnamend context that has fixed the parameters and assumed the assumptions. Here's an example:

 locale l = fixes a :: 'a assumes "a ~= undefined" begin
 definition foo :: 'a where "foo = a"
 lemma lem: "a = foo" by(simp add: foo_def)
 end

 thm l.lem (* a is generalized to ?a *)

 consts bar :: nat

 context assumes *: "bar ~= undefined" begin
 interpretation bar: l bar by(fact bar)
 thm lem (* a is instantiated with bar *)
 end

Isabelle use Locale or Context outside of any locale

1 Answers