# HG changeset patch
# User griff
# Date 1333441590 -32400
# Node ID 07f4bf913230f9797c0183b09ea176fbc520b4c8
# Parent  56d72c9232818ef63acb9c555cef83c8cd3a9a27
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")

diff -r 56d72c923281 -r 07f4bf913230 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Apr 03 08:55:06 2012 +0200
+++ b/src/HOL/List.thy	Tue Apr 03 17:26:30 2012 +0900
@@ -5747,7 +5747,7 @@
   "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)"
   by (simp add: finite_trancl_ntranl)
 
-lemma set_rel_comp [code]:
+lemma set_relcomp [code]:
   "set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
   by (auto simp add: Bex_def)
 
diff -r 56d72c923281 -r 07f4bf913230 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Tue Apr 03 08:55:06 2012 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Tue Apr 03 17:26:30 2012 +0900
@@ -1027,8 +1027,8 @@
   (o * o => bool) => i * i => bool) [inductify] converse .
 
 thm converse.equation
-code_pred [inductify] rel_comp .
-thm rel_comp.equation
+code_pred [inductify] relcomp .
+thm relcomp.equation
 code_pred [inductify] Image .
 thm Image.equation
 declare singleton_iff[code_pred_inline]
diff -r 56d72c923281 -r 07f4bf913230 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Tue Apr 03 08:55:06 2012 +0200
+++ b/src/HOL/Relation.thy	Tue Apr 03 17:26:30 2012 +0900
@@ -507,29 +507,29 @@
 
 subsubsection {* Composition *}
 
-inductive_set rel_comp  :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'c) set \<Rightarrow> ('a \<times> 'c) set" (infixr "O" 75)
+inductive_set relcomp  :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'c) set \<Rightarrow> ('a \<times> 'c) set" (infixr "O" 75)
   for r :: "('a \<times> 'b) set" and s :: "('b \<times> 'c) set"
 where
-  rel_compI [intro]: "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> s \<Longrightarrow> (a, c) \<in> r O s"
+  relcompI [intro]: "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> s \<Longrightarrow> (a, c) \<in> r O s"
 
 abbreviation pred_comp (infixr "OO" 75) where
-  "pred_comp \<equiv> rel_compp"
+  "pred_comp \<equiv> relcompp"
 
-lemmas pred_compI = rel_compp.intros
+lemmas pred_compI = relcompp.intros
 
 text {*
   For historic reasons, the elimination rules are not wholly corresponding.
   Feel free to consolidate this.
 *}
 
-inductive_cases rel_compEpair: "(a, c) \<in> r O s"
+inductive_cases relcompEpair: "(a, c) \<in> r O s"
 inductive_cases pred_compE [elim!]: "(r OO s) a c"
 
-lemma rel_compE [elim!]: "xz \<in> r O s \<Longrightarrow>
+lemma relcompE [elim!]: "xz \<in> r O s \<Longrightarrow>
   (\<And>x y z. xz = (x, z) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, z) \<in> s  \<Longrightarrow> P) \<Longrightarrow> P"
-  by (cases xz) (simp, erule rel_compEpair, iprover)
+  by (cases xz) (simp, erule relcompEpair, iprover)
 
-lemmas pred_comp_rel_comp_eq = rel_compp_rel_comp_eq
+lemmas pred_comp_relcomp_eq = relcompp_relcomp_eq
 
 lemma R_O_Id [simp]:
   "R O Id = R"
@@ -539,21 +539,21 @@
   "Id O R = R"
   by fast
 
-lemma rel_comp_empty1 [simp]:
+lemma relcomp_empty1 [simp]:
   "{} O R = {}"
   by blast
 
 lemma pred_comp_bot1 [simp]:
   "\<bottom> OO R = \<bottom>"
-  by (fact rel_comp_empty1 [to_pred])
+  by (fact relcomp_empty1 [to_pred])
 
