# HG changeset patch # User paulson # Date 1012389760 -3600 # Node ID 7fc3fbfed8ef43a80abd0d926b8e61383e13f27d # Parent f63315dfffd42a2da87af02d6c9c036a7d708691 Multiset: added the translation Mult(A) => A-||>nat-{0} (which internalises the `multiset' relation). FoldSet: weakened the typing conditions of the function f and (by the way) removed the `locale' declarations. diff -r f63315dfffd4 -r 7fc3fbfed8ef src/ZF/Induct/FoldSet.ML --- a/src/ZF/Induct/FoldSet.ML Mon Jan 28 23:35:20 2002 +0100 +++ b/src/ZF/Induct/FoldSet.ML Wed Jan 30 12:22:40 2002 +0100 @@ -16,9 +16,6 @@ bind_thm("cons_fold_setE", fold_set.mk_cases " : fold_set(A, B, f,e)"); -bind_thm("fold_set_lhs", fold_set.dom_subset RS subsetD RS SigmaD1); -bind_thm("fold_set_rhs", fold_set.dom_subset RS subsetD RS SigmaD2); - (* add-hoc lemmas *) Goal "[| x~:C; x~:B |] ==> cons(x,B)=cons(x,C) <-> B = C"; @@ -30,53 +27,79 @@ by (auto_tac (claset() addEs [equalityE], simpset())); qed "cons_lemma2"; - -Open_locale "LC"; -val f_lcomm = thm "lcomm"; -val f_type = thm "ftype"; +(* fold_set monotonicity *) +Goal " : fold_set(A, B, f, e) \ +\ ==> ALL D. A<=D --> : fold_set(D, B, f, e)"; +by (etac fold_set.induct 1); +by (auto_tac (claset() addIs fold_set.intrs, simpset())); +qed "fold_set_mono_lemma"; -Goal "[| : fold_set(A, B, f,e); x:C; x:A |] \ -\ ==> : fold_set(A, B, f, e)"; -by (ftac fold_set_rhs 1); +Goal " C<=A ==> fold_set(C, B, f, e) <= fold_set(A, B, f, e)"; +by (Clarify_tac 1); +by (forward_tac [impOfSubs fold_set.dom_subset] 1); +by (Clarify_tac 1); +by (auto_tac (claset() addDs [fold_set_mono_lemma], simpset())); +qed "fold_set_mono"; + +Goal ":fold_set(A, B, f, e) ==> :fold_set(C, B, f, e) & C<=A"; +by (etac fold_set.induct 1); +by (auto_tac (claset() addSIs fold_set.intrs + addIs [fold_set_mono RS subsetD], simpset())); +qed "fold_set_lemma"; + +(* Proving that fold_set is deterministic *) +Goal "[| : fold_set(A, B, f,e); x:C; x:A; f(x, y):B |] \ +\ ==> : fold_set(A, B, f, e)"; +by (ftac (fold_set.dom_subset RS subsetD) 1); by (etac (cons_Diff RS subst) 1 THEN resolve_tac fold_set.intrs 1); -by (auto_tac (claset() addIs [f_type], simpset())); +by Auto_tac; qed "Diff1_fold_set"; -Goal "[| C:Fin(A); e:B |] ==> EX x. : fold_set(A, B, f,e)"; +Goal "[| C:Fin(A); e:B; ALL x:A. ALL y:B. f(x, y):B |] ==>\ +\ (EX x. : fold_set(A, B, f,e))"; by (etac Fin_induct 1); -by (ALLGOALS(Clarify_tac)); -by (ftac fold_set_rhs 2); -by (cut_inst_tac [("x", "x"), ("y", "xa")] f_type 2); -by (REPEAT(blast_tac (claset() addIs fold_set.intrs) 1)); +by Auto_tac; +by (ftac (fold_set.dom_subset RS subsetD) 2); +by (auto_tac (claset() addDs [fold_set.dom_subset RS subsetD] + addIs fold_set.intrs, simpset())); qed_spec_mp "Fin_imp_fold_set"; - -Goal "n:nat \ -\ ==> ALL C x. |C| e:B --> : fold_set(A, B, f,e)-->\ -\ (ALL y. : fold_set(A, B, f,e) --> y=x)"; +Goal +"[| n:nat; e:B; \ +\ ALL x:A. ALL y:B. f(x, y):B; \ +\ ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))=f(y, f(x, z)) |] \ +\ ==> ALL C. |C| \ +\ (ALL x. : fold_set(A, B, f,e)-->\ +\ (ALL y. : fold_set(A, B, f,e) --> y=x))"; by (etac nat_induct 1); by (auto_tac (claset(), simpset() addsimps [le_iff])); +by (Blast_tac 1); by (etac fold_set.elim 1); -by (blast_tac (claset() addEs [empty_fold_setE]) 1); +by (force_tac (claset() addSEs [empty_fold_setE], simpset()) 1); by (etac fold_set.elim 1); -by (blast_tac (claset() addEs [empty_fold_setE]) 1); +by (force_tac (claset() addSEs [empty_fold_setE], simpset()) 1); by (Clarify_tac 1); (*force simplification of "|C| < |cons(...)|"*) -by (rotate_tac 2 1); +by (rotate_tac 4 1); by (etac rev_mp 1); -by (forw_inst_tac [("a", "Ca")] fold_set_lhs 1); -by (forw_inst_tac [("a", "Cb")] fold_set_lhs 1); -by (asm_simp_tac (simpset() addsimps [Fin_into_Finite RS Finite_imp_cardinal_cons]) 1); +by (forw_inst_tac [("a", "Ca")] + (fold_set.dom_subset RS subsetD RS SigmaD1) 1); +by (forw_inst_tac [("a", "Cb")] + (fold_set.dom_subset RS subsetD RS SigmaD1) 1); +by (asm_simp_tac (simpset() addsimps + [Fin_into_Finite RS Finite_imp_cardinal_cons]) 1); by (rtac impI 1); (** LEVEL 10 **) by (case_tac "x=xb" 1 THEN Auto_tac); -by (asm_full_simp_tac (simpset() addsimps [cons_lemma1]) 1); -by (Blast_tac 1); +by (asm_full_simp_tac (simpset() addsimps [cons_lemma1]) 1); +by (REPEAT(thin_tac "ALL x:A. ?u(x)" 1) THEN Blast_tac 1); (*case x ~= xb*) by (dtac cons_lemma2 1 THEN ALLGOALS Clarify_tac); by (subgoal_tac "Ca = cons(xb, Cb) - {x}" 1); -by (blast_tac (claset() addEs [equalityE]) 2); -(** LEVEL 20 **) +by (REPEAT(thin_tac "ALL C. ?P(C)" 2)); +by (REPEAT(thin_tac "ALL x:?u. ?P(x)" 2)); +by (blast_tac (claset() addEs [equalityE]) 2); +(** LEVEL 22 **) by (subgoal_tac "|Ca| le |Cb|" 1); by (rtac succ_le_imp_le 2); by (hyp_subst_tac 2); @@ -84,39 +107,60 @@ by (asm_simp_tac (simpset() addsimps [Finite_imp_succ_cardinal_Diff, Fin_into_Finite RS Finite_imp_cardinal_cons]) 2); by (asm_simp_tac (simpset() addsimps [Fin.consI RS Fin_into_Finite]) 2); -by (res_inst_tac [("C1", "Ca-{xb}"), ("e1","e"), ("A1", "A")] +by (res_inst_tac [("C1", "Ca-{xb}"), ("e1","e"), ("A1", "A"), ("f1", "f")] (Fin_imp_fold_set RS exE) 1); by (blast_tac (claset() addIs [Diff_subset RS Fin_subset]) 1); by (Blast_tac 1); -(** LEVEL 28 **) -by (ftac Diff1_fold_set 1 THEN assume_tac 1 THEN assume_tac 1); +by (blast_tac (claset() addSDs [FinD]) 1); +(** LEVEL 32 **) +by (ftac Diff1_fold_set 1); +by (Blast_tac 1); +by (Blast_tac 1); +by (blast_tac (claset() addSDs [fold_set.dom_subset RS subsetD]) 1); by (subgoal_tac "ya = f(xb, xa)" 1); +by (dres_inst_tac [("x", "Ca")] spec 2); by (blast_tac (claset() delrules [equalityCE]) 2); by (subgoal_tac ": fold_set(A, B, f, e)" 1); - by (Asm_full_simp_tac 2); +by (Asm_full_simp_tac 2); by (subgoal_tac "yb = f(x, xa)" 1); - by (blast_tac (claset() delrules [equalityCE] - addDs [Diff1_fold_set]) 2); -by (asm_simp_tac (simpset() addsimps [f_lcomm]) 1); -qed_spec_mp "lemma"; +by (dres_inst_tac [("C", "Cb")] Diff1_fold_set 2); +by (ALLGOALS(Asm_simp_tac)); +by (force_tac (claset() addSDs [fold_set.dom_subset RS subsetD], simpset()) 2); +by (force_tac (claset() addSDs [fold_set.dom_subset RS subsetD], simpset()) 1); +by (dres_inst_tac [("x", "Cb")] spec 1); +by Auto_tac; +qed_spec_mp "fold_set_determ_lemma"; - -Goal "[| : fold_set(A, B, f, e); \ -\ : fold_set(A, B, f, e); e:B |] ==> y=x"; -by (forward_tac [fold_set_lhs RS Fin_into_Finite] 1); +Goal +"[| :fold_set(A, B, f, e); \ +\ :fold_set(A, B, f, e); e:B; \ +\ ALL x:A. ALL y:B. f(x, y):B; \ +\ ALL x:A. ALL y:A. ALL z:B. f(x,f(y, z))=f(y, f(x, z)) |]\ +\ ==> y=x"; +by (forward_tac [fold_set.dom_subset RS subsetD] 1); +by (Clarify_tac 1); +by (dtac Fin_into_Finite 1); by (rewtac Finite_def); by (Clarify_tac 1); -by (res_inst_tac [("n", "succ(n)")] lemma 1); -by (auto_tac (claset() addIs - [eqpoll_imp_lepoll RS lepoll_cardinal_le], - simpset())); +by (res_inst_tac [("n", "succ(n)"), ("e", "e"), ("A", "A"), + ("f", "f"), ("B", "B")] fold_set_determ_lemma 1); +by (auto_tac (claset() addIs [eqpoll_imp_lepoll RS + lepoll_cardinal_le], simpset())); qed "fold_set_determ"; +(** The fold function **) + Goalw [fold_def] - "[| : fold_set(C, B, f, e); e:B |] ==> fold[B](f,e,C) = y"; +"[| :fold_set(A, B, f, e); e:B; \ +\ ALL x:A. ALL y:B. f(x, y):B; \ +\ ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))=f(y, f(x, z)) |] \ +\ ==> fold[B](f, e, C) = y"; +by (forward_tac [fold_set.dom_subset RS subsetD] 1); +by (Clarify_tac 1); by (rtac the_equality 1); -by (rtac fold_set_determ 2); -by Auto_tac; +by (res_inst_tac [("f", "f"), ("e", "e"), ("B", "B")] fold_set_determ 2); +by (auto_tac (claset() addDs [fold_set_lemma], simpset())); +by (blast_tac (claset() addSDs [FinD]) 1); qed "fold_equality"; Goalw [fold_def] "e:B ==> fold[B](f,e,0) = e"; @@ -125,75 +169,78 @@ qed "fold_0"; Addsimps [fold_0]; -Goal "[| x ~: C; x:A; e:B |] \ -\ ==> : fold_set(A, B, f, e) <-> \ -\ (EX y. : fold_set(A, B, f, e) & v = f(x, y))"; +Goal +"[| C:Fin(A); c:A; c~:C; e:B; ALL x:A. ALL y:B. f(x, y):B; \ +\ ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))=f(y, f(x,z)) |] \ +\ ==> : fold_set(cons(c, C), B, f, e) <-> \ +\ (EX y. : fold_set(C, B, f, e) & v = f(c, y))"; by Auto_tac; -by (res_inst_tac [("A1", "A"), ("C1", "C")] (Fin_imp_fold_set RS exE) 1); -by (res_inst_tac [("x", "xa")] exI 3); -by (res_inst_tac [("b", "cons(x, C)")] Fin_subset 1); -by (auto_tac (claset() addDs [fold_set_lhs] - addIs [f_type]@fold_set.intrs, simpset())); -by (blast_tac (claset() addIs [fold_set_determ, f_type]@fold_set.intrs) 1); -val lemma = result(); - -Goal " : fold_set(C, B, f, e) \ -\ ==> ALL A. C<=A --> : fold_set(A, B, f, e)"; -by (etac fold_set.induct 1); +by (forward_tac [inst "a" "c" Fin.consI RS FinD RS fold_set_mono RS subsetD] 1); +by (assume_tac 1); +by (assume_tac 1); +by (forward_tac [FinD RS fold_set_mono RS subsetD] 2); +by (assume_tac 2); +by (ALLGOALS(forward_tac [inst "A" "A" fold_set.dom_subset RS subsetD])); +by (ALLGOALS(dresolve_tac [FinD])); +by (res_inst_tac [("A1", "cons(c, C)"), ("f1", "f"), + ("B1", "B"), ("C1", "C")] (Fin_imp_fold_set RS exE) 1); +by (res_inst_tac [("b", "cons(c, C)")] Fin_subset 1); +by (resolve_tac [Finite_into_Fin] 2); +by (resolve_tac [Fin_into_Finite] 2); +by (Blast_tac 2); +by (res_inst_tac [("x", "x")] exI 4); by (auto_tac (claset() addIs fold_set.intrs, simpset())); -qed "lemma2"; - -Goal " C<=A ==> fold_set(C, B, f, e) <= fold_set(A, B, f, e)"; -by (Clarify_tac 1); -by (forward_tac [impOfSubs fold_set.dom_subset] 1); -by (Clarify_tac 1); -by (auto_tac (claset() addDs [lemma2], simpset())); -qed "fold_set_mono"; - -Goal " : fold_set(A, B, f, e) ==> : fold_set(C,B, f,e)"; -by (etac fold_set.induct 1); -by (auto_tac (claset() addSIs fold_set.intrs, simpset())); -by (res_inst_tac [("C1", "C"), ("A1", "cons(x, C)")] - (fold_set_mono RS subsetD) 1); +by (dresolve_tac [inst "C" "C" fold_set_lemma] 1); +by (Blast_tac 1); +by (resolve_tac fold_set.intrs 2); by Auto_tac; -qed "fold_set_mono2"; - +by (blast_tac (claset() addIs [fold_set_mono RS subsetD]) 2); +by (resolve_tac [fold_set_determ] 1); +by (assume_tac 5); +by Auto_tac; +by (resolve_tac fold_set.intrs 1); +by Auto_tac; +by (blast_tac (claset() addIs [fold_set_mono RS subsetD]) 1); +by (blast_tac (claset() addDs [fold_set.dom_subset RS subsetD]) 1); +qed_spec_mp "fold_cons_lemma"; Goalw [fold_def] - "[| Finite(C); x ~: C; e:B |] \ -\ ==> fold[B](f, e, cons(x, C)) = f(x, fold[B](f,e, C))"; -by (asm_simp_tac (simpset() addsimps [lemma]) 1); -by (dtac Finite_into_Fin 1); +"[| C:Fin(A); c:A; c~:C; e:B; \ +\ (ALL x:A. ALL y:B. f(x, y):B); \ +\ (ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))=f(y, f(x, z))) |]\ +\ ==> fold[B](f, e, cons(c, C)) = f(c, fold[B](f, e, C))"; +by (asm_simp_tac (simpset() addsimps [fold_cons_lemma]) 1); by (rtac the_equality 1); -by (dtac Fin_imp_fold_set 1); +by (dres_inst_tac [("e", "e"), ("f", "f")] Fin_imp_fold_set 1); by Auto_tac; -by (res_inst_tac [("x", "xa")] exI 1); +by (res_inst_tac [("x", "x")] exI 1); by Auto_tac; -by (resolve_tac [fold_set_mono RS subsetD] 1); -by (Blast_tac 2); -by (dtac fold_set_mono2 3); -by (auto_tac (claset() addIs [Fin_imp_fold_set], - simpset() addsimps [symmetric fold_def, fold_equality])); +by (blast_tac (claset() addDs [fold_set_lemma]) 1); +by (ALLGOALS(dtac fold_equality)); +by (auto_tac (claset(), simpset() addsimps [symmetric fold_def])); +by (REPEAT(blast_tac (claset() addDs [FinD]) 1)); qed "fold_cons"; +Goal +"[| C:Fin(A); e:B; \ +\ (ALL x:A. ALL y:B. f(x, y):B); \ +\ (ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))=f(y, f(x, z))) |] ==> \ +\ fold[B](f, e,C):B"; +by (etac Fin_induct 1); +by (ALLGOALS(asm_simp_tac (simpset() addsimps [fold_cons]))); +qed_spec_mp "fold_type"; +AddTCs [fold_type]; +Addsimps [fold_type]; -Goal "Finite(C) \ -\ ==> ALL e:B. f(x, fold[B](f, e, C)) = fold[B](f, f(x, e), C)"; -by (etac Finite_induct 1); -by (ALLGOALS(Clarify_tac)); -by (asm_full_simp_tac (simpset() addsimps [f_type]) 1); -by (asm_simp_tac (simpset() - addsimps [f_lcomm, fold_cons, f_type]) 1); +Goal +"[| C:Fin(A); c:A; \ +\ ALL x:A. ALL y:B. f(x, y):B; \ +\ ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))=f(y, f(x, z)) |] \ +\ ==> (ALL y:B. f(c, fold[B](f, y, C)) = fold[B](f, f(c, y), C))"; +by (etac Fin_induct 1); +by (ALLGOALS(asm_simp_tac (simpset() addsimps [fold_cons]))); qed_spec_mp "fold_commute"; - -Goal "Finite(C) ==> e:B -->fold[B](f, e, C):B"; -by (etac Finite_induct 1); -by (ALLGOALS(Clarify_tac)); -by (Asm_simp_tac 1); -by (asm_simp_tac (simpset() addsimps [fold_cons, f_type]) 1); -qed_spec_mp "fold_type"; - Goal "x:D ==> cons(x, C) Int D = cons(x, C Int D)"; by Auto_tac; qed "cons_Int_right_lemma1"; @@ -202,30 +249,36 @@ by Auto_tac; qed "cons_Int_right_lemma2"; -Goal "[| Finite(C); Finite(D); e:B|] \ -\ ==> fold[B](f, fold[B](f, e, D), C) \ +Goal +"[| C:Fin(A); D:Fin(A); e:B; \ +\ ALL x:A. ALL y:B. f(x, y):B; \ +\ ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))=f(y, f(x, z)) |] \ +\ ==> \ +\ fold[B](f, fold[B](f, e, D), C) \ \ = fold[B](f, fold[B](f, e, (C Int D)), C Un D)"; -by (etac Finite_induct 1); -by (asm_full_simp_tac (simpset() addsimps [f_type, fold_type]) 1); -by (subgoal_tac "Finite(Ba Int D) & \ - \cons(x, Ba) Un D = cons(x, Ba Un D) & \ - \Finite(Ba Un D)" 1); -by (auto_tac (claset() - addIs [Finite_Un,Int_lower1 RS subset_Finite], simpset())); +by (etac Fin_induct 1); +by Auto_tac; +by (subgoal_tac "cons(x, y) Un D = cons(x, y Un D)" 1); +by Auto_tac; +by (subgoal_tac "y Int D:Fin(A) & y Un D:Fin(A)" 1); +by (Clarify_tac 1); by (case_tac "x:D" 1); by (ALLGOALS(asm_simp_tac (simpset() addsimps [cons_Int_right_lemma1,cons_Int_right_lemma2, - fold_type, fold_cons,fold_commute,cons_absorb, f_type]))); + fold_cons, fold_commute,cons_absorb]))); qed "fold_nest_Un_Int"; - -Goal "[| Finite(C); Finite(D); C Int D = 0; e:B |] \ +Goal "[| C:Fin(A); D:Fin(A); C Int D = 0; e:B; \ +\ ALL x:A. ALL y:B. f(x, y):B; \ +\ ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))=f(y, f(x, z)) |] \ \ ==> fold[B](f,e,C Un D) = fold[B](f, fold[B](f,e,D), C)"; by (asm_simp_tac (simpset() addsimps [fold_nest_Un_Int]) 1); qed "fold_nest_Un_disjoint"; -Close_locale "LC"; - +Goal "Finite(C) ==> C:Fin(cons(c, C))"; +by (dtac Finite_into_Fin 1); +by (blast_tac (claset() addIs [Fin_mono RS subsetD]) 1); +qed "Finite_cons_lemma"; (** setsum **) @@ -237,7 +290,9 @@ Goalw [setsum_def] "[| Finite(C); c~:C |] \ \ ==> setsum(g, cons(c, C)) = g(c) $+ setsum(g, C)"; -by (asm_simp_tac (simpset() addsimps [Finite_cons,export fold_cons]) 1); +by (auto_tac (claset(), simpset() addsimps [Finite_cons])); +by (res_inst_tac [("A", "cons(c, C)")] fold_cons 1); +by (auto_tac (claset() addIs [Finite_cons_lemma], simpset())); qed "setsum_cons"; Addsimps [setsum_cons]; @@ -341,8 +396,6 @@ by (asm_full_simp_tac (simpset() addsimps [Ball_def, major]@prems) 1); qed_spec_mp "setsum_cong"; -(** For the natural numbers, we have subtraction **) - Goal "[| Finite(A); Finite(B) |] \ \ ==> setsum(f, A Un B) = \ \ setsum(f, A) $+ setsum(f, B) $- setsum(f, A Int B)"; diff -r f63315dfffd4 -r 7fc3fbfed8ef src/ZF/Induct/FoldSet.thy --- a/src/ZF/Induct/FoldSet.thy Mon Jan 28 23:35:20 2002 +0100 +++ b/src/ZF/Induct/FoldSet.thy Wed Jan 30 12:22:40 2002 +0100 @@ -23,16 +23,9 @@ constdefs fold :: "[i, [i,i]=>i, i, i] => i" ("fold[_]'(_,_,_')") - "fold[B](f,e,C) == THE x. :fold_set(C, B, f,e)" + "fold[B](f,e, A) == THE x. :fold_set(A, B, f,e)" setsum :: "[i=>i, i] => i" "setsum(g, C) == if Finite(C) then fold[int](%x y. g(x) $+ y, #0, C) else #0" -locale LC = - fixes - B :: i - f :: [i,i] => i - assumes - ftype "f(x,y):B" - lcomm "f(x, f(y, z)) = f(y,f(x, z))" end \ No newline at end of file diff -r f63315dfffd4 -r 7fc3fbfed8ef src/ZF/Induct/Multiset.ML --- a/src/ZF/Induct/Multiset.ML Mon Jan 28 23:35:20 2002 +0100 +++ b/src/ZF/Induct/Multiset.ML Wed Jan 30 12:22:40 2002 +0100 @@ -29,37 +29,46 @@ simpset() addsimps [range_of_fun, apply_iff])); qed "multiset_fun_iff"; -(** multiset and multiset_on **) - -Goalw [multiset_on_def, multiset_def] -"multiset[A](M) ==> multiset(M)"; -by Auto_tac; -qed "multiset_on_imp_multiset"; +(** The multiset space **) +Goalw [multiset_def] + "[| multiset(M); mset_of(M)<=A |] ==> M:Mult(A)"; +by (auto_tac (claset(), simpset() + addsimps [multiset_fun_iff, mset_of_def])); +by (rotate_simp_tac "M:?u" 1); +by (res_inst_tac [("B1","nat-{0}")] (FiniteFun_mono RS subsetD) 1); +by (ALLGOALS(Asm_simp_tac)); +by (rtac (Finite_into_Fin RSN (2, Fin_mono RS subsetD) RS fun_FiniteFunI) 1); +by (ALLGOALS(asm_simp_tac (simpset() addsimps [multiset_fun_iff]))); +qed "multiset_into_Mult"; -Goalw [multiset_on_def, multiset_def] -"multiset(M) ==> multiset[mset_of(M)](M)"; -by Auto_tac; -qed "multiset_imp_multiset_on_set_of"; +Goalw [multiset_def, mset_of_def] + "M:Mult(A) ==> multiset(M) & mset_of(M)<=A"; +by (ftac FiniteFun_is_fun 1); +by (dtac FiniteFun_domain_Fin 1); +by (ftac FinD 1); +by (Clarify_tac 1); +by (res_inst_tac [("x", "domain(M)")] exI 1); +by (blast_tac (claset() addIs [Fin_into_Finite]) 1); +qed "Mult_into_multiset"; -Goal "multiset(M) <-> multiset[mset_of(M)](M)"; -by (blast_tac (claset() addIs [multiset_on_imp_multiset, - multiset_imp_multiset_on_set_of]) 1); -qed "multiset_iff_multiset_on_set_of"; +Goal "M:Mult(A) <-> multiset(M) & mset_of(M)<=A"; +by (blast_tac (claset() addDs [Mult_into_multiset] + addIs [multiset_into_Mult]) 1); +qed "Mult_iff_multiset"; -Goalw [multiset_on_def] - "[| A<= B; multiset[A](M) |] ==> multiset[B](M)"; -by Auto_tac; -qed "subset_multiset_on"; +Goal "multiset(M) <-> M:Mult(mset_of(M))"; +by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset])); +qed "multiset_iff_Mult_mset_of"; + +(** multiset **) (* the empty multiset is 0 *) -Goalw [multiset_def, mset_of_def] - "multiset(0)"; -by Auto_tac; -by (res_inst_tac [("x", "0")] exI 1); -by (simp_tac (simpset() addsimps [Finite_0]) 1); +Goal "multiset(0)"; +by (auto_tac (claset() addIs FiniteFun.intrs, + simpset() addsimps [multiset_iff_Mult_mset_of])); qed "multiset_0"; -AddIffs [multiset_0]; +Addsimps [multiset_0]; (** mset_of **) @@ -151,7 +160,7 @@ qed "normalize_multiset"; Addsimps [normalize_multiset]; -Goalw [multiset_def, multiset_on_def] +Goalw [multiset_def] "[| f:A -> nat; Finite(A) |] ==> multiset(normalize(f))"; by (rewrite_goals_tac [normalize_def, mset_of_def]); by Auto_tac; @@ -261,13 +270,13 @@ by (rewrite_goals_tac [mcount_def, mset_of_def]); by (auto_tac (claset(), simpset() addsimps [multiset_fun_iff])); qed "mcount_type"; -AddIs [mcount_type]; +AddTCs [mcount_type]; Addsimps [mcount_type]; Goalw [mcount_def] "mcount(0, a) = 0"; by Auto_tac; qed "mcount_0"; -AddIffs [mcount_0]; +Addsimps [mcount_0]; Goalw [mcount_def, mset_of_def, msingle_def] "mcount({#b#}, a) = (if a=b then 1 else 0)"; @@ -319,8 +328,6 @@ qed "msize_type"; Addsimps [msize_type]; AddTCs [msize_type]; -AddIs [msize_type]; - Goalw [msize_def] "multiset(M)==> #0 $<= msize(M)"; by (auto_tac (claset() addIs [g_zpos_imp_setsum_zpos], simpset())); @@ -751,94 +758,61 @@ by Auto_tac; qed "munion_eq_conv_diff"; -Goalw [multiset_on_def] -"[| multiset[A](M); multiset[A](N) |] \ +Goal +"[| M:Mult(A); N:Mult(A) |] \ \ ==> (M +# {#a#} = N +# {#b#}) <-> \ -\ (M=N & a=b | (EX K. multiset[A](K)& M= K +# {#b#} & N=K +# {#a#}))"; +\ (M=N & a=b | (EX K:Mult(A). M= K +# {#b#} & N=K +# {#a#}))"; by (auto_tac (claset(), - simpset() addsimps [melem_diff_single, munion_eq_conv_diff])); + simpset() addsimps [Bex_def, Mult_iff_multiset, + melem_diff_single, munion_eq_conv_diff])); qed "munion_eq_conv_exist"; (** multiset orderings **) (* multiset on a domain A are finite functions from A to nat-{0} *) -Goalw [multiset_on_def, multiset_def] - "multiset[A](M) ==> M:A-||>nat-{0}"; -by (auto_tac (claset(), simpset() - addsimps [multiset_fun_iff, mset_of_def])); -by (rotate_simp_tac "M:?u" 1); -by (res_inst_tac [("B1","nat-{0}")] (FiniteFun_mono RS subsetD) 1); -by (ALLGOALS(Asm_simp_tac)); -by (rtac (Finite_into_Fin RSN (2, Fin_mono RS subsetD) RS fun_FiniteFunI) 1); -by (ALLGOALS(asm_simp_tac (simpset() addsimps [multiset_fun_iff]))); -qed "multiset_on_is_FiniteFun"; - -Goalw [multiset_on_def, multiset_def, mset_of_def] - "M:A-||>nat-{0} ==> multiset[A](M)"; -by (ftac FiniteFun_is_fun 1); -by (dtac FiniteFun_domain_Fin 1); -by (ftac FinD 1); -by (Clarify_tac 1); -by (res_inst_tac [("x", "domain(M)")] exI 1); -by (blast_tac (claset() addIs [Fin_into_Finite]) 1); -qed "FiniteFun_is_multiset_on"; - -Goal "M:A-||>nat-{0} <-> multiset[A](M)"; -by (blast_tac (claset() addDs [FiniteFun_is_multiset_on] - addIs [multiset_on_is_FiniteFun]) 1); -qed "FiniteFun_iff_multiset_on"; (* multirel1 type *) Goalw [multirel1_def] -"multirel1(A, r) <= (A-||>nat-{0})*(A-||>nat-{0})"; +"multirel1(A, r) <= Mult(A)*Mult(A)"; by Auto_tac; qed "multirel1_type"; -Goal ":multirel1(A, r) ==> multiset[A](M) & multiset[A](N)"; -by (dtac (multirel1_type RS subsetD) 1); -by (asm_full_simp_tac (simpset() addsimps [FiniteFun_iff_multiset_on]) 1); -qed "multirel1D"; - Goalw [multirel1_def] "multirel1(0, r) =0"; by Auto_tac; qed "multirel1_0"; AddIffs [multirel1_0]; -Goalw [multirel1_def, Ball_def, Bex_def] +Goalw [multirel1_def] " :multirel1(A, r) <-> \ -\ (EX a. a:A & \ -\ (EX M0. multiset[A](M0) & (EX K. multiset[A](K) & \ +\ (EX a. a:A & \ +\ (EX M0. M0:Mult(A) & (EX K. K:Mult(A) & \ \ M=M0 +# {#a#} & N=M0 +# K & (ALL b:mset_of(K). :r))))"; -by (auto_tac (claset(), simpset() - addsimps [FiniteFun_iff_multiset_on, multiset_on_def])); +by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset, Ball_def, Bex_def])); qed "multirel1_iff"; (* Monotonicity of multirel1 *) Goalw [multirel1_def] "A<=B ==> multirel1(A, r)<=multirel1(B, r)"; -by (auto_tac (claset(), simpset() addsimps [FiniteFun_iff_multiset_on])); +by (auto_tac (claset(), simpset() addsimps [])); by (ALLGOALS(asm_full_simp_tac(simpset() - addsimps [Un_subset_iff, multiset_on_def]))); + addsimps [Un_subset_iff, Mult_iff_multiset]))); by (res_inst_tac [("x", "x")] bexI 3); by (res_inst_tac [("x", "xb")] bexI 3); by (Asm_simp_tac 3); by (res_inst_tac [("x", "K")] bexI 3); -by (ALLGOALS(asm_simp_tac (simpset() - addsimps [FiniteFun_iff_multiset_on, multiset_on_def]))); +by (ALLGOALS(asm_simp_tac (simpset() addsimps [Mult_iff_multiset]))); by Auto_tac; qed "multirel1_mono1"; Goalw [multirel1_def] "r<=s ==> multirel1(A,r)<=multirel1(A, s)"; -by (auto_tac (claset(), simpset() addsimps [FiniteFun_iff_multiset_on])); +by (auto_tac (claset(), simpset() addsimps [])); by (res_inst_tac [("x", "x")] bexI 1); by (res_inst_tac [("x", "xb")] bexI 1); -by (ALLGOALS(asm_full_simp_tac (simpset() - addsimps [FiniteFun_iff_multiset_on, multiset_on_def]))); +by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [Mult_iff_multiset]))); by (res_inst_tac [("x", "K")] bexI 1); -by (ALLGOALS(asm_full_simp_tac (simpset() - addsimps [FiniteFun_iff_multiset_on,multiset_on_def]))); +by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [Mult_iff_multiset]))); by Auto_tac; qed "multirel1_mono2"; @@ -853,27 +827,26 @@ (* Towards the proof of well-foundedness of multirel1 *) Goalw [multirel1_def] "~:multirel1(A, r)"; -by (auto_tac (claset(), simpset() - addsimps [FiniteFun_iff_multiset_on, multiset_on_def])); +by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset])); qed "not_less_0"; AddIffs [not_less_0]; -Goal "[| :multirel1(A, r); multiset[A](M0) |] ==> \ +Goal "[| :multirel1(A, r); M0:Mult(A) |] ==> \ \ (EX M. :multirel1(A, r) & N = M +# {#a#}) | \ -\ (EX K. multiset[A](K) & (ALL b:mset_of(K). :r) & N = M0 +# K)"; -by (ftac multirel1D 1); +\ (EX K. K:Mult(A) & (ALL b:mset_of(K). :r) & N = M0 +# K)"; +by (forward_tac [multirel1_type RS subsetD] 1); by (asm_full_simp_tac (simpset() addsimps [multirel1_iff]) 1); by (auto_tac (claset(), simpset() addsimps [munion_eq_conv_exist])); by (ALLGOALS(res_inst_tac [("x", "Ka +# K")] exI)); by Auto_tac; -by (rewtac multiset_on_def); +by (rewtac (Mult_iff_multiset RS iff_reflection)); by (asm_simp_tac (simpset() addsimps [munion_left_cancel, munion_assoc]) 1); by (auto_tac (claset(), simpset() addsimps [munion_commute])); qed "less_munion"; -Goal "[| multiset[A](M); a:A |] ==> : multirel1(A, r)"; +Goal "[| M:Mult(A); a:A |] ==> : multirel1(A, r)"; by (auto_tac (claset(), simpset() addsimps [multirel1_iff])); -by (rewtac multiset_on_def); +by (rewrite_goals_tac [Mult_iff_multiset RS iff_reflection]); by (res_inst_tac [("x", "a")] exI 1); by (Clarify_tac 1); by (res_inst_tac [("x", "M")] exI 1); @@ -892,15 +865,15 @@ \ M0:acc(multirel1(A, r)); a:A; \ \ ALL M. : multirel1(A, r) --> M +# {#a#} : acc(multirel1(A, r)) |] \ \ ==> M0 +# {#a#} : acc(multirel1(A, r))"; -by (subgoal_tac "multiset[A](M0)" 1); +by (subgoal_tac "M0:Mult(A)" 1); by (etac (thm "acc.cases") 2); by (etac fieldE 2); -by (REPEAT(blast_tac (claset() addDs [multirel1D]) 2)); +by (REPEAT(blast_tac (claset() addDs [multirel1_type RS subsetD]) 2)); by (rtac (thm "accI") 1); by (rename_tac "N" 1); by (dtac less_munion 1); by (Blast_tac 1); -by (auto_tac (claset(), simpset() addsimps [multiset_on_def])); +by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset])); by (eres_inst_tac [("P", "ALL x:mset_of(K). :r")] rev_mp 1); by (eres_inst_tac [("P", "mset_of(K)<=A")] rev_mp 1); by (eres_inst_tac [("M", "K")] multiset_induct 1); @@ -920,7 +893,7 @@ by (asm_full_simp_tac (simpset() addsimps [munion_assoc RS sym]) 1); (* subgoal 3: additional conditions *) by (auto_tac (claset() addSIs [multirel1_base RS fieldI2], - simpset() addsimps [multiset_on_def])); + simpset() addsimps [Mult_iff_multiset])); qed "lemma1"; Goal "[| ALL b:A. :r \ @@ -955,15 +928,15 @@ by (Blast_tac 1); by (subgoal_tac "M:field(multirel1(A,r))" 1); by (rtac (multirel1_base RS fieldI1) 2); -by (rewrite_goal_tac [multiset_on_def] 2); +by (rewrite_goal_tac [Mult_iff_multiset RS iff_reflection] 2); by (REPEAT(Blast_tac 1)); qed "lemma4"; -Goal "[| wf[A](r); multiset[A](M); A ~= 0|] ==> M:acc(multirel1(A, r))"; +Goal "[| wf[A](r); M:Mult(A); A ~= 0|] ==> M:acc(multirel1(A, r))"; by (etac not_emptyE 1); by (rtac (lemma4 RS mp RS mp RS mp) 1); by (rtac (multirel1_base RS fieldI1) 4); -by (auto_tac (claset(), simpset() addsimps [multiset_on_def])); +by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset])); qed "all_accessible"; Goal "wf[A](r) ==> wf[A-||>nat-{0}](multirel1(A, r))"; @@ -975,7 +948,7 @@ by (res_inst_tac [("A", "acc(multirel1(A,r))")] wf_on_subset_A 1); by (rtac (thm "wf_on_acc") 1); by (Clarify_tac 1); -by (full_simp_tac (simpset() addsimps [FiniteFun_iff_multiset_on]) 1); +by (full_simp_tac (simpset() addsimps []) 1); by (blast_tac (claset() addIs [all_accessible]) 1); qed "wf_on_multirel1"; @@ -991,21 +964,14 @@ (** multirel **) Goalw [multirel_def] - "multirel(A, r) <= (A-||>nat-{0}) * (A-||>nat-{0})"; + "multirel(A, r) <= Mult(A)*Mult(A)"; by (rtac (trancl_type RS subset_trans) 1); by (Clarify_tac 1); -by (auto_tac (claset() addDs [multirel1D], - simpset() addsimps [FiniteFun_iff_multiset_on])); +by (auto_tac (claset() addDs [multirel1_type RS subsetD], + simpset() addsimps [])); qed "multirel_type"; -Goal ":multirel(A, r) ==> multiset[A](M) & multiset[A](N)"; -by (dtac (multirel_type RS subsetD) 1); -by (asm_simp_tac (simpset() addsimps [FiniteFun_iff_multiset_on RS iff_sym]) 1); -by Auto_tac; -qed "multirelD"; - (* Monotonicity of multirel *) - Goalw [multirel_def] "[| A<=B; r<=s |] ==> multirel(A, r)<=multirel(B,s)"; by (rtac trancl_mono 1); @@ -1041,12 +1007,12 @@ ":multirel(A, r) ==> \ \ trans[A](r) --> \ \ (EX I J K. \ -\ multiset[A](I) & multiset[A](J) & multiset[A](K) & \ +\ I:Mult(A) & J:Mult(A) & K:Mult(A) & \ \ N = I +# J & M = I +# K & J ~= 0 & \ \ (ALL k:mset_of(K). EX j:mset_of(J). :r))"; by (etac converse_trancl_induct 1); by (ALLGOALS(asm_full_simp_tac (simpset() - addsimps [multirel1_iff, multiset_on_def]))); + addsimps [multirel1_iff, Mult_iff_multiset]))); by (ALLGOALS(Clarify_tac)); (* Two subgoals remain *) (* Subgoal 1 *) @@ -1103,23 +1069,23 @@ qed "melem_imp_eq_diff_union"; Addsimps [melem_imp_eq_diff_union]; -Goal "[| msize(M)=$# succ(n); multiset[A](M); n:nat |] \ -\ ==> EX a N. M = N +# {#a#} & multiset[A](N) & a:A"; +Goal "[| msize(M)=$# succ(n); M:Mult(A); n:nat |] \ +\ ==> EX a N. M = N +# {#a#} & N:Mult(A) & a:A"; by (dtac msize_eq_succ_imp_elem 1); by Auto_tac; by (res_inst_tac [("x", "a")] exI 1); by (res_inst_tac [("x", "M -# {#a#}")] exI 1); -by (ftac multiset_on_imp_multiset 1); +by (ftac Mult_into_multiset 1); by (Asm_simp_tac 1); -by (auto_tac (claset(), simpset() addsimps [multiset_on_def])); +by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset])); qed "msize_eq_succ_imp_eq_union"; (* The second direction *) -Goalw [multiset_on_def] +Goalw [Mult_iff_multiset RS iff_reflection] "n:nat ==> \ \ (ALL I J K. \ -\ multiset[A](I) & multiset[A](J) & multiset[A](K) & \ +\ I:Mult(A) & J:Mult(A) & K:Mult(A) & \ \ (msize(J) = $# n & J ~=0 & (ALL k:mset_of(K). EX j:mset_of(J). :r)) \ \ --> :multirel(A, r))"; by (etac nat_induct 1); @@ -1130,7 +1096,7 @@ by (subgoal_tac "msize(J)=$# succ(x)" 1); by (Asm_simp_tac 2); by (forw_inst_tac [("A", "A")] msize_eq_succ_imp_eq_union 1); -by (rewtac multiset_on_def); +by (rewtac (Mult_iff_multiset RS iff_reflection)); by (Clarify_tac 3 THEN rotate_tac ~1 3); by (ALLGOALS(Asm_full_simp_tac)); by (rename_tac "J'" 1); @@ -1139,7 +1105,7 @@ by (asm_full_simp_tac (simpset() addsimps [multirel_def]) 1); by (rtac r_into_trancl 1); by (Clarify_tac 1); -by (asm_full_simp_tac (simpset() addsimps [multirel1_iff, multiset_on_def]) 1); +by (asm_full_simp_tac (simpset() addsimps [multirel1_iff, Mult_iff_multiset]) 1); by (Force_tac 1); (*Now we know J' ~= 0*) by (rotate_simp_tac "multiset(J')" 1); @@ -1165,7 +1131,7 @@ by (res_inst_tac [("b", "I +# {# x:K. :r#} +# J'")] trancl_trans 1); by (Blast_tac 1); by (rtac r_into_trancl 1); -by (asm_full_simp_tac (simpset() addsimps [multirel1_iff, multiset_on_def]) 1); +by (asm_full_simp_tac (simpset() addsimps [multirel1_iff, Mult_iff_multiset]) 1); by (res_inst_tac [("x", "a")] exI 1); by (Asm_simp_tac 1); by (res_inst_tac [("x", "I +# J'")] exI 1); @@ -1177,10 +1143,10 @@ qed_spec_mp "one_step_implies_multirel_lemma"; Goal "[| J ~= 0; ALL k:mset_of(K). EX j:mset_of(J). :r;\ -\ multiset[A](I); multiset[A](J); multiset[A](K) |] \ +\ I:Mult(A); J:Mult(A); K:Mult(A) |] \ \ ==> : multirel(A, r)"; by (subgoal_tac "multiset(J)" 1); -by (asm_full_simp_tac (simpset() addsimps [multiset_on_def]) 2); +by (asm_full_simp_tac (simpset() addsimps [Mult_iff_multiset]) 2); by (forw_inst_tac [("M", "J")] msize_int_of_nat 1); by (auto_tac (claset() addIs [one_step_implies_multirel_lemma], simpset())); qed "one_step_implies_multirel"; @@ -1201,14 +1167,14 @@ qed "multirel_irrefl_lemma"; Goalw [irrefl_def] -"part_ord(A, r) ==> irrefl(A-||>nat-{0}, multirel(A, r))"; +"part_ord(A, r) ==> irrefl(Mult(A), multirel(A, r))"; by (subgoal_tac "trans[A](r)" 1); by (asm_full_simp_tac (simpset() addsimps [part_ord_def]) 2); by (Clarify_tac 1); -by (asm_full_simp_tac (simpset() addsimps [FiniteFun_iff_multiset_on]) 1); +by (asm_full_simp_tac (simpset() addsimps []) 1); by (dtac multirel_implies_one_step 1); by (Clarify_tac 1); -by (rewrite_goal_tac [multiset_on_def] 1); +by (rewrite_goal_tac [Mult_iff_multiset RS iff_reflection] 1); by (Asm_full_simp_tac 1); by (Clarify_tac 1); by (subgoal_tac "Finite(mset_of(K))" 1); @@ -1219,8 +1185,7 @@ by (rotate_simp_tac "K:?u" 1); qed "irrefl_on_multirel"; -Goalw [multirel_def, trans_on_def] -"trans[A-||>nat-{0}](multirel(A, r))"; +Goalw [multirel_def, trans_on_def] "trans[Mult(A)](multirel(A, r))"; by (blast_tac (claset() addIs [trancl_trans]) 1); qed "trans_on_multirel"; @@ -1233,7 +1198,7 @@ by (rtac trans_trancl 1); qed "trans_multirel"; -Goal "part_ord(A,r) ==> part_ord(A-||>nat-{0}, multirel(A, r))"; +Goal "part_ord(A,r) ==> part_ord(Mult(A), multirel(A, r))"; by (simp_tac (simpset() addsimps [part_ord_def]) 1); by (blast_tac (claset() addIs [irrefl_on_multirel, trans_on_multirel]) 1); qed "part_ord_multirel"; @@ -1241,9 +1206,9 @@ (** Monotonicity of multiset union **) Goal -"[|:multirel1(A, r); multiset[A](K)|] ==> : multirel1(A, r)"; -by (ftac multirel1D 1); -by (auto_tac (claset(), simpset() addsimps [multirel1_iff, multiset_on_def])); +"[|:multirel1(A, r); K:Mult(A) |] ==> :multirel1(A, r)"; +by (ftac (multirel1_type RS subsetD) 1); +by (auto_tac (claset(), simpset() addsimps [multirel1_iff, Mult_iff_multiset])); by (res_inst_tac [("x", "a")] exI 1); by (Asm_simp_tac 1); by (res_inst_tac [("x", "K+#M0")] exI 1); @@ -1252,10 +1217,9 @@ by (asm_simp_tac (simpset() addsimps [munion_assoc]) 1); qed "munion_multirel1_mono"; - Goal - "[| :multirel(A, r); multiset[A](K) |]==>:multirel(A, r)"; -by (ftac multirelD 1); + "[| :multirel(A, r); K:Mult(A) |]==>:multirel(A, r)"; +by (ftac (multirel_type RS subsetD) 1); by (full_simp_tac (simpset() addsimps [multirel_def]) 1); by (Clarify_tac 1); by (dres_inst_tac [("psi", ":multirel1(A, r)^+")] asm_rl 1); @@ -1266,28 +1230,26 @@ by (Clarify_tac 1); by (blast_tac (claset() addIs [munion_multirel1_mono, r_into_trancl]) 1); by (Clarify_tac 1); -by (subgoal_tac "multiset[A](y)" 1); -by (blast_tac (claset() addDs [rewrite_rule [multirel_def] multirelD]) 2); +by (subgoal_tac "y:Mult(A)" 1); +by (blast_tac (claset() addDs [rewrite_rule [multirel_def] multirel_type RS subsetD]) 2); by (subgoal_tac ":multirel1(A, r)" 1); by (blast_tac (claset() addIs [munion_multirel1_mono]) 2); by (blast_tac (claset() addIs [r_into_trancl, trancl_trans]) 1); qed "munion_multirel_mono2"; Goal -"[|:multirel(A, r); multiset[A](K)|] ==> :multirel(A, r)"; -by (ftac multirelD 1); +"[|:multirel(A, r); K:Mult(A)|] ==> :multirel(A, r)"; +by (ftac (multirel_type RS subsetD) 1); by (res_inst_tac [("P", "%x. :multirel(A, r)")] (munion_commute RS subst) 1); by (stac (munion_commute RS sym) 3); -by (rtac munion_multirel_mono2 5); -by (rewtac multiset_on_def); -by Auto_tac; +by (rtac munion_multirel_mono2 5); +by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset])); qed "munion_multirel_mono1"; Goal "[|:multirel(A, r); :multirel(A, r)|]==>:multirel(A, r)"; -by (subgoal_tac "multiset[A](M)& multiset[A](N) & \ -\ multiset[A](K)& multiset[A](L)" 1); -by (blast_tac (claset() addDs [multirelD]) 2); +by (subgoal_tac "M:Mult(A)& N:Mult(A) & K:Mult(A)& L:Mult(A)" 1); +by (blast_tac (claset() addDs [multirel_type RS subsetD]) 2); by (blast_tac (claset() addIs [munion_multirel_mono1, multirel_trans, munion_multirel_mono2]) 1); qed "munion_multirel_mono"; @@ -1304,8 +1266,8 @@ bind_thm ("multirel_Memrel_mono", [field_Memrel_mono, Memrel_mono]MRS multirel_mono); -Goalw [omultiset_def, multiset_on_def] "omultiset(M) ==> multiset(M)"; -by Auto_tac; +Goalw [omultiset_def] "omultiset(M) ==> multiset(M)"; +by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset])); qed "omultiset_is_multiset"; Addsimps [omultiset_is_multiset]; @@ -1313,13 +1275,13 @@ by (Clarify_tac 1); by (res_inst_tac [("x", "i Un ia")] exI 1); by (asm_full_simp_tac (simpset() addsimps - [multiset_on_def, Ord_Un, Un_subset_iff]) 1); + [Mult_iff_multiset, Ord_Un, Un_subset_iff]) 1); by (blast_tac (claset() addIs [field_Memrel_mono]) 1); qed "munion_omultiset"; Addsimps [munion_omultiset]; Goalw [omultiset_def] "omultiset(M) ==> omultiset(M -# N)"; -by (auto_tac (claset(), simpset() addsimps [multiset_on_def])); +by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset])); by (res_inst_tac [("x", "i")] exI 1); by (Asm_simp_tac 1); qed "mdiff_omultiset"; @@ -1422,9 +1384,9 @@ by (Clarify_tac 1); by (res_inst_tac [("x", "i Un ia")] exI 1); by (asm_full_simp_tac (simpset() - addsimps [multiset_on_def, Ord_Un, Un_subset_iff]) 1); + addsimps [Mult_iff_multiset, Ord_Un, Un_subset_iff]) 1); by (rtac munion_multirel_mono2 1); -by (asm_simp_tac (simpset() addsimps [multiset_on_def]) 2); +by (asm_simp_tac (simpset() addsimps [Mult_iff_multiset]) 2); by (blast_tac (claset() addIs [multirel_Memrel_mono RS subsetD]) 1); by (blast_tac (claset() addIs [field_Memrel_mono RS subsetD]) 1); qed "munion_less_mono2"; @@ -1434,16 +1396,16 @@ by (Clarify_tac 1); by (res_inst_tac [("x", "i Un ia")] exI 1); by (asm_full_simp_tac (simpset() - addsimps [multiset_on_def, Ord_Un, Un_subset_iff]) 1); + addsimps [Mult_iff_multiset, Ord_Un, Un_subset_iff]) 1); by (rtac munion_multirel_mono1 1); -by (asm_simp_tac (simpset() addsimps [multiset_on_def]) 2); +by (asm_simp_tac (simpset() addsimps [Mult_iff_multiset]) 2); by (blast_tac (claset() addIs [multirel_Memrel_mono RS subsetD]) 1); by (blast_tac (claset() addIs [field_Memrel_mono RS subsetD]) 1); qed "munion_less_mono1"; Goalw [mless_def, omultiset_def] "M <# N ==> omultiset(M) & omultiset(N)"; -by (auto_tac (claset() addDs [multirelD], simpset())); +by (auto_tac (claset() addDs [multirel_type RS subsetD], simpset())); qed "mless_imp_omultiset"; Goal "[| M <# K; N <# L |] ==> M +# N <# K +# L"; @@ -1472,22 +1434,20 @@ munion_less_mono], simpset())); qed "mle_mono"; -Goalw [omultiset_def, multiset_on_def] "omultiset(0)"; -by Auto_tac; +Goalw [omultiset_def] "omultiset(0)"; +by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset])); qed "omultiset_0"; AddIffs [omultiset_0]; Goalw [mle_def, mless_def] "omultiset(M) ==> 0 <#= M"; -by (subgoal_tac "EX i. Ord(i) & multiset[field(Memrel(i))](M)" 1); +by (subgoal_tac "EX i. Ord(i) & M:Mult(field(Memrel(i)))" 1); by (asm_full_simp_tac (simpset() addsimps [omultiset_def]) 2); by (case_tac "M=0" 1); by (ALLGOALS(Asm_full_simp_tac)); by (Clarify_tac 1); by (subgoal_tac "<0 +# 0, 0 +# M>: multirel(field(Memrel(i)), Memrel(i))" 1); by (rtac one_step_implies_multirel 2); -by Auto_tac; -by (dres_inst_tac [("x", "i")] spec 1); -by (auto_tac (claset(), simpset() addsimps [multiset_on_def])); +by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset])); qed "empty_leI"; Addsimps [empty_leI]; @@ -1498,11 +1458,5 @@ qed "munion_upper1"; -Goal "[| omultiset(M); omultiset(N) |] ==> N <#= M +# N"; -by (stac munion_commute 1); -by (rtac munion_upper1 3); -by Auto_tac; -qed "munion_upper2"; -Delsimps [domain_of_fun]; -AddSEs [domainE]; + diff -r f63315dfffd4 -r 7fc3fbfed8ef src/ZF/Induct/Multiset.thy --- a/src/ZF/Induct/Multiset.thy Mon Jan 28 23:35:20 2002 +0100 +++ b/src/ZF/Induct/Multiset.thy Wed Jan 30 12:22:40 2002 +0100 @@ -9,7 +9,12 @@ *) Multiset = FoldSet + Acc + - +consts + (* Short cut for multiset space *) + Mult :: i=>i +translations + "Mult(A)" => "A-||>nat-{0}" + constdefs (* M is a multiset *) multiset :: i => o @@ -18,16 +23,12 @@ mset_of :: "i=>i" "mset_of(M) == domain(M)" - (* M is a multiset over A *) - multiset_on :: [i,i]=>o ("multiset[_]'(_')") - "multiset[A](M) == multiset(M) & mset_of(M) <= A" - munion :: "[i, i] => i" (infixl "+#" 65) "M +# N == lam x:mset_of(M) Un mset_of(N). if x:mset_of(M) Int mset_of(N) then (M`x) #+ (N`x) else (if x:mset_of(M) then M`x else N`x)" - (* eliminating zeros from a function *) + (* eliminating 0's from a function *) normalize :: i => i "normalize(M) == restrict(M, {x:mset_of(M). 0i" "multirel1(A, r) == - { : (A-||>nat-{0})*(A-||>nat-{0}). - EX a:A. EX M0:A-||>nat-{0}. EX K:A-||>nat-{0}. - N=M0 +# {#a#} & M=M0 +# K & (ALL b:mset_of(K). :r)}" + { : Mult(A)*Mult(A). + EX a:A. EX M0:Mult(A). EX K:Mult(A). + N=M0 +# {#a#} & M=M0 +# K & (ALL b:mset_of(K). :r)}" multirel :: "[i, i] => i" "multirel(A, r) == multirel1(A, r)^+" - (* ordinal multisets orderings *) + (* ordinal multiset orderings *) omultiset :: i => o - "omultiset(M) == EX i. Ord(i) & multiset[field(Memrel(i))](M)" + "omultiset(M) == EX i. Ord(i) & M:Mult(field(Memrel(i)))" mless :: [i, i] => o (infixl "<#" 50) "M <# N == EX i. Ord(i) & :multirel(field(Memrel(i)), Memrel(i))"