src/HOL/Integ/Presburger.thy
changeset 14577 dbb95b825244
parent 14485 ea2707645af8
child 14738 83f1a514dcb4
     1.1 --- a/src/HOL/Integ/Presburger.thy	Fri Apr 16 04:06:52 2004 +0200
     1.2 +++ b/src/HOL/Integ/Presburger.thy	Fri Apr 16 04:07:10 2004 +0200
     1.3 @@ -7,6 +7,8 @@
     1.4  generation for Cooper Algorithm  
     1.5  *)
     1.6  
     1.7 +header {* Presburger Arithmetic: Cooper Algorithm *}
     1.8 +
     1.9  theory Presburger = NatSimprocs + SetInterval
    1.10  files
    1.11    ("cooper_dec.ML")
    1.12 @@ -14,7 +16,7 @@
    1.13    ("qelim.ML")
    1.14    ("presburger.ML"):
    1.15  
    1.16 -(* Theorem for unitifying the coeffitients of x in an existential formula*)
    1.17 +text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*}
    1.18  
    1.19  theorem unity_coeff_ex: "(\<exists>x::int. P (l * x)) = (\<exists>x. l dvd (1*x+0) \<and> P x)"
    1.20    apply (rule iffI)
    1.21 @@ -54,7 +56,7 @@
    1.22  
    1.23  
    1.24  
    1.25 -(*Theorems for the combination of proofs of the equality of P and P_m for integers x less than some integer z.*)
    1.26 +text {*Theorems for the combination of proofs of the equality of @{text P} and @{text P_m} for integers @{text x} less than some integer @{text z}.*}
    1.27  
    1.28  theorem eq_minf_conjI: "\<exists>z1::int. \<forall>x. x < z1 \<longrightarrow> (A1 x = A2 x) \<Longrightarrow>
    1.29    \<exists>z2::int. \<forall>x. x < z2 \<longrightarrow> (B1 x = B2 x) \<Longrightarrow>
    1.30 @@ -75,7 +77,7 @@
    1.31    done
    1.32  
    1.33  
    1.34 -(*Theorems for the combination of proofs of the equality of P and P_m for integers x greather than some integer z.*)
    1.35 +text {*Theorems for the combination of proofs of the equality of @{text P} and @{text P_m} for integers @{text x} greather than some integer @{text z}.*}
    1.36  
    1.37  theorem eq_pinf_conjI: "\<exists>z1::int. \<forall>x. z1 < x \<longrightarrow> (A1 x = A2 x) \<Longrightarrow>
    1.38    \<exists>z2::int. \<forall>x. z2 < x \<longrightarrow> (B1 x = B2 x) \<Longrightarrow>
    1.39 @@ -93,75 +95,76 @@
    1.40    apply (rule_tac x = "max z1 z2" in exI)
    1.41    apply simp
    1.42    done
    1.43 -(*=============================================================================*)
    1.44 -(*Theorems for the combination of proofs of the modulo D property for P
    1.45 -pluusinfinity*)
    1.46 -(* FIXME : This is THE SAME theorem as for the minusinf version, but with +k.. instead of -k.. In the future replace these both with only one*)
    1.47 +
    1.48 +text {*
    1.49 +  \medskip Theorems for the combination of proofs of the modulo @{text
    1.50 +  D} property for @{text "P plusinfinity"}
    1.51 +
    1.52 +  FIXME: This is THE SAME theorem as for the @{text minusinf} version,
    1.53 +  but with @{text "+k.."} instead of @{text "-k.."} In the future
    1.54 +  replace these both with only one. *}
    1.55  
    1.56  theorem modd_pinf_conjI: "\<forall>(x::int) k. A x = A (x+k*d) \<Longrightarrow>
    1.57    \<forall>(x::int) k. B x = B (x+k*d) \<Longrightarrow>
    1.58    \<forall>(x::int) (k::int). (A x \<and> B x) = (A (x+k*d) \<and> B (x+k*d))"
    1.59    by simp
    1.60  
    1.61 -
    1.62  theorem modd_pinf_disjI: "\<forall>(x::int) k. A x = A (x+k*d) \<Longrightarrow>
    1.63    \<forall>(x::int) k. B x = B (x+k*d) \<Longrightarrow>
    1.64    \<forall>(x::int) (k::int). (A x \<or> B x) = (A (x+k*d) \<or> B (x+k*d))"
    1.65    by simp
    1.66  
    1.67 -(*=============================================================================*)
    1.68 -(*This is one of the cases where the simplifed formula is prooved to habe some property
    1.69 -(in relation to P_m) but we need to proove the property for the original formula (P_m)*)
    1.70 -(*FIXME : This is exaclty the same thm as for minusinf.*)
    1.71 +text {*
    1.72 +  This is one of the cases where the simplifed formula is prooved to
    1.73 +  habe some property (in relation to @{text P_m}) but we need to prove
    1.74 +  the property for the original formula (@{text P_m})
    1.75 +
    1.76 +  FIXME: This is exaclty the same thm as for @{text minusinf}. *}
    1.77 +
    1.78  lemma pinf_simp_eq: "ALL x. P(x) = Q(x) ==> (EX (x::int). P(x)) --> (EX (x::int). F(x))  ==> (EX (x::int). Q(x)) --> (EX (x::int). F(x)) "
    1.79 -by blast
    1.80 +  by blast
    1.81  
    1.82  
    1.83 -
    1.84 -(*=============================================================================*)
    1.85 -(*Theorems for the combination of proofs of the modulo D property for P
    1.86 -minusinfinity*)
    1.87 +text {*
    1.88 +  \medskip Theorems for the combination of proofs of the modulo @{text D}
    1.89 +  property for @{text "P minusinfinity"} *}
    1.90  
    1.91  theorem modd_minf_conjI: "\<forall>(x::int) k. A x = A (x-k*d) \<Longrightarrow>
    1.92    \<forall>(x::int) k. B x = B (x-k*d) \<Longrightarrow>
    1.93    \<forall>(x::int) (k::int). (A x \<and> B x) = (A (x-k*d) \<and> B (x-k*d))"
    1.94    by simp
    1.95  
    1.96 -
    1.97  theorem modd_minf_disjI: "\<forall>(x::int) k. A x = A (x-k*d) \<Longrightarrow>
    1.98    \<forall>(x::int) k. B x = B (x-k*d) \<Longrightarrow>
    1.99    \<forall>(x::int) (k::int). (A x \<or> B x) = (A (x-k*d) \<or> B (x-k*d))"
   1.100    by simp
   1.101  
   1.102 -(*=============================================================================*)
   1.103 -(*This is one of the cases where the simplifed formula is prooved to habe some property
   1.104 -(in relation to P_m) but we need to proove the property for the original formula (P_m)*)
   1.105 +text {*
   1.106 +  This is one of the cases where the simplifed formula is prooved to
   1.107 +  have some property (in relation to @{text P_m}) but we need to
   1.108 +  prove the property for the original formula (@{text P_m}). *}
   1.109  
   1.110  lemma minf_simp_eq: "ALL x. P(x) = Q(x) ==> (EX (x::int). P(x)) --> (EX (x::int). F(x))  ==> (EX (x::int). Q(x)) --> (EX (x::int). F(x)) "
   1.111 -by blast
   1.112 +  by blast
   1.113  
   1.114 -(*=============================================================================*)
   1.115 -
   1.116 -(*theorem needed for prooving at runtime divide properties using the arithmetic tatic
   1.117 -(who knows only about modulo = 0)*)
   1.118 +text {*
   1.119 +  Theorem needed for proving at runtime divide properties using the
   1.120 +  arithmetic tactic (which knows only about modulo = 0). *}
   1.121  
   1.122  lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
   1.123 -by(simp add:dvd_def zmod_eq_0_iff)
   1.124 -
   1.125 -(*=============================================================================*)
   1.126 +  by(simp add:dvd_def zmod_eq_0_iff)
   1.127  
   1.128 -
   1.129 -
   1.130 -(*Theorems used for the combination of proof for the backwards direction of cooper's
   1.131 -theorem. they rely exclusively on Predicate calculus.*)
   1.132 +text {*
   1.133 +  \medskip Theorems used for the combination of proof for the
   1.134 +  backwards direction of Cooper's Theorem. They rely exclusively on
   1.135 +  Predicate calculus.*}
   1.136  
   1.137  lemma not_ast_p_disjI: "(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> P1(x) --> P1(x + d))
   1.138  ==>
   1.139  (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> P2(x) --> P2(x + d))
   1.140  ==>
   1.141  (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) -->(P1(x) \<or> P2(x)) --> (P1(x + d) \<or> P2(x + d))) "
   1.142 -by blast
   1.143 -
   1.144 +  by blast
   1.145  
   1.146  
   1.147  lemma not_ast_p_conjI: "(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a- j)) --> P1(x) --> P1(x + d))
   1.148 @@ -170,18 +173,18 @@
   1.149  ==>
   1.150  (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) -->(P1(x) \<and> P2(x)) --> (P1(x + d)
   1.151  \<and> P2(x + d))) "
   1.152 -by blast
   1.153 +  by blast
   1.154  
   1.155  lemma not_ast_p_Q_elim: "
   1.156  (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) -->P(x) --> P(x + d))
   1.157  ==> ( P = Q )
   1.158  ==> (ALL x. ~(EX (j::int) : {1..d}. EX (a::int) : A. P(a - j)) -->P(x) --> P(x + d))"
   1.159 -by blast
   1.160 -(*=============================================================================*)
   1.161 +  by blast
   1.162  
   1.163 -
   1.164 -(*Theorems used for the combination of proof for the backwards direction of cooper's
   1.165 -theorem. they rely exclusively on Predicate calculus.*)
   1.166 +text {*
   1.167 +  \medskip Theorems used for the combination of proof for the
   1.168 +  backwards direction of Cooper's Theorem. They rely exclusively on
   1.169 +  Predicate calculus.*}
   1.170  
   1.171  lemma not_bst_p_disjI: "(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> P1(x) --> P1(x - d))
   1.172  ==>
   1.173 @@ -189,9 +192,7 @@
   1.174  ==>
   1.175  (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) -->(P1(x) \<or> P2(x)) --> (P1(x - d)
   1.176  \<or> P2(x-d))) "
   1.177 -by blast
   1.178 -
   1.179 -
   1.180 +  by blast
   1.181  
   1.182  lemma not_bst_p_conjI: "(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> P1(x) --> P1(x - d))
   1.183  ==>
   1.184 @@ -199,68 +200,67 @@
   1.185  ==>
   1.186  (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) -->(P1(x) \<and> P2(x)) --> (P1(x - d)
   1.187  \<and> P2(x-d))) "
   1.188 -by blast
   1.189 +  by blast
   1.190  
   1.191  lemma not_bst_p_Q_elim: "
   1.192  (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) -->P(x) --> P(x - d)) 
   1.193  ==> ( P = Q )
   1.194  ==> (ALL x. ~(EX (j::int) : {1..d}. EX (b::int) : B. P(b+j)) -->P(x) --> P(x - d))"
   1.195 -by blast
   1.196 -(*=============================================================================*)
   1.197 +  by blast
   1.198  
   1.199 -(*This is the first direction of cooper's theorem*)
   1.200 +text {* \medskip This is the first direction of Cooper's Theorem. *}
   1.201  lemma cooper_thm: "(R --> (EX x::int. P x))  ==> (Q -->(EX x::int.  P x )) ==> ((R|Q) --> (EX x::int. P x )) "
   1.202 -by blast
   1.203 +  by blast
   1.204  
   1.205 -(*=============================================================================*)
   1.206 -(*The full cooper's theoorem in its equivalence Form- Given the premisses it is trivial
   1.207 -too, it relies exclusively on prediacte calculus.*)
   1.208 +text {*
   1.209 +  \medskip The full Cooper's Theorem in its equivalence Form. Given
   1.210 +  the premises it is trivial too, it relies exclusively on prediacte calculus.*}
   1.211  lemma cooper_eq_thm: "(R --> (EX x::int. P x))  ==> (Q -->(EX x::int.  P x )) ==> ((~Q)
   1.212  --> (EX x::int. P x ) --> R) ==> (EX x::int. P x) = R|Q "
   1.213 -by blast
   1.214 +  by blast
   1.215  
   1.216 -(*=============================================================================*)
   1.217 -(*Some of the atomic theorems generated each time the atom does not depend on x, they
   1.218 -are trivial.*)
   1.219 +text {*
   1.220 +  \medskip Some of the atomic theorems generated each time the atom
   1.221 +  does not depend on @{text x}, they are trivial.*}
   1.222  
   1.223  lemma  fm_eq_minf: "EX z::int. ALL x. x < z --> (P = P) "
   1.224 -by blast
   1.225 +  by blast
   1.226  
   1.227  lemma  fm_modd_minf: "ALL (x::int). ALL (k::int). (P = P)"
   1.228 -by blast
   1.229 +  by blast
   1.230  
   1.231  lemma not_bst_p_fm: "ALL (x::int). Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> fm --> fm"
   1.232 -by blast
   1.233 -
   1.234 -
   1.235 +  by blast
   1.236  
   1.237  lemma  fm_eq_pinf: "EX z::int. ALL x. z < x --> (P = P) "
   1.238 -by blast
   1.239 +  by blast
   1.240  
   1.241 -(* The next 2 thms are the same as the minusinf version*)
   1.242 +text {* The next two thms are the same as the @{text minusinf} version. *}
   1.243 +
   1.244  lemma  fm_modd_pinf: "ALL (x::int). ALL (k::int). (P = P)"
   1.245 -by blast
   1.246 +  by blast
   1.247  
   1.248  lemma not_ast_p_fm: "ALL (x::int). Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> fm --> fm"
   1.249 -by blast
   1.250 +  by blast
   1.251  
   1.252 +text {* Theorems to be deleted from simpset when proving simplified formulaes. *}
   1.253  
   1.254 -(* Theorems to be deleted from simpset when proving simplified formulaes*)
   1.255  lemma P_eqtrue: "(P=True) = P"
   1.256    by rules
   1.257  
   1.258  lemma P_eqfalse: "(P=False) = (~P)"
   1.259    by rules
   1.260  
   1.261 -(*=============================================================================*)
   1.262 +text {*
   1.263 +  \medskip Theorems for the generation of the bachwards direction of
   1.264 +  Cooper's Theorem.
   1.265  
   1.266 -(*Theorems for the generation of the bachwards direction of cooper's theorem*)
   1.267 -(*These are the 6 interesting atomic cases which have to be proved relying on the
   1.268 -properties of B-set ant the arithmetic and contradiction proofs*)
   1.269 +  These are the 6 interesting atomic cases which have to be proved relying on the
   1.270 +  properties of B-set and the arithmetic and contradiction proofs. *}
   1.271  
   1.272  lemma not_bst_p_lt: "0 < (d::int) ==>
   1.273   ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> ( 0 < -x + a) --> (0 < -(x - d) + a )"
   1.274 -by arith
   1.275 +  by arith
   1.276  
   1.277  lemma not_bst_p_gt: "\<lbrakk> (g::int) \<in> B; g = -a \<rbrakk> \<Longrightarrow>
   1.278   ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> (0 < (x) + a) --> ( 0 < (x - d) + a)"
   1.279 @@ -315,16 +315,17 @@
   1.280  apply(simp add:int_distrib)
   1.281  done
   1.282  
   1.283 -
   1.284 +text {*
   1.285 +  \medskip Theorems for the generation of the bachwards direction of
   1.286 +  Cooper's Theorem.
   1.287  
   1.288 -(*Theorems for the generation of the bachwards direction of cooper's theorem*)
   1.289 -(*These are the 6 interesting atomic cases which have to be proved relying on the
   1.290 -properties of A-set ant the arithmetic and contradiction proofs*)
   1.291 +  These are the 6 interesting atomic cases which have to be proved
   1.292 +  relying on the properties of A-set ant the arithmetic and
   1.293 +  contradiction proofs. *}
   1.294  
   1.295  lemma not_ast_p_gt: "0 < (d::int) ==>
   1.296   ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> ( 0 < x + t) --> (0 < (x + d) + t )"
   1.297 -by arith
   1.298 -
   1.299 +  by arith
   1.300  
   1.301  lemma not_ast_p_lt: "\<lbrakk>0 < d ;(t::int) \<in> A \<rbrakk> \<Longrightarrow>
   1.302   ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> (0 < -x + t) --> ( 0 < -(x + d) + t)"
   1.303 @@ -377,12 +378,11 @@
   1.304    apply(simp add:int_distrib)
   1.305    done
   1.306  
   1.307 -
   1.308 +text {*
   1.309 +  \medskip These are the atomic cases for the proof generation for the
   1.310 +  modulo @{text D} property for @{text "P plusinfinity"}
   1.311  
   1.312 -(*=============================================================================*)
   1.313 -(*These are the atomic cases for the proof generation for the modulo D property for P
   1.314 -plusinfinity*)
   1.315 -(*They are fully based on arithmetics*)
   1.316 +  They are fully based on arithmetics. *}
   1.317  
   1.318  lemma  dvd_modd_pinf: "((d::int) dvd d1) ==>
   1.319   (ALL (x::int). ALL (k::int). (((d::int) dvd (x + t)) = (d dvd (x+k*d1 + t))))"
   1.320 @@ -412,10 +412,12 @@
   1.321    apply(simp add:int_distrib mult_ac)
   1.322    done
   1.323  
   1.324 -(*=============================================================================*)
   1.325 -(*These are the atomic cases for the proof generation for the equivalence of P and P
   1.326 -plusinfinity for integers x greather than some integer z.*)
   1.327 -(*They are fully based on arithmetics*)
   1.328 +text {*
   1.329 +  \medskip These are the atomic cases for the proof generation for the
   1.330 +  equivalence of @{text P} and @{text "P plusinfinity"} for integers
   1.331 +  @{text x} greater than some integer @{text z}.
   1.332 +
   1.333 +  They are fully based on arithmetics. *}
   1.334  
   1.335  lemma  eq_eq_pinf: "EX z::int. ALL x. z < x --> (( 0 = x +t ) = False )"
   1.336    apply(rule_tac x = "-t" in exI)
   1.337 @@ -438,18 +440,16 @@
   1.338    done
   1.339  
   1.340  lemma  dvd_eq_pinf: "EX z::int. ALL x.  z < x --> ((d dvd (x + t)) = (d dvd (x + t))) "
   1.341 -by simp
   1.342 +  by simp
   1.343  
   1.344  lemma  not_dvd_eq_pinf: "EX z::int. ALL x. z < x  --> ((~(d dvd (x + t))) = (~(d dvd (x + t)))) "
   1.345 -by simp
   1.346 -
   1.347 -
   1.348 -
   1.349 +  by simp
   1.350  
   1.351 -(*=============================================================================*)
   1.352 -(*These are the atomic cases for the proof generation for the modulo D property for P
   1.353 -minusinfinity*)
   1.354 -(*They are fully based on arithmetics*)
   1.355 +text {*
   1.356 +  \medskip These are the atomic cases for the proof generation for the
   1.357 +  modulo @{text D} property for @{text "P minusinfinity"}.
   1.358 +
   1.359 +  They are fully based on arithmetics. *}
   1.360  
   1.361  lemma  dvd_modd_minf: "((d::int) dvd d1) ==>
   1.362   (ALL (x::int). ALL (k::int). (((d::int) dvd (x + t)) = (d dvd (x-k*d1 + t))))"
   1.363 @@ -480,11 +480,12 @@
   1.364  apply(simp add:int_distrib mult_ac)
   1.365  done
   1.366  
   1.367 +text {*
   1.368 +  \medskip These are the atomic cases for the proof generation for the
   1.369 +  equivalence of @{text P} and @{text "P minusinfinity"} for integers
   1.370 +  @{text x} less than some integer @{text z}.
   1.371  
   1.372 -(*=============================================================================*)
   1.373 -(*These are the atomic cases for the proof generation for the equivalence of P and P
   1.374 -minusinfinity for integers x less than some integer z.*)
   1.375 -(*They are fully based on arithmetics*)
   1.376 +  They are fully based on arithmetics. *}
   1.377  
   1.378  lemma  eq_eq_minf: "EX z::int. ALL x. x < z --> (( 0 = x +t ) = False )"
   1.379  apply(rule_tac x = "-t" in exI)
   1.380 @@ -508,17 +509,18 @@
   1.381  done
   1.382  
   1.383  lemma  dvd_eq_minf: "EX z::int. ALL x. x < z --> ((d dvd (x + t)) = (d dvd (x + t))) "
   1.384 -by simp
   1.385 +  by simp
   1.386  
   1.387  lemma  not_dvd_eq_minf: "EX z::int. ALL x. x < z --> ((~(d dvd (x + t))) = (~(d dvd (x + t)))) "
   1.388 -by simp
   1.389 -
   1.390 +  by simp
   1.391  
   1.392 -(*=============================================================================*)
   1.393 -(*This Theorem combines whithnesses about P minusinfinity to schow one component of the
   1.394 -equivalence proof for cooper's theorem*)
   1.395 +text {*
   1.396 +  \medskip This Theorem combines whithnesses about @{text "P
   1.397 +  minusinfinity"} to show one component of the equivalence proof for
   1.398 +  Cooper's Theorem.
   1.399  
   1.400 -(* FIXME: remove once they are part of the distribution *)
   1.401 +  FIXME: remove once they are part of the distribution. *}
   1.402 +
   1.403  theorem int_ge_induct[consumes 1,case_names base step]:
   1.404    assumes ge: "k \<le> (i::int)" and
   1.405          base: "P(k)" and
   1.406 @@ -590,9 +592,10 @@
   1.407    qed
   1.408  qed
   1.409  
   1.410 -(*=============================================================================*)
   1.411 -(*This Theorem combines whithnesses about P minusinfinity to schow one component of the
   1.412 -equivalence proof for cooper's theorem*)
   1.413 +text {*
   1.414 +  \medskip This Theorem combines whithnesses about @{text "P
   1.415 +  minusinfinity"} to show one component of the equivalence proof for
   1.416 +  Cooper's Theorem. *}
   1.417  
   1.418  lemma plusinfinity:
   1.419    assumes "0 < d" and
   1.420 @@ -613,10 +616,8 @@
   1.421    qed
   1.422  qed
   1.423   
   1.424 -
   1.425 -
   1.426 -(*=============================================================================*)
   1.427 -(*Theorem for periodic function on discrete sets*)
   1.428 +text {*
   1.429 +  \medskip Theorem for periodic function on discrete sets. *}
   1.430  
   1.431  lemma minf_vee:
   1.432    assumes dpos: "(0::int) < d" and modd: "ALL x k. P x = P(x - k*d)"
   1.433 @@ -651,8 +652,9 @@
   1.434    assume ?RHS thus ?LHS by blast
   1.435  qed
   1.436  
   1.437 -(*=============================================================================*)
   1.438 -(*Theorem for periodic function on discrete sets*)
   1.439 +text {*
   1.440 +  \medskip Theorem for periodic function on discrete sets. *}
   1.441 +
   1.442  lemma pinf_vee:
   1.443    assumes dpos: "0 < (d::int)" and modd: "ALL (x::int) (k::int). P x = P (x+k*d)"
   1.444    shows "(EX x::int. P x) = (EX (j::int) : {1..d} . P j)"
   1.445 @@ -750,7 +752,7 @@
   1.446  apply(blast dest:decr_mult_lemma)
   1.447  done
   1.448  
   1.449 -(* Cooper Thm `, plus infinity version*)
   1.450 +text {* Cooper Theorem, plus infinity version. *}
   1.451  lemma cppi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. z < x --> (P x = P1 x))
   1.452  ==> ALL x.~(EX (j::int) : {1..D}. EX (a::int) : A. P(a - j)) --> P (x) --> P (x + D) 
   1.453  ==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x+k*D))))
   1.454 @@ -774,9 +776,8 @@
   1.455    done
   1.456  
   1.457  
   1.458 -(*=============================================================================*)
   1.459 -
   1.460 -(*Theorems for the quantifier elminination Functions.*)
   1.461 +text {*
   1.462 +  \bigskip Theorems for the quantifier elminination Functions. *}
   1.463  
   1.464  lemma qe_ex_conj: "(EX (x::int). A x) = R
   1.465  		==> (EX (x::int). P x) = (Q & (EX x::int. A x))
   1.466 @@ -805,7 +806,7 @@
   1.467  lemma qe_ALL: "(EX x. ~P x) = R ==> (ALL x. P x) = (~R)"
   1.468  by blast
   1.469  
   1.470 -(* Theorems for proving NNF *)
   1.471 +text {* \bigskip Theorems for proving NNF *}
   1.472  
   1.473  lemma nnf_im: "((~P) = P1) ==> (Q=Q1) ==> ((P --> Q) = (P1 | Q1))"
   1.474  by blast
   1.475 @@ -851,7 +852,7 @@
   1.476  apply(fastsimp)
   1.477  done
   1.478  
   1.479 -(* Theorems required for the adjustcoeffitienteq*)
   1.480 +text {* \bigskip Theorems required for the @{text adjustcoeffitienteq} *}
   1.481  
   1.482  lemma ac_dvd_eq: assumes not0: "0 ~= (k::int)"
   1.483  shows "((m::int) dvd (c*n+t)) = (k*m dvd ((k*c)*n+(k*t)))" (is "?P = ?Q")
   1.484 @@ -925,7 +926,7 @@
   1.485  lemma lf_dvd: "(l::int) = ll ==> (r::int) = lr ==> (l dvd r) =(ll dvd lr)"
   1.486  by simp
   1.487  
   1.488 -(* Theorems for transforming predicates on nat to predicates on int*)
   1.489 +text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*}
   1.490  
   1.491  theorem all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))"
   1.492    by (simp split add: split_nat)
   1.493 @@ -973,7 +974,9 @@
   1.494  
   1.495  theorem Suc_plus1: "Suc n = n + 1" by simp
   1.496  
   1.497 -(* specific instances of congruence rules, to prevent simplifier from looping *)
   1.498 +text {*
   1.499 +  \medskip Specific instances of congruence rules, to prevent
   1.500 +  simplifier from looping. *}
   1.501  
   1.502  theorem imp_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::nat) \<longrightarrow> P) = (0 <= x \<longrightarrow> P')"
   1.503    by simp