Случаи именованных функций в доказательстве по индукции

Можно ли использовать имена pred_Zero и pred_Suc вместо 1 и 2 в следующем доказательстве по индукции?

fun pred where
  pred_Zero:
  "pred 0 = 0"
| pred_Suc:
  "pred (Suc n) = n"

lemma pred_le:
  "pred n ≤ n"
proof (induct rule: pred.induct)
  case 1
  thus ?case by simp
next
  case (2 n)
  thus ?case by simp
qed

isabelle
person Denis    schedule 02.03.2021    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Вы можете присвоить имена случаям правила induction или cases с помощью атрибута case_names:

proof (induct rule: pred.induct [case_names pred_Zero pred_Suc])

Более каноническими именами для случаев были бы 0 и Suc, и в этом конкретном случае вы могли бы в любом случае просто использовать правило индукции по умолчанию nat.induct, поскольку правило индукции, сгенерированное дляpred, идентично nat.induct.

person Manuel Eberl    schedule 02.03.2021
comment
Спасибо! Это просто упрощенный пример. В общем, я определяю более сложную функцию с большим количеством случаев. Таким образом, доказательство с помощью 1, 2, 3, ... нечитаемо. Если я вас правильно понял, то я должен определить что-то вроде lemmas pred_induct = pred.induct [case_names 0 Suc]? Это делается автоматически для индуктивных предикатов, почему не для функций? Или я что-то неправильно понял? - person Denis; 02.03.2021
comment
Да, так можно. Я не знаю, почему пакет функций этого не делает. Но также несколько необычно давать имена отдельным случаям функциональных предложений. Я, например, не могу припомнить, чтобы видел это раньше. - person Manuel Eberl; 03.03.2021