generalize some lemmas
authorhuffman
Fri Feb 20 22:10:37 2009 -0800 (2009-02-20)
changeset 300363a074e3a9a18
parent 30033 e54d4d41fe8f
child 30037 6ff7793d0f0d
generalize some lemmas
src/HOL/Library/Permutations.thy
     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.13  proof(auto simp add: inj_on_def)
    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