TFL/dcterm.sml

 
 structure Dcterm :
 sig
     val mk_conj : cterm * cterm -> cterm
     val mk_disj : cterm * cterm -> cterm
-    val mk_select : cterm * cterm -> cterm
-    val mk_forall : 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_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_select : 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_forall : cterm -> bool
     val is_imp : cterm -> bool
     val is_let : cterm -> bool
     val is_neg : cterm -> bool
     val is_pair : cterm -> bool
-    val is_select : cterm -> bool
     val list_mk_abs : cterm list -> cterm -> cterm
     val list_mk_exists : cterm list * cterm -> cterm
-    val list_mk_forall : cterm list * cterm -> cterm
     val list_mk_disj : cterm list -> cterm
     val strip_abs : cterm -> cterm list * cterm
     val strip_comb : cterm -> cterm * cterm list
-    val strip_conj : 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 strip_pair : cterm -> cterm list
     val drop_prop : cterm -> cterm
     val mk_prop : cterm -> cterm
   end =
 struct
 

  * Some simple constructor functions.
  *---------------------------------------------------------------------------*)
 
 fun mk_const sign pr = cterm_of sign (Const pr);
 val mk_hol_const = mk_const (sign_of HOL.thy);
-
-fun mk_select (r as (Bvar,Body)) = 
-  let val ty = #T(rep_cterm Bvar)
-      val c = mk_hol_const("Eps", (ty --> HOLogic.boolT) --> ty)
-  in capply c (uncurry cabs r)
-  end;
-
-fun mk_forall (r as (Bvar,Body)) = 
-  let val ty = #T(rep_cterm Bvar)
-      val c = mk_hol_const("All", (ty --> HOLogic.boolT) --> HOLogic.boolT)
-  in capply c (uncurry cabs r)
-  end;
 
 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)

  * Iterated creation.
  *---------------------------------------------------------------------------*)
 val list_mk_abs = itlist cabs;
 
 fun list_mk_exists(V,t) = itlist(fn v => fn b => mk_exists(v, b)) V t;
-fun list_mk_forall(V,t) = itlist(fn v => fn b => mk_forall(v, b)) V t;
 val list_mk_disj = end_itlist(fn d1 => fn tm => mk_disj(d1, tm))
 
 (*---------------------------------------------------------------------------
  * Iterated destruction. (To the "right" in a term.)
  *---------------------------------------------------------------------------*)

 val strip_imp    = rev2swap o strip dest_imp
 val strip_abs    = rev2swap o strip dest_abs
 val strip_forall = rev2swap o strip dest_forall
 val strip_exists = rev2swap o strip dest_exists
 
-val strip_conj   = rev o (op::) o strip dest_conj
 val strip_disj   = rev o (op::) o strip dest_disj
-val strip_pair   = rev o (op::) o strip dest_pair;
 
 
 (*---------------------------------------------------------------------------
  * Going into and out of prop
  *---------------------------------------------------------------------------*)