src/HOL/Presburger.thy
 changeset 60758 d8d85a8172b5 parent 58925 1b655309617c child 61476 1884c40f1539
```     1.1 --- a/src/HOL/Presburger.thy	Sat Jul 18 21:44:18 2015 +0200
1.2 +++ b/src/HOL/Presburger.thy	Sat Jul 18 22:58:50 2015 +0200
1.3 @@ -2,7 +2,7 @@
1.4     Author:     Amine Chaieb, TU Muenchen
1.5  *)
1.6
1.7 -section {* Decision Procedure for Presburger Arithmetic *}
1.8 +section \<open>Decision Procedure for Presburger Arithmetic\<close>
1.9
1.10  theory Presburger
1.11  imports Groebner_Basis Set_Interval
1.12 @@ -12,7 +12,7 @@
1.13  ML_file "Tools/Qelim/qelim.ML"
1.14  ML_file "Tools/Qelim/cooper_procedure.ML"
1.15
1.16 -subsection{* The @{text "-\<infinity>"} and @{text "+\<infinity>"} Properties *}
1.17 +subsection\<open>The @{text "-\<infinity>"} and @{text "+\<infinity>"} Properties\<close>
1.18
1.19  lemma minf:
1.20    "\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x<z. P x = P' x; \<exists>z.\<forall>x<z. Q x = Q' x\<rbrakk>
1.21 @@ -59,7 +59,7 @@
1.22  unfolding dvd_def mult.commute [of d]
1.23  by auto
1.24
1.25 -subsection{* The A and B sets *}
1.26 +subsection\<open>The A and B sets\<close>
1.27  lemma bset:
1.28    "\<lbrakk>\<forall>x.(\<forall>j \<in> {1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> P x \<longrightarrow> P(x - D) ;
1.29       \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> Q x \<longrightarrow> Q(x - D)\<rbrakk> \<Longrightarrow>
1.30 @@ -176,9 +176,9 @@
1.31    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.32  qed blast
1.33
1.34 -subsection{* Cooper's Theorem @{text "-\<infinity>"} and @{text "+\<infinity>"} Version *}
1.35 +subsection\<open>Cooper's Theorem @{text "-\<infinity>"} and @{text "+\<infinity>"} Version\<close>
1.36
1.37 -subsubsection{* First some trivial facts about periodic sets or predicates *}
1.38 +subsubsection\<open>First some trivial facts about periodic sets or predicates\<close>
1.39  lemma periodic_finite_ex:
1.40    assumes dpos: "(0::int) < d" and modd: "ALL x k. P x = P(x - k*d)"
1.41    shows "(EX x. P x) = (EX j : {1..d}. P j)"
1.42 @@ -209,7 +209,7 @@
1.43    qed
1.44  qed auto
1.45
1.46 -subsubsection{* The @{text "-\<infinity>"} Version*}
1.47 +subsubsection\<open>The @{text "-\<infinity>"} Version\<close>
1.48
1.49  lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (abs(x-z)+1) * d < z"
1.51 @@ -277,7 +277,7 @@
1.52   ultimately show ?thesis by blast
1.53  qed
1.54
1.55 -subsubsection {* The @{text "+\<infinity>"} Version*}
1.56 +subsubsection \<open>The @{text "+\<infinity>"} Version\<close>
1.57
1.58  lemma  plusinfinity:
1.59    assumes dpos: "(0::int) < d" and
1.60 @@ -372,15 +372,15 @@
1.61    shows "d dvd t \<equiv> - d dvd t" and "d dvd t \<equiv> d dvd - t"
1.62    by simp_all
1.63
1.64 -text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*}
1.65 +text \<open>\bigskip Theorems for transforming predicates on nat to predicates on @{text int}\<close>
1.66
1.67  lemma zdiff_int_split: "P (int (x - y)) =
1.68    ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
1.69    by (cases "y \<le> x") (simp_all add: zdiff_int)
1.70
1.71 -text {*
1.72 +text \<open>
1.73    \medskip Specific instances of congruence rules, to prevent
1.74 -  simplifier from looping. *}
1.75 +  simplifier from looping.\<close>
1.76
1.77  theorem imp_le_cong:
1.78    "\<lbrakk>x = x'; 0 \<le> x' \<Longrightarrow> P = P'\<rbrakk> \<Longrightarrow> (0 \<le> (x::int) \<longrightarrow> P) = (0 \<le> x' \<longrightarrow> P')"
1.79 @@ -392,7 +392,7 @@
1.80
1.81  ML_file "Tools/Qelim/cooper.ML"
1.82
1.83 -method_setup presburger = {*
1.84 +method_setup presburger = \<open>
1.85    let
1.86      fun keyword k = Scan.lift (Args.\$\$\$ k -- Args.colon) >> K ()
1.87      fun simple_keyword k = Scan.lift (Args.\$\$\$ k) >> K ()
1.88 @@ -408,7 +408,7 @@
1.89      (fn ((elim, add_ths), del_ths) => fn ctxt =>
1.90        SIMPLE_METHOD' (Cooper.tac elim add_ths del_ths ctxt))
1.91    end
1.92 -*} "Cooper's algorithm for Presburger arithmetic"
1.93 +\<close> "Cooper's algorithm for Presburger arithmetic"
1.94
1.95  declare dvd_eq_mod_eq_0 [symmetric, presburger]
1.96  declare mod_1 [presburger]
1.97 @@ -490,7 +490,7 @@
1.98    using even_int_iff [of n] by simp
1.99
1.100
1.101 -subsection {* Nice facts about division by @{term 4} *}
1.102 +subsection \<open>Nice facts about division by @{term 4}\<close>
1.103
1.104  lemma even_even_mod_4_iff:
1.105    "even (n::nat) \<longleftrightarrow> even (n mod 4)"
1.106 @@ -505,7 +505,7 @@
1.107    by presburger
1.108
1.109
1.110 -subsection {* Try0 *}
1.111 +subsection \<open>Try0\<close>
1.112
1.113  ML_file "Tools/try0.ML"
1.114
```