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