1(* Title: ZF/Induct/FoldSet.thy 2 Author: Sidi O Ehmety, Cambridge University Computer Laboratory 3 4A "fold" functional for finite sets. For n non-negative we have 5fold f e {x1,...,xn} = f x1 (... (f xn e)) where f is at 6least left-commutative. 7*) 8 9theory FoldSet imports ZF begin 10 11consts fold_set :: "[i, i, [i,i]=>i, i] => i" 12 13inductive 14 domains "fold_set(A, B, f,e)" \<subseteq> "Fin(A)*B" 15 intros 16 emptyI: "e\<in>B ==> <0, e>\<in>fold_set(A, B, f,e)" 17 consI: "[| x\<in>A; x \<notin>C; <C,y> \<in> fold_set(A, B,f,e); f(x,y):B |] 18 ==> <cons(x,C), f(x,y)>\<in>fold_set(A, B, f, e)" 19 type_intros Fin.intros 20 21definition 22 fold :: "[i, [i,i]=>i, i, i] => i" (\<open>fold[_]'(_,_,_')\<close>) where 23 "fold[B](f,e, A) == THE x. <A, x>\<in>fold_set(A, B, f,e)" 24 25definition 26 setsum :: "[i=>i, i] => i" where 27 "setsum(g, C) == if Finite(C) then 28 fold[int](%x y. g(x) $+ y, #0, C) else #0" 29 30(** foldSet **) 31 32inductive_cases empty_fold_setE: "<0, x> \<in> fold_set(A, B, f,e)" 33inductive_cases cons_fold_setE: "<cons(x,C), y> \<in> fold_set(A, B, f,e)" 34 35(* add-hoc lemmas *) 36 37lemma cons_lemma1: "[| x\<notin>C; x\<notin>B |] ==> cons(x,B)=cons(x,C) \<longleftrightarrow> B = C" 38by (auto elim: equalityE) 39 40lemma cons_lemma2: "[| cons(x, B)=cons(y, C); x\<noteq>y; x\<notin>B; y\<notin>C |] 41 ==> B - {y} = C-{x} & x\<in>C & y\<in>B" 42apply (auto elim: equalityE) 43done 44 45(* fold_set monotonicity *) 46lemma fold_set_mono_lemma: 47 "<C, x> \<in> fold_set(A, B, f, e) 48 ==> \<forall>D. A<=D \<longrightarrow> <C, x> \<in> fold_set(D, B, f, e)" 49apply (erule fold_set.induct) 50apply (auto intro: fold_set.intros) 51done 52 53lemma fold_set_mono: " C<=A ==> fold_set(C, B, f, e) \<subseteq> fold_set(A, B, f, e)" 54apply clarify 55apply (frule fold_set.dom_subset [THEN subsetD], clarify) 56apply (auto dest: fold_set_mono_lemma) 57done 58 59lemma fold_set_lemma: 60 "<C, x>\<in>fold_set(A, B, f, e) ==> <C, x>\<in>fold_set(C, B, f, e) & C<=A" 61apply (erule fold_set.induct) 62apply (auto intro!: fold_set.intros intro: fold_set_mono [THEN subsetD]) 63done 64 65(* Proving that fold_set is deterministic *) 66lemma Diff1_fold_set: 67 "[| <C-{x},y> \<in> fold_set(A, B, f,e); x\<in>C; x\<in>A; f(x, y):B |] 68 ==> <C, f(x, y)> \<in> fold_set(A, B, f, e)" 69apply (frule fold_set.dom_subset [THEN subsetD]) 70apply (erule cons_Diff [THEN subst], rule fold_set.intros, auto) 71done 72 73 74locale fold_typing = 75 fixes A and B and e and f 76 assumes ftype [intro,simp]: "[|x \<in> A; y \<in> B|] ==> f(x,y) \<in> B" 77 and etype [intro,simp]: "e \<in> B" 78 and fcomm: "[|x \<in> A; y \<in> A; z \<in> B|] ==> f(x, f(y, z))=f(y, f(x, z))" 79 80 81lemma (in fold_typing) Fin_imp_fold_set: 82 "C\<in>Fin(A) ==> (\<exists>x. <C, x> \<in> fold_set(A, B, f,e))" 83apply (erule Fin_induct) 84apply (auto dest: fold_set.dom_subset [THEN subsetD] 85 intro: fold_set.intros etype ftype) 86done 87 88lemma Diff_sing_imp: 89 "[|C - {b} = D - {a}; a \<noteq> b; b \<in> C|] ==> C = cons(b,D) - {a}" 90by (blast elim: equalityE) 91 92lemma (in fold_typing) fold_set_determ_lemma [rule_format]: 93"n\<in>nat 94 ==> \<forall>C. |C|<n \<longrightarrow> 95 (\<forall>x. <C, x> \<in> fold_set(A, B, f,e)\<longrightarrow> 96 (\<forall>y. <C, y> \<in> fold_set(A, B, f,e) \<longrightarrow> y=x))" 97apply (erule nat_induct) 98 apply (auto simp add: le_iff) 99apply (erule fold_set.cases) 100 apply (force elim!: empty_fold_setE) 101apply (erule fold_set.cases) 102 apply (force elim!: empty_fold_setE, clarify) 103(*force simplification of "|C| < |cons(...)|"*) 104apply (frule_tac a = Ca in fold_set.dom_subset [THEN subsetD, THEN SigmaD1]) 105apply (frule_tac a = Cb in fold_set.dom_subset [THEN subsetD, THEN SigmaD1]) 106apply (simp add: Fin_into_Finite [THEN Finite_imp_cardinal_cons]) 107apply (case_tac "x=xb", auto) 108apply (simp add: cons_lemma1, blast) 109txt\<open>case \<^term>\<open>x\<noteq>xb\<close>\<close> 110apply (drule cons_lemma2, safe) 111apply (frule Diff_sing_imp, assumption+) 112txt\<open>* LEVEL 17\<close> 113apply (subgoal_tac "|Ca| \<le> |Cb|") 114 prefer 2 115 apply (rule succ_le_imp_le) 116 apply (simp add: Fin_into_Finite Finite_imp_succ_cardinal_Diff 117 Fin_into_Finite [THEN Finite_imp_cardinal_cons]) 118apply (rule_tac C1 = "Ca-{xb}" in Fin_imp_fold_set [THEN exE]) 119 apply (blast intro: Diff_subset [THEN Fin_subset]) 120txt\<open>* LEVEL 24 *\<close> 121apply (frule Diff1_fold_set, blast, blast) 122apply (blast dest!: ftype fold_set.dom_subset [THEN subsetD]) 123apply (subgoal_tac "ya = f(xb,xa) ") 124 prefer 2 apply (blast del: equalityCE) 125apply (subgoal_tac "<Cb-{x}, xa> \<in> fold_set(A,B,f,e)") 126 prefer 2 apply simp 127apply (subgoal_tac "yb = f (x, xa) ") 128 apply (drule_tac [2] C = Cb in Diff1_fold_set, simp_all) 129 apply (blast intro: fcomm dest!: fold_set.dom_subset [THEN subsetD]) 130 apply (blast intro: ftype dest!: fold_set.dom_subset [THEN subsetD], blast) 131done 132 133lemma (in fold_typing) fold_set_determ: 134 "[| <C, x>\<in>fold_set(A, B, f, e); 135 <C, y>\<in>fold_set(A, B, f, e)|] ==> y=x" 136apply (frule fold_set.dom_subset [THEN subsetD], clarify) 137apply (drule Fin_into_Finite) 138apply (unfold Finite_def, clarify) 139apply (rule_tac n = "succ (n)" in fold_set_determ_lemma) 140apply (auto intro: eqpoll_imp_lepoll [THEN lepoll_cardinal_le]) 141done 142 143(** The fold function **) 144 145lemma (in fold_typing) fold_equality: 146 "<C,y> \<in> fold_set(A,B,f,e) ==> fold[B](f,e,C) = y" 147apply (unfold fold_def) 148apply (frule fold_set.dom_subset [THEN subsetD], clarify) 149apply (rule the_equality) 150 apply (rule_tac [2] A=C in fold_typing.fold_set_determ) 151apply (force dest: fold_set_lemma) 152apply (auto dest: fold_set_lemma) 153apply (simp add: fold_typing_def, auto) 154apply (auto dest: fold_set_lemma intro: ftype etype fcomm) 155done 156 157lemma fold_0 [simp]: "e \<in> B ==> fold[B](f,e,0) = e" 158apply (unfold fold_def) 159apply (blast elim!: empty_fold_setE intro: fold_set.intros) 160done 161 162text\<open>This result is the right-to-left direction of the subsequent result\<close> 163lemma (in fold_typing) fold_set_imp_cons: 164 "[| <C, y> \<in> fold_set(C, B, f, e); C \<in> Fin(A); c \<in> A; c\<notin>C |] 165 ==> <cons(c, C), f(c,y)> \<in> fold_set(cons(c, C), B, f, e)" 166apply (frule FinD [THEN fold_set_mono, THEN subsetD]) 167 apply assumption 168apply (frule fold_set.dom_subset [of A, THEN subsetD]) 169apply (blast intro!: fold_set.consI intro: fold_set_mono [THEN subsetD]) 170done 171 172lemma (in fold_typing) fold_cons_lemma [rule_format]: 173"[| C \<in> Fin(A); c \<in> A; c\<notin>C |] 174 ==> <cons(c, C), v> \<in> fold_set(cons(c, C), B, f, e) \<longleftrightarrow> 175 (\<exists>y. <C, y> \<in> fold_set(C, B, f, e) & v = f(c, y))" 176apply auto 177 prefer 2 apply (blast intro: fold_set_imp_cons) 178 apply (frule_tac Fin.consI [of c, THEN FinD, THEN fold_set_mono, THEN subsetD], assumption+) 179apply (frule_tac fold_set.dom_subset [of A, THEN subsetD]) 180apply (drule FinD) 181apply (rule_tac A1 = "cons(c,C)" and f1=f and B1=B and C1=C and e1=e in fold_typing.Fin_imp_fold_set [THEN exE]) 182apply (blast intro: fold_typing.intro ftype etype fcomm) 183apply (blast intro: Fin_subset [of _ "cons(c,C)"] Finite_into_Fin 184 dest: Fin_into_Finite) 185apply (rule_tac x = x in exI) 186apply (auto intro: fold_set.intros) 187apply (drule_tac fold_set_lemma [of C], blast) 188apply (blast intro!: fold_set.consI 189 intro: fold_set_determ fold_set_mono [THEN subsetD] 190 dest: fold_set.dom_subset [THEN subsetD]) 191done 192 193lemma (in fold_typing) fold_cons: 194 "[| C\<in>Fin(A); c\<in>A; c\<notin>C|] 195 ==> fold[B](f, e, cons(c, C)) = f(c, fold[B](f, e, C))" 196apply (unfold fold_def) 197apply (simp add: fold_cons_lemma) 198apply (rule the_equality, auto) 199 apply (subgoal_tac [2] "\<langle>C, y\<rangle> \<in> fold_set(A, B, f, e)") 200 apply (drule Fin_imp_fold_set) 201apply (auto dest: fold_set_lemma simp add: fold_def [symmetric] fold_equality) 202apply (blast intro: fold_set_mono [THEN subsetD] dest!: FinD) 203done 204 205lemma (in fold_typing) fold_type [simp,TC]: 206 "C\<in>Fin(A) ==> fold[B](f,e,C):B" 207apply (erule Fin_induct) 208apply (simp_all add: fold_cons ftype etype) 209done 210 211lemma (in fold_typing) fold_commute [rule_format]: 212 "[| C\<in>Fin(A); c\<in>A |] 213 ==> (\<forall>y\<in>B. f(c, fold[B](f, y, C)) = fold[B](f, f(c, y), C))" 214apply (erule Fin_induct) 215apply (simp_all add: fold_typing.fold_cons [of A B _ f] 216 fold_typing.fold_type [of A B _ f] 217 fold_typing_def fcomm) 218done 219 220lemma (in fold_typing) fold_nest_Un_Int: 221 "[| C\<in>Fin(A); D\<in>Fin(A) |] 222 ==> fold[B](f, fold[B](f, e, D), C) = 223 fold[B](f, fold[B](f, e, (C \<inter> D)), C \<union> D)" 224apply (erule Fin_induct, auto) 225apply (simp add: Un_cons Int_cons_left fold_type fold_commute 226 fold_typing.fold_cons [of A _ _ f] 227 fold_typing_def fcomm cons_absorb) 228done 229 230lemma (in fold_typing) fold_nest_Un_disjoint: 231 "[| C\<in>Fin(A); D\<in>Fin(A); C \<inter> D = 0 |] 232 ==> fold[B](f,e,C \<union> D) = fold[B](f, fold[B](f,e,D), C)" 233by (simp add: fold_nest_Un_Int) 234 235lemma Finite_cons_lemma: "Finite(C) ==> C\<in>Fin(cons(c, C))" 236apply (drule Finite_into_Fin) 237apply (blast intro: Fin_mono [THEN subsetD]) 238done 239 240subsection\<open>The Operator \<^term>\<open>setsum\<close>\<close> 241 242lemma setsum_0 [simp]: "setsum(g, 0) = #0" 243by (simp add: setsum_def) 244 245lemma setsum_cons [simp]: 246 "Finite(C) ==> 247 setsum(g, cons(c,C)) = 248 (if c \<in> C then setsum(g,C) else g(c) $+ setsum(g,C))" 249apply (auto simp add: setsum_def Finite_cons cons_absorb) 250apply (rule_tac A = "cons (c, C)" in fold_typing.fold_cons) 251apply (auto intro: fold_typing.intro Finite_cons_lemma) 252done 253 254lemma setsum_K0: "setsum((%i. #0), C) = #0" 255apply (case_tac "Finite (C) ") 256 prefer 2 apply (simp add: setsum_def) 257apply (erule Finite_induct, auto) 258done 259 260(*The reversed orientation looks more natural, but LOOPS as a simprule!*) 261lemma setsum_Un_Int: 262 "[| Finite(C); Finite(D) |] 263 ==> setsum(g, C \<union> D) $+ setsum(g, C \<inter> D) 264 = setsum(g, C) $+ setsum(g, D)" 265apply (erule Finite_induct) 266apply (simp_all add: Int_cons_right cons_absorb Un_cons Int_commute Finite_Un 267 Int_lower1 [THEN subset_Finite]) 268done 269 270lemma setsum_type [simp,TC]: "setsum(g, C):int" 271apply (case_tac "Finite (C) ") 272 prefer 2 apply (simp add: setsum_def) 273apply (erule Finite_induct, auto) 274done 275 276lemma setsum_Un_disjoint: 277 "[| Finite(C); Finite(D); C \<inter> D = 0 |] 278 ==> setsum(g, C \<union> D) = setsum(g, C) $+ setsum(g,D)" 279apply (subst setsum_Un_Int [symmetric]) 280apply (subgoal_tac [3] "Finite (C \<union> D) ") 281apply (auto intro: Finite_Un) 282done 283 284lemma Finite_RepFun [rule_format (no_asm)]: 285 "Finite(I) ==> (\<forall>i\<in>I. Finite(C(i))) \<longrightarrow> Finite(RepFun(I, C))" 286apply (erule Finite_induct, auto) 287done 288 289lemma setsum_UN_disjoint [rule_format (no_asm)]: 290 "Finite(I) 291 ==> (\<forall>i\<in>I. Finite(C(i))) \<longrightarrow> 292 (\<forall>i\<in>I. \<forall>j\<in>I. i\<noteq>j \<longrightarrow> C(i) \<inter> C(j) = 0) \<longrightarrow> 293 setsum(f, \<Union>i\<in>I. C(i)) = setsum (%i. setsum(f, C(i)), I)" 294apply (erule Finite_induct, auto) 295apply (subgoal_tac "\<forall>i\<in>B. x \<noteq> i") 296 prefer 2 apply blast 297apply (subgoal_tac "C (x) \<inter> (\<Union>i\<in>B. C (i)) = 0") 298 prefer 2 apply blast 299apply (subgoal_tac "Finite (\<Union>i\<in>B. C (i)) & Finite (C (x)) & Finite (B) ") 300apply (simp (no_asm_simp) add: setsum_Un_disjoint) 301apply (auto intro: Finite_Union Finite_RepFun) 302done 303 304 305lemma setsum_addf: "setsum(%x. f(x) $+ g(x),C) = setsum(f, C) $+ setsum(g, C)" 306apply (case_tac "Finite (C) ") 307 prefer 2 apply (simp add: setsum_def) 308apply (erule Finite_induct, auto) 309done 310 311 312lemma fold_set_cong: 313 "[| A=A'; B=B'; e=e'; (\<forall>x\<in>A'. \<forall>y\<in>B'. f(x,y) = f'(x,y)) |] 314 ==> fold_set(A,B,f,e) = fold_set(A',B',f',e')" 315apply (simp add: fold_set_def) 316apply (intro refl iff_refl lfp_cong Collect_cong disj_cong ex_cong, auto) 317done 318 319lemma fold_cong: 320"[| B=B'; A=A'; e=e'; 321 !!x y. [|x\<in>A'; y\<in>B'|] ==> f(x,y) = f'(x,y) |] ==> 322 fold[B](f,e,A) = fold[B'](f', e', A')" 323apply (simp add: fold_def) 324apply (subst fold_set_cong) 325apply (rule_tac [5] refl, simp_all) 326done 327 328lemma setsum_cong: 329 "[| A=B; !!x. x\<in>B ==> f(x) = g(x) |] ==> 330 setsum(f, A) = setsum(g, B)" 331by (simp add: setsum_def cong add: fold_cong) 332 333lemma setsum_Un: 334 "[| Finite(A); Finite(B) |] 335 ==> setsum(f, A \<union> B) = 336 setsum(f, A) $+ setsum(f, B) $- setsum(f, A \<inter> B)" 337apply (subst setsum_Un_Int [symmetric], auto) 338done 339 340 341lemma setsum_zneg_or_0 [rule_format (no_asm)]: 342 "Finite(A) ==> (\<forall>x\<in>A. g(x) $\<le> #0) \<longrightarrow> setsum(g, A) $\<le> #0" 343apply (erule Finite_induct) 344apply (auto intro: zneg_or_0_add_zneg_or_0_imp_zneg_or_0) 345done 346 347lemma setsum_succD_lemma [rule_format]: 348 "Finite(A) 349 ==> \<forall>n\<in>nat. setsum(f,A) = $# succ(n) \<longrightarrow> (\<exists>a\<in>A. #0 $< f(a))" 350apply (erule Finite_induct) 351apply (auto simp del: int_of_0 int_of_succ simp add: not_zless_iff_zle int_of_0 [symmetric]) 352apply (subgoal_tac "setsum (f, B) $\<le> #0") 353apply simp_all 354prefer 2 apply (blast intro: setsum_zneg_or_0) 355apply (subgoal_tac "$# 1 $\<le> f (x) $+ setsum (f, B) ") 356apply (drule zdiff_zle_iff [THEN iffD2]) 357apply (subgoal_tac "$# 1 $\<le> $# 1 $- setsum (f,B) ") 358apply (drule_tac x = "$# 1" in zle_trans) 359apply (rule_tac [2] j = "#1" in zless_zle_trans, auto) 360done 361 362lemma setsum_succD: 363 "[| setsum(f, A) = $# succ(n); n\<in>nat |]==> \<exists>a\<in>A. #0 $< f(a)" 364apply (case_tac "Finite (A) ") 365apply (blast intro: setsum_succD_lemma) 366apply (unfold setsum_def) 367apply (auto simp del: int_of_0 int_of_succ simp add: int_succ_int_1 [symmetric] int_of_0 [symmetric]) 368done 369 370lemma g_zpos_imp_setsum_zpos [rule_format]: 371 "Finite(A) ==> (\<forall>x\<in>A. #0 $\<le> g(x)) \<longrightarrow> #0 $\<le> setsum(g, A)" 372apply (erule Finite_induct) 373apply (simp (no_asm)) 374apply (auto intro: zpos_add_zpos_imp_zpos) 375done 376 377lemma g_zpos_imp_setsum_zpos2 [rule_format]: 378 "[| Finite(A); \<forall>x. #0 $\<le> g(x) |] ==> #0 $\<le> setsum(g, A)" 379apply (erule Finite_induct) 380apply (auto intro: zpos_add_zpos_imp_zpos) 381done 382 383lemma g_zspos_imp_setsum_zspos [rule_format]: 384 "Finite(A) 385 ==> (\<forall>x\<in>A. #0 $< g(x)) \<longrightarrow> A \<noteq> 0 \<longrightarrow> (#0 $< setsum(g, A))" 386apply (erule Finite_induct) 387apply (auto intro: zspos_add_zspos_imp_zspos) 388done 389 390lemma setsum_Diff [rule_format]: 391 "Finite(A) ==> \<forall>a. M(a) = #0 \<longrightarrow> setsum(M, A) = setsum(M, A-{a})" 392apply (erule Finite_induct) 393apply (simp_all add: Diff_cons_eq Finite_Diff) 394done 395 396end 397