src/HOL/Library/Permutation.thy
 changeset 25379 12bcf37252b1 parent 25287 094dab519ff5 child 26072 f65a7fa2da6c
equal inserted replaced
25378:dca691610489 25379:12bcf37252b1
20   by (induct l) auto
20   by (induct l) auto
21
21
22
22
23 subsection {* Some examples of rule induction on permutations *}
23 subsection {* Some examples of rule induction on permutations *}
24
24
32 lemma xperm_empty_imp: "[] <~~> ys ==> ys = []"
25 lemma xperm_empty_imp: "[] <~~> ys ==> ys = []"
33   using xperm_empty_imp_aux by blast
26   by (induct xs == "[]::'a list" ys pred: perm) simp_all
34
27
35
28
36 text {*
29 text {*
37   \medskip This more general theorem is easier to understand!
30   \medskip This more general theorem is easier to understand!
38   *}
31   *}
39
32
40 lemma perm_length: "xs <~~> ys ==> length xs = length ys"
33 lemma perm_length: "xs <~~> ys ==> length xs = length ys"
41   by (erule perm.induct) simp_all
34   by (induct pred: perm) simp_all
42
35
43 lemma perm_empty_imp: "[] <~~> xs ==> xs = []"
36 lemma perm_empty_imp: "[] <~~> xs ==> xs = []"
44   by (drule perm_length) auto
37   by (drule perm_length) auto
45
38
46 lemma perm_sym: "xs <~~> ys ==> ys <~~> xs"
39 lemma perm_sym: "xs <~~> ys ==> ys <~~> xs"
47   by (erule perm.induct) auto
40   by (induct pred: perm) auto
48
41
49
42
50 subsection {* Ways of making new permutations *}
43 subsection {* Ways of making new permutations *}
51
44
52 text {*
45 text {*
86 lemma perm_empty2 [iff]: "(xs <~~> []) = (xs = [])"
79 lemma perm_empty2 [iff]: "(xs <~~> []) = (xs = [])"
87   apply auto
80   apply auto
88   apply (erule perm_sym [THEN perm_empty_imp])
81   apply (erule perm_sym [THEN perm_empty_imp])
89   done
82   done
90
83
91 lemma perm_sing_imp [rule_format]: "ys <~~> xs ==> xs = [y] --> ys = [y]"
84 lemma perm_sing_imp: "ys <~~> xs ==> xs = [y] ==> ys = [y]"
92   by (erule perm.induct) auto
85   by (induct pred: perm) auto
93
86
94 lemma perm_sing_eq [iff]: "(ys <~~> [y]) = (ys = [y])"
87 lemma perm_sing_eq [iff]: "(ys <~~> [y]) = (ys = [y])"
95   by (blast intro: perm_sing_imp)
88   by (blast intro: perm_sing_imp)
96
89
97 lemma perm_sing_eq2 [iff]: "([y] <~~> ys) = (ys = [y])"
90 lemma perm_sing_eq2 [iff]: "([y] <~~> ys) = (ys = [y])"
110   by (induct ys) auto
103   by (induct ys) auto
111
104
112 lemma remove_commute: "remove x (remove y l) = remove y (remove x l)"
105 lemma remove_commute: "remove x (remove y l) = remove y (remove x l)"
113   by (induct l) auto
106   by (induct l) auto
114
107
115 lemma multiset_of_remove[simp]:
108 lemma multiset_of_remove [simp]:
116     "multiset_of (remove a x) = multiset_of x - {#a#}"
109     "multiset_of (remove a x) = multiset_of x - {#a#}"
117   apply (induct x)
110   apply (induct x)
118    apply (auto simp: multiset_eq_conv_count_eq)
111    apply (auto simp: multiset_eq_conv_count_eq)
119   done
112   done
120
113
121
114
122 text {* \medskip Congruence rule *}
115 text {* \medskip Congruence rule *}
123
116
124 lemma perm_remove_perm: "xs <~~> ys ==> remove z xs <~~> remove z ys"
117 lemma perm_remove_perm: "xs <~~> ys ==> remove z xs <~~> remove z ys"
125   by (erule perm.induct) auto
118   by (induct pred: perm) auto
126
119
127 lemma remove_hd [simp]: "remove z (z # xs) = xs"
120 lemma remove_hd [simp]: "remove z (z # xs) = xs"
128   by auto
121   by auto
129
122
130 lemma cons_perm_imp_perm: "z # xs <~~> z # ys ==> xs <~~> ys"
123 lemma cons_perm_imp_perm: "z # xs <~~> z # ys ==> xs <~~> ys"
131   by (drule_tac z = z in perm_remove_perm) auto
124   by (drule_tac z = z in perm_remove_perm) auto
132
125
133 lemma cons_perm_eq [iff]: "(z#xs <~~> z#ys) = (xs <~~> ys)"
126 lemma cons_perm_eq [iff]: "(z#xs <~~> z#ys) = (xs <~~> ys)"
134   by (blast intro: cons_perm_imp_perm)
127   by (blast intro: cons_perm_imp_perm)
135
128
136 lemma append_perm_imp_perm: "!!xs ys. zs @ xs <~~> zs @ ys ==> xs <~~> ys"
129 lemma append_perm_imp_perm: "zs @ xs <~~> zs @ ys ==> xs <~~> ys"
137   apply (induct zs rule: rev_induct)
130   apply (induct zs arbitrary: xs ys rule: rev_induct)
138    apply (simp_all (no_asm_use))
131    apply (simp_all (no_asm_use))
139   apply blast
132   apply blast
140   done
133   done
141
134
142 lemma perm_append1_eq [iff]: "(zs @ xs <~~> zs @ ys) = (xs <~~> ys)"
135 lemma perm_append1_eq [iff]: "(zs @ xs <~~> zs @ ys) = (xs <~~> ys)"
168   apply (insert surj_multiset_of, drule surjD)
161   apply (insert surj_multiset_of, drule surjD)
169   apply (blast intro: sym)+
162   apply (blast intro: sym)+
170   done
163   done
171
164
172 lemma perm_set_eq: "xs <~~> ys ==> set xs = set ys"
165 lemma perm_set_eq: "xs <~~> ys ==> set xs = set ys"
173 by (metis multiset_of_eq_perm multiset_of_eq_setD)
166   by (metis multiset_of_eq_perm multiset_of_eq_setD)
174
167
175 lemma perm_distinct_iff: "xs <~~> ys ==> distinct xs = distinct ys"
168 lemma perm_distinct_iff: "xs <~~> ys ==> distinct xs = distinct ys"
176 apply(induct rule:perm.induct)
169   apply (induct pred: perm)
177    apply simp_all
170      apply simp_all
178  apply fastsimp
171    apply fastsimp
179 apply (metis perm_set_eq)
172   apply (metis perm_set_eq)
180 done
173   done
181
174
182 lemma eq_set_perm_remdups: "set xs = set ys ==> remdups xs <~~> remdups ys"
175 lemma eq_set_perm_remdups: "set xs = set ys ==> remdups xs <~~> remdups ys"
183 apply(induct xs arbitrary: ys rule:length_induct)
176   apply (induct xs arbitrary: ys rule: length_induct)
184 apply (case_tac "remdups xs", simp, simp)
177   apply (case_tac "remdups xs", simp, simp)
185 apply(subgoal_tac "a : set (remdups ys)")
178   apply (subgoal_tac "a : set (remdups ys)")
186  prefer 2 apply (metis set.simps(2) insert_iff set_remdups)
179    prefer 2 apply (metis set.simps(2) insert_iff set_remdups)
187 apply(drule split_list) apply(elim exE conjE)
180   apply (drule split_list) apply(elim exE conjE)
188 apply(drule_tac x=list in spec) apply(erule impE) prefer 2
181   apply (drule_tac x=list in spec) apply(erule impE) prefer 2
189  apply(drule_tac x="ysa@zs" in spec) apply(erule impE) prefer 2
182    apply (drule_tac x="ysa@zs" in spec) apply(erule impE) prefer 2
190   apply simp
183     apply simp
191   apply(subgoal_tac "a#list <~~> a#ysa@zs")
184     apply (subgoal_tac "a#list <~~> a#ysa@zs")
192    apply (metis Cons_eq_appendI perm_append_Cons trans)
185      apply (metis Cons_eq_appendI perm_append_Cons trans)
193   apply (metis Cons Cons_eq_appendI distinct.simps(2) distinct_remdups distinct_remdups_id perm_append_swap perm_distinct_iff)
186     apply (metis Cons Cons_eq_appendI distinct.simps(2)
194  apply(subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)")
187       distinct_remdups distinct_remdups_id perm_append_swap perm_distinct_iff)
188    apply (subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)")
196  apply (metis distinct_remdups set_remdups)
189     apply (fastsimp simp add: insert_ident)
197 apply (metis Nat.le_less_trans Suc_length_conv le_def length_remdups_leq less_Suc_eq)
190    apply (metis distinct_remdups set_remdups)
198 done
191   apply (metis Nat.le_less_trans Suc_length_conv le_def length_remdups_leq less_Suc_eq)

192   done
199
193
200 lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y = (set x = set y)"
194 lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y = (set x = set y)"
201 by (metis List.set_remdups perm_set_eq eq_set_perm_remdups)
195   by (metis List.set_remdups perm_set_eq eq_set_perm_remdups)
202
196
203 end
197 end