-lemma rel_comp_empty2 [simp]:
+lemma relcomp_empty2 [simp]:
   "R O {} = {}"
   by blast
 
 lemma pred_comp_bot2 [simp]:
   "R OO \<bottom> = \<bottom>"
-  by (fact rel_comp_empty2 [to_pred])
+  by (fact relcomp_empty2 [to_pred])
 
 lemma O_assoc:
   "(R O S) O T = R O (S O T)"
@@ -572,51 +572,51 @@
   "transp r \<Longrightarrow> r OO r \<le> r "
   by (fact trans_O_subset [to_pred])
 
-lemma rel_comp_mono:
+lemma relcomp_mono:
   "r' \<subseteq> r \<Longrightarrow> s' \<subseteq> s \<Longrightarrow> r' O s' \<subseteq> r O s"
   by blast
 
 lemma pred_comp_mono:
   "r' \<le> r \<Longrightarrow> s' \<le> s \<Longrightarrow> r' OO s' \<le> r OO s "
-  by (fact rel_comp_mono [to_pred])
+  by (fact relcomp_mono [to_pred])
 
-lemma rel_comp_subset_Sigma:
+lemma relcomp_subset_Sigma:
   "r \<subseteq> A \<times> B \<Longrightarrow> s \<subseteq> B \<times> C \<Longrightarrow> r O s \<subseteq> A \<times> C"
   by blast
 
-lemma rel_comp_distrib [simp]:
+lemma relcomp_distrib [simp]:
   "R O (S \<union> T) = (R O S) \<union> (R O T)" 
   by auto
 
 lemma pred_comp_distrib [simp]:
   "R OO (S \<squnion> T) = R OO S \<squnion> R OO T"
-  by (fact rel_comp_distrib [to_pred])
+  by (fact relcomp_distrib [to_pred])
 
-lemma rel_comp_distrib2 [simp]:
+lemma relcomp_distrib2 [simp]:
   "(S \<union> T) O R = (S O R) \<union> (T O R)"
   by auto
 
 lemma pred_comp_distrib2 [simp]:
   "(S \<squnion> T) OO R = S OO R \<squnion> T OO R"
-  by (fact rel_comp_distrib2 [to_pred])
+  by (fact relcomp_distrib2 [to_pred])
 
-lemma rel_comp_UNION_distrib:
+lemma relcomp_UNION_distrib:
   "s O UNION I r = (\<Union>i\<in>I. s O r i) "
   by auto
 
-(* FIXME thm rel_comp_UNION_distrib [to_pred] *)
+(* FIXME thm relcomp_UNION_distrib [to_pred] *)
 
-lemma rel_comp_UNION_distrib2:
+lemma relcomp_UNION_distrib2:
   "UNION I r O s = (\<Union>i\<in>I. r i O s) "
   by auto
 
-(* FIXME thm rel_comp_UNION_distrib2 [to_pred] *)
+(* FIXME thm relcomp_UNION_distrib2 [to_pred] *)
 
-lemma single_valued_rel_comp:
+lemma single_valued_relcomp:
   "single_valued r \<Longrightarrow> single_valued s \<Longrightarrow> single_valued (r O s)"
   by (unfold single_valued_def) blast
 
-lemma rel_comp_unfold:
+lemma relcomp_unfold:
   "r O s = {(x, z). \<exists>y. (x, y) \<in> r \<and> (y, z) \<in> s}"
   by (auto simp add: set_eq_iff)
 
@@ -676,7 +676,7 @@
   "(r\<inverse>\<inverse>)\<inverse>\<inverse> = r"
   by (fact converse_converse [to_pred])
 
-lemma converse_rel_comp: "(r O s)^-1 = s^-1 O r^-1"
+lemma converse_relcomp: "(r O s)^-1 = s^-1 O r^-1"
   by blast
 
 lemma converse_pred_comp: "(r OO s)^--1 = s^--1 OO r^--1"
