equal
deleted
inserted
replaced
314 apply arith |
314 apply arith |
315 apply (simp add: bin_last_def bin_rest_def Bit_def) |
315 apply (simp add: bin_last_def bin_rest_def Bit_def) |
316 apply (clarsimp simp: mod_mult_mult1 [symmetric] |
316 apply (clarsimp simp: mod_mult_mult1 [symmetric] |
317 zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2 [THEN sym]]]) |
317 zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2 [THEN sym]]]) |
318 apply (rule trans [symmetric, OF _ emep1]) |
318 apply (rule trans [symmetric, OF _ emep1]) |
319 apply auto |
319 apply auto |
320 apply (auto simp: even_iff_mod_2_eq_zero) |
|
321 done |
320 done |
322 |
321 |
323 subsection "Simplifications for (s)bintrunc" |
322 subsection "Simplifications for (s)bintrunc" |
324 |
323 |
325 lemma bintrunc_n_0 [simp]: "bintrunc n 0 = 0" |
324 lemma bintrunc_n_0 [simp]: "bintrunc n 0 = 0" |