24333

1 
(*


2 
ID: $Id$


3 
Author: Jeremy Dawson, NICTA


4 


5 
contains basic definition to do with integers


6 
expressed using Pls, Min, BIT and important resulting theorems,


7 
in particular, bin_rec and related work


8 
*)


9 


10 
theory BinGeneral imports TdThs Num_Lemmas


11 


12 
begin


13 


14 
lemma brlem: "(bin = Numeral.Min) = ( bin + Numeral.pred 0 = 0)"


15 
unfolding Min_def pred_def by arith


16 


17 
function


18 
bin_rec' :: "int * 'a * 'a * (int => bit => 'a => 'a) => 'a"


19 
where


20 
"bin_rec' (bin, f1, f2, f3) = (if bin = Numeral.Pls then f1


21 
else if bin = Numeral.Min then f2


22 
else case bin_rl bin of (w, b) => f3 w b (bin_rec' (w, f1, f2, f3)))"


23 
by pat_completeness auto


24 


25 
termination


26 
apply (relation "measure (nat o abs o fst)")


27 
apply simp


28 
apply (simp add: Pls_def brlem)


29 
apply (clarsimp simp: bin_rl_char pred_def)


30 
apply (frule thin_rl [THEN refl [THEN bin_abs_lem [rule_format]]])


31 
apply (unfold Pls_def Min_def number_of_eq)


32 
prefer 2


33 
apply (erule asm_rl)


34 
apply auto


35 
done


36 


37 
constdefs


38 
bin_rec :: "'a => 'a => (int => bit => 'a => 'a) => int => 'a"


39 
"bin_rec f1 f2 f3 bin == bin_rec' (bin, f1, f2, f3)"


40 


41 
consts


42 
 "corresponding operations analysing bins"


43 
bin_last :: "int => bit"


44 
bin_rest :: "int => int"


45 
bin_sign :: "int => int"


46 
bin_nth :: "int => nat => bool"


47 


48 
primrec


49 
Z : "bin_nth w 0 = (bin_last w = bit.B1)"


50 
Suc : "bin_nth w (Suc n) = bin_nth (bin_rest w) n"


51 


52 
defs


53 
bin_rest_def : "bin_rest w == fst (bin_rl w)"


54 
bin_last_def : "bin_last w == snd (bin_rl w)"


55 
bin_sign_def : "bin_sign == bin_rec Numeral.Pls Numeral.Min (%w b s. s)"


56 


57 
consts


58 
bintrunc :: "nat => int => int"


59 
primrec


60 
Z : "bintrunc 0 bin = Numeral.Pls"


61 
Suc : "bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT (bin_last bin)"


62 


63 
consts


64 
sbintrunc :: "nat => int => int"


65 
primrec


66 
Z : "sbintrunc 0 bin =


67 
(case bin_last bin of bit.B1 => Numeral.Min  bit.B0 => Numeral.Pls)"


68 
Suc : "sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)"


69 


70 
consts


71 
bin_split :: "nat => int => int * int"


72 
primrec


73 
Z : "bin_split 0 w = (w, Numeral.Pls)"


74 
Suc : "bin_split (Suc n) w = (let (w1, w2) = bin_split n (bin_rest w)


75 
in (w1, w2 BIT bin_last w))"


76 


77 
consts


78 
bin_cat :: "int => nat => int => int"


79 
primrec


80 
Z : "bin_cat w 0 v = w"


81 
Suc : "bin_cat w (Suc n) v = bin_cat w n (bin_rest v) BIT bin_last v"


82 


83 
lemmas funpow_minus_simp =


84 
trans [OF gen_minus [where f = "power f"] funpow_Suc, standard]


85 


86 
lemmas funpow_pred_simp [simp] =


87 
funpow_minus_simp [of "number_of bin", simplified nobm1, standard]


88 


89 
lemmas replicate_minus_simp =


90 
trans [OF gen_minus [where f = "%n. replicate n x"] replicate.replicate_Suc,


91 
standard]


92 


93 
lemmas replicate_pred_simp [simp] =


94 
replicate_minus_simp [of "number_of bin", simplified nobm1, standard]


95 


96 
lemmas power_Suc_no [simp] = power_Suc [of "number_of ?a"]


97 


98 
lemmas power_minus_simp =


99 
trans [OF gen_minus [where f = "power f"] power_Suc, standard]


100 


101 
lemmas power_pred_simp =


102 
power_minus_simp [of "number_of bin", simplified nobm1, standard]


