src/HOL/BNF/BNF_GFP.thy
changeset 51447 a19e973fa2cf
parent 51446 a6ebb12cc003
child 51739 3514b90d0a8b
     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"