src/Pure/term.ML
changeset 16589 24c32abc8b84
parent 16570 861b9fa2c98c
child 16599 34f99c3221bb
     1.1 --- a/src/Pure/term.ML	Tue Jun 28 15:28:04 2005 +0200
     1.2 +++ b/src/Pure/term.ML	Tue Jun 28 15:28:30 2005 +0200
     1.3 @@ -43,7 +43,7 @@
     1.4    val is_Const: term -> bool
     1.5    val is_Free: term -> bool
     1.6    val is_Var: term -> bool
     1.7 -  val is_first_order: term -> bool
     1.8 +  val is_first_order: string list -> term -> bool
     1.9    val dest_Type: typ -> string * typ list
    1.10    val dest_TVar: typ -> indexname * sort
    1.11    val dest_TFree: typ -> string * sort
    1.12 @@ -814,21 +814,22 @@
    1.13  fun has_not_funtype Ts t = not (is_funtype (fastype_of1 (Ts,t)));
    1.14  
    1.15  (*First order means in all terms of the form f(t1,...,tn) no argument has a
    1.16 -  function type. The meta-quantifier "all" is excluded--its argument always
    1.17 -  has a function type--through a recursive call into its body.*)
    1.18 -fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body
    1.19 -  | first_order1 Ts (Const("all",_)$Abs(a,T,body)) =
    1.20 -      not (is_funtype T) andalso first_order1 (T::Ts) body
    1.21 -  | first_order1 Ts t =
    1.22 -      case strip_comb t of
    1.23 -               (Var _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
    1.24 -             | (Free _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
    1.25 -             | (Const _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
    1.26 -             | (Bound _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
    1.27 -             | (Abs _, ts) => false (*not in beta-normal form*)
    1.28 -             | _ => error "first_order: unexpected case";
    1.29 -
    1.30 -val is_first_order = first_order1 [];
    1.31 +  function type. The supplied quantifiers are excluded: their argument always
    1.32 +  has a function type through a recursive call into its body.*)
    1.33 +fun is_first_order quants = 
    1.34 +  let fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body
    1.35 +	| first_order1 Ts (Const(q,_) $ Abs(a,T,body)) =
    1.36 +	    q mem_string quants  andalso   (*it is a known quantifier*)
    1.37 +            not (is_funtype T)   andalso first_order1 (T::Ts) body
    1.38 +	| first_order1 Ts t =
    1.39 +	    case strip_comb t of
    1.40 +		 (Var _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
    1.41 +	       | (Free _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
    1.42 +	       | (Const _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
    1.43 +	       | (Bound _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
    1.44 +	       | (Abs _, ts) => false (*not in beta-normal form*)
    1.45 +	       | _ => error "first_order: unexpected case"
    1.46 +    in  first_order1 []  end;
    1.47  
    1.48  (*Computing the maximum index of a typ*)
    1.49  fun maxidx_of_typ(Type(_,Ts)) = maxidx_of_typs Ts