1.1 --- a/src/ZF/Induct/FoldSet.ML Mon Jan 28 23:35:20 2002 +0100
1.2 +++ b/src/ZF/Induct/FoldSet.ML Wed Jan 30 12:22:40 2002 +0100
1.3 @@ -16,9 +16,6 @@
1.4 bind_thm("cons_fold_setE",
1.5 fold_set.mk_cases "<cons(x,C), y> : fold_set(A, B, f,e)");
1.6
1.7 -bind_thm("fold_set_lhs", fold_set.dom_subset RS subsetD RS SigmaD1);
1.8 -bind_thm("fold_set_rhs", fold_set.dom_subset RS subsetD RS SigmaD2);
1.9 -
1.10 (* add-hoc lemmas *)
1.11
1.12 Goal "[| x~:C; x~:B |] ==> cons(x,B)=cons(x,C) <-> B = C";
1.13 @@ -30,53 +27,79 @@
1.14 by (auto_tac (claset() addEs [equalityE], simpset()));
1.15 qed "cons_lemma2";
1.16
1.17 +(* fold_set monotonicity *)
1.18 +Goal "<C, x> : fold_set(A, B, f, e) \
1.19 +\ ==> ALL D. A<=D --> <C, x> : fold_set(D, B, f, e)";
1.20 +by (etac fold_set.induct 1);
1.21 +by (auto_tac (claset() addIs fold_set.intrs, simpset()));
1.22 +qed "fold_set_mono_lemma";
1.23
1.24 -Open_locale "LC";
1.25 -val f_lcomm = thm "lcomm";
1.26 -val f_type = thm "ftype";
1.27 +Goal " C<=A ==> fold_set(C, B, f, e) <= fold_set(A, B, f, e)";
1.28 +by (Clarify_tac 1);
1.29 +by (forward_tac [impOfSubs fold_set.dom_subset] 1);
1.30 +by (Clarify_tac 1);
1.31 +by (auto_tac (claset() addDs [fold_set_mono_lemma], simpset()));
1.32 +qed "fold_set_mono";
1.33
1.34 -Goal "[| <C-{x},y> : fold_set(A, B, f,e); x:C; x:A |] \
1.35 -\ ==> <C, f(x,y)> : fold_set(A, B, f, e)";
1.36 -by (ftac fold_set_rhs 1);
1.37 +Goal "<C, x>:fold_set(A, B, f, e) ==> <C, x>:fold_set(C, B, f, e) & C<=A";
1.38 +by (etac fold_set.induct 1);
1.39 +by (auto_tac (claset() addSIs fold_set.intrs
1.40 + addIs [fold_set_mono RS subsetD], simpset()));
1.41 +qed "fold_set_lemma";
1.42 +
1.43 +(* Proving that fold_set is deterministic *)
1.44 +Goal "[| <C-{x},y> : fold_set(A, B, f,e); x:C; x:A; f(x, y):B |] \
1.45 +\ ==> <C, f(x, y)> : fold_set(A, B, f, e)";
1.46 +by (ftac (fold_set.dom_subset RS subsetD) 1);
1.47 by (etac (cons_Diff RS subst) 1 THEN resolve_tac fold_set.intrs 1);
1.48 -by (auto_tac (claset() addIs [f_type], simpset()));
1.49 +by Auto_tac;
1.50 qed "Diff1_fold_set";
1.51
1.52 -Goal "[| C:Fin(A); e:B |] ==> EX x. <C, x> : fold_set(A, B, f,e)";
1.53 +Goal "[| C:Fin(A); e:B; ALL x:A. ALL y:B. f(x, y):B |] ==>\
1.54 +\ (EX x. <C, x> : fold_set(A, B, f,e))";
1.55 by (etac Fin_induct 1);
1.56 -by (ALLGOALS(Clarify_tac));
1.57 -by (ftac fold_set_rhs 2);
1.58 -by (cut_inst_tac [("x", "x"), ("y", "xa")] f_type 2);
1.59 -by (REPEAT(blast_tac (claset() addIs fold_set.intrs) 1));
1.60 +by Auto_tac;
1.61 +by (ftac (fold_set.dom_subset RS subsetD) 2);
1.62 +by (auto_tac (claset() addDs [fold_set.dom_subset RS subsetD]
1.63 + addIs fold_set.intrs, simpset()));
1.64 qed_spec_mp "Fin_imp_fold_set";
1.65
1.66 -
1.67 -Goal "n:nat \
1.68 -\ ==> ALL C x. |C|<n --> e:B --> <C, x> : fold_set(A, B, f,e)-->\
1.69 -\ (ALL y. <C, y> : fold_set(A, B, f,e) --> y=x)";
1.70 +Goal
1.71 +"[| n:nat; e:B; \
1.72 +\ ALL x:A. ALL y:B. f(x, y):B; \
1.73 +\ ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))=f(y, f(x, z)) |] \
1.74 +\ ==> ALL C. |C|<n --> \
1.75 +\ (ALL x. <C, x> : fold_set(A, B, f,e)-->\
1.76 +\ (ALL y. <C, y> : fold_set(A, B, f,e) --> y=x))";
1.77 by (etac nat_induct 1);
1.78 by (auto_tac (claset(), simpset() addsimps [le_iff]));
1.79 +by (Blast_tac 1);
1.80 by (etac fold_set.elim 1);
1.81 -by (blast_tac (claset() addEs [empty_fold_setE]) 1);
1.82 +by (force_tac (claset() addSEs [empty_fold_setE], simpset()) 1);
1.83 by (etac fold_set.elim 1);
1.84 -by (blast_tac (claset() addEs [empty_fold_setE]) 1);
1.85 +by (force_tac (claset() addSEs [empty_fold_setE], simpset()) 1);
1.86 by (Clarify_tac 1);
1.87 (*force simplification of "|C| < |cons(...)|"*)
1.88 -by (rotate_tac 2 1);
1.89 +by (rotate_tac 4 1);
1.90 by (etac rev_mp 1);
1.91 -by (forw_inst_tac [("a", "Ca")] fold_set_lhs 1);
1.92 -by (forw_inst_tac [("a", "Cb")] fold_set_lhs 1);
1.93 -by (asm_simp_tac (simpset() addsimps [Fin_into_Finite RS Finite_imp_cardinal_cons]) 1);
1.94 +by (forw_inst_tac [("a", "Ca")]
1.95 + (fold_set.dom_subset RS subsetD RS SigmaD1) 1);
1.96 +by (forw_inst_tac [("a", "Cb")]
1.97 + (fold_set.dom_subset RS subsetD RS SigmaD1) 1);
1.98 +by (asm_simp_tac (simpset() addsimps
1.99 + [Fin_into_Finite RS Finite_imp_cardinal_cons]) 1);
1.100 by (rtac impI 1);
1.101 (** LEVEL 10 **)
1.102 by (case_tac "x=xb" 1 THEN Auto_tac);
1.103 -by (asm_full_simp_tac (simpset() addsimps [cons_lemma1]) 1);
1.104 -by (Blast_tac 1);
1.105 +by (asm_full_simp_tac (simpset() addsimps [cons_lemma1]) 1);
1.106 +by (REPEAT(thin_tac "ALL x:A. ?u(x)" 1) THEN Blast_tac 1);
1.107 (*case x ~= xb*)
1.108 by (dtac cons_lemma2 1 THEN ALLGOALS Clarify_tac);
1.109 by (subgoal_tac "Ca = cons(xb, Cb) - {x}" 1);
1.110 -by (blast_tac (claset() addEs [equalityE]) 2);
1.111 -(** LEVEL 20 **)
1.112 +by (REPEAT(thin_tac "ALL C. ?P(C)" 2));
1.113 +by (REPEAT(thin_tac "ALL x:?u. ?P(x)" 2));
1.114 +by (blast_tac (claset() addEs [equalityE]) 2);
1.115 +(** LEVEL 22 **)
1.116 by (subgoal_tac "|Ca| le |Cb|" 1);
1.117 by (rtac succ_le_imp_le 2);
1.118 by (hyp_subst_tac 2);
1.119 @@ -84,39 +107,60 @@
1.120 by (asm_simp_tac (simpset() addsimps [Finite_imp_succ_cardinal_Diff,
1.121 Fin_into_Finite RS Finite_imp_cardinal_cons]) 2);
1.122 by (asm_simp_tac (simpset() addsimps [Fin.consI RS Fin_into_Finite]) 2);
1.123 -by (res_inst_tac [("C1", "Ca-{xb}"), ("e1","e"), ("A1", "A")]
1.124 +by (res_inst_tac [("C1", "Ca-{xb}"), ("e1","e"), ("A1", "A"), ("f1", "f")]
1.125 (Fin_imp_fold_set RS exE) 1);
1.126 by (blast_tac (claset() addIs [Diff_subset RS Fin_subset]) 1);
1.127 by (Blast_tac 1);
1.128 -(** LEVEL 28 **)
1.129 -by (ftac Diff1_fold_set 1 THEN assume_tac 1 THEN assume_tac 1);
1.130 +by (blast_tac (claset() addSDs [FinD]) 1);
1.131 +(** LEVEL 32 **)
1.132 +by (ftac Diff1_fold_set 1);
1.133 +by (Blast_tac 1);
1.134 +by (Blast_tac 1);
1.135 +by (blast_tac (claset() addSDs [fold_set.dom_subset RS subsetD]) 1);
1.136 by (subgoal_tac "ya = f(xb, xa)" 1);
1.137 +by (dres_inst_tac [("x", "Ca")] spec 2);
1.138 by (blast_tac (claset() delrules [equalityCE]) 2);
1.139 by (subgoal_tac "<Cb-{x}, xa>: fold_set(A, B, f, e)" 1);
1.140 - by (Asm_full_simp_tac 2);
1.141 +by (Asm_full_simp_tac 2);
1.142 by (subgoal_tac "yb = f(x, xa)" 1);
1.143 - by (blast_tac (claset() delrules [equalityCE]
1.144 - addDs [Diff1_fold_set]) 2);
1.145 -by (asm_simp_tac (simpset() addsimps [f_lcomm]) 1);
1.146 -qed_spec_mp "lemma";
1.147 +by (dres_inst_tac [("C", "Cb")] Diff1_fold_set 2);
1.148 +by (ALLGOALS(Asm_simp_tac));
1.149 +by (force_tac (claset() addSDs [fold_set.dom_subset RS subsetD], simpset()) 2);
1.150 +by (force_tac (claset() addSDs [fold_set.dom_subset RS subsetD], simpset()) 1);
1.151 +by (dres_inst_tac [("x", "Cb")] spec 1);
1.152 +by Auto_tac;
1.153 +qed_spec_mp "fold_set_determ_lemma";
1.154
1.155 -
1.156 -Goal "[| <C, x> : fold_set(A, B, f, e); \
1.157 -\ <C, y> : fold_set(A, B, f, e); e:B |] ==> y=x";
1.158 -by (forward_tac [fold_set_lhs RS Fin_into_Finite] 1);
1.159 +Goal
1.160 +"[| <C, x>:fold_set(A, B, f, e); \
1.161 +\ <C, y>:fold_set(A, B, f, e); e:B; \
1.162 +\ ALL x:A. ALL y:B. f(x, y):B; \
1.163 +\ ALL x:A. ALL y:A. ALL z:B. f(x,f(y, z))=f(y, f(x, z)) |]\
1.164 +\ ==> y=x";
1.165 +by (forward_tac [fold_set.dom_subset RS subsetD] 1);
1.166 +by (Clarify_tac 1);
1.167 +by (dtac Fin_into_Finite 1);
1.168 by (rewtac Finite_def);
1.169 by (Clarify_tac 1);
1.170 -by (res_inst_tac [("n", "succ(n)")] lemma 1);
1.171 -by (auto_tac (claset() addIs
1.172 - [eqpoll_imp_lepoll RS lepoll_cardinal_le],
1.173 - simpset()));
1.174 +by (res_inst_tac [("n", "succ(n)"), ("e", "e"), ("A", "A"),
1.175 + ("f", "f"), ("B", "B")] fold_set_determ_lemma 1);
1.176 +by (auto_tac (claset() addIs [eqpoll_imp_lepoll RS
1.177 + lepoll_cardinal_le], simpset()));
1.178 qed "fold_set_determ";
1.179
1.180 +(** The fold function **)
1.181 +
1.182 Goalw [fold_def]
1.183 - "[| <C,y> : fold_set(C, B, f, e); e:B |] ==> fold[B](f,e,C) = y";
1.184 +"[| <C, y>:fold_set(A, B, f, e); e:B; \
1.185 +\ ALL x:A. ALL y:B. f(x, y):B; \
1.186 +\ ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))=f(y, f(x, z)) |] \
1.187 +\ ==> fold[B](f, e, C) = y";
1.188 +by (forward_tac [fold_set.dom_subset RS subsetD] 1);
1.189 +by (Clarify_tac 1);
1.190 by (rtac the_equality 1);
1.191 -by (rtac fold_set_determ 2);
1.192 -by Auto_tac;
1.193 +by (res_inst_tac [("f", "f"), ("e", "e"), ("B", "B")] fold_set_determ 2);
1.194 +by (auto_tac (claset() addDs [fold_set_lemma], simpset()));
1.195 +by (blast_tac (claset() addSDs [FinD]) 1);
1.196 qed "fold_equality";
1.197
1.198 Goalw [fold_def] "e:B ==> fold[B](f,e,0) = e";
1.199 @@ -125,75 +169,78 @@
1.200 qed "fold_0";
1.201 Addsimps [fold_0];
1.202
1.203 -Goal "[| x ~: C; x:A; e:B |] \
1.204 -\ ==> <cons(x, C), v> : fold_set(A, B, f, e) <-> \
1.205 -\ (EX y. <C, y> : fold_set(A, B, f, e) & v = f(x, y))";
1.206 +Goal
1.207 +"[| C:Fin(A); c:A; c~:C; e:B; ALL x:A. ALL y:B. f(x, y):B; \
1.208 +\ ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))=f(y, f(x,z)) |] \
1.209 +\ ==> <cons(c, C), v> : fold_set(cons(c, C), B, f, e) <-> \
1.210 +\ (EX y. <C, y> : fold_set(C, B, f, e) & v = f(c, y))";
1.211 by Auto_tac;
1.212 -by (res_inst_tac [("A1", "A"), ("C1", "C")] (Fin_imp_fold_set RS exE) 1);
1.213 -by (res_inst_tac [("x", "xa")] exI 3);
1.214 -by (res_inst_tac [("b", "cons(x, C)")] Fin_subset 1);
1.215 -by (auto_tac (claset() addDs [fold_set_lhs]
1.216 - addIs [f_type]@fold_set.intrs, simpset()));
1.217 -by (blast_tac (claset() addIs [fold_set_determ, f_type]@fold_set.intrs) 1);
1.218 -val lemma = result();
1.219 -
1.220 -Goal "<D, x> : fold_set(C, B, f, e) \
1.221 -\ ==> ALL A. C<=A --> <D, x> : fold_set(A, B, f, e)";
1.222 -by (etac fold_set.induct 1);
1.223 +by (forward_tac [inst "a" "c" Fin.consI RS FinD RS fold_set_mono RS subsetD] 1);
1.224 +by (assume_tac 1);
1.225 +by (assume_tac 1);
1.226 +by (forward_tac [FinD RS fold_set_mono RS subsetD] 2);
1.227 +by (assume_tac 2);
1.228 +by (ALLGOALS(forward_tac [inst "A" "A" fold_set.dom_subset RS subsetD]));
1.229 +by (ALLGOALS(dresolve_tac [FinD]));
1.230 +by (res_inst_tac [("A1", "cons(c, C)"), ("f1", "f"),
1.231 + ("B1", "B"), ("C1", "C")] (Fin_imp_fold_set RS exE) 1);
1.232 +by (res_inst_tac [("b", "cons(c, C)")] Fin_subset 1);
1.233 +by (resolve_tac [Finite_into_Fin] 2);
1.234 +by (resolve_tac [Fin_into_Finite] 2);
1.235 +by (Blast_tac 2);
1.236 +by (res_inst_tac [("x", "x")] exI 4);
1.237 by (auto_tac (claset() addIs fold_set.intrs, simpset()));
1.238 -qed "lemma2";
1.239 -
1.240 -Goal " C<=A ==> fold_set(C, B, f, e) <= fold_set(A, B, f, e)";
1.241 -by (Clarify_tac 1);
1.242 -by (forward_tac [impOfSubs fold_set.dom_subset] 1);
1.243 -by (Clarify_tac 1);
1.244 -by (auto_tac (claset() addDs [lemma2], simpset()));
1.245 -qed "fold_set_mono";
1.246 -
1.247 -Goal "<C,x> : fold_set(A, B, f, e) ==> <C, x> : fold_set(C,B, f,e)";
1.248 -by (etac fold_set.induct 1);
1.249 -by (auto_tac (claset() addSIs fold_set.intrs, simpset()));
1.250 -by (res_inst_tac [("C1", "C"), ("A1", "cons(x, C)")]
1.251 - (fold_set_mono RS subsetD) 1);
1.252 +by (dresolve_tac [inst "C" "C" fold_set_lemma] 1);
1.253 +by (Blast_tac 1);
1.254 +by (resolve_tac fold_set.intrs 2);
1.255 by Auto_tac;
1.256 -qed "fold_set_mono2";
1.257 -
1.258 +by (blast_tac (claset() addIs [fold_set_mono RS subsetD]) 2);
1.259 +by (resolve_tac [fold_set_determ] 1);
1.260 +by (assume_tac 5);
1.261 +by Auto_tac;
1.262 +by (resolve_tac fold_set.intrs 1);
1.263 +by Auto_tac;
1.264 +by (blast_tac (claset() addIs [fold_set_mono RS subsetD]) 1);
1.265 +by (blast_tac (claset() addDs [fold_set.dom_subset RS subsetD]) 1);
1.266 +qed_spec_mp "fold_cons_lemma";
1.267
1.268 Goalw [fold_def]
1.269 - "[| Finite(C); x ~: C; e:B |] \
1.270 -\ ==> fold[B](f, e, cons(x, C)) = f(x, fold[B](f,e, C))";
1.271 -by (asm_simp_tac (simpset() addsimps [lemma]) 1);
1.272 -by (dtac Finite_into_Fin 1);
1.273 +"[| C:Fin(A); c:A; c~:C; e:B; \
1.274 +\ (ALL x:A. ALL y:B. f(x, y):B); \
1.275 +\ (ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))=f(y, f(x, z))) |]\
1.276 +\ ==> fold[B](f, e, cons(c, C)) = f(c, fold[B](f, e, C))";
1.277 +by (asm_simp_tac (simpset() addsimps [fold_cons_lemma]) 1);
1.278 by (rtac the_equality 1);
1.279 -by (dtac Fin_imp_fold_set 1);
1.280 +by (dres_inst_tac [("e", "e"), ("f", "f")] Fin_imp_fold_set 1);
1.281 by Auto_tac;
1.282 -by (res_inst_tac [("x", "xa")] exI 1);
1.283 +by (res_inst_tac [("x", "x")] exI 1);
1.284 by Auto_tac;
1.285 -by (resolve_tac [fold_set_mono RS subsetD] 1);
1.286 -by (Blast_tac 2);
1.287 -by (dtac fold_set_mono2 3);
1.288 -by (auto_tac (claset() addIs [Fin_imp_fold_set],
1.289 - simpset() addsimps [symmetric fold_def, fold_equality]));
1.290 +by (blast_tac (claset() addDs [fold_set_lemma]) 1);
1.291 +by (ALLGOALS(dtac fold_equality));
1.292 +by (auto_tac (claset(), simpset() addsimps [symmetric fold_def]));
1.293 +by (REPEAT(blast_tac (claset() addDs [FinD]) 1));
1.294 qed "fold_cons";
1.295
1.296 +Goal
1.297 +"[| C:Fin(A); e:B; \
1.298 +\ (ALL x:A. ALL y:B. f(x, y):B); \
1.299 +\ (ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))=f(y, f(x, z))) |] ==> \
1.300 +\ fold[B](f, e,C):B";
1.301 +by (etac Fin_induct 1);
1.302 +by (ALLGOALS(asm_simp_tac (simpset() addsimps [fold_cons])));
1.303 +qed_spec_mp "fold_type";
1.304 +AddTCs [fold_type];
1.305 +Addsimps [fold_type];
1.306
1.307 -Goal "Finite(C) \
1.308 -\ ==> ALL e:B. f(x, fold[B](f, e, C)) = fold[B](f, f(x, e), C)";
1.309 -by (etac Finite_induct 1);
1.310 -by (ALLGOALS(Clarify_tac));
1.311 -by (asm_full_simp_tac (simpset() addsimps [f_type]) 1);
1.312 -by (asm_simp_tac (simpset()
1.313 - addsimps [f_lcomm, fold_cons, f_type]) 1);
1.314 +Goal
1.315 +"[| C:Fin(A); c:A; \
1.316 +\ ALL x:A. ALL y:B. f(x, y):B; \
1.317 +\ ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))=f(y, f(x, z)) |] \
1.318 +\ ==> (ALL y:B. f(c, fold[B](f, y, C)) = fold[B](f, f(c, y), C))";
1.319 +by (etac Fin_induct 1);
1.320 +by (ALLGOALS(asm_simp_tac (simpset() addsimps [fold_cons])));
1.321 qed_spec_mp "fold_commute";
1.322
1.323 -
1.324 -Goal "Finite(C) ==> e:B -->fold[B](f, e, C):B";
1.325 -by (etac Finite_induct 1);
1.326 -by (ALLGOALS(Clarify_tac));
1.327 -by (Asm_simp_tac 1);
1.328 -by (asm_simp_tac (simpset() addsimps [fold_cons, f_type]) 1);
1.329 -qed_spec_mp "fold_type";
1.330 -
1.331 Goal "x:D ==> cons(x, C) Int D = cons(x, C Int D)";
1.332 by Auto_tac;
1.333 qed "cons_Int_right_lemma1";
1.334 @@ -202,30 +249,36 @@
1.335 by Auto_tac;
1.336 qed "cons_Int_right_lemma2";
1.337
1.338 -Goal "[| Finite(C); Finite(D); e:B|] \
1.339 -\ ==> fold[B](f, fold[B](f, e, D), C) \
1.340 +Goal
1.341 +"[| C:Fin(A); D:Fin(A); e:B; \
1.342 +\ ALL x:A. ALL y:B. f(x, y):B; \
1.343 +\ ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))=f(y, f(x, z)) |] \
1.344 +\ ==> \
1.345 +\ fold[B](f, fold[B](f, e, D), C) \
1.346 \ = fold[B](f, fold[B](f, e, (C Int D)), C Un D)";
1.347 -by (etac Finite_induct 1);
1.348 -by (asm_full_simp_tac (simpset() addsimps [f_type, fold_type]) 1);
1.349 -by (subgoal_tac "Finite(Ba Int D) & \
1.350 - \cons(x, Ba) Un D = cons(x, Ba Un D) & \
1.351 - \Finite(Ba Un D)" 1);
1.352 -by (auto_tac (claset()
1.353 - addIs [Finite_Un,Int_lower1 RS subset_Finite], simpset()));
1.354 +by (etac Fin_induct 1);
1.355 +by Auto_tac;
1.356 +by (subgoal_tac "cons(x, y) Un D = cons(x, y Un D)" 1);
1.357 +by Auto_tac;
1.358 +by (subgoal_tac "y Int D:Fin(A) & y Un D:Fin(A)" 1);
1.359 +by (Clarify_tac 1);
1.360 by (case_tac "x:D" 1);
1.361 by (ALLGOALS(asm_simp_tac (simpset() addsimps
1.362 [cons_Int_right_lemma1,cons_Int_right_lemma2,
1.363 - fold_type, fold_cons,fold_commute,cons_absorb, f_type])));
1.364 + fold_cons, fold_commute,cons_absorb])));
1.365 qed "fold_nest_Un_Int";
1.366
1.367 -
1.368 -Goal "[| Finite(C); Finite(D); C Int D = 0; e:B |] \
1.369 +Goal "[| C:Fin(A); D:Fin(A); C Int D = 0; e:B; \
1.370 +\ ALL x:A. ALL y:B. f(x, y):B; \
1.371 +\ ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))=f(y, f(x, z)) |] \
1.372 \ ==> fold[B](f,e,C Un D) = fold[B](f, fold[B](f,e,D), C)";
1.373 by (asm_simp_tac (simpset() addsimps [fold_nest_Un_Int]) 1);
1.374 qed "fold_nest_Un_disjoint";
1.375
1.376 -Close_locale "LC";
1.377 -
1.378 +Goal "Finite(C) ==> C:Fin(cons(c, C))";
1.379 +by (dtac Finite_into_Fin 1);
1.380 +by (blast_tac (claset() addIs [Fin_mono RS subsetD]) 1);
1.381 +qed "Finite_cons_lemma";
1.382
1.383 (** setsum **)
1.384
1.385 @@ -237,7 +290,9 @@
1.386 Goalw [setsum_def]
1.387 "[| Finite(C); c~:C |] \
1.388 \ ==> setsum(g, cons(c, C)) = g(c) $+ setsum(g, C)";
1.389 -by (asm_simp_tac (simpset() addsimps [Finite_cons,export fold_cons]) 1);
1.390 +by (auto_tac (claset(), simpset() addsimps [Finite_cons]));
1.391 +by (res_inst_tac [("A", "cons(c, C)")] fold_cons 1);
1.392 +by (auto_tac (claset() addIs [Finite_cons_lemma], simpset()));
1.393 qed "setsum_cons";
1.394 Addsimps [setsum_cons];
1.395
1.396 @@ -341,8 +396,6 @@
1.397 by (asm_full_simp_tac (simpset() addsimps [Ball_def, major]@prems) 1);
1.398 qed_spec_mp "setsum_cong";
1.399
1.400 -(** For the natural numbers, we have subtraction **)
1.401 -
1.402 Goal "[| Finite(A); Finite(B) |] \
1.403 \ ==> setsum(f, A Un B) = \
1.404 \ setsum(f, A) $+ setsum(f, B) $- setsum(f, A Int B)";
2.1 --- a/src/ZF/Induct/FoldSet.thy Mon Jan 28 23:35:20 2002 +0100
2.2 +++ b/src/ZF/Induct/FoldSet.thy Wed Jan 30 12:22:40 2002 +0100
2.3 @@ -23,16 +23,9 @@
2.4 constdefs
2.5
2.6 fold :: "[i, [i,i]=>i, i, i] => i" ("fold[_]'(_,_,_')")
2.7 - "fold[B](f,e,C) == THE x. <C,x>:fold_set(C, B, f,e)"
2.8 + "fold[B](f,e, A) == THE x. <A, x>:fold_set(A, B, f,e)"
2.9
2.10 setsum :: "[i=>i, i] => i"
2.11 "setsum(g, C) == if Finite(C) then
2.12 fold[int](%x y. g(x) $+ y, #0, C) else #0"
2.13 -locale LC =
2.14 - fixes
2.15 - B :: i
2.16 - f :: [i,i] => i
2.17 - assumes
2.18 - ftype "f(x,y):B"
2.19 - lcomm "f(x, f(y, z)) = f(y,f(x, z))"
2.20 end
2.21 \ No newline at end of file
3.1 --- a/src/ZF/Induct/Multiset.ML Mon Jan 28 23:35:20 2002 +0100
3.2 +++ b/src/ZF/Induct/Multiset.ML Wed Jan 30 12:22:40 2002 +0100
3.3 @@ -29,37 +29,46 @@
3.4 simpset() addsimps [range_of_fun, apply_iff]));
3.5 qed "multiset_fun_iff";
3.6
3.7 -(** multiset and multiset_on **)
3.8 +(** The multiset space **)
3.9 +Goalw [multiset_def]
3.10 + "[| multiset(M); mset_of(M)<=A |] ==> M:Mult(A)";
3.11 +by (auto_tac (claset(), simpset()
3.12 + addsimps [multiset_fun_iff, mset_of_def]));
3.13 +by (rotate_simp_tac "M:?u" 1);
3.14 +by (res_inst_tac [("B1","nat-{0}")] (FiniteFun_mono RS subsetD) 1);
3.15 +by (ALLGOALS(Asm_simp_tac));
3.16 +by (rtac (Finite_into_Fin RSN (2, Fin_mono RS subsetD) RS fun_FiniteFunI) 1);
3.17 +by (ALLGOALS(asm_simp_tac (simpset() addsimps [multiset_fun_iff])));
3.18 +qed "multiset_into_Mult";
3.19
3.20 -Goalw [multiset_on_def, multiset_def]
3.21 -"multiset[A](M) ==> multiset(M)";
3.22 -by Auto_tac;
3.23 -qed "multiset_on_imp_multiset";
3.24 +Goalw [multiset_def, mset_of_def]
3.25 + "M:Mult(A) ==> multiset(M) & mset_of(M)<=A";
3.26 +by (ftac FiniteFun_is_fun 1);
3.27 +by (dtac FiniteFun_domain_Fin 1);
3.28 +by (ftac FinD 1);
3.29 +by (Clarify_tac 1);
3.30 +by (res_inst_tac [("x", "domain(M)")] exI 1);
3.31 +by (blast_tac (claset() addIs [Fin_into_Finite]) 1);
3.32 +qed "Mult_into_multiset";
3.33
3.34 -Goalw [multiset_on_def, multiset_def]
3.35 -"multiset(M) ==> multiset[mset_of(M)](M)";
3.36 -by Auto_tac;
3.37 -qed "multiset_imp_multiset_on_set_of";
3.38 +Goal "M:Mult(A) <-> multiset(M) & mset_of(M)<=A";
3.39 +by (blast_tac (claset() addDs [Mult_into_multiset]
3.40 + addIs [multiset_into_Mult]) 1);
3.41 +qed "Mult_iff_multiset";
3.42
3.43 -Goal "multiset(M) <-> multiset[mset_of(M)](M)";
3.44 -by (blast_tac (claset() addIs [multiset_on_imp_multiset,
3.45 - multiset_imp_multiset_on_set_of]) 1);
3.46 -qed "multiset_iff_multiset_on_set_of";
3.47 +Goal "multiset(M) <-> M:Mult(mset_of(M))";
3.48 +by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
3.49 +qed "multiset_iff_Mult_mset_of";
3.50
3.51 -Goalw [multiset_on_def]
3.52 - "[| A<= B; multiset[A](M) |] ==> multiset[B](M)";
3.53 -by Auto_tac;
3.54 -qed "subset_multiset_on";
3.55 +(** multiset **)
3.56
3.57 (* the empty multiset is 0 *)
3.58
3.59 -Goalw [multiset_def, mset_of_def]
3.60 - "multiset(0)";
3.61 -by Auto_tac;
3.62 -by (res_inst_tac [("x", "0")] exI 1);
3.63 -by (simp_tac (simpset() addsimps [Finite_0]) 1);
3.64 +Goal "multiset(0)";
3.65 +by (auto_tac (claset() addIs FiniteFun.intrs,
3.66 + simpset() addsimps [multiset_iff_Mult_mset_of]));
3.67 qed "multiset_0";
3.68 -AddIffs [multiset_0];
3.69 +Addsimps [multiset_0];
3.70
3.71 (** mset_of **)
3.72
3.73 @@ -151,7 +160,7 @@
3.74 qed "normalize_multiset";
3.75 Addsimps [normalize_multiset];
3.76
3.77 -Goalw [multiset_def, multiset_on_def]
3.78 +Goalw [multiset_def]
3.79 "[| f:A -> nat; Finite(A) |] ==> multiset(normalize(f))";
3.80 by (rewrite_goals_tac [normalize_def, mset_of_def]);
3.81 by Auto_tac;
3.82 @@ -261,13 +270,13 @@
3.83 by (rewrite_goals_tac [mcount_def, mset_of_def]);
3.84 by (auto_tac (claset(), simpset() addsimps [multiset_fun_iff]));
3.85 qed "mcount_type";
3.86 -AddIs [mcount_type];
3.87 +AddTCs [mcount_type];
3.88 Addsimps [mcount_type];
3.89
3.90 Goalw [mcount_def] "mcount(0, a) = 0";
3.91 by Auto_tac;
3.92 qed "mcount_0";
3.93 -AddIffs [mcount_0];
3.94 +Addsimps [mcount_0];
3.95
3.96 Goalw [mcount_def, mset_of_def, msingle_def]
3.97 "mcount({#b#}, a) = (if a=b then 1 else 0)";
3.98 @@ -319,8 +328,6 @@
3.99 qed "msize_type";
3.100 Addsimps [msize_type];
3.101 AddTCs [msize_type];
3.102 -AddIs [msize_type];
3.103 -
3.104
3.105 Goalw [msize_def] "multiset(M)==> #0 $<= msize(M)";
3.106 by (auto_tac (claset() addIs [g_zpos_imp_setsum_zpos], simpset()));
3.107 @@ -751,94 +758,61 @@
3.108 by Auto_tac;
3.109 qed "munion_eq_conv_diff";
3.110
3.111 -Goalw [multiset_on_def]
3.112 -"[| multiset[A](M); multiset[A](N) |] \
3.113 +Goal
3.114 +"[| M:Mult(A); N:Mult(A) |] \
3.115 \ ==> (M +# {#a#} = N +# {#b#}) <-> \
3.116 -\ (M=N & a=b | (EX K. multiset[A](K)& M= K +# {#b#} & N=K +# {#a#}))";
3.117 +\ (M=N & a=b | (EX K:Mult(A). M= K +# {#b#} & N=K +# {#a#}))";
3.118 by (auto_tac (claset(),
3.119 - simpset() addsimps [melem_diff_single, munion_eq_conv_diff]));
3.120 + simpset() addsimps [Bex_def, Mult_iff_multiset,
3.121 + melem_diff_single, munion_eq_conv_diff]));
3.122 qed "munion_eq_conv_exist";
3.123
3.124 (** multiset orderings **)
3.125
3.126 (* multiset on a domain A are finite functions from A to nat-{0} *)
3.127
3.128 -Goalw [multiset_on_def, multiset_def]
3.129 - "multiset[A](M) ==> M:A-||>nat-{0}";
3.130 -by (auto_tac (claset(), simpset()
3.131 - addsimps [multiset_fun_iff, mset_of_def]));
3.132 -by (rotate_simp_tac "M:?u" 1);
3.133 -by (res_inst_tac [("B1","nat-{0}")] (FiniteFun_mono RS subsetD) 1);
3.134 -by (ALLGOALS(Asm_simp_tac));
3.135 -by (rtac (Finite_into_Fin RSN (2, Fin_mono RS subsetD) RS fun_FiniteFunI) 1);
3.136 -by (ALLGOALS(asm_simp_tac (simpset() addsimps [multiset_fun_iff])));
3.137 -qed "multiset_on_is_FiniteFun";
3.138 -
3.139 -Goalw [multiset_on_def, multiset_def, mset_of_def]
3.140 - "M:A-||>nat-{0} ==> multiset[A](M)";
3.141 -by (ftac FiniteFun_is_fun 1);
3.142 -by (dtac FiniteFun_domain_Fin 1);
3.143 -by (ftac FinD 1);
3.144 -by (Clarify_tac 1);
3.145 -by (res_inst_tac [("x", "domain(M)")] exI 1);
3.146 -by (blast_tac (claset() addIs [Fin_into_Finite]) 1);
3.147 -qed "FiniteFun_is_multiset_on";
3.148 -
3.149 -Goal "M:A-||>nat-{0} <-> multiset[A](M)";
3.150 -by (blast_tac (claset() addDs [FiniteFun_is_multiset_on]
3.151 - addIs [multiset_on_is_FiniteFun]) 1);
3.152 -qed "FiniteFun_iff_multiset_on";
3.153
3.154 (* multirel1 type *)
3.155
3.156 Goalw [multirel1_def]
3.157 -"multirel1(A, r) <= (A-||>nat-{0})*(A-||>nat-{0})";
3.158 +"multirel1(A, r) <= Mult(A)*Mult(A)";
3.159 by Auto_tac;
3.160 qed "multirel1_type";
3.161
3.162 -Goal "<M, N>:multirel1(A, r) ==> multiset[A](M) & multiset[A](N)";
3.163 -by (dtac (multirel1_type RS subsetD) 1);
3.164 -by (asm_full_simp_tac (simpset() addsimps [FiniteFun_iff_multiset_on]) 1);
3.165 -qed "multirel1D";
3.166 -
3.167 Goalw [multirel1_def] "multirel1(0, r) =0";
3.168 by Auto_tac;
3.169 qed "multirel1_0";
3.170 AddIffs [multirel1_0];
3.171
3.172 -Goalw [multirel1_def, Ball_def, Bex_def]
3.173 +Goalw [multirel1_def]
3.174 " <N, M>:multirel1(A, r) <-> \
3.175 -\ (EX a. a:A & \
3.176 -\ (EX M0. multiset[A](M0) & (EX K. multiset[A](K) & \
3.177 +\ (EX a. a:A & \
3.178 +\ (EX M0. M0:Mult(A) & (EX K. K:Mult(A) & \
3.179 \ M=M0 +# {#a#} & N=M0 +# K & (ALL b:mset_of(K). <b,a>:r))))";
3.180 -by (auto_tac (claset(), simpset()
3.181 - addsimps [FiniteFun_iff_multiset_on, multiset_on_def]));
3.182 +by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset, Ball_def, Bex_def]));
3.183 qed "multirel1_iff";
3.184
3.185 (* Monotonicity of multirel1 *)
3.186
3.187 Goalw [multirel1_def] "A<=B ==> multirel1(A, r)<=multirel1(B, r)";
3.188 -by (auto_tac (claset(), simpset() addsimps [FiniteFun_iff_multiset_on]));
3.189 +by (auto_tac (claset(), simpset() addsimps []));
3.190 by (ALLGOALS(asm_full_simp_tac(simpset()
3.191 - addsimps [Un_subset_iff, multiset_on_def])));
3.192 + addsimps [Un_subset_iff, Mult_iff_multiset])));
3.193 by (res_inst_tac [("x", "x")] bexI 3);
3.194 by (res_inst_tac [("x", "xb")] bexI 3);
3.195 by (Asm_simp_tac 3);
3.196 by (res_inst_tac [("x", "K")] bexI 3);
3.197 -by (ALLGOALS(asm_simp_tac (simpset()
3.198 - addsimps [FiniteFun_iff_multiset_on, multiset_on_def])));
3.199 +by (ALLGOALS(asm_simp_tac (simpset() addsimps [Mult_iff_multiset])));
3.200 by Auto_tac;
3.201 qed "multirel1_mono1";
3.202
3.203 Goalw [multirel1_def] "r<=s ==> multirel1(A,r)<=multirel1(A, s)";
3.204 -by (auto_tac (claset(), simpset() addsimps [FiniteFun_iff_multiset_on]));
3.205 +by (auto_tac (claset(), simpset() addsimps []));
3.206 by (res_inst_tac [("x", "x")] bexI 1);
3.207 by (res_inst_tac [("x", "xb")] bexI 1);
3.208 -by (ALLGOALS(asm_full_simp_tac (simpset()
3.209 - addsimps [FiniteFun_iff_multiset_on, multiset_on_def])));
3.210 +by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [Mult_iff_multiset])));
3.211 by (res_inst_tac [("x", "K")] bexI 1);
3.212 -by (ALLGOALS(asm_full_simp_tac (simpset()
3.213 - addsimps [FiniteFun_iff_multiset_on,multiset_on_def])));
3.214 +by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [Mult_iff_multiset])));
3.215 by Auto_tac;
3.216 qed "multirel1_mono2";
3.217
3.218 @@ -853,27 +827,26 @@
3.219 (* Towards the proof of well-foundedness of multirel1 *)
3.220
3.221 Goalw [multirel1_def] "<M,0>~:multirel1(A, r)";
3.222 -by (auto_tac (claset(), simpset()
3.223 - addsimps [FiniteFun_iff_multiset_on, multiset_on_def]));
3.224 +by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
3.225 qed "not_less_0";
3.226 AddIffs [not_less_0];
3.227
3.228 -Goal "[| <N, M0 +# {#a#}>:multirel1(A, r); multiset[A](M0) |] ==> \
3.229 +Goal "[| <N, M0 +# {#a#}>:multirel1(A, r); M0:Mult(A) |] ==> \
3.230 \ (EX M. <M, M0>:multirel1(A, r) & N = M +# {#a#}) | \
3.231 -\ (EX K. multiset[A](K) & (ALL b:mset_of(K). <b, a>:r) & N = M0 +# K)";
3.232 -by (ftac multirel1D 1);
3.233 +\ (EX K. K:Mult(A) & (ALL b:mset_of(K). <b, a>:r) & N = M0 +# K)";
3.234 +by (forward_tac [multirel1_type RS subsetD] 1);
3.235 by (asm_full_simp_tac (simpset() addsimps [multirel1_iff]) 1);
3.236 by (auto_tac (claset(), simpset() addsimps [munion_eq_conv_exist]));
3.237 by (ALLGOALS(res_inst_tac [("x", "Ka +# K")] exI));
3.238 by Auto_tac;
3.239 -by (rewtac multiset_on_def);
3.240 +by (rewtac (Mult_iff_multiset RS iff_reflection));
3.241 by (asm_simp_tac (simpset() addsimps [munion_left_cancel, munion_assoc]) 1);
3.242 by (auto_tac (claset(), simpset() addsimps [munion_commute]));
3.243 qed "less_munion";
3.244
3.245 -Goal "[| multiset[A](M); a:A |] ==> <M, M +# {#a#}>: multirel1(A, r)";
3.246 +Goal "[| M:Mult(A); a:A |] ==> <M, M +# {#a#}>: multirel1(A, r)";
3.247 by (auto_tac (claset(), simpset() addsimps [multirel1_iff]));
3.248 -by (rewtac multiset_on_def);
3.249 +by (rewrite_goals_tac [Mult_iff_multiset RS iff_reflection]);
3.250 by (res_inst_tac [("x", "a")] exI 1);
3.251 by (Clarify_tac 1);
3.252 by (res_inst_tac [("x", "M")] exI 1);
3.253 @@ -892,15 +865,15 @@
3.254 \ M0:acc(multirel1(A, r)); a:A; \
3.255 \ ALL M. <M,M0> : multirel1(A, r) --> M +# {#a#} : acc(multirel1(A, r)) |] \
3.256 \ ==> M0 +# {#a#} : acc(multirel1(A, r))";
3.257 -by (subgoal_tac "multiset[A](M0)" 1);
3.258 +by (subgoal_tac "M0:Mult(A)" 1);
3.259 by (etac (thm "acc.cases") 2);
3.260 by (etac fieldE 2);
3.261 -by (REPEAT(blast_tac (claset() addDs [multirel1D]) 2));
3.262 +by (REPEAT(blast_tac (claset() addDs [multirel1_type RS subsetD]) 2));
3.263 by (rtac (thm "accI") 1);
3.264 by (rename_tac "N" 1);
3.265 by (dtac less_munion 1);
3.266 by (Blast_tac 1);
3.267 -by (auto_tac (claset(), simpset() addsimps [multiset_on_def]));
3.268 +by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
3.269 by (eres_inst_tac [("P", "ALL x:mset_of(K). <x, a>:r")] rev_mp 1);
3.270 by (eres_inst_tac [("P", "mset_of(K)<=A")] rev_mp 1);
3.271 by (eres_inst_tac [("M", "K")] multiset_induct 1);
3.272 @@ -920,7 +893,7 @@
3.273 by (asm_full_simp_tac (simpset() addsimps [munion_assoc RS sym]) 1);
3.274 (* subgoal 3: additional conditions *)
3.275 by (auto_tac (claset() addSIs [multirel1_base RS fieldI2],
3.276 - simpset() addsimps [multiset_on_def]));
3.277 + simpset() addsimps [Mult_iff_multiset]));
3.278 qed "lemma1";
3.279
3.280 Goal "[| ALL b:A. <b,a>:r \
3.281 @@ -955,15 +928,15 @@
3.282 by (Blast_tac 1);
3.283 by (subgoal_tac "M:field(multirel1(A,r))" 1);
3.284 by (rtac (multirel1_base RS fieldI1) 2);
3.285 -by (rewrite_goal_tac [multiset_on_def] 2);
3.286 +by (rewrite_goal_tac [Mult_iff_multiset RS iff_reflection] 2);
3.287 by (REPEAT(Blast_tac 1));
3.288 qed "lemma4";
3.289
3.290 -Goal "[| wf[A](r); multiset[A](M); A ~= 0|] ==> M:acc(multirel1(A, r))";
3.291 +Goal "[| wf[A](r); M:Mult(A); A ~= 0|] ==> M:acc(multirel1(A, r))";
3.292 by (etac not_emptyE 1);
3.293 by (rtac (lemma4 RS mp RS mp RS mp) 1);
3.294 by (rtac (multirel1_base RS fieldI1) 4);
3.295 -by (auto_tac (claset(), simpset() addsimps [multiset_on_def]));
3.296 +by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
3.297 qed "all_accessible";
3.298
3.299 Goal "wf[A](r) ==> wf[A-||>nat-{0}](multirel1(A, r))";
3.300 @@ -975,7 +948,7 @@
3.301 by (res_inst_tac [("A", "acc(multirel1(A,r))")] wf_on_subset_A 1);
3.302 by (rtac (thm "wf_on_acc") 1);
3.303 by (Clarify_tac 1);
3.304 -by (full_simp_tac (simpset() addsimps [FiniteFun_iff_multiset_on]) 1);
3.305 +by (full_simp_tac (simpset() addsimps []) 1);
3.306 by (blast_tac (claset() addIs [all_accessible]) 1);
3.307 qed "wf_on_multirel1";
3.308
3.309 @@ -991,21 +964,14 @@
3.310 (** multirel **)
3.311
3.312 Goalw [multirel_def]
3.313 - "multirel(A, r) <= (A-||>nat-{0}) * (A-||>nat-{0})";
3.314 + "multirel(A, r) <= Mult(A)*Mult(A)";
3.315 by (rtac (trancl_type RS subset_trans) 1);
3.316 by (Clarify_tac 1);
3.317 -by (auto_tac (claset() addDs [multirel1D],
3.318 - simpset() addsimps [FiniteFun_iff_multiset_on]));
3.319 +by (auto_tac (claset() addDs [multirel1_type RS subsetD],
3.320 + simpset() addsimps []));
3.321 qed "multirel_type";
3.322
3.323 -Goal "<M, N>:multirel(A, r) ==> multiset[A](M) & multiset[A](N)";
3.324 -by (dtac (multirel_type RS subsetD) 1);
3.325 -by (asm_simp_tac (simpset() addsimps [FiniteFun_iff_multiset_on RS iff_sym]) 1);
3.326 -by Auto_tac;
3.327 -qed "multirelD";
3.328 -
3.329 (* Monotonicity of multirel *)
3.330 -
3.331 Goalw [multirel_def]
3.332 "[| A<=B; r<=s |] ==> multirel(A, r)<=multirel(B,s)";
3.333 by (rtac trancl_mono 1);
3.334 @@ -1041,12 +1007,12 @@
3.335 "<M,N>:multirel(A, r) ==> \
3.336 \ trans[A](r) --> \
3.337 \ (EX I J K. \
3.338 -\ multiset[A](I) & multiset[A](J) & multiset[A](K) & \
3.339 +\ I:Mult(A) & J:Mult(A) & K:Mult(A) & \
3.340 \ N = I +# J & M = I +# K & J ~= 0 & \
3.341 \ (ALL k:mset_of(K). EX j:mset_of(J). <k,j>:r))";
3.342 by (etac converse_trancl_induct 1);
3.343 by (ALLGOALS(asm_full_simp_tac (simpset()
3.344 - addsimps [multirel1_iff, multiset_on_def])));
3.345 + addsimps [multirel1_iff, Mult_iff_multiset])));
3.346 by (ALLGOALS(Clarify_tac));
3.347 (* Two subgoals remain *)
3.348 (* Subgoal 1 *)
3.349 @@ -1103,23 +1069,23 @@
3.350 qed "melem_imp_eq_diff_union";
3.351 Addsimps [melem_imp_eq_diff_union];
3.352
3.353 -Goal "[| msize(M)=$# succ(n); multiset[A](M); n:nat |] \
3.354 -\ ==> EX a N. M = N +# {#a#} & multiset[A](N) & a:A";
3.355 +Goal "[| msize(M)=$# succ(n); M:Mult(A); n:nat |] \
3.356 +\ ==> EX a N. M = N +# {#a#} & N:Mult(A) & a:A";
3.357 by (dtac msize_eq_succ_imp_elem 1);
3.358 by Auto_tac;
3.359 by (res_inst_tac [("x", "a")] exI 1);
3.360 by (res_inst_tac [("x", "M -# {#a#}")] exI 1);
3.361 -by (ftac multiset_on_imp_multiset 1);
3.362 +by (ftac Mult_into_multiset 1);
3.363 by (Asm_simp_tac 1);
3.364 -by (auto_tac (claset(), simpset() addsimps [multiset_on_def]));
3.365 +by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
3.366 qed "msize_eq_succ_imp_eq_union";
3.367
3.368 (* The second direction *)
3.369
3.370 -Goalw [multiset_on_def]
3.371 +Goalw [Mult_iff_multiset RS iff_reflection]
3.372 "n:nat ==> \
3.373 \ (ALL I J K. \
3.374 -\ multiset[A](I) & multiset[A](J) & multiset[A](K) & \
3.375 +\ I:Mult(A) & J:Mult(A) & K:Mult(A) & \
3.376 \ (msize(J) = $# n & J ~=0 & (ALL k:mset_of(K). EX j:mset_of(J). <k, j>:r)) \
3.377 \ --> <I +# K, I +# J>:multirel(A, r))";
3.378 by (etac nat_induct 1);
3.379 @@ -1130,7 +1096,7 @@
3.380 by (subgoal_tac "msize(J)=$# succ(x)" 1);
3.381 by (Asm_simp_tac 2);
3.382 by (forw_inst_tac [("A", "A")] msize_eq_succ_imp_eq_union 1);
3.383 -by (rewtac multiset_on_def);
3.384 +by (rewtac (Mult_iff_multiset RS iff_reflection));
3.385 by (Clarify_tac 3 THEN rotate_tac ~1 3);
3.386 by (ALLGOALS(Asm_full_simp_tac));
3.387 by (rename_tac "J'" 1);
3.388 @@ -1139,7 +1105,7 @@
3.389 by (asm_full_simp_tac (simpset() addsimps [multirel_def]) 1);
3.390 by (rtac r_into_trancl 1);
3.391 by (Clarify_tac 1);
3.392 -by (asm_full_simp_tac (simpset() addsimps [multirel1_iff, multiset_on_def]) 1);
3.393 +by (asm_full_simp_tac (simpset() addsimps [multirel1_iff, Mult_iff_multiset]) 1);
3.394 by (Force_tac 1);
3.395 (*Now we know J' ~= 0*)
3.396 by (rotate_simp_tac "multiset(J')" 1);
3.397 @@ -1165,7 +1131,7 @@
3.398 by (res_inst_tac [("b", "I +# {# x:K. <x, a>:r#} +# J'")] trancl_trans 1);
3.399 by (Blast_tac 1);
3.400 by (rtac r_into_trancl 1);
3.401 -by (asm_full_simp_tac (simpset() addsimps [multirel1_iff, multiset_on_def]) 1);
3.402 +by (asm_full_simp_tac (simpset() addsimps [multirel1_iff, Mult_iff_multiset]) 1);
3.403 by (res_inst_tac [("x", "a")] exI 1);
3.404 by (Asm_simp_tac 1);
3.405 by (res_inst_tac [("x", "I +# J'")] exI 1);
3.406 @@ -1177,10 +1143,10 @@
3.407 qed_spec_mp "one_step_implies_multirel_lemma";
3.408
3.409 Goal "[| J ~= 0; ALL k:mset_of(K). EX j:mset_of(J). <k,j>:r;\
3.410 -\ multiset[A](I); multiset[A](J); multiset[A](K) |] \
3.411 +\ I:Mult(A); J:Mult(A); K:Mult(A) |] \
3.412 \ ==> <I+#K, I+#J> : multirel(A, r)";
3.413 by (subgoal_tac "multiset(J)" 1);
3.414 -by (asm_full_simp_tac (simpset() addsimps [multiset_on_def]) 2);
3.415 +by (asm_full_simp_tac (simpset() addsimps [Mult_iff_multiset]) 2);
3.416 by (forw_inst_tac [("M", "J")] msize_int_of_nat 1);
3.417 by (auto_tac (claset() addIs [one_step_implies_multirel_lemma], simpset()));
3.418 qed "one_step_implies_multirel";
3.419 @@ -1201,14 +1167,14 @@
3.420 qed "multirel_irrefl_lemma";
3.421
3.422 Goalw [irrefl_def]
3.423 -"part_ord(A, r) ==> irrefl(A-||>nat-{0}, multirel(A, r))";
3.424 +"part_ord(A, r) ==> irrefl(Mult(A), multirel(A, r))";
3.425 by (subgoal_tac "trans[A](r)" 1);
3.426 by (asm_full_simp_tac (simpset() addsimps [part_ord_def]) 2);
3.427 by (Clarify_tac 1);
3.428 -by (asm_full_simp_tac (simpset() addsimps [FiniteFun_iff_multiset_on]) 1);
3.429 +by (asm_full_simp_tac (simpset() addsimps []) 1);
3.430 by (dtac multirel_implies_one_step 1);
3.431 by (Clarify_tac 1);
3.432 -by (rewrite_goal_tac [multiset_on_def] 1);
3.433 +by (rewrite_goal_tac [Mult_iff_multiset RS iff_reflection] 1);
3.434 by (Asm_full_simp_tac 1);
3.435 by (Clarify_tac 1);
3.436 by (subgoal_tac "Finite(mset_of(K))" 1);
3.437 @@ -1219,8 +1185,7 @@
3.438 by (rotate_simp_tac "K:?u" 1);
3.439 qed "irrefl_on_multirel";
3.440
3.441 -Goalw [multirel_def, trans_on_def]
3.442 -"trans[A-||>nat-{0}](multirel(A, r))";
3.443 +Goalw [multirel_def, trans_on_def] "trans[Mult(A)](multirel(A, r))";
3.444 by (blast_tac (claset() addIs [trancl_trans]) 1);
3.445 qed "trans_on_multirel";
3.446
3.447 @@ -1233,7 +1198,7 @@
3.448 by (rtac trans_trancl 1);
3.449 qed "trans_multirel";
3.450
3.451 -Goal "part_ord(A,r) ==> part_ord(A-||>nat-{0}, multirel(A, r))";
3.452 +Goal "part_ord(A,r) ==> part_ord(Mult(A), multirel(A, r))";
3.453 by (simp_tac (simpset() addsimps [part_ord_def]) 1);
3.454 by (blast_tac (claset() addIs [irrefl_on_multirel, trans_on_multirel]) 1);
3.455 qed "part_ord_multirel";
3.456 @@ -1241,9 +1206,9 @@
3.457 (** Monotonicity of multiset union **)
3.458
3.459 Goal
3.460 -"[|<M,N>:multirel1(A, r); multiset[A](K)|] ==> <K +# M, K +# N>: multirel1(A, r)";
3.461 -by (ftac multirel1D 1);
3.462 -by (auto_tac (claset(), simpset() addsimps [multirel1_iff, multiset_on_def]));
3.463 +"[|<M,N>:multirel1(A, r); K:Mult(A) |] ==> <K +# M, K +# N>:multirel1(A, r)";
3.464 +by (ftac (multirel1_type RS subsetD) 1);
3.465 +by (auto_tac (claset(), simpset() addsimps [multirel1_iff, Mult_iff_multiset]));
3.466 by (res_inst_tac [("x", "a")] exI 1);
3.467 by (Asm_simp_tac 1);
3.468 by (res_inst_tac [("x", "K+#M0")] exI 1);
3.469 @@ -1252,10 +1217,9 @@
3.470 by (asm_simp_tac (simpset() addsimps [munion_assoc]) 1);
3.471 qed "munion_multirel1_mono";
3.472
3.473 -
3.474 Goal
3.475 - "[| <M, N>:multirel(A, r); multiset[A](K) |]==><K +# M, K +# N>:multirel(A, r)";
3.476 -by (ftac multirelD 1);
3.477 + "[| <M, N>:multirel(A, r); K:Mult(A) |]==><K +# M, K +# N>:multirel(A, r)";
3.478 +by (ftac (multirel_type RS subsetD) 1);
3.479 by (full_simp_tac (simpset() addsimps [multirel_def]) 1);
3.480 by (Clarify_tac 1);
3.481 by (dres_inst_tac [("psi", "<M,N>:multirel1(A, r)^+")] asm_rl 1);
3.482 @@ -1266,28 +1230,26 @@
3.483 by (Clarify_tac 1);
3.484 by (blast_tac (claset() addIs [munion_multirel1_mono, r_into_trancl]) 1);
3.485 by (Clarify_tac 1);
3.486 -by (subgoal_tac "multiset[A](y)" 1);
3.487 -by (blast_tac (claset() addDs [rewrite_rule [multirel_def] multirelD]) 2);
3.488 +by (subgoal_tac "y:Mult(A)" 1);
3.489 +by (blast_tac (claset() addDs [rewrite_rule [multirel_def] multirel_type RS subsetD]) 2);
3.490 by (subgoal_tac "<K +# y, K +# z>:multirel1(A, r)" 1);
3.491 by (blast_tac (claset() addIs [munion_multirel1_mono]) 2);
3.492 by (blast_tac (claset() addIs [r_into_trancl, trancl_trans]) 1);
3.493 qed "munion_multirel_mono2";
3.494
3.495 Goal
3.496 -"[|<M, N>:multirel(A, r); multiset[A](K)|] ==> <M +# K, N +# K>:multirel(A, r)";
3.497 -by (ftac multirelD 1);
3.498 +"[|<M, N>:multirel(A, r); K:Mult(A)|] ==> <M +# K, N +# K>:multirel(A, r)";
3.499 +by (ftac (multirel_type RS subsetD) 1);
3.500 by (res_inst_tac [("P", "%x. <x,?u>:multirel(A, r)")] (munion_commute RS subst) 1);
3.501 by (stac (munion_commute RS sym) 3);
3.502 -by (rtac munion_multirel_mono2 5);
3.503 -by (rewtac multiset_on_def);
3.504 -by Auto_tac;
3.505 +by (rtac munion_multirel_mono2 5);
3.506 +by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
3.507 qed "munion_multirel_mono1";
3.508
3.509 Goal
3.510 "[|<M,K>:multirel(A, r); <N,L>:multirel(A, r)|]==><M +# N, K +# L>:multirel(A, r)";
3.511 -by (subgoal_tac "multiset[A](M)& multiset[A](N) & \
3.512 -\ multiset[A](K)& multiset[A](L)" 1);
3.513 -by (blast_tac (claset() addDs [multirelD]) 2);
3.514 +by (subgoal_tac "M:Mult(A)& N:Mult(A) & K:Mult(A)& L:Mult(A)" 1);
3.515 +by (blast_tac (claset() addDs [multirel_type RS subsetD]) 2);
3.516 by (blast_tac (claset()
3.517 addIs [munion_multirel_mono1, multirel_trans, munion_multirel_mono2]) 1);
3.518 qed "munion_multirel_mono";
3.519 @@ -1304,8 +1266,8 @@
3.520 bind_thm ("multirel_Memrel_mono",
3.521 [field_Memrel_mono, Memrel_mono]MRS multirel_mono);
3.522
3.523 -Goalw [omultiset_def, multiset_on_def] "omultiset(M) ==> multiset(M)";
3.524 -by Auto_tac;
3.525 +Goalw [omultiset_def] "omultiset(M) ==> multiset(M)";
3.526 +by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
3.527 qed "omultiset_is_multiset";
3.528 Addsimps [omultiset_is_multiset];
3.529
3.530 @@ -1313,13 +1275,13 @@
3.531 by (Clarify_tac 1);
3.532 by (res_inst_tac [("x", "i Un ia")] exI 1);
3.533 by (asm_full_simp_tac (simpset() addsimps
3.534 - [multiset_on_def, Ord_Un, Un_subset_iff]) 1);
3.535 + [Mult_iff_multiset, Ord_Un, Un_subset_iff]) 1);
3.536 by (blast_tac (claset() addIs [field_Memrel_mono]) 1);
3.537 qed "munion_omultiset";
3.538 Addsimps [munion_omultiset];
3.539
3.540 Goalw [omultiset_def] "omultiset(M) ==> omultiset(M -# N)";
3.541 -by (auto_tac (claset(), simpset() addsimps [multiset_on_def]));
3.542 +by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
3.543 by (res_inst_tac [("x", "i")] exI 1);
3.544 by (Asm_simp_tac 1);
3.545 qed "mdiff_omultiset";
3.546 @@ -1422,9 +1384,9 @@
3.547 by (Clarify_tac 1);
3.548 by (res_inst_tac [("x", "i Un ia")] exI 1);
3.549 by (asm_full_simp_tac (simpset()
3.550 - addsimps [multiset_on_def, Ord_Un, Un_subset_iff]) 1);
3.551 + addsimps [Mult_iff_multiset, Ord_Un, Un_subset_iff]) 1);
3.552 by (rtac munion_multirel_mono2 1);
3.553 -by (asm_simp_tac (simpset() addsimps [multiset_on_def]) 2);
3.554 +by (asm_simp_tac (simpset() addsimps [Mult_iff_multiset]) 2);
3.555 by (blast_tac (claset() addIs [multirel_Memrel_mono RS subsetD]) 1);
3.556 by (blast_tac (claset() addIs [field_Memrel_mono RS subsetD]) 1);
3.557 qed "munion_less_mono2";
3.558 @@ -1434,16 +1396,16 @@
3.559 by (Clarify_tac 1);
3.560 by (res_inst_tac [("x", "i Un ia")] exI 1);
3.561 by (asm_full_simp_tac (simpset()
3.562 - addsimps [multiset_on_def, Ord_Un, Un_subset_iff]) 1);
3.563 + addsimps [Mult_iff_multiset, Ord_Un, Un_subset_iff]) 1);
3.564 by (rtac munion_multirel_mono1 1);
3.565 -by (asm_simp_tac (simpset() addsimps [multiset_on_def]) 2);
3.566 +by (asm_simp_tac (simpset() addsimps [Mult_iff_multiset]) 2);
3.567 by (blast_tac (claset() addIs [multirel_Memrel_mono RS subsetD]) 1);
3.568 by (blast_tac (claset() addIs [field_Memrel_mono RS subsetD]) 1);
3.569 qed "munion_less_mono1";
3.570
3.571 Goalw [mless_def, omultiset_def]
3.572 "M <# N ==> omultiset(M) & omultiset(N)";
3.573 -by (auto_tac (claset() addDs [multirelD], simpset()));
3.574 +by (auto_tac (claset() addDs [multirel_type RS subsetD], simpset()));
3.575 qed "mless_imp_omultiset";
3.576
3.577 Goal "[| M <# K; N <# L |] ==> M +# N <# K +# L";
3.578 @@ -1472,22 +1434,20 @@
3.579 munion_less_mono], simpset()));
3.580 qed "mle_mono";
3.581
3.582 -Goalw [omultiset_def, multiset_on_def] "omultiset(0)";
3.583 -by Auto_tac;
3.584 +Goalw [omultiset_def] "omultiset(0)";
3.585 +by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
3.586 qed "omultiset_0";
3.587 AddIffs [omultiset_0];
3.588
3.589 Goalw [mle_def, mless_def] "omultiset(M) ==> 0 <#= M";
3.590 -by (subgoal_tac "EX i. Ord(i) & multiset[field(Memrel(i))](M)" 1);
3.591 +by (subgoal_tac "EX i. Ord(i) & M:Mult(field(Memrel(i)))" 1);
3.592 by (asm_full_simp_tac (simpset() addsimps [omultiset_def]) 2);
3.593 by (case_tac "M=0" 1);
3.594 by (ALLGOALS(Asm_full_simp_tac));
3.595 by (Clarify_tac 1);
3.596 by (subgoal_tac "<0 +# 0, 0 +# M>: multirel(field(Memrel(i)), Memrel(i))" 1);
3.597 by (rtac one_step_implies_multirel 2);
3.598 -by Auto_tac;
3.599 -by (dres_inst_tac [("x", "i")] spec 1);
3.600 -by (auto_tac (claset(), simpset() addsimps [multiset_on_def]));
3.601 +by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
3.602 qed "empty_leI";
3.603 Addsimps [empty_leI];
3.604
3.605 @@ -1498,11 +1458,5 @@
3.606 qed "munion_upper1";
3.607
3.608
3.609 -Goal "[| omultiset(M); omultiset(N) |] ==> N <#= M +# N";
3.610 -by (stac munion_commute 1);
3.611 -by (rtac munion_upper1 3);
3.612 -by Auto_tac;
3.613 -qed "munion_upper2";
3.614
3.615 -Delsimps [domain_of_fun];
3.616 -AddSEs [domainE];
3.617 +
4.1 --- a/src/ZF/Induct/Multiset.thy Mon Jan 28 23:35:20 2002 +0100
4.2 +++ b/src/ZF/Induct/Multiset.thy Wed Jan 30 12:22:40 2002 +0100
4.3 @@ -9,7 +9,12 @@
4.4 *)
4.5
4.6 Multiset = FoldSet + Acc +
4.7 -
4.8 +consts
4.9 + (* Short cut for multiset space *)
4.10 + Mult :: i=>i
4.11 +translations
4.12 + "Mult(A)" => "A-||>nat-{0}"
4.13 +
4.14 constdefs
4.15 (* M is a multiset *)
4.16 multiset :: i => o
4.17 @@ -18,16 +23,12 @@
4.18 mset_of :: "i=>i"
4.19 "mset_of(M) == domain(M)"
4.20
4.21 - (* M is a multiset over A *)
4.22 - multiset_on :: [i,i]=>o ("multiset[_]'(_')")
4.23 - "multiset[A](M) == multiset(M) & mset_of(M) <= A"
4.24 -
4.25 munion :: "[i, i] => i" (infixl "+#" 65)
4.26 "M +# N == lam x:mset_of(M) Un mset_of(N).
4.27 if x:mset_of(M) Int mset_of(N) then (M`x) #+ (N`x)
4.28 else (if x:mset_of(M) then M`x else N`x)"
4.29
4.30 - (* eliminating zeros from a function *)
4.31 + (* eliminating 0's from a function *)
4.32 normalize :: i => i
4.33 "normalize(M) == restrict(M, {x:mset_of(M). 0<M`x})"
4.34
4.35 @@ -65,17 +66,17 @@
4.36
4.37 multirel1 :: "[i,i]=>i"
4.38 "multirel1(A, r) ==
4.39 - {<M, N> : (A-||>nat-{0})*(A-||>nat-{0}).
4.40 - EX a:A. EX M0:A-||>nat-{0}. EX K:A-||>nat-{0}.
4.41 - N=M0 +# {#a#} & M=M0 +# K & (ALL b:mset_of(K). <b,a>:r)}"
4.42 + {<M, N> : Mult(A)*Mult(A).
4.43 + EX a:A. EX M0:Mult(A). EX K:Mult(A).
4.44 + N=M0 +# {#a#} & M=M0 +# K & (ALL b:mset_of(K). <b,a>:r)}"
4.45
4.46 multirel :: "[i, i] => i"
4.47 "multirel(A, r) == multirel1(A, r)^+"
4.48
4.49 - (* ordinal multisets orderings *)
4.50 + (* ordinal multiset orderings *)
4.51
4.52 omultiset :: i => o
4.53 - "omultiset(M) == EX i. Ord(i) & multiset[field(Memrel(i))](M)"
4.54 + "omultiset(M) == EX i. Ord(i) & M:Mult(field(Memrel(i)))"
4.55
4.56 mless :: [i, i] => o (infixl "<#" 50)
4.57 "M <# N == EX i. Ord(i) & <M, N>:multirel(field(Memrel(i)), Memrel(i))"