src/HOL/Library/Abstract_Rat.thy
changeset 27567 e3fe9a327c63
parent 27556 292098f2efdf
child 27668 6eb20b2cecf8
     1.1 --- a/src/HOL/Library/Abstract_Rat.thy	Mon Jul 14 11:19:43 2008 +0200
     1.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Mon Jul 14 16:13:42 2008 +0200
     1.3 @@ -44,7 +44,7 @@
     1.4      let ?g' = "zgcd ?a' ?b'"
     1.5      from anz bnz have "?g \<noteq> 0" by simp  with zgcd_pos[of a b] 
     1.6      have gpos: "?g > 0"  by arith
     1.7 -    have gdvd: "?g dvd a" "?g dvd b" by (simp_all add: zgcd_dvd1 zgcd_dvd2)
     1.8 +    have gdvd: "?g dvd a" "?g dvd b" by (simp_all add: zgcd_zdvd1 zgcd_zdvd2)
     1.9      from zdvd_mult_div_cancel[OF gdvd(1)] zdvd_mult_div_cancel[OF gdvd(2)]
    1.10      anz bnz
    1.11      have nz':"?a' \<noteq> 0" "?b' \<noteq> 0" 
    1.12 @@ -296,10 +296,8 @@
    1.13        let ?g = "zgcd (a * b' + b * a') (b*b')"
    1.14        have gz: "?g \<noteq> 0" using z by simp
    1.15        have ?thesis using aa' bb' z gz
    1.16 -	of_int_div[where ?'a = 'a, 
    1.17 -	OF gz zgcd_dvd1[where i="a * b' + b * a'" and j="b*b'"]]
    1.18 -	of_int_div[where ?'a = 'a,
    1.19 -	OF gz zgcd_dvd2[where i="a * b' + b * a'" and j="b*b'"]]
    1.20 +	of_int_div[where ?'a = 'a, OF gz zgcd_zdvd1[where i="a * b' + b * a'" and j="b*b'"]]	of_int_div[where ?'a = 'a,
    1.21 +	OF gz zgcd_zdvd2[where i="a * b' + b * a'" and j="b*b'"]]
    1.22  	by (simp add: x y Nadd_def INum_def normNum_def Let_def add_divide_distrib)}
    1.23      ultimately have ?thesis using aa' bb' 
    1.24        by (simp add: Nadd_def INum_def normNum_def x y Let_def) }
    1.25 @@ -320,8 +318,8 @@
    1.26    {assume z: "a \<noteq> 0" "a' \<noteq> 0" "b \<noteq> 0" "b' \<noteq> 0"
    1.27      let ?g="zgcd (a*a') (b*b')"
    1.28      have gz: "?g \<noteq> 0" using z by simp
    1.29 -    from z of_int_div[where ?'a = 'a, OF gz zgcd_dvd1[where i="a*a'" and j="b*b'"]] 
    1.30 -      of_int_div[where ?'a = 'a , OF gz zgcd_dvd2[where i="a*a'" and j="b*b'"]] 
    1.31 +    from z of_int_div[where ?'a = 'a, OF gz zgcd_zdvd1[where i="a*a'" and j="b*b'"]] 
    1.32 +      of_int_div[where ?'a = 'a , OF gz zgcd_zdvd2[where i="a*a'" and j="b*b'"]] 
    1.33      have ?thesis by (simp add: Nmul_def x y Let_def INum_def)}
    1.34    ultimately show ?thesis by blast
    1.35  qed