src/HOL/Presburger.thy

 begin
 
 ML_file "Tools/Qelim/qelim.ML"
 ML_file "Tools/Qelim/cooper_procedure.ML"
 
-subsection\<open>The @{text "-\<infinity>"} and @{text "+\<infinity>"} Properties\<close>
+subsection\<open>The \<open>-\<infinity>\<close> and \<open>+\<infinity>\<close> Properties\<close>
 
 lemma minf:
   "\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x<z. P x = P' x; \<exists>z.\<forall>x<z. Q x = Q' x\<rbrakk> 
      \<Longrightarrow> \<exists>z.\<forall>x<z. (P x \<and> Q x) = (P' x \<and> Q' x)"
   "\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x<z. P x = P' x; \<exists>z.\<forall>x<z. Q x = Q' x\<rbrakk> 

   {fix x assume H: "\<not>(d dvd x + t)" with d have "\<not>d dvd (x + D) + t"
       by (clarsimp simp add: dvd_def,erule_tac x= "ka - k" in allE,simp add: algebra_simps)}
   thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (\<not>d dvd x+t) \<longrightarrow> (\<not>d dvd (x + D) + t)" by auto
 qed blast
 
-subsection\<open>Cooper's Theorem @{text "-\<infinity>"} and @{text "+\<infinity>"} Version\<close>
+subsection\<open>Cooper's Theorem \<open>-\<infinity>\<close> and \<open>+\<infinity>\<close> Version\<close>
 
 subsubsection\<open>First some trivial facts about periodic sets or predicates\<close>
 lemma periodic_finite_ex:
   assumes dpos: "(0::int) < d" and modd: "ALL x k. P x = P(x - k*d)"
   shows "(EX x. P x) = (EX j : {1..d}. P j)"

     qed
     ultimately show ?RHS ..
   qed
 qed auto
 
-subsubsection\<open>The @{text "-\<infinity>"} Version\<close>
+subsubsection\<open>The \<open>-\<infinity>\<close> Version\<close>
 
 lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (abs(x-z)+1) * d < z"
 by(induct rule: int_gr_induct,simp_all add:int_distrib)
 
 lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (abs(x-z)+1) * d"

    with periodic_finite_ex[OF dp pd]
    have "?R1" by blast}
  ultimately show ?thesis by blast
 qed
 
-subsubsection \<open>The @{text "+\<infinity>"} Version\<close>
+subsubsection \<open>The \<open>+\<infinity>\<close> Version\<close>
 
 lemma  plusinfinity:
   assumes dpos: "(0::int) < d" and
     P1eqP1: "\<forall>x k. P' x = P'(x - k*d)" and ePeqP1: "\<exists> z. \<forall> x>z. P x = P' x"
   shows "(\<exists> x. P' x) \<longrightarrow> (\<exists> x. P x)"

 lemma uminus_dvd_conv:
   fixes d t :: int
   shows "d dvd t \<equiv> - d dvd t" and "d dvd t \<equiv> d dvd - t"
   by simp_all
 
-text \<open>\bigskip Theorems for transforming predicates on nat to predicates on @{text int}\<close>
+text \<open>\bigskip Theorems for transforming predicates on nat to predicates on \<open>int\<close>\<close>
 
 lemma zdiff_int_split: "P (int (x - y)) =
   ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
   by (cases "y \<le> x") (simp_all add: zdiff_int)