103 
lemmas power_pred_simp_no [simp] = power_pred_simp [where f= "number_of ?f"]


104 


105 
lemma bin_rl: "bin_rl w = (bin_rest w, bin_last w)"


106 
unfolding bin_rest_def bin_last_def by auto


107 


108 
lemmas bin_rl_simp [simp] = iffD1 [OF bin_rl_char bin_rl]


109 


110 
lemma bin_rec_PM:


111 
"f = bin_rec f1 f2 f3 ==> f Numeral.Pls = f1 & f Numeral.Min = f2"


112 
apply safe


113 
apply (unfold bin_rec_def)


114 
apply (auto intro: bin_rec'.simps [THEN trans])


115 
done


116 


117 
lemmas bin_rec_Pls = refl [THEN bin_rec_PM, THEN conjunct1, standard]


118 
lemmas bin_rec_Min = refl [THEN bin_rec_PM, THEN conjunct2, standard]


119 


120 
lemma bin_rec_Bit:


121 
"f = bin_rec f1 f2 f3 ==> f3 Numeral.Pls bit.B0 f1 = f1 ==>


122 
f3 Numeral.Min bit.B1 f2 = f2 ==> f (w BIT b) = f3 w b (f w)"


123 
apply clarify


124 
apply (unfold bin_rec_def)


125 
apply (rule bin_rec'.simps [THEN trans])


126 
apply auto


127 
apply (unfold Pls_def Min_def Bit_def)


128 
apply (cases b, auto)+


129 
done


130 


131 
lemmas bin_rec_simps = refl [THEN bin_rec_Bit] bin_rec_Pls bin_rec_Min


132 


133 
lemma bin_rest_simps [simp]:


134 
"bin_rest Numeral.Pls = Numeral.Pls"


135 
"bin_rest Numeral.Min = Numeral.Min"


136 
"bin_rest (w BIT b) = w"


137 
unfolding bin_rest_def by auto


138 


139 
lemma bin_last_simps [simp]:


140 
"bin_last Numeral.Pls = bit.B0"


141 
"bin_last Numeral.Min = bit.B1"


142 
"bin_last (w BIT b) = b"


143 
unfolding bin_last_def by auto


144 


145 
lemma bin_sign_simps [simp]:


146 
"bin_sign Numeral.Pls = Numeral.Pls"


147 
"bin_sign Numeral.Min = Numeral.Min"


148 
"bin_sign (w BIT b) = bin_sign w"


149 
unfolding bin_sign_def by (auto simp: bin_rec_simps)


150 


151 
lemma bin_r_l_extras [simp]:


152 
"bin_last 0 = bit.B0"


153 
"bin_last ( 1) = bit.B1"


154 
"bin_last 1 = bit.B1"


155 
"bin_last 1 = bit.B1"


156 
"bin_rest 1 = 0"


157 
"bin_rest 0 = 0"


158 
"bin_rest ( 1) =  1"


159 
"bin_rest 1 = 1"


160 
apply (unfold number_of_Min)


161 
apply (unfold Pls_def [symmetric] Min_def [symmetric])


162 
apply (unfold numeral_1_eq_1 [symmetric])


163 
apply (auto simp: number_of_eq)


164 
done


165 


166 
lemma bin_last_mod:


167 
"bin_last w = (if w mod 2 = 0 then bit.B0 else bit.B1)"


168 
apply (case_tac w rule: bin_exhaust)


169 
apply (case_tac b)


170 
apply auto


171 
done


172 


173 
lemma bin_rest_div:


174 
"bin_rest w = w div 2"


175 
apply (case_tac w rule: bin_exhaust)


176 
apply (rule trans)


177 
apply clarsimp


178 
apply (rule refl)


179 
apply (drule trans)


180 
apply (rule Bit_def)


181 
apply (simp add: z1pdiv2 split: bit.split)


182 
done


183 


184 
lemma Bit_div2 [simp]: "(w BIT b) div 2 = w"


185 
unfolding bin_rest_div [symmetric] by auto


186 


187 
lemma bin_nth_lem [rule_format]:


188 
"ALL y. bin_nth x = bin_nth y > x = y"


189 
apply (induct x rule: bin_induct)


190 
apply safe


191 
apply (erule rev_mp)


192 
apply (induct_tac y rule: bin_induct)


193 
apply safe


194 
apply (drule_tac x=0 in fun_cong, force)


195 
apply (erule notE, rule ext,


196 
drule_tac x="Suc x" in fun_cong, force)


197 
apply (drule_tac x=0 in fun_cong, force)


198 
apply (erule rev_mp)


199 
apply (induct_tac y rule: bin_induct)


200 
apply safe


201 
apply (drule_tac x=0 in fun_cong, force)


202 
apply (erule notE, rule ext,


203 
drule_tac x="Suc x" in fun_cong, force)


204 
apply (drule_tac x=0 in fun_cong, force)


205 
apply (case_tac y rule: bin_exhaust)


206 
apply clarify


207 
apply (erule allE)


208 
apply (erule impE)


209 
prefer 2


210 
apply (erule BIT_eqI)


211 
apply (drule_tac x=0 in fun_cong, force)


212 
apply (rule ext)


213 
apply (drule_tac x="Suc ?x" in fun_cong, force)


214 
done


215 


216 
lemma bin_nth_eq_iff: "(bin_nth x = bin_nth y) = (x = y)"


217 
by (auto elim: bin_nth_lem)


218 


219 
lemmas bin_eqI = ext [THEN bin_nth_eq_iff [THEN iffD1], standard]


220 


221 
lemma bin_nth_Pls [simp]: "~ bin_nth Numeral.Pls n"


222 
by (induct n) auto


223 


224 
lemma bin_nth_Min [simp]: "bin_nth Numeral.Min n"


225 
by (induct n) auto


226 


227 
lemma bin_nth_0_BIT: "bin_nth (w BIT b) 0 = (b = bit.B1)"


228 
by auto


229 


230 
lemma bin_nth_Suc_BIT: "bin_nth (w BIT b) (Suc n) = bin_nth w n"


231 
by auto


232 


233 
lemma bin_nth_minus [simp]: "0 < n ==> bin_nth (w BIT b) n = bin_nth w (n  1)"


234 
by (cases n) auto


235 


236 
lemmas bin_nth_0 = bin_nth.simps(1)


237 
lemmas bin_nth_Suc = bin_nth.simps(2)


238 


239 
lemmas bin_nth_simps =


240 
bin_nth_0 bin_nth_Suc bin_nth_Pls bin_nth_Min bin_nth_minus


241 


242 
lemma sign_bintr:


243 
"!!w. bin_sign (bintrunc n w) = Numeral.Pls"


244 
by (induct n) auto


245 


246 
lemma bin_sign_rest [simp]:


247 
"bin_sign (bin_rest w) = (bin_sign w)"


248 
by (case_tac w rule: bin_exhaust) auto


249 


250 
lemma bintrunc_mod2p:


251 
"!!w. bintrunc n w = (w mod 2 ^ n :: int)"


252 
apply (induct n, clarsimp)


253 
apply (simp add: bin_last_mod bin_rest_div Bit_def zmod_zmult2_eq


254 
cong: number_of_False_cong)


255 
done


256 


257 
lemma sbintrunc_mod2p:


258 
"!!w. sbintrunc n w = ((w + 2 ^ n) mod 2 ^ (Suc n)  2 ^ n :: int)"


259 
apply (induct n)


260 
apply clarsimp


261 
apply (subst zmod_zadd_left_eq)


262 
apply (simp add: bin_last_mod)


263 
apply (simp add: number_of_eq)


264 
apply clarsimp


265 
apply (simp add: bin_last_mod bin_rest_div Bit_def


266 
cong: number_of_False_cong)


267 
apply (clarsimp simp: zmod_zmult_zmult1 [symmetric]


268 
zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2 [THEN sym]]])