diff -r 56d72c923281 -r 07f4bf913230 src/HOL/Tools/Function/termination.ML
--- a/src/HOL/Tools/Function/termination.ML	Tue Apr 03 08:55:06 2012 +0200
+++ b/src/HOL/Tools/Function/termination.ML	Tue Apr 03 17:26:30 2012 +0900
@@ -141,7 +141,7 @@
 fun prove_chain thy chain_tac (c1, c2) =
   let
     val goal =
-      HOLogic.mk_eq (HOLogic.mk_binop @{const_name Relation.rel_comp} (c1, c2),
+      HOLogic.mk_eq (HOLogic.mk_binop @{const_name Relation.relcomp} (c1, c2),
         Const (@{const_abbrev Set.empty}, fastype_of c1))
       |> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *)
   in
diff -r 56d72c923281 -r 07f4bf913230 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Apr 03 08:55:06 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Apr 03 17:26:30 2012 +0900
@@ -391,7 +391,7 @@
    (@{const_name Id}, 0),
    (@{const_name converse}, 1),
    (@{const_name trancl}, 1),
-   (@{const_name rel_comp}, 2),
+   (@{const_name relcomp}, 2),
    (@{const_name finite}, 1),
    (@{const_name unknown}, 0),
    (@{const_name is_unknown}, 1),
diff -r 56d72c923281 -r 07f4bf913230 src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Apr 03 08:55:06 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Apr 03 17:26:30 2012 +0900
@@ -856,7 +856,7 @@
                  accum ||> add_annotation_atom_comp Neq [] (V x) (A New))
               end
             | @{const_name trancl} => do_fragile_set_operation T accum
-            | @{const_name rel_comp} =>
+            | @{const_name relcomp} =>
               let
                 val x = Unsynchronized.inc max_fresh
                 val bc_set_M = domain_type T |> mtype_for_set x
diff -r 56d72c923281 -r 07f4bf913230 src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Apr 03 08:55:06 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Apr 03 17:26:30 2012 +0900
@@ -522,7 +522,7 @@
           Op1 (Converse, range_type T, Any, sub t1)
         | (Const (@{const_name trancl}, T), [t1]) =>
           Op1 (Closure, range_type T, Any, sub t1)
-        | (Const (@{const_name rel_comp}, T), [t1, t2]) =>
+        | (Const (@{const_name relcomp}, T), [t1, t2]) =>
           Op2 (Composition, nth_range_type 2 T, Any, sub t1, sub t2)
         | (Const (x as (s as @{const_name Suc}, T)), []) =>
           if is_built_in_const thy stds x then Cst (Suc, T, Any)
diff -r 56d72c923281 -r 07f4bf913230 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Tue Apr 03 08:55:06 2012 +0200
+++ b/src/HOL/Transitive_Closure.thy	Tue Apr 03 17:26:30 2012 +0900
@@ -726,7 +726,7 @@
 lemma relpowp_relpow_eq [pred_set_conv]:
   fixes R :: "'a rel"
   shows "(\<lambda>x y. (x, y) \<in> R) ^^ n = (\<lambda>x y. (x, y) \<in> R ^^ n)"
-  by (induct n) (simp_all add: rel_compp_rel_comp_eq)
+  by (induct n) (simp_all add: relcompp_relcomp_eq)
 
 text {* for code generation *}
 
@@ -849,7 +849,7 @@
    apply (drule tranclD2)
    apply (clarsimp simp: rtrancl_is_UN_relpow)
    apply (rule_tac x="Suc n" in exI)
-   apply (clarsimp simp: rel_comp_unfold)
+   apply (clarsimp simp: relcomp_unfold)
    apply fastforce
   apply clarsimp
   apply (case_tac n, simp)
@@ -870,7 +870,7 @@
 next
   case (Suc n)
   show ?case
-  proof (simp add: rel_comp_unfold Suc)
+  proof (simp add: relcomp_unfold Suc)
     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)
      = (\<exists>f. f 0 = a \<and> f(Suc n) = b \<and> (\<forall>i<Suc n. (f i, f (Suc i)) \<in> R))"
     (is "?l = ?r")
