Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/UNITY/MultisetSum.ML
changeset 14092 68da54626309
parent 14071 373806545656 
--- a/src/ZF/UNITY/MultisetSum.ML	Mon Jul 07 17:58:21 2003 +0200
+++ b/src/ZF/UNITY/MultisetSum.ML	Tue Jul 08 11:44:30 2003 +0200
@@ -1,5 +1,5 @@
 (*  Title:      ZF/UNITY/MultusetSum.thy
-    ID:         $Id$
+    ID:         $Id \\<in> MultisetSum.ML,v 1.2 2003/06/24 14:33:00 paulson Exp $
     Author:     Sidi O Ehmety
     Copyright:  2002 University of Cambridge
 Setsum for multisets.
@@ -16,7 +16,7 @@
 Addsimps [general_setsum_0];
 
 Goalw [general_setsum_def] 
-"[| C:Fin(A); a:A; a~:C; e:B; ALL x:A. g(x):B; lcomm(B, B, f) |] ==> \
+"[| C \\<in> Fin(A); a \\<in> A; a\\<notin>C; e \\<in> B; \\<forall>x \\<in> A. g(x):B; lcomm(B, B, f) |] ==> \
 \ general_setsum(cons(a, C), B, e, f, g) = \
 \   f(g(a), general_setsum(C, B, e, f,g))";
 by  (auto_tac (claset(), simpset() addsimps [Fin_into_Finite RS Finite_cons, 
@@ -45,7 +45,7 @@
 (** msetsum **)
 
 Goal
-"[| C:Fin(A); ALL x:A. multiset(g(x))& mset_of(g(x))<=B  |]  \
+"[| C \\<in> Fin(A); \\<forall>x \\<in> A. multiset(g(x))& mset_of(g(x))<=B  |]  \
 \  ==> multiset(general_setsum(C, B -||> nat - {0}, 0, \\<lambda>u v. u +# v, g))";
 by (etac Fin_induct 1);
 by Auto_tac;
@@ -59,7 +59,7 @@
 Addsimps [msetsum_0];
 
 Goalw [msetsum_def]
-"[| C:Fin(A); a~:C; a:A; ALL x:A. multiset(g(x)) & mset_of(g(x))<=B  |]  \
+"[| C \\<in> Fin(A); a\\<notin>C; a \\<in> A; \\<forall>x \\<in> A. multiset(g(x)) & mset_of(g(x))<=B  |]  \
 \  ==> msetsum(g, cons(a, C), B) = g(a) +#  msetsum(g, C, B)";
 by (stac general_setsum_cons 1); 
 by (auto_tac (claset(), simpset() addsimps [multiset_general_setsum, Mult_iff_multiset]));
@@ -73,7 +73,7 @@
 qed "msetsum_multiset";
 
 Goal 
-"[| C:Fin(A); ALL x:A. multiset(g(x)) & mset_of(g(x))<=B |] \ 
+"[| C \\<in> Fin(A); \\<forall>x \\<in> A. multiset(g(x)) & mset_of(g(x))<=B |] \ 
 \ ==> mset_of(msetsum(g, C, B))<=B";
 by (etac Fin_induct 1);
 by Auto_tac;
@@ -83,15 +83,15 @@
 
 (*The reversed orientation looks more natural, but LOOPS as a simprule!*)
 Goal 
-"[| C:Fin(A); D:Fin(A); ALL x:A. multiset(g(x)) & mset_of(g(x))<=B |] \
+"[| C \\<in> Fin(A); D \\<in> Fin(A); \\<forall>x \\<in> A. multiset(g(x)) & mset_of(g(x))<=B |] \
 \     ==> msetsum(g, C Un D, B) +# msetsum(g, C Int D, B) \
 \       = msetsum(g, C, B) +# msetsum(g, D, B)";
 by (etac Fin_induct 1);
 by (subgoal_tac "cons(x, y) Un D = cons(x, y Un D)" 2);
 by (auto_tac (claset(), simpset() addsimps [msetsum_multiset]));
-by (subgoal_tac "y Un D:Fin(A) & y Int D : Fin(A)" 1);
+by (subgoal_tac "y Un D \\<in> Fin(A) & y Int D \\<in> Fin(A)" 1);
 by (Clarify_tac 1);
-by (case_tac "x:D" 1);
+by (case_tac "x \\<in> D" 1);
 by (subgoal_tac "cons(x, y) Int D = y Int D" 2);
 by (subgoal_tac "cons(x, y) Int D = cons(x, y Int D)" 1);
 by (ALLGOALS(asm_simp_tac (simpset() addsimps [cons_absorb,
@@ -101,34 +101,34 @@
 qed "msetsum_Un_Int";
 
 
-Goal "[| C:Fin(A); D:Fin(A); C Int D = 0; \
-\  ALL x:A. multiset(g(x)) & mset_of(g(x))<=B |] \
+Goal "[| C \\<in> Fin(A); D \\<in> Fin(A); C Int D = 0; \
+\  \\<forall>x \\<in> A. multiset(g(x)) & mset_of(g(x))<=B |] \
 \     ==> msetsum(g, C Un D, B) = msetsum(g, C, B) +# msetsum(g,D, B)";  
 by (stac (msetsum_Un_Int RS sym) 1);
 by (auto_tac (claset(),  simpset() addsimps [msetsum_multiset]));
 qed "msetsum_Un_disjoint";
 
-Goal "I:Fin(A) ==> (ALL i:I. C(i):Fin(B)) --> (UN i:I. C(i)):Fin(B)";
+Goal "I \\<in> Fin(A) ==> (\\<forall>i \\<in> I. C(i):Fin(B)) --> (\\<Union>i \\<in> I. C(i)):Fin(B)";
 by (etac Fin_induct 1);
 by Auto_tac;
 qed_spec_mp "UN_Fin_lemma";
  
-Goal "!!I. [| I:Fin(K); ALL i:K. C(i):Fin(A) |] ==> \
-\ (ALL x:A. multiset(f(x)) & mset_of(f(x))<=B) -->  \
-\ (ALL i:I. ALL j:I. i~=j --> C(i) Int C(j) = 0) --> \
-\   msetsum(f, UN i:I. C(i), B) = msetsum (%i. msetsum(f, C(i),B), I, B)"; 
+Goal "!!I. [| I \\<in> Fin(K); \\<forall>i \\<in> K. C(i):Fin(A) |] ==> \
+\ (\\<forall>x \\<in> A. multiset(f(x)) & mset_of(f(x))<=B) -->  \
+\ (\\<forall>i \\<in> I. \\<forall>j \\<in> I. i\\<noteq>j --> C(i) Int C(j) = 0) --> \
+\   msetsum(f, \\<Union>i \\<in> I. C(i), B) = msetsum (%i. msetsum(f, C(i),B), I, B)"; 
 by (etac Fin_induct 1);
 by (ALLGOALS(Clarify_tac));
 by Auto_tac;
-by (subgoal_tac "ALL i:y. x ~= i" 1);
+by (subgoal_tac "\\<forall>i \\<in> y. x \\<noteq> i" 1);
  by (Blast_tac 2); 
-by (subgoal_tac "C(x) Int (UN i:y. C(i)) = 0" 1);
+by (subgoal_tac "C(x) Int (\\<Union>i \\<in> y. C(i)) = 0" 1);
  by (Blast_tac 2);
-by (subgoal_tac " (UN i:y. C(i)):Fin(A) & C(x):Fin(A)" 1);
+by (subgoal_tac " (\\<Union>i \\<in> y. C(i)):Fin(A) & C(x):Fin(A)" 1);
 by (blast_tac (claset() addIs [UN_Fin_lemma] addDs [FinD]) 2);
 by (Clarify_tac 1);
 by (asm_simp_tac (simpset() addsimps [msetsum_Un_disjoint]) 1);
-by (subgoal_tac "ALL x:K. multiset(msetsum(f, C(x), B)) &\
+by (subgoal_tac "\\<forall>x \\<in> K. multiset(msetsum(f, C(x), B)) &\
                 \ mset_of(msetsum(f, C(x), B)) <= B" 1);
 by (Asm_simp_tac 1);
 by (Clarify_tac 1);
@@ -137,11 +137,11 @@
 qed_spec_mp "msetsum_UN_disjoint";
 
 Goal 
-"[| C:Fin(A); \
-\ ALL x:A. multiset(f(x)) & mset_of(f(x))<=B; \
-\ ALL x:A. multiset(g(x)) & mset_of(g(x))<=B |] ==>\
+"[| C \\<in> Fin(A); \
+\ \\<forall>x \\<in> A. multiset(f(x)) & mset_of(f(x))<=B; \
+\ \\<forall>x \\<in> A. multiset(g(x)) & mset_of(g(x))<=B |] ==>\
 \ msetsum(%x. f(x) +# g(x), C, B) = msetsum(f, C, B) +# msetsum(g, C, B)";
-by (subgoal_tac "ALL x:A. multiset(f(x) +# g(x)) & mset_of(f(x) +# g(x))<=B" 1);
+by (subgoal_tac "\\<forall>x \\<in> A. multiset(f(x) +# g(x)) & mset_of(f(x) +# g(x))<=B" 1);
 by (etac Fin_induct 1);
 by (ALLGOALS(Asm_simp_tac));
 by (resolve_tac [trans] 1);
@@ -153,7 +153,7 @@
 
 
 val prems = Goal
- "[| C=D; !!x. x:D ==> f(x) = g(x) |] ==> \
+ "[| C=D; !!x. x \\<in> D ==> f(x) = g(x) |] ==> \
 \    msetsum(f, C, B) = msetsum(g, D, B)";
 by (asm_full_simp_tac (simpset() addsimps [msetsum_def, general_setsum_def]@prems addcongs [fold_cong]) 1);
 qed  "msetsum_cong";
@@ -163,11 +163,11 @@
 qed "multiset_union_diff";
 
 
-Goal "[| C:Fin(A); D:Fin(A); \
-\ ALL x:A. multiset(f(x)) & mset_of(f(x))<=B  |] \
+Goal "[| C \\<in> Fin(A); D \\<in> Fin(A); \
+\ \\<forall>x \\<in> A. multiset(f(x)) & mset_of(f(x))<=B  |] \
 \  ==> msetsum(f, C Un D, B) = \
 \         msetsum(f, C, B) +# msetsum(f, D, B) -# msetsum(f, C Int D, B)";
-by (subgoal_tac "C Un D:Fin(A) & C Int D:Fin(A)" 1);
+by (subgoal_tac "C Un D \\<in> Fin(A) & C Int D \\<in> Fin(A)" 1);
 by (Clarify_tac 1);
 by (stac (msetsum_Un_Int RS sym) 1);
 by (ALLGOALS(asm_simp_tac (simpset() addsimps 
@@ -182,7 +182,7 @@
 Addsimps [nsetsum_0];
 
 Goalw [nsetsum_def, general_setsum_def] 
-"[| Finite(C); x~:C |] \
+"[| Finite(C); x\\<notin>C |] \
 \  ==> nsetsum(g, cons(x, C))= g(x) #+ nsetsum(g, C)";
 by (auto_tac (claset(), simpset() addsimps [Finite_cons]));
 by (res_inst_tac [("A", "cons(x, C)")] (thm"fold_typing.fold_cons") 1);
isabelle