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
```