467 apply simp+ |
467 apply simp+ |
468 apply(subgoal_tac "rsimp_ALTs (aa # list @ aaa # lista) = RALTS (aa # list @ aaa # lista)") |
468 apply(subgoal_tac "rsimp_ALTs (aa # list @ aaa # lista) = RALTS (aa # list @ aaa # lista)") |
469 apply simp |
469 apply simp |
470 using rsimpalts_conscons by presburger |
470 using rsimpalts_conscons by presburger |
471 |
471 |
|
472 lemma no0_flts: |
|
473 shows "RZERO \<notin> set (rflts rs)" |
|
474 apply (induct rs) |
|
475 apply simp |
|
476 apply(case_tac a) |
|
477 apply simp+ |
|
478 oops |
472 |
479 |
473 |
480 |
474 |
481 |
475 lemma distinct_flts_no0: |
482 lemma distinct_flts_no0: |
476 shows "rdistinct (rflts rs) (insert RZERO rset) = rdistinct (rflts rs) rset" |
483 shows " rflts (map rsimp (rdistinct rs (insert RZERO rset))) = |
477 apply(induct rs) |
484 rflts (map rsimp (rdistinct rs rset)) " |
478 apply simp |
485 |
479 apply(case_tac a) |
486 apply(induct rs arbitrary: rset) |
480 using rflts.simps(2) apply presburger |
487 apply simp |
481 sorry |
488 apply(case_tac a) |
|
489 apply simp+ |
|
490 apply (smt (verit, ccfv_SIG) rflts.simps(2) rflts.simps(3) rflts_def_idiot) |
|
491 prefer 2 |
|
492 apply simp |
|
493 by (smt (verit, ccfv_threshold) Un_insert_right insert_iff list.simps(9) rdistinct.simps(2) rflts.simps(2) rflts.simps(3) rflts_def_idiot rrexp.distinct(7)) |
|
494 |
482 |
495 |
483 |
496 |
484 lemma simp_der_flts: |
497 lemma simp_der_flts: |
485 shows "rsimp (RALTS (rdistinct (map (rder x) (rflts rs)) rset))= |
498 shows "rsimp (RALTS (rdistinct (map (rder x) (rflts rs)) rset))= |
486 rsimp (RALTS (rdistinct (rflts (map (rder x) rs)) rset))" |
499 rsimp (RALTS (rdistinct (rflts (map (rder x) rs)) rset))" |
487 |
500 |
488 apply(induct rs arbitrary: rset) |
501 apply(induct rs) |
489 apply simp |
502 apply simp |
490 apply(case_tac a) |
503 apply(case_tac a) |
491 apply simp |
504 apply simp |
492 apply(case_tac "RZERO \<in> rset") |
505 apply(case_tac "RZERO \<in> rset") |
493 apply simp |
506 apply simp+ |
494 apply simp |
507 using distinct_flts_no0 apply presburger |
|
508 apply (case_tac "x = x3") |
|
509 prefer 2 |
|
510 apply simp |
|
511 using distinct_flts_no0 apply presburger |
|
512 apply(case_tac "RONE \<in> rset") |
|
513 apply simp+ |
495 |
514 |
496 sorry |
515 sorry |
497 |
516 |
498 |
517 |
499 lemma simp_der_pierce_flts: |
518 lemma simp_der_pierce_flts: |