src/HOL/Decision_Procs/MIR.thy
 changeset 50252 4aa34bd43228 parent 50241 8b0fdeeefef7 child 51143 0a2371e7ced3
```     1.1 --- a/src/HOL/Decision_Procs/MIR.thy	Wed Nov 28 15:38:12 2012 +0100
1.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Wed Nov 28 15:59:18 2012 +0100
1.3 @@ -1947,7 +1947,7 @@
1.4  text{* plusinf : Virtual substitution of @{text "+\<infinity>"}
1.5         minusinf: Virtual substitution of @{text "-\<infinity>"}
1.6         @{text "\<delta>"} Compute lcm @{text "d| Dvd d  c*x+t \<in> p"}
1.7 -       @{text "d\<delta>"} checks if a given l divides all the ds above*}
1.8 +       @{text "d_\<delta>"} checks if a given l divides all the ds above*}
1.9
1.10  fun minusinf:: "fm \<Rightarrow> fm" where
1.11    "minusinf (And p q) = conj (minusinf p) (minusinf q)"
1.12 @@ -1981,18 +1981,18 @@
1.13  | "\<delta> (NDvd i (CN 0 c e)) = i"
1.14  | "\<delta> p = 1"
1.15
1.16 -fun d\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool" where
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 +fun d_\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool" where
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 bs"
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.37  proof(induct p rule: iszlfm.induct)
1.38    case (9 i c e)  thus ?case using d
1.39 @@ -2003,26 +2003,26 @@
1.40  qed simp_all
1.41
1.42  lemma \<delta> : assumes lin:"iszlfm p bs"
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"
1.52 +  hence th: "d_\<delta> p ?d"
1.53      using delta_mono 1 by (simp only: iszlfm.simps) blast
1.54    have "\<delta> q dvd \<delta> (And p q)" using 1 by simp
1.55 -  hence th': "d\<delta> q ?d" using delta_mono 1 by (simp only: iszlfm.simps) blast
1.56 +  hence th': "d_\<delta> q ?d" using delta_mono 1 by (simp only: iszlfm.simps) blast
1.57    from th th' dp show ?case by simp
1.58  next
1.59    case (2 p q)
1.60    let ?d = "\<delta> (And p q)"
1.61    from 2 lcm_pos_int have dp: "?d >0" by simp
1.62    have "\<delta> p dvd \<delta> (And p q)" using 2 by simp
1.63 -  hence th: "d\<delta> p ?d" using delta_mono 2 by (simp only: iszlfm.simps) blast
1.64 +  hence th: "d_\<delta> p ?d" using delta_mono 2 by (simp only: iszlfm.simps) blast
1.65    have "\<delta> q dvd \<delta> (And p q)" using 2 by simp
1.66 -  hence th': "d\<delta> q ?d" using delta_mono 2 by (simp only: iszlfm.simps) blast
1.67 +  hence th': "d_\<delta> q ?d" using delta_mono 2 by (simp only: iszlfm.simps) blast
1.68    from th th' dp show ?case by simp
1.69  qed simp_all
1.70
1.71 @@ -2152,7 +2152,7 @@
1.72  qed simp_all
1.73
1.74  lemma minusinf_repeats:
1.75 -  assumes d: "d\<delta> p d" and linp: "iszlfm p (a # bs)"
1.76 +  assumes d: "d_\<delta> p d" and linp: "iszlfm p (a # bs)"
1.77    shows "Ifm ((real(x - k*d))#bs) (minusinf p) = Ifm (real x #bs) (minusinf p)"
1.78  using linp d
1.79  proof(induct p rule: iszlfm.induct)
1.80 @@ -2218,7 +2218,7 @@
1.81  proof-
1.82    let ?d = "\<delta> p"
1.83    from \<delta> [OF lin] have dpos: "?d >0" by simp
1.84 -  from \<delta> [OF lin] have alld: "d\<delta> p ?d" by simp
1.85 +  from \<delta> [OF lin] have alld: "d_\<delta> p ?d" by simp
1.86    from minusinf_repeats[OF alld lin] have th1:"\<forall> x k. ?P1 x = ?P1 (x - (k * ?d))" by simp
1.87    from minusinf_inf[OF lin] have th2:"\<exists> z. \<forall> x. x<z \<longrightarrow> (?P x = ?P1 x)" by blast
1.88    from minusinfinity [OF dpos th1 th2] exmi show ?thesis by blast
1.89 @@ -2232,7 +2232,7 @@
1.90  proof-
1.91    let ?d = "\<delta> p"
1.92    from \<delta> [OF lin] have dpos: "?d >0" by simp
1.93 -  from \<delta> [OF lin] have alld: "d\<delta> p ?d" by simp
1.94 +  from \<delta> [OF lin] have alld: "d_\<delta> p ?d" by simp
1.95    from minusinf_repeats[OF alld lin] have th1:"\<forall> x k. ?P x = ?P (x - (k * ?d))" by simp
1.96    from periodic_finite_ex[OF dpos th1] show ?thesis by blast
1.97  qed
1.98 @@ -2240,37 +2240,37 @@
1.99  lemma dvd1_eq1: "x >0 \<Longrightarrow> (x::int) dvd 1 = (x = 1)" by auto
1.100
1.101  consts
1.102 -  a\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" (* adjusts the coeffitients of a formula *)
1.103 -  d\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool" (* tests if all coeffs c of c divide a given l*)
1.104 +  a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" (* adjusts the coeffitients of a formula *)
1.105 +  d_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool" (* tests if all coeffs c of c divide a given l*)
1.106    \<zeta>  :: "fm \<Rightarrow> int" (* computes the lcm of all coefficients of x*)
1.107    \<beta> :: "fm \<Rightarrow> num list"
1.108    \<alpha> :: "fm \<Rightarrow> num list"
1.109
1.110 -recdef a\<beta> "measure size"
1.111 -  "a\<beta> (And p q) = (\<lambda> k. And (a\<beta> p k) (a\<beta> q k))"
1.112 -  "a\<beta> (Or p q) = (\<lambda> k. Or (a\<beta> p k) (a\<beta> q k))"
1.113 -  "a\<beta> (Eq  (CN 0 c e)) = (\<lambda> k. Eq (CN 0 1 (Mul (k div c) e)))"
1.114 -  "a\<beta> (NEq (CN 0 c e)) = (\<lambda> k. NEq (CN 0 1 (Mul (k div c) e)))"
1.115 -  "a\<beta> (Lt  (CN 0 c e)) = (\<lambda> k. Lt (CN 0 1 (Mul (k div c) e)))"
1.116 -  "a\<beta> (Le  (CN 0 c e)) = (\<lambda> k. Le (CN 0 1 (Mul (k div c) e)))"
1.117 -  "a\<beta> (Gt  (CN 0 c e)) = (\<lambda> k. Gt (CN 0 1 (Mul (k div c) e)))"
1.118 -  "a\<beta> (Ge  (CN 0 c e)) = (\<lambda> k. Ge (CN 0 1 (Mul (k div c) e)))"
1.119 -  "a\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
1.120 -  "a\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
1.121 -  "a\<beta> p = (\<lambda> k. p)"
1.122 -
1.123 -recdef d\<beta> "measure size"
1.124 -  "d\<beta> (And p q) = (\<lambda> k. (d\<beta> p k) \<and> (d\<beta> q k))"
1.125 -  "d\<beta> (Or p q) = (\<lambda> k. (d\<beta> p k) \<and> (d\<beta> q k))"
1.126 -  "d\<beta> (Eq  (CN 0 c e)) = (\<lambda> k. c dvd k)"
1.127 -  "d\<beta> (NEq (CN 0 c e)) = (\<lambda> k. c dvd k)"
1.128 -  "d\<beta> (Lt  (CN 0 c e)) = (\<lambda> k. c dvd k)"
1.129 -  "d\<beta> (Le  (CN 0 c e)) = (\<lambda> k. c dvd k)"
1.130 -  "d\<beta> (Gt  (CN 0 c e)) = (\<lambda> k. c dvd k)"
1.131 -  "d\<beta> (Ge  (CN 0 c e)) = (\<lambda> k. c dvd k)"
1.132 -  "d\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. c dvd k)"
1.133 -  "d\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. c dvd k)"
1.134 -  "d\<beta> p = (\<lambda> k. True)"
1.135 +recdef a_\<beta> "measure size"
1.136 +  "a_\<beta> (And p q) = (\<lambda> k. And (a_\<beta> p k) (a_\<beta> q k))"
1.137 +  "a_\<beta> (Or p q) = (\<lambda> k. Or (a_\<beta> p k) (a_\<beta> q k))"
1.138 +  "a_\<beta> (Eq  (CN 0 c e)) = (\<lambda> k. Eq (CN 0 1 (Mul (k div c) e)))"
1.139 +  "a_\<beta> (NEq (CN 0 c e)) = (\<lambda> k. NEq (CN 0 1 (Mul (k div c) e)))"
1.140 +  "a_\<beta> (Lt  (CN 0 c e)) = (\<lambda> k. Lt (CN 0 1 (Mul (k div c) e)))"
1.141 +  "a_\<beta> (Le  (CN 0 c e)) = (\<lambda> k. Le (CN 0 1 (Mul (k div c) e)))"
1.142 +  "a_\<beta> (Gt  (CN 0 c e)) = (\<lambda> k. Gt (CN 0 1 (Mul (k div c) e)))"
1.143 +  "a_\<beta> (Ge  (CN 0 c e)) = (\<lambda> k. Ge (CN 0 1 (Mul (k div c) e)))"
1.144 +  "a_\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
1.145 +  "a_\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
1.146 +  "a_\<beta> p = (\<lambda> k. p)"
1.147 +
1.148 +recdef d_\<beta> "measure size"
1.149 +  "d_\<beta> (And p q) = (\<lambda> k. (d_\<beta> p k) \<and> (d_\<beta> q k))"
1.150 +  "d_\<beta> (Or p q) = (\<lambda> k. (d_\<beta> p k) \<and> (d_\<beta> q k))"
1.151 +  "d_\<beta> (Eq  (CN 0 c e)) = (\<lambda> k. c dvd k)"
1.152 +  "d_\<beta> (NEq (CN 0 c e)) = (\<lambda> k. c dvd k)"
1.153 +  "d_\<beta> (Lt  (CN 0 c e)) = (\<lambda> k. c dvd k)"
1.154 +  "d_\<beta> (Le  (CN 0 c e)) = (\<lambda> k. c dvd k)"
1.155 +  "d_\<beta> (Gt  (CN 0 c e)) = (\<lambda> k. c dvd k)"
1.156 +  "d_\<beta> (Ge  (CN 0 c e)) = (\<lambda> k. c dvd k)"
1.157 +  "d_\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. c dvd k)"
1.158 +  "d_\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. c dvd k)"
1.159 +  "d_\<beta> p = (\<lambda> k. True)"
1.160
1.161  recdef \<zeta> "measure size"
1.162    "\<zeta> (And p q) = lcm (\<zeta> p) (\<zeta> q)"
1.163 @@ -2320,7 +2320,7 @@
1.164    "mirror (NDvd i (CN 0 c e)) = NDvd i (CN 0 c (Neg e))"
1.165    "mirror p = p"
1.166
1.167 -lemma mirror\<alpha>\<beta>:
1.168 +lemma mirror_\<alpha>_\<beta>:
1.169    assumes lp: "iszlfm p (a#bs)"
1.170    shows "(Inum (real (i::int)#bs)) ` set (\<alpha> p) = (Inum (real i#bs)) ` set (\<beta> (mirror p))"
1.171  using lp
1.172 @@ -2351,8 +2351,8 @@
1.173  lemma mirror_l: "iszlfm p (a#bs) \<Longrightarrow> iszlfm (mirror p) (a#bs)"
1.174  by (induct p rule: mirror.induct, auto simp add: isint_neg)
1.175
1.176 -lemma mirror_d\<beta>: "iszlfm p (a#bs) \<and> d\<beta> p 1
1.177 -  \<Longrightarrow> iszlfm (mirror p) (a#bs) \<and> d\<beta> (mirror p) 1"
1.178 +lemma mirror_d_\<beta>: "iszlfm p (a#bs) \<and> d_\<beta> p 1
1.179 +  \<Longrightarrow> iszlfm (mirror p) (a#bs) \<and> d_\<beta> (mirror p) 1"
1.180  by (induct p rule: mirror.induct, auto simp add: isint_neg)
1.181
1.182  lemma mirror_\<delta>: "iszlfm p (a#bs) \<Longrightarrow> \<delta> (mirror p) = \<delta> p"
1.183 @@ -2376,11 +2376,11 @@
1.184    shows "\<forall> b\<in> set (\<beta> p). numbound0 b"
1.185    using lp by (induct p rule: \<beta>.induct,auto)
1.186
1.187 -lemma d\<beta>_mono:
1.188 +lemma d_\<beta>_mono:
1.189    assumes linp: "iszlfm p (a #bs)"
1.190 -  and dr: "d\<beta> p l"
1.191 +  and dr: "d_\<beta> p l"
1.192    and d: "l dvd l'"
1.193 -  shows "d\<beta> p l'"
1.194 +  shows "d_\<beta> p l'"
1.195  using dr linp dvd_trans[of _ "l" "l'", simplified d]
1.196  by (induct p rule: iszlfm.induct) simp_all
1.197
1.198 @@ -2391,26 +2391,26 @@
1.199
1.200  lemma \<zeta>:
1.201    assumes linp: "iszlfm p (a #bs)"
1.202 -  shows "\<zeta> p > 0 \<and> d\<beta> p (\<zeta> p)"
1.203 +  shows "\<zeta> p > 0 \<and> d_\<beta> p (\<zeta> p)"
1.204  using linp
1.205  proof(induct p rule: iszlfm.induct)
1.206    case (1 p q)
1.207    then  have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
1.208    from 1 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
1.209 -  from 1 d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"]
1.210 -    d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"]
1.211 +  from 1 d_\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"]
1.212 +    d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"]
1.213      dl1 dl2 show ?case by (auto simp add: lcm_pos_int)
1.214  next
1.215    case (2 p q)
1.216    then have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
1.217    from 2 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
1.218 -  from 2 d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"]
1.219 -    d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"]
1.220 +  from 2 d_\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"]
1.221 +    d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"]
1.222      dl1 dl2 show ?case by (auto simp add: lcm_pos_int)
1.223  qed (auto simp add: lcm_pos_int)
1.224
1.225 -lemma a\<beta>: assumes linp: "iszlfm p (a #bs)" and d: "d\<beta> p l" and lp: "l > 0"
1.226 -  shows "iszlfm (a\<beta> p l) (a #bs) \<and> d\<beta> (a\<beta> p l) 1 \<and> (Ifm (real (l * x) #bs) (a\<beta> p l) = Ifm ((real x)#bs) p)"
1.227 +lemma a_\<beta>: assumes linp: "iszlfm p (a #bs)" and d: "d_\<beta> p l" and lp: "l > 0"
1.228 +  shows "iszlfm (a_\<beta> p l) (a #bs) \<and> d_\<beta> (a_\<beta> p l) 1 \<and> (Ifm (real (l * x) #bs) (a_\<beta> p l) = Ifm ((real x)#bs) p)"
1.229  using linp d
1.230  proof (induct p rule: iszlfm.induct)
1.231    case (5 c e) hence cp: "c>0" and be: "numbound0 e" and ei:"isint e (a#bs)" and d': "c dvd l" by simp+
1.232 @@ -2556,20 +2556,20 @@
1.233    finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"] rdvd_def  be  isint_Mul[OF ei]  mult_strict_mono[OF ldcp jp ldcp ] by simp
1.234  qed (simp_all add: numbound0_I[where bs="bs" and b="real (l * x)" and b'="real x"] isint_Mul del: real_of_int_mult)
1.235
1.236 -lemma a\<beta>_ex: assumes linp: "iszlfm p (a#bs)" and d: "d\<beta> p l" and lp: "l>0"
1.237 -  shows "(\<exists> x. l dvd x \<and> Ifm (real x #bs) (a\<beta> p l)) = (\<exists> (x::int). Ifm (real x#bs) p)"
1.238 +lemma a_\<beta>_ex: assumes linp: "iszlfm p (a#bs)" and d: "d_\<beta> p l" and lp: "l>0"
1.239 +  shows "(\<exists> x. l dvd x \<and> Ifm (real x #bs) (a_\<beta> p l)) = (\<exists> (x::int). Ifm (real x#bs) p)"
1.240    (is "(\<exists> x. l dvd x \<and> ?P x) = (\<exists> x. ?P' x)")
1.241  proof-
1.242    have "(\<exists> x. l dvd x \<and> ?P x) = (\<exists> (x::int). ?P (l*x))"
1.243      using unity_coeff_ex[where l="l" and P="?P", simplified] by simp
1.244 -  also have "\<dots> = (\<exists> (x::int). ?P' x)" using a\<beta>[OF linp d lp] by simp
1.245 +  also have "\<dots> = (\<exists> (x::int). ?P' x)" using a_\<beta>[OF linp d lp] by simp
1.246    finally show ?thesis  .
1.247  qed
1.248
1.249  lemma \<beta>:
1.250    assumes lp: "iszlfm p (a#bs)"
1.251 -  and u: "d\<beta> p 1"
1.252 -  and d: "d\<delta> p d"
1.253 +  and u: "d_\<beta> p 1"
1.254 +  and d: "d_\<delta> p d"
1.255    and dp: "d > 0"
1.256    and nob: "\<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists> b\<in> (Inum (a#bs)) ` set(\<beta> p). real x = b + real j)"
1.257    and p: "Ifm (real x#bs) p" (is "?P x")
1.258 @@ -2705,8 +2705,8 @@
1.259
1.260  lemma \<beta>':
1.261    assumes lp: "iszlfm p (a #bs)"
1.262 -  and u: "d\<beta> p 1"
1.263 -  and d: "d\<delta> p d"
1.264 +  and u: "d_\<beta> p 1"
1.265 +  and d: "d_\<delta> p d"
1.266    and dp: "d > 0"
1.267    shows "\<forall> x. \<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists> b\<in> set(\<beta> p). Ifm ((Inum (a#bs) b + real j) #bs) p) \<longrightarrow> Ifm (real x#bs) p \<longrightarrow> Ifm (real (x - d)#bs) p" (is "\<forall> x. ?b \<longrightarrow> ?P x \<longrightarrow> ?P (x - d)")
1.268  proof(clarify)
1.269 @@ -2746,8 +2746,8 @@
1.270
1.271  theorem cp_thm:
1.272    assumes lp: "iszlfm p (a #bs)"
1.273 -  and u: "d\<beta> p 1"
1.274 -  and d: "d\<delta> p d"
1.275 +  and u: "d_\<beta> p 1"
1.276 +  and d: "d_\<delta> p d"
1.277    and dp: "d > 0"
1.278    shows "(\<exists> (x::int). Ifm (real x #bs) p) = (\<exists> j\<in> {1.. d}. Ifm (real j #bs) (minusinf p) \<or> (\<exists> b \<in> set (\<beta> p). Ifm ((Inum (a#bs) b + real j) #bs) p))"
1.279    (is "(\<exists> (x::int). ?P (real x)) = (\<exists> j\<in> ?D. ?M j \<or> (\<exists> b\<in> ?B. ?P (?I b + real j)))")
1.280 @@ -2775,9 +2775,9 @@
1.281
1.282  consts
1.283    \<rho> :: "fm \<Rightarrow> (num \<times> int) list" (* Compute the Reddy and Loveland Bset*)
1.284 -  \<sigma>\<rho>:: "fm \<Rightarrow> num \<times> int \<Rightarrow> fm" (* Performs the modified substitution of Reddy and Loveland*)
1.285 -  \<alpha>\<rho> :: "fm \<Rightarrow> (num\<times>int) list"
1.286 -  a\<rho> :: "fm \<Rightarrow> int \<Rightarrow> fm"
1.287 +  \<sigma>_\<rho>:: "fm \<Rightarrow> num \<times> int \<Rightarrow> fm" (* Performs the modified substitution of Reddy and Loveland*)
1.288 +  \<alpha>_\<rho> :: "fm \<Rightarrow> (num\<times>int) list"
1.289 +  a_\<rho> :: "fm \<Rightarrow> int \<Rightarrow> fm"
1.290  recdef \<rho> "measure size"
1.291    "\<rho> (And p q) = (\<rho> p @ \<rho> q)"
1.292    "\<rho> (Or p q) = (\<rho> p @ \<rho> q)"
1.293 @@ -2789,52 +2789,52 @@
1.294    "\<rho> (Ge  (CN 0 c e)) = [(Sub (C (-1)) e, c)]"
1.295    "\<rho> p = []"
1.296
1.297 -recdef \<sigma>\<rho> "measure size"
1.298 -  "\<sigma>\<rho> (And p q) = (\<lambda> (t,k). And (\<sigma>\<rho> p (t,k)) (\<sigma>\<rho> q (t,k)))"
1.299 -  "\<sigma>\<rho> (Or p q) = (\<lambda> (t,k). Or (\<sigma>\<rho> p (t,k)) (\<sigma>\<rho> q (t,k)))"
1.300 -  "\<sigma>\<rho> (Eq  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Eq (Add (Mul (c div k) t) e))
1.301 +recdef \<sigma>_\<rho> "measure size"
1.302 +  "\<sigma>_\<rho> (And p q) = (\<lambda> (t,k). And (\<sigma>_\<rho> p (t,k)) (\<sigma>_\<rho> q (t,k)))"
1.303 +  "\<sigma>_\<rho> (Or p q) = (\<lambda> (t,k). Or (\<sigma>_\<rho> p (t,k)) (\<sigma>_\<rho> q (t,k)))"
1.304 +  "\<sigma>_\<rho> (Eq  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Eq (Add (Mul (c div k) t) e))
1.305                                              else (Eq (Add (Mul c t) (Mul k e))))"
1.306 -  "\<sigma>\<rho> (NEq (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (NEq (Add (Mul (c div k) t) e))
1.307 +  "\<sigma>_\<rho> (NEq (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (NEq (Add (Mul (c div k) t) e))
1.308                                              else (NEq (Add (Mul c t) (Mul k e))))"
1.309 -  "\<sigma>\<rho> (Lt  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Lt (Add (Mul (c div k) t) e))
1.310 +  "\<sigma>_\<rho> (Lt  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Lt (Add (Mul (c div k) t) e))
1.311                                              else (Lt (Add (Mul c t) (Mul k e))))"
1.312 -  "\<sigma>\<rho> (Le  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Le (Add (Mul (c div k) t) e))
1.313 +  "\<sigma>_\<rho> (Le  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Le (Add (Mul (c div k) t) e))
1.314                                              else (Le (Add (Mul c t) (Mul k e))))"
1.315 -  "\<sigma>\<rho> (Gt  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Gt (Add (Mul (c div k) t) e))
1.316 +  "\<sigma>_\<rho> (Gt  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Gt (Add (Mul (c div k) t) e))
1.317                                              else (Gt (Add (Mul c t) (Mul k e))))"
1.318 -  "\<sigma>\<rho> (Ge  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Ge (Add (Mul (c div k) t) e))
1.319 +  "\<sigma>_\<rho> (Ge  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Ge (Add (Mul (c div k) t) e))
1.320                                              else (Ge (Add (Mul c t) (Mul k e))))"
1.321 -  "\<sigma>\<rho> (Dvd i (CN 0 c e)) =(\<lambda> (t,k). if k dvd c then (Dvd i (Add (Mul (c div k) t) e))
1.322 +  "\<sigma>_\<rho> (Dvd i (CN 0 c e)) =(\<lambda> (t,k). if k dvd c then (Dvd i (Add (Mul (c div k) t) e))
1.323                                              else (Dvd (i*k) (Add (Mul c t) (Mul k e))))"
1.324 -  "\<sigma>\<rho> (NDvd i (CN 0 c e))=(\<lambda> (t,k). if k dvd c then (NDvd i (Add (Mul (c div k) t) e))
1.325 +  "\<sigma>_\<rho> (NDvd i (CN 0 c e))=(\<lambda> (t,k). if k dvd c then (NDvd i (Add (Mul (c div k) t) e))
1.326                                              else (NDvd (i*k) (Add (Mul c t) (Mul k e))))"
1.327 -  "\<sigma>\<rho> p = (\<lambda> (t,k). p)"
1.328 -
1.329 -recdef \<alpha>\<rho> "measure size"
1.330 -  "\<alpha>\<rho> (And p q) = (\<alpha>\<rho> p @ \<alpha>\<rho> q)"
1.331 -  "\<alpha>\<rho> (Or p q) = (\<alpha>\<rho> p @ \<alpha>\<rho> q)"
1.332 -  "\<alpha>\<rho> (Eq  (CN 0 c e)) = [(Add (C -1) e,c)]"
1.333 -  "\<alpha>\<rho> (NEq (CN 0 c e)) = [(e,c)]"
1.334 -  "\<alpha>\<rho> (Lt  (CN 0 c e)) = [(e,c)]"
1.335 -  "\<alpha>\<rho> (Le  (CN 0 c e)) = [(Add (C -1) e,c)]"
1.336 -  "\<alpha>\<rho> p = []"
1.337 +  "\<sigma>_\<rho> p = (\<lambda> (t,k). p)"
1.338 +
1.339 +recdef \<alpha>_\<rho> "measure size"
1.340 +  "\<alpha>_\<rho> (And p q) = (\<alpha>_\<rho> p @ \<alpha>_\<rho> q)"
1.341 +  "\<alpha>_\<rho> (Or p q) = (\<alpha>_\<rho> p @ \<alpha>_\<rho> q)"
1.342 +  "\<alpha>_\<rho> (Eq  (CN 0 c e)) = [(Add (C -1) e,c)]"
1.343 +  "\<alpha>_\<rho> (NEq (CN 0 c e)) = [(e,c)]"
1.344 +  "\<alpha>_\<rho> (Lt  (CN 0 c e)) = [(e,c)]"
1.345 +  "\<alpha>_\<rho> (Le  (CN 0 c e)) = [(Add (C -1) e,c)]"
1.346 +  "\<alpha>_\<rho> p = []"
1.347
1.348      (* Simulates normal substituion by modifying the formula see correctness theorem *)
1.349
1.350  definition \<sigma> :: "fm \<Rightarrow> int \<Rightarrow> num \<Rightarrow> fm" where
1.351 -  "\<sigma> p k t \<equiv> And (Dvd k t) (\<sigma>\<rho> p (t,k))"
1.352 -
1.353 -lemma \<sigma>\<rho>:
1.354 +  "\<sigma> p k t \<equiv> And (Dvd k t) (\<sigma>_\<rho> p (t,k))"
1.355 +
1.356 +lemma \<sigma>_\<rho>:
1.357    assumes linp: "iszlfm p (real (x::int)#bs)"
1.358    and kpos: "real k > 0"
1.359    and tnb: "numbound0 t"
1.360    and tint: "isint t (real x#bs)"
1.361    and kdt: "k dvd floor (Inum (b'#bs) t)"
1.362 -  shows "Ifm (real x#bs) (\<sigma>\<rho> p (t,k)) =
1.363 +  shows "Ifm (real x#bs) (\<sigma>_\<rho> p (t,k)) =
1.364    (Ifm ((real ((floor (Inum (b'#bs) t)) div k))#bs) p)"
1.365    (is "?I (real x) (?s p) = (?I (real ((floor (?N b' t)) div k)) p)" is "_ = (?I ?tk p)")
1.366  using linp kpos tnb
1.367 -proof(induct p rule: \<sigma>\<rho>.induct)
1.368 +proof(induct p rule: \<sigma>_\<rho>.induct)
1.369    case (3 c e)
1.370    from 3 have cp: "c > 0" and nb: "numbound0 e" by auto
1.371    { assume kdc: "k dvd c"
1.372 @@ -3033,8 +3033,8 @@
1.373    numbound0_I[where bs="bs" and b="real ((floor (?N b' t)) div k)" and b'="real x"])
1.374
1.375
1.376 -lemma \<sigma>\<rho>_nb: assumes lp:"iszlfm p (a#bs)" and nb: "numbound0 t"
1.377 -  shows "bound0 (\<sigma>\<rho> p (t,k))"
1.378 +lemma \<sigma>_\<rho>_nb: assumes lp:"iszlfm p (a#bs)" and nb: "numbound0 t"
1.379 +  shows "bound0 (\<sigma>_\<rho> p (t,k))"
1.380    using lp
1.381    by (induct p rule: iszlfm.induct, auto simp add: nb)
1.382
1.383 @@ -3043,15 +3043,15 @@
1.384    shows "\<forall> (b,k) \<in> set (\<rho> p). k >0 \<and> numbound0 b \<and> isint b (real i#bs)"
1.385  using lp by (induct p rule: \<rho>.induct, auto simp add: isint_sub isint_neg)
1.386
1.387 -lemma \<alpha>\<rho>_l:
1.388 +lemma \<alpha>_\<rho>_l:
1.389    assumes lp: "iszlfm p (real (i::int)#bs)"
1.390 -  shows "\<forall> (b,k) \<in> set (\<alpha>\<rho> p). k >0 \<and> numbound0 b \<and> isint b (real i#bs)"
1.391 +  shows "\<forall> (b,k) \<in> set (\<alpha>_\<rho> p). k >0 \<and> numbound0 b \<and> isint b (real i#bs)"
1.392  using lp isint_add [OF isint_c[where j="- 1"],where bs="real i#bs"]
1.393 - by (induct p rule: \<alpha>\<rho>.induct, auto)
1.394 + by (induct p rule: \<alpha>_\<rho>.induct, auto)
1.395
1.396  lemma \<rho>: assumes lp: "iszlfm p (real (i::int) #bs)"
1.397    and pi: "Ifm (real i#bs) p"
1.398 -  and d: "d\<delta> p d"
1.399 +  and d: "d_\<delta> p d"
1.400    and dp: "d > 0"
1.401    and nob: "\<forall>(e,c) \<in> set (\<rho> p). \<forall> j\<in> {1 .. c*d}. real (c*i) \<noteq> Inum (real i#bs) e + real j"
1.402    (is "\<forall>(e,c) \<in> set (\<rho> p). \<forall> j\<in> {1 .. c*d}. _ \<noteq> ?N i e + _")
1.403 @@ -3187,10 +3187,10 @@
1.404
1.405  lemma \<sigma>_nb: assumes lp: "iszlfm p (a#bs)" and nb: "numbound0 t"
1.406    shows "bound0 (\<sigma> p k t)"
1.407 -  using \<sigma>\<rho>_nb[OF lp nb] nb by (simp add: \<sigma>_def)
1.408 +  using \<sigma>_\<rho>_nb[OF lp nb] nb by (simp add: \<sigma>_def)
1.409
1.410  lemma \<rho>':   assumes lp: "iszlfm p (a #bs)"
1.411 -  and d: "d\<delta> p d"
1.412 +  and d: "d_\<delta> p d"
1.413    and dp: "d > 0"
1.414    shows "\<forall> x. \<not>(\<exists> (e,c) \<in> set(\<rho> p). \<exists>(j::int) \<in> {1 .. c*d}. Ifm (a #bs) (\<sigma> p c (Add e (C j)))) \<longrightarrow> Ifm (real x#bs) p \<longrightarrow> Ifm (real (x - d)#bs) p" (is "\<forall> x. ?b x \<longrightarrow> ?P x \<longrightarrow> ?P (x - d)")
1.415  proof(clarify)
1.416 @@ -3219,8 +3219,8 @@
1.417      from nb have nb': "numbound0 (Add e (C j))" by simp
1.418      have ji: "isint (C j) (real x#bs)" by (simp add: isint_def)
1.419      from isint_add[OF ei ji] have ei':"isint (Add e (C j)) (real x#bs)" .
1.420 -    from th \<sigma>\<rho>[where b'="real x", OF lp' cp' nb' ei' cdej',symmetric]
1.421 -    have "Ifm (real x#bs) (\<sigma>\<rho> p (Add e (C j), c))" by simp
1.422 +    from th \<sigma>_\<rho>[where b'="real x", OF lp' cp' nb' ei' cdej',symmetric]
1.423 +    have "Ifm (real x#bs) (\<sigma>_\<rho> p (Add e (C j), c))" by simp
1.424      with rcdej have th: "Ifm (real x#bs) (\<sigma> p c (Add e (C j)))" by (simp add: \<sigma>_def)
1.425      from th bound0_I[OF \<sigma>_nb[OF lp nb', where k="c"],where bs="bs" and b="real x" and b'="a"]
1.426      have "Ifm (a#bs) (\<sigma> p c (Add e (C j)))" by blast
1.427 @@ -3237,7 +3237,7 @@
1.428      is "?lhs = (?MD \<or> ?RD)"  is "?lhs = ?rhs")
1.429  proof-
1.430    let ?d= "\<delta> p"
1.431 -  from \<delta>[OF lp] have d:"d\<delta> p ?d" and dp: "?d > 0" by auto
1.432 +  from \<delta>[OF lp] have d:"d_\<delta> p ?d" and dp: "?d > 0" by auto
1.433    { assume H:"?MD" hence th:"\<exists> (x::int). ?MP x" by blast
1.434      from H minusinf_ex[OF lp th] have ?thesis  by blast}
1.435    moreover
1.436 @@ -3251,12 +3251,12 @@
1.437      from spx bound0_I[OF \<sigma>_nb[OF lp nb', where k="c"], where bs="bs" and b="a" and b'="real i"]
1.438      have spx': "Ifm (real i # bs) (\<sigma> p c (Add e (C j)))" by blast
1.439      from spx' have rcdej:"real c rdvd (Inum (real i#bs) (Add e (C j)))"
1.440 -      and sr:"Ifm (real i#bs) (\<sigma>\<rho> p (Add e (C j),c))" by (simp add: \<sigma>_def)+
1.441 +      and sr:"Ifm (real i#bs) (\<sigma>_\<rho> p (Add e (C j),c))" by (simp add: \<sigma>_def)+
1.442      from rcdej eji[simplified isint_iff]
1.443      have "real c rdvd real (floor (Inum (real i#bs) (Add e (C j))))" by simp
1.444      hence cdej:"c dvd floor (Inum (real i#bs) (Add e (C j)))" by (simp only: int_rdvd_iff)
1.445      from cp have cp': "real c > 0" by simp
1.446 -    from \<sigma>\<rho>[OF lp cp' nb' eji cdej] spx' have "?P (\<lfloor>Inum (real i # bs) (Add e (C j))\<rfloor> div c)"
1.447 +    from \<sigma>_\<rho>[OF lp cp' nb' eji cdej] spx' have "?P (\<lfloor>Inum (real i # bs) (Add e (C j))\<rfloor> div c)"
1.449      hence ?lhs by blast
1.450      with exR jD spx have ?thesis by blast}
1.451 @@ -3272,8 +3272,8 @@
1.452    ultimately show ?thesis by blast
1.453  qed
1.454
1.455 -lemma mirror_\<alpha>\<rho>:   assumes lp: "iszlfm p (a#bs)"
1.456 -  shows "(\<lambda> (t,k). (Inum (a#bs) t, k)) ` set (\<alpha>\<rho> p) = (\<lambda> (t,k). (Inum (a#bs) t,k)) ` set (\<rho> (mirror p))"
1.457 +lemma mirror_\<alpha>_\<rho>:   assumes lp: "iszlfm p (a#bs)"
1.458 +  shows "(\<lambda> (t,k). (Inum (a#bs) t, k)) ` set (\<alpha>_\<rho> p) = (\<lambda> (t,k). (Inum (a#bs) t,k)) ` set (\<rho> (mirror p))"
1.459  using lp
1.460  by (induct p rule: mirror.induct, simp_all add: split_def image_Un )
1.461
1.462 @@ -4714,7 +4714,7 @@
1.463  qed
1.464
1.465
1.466 -lemma fr_eq\<upsilon>:
1.467 +lemma fr_eq_\<upsilon>:
1.468    assumes lp: "isrlfm p"
1.469    shows "(\<exists> x. Ifm (x#bs) p) = ((Ifm (x#bs) (minusinf p)) \<or> (Ifm (x#bs) (plusinf p)) \<or> (\<exists> (t,k) \<in> set (\<Upsilon> p). \<exists> (s,l) \<in> set (\<Upsilon> p). Ifm (x#bs) (\<upsilon> p (Add(Mul l t) (Mul k s) , 2*k*l))))"
1.470    (is "(\<exists> x. ?I x p) = (?M \<or> ?P \<or> ?F)" is "?E = ?D")
1.471 @@ -4856,7 +4856,7 @@
1.472      hence lqx: "?I x ?rq " using simpfm[where p="?rq" and bs="x#bs"] by auto
1.473      from qf have qfq:"isrlfm ?rq"
1.474        by (auto simp add: rsplit_def lt_def ge_def rlfm_I[OF qf xp x1])
1.475 -    with lqx fr_eq\<upsilon>[OF qfq] show "?M \<or> ?P \<or> ?F" by blast
1.476 +    with lqx fr_eq_\<upsilon>[OF qfq] show "?M \<or> ?P \<or> ?F" by blast
1.477    next
1.478      assume D: "?D"
1.479      let ?U = "set (\<Upsilon> ?rq )"
1.480 @@ -5066,27 +5066,27 @@
1.481
1.482  lemma cp_thm':
1.483    assumes lp: "iszlfm p (real (i::int)#bs)"
1.484 -  and up: "d\<beta> p 1" and dd: "d\<delta> p d" and dp: "d > 0"
1.485 +  and up: "d_\<beta> p 1" and dd: "d_\<delta> p d" and dp: "d > 0"
1.486    shows "(\<exists> (x::int). Ifm (real x#bs) p) = ((\<exists> j\<in> {1 .. d}. Ifm (real j#bs) (minusinf p)) \<or> (\<exists> j\<in> {1.. d}. \<exists> b\<in> (Inum (real i#bs)) ` set (\<beta> p). Ifm ((b+real j)#bs) p))"
1.487    using cp_thm[OF lp up dd dp] by auto
1.488
1.489  definition unit :: "fm \<Rightarrow> fm \<times> num list \<times> int" where
1.490 -  "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.491 +  "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.492               B = remdups (map simpnum (\<beta> q)) ; a = remdups (map simpnum (\<alpha> q))
1.493               in if length B \<le> length a then (q,B,d) else (mirror q, a,d))"
1.494
1.495  lemma unit: assumes qf: "qfree p"
1.496 -  shows "\<And> q B d. unit p = (q,B,d) \<Longrightarrow> ((\<exists> (x::int). Ifm (real x#bs) p) = (\<exists> (x::int). Ifm (real x#bs) q)) \<and> (Inum (real i#bs)) ` set B = (Inum (real i#bs)) ` set (\<beta> q) \<and> d\<beta> q 1 \<and> d\<delta> q d \<and> d >0 \<and> iszlfm q (real (i::int)#bs) \<and> (\<forall> b\<in> set B. numbound0 b)"
1.497 +  shows "\<And> q B d. unit p = (q,B,d) \<Longrightarrow> ((\<exists> (x::int). Ifm (real x#bs) p) = (\<exists> (x::int). Ifm (real x#bs) q)) \<and> (Inum (real i#bs)) ` set B = (Inum (real i#bs)) ` set (\<beta> q) \<and> d_\<beta> q 1 \<and> d_\<delta> q d \<and> d >0 \<and> iszlfm q (real (i::int)#bs) \<and> (\<forall> b\<in> set B. numbound0 b)"
1.498  proof-
1.499    fix q B d
1.500    assume qBd: "unit p = (q,B,d)"
1.501    let ?thes = "((\<exists> (x::int). Ifm (real x#bs) p) = (\<exists> (x::int). Ifm (real x#bs) q)) \<and>
1.502      Inum (real i#bs) ` set B = Inum (real i#bs) ` set (\<beta> q) \<and>
1.503 -    d\<beta> q 1 \<and> d\<delta> q d \<and> 0 < d \<and> iszlfm q (real i # bs) \<and> (\<forall> b\<in> set B. numbound0 b)"
1.504 +    d_\<beta> q 1 \<and> d_\<delta> q d \<and> 0 < d \<and> iszlfm q (real i # bs) \<and> (\<forall> b\<in> set B. numbound0 b)"
1.505    let ?I = "\<lambda> (x::int) p. Ifm (real x#bs) p"
1.506    let ?p' = "zlfm p"
1.507    let ?l = "\<zeta> ?p'"
1.508 -  let ?q = "And (Dvd ?l (CN 0 1 (C 0))) (a\<beta> ?p' ?l)"
1.509 +  let ?q = "And (Dvd ?l (CN 0 1 (C 0))) (a_\<beta> ?p' ?l)"
1.510    let ?d = "\<delta> ?q"
1.511    let ?B = "set (\<beta> ?q)"
1.512    let ?B'= "remdups (map simpnum (\<beta> ?q))"
1.513 @@ -5097,12 +5097,12 @@
1.514    from iszlfm_gen[OF conjunct2[OF zlfm_I[OF qf, where bs="bs" and i="i"]]]
1.515    have lp': "\<forall> (i::int). iszlfm ?p' (real i#bs)" by simp
1.516    hence lp'': "iszlfm ?p' (real (i::int)#bs)" by simp
1.517 -  from lp' \<zeta>[where p="?p'" and bs="bs"] have lp: "?l >0" and dl: "d\<beta> ?p' ?l" by auto
1.518 -  from a\<beta>_ex[where p="?p'" and l="?l" and bs="bs", OF lp'' dl lp] pp'
1.519 +  from lp' \<zeta>[where p="?p'" and bs="bs"] have lp: "?l >0" and dl: "d_\<beta> ?p' ?l" by auto
1.520 +  from a_\<beta>_ex[where p="?p'" and l="?l" and bs="bs", OF lp'' dl lp] pp'
1.521    have pq_ex:"(\<exists> (x::int). ?I x p) = (\<exists> x. ?I x ?q)" by (simp add: int_rdvd_iff)
1.522 -  from lp'' lp a\<beta>[OF lp'' dl lp] have lq:"iszlfm ?q (real i#bs)" and uq: "d\<beta> ?q 1"
1.523 +  from lp'' lp a_\<beta>[OF lp'' dl lp] have lq:"iszlfm ?q (real i#bs)" and uq: "d_\<beta> ?q 1"
1.524      by (auto simp add: isint_def)
1.525 -  from \<delta>[OF lq] have dp:"?d >0" and dd: "d\<delta> ?q ?d" by blast+
1.526 +  from \<delta>[OF lq] have dp:"?d >0" and dd: "d_\<delta> ?q ?d" by blast+
1.527    let ?N = "\<lambda> t. Inum (real (i::int)#bs) t"
1.528    have "?N ` set ?B' = ((?N o simpnum) ` ?B)" by (simp add:image_compose)
1.529    also have "\<dots> = ?N ` ?B" using simpnum_ci[where bs="real i #bs"] by auto
1.530 @@ -5124,13 +5124,13 @@
1.531    {assume "\<not> (length ?B' \<le> length ?A')"
1.532      hence q:"q=mirror ?q" and "B = ?A'" and d:"d = ?d"
1.533        using qBd by (auto simp add: Let_def unit_def)
1.534 -    with AA' mirror\<alpha>\<beta>[OF lq] A_nb have b:"?N ` (set B) = ?N ` set (\<beta> q)"
1.535 +    with AA' mirror_\<alpha>_\<beta>[OF lq] A_nb have b:"?N ` (set B) = ?N ` set (\<beta> q)"
1.536        and bn: "\<forall>b\<in> set B. numbound0 b" by simp+
1.537      from mirror_ex[OF lq] pq_ex q
1.538      have pqm_eq:"(\<exists> (x::int). ?I x p) = (\<exists> (x::int). ?I x q)" by simp
1.539 -    from lq uq q mirror_d\<beta> [where p="?q" and bs="bs" and a="real i"]
1.540 -    have lq': "iszlfm q (real i#bs)" and uq: "d\<beta> q 1" by auto
1.541 -    from \<delta>[OF lq'] mirror_\<delta>[OF lq] q d have dq:"d\<delta> q d " by auto
1.542 +    from lq uq q mirror_d_\<beta> [where p="?q" and bs="bs" and a="real i"]
1.543 +    have lq': "iszlfm q (real i#bs)" and uq: "d_\<beta> q 1" by auto
1.544 +    from \<delta>[OF lq'] mirror_\<delta>[OF lq] q d have dq:"d_\<delta> q d " by auto
1.545      from pqm_eq b bn uq lq' dp dq q dp d have ?thes by simp
1.546    }
1.547    ultimately show ?thes by blast
1.548 @@ -5168,7 +5168,7 @@
1.549    have qbf:"unit p = (?q,?B,?d)" by simp
1.550    from unit[OF qf qbf] have pq_ex: "(\<exists>(x::int). ?I x p) = (\<exists> (x::int). ?I x ?q)" and
1.551      B:"?N ` set ?B = ?N ` set (\<beta> ?q)" and
1.552 -    uq:"d\<beta> ?q 1" and dd: "d\<delta> ?q ?d" and dp: "?d > 0" and
1.553 +    uq:"d_\<beta> ?q 1" and dd: "d_\<delta> ?q ?d" and dp: "?d > 0" and
1.554      lq: "iszlfm ?q (real i#bs)" and
1.555      Bn: "\<forall> b\<in> set ?B. numbound0 b" by auto
1.556    from zlin_qfree[OF lq] have qfq: "qfree ?q" .
1.557 @@ -5231,14 +5231,14 @@
1.558
1.559      (* Redy and Loveland *)
1.560
1.561 -lemma \<sigma>\<rho>_cong: assumes lp: "iszlfm p (a#bs)" and tt': "Inum (a#bs) t = Inum (a#bs) t'"
1.562 -  shows "Ifm (a#bs) (\<sigma>\<rho> p (t,c)) = Ifm (a#bs) (\<sigma>\<rho> p (t',c))"
1.563 +lemma \<sigma>_\<rho>_cong: assumes lp: "iszlfm p (a#bs)" and tt': "Inum (a#bs) t = Inum (a#bs) t'"
1.564 +  shows "Ifm (a#bs) (\<sigma>_\<rho> p (t,c)) = Ifm (a#bs) (\<sigma>_\<rho> p (t',c))"
1.565    using lp
1.566    by (induct p rule: iszlfm.induct, auto simp add: tt')
1.567
1.568  lemma \<sigma>_cong: assumes lp: "iszlfm p (a#bs)" and tt': "Inum (a#bs) t = Inum (a#bs) t'"
1.569    shows "Ifm (a#bs) (\<sigma> p c t) = Ifm (a#bs) (\<sigma> p c t')"
1.570 -  by (simp add: \<sigma>_def tt' \<sigma>\<rho>_cong[OF lp tt'])
1.571 +  by (simp add: \<sigma>_def tt' \<sigma>_\<rho>_cong[OF lp tt'])
1.572
1.573  lemma \<rho>_cong: assumes lp: "iszlfm p (a#bs)"
1.574    and RR: "(\<lambda>(b,k). (Inum (a#bs) b,k)) ` R =  (\<lambda>(b,k). (Inum (a#bs) b,k)) ` set (\<rho> p)"
1.575 @@ -5284,7 +5284,7 @@
1.576  definition chooset :: "fm \<Rightarrow> fm \<times> ((num\<times>int) list) \<times> int" where
1.577    "chooset p \<equiv> (let q = zlfm p ; d = \<delta> q;
1.578               B = remdups (map (\<lambda> (t,k). (simpnum t,k)) (\<rho> q)) ;
1.579 -             a = remdups (map (\<lambda> (t,k). (simpnum t,k)) (\<alpha>\<rho> q))
1.580 +             a = remdups (map (\<lambda> (t,k). (simpnum t,k)) (\<alpha>_\<rho> q))
1.581               in if length B \<le> length a then (q,B,d) else (mirror q, a,d))"
1.582
1.583  lemma chooset: assumes qf: "qfree p"
1.584 @@ -5299,8 +5299,8 @@
1.585    let ?B = "set (\<rho> ?q)"
1.586    let ?f = "\<lambda> (t,k). (simpnum t,k)"
1.587    let ?B'= "remdups (map ?f (\<rho> ?q))"
1.588 -  let ?A = "set (\<alpha>\<rho> ?q)"
1.589 -  let ?A'= "remdups (map ?f (\<alpha>\<rho> ?q))"
1.590 +  let ?A = "set (\<alpha>_\<rho> ?q)"
1.591 +  let ?A'= "remdups (map ?f (\<alpha>_\<rho> ?q))"
1.592    from conjunct1[OF zlfm_I[OF qf, where bs="bs"]]
1.593    have pp': "\<forall> i. ?I i ?q = ?I i p" by auto
1.594    hence pq_ex:"(\<exists> (x::int). ?I x p) = (\<exists> x. ?I x ?q)" by simp
1.595 @@ -5318,7 +5318,7 @@
1.596    finally have AA': "?N ` set ?A' = ?N ` ?A" .
1.597    from \<rho>_l[OF lq] have B_nb:"\<forall> (e,c)\<in> set ?B'. numbound0 e \<and> c > 0"
1.598      by (simp add: simpnum_numbound0 split_def)
1.599 -  from \<alpha>\<rho>_l[OF lq] have A_nb: "\<forall> (e,c)\<in> set ?A'. numbound0 e \<and> c > 0"
1.600 +  from \<alpha>_\<rho>_l[OF lq] have A_nb: "\<forall> (e,c)\<in> set ?A'. numbound0 e \<and> c > 0"
1.601      by (simp add: simpnum_numbound0 split_def)
1.602      {assume "length ?B' \<le> length ?A'"
1.603      hence q:"q=?q" and "B = ?B'" and d:"d = ?d"
1.604 @@ -5330,7 +5330,7 @@
1.605    {assume "\<not> (length ?B' \<le> length ?A')"
1.606      hence q:"q=mirror ?q" and "B = ?A'" and d:"d = ?d"
1.607        using qBd by (auto simp add: Let_def chooset_def)
1.608 -    with AA' mirror_\<alpha>\<rho>[OF lq] A_nb have b:"?N ` (set B) = ?N ` set (\<rho> q)"
1.609 +    with AA' mirror_\<alpha>_\<rho>[OF lq] A_nb have b:"?N ` (set B) = ?N ` set (\<rho> q)"
1.610        and bn: "\<forall>(e,c)\<in> set B. numbound0 e \<and> c > 0" by auto
1.611      from mirror_ex[OF lq] pq_ex q
1.612      have pqm_eq:"(\<exists> (x::int). ?I x p) = (\<exists> (x::int). ?I x q)" by simp
```