src/HOL/Word/Bit_Representation.thy
changeset 45855 b49cffac6c97
parent 45853 cbb6f2243b52
child 45856 caa99836aed8
equal deleted inserted replaced
45854:40554613b4f0 45855:b49cffac6c97
   374 subsection "Simplifications for (s)bintrunc"
   374 subsection "Simplifications for (s)bintrunc"
   375 
   375 
   376 lemma bintrunc_n_0 [simp]: "bintrunc n 0 = 0"
   376 lemma bintrunc_n_0 [simp]: "bintrunc n 0 = 0"
   377   by (induct n) (auto simp add: Int.Pls_def)
   377   by (induct n) (auto simp add: Int.Pls_def)
   378 
   378 
       
   379 lemma sbintrunc_n_0 [simp]: "sbintrunc n 0 = 0"
       
   380   by (induct n) (auto simp add: Int.Pls_def)
       
   381 
   379 lemma bintrunc_Suc_numeral:
   382 lemma bintrunc_Suc_numeral:
   380   "bintrunc (Suc n) 1 = 1"
   383   "bintrunc (Suc n) 1 = 1"
   381   "bintrunc (Suc n) -1 = bintrunc n -1 BIT 1"
   384   "bintrunc (Suc n) -1 = bintrunc n -1 BIT 1"
   382   "bintrunc (Suc n) (number_of (Int.Bit0 w)) = bintrunc n (number_of w) BIT 0"
   385   "bintrunc (Suc n) (number_of (Int.Bit0 w)) = bintrunc n (number_of w) BIT 0"
   383   "bintrunc (Suc n) (number_of (Int.Bit1 w)) = bintrunc n (number_of w) BIT 1"
   386   "bintrunc (Suc n) (number_of (Int.Bit1 w)) = bintrunc n (number_of w) BIT 1"
   384   by simp_all
   387   by simp_all
   385 
   388 
       
   389 lemma sbintrunc_Suc_numeral:
       
   390   "sbintrunc (Suc n) 1 = 1"
       
   391   "sbintrunc (Suc n) -1 = sbintrunc n -1 BIT 1"
       
   392   "sbintrunc (Suc n) (number_of (Int.Bit0 w)) = sbintrunc n (number_of w) BIT 0"
       
   393   "sbintrunc (Suc n) (number_of (Int.Bit1 w)) = sbintrunc n (number_of w) BIT 1"
       
   394   by simp_all
       
   395 
   386 lemma bit_bool:
   396 lemma bit_bool:
   387   "(b = (b' = (1::bit))) = (b' = (if b then (1::bit) else (0::bit)))"
   397   "(b = (b' = (1::bit))) = (b' = (if b then (1::bit) else (0::bit)))"
   388   by (cases b') auto
   398   by (cases b') auto
   389 
   399 
   390 lemmas bit_bool1 [simp] = refl [THEN bit_bool [THEN iffD1], symmetric]
   400 lemmas bit_bool1 [simp] = refl [THEN bit_bool [THEN iffD1], symmetric]
   484   "sbintrunc (Suc n) (Int.Bit1 w) = Int.Bit1 (sbintrunc n w)"
   494   "sbintrunc (Suc n) (Int.Bit1 w) = Int.Bit1 (sbintrunc n w)"
   485   using sbintrunc_Suc_BIT [where b="(1::bit)"] by (simp add: BIT_simps)
   495   using sbintrunc_Suc_BIT [where b="(1::bit)"] by (simp add: BIT_simps)
   486 
   496 
   487 lemmas sbintrunc_Sucs = sbintrunc_Suc_Pls sbintrunc_Suc_Min sbintrunc_Suc_BIT
   497 lemmas sbintrunc_Sucs = sbintrunc_Suc_Pls sbintrunc_Suc_Min sbintrunc_Suc_BIT
   488   sbintrunc_Suc_Bit0 sbintrunc_Suc_Bit1
   498   sbintrunc_Suc_Bit0 sbintrunc_Suc_Bit1
       
   499   sbintrunc_Suc_numeral
   489 
   500 
   490 lemmas sbintrunc_Pls = 
   501 lemmas sbintrunc_Pls = 
   491   sbintrunc.Z [where bin="Int.Pls", 
   502   sbintrunc.Z [where bin="Int.Pls", 
   492                simplified bin_last_simps bin_rest_simps bit.simps]
   503                simplified bin_last_simps bin_rest_simps bit.simps]
   493 
   504