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.50  by(induct rule: int_gr_induct,simp_all add:int_distrib)
    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