| | | B.4.3 case: Perform Case Distinction |
case A
case A1, A2, ..., An
In proving mode.
The command case A takes a formula A and extends the current proof states by two child states. Both states are duplicates of the current state except that in the first state A is added as an assumption while in the second state ¬A is added as an assumption. In other words, the command implements the rule
[E] ..., A |- ...
[E] ..., ~A |- ...
------------------
[E] ... |- ...
An additional proof state may be generated for a type checking condition corresponding to the value A.
The more general form case A1, A2, ..., An implements the rule
[E] ..., A1 |- ...
[E] ..., ~A1, A2 |- ...
...
[E] ..., ~A1, ~A2, ..., ~An |- ...
-----------------
[E] ... |- ...
Additional proof states may be generated for the type checking conditions corresponding to the values A1, A2, ....
The two proof states resulting from the application of case A are logically equivalent to the proof states resulting from the corresponding application of the command assume. However, the application of case leaves in the second state the goal unchanged.
The net effect of the execution of case A1, A2, ... is the same as that of a sequence of commands case A1, case A2, ..., executed (each command, apart from the first one, executed in the second state resulting from the application of the previous command).
| | | B.4.3 case: Perform Case Distinction |