summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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