Изабель / HOL: доступ к интерпретации в другом регионе - PullRequest
Новая
       10

Изабель / HOL: доступ к интерпретации в другом регионе

0 голосов
/ 11 июня 2018

Есть библиотека Isabelle / HOL, на которой я хочу построить новые определения и доказательства.Библиотека определяет locale2, на которой я хотел бы построить.Внутри locale2 есть интерпретация locale1.

Чтобы расширить locale2 в отдельной теории, я определяю locale3 = locale2.Однако внутри locale3 я не могу понять, как получить доступ к интерпретации locale2 для locale1.Как я могу это сделать?(Я вообще вообще об этом правильно говорю?)

Ниже приведен MWE.Это теория библиотеки с языком, который я хочу расширить: 

theory ExistingLibrary
  imports Main
begin

(* this is the locale with the function I want *)
locale locale1 = assumes True
begin

fun inc :: "nat ⇒ nat"
  where "inc n = n + 1"

end

(* this is the locale that interprets the locale I want *)
locale locale2 = assumes True
begin

interpretation I: locale1
  by unfold_locales auto

end
end

Это моя теория расширения.Моя попытка находится внизу, вызывая ошибку: 

theory MyExtension
  imports ExistingLibrary
begin

locale locale3 = locale2
begin

definition x :: nat
  where "x = I.inc 7" (* Undefined constant: "I.inc" *)

end
end

1 Ответ

0 голосов
/ 12 июня 2018

Интерпретации внутри контекста продолжаются только до конца контекста.Когда контекст вводится снова, вам нужно повторить интерпретацию, чтобы сделать определения и теоремы доступными: 

locale 3 = locale2 begin
interpretation I: locale1 <proof>

По этой причине я рекомендую разделить первый шаг интерпретации на два:

  1. Лемма с именем, которая доказывает цель этапа интерпретации.
  2. Сама команда interpretation, которая может быть доказана by(rule лемма )

Если вы хотите, чтобы интерпретация выполнялась всякий раз, когда вы открываете локаль и всякий раз, когда вы интерпретируете локаль, тогда лучше будет sublocale вместо interpretation.

...