Proving theorem in Isar with no local assumptions

Question

The statement n+0 = n is quite trivial to prove:

theorem add_0: "n+0 = (n::nat)"
  apply(simp)
  done

Upon trying to convert it to Isar however, I've noticed that it doesn't seem to require any assumption. So in the this attempt:

theorem add_0: "n+0 = (n::nat)"
proof -
  thus "True" by simp
qed

It fails, as there are "No current facts available". This second attempt also fails:

theorem add_0: "n+0 = (n::nat)"
proof -
  from add_0 show "True" by simp
qed

This time with the error "Failed to refine any pending goal".

Is it possible to prove a statement that requires no assume clause in Isar? If yes, then how?

Answer 1

There are two problems with thus "True"

1. As you've noted, the proof state that you begin doesn't have any assumptions, therefore no facts in the proof state. The abbreviation thus expands to then show, as we have no facts in our proof state it doesn't make sense to use then so we should instead replace it with show.
2. show "True" is saying that we want to prove "True" instead we want to prove the goal of the theorem. We can use the schematic variable ?thesis to refer to the original thesis of the theorem. The error Failed to refine any pending goal is just saying that if we were to prove that True is true, it wouldn't help solve the goal of our thesis.

So we can prove our original theorem with an Isar proof using the following pattern.

theorem add_0: "n+0 = (n::nat)"
proof -
  show ?thesis by simp
qed