37 

    38 text {* \solution{fun:killqnt} *}

    39 

    40 ML %linenosgray{*val quantifiers = [@{const_name All}, @{const_name Ex}]

    41 

    42 fun kill_trivial_quantifiers trm =

    43 let

    44   fun aux t =

    45     case t of

    46       Const (s1, T1) $ Abs (x, T2, t2) =>

    47         if member (op =) quantifiers s1 andalso not (loose_bvar1 (t2, 0)) 

    48         then incr_boundvars ~1 (aux t2)

    49         else Const (s1, T1) $ Abs (x, T2, aux t2)

    50     | t1 $ t2 => aux t1 $ aux t2

    51     | Abs (s, T, t') => Abs (s, T, aux t')

    52     | _ => t

    53 in 

    54   aux trm

    55 end*}

    56 

    57 text {*

    58   In line 7 we traverse the term, by first checking whether a term is an

    59   application of a constant with an abstraction. If the constant stands for

    60   a listed quantifier (see Line 1) and the bound variable does not occur

    61   as a loose bound variable in the body, then we delete the quantifier. 

    62   For this we have to increase all other dangling de Bruijn indices by

    63   @{text "-1"} to account for the deleted quantifier. An example is 

    64   as follows:

    65 

    66   @{ML_response_fake [display,gray]

    67   "@{prop \"\<forall>x y z. P x = P z\"}

    68   |> kill_trivial_quantifiers

    69   |> pretty_term @{context} 

    70   |> pwriteln"

    71   "\<forall>x z. P x = P z"}

    72 *}

    73