equal
deleted
inserted
replaced
460 using good_flatten_aux by blast |
460 using good_flatten_aux by blast |
461 |
461 |
462 |
462 |
463 lemma simp_flatten3: |
463 lemma simp_flatten3: |
464 shows "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))" |
464 shows "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))" |
|
465 proof - |
|
466 have "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = |
|
467 rsimp (RALTS (map rsimp rsa @ [rsimp (RALTS rs)] @ map rsimp rsb)) " |
|
468 by (metis append_Cons append_Nil list.simps(9) map_append simp_flatten_aux0) |
|
469 apply(simp only:) |
|
470 |
|
471 oops |
|
472 |
|
473 lemma simp_flatten3: |
|
474 shows "rsimp (RALTS (rsa @ [RALTS rs ] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))" |
465 apply(subgoal_tac "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = |
475 apply(subgoal_tac "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = |
466 rsimp (RALTS (map rsimp rsa @ [rsimp (RALTS rs)] @ map rsimp rsb)) ") |
476 rsimp (RALTS (map rsimp rsa @ [rsimp (RALTS rs)] @ map rsimp rsb)) ") |
467 prefer 2 |
477 prefer 2 |
468 apply (metis append.left_neutral append_Cons list.simps(9) map_append simp_flatten_aux0) |
478 apply (metis append.left_neutral append_Cons list.simps(9) map_append simp_flatten_aux0) |
469 apply (simp only:) |
479 apply (simp only:) |
1535 then have "created_by_star (rder c r1)" |
1545 then have "created_by_star (rder c r1)" |
1536 using cbs_ders_cbs by blast |
1546 using cbs_ders_cbs by blast |
1537 then have "created_by_star (rder c r2)" |
1547 then have "created_by_star (rder c r2)" |
1538 using "2.hyps"(3) cbs_ders_cbs by auto |
1548 using "2.hyps"(3) cbs_ders_cbs by auto |
1539 then show ?case |
1549 then show ?case |
1540 apply simp |
1550 |
1541 by (simp add: "2.hyps"(2) "2.hyps"(4)) |
1551 by (simp add: "2.hyps"(2) "2.hyps"(4)) |
1542 qed |
1552 qed |
1543 |
1553 |
1544 |
1554 |
1545 |
1555 |