src/HOL/hologic.ML
changeset 8302 da404f79c1fc
parent 8275 32387a2c7749
child 8429 515fa7533354
equal deleted inserted replaced
8301:d9345bad5e5c 8302:da404f79c1fc
    23   val imp: term
    23   val imp: term
    24   val mk_conj: term * term -> term
    24   val mk_conj: term * term -> term
    25   val mk_disj: term * term -> term
    25   val mk_disj: term * term -> term
    26   val mk_imp: term * term -> term
    26   val mk_imp: term * term -> term
    27   val dest_imp: term -> term * term
    27   val dest_imp: term -> term * term
       
    28   val dest_conj: term -> term list
    28   val eq_const: typ -> term
    29   val eq_const: typ -> term
    29   val all_const: typ -> term
    30   val all_const: typ -> term
    30   val exists_const: typ -> term
    31   val exists_const: typ -> term
    31   val Collect_const: typ -> term
    32   val Collect_const: typ -> term
    32   val mk_eq: term * term -> term
    33   val mk_eq: term * term -> term
   112 and mk_imp (t1, t2) = imp $ t1 $ t2;
   113 and mk_imp (t1, t2) = imp $ t1 $ t2;
   113 
   114 
   114 fun dest_imp (Const("op -->",_) $ A $ B) = (A, B)
   115 fun dest_imp (Const("op -->",_) $ A $ B) = (A, B)
   115   | dest_imp  t = raise TERM ("dest_imp", [t]);
   116   | dest_imp  t = raise TERM ("dest_imp", [t]);
   116 
   117 
       
   118 fun dest_conj (Const ("op &", _) $ t $ t') = t :: dest_conj t'
       
   119   | dest_conj t = [t];
       
   120 
   117 fun eq_const T = Const ("op =", [T, T] ---> boolT);
   121 fun eq_const T = Const ("op =", [T, T] ---> boolT);
   118 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
   122 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
   119 
   123 
   120 fun dest_eq (Const ("op =", _) $ lhs $ rhs) = (lhs, rhs)
   124 fun dest_eq (Const ("op =", _) $ lhs $ rhs) = (lhs, rhs)
   121   | dest_eq t = raise TERM ("dest_eq", [t])
   125   | dest_eq t = raise TERM ("dest_eq", [t])