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