CasesbossLib.Cases : tacticPerforms case analysis on the variable of the leading universally quantified variable of the goal.
When applied to a universally quantified goal ?- !u. G,
Cases performs a case-split, based on the cases theorem for
the type of u stored in the global TypeBase
database.
The cases theorem for a type ty will be of the form:
|- !v:ty. (?x11...x1n1. v = C1 x11 ... x1n1) \/ .... \/
(?xm1...xmnm. v = Cm xm1 ... xmnm)where there is no requirement for there to be more than one disjunct,
nor for there to be any particular number of existentially quantified
variables in any disjunct. For example, the cases theorem for natural
numbers initially in the TypeBase is:
|- !n. (n = 0) \/ (?m. n = SUC m)Case-splitting consists of specialising the cases theorem with the
variable from the goal and then generating as many sub-goals as there
are disjuncts in the cases theorem, where in each sub-goal (including
the assumptions) the variable has been replaced by an expression
involving the given ‘constructor’ (the Ci’s above) applied
to as many fresh variables as appropriate.
Fails if the goal is not universally quantified, or if the type of
the universally quantified variable does not have a case theorem in the
TypeBase, as will happen, for example, with variable
types.
If we have defined the following type:
- Hol_datatype `foo = Bar of num | Baz of bool`;
> val it = () : unitand the following function:
- val foofn_def = Define `(foofn (Bar n) = n + 10) /\
(foofn (Baz x) = 10)`;
> val foofn_def =
|- (!n. foofn (Bar n) = n + 10) /\
!x. foofn (Baz x) = 10 : thmthen it is possible to make progress with the goal
!x. foofn x >= 10 by applying the tactic
Cases, thus:
?- !x. foofn x >= 10
====================================================== Cases
?- foofn (Bar n) >= 10 ?- foofn (Baz b) >= 10producing two new goals, one for each constructor of the type.