equal
deleted
inserted
replaced
331 by auto |
331 by auto |
332 |
332 |
333 lemma set_decode_plus_power_2: |
333 lemma set_decode_plus_power_2: |
334 "n \<notin> set_decode z \<Longrightarrow> set_decode (2 ^ n + z) = insert n (set_decode z)" |
334 "n \<notin> set_decode z \<Longrightarrow> set_decode (2 ^ n + z) = insert n (set_decode z)" |
335 apply (induct n arbitrary: z, simp_all) |
335 apply (induct n arbitrary: z, simp_all) |
336 apply (rule set_ext, induct_tac x, simp, simp add: even_nat_Suc_div_2) |
336 apply (rule set_eqI, induct_tac x, simp, simp add: even_nat_Suc_div_2) |
337 apply (rule set_ext, induct_tac x, simp, simp add: add_commute) |
337 apply (rule set_eqI, induct_tac x, simp, simp add: add_commute) |
338 done |
338 done |
339 |
339 |
340 lemma finite_set_decode [simp]: "finite (set_decode n)" |
340 lemma finite_set_decode [simp]: "finite (set_decode n)" |
341 apply (induct n rule: nat_less_induct) |
341 apply (induct n rule: nat_less_induct) |
342 apply (case_tac "n = 0", simp) |
342 apply (case_tac "n = 0", simp) |