# 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 \ carrier (G A_Mod (a_kernel G H h))" - shows "contents (h`X) \ carrier H" -by (rule group_hom.FactGroup_contents_mem[OF a_group_hom, + shows "the_elem (h`X) \ 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: - "(\X. contents (h`X)) \ hom (G A_Mod (a_kernel G H h)) + "(\X. the_elem (h`X)) \ hom (G A_Mod (a_kernel G H h)) \carrier = carrier H, mult = add H, one = zero H\" 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 (\X. contents (h ` X)) (carrier (G A_Mod a_kernel G H h))" + "inj_on (\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 "(\X. contents (h ` X)) ` carrier (G A_Mod a_kernel G H h) = carrier H" + shows "(\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 - \ (\X. contents (h`X)) \ (G A_Mod (a_kernel G H h)) \ + \ (\X. the_elem (h`X)) \ (G A_Mod (a_kernel G H h)) \ (| 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 \ carrier (G Mod (kernel G H h))" - shows "contents (h`X) \ carrier H" + shows "the_elem (h`X) \ carrier H" proof - from X obtain g where g: "g \ carrier G" @@ -937,8 +937,8 @@ qed lemma (in group_hom) FactGroup_hom: - "(\X. contents (h`X)) \ 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) + "(\X. the_elem (h`X)) \ 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 \ 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) \\<^bsub>H\<^esub> contents (h ` X')" + thus "the_elem (h ` (X <#> X')) = the_elem (h ` X) \\<^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 (\X. contents (h ` X)) (carrier (G Mod kernel G H h))" + "inj_on (\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 \ carrier (G Mod kernel G H h)" @@ -983,7 +983,7 @@ by (auto simp add: FactGroup_def RCOSETS_def) hence all: "\x\X. h x = h g" "\x\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 "(\X. contents (h ` X)) ` carrier (G Mod kernel G H h) = carrier H" + shows "(\X. the_elem (h ` X)) ` carrier (G Mod kernel G H h) = carrier H" proof - show "(\X. contents (h ` X)) ` carrier (G Mod kernel G H h) \ carrier H" - by (auto simp add: FactGroup_contents_mem) - show "carrier H \ (\X. contents (h ` X)) ` carrier (G Mod kernel G H h)" + show "(\X. the_elem (h ` X)) ` carrier (G Mod kernel G H h) \ carrier H" + by (auto simp add: FactGroup_the_elem_mem) + show "carrier H \ (\X. the_elem (h ` X)) ` carrier (G Mod kernel G H h)" proof fix y assume y: "y \ carrier H" @@ -1005,7 +1005,7 @@ by (blast elim: equalityE) hence "(\x\kernel G H h #> g. {h x}) = {y}" by (auto simp add: y kernel_def r_coset_def) - with g show "y \ (\X. contents (h ` X)) ` carrier (G Mod kernel G H h)" + with g show "y \ (\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 - \ (\X. contents (h`X)) \ (G Mod (kernel G H h)) \ H" + \ (\X. the_elem (h`X)) \ (G Mod (kernel G H h)) \ 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 \ int" where - "discrim X = contents (\U \ Rep_Msg X. {freediscrim U})" + "discrim X = the_elem (\U \ Rep_Msg X. {freediscrim U})" lemma discrim_congruent: "(\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 \ nat" where - "fun X = contents (\U \ Rep_Exp X. {freefun U})" + "fun X = the_elem (\U \ 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 \ exp list" where - "args X = contents (\U \ Rep_Exp X. {Abs_ExpList (freeargs U)})" + "args X = the_elem (\U \ 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 \ int" where - "discrim X = contents (\U \ Rep_Exp X. {freediscrim U})" + "discrim X = the_elem (\U \ Rep_Exp X. {freediscrim U})" lemma discrim_respects: "(\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 \ 'a" where - "of_int z = contents (\(i, j) \ Rep_Integ z. { of_nat i - of_nat j })" + "of_int z = the_elem (\(i, j) \ 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 \ nat" where - "nat z = contents (\(x, y) \ Rep_Integ z. {x-y})" + "nat z = the_elem (\(x, y) \ 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 \ r \ contents (\x \ Rep_fract q. \y \ Rep_fract r. + "q \ r \ the_elem (\x \ Rep_fract q. \y \ Rep_fract r. {(fst x * snd y)*(snd x * snd y) \ (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 = (\A\(\x. f -` {f x} \ g -` {g x} \ space M) ` space M. contents (f`A) * \ A)" + shows "simple_integral f = (\A\(\x. f -` {f x} \ g -` {g x} \ space M) ` space M. the_elem (f`A) * \ A)" (is "_ = setsum _ (?p ` space M)") proof- let "?sub x" = "?p ` (f -` {x} \ 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 "\ = (\A\?p ` space M. contents (f`A) * \ A)" + also have "\ = (\A\?p ` space M. the_elem (f`A) * \ A)" proof - have [simp]: "\x. x \ space M \ f ` ?p x = {f x}" by (auto intro!: imageI) - have "(\A. (contents (f ` A), A)) ` ?p ` space M + have "(\A. (the_elem (f ` A), A)) ` ?p ` space M = (\x. (f x, ?p x)) ` space M" proof safe fix x assume "x \ space M" - thus "(f x, ?p x) \ (\A. (contents (f`A), A)) ` ?p ` space M" + thus "(f x, ?p x) \ (\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 "\A. (contents (f`A), A)"] inj_onI) + apply (auto intro!: setsum_reindex_cong[of "\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} \ f -` {f x} \ space M" assume "x \ space M" hence "f ` ?S = {f x}" "g ` ?S = {g x}" by auto - thus "contents (f`?S) * \ ?S \ contents (g`?S) * \ ?S" + thus "the_elem (f`?S) * \ ?S \ the_elem (g`?S) * \ ?S" using mono[OF `x \ 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 \ r \ contents (\x \ Rep_Rat q. \y \ Rep_Rat r. + "q \ r \ the_elem (\x \ Rep_Rat q. \y \ Rep_Rat r. {(fst x * snd y) * (snd x * snd y) \ (fst y * snd x) * (snd x * snd y)})" lemma le_rat [simp]: @@ -775,7 +775,7 @@ begin definition of_rat :: "rat \ 'a" where - "of_rat q = contents (\(a,b) \ Rep_Rat q. {of_int a / of_int b})" + "of_rat q = the_elem (\(a,b) \ 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 \ 'a" where - "contents X = (THE x. X = {x})" +definition the_elem :: "'a set \ '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 \ G \ H \ G \ (H::Pg)" definition - Pg_minus_def: "- G = contents (\ g \ Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})" + Pg_minus_def: "- G = the_elem (\ g \ Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})" definition - Pg_plus_def: "G + H = contents (\ g \ Rep_Pg G. \ h \ Rep_Pg H. {Abs_Pg (eq_game_rel `` {plus_game g h})})" + Pg_plus_def: "G + H = the_elem (\ g \ Rep_Pg G. \ h \ 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 (\(x,y) \ Rep_Real(z). \(u,v) \ Rep_Real(w). + the_elem (\(x,y) \ Rep_Real(z). \(u,v) \ Rep_Real(w). { Abs_Real(realrel``{(x+u, y+v)}) })" definition - real_minus_def: "- r = contents (\(x,y) \ Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })" + real_minus_def: "- r = the_elem (\(x,y) \ 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 (\(x,y) \ Rep_Real(z). \(u,v) \ Rep_Real(w). + the_elem (\(x,y) \ Rep_Real(z). \(u,v) \ Rep_Real(w). { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })" definition