src/HOL/Decision_Procs/MIR.thy

   assume lb: "real n \<le> x"
     and ub: "x < real n + 1"
   have "real (floor x) \<le> x" by simp 
   hence "real (floor x) < real (n + 1) " using ub by arith
   hence "floor x < n+1" by simp
-  moreover from lb have "n \<le> floor x" using floor_mono2[where x="real n" and y="x"] 
+  moreover from lb have "n \<le> floor x" using floor_mono[where x="real n" and y="x"] 
     by simp ultimately show "floor x = n" by simp
 qed
 
 (* Periodicity of dvd *)
 lemma dvd_period:

   "(abs (real d) rdvd t) = (real (d ::int) rdvd t)"
 proof
   assume d: "real d rdvd t"
   from d int_rdvd_real have d2: "d dvd (floor t)" and ti: "real (floor t) = t" by auto
 
-  from iffD2[OF zdvd_abs1] d2 have "(abs d) dvd (floor t)" by blast
+  from iffD2[OF abs_dvd_iff] d2 have "(abs d) dvd (floor t)" by blast
   with ti int_rdvd_real[symmetric] have "real (abs d) rdvd t" by blast 
   thus "abs (real d) rdvd t" by simp
 next
   assume "abs (real d) rdvd t" hence "real (abs d) rdvd t" by simp
   with int_rdvd_real[where i="abs d" and x="t"] have d2: "abs d dvd floor t" and ti: "real (floor t) =t" by auto
-  from iffD1[OF zdvd_abs1] d2 have "d dvd floor t" by blast
+  from iffD1[OF abs_dvd_iff] d2 have "d dvd floor t" by blast
   with ti int_rdvd_real[symmetric] show "real d rdvd t" by blast
 qed
 
 lemma rdvd_minus: "(real (d::int) rdvd t) = (real d rdvd -t)"
   apply (auto simp add: rdvd_def)

 
 lemma dvdnumcoeff_trans: 
   assumes gdg: "g dvd g'" and dgt':"dvdnumcoeff t g'"
   shows "dvdnumcoeff t g"
   using dgt' gdg 
-  by (induct t rule: dvdnumcoeff.induct, simp_all add: gdg zdvd_trans[OF gdg])
-
-declare zdvd_trans [trans add]
+  by (induct t rule: dvdnumcoeff.induct, simp_all add: gdg dvd_trans[OF gdg])
+
+declare dvd_trans [trans add]
 
 lemma natabs0: "(nat (abs x) = 0) = (x = 0)"
 by arith
 
 lemma numgcd0:

 
 lemma split_int_le_real: 
   "(real (a::int) \<le> b) = (a \<le> floor b \<or> (a = floor b \<and> real (floor b) < b))"
 proof( auto)
   assume alb: "real a \<le> b" and agb: "\<not> a \<le> floor b"
-  from alb have "floor (real a) \<le> floor b " by (simp only: floor_mono2) 
+  from alb have "floor (real a) \<le> floor b " by (simp only: floor_mono) 
   hence "a \<le> floor b" by simp with agb show "False" by simp
 next
   assume alb: "a \<le> floor b"
-  hence "real a \<le> real (floor b)" by (simp only: floor_mono2)
+  hence "real a \<le> real (floor b)" by (simp only: floor_mono)
   also have "\<dots>\<le> b" by simp  finally show  "real a \<le> b" . 
 qed
 
 lemma split_int_le_real': 
   "(real (a::int) + b \<le> 0) = (real a - real (floor(-b)) \<le> 0 \<or> (real a - real (floor (-b)) = 0 \<and> real (floor (-b)) + b < 0))"

   and ad: "d\<delta> p d"
   shows "d\<delta> p d'"
   using lin ad d
 proof(induct p rule: iszlfm.induct)
   case (9 i c e)  thus ?case using d
-    by (simp add: zdvd_trans[where m="i" and n="d" and k="d'"])
+    by (simp add: dvd_trans[of "i" "d" "d'"])
 next
   case (10 i c e) thus ?case using d
-    by (simp add: zdvd_trans[where m="i" and n="d" and k="d'"])
+    by (simp add: dvd_trans[of "i" "d" "d'"])
 qed simp_all
 
 lemma \<delta> : assumes lin:"iszlfm p bs"
   shows "d\<delta> p (\<delta> p) \<and> \<delta> p >0"
 using lin

 lemma d\<beta>_mono: 
   assumes linp: "iszlfm p (a #bs)"
   and dr: "d\<beta> p l"
   and d: "l dvd l'"
   shows "d\<beta> p l'"
-using dr linp zdvd_trans[where n="l" and k="l'", simplified d]
+using dr linp dvd_trans[of _ "l" "l'", simplified d]
 by (induct p rule: iszlfm.induct) simp_all
 
 lemma \<alpha>_l: assumes lp: "iszlfm p (a#bs)"
   shows "\<forall> b\<in> set (\<alpha> p). numbound0 b \<and> isint b (a#bs)"
 using lp

     from cp have cnz: "c \<noteq> 0" by simp
     have "c div c\<le> l div c"
       by (simp add: zdiv_mono1[OF clel cp])
     then have ldcp:"0 < l div c" 
       by (simp add: zdiv_self[OF cnz])
-    have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+    have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
       by simp
     hence "(real l * real x + real (l div c) * Inum (real x # bs) e < (0\<Colon>real)) =
           (real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e < 0)"
       by simp

     from cp have cnz: "c \<noteq> 0" by simp
     have "c div c\<le> l div c"
       by (simp add: zdiv_mono1[OF clel cp])
     then have ldcp:"0 < l div c" 
       by (simp add: zdiv_self[OF cnz])