@@ -979,7 +979,7 @@
 apply(auto dest: relpow_finite_bounded1)
 done
 
-lemma finite_rel_comp[simp,intro]:
+lemma finite_relcomp[simp,intro]:
 assumes "finite R" and "finite S"
 shows "finite(R O S)"
 proof-
diff -r 56d72c923281 -r 07f4bf913230 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Tue Apr 03 08:55:06 2012 +0200
+++ b/src/HOL/Wellfounded.thy	Tue Apr 03 17:26:30 2012 +0900
@@ -271,7 +271,7 @@
       assume "y \<in> Q"
       with `y \<notin> ?Q'` 
       obtain w where "(w, y) \<in> R" and "w \<in> Q" by auto
-      from `(w, y) \<in> R` `(y, z) \<in> S` have "(w, z) \<in> R O S" by (rule rel_compI)
+      from `(w, y) \<in> R` `(y, z) \<in> S` have "(w, z) \<in> R O S" by (rule relcompI)
       with `R O S \<subseteq> R` have "(w, z) \<in> R" ..
       with `z \<in> ?Q'` have "w \<notin> Q" by blast 
       with `w \<in> Q` show False by contradiction
diff -r 56d72c923281 -r 07f4bf913230 src/HOL/ex/Coherent.thy
--- a/src/HOL/ex/Coherent.thy	Tue Apr 03 08:55:06 2012 +0200
+++ b/src/HOL/ex/Coherent.thy	Tue Apr 03 17:26:30 2012 +0900
@@ -13,7 +13,7 @@
 
 no_notation
   comp (infixl "o" 55) and
-  rel_comp (infixr "O" 75)
+  relcomp (infixr "O" 75)
 
 lemma p1p2:
   assumes
diff -r 56d72c923281 -r 07f4bf913230 src/HOL/ex/Executable_Relation.thy
--- a/src/HOL/ex/Executable_Relation.thy	Tue Apr 03 08:55:06 2012 +0200
+++ b/src/HOL/ex/Executable_Relation.thy	Tue Apr 03 17:26:30 2012 +0900
@@ -27,7 +27,7 @@
 
 lemma comp_Id_on:
   "Id_on X O R = Set.project (%(x, y). x : X) R"
-by (auto intro!: rel_compI)
+by (auto intro!: relcompI)
 
 lemma comp_Id_on':
   "R O Id_on X = Set.project (%(x, y). y : X) R"
@@ -37,7 +37,7 @@
   "Set.project (%(x, y). x : X) (Id_on Y) = Id_on (X Int Y)"
 by auto
 
-lemma rel_comp_raw:
+lemma relcomp_raw:
   "(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))"
 unfolding rel_raw_def
 apply simp
@@ -79,7 +79,7 @@
 
 subsubsection {* Constant definitions on relations *}
 
-hide_const (open) converse rel_comp rtrancl Image
+hide_const (open) converse relcomp rtrancl Image
 
 quotient_definition member :: "'a * 'a => 'a rel => bool" where
   "member" is "Set.member :: 'a * 'a => ('a * 'a) set => bool" done
@@ -92,9 +92,9 @@
 where
   "union" is "Set.union :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" done
 
-quotient_definition rel_comp :: "'a rel => 'a rel => 'a rel"
+quotient_definition relcomp :: "'a rel => 'a rel => 'a rel"
 where
-  "rel_comp" is "Relation.rel_comp :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" done
+  "relcomp" is "Relation.relcomp :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" done
 
 quotient_definition rtrancl :: "'a rel => 'a rel"
 where
@@ -121,8 +121,8 @@
 by (lifting union_raw)
 
 lemma [code]:
-   "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))"
-by (lifting rel_comp_raw)
+   "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))"
+by (lifting relcomp_raw)
 
 lemma [code]:
   "rtrancl (rel X R) = rel UNIV (R^+)"