author | obua |
Tue, 11 May 2004 20:11:08 +0200 | |
changeset 14738 | 83f1a514dcb4 |
parent 14705 | 14b2c22a7e40 |
child 14754 | a080eeeaec14 |
permissions | -rw-r--r-- |
1632 | 1 |
(* Title: HOL/Integ/Bin.thy |
6910 | 2 |
ID: $Id$ |
1632 | 3 |
Authors: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 |
Copyright 1994 University of Cambridge |
|
14705 | 5 |
|
6 |
Ported from ZF to HOL by David Spelt. |
|
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
7 |
*) |
1632 | 8 |
|
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
9 |
header{*Arithmetic on Binary Integers*} |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
10 |
|
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset
|
11 |
theory Bin = IntDef + Numeral: |
1632 | 12 |
|
14738 | 13 |
axclass number_ring \<subseteq> number, comm_ring_1 |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
14 |
number_of_Pls: "number_of bin.Pls = 0" |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
15 |
number_of_Min: "number_of bin.Min = - 1" |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
16 |
number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) + |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
17 |
(number_of w) + (number_of w)" |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
18 |
subsection{*Converting Numerals to Rings: @{term number_of}*} |
1632 | 19 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
20 |
lemmas number_of = number_of_Pls number_of_Min number_of_BIT |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
21 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
22 |
lemma number_of_NCons [simp]: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
23 |
"number_of(NCons w b) = (number_of(w BIT b)::'a::number_ring)" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
24 |
by (induct_tac "w", simp_all add: number_of) |
5491 | 25 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
26 |
lemma number_of_succ: "number_of(bin_succ w) = (1 + number_of w ::'a::number_ring)" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
27 |
apply (induct_tac "w") |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
28 |
apply (simp_all add: number_of add_ac) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
29 |
done |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
30 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
31 |
lemma number_of_pred: "number_of(bin_pred w) = (- 1 + number_of w ::'a::number_ring)" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
32 |
apply (induct_tac "w") |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
33 |
apply (simp_all add: number_of add_assoc [symmetric]) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
34 |
apply (simp add: add_ac) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
35 |
done |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
36 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
37 |
lemma number_of_minus: "number_of(bin_minus w) = (- (number_of w)::'a::number_ring)" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
38 |
apply (induct_tac "w") |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
39 |
apply (simp_all del: bin_pred_Pls bin_pred_Min bin_pred_BIT |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
40 |
add: number_of number_of_succ number_of_pred add_assoc) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
41 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
42 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
43 |
text{*This proof is complicated by the mutual recursion*} |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
44 |
lemma number_of_add [rule_format]: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
45 |
"\<forall>w. number_of(bin_add v w) = (number_of v + number_of w::'a::number_ring)" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
46 |
apply (induct_tac "v") |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
47 |
apply (simp add: number_of) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
48 |
apply (simp add: number_of number_of_pred) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
49 |
apply (rule allI) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
50 |
apply (induct_tac "w") |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
51 |
apply (simp_all add: number_of bin_add_BIT_BIT number_of_succ number_of_pred add_ac) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
52 |
apply (simp add: add_left_commute [of "1::'a::number_ring"]) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
53 |
done |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
54 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
55 |
lemma number_of_mult: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
56 |
"number_of(bin_mult v w) = (number_of v * number_of w::'a::number_ring)" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
57 |
apply (induct_tac "v", simp add: number_of) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
58 |
apply (simp add: number_of number_of_minus) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
59 |
apply (simp add: number_of number_of_add left_distrib add_ac) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
60 |
done |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
61 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
62 |
text{*The correctness of shifting. But it doesn't seem to give a measurable |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
63 |
speed-up.*} |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
64 |
lemma double_number_of_BIT: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
65 |
"(1+1) * number_of w = (number_of (w BIT False) ::'a::number_ring)" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
66 |
apply (induct_tac "w") |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
67 |
apply (simp_all add: number_of number_of_add left_distrib add_ac) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
68 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
69 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
70 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
71 |
text{*Converting numerals 0 and 1 to their abstract versions*} |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
72 |
lemma numeral_0_eq_0 [simp]: "Numeral0 = (0::'a::number_ring)" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
73 |
by (simp add: number_of) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
74 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
75 |
lemma numeral_1_eq_1 [simp]: "Numeral1 = (1::'a::number_ring)" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
76 |
by (simp add: number_of) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
77 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
78 |
text{*Special-case simplification for small constants*} |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
79 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
80 |
text{*Unary minus for the abstract constant 1. Cannot be inserted |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
81 |
as a simprule until later: it is @{text number_of_Min} re-oriented!*} |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
82 |
lemma numeral_m1_eq_minus_1: "(-1::'a::number_ring) = - 1" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
83 |
by (simp add: number_of) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
84 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
85 |
lemma mult_minus1 [simp]: "-1 * z = -(z::'a::number_ring)" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
86 |
by (simp add: numeral_m1_eq_minus_1) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
87 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
88 |
lemma mult_minus1_right [simp]: "z * -1 = -(z::'a::number_ring)" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
89 |
by (simp add: numeral_m1_eq_minus_1) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
90 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
91 |
(*Negation of a coefficient*) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
92 |
lemma minus_number_of_mult [simp]: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
93 |
"- (number_of w) * z = number_of(bin_minus w) * (z::'a::number_ring)" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
94 |
by (simp add: number_of_minus) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
95 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
96 |
text{*Subtraction*} |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
97 |
lemma diff_number_of_eq: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
98 |
"number_of v - number_of w = |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
99 |
(number_of(bin_add v (bin_minus w))::'a::number_ring)" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
100 |
by (simp add: diff_minus number_of_add number_of_minus) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
101 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
102 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
103 |
subsection{*Equality of Binary Numbers*} |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
104 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
105 |
text{*First version by Norbert Voelker*} |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
106 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
107 |
lemma eq_number_of_eq: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
108 |
"((number_of x::'a::number_ring) = number_of y) = |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
109 |
iszero (number_of (bin_add x (bin_minus y)) :: 'a)" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
110 |
by (simp add: iszero_def compare_rls number_of_add number_of_minus) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
111 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
112 |
lemma iszero_number_of_Pls: "iszero ((number_of bin.Pls)::'a::number_ring)" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
113 |
by (simp add: iszero_def numeral_0_eq_0) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
114 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
115 |
lemma nonzero_number_of_Min: "~ iszero ((number_of bin.Min)::'a::number_ring)" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
116 |
by (simp add: iszero_def numeral_m1_eq_minus_1 eq_commute) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
117 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
118 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
119 |
subsection{*Comparisons, for Ordered Rings*} |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
120 |
|
14738 | 121 |
lemma double_eq_0_iff: "(a + a = 0) = (a = (0::'a::ordered_idom))" |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
122 |
proof - |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
123 |
have "a + a = (1+1)*a" by (simp add: left_distrib) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
124 |
with zero_less_two [where 'a = 'a] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
125 |
show ?thesis by force |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
126 |
qed |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
127 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
128 |
lemma le_imp_0_less: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
129 |
assumes le: "0 \<le> z" shows "(0::int) < 1 + z" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
130 |
proof - |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
131 |
have "0 \<le> z" . |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
132 |
also have "... < z + 1" by (rule less_add_one) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
133 |
also have "... = 1 + z" by (simp add: add_ac) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
134 |
finally show "0 < 1 + z" . |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
135 |
qed |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
136 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
137 |
lemma odd_nonzero: "1 + z + z \<noteq> (0::int)"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
138 |
proof (cases z rule: int_cases) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
139 |
case (nonneg n) |
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
140 |
have le: "0 \<le> z+z" by (simp add: nonneg add_increasing) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
141 |
thus ?thesis using le_imp_0_less [OF le] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
142 |
by (auto simp add: add_assoc) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
143 |
next |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
144 |
case (neg n) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
145 |
show ?thesis |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
146 |
proof |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
147 |
assume eq: "1 + z + z = 0" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
148 |
have "0 < 1 + (int n + int n)" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
149 |
by (simp add: le_imp_0_less add_increasing) |
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
150 |
also have "... = - (1 + z + z)" |
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
151 |
by (simp add: neg add_assoc [symmetric], simp add: add_commute) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
152 |
also have "... = 0" by (simp add: eq) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
153 |
finally have "0<0" .. |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
154 |
thus False by blast |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
155 |
qed |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
156 |
qed |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
157 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
158 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
159 |
text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*} |
14738 | 160 |
lemma Ints_odd_nonzero: "a \<in> Ints ==> 1 + a + a \<noteq> (0::'a::ordered_idom)" |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
161 |
proof (unfold Ints_def) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
162 |
assume "a \<in> range of_int" |
14473 | 163 |
then obtain z where a: "a = of_int z" .. |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
164 |
show ?thesis |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
165 |
proof |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
166 |
assume eq: "1 + a + a = 0" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
167 |
hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
168 |
hence "1 + z + z = 0" by (simp only: of_int_eq_iff) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
169 |
with odd_nonzero show False by blast |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
170 |
qed |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
171 |
qed |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
172 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
173 |
lemma Ints_number_of: "(number_of w :: 'a::number_ring) \<in> Ints" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
174 |
by (induct_tac "w", simp_all add: number_of) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
175 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
176 |
lemma iszero_number_of_BIT: |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
177 |
"iszero (number_of (w BIT x)::'a) = |
14738 | 178 |
(~x & iszero (number_of w::'a::{ordered_idom,number_ring}))" |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
179 |
by (simp add: iszero_def compare_rls zero_reorient double_eq_0_iff |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
180 |
number_of Ints_odd_nonzero [OF Ints_number_of]) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
181 |
|
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset
|
182 |
lemma iszero_number_of_0: |
14738 | 183 |
"iszero (number_of (w BIT False) :: 'a::{ordered_idom,number_ring}) = |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
184 |
iszero (number_of w :: 'a)" |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
185 |
by (simp only: iszero_number_of_BIT simp_thms) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
186 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
187 |
lemma iszero_number_of_1: |
14738 | 188 |
"~ iszero (number_of (w BIT True)::'a::{ordered_idom,number_ring})" |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
189 |
by (simp only: iszero_number_of_BIT simp_thms) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
190 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
191 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
192 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
193 |
subsection{*The Less-Than Relation*} |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
194 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
195 |
lemma less_number_of_eq_neg: |
14738 | 196 |
"((number_of x::'a::{ordered_idom,number_ring}) < number_of y) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
197 |
= neg (number_of (bin_add x (bin_minus y)) :: 'a)" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
198 |
apply (subst less_iff_diff_less_0) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
199 |
apply (simp add: neg_def diff_minus number_of_add number_of_minus) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
200 |
done |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
201 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
202 |
text{*If @{term Numeral0} is rewritten to 0 then this rule can't be applied: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
203 |
@{term Numeral0} IS @{term "number_of Pls"} *} |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
204 |
lemma not_neg_number_of_Pls: |
14738 | 205 |
"~ neg (number_of bin.Pls ::'a::{ordered_idom,number_ring})" |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
206 |
by (simp add: neg_def numeral_0_eq_0) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
207 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
208 |
lemma neg_number_of_Min: |
14738 | 209 |
"neg (number_of bin.Min ::'a::{ordered_idom,number_ring})" |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
210 |
by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
211 |
|
14738 | 212 |
lemma double_less_0_iff: "(a + a < 0) = (a < (0::'a::ordered_idom))" |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
213 |
proof - |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
214 |
have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
215 |
also have "... = (a < 0)" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
216 |
by (simp add: mult_less_0_iff zero_less_two |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
217 |
order_less_not_sym [OF zero_less_two]) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
218 |
finally show ?thesis . |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
219 |
qed |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
220 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
221 |
lemma odd_less_0: "(1 + z + z < 0) = (z < (0::int))"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
222 |
proof (cases z rule: int_cases) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
223 |
case (nonneg n) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
224 |
thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
225 |
le_imp_0_less [THEN order_less_imp_le]) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
226 |
next |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
227 |
case (neg n) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
228 |
thus ?thesis by (simp del: int_Suc |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
229 |
add: int_Suc0_eq_1 [symmetric] zadd_int compare_rls) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
230 |
qed |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
231 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
232 |
text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*} |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
233 |
lemma Ints_odd_less_0: |
14738 | 234 |
"a \<in> Ints ==> (1 + a + a < 0) = (a < (0::'a::ordered_idom))"; |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
235 |
proof (unfold Ints_def) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
236 |
assume "a \<in> range of_int" |
14473 | 237 |
then obtain z where a: "a = of_int z" .. |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
238 |
hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))" |
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
239 |
by (simp add: a) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
240 |
also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0) |
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
241 |
also have "... = (a < 0)" by (simp add: a) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
242 |
finally show ?thesis . |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
243 |
qed |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
244 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
245 |
lemma neg_number_of_BIT: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
246 |
"neg (number_of (w BIT x)::'a) = |
14738 | 247 |
neg (number_of w :: 'a::{ordered_idom,number_ring})" |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
248 |
by (simp add: number_of neg_def double_less_0_iff |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
249 |
Ints_odd_less_0 [OF Ints_number_of]) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
250 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
251 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
252 |
text{*Less-Than or Equals*} |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
253 |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14288
diff
changeset
|
254 |
text{*Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals*} |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14288
diff
changeset
|
255 |
lemmas le_number_of_eq_not_less = |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
256 |
linorder_not_less [of "number_of w" "number_of v", symmetric, |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
257 |
standard] |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14288
diff
changeset
|
258 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
259 |
lemma le_number_of_eq: |
14738 | 260 |
"((number_of x::'a::{ordered_idom,number_ring}) \<le> number_of y) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
261 |
= (~ (neg (number_of (bin_add y (bin_minus x)) :: 'a)))" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
262 |
by (simp add: le_number_of_eq_not_less less_number_of_eq_neg) |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14288
diff
changeset
|
263 |
|
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
264 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
265 |
text{*Absolute value (@{term abs})*} |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
266 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
267 |
lemma abs_number_of: |
14738 | 268 |
"abs(number_of x::'a::{ordered_idom,number_ring}) = |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
269 |
(if number_of x < (0::'a) then -number_of x else number_of x)" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
270 |
by (simp add: abs_if) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
271 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
272 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
273 |
text{*Re-orientation of the equation nnn=x*} |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
274 |
lemma number_of_reorient: "(number_of w = x) = (x = number_of w)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
275 |
by auto |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
276 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
277 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
278 |
(*Delete the original rewrites, with their clumsy conditional expressions*) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
279 |
declare bin_succ_BIT [simp del] bin_pred_BIT [simp del] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
280 |
bin_minus_BIT [simp del] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
281 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
282 |
declare bin_add_BIT [simp del] bin_mult_BIT [simp del] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
283 |
declare NCons_Pls [simp del] NCons_Min [simp del] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
284 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
285 |
(*Hide the binary representation of integer constants*) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
286 |
declare number_of_Pls [simp del] number_of_Min [simp del] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
287 |
number_of_BIT [simp del] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
288 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
289 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
290 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
291 |
(*Simplification of arithmetic operations on integer constants. |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
292 |
Note that bin_pred_Pls, etc. were added to the simpset by primrec.*) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
293 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
294 |
lemmas NCons_simps = NCons_Pls_0 NCons_Pls_1 NCons_Min_0 NCons_Min_1 NCons_BIT |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
295 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
296 |
lemmas bin_arith_extra_simps = |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
297 |
number_of_add [symmetric] |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
298 |
number_of_minus [symmetric] numeral_m1_eq_minus_1 [symmetric] |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
299 |
number_of_mult [symmetric] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
300 |
bin_succ_1 bin_succ_0 |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
301 |
bin_pred_1 bin_pred_0 |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
302 |
bin_minus_1 bin_minus_0 |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
303 |
bin_add_Pls_right bin_add_Min_right |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
304 |
bin_add_BIT_0 bin_add_BIT_10 bin_add_BIT_11 |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
305 |
diff_number_of_eq abs_number_of abs_zero abs_one |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
306 |
bin_mult_1 bin_mult_0 NCons_simps |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
307 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
308 |
(*For making a minimal simpset, one must include these default simprules |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
309 |
of thy. Also include simp_thms, or at least (~False)=True*) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
310 |
lemmas bin_arith_simps = |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
311 |
bin_pred_Pls bin_pred_Min |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
312 |
bin_succ_Pls bin_succ_Min |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
313 |
bin_add_Pls bin_add_Min |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
314 |
bin_minus_Pls bin_minus_Min |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
315 |
bin_mult_Pls bin_mult_Min bin_arith_extra_simps |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
316 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
317 |
(*Simplification of relational operations*) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
318 |
lemmas bin_rel_simps = |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
319 |
eq_number_of_eq iszero_number_of_Pls nonzero_number_of_Min |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
320 |
iszero_number_of_0 iszero_number_of_1 |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
321 |
less_number_of_eq_neg |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
322 |
not_neg_number_of_Pls not_neg_0 not_neg_1 not_iszero_1 |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
323 |
neg_number_of_Min neg_number_of_BIT |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
324 |
le_number_of_eq |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
325 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
326 |
declare bin_arith_extra_simps [simp] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
327 |
declare bin_rel_simps [simp] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
328 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
329 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
330 |
subsection{*Simplification of arithmetic when nested to the right*} |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
331 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
332 |
lemma add_number_of_left [simp]: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
333 |
"number_of v + (number_of w + z) = |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
334 |
(number_of(bin_add v w) + z::'a::number_ring)" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
335 |
by (simp add: add_assoc [symmetric]) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
336 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
337 |
lemma mult_number_of_left [simp]: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
338 |
"number_of v * (number_of w * z) = |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
339 |
(number_of(bin_mult v w) * z::'a::number_ring)" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
340 |
by (simp add: mult_assoc [symmetric]) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
341 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
342 |
lemma add_number_of_diff1: |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
343 |
"number_of v + (number_of w - c) = |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
344 |
number_of(bin_add v w) - (c::'a::number_ring)" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
345 |
by (simp add: diff_minus add_number_of_left) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
346 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
347 |
lemma add_number_of_diff2 [simp]: "number_of v + (c - number_of w) = |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
348 |
number_of (bin_add v (bin_minus w)) + (c::'a::number_ring)" |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
349 |
apply (subst diff_number_of_eq [symmetric]) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
350 |
apply (simp only: compare_rls) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
351 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
352 |
|
1632 | 353 |
end |