How to prove this simple theorem in Isabelle?

Question

I define a very simple function replace which replaces 1 with 0 while preserving other input values. I want to prove that the output of the function cannot be 1. How to achieve this?

Here's the code.

theory Question
  imports Main
begin
fun replace :: "nat ⇒ nat" where
"replace (Suc 0) = 0" |
"replace x = x"

theorem no1: "replace x ≠ (Suc 0)"
  sorry
end

Thanks!

Answer 1

There exist several approaches for proving the statement that you are trying to prove.

---

You can make an attempt to use sledgehammer to find the proof automatically, e.g.

theorem no1: "replace x ≠ (Suc 0)"
  by sledgehammer
  (*using replace.elims by blast*)

Once the proof is found, you can delete the explicit invocation of the command sledgehammer.

Perhaps, a slightly better way to state the proof found by the sledgehammer would be

theorem no1': "replace x ≠ (Suc 0)"
  by (auto elim: replace.elims)

---

You can also try to provide a more specialized proof. For example,

theorem no1: "replace x ≠ (Suc 0)"
  by (cases x rule: replace.cases) simp_all

This proof looks at the different cases the value of x can have and then uses simplifier (in conjunction with the simp rules provided by the command fun during the definition of your function) to finish the proof. You can see all theorems that are generated by the command fun by typing print_theorems immediately after the specification of replace, e.g.

fun replace :: "nat ⇒ nat" where
  "replace (Suc 0) = 0" |
  "replace x = x"

print_theorems 

---

Of course, there are other ways to prove the result that you are trying to prove. One good way to improve your ability to find such proofs is by reading the documentation and tutorials on Isabelle. My own starting point for learning Isabelle was the book "Concrete Semantics" by Tobias Nipkow and Gerwin Klein.