--- 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 \<Longrightarrow> 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 \<Longrightarrow> ALL a:A. b \<le> a \<Longrightarrow> inf b c \<le> fold inf c A"
by (induct pred: finite) (auto intro: le_infI1)
--- 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 \<Rightarrow> 'b \<Rightarrow> 'b"
- assumes commute_comp: "f y \<circ> f x = f x \<circ> f y"
+ assumes comp_fun_commute: "f y \<circ> f x = f x \<circ> 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 \<circ> g)"
+lemma (in comp_fun_commute) comp_comp_fun_commute:
+ "comp_fun_commute (f \<circ> 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 \<circ> 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 \<circ> 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 (\<lambda>x A. A - {x})"
+lemma comp_fun_idem_remove:
+ "comp_fun_idem (\<lambda>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 \<union> 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 (\<lambda>x A. A - {x}) B A"
proof -
- interpret fun_left_comm_idem "\<lambda>x A. A - {x}" by (fact fun_left_comm_idem_remove)
+ interpret comp_fun_idem "\<lambda>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 (\<lambda>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 \<circ> f" by (fact comp_comp_fun_idem)
+ interpret comp_fun_idem inf by (fact comp_fun_idem_inf)
+ interpret comp_fun_idem "inf \<circ> f" by (fact comp_comp_fun_idem)
from `finite A` have "fold (inf \<circ> 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 (\<lambda>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 \<circ> f" by (fact comp_comp_fun_idem)
+ interpret comp_fun_idem sup by (fact comp_fun_idem_sup)
+ interpret comp_fun_idem "sup \<circ> f" by (fact comp_comp_fun_idem)
from `finite A` have "fold (sup \<circ> 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 \<notin> 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 \<notin> A"
shows "fold_graph times z (insert b A) (z * y)"
proof -
- interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
+ interpret comp_fun_commute "op *::'a \<Rightarrow> 'a \<Rightarrow> '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 \<notin> A" shows "fold1 times (insert a A) = fold times a A"
proof -
- interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
+ interpret comp_fun_commute "op *::'a \<Rightarrow> 'a \<Rightarrow> '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 \<noteq> {}" and A: "finite A" "x \<notin> A"
shows "fold1 times (insert x A) = x * fold1 times A"
proof -
- interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
+ interpret comp_fun_commute "op *::'a \<Rightarrow> 'a \<Rightarrow> '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 \<noteq> {}" and A: "finite A"
shows "fold1 times (insert x A) = x * fold1 times A"
proof -
- interpret fun_left_comm_idem "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"
- by (rule fun_left_comm_idem)
+ interpret comp_fun_idem "op *::'a \<Rightarrow> 'a \<Rightarrow> '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 \<notin> B" by (rule set_insert)
with assms have "finite B" by auto
@@ -1315,7 +1315,7 @@
locale folding =
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
fixes F :: "'a set \<Rightarrow> 'b \<Rightarrow> 'b"
- assumes commute_comp: "f y \<circ> f x = f x \<circ> f y"
+ assumes comp_fun_commute: "f y \<circ> f x = f x \<circ> f y"
assumes eq_fold: "finite A \<Longrightarrow> F A s = fold f s A"
begin
@@ -1327,8 +1327,8 @@
assumes "finite A" and "x \<notin> A"
shows "F (insert x A) = F A \<circ> 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 "\<And>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 \<circ> (f x \<circ> g) = f x \<circ> (f y \<circ> 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 \<circ> F A = F A \<circ> 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 \<circ> (F A \<circ> g) = F A \<circ> (f x \<circ> 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 \<circ> F A = F A \<circ> 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 \<circ> (F A \<circ> g) = F A \<circ> (F B \<circ> 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 \<union> B) \<circ> F (A \<inter> B) = F A \<circ> 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 \<in> A"
shows "F A \<circ> 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 \<subseteq> A"
@@ -1460,7 +1460,7 @@
assumes "finite A" and "x \<notin> 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 *" "\<lambda>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 \<circ> (\<lambda>b. fold op * b B) = (\<lambda>b. fold op * b B) \<circ> 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]
--- 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) \<longleftrightarrow> 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\<Rightarrow>nat\<Rightarrow>nat)"
+lemma comp_fun_idem_gcd_nat: "comp_fun_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
proof qed (auto simp add: gcd_ac_nat)
-lemma fun_left_comm_idem_gcd_int: "fun_left_comm_idem (gcd :: int\<Rightarrow>int\<Rightarrow>int)"
+lemma comp_fun_idem_gcd_int: "comp_fun_idem (gcd :: int\<Rightarrow>int\<Rightarrow>int)"
proof qed (auto simp add: gcd_ac_int)
-lemma fun_left_comm_idem_lcm_nat: "fun_left_comm_idem (lcm :: nat\<Rightarrow>nat\<Rightarrow>nat)"
+lemma comp_fun_idem_lcm_nat: "comp_fun_idem (lcm :: nat\<Rightarrow>nat\<Rightarrow>nat)"
proof qed (auto simp add: lcm_ac_nat)
-lemma fun_left_comm_idem_lcm_int: "fun_left_comm_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)"
+lemma comp_fun_idem_lcm_int: "comp_fun_idem (lcm :: int\<Rightarrow>int\<Rightarrow>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\<Rightarrow>nat\<Rightarrow>nat"
- by (rule fun_left_comm_idem_lcm_nat)
+ interpret comp_fun_idem "lcm::nat\<Rightarrow>nat\<Rightarrow>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\<Rightarrow>int\<Rightarrow>int"
- by (rule fun_left_comm_idem_lcm_int)
+ interpret comp_fun_idem "lcm::int\<Rightarrow>int\<Rightarrow>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\<Rightarrow>nat\<Rightarrow>nat"
- by (rule fun_left_comm_idem_gcd_nat)
+ interpret comp_fun_idem "gcd::nat\<Rightarrow>nat\<Rightarrow>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\<Rightarrow>int\<Rightarrow>int"
- by (rule fun_left_comm_idem_gcd_int)
+ interpret comp_fun_idem "gcd::int\<Rightarrow>int\<Rightarrow>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\<Rightarrow>nat\<Rightarrow>nat" by (rule fun_left_comm_idem_lcm_nat)
+ interpret comp_fun_idem "lcm::nat\<Rightarrow>nat\<Rightarrow>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\<Rightarrow>int\<Rightarrow>int" by (rule fun_left_comm_idem_lcm_int)
+ interpret comp_fun_idem "lcm::int\<Rightarrow>int\<Rightarrow>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\<Rightarrow>nat\<Rightarrow>nat" by (rule fun_left_comm_idem_gcd_nat)
+ interpret comp_fun_idem "gcd::nat\<Rightarrow>nat\<Rightarrow>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\<Rightarrow>int\<Rightarrow>int" by (rule fun_left_comm_idem_gcd_int)
+ interpret comp_fun_idem "gcd::int\<Rightarrow>int\<Rightarrow>int" by (rule comp_fun_idem_gcd_int)
show ?thesis by(simp add: Gcd_def fold_set gcd_commute_int)
qed
--- 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 \<noteq> []"
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 \<Rightarrow> 'a \<Rightarrow> 'a"
- by (fact fun_left_comm_idem_inf)
+ interpret comp_fun_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> '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 \<Rightarrow> 'a \<Rightarrow> 'a"
- by (fact fun_left_comm_idem_sup)
+ interpret comp_fun_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+ by (fact comp_fun_idem_sup)
show ?thesis by (simp add: Sup_fold_sup fold_set sup_commute)
qed
--- 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 \<Rightarrow> 'a set \<Rightarrow> '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 = (\<lambda>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 \<union> 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
--- 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 "(\<And>x y. h (g x y) = f x (h y)) \<Longrightarrow> 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 \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> '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 {#} = {#}"
--- 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 (\<lambda>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 (\<lambda>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 \<noteq> []"
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 \<Rightarrow> 'a \<Rightarrow> 'a"
- by (fact fun_left_comm_idem_inf)
+ interpret comp_fun_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> '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 \<Rightarrow> 'a \<Rightarrow> 'a"
- by (fact fun_left_comm_idem_sup)
+ interpret comp_fun_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> '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
--- 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 \<subseteq> 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:
"\<And>f g s. support opp f {} = {}"
@@ -1850,12 +1850,12 @@
proof(cases "x\<in>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: