equal
deleted
inserted
replaced
1 |
1 |
2 theory BitCoded |
2 theory BitCodedCT |
3 imports "Lexer" |
3 imports "Lexer" |
4 begin |
4 begin |
5 |
5 |
6 section \<open>Bit-Encodings\<close> |
6 section \<open>Bit-Encodings\<close> |
7 |
7 |
2754 lemma patience_good5: |
2754 lemma patience_good5: |
2755 assumes "bsimp r = AALTs x y" |
2755 assumes "bsimp r = AALTs x y" |
2756 shows " \<exists> a aa list. y = a#aa#list" |
2756 shows " \<exists> a aa list. y = a#aa#list" |
2757 by (metis Nil_is_map_conv arexp.simps(13) assms bsimp_AALTs.elims flts1 good.simps(5) good1 k0a) |
2757 by (metis Nil_is_map_conv arexp.simps(13) assms bsimp_AALTs.elims flts1 good.simps(5) good1 k0a) |
2758 |
2758 |
2759 |
2759 (*SAD*) |
2760 (*this does not hold actually |
2760 (*this does not hold actually |
2761 lemma bsimp_equiv0: |
2761 lemma bsimp_equiv0: |
2762 shows "bsimp(bsimp r) = bsimp(bsimp (AALTs [] [r]))" |
2762 shows "bsimp(bsimp r) = bsimp(bsimp (AALTs [] [r]))" |
2763 apply(simp) |
2763 apply(simp) |
2764 apply(case_tac "bsimp r") |
2764 apply(case_tac "bsimp r") |
2879 done |
2879 done |
2880 lemma map_application2: |
2880 lemma map_application2: |
2881 shows"map f [a,b] = [f a, f b]" |
2881 shows"map f [a,b] = [f a, f b]" |
2882 apply simp |
2882 apply simp |
2883 done |
2883 done |
2884 |
2884 (*SAD*) |
2885 (* bsimp (bder c (bsimp_AALTs x51 (flts [bsimp a1, bsimp a2]))) = |
2885 (* bsimp (bder c (bsimp_AALTs x51 (flts [bsimp a1, bsimp a2]))) = |
2886 bsimp (AALT x51 (bder c (bsimp a1)) (bder c (bsimp a2)))*) |
2886 bsimp (AALT x51 (bder c (bsimp a1)) (bder c (bsimp a2)))*) |
2887 (*This equality does not hold*) |
2887 (*This equality does not hold*) |
2888 lemma medium01: |
2888 lemma medium01: |
2889 assumes " (bder c a1 = AZERO) " |
2889 assumes " (bder c a1 = AZERO) " |