moved from Induct/ to Library/
authorwenzelm
Sun Feb 04 19:42:54 2001 +0100 (2001-02-04)
changeset 11054a5404c70982f
parent 11053 026007eb2ccc
child 11055 b84dd2c25a1c
moved from Induct/ to Library/
src/HOL/Induct/Perm.ML
src/HOL/Induct/Perm.thy
src/HOL/Library/Permutation.thy
     1.1 --- a/src/HOL/Induct/Perm.ML	Sun Feb 04 19:41:47 2001 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,165 +0,0 @@
     1.4 -(*  Title:      HOL/ex/Perm.ML
     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 -Permutations: example of an inductive definition
    1.10 -*)
    1.11 -
    1.12 -(*It would be nice to prove (for "multiset", defined on HOL/ex/Sorting.thy)
    1.13 -    xs <~~> ys = (ALL x. multiset xs x = multiset ys x)
    1.14 -*)
    1.15 -
    1.16 -AddIs perm.intrs;
    1.17 -
    1.18 -Goal "l <~~> l";
    1.19 -by (induct_tac "l" 1);
    1.20 -by Auto_tac;
    1.21 -qed "perm_refl";
    1.22 -AddIffs [perm_refl];
    1.23 -
    1.24 -(** Some examples of rule induction on permutations **)
    1.25 -
    1.26 -(*The form of the premise lets the induction bind xs and ys.*)
    1.27 -Goal "xs <~~> ys ==> xs=[] --> ys=[]";
    1.28 -by (etac perm.induct 1);
    1.29 -by (ALLGOALS Asm_simp_tac);
    1.30 -bind_thm ("xperm_empty_imp",    (* [] <~~> ys ==> ys=[] *)
    1.31 -	  [refl, result()] MRS rev_mp);
    1.32 -
    1.33 -(*This more general theorem is easier to understand!*)
    1.34 -Goal "xs <~~> ys ==> length(xs) = length(ys)";
    1.35 -by (etac perm.induct 1);
    1.36 -by (ALLGOALS Asm_simp_tac);
    1.37 -qed "perm_length";
    1.38 -
    1.39 -Goal "[] <~~> xs ==> xs=[]";
    1.40 -by (dtac perm_length 1);
    1.41 -by Auto_tac;
    1.42 -qed "perm_empty_imp";
    1.43 -
    1.44 -Goal "xs <~~> ys ==> ys <~~> xs";
    1.45 -by (etac perm.induct 1);
    1.46 -by Auto_tac;
    1.47 -qed "perm_sym";
    1.48 -
    1.49 -Goal "xs <~~> ys ==> x mem xs --> x mem ys";
    1.50 -by (etac perm.induct 1);
    1.51 -by Auto_tac;
    1.52 -val perm_mem_lemma = result();
    1.53 -
    1.54 -bind_thm ("perm_mem", perm_mem_lemma RS mp);
    1.55 -
    1.56 -(** Ways of making new permutations **)
    1.57 -
    1.58 -(*We can insert the head anywhere in the list*)
    1.59 -Goal "a # xs @ ys <~~> xs @ a # ys";
    1.60 -by (induct_tac "xs" 1);
    1.61 -by Auto_tac;
    1.62 -qed "perm_append_Cons";
    1.63 -
    1.64 -Goal "xs@ys <~~> ys@xs";
    1.65 -by (induct_tac "xs" 1);
    1.66 -by (ALLGOALS Simp_tac);
    1.67 -by (blast_tac (claset() addIs [perm_append_Cons]) 1);
    1.68 -qed "perm_append_swap";
    1.69 -
    1.70 -Goal "a # xs <~~> xs @ [a]";
    1.71 -by (rtac perm.trans 1);
    1.72 -by (rtac perm_append_swap 2);
    1.73 -by (Simp_tac 1);
    1.74 -qed "perm_append_single";
    1.75 -
    1.76 -Goal "rev xs <~~> xs";
    1.77 -by (induct_tac "xs" 1);
    1.78 -by (ALLGOALS Simp_tac);
    1.79 -by (blast_tac (claset() addIs [perm_sym, perm_append_single]) 1);
    1.80 -qed "perm_rev";
    1.81 -
    1.82 -Goal "xs <~~> ys ==> l@xs <~~> l@ys";
    1.83 -by (induct_tac "l" 1);
    1.84 -by Auto_tac;
    1.85 -qed "perm_append1";
    1.86 -
    1.87 -Goal "xs <~~> ys ==> xs@l <~~> ys@l";
    1.88 -by (blast_tac (claset() addSIs [perm_append_swap, perm_append1]) 1);
    1.89 -qed "perm_append2";
    1.90 -
    1.91 -(** Further results mostly by Thomas Marthedal Rasmussen **)
    1.92 -
    1.93 -Goal "([] <~~> xs) = (xs = [])";
    1.94 -by (blast_tac (claset() addIs [perm_empty_imp]) 1);
    1.95 -qed "perm_empty";
    1.96 -AddIffs [perm_empty];
    1.97 -
    1.98 -Goal "(xs <~~> []) = (xs = [])";
    1.99 -by Auto_tac;
   1.100 -by (etac (perm_sym RS perm_empty_imp) 1);
   1.101 -qed "perm_empty2";
   1.102 -AddIffs [perm_empty2];
   1.103 -
   1.104 -Goal "ys <~~> xs ==> xs=[y] --> ys=[y]";
   1.105 -by (etac perm.induct 1);
   1.106 -by Auto_tac;
   1.107 -qed_spec_mp "perm_sing_imp";
   1.108 -
   1.109 -Goal "(ys <~~> [y]) = (ys = [y])"; 
   1.110 -by (blast_tac (claset() addIs [perm_sing_imp]) 1);
   1.111 -qed "perm_sing_eq";
   1.112 -AddIffs [perm_sing_eq];
   1.113 -
   1.114 -Goal "([y] <~~> ys) = (ys = [y])"; 
   1.115 -by (blast_tac (claset() addDs [perm_sym]) 1);
   1.116 -qed "perm_sing_eq2";
   1.117 -AddIffs [perm_sing_eq2];
   1.118 -
   1.119 -Goal "x:set ys --> ys <~~> x#(remove x ys)";
   1.120 -by (induct_tac "ys" 1);
   1.121 -by Auto_tac;
   1.122 -qed_spec_mp "perm_remove"; 
   1.123 -
   1.124 -Goal "remove x (remove y l) = remove y (remove x l)";
   1.125 -by (induct_tac "l" 1);
   1.126 -by Auto_tac;
   1.127 -qed "remove_commute";
   1.128 -
   1.129 -(*Congruence rule*)
   1.130 -Goal "xs <~~> ys ==> remove z xs <~~> remove z ys";
   1.131 -by (etac perm.induct 1);
   1.132 -by Auto_tac;
   1.133 -qed "perm_remove_perm";
   1.134 -
   1.135 -Goal "remove z (z#xs) = xs";
   1.136 -by Auto_tac;
   1.137 -qed "remove_hd";
   1.138 -Addsimps [remove_hd];
   1.139 -
   1.140 -Goal "z#xs <~~> z#ys ==> xs <~~> ys";
   1.141 -by (dres_inst_tac [("z","z")] perm_remove_perm 1);
   1.142 -by Auto_tac;
   1.143 -qed "cons_perm_imp_perm";
   1.144 -
   1.145 -Goal "(z#xs <~~> z#ys) = (xs <~~> ys)";
   1.146 -by (blast_tac (claset() addIs [cons_perm_imp_perm]) 1);
   1.147 -qed "cons_perm_eq";
   1.148 -AddIffs [cons_perm_eq];
   1.149 -
   1.150 -Goal "ALL xs ys. zs@xs <~~> zs@ys --> xs <~~> ys";
   1.151 -by (rev_induct_tac "zs" 1);
   1.152 -by (ALLGOALS Full_simp_tac);
   1.153 -by (Blast_tac 1);
   1.154 -qed_spec_mp "append_perm_imp_perm";
   1.155 -
   1.156 -Goal "(zs@xs <~~> zs@ys) = (xs <~~> ys)";
   1.157 -by (blast_tac (claset() addIs [append_perm_imp_perm, perm_append1]) 1);
   1.158 -qed "perm_append1_eq";
   1.159 -AddIffs [perm_append1_eq];
   1.160 -
   1.161 -Goal "(xs@zs <~~> ys@zs) = (xs <~~> ys)";
   1.162 -by (safe_tac (claset() addSIs [perm_append2]));
   1.163 -by (rtac append_perm_imp_perm 1);
   1.164 -by (rtac (perm_append_swap RS perm.trans) 1);
   1.165 -(*The previous step helps this blast_tac call succeed quickly.*)
   1.166 -by (blast_tac (claset() addIs [perm_append_swap]) 1);
   1.167 -qed "perm_append2_eq";
   1.168 -AddIffs [perm_append2_eq];
     2.1 --- a/src/HOL/Induct/Perm.thy	Sun Feb 04 19:41:47 2001 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,32 +0,0 @@
     2.4 -(*  Title:      HOL/ex/Perm.thy
     2.5 -    ID:         $Id$
     2.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 -    Copyright   1995  University of Cambridge
     2.8 -
     2.9 -Permutations: example of an inductive definition
    2.10 -*)
    2.11 -
    2.12 -Perm = Main +
    2.13 -
    2.14 -consts  perm    :: "('a list * 'a list) set"   
    2.15 -syntax "@perm"  :: ['a list, 'a list] => bool ("_ <~~> _"  [50,50] 50)
    2.16 -
    2.17 -translations
    2.18 -    "x <~~> y" == "(x,y) : perm"
    2.19 -
    2.20 -inductive perm
    2.21 -  intrs
    2.22 -    Nil   "[] <~~> []"
    2.23 -    swap  "y#x#l <~~> x#y#l"
    2.24 -    Cons  "xs <~~> ys ==> z#xs <~~> z#ys"
    2.25 -    trans "[| xs <~~> ys;  ys <~~> zs |] ==> xs <~~> zs"
    2.26 -
    2.27 -
    2.28 -consts
    2.29 -  remove  :: ['a, 'a list] => 'a list
    2.30 -
    2.31 -primrec 
    2.32 -  "remove x []     = []"
    2.33 -  "remove x (y#ys) = (if x=y then ys else y#remove x ys)"
    2.34 -
    2.35 -end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/Permutation.thy	Sun Feb 04 19:42:54 2001 +0100
     3.3 @@ -0,0 +1,199 @@
     3.4 +(*  Title:      HOL/Library/Permutation.thy
     3.5 +    ID:         $Id$
     3.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 +    Copyright   1995  University of Cambridge
     3.8 +
     3.9 +TODO: it would be nice to prove (for "multiset", defined on
    3.10 +HOL/ex/Sorting.thy) xs <~~> ys = (\<forall>x. multiset xs x = multiset ys x)
    3.11 +*)
    3.12 +
    3.13 +header {*
    3.14 + \title{Permutations}
    3.15 + \author{Lawrence C Paulson and Thomas M Rasmussen}
    3.16 +*}
    3.17 +
    3.18 +theory Permutation = Main:
    3.19 +
    3.20 +consts
    3.21 +  perm :: "('a list * 'a list) set"
    3.22 +
    3.23 +syntax
    3.24 +  "_perm" :: "'a list => 'a list => bool"    ("_ <~~> _"  [50, 50] 50)
    3.25 +translations
    3.26 +  "x <~~> y" == "(x, y) \<in> perm"
    3.27 +
    3.28 +inductive perm
    3.29 +  intros [intro]
    3.30 +    Nil: "[] <~~> []"
    3.31 +    swap: "y # x # l <~~> x # y # l"
    3.32 +    Cons: "xs <~~> ys ==> z # xs <~~> z # ys"
    3.33 +    trans: "xs <~~> ys ==> ys <~~> zs ==> xs <~~> zs"
    3.34 +
    3.35 +lemma perm_refl [iff]: "l <~~> l"
    3.36 +  apply (induct l)
    3.37 +   apply auto
    3.38 +  done
    3.39 +
    3.40 +
    3.41 +subsection {* Some examples of rule induction on permutations *}
    3.42 +
    3.43 +lemma xperm_empty_imp_aux: "xs <~~> ys ==> xs = [] --> ys = []"
    3.44 +    -- {* the form of the premise lets the induction bind @{term xs} and @{term ys} *}
    3.45 +  apply (erule perm.induct)
    3.46 +     apply (simp_all (no_asm_simp))
    3.47 +  done
    3.48 +
    3.49 +lemma xperm_empty_imp: "[] <~~> ys ==> ys = []"
    3.50 +  apply (insert xperm_empty_imp_aux)
    3.51 +  apply blast
    3.52 +  done
    3.53 +
    3.54 +
    3.55 +text {*
    3.56 +  \medskip This more general theorem is easier to understand!
    3.57 +  *}
    3.58 +
    3.59 +lemma perm_length: "xs <~~> ys ==> length xs = length ys"
    3.60 +  apply (erule perm.induct)
    3.61 +     apply simp_all
    3.62 +  done
    3.63 +
    3.64 +lemma perm_empty_imp: "[] <~~> xs ==> xs = []"
    3.65 +  apply (drule perm_length)
    3.66 +  apply auto
    3.67 +  done
    3.68 +
    3.69 +lemma perm_sym: "xs <~~> ys ==> ys <~~> xs"
    3.70 +  apply (erule perm.induct)
    3.71 +     apply auto
    3.72 +  done
    3.73 +
    3.74 +lemma perm_mem [rule_format]: "xs <~~> ys ==> x mem xs --> x mem ys"
    3.75 +  apply (erule perm.induct)
    3.76 +     apply auto
    3.77 +  done
    3.78 +
    3.79 +
    3.80 +subsection {* Ways of making new permutations *}
    3.81 +
    3.82 +text {*
    3.83 +  We can insert the head anywhere in the list.
    3.84 +*}
    3.85 +
    3.86 +lemma perm_append_Cons: "a # xs @ ys <~~> xs @ a # ys"
    3.87 +  apply (induct xs)
    3.88 +   apply auto
    3.89 +  done
    3.90 +
    3.91 +lemma perm_append_swap: "xs @ ys <~~> ys @ xs"
    3.92 +  apply (induct xs)
    3.93 +    apply simp_all
    3.94 +  apply (blast intro: perm_append_Cons)
    3.95 +  done
    3.96 +
    3.97 +lemma perm_append_single: "a # xs <~~> xs @ [a]"
    3.98 +  apply (rule perm.trans)
    3.99 +   prefer 2
   3.100 +   apply (rule perm_append_swap)
   3.101 +  apply simp
   3.102 +  done
   3.103 +
   3.104 +lemma perm_rev: "rev xs <~~> xs"
   3.105 +  apply (induct xs)
   3.106 +   apply simp_all
   3.107 +  apply (blast intro: perm_sym perm_append_single)
   3.108 +  done
   3.109 +
   3.110 +lemma perm_append1: "xs <~~> ys ==> l @ xs <~~> l @ ys"
   3.111 +  apply (induct l)
   3.112 +   apply auto
   3.113 +  done
   3.114 +
   3.115 +lemma perm_append2: "xs <~~> ys ==> xs @ l <~~> ys @ l"
   3.116 +  apply (blast intro!: perm_append_swap perm_append1)
   3.117 +  done
   3.118 +
   3.119 +
   3.120 +subsection {* Further results *}
   3.121 +
   3.122 +lemma perm_empty [iff]: "([] <~~> xs) = (xs = [])"
   3.123 +  apply (blast intro: perm_empty_imp)
   3.124 +  done
   3.125 +
   3.126 +lemma perm_empty2 [iff]: "(xs <~~> []) = (xs = [])"
   3.127 +  apply auto
   3.128 +  apply (erule perm_sym [THEN perm_empty_imp])
   3.129 +  done
   3.130 +
   3.131 +lemma perm_sing_imp [rule_format]: "ys <~~> xs ==> xs = [y] --> ys = [y]"
   3.132 +  apply (erule perm.induct)
   3.133 +     apply auto
   3.134 +  done
   3.135 +
   3.136 +lemma perm_sing_eq [iff]: "(ys <~~> [y]) = (ys = [y])"
   3.137 +  apply (blast intro: perm_sing_imp)
   3.138 +  done
   3.139 +
   3.140 +lemma perm_sing_eq2 [iff]: "([y] <~~> ys) = (ys = [y])"
   3.141 +  apply (blast dest: perm_sym)
   3.142 +  done
   3.143 +
   3.144 +
   3.145 +subsection {* Removing elements *}
   3.146 +
   3.147 +consts
   3.148 +  remove :: "'a => 'a list => 'a list"
   3.149 +primrec
   3.150 +  "remove x [] = []"
   3.151 +  "remove x (y # ys) = (if x = y then ys else y # remove x ys)"
   3.152 +
   3.153 +lemma perm_remove: "x \<in> set ys ==> ys <~~> x # remove x ys"
   3.154 +  apply (induct ys)
   3.155 +   apply auto
   3.156 +  done
   3.157 +
   3.158 +lemma remove_commute: "remove x (remove y l) = remove y (remove x l)"
   3.159 +  apply (induct l)
   3.160 +   apply auto
   3.161 +  done
   3.162 +
   3.163 +
   3.164 +text {* \medskip Congruence rule *}
   3.165 +
   3.166 +lemma perm_remove_perm: "xs <~~> ys ==> remove z xs <~~> remove z ys"
   3.167 +  apply (erule perm.induct)
   3.168 +     apply auto
   3.169 +  done
   3.170 +
   3.171 +lemma remove_hd [simp]: "remove z (z # xs) = xs"
   3.172 +  apply auto
   3.173 +  done
   3.174 +
   3.175 +lemma cons_perm_imp_perm: "z # xs <~~> z # ys ==> xs <~~> ys"
   3.176 +  apply (drule_tac z = z in perm_remove_perm)
   3.177 +  apply auto
   3.178 +  done
   3.179 +
   3.180 +lemma cons_perm_eq [iff]: "(z#xs <~~> z#ys) = (xs <~~> ys)"
   3.181 +  apply (blast intro: cons_perm_imp_perm)
   3.182 +  done
   3.183 +
   3.184 +lemma append_perm_imp_perm: "!!xs ys. zs @ xs <~~> zs @ ys ==> xs <~~> ys"
   3.185 +  apply (induct zs rule: rev_induct)
   3.186 +   apply (simp_all (no_asm_use))
   3.187 +  apply blast
   3.188 +  done
   3.189 +
   3.190 +lemma perm_append1_eq [iff]: "(zs @ xs <~~> zs @ ys) = (xs <~~> ys)"
   3.191 +  apply (blast intro: append_perm_imp_perm perm_append1)
   3.192 +  done
   3.193 +
   3.194 +lemma perm_append2_eq [iff]: "(xs @ zs <~~> ys @ zs) = (xs <~~> ys)"
   3.195 +  apply (safe intro!: perm_append2)
   3.196 +  apply (rule append_perm_imp_perm)
   3.197 +  apply (rule perm_append_swap [THEN perm.trans])
   3.198 +    -- {* the previous step helps this @{text blast} call succeed quickly *}
   3.199 +  apply (blast intro: perm_append_swap)
   3.200 +  done
   3.201 +
   3.202 +end