equal
deleted
inserted
replaced
174 instance proof |
174 instance proof |
175 qed (auto simp add: code_numeral left_distrib div_mult_self1) |
175 qed (auto simp add: code_numeral left_distrib div_mult_self1) |
176 |
176 |
177 end |
177 end |
178 |
178 |
179 lemma zero_code_numeral_code [code_inline, code]: |
179 lemma zero_code_numeral_code [code, code_unfold]: |
180 "(0\<Colon>code_numeral) = Numeral0" |
180 "(0\<Colon>code_numeral) = Numeral0" |
181 by (simp add: number_of_code_numeral_def Pls_def) |
181 by (simp add: number_of_code_numeral_def Pls_def) |
182 lemma [code_post]: "Numeral0 = (0\<Colon>code_numeral)" |
182 lemma [code_post]: "Numeral0 = (0\<Colon>code_numeral)" |
183 using zero_code_numeral_code .. |
183 using zero_code_numeral_code .. |
184 |
184 |
185 lemma one_code_numeral_code [code_inline, code]: |
185 lemma one_code_numeral_code [code, code_unfold]: |
186 "(1\<Colon>code_numeral) = Numeral1" |
186 "(1\<Colon>code_numeral) = Numeral1" |
187 by (simp add: number_of_code_numeral_def Pls_def Bit1_def) |
187 by (simp add: number_of_code_numeral_def Pls_def Bit1_def) |
188 lemma [code_post]: "Numeral1 = (1\<Colon>code_numeral)" |
188 lemma [code_post]: "Numeral1 = (1\<Colon>code_numeral)" |
189 using one_code_numeral_code .. |
189 using one_code_numeral_code .. |
190 |
190 |