269 
apply (rule trans [symmetric, OF _ emep1])


270 
apply auto


271 
apply (auto simp: even_def)


272 
done


273 


274 
lemmas m2pths [OF zless2p, standard] = pos_mod_sign pos_mod_bound


275 


276 
lemma list_exhaust_size_gt0:


277 
assumes y: "\<And>a list. y = a # list \<Longrightarrow> P"


278 
shows "0 < length y \<Longrightarrow> P"


279 
apply (cases y, simp)


280 
apply (rule y)


281 
apply fastsimp


282 
done


283 


284 
lemma list_exhaust_size_eq0:


285 
assumes y: "y = [] \<Longrightarrow> P"


286 
shows "length y = 0 \<Longrightarrow> P"


287 
apply (cases y)


288 
apply (rule y, simp)


289 
apply simp


290 
done


291 


292 
lemma size_Cons_lem_eq:


293 
"y = xa # list ==> size y = Suc k ==> size list = k"


294 
by auto


295 


296 
lemma size_Cons_lem_eq_bin:


297 
"y = xa # list ==> size y = number_of (Numeral.succ k) ==>


298 
size list = number_of k"


299 
by (auto simp: pred_def succ_def split add : split_if_asm)


300 


301 


302 
section "Simplifications for (s)bintrunc"


