TFL/usyntax.sig
author paulson
Tue, 20 May 1997 11:49:57 +0200
changeset 3245 241838c01caf
parent 2112 3902e9af752f
child 3302 404fe31fd8d2
permissions -rw-r--r--
Removal of redundant code (unused or already present in Isabelle. This eliminates HOL compatibility but makes the code smaller and more readable
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     1
signature USyntax_sig =
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     2
sig
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     3
  structure Utils : Utils_sig
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     4
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     5
  type 'a binding
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     6
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
     7
  datatype lambda = VAR   of {Name : string, Ty : typ}
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
     8
                  | CONST of {Name : string, Ty : typ}
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
     9
                  | COMB  of {Rator: term, Rand : term}
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    10
                  | LAMB  of {Bvar : term, Body : term}
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    11
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    12
  val alpha : typ
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    13
  val mk_preterm : cterm -> term
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    14
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    15
  (* Types *)
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    16
  val type_vars  : typ -> typ list
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    17
  val type_varsl : typ list -> typ list
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    18
  val mk_vartype : string -> typ
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    19
  val is_vartype : typ -> bool
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    20
  val -->        : typ * typ -> typ
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    21
  val strip_type : typ -> typ list * typ
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    22
  val strip_prod_type : typ -> typ list
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    23
  val match_type: typ -> typ -> typ binding list
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    24
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    25
  (* Terms *)
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    26
  val free_vars  : term -> term list
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    27
  val free_varsl : term list -> term list
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    28
  val free_vars_lr : term -> term list
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    29
  val all_vars   : term -> term list
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    30
  val all_varsl  : term list -> term list
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    31
  val variant    : term list -> term -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    32
  val type_vars_in_term : term -> typ list
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    33
  val dest_term  : term -> lambda
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    34
  
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    35
  (* Prelogic *)
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    36
  val aconv     : term -> term -> bool
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    37
  val subst     : term binding list -> term -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    38
  val inst      : typ binding list -> term -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    39
  val beta_conv : term -> term
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    40
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    41
  (* Construction routines *)
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    42
  val mk_var    :{Name : string, Ty : typ} -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    43
  val mk_const  :{Name : string, Ty : typ} -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    44
  val mk_comb   :{Rator : term, Rand : term} -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    45
  val mk_abs    :{Bvar  : term, Body : term} -> term
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    46
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    47
  val mk_imp    :{ant : term, conseq :  term} -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    48
  val mk_select :{Bvar : term, Body : term} -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    49
  val mk_forall :{Bvar : term, Body : term} -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    50
  val mk_exists :{Bvar : term, Body : term} -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    51
  val mk_conj   :{conj1 : term, conj2 : term} -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    52
  val mk_disj   :{disj1 : term, disj2 : term} -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    53
  val mk_pabs   :{varstruct : term, body : term} -> term
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    54
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    55
  (* Destruction routines *)
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    56
  val dest_var  : term -> {Name : string, Ty : typ}
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    57
  val dest_const: term -> {Name : string, Ty : typ}
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    58
  val dest_comb : term -> {Rator : term, Rand : term}
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    59
  val dest_abs  : term -> {Bvar : term, Body : term}
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    60
  val dest_eq     : term -> {lhs : term, rhs : term}
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    61
  val dest_imp    : term -> {ant : term, conseq : term}
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    62
  val dest_select : term -> {Bvar : term, Body : term}
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    63
  val dest_forall : term -> {Bvar : term, Body : term}
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    64
  val dest_exists : term -> {Bvar : term, Body : term}
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    65
  val dest_neg    : term -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    66
  val dest_conj   : term -> {conj1 : term, conj2 : term}
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    67
  val dest_disj   : term -> {disj1 : term, disj2 : term}
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    68
  val dest_pair   : term -> {fst : term, snd : term}
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    69
  val dest_pabs   : term -> {varstruct : term, body : term}
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    70
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    71
  val lhs   : term -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    72
  val rhs   : term -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    73
  val rator : term -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    74
  val rand  : term -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    75
  val bvar  : term -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    76
  val body  : term -> term
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    77
  
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    78
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    79
  (* Query routines *)
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    80
  val is_var  : term -> bool
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    81
  val is_const: term -> bool
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    82
  val is_comb : term -> bool
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    83
  val is_abs  : term -> bool
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    84
  val is_eq     : term -> bool
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    85
  val is_imp    : term -> bool
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    86
  val is_forall : term -> bool 
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    87
  val is_exists : term -> bool 
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    88
  val is_neg    : term -> bool
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    89
  val is_conj   : term -> bool
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    90
  val is_disj   : term -> bool
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    91
  val is_pair   : term -> bool
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    92
  val is_pabs   : term -> bool
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    93
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    94
  (* Construction of a term from a list of Preterms *)
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    95
  val list_mk_abs    : (term list * term) -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    96
  val list_mk_imp    : (term list * term) -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    97
  val list_mk_forall : (term list * term) -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    98
  val list_mk_exists : (term list * term) -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    99
  val list_mk_conj   : term list -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   100
  val list_mk_disj   : term list -> term
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   101
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   102
  (* Destructing a term to a list of Preterms *)
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   103
  val strip_comb     : term -> (term * term list)
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   104
  val strip_abs      : term -> (term list * term)
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   105
  val strip_imp      : term -> (term list * term)
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   106
  val strip_forall   : term -> (term list * term)
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   107
  val strip_exists   : term -> (term list * term)
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   108
  val strip_conj     : term -> term list
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   109
  val strip_disj     : term -> term list
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   110
  val strip_pair     : term -> term list
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   111
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   112
  (* Miscellaneous *)
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   113
  val mk_vstruct : typ -> term list -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   114
  val gen_all    : term -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   115
  val find_term  : (term -> bool) -> term -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   116
  val find_terms : (term -> bool) -> term -> term list
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   117
  val dest_relation : term -> term * term * term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   118
  val is_WFR : term -> bool
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   119
  val ARB : typ -> term
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   120
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   121
  (* Prettyprinting *)
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
   122
  val Term_to_string : cterm -> string
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   123
end;