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.13 +header {*
    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