src/HOL/Decision_Procs/Cooper.thy
changeset 55981 66739f41d5b2
parent 55964 acdde1a5faa0
child 55999 6477fc70cfa0
     1.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Fri Mar 07 16:50:42 2014 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Fri Mar 07 17:07:30 2014 +0100
     1.3 @@ -62,25 +62,25 @@
     1.4  
     1.5  primrec Ifm :: "bool list \<Rightarrow> int list \<Rightarrow> fm \<Rightarrow> bool"  -- {* Semantics of formulae (fm) *}
     1.6  where
     1.7 -  "Ifm bbs bs T = True"
     1.8 -| "Ifm bbs bs F = False"
     1.9 -| "Ifm bbs bs (Lt a) = (Inum bs a < 0)"
    1.10 -| "Ifm bbs bs (Gt a) = (Inum bs a > 0)"
    1.11 -| "Ifm bbs bs (Le a) = (Inum bs a \<le> 0)"
    1.12 -| "Ifm bbs bs (Ge a) = (Inum bs a \<ge> 0)"
    1.13 -| "Ifm bbs bs (Eq a) = (Inum bs a = 0)"
    1.14 -| "Ifm bbs bs (NEq a) = (Inum bs a \<noteq> 0)"
    1.15 -| "Ifm bbs bs (Dvd i b) = (i dvd Inum bs b)"
    1.16 -| "Ifm bbs bs (NDvd i b) = (\<not>(i dvd Inum bs b))"
    1.17 -| "Ifm bbs bs (NOT p) = (\<not> (Ifm bbs bs p))"
    1.18 -| "Ifm bbs bs (And p q) = (Ifm bbs bs p \<and> Ifm bbs bs q)"
    1.19 -| "Ifm bbs bs (Or p q) = (Ifm bbs bs p \<or> Ifm bbs bs q)"
    1.20 -| "Ifm bbs bs (Imp p q) = ((Ifm bbs bs p) \<longrightarrow> (Ifm bbs bs q))"
    1.21 -| "Ifm bbs bs (Iff p q) = (Ifm bbs bs p = Ifm bbs bs q)"
    1.22 -| "Ifm bbs bs (E p) = (\<exists>x. Ifm bbs (x#bs) p)"
    1.23 -| "Ifm bbs bs (A p) = (\<forall>x. Ifm bbs (x#bs) p)"
    1.24 -| "Ifm bbs bs (Closed n) = bbs!n"
    1.25 -| "Ifm bbs bs (NClosed n) = (\<not> bbs!n)"
    1.26 +  "Ifm bbs bs T \<longleftrightarrow> True"
    1.27 +| "Ifm bbs bs F \<longleftrightarrow> False"
    1.28 +| "Ifm bbs bs (Lt a) \<longleftrightarrow> Inum bs a < 0"
    1.29 +| "Ifm bbs bs (Gt a) \<longleftrightarrow> Inum bs a > 0"
    1.30 +| "Ifm bbs bs (Le a) \<longleftrightarrow> Inum bs a \<le> 0"
    1.31 +| "Ifm bbs bs (Ge a) \<longleftrightarrow> Inum bs a \<ge> 0"
    1.32 +| "Ifm bbs bs (Eq a) \<longleftrightarrow> Inum bs a = 0"
    1.33 +| "Ifm bbs bs (NEq a) \<longleftrightarrow> Inum bs a \<noteq> 0"
    1.34 +| "Ifm bbs bs (Dvd i b) \<longleftrightarrow> i dvd Inum bs b"
    1.35 +| "Ifm bbs bs (NDvd i b) \<longleftrightarrow> \<not> i dvd Inum bs b"
    1.36 +| "Ifm bbs bs (NOT p) \<longleftrightarrow> \<not> Ifm bbs bs p"
    1.37 +| "Ifm bbs bs (And p q) \<longleftrightarrow> Ifm bbs bs p \<and> Ifm bbs bs q"
    1.38 +| "Ifm bbs bs (Or p q) \<longleftrightarrow> Ifm bbs bs p \<or> Ifm bbs bs q"
    1.39 +| "Ifm bbs bs (Imp p q) \<longleftrightarrow> (Ifm bbs bs p \<longrightarrow> Ifm bbs bs q)"
    1.40 +| "Ifm bbs bs (Iff p q) \<longleftrightarrow> Ifm bbs bs p = Ifm bbs bs q"
    1.41 +| "Ifm bbs bs (E p) \<longleftrightarrow> (\<exists>x. Ifm bbs (x # bs) p)"
    1.42 +| "Ifm bbs bs (A p) \<longleftrightarrow> (\<forall>x. Ifm bbs (x # bs) p)"
    1.43 +| "Ifm bbs bs (Closed n) \<longleftrightarrow> bbs!n"
    1.44 +| "Ifm bbs bs (NClosed n) \<longleftrightarrow> \<not> bbs!n"
    1.45  
    1.46  consts prep :: "fm \<Rightarrow> fm"
    1.47  recdef prep "measure fmsize"
    1.48 @@ -129,44 +129,44 @@
    1.49  
    1.50  primrec numbound0 :: "num \<Rightarrow> bool"  -- {* a num is INDEPENDENT of Bound 0 *}
    1.51  where
    1.52 -  "numbound0 (C c) = True"
    1.53 -| "numbound0 (Bound n) = (n>0)"
    1.54 -| "numbound0 (CN n i a) = (n >0 \<and> numbound0 a)"
    1.55 -| "numbound0 (Neg a) = numbound0 a"
    1.56 -| "numbound0 (Add a b) = (numbound0 a \<and> numbound0 b)"
    1.57 -| "numbound0 (Sub a b) = (numbound0 a \<and> numbound0 b)"
    1.58 -| "numbound0 (Mul i a) = numbound0 a"
    1.59 +  "numbound0 (C c) \<longleftrightarrow> True"
    1.60 +| "numbound0 (Bound n) \<longleftrightarrow> n > 0"
    1.61 +| "numbound0 (CN n i a) \<longleftrightarrow> n > 0 \<and> numbound0 a"
    1.62 +| "numbound0 (Neg a) \<longleftrightarrow> numbound0 a"
    1.63 +| "numbound0 (Add a b) \<longleftrightarrow> numbound0 a \<and> numbound0 b"
    1.64 +| "numbound0 (Sub a b) \<longleftrightarrow> numbound0 a \<and> numbound0 b"
    1.65 +| "numbound0 (Mul i a) \<longleftrightarrow> numbound0 a"
    1.66  
    1.67  lemma numbound0_I:
    1.68    assumes nb: "numbound0 a"
    1.69 -  shows "Inum (b#bs) a = Inum (b'#bs) a"
    1.70 +  shows "Inum (b # bs) a = Inum (b' # bs) a"
    1.71    using nb by (induct a rule: num.induct) (auto simp add: gr0_conv_Suc)
    1.72  
    1.73  primrec bound0 :: "fm \<Rightarrow> bool" -- {* A Formula is independent of Bound 0 *}
    1.74  where
    1.75 -  "bound0 T = True"
    1.76 -| "bound0 F = True"
    1.77 -| "bound0 (Lt a) = numbound0 a"
    1.78 -| "bound0 (Le a) = numbound0 a"
    1.79 -| "bound0 (Gt a) = numbound0 a"
    1.80 -| "bound0 (Ge a) = numbound0 a"
    1.81 -| "bound0 (Eq a) = numbound0 a"
    1.82 -| "bound0 (NEq a) = numbound0 a"
    1.83 -| "bound0 (Dvd i a) = numbound0 a"
    1.84 -| "bound0 (NDvd i a) = numbound0 a"
    1.85 -| "bound0 (NOT p) = bound0 p"
    1.86 -| "bound0 (And p q) = (bound0 p \<and> bound0 q)"
    1.87 -| "bound0 (Or p q) = (bound0 p \<and> bound0 q)"
    1.88 -| "bound0 (Imp p q) = ((bound0 p) \<and> (bound0 q))"
    1.89 -| "bound0 (Iff p q) = (bound0 p \<and> bound0 q)"
    1.90 -| "bound0 (E p) = False"
    1.91 -| "bound0 (A p) = False"
    1.92 -| "bound0 (Closed P) = True"
    1.93 -| "bound0 (NClosed P) = True"
    1.94 +  "bound0 T \<longleftrightarrow> True"
    1.95 +| "bound0 F \<longleftrightarrow> True"
    1.96 +| "bound0 (Lt a) \<longleftrightarrow> numbound0 a"
    1.97 +| "bound0 (Le a) \<longleftrightarrow> numbound0 a"
    1.98 +| "bound0 (Gt a) \<longleftrightarrow> numbound0 a"
    1.99 +| "bound0 (Ge a) \<longleftrightarrow> numbound0 a"
   1.100 +| "bound0 (Eq a) \<longleftrightarrow> numbound0 a"
   1.101 +| "bound0 (NEq a) \<longleftrightarrow> numbound0 a"
   1.102 +| "bound0 (Dvd i a) \<longleftrightarrow> numbound0 a"
   1.103 +| "bound0 (NDvd i a) \<longleftrightarrow> numbound0 a"
   1.104 +| "bound0 (NOT p) \<longleftrightarrow> bound0 p"
   1.105 +| "bound0 (And p q) \<longleftrightarrow> bound0 p \<and> bound0 q"
   1.106 +| "bound0 (Or p q) \<longleftrightarrow> bound0 p \<and> bound0 q"
   1.107 +| "bound0 (Imp p q) \<longleftrightarrow> bound0 p \<and> bound0 q"
   1.108 +| "bound0 (Iff p q) \<longleftrightarrow> bound0 p \<and> bound0 q"
   1.109 +| "bound0 (E p) \<longleftrightarrow> False"
   1.110 +| "bound0 (A p) \<longleftrightarrow> False"
   1.111 +| "bound0 (Closed P) \<longleftrightarrow> True"
   1.112 +| "bound0 (NClosed P) \<longleftrightarrow> True"
   1.113  
   1.114  lemma bound0_I:
   1.115    assumes bp: "bound0 p"
   1.116 -  shows "Ifm bbs (b#bs) p = Ifm bbs (b'#bs) p"
   1.117 +  shows "Ifm bbs (b # bs) p = Ifm bbs (b' # bs) p"
   1.118    using bp numbound0_I[where b="b" and bs="bs" and b'="b'"]
   1.119    by (induct p rule: fm.induct) (auto simp add: gr0_conv_Suc)
   1.120  
   1.121 @@ -256,19 +256,19 @@
   1.122  
   1.123  fun isatom :: "fm \<Rightarrow> bool"  -- {* test for atomicity *}
   1.124  where
   1.125 -  "isatom T = True"
   1.126 -| "isatom F = True"
   1.127 -| "isatom (Lt a) = True"
   1.128 -| "isatom (Le a) = True"
   1.129 -| "isatom (Gt a) = True"
   1.130 -| "isatom (Ge a) = True"
   1.131 -| "isatom (Eq a) = True"
   1.132 -| "isatom (NEq a) = True"
   1.133 -| "isatom (Dvd i b) = True"
   1.134 -| "isatom (NDvd i b) = True"
   1.135 -| "isatom (Closed P) = True"
   1.136 -| "isatom (NClosed P) = True"
   1.137 -| "isatom p = False"
   1.138 +  "isatom T \<longleftrightarrow> True"
   1.139 +| "isatom F \<longleftrightarrow> True"
   1.140 +| "isatom (Lt a) \<longleftrightarrow> True"
   1.141 +| "isatom (Le a) \<longleftrightarrow> True"
   1.142 +| "isatom (Gt a) \<longleftrightarrow> True"
   1.143 +| "isatom (Ge a) \<longleftrightarrow> True"
   1.144 +| "isatom (Eq a) \<longleftrightarrow> True"
   1.145 +| "isatom (NEq a) \<longleftrightarrow> True"
   1.146 +| "isatom (Dvd i b) \<longleftrightarrow> True"
   1.147 +| "isatom (NDvd i b) \<longleftrightarrow> True"
   1.148 +| "isatom (Closed P) \<longleftrightarrow> True"
   1.149 +| "isatom (NClosed P) \<longleftrightarrow> True"
   1.150 +| "isatom p \<longleftrightarrow> False"
   1.151  
   1.152  lemma numsubst0_numbound0:
   1.153    assumes "numbound0 t"
   1.154 @@ -423,10 +423,10 @@
   1.155  
   1.156  consts numadd:: "num \<times> num \<Rightarrow> num"
   1.157  recdef numadd "measure (\<lambda>(t, s). num_size t + num_size s)"
   1.158 -  "numadd (CN n1 c1 r1 ,CN n2 c2 r2) =
   1.159 +  "numadd (CN n1 c1 r1, CN n2 c2 r2) =
   1.160      (if n1 = n2 then
   1.161 -      (let c = c1 + c2
   1.162 -       in if c = 0 then numadd (r1, r2) else CN n1 c (numadd (r1, r2)))
   1.163 +       let c = c1 + c2
   1.164 +       in if c = 0 then numadd (r1, r2) else CN n1 c (numadd (r1, r2))
   1.165       else if n1 \<le> n2 then CN n1 c1 (numadd (r1, Add (Mul c2 (Bound n2)) r2))
   1.166       else CN n2 c2 (numadd (Add (Mul c1 (Bound n1)) r1, r2)))"
   1.167    "numadd (CN n1 c1 r1, t) = CN n1 c1 (numadd (r1, t))"
   1.168 @@ -1108,8 +1108,8 @@
   1.169  
   1.170  lemma zlfm_I:
   1.171    assumes qfp: "qfree p"
   1.172 -  shows "(Ifm bbs (i # bs) (zlfm p) = Ifm bbs (i # bs) p) \<and> iszlfm (zlfm p)"
   1.173 -  (is "(?I (?l p) = ?I p) \<and> ?L (?l p)")
   1.174 +  shows "Ifm bbs (i # bs) (zlfm p) = Ifm bbs (i # bs) p \<and> iszlfm (zlfm p)"
   1.175 +  (is "?I (?l p) = ?I p \<and> ?L (?l p)")
   1.176    using qfp
   1.177  proof (induct p rule: zlfm.induct)
   1.178    case (5 a)
   1.179 @@ -2204,20 +2204,20 @@
   1.180      \<Longrightarrow> (\<exists>(x::int). P x) = ((\<exists>(j::int) \<in> {1..D}. P1 j) \<or> (\<exists>(j::int) \<in> {1..D}. \<exists>(b::int) \<in> B. P (b + j)))"
   1.181    apply(rule iffI)
   1.182    prefer 2
   1.183 -  apply(drule minusinfinity)
   1.184 +  apply (drule minusinfinity)
   1.185    apply assumption+
   1.186 -  apply(fastforce)
   1.187 +  apply fastforce
   1.188    apply clarsimp
   1.189 -  apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x - k*D)")
   1.190 -  apply(frule_tac x = x and z=z in decr_lemma)
   1.191 -  apply(subgoal_tac "P1(x - (\<bar>x - z\<bar> + 1) * D)")
   1.192 +  apply (subgoal_tac "\<And>k. 0 \<le> k \<Longrightarrow> \<forall>x. P x \<longrightarrow> P (x - k * D)")
   1.193 +  apply (frule_tac x = x and z=z in decr_lemma)
   1.194 +  apply (subgoal_tac "P1 (x - (\<bar>x - z\<bar> + 1) * D)")
   1.195    prefer 2
   1.196 -  apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)")
   1.197 +  apply (subgoal_tac "0 \<le> \<bar>x - z\<bar> + 1")
   1.198    prefer 2 apply arith
   1.199     apply fastforce
   1.200 -  apply(drule (1)  periodic_finite_ex)
   1.201 +  apply (drule (1)  periodic_finite_ex)
   1.202    apply blast
   1.203 -  apply(blast dest:decr_mult_lemma)
   1.204 +  apply (blast dest: decr_mult_lemma)
   1.205    done
   1.206  
   1.207  theorem cp_thm:
   1.208 @@ -2297,7 +2297,7 @@
   1.209  proof -
   1.210    fix q B d
   1.211    assume qBd: "unit p = (q,B,d)"
   1.212 -  let ?thes = "((\<exists>x. Ifm bbs (x#bs) p) = (\<exists>x. Ifm bbs (x#bs) q)) \<and>
   1.213 +  let ?thes = "((\<exists>x. Ifm bbs (x#bs) p) \<longleftrightarrow> (\<exists>x. Ifm bbs (x#bs) q)) \<and>
   1.214      Inum (i#bs) ` set B = Inum (i#bs) ` set (\<beta> q) \<and>
   1.215      d_\<beta> q 1 \<and> d_\<delta> q d \<and> 0 < d \<and> iszlfm q \<and> (\<forall>b\<in> set B. numbound0 b)"
   1.216    let ?I = "\<lambda>x p. Ifm bbs (x#bs) p"
   1.217 @@ -2319,34 +2319,47 @@
   1.218    from lp' lp a_\<beta>[OF lp' dl lp] have lq:"iszlfm ?q" and uq: "d_\<beta> ?q 1"  by auto
   1.219    from \<delta>[OF lq] have dp:"?d >0" and dd: "d_\<delta> ?q ?d" by blast+
   1.220    let ?N = "\<lambda>t. Inum (i#bs) t"
   1.221 -  have "?N ` set ?B' = ((?N o simpnum) ` ?B)" by auto
   1.222 -  also have "\<dots> = ?N ` ?B" using simpnum_ci[where bs="i#bs"] by auto
   1.223 +  have "?N ` set ?B' = ((?N \<circ> simpnum) ` ?B)"
   1.224 +    by auto
   1.225 +  also have "\<dots> = ?N ` ?B"
   1.226 +    using simpnum_ci[where bs="i#bs"] by auto
   1.227    finally have BB': "?N ` set ?B' = ?N ` ?B" .
   1.228 -  have "?N ` set ?A' = ((?N o simpnum) ` ?A)" by auto
   1.229 -  also have "\<dots> = ?N ` ?A" using simpnum_ci[where bs="i#bs"] by auto
   1.230 +  have "?N ` set ?A' = ((?N \<circ> simpnum) ` ?A)"
   1.231 +    by auto
   1.232 +  also have "\<dots> = ?N ` ?A"
   1.233 +    using simpnum_ci[where bs="i#bs"] by auto
   1.234    finally have AA': "?N ` set ?A' = ?N ` ?A" .
   1.235    from \<beta>_numbound0[OF lq] have B_nb:"\<forall>b\<in> set ?B'. numbound0 b"
   1.236      by (simp add: simpnum_numbound0)
   1.237    from \<alpha>_l[OF lq] have A_nb: "\<forall>b\<in> set ?A'. numbound0 b"
   1.238      by (simp add: simpnum_numbound0)
   1.239 -    {assume "length ?B' \<le> length ?A'"
   1.240 -    then have q:"q=?q" and "B = ?B'" and d:"d = ?d"
   1.241 +  {
   1.242 +    assume "length ?B' \<le> length ?A'"
   1.243 +    then have q: "q = ?q" and "B = ?B'" and d: "d = ?d"
   1.244        using qBd by (auto simp add: Let_def unit_def)
   1.245 -    with BB' B_nb have b: "?N ` (set B) = ?N ` set (\<beta> q)"
   1.246 -      and bn: "\<forall>b\<in> set B. numbound0 b" by simp_all
   1.247 -  with pq_ex dp uq dd lq q d have ?thes by simp}
   1.248 +    with BB' B_nb
   1.249 +    have b: "?N ` (set B) = ?N ` set (\<beta> q)" and bn: "\<forall>b\<in> set B. numbound0 b"
   1.250 +      by simp_all
   1.251 +    with pq_ex dp uq dd lq q d have ?thes
   1.252 +      by simp
   1.253 +  }
   1.254    moreover
   1.255 -  {assume "\<not> (length ?B' \<le> length ?A')"
   1.256 +  {
   1.257 +    assume "\<not> (length ?B' \<le> length ?A')"
   1.258      then have q:"q=mirror ?q" and "B = ?A'" and d:"d = ?d"
   1.259        using qBd by (auto simp add: Let_def unit_def)
   1.260      with AA' mirror_\<alpha>_\<beta>[OF lq] A_nb have b:"?N ` (set B) = ?N ` set (\<beta> q)"
   1.261        and bn: "\<forall>b\<in> set B. numbound0 b" by simp_all
   1.262      from mirror_ex[OF lq] pq_ex q
   1.263 -    have pqm_eq:"(\<exists>(x::int). ?I x p) = (\<exists>(x::int). ?I x q)" by simp
   1.264 +    have pqm_eq:"(\<exists>(x::int). ?I x p) = (\<exists>(x::int). ?I x q)"
   1.265 +      by simp
   1.266      from lq uq q mirror_l[where p="?q"]
   1.267 -    have lq': "iszlfm q" and uq: "d_\<beta> q 1" by auto
   1.268 -    from \<delta>[OF lq'] mirror_\<delta>[OF lq] q d have dq:"d_\<delta> q d " by auto
   1.269 -    from pqm_eq b bn uq lq' dp dq q dp d have ?thes by simp
   1.270 +    have lq': "iszlfm q" and uq: "d_\<beta> q 1"
   1.271 +      by auto
   1.272 +    from \<delta>[OF lq'] mirror_\<delta>[OF lq] q d have dq: "d_\<delta> q d"
   1.273 +      by auto
   1.274 +    from pqm_eq b bn uq lq' dp dq q dp d have ?thes
   1.275 +      by simp
   1.276    }
   1.277    ultimately show ?thes by blast
   1.278  qed
   1.279 @@ -2354,7 +2367,8 @@
   1.280  
   1.281  text {* Cooper's Algorithm *}
   1.282  
   1.283 -definition cooper :: "fm \<Rightarrow> fm" where
   1.284 +definition cooper :: "fm \<Rightarrow> fm"
   1.285 +where
   1.286    "cooper p =
   1.287      (let
   1.288        (q, B, d) = unit p;
   1.289 @@ -2386,60 +2400,67 @@
   1.290    let ?Bjs = "[(b,j). b\<leftarrow>?B,j\<leftarrow>?js]"
   1.291    let ?qd = "evaldjf (\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)) ?Bjs"
   1.292    have qbf:"unit p = (?q,?B,?d)" by simp
   1.293 -  from unit[OF qf qbf] have pq_ex: "(\<exists>(x::int). ?I x p) = (\<exists>(x::int). ?I x ?q)" and
   1.294 -    B:"?N ` set ?B = ?N ` set (\<beta> ?q)" and
   1.295 -    uq:"d_\<beta> ?q 1" and dd: "d_\<delta> ?q ?d" and dp: "?d > 0" and
   1.296 -    lq: "iszlfm ?q" and
   1.297 -    Bn: "\<forall>b\<in> set ?B. numbound0 b" by auto
   1.298 +  from unit[OF qf qbf]
   1.299 +  have pq_ex: "(\<exists>(x::int). ?I x p) \<longleftrightarrow> (\<exists>(x::int). ?I x ?q)"
   1.300 +    and B: "?N ` set ?B = ?N ` set (\<beta> ?q)"
   1.301 +    and uq: "d_\<beta> ?q 1"
   1.302 +    and dd: "d_\<delta> ?q ?d"
   1.303 +    and dp: "?d > 0"
   1.304 +    and lq: "iszlfm ?q"
   1.305 +    and Bn: "\<forall>b\<in> set ?B. numbound0 b"
   1.306 +    by auto
   1.307    from zlin_qfree[OF lq] have qfq: "qfree ?q" .
   1.308    from simpfm_qf[OF minusinf_qfree[OF qfq]] have qfmq: "qfree ?smq" .
   1.309 -  have jsnb: "\<forall>j \<in> set ?js. numbound0 (C j)" by simp
   1.310 +  have jsnb: "\<forall>j \<in> set ?js. numbound0 (C j)"
   1.311 +    by simp
   1.312    then have "\<forall>j\<in> set ?js. bound0 (subst0 (C j) ?smq)"
   1.313      by (auto simp only: subst0_bound0[OF qfmq])
   1.314    then have th: "\<forall>j\<in> set ?js. bound0 (simpfm (subst0 (C j) ?smq))"
   1.315      by (auto simp add: simpfm_bound0)
   1.316 -  from evaldjf_bound0[OF th] have mdb: "bound0 ?md" by simp
   1.317 +  from evaldjf_bound0[OF th] have mdb: "bound0 ?md"
   1.318 +    by simp
   1.319    from Bn jsnb have "\<forall>(b,j) \<in> set ?Bjs. numbound0 (Add b (C j))"
   1.320      by simp
   1.321    then have "\<forall>(b,j) \<in> set ?Bjs. bound0 (subst0 (Add b (C j)) ?q)"
   1.322      using subst0_bound0[OF qfq] by blast
   1.323    then have "\<forall>(b,j) \<in> set ?Bjs. bound0 (simpfm (subst0 (Add b (C j)) ?q))"
   1.324 -    using simpfm_bound0  by blast
   1.325 +    using simpfm_bound0 by blast
   1.326    then have th': "\<forall>x \<in> set ?Bjs. bound0 ((\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)) x)"
   1.327      by auto
   1.328 -  from evaldjf_bound0 [OF th'] have qdb: "bound0 ?qd" by simp
   1.329 -  from mdb qdb
   1.330 -  have mdqdb: "bound0 (disj ?md ?qd)"
   1.331 -    unfolding disj_def by (cases "?md=T \<or> ?qd=T") simp_all
   1.332 +  from evaldjf_bound0 [OF th'] have qdb: "bound0 ?qd"
   1.333 +    by simp
   1.334 +  from mdb qdb have mdqdb: "bound0 (disj ?md ?qd)"
   1.335 +    unfolding disj_def by (cases "?md = T \<or> ?qd = T") simp_all
   1.336    from trans [OF pq_ex cp_thm'[OF lq uq dd dp,where i="i"]] B
   1.337 -  have "?lhs = (\<exists>j\<in> {1.. ?d}. ?I j ?mq \<or> (\<exists>b\<in> ?N ` set ?B. Ifm bbs ((b+ j)#bs) ?q))"
   1.338 +  have "?lhs \<longleftrightarrow> (\<exists>j \<in> {1.. ?d}. ?I j ?mq \<or> (\<exists>b \<in> ?N ` set ?B. Ifm bbs ((b + j) # bs) ?q))"
   1.339      by auto
   1.340 -  also have "\<dots> = (\<exists>j\<in> {1.. ?d}. ?I j ?mq \<or> (\<exists>b\<in> set ?B. Ifm bbs ((?N b+ j)#bs) ?q))"
   1.341 +  also have "\<dots> \<longleftrightarrow> (\<exists>j \<in> {1.. ?d}. ?I j ?mq \<or> (\<exists>b \<in> set ?B. Ifm bbs ((?N b + j) # bs) ?q))"
   1.342      by simp
   1.343 -  also have "\<dots> = ((\<exists>j\<in> {1.. ?d}. ?I j ?mq ) \<or>
   1.344 -      (\<exists>j\<in> {1.. ?d}. \<exists>b\<in> set ?B. Ifm bbs ((?N (Add b (C j)))#bs) ?q))"
   1.345 +  also have "\<dots> \<longleftrightarrow> (\<exists>j \<in> {1.. ?d}. ?I j ?mq ) \<or>
   1.346 +      (\<exists>j\<in> {1.. ?d}. \<exists>b \<in> set ?B. Ifm bbs ((?N (Add b (C j))) # bs) ?q)"
   1.347      by (simp only: Inum.simps) blast
   1.348 -  also have "\<dots> = ((\<exists>j\<in> {1.. ?d}. ?I j ?smq ) \<or>
   1.349 -      (\<exists>j\<in> {1.. ?d}. \<exists>b\<in> set ?B. Ifm bbs ((?N (Add b (C j)))#bs) ?q))"
   1.350 +  also have "\<dots> \<longleftrightarrow> (\<exists>j \<in> {1.. ?d}. ?I j ?smq) \<or>
   1.351 +      (\<exists>j \<in> {1.. ?d}. \<exists>b \<in> set ?B. Ifm bbs ((?N (Add b (C j))) # bs) ?q)"
   1.352      by (simp add: simpfm)
   1.353 -  also have "\<dots> = ((\<exists>j\<in> set ?js. (\<lambda>j. ?I i (simpfm (subst0 (C j) ?smq))) j) \<or>
   1.354 -      (\<exists>j\<in> set ?js. \<exists>b\<in> set ?B. Ifm bbs ((?N (Add b (C j)))#bs) ?q))"
   1.355 +  also have "\<dots> \<longleftrightarrow> (\<exists>j\<in> set ?js. (\<lambda>j. ?I i (simpfm (subst0 (C j) ?smq))) j) \<or>
   1.356 +      (\<exists>j\<in> set ?js. \<exists>b\<in> set ?B. Ifm bbs ((?N (Add b (C j)))#bs) ?q)"
   1.357      by (simp only: simpfm subst0_I[OF qfmq] set_upto) auto
   1.358 -  also have "\<dots> = (?I i (evaldjf (\<lambda>j. simpfm (subst0 (C j) ?smq)) ?js) \<or>
   1.359 -      (\<exists>j\<in> set ?js. \<exists>b\<in> set ?B. ?I i (subst0 (Add b (C j)) ?q)))"
   1.360 +  also have "\<dots> \<longleftrightarrow> ?I i (evaldjf (\<lambda>j. simpfm (subst0 (C j) ?smq)) ?js) \<or>
   1.361 +      (\<exists>j\<in> set ?js. \<exists>b\<in> set ?B. ?I i (subst0 (Add b (C j)) ?q))"
   1.362      by (simp only: evaldjf_ex subst0_I[OF qfq])
   1.363 -  also have "\<dots>= (?I i ?md \<or> (\<exists>(b,j) \<in> set ?Bjs. (\<lambda>(b,j). ?I i (simpfm (subst0 (Add b (C j)) ?q))) (b,j)))"
   1.364 +  also have "\<dots> \<longleftrightarrow> ?I i ?md \<or>
   1.365 +      (\<exists>(b,j) \<in> set ?Bjs. (\<lambda>(b,j). ?I i (simpfm (subst0 (Add b (C j)) ?q))) (b,j))"
   1.366      by (simp only: simpfm set_concat set_map concat_map_singleton UN_simps) blast
   1.367 -  also have "\<dots> = (?I i ?md \<or> (?I i (evaldjf (\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)) ?Bjs)))"
   1.368 +  also have "\<dots> \<longleftrightarrow> ?I i ?md \<or> ?I i (evaldjf (\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)) ?Bjs)"
   1.369      by (simp only: evaldjf_ex[where bs="i#bs" and f="\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)" and ps="?Bjs"])
   1.370        (auto simp add: split_def)
   1.371 -  finally have mdqd: "?lhs = (?I i ?md \<or> ?I i ?qd)"
   1.372 +  finally have mdqd: "?lhs \<longleftrightarrow> ?I i ?md \<or> ?I i ?qd"
   1.373      by simp
   1.374 -  also have "\<dots> = (?I i (disj ?md ?qd))"
   1.375 +  also have "\<dots> \<longleftrightarrow> ?I i (disj ?md ?qd)"
   1.376      by (simp add: disj)
   1.377 -  also have "\<dots> = (Ifm bbs bs (decr (disj ?md ?qd)))"
   1.378 +  also have "\<dots> \<longleftrightarrow> Ifm bbs bs (decr (disj ?md ?qd))"
   1.379      by (simp only: decr [OF mdqdb])
   1.380 -  finally have mdqd2: "?lhs = (Ifm bbs bs (decr (disj ?md ?qd)))" .
   1.381 +  finally have mdqd2: "?lhs \<longleftrightarrow> Ifm bbs bs (decr (disj ?md ?qd))" .
   1.382    {
   1.383      assume mdT: "?md = T"
   1.384      then have cT: "cooper p = T"
   1.385 @@ -2448,7 +2469,8 @@
   1.386        using mdqd by simp
   1.387      from mdT have "?rhs"
   1.388        by (simp add: cooper_def unit_def split_def)
   1.389 -    with lhs cT have ?thesis by simp
   1.390 +    with lhs cT have ?thesis
   1.391 +      by simp
   1.392    }
   1.393    moreover
   1.394    {