TFL/usyntax.sig
author paulson
Mon, 23 Jun 1997 11:30:35 +0200
changeset 3458 5ff4bfab859c
parent 3405 2cccd0e3e9ea
child 3713 8a1f7d5b1eff
permissions -rw-r--r--
Removal of COND_CONG, which is just if_cong RS eq_reflection
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3302
404fe31fd8d2 New headers and other minor changes
paulson
parents: 3245
diff changeset
     1
(*  Title:      TFL/usyntax
404fe31fd8d2 New headers and other minor changes
paulson
parents: 3245
diff changeset
     2
    ID:         $Id$
404fe31fd8d2 New headers and other minor changes
paulson
parents: 3245
diff changeset
     3
    Author:     Konrad Slind, Cambridge University Computer Laboratory
404fe31fd8d2 New headers and other minor changes
paulson
parents: 3245
diff changeset
     4
    Copyright   1997  University of Cambridge
404fe31fd8d2 New headers and other minor changes
paulson
parents: 3245
diff changeset
     5
404fe31fd8d2 New headers and other minor changes
paulson
parents: 3245
diff changeset
     6
Emulation of HOL's abstract syntax functions
404fe31fd8d2 New headers and other minor changes
paulson
parents: 3245
diff changeset
     7
*)
404fe31fd8d2 New headers and other minor changes
paulson
parents: 3245
diff changeset
     8
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     9
signature USyntax_sig =
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    10
sig
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    11
  structure Utils : Utils_sig
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    12
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    13
  datatype lambda = VAR   of {Name : string, Ty : typ}
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    14
                  | CONST of {Name : string, Ty : typ}
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    15
                  | COMB  of {Rator: term, Rand : term}
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    16
                  | LAMB  of {Bvar : term, Body : term}
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    17
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    18
  val alpha : typ
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    19
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    20
  (* Types *)
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    21
  val type_vars  : typ -> typ list
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    22
  val type_varsl : typ list -> typ list
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    23
  val mk_vartype : string -> typ
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    24
  val is_vartype : typ -> bool
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    25
  val strip_prod_type : typ -> typ list
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    26
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    27
  (* Terms *)
3245
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 type_vars_in_term : term -> typ list
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    30
  val dest_term  : term -> lambda
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    31
  
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    32
  (* Prelogic *)
3353
9112a2efb9a3 Removal of module Mask and datatype binding with its constructor |->
paulson
parents: 3330
diff changeset
    33
  val inst      : (typ*typ) list -> term -> term
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    34
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    35
  (* Construction routines *)
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    36
  val mk_abs    :{Bvar  : term, Body : term} -> term
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    37
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    38
  val mk_imp    :{ant : term, conseq :  term} -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    39
  val mk_select :{Bvar : term, Body : term} -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    40
  val mk_forall :{Bvar : term, Body : term} -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    41
  val mk_exists :{Bvar : term, Body : term} -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    42
  val mk_conj   :{conj1 : term, conj2 : term} -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    43
  val mk_disj   :{disj1 : term, disj2 : term} -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    44
  val mk_pabs   :{varstruct : term, body : term} -> term
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    45
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    46
  (* Destruction routines *)
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    47
  val dest_const: term -> {Name : string, Ty : typ}
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    48
  val dest_comb : term -> {Rator : term, Rand : term}
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    49
  val dest_abs  : term -> {Bvar : term, Body : term}
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    50
  val dest_eq     : term -> {lhs : term, rhs : term}
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    51
  val dest_imp    : term -> {ant : term, conseq : term}
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    52
  val dest_forall : term -> {Bvar : term, Body : term}
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    53
  val dest_exists : term -> {Bvar : term, Body : term}
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    54
  val dest_neg    : term -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    55
  val dest_conj   : term -> {conj1 : term, conj2 : term}
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    56
  val dest_disj   : term -> {disj1 : term, disj2 : term}
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    57
  val dest_pair   : term -> {fst : term, snd : term}
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    58
  val dest_pabs   : term -> {varstruct : term, body : term}
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    59
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    60
  val lhs   : term -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    61
  val rhs   : term -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    62
  val rand  : term -> term
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    63
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    64
  (* Query routines *)
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    65
  val is_imp    : term -> bool
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    66
  val is_forall : term -> bool 
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    67
  val is_exists : term -> bool 
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    68
  val is_neg    : term -> bool
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    69
  val is_conj   : term -> bool
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    70
  val is_disj   : term -> bool
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    71
  val is_pair   : term -> bool
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    72
  val is_pabs   : term -> bool
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    73
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    74
  (* 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
    75
  val list_mk_abs    : (term list * term) -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    76
  val list_mk_imp    : (term list * term) -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    77
  val list_mk_forall : (term list * term) -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    78
  val list_mk_conj   : term list -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    79
  val list_mk_disj   : term list -> term
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    80
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    81
  (* Destructing a term to a list of Preterms *)
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    82
  val strip_comb     : term -> (term * term list)
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    83
  val strip_abs      : term -> (term list * term)
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    84
  val strip_imp      : term -> (term list * term)
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    85
  val strip_forall   : term -> (term list * term)
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    86
  val strip_exists   : term -> (term list * term)
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    87
  val strip_disj     : term -> term list
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    88
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    89
  (* Miscellaneous *)
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    90
  val mk_vstruct : typ -> term list -> term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    91
  val gen_all    : term -> term
3405
2cccd0e3e9ea Numerous simplifications and removal of HOL-isms
paulson
parents: 3391
diff changeset
    92
  val find_term  : (term -> bool) -> term -> term option
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    93
  val dest_relation : term -> term * term * term
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    94
  val is_WFR : term -> bool
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    95
  val ARB : typ -> term
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    96
end;