700 (** Identifying first-order terms **) |
700 (** Identifying first-order terms **) |
701 |
701 |
702 (*Argument Ts is a reverse list of binder types, needed if term t contains Bound vars*) |
702 (*Argument Ts is a reverse list of binder types, needed if term t contains Bound vars*) |
703 fun has_not_funtype Ts t = not (is_funtype (fastype_of1 (Ts,t))); |
703 fun has_not_funtype Ts t = not (is_funtype (fastype_of1 (Ts,t))); |
704 |
704 |
705 (*First order means in all terms of the form f(t1,...,tn) no argument has a function |
705 (*First order means in all terms of the form f(t1,...,tn) no argument has a |
706 type. The meta-quantifier "all" is excluded--its argument always has a function |
706 function type. The meta-quantifier "all" is excluded--its argument always |
707 type--through a recursive call into its body.*) |
707 has a function type--through a recursive call into its body.*) |
708 fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body |
708 fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body |
709 | first_order1 Ts (Const("all",_)$Abs(a,T,body)) = |
709 | first_order1 Ts (Const("all",_)$Abs(a,T,body)) = |
710 not (is_funtype T) andalso first_order1 (T::Ts) body |
710 not (is_funtype T) andalso first_order1 (T::Ts) body |
711 | first_order1 Ts t = |
711 | first_order1 Ts t = |
712 case strip_comb t of |
712 case strip_comb t of |