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.                        *)