--- a/src/HOL/Tools/BNF/bnf_util.ML Wed Apr 23 10:23:26 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML Wed Apr 23 10:23:26 2014 +0200
@@ -101,6 +101,7 @@
val mk_rel_fun: term -> term -> term
val mk_image: term -> term
val mk_in: term list -> term list -> typ -> term
+ val mk_inj: term -> term
val mk_leq: term -> term -> term
val mk_ordLeq: term -> term -> term
val mk_rel_comp: term * term -> term
@@ -470,6 +471,12 @@
else HOLogic.mk_UNIV T
end;
+fun mk_inj t =
+ let val T as Type (@{type_name fun}, [domT, ranT]) = fastype_of t in
+ Const (@{const_name inj_on}, T --> HOLogic.mk_setT domT --> HOLogic.boolT) $ t
+ $ HOLogic.mk_UNIV domT
+ end;
+
fun mk_leq t1 t2 =
Const (@{const_name less_eq}, (fastype_of t1) --> (fastype_of t2) --> HOLogic.boolT) $ t1 $ t2;