tuned proofs;
authorwenzelm
Thu Mar 06 22:10:38 2014 +0100 (2014-03-06)
changeset 55964acdde1a5faa0
parent 55963 a8ebafaa56d4
child 55965 0c2c61a87a7d
tuned proofs;
src/HOL/Decision_Procs/Cooper.thy
     1.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Thu Mar 06 21:33:15 2014 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Thu Mar 06 22:10:38 2014 +0100
     1.3 @@ -881,9 +881,9 @@
     1.4    assumes qe_inv: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> Ifm bbs bs (qe p) = Ifm bbs bs (E p)"
     1.5    shows "\<And>bs. qfree (qelim p qe) \<and> Ifm bbs bs (qelim p qe) = Ifm bbs bs p"
     1.6    using qe_inv DJ_qe[OF qe_inv]
     1.7 -  by(induct p rule: qelim.induct)
     1.8 -  (auto simp add: not disj conj iff imp not_qf disj_qf conj_qf imp_qf iff_qf
     1.9 -    simpfm simpfm_qf simp del: simpfm.simps)
    1.10 +  by (induct p rule: qelim.induct)
    1.11 +    (auto simp add: not disj conj iff imp not_qf disj_qf conj_qf imp_qf iff_qf
    1.12 +      simpfm simpfm_qf simp del: simpfm.simps)
    1.13  
    1.14  text {* Linearity for fm where Bound 0 ranges over @{text "\<int>"} *}
    1.15  
    1.16 @@ -908,7 +908,7 @@
    1.17  | "zsplit0 (Mul i a) = (let (i', a') = zsplit0 a in (i*i', Mul i a'))"
    1.18  
    1.19  lemma zsplit0_I:
    1.20 -  shows "\<And>n a. zsplit0 t = (n, a) \<Longrightarrow>
    1.21 +  "\<And>n a. zsplit0 t = (n, a) \<Longrightarrow>
    1.22      (Inum ((x::int) # bs) (CN 0 n a) = Inum (x # bs) t) \<and> numbound0 a"
    1.23    (is "\<And>n a. ?S t = (n,a) \<Longrightarrow> (?I x (CN 0 n a) = ?I x t) \<and> ?N a")
    1.24  proof (induct t rule: zsplit0.induct)
    1.25 @@ -930,11 +930,11 @@
    1.26    moreover
    1.27    {
    1.28      assume m0: "m = 0"
    1.29 -    with abj have th: "a'=?b \<and> n=i+?j" using 3
    1.30 -      by (simp add: Let_def split_def)
    1.31 +    with abj have th: "a' = ?b \<and> n = i + ?j"
    1.32 +      using 3 by (simp add: Let_def split_def)
    1.33      from abj 3 m0 have th2: "(?I x (CN 0 ?j ?b) = ?I x a) \<and> ?N ?b"
    1.34        by blast
    1.35 -    from th have "?I x (CN 0 n a') = ?I x (CN 0 (i+?j) ?b)"
    1.36 +    from th have "?I x (CN 0 n a') = ?I x (CN 0 (i + ?j) ?b)"
    1.37        by simp
    1.38      also from th2 have "\<dots> = ?I x (CN 0 i (CN 0 ?j ?b))"
    1.39        by (simp add: distrib_right)
    1.40 @@ -948,8 +948,9 @@
    1.41    case (4 t n a)
    1.42    let ?nt = "fst (zsplit0 t)"
    1.43    let ?at = "snd (zsplit0 t)"
    1.44 -  have abj: "zsplit0 t = (?nt,?at)" by simp
    1.45 -  then have th: "a=Neg ?at \<and> n=-?nt"
    1.46 +  have abj: "zsplit0 t = (?nt, ?at)"
    1.47 +    by simp
    1.48 +  then have th: "a = Neg ?at \<and> n = - ?nt"
    1.49      using 4 by (simp add: Let_def split_def)
    1.50    from abj 4 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at"
    1.51      by blast
    1.52 @@ -965,9 +966,9 @@
    1.53      by simp
    1.54    moreover have abjt: "zsplit0 t = (?nt, ?at)"
    1.55      by simp
    1.56 -  ultimately have th: "a=Add ?as ?at \<and> n=?ns + ?nt"
    1.57 +  ultimately have th: "a = Add ?as ?at \<and> n = ?ns + ?nt"
    1.58      using 5 by (simp add: Let_def split_def)
    1.59 -  from abjs[symmetric] have bluddy: "\<exists>x y. (x,y) = zsplit0 s"
    1.60 +  from abjs[symmetric] have bluddy: "\<exists>x y. (x, y) = zsplit0 s"
    1.61      by blast
    1.62    from 5 have "(\<exists>x y. (x, y) = zsplit0 s) \<longrightarrow>
    1.63      (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t \<and> numbound0 xb)"
    1.64 @@ -988,9 +989,9 @@
    1.65      by simp
    1.66    moreover have abjt: "zsplit0 t = (?nt, ?at)"
    1.67      by simp
    1.68 -  ultimately have th: "a=Sub ?as ?at \<and> n=?ns - ?nt"
    1.69 +  ultimately have th: "a = Sub ?as ?at \<and> n = ?ns - ?nt"
    1.70      using 6 by (simp add: Let_def split_def)
    1.71 -  from abjs[symmetric] have bluddy: "\<exists>x y. (x,y) = zsplit0 s"
    1.72 +  from abjs[symmetric] have bluddy: "\<exists>x y. (x, y) = zsplit0 s"
    1.73      by blast
    1.74    from 6 have "(\<exists>x y. (x,y) = zsplit0 s) \<longrightarrow>
    1.75      (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t \<and> numbound0 xb)"
    1.76 @@ -1007,7 +1008,7 @@
    1.77    let ?at = "snd (zsplit0 t)"
    1.78    have abj: "zsplit0 t = (?nt,?at)"
    1.79      by simp
    1.80 -  then have th: "a=Mul i ?at \<and> n=i*?nt"
    1.81 +  then have th: "a = Mul i ?at \<and> n = i * ?nt"
    1.82      using 7 by (simp add: Let_def split_def)
    1.83    from abj 7 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at"
    1.84      by blast
    1.85 @@ -1042,34 +1043,50 @@
    1.86    "zlfm (Or p q) = Or (zlfm p) (zlfm q)"
    1.87    "zlfm (Imp p q) = Or (zlfm (NOT p)) (zlfm q)"
    1.88    "zlfm (Iff p q) = Or (And (zlfm p) (zlfm q)) (And (zlfm (NOT p)) (zlfm (NOT q)))"
    1.89 -  "zlfm (Lt a) = (let (c,r) = zsplit0 a in
    1.90 -     if c=0 then Lt r else
    1.91 -     if c>0 then (Lt (CN 0 c r)) else (Gt (CN 0 (- c) (Neg r))))"
    1.92 -  "zlfm (Le a) = (let (c,r) = zsplit0 a in
    1.93 -     if c=0 then Le r else
    1.94 -     if c>0 then (Le (CN 0 c r)) else (Ge (CN 0 (- c) (Neg r))))"
    1.95 -  "zlfm (Gt a) = (let (c,r) = zsplit0 a in
    1.96 -     if c=0 then Gt r else
    1.97 -     if c>0 then (Gt (CN 0 c r)) else (Lt (CN 0 (- c) (Neg r))))"
    1.98 -  "zlfm (Ge a) = (let (c,r) = zsplit0 a in
    1.99 -     if c=0 then Ge r else
   1.100 -     if c>0 then (Ge (CN 0 c r)) else (Le (CN 0 (- c) (Neg r))))"
   1.101 -  "zlfm (Eq a) = (let (c,r) = zsplit0 a in
   1.102 -     if c=0 then Eq r else
   1.103 -     if c>0 then (Eq (CN 0 c r)) else (Eq (CN 0 (- c) (Neg r))))"
   1.104 -  "zlfm (NEq a) = (let (c,r) = zsplit0 a in
   1.105 -     if c=0 then NEq r else
   1.106 -     if c>0 then (NEq (CN 0 c r)) else (NEq (CN 0 (- c) (Neg r))))"
   1.107 -  "zlfm (Dvd i a) = (if i=0 then zlfm (Eq a)
   1.108 -        else (let (c,r) = zsplit0 a in
   1.109 -              if c=0 then (Dvd (abs i) r) else
   1.110 -      if c>0 then (Dvd (abs i) (CN 0 c r))
   1.111 -      else (Dvd (abs i) (CN 0 (- c) (Neg r)))))"
   1.112 -  "zlfm (NDvd i a) = (if i=0 then zlfm (NEq a)
   1.113 -        else (let (c,r) = zsplit0 a in
   1.114 -              if c=0 then (NDvd (abs i) r) else
   1.115 -      if c>0 then (NDvd (abs i) (CN 0 c r))
   1.116 -      else (NDvd (abs i) (CN 0 (- c) (Neg r)))))"
   1.117 +  "zlfm (Lt a) =
   1.118 +    (let (c, r) = zsplit0 a in
   1.119 +      if c = 0 then Lt r else
   1.120 +      if c > 0 then (Lt (CN 0 c r))
   1.121 +      else Gt (CN 0 (- c) (Neg r)))"
   1.122 +  "zlfm (Le a) =
   1.123 +    (let (c, r) = zsplit0 a in
   1.124 +      if c = 0 then Le r
   1.125 +      else if c > 0 then Le (CN 0 c r)
   1.126 +      else Ge (CN 0 (- c) (Neg r)))"
   1.127 +  "zlfm (Gt a) =
   1.128 +    (let (c, r) = zsplit0 a in
   1.129 +      if c = 0 then Gt r else
   1.130 +      if c > 0 then Gt (CN 0 c r)
   1.131 +      else Lt (CN 0 (- c) (Neg r)))"
   1.132 +  "zlfm (Ge a) =
   1.133 +    (let (c, r) = zsplit0 a in
   1.134 +      if c = 0 then Ge r
   1.135 +      else if c > 0 then Ge (CN 0 c r)
   1.136 +      else Le (CN 0 (- c) (Neg r)))"
   1.137 +  "zlfm (Eq a) =
   1.138 +    (let (c, r) = zsplit0 a in
   1.139 +      if c = 0 then Eq r
   1.140 +      else if c > 0 then Eq (CN 0 c r)
   1.141 +      else Eq (CN 0 (- c) (Neg r)))"
   1.142 +  "zlfm (NEq a) =
   1.143 +    (let (c, r) = zsplit0 a in
   1.144 +      if c = 0 then NEq r
   1.145 +      else if c > 0 then NEq (CN 0 c r)
   1.146 +      else NEq (CN 0 (- c) (Neg r)))"
   1.147 +  "zlfm (Dvd i a) =
   1.148 +    (if i = 0 then zlfm (Eq a)
   1.149 +     else
   1.150 +      let (c, r) = zsplit0 a in
   1.151 +        if c = 0 then Dvd (abs i) r
   1.152 +        else if c > 0 then Dvd (abs i) (CN 0 c r)
   1.153 +        else Dvd (abs i) (CN 0 (- c) (Neg r)))"
   1.154 +  "zlfm (NDvd i a) =
   1.155 +    (if i = 0 then zlfm (NEq a)
   1.156 +     else
   1.157 +      let (c, r) = zsplit0 a in
   1.158 +        if c = 0 then NDvd (abs i) r
   1.159 +        else if c > 0 then NDvd (abs i) (CN 0 c r)
   1.160 +        else NDvd (abs i) (CN 0 (- c) (Neg r)))"
   1.161    "zlfm (NOT (And p q)) = Or (zlfm (NOT p)) (zlfm (NOT q))"
   1.162    "zlfm (NOT (Or p q)) = And (zlfm (NOT p)) (zlfm (NOT q))"
   1.163    "zlfm (NOT (Imp p q)) = And (zlfm p) (zlfm (NOT q))"
   1.164 @@ -1091,7 +1108,7 @@
   1.165  
   1.166  lemma zlfm_I:
   1.167    assumes qfp: "qfree p"
   1.168 -  shows "(Ifm bbs (i#bs) (zlfm p) = Ifm bbs (i# bs) p) \<and> iszlfm (zlfm p)"
   1.169 +  shows "(Ifm bbs (i # bs) (zlfm p) = Ifm bbs (i # bs) p) \<and> iszlfm (zlfm p)"
   1.170    (is "(?I (?l p) = ?I p) \<and> ?L (?l p)")
   1.171    using qfp
   1.172  proof (induct p rule: zlfm.induct)
   1.173 @@ -1101,10 +1118,10 @@
   1.174    have spl: "zsplit0 a = (?c, ?r)"
   1.175      by simp
   1.176    from zsplit0_I[OF spl, where x="i" and bs="bs"]
   1.177 -  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
   1.178 +  have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
   1.179      by auto
   1.180 -  let ?N = "\<lambda>t. Inum (i#bs) t"
   1.181 -  from 5 Ia nb  show ?case
   1.182 +  let ?N = "\<lambda>t. Inum (i # bs) t"
   1.183 +  from 5 Ia nb show ?case
   1.184      apply (auto simp add: Let_def split_def algebra_simps)
   1.185      apply (cases "?r")
   1.186      apply auto
   1.187 @@ -1118,9 +1135,9 @@
   1.188    have spl: "zsplit0 a = (?c, ?r)"
   1.189      by simp
   1.190    from zsplit0_I[OF spl, where x="i" and bs="bs"]
   1.191 -  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
   1.192 +  have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
   1.193      by auto
   1.194 -  let ?N = "\<lambda>t. Inum (i#bs) t"
   1.195 +  let ?N = "\<lambda>t. Inum (i # bs) t"
   1.196    from 6 Ia nb show ?case
   1.197      apply (auto simp add: Let_def split_def algebra_simps)
   1.198      apply (cases "?r")
   1.199 @@ -1137,7 +1154,7 @@
   1.200    from zsplit0_I[OF spl, where x="i" and bs="bs"]
   1.201    have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
   1.202      by auto
   1.203 -  let ?N = "\<lambda>t. Inum (i#bs) t"
   1.204 +  let ?N = "\<lambda>t. Inum (i # bs) t"
   1.205    from 7 Ia nb show ?case
   1.206      apply (auto simp add: Let_def split_def algebra_simps)
   1.207      apply (cases "?r")
   1.208 @@ -1152,9 +1169,9 @@
   1.209    have spl: "zsplit0 a = (?c, ?r)"
   1.210      by simp
   1.211    from zsplit0_I[OF spl, where x="i" and bs="bs"]
   1.212 -  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
   1.213 +  have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
   1.214      by auto
   1.215 -  let ?N = "\<lambda>t. Inum (i#bs) t"
   1.216 +  let ?N = "\<lambda>t. Inum (i # bs) t"
   1.217    from 8 Ia nb show ?case
   1.218      apply (auto simp add: Let_def split_def algebra_simps)
   1.219      apply (cases "?r")
   1.220 @@ -1171,7 +1188,7 @@
   1.221    from zsplit0_I[OF spl, where x="i" and bs="bs"]
   1.222    have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
   1.223      by auto
   1.224 -  let ?N = "\<lambda>t. Inum (i#bs) t"
   1.225 +  let ?N = "\<lambda>t. Inum (i # bs) t"
   1.226    from 9 Ia nb show ?case
   1.227      apply (auto simp add: Let_def split_def algebra_simps)
   1.228      apply (cases "?r")
   1.229 @@ -1188,7 +1205,7 @@
   1.230    from zsplit0_I[OF spl, where x="i" and bs="bs"]
   1.231    have Ia: "Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
   1.232      by auto
   1.233 -  let ?N = "\<lambda>t. Inum (i#bs) t"
   1.234 +  let ?N = "\<lambda>t. Inum (i # bs) t"
   1.235    from 10 Ia nb show ?case
   1.236      apply (auto simp add: Let_def split_def algebra_simps)
   1.237      apply (cases "?r")
   1.238 @@ -1255,13 +1272,13 @@
   1.239    from zsplit0_I[OF spl, where x="i" and bs="bs"]
   1.240    have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r"
   1.241      by auto
   1.242 -  let ?N = "\<lambda>t. Inum (i#bs) t"
   1.243 +  let ?N = "\<lambda>t. Inum (i # bs) t"
   1.244    have "j = 0 \<or> (j \<noteq> 0 \<and> ?c = 0) \<or> (j \<noteq> 0 \<and> ?c > 0) \<or> (j \<noteq> 0 \<and> ?c < 0)"
   1.245      by arith
   1.246    moreover
   1.247    {
   1.248      assume "j = 0"
   1.249 -    then have z: "zlfm (NDvd j a) = (zlfm (NEq a))"
   1.250 +    then have z: "zlfm (NDvd j a) = zlfm (NEq a)"
   1.251        by (simp add: Let_def)
   1.252      then have ?case
   1.253        using assms 12 `j = 0` by (simp del: zlfm.simps)
   1.254 @@ -1484,17 +1501,17 @@
   1.255  lemma minusinf_inf:
   1.256    assumes linp: "iszlfm p"
   1.257      and u: "d_\<beta> p 1"
   1.258 -  shows "\<exists>(z::int). \<forall>x < z. Ifm bbs (x#bs) (minusinf p) = Ifm bbs (x#bs) p"
   1.259 +  shows "\<exists>z::int. \<forall>x < z. Ifm bbs (x # bs) (minusinf p) = Ifm bbs (x # bs) p"
   1.260    (is "?P p" is "\<exists>(z::int). \<forall>x < z. ?I x (?M p) = ?I x p")
   1.261    using linp u
   1.262  proof (induct p rule: minusinf.induct)
   1.263    case (1 p q)
   1.264    then show ?case
   1.265 -    by auto (rule_tac x="min z za" in exI, simp)
   1.266 +    by auto (rule_tac x = "min z za" in exI, simp)
   1.267  next
   1.268    case (2 p q)
   1.269    then show ?case
   1.270 -    by auto (rule_tac x="min z za" in exI, simp)
   1.271 +    by auto (rule_tac x = "min z za" in exI, simp)
   1.272  next
   1.273    case (3 c e)
   1.274    then have c1: "c = 1" and nb: "numbound0 e"
   1.275 @@ -1513,10 +1530,10 @@
   1.276    then have c1: "c = 1" and nb: "numbound0 e"
   1.277      by simp_all
   1.278    fix a
   1.279 -  from 4 have "\<forall>x < (- Inum (a#bs) e). c*x + Inum (x#bs) e \<noteq> 0"
   1.280 +  from 4 have "\<forall>x < (- Inum (a # bs) e). c * x + Inum (x # bs) e \<noteq> 0"
   1.281    proof clarsimp
   1.282      fix x
   1.283 -    assume "x < (- Inum (a#bs) e)" and"x + Inum (x # bs) e = 0"
   1.284 +    assume "x < (- Inum (a # bs) e)" and "x + Inum (x # bs) e = 0"
   1.285      with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
   1.286      show "False" by simp
   1.287    qed
   1.288 @@ -1526,10 +1543,10 @@
   1.289    then have c1: "c = 1" and nb: "numbound0 e"
   1.290      by simp_all
   1.291    fix a
   1.292 -  from 5 have "\<forall>x<(- Inum (a#bs) e). c*x + Inum (x#bs) e < 0"
   1.293 +  from 5 have "\<forall>x<(- Inum (a # bs) e). c*x + Inum (x # bs) e < 0"
   1.294    proof clarsimp
   1.295      fix x
   1.296 -    assume "x < (- Inum (a#bs) e)"
   1.297 +    assume "x < (- Inum (a # bs) e)"
   1.298      with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
   1.299      show "x + Inum (x # bs) e < 0"
   1.300        by simp
   1.301 @@ -1540,12 +1557,12 @@
   1.302    then have c1: "c = 1" and nb: "numbound0 e"
   1.303      by simp_all
   1.304    fix a
   1.305 -  from 6 have "\<forall>x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<le> 0"
   1.306 +  from 6 have "\<forall>x<(- Inum (a # bs) e). c * x + Inum (x # bs) e \<le> 0"
   1.307    proof clarsimp
   1.308      fix x
   1.309 -    assume "x < (- Inum (a#bs) e)"
   1.310 +    assume "x < (- Inum (a # bs) e)"
   1.311      with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
   1.312 -    show "x + Inum (x#bs) e \<le> 0" by simp
   1.313 +    show "x + Inum (x # bs) e \<le> 0" by simp
   1.314    qed
   1.315    then show ?case by auto
   1.316  next
   1.317 @@ -1553,10 +1570,10 @@
   1.318    then have c1: "c = 1" and nb: "numbound0 e"
   1.319      by simp_all
   1.320    fix a
   1.321 -  from 7 have "\<forall>x<(- Inum (a#bs) e). \<not> (c*x + Inum (x#bs) e > 0)"
   1.322 +  from 7 have "\<forall>x<(- Inum (a # bs) e). \<not> (c * x + Inum (x # bs) e > 0)"
   1.323    proof clarsimp
   1.324      fix x
   1.325 -    assume "x < (- Inum (a#bs) e)" and"x + Inum (x#bs) e > 0"
   1.326 +    assume "x < - Inum (a # bs) e" and "x + Inum (x # bs) e > 0"
   1.327      with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
   1.328      show False by simp
   1.329    qed
   1.330 @@ -1596,23 +1613,23 @@
   1.331        (is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt")
   1.332      then have "\<exists>l::int. ?rt = i * l"
   1.333        by (simp add: dvd_def)
   1.334 -    then have "\<exists>l::int. c*x+ ?I x e = i * l + c * (k * i * di)"
   1.335 +    then have "\<exists>l::int. c * x + ?I x e = i * l + c * (k * i * di)"
   1.336        by (simp add: algebra_simps di_def)
   1.337 -    then have "\<exists>l::int. c*x+ ?I x e = i*(l + c * k * di)"
   1.338 +    then have "\<exists>l::int. c * x + ?I x e = i* (l + c * k * di)"
   1.339        by (simp add: algebra_simps)
   1.340      then have "\<exists>l::int. c * x + ?I x e = i * l"
   1.341        by blast
   1.342      then show "i dvd c * x + Inum (x # bs) e"
   1.343        by (simp add: dvd_def)
   1.344    next
   1.345 -    assume "i dvd c*x + Inum (x # bs) e" (is "?ri dvd ?rc * ?rx + ?e")
   1.346 +    assume "i dvd c * x + Inum (x # bs) e"  (is "?ri dvd ?rc * ?rx + ?e")
   1.347      then have "\<exists>l::int. c * x + ?e = i * l"
   1.348        by (simp add: dvd_def)
   1.349      then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l - c * (k * d)"
   1.350        by simp
   1.351      then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l - c * (k * i * di)"
   1.352        by (simp add: di_def)
   1.353 -    then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * ((l - c * k * di))"
   1.354 +    then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * (l - c * k * di)"
   1.355        by (simp add: algebra_simps)
   1.356      then have "\<exists>l::int. c * x - c * (k * d) + ?e = i * l"
   1.357        by blast
   1.358 @@ -1660,7 +1677,7 @@
   1.359  
   1.360  lemma mirror_\<alpha>_\<beta>:
   1.361    assumes lp: "iszlfm p"
   1.362 -  shows "(Inum (i#bs)) ` set (\<alpha> p) = (Inum (i#bs)) ` set (\<beta> (mirror p))"
   1.363 +  shows "Inum (i # bs) ` set (\<alpha> p) = Inum (i # bs) ` set (\<beta> (mirror p))"
   1.364    using lp by (induct p rule: mirror.induct) auto
   1.365  
   1.366  lemma mirror:
   1.367 @@ -1669,27 +1686,30 @@
   1.368    using lp
   1.369  proof (induct p rule: iszlfm.induct)
   1.370    case (9 j c e)
   1.371 -  then have nb: "numbound0 e" by simp
   1.372 -  have "Ifm bbs (x#bs) (mirror (Dvd j (CN 0 c e))) = (j dvd c*x - Inum (x#bs) e)"
   1.373 +  then have nb: "numbound0 e"
   1.374 +    by simp
   1.375 +  have "Ifm bbs (x # bs) (mirror (Dvd j (CN 0 c e))) \<longleftrightarrow> j dvd c * x - Inum (x # bs) e"
   1.376      (is "_ = (j dvd c*x - ?e)") by simp
   1.377 -  also have "\<dots> = (j dvd (- (c*x - ?e)))"
   1.378 +  also have "\<dots> \<longleftrightarrow> j dvd (- (c * x - ?e))"
   1.379      by (simp only: dvd_minus_iff)
   1.380 -  also have "\<dots> = (j dvd (c* (- x)) + ?e)"
   1.381 +  also have "\<dots> \<longleftrightarrow> j dvd (c * (- x)) + ?e"
   1.382      by (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] add_ac minus_add_distrib)
   1.383        (simp add: algebra_simps)
   1.384 -  also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))"
   1.385 +  also have "\<dots> = Ifm bbs ((- x) # bs) (Dvd j (CN 0 c e))"
   1.386      using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] by simp
   1.387    finally show ?case .
   1.388  next
   1.389 -  case (10 j c e) then have nb: "numbound0 e" by simp
   1.390 -  have "Ifm bbs (x#bs) (mirror (Dvd j (CN 0 c e))) = (j dvd c*x - Inum (x#bs) e)"
   1.391 -    (is "_ = (j dvd c*x - ?e)") by simp
   1.392 -  also have "\<dots> = (j dvd (- (c*x - ?e)))"
   1.393 +  case (10 j c e)
   1.394 +  then have nb: "numbound0 e"
   1.395 +    by simp
   1.396 +  have "Ifm bbs (x # bs) (mirror (Dvd j (CN 0 c e))) \<longleftrightarrow> j dvd c * x - Inum (x # bs) e"
   1.397 +    (is "_ = (j dvd c * x - ?e)") by simp
   1.398 +  also have "\<dots> \<longleftrightarrow> j dvd (- (c * x - ?e))"
   1.399      by (simp only: dvd_minus_iff)
   1.400 -  also have "\<dots> = (j dvd (c* (- x)) + ?e)"
   1.401 +  also have "\<dots> \<longleftrightarrow> j dvd (c * (- x)) + ?e"
   1.402      by (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] add_ac minus_add_distrib)
   1.403        (simp add: algebra_simps)
   1.404 -  also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))"
   1.405 +  also have "\<dots> \<longleftrightarrow> Ifm bbs ((- x) # bs) (Dvd j (CN 0 c e))"
   1.406      using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] by simp
   1.407    finally show ?case by simp
   1.408  qed (auto simp add: numbound0_I[where bs="bs" and b="x" and b'="- x"] gr0_conv_Suc)
   1.409 @@ -1702,7 +1722,7 @@
   1.410  
   1.411  lemma \<beta>_numbound0:
   1.412    assumes lp: "iszlfm p"
   1.413 -  shows "\<forall>b\<in> set (\<beta> p). numbound0 b"
   1.414 +  shows "\<forall>b \<in> set (\<beta> p). numbound0 b"
   1.415    using lp by (induct p rule: \<beta>.induct) auto
   1.416  
   1.417  lemma d_\<beta>_mono:
   1.418 @@ -1724,29 +1744,37 @@
   1.419    using linp
   1.420  proof (induct p rule: iszlfm.induct)
   1.421    case (1 p q)
   1.422 -  from 1 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
   1.423 -  from 1 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
   1.424 +  from 1 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)"
   1.425 +    by simp
   1.426 +  from 1 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)"
   1.427 +    by simp
   1.428    from 1 d_\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"]
   1.429 -    d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"]
   1.430 -    dl1 dl2 show ?case by (auto simp add: lcm_pos_int)
   1.431 +      d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"]
   1.432 +      dl1 dl2
   1.433 +  show ?case
   1.434 +    by (auto simp add: lcm_pos_int)
   1.435  next
   1.436    case (2 p q)
   1.437 -  from 2 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
   1.438 -  from 2 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
   1.439 +  from 2 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)"
   1.440 +    by simp
   1.441 +  from 2 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)"
   1.442 +    by simp
   1.443    from 2 d_\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"]
   1.444 -    d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"]
   1.445 -    dl1 dl2 show ?case by (auto simp add: lcm_pos_int)
   1.446 +      d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"]
   1.447 +      dl1 dl2
   1.448 +  show ?case
   1.449 +    by (auto simp add: lcm_pos_int)
   1.450  qed (auto simp add: lcm_pos_int)
   1.451  
   1.452  lemma a_\<beta>:
   1.453    assumes linp: "iszlfm p"
   1.454      and d: "d_\<beta> p l"
   1.455      and lp: "l > 0"
   1.456 -  shows "iszlfm (a_\<beta> p l) \<and> d_\<beta> (a_\<beta> p l) 1 \<and> (Ifm bbs (l*x #bs) (a_\<beta> p l) = Ifm bbs (x#bs) p)"
   1.457 +  shows "iszlfm (a_\<beta> p l) \<and> d_\<beta> (a_\<beta> p l) 1 \<and> Ifm bbs (l * x # bs) (a_\<beta> p l) = Ifm bbs (x # bs) p"
   1.458    using linp d
   1.459  proof (induct p rule: iszlfm.induct)
   1.460    case (5 c e)
   1.461 -  then have cp: "c>0" and be: "numbound0 e" and d': "c dvd l"
   1.462 +  then have cp: "c > 0" and be: "numbound0 e" and d': "c dvd l"
   1.463      by simp_all
   1.464    from lp cp have clel: "c \<le> l"
   1.465      by (simp add: zdvd_imp_le [OF d' lp])
   1.466 @@ -1760,15 +1788,17 @@
   1.467      using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   1.468    then have cl: "c * (l div c) =l"
   1.469      using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
   1.470 -  then have "(l*x + (l div c) * Inum (x # bs) e < 0) =
   1.471 +  then have "(l * x + (l div c) * Inum (x # bs) e < 0) \<longleftrightarrow>
   1.472        ((c * (l div c)) * x + (l div c) * Inum (x # bs) e < 0)"
   1.473      by simp
   1.474 -  also have "\<dots> = ((l div c) * (c*x + Inum (x # bs) e) < (l div c) * 0)"
   1.475 +  also have "\<dots> \<longleftrightarrow> (l div c) * (c*x + Inum (x # bs) e) < (l div c) * 0"
   1.476      by (simp add: algebra_simps)
   1.477 -  also have "\<dots> = (c*x + Inum (x # bs) e < 0)"
   1.478 -    using mult_less_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp by simp
   1.479 +  also have "\<dots> \<longleftrightarrow> c * x + Inum (x # bs) e < 0"
   1.480 +    using mult_less_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp
   1.481 +    by simp
   1.482    finally show ?case
   1.483 -    using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be by simp
   1.484 +    using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be
   1.485 +    by simp
   1.486  next
   1.487    case (6 c e)
   1.488    then have cp: "c > 0" and be: "numbound0 e" and d': "c dvd l"
   1.489 @@ -1777,20 +1807,20 @@
   1.490      by (simp add: zdvd_imp_le [OF d' lp])
   1.491    from cp have cnz: "c \<noteq> 0"
   1.492      by simp
   1.493 -  have "c div c\<le> l div c"
   1.494 +  have "c div c \<le> l div c"
   1.495      by (simp add: zdiv_mono1[OF clel cp])
   1.496    then have ldcp:"0 < l div c"
   1.497      by (simp add: div_self[OF cnz])
   1.498 -  have "c * (l div c) = c* (l div c) + l mod c"
   1.499 +  have "c * (l div c) = c * (l div c) + l mod c"
   1.500      using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   1.501    then have cl: "c * (l div c) = l"
   1.502      using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
   1.503 -  then have "(l*x + (l div c) * Inum (x# bs) e \<le> 0) =
   1.504 -      ((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<le> 0)"
   1.505 +  then have "l * x + (l div c) * Inum (x # bs) e \<le> 0 \<longleftrightarrow>
   1.506 +      (c * (l div c)) * x + (l div c) * Inum (x # bs) e \<le> 0"
   1.507      by simp
   1.508 -  also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<le> ((l div c)) * 0)"
   1.509 +  also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) \<le> (l div c) * 0"
   1.510      by (simp add: algebra_simps)
   1.511 -  also have "\<dots> = (c*x + Inum (x # bs) e \<le> 0)"
   1.512 +  also have "\<dots> \<longleftrightarrow> c * x + Inum (x # bs) e \<le> 0"
   1.513      using mult_le_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp by simp
   1.514    finally show ?case
   1.515      using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be by simp
   1.516 @@ -1804,18 +1834,18 @@
   1.517      by simp
   1.518    have "c div c \<le> l div c"
   1.519      by (simp add: zdiv_mono1[OF clel cp])
   1.520 -  then have ldcp:"0 < l div c"
   1.521 +  then have ldcp: "0 < l div c"
   1.522      by (simp add: div_self[OF cnz])
   1.523 -  have "c * (l div c) = c* (l div c) + l mod c"
   1.524 +  have "c * (l div c) = c * (l div c) + l mod c"
   1.525      using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   1.526 -  then have cl:"c * (l div c) = l"
   1.527 +  then have cl: "c * (l div c) = l"
   1.528      using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
   1.529 -  then have "(l * x + (l div c) * Inum (x # bs) e > 0) =
   1.530 -      ((c * (l div c)) * x + (l div c) * Inum (x # bs) e > 0)"
   1.531 +  then have "l * x + (l div c) * Inum (x # bs) e > 0 \<longleftrightarrow>
   1.532 +      (c * (l div c)) * x + (l div c) * Inum (x # bs) e > 0"
   1.533      by simp
   1.534 -  also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) > ((l div c)) * 0)"
   1.535 +  also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) > (l div c) * 0"
   1.536      by (simp add: algebra_simps)
   1.537 -  also have "\<dots> = (c * x + Inum (x # bs) e > 0)"
   1.538 +  also have "\<dots> \<longleftrightarrow> c * x + Inum (x # bs) e > 0"
   1.539      using zero_less_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp
   1.540      by simp
   1.541    finally show ?case
   1.542 @@ -1833,17 +1863,17 @@
   1.543      by (simp add: zdiv_mono1[OF clel cp])
   1.544    then have ldcp: "0 < l div c"
   1.545      by (simp add: div_self[OF cnz])
   1.546 -  have "c * (l div c) = c* (l div c) + l mod c"
   1.547 +  have "c * (l div c) = c * (l div c) + l mod c"
   1.548      using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   1.549    then have cl: "c * (l div c) =l"
   1.550      using zmod_zdiv_equality[where a="l" and b="c", symmetric]
   1.551      by simp
   1.552 -  then have "(l*x + (l div c)* Inum (x # bs) e \<ge> 0) =
   1.553 -      ((c*(l div c))*x + (l div c)* Inum (x # bs) e \<ge> 0)"
   1.554 +  then have "l * x + (l div c) * Inum (x # bs) e \<ge> 0 \<longleftrightarrow>
   1.555 +      (c * (l div c)) * x + (l div c) * Inum (x # bs) e \<ge> 0"
   1.556      by simp
   1.557 -  also have "\<dots> = ((l div c)*(c*x + Inum (x # bs) e) \<ge> ((l div c)) * 0)"
   1.558 +  also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) \<ge> (l div c) * 0"
   1.559      by (simp add: algebra_simps)
   1.560 -  also have "\<dots> = (c*x + Inum (x # bs) e \<ge> 0)"
   1.561 +  also have "\<dots> \<longleftrightarrow> c * x + Inum (x # bs) e \<ge> 0"
   1.562      using ldcp zero_le_mult_iff [where a="l div c" and b="c*x + Inum (x # bs) e"]
   1.563      by simp
   1.564    finally show ?case
   1.565 @@ -1861,16 +1891,16 @@
   1.566      by (simp add: zdiv_mono1[OF clel cp])
   1.567    then have ldcp:"0 < l div c"
   1.568      by (simp add: div_self[OF cnz])
   1.569 -  have "c * (l div c) = c* (l div c) + l mod c"
   1.570 +  have "c * (l div c) = c * (l div c) + l mod c"
   1.571      using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   1.572    then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
   1.573      by simp
   1.574 -  then have "(l * x + (l div c) * Inum (x # bs) e = 0) =
   1.575 -      ((c * (l div c)) * x + (l div c) * Inum (x # bs) e = 0)"
   1.576 +  then have "l * x + (l div c) * Inum (x # bs) e = 0 \<longleftrightarrow>
   1.577 +      (c * (l div c)) * x + (l div c) * Inum (x # bs) e = 0"
   1.578      by simp
   1.579 -  also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) = ((l div c)) * 0)"
   1.580 +  also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) = ((l div c)) * 0"
   1.581      by (simp add: algebra_simps)
   1.582 -  also have "\<dots> = (c * x + Inum (x # bs) e = 0)"
   1.583 +  also have "\<dots> \<longleftrightarrow> c * x + Inum (x # bs) e = 0"
   1.584      using mult_eq_0_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp
   1.585      by simp
   1.586    finally show ?case
   1.587 @@ -1888,11 +1918,11 @@
   1.588      by (simp add: zdiv_mono1[OF clel cp])
   1.589    then have ldcp:"0 < l div c"
   1.590      by (simp add: div_self[OF cnz])
   1.591 -  have "c * (l div c) = c* (l div c) + l mod c"
   1.592 +  have "c * (l div c) = c * (l div c) + l mod c"
   1.593      using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   1.594    then have cl: "c * (l div c) = l"
   1.595      using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
   1.596 -  then have "(l * x + (l div c) * Inum (x # bs) e \<noteq> 0) \<longleftrightarrow>
   1.597 +  then have "l * x + (l div c) * Inum (x # bs) e \<noteq> 0 \<longleftrightarrow>
   1.598        (c * (l div c)) * x + (l div c) * Inum (x # bs) e \<noteq> 0"
   1.599      by simp
   1.600    also have "\<dots> \<longleftrightarrow> (l div c) * (c * x + Inum (x # bs) e) \<noteq> (l div c) * 0"
   1.601 @@ -1914,14 +1944,14 @@
   1.602      by (simp add: zdiv_mono1[OF clel cp])
   1.603    then have ldcp:"0 < l div c"
   1.604      by (simp add: div_self[OF cnz])
   1.605 -  have "c * (l div c) = c* (l div c) + l mod c"
   1.606 +  have "c * (l div c) = c * (l div c) + l mod c"
   1.607      using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
   1.608    then have cl: "c * (l div c) = l"
   1.609      using zmod_zdiv_equality[where a="l" and b="c", symmetric] by simp
   1.610    then have "(\<exists>k::int. l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) \<longleftrightarrow>
   1.611 -      (\<exists>(k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)"
   1.612 +      (\<exists>k::int. (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)"
   1.613      by simp
   1.614 -  also have "\<dots> \<longleftrightarrow> (\<exists>(k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c) * 0)"
   1.615 +  also have "\<dots> \<longleftrightarrow> (\<exists>k::int. (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c) * 0)"
   1.616      by (simp add: algebra_simps)
   1.617    also
   1.618    fix k
   1.619 @@ -1958,10 +1988,10 @@
   1.620      by (simp add: algebra_simps)
   1.621    also
   1.622    fix k
   1.623 -  have "\<dots> = (\<exists>k::int. c * x + Inum (x # bs) e - j * k = 0)"
   1.624 +  have "\<dots> \<longleftrightarrow> (\<exists>k::int. c * x + Inum (x # bs) e - j * k = 0)"
   1.625      using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp
   1.626      by simp
   1.627 -  also have "\<dots> = (\<exists>k::int. c * x + Inum (x # bs) e = j * k)"
   1.628 +  also have "\<dots> \<longleftrightarrow> (\<exists>k::int. c * x + Inum (x # bs) e = j * k)"
   1.629      by simp
   1.630    finally show ?case
   1.631      using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be
   1.632 @@ -1988,15 +2018,15 @@
   1.633      and u: "d_\<beta> p 1"
   1.634      and d: "d_\<delta> p d"
   1.635      and dp: "d > 0"
   1.636 -    and nob: "\<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists>b\<in> (Inum (a#bs)) ` set(\<beta> p). x = b + j)"
   1.637 -    and p: "Ifm bbs (x#bs) p" (is "?P x")
   1.638 +    and nob: "\<not> (\<exists>j::int \<in> {1 .. d}. \<exists>b \<in> Inum (a # bs) ` set (\<beta> p). x = b + j)"
   1.639 +    and p: "Ifm bbs (x # bs) p" (is "?P x")
   1.640    shows "?P (x - d)"
   1.641    using lp u d dp nob p
   1.642  proof (induct p rule: iszlfm.induct)
   1.643    case (5 c e)
   1.644    then have c1: "c = 1" and  bn: "numbound0 e"
   1.645      by simp_all
   1.646 -  with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] 5
   1.647 +  with dp p c1 numbound0_I[OF bn,where b = "(x - d)" and b' = "x" and bs = "bs"] 5
   1.648    show ?case by simp
   1.649  next
   1.650    case (6 c e)
   1.651 @@ -2006,29 +2036,30 @@
   1.652    show ?case by simp
   1.653  next
   1.654    case (7 c e)
   1.655 -  then have p: "Ifm bbs (x #bs) (Gt (CN 0 c e))" and c1: "c=1" and bn: "numbound0 e"
   1.656 +  then have p: "Ifm bbs (x # bs) (Gt (CN 0 c e))" and c1: "c=1" and bn: "numbound0 e"
   1.657      by simp_all
   1.658    let ?e = "Inum (x # bs) e"
   1.659    {
   1.660 -    assume "(x-d) +?e > 0"
   1.661 +    assume "(x - d) + ?e > 0"
   1.662      then have ?case
   1.663        using c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] by simp
   1.664    }
   1.665    moreover
   1.666    {
   1.667 -    assume H: "\<not> (x-d) + ?e > 0"
   1.668 -    let ?v="Neg e"
   1.669 -    have vb: "?v \<in> set (\<beta> (Gt (CN 0 c e)))" by simp
   1.670 +    assume H: "\<not> (x - d) + ?e > 0"
   1.671 +    let ?v = "Neg e"
   1.672 +    have vb: "?v \<in> set (\<beta> (Gt (CN 0 c e)))"
   1.673 +      by simp
   1.674      from 7(5)[simplified simp_thms Inum.simps \<beta>.simps set_simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]]
   1.675 -    have nob: "\<not> (\<exists>j\<in> {1 ..d}. x =  - ?e + j)"
   1.676 +    have nob: "\<not> (\<exists>j\<in> {1 ..d}. x = - ?e + j)"
   1.677        by auto
   1.678      from H p have "x + ?e > 0 \<and> x + ?e \<le> d"
   1.679        by (simp add: c1)
   1.680      then have "x + ?e \<ge> 1 \<and> x + ?e \<le> d"
   1.681        by simp
   1.682 -    then have "\<exists>(j::int) \<in> {1 .. d}. j = x + ?e"
   1.683 +    then have "\<exists>j::int \<in> {1 .. d}. j = x + ?e"
   1.684        by simp
   1.685 -    then have "\<exists>(j::int) \<in> {1 .. d}. x = (- ?e + j)"
   1.686 +    then have "\<exists>j::int \<in> {1 .. d}. x = (- ?e + j)"
   1.687        by (simp add: algebra_simps)
   1.688      with nob have ?case
   1.689        by auto
   1.690 @@ -2059,9 +2090,9 @@
   1.691        by (simp add: c1)
   1.692      then have "x + ?e +1 \<ge> 1 \<and> x + ?e + 1 \<le> d"
   1.693        by simp
   1.694 -    then have "\<exists>(j::int) \<in> {1 .. d}. j = x + ?e + 1"
   1.695 +    then have "\<exists>j::int \<in> {1 .. d}. j = x + ?e + 1"
   1.696        by simp
   1.697 -    then have "\<exists>(j::int) \<in> {1 .. d}. x= - ?e - 1 + j"
   1.698 +    then have "\<exists>j::int \<in> {1 .. d}. x= - ?e - 1 + j"
   1.699        by (simp add: algebra_simps)
   1.700      with nob have ?case
   1.701        by simp
   1.702 @@ -2072,35 +2103,38 @@
   1.703    case (3 c e)
   1.704    then
   1.705    have p: "Ifm bbs (x #bs) (Eq (CN 0 c e))" (is "?p x")
   1.706 -    and c1: "c=1"
   1.707 +    and c1: "c = 1"
   1.708      and bn: "numbound0 e"
   1.709      by simp_all
   1.710    let ?e = "Inum (x # bs) e"
   1.711    let ?v="(Sub (C -1) e)"
   1.712    have vb: "?v \<in> set (\<beta> (Eq (CN 0 c e)))"
   1.713      by simp
   1.714 -  from p have "x= - ?e" by (simp add: c1) with 3(5) show ?case
   1.715 +  from p have "x= - ?e"
   1.716 +    by (simp add: c1) with 3(5)
   1.717 +  show ?case
   1.718      using dp
   1.719      by simp (erule ballE[where x="1"],
   1.720        simp_all add:algebra_simps numbound0_I[OF bn,where b="x"and b'="a"and bs="bs"])
   1.721  next
   1.722    case (4 c e)
   1.723    then
   1.724 -  have p: "Ifm bbs (x #bs) (NEq (CN 0 c e))" (is "?p x")
   1.725 +  have p: "Ifm bbs (x # bs) (NEq (CN 0 c e))" (is "?p x")
   1.726      and c1: "c = 1"
   1.727      and bn: "numbound0 e"
   1.728      by simp_all
   1.729    let ?e = "Inum (x # bs) e"
   1.730    let ?v="Neg e"
   1.731 -  have vb: "?v \<in> set (\<beta> (NEq (CN 0 c e)))" by simp
   1.732 +  have vb: "?v \<in> set (\<beta> (NEq (CN 0 c e)))"
   1.733 +    by simp
   1.734    {
   1.735      assume "x - d + Inum (((x -d)) # bs) e \<noteq> 0"
   1.736      then have ?case by (simp add: c1)
   1.737    }
   1.738    moreover
   1.739    {
   1.740 -    assume H: "x - d + Inum (((x -d)) # bs) e = 0"
   1.741 -    then have "x = - Inum (((x -d)) # bs) e + d"
   1.742 +    assume H: "x - d + Inum ((x - d) # bs) e = 0"
   1.743 +    then have "x = - Inum ((x - d) # bs) e + d"
   1.744        by simp
   1.745      then have "x = - Inum (a # bs) e + d"
   1.746        by (simp add: numbound0_I[OF bn,where b="x - d"and b'="a"and bs="bs"])
   1.747 @@ -2119,9 +2153,9 @@
   1.748    let ?e = "Inum (x # bs) e"
   1.749    from 9 have id: "j dvd d"
   1.750      by simp
   1.751 -  from c1 have "?p x = (j dvd (x + ?e))"
   1.752 +  from c1 have "?p x \<longleftrightarrow> j dvd (x + ?e)"
   1.753      by simp
   1.754 -  also have "\<dots> = (j dvd x - d + ?e)"
   1.755 +  also have "\<dots> \<longleftrightarrow> j dvd x - d + ?e"
   1.756      using zdvd_period[OF id, where x="x" and c="-1" and t="?e"]
   1.757      by simp
   1.758    finally show ?case
   1.759 @@ -2130,16 +2164,16 @@
   1.760  next
   1.761    case (10 j c e)
   1.762    then
   1.763 -  have p: "Ifm bbs (x #bs) (NDvd j (CN 0 c e))" (is "?p x")
   1.764 +  have p: "Ifm bbs (x # bs) (NDvd j (CN 0 c e))" (is "?p x")
   1.765      and c1: "c = 1"
   1.766      and bn: "numbound0 e"
   1.767      by simp_all
   1.768    let ?e = "Inum (x # bs) e"
   1.769    from 10 have id: "j dvd d"
   1.770      by simp
   1.771 -  from c1 have "?p x = (\<not> j dvd (x + ?e))"
   1.772 +  from c1 have "?p x \<longleftrightarrow> \<not> j dvd (x + ?e)"
   1.773      by simp
   1.774 -  also have "\<dots> = (\<not> j dvd x - d + ?e)"
   1.775 +  also have "\<dots> \<longleftrightarrow> \<not> j dvd x - d + ?e"
   1.776      using zdvd_period[OF id, where x="x" and c="-1" and t="?e"]
   1.777      by simp
   1.778    finally show ?case
   1.779 @@ -2152,13 +2186,13 @@
   1.780    and u: "d_\<beta> p 1"
   1.781    and d: "d_\<delta> p d"
   1.782    and dp: "d > 0"
   1.783 -  shows "\<forall>x. \<not> (\<exists>(j::int) \<in> {1 .. d}. \<exists>b\<in> set(\<beta> p). Ifm bbs ((Inum (a#bs) b + j) #bs) p) \<longrightarrow>
   1.784 -    Ifm bbs (x#bs) p \<longrightarrow> Ifm bbs ((x - d)#bs) p" (is "\<forall>x. ?b \<longrightarrow> ?P x \<longrightarrow> ?P (x - d)")
   1.785 +  shows "\<forall>x. \<not> (\<exists>j::int \<in> {1 .. d}. \<exists>b \<in> set(\<beta> p). Ifm bbs ((Inum (a#bs) b + j) #bs) p) \<longrightarrow>
   1.786 +    Ifm bbs (x # bs) p \<longrightarrow> Ifm bbs ((x - d) # bs) p" (is "\<forall>x. ?b \<longrightarrow> ?P x \<longrightarrow> ?P (x - d)")
   1.787  proof clarify
   1.788    fix x
   1.789    assume nb: "?b"
   1.790      and px: "?P x"
   1.791 -  then have nb2: "\<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists>b\<in> (Inum (a#bs)) ` set(\<beta> p). x = b + j)"
   1.792 +  then have nb2: "\<not> (\<exists>j::int \<in> {1 .. d}. \<exists>b \<in> Inum (a # bs) ` set (\<beta> p). x = b + j)"
   1.793      by auto
   1.794    from  \<beta>[OF lp u d dp nb2 px] show "?P (x -d )" .
   1.795  qed
   1.796 @@ -2191,16 +2225,18 @@
   1.797      and u: "d_\<beta> p 1"
   1.798      and d: "d_\<delta> p d"
   1.799      and dp: "d > 0"
   1.800 -  shows "(\<exists>(x::int). Ifm bbs (x #bs) p) = (\<exists>j\<in> {1.. d}. Ifm bbs (j #bs) (minusinf p) \<or> (\<exists>b \<in> set (\<beta> p). Ifm bbs ((Inum (i#bs) b + j) #bs) p))"
   1.801 +  shows "(\<exists>(x::int). Ifm bbs (x # bs) p) \<longleftrightarrow>
   1.802 +    (\<exists>j \<in> {1.. d}. Ifm bbs (j # bs) (minusinf p) \<or>
   1.803 +      (\<exists>b \<in> set (\<beta> p). Ifm bbs ((Inum (i # bs) b + j) # bs) p))"
   1.804    (is "(\<exists>(x::int). ?P (x)) = (\<exists>j\<in> ?D. ?M j \<or> (\<exists>b\<in> ?B. ?P (?I b + j)))")
   1.805  proof -
   1.806    from minusinf_inf[OF lp u]
   1.807 -  have th: "\<exists>(z::int). \<forall>x<z. ?P (x) = ?M x"
   1.808 +  have th: "\<exists>z::int. \<forall>x<z. ?P (x) = ?M x"
   1.809      by blast
   1.810 -  let ?B' = "{?I b | b. b\<in> ?B}"
   1.811 -  have BB': "(\<exists>j\<in>?D. \<exists>b\<in> ?B. ?P (?I b +j)) = (\<exists>j \<in> ?D. \<exists>b \<in> ?B'. ?P (b + j))"
   1.812 +  let ?B' = "{?I b | b. b \<in> ?B}"
   1.813 +  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.814      by auto
   1.815 -  then have th2: "\<forall>x. \<not> (\<exists>j \<in> ?D. \<exists>b \<in> ?B'. ?P ((b + j))) \<longrightarrow> ?P (x) \<longrightarrow> ?P ((x - d))"
   1.816 +  then have th2: "\<forall>x. \<not> (\<exists>j \<in> ?D. \<exists>b \<in> ?B'. ?P (b + j)) \<longrightarrow> ?P x \<longrightarrow> ?P (x - d)"
   1.817      using \<beta>'[OF lp u d dp, where a="i" and bbs = "bbs"] by blast
   1.818    from minusinf_repeats[OF d lp]
   1.819    have th3: "\<forall>x k. ?M x = ?M (x-k*d)"
   1.820 @@ -2214,31 +2250,50 @@
   1.821    assumes lp: "iszlfm p"
   1.822    shows "(\<exists>x. Ifm bbs (x#bs) (mirror p)) = (\<exists>x. Ifm bbs (x#bs) p)"
   1.823    (is "(\<exists>x. ?I x ?mp) = (\<exists>x. ?I x p)")
   1.824 -proof(auto)
   1.825 -  fix x assume "?I x ?mp" then have "?I (- x) p" using mirror[OF lp] by blast
   1.826 -  then show "\<exists>x. ?I x p" by blast
   1.827 +proof auto
   1.828 +  fix x
   1.829 +  assume "?I x ?mp"
   1.830 +  then have "?I (- x) p"
   1.831 +    using mirror[OF lp] by blast
   1.832 +  then show "\<exists>x. ?I x p"
   1.833 +    by blast
   1.834  next
   1.835 -  fix x assume "?I x p" then have "?I (- x) ?mp"
   1.836 +  fix x
   1.837 +  assume "?I x p"
   1.838 +  then have "?I (- x) ?mp"
   1.839      using mirror[OF lp, where x="- x", symmetric] by auto
   1.840 -  then show "\<exists>x. ?I x ?mp" by blast
   1.841 +  then show "\<exists>x. ?I x ?mp"
   1.842 +    by blast
   1.843  qed
   1.844  
   1.845 -
   1.846  lemma cp_thm':
   1.847    assumes lp: "iszlfm p"
   1.848 -  and up: "d_\<beta> p 1" and dd: "d_\<delta> p d" and dp: "d > 0"
   1.849 -  shows "(\<exists>x. Ifm bbs (x#bs) p) = ((\<exists>j\<in> {1 .. d}. Ifm bbs (j#bs) (minusinf p)) \<or> (\<exists>j\<in> {1.. d}. \<exists>b\<in> (Inum (i#bs)) ` set (\<beta> p). Ifm bbs ((b+j)#bs) p))"
   1.850 +    and up: "d_\<beta> p 1"
   1.851 +    and dd: "d_\<delta> p d"
   1.852 +    and dp: "d > 0"
   1.853 +  shows "(\<exists>x. Ifm bbs (x # bs) p) \<longleftrightarrow>
   1.854 +    ((\<exists>j\<in> {1 .. d}. Ifm bbs (j#bs) (minusinf p)) \<or>
   1.855 +      (\<exists>j\<in> {1.. d}. \<exists>b\<in> (Inum (i#bs)) ` set (\<beta> p). Ifm bbs ((b + j) # bs) p))"
   1.856    using cp_thm[OF lp up dd dp,where i="i"] by auto
   1.857  
   1.858  definition unit :: "fm \<Rightarrow> fm \<times> num list \<times> int"
   1.859  where
   1.860 -  "unit p = (let p' = zlfm p ; l = \<zeta> p' ; q = And (Dvd l (CN 0 1 (C 0))) (a_\<beta> p' l); d = \<delta> q;
   1.861 -             B = remdups (map simpnum (\<beta> q)) ; a = remdups (map simpnum (\<alpha> q))
   1.862 -             in if length B \<le> length a then (q,B,d) else (mirror q, a,d))"
   1.863 +  "unit p =
   1.864 +     (let
   1.865 +        p' = zlfm p;
   1.866 +        l = \<zeta> p';
   1.867 +        q = And (Dvd l (CN 0 1 (C 0))) (a_\<beta> p' l);
   1.868 +        d = \<delta> q;
   1.869 +        B = remdups (map simpnum (\<beta> q));
   1.870 +        a = remdups (map simpnum (\<alpha> q))
   1.871 +      in if length B \<le> length a then (q, B, d) else (mirror q, a, d))"
   1.872  
   1.873  lemma unit:
   1.874    assumes qf: "qfree p"
   1.875 -  shows "\<And>q B d. unit p = (q,B,d) \<Longrightarrow> ((\<exists>x. Ifm bbs (x#bs) p) = (\<exists>x. Ifm bbs (x#bs) q)) \<and> (Inum (i#bs)) ` set B = (Inum (i#bs)) ` set (\<beta> q) \<and> d_\<beta> q 1 \<and> d_\<delta> q d \<and> d >0 \<and> iszlfm q \<and> (\<forall>b\<in> set B. numbound0 b)"
   1.876 +  shows "\<And>q B d. unit p = (q, B, d) \<Longrightarrow>
   1.877 +    ((\<exists>x. Ifm bbs (x # bs) p) \<longleftrightarrow> (\<exists>x. Ifm bbs (x # bs) q)) \<and>
   1.878 +    (Inum (i # bs)) ` set B = (Inum (i # bs)) ` set (\<beta> q) \<and> d_\<beta> q 1 \<and> d_\<delta> q d \<and> d > 0 \<and>
   1.879 +    iszlfm q \<and> (\<forall>b\<in> set B. numbound0 b)"
   1.880  proof -
   1.881    fix q B d
   1.882    assume qBd: "unit p = (q,B,d)"