merged
authorbulwahn
Thu Apr 12 11:01:15 2012 +0200 (2012-04-12)
changeset 47436d8fad618a67a
parent 47429 ec64d94cbf9c
parent 47435 e1b761c216ac
child 47438 11a0aa6cc677
merged
src/HOL/Lifting.thy
src/HOL/List.thy
src/HOL/Quotient.thy
src/HOL/Relation.thy
     1.1 --- a/src/HOL/Lifting.thy	Thu Apr 12 10:13:33 2012 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Thu Apr 12 11:01:15 2012 +0200
     1.3 @@ -199,19 +199,19 @@
     1.4      apply safe
     1.5      apply (drule Abs1, simp)
     1.6      apply (erule Abs2)
     1.7 -    apply (rule pred_compI)
     1.8 +    apply (rule relcomppI)
     1.9      apply (rule Rep1)
    1.10      apply (rule Rep2)
    1.11 -    apply (rule pred_compI, assumption)
    1.12 +    apply (rule relcomppI, assumption)
    1.13      apply (drule Abs1, simp)
    1.14      apply (clarsimp simp add: R2)
    1.15 -    apply (rule pred_compI, assumption)
    1.16 +    apply (rule relcomppI, assumption)
    1.17      apply (drule Abs1, simp)+
    1.18      apply (clarsimp simp add: R2)
    1.19      apply (drule Abs1, simp)+
    1.20      apply (clarsimp simp add: R2)
    1.21 -    apply (rule pred_compI, assumption)
    1.22 -    apply (rule pred_compI [rotated])
    1.23 +    apply (rule relcomppI, assumption)
    1.24 +    apply (rule relcomppI [rotated])
    1.25      apply (erule conversepI)
    1.26      apply (drule Abs1, simp)+
    1.27      apply (simp add: R2)
     2.1 --- a/src/HOL/List.thy	Thu Apr 12 10:13:33 2012 +0200
     2.2 +++ b/src/HOL/List.thy	Thu Apr 12 11:01:15 2012 +0200
     2.3 @@ -5677,7 +5677,7 @@
     2.4    "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)"
     2.5    by (simp add: finite_trancl_ntranl)
     2.6  
     2.7 -lemma set_rel_comp [code]:
     2.8 +lemma set_relcomp [code]:
     2.9    "set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
    2.10    by (auto simp add: Bex_def)
    2.11  
     3.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Thu Apr 12 10:13:33 2012 +0200
     3.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Thu Apr 12 11:01:15 2012 +0200
     3.3 @@ -1027,8 +1027,8 @@
     3.4    (o * o => bool) => i * i => bool) [inductify] converse .
     3.5  
     3.6  thm converse.equation
     3.7 -code_pred [inductify] rel_comp .
     3.8 -thm rel_comp.equation
     3.9 +code_pred [inductify] relcomp .
    3.10 +thm relcomp.equation
    3.11  code_pred [inductify] Image .
    3.12  thm Image.equation
    3.13  declare singleton_iff[code_pred_inline]
     4.1 --- a/src/HOL/Quotient.thy	Thu Apr 12 10:13:33 2012 +0200
     4.2 +++ b/src/HOL/Quotient.thy	Thu Apr 12 11:01:15 2012 +0200
     4.3 @@ -694,9 +694,9 @@
     4.4  apply (rule Quotient3I)
     4.5     apply (simp add: o_def Quotient3_abs_rep [OF R2] Quotient3_abs_rep [OF R1])
     4.6    apply simp
     4.7 -  apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI)
     4.8 +  apply (rule_tac b="Rep1 (Rep2 a)" in relcomppI)
     4.9     apply (rule Quotient3_rep_reflp [OF R1])
    4.10 -  apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI [rotated])
    4.11 +  apply (rule_tac b="Rep1 (Rep2 a)" in relcomppI [rotated])
    4.12     apply (rule Quotient3_rep_reflp [OF R1])
    4.13    apply (rule Rep1)
    4.14    apply (rule Quotient3_rep_reflp [OF R2])
    4.15 @@ -707,8 +707,8 @@
    4.16       apply (erule Quotient3_refl1 [OF R1])
    4.17      apply (drule Quotient3_refl1 [OF R2], drule Rep1)
    4.18      apply (subgoal_tac "R1 r (Rep1 (Abs1 x))")
    4.19 -     apply (rule_tac b="Rep1 (Abs1 x)" in pred_compI, assumption)
    4.20 -     apply (erule pred_compI)
    4.21 +     apply (rule_tac b="Rep1 (Abs1 x)" in relcomppI, assumption)
    4.22 +     apply (erule relcomppI)
    4.23       apply (erule Quotient3_symp [OF R1, THEN sympD])
    4.24      apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2])
    4.25      apply (rule conjI, erule Quotient3_refl1 [OF R1])
    4.26 @@ -721,8 +721,8 @@
    4.27      apply (erule Quotient3_refl1 [OF R1])
    4.28     apply (drule Quotient3_refl2 [OF R2], drule Rep1)
    4.29     apply (subgoal_tac "R1 s (Rep1 (Abs1 y))")
    4.30 -    apply (rule_tac b="Rep1 (Abs1 y)" in pred_compI, assumption)
    4.31 -    apply (erule pred_compI)
    4.32 +    apply (rule_tac b="Rep1 (Abs1 y)" in relcomppI, assumption)
    4.33 +    apply (erule relcomppI)
    4.34      apply (erule Quotient3_symp [OF R1, THEN sympD])
    4.35     apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2])
    4.36     apply (rule conjI, erule Quotient3_refl2 [OF R1])
    4.37 @@ -738,11 +738,11 @@
    4.38    apply (erule Quotient3_refl1 [OF R1])
    4.39   apply (rename_tac a b c d)
    4.40   apply simp
    4.41 - apply (rule_tac b="Rep1 (Abs1 r)" in pred_compI)
    4.42 + apply (rule_tac b="Rep1 (Abs1 r)" in relcomppI)
    4.43    apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2])
    4.44    apply (rule conjI, erule Quotient3_refl1 [OF R1])
    4.45    apply (simp add: Quotient3_abs_rep [OF R1] Quotient3_rep_reflp [OF R1])
    4.46 - apply (rule_tac b="Rep1 (Abs1 s)" in pred_compI [rotated])
    4.47 + apply (rule_tac b="Rep1 (Abs1 s)" in relcomppI [rotated])
    4.48    apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2])
    4.49    apply (simp add: Quotient3_abs_rep [OF R1] Quotient3_rep_reflp [OF R1])
    4.50    apply (erule Quotient3_refl2 [OF R1])
     5.1 --- a/src/HOL/Quotient_Examples/FSet.thy	Thu Apr 12 10:13:33 2012 +0200
     5.2 +++ b/src/HOL/Quotient_Examples/FSet.thy	Thu Apr 12 11:01:15 2012 +0200
     5.3 @@ -140,7 +140,7 @@
     5.4    next
     5.5      assume a: "(list_all2 R OOO op \<approx>) r s"
     5.6      then have b: "map Abs r \<approx> map Abs s"
     5.7 -    proof (elim pred_compE)
     5.8 +    proof (elim relcomppE)
     5.9        fix b ba
    5.10        assume c: "list_all2 R r b"
    5.11        assume d: "b \<approx> ba"
    5.12 @@ -165,11 +165,11 @@
    5.13      have y: "list_all2 R (map Rep (map Abs s)) s"
    5.14        by (fact rep_abs_rsp_left[OF list_quotient3[OF q], OF list_all2_refl'[OF e, of s]])
    5.15      have c: "(op \<approx> OO list_all2 R) (map Rep (map Abs r)) s"
    5.16 -      by (rule pred_compI) (rule b, rule y)
    5.17 +      by (rule relcomppI) (rule b, rule y)
    5.18      have z: "list_all2 R r (map Rep (map Abs r))"
    5.19        by (fact rep_abs_rsp[OF list_quotient3[OF q], OF list_all2_refl'[OF e, of r]])
    5.20      then show "(list_all2 R OOO op \<approx>) r s"
    5.21 -      using a c pred_compI by simp
    5.22 +      using a c relcomppI by simp
    5.23    qed
    5.24  qed
    5.25  
    5.26 @@ -360,7 +360,7 @@
    5.27  quotient_definition
    5.28    "concat_fset :: ('a fset) fset \<Rightarrow> 'a fset"
    5.29    is concat 
    5.30 -proof (elim pred_compE)
    5.31 +proof (elim relcomppE)
    5.32  fix a b ba bb
    5.33    assume a: "list_all2 op \<approx> a ba"
    5.34    with list_symp [OF list_eq_symp] have a': "list_all2 op \<approx> ba a" by (rule sympE)
    5.35 @@ -397,9 +397,9 @@
    5.36  lemma Cons_rsp2 [quot_respect]:
    5.37    shows "(op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) Cons Cons"
    5.38    apply (auto intro!: fun_relI)
    5.39 -  apply (rule_tac b="x # b" in pred_compI)
    5.40 +  apply (rule_tac b="x # b" in relcomppI)
    5.41    apply auto
    5.42 -  apply (rule_tac b="x # ba" in pred_compI)
    5.43 +  apply (rule_tac b="x # ba" in relcomppI)
    5.44    apply auto
    5.45    done
    5.46  
    5.47 @@ -453,7 +453,7 @@
    5.48    assumes "(R1 ===> R2 ===> R3) C C" and "(R4 ===> R5 ===> R6) C C"
    5.49    shows "(R1 OOO R4 ===> R2 OOO R5 ===> R3 OOO R6) C C"
    5.50    by (auto intro!: fun_relI)
    5.51 -     (metis (full_types) assms fun_relE pred_compI)
    5.52 +     (metis (full_types) assms fun_relE relcomppI)
    5.53  
    5.54  lemma append_rsp2 [quot_respect]:
    5.55    "(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) append append"
    5.56 @@ -479,7 +479,7 @@
    5.57      by (induct y ya rule: list_induct2')
    5.58         (simp_all, metis apply_rsp' list_eq_def)
    5.59    show "(list_all2 op \<approx> OOO op \<approx>) (map f xa) (map f' ya)"
    5.60 -    by (metis a b c list_eq_def pred_compI)
    5.61 +    by (metis a b c list_eq_def relcomppI)
    5.62  qed
    5.63  
    5.64  lemma map_prs2 [quot_preserve]:
     6.1 --- a/src/HOL/Relation.thy	Thu Apr 12 10:13:33 2012 +0200
     6.2 +++ b/src/HOL/Relation.thy	Thu Apr 12 11:01:15 2012 +0200
     6.3 @@ -507,29 +507,26 @@
     6.4  
     6.5  subsubsection {* Composition *}
     6.6  
     6.7 -inductive_set rel_comp  :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'c) set \<Rightarrow> ('a \<times> 'c) set" (infixr "O" 75)
     6.8 +inductive_set relcomp  :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'c) set \<Rightarrow> ('a \<times> 'c) set" (infixr "O" 75)
     6.9    for r :: "('a \<times> 'b) set" and s :: "('b \<times> 'c) set"
    6.10  where
    6.11 -  rel_compI [intro]: "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> s \<Longrightarrow> (a, c) \<in> r O s"
    6.12 +  relcompI [intro]: "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> s \<Longrightarrow> (a, c) \<in> r O s"
    6.13  
    6.14 -abbreviation pred_comp (infixr "OO" 75) where
    6.15 -  "pred_comp \<equiv> rel_compp"
    6.16 +notation relcompp (infixr "OO" 75)
    6.17  
    6.18 -lemmas pred_compI = rel_compp.intros
    6.19 +lemmas relcomppI = relcompp.intros
    6.20  
    6.21  text {*
    6.22    For historic reasons, the elimination rules are not wholly corresponding.
    6.23    Feel free to consolidate this.
    6.24  *}
    6.25  
    6.26 -inductive_cases rel_compEpair: "(a, c) \<in> r O s"
    6.27 -inductive_cases pred_compE [elim!]: "(r OO s) a c"
    6.28 +inductive_cases relcompEpair: "(a, c) \<in> r O s"
    6.29 +inductive_cases relcomppE [elim!]: "(r OO s) a c"
    6.30  
    6.31 -lemma rel_compE [elim!]: "xz \<in> r O s \<Longrightarrow>
    6.32 +lemma relcompE [elim!]: "xz \<in> r O s \<Longrightarrow>
    6.33    (\<And>x y z. xz = (x, z) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, z) \<in> s  \<Longrightarrow> P) \<Longrightarrow> P"
    6.34 -  by (cases xz) (simp, erule rel_compEpair, iprover)
    6.35 -
    6.36 -lemmas pred_comp_rel_comp_eq = rel_compp_rel_comp_eq
    6.37 +  by (cases xz) (simp, erule relcompEpair, iprover)
    6.38  
    6.39  lemma R_O_Id [simp]:
    6.40    "R O Id = R"
    6.41 @@ -539,28 +536,28 @@
    6.42    "Id O R = R"
    6.43    by fast
    6.44  
    6.45 -lemma rel_comp_empty1 [simp]:
    6.46 +lemma relcomp_empty1 [simp]:
    6.47    "{} O R = {}"
    6.48    by blast
    6.49  
    6.50 -lemma pred_comp_bot1 [simp]:
    6.51 +lemma relcompp_bot1 [simp]:
    6.52    "\<bottom> OO R = \<bottom>"
    6.53 -  by (fact rel_comp_empty1 [to_pred])
    6.54 +  by (fact relcomp_empty1 [to_pred])
    6.55  
    6.56 -lemma rel_comp_empty2 [simp]:
    6.57 +lemma relcomp_empty2 [simp]:
    6.58    "R O {} = {}"
    6.59    by blast
    6.60  
    6.61 -lemma pred_comp_bot2 [simp]:
    6.62 +lemma relcompp_bot2 [simp]:
    6.63    "R OO \<bottom> = \<bottom>"
    6.64 -  by (fact rel_comp_empty2 [to_pred])
    6.65 +  by (fact relcomp_empty2 [to_pred])
    6.66  
    6.67  lemma O_assoc:
    6.68    "(R O S) O T = R O (S O T)"
    6.69    by blast
    6.70  
    6.71  
    6.72 -lemma pred_comp_assoc:
    6.73 +lemma relcompp_assoc:
    6.74    "(r OO s) OO t = r OO (s OO t)"
    6.75    by (fact O_assoc [to_pred])
    6.76  
    6.77 @@ -568,55 +565,55 @@
    6.78    "trans r \<Longrightarrow> r O r \<subseteq> r"
    6.79    by (unfold trans_def) blast
    6.80  
    6.81 -lemma transp_pred_comp_less_eq:
    6.82 +lemma transp_relcompp_less_eq:
    6.83    "transp r \<Longrightarrow> r OO r \<le> r "
    6.84    by (fact trans_O_subset [to_pred])
    6.85  
    6.86 -lemma rel_comp_mono:
    6.87 +lemma relcomp_mono:
    6.88    "r' \<subseteq> r \<Longrightarrow> s' \<subseteq> s \<Longrightarrow> r' O s' \<subseteq> r O s"
    6.89    by blast
    6.90  
    6.91 -lemma pred_comp_mono:
    6.92 +lemma relcompp_mono:
    6.93    "r' \<le> r \<Longrightarrow> s' \<le> s \<Longrightarrow> r' OO s' \<le> r OO s "
    6.94 -  by (fact rel_comp_mono [to_pred])
    6.95 +  by (fact relcomp_mono [to_pred])
    6.96  
    6.97 -lemma rel_comp_subset_Sigma:
    6.98 +lemma relcomp_subset_Sigma:
    6.99    "r \<subseteq> A \<times> B \<Longrightarrow> s \<subseteq> B \<times> C \<Longrightarrow> r O s \<subseteq> A \<times> C"
   6.100    by blast
   6.101  
   6.102 -lemma rel_comp_distrib [simp]:
   6.103 +lemma relcomp_distrib [simp]:
   6.104    "R O (S \<union> T) = (R O S) \<union> (R O T)" 
   6.105    by auto
   6.106  
   6.107 -lemma pred_comp_distrib [simp]:
   6.108 +lemma relcompp_distrib [simp]:
   6.109    "R OO (S \<squnion> T) = R OO S \<squnion> R OO T"
   6.110 -  by (fact rel_comp_distrib [to_pred])
   6.111 +  by (fact relcomp_distrib [to_pred])
   6.112  
   6.113 -lemma rel_comp_distrib2 [simp]:
   6.114 +lemma relcomp_distrib2 [simp]:
   6.115    "(S \<union> T) O R = (S O R) \<union> (T O R)"
   6.116    by auto
   6.117  
   6.118 -lemma pred_comp_distrib2 [simp]:
   6.119 +lemma relcompp_distrib2 [simp]:
   6.120    "(S \<squnion> T) OO R = S OO R \<squnion> T OO R"
   6.121 -  by (fact rel_comp_distrib2 [to_pred])
   6.122 +  by (fact relcomp_distrib2 [to_pred])
   6.123  
   6.124 -lemma rel_comp_UNION_distrib:
   6.125 +lemma relcomp_UNION_distrib:
   6.126    "s O UNION I r = (\<Union>i\<in>I. s O r i) "
   6.127    by auto
   6.128  
   6.129 -(* FIXME thm rel_comp_UNION_distrib [to_pred] *)
   6.130 +(* FIXME thm relcomp_UNION_distrib [to_pred] *)
   6.131  
   6.132 -lemma rel_comp_UNION_distrib2:
   6.133 +lemma relcomp_UNION_distrib2:
   6.134    "UNION I r O s = (\<Union>i\<in>I. r i O s) "
   6.135    by auto
   6.136  
   6.137 -(* FIXME thm rel_comp_UNION_distrib2 [to_pred] *)
   6.138 +(* FIXME thm relcomp_UNION_distrib2 [to_pred] *)
   6.139  
   6.140 -lemma single_valued_rel_comp:
   6.141 +lemma single_valued_relcomp:
   6.142    "single_valued r \<Longrightarrow> single_valued s \<Longrightarrow> single_valued (r O s)"
   6.143    by (unfold single_valued_def) blast
   6.144  
   6.145 -lemma rel_comp_unfold:
   6.146 +lemma relcomp_unfold:
   6.147    "r O s = {(x, z). \<exists>y. (x, y) \<in> r \<and> (y, z) \<in> s}"
   6.148    by (auto simp add: set_eq_iff)
   6.149  
   6.150 @@ -676,12 +673,12 @@
   6.151    "(r\<inverse>\<inverse>)\<inverse>\<inverse> = r"
   6.152    by (fact converse_converse [to_pred])
   6.153  
   6.154 -lemma converse_rel_comp: "(r O s)^-1 = s^-1 O r^-1"
   6.155 +lemma converse_relcomp: "(r O s)^-1 = s^-1 O r^-1"
   6.156    by blast
   6.157  
   6.158 -lemma converse_pred_comp: "(r OO s)^--1 = s^--1 OO r^--1"
   6.159 -  by (iprover intro: order_antisym conversepI pred_compI
   6.160 -    elim: pred_compE dest: conversepD)
   6.161 +lemma converse_relcompp: "(r OO s)^--1 = s^--1 OO r^--1"
   6.162 +  by (iprover intro: order_antisym conversepI relcomppI
   6.163 +    elim: relcomppE dest: conversepD)
   6.164  
   6.165  lemma converse_Int: "(r \<inter> s)^-1 = r^-1 \<inter> s^-1"
   6.166    by blast
     7.1 --- a/src/HOL/Tools/Function/termination.ML	Thu Apr 12 10:13:33 2012 +0200
     7.2 +++ b/src/HOL/Tools/Function/termination.ML	Thu Apr 12 11:01:15 2012 +0200
     7.3 @@ -141,7 +141,7 @@
     7.4  fun prove_chain thy chain_tac (c1, c2) =
     7.5    let
     7.6      val goal =
     7.7 -      HOLogic.mk_eq (HOLogic.mk_binop @{const_name Relation.rel_comp} (c1, c2),
     7.8 +      HOLogic.mk_eq (HOLogic.mk_binop @{const_name Relation.relcomp} (c1, c2),
     7.9          Const (@{const_abbrev Set.empty}, fastype_of c1))
    7.10        |> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *)
    7.11    in
     8.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Apr 12 10:13:33 2012 +0200
     8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Apr 12 11:01:15 2012 +0200
     8.3 @@ -391,7 +391,7 @@
     8.4     (@{const_name Id}, 0),
     8.5     (@{const_name converse}, 1),
     8.6     (@{const_name trancl}, 1),
     8.7 -   (@{const_name rel_comp}, 2),
     8.8 +   (@{const_name relcomp}, 2),
     8.9     (@{const_name finite}, 1),
    8.10     (@{const_name unknown}, 0),
    8.11     (@{const_name is_unknown}, 1),
     9.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Apr 12 10:13:33 2012 +0200
     9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Apr 12 11:01:15 2012 +0200
     9.3 @@ -856,7 +856,7 @@
     9.4                   accum ||> add_annotation_atom_comp Neq [] (V x) (A New))
     9.5                end
     9.6              | @{const_name trancl} => do_fragile_set_operation T accum
     9.7 -            | @{const_name rel_comp} =>
     9.8 +            | @{const_name relcomp} =>
     9.9                let
    9.10                  val x = Unsynchronized.inc max_fresh
    9.11                  val bc_set_M = domain_type T |> mtype_for_set x
    10.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Thu Apr 12 10:13:33 2012 +0200
    10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Thu Apr 12 11:01:15 2012 +0200
    10.3 @@ -522,7 +522,7 @@
    10.4            Op1 (Converse, range_type T, Any, sub t1)
    10.5          | (Const (@{const_name trancl}, T), [t1]) =>
    10.6            Op1 (Closure, range_type T, Any, sub t1)
    10.7 -        | (Const (@{const_name rel_comp}, T), [t1, t2]) =>
    10.8 +        | (Const (@{const_name relcomp}, T), [t1, t2]) =>
    10.9            Op2 (Composition, nth_range_type 2 T, Any, sub t1, sub t2)
   10.10          | (Const (x as (s as @{const_name Suc}, T)), []) =>
   10.11            if is_built_in_const thy stds x then Cst (Suc, T, Any)
    11.1 --- a/src/HOL/Transitive_Closure.thy	Thu Apr 12 10:13:33 2012 +0200
    11.2 +++ b/src/HOL/Transitive_Closure.thy	Thu Apr 12 11:01:15 2012 +0200
    11.3 @@ -726,7 +726,7 @@
    11.4  lemma relpowp_relpow_eq [pred_set_conv]:
    11.5    fixes R :: "'a rel"
    11.6    shows "(\<lambda>x y. (x, y) \<in> R) ^^ n = (\<lambda>x y. (x, y) \<in> R ^^ n)"
    11.7 -  by (induct n) (simp_all add: rel_compp_rel_comp_eq)
    11.8 +  by (induct n) (simp_all add: relcompp_relcomp_eq)
    11.9  
   11.10  text {* for code generation *}
   11.11  
   11.12 @@ -849,7 +849,7 @@
   11.13     apply (drule tranclD2)
   11.14     apply (clarsimp simp: rtrancl_is_UN_relpow)
   11.15     apply (rule_tac x="Suc n" in exI)
   11.16 -   apply (clarsimp simp: rel_comp_unfold)
   11.17 +   apply (clarsimp simp: relcomp_unfold)
   11.18     apply fastforce
   11.19    apply clarsimp
   11.20    apply (case_tac n, simp)
   11.21 @@ -870,7 +870,7 @@
   11.22  next
   11.23    case (Suc n)
   11.24    show ?case
   11.25 -  proof (simp add: rel_comp_unfold Suc)
   11.26 +  proof (simp add: relcomp_unfold Suc)
   11.27      show "(\<exists>y. (\<exists>f. f 0 = a \<and> f n = y \<and> (\<forall>i<n. (f i,f(Suc i)) \<in> R)) \<and> (y,b) \<in> R)
   11.28       = (\<exists>f. f 0 = a \<and> f(Suc n) = b \<and> (\<forall>i<Suc n. (f i, f (Suc i)) \<in> R))"
   11.29      (is "?l = ?r")
   11.30 @@ -979,7 +979,7 @@
   11.31  apply(auto dest: relpow_finite_bounded1)
   11.32  done
   11.33  
   11.34 -lemma finite_rel_comp[simp,intro]:
   11.35 +lemma finite_relcomp[simp,intro]:
   11.36  assumes "finite R" and "finite S"
   11.37  shows "finite(R O S)"
   11.38  proof-
    12.1 --- a/src/HOL/Wellfounded.thy	Thu Apr 12 10:13:33 2012 +0200
    12.2 +++ b/src/HOL/Wellfounded.thy	Thu Apr 12 11:01:15 2012 +0200
    12.3 @@ -271,7 +271,7 @@
    12.4        assume "y \<in> Q"
    12.5        with `y \<notin> ?Q'` 
    12.6        obtain w where "(w, y) \<in> R" and "w \<in> Q" by auto
    12.7 -      from `(w, y) \<in> R` `(y, z) \<in> S` have "(w, z) \<in> R O S" by (rule rel_compI)
    12.8 +      from `(w, y) \<in> R` `(y, z) \<in> S` have "(w, z) \<in> R O S" by (rule relcompI)
    12.9        with `R O S \<subseteq> R` have "(w, z) \<in> R" ..
   12.10        with `z \<in> ?Q'` have "w \<notin> Q" by blast 
   12.11        with `w \<in> Q` show False by contradiction
    13.1 --- a/src/HOL/ex/Coherent.thy	Thu Apr 12 10:13:33 2012 +0200
    13.2 +++ b/src/HOL/ex/Coherent.thy	Thu Apr 12 11:01:15 2012 +0200
    13.3 @@ -13,7 +13,7 @@
    13.4  
    13.5  no_notation
    13.6    comp (infixl "o" 55) and
    13.7 -  rel_comp (infixr "O" 75)
    13.8 +  relcomp (infixr "O" 75)
    13.9  
   13.10  lemma p1p2:
   13.11    assumes
    14.1 --- a/src/HOL/ex/Executable_Relation.thy	Thu Apr 12 10:13:33 2012 +0200
    14.2 +++ b/src/HOL/ex/Executable_Relation.thy	Thu Apr 12 11:01:15 2012 +0200
    14.3 @@ -27,7 +27,7 @@
    14.4  
    14.5  lemma comp_Id_on:
    14.6    "Id_on X O R = Set.project (%(x, y). x : X) R"
    14.7 -by (auto intro!: rel_compI)
    14.8 +by (auto intro!: relcompI)
    14.9  
   14.10  lemma comp_Id_on':
   14.11    "R O Id_on X = Set.project (%(x, y). y : X) R"
   14.12 @@ -37,7 +37,7 @@
   14.13    "Set.project (%(x, y). x : X) (Id_on Y) = Id_on (X Int Y)"
   14.14  by auto
   14.15  
   14.16 -lemma rel_comp_raw:
   14.17 +lemma relcomp_raw:
   14.18    "(rel_raw X R) O (rel_raw Y S) = rel_raw (X Int Y) (Set.project (%(x, y). y : Y) R Un (Set.project (%(x, y). x : X) S Un R O S))"
   14.19  unfolding rel_raw_def
   14.20  apply simp
   14.21 @@ -79,7 +79,7 @@
   14.22  
   14.23  subsubsection {* Constant definitions on relations *}
   14.24  
   14.25 -hide_const (open) converse rel_comp rtrancl Image
   14.26 +hide_const (open) converse relcomp rtrancl Image
   14.27  
   14.28  quotient_definition member :: "'a * 'a => 'a rel => bool" where
   14.29    "member" is "Set.member :: 'a * 'a => ('a * 'a) set => bool" done
   14.30 @@ -92,9 +92,9 @@
   14.31  where
   14.32    "union" is "Set.union :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" done
   14.33  
   14.34 -quotient_definition rel_comp :: "'a rel => 'a rel => 'a rel"
   14.35 +quotient_definition relcomp :: "'a rel => 'a rel => 'a rel"
   14.36  where
   14.37 -  "rel_comp" is "Relation.rel_comp :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" done
   14.38 +  "relcomp" is "Relation.relcomp :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" done
   14.39  
   14.40  quotient_definition rtrancl :: "'a rel => 'a rel"
   14.41  where
   14.42 @@ -121,8 +121,8 @@
   14.43  by (lifting union_raw)
   14.44  
   14.45  lemma [code]:
   14.46 -   "rel_comp (rel X R) (rel Y S) = rel (X Int Y) (Set.project (%(x, y). y : Y) R Un (Set.project (%(x, y). x : X) S Un R O S))"
   14.47 -by (lifting rel_comp_raw)
   14.48 +   "relcomp (rel X R) (rel Y S) = rel (X Int Y) (Set.project (%(x, y). y : Y) R Un (Set.project (%(x, y). x : X) S Un R O S))"
   14.49 +by (lifting relcomp_raw)
   14.50  
   14.51  lemma [code]:
   14.52    "rtrancl (rel X R) = rel UNIV (R^+)"