equal
deleted
inserted
replaced
29 done |
29 done |
30 |
30 |
31 lemma number_of_pred: "number_of(bin_pred w) = (- 1 + number_of w ::'a::number_ring)" |
31 lemma number_of_pred: "number_of(bin_pred w) = (- 1 + number_of w ::'a::number_ring)" |
32 apply (induct_tac "w") |
32 apply (induct_tac "w") |
33 apply (simp_all add: number_of add_assoc [symmetric]) |
33 apply (simp_all add: number_of add_assoc [symmetric]) |
34 apply (simp add: add_ac) |
|
35 done |
34 done |
36 |
35 |
37 lemma number_of_minus: "number_of(bin_minus w) = (- (number_of w)::'a::number_ring)" |
36 lemma number_of_minus: "number_of(bin_minus w) = (- (number_of w)::'a::number_ring)" |
38 apply (induct_tac "w") |
37 apply (induct_tac "w") |
39 apply (simp_all del: bin_pred_Pls bin_pred_Min bin_pred_BIT |
38 apply (simp_all del: bin_pred_Pls bin_pred_Min bin_pred_BIT |
47 apply (simp add: number_of) |
46 apply (simp add: number_of) |
48 apply (simp add: number_of number_of_pred) |
47 apply (simp add: number_of number_of_pred) |
49 apply (rule allI) |
48 apply (rule allI) |
50 apply (induct_tac "w") |
49 apply (induct_tac "w") |
51 apply (simp_all add: number_of bin_add_BIT_BIT number_of_succ number_of_pred add_ac) |
50 apply (simp_all add: number_of bin_add_BIT_BIT number_of_succ number_of_pred add_ac) |
52 apply (simp add: add_left_commute [of "1::'a::number_ring"]) |
|
53 done |
51 done |
54 |
52 |
55 lemma number_of_mult: |
53 lemma number_of_mult: |
56 "number_of(bin_mult v w) = (number_of v * number_of w::'a::number_ring)" |
54 "number_of(bin_mult v w) = (number_of v * number_of w::'a::number_ring)" |
57 apply (induct_tac "v", simp add: number_of) |
55 apply (induct_tac "v", simp add: number_of) |
145 show ?thesis |
143 show ?thesis |
146 proof |
144 proof |
147 assume eq: "1 + z + z = 0" |
145 assume eq: "1 + z + z = 0" |
148 have "0 < 1 + (int n + int n)" |
146 have "0 < 1 + (int n + int n)" |
149 by (simp add: le_imp_0_less add_increasing) |
147 by (simp add: le_imp_0_less add_increasing) |
150 also have "... = - (1 + z + z)" |
148 also have "... = - (1 + z + z)" |
151 by (simp add: neg add_assoc [symmetric], simp add: add_commute) |
149 by (simp add: neg add_assoc [symmetric]) |
152 also have "... = 0" by (simp add: eq) |
150 also have "... = 0" by (simp add: eq) |
153 finally have "0<0" .. |
151 finally have "0<0" .. |
154 thus False by blast |
152 thus False by blast |
155 qed |
153 qed |
156 qed |
154 qed |