equal
deleted
inserted
replaced
101 (* ------------------------------------------------------------------------- *) |
101 (* ------------------------------------------------------------------------- *) |
102 |
102 |
103 lemma setprod_permute: |
103 lemma setprod_permute: |
104 assumes p: "p permutes S" |
104 assumes p: "p permutes S" |
105 shows "setprod f S = setprod (f o p) S" |
105 shows "setprod f S = setprod (f o p) S" |
106 proof- |
106 using assms by (fact setprod.permute) |
107 {assume "\<not> finite S" hence ?thesis by simp} |
|
108 moreover |
|
109 {assume fS: "finite S" |
|
110 then have ?thesis |
|
111 apply (simp add: setprod_def cong del:strong_setprod_cong) |
|
112 apply (rule ab_semigroup_mult.fold_image_permute) |
|
113 apply (auto simp add: p) |
|
114 apply unfold_locales |
|
115 done} |
|
116 ultimately show ?thesis by blast |
|
117 qed |
|
118 |
107 |
119 lemma setproduct_permute_nat_interval: "p permutes {m::nat .. n} ==> setprod f {m..n} = setprod (f o p) {m..n}" |
108 lemma setproduct_permute_nat_interval: "p permutes {m::nat .. n} ==> setprod f {m..n} = setprod (f o p) {m..n}" |
120 by (blast intro!: setprod_permute) |
109 by (blast intro!: setprod_permute) |
121 |
110 |
122 (* ------------------------------------------------------------------------- *) |
111 (* ------------------------------------------------------------------------- *) |