Изабель использует локаль или контекст за пределами локали

Question

Я определил локаль и доказал несколько теорем. Теперь мне нужно использовать их вне этой локали / контекста. Как я могу это сделать? Могу ли я получить теорему с гипотезами, расширенными предположениями локали? (Как это сделано в Coq.)

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

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

end

Мне нужно получить теорему "a∈A ==> a∈A" из thm, которая определена выше. (Мне не нужна именно эта теорема, это просто простейший пример получения теоремы с расширенным набором предположений. (Thm внутри mylocale имеет нулевые гипотезы))

Answer 1

Каждое определение и теорема в контексте локали генерирует глобальную версию. Вы можете получить доступ к этой глобальной версии (обобщенной по параметрам локали и расширенной с допущениями локали), используя locale_name.constant_name или locale_name.theorem_name. В вашем примере mylocale.thm дает вам то, что вы хотите.

Если вам нужно несколько теорем без обобщения параметров локали, вы можете интерпретировать локаль в неназванном контексте, который зафиксировал параметры и принял предположения , Вот пример:

 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