# HG changeset patch
# User blanchet
# Date 1348736350 -7200
# Node ID ea566f5e1724c6bfefb95ad10211795fdb161c94
# Parent  c54d901d29467dab9337b761137f8c980131d0a7
avoid another brand of trivial "disc_rel" theorems (which made the simplifier loop for all single-constructor types)

diff -r c54d901d2946 -r ea566f5e1724 src/HOL/BNF/Tools/bnf_fp_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_sugar.ML	Thu Sep 27 10:43:40 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_sugar.ML	Thu Sep 27 10:59:10 2012 +0200
@@ -116,10 +116,6 @@
 fun merge_type_args (As, As') =
   if length As = length As' then map2 merge_type_arg As As' else cannot_merge_types ();
 
-fun is_triv_implies thm =
-  op aconv (Logic.dest_implies (Thm.prop_of thm))
-  handle TERM _ => false;
-
 fun reassoc_conjs thm =
   reassoc_conjs (thm RS @{thm conj_assoc[THEN iffD1]})
   handle THM _ => thm;
@@ -1027,8 +1023,10 @@
              map2 proves corec_goalss corec_tacss)
           end;
 
+        val is_triv_discI = is_triv_implies orf is_concl_refl;
+
         fun mk_disc_corec_like_thms corec_likes discIs =
-          map (op RS) (filter_out (is_triv_implies o snd) (corec_likes ~~ discIs));
+          map (op RS) (filter_out (is_triv_discI o snd) (corec_likes ~~ discIs));
 
         val disc_unfold_thmss = map2 mk_disc_corec_like_thms unfold_thmss discIss;
         val disc_corec_thmss = map2 mk_disc_corec_like_thms corec_thmss discIss;
diff -r c54d901d2946 -r ea566f5e1724 src/HOL/BNF/Tools/bnf_util.ML
--- a/src/HOL/BNF/Tools/bnf_util.ML	Thu Sep 27 10:43:40 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML	Thu Sep 27 10:59:10 2012 +0200
@@ -135,7 +135,9 @@
   val mk_trans: thm -> thm -> thm
   val mk_unabs_def: int -> thm -> thm
 
+  val is_triv_implies: thm -> bool
   val is_refl: thm -> bool
+  val is_concl_refl: thm -> bool
   val no_refl: thm list -> thm list
   val no_reflexive: thm list -> thm list
 
@@ -616,10 +618,17 @@
 
 fun mk_unabs_def n = funpow n (fn thm => thm RS fun_cong);
 
-fun is_refl thm =
-  op aconv (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of thm)))
+fun is_triv_implies thm =
+  op aconv (Logic.dest_implies (Thm.prop_of thm))
   handle TERM _ => false;
 
+fun is_refl_prop t =
+  op aconv (HOLogic.dest_eq (HOLogic.dest_Trueprop t))
+  handle TERM _ => false;
+
+val is_refl = is_refl_prop o Thm.prop_of;
+val is_concl_refl = is_refl_prop o Logic.strip_imp_concl o Thm.prop_of;
+
 val no_refl = filter_out is_refl;
 val no_reflexive = filter_out Thm.is_reflexive;