tuned document;
authorwenzelm
Fri Apr 16 04:07:10 2004 +0200 (2004-04-16)
changeset 14577dbb95b825244
parent 14576 37a92211a5d3
child 14578 1f3f7e58b195
tuned document;
src/HOL/Algebra/CRing.thy
src/HOL/Algebra/Lattice.thy
src/HOL/Algebra/Module.thy
src/HOL/Algebra/UnivPoly.thy
src/HOL/Integ/NatSimprocs.thy
src/HOL/Integ/Presburger.thy
src/HOL/Power.thy
src/HOL/PreList.thy
src/HOL/Presburger.thy
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/Algebra/CRing.thy	Fri Apr 16 04:06:52 2004 +0200
     1.2 +++ b/src/HOL/Algebra/CRing.thy	Fri Apr 16 04:07:10 2004 +0200
     1.3 @@ -5,11 +5,11 @@
     1.4    Copyright: Clemens Ballarin
     1.5  *)
     1.6  
     1.7 +header {* Abelian Groups *}
     1.8 +
     1.9  theory CRing = FiniteProduct
    1.10  files ("ringsimp.ML"):
    1.11  
    1.12 -section {* Abelian Groups *}
    1.13 -
    1.14  record 'a ring = "'a monoid" +
    1.15    zero :: 'a ("\<zero>\<index>")
    1.16    add :: "['a, 'a] => 'a" (infixl "\<oplus>\<index>" 65)
     2.1 --- a/src/HOL/Algebra/Lattice.thy	Fri Apr 16 04:06:52 2004 +0200
     2.2 +++ b/src/HOL/Algebra/Lattice.thy	Fri Apr 16 04:07:10 2004 +0200
     2.3 @@ -5,9 +5,9 @@
     2.4    Copyright: Clemens Ballarin
     2.5  *)
     2.6  
     2.7 -theory Lattice = Group:
     2.8 +header {* Order and Lattices *}
     2.9  
    2.10 -section {* Order and Lattices *}
    2.11 +theory Lattice = Group:
    2.12  
    2.13  subsection {* Partial Orders *}
    2.14  
     3.1 --- a/src/HOL/Algebra/Module.thy	Fri Apr 16 04:06:52 2004 +0200
     3.2 +++ b/src/HOL/Algebra/Module.thy	Fri Apr 16 04:07:10 2004 +0200
     3.3 @@ -4,9 +4,9 @@
     3.4      Copyright:  Clemens Ballarin
     3.5  *)
     3.6  
     3.7 -theory Module = CRing:
     3.8 +header {* Modules over an Abelian Group *}
     3.9  
    3.10 -section {* Modules over an Abelian Group *}
    3.11 +theory Module = CRing:
    3.12  
    3.13  record ('a, 'b) module = "'b ring" +
    3.14    smult :: "['a, 'b] => 'b" (infixl "\<odot>\<index>" 70)
     4.1 --- a/src/HOL/Algebra/UnivPoly.thy	Fri Apr 16 04:06:52 2004 +0200
     4.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Fri Apr 16 04:07:10 2004 +0200
     4.3 @@ -5,9 +5,9 @@
     4.4    Copyright: Clemens Ballarin
     4.5  *)
     4.6  
     4.7 -theory UnivPoly = Module:
     4.8 +header {* Univariate Polynomials *}
     4.9  
    4.10 -section {* Univariate Polynomials *}
    4.11 +theory UnivPoly = Module:
    4.12  
    4.13  text {*
    4.14    Polynomials are formalised as modules with additional operations for 
     5.1 --- a/src/HOL/Integ/NatSimprocs.thy	Fri Apr 16 04:06:52 2004 +0200
     5.2 +++ b/src/HOL/Integ/NatSimprocs.thy	Fri Apr 16 04:07:10 2004 +0200
     5.3 @@ -17,8 +17,9 @@
     5.4  lemma Suc_diff_eq_diff_pred: "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)"
     5.5  by (simp add: numeral_0_eq_0 numeral_1_eq_1 split add: nat_diff_split)
     5.6  
     5.7 -(*Now just instantiating n to (number_of v) does the right simplification,
     5.8 -  but with some redundant inequality tests.*)
     5.9 +text {*Now just instantiating @{text n} to @{text "number_of v"} does
    5.10 +  the right simplification, but with some redundant inequality
    5.11 +  tests.*}
    5.12  lemma neg_number_of_bin_pred_iff_0:
    5.13       "neg (number_of (bin_pred v)::int) = (number_of v = (0::nat))"
    5.14  apply (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < Suc 0) ")
    5.15 @@ -171,8 +172,9 @@
    5.16  declare zero_le_divide_iff [of "number_of w", standard, simp]
    5.17  declare divide_le_0_iff [of "number_of w", standard, simp]
    5.18  
    5.19 -(*Replaces "inverse #nn" by 1/#nn.  It looks strange, but then other simprocs
    5.20 -simplify the quotient.*)
    5.21 +text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}.  It looks
    5.22 +  strange, but then other simprocs simplify the quotient.*}
    5.23 +
    5.24  declare inverse_eq_divide [of "number_of w", standard, simp]
    5.25  
    5.26  text{*These laws simplify inequalities, moving unary minus from a term
    5.27 @@ -194,16 +196,14 @@
    5.28  declare minus_le_iff [of _ 1, simplified, simp]
    5.29  declare minus_equation_iff [of _ 1, simplified, simp]
    5.30  
    5.31 -
    5.32 -(*Cancellation of constant factors in comparisons (< and \<le>) *)
    5.33 +text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
    5.34  
    5.35  declare mult_less_cancel_left [of "number_of v", standard, simp]
    5.36  declare mult_less_cancel_right [of _ "number_of v", standard, simp]
    5.37  declare mult_le_cancel_left [of "number_of v", standard, simp]
    5.38  declare mult_le_cancel_right [of _ "number_of v", standard, simp]
    5.39  
    5.40 -
    5.41 -(*Multiplying out constant divisors in comparisons (< \<le> and =) *)
    5.42 +text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *}
    5.43  
    5.44  declare le_divide_eq [of _ _ "number_of w", standard, simp]
    5.45  declare divide_le_eq [of _ "number_of w", standard, simp]
     6.1 --- a/src/HOL/Integ/Presburger.thy	Fri Apr 16 04:06:52 2004 +0200
     6.2 +++ b/src/HOL/Integ/Presburger.thy	Fri Apr 16 04:07:10 2004 +0200
     6.3 @@ -7,6 +7,8 @@
     6.4  generation for Cooper Algorithm  
     6.5  *)
     6.6  
     6.7 +header {* Presburger Arithmetic: Cooper Algorithm *}
     6.8 +
     6.9  theory Presburger = NatSimprocs + SetInterval
    6.10  files
    6.11    ("cooper_dec.ML")
    6.12 @@ -14,7 +16,7 @@
    6.13    ("qelim.ML")
    6.14    ("presburger.ML"):
    6.15  
    6.16 -(* Theorem for unitifying the coeffitients of x in an existential formula*)
    6.17 +text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*}
    6.18  
    6.19  theorem unity_coeff_ex: "(\<exists>x::int. P (l * x)) = (\<exists>x. l dvd (1*x+0) \<and> P x)"
    6.20    apply (rule iffI)
    6.21 @@ -54,7 +56,7 @@
    6.22  
    6.23  
    6.24  
    6.25 -(*Theorems for the combination of proofs of the equality of P and P_m for integers x less than some integer z.*)
    6.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}.*}
    6.27  
    6.28  theorem eq_minf_conjI: "\<exists>z1::int. \<forall>x. x < z1 \<longrightarrow> (A1 x = A2 x) \<Longrightarrow>
    6.29    \<exists>z2::int. \<forall>x. x < z2 \<longrightarrow> (B1 x = B2 x) \<Longrightarrow>
    6.30 @@ -75,7 +77,7 @@
    6.31    done
    6.32  
    6.33  
    6.34 -(*Theorems for the combination of proofs of the equality of P and P_m for integers x greather than some integer z.*)
    6.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}.*}
    6.36  
    6.37  theorem eq_pinf_conjI: "\<exists>z1::int. \<forall>x. z1 < x \<longrightarrow> (A1 x = A2 x) \<Longrightarrow>
    6.38    \<exists>z2::int. \<forall>x. z2 < x \<longrightarrow> (B1 x = B2 x) \<Longrightarrow>
    6.39 @@ -93,75 +95,76 @@
    6.40    apply (rule_tac x = "max z1 z2" in exI)
    6.41    apply simp
    6.42    done
    6.43 -(*=============================================================================*)
    6.44 -(*Theorems for the combination of proofs of the modulo D property for P
    6.45 -pluusinfinity*)
    6.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*)
    6.47 +
    6.48 +text {*
    6.49 +  \medskip Theorems for the combination of proofs of the modulo @{text
    6.50 +  D} property for @{text "P plusinfinity"}
    6.51 +
    6.52 +  FIXME: This is THE SAME theorem as for the @{text minusinf} version,
    6.53 +  but with @{text "+k.."} instead of @{text "-k.."} In the future
    6.54 +  replace these both with only one. *}
    6.55  
    6.56  theorem modd_pinf_conjI: "\<forall>(x::int) k. A x = A (x+k*d) \<Longrightarrow>
    6.57    \<forall>(x::int) k. B x = B (x+k*d) \<Longrightarrow>
    6.58    \<forall>(x::int) (k::int). (A x \<and> B x) = (A (x+k*d) \<and> B (x+k*d))"
    6.59    by simp
    6.60  
    6.61 -
    6.62  theorem modd_pinf_disjI: "\<forall>(x::int) k. A x = A (x+k*d) \<Longrightarrow>
    6.63    \<forall>(x::int) k. B x = B (x+k*d) \<Longrightarrow>
    6.64    \<forall>(x::int) (k::int). (A x \<or> B x) = (A (x+k*d) \<or> B (x+k*d))"
    6.65    by simp
    6.66  
    6.67 -(*=============================================================================*)
    6.68 -(*This is one of the cases where the simplifed formula is prooved to habe some property
    6.69 -(in relation to P_m) but we need to proove the property for the original formula (P_m)*)
    6.70 -(*FIXME : This is exaclty the same thm as for minusinf.*)
    6.71 +text {*
    6.72 +  This is one of the cases where the simplifed formula is prooved to
    6.73 +  habe some property (in relation to @{text P_m}) but we need to prove
    6.74 +  the property for the original formula (@{text P_m})
    6.75 +
    6.76 +  FIXME: This is exaclty the same thm as for @{text minusinf}. *}
    6.77 +
    6.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)) "
    6.79 -by blast
    6.80 +  by blast
    6.81  
    6.82  
    6.83 -
    6.84 -(*=============================================================================*)
    6.85 -(*Theorems for the combination of proofs of the modulo D property for P
    6.86 -minusinfinity*)
    6.87 +text {*
    6.88 +  \medskip Theorems for the combination of proofs of the modulo @{text D}
    6.89 +  property for @{text "P minusinfinity"} *}
    6.90  
    6.91  theorem modd_minf_conjI: "\<forall>(x::int) k. A x = A (x-k*d) \<Longrightarrow>
    6.92    \<forall>(x::int) k. B x = B (x-k*d) \<Longrightarrow>
    6.93    \<forall>(x::int) (k::int). (A x \<and> B x) = (A (x-k*d) \<and> B (x-k*d))"
    6.94    by simp
    6.95  
    6.96 -
    6.97  theorem modd_minf_disjI: "\<forall>(x::int) k. A x = A (x-k*d) \<Longrightarrow>
    6.98    \<forall>(x::int) k. B x = B (x-k*d) \<Longrightarrow>
    6.99    \<forall>(x::int) (k::int). (A x \<or> B x) = (A (x-k*d) \<or> B (x-k*d))"
   6.100    by simp
   6.101  
   6.102 -(*=============================================================================*)
   6.103 -(*This is one of the cases where the simplifed formula is prooved to habe some property
   6.104 -(in relation to P_m) but we need to proove the property for the original formula (P_m)*)
   6.105 +text {*
   6.106 +  This is one of the cases where the simplifed formula is prooved to
   6.107 +  have some property (in relation to @{text P_m}) but we need to
   6.108 +  prove the property for the original formula (@{text P_m}). *}
   6.109  
   6.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)) "
   6.111 -by blast
   6.112 +  by blast
   6.113  
   6.114 -(*=============================================================================*)
   6.115 -
   6.116 -(*theorem needed for prooving at runtime divide properties using the arithmetic tatic
   6.117 -(who knows only about modulo = 0)*)
   6.118 +text {*
   6.119 +  Theorem needed for proving at runtime divide properties using the
   6.120 +  arithmetic tactic (which knows only about modulo = 0). *}
   6.121  
   6.122  lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
   6.123 -by(simp add:dvd_def zmod_eq_0_iff)
   6.124 -
   6.125 -(*=============================================================================*)
   6.126 +  by(simp add:dvd_def zmod_eq_0_iff)
   6.127  
   6.128 -
   6.129 -
   6.130 -(*Theorems used for the combination of proof for the backwards direction of cooper's
   6.131 -theorem. they rely exclusively on Predicate calculus.*)
   6.132 +text {*
   6.133 +  \medskip Theorems used for the combination of proof for the
   6.134 +  backwards direction of Cooper's Theorem. They rely exclusively on
   6.135 +  Predicate calculus.*}
   6.136  
   6.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))
   6.138  ==>
   6.139  (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> P2(x) --> P2(x + d))
   6.140  ==>
   6.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))) "
   6.142 -by blast
   6.143 -
   6.144 +  by blast
   6.145  
   6.146  
   6.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))
   6.148 @@ -170,18 +173,18 @@
   6.149  ==>
   6.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)
   6.151  \<and> P2(x + d))) "
   6.152 -by blast
   6.153 +  by blast
   6.154  
   6.155  lemma not_ast_p_Q_elim: "
   6.156  (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) -->P(x) --> P(x + d))
   6.157  ==> ( P = Q )
   6.158  ==> (ALL x. ~(EX (j::int) : {1..d}. EX (a::int) : A. P(a - j)) -->P(x) --> P(x + d))"
   6.159 -by blast
   6.160 -(*=============================================================================*)
   6.161 +  by blast
   6.162  
   6.163 -
   6.164 -(*Theorems used for the combination of proof for the backwards direction of cooper's
   6.165 -theorem. they rely exclusively on Predicate calculus.*)
   6.166 +text {*
   6.167 +  \medskip Theorems used for the combination of proof for the
   6.168 +  backwards direction of Cooper's Theorem. They rely exclusively on
   6.169 +  Predicate calculus.*}
   6.170  
   6.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))
   6.172  ==>
   6.173 @@ -189,9 +192,7 @@
   6.174  ==>
   6.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)
   6.176  \<or> P2(x-d))) "
   6.177 -by blast
   6.178 -
   6.179 -
   6.180 +  by blast
   6.181  
   6.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))
   6.183  ==>
   6.184 @@ -199,68 +200,67 @@
   6.185  ==>
   6.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)
   6.187  \<and> P2(x-d))) "
   6.188 -by blast
   6.189 +  by blast
   6.190  
   6.191  lemma not_bst_p_Q_elim: "
   6.192  (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) -->P(x) --> P(x - d)) 
   6.193  ==> ( P = Q )
   6.194  ==> (ALL x. ~(EX (j::int) : {1..d}. EX (b::int) : B. P(b+j)) -->P(x) --> P(x - d))"
   6.195 -by blast
   6.196 -(*=============================================================================*)
   6.197 +  by blast
   6.198  
   6.199 -(*This is the first direction of cooper's theorem*)
   6.200 +text {* \medskip This is the first direction of Cooper's Theorem. *}
   6.201  lemma cooper_thm: "(R --> (EX x::int. P x))  ==> (Q -->(EX x::int.  P x )) ==> ((R|Q) --> (EX x::int. P x )) "
   6.202 -by blast
   6.203 +  by blast
   6.204  
   6.205 -(*=============================================================================*)
   6.206 -(*The full cooper's theoorem in its equivalence Form- Given the premisses it is trivial
   6.207 -too, it relies exclusively on prediacte calculus.*)
   6.208 +text {*
   6.209 +  \medskip The full Cooper's Theorem in its equivalence Form. Given
   6.210 +  the premises it is trivial too, it relies exclusively on prediacte calculus.*}
   6.211  lemma cooper_eq_thm: "(R --> (EX x::int. P x))  ==> (Q -->(EX x::int.  P x )) ==> ((~Q)
   6.212  --> (EX x::int. P x ) --> R) ==> (EX x::int. P x) = R|Q "
   6.213 -by blast
   6.214 +  by blast
   6.215  
   6.216 -(*=============================================================================*)
   6.217 -(*Some of the atomic theorems generated each time the atom does not depend on x, they
   6.218 -are trivial.*)
   6.219 +text {*
   6.220 +  \medskip Some of the atomic theorems generated each time the atom
   6.221 +  does not depend on @{text x}, they are trivial.*}
   6.222  
   6.223  lemma  fm_eq_minf: "EX z::int. ALL x. x < z --> (P = P) "
   6.224 -by blast
   6.225 +  by blast
   6.226  
   6.227  lemma  fm_modd_minf: "ALL (x::int). ALL (k::int). (P = P)"
   6.228 -by blast
   6.229 +  by blast
   6.230  
   6.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"
   6.232 -by blast
   6.233 -
   6.234 -
   6.235 +  by blast
   6.236  
   6.237  lemma  fm_eq_pinf: "EX z::int. ALL x. z < x --> (P = P) "
   6.238 -by blast
   6.239 +  by blast
   6.240  
   6.241 -(* The next 2 thms are the same as the minusinf version*)
   6.242 +text {* The next two thms are the same as the @{text minusinf} version. *}
   6.243 +
   6.244  lemma  fm_modd_pinf: "ALL (x::int). ALL (k::int). (P = P)"
   6.245 -by blast
   6.246 +  by blast
   6.247  
   6.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"
   6.249 -by blast
   6.250 +  by blast
   6.251  
   6.252 +text {* Theorems to be deleted from simpset when proving simplified formulaes. *}
   6.253  
   6.254 -(* Theorems to be deleted from simpset when proving simplified formulaes*)
   6.255  lemma P_eqtrue: "(P=True) = P"
   6.256    by rules
   6.257  
   6.258  lemma P_eqfalse: "(P=False) = (~P)"
   6.259    by rules
   6.260  
   6.261 -(*=============================================================================*)
   6.262 +text {*
   6.263 +  \medskip Theorems for the generation of the bachwards direction of
   6.264 +  Cooper's Theorem.
   6.265  
   6.266 -(*Theorems for the generation of the bachwards direction of cooper's theorem*)
   6.267 -(*These are the 6 interesting atomic cases which have to be proved relying on the
   6.268 -properties of B-set ant the arithmetic and contradiction proofs*)
   6.269 +  These are the 6 interesting atomic cases which have to be proved relying on the
   6.270 +  properties of B-set and the arithmetic and contradiction proofs. *}
   6.271  
   6.272  lemma not_bst_p_lt: "0 < (d::int) ==>
   6.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 )"
   6.274 -by arith
   6.275 +  by arith
   6.276  
   6.277  lemma not_bst_p_gt: "\<lbrakk> (g::int) \<in> B; g = -a \<rbrakk> \<Longrightarrow>
   6.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)"
   6.279 @@ -315,16 +315,17 @@
   6.280  apply(simp add:int_distrib)
   6.281  done
   6.282  
   6.283 -
   6.284 +text {*
   6.285 +  \medskip Theorems for the generation of the bachwards direction of
   6.286 +  Cooper's Theorem.
   6.287  
   6.288 -(*Theorems for the generation of the bachwards direction of cooper's theorem*)
   6.289 -(*These are the 6 interesting atomic cases which have to be proved relying on the
   6.290 -properties of A-set ant the arithmetic and contradiction proofs*)
   6.291 +  These are the 6 interesting atomic cases which have to be proved
   6.292 +  relying on the properties of A-set ant the arithmetic and
   6.293 +  contradiction proofs. *}
   6.294  
   6.295  lemma not_ast_p_gt: "0 < (d::int) ==>
   6.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 )"
   6.297 -by arith
   6.298 -
   6.299 +  by arith
   6.300  
   6.301  lemma not_ast_p_lt: "\<lbrakk>0 < d ;(t::int) \<in> A \<rbrakk> \<Longrightarrow>
   6.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)"
   6.303 @@ -377,12 +378,11 @@
   6.304    apply(simp add:int_distrib)
   6.305    done
   6.306  
   6.307 -
   6.308 +text {*
   6.309 +  \medskip These are the atomic cases for the proof generation for the
   6.310 +  modulo @{text D} property for @{text "P plusinfinity"}
   6.311  
   6.312 -(*=============================================================================*)
   6.313 -(*These are the atomic cases for the proof generation for the modulo D property for P
   6.314 -plusinfinity*)
   6.315 -(*They are fully based on arithmetics*)
   6.316 +  They are fully based on arithmetics. *}
   6.317  
   6.318  lemma  dvd_modd_pinf: "((d::int) dvd d1) ==>
   6.319   (ALL (x::int). ALL (k::int). (((d::int) dvd (x + t)) = (d dvd (x+k*d1 + t))))"
   6.320 @@ -412,10 +412,12 @@
   6.321    apply(simp add:int_distrib mult_ac)
   6.322    done
   6.323  
   6.324 -(*=============================================================================*)
   6.325 -(*These are the atomic cases for the proof generation for the equivalence of P and P
   6.326 -plusinfinity for integers x greather than some integer z.*)
   6.327 -(*They are fully based on arithmetics*)
   6.328 +text {*
   6.329 +  \medskip These are the atomic cases for the proof generation for the
   6.330 +  equivalence of @{text P} and @{text "P plusinfinity"} for integers
   6.331 +  @{text x} greater than some integer @{text z}.
   6.332 +
   6.333 +  They are fully based on arithmetics. *}
   6.334  
   6.335  lemma  eq_eq_pinf: "EX z::int. ALL x. z < x --> (( 0 = x +t ) = False )"
   6.336    apply(rule_tac x = "-t" in exI)
   6.337 @@ -438,18 +440,16 @@
   6.338    done
   6.339  
   6.340  lemma  dvd_eq_pinf: "EX z::int. ALL x.  z < x --> ((d dvd (x + t)) = (d dvd (x + t))) "
   6.341 -by simp
   6.342 +  by simp
   6.343  
   6.344  lemma  not_dvd_eq_pinf: "EX z::int. ALL x. z < x  --> ((~(d dvd (x + t))) = (~(d dvd (x + t)))) "
   6.345 -by simp
   6.346 -
   6.347 -
   6.348 -
   6.349 +  by simp
   6.350  
   6.351 -(*=============================================================================*)
   6.352 -(*These are the atomic cases for the proof generation for the modulo D property for P
   6.353 -minusinfinity*)
   6.354 -(*They are fully based on arithmetics*)
   6.355 +text {*
   6.356 +  \medskip These are the atomic cases for the proof generation for the
   6.357 +  modulo @{text D} property for @{text "P minusinfinity"}.
   6.358 +
   6.359 +  They are fully based on arithmetics. *}
   6.360  
   6.361  lemma  dvd_modd_minf: "((d::int) dvd d1) ==>
   6.362   (ALL (x::int). ALL (k::int). (((d::int) dvd (x + t)) = (d dvd (x-k*d1 + t))))"
   6.363 @@ -480,11 +480,12 @@
   6.364  apply(simp add:int_distrib mult_ac)
   6.365  done
   6.366  
   6.367 +text {*
   6.368 +  \medskip These are the atomic cases for the proof generation for the
   6.369 +  equivalence of @{text P} and @{text "P minusinfinity"} for integers
   6.370 +  @{text x} less than some integer @{text z}.
   6.371  
   6.372 -(*=============================================================================*)
   6.373 -(*These are the atomic cases for the proof generation for the equivalence of P and P
   6.374 -minusinfinity for integers x less than some integer z.*)
   6.375 -(*They are fully based on arithmetics*)
   6.376 +  They are fully based on arithmetics. *}
   6.377  
   6.378  lemma  eq_eq_minf: "EX z::int. ALL x. x < z --> (( 0 = x +t ) = False )"
   6.379  apply(rule_tac x = "-t" in exI)
   6.380 @@ -508,17 +509,18 @@
   6.381  done
   6.382  
   6.383  lemma  dvd_eq_minf: "EX z::int. ALL x. x < z --> ((d dvd (x + t)) = (d dvd (x + t))) "
   6.384 -by simp
   6.385 +  by simp
   6.386  
   6.387  lemma  not_dvd_eq_minf: "EX z::int. ALL x. x < z --> ((~(d dvd (x + t))) = (~(d dvd (x + t)))) "
   6.388 -by simp
   6.389 -
   6.390 +  by simp
   6.391  
   6.392 -(*=============================================================================*)
   6.393 -(*This Theorem combines whithnesses about P minusinfinity to schow one component of the
   6.394 -equivalence proof for cooper's theorem*)
   6.395 +text {*
   6.396 +  \medskip This Theorem combines whithnesses about @{text "P
   6.397 +  minusinfinity"} to show one component of the equivalence proof for
   6.398 +  Cooper's Theorem.
   6.399  
   6.400 -(* FIXME: remove once they are part of the distribution *)
   6.401 +  FIXME: remove once they are part of the distribution. *}
   6.402 +
   6.403  theorem int_ge_induct[consumes 1,case_names base step]:
   6.404    assumes ge: "k \<le> (i::int)" and
   6.405          base: "P(k)" and
   6.406 @@ -590,9 +592,10 @@
   6.407    qed
   6.408  qed
   6.409  
   6.410 -(*=============================================================================*)
   6.411 -(*This Theorem combines whithnesses about P minusinfinity to schow one component of the
   6.412 -equivalence proof for cooper's theorem*)
   6.413 +text {*
   6.414 +  \medskip This Theorem combines whithnesses about @{text "P
   6.415 +  minusinfinity"} to show one component of the equivalence proof for
   6.416 +  Cooper's Theorem. *}
   6.417  
   6.418  lemma plusinfinity:
   6.419    assumes "0 < d" and
   6.420 @@ -613,10 +616,8 @@
   6.421    qed
   6.422  qed
   6.423   
   6.424 -
   6.425 -
   6.426 -(*=============================================================================*)
   6.427 -(*Theorem for periodic function on discrete sets*)
   6.428 +text {*
   6.429 +  \medskip Theorem for periodic function on discrete sets. *}
   6.430  
   6.431  lemma minf_vee:
   6.432    assumes dpos: "(0::int) < d" and modd: "ALL x k. P x = P(x - k*d)"
   6.433 @@ -651,8 +652,9 @@
   6.434    assume ?RHS thus ?LHS by blast
   6.435  qed
   6.436  
   6.437 -(*=============================================================================*)
   6.438 -(*Theorem for periodic function on discrete sets*)
   6.439 +text {*
   6.440 +  \medskip Theorem for periodic function on discrete sets. *}
   6.441 +
   6.442  lemma pinf_vee:
   6.443    assumes dpos: "0 < (d::int)" and modd: "ALL (x::int) (k::int). P x = P (x+k*d)"
   6.444    shows "(EX x::int. P x) = (EX (j::int) : {1..d} . P j)"
   6.445 @@ -750,7 +752,7 @@
   6.446  apply(blast dest:decr_mult_lemma)
   6.447  done
   6.448  
   6.449 -(* Cooper Thm `, plus infinity version*)
   6.450 +text {* Cooper Theorem, plus infinity version. *}
   6.451  lemma cppi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. z < x --> (P x = P1 x))
   6.452  ==> ALL x.~(EX (j::int) : {1..D}. EX (a::int) : A. P(a - j)) --> P (x) --> P (x + D) 
   6.453  ==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x+k*D))))
   6.454 @@ -774,9 +776,8 @@
   6.455    done
   6.456  
   6.457  
   6.458 -(*=============================================================================*)
   6.459 -
   6.460 -(*Theorems for the quantifier elminination Functions.*)
   6.461 +text {*
   6.462 +  \bigskip Theorems for the quantifier elminination Functions. *}
   6.463  
   6.464  lemma qe_ex_conj: "(EX (x::int). A x) = R
   6.465  		==> (EX (x::int). P x) = (Q & (EX x::int. A x))
   6.466 @@ -805,7 +806,7 @@
   6.467  lemma qe_ALL: "(EX x. ~P x) = R ==> (ALL x. P x) = (~R)"
   6.468  by blast
   6.469  
   6.470 -(* Theorems for proving NNF *)
   6.471 +text {* \bigskip Theorems for proving NNF *}
   6.472  
   6.473  lemma nnf_im: "((~P) = P1) ==> (Q=Q1) ==> ((P --> Q) = (P1 | Q1))"
   6.474  by blast
   6.475 @@ -851,7 +852,7 @@
   6.476  apply(fastsimp)
   6.477  done
   6.478  
   6.479 -(* Theorems required for the adjustcoeffitienteq*)
   6.480 +text {* \bigskip Theorems required for the @{text adjustcoeffitienteq} *}
   6.481  
   6.482  lemma ac_dvd_eq: assumes not0: "0 ~= (k::int)"
   6.483  shows "((m::int) dvd (c*n+t)) = (k*m dvd ((k*c)*n+(k*t)))" (is "?P = ?Q")
   6.484 @@ -925,7 +926,7 @@
   6.485  lemma lf_dvd: "(l::int) = ll ==> (r::int) = lr ==> (l dvd r) =(ll dvd lr)"
   6.486  by simp
   6.487  
   6.488 -(* Theorems for transforming predicates on nat to predicates on int*)
   6.489 +text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*}
   6.490  
   6.491  theorem all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))"
   6.492    by (simp split add: split_nat)
   6.493 @@ -973,7 +974,9 @@
   6.494  
   6.495  theorem Suc_plus1: "Suc n = n + 1" by simp
   6.496  
   6.497 -(* specific instances of congruence rules, to prevent simplifier from looping *)
   6.498 +text {*
   6.499 +  \medskip Specific instances of congruence rules, to prevent
   6.500 +  simplifier from looping. *}
   6.501  
   6.502  theorem imp_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::nat) \<longrightarrow> P) = (0 <= x \<longrightarrow> P')"
   6.503    by simp
     7.1 --- a/src/HOL/Power.thy	Fri Apr 16 04:06:52 2004 +0200
     7.2 +++ b/src/HOL/Power.thy	Fri Apr 16 04:07:10 2004 +0200
     7.3 @@ -24,7 +24,7 @@
     7.4  
     7.5  lemma power_one [simp]: "1^n = (1::'a::ringpower)"
     7.6  apply (induct_tac "n")
     7.7 -apply (auto simp add: power_Suc)  
     7.8 +apply (auto simp add: power_Suc)
     7.9  done
    7.10  
    7.11  lemma power_one_right [simp]: "(a::'a::ringpower) ^ 1 = a"
    7.12 @@ -41,7 +41,7 @@
    7.13  done
    7.14  
    7.15  lemma power_mult_distrib: "((a::'a::ringpower) * b) ^ n = (a^n) * (b^n)"
    7.16 -apply (induct_tac "n") 
    7.17 +apply (induct_tac "n")
    7.18  apply (auto simp add: power_Suc mult_ac)
    7.19  done
    7.20  
    7.21 @@ -54,7 +54,7 @@
    7.22  lemma zero_le_power:
    7.23       "0 \<le> (a::'a::{ordered_semiring,ringpower}) ==> 0 \<le> a^n"
    7.24  apply (simp add: order_le_less)
    7.25 -apply (erule disjE) 
    7.26 +apply (erule disjE)
    7.27  apply (simp_all add: zero_less_power zero_less_one power_0_left)
    7.28  done
    7.29  
    7.30 @@ -62,25 +62,22 @@
    7.31       "1 \<le> (a::'a::{ordered_semiring,ringpower}) ==> 1 \<le> a^n"
    7.32  apply (induct_tac "n")
    7.33  apply (simp_all add: power_Suc)
    7.34 -apply (rule order_trans [OF _ mult_mono [of 1 _ 1]]) 
    7.35 -apply (simp_all add: zero_le_one order_trans [OF zero_le_one]) 
    7.36 +apply (rule order_trans [OF _ mult_mono [of 1 _ 1]])
    7.37 +apply (simp_all add: zero_le_one order_trans [OF zero_le_one])
    7.38  done
    7.39  
    7.40  lemma gt1_imp_ge0: "1 < a ==> 0 \<le> (a::'a::ordered_semiring)"
    7.41    by (simp add: order_trans [OF zero_le_one order_less_imp_le])
    7.42  
    7.43  lemma power_gt1_lemma:
    7.44 -     assumes gt1: "1 < (a::'a::{ordered_semiring,ringpower})"
    7.45 -        shows     "1 < a * a^n"
    7.46 +  assumes gt1: "1 < (a::'a::{ordered_semiring,ringpower})"
    7.47 +  shows "1 < a * a^n"
    7.48  proof -
    7.49 -  have "1*1 < a * a^n"
    7.50 -    proof (rule order_less_le_trans) 
    7.51 -      show "1*1 < a*1" by (simp add: gt1)
    7.52 -      show  "a*1 \<le> a * a^n"
    7.53 -   by (simp only: mult_mono gt1 gt1_imp_ge0 one_le_power order_less_imp_le 
    7.54 -                  zero_le_one order_refl)
    7.55 -    qed
    7.56 -  thus ?thesis by simp
    7.57 +  have "1*1 < a*1" using gt1 by simp
    7.58 +  also have "\<dots> \<le> a * a^n" using gt1
    7.59 +    by (simp only: mult_mono gt1_imp_ge0 one_le_power order_less_imp_le
    7.60 +        zero_le_one order_refl)
    7.61 +  finally show ?thesis by simp
    7.62  qed
    7.63  
    7.64  lemma power_gt1:
    7.65 @@ -88,52 +85,52 @@
    7.66  by (simp add: power_gt1_lemma power_Suc)
    7.67  
    7.68  lemma power_le_imp_le_exp:
    7.69 -     assumes gt1: "(1::'a::{ringpower,ordered_semiring}) < a"
    7.70 -       shows      "!!n. a^m \<le> a^n ==> m \<le> n"
    7.71 -proof (induct "m")
    7.72 +  assumes gt1: "(1::'a::{ringpower,ordered_semiring}) < a"
    7.73 +  shows "!!n. a^m \<le> a^n ==> m \<le> n"
    7.74 +proof (induct m)
    7.75    case 0
    7.76 -    show ?case by simp
    7.77 +  show ?case by simp
    7.78  next
    7.79    case (Suc m)
    7.80 -    show ?case 
    7.81 -      proof (cases n)
    7.82 -        case 0
    7.83 -          from prems have "a * a^m \<le> 1" by (simp add: power_Suc)
    7.84 -          with gt1 show ?thesis
    7.85 -            by (force simp only: power_gt1_lemma 
    7.86 -                                 linorder_not_less [symmetric])
    7.87 -      next
    7.88 -        case (Suc n)
    7.89 -          from prems show ?thesis 
    7.90 -	    by (force dest: mult_left_le_imp_le
    7.91 -	          simp add: power_Suc order_less_trans [OF zero_less_one gt1]) 
    7.92 -      qed
    7.93 +  show ?case
    7.94 +  proof (cases n)
    7.95 +    case 0
    7.96 +    from prems have "a * a^m \<le> 1" by (simp add: power_Suc)
    7.97 +    with gt1 show ?thesis
    7.98 +      by (force simp only: power_gt1_lemma
    7.99 +          linorder_not_less [symmetric])
   7.100 +  next
   7.101 +    case (Suc n)
   7.102 +    from prems show ?thesis
   7.103 +      by (force dest: mult_left_le_imp_le
   7.104 +          simp add: power_Suc order_less_trans [OF zero_less_one gt1])
   7.105 +  qed
   7.106  qed
   7.107  
   7.108 -text{*Surely we can strengthen this? It holds for 0<a<1 too.*}
   7.109 +text{*Surely we can strengthen this? It holds for @{text "0<a<1"} too.*}
   7.110  lemma power_inject_exp [simp]:
   7.111       "1 < (a::'a::{ordered_semiring,ringpower}) ==> (a^m = a^n) = (m=n)"
   7.112 -  by (force simp add: order_antisym power_le_imp_le_exp)  
   7.113 +  by (force simp add: order_antisym power_le_imp_le_exp)
   7.114  
   7.115  text{*Can relax the first premise to @{term "0<a"} in the case of the
   7.116  natural numbers.*}
   7.117  lemma power_less_imp_less_exp:
   7.118       "[| (1::'a::{ringpower,ordered_semiring}) < a; a^m < a^n |] ==> m < n"
   7.119 -by (simp add: order_less_le [of m n] order_less_le [of "a^m" "a^n"] 
   7.120 -              power_le_imp_le_exp) 
   7.121 +by (simp add: order_less_le [of m n] order_less_le [of "a^m" "a^n"]
   7.122 +              power_le_imp_le_exp)
   7.123  
   7.124  
   7.125  lemma power_mono:
   7.126       "[|a \<le> b; (0::'a::{ringpower,ordered_semiring}) \<le> a|] ==> a^n \<le> b^n"
   7.127 -apply (induct_tac "n") 
   7.128 +apply (induct_tac "n")
   7.129  apply (simp_all add: power_Suc)
   7.130  apply (auto intro: mult_mono zero_le_power order_trans [of 0 a b])
   7.131  done
   7.132  
   7.133  lemma power_strict_mono [rule_format]:
   7.134 -     "[|a < b; (0::'a::{ringpower,ordered_semiring}) \<le> a|] 
   7.135 -      ==> 0 < n --> a^n < b^n" 
   7.136 -apply (induct_tac "n") 
   7.137 +     "[|a < b; (0::'a::{ringpower,ordered_semiring}) \<le> a|]
   7.138 +      ==> 0 < n --> a^n < b^n"
   7.139 +apply (induct_tac "n")
   7.140  apply (auto simp add: mult_strict_mono zero_le_power power_Suc
   7.141                        order_le_less_trans [of 0 a b])
   7.142  done
   7.143 @@ -166,15 +163,15 @@
   7.144  apply (auto simp add: power_Suc inverse_mult_distrib)
   7.145  done
   7.146  
   7.147 -lemma nonzero_power_divide: 
   7.148 +lemma nonzero_power_divide:
   7.149      "b \<noteq> 0 ==> (a/b) ^ n = ((a::'a::{field,ringpower}) ^ n) / (b ^ n)"
   7.150  by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse)
   7.151  
   7.152 -lemma power_divide: 
   7.153 +lemma power_divide:
   7.154      "(a/b) ^ n = ((a::'a::{field,division_by_zero,ringpower}) ^ n / b ^ n)"
   7.155  apply (case_tac "b=0", simp add: power_0_left)
   7.156 -apply (rule nonzero_power_divide) 
   7.157 -apply assumption 
   7.158 +apply (rule nonzero_power_divide)
   7.159 +apply assumption
   7.160  done
   7.161  
   7.162  lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_ring,ringpower}) ^ n"
   7.163 @@ -183,7 +180,7 @@
   7.164  done
   7.165  
   7.166  lemma zero_less_power_abs_iff [simp]:
   7.167 -     "(0 < (abs a)^n) = (a \<noteq> (0::'a::{ordered_ring,ringpower}) | n=0)" 
   7.168 +     "(0 < (abs a)^n) = (a \<noteq> (0::'a::{ordered_ring,ringpower}) | n=0)"
   7.169  proof (induct "n")
   7.170    case 0
   7.171      show ?case by (simp add: zero_less_one)
   7.172 @@ -208,19 +205,19 @@
   7.173  lemma power_Suc_less:
   7.174       "[|(0::'a::{ordered_semiring,ringpower}) < a; a < 1|]
   7.175        ==> a * a^n < a^n"
   7.176 -apply (induct_tac n) 
   7.177 -apply (auto simp add: power_Suc mult_strict_left_mono) 
   7.178 +apply (induct_tac n)
   7.179 +apply (auto simp add: power_Suc mult_strict_left_mono)
   7.180  done
   7.181  
   7.182  lemma power_strict_decreasing:
   7.183       "[|n < N; 0 < a; a < (1::'a::{ordered_semiring,ringpower})|]
   7.184        ==> a^N < a^n"
   7.185 -apply (erule rev_mp) 
   7.186 -apply (induct_tac "N")  
   7.187 -apply (auto simp add: power_Suc power_Suc_less less_Suc_eq) 
   7.188 -apply (rename_tac m)  
   7.189 +apply (erule rev_mp)
   7.190 +apply (induct_tac "N")
   7.191 +apply (auto simp add: power_Suc power_Suc_less less_Suc_eq)
   7.192 +apply (rename_tac m)
   7.193  apply (subgoal_tac "a * a^m < 1 * a^n", simp)
   7.194 -apply (rule mult_strict_mono) 
   7.195 +apply (rule mult_strict_mono)
   7.196  apply (auto simp add: zero_le_power zero_less_one order_less_imp_le)
   7.197  done
   7.198  
   7.199 @@ -228,47 +225,47 @@
   7.200  lemma power_decreasing:
   7.201       "[|n \<le> N; 0 \<le> a; a \<le> (1::'a::{ordered_semiring,ringpower})|]
   7.202        ==> a^N \<le> a^n"
   7.203 -apply (erule rev_mp) 
   7.204 -apply (induct_tac "N") 
   7.205 -apply (auto simp add: power_Suc  le_Suc_eq) 
   7.206 -apply (rename_tac m)  
   7.207 +apply (erule rev_mp)
   7.208 +apply (induct_tac "N")
   7.209 +apply (auto simp add: power_Suc  le_Suc_eq)
   7.210 +apply (rename_tac m)
   7.211  apply (subgoal_tac "a * a^m \<le> 1 * a^n", simp)
   7.212 -apply (rule mult_mono) 
   7.213 +apply (rule mult_mono)
   7.214  apply (auto simp add: zero_le_power zero_le_one)
   7.215  done
   7.216  
   7.217  lemma power_Suc_less_one:
   7.218       "[| 0 < a; a < (1::'a::{ordered_semiring,ringpower}) |] ==> a ^ Suc n < 1"
   7.219 -apply (insert power_strict_decreasing [of 0 "Suc n" a], simp) 
   7.220 +apply (insert power_strict_decreasing [of 0 "Suc n" a], simp)
   7.221  done
   7.222  
   7.223  text{*Proof again resembles that of @{text power_strict_decreasing}*}
   7.224  lemma power_increasing:
   7.225       "[|n \<le> N; (1::'a::{ordered_semiring,ringpower}) \<le> a|] ==> a^n \<le> a^N"
   7.226 -apply (erule rev_mp) 
   7.227 -apply (induct_tac "N") 
   7.228 -apply (auto simp add: power_Suc le_Suc_eq) 
   7.229 +apply (erule rev_mp)
   7.230 +apply (induct_tac "N")
   7.231 +apply (auto simp add: power_Suc le_Suc_eq)
   7.232  apply (rename_tac m)
   7.233  apply (subgoal_tac "1 * a^n \<le> a * a^m", simp)
   7.234 -apply (rule mult_mono) 
   7.235 +apply (rule mult_mono)
   7.236  apply (auto simp add: order_trans [OF zero_le_one] zero_le_power)
   7.237  done
   7.238  
   7.239  text{*Lemma for @{text power_strict_increasing}*}
   7.240  lemma power_less_power_Suc:
   7.241       "(1::'a::{ordered_semiring,ringpower}) < a ==> a^n < a * a^n"
   7.242 -apply (induct_tac n) 
   7.243 -apply (auto simp add: power_Suc mult_strict_left_mono order_less_trans [OF zero_less_one]) 
   7.244 +apply (induct_tac n)
   7.245 +apply (auto simp add: power_Suc mult_strict_left_mono order_less_trans [OF zero_less_one])
   7.246  done
   7.247  
   7.248  lemma power_strict_increasing:
   7.249       "[|n < N; (1::'a::{ordered_semiring,ringpower}) < a|] ==> a^n < a^N"
   7.250 -apply (erule rev_mp) 
   7.251 -apply (induct_tac "N")  
   7.252 -apply (auto simp add: power_less_power_Suc power_Suc less_Suc_eq) 
   7.253 +apply (erule rev_mp)
   7.254 +apply (induct_tac "N")
   7.255 +apply (auto simp add: power_less_power_Suc power_Suc less_Suc_eq)
   7.256  apply (rename_tac m)
   7.257  apply (subgoal_tac "1 * a^n < a * a^m", simp)
   7.258 -apply (rule mult_strict_mono)  
   7.259 +apply (rule mult_strict_mono)
   7.260  apply (auto simp add: order_less_trans [OF zero_less_one] zero_le_power
   7.261                   order_less_imp_le)
   7.262  done
   7.263 @@ -282,13 +279,13 @@
   7.264     assume "~ a \<le> b"
   7.265     then have "b < a" by (simp only: linorder_not_le)
   7.266     then have "b ^ Suc n < a ^ Suc n"
   7.267 -     by (simp only: prems power_strict_mono) 
   7.268 +     by (simp only: prems power_strict_mono)
   7.269     from le and this show "False"
   7.270        by (simp add: linorder_not_less [symmetric])
   7.271   qed
   7.272 -  
   7.273 +
   7.274  lemma power_inject_base:
   7.275 -     "[| a ^ Suc n = b ^ Suc n; 0 \<le> a; 0 \<le> b |] 
   7.276 +     "[| a ^ Suc n = b ^ Suc n; 0 \<le> a; 0 \<le> b |]
   7.277        ==> a = (b::'a::{ordered_semiring,ringpower})"
   7.278  by (blast intro: power_le_imp_le_base order_antisym order_eq_refl sym)
   7.279  
   7.280 @@ -298,7 +295,7 @@
   7.281  primrec (power)
   7.282    "p ^ 0 = 1"
   7.283    "p ^ (Suc n) = (p::nat) * (p ^ n)"
   7.284 -  
   7.285 +
   7.286  instance nat :: ringpower
   7.287  proof
   7.288    fix z n :: nat
   7.289 @@ -321,7 +318,7 @@
   7.290  lemma nat_power_less_imp_less: "!!i::nat. [| 0 < i; i^m < i^n |] ==> m < n"
   7.291  apply (rule ccontr)
   7.292  apply (drule leI [THEN le_imp_power_dvd, THEN dvd_imp_le, THEN leD])
   7.293 -apply (erule zero_less_power, auto) 
   7.294 +apply (erule zero_less_power, auto)
   7.295  done
   7.296  
   7.297  lemma nat_zero_less_power_iff [simp]: "(0 < x^n) = (x \<noteq> (0::nat) | n=0)"
   7.298 @@ -341,7 +338,7 @@
   7.299  
   7.300  subsection{*Binomial Coefficients*}
   7.301  
   7.302 -text{*This development is based on the work of Andy Gordon and 
   7.303 +text{*This development is based on the work of Andy Gordon and
   7.304  Florian Kammueller*}
   7.305  
   7.306  consts
   7.307 @@ -400,7 +397,7 @@
   7.308  apply (induct_tac "n")
   7.309  apply (simp add: binomial_0, clarify)
   7.310  apply (case_tac "k")
   7.311 -apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq 
   7.312 +apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq
   7.313                        binomial_eq_0)
   7.314  done
   7.315  
   7.316 @@ -408,7 +405,7 @@
   7.317    need to reason about division.*}
   7.318  lemma binomial_Suc_Suc_eq_times:
   7.319       "k \<le> n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k"
   7.320 -by (simp add: Suc_times_binomial_eq div_mult_self_is_m zero_less_Suc 
   7.321 +by (simp add: Suc_times_binomial_eq div_mult_self_is_m zero_less_Suc
   7.322          del: mult_Suc mult_Suc_right)
   7.323  
   7.324  text{*Another version, with -1 instead of Suc.*}
   7.325 @@ -460,7 +457,7 @@
   7.326  val power_le_imp_le_base = thm"power_le_imp_le_base";
   7.327  val power_inject_base = thm"power_inject_base";
   7.328  *}
   7.329 - 
   7.330 +
   7.331  text{*ML bindings for the remaining theorems*}
   7.332  ML
   7.333  {*
     8.1 --- a/src/HOL/PreList.thy	Fri Apr 16 04:06:52 2004 +0200
     8.2 +++ b/src/HOL/PreList.thy	Fri Apr 16 04:07:10 2004 +0200
     8.3 @@ -6,13 +6,14 @@
     8.4  
     8.5  header{*A Basis for Building the Theory of Lists*}
     8.6  
     8.7 -(*Is defined separately to serve as a basis for theory ToyList in the
     8.8 -documentation.*)
     8.9 -
    8.10  theory PreList =
    8.11      Wellfounded_Relations + Presburger + Recdef + Relation_Power + Parity:
    8.12  
    8.13 -(*belongs to theory Wellfounded_Recursion*)
    8.14 +text {*
    8.15 +  Is defined separately to serve as a basis for theory ToyList in the
    8.16 +  documentation. *}
    8.17 +
    8.18  lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf]
    8.19 +  -- {* belongs to theory @{text Wellfounded_Recursion} *}
    8.20  
    8.21  end
     9.1 --- a/src/HOL/Presburger.thy	Fri Apr 16 04:06:52 2004 +0200
     9.2 +++ b/src/HOL/Presburger.thy	Fri Apr 16 04:07:10 2004 +0200
     9.3 @@ -7,6 +7,8 @@
     9.4  generation for Cooper Algorithm  
     9.5  *)
     9.6  
     9.7 +header {* Presburger Arithmetic: Cooper Algorithm *}
     9.8 +
     9.9  theory Presburger = NatSimprocs + SetInterval
    9.10  files
    9.11    ("cooper_dec.ML")
    9.12 @@ -14,7 +16,7 @@
    9.13    ("qelim.ML")
    9.14    ("presburger.ML"):
    9.15  
    9.16 -(* Theorem for unitifying the coeffitients of x in an existential formula*)
    9.17 +text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*}
    9.18  
    9.19  theorem unity_coeff_ex: "(\<exists>x::int. P (l * x)) = (\<exists>x. l dvd (1*x+0) \<and> P x)"
    9.20    apply (rule iffI)
    9.21 @@ -54,7 +56,7 @@
    9.22  
    9.23  
    9.24  
    9.25 -(*Theorems for the combination of proofs of the equality of P and P_m for integers x less than some integer z.*)
    9.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}.*}
    9.27  
    9.28  theorem eq_minf_conjI: "\<exists>z1::int. \<forall>x. x < z1 \<longrightarrow> (A1 x = A2 x) \<Longrightarrow>
    9.29    \<exists>z2::int. \<forall>x. x < z2 \<longrightarrow> (B1 x = B2 x) \<Longrightarrow>
    9.30 @@ -75,7 +77,7 @@
    9.31    done
    9.32  
    9.33  
    9.34 -(*Theorems for the combination of proofs of the equality of P and P_m for integers x greather than some integer z.*)
    9.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}.*}
    9.36  
    9.37  theorem eq_pinf_conjI: "\<exists>z1::int. \<forall>x. z1 < x \<longrightarrow> (A1 x = A2 x) \<Longrightarrow>
    9.38    \<exists>z2::int. \<forall>x. z2 < x \<longrightarrow> (B1 x = B2 x) \<Longrightarrow>
    9.39 @@ -93,75 +95,76 @@
    9.40    apply (rule_tac x = "max z1 z2" in exI)
    9.41    apply simp
    9.42    done
    9.43 -(*=============================================================================*)
    9.44 -(*Theorems for the combination of proofs of the modulo D property for P
    9.45 -pluusinfinity*)
    9.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*)
    9.47 +
    9.48 +text {*
    9.49 +  \medskip Theorems for the combination of proofs of the modulo @{text
    9.50 +  D} property for @{text "P plusinfinity"}
    9.51 +
    9.52 +  FIXME: This is THE SAME theorem as for the @{text minusinf} version,
    9.53 +  but with @{text "+k.."} instead of @{text "-k.."} In the future
    9.54 +  replace these both with only one. *}
    9.55  
    9.56  theorem modd_pinf_conjI: "\<forall>(x::int) k. A x = A (x+k*d) \<Longrightarrow>
    9.57    \<forall>(x::int) k. B x = B (x+k*d) \<Longrightarrow>
    9.58    \<forall>(x::int) (k::int). (A x \<and> B x) = (A (x+k*d) \<and> B (x+k*d))"
    9.59    by simp
    9.60  
    9.61 -
    9.62  theorem modd_pinf_disjI: "\<forall>(x::int) k. A x = A (x+k*d) \<Longrightarrow>
    9.63    \<forall>(x::int) k. B x = B (x+k*d) \<Longrightarrow>
    9.64    \<forall>(x::int) (k::int). (A x \<or> B x) = (A (x+k*d) \<or> B (x+k*d))"
    9.65    by simp
    9.66  
    9.67 -(*=============================================================================*)
    9.68 -(*This is one of the cases where the simplifed formula is prooved to habe some property
    9.69 -(in relation to P_m) but we need to proove the property for the original formula (P_m)*)
    9.70 -(*FIXME : This is exaclty the same thm as for minusinf.*)
    9.71 +text {*
    9.72 +  This is one of the cases where the simplifed formula is prooved to
    9.73 +  habe some property (in relation to @{text P_m}) but we need to prove
    9.74 +  the property for the original formula (@{text P_m})
    9.75 +
    9.76 +  FIXME: This is exaclty the same thm as for @{text minusinf}. *}
    9.77 +
    9.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)) "
    9.79 -by blast
    9.80 +  by blast
    9.81  
    9.82  
    9.83 -
    9.84 -(*=============================================================================*)
    9.85 -(*Theorems for the combination of proofs of the modulo D property for P
    9.86 -minusinfinity*)
    9.87 +text {*
    9.88 +  \medskip Theorems for the combination of proofs of the modulo @{text D}
    9.89 +  property for @{text "P minusinfinity"} *}
    9.90  
    9.91  theorem modd_minf_conjI: "\<forall>(x::int) k. A x = A (x-k*d) \<Longrightarrow>
    9.92    \<forall>(x::int) k. B x = B (x-k*d) \<Longrightarrow>
    9.93    \<forall>(x::int) (k::int). (A x \<and> B x) = (A (x-k*d) \<and> B (x-k*d))"
    9.94    by simp
    9.95  
    9.96 -
    9.97  theorem modd_minf_disjI: "\<forall>(x::int) k. A x = A (x-k*d) \<Longrightarrow>
    9.98    \<forall>(x::int) k. B x = B (x-k*d) \<Longrightarrow>
    9.99    \<forall>(x::int) (k::int). (A x \<or> B x) = (A (x-k*d) \<or> B (x-k*d))"
   9.100    by simp
   9.101  
   9.102 -(*=============================================================================*)
   9.103 -(*This is one of the cases where the simplifed formula is prooved to habe some property
   9.104 -(in relation to P_m) but we need to proove the property for the original formula (P_m)*)
   9.105 +text {*
   9.106 +  This is one of the cases where the simplifed formula is prooved to
   9.107 +  have some property (in relation to @{text P_m}) but we need to
   9.108 +  prove the property for the original formula (@{text P_m}). *}
   9.109  
   9.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)) "
   9.111 -by blast
   9.112 +  by blast
   9.113  
   9.114 -(*=============================================================================*)
   9.115 -
   9.116 -(*theorem needed for prooving at runtime divide properties using the arithmetic tatic
   9.117 -(who knows only about modulo = 0)*)
   9.118 +text {*
   9.119 +  Theorem needed for proving at runtime divide properties using the
   9.120 +  arithmetic tactic (which knows only about modulo = 0). *}
   9.121  
   9.122  lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
   9.123 -by(simp add:dvd_def zmod_eq_0_iff)
   9.124 -
   9.125 -(*=============================================================================*)
   9.126 +  by(simp add:dvd_def zmod_eq_0_iff)
   9.127  
   9.128 -
   9.129 -
   9.130 -(*Theorems used for the combination of proof for the backwards direction of cooper's
   9.131 -theorem. they rely exclusively on Predicate calculus.*)
   9.132 +text {*
   9.133 +  \medskip Theorems used for the combination of proof for the
   9.134 +  backwards direction of Cooper's Theorem. They rely exclusively on
   9.135 +  Predicate calculus.*}
   9.136  
   9.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))
   9.138  ==>
   9.139  (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> P2(x) --> P2(x + d))
   9.140  ==>
   9.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))) "
   9.142 -by blast
   9.143 -
   9.144 +  by blast
   9.145  
   9.146  
   9.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))
   9.148 @@ -170,18 +173,18 @@
   9.149  ==>
   9.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)
   9.151  \<and> P2(x + d))) "
   9.152 -by blast
   9.153 +  by blast
   9.154  
   9.155  lemma not_ast_p_Q_elim: "
   9.156  (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) -->P(x) --> P(x + d))
   9.157  ==> ( P = Q )
   9.158  ==> (ALL x. ~(EX (j::int) : {1..d}. EX (a::int) : A. P(a - j)) -->P(x) --> P(x + d))"
   9.159 -by blast
   9.160 -(*=============================================================================*)
   9.161 +  by blast
   9.162  
   9.163 -
   9.164 -(*Theorems used for the combination of proof for the backwards direction of cooper's
   9.165 -theorem. they rely exclusively on Predicate calculus.*)
   9.166 +text {*
   9.167 +  \medskip Theorems used for the combination of proof for the
   9.168 +  backwards direction of Cooper's Theorem. They rely exclusively on
   9.169 +  Predicate calculus.*}
   9.170  
   9.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))
   9.172  ==>
   9.173 @@ -189,9 +192,7 @@
   9.174  ==>
   9.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)
   9.176  \<or> P2(x-d))) "
   9.177 -by blast
   9.178 -
   9.179 -
   9.180 +  by blast
   9.181  
   9.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))
   9.183  ==>
   9.184 @@ -199,68 +200,67 @@
   9.185  ==>
   9.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)
   9.187  \<and> P2(x-d))) "
   9.188 -by blast
   9.189 +  by blast
   9.190  
   9.191  lemma not_bst_p_Q_elim: "
   9.192  (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) -->P(x) --> P(x - d)) 
   9.193  ==> ( P = Q )
   9.194  ==> (ALL x. ~(EX (j::int) : {1..d}. EX (b::int) : B. P(b+j)) -->P(x) --> P(x - d))"
   9.195 -by blast
   9.196 -(*=============================================================================*)
   9.197 +  by blast
   9.198  
   9.199 -(*This is the first direction of cooper's theorem*)
   9.200 +text {* \medskip This is the first direction of Cooper's Theorem. *}
   9.201  lemma cooper_thm: "(R --> (EX x::int. P x))  ==> (Q -->(EX x::int.  P x )) ==> ((R|Q) --> (EX x::int. P x )) "
   9.202 -by blast
   9.203 +  by blast
   9.204  
   9.205 -(*=============================================================================*)
   9.206 -(*The full cooper's theoorem in its equivalence Form- Given the premisses it is trivial
   9.207 -too, it relies exclusively on prediacte calculus.*)
   9.208 +text {*
   9.209 +  \medskip The full Cooper's Theorem in its equivalence Form. Given
   9.210 +  the premises it is trivial too, it relies exclusively on prediacte calculus.*}
   9.211  lemma cooper_eq_thm: "(R --> (EX x::int. P x))  ==> (Q -->(EX x::int.  P x )) ==> ((~Q)
   9.212  --> (EX x::int. P x ) --> R) ==> (EX x::int. P x) = R|Q "
   9.213 -by blast
   9.214 +  by blast
   9.215  
   9.216 -(*=============================================================================*)
   9.217 -(*Some of the atomic theorems generated each time the atom does not depend on x, they
   9.218 -are trivial.*)
   9.219 +text {*
   9.220 +  \medskip Some of the atomic theorems generated each time the atom
   9.221 +  does not depend on @{text x}, they are trivial.*}
   9.222  
   9.223  lemma  fm_eq_minf: "EX z::int. ALL x. x < z --> (P = P) "
   9.224 -by blast
   9.225 +  by blast
   9.226  
   9.227  lemma  fm_modd_minf: "ALL (x::int). ALL (k::int). (P = P)"
   9.228 -by blast
   9.229 +  by blast
   9.230  
   9.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"
   9.232 -by blast
   9.233 -
   9.234 -
   9.235 +  by blast
   9.236  
   9.237  lemma  fm_eq_pinf: "EX z::int. ALL x. z < x --> (P = P) "
   9.238 -by blast
   9.239 +  by blast
   9.240  
   9.241 -(* The next 2 thms are the same as the minusinf version*)
   9.242 +text {* The next two thms are the same as the @{text minusinf} version. *}
   9.243 +
   9.244  lemma  fm_modd_pinf: "ALL (x::int). ALL (k::int). (P = P)"
   9.245 -by blast
   9.246 +  by blast
   9.247  
   9.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"
   9.249 -by blast
   9.250 +  by blast
   9.251  
   9.252 +text {* Theorems to be deleted from simpset when proving simplified formulaes. *}
   9.253  
   9.254 -(* Theorems to be deleted from simpset when proving simplified formulaes*)
   9.255  lemma P_eqtrue: "(P=True) = P"
   9.256    by rules
   9.257  
   9.258  lemma P_eqfalse: "(P=False) = (~P)"
   9.259    by rules
   9.260  
   9.261 -(*=============================================================================*)
   9.262 +text {*
   9.263 +  \medskip Theorems for the generation of the bachwards direction of
   9.264 +  Cooper's Theorem.
   9.265  
   9.266 -(*Theorems for the generation of the bachwards direction of cooper's theorem*)
   9.267 -(*These are the 6 interesting atomic cases which have to be proved relying on the
   9.268 -properties of B-set ant the arithmetic and contradiction proofs*)
   9.269 +  These are the 6 interesting atomic cases which have to be proved relying on the
   9.270 +  properties of B-set and the arithmetic and contradiction proofs. *}
   9.271  
   9.272  lemma not_bst_p_lt: "0 < (d::int) ==>
   9.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 )"
   9.274 -by arith
   9.275 +  by arith
   9.276  
   9.277  lemma not_bst_p_gt: "\<lbrakk> (g::int) \<in> B; g = -a \<rbrakk> \<Longrightarrow>
   9.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)"
   9.279 @@ -315,16 +315,17 @@
   9.280  apply(simp add:int_distrib)
   9.281  done
   9.282  
   9.283 -
   9.284 +text {*
   9.285 +  \medskip Theorems for the generation of the bachwards direction of
   9.286 +  Cooper's Theorem.
   9.287  
   9.288 -(*Theorems for the generation of the bachwards direction of cooper's theorem*)
   9.289 -(*These are the 6 interesting atomic cases which have to be proved relying on the
   9.290 -properties of A-set ant the arithmetic and contradiction proofs*)
   9.291 +  These are the 6 interesting atomic cases which have to be proved
   9.292 +  relying on the properties of A-set ant the arithmetic and
   9.293 +  contradiction proofs. *}
   9.294  
   9.295  lemma not_ast_p_gt: "0 < (d::int) ==>
   9.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 )"
   9.297 -by arith
   9.298 -
   9.299 +  by arith
   9.300  
   9.301  lemma not_ast_p_lt: "\<lbrakk>0 < d ;(t::int) \<in> A \<rbrakk> \<Longrightarrow>
   9.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)"
   9.303 @@ -377,12 +378,11 @@
   9.304    apply(simp add:int_distrib)
   9.305    done
   9.306  
   9.307 -
   9.308 +text {*
   9.309 +  \medskip These are the atomic cases for the proof generation for the
   9.310 +  modulo @{text D} property for @{text "P plusinfinity"}
   9.311  
   9.312 -(*=============================================================================*)
   9.313 -(*These are the atomic cases for the proof generation for the modulo D property for P
   9.314 -plusinfinity*)
   9.315 -(*They are fully based on arithmetics*)
   9.316 +  They are fully based on arithmetics. *}
   9.317  
   9.318  lemma  dvd_modd_pinf: "((d::int) dvd d1) ==>
   9.319   (ALL (x::int). ALL (k::int). (((d::int) dvd (x + t)) = (d dvd (x+k*d1 + t))))"
   9.320 @@ -412,10 +412,12 @@
   9.321    apply(simp add:int_distrib mult_ac)
   9.322    done
   9.323  
   9.324 -(*=============================================================================*)
   9.325 -(*These are the atomic cases for the proof generation for the equivalence of P and P
   9.326 -plusinfinity for integers x greather than some integer z.*)
   9.327 -(*They are fully based on arithmetics*)
   9.328 +text {*
   9.329 +  \medskip These are the atomic cases for the proof generation for the
   9.330 +  equivalence of @{text P} and @{text "P plusinfinity"} for integers
   9.331 +  @{text x} greater than some integer @{text z}.
   9.332 +
   9.333 +  They are fully based on arithmetics. *}
   9.334  
   9.335  lemma  eq_eq_pinf: "EX z::int. ALL x. z < x --> (( 0 = x +t ) = False )"
   9.336    apply(rule_tac x = "-t" in exI)
   9.337 @@ -438,18 +440,16 @@
   9.338    done
   9.339  
   9.340  lemma  dvd_eq_pinf: "EX z::int. ALL x.  z < x --> ((d dvd (x + t)) = (d dvd (x + t))) "
   9.341 -by simp
   9.342 +  by simp
   9.343  
   9.344  lemma  not_dvd_eq_pinf: "EX z::int. ALL x. z < x  --> ((~(d dvd (x + t))) = (~(d dvd (x + t)))) "
   9.345 -by simp
   9.346 -
   9.347 -
   9.348 -
   9.349 +  by simp
   9.350  
   9.351 -(*=============================================================================*)
   9.352 -(*These are the atomic cases for the proof generation for the modulo D property for P
   9.353 -minusinfinity*)
   9.354 -(*They are fully based on arithmetics*)
   9.355 +text {*
   9.356 +  \medskip These are the atomic cases for the proof generation for the
   9.357 +  modulo @{text D} property for @{text "P minusinfinity"}.
   9.358 +
   9.359 +  They are fully based on arithmetics. *}
   9.360  
   9.361  lemma  dvd_modd_minf: "((d::int) dvd d1) ==>
   9.362   (ALL (x::int). ALL (k::int). (((d::int) dvd (x + t)) = (d dvd (x-k*d1 + t))))"
   9.363 @@ -480,11 +480,12 @@
   9.364  apply(simp add:int_distrib mult_ac)
   9.365  done
   9.366  
   9.367 +text {*
   9.368 +  \medskip These are the atomic cases for the proof generation for the
   9.369 +  equivalence of @{text P} and @{text "P minusinfinity"} for integers
   9.370 +  @{text x} less than some integer @{text z}.
   9.371  
   9.372 -(*=============================================================================*)
   9.373 -(*These are the atomic cases for the proof generation for the equivalence of P and P
   9.374 -minusinfinity for integers x less than some integer z.*)
   9.375 -(*They are fully based on arithmetics*)
   9.376 +  They are fully based on arithmetics. *}
   9.377  
   9.378  lemma  eq_eq_minf: "EX z::int. ALL x. x < z --> (( 0 = x +t ) = False )"
   9.379  apply(rule_tac x = "-t" in exI)
   9.380 @@ -508,17 +509,18 @@
   9.381  done
   9.382  
   9.383  lemma  dvd_eq_minf: "EX z::int. ALL x. x < z --> ((d dvd (x + t)) = (d dvd (x + t))) "
   9.384 -by simp
   9.385 +  by simp
   9.386  
   9.387  lemma  not_dvd_eq_minf: "EX z::int. ALL x. x < z --> ((~(d dvd (x + t))) = (~(d dvd (x + t)))) "
   9.388 -by simp
   9.389 -
   9.390 +  by simp
   9.391  
   9.392 -(*=============================================================================*)
   9.393 -(*This Theorem combines whithnesses about P minusinfinity to schow one component of the
   9.394 -equivalence proof for cooper's theorem*)
   9.395 +text {*
   9.396 +  \medskip This Theorem combines whithnesses about @{text "P
   9.397 +  minusinfinity"} to show one component of the equivalence proof for
   9.398 +  Cooper's Theorem.
   9.399  
   9.400 -(* FIXME: remove once they are part of the distribution *)
   9.401 +  FIXME: remove once they are part of the distribution. *}
   9.402 +
   9.403  theorem int_ge_induct[consumes 1,case_names base step]:
   9.404    assumes ge: "k \<le> (i::int)" and
   9.405          base: "P(k)" and
   9.406 @@ -590,9 +592,10 @@
   9.407    qed
   9.408  qed
   9.409  
   9.410 -(*=============================================================================*)
   9.411 -(*This Theorem combines whithnesses about P minusinfinity to schow one component of the
   9.412 -equivalence proof for cooper's theorem*)
   9.413 +text {*
   9.414 +  \medskip This Theorem combines whithnesses about @{text "P
   9.415 +  minusinfinity"} to show one component of the equivalence proof for
   9.416 +  Cooper's Theorem. *}
   9.417  
   9.418  lemma plusinfinity:
   9.419    assumes "0 < d" and
   9.420 @@ -613,10 +616,8 @@
   9.421    qed
   9.422  qed
   9.423   
   9.424 -
   9.425 -
   9.426 -(*=============================================================================*)
   9.427 -(*Theorem for periodic function on discrete sets*)
   9.428 +text {*
   9.429 +  \medskip Theorem for periodic function on discrete sets. *}
   9.430  
   9.431  lemma minf_vee:
   9.432    assumes dpos: "(0::int) < d" and modd: "ALL x k. P x = P(x - k*d)"
   9.433 @@ -651,8 +652,9 @@
   9.434    assume ?RHS thus ?LHS by blast
   9.435  qed
   9.436  
   9.437 -(*=============================================================================*)
   9.438 -(*Theorem for periodic function on discrete sets*)
   9.439 +text {*
   9.440 +  \medskip Theorem for periodic function on discrete sets. *}
   9.441 +
   9.442  lemma pinf_vee:
   9.443    assumes dpos: "0 < (d::int)" and modd: "ALL (x::int) (k::int). P x = P (x+k*d)"
   9.444    shows "(EX x::int. P x) = (EX (j::int) : {1..d} . P j)"
   9.445 @@ -750,7 +752,7 @@
   9.446  apply(blast dest:decr_mult_lemma)
   9.447  done
   9.448  
   9.449 -(* Cooper Thm `, plus infinity version*)
   9.450 +text {* Cooper Theorem, plus infinity version. *}
   9.451  lemma cppi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. z < x --> (P x = P1 x))
   9.452  ==> ALL x.~(EX (j::int) : {1..D}. EX (a::int) : A. P(a - j)) --> P (x) --> P (x + D) 
   9.453  ==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x+k*D))))
   9.454 @@ -774,9 +776,8 @@
   9.455    done
   9.456  
   9.457  
   9.458 -(*=============================================================================*)
   9.459 -
   9.460 -(*Theorems for the quantifier elminination Functions.*)
   9.461 +text {*
   9.462 +  \bigskip Theorems for the quantifier elminination Functions. *}
   9.463  
   9.464  lemma qe_ex_conj: "(EX (x::int). A x) = R
   9.465  		==> (EX (x::int). P x) = (Q & (EX x::int. A x))
   9.466 @@ -805,7 +806,7 @@
   9.467  lemma qe_ALL: "(EX x. ~P x) = R ==> (ALL x. P x) = (~R)"
   9.468  by blast
   9.469  
   9.470 -(* Theorems for proving NNF *)
   9.471 +text {* \bigskip Theorems for proving NNF *}
   9.472  
   9.473  lemma nnf_im: "((~P) = P1) ==> (Q=Q1) ==> ((P --> Q) = (P1 | Q1))"
   9.474  by blast
   9.475 @@ -851,7 +852,7 @@
   9.476  apply(fastsimp)
   9.477  done
   9.478  
   9.479 -(* Theorems required for the adjustcoeffitienteq*)
   9.480 +text {* \bigskip Theorems required for the @{text adjustcoeffitienteq} *}
   9.481  
   9.482  lemma ac_dvd_eq: assumes not0: "0 ~= (k::int)"
   9.483  shows "((m::int) dvd (c*n+t)) = (k*m dvd ((k*c)*n+(k*t)))" (is "?P = ?Q")
   9.484 @@ -925,7 +926,7 @@
   9.485  lemma lf_dvd: "(l::int) = ll ==> (r::int) = lr ==> (l dvd r) =(ll dvd lr)"
   9.486  by simp
   9.487  
   9.488 -(* Theorems for transforming predicates on nat to predicates on int*)
   9.489 +text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*}
   9.490  
   9.491  theorem all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))"
   9.492    by (simp split add: split_nat)
   9.493 @@ -973,7 +974,9 @@
   9.494  
   9.495  theorem Suc_plus1: "Suc n = n + 1" by simp
   9.496  
   9.497 -(* specific instances of congruence rules, to prevent simplifier from looping *)
   9.498 +text {*
   9.499 +  \medskip Specific instances of congruence rules, to prevent
   9.500 +  simplifier from looping. *}
   9.501  
   9.502  theorem imp_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::nat) \<longrightarrow> P) = (0 <= x \<longrightarrow> P')"
   9.503    by simp
    10.1 --- a/src/HOL/SetInterval.thy	Fri Apr 16 04:06:52 2004 +0200
    10.2 +++ b/src/HOL/SetInterval.thy	Fri Apr 16 04:07:10 2004 +0200
    10.3 @@ -7,6 +7,8 @@
    10.4  lessThan, greaterThan, atLeast, atMost and two-sided intervals
    10.5  *)
    10.6  
    10.7 +header {* Set intervals *}
    10.8 +
    10.9  theory SetInterval = IntArith:
   10.10  
   10.11  constdefs
   10.12 @@ -145,33 +147,33 @@
   10.13  
   10.14  subsection {*Two-sided intervals*}
   10.15  
   10.16 -(* greaterThanLessThan *)
   10.17 +text {* @{text greaterThanLessThan} *}
   10.18  
   10.19  lemma greaterThanLessThan_iff [simp]:
   10.20    "(i : {)l..u(}) = (l < i & i < u)"
   10.21  by (simp add: greaterThanLessThan_def)
   10.22  
   10.23 -(* atLeastLessThan *)
   10.24 +text {* @{text atLeastLessThan} *}
   10.25  
   10.26  lemma atLeastLessThan_iff [simp]:
   10.27    "(i : {l..u(}) = (l <= i & i < u)"
   10.28  by (simp add: atLeastLessThan_def)
   10.29  
   10.30 -(* greaterThanAtMost *)
   10.31 +text {* @{text greaterThanAtMost} *}
   10.32  
   10.33  lemma greaterThanAtMost_iff [simp]:
   10.34    "(i : {)l..u}) = (l < i & i <= u)"
   10.35  by (simp add: greaterThanAtMost_def)
   10.36  
   10.37 -(* atLeastAtMost *)
   10.38 +text {* @{text atLeastAtMost} *}
   10.39  
   10.40  lemma atLeastAtMost_iff [simp]:
   10.41    "(i : {l..u}) = (l <= i & i <= u)"
   10.42  by (simp add: atLeastAtMost_def)
   10.43  
   10.44 -(* The above four lemmas could be declared as iffs.
   10.45 -   If we do so, a call to blast in Hyperreal/Star.ML, lemma STAR_Int
   10.46 -   seems to take forever (more than one hour). *)
   10.47 +text {* The above four lemmas could be declared as iffs.
   10.48 +  If we do so, a call to blast in Hyperreal/Star.ML, lemma @{text STAR_Int}
   10.49 +  seems to take forever (more than one hour). *}
   10.50  
   10.51  
   10.52  subsection {* Intervals of natural numbers *}
   10.53 @@ -227,7 +229,7 @@
   10.54  lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"
   10.55  by blast
   10.56  
   10.57 -(* Intervals of nats with Suc *)
   10.58 +text {* Intervals of nats with @{text Suc} *}
   10.59  
   10.60  lemma atLeastLessThanSuc_atLeastAtMost: "{l..Suc u(} = {l..u}"
   10.61    by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def)
   10.62 @@ -391,11 +393,11 @@
   10.63  
   10.64  subsection {*Lemmas useful with the summation operator setsum*}
   10.65  
   10.66 -(* For examples, see Algebra/poly/UnivPoly.thy *)
   10.67 +text {* For examples, see Algebra/poly/UnivPoly.thy *}
   10.68  
   10.69 -(** Disjoint Unions **)
   10.70 +subsubsection {* Disjoint Unions *}
   10.71  
   10.72 -(* Singletons and open intervals *)
   10.73 +text {* Singletons and open intervals *}
   10.74  
   10.75  lemma ivl_disj_un_singleton:
   10.76    "{l::'a::linorder} Un {)l..} = {l..}"
   10.77 @@ -406,7 +408,7 @@
   10.78    "(l::'a::linorder) <= u ==> {l..u(} Un {u} = {l..u}"
   10.79  by auto
   10.80  
   10.81 -(* One- and two-sided intervals *)
   10.82 +text {* One- and two-sided intervals *}
   10.83  
   10.84  lemma ivl_disj_un_one:
   10.85    "(l::'a::linorder) < u ==> {..l} Un {)l..u(} = {..u(}"
   10.86 @@ -419,7 +421,7 @@
   10.87    "(l::'a::linorder) <= u ==> {l..u(} Un {u..} = {l..}"
   10.88  by auto
   10.89  
   10.90 -(* Two- and two-sided intervals *)
   10.91 +text {* Two- and two-sided intervals *}
   10.92  
   10.93  lemma ivl_disj_un_two:
   10.94    "[| (l::'a::linorder) < m; m <= u |] ==> {)l..m(} Un {m..u(} = {)l..u(}"
   10.95 @@ -434,9 +436,9 @@
   10.96  
   10.97  lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two
   10.98  
   10.99 -(** Disjoint Intersections **)
  10.100 +subsubsection {* Disjoint Intersections *}
  10.101  
  10.102 -(* Singletons and open intervals *)
  10.103 +text {* Singletons and open intervals *}
  10.104  
  10.105  lemma ivl_disj_int_singleton:
  10.106    "{l::'a::order} Int {)l..} = {}"
  10.107 @@ -447,7 +449,7 @@
  10.108    "{l..u(} Int {u} = {}"
  10.109    by simp+
  10.110  
  10.111 -(* One- and two-sided intervals *)
  10.112 +text {* One- and two-sided intervals *}
  10.113  
  10.114  lemma ivl_disj_int_one:
  10.115    "{..l::'a::order} Int {)l..u(} = {}"
  10.116 @@ -460,7 +462,7 @@
  10.117    "{l..u(} Int {u..} = {}"
  10.118    by auto
  10.119  
  10.120 -(* Two- and two-sided intervals *)
  10.121 +text {* Two- and two-sided intervals *}
  10.122  
  10.123  lemma ivl_disj_int_two:
  10.124    "{)l::'a::order..m(} Int {m..u(} = {}"