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 
25 lemma xperm_empty_imp_aux: "xs <~~> ys ==> xs = [] > ys = []" 

26  {*the form of the premise lets the induction bind @{term xs} 

27 and @{term ys} *} 

28 apply (erule perm.induct) 

29 apply (simp_all (no_asm_simp)) 

30 done 

31 

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) 
195 apply(fastsimp simp add: insert_ident) 
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 