# HG changeset patch
# User haftmann
# Date 1285941925 -7200
# Node ID 10097e0a9dbd4534b2f846a1a0c24827764add3f
# Parent  ff9e9d5ac17173edbe51a8d3b4554f9ebfbecb0a
constant `contents` renamed to `the_elem`

diff -r ff9e9d5ac171 -r 10097e0a9dbd NEWS
--- 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
diff -r ff9e9d5ac171 -r 10097e0a9dbd src/HOL/Algebra/AbelCoset.thy
--- 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])
diff -r ff9e9d5ac171 -r 10097e0a9dbd src/HOL/Algebra/Coset.thy
--- 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) 
 
diff -r ff9e9d5ac171 -r 10097e0a9dbd src/HOL/Induct/QuoDataType.thy
--- 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) 
diff -r ff9e9d5ac171 -r 10097e0a9dbd src/HOL/Induct/QuoNestedDataType.thy
--- 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) 
diff -r ff9e9d5ac171 -r 10097e0a9dbd src/HOL/Int.thy
--- 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 -
diff -r ff9e9d5ac171 -r 10097e0a9dbd src/HOL/Library/Fraction_Field.thy
--- 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
diff -r ff9e9d5ac171 -r 10097e0a9dbd src/HOL/Probability/Lebesgue_Integration.thy
--- 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
 
diff -r ff9e9d5ac171 -r 10097e0a9dbd src/HOL/Rat.thy
--- 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
 
diff -r ff9e9d5ac171 -r 10097e0a9dbd src/HOL/Set.thy
--- 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 *}
diff -r ff9e9d5ac171 -r 10097e0a9dbd src/HOL/Word/Misc_Numeric.thy
--- 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
diff -r ff9e9d5ac171 -r 10097e0a9dbd src/HOL/Word/Word.thy
--- 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
diff -r ff9e9d5ac171 -r 10097e0a9dbd src/HOL/ZF/Games.thy
--- 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))"
diff -r ff9e9d5ac171 -r 10097e0a9dbd src/HOL/ex/Dedekind_Real.thy
--- 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