303 


304 
lemma bit_bool:


305 
"(b = (b' = bit.B1)) = (b' = (if b then bit.B1 else bit.B0))"


306 
by (cases b') auto


307 


308 
lemmas bit_bool1 [simp] = refl [THEN bit_bool [THEN iffD1], symmetric]


309 


310 
lemma bin_sign_lem:


311 
"!!bin. (bin_sign (sbintrunc n bin) = Numeral.Min) = bin_nth bin n"


312 
apply (induct n)


313 
apply (case_tac bin rule: bin_exhaust, case_tac b, auto)+


314 
done


315 


316 
lemma nth_bintr:


317 
"!!w m. bin_nth (bintrunc m w) n = (n < m & bin_nth w n)"


318 
apply (induct n)


319 
apply (case_tac m, auto)[1]


320 
apply (case_tac m, auto)[1]


321 
done


322 


323 
lemma nth_sbintr:


324 
"!!w m. bin_nth (sbintrunc m w) n =


325 
(if n < m then bin_nth w n else bin_nth w m)"


326 
apply (induct n)


327 
apply (case_tac m, simp_all split: bit.splits)[1]


328 
apply (case_tac m, simp_all split: bit.splits)[1]


329 
done


330 


331 
lemma bin_nth_Bit:


332 
"bin_nth (w BIT b) n = (n = 0 & b = bit.B1  (EX m. n = Suc m & bin_nth w m))"


333 
by (cases n) auto


334 


335 
lemma bintrunc_bintrunc_l:


336 
"n <= m ==> (bintrunc m (bintrunc n w) = bintrunc n w)"


337 
by (rule bin_eqI) (auto simp add : nth_bintr)


338 


339 
lemma sbintrunc_sbintrunc_l:


340 
"n <= m ==> (sbintrunc m (sbintrunc n w) = sbintrunc n w)"


341 
by (rule bin_eqI) (auto simp: nth_sbintr min_def)


342 


343 
lemma bintrunc_bintrunc_ge:


344 
"n <= m ==> (bintrunc n (bintrunc m w) = bintrunc n w)"


345 
by (rule bin_eqI) (auto simp: nth_bintr)


346 


347 
lemma bintrunc_bintrunc_min [simp]:


348 
"bintrunc m (bintrunc n w) = bintrunc (min m n) w"


349 
apply (unfold min_def)


350 
apply (rule bin_eqI)


351 
apply (auto simp: nth_bintr)


352 
done


353 


354 
lemma sbintrunc_sbintrunc_min [simp]:


355 
"sbintrunc m (sbintrunc n w) = sbintrunc (min m n) w"


356 
apply (unfold min_def)


357 
apply (rule bin_eqI)


358 
apply (auto simp: nth_sbintr)


359 
done


360 


361 
lemmas bintrunc_Pls =


362 
bintrunc.Suc [where bin="Numeral.Pls", simplified bin_last_simps bin_rest_simps]


363 


364 
lemmas bintrunc_Min [simp] =


365 
bintrunc.Suc [where bin="Numeral.Min", simplified bin_last_simps bin_rest_simps]


366 


367 
lemmas bintrunc_BIT [simp] =


368 
bintrunc.Suc [where bin="?w BIT ?b", simplified bin_last_simps bin_rest_simps]


369 


370 
lemmas bintrunc_Sucs = bintrunc_Pls bintrunc_Min bintrunc_BIT


371 


372 
lemmas sbintrunc_Suc_Pls =


373 
sbintrunc.Suc [where bin="Numeral.Pls", simplified bin_last_simps bin_rest_simps]


374 


375 
lemmas sbintrunc_Suc_Min =


376 
sbintrunc.Suc [where bin="Numeral.Min", simplified bin_last_simps bin_rest_simps]


377 


378 
lemmas sbintrunc_Suc_BIT [simp] =


379 
sbintrunc.Suc [where bin="?w BIT ?b", simplified bin_last_simps bin_rest_simps]


380 


381 
lemmas sbintrunc_Sucs = sbintrunc_Suc_Pls sbintrunc_Suc_Min sbintrunc_Suc_BIT


382 


383 
lemmas sbintrunc_Pls =


384 
sbintrunc.Z [where bin="Numeral.Pls",


385 
simplified bin_last_simps bin_rest_simps bit.simps]


386 


387 
lemmas sbintrunc_Min =


388 
sbintrunc.Z [where bin="Numeral.Min",


389 
simplified bin_last_simps bin_rest_simps bit.simps]


390 


391 
lemmas sbintrunc_0_BIT_B0 [simp] =


392 
sbintrunc.Z [where bin="?w BIT bit.B0",


393 
simplified bin_last_simps bin_rest_simps bit.simps]


394 


395 
lemmas sbintrunc_0_BIT_B1 [simp] =


396 
sbintrunc.Z [where bin="?w BIT bit.B1",


397 
simplified bin_last_simps bin_rest_simps bit.simps]


398 


399 
lemmas sbintrunc_0_simps =


400 
sbintrunc_Pls sbintrunc_Min sbintrunc_0_BIT_B0 sbintrunc_0_BIT_B1


401 


402 
lemmas bintrunc_simps = bintrunc.Z bintrunc_Sucs


403 
lemmas sbintrunc_simps = sbintrunc_0_simps sbintrunc_Sucs


404 


405 
lemma bintrunc_minus:


406 
"0 < n ==> bintrunc (Suc (n  1)) w = bintrunc n w"


407 
by auto


408 


409 
lemma sbintrunc_minus:


410 
"0 < n ==> sbintrunc (Suc (n  1)) w = sbintrunc n w"


411 
by auto


412 


413 
lemmas bintrunc_minus_simps =


414 
bintrunc_Sucs [THEN [2] bintrunc_minus [symmetric, THEN trans], standard]


415 
lemmas sbintrunc_minus_simps =


416 
sbintrunc_Sucs [THEN [2] sbintrunc_minus [symmetric, THEN trans], standard]


417 


418 
lemma bintrunc_n_Pls [simp]:


419 
"bintrunc n Numeral.Pls = Numeral.Pls"


420 
by (induct n) auto


421 


422 
lemma sbintrunc_n_PM [simp]:


423 
"sbintrunc n Numeral.Pls = Numeral.Pls"


424 
"sbintrunc n Numeral.Min = Numeral.Min"


425 
by (induct n) auto


426 


427 
lemmas thobini1 = arg_cong [where f = "%w. w BIT ?b"]


428 


429 
lemmas bintrunc_BIT_I = trans [OF bintrunc_BIT thobini1]


430 
lemmas bintrunc_Min_I = trans [OF bintrunc_Min thobini1]


431 


432 
lemmas bmsts = bintrunc_minus_simps [THEN thobini1 [THEN [2] trans], standard]


433 
lemmas bintrunc_Pls_minus_I = bmsts(1)


434 
lemmas bintrunc_Min_minus_I = bmsts(2)


435 
lemmas bintrunc_BIT_minus_I = bmsts(3)


436 


437 
lemma bintrunc_0_Min: "bintrunc 0 Numeral.Min = Numeral.Pls"


438 
by auto


439 
lemma bintrunc_0_BIT: "bintrunc 0 (w BIT b) = Numeral.Pls"


440 
by auto


441 


442 
lemma bintrunc_Suc_lem:


443 
"bintrunc (Suc n) x = y ==> m = Suc n ==> bintrunc m x = y"


444 
by auto


445 


446 
lemmas bintrunc_Suc_Ialts =


447 
bintrunc_Min_I bintrunc_BIT_I [THEN bintrunc_Suc_lem, standard]


448 


449 
lemmas sbintrunc_BIT_I = trans [OF sbintrunc_Suc_BIT thobini1]


450 


451 
lemmas sbintrunc_Suc_Is =


452 
sbintrunc_Sucs [THEN thobini1 [THEN [2] trans], standard]


453 


454 
lemmas sbintrunc_Suc_minus_Is =


455 
sbintrunc_minus_simps [THEN thobini1 [THEN [2] trans], standard]


456 


457 
lemma sbintrunc_Suc_lem:


458 
"sbintrunc (Suc n) x = y ==> m = Suc n ==> sbintrunc m x = y"


459 
by auto


460 


461 
lemmas sbintrunc_Suc_Ialts =


462 
sbintrunc_Suc_Is [THEN sbintrunc_Suc_lem, standard]


463 


464 
lemma sbintrunc_bintrunc_lt:


465 
"m > n ==> sbintrunc n (bintrunc m w) = sbintrunc n w"


466 
by (rule bin_eqI) (auto simp: nth_sbintr nth_bintr)


467 


468 
lemma bintrunc_sbintrunc_le:


469 
"m <= Suc n ==> bintrunc m (sbintrunc n w) = bintrunc m w"


470 
apply (rule bin_eqI)


471 
apply (auto simp: nth_sbintr nth_bintr)


472 
apply (subgoal_tac "x=n", safe, arith+)[1]


473 
apply (subgoal_tac "x=n", safe, arith+)[1]


474 
done


475 


476 
lemmas bintrunc_sbintrunc [simp] = order_refl [THEN bintrunc_sbintrunc_le]


477 
lemmas sbintrunc_bintrunc [simp] = lessI [THEN sbintrunc_bintrunc_lt]


478 
lemmas bintrunc_bintrunc [simp] = order_refl [THEN bintrunc_bintrunc_l]


479 
lemmas sbintrunc_sbintrunc [simp] = order_refl [THEN sbintrunc_sbintrunc_l]


480 


481 
lemma bintrunc_sbintrunc' [simp]:


482 
"0 < n \<Longrightarrow> bintrunc n (sbintrunc (n  1) w) = bintrunc n w"


483 
by (cases n) (auto simp del: bintrunc.Suc)


484 


485 
lemma sbintrunc_bintrunc' [simp]:


486 
"0 < n \<Longrightarrow> sbintrunc (n  1) (bintrunc n w) = sbintrunc (n  1) w"


487 
by (cases n) (auto simp del: bintrunc.Suc)


488 


489 
lemma bin_sbin_eq_iff:


490 
"bintrunc (Suc n) x = bintrunc (Suc n) y <>


491 
sbintrunc n x = sbintrunc n y"


492 
apply (rule iffI)


493 
apply (rule box_equals [OF _ sbintrunc_bintrunc sbintrunc_bintrunc])


494 
apply simp


495 
apply (rule box_equals [OF _ bintrunc_sbintrunc bintrunc_sbintrunc])


496 
apply simp


497 
done


498 


499 
lemma bin_sbin_eq_iff':


500 
"0 < n \<Longrightarrow> bintrunc n x = bintrunc n y <>


501 
sbintrunc (n  1) x = sbintrunc (n  1) y"


502 
by (cases n) (simp_all add: bin_sbin_eq_iff del: bintrunc.Suc)


503 


504 
lemmas bintrunc_sbintruncS0 [simp] = bintrunc_sbintrunc' [unfolded One_nat_def]


505 
lemmas sbintrunc_bintruncS0 [simp] = sbintrunc_bintrunc' [unfolded One_nat_def]


506 


507 
lemmas bintrunc_bintrunc_l' = le_add1 [THEN bintrunc_bintrunc_l]


508 
lemmas sbintrunc_sbintrunc_l' = le_add1 [THEN sbintrunc_sbintrunc_l]


509 


510 
(* although bintrunc_minus_simps, if added to default simpset,


511 
tends to get applied where it's not wanted in developing the theories,


512 
we get a version for when the word length is given literally *)


513 


514 
lemmas nat_non0_gr =


515 
trans [OF iszero_def [THEN Not_eq_iff [THEN iffD2]] neq0_conv, standard]


516 


517 
lemmas bintrunc_pred_simps [simp] =


518 
bintrunc_minus_simps [of "number_of bin", simplified nobm1, standard]


519 


520 
lemmas sbintrunc_pred_simps [simp] =


521 
sbintrunc_minus_simps [of "number_of bin", simplified nobm1, standard]


522 


523 
lemma no_bintr_alt:


524 
"number_of (bintrunc n w) = w mod 2 ^ n"


525 
by (simp add: number_of_eq bintrunc_mod2p)


526 


527 
lemma no_bintr_alt1: "bintrunc n = (%w. w mod 2 ^ n :: int)"


528 
by (rule ext) (rule bintrunc_mod2p)


529 


530 
lemma range_bintrunc: "range (bintrunc n) = {i. 0 <= i & i < 2 ^ n}"


531 
apply (unfold no_bintr_alt1)


532 
apply (auto simp add: image_iff)


533 
apply (rule exI)


534 
apply (auto intro: int_mod_lem [THEN iffD1, symmetric])


535 
done


536 


537 
lemma no_bintr:


538 
"number_of (bintrunc n w) = (number_of w mod 2 ^ n :: int)"


539 
by (simp add : bintrunc_mod2p number_of_eq)


540 


541 
lemma no_sbintr_alt2:


542 
"sbintrunc n = (%w. (w + 2 ^ n) mod 2 ^ Suc n  2 ^ n :: int)"


543 
by (rule ext) (simp add : sbintrunc_mod2p)


544 


545 
lemma no_sbintr:


546 
"number_of (sbintrunc n w) =


547 
((number_of w + 2 ^ n) mod 2 ^ Suc n  2 ^ n :: int)"


548 
by (simp add : no_sbintr_alt2 number_of_eq)


549 


550 
lemma range_sbintrunc:


551 
"range (sbintrunc n) = {i.  (2 ^ n) <= i & i < 2 ^ n}"


552 
apply (unfold no_sbintr_alt2)


553 
apply (auto simp add: image_iff eq_diff_eq)


554 
apply (rule exI)


555 
apply (auto intro: int_mod_lem [THEN iffD1, symmetric])


556 
done


557 


558 
lemmas sb_inc_lem = int_mod_ge'


559 
[where n = "2 ^ (Suc ?k)" and b = "?a + 2 ^ ?k",


560 
simplified zless2p, OF _ TrueI]


561 


562 
lemmas sb_inc_lem' =


563 
iffD1 [OF less_diff_eq, THEN sb_inc_lem, simplified OrderedGroup.diff_0]


564 


565 
lemma sbintrunc_inc:


566 
"x <  (2 ^ n) ==> x + 2 ^ (Suc n) <= sbintrunc n x"


567 
unfolding no_sbintr_alt2 by (drule sb_inc_lem') simp


568 


569 
lemmas sb_dec_lem = int_mod_le'


570 
[where n = "2 ^ (Suc ?k)" and b = "?a + 2 ^ ?k",


571 
simplified zless2p, OF _ TrueI, simplified]


572 


573 
lemmas sb_dec_lem' = iffD1 [OF diff_le_eq', THEN sb_dec_lem, simplified]


574 


575 
lemma sbintrunc_dec:


576 
"x >= (2 ^ n) ==> x  2 ^ (Suc n) >= sbintrunc n x"


577 
unfolding no_sbintr_alt2 by (drule sb_dec_lem') simp


578 


579 
lemmas zmod_uminus' = zmod_uminus [where b="?c"]


580 
lemmas zpower_zmod' = zpower_zmod [where m="?c" and y="?k"]


581 


582 
lemmas brdmod1s' [symmetric] =


583 
zmod_zadd_left_eq zmod_zadd_right_eq


584 
zmod_zsub_left_eq zmod_zsub_right_eq


585 
zmod_zmult1_eq zmod_zmult1_eq_rev


586 


587 
lemmas brdmods' [symmetric] =


588 
zpower_zmod' [symmetric]


589 
trans [OF zmod_zadd_left_eq zmod_zadd_right_eq]


590 
trans [OF zmod_zsub_left_eq zmod_zsub_right_eq]


591 
trans [OF zmod_zmult1_eq zmod_zmult1_eq_rev]


592 
zmod_uminus' [symmetric]


593 
zmod_zadd_left_eq [where b = "1"]


594 
zmod_zsub_left_eq [where b = "1"]


595 


596 
lemmas bintr_arith1s =


597 
brdmod1s' [where c="2^?n", folded pred_def succ_def bintrunc_mod2p]


598 
lemmas bintr_ariths =


599 
brdmods' [where c="2^?n", folded pred_def succ_def bintrunc_mod2p]


600 


601 
lemma bintr_ge0: "(0 :: int) <= number_of (bintrunc n w)"


602 
by (simp add : no_bintr m2pths)


603 


604 
lemma bintr_lt2p: "number_of (bintrunc n w) < (2 ^ n :: int)"


605 
by (simp add : no_bintr m2pths)


606 


607 
lemma bintr_Min:


608 
"number_of (bintrunc n Numeral.Min) = (2 ^ n :: int)  1"


609 
by (simp add : no_bintr m1mod2k)


610 


611 
lemma sbintr_ge: "( (2 ^ n) :: int) <= number_of (sbintrunc n w)"


612 
by (simp add : no_sbintr m2pths)


613 


614 
lemma sbintr_lt: "number_of (sbintrunc n w) < (2 ^ n :: int)"


615 
by (simp add : no_sbintr m2pths)


616 


617 
lemma bintrunc_Suc:


618 
"bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT bin_last bin"


619 
by (case_tac bin rule: bin_exhaust) auto


620 


621 
lemma sign_Pls_ge_0:


622 
"(bin_sign bin = Numeral.Pls) = (number_of bin >= (0 :: int))"


623 
by (induct bin rule: bin_induct) auto


624 


625 
lemma sign_Min_lt_0:


626 
"(bin_sign bin = Numeral.Min) = (number_of bin < (0 :: int))"


627 
by (induct bin rule: bin_induct) auto


628 


629 
lemmas sign_Min_neg = trans [OF sign_Min_lt_0 neg_def [symmetric]]


630 


631 
lemma bin_rest_trunc:


632 
"!!bin. (bin_rest (bintrunc n bin)) = bintrunc (n  1) (bin_rest bin)"


633 
by (induct n) auto


634 


635 
lemma bin_rest_power_trunc [rule_format] :


636 
"(bin_rest ^ k) (bintrunc n bin) =


637 
bintrunc (n  k) ((bin_rest ^ k) bin)"


638 
by (induct k) (auto simp: bin_rest_trunc)


639 


640 
lemma bin_rest_trunc_i:


641 
"bintrunc n (bin_rest bin) = bin_rest (bintrunc (Suc n) bin)"


642 
by auto


643 


644 
lemma bin_rest_strunc:


645 
"!!bin. bin_rest (sbintrunc (Suc n) bin) = sbintrunc n (bin_rest bin)"


646 
by (induct n) auto


647 


648 
lemma bintrunc_rest [simp]:


649 
"!!bin. bintrunc n (bin_rest (bintrunc n bin)) = bin_rest (bintrunc n bin)"


650 
apply (induct n, simp)


651 
apply (case_tac bin rule: bin_exhaust)


652 
apply (auto simp: bintrunc_bintrunc_l)


653 
done


654 


655 
lemma sbintrunc_rest [simp]:


656 
"!!bin. sbintrunc n (bin_rest (sbintrunc n bin)) = bin_rest (sbintrunc n bin)"


657 
apply (induct n, simp)


658 
apply (case_tac bin rule: bin_exhaust)


659 
apply (auto simp: bintrunc_bintrunc_l split: bit.splits)


660 
done


661 


662 
lemma bintrunc_rest':


663 
"bintrunc n o bin_rest o bintrunc n = bin_rest o bintrunc n"


664 
by (rule ext) auto


665 


666 
lemma sbintrunc_rest' :


667 
"sbintrunc n o bin_rest o sbintrunc n = bin_rest o sbintrunc n"


668 
by (rule ext) auto


669 


670 
lemma rco_lem:


671 
"f o g o f = g o f ==> f o (g o f) ^ n = g ^ n o f"


672 
apply (rule ext)


673 
apply (induct_tac n)


674 
apply (simp_all (no_asm))


675 
apply (drule fun_cong)


676 
apply (unfold o_def)


677 
apply (erule trans)


678 
apply simp


679 
done


680 


681 
lemma rco_alt: "(f o g) ^ n o f = f o (g o f) ^ n"


682 
apply (rule ext)


683 
apply (induct n)


684 
apply (simp_all add: o_def)


685 
done


686 


687 
lemmas rco_bintr = bintrunc_rest'


688 
[THEN rco_lem [THEN fun_cong], unfolded o_def]


689 
lemmas rco_sbintr = sbintrunc_rest'


690 
[THEN rco_lem [THEN fun_cong], unfolded o_def]


691 


692 
lemmas ls_splits =


693 
prod.split split_split prod.split_asm split_split_asm split_if_asm


694 


695 
lemma not_B1_is_B0: "y \<noteq> bit.B1 \<Longrightarrow> y = bit.B0"


696 
by (cases y) auto


697 


698 
lemma B1_ass_B0:


699 
assumes y: "y = bit.B0 \<Longrightarrow> y = bit.B1"


700 
shows "y = bit.B1"


701 
apply (rule classical)


702 
apply (drule not_B1_is_B0)


703 
apply (erule y)


704 
done


705 


706 
 "simplifications for specific word lengths"


707 
lemmas n2s_ths [THEN eq_reflection] = add_2_eq_Suc add_2_eq_Suc'


708 


709 
lemmas s2n_ths = n2s_ths [symmetric]


710 


711 


712 
end


713 


714 
