tuned proofs;
authorwenzelm
Sat Mar 08 22:21:44 2014 +0100 (2014-03-08)
changeset 559996477fc70cfa0
parent 55998 f5f9fad3321c
child 56000 899ad5a3ad00
tuned proofs;
src/HOL/Decision_Procs/Cooper.thy
     1.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Sat Mar 08 21:31:12 2014 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Sat Mar 08 22:21:44 2014 +0100
     1.3 @@ -115,14 +115,14 @@
     1.4  
     1.5  fun qfree :: "fm \<Rightarrow> bool"  -- {* Quantifier freeness *}
     1.6  where
     1.7 -  "qfree (E p) = False"
     1.8 -| "qfree (A p) = False"
     1.9 -| "qfree (NOT p) = qfree p"
    1.10 -| "qfree (And p q) = (qfree p \<and> qfree q)"
    1.11 -| "qfree (Or  p q) = (qfree p \<and> qfree q)"
    1.12 -| "qfree (Imp p q) = (qfree p \<and> qfree q)"
    1.13 -| "qfree (Iff p q) = (qfree p \<and> qfree q)"
    1.14 -| "qfree p = True"
    1.15 +  "qfree (E p) \<longleftrightarrow> False"
    1.16 +| "qfree (A p) \<longleftrightarrow> False"
    1.17 +| "qfree (NOT p) \<longleftrightarrow> qfree p"
    1.18 +| "qfree (And p q) \<longleftrightarrow> qfree p \<and> qfree q"
    1.19 +| "qfree (Or  p q) \<longleftrightarrow> qfree p \<and> qfree q"
    1.20 +| "qfree (Imp p q) \<longleftrightarrow> qfree p \<and> qfree q"
    1.21 +| "qfree (Iff p q) \<longleftrightarrow> qfree p \<and> qfree q"
    1.22 +| "qfree p \<longleftrightarrow> True"
    1.23  
    1.24  
    1.25  text {* Boundedness and substitution *}
    1.26 @@ -209,9 +209,9 @@
    1.27  | "subst0 t (NClosed P) = (NClosed P)"
    1.28  
    1.29  lemma subst0_I:
    1.30 -  assumes qfp: "qfree p"
    1.31 +  assumes "qfree p"
    1.32    shows "Ifm bbs (b # bs) (subst0 a p) = Ifm bbs (Inum (b # bs) a # bs) p"
    1.33 -  using qfp numsubst0_I[where b="b" and bs="bs" and a="a"]
    1.34 +  using assms numsubst0_I[where b="b" and bs="bs" and a="a"]
    1.35    by (induct p) (simp_all add: gr0_conv_Suc)
    1.36  
    1.37  fun decrnum:: "num \<Rightarrow> num"
    1.38 @@ -329,19 +329,20 @@
    1.39    by (induct p rule: disjuncts.induct) auto
    1.40  
    1.41  lemma disjuncts_nb:
    1.42 -  assumes nb: "bound0 p"
    1.43 +  assumes "bound0 p"
    1.44    shows "\<forall>q \<in> set (disjuncts p). bound0 q"
    1.45  proof -
    1.46 -  from nb have "list_all bound0 (disjuncts p)"
    1.47 +  from assms have "list_all bound0 (disjuncts p)"
    1.48      by (induct p rule: disjuncts.induct) auto
    1.49 -  then show ?thesis by (simp only: list_all_iff)
    1.50 +  then show ?thesis
    1.51 +    by (simp only: list_all_iff)
    1.52  qed
    1.53  
    1.54  lemma disjuncts_qf:
    1.55 -  assumes qf: "qfree p"
    1.56 +  assumes "qfree p"
    1.57    shows "\<forall>q \<in> set (disjuncts p). qfree q"
    1.58  proof -
    1.59 -  from qf have "list_all qfree (disjuncts p)"
    1.60 +  from assms have "list_all qfree (disjuncts p)"
    1.61      by (induct p rule: disjuncts.induct) auto
    1.62    then show ?thesis by (simp only: list_all_iff)
    1.63  qed
    1.64 @@ -350,19 +351,19 @@
    1.65    where "DJ f p = evaldjf f (disjuncts p)"
    1.66  
    1.67  lemma DJ:
    1.68 -  assumes fdj: "\<forall>p q. f (Or p q) = Or (f p) (f q)"
    1.69 -    and fF: "f F = F"
    1.70 +  assumes "\<forall>p q. f (Or p q) = Or (f p) (f q)"
    1.71 +    and "f F = F"
    1.72    shows "Ifm bbs bs (DJ f p) = Ifm bbs bs (f p)"
    1.73  proof -
    1.74 -  have "Ifm bbs bs (DJ f p) = (\<exists>q \<in> set (disjuncts p). Ifm bbs bs (f q))"
    1.75 +  have "Ifm bbs bs (DJ f p) \<longleftrightarrow> (\<exists>q \<in> set (disjuncts p). Ifm bbs bs (f q))"
    1.76      by (simp add: DJ_def evaldjf_ex)
    1.77 -  also have "\<dots> = Ifm bbs bs (f p)"
    1.78 -    using fdj fF by (induct p rule: disjuncts.induct) auto
    1.79 +  also from assms have "\<dots> = Ifm bbs bs (f p)"
    1.80 +    by (induct p rule: disjuncts.induct) auto
    1.81    finally show ?thesis .
    1.82  qed
    1.83  
    1.84  lemma DJ_qf:
    1.85 -  assumes fqf: "\<forall>p. qfree p \<longrightarrow> qfree (f p)"
    1.86 +  assumes "\<forall>p. qfree p \<longrightarrow> qfree (f p)"
    1.87    shows "\<forall>p. qfree p \<longrightarrow> qfree (DJ f p) "
    1.88  proof clarify
    1.89    fix p
    1.90 @@ -370,7 +371,7 @@
    1.91    have th: "DJ f p = evaldjf f (disjuncts p)"
    1.92      by (simp add: DJ_def)
    1.93    from disjuncts_qf[OF qf] have "\<forall>q \<in> set (disjuncts p). qfree q" .
    1.94 -  with fqf have th':"\<forall>q \<in> set (disjuncts p). qfree (f q)"
    1.95 +  with assms have th': "\<forall>q \<in> set (disjuncts p). qfree (f q)"
    1.96      by blast
    1.97    from evaldjf_qf[OF th'] th show "qfree (DJ f p)"
    1.98      by simp
    1.99 @@ -389,7 +390,7 @@
   1.100      by auto
   1.101    have "Ifm bbs bs (DJ qe p) = (\<exists>q\<in> set (disjuncts p). Ifm bbs bs (qe q))"
   1.102      by (simp add: DJ_def evaldjf_ex)
   1.103 -  also have "\<dots> \<longleftrightarrow> (\<exists>q \<in> set(disjuncts p). Ifm bbs bs (E q))"
   1.104 +  also have "\<dots> \<longleftrightarrow> (\<exists>q \<in> set (disjuncts p). Ifm bbs bs (E q))"
   1.105      using qe disjuncts_qf[OF qf] by auto
   1.106    also have "\<dots> \<longleftrightarrow> Ifm bbs bs (E p)"
   1.107      by (induct p rule: disjuncts.induct) auto
   1.108 @@ -408,7 +409,7 @@
   1.109  | "bnds (CN n c a) = n # bnds a"
   1.110  | "bnds (Neg a) = bnds a"
   1.111  | "bnds (Add a b) = bnds a @ bnds b"
   1.112 -| "bnds (Sub a b) =  bnds a @ bnds b"
   1.113 +| "bnds (Sub a b) = bnds a @ bnds b"
   1.114  | "bnds (Mul i a) = bnds a"
   1.115  | "bnds a = []"
   1.116  
   1.117 @@ -1363,7 +1364,7 @@
   1.118      and d: "d dvd d'"
   1.119      and ad: "d_\<delta> p d"
   1.120    shows "d_\<delta> p d'"
   1.121 -  using lin ad d
   1.122 +  using lin ad
   1.123  proof (induct p rule: iszlfm.induct)
   1.124    case (9 i c e)
   1.125    then show ?case using d
   1.126 @@ -1467,8 +1468,8 @@
   1.127  
   1.128  consts \<alpha> :: "fm \<Rightarrow> num list"
   1.129  recdef \<alpha> "measure size"
   1.130 -  "\<alpha> (And p q) = (\<alpha> p @ \<alpha> q)"
   1.131 -  "\<alpha> (Or p q) = (\<alpha> p @ \<alpha> q)"
   1.132 +  "\<alpha> (And p q) = \<alpha> p @ \<alpha> q"
   1.133 +  "\<alpha> (Or p q) = \<alpha> p @ \<alpha> q"
   1.134    "\<alpha> (Eq  (CN 0 c e)) = [Add (C -1) e]"
   1.135    "\<alpha> (NEq (CN 0 c e)) = [e]"
   1.136    "\<alpha> (Lt  (CN 0 c e)) = [e]"
   1.137 @@ -1517,10 +1518,10 @@
   1.138    then have c1: "c = 1" and nb: "numbound0 e"
   1.139      by simp_all
   1.140    fix a
   1.141 -  from 3 have "\<forall>x<(- Inum (a#bs) e). c * x + Inum (x # bs) e \<noteq> 0"
   1.142 +  from 3 have "\<forall>x<(- Inum (a # bs) e). c * x + Inum (x # bs) e \<noteq> 0"
   1.143    proof clarsimp
   1.144      fix x
   1.145 -    assume "x < (- Inum (a#bs) e)" and "x + Inum (x#bs) e = 0"
   1.146 +    assume "x < (- Inum (a # bs) e)" and "x + Inum (x # bs) e = 0"
   1.147      with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
   1.148      show False by simp
   1.149    qed
   1.150 @@ -1543,7 +1544,7 @@
   1.151    then have c1: "c = 1" and nb: "numbound0 e"
   1.152      by simp_all
   1.153    fix a
   1.154 -  from 5 have "\<forall>x<(- Inum (a # bs) e). c*x + Inum (x # bs) e < 0"
   1.155 +  from 5 have "\<forall>x<(- Inum (a # bs) e). c * x + Inum (x # bs) e < 0"
   1.156    proof clarsimp
   1.157      fix x
   1.158      assume "x < (- Inum (a # bs) e)"
   1.159 @@ -1583,10 +1584,10 @@
   1.160    then have c1: "c = 1" and nb: "numbound0 e"
   1.161      by simp_all
   1.162    fix a
   1.163 -  from 8 have "\<forall>x<(- Inum (a#bs) e). \<not> (c*x + Inum (x#bs) e \<ge> 0)"
   1.164 +  from 8 have "\<forall>x<(- Inum (a # bs) e). \<not> c * x + Inum (x # bs) e \<ge> 0"
   1.165    proof clarsimp
   1.166      fix x
   1.167 -    assume "x < (- Inum (a#bs) e)" and "x + Inum (x#bs) e \<ge> 0"
   1.168 +    assume "x < (- Inum (a # bs) e)" and "x + Inum (x # bs) e \<ge> 0"
   1.169      with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
   1.170      show False by simp
   1.171    qed
   1.172 @@ -1610,7 +1611,7 @@
   1.173    proof (simp add: numbound0_I[OF nbe,where bs="bs" and b="x - k * d" and b'="x"] right_diff_distrib,
   1.174        rule iffI)
   1.175      assume "i dvd c * x - c * (k * d) + Inum (x # bs) e"
   1.176 -      (is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt")
   1.177 +      (is "?ri dvd ?rc * ?rx - ?rc * (?rk * ?rd) + ?I x e" is "?ri dvd ?rt")
   1.178      then have "\<exists>l::int. ?rt = i * l"
   1.179        by (simp add: dvd_def)
   1.180      then have "\<exists>l::int. c * x + ?I x e = i * l + c * (k * i * di)"
   1.181 @@ -1645,9 +1646,10 @@
   1.182    then obtain di where di_def: "d = i * di"
   1.183      by blast
   1.184    show ?case
   1.185 -  proof (simp add: numbound0_I[OF nbe,where bs="bs" and b="x - k * d" and b'="x"] right_diff_distrib, rule iffI)
   1.186 +  proof (simp add: numbound0_I[OF nbe,where bs="bs" and b="x - k * d" and b'="x"] right_diff_distrib,
   1.187 +      rule iffI)
   1.188      assume "i dvd c * x - c * (k * d) + Inum (x # bs) e"
   1.189 -      (is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt")
   1.190 +      (is "?ri dvd ?rc * ?rx - ?rc * (?rk * ?rd) + ?I x e" is "?ri dvd ?rt")
   1.191      then have "\<exists>l::int. ?rt = i * l"
   1.192        by (simp add: dvd_def)
   1.193      then have "\<exists>l::int. c * x + ?I x e = i * l + c * (k * i * di)"
   1.194 @@ -1666,7 +1668,7 @@
   1.195        by simp
   1.196      then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l - c * (k * i * di)"
   1.197        by (simp add: di_def)
   1.198 -    then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * ((l - c * k * di))"
   1.199 +    then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * (l - c * k * di)"
   1.200        by (simp add: algebra_simps)
   1.201      then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l"
   1.202        by blast
   1.203 @@ -1734,14 +1736,14 @@
   1.204    by (induct p rule: iszlfm.induct) simp_all
   1.205  
   1.206  lemma \<alpha>_l:
   1.207 -  assumes lp: "iszlfm p"
   1.208 +  assumes "iszlfm p"
   1.209    shows "\<forall>b \<in> set (\<alpha> p). numbound0 b"
   1.210 -  using lp by (induct p rule: \<alpha>.induct) auto
   1.211 +  using assms by (induct p rule: \<alpha>.induct) auto
   1.212  
   1.213  lemma \<zeta>:
   1.214 -  assumes linp: "iszlfm p"
   1.215 +  assumes "iszlfm p"
   1.216    shows "\<zeta> p > 0 \<and> d_\<beta> p (\<zeta> p)"
   1.217 -  using linp
   1.218 +  using assms
   1.219  proof (induct p rule: iszlfm.induct)
   1.220    case (1 p q)
   1.221    from 1 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)"
   1.222 @@ -1782,7 +1784,7 @@
   1.223      by simp
   1.224    have "c div c \<le> l div c"
   1.225      by (simp add: zdiv_mono1[OF clel cp])
   1.226 -  then have ldcp:"0 < l div c"
   1.227 +  then have ldcp: "0 < l div c"
   1.228      by (simp add: div_self[OF cnz])
   1.229    have "c * (l div c) = c * (l div c) + l mod c"
   1.230      using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   1.231 @@ -1791,7 +1793,7 @@
   1.232    then have "(l * x + (l div c) * Inum (x # bs) e < 0) \<longleftrightarrow>
   1.233        ((c * (l div c)) * x + (l div c) * Inum (x # bs) e < 0)"
   1.234      by simp
   1.235 -  also have "\<dots> \<longleftrightarrow> (l div c) * (c*x + Inum (x # bs) e) < (l div c) * 0"
   1.236 +  also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) < (l div c) * 0"
   1.237      by (simp add: algebra_simps)
   1.238    also have "\<dots> \<longleftrightarrow> c * x + Inum (x # bs) e < 0"
   1.239      using mult_less_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp
   1.240 @@ -2006,7 +2008,7 @@
   1.241    shows "(\<exists>x. l dvd x \<and> Ifm bbs (x #bs) (a_\<beta> p l)) \<longleftrightarrow> (\<exists>x::int. Ifm bbs (x#bs) p)"
   1.242    (is "(\<exists>x. l dvd x \<and> ?P x) \<longleftrightarrow> (\<exists>x. ?P' x)")
   1.243  proof-
   1.244 -  have "(\<exists>x. l dvd x \<and> ?P x) \<longleftrightarrow> (\<exists>(x::int). ?P (l*x))"
   1.245 +  have "(\<exists>x. l dvd x \<and> ?P x) \<longleftrightarrow> (\<exists>x::int. ?P (l * x))"
   1.246      using unity_coeff_ex[where l="l" and P="?P", simplified] by simp
   1.247    also have "\<dots> = (\<exists>x::int. ?P' x)"
   1.248      using a_\<beta>[OF linp d lp] by simp
   1.249 @@ -2014,14 +2016,14 @@
   1.250  qed
   1.251  
   1.252  lemma \<beta>:
   1.253 -  assumes lp: "iszlfm p"
   1.254 -    and u: "d_\<beta> p 1"
   1.255 -    and d: "d_\<delta> p d"
   1.256 +  assumes "iszlfm p"
   1.257 +    and "d_\<beta> p 1"
   1.258 +    and "d_\<delta> p d"
   1.259      and dp: "d > 0"
   1.260 -    and nob: "\<not> (\<exists>j::int \<in> {1 .. d}. \<exists>b \<in> Inum (a # bs) ` set (\<beta> p). x = b + j)"
   1.261 +    and "\<not> (\<exists>j::int \<in> {1 .. d}. \<exists>b \<in> Inum (a # bs) ` set (\<beta> p). x = b + j)"
   1.262      and p: "Ifm bbs (x # bs) p" (is "?P x")
   1.263    shows "?P (x - d)"
   1.264 -  using lp u d dp nob p
   1.265 +  using assms
   1.266  proof (induct p rule: iszlfm.induct)
   1.267    case (5 c e)
   1.268    then have c1: "c = 1" and  bn: "numbound0 e"
   1.269 @@ -2198,11 +2200,14 @@
   1.270  qed
   1.271  
   1.272  lemma cpmi_eq:
   1.273 -  "0 < D \<Longrightarrow> (\<exists>z::int. \<forall>x. x < z \<longrightarrow> P x = P1 x)
   1.274 -    \<Longrightarrow> \<forall>x. \<not>(\<exists>(j::int) \<in> {1..D}. \<exists>(b::int) \<in> B. P (b + j)) \<longrightarrow> P x \<longrightarrow> P (x - D)
   1.275 -    \<Longrightarrow> (\<forall>(x::int). \<forall>(k::int). P1 x = (P1 (x - k * D)))
   1.276 -    \<Longrightarrow> (\<exists>(x::int). P x) = ((\<exists>(j::int) \<in> {1..D}. P1 j) \<or> (\<exists>(j::int) \<in> {1..D}. \<exists>(b::int) \<in> B. P (b + j)))"
   1.277 -  apply(rule iffI)
   1.278 +  fixes P P1 :: "int \<Rightarrow> bool"
   1.279 +  assumes "0 < D"
   1.280 +    and "\<exists>z. \<forall>x. x < z \<longrightarrow> P x = P1 x"
   1.281 +    and "\<forall>x. \<not> (\<exists>j \<in> {1..D}. \<exists>b \<in> B. P (b + j)) \<longrightarrow> P x \<longrightarrow> P (x - D)"
   1.282 +    and "\<forall>x k. P1 x = P1 (x - k * D)"
   1.283 +  shows "(\<exists>x. P x) \<longleftrightarrow> (\<exists>j \<in> {1..D}. P1 j) \<or> (\<exists>j \<in> {1..D}. \<exists>b \<in> B. P (b + j))"
   1.284 +  apply (insert assms)
   1.285 +  apply (rule iffI)
   1.286    prefer 2
   1.287    apply (drule minusinfinity)
   1.288    apply assumption+
   1.289 @@ -2225,13 +2230,13 @@
   1.290      and u: "d_\<beta> p 1"
   1.291      and d: "d_\<delta> p d"
   1.292      and dp: "d > 0"
   1.293 -  shows "(\<exists>(x::int). Ifm bbs (x # bs) p) \<longleftrightarrow>
   1.294 +  shows "(\<exists>x. Ifm bbs (x # bs) p) \<longleftrightarrow>
   1.295      (\<exists>j \<in> {1.. d}. Ifm bbs (j # bs) (minusinf p) \<or>
   1.296        (\<exists>b \<in> set (\<beta> p). Ifm bbs ((Inum (i # bs) b + j) # bs) p))"
   1.297 -  (is "(\<exists>(x::int). ?P (x)) = (\<exists>j\<in> ?D. ?M j \<or> (\<exists>b\<in> ?B. ?P (?I b + j)))")
   1.298 +  (is "(\<exists>x. ?P x) \<longleftrightarrow> (\<exists>j \<in> ?D. ?M j \<or> (\<exists>b \<in> ?B. ?P (?I b + j)))")
   1.299  proof -
   1.300    from minusinf_inf[OF lp u]
   1.301 -  have th: "\<exists>z::int. \<forall>x<z. ?P (x) = ?M x"
   1.302 +  have th: "\<exists>z. \<forall>x<z. ?P x = ?M x"
   1.303      by blast
   1.304    let ?B' = "{?I b | b. b \<in> ?B}"
   1.305    have BB': "(\<exists>j\<in>?D. \<exists>b \<in> ?B. ?P (?I b + j)) \<longleftrightarrow> (\<exists>j \<in> ?D. \<exists>b \<in> ?B'. ?P (b + j))"
   1.306 @@ -2247,34 +2252,34 @@
   1.307  
   1.308  (* Implement the right hand sides of Cooper's theorem and Ferrante and Rackoff. *)
   1.309  lemma mirror_ex:
   1.310 -  assumes lp: "iszlfm p"
   1.311 -  shows "(\<exists>x. Ifm bbs (x#bs) (mirror p)) = (\<exists>x. Ifm bbs (x#bs) p)"
   1.312 +  assumes "iszlfm p"
   1.313 +  shows "(\<exists>x. Ifm bbs (x#bs) (mirror p)) \<longleftrightarrow> (\<exists>x. Ifm bbs (x#bs) p)"
   1.314    (is "(\<exists>x. ?I x ?mp) = (\<exists>x. ?I x p)")
   1.315  proof auto
   1.316    fix x
   1.317    assume "?I x ?mp"
   1.318    then have "?I (- x) p"
   1.319 -    using mirror[OF lp] by blast
   1.320 +    using mirror[OF assms] by blast
   1.321    then show "\<exists>x. ?I x p"
   1.322      by blast
   1.323  next
   1.324    fix x
   1.325    assume "?I x p"
   1.326    then have "?I (- x) ?mp"
   1.327 -    using mirror[OF lp, where x="- x", symmetric] by auto
   1.328 +    using mirror[OF assms, where x="- x", symmetric] by auto
   1.329    then show "\<exists>x. ?I x ?mp"
   1.330      by blast
   1.331  qed
   1.332  
   1.333  lemma cp_thm':
   1.334 -  assumes lp: "iszlfm p"
   1.335 -    and up: "d_\<beta> p 1"
   1.336 -    and dd: "d_\<delta> p d"
   1.337 -    and dp: "d > 0"
   1.338 +  assumes "iszlfm p"
   1.339 +    and "d_\<beta> p 1"
   1.340 +    and "d_\<delta> p d"
   1.341 +    and "d > 0"
   1.342    shows "(\<exists>x. Ifm bbs (x # bs) p) \<longleftrightarrow>
   1.343      ((\<exists>j\<in> {1 .. d}. Ifm bbs (j#bs) (minusinf p)) \<or>
   1.344        (\<exists>j\<in> {1.. d}. \<exists>b\<in> (Inum (i#bs)) ` set (\<beta> p). Ifm bbs ((b + j) # bs) p))"
   1.345 -  using cp_thm[OF lp up dd dp,where i="i"] by auto
   1.346 +  using cp_thm[OF assms,where i="i"] by auto
   1.347  
   1.348  definition unit :: "fm \<Rightarrow> fm \<times> num list \<times> int"
   1.349  where