summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/Abstract_Rat.thy

changeset 47162 | 9d7d919b9fd8 |

parent 44780 | a13cdb1e9e08 |

child 50282 | fe4d4bb9f4c2 |

1.1 --- a/src/HOL/Library/Abstract_Rat.thy Tue Mar 27 15:34:36 2012 +0200 1.2 +++ b/src/HOL/Library/Abstract_Rat.thy Tue Mar 27 15:40:11 2012 +0200 1.3 @@ -40,7 +40,7 @@ 1.4 from anz bnz have "?g \<noteq> 0" by simp with gcd_ge_0_int[of a b] 1.5 have gpos: "?g > 0" by arith 1.6 have gdvd: "?g dvd a" "?g dvd b" by arith+ 1.7 - from zdvd_mult_div_cancel[OF gdvd(1)] zdvd_mult_div_cancel[OF gdvd(2)] anz bnz 1.8 + from dvd_mult_div_cancel[OF gdvd(1)] dvd_mult_div_cancel[OF gdvd(2)] anz bnz 1.9 have nz': "?a' \<noteq> 0" "?b' \<noteq> 0" by - (rule notI, simp)+ 1.10 from anz bnz have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by arith 1.11 from div_gcd_coprime_int[OF stupid] have gp1: "?g' = 1" . 1.12 @@ -56,7 +56,7 @@ 1.13 assume b: "b < 0" 1.14 { assume b': "?b' \<ge> 0" 1.15 from gpos have th: "?g \<ge> 0" by arith 1.16 - from mult_nonneg_nonneg[OF th b'] zdvd_mult_div_cancel[OF gdvd(2)] 1.17 + from mult_nonneg_nonneg[OF th b'] dvd_mult_div_cancel[OF gdvd(2)] 1.18 have False using b by arith } 1.19 hence b': "?b' < 0" by (presburger add: linorder_not_le[symmetric]) 1.20 from anz bnz nz' b b' gp1 have ?thesis