eliminate duplicated constant (diag vs. Id_on)

--- a/src/HOL/BNF/BNF_GFP.thy	Mon Mar 18 11:05:33 2013 +0100
+++ b/src/HOL/BNF/BNF_GFP.thy	Mon Mar 18 11:25:24 2013 +0100
@@ -44,35 +44,29 @@
 qed
 
 (* Operators: *)
-definition diag where "diag A \<equiv> {(a,a) | a. a \<in> A}"
 definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}"
 
-lemma diagI: "x \<in> A \<Longrightarrow> (x, x) \<in> diag A"
-unfolding diag_def by simp
 
-lemma diagE: "(a, b) \<in> diag A \<Longrightarrow> a = b"
-unfolding diag_def by simp
+lemma Id_onD: "(a, b) \<in> Id_on A \<Longrightarrow> a = b"
+unfolding Id_on_def by simp
 
-lemma diagE': "x \<in> diag A \<Longrightarrow> fst x = snd x"
-unfolding diag_def by auto
+lemma Id_onD': "x \<in> Id_on A \<Longrightarrow> fst x = snd x"
+unfolding Id_on_def by auto
 
-lemma diag_fst: "x \<in> diag A \<Longrightarrow> fst x \<in> A"
-unfolding diag_def by auto
+lemma Id_on_fst: "x \<in> Id_on A \<Longrightarrow> fst x \<in> A"
+unfolding Id_on_def by auto
 
-lemma diag_UNIV: "diag UNIV = Id"
-unfolding diag_def by auto
+lemma Id_on_UNIV: "Id_on UNIV = Id"
+unfolding Id_on_def by auto
 
-lemma diag_converse: "diag A = (diag A) ^-1"
-unfolding diag_def by auto
+lemma Id_on_Comp: "Id_on A = Id_on A O Id_on A"
+unfolding Id_on_def by auto
 
-lemma diag_Comp: "diag A = diag A O diag A"
-unfolding diag_def by auto
+lemma Id_on_Gr: "Id_on A = Gr A id"
+unfolding Id_on_def Gr_def by auto
 
-lemma diag_Gr: "diag A = Gr A id"
-unfolding diag_def Gr_def by simp
-
-lemma diag_UNIV_I: "x = y \<Longrightarrow> (x, y) \<in> diag UNIV"
-unfolding diag_def by auto
+lemma Id_on_UNIV_I: "x = y \<Longrightarrow> (x, y) \<in> Id_on UNIV"
+unfolding Id_on_def by auto
 
 lemma image2_eqI: "\<lbrakk>b = f x; c = g x; x \<in> A\<rbrakk> \<Longrightarrow> (b, c) \<in> image2 A f g"
 unfolding image2_def by auto
@@ -122,9 +116,9 @@
 "R1 \<subseteq> R2 \<Longrightarrow> relInvImage A R1 f \<subseteq> relInvImage A R2 f"
 unfolding relInvImage_def by auto
 
-lemma relInvImage_diag:
-"(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (diag B) f \<subseteq> Id"
-unfolding relInvImage_def diag_def by auto
+lemma relInvImage_Id_on:
+"(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (Id_on B) f \<subseteq> Id"
+unfolding relInvImage_def Id_on_def by auto
 
 lemma relInvImage_UNIV_relImage:
 "R \<subseteq> relInvImage UNIV (relImage R f) f"
@@ -135,10 +129,10 @@
 
 lemma relImage_proj:
 assumes "equiv A R"
-shows "relImage R (proj R) \<subseteq> diag (A//R)"
-unfolding relImage_def diag_def apply safe
-using proj_iff[OF assms]
-by (metis assms equiv_Image proj_def proj_preserves)
+shows "relImage R (proj R) \<subseteq> Id_on (A//R)"
+unfolding relImage_def Id_on_def
+using proj_iff[OF assms] equiv_class_eq_iff[OF assms]
+by (auto simp: proj_preserves)
 
 lemma relImage_relInvImage:
 assumes "R \<subseteq> f ` A <*> f ` A"

