src/HOL/Library/Permutations.thy
changeset 32960 69916a850301
parent 32456 341c83339aeb
child 32989 c28279b29ff1
     1.1 --- a/src/HOL/Library/Permutations.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOL/Library/Permutations.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -181,42 +181,42 @@
     1.4        from hassize_insert[OF xF H0] have Fs: "F hassize (n - 1)" .
     1.5        from H Fs have pFs: "?pF hassize fact (n - 1)" by blast
     1.6        hence pF'f: "finite ?pF'" using H0 unfolding hassize_def
     1.7 -	apply (simp only: Collect_split Collect_mem_eq)
     1.8 -	apply (rule finite_cartesian_product)
     1.9 -	apply simp_all
    1.10 -	done
    1.11 +        apply (simp only: Collect_split Collect_mem_eq)
    1.12 +        apply (rule finite_cartesian_product)
    1.13 +        apply simp_all
    1.14 +        done
    1.15  
    1.16        have ginj: "inj_on ?g ?pF'"
    1.17        proof-
    1.18 -	{
    1.19 -	  fix b p c q assume bp: "(b,p) \<in> ?pF'" and cq: "(c,q) \<in> ?pF'"
    1.20 -	    and eq: "?g (b,p) = ?g (c,q)"
    1.21 -	  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.22 -	  from ths(4) xF eq have "b = ?g (b,p) x" unfolding permutes_def
    1.23 -	    by (auto simp add: swap_def fun_upd_def expand_fun_eq)
    1.24 -	  also have "\<dots> = ?g (c,q) x" using ths(5) xF eq
    1.25 -	    by (auto simp add: swap_def fun_upd_def expand_fun_eq)
    1.26 -	  also have "\<dots> = c"using ths(5) xF unfolding permutes_def
    1.27 -	    by (auto simp add: swap_def fun_upd_def expand_fun_eq)
    1.28 -	  finally have bc: "b = c" .
    1.29 -	  hence "Fun.swap x b id = Fun.swap x c id" by simp
    1.30 -	  with eq have "Fun.swap x b id o p = Fun.swap x b id o q" by simp
    1.31 -	  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.32 -	  hence "p = q" by (simp add: o_assoc)
    1.33 -	  with bc have "(b,p) = (c,q)" by simp }
    1.34 -	thus ?thesis  unfolding inj_on_def by blast
    1.35 +        {
    1.36 +          fix b p c q assume bp: "(b,p) \<in> ?pF'" and cq: "(c,q) \<in> ?pF'"
    1.37 +            and eq: "?g (b,p) = ?g (c,q)"
    1.38 +          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.39 +          from ths(4) xF eq have "b = ?g (b,p) x" unfolding permutes_def
    1.40 +            by (auto simp add: swap_def fun_upd_def expand_fun_eq)
    1.41 +          also have "\<dots> = ?g (c,q) x" using ths(5) xF eq
    1.42 +            by (auto simp add: swap_def fun_upd_def expand_fun_eq)
    1.43 +          also have "\<dots> = c"using ths(5) xF unfolding permutes_def
    1.44 +            by (auto simp add: swap_def fun_upd_def expand_fun_eq)
    1.45 +          finally have bc: "b = c" .
    1.46 +          hence "Fun.swap x b id = Fun.swap x c id" by simp
    1.47 +          with eq have "Fun.swap x b id o p = Fun.swap x b id o q" by simp
    1.48 +          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.49 +          hence "p = q" by (simp add: o_assoc)
    1.50 +          with bc have "(b,p) = (c,q)" by simp }
    1.51 +        thus ?thesis  unfolding inj_on_def by blast
    1.52        qed
    1.53        from xF H0 have n0: "n \<noteq> 0 " by (auto simp add: hassize_def)
    1.54        hence "\<exists>m. n = Suc m" by arith
    1.55        then obtain m where n[simp]: "n = Suc m" by blast
    1.56        from pFs H0 have xFc: "card ?xF = fact n"
    1.57 -	unfolding xfgpF' card_image[OF ginj] hassize_def
    1.58 -	apply (simp only: Collect_split Collect_mem_eq card_cartesian_product)
    1.59 -	by simp
    1.60 +        unfolding xfgpF' card_image[OF ginj] hassize_def
    1.61 +        apply (simp only: Collect_split Collect_mem_eq card_cartesian_product)
    1.62 +        by simp
    1.63        from finite_imageI[OF pF'f, of ?g] have xFf: "finite ?xF" unfolding xfgpF' by simp
    1.64        have "?xF hassize fact n"
    1.65 -	using xFf xFc
    1.66 -	unfolding hassize_def  xFf by blast }
    1.67 +        using xFf xFc
    1.68 +        unfolding hassize_def  xFf by blast }
    1.69      thus "\<forall>n. (insert x F hassize n) \<longrightarrow> ({p. p permutes insert x F} hassize fact n)"
    1.70        by blast
    1.71    qed
    1.72 @@ -689,17 +689,17 @@
    1.73        using p le
    1.74      proof(induct n arbitrary: S rule: less_induct)
    1.75        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.76 -	"p permutes S" "\<forall>i \<in>S. p i \<le> i"
    1.77 +        "p permutes S" "\<forall>i \<in>S. p i \<le> i"
    1.78        {assume "n \<notin> S"
    1.79 -	with H(2) have "p n = n" unfolding permutes_def by metis}
    1.80 +        with H(2) have "p n = n" unfolding permutes_def by metis}
    1.81        moreover
    1.82        {assume ns: "n \<in> S"
    1.83 -	from H(3)  ns have "p n < n \<or> p n = n" by auto
    1.84 -	moreover{assume h: "p n < n"
    1.85 -	  from H h have "p (p n) = p n" by metis
    1.86 -	  with permutes_inj[OF H(2)] have "p n = n" unfolding inj_on_def by blast
    1.87 -	  with h have False by simp}
    1.88 -	ultimately have "p n = n" by blast }
    1.89 +        from H(3)  ns have "p n < n \<or> p n = n" by auto
    1.90 +        moreover{assume h: "p n < n"
    1.91 +          from H h have "p (p n) = p n" by metis
    1.92 +          with permutes_inj[OF H(2)] have "p n = n" unfolding inj_on_def by blast
    1.93 +          with h have False by simp}
    1.94 +        ultimately have "p n = n" by blast }
    1.95        ultimately show "p n = n"  by blast
    1.96      qed}
    1.97    thus ?thesis by (auto simp add: expand_fun_eq)
    1.98 @@ -840,13 +840,13 @@
    1.99        and p: "p permutes S" and q: "q permutes S"
   1.100        and eq: "Fun.swap a b id o p = Fun.swap a c id o q"
   1.101        from p q aS have pa: "p a = a" and qa: "q a = a"
   1.102 -	unfolding permutes_def by metis+
   1.103 +        unfolding permutes_def by metis+
   1.104        from eq have "(Fun.swap a b id o p) a  = (Fun.swap a c id o q) a" by simp
   1.105        hence bc: "b = c"
   1.106 -	by (simp add: permutes_def pa qa o_def fun_upd_def swap_def id_def cong del: if_weak_cong split: split_if_asm)
   1.107 +        by (simp add: permutes_def pa qa o_def fun_upd_def swap_def id_def cong del: if_weak_cong split: split_if_asm)
   1.108        from eq[unfolded bc] have "(\<lambda>p. Fun.swap a c id o p) (Fun.swap a c id o p) = (\<lambda>p. Fun.swap a c id o p) (Fun.swap a c id o q)" by simp
   1.109        hence "p = q" unfolding o_assoc swap_id_idempotent
   1.110 -	by (simp add: o_def)
   1.111 +        by (simp add: o_def)
   1.112        with bc have "b = c \<and> p = q" by blast
   1.113      }
   1.114