src/HOL/Finite_Set.thy
equal inserted replaced
12692:df42e9a53a02 12693:827818b891c7
`   709 `
`   709 `
`   710 lemma (in ACe)`
`   710 lemma (in ACe)`
`   711     AC: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"  "x \<cdot> y = y \<cdot> x"  "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"`
`   711     AC: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"  "x \<cdot> y = y \<cdot> x"  "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"`
`   712   by (rule assoc, rule commute, rule left_commute)  (* FIXME localize "lemmas" (!??) *)`
`   712   by (rule assoc, rule commute, rule left_commute)  (* FIXME localize "lemmas" (!??) *)`
`   713 `
`   713 `
`   714 lemma (in ACe [simp]) left_ident: "e \<cdot> x = x"`
`   714 lemma (in ACe) left_ident [simp]: "e \<cdot> x = x"`
`   715 proof -`
`   715 proof -`
`   716   have "x \<cdot> e = x" by (rule ident)`
`   716   have "x \<cdot> e = x" by (rule ident)`
`   717   thus ?thesis by (subst commute)`
`   717   thus ?thesis by (subst commute)`
`   718 qed`
`   718 qed`
`   719 `
`   719 `
`   720 lemma (in ACe) fold_Un_Int:`
`   720 lemma (in ACe) fold_Un_Int:`
`   721   "finite A ==> finite B ==>`
`   721   "finite A ==> finite B ==>`
`   722     fold f e A \<cdot> fold f e B = fold f e (A Un B) \<cdot> fold f e (A Int B)"`
`   722     fold f e A \<cdot> fold f e B = fold f e (A Un B) \<cdot> fold f e (A Int B)"`
`   723   apply (induct set: Finites)`
`   723   apply (induct set: Finites)`
`   724    apply simp`
`   724    apply simp`
`   725   apply (simp add: AC fold_insert insert_absorb Int_insert_left)`
`   725   apply (simp add: AC LC.fold_insert insert_absorb Int_insert_left)`
`   726   done`
`   726   done`
`   727 `
`   727 `
`   728 lemma (in ACe) fold_Un_disjoint:`
`   728 lemma (in ACe) fold_Un_disjoint:`
`   729   "finite A ==> finite B ==> A Int B = {} ==>`
`   729   "finite A ==> finite B ==> A Int B = {} ==>`
`   730     fold f e (A Un B) = fold f e A \<cdot> fold f e B"`
`   730     fold f e (A Un B) = fold f e A \<cdot> fold f e B"`
`   744   next`
`   744   next`
`   745     case (insert F x)`
`   745     case (insert F x)`
`   746     have "fold (f \<circ> g) e (insert x F \<union> B) = fold (f \<circ> g) e (insert x (F \<union> B))"`
`   746     have "fold (f \<circ> g) e (insert x F \<union> B) = fold (f \<circ> g) e (insert x (F \<union> B))"`
`   747       by simp`
`   747       by simp`
`   748     also have "... = (f \<circ> g) x (fold (f \<circ> g) e (F \<union> B))"`
`   748     also have "... = (f \<circ> g) x (fold (f \<circ> g) e (F \<union> B))"`
`   749       by (rule fold_insert) (insert b insert, auto simp add: left_commute)  (* FIXME import of fold_insert (!?) *)`
`   749       by (rule LC.fold_insert) (insert b insert, auto simp add: left_commute)  (* FIXME import of fold_insert (!?) *)`
`   750     also from insert have "fold (f \<circ> g) e (F \<union> B) =`
`   750     also from insert have "fold (f \<circ> g) e (F \<union> B) =`
`   751       fold (f \<circ> g) e F \<cdot> fold (f \<circ> g) e B" by blast`
`   751       fold (f \<circ> g) e F \<cdot> fold (f \<circ> g) e B" by blast`
`   752     also have "(f \<circ> g) x ... = (f \<circ> g) x (fold (f \<circ> g) e F) \<cdot> fold (f \<circ> g) e B"`
`   752     also have "(f \<circ> g) x ... = (f \<circ> g) x (fold (f \<circ> g) e F) \<cdot> fold (f \<circ> g) e B"`
`   753       by (simp add: AC)`
`   753       by (simp add: AC)`
`   754     also have "(f \<circ> g) x (fold (f \<circ> g) e F) = fold (f \<circ> g) e (insert x F)"`
`   754     also have "(f \<circ> g) x (fold (f \<circ> g) e F) = fold (f \<circ> g) e (insert x F)"`
`   755       by (rule fold_insert [symmetric]) (insert b insert, auto simp add: left_commute)`
`   755       by (rule LC.fold_insert [symmetric]) (insert b insert, auto simp add: left_commute)`
`   756     finally show ?case .`
`   756     finally show ?case .`
`   757   qed`
`   757   qed`
`   758 qed`
`   758 qed`
`   759 `
`   759 `
`   760 `
`   760 `
`   775 lemma setsum_empty [simp]: "setsum f {} = 0"`
`   775 lemma setsum_empty [simp]: "setsum f {} = 0"`
`   776   by (simp add: setsum_def)`
`   776   by (simp add: setsum_def)`
`   777 `
`   777 `
`   778 lemma setsum_insert [simp]:`
`   778 lemma setsum_insert [simp]:`
`   779     "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"`
`   779     "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"`
`   780   by (simp add: setsum_def fold_insert plus_ac0_left_commute)`
`   780   by (simp add: setsum_def LC.fold_insert plus_ac0_left_commute)`
`   781 `
`   781 `
`   782 lemma setsum_0: "setsum (\<lambda>i. 0) A = 0"`
`   782 lemma setsum_0: "setsum (\<lambda>i. 0) A = 0"`
`   783   apply (case_tac "finite A")`
`   783   apply (case_tac "finite A")`
`   784    prefer 2 apply (simp add: setsum_def)`
`   784    prefer 2 apply (simp add: setsum_def)`
`   785   apply (erule finite_induct)`
`   785   apply (erule finite_induct)`