Dinamakan kasus fungsi yang dibuktikan dengan induksi

Apakah mungkin menggunakan nama pred_Zero dan pred_Suc sebagai pengganti 1 dan 2 dalam pembuktian dengan induksi berikut?

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 sumber

Jawaban (1)


arrow_upward
2
arrow_downward

Anda dapat memberi nama pada kasus aturan induction atau cases menggunakan atribut case_names:

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

Nama yang lebih kanonik untuk kasus ini adalah 0 dan Suc, dan dalam kasus khusus ini Anda sebaiknya tetap menggunakan aturan induksi default nat.induct karena aturan induksi yang dihasilkan untukpred identik dengan nat.induct.

person Manuel Eberl    schedule 02.03.2021
comment
Terima kasih! Itu hanyalah contoh yang disederhanakan. Secara umum saya mendefinisikan fungsi yang lebih rumit dengan banyak kasus. Jadi pembuktian dengan 1, 2, 3, ... tidak terbaca. Jika saya memahami Anda dengan benar, saya harus mendefinisikan sesuatu seperti lemmas pred_induct = pred.induct [case_names 0 Suc]? Ini dilakukan secara otomatis untuk predikat induktif, mengapa tidak untuk fungsi? Atau saya salah memahami sesuatu? - person Denis; 02.03.2021
comment
Ya, Anda bisa melakukannya dengan cara itu. Saya tidak tahu mengapa paket fungsi tidak melakukannya. Namun jarang juga memberi nama pada masing-masing kasus klausa fungsi. Saya sendiri tidak dapat mengingat pernah melihat itu sebelumnya. - person Manuel Eberl; 03.03.2021