Как исправить «частично примененную константу в левой части уравнения кода»?

Question

Я пытаюсь определить кодовое уравнение:

datatype t = A | B | C

inductive less_t :: "t ⇒ t ⇒ bool" where
  "less_t A B"
| "less_t B C"

code_pred [show_modes] less_t .

fun less_t_fun :: "t ⇒ t ⇒ bool" where
  "less_t_fun A A = False"
| "less_t_fun A B = True"
| "less_t_fun A C = True"
| "less_t_fun B C = True"
| "less_t_fun B _ = False"
| "less_t_fun C _ = False"

lemma tancl_less_t_code [code]:
  "less_t⇧+⇧+ x y ⟷ less_t_fun x y"
  apply (rule iffI)
  apply (erule tranclp_trans_induct)
  apply (erule less_t.cases; simp)
  apply (metis less_t_fun.elims(2) less_t_fun.simps(3) t.simps(4))
  apply (induct rule: less_t_fun.induct; simp)
  using less_t.intros apply auto
  done

value "less_t A B"
value "less_t_fun A C"
value "less_t⇧+⇧+ A C"

И получаю следующее предупреждение:

Partially applied constant "less_t" on left hand side of equation, in theorem:
less_t⇧+⇧+ ?x ?y ≡ less_t_fun ?x ?y

Этот вопрос не связан с переходными замыканиями.Я уже получил такое предупреждение для разных теорем:

• Частично примененная константа в левой части кодового уравнения
• Как использовать разные кодовые леммыдля разных режимов индуктивного предиката?

Мне просто нужно понять смысл этого предупреждения и как его исправить.Может быть, я должен определить другую лемму?

Answer 1

Проблема в том, что структура вашей леммы tancl_less_t_code действительно не подходит в качестве кодовых уравнений.Обратите внимание, что самой внешней константой в левой части уравнений является предикат транзитивного замыкания tranclp.Таким образом, это говорит генератору кода использовать лемму для реализации tranclp.Однако, используя вашу лемму, известно только, как реализовать tranclp для одного конкретного предиката, а именно less_t.Поэтому вы получаете жалобу от Изабель, что ваша реализация слишком конкретна.

Есть как минимум два обходных пути.

Во-первых, вместо объявления [code] вы можете использовать [code unfold].Тогда каждое вхождение tranclp less_t x y будет заменено на less_t_fun во время генерации кода.Чтобы сделать это правило еще более применимым, я бы затем переформулировал лемму на tranclp less = less_t_fun, так что даже если tranclp less_t не применен полностью, разворачивание может произойти.

Во-вторых, вы можете взять симметричную версиювашей леммы и объявить ее как [simp].Тогда в вашей реализации вы просто вызываете less_t_fun вместо tranclp less_t, и в доказательствах упрощатель переключится на последний.

Для получения дополнительной информации о [code] и [code_unfold] смотритедокументация генератора кода.