author | haftmann |
Wed, 24 Feb 2021 13:31:33 +0000 | |
changeset 73301 | bfe92e4f6ea4 |
parent 73300 | c52c5a5bf4e6 |
child 73305 | 47616dc81488 |
permissions | -rw-r--r-- |
73297 | 1 |
(* Title: HOL/Library/List_Permutation.thy |
15005 | 2 |
Author: Lawrence C Paulson and Thomas M Rasmussen and Norbert Voelker |
11054 | 3 |
*) |
4 |
||
73297 | 5 |
section \<open>Permuted Lists\<close> |
11054 | 6 |
|
73297 | 7 |
theory List_Permutation |
51542 | 8 |
imports Multiset |
15131 | 9 |
begin |
11054 | 10 |
|
73300 | 11 |
subsection \<open>An inductive definition\<dots>\<close> |
12 |
||
70680 | 13 |
inductive perm :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infixr \<open><~~>\<close> 50) |
53238 | 14 |
where |
15 |
Nil [intro!]: "[] <~~> []" |
|
16 |
| swap [intro!]: "y # x # l <~~> x # y # l" |
|
17 |
| Cons [intro!]: "xs <~~> ys \<Longrightarrow> z # xs <~~> z # ys" |
|
18 |
| trans [intro]: "xs <~~> ys \<Longrightarrow> ys <~~> zs \<Longrightarrow> xs <~~> zs" |
|
11054 | 19 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
20 |
proposition perm_refl [iff]: "l <~~> l" |
17200 | 21 |
by (induct l) auto |
11054 | 22 |
|
73300 | 23 |
text \<open>\<dots>that is equivalent to an already existing notion:\<close> |
11054 | 24 |
|
73300 | 25 |
lemma perm_iff_eq_mset: |
26 |
\<open>xs <~~> ys \<longleftrightarrow> mset xs = mset ys\<close> |
|
27 |
proof |
|
28 |
assume \<open>mset xs = mset ys\<close> |
|
29 |
then show \<open>xs <~~> ys\<close> |
|
30 |
proof (induction xs arbitrary: ys) |
|
31 |
case Nil |
|
32 |
then show ?case |
|
33 |
by simp |
|
34 |
next |
|
35 |
case (Cons x xs) |
|
36 |
from Cons.prems [symmetric] have \<open>mset xs = mset (remove1 x ys)\<close> |
|
37 |
by simp |
|
38 |
then have \<open>xs <~~> remove1 x ys\<close> |
|
39 |
by (rule Cons.IH) |
|
40 |
then have \<open>x # xs <~~> x # remove1 x ys\<close> |
|
41 |
by (rule perm.Cons) |
|
42 |
moreover from Cons.prems have \<open>x \<in> set ys\<close> |
|
43 |
by (auto dest: union_single_eq_member) |
|
44 |
then have \<open>x # remove1 x ys <~~> ys\<close> |
|
45 |
by (induction ys) auto |
|
46 |
ultimately show \<open>x # xs <~~> ys\<close> |
|
47 |
by (rule perm.trans) |
|
48 |
qed |
|
49 |
next |
|
50 |
assume \<open>xs <~~> ys\<close> |
|
51 |
then show \<open>mset xs = mset ys\<close> |
|
52 |
by induction simp_all |
|
53 |
qed |
|
11054 | 54 |
|
73300 | 55 |
theorem mset_eq_perm: \<open>mset xs = mset ys \<longleftrightarrow> xs <~~> ys\<close> |
56 |
by (simp add: perm_iff_eq_mset) |
|
11054 | 57 |
|
58 |
||
73300 | 59 |
subsection \<open>Nontrivial conclusions\<close> |
11054 | 60 |
|
73300 | 61 |
proposition perm_swap: |
62 |
\<open>xs[i := xs ! j, j := xs ! i] <~~> xs\<close> |
|
63 |
if \<open>i < length xs\<close> \<open>j < length xs\<close> |
|
73301 | 64 |
using that by (simp add: perm_iff_eq_mset mset_swap) |
15005 | 65 |
|
64587 | 66 |
proposition mset_le_perm_append: "mset xs \<subseteq># mset ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)" |
73300 | 67 |
by (auto simp add: perm_iff_eq_mset mset_subset_eq_exists_conv ex_mset dest: sym) |
15005 | 68 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
69 |
proposition perm_set_eq: "xs <~~> ys \<Longrightarrow> set xs = set ys" |
73300 | 70 |
by (rule mset_eq_setD) (simp add: perm_iff_eq_mset) |
25277 | 71 |
|
73301 | 72 |
proposition perm_distinct_iff: "xs <~~> ys \<Longrightarrow> distinct xs \<longleftrightarrow> distinct ys" |
73 |
by (rule mset_eq_imp_distinct_iff) (simp add: perm_iff_eq_mset) |
|
25277 | 74 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
75 |
theorem eq_set_perm_remdups: "set xs = set ys \<Longrightarrow> remdups xs <~~> remdups ys" |
73300 | 76 |
by (simp add: perm_iff_eq_mset set_eq_iff_mset_remdups_eq) |
25287 | 77 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
78 |
proposition perm_remdups_iff_eq_set: "remdups x <~~> remdups y \<longleftrightarrow> set x = set y" |
73300 | 79 |
by (simp add: perm_iff_eq_mset set_eq_iff_mset_remdups_eq) |
25287 | 80 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
81 |
theorem permutation_Ex_bij: |
39075 | 82 |
assumes "xs <~~> ys" |
83 |
shows "\<exists>f. bij_betw f {..<length xs} {..<length ys} \<and> (\<forall>i<length xs. xs ! i = ys ! (f i))" |
|
73301 | 84 |
proof - |
85 |
from assms have \<open>mset ys = mset xs\<close> |
|
86 |
by (simp add: perm_iff_eq_mset) |
|
87 |
then obtain f where \<open>bij_betw f {..<length ys} {..<length xs}\<close> |
|
88 |
\<open>xs = map (\<lambda>n. ys ! f n) [0..<length ys]\<close> |
|
89 |
by (rule mset_eq_permutation) |
|
90 |
then show ?thesis by auto |
|
39075 | 91 |
qed |
92 |
||
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
93 |
proposition perm_finite: "finite {B. B <~~> A}" |
73301 | 94 |
using mset_eq_finite by (auto simp add: perm_iff_eq_mset) |
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
95 |
|
73300 | 96 |
|
97 |
subsection \<open>Trivial conclusions:\<close> |
|
98 |
||
99 |
proposition perm_empty_imp: "[] <~~> ys \<Longrightarrow> ys = []" |
|
100 |
by (simp add: perm_iff_eq_mset) |
|
101 |
||
102 |
||
103 |
text \<open>\medskip This more general theorem is easier to understand!\<close> |
|
104 |
||
105 |
proposition perm_length: "xs <~~> ys \<Longrightarrow> length xs = length ys" |
|
106 |
by (rule mset_eq_length) (simp add: perm_iff_eq_mset) |
|
107 |
||
108 |
proposition perm_sym: "xs <~~> ys \<Longrightarrow> ys <~~> xs" |
|
109 |
by (simp add: perm_iff_eq_mset) |
|
110 |
||
111 |
||
112 |
text \<open>We can insert the head anywhere in the list.\<close> |
|
113 |
||
114 |
proposition perm_append_Cons: "a # xs @ ys <~~> xs @ a # ys" |
|
115 |
by (simp add: perm_iff_eq_mset) |
|
116 |
||
117 |
proposition perm_append_swap: "xs @ ys <~~> ys @ xs" |
|
118 |
by (simp add: perm_iff_eq_mset) |
|
119 |
||
120 |
proposition perm_append_single: "a # xs <~~> xs @ [a]" |
|
121 |
by (simp add: perm_iff_eq_mset) |
|
122 |
||
123 |
proposition perm_rev: "rev xs <~~> xs" |
|
124 |
by (simp add: perm_iff_eq_mset) |
|
125 |
||
126 |
proposition perm_append1: "xs <~~> ys \<Longrightarrow> l @ xs <~~> l @ ys" |
|
127 |
by (simp add: perm_iff_eq_mset) |
|
128 |
||
129 |
proposition perm_append2: "xs <~~> ys \<Longrightarrow> xs @ l <~~> ys @ l" |
|
130 |
by (simp add: perm_iff_eq_mset) |
|
131 |
||
132 |
proposition perm_empty [iff]: "[] <~~> xs \<longleftrightarrow> xs = []" |
|
133 |
by (simp add: perm_iff_eq_mset) |
|
134 |
||
135 |
proposition perm_empty2 [iff]: "xs <~~> [] \<longleftrightarrow> xs = []" |
|
136 |
by (simp add: perm_iff_eq_mset) |
|
137 |
||
138 |
proposition perm_sing_imp: "ys <~~> xs \<Longrightarrow> xs = [y] \<Longrightarrow> ys = [y]" |
|
139 |
by (simp add: perm_iff_eq_mset) |
|
140 |
||
141 |
proposition perm_sing_eq [iff]: "ys <~~> [y] \<longleftrightarrow> ys = [y]" |
|
142 |
by (simp add: perm_iff_eq_mset) |
|
143 |
||
144 |
proposition perm_sing_eq2 [iff]: "[y] <~~> ys \<longleftrightarrow> ys = [y]" |
|
145 |
by (simp add: perm_iff_eq_mset) |
|
146 |
||
147 |
proposition perm_remove: "x \<in> set ys \<Longrightarrow> ys <~~> x # remove1 x ys" |
|
148 |
by (simp add: perm_iff_eq_mset) |
|
149 |
||
150 |
||
151 |
text \<open>\medskip Congruence rule\<close> |
|
152 |
||
153 |
proposition perm_remove_perm: "xs <~~> ys \<Longrightarrow> remove1 z xs <~~> remove1 z ys" |
|
154 |
by (simp add: perm_iff_eq_mset) |
|
155 |
||
156 |
proposition remove_hd [simp]: "remove1 z (z # xs) = xs" |
|
157 |
by (simp add: perm_iff_eq_mset) |
|
158 |
||
159 |
proposition cons_perm_imp_perm: "z # xs <~~> z # ys \<Longrightarrow> xs <~~> ys" |
|
160 |
by (simp add: perm_iff_eq_mset) |
|
161 |
||
162 |
proposition cons_perm_eq [simp]: "z#xs <~~> z#ys \<longleftrightarrow> xs <~~> ys" |
|
163 |
by (simp add: perm_iff_eq_mset) |
|
164 |
||
165 |
proposition append_perm_imp_perm: "zs @ xs <~~> zs @ ys \<Longrightarrow> xs <~~> ys" |
|
166 |
by (simp add: perm_iff_eq_mset) |
|
167 |
||
168 |
proposition perm_append1_eq [iff]: "zs @ xs <~~> zs @ ys \<longleftrightarrow> xs <~~> ys" |
|
169 |
by (simp add: perm_iff_eq_mset) |
|
170 |
||
171 |
proposition perm_append2_eq [iff]: "xs @ zs <~~> ys @ zs \<longleftrightarrow> xs <~~> ys" |
|
172 |
by (simp add: perm_iff_eq_mset) |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
173 |
|
11054 | 174 |
end |