Имена случаев для интерпретации локали

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

locale Foo = 
    fixes P 
    assumes 0: "P 0" 
    assumes Suc: "P n ⟹ P (Suc n)" 

interpretation Foo "λ _ . True" 
proof(default) 
    case 0 show ?case.. 
next 
    case (Suc n) show ?case .. 
qed

источник

2014-10-16 Joachim Breitner

Метод default внутренним образом называет методы rule, unfold_locales и intro_classes. Ни одна из них не поддерживает имена case (для unfold_locales, об этом уже говорилось на Isabelle mailing list in 2008). Таким образом, нет способа получить систему case_name для работы с default. Этот поток упоминает два важных момента:

Если иерархия локаль плоская, unfold_locales в основном только относится правило Foo.intro где Foo это имя локали. Если у вас сложная иерархия локалей, она проверяет, какие интерпретации уже доступны, и соответственно сочетает в себе правила .intro.
cases - канонический метод получения имен имен.

Таким образом, вы можете получить к регистру имена вручную с case_name атрибута:

interpretation Foo "λ _ . True" 
proof(cases rule: Foo.intro[case_names 0 Suc])

Конечно, вы можете также маркировать теорему с именами случае, если вам это нужно несколько раз:

lemmas Foo_intro[case_names 0 Suc] = Foo.intro

Проблема с поддержкой имени регистра в unfold_locales заключается в том, что реализация не отслеживает, какая из подцелей приходит из этого наследования локали. Если у вас есть свободное время, не стесняйтесь внедрять поддержку имен имен.

источник

2014-10-16 11:57:34

Спасибо, особенно за указание 'Foo.intro'. У меня было ощущение, что это так, но не найти его, потому что теорема не появляется, когда я выхожу 'find_theorems Foo'. –

У меня была такая же проблема, и поэтому я использовал неудобные вспомогательные леммы в моем ответе ниже. – chris

Насколько я знаю методы induct и case ответственны за создание названных случаев. Таким образом, я не вижу способ, которым default будет делать, как вы просите.

Вы можете ввести новое правило, как

lemma foo_rule [case_names 0 Suc]: 
    assumes "P 0" 
    and "⋀n. P n ⟹ P (Suc n)" 
    shows "foo P" 
    using assms by (simp add: foo_def)

или в качестве альтернативы, как

lemmas foo_rule [case_names 0 Suc] = 
    conjI [THEN foo_def [THEN meta_eq_to_obj_eq, THEN iffD2], rule_format]

если вы склонны константы выглядит. А затем использовать

interpretation foo "λ_. True" 
proof (induct rule: foo_rule)

Нечаянно я узнал, что объявление foo_rule [case_names 0 Suc, induct type] позволяет опустить имя правила, т.е.

interpretation foo "λ_. True" 
proof (induct)

Но я мог себе представить, что это будет нарушать существующие правила INDUCT по умолчанию.

источник

2014-10-16 11:37:29 chris

Имена случаев для интерпретации локали

ответ

Смежные вопросы