如何使用 Isabelle/HOL 证明以下陈述?
how to prove following statements using Isabelle/HOL?
谁能帮我证明 X=M
在 Isabelle/HOL 中使用下面的方程组(一阶逻辑)?
N>=M
forall n. 0=<n<N --> n<M
X=N
其中 N, M, X
是整数常量。 n
整型变量.. '-->'代表隐含
仅当变量是自然数而不是整数时才能进行证明,例如使用此证明:
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=M
在 Isabelle/HOL 中使用下面的方程组(一阶逻辑)?
N>=M
forall n. 0=<n<N --> n<M
X=N
其中 N, M, X
是整数常量。 n
整型变量.. '-->'代表隐含
仅当变量是自然数而不是整数时才能进行证明,例如使用此证明:
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
。