--- a/src/HOL/Codatatype/Tools/bnf_util.ML Thu Sep 20 17:25:07 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_util.ML Thu Sep 20 17:35:49 2012 +0200
@@ -125,6 +125,10 @@
val mk_trans: thm -> thm -> thm
val mk_unabs_def: int -> thm -> thm
+ val is_refl: thm -> bool
+ val no_refl: thm list -> thm list
+ val no_reflexive: thm list -> thm list
+
val fold_defs: Proof.context -> thm list -> thm -> thm
val unfold_defs: Proof.context -> thm list -> thm -> thm
@@ -592,6 +596,13 @@
fun mk_unabs_def 0 thm = thm
| mk_unabs_def n thm = mk_unabs_def (n - 1) thm RS @{thm spec[OF iffD1[OF fun_eq_iff]]};
+fun is_refl thm =
+ op aconv (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of thm)))
+ handle TERM _ => false;
+
+val no_refl = filter_out is_refl;
+val no_reflexive = filter_out Thm.is_reflexive;
+
fun fold_defs ctxt thms = Local_Defs.fold ctxt (distinct Thm.eq_thm_prop thms);
fun unfold_defs ctxt thms = Local_Defs.unfold ctxt (distinct Thm.eq_thm_prop thms);