1.1 --- a/src/HOL/Groups_Big.thy Fri May 30 12:54:42 2014 +0200
1.2 +++ b/src/HOL/Groups_Big.thy Fri May 30 14:55:10 2014 +0200
1.3 @@ -131,27 +131,8 @@
1.4 assumes "A = B"
1.5 assumes g_h: "\<And>x. x \<in> B \<Longrightarrow> g x = h x"
1.6 shows "F g A = F h B"
1.7 -proof (cases "finite A")
1.8 - case True
1.9 - then have "\<And>C. C \<subseteq> A \<longrightarrow> (\<forall>x\<in>C. g x = h x) \<longrightarrow> F g C = F h C"
1.10 - proof induct
1.11 - case empty then show ?case by simp
1.12 - next
1.13 - case (insert x F) then show ?case apply -
1.14 - apply (simp add: subset_insert_iff, clarify)
1.15 - apply (subgoal_tac "finite C")
1.16 - prefer 2 apply (blast dest: finite_subset [rotated])
1.17 - apply (subgoal_tac "C = insert x (C - {x})")
1.18 - prefer 2 apply blast
1.19 - apply (erule ssubst)
1.20 - apply (simp add: Ball_def del: insert_Diff_single)
1.21 - done
1.22 - qed
1.23 - with `A = B` g_h show ?thesis by simp
1.24 -next
1.25 - case False
1.26 - with `A = B` show ?thesis by simp
1.27 -qed
1.28 + using g_h unfolding `A = B`
1.29 + by (induct B rule: infinite_finite_induct) auto
1.30
1.31 lemma strong_cong [cong]:
1.32 assumes "A = B" "\<And>x. x \<in> B =simp=> g x = h x"
1.33 @@ -206,42 +187,6 @@
1.34 shows "R (F h S) (F g S)"
1.35 using fS by (rule finite_subset_induct) (insert assms, auto)
1.36
1.37 -lemma eq_general:
1.38 - assumes h: "\<forall>y\<in>S'. \<exists>!x. x \<in> S \<and> h x = y"
1.39 - and f12: "\<forall>x\<in>S. h x \<in> S' \<and> f2 (h x) = f1 x"
1.40 - shows "F f1 S = F f2 S'"
1.41 -proof-
1.42 - from h f12 have hS: "h ` S = S'" by blast
1.43 - {fix x y assume H: "x \<in> S" "y \<in> S" "h x = h y"
1.44 - from f12 h H have "x = y" by auto }
1.45 - hence hinj: "inj_on h S" unfolding inj_on_def Ex1_def by blast
1.46 - from f12 have th: "\<And>x. x \<in> S \<Longrightarrow> (f2 \<circ> h) x = f1 x" by auto
1.47 - from hS have "F f2 S' = F f2 (h ` S)" by simp
1.48 - also have "\<dots> = F (f2 o h) S" using reindex [OF hinj, of f2] .
1.49 - also have "\<dots> = F f1 S " using th cong [of _ _ "f2 o h" f1]
1.50 - by blast
1.51 - finally show ?thesis ..
1.52 -qed
1.53 -
1.54 -lemma eq_general_reverses:
1.55 - assumes kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
1.56 - and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = j x"
1.57 - shows "F j S = F g T"
1.58 - (* metis solves it, but not yet available here *)
1.59 - apply (rule eq_general [of T S h g j])
1.60 - apply (rule ballI)
1.61 - apply (frule kh)
1.62 - apply (rule ex1I[])
1.63 - apply blast
1.64 - apply clarsimp
1.65 - apply (drule hk) apply simp
1.66 - apply (rule sym)
1.67 - apply (erule conjunct1[OF conjunct2[OF hk]])
1.68 - apply (rule ballI)
1.69 - apply (drule hk)
1.70 - apply blast
1.71 - done
1.72 -
1.73 lemma mono_neutral_cong_left:
1.74 assumes "finite T" and "S \<subseteq> T" and "\<forall>i \<in> T - S. h i = 1"
1.75 and "\<And>x. x \<in> S \<Longrightarrow> g x = h x" shows "F g S = F h T"
1.76 @@ -267,6 +212,74 @@
1.77 "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 1 \<rbrakk> \<Longrightarrow> F g T = F g S"
1.78 by (blast intro!: mono_neutral_left [symmetric])
1.79
1.80 +lemma reindex_bij_betw: "bij_betw h S T \<Longrightarrow> F (\<lambda>x. g (h x)) S = F g T"
1.81 + by (auto simp: bij_betw_def reindex)
1.82 +
1.83 +lemma reindex_bij_witness:
1.84 + assumes witness:
1.85 + "\<And>a. a \<in> S \<Longrightarrow> i (j a) = a"
1.86 + "\<And>a. a \<in> S \<Longrightarrow> j a \<in> T"
1.87 + "\<And>b. b \<in> T \<Longrightarrow> j (i b) = b"
1.88 + "\<And>b. b \<in> T \<Longrightarrow> i b \<in> S"
1.89 + assumes eq:
1.90 + "\<And>a. a \<in> S \<Longrightarrow> h (j a) = g a"
1.91 + shows "F g S = F h T"
1.92 +proof -
1.93 + have "bij_betw j S T"
1.94 + using bij_betw_byWitness[where A=S and f=j and f'=i and A'=T] witness by auto
1.95 + moreover have "F g S = F (\<lambda>x. h (j x)) S"
1.96 + by (intro cong) (auto simp: eq)
1.97 + ultimately show ?thesis
1.98 + by (simp add: reindex_bij_betw)
1.99 +qed
1.100 +
1.101 +lemma reindex_bij_betw_not_neutral:
1.102 + assumes fin: "finite S'" "finite T'"
1.103 + assumes bij: "bij_betw h (S - S') (T - T')"
1.104 + assumes nn:
1.105 + "\<And>a. a \<in> S' \<Longrightarrow> g (h a) = z"
1.106 + "\<And>b. b \<in> T' \<Longrightarrow> g b = z"
1.107 + shows "F (\<lambda>x. g (h x)) S = F g T"
1.108 +proof -
1.109 + have [simp]: "finite S \<longleftrightarrow> finite T"
1.110 + using bij_betw_finite[OF bij] fin by auto
1.111 +
1.112 + show ?thesis
1.113 + proof cases
1.114 + assume "finite S"
1.115 + with nn have "F (\<lambda>x. g (h x)) S = F (\<lambda>x. g (h x)) (S - S')"
1.116 + by (intro mono_neutral_cong_right) auto
1.117 + also have "\<dots> = F g (T - T')"
1.118 + using bij by (rule reindex_bij_betw)
1.119 + also have "\<dots> = F g T"
1.120 + using nn `finite S` by (intro mono_neutral_cong_left) auto
1.121 + finally show ?thesis .
1.122 + qed simp
1.123 +qed
1.124 +
1.125 +lemma reindex_bij_witness_not_neutral:
1.126 + assumes fin: "finite S'" "finite T'"
1.127 + assumes witness:
1.128 + "\<And>a. a \<in> S - S' \<Longrightarrow> i (j a) = a"
1.129 + "\<And>a. a \<in> S - S' \<Longrightarrow> j a \<in> T - T'"
1.130 + "\<And>b. b \<in> T - T' \<Longrightarrow> j (i b) = b"
1.131 + "\<And>b. b \<in> T - T' \<Longrightarrow> i b \<in> S - S'"
1.132 + assumes nn:
1.133 + "\<And>a. a \<in> S' \<Longrightarrow> g a = z"
1.134 + "\<And>b. b \<in> T' \<Longrightarrow> h b = z"
1.135 + assumes eq:
1.136 + "\<And>a. a \<in> S \<Longrightarrow> h (j a) = g a"
1.137 + shows "F g S = F h T"
1.138 +proof -
1.139 + have bij: "bij_betw j (S - (S' \<inter> S)) (T - (T' \<inter> T))"
1.140 + using witness by (intro bij_betw_byWitness[where f'=i]) auto
1.141 + have F_eq: "F g S = F (\<lambda>x. h (j x)) S"
1.142 + by (intro cong) (auto simp: eq)
1.143 + show ?thesis
1.144 + unfolding F_eq using fin nn eq
1.145 + by (intro reindex_bij_betw_not_neutral[OF _ _ bij]) auto
1.146 +qed
1.147 +
1.148 lemma delta:
1.149 assumes fS: "finite S"
1.150 shows "F (\<lambda>k. if k = a then b k else 1) S = (if a \<in> S then b a else 1)"
1.151 @@ -403,46 +416,17 @@
1.152 begin
1.153
1.154 lemma setsum_reindex_id:
1.155 - "inj_on f B ==> setsum f B = setsum id (f ` B)"
1.156 + "inj_on f B \<Longrightarrow> setsum f B = setsum id (f ` B)"
1.157 by (simp add: setsum.reindex)
1.158
1.159 lemma setsum_reindex_nonzero:
1.160 assumes fS: "finite S"
1.161 and nz: "\<And>x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<noteq> y \<Longrightarrow> f x = f y \<Longrightarrow> h (f x) = 0"
1.162 shows "setsum h (f ` S) = setsum (h \<circ> f) S"
1.163 -using nz proof (induct rule: finite_induct [OF fS])
1.164 - case 1 thus ?case by simp
1.165 -next
1.166 - case (2 x F)
1.167 - { assume fxF: "f x \<in> f ` F" hence "\<exists>y \<in> F . f y = f x" by auto
1.168 - then obtain y where y: "y \<in> F" "f x = f y" by auto
1.169 - from "2.hyps" y have xy: "x \<noteq> y" by auto
1.170 - from "2.prems" [of x y] "2.hyps" xy y have h0: "h (f x) = 0" by simp
1.171 - have "setsum h (f ` insert x F) = setsum h (f ` F)" using fxF by auto
1.172 - also have "\<dots> = setsum (h o f) (insert x F)"
1.173 - unfolding setsum.insert[OF `finite F` `x\<notin>F`]
1.174 - using h0
1.175 - apply (simp cong del: setsum.strong_cong)
1.176 - apply (rule "2.hyps"(3))
1.177 - apply (rule_tac y="y" in "2.prems")
1.178 - apply simp_all
1.179 - done
1.180 - finally have ?case . }
1.181 - moreover
1.182 - { assume fxF: "f x \<notin> f ` F"
1.183 - have "setsum h (f ` insert x F) = h (f x) + setsum h (f ` F)"
1.184 - using fxF "2.hyps" by simp
1.185 - also have "\<dots> = setsum (h o f) (insert x F)"
1.186 - unfolding setsum.insert[OF `finite F` `x\<notin>F`]
1.187 - apply (simp cong del: setsum.strong_cong)
1.188 - apply (rule cong [OF refl [of "op + (h (f x))"]])
1.189 - apply (rule "2.hyps"(3))
1.190 - apply (rule_tac y="y" in "2.prems")
1.191 - apply simp_all
1.192 - done
1.193 - finally have ?case . }
1.194 - ultimately show ?case by blast
1.195 -qed
1.196 +proof (subst setsum.reindex_bij_betw_not_neutral[symmetric])
1.197 + show "bij_betw f (S - {x\<in>S. h (f x) = 0}) (f`S - f`{x\<in>S. h (f x) = 0})"
1.198 + using nz by (auto intro!: inj_onI simp: bij_betw_def)
1.199 +qed (insert fS, auto)
1.200
1.201 lemma setsum_cong2:
1.202 "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> setsum f A = setsum g A"
1.203 @@ -494,19 +478,8 @@
1.204
1.205 lemma setsum_commute:
1.206 "(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)"
1.207 -proof (simp add: setsum_cartesian_product)
1.208 - have "(\<Sum>(x,y) \<in> A <*> B. f x y) =
1.209 - (\<Sum>(y,x) \<in> (%(i, j). (j, i)) ` (A \<times> B). f x y)"
1.210 - (is "?s = _")
1.211 - apply (simp add: setsum.reindex [where h = "%(i, j). (j, i)"] swap_inj_on)
1.212 - apply (simp add: split_def)
1.213 - done
1.214 - also have "... = (\<Sum>(y,x)\<in>B \<times> A. f x y)"
1.215 - (is "_ = ?t")
1.216 - apply (simp add: swap_product)
1.217 - done
1.218 - finally show "?s = ?t" .
1.219 -qed
1.220 + unfolding setsum_cartesian_product
1.221 + by (rule setsum.reindex_bij_witness[where i="\<lambda>(i, j). (j, i)" and j="\<lambda>(i, j). (j, i)"]) auto
1.222
1.223 lemma setsum_Plus:
1.224 fixes A :: "'a set" and B :: "'b set"
1.225 @@ -616,14 +589,6 @@
1.226 setsum f (S \<union> T) = setsum f S + setsum f T"
1.227 by (fact setsum.union_inter_neutral)
1.228
1.229 -lemma setsum_eq_general_reverses:
1.230 - assumes fS: "finite S" and fT: "finite T"
1.231 - and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
1.232 - and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = f x"
1.233 - shows "setsum f S = setsum g T"
1.234 - using kh hk by (fact setsum.eq_general_reverses)
1.235 -
1.236 -
1.237 subsubsection {* Properties in more restricted classes of structures *}
1.238
1.239 lemma setsum_Un: "finite A ==> finite B ==>
1.240 @@ -1124,17 +1089,9 @@
1.241 by (frule setprod.reindex, simp)
1.242
1.243 lemma strong_setprod_reindex_cong:
1.244 - assumes i: "inj_on f A"
1.245 - and B: "B = f ` A" and eq: "\<And>x. x \<in> A \<Longrightarrow> g x = (h \<circ> f) x"
1.246 - shows "setprod h B = setprod g A"
1.247 -proof-
1.248 - have "setprod h B = setprod (h o f) A"
1.249 - by (simp add: B setprod.reindex [OF i, of h])
1.250 - then show ?thesis apply simp
1.251 - apply (rule setprod.cong)
1.252 - apply simp
1.253 - by (simp add: eq)
1.254 -qed
1.255 + "inj_on f A \<Longrightarrow> B = f ` A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> g x = (h \<circ> f) x) \<Longrightarrow> setprod h B = setprod g A"
1.256 + by (subst setprod.reindex_bij_betw[symmetric, where h=f])
1.257 + (auto simp: bij_betw_def)
1.258
1.259 lemma setprod_Union_disjoint:
1.260 assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A Int B = {}"