equal
deleted
inserted
replaced
26 have g: "! a b. a - -1 = a + (1::int)" by arith |
26 have g: "! a b. a - -1 = a + (1::int)" by arith |
27 have pos: "! n. pow2 (int n + 1) = 2 * pow2 (int n)" |
27 have pos: "! n. pow2 (int n + 1) = 2 * pow2 (int n)" |
28 apply (auto, induct_tac n) |
28 apply (auto, induct_tac n) |
29 apply (simp_all add: pow2_def) |
29 apply (simp_all add: pow2_def) |
30 apply (rule_tac m1="2" and n1="nat (2 + int na)" in ssubst[OF realpow_num_eq_if]) |
30 apply (rule_tac m1="2" and n1="nat (2 + int na)" in ssubst[OF realpow_num_eq_if]) |
31 apply (auto simp add: h) |
31 by (auto simp add: h) |
32 apply arith |
|
33 done |
|
34 show ?thesis |
32 show ?thesis |
35 proof (induct a) |
33 proof (induct a) |
36 case (1 n) |
34 case (1 n) |
37 from pos show ?case by (simp add: ring_eq_simps) |
35 from pos show ?case by (simp add: ring_eq_simps) |
38 next |
36 next |