equal
deleted
inserted
replaced
52 |
52 |
53 lemma size_Cons_lem_eq: |
53 lemma size_Cons_lem_eq: |
54 "y = xa # list ==> size y = Suc k ==> size list = k" |
54 "y = xa # list ==> size y = Suc k ==> size list = k" |
55 by auto |
55 by auto |
56 |
56 |
57 lemmas ls_splits = prod.split prod.split_asm split_if_asm |
57 lemmas ls_splits = prod.split prod.split_asm if_split_asm |
58 |
58 |
59 lemma not_B1_is_B0: "y \<noteq> (1::bit) \<Longrightarrow> y = (0::bit)" |
59 lemma not_B1_is_B0: "y \<noteq> (1::bit) \<Longrightarrow> y = (0::bit)" |
60 by (cases y) auto |
60 by (cases y) auto |
61 |
61 |
62 lemma B1_ass_B0: |
62 lemma B1_ass_B0: |