src/HOL/Word/Bit_Representation.thy
changeset 45954 f67d3bb5f09c
parent 45953 1d6fcb19aa50
child 45999 cce7e6197a46
equal deleted inserted replaced
45953:1d6fcb19aa50 45954:f67d3bb5f09c
   340   "sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)"
   340   "sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)"
   341   apply simp_all
   341   apply simp_all
   342   apply (simp only: Pls_def Min_def)
   342   apply (simp only: Pls_def Min_def)
   343   done
   343   done
   344 
   344 
   345 lemma sign_bintr:
   345 lemma sign_bintr: "bin_sign (bintrunc n w) = Int.Pls"
   346   "!!w. bin_sign (bintrunc n w) = Int.Pls"
   346   by (induct n arbitrary: w) auto
   347   by (induct n) auto
   347 
   348 
   348 lemma bintrunc_mod2p: "bintrunc n w = (w mod 2 ^ n)"
   349 lemma bintrunc_mod2p:
   349   apply (induct n arbitrary: w)
   350   "!!w. bintrunc n w = (w mod 2 ^ n :: int)"
       
   351   apply (induct n)
       
   352   apply (simp add: Pls_def)
   350   apply (simp add: Pls_def)
   353   apply (simp add: bin_last_def bin_rest_def Bit_def zmod_zmult2_eq
   351   apply (simp add: bin_last_def bin_rest_def Bit_def zmod_zmult2_eq)
   354               cong: number_of_False_cong)
   352   done
   355   done
   353 
   356 
   354 lemma sbintrunc_mod2p: "sbintrunc n w = (w + 2 ^ n) mod 2 ^ (Suc n) - 2 ^ n"
   357 lemma sbintrunc_mod2p:
   355   apply (induct n arbitrary: w)
   358   "!!w. sbintrunc n w = ((w + 2 ^ n) mod 2 ^ (Suc n) - 2 ^ n :: int)"
       
   359   apply (induct n)
       
   360    apply clarsimp
   356    apply clarsimp
   361    apply (subst mod_add_left_eq)
   357    apply (subst mod_add_left_eq)
   362    apply (simp add: bin_last_def)
   358    apply (simp add: bin_last_def)
   363    apply (simp add: number_of_eq)
   359    apply (simp add: number_of_eq)
   364   apply (simp add: Pls_def)
   360   apply (simp add: Pls_def)
   405   "(b = (b' = (1::bit))) = (b' = (if b then (1::bit) else (0::bit)))"
   401   "(b = (b' = (1::bit))) = (b' = (if b then (1::bit) else (0::bit)))"
   406   by (cases b') auto
   402   by (cases b') auto
   407 
   403 
   408 lemmas bit_bool1 [simp] = refl [THEN bit_bool [THEN iffD1], symmetric]
   404 lemmas bit_bool1 [simp] = refl [THEN bit_bool [THEN iffD1], symmetric]
   409 
   405 
   410 lemma bin_sign_lem:
   406 lemma bin_sign_lem: "(bin_sign (sbintrunc n bin) = Int.Min) = bin_nth bin n"
   411   "!!bin. (bin_sign (sbintrunc n bin) = Int.Min) = bin_nth bin n"
   407   apply (induct n arbitrary: bin)
   412   apply (induct n)
       
   413    apply (case_tac bin rule: bin_exhaust, case_tac b, auto)+
   408    apply (case_tac bin rule: bin_exhaust, case_tac b, auto)+
   414   done
   409   done
   415 
   410 
   416 lemma nth_bintr:
   411 lemma nth_bintr: "bin_nth (bintrunc m w) n = (n < m & bin_nth w n)"
   417   "!!w m. bin_nth (bintrunc m w) n = (n < m & bin_nth w n)"
   412   apply (induct n arbitrary: w m)
   418   apply (induct n)
       
   419    apply (case_tac m, auto)[1]
   413    apply (case_tac m, auto)[1]
   420   apply (case_tac m, auto)[1]
   414   apply (case_tac m, auto)[1]
   421   done
   415   done
   422 
   416 
   423 lemma nth_sbintr:
   417 lemma nth_sbintr:
   424   "!!w m. bin_nth (sbintrunc m w) n = 
   418   "bin_nth (sbintrunc m w) n = 
   425           (if n < m then bin_nth w n else bin_nth w m)"
   419           (if n < m then bin_nth w n else bin_nth w m)"
   426   apply (induct n)
   420   apply (induct n arbitrary: w m)
   427    apply (case_tac m, simp_all split: bit.splits)[1]
   421    apply (case_tac m, simp_all split: bit.splits)[1]
   428   apply (case_tac m, simp_all split: bit.splits)[1]
   422   apply (case_tac m, simp_all split: bit.splits)[1]
   429   done
   423   done
   430 
   424 
   431 lemma bin_nth_Bit:
   425 lemma bin_nth_Bit:
   769   by (induct bin rule: numeral_induct) auto
   763   by (induct bin rule: numeral_induct) auto
   770 
   764 
   771 lemmas sign_Min_neg = trans [OF sign_Min_lt_0 neg_def [symmetric]] 
   765 lemmas sign_Min_neg = trans [OF sign_Min_lt_0 neg_def [symmetric]] 
   772 
   766 
   773 lemma bin_rest_trunc:
   767 lemma bin_rest_trunc:
   774   "!!bin. (bin_rest (bintrunc n bin)) = bintrunc (n - 1) (bin_rest bin)"
   768   "(bin_rest (bintrunc n bin)) = bintrunc (n - 1) (bin_rest bin)"
   775   by (induct n) auto
   769   by (induct n arbitrary: bin) auto
   776 
   770 
   777 lemma bin_rest_power_trunc [rule_format] :
   771 lemma bin_rest_power_trunc [rule_format] :
   778   "(bin_rest ^^ k) (bintrunc n bin) = 
   772   "(bin_rest ^^ k) (bintrunc n bin) = 
   779     bintrunc (n - k) ((bin_rest ^^ k) bin)"
   773     bintrunc (n - k) ((bin_rest ^^ k) bin)"
   780   by (induct k) (auto simp: bin_rest_trunc)
   774   by (induct k) (auto simp: bin_rest_trunc)
   782 lemma bin_rest_trunc_i:
   776 lemma bin_rest_trunc_i:
   783   "bintrunc n (bin_rest bin) = bin_rest (bintrunc (Suc n) bin)"
   777   "bintrunc n (bin_rest bin) = bin_rest (bintrunc (Suc n) bin)"
   784   by auto
   778   by auto
   785 
   779 
   786 lemma bin_rest_strunc:
   780 lemma bin_rest_strunc:
   787   "!!bin. bin_rest (sbintrunc (Suc n) bin) = sbintrunc n (bin_rest bin)"
   781   "bin_rest (sbintrunc (Suc n) bin) = sbintrunc n (bin_rest bin)"
   788   by (induct n) auto
   782   by (induct n arbitrary: bin) auto
   789 
   783 
   790 lemma bintrunc_rest [simp]: 
   784 lemma bintrunc_rest [simp]: 
   791   "!!bin. bintrunc n (bin_rest (bintrunc n bin)) = bin_rest (bintrunc n bin)"
   785   "bintrunc n (bin_rest (bintrunc n bin)) = bin_rest (bintrunc n bin)"
   792   apply (induct n, simp)
   786   apply (induct n arbitrary: bin, simp)
   793   apply (case_tac bin rule: bin_exhaust)
   787   apply (case_tac bin rule: bin_exhaust)
   794   apply (auto simp: bintrunc_bintrunc_l)
   788   apply (auto simp: bintrunc_bintrunc_l)
   795   done
   789   done
   796 
   790 
   797 lemma sbintrunc_rest [simp]:
   791 lemma sbintrunc_rest [simp]:
   798   "!!bin. sbintrunc n (bin_rest (sbintrunc n bin)) = bin_rest (sbintrunc n bin)"
   792   "sbintrunc n (bin_rest (sbintrunc n bin)) = bin_rest (sbintrunc n bin)"
   799   apply (induct n, simp)
   793   apply (induct n arbitrary: bin, simp)
   800   apply (case_tac bin rule: bin_exhaust)
   794   apply (case_tac bin rule: bin_exhaust)
   801   apply (auto simp: bintrunc_bintrunc_l split: bit.splits)
   795   apply (auto simp: bintrunc_bintrunc_l split: bit.splits)
   802   done
   796   done
   803 
   797 
   804 lemma bintrunc_rest':
   798 lemma bintrunc_rest':