wenzelm@10769: (*  Title:      TFL/dcterm.ML
wenzelm@10769:     ID:         $Id$
wenzelm@10769:     Author:     Konrad Slind, Cambridge University Computer Laboratory
wenzelm@10769:     Copyright   1997  University of Cambridge
wenzelm@10769: *)
wenzelm@10769: 
wenzelm@10769: (*---------------------------------------------------------------------------
wenzelm@10769:  * Derived efficient cterm destructors.
wenzelm@10769:  *---------------------------------------------------------------------------*)
wenzelm@10769: 
wenzelm@10769: signature DCTERM =
wenzelm@10769: sig
wenzelm@10769:   val dest_comb: cterm -> cterm * cterm
wenzelm@10769:   val dest_abs: string option -> cterm -> cterm * cterm
wenzelm@10769:   val capply: cterm -> cterm -> cterm
wenzelm@10769:   val cabs: cterm -> cterm -> cterm
wenzelm@10769:   val mk_conj: cterm * cterm -> cterm
wenzelm@10769:   val mk_disj: cterm * cterm -> cterm
wenzelm@10769:   val mk_exists: cterm * cterm -> cterm
wenzelm@10769:   val dest_conj: cterm -> cterm * cterm
wenzelm@10769:   val dest_const: cterm -> {Name: string, Ty: typ}
wenzelm@10769:   val dest_disj: cterm -> cterm * cterm
wenzelm@10769:   val dest_eq: cterm -> cterm * cterm
wenzelm@10769:   val dest_exists: cterm -> cterm * cterm
wenzelm@10769:   val dest_forall: cterm -> cterm * cterm
wenzelm@10769:   val dest_imp: cterm -> cterm * cterm
wenzelm@10769:   val dest_let: cterm -> cterm * cterm
wenzelm@10769:   val dest_neg: cterm -> cterm
wenzelm@10769:   val dest_pair: cterm -> cterm * cterm
wenzelm@10769:   val dest_var: cterm -> {Name:string, Ty:typ}
wenzelm@10769:   val is_conj: cterm -> bool
wenzelm@10769:   val is_cons: cterm -> bool
wenzelm@10769:   val is_disj: cterm -> bool
wenzelm@10769:   val is_eq: cterm -> bool
wenzelm@10769:   val is_exists: cterm -> bool
wenzelm@10769:   val is_forall: cterm -> bool
wenzelm@10769:   val is_imp: cterm -> bool
wenzelm@10769:   val is_let: cterm -> bool
wenzelm@10769:   val is_neg: cterm -> bool
wenzelm@10769:   val is_pair: cterm -> bool
wenzelm@10769:   val list_mk_disj: cterm list -> cterm
wenzelm@10769:   val strip_abs: cterm -> cterm list * cterm
wenzelm@10769:   val strip_comb: cterm -> cterm * cterm list
wenzelm@10769:   val strip_disj: cterm -> cterm list
wenzelm@10769:   val strip_exists: cterm -> cterm list * cterm
wenzelm@10769:   val strip_forall: cterm -> cterm list * cterm
wenzelm@10769:   val strip_imp: cterm -> cterm list * cterm
wenzelm@10769:   val drop_prop: cterm -> cterm
wenzelm@10769:   val mk_prop: cterm -> cterm
wenzelm@10769: end;
wenzelm@10769: 
wenzelm@10769: structure Dcterm: DCTERM =
wenzelm@10769: struct
wenzelm@10769: 
wenzelm@10769: structure U = Utils;
wenzelm@10769: 
wenzelm@10769: fun ERR func mesg = U.ERR {module = "Dcterm", func = func, mesg = mesg};
wenzelm@10769: 
wenzelm@10769: 
wenzelm@10769: fun dest_comb t = Thm.dest_comb t
wenzelm@10769:   handle CTERM msg => raise ERR "dest_comb" msg;
wenzelm@10769: 
wenzelm@10769: fun dest_abs a t = Thm.dest_abs a t
wenzelm@10769:   handle CTERM msg => raise ERR "dest_abs" msg;
wenzelm@10769: 
wenzelm@10769: fun capply t u = Thm.capply t u
wenzelm@10769:   handle CTERM msg => raise ERR "capply" msg;
wenzelm@10769: 
wenzelm@10769: fun cabs a t = Thm.cabs a t
wenzelm@10769:   handle CTERM msg => raise ERR "cabs" msg;
wenzelm@10769: 
wenzelm@10769: 
wenzelm@10769: (*---------------------------------------------------------------------------
wenzelm@15674:  * Some simple constructor functions.
wenzelm@10769:  *---------------------------------------------------------------------------*)
wenzelm@10769: 
wenzelm@10769: val mk_hol_const = Thm.cterm_of (Theory.sign_of HOL.thy) o Const;
wenzelm@10769: 
wenzelm@10769: fun mk_exists (r as (Bvar, Body)) =
wenzelm@10769:   let val ty = #T(rep_cterm Bvar)
wenzelm@10769:       val c = mk_hol_const("Ex", (ty --> HOLogic.boolT) --> HOLogic.boolT)
wenzelm@10769:   in capply c (uncurry cabs r) end;
wenzelm@10769: 
wenzelm@10769: 
wenzelm@10769: local val c = mk_hol_const("op &", HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
wenzelm@10769: in fun mk_conj(conj1,conj2) = capply (capply c conj1) conj2
wenzelm@10769: end;
wenzelm@10769: 
wenzelm@10769: local val c = mk_hol_const("op |", HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
wenzelm@10769: in fun mk_disj(disj1,disj2) = capply (capply c disj1) disj2
wenzelm@10769: end;
wenzelm@10769: 
wenzelm@10769: 
wenzelm@10769: (*---------------------------------------------------------------------------
wenzelm@10769:  * The primitives.
wenzelm@10769:  *---------------------------------------------------------------------------*)
wenzelm@10769: fun dest_const ctm =
wenzelm@10769:    (case #t(rep_cterm ctm)
wenzelm@10769:       of Const(s,ty) => {Name = s, Ty = ty}
wenzelm@10769:        | _ => raise ERR "dest_const" "not a constant");
wenzelm@10769: 
wenzelm@10769: fun dest_var ctm =
wenzelm@10769:    (case #t(rep_cterm ctm)
wenzelm@10769:       of Var((s,i),ty) => {Name=s, Ty=ty}
wenzelm@10769:        | Free(s,ty)    => {Name=s, Ty=ty}
wenzelm@10769:        |             _ => raise ERR "dest_var" "not a variable");
wenzelm@10769: 
wenzelm@10769: 
wenzelm@10769: (*---------------------------------------------------------------------------
wenzelm@10769:  * Derived destructor operations.
wenzelm@10769:  *---------------------------------------------------------------------------*)
wenzelm@10769: 
wenzelm@10769: fun dest_monop expected tm =
wenzelm@10769:  let
wenzelm@10769:    fun err () = raise ERR "dest_monop" ("Not a(n) " ^ quote expected);
wenzelm@10769:    val (c, N) = dest_comb tm handle U.ERR _ => err ();
wenzelm@10769:    val name = #Name (dest_const c handle U.ERR _ => err ());
wenzelm@10769:  in if name = expected then N else err () end;
wenzelm@10769: 
wenzelm@10769: fun dest_binop expected tm =
wenzelm@10769:  let
wenzelm@10769:    fun err () = raise ERR "dest_binop" ("Not a(n) " ^ quote expected);
wenzelm@10769:    val (M, N) = dest_comb tm handle U.ERR _ => err ()
wenzelm@10769:  in (dest_monop expected M, N) handle U.ERR _ => err () end;
wenzelm@10769: 
wenzelm@10769: fun dest_binder expected tm =
skalberg@15531:   dest_abs NONE (dest_monop expected tm)
wenzelm@10769:   handle U.ERR _ => raise ERR "dest_binder" ("Not a(n) " ^ quote expected);
wenzelm@10769: 
wenzelm@10769: 
wenzelm@10769: val dest_neg    = dest_monop "not"
wenzelm@10769: val dest_pair   = dest_binop "Pair";
wenzelm@10769: val dest_eq     = dest_binop "op ="
wenzelm@10769: val dest_imp    = dest_binop "op -->"
wenzelm@10769: val dest_conj   = dest_binop "op &"
wenzelm@10769: val dest_disj   = dest_binop "op |"
wenzelm@10769: val dest_cons   = dest_binop "Cons"
wenzelm@10769: val dest_let    = Library.swap o dest_binop "Let";
berghofe@13182: val dest_select = dest_binder "Hilbert_Choice.Eps"
wenzelm@10769: val dest_exists = dest_binder "Ex"
wenzelm@10769: val dest_forall = dest_binder "All"
wenzelm@10769: 
wenzelm@10769: (* Query routines *)
wenzelm@10769: 
wenzelm@10769: val is_eq     = can dest_eq
wenzelm@10769: val is_imp    = can dest_imp
wenzelm@10769: val is_select = can dest_select
wenzelm@10769: val is_forall = can dest_forall
wenzelm@10769: val is_exists = can dest_exists
wenzelm@10769: val is_neg    = can dest_neg
wenzelm@10769: val is_conj   = can dest_conj
wenzelm@10769: val is_disj   = can dest_disj
wenzelm@10769: val is_pair   = can dest_pair
wenzelm@10769: val is_let    = can dest_let
wenzelm@10769: val is_cons   = can dest_cons
wenzelm@10769: 
wenzelm@10769: 
wenzelm@10769: (*---------------------------------------------------------------------------
wenzelm@10769:  * Iterated creation.
wenzelm@10769:  *---------------------------------------------------------------------------*)
wenzelm@10769: val list_mk_disj = U.end_itlist (fn d1 => fn tm => mk_disj (d1, tm));
wenzelm@10769: 
wenzelm@10769: (*---------------------------------------------------------------------------
wenzelm@10769:  * Iterated destruction. (To the "right" in a term.)
wenzelm@10769:  *---------------------------------------------------------------------------*)
wenzelm@10769: fun strip break tm =
wenzelm@10769:   let fun dest (p as (ctm,accum)) =
wenzelm@10769:         let val (M,N) = break ctm
wenzelm@10769:         in dest (N, M::accum)
wenzelm@10769:         end handle U.ERR _ => p
wenzelm@10769:   in dest (tm,[])
wenzelm@10769:   end;
wenzelm@10769: 
wenzelm@10769: fun rev2swap (x,l) = (rev l, x);
wenzelm@10769: 
wenzelm@10769: val strip_comb   = strip (Library.swap o dest_comb)  (* Goes to the "left" *)
wenzelm@10769: val strip_imp    = rev2swap o strip dest_imp
skalberg@15531: val strip_abs    = rev2swap o strip (dest_abs NONE)
wenzelm@10769: val strip_forall = rev2swap o strip dest_forall
wenzelm@10769: val strip_exists = rev2swap o strip dest_exists
wenzelm@10769: 
wenzelm@10769: val strip_disj   = rev o (op::) o strip dest_disj
wenzelm@10769: 
wenzelm@10769: 
wenzelm@10769: (*---------------------------------------------------------------------------
wenzelm@10769:  * Going into and out of prop
wenzelm@10769:  *---------------------------------------------------------------------------*)
wenzelm@10769: 
wenzelm@10769: fun mk_prop ctm =
wenzelm@10769:   let val {t, sign, ...} = Thm.rep_cterm ctm in
wenzelm@10769:     if can HOLogic.dest_Trueprop t then ctm
wenzelm@10769:     else Thm.cterm_of sign (HOLogic.mk_Trueprop t)
wenzelm@10769:   end
wenzelm@10769:   handle TYPE (msg, _, _) => raise ERR "mk_prop" msg
wenzelm@10769:     | TERM (msg, _) => raise ERR "mk_prop" msg;
wenzelm@10769: 
wenzelm@10769: fun drop_prop ctm = dest_monop "Trueprop" ctm handle U.ERR _ => ctm;
wenzelm@10769: 
wenzelm@10769: 
wenzelm@10769: end;