# HG changeset patch
# User wenzelm
# Date 1394313704 -3600
# Node ID 6477fc70cfa055c9131a77ee71f73c85859b050f
# Parent f5f9fad3321c71b8d778bf1e057d34bece2d14d8
tuned proofs;
diff -r f5f9fad3321c -r 6477fc70cfa0 src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy Sat Mar 08 21:31:12 2014 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy Sat Mar 08 22:21:44 2014 +0100
@@ -115,14 +115,14 @@
fun qfree :: "fm \ bool" -- {* Quantifier freeness *}
where
- "qfree (E p) = False"
-| "qfree (A p) = False"
-| "qfree (NOT p) = qfree p"
-| "qfree (And p q) = (qfree p \ qfree q)"
-| "qfree (Or p q) = (qfree p \ qfree q)"
-| "qfree (Imp p q) = (qfree p \ qfree q)"
-| "qfree (Iff p q) = (qfree p \ qfree q)"
-| "qfree p = True"
+ "qfree (E p) \ False"
+| "qfree (A p) \ False"
+| "qfree (NOT p) \ qfree p"
+| "qfree (And p q) \ qfree p \ qfree q"
+| "qfree (Or p q) \ qfree p \ qfree q"
+| "qfree (Imp p q) \ qfree p \ qfree q"
+| "qfree (Iff p q) \ qfree p \ qfree q"
+| "qfree p \ True"
text {* Boundedness and substitution *}
@@ -209,9 +209,9 @@
| "subst0 t (NClosed P) = (NClosed P)"
lemma subst0_I:
- assumes qfp: "qfree p"
+ assumes "qfree p"
shows "Ifm bbs (b # bs) (subst0 a p) = Ifm bbs (Inum (b # bs) a # bs) p"
- using qfp numsubst0_I[where b="b" and bs="bs" and a="a"]
+ using assms numsubst0_I[where b="b" and bs="bs" and a="a"]
by (induct p) (simp_all add: gr0_conv_Suc)
fun decrnum:: "num \ num"
@@ -329,19 +329,20 @@
by (induct p rule: disjuncts.induct) auto
lemma disjuncts_nb:
- assumes nb: "bound0 p"
+ assumes "bound0 p"
shows "\q \ set (disjuncts p). bound0 q"
proof -
- from nb have "list_all bound0 (disjuncts p)"
+ from assms have "list_all bound0 (disjuncts p)"
by (induct p rule: disjuncts.induct) auto
- then show ?thesis by (simp only: list_all_iff)
+ then show ?thesis
+ by (simp only: list_all_iff)
qed
lemma disjuncts_qf:
- assumes qf: "qfree p"
+ assumes "qfree p"
shows "\q \ set (disjuncts p). qfree q"
proof -
- from qf have "list_all qfree (disjuncts p)"
+ from assms have "list_all qfree (disjuncts p)"
by (induct p rule: disjuncts.induct) auto
then show ?thesis by (simp only: list_all_iff)
qed
@@ -350,19 +351,19 @@
where "DJ f p = evaldjf f (disjuncts p)"
lemma DJ:
- assumes fdj: "\p q. f (Or p q) = Or (f p) (f q)"
- and fF: "f F = F"
+ assumes "\p q. f (Or p q) = Or (f p) (f q)"
+ and "f F = F"
shows "Ifm bbs bs (DJ f p) = Ifm bbs bs (f p)"
proof -
- have "Ifm bbs bs (DJ f p) = (\q \ set (disjuncts p). Ifm bbs bs (f q))"
+ have "Ifm bbs bs (DJ f p) \ (\q \ set (disjuncts p). Ifm bbs bs (f q))"
by (simp add: DJ_def evaldjf_ex)
- also have "\ = Ifm bbs bs (f p)"
- using fdj fF by (induct p rule: disjuncts.induct) auto
+ also from assms have "\ = Ifm bbs bs (f p)"
+ by (induct p rule: disjuncts.induct) auto
finally show ?thesis .
qed
lemma DJ_qf:
- assumes fqf: "\p. qfree p \ qfree (f p)"
+ assumes "\p. qfree p \ qfree (f p)"
shows "\p. qfree p \ qfree (DJ f p) "
proof clarify
fix p
@@ -370,7 +371,7 @@
have th: "DJ f p = evaldjf f (disjuncts p)"
by (simp add: DJ_def)
from disjuncts_qf[OF qf] have "\q \ set (disjuncts p). qfree q" .
- with fqf have th':"\q \ set (disjuncts p). qfree (f q)"
+ with assms have th': "\q \ set (disjuncts p). qfree (f q)"
by blast
from evaldjf_qf[OF th'] th show "qfree (DJ f p)"
by simp
@@ -389,7 +390,7 @@
by auto
have "Ifm bbs bs (DJ qe p) = (\q\ set (disjuncts p). Ifm bbs bs (qe q))"
by (simp add: DJ_def evaldjf_ex)
- also have "\ \ (\q \ set(disjuncts p). Ifm bbs bs (E q))"
+ also have "\ \ (\q \ set (disjuncts p). Ifm bbs bs (E q))"
using qe disjuncts_qf[OF qf] by auto
also have "\ \ Ifm bbs bs (E p)"
by (induct p rule: disjuncts.induct) auto
@@ -408,7 +409,7 @@
| "bnds (CN n c a) = n # bnds a"
| "bnds (Neg a) = bnds a"
| "bnds (Add a b) = bnds a @ bnds b"
-| "bnds (Sub a b) = bnds a @ bnds b"
+| "bnds (Sub a b) = bnds a @ bnds b"
| "bnds (Mul i a) = bnds a"
| "bnds a = []"
@@ -1363,7 +1364,7 @@
and d: "d dvd d'"
and ad: "d_\ p d"
shows "d_\ p d'"
- using lin ad d
+ using lin ad
proof (induct p rule: iszlfm.induct)
case (9 i c e)
then show ?case using d
@@ -1467,8 +1468,8 @@
consts \ :: "fm \ num list"
recdef \ "measure size"
- "\ (And p q) = (\ p @ \ q)"
- "\ (Or p q) = (\ p @ \ q)"
+ "\ (And p q) = \ p @ \ q"
+ "\ (Or p q) = \ p @ \ q"
"\ (Eq (CN 0 c e)) = [Add (C -1) e]"
"\ (NEq (CN 0 c e)) = [e]"
"\ (Lt (CN 0 c e)) = [e]"
@@ -1517,10 +1518,10 @@
then have c1: "c = 1" and nb: "numbound0 e"
by simp_all
fix a
- from 3 have "\x<(- Inum (a#bs) e). c * x + Inum (x # bs) e \ 0"
+ from 3 have "\x<(- Inum (a # bs) e). c * x + Inum (x # bs) e \ 0"
proof clarsimp
fix x
- assume "x < (- Inum (a#bs) e)" and "x + Inum (x#bs) e = 0"
+ assume "x < (- Inum (a # bs) e)" and "x + Inum (x # bs) e = 0"
with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
show False by simp
qed
@@ -1543,7 +1544,7 @@
then have c1: "c = 1" and nb: "numbound0 e"
by simp_all
fix a
- from 5 have "\x<(- Inum (a # bs) e). c*x + Inum (x # bs) e < 0"
+ from 5 have "\x<(- Inum (a # bs) e). c * x + Inum (x # bs) e < 0"
proof clarsimp
fix x
assume "x < (- Inum (a # bs) e)"
@@ -1583,10 +1584,10 @@
then have c1: "c = 1" and nb: "numbound0 e"
by simp_all
fix a
- from 8 have "\x<(- Inum (a#bs) e). \ (c*x + Inum (x#bs) e \ 0)"
+ from 8 have "\x<(- Inum (a # bs) e). \ c * x + Inum (x # bs) e \ 0"
proof clarsimp
fix x
- assume "x < (- Inum (a#bs) e)" and "x + Inum (x#bs) e \ 0"
+ assume "x < (- Inum (a # bs) e)" and "x + Inum (x # bs) e \ 0"
with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
show False by simp
qed
@@ -1610,7 +1611,7 @@
proof (simp add: numbound0_I[OF nbe,where bs="bs" and b="x - k * d" and b'="x"] right_diff_distrib,
rule iffI)
assume "i dvd c * x - c * (k * d) + Inum (x # bs) e"
- (is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt")
+ (is "?ri dvd ?rc * ?rx - ?rc * (?rk * ?rd) + ?I x e" is "?ri dvd ?rt")
then have "\l::int. ?rt = i * l"
by (simp add: dvd_def)
then have "\l::int. c * x + ?I x e = i * l + c * (k * i * di)"
@@ -1645,9 +1646,10 @@
then obtain di where di_def: "d = i * di"
by blast
show ?case
- proof (simp add: numbound0_I[OF nbe,where bs="bs" and b="x - k * d" and b'="x"] right_diff_distrib, rule iffI)
+ proof (simp add: numbound0_I[OF nbe,where bs="bs" and b="x - k * d" and b'="x"] right_diff_distrib,
+ rule iffI)
assume "i dvd c * x - c * (k * d) + Inum (x # bs) e"
- (is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt")
+ (is "?ri dvd ?rc * ?rx - ?rc * (?rk * ?rd) + ?I x e" is "?ri dvd ?rt")
then have "\l::int. ?rt = i * l"
by (simp add: dvd_def)
then have "\l::int. c * x + ?I x e = i * l + c * (k * i * di)"
@@ -1666,7 +1668,7 @@
by simp
then have "\l::int. c * x - c * (k * d) + ?e = i * l - c * (k * i * di)"
by (simp add: di_def)
- then have "\l::int. c * x - c * (k * d) + ?e = i * ((l - c * k * di))"
+ then have "\l::int. c * x - c * (k * d) + ?e = i * (l - c * k * di)"
by (simp add: algebra_simps)
then have "\l::int. c * x - c * (k * d) + ?e = i * l"
by blast
@@ -1734,14 +1736,14 @@
by (induct p rule: iszlfm.induct) simp_all
lemma \_l:
- assumes lp: "iszlfm p"
+ assumes "iszlfm p"
shows "\b \ set (\ p). numbound0 b"
- using lp by (induct p rule: \.induct) auto
+ using assms by (induct p rule: \.induct) auto
lemma \:
- assumes linp: "iszlfm p"
+ assumes "iszlfm p"
shows "\ p > 0 \ d_\ p (\ p)"
- using linp
+ using assms
proof (induct p rule: iszlfm.induct)
case (1 p q)
from 1 have dl1: "\ p dvd lcm (\ p) (\ q)"
@@ -1782,7 +1784,7 @@
by simp
have "c div c \ l div c"
by (simp add: zdiv_mono1[OF clel cp])
- then have ldcp:"0 < l div c"
+ then have ldcp: "0 < l div c"
by (simp add: div_self[OF cnz])
have "c * (l div c) = c * (l div c) + l mod c"
using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
@@ -1791,7 +1793,7 @@
then have "(l * x + (l div c) * Inum (x # bs) e < 0) \
((c * (l div c)) * x + (l div c) * Inum (x # bs) e < 0)"
by simp
- also have "\ \ (l div c) * (c*x + Inum (x # bs) e) < (l div c) * 0"
+ also have "\ \ (l div c) * (c * x + Inum (x # bs) e) < (l div c) * 0"
by (simp add: algebra_simps)
also have "\ \ c * x + Inum (x # bs) e < 0"
using mult_less_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp
@@ -2006,7 +2008,7 @@
shows "(\x. l dvd x \ Ifm bbs (x #bs) (a_\ p l)) \ (\x::int. Ifm bbs (x#bs) p)"
(is "(\x. l dvd x \ ?P x) \ (\x. ?P' x)")
proof-
- have "(\x. l dvd x \ ?P x) \ (\(x::int). ?P (l*x))"
+ have "(\x. l dvd x \ ?P x) \ (\x::int. ?P (l * x))"
using unity_coeff_ex[where l="l" and P="?P", simplified] by simp
also have "\ = (\x::int. ?P' x)"
using a_\[OF linp d lp] by simp
@@ -2014,14 +2016,14 @@
qed
lemma \:
- assumes lp: "iszlfm p"
- and u: "d_\ p 1"
- and d: "d_\ p d"
+ assumes "iszlfm p"
+ and "d_\ p 1"
+ and "d_\ p d"
and dp: "d > 0"
- and nob: "\ (\j::int \ {1 .. d}. \b \ Inum (a # bs) ` set (\ p). x = b + j)"
+ and "\ (\j::int \ {1 .. d}. \b \ Inum (a # bs) ` set (\ p). x = b + j)"
and p: "Ifm bbs (x # bs) p" (is "?P x")
shows "?P (x - d)"
- using lp u d dp nob p
+ using assms
proof (induct p rule: iszlfm.induct)
case (5 c e)
then have c1: "c = 1" and bn: "numbound0 e"
@@ -2198,11 +2200,14 @@
qed
lemma cpmi_eq:
- "0 < D \ (\z::int. \x. x < z \ P x = P1 x)
- \ \x. \(\(j::int) \ {1..D}. \(b::int) \ B. P (b + j)) \ P x \ P (x - D)
- \ (\(x::int). \(k::int). P1 x = (P1 (x - k * D)))
- \ (\(x::int). P x) = ((\(j::int) \ {1..D}. P1 j) \ (\(j::int) \ {1..D}. \(b::int) \ B. P (b + j)))"
- apply(rule iffI)
+ fixes P P1 :: "int \ bool"
+ assumes "0 < D"
+ and "\z. \x. x < z \ P x = P1 x"
+ and "\x. \ (\j \ {1..D}. \b \ B. P (b + j)) \ P x \ P (x - D)"
+ and "\x k. P1 x = P1 (x - k * D)"
+ shows "(\x. P x) \ (\j \ {1..D}. P1 j) \ (\j \ {1..D}. \b \ B. P (b + j))"
+ apply (insert assms)
+ apply (rule iffI)
prefer 2
apply (drule minusinfinity)
apply assumption+
@@ -2225,13 +2230,13 @@
and u: "d_\ p 1"
and d: "d_\ p d"
and dp: "d > 0"
- shows "(\(x::int). Ifm bbs (x # bs) p) \
+ shows "(\x. Ifm bbs (x # bs) p) \
(\j \ {1.. d}. Ifm bbs (j # bs) (minusinf p) \
(\b \ set (\ p). Ifm bbs ((Inum (i # bs) b + j) # bs) p))"
- (is "(\(x::int). ?P (x)) = (\j\ ?D. ?M j \ (\b\ ?B. ?P (?I b + j)))")
+ (is "(\x. ?P x) \ (\j \ ?D. ?M j \ (\b \ ?B. ?P (?I b + j)))")
proof -
from minusinf_inf[OF lp u]
- have th: "\z::int. \xz. \x ?B}" have bb': "(\j\?D. \b \ ?B. ?P (?I b + j)) \ (\j \ ?D. \b \ ?B'. ?P (b + j))"
@@ -2247,34 +2252,34 @@
(* Implement the right hand sides of Cooper's theorem and Ferrante and Rackoff. *)
lemma mirror_ex:
- assumes lp: "iszlfm p"
- shows "(\x. Ifm bbs (x#bs) (mirror p)) = (\x. Ifm bbs (x#bs) p)"
+ assumes "iszlfm p"
+ shows "(\x. Ifm bbs (x#bs) (mirror p)) \ (\x. Ifm bbs (x#bs) p)"
(is "(\x. ?I x ?mp) = (\x. ?I x p)")
proof auto
fix x
assume "?I x ?mp"
then have "?I (- x) p"
- using mirror[OF lp] by blast
+ using mirror[OF assms] by blast
then show "\x. ?I x p"
by blast
next
fix x
assume "?I x p"
then have "?I (- x) ?mp"
- using mirror[OF lp, where x="- x", symmetric] by auto
+ using mirror[OF assms, where x="- x", symmetric] by auto
then show "\x. ?I x ?mp"
by blast
qed
lemma cp_thm':
- assumes lp: "iszlfm p"
- and up: "d_\ p 1"
- and dd: "d_\ p d"
- and dp: "d > 0"
+ assumes "iszlfm p"
+ and "d_\ p 1"
+ and "d_\ p d"
+ and "d > 0"
shows "(\