Type.match

STRUCTURE

SYNOPSIS

Match types with restrictions.

DESCRIPTION

An invocation match_typel away pat ty matches pat to ty in the same way as match_type, but prohibits any of the type variables in away from being instantiated. In effect, the elements of away, although type variables, are treated as constants in pat during the matching process.

FAILURE

An invocation of match_typel away pat ty will fail if match_type pat ty would fail. It will also fail if match_type pat ty would succeed giving a substitution [{redex_1,residue_1},...,{redex_n,residue_n}] where one or more of the redex_i are members of away.

EXAMPLE

In the first example, we perform a normal match operation

   - match_typel [] (alpha --> beta --> gamma)
                    (bool --> ind --> delta);
   > val it = [{redex = `:'c`, residue = `:'d`}, 
               {redex = `:'b`, residue = `:ind`},
               {redex = `:'a`, residue = `:bool`}] : ...

Now we require that gamma, although a type variable in the pattern, not be instantiable. In the first try, the match succeeds because 'c is mapped only to itself. In the second, it fails because an association is made between 'c and 'd.

   - match_typel [gamma] (alpha --> beta --> gamma)
                         (bool --> ind --> gamma);
   > val it = [{redex = `:'b`, residue = `:ind`},
               {redex = `:'a`, residue = `:bool`}] : ...

   - match_typel [gamma] (alpha --> beta --> gamma)
                         (bool --> ind --> delta);
   ! Uncaught exception: 
   ! HOL_ERR

COMMENTS

The use of away allows matching to take account of type variables that are ’frozen’ (by occurring in the hypotheses of a theorem, for example). This allows certain fruitless proof attempts to be avoided at the matching stage.

SEEALSO

match_type, match_term, ho_match_term, type_subst