cases vs case_tac/induct vs induct_tac

Question

I've been working with Isabelle/HOL for a few months now, but I've been unable to figure out the exact intention of the use of _tac.

Specifically, I'm talking about cases vs case_tac and induct vs indut_tac (although it would be nice to know the meaning of tac in general, since I'm also using other methods such as cut_tac).

I've noticed I can't use cases or induct using apply with ⋀-bound variables, but I can if it's an structured proof. Why?

An example of this:

    lemma "¬(∀x. ¬(P x)) ⟹ ∃x. P x"
  apply (rule ccontr)
  apply (erule notE)
  apply (rule allI)
  apply (case_tac "P x")
  apply (erule notE)
  apply (erule exI)
  apply assumption
  done

On the other hand, another difference I've noticed between induct and induct_tac is that I can use double induction with the latter, but not with the former. Again, I'm clueless why.

Thanks in advance.

*_tac are built-in tactics used in Isabelle proof scripts. I strongly suggest that you use Isabelle/Isar instead. — Javier Díaz
I don't understand what you mean by using "Isabelle/Isar" instead. — Darsen
I mean writing structured proofs using the Isabelle/Isar language environment. I strongly suggest you read this tutorial on Isabelle/HOL and The Isabelle/Isar Reference Manual for further information. — Javier Díaz
Regarding the specific issues with the use of the proof methods cases and induction versus the use of the tactics case_tac and induct_tac it would be good to see an example of what you're trying to achieve. — Javier Díaz

Javier Díaz Javier Díaz · Accepted Answer · 2021-06-06T00:55:47

*_tac are built-in tactics used in apply-scripts. In particular, case_tac and induct_tac have been basically superseded by the cases and induction proof methods in Isabelle/Isar. As you mentioned, case_tac and induct_tac can handle ⋀-bound variables. However, this is quite fragile, since their names are often generated automatically and may change when Isabelle changes (of course, you could use rename_tac to choose fixed names). That's one of the reasons why nowadays structured proof methods are preferred to unstructured tactic scripts. Now, back to your example: In order to be able to use cases, you can introduce a structured block as follows:

lemma "¬(∀x. ¬(P x)) ⟹ ∃x. P x"
  apply (rule ccontr)
  apply (erule notE)
  proof (intro allI)
    fix x
    assume "∄x. P x"
    then show "¬ P x"
      apply (cases "P x")
      apply (erule notE)
      apply (erule exI)
      apply assumption
      done
  qed

As you can see, structured proofs are typically verbose but much more readable than linear apply-scripts.

If you're still curious about the "double-induction" issue, an example would be very welcome. Finally, if you want to learn more about structured proofs using the Isabelle/Isar language environment, I'd strongly suggest you read this tutorial on Isabelle/HOL and The Isabelle/Isar Reference Manual for more detailed information.

cases vs case_tac/induct vs induct_tac

1 Answers