remove constant negateSnd in favor of 'apsnd uminus' (from Florian Haftmann)
authorhuffman
Tue Feb 21 11:04:38 2012 +0100 (2012-02-21)
changeset 465608e252a608765
parent 46559 69a273fcd53a
child 46561 092f4eca9848
remove constant negateSnd in favor of 'apsnd uminus' (from Florian Haftmann)
src/HOL/Divides.thy
src/HOL/Matrix/ComputeNumeral.thy
     1.1 --- a/src/HOL/Divides.thy	Tue Feb 21 10:30:57 2012 +0100
     1.2 +++ b/src/HOL/Divides.thy	Tue Feb 21 11:04:38 2012 +0100
     1.3 @@ -1207,8 +1207,6 @@
     1.4    (auto simp add: mult_2)
     1.5  
     1.6  text{*algorithm for the general case @{term "b\<noteq>0"}*}
     1.7 -definition negateSnd :: "int \<times> int \<Rightarrow> int \<times> int" where
     1.8 -  [code_unfold]: "negateSnd = apsnd uminus"
     1.9  
    1.10  definition divmod_int :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
    1.11      --{*The full division algorithm considers all possible signs for a, b
    1.12 @@ -1216,10 +1214,10 @@
    1.13         @{term negDivAlg} requires @{term "a<0"}.*}
    1.14    "divmod_int a b = (if 0 \<le> a then if 0 \<le> b then posDivAlg a b
    1.15                    else if a = 0 then (0, 0)
    1.16 -                       else negateSnd (negDivAlg (-a) (-b))
    1.17 +                       else apsnd uminus (negDivAlg (-a) (-b))
    1.18                 else 
    1.19                    if 0 < b then negDivAlg a b
    1.20 -                  else negateSnd (posDivAlg (-a) (-b)))"
    1.21 +                  else apsnd uminus (posDivAlg (-a) (-b)))"
    1.22  
    1.23  instantiation int :: Divides.div
    1.24  begin
    1.25 @@ -1232,7 +1230,7 @@
    1.26    by (simp add: div_int_def)
    1.27  
    1.28  definition mod_int where
    1.29 - "a mod b = snd (divmod_int a b)"
    1.30 +  "a mod b = snd (divmod_int a b)"
    1.31  
    1.32  lemma snd_divmod_int [simp]:
    1.33    "snd (divmod_int a b) = a mod b"
    1.34 @@ -1392,10 +1390,7 @@
    1.35  lemma negDivAlg_minus1 [simp]: "negDivAlg -1 b = (-1, b - 1)"
    1.36  by (subst negDivAlg.simps, auto)
    1.37  
    1.38 -lemma negateSnd_eq [simp]: "negateSnd(q,r) = (q,-r)"
    1.39 -by (simp add: negateSnd_def)
    1.40 -
    1.41 -lemma divmod_int_rel_neg: "divmod_int_rel (-a) (-b) qr ==> divmod_int_rel a b (negateSnd qr)"
    1.42 +lemma divmod_int_rel_neg: "divmod_int_rel (-a) (-b) qr ==> divmod_int_rel a b (apsnd uminus qr)"
    1.43  by (auto simp add: split_ifs divmod_int_rel_def)
    1.44  
    1.45  lemma divmod_int_correct: "b \<noteq> 0 ==> divmod_int_rel a b (divmod_int a b)"
    1.46 @@ -1645,21 +1640,21 @@
    1.47  text{*a positive, b negative *}
    1.48  
    1.49  lemma div_pos_neg:
    1.50 -     "[| 0 < a;  b < 0 |] ==> a div b = fst (negateSnd (negDivAlg (-a) (-b)))"
    1.51 +     "[| 0 < a;  b < 0 |] ==> a div b = fst (apsnd uminus (negDivAlg (-a) (-b)))"
    1.52  by (simp add: div_int_def divmod_int_def)
    1.53  
    1.54  lemma mod_pos_neg:
    1.55 -     "[| 0 < a;  b < 0 |] ==> a mod b = snd (negateSnd (negDivAlg (-a) (-b)))"
    1.56 +     "[| 0 < a;  b < 0 |] ==> a mod b = snd (apsnd uminus (negDivAlg (-a) (-b)))"
    1.57  by (simp add: mod_int_def divmod_int_def)
    1.58  
    1.59  text{*a negative, b negative *}
    1.60  
    1.61  lemma div_neg_neg:
    1.62 -     "[| a < 0;  b \<le> 0 |] ==> a div b = fst (negateSnd (posDivAlg (-a) (-b)))"
    1.63 +     "[| a < 0;  b \<le> 0 |] ==> a div b = fst (apsnd uminus (posDivAlg (-a) (-b)))"
    1.64  by (simp add: div_int_def divmod_int_def)
    1.65  
    1.66  lemma mod_neg_neg:
    1.67 -     "[| a < 0;  b \<le> 0 |] ==> a mod b = snd (negateSnd (posDivAlg (-a) (-b)))"
    1.68 +     "[| a < 0;  b \<le> 0 |] ==> a mod b = snd (apsnd uminus (posDivAlg (-a) (-b)))"
    1.69  by (simp add: mod_int_def divmod_int_def)
    1.70  
    1.71  text {*Simplify expresions in which div and mod combine numerical constants*}
     2.1 --- a/src/HOL/Matrix/ComputeNumeral.thy	Tue Feb 21 10:30:57 2012 +0100
     2.2 +++ b/src/HOL/Matrix/ComputeNumeral.thy	Tue Feb 21 11:04:38 2012 +0100
     2.3 @@ -147,19 +147,16 @@
     2.4  lemma adjust: "adjust b (q, r) = (if 0 \<le> r - b then (2 * q + 1, r - b) else (2 * q, r))"
     2.5    by (auto simp only: adjust_def)
     2.6  
     2.7 -lemma negateSnd: "negateSnd (q, r) = (q, -r)" 
     2.8 -  by (simp add: negateSnd_def)
     2.9 -
    2.10  lemma divmod: "divmod_int a b = (if 0\<le>a then
    2.11                    if 0\<le>b then posDivAlg a b
    2.12                    else if a=0 then (0, 0)
    2.13 -                       else negateSnd (negDivAlg (-a) (-b))
    2.14 +                       else apsnd uminus (negDivAlg (-a) (-b))
    2.15                 else 
    2.16                    if 0<b then negDivAlg a b
    2.17 -                  else negateSnd (posDivAlg (-a) (-b)))"
    2.18 +                  else apsnd uminus (posDivAlg (-a) (-b)))"
    2.19    by (auto simp only: divmod_int_def)
    2.20  
    2.21 -lemmas compute_div_mod = div_int_def mod_int_def divmod adjust negateSnd posDivAlg.simps negDivAlg.simps
    2.22 +lemmas compute_div_mod = div_int_def mod_int_def divmod adjust posDivAlg.simps negDivAlg.simps
    2.23  
    2.24  
    2.25