src/HOL/Divides.thy
changeset 55440 721b4561007a
parent 55414 eab03e9cee8a
parent 55439 db691cc79289
child 57492 74bf65a1910a
     1.1 --- a/src/HOL/Divides.thy	Wed Feb 12 10:59:25 2014 +0100
     1.2 +++ b/src/HOL/Divides.thy	Wed Feb 12 14:32:45 2014 +0100
     1.3 @@ -1968,13 +1968,13 @@
     1.4  lemma [simp]:
     1.5    shows div_one_bit0: "1 div numeral (Num.Bit0 v) = (0 :: int)"
     1.6      and mod_one_bit0: "1 mod numeral (Num.Bit0 v) = (1 :: int)"
     1.7 -	  and div_one_bit1: "1 div numeral (Num.Bit1 v) = (0 :: int)"
     1.8 -	  and mod_one_bit1: "1 mod numeral (Num.Bit1 v) = (1 :: int)"
     1.9 -	  and div_one_neg_numeral: "1 div - numeral v = (- 1 :: int)"
    1.10 -	  and mod_one_neg_numeral: "1 mod - numeral v = (1 :: int) - numeral v"
    1.11 +    and div_one_bit1: "1 div numeral (Num.Bit1 v) = (0 :: int)"
    1.12 +    and mod_one_bit1: "1 mod numeral (Num.Bit1 v) = (1 :: int)"
    1.13 +    and div_one_neg_numeral: "1 div - numeral v = (- 1 :: int)"
    1.14 +    and mod_one_neg_numeral: "1 mod - numeral v = (1 :: int) - numeral v"
    1.15    by (simp_all del: arith_special
    1.16      add: div_pos_pos mod_pos_pos div_pos_neg mod_pos_neg posDivAlg_eqn)
    1.17 -	
    1.18 +
    1.19  lemma [simp]:
    1.20    shows div_neg_one_numeral: "- 1 div numeral v = (- 1 :: int)"
    1.21      and mod_neg_one_numeral: "- 1 mod numeral v = numeral v - (1 :: int)"