--- a/src/HOL/Library/Multiset.thy Thu Apr 12 10:29:45 2012 +0200
+++ b/src/HOL/Library/Multiset.thy Thu Apr 12 13:47:21 2012 +0200
@@ -19,7 +19,7 @@
show "(\<lambda>x. 0::nat) \<in> {f. finite {x. f x > 0}}" by simp
qed
-lemmas multiset_typedef = Abs_multiset_inverse count_inverse count
+setup_lifting type_definition_multiset
abbreviation Melem :: "'a => 'a multiset => bool" ("(_/ :# _)" [50, 51] 50) where
"a :# M == 0 < count M a"
@@ -82,21 +82,21 @@
instantiation multiset :: (type) "{zero, plus}"
begin
-definition Mempty_def:
- "0 = Abs_multiset (\<lambda>a. 0)"
+lift_definition zero_multiset :: "'a multiset" is "\<lambda>a. 0"
+by (rule const0_in_multiset)
abbreviation Mempty :: "'a multiset" ("{#}") where
"Mempty \<equiv> 0"
-definition union_def:
- "M + N = Abs_multiset (\<lambda>a. count M a + count N a)"
+lift_definition plus_multiset :: "'a multiset => 'a multiset => 'a multiset" is "\<lambda>M N. (\<lambda>a. M a + N a)"
+by (rule union_preserves_multiset)
instance ..
end
-definition single :: "'a => 'a multiset" where
- "single a = Abs_multiset (\<lambda>b. if b = a then 1 else 0)"
+lift_definition single :: "'a => 'a multiset" is "\<lambda>a b. if b = a then 1 else 0"
+by (rule only1_in_multiset)
syntax
"_multiset" :: "args => 'a multiset" ("{#(_)#}")
@@ -105,10 +105,10 @@
"{#x#}" == "CONST single x"
lemma count_empty [simp]: "count {#} a = 0"
- by (simp add: Mempty_def in_multiset multiset_typedef)
+ by (simp add: zero_multiset.rep_eq)
lemma count_single [simp]: "count {#b#} a = (if b = a then 1 else 0)"
- by (simp add: single_def in_multiset multiset_typedef)
+ by (simp add: single.rep_eq)
subsection {* Basic operations *}
@@ -116,7 +116,7 @@
subsubsection {* Union *}
lemma count_union [simp]: "count (M + N) a = count M a + count N a"
- by (simp add: union_def in_multiset multiset_typedef)
+ by (simp add: plus_multiset.rep_eq)
instance multiset :: (type) cancel_comm_monoid_add
by default (simp_all add: multiset_eq_iff)
@@ -127,15 +127,15 @@
instantiation multiset :: (type) minus
begin
-definition diff_def:
- "M - N = Abs_multiset (\<lambda>a. count M a - count N a)"
-
+lift_definition minus_multiset :: "'a multiset => 'a multiset => 'a multiset" is "\<lambda> M N. \<lambda>a. M a - N a"
+by (rule diff_preserves_multiset)
+
instance ..
end
lemma count_diff [simp]: "count (M - N) a = count M a - count N a"
- by (simp add: diff_def in_multiset multiset_typedef)
+ by (simp add: minus_multiset.rep_eq)
lemma diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}"
by(simp add: multiset_eq_iff)
@@ -264,8 +264,9 @@
instantiation multiset :: (type) ordered_ab_semigroup_add_imp_le
begin
-definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
- mset_le_def: "A \<le> B \<longleftrightarrow> (\<forall>a. count A a \<le> count B a)"
+lift_definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" is "\<lambda> A B. (\<forall>a. A a \<le> B a)"
+by simp
+lemmas mset_le_def = less_eq_multiset_def
definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
mset_less_def: "(A::'a multiset) < B \<longleftrightarrow> A \<le> B \<and> A \<noteq> B"
@@ -391,7 +392,7 @@
lemma multiset_inter_count [simp]:
"count (A #\<inter> B) x = min (count A x) (count B x)"
- by (simp add: multiset_inter_def multiset_typedef)
+ by (simp add: multiset_inter_def)
lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}"
by (rule multiset_eqI) auto
@@ -414,14 +415,14 @@
text {* Multiset comprehension *}
-definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
- "filter P M = Abs_multiset (\<lambda>x. if P x then count M x else 0)"
+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"
+by (rule filter_preserves_multiset)
hide_const (open) filter
lemma count_filter [simp]:
"count (Multiset.filter P M) a = (if P a then count M a else 0)"
- by (simp add: filter_def in_multiset multiset_typedef)
+ by (simp add: filter.rep_eq)
lemma filter_empty [simp]:
"Multiset.filter P {#} = {#}"
@@ -593,7 +594,7 @@
and add: "!!M x. P M ==> P (M + {#x#})"
shows "P M"
proof -
- note defns = union_def single_def Mempty_def
+ note defns = plus_multiset_def single_def zero_multiset_def
note add' = add [unfolded defns, simplified]
have aux: "\<And>a::'a. count (Abs_multiset (\<lambda>b. if b = a then 1 else 0)) =
(\<lambda>b. if b = a then 1 else 0)" by (simp add: Abs_multiset_inverse in_multiset)
@@ -1073,7 +1074,8 @@
lemma map_of_join_raw:
assumes "distinct (map fst ys)"
- 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'))))"
+ 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'))))"
using assms
apply (induct ys)
apply (auto simp add: map_of_map_default split: option.split)
@@ -1093,8 +1095,10 @@
"subtract_entries_raw xs ys = foldr (%(k, v). AList.map_entry k (%v'. v' - v)) ys xs"
lemma map_of_subtract_entries_raw:
- "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')))"
-unfolding subtract_entries_raw_def
+ assumes "distinct (map fst ys)"
+ shows "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')))"
+using assms unfolding subtract_entries_raw_def
apply (induct ys)
apply auto
apply (simp split: option.split)
@@ -1197,7 +1201,7 @@
lemma filter_Bag [code]:
"Multiset.filter P (Bag xs) = Bag (DAList.filter (P \<circ> fst) xs)"
-by (rule multiset_eqI) (simp add: count_of_filter filter.rep_eq)
+by (rule multiset_eqI) (simp add: count_of_filter DAList.filter.rep_eq)
lemma mset_less_eq_Bag [code]:
"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)"
--- a/src/HOL/Lifting.thy Thu Apr 12 10:29:45 2012 +0200
+++ b/src/HOL/Lifting.thy Thu Apr 12 13:47:21 2012 +0200
@@ -199,19 +199,19 @@
apply safe
apply (drule Abs1, simp)
apply (erule Abs2)
- apply (rule pred_compI)
+ apply (rule relcomppI)
apply (rule Rep1)
apply (rule Rep2)
- apply (rule pred_compI, assumption)
+ apply (rule relcomppI, assumption)
apply (drule Abs1, simp)
apply (clarsimp simp add: R2)
- apply (rule pred_compI, assumption)
+ apply (rule relcomppI, assumption)
apply (drule Abs1, simp)+
apply (clarsimp simp add: R2)
apply (drule Abs1, simp)+
apply (clarsimp simp add: R2)
- apply (rule pred_compI, assumption)
- apply (rule pred_compI [rotated])
+ apply (rule relcomppI, assumption)
+ apply (rule relcomppI [rotated])
apply (erule conversepI)
apply (drule Abs1, simp)+
apply (simp add: R2)
--- a/src/HOL/List.thy Thu Apr 12 10:29:45 2012 +0200
+++ b/src/HOL/List.thy Thu Apr 12 13:47:21 2012 +0200
@@ -5677,7 +5677,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)
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Thu Apr 12 10:29:45 2012 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Thu Apr 12 13:47:21 2012 +0200
@@ -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]
--- a/src/HOL/Quotient.thy Thu Apr 12 10:29:45 2012 +0200
+++ b/src/HOL/Quotient.thy Thu Apr 12 13:47:21 2012 +0200
@@ -694,9 +694,9 @@
apply (rule Quotient3I)
apply (simp add: o_def Quotient3_abs_rep [OF R2] Quotient3_abs_rep [OF R1])
apply simp
- apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI)
+ apply (rule_tac b="Rep1 (Rep2 a)" in relcomppI)
apply (rule Quotient3_rep_reflp [OF R1])
- apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI [rotated])
+ apply (rule_tac b="Rep1 (Rep2 a)" in relcomppI [rotated])
apply (rule Quotient3_rep_reflp [OF R1])
apply (rule Rep1)
apply (rule Quotient3_rep_reflp [OF R2])
@@ -707,8 +707,8 @@
apply (erule Quotient3_refl1 [OF R1])
apply (drule Quotient3_refl1 [OF R2], drule Rep1)
apply (subgoal_tac "R1 r (Rep1 (Abs1 x))")
- apply (rule_tac b="Rep1 (Abs1 x)" in pred_compI, assumption)
- apply (erule pred_compI)
+ apply (rule_tac b="Rep1 (Abs1 x)" in relcomppI, assumption)
+ apply (erule relcomppI)
apply (erule Quotient3_symp [OF R1, THEN sympD])
apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2])
apply (rule conjI, erule Quotient3_refl1 [OF R1])
@@ -721,8 +721,8 @@
apply (erule Quotient3_refl1 [OF R1])
apply (drule Quotient3_refl2 [OF R2], drule Rep1)
apply (subgoal_tac "R1 s (Rep1 (Abs1 y))")
- apply (rule_tac b="Rep1 (Abs1 y)" in pred_compI, assumption)
- apply (erule pred_compI)
+ apply (rule_tac b="Rep1 (Abs1 y)" in relcomppI, assumption)
+ apply (erule relcomppI)
apply (erule Quotient3_symp [OF R1, THEN sympD])
apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2])
apply (rule conjI, erule Quotient3_refl2 [OF R1])
@@ -738,11 +738,11 @@
apply (erule Quotient3_refl1 [OF R1])
apply (rename_tac a b c d)
apply simp
- apply (rule_tac b="Rep1 (Abs1 r)" in pred_compI)
+ apply (rule_tac b="Rep1 (Abs1 r)" in relcomppI)
apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2])
apply (rule conjI, erule Quotient3_refl1 [OF R1])
apply (simp add: Quotient3_abs_rep [OF R1] Quotient3_rep_reflp [OF R1])
- apply (rule_tac b="Rep1 (Abs1 s)" in pred_compI [rotated])
+ apply (rule_tac b="Rep1 (Abs1 s)" in relcomppI [rotated])
apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2])
apply (simp add: Quotient3_abs_rep [OF R1] Quotient3_rep_reflp [OF R1])
apply (erule Quotient3_refl2 [OF R1])
--- a/src/HOL/Quotient_Examples/FSet.thy Thu Apr 12 10:29:45 2012 +0200
+++ b/src/HOL/Quotient_Examples/FSet.thy Thu Apr 12 13:47:21 2012 +0200
@@ -140,7 +140,7 @@
next
assume a: "(list_all2 R OOO op \<approx>) r s"
then have b: "map Abs r \<approx> map Abs s"
- proof (elim pred_compE)
+ proof (elim relcomppE)
fix b ba
assume c: "list_all2 R r b"
assume d: "b \<approx> ba"
@@ -165,11 +165,11 @@
have y: "list_all2 R (map Rep (map Abs s)) s"
by (fact rep_abs_rsp_left[OF list_quotient3[OF q], OF list_all2_refl'[OF e, of s]])
have c: "(op \<approx> OO list_all2 R) (map Rep (map Abs r)) s"
- by (rule pred_compI) (rule b, rule y)
+ by (rule relcomppI) (rule b, rule y)
have z: "list_all2 R r (map Rep (map Abs r))"
by (fact rep_abs_rsp[OF list_quotient3[OF q], OF list_all2_refl'[OF e, of r]])
then show "(list_all2 R OOO op \<approx>) r s"
- using a c pred_compI by simp
+ using a c relcomppI by simp
qed
qed
@@ -360,7 +360,7 @@
quotient_definition
"concat_fset :: ('a fset) fset \<Rightarrow> 'a fset"
is concat
-proof (elim pred_compE)
+proof (elim relcomppE)
fix a b ba bb
assume a: "list_all2 op \<approx> a ba"
with list_symp [OF list_eq_symp] have a': "list_all2 op \<approx> ba a" by (rule sympE)
@@ -397,9 +397,9 @@
lemma Cons_rsp2 [quot_respect]:
shows "(op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) Cons Cons"
apply (auto intro!: fun_relI)
- apply (rule_tac b="x # b" in pred_compI)
+ apply (rule_tac b="x # b" in relcomppI)
apply auto
- apply (rule_tac b="x # ba" in pred_compI)
+ apply (rule_tac b="x # ba" in relcomppI)
apply auto
done
@@ -453,7 +453,7 @@
assumes "(R1 ===> R2 ===> R3) C C" and "(R4 ===> R5 ===> R6) C C"
shows "(R1 OOO R4 ===> R2 OOO R5 ===> R3 OOO R6) C C"
by (auto intro!: fun_relI)
- (metis (full_types) assms fun_relE pred_compI)
+ (metis (full_types) assms fun_relE relcomppI)
lemma append_rsp2 [quot_respect]:
"(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) append append"
@@ -479,7 +479,7 @@
by (induct y ya rule: list_induct2')
(simp_all, metis apply_rsp' list_eq_def)
show "(list_all2 op \<approx> OOO op \<approx>) (map f xa) (map f' ya)"
- by (metis a b c list_eq_def pred_compI)
+ by (metis a b c list_eq_def relcomppI)
qed
lemma map_prs2 [quot_preserve]:
--- a/src/HOL/Relation.thy Thu Apr 12 10:29:45 2012 +0200
+++ b/src/HOL/Relation.thy Thu Apr 12 13:47:21 2012 +0200
@@ -507,29 +507,26 @@
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"
+notation relcompp (infixr "OO" 75)
-lemmas pred_compI = rel_compp.intros
+lemmas relcomppI = 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 pred_compE [elim!]: "(r OO s) a c"
+inductive_cases relcompEpair: "(a, c) \<in> r O s"
+inductive_cases relcomppE [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)
-
-lemmas pred_comp_rel_comp_eq = rel_compp_rel_comp_eq
+ by (cases xz) (simp, erule relcompEpair, iprover)
lemma R_O_Id [simp]:
"R O Id = R"
@@ -539,28 +536,28 @@
"Id O R = R"
by fast
-lemma rel_comp_empty1 [simp]:
+lemma relcomp_empty1 [simp]:
"{} O R = {}"
by blast
-lemma pred_comp_bot1 [simp]:
+lemma relcompp_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]:
+lemma relcompp_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)"
by blast
-lemma pred_comp_assoc:
+lemma relcompp_assoc:
"(r OO s) OO t = r OO (s OO t)"
by (fact O_assoc [to_pred])
@@ -568,55 +565,55 @@
"trans r \<Longrightarrow> r O r \<subseteq> r"
by (unfold trans_def) blast
-lemma transp_pred_comp_less_eq:
+lemma transp_relcompp_less_eq:
"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:
+lemma relcompp_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]:
+lemma relcompp_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]:
+lemma relcompp_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,12 +673,12 @@
"(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"
- by (iprover intro: order_antisym conversepI pred_compI
- elim: pred_compE dest: conversepD)
+lemma converse_relcompp: "(r OO s)^--1 = s^--1 OO r^--1"
+ by (iprover intro: order_antisym conversepI relcomppI
+ elim: relcomppE dest: conversepD)
lemma converse_Int: "(r \<inter> s)^-1 = r^-1 \<inter> s^-1"
by blast
--- a/src/HOL/Tools/Function/termination.ML Thu Apr 12 10:29:45 2012 +0200
+++ b/src/HOL/Tools/Function/termination.ML Thu Apr 12 13:47:21 2012 +0200
@@ -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
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Apr 12 10:29:45 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Apr 12 13:47:21 2012 +0200
@@ -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),
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Apr 12 10:29:45 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Apr 12 13:47:21 2012 +0200
@@ -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
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Thu Apr 12 10:29:45 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Thu Apr 12 13:47:21 2012 +0200
@@ -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)
--- a/src/HOL/Transitive_Closure.thy Thu Apr 12 10:29:45 2012 +0200
+++ b/src/HOL/Transitive_Closure.thy Thu Apr 12 13:47:21 2012 +0200
@@ -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-
--- a/src/HOL/Wellfounded.thy Thu Apr 12 10:29:45 2012 +0200
+++ b/src/HOL/Wellfounded.thy Thu Apr 12 13:47:21 2012 +0200
@@ -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
--- a/src/HOL/ex/Coherent.thy Thu Apr 12 10:29:45 2012 +0200
+++ b/src/HOL/ex/Coherent.thy Thu Apr 12 13:47:21 2012 +0200
@@ -13,7 +13,7 @@
no_notation
comp (infixl "o" 55) and
- rel_comp (infixr "O" 75)
+ relcomp (infixr "O" 75)
lemma p1p2:
assumes
--- a/src/HOL/ex/Executable_Relation.thy Thu Apr 12 10:29:45 2012 +0200
+++ b/src/HOL/ex/Executable_Relation.thy Thu Apr 12 13:47:21 2012 +0200
@@ -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^+)"