equal
deleted
inserted
replaced
74 "nibble_of_nat 14 = NibbleE" |
74 "nibble_of_nat 14 = NibbleE" |
75 "nibble_of_nat 15 = NibbleF" |
75 "nibble_of_nat 15 = NibbleF" |
76 unfolding nibble_of_nat_def Let_def by auto |
76 unfolding nibble_of_nat_def Let_def by auto |
77 |
77 |
78 lemmas nibble_of_nat_code [code func] = nibble_of_nat_simps |
78 lemmas nibble_of_nat_code [code func] = nibble_of_nat_simps |
79 [simplified nat_number Let_def not_neg_number_of_Pls neg_number_of_BIT if_False add_0 add_Suc] |
79 [simplified nat_number Let_def not_neg_number_of_Pls neg_number_of_Bit0 neg_number_of_Bit1 if_False add_0 add_Suc] |
80 |
80 |
81 lemma nibble_of_nat_of_nibble: "nibble_of_nat (nat_of_nibble n) = n" |
81 lemma nibble_of_nat_of_nibble: "nibble_of_nat (nat_of_nibble n) = n" |
82 by (cases n) (simp_all only: nat_of_nibble.simps nibble_of_nat_simps) |
82 by (cases n) (simp_all only: nat_of_nibble.simps nibble_of_nat_simps) |
83 |
83 |
84 lemma nat_of_nibble_of_nat: "nat_of_nibble (nibble_of_nat n) = n mod 16" |
84 lemma nat_of_nibble_of_nat: "nat_of_nibble (nibble_of_nat n) = n mod 16" |