104 apply (frule_tac a = Ca in fold_set.dom_subset [THEN subsetD, THEN SigmaD1]) |
104 apply (frule_tac a = Ca in fold_set.dom_subset [THEN subsetD, THEN SigmaD1]) |
105 apply (frule_tac a = Cb in fold_set.dom_subset [THEN subsetD, THEN SigmaD1]) |
105 apply (frule_tac a = Cb in fold_set.dom_subset [THEN subsetD, THEN SigmaD1]) |
106 apply (simp add: Fin_into_Finite [THEN Finite_imp_cardinal_cons]) |
106 apply (simp add: Fin_into_Finite [THEN Finite_imp_cardinal_cons]) |
107 apply (case_tac "x=xb", auto) |
107 apply (case_tac "x=xb", auto) |
108 apply (simp add: cons_lemma1, blast) |
108 apply (simp add: cons_lemma1, blast) |
109 txt{*case @{term "x\<noteq>xb"}*} |
109 txt\<open>case @{term "x\<noteq>xb"}\<close> |
110 apply (drule cons_lemma2, safe) |
110 apply (drule cons_lemma2, safe) |
111 apply (frule Diff_sing_imp, assumption+) |
111 apply (frule Diff_sing_imp, assumption+) |
112 txt{** LEVEL 17*} |
112 txt\<open>* LEVEL 17\<close> |
113 apply (subgoal_tac "|Ca| \<le> |Cb|") |
113 apply (subgoal_tac "|Ca| \<le> |Cb|") |
114 prefer 2 |
114 prefer 2 |
115 apply (rule succ_le_imp_le) |
115 apply (rule succ_le_imp_le) |
116 apply (simp add: Fin_into_Finite Finite_imp_succ_cardinal_Diff |
116 apply (simp add: Fin_into_Finite Finite_imp_succ_cardinal_Diff |
117 Fin_into_Finite [THEN Finite_imp_cardinal_cons]) |
117 Fin_into_Finite [THEN Finite_imp_cardinal_cons]) |
118 apply (rule_tac C1 = "Ca-{xb}" in Fin_imp_fold_set [THEN exE]) |
118 apply (rule_tac C1 = "Ca-{xb}" in Fin_imp_fold_set [THEN exE]) |
119 apply (blast intro: Diff_subset [THEN Fin_subset]) |
119 apply (blast intro: Diff_subset [THEN Fin_subset]) |
120 txt{** LEVEL 24 **} |
120 txt\<open>* LEVEL 24 *\<close> |
121 apply (frule Diff1_fold_set, blast, blast) |
121 apply (frule Diff1_fold_set, blast, blast) |
122 apply (blast dest!: ftype fold_set.dom_subset [THEN subsetD]) |
122 apply (blast dest!: ftype fold_set.dom_subset [THEN subsetD]) |
123 apply (subgoal_tac "ya = f(xb,xa) ") |
123 apply (subgoal_tac "ya = f(xb,xa) ") |
124 prefer 2 apply (blast del: equalityCE) |
124 prefer 2 apply (blast del: equalityCE) |
125 apply (subgoal_tac "<Cb-{x}, xa> \<in> fold_set(A,B,f,e)") |
125 apply (subgoal_tac "<Cb-{x}, xa> \<in> fold_set(A,B,f,e)") |
157 lemma fold_0 [simp]: "e \<in> B ==> fold[B](f,e,0) = e" |
157 lemma fold_0 [simp]: "e \<in> B ==> fold[B](f,e,0) = e" |
158 apply (unfold fold_def) |
158 apply (unfold fold_def) |
159 apply (blast elim!: empty_fold_setE intro: fold_set.intros) |
159 apply (blast elim!: empty_fold_setE intro: fold_set.intros) |
160 done |
160 done |
161 |
161 |
162 text{*This result is the right-to-left direction of the subsequent result*} |
162 text\<open>This result is the right-to-left direction of the subsequent result\<close> |
163 lemma (in fold_typing) fold_set_imp_cons: |
163 lemma (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 |] |
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)" |
165 ==> <cons(c, C), f(c,y)> \<in> fold_set(cons(c, C), B, f, e)" |
166 apply (frule FinD [THEN fold_set_mono, THEN subsetD]) |
166 apply (frule FinD [THEN fold_set_mono, THEN subsetD]) |
167 apply assumption |
167 apply assumption |
235 lemma Finite_cons_lemma: "Finite(C) ==> C\<in>Fin(cons(c, C))" |
235 lemma Finite_cons_lemma: "Finite(C) ==> C\<in>Fin(cons(c, C))" |
236 apply (drule Finite_into_Fin) |
236 apply (drule Finite_into_Fin) |
237 apply (blast intro: Fin_mono [THEN subsetD]) |
237 apply (blast intro: Fin_mono [THEN subsetD]) |
238 done |
238 done |
239 |
239 |
240 subsection{*The Operator @{term setsum}*} |
240 subsection\<open>The Operator @{term setsum}\<close> |
241 |
241 |
242 lemma setsum_0 [simp]: "setsum(g, 0) = #0" |
242 lemma setsum_0 [simp]: "setsum(g, 0) = #0" |
243 by (simp add: setsum_def) |
243 by (simp add: setsum_def) |
244 |
244 |
245 lemma setsum_cons [simp]: |
245 lemma setsum_cons [simp]: |