Я определил метод доказательства с использованием Eisbach в локали.Вызывая этот метод, Изабель, кажется, иногда выбирает его из-за неправильной интерпретации локали.Рассмотрим следующий минимальный пример:
theory Locale_Methods
imports Main "HOL-Eisbach.Eisbach"
begin
locale l =
fixes n :: nat
begin
method m = (rule trans [of _ n _])
end
locale l' = p: l
begin
lemma 1: "n = n"
proof p.m
oops
sublocale s: l "Suc n" .
lemma 2: "n = n"
proof p.m
oops
end
end
Метод m, определенный в локали l, заменяет цель формы i = j на две цели i = n и n = j.Положение курсора за proof p.m в лемме 1 показывает, что ожидаемые цели, n = n и еще один n = n, были сгенерированы.При наведении курсора на proof p.m в лемме 2 должны отображаться те же цели, но на самом деле цели n = Suc n и Suc n = n представлены.По-видимому, был выбран метод доказательства s.m.
Это ошибка в действии, или есть другое объяснение этого поведения?Как я могу получить доступ к p.m после объявления подлокары s?
Я использую Isabelle2018.