46 apply(subgoal_tac "rdistinct ((a # as) @ [ab]) rset1 = rdistinct (a # as) rset1") |
48 apply(subgoal_tac "rdistinct ((a # as) @ [ab]) rset1 = rdistinct (a # as) rset1") |
47 apply simp |
49 apply simp |
48 by (metis append_Cons insert_iff insert_is_Un rdistinct.simps(2)) |
50 by (metis append_Cons insert_iff insert_is_Un rdistinct.simps(2)) |
49 |
51 |
50 |
52 |
|
53 lemma distinct_removes_middle: |
|
54 shows "\<lbrakk>a \<in> set as\<rbrakk> |
|
55 \<Longrightarrow> rdistinct (as @ as2) rset = rdistinct (as @ [a] @ as2) rset" |
|
56 and "rdistinct (ab # as @ [ab] @ as3) rset1 = rdistinct (ab # as @ as3) rset1" |
|
57 apply(induct as arbitrary: rset rset1 ab as2 as3 a) |
|
58 apply simp |
|
59 apply simp |
|
60 apply(case_tac "a \<in> rset") |
|
61 apply simp |
|
62 apply metis |
|
63 apply simp |
|
64 apply (metis insertI1) |
|
65 apply(case_tac "a = ab") |
|
66 apply simp |
|
67 apply(case_tac "ab \<in> rset") |
|
68 apply simp |
|
69 apply presburger |
|
70 apply (meson insertI1) |
|
71 apply(case_tac "a \<in> rset") |
|
72 apply (metis (no_types, opaque_lifting) Un_insert_left append_Cons insert_iff rdistinct.simps(2) sup_bot_left) |
|
73 apply(case_tac "ab \<in> rset") |
|
74 apply simp |
|
75 apply (meson insert_iff) |
|
76 apply simp |
|
77 by (metis insertI1) |
|
78 |
|
79 |
|
80 lemma distinct_removes_middle3: |
|
81 shows "\<lbrakk>a \<in> set as\<rbrakk> |
|
82 \<Longrightarrow> rdistinct (as @ a #as2) rset = rdistinct (as @ as2) rset" |
|
83 using distinct_removes_middle(1) by fastforce |
|
84 |
51 lemma distinct_removes_last2: |
85 lemma distinct_removes_last2: |
52 shows "\<lbrakk>(a::rrexp) \<in> set as\<rbrakk> |
86 shows "\<lbrakk>a \<in> set as\<rbrakk> |
53 \<Longrightarrow> rdistinct as rset = rdistinct (as @ [a]) rset" |
87 \<Longrightarrow> rdistinct as rset = rdistinct (as @ [a]) rset" |
54 using distinct_removes_last(1) by presburger |
88 by (simp add: distinct_removes_last(1)) |
55 |
89 |
56 lemma distinct_append_simp: |
90 lemma distinct_removes_middle2: |
57 shows " rsimp (rsimp_ALTs rs1) = rsimp (rsimp_ALTs rs2) \<Longrightarrow> |
91 shows "a \<in> set as \<Longrightarrow> rdistinct (as @ [a] @ rs) {} = rdistinct (as @ rs) {}" |
58 rsimp (rsimp_ALTs (f a # rs1)) = |
92 by (metis distinct_removes_middle(1)) |
59 rsimp (rsimp_ALTs (f a # rs2))" |
93 |
60 apply(case_tac rs1) |
94 lemma distinct_removes_list: |
61 apply simp |
95 shows "\<lbrakk>a \<in> set as; \<forall>r \<in> set rs. r \<in> set as\<rbrakk> \<Longrightarrow> rdistinct (as @ rs) {} = rdistinct as {}" |
62 apply(case_tac rs2) |
96 apply(induct rs) |
63 apply simp |
97 apply simp+ |
64 apply simp |
98 apply(subgoal_tac "rdistinct (as @ aa # rs) {} = rdistinct (as @ rs) {}") |
65 prefer 2 |
99 prefer 2 |
66 apply(case_tac list) |
100 apply (metis append_Cons append_Nil distinct_removes_middle(1)) |
67 apply(case_tac rs2) |
101 by presburger |
68 apply simp |
|
69 using add0_isomorphic apply blast |
|
70 apply simp |
|
71 sorry |
|
72 |
|
73 (* apply (smt (z3) append.right_neutral empty_iff list.distinct(1) list.inject no_alt_short_list_after_simp no_further_dB_after_simp rdistinct.elims rflts.elims rflts.simps(2) rsimp_ALTs.simps(1) rsimp_ALTs.simps(2)))*) |
|
74 |
|
75 |
|
76 |
102 |
77 |
103 |
78 |
104 |
79 lemma simp_rdistinct_f: shows |
105 lemma simp_rdistinct_f: shows |
80 "f ` rset = frset \<Longrightarrow> rsimp (rsimp_ALTs (map f (rdistinct rs rset))) = rsimp (rsimp_ALTs (rdistinct (map f rs) frset)) " |
106 "f ` rset = frset \<Longrightarrow> rsimp (rsimp_ALTs (map f (rdistinct rs rset))) = |
|
107 rsimp (rsimp_ALTs (rdistinct (map f rs) frset)) " |
81 apply(induct rs arbitrary: rset) |
108 apply(induct rs arbitrary: rset) |
82 apply simp |
109 apply simp |
83 apply(case_tac "a \<in> rset") |
110 apply(case_tac "a \<in> rset") |
84 apply(case_tac " f a \<in> frset") |
111 apply(case_tac " f a \<in> frset") |
85 apply simp |
112 apply simp |
207 lemma simp_more_flts: |
234 lemma simp_more_flts: |
208 shows "rsimp (rsimp_ALTs (rdistinct rs {})) = rsimp (rsimp_ALTs (rdistinct (rflts rs) {}))" |
235 shows "rsimp (rsimp_ALTs (rdistinct rs {})) = rsimp (rsimp_ALTs (rdistinct (rflts rs) {}))" |
209 |
236 |
210 oops |
237 oops |
211 |
238 |
|
239 lemma simp_more_distinct1: |
|
240 shows "rsimp (rsimp_ALTs rs) = rsimp (rsimp_ALTs (rdistinct rs {}))" |
|
241 apply(induct rs) |
|
242 apply simp |
|
243 apply simp |
|
244 oops |
|
245 |
|
246 |
|
247 (* |
|
248 \<and> |
|
249 rsimp (rsimp_ALTs (rsb @ (rdistinct rs (set rsb)))) = |
|
250 rsimp (rsimp_ALTs (rsb @ (rdistinct (rflts rs) (set rsb)))) |
|
251 *) |
|
252 lemma simp_removes_duplicate2: |
|
253 shows "a " |
|
254 |
|
255 oops |
|
256 |
|
257 lemma flts_removes0: |
|
258 shows " rflts (rs @ [RZERO]) = |
|
259 rflts rs" |
|
260 apply(induct rs) |
|
261 apply simp |
|
262 by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot) |
|
263 |
|
264 lemma flts_keeps1: |
|
265 shows " rflts (rs @ [RONE]) = |
|
266 rflts rs @ [RONE] " |
|
267 apply (induct rs) |
|
268 apply simp |
|
269 by (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot) |
|
270 |
|
271 lemma flts_keeps_others: |
|
272 shows "\<lbrakk>a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1\<rbrakk> \<Longrightarrow>rflts (rs @ [a]) = rflts rs @ [a]" |
|
273 apply(induct rs) |
|
274 apply simp |
|
275 apply (simp add: rflts_def_idiot) |
|
276 apply(case_tac a) |
|
277 apply simp |
|
278 using flts_keeps1 apply blast |
|
279 apply (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot) |
|
280 apply (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot) |
|
281 apply blast |
|
282 by (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot) |
|
283 |
|
284 |
|
285 lemma rflts_def_idiot2: |
|
286 shows "\<lbrakk>a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1; a \<in> set rs\<rbrakk> \<Longrightarrow> a \<in> set (rflts rs)" |
|
287 apply(induct rs) |
|
288 apply simp |
|
289 by (metis append.assoc in_set_conv_decomp insert_iff list.simps(15) rflts.simps(2) rflts.simps(3) rflts_def_idiot) |
|
290 |
|
291 lemma rflts_spills_last: |
|
292 shows "a = RALTS rs \<Longrightarrow> rflts (rs1 @ [a]) = rflts rs1 @ rs" |
|
293 apply (induct rs1) |
|
294 apply simp |
|
295 by (metis append.assoc append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot) |
|
296 |
|
297 |
|
298 lemma spilled_alts_contained: |
|
299 shows "\<lbrakk>a = RALTS rs ; a \<in> set rs1\<rbrakk> \<Longrightarrow> \<forall>r \<in> set rs. r \<in> set (rflts rs1)" |
|
300 apply(induct rs1) |
|
301 apply simp |
|
302 apply(case_tac "a = aa") |
|
303 apply simp |
|
304 apply(subgoal_tac " a \<in> set rs1") |
|
305 prefer 2 |
|
306 apply (meson set_ConsD) |
|
307 apply(case_tac aa) |
|
308 using rflts.simps(2) apply presburger |
|
309 apply fastforce |
|
310 apply fastforce |
|
311 apply fastforce |
|
312 apply fastforce |
|
313 by fastforce |
|
314 |
|
315 lemma distinct_removes_duplicate_flts: |
|
316 shows " a \<in> set rsa |
|
317 \<Longrightarrow> rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} = |
|
318 rdistinct (rflts (map rsimp rsa)) {}" |
|
319 apply(subgoal_tac "rsimp a \<in> set (map rsimp rsa)") |
|
320 prefer 2 |
|
321 apply simp |
|
322 apply(induct "rsimp a") |
|
323 apply simp |
|
324 using flts_removes0 apply presburger |
|
325 apply(subgoal_tac " rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} = |
|
326 rdistinct (rflts (map rsimp rsa @ [RONE])) {}") |
|
327 apply (simp only:) |
|
328 apply(subst flts_keeps1) |
|
329 apply (metis distinct_removes_last2 rflts_def_idiot2 rrexp.simps(20) rrexp.simps(6)) |
|
330 apply presburger |
|
331 apply(subgoal_tac " rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} = |
|
332 rdistinct ((rflts (map rsimp rsa)) @ [RCHAR x]) {}") |
|
333 apply (simp only:) |
|
334 prefer 2 |
|
335 apply (metis flts_keeps_others rrexp.distinct(21) rrexp.distinct(3)) |
|
336 apply (metis distinct_removes_last2 rflts_def_idiot2 rrexp.distinct(21) rrexp.distinct(3)) |
|
337 |
|
338 apply (metis distinct_removes_last2 flts_keeps_others rflts_def_idiot2 rrexp.distinct(25) rrexp.distinct(5)) |
|
339 prefer 2 |
|
340 apply (metis distinct_removes_last2 flts_keeps_others flts_removes0 rflts_def_idiot2 rrexp.distinct(29)) |
|
341 apply(subgoal_tac "rflts (map rsimp rsa @ [rsimp a]) = rflts (map rsimp rsa) @ x") |
|
342 prefer 2 |
|
343 apply (simp add: rflts_spills_last) |
|
344 apply(simp only:) |
|
345 apply(subgoal_tac "\<forall> r \<in> set x. r \<in> set (rflts (map rsimp rsa))") |
|
346 prefer 2 |
|
347 using spilled_alts_contained apply presburger |
|
348 by (metis append_self_conv distinct_removes_list in_set_conv_decomp rev_exhaust) |
|
349 |
|
350 lemma flts_middle0: |
|
351 shows "rflts (rsa @ RZERO # rsb) = rflts (rsa @ rsb)" |
|
352 apply(induct rsa) |
|
353 apply simp |
|
354 by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot) |
|
355 |
|
356 lemma flts_middle01: |
|
357 shows "rflts (rsa @ [RZERO] @ rsb) = rflts (rsa @ rsb)" |
|
358 by (simp add: flts_middle0) |
|
359 |
|
360 lemma flts_append1: |
|
361 shows "\<lbrakk>a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1; a \<in> set rs\<rbrakk> \<Longrightarrow> |
|
362 rflts (rsa @ [a] @ rsb) = rflts rsa @ [a] @ (rflts rsb)" |
|
363 apply(induct rsa arbitrary: rsb) |
|
364 apply simp |
|
365 using rflts_def_idiot apply presburger |
|
366 apply(case_tac aa) |
|
367 apply simp+ |
|
368 done |
|
369 |
|
370 lemma flts_append: |
|
371 shows "rflts (rs1 @ rs2) = rflts rs1 @ rflts rs2" |
|
372 apply(induct rs1) |
|
373 apply simp |
|
374 apply(case_tac a) |
|
375 apply simp+ |
|
376 done |
|
377 |
|
378 lemma simp_removes_duplicate1: |
|
379 shows " a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ [a])) = rsimp (RALTS (rsa))" |
|
380 and " rsimp (RALTS (a1 # rsa @ [a1])) = rsimp (RALTS (a1 # rsa))" |
|
381 apply(induct rsa arbitrary: a1) |
|
382 apply simp |
|
383 apply simp |
|
384 prefer 2 |
|
385 apply(case_tac "a = aa") |
|
386 apply simp |
|
387 apply simp |
|
388 apply (metis Cons_eq_appendI Cons_eq_map_conv distinct_removes_duplicate_flts list.set_intros(2)) |
|
389 apply (metis append_Cons append_Nil distinct_removes_duplicate_flts list.set_intros(1) list.simps(8) list.simps(9)) |
|
390 by (metis (mono_tags, lifting) append_Cons distinct_removes_duplicate_flts list.set_intros(1) list.simps(8) list.simps(9) map_append rsimp.simps(2)) |
|
391 |
|
392 lemma simp_removes_duplicate2: |
|
393 shows "a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ [a] @ rsb)) = rsimp (RALTS (rsa @ rsb))" |
|
394 apply(induct rsb arbitrary: rsa) |
|
395 apply simp |
|
396 using distinct_removes_duplicate_flts apply auto[1] |
|
397 by (metis append.assoc head_one_more_simp rsimp.simps(2) simp_flatten simp_removes_duplicate1(1)) |
|
398 |
|
399 lemma simp_removes_duplicate3: |
|
400 shows "a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ a # rsb)) = rsimp (RALTS (rsa @ rsb))" |
|
401 using simp_removes_duplicate2 by auto |
|
402 |
|
403 lemma distinct_removes_middle4: |
|
404 shows "a \<in> set rsa \<Longrightarrow> rdistinct (rsa @ [a] @ rsb) rset = rdistinct (rsa @ rsb) rset" |
|
405 using distinct_removes_middle(1) by fastforce |
|
406 |
|
407 lemma distinct_removes_middle_list: |
|
408 shows "\<forall>a \<in> set x. a \<in> set rsa \<Longrightarrow> rdistinct (rsa @ x @ rsb) rset = rdistinct (rsa @ rsb) rset" |
|
409 apply(induct x) |
|
410 apply simp |
|
411 by (simp add: distinct_removes_middle3) |
|
412 |
|
413 |
|
414 lemma distinct_removes_duplicate_flts2: |
|
415 shows " a \<in> set rsa |
|
416 \<Longrightarrow> rdistinct (rflts (rsa @ [a] @ rsb)) {} = |
|
417 rdistinct (rflts (rsa @ rsb)) {}" |
|
418 apply(induct a arbitrary: rsb) |
|
419 using flts_middle01 apply presburger |
|
420 apply(subgoal_tac "rflts (rsa @ [RONE] @ rsb) = rflts rsa @ [RONE] @ rflts rsb") |
|
421 prefer 2 |
|
422 using flts_append1 apply blast |
|
423 apply simp |
|
424 apply(subgoal_tac "RONE \<in> set (rflts rsa)") |
|
425 prefer 2 |
|
426 using rflts_def_idiot2 apply blast |
|
427 apply(subst distinct_removes_middle3) |
|
428 apply simp |
|
429 using flts_append apply presburger |
|
430 apply simp |
|
431 apply (metis distinct_removes_middle3 flts_append in_set_conv_decomp rflts.simps(5)) |
|
432 apply (metis distinct_removes_middle(1) flts_append flts_append1 rflts_def_idiot2 rrexp.distinct(25) rrexp.distinct(5)) |
|
433 apply(subgoal_tac "rflts (rsa @ [RALTS x] @ rsb) = rflts rsa @ x @ rflts rsb") |
|
434 prefer 2 |
|
435 apply (simp add: flts_append) |
|
436 apply (simp only:) |
|
437 |
|
438 apply(subgoal_tac "\<forall>r1 \<in> set x. r1 \<in> set (rflts rsa)") |
|
439 prefer 2 |
|
440 using spilled_alts_contained apply blast |
|
441 apply(subst flts_append) |
|
442 using distinct_removes_middle_list apply blast |
|
443 using distinct_removes_middle2 flts_append rflts_def_idiot2 by fastforce |
|
444 |
|
445 |
|
446 lemma simp_removes_duplicate: |
|
447 shows "a \<in> set rsa \<Longrightarrow> rsimp (rsimp_ALTs (rsa @ a # rs)) = rsimp (rsimp_ALTs (rsa @ rs))" |
|
448 apply(subgoal_tac "rsimp (rsimp_ALTs (rsa @ a # rs)) = rsimp (RALTS (rsa @ a # rs))") |
|
449 prefer 2 |
|
450 apply (smt (verit, best) Cons_eq_append_conv append_is_Nil_conv empty_set equals0D list.distinct(1) rsimp_ALTs.elims) |
|
451 apply(simp only:) |
|
452 apply simp |
|
453 apply(subgoal_tac "(rdistinct (rflts (map rsimp rsa @ rsimp a # map rsimp rs)) {}) = (rdistinct (rflts (map rsimp rsa @ map rsimp rs)) {})") |
|
454 apply(simp only:) |
|
455 prefer 2 |
|
456 apply(subgoal_tac "rsimp a \<in> set (map rsimp rsa)") |
|
457 prefer 2 |
|
458 apply simp |
|
459 using distinct_removes_duplicate_flts2 apply force |
|
460 apply(case_tac rsa) |
|
461 apply simp |
|
462 apply(case_tac rs) |
|
463 apply simp |
|
464 apply(case_tac list) |
|
465 apply simp |
|
466 using idem_after_simp1 apply presburger |
|
467 apply simp+ |
|
468 apply(subgoal_tac "rsimp_ALTs (aa # list @ aaa # lista) = RALTS (aa # list @ aaa # lista)") |
|
469 apply simp |
|
470 using rsimpalts_conscons by presburger |
|
471 |
|
472 lemma simp_der_pierce_flts: |
|
473 shows " rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {})) = |
|
474 rsimp (rsimp_ALTs (rdistinct (rflts (map (rder x) (map (rsimp \<circ> (\<lambda>r. rders_simp r xs)) rs))) {}))" |
|
475 oops |
|
476 |
212 |
477 |
213 |
478 |
214 lemma simp_more_distinct: |
479 lemma simp_more_distinct: |
215 shows "rsimp (rsimp_ALTs (rsa @ rs)) = rsimp (rsimp_ALTs (rsa @ (rdistinct rs (set rsa)))) \<and> |
480 shows "rsimp (rsimp_ALTs (rsa @ rs)) = rsimp (rsimp_ALTs (rsa @ (rdistinct rs (set rsa)))) " |
216 rsimp (rsimp_ALTs (rsb @ (rdistinct rs (set rsb)))) = |
481 and "a1 \<in> set rsb \<Longrightarrow> rsimp (rsimp_ALTs (rsb @ a1 # rs)) = rsimp (rsimp_ALTs (rsb @ rs))" |
217 rsimp (rsimp_ALTs (rsb @ (rdistinct (rflts rs) (set rsb))))" |
482 apply(induct rs arbitrary: rsa rsb a1) |
218 apply(induct rs arbitrary: rsa rsb) |
483 apply simp |
219 apply simp |
484 apply simp |
|
485 apply(case_tac " a \<in> set rsa") |
|
486 apply simp |
|
487 prefer 2 |
|
488 apply simp |
|
489 apply(drule_tac x = "rsa @ [a]" in meta_spec) |
|
490 apply simp |
|
491 |
220 |
492 |
221 sorry |
493 sorry |
222 |
494 |
223 lemma non_empty_list: |
495 lemma non_empty_list: |
224 shows "a \<in> set as \<Longrightarrow> as \<noteq> []" |
496 shows "a \<in> set as \<Longrightarrow> as \<noteq> []" |