--- 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