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" .