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