src/HOL/Library/Permutation.thy
 changeset 11054 a5404c70982f child 11153 950ede59c05a
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Library/Permutation.thy	Sun Feb 04 19:42:54 2001 +0100
1.3 @@ -0,0 +1,199 @@
1.4 +(*  Title:      HOL/Library/Permutation.thy
1.5 +    ID:         \$Id\$
1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1.7 +    Copyright   1995  University of Cambridge
1.8 +
1.9 +TODO: it would be nice to prove (for "multiset", defined on
1.10 +HOL/ex/Sorting.thy) xs <~~> ys = (\<forall>x. multiset xs x = multiset ys x)
1.11 +*)
1.12 +
1.14 + \title{Permutations}
1.15 + \author{Lawrence C Paulson and Thomas M Rasmussen}
1.16 +*}
1.17 +
1.18 +theory Permutation = Main:
1.19 +
1.20 +consts
1.21 +  perm :: "('a list * 'a list) set"
1.22 +
1.23 +syntax
1.24 +  "_perm" :: "'a list => 'a list => bool"    ("_ <~~> _"  [50, 50] 50)
1.25 +translations
1.26 +  "x <~~> y" == "(x, y) \<in> perm"
1.27 +
1.28 +inductive perm
1.29 +  intros [intro]
1.30 +    Nil: "[] <~~> []"
1.31 +    swap: "y # x # l <~~> x # y # l"
1.32 +    Cons: "xs <~~> ys ==> z # xs <~~> z # ys"
1.33 +    trans: "xs <~~> ys ==> ys <~~> zs ==> xs <~~> zs"
1.34 +
1.35 +lemma perm_refl [iff]: "l <~~> l"
1.36 +  apply (induct l)
1.37 +   apply auto
1.38 +  done
1.39 +
1.40 +
1.41 +subsection {* Some examples of rule induction on permutations *}
1.42 +
1.43 +lemma xperm_empty_imp_aux: "xs <~~> ys ==> xs = [] --> ys = []"
1.44 +    -- {* the form of the premise lets the induction bind @{term xs} and @{term ys} *}
1.45 +  apply (erule perm.induct)
1.46 +     apply (simp_all (no_asm_simp))
1.47 +  done
1.48 +
1.49 +lemma xperm_empty_imp: "[] <~~> ys ==> ys = []"
1.50 +  apply (insert xperm_empty_imp_aux)
1.51 +  apply blast
1.52 +  done
1.53 +
1.54 +
1.55 +text {*
1.56 +  \medskip This more general theorem is easier to understand!
1.57 +  *}
1.58 +
1.59 +lemma perm_length: "xs <~~> ys ==> length xs = length ys"
1.60 +  apply (erule perm.induct)
1.61 +     apply simp_all
1.62 +  done
1.63 +
1.64 +lemma perm_empty_imp: "[] <~~> xs ==> xs = []"
1.65 +  apply (drule perm_length)
1.66 +  apply auto
1.67 +  done
1.68 +
1.69 +lemma perm_sym: "xs <~~> ys ==> ys <~~> xs"
1.70 +  apply (erule perm.induct)
1.71 +     apply auto
1.72 +  done
1.73 +
1.74 +lemma perm_mem [rule_format]: "xs <~~> ys ==> x mem xs --> x mem ys"
1.75 +  apply (erule perm.induct)
1.76 +     apply auto
1.77 +  done
1.78 +
1.79 +
1.80 +subsection {* Ways of making new permutations *}
1.81 +
1.82 +text {*
1.83 +  We can insert the head anywhere in the list.
1.84 +*}
1.85 +
1.86 +lemma perm_append_Cons: "a # xs @ ys <~~> xs @ a # ys"
1.87 +  apply (induct xs)
1.88 +   apply auto
1.89 +  done
1.90 +
1.91 +lemma perm_append_swap: "xs @ ys <~~> ys @ xs"
1.92 +  apply (induct xs)
1.93 +    apply simp_all
1.94 +  apply (blast intro: perm_append_Cons)
1.95 +  done
1.96 +
1.97 +lemma perm_append_single: "a # xs <~~> xs @ [a]"
1.98 +  apply (rule perm.trans)
1.99 +   prefer 2
1.100 +   apply (rule perm_append_swap)
1.101 +  apply simp
1.102 +  done
1.103 +
1.104 +lemma perm_rev: "rev xs <~~> xs"
1.105 +  apply (induct xs)
1.106 +   apply simp_all
1.107 +  apply (blast intro: perm_sym perm_append_single)
1.108 +  done
1.109 +
1.110 +lemma perm_append1: "xs <~~> ys ==> l @ xs <~~> l @ ys"
1.111 +  apply (induct l)
1.112 +   apply auto
1.113 +  done
1.114 +
1.115 +lemma perm_append2: "xs <~~> ys ==> xs @ l <~~> ys @ l"
1.116 +  apply (blast intro!: perm_append_swap perm_append1)
1.117 +  done
1.118 +
1.119 +
1.120 +subsection {* Further results *}
1.121 +
1.122 +lemma perm_empty [iff]: "([] <~~> xs) = (xs = [])"
1.123 +  apply (blast intro: perm_empty_imp)
1.124 +  done
1.125 +
1.126 +lemma perm_empty2 [iff]: "(xs <~~> []) = (xs = [])"
1.127 +  apply auto
1.128 +  apply (erule perm_sym [THEN perm_empty_imp])
1.129 +  done
1.130 +
1.131 +lemma perm_sing_imp [rule_format]: "ys <~~> xs ==> xs = [y] --> ys = [y]"
1.132 +  apply (erule perm.induct)
1.133 +     apply auto
1.134 +  done
1.135 +
1.136 +lemma perm_sing_eq [iff]: "(ys <~~> [y]) = (ys = [y])"
1.137 +  apply (blast intro: perm_sing_imp)
1.138 +  done
1.139 +
1.140 +lemma perm_sing_eq2 [iff]: "([y] <~~> ys) = (ys = [y])"
1.141 +  apply (blast dest: perm_sym)
1.142 +  done
1.143 +
1.144 +
1.145 +subsection {* Removing elements *}
1.146 +
1.147 +consts
1.148 +  remove :: "'a => 'a list => 'a list"
1.149 +primrec
1.150 +  "remove x [] = []"
1.151 +  "remove x (y # ys) = (if x = y then ys else y # remove x ys)"
1.152 +
1.153 +lemma perm_remove: "x \<in> set ys ==> ys <~~> x # remove x ys"
1.154 +  apply (induct ys)
1.155 +   apply auto
1.156 +  done
1.157 +
1.158 +lemma remove_commute: "remove x (remove y l) = remove y (remove x l)"
1.159 +  apply (induct l)
1.160 +   apply auto
1.161 +  done
1.162 +
1.163 +
1.164 +text {* \medskip Congruence rule *}
1.165 +
1.166 +lemma perm_remove_perm: "xs <~~> ys ==> remove z xs <~~> remove z ys"
1.167 +  apply (erule perm.induct)
1.168 +     apply auto
1.169 +  done
1.170 +
1.171 +lemma remove_hd [simp]: "remove z (z # xs) = xs"
1.172 +  apply auto
1.173 +  done
1.174 +
1.175 +lemma cons_perm_imp_perm: "z # xs <~~> z # ys ==> xs <~~> ys"
1.176 +  apply (drule_tac z = z in perm_remove_perm)
1.177 +  apply auto
1.178 +  done
1.179 +
1.180 +lemma cons_perm_eq [iff]: "(z#xs <~~> z#ys) = (xs <~~> ys)"
1.181 +  apply (blast intro: cons_perm_imp_perm)
1.182 +  done
1.183 +
1.184 +lemma append_perm_imp_perm: "!!xs ys. zs @ xs <~~> zs @ ys ==> xs <~~> ys"
1.185 +  apply (induct zs rule: rev_induct)
1.186 +   apply (simp_all (no_asm_use))
1.187 +  apply blast
1.188 +  done
1.189 +
1.190 +lemma perm_append1_eq [iff]: "(zs @ xs <~~> zs @ ys) = (xs <~~> ys)"
1.191 +  apply (blast intro: append_perm_imp_perm perm_append1)
1.192 +  done
1.193 +
1.194 +lemma perm_append2_eq [iff]: "(xs @ zs <~~> ys @ zs) = (xs <~~> ys)"
1.195 +  apply (safe intro!: perm_append2)
1.196 +  apply (rule append_perm_imp_perm)
1.197 +  apply (rule perm_append_swap [THEN perm.trans])
1.198 +    -- {* the previous step helps this @{text blast} call succeed quickly *}
1.199 +  apply (blast intro: perm_append_swap)
1.200 +  done
1.201 +
1.202 +end
```