src/HOL/Library/Abstract_Rat.thy

 where
   "normNum = (\<lambda>(a,b). (if a=0 \<or> b = 0 then (0,0) else 
   (let g = gcd a b 
    in if b > 0 then (a div g, b div g) else (- (a div g), - (b div g)))))"
 
-declare int_gcd_dvd1[presburger]
-declare int_gcd_dvd2[presburger]
+declare gcd_dvd1_int[presburger]
+declare gcd_dvd2_int[presburger]
 lemma normNum_isnormNum [simp]: "isnormNum (normNum x)"
 proof -
   have " \<exists> a b. x = (a,b)" by auto
   then obtain a b where x[simp]: "x = (a,b)" by blast
   {assume "a=0 \<or> b = 0" hence ?thesis by (simp add: normNum_def isnormNum_def)}  

   {assume anz: "a \<noteq> 0" and bnz: "b \<noteq> 0" 
     let ?g = "gcd a b"
     let ?a' = "a div ?g"
     let ?b' = "b div ?g"
     let ?g' = "gcd ?a' ?b'"
-    from anz bnz have "?g \<noteq> 0" by simp  with int_gcd_ge_0[of a b] 
+    from anz bnz have "?g \<noteq> 0" by simp  with gcd_ge_0_int[of a b] 
     have gpos: "?g > 0"  by arith
     have gdvd: "?g dvd a" "?g dvd b" by arith+ 
     from zdvd_mult_div_cancel[OF gdvd(1)] zdvd_mult_div_cancel[OF gdvd(2)]
     anz bnz
     have nz':"?a' \<noteq> 0" "?b' \<noteq> 0"
       by - (rule notI, simp)+
     from anz bnz have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by arith 
-    from int_div_gcd_coprime[OF stupid] have gp1: "?g' = 1" .
+    from div_gcd_coprime_int[OF stupid] have gp1: "?g' = 1" .
     from bnz have "b < 0 \<or> b > 0" by arith
     moreover
     {assume b: "b > 0"
       from b have "?b' \<ge> 0" 
 	by (presburger add: pos_imp_zdiv_nonneg_iff[OF gpos])  

   ultimately show ?thesis by blast
 qed
 
 lemma Ninv_normN[simp]: "isnormNum x \<Longrightarrow> isnormNum (Ninv x)"
   by (simp add: Ninv_def isnormNum_def split_def)
-    (cases "fst x = 0", auto simp add: int_gcd_commute)
+    (cases "fst x = 0", auto simp add: gcd_commute_int)
 
 lemma isnormNum_int[simp]: 
   "isnormNum 0\<^sub>N" "isnormNum (1::int)\<^sub>N" "i \<noteq> 0 \<Longrightarrow> isnormNum i\<^sub>N"
   by (simp_all add: isnormNum_def)
 

   { assume az: "a \<noteq> 0" and bz: "b \<noteq> 0" and a'z: "a'\<noteq>0" and b'z: "b'\<noteq>0"
     from az bz a'z b'z na nb have pos: "b > 0" "b' > 0" by (simp_all add: isnormNum_def)
     from prems have eq:"a * b' = a'*b" 
       by (simp add: INum_def  eq_divide_eq divide_eq_eq of_int_mult[symmetric] del: of_int_mult)
     from prems have gcd1: "gcd a b = 1" "gcd b a = 1" "gcd a' b' = 1" "gcd b' a' = 1"       
-      by (simp_all add: isnormNum_def add: int_gcd_commute)
+      by (simp_all add: isnormNum_def add: gcd_commute_int)
     from eq have raw_dvd: "a dvd a'*b" "b dvd b'*a" "a' dvd a*b'" "b' dvd b*a'"
       apply - 
       apply algebra
       apply algebra
       apply simp
       apply algebra
       done
-    from zdvd_dvd_eq[OF bz int_coprime_dvd_mult[OF gcd1(2) raw_dvd(2)]
-      int_coprime_dvd_mult[OF gcd1(4) raw_dvd(4)]]
+    from zdvd_dvd_eq[OF bz coprime_dvd_mult_int[OF gcd1(2) raw_dvd(2)]
+      coprime_dvd_mult_int[OF gcd1(4) raw_dvd(4)]]
       have eq1: "b = b'" using pos by arith  
       with eq have "a = a'" using pos by simp
       with eq1 have ?rhs by simp}
   ultimately show ?rhs by blast
 next

 	by (simp add: th Nadd_def normNum_def INum_def split_def)}
     moreover {assume z: "a * b' + b * a' \<noteq> 0"
       let ?g = "gcd (a * b' + b * a') (b*b')"
       have gz: "?g \<noteq> 0" using z by simp
       have ?thesis using aa' bb' z gz
-	of_int_div[where ?'a = 'a, OF gz int_gcd_dvd1[where x="a * b' + b * a'" and y="b*b'"]]	of_int_div[where ?'a = 'a,
-	OF gz int_gcd_dvd2[where x="a * b' + b * a'" and y="b*b'"]]
+	of_int_div[where ?'a = 'a, OF gz gcd_dvd1_int[where x="a * b' + b * a'" and y="b*b'"]]	of_int_div[where ?'a = 'a,
+	OF gz gcd_dvd2_int[where x="a * b' + b * a'" and y="b*b'"]]
 	by (simp add: x y Nadd_def INum_def normNum_def Let_def add_divide_distrib)}
     ultimately have ?thesis using aa' bb' 
       by (simp add: Nadd_def INum_def normNum_def x y Let_def) }
   ultimately show ?thesis by blast
 qed

       done }
   moreover
   {assume z: "a \<noteq> 0" "a' \<noteq> 0" "b \<noteq> 0" "b' \<noteq> 0"
     let ?g="gcd (a*a') (b*b')"
     have gz: "?g \<noteq> 0" using z by simp
-    from z of_int_div[where ?'a = 'a, OF gz int_gcd_dvd1[where x="a*a'" and y="b*b'"]] 
-      of_int_div[where ?'a = 'a , OF gz int_gcd_dvd2[where x="a*a'" and y="b*b'"]] 
+    from z of_int_div[where ?'a = 'a, OF gz gcd_dvd1_int[where x="a*a'" and y="b*b'"]] 
+      of_int_div[where ?'a = 'a , OF gz gcd_dvd2_int[where x="a*a'" and y="b*b'"]] 
     have ?thesis by (simp add: Nmul_def x y Let_def INum_def)}
   ultimately show ?thesis by blast
 qed
 
 lemma Nneg[simp]: "INum (~\<^sub>N x) = - (INum x ::'a:: field)"

   have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" by simp
   with isnormNum_unique[OF n] show ?thesis by simp
 qed
 
 lemma Nmul_commute: "isnormNum x \<Longrightarrow> isnormNum y \<Longrightarrow> x *\<^sub>N y = y *\<^sub>N x"
-  by (simp add: Nmul_def split_def Let_def int_gcd_commute mult_commute)
+  by (simp add: Nmul_def split_def Let_def gcd_commute_int mult_commute)
 
 lemma Nmul_assoc:
   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
   assumes nx: "isnormNum x" and ny:"isnormNum y" and nz:"isnormNum z"
   shows "x *\<^sub>N y *\<^sub>N z = x *\<^sub>N (y *\<^sub>N z)"