-    have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+    have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
       by simp
     hence "(real l * real x + real (l div c) * Inum (real x # bs) e \<le> (0\<Colon>real)) =
           (real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e \<le> 0)"
       by simp

     from cp have cnz: "c \<noteq> 0" by simp
     have "c div c\<le> l div c"
       by (simp add: zdiv_mono1[OF clel cp])
     then have ldcp:"0 < l div c" 
       by (simp add: zdiv_self[OF cnz])
-    have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+    have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
       by simp
     hence "(real l * real x + real (l div c) * Inum (real x # bs) e > (0\<Colon>real)) =
           (real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e > 0)"
       by simp

     from cp have cnz: "c \<noteq> 0" by simp
     have "c div c\<le> l div c"
       by (simp add: zdiv_mono1[OF clel cp])
     then have ldcp:"0 < l div c" 
       by (simp add: zdiv_self[OF cnz])
-    have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+    have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
       by simp
     hence "(real l * real x + real (l div c) * Inum (real x # bs) e \<ge> (0\<Colon>real)) =
           (real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e \<ge> 0)"
       by simp

     from cp have cnz: "c \<noteq> 0" by simp
     have "c div c\<le> l div c"
       by (simp add: zdiv_mono1[OF clel cp])
     then have ldcp:"0 < l div c" 
       by (simp add: zdiv_self[OF cnz])
-    have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+    have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
       by simp
     hence "(real l * real x + real (l div c) * Inum (real x # bs) e = (0\<Colon>real)) =
           (real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e = 0)"
       by simp

     from cp have cnz: "c \<noteq> 0" by simp
     have "c div c\<le> l div c"
       by (simp add: zdiv_mono1[OF clel cp])
     then have ldcp:"0 < l div c" 
       by (simp add: zdiv_self[OF cnz])
-    have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+    have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
       by simp
     hence "(real l * real x + real (l div c) * Inum (real x # bs) e \<noteq> (0\<Colon>real)) =
           (real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e \<noteq> 0)"
       by simp

     from cp have cnz: "c \<noteq> 0" by simp
     have "c div c\<le> l div c"
       by (simp add: zdiv_mono1[OF clel cp])
     then have ldcp:"0 < l div c" 
       by (simp add: zdiv_self[OF cnz])
-    have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+    have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
       by simp
     hence "(\<exists> (k::int). real l * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k) = (\<exists> (k::int). real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k)"  by simp
     also have "\<dots> = (\<exists> (k::int). real (l div c) * (real c * real x + Inum (real x # bs) e - real j * real k) = real (l div c)*0)" by (simp add: algebra_simps)
     also fix k have "\<dots> = (\<exists> (k::int). real c * real x + Inum (real x # bs) e - real j * real k = 0)"

     from cp have cnz: "c \<noteq> 0" by simp
     have "c div c\<le> l div c"
       by (simp add: zdiv_mono1[OF clel cp])
     then have ldcp:"0 < l div c" 
       by (simp add: zdiv_self[OF cnz])
-    have "c * (l div c) = c* (l div c) + l mod c" using d' zdvd_iff_zmod_eq_0[where m="c" and n="l"] by simp
+    have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
       by simp
     hence "(\<exists> (k::int). real l * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k) = (\<exists> (k::int). real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k)"  by simp
     also have "\<dots> = (\<exists> (k::int). real (l div c) * (real c * real x + Inum (real x # bs) e - real j * real k) = real (l div c)*0)" by (simp add: algebra_simps)
     also fix k have "\<dots> = (\<exists> (k::int). real c * real x + Inum (real x # bs) e - real j * real k = 0)"

 
 lemma real_in_int_intervals: 
   assumes xb: "real m \<le> x \<and> x < real ((n::int) + 1)"
   shows "\<exists> j\<in> {m.. n}. real j \<le> x \<and> x < real (j+1)" (is "\<exists> j\<in> ?N. ?P j")
 by (rule bexI[where P="?P" and x="floor x" and A="?N"]) 
-(auto simp add: floor_less_eq[where x="x" and a="n+1", simplified] xb[simplified] floor_mono2[where x="real m" and y="x", OF conjunct1[OF xb], simplified floor_real_of_int[where n="m"]])
+(auto simp add: floor_less_eq[where x="x" and a="n+1", simplified] xb[simplified] floor_mono[where x="real m" and y="x", OF conjunct1[OF xb], simplified floor_real_of_int[where n="m"]])
 
 lemma rsplit0_complete:
   assumes xp:"0 \<le> x" and x1:"x < 1"
   shows "\<exists> (p,n,s) \<in> set (rsplit0 t). Ifm (x#bs) p" (is "\<exists> (p,n,s) \<in> ?SS t. ?I p")
 proof(induct t rule: rsplit0.induct)

 
 lemma "ALL (x::real). \<exists>y \<le> x. (\<lfloor>x\<rfloor> = \<lceil>y\<rceil>)"
 apply mir
 done
 
-lemma "ALL x y. \<lfloor>x\<rfloor> = \<lfloor>y\<rfloor> \<longrightarrow> 0 \<le> abs (y - x) \<and> abs (y - x) \<le> 1"
+lemma "ALL (x::real) (y::real). \<lfloor>x\<rfloor> = \<lfloor>y\<rfloor> \<longrightarrow> 0 \<le> abs (y - x) \<and> abs (y - x) \<le> 1"
 apply mir
 done
 
 end