author huffman Tue Feb 21 11:04:38 2012 +0100 (2012-02-21) changeset 46560 8e252a608765 parent 46559 69a273fcd53a child 46561 092f4eca9848
remove constant negateSnd in favor of 'apsnd uminus' (from Florian Haftmann)
 src/HOL/Divides.thy file | annotate | diff | revisions src/HOL/Matrix/ComputeNumeral.thy file | annotate | diff | revisions
```     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.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.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.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
```