equal
deleted
inserted
replaced
492 apply simp |
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)) |
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 |
494 |
495 |
495 |
496 |
496 |
|
497 lemma rflts_fltsder_derflts: |
|
498 shows "rflts (map rsimp (rdistinct (map (rder x3) (rflts rs)) rset)) = |
|
499 rflts (map rsimp (rdistinct (rflts (map (rder x3) rs)) rset))" |
|
500 sorry |
|
501 |
|
502 |
497 lemma simp_der_flts: |
503 lemma simp_der_flts: |
498 shows "rsimp (RALTS (rdistinct (map (rder x) (rflts rs)) rset))= |
504 shows "rsimp (RALTS (rdistinct (map (rder x) (rflts rs)) rset))= |
499 rsimp (RALTS (rdistinct (rflts (map (rder x) rs)) rset))" |
505 rsimp (RALTS (rdistinct (rflts (map (rder x) rs)) rset))" |
500 |
506 |
501 apply(induct rs) |
507 apply(induct rs arbitrary: rset) |
502 apply simp |
508 apply simp |
503 apply(case_tac a) |
509 apply(case_tac a) |
504 apply simp |
510 apply simp |
505 apply(case_tac "RZERO \<in> rset") |
511 apply(case_tac "RZERO \<in> rset") |
506 apply simp+ |
512 apply simp+ |