# HG changeset patch # User haftmann # Date 1305884674 -7200 # Node ID 585c8333b0da0c43efda403265c9739861b0397f # Parent 36abaf4cce1f6f95f49a8e3a3964b6afca5d3ef9# Parent 1c0b99f950d977d4e0df39d7dfe27e5053f661eb merged diff -r 36abaf4cce1f -r 585c8333b0da src/HOL/Big_Operators.thy --- a/src/HOL/Big_Operators.thy Fri May 20 09:31:36 2011 +0200 +++ b/src/HOL/Big_Operators.thy Fri May 20 11:44:34 2011 +0200 @@ -1205,7 +1205,7 @@ proof qed (rule inf_assoc inf_commute inf_idem)+ lemma fold_inf_insert[simp]: "finite A \ fold inf b (insert a A) = inf a (fold inf b A)" -by(rule fun_left_comm_idem.fold_insert_idem[OF ab_semigroup_idem_mult.fun_left_comm_idem[OF ab_semigroup_idem_mult_inf]]) +by(rule comp_fun_idem.fold_insert_idem[OF ab_semigroup_idem_mult.comp_fun_idem[OF ab_semigroup_idem_mult_inf]]) lemma inf_le_fold_inf: "finite A \ ALL a:A. b \ a \ inf b c \ fold inf c A" by (induct pred: finite) (auto intro: le_infI1) diff -r 36abaf4cce1f -r 585c8333b0da src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Fri May 20 09:31:36 2011 +0200 +++ b/src/HOL/Finite_Set.thy Fri May 20 11:44:34 2011 +0200 @@ -532,13 +532,13 @@ if @{text f} is ``left-commutative'': *} -locale fun_left_comm = +locale comp_fun_commute = fixes f :: "'a \ 'b \ 'b" - assumes commute_comp: "f y \ f x = f x \ f y" + assumes comp_fun_commute: "f y \ f x = f x \ f y" begin lemma fun_left_comm: "f x (f y z) = f y (f x z)" - using commute_comp by (simp add: fun_eq_iff) + using comp_fun_commute by (simp add: fun_eq_iff) end @@ -565,7 +565,7 @@ subsubsection{*From @{const fold_graph} to @{term fold}*} -context fun_left_comm +context comp_fun_commute begin lemma fold_graph_insertE_aux: @@ -671,12 +671,12 @@ text{* A simplified version for idempotent functions: *} -locale fun_left_comm_idem = fun_left_comm + - assumes fun_comp_idem: "f x o f x = f x" +locale comp_fun_idem = comp_fun_commute + + assumes comp_fun_idem: "f x o f x = f x" begin lemma fun_left_idem: "f x (f x z) = f x z" - using fun_comp_idem by (simp add: fun_eq_iff) + using comp_fun_idem by (simp add: fun_eq_iff) lemma fold_insert_idem: assumes fin: "finite A" @@ -700,33 +700,33 @@ subsubsection {* Expressing set operations via @{const fold} *} -lemma (in fun_left_comm) comp_comp_fun_commute: - "fun_left_comm (f \ g)" +lemma (in comp_fun_commute) comp_comp_fun_commute: + "comp_fun_commute (f \ g)" proof -qed (simp_all add: commute_comp) +qed (simp_all add: comp_fun_commute) -lemma (in fun_left_comm_idem) comp_comp_fun_idem: - "fun_left_comm_idem (f \ g)" - by (rule fun_left_comm_idem.intro, rule comp_comp_fun_commute, unfold_locales) - (simp_all add: fun_comp_idem) +lemma (in comp_fun_idem) comp_comp_fun_idem: + "comp_fun_idem (f \ g)" + by (rule comp_fun_idem.intro, rule comp_comp_fun_commute, unfold_locales) + (simp_all add: comp_fun_idem) -lemma fun_left_comm_idem_insert: - "fun_left_comm_idem insert" +lemma comp_fun_idem_insert: + "comp_fun_idem insert" proof qed auto -lemma fun_left_comm_idem_remove: - "fun_left_comm_idem (\x A. A - {x})" +lemma comp_fun_idem_remove: + "comp_fun_idem (\x A. A - {x})" proof qed auto -lemma (in semilattice_inf) fun_left_comm_idem_inf: - "fun_left_comm_idem inf" +lemma (in semilattice_inf) comp_fun_idem_inf: + "comp_fun_idem inf" proof qed (auto simp add: inf_left_commute) -lemma (in semilattice_sup) fun_left_comm_idem_sup: - "fun_left_comm_idem sup" +lemma (in semilattice_sup) comp_fun_idem_sup: + "comp_fun_idem sup" proof qed (auto simp add: sup_left_commute) @@ -734,7 +734,7 @@ assumes "finite A" shows "A \ B = fold insert B A" proof - - interpret fun_left_comm_idem insert by (fact fun_left_comm_idem_insert) + interpret comp_fun_idem insert by (fact comp_fun_idem_insert) from `finite A` show ?thesis by (induct A arbitrary: B) simp_all qed @@ -742,7 +742,7 @@ assumes "finite A" shows "B - A = fold (\x A. A - {x}) B A" proof - - interpret fun_left_comm_idem "\x A. A - {x}" by (fact fun_left_comm_idem_remove) + interpret comp_fun_idem "\x A. A - {x}" by (fact comp_fun_idem_remove) from `finite A` show ?thesis by (induct A arbitrary: B) auto qed @@ -753,7 +753,7 @@ assumes "finite A" shows "inf B (Inf A) = fold inf B A" proof - - interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf) + interpret comp_fun_idem inf by (fact comp_fun_idem_inf) from `finite A` show ?thesis by (induct A arbitrary: B) (simp_all add: Inf_insert inf_commute fold_fun_comm) qed @@ -762,7 +762,7 @@ assumes "finite A" shows "sup B (Sup A) = fold sup B A" proof - - interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup) + interpret comp_fun_idem sup by (fact comp_fun_idem_sup) from `finite A` show ?thesis by (induct A arbitrary: B) (simp_all add: Sup_insert sup_commute fold_fun_comm) qed @@ -781,8 +781,8 @@ assumes "finite A" shows "inf B (INFI A f) = fold (\A. inf (f A)) B A" (is "?inf = ?fold") proof (rule sym) - interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf) - interpret fun_left_comm_idem "inf \ f" by (fact comp_comp_fun_idem) + interpret comp_fun_idem inf by (fact comp_fun_idem_inf) + interpret comp_fun_idem "inf \ f" by (fact comp_comp_fun_idem) from `finite A` have "fold (inf \ f) B A = ?inf" by (induct A arbitrary: B) (simp_all add: INFI_def Inf_insert inf_left_commute) @@ -793,8 +793,8 @@ assumes "finite A" shows "sup B (SUPR A f) = fold (\A. sup (f A)) B A" (is "?sup = ?fold") proof (rule sym) - interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup) - interpret fun_left_comm_idem "sup \ f" by (fact comp_comp_fun_idem) + interpret comp_fun_idem sup by (fact comp_fun_idem_sup) + interpret comp_fun_idem "sup \ f" by (fact comp_comp_fun_idem) from `finite A` have "fold (sup \ f) B A = ?sup" by (induct A arbitrary: B) (simp_all add: SUPR_def Sup_insert sup_left_commute) @@ -829,7 +829,7 @@ assumes "finite A" and "a \ A" shows "fold_image times g z (insert a A) = g a * (fold_image times g z A)" proof - - interpret I: fun_left_comm "%x y. (g x) * y" proof + interpret I: comp_fun_commute "%x y. (g x) * y" proof qed (simp add: fun_eq_iff mult_ac) show ?thesis using assms by (simp add: fold_image_def) qed @@ -1052,14 +1052,14 @@ context ab_semigroup_mult begin -lemma fun_left_comm: "fun_left_comm (op *)" proof +lemma comp_fun_commute: "comp_fun_commute (op *)" proof qed (simp add: fun_eq_iff mult_ac) lemma fold_graph_insert_swap: assumes fold: "fold_graph times (b::'a) A y" and "b \ A" shows "fold_graph times z (insert b A) (z * y)" proof - - interpret fun_left_comm "op *::'a \ 'a \ 'a" by (rule fun_left_comm) + interpret comp_fun_commute "op *::'a \ 'a \ 'a" by (rule comp_fun_commute) from assms show ?thesis proof (induct rule: fold_graph.induct) case emptyI show ?case by (subst mult_commute [of z b], fast) @@ -1099,7 +1099,7 @@ lemma fold1_eq_fold: assumes "finite A" "a \ A" shows "fold1 times (insert a A) = fold times a A" proof - - interpret fun_left_comm "op *::'a \ 'a \ 'a" by (rule fun_left_comm) + interpret comp_fun_commute "op *::'a \ 'a \ 'a" by (rule comp_fun_commute) from assms show ?thesis apply (simp add: fold1_def fold_def) apply (rule the_equality) @@ -1126,7 +1126,7 @@ assumes nonempty: "A \ {}" and A: "finite A" "x \ A" shows "fold1 times (insert x A) = x * fold1 times A" proof - - interpret fun_left_comm "op *::'a \ 'a \ 'a" by (rule fun_left_comm) + interpret comp_fun_commute "op *::'a \ 'a \ 'a" by (rule comp_fun_commute) from nonempty obtain a A' where "A = insert a A' & a ~: A'" by (auto simp add: nonempty_iff) with A show ?thesis @@ -1138,15 +1138,15 @@ context ab_semigroup_idem_mult begin -lemma fun_left_comm_idem: "fun_left_comm_idem (op *)" proof +lemma comp_fun_idem: "comp_fun_idem (op *)" proof qed (simp_all add: fun_eq_iff mult_left_commute) lemma fold1_insert_idem [simp]: assumes nonempty: "A \ {}" and A: "finite A" shows "fold1 times (insert x A) = x * fold1 times A" proof - - interpret fun_left_comm_idem "op *::'a \ 'a \ 'a" - by (rule fun_left_comm_idem) + interpret comp_fun_idem "op *::'a \ 'a \ 'a" + by (rule comp_fun_idem) from nonempty obtain a A' where A': "A = insert a A' & a ~: A'" by (auto simp add: nonempty_iff) show ?thesis @@ -1191,7 +1191,7 @@ case False with assms show ?thesis by (simp add: fold1_eq_fold) next - interpret fun_left_comm_idem times by (fact fun_left_comm_idem) + interpret comp_fun_idem times by (fact comp_fun_idem) case True then obtain b B where A: "A = insert a B" and "a \ B" by (rule set_insert) with assms have "finite B" by auto @@ -1315,7 +1315,7 @@ locale folding = fixes f :: "'a \ 'b \ 'b" fixes F :: "'a set \ 'b \ 'b" - assumes commute_comp: "f y \ f x = f x \ f y" + assumes comp_fun_commute: "f y \ f x = f x \ f y" assumes eq_fold: "finite A \ F A s = fold f s A" begin @@ -1327,8 +1327,8 @@ assumes "finite A" and "x \ A" shows "F (insert x A) = F A \ f x" proof - - interpret fun_left_comm f proof - qed (insert commute_comp, simp add: fun_eq_iff) + interpret comp_fun_commute f proof + qed (insert comp_fun_commute, simp add: fun_eq_iff) from fold_insert2 assms have "\s. fold f s (insert x A) = fold f (f x s) A" . with `finite A` show ?thesis by (simp add: eq_fold fun_eq_iff) @@ -1351,38 +1351,38 @@ lemma commute_left_comp: "f y \ (f x \ g) = f x \ (f y \ g)" - by (simp add: o_assoc commute_comp) + by (simp add: o_assoc comp_fun_commute) -lemma commute_comp': +lemma comp_fun_commute': assumes "finite A" shows "f x \ F A = F A \ f x" using assms by (induct A) - (simp, simp del: o_apply add: o_assoc, simp del: o_apply add: o_assoc [symmetric] commute_comp) + (simp, simp del: o_apply add: o_assoc, simp del: o_apply add: o_assoc [symmetric] comp_fun_commute) lemma commute_left_comp': assumes "finite A" shows "f x \ (F A \ g) = F A \ (f x \ g)" - using assms by (simp add: o_assoc commute_comp') + using assms by (simp add: o_assoc comp_fun_commute') -lemma commute_comp'': +lemma comp_fun_commute'': assumes "finite A" and "finite B" shows "F B \ F A = F A \ F B" using assms by (induct A) - (simp_all add: o_assoc, simp add: o_assoc [symmetric] commute_comp') + (simp_all add: o_assoc, simp add: o_assoc [symmetric] comp_fun_commute') lemma commute_left_comp'': assumes "finite A" and "finite B" shows "F B \ (F A \ g) = F A \ (F B \ g)" - using assms by (simp add: o_assoc commute_comp'') + using assms by (simp add: o_assoc comp_fun_commute'') -lemmas commute_comps = o_assoc [symmetric] commute_comp commute_left_comp - commute_comp' commute_left_comp' commute_comp'' commute_left_comp'' +lemmas comp_fun_commutes = o_assoc [symmetric] comp_fun_commute commute_left_comp + comp_fun_commute' commute_left_comp' comp_fun_commute'' commute_left_comp'' lemma union_inter: assumes "finite A" and "finite B" shows "F (A \ B) \ F (A \ B) = F A \ F B" using assms by (induct A) - (simp_all del: o_apply add: insert_absorb Int_insert_left commute_comps, + (simp_all del: o_apply add: insert_absorb Int_insert_left comp_fun_commutes, simp add: o_assoc) lemma union: @@ -1411,7 +1411,7 @@ assumes "finite A" and "x \ A" shows "F A \ f x = F A" using assms by (induct A) - (auto simp add: commute_comps idem_comp, simp add: commute_left_comp' [symmetric] commute_comp') + (auto simp add: comp_fun_commutes idem_comp, simp add: commute_left_comp' [symmetric] comp_fun_commute') lemma subset_comp_idem: assumes "finite A" and "B \ A" @@ -1460,7 +1460,7 @@ assumes "finite A" and "x \ A" shows "F (insert x A) = g x * F A" proof - - interpret fun_left_comm "%x y. (g x) * y" proof + interpret comp_fun_commute "%x y. (g x) * y" proof qed (simp add: ac_simps fun_eq_iff) with assms have "fold_image (op *) g 1 (insert x A) = g x * fold_image (op *) g 1 A" by (simp add: fold_image_def) @@ -1697,8 +1697,8 @@ with `finite A` have "finite B" by simp interpret fold: folding "op *" "\a b. fold (op *) b a" proof qed (simp_all add: fun_eq_iff ac_simps) - thm fold.commute_comp' [of B b, simplified fun_eq_iff, simplified] - from `finite B` fold.commute_comp' [of B x] + thm fold.comp_fun_commute' [of B b, simplified fun_eq_iff, simplified] + from `finite B` fold.comp_fun_commute' [of B x] have "op * x \ (\b. fold op * b B) = (\b. fold op * b B) \ op * x" by simp then have A: "x * fold op * b B = fold op * (b * x) B" by (simp add: fun_eq_iff commute) from `finite B` * fold.insert [of B b] diff -r 36abaf4cce1f -r 585c8333b0da src/HOL/GCD.thy --- a/src/HOL/GCD.thy Fri May 20 09:31:36 2011 +0200 +++ b/src/HOL/GCD.thy Fri May 20 11:44:34 2011 +0200 @@ -1436,16 +1436,16 @@ lemma lcm_proj2_iff_int[simp]: "lcm m n = abs(n::int) \ m dvd n" by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int) -lemma fun_left_comm_idem_gcd_nat: "fun_left_comm_idem (gcd :: nat\nat\nat)" +lemma comp_fun_idem_gcd_nat: "comp_fun_idem (gcd :: nat\nat\nat)" proof qed (auto simp add: gcd_ac_nat) -lemma fun_left_comm_idem_gcd_int: "fun_left_comm_idem (gcd :: int\int\int)" +lemma comp_fun_idem_gcd_int: "comp_fun_idem (gcd :: int\int\int)" proof qed (auto simp add: gcd_ac_int) -lemma fun_left_comm_idem_lcm_nat: "fun_left_comm_idem (lcm :: nat\nat\nat)" +lemma comp_fun_idem_lcm_nat: "comp_fun_idem (lcm :: nat\nat\nat)" proof qed (auto simp add: lcm_ac_nat) -lemma fun_left_comm_idem_lcm_int: "fun_left_comm_idem (lcm :: int\int\int)" +lemma comp_fun_idem_lcm_int: "comp_fun_idem (lcm :: int\int\int)" proof qed (auto simp add: lcm_ac_int) @@ -1516,8 +1516,8 @@ assumes "finite N" shows "Lcm (insert (n::nat) N) = lcm n (Lcm N)" proof - - interpret fun_left_comm_idem "lcm::nat\nat\nat" - by (rule fun_left_comm_idem_lcm_nat) + interpret comp_fun_idem "lcm::nat\nat\nat" + by (rule comp_fun_idem_lcm_nat) from assms show ?thesis by(simp add: Lcm_def) qed @@ -1525,8 +1525,8 @@ assumes "finite N" shows "Lcm (insert (n::int) N) = lcm n (Lcm N)" proof - - interpret fun_left_comm_idem "lcm::int\int\int" - by (rule fun_left_comm_idem_lcm_int) + interpret comp_fun_idem "lcm::int\int\int" + by (rule comp_fun_idem_lcm_int) from assms show ?thesis by(simp add: Lcm_def) qed @@ -1534,8 +1534,8 @@ assumes "finite N" shows "Gcd (insert (n::nat) N) = gcd n (Gcd N)" proof - - interpret fun_left_comm_idem "gcd::nat\nat\nat" - by (rule fun_left_comm_idem_gcd_nat) + interpret comp_fun_idem "gcd::nat\nat\nat" + by (rule comp_fun_idem_gcd_nat) from assms show ?thesis by(simp add: Gcd_def) qed @@ -1543,8 +1543,8 @@ assumes "finite N" shows "Gcd (insert (n::int) N) = gcd n (Gcd N)" proof - - interpret fun_left_comm_idem "gcd::int\int\int" - by (rule fun_left_comm_idem_gcd_int) + interpret comp_fun_idem "gcd::int\int\int" + by (rule comp_fun_idem_gcd_int) from assms show ?thesis by(simp add: Gcd_def) qed @@ -1685,28 +1685,28 @@ lemma Lcm_set_nat [code_unfold]: "Lcm (set ns) = foldl lcm (1::nat) ns" proof - - interpret fun_left_comm_idem "lcm::nat\nat\nat" by (rule fun_left_comm_idem_lcm_nat) + interpret comp_fun_idem "lcm::nat\nat\nat" by (rule comp_fun_idem_lcm_nat) show ?thesis by(simp add: Lcm_def fold_set lcm_commute_nat) qed lemma Lcm_set_int [code_unfold]: "Lcm (set is) = foldl lcm (1::int) is" proof - - interpret fun_left_comm_idem "lcm::int\int\int" by (rule fun_left_comm_idem_lcm_int) + interpret comp_fun_idem "lcm::int\int\int" by (rule comp_fun_idem_lcm_int) show ?thesis by(simp add: Lcm_def fold_set lcm_commute_int) qed lemma Gcd_set_nat [code_unfold]: "Gcd (set ns) = foldl gcd (0::nat) ns" proof - - interpret fun_left_comm_idem "gcd::nat\nat\nat" by (rule fun_left_comm_idem_gcd_nat) + interpret comp_fun_idem "gcd::nat\nat\nat" by (rule comp_fun_idem_gcd_nat) show ?thesis by(simp add: Gcd_def fold_set gcd_commute_nat) qed lemma Gcd_set_int [code_unfold]: "Gcd (set ns) = foldl gcd (0::int) ns" proof - - interpret fun_left_comm_idem "gcd::int\int\int" by (rule fun_left_comm_idem_gcd_int) + interpret comp_fun_idem "gcd::int\int\int" by (rule comp_fun_idem_gcd_int) show ?thesis by(simp add: Gcd_def fold_set gcd_commute_int) qed diff -r 36abaf4cce1f -r 585c8333b0da src/HOL/Library/More_List.thy --- a/src/HOL/Library/More_List.thy Fri May 20 09:31:36 2011 +0200 +++ b/src/HOL/Library/More_List.thy Fri May 20 11:44:34 2011 +0200 @@ -158,11 +158,11 @@ text {* @{const Finite_Set.fold} and @{const fold} *} -lemma (in fun_left_comm) fold_set_remdups: +lemma (in comp_fun_commute) fold_set_remdups: "Finite_Set.fold f y (set xs) = fold f (remdups xs) y" by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb) -lemma (in fun_left_comm_idem) fold_set: +lemma (in comp_fun_idem) fold_set: "Finite_Set.fold f y (set xs) = fold f xs y" by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm) @@ -170,7 +170,7 @@ assumes "xs \ []" shows "Finite_Set.fold1 times (set xs) = fold times (tl xs) (hd xs)" proof - - interpret fun_left_comm_idem times by (fact fun_left_comm_idem) + interpret comp_fun_idem times by (fact comp_fun_idem) from assms obtain y ys where xs: "xs = y # ys" by (cases xs) auto show ?thesis @@ -239,8 +239,8 @@ lemma (in complete_lattice) Inf_set_fold: "Inf (set xs) = fold inf xs top" proof - - interpret fun_left_comm_idem "inf :: 'a \ 'a \ 'a" - by (fact fun_left_comm_idem_inf) + interpret comp_fun_idem "inf :: 'a \ 'a \ 'a" + by (fact comp_fun_idem_inf) show ?thesis by (simp add: Inf_fold_inf fold_set inf_commute) qed @@ -251,8 +251,8 @@ lemma (in complete_lattice) Sup_set_fold: "Sup (set xs) = fold sup xs bot" proof - - interpret fun_left_comm_idem "sup :: 'a \ 'a \ 'a" - by (fact fun_left_comm_idem_sup) + interpret comp_fun_idem "sup :: 'a \ 'a \ 'a" + by (fact comp_fun_idem_sup) show ?thesis by (simp add: Sup_fold_sup fold_set sup_commute) qed diff -r 36abaf4cce1f -r 585c8333b0da src/HOL/Library/More_Set.thy --- a/src/HOL/Library/More_Set.thy Fri May 20 09:31:36 2011 +0200 +++ b/src/HOL/Library/More_Set.thy Fri May 20 11:44:34 2011 +0200 @@ -15,11 +15,11 @@ definition remove :: "'a \ 'a set \ 'a set" where "remove x A = A - {x}" -lemma fun_left_comm_idem_remove: - "fun_left_comm_idem remove" +lemma comp_fun_idem_remove: + "comp_fun_idem remove" proof - have rem: "remove = (\x A. A - {x})" by (simp add: fun_eq_iff remove_def) - show ?thesis by (simp only: fun_left_comm_idem_remove rem) + show ?thesis by (simp only: comp_fun_idem_remove rem) qed lemma minus_fold_remove: @@ -66,8 +66,8 @@ lemma union_set: "set xs \ A = fold Set.insert xs A" proof - - interpret fun_left_comm_idem Set.insert - by (fact fun_left_comm_idem_insert) + interpret comp_fun_idem Set.insert + by (fact comp_fun_idem_insert) show ?thesis by (simp add: union_fold_insert fold_set) qed @@ -82,8 +82,8 @@ lemma minus_set: "A - set xs = fold remove xs A" proof - - interpret fun_left_comm_idem remove - by (fact fun_left_comm_idem_remove) + interpret comp_fun_idem remove + by (fact comp_fun_idem_remove) show ?thesis by (simp add: minus_fold_remove [of _ A] fold_set) qed diff -r 36abaf4cce1f -r 585c8333b0da src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Fri May 20 09:31:36 2011 +0200 +++ b/src/HOL/Library/Multiset.thy Fri May 20 11:44:34 2011 +0200 @@ -1457,7 +1457,7 @@ lemma fold_mset_empty[simp]: "fold_mset f z {#} = z" unfolding fold_mset_def by blast -context fun_left_comm +context comp_fun_commute begin lemma fold_msetG_determ: @@ -1563,10 +1563,10 @@ qed lemma fold_mset_fusion: - assumes "fun_left_comm g" + assumes "comp_fun_commute g" shows "(\x y. h (g x y) = f x (h y)) \ h (fold_mset g w A) = fold_mset f (h w) A" (is "PROP ?P") proof - - interpret fun_left_comm g by (fact assms) + interpret comp_fun_commute g by (fact assms) show "PROP ?P" by (induct A) auto qed @@ -1598,7 +1598,7 @@ definition image_mset :: "('a \ 'b) \ 'a multiset \ 'b multiset" where "image_mset f = fold_mset (op + o single o f) {#}" -interpretation image_left_comm: fun_left_comm "op + o single o f" +interpretation image_fun_commute: comp_fun_commute "op + o single o f" proof qed (simp add: add_ac fun_eq_iff) lemma image_mset_empty [simp]: "image_mset f {#} = {#}" diff -r 36abaf4cce1f -r 585c8333b0da src/HOL/List.thy --- a/src/HOL/List.thy Fri May 20 09:31:36 2011 +0200 +++ b/src/HOL/List.thy Fri May 20 11:44:34 2011 +0200 @@ -2478,11 +2478,11 @@ text {* @{const Finite_Set.fold} and @{const foldl} *} -lemma (in fun_left_comm) fold_set_remdups: +lemma (in comp_fun_commute) fold_set_remdups: "fold f y (set xs) = foldl (\y x. f x y) y (remdups xs)" by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb) -lemma (in fun_left_comm_idem) fold_set: +lemma (in comp_fun_idem) fold_set: "fold f y (set xs) = foldl (\y x. f x y) y xs" by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm) @@ -2490,7 +2490,7 @@ assumes "xs \ []" shows "fold1 times (set xs) = foldl times (hd xs) (tl xs)" proof - - interpret fun_left_comm_idem times by (fact fun_left_comm_idem) + interpret comp_fun_idem times by (fact comp_fun_idem) from assms obtain y ys where xs: "xs = y # ys" by (cases xs) auto show ?thesis @@ -2543,16 +2543,16 @@ lemma (in complete_lattice) Inf_set_fold [code_unfold]: "Inf (set xs) = foldl inf top xs" proof - - interpret fun_left_comm_idem "inf :: 'a \ 'a \ 'a" - by (fact fun_left_comm_idem_inf) + interpret comp_fun_idem "inf :: 'a \ 'a \ 'a" + by (fact comp_fun_idem_inf) show ?thesis by (simp add: Inf_fold_inf fold_set inf_commute) qed lemma (in complete_lattice) Sup_set_fold [code_unfold]: "Sup (set xs) = foldl sup bot xs" proof - - interpret fun_left_comm_idem "sup :: 'a \ 'a \ 'a" - by (fact fun_left_comm_idem_sup) + interpret comp_fun_idem "sup :: 'a \ 'a \ 'a" + by (fact comp_fun_idem_sup) show ?thesis by (simp add: Sup_fold_sup fold_set sup_commute) qed @@ -3762,8 +3762,8 @@ "insort x (insort y xs) = insort y (insort x xs)" by (cases "x = y") (auto intro: insort_key_left_comm) -lemma fun_left_comm_insort: - "fun_left_comm insort" +lemma comp_fun_commute_insort: + "comp_fun_commute insort" proof qed (simp add: insort_left_comm fun_eq_iff) @@ -4249,7 +4249,7 @@ assumes "finite A" shows "sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))" proof - - interpret fun_left_comm insort by (fact fun_left_comm_insort) + interpret comp_fun_commute insort by (fact comp_fun_commute_insort) with assms show ?thesis by (simp add: sorted_list_of_set_def fold_insert_remove) qed @@ -4261,7 +4261,7 @@ lemma sorted_list_of_set_sort_remdups: "sorted_list_of_set (set xs) = sort (remdups xs)" proof - - interpret fun_left_comm insort by (fact fun_left_comm_insort) + interpret comp_fun_commute insort by (fact comp_fun_commute_insort) show ?thesis by (simp add: sort_foldl_insort sorted_list_of_set_def fold_set_remdups) qed diff -r 36abaf4cce1f -r 585c8333b0da src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Fri May 20 09:31:36 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Fri May 20 11:44:34 2011 +0200 @@ -1826,8 +1826,8 @@ lemma support_subset[intro]:"support opp f s \ s" unfolding support_def by auto lemma support_empty[simp]:"support opp f {} = {}" using support_subset[of opp f "{}"] by auto -lemma fun_left_comm_monoidal[intro]: assumes "monoidal opp" shows "fun_left_comm opp" - unfolding fun_left_comm_def using monoidal_ac[OF assms] by auto +lemma comp_fun_commute_monoidal[intro]: assumes "monoidal opp" shows "comp_fun_commute opp" + unfolding comp_fun_commute_def using monoidal_ac[OF assms] by auto lemma support_clauses: "\f g s. support opp f {} = {}" @@ -1850,12 +1850,12 @@ proof(cases "x\s") case True hence *:"insert x s = s" by auto show ?thesis unfolding iterate_def if_P[OF True] * by auto next case False note x=this - note * = fun_left_comm.comp_comp_fun_commute [OF fun_left_comm_monoidal[OF assms(1)]] + note * = comp_fun_commute.comp_comp_fun_commute [OF comp_fun_commute_monoidal[OF assms(1)]] show ?thesis proof(cases "f x = neutral opp") case True show ?thesis unfolding iterate_def if_not_P[OF x] support_clauses if_P[OF True] unfolding True monoidal_simps[OF assms(1)] by auto next case False show ?thesis unfolding iterate_def fold'_def if_not_P[OF x] support_clauses if_not_P[OF False] - apply(subst fun_left_comm.fold_insert[OF * finite_support, simplified comp_def]) + apply(subst comp_fun_commute.fold_insert[OF * finite_support, simplified comp_def]) using `finite s` unfolding support_def using False x by auto qed qed lemma iterate_some: