Изабель разрешает интерпретацию

Я использую Isabelle 2019, и у меня возникли некоторые проблемы с местными жителями:

Я создаю локаль с аббревиатурой, например:

interpretation myInstance : myLocale "abbreviation"

Я использую это с функцией из локали, например:

myInstance.getter myinput

Но apply simp теперь "упрощает" цель примерно так

myLocale.getter "abbreviation" myinput

Как я могу избежать простоты, чтобы сделать это? (Я почти уверен, что это причина, по которой мой код обрабатывается целую вечность)...

Лучший


locale interpretation isabelle
person Kevin    schedule 22.03.2020    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Это известная проблема. нет идеального решения. Некоторые частичные решения:

  • живите с этим/избегайте использования чего-то, что можно упростить. Используйте определение вместо аббревиатуры (и в конечном итоге пометьте определение как простое, чтобы автоматически развернуть его).

  • добавить правило соответствия (как упоминалось ): ⋀a b. myLocale.getter a b == myLocale.getter "abbreviation" myinput a b. Не всегда получается.

  • Определите новую константу и поднимите все теоремы до этой константы. Это раздражает (и может сделать кувалду менее мощной).

person Mathias Fleury    schedule 22.03.2020