equal
deleted
inserted
replaced
33 apply (simp_all add: pow2_def) |
33 apply (simp_all add: pow2_def) |
34 apply (rule_tac m1="2" and n1="nat (2 + int na)" in ssubst[OF realpow_num_eq_if]) |
34 apply (rule_tac m1="2" and n1="nat (2 + int na)" in ssubst[OF realpow_num_eq_if]) |
35 by (auto simp add: h) |
35 by (auto simp add: h) |
36 show ?thesis |
36 show ?thesis |
37 proof (induct a) |
37 proof (induct a) |
38 case (1 n) |
38 case (nonneg n) |
39 from pos show ?case by (simp add: algebra_simps) |
39 from pos show ?case by (simp add: algebra_simps) |
40 next |
40 next |
41 case (2 n) |
41 case (neg n) |
42 show ?case |
42 show ?case |
43 apply (auto) |
43 apply (auto) |
44 apply (subst pow2_neg[of "- int n"]) |
44 apply (subst pow2_neg[of "- int n"]) |
45 apply (subst pow2_neg[of "-1 - int n"]) |
45 apply (subst pow2_neg[of "-1 - int n"]) |
46 apply (auto simp add: g pos) |
46 apply (auto simp add: g pos) |
48 qed |
48 qed |
49 qed |
49 qed |
50 |
50 |
51 lemma pow2_add: "pow2 (a+b) = (pow2 a) * (pow2 b)" |
51 lemma pow2_add: "pow2 (a+b) = (pow2 a) * (pow2 b)" |
52 proof (induct b) |
52 proof (induct b) |
53 case (1 n) |
53 case (nonneg n) |
54 show ?case |
54 show ?case |
55 proof (induct n) |
55 proof (induct n) |
56 case 0 |
56 case 0 |
57 show ?case by simp |
57 show ?case by simp |
58 next |
58 next |
59 case (Suc m) |
59 case (Suc m) |
60 show ?case by (auto simp add: algebra_simps pow2_add1 1 Suc) |
60 show ?case by (auto simp add: algebra_simps pow2_add1 nonneg Suc) |
61 qed |
61 qed |
62 next |
62 next |
63 case (2 n) |
63 case (neg n) |
64 show ?case |
64 show ?case |
65 proof (induct n) |
65 proof (induct n) |
66 case 0 |
66 case 0 |
67 show ?case |
67 show ?case |
68 apply (auto) |
68 apply (auto) |