--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Mon Mar 18 11:05:33 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Mon Mar 18 11:25:24 2013 +0100
@@ -198,7 +198,7 @@
       ||>> mk_Freess "K" (map (fn AT => map (fn T => T --> AT) activeAs) ATs);
 
     val passive_UNIVs = map HOLogic.mk_UNIV passiveAs;
-    val passive_diags = map mk_diag As;
+    val passive_Id_ons = map mk_Id_on As;
     val active_UNIVs = map HOLogic.mk_UNIV activeAs;
     val sum_UNIVs = map HOLogic.mk_UNIV sumBsAs;
     val passive_ids = map HOLogic.id_const passiveAs;
@@ -854,7 +854,7 @@
           list_all_free [b1, b2] (HOLogic.mk_imp
             (HOLogic.mk_mem (HOLogic.mk_prod (b1, b2), R),
             HOLogic.mk_mem (HOLogic.mk_prod (s $ b1, s' $ b2),
-              Term.list_comb (srel, passive_diags @ Rs))));
+              Term.list_comb (srel, passive_Id_ons @ Rs))));
 
         val rhs = HOLogic.mk_conj
           (bis_le, Library.foldr1 HOLogic.mk_conj
@@ -907,8 +907,8 @@
       ((bis_O_thm OF [bis_Gr_thm RS bis_converse_thm, bis_Gr_thm]) ::
       replicate n @{thm image2_Gr});
 
-    val bis_diag_thm = bis_cong_thm OF ((mor_id_thm RSN (2, bis_Gr_thm)) ::
-      replicate n @{thm diag_Gr});
+    val bis_Id_on_thm = bis_cong_thm OF ((mor_id_thm RSN (2, bis_Gr_thm)) ::
+      replicate n @{thm Id_on_Gr});
 
     val bis_Union_thm =
       let
@@ -1004,7 +1004,7 @@
         map3 (fn goal => fn l_incl => fn incl_l =>
           Skip_Proof.prove lthy [] [] goal
             (K (mk_equiv_lsbis_tac sbis_lsbis_thm l_incl incl_l
-              bis_diag_thm bis_converse_thm bis_O_thm))
+              bis_Id_on_thm bis_converse_thm bis_O_thm))
           |> Thm.close_derivation)
         goals lsbis_incl_thms incl_lsbis_thms
       end;
@@ -2187,7 +2187,7 @@
         val zs = Jzs1 @ Jzs2;
         val frees = phis @ zs;
 
-        fun mk_Ids Id = if Id then map Id_const passiveAs else map mk_diag passive_UNIVs;
+        fun mk_Ids Id = if Id then map Id_const passiveAs else map mk_Id_on passive_UNIVs;
 
         fun mk_phi strong_eq phi z1 z2 = if strong_eq
           then Term.absfree (dest_Free z1) (Term.absfree (dest_Free z2)
@@ -2220,7 +2220,7 @@
           fold_rev Logic.all frees (Logic.list_implies (srel_prems, concl));
         val coinduct_params = rev (Term.add_tfrees dtor_srel_coinduct_goal []);
 
-        val dtor_srel_coinduct = unfold_thms lthy @{thms diag_UNIV}
+        val dtor_srel_coinduct = unfold_thms lthy @{thms Id_on_UNIV}
           (Skip_Proof.prove lthy [] [] dtor_srel_coinduct_goal
             (K (mk_dtor_srel_coinduct_tac ks raw_coind_thm bis_srel_thm))
           |> Thm.close_derivation);
@@ -2270,7 +2270,7 @@
           (Skip_Proof.prove lthy [] []
             (fold_rev Logic.all zs (Logic.list_implies (strong_prems, concl)))
             (K (mk_dtor_map_strong_coinduct_tac ks cTs cts dtor_map_coinduct bis_def
-              (tcoalg_thm RS bis_diag_thm))))
+              (tcoalg_thm RS bis_Id_on_thm))))
           |> Thm.close_derivation;
 
         val rel_of_srel_thms =

