--- 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 \<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]