--- a/NEWS Fri Oct 01 14:15:49 2010 +0200
+++ b/NEWS Fri Oct 01 16:05:25 2010 +0200
@@ -74,6 +74,9 @@
*** HOL ***
+* Constant `contents` renamed to `the_elem`, to free the generic name
+contents for other uses. INCOMPATIBILITY.
+
* Dropped old primrec package. INCOMPATIBILITY.
* Improved infrastructure for term evaluation using code generator
--- a/src/HOL/Algebra/AbelCoset.thy Fri Oct 01 14:15:49 2010 +0200
+++ b/src/HOL/Algebra/AbelCoset.thy Fri Oct 01 16:05:25 2010 +0200
@@ -607,20 +607,20 @@
by (rule group_hom.FactGroup_nonempty[OF a_group_hom,
folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule X)
-lemma (in abelian_group_hom) FactGroup_contents_mem:
+lemma (in abelian_group_hom) FactGroup_the_elem_mem:
assumes X: "X \<in> carrier (G A_Mod (a_kernel G H h))"
- shows "contents (h`X) \<in> carrier H"
-by (rule group_hom.FactGroup_contents_mem[OF a_group_hom,
+ shows "the_elem (h`X) \<in> carrier H"
+by (rule group_hom.FactGroup_the_elem_mem[OF a_group_hom,
folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule X)
lemma (in abelian_group_hom) A_FactGroup_hom:
- "(\<lambda>X. contents (h`X)) \<in> hom (G A_Mod (a_kernel G H h))
+ "(\<lambda>X. the_elem (h`X)) \<in> hom (G A_Mod (a_kernel G H h))
\<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr>"
by (rule group_hom.FactGroup_hom[OF a_group_hom,
folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
lemma (in abelian_group_hom) A_FactGroup_inj_on:
- "inj_on (\<lambda>X. contents (h ` X)) (carrier (G A_Mod a_kernel G H h))"
+ "inj_on (\<lambda>X. the_elem (h ` X)) (carrier (G A_Mod a_kernel G H h))"
by (rule group_hom.FactGroup_inj_on[OF a_group_hom,
folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
@@ -628,7 +628,7 @@
homomorphism from the quotient group*}
lemma (in abelian_group_hom) A_FactGroup_onto:
assumes h: "h ` carrier G = carrier H"
- shows "(\<lambda>X. contents (h ` X)) ` carrier (G A_Mod a_kernel G H h) = carrier H"
+ shows "(\<lambda>X. the_elem (h ` X)) ` carrier (G A_Mod a_kernel G H h) = carrier H"
by (rule group_hom.FactGroup_onto[OF a_group_hom,
folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule h)
@@ -636,7 +636,7 @@
quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
theorem (in abelian_group_hom) A_FactGroup_iso:
"h ` carrier G = carrier H
- \<Longrightarrow> (\<lambda>X. contents (h`X)) \<in> (G A_Mod (a_kernel G H h)) \<cong>
+ \<Longrightarrow> (\<lambda>X. the_elem (h`X)) \<in> (G A_Mod (a_kernel G H h)) \<cong>
(| carrier = carrier H, mult = add H, one = zero H |)"
by (rule group_hom.FactGroup_iso[OF a_group_hom,
folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
--- a/src/HOL/Algebra/Coset.thy Fri Oct 01 14:15:49 2010 +0200
+++ b/src/HOL/Algebra/Coset.thy Fri Oct 01 16:05:25 2010 +0200
@@ -924,9 +924,9 @@
qed
-lemma (in group_hom) FactGroup_contents_mem:
+lemma (in group_hom) FactGroup_the_elem_mem:
assumes X: "X \<in> carrier (G Mod (kernel G H h))"
- shows "contents (h`X) \<in> carrier H"
+ shows "the_elem (h`X) \<in> carrier H"
proof -
from X
obtain g where g: "g \<in> carrier G"
@@ -937,8 +937,8 @@
qed
lemma (in group_hom) FactGroup_hom:
- "(\<lambda>X. contents (h`X)) \<in> hom (G Mod (kernel G H h)) H"
-apply (simp add: hom_def FactGroup_contents_mem normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
+ "(\<lambda>X. the_elem (h`X)) \<in> hom (G Mod (kernel G H h)) H"
+apply (simp add: hom_def FactGroup_the_elem_mem normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
proof (intro ballI)
fix X and X'
assume X: "X \<in> carrier (G Mod kernel G H h)"
@@ -955,7 +955,7 @@
by (auto dest!: FactGroup_nonempty
simp add: set_mult_def image_eq_UN
subsetD [OF Xsub] subsetD [OF X'sub])
- thus "contents (h ` (X <#> X')) = contents (h ` X) \<otimes>\<^bsub>H\<^esub> contents (h ` X')"
+ thus "the_elem (h ` (X <#> X')) = the_elem (h ` X) \<otimes>\<^bsub>H\<^esub> the_elem (h ` X')"
by (simp add: all image_eq_UN FactGroup_nonempty X X')
qed
@@ -971,7 +971,7 @@
done
lemma (in group_hom) FactGroup_inj_on:
- "inj_on (\<lambda>X. contents (h ` X)) (carrier (G Mod kernel G H h))"
+ "inj_on (\<lambda>X. the_elem (h ` X)) (carrier (G Mod kernel G H h))"
proof (simp add: inj_on_def, clarify)
fix X and X'
assume X: "X \<in> carrier (G Mod kernel G H h)"
@@ -983,7 +983,7 @@
by (auto simp add: FactGroup_def RCOSETS_def)
hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'"
by (force simp add: kernel_def r_coset_def image_def)+
- assume "contents (h ` X) = contents (h ` X')"
+ assume "the_elem (h ` X) = the_elem (h ` X')"
hence h: "h g = h g'"
by (simp add: image_eq_UN all FactGroup_nonempty X X')
show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX)
@@ -993,11 +993,11 @@
homomorphism from the quotient group*}
lemma (in group_hom) FactGroup_onto:
assumes h: "h ` carrier G = carrier H"
- shows "(\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h) = carrier H"
+ shows "(\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h) = carrier H"
proof
- show "(\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h) \<subseteq> carrier H"
- by (auto simp add: FactGroup_contents_mem)
- show "carrier H \<subseteq> (\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h)"
+ show "(\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h) \<subseteq> carrier H"
+ by (auto simp add: FactGroup_the_elem_mem)
+ show "carrier H \<subseteq> (\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h)"
proof
fix y
assume y: "y \<in> carrier H"
@@ -1005,7 +1005,7 @@
by (blast elim: equalityE)
hence "(\<Union>x\<in>kernel G H h #> g. {h x}) = {y}"
by (auto simp add: y kernel_def r_coset_def)
- with g show "y \<in> (\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h)"
+ with g show "y \<in> (\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h)"
by (auto intro!: bexI simp add: FactGroup_def RCOSETS_def image_eq_UN)
qed
qed
@@ -1015,7 +1015,7 @@
quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
theorem (in group_hom) FactGroup_iso:
"h ` carrier G = carrier H
- \<Longrightarrow> (\<lambda>X. contents (h`X)) \<in> (G Mod (kernel G H h)) \<cong> H"
+ \<Longrightarrow> (\<lambda>X. the_elem (h`X)) \<in> (G Mod (kernel G H h)) \<cong> H"
by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def
FactGroup_onto)
--- a/src/HOL/Induct/QuoDataType.thy Fri Oct 01 14:15:49 2010 +0200
+++ b/src/HOL/Induct/QuoDataType.thy Fri Oct 01 16:05:25 2010 +0200
@@ -422,7 +422,7 @@
definition
discrim :: "msg \<Rightarrow> int" where
- "discrim X = contents (\<Union>U \<in> Rep_Msg X. {freediscrim U})"
+ "discrim X = the_elem (\<Union>U \<in> Rep_Msg X. {freediscrim U})"
lemma discrim_congruent: "(\<lambda>U. {freediscrim U}) respects msgrel"
by (simp add: congruent_def msgrel_imp_eq_freediscrim)
--- a/src/HOL/Induct/QuoNestedDataType.thy Fri Oct 01 14:15:49 2010 +0200
+++ b/src/HOL/Induct/QuoNestedDataType.thy Fri Oct 01 16:05:25 2010 +0200
@@ -337,7 +337,7 @@
definition
"fun" :: "exp \<Rightarrow> nat" where
- "fun X = contents (\<Union>U \<in> Rep_Exp X. {freefun U})"
+ "fun X = the_elem (\<Union>U \<in> Rep_Exp X. {freefun U})"
lemma fun_respects: "(%U. {freefun U}) respects exprel"
by (simp add: congruent_def exprel_imp_eq_freefun)
@@ -349,7 +349,7 @@
definition
args :: "exp \<Rightarrow> exp list" where
- "args X = contents (\<Union>U \<in> Rep_Exp X. {Abs_ExpList (freeargs U)})"
+ "args X = the_elem (\<Union>U \<in> Rep_Exp X. {Abs_ExpList (freeargs U)})"
text{*This result can probably be generalized to arbitrary equivalence
relations, but with little benefit here.*}
@@ -384,7 +384,7 @@
definition
discrim :: "exp \<Rightarrow> int" where
- "discrim X = contents (\<Union>U \<in> Rep_Exp X. {freediscrim U})"
+ "discrim X = the_elem (\<Union>U \<in> Rep_Exp X. {freediscrim U})"
lemma discrim_respects: "(\<lambda>U. {freediscrim U}) respects exprel"
by (simp add: congruent_def exprel_imp_eq_freediscrim)
--- a/src/HOL/Int.thy Fri Oct 01 14:15:49 2010 +0200
+++ b/src/HOL/Int.thy Fri Oct 01 16:05:25 2010 +0200
@@ -283,7 +283,7 @@
begin
definition of_int :: "int \<Rightarrow> 'a" where
- "of_int z = contents (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
+ "of_int z = the_elem (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
proof -
@@ -389,7 +389,7 @@
subsection {* Magnitude of an Integer, as a Natural Number: @{text nat} *}
definition nat :: "int \<Rightarrow> nat" where
- "nat z = contents (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
+ "nat z = the_elem (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
proof -
--- a/src/HOL/Library/Fraction_Field.thy Fri Oct 01 14:15:49 2010 +0200
+++ b/src/HOL/Library/Fraction_Field.thy Fri Oct 01 16:05:25 2010 +0200
@@ -319,7 +319,7 @@
definition
le_fract_def:
- "q \<le> r \<longleftrightarrow> contents (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r.
+ "q \<le> r \<longleftrightarrow> the_elem (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r.
{(fst x * snd y)*(snd x * snd y) \<le> (fst y * snd x)*(snd x * snd y)})"
definition
--- a/src/HOL/Probability/Lebesgue_Integration.thy Fri Oct 01 14:15:49 2010 +0200
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Fri Oct 01 16:05:25 2010 +0200
@@ -495,7 +495,7 @@
lemma (in measure_space) simple_function_partition:
assumes "simple_function f" and "simple_function g"
- shows "simple_integral f = (\<Sum>A\<in>(\<lambda>x. f -` {f x} \<inter> g -` {g x} \<inter> space M) ` space M. contents (f`A) * \<mu> A)"
+ shows "simple_integral f = (\<Sum>A\<in>(\<lambda>x. f -` {f x} \<inter> g -` {g x} \<inter> space M) ` space M. the_elem (f`A) * \<mu> A)"
(is "_ = setsum _ (?p ` space M)")
proof-
let "?sub x" = "?p ` (f -` {x} \<inter> space M)"
@@ -530,18 +530,18 @@
unfolding simple_integral_def
by (subst setsum_Sigma[symmetric],
auto intro!: setsum_cong simp: setsum_right_distrib[symmetric])
- also have "\<dots> = (\<Sum>A\<in>?p ` space M. contents (f`A) * \<mu> A)"
+ also have "\<dots> = (\<Sum>A\<in>?p ` space M. the_elem (f`A) * \<mu> A)"
proof -
have [simp]: "\<And>x. x \<in> space M \<Longrightarrow> f ` ?p x = {f x}" by (auto intro!: imageI)
- have "(\<lambda>A. (contents (f ` A), A)) ` ?p ` space M
+ have "(\<lambda>A. (the_elem (f ` A), A)) ` ?p ` space M
= (\<lambda>x. (f x, ?p x)) ` space M"
proof safe
fix x assume "x \<in> space M"
- thus "(f x, ?p x) \<in> (\<lambda>A. (contents (f`A), A)) ` ?p ` space M"
+ thus "(f x, ?p x) \<in> (\<lambda>A. (the_elem (f`A), A)) ` ?p ` space M"
by (auto intro!: image_eqI[of _ _ "?p x"])
qed auto
thus ?thesis
- apply (auto intro!: setsum_reindex_cong[of "\<lambda>A. (contents (f`A), A)"] inj_onI)
+ apply (auto intro!: setsum_reindex_cong[of "\<lambda>A. (the_elem (f`A), A)"] inj_onI)
apply (rule_tac x="xa" in image_eqI)
by simp_all
qed
@@ -602,7 +602,7 @@
fix x let ?S = "g -` {g x} \<inter> f -` {f x} \<inter> space M"
assume "x \<in> space M"
hence "f ` ?S = {f x}" "g ` ?S = {g x}" by auto
- thus "contents (f`?S) * \<mu> ?S \<le> contents (g`?S) * \<mu> ?S"
+ thus "the_elem (f`?S) * \<mu> ?S \<le> the_elem (g`?S) * \<mu> ?S"
using mono[OF `x \<in> space M`] by (auto intro!: mult_right_mono)
qed
--- a/src/HOL/Rat.thy Fri Oct 01 14:15:49 2010 +0200
+++ b/src/HOL/Rat.thy Fri Oct 01 16:05:25 2010 +0200
@@ -470,7 +470,7 @@
definition
le_rat_def:
- "q \<le> r \<longleftrightarrow> contents (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
+ "q \<le> r \<longleftrightarrow> the_elem (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
{(fst x * snd y) * (snd x * snd y) \<le> (fst y * snd x) * (snd x * snd y)})"
lemma le_rat [simp]:
@@ -775,7 +775,7 @@
begin
definition of_rat :: "rat \<Rightarrow> 'a" where
- "of_rat q = contents (\<Union>(a,b) \<in> Rep_Rat q. {of_int a / of_int b})"
+ "of_rat q = the_elem (\<Union>(a,b) \<in> Rep_Rat q. {of_int a / of_int b})"
end
--- a/src/HOL/Set.thy Fri Oct 01 14:15:49 2010 +0200
+++ b/src/HOL/Set.thy Fri Oct 01 16:05:25 2010 +0200
@@ -1656,11 +1656,11 @@
subsubsection {* Getting the Contents of a Singleton Set *}
-definition contents :: "'a set \<Rightarrow> 'a" where
- "contents X = (THE x. X = {x})"
+definition the_elem :: "'a set \<Rightarrow> 'a" where
+ "the_elem X = (THE x. X = {x})"
-lemma contents_eq [simp]: "contents {x} = x"
- by (simp add: contents_def)
+lemma the_elem_eq [simp]: "the_elem {x} = x"
+ by (simp add: the_elem_def)
subsubsection {* Least value operator *}
--- a/src/HOL/Word/Misc_Numeric.thy Fri Oct 01 14:15:49 2010 +0200
+++ b/src/HOL/Word/Misc_Numeric.thy Fri Oct 01 16:05:25 2010 +0200
@@ -8,8 +8,8 @@
imports Main Parity
begin
-lemma contentsI: "y = {x} ==> contents y = x"
- unfolding contents_def by auto -- {* FIXME move *}
+lemma the_elemI: "y = {x} ==> the_elem y = x"
+ by simp
lemmas split_split = prod.split
lemmas split_split_asm = prod.split_asm
--- a/src/HOL/Word/Word.thy Fri Oct 01 14:15:49 2010 +0200
+++ b/src/HOL/Word/Word.thy Fri Oct 01 16:05:25 2010 +0200
@@ -1772,7 +1772,7 @@
lemma word_of_int: "of_int = word_of_int"
apply (rule ext)
apply (unfold of_int_def)
- apply (rule contentsI)
+ apply (rule the_elemI)
apply safe
apply (simp_all add: word_of_nat word_of_int_homs)
defer
--- a/src/HOL/ZF/Games.thy Fri Oct 01 14:15:49 2010 +0200
+++ b/src/HOL/ZF/Games.thy Fri Oct 01 16:05:25 2010 +0200
@@ -859,10 +859,10 @@
Pg_less_def: "G < H \<longleftrightarrow> G \<le> H \<and> G \<noteq> (H::Pg)"
definition
- Pg_minus_def: "- G = contents (\<Union> g \<in> Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})"
+ Pg_minus_def: "- G = the_elem (\<Union> g \<in> Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})"
definition
- Pg_plus_def: "G + H = contents (\<Union> g \<in> Rep_Pg G. \<Union> h \<in> Rep_Pg H. {Abs_Pg (eq_game_rel `` {plus_game g h})})"
+ Pg_plus_def: "G + H = the_elem (\<Union> g \<in> Rep_Pg G. \<Union> h \<in> Rep_Pg H. {Abs_Pg (eq_game_rel `` {plus_game g h})})"
definition
Pg_diff_def: "G - H = G + (- (H::Pg))"
--- a/src/HOL/ex/Dedekind_Real.thy Fri Oct 01 14:15:49 2010 +0200
+++ b/src/HOL/ex/Dedekind_Real.thy Fri Oct 01 16:05:25 2010 +0200
@@ -1183,11 +1183,11 @@
definition
real_add_def: "z + w =
- contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
+ the_elem (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
{ Abs_Real(realrel``{(x+u, y+v)}) })"
definition
- real_minus_def: "- r = contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
+ real_minus_def: "- r = the_elem (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
definition
real_diff_def: "r - (s::real) = r + - s"
@@ -1195,7 +1195,7 @@
definition
real_mult_def:
"z * w =
- contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
+ the_elem (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
{ Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })"
definition