eliminate duplicated constant (diag vs. Id_on)
authortraytel
Mon Mar 18 11:25:24 2013 +0100 (2013-03-18)
changeset 51447a19e973fa2cf
parent 51446 a6ebb12cc003
child 51448 b041137f7fe5
eliminate duplicated constant (diag vs. Id_on)
src/HOL/BNF/BNF_GFP.thy
src/HOL/BNF/Tools/bnf_gfp.ML
src/HOL/BNF/Tools/bnf_gfp_tactics.ML
src/HOL/BNF/Tools/bnf_gfp_util.ML
     1.1 --- a/src/HOL/BNF/BNF_GFP.thy	Mon Mar 18 11:05:33 2013 +0100
     1.2 +++ b/src/HOL/BNF/BNF_GFP.thy	Mon Mar 18 11:25:24 2013 +0100
     1.3 @@ -44,35 +44,29 @@
     1.4  qed
     1.5  
     1.6  (* Operators: *)
     1.7 -definition diag where "diag A \<equiv> {(a,a) | a. a \<in> A}"
     1.8  definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}"
     1.9  
    1.10 -lemma diagI: "x \<in> A \<Longrightarrow> (x, x) \<in> diag A"
    1.11 -unfolding diag_def by simp
    1.12  
    1.13 -lemma diagE: "(a, b) \<in> diag A \<Longrightarrow> a = b"
    1.14 -unfolding diag_def by simp
    1.15 +lemma Id_onD: "(a, b) \<in> Id_on A \<Longrightarrow> a = b"
    1.16 +unfolding Id_on_def by simp
    1.17  
    1.18 -lemma diagE': "x \<in> diag A \<Longrightarrow> fst x = snd x"
    1.19 -unfolding diag_def by auto
    1.20 +lemma Id_onD': "x \<in> Id_on A \<Longrightarrow> fst x = snd x"
    1.21 +unfolding Id_on_def by auto
    1.22  
    1.23 -lemma diag_fst: "x \<in> diag A \<Longrightarrow> fst x \<in> A"
    1.24 -unfolding diag_def by auto
    1.25 +lemma Id_on_fst: "x \<in> Id_on A \<Longrightarrow> fst x \<in> A"
    1.26 +unfolding Id_on_def by auto
    1.27  
    1.28 -lemma diag_UNIV: "diag UNIV = Id"
    1.29 -unfolding diag_def by auto
    1.30 +lemma Id_on_UNIV: "Id_on UNIV = Id"
    1.31 +unfolding Id_on_def by auto
    1.32  
    1.33 -lemma diag_converse: "diag A = (diag A) ^-1"
    1.34 -unfolding diag_def by auto
    1.35 +lemma Id_on_Comp: "Id_on A = Id_on A O Id_on A"
    1.36 +unfolding Id_on_def by auto
    1.37  
    1.38 -lemma diag_Comp: "diag A = diag A O diag A"
    1.39 -unfolding diag_def by auto
    1.40 +lemma Id_on_Gr: "Id_on A = Gr A id"
    1.41 +unfolding Id_on_def Gr_def by auto
    1.42  
    1.43 -lemma diag_Gr: "diag A = Gr A id"
    1.44 -unfolding diag_def Gr_def by simp
    1.45 -
    1.46 -lemma diag_UNIV_I: "x = y \<Longrightarrow> (x, y) \<in> diag UNIV"
    1.47 -unfolding diag_def by auto
    1.48 +lemma Id_on_UNIV_I: "x = y \<Longrightarrow> (x, y) \<in> Id_on UNIV"
    1.49 +unfolding Id_on_def by auto
    1.50  
    1.51  lemma image2_eqI: "\<lbrakk>b = f x; c = g x; x \<in> A\<rbrakk> \<Longrightarrow> (b, c) \<in> image2 A f g"
    1.52  unfolding image2_def by auto
    1.53 @@ -122,9 +116,9 @@
    1.54  "R1 \<subseteq> R2 \<Longrightarrow> relInvImage A R1 f \<subseteq> relInvImage A R2 f"
    1.55  unfolding relInvImage_def by auto
    1.56  
    1.57 -lemma relInvImage_diag:
    1.58 -"(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (diag B) f \<subseteq> Id"
    1.59 -unfolding relInvImage_def diag_def by auto
    1.60 +lemma relInvImage_Id_on:
    1.61 +"(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (Id_on B) f \<subseteq> Id"
    1.62 +unfolding relInvImage_def Id_on_def by auto
    1.63  
    1.64  lemma relInvImage_UNIV_relImage:
    1.65  "R \<subseteq> relInvImage UNIV (relImage R f) f"
    1.66 @@ -135,10 +129,10 @@
    1.67  
    1.68  lemma relImage_proj:
    1.69  assumes "equiv A R"
    1.70 -shows "relImage R (proj R) \<subseteq> diag (A//R)"
    1.71 -unfolding relImage_def diag_def apply safe
    1.72 -using proj_iff[OF assms]
    1.73 -by (metis assms equiv_Image proj_def proj_preserves)
    1.74 +shows "relImage R (proj R) \<subseteq> Id_on (A//R)"
    1.75 +unfolding relImage_def Id_on_def
    1.76 +using proj_iff[OF assms] equiv_class_eq_iff[OF assms]
    1.77 +by (auto simp: proj_preserves)
    1.78  
    1.79  lemma relImage_relInvImage:
    1.80  assumes "R \<subseteq> f ` A <*> f ` A"
     2.1 --- a/src/HOL/BNF/Tools/bnf_gfp.ML	Mon Mar 18 11:05:33 2013 +0100
     2.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Mon Mar 18 11:25:24 2013 +0100
     2.3 @@ -198,7 +198,7 @@
     2.4        ||>> mk_Freess "K" (map (fn AT => map (fn T => T --> AT) activeAs) ATs);
     2.5  
     2.6      val passive_UNIVs = map HOLogic.mk_UNIV passiveAs;
     2.7 -    val passive_diags = map mk_diag As;
     2.8 +    val passive_Id_ons = map mk_Id_on As;
     2.9      val active_UNIVs = map HOLogic.mk_UNIV activeAs;
    2.10      val sum_UNIVs = map HOLogic.mk_UNIV sumBsAs;
    2.11      val passive_ids = map HOLogic.id_const passiveAs;
    2.12 @@ -854,7 +854,7 @@
    2.13            list_all_free [b1, b2] (HOLogic.mk_imp
    2.14              (HOLogic.mk_mem (HOLogic.mk_prod (b1, b2), R),
    2.15              HOLogic.mk_mem (HOLogic.mk_prod (s $ b1, s' $ b2),
    2.16 -              Term.list_comb (srel, passive_diags @ Rs))));
    2.17 +              Term.list_comb (srel, passive_Id_ons @ Rs))));
    2.18  
    2.19          val rhs = HOLogic.mk_conj
    2.20            (bis_le, Library.foldr1 HOLogic.mk_conj
    2.21 @@ -907,8 +907,8 @@
    2.22        ((bis_O_thm OF [bis_Gr_thm RS bis_converse_thm, bis_Gr_thm]) ::
    2.23        replicate n @{thm image2_Gr});
    2.24  
    2.25 -    val bis_diag_thm = bis_cong_thm OF ((mor_id_thm RSN (2, bis_Gr_thm)) ::
    2.26 -      replicate n @{thm diag_Gr});
    2.27 +    val bis_Id_on_thm = bis_cong_thm OF ((mor_id_thm RSN (2, bis_Gr_thm)) ::
    2.28 +      replicate n @{thm Id_on_Gr});
    2.29  
    2.30      val bis_Union_thm =
    2.31        let
    2.32 @@ -1004,7 +1004,7 @@
    2.33          map3 (fn goal => fn l_incl => fn incl_l =>
    2.34            Skip_Proof.prove lthy [] [] goal
    2.35              (K (mk_equiv_lsbis_tac sbis_lsbis_thm l_incl incl_l
    2.36 -              bis_diag_thm bis_converse_thm bis_O_thm))
    2.37 +              bis_Id_on_thm bis_converse_thm bis_O_thm))
    2.38            |> Thm.close_derivation)
    2.39          goals lsbis_incl_thms incl_lsbis_thms
    2.40        end;
    2.41 @@ -2187,7 +2187,7 @@
    2.42          val zs = Jzs1 @ Jzs2;
    2.43          val frees = phis @ zs;
    2.44  
    2.45 -        fun mk_Ids Id = if Id then map Id_const passiveAs else map mk_diag passive_UNIVs;
    2.46 +        fun mk_Ids Id = if Id then map Id_const passiveAs else map mk_Id_on passive_UNIVs;
    2.47  
    2.48          fun mk_phi strong_eq phi z1 z2 = if strong_eq
    2.49            then Term.absfree (dest_Free z1) (Term.absfree (dest_Free z2)
    2.50 @@ -2220,7 +2220,7 @@
    2.51            fold_rev Logic.all frees (Logic.list_implies (srel_prems, concl));
    2.52          val coinduct_params = rev (Term.add_tfrees dtor_srel_coinduct_goal []);
    2.53  
    2.54 -        val dtor_srel_coinduct = unfold_thms lthy @{thms diag_UNIV}
    2.55 +        val dtor_srel_coinduct = unfold_thms lthy @{thms Id_on_UNIV}
    2.56            (Skip_Proof.prove lthy [] [] dtor_srel_coinduct_goal
    2.57              (K (mk_dtor_srel_coinduct_tac ks raw_coind_thm bis_srel_thm))
    2.58            |> Thm.close_derivation);
    2.59 @@ -2270,7 +2270,7 @@
    2.60            (Skip_Proof.prove lthy [] []
    2.61              (fold_rev Logic.all zs (Logic.list_implies (strong_prems, concl)))
    2.62              (K (mk_dtor_map_strong_coinduct_tac ks cTs cts dtor_map_coinduct bis_def
    2.63 -              (tcoalg_thm RS bis_diag_thm))))
    2.64 +              (tcoalg_thm RS bis_Id_on_thm))))
    2.65            |> Thm.close_derivation;
    2.66  
    2.67          val rel_of_srel_thms =
     3.1 --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Mon Mar 18 11:05:33 2013 +0100
     3.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Mon Mar 18 11:25:24 2013 +0100
     3.3 @@ -270,7 +270,7 @@
     3.4              CONJ_WRAP' (fn (i, thm) =>
     3.5                if i <= m
     3.6                then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans,
     3.7 -                etac @{thm image_mono}, rtac @{thm image_subsetI}, etac @{thm diagI}]
     3.8 +                etac @{thm image_mono}, rtac @{thm image_subsetI}, etac @{thm Id_onI}]
     3.9                else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
    3.10                  rtac trans_fun_cong_image_id_id_apply, atac])
    3.11              (1 upto (m + n) ~~ set_naturals),
    3.12 @@ -295,13 +295,13 @@
    3.13          REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
    3.14          REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
    3.15          rtac trans, rtac map_cong,
    3.16 -        REPEAT_DETERM_N m o EVERY' [rtac @{thm diagE'}, etac set_mp, atac],
    3.17 +        REPEAT_DETERM_N m o EVERY' [rtac @{thm Id_onD'}, etac set_mp, atac],
    3.18          REPEAT_DETERM_N n o rtac refl,
    3.19          etac sym, rtac CollectI,
    3.20          CONJ_WRAP' (fn (i, thm) =>
    3.21            if i <= m
    3.22            then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI},
    3.23 -            rtac @{thm diag_fst}, etac set_mp, atac]
    3.24 +            rtac @{thm Id_on_fst}, etac set_mp, atac]
    3.25            else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
    3.26              rtac trans_fun_cong_image_id_id_apply, atac])
    3.27          (1 upto (m + n) ~~ set_naturals)];
    3.28 @@ -319,7 +319,7 @@
    3.29      CONJ_WRAP' (fn (srel_cong, srel_converse) =>
    3.30        EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm set_mp[OF equalityD2]},
    3.31          rtac (srel_cong RS trans),
    3.32 -        REPEAT_DETERM_N m o rtac @{thm diag_converse},
    3.33 +        REPEAT_DETERM_N m o rtac (@{thm converse_Id_on} RS sym),
    3.34          REPEAT_DETERM_N (length srel_congs) o rtac refl,
    3.35          rtac srel_converse,
    3.36          REPEAT_DETERM o etac allE,
    3.37 @@ -332,7 +332,7 @@
    3.38      CONJ_WRAP' (fn (srel_cong, srel_O) =>
    3.39        EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm set_mp[OF equalityD2]},
    3.40          rtac (srel_cong RS trans),
    3.41 -        REPEAT_DETERM_N m o rtac @{thm diag_Comp},
    3.42 +        REPEAT_DETERM_N m o rtac @{thm Id_on_Comp},
    3.43          REPEAT_DETERM_N (length srel_congs) o rtac refl,
    3.44          rtac srel_O,
    3.45          etac @{thm relcompE},
    3.46 @@ -343,7 +343,7 @@
    3.47  
    3.48  fun mk_bis_Gr_tac bis_srel srel_Grs mor_images morEs coalg_ins
    3.49    {context = ctxt, prems = _} =
    3.50 -  unfold_thms_tac ctxt (bis_srel :: @{thm diag_Gr} :: srel_Grs) THEN
    3.51 +  unfold_thms_tac ctxt (bis_srel :: @{thm Id_on_Gr} :: srel_Grs) THEN
    3.52    EVERY' [rtac conjI,
    3.53      CONJ_WRAP' (fn thm => rtac (@{thm Gr_incl} RS ssubst) THEN' etac thm) mor_images,
    3.54      CONJ_WRAP' (fn (coalg_in, morE) =>
    3.55 @@ -383,12 +383,12 @@
    3.56      REPEAT_DETERM_N n o rtac exI, rtac conjI, rtac refl, atac, rtac equalityD2,
    3.57      rtac (mk_nth_conv n i)] 1;
    3.58  
    3.59 -fun mk_equiv_lsbis_tac sbis_lsbis lsbis_incl incl_lsbis bis_diag bis_converse bis_O =
    3.60 +fun mk_equiv_lsbis_tac sbis_lsbis lsbis_incl incl_lsbis bis_Id_on bis_converse bis_O =
    3.61    EVERY' [rtac (@{thm equiv_def} RS iffD2),
    3.62  
    3.63      rtac conjI, rtac (@{thm refl_on_def} RS iffD2),
    3.64      rtac conjI, rtac lsbis_incl, rtac ballI, rtac set_mp,
    3.65 -    rtac incl_lsbis, rtac bis_diag, atac, etac @{thm diagI},
    3.66 +    rtac incl_lsbis, rtac bis_Id_on, atac, etac @{thm Id_onI},
    3.67  
    3.68      rtac conjI, rtac (@{thm sym_def} RS iffD2),
    3.69      rtac allI, rtac allI, rtac impI, rtac set_mp,
    3.70 @@ -1090,7 +1090,7 @@
    3.71            rtac @{thm xt1(3)}, rtac @{thm Sigma_cong},
    3.72            rtac @{thm proj_image}, rtac @{thm proj_image}, rtac lsbis_incl,
    3.73            rtac subset_trans, rtac @{thm relImage_mono}, rtac incl_lsbis, atac,
    3.74 -          rtac @{thm relImage_proj}, rtac equiv_LSBIS, rtac @{thm relInvImage_diag},
    3.75 +          rtac @{thm relImage_proj}, rtac equiv_LSBIS, rtac @{thm relInvImage_Id_on},
    3.76            rtac Rep_inject])
    3.77        (Rep_injects ~~ (equiv_LSBISs ~~ (incl_lsbiss ~~ lsbis_incls)))] 1
    3.78    end;
    3.79 @@ -1163,16 +1163,16 @@
    3.80          rtac CollectI, etac (refl RSN (2, @{thm subst_Pair}))]) ks] 1
    3.81    end;
    3.82  
    3.83 -fun mk_dtor_map_strong_coinduct_tac ks cTs cts dtor_map_coinduct bis_def bis_diag =
    3.84 +fun mk_dtor_map_strong_coinduct_tac ks cTs cts dtor_map_coinduct bis_def bis_Id_on =
    3.85    EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts dtor_map_coinduct),
    3.86      EVERY' (map (fn i =>
    3.87        EVERY' [etac disjE, REPEAT_DETERM o dtac @{thm meta_spec}, etac meta_mp,
    3.88 -        atac, rtac rev_mp, rtac subst, rtac bis_def, rtac bis_diag,
    3.89 +        atac, rtac rev_mp, rtac subst, rtac bis_def, rtac bis_Id_on,
    3.90          rtac impI, dtac conjunct2, dtac (mk_conjunctN (length ks) i), REPEAT_DETERM o etac allE,
    3.91 -        etac impE, etac @{thm diag_UNIV_I}, REPEAT_DETERM o eresolve_tac [bexE, conjE, CollectE],
    3.92 +        etac impE, etac @{thm Id_on_UNIV_I}, REPEAT_DETERM o eresolve_tac [bexE, conjE, CollectE],
    3.93          rtac exI, rtac conjI, etac conjI, atac,
    3.94          CONJ_WRAP' (K (EVERY' [REPEAT_DETERM o resolve_tac [allI, impI],
    3.95 -          rtac disjI2, rtac @{thm diagE}, etac set_mp, atac])) ks])
    3.96 +          rtac disjI2, rtac @{thm Id_onD}, etac set_mp, atac])) ks])
    3.97      ks),
    3.98      rtac impI, REPEAT_DETERM o etac conjE,
    3.99      CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) ks] 1;
     4.1 --- a/src/HOL/BNF/Tools/bnf_gfp_util.ML	Mon Mar 18 11:05:33 2013 +0100
     4.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_util.ML	Mon Mar 18 11:25:24 2013 +0100
     4.3 @@ -18,7 +18,7 @@
     4.4    val mk_append: term * term -> term
     4.5    val mk_congruent: term -> term -> term
     4.6    val mk_clists: term -> term
     4.7 -  val mk_diag: term -> term
     4.8 +  val mk_Id_on: term -> term
     4.9    val mk_equiv: term -> term -> term
    4.10    val mk_fromCard: term -> term -> term
    4.11    val mk_list_rec: term -> term -> term
    4.12 @@ -59,11 +59,11 @@
    4.13      val ABT = mk_relT (HOLogic.dest_setT AT, HOLogic.dest_setT (range_type BT));
    4.14    in Const (@{const_name Sigma}, AT --> BT --> ABT) $ A $ B end;
    4.15  
    4.16 -fun mk_diag A =
    4.17 +fun mk_Id_on A =
    4.18    let
    4.19      val AT = fastype_of A;
    4.20      val AAT = mk_relT (HOLogic.dest_setT AT, HOLogic.dest_setT AT);
    4.21 -  in Const (@{const_name diag}, AT --> AAT) $ A end;
    4.22 +  in Const (@{const_name Id_on}, AT --> AAT) $ A end;
    4.23  
    4.24  fun mk_Times (A, B) =
    4.25    let val AT = HOLogic.dest_setT (fastype_of A);