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