Custom case distinctions in proofs

Question

Does Isabelle support custom case distinctions when proving statements? Let's say I want to prove a statement for all natural numbers n, but the proof is entirely different depending on whether n is even or odd. Is it possible to do that case distinction in a proof, like

 proof(cases n) 
   assume "n mod 2 = 0"
   <proof>
   next assume "n mod 2 = 1"
   <proof>
qed

So far, I'd split the lemma/theorem in two seperate parts (assuming n even/odd) and then use these parts to proof the statement for all natural numbers, but that does not appear to be the optimal solution.

score 6 · Accepted Answer · answered Jan 26 '18 at 12:27

6

In Isabelle2017, you can prove ad-hoc case distinction rules easily, like so:

lemma "P (n::nat)"
proof -
  consider (odd) "odd n" | (even) "even n" by auto
  then show ?thesis
  proof cases
    case odd
    then show ?thesis sorry
  next
    case even
    then show ?thesis sorry
  qed
qed

answered Jan 26 '18 at 12:27

larsrh

2,579
8
30

1

While this is true (and has some advantages, e.g. being able to use `case`), `odd n` is just an abbreviation for `¬even n`, so one can just use the default case distinction rule: `have P proof cases assume "even n" … next assume "odd n" … qed` – Manuel Eberl Jan 26 '18 at 13:01

score 0 · Answer 2 · edited Mar 14 '18 at 11:47

0

You can probably try the following thing:

proof -
   have "your statement" when "n mod 2 = 0"
   <proof>
   moreover
   have "your statement" when "n mod 2 = 1"
   <proof>
   ultimately
   show "your statement"
     by <some tactic>
qed

edited Mar 14 '18 at 11:47

chris

4,988
20
36

answered Jan 26 '18 at 12:35

A. Bordg

101
3

Custom case distinctions in proofs

2 Answers2