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.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 @@ -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.448        by (simp add: \<sigma>_def)
   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