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.
--- 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 "<cons(x,C), y> : 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 "<C, x> : fold_set(A, B, f, e) \
+\ ==> ALL D. A<=D --> <C, x> : 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 "[| <C-{x},y> : fold_set(A, B, f,e); x:C; x:A |] \
-\ ==> <C, f(x,y)> : 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 "<C, x>:fold_set(A, B, f, e) ==> <C, x>: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 "[| <C-{x},y> : fold_set(A, B, f,e); x:C; x:A; f(x, y):B |] \
+\ ==> <C, f(x, y)> : 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. <C, 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. <C, 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|<n --> e:B --> <C, x> : fold_set(A, B, f,e)-->\
-\ (ALL y. <C, 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|<n --> \
+\ (ALL x. <C, x> : fold_set(A, B, f,e)-->\
+\ (ALL y. <C, 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 "<Cb-{x}, xa>: 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 "[| <C, x> : fold_set(A, B, f, e); \
-\ <C, y> : fold_set(A, B, f, e); e:B |] ==> y=x";
-by (forward_tac [fold_set_lhs RS Fin_into_Finite] 1);
+Goal
+"[| <C, x>:fold_set(A, 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)) |]\
+\ ==> 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]
- "[| <C,y> : fold_set(C, B, f, e); e:B |] ==> fold[B](f,e,C) = y";
+"[| <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 |] \
-\ ==> <cons(x, C), v> : fold_set(A, B, f, e) <-> \
-\ (EX y. <C, 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)) |] \
+\ ==> <cons(c, C), v> : fold_set(cons(c, C), B, f, e) <-> \
+\ (EX y. <C, 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 "<D, x> : fold_set(C, B, f, e) \
-\ ==> ALL A. C<=A --> <D, x> : 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 "<C,x> : fold_set(A, B, f, e) ==> <C, x> : 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)";
--- 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. <C,x>:fold_set(C, B, f,e)"
+ "fold[B](f,e, A) == THE x. <A, 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
--- 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 "<M, N>: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]
" <N, M>: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). <b,a>: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] "<M,0>~: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 "[| <N, M0 +# {#a#}>:multirel1(A, r); multiset[A](M0) |] ==> \
+Goal "[| <N, M0 +# {#a#}>:multirel1(A, r); M0:Mult(A) |] ==> \
\ (EX M. <M, M0>:multirel1(A, r) & N = M +# {#a#}) | \
-\ (EX K. multiset[A](K) & (ALL b:mset_of(K). <b, a>:r) & N = M0 +# K)";
-by (ftac multirel1D 1);
+\ (EX K. K:Mult(A) & (ALL b:mset_of(K). <b, a>: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 |] ==> <M, M +# {#a#}>: multirel1(A, r)";
+Goal "[| M:Mult(A); a:A |] ==> <M, M +# {#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. <M,M0> : 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). <x, a>: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. <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 "<M, N>: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 @@
"<M,N>: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). <k,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). <k, j>:r)) \
\ --> <I +# K, I +# J>: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. <x, a>: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). <k,j>:r;\
-\ multiset[A](I); multiset[A](J); multiset[A](K) |] \
+\ I:Mult(A); J:Mult(A); K:Mult(A) |] \
\ ==> <I+#K, I+#J> : 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
-"[|<M,N>:multirel1(A, r); multiset[A](K)|] ==> <K +# M, K +# N>: multirel1(A, r)";
-by (ftac multirel1D 1);
-by (auto_tac (claset(), simpset() addsimps [multirel1_iff, multiset_on_def]));
+"[|<M,N>:multirel1(A, r); K:Mult(A) |] ==> <K +# M, K +# N>: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
- "[| <M, N>:multirel(A, r); multiset[A](K) |]==><K +# M, K +# N>:multirel(A, r)";
-by (ftac multirelD 1);
+ "[| <M, N>:multirel(A, r); K:Mult(A) |]==><K +# M, K +# N>: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", "<M,N>: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 "<K +# y, K +# z>: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
-"[|<M, N>:multirel(A, r); multiset[A](K)|] ==> <M +# K, N +# K>:multirel(A, r)";
-by (ftac multirelD 1);
+"[|<M, N>:multirel(A, r); K:Mult(A)|] ==> <M +# K, N +# K>:multirel(A, r)";
+by (ftac (multirel_type RS subsetD) 1);
by (res_inst_tac [("P", "%x. <x,?u>: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
"[|<M,K>:multirel(A, r); <N,L>:multirel(A, r)|]==><M +# N, K +# L>: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];
+
--- 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). 0<M`x})"
@@ -65,17 +66,17 @@
multirel1 :: "[i,i]=>i"
"multirel1(A, r) ==
- {<M, N> : (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). <b,a>:r)}"
+ {<M, N> : 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). <b,a>: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) & <M, N>:multirel(field(Memrel(i)), Memrel(i))"