move special BNFs used for composition only to BNF_Comp;
use local copy of identity function that gets unfolded later for ID

--- a/src/HOL/BNF_Comp.thy	Thu Mar 06 13:36:50 2014 +0100
+++ b/src/HOL/BNF_Comp.thy	Thu Mar 06 14:14:54 2014 +0100
@@ -42,6 +42,17 @@
 apply (rule Card_order_cprod)
 done
 
+lemma csum_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p +c p' =o r +c r \<Longrightarrow> p +c p' =o r"
+apply (erule ordIso_transitive)
+apply (frule csum_absorb2')
+apply (erule ordLeq_refl)
+by simp
+
+lemma cprod_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p *c p' =o r *c r \<Longrightarrow> p *c p' =o r"
+apply (erule ordIso_transitive)
+apply (rule cprod_infinite)
+by simp
+
 lemma Union_image_insert: "\<Union>(f ` insert a B) = f a \<union> \<Union>(f ` B)"
 by simp
 
@@ -128,22 +139,28 @@
 
 end
 
-definition id_bnf_comp :: "'a \<Rightarrow> 'a" where "id_bnf_comp = (\<lambda>x. x)"
+bnf DEADID: 'a
+  map: "id :: 'a \<Rightarrow> 'a"
+  bd: natLeq
+  rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
+by (auto simp add: Grp_def natLeq_card_order natLeq_cinfinite)
+
+definition id_bnf_comp :: "'a \<Rightarrow> 'a" where "id_bnf_comp \<equiv> (\<lambda>x. x)"
+
+bnf ID: 'a
+  map: "id_bnf_comp :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+  sets: "\<lambda>x. {x}"
+  bd: natLeq
+  rel: "id_bnf_comp :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
+unfolding id_bnf_comp_def
+apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite)
+apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
+apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3]
+done
 
 lemma type_definition_id_bnf_comp_UNIV: "type_definition id_bnf_comp id_bnf_comp UNIV"
   unfolding id_bnf_comp_def by unfold_locales auto
 
-lemma csum_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p +c p' =o r +c r \<Longrightarrow> p +c p' =o r"
-apply (erule ordIso_transitive)
-apply (frule csum_absorb2')
-apply (erule ordLeq_refl)
-by simp
-
-lemma cprod_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p *c p' =o r *c r \<Longrightarrow> p *c p' =o r"
-apply (erule ordIso_transitive)
-apply (rule cprod_infinite)
-by simp
-
 ML_file "Tools/BNF/bnf_comp_tactics.ML"
 ML_file "Tools/BNF/bnf_comp.ML"
 

--- a/src/HOL/Basic_BNFs.thy	Thu Mar 06 13:36:50 2014 +0100
+++ b/src/HOL/Basic_BNFs.thy	Thu Mar 06 14:14:54 2014 +0100
@@ -13,22 +13,6 @@
 imports BNF_Def
 begin
 
-bnf ID: 'a
-  map: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
-  sets: "\<lambda>x. {x}"
-  bd: natLeq
-  rel: "id :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
-apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite)
-apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
-apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3]
-done
-
-bnf DEADID: 'a
-  map: "id :: 'a \<Rightarrow> 'a"
-  bd: natLeq
-  rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
-by (auto simp add: Grp_def natLeq_card_order natLeq_cinfinite)
-
 definition setl :: "'a + 'b \<Rightarrow> 'a set" where
 "setl x = (case x of Inl z => {z} | _ => {})"
 

--- a/src/HOL/Tools/BNF/bnf_comp.ML	Thu Mar 06 13:36:50 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Thu Mar 06 14:14:54 2014 +0100
@@ -56,8 +56,8 @@
 open BNF_Tactics
 open BNF_Comp_Tactics
 
-val ID_bnf = the (bnf_of @{context} "Basic_BNFs.ID");
-val DEADID_bnf = the (bnf_of @{context} "Basic_BNFs.DEADID");
+val ID_bnf = the (bnf_of @{context} "BNF_Comp.ID");
+val DEADID_bnf = the (bnf_of @{context} "BNF_Comp.DEADID");
 
 type comp_cache = (bnf * (typ list * typ list)) Typtab.table;
 
@@ -109,6 +109,8 @@
 fun mk_permuteN src dest =
   "_permute_" ^ implode (map string_of_int src) ^ "_" ^ implode (map string_of_int dest);
 
+val id_bnf_comp_def = @{thm id_bnf_comp_def}
+
 (*copied from Envir.expand_term_free*)
 fun expand_term_const defs =
   let
@@ -339,9 +341,9 @@
         Binding.empty [] ((((((b, CCA), mapx), sets'), bd'), wits), SOME rel) lthy;
 
     val phi =
-      Morphism.thm_morphism "BNF" (unfold_thms lthy' @{thms id_bnf_comp_def})
+      Morphism.thm_morphism "BNF" (unfold_thms lthy' [id_bnf_comp_def])
       $> Morphism.term_morphism "BNF" (Raw_Simplifier.rewrite_term (Proof_Context.theory_of lthy')
-        @{thms id_bnf_comp_def[abs_def]} []);
+        [id_bnf_comp_def] []);
 
     val bnf'' = morph_bnf phi bnf';
   in
@@ -761,19 +763,21 @@
       |> mk_Frees' "f" (map2 (curry op -->) As Bs)
       ||>> mk_Frees' "R" (map2 mk_pred2T As Bs)
 
+    val expand_id_bnf_comp_def =
+      expand_term_const [Thm.prop_of id_bnf_comp_def |> Logic.dest_equals]
     val map_unfolds = #map_unfolds unfold_set;
     val set_unfoldss = #set_unfoldss unfold_set;
     val rel_unfolds = #rel_unfolds unfold_set;
 
-    val expand_maps =
+    val expand_maps = expand_id_bnf_comp_def o
       fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) map_unfolds);
     val expand_sets =
       fold expand_term_const (map (map (Logic.dest_equals o Thm.prop_of)) set_unfoldss);
-    val expand_rels =
+    val expand_rels = expand_id_bnf_comp_def o
       fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) rel_unfolds);
-    fun unfold_maps ctxt = fold (unfold_thms ctxt o single) map_unfolds;
+    fun unfold_maps ctxt = fold (unfold_thms ctxt o single) (id_bnf_comp_def :: map_unfolds);
     fun unfold_sets ctxt = fold (unfold_thms ctxt) set_unfoldss;
-    fun unfold_rels ctxt = unfold_thms ctxt rel_unfolds;
+    fun unfold_rels ctxt = fold (unfold_thms ctxt o single) (id_bnf_comp_def :: rel_unfolds);
     fun unfold_all ctxt = unfold_sets ctxt o unfold_maps ctxt o unfold_rels ctxt;
 
     val repTA = mk_T_of_bnf Ds As bnf;
@@ -854,7 +858,7 @@
 
     val bnf_wits = map (fn (I, t) =>
         fold Term.absdummy (map (nth As) I)
-          (AbsA $ Term.list_comb (t, map Bound (0 upto length I - 1))))
+          (AbsA $ Term.list_comb (expand_id_bnf_comp_def t, map Bound (0 upto length I - 1))))
       (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
 
     fun wit_tac ctxt = ALLGOALS (dtac (type_definition RS @{thm type_copy_wit})) THEN