src/HOL/Complex/ex/MIR.thy

   from prems have th:"zgcd c ?g > 1" by simp
   from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
   have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp
   moreover {assume "abs c > 1" and gp: "?g > 1" with prems
     have th: "dvdnumcoeff t ?g" by simp
-    have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_dvd2)
-    from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_dvd1)}
+    have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2)
+    from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1)}
   moreover {assume "abs c = 0 \<and> ?g > 1"
     with prems have th: "dvdnumcoeff t ?g" by simp
-    have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_dvd2)
-    from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_dvd1)
+    have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2)
+    from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1)
     hence ?case by simp }
   moreover {assume "abs c > 1" and g0:"?g = 0" 
     from numgcdh0[OF g0] have "m=0". with prems   have ?case by simp }
   ultimately show ?case by blast
 next

   from prems have th:"zgcd c ?g > 1" by simp
   from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
   have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp
   moreover {assume "abs c > 1" and gp: "?g > 1" with prems
     have th: "dvdnumcoeff t ?g" by simp
-    have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_dvd2)
-    from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_dvd1)}
+    have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2)
+    from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1)}
   moreover {assume "abs c = 0 \<and> ?g > 1"
     with prems have th: "dvdnumcoeff t ?g" by simp
-    have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_dvd2)
-    from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_dvd1)
+    have th': "zgcd c ?g dvd ?g" by (simp add:zgcd_zdvd2)
+    from dvdnumcoeff_trans[OF th' th] have ?case by (simp add: zgcd_zdvd1)
     hence ?case by simp }
   moreover {assume "abs c > 1" and g0:"?g = 0" 
     from numgcdh0[OF g0] have "m=0". with prems   have ?case by simp }
   ultimately show ?case by blast
-qed(auto simp add: zgcd_dvd1)
+qed(auto simp add: zgcd_zdvd1)
 
 lemma dvdnumcoeff_aux2:
   assumes "numgcd t > 1" shows "dvdnumcoeff t (numgcd t) \<and> numgcd t > 0"
   using prems 
 proof (simp add: numgcd_def)

       moreover {assume "?g'=1" hence ?thesis by (simp add: Let_def simp_num_pair_def)}
       moreover {assume g'1:"?g'>1"
 	from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff ?t' ?g" ..
 	let ?tt = "reducecoeffh ?t' ?g'"
 	let ?t = "Inum bs ?tt"
-	have gpdg: "?g' dvd ?g" by (simp add: zgcd_dvd2)
-	have gpdd: "?g' dvd n" by (simp add: zgcd_dvd1) 
+	have gpdg: "?g' dvd ?g" by (simp add: zgcd_zdvd2)
+	have gpdd: "?g' dvd n" by (simp add: zgcd_zdvd1) 
 	have gpdgp: "?g' dvd ?g'" by simp
 	from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p] 
 	have th2:"real ?g' * ?t = Inum bs ?t'" by simp
 	from prems have "?lhs = ?t / real (n div ?g')" by (simp add: simp_num_pair_def Let_def)
 	also have "\<dots> = (real ?g' * ?t) / (real ?g' * (real (n div ?g')))" by simp

       hence g'p: "?g' > 0" using zgcd_pos[where i="n" and j="numgcd ?t'"] by arith
       hence "?g'= 1 \<or> ?g' > 1" by arith
       moreover {assume "?g'=1" hence ?thesis using prems 
 	  by (auto simp add: Let_def simp_num_pair_def)}
       moreover {assume g'1:"?g'>1"
-	have gpdg: "?g' dvd ?g" by (simp add: zgcd_dvd2)
-	have gpdd: "?g' dvd n" by (simp add: zgcd_dvd1) 
+	have gpdg: "?g' dvd ?g" by (simp add: zgcd_zdvd2)
+	have gpdd: "?g' dvd n" by (simp add: zgcd_zdvd1) 
 	have gpdgp: "?g' dvd ?g'" by simp
 	from zdvd_imp_le[OF gpdd np] have g'n: "?g' \<le> n" .
 	from zdiv_mono1[OF g'n g'p, simplified zdiv_self[OF gp0]]
 	have "n div ?g' >0" by simp
 	hence ?thesis using prems 

     moreover {assume "?g'=1" hence ?thesis by (simp add: Let_def simpdvd_def)}
     moreover {assume g'1:"?g'>1"
       from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff t ?g" ..
       let ?tt = "reducecoeffh t ?g'"
       let ?t = "Inum bs ?tt"
-      have gpdg: "?g' dvd ?g" by (simp add: zgcd_dvd2)
-      have gpdd: "?g' dvd d" by (simp add: zgcd_dvd1) 
+      have gpdg: "?g' dvd ?g" by (simp add: zgcd_zdvd2)
+      have gpdd: "?g' dvd d" by (simp add: zgcd_zdvd1) 
       have gpdgp: "?g' dvd ?g'" by simp
       from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p] 
       have th2:"real ?g' * ?t = Inum bs t" by simp
       from prems have "Ifm bs (Dvd (fst (simpdvd d t)) (snd(simpdvd d t))) = Ifm bs (Dvd (d div ?g') ?tt)"
 	by (simp add: simpdvd_def Let_def)

 
 lemma bound0at_l : "\<lbrakk>isatom p ; bound0 p\<rbrakk> \<Longrightarrow> isrlfm p"
   by (induct p rule: isrlfm.induct, auto)
 lemma zgcd_le1: assumes ip: "0 < i" shows "zgcd i j \<le> i"
 proof-
-  from zgcd_dvd1 have th: "zgcd i j dvd i" by blast
+  from zgcd_zdvd1 have th: "zgcd i j dvd i" by blast
   from zdvd_imp_le[OF th ip] show ?thesis .
 qed
 
 
 lemma simpfm_rl: "isrlfm p \<Longrightarrow> isrlfm (simpfm p)"