src/FOL/fologic.ML
changeset 27325 70e4eb732fa9
parent 11668 548ba68385a3
child 31974 e81979a703a4
equal deleted inserted replaced
27324:904acdaf4299 27325:70e4eb732fa9
    18   val mk_conj		: term * term -> term
    18   val mk_conj		: term * term -> term
    19   val mk_disj		: term * term -> term
    19   val mk_disj		: term * term -> term
    20   val mk_imp		: term * term -> term
    20   val mk_imp		: term * term -> term
    21   val dest_imp	       	: term -> term*term
    21   val dest_imp	       	: term -> term*term
    22   val dest_conj         : term -> term list
    22   val dest_conj         : term -> term list
    23   val dest_concls       : term -> term list
       
    24   val mk_iff		: term * term -> term
    23   val mk_iff		: term * term -> term
    25   val dest_iff	       	: term -> term*term
    24   val dest_iff	       	: term -> term*term
    26   val all_const		: typ -> term
    25   val all_const		: typ -> term
    27   val mk_all		: term * term -> term
    26   val mk_all		: term * term -> term
    28   val exists_const	: typ -> term
    27   val exists_const	: typ -> term
    65   | dest_imp  t = raise TERM ("dest_imp", [t]);
    64   | dest_imp  t = raise TERM ("dest_imp", [t]);
    66 
    65 
    67 fun dest_conj (Const ("op &", _) $ t $ t') = t :: dest_conj t'
    66 fun dest_conj (Const ("op &", _) $ t $ t') = t :: dest_conj t'
    68   | dest_conj t = [t];
    67   | dest_conj t = [t];
    69 
    68 
    70 fun imp_concl_of t = imp_concl_of (#2 (dest_imp t)) handle TERM _ => t;
       
    71 val dest_concls = map imp_concl_of o dest_conj o dest_Trueprop;
       
    72 
       
    73 fun dest_iff (Const("op <->",_) $ A $ B) = (A, B)
    69 fun dest_iff (Const("op <->",_) $ A $ B) = (A, B)
    74   | dest_iff  t = raise TERM ("dest_iff", [t]);
    70   | dest_iff  t = raise TERM ("dest_iff", [t]);
    75 
    71 
    76 fun eq_const T = Const ("op =", [T, T] ---> oT);
    72 fun eq_const T = Const ("op =", [T, T] ---> oT);
    77 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
    73 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;