TFL/dcterm.sml
author wenzelm
Thu, 16 Oct 1997 15:33:06 +0200
changeset 3906 5ae0e1324c56
parent 3405 2cccd0e3e9ea
child 6397 e70ae9b575cc
permissions -rw-r--r--
global;
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/dcterm
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
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     7
(*---------------------------------------------------------------------------
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     8
 * Derived efficient cterm destructors.
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     9
 *---------------------------------------------------------------------------*)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    10
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    11
structure Dcterm :
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    12
sig
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    13
    val mk_conj : cterm * cterm -> cterm
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    14
    val mk_disj : cterm * cterm -> cterm
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    15
    val mk_exists : cterm * cterm -> cterm
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    16
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    17
    val dest_conj : cterm -> cterm * cterm
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    18
    val dest_const : cterm -> {Name:string, Ty:typ}
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    19
    val dest_disj : cterm -> cterm * cterm
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    20
    val dest_eq : cterm -> cterm * cterm
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    21
    val dest_exists : cterm -> cterm * cterm
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    22
    val dest_forall : cterm -> cterm * cterm
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    23
    val dest_imp : cterm -> cterm * cterm
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    24
    val dest_let : cterm -> cterm * cterm
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    25
    val dest_neg : cterm -> cterm
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    26
    val dest_pair : cterm -> cterm * cterm
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    27
    val dest_var : cterm -> {Name:string, Ty:typ}
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    28
    val is_conj : cterm -> bool
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    29
    val is_cons : cterm -> bool
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    30
    val is_disj : cterm -> bool
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    31
    val is_eq : cterm -> bool
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    32
    val is_exists : cterm -> bool
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    33
    val is_forall : cterm -> bool
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    34
    val is_imp : cterm -> bool
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    35
    val is_let : cterm -> bool
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    36
    val is_neg : cterm -> bool
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    37
    val is_pair : cterm -> bool
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    38
    val list_mk_disj : cterm list -> cterm
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    39
    val strip_abs : cterm -> cterm list * cterm
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    40
    val strip_comb : cterm -> cterm * cterm list
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    41
    val strip_disj : cterm -> cterm list
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    42
    val strip_exists : cterm -> cterm list * cterm
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    43
    val strip_forall : cterm -> cterm list * cterm
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    44
    val strip_imp : cterm -> cterm list * cterm
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    45
    val drop_prop : cterm -> cterm
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    46
    val mk_prop : cterm -> cterm
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    47
  end =
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    48
struct
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    49
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    50
fun ERR func mesg = Utils.ERR{module = "Dcterm", func = func, mesg = mesg};
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    51
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    52
(*---------------------------------------------------------------------------
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    53
 * General support routines
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    54
 *---------------------------------------------------------------------------*)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    55
