merged

--- a/src/HOL/BNF/Examples/TreeFI.thy	Thu Sep 27 12:07:50 2012 +0200
+++ b/src/HOL/BNF/Examples/TreeFI.thy	Thu Sep 27 12:08:38 2012 +0200
@@ -14,36 +14,27 @@
 
 hide_const (open) Sublist.sub
 
-codata_raw treeFI: 'tree = "'a \<times> 'tree listF"
+codata 'a treeFI = Tree (lab: 'a) (sub: "'a treeFI listF")
 
 lemma pre_treeFI_listF_set[simp]: "pre_treeFI_set2 (i, xs) = listF_set xs"
 unfolding pre_treeFI_set2_def collect_def[abs_def] prod_set_defs
 by (auto simp add: listF.set_natural')
 
-(* selectors for trees *)
-definition "lab tr \<equiv> fst (treeFI_dtor tr)"
-definition "sub tr \<equiv> snd (treeFI_dtor tr)"
-
 lemma dtor[simp]: "treeFI_dtor tr = (lab tr, sub tr)"
-unfolding lab_def sub_def by simp
+unfolding lab_def sub_def treeFI_case_def
+by (metis fst_def pair_collapse snd_def)
 
 definition pair_fun (infixr "\<odot>" 50) where
   "f \<odot> g \<equiv> \<lambda>x. (f x, g x)"
 
-lemma unfold_pair_fun_lab: "lab (treeFI_dtor_unfold (f \<odot> g) t) = f t"
-unfolding lab_def pair_fun_def treeFI.dtor_unfold pre_treeFI_map_def by simp
-
-lemma unfold_pair_fun_sub: "sub (treeFI_dtor_unfold (f \<odot> g) t) = listF_map (treeFI_dtor_unfold (f \<odot> g)) (g t)"
-unfolding sub_def pair_fun_def treeFI.dtor_unfold pre_treeFI_map_def by simp
-
 (* Tree reverse:*)
-definition "trev \<equiv> treeFI_dtor_unfold (lab \<odot> lrev o sub)"
+definition "trev \<equiv> treeFI_unfold lab (lrev o sub)"
 
 lemma trev_simps1[simp]: "lab (trev t) = lab t"
-unfolding trev_def by (simp add: unfold_pair_fun_lab)
+unfolding trev_def by simp
 
 lemma trev_simps2[simp]: "sub (trev t) = listF_map trev (lrev (sub t))"
-unfolding trev_def by (simp add: unfold_pair_fun_sub)
+unfolding trev_def by simp
 
 lemma treeFI_coinduct:
 assumes *: "phi x y"

--- a/src/HOL/BNF/Tools/bnf_fp_sugar.ML	Thu Sep 27 12:07:50 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_sugar.ML	Thu Sep 27 12:08:38 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;

--- a/src/HOL/BNF/Tools/bnf_util.ML	Thu Sep 27 12:07:50 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML	Thu Sep 27 12:08:38 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;