TFL/usyntax.sig
changeset 3405 2cccd0e3e9ea
parent 3391 5e45dd3b64e9
child 3713 8a1f7d5b1eff
equal deleted inserted replaced
3404:91a91790899a 3405:2cccd0e3e9ea
    23   val mk_vartype : string -> typ
    23   val mk_vartype : string -> typ
    24   val is_vartype : typ -> bool
    24   val is_vartype : typ -> bool
    25   val strip_prod_type : typ -> typ list
    25   val strip_prod_type : typ -> typ list
    26 
    26 
    27   (* Terms *)
    27   (* Terms *)
    28   val free_varsl : term list -> term list
       
    29   val free_vars_lr : term -> term list
    28   val free_vars_lr : term -> term list
    30   val all_vars   : term -> term list
       
    31   val all_varsl  : term list -> term list
       
    32   val variant    : term list -> term -> term
       
    33   val type_vars_in_term : term -> typ list
    29   val type_vars_in_term : term -> typ list
    34   val dest_term  : term -> lambda
    30   val dest_term  : term -> lambda
    35   
    31   
    36   (* Prelogic *)
    32   (* Prelogic *)
    37   val aconv     : term -> term -> bool
       
    38   val inst      : (typ*typ) list -> term -> term
    33   val inst      : (typ*typ) list -> term -> term
    39   val beta_conv : term -> term
       
    40 
    34 
    41   (* Construction routines *)
    35   (* Construction routines *)
    42   val mk_comb   :{Rator : term, Rand : term} -> term
       
    43   val mk_abs    :{Bvar  : term, Body : term} -> term
    36   val mk_abs    :{Bvar  : term, Body : term} -> term
    44 
    37 
    45   val mk_imp    :{ant : term, conseq :  term} -> term
    38   val mk_imp    :{ant : term, conseq :  term} -> term
    46   val mk_select :{Bvar : term, Body : term} -> term
    39   val mk_select :{Bvar : term, Body : term} -> term
    47   val mk_forall :{Bvar : term, Body : term} -> term
    40   val mk_forall :{Bvar : term, Body : term} -> term
    64   val dest_pair   : term -> {fst : term, snd : term}
    57   val dest_pair   : term -> {fst : term, snd : term}
    65   val dest_pabs   : term -> {varstruct : term, body : term}
    58   val dest_pabs   : term -> {varstruct : term, body : term}
    66 
    59 
    67   val lhs   : term -> term
    60   val lhs   : term -> term
    68   val rhs   : term -> term
    61   val rhs   : term -> term
    69   val rator : term -> term
       
    70   val rand  : term -> term
    62   val rand  : term -> term
    71   val bvar  : term -> term
       
    72   val body  : term -> term
       
    73   
       
    74 
    63 
    75   (* Query routines *)
    64   (* Query routines *)
    76   val is_eq     : term -> bool
       
    77   val is_imp    : term -> bool
    65   val is_imp    : term -> bool
    78   val is_forall : term -> bool 
    66   val is_forall : term -> bool 
    79   val is_exists : term -> bool 
    67   val is_exists : term -> bool 
    80   val is_neg    : term -> bool
    68   val is_neg    : term -> bool
    81   val is_conj   : term -> bool
    69   val is_conj   : term -> bool
    85 
    73 
    86   (* Construction of a term from a list of Preterms *)
    74   (* Construction of a term from a list of Preterms *)
    87   val list_mk_abs    : (term list * term) -> term
    75   val list_mk_abs    : (term list * term) -> term
    88   val list_mk_imp    : (term list * term) -> term
    76   val list_mk_imp    : (term list * term) -> term
    89   val list_mk_forall : (term list * term) -> term
    77   val list_mk_forall : (term list * term) -> term
    90   val list_mk_exists : (term list * term) -> term
       
    91   val list_mk_conj   : term list -> term
    78   val list_mk_conj   : term list -> term
    92   val list_mk_disj   : term list -> term
    79   val list_mk_disj   : term list -> term
    93 
    80 
    94   (* Destructing a term to a list of Preterms *)
    81   (* Destructing a term to a list of Preterms *)
    95   val strip_comb     : term -> (term * term list)
    82   val strip_comb     : term -> (term * term list)
   100   val strip_disj     : term -> term list
    87   val strip_disj     : term -> term list
   101 
    88 
   102   (* Miscellaneous *)
    89   (* Miscellaneous *)
   103   val mk_vstruct : typ -> term list -> term
    90   val mk_vstruct : typ -> term list -> term
   104   val gen_all    : term -> term
    91   val gen_all    : term -> term
   105   val find_term  : (term -> bool) -> term -> term
    92   val find_term  : (term -> bool) -> term -> term option
   106   val find_terms : (term -> bool) -> term -> term list
       
   107   val dest_relation : term -> term * term * term
    93   val dest_relation : term -> term * term * term
   108   val is_WFR : term -> bool
    94   val is_WFR : term -> bool
   109   val ARB : typ -> term
    95   val ARB : typ -> term
   110 end;
    96 end;