diff -r 43b0f61f56d0 -r 1c0b99f950d9 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Fri May 20 08:16:56 2011 +0200 +++ b/src/HOL/Finite_Set.thy Fri May 20 11:44:16 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]