1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7section "Distinct Proposition"
8
9theory Distinct_Prop  (* part of non-AFP Word_Lib *)
10imports
11  "HOL_Lemmas"
12  "HOL-Library.Prefix_Order"
13begin
14
15primrec
16  distinct_prop :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a list \<Rightarrow> bool)"
17where
18  "distinct_prop P [] = True"
19| "distinct_prop P (x # xs) = ((\<forall>y\<in>set xs. P x y) \<and> distinct_prop P xs)"
20
21primrec
22  distinct_sets :: "'a set list \<Rightarrow> bool"
23where
24  "distinct_sets [] = True"
25| "distinct_sets (x#xs) = (x \<inter> \<Union> (set xs) = {} \<and> distinct_sets xs)"
26
27
28lemma distinct_prop_map:
29  "distinct_prop P (map f xs) = distinct_prop (\<lambda>x y. P (f x) (f y)) xs"
30  by (induct xs) auto
31
32lemma distinct_prop_append:
33  "distinct_prop P (xs @ ys) =
34    (distinct_prop P xs \<and> distinct_prop P ys \<and> (\<forall>x \<in> set xs. \<forall>y \<in> set ys. P x y))"
35  by (induct xs arbitrary: ys) (auto simp: conj_comms ball_Un)
36
37lemma distinct_prop_distinct:
38  "\<lbrakk> distinct xs; \<And>x y. \<lbrakk> x \<in> set xs; y \<in> set xs; x \<noteq> y \<rbrakk> \<Longrightarrow> P x y \<rbrakk> \<Longrightarrow> distinct_prop P xs"
39  by (induct xs) auto
40
41lemma distinct_prop_True [simp]:
42  "distinct_prop (\<lambda>x y. True) xs"
43  by (induct xs, auto)
44
45
46lemma distinct_prefix:
47  "\<lbrakk> distinct xs; ys \<le> xs \<rbrakk> \<Longrightarrow> distinct ys"
48  apply (induct xs arbitrary: ys; clarsimp)
49  apply (case_tac ys; clarsimp)
50  by (fastforce simp: less_eq_list_def dest: set_mono_prefix)
51
52lemma distinct_sets_prop:
53  "distinct_sets xs = distinct_prop (\<lambda>x y. x \<inter> y = {}) xs"
54  by (induct xs) auto
55
56lemma distinct_take_strg:
57  "distinct xs \<longrightarrow> distinct (take n xs)"
58  by simp
59
60lemma distinct_prop_prefixE:
61  "\<lbrakk> distinct_prop P ys; prefix xs ys \<rbrakk> \<Longrightarrow> distinct_prop P xs"
62  apply (induct xs arbitrary: ys; clarsimp)
63  apply (case_tac ys; clarsimp)
64  by (fastforce dest: set_mono_prefix)
65
66
67lemma distinct_sets_union_sub:
68  "\<lbrakk>x \<in> A; distinct_sets [A,B]\<rbrakk> \<Longrightarrow> A \<union> B - {x} = A - {x} \<union> B"
69  by (auto simp: distinct_sets_def)
70
71lemma distinct_sets_append:
72  "distinct_sets (xs @ ys) \<Longrightarrow> distinct_sets xs \<and> distinct_sets ys"
73  apply (subst distinct_sets_prop)+
74  apply (subst (asm) distinct_sets_prop)
75  apply (subst (asm) distinct_prop_append)
76  apply clarsimp
77  done
78
79lemma distinct_sets_append1:
80  "distinct_sets (xs @ ys) \<Longrightarrow> distinct_sets xs"
81  by (drule distinct_sets_append, simp)
82
83lemma distinct_sets_append2:
84  "distinct_sets (xs @ ys) \<Longrightarrow> distinct_sets ys"
85  by (drule distinct_sets_append, simp)
86
87lemma distinct_sets_append_Cons:
88  "distinct_sets (xs @ a # ys) \<Longrightarrow> distinct_sets (xs @ ys)"
89  apply (subst distinct_sets_prop)+
90  apply (subst (asm) distinct_sets_prop)
91  apply (subst distinct_prop_append)
92  apply (subst (asm) distinct_prop_append)
93  apply clarsimp
94  done
95
96lemma distinct_sets_append_Cons_disjoint:
97  "distinct_sets (xs @ a # ys) \<Longrightarrow>  a \<inter> \<Union> (set xs) = {} "
98  apply (subst (asm) distinct_sets_prop)
99  apply (subst (asm) distinct_prop_append)
100  apply (subst Int_commute)
101  apply (subst Union_disjoint)
102  apply clarsimp
103  done
104
105lemma distinct_prop_take:
106  "\<lbrakk>distinct_prop P xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_prop P (take i xs)"
107  by (metis take_is_prefix distinct_prop_prefixE)
108
109lemma distinct_sets_take:
110  "\<lbrakk>distinct_sets xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_sets (take i xs)"
111  by (simp add: distinct_sets_prop distinct_prop_take)
112
113lemma distinct_prop_take_Suc:
114  "\<lbrakk>distinct_prop P xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_prop P (take (Suc i) xs)"
115  by (metis distinct_prop_take not_less take_all)
116
117lemma distinct_sets_take_Suc:
118  "\<lbrakk>distinct_sets xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_sets (take (Suc i) xs)"
119  by (simp add: distinct_sets_prop distinct_prop_take_Suc)
120
121lemma distinct_prop_rev:
122  "distinct_prop P (rev xs) = distinct_prop (\<lambda>y x. P x y) xs"
123  by (induct xs) (auto simp: distinct_prop_append)
124
125lemma distinct_sets_rev [simp]:
126  "distinct_sets (rev xs) = distinct_sets xs"
127  apply (unfold distinct_sets_prop)
128  apply (subst distinct_prop_rev)
129  apply (subst Int_commute)
130  apply clarsimp
131  done
132
133lemma distinct_sets_drop:
134  "\<lbrakk>distinct_sets xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_sets (drop i xs)"
135  apply (cases "i=0", simp)
136  apply (subst distinct_sets_rev [symmetric])
137  apply (subst rev_drop)
138  apply (subst distinct_sets_take, simp_all)
139  done
140
141lemma distinct_sets_drop_Suc:
142  "\<lbrakk>distinct_sets xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_sets (drop (Suc i) xs)"
143  apply (subst distinct_sets_rev [symmetric])
144  apply (subst rev_drop)
145  apply (subst distinct_sets_take, simp_all)
146  done
147
148lemma distinct_sets_take_nth:
149  "\<lbrakk>distinct_sets xs; i < length xs; x \<in> set (take i xs)\<rbrakk> \<Longrightarrow> x \<inter> xs ! i = {}"
150  apply (drule (1) distinct_sets_take_Suc)
151  apply (subst (asm) take_Suc_conv_app_nth, assumption)
152  apply (unfold distinct_sets_prop)
153  apply (subst (asm) distinct_prop_append)
154  apply clarsimp
155  done
156
157lemma distinct_sets_drop_nth:
158  "\<lbrakk>distinct_sets xs; i < length xs; x \<in> set (drop (Suc i) xs)\<rbrakk> \<Longrightarrow> x \<inter> xs ! i = {}"
159  apply (drule (1) distinct_sets_drop)
160  apply (subst (asm) drop_Suc_nth, assumption)
161  apply fastforce
162  done
163
164lemma distinct_sets_append_distinct:
165  "\<lbrakk>x \<in> set xs; y \<in> set ys; distinct_sets (xs @ ys)\<rbrakk> \<Longrightarrow> x \<inter> y = {}"
166  unfolding distinct_sets_prop by (clarsimp simp: distinct_prop_append)
167
168lemma distinct_sets_update:
169 "\<lbrakk>a \<subseteq> xs ! i; distinct_sets xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_sets (xs[i := a])"
170  apply (subst distinct_sets_prop)
171  apply (subst (asm) distinct_sets_prop)
172  apply (subst upd_conv_take_nth_drop, simp)
173  apply (subst distinct_prop_append)
174  apply (intro conjI)
175    apply (erule (1) distinct_prop_take)
176   apply (rule conjI|clarsimp)+
177    apply (fold distinct_sets_prop)
178    apply (drule (1) distinct_sets_drop)
179    apply (subst (asm) drop_Suc_nth, assumption)
180    apply fastforce
181   apply (drule (1) distinct_sets_drop)
182   apply (subst (asm) drop_Suc_nth, assumption)
183   apply clarsimp
184  apply clarsimp
185  apply (rule conjI)
186   apply (drule (2) distinct_sets_take_nth)
187   apply blast
188  apply clarsimp
189  apply (thin_tac "P \<subseteq> Q" for P Q)
190  apply (subst (asm) id_take_nth_drop, assumption)
191  apply (drule distinct_sets_append_Cons)
192  apply (erule (2) distinct_sets_append_distinct)
193  done
194
195lemma distinct_sets_map_update:
196  "\<lbrakk>distinct_sets (map f xs); i < length xs; f a \<subseteq> f(xs ! i)\<rbrakk>
197  \<Longrightarrow> distinct_sets (map f (xs[i := a]))"
198  by (metis distinct_sets_update length_map map_update nth_map)
199
200lemma Union_list_update:
201  "\<lbrakk>i < length xs; distinct_sets (map f xs)\<rbrakk>
202  \<Longrightarrow> (\<Union>x\<in>set (xs [i := a]). f x) = (\<Union>x\<in>set xs. f x) - f (xs ! i) \<union> f a"
203  apply (induct xs arbitrary: i; clarsimp)
204  apply (case_tac i; (clarsimp, fastforce))
205  done
206
207lemma fst_enumerate:
208  "i < length xs \<Longrightarrow> fst (enumerate n xs ! i) = i + n"
209  by (metis add.commute fst_conv nth_enumerate_eq)
210
211lemma snd_enumerate:
212  "i < length xs \<Longrightarrow> snd (enumerate n xs ! i) = xs ! i"
213  by (metis nth_enumerate_eq snd_conv)
214
215lemma enumerate_member:
216  assumes "i < length xs"
217  shows "(n + i, xs ! i) \<in> set (enumerate n xs)"
218proof -
219  have pair_unpack: "\<And>a b x. ((a, b) = x) = (a = fst x \<and> b = snd x)" by fastforce
220  from assms have "(n + i, xs ! i) = enumerate n xs ! i"
221    by (auto simp: fst_enumerate snd_enumerate pair_unpack)
222  with assms show ?thesis by simp
223qed
224
225lemma distinct_prop_nth:
226  "\<lbrakk> distinct_prop P ls; n < n'; n' < length ls \<rbrakk> \<Longrightarrow> P (ls ! n) (ls ! n')"
227  apply (induct ls arbitrary: n n'; simp)
228  apply (case_tac n'; simp)
229  apply (case_tac n; simp)
230  done
231
232end
233