src/HOL/Decision_Procs/Cooper.thy
 changeset 50252 4aa34bd43228 parent 49962 a8cc904a6820 child 50313 5b49cfd43a37
```     1.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Wed Nov 28 15:38:12 2012 +0100
1.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Wed Nov 28 15:59:18 2012 +0100
1.3 @@ -1004,7 +1004,7 @@
1.4    plusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of +\<infinity>*)
1.5    minusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of -\<infinity>*)
1.6    \<delta> :: "fm \<Rightarrow> int" (* Compute lcm {d| N\<^isup>? Dvd c*x+t \<in> p}*)
1.7 -  d\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool" (* checks if a given l divides all the ds above*)
1.8 +  d_\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool" (* checks if a given l divides all the ds above*)
1.9
1.10  recdef minusinf "measure size"
1.11    "minusinf (And p q) = And (minusinf p) (minusinf q)"
1.12 @@ -1038,18 +1038,18 @@
1.13    "\<delta> (NDvd i (CN 0 c e)) = i"
1.14    "\<delta> p = 1"
1.15
1.16 -recdef d\<delta> "measure size"
1.17 -  "d\<delta> (And p q) = (\<lambda> d. d\<delta> p d \<and> d\<delta> q d)"
1.18 -  "d\<delta> (Or p q) = (\<lambda> d. d\<delta> p d \<and> d\<delta> q d)"
1.19 -  "d\<delta> (Dvd i (CN 0 c e)) = (\<lambda> d. i dvd d)"
1.20 -  "d\<delta> (NDvd i (CN 0 c e)) = (\<lambda> d. i dvd d)"
1.21 -  "d\<delta> p = (\<lambda> d. True)"
1.22 +recdef d_\<delta> "measure size"
1.23 +  "d_\<delta> (And p q) = (\<lambda> d. d_\<delta> p d \<and> d_\<delta> q d)"
1.24 +  "d_\<delta> (Or p q) = (\<lambda> d. d_\<delta> p d \<and> d_\<delta> q d)"
1.25 +  "d_\<delta> (Dvd i (CN 0 c e)) = (\<lambda> d. i dvd d)"
1.26 +  "d_\<delta> (NDvd i (CN 0 c e)) = (\<lambda> d. i dvd d)"
1.27 +  "d_\<delta> p = (\<lambda> d. True)"
1.28
1.29  lemma delta_mono:
1.30    assumes lin: "iszlfm p"
1.31    and d: "d dvd d'"
1.32 -  and ad: "d\<delta> p d"
1.33 -  shows "d\<delta> p d'"
1.34 +  and ad: "d_\<delta> p d"
1.35 +  shows "d_\<delta> p d'"
1.36    using lin ad d
1.37  proof(induct p rule: iszlfm.induct)
1.38    case (9 i c e)  thus ?case using d
1.39 @@ -1060,61 +1060,61 @@
1.40  qed simp_all
1.41
1.42  lemma \<delta> : assumes lin:"iszlfm p"
1.43 -  shows "d\<delta> p (\<delta> p) \<and> \<delta> p >0"
1.44 +  shows "d_\<delta> p (\<delta> p) \<and> \<delta> p >0"
1.45  using lin
1.46  proof (induct p rule: iszlfm.induct)
1.47    case (1 p q)
1.48    let ?d = "\<delta> (And p q)"
1.49    from 1 lcm_pos_int have dp: "?d >0" by simp
1.50    have d1: "\<delta> p dvd \<delta> (And p q)" using 1 by simp
1.51 -  hence th: "d\<delta> p ?d" using delta_mono 1(2,3) by(simp only: iszlfm.simps)
1.52 +  hence th: "d_\<delta> p ?d" using delta_mono 1(2,3) by(simp only: iszlfm.simps)
1.53    have "\<delta> q dvd \<delta> (And p q)" using 1 by simp
1.54 -  hence th': "d\<delta> q ?d" using delta_mono 1 by(simp only: iszlfm.simps)
1.55 +  hence th': "d_\<delta> q ?d" using delta_mono 1 by(simp only: iszlfm.simps)
1.56    from th th' dp show ?case by simp
1.57  next
1.58    case (2 p q)
1.59    let ?d = "\<delta> (And p q)"
1.60    from 2 lcm_pos_int have dp: "?d >0" by simp
1.61    have "\<delta> p dvd \<delta> (And p q)" using 2 by simp
1.62 -  hence th: "d\<delta> p ?d" using delta_mono 2 by(simp only: iszlfm.simps)
1.63 +  hence th: "d_\<delta> p ?d" using delta_mono 2 by(simp only: iszlfm.simps)
1.64    have "\<delta> q dvd \<delta> (And p q)" using 2 by simp
1.65 -  hence th': "d\<delta> q ?d" using delta_mono 2 by(simp only: iszlfm.simps)
1.66 +  hence th': "d_\<delta> q ?d" using delta_mono 2 by(simp only: iszlfm.simps)
1.67    from th th' dp show ?case by simp
1.68  qed simp_all
1.69
1.70
1.71  consts
1.72 -  a\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" (* adjusts the coeffitients of a formula *)
1.73 -  d\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool" (* tests if all coeffs c of c divide a given l*)
1.74 +  a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" (* adjusts the coeffitients of a formula *)
1.75 +  d_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool" (* tests if all coeffs c of c divide a given l*)
1.76    \<zeta>  :: "fm \<Rightarrow> int" (* computes the lcm of all coefficients of x*)
1.77    \<beta> :: "fm \<Rightarrow> num list"
1.78    \<alpha> :: "fm \<Rightarrow> num list"
1.79
1.80 -recdef a\<beta> "measure size"
1.81 -  "a\<beta> (And p q) = (\<lambda> k. And (a\<beta> p k) (a\<beta> q k))"
1.82 -  "a\<beta> (Or p q) = (\<lambda> k. Or (a\<beta> p k) (a\<beta> q k))"
1.83 -  "a\<beta> (Eq  (CN 0 c e)) = (\<lambda> k. Eq (CN 0 1 (Mul (k div c) e)))"
1.84 -  "a\<beta> (NEq (CN 0 c e)) = (\<lambda> k. NEq (CN 0 1 (Mul (k div c) e)))"
1.85 -  "a\<beta> (Lt  (CN 0 c e)) = (\<lambda> k. Lt (CN 0 1 (Mul (k div c) e)))"
1.86 -  "a\<beta> (Le  (CN 0 c e)) = (\<lambda> k. Le (CN 0 1 (Mul (k div c) e)))"
1.87 -  "a\<beta> (Gt  (CN 0 c e)) = (\<lambda> k. Gt (CN 0 1 (Mul (k div c) e)))"
1.88 -  "a\<beta> (Ge  (CN 0 c e)) = (\<lambda> k. Ge (CN 0 1 (Mul (k div c) e)))"
1.89 -  "a\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
1.90 -  "a\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
1.91 -  "a\<beta> p = (\<lambda> k. p)"
1.92 +recdef a_\<beta> "measure size"
1.93 +  "a_\<beta> (And p q) = (\<lambda> k. And (a_\<beta> p k) (a_\<beta> q k))"
1.94 +  "a_\<beta> (Or p q) = (\<lambda> k. Or (a_\<beta> p k) (a_\<beta> q k))"
1.95 +  "a_\<beta> (Eq  (CN 0 c e)) = (\<lambda> k. Eq (CN 0 1 (Mul (k div c) e)))"
1.96 +  "a_\<beta> (NEq (CN 0 c e)) = (\<lambda> k. NEq (CN 0 1 (Mul (k div c) e)))"
1.97 +  "a_\<beta> (Lt  (CN 0 c e)) = (\<lambda> k. Lt (CN 0 1 (Mul (k div c) e)))"
1.98 +  "a_\<beta> (Le  (CN 0 c e)) = (\<lambda> k. Le (CN 0 1 (Mul (k div c) e)))"
1.99 +  "a_\<beta> (Gt  (CN 0 c e)) = (\<lambda> k. Gt (CN 0 1 (Mul (k div c) e)))"
1.100 +  "a_\<beta> (Ge  (CN 0 c e)) = (\<lambda> k. Ge (CN 0 1 (Mul (k div c) e)))"
1.101 +  "a_\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
1.102 +  "a_\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
1.103 +  "a_\<beta> p = (\<lambda> k. p)"
1.104
1.105 -recdef d\<beta> "measure size"
1.106 -  "d\<beta> (And p q) = (\<lambda> k. (d\<beta> p k) \<and> (d\<beta> q k))"
1.107 -  "d\<beta> (Or p q) = (\<lambda> k. (d\<beta> p k) \<and> (d\<beta> q k))"
1.108 -  "d\<beta> (Eq  (CN 0 c e)) = (\<lambda> k. c dvd k)"
1.109 -  "d\<beta> (NEq (CN 0 c e)) = (\<lambda> k. c dvd k)"
1.110 -  "d\<beta> (Lt  (CN 0 c e)) = (\<lambda> k. c dvd k)"
1.111 -  "d\<beta> (Le  (CN 0 c e)) = (\<lambda> k. c dvd k)"
1.112 -  "d\<beta> (Gt  (CN 0 c e)) = (\<lambda> k. c dvd k)"
1.113 -  "d\<beta> (Ge  (CN 0 c e)) = (\<lambda> k. c dvd k)"
1.114 -  "d\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. c dvd k)"
1.115 -  "d\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. c dvd k)"
1.116 -  "d\<beta> p = (\<lambda> k. True)"
1.117 +recdef d_\<beta> "measure size"
1.118 +  "d_\<beta> (And p q) = (\<lambda> k. (d_\<beta> p k) \<and> (d_\<beta> q k))"
1.119 +  "d_\<beta> (Or p q) = (\<lambda> k. (d_\<beta> p k) \<and> (d_\<beta> q k))"
1.120 +  "d_\<beta> (Eq  (CN 0 c e)) = (\<lambda> k. c dvd k)"
1.121 +  "d_\<beta> (NEq (CN 0 c e)) = (\<lambda> k. c dvd k)"
1.122 +  "d_\<beta> (Lt  (CN 0 c e)) = (\<lambda> k. c dvd k)"
1.123 +  "d_\<beta> (Le  (CN 0 c e)) = (\<lambda> k. c dvd k)"
1.124 +  "d_\<beta> (Gt  (CN 0 c e)) = (\<lambda> k. c dvd k)"
1.125 +  "d_\<beta> (Ge  (CN 0 c e)) = (\<lambda> k. c dvd k)"
1.126 +  "d_\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. c dvd k)"
1.127 +  "d_\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. c dvd k)"
1.128 +  "d_\<beta> p = (\<lambda> k. True)"
1.129
1.130  recdef \<zeta> "measure size"
1.131    "\<zeta> (And p q) = lcm (\<zeta> p) (\<zeta> q)"
1.132 @@ -1169,7 +1169,7 @@
1.133
1.134  lemma minusinf_inf:
1.135    assumes linp: "iszlfm p"
1.136 -  and u: "d\<beta> p 1"
1.137 +  and u: "d_\<beta> p 1"
1.138    shows "\<exists> (z::int). \<forall> x < z. Ifm bbs (x#bs) (minusinf p) = Ifm bbs (x#bs) p"
1.139    (is "?P p" is "\<exists> (z::int). \<forall> x < z. ?I x (?M p) = ?I x p")
1.140  using linp u
1.141 @@ -1242,7 +1242,7 @@
1.142  qed auto
1.143
1.144  lemma minusinf_repeats:
1.145 -  assumes d: "d\<delta> p d" and linp: "iszlfm p"
1.146 +  assumes d: "d_\<delta> p d" and linp: "iszlfm p"
1.147    shows "Ifm bbs ((x - k*d)#bs) (minusinf p) = Ifm bbs (x #bs) (minusinf p)"
1.148  using linp d
1.149  proof(induct p rule: iszlfm.induct)
1.150 @@ -1301,7 +1301,7 @@
1.151      qed
1.152  qed (auto simp add: gr0_conv_Suc numbound0_I[where bs="bs" and b="x - k*d" and b'="x"])
1.153
1.154 -lemma mirror\<alpha>\<beta>:
1.155 +lemma mirror_\<alpha>_\<beta>:
1.156    assumes lp: "iszlfm p"
1.157    shows "(Inum (i#bs)) ` set (\<alpha> p) = (Inum (i#bs)) ` set (\<beta> (mirror p))"
1.158  using lp
1.159 @@ -1337,8 +1337,8 @@
1.160    finally show ?case by simp
1.161  qed (auto simp add: numbound0_I[where bs="bs" and b="x" and b'="- x"] gr0_conv_Suc)
1.162
1.163 -lemma mirror_l: "iszlfm p \<and> d\<beta> p 1
1.164 -  \<Longrightarrow> iszlfm (mirror p) \<and> d\<beta> (mirror p) 1"
1.165 +lemma mirror_l: "iszlfm p \<and> d_\<beta> p 1
1.166 +  \<Longrightarrow> iszlfm (mirror p) \<and> d_\<beta> (mirror p) 1"
1.167    by (induct p rule: mirror.induct) auto
1.168
1.169  lemma mirror_\<delta>: "iszlfm p \<Longrightarrow> \<delta> (mirror p) = \<delta> p"
1.170 @@ -1348,11 +1348,11 @@
1.171    shows "\<forall> b\<in> set (\<beta> p). numbound0 b"
1.172    using lp by (induct p rule: \<beta>.induct) auto
1.173
1.174 -lemma d\<beta>_mono:
1.175 +lemma d_\<beta>_mono:
1.176    assumes linp: "iszlfm p"
1.177 -  and dr: "d\<beta> p l"
1.178 +  and dr: "d_\<beta> p l"
1.179    and d: "l dvd l'"
1.180 -  shows "d\<beta> p l'"
1.181 +  shows "d_\<beta> p l'"
1.182  using dr linp dvd_trans[of _ "l" "l'", simplified d]
1.183    by (induct p rule: iszlfm.induct) simp_all
1.184
1.185 @@ -1363,26 +1363,26 @@
1.186
1.187  lemma \<zeta>:
1.188    assumes linp: "iszlfm p"
1.189 -  shows "\<zeta> p > 0 \<and> d\<beta> p (\<zeta> p)"
1.190 +  shows "\<zeta> p > 0 \<and> d_\<beta> p (\<zeta> p)"
1.191  using linp
1.192  proof(induct p rule: iszlfm.induct)
1.193    case (1 p q)
1.194    from 1 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
1.195    from 1 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
1.196 -  from 1 d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"]
1.197 -    d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"]
1.198 +  from 1 d_\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"]
1.199 +    d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"]
1.200      dl1 dl2 show ?case by (auto simp add: lcm_pos_int)
1.201  next
1.202    case (2 p q)
1.203    from 2 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
1.204    from 2 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
1.205 -  from 2 d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"]
1.206 -    d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"]
1.207 +  from 2 d_\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"]
1.208 +    d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"]
1.209      dl1 dl2 show ?case by (auto simp add: lcm_pos_int)
1.210  qed (auto simp add: lcm_pos_int)
1.211
1.212 -lemma a\<beta>: assumes linp: "iszlfm p" and d: "d\<beta> p l" and lp: "l > 0"
1.213 -  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.214 +lemma a_\<beta>: assumes linp: "iszlfm p" and d: "d_\<beta> p l" and lp: "l > 0"
1.215 +  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.216  using linp d
1.217  proof (induct p rule: iszlfm.induct)
1.218    case (5 c e) hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp+
1.219 @@ -1530,20 +1530,20 @@
1.220    finally show ?case using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be  mult_strict_mono[OF ldcp jp ldcp ] by (simp add: dvd_def)
1.221  qed (auto simp add: gr0_conv_Suc numbound0_I[where bs="bs" and b="(l * x)" and b'="x"])
1.222
1.223 -lemma a\<beta>_ex: assumes linp: "iszlfm p" and d: "d\<beta> p l" and lp: "l>0"
1.224 -  shows "(\<exists> x. l dvd x \<and> Ifm bbs (x #bs) (a\<beta> p l)) = (\<exists> (x::int). Ifm bbs (x#bs) p)"
1.225 +lemma a_\<beta>_ex: assumes linp: "iszlfm p" and d: "d_\<beta> p l" and lp: "l>0"
1.226 +  shows "(\<exists> x. l dvd x \<and> Ifm bbs (x #bs) (a_\<beta> p l)) = (\<exists> (x::int). Ifm bbs (x#bs) p)"
1.227    (is "(\<exists> x. l dvd x \<and> ?P x) = (\<exists> x. ?P' x)")
1.228  proof-
1.229    have "(\<exists> x. l dvd x \<and> ?P x) = (\<exists> (x::int). ?P (l*x))"
1.230      using unity_coeff_ex[where l="l" and P="?P", simplified] by simp
1.231 -  also have "\<dots> = (\<exists> (x::int). ?P' x)" using a\<beta>[OF linp d lp] by simp
1.232 +  also have "\<dots> = (\<exists> (x::int). ?P' x)" using a_\<beta>[OF linp d lp] by simp
1.233    finally show ?thesis  .
1.234  qed
1.235
1.236  lemma \<beta>:
1.237    assumes lp: "iszlfm p"
1.238 -  and u: "d\<beta> p 1"
1.239 -  and d: "d\<delta> p d"
1.240 +  and u: "d_\<beta> p 1"
1.241 +  and d: "d_\<delta> p d"
1.242    and dp: "d > 0"
1.243    and nob: "\<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists> b\<in> (Inum (a#bs)) ` set(\<beta> p). x = b + j)"
1.244    and p: "Ifm bbs (x#bs) p" (is "?P x")
1.245 @@ -1637,8 +1637,8 @@
1.246
1.247  lemma \<beta>':
1.248    assumes lp: "iszlfm p"
1.249 -  and u: "d\<beta> p 1"
1.250 -  and d: "d\<delta> p d"
1.251 +  and u: "d_\<beta> p 1"
1.252 +  and d: "d_\<delta> p d"
1.253    and dp: "d > 0"
1.254    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> Ifm bbs (x#bs) p \<longrightarrow> Ifm bbs ((x - d)#bs) p" (is "\<forall> x. ?b \<longrightarrow> ?P x \<longrightarrow> ?P (x - d)")
1.255  proof(clarify)
1.256 @@ -1672,8 +1672,8 @@
1.257
1.258  theorem cp_thm:
1.259    assumes lp: "iszlfm p"
1.260 -  and u: "d\<beta> p 1"
1.261 -  and d: "d\<delta> p d"
1.262 +  and u: "d_\<beta> p 1"
1.263 +  and d: "d_\<delta> p d"
1.264    and dp: "d > 0"
1.265    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.266    (is "(\<exists> (x::int). ?P (x)) = (\<exists> j\<in> ?D. ?M j \<or> (\<exists> b\<in> ?B. ?P (?I b + j)))")
1.267 @@ -1706,27 +1706,27 @@
1.268
1.269  lemma cp_thm':
1.270    assumes lp: "iszlfm p"
1.271 -  and up: "d\<beta> p 1" and dd: "d\<delta> p d" and dp: "d > 0"
1.272 +  and up: "d_\<beta> p 1" and dd: "d_\<delta> p d" and dp: "d > 0"
1.273    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.274    using cp_thm[OF lp up dd dp,where i="i"] by auto
1.275
1.276  definition unit :: "fm \<Rightarrow> fm \<times> num list \<times> int" where
1.277 -  "unit p \<equiv> (let p' = zlfm p ; l = \<zeta> p' ; q = And (Dvd l (CN 0 1 (C 0))) (a\<beta> p' l); d = \<delta> q;
1.278 +  "unit p \<equiv> (let p' = zlfm p ; l = \<zeta> p' ; q = And (Dvd l (CN 0 1 (C 0))) (a_\<beta> p' l); d = \<delta> q;
1.279               B = remdups (map simpnum (\<beta> q)) ; a = remdups (map simpnum (\<alpha> q))
1.280               in if length B \<le> length a then (q,B,d) else (mirror q, a,d))"
1.281
1.282  lemma unit: assumes qf: "qfree p"
1.283 -  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.284 +  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.285  proof-
1.286    fix q B d
1.287    assume qBd: "unit p = (q,B,d)"
1.288    let ?thes = "((\<exists> x. Ifm bbs (x#bs) p) = (\<exists> x. Ifm bbs (x#bs) q)) \<and>
1.289      Inum (i#bs) ` set B = Inum (i#bs) ` set (\<beta> q) \<and>
1.290 -    d\<beta> q 1 \<and> d\<delta> q d \<and> 0 < d \<and> iszlfm q \<and> (\<forall> b\<in> set B. numbound0 b)"
1.291 +    d_\<beta> q 1 \<and> d_\<delta> q d \<and> 0 < d \<and> iszlfm q \<and> (\<forall> b\<in> set B. numbound0 b)"
1.292    let ?I = "\<lambda> x p. Ifm bbs (x#bs) p"
1.293    let ?p' = "zlfm p"
1.294    let ?l = "\<zeta> ?p'"
1.295 -  let ?q = "And (Dvd ?l (CN 0 1 (C 0))) (a\<beta> ?p' ?l)"
1.296 +  let ?q = "And (Dvd ?l (CN 0 1 (C 0))) (a_\<beta> ?p' ?l)"
1.297    let ?d = "\<delta> ?q"
1.298    let ?B = "set (\<beta> ?q)"
1.299    let ?B'= "remdups (map simpnum (\<beta> ?q))"
1.300 @@ -1736,11 +1736,11 @@
1.301    have pp': "\<forall> i. ?I i ?p' = ?I i p" by auto
1.302    from conjunct2[OF zlfm_I[OF qf, where bs="bs" and i="i"]]
1.303    have lp': "iszlfm ?p'" .
1.304 -  from lp' \<zeta>[where p="?p'"] have lp: "?l >0" and dl: "d\<beta> ?p' ?l" by auto
1.305 -  from a\<beta>_ex[where p="?p'" and l="?l" and bs="bs", OF lp' dl lp] pp'
1.306 +  from lp' \<zeta>[where p="?p'"] have lp: "?l >0" and dl: "d_\<beta> ?p' ?l" by auto
1.307 +  from a_\<beta>_ex[where p="?p'" and l="?l" and bs="bs", OF lp' dl lp] pp'
1.308    have pq_ex:"(\<exists> (x::int). ?I x p) = (\<exists> x. ?I x ?q)" by simp
1.309 -  from lp' lp a\<beta>[OF lp' dl lp] have lq:"iszlfm ?q" and uq: "d\<beta> ?q 1"  by auto
1.310 -  from \<delta>[OF lq] have dp:"?d >0" and dd: "d\<delta> ?q ?d" by blast+
1.311 +  from lp' lp a_\<beta>[OF lp' dl lp] have lq:"iszlfm ?q" and uq: "d_\<beta> ?q 1"  by auto
1.312 +  from \<delta>[OF lq] have dp:"?d >0" and dd: "d_\<delta> ?q ?d" by blast+
1.313    let ?N = "\<lambda> t. Inum (i#bs) t"
1.314    have "?N ` set ?B' = ((?N o simpnum) ` ?B)" by auto
1.315    also have "\<dots> = ?N ` ?B" using simpnum_ci[where bs="i#bs"] by auto
1.316 @@ -1762,13 +1762,13 @@
1.317    {assume "\<not> (length ?B' \<le> length ?A')"
1.318      hence q:"q=mirror ?q" and "B = ?A'" and d:"d = ?d"
1.319        using qBd by (auto simp add: Let_def unit_def)
1.320 -    with AA' mirror\<alpha>\<beta>[OF lq] A_nb have b:"?N ` (set B) = ?N ` set (\<beta> q)"
1.321 +    with AA' mirror_\<alpha>_\<beta>[OF lq] A_nb have b:"?N ` (set B) = ?N ` set (\<beta> q)"
1.322        and bn: "\<forall>b\<in> set B. numbound0 b" by simp+
1.323      from mirror_ex[OF lq] pq_ex q
1.324      have pqm_eq:"(\<exists> (x::int). ?I x p) = (\<exists> (x::int). ?I x q)" by simp
1.325      from lq uq q mirror_l[where p="?q"]
1.326 -    have lq': "iszlfm q" and uq: "d\<beta> q 1" by auto
1.327 -    from \<delta>[OF lq'] mirror_\<delta>[OF lq] q d have dq:"d\<delta> q d " by auto
1.328 +    have lq': "iszlfm q" and uq: "d_\<beta> q 1" by auto
1.329 +    from \<delta>[OF lq'] mirror_\<delta>[OF lq] q d have dq:"d_\<delta> q d " by auto
1.330      from pqm_eq b bn uq lq' dp dq q dp d have ?thes by simp
1.331    }
1.332    ultimately show ?thes by blast
1.333 @@ -1803,7 +1803,7 @@
1.334    have qbf:"unit p = (?q,?B,?d)" by simp
1.335    from unit[OF qf qbf] have pq_ex: "(\<exists>(x::int). ?I x p) = (\<exists> (x::int). ?I x ?q)" and
1.336      B:"?N ` set ?B = ?N ` set (\<beta> ?q)" and
1.337 -    uq:"d\<beta> ?q 1" and dd: "d\<delta> ?q ?d" and dp: "?d > 0" and
1.338 +    uq:"d_\<beta> ?q 1" and dd: "d_\<delta> ?q ?d" and dp: "?d > 0" and
1.339      lq: "iszlfm ?q" and
1.340      Bn: "\<forall> b\<in> set ?B. numbound0 b" by auto
1.341    from zlin_qfree[OF lq] have qfq: "qfree ?q" .
```