src/HOL/Library/Permutations.thy
 changeset 33715 8cce3a34c122 parent 33057 764547b68538 child 34102 d397496894c4
```     1.1 --- a/src/HOL/Library/Permutations.thy	Mon Nov 16 15:06:34 2009 +0100
1.2 +++ b/src/HOL/Library/Permutations.thy	Mon Nov 16 15:03:23 2009 +0100
1.3 @@ -152,78 +152,66 @@
1.4    thus ?thesis by auto
1.5  qed
1.6
1.7 -lemma hassize_insert: "a \<notin> F \<Longrightarrow> insert a F hassize n \<Longrightarrow> F hassize (n - 1)"
1.8 -  by (auto simp add: hassize_def)
1.9 -
1.10 -lemma hassize_permutations: assumes Sn: "S hassize n"
1.11 -  shows "{p. p permutes S} hassize (fact n)"
1.12 -proof-
1.13 -  from Sn have fS:"finite S" by (simp add: hassize_def)
1.14 -
1.15 -  have "\<forall>n. (S hassize n) \<longrightarrow> ({p. p permutes S} hassize (fact n))"
1.16 -  proof(rule finite_induct[where F = S])
1.17 -    from fS show "finite S" .
1.18 -  next
1.19 -    show "\<forall>n. ({} hassize n) \<longrightarrow> ({p. p permutes {}} hassize fact n)"
1.20 -      by (simp add: hassize_def permutes_empty)
1.21 -  next
1.22 -    fix x F
1.23 -    assume fF: "finite F" and xF: "x \<notin> F"
1.24 -      and H: "\<forall>n. (F hassize n) \<longrightarrow> ({p. p permutes F} hassize fact n)"
1.25 -    {fix n assume H0: "insert x F hassize n"
1.26 -      let ?xF = "{p. p permutes insert x F}"
1.27 -      let ?pF = "{p. p permutes F}"
1.28 -      let ?pF' = "{(b, p). b \<in> insert x F \<and> p \<in> ?pF}"
1.29 -      let ?g = "(\<lambda>(b, p). Fun.swap x b id \<circ> p)"
1.30 -      from permutes_insert[of x F]
1.31 -      have xfgpF': "?xF = ?g ` ?pF'" .
1.32 -      from hassize_insert[OF xF H0] have Fs: "F hassize (n - 1)" .
1.33 -      from H Fs have pFs: "?pF hassize fact (n - 1)" by blast
1.34 -      hence pF'f: "finite ?pF'" using H0 unfolding hassize_def
1.35 -        apply (simp only: Collect_split Collect_mem_eq)
1.36 -        apply (rule finite_cartesian_product)
1.37 -        apply simp_all
1.38 -        done
1.39 +lemma card_permutations: assumes Sn: "card S = n" and fS: "finite S"
1.40 +  shows "card {p. p permutes S} = fact n"
1.41 +using fS Sn proof (induct arbitrary: n)
1.42 +  case empty thus ?case by (simp add: permutes_empty)
1.43 +next
1.44 +  case (insert x F)
1.45 +  { fix n assume H0: "card (insert x F) = n"
1.46 +    let ?xF = "{p. p permutes insert x F}"
1.47 +    let ?pF = "{p. p permutes F}"
1.48 +    let ?pF' = "{(b, p). b \<in> insert x F \<and> p \<in> ?pF}"
1.49 +    let ?g = "(\<lambda>(b, p). Fun.swap x b id \<circ> p)"
1.50 +    from permutes_insert[of x F]
1.51 +    have xfgpF': "?xF = ?g ` ?pF'" .
1.52 +    have Fs: "card F = n - 1" using `x \<notin> F` H0 `finite F` by auto
1.53 +    from insert.hyps Fs have pFs: "card ?pF = fact (n - 1)" using `finite F` by auto
1.54 +    moreover hence "finite ?pF" using fact_gt_zero_nat by (auto intro: card_ge_0_finite)
1.55 +    ultimately have pF'f: "finite ?pF'" using H0 `finite F`
1.56 +      apply (simp only: Collect_split Collect_mem_eq)
1.57 +      apply (rule finite_cartesian_product)
1.58 +      apply simp_all
1.59 +      done
1.60
1.61 -      have ginj: "inj_on ?g ?pF'"
1.62 -      proof-
1.63 -        {
1.64 -          fix b p c q assume bp: "(b,p) \<in> ?pF'" and cq: "(c,q) \<in> ?pF'"
1.65 -            and eq: "?g (b,p) = ?g (c,q)"
1.66 -          from bp cq have ths: "b \<in> insert x F" "c \<in> insert x F" "x \<in> insert x F" "p permutes F" "q permutes F" by auto
1.67 -          from ths(4) xF eq have "b = ?g (b,p) x" unfolding permutes_def
1.68 -            by (auto simp add: swap_def fun_upd_def expand_fun_eq)
1.69 -          also have "\<dots> = ?g (c,q) x" using ths(5) xF eq
1.70 -            by (auto simp add: swap_def fun_upd_def expand_fun_eq)
1.71 -          also have "\<dots> = c"using ths(5) xF unfolding permutes_def
1.72 -            by (auto simp add: swap_def fun_upd_def expand_fun_eq)
1.73 -          finally have bc: "b = c" .
1.74 -          hence "Fun.swap x b id = Fun.swap x c id" by simp
1.75 -          with eq have "Fun.swap x b id o p = Fun.swap x b id o q" by simp
1.76 -          hence "Fun.swap x b id o (Fun.swap x b id o p) = Fun.swap x b id o (Fun.swap x b id o q)" by simp
1.77 -          hence "p = q" by (simp add: o_assoc)
1.78 -          with bc have "(b,p) = (c,q)" by simp }
1.79 -        thus ?thesis  unfolding inj_on_def by blast
1.80 -      qed
1.81 -      from xF H0 have n0: "n \<noteq> 0 " by (auto simp add: hassize_def)
1.82 -      hence "\<exists>m. n = Suc m" by arith
1.83 -      then obtain m where n[simp]: "n = Suc m" by blast
1.84 -      from pFs H0 have xFc: "card ?xF = fact n"
1.85 -        unfolding xfgpF' card_image[OF ginj] hassize_def
1.86 -        apply (simp only: Collect_split Collect_mem_eq card_cartesian_product)
1.87 -        by simp
1.88 -      from finite_imageI[OF pF'f, of ?g] have xFf: "finite ?xF" unfolding xfgpF' by simp
1.89 -      have "?xF hassize fact n"
1.90 -        using xFf xFc
1.91 -        unfolding hassize_def  xFf by blast }
1.92 -    thus "\<forall>n. (insert x F hassize n) \<longrightarrow> ({p. p permutes insert x F} hassize fact n)"
1.93 -      by blast
1.94 -  qed
1.95 -  with Sn show ?thesis by blast
1.96 +    have ginj: "inj_on ?g ?pF'"
1.97 +    proof-
1.98 +      {
1.99 +        fix b p c q assume bp: "(b,p) \<in> ?pF'" and cq: "(c,q) \<in> ?pF'"
1.100 +          and eq: "?g (b,p) = ?g (c,q)"
1.101 +        from bp cq have ths: "b \<in> insert x F" "c \<in> insert x F" "x \<in> insert x F" "p permutes F" "q permutes F" by auto
1.102 +        from ths(4) `x \<notin> F` eq have "b = ?g (b,p) x" unfolding permutes_def
1.103 +          by (auto simp add: swap_def fun_upd_def expand_fun_eq)
1.104 +        also have "\<dots> = ?g (c,q) x" using ths(5) `x \<notin> F` eq
1.105 +          by (auto simp add: swap_def fun_upd_def expand_fun_eq)
1.106 +        also have "\<dots> = c"using ths(5) `x \<notin> F` unfolding permutes_def
1.107 +          by (auto simp add: swap_def fun_upd_def expand_fun_eq)
1.108 +        finally have bc: "b = c" .
1.109 +        hence "Fun.swap x b id = Fun.swap x c id" by simp
1.110 +        with eq have "Fun.swap x b id o p = Fun.swap x b id o q" by simp
1.111 +        hence "Fun.swap x b id o (Fun.swap x b id o p) = Fun.swap x b id o (Fun.swap x b id o q)" by simp
1.112 +        hence "p = q" by (simp add: o_assoc)
1.113 +        with bc have "(b,p) = (c,q)" by simp
1.114 +      }
1.115 +      thus ?thesis  unfolding inj_on_def by blast
1.116 +    qed
1.117 +    from `x \<notin> F` H0 have n0: "n \<noteq> 0 " using `finite F` by auto
1.118 +    hence "\<exists>m. n = Suc m" by arith
1.119 +    then obtain m where n[simp]: "n = Suc m" by blast
1.120 +    from pFs H0 have xFc: "card ?xF = fact n"
1.121 +      unfolding xfgpF' card_image[OF ginj] using `finite F` `finite ?pF`
1.122 +      apply (simp only: Collect_split Collect_mem_eq card_cartesian_product)
1.123 +      by simp
1.124 +    from finite_imageI[OF pF'f, of ?g] have xFf: "finite ?xF" unfolding xfgpF' by simp
1.125 +    have "card ?xF = fact n"
1.126 +      using xFf xFc unfolding xFf by blast
1.127 +  }
1.128 +  thus ?case using insert by simp
1.129  qed
1.130
1.131 -lemma finite_permutations: "finite S ==> finite {p. p permutes S}"
1.132 -  using hassize_permutations[of S] unfolding hassize_def by blast
1.133 +lemma finite_permutations: assumes fS: "finite S" shows "finite {p. p permutes S}"
1.134 +  using card_permutations[OF refl fS] fact_gt_zero_nat
1.135 +  by (auto intro: card_ge_0_finite)
1.136
1.137  (* ------------------------------------------------------------------------- *)
1.138  (* Permutations of index set for iterated operations.                        *)
```