У меня есть структура локали, в которой определенная локаль появляется два раза как предок другой локали, один раз через наследование, а другой через последовательность из нескольких sublocale интерпретаций.Параметры двух экземпляров локали этого предка равны, но не идентичны (их равенство должно быть и может быть установлено с помощью доказательства).Как я могу заставить Изабель свернуть эти два экземпляра локали предка в один, как это было бы, когда параметры были идентичны?
Следующий минимальный пример демонстрирует мою ситуацию:
theory Diamond
imports Main
begin
typedecl a
typedecl b
typedecl c
consts a_from_b :: "b ⇒ a"
consts b_from_a_and_c :: "[a, c] ⇒ b"
lemma equality: "a_from_b (b_from_a_and_c a c) = a"
sorry
locale a =
fixes a :: a
locale b =
fixes b :: b
begin
sublocale a "a_from_b b" .
end
locale c = a +
fixes c :: c
begin
sublocale b "b_from_a_and_c a c" .
end
end
Команда print_dependencies! c дает следующий вывод:
dependencies:
a "a"
a "a_from_b (b_from_a_and_c a c)"
b "b_from_a_and_c a c"
c "a" "c"
Очевидно, есть два экземпляра a.Как я могу использовать лемму, упомянутую в приведенном выше фрагменте кода, чтобы превратить эти два экземпляра локали в один экземпляр a "a"?Я пытался добиться этого, изменив интерпретацию sublocale в объявлении locale c следующим образом:
sublocale b "b_from_a_and_c a c" rewrites "a = a_from_b (b_from_a_and_c a c)"
by (simp add: equality)
Однако это приводит к зависанию Изабель.