val can = Utils.can;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    56
fun swap (x,y) = (y,x);
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    57
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    58
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    59
(*---------------------------------------------------------------------------
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    60
 * Some simple constructor functions.
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    61
 *---------------------------------------------------------------------------*)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    62
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    63
fun mk_const sign pr = cterm_of sign (Const pr);
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    64
val mk_hol_const = mk_const (sign_of HOL.thy);
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    65
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    66
fun mk_exists (r as (Bvar,Body)) = 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    67
  let val ty = #T(rep_cterm Bvar)
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    68
      val c = mk_hol_const("Ex", (ty --> HOLogic.boolT) --> HOLogic.boolT)
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    69
  in capply c (uncurry cabs r)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    70
  end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    71
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    72
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    73
local val c = mk_hol_const("op &", HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    74
in fun mk_conj(conj1,conj2) = capply (capply c conj1) conj2
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    75
end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    76
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 2112
diff changeset
    77
local val c = mk_hol_const("op |", HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    78
in fun mk_disj(disj1,disj2) = capply (capply c disj1) disj2
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    79
end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    80
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    81
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    82
(*---------------------------------------------------------------------------
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    83
 * The primitives.
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    84
 *---------------------------------------------------------------------------*)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    85
fun dest_const ctm = 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    86
   (case #t(rep_cterm ctm)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    87
      of Const(s,ty) => {Name = s, Ty = ty}
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    88
       | _ => raise ERR "dest_const" "not a constant");
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    89
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    90
fun dest_var ctm = 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    91
   (case #t(rep_cterm ctm)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    92
      of Var((s,i),ty) => {Name=s, Ty=ty}
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    93
       | Free(s,ty)    => {Name=s, Ty=ty}
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    94
       |             _ => raise ERR "dest_var" "not a variable");
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    95
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    96
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    97
(*---------------------------------------------------------------------------
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    98
 * Derived destructor operations. 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    99
 *---------------------------------------------------------------------------*)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   100
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   101
fun dest_monop expected tm = 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   102
 let exception Fail
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   103
     val (c,N) = dest_comb tm
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   104
 in if (#Name(dest_const c) = expected) then N else raise Fail
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   105
 end handle e => raise ERR "dest_monop" ("Not a(n) "^quote expected);
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   106
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   107
fun dest_binop expected tm =
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   108
 let val (M,N) = dest_comb tm
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   109
 in (dest_monop expected M, N)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   110
 end handle e => raise ERR "dest_binop" ("Not a(n) "^quote expected);
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   111
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   112
(* For "if-then-else" 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   113
fun dest_triop expected tm =
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   114
 let val (MN,P) = dest_comb tm
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   115
     val (M,N) = dest_binop expected MN
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   116
 in (M,N,P)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   117
 end handle e => raise ERR "dest_triop" ("Not a(n) "^quote expected);
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   118
*)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   119
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   120
fun dest_binder expected tm = 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   121
  dest_abs(dest_monop expected tm)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   122
  handle e => raise ERR "dest_binder" ("Not a(n) "^quote expected);
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   123
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   124
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   125
val dest_neg    = dest_monop "not"
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   126
val dest_pair   = dest_binop "Pair";
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   127
val dest_eq     = dest_binop "op ="
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   128
val dest_imp    = dest_binop "op -->"
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   129
val dest_conj   = dest_binop "op &"
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   130
val dest_disj   = dest_binop "op |"
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   131
val dest_cons   = dest_binop "op #"
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   132
val dest_let    = swap o dest_binop "Let";
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   133
(* val dest_cond   = dest_triop "if" *)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   134
val dest_select = dest_binder "Eps"
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   135
val dest_exists = dest_binder "Ex"
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   136
val dest_forall = dest_binder "All"
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   137
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   138
(* Query routines *)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   139
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   140
val is_eq     = can dest_eq
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   141
val is_imp    = can dest_imp
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   142
val is_select = can dest_select
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   143
val is_forall = can dest_forall
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   144
val is_exists = can dest_exists
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   145
val is_neg    = can dest_neg
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   146
val is_conj   = can dest_conj
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   147
val is_disj   = can dest_disj
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   148
(* val is_cond   = can dest_cond *)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   149
val is_pair   = can dest_pair
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   150
val is_let    = can dest_let
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   151
val is_cons   = can dest_cons
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   152
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   153
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   154
(*---------------------------------------------------------------------------
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   155
 * Iterated creation.
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   156
 *---------------------------------------------------------------------------*)
3405
2cccd0e3e9ea Numerous simplifications and removal of HOL-isms
paulson
parents: 3391
diff changeset
   157
val list_mk_disj = Utils.end_itlist(fn d1 => fn tm => mk_disj(d1, tm))
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   158
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   159
(*---------------------------------------------------------------------------
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   160
 * Iterated destruction. (To the "right" in a term.)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   161
 *---------------------------------------------------------------------------*)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   162
fun strip break tm = 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   163
  let fun dest (p as (ctm,accum)) = 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   164
        let val (M,N) = break ctm
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   165
        in dest (N, M::accum)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   166
        end handle _ => p
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   167
  in dest (tm,[])
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   168
  end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   169
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   170
fun rev2swap (x,l) = (rev l, x);
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   171
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   172
val strip_comb   = strip (swap o dest_comb)  (* Goes to the "left" *)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   173
val strip_imp    = rev2swap o strip dest_imp
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   174
val strip_abs    = rev2swap o strip dest_abs
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   175
val strip_forall = rev2swap o strip dest_forall
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   176
val strip_exists = rev2swap o strip dest_exists
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   177
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   178
val strip_disj   = rev o (op::) o strip dest_disj
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   179
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   180
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   181
(*---------------------------------------------------------------------------
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   182
 * Going into and out of prop
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   183
 *---------------------------------------------------------------------------*)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   184
local val prop = cterm_of (sign_of HOL.thy) (read"Trueprop")
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   185
in fun mk_prop ctm =
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   186
     case (#t(rep_cterm ctm))
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   187
       of (Const("Trueprop",_)$_) => ctm
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   188
        |  _ => capply prop ctm
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   189
end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   190
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   191
fun drop_prop ctm = dest_monop "Trueprop" ctm handle _ => ctm;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   192
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
   193
end;