71986
|
1 |
theory Ancient_Numeral
|
72000
|
2 |
imports Main Bits_Int Misc_lsb Misc_msb
|
71986
|
3 |
begin
|
|
4 |
|
|
5 |
definition Bit :: "int \<Rightarrow> bool \<Rightarrow> int" (infixl "BIT" 90)
|
|
6 |
where "k BIT b = (if b then 1 else 0) + k + k"
|
|
7 |
|
|
8 |
lemma Bit_B0: "k BIT False = k + k"
|
|
9 |
by (simp add: Bit_def)
|
|
10 |
|
|
11 |
lemma Bit_B1: "k BIT True = k + k + 1"
|
|
12 |
by (simp add: Bit_def)
|
|
13 |
|
|
14 |
lemma Bit_B0_2t: "k BIT False = 2 * k"
|
|
15 |
by (rule trans, rule Bit_B0) simp
|
|
16 |
|
|
17 |
lemma Bit_B1_2t: "k BIT True = 2 * k + 1"
|
|
18 |
by (rule trans, rule Bit_B1) simp
|
|
19 |
|
|
20 |
lemma uminus_Bit_eq:
|
|
21 |
"- k BIT b = (- k - of_bool b) BIT b"
|
|
22 |
by (cases b) (simp_all add: Bit_def)
|
|
23 |
|
|
24 |
lemma power_BIT: "2 ^ Suc n - 1 = (2 ^ n - 1) BIT True"
|
|
25 |
by (simp add: Bit_B1)
|
|
26 |
|
|
27 |
lemma bin_rl_simp [simp]: "bin_rest w BIT bin_last w = w"
|
|
28 |
by (simp add: Bit_def)
|
|
29 |
|
|
30 |
lemma bin_rest_BIT [simp]: "bin_rest (x BIT b) = x"
|
|
31 |
by (simp add: Bit_def)
|
|
32 |
|
|
33 |
lemma even_BIT [simp]: "even (x BIT b) \<longleftrightarrow> \<not> b"
|
|
34 |
by (simp add: Bit_def)
|
|
35 |
|
|
36 |
lemma bin_last_BIT [simp]: "bin_last (x BIT b) = b"
|
|
37 |
by simp
|
|
38 |
|
|
39 |
lemma BIT_eq_iff [iff]: "u BIT b = v BIT c \<longleftrightarrow> u = v \<and> b = c"
|
|
40 |
by (auto simp: Bit_def) arith+
|
|
41 |
|
|
42 |
lemma BIT_bin_simps [simp]:
|
|
43 |
"numeral k BIT False = numeral (Num.Bit0 k)"
|
|
44 |
"numeral k BIT True = numeral (Num.Bit1 k)"
|
|
45 |
"(- numeral k) BIT False = - numeral (Num.Bit0 k)"
|
|
46 |
"(- numeral k) BIT True = - numeral (Num.BitM k)"
|
|
47 |
by (simp_all only: Bit_B0 Bit_B1 numeral.simps numeral_BitM)
|
|
48 |
|
|
49 |
lemma BIT_special_simps [simp]:
|
|
50 |
shows "0 BIT False = 0"
|
|
51 |
and "0 BIT True = 1"
|
|
52 |
and "1 BIT False = 2"
|
|
53 |
and "1 BIT True = 3"
|
|
54 |
and "(- 1) BIT False = - 2"
|
|
55 |
and "(- 1) BIT True = - 1"
|
|
56 |
by (simp_all add: Bit_def)
|
|
57 |
|
|
58 |
lemma Bit_eq_0_iff: "w BIT b = 0 \<longleftrightarrow> w = 0 \<and> \<not> b"
|
|
59 |
by (auto simp: Bit_def) arith
|
|
60 |
|
|
61 |
lemma Bit_eq_m1_iff: "w BIT b = -1 \<longleftrightarrow> w = -1 \<and> b"
|
|
62 |
by (auto simp: Bit_def) arith
|
|
63 |
|
|
64 |
lemma expand_BIT:
|
|
65 |
"numeral (Num.Bit0 w) = numeral w BIT False"
|
|
66 |
"numeral (Num.Bit1 w) = numeral w BIT True"
|
|
67 |
"- numeral (Num.Bit0 w) = (- numeral w) BIT False"
|
|
68 |
"- numeral (Num.Bit1 w) = (- numeral (w + Num.One)) BIT True"
|
71991
|
69 |
by (simp_all add: BitM_inc_eq add_One)
|
71986
|
70 |
|
|
71 |
lemma less_Bits: "v BIT b < w BIT c \<longleftrightarrow> v < w \<or> v \<le> w \<and> \<not> b \<and> c"
|
|
72 |
by (auto simp: Bit_def)
|
|
73 |
|
|
74 |
lemma le_Bits: "v BIT b \<le> w BIT c \<longleftrightarrow> v < w \<or> v \<le> w \<and> (\<not> b \<or> c)"
|
|
75 |
by (auto simp: Bit_def)
|
|
76 |
|
|
77 |
lemma pred_BIT_simps [simp]:
|
|
78 |
"x BIT False - 1 = (x - 1) BIT True"
|
|
79 |
"x BIT True - 1 = x BIT False"
|
|
80 |
by (simp_all add: Bit_B0_2t Bit_B1_2t)
|
|
81 |
|
|
82 |
lemma succ_BIT_simps [simp]:
|
|
83 |
"x BIT False + 1 = x BIT True"
|
|
84 |
"x BIT True + 1 = (x + 1) BIT False"
|
|
85 |
by (simp_all add: Bit_B0_2t Bit_B1_2t)
|
|
86 |
|
|
87 |
lemma add_BIT_simps [simp]:
|
|
88 |
"x BIT False + y BIT False = (x + y) BIT False"
|
|
89 |
"x BIT False + y BIT True = (x + y) BIT True"
|
|
90 |
"x BIT True + y BIT False = (x + y) BIT True"
|
|
91 |
"x BIT True + y BIT True = (x + y + 1) BIT False"
|
|
92 |
by (simp_all add: Bit_B0_2t Bit_B1_2t)
|
|
93 |
|
|
94 |
lemma mult_BIT_simps [simp]:
|
|
95 |
"x BIT False * y = (x * y) BIT False"
|
|
96 |
"x * y BIT False = (x * y) BIT False"
|
|
97 |
"x BIT True * y = (x * y) BIT False + y"
|
|
98 |
by (simp_all add: Bit_B0_2t Bit_B1_2t algebra_simps)
|
|
99 |
|
|
100 |
lemma B_mod_2': "X = 2 \<Longrightarrow> (w BIT True) mod X = 1 \<and> (w BIT False) mod X = 0"
|
|
101 |
by (simp add: Bit_B0 Bit_B1)
|
|
102 |
|
|
103 |
lemma bin_ex_rl: "\<exists>w b. w BIT b = bin"
|
|
104 |
by (metis bin_rl_simp)
|
|
105 |
|
|
106 |
lemma bin_exhaust: "(\<And>x b. bin = x BIT b \<Longrightarrow> Q) \<Longrightarrow> Q"
|
|
107 |
by (metis bin_ex_rl)
|
|
108 |
|
|
109 |
lemma bin_abs_lem: "bin = (w BIT b) \<Longrightarrow> bin \<noteq> -1 \<longrightarrow> bin \<noteq> 0 \<longrightarrow> nat \<bar>w\<bar> < nat \<bar>bin\<bar>"
|
|
110 |
apply clarsimp
|
|
111 |
apply (unfold Bit_def)
|
|
112 |
apply (cases b)
|
|
113 |
apply (clarsimp, arith)
|
|
114 |
apply (clarsimp, arith)
|
|
115 |
done
|
|
116 |
|
|
117 |
lemma bin_induct:
|
|
118 |
assumes PPls: "P 0"
|
|
119 |
and PMin: "P (- 1)"
|
|
120 |
and PBit: "\<And>bin bit. P bin \<Longrightarrow> P (bin BIT bit)"
|
|
121 |
shows "P bin"
|
|
122 |
apply (rule_tac P=P and a=bin and f1="nat \<circ> abs" in wf_measure [THEN wf_induct])
|
|
123 |
apply (simp add: measure_def inv_image_def)
|
|
124 |
apply (case_tac x rule: bin_exhaust)
|
|
125 |
apply (frule bin_abs_lem)
|
|
126 |
apply (auto simp add : PPls PMin PBit)
|
|
127 |
done
|
|
128 |
|
|
129 |
lemma Bit_div2: "(w BIT b) div 2 = w"
|
|
130 |
by (fact bin_rest_BIT)
|
|
131 |
|
|
132 |
lemma twice_conv_BIT: "2 * x = x BIT False"
|
|
133 |
by (simp add: Bit_def)
|
|
134 |
|
|
135 |
lemma BIT_lt0 [simp]: "x BIT b < 0 \<longleftrightarrow> x < 0"
|
|
136 |
by(cases b)(auto simp add: Bit_def)
|
|
137 |
|
|
138 |
lemma BIT_ge0 [simp]: "x BIT b \<ge> 0 \<longleftrightarrow> x \<ge> 0"
|
|
139 |
by(cases b)(auto simp add: Bit_def)
|
|
140 |
|
|
141 |
lemma bin_to_bl_aux_Bit_minus_simp [simp]:
|
|
142 |
"0 < n \<Longrightarrow> bin_to_bl_aux n (w BIT b) bl = bin_to_bl_aux (n - 1) w (b # bl)"
|
|
143 |
by (cases n) auto
|
|
144 |
|
|
145 |
lemma bl_to_bin_BIT:
|
|
146 |
"bl_to_bin bs BIT b = bl_to_bin (bs @ [b])"
|
|
147 |
by (simp add: bl_to_bin_append Bit_def)
|
|
148 |
|
|
149 |
lemma bin_nth_0_BIT: "bin_nth (w BIT b) 0 \<longleftrightarrow> b"
|
|
150 |
by simp
|
|
151 |
|
|
152 |
lemma bin_nth_Suc_BIT: "bin_nth (w BIT b) (Suc n) = bin_nth w n"
|
|
153 |
by (simp add: bit_Suc)
|
|
154 |
|
|
155 |
lemma bin_nth_minus [simp]: "0 < n \<Longrightarrow> bin_nth (w BIT b) n = bin_nth w (n - 1)"
|
|
156 |
by (cases n) (simp_all add: bit_Suc)
|
|
157 |
|
|
158 |
lemma bin_sign_simps [simp]:
|
|
159 |
"bin_sign (w BIT b) = bin_sign w"
|
|
160 |
by (simp add: bin_sign_def Bit_def)
|
|
161 |
|
|
162 |
lemma bin_nth_Bit: "bin_nth (w BIT b) n \<longleftrightarrow> n = 0 \<and> b \<or> (\<exists>m. n = Suc m \<and> bin_nth w m)"
|
|
163 |
by (cases n) auto
|
|
164 |
|
|
165 |
lemmas sbintrunc_Suc_BIT [simp] =
|
72010
|
166 |
signed_take_bit_Suc [where k="w BIT b", simplified bin_last_BIT bin_rest_BIT] for w b
|
71986
|
167 |
|
|
168 |
lemmas sbintrunc_0_BIT_B0 [simp] =
|
72010
|
169 |
signed_take_bit_0 [where k="w BIT False", simplified bin_last_numeral_simps bin_rest_numeral_simps]
|
71986
|
170 |
for w
|
|
171 |
|
|
172 |
lemmas sbintrunc_0_BIT_B1 [simp] =
|
72010
|
173 |
signed_take_bit_0 [where k="w BIT True", simplified bin_last_BIT bin_rest_numeral_simps]
|
71986
|
174 |
for w
|
|
175 |
|
|
176 |
lemma sbintrunc_Suc_minus_Is:
|
|
177 |
\<open>0 < n \<Longrightarrow>
|
|
178 |
sbintrunc (n - 1) w = y \<Longrightarrow>
|
|
179 |
sbintrunc n (w BIT b) = y BIT b\<close>
|
72010
|
180 |
by (cases n) (simp_all add: Bit_def signed_take_bit_Suc)
|
71986
|
181 |
|
|
182 |
lemma bin_cat_Suc_Bit: "bin_cat w (Suc n) (v BIT b) = bin_cat w n v BIT b"
|
|
183 |
by (auto simp add: Bit_def)
|
|
184 |
|
|
185 |
lemma int_not_BIT [simp]: "NOT (w BIT b) = (NOT w) BIT (\<not> b)"
|
|
186 |
by (simp add: not_int_def Bit_def)
|
|
187 |
|
|
188 |
lemma int_and_Bits [simp]: "(x BIT b) AND (y BIT c) = (x AND y) BIT (b \<and> c)"
|
|
189 |
using and_int_rec [of \<open>x BIT b\<close> \<open>y BIT c\<close>] by (auto simp add: Bit_B0_2t Bit_B1_2t)
|
|
190 |
|
|
191 |
lemma int_or_Bits [simp]: "(x BIT b) OR (y BIT c) = (x OR y) BIT (b \<or> c)"
|
|
192 |
using or_int_rec [of \<open>x BIT b\<close> \<open>y BIT c\<close>] by (auto simp add: Bit_B0_2t Bit_B1_2t)
|
|
193 |
|
|
194 |
lemma int_xor_Bits [simp]: "(x BIT b) XOR (y BIT c) = (x XOR y) BIT ((b \<or> c) \<and> \<not> (b \<and> c))"
|
|
195 |
using xor_int_rec [of \<open>x BIT b\<close> \<open>y BIT c\<close>] by (auto simp add: Bit_B0_2t Bit_B1_2t)
|
|
196 |
|
|
197 |
lemma mod_BIT:
|
|
198 |
"bin BIT bit mod 2 ^ Suc n = (bin mod 2 ^ n) BIT bit" for bit
|
|
199 |
proof -
|
|
200 |
have "2 * (bin mod 2 ^ n) + 1 = (2 * bin mod 2 ^ Suc n) + 1"
|
|
201 |
by (simp add: mod_mult_mult1)
|
|
202 |
also have "\<dots> = ((2 * bin mod 2 ^ Suc n) + 1) mod 2 ^ Suc n"
|
|
203 |
by (simp add: ac_simps pos_zmod_mult_2)
|
|
204 |
also have "\<dots> = (2 * bin + 1) mod 2 ^ Suc n"
|
|
205 |
by (simp only: mod_simps)
|
|
206 |
finally show ?thesis
|
|
207 |
by (auto simp add: Bit_def)
|
|
208 |
qed
|
|
209 |
|
|
210 |
lemma minus_BIT_0: fixes x y :: int shows "x BIT b - y BIT False = (x - y) BIT b"
|
|
211 |
by(simp add: Bit_def)
|
|
212 |
|
|
213 |
lemma int_lsb_BIT [simp]: fixes x :: int shows
|
|
214 |
"lsb (x BIT b) \<longleftrightarrow> b"
|
|
215 |
by(simp add: lsb_int_def)
|
|
216 |
|
|
217 |
lemma int_shiftr_BIT [simp]: fixes x :: int
|
|
218 |
shows int_shiftr0: "x >> 0 = x"
|
|
219 |
and int_shiftr_Suc: "x BIT b >> Suc n = x >> n"
|
|
220 |
proof -
|
|
221 |
show "x >> 0 = x" by (simp add: shiftr_int_def)
|
|
222 |
show "x BIT b >> Suc n = x >> n" by (cases b)
|
|
223 |
(simp_all add: shiftr_int_def Bit_def add.commute pos_zdiv_mult_2)
|
|
224 |
qed
|
|
225 |
|
|
226 |
lemma msb_BIT [simp]: "msb (x BIT b) = msb x"
|
|
227 |
by(simp add: msb_int_def)
|
|
228 |
|
|
229 |
end |