src/HOL/Relation.thy
changeset 47433 07f4bf913230
parent 47087 08c22e8ffe70
child 47434 b75ce48a93ee
     1.1 --- a/src/HOL/Relation.thy	Tue Apr 03 08:55:06 2012 +0200
     1.2 +++ b/src/HOL/Relation.thy	Tue Apr 03 17:26:30 2012 +0900
     1.3 @@ -507,29 +507,29 @@
     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 +  "pred_comp \<equiv> relcompp"
    1.17  
    1.18 -lemmas pred_compI = rel_compp.intros
    1.19 +lemmas pred_compI = 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 relcompEpair: "(a, c) \<in> r O s"
    1.28  inductive_cases pred_compE [elim!]: "(r OO s) a c"
    1.29  
    1.30 -lemma rel_compE [elim!]: "xz \<in> r O s \<Longrightarrow>
    1.31 +lemma relcompE [elim!]: "xz \<in> r O s \<Longrightarrow>
    1.32    (\<And>x y z. xz = (x, z) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, z) \<in> s  \<Longrightarrow> P) \<Longrightarrow> P"
    1.33 -  by (cases xz) (simp, erule rel_compEpair, iprover)
    1.34 +  by (cases xz) (simp, erule relcompEpair, iprover)
    1.35  
    1.36 -lemmas pred_comp_rel_comp_eq = rel_compp_rel_comp_eq
    1.37 +lemmas pred_comp_relcomp_eq = relcompp_relcomp_eq
    1.38  
    1.39  lemma R_O_Id [simp]:
    1.40    "R O Id = R"
    1.41 @@ -539,21 +539,21 @@
    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    "\<bottom> OO R = \<bottom>"
    1.52 -  by (fact rel_comp_empty1 [to_pred])
    1.53 +  by (fact relcomp_empty1 [to_pred])
    1.54  
    1.55 -lemma rel_comp_empty2 [simp]:
    1.56 +lemma relcomp_empty2 [simp]:
    1.57    "R O {} = {}"
    1.58    by blast
    1.59  
    1.60  lemma pred_comp_bot2 [simp]:
    1.61    "R OO \<bottom> = \<bottom>"
    1.62 -  by (fact rel_comp_empty2 [to_pred])
    1.63 +  by (fact relcomp_empty2 [to_pred])
    1.64  
    1.65  lemma O_assoc:
    1.66    "(R O S) O T = R O (S O T)"
    1.67 @@ -572,51 +572,51 @@
    1.68    "transp r \<Longrightarrow> r OO r \<le> r "
    1.69    by (fact trans_O_subset [to_pred])
    1.70  
    1.71 -lemma rel_comp_mono:
    1.72 +lemma relcomp_mono:
    1.73    "r' \<subseteq> r \<Longrightarrow> s' \<subseteq> s \<Longrightarrow> r' O s' \<subseteq> r O s"
    1.74    by blast
    1.75  
    1.76  lemma pred_comp_mono:
    1.77    "r' \<le> r \<Longrightarrow> s' \<le> s \<Longrightarrow> r' OO s' \<le> r OO s "
    1.78 -  by (fact rel_comp_mono [to_pred])
    1.79 +  by (fact relcomp_mono [to_pred])
    1.80  
    1.81 -lemma rel_comp_subset_Sigma:
    1.82 +lemma relcomp_subset_Sigma:
    1.83    "r \<subseteq> A \<times> B \<Longrightarrow> s \<subseteq> B \<times> C \<Longrightarrow> r O s \<subseteq> A \<times> C"
    1.84    by blast
    1.85  
    1.86 -lemma rel_comp_distrib [simp]:
    1.87 +lemma relcomp_distrib [simp]:
    1.88    "R O (S \<union> T) = (R O S) \<union> (R O T)" 
    1.89    by auto
    1.90  
    1.91  lemma pred_comp_distrib [simp]:
    1.92    "R OO (S \<squnion> T) = R OO S \<squnion> R OO T"
    1.93 -  by (fact rel_comp_distrib [to_pred])
    1.94 +  by (fact relcomp_distrib [to_pred])
    1.95  
    1.96 -lemma rel_comp_distrib2 [simp]:
    1.97 +lemma relcomp_distrib2 [simp]:
    1.98    "(S \<union> T) O R = (S O R) \<union> (T O R)"
    1.99    by auto
   1.100  
   1.101  lemma pred_comp_distrib2 [simp]:
   1.102    "(S \<squnion> T) OO R = S OO R \<squnion> T OO R"
   1.103 -  by (fact rel_comp_distrib2 [to_pred])
   1.104 +  by (fact relcomp_distrib2 [to_pred])
   1.105  
   1.106 -lemma rel_comp_UNION_distrib:
   1.107 +lemma relcomp_UNION_distrib:
   1.108    "s O UNION I r = (\<Union>i\<in>I. s O r i) "
   1.109    by auto
   1.110  
   1.111 -(* FIXME thm rel_comp_UNION_distrib [to_pred] *)
   1.112 +(* FIXME thm relcomp_UNION_distrib [to_pred] *)
   1.113  
   1.114 -lemma rel_comp_UNION_distrib2:
   1.115 +lemma relcomp_UNION_distrib2:
   1.116    "UNION I r O s = (\<Union>i\<in>I. r i O s) "
   1.117    by auto
   1.118  
   1.119 -(* FIXME thm rel_comp_UNION_distrib2 [to_pred] *)
   1.120 +(* FIXME thm relcomp_UNION_distrib2 [to_pred] *)
   1.121  
   1.122 -lemma single_valued_rel_comp:
   1.123 +lemma single_valued_relcomp:
   1.124    "single_valued r \<Longrightarrow> single_valued s \<Longrightarrow> single_valued (r O s)"
   1.125    by (unfold single_valued_def) blast
   1.126  
   1.127 -lemma rel_comp_unfold:
   1.128 +lemma relcomp_unfold:
   1.129    "r O s = {(x, z). \<exists>y. (x, y) \<in> r \<and> (y, z) \<in> s}"
   1.130    by (auto simp add: set_eq_iff)
   1.131  
   1.132 @@ -676,7 +676,7 @@
   1.133    "(r\<inverse>\<inverse>)\<inverse>\<inverse> = r"
   1.134    by (fact converse_converse [to_pred])
   1.135  
   1.136 -lemma converse_rel_comp: "(r O s)^-1 = s^-1 O r^-1"
   1.137 +lemma converse_relcomp: "(r O s)^-1 = s^-1 O r^-1"
   1.138    by blast
   1.139  
   1.140  lemma converse_pred_comp: "(r OO s)^--1 = s^--1 OO r^--1"