src/HOL/Library/Permutations.thy
 changeset 30240 5b25fee0362c parent 29840 cfab6a76aa13 child 30242 aea5d7fa7ef5
```     1.1 --- a/src/HOL/Library/Permutations.thy	Wed Mar 04 10:43:39 2009 +0100
1.2 +++ b/src/HOL/Library/Permutations.thy	Wed Mar 04 10:45:52 2009 +0100
1.3 @@ -6,7 +6,7 @@
1.4  header {* Permutations, both general and specifically on finite sets.*}
1.5
1.6  theory Permutations
1.7 -imports Main Finite_Cartesian_Product Parity
1.8 +imports Main Finite_Cartesian_Product Parity Fact
1.9  begin
1.10
1.11    (* Why should I import Main just to solve the Typerep problem! *)
1.12 @@ -683,13 +683,13 @@
1.13  (* ------------------------------------------------------------------------- *)
1.14
1.15  lemma permutes_natset_le:
1.16 -  assumes p: "p permutes (S:: nat set)" and le: "\<forall>i \<in> S.  p i <= i" shows "p = id"
1.17 +  assumes p: "p permutes (S::'a::wellorder set)" and le: "\<forall>i \<in> S.  p i <= i" shows "p = id"
1.18  proof-
1.19    {fix n
1.20      have "p n = n"
1.21        using p le
1.22 -    proof(induct n arbitrary: S rule: nat_less_induct)
1.23 -      fix n S assume H: "\<forall> m< n. \<forall>S. p permutes S \<longrightarrow> (\<forall>i\<in>S. p i \<le> i) \<longrightarrow> p m = m"
1.24 +    proof(induct n arbitrary: S rule: less_induct)
1.25 +      fix n S assume H: "\<And>m S. \<lbrakk>m < n; p permutes S; \<forall>i\<in>S. p i \<le> i\<rbrakk> \<Longrightarrow> p m = m"
1.26  	"p permutes S" "\<forall>i \<in>S. p i \<le> i"
1.27        {assume "n \<notin> S"
1.28  	with H(2) have "p n = n" unfolding permutes_def by metis}
1.29 @@ -699,7 +699,7 @@
1.30  	moreover{assume h: "p n < n"
1.31  	  from H h have "p (p n) = p n" by metis
1.32  	  with permutes_inj[OF H(2)] have "p n = n" unfolding inj_on_def by blast
1.33 -	  with h have False by arith}
1.34 +	  with h have False by simp}
1.35  	ultimately have "p n = n" by blast }
1.36        ultimately show "p n = n"  by blast
1.37      qed}
1.38 @@ -707,7 +707,7 @@
1.39  qed
1.40
1.41  lemma permutes_natset_ge:
1.42 -  assumes p: "p permutes (S:: nat set)" and le: "\<forall>i \<in> S.  p i \<ge> i" shows "p = id"
1.43 +  assumes p: "p permutes (S::'a::wellorder set)" and le: "\<forall>i \<in> S.  p i \<ge> i" shows "p = id"
1.44  proof-
1.45    {fix i assume i: "i \<in> S"
1.46      from i permutes_in_image[OF permutes_inv[OF p]] have "inv p i \<in> S" by simp
1.47 @@ -757,13 +757,13 @@
1.48  done
1.49
1.50  term setsum
1.51 -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.52 +lemma setsum_permutations_inverse: "setsum f {p. p permutes S} = setsum (\<lambda>p. f(inv p)) {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: "inj_on inv ?S"
1.58    fix q r
1.59 -  assume q: "q permutes {m .. n}" and r: "r permutes {m .. n}" and qr: "inv q = inv r"
1.60 +  assume q: "q permutes S" and r: "r permutes S" and qr: "inv q = inv r"
1.61    hence "inv (inv q) = inv (inv r)" by simp
1.62    with permutes_inv_inv[OF q] permutes_inv_inv[OF r]
1.63    show "q = r" by metis
1.64 @@ -774,17 +774,17 @@
1.65  qed
1.66
1.67  lemma setum_permutations_compose_left:
1.68 -  assumes q: "q permutes {m..n}"
1.69 -  shows "setsum f {p. p permutes {m..n}} =
1.70 -            setsum (\<lambda>p. f(q o p)) {p. p permutes {m..n}}" (is "?lhs = ?rhs")
1.71 +  assumes q: "q permutes S"
1.72 +  shows "setsum f {p. p permutes S} =
1.73 +            setsum (\<lambda>p. f(q o p)) {p. p permutes S}" (is "?lhs = ?rhs")
1.74  proof-
1.75 -  let ?S = "{p. p permutes {m..n}}"
1.76 +  let ?S = "{p. p permutes S}"
1.77    have th0: "?rhs = setsum (f o (op o q)) ?S" by (simp add: o_def)
1.78    have th1: "inj_on (op o q) ?S"
1.79      apply (auto simp add: inj_on_def)
1.80    proof-
1.81      fix p r
1.82 -    assume "p permutes {m..n}" and r:"r permutes {m..n}" and rp: "q \<circ> p = q \<circ> r"
1.83 +    assume "p permutes S" and r:"r permutes S" and rp: "q \<circ> p = q \<circ> r"
1.84      hence "inv q o q o p = inv q o q o r" by (simp add: o_assoc[symmetric])
1.85      with permutes_inj[OF q, unfolded inj_iff]
1.86
1.87 @@ -796,17 +796,17 @@
1.88  qed
1.89
1.90  lemma sum_permutations_compose_right:
1.91 -  assumes q: "q permutes {m..n}"
1.92 -  shows "setsum f {p. p permutes {m..n}} =
1.93 -            setsum (\<lambda>p. f(p o q)) {p. p permutes {m..n}}" (is "?lhs = ?rhs")
1.94 +  assumes q: "q permutes S"
1.95 +  shows "setsum f {p. p permutes S} =
1.96 +            setsum (\<lambda>p. f(p o q)) {p. p permutes S}" (is "?lhs = ?rhs")
1.97  proof-
1.98 -  let ?S = "{p. p permutes {m..n}}"
1.99 +  let ?S = "{p. p permutes S}"
1.100    have th0: "?rhs = setsum (f o (\<lambda>p. p o q)) ?S" by (simp add: o_def)
1.101    have th1: "inj_on (\<lambda>p. p o q) ?S"
1.102      apply (auto simp add: inj_on_def)
1.103    proof-
1.104      fix p r
1.105 -    assume "p permutes {m..n}" and r:"r permutes {m..n}" and rp: "p o q = r o q"
1.106 +    assume "p permutes S" and r:"r permutes S" and rp: "p o q = r o q"
1.107      hence "p o (q o inv q)  = r o (q o inv q)" by (simp add: o_assoc)
1.108      with permutes_surj[OF q, unfolded surj_iff]
1.109
```