renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
authorgriff
Tue Apr 03 17:26:30 2012 +0900 (2012-04-03)
changeset 4743307f4bf913230
parent 47306 56d72c923281
child 47434 b75ce48a93ee
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
src/HOL/List.thy
src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
src/HOL/Relation.thy
src/HOL/Tools/Function/termination.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
src/HOL/Tools/Nitpick/nitpick_nut.ML
src/HOL/Transitive_Closure.thy
src/HOL/Wellfounded.thy
src/HOL/ex/Coherent.thy
src/HOL/ex/Executable_Relation.thy
     1.1 --- a/src/HOL/List.thy	Tue Apr 03 08:55:06 2012 +0200
     1.2 +++ b/src/HOL/List.thy	Tue Apr 03 17:26:30 2012 +0900
     1.3 @@ -5747,7 +5747,7 @@
     1.4    "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)"
     1.5    by (simp add: finite_trancl_ntranl)
     1.6  
     1.7 -lemma set_rel_comp [code]:
     1.8 +lemma set_relcomp [code]:
     1.9    "set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
    1.10    by (auto simp add: Bex_def)
    1.11  
     2.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Tue Apr 03 08:55:06 2012 +0200
     2.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Tue Apr 03 17:26:30 2012 +0900
     2.3 @@ -1027,8 +1027,8 @@
     2.4    (o * o => bool) => i * i => bool) [inductify] converse .
     2.5  
     2.6  thm converse.equation
     2.7 -code_pred [inductify] rel_comp .
     2.8 -thm rel_comp.equation
     2.9 +code_pred [inductify] relcomp .
    2.10 +thm relcomp.equation
    2.11  code_pred [inductify] Image .
    2.12  thm Image.equation
    2.13  declare singleton_iff[code_pred_inline]
     3.1 --- a/src/HOL/Relation.thy	Tue Apr 03 08:55:06 2012 +0200
     3.2 +++ b/src/HOL/Relation.thy	Tue Apr 03 17:26:30 2012 +0900
     3.3 @@ -507,29 +507,29 @@
     3.4  
     3.5  subsubsection {* Composition *}
     3.6  
     3.7 -inductive_set rel_comp  :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'c) set \<Rightarrow> ('a \<times> 'c) set" (infixr "O" 75)
     3.8 +inductive_set relcomp  :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'c) set \<Rightarrow> ('a \<times> 'c) set" (infixr "O" 75)
     3.9    for r :: "('a \<times> 'b) set" and s :: "('b \<times> 'c) set"
    3.10  where
    3.11 -  rel_compI [intro]: "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> s \<Longrightarrow> (a, c) \<in> r O s"
    3.12 +  relcompI [intro]: "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> s \<Longrightarrow> (a, c) \<in> r O s"
    3.13  
    3.14  abbreviation pred_comp (infixr "OO" 75) where
    3.15 -  "pred_comp \<equiv> rel_compp"
    3.16 +  "pred_comp \<equiv> relcompp"
    3.17  
    3.18 -lemmas pred_compI = rel_compp.intros
    3.19 +lemmas pred_compI = relcompp.intros
    3.20  
    3.21  text {*
    3.22    For historic reasons, the elimination rules are not wholly corresponding.
    3.23    Feel free to consolidate this.
    3.24  *}
    3.25  
    3.26 -inductive_cases rel_compEpair: "(a, c) \<in> r O s"
    3.27 +inductive_cases relcompEpair: "(a, c) \<in> r O s"
    3.28  inductive_cases pred_compE [elim!]: "(r OO s) a c"
    3.29  
    3.30 -lemma rel_compE [elim!]: "xz \<in> r O s \<Longrightarrow>
    3.31 +lemma relcompE [elim!]: "xz \<in> r O s \<Longrightarrow>
    3.32    (\<And>x y z. xz = (x, z) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, z) \<in> s  \<Longrightarrow> P) \<Longrightarrow> P"
    3.33 -  by (cases xz) (simp, erule rel_compEpair, iprover)
    3.34 +  by (cases xz) (simp, erule relcompEpair, iprover)
    3.35  
    3.36 -lemmas pred_comp_rel_comp_eq = rel_compp_rel_comp_eq
    3.37 +lemmas pred_comp_relcomp_eq = relcompp_relcomp_eq
    3.38  
    3.39  lemma R_O_Id [simp]:
    3.40    "R O Id = R"
    3.41 @@ -539,21 +539,21 @@
    3.42    "Id O R = R"
    3.43    by fast
    3.44  
    3.45 -lemma rel_comp_empty1 [simp]:
    3.46 +lemma relcomp_empty1 [simp]:
    3.47    "{} O R = {}"
    3.48    by blast
    3.49  
    3.50  lemma pred_comp_bot1 [simp]:
    3.51    "\<bottom> OO R = \<bottom>"
    3.52 -  by (fact rel_comp_empty1 [to_pred])
    3.53 +  by (fact relcomp_empty1 [to_pred])
    3.54  
    3.55 -lemma rel_comp_empty2 [simp]:
    3.56 +lemma relcomp_empty2 [simp]:
    3.57    "R O {} = {}"
    3.58    by blast
    3.59  
    3.60  lemma pred_comp_bot2 [simp]:
    3.61    "R OO \<bottom> = \<bottom>"
    3.62 -  by (fact rel_comp_empty2 [to_pred])
    3.63 +  by (fact relcomp_empty2 [to_pred])
    3.64  
    3.65  lemma O_assoc:
    3.66    "(R O S) O T = R O (S O T)"
    3.67 @@ -572,51 +572,51 @@
    3.68    "transp r \<Longrightarrow> r OO r \<le> r "
    3.69    by (fact trans_O_subset [to_pred])
    3.70  
    3.71 -lemma rel_comp_mono:
    3.72 +lemma relcomp_mono:
    3.73    "r' \<subseteq> r \<Longrightarrow> s' \<subseteq> s \<Longrightarrow> r' O s' \<subseteq> r O s"
    3.74    by blast
    3.75  
    3.76  lemma pred_comp_mono:
    3.77    "r' \<le> r \<Longrightarrow> s' \<le> s \<Longrightarrow> r' OO s' \<le> r OO s "
    3.78 -  by (fact rel_comp_mono [to_pred])
    3.79 +  by (fact relcomp_mono [to_pred])
    3.80  
    3.81 -lemma rel_comp_subset_Sigma:
    3.82 +lemma relcomp_subset_Sigma:
    3.83    "r \<subseteq> A \<times> B \<Longrightarrow> s \<subseteq> B \<times> C \<Longrightarrow> r O s \<subseteq> A \<times> C"
    3.84    by blast
    3.85  
    3.86 -lemma rel_comp_distrib [simp]:
    3.87 +lemma relcomp_distrib [simp]:
    3.88    "R O (S \<union> T) = (R O S) \<union> (R O T)" 
    3.89    by auto
    3.90  
    3.91  lemma pred_comp_distrib [simp]:
    3.92    "R OO (S \<squnion> T) = R OO S \<squnion> R OO T"
    3.93 -  by (fact rel_comp_distrib [to_pred])
    3.94 +  by (fact relcomp_distrib [to_pred])
    3.95  
    3.96 -lemma rel_comp_distrib2 [simp]:
    3.97 +lemma relcomp_distrib2 [simp]:
    3.98    "(S \<union> T) O R = (S O R) \<union> (T O R)"
    3.99    by auto
   3.100  
   3.101  lemma pred_comp_distrib2 [simp]:
   3.102    "(S \<squnion> T) OO R = S OO R \<squnion> T OO R"
   3.103 -  by (fact rel_comp_distrib2 [to_pred])
   3.104 +  by (fact relcomp_distrib2 [to_pred])
   3.105  
   3.106 -lemma rel_comp_UNION_distrib:
   3.107 +lemma relcomp_UNION_distrib:
   3.108    "s O UNION I r = (\<Union>i\<in>I. s O r i) "
   3.109    by auto
   3.110  
   3.111 -(* FIXME thm rel_comp_UNION_distrib [to_pred] *)
   3.112 +(* FIXME thm relcomp_UNION_distrib [to_pred] *)
   3.113  
   3.114 -lemma rel_comp_UNION_distrib2:
   3.115 +lemma relcomp_UNION_distrib2:
   3.116    "UNION I r O s = (\<Union>i\<in>I. r i O s) "
   3.117    by auto
   3.118  
   3.119 -(* FIXME thm rel_comp_UNION_distrib2 [to_pred] *)
   3.120 +(* FIXME thm relcomp_UNION_distrib2 [to_pred] *)
   3.121  
   3.122 -lemma single_valued_rel_comp:
   3.123 +lemma single_valued_relcomp:
   3.124    "single_valued r \<Longrightarrow> single_valued s \<Longrightarrow> single_valued (r O s)"
   3.125    by (unfold single_valued_def) blast
   3.126  
   3.127 -lemma rel_comp_unfold:
   3.128 +lemma relcomp_unfold:
   3.129    "r O s = {(x, z). \<exists>y. (x, y) \<in> r \<and> (y, z) \<in> s}"
   3.130    by (auto simp add: set_eq_iff)
   3.131  
   3.132 @@ -676,7 +676,7 @@
   3.133    "(r\<inverse>\<inverse>)\<inverse>\<inverse> = r"
   3.134    by (fact converse_converse [to_pred])
   3.135  
   3.136 -lemma converse_rel_comp: "(r O s)^-1 = s^-1 O r^-1"
   3.137 +lemma converse_relcomp: "(r O s)^-1 = s^-1 O r^-1"
   3.138    by blast
   3.139  
   3.140  lemma converse_pred_comp: "(r OO s)^--1 = s^--1 OO r^--1"
     4.1 --- a/src/HOL/Tools/Function/termination.ML	Tue Apr 03 08:55:06 2012 +0200
     4.2 +++ b/src/HOL/Tools/Function/termination.ML	Tue Apr 03 17:26:30 2012 +0900
     4.3 @@ -141,7 +141,7 @@
     4.4  fun prove_chain thy chain_tac (c1, c2) =
     4.5    let
     4.6      val goal =
     4.7 -      HOLogic.mk_eq (HOLogic.mk_binop @{const_name Relation.rel_comp} (c1, c2),
     4.8 +      HOLogic.mk_eq (HOLogic.mk_binop @{const_name Relation.relcomp} (c1, c2),
     4.9          Const (@{const_abbrev Set.empty}, fastype_of c1))
    4.10        |> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *)
    4.11    in
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Apr 03 08:55:06 2012 +0200
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Apr 03 17:26:30 2012 +0900
     5.3 @@ -391,7 +391,7 @@
     5.4     (@{const_name Id}, 0),
     5.5     (@{const_name converse}, 1),
     5.6     (@{const_name trancl}, 1),
     5.7 -   (@{const_name rel_comp}, 2),
     5.8 +   (@{const_name relcomp}, 2),
     5.9     (@{const_name finite}, 1),
    5.10     (@{const_name unknown}, 0),
    5.11     (@{const_name is_unknown}, 1),
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Apr 03 08:55:06 2012 +0200
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Apr 03 17:26:30 2012 +0900
     6.3 @@ -856,7 +856,7 @@
     6.4                   accum ||> add_annotation_atom_comp Neq [] (V x) (A New))
     6.5                end
     6.6              | @{const_name trancl} => do_fragile_set_operation T accum
     6.7 -            | @{const_name rel_comp} =>
     6.8 +            | @{const_name relcomp} =>
     6.9                let
    6.10                  val x = Unsynchronized.inc max_fresh
    6.11                  val bc_set_M = domain_type T |> mtype_for_set x
     7.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Apr 03 08:55:06 2012 +0200
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Apr 03 17:26:30 2012 +0900
     7.3 @@ -522,7 +522,7 @@
     7.4            Op1 (Converse, range_type T, Any, sub t1)
     7.5          | (Const (@{const_name trancl}, T), [t1]) =>
     7.6            Op1 (Closure, range_type T, Any, sub t1)
     7.7 -        | (Const (@{const_name rel_comp}, T), [t1, t2]) =>
     7.8 +        | (Const (@{const_name relcomp}, T), [t1, t2]) =>
     7.9            Op2 (Composition, nth_range_type 2 T, Any, sub t1, sub t2)
    7.10          | (Const (x as (s as @{const_name Suc}, T)), []) =>
    7.11            if is_built_in_const thy stds x then Cst (Suc, T, Any)
     8.1 --- a/src/HOL/Transitive_Closure.thy	Tue Apr 03 08:55:06 2012 +0200
     8.2 +++ b/src/HOL/Transitive_Closure.thy	Tue Apr 03 17:26:30 2012 +0900
     8.3 @@ -726,7 +726,7 @@
     8.4  lemma relpowp_relpow_eq [pred_set_conv]:
     8.5    fixes R :: "'a rel"
     8.6    shows "(\<lambda>x y. (x, y) \<in> R) ^^ n = (\<lambda>x y. (x, y) \<in> R ^^ n)"
     8.7 -  by (induct n) (simp_all add: rel_compp_rel_comp_eq)
     8.8 +  by (induct n) (simp_all add: relcompp_relcomp_eq)
     8.9  
    8.10  text {* for code generation *}
    8.11  
    8.12 @@ -849,7 +849,7 @@
    8.13     apply (drule tranclD2)
    8.14     apply (clarsimp simp: rtrancl_is_UN_relpow)
    8.15     apply (rule_tac x="Suc n" in exI)
    8.16 -   apply (clarsimp simp: rel_comp_unfold)
    8.17 +   apply (clarsimp simp: relcomp_unfold)
    8.18     apply fastforce
    8.19    apply clarsimp
    8.20    apply (case_tac n, simp)
    8.21 @@ -870,7 +870,7 @@
    8.22  next
    8.23    case (Suc n)
    8.24    show ?case
    8.25 -  proof (simp add: rel_comp_unfold Suc)
    8.26 +  proof (simp add: relcomp_unfold Suc)
    8.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)
    8.28       = (\<exists>f. f 0 = a \<and> f(Suc n) = b \<and> (\<forall>i<Suc n. (f i, f (Suc i)) \<in> R))"
    8.29      (is "?l = ?r")
    8.30 @@ -979,7 +979,7 @@
    8.31  apply(auto dest: relpow_finite_bounded1)
    8.32  done
    8.33  
    8.34 -lemma finite_rel_comp[simp,intro]:
    8.35 +lemma finite_relcomp[simp,intro]:
    8.36  assumes "finite R" and "finite S"
    8.37  shows "finite(R O S)"
    8.38  proof-
     9.1 --- a/src/HOL/Wellfounded.thy	Tue Apr 03 08:55:06 2012 +0200
     9.2 +++ b/src/HOL/Wellfounded.thy	Tue Apr 03 17:26:30 2012 +0900
     9.3 @@ -271,7 +271,7 @@
     9.4        assume "y \<in> Q"
     9.5        with `y \<notin> ?Q'` 
     9.6        obtain w where "(w, y) \<in> R" and "w \<in> Q" by auto
     9.7 -      from `(w, y) \<in> R` `(y, z) \<in> S` have "(w, z) \<in> R O S" by (rule rel_compI)
     9.8 +      from `(w, y) \<in> R` `(y, z) \<in> S` have "(w, z) \<in> R O S" by (rule relcompI)
     9.9        with `R O S \<subseteq> R` have "(w, z) \<in> R" ..
    9.10        with `z \<in> ?Q'` have "w \<notin> Q" by blast 
    9.11        with `w \<in> Q` show False by contradiction
    10.1 --- a/src/HOL/ex/Coherent.thy	Tue Apr 03 08:55:06 2012 +0200
    10.2 +++ b/src/HOL/ex/Coherent.thy	Tue Apr 03 17:26:30 2012 +0900
    10.3 @@ -13,7 +13,7 @@
    10.4  
    10.5  no_notation
    10.6    comp (infixl "o" 55) and
    10.7 -  rel_comp (infixr "O" 75)
    10.8 +  relcomp (infixr "O" 75)
    10.9  
   10.10  lemma p1p2:
   10.11    assumes
    11.1 --- a/src/HOL/ex/Executable_Relation.thy	Tue Apr 03 08:55:06 2012 +0200
    11.2 +++ b/src/HOL/ex/Executable_Relation.thy	Tue Apr 03 17:26:30 2012 +0900
    11.3 @@ -27,7 +27,7 @@
    11.4  
    11.5  lemma comp_Id_on:
    11.6    "Id_on X O R = Set.project (%(x, y). x : X) R"
    11.7 -by (auto intro!: rel_compI)
    11.8 +by (auto intro!: relcompI)
    11.9  
   11.10  lemma comp_Id_on':
   11.11    "R O Id_on X = Set.project (%(x, y). y : X) R"
   11.12 @@ -37,7 +37,7 @@
   11.13    "Set.project (%(x, y). x : X) (Id_on Y) = Id_on (X Int Y)"
   11.14  by auto
   11.15  
   11.16 -lemma rel_comp_raw:
   11.17 +lemma relcomp_raw:
   11.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))"
   11.19  unfolding rel_raw_def
   11.20  apply simp
   11.21 @@ -79,7 +79,7 @@
   11.22  
   11.23  subsubsection {* Constant definitions on relations *}
   11.24  
   11.25 -hide_const (open) converse rel_comp rtrancl Image
   11.26 +hide_const (open) converse relcomp rtrancl Image
   11.27  
   11.28  quotient_definition member :: "'a * 'a => 'a rel => bool" where
   11.29    "member" is "Set.member :: 'a * 'a => ('a * 'a) set => bool" done
   11.30 @@ -92,9 +92,9 @@
   11.31  where
   11.32    "union" is "Set.union :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" done
   11.33  
   11.34 -quotient_definition rel_comp :: "'a rel => 'a rel => 'a rel"
   11.35 +quotient_definition relcomp :: "'a rel => 'a rel => 'a rel"
   11.36  where
   11.37 -  "rel_comp" is "Relation.rel_comp :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" done
   11.38 +  "relcomp" is "Relation.relcomp :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" done
   11.39  
   11.40  quotient_definition rtrancl :: "'a rel => 'a rel"
   11.41  where
   11.42 @@ -121,8 +121,8 @@
   11.43  by (lifting union_raw)
   11.44  
   11.45  lemma [code]:
   11.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))"
   11.47 -by (lifting rel_comp_raw)
   11.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))"
   11.49 +by (lifting relcomp_raw)
   11.50  
   11.51  lemma [code]:
   11.52    "rtrancl (rel X R) = rel UNIV (R^+)"