
diff -r 9787769764bb -r 40501bb2d57c src/HOL/Library/Abstract_Rat.thy
--- a/src/HOL/Library/Abstract_Rat.thy	Tue Jul 07 07:56:24 2009 +0200
+++ b/src/HOL/Library/Abstract_Rat.thy	Tue Jul 07 17:39:51 2009 +0200
@@ -30,8 +30,8 @@
   (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
@@ -43,7 +43,7 @@
     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)]
@@ -51,7 +51,7 @@
     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"
@@ -137,7 +137,7 @@
 
 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"
@@ -203,7 +203,7 @@
     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
@@ -211,8 +211,8 @@
       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}
@@ -297,8 +297,8 @@
       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) }
@@ -319,8 +319,8 @@
   {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
@@ -478,7 +478,7 @@
 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})"




