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)

COMMENTS

The simple cases where the structure completely determines the result are built into the default rewrites, though nothing will happen in more general cases, even if the conditions can be discharged straightforwardly, e.g:

  # REWRITE_CONV[] `match [1;2;3] with CONS h t when h = 1  -> h + LENGTH t`;;
  val it : thm =
    |- (match [1; 2; 3] with CONS h t when h = 1 -> h + LENGTH t) =
       1 + LENGTH [2; 3]
  # REWRITE_CONV[] `match [1;2;3] with CONS h t when h < 7 -> h + LENGTH t`;;
  val it : thm =
    |- (match [1; 2; 3] with CONS h t when h < 7 -> h + LENGTH t) =
       (match [1; 2; 3] with CONS h t when h < 7 -> h + LENGTH t)

SEE ALSO

BETA_CONV, GEN_BETA_CONV.