src/HOL/Library/Permutations.thy
 changeset 30036 3a074e3a9a18 parent 29840 cfab6a76aa13 child 30037 6ff7793d0f0d
```     1.1 --- a/src/HOL/Library/Permutations.thy	Fri Feb 20 16:07:20 2009 -0800
1.2 +++ b/src/HOL/Library/Permutations.thy	Fri Feb 20 22:10:37 2009 -0800
1.3 @@ -757,13 +757,13 @@
1.4  done
1.5
1.6  term setsum
1.7 -lemma setsum_permutations_inverse: "setsum f {p. p permutes {m..n}} = setsum (\<lambda>p. f(inv p)) {p. p permutes {m..n}}" (is "?lhs = ?rhs")
1.8 +lemma setsum_permutations_inverse: "setsum f {p. p permutes S} = setsum (\<lambda>p. f(inv p)) {p. p permutes S}" (is "?lhs = ?rhs")
1.9  proof-
1.10 -  let ?S = "{p . p permutes {m .. n}}"
1.11 +  let ?S = "{p . p permutes S}"
1.12  have th0: "inj_on inv ?S"
1.14    fix q r
1.15 -  assume q: "q permutes {m .. n}" and r: "r permutes {m .. n}" and qr: "inv q = inv r"
1.16 +  assume q: "q permutes S" and r: "r permutes S" and qr: "inv q = inv r"
1.17    hence "inv (inv q) = inv (inv r)" by simp
1.18    with permutes_inv_inv[OF q] permutes_inv_inv[OF r]
1.19    show "q = r" by metis
1.20 @@ -774,17 +774,17 @@
1.21  qed
1.22
1.23  lemma setum_permutations_compose_left:
1.24 -  assumes q: "q permutes {m..n}"
1.25 -  shows "setsum f {p. p permutes {m..n}} =
1.26 -            setsum (\<lambda>p. f(q o p)) {p. p permutes {m..n}}" (is "?lhs = ?rhs")
1.27 +  assumes q: "q permutes S"
1.28 +  shows "setsum f {p. p permutes S} =
1.29 +            setsum (\<lambda>p. f(q o p)) {p. p permutes S}" (is "?lhs = ?rhs")
1.30  proof-
1.31 -  let ?S = "{p. p permutes {m..n}}"
1.32 +  let ?S = "{p. p permutes S}"
1.33    have th0: "?rhs = setsum (f o (op o q)) ?S" by (simp add: o_def)
1.34    have th1: "inj_on (op o q) ?S"
1.35      apply (auto simp add: inj_on_def)
1.36    proof-
1.37      fix p r
1.38 -    assume "p permutes {m..n}" and r:"r permutes {m..n}" and rp: "q \<circ> p = q \<circ> r"
1.39 +    assume "p permutes S" and r:"r permutes S" and rp: "q \<circ> p = q \<circ> r"
1.40      hence "inv q o q o p = inv q o q o r" by (simp add: o_assoc[symmetric])
1.41      with permutes_inj[OF q, unfolded inj_iff]
1.42
1.43 @@ -796,17 +796,17 @@
1.44  qed
1.45
1.46  lemma sum_permutations_compose_right:
1.47 -  assumes q: "q permutes {m..n}"
1.48 -  shows "setsum f {p. p permutes {m..n}} =
1.49 -            setsum (\<lambda>p. f(p o q)) {p. p permutes {m..n}}" (is "?lhs = ?rhs")
1.50 +  assumes q: "q permutes S"
1.51 +  shows "setsum f {p. p permutes S} =
1.52 +            setsum (\<lambda>p. f(p o q)) {p. p permutes S}" (is "?lhs = ?rhs")
1.53  proof-
1.54 -  let ?S = "{p. p permutes {m..n}}"
1.55 +  let ?S = "{p. p permutes S}"
1.56    have th0: "?rhs = setsum (f o (\<lambda>p. p o q)) ?S" by (simp add: o_def)
1.57    have th1: "inj_on (\<lambda>p. p o q) ?S"
1.58      apply (auto simp add: inj_on_def)
1.59    proof-
1.60      fix p r
1.61 -    assume "p permutes {m..n}" and r:"r permutes {m..n}" and rp: "p o q = r o q"
1.62 +    assume "p permutes S" and r:"r permutes S" and rp: "p o q = r o q"
1.63      hence "p o (q o inv q)  = r o (q o inv q)" by (simp add: o_assoc)
1.64      with permutes_surj[OF q, unfolded surj_iff]
1.65
```