--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Mon Mar 18 11:05:33 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Mon Mar 18 11:25:24 2013 +0100
@@ -270,7 +270,7 @@
             CONJ_WRAP' (fn (i, thm) =>
               if i <= m
               then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans,
-                etac @{thm image_mono}, rtac @{thm image_subsetI}, etac @{thm diagI}]
+                etac @{thm image_mono}, rtac @{thm image_subsetI}, etac @{thm Id_onI}]
               else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
                 rtac trans_fun_cong_image_id_id_apply, atac])
             (1 upto (m + n) ~~ set_naturals),
@@ -295,13 +295,13 @@
         REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
         REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
         rtac trans, rtac map_cong,
-        REPEAT_DETERM_N m o EVERY' [rtac @{thm diagE'}, etac set_mp, atac],
+        REPEAT_DETERM_N m o EVERY' [rtac @{thm Id_onD'}, etac set_mp, atac],
         REPEAT_DETERM_N n o rtac refl,
         etac sym, rtac CollectI,
         CONJ_WRAP' (fn (i, thm) =>
           if i <= m
           then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI},
-            rtac @{thm diag_fst}, etac set_mp, atac]
+            rtac @{thm Id_on_fst}, etac set_mp, atac]
           else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
             rtac trans_fun_cong_image_id_id_apply, atac])
         (1 upto (m + n) ~~ set_naturals)];
@@ -319,7 +319,7 @@
     CONJ_WRAP' (fn (srel_cong, srel_converse) =>
       EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm set_mp[OF equalityD2]},
         rtac (srel_cong RS trans),
-        REPEAT_DETERM_N m o rtac @{thm diag_converse},
+        REPEAT_DETERM_N m o rtac (@{thm converse_Id_on} RS sym),
         REPEAT_DETERM_N (length srel_congs) o rtac refl,
         rtac srel_converse,
         REPEAT_DETERM o etac allE,
@@ -332,7 +332,7 @@
     CONJ_WRAP' (fn (srel_cong, srel_O) =>
       EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm set_mp[OF equalityD2]},
         rtac (srel_cong RS trans),
-        REPEAT_DETERM_N m o rtac @{thm diag_Comp},
+        REPEAT_DETERM_N m o rtac @{thm Id_on_Comp},
         REPEAT_DETERM_N (length srel_congs) o rtac refl,
         rtac srel_O,
         etac @{thm relcompE},
@@ -343,7 +343,7 @@
 
 fun mk_bis_Gr_tac bis_srel srel_Grs mor_images morEs coalg_ins
   {context = ctxt, prems = _} =
-  unfold_thms_tac ctxt (bis_srel :: @{thm diag_Gr} :: srel_Grs) THEN
+  unfold_thms_tac ctxt (bis_srel :: @{thm Id_on_Gr} :: srel_Grs) THEN
   EVERY' [rtac conjI,
     CONJ_WRAP' (fn thm => rtac (@{thm Gr_incl} RS ssubst) THEN' etac thm) mor_images,
     CONJ_WRAP' (fn (coalg_in, morE) =>
@@ -383,12 +383,12 @@
     REPEAT_DETERM_N n o rtac exI, rtac conjI, rtac refl, atac, rtac equalityD2,
     rtac (mk_nth_conv n i)] 1;
 
-fun mk_equiv_lsbis_tac sbis_lsbis lsbis_incl incl_lsbis bis_diag bis_converse bis_O =
+fun mk_equiv_lsbis_tac sbis_lsbis lsbis_incl incl_lsbis bis_Id_on bis_converse bis_O =
   EVERY' [rtac (@{thm equiv_def} RS iffD2),
 
     rtac conjI, rtac (@{thm refl_on_def} RS iffD2),
     rtac conjI, rtac lsbis_incl, rtac ballI, rtac set_mp,
