`MATCH_CONV : term -> thm`

SYNOPSIS
Expands application of pattern-matching construct to particular case.

DESCRIPTION
The conversion MATCH_CONV will reduce the application of a pattern to a specific argument, either for a term match x with ... or (function ...) x. In the case of a sequential pattern, the first match will be reduced, resulting either in a conditional expression or simply one of the cases if it can be deduced just from the pattern. In the case of a single pattern, it will be reduced immediately.

FAILURE CONDITIONS
MATCH_CONV tm fails if tm is neither of the two applications of a pattern to an argument.

EXAMPLE
In cases where the structure of the argument determines the match, a complete reduction is performed:
```  # MATCH_CONV `match [1;2;3;4;5] with CONS x (CONS y z) -> z`;;
val it : thm =
|- (match [1; 2; 3; 4; 5] with CONS x (CONS y z) -> z) = [3; 4; 5]
```
However, only one reduction is performed for a sequential match:
```  # MATCH_CONV `(function [] -> 0 | CONS h t -> h + 1) [1;2;3;4]`;;
val it : thm =
|- (function [] -> 0 | CONS h t -> h + 1) [1; 2; 3; 4] =
(function CONS h t -> h + 1) [1; 2; 3; 4]
```
so the conversion may need to be repeated:
```  # TOP_DEPTH_CONV MATCH_CONV
`(function [] -> 0 | CONS h t -> h + 1) [1;2;3;4]`;;
val it : thm = |- (function [] -> 0 | CONS h t -> h + 1) [1; 2; 3; 4] = 1 + 1
```
In cases where the structure of the argument cannot be determined, a conditional expression or other more involved result may be returned:
```  # MATCH_CONV `(function [] -> 0 | CONS h t -> h + 1) l`;;
val it : thm =
|- (function [] -> 0 | CONS h t -> h + 1) l =
(if [] = l then (function [] -> 0) l else (function CONS h t -> h + 1) l)
```

```  # REWRITE_CONV[] `match [1;2;3] with CONS h t when h = 1  -> h + LENGTH t`;;