Search code examples
isabellefirst-order-logic

how to prove following statements using Isabelle/HOL?

Can anyone please help me to prove X=M using the following set of the equation(first-order logic)in Isabelle/HOL?

N>=M

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

X=N

where N, M, X are integers constant. n integer variable.. '-->' stands for implies

Solution

  • The proof can only be done if the variables are naturals, not integers, e.g. using this proof:

    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

    If you allow integers than a counter-example wold be M=-2, N=-1 and X=-2.