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.57  proof(auto simp add: inj_on_def)
    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