src/HOL/Relation.thy
changeset 47436 d8fad618a67a
parent 47375 8e6a45f1bf8f
parent 47434 b75ce48a93ee
child 47937 70375fa2679d
     1.1 --- a/src/HOL/Relation.thy	Thu Apr 12 10:13:33 2012 +0200
     1.2 +++ b/src/HOL/Relation.thy	Thu Apr 12 11:01:15 2012 +0200
     1.3 @@ -507,29 +507,26 @@
     1.4  
     1.5  subsubsection {* Composition *}
     1.6  
     1.7 -inductive_set rel_comp  :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'c) set \<Rightarrow> ('a \<times> 'c) set" (infixr "O" 75)
     1.8 +inductive_set relcomp  :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'c) set \<Rightarrow> ('a \<times> 'c) set" (infixr "O" 75)
     1.9    for r :: "('a \<times> 'b) set" and s :: "('b \<times> 'c) set"
    1.10  where
    1.11 -  rel_compI [intro]: "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> s \<Longrightarrow> (a, c) \<in> r O s"
    1.12 +  relcompI [intro]: "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> s \<Longrightarrow> (a, c) \<in> r O s"
    1.13  
    1.14 -abbreviation pred_comp (infixr "OO" 75) where
    1.15 -  "pred_comp \<equiv> rel_compp"
    1.16 +notation relcompp (infixr "OO" 75)
    1.17  
    1.18 -lemmas pred_compI = rel_compp.intros
    1.19 +lemmas relcomppI = relcompp.intros
    1.20  
    1.21  text {*
    1.22    For historic reasons, the elimination rules are not wholly corresponding.
    1.23    Feel free to consolidate this.
    1.24  *}
    1.25  
    1.26 -inductive_cases rel_compEpair: "(a, c) \<in> r O s"
    1.27 -inductive_cases pred_compE [elim!]: "(r OO s) a c"
    1.28 +inductive_cases relcompEpair: "(a, c) \<in> r O s"
    1.29 +inductive_cases relcomppE [elim!]: "(r OO s) a c"
    1.30  
    1.31 -lemma rel_compE [elim!]: "xz \<in> r O s \<Longrightarrow>
    1.32 +lemma relcompE [elim!]: "xz \<in> r O s \<Longrightarrow>
    1.33    (\<And>x y z. xz = (x, z) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, z) \<in> s  \<Longrightarrow> P) \<Longrightarrow> P"
    1.34 -  by (cases xz) (simp, erule rel_compEpair, iprover)
    1.35 -
    1.36 -lemmas pred_comp_rel_comp_eq = rel_compp_rel_comp_eq
    1.37 +  by (cases xz) (simp, erule relcompEpair, iprover)
    1.38  
    1.39  lemma R_O_Id [simp]:
    1.40    "R O Id = R"
    1.41 @@ -539,28 +536,28 @@
    1.42    "Id O R = R"
    1.43    by fast
    1.44  
    1.45 -lemma rel_comp_empty1 [simp]:
    1.46 +lemma relcomp_empty1 [simp]:
    1.47    "{} O R = {}"
    1.48    by blast
    1.49  
    1.50 -lemma pred_comp_bot1 [simp]:
    1.51 +lemma relcompp_bot1 [simp]:
    1.52    "\<bottom> OO R = \<bottom>"
    1.53 -  by (fact rel_comp_empty1 [to_pred])
    1.54 +  by (fact relcomp_empty1 [to_pred])
    1.55  
    1.56 -lemma rel_comp_empty2 [simp]:
    1.57 +lemma relcomp_empty2 [simp]:
    1.58    "R O {} = {}"
    1.59    by blast
    1.60  
    1.61 -lemma pred_comp_bot2 [simp]:
    1.62 +lemma relcompp_bot2 [simp]:
    1.63    "R OO \<bottom> = \<bottom>"
    1.64 -  by (fact rel_comp_empty2 [to_pred])
    1.65 +  by (fact relcomp_empty2 [to_pred])
    1.66  
    1.67  lemma O_assoc:
    1.68    "(R O S) O T = R O (S O T)"
    1.69    by blast
    1.70  
    1.71  
    1.72 -lemma pred_comp_assoc:
    1.73 +lemma relcompp_assoc:
    1.74    "(r OO s) OO t = r OO (s OO t)"
    1.75    by (fact O_assoc [to_pred])
    1.76  
    1.77 @@ -568,55 +565,55 @@
    1.78    "trans r \<Longrightarrow> r O r \<subseteq> r"
    1.79    by (unfold trans_def) blast
    1.80  
    1.81 -lemma transp_pred_comp_less_eq:
    1.82 +lemma transp_relcompp_less_eq:
    1.83    "transp r \<Longrightarrow> r OO r \<le> r "
    1.84    by (fact trans_O_subset [to_pred])
    1.85  
    1.86 -lemma rel_comp_mono:
    1.87 +lemma relcomp_mono:
    1.88    "r' \<subseteq> r \<Longrightarrow> s' \<subseteq> s \<Longrightarrow> r' O s' \<subseteq> r O s"
    1.89    by blast
    1.90  
    1.91 -lemma pred_comp_mono:
    1.92 +lemma relcompp_mono:
    1.93    "r' \<le> r \<Longrightarrow> s' \<le> s \<Longrightarrow> r' OO s' \<le> r OO s "
    1.94 -  by (fact rel_comp_mono [to_pred])
    1.95 +  by (fact relcomp_mono [to_pred])
    1.96  
    1.97 -lemma rel_comp_subset_Sigma:
    1.98 +lemma relcomp_subset_Sigma:
    1.99    "r \<subseteq> A \<times> B \<Longrightarrow> s \<subseteq> B \<times> C \<Longrightarrow> r O s \<subseteq> A \<times> C"
   1.100    by blast
   1.101  
   1.102 -lemma rel_comp_distrib [simp]:
   1.103 +lemma relcomp_distrib [simp]:
   1.104    "R O (S \<union> T) = (R O S) \<union> (R O T)" 
   1.105    by auto
   1.106  
   1.107 -lemma pred_comp_distrib [simp]:
   1.108 +lemma relcompp_distrib [simp]:
   1.109    "R OO (S \<squnion> T) = R OO S \<squnion> R OO T"
   1.110 -  by (fact rel_comp_distrib [to_pred])
   1.111 +  by (fact relcomp_distrib [to_pred])
   1.112  
   1.113 -lemma rel_comp_distrib2 [simp]:
   1.114 +lemma relcomp_distrib2 [simp]:
   1.115    "(S \<union> T) O R = (S O R) \<union> (T O R)"
   1.116    by auto
   1.117  
   1.118 -lemma pred_comp_distrib2 [simp]:
   1.119 +lemma relcompp_distrib2 [simp]:
   1.120    "(S \<squnion> T) OO R = S OO R \<squnion> T OO R"
   1.121 -  by (fact rel_comp_distrib2 [to_pred])
   1.122 +  by (fact relcomp_distrib2 [to_pred])
   1.123  
   1.124 -lemma rel_comp_UNION_distrib:
   1.125 +lemma relcomp_UNION_distrib:
   1.126    "s O UNION I r = (\<Union>i\<in>I. s O r i) "
   1.127    by auto
   1.128  
   1.129 -(* FIXME thm rel_comp_UNION_distrib [to_pred] *)
   1.130 +(* FIXME thm relcomp_UNION_distrib [to_pred] *)
   1.131  
   1.132 -lemma rel_comp_UNION_distrib2:
   1.133 +lemma relcomp_UNION_distrib2:
   1.134    "UNION I r O s = (\<Union>i\<in>I. r i O s) "
   1.135    by auto
   1.136  
   1.137 -(* FIXME thm rel_comp_UNION_distrib2 [to_pred] *)
   1.138 +(* FIXME thm relcomp_UNION_distrib2 [to_pred] *)
   1.139  
   1.140 -lemma single_valued_rel_comp:
   1.141 +lemma single_valued_relcomp:
   1.142    "single_valued r \<Longrightarrow> single_valued s \<Longrightarrow> single_valued (r O s)"
   1.143    by (unfold single_valued_def) blast
   1.144  
   1.145 -lemma rel_comp_unfold:
   1.146 +lemma relcomp_unfold:
   1.147    "r O s = {(x, z). \<exists>y. (x, y) \<in> r \<and> (y, z) \<in> s}"
   1.148    by (auto simp add: set_eq_iff)
   1.149  
   1.150 @@ -676,12 +673,12 @@
   1.151    "(r\<inverse>\<inverse>)\<inverse>\<inverse> = r"
   1.152    by (fact converse_converse [to_pred])
   1.153  
   1.154 -lemma converse_rel_comp: "(r O s)^-1 = s^-1 O r^-1"
   1.155 +lemma converse_relcomp: "(r O s)^-1 = s^-1 O r^-1"
   1.156    by blast
   1.157  
   1.158 -lemma converse_pred_comp: "(r OO s)^--1 = s^--1 OO r^--1"
   1.159 -  by (iprover intro: order_antisym conversepI pred_compI
   1.160 -    elim: pred_compE dest: conversepD)
   1.161 +lemma converse_relcompp: "(r OO s)^--1 = s^--1 OO r^--1"
   1.162 +  by (iprover intro: order_antisym conversepI relcomppI
   1.163 +    elim: relcomppE dest: conversepD)
   1.164  
   1.165  lemma converse_Int: "(r \<inter> s)^-1 = r^-1 \<inter> s^-1"
   1.166    by blast