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