--- a/src/HOL/Algebra/CRing.thy Fri Apr 16 04:06:52 2004 +0200
+++ b/src/HOL/Algebra/CRing.thy Fri Apr 16 04:07:10 2004 +0200
@@ -5,11 +5,11 @@
Copyright: Clemens Ballarin
*)
+header {* Abelian Groups *}
+
theory CRing = FiniteProduct
files ("ringsimp.ML"):
-section {* Abelian Groups *}
-
record 'a ring = "'a monoid" +
zero :: 'a ("\<zero>\<index>")
add :: "['a, 'a] => 'a" (infixl "\<oplus>\<index>" 65)
--- a/src/HOL/Algebra/Lattice.thy Fri Apr 16 04:06:52 2004 +0200
+++ b/src/HOL/Algebra/Lattice.thy Fri Apr 16 04:07:10 2004 +0200
@@ -5,9 +5,9 @@
Copyright: Clemens Ballarin
*)
-theory Lattice = Group:
+header {* Order and Lattices *}
-section {* Order and Lattices *}
+theory Lattice = Group:
subsection {* Partial Orders *}
--- a/src/HOL/Algebra/Module.thy Fri Apr 16 04:06:52 2004 +0200
+++ b/src/HOL/Algebra/Module.thy Fri Apr 16 04:07:10 2004 +0200
@@ -4,9 +4,9 @@
Copyright: Clemens Ballarin
*)
-theory Module = CRing:
+header {* Modules over an Abelian Group *}
-section {* Modules over an Abelian Group *}
+theory Module = CRing:
record ('a, 'b) module = "'b ring" +
smult :: "['a, 'b] => 'b" (infixl "\<odot>\<index>" 70)
--- a/src/HOL/Algebra/UnivPoly.thy Fri Apr 16 04:06:52 2004 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy Fri Apr 16 04:07:10 2004 +0200
@@ -5,9 +5,9 @@
Copyright: Clemens Ballarin
*)
-theory UnivPoly = Module:
+header {* Univariate Polynomials *}
-section {* Univariate Polynomials *}
+theory UnivPoly = Module:
text {*
Polynomials are formalised as modules with additional operations for
--- a/src/HOL/Integ/NatSimprocs.thy Fri Apr 16 04:06:52 2004 +0200
+++ b/src/HOL/Integ/NatSimprocs.thy Fri Apr 16 04:07:10 2004 +0200
@@ -17,8 +17,9 @@
lemma Suc_diff_eq_diff_pred: "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)"
by (simp add: numeral_0_eq_0 numeral_1_eq_1 split add: nat_diff_split)
-(*Now just instantiating n to (number_of v) does the right simplification,
- but with some redundant inequality tests.*)
+text {*Now just instantiating @{text n} to @{text "number_of v"} does
+ the right simplification, but with some redundant inequality
+ tests.*}
lemma neg_number_of_bin_pred_iff_0:
"neg (number_of (bin_pred v)::int) = (number_of v = (0::nat))"
apply (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < Suc 0) ")
@@ -171,8 +172,9 @@
declare zero_le_divide_iff [of "number_of w", standard, simp]
declare divide_le_0_iff [of "number_of w", standard, simp]
-(*Replaces "inverse #nn" by 1/#nn. It looks strange, but then other simprocs
-simplify the quotient.*)
+text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}. It looks
+ strange, but then other simprocs simplify the quotient.*}
+
declare inverse_eq_divide [of "number_of w", standard, simp]
text{*These laws simplify inequalities, moving unary minus from a term
@@ -194,16 +196,14 @@
declare minus_le_iff [of _ 1, simplified, simp]
declare minus_equation_iff [of _ 1, simplified, simp]
-
-(*Cancellation of constant factors in comparisons (< and \<le>) *)
+text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
declare mult_less_cancel_left [of "number_of v", standard, simp]
declare mult_less_cancel_right [of _ "number_of v", standard, simp]
declare mult_le_cancel_left [of "number_of v", standard, simp]
declare mult_le_cancel_right [of _ "number_of v", standard, simp]
-
-(*Multiplying out constant divisors in comparisons (< \<le> and =) *)
+text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *}
declare le_divide_eq [of _ _ "number_of w", standard, simp]
declare divide_le_eq [of _ "number_of w", standard, simp]
--- a/src/HOL/Integ/Presburger.thy Fri Apr 16 04:06:52 2004 +0200
+++ b/src/HOL/Integ/Presburger.thy Fri Apr 16 04:07:10 2004 +0200
@@ -7,6 +7,8 @@
generation for Cooper Algorithm
*)
+header {* Presburger Arithmetic: Cooper Algorithm *}
+
theory Presburger = NatSimprocs + SetInterval
files
("cooper_dec.ML")
@@ -14,7 +16,7 @@
("qelim.ML")
("presburger.ML"):
-(* Theorem for unitifying the coeffitients of x in an existential formula*)
+text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*}
theorem unity_coeff_ex: "(\<exists>x::int. P (l * x)) = (\<exists>x. l dvd (1*x+0) \<and> P x)"
apply (rule iffI)
@@ -54,7 +56,7 @@
-(*Theorems for the combination of proofs of the equality of P and P_m for integers x less than some integer z.*)
+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}.*}
theorem eq_minf_conjI: "\<exists>z1::int. \<forall>x. x < z1 \<longrightarrow> (A1 x = A2 x) \<Longrightarrow>
\<exists>z2::int. \<forall>x. x < z2 \<longrightarrow> (B1 x = B2 x) \<Longrightarrow>
@@ -75,7 +77,7 @@
done
-(*Theorems for the combination of proofs of the equality of P and P_m for integers x greather than some integer z.*)
+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}.*}
theorem eq_pinf_conjI: "\<exists>z1::int. \<forall>x. z1 < x \<longrightarrow> (A1 x = A2 x) \<Longrightarrow>
\<exists>z2::int. \<forall>x. z2 < x \<longrightarrow> (B1 x = B2 x) \<Longrightarrow>
@@ -93,75 +95,76 @@
apply (rule_tac x = "max z1 z2" in exI)
apply simp
done
-(*=============================================================================*)
-(*Theorems for the combination of proofs of the modulo D property for P
-pluusinfinity*)
-(* 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*)
+
+text {*
+ \medskip Theorems for the combination of proofs of the modulo @{text
+ D} property for @{text "P plusinfinity"}
+
+ FIXME: This is THE SAME theorem as for the @{text minusinf} version,
+ but with @{text "+k.."} instead of @{text "-k.."} In the future
+ replace these both with only one. *}
theorem modd_pinf_conjI: "\<forall>(x::int) k. A x = A (x+k*d) \<Longrightarrow>
\<forall>(x::int) k. B x = B (x+k*d) \<Longrightarrow>
\<forall>(x::int) (k::int). (A x \<and> B x) = (A (x+k*d) \<and> B (x+k*d))"
by simp
-
theorem modd_pinf_disjI: "\<forall>(x::int) k. A x = A (x+k*d) \<Longrightarrow>
\<forall>(x::int) k. B x = B (x+k*d) \<Longrightarrow>
\<forall>(x::int) (k::int). (A x \<or> B x) = (A (x+k*d) \<or> B (x+k*d))"
by simp
-(*=============================================================================*)
-(*This is one of the cases where the simplifed formula is prooved to habe some property
-(in relation to P_m) but we need to proove the property for the original formula (P_m)*)
-(*FIXME : This is exaclty the same thm as for minusinf.*)
+text {*
+ This is one of the cases where the simplifed formula is prooved to
+ habe some property (in relation to @{text P_m}) but we need to prove
+ the property for the original formula (@{text P_m})
+
+ FIXME: This is exaclty the same thm as for @{text minusinf}. *}
+
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)) "
-by blast
+ by blast
-
-(*=============================================================================*)
-(*Theorems for the combination of proofs of the modulo D property for P
-minusinfinity*)
+text {*
+ \medskip Theorems for the combination of proofs of the modulo @{text D}
+ property for @{text "P minusinfinity"} *}
theorem modd_minf_conjI: "\<forall>(x::int) k. A x = A (x-k*d) \<Longrightarrow>
\<forall>(x::int) k. B x = B (x-k*d) \<Longrightarrow>
\<forall>(x::int) (k::int). (A x \<and> B x) = (A (x-k*d) \<and> B (x-k*d))"
by simp
-
theorem modd_minf_disjI: "\<forall>(x::int) k. A x = A (x-k*d) \<Longrightarrow>
\<forall>(x::int) k. B x = B (x-k*d) \<Longrightarrow>
\<forall>(x::int) (k::int). (A x \<or> B x) = (A (x-k*d) \<or> B (x-k*d))"
by simp
-(*=============================================================================*)
-(*This is one of the cases where the simplifed formula is prooved to habe some property
-(in relation to P_m) but we need to proove the property for the original formula (P_m)*)
+text {*
+ This is one of the cases where the simplifed formula is prooved to
+ have some property (in relation to @{text P_m}) but we need to
+ prove the property for the original formula (@{text P_m}). *}
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)) "
-by blast
+ by blast
-(*=============================================================================*)
-
-(*theorem needed for prooving at runtime divide properties using the arithmetic tatic
-(who knows only about modulo = 0)*)
+text {*
+ Theorem needed for proving at runtime divide properties using the
+ arithmetic tactic (which knows only about modulo = 0). *}
lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
-by(simp add:dvd_def zmod_eq_0_iff)
-
-(*=============================================================================*)
+ by(simp add:dvd_def zmod_eq_0_iff)
-
-
-(*Theorems used for the combination of proof for the backwards direction of cooper's
-theorem. they rely exclusively on Predicate calculus.*)
+text {*
+ \medskip Theorems used for the combination of proof for the
+ backwards direction of Cooper's Theorem. They rely exclusively on
+ Predicate calculus.*}
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))
==>
(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> P2(x) --> P2(x + d))
==>
(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))) "
-by blast
-
+ by blast
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))
@@ -170,18 +173,18 @@
==>
(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)
\<and> P2(x + d))) "
-by blast
+ by blast
lemma not_ast_p_Q_elim: "
(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) -->P(x) --> P(x + d))
==> ( P = Q )
==> (ALL x. ~(EX (j::int) : {1..d}. EX (a::int) : A. P(a - j)) -->P(x) --> P(x + d))"
-by blast
-(*=============================================================================*)
+ by blast
-
-(*Theorems used for the combination of proof for the backwards direction of cooper's
-theorem. they rely exclusively on Predicate calculus.*)
+text {*
+ \medskip Theorems used for the combination of proof for the
+ backwards direction of Cooper's Theorem. They rely exclusively on
+ Predicate calculus.*}
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))
==>
@@ -189,9 +192,7 @@
==>
(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)
\<or> P2(x-d))) "
-by blast
-
-
+ by blast
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))
==>
@@ -199,68 +200,67 @@
==>
(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)
\<and> P2(x-d))) "
-by blast
+ by blast
lemma not_bst_p_Q_elim: "
(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) -->P(x) --> P(x - d))
==> ( P = Q )
==> (ALL x. ~(EX (j::int) : {1..d}. EX (b::int) : B. P(b+j)) -->P(x) --> P(x - d))"
-by blast
-(*=============================================================================*)
+ by blast
-(*This is the first direction of cooper's theorem*)
+text {* \medskip This is the first direction of Cooper's Theorem. *}
lemma cooper_thm: "(R --> (EX x::int. P x)) ==> (Q -->(EX x::int. P x )) ==> ((R|Q) --> (EX x::int. P x )) "
-by blast
+ by blast
-(*=============================================================================*)
-(*The full cooper's theoorem in its equivalence Form- Given the premisses it is trivial
-too, it relies exclusively on prediacte calculus.*)
+text {*
+ \medskip The full Cooper's Theorem in its equivalence Form. Given
+ the premises it is trivial too, it relies exclusively on prediacte calculus.*}
lemma cooper_eq_thm: "(R --> (EX x::int. P x)) ==> (Q -->(EX x::int. P x )) ==> ((~Q)
--> (EX x::int. P x ) --> R) ==> (EX x::int. P x) = R|Q "
-by blast
+ by blast
-(*=============================================================================*)
-(*Some of the atomic theorems generated each time the atom does not depend on x, they
-are trivial.*)
+text {*
+ \medskip Some of the atomic theorems generated each time the atom
+ does not depend on @{text x}, they are trivial.*}
lemma fm_eq_minf: "EX z::int. ALL x. x < z --> (P = P) "
-by blast
+ by blast
lemma fm_modd_minf: "ALL (x::int). ALL (k::int). (P = P)"
-by blast
+ by blast
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"
-by blast
-
-
+ by blast
lemma fm_eq_pinf: "EX z::int. ALL x. z < x --> (P = P) "
-by blast
+ by blast
-(* The next 2 thms are the same as the minusinf version*)
+text {* The next two thms are the same as the @{text minusinf} version. *}
+
lemma fm_modd_pinf: "ALL (x::int). ALL (k::int). (P = P)"
-by blast
+ by blast
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"
-by blast
+ by blast
+text {* Theorems to be deleted from simpset when proving simplified formulaes. *}
-(* Theorems to be deleted from simpset when proving simplified formulaes*)
lemma P_eqtrue: "(P=True) = P"
by rules
lemma P_eqfalse: "(P=False) = (~P)"
by rules
-(*=============================================================================*)
+text {*
+ \medskip Theorems for the generation of the bachwards direction of
+ Cooper's Theorem.
-(*Theorems for the generation of the bachwards direction of cooper's theorem*)
-(*These are the 6 interesting atomic cases which have to be proved relying on the
-properties of B-set ant the arithmetic and contradiction proofs*)
+ These are the 6 interesting atomic cases which have to be proved relying on the
+ properties of B-set and the arithmetic and contradiction proofs. *}
lemma not_bst_p_lt: "0 < (d::int) ==>
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 )"
-by arith
+ by arith
lemma not_bst_p_gt: "\<lbrakk> (g::int) \<in> B; g = -a \<rbrakk> \<Longrightarrow>
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)"
@@ -315,16 +315,17 @@
apply(simp add:int_distrib)
done
-
+text {*
+ \medskip Theorems for the generation of the bachwards direction of
+ Cooper's Theorem.
-(*Theorems for the generation of the bachwards direction of cooper's theorem*)
-(*These are the 6 interesting atomic cases which have to be proved relying on the
-properties of A-set ant the arithmetic and contradiction proofs*)
+ These are the 6 interesting atomic cases which have to be proved
+ relying on the properties of A-set ant the arithmetic and
+ contradiction proofs. *}
lemma not_ast_p_gt: "0 < (d::int) ==>
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 )"
-by arith
-
+ by arith
lemma not_ast_p_lt: "\<lbrakk>0 < d ;(t::int) \<in> A \<rbrakk> \<Longrightarrow>
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)"
@@ -377,12 +378,11 @@
apply(simp add:int_distrib)
done
-
+text {*
+ \medskip These are the atomic cases for the proof generation for the
+ modulo @{text D} property for @{text "P plusinfinity"}
-(*=============================================================================*)
-(*These are the atomic cases for the proof generation for the modulo D property for P
-plusinfinity*)
-(*They are fully based on arithmetics*)
+ They are fully based on arithmetics. *}
lemma dvd_modd_pinf: "((d::int) dvd d1) ==>
(ALL (x::int). ALL (k::int). (((d::int) dvd (x + t)) = (d dvd (x+k*d1 + t))))"
@@ -412,10 +412,12 @@
apply(simp add:int_distrib mult_ac)
done
-(*=============================================================================*)
-(*These are the atomic cases for the proof generation for the equivalence of P and P
-plusinfinity for integers x greather than some integer z.*)
-(*They are fully based on arithmetics*)
+text {*
+ \medskip These are the atomic cases for the proof generation for the
+ equivalence of @{text P} and @{text "P plusinfinity"} for integers
+ @{text x} greater than some integer @{text z}.
+
+ They are fully based on arithmetics. *}
lemma eq_eq_pinf: "EX z::int. ALL x. z < x --> (( 0 = x +t ) = False )"
apply(rule_tac x = "-t" in exI)
@@ -438,18 +440,16 @@
done
lemma dvd_eq_pinf: "EX z::int. ALL x. z < x --> ((d dvd (x + t)) = (d dvd (x + t))) "
-by simp
+ by simp
lemma not_dvd_eq_pinf: "EX z::int. ALL x. z < x --> ((~(d dvd (x + t))) = (~(d dvd (x + t)))) "
-by simp
-
-
-
+ by simp
-(*=============================================================================*)
-(*These are the atomic cases for the proof generation for the modulo D property for P
-minusinfinity*)
-(*They are fully based on arithmetics*)
+text {*
+ \medskip These are the atomic cases for the proof generation for the
+ modulo @{text D} property for @{text "P minusinfinity"}.
+
+ They are fully based on arithmetics. *}
lemma dvd_modd_minf: "((d::int) dvd d1) ==>
(ALL (x::int). ALL (k::int). (((d::int) dvd (x + t)) = (d dvd (x-k*d1 + t))))"
@@ -480,11 +480,12 @@
apply(simp add:int_distrib mult_ac)
done
+text {*
+ \medskip These are the atomic cases for the proof generation for the
+ equivalence of @{text P} and @{text "P minusinfinity"} for integers
+ @{text x} less than some integer @{text z}.
-(*=============================================================================*)
-(*These are the atomic cases for the proof generation for the equivalence of P and P
-minusinfinity for integers x less than some integer z.*)
-(*They are fully based on arithmetics*)
+ They are fully based on arithmetics. *}
lemma eq_eq_minf: "EX z::int. ALL x. x < z --> (( 0 = x +t ) = False )"
apply(rule_tac x = "-t" in exI)
@@ -508,17 +509,18 @@
done
lemma dvd_eq_minf: "EX z::int. ALL x. x < z --> ((d dvd (x + t)) = (d dvd (x + t))) "
-by simp
+ by simp
lemma not_dvd_eq_minf: "EX z::int. ALL x. x < z --> ((~(d dvd (x + t))) = (~(d dvd (x + t)))) "
-by simp
-
+ by simp
-(*=============================================================================*)
-(*This Theorem combines whithnesses about P minusinfinity to schow one component of the
-equivalence proof for cooper's theorem*)
+text {*
+ \medskip This Theorem combines whithnesses about @{text "P
+ minusinfinity"} to show one component of the equivalence proof for
+ Cooper's Theorem.
-(* FIXME: remove once they are part of the distribution *)
+ FIXME: remove once they are part of the distribution. *}
+
theorem int_ge_induct[consumes 1,case_names base step]:
assumes ge: "k \<le> (i::int)" and
base: "P(k)" and
@@ -590,9 +592,10 @@
qed
qed
-(*=============================================================================*)
-(*This Theorem combines whithnesses about P minusinfinity to schow one component of the
-equivalence proof for cooper's theorem*)
+text {*
+ \medskip This Theorem combines whithnesses about @{text "P
+ minusinfinity"} to show one component of the equivalence proof for
+ Cooper's Theorem. *}
lemma plusinfinity:
assumes "0 < d" and
@@ -613,10 +616,8 @@
qed
qed
-
-
-(*=============================================================================*)
-(*Theorem for periodic function on discrete sets*)
+text {*
+ \medskip Theorem for periodic function on discrete sets. *}
lemma minf_vee:
assumes dpos: "(0::int) < d" and modd: "ALL x k. P x = P(x - k*d)"
@@ -651,8 +652,9 @@
assume ?RHS thus ?LHS by blast
qed
-(*=============================================================================*)
-(*Theorem for periodic function on discrete sets*)
+text {*
+ \medskip Theorem for periodic function on discrete sets. *}
+
lemma pinf_vee:
assumes dpos: "0 < (d::int)" and modd: "ALL (x::int) (k::int). P x = P (x+k*d)"
shows "(EX x::int. P x) = (EX (j::int) : {1..d} . P j)"
@@ -750,7 +752,7 @@
apply(blast dest:decr_mult_lemma)
done
-(* Cooper Thm `, plus infinity version*)
+text {* Cooper Theorem, plus infinity version. *}
lemma cppi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. z < x --> (P x = P1 x))
==> ALL x.~(EX (j::int) : {1..D}. EX (a::int) : A. P(a - j)) --> P (x) --> P (x + D)
==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x+k*D))))
@@ -774,9 +776,8 @@
done
-(*=============================================================================*)
-
-(*Theorems for the quantifier elminination Functions.*)
+text {*
+ \bigskip Theorems for the quantifier elminination Functions. *}
lemma qe_ex_conj: "(EX (x::int). A x) = R
==> (EX (x::int). P x) = (Q & (EX x::int. A x))
@@ -805,7 +806,7 @@
lemma qe_ALL: "(EX x. ~P x) = R ==> (ALL x. P x) = (~R)"
by blast
-(* Theorems for proving NNF *)
+text {* \bigskip Theorems for proving NNF *}
lemma nnf_im: "((~P) = P1) ==> (Q=Q1) ==> ((P --> Q) = (P1 | Q1))"
by blast
@@ -851,7 +852,7 @@
apply(fastsimp)
done
-(* Theorems required for the adjustcoeffitienteq*)
+text {* \bigskip Theorems required for the @{text adjustcoeffitienteq} *}
lemma ac_dvd_eq: assumes not0: "0 ~= (k::int)"
shows "((m::int) dvd (c*n+t)) = (k*m dvd ((k*c)*n+(k*t)))" (is "?P = ?Q")
@@ -925,7 +926,7 @@
lemma lf_dvd: "(l::int) = ll ==> (r::int) = lr ==> (l dvd r) =(ll dvd lr)"
by simp
-(* Theorems for transforming predicates on nat to predicates on int*)
+text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*}
theorem all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))"
by (simp split add: split_nat)
@@ -973,7 +974,9 @@
theorem Suc_plus1: "Suc n = n + 1" by simp
-(* specific instances of congruence rules, to prevent simplifier from looping *)
+text {*
+ \medskip Specific instances of congruence rules, to prevent
+ simplifier from looping. *}
theorem imp_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::nat) \<longrightarrow> P) = (0 <= x \<longrightarrow> P')"
by simp
--- a/src/HOL/Power.thy Fri Apr 16 04:06:52 2004 +0200
+++ b/src/HOL/Power.thy Fri Apr 16 04:07:10 2004 +0200
@@ -24,7 +24,7 @@
lemma power_one [simp]: "1^n = (1::'a::ringpower)"
apply (induct_tac "n")
-apply (auto simp add: power_Suc)
+apply (auto simp add: power_Suc)
done
lemma power_one_right [simp]: "(a::'a::ringpower) ^ 1 = a"
@@ -41,7 +41,7 @@
done
lemma power_mult_distrib: "((a::'a::ringpower) * b) ^ n = (a^n) * (b^n)"
-apply (induct_tac "n")
+apply (induct_tac "n")
apply (auto simp add: power_Suc mult_ac)
done
@@ -54,7 +54,7 @@
lemma zero_le_power:
"0 \<le> (a::'a::{ordered_semiring,ringpower}) ==> 0 \<le> a^n"
apply (simp add: order_le_less)
-apply (erule disjE)
+apply (erule disjE)
apply (simp_all add: zero_less_power zero_less_one power_0_left)
done
@@ -62,25 +62,22 @@
"1 \<le> (a::'a::{ordered_semiring,ringpower}) ==> 1 \<le> a^n"
apply (induct_tac "n")
apply (simp_all add: power_Suc)
-apply (rule order_trans [OF _ mult_mono [of 1 _ 1]])
-apply (simp_all add: zero_le_one order_trans [OF zero_le_one])
+apply (rule order_trans [OF _ mult_mono [of 1 _ 1]])
+apply (simp_all add: zero_le_one order_trans [OF zero_le_one])
done
lemma gt1_imp_ge0: "1 < a ==> 0 \<le> (a::'a::ordered_semiring)"
by (simp add: order_trans [OF zero_le_one order_less_imp_le])
lemma power_gt1_lemma:
- assumes gt1: "1 < (a::'a::{ordered_semiring,ringpower})"
- shows "1 < a * a^n"
+ assumes gt1: "1 < (a::'a::{ordered_semiring,ringpower})"
+ shows "1 < a * a^n"
proof -
- have "1*1 < a * a^n"
- proof (rule order_less_le_trans)
- show "1*1 < a*1" by (simp add: gt1)
- show "a*1 \<le> a * a^n"
- by (simp only: mult_mono gt1 gt1_imp_ge0 one_le_power order_less_imp_le
- zero_le_one order_refl)
- qed
- thus ?thesis by simp
+ have "1*1 < a*1" using gt1 by simp
+ also have "\<dots> \<le> a * a^n" using gt1
+ by (simp only: mult_mono gt1_imp_ge0 one_le_power order_less_imp_le
+ zero_le_one order_refl)
+ finally show ?thesis by simp
qed
lemma power_gt1:
@@ -88,52 +85,52 @@
by (simp add: power_gt1_lemma power_Suc)
lemma power_le_imp_le_exp:
- assumes gt1: "(1::'a::{ringpower,ordered_semiring}) < a"
- shows "!!n. a^m \<le> a^n ==> m \<le> n"
-proof (induct "m")
+ assumes gt1: "(1::'a::{ringpower,ordered_semiring}) < a"
+ shows "!!n. a^m \<le> a^n ==> m \<le> n"
+proof (induct m)
case 0
- show ?case by simp
+ show ?case by simp
next
case (Suc m)
- show ?case
- proof (cases n)
- case 0
- from prems have "a * a^m \<le> 1" by (simp add: power_Suc)
- with gt1 show ?thesis
- by (force simp only: power_gt1_lemma
- linorder_not_less [symmetric])
- next
- case (Suc n)
- from prems show ?thesis
- by (force dest: mult_left_le_imp_le
- simp add: power_Suc order_less_trans [OF zero_less_one gt1])
- qed
+ show ?case
+ proof (cases n)
+ case 0
+ from prems have "a * a^m \<le> 1" by (simp add: power_Suc)
+ with gt1 show ?thesis
+ by (force simp only: power_gt1_lemma
+ linorder_not_less [symmetric])
+ next
+ case (Suc n)
+ from prems show ?thesis
+ by (force dest: mult_left_le_imp_le
+ simp add: power_Suc order_less_trans [OF zero_less_one gt1])
+ qed
qed
-text{*Surely we can strengthen this? It holds for 0<a<1 too.*}
+text{*Surely we can strengthen this? It holds for @{text "0<a<1"} too.*}
lemma power_inject_exp [simp]:
"1 < (a::'a::{ordered_semiring,ringpower}) ==> (a^m = a^n) = (m=n)"
- by (force simp add: order_antisym power_le_imp_le_exp)
+ by (force simp add: order_antisym power_le_imp_le_exp)
text{*Can relax the first premise to @{term "0<a"} in the case of the
natural numbers.*}
lemma power_less_imp_less_exp:
"[| (1::'a::{ringpower,ordered_semiring}) < a; a^m < a^n |] ==> m < n"
-by (simp add: order_less_le [of m n] order_less_le [of "a^m" "a^n"]
- power_le_imp_le_exp)
+by (simp add: order_less_le [of m n] order_less_le [of "a^m" "a^n"]
+ power_le_imp_le_exp)
lemma power_mono:
"[|a \<le> b; (0::'a::{ringpower,ordered_semiring}) \<le> a|] ==> a^n \<le> b^n"
-apply (induct_tac "n")
+apply (induct_tac "n")
apply (simp_all add: power_Suc)
apply (auto intro: mult_mono zero_le_power order_trans [of 0 a b])
done
lemma power_strict_mono [rule_format]:
- "[|a < b; (0::'a::{ringpower,ordered_semiring}) \<le> a|]
- ==> 0 < n --> a^n < b^n"
-apply (induct_tac "n")
+ "[|a < b; (0::'a::{ringpower,ordered_semiring}) \<le> a|]
+ ==> 0 < n --> a^n < b^n"
+apply (induct_tac "n")
apply (auto simp add: mult_strict_mono zero_le_power power_Suc
order_le_less_trans [of 0 a b])
done
@@ -166,15 +163,15 @@
apply (auto simp add: power_Suc inverse_mult_distrib)
done
-lemma nonzero_power_divide:
+lemma nonzero_power_divide:
"b \<noteq> 0 ==> (a/b) ^ n = ((a::'a::{field,ringpower}) ^ n) / (b ^ n)"
by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse)
-lemma power_divide:
+lemma power_divide:
"(a/b) ^ n = ((a::'a::{field,division_by_zero,ringpower}) ^ n / b ^ n)"
apply (case_tac "b=0", simp add: power_0_left)
-apply (rule nonzero_power_divide)
-apply assumption
+apply (rule nonzero_power_divide)
+apply assumption
done
lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_ring,ringpower}) ^ n"
@@ -183,7 +180,7 @@
done
lemma zero_less_power_abs_iff [simp]:
- "(0 < (abs a)^n) = (a \<noteq> (0::'a::{ordered_ring,ringpower}) | n=0)"
+ "(0 < (abs a)^n) = (a \<noteq> (0::'a::{ordered_ring,ringpower}) | n=0)"
proof (induct "n")
case 0
show ?case by (simp add: zero_less_one)
@@ -208,19 +205,19 @@
lemma power_Suc_less:
"[|(0::'a::{ordered_semiring,ringpower}) < a; a < 1|]
==> a * a^n < a^n"
-apply (induct_tac n)
-apply (auto simp add: power_Suc mult_strict_left_mono)
+apply (induct_tac n)
+apply (auto simp add: power_Suc mult_strict_left_mono)
done
lemma power_strict_decreasing:
"[|n < N; 0 < a; a < (1::'a::{ordered_semiring,ringpower})|]
==> a^N < a^n"
-apply (erule rev_mp)
-apply (induct_tac "N")
-apply (auto simp add: power_Suc power_Suc_less less_Suc_eq)
-apply (rename_tac m)
+apply (erule rev_mp)
+apply (induct_tac "N")
+apply (auto simp add: power_Suc power_Suc_less less_Suc_eq)
+apply (rename_tac m)
apply (subgoal_tac "a * a^m < 1 * a^n", simp)
-apply (rule mult_strict_mono)
+apply (rule mult_strict_mono)
apply (auto simp add: zero_le_power zero_less_one order_less_imp_le)
done
@@ -228,47 +225,47 @@
lemma power_decreasing:
"[|n \<le> N; 0 \<le> a; a \<le> (1::'a::{ordered_semiring,ringpower})|]
==> a^N \<le> a^n"
-apply (erule rev_mp)
-apply (induct_tac "N")
-apply (auto simp add: power_Suc le_Suc_eq)
-apply (rename_tac m)
+apply (erule rev_mp)
+apply (induct_tac "N")
+apply (auto simp add: power_Suc le_Suc_eq)
+apply (rename_tac m)
apply (subgoal_tac "a * a^m \<le> 1 * a^n", simp)
-apply (rule mult_mono)
+apply (rule mult_mono)
apply (auto simp add: zero_le_power zero_le_one)
done
lemma power_Suc_less_one:
"[| 0 < a; a < (1::'a::{ordered_semiring,ringpower}) |] ==> a ^ Suc n < 1"
-apply (insert power_strict_decreasing [of 0 "Suc n" a], simp)
+apply (insert power_strict_decreasing [of 0 "Suc n" a], simp)
done
text{*Proof again resembles that of @{text power_strict_decreasing}*}
lemma power_increasing:
"[|n \<le> N; (1::'a::{ordered_semiring,ringpower}) \<le> a|] ==> a^n \<le> a^N"
-apply (erule rev_mp)
-apply (induct_tac "N")
-apply (auto simp add: power_Suc le_Suc_eq)
+apply (erule rev_mp)
+apply (induct_tac "N")
+apply (auto simp add: power_Suc le_Suc_eq)
apply (rename_tac m)
apply (subgoal_tac "1 * a^n \<le> a * a^m", simp)
-apply (rule mult_mono)
+apply (rule mult_mono)
apply (auto simp add: order_trans [OF zero_le_one] zero_le_power)
done
text{*Lemma for @{text power_strict_increasing}*}
lemma power_less_power_Suc:
"(1::'a::{ordered_semiring,ringpower}) < a ==> a^n < a * a^n"
-apply (induct_tac n)
-apply (auto simp add: power_Suc mult_strict_left_mono order_less_trans [OF zero_less_one])
+apply (induct_tac n)
+apply (auto simp add: power_Suc mult_strict_left_mono order_less_trans [OF zero_less_one])
done
lemma power_strict_increasing:
"[|n < N; (1::'a::{ordered_semiring,ringpower}) < a|] ==> a^n < a^N"
-apply (erule rev_mp)
-apply (induct_tac "N")
-apply (auto simp add: power_less_power_Suc power_Suc less_Suc_eq)
+apply (erule rev_mp)
+apply (induct_tac "N")
+apply (auto simp add: power_less_power_Suc power_Suc less_Suc_eq)
apply (rename_tac m)
apply (subgoal_tac "1 * a^n < a * a^m", simp)
-apply (rule mult_strict_mono)
+apply (rule mult_strict_mono)
apply (auto simp add: order_less_trans [OF zero_less_one] zero_le_power
order_less_imp_le)
done
@@ -282,13 +279,13 @@
assume "~ a \<le> b"
then have "b < a" by (simp only: linorder_not_le)
then have "b ^ Suc n < a ^ Suc n"
- by (simp only: prems power_strict_mono)
+ by (simp only: prems power_strict_mono)
from le and this show "False"
by (simp add: linorder_not_less [symmetric])
qed
-
+
lemma power_inject_base:
- "[| a ^ Suc n = b ^ Suc n; 0 \<le> a; 0 \<le> b |]
+ "[| a ^ Suc n = b ^ Suc n; 0 \<le> a; 0 \<le> b |]
==> a = (b::'a::{ordered_semiring,ringpower})"
by (blast intro: power_le_imp_le_base order_antisym order_eq_refl sym)
@@ -298,7 +295,7 @@
primrec (power)
"p ^ 0 = 1"
"p ^ (Suc n) = (p::nat) * (p ^ n)"
-
+
instance nat :: ringpower
proof
fix z n :: nat
@@ -321,7 +318,7 @@
lemma nat_power_less_imp_less: "!!i::nat. [| 0 < i; i^m < i^n |] ==> m < n"
apply (rule ccontr)
apply (drule leI [THEN le_imp_power_dvd, THEN dvd_imp_le, THEN leD])
-apply (erule zero_less_power, auto)
+apply (erule zero_less_power, auto)
done
lemma nat_zero_less_power_iff [simp]: "(0 < x^n) = (x \<noteq> (0::nat) | n=0)"
@@ -341,7 +338,7 @@
subsection{*Binomial Coefficients*}
-text{*This development is based on the work of Andy Gordon and
+text{*This development is based on the work of Andy Gordon and
Florian Kammueller*}
consts
@@ -400,7 +397,7 @@
apply (induct_tac "n")
apply (simp add: binomial_0, clarify)
apply (case_tac "k")
-apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq
+apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq
binomial_eq_0)
done
@@ -408,7 +405,7 @@
need to reason about division.*}
lemma binomial_Suc_Suc_eq_times:
"k \<le> n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k"
-by (simp add: Suc_times_binomial_eq div_mult_self_is_m zero_less_Suc
+by (simp add: Suc_times_binomial_eq div_mult_self_is_m zero_less_Suc
del: mult_Suc mult_Suc_right)
text{*Another version, with -1 instead of Suc.*}
@@ -460,7 +457,7 @@
val power_le_imp_le_base = thm"power_le_imp_le_base";
val power_inject_base = thm"power_inject_base";
*}
-
+
text{*ML bindings for the remaining theorems*}
ML
{*
--- a/src/HOL/PreList.thy Fri Apr 16 04:06:52 2004 +0200
+++ b/src/HOL/PreList.thy Fri Apr 16 04:07:10 2004 +0200
@@ -6,13 +6,14 @@
header{*A Basis for Building the Theory of Lists*}
-(*Is defined separately to serve as a basis for theory ToyList in the
-documentation.*)
-
theory PreList =
Wellfounded_Relations + Presburger + Recdef + Relation_Power + Parity:
-(*belongs to theory Wellfounded_Recursion*)
+text {*
+ Is defined separately to serve as a basis for theory ToyList in the
+ documentation. *}
+
lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf]
+ -- {* belongs to theory @{text Wellfounded_Recursion} *}
end
--- a/src/HOL/Presburger.thy Fri Apr 16 04:06:52 2004 +0200
+++ b/src/HOL/Presburger.thy Fri Apr 16 04:07:10 2004 +0200
@@ -7,6 +7,8 @@
generation for Cooper Algorithm
*)
+header {* Presburger Arithmetic: Cooper Algorithm *}
+
theory Presburger = NatSimprocs + SetInterval
files
("cooper_dec.ML")
@@ -14,7 +16,7 @@
("qelim.ML")
("presburger.ML"):
-(* Theorem for unitifying the coeffitients of x in an existential formula*)
+text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*}
theorem unity_coeff_ex: "(\<exists>x::int. P (l * x)) = (\<exists>x. l dvd (1*x+0) \<and> P x)"
apply (rule iffI)
@@ -54,7 +56,7 @@
-(*Theorems for the combination of proofs of the equality of P and P_m for integers x less than some integer z.*)
+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}.*}
theorem eq_minf_conjI: "\<exists>z1::int. \<forall>x. x < z1 \<longrightarrow> (A1 x = A2 x) \<Longrightarrow>
\<exists>z2::int. \<forall>x. x < z2 \<longrightarrow> (B1 x = B2 x) \<Longrightarrow>
@@ -75,7 +77,7 @@
done
-(*Theorems for the combination of proofs of the equality of P and P_m for integers x greather than some integer z.*)
+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}.*}
theorem eq_pinf_conjI: "\<exists>z1::int. \<forall>x. z1 < x \<longrightarrow> (A1 x = A2 x) \<Longrightarrow>
\<exists>z2::int. \<forall>x. z2 < x \<longrightarrow> (B1 x = B2 x) \<Longrightarrow>
@@ -93,75 +95,76 @@
apply (rule_tac x = "max z1 z2" in exI)
apply simp
done
-(*=============================================================================*)
-(*Theorems for the combination of proofs of the modulo D property for P
-pluusinfinity*)
-(* 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*)
+
+text {*
+ \medskip Theorems for the combination of proofs of the modulo @{text
+ D} property for @{text "P plusinfinity"}
+
+ FIXME: This is THE SAME theorem as for the @{text minusinf} version,
+ but with @{text "+k.."} instead of @{text "-k.."} In the future
+ replace these both with only one. *}
theorem modd_pinf_conjI: "\<forall>(x::int) k. A x = A (x+k*d) \<Longrightarrow>
\<forall>(x::int) k. B x = B (x+k*d) \<Longrightarrow>
\<forall>(x::int) (k::int). (A x \<and> B x) = (A (x+k*d) \<and> B (x+k*d))"
by simp
-
theorem modd_pinf_disjI: "\<forall>(x::int) k. A x = A (x+k*d) \<Longrightarrow>
\<forall>(x::int) k. B x = B (x+k*d) \<Longrightarrow>
\<forall>(x::int) (k::int). (A x \<or> B x) = (A (x+k*d) \<or> B (x+k*d))"
by simp
-(*=============================================================================*)
-(*This is one of the cases where the simplifed formula is prooved to habe some property
-(in relation to P_m) but we need to proove the property for the original formula (P_m)*)
-(*FIXME : This is exaclty the same thm as for minusinf.*)
+text {*
+ This is one of the cases where the simplifed formula is prooved to
+ habe some property (in relation to @{text P_m}) but we need to prove
+ the property for the original formula (@{text P_m})
+
+ FIXME: This is exaclty the same thm as for @{text minusinf}. *}
+
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)) "
-by blast
+ by blast
-
-(*=============================================================================*)
-(*Theorems for the combination of proofs of the modulo D property for P
-minusinfinity*)
+text {*
+ \medskip Theorems for the combination of proofs of the modulo @{text D}
+ property for @{text "P minusinfinity"} *}
theorem modd_minf_conjI: "\<forall>(x::int) k. A x = A (x-k*d) \<Longrightarrow>
\<forall>(x::int) k. B x = B (x-k*d) \<Longrightarrow>
\<forall>(x::int) (k::int). (A x \<and> B x) = (A (x-k*d) \<and> B (x-k*d))"
by simp
-
theorem modd_minf_disjI: "\<forall>(x::int) k. A x = A (x-k*d) \<Longrightarrow>
\<forall>(x::int) k. B x = B (x-k*d) \<Longrightarrow>
\<forall>(x::int) (k::int). (A x \<or> B x) = (A (x-k*d) \<or> B (x-k*d))"
by simp
-(*=============================================================================*)
-(*This is one of the cases where the simplifed formula is prooved to habe some property
-(in relation to P_m) but we need to proove the property for the original formula (P_m)*)
+text {*
+ This is one of the cases where the simplifed formula is prooved to
+ have some property (in relation to @{text P_m}) but we need to
+ prove the property for the original formula (@{text P_m}). *}
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)) "
-by blast
+ by blast
-(*=============================================================================*)
-
-(*theorem needed for prooving at runtime divide properties using the arithmetic tatic
-(who knows only about modulo = 0)*)
+text {*
+ Theorem needed for proving at runtime divide properties using the
+ arithmetic tactic (which knows only about modulo = 0). *}
lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
-by(simp add:dvd_def zmod_eq_0_iff)
-
-(*=============================================================================*)
+ by(simp add:dvd_def zmod_eq_0_iff)
-
-
-(*Theorems used for the combination of proof for the backwards direction of cooper's
-theorem. they rely exclusively on Predicate calculus.*)
+text {*
+ \medskip Theorems used for the combination of proof for the
+ backwards direction of Cooper's Theorem. They rely exclusively on
+ Predicate calculus.*}
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))
==>
(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> P2(x) --> P2(x + d))
==>
(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))) "
-by blast
-
+ by blast
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))
@@ -170,18 +173,18 @@
==>
(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)
\<and> P2(x + d))) "
-by blast
+ by blast
lemma not_ast_p_Q_elim: "
(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) -->P(x) --> P(x + d))
==> ( P = Q )
==> (ALL x. ~(EX (j::int) : {1..d}. EX (a::int) : A. P(a - j)) -->P(x) --> P(x + d))"
-by blast
-(*=============================================================================*)
+ by blast
-
-(*Theorems used for the combination of proof for the backwards direction of cooper's
-theorem. they rely exclusively on Predicate calculus.*)
+text {*
+ \medskip Theorems used for the combination of proof for the
+ backwards direction of Cooper's Theorem. They rely exclusively on
+ Predicate calculus.*}
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))
==>
@@ -189,9 +192,7 @@
==>
(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)
\<or> P2(x-d))) "
-by blast
-
-
+ by blast
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))
==>
@@ -199,68 +200,67 @@
==>
(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)
\<and> P2(x-d))) "
-by blast
+ by blast
lemma not_bst_p_Q_elim: "
(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) -->P(x) --> P(x - d))
==> ( P = Q )
==> (ALL x. ~(EX (j::int) : {1..d}. EX (b::int) : B. P(b+j)) -->P(x) --> P(x - d))"
-by blast
-(*=============================================================================*)
+ by blast
-(*This is the first direction of cooper's theorem*)
+text {* \medskip This is the first direction of Cooper's Theorem. *}
lemma cooper_thm: "(R --> (EX x::int. P x)) ==> (Q -->(EX x::int. P x )) ==> ((R|Q) --> (EX x::int. P x )) "
-by blast
+ by blast
-(*=============================================================================*)
-(*The full cooper's theoorem in its equivalence Form- Given the premisses it is trivial
-too, it relies exclusively on prediacte calculus.*)
+text {*
+ \medskip The full Cooper's Theorem in its equivalence Form. Given
+ the premises it is trivial too, it relies exclusively on prediacte calculus.*}
lemma cooper_eq_thm: "(R --> (EX x::int. P x)) ==> (Q -->(EX x::int. P x )) ==> ((~Q)
--> (EX x::int. P x ) --> R) ==> (EX x::int. P x) = R|Q "
-by blast
+ by blast
-(*=============================================================================*)
-(*Some of the atomic theorems generated each time the atom does not depend on x, they
-are trivial.*)
+text {*
+ \medskip Some of the atomic theorems generated each time the atom
+ does not depend on @{text x}, they are trivial.*}
lemma fm_eq_minf: "EX z::int. ALL x. x < z --> (P = P) "
-by blast
+ by blast
lemma fm_modd_minf: "ALL (x::int). ALL (k::int). (P = P)"
-by blast
+ by blast
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"
-by blast
-
-
+ by blast
lemma fm_eq_pinf: "EX z::int. ALL x. z < x --> (P = P) "
-by blast
+ by blast
-(* The next 2 thms are the same as the minusinf version*)
+text {* The next two thms are the same as the @{text minusinf} version. *}
+
lemma fm_modd_pinf: "ALL (x::int). ALL (k::int). (P = P)"
-by blast
+ by blast
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"
-by blast
+ by blast
+text {* Theorems to be deleted from simpset when proving simplified formulaes. *}
-(* Theorems to be deleted from simpset when proving simplified formulaes*)
lemma P_eqtrue: "(P=True) = P"
by rules
lemma P_eqfalse: "(P=False) = (~P)"
by rules
-(*=============================================================================*)
+text {*
+ \medskip Theorems for the generation of the bachwards direction of
+ Cooper's Theorem.
-(*Theorems for the generation of the bachwards direction of cooper's theorem*)
-(*These are the 6 interesting atomic cases which have to be proved relying on the
-properties of B-set ant the arithmetic and contradiction proofs*)
+ These are the 6 interesting atomic cases which have to be proved relying on the
+ properties of B-set and the arithmetic and contradiction proofs. *}
lemma not_bst_p_lt: "0 < (d::int) ==>
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 )"
-by arith
+ by arith
lemma not_bst_p_gt: "\<lbrakk> (g::int) \<in> B; g = -a \<rbrakk> \<Longrightarrow>
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)"
@@ -315,16 +315,17 @@
apply(simp add:int_distrib)
done
-
+text {*
+ \medskip Theorems for the generation of the bachwards direction of
+ Cooper's Theorem.
-(*Theorems for the generation of the bachwards direction of cooper's theorem*)
-(*These are the 6 interesting atomic cases which have to be proved relying on the
-properties of A-set ant the arithmetic and contradiction proofs*)
+ These are the 6 interesting atomic cases which have to be proved
+ relying on the properties of A-set ant the arithmetic and
+ contradiction proofs. *}
lemma not_ast_p_gt: "0 < (d::int) ==>
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 )"
-by arith
-
+ by arith
lemma not_ast_p_lt: "\<lbrakk>0 < d ;(t::int) \<in> A \<rbrakk> \<Longrightarrow>
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)"
@@ -377,12 +378,11 @@
apply(simp add:int_distrib)
done
-
+text {*
+ \medskip These are the atomic cases for the proof generation for the
+ modulo @{text D} property for @{text "P plusinfinity"}
-(*=============================================================================*)
-(*These are the atomic cases for the proof generation for the modulo D property for P
-plusinfinity*)
-(*They are fully based on arithmetics*)
+ They are fully based on arithmetics. *}
lemma dvd_modd_pinf: "((d::int) dvd d1) ==>
(ALL (x::int). ALL (k::int). (((d::int) dvd (x + t)) = (d dvd (x+k*d1 + t))))"
@@ -412,10 +412,12 @@
apply(simp add:int_distrib mult_ac)
done
-(*=============================================================================*)
-(*These are the atomic cases for the proof generation for the equivalence of P and P
-plusinfinity for integers x greather than some integer z.*)
-(*They are fully based on arithmetics*)
+text {*
+ \medskip These are the atomic cases for the proof generation for the
+ equivalence of @{text P} and @{text "P plusinfinity"} for integers
+ @{text x} greater than some integer @{text z}.
+
+ They are fully based on arithmetics. *}
lemma eq_eq_pinf: "EX z::int. ALL x. z < x --> (( 0 = x +t ) = False )"
apply(rule_tac x = "-t" in exI)
@@ -438,18 +440,16 @@
done
lemma dvd_eq_pinf: "EX z::int. ALL x. z < x --> ((d dvd (x + t)) = (d dvd (x + t))) "
-by simp
+ by simp
lemma not_dvd_eq_pinf: "EX z::int. ALL x. z < x --> ((~(d dvd (x + t))) = (~(d dvd (x + t)))) "
-by simp
-
-
-
+ by simp
-(*=============================================================================*)
-(*These are the atomic cases for the proof generation for the modulo D property for P
-minusinfinity*)
-(*They are fully based on arithmetics*)
+text {*
+ \medskip These are the atomic cases for the proof generation for the
+ modulo @{text D} property for @{text "P minusinfinity"}.
+
+ They are fully based on arithmetics. *}
lemma dvd_modd_minf: "((d::int) dvd d1) ==>
(ALL (x::int). ALL (k::int). (((d::int) dvd (x + t)) = (d dvd (x-k*d1 + t))))"
@@ -480,11 +480,12 @@
apply(simp add:int_distrib mult_ac)
done
+text {*
+ \medskip These are the atomic cases for the proof generation for the
+ equivalence of @{text P} and @{text "P minusinfinity"} for integers
+ @{text x} less than some integer @{text z}.
-(*=============================================================================*)
-(*These are the atomic cases for the proof generation for the equivalence of P and P
-minusinfinity for integers x less than some integer z.*)
-(*They are fully based on arithmetics*)
+ They are fully based on arithmetics. *}
lemma eq_eq_minf: "EX z::int. ALL x. x < z --> (( 0 = x +t ) = False )"
apply(rule_tac x = "-t" in exI)
@@ -508,17 +509,18 @@
done
lemma dvd_eq_minf: "EX z::int. ALL x. x < z --> ((d dvd (x + t)) = (d dvd (x + t))) "
-by simp
+ by simp
lemma not_dvd_eq_minf: "EX z::int. ALL x. x < z --> ((~(d dvd (x + t))) = (~(d dvd (x + t)))) "
-by simp
-
+ by simp
-(*=============================================================================*)
-(*This Theorem combines whithnesses about P minusinfinity to schow one component of the
-equivalence proof for cooper's theorem*)
+text {*
+ \medskip This Theorem combines whithnesses about @{text "P
+ minusinfinity"} to show one component of the equivalence proof for
+ Cooper's Theorem.
-(* FIXME: remove once they are part of the distribution *)
+ FIXME: remove once they are part of the distribution. *}
+
theorem int_ge_induct[consumes 1,case_names base step]:
assumes ge: "k \<le> (i::int)" and
base: "P(k)" and
@@ -590,9 +592,10 @@
qed
qed
-(*=============================================================================*)
-(*This Theorem combines whithnesses about P minusinfinity to schow one component of the
-equivalence proof for cooper's theorem*)
+text {*
+ \medskip This Theorem combines whithnesses about @{text "P
+ minusinfinity"} to show one component of the equivalence proof for
+ Cooper's Theorem. *}
lemma plusinfinity:
assumes "0 < d" and
@@ -613,10 +616,8 @@
qed
qed
-
-
-(*=============================================================================*)
-(*Theorem for periodic function on discrete sets*)
+text {*
+ \medskip Theorem for periodic function on discrete sets. *}
lemma minf_vee:
assumes dpos: "(0::int) < d" and modd: "ALL x k. P x = P(x - k*d)"
@@ -651,8 +652,9 @@
assume ?RHS thus ?LHS by blast
qed
-(*=============================================================================*)
-(*Theorem for periodic function on discrete sets*)
+text {*
+ \medskip Theorem for periodic function on discrete sets. *}
+
lemma pinf_vee:
assumes dpos: "0 < (d::int)" and modd: "ALL (x::int) (k::int). P x = P (x+k*d)"
shows "(EX x::int. P x) = (EX (j::int) : {1..d} . P j)"
@@ -750,7 +752,7 @@
apply(blast dest:decr_mult_lemma)
done
-(* Cooper Thm `, plus infinity version*)
+text {* Cooper Theorem, plus infinity version. *}
lemma cppi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. z < x --> (P x = P1 x))
==> ALL x.~(EX (j::int) : {1..D}. EX (a::int) : A. P(a - j)) --> P (x) --> P (x + D)
==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x+k*D))))
@@ -774,9 +776,8 @@
done
-(*=============================================================================*)
-
-(*Theorems for the quantifier elminination Functions.*)
+text {*
+ \bigskip Theorems for the quantifier elminination Functions. *}
lemma qe_ex_conj: "(EX (x::int). A x) = R
==> (EX (x::int). P x) = (Q & (EX x::int. A x))
@@ -805,7 +806,7 @@
lemma qe_ALL: "(EX x. ~P x) = R ==> (ALL x. P x) = (~R)"
by blast
-(* Theorems for proving NNF *)
+text {* \bigskip Theorems for proving NNF *}
lemma nnf_im: "((~P) = P1) ==> (Q=Q1) ==> ((P --> Q) = (P1 | Q1))"
by blast
@@ -851,7 +852,7 @@
apply(fastsimp)
done
-(* Theorems required for the adjustcoeffitienteq*)
+text {* \bigskip Theorems required for the @{text adjustcoeffitienteq} *}
lemma ac_dvd_eq: assumes not0: "0 ~= (k::int)"
shows "((m::int) dvd (c*n+t)) = (k*m dvd ((k*c)*n+(k*t)))" (is "?P = ?Q")
@@ -925,7 +926,7 @@
lemma lf_dvd: "(l::int) = ll ==> (r::int) = lr ==> (l dvd r) =(ll dvd lr)"
by simp
-(* Theorems for transforming predicates on nat to predicates on int*)
+text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*}
theorem all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))"
by (simp split add: split_nat)
@@ -973,7 +974,9 @@
theorem Suc_plus1: "Suc n = n + 1" by simp
-(* specific instances of congruence rules, to prevent simplifier from looping *)
+text {*
+ \medskip Specific instances of congruence rules, to prevent
+ simplifier from looping. *}
theorem imp_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::nat) \<longrightarrow> P) = (0 <= x \<longrightarrow> P')"
by simp
--- a/src/HOL/SetInterval.thy Fri Apr 16 04:06:52 2004 +0200
+++ b/src/HOL/SetInterval.thy Fri Apr 16 04:07:10 2004 +0200
@@ -7,6 +7,8 @@
lessThan, greaterThan, atLeast, atMost and two-sided intervals
*)
+header {* Set intervals *}
+
theory SetInterval = IntArith:
constdefs
@@ -145,33 +147,33 @@
subsection {*Two-sided intervals*}
-(* greaterThanLessThan *)
+text {* @{text greaterThanLessThan} *}
lemma greaterThanLessThan_iff [simp]:
"(i : {)l..u(}) = (l < i & i < u)"
by (simp add: greaterThanLessThan_def)
-(* atLeastLessThan *)
+text {* @{text atLeastLessThan} *}
lemma atLeastLessThan_iff [simp]:
"(i : {l..u(}) = (l <= i & i < u)"
by (simp add: atLeastLessThan_def)
-(* greaterThanAtMost *)
+text {* @{text greaterThanAtMost} *}
lemma greaterThanAtMost_iff [simp]:
"(i : {)l..u}) = (l < i & i <= u)"
by (simp add: greaterThanAtMost_def)
-(* atLeastAtMost *)
+text {* @{text atLeastAtMost} *}
lemma atLeastAtMost_iff [simp]:
"(i : {l..u}) = (l <= i & i <= u)"
by (simp add: atLeastAtMost_def)
-(* The above four lemmas could be declared as iffs.
- If we do so, a call to blast in Hyperreal/Star.ML, lemma STAR_Int
- seems to take forever (more than one hour). *)
+text {* The above four lemmas could be declared as iffs.
+ If we do so, a call to blast in Hyperreal/Star.ML, lemma @{text STAR_Int}
+ seems to take forever (more than one hour). *}
subsection {* Intervals of natural numbers *}
@@ -227,7 +229,7 @@
lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"
by blast
-(* Intervals of nats with Suc *)
+text {* Intervals of nats with @{text Suc} *}
lemma atLeastLessThanSuc_atLeastAtMost: "{l..Suc u(} = {l..u}"
by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def)
@@ -391,11 +393,11 @@
subsection {*Lemmas useful with the summation operator setsum*}
-(* For examples, see Algebra/poly/UnivPoly.thy *)
+text {* For examples, see Algebra/poly/UnivPoly.thy *}
-(** Disjoint Unions **)
+subsubsection {* Disjoint Unions *}
-(* Singletons and open intervals *)
+text {* Singletons and open intervals *}
lemma ivl_disj_un_singleton:
"{l::'a::linorder} Un {)l..} = {l..}"
@@ -406,7 +408,7 @@
"(l::'a::linorder) <= u ==> {l..u(} Un {u} = {l..u}"
by auto
-(* One- and two-sided intervals *)
+text {* One- and two-sided intervals *}
lemma ivl_disj_un_one:
"(l::'a::linorder) < u ==> {..l} Un {)l..u(} = {..u(}"
@@ -419,7 +421,7 @@
"(l::'a::linorder) <= u ==> {l..u(} Un {u..} = {l..}"
by auto
-(* Two- and two-sided intervals *)
+text {* Two- and two-sided intervals *}
lemma ivl_disj_un_two:
"[| (l::'a::linorder) < m; m <= u |] ==> {)l..m(} Un {m..u(} = {)l..u(}"
@@ -434,9 +436,9 @@
lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two
-(** Disjoint Intersections **)
+subsubsection {* Disjoint Intersections *}
-(* Singletons and open intervals *)
+text {* Singletons and open intervals *}
lemma ivl_disj_int_singleton:
"{l::'a::order} Int {)l..} = {}"
@@ -447,7 +449,7 @@
"{l..u(} Int {u} = {}"
by simp+
-(* One- and two-sided intervals *)
+text {* One- and two-sided intervals *}
lemma ivl_disj_int_one:
"{..l::'a::order} Int {)l..u(} = {}"
@@ -460,7 +462,7 @@
"{l..u(} Int {u..} = {}"
by auto
-(* Two- and two-sided intervals *)
+text {* Two- and two-sided intervals *}
lemma ivl_disj_int_two:
"{)l::'a::order..m(} Int {m..u(} = {}"