more direct simplification rules for 1 div/mod numeral;
authorhaftmann
Thu Jan 30 10:00:53 2014 +0100 (2014-01-30)
changeset 5517292735f0d5302
parent 55171 dc7a6f6be01b
child 55175 56c0d70127a9
more direct simplification rules for 1 div/mod numeral;
added simplification rules for (- 1) div/mod numeral
src/HOL/Divides.thy
src/HOL/Number_Theory/Residues.thy
     1.1 --- a/src/HOL/Divides.thy	Thu Jan 30 01:03:55 2014 +0100
     1.2 +++ b/src/HOL/Divides.thy	Thu Jan 30 10:00:53 2014 +0100
     1.3 @@ -1963,30 +1963,26 @@
     1.4      negDivAlg_eqn [of "numeral v" "- numeral w", OF zero_less_numeral] for v w
     1.5  
     1.6  
     1.7 -text{*Special-case simplification *}
     1.8 -
     1.9 -(** The last remaining special cases for constant arithmetic:
    1.10 -    1 div z and 1 mod z **)
    1.11 -
    1.12 -lemmas div_pos_pos_1_numeral [simp] =
    1.13 -  div_pos_pos [OF zero_less_one, of "numeral w", OF zero_le_numeral] for w
    1.14 -
    1.15 -lemmas div_pos_neg_1_numeral [simp] =
    1.16 -  div_pos_neg [OF zero_less_one, of "- numeral w",
    1.17 -  OF neg_numeral_less_zero] for w
    1.18 -
    1.19 -lemmas mod_pos_pos_1_numeral [simp] =
    1.20 -  mod_pos_pos [OF zero_less_one, of "numeral w", OF zero_le_numeral] for w
    1.21 -
    1.22 -lemmas mod_pos_neg_1_numeral [simp] =
    1.23 -  mod_pos_neg [OF zero_less_one, of "- numeral w",
    1.24 -  OF neg_numeral_less_zero] for w
    1.25 -
    1.26 -lemmas posDivAlg_eqn_1_numeral [simp] =
    1.27 -    posDivAlg_eqn [of concl: 1 "numeral w", OF zero_less_numeral] for w
    1.28 -
    1.29 -lemmas negDivAlg_eqn_1_numeral [simp] =
    1.30 -    negDivAlg_eqn [of concl: 1 "numeral w", OF zero_less_numeral] for w
    1.31 +text {* Special-case simplification: @{text "\<plusminus>1 div z"} and @{text "\<plusminus>1 mod z"} *}
    1.32 +
    1.33 +lemma [simp]:
    1.34 +  shows div_one_bit0: "1 div numeral (Num.Bit0 v) = (0 :: int)"
    1.35 +    and mod_one_bit0: "1 mod numeral (Num.Bit0 v) = (1 :: int)"
    1.36 +	  and div_one_bit1: "1 div numeral (Num.Bit1 v) = (0 :: int)"
    1.37 +	  and mod_one_bit1: "1 mod numeral (Num.Bit1 v) = (1 :: int)"
    1.38 +	  and div_one_neg_numeral: "1 div - numeral v = (- 1 :: int)"
    1.39 +	  and mod_one_neg_numeral: "1 mod - numeral v = (1 :: int) - numeral v"
    1.40 +  by (simp_all del: arith_special
    1.41 +    add: div_pos_pos mod_pos_pos div_pos_neg mod_pos_neg posDivAlg_eqn)
    1.42 +	
    1.43 +lemma [simp]:
    1.44 +  shows div_neg_one_numeral: "- 1 div numeral v = (- 1 :: int)"
    1.45 +    and mod_neg_one_numeral: "- 1 mod numeral v = numeral v - (1 :: int)"
    1.46 +    and div_neg_one_neg_bit0: "- 1 div - numeral (Num.Bit0 v) = (0 :: int)"
    1.47 +    and mod_neg_one_neb_bit0: "- 1 mod - numeral (Num.Bit0 v) = (- 1 :: int)"
    1.48 +    and div_neg_one_neg_bit1: "- 1 div - numeral (Num.Bit1 v) = (0 :: int)"
    1.49 +    and mod_neg_one_neb_bit1: "- 1 mod - numeral (Num.Bit1 v) = (- 1 :: int)"
    1.50 +  by (simp_all add: div_eq_minus1 zmod_minus1)
    1.51  
    1.52  
    1.53  subsubsection {* Monotonicity in the First Argument (Dividend) *}
     2.1 --- a/src/HOL/Number_Theory/Residues.thy	Thu Jan 30 01:03:55 2014 +0100
     2.2 +++ b/src/HOL/Number_Theory/Residues.thy	Thu Jan 30 10:00:53 2014 +0100
     2.3 @@ -453,7 +453,6 @@
     2.4    apply (subst fact_altdef_int, simp)
     2.5    apply (subst cong_int_def)
     2.6    apply simp
     2.7 -  apply presburger
     2.8    apply (rule residues_prime.wilson_theorem1)
     2.9    apply (rule residues_prime.intro)
    2.10    apply auto