|
1 theory RfltsRdistinctProps imports "Rsimp" |
|
2 begin |
|
3 |
|
4 |
|
5 |
|
6 lemma all_that_same_elem: |
|
7 shows "\<lbrakk> a \<in> rset; rdistinct rs {a} = []\<rbrakk> |
|
8 \<Longrightarrow> rdistinct (rs @ rsb) rset = rdistinct rsb rset" |
|
9 apply(induct rs) |
|
10 apply simp |
|
11 apply(subgoal_tac "aa = a") |
|
12 apply simp |
|
13 by (metis empty_iff insert_iff list.discI rdistinct.simps(2)) |
|
14 |
|
15 |
|
16 lemma rdistinct1: |
|
17 assumes "a \<in> acc" |
|
18 shows "a \<notin> set (rdistinct rs acc)" |
|
19 using assms |
|
20 apply(induct rs arbitrary: acc a) |
|
21 apply(auto) |
|
22 done |
|
23 |
|
24 |
|
25 lemma rdistinct_does_the_job: |
|
26 shows "distinct (rdistinct rs s)" |
|
27 apply(induct rs s rule: rdistinct.induct) |
|
28 apply(auto simp add: rdistinct1) |
|
29 done |
|
30 |
|
31 |
|
32 |
|
33 lemma rdistinct_concat: |
|
34 assumes "set rs \<subseteq> rset" |
|
35 shows "rdistinct (rs @ rsa) rset = rdistinct rsa rset" |
|
36 using assms |
|
37 apply(induct rs) |
|
38 apply simp+ |
|
39 done |
|
40 |
|
41 lemma distinct_not_exist: |
|
42 assumes "a \<notin> set rs" |
|
43 shows "rdistinct rs rset = rdistinct rs (insert a rset)" |
|
44 using assms |
|
45 apply(induct rs arbitrary: rset) |
|
46 apply(auto) |
|
47 done |
|
48 |
|
49 lemma rdistinct_on_distinct: |
|
50 shows "distinct rs \<Longrightarrow> rdistinct rs {} = rs" |
|
51 apply(induct rs) |
|
52 apply simp |
|
53 using distinct_not_exist by fastforce |
|
54 |
|
55 lemma distinct_rdistinct_append: |
|
56 assumes "distinct rs1" "\<forall>r \<in> set rs1. r \<notin> acc" |
|
57 shows "rdistinct (rs1 @ rsa) acc = rs1 @ (rdistinct rsa (acc \<union> set rs1))" |
|
58 using assms |
|
59 apply(induct rs1 arbitrary: rsa acc) |
|
60 apply(auto)[1] |
|
61 apply(auto)[1] |
|
62 apply(drule_tac x="rsa" in meta_spec) |
|
63 apply(drule_tac x="{a} \<union> acc" in meta_spec) |
|
64 apply(simp) |
|
65 apply(drule meta_mp) |
|
66 apply(auto)[1] |
|
67 apply(simp) |
|
68 done |
|
69 |
|
70 |
|
71 lemma rdistinct_set_equality1: |
|
72 shows "set (rdistinct rs acc) = set rs - acc" |
|
73 apply(induct rs acc rule: rdistinct.induct) |
|
74 apply(auto) |
|
75 done |
|
76 |
|
77 |
|
78 lemma rdistinct_set_equality: |
|
79 shows "set (rdistinct rs {}) = set rs" |
|
80 by (simp add: rdistinct_set_equality1) |
|
81 |
|
82 |
|
83 |
|
84 lemma distinct_removes_last: |
|
85 shows "\<lbrakk>a \<in> set as\<rbrakk> |
|
86 \<Longrightarrow> rdistinct as rset = rdistinct (as @ [a]) rset" |
|
87 and "rdistinct (ab # as @ [ab]) rset1 = rdistinct (ab # as) rset1" |
|
88 apply(induct as arbitrary: rset ab rset1 a) |
|
89 apply simp |
|
90 apply simp |
|
91 apply(case_tac "aa \<in> rset") |
|
92 apply(case_tac "a = aa") |
|
93 apply (metis append_Cons) |
|
94 apply simp |
|
95 apply(case_tac "a \<in> set as") |
|
96 apply (metis append_Cons rdistinct.simps(2) set_ConsD) |
|
97 apply(case_tac "a = aa") |
|
98 prefer 2 |
|
99 apply simp |
|
100 apply (metis append_Cons) |
|
101 apply(case_tac "ab \<in> rset1") |
|
102 prefer 2 |
|
103 apply(subgoal_tac "rdistinct (ab # (a # as) @ [ab]) rset1 = |
|
104 ab # (rdistinct ((a # as) @ [ab]) (insert ab rset1))") |
|
105 prefer 2 |
|
106 apply force |
|
107 apply(simp only:) |
|
108 apply(subgoal_tac "rdistinct (ab # a # as) rset1 = ab # (rdistinct (a # as) (insert ab rset1))") |
|
109 apply(simp only:) |
|
110 apply(subgoal_tac "rdistinct ((a # as) @ [ab]) (insert ab rset1) = rdistinct (a # as) (insert ab rset1)") |
|
111 apply blast |
|
112 apply(case_tac "a \<in> insert ab rset1") |
|
113 apply simp |
|
114 apply (metis insertI1) |
|
115 apply simp |
|
116 apply (meson insertI1) |
|
117 apply simp |
|
118 apply(subgoal_tac "rdistinct ((a # as) @ [ab]) rset1 = rdistinct (a # as) rset1") |
|
119 apply simp |
|
120 by (metis append_Cons insert_iff insert_is_Un rdistinct.simps(2)) |
|
121 |
|
122 |
|
123 lemma distinct_removes_middle: |
|
124 shows "\<lbrakk>a \<in> set as\<rbrakk> |
|
125 \<Longrightarrow> rdistinct (as @ as2) rset = rdistinct (as @ [a] @ as2) rset" |
|
126 and "rdistinct (ab # as @ [ab] @ as3) rset1 = rdistinct (ab # as @ as3) rset1" |
|
127 apply(induct as arbitrary: rset rset1 ab as2 as3 a) |
|
128 apply simp |
|
129 apply simp |
|
130 apply(case_tac "a \<in> rset") |
|
131 apply simp |
|
132 apply metis |
|
133 apply simp |
|
134 apply (metis insertI1) |
|
135 apply(case_tac "a = ab") |
|
136 apply simp |
|
137 apply(case_tac "ab \<in> rset") |
|
138 apply simp |
|
139 apply presburger |
|
140 apply (meson insertI1) |
|
141 apply(case_tac "a \<in> rset") |
|
142 apply (metis (no_types, opaque_lifting) Un_insert_left append_Cons insert_iff rdistinct.simps(2) sup_bot_left) |
|
143 apply(case_tac "ab \<in> rset") |
|
144 apply simp |
|
145 apply (meson insert_iff) |
|
146 apply simp |
|
147 by (metis insertI1) |
|
148 |
|
149 |
|
150 lemma k0b: |
|
151 assumes "nonalt r" "r \<noteq> RZERO" |
|
152 shows "rflts [r] = [r]" |
|
153 using assms |
|
154 apply(case_tac r) |
|
155 apply(simp_all) |
|
156 done |
|
157 |
|
158 lemma rflts_def_idiot: |
|
159 shows "\<lbrakk> a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1\<rbrakk> \<Longrightarrow> rflts (a # rs) = a # rflts rs" |
|
160 apply(case_tac a) |
|
161 apply simp_all |
|
162 done |
|
163 |
|
164 lemma flts_middle0: |
|
165 shows "rflts (rsa @ RZERO # rsb) = rflts (rsa @ rsb)" |
|
166 apply(induct rsa) |
|
167 apply simp |
|
168 by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot) |
|
169 |
|
170 |
|
171 lemma flts_removes0: |
|
172 shows " rflts (rs @ [RZERO]) = |
|
173 rflts rs" |
|
174 apply(induct rs) |
|
175 apply simp |
|
176 by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot) |
|
177 |
|
178 lemma rflts_spills_last: |
|
179 shows "rflts (rs1 @ [RALTS rs]) = rflts rs1 @ rs" |
|
180 apply (induct rs1 rule: rflts.induct) |
|
181 apply(auto) |
|
182 done |
|
183 |
|
184 lemma flts_keeps1: |
|
185 shows "rflts (rs @ [RONE]) = rflts rs @ [RONE]" |
|
186 apply (induct rs rule: rflts.induct) |
|
187 apply(auto) |
|
188 done |
|
189 |
|
190 lemma flts_keeps_others: |
|
191 shows "\<lbrakk>a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1\<rbrakk> \<Longrightarrow>rflts (rs @ [a]) = rflts rs @ [a]" |
|
192 apply(induct rs rule: rflts.induct) |
|
193 apply(auto) |
|
194 by (meson k0b nonalt.elims(3)) |
|
195 |
|
196 lemma spilled_alts_contained: |
|
197 shows "\<lbrakk>a = RALTS rs ; a \<in> set rs1\<rbrakk> \<Longrightarrow> \<forall>r \<in> set rs. r \<in> set (rflts rs1)" |
|
198 apply(induct rs1) |
|
199 apply simp |
|
200 apply(case_tac "a = aa") |
|
201 apply simp |
|
202 apply(subgoal_tac " a \<in> set rs1") |
|
203 prefer 2 |
|
204 apply (meson set_ConsD) |
|
205 apply(case_tac aa) |
|
206 using rflts.simps(2) apply presburger |
|
207 apply fastforce |
|
208 apply fastforce |
|
209 apply fastforce |
|
210 apply fastforce |
|
211 by fastforce |
|
212 |
|
213 |
|
214 lemma rflts_def_idiot2: |
|
215 shows "\<lbrakk>a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1; a \<in> set rs\<rbrakk> \<Longrightarrow> a \<in> set (rflts rs)" |
|
216 apply(induct rs rule: rflts.induct) |
|
217 apply(auto) |
|
218 done |
|
219 |
|
220 lemma flts_append: |
|
221 shows "rflts (rs1 @ rs2) = rflts rs1 @ rflts rs2" |
|
222 apply(induct rs1) |
|
223 apply simp |
|
224 apply(case_tac a) |
|
225 apply simp+ |
|
226 done |
|
227 lemma distinct_removes_middle3: |
|
228 shows "\<lbrakk>a \<in> set as\<rbrakk> |
|
229 \<Longrightarrow> rdistinct (as @ a #as2) rset = rdistinct (as @ as2) rset" |
|
230 using distinct_removes_middle(1) by fastforce |
|
231 |
|
232 |
|
233 lemma distinct_removes_list: |
|
234 shows "\<lbrakk> \<forall>r \<in> set rs. r \<in> set as\<rbrakk> \<Longrightarrow> rdistinct (as @ rs) {} = rdistinct as {}" |
|
235 apply(induct rs) |
|
236 apply simp+ |
|
237 apply(subgoal_tac "rdistinct (as @ a # rs) {} = rdistinct (as @ rs) {}") |
|
238 prefer 2 |
|
239 apply (metis append_Cons append_Nil distinct_removes_middle(1)) |
|
240 by presburger |
|
241 |
|
242 lemma last_elem_out: |
|
243 shows "\<lbrakk>x \<notin> set xs; x \<notin> rset \<rbrakk> \<Longrightarrow> rdistinct (xs @ [x]) rset = rdistinct xs rset @ [x]" |
|
244 apply(induct xs arbitrary: rset) |
|
245 apply simp+ |
|
246 done |
|
247 |
|
248 |
|
249 lemma rdistinct_concat_general: |
|
250 shows "rdistinct (rs1 @ rs2) {} = (rdistinct rs1 {}) @ (rdistinct rs2 (set rs1))" |
|
251 apply(induct rs1 arbitrary: rs2 rule: rev_induct) |
|
252 apply simp |
|
253 apply(drule_tac x = "x # rs2" in meta_spec) |
|
254 apply simp |
|
255 apply(case_tac "x \<in> set xs") |
|
256 apply simp |
|
257 |
|
258 apply (simp add: distinct_removes_middle3 insert_absorb) |
|
259 apply simp |
|
260 by (simp add: last_elem_out) |
|
261 |
|
262 |
|
263 |
|
264 |
|
265 lemma distinct_once_enough: |
|
266 shows "rdistinct (rs @ rsa) {} = rdistinct (rdistinct rs {} @ rsa) {}" |
|
267 apply(subgoal_tac "distinct (rdistinct rs {})") |
|
268 apply(subgoal_tac |
|
269 " rdistinct (rdistinct rs {} @ rsa) {} = rdistinct rs {} @ (rdistinct rsa (set rs))") |
|
270 apply(simp only:) |
|
271 using rdistinct_concat_general apply blast |
|
272 apply (simp add: distinct_rdistinct_append rdistinct_set_equality1) |
|
273 by (simp add: rdistinct_does_the_job) |
|
274 |
|
275 |
|
276 |
|
277 |
|
278 lemma distinct_removes_duplicate_flts: |
|
279 shows " a \<in> set rsa |
|
280 \<Longrightarrow> rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} = |
|
281 rdistinct (rflts (map rsimp rsa)) {}" |
|
282 apply(subgoal_tac "rsimp a \<in> set (map rsimp rsa)") |
|
283 prefer 2 |
|
284 apply simp |
|
285 apply(induct "rsimp a") |
|
286 apply simp |
|
287 using flts_removes0 apply presburger |
|
288 apply(subgoal_tac " rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} = |
|
289 rdistinct (rflts (map rsimp rsa @ [RONE])) {}") |
|
290 apply (simp only:) |
|
291 apply(subst flts_keeps1) |
|
292 apply (metis distinct_removes_last(1) rflts_def_idiot2 rrexp.simps(20) rrexp.simps(6)) |
|
293 apply presburger |
|
294 apply(subgoal_tac " rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} = |
|
295 rdistinct ((rflts (map rsimp rsa)) @ [RCHAR x]) {}") |
|
296 apply (simp only:) |
|
297 prefer 2 |
|
298 apply (metis flts_keeps_others rrexp.distinct(21) rrexp.distinct(3)) |
|
299 apply (metis distinct_removes_last(1) rflts_def_idiot2 rrexp.distinct(21) rrexp.distinct(3)) |
|
300 |
|
301 apply (metis distinct_removes_last(1) flts_keeps_others rflts_def_idiot2 rrexp.distinct(25) rrexp.distinct(5)) |
|
302 prefer 2 |
|
303 apply (metis distinct_removes_last(1) flts_keeps_others flts_removes0 rflts_def_idiot2 rrexp.distinct(29)) |
|
304 apply(subgoal_tac "rflts (map rsimp rsa @ [rsimp a]) = rflts (map rsimp rsa) @ x") |
|
305 prefer 2 |
|
306 apply (simp add: rflts_spills_last) |
|
307 apply(subgoal_tac "\<forall> r \<in> set x. r \<in> set (rflts (map rsimp rsa))") |
|
308 prefer 2 |
|
309 apply (metis (mono_tags, lifting) image_iff image_set spilled_alts_contained) |
|
310 apply (metis rflts_spills_last) |
|
311 by (metis distinct_removes_list spilled_alts_contained) |
|
312 |
|
313 |
|
314 |
|
315 |
|
316 |
|
317 lemma distinct_early_app1: |
|
318 shows "rset1 \<subseteq> rset \<Longrightarrow> rdistinct rs rset = rdistinct (rdistinct rs rset1) rset" |
|
319 apply(induct rs arbitrary: rset rset1) |
|
320 apply simp |
|
321 apply simp |
|
322 apply(case_tac "a \<in> rset1") |
|
323 apply simp |
|
324 apply(case_tac "a \<in> rset") |
|
325 apply simp+ |
|
326 |
|
327 apply blast |
|
328 apply(case_tac "a \<in> rset1") |
|
329 apply simp+ |
|
330 apply(case_tac "a \<in> rset") |
|
331 apply simp |
|
332 apply (metis insert_subsetI) |
|
333 apply simp |
|
334 by (meson insert_mono) |
|
335 |
|
336 |
|
337 lemma distinct_early_app: |
|
338 shows " rdistinct (rs @ rsb) rset = rdistinct (rdistinct rs {} @ rsb) rset" |
|
339 apply(induct rsb) |
|
340 apply simp |
|
341 using distinct_early_app1 apply blast |
|
342 by (metis distinct_early_app1 distinct_once_enough empty_subsetI) |
|
343 |
|
344 |
|
345 lemma distinct_eq_interesting1: |
|
346 shows "a \<in> rset \<Longrightarrow> rdistinct (rs @ rsb) rset = rdistinct (rdistinct (a # rs) {} @ rsb) rset" |
|
347 apply(subgoal_tac "rdistinct (rdistinct (a # rs) {} @ rsb) rset = rdistinct (rdistinct rs {} @ rsb) rset") |
|
348 apply(simp only:) |
|
349 using distinct_early_app apply blast |
|
350 by (metis append_Cons distinct_early_app rdistinct.simps(2)) |
|
351 |
|
352 |
|
353 |
|
354 |
|
355 end |