Proof Method. case_tac [isa-001L]

The case_tac method splits the current goal into multiple cases. Given a term t of type \tau , apply (case_tac t) will produce a new goal for each possible case of t according to the .cases theorem for the type \tau .

This works for all types defined with datatype, as well as for natural numbers (type nat) and bools — often an easier way to do classical reasoning than using rule ccontr.