src/HOL/Tools/TFL/dcterm.ML
author wenzelm
Fri Mar 06 15:58:56 2015 +0100 (2015-03-06)
changeset 59621 291934bac95e
parent 59586 ddf6deaadfe8
child 59640 a6d29266f01c
permissions -rw-r--r--
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm@23150
     1
(*  Title:      HOL/Tools/TFL/dcterm.ML
wenzelm@23150
     2
    Author:     Konrad Slind, Cambridge University Computer Laboratory
wenzelm@23150
     3
*)
wenzelm@23150
     4
wenzelm@23150
     5
(*---------------------------------------------------------------------------
wenzelm@23150
     6
 * Derived efficient cterm destructors.
wenzelm@23150
     7
 *---------------------------------------------------------------------------*)
wenzelm@23150
     8
wenzelm@23150
     9
signature DCTERM =
wenzelm@23150
    10
sig
wenzelm@23150
    11
  val dest_comb: cterm -> cterm * cterm
wenzelm@23150
    12
  val dest_abs: string option -> cterm -> cterm * cterm
wenzelm@23150
    13
  val capply: cterm -> cterm -> cterm
wenzelm@23150
    14
  val cabs: cterm -> cterm -> cterm
wenzelm@23150
    15
  val mk_conj: cterm * cterm -> cterm
wenzelm@23150
    16
  val mk_disj: cterm * cterm -> cterm
wenzelm@23150
    17
  val mk_exists: cterm * cterm -> cterm
wenzelm@23150
    18
  val dest_conj: cterm -> cterm * cterm
wenzelm@23150
    19
  val dest_const: cterm -> {Name: string, Ty: typ}
wenzelm@23150
    20
  val dest_disj: cterm -> cterm * cterm
wenzelm@23150
    21
  val dest_eq: cterm -> cterm * cterm
wenzelm@23150
    22
  val dest_exists: cterm -> cterm * cterm
wenzelm@23150
    23
  val dest_forall: cterm -> cterm * cterm
wenzelm@23150
    24
  val dest_imp: cterm -> cterm * cterm
wenzelm@23150
    25
  val dest_neg: cterm -> cterm
wenzelm@23150
    26
  val dest_pair: cterm -> cterm * cterm
wenzelm@23150
    27
  val dest_var: cterm -> {Name:string, Ty:typ}
wenzelm@23150
    28
  val is_conj: cterm -> bool
wenzelm@23150
    29
  val is_disj: cterm -> bool
wenzelm@23150
    30
  val is_eq: cterm -> bool
wenzelm@23150
    31
  val is_exists: cterm -> bool
wenzelm@23150
    32
  val is_forall: cterm -> bool
wenzelm@23150
    33
  val is_imp: cterm -> bool
wenzelm@23150
    34
  val is_neg: cterm -> bool
wenzelm@23150
    35
  val is_pair: cterm -> bool
wenzelm@23150
    36
  val list_mk_disj: cterm list -> cterm
wenzelm@23150
    37
  val strip_abs: cterm -> cterm list * cterm
wenzelm@23150
    38
  val strip_comb: cterm -> cterm * cterm list
wenzelm@23150
    39
  val strip_disj: cterm -> cterm list
wenzelm@23150
    40
  val strip_exists: cterm -> cterm list * cterm
wenzelm@23150
    41
  val strip_forall: cterm -> cterm list * cterm
wenzelm@23150
    42
  val strip_imp: cterm -> cterm list * cterm
wenzelm@23150
    43
  val drop_prop: cterm -> cterm
wenzelm@23150
    44
  val mk_prop: cterm -> cterm
wenzelm@23150
    45
end;
wenzelm@23150
    46
wenzelm@23150
    47
structure Dcterm: DCTERM =
wenzelm@23150
    48
struct
wenzelm@23150
    49
wenzelm@41164
    50
fun ERR func mesg = Utils.ERR {module = "Dcterm", func = func, mesg = mesg};
wenzelm@23150
    51
wenzelm@23150
    52
wenzelm@23150
    53
fun dest_comb t = Thm.dest_comb t
wenzelm@23150
    54
  handle CTERM (msg, _) => raise ERR "dest_comb" msg;
wenzelm@23150
    55
wenzelm@23150
    56
fun dest_abs a t = Thm.dest_abs a t
wenzelm@23150
    57
  handle CTERM (msg, _) => raise ERR "dest_abs" msg;
wenzelm@23150
    58
wenzelm@46497
    59
fun capply t u = Thm.apply t u
wenzelm@23150
    60
  handle CTERM (msg, _) => raise ERR "capply" msg;
wenzelm@23150
    61
wenzelm@46497
    62
fun cabs a t = Thm.lambda a t
wenzelm@23150
    63
  handle CTERM (msg, _) => raise ERR "cabs" msg;
wenzelm@23150
    64
wenzelm@23150
    65
wenzelm@23150
    66
(*---------------------------------------------------------------------------
wenzelm@23150
    67
 * Some simple constructor functions.
wenzelm@23150
    68
 *---------------------------------------------------------------------------*)
wenzelm@23150
    69
wenzelm@59621
    70
val mk_hol_const = Thm.global_cterm_of @{theory HOL} o Const;
wenzelm@23150
    71
wenzelm@23150
    72
fun mk_exists (r as (Bvar, Body)) =
wenzelm@59586
    73
  let val ty = Thm.typ_of_cterm Bvar
haftmann@38554
    74
      val c = mk_hol_const(@{const_name Ex}, (ty --> HOLogic.boolT) --> HOLogic.boolT)
wenzelm@23150
    75
  in capply c (uncurry cabs r) end;
wenzelm@23150
    76
wenzelm@23150
    77
haftmann@38795
    78
local val c = mk_hol_const(@{const_name HOL.conj}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
wenzelm@23150
    79
in fun mk_conj(conj1,conj2) = capply (capply c conj1) conj2
wenzelm@23150
    80
end;
wenzelm@23150
    81
haftmann@38795
    82
local val c = mk_hol_const(@{const_name HOL.disj}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
wenzelm@23150
    83
in fun mk_disj(disj1,disj2) = capply (capply c disj1) disj2
wenzelm@23150
    84
end;
wenzelm@23150
    85
wenzelm@23150
    86
wenzelm@23150
    87
(*---------------------------------------------------------------------------
wenzelm@23150
    88
 * The primitives.
wenzelm@23150
    89
 *---------------------------------------------------------------------------*)
wenzelm@23150
    90
fun dest_const ctm =
wenzelm@59586
    91
   (case Thm.term_of ctm
wenzelm@23150
    92
      of Const(s,ty) => {Name = s, Ty = ty}
wenzelm@23150
    93
       | _ => raise ERR "dest_const" "not a constant");
wenzelm@23150
    94
wenzelm@23150
    95
fun dest_var ctm =
wenzelm@59586
    96
   (case Thm.term_of ctm
wenzelm@23150
    97
      of Var((s,i),ty) => {Name=s, Ty=ty}
wenzelm@23150
    98
       | Free(s,ty)    => {Name=s, Ty=ty}
wenzelm@23150
    99
       |             _ => raise ERR "dest_var" "not a variable");
wenzelm@23150
   100
wenzelm@23150
   101
wenzelm@23150
   102
(*---------------------------------------------------------------------------
wenzelm@23150
   103
 * Derived destructor operations.
wenzelm@23150
   104
 *---------------------------------------------------------------------------*)
wenzelm@23150
   105
wenzelm@23150
   106
fun dest_monop expected tm =
wenzelm@23150
   107
 let
wenzelm@23150
   108
   fun err () = raise ERR "dest_monop" ("Not a(n) " ^ quote expected);
wenzelm@41164
   109
   val (c, N) = dest_comb tm handle Utils.ERR _ => err ();
wenzelm@41164
   110
   val name = #Name (dest_const c handle Utils.ERR _ => err ());
wenzelm@23150
   111
 in if name = expected then N else err () end;
wenzelm@23150
   112
wenzelm@23150
   113
fun dest_binop expected tm =
wenzelm@23150
   114
 let
wenzelm@23150
   115
   fun err () = raise ERR "dest_binop" ("Not a(n) " ^ quote expected);
wenzelm@41164
   116
   val (M, N) = dest_comb tm handle Utils.ERR _ => err ()
wenzelm@41164
   117
 in (dest_monop expected M, N) handle Utils.ERR _ => err () end;
wenzelm@23150
   118
wenzelm@23150
   119
fun dest_binder expected tm =
wenzelm@23150
   120
  dest_abs NONE (dest_monop expected tm)
wenzelm@41164
   121
  handle Utils.ERR _ => raise ERR "dest_binder" ("Not a(n) " ^ quote expected);
wenzelm@23150
   122
wenzelm@23150
   123
haftmann@38554
   124
val dest_neg    = dest_monop @{const_name Not}
haftmann@38554
   125
val dest_pair   = dest_binop @{const_name Pair}
haftmann@38864
   126
val dest_eq     = dest_binop @{const_name HOL.eq}
haftmann@38786
   127
val dest_imp    = dest_binop @{const_name HOL.implies}
haftmann@38795
   128
val dest_conj   = dest_binop @{const_name HOL.conj}
haftmann@38795
   129
val dest_disj   = dest_binop @{const_name HOL.disj}
haftmann@38554
   130
val dest_select = dest_binder @{const_name Eps}
haftmann@38554
   131
val dest_exists = dest_binder @{const_name Ex}
haftmann@38554
   132
val dest_forall = dest_binder @{const_name All}
wenzelm@23150
   133
wenzelm@23150
   134
(* Query routines *)
wenzelm@23150
   135
wenzelm@23150
   136
val is_eq     = can dest_eq
wenzelm@23150
   137
val is_imp    = can dest_imp
wenzelm@23150
   138
val is_select = can dest_select
wenzelm@23150
   139
val is_forall = can dest_forall
wenzelm@23150
   140
val is_exists = can dest_exists
wenzelm@23150
   141
val is_neg    = can dest_neg
wenzelm@23150
   142
val is_conj   = can dest_conj
wenzelm@23150
   143
val is_disj   = can dest_disj
wenzelm@23150
   144
val is_pair   = can dest_pair
wenzelm@23150
   145
wenzelm@23150
   146
wenzelm@23150
   147
(*---------------------------------------------------------------------------
wenzelm@23150
   148
 * Iterated creation.
wenzelm@23150
   149
 *---------------------------------------------------------------------------*)
wenzelm@41164
   150
val list_mk_disj = Utils.end_itlist (fn d1 => fn tm => mk_disj (d1, tm));
wenzelm@23150
   151
wenzelm@23150
   152
(*---------------------------------------------------------------------------
wenzelm@23150
   153
 * Iterated destruction. (To the "right" in a term.)
wenzelm@23150
   154
 *---------------------------------------------------------------------------*)
wenzelm@23150
   155
fun strip break tm =
wenzelm@23150
   156
  let fun dest (p as (ctm,accum)) =
wenzelm@23150
   157
        let val (M,N) = break ctm
wenzelm@23150
   158
        in dest (N, M::accum)
wenzelm@41164
   159
        end handle Utils.ERR _ => p
wenzelm@23150
   160
  in dest (tm,[])
wenzelm@23150
   161
  end;
wenzelm@23150
   162
wenzelm@23150
   163
fun rev2swap (x,l) = (rev l, x);
wenzelm@23150
   164
wenzelm@23150
   165
val strip_comb   = strip (Library.swap o dest_comb)  (* Goes to the "left" *)
wenzelm@23150
   166
val strip_imp    = rev2swap o strip dest_imp
wenzelm@23150
   167
val strip_abs    = rev2swap o strip (dest_abs NONE)
wenzelm@23150
   168
val strip_forall = rev2swap o strip dest_forall
wenzelm@23150
   169
val strip_exists = rev2swap o strip dest_exists
wenzelm@23150
   170
wenzelm@23150
   171
val strip_disj   = rev o (op::) o strip dest_disj
wenzelm@23150
   172
wenzelm@23150
   173
wenzelm@23150
   174
(*---------------------------------------------------------------------------
wenzelm@23150
   175
 * Going into and out of prop
wenzelm@23150
   176
 *---------------------------------------------------------------------------*)
wenzelm@23150
   177
wenzelm@23150
   178
fun mk_prop ctm =
wenzelm@26626
   179
  let
wenzelm@26626
   180
    val thy = Thm.theory_of_cterm ctm;
wenzelm@26626
   181
    val t = Thm.term_of ctm;
wenzelm@26626
   182
  in
wenzelm@23150
   183
    if can HOLogic.dest_Trueprop t then ctm
wenzelm@59621
   184
    else Thm.global_cterm_of thy (HOLogic.mk_Trueprop t)
wenzelm@23150
   185
  end
wenzelm@23150
   186
  handle TYPE (msg, _, _) => raise ERR "mk_prop" msg
wenzelm@23150
   187
    | TERM (msg, _) => raise ERR "mk_prop" msg;
wenzelm@23150
   188
wenzelm@41164
   189
fun drop_prop ctm = dest_monop @{const_name Trueprop} ctm handle Utils.ERR _ => ctm;
wenzelm@23150
   190
wenzelm@23150
   191
wenzelm@23150
   192
end;