author | wenzelm |
Fri, 12 Aug 2022 19:47:38 +0200 | |
changeset 75827 | 4920ebbde486 |
parent 73706 | 4b1386b2c23e |
permissions | -rw-r--r-- |
73477 | 1 |
(* Author: Lawrence C Paulson and Thomas M Rasmussen and Norbert Voelker |
11054 | 2 |
*) |
3 |
||
73297 | 4 |
section \<open>Permuted Lists\<close> |
11054 | 5 |
|
73297 | 6 |
theory List_Permutation |
73327
fd32f08f4fb5
more connections between mset _ = mset _ and permutations
haftmann
parents:
73305
diff
changeset
|
7 |
imports Permutations |
15131 | 8 |
begin |
11054 | 9 |
|
73329 | 10 |
text \<open> |
11 |
Note that multisets already provide the notion of permutated list and hence |
|
12 |
this theory mostly echoes material already logically present in theory |
|
13 |
\<^text>\<open>Permutations\<close>; it should be seldom needed. |
|
14 |
\<close> |
|
15 |
||
73706 | 16 |
subsection \<open>An existing notion\<close> |
11054 | 17 |
|
73706 | 18 |
abbreviation (input) perm :: \<open>'a list \<Rightarrow> 'a list \<Rightarrow> bool\<close> (infixr \<open><~~>\<close> 50) |
19 |
where \<open>xs <~~> ys \<equiv> mset xs = mset ys\<close> |
|
11054 | 20 |
|
21 |
||
73300 | 22 |
subsection \<open>Nontrivial conclusions\<close> |
11054 | 23 |
|
73300 | 24 |
proposition perm_swap: |
25 |
\<open>xs[i := xs ! j, j := xs ! i] <~~> xs\<close> |
|
26 |
if \<open>i < length xs\<close> \<open>j < length xs\<close> |
|
73706 | 27 |
using that by (simp add: mset_swap) |
15005 | 28 |
|
64587 | 29 |
proposition mset_le_perm_append: "mset xs \<subseteq># mset ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)" |
73706 | 30 |
by (auto simp add: mset_subset_eq_exists_conv ex_mset dest: sym) |
15005 | 31 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
32 |
proposition perm_set_eq: "xs <~~> ys \<Longrightarrow> set xs = set ys" |
73706 | 33 |
by (rule mset_eq_setD) simp |
25277 | 34 |
|
73301 | 35 |
proposition perm_distinct_iff: "xs <~~> ys \<Longrightarrow> distinct xs \<longleftrightarrow> distinct ys" |
73706 | 36 |
by (rule mset_eq_imp_distinct_iff) simp |
25277 | 37 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
38 |
theorem eq_set_perm_remdups: "set xs = set ys \<Longrightarrow> remdups xs <~~> remdups ys" |
73706 | 39 |
by (simp add: set_eq_iff_mset_remdups_eq) |
25287 | 40 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
41 |
proposition perm_remdups_iff_eq_set: "remdups x <~~> remdups y \<longleftrightarrow> set x = set y" |
73706 | 42 |
by (simp add: set_eq_iff_mset_remdups_eq) |
25287 | 43 |
|
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
44 |
theorem permutation_Ex_bij: |
39075 | 45 |
assumes "xs <~~> ys" |
46 |
shows "\<exists>f. bij_betw f {..<length xs} {..<length ys} \<and> (\<forall>i<length xs. xs ! i = ys ! (f i))" |
|
73301 | 47 |
proof - |
73327
fd32f08f4fb5
more connections between mset _ = mset _ and permutations
haftmann
parents:
73305
diff
changeset
|
48 |
from assms have \<open>mset xs = mset ys\<close> \<open>length xs = length ys\<close> |
73706 | 49 |
by (auto simp add: dest: mset_eq_length) |
73327
fd32f08f4fb5
more connections between mset _ = mset _ and permutations
haftmann
parents:
73305
diff
changeset
|
50 |
from \<open>mset xs = mset ys\<close> obtain p where \<open>p permutes {..<length ys}\<close> \<open>permute_list p ys = xs\<close> |
73301 | 51 |
by (rule mset_eq_permutation) |
73327
fd32f08f4fb5
more connections between mset _ = mset _ and permutations
haftmann
parents:
73305
diff
changeset
|
52 |
then have \<open>bij_betw p {..<length xs} {..<length ys}\<close> |
fd32f08f4fb5
more connections between mset _ = mset _ and permutations
haftmann
parents:
73305
diff
changeset
|
53 |
by (simp add: \<open>length xs = length ys\<close> permutes_imp_bij) |
fd32f08f4fb5
more connections between mset _ = mset _ and permutations
haftmann
parents:
73305
diff
changeset
|
54 |
moreover have \<open>\<forall>i<length xs. xs ! i = ys ! (p i)\<close> |
fd32f08f4fb5
more connections between mset _ = mset _ and permutations
haftmann
parents:
73305
diff
changeset
|
55 |
using \<open>permute_list p ys = xs\<close> \<open>length xs = length ys\<close> \<open>p permutes {..<length ys}\<close> permute_list_nth |
fd32f08f4fb5
more connections between mset _ = mset _ and permutations
haftmann
parents:
73305
diff
changeset
|
56 |
by auto |
fd32f08f4fb5
more connections between mset _ = mset _ and permutations
haftmann
parents:
73305
diff
changeset
|
57 |
ultimately show ?thesis |
fd32f08f4fb5
more connections between mset _ = mset _ and permutations
haftmann
parents:
73305
diff
changeset
|
58 |
by blast |
39075 | 59 |
qed |
60 |
||
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
61 |
proposition perm_finite: "finite {B. B <~~> A}" |
73706 | 62 |
using mset_eq_finite by auto |
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
63 |
|
73300 | 64 |
|
65 |
subsection \<open>Trivial conclusions:\<close> |
|
66 |
||
67 |
proposition perm_empty_imp: "[] <~~> ys \<Longrightarrow> ys = []" |
|
73706 | 68 |
by simp |
73300 | 69 |
|
70 |
||
71 |
text \<open>\medskip This more general theorem is easier to understand!\<close> |
|
72 |
||
73 |
proposition perm_length: "xs <~~> ys \<Longrightarrow> length xs = length ys" |
|
73706 | 74 |
by (rule mset_eq_length) simp |
73300 | 75 |
|
76 |
proposition perm_sym: "xs <~~> ys \<Longrightarrow> ys <~~> xs" |
|
73706 | 77 |
by simp |
73300 | 78 |
|
79 |
||
80 |
text \<open>We can insert the head anywhere in the list.\<close> |
|
81 |
||
82 |
proposition perm_append_Cons: "a # xs @ ys <~~> xs @ a # ys" |
|
73706 | 83 |
by simp |
73300 | 84 |
|
85 |
proposition perm_append_swap: "xs @ ys <~~> ys @ xs" |
|
73706 | 86 |
by simp |
73300 | 87 |
|
88 |
proposition perm_append_single: "a # xs <~~> xs @ [a]" |
|
73706 | 89 |
by simp |
73300 | 90 |
|
91 |
proposition perm_rev: "rev xs <~~> xs" |
|
73706 | 92 |
by simp |
73300 | 93 |
|
94 |
proposition perm_append1: "xs <~~> ys \<Longrightarrow> l @ xs <~~> l @ ys" |
|
73706 | 95 |
by simp |
73300 | 96 |
|
97 |
proposition perm_append2: "xs <~~> ys \<Longrightarrow> xs @ l <~~> ys @ l" |
|
73706 | 98 |
by simp |
73300 | 99 |
|
100 |
proposition perm_empty [iff]: "[] <~~> xs \<longleftrightarrow> xs = []" |
|
73706 | 101 |
by simp |
73300 | 102 |
|
103 |
proposition perm_empty2 [iff]: "xs <~~> [] \<longleftrightarrow> xs = []" |
|
73706 | 104 |
by simp |
73300 | 105 |
|
106 |
proposition perm_sing_imp: "ys <~~> xs \<Longrightarrow> xs = [y] \<Longrightarrow> ys = [y]" |
|
73706 | 107 |
by simp |
73300 | 108 |
|
109 |
proposition perm_sing_eq [iff]: "ys <~~> [y] \<longleftrightarrow> ys = [y]" |
|
73706 | 110 |
by simp |
73300 | 111 |
|
112 |
proposition perm_sing_eq2 [iff]: "[y] <~~> ys \<longleftrightarrow> ys = [y]" |
|
73706 | 113 |
by simp |
73300 | 114 |
|
115 |
proposition perm_remove: "x \<in> set ys \<Longrightarrow> ys <~~> x # remove1 x ys" |
|
73706 | 116 |
by simp |
73300 | 117 |
|
118 |
||
119 |
text \<open>\medskip Congruence rule\<close> |
|
120 |
||
121 |
proposition perm_remove_perm: "xs <~~> ys \<Longrightarrow> remove1 z xs <~~> remove1 z ys" |
|
73706 | 122 |
by simp |
73300 | 123 |
|
124 |
proposition remove_hd [simp]: "remove1 z (z # xs) = xs" |
|
73706 | 125 |
by simp |
73300 | 126 |
|
127 |
proposition cons_perm_imp_perm: "z # xs <~~> z # ys \<Longrightarrow> xs <~~> ys" |
|
73706 | 128 |
by simp |
73300 | 129 |
|
130 |
proposition cons_perm_eq [simp]: "z#xs <~~> z#ys \<longleftrightarrow> xs <~~> ys" |
|
73706 | 131 |
by simp |
73300 | 132 |
|
133 |
proposition append_perm_imp_perm: "zs @ xs <~~> zs @ ys \<Longrightarrow> xs <~~> ys" |
|
73706 | 134 |
by simp |
73300 | 135 |
|
136 |
proposition perm_append1_eq [iff]: "zs @ xs <~~> zs @ ys \<longleftrightarrow> xs <~~> ys" |
|
73706 | 137 |
by simp |
73300 | 138 |
|
139 |
proposition perm_append2_eq [iff]: "xs @ zs <~~> ys @ zs \<longleftrightarrow> xs <~~> ys" |
|
73706 | 140 |
by simp |
61699
a81dc5c4d6a9
New theorems mostly from Peter Gammie
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset
|
141 |
|
11054 | 142 |
end |