src/HOL/Presburger.thy
changeset 61799 4cf66f21b764
parent 61476 1884c40f1539
child 61944 5d06ecfdb472
     1.1 --- a/src/HOL/Presburger.thy	Mon Dec 07 10:23:50 2015 +0100
     1.2 +++ b/src/HOL/Presburger.thy	Mon Dec 07 10:38:04 2015 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4  ML_file "Tools/Qelim/qelim.ML"
     1.5  ML_file "Tools/Qelim/cooper_procedure.ML"
     1.6  
     1.7 -subsection\<open>The @{text "-\<infinity>"} and @{text "+\<infinity>"} Properties\<close>
     1.8 +subsection\<open>The \<open>-\<infinity>\<close> and \<open>+\<infinity>\<close> Properties\<close>
     1.9  
    1.10  lemma minf:
    1.11    "\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x<z. P x = P' x; \<exists>z.\<forall>x<z. Q x = Q' x\<rbrakk> 
    1.12 @@ -176,7 +176,7 @@
    1.13    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
    1.14  qed blast
    1.15  
    1.16 -subsection\<open>Cooper's Theorem @{text "-\<infinity>"} and @{text "+\<infinity>"} Version\<close>
    1.17 +subsection\<open>Cooper's Theorem \<open>-\<infinity>\<close> and \<open>+\<infinity>\<close> Version\<close>
    1.18  
    1.19  subsubsection\<open>First some trivial facts about periodic sets or predicates\<close>
    1.20  lemma periodic_finite_ex:
    1.21 @@ -209,7 +209,7 @@
    1.22    qed
    1.23  qed auto
    1.24  
    1.25 -subsubsection\<open>The @{text "-\<infinity>"} Version\<close>
    1.26 +subsubsection\<open>The \<open>-\<infinity>\<close> Version\<close>
    1.27  
    1.28  lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (abs(x-z)+1) * d < z"
    1.29  by(induct rule: int_gr_induct,simp_all add:int_distrib)
    1.30 @@ -277,7 +277,7 @@
    1.31   ultimately show ?thesis by blast
    1.32  qed
    1.33  
    1.34 -subsubsection \<open>The @{text "+\<infinity>"} Version\<close>
    1.35 +subsubsection \<open>The \<open>+\<infinity>\<close> Version\<close>
    1.36  
    1.37  lemma  plusinfinity:
    1.38    assumes dpos: "(0::int) < d" and
    1.39 @@ -372,7 +372,7 @@
    1.40    shows "d dvd t \<equiv> - d dvd t" and "d dvd t \<equiv> d dvd - t"
    1.41    by simp_all
    1.42  
    1.43 -text \<open>\bigskip Theorems for transforming predicates on nat to predicates on @{text int}\<close>
    1.44 +text \<open>\bigskip Theorems for transforming predicates on nat to predicates on \<open>int\<close>\<close>
    1.45  
    1.46  lemma zdiff_int_split: "P (int (x - y)) =
    1.47    ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"