在 HOL 中证明非负整数是有根据的 或者只是它们的归纳原理

如何解决在 HOL 中证明非负整数是有根据的 或者只是它们的归纳原理

我想在 HOL 中证明非负整数是有根据的。 怎么办？

DeFinition int_lt_def:
  int_lt = λ(x:int). λ(y:int). (0≤x)/\(x<y)
End

Theorem WF_int_lt:
  WF int_lt
Proof
  simp [relationTheory.WF_DEF] >>
  gen_tac >>
  simp [int_lt_def] >>
  cheat
QED

我知道，自然数和非负数之间存在双射。

这个双射保留了两种方式的顺序。

归纳原理适用于自然数。

从归纳原则遵循最小数原则。

如果我有正数的归纳原理，那么我可以重复证明，证明非负整数的最小数原理。

所以我认为主要问题可以浓缩为以下问题：

如何证明非负数的归纳原理？

原则：

∀P. (∀x. (∀y. 0 ≤ y ∧ y < x ⇒ P y) ⇒ P x) ⇒ ∀x. P x