src/HOL/Relation.thy
changeset 47434 b75ce48a93ee
parent 47433 07f4bf913230
child 47436 d8fad618a67a
     1.1 --- a/src/HOL/Relation.thy	Tue Apr 03 17:26:30 2012 +0900
     1.2 +++ b/src/HOL/Relation.thy	Tue Apr 03 17:45:06 2012 +0900
     1.3 @@ -512,10 +512,9 @@
     1.4  where
     1.5    relcompI [intro]: "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> s \<Longrightarrow> (a, c) \<in> r O s"
     1.6  
     1.7 -abbreviation pred_comp (infixr "OO" 75) where
     1.8 -  "pred_comp \<equiv> relcompp"
     1.9 +notation relcompp (infixr "OO" 75)
    1.10  
    1.11 -lemmas pred_compI = relcompp.intros
    1.12 +lemmas relcomppI = relcompp.intros
    1.13  
    1.14  text {*
    1.15    For historic reasons, the elimination rules are not wholly corresponding.
    1.16 @@ -523,14 +522,12 @@
    1.17  *}
    1.18  
    1.19  inductive_cases relcompEpair: "(a, c) \<in> r O s"
    1.20 -inductive_cases pred_compE [elim!]: "(r OO s) a c"
    1.21 +inductive_cases relcomppE [elim!]: "(r OO s) a c"
    1.22  
    1.23  lemma relcompE [elim!]: "xz \<in> r O s \<Longrightarrow>
    1.24    (\<And>x y z. xz = (x, z) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, z) \<in> s  \<Longrightarrow> P) \<Longrightarrow> P"
    1.25    by (cases xz) (simp, erule relcompEpair, iprover)
    1.26  
    1.27 -lemmas pred_comp_relcomp_eq = relcompp_relcomp_eq
    1.28 -
    1.29  lemma R_O_Id [simp]:
    1.30    "R O Id = R"
    1.31    by fast
    1.32 @@ -543,7 +540,7 @@
    1.33    "{} O R = {}"
    1.34    by blast
    1.35  
    1.36 -lemma pred_comp_bot1 [simp]:
    1.37 +lemma relcompp_bot1 [simp]:
    1.38    "\<bottom> OO R = \<bottom>"
    1.39    by (fact relcomp_empty1 [to_pred])
    1.40  
    1.41 @@ -551,7 +548,7 @@
    1.42    "R O {} = {}"
    1.43    by blast
    1.44  
    1.45 -lemma pred_comp_bot2 [simp]:
    1.46 +lemma relcompp_bot2 [simp]:
    1.47    "R OO \<bottom> = \<bottom>"
    1.48    by (fact relcomp_empty2 [to_pred])
    1.49  
    1.50 @@ -560,7 +557,7 @@
    1.51    by blast
    1.52  
    1.53  
    1.54 -lemma pred_comp_assoc:
    1.55 +lemma relcompp_assoc:
    1.56    "(r OO s) OO t = r OO (s OO t)"
    1.57    by (fact O_assoc [to_pred])
    1.58  
    1.59 @@ -568,7 +565,7 @@
    1.60    "trans r \<Longrightarrow> r O r \<subseteq> r"
    1.61    by (unfold trans_def) blast
    1.62  
    1.63 -lemma transp_pred_comp_less_eq:
    1.64 +lemma transp_relcompp_less_eq:
    1.65    "transp r \<Longrightarrow> r OO r \<le> r "
    1.66    by (fact trans_O_subset [to_pred])
    1.67  
    1.68 @@ -576,7 +573,7 @@
    1.69    "r' \<subseteq> r \<Longrightarrow> s' \<subseteq> s \<Longrightarrow> r' O s' \<subseteq> r O s"
    1.70    by blast
    1.71  
    1.72 -lemma pred_comp_mono:
    1.73 +lemma relcompp_mono:
    1.74    "r' \<le> r \<Longrightarrow> s' \<le> s \<Longrightarrow> r' OO s' \<le> r OO s "
    1.75    by (fact relcomp_mono [to_pred])
    1.76  
    1.77 @@ -588,7 +585,7 @@
    1.78    "R O (S \<union> T) = (R O S) \<union> (R O T)" 
    1.79    by auto
    1.80  
    1.81 -lemma pred_comp_distrib [simp]:
    1.82 +lemma relcompp_distrib [simp]:
    1.83    "R OO (S \<squnion> T) = R OO S \<squnion> R OO T"
    1.84    by (fact relcomp_distrib [to_pred])
    1.85  
    1.86 @@ -596,7 +593,7 @@
    1.87    "(S \<union> T) O R = (S O R) \<union> (T O R)"
    1.88    by auto
    1.89  
    1.90 -lemma pred_comp_distrib2 [simp]:
    1.91 +lemma relcompp_distrib2 [simp]:
    1.92    "(S \<squnion> T) OO R = S OO R \<squnion> T OO R"
    1.93    by (fact relcomp_distrib2 [to_pred])
    1.94  
    1.95 @@ -679,9 +676,9 @@
    1.96  lemma converse_relcomp: "(r O s)^-1 = s^-1 O r^-1"
    1.97    by blast
    1.98  
    1.99 -lemma converse_pred_comp: "(r OO s)^--1 = s^--1 OO r^--1"
   1.100 -  by (iprover intro: order_antisym conversepI pred_compI
   1.101 -    elim: pred_compE dest: conversepD)
   1.102 +lemma converse_relcompp: "(r OO s)^--1 = s^--1 OO r^--1"
   1.103 +  by (iprover intro: order_antisym conversepI relcomppI
   1.104 +    elim: relcomppE dest: conversepD)
   1.105  
   1.106  lemma converse_Int: "(r \<inter> s)^-1 = r^-1 \<inter> s^-1"
   1.107    by blast