如何使用 Isabelle/HOL 证明以下陈述？

【问题标题】：how to prove following statements using Isabelle/HOL?如何使用 Isabelle/HOL 证明以下陈述？
【发布时间】：2019-09-23 10:56:43
【问题描述】：

谁能帮我证明 X=M 在 Isabelle/HOL 中使用以下方程组（一阶逻辑）？

N>=M

forall n. 0=<n<N --> n<M

X=N

其中N, M, X 是整数常量。 n整型变量.. '-->' 代表暗示

【问题讨论】：

标签： isabelle first-order-logic

【解决方案1】：

只有当变量是 naturals 而不是整数时才能进行证明，例如使用这个证明：

theory Scratch
imports Main
begin
theorem
  fixes N M X :: nat
  assumes "N ≥ M"
  assumes "∀ n. (0 ≤ n ∧ n < N) ⟶ n<M"
  assumes "X = N"
  shows "X = M"
proof-
  have "¬ N > M"
  proof
    assume "M < N" with `∀ n. _` show False by auto
  qed
  with `N ≥ M` and `X = N`
  show "X = M" by auto
qed

end

如果您允许整数，则反例将是 M=-2、N=-1 和 X=-2。

【讨论】：

非常感谢。还有一个问题，如果属性是 X=N^3，那么我们需要定义幂。你能在这方面指导我吗？
我想你可以写N ^ 3来获取权力。