2

I'm going through chapter 5 of concrete semantics.

I got some error while working through this toy example proof:

lemma
  shows "¬ ev (Suc 0)"

I know this is more than needed (since by cases) magically solves everything & gives a finished proof, but I wanted to make explicit the cases.

I tried this:

lemma
  shows "¬ ev (Suc 0)"
proof (rule notI)
  assume "ev (Suc 0)"
  then show False 
  proof (cases)
  case ev0
    then show ?case by blast
  next
    case evSS
    then show ?case sorry
qed

but if I put my mouse on the ?cases I get a complaint by Isabelle's (type checker?) verifier:

proof (chain)
picking this:

Failed to refine any pending goal 
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
  HOL.induct_true

what does this error mean?

Why can't I make the proof explicit with the case syntax here? even if it's trivial?

How question is, how do you close a case immediately?

If there are no cases to be proved you can close a proof immediately with qed.

is referenced later but I can't make it work for real proofs.

Charlie Parker
  • 5,884
  • 57
  • 198
  • 323
  • "If there are no cases to be proved you can close a proof immediately with qed.". I am not certain what the problem is. I believe, in your example, you can simply write `then show False proof cases qed` or, better yet, `then show False by cases`. If we are using the same definition of `ev`, then this should be enough to finish the proof. – user9716869 - supports Ukraine May 20 '20 at 21:13
  • "but if I put my mouse on the ?cases I get a complaint...". I believe that the auto-generated proof outline is redundant in this situation: there are no cases to be proved. See my previous comment. – user9716869 - supports Ukraine May 20 '20 at 21:16

1 Answers1

1

The auto-generated proof outline is sometimes just wrong. This is one such case.

The reason why cases solves your goal here is that it does some pre-simplification of the cases (as documented in §6.5.2 of the Isabelle/Isar reference manual). This is enough to make both cases disappear automatically here, since they are clearly impossible. Your proof state therefore has no proof obligations left, and Isar only allows you to prove things with show that you still have to prove. That's why you get the error message Failed to refine any pending goal: There simply are no pending goals.

You can disable the pre-simplification of cases using the (no_simp) parameter, i.e.

proof (cases (no_simp))

Note however that cases does not define the ?case variable because it does not change the goal. Just use ?thesis instead.

Manuel Eberl
  • 7,858
  • 15
  • 24