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.124 -
1.125 -(*=============================================================================*)
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.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.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.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.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.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
```