merged
authorAndreas Lochbihler
Thu Apr 12 13:47:21 2012 +0200 (2012-04-12)
changeset 4743811a0aa6cc677
parent 47437 4625ee486ff6
parent 47436 d8fad618a67a
child 47439 83294cd0e7ee
child 47443 aeff49a3369b
child 47450 2ada2be850cb
merged
     1.1 --- a/src/HOL/Library/Multiset.thy	Thu Apr 12 10:29:45 2012 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Thu Apr 12 13:47:21 2012 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4    show "(\<lambda>x. 0::nat) \<in> {f. finite {x. f x > 0}}" by simp
     1.5  qed
     1.6  
     1.7 -lemmas multiset_typedef = Abs_multiset_inverse count_inverse count
     1.8 +setup_lifting type_definition_multiset
     1.9  
    1.10  abbreviation Melem :: "'a => 'a multiset => bool"  ("(_/ :# _)" [50, 51] 50) where
    1.11    "a :# M == 0 < count M a"
    1.12 @@ -82,21 +82,21 @@
    1.13  instantiation multiset :: (type) "{zero, plus}"
    1.14  begin
    1.15  
    1.16 -definition Mempty_def:
    1.17 -  "0 = Abs_multiset (\<lambda>a. 0)"
    1.18 +lift_definition zero_multiset :: "'a multiset" is "\<lambda>a. 0"
    1.19 +by (rule const0_in_multiset)
    1.20  
    1.21  abbreviation Mempty :: "'a multiset" ("{#}") where
    1.22    "Mempty \<equiv> 0"
    1.23  
    1.24 -definition union_def:
    1.25 -  "M + N = Abs_multiset (\<lambda>a. count M a + count N a)"
    1.26 +lift_definition plus_multiset :: "'a multiset => 'a multiset => 'a multiset" is "\<lambda>M N. (\<lambda>a. M a + N a)"
    1.27 +by (rule union_preserves_multiset)
    1.28  
    1.29  instance ..
    1.30  
    1.31  end
    1.32  
    1.33 -definition single :: "'a => 'a multiset" where
    1.34 -  "single a = Abs_multiset (\<lambda>b. if b = a then 1 else 0)"
    1.35 +lift_definition single :: "'a => 'a multiset" is "\<lambda>a b. if b = a then 1 else 0"
    1.36 +by (rule only1_in_multiset)
    1.37  
    1.38  syntax
    1.39    "_multiset" :: "args => 'a multiset"    ("{#(_)#}")
    1.40 @@ -105,10 +105,10 @@
    1.41    "{#x#}" == "CONST single x"
    1.42  
    1.43  lemma count_empty [simp]: "count {#} a = 0"
    1.44 -  by (simp add: Mempty_def in_multiset multiset_typedef)
    1.45 +  by (simp add: zero_multiset.rep_eq)
    1.46  
    1.47  lemma count_single [simp]: "count {#b#} a = (if b = a then 1 else 0)"
    1.48 -  by (simp add: single_def in_multiset multiset_typedef)
    1.49 +  by (simp add: single.rep_eq)
    1.50  
    1.51  
    1.52  subsection {* Basic operations *}
    1.53 @@ -116,7 +116,7 @@
    1.54  subsubsection {* Union *}
    1.55  
    1.56  lemma count_union [simp]: "count (M + N) a = count M a + count N a"
    1.57 -  by (simp add: union_def in_multiset multiset_typedef)
    1.58 +  by (simp add: plus_multiset.rep_eq)
    1.59  
    1.60  instance multiset :: (type) cancel_comm_monoid_add
    1.61    by default (simp_all add: multiset_eq_iff)
    1.62 @@ -127,15 +127,15 @@
    1.63  instantiation multiset :: (type) minus
    1.64  begin
    1.65  
    1.66 -definition diff_def:
    1.67 -  "M - N = Abs_multiset (\<lambda>a. count M a - count N a)"
    1.68 -
    1.69 +lift_definition minus_multiset :: "'a multiset => 'a multiset => 'a multiset" is "\<lambda> M N. \<lambda>a. M a - N a"
    1.70 +by (rule diff_preserves_multiset)
    1.71 + 
    1.72  instance ..
    1.73  
    1.74  end
    1.75  
    1.76  lemma count_diff [simp]: "count (M - N) a = count M a - count N a"
    1.77 -  by (simp add: diff_def in_multiset multiset_typedef)
    1.78 +  by (simp add: minus_multiset.rep_eq)
    1.79  
    1.80  lemma diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}"
    1.81  by(simp add: multiset_eq_iff)
    1.82 @@ -264,8 +264,9 @@
    1.83  instantiation multiset :: (type) ordered_ab_semigroup_add_imp_le
    1.84  begin
    1.85  
    1.86 -definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
    1.87 -  mset_le_def: "A \<le> B \<longleftrightarrow> (\<forall>a. count A a \<le> count B a)"
    1.88 +lift_definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" is "\<lambda> A B. (\<forall>a. A a \<le> B a)"
    1.89 +by simp
    1.90 +lemmas mset_le_def = less_eq_multiset_def
    1.91  
    1.92  definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
    1.93    mset_less_def: "(A::'a multiset) < B \<longleftrightarrow> A \<le> B \<and> A \<noteq> B"
    1.94 @@ -391,7 +392,7 @@
    1.95  
    1.96  lemma multiset_inter_count [simp]:
    1.97    "count (A #\<inter> B) x = min (count A x) (count B x)"
    1.98 -  by (simp add: multiset_inter_def multiset_typedef)
    1.99 +  by (simp add: multiset_inter_def)
   1.100  
   1.101  lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}"
   1.102    by (rule multiset_eqI) auto
   1.103 @@ -414,14 +415,14 @@
   1.104  
   1.105  text {* Multiset comprehension *}
   1.106  
   1.107 -definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
   1.108 -  "filter P M = Abs_multiset (\<lambda>x. if P x then count M x else 0)"
   1.109 +lift_definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" is "\<lambda>P M. \<lambda>x. if P x then M x else 0"
   1.110 +by (rule filter_preserves_multiset)
   1.111  
   1.112  hide_const (open) filter
   1.113  
   1.114  lemma count_filter [simp]:
   1.115    "count (Multiset.filter P M) a = (if P a then count M a else 0)"
   1.116 -  by (simp add: filter_def in_multiset multiset_typedef)
   1.117 +  by (simp add: filter.rep_eq)
   1.118  
   1.119  lemma filter_empty [simp]:
   1.120    "Multiset.filter P {#} = {#}"
   1.121 @@ -593,7 +594,7 @@
   1.122    and add: "!!M x. P M ==> P (M + {#x#})"
   1.123  shows "P M"
   1.124  proof -
   1.125 -  note defns = union_def single_def Mempty_def
   1.126 +  note defns = plus_multiset_def single_def zero_multiset_def
   1.127    note add' = add [unfolded defns, simplified]
   1.128    have aux: "\<And>a::'a. count (Abs_multiset (\<lambda>b. if b = a then 1 else 0)) =
   1.129      (\<lambda>b. if b = a then 1 else 0)" by (simp add: Abs_multiset_inverse in_multiset) 
   1.130 @@ -1073,7 +1074,8 @@
   1.131  
   1.132  lemma map_of_join_raw:
   1.133    assumes "distinct (map fst ys)"
   1.134 -  shows "map_of (join_raw f xs ys) x = (case map_of xs x of None => map_of ys x | Some v => (case map_of ys x of None => Some v | Some v' => Some (f x (v, v'))))"
   1.135 +  shows "map_of (join_raw f xs ys) x = (case map_of xs x of None => map_of ys x | Some v =>
   1.136 +    (case map_of ys x of None => Some v | Some v' => Some (f x (v, v'))))"
   1.137  using assms
   1.138  apply (induct ys)
   1.139  apply (auto simp add: map_of_map_default split: option.split)
   1.140 @@ -1093,8 +1095,10 @@
   1.141    "subtract_entries_raw xs ys = foldr (%(k, v). AList.map_entry k (%v'. v' - v)) ys xs"
   1.142  
   1.143  lemma map_of_subtract_entries_raw:
   1.144 -  "distinct (map fst ys) ==> map_of (subtract_entries_raw xs ys) x = (case map_of xs x of None => None | Some v => (case map_of ys x of None => Some v | Some v' => Some (v - v')))"
   1.145 -unfolding subtract_entries_raw_def
   1.146 +  assumes "distinct (map fst ys)"
   1.147 +  shows "map_of (subtract_entries_raw xs ys) x = (case map_of xs x of None => None | Some v =>
   1.148 +    (case map_of ys x of None => Some v | Some v' => Some (v - v')))"
   1.149 +using assms unfolding subtract_entries_raw_def
   1.150  apply (induct ys)
   1.151  apply auto
   1.152  apply (simp split: option.split)
   1.153 @@ -1197,7 +1201,7 @@
   1.154  
   1.155  lemma filter_Bag [code]:
   1.156    "Multiset.filter P (Bag xs) = Bag (DAList.filter (P \<circ> fst) xs)"
   1.157 -by (rule multiset_eqI) (simp add: count_of_filter filter.rep_eq)
   1.158 +by (rule multiset_eqI) (simp add: count_of_filter DAList.filter.rep_eq)
   1.159  
   1.160  lemma mset_less_eq_Bag [code]:
   1.161    "Bag xs \<le> A \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). count_of (DAList.impl_of xs) x \<le> count A x)"
     2.1 --- a/src/HOL/Lifting.thy	Thu Apr 12 10:29:45 2012 +0200
     2.2 +++ b/src/HOL/Lifting.thy	Thu Apr 12 13:47:21 2012 +0200
     2.3 @@ -199,19 +199,19 @@
     2.4      apply safe
     2.5      apply (drule Abs1, simp)
     2.6      apply (erule Abs2)
     2.7 -    apply (rule pred_compI)
     2.8 +    apply (rule relcomppI)
     2.9      apply (rule Rep1)
    2.10      apply (rule Rep2)
    2.11 -    apply (rule pred_compI, assumption)
    2.12 +    apply (rule relcomppI, assumption)
    2.13      apply (drule Abs1, simp)
    2.14      apply (clarsimp simp add: R2)
    2.15 -    apply (rule pred_compI, assumption)
    2.16 +    apply (rule relcomppI, assumption)
    2.17      apply (drule Abs1, simp)+
    2.18      apply (clarsimp simp add: R2)
    2.19      apply (drule Abs1, simp)+
    2.20      apply (clarsimp simp add: R2)
    2.21 -    apply (rule pred_compI, assumption)
    2.22 -    apply (rule pred_compI [rotated])
    2.23 +    apply (rule relcomppI, assumption)
    2.24 +    apply (rule relcomppI [rotated])
    2.25      apply (erule conversepI)
    2.26      apply (drule Abs1, simp)+
    2.27      apply (simp add: R2)
     3.1 --- a/src/HOL/List.thy	Thu Apr 12 10:29:45 2012 +0200
     3.2 +++ b/src/HOL/List.thy	Thu Apr 12 13:47:21 2012 +0200
     3.3 @@ -5677,7 +5677,7 @@
     3.4    "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)"
     3.5    by (simp add: finite_trancl_ntranl)
     3.6  
     3.7 -lemma set_rel_comp [code]:
     3.8 +lemma set_relcomp [code]:
     3.9    "set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
    3.10    by (auto simp add: Bex_def)
    3.11  
     4.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Thu Apr 12 10:29:45 2012 +0200
     4.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Thu Apr 12 13:47:21 2012 +0200
     4.3 @@ -1027,8 +1027,8 @@
     4.4    (o * o => bool) => i * i => bool) [inductify] converse .
     4.5  
     4.6  thm converse.equation
     4.7 -code_pred [inductify] rel_comp .
     4.8 -thm rel_comp.equation
     4.9 +code_pred [inductify] relcomp .
    4.10 +thm relcomp.equation
    4.11  code_pred [inductify] Image .
    4.12  thm Image.equation
    4.13  declare singleton_iff[code_pred_inline]
     5.1 --- a/src/HOL/Quotient.thy	Thu Apr 12 10:29:45 2012 +0200
     5.2 +++ b/src/HOL/Quotient.thy	Thu Apr 12 13:47:21 2012 +0200
     5.3 @@ -694,9 +694,9 @@
     5.4  apply (rule Quotient3I)
     5.5     apply (simp add: o_def Quotient3_abs_rep [OF R2] Quotient3_abs_rep [OF R1])
     5.6    apply simp
     5.7 -  apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI)
     5.8 +  apply (rule_tac b="Rep1 (Rep2 a)" in relcomppI)
     5.9     apply (rule Quotient3_rep_reflp [OF R1])
    5.10 -  apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI [rotated])
    5.11 +  apply (rule_tac b="Rep1 (Rep2 a)" in relcomppI [rotated])
    5.12     apply (rule Quotient3_rep_reflp [OF R1])
    5.13    apply (rule Rep1)
    5.14    apply (rule Quotient3_rep_reflp [OF R2])
    5.15 @@ -707,8 +707,8 @@
    5.16       apply (erule Quotient3_refl1 [OF R1])
    5.17      apply (drule Quotient3_refl1 [OF R2], drule Rep1)
    5.18      apply (subgoal_tac "R1 r (Rep1 (Abs1 x))")
    5.19 -     apply (rule_tac b="Rep1 (Abs1 x)" in pred_compI, assumption)
    5.20 -     apply (erule pred_compI)
    5.21 +     apply (rule_tac b="Rep1 (Abs1 x)" in relcomppI, assumption)
    5.22 +     apply (erule relcomppI)
    5.23       apply (erule Quotient3_symp [OF R1, THEN sympD])
    5.24      apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2])
    5.25      apply (rule conjI, erule Quotient3_refl1 [OF R1])
    5.26 @@ -721,8 +721,8 @@
    5.27      apply (erule Quotient3_refl1 [OF R1])
    5.28     apply (drule Quotient3_refl2 [OF R2], drule Rep1)
    5.29     apply (subgoal_tac "R1 s (Rep1 (Abs1 y))")
    5.30 -    apply (rule_tac b="Rep1 (Abs1 y)" in pred_compI, assumption)
    5.31 -    apply (erule pred_compI)
    5.32 +    apply (rule_tac b="Rep1 (Abs1 y)" in relcomppI, assumption)
    5.33 +    apply (erule relcomppI)
    5.34      apply (erule Quotient3_symp [OF R1, THEN sympD])
    5.35     apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2])
    5.36     apply (rule conjI, erule Quotient3_refl2 [OF R1])
    5.37 @@ -738,11 +738,11 @@
    5.38    apply (erule Quotient3_refl1 [OF R1])
    5.39   apply (rename_tac a b c d)
    5.40   apply simp
    5.41 - apply (rule_tac b="Rep1 (Abs1 r)" in pred_compI)
    5.42 + apply (rule_tac b="Rep1 (Abs1 r)" in relcomppI)
    5.43    apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2])
    5.44    apply (rule conjI, erule Quotient3_refl1 [OF R1])
    5.45    apply (simp add: Quotient3_abs_rep [OF R1] Quotient3_rep_reflp [OF R1])
    5.46 - apply (rule_tac b="Rep1 (Abs1 s)" in pred_compI [rotated])
    5.47 + apply (rule_tac b="Rep1 (Abs1 s)" in relcomppI [rotated])
    5.48    apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2])
    5.49    apply (simp add: Quotient3_abs_rep [OF R1] Quotient3_rep_reflp [OF R1])
    5.50    apply (erule Quotient3_refl2 [OF R1])
     6.1 --- a/src/HOL/Quotient_Examples/FSet.thy	Thu Apr 12 10:29:45 2012 +0200
     6.2 +++ b/src/HOL/Quotient_Examples/FSet.thy	Thu Apr 12 13:47:21 2012 +0200
     6.3 @@ -140,7 +140,7 @@
     6.4    next
     6.5      assume a: "(list_all2 R OOO op \<approx>) r s"
     6.6      then have b: "map Abs r \<approx> map Abs s"
     6.7 -    proof (elim pred_compE)
     6.8 +    proof (elim relcomppE)
     6.9        fix b ba
    6.10        assume c: "list_all2 R r b"
    6.11        assume d: "b \<approx> ba"
    6.12 @@ -165,11 +165,11 @@
    6.13      have y: "list_all2 R (map Rep (map Abs s)) s"
    6.14        by (fact rep_abs_rsp_left[OF list_quotient3[OF q], OF list_all2_refl'[OF e, of s]])
    6.15      have c: "(op \<approx> OO list_all2 R) (map Rep (map Abs r)) s"
    6.16 -      by (rule pred_compI) (rule b, rule y)
    6.17 +      by (rule relcomppI) (rule b, rule y)
    6.18      have z: "list_all2 R r (map Rep (map Abs r))"
    6.19        by (fact rep_abs_rsp[OF list_quotient3[OF q], OF list_all2_refl'[OF e, of r]])
    6.20      then show "(list_all2 R OOO op \<approx>) r s"
    6.21 -      using a c pred_compI by simp
    6.22 +      using a c relcomppI by simp
    6.23    qed
    6.24  qed
    6.25  
    6.26 @@ -360,7 +360,7 @@
    6.27  quotient_definition
    6.28    "concat_fset :: ('a fset) fset \<Rightarrow> 'a fset"
    6.29    is concat 
    6.30 -proof (elim pred_compE)
    6.31 +proof (elim relcomppE)
    6.32  fix a b ba bb
    6.33    assume a: "list_all2 op \<approx> a ba"
    6.34    with list_symp [OF list_eq_symp] have a': "list_all2 op \<approx> ba a" by (rule sympE)
    6.35 @@ -397,9 +397,9 @@
    6.36  lemma Cons_rsp2 [quot_respect]:
    6.37    shows "(op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) Cons Cons"
    6.38    apply (auto intro!: fun_relI)
    6.39 -  apply (rule_tac b="x # b" in pred_compI)
    6.40 +  apply (rule_tac b="x # b" in relcomppI)
    6.41    apply auto
    6.42 -  apply (rule_tac b="x # ba" in pred_compI)
    6.43 +  apply (rule_tac b="x # ba" in relcomppI)
    6.44    apply auto
    6.45    done
    6.46  
    6.47 @@ -453,7 +453,7 @@
    6.48    assumes "(R1 ===> R2 ===> R3) C C" and "(R4 ===> R5 ===> R6) C C"
    6.49    shows "(R1 OOO R4 ===> R2 OOO R5 ===> R3 OOO R6) C C"
    6.50    by (auto intro!: fun_relI)
    6.51 -     (metis (full_types) assms fun_relE pred_compI)
    6.52 +     (metis (full_types) assms fun_relE relcomppI)
    6.53  
    6.54  lemma append_rsp2 [quot_respect]:
    6.55    "(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) append append"
    6.56 @@ -479,7 +479,7 @@
    6.57      by (induct y ya rule: list_induct2')
    6.58         (simp_all, metis apply_rsp' list_eq_def)
    6.59    show "(list_all2 op \<approx> OOO op \<approx>) (map f xa) (map f' ya)"
    6.60 -    by (metis a b c list_eq_def pred_compI)
    6.61 +    by (metis a b c list_eq_def relcomppI)
    6.62  qed
    6.63  
    6.64  lemma map_prs2 [quot_preserve]:
     7.1 --- a/src/HOL/Relation.thy	Thu Apr 12 10:29:45 2012 +0200
     7.2 +++ b/src/HOL/Relation.thy	Thu Apr 12 13:47:21 2012 +0200
     7.3 @@ -507,29 +507,26 @@
     7.4  
     7.5  subsubsection {* Composition *}
     7.6  
     7.7 -inductive_set rel_comp  :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'c) set \<Rightarrow> ('a \<times> 'c) set" (infixr "O" 75)
     7.8 +inductive_set relcomp  :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'c) set \<Rightarrow> ('a \<times> 'c) set" (infixr "O" 75)
     7.9    for r :: "('a \<times> 'b) set" and s :: "('b \<times> 'c) set"
    7.10  where
    7.11 -  rel_compI [intro]: "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> s \<Longrightarrow> (a, c) \<in> r O s"
    7.12 +  relcompI [intro]: "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> s \<Longrightarrow> (a, c) \<in> r O s"
    7.13  
    7.14 -abbreviation pred_comp (infixr "OO" 75) where
    7.15 -  "pred_comp \<equiv> rel_compp"
    7.16 +notation relcompp (infixr "OO" 75)
    7.17  
    7.18 -lemmas pred_compI = rel_compp.intros
    7.19 +lemmas relcomppI = relcompp.intros
    7.20  
    7.21  text {*
    7.22    For historic reasons, the elimination rules are not wholly corresponding.
    7.23    Feel free to consolidate this.
    7.24  *}
    7.25  
    7.26 -inductive_cases rel_compEpair: "(a, c) \<in> r O s"
    7.27 -inductive_cases pred_compE [elim!]: "(r OO s) a c"
    7.28 +inductive_cases relcompEpair: "(a, c) \<in> r O s"
    7.29 +inductive_cases relcomppE [elim!]: "(r OO s) a c"
    7.30  
    7.31 -lemma rel_compE [elim!]: "xz \<in> r O s \<Longrightarrow>
    7.32 +lemma relcompE [elim!]: "xz \<in> r O s \<Longrightarrow>
    7.33    (\<And>x y z. xz = (x, z) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, z) \<in> s  \<Longrightarrow> P) \<Longrightarrow> P"
    7.34 -  by (cases xz) (simp, erule rel_compEpair, iprover)
    7.35 -
    7.36 -lemmas pred_comp_rel_comp_eq = rel_compp_rel_comp_eq
    7.37 +  by (cases xz) (simp, erule relcompEpair, iprover)
    7.38  
    7.39  lemma R_O_Id [simp]:
    7.40    "R O Id = R"
    7.41 @@ -539,28 +536,28 @@
    7.42    "Id O R = R"
    7.43    by fast
    7.44  
    7.45 -lemma rel_comp_empty1 [simp]:
    7.46 +lemma relcomp_empty1 [simp]:
    7.47    "{} O R = {}"
    7.48    by blast
    7.49  
    7.50 -lemma pred_comp_bot1 [simp]:
    7.51 +lemma relcompp_bot1 [simp]:
    7.52    "\<bottom> OO R = \<bottom>"
    7.53 -  by (fact rel_comp_empty1 [to_pred])
    7.54 +  by (fact relcomp_empty1 [to_pred])
    7.55  
    7.56 -lemma rel_comp_empty2 [simp]:
    7.57 +lemma relcomp_empty2 [simp]:
    7.58    "R O {} = {}"
    7.59    by blast
    7.60  
    7.61 -lemma pred_comp_bot2 [simp]:
    7.62 +lemma relcompp_bot2 [simp]:
    7.63    "R OO \<bottom> = \<bottom>"
    7.64 -  by (fact rel_comp_empty2 [to_pred])
    7.65 +  by (fact relcomp_empty2 [to_pred])
    7.66  
    7.67  lemma O_assoc:
    7.68    "(R O S) O T = R O (S O T)"
    7.69    by blast
    7.70  
    7.71  
    7.72 -lemma pred_comp_assoc:
    7.73 +lemma relcompp_assoc:
    7.74    "(r OO s) OO t = r OO (s OO t)"
    7.75    by (fact O_assoc [to_pred])
    7.76  
    7.77 @@ -568,55 +565,55 @@
    7.78    "trans r \<Longrightarrow> r O r \<subseteq> r"
    7.79    by (unfold trans_def) blast
    7.80  
    7.81 -lemma transp_pred_comp_less_eq:
    7.82 +lemma transp_relcompp_less_eq:
    7.83    "transp r \<Longrightarrow> r OO r \<le> r "
    7.84    by (fact trans_O_subset [to_pred])
    7.85  
    7.86 -lemma rel_comp_mono:
    7.87 +lemma relcomp_mono:
    7.88    "r' \<subseteq> r \<Longrightarrow> s' \<subseteq> s \<Longrightarrow> r' O s' \<subseteq> r O s"
    7.89    by blast
    7.90  
    7.91 -lemma pred_comp_mono:
    7.92 +lemma relcompp_mono:
    7.93    "r' \<le> r \<Longrightarrow> s' \<le> s \<Longrightarrow> r' OO s' \<le> r OO s "
    7.94 -  by (fact rel_comp_mono [to_pred])
    7.95 +  by (fact relcomp_mono [to_pred])
    7.96  
    7.97 -lemma rel_comp_subset_Sigma:
    7.98 +lemma relcomp_subset_Sigma:
    7.99    "r \<subseteq> A \<times> B \<Longrightarrow> s \<subseteq> B \<times> C \<Longrightarrow> r O s \<subseteq> A \<times> C"
   7.100    by blast
   7.101  
   7.102 -lemma rel_comp_distrib [simp]:
   7.103 +lemma relcomp_distrib [simp]:
   7.104    "R O (S \<union> T) = (R O S) \<union> (R O T)" 
   7.105    by auto
   7.106  
   7.107 -lemma pred_comp_distrib [simp]:
   7.108 +lemma relcompp_distrib [simp]:
   7.109    "R OO (S \<squnion> T) = R OO S \<squnion> R OO T"
   7.110 -  by (fact rel_comp_distrib [to_pred])
   7.111 +  by (fact relcomp_distrib [to_pred])
   7.112  
   7.113 -lemma rel_comp_distrib2 [simp]:
   7.114 +lemma relcomp_distrib2 [simp]:
   7.115    "(S \<union> T) O R = (S O R) \<union> (T O R)"
   7.116    by auto
   7.117  
   7.118 -lemma pred_comp_distrib2 [simp]:
   7.119 +lemma relcompp_distrib2 [simp]:
   7.120    "(S \<squnion> T) OO R = S OO R \<squnion> T OO R"
   7.121 -  by (fact rel_comp_distrib2 [to_pred])
   7.122 +  by (fact relcomp_distrib2 [to_pred])
   7.123  
   7.124 -lemma rel_comp_UNION_distrib:
   7.125 +lemma relcomp_UNION_distrib:
   7.126    "s O UNION I r = (\<Union>i\<in>I. s O r i) "
   7.127    by auto
   7.128  
   7.129 -(* FIXME thm rel_comp_UNION_distrib [to_pred] *)
   7.130 +(* FIXME thm relcomp_UNION_distrib [to_pred] *)
   7.131  
   7.132 -lemma rel_comp_UNION_distrib2:
   7.133 +lemma relcomp_UNION_distrib2:
   7.134    "UNION I r O s = (\<Union>i\<in>I. r i O s) "
   7.135    by auto
   7.136  
   7.137 -(* FIXME thm rel_comp_UNION_distrib2 [to_pred] *)
   7.138 +(* FIXME thm relcomp_UNION_distrib2 [to_pred] *)
   7.139  
   7.140 -lemma single_valued_rel_comp:
   7.141 +lemma single_valued_relcomp:
   7.142    "single_valued r \<Longrightarrow> single_valued s \<Longrightarrow> single_valued (r O s)"
   7.143    by (unfold single_valued_def) blast
   7.144  
   7.145 -lemma rel_comp_unfold:
   7.146 +lemma relcomp_unfold:
   7.147    "r O s = {(x, z). \<exists>y. (x, y) \<in> r \<and> (y, z) \<in> s}"
   7.148    by (auto simp add: set_eq_iff)
   7.149  
   7.150 @@ -676,12 +673,12 @@
   7.151    "(r\<inverse>\<inverse>)\<inverse>\<inverse> = r"
   7.152    by (fact converse_converse [to_pred])
   7.153  
   7.154 -lemma converse_rel_comp: "(r O s)^-1 = s^-1 O r^-1"
   7.155 +lemma converse_relcomp: "(r O s)^-1 = s^-1 O r^-1"
   7.156    by blast
   7.157  
   7.158 -lemma converse_pred_comp: "(r OO s)^--1 = s^--1 OO r^--1"
   7.159 -  by (iprover intro: order_antisym conversepI pred_compI
   7.160 -    elim: pred_compE dest: conversepD)
   7.161 +lemma converse_relcompp: "(r OO s)^--1 = s^--1 OO r^--1"
   7.162 +  by (iprover intro: order_antisym conversepI relcomppI
   7.163 +    elim: relcomppE dest: conversepD)
   7.164  
   7.165  lemma converse_Int: "(r \<inter> s)^-1 = r^-1 \<inter> s^-1"
   7.166    by blast
     8.1 --- a/src/HOL/Tools/Function/termination.ML	Thu Apr 12 10:29:45 2012 +0200
     8.2 +++ b/src/HOL/Tools/Function/termination.ML	Thu Apr 12 13:47:21 2012 +0200
     8.3 @@ -141,7 +141,7 @@
     8.4  fun prove_chain thy chain_tac (c1, c2) =
     8.5    let
     8.6      val goal =
     8.7 -      HOLogic.mk_eq (HOLogic.mk_binop @{const_name Relation.rel_comp} (c1, c2),
     8.8 +      HOLogic.mk_eq (HOLogic.mk_binop @{const_name Relation.relcomp} (c1, c2),
     8.9          Const (@{const_abbrev Set.empty}, fastype_of c1))
    8.10        |> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *)
    8.11    in
     9.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Apr 12 10:29:45 2012 +0200
     9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Apr 12 13:47:21 2012 +0200
     9.3 @@ -391,7 +391,7 @@
     9.4     (@{const_name Id}, 0),
     9.5     (@{const_name converse}, 1),
     9.6     (@{const_name trancl}, 1),
     9.7 -   (@{const_name rel_comp}, 2),
     9.8 +   (@{const_name relcomp}, 2),
     9.9     (@{const_name finite}, 1),
    9.10     (@{const_name unknown}, 0),
    9.11     (@{const_name is_unknown}, 1),
    10.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Apr 12 10:29:45 2012 +0200
    10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Apr 12 13:47:21 2012 +0200
    10.3 @@ -856,7 +856,7 @@
    10.4                   accum ||> add_annotation_atom_comp Neq [] (V x) (A New))
    10.5                end
    10.6              | @{const_name trancl} => do_fragile_set_operation T accum
    10.7 -            | @{const_name rel_comp} =>
    10.8 +            | @{const_name relcomp} =>
    10.9                let
   10.10                  val x = Unsynchronized.inc max_fresh
   10.11                  val bc_set_M = domain_type T |> mtype_for_set x
    11.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Thu Apr 12 10:29:45 2012 +0200
    11.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Thu Apr 12 13:47:21 2012 +0200
    11.3 @@ -522,7 +522,7 @@
    11.4            Op1 (Converse, range_type T, Any, sub t1)
    11.5          | (Const (@{const_name trancl}, T), [t1]) =>
    11.6            Op1 (Closure, range_type T, Any, sub t1)
    11.7 -        | (Const (@{const_name rel_comp}, T), [t1, t2]) =>
    11.8 +        | (Const (@{const_name relcomp}, T), [t1, t2]) =>
    11.9            Op2 (Composition, nth_range_type 2 T, Any, sub t1, sub t2)
   11.10          | (Const (x as (s as @{const_name Suc}, T)), []) =>
   11.11            if is_built_in_const thy stds x then Cst (Suc, T, Any)
    12.1 --- a/src/HOL/Transitive_Closure.thy	Thu Apr 12 10:29:45 2012 +0200
    12.2 +++ b/src/HOL/Transitive_Closure.thy	Thu Apr 12 13:47:21 2012 +0200
    12.3 @@ -726,7 +726,7 @@
    12.4  lemma relpowp_relpow_eq [pred_set_conv]:
    12.5    fixes R :: "'a rel"
    12.6    shows "(\<lambda>x y. (x, y) \<in> R) ^^ n = (\<lambda>x y. (x, y) \<in> R ^^ n)"
    12.7 -  by (induct n) (simp_all add: rel_compp_rel_comp_eq)
    12.8 +  by (induct n) (simp_all add: relcompp_relcomp_eq)
    12.9  
   12.10  text {* for code generation *}
   12.11  
   12.12 @@ -849,7 +849,7 @@
   12.13     apply (drule tranclD2)
   12.14     apply (clarsimp simp: rtrancl_is_UN_relpow)
   12.15     apply (rule_tac x="Suc n" in exI)
   12.16 -   apply (clarsimp simp: rel_comp_unfold)
   12.17 +   apply (clarsimp simp: relcomp_unfold)
   12.18     apply fastforce
   12.19    apply clarsimp
   12.20    apply (case_tac n, simp)
   12.21 @@ -870,7 +870,7 @@
   12.22  next
   12.23    case (Suc n)
   12.24    show ?case
   12.25 -  proof (simp add: rel_comp_unfold Suc)
   12.26 +  proof (simp add: relcomp_unfold Suc)
   12.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)
   12.28       = (\<exists>f. f 0 = a \<and> f(Suc n) = b \<and> (\<forall>i<Suc n. (f i, f (Suc i)) \<in> R))"
   12.29      (is "?l = ?r")
   12.30 @@ -979,7 +979,7 @@
   12.31  apply(auto dest: relpow_finite_bounded1)
   12.32  done
   12.33  
   12.34 -lemma finite_rel_comp[simp,intro]:
   12.35 +lemma finite_relcomp[simp,intro]:
   12.36  assumes "finite R" and "finite S"
   12.37  shows "finite(R O S)"
   12.38  proof-
    13.1 --- a/src/HOL/Wellfounded.thy	Thu Apr 12 10:29:45 2012 +0200
    13.2 +++ b/src/HOL/Wellfounded.thy	Thu Apr 12 13:47:21 2012 +0200
    13.3 @@ -271,7 +271,7 @@
    13.4        assume "y \<in> Q"
    13.5        with `y \<notin> ?Q'` 
    13.6        obtain w where "(w, y) \<in> R" and "w \<in> Q" by auto
    13.7 -      from `(w, y) \<in> R` `(y, z) \<in> S` have "(w, z) \<in> R O S" by (rule rel_compI)
    13.8 +      from `(w, y) \<in> R` `(y, z) \<in> S` have "(w, z) \<in> R O S" by (rule relcompI)
    13.9        with `R O S \<subseteq> R` have "(w, z) \<in> R" ..
   13.10        with `z \<in> ?Q'` have "w \<notin> Q" by blast 
   13.11        with `w \<in> Q` show False by contradiction
    14.1 --- a/src/HOL/ex/Coherent.thy	Thu Apr 12 10:29:45 2012 +0200
    14.2 +++ b/src/HOL/ex/Coherent.thy	Thu Apr 12 13:47:21 2012 +0200
    14.3 @@ -13,7 +13,7 @@
    14.4  
    14.5  no_notation
    14.6    comp (infixl "o" 55) and
    14.7 -  rel_comp (infixr "O" 75)
    14.8 +  relcomp (infixr "O" 75)
    14.9  
   14.10  lemma p1p2:
   14.11    assumes
    15.1 --- a/src/HOL/ex/Executable_Relation.thy	Thu Apr 12 10:29:45 2012 +0200
    15.2 +++ b/src/HOL/ex/Executable_Relation.thy	Thu Apr 12 13:47:21 2012 +0200
    15.3 @@ -27,7 +27,7 @@
    15.4  
    15.5  lemma comp_Id_on:
    15.6    "Id_on X O R = Set.project (%(x, y). x : X) R"
    15.7 -by (auto intro!: rel_compI)
    15.8 +by (auto intro!: relcompI)
    15.9  
   15.10  lemma comp_Id_on':
   15.11    "R O Id_on X = Set.project (%(x, y). y : X) R"
   15.12 @@ -37,7 +37,7 @@
   15.13    "Set.project (%(x, y). x : X) (Id_on Y) = Id_on (X Int Y)"
   15.14  by auto
   15.15  
   15.16 -lemma rel_comp_raw:
   15.17 +lemma relcomp_raw:
   15.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))"
   15.19  unfolding rel_raw_def
   15.20  apply simp
   15.21 @@ -79,7 +79,7 @@
   15.22  
   15.23  subsubsection {* Constant definitions on relations *}
   15.24  
   15.25 -hide_const (open) converse rel_comp rtrancl Image
   15.26 +hide_const (open) converse relcomp rtrancl Image
   15.27  
   15.28  quotient_definition member :: "'a * 'a => 'a rel => bool" where
   15.29    "member" is "Set.member :: 'a * 'a => ('a * 'a) set => bool" done
   15.30 @@ -92,9 +92,9 @@
   15.31  where
   15.32    "union" is "Set.union :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" done
   15.33  
   15.34 -quotient_definition rel_comp :: "'a rel => 'a rel => 'a rel"
   15.35 +quotient_definition relcomp :: "'a rel => 'a rel => 'a rel"
   15.36  where
   15.37 -  "rel_comp" is "Relation.rel_comp :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" done
   15.38 +  "relcomp" is "Relation.relcomp :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" done
   15.39  
   15.40  quotient_definition rtrancl :: "'a rel => 'a rel"
   15.41  where
   15.42 @@ -121,8 +121,8 @@
   15.43  by (lifting union_raw)
   15.44  
   15.45  lemma [code]:
   15.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))"
   15.47 -by (lifting rel_comp_raw)
   15.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))"
   15.49 +by (lifting relcomp_raw)
   15.50  
   15.51  lemma [code]:
   15.52    "rtrancl (rel X R) = rel UNIV (R^+)"