Как доказать следующие утверждения, используя Изабель / HOL?

Question

Может ли кто-нибудь помочь мне доказать X=M, используя следующий набор уравнений (логика первого порядка) в Изабель / HOL?

N>=M

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

X=N

, где N, M, X - целые константы.n целочисленная переменная .. '->' означает, подразумевается

Answer 1

Доказательство может быть выполнено только в том случае, если переменные натуральные , а не целые числа, например, используя это доказательство:

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.