-    rtac incl_lsbis, rtac bis_diag, atac, etac @{thm diagI},
+    rtac incl_lsbis, rtac bis_Id_on, atac, etac @{thm Id_onI},
 
     rtac conjI, rtac (@{thm sym_def} RS iffD2),
     rtac allI, rtac allI, rtac impI, rtac set_mp,
@@ -1090,7 +1090,7 @@
           rtac @{thm xt1(3)}, rtac @{thm Sigma_cong},
           rtac @{thm proj_image}, rtac @{thm proj_image}, rtac lsbis_incl,
           rtac subset_trans, rtac @{thm relImage_mono}, rtac incl_lsbis, atac,
-          rtac @{thm relImage_proj}, rtac equiv_LSBIS, rtac @{thm relInvImage_diag},
+          rtac @{thm relImage_proj}, rtac equiv_LSBIS, rtac @{thm relInvImage_Id_on},
           rtac Rep_inject])
       (Rep_injects ~~ (equiv_LSBISs ~~ (incl_lsbiss ~~ lsbis_incls)))] 1
   end;
@@ -1163,16 +1163,16 @@
         rtac CollectI, etac (refl RSN (2, @{thm subst_Pair}))]) ks] 1
   end;
 
-fun mk_dtor_map_strong_coinduct_tac ks cTs cts dtor_map_coinduct bis_def bis_diag =
+fun mk_dtor_map_strong_coinduct_tac ks cTs cts dtor_map_coinduct bis_def bis_Id_on =
   EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts dtor_map_coinduct),
     EVERY' (map (fn i =>
       EVERY' [etac disjE, REPEAT_DETERM o dtac @{thm meta_spec}, etac meta_mp,
-        atac, rtac rev_mp, rtac subst, rtac bis_def, rtac bis_diag,
+        atac, rtac rev_mp, rtac subst, rtac bis_def, rtac bis_Id_on,
         rtac impI, dtac conjunct2, dtac (mk_conjunctN (length ks) i), REPEAT_DETERM o etac allE,
-        etac impE, etac @{thm diag_UNIV_I}, REPEAT_DETERM o eresolve_tac [bexE, conjE, CollectE],
+        etac impE, etac @{thm Id_on_UNIV_I}, REPEAT_DETERM o eresolve_tac [bexE, conjE, CollectE],
         rtac exI, rtac conjI, etac conjI, atac,
         CONJ_WRAP' (K (EVERY' [REPEAT_DETERM o resolve_tac [allI, impI],
-          rtac disjI2, rtac @{thm diagE}, etac set_mp, atac])) ks])
+          rtac disjI2, rtac @{thm Id_onD}, etac set_mp, atac])) ks])
     ks),
     rtac impI, REPEAT_DETERM o etac conjE,
     CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) ks] 1;

--- a/src/HOL/BNF/Tools/bnf_gfp_util.ML	Mon Mar 18 11:05:33 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_util.ML	Mon Mar 18 11:25:24 2013 +0100
@@ -18,7 +18,7 @@
   val mk_append: term * term -> term
   val mk_congruent: term -> term -> term
   val mk_clists: term -> term
-  val mk_diag: term -> term
+  val mk_Id_on: term -> term
   val mk_equiv: term -> term -> term
   val mk_fromCard: term -> term -> term
   val mk_list_rec: term -> term -> term
@@ -59,11 +59,11 @@
     val ABT = mk_relT (HOLogic.dest_setT AT, HOLogic.dest_setT (range_type BT));
   in Const (@{const_name Sigma}, AT --> BT --> ABT) $ A $ B end;
 
-fun mk_diag A =
+fun mk_Id_on A =
   let
     val AT = fastype_of A;
     val AAT = mk_relT (HOLogic.dest_setT AT, HOLogic.dest_setT AT);
-  in Const (@{const_name diag}, AT --> AAT) $ A end;
+  in Const (@{const_name Id_on}, AT --> AAT) $ A end;
 
 fun mk_Times (A, B) =
   let val AT = HOLogic.dest_setT (fastype_of A);