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^+)"