src/HOL/Finite_Set.thy
changeset 15074 277b3a4da341
parent 15047 fa62de5862b9
child 15111 c108189645f8
equal deleted inserted replaced
15073:279c2daaf517 15074:277b3a4da341
   763 
   763 
   764 text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
   764 text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
   765 written @{text"\<Sum>x\<in>A. e"}. *}
   765 written @{text"\<Sum>x\<in>A. e"}. *}
   766 
   766 
   767 syntax
   767 syntax
   768   "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_:_. _)" [0, 51, 10] 10)
   768   "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_. _)" [0, 51, 10] 10)
   769 syntax (xsymbols)
   769 syntax (xsymbols)
   770   "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
   770   "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
   771 syntax (HTML output)
   771 syntax (HTML output)
   772   "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
   772   "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
   773 translations
   773 
   774   "\<Sum>i:A. b" == "setsum (%i. b) A"  -- {* Beware of argument permutation! *}
   774 translations -- {* Beware of argument permutation! *}
       
   775   "SUM i:A. b" == "setsum (%i. b) A"
       
   776   "\<Sum>i\<in>A. b" == "setsum (%i. b) A"
   775 
   777 
   776 text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
   778 text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
   777  @{text"\<Sum>x|P. e"}. *}
   779  @{text"\<Sum>x|P. e"}. *}
   778 
   780 
   779 syntax
   781 syntax
   780   "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ | / _./ _)" [0,0,10] 10)
   782   "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
   781 syntax (xsymbols)
   783 syntax (xsymbols)
   782   "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   784   "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   783 syntax (HTML output)
   785 syntax (HTML output)
   784   "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   786   "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   785 
   787 
   786 translations "\<Sum>x|P. t" => "setsum (%x. t) {x. P}"
   788 translations
       
   789   "SUM x|P. t" => "setsum (%x. t) {x. P}"
       
   790   "\<Sum>x|P. t" => "setsum (%x. t) {x. P}"
   787 
   791 
   788 print_translation {*
   792 print_translation {*
   789 let
   793 let
   790   fun setsum_tr' [Abs(x,Tx,t), Const ("Collect",_) $ Abs(y,Ty,P)] = 
   794   fun setsum_tr' [Abs(x,Tx,t), Const ("Collect",_) $ Abs(y,Ty,P)] = 
   791     (if x<>y then raise Match
   795     (if x<>y then raise Match
   892   apply (frule setsum_UN_disjoint [of C id f])
   896   apply (frule setsum_UN_disjoint [of C id f])
   893   apply (unfold Union_def id_def, assumption+)
   897   apply (unfold Union_def id_def, assumption+)
   894   done
   898   done
   895 
   899 
   896 lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
   900 lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
   897     (\<Sum>x:A. (\<Sum>y:B x. f x y)) =
   901     (\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) =
   898     (\<Sum>z:(SIGMA x:A. B x). f (fst z) (snd z))"
   902     (\<Sum>z\<in>(SIGMA x:A. B x). f (fst z) (snd z))"
   899   apply (subst Sigma_def)
   903   apply (subst Sigma_def)
   900   apply (subst setsum_UN_disjoint)
   904   apply (subst setsum_UN_disjoint)
   901   apply assumption
   905   apply assumption
   902   apply (rule ballI)
   906   apply (rule ballI)
   903   apply (drule_tac x = i in bspec, assumption)
   907   apply (drule_tac x = i in bspec, assumption)
   909   apply (erule bspec, assumption)
   913   apply (erule bspec, assumption)
   910   apply auto
   914   apply auto
   911   done
   915   done
   912 
   916 
   913 lemma setsum_cartesian_product: "finite A ==> finite B ==>
   917 lemma setsum_cartesian_product: "finite A ==> finite B ==>
   914     (\<Sum>x:A. (\<Sum>y:B. f x y)) =
   918     (\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) =
   915     (\<Sum>z:A <*> B. f (fst z) (snd z))"
   919     (\<Sum>z\<in>A <*> B. f (fst z) (snd z))"
   916   by (erule setsum_Sigma, auto);
   920   by (erule setsum_Sigma, auto);
   917 
   921 
   918 lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
   922 lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
   919   apply (case_tac "finite A")
   923   apply (case_tac "finite A")
   920    prefer 2 apply (simp add: setsum_def)
   924    prefer 2 apply (simp add: setsum_def)
   934 lemma setsum_eq_0_iff [simp]:
   938 lemma setsum_eq_0_iff [simp]:
   935     "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
   939     "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
   936   by (induct set: Finites) auto
   940   by (induct set: Finites) auto
   937 
   941 
   938 lemma setsum_constant_nat:
   942 lemma setsum_constant_nat:
   939     "finite A ==> (\<Sum>x: A. y) = (card A) * y"
   943     "finite A ==> (\<Sum>x\<in>A. y) = (card A) * y"
   940   -- {* Generalized to any @{text comm_semiring_1_cancel} in
   944   -- {* Generalized to any @{text comm_semiring_1_cancel} in
   941         @{text IntDef} as @{text setsum_constant}. *}
   945         @{text IntDef} as @{text setsum_constant}. *}
   942   by (erule finite_induct, auto)
   946   by (erule finite_induct, auto)
   943 
   947 
   944 lemma setsum_Un: "finite A ==> finite B ==>
   948 lemma setsum_Un: "finite A ==> finite B ==>
  1045   apply (auto simp add: inj_on_def)
  1049   apply (auto simp add: inj_on_def)
  1046   done
  1050   done
  1047 
  1051 
  1048 lemma card_SigmaI [rule_format,simp]: "finite A ==>
  1052 lemma card_SigmaI [rule_format,simp]: "finite A ==>
  1049   (ALL a:A. finite (B a)) -->
  1053   (ALL a:A. finite (B a)) -->
  1050   card (SIGMA x: A. B x) = (\<Sum>a: A. card (B a))"
  1054   card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
  1051   apply (erule finite_induct, auto)
  1055   apply (erule finite_induct, auto)
  1052   apply (subst SigmaI_insert, assumption)
  1056   apply (subst SigmaI_insert, assumption)
  1053   apply (subst card_Un_disjoint)
  1057   apply (subst card_Un_disjoint)
  1054   apply (auto intro: finite_SigmaI simp add: card_cartesian_product_singleton)
  1058   apply (auto intro: finite_SigmaI simp add: card_cartesian_product_singleton)
  1055   done
  1059   done