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

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

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

isabelle isar
person Joachim Breitner    schedule 16.10.2014    source источник

Ответы (2)


arrow_upward
2
arrow_downward

Метод default внутренне вызывает методы rule, unfold_locales и intro_classes. Ни одно из них не поддерживает case имена (для unfold_locales это уже обсуждалось на список рассылки Изабель в 2008 году). Таким образом, невозможно заставить систему case_name работать с default. В этой ветке упоминаются два важных момента:

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

  2. 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 заключается в том, что реализация не отслеживает, какая подцель исходит от наследования языкового стандарта. Если у вас есть свободное время, не стесняйтесь реализовать поддержку имен случаев.

person Andreas Lochbihler    schedule 16.10.2014
comment
Спасибо, особенно за указание на Foo.intro. У меня было ощущение, что это так, но я не нашел, потому что теорема не проявляется, когда я выдаю find_theorems Foo. - person Joachim Breitner; 16.10.2014
comment
У меня была такая же проблема, и поэтому я использовал неудобные вспомогательные леммы в своем ответе ниже. - person chris; 16.10.2014

arrow_upward
1
arrow_downward

Насколько мне известно, методы 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)

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

person chris    schedule 16.10.2014