src/HOL/Decision_Procs/Cooper.thy
changeset 50313 5b49cfd43a37
parent 50252 4aa34bd43228
child 51143 0a2371e7ced3
     1.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Sun Dec 02 14:56:49 2012 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Sun Dec 02 17:22:19 2012 +0100
     1.3 @@ -12,11 +12,11 @@
     1.4    (****                            SHADOW SYNTAX AND SEMANTICS                  ****)
     1.5    (*********************************************************************************)
     1.6  
     1.7 -datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num 
     1.8 +datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num
     1.9    | Mul int num
    1.10  
    1.11 -  (* A size for num to make inductive proofs simpler*)
    1.12 -primrec num_size :: "num \<Rightarrow> nat" where
    1.13 +primrec num_size :: "num \<Rightarrow> nat" -- {* A size for num to make inductive proofs simpler *}
    1.14 +where
    1.15    "num_size (C c) = 1"
    1.16  | "num_size (Bound n) = 1"
    1.17  | "num_size (Neg a) = 1 + num_size a"
    1.18 @@ -34,14 +34,14 @@
    1.19  | "Inum bs (Sub a b) = Inum bs a - Inum bs b"
    1.20  | "Inum bs (Mul c a) = c* Inum bs a"
    1.21  
    1.22 -datatype fm  = 
    1.23 +datatype fm  =
    1.24    T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| Dvd int num| NDvd int num|
    1.25 -  NOT fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm 
    1.26 +  NOT fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
    1.27    | Closed nat | NClosed nat
    1.28  
    1.29  
    1.30 -  (* A size for fm *)
    1.31 -fun fmsize :: "fm \<Rightarrow> nat" where
    1.32 +fun fmsize :: "fm \<Rightarrow> nat"  -- {* A size for fm *}
    1.33 +where
    1.34    "fmsize (NOT p) = 1 + fmsize p"
    1.35  | "fmsize (And p q) = 1 + fmsize p + fmsize q"
    1.36  | "fmsize (Or p q) = 1 + fmsize p + fmsize q"
    1.37 @@ -52,12 +52,12 @@
    1.38  | "fmsize (Dvd i t) = 2"
    1.39  | "fmsize (NDvd i t) = 2"
    1.40  | "fmsize p = 1"
    1.41 -  (* several lemmas about fmsize *)
    1.42 +
    1.43  lemma fmsize_pos: "fmsize p > 0"
    1.44    by (induct p rule: fmsize.induct) simp_all
    1.45  
    1.46 -  (* Semantics of formulae (fm) *)
    1.47 -primrec Ifm ::"bool list \<Rightarrow> int list \<Rightarrow> fm \<Rightarrow> bool" where
    1.48 +primrec Ifm :: "bool list \<Rightarrow> int list \<Rightarrow> fm \<Rightarrow> bool"  -- {* Semantics of formulae (fm) *}
    1.49 +where
    1.50    "Ifm bbs bs T = True"
    1.51  | "Ifm bbs bs F = False"
    1.52  | "Ifm bbs bs (Lt a) = (Inum bs a < 0)"
    1.53 @@ -73,8 +73,8 @@
    1.54  | "Ifm bbs bs (Or p q) = (Ifm bbs bs p \<or> Ifm bbs bs q)"
    1.55  | "Ifm bbs bs (Imp p q) = ((Ifm bbs bs p) \<longrightarrow> (Ifm bbs bs q))"
    1.56  | "Ifm bbs bs (Iff p q) = (Ifm bbs bs p = Ifm bbs bs q)"
    1.57 -| "Ifm bbs bs (E p) = (\<exists> x. Ifm bbs (x#bs) p)"
    1.58 -| "Ifm bbs bs (A p) = (\<forall> x. Ifm bbs (x#bs) p)"
    1.59 +| "Ifm bbs bs (E p) = (\<exists>x. Ifm bbs (x#bs) p)"
    1.60 +| "Ifm bbs bs (A p) = (\<forall>x. Ifm bbs (x#bs) p)"
    1.61  | "Ifm bbs bs (Closed n) = bbs!n"
    1.62  | "Ifm bbs bs (NClosed n) = (\<not> bbs!n)"
    1.63  
    1.64 @@ -84,7 +84,7 @@
    1.65    "prep (E F) = F"
    1.66    "prep (E (Or p q)) = Or (prep (E p)) (prep (E q))"
    1.67    "prep (E (Imp p q)) = Or (prep (E (NOT p))) (prep (E q))"
    1.68 -  "prep (E (Iff p q)) = Or (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))" 
    1.69 +  "prep (E (Iff p q)) = Or (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))"
    1.70    "prep (E (NOT (And p q))) = Or (prep (E (NOT p))) (prep (E(NOT q)))"
    1.71    "prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))"
    1.72    "prep (E (NOT (Iff p q))) = Or (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))"
    1.73 @@ -103,40 +103,43 @@
    1.74    "prep (Imp p q) = prep (Or (NOT p) q)"
    1.75    "prep (Iff p q) = Or (prep (And p q)) (prep (And (NOT p) (NOT q)))"
    1.76    "prep p = p"
    1.77 -(hints simp add: fmsize_pos)
    1.78 +  (hints simp add: fmsize_pos)
    1.79 +
    1.80  lemma prep: "Ifm bbs bs (prep p) = Ifm bbs bs p"
    1.81 -by (induct p arbitrary: bs rule: prep.induct, auto)
    1.82 +  by (induct p arbitrary: bs rule: prep.induct) auto
    1.83  
    1.84  
    1.85 -  (* Quantifier freeness *)
    1.86 -fun qfree:: "fm \<Rightarrow> bool" where
    1.87 +fun qfree :: "fm \<Rightarrow> bool"  -- {* Quantifier freeness *}
    1.88 +where
    1.89    "qfree (E p) = False"
    1.90  | "qfree (A p) = False"
    1.91 -| "qfree (NOT p) = qfree p" 
    1.92 -| "qfree (And p q) = (qfree p \<and> qfree q)" 
    1.93 -| "qfree (Or  p q) = (qfree p \<and> qfree q)" 
    1.94 -| "qfree (Imp p q) = (qfree p \<and> qfree q)" 
    1.95 +| "qfree (NOT p) = qfree p"
    1.96 +| "qfree (And p q) = (qfree p \<and> qfree q)"
    1.97 +| "qfree (Or  p q) = (qfree p \<and> qfree q)"
    1.98 +| "qfree (Imp p q) = (qfree p \<and> qfree q)"
    1.99  | "qfree (Iff p q) = (qfree p \<and> qfree q)"
   1.100  | "qfree p = True"
   1.101  
   1.102 -  (* Boundedness and substitution *)
   1.103 -    
   1.104 -primrec numbound0:: "num \<Rightarrow> bool" (* a num is INDEPENDENT of Bound 0 *) where
   1.105 +
   1.106 +text {* Boundedness and substitution *}
   1.107 +
   1.108 +primrec numbound0 :: "num \<Rightarrow> bool"  -- {* a num is INDEPENDENT of Bound 0 *}
   1.109 +where
   1.110    "numbound0 (C c) = True"
   1.111  | "numbound0 (Bound n) = (n>0)"
   1.112  | "numbound0 (CN n i a) = (n >0 \<and> numbound0 a)"
   1.113  | "numbound0 (Neg a) = numbound0 a"
   1.114  | "numbound0 (Add a b) = (numbound0 a \<and> numbound0 b)"
   1.115 -| "numbound0 (Sub a b) = (numbound0 a \<and> numbound0 b)" 
   1.116 +| "numbound0 (Sub a b) = (numbound0 a \<and> numbound0 b)"
   1.117  | "numbound0 (Mul i a) = numbound0 a"
   1.118  
   1.119  lemma numbound0_I:
   1.120    assumes nb: "numbound0 a"
   1.121    shows "Inum (b#bs) a = Inum (b'#bs) a"
   1.122 -using nb
   1.123 -by (induct a rule: num.induct) (auto simp add: gr0_conv_Suc)
   1.124 +  using nb by (induct a rule: num.induct) (auto simp add: gr0_conv_Suc)
   1.125  
   1.126 -primrec bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *) where
   1.127 +primrec bound0 :: "fm \<Rightarrow> bool" -- {* A Formula is independent of Bound 0 *}
   1.128 +where
   1.129    "bound0 T = True"
   1.130  | "bound0 F = True"
   1.131  | "bound0 (Lt a) = numbound0 a"
   1.132 @@ -156,31 +159,33 @@
   1.133  | "bound0 (A p) = False"
   1.134  | "bound0 (Closed P) = True"
   1.135  | "bound0 (NClosed P) = True"
   1.136 +
   1.137  lemma bound0_I:
   1.138    assumes bp: "bound0 p"
   1.139    shows "Ifm bbs (b#bs) p = Ifm bbs (b'#bs) p"
   1.140 -using bp numbound0_I[where b="b" and bs="bs" and b'="b'"]
   1.141 -by (induct p rule: fm.induct) (auto simp add: gr0_conv_Suc)
   1.142 +  using bp numbound0_I[where b="b" and bs="bs" and b'="b'"]
   1.143 +  by (induct p rule: fm.induct) (auto simp add: gr0_conv_Suc)
   1.144  
   1.145 -fun numsubst0:: "num \<Rightarrow> num \<Rightarrow> num" where
   1.146 +fun numsubst0 :: "num \<Rightarrow> num \<Rightarrow> num"
   1.147 +where
   1.148    "numsubst0 t (C c) = (C c)"
   1.149  | "numsubst0 t (Bound n) = (if n=0 then t else Bound n)"
   1.150  | "numsubst0 t (CN 0 i a) = Add (Mul i t) (numsubst0 t a)"
   1.151  | "numsubst0 t (CN n i a) = CN n i (numsubst0 t a)"
   1.152  | "numsubst0 t (Neg a) = Neg (numsubst0 t a)"
   1.153  | "numsubst0 t (Add a b) = Add (numsubst0 t a) (numsubst0 t b)"
   1.154 -| "numsubst0 t (Sub a b) = Sub (numsubst0 t a) (numsubst0 t b)" 
   1.155 +| "numsubst0 t (Sub a b) = Sub (numsubst0 t a) (numsubst0 t b)"
   1.156  | "numsubst0 t (Mul i a) = Mul i (numsubst0 t a)"
   1.157  
   1.158 -lemma numsubst0_I:
   1.159 -  "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b#bs) a)#bs) t"
   1.160 -by (induct t rule: numsubst0.induct,auto simp:nth_Cons')
   1.161 +lemma numsubst0_I: "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b#bs) a)#bs) t"
   1.162 +  by (induct t rule: numsubst0.induct) (auto simp: nth_Cons')
   1.163  
   1.164  lemma numsubst0_I':
   1.165    "numbound0 a \<Longrightarrow> Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b'#bs) a)#bs) t"
   1.166 -by (induct t rule: numsubst0.induct, auto simp: nth_Cons' numbound0_I[where b="b" and b'="b'"])
   1.167 +  by (induct t rule: numsubst0.induct) (auto simp: nth_Cons' numbound0_I[where b="b" and b'="b'"])
   1.168  
   1.169 -primrec subst0:: "num \<Rightarrow> fm \<Rightarrow> fm" (* substitue a num into a formula for Bound 0 *) where
   1.170 +primrec subst0:: "num \<Rightarrow> fm \<Rightarrow> fm"  -- {* substitue a num into a formula for Bound 0 *}
   1.171 +where
   1.172    "subst0 t T = T"
   1.173  | "subst0 t F = F"
   1.174  | "subst0 t (Lt a) = Lt (numsubst0 t a)"
   1.175 @@ -199,12 +204,14 @@
   1.176  | "subst0 t (Closed P) = (Closed P)"
   1.177  | "subst0 t (NClosed P) = (NClosed P)"
   1.178  
   1.179 -lemma subst0_I: assumes qfp: "qfree p"
   1.180 +lemma subst0_I:
   1.181 +  assumes qfp: "qfree p"
   1.182    shows "Ifm bbs (b#bs) (subst0 a p) = Ifm bbs ((Inum (b#bs) a)#bs) p"
   1.183    using qfp numsubst0_I[where b="b" and bs="bs" and a="a"]
   1.184    by (induct p) (simp_all add: gr0_conv_Suc)
   1.185  
   1.186 -fun decrnum:: "num \<Rightarrow> num" where
   1.187 +fun decrnum:: "num \<Rightarrow> num"
   1.188 +where
   1.189    "decrnum (Bound n) = Bound (n - 1)"
   1.190  | "decrnum (Neg a) = Neg (decrnum a)"
   1.191  | "decrnum (Add a b) = Add (decrnum a) (decrnum b)"
   1.192 @@ -213,7 +220,8 @@
   1.193  | "decrnum (CN n i a) = (CN (n - 1) i (decrnum a))"
   1.194  | "decrnum a = a"
   1.195  
   1.196 -fun decr :: "fm \<Rightarrow> fm" where
   1.197 +fun decr :: "fm \<Rightarrow> fm"
   1.198 +where
   1.199    "decr (Lt a) = Lt (decrnum a)"
   1.200  | "decr (Le a) = Le (decrnum a)"
   1.201  | "decr (Gt a) = Gt (decrnum a)"
   1.202 @@ -222,26 +230,28 @@
   1.203  | "decr (NEq a) = NEq (decrnum a)"
   1.204  | "decr (Dvd i a) = Dvd i (decrnum a)"
   1.205  | "decr (NDvd i a) = NDvd i (decrnum a)"
   1.206 -| "decr (NOT p) = NOT (decr p)" 
   1.207 +| "decr (NOT p) = NOT (decr p)"
   1.208  | "decr (And p q) = And (decr p) (decr q)"
   1.209  | "decr (Or p q) = Or (decr p) (decr q)"
   1.210  | "decr (Imp p q) = Imp (decr p) (decr q)"
   1.211  | "decr (Iff p q) = Iff (decr p) (decr q)"
   1.212  | "decr p = p"
   1.213  
   1.214 -lemma decrnum: assumes nb: "numbound0 t"
   1.215 +lemma decrnum:
   1.216 +  assumes nb: "numbound0 t"
   1.217    shows "Inum (x#bs) t = Inum bs (decrnum t)"
   1.218 -  using nb by (induct t rule: decrnum.induct, auto simp add: gr0_conv_Suc)
   1.219 +  using nb by (induct t rule: decrnum.induct) (auto simp add: gr0_conv_Suc)
   1.220  
   1.221 -lemma decr: assumes nb: "bound0 p"
   1.222 +lemma decr:
   1.223 +  assumes nb: "bound0 p"
   1.224    shows "Ifm bbs (x#bs) p = Ifm bbs bs (decr p)"
   1.225 -  using nb 
   1.226 -  by (induct p rule: decr.induct, simp_all add: gr0_conv_Suc decrnum)
   1.227 +  using nb by (induct p rule: decr.induct) (simp_all add: gr0_conv_Suc decrnum)
   1.228  
   1.229  lemma decr_qf: "bound0 p \<Longrightarrow> qfree (decr p)"
   1.230 -by (induct p, simp_all)
   1.231 +  by (induct p) simp_all
   1.232  
   1.233 -fun isatom :: "fm \<Rightarrow> bool" (* test for atomicity *) where
   1.234 +fun isatom :: "fm \<Rightarrow> bool"  -- {* test for atomicity *}
   1.235 +where
   1.236    "isatom T = True"
   1.237  | "isatom F = True"
   1.238  | "isatom (Lt a) = True"
   1.239 @@ -256,110 +266,129 @@
   1.240  | "isatom (NClosed P) = True"
   1.241  | "isatom p = False"
   1.242  
   1.243 -lemma numsubst0_numbound0: assumes nb: "numbound0 t"
   1.244 +lemma numsubst0_numbound0:
   1.245 +  assumes nb: "numbound0 t"
   1.246    shows "numbound0 (numsubst0 t a)"
   1.247 -using nb apply (induct a)
   1.248 -apply simp_all
   1.249 -apply (case_tac nat, simp_all)
   1.250 -done
   1.251 +  using nb apply (induct a) 
   1.252 +  apply simp_all
   1.253 +  apply (case_tac nat, simp_all)
   1.254 +  done
   1.255  
   1.256 -lemma subst0_bound0: assumes qf: "qfree p" and nb: "numbound0 t"
   1.257 +lemma subst0_bound0:
   1.258 +  assumes qf: "qfree p" and nb: "numbound0 t"
   1.259    shows "bound0 (subst0 t p)"
   1.260 -using qf numsubst0_numbound0[OF nb] by (induct p) auto
   1.261 +  using qf numsubst0_numbound0[OF nb] by (induct p) auto
   1.262  
   1.263  lemma bound0_qf: "bound0 p \<Longrightarrow> qfree p"
   1.264 -by (induct p, simp_all)
   1.265 +  by (induct p) simp_all
   1.266  
   1.267  
   1.268 -definition djf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a \<Rightarrow> fm \<Rightarrow> fm" where
   1.269 -  "djf f p q \<equiv> (if q=T then T else if q=F then f p else 
   1.270 -  (let fp = f p in case fp of T \<Rightarrow> T | F \<Rightarrow> q | _ \<Rightarrow> Or (f p) q))"
   1.271 -definition evaldjf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a list \<Rightarrow> fm" where
   1.272 -  "evaldjf f ps \<equiv> foldr (djf f) ps F"
   1.273 +definition djf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a \<Rightarrow> fm \<Rightarrow> fm"
   1.274 +where
   1.275 +  "djf f p q =
   1.276 +    (if q = T then T
   1.277 +     else if q = F then f p
   1.278 +     else (let fp = f p in case fp of T \<Rightarrow> T | F \<Rightarrow> q | _ \<Rightarrow> Or (f p) q))"
   1.279 +
   1.280 +definition evaldjf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a list \<Rightarrow> fm"
   1.281 +  where "evaldjf f ps = foldr (djf f) ps F"
   1.282  
   1.283  lemma djf_Or: "Ifm bbs bs (djf f p q) = Ifm bbs bs (Or (f p) q)"
   1.284 -by (cases "q=T", simp add: djf_def,cases "q=F",simp add: djf_def) 
   1.285 -(cases "f p", simp_all add: Let_def djf_def) 
   1.286 +  by (cases "q=T", simp add: djf_def,cases "q=F",simp add: djf_def)
   1.287 +    (cases "f p", simp_all add: Let_def djf_def)
   1.288  
   1.289 -lemma evaldjf_ex: "Ifm bbs bs (evaldjf f ps) = (\<exists> p \<in> set ps. Ifm bbs bs (f p))"
   1.290 -  by(induct ps, simp_all add: evaldjf_def djf_Or)
   1.291 +lemma evaldjf_ex: "Ifm bbs bs (evaldjf f ps) = (\<exists>p \<in> set ps. Ifm bbs bs (f p))"
   1.292 +  by (induct ps) (simp_all add: evaldjf_def djf_Or)
   1.293  
   1.294 -lemma evaldjf_bound0: 
   1.295 -  assumes nb: "\<forall> x\<in> set xs. bound0 (f x)"
   1.296 +lemma evaldjf_bound0:
   1.297 +  assumes nb: "\<forall>x\<in> set xs. bound0 (f x)"
   1.298    shows "bound0 (evaldjf f xs)"
   1.299 -  using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto) 
   1.300 +  using nb by (induct xs) (auto simp add: evaldjf_def djf_def Let_def, case_tac "f a", auto)
   1.301  
   1.302 -lemma evaldjf_qf: 
   1.303 -  assumes nb: "\<forall> x\<in> set xs. qfree (f x)"
   1.304 +lemma evaldjf_qf:
   1.305 +  assumes nb: "\<forall>x\<in> set xs. qfree (f x)"
   1.306    shows "qfree (evaldjf f xs)"
   1.307 -  using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto) 
   1.308 +  using nb by (induct xs) (auto simp add: evaldjf_def djf_def Let_def, case_tac "f a", auto)
   1.309  
   1.310 -fun disjuncts :: "fm \<Rightarrow> fm list" where
   1.311 -  "disjuncts (Or p q) = (disjuncts p) @ (disjuncts q)"
   1.312 +fun disjuncts :: "fm \<Rightarrow> fm list"
   1.313 +where
   1.314 +  "disjuncts (Or p q) = disjuncts p @ disjuncts q"
   1.315  | "disjuncts F = []"
   1.316  | "disjuncts p = [p]"
   1.317  
   1.318 -lemma disjuncts: "(\<exists> q\<in> set (disjuncts p). Ifm bbs bs q) = Ifm bbs bs p"
   1.319 -by(induct p rule: disjuncts.induct, auto)
   1.320 +lemma disjuncts: "(\<exists>q \<in> set (disjuncts p). Ifm bbs bs q) = Ifm bbs bs p"
   1.321 + by (induct p rule: disjuncts.induct) auto
   1.322  
   1.323 -lemma disjuncts_nb: "bound0 p \<Longrightarrow> \<forall> q\<in> set (disjuncts p). bound0 q"
   1.324 -proof-
   1.325 -  assume nb: "bound0 p"
   1.326 -  hence "list_all bound0 (disjuncts p)" by (induct p rule:disjuncts.induct,auto)
   1.327 +lemma disjuncts_nb:
   1.328 +  assumes nb: "bound0 p"
   1.329 +  shows "\<forall>q \<in> set (disjuncts p). bound0 q"
   1.330 +proof -
   1.331 +  from nb have "list_all bound0 (disjuncts p)"
   1.332 +    by (induct p rule: disjuncts.induct) auto
   1.333    thus ?thesis by (simp only: list_all_iff)
   1.334  qed
   1.335  
   1.336 -lemma disjuncts_qf: "qfree p \<Longrightarrow> \<forall> q\<in> set (disjuncts p). qfree q"
   1.337 -proof-
   1.338 -  assume qf: "qfree p"
   1.339 -  hence "list_all qfree (disjuncts p)"
   1.340 -    by (induct p rule: disjuncts.induct, auto)
   1.341 +lemma disjuncts_qf:
   1.342 +  assumes qf: "qfree p"
   1.343 +  shows "\<forall>q \<in> set (disjuncts p). qfree q"
   1.344 +proof -
   1.345 +  from qf have "list_all qfree (disjuncts p)"
   1.346 +    by (induct p rule: disjuncts.induct) auto
   1.347    thus ?thesis by (simp only: list_all_iff)
   1.348  qed
   1.349  
   1.350 -definition DJ :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm" where
   1.351 -  "DJ f p \<equiv> evaldjf f (disjuncts p)"
   1.352 +definition DJ :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm"
   1.353 +  where "DJ f p = evaldjf f (disjuncts p)"
   1.354  
   1.355 -lemma DJ: assumes fdj: "\<forall> p q. f (Or p q) = Or (f p) (f q)"
   1.356 -  and fF: "f F = F"
   1.357 +lemma DJ:
   1.358 +  assumes fdj: "\<forall>p q. f (Or p q) = Or (f p) (f q)"
   1.359 +    and fF: "f F = F"
   1.360    shows "Ifm bbs bs (DJ f p) = Ifm bbs bs (f p)"
   1.361 -proof-
   1.362 -  have "Ifm bbs bs (DJ f p) = (\<exists> q \<in> set (disjuncts p). Ifm bbs bs (f q))"
   1.363 -    by (simp add: DJ_def evaldjf_ex) 
   1.364 -  also have "\<dots> = Ifm bbs bs (f p)" using fdj fF by (induct p rule: disjuncts.induct, auto)
   1.365 +proof -
   1.366 +  have "Ifm bbs bs (DJ f p) = (\<exists>q \<in> set (disjuncts p). Ifm bbs bs (f q))"
   1.367 +    by (simp add: DJ_def evaldjf_ex)
   1.368 +  also have "\<dots> = Ifm bbs bs (f p)"
   1.369 +    using fdj fF by (induct p rule: disjuncts.induct) auto
   1.370    finally show ?thesis .
   1.371  qed
   1.372  
   1.373 -lemma DJ_qf: assumes 
   1.374 -  fqf: "\<forall> p. qfree p \<longrightarrow> qfree (f p)"
   1.375 +lemma DJ_qf:
   1.376 +  assumes fqf: "\<forall>p. qfree p \<longrightarrow> qfree (f p)"
   1.377    shows "\<forall>p. qfree p \<longrightarrow> qfree (DJ f p) "
   1.378 -proof(clarify)
   1.379 -  fix  p assume qf: "qfree p"
   1.380 +proof clarify
   1.381 +  fix p assume qf: "qfree p"
   1.382    have th: "DJ f p = evaldjf f (disjuncts p)" by (simp add: DJ_def)
   1.383 -  from disjuncts_qf[OF qf] have "\<forall> q\<in> set (disjuncts p). qfree q" .
   1.384 -  with fqf have th':"\<forall> q\<in> set (disjuncts p). qfree (f q)" by blast
   1.385 -  
   1.386 +  from disjuncts_qf[OF qf] have "\<forall>q\<in> set (disjuncts p). qfree q" .
   1.387 +  with fqf have th':"\<forall>q\<in> set (disjuncts p). qfree (f q)" by blast
   1.388 +
   1.389    from evaldjf_qf[OF th'] th show "qfree (DJ f p)" by simp
   1.390  qed
   1.391  
   1.392 -lemma DJ_qe: assumes qe: "\<forall> bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bbs bs (qe p) = Ifm bbs bs (E p))"
   1.393 -  shows "\<forall> bs p. qfree p \<longrightarrow> qfree (DJ qe p) \<and> (Ifm bbs bs ((DJ qe p)) = Ifm bbs bs (E p))"
   1.394 -proof(clarify)
   1.395 -  fix p::fm and bs
   1.396 +lemma DJ_qe:
   1.397 +  assumes qe: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bbs bs (qe p) = Ifm bbs bs (E p))"
   1.398 +  shows "\<forall>bs p. qfree p \<longrightarrow> qfree (DJ qe p) \<and> (Ifm bbs bs ((DJ qe p)) = Ifm bbs bs (E p))"
   1.399 +proof clarify
   1.400 +  fix p :: fm and bs
   1.401    assume qf: "qfree p"
   1.402 -  from qe have qth: "\<forall> p. qfree p \<longrightarrow> qfree (qe p)" by blast
   1.403 +  from qe have qth: "\<forall>p. qfree p \<longrightarrow> qfree (qe p)" by blast
   1.404    from DJ_qf[OF qth] qf have qfth:"qfree (DJ qe p)" by auto
   1.405 -  have "Ifm bbs bs (DJ qe p) = (\<exists> q\<in> set (disjuncts p). Ifm bbs bs (qe q))"
   1.406 +  have "Ifm bbs bs (DJ qe p) = (\<exists>q\<in> set (disjuncts p). Ifm bbs bs (qe q))"
   1.407      by (simp add: DJ_def evaldjf_ex)
   1.408 -  also have "\<dots> = (\<exists> q \<in> set(disjuncts p). Ifm bbs bs (E q))" using qe disjuncts_qf[OF qf] by auto
   1.409 -  also have "\<dots> = Ifm bbs bs (E p)" by (induct p rule: disjuncts.induct, auto)
   1.410 -  finally show "qfree (DJ qe p) \<and> Ifm bbs bs (DJ qe p) = Ifm bbs bs (E p)" using qfth by blast
   1.411 +  also have "\<dots> = (\<exists>q \<in> set(disjuncts p). Ifm bbs bs (E q))"
   1.412 +    using qe disjuncts_qf[OF qf] by auto
   1.413 +  also have "\<dots> = Ifm bbs bs (E p)"
   1.414 +    by (induct p rule: disjuncts.induct) auto
   1.415 +  finally show "qfree (DJ qe p) \<and> Ifm bbs bs (DJ qe p) = Ifm bbs bs (E p)"
   1.416 +    using qfth by blast
   1.417  qed
   1.418 -  (* Simplification *)
   1.419 +
   1.420 +
   1.421 +text {* Simplification *}
   1.422  
   1.423 -  (* Algebraic simplifications for nums *)
   1.424 +text {* Algebraic simplifications for nums *}
   1.425  
   1.426 -fun bnds:: "num \<Rightarrow> nat list" where
   1.427 +fun bnds :: "num \<Rightarrow> nat list"
   1.428 +where
   1.429    "bnds (Bound n) = [n]"
   1.430  | "bnds (CN n c a) = n#(bnds a)"
   1.431  | "bnds (Neg a) = bnds a"
   1.432 @@ -368,26 +397,27 @@
   1.433  | "bnds (Mul i a) = bnds a"
   1.434  | "bnds a = []"
   1.435  
   1.436 -fun lex_ns:: "nat list \<Rightarrow> nat list \<Rightarrow> bool" where
   1.437 +fun lex_ns:: "nat list \<Rightarrow> nat list \<Rightarrow> bool"
   1.438 +where
   1.439    "lex_ns [] ms = True"
   1.440  | "lex_ns ns [] = False"
   1.441  | "lex_ns (n#ns) (m#ms) = (n<m \<or> ((n = m) \<and> lex_ns ns ms)) "
   1.442 -definition lex_bnd :: "num \<Rightarrow> num \<Rightarrow> bool" where
   1.443 -  "lex_bnd t s \<equiv> lex_ns (bnds t) (bnds s)"
   1.444  
   1.445 -consts
   1.446 -  numadd:: "num \<times> num \<Rightarrow> num"
   1.447 -recdef numadd "measure (\<lambda> (t,s). num_size t + num_size s)"
   1.448 +definition lex_bnd :: "num \<Rightarrow> num \<Rightarrow> bool"
   1.449 +  where "lex_bnd t s = lex_ns (bnds t) (bnds s)"
   1.450 +
   1.451 +consts numadd:: "num \<times> num \<Rightarrow> num"
   1.452 +recdef numadd "measure (\<lambda>(t,s). num_size t + num_size s)"
   1.453    "numadd (CN n1 c1 r1 ,CN n2 c2 r2) =
   1.454 -  (if n1=n2 then 
   1.455 -  (let c = c1 + c2
   1.456 -  in (if c=0 then numadd(r1,r2) else CN n1 c (numadd (r1,r2))))
   1.457 -  else if n1 \<le> n2 then CN n1 c1 (numadd (r1,Add (Mul c2 (Bound n2)) r2))
   1.458 -  else CN n2 c2 (numadd (Add (Mul c1 (Bound n1)) r1,r2)))"
   1.459 -  "numadd (CN n1 c1 r1, t) = CN n1 c1 (numadd (r1, t))"  
   1.460 -  "numadd (t,CN n2 c2 r2) = CN n2 c2 (numadd (t,r2))" 
   1.461 -  "numadd (C b1, C b2) = C (b1+b2)"
   1.462 -  "numadd (a,b) = Add a b"
   1.463 +    (if n1 = n2 then
   1.464 +      (let c = c1 + c2
   1.465 +       in if c=0 then numadd (r1, r2) else CN n1 c (numadd (r1, r2)))
   1.466 +     else if n1 \<le> n2 then CN n1 c1 (numadd (r1,Add (Mul c2 (Bound n2)) r2))
   1.467 +     else CN n2 c2 (numadd (Add (Mul c1 (Bound n1)) r1, r2)))"
   1.468 +  "numadd (CN n1 c1 r1, t) = CN n1 c1 (numadd (r1, t))"
   1.469 +  "numadd (t, CN n2 c2 r2) = CN n2 c2 (numadd (t, r2))"
   1.470 +  "numadd (C b1, C b2) = C (b1 + b2)"
   1.471 +  "numadd (a, b) = Add a b"
   1.472  
   1.473  (*function (sequential)
   1.474    numadd :: "num \<Rightarrow> num \<Rightarrow> num"
   1.475 @@ -401,335 +431,387 @@
   1.476        else
   1.477          Add (Mul c2 (Bound n2)) (numadd (Add (Mul c1 (Bound n1)) r1) r2))"
   1.478    | "numadd (Add (Mul c1 (Bound n1)) r1) t =
   1.479 -      Add (Mul c1 (Bound n1)) (numadd r1 t)"  
   1.480 +      Add (Mul c1 (Bound n1)) (numadd r1 t)"
   1.481    | "numadd t (Add (Mul c2 (Bound n2)) r2) =
   1.482 -      Add (Mul c2 (Bound n2)) (numadd t r2)" 
   1.483 +      Add (Mul c2 (Bound n2)) (numadd t r2)"
   1.484    | "numadd (C b1) (C b2) = C (b1 + b2)"
   1.485    | "numadd a b = Add a b"
   1.486  apply pat_completeness apply auto*)
   1.487 -  
   1.488 +
   1.489  lemma numadd: "Inum bs (numadd (t,s)) = Inum bs (Add t s)"
   1.490 -apply (induct t s rule: numadd.induct, simp_all add: Let_def)
   1.491 -apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
   1.492 - apply (case_tac "n1 = n2")
   1.493 -  apply(simp_all add: algebra_simps)
   1.494 -apply(simp add: distrib_right[symmetric])
   1.495 -done
   1.496 +  apply (induct t s rule: numadd.induct, simp_all add: Let_def)
   1.497 +  apply (case_tac "c1 + c2 = 0", case_tac "n1 \<le> n2", simp_all)
   1.498 +   apply (case_tac "n1 = n2")
   1.499 +    apply(simp_all add: algebra_simps)
   1.500 +  apply(simp add: distrib_right[symmetric])
   1.501 +  done
   1.502  
   1.503 -lemma numadd_nb: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))"
   1.504 -by (induct t s rule: numadd.induct, auto simp add: Let_def)
   1.505 +lemma numadd_nb: "numbound0 t \<Longrightarrow> numbound0 s \<Longrightarrow> numbound0 (numadd (t, s))"
   1.506 +  by (induct t s rule: numadd.induct) (auto simp add: Let_def)
   1.507  
   1.508 -fun nummul :: "int \<Rightarrow> num \<Rightarrow> num" where
   1.509 +fun nummul :: "int \<Rightarrow> num \<Rightarrow> num"
   1.510 +where
   1.511    "nummul i (C j) = C (i * j)"
   1.512  | "nummul i (CN n c t) = CN n (c*i) (nummul i t)"
   1.513  | "nummul i t = Mul i t"
   1.514  
   1.515 -lemma nummul: "\<And> i. Inum bs (nummul i t) = Inum bs (Mul i t)"
   1.516 -by (induct t rule: nummul.induct, auto simp add: algebra_simps numadd)
   1.517 +lemma nummul: "Inum bs (nummul i t) = Inum bs (Mul i t)"
   1.518 +  by (induct t arbitrary: i rule: nummul.induct) (auto simp add: algebra_simps numadd)
   1.519  
   1.520 -lemma nummul_nb: "\<And> i. numbound0 t \<Longrightarrow> numbound0 (nummul i t)"
   1.521 -by (induct t rule: nummul.induct, auto simp add: numadd_nb)
   1.522 +lemma nummul_nb: "numbound0 t \<Longrightarrow> numbound0 (nummul i t)"
   1.523 +  by (induct t arbitrary: i rule: nummul.induct) (auto simp add: numadd_nb)
   1.524  
   1.525 -definition numneg :: "num \<Rightarrow> num" where
   1.526 -  "numneg t \<equiv> nummul (- 1) t"
   1.527 +definition numneg :: "num \<Rightarrow> num"
   1.528 +  where "numneg t = nummul (- 1) t"
   1.529  
   1.530 -definition numsub :: "num \<Rightarrow> num \<Rightarrow> num" where
   1.531 -  "numsub s t \<equiv> (if s = t then C 0 else numadd (s, numneg t))"
   1.532 +definition numsub :: "num \<Rightarrow> num \<Rightarrow> num"
   1.533 +  where "numsub s t = (if s = t then C 0 else numadd (s, numneg t))"
   1.534  
   1.535  lemma numneg: "Inum bs (numneg t) = Inum bs (Neg t)"
   1.536 -using numneg_def nummul by simp
   1.537 +  using numneg_def nummul by simp
   1.538  
   1.539  lemma numneg_nb: "numbound0 t \<Longrightarrow> numbound0 (numneg t)"
   1.540 -using numneg_def nummul_nb by simp
   1.541 +  using numneg_def nummul_nb by simp
   1.542  
   1.543  lemma numsub: "Inum bs (numsub a b) = Inum bs (Sub a b)"
   1.544 -using numneg numadd numsub_def by simp
   1.545 +  using numneg numadd numsub_def by simp
   1.546  
   1.547 -lemma numsub_nb: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numsub t s)"
   1.548 -using numsub_def numadd_nb numneg_nb by simp
   1.549 +lemma numsub_nb: "numbound0 t \<Longrightarrow> numbound0 s \<Longrightarrow> numbound0 (numsub t s)"
   1.550 +  using numsub_def numadd_nb numneg_nb by simp
   1.551  
   1.552 -fun
   1.553 -  simpnum :: "num \<Rightarrow> num"
   1.554 +fun simpnum :: "num \<Rightarrow> num"
   1.555  where
   1.556    "simpnum (C j) = C j"
   1.557 -  | "simpnum (Bound n) = CN n 1 (C 0)"
   1.558 -  | "simpnum (Neg t) = numneg (simpnum t)"
   1.559 -  | "simpnum (Add t s) = numadd (simpnum t, simpnum s)"
   1.560 -  | "simpnum (Sub t s) = numsub (simpnum t) (simpnum s)"
   1.561 -  | "simpnum (Mul i t) = (if i = 0 then C 0 else nummul i (simpnum t))"
   1.562 -  | "simpnum t = t"
   1.563 +| "simpnum (Bound n) = CN n 1 (C 0)"
   1.564 +| "simpnum (Neg t) = numneg (simpnum t)"
   1.565 +| "simpnum (Add t s) = numadd (simpnum t, simpnum s)"
   1.566 +| "simpnum (Sub t s) = numsub (simpnum t) (simpnum s)"
   1.567 +| "simpnum (Mul i t) = (if i = 0 then C 0 else nummul i (simpnum t))"
   1.568 +| "simpnum t = t"
   1.569  
   1.570  lemma simpnum_ci: "Inum bs (simpnum t) = Inum bs t"
   1.571 -by (induct t rule: simpnum.induct, auto simp add: numneg numadd numsub nummul)
   1.572 +  by (induct t rule: simpnum.induct) (auto simp add: numneg numadd numsub nummul)
   1.573  
   1.574 -lemma simpnum_numbound0: 
   1.575 -  "numbound0 t \<Longrightarrow> numbound0 (simpnum t)"
   1.576 -by (induct t rule: simpnum.induct, auto simp add: numadd_nb numsub_nb nummul_nb numneg_nb)
   1.577 +lemma simpnum_numbound0: "numbound0 t \<Longrightarrow> numbound0 (simpnum t)"
   1.578 +  by (induct t rule: simpnum.induct) (auto simp add: numadd_nb numsub_nb nummul_nb numneg_nb)
   1.579  
   1.580 -fun
   1.581 -  not :: "fm \<Rightarrow> fm"
   1.582 +fun not :: "fm \<Rightarrow> fm"
   1.583  where
   1.584    "not (NOT p) = p"
   1.585 -  | "not T = F"
   1.586 -  | "not F = T"
   1.587 -  | "not p = NOT p"
   1.588 +| "not T = F"
   1.589 +| "not F = T"
   1.590 +| "not p = NOT p"
   1.591 +
   1.592  lemma not: "Ifm bbs bs (not p) = Ifm bbs bs (NOT p)"
   1.593    by (cases p) auto
   1.594 +
   1.595  lemma not_qf: "qfree p \<Longrightarrow> qfree (not p)"
   1.596    by (cases p) auto
   1.597 +
   1.598  lemma not_bn: "bound0 p \<Longrightarrow> bound0 (not p)"
   1.599    by (cases p) auto
   1.600  
   1.601 -definition conj :: "fm \<Rightarrow> fm \<Rightarrow> fm" where
   1.602 -  "conj p q \<equiv> (if (p = F \<or> q=F) then F else if p=T then q else if q=T then p else And p q)"
   1.603 +definition conj :: "fm \<Rightarrow> fm \<Rightarrow> fm"
   1.604 +  where
   1.605 +    "conj p q = (if (p = F \<or> q=F) then F else if p=T then q else if q=T then p else And p q)"
   1.606 +
   1.607  lemma conj: "Ifm bbs bs (conj p q) = Ifm bbs bs (And p q)"
   1.608 -by (cases "p=F \<or> q=F",simp_all add: conj_def) (cases p,simp_all)
   1.609 +  by (cases "p=F \<or> q=F", simp_all add: conj_def) (cases p, simp_all)
   1.610  
   1.611 -lemma conj_qf: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (conj p q)"
   1.612 -using conj_def by auto 
   1.613 -lemma conj_nb: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (conj p q)"
   1.614 -using conj_def by auto 
   1.615 +lemma conj_qf: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (conj p q)"
   1.616 +  using conj_def by auto
   1.617  
   1.618 -definition disj :: "fm \<Rightarrow> fm \<Rightarrow> fm" where
   1.619 -  "disj p q \<equiv> (if (p = T \<or> q=T) then T else if p=F then q else if q=F then p else Or p q)"
   1.620 +lemma conj_nb: "bound0 p \<Longrightarrow> bound0 q \<Longrightarrow> bound0 (conj p q)"
   1.621 +  using conj_def by auto
   1.622 +
   1.623 +definition disj :: "fm \<Rightarrow> fm \<Rightarrow> fm"
   1.624 +  where
   1.625 +    "disj p q =
   1.626 +      (if (p = T \<or> q=T) then T else if p=F then q else if q=F then p else Or p q)"
   1.627  
   1.628  lemma disj: "Ifm bbs bs (disj p q) = Ifm bbs bs (Or p q)"
   1.629 -by (cases "p=T \<or> q=T",simp_all add: disj_def) (cases p,simp_all)
   1.630 +  by (cases "p=T \<or> q=T", simp_all add: disj_def) (cases p, simp_all)
   1.631 +
   1.632  lemma disj_qf: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (disj p q)"
   1.633 -using disj_def by auto 
   1.634 +  using disj_def by auto
   1.635 +
   1.636  lemma disj_nb: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (disj p q)"
   1.637 -using disj_def by auto 
   1.638 +  using disj_def by auto
   1.639  
   1.640 -definition imp :: "fm \<Rightarrow> fm \<Rightarrow> fm" where
   1.641 -  "imp p q \<equiv> (if (p = F \<or> q=T) then T else if p=T then q else if q=F then not p else Imp p q)"
   1.642 +definition imp :: "fm \<Rightarrow> fm \<Rightarrow> fm"
   1.643 +  where
   1.644 +    "imp p q = (if (p = F \<or> q=T) then T else if p=T then q else if q=F then not p else Imp p q)"
   1.645 +
   1.646  lemma imp: "Ifm bbs bs (imp p q) = Ifm bbs bs (Imp p q)"
   1.647 -by (cases "p=F \<or> q=T",simp_all add: imp_def,cases p) (simp_all add: not)
   1.648 -lemma imp_qf: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (imp p q)"
   1.649 -using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def,cases p) (simp_all add: not_qf) 
   1.650 -lemma imp_nb: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (imp p q)"
   1.651 -using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def,cases p) simp_all
   1.652 +  by (cases "p=F \<or> q=T", simp_all add: imp_def, cases p) (simp_all add: not)
   1.653 +
   1.654 +lemma imp_qf: "qfree p \<Longrightarrow> qfree q \<Longrightarrow> qfree (imp p q)"
   1.655 +  using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def,cases p) (simp_all add: not_qf)
   1.656 +
   1.657 +lemma imp_nb: "bound0 p \<Longrightarrow> bound0 q \<Longrightarrow> bound0 (imp p q)"
   1.658 +  using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def,cases p) simp_all
   1.659  
   1.660 -definition iff :: "fm \<Rightarrow> fm \<Rightarrow> fm" where
   1.661 -  "iff p q \<equiv> (if (p = q) then T else if (p = not q \<or> not p = q) then F else 
   1.662 -       if p=F then not q else if q=F then not p else if p=T then q else if q=T then p else 
   1.663 -  Iff p q)"
   1.664 +definition iff :: "fm \<Rightarrow> fm \<Rightarrow> fm"
   1.665 +  where
   1.666 +    "iff p q =
   1.667 +      (if (p = q) then T
   1.668 +       else if (p = not q \<or> not p = q) then F
   1.669 +       else if p = F then not q
   1.670 +       else if q = F then not p
   1.671 +       else if p = T then q
   1.672 +       else if q = T then p
   1.673 +       else Iff p q)"
   1.674 +
   1.675  lemma iff: "Ifm bbs bs (iff p q) = Ifm bbs bs (Iff p q)"
   1.676 -  by (unfold iff_def,cases "p=q", simp,cases "p=not q", simp add:not) 
   1.677 -(cases "not p= q", auto simp add:not)
   1.678 +  by (unfold iff_def,cases "p=q", simp,cases "p=not q", simp add:not)
   1.679 +    (cases "not p= q", auto simp add:not)
   1.680 +
   1.681  lemma iff_qf: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (iff p q)"
   1.682    by (unfold iff_def,cases "p=q", auto simp add: not_qf)
   1.683 -lemma iff_nb: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (iff p q)"
   1.684 -using iff_def by (unfold iff_def,cases "p=q", auto simp add: not_bn)
   1.685  
   1.686 -function (sequential)
   1.687 -  simpfm :: "fm \<Rightarrow> fm"
   1.688 +lemma iff_nb: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (iff p q)"
   1.689 +  using iff_def by (unfold iff_def,cases "p=q", auto simp add: not_bn)
   1.690 +
   1.691 +function (sequential) simpfm :: "fm \<Rightarrow> fm"
   1.692  where
   1.693    "simpfm (And p q) = conj (simpfm p) (simpfm q)"
   1.694 -  | "simpfm (Or p q) = disj (simpfm p) (simpfm q)"
   1.695 -  | "simpfm (Imp p q) = imp (simpfm p) (simpfm q)"
   1.696 -  | "simpfm (Iff p q) = iff (simpfm p) (simpfm q)"
   1.697 -  | "simpfm (NOT p) = not (simpfm p)"
   1.698 -  | "simpfm (Lt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v < 0) then T else F 
   1.699 -      | _ \<Rightarrow> Lt a')"
   1.700 -  | "simpfm (Le a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<le> 0)  then T else F | _ \<Rightarrow> Le a')"
   1.701 -  | "simpfm (Gt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v > 0)  then T else F | _ \<Rightarrow> Gt a')"
   1.702 -  | "simpfm (Ge a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<ge> 0)  then T else F | _ \<Rightarrow> Ge a')"
   1.703 -  | "simpfm (Eq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v = 0)  then T else F | _ \<Rightarrow> Eq a')"
   1.704 -  | "simpfm (NEq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<noteq> 0)  then T else F | _ \<Rightarrow> NEq a')"
   1.705 -  | "simpfm (Dvd i a) = (if i=0 then simpfm (Eq a)
   1.706 -             else if (abs i = 1) then T
   1.707 -             else let a' = simpnum a in case a' of C v \<Rightarrow> if (i dvd v)  then T else F | _ \<Rightarrow> Dvd i a')"
   1.708 -  | "simpfm (NDvd i a) = (if i=0 then simpfm (NEq a) 
   1.709 -             else if (abs i = 1) then F
   1.710 -             else let a' = simpnum a in case a' of C v \<Rightarrow> if (\<not>(i dvd v)) then T else F | _ \<Rightarrow> NDvd i a')"
   1.711 -  | "simpfm p = p"
   1.712 -by pat_completeness auto
   1.713 +| "simpfm (Or p q) = disj (simpfm p) (simpfm q)"
   1.714 +| "simpfm (Imp p q) = imp (simpfm p) (simpfm q)"
   1.715 +| "simpfm (Iff p q) = iff (simpfm p) (simpfm q)"
   1.716 +| "simpfm (NOT p) = not (simpfm p)"
   1.717 +| "simpfm (Lt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v < 0) then T else F | _ \<Rightarrow> Lt a')"
   1.718 +| "simpfm (Le a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<le> 0)  then T else F | _ \<Rightarrow> Le a')"
   1.719 +| "simpfm (Gt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v > 0)  then T else F | _ \<Rightarrow> Gt a')"
   1.720 +| "simpfm (Ge a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<ge> 0)  then T else F | _ \<Rightarrow> Ge a')"
   1.721 +| "simpfm (Eq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v = 0)  then T else F | _ \<Rightarrow> Eq a')"
   1.722 +| "simpfm (NEq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<noteq> 0)  then T else F | _ \<Rightarrow> NEq a')"
   1.723 +| "simpfm (Dvd i a) =
   1.724 +    (if i=0 then simpfm (Eq a)
   1.725 +     else if (abs i = 1) then T
   1.726 +     else let a' = simpnum a in case a' of C v \<Rightarrow> if (i dvd v)  then T else F | _ \<Rightarrow> Dvd i a')"
   1.727 +| "simpfm (NDvd i a) =
   1.728 +    (if i=0 then simpfm (NEq a)
   1.729 +     else if (abs i = 1) then F
   1.730 +     else let a' = simpnum a in case a' of C v \<Rightarrow> if (\<not>(i dvd v)) then T else F | _ \<Rightarrow> NDvd i a')"
   1.731 +| "simpfm p = p"
   1.732 +  by pat_completeness auto
   1.733  termination by (relation "measure fmsize") auto
   1.734  
   1.735  lemma simpfm: "Ifm bbs bs (simpfm p) = Ifm bbs bs p"
   1.736  proof(induct p rule: simpfm.induct)
   1.737 -  case (6 a) let ?sa = "simpnum a" from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
   1.738 -  {fix v assume "?sa = C v" hence ?case using sa by simp }
   1.739 -  moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa 
   1.740 -      by (cases ?sa, simp_all add: Let_def)}
   1.741 +  case (6 a)
   1.742 +  let ?sa = "simpnum a"
   1.743 +  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
   1.744 +  { fix v assume "?sa = C v" hence ?case using sa by simp }
   1.745 +  moreover {
   1.746 +    assume "\<not> (\<exists>v. ?sa = C v)"
   1.747 +    hence ?case using sa by (cases ?sa) (simp_all add: Let_def)
   1.748 +  }
   1.749    ultimately show ?case by blast
   1.750  next
   1.751 -  case (7 a)  let ?sa = "simpnum a" 
   1.752 +  case (7 a)
   1.753 +  let ?sa = "simpnum a"
   1.754    from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
   1.755 -  {fix v assume "?sa = C v" hence ?case using sa by simp }
   1.756 -  moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa 
   1.757 -      by (cases ?sa, simp_all add: Let_def)}
   1.758 -  ultimately show ?case by blast
   1.759 -next
   1.760 -  case (8 a)  let ?sa = "simpnum a" 
   1.761 -  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
   1.762 -  {fix v assume "?sa = C v" hence ?case using sa by simp }
   1.763 -  moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa 
   1.764 -      by (cases ?sa, simp_all add: Let_def)}
   1.765 +  { fix v assume "?sa = C v" hence ?case using sa by simp }
   1.766 +  moreover {
   1.767 +    assume "\<not> (\<exists>v. ?sa = C v)"
   1.768 +    hence ?case using sa by (cases ?sa) (simp_all add: Let_def)
   1.769 +  }
   1.770    ultimately show ?case by blast
   1.771  next
   1.772 -  case (9 a)  let ?sa = "simpnum a" 
   1.773 +  case (8 a)
   1.774 +  let ?sa = "simpnum a"
   1.775    from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
   1.776 -  {fix v assume "?sa = C v" hence ?case using sa by simp }
   1.777 -  moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa 
   1.778 -      by (cases ?sa, simp_all add: Let_def)}
   1.779 +  { fix v assume "?sa = C v" hence ?case using sa by simp }
   1.780 +  moreover {
   1.781 +    assume "\<not> (\<exists>v. ?sa = C v)"
   1.782 +    hence ?case using sa by (cases ?sa) (simp_all add: Let_def)
   1.783 +  }
   1.784    ultimately show ?case by blast
   1.785  next
   1.786 -  case (10 a)  let ?sa = "simpnum a" 
   1.787 +  case (9 a)
   1.788 +  let ?sa = "simpnum a"
   1.789    from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
   1.790 -  {fix v assume "?sa = C v" hence ?case using sa by simp }
   1.791 -  moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa 
   1.792 -      by (cases ?sa, simp_all add: Let_def)}
   1.793 +  { fix v assume "?sa = C v" hence ?case using sa by simp }
   1.794 +  moreover {
   1.795 +    assume "\<not> (\<exists>v. ?sa = C v)"
   1.796 +    hence ?case using sa by (cases ?sa) (simp_all add: Let_def)
   1.797 +  }
   1.798    ultimately show ?case by blast
   1.799  next
   1.800 -  case (11 a)  let ?sa = "simpnum a" 
   1.801 +  case (10 a)
   1.802 +  let ?sa = "simpnum a"
   1.803    from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
   1.804 -  {fix v assume "?sa = C v" hence ?case using sa by simp }
   1.805 -  moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa 
   1.806 -      by (cases ?sa, simp_all add: Let_def)}
   1.807 +  { fix v assume "?sa = C v" hence ?case using sa by simp }
   1.808 +  moreover {
   1.809 +    assume "\<not> (\<exists>v. ?sa = C v)"
   1.810 +    hence ?case using sa by (cases ?sa) (simp_all add: Let_def)
   1.811 +  }
   1.812    ultimately show ?case by blast
   1.813  next
   1.814 -  case (12 i a)  let ?sa = "simpnum a" from simpnum_ci 
   1.815 -  have sa: "Inum bs ?sa = Inum bs a" by simp
   1.816 -  have "i=0 \<or> abs i = 1 \<or> (i\<noteq>0 \<and> (abs i \<noteq> 1))" by auto
   1.817 -  {assume "i=0" hence ?case using "12.hyps" by (simp add: dvd_def Let_def)}
   1.818 -  moreover 
   1.819 -  {assume i1: "abs i = 1"
   1.820 -      from one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
   1.821 -      have ?case using i1 apply (cases "i=0", simp_all add: Let_def) 
   1.822 -        by (cases "i > 0", simp_all)}
   1.823 -  moreover   
   1.824 -  {assume inz: "i\<noteq>0" and cond: "abs i \<noteq> 1"
   1.825 -    {fix v assume "?sa = C v" hence ?case using sa[symmetric] inz cond
   1.826 -        by (cases "abs i = 1", auto) }
   1.827 -    moreover {assume "\<not> (\<exists> v. ?sa = C v)" 
   1.828 -      hence "simpfm (Dvd i a) = Dvd i ?sa" using inz cond 
   1.829 -        by (cases ?sa, auto simp add: Let_def)
   1.830 -      hence ?case using sa by simp}
   1.831 -    ultimately have ?case by blast}
   1.832 +  case (11 a)
   1.833 +  let ?sa = "simpnum a"
   1.834 +  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
   1.835 +  { fix v assume "?sa = C v" hence ?case using sa by simp }
   1.836 +  moreover {
   1.837 +    assume "\<not> (\<exists>v. ?sa = C v)"
   1.838 +    hence ?case using sa by (cases ?sa) (simp_all add: Let_def)
   1.839 +  }
   1.840    ultimately show ?case by blast
   1.841  next
   1.842 -  case (13 i a)  let ?sa = "simpnum a" from simpnum_ci 
   1.843 +  case (12 i a)
   1.844 +  let ?sa = "simpnum a"
   1.845 +  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
   1.846 +  { assume "i=0" hence ?case using "12.hyps" by (simp add: dvd_def Let_def) }
   1.847 +  moreover
   1.848 +  { assume i1: "abs i = 1"
   1.849 +    from one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
   1.850 +    have ?case using i1
   1.851 +      apply (cases "i=0", simp_all add: Let_def)
   1.852 +      apply (cases "i > 0", simp_all)
   1.853 +      done
   1.854 +  }
   1.855 +  moreover
   1.856 +  { assume inz: "i\<noteq>0" and cond: "abs i \<noteq> 1"
   1.857 +    { fix v assume "?sa = C v"
   1.858 +      hence ?case using sa[symmetric] inz cond
   1.859 +        by (cases "abs i = 1") auto }
   1.860 +    moreover {
   1.861 +      assume "\<not> (\<exists>v. ?sa = C v)"
   1.862 +      hence "simpfm (Dvd i a) = Dvd i ?sa" using inz cond
   1.863 +        by (cases ?sa) (auto simp add: Let_def)
   1.864 +      hence ?case using sa by simp }
   1.865 +    ultimately have ?case by blast }
   1.866 +  ultimately show ?case by blast
   1.867 +next
   1.868 +  case (13 i a)
   1.869 +  let ?sa = "simpnum a" from simpnum_ci
   1.870    have sa: "Inum bs ?sa = Inum bs a" by simp
   1.871 -  have "i=0 \<or> abs i = 1 \<or> (i\<noteq>0 \<and> (abs i \<noteq> 1))" by auto
   1.872 -  {assume "i=0" hence ?case using "13.hyps" by (simp add: dvd_def Let_def)}
   1.873 -  moreover 
   1.874 -  {assume i1: "abs i = 1"
   1.875 -      from one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
   1.876 -      have ?case using i1 apply (cases "i=0", simp_all add: Let_def)
   1.877 -      apply (cases "i > 0", simp_all) done}
   1.878 -  moreover   
   1.879 -  {assume inz: "i\<noteq>0" and cond: "abs i \<noteq> 1"
   1.880 -    {fix v assume "?sa = C v" hence ?case using sa[symmetric] inz cond
   1.881 -        by (cases "abs i = 1", auto) }
   1.882 -    moreover {assume "\<not> (\<exists> v. ?sa = C v)" 
   1.883 -      hence "simpfm (NDvd i a) = NDvd i ?sa" using inz cond 
   1.884 -        by (cases ?sa, auto simp add: Let_def)
   1.885 -      hence ?case using sa by simp}
   1.886 -    ultimately have ?case by blast}
   1.887 +  { assume "i=0" hence ?case using "13.hyps" by (simp add: dvd_def Let_def) }
   1.888 +  moreover
   1.889 +  { assume i1: "abs i = 1"
   1.890 +    from one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
   1.891 +    have ?case using i1
   1.892 +      apply (cases "i=0", simp_all add: Let_def)
   1.893 +      apply (cases "i > 0", simp_all)
   1.894 +      done
   1.895 +  }
   1.896 +  moreover
   1.897 +  { assume inz: "i\<noteq>0" and cond: "abs i \<noteq> 1"
   1.898 +    { fix v assume "?sa = C v"
   1.899 +      hence ?case using sa[symmetric] inz cond
   1.900 +        by (cases "abs i = 1") auto }
   1.901 +    moreover {
   1.902 +      assume "\<not> (\<exists>v. ?sa = C v)"
   1.903 +      hence "simpfm (NDvd i a) = NDvd i ?sa" using inz cond
   1.904 +        by (cases ?sa) (auto simp add: Let_def)
   1.905 +      hence ?case using sa by simp }
   1.906 +    ultimately have ?case by blast }
   1.907    ultimately show ?case by blast
   1.908 -qed (induct p rule: simpfm.induct, simp_all add: conj disj imp iff not)
   1.909 +qed (simp_all add: conj disj imp iff not)
   1.910  
   1.911  lemma simpfm_bound0: "bound0 p \<Longrightarrow> bound0 (simpfm p)"
   1.912 -proof(induct p rule: simpfm.induct)
   1.913 +proof (induct p rule: simpfm.induct)
   1.914    case (6 a) hence nb: "numbound0 a" by simp
   1.915    hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
   1.916 -  thus ?case by (cases "simpnum a", auto simp add: Let_def)
   1.917 +  thus ?case by (cases "simpnum a") (auto simp add: Let_def)
   1.918  next
   1.919    case (7 a) hence nb: "numbound0 a" by simp
   1.920    hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
   1.921 -  thus ?case by (cases "simpnum a", auto simp add: Let_def)
   1.922 +  thus ?case by (cases "simpnum a") (auto simp add: Let_def)
   1.923  next
   1.924    case (8 a) hence nb: "numbound0 a" by simp
   1.925    hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
   1.926 -  thus ?case by (cases "simpnum a", auto simp add: Let_def)
   1.927 +  thus ?case by (cases "simpnum a") (auto simp add: Let_def)
   1.928  next
   1.929    case (9 a) hence nb: "numbound0 a" by simp
   1.930    hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
   1.931 -  thus ?case by (cases "simpnum a", auto simp add: Let_def)
   1.932 +  thus ?case by (cases "simpnum a") (auto simp add: Let_def)
   1.933  next
   1.934    case (10 a) hence nb: "numbound0 a" by simp
   1.935    hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
   1.936 -  thus ?case by (cases "simpnum a", auto simp add: Let_def)
   1.937 +  thus ?case by (cases "simpnum a") (auto simp add: Let_def)
   1.938  next
   1.939    case (11 a) hence nb: "numbound0 a" by simp
   1.940    hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
   1.941 -  thus ?case by (cases "simpnum a", auto simp add: Let_def)
   1.942 +  thus ?case by (cases "simpnum a") (auto simp add: Let_def)
   1.943  next
   1.944    case (12 i a) hence nb: "numbound0 a" by simp
   1.945    hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
   1.946 -  thus ?case by (cases "simpnum a", auto simp add: Let_def)
   1.947 +  thus ?case by (cases "simpnum a") (auto simp add: Let_def)
   1.948  next
   1.949    case (13 i a) hence nb: "numbound0 a" by simp
   1.950    hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
   1.951 -  thus ?case by (cases "simpnum a", auto simp add: Let_def)
   1.952 -qed(auto simp add: disj_def imp_def iff_def conj_def not_bn)
   1.953 +  thus ?case by (cases "simpnum a") (auto simp add: Let_def)
   1.954 +qed (auto simp add: disj_def imp_def iff_def conj_def not_bn)
   1.955  
   1.956  lemma simpfm_qf: "qfree p \<Longrightarrow> qfree (simpfm p)"
   1.957 -by (induct p rule: simpfm.induct, auto simp add: disj_qf imp_qf iff_qf conj_qf not_qf Let_def)
   1.958 - (case_tac "simpnum a",auto)+
   1.959 +  by (induct p rule: simpfm.induct, auto simp add: disj_qf imp_qf iff_qf conj_qf not_qf Let_def)
   1.960 +    (case_tac "simpnum a", auto)+
   1.961  
   1.962 -  (* Generic quantifier elimination *)
   1.963 -function (sequential) qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm" where
   1.964 -  "qelim (E p) = (\<lambda> qe. DJ qe (qelim p qe))"
   1.965 -| "qelim (A p) = (\<lambda> qe. not (qe ((qelim (NOT p) qe))))"
   1.966 -| "qelim (NOT p) = (\<lambda> qe. not (qelim p qe))"
   1.967 -| "qelim (And p q) = (\<lambda> qe. conj (qelim p qe) (qelim q qe))" 
   1.968 -| "qelim (Or  p q) = (\<lambda> qe. disj (qelim p qe) (qelim q qe))" 
   1.969 -| "qelim (Imp p q) = (\<lambda> qe. imp (qelim p qe) (qelim q qe))"
   1.970 -| "qelim (Iff p q) = (\<lambda> qe. iff (qelim p qe) (qelim q qe))"
   1.971 -| "qelim p = (\<lambda> y. simpfm p)"
   1.972 -by pat_completeness auto
   1.973 +text {* Generic quantifier elimination *}
   1.974 +function (sequential) qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm"
   1.975 +where
   1.976 +  "qelim (E p) = (\<lambda>qe. DJ qe (qelim p qe))"
   1.977 +| "qelim (A p) = (\<lambda>qe. not (qe ((qelim (NOT p) qe))))"
   1.978 +| "qelim (NOT p) = (\<lambda>qe. not (qelim p qe))"
   1.979 +| "qelim (And p q) = (\<lambda>qe. conj (qelim p qe) (qelim q qe))"
   1.980 +| "qelim (Or  p q) = (\<lambda>qe. disj (qelim p qe) (qelim q qe))"
   1.981 +| "qelim (Imp p q) = (\<lambda>qe. imp (qelim p qe) (qelim q qe))"
   1.982 +| "qelim (Iff p q) = (\<lambda>qe. iff (qelim p qe) (qelim q qe))"
   1.983 +| "qelim p = (\<lambda>y. simpfm p)"
   1.984 +  by pat_completeness auto
   1.985  termination by (relation "measure fmsize") auto
   1.986  
   1.987  lemma qelim_ci:
   1.988 -  assumes qe_inv: "\<forall> bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bbs bs (qe p) = Ifm bbs bs (E p))"
   1.989 -  shows "\<And> bs. qfree (qelim p qe) \<and> (Ifm bbs bs (qelim p qe) = Ifm bbs bs p)"
   1.990 -using qe_inv DJ_qe[OF qe_inv] 
   1.991 -by(induct p rule: qelim.induct) 
   1.992 -(auto simp add: not disj conj iff imp not_qf disj_qf conj_qf imp_qf iff_qf 
   1.993 -  simpfm simpfm_qf simp del: simpfm.simps)
   1.994 -  (* Linearity for fm where Bound 0 ranges over \<int> *)
   1.995 +  assumes qe_inv: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bbs bs (qe p) = Ifm bbs bs (E p))"
   1.996 +  shows "\<And>bs. qfree (qelim p qe) \<and> (Ifm bbs bs (qelim p qe) = Ifm bbs bs p)"
   1.997 +  using qe_inv DJ_qe[OF qe_inv]
   1.998 +  by(induct p rule: qelim.induct)
   1.999 +  (auto simp add: not disj conj iff imp not_qf disj_qf conj_qf imp_qf iff_qf
  1.1000 +    simpfm simpfm_qf simp del: simpfm.simps)
  1.1001  
  1.1002 -fun zsplit0 :: "num \<Rightarrow> int \<times> num" (* splits the bounded from the unbounded part*)
  1.1003 +text {* Linearity for fm where Bound 0 ranges over @{text "\<int>"} *}
  1.1004 +
  1.1005 +fun zsplit0 :: "num \<Rightarrow> int \<times> num"  -- {* splits the bounded from the unbounded part *}
  1.1006  where
  1.1007    "zsplit0 (C c) = (0,C c)"
  1.1008 -  | "zsplit0 (Bound n) = (if n=0 then (1, C 0) else (0,Bound n))"
  1.1009 -  | "zsplit0 (CN n i a) = 
  1.1010 -      (let (i',a') =  zsplit0 a 
  1.1011 -       in if n=0 then (i+i', a') else (i',CN n i a'))"
  1.1012 -  | "zsplit0 (Neg a) = (let (i',a') =  zsplit0 a in (-i', Neg a'))"
  1.1013 -  | "zsplit0 (Add a b) = (let (ia,a') =  zsplit0 a ; 
  1.1014 -                            (ib,b') =  zsplit0 b 
  1.1015 -                            in (ia+ib, Add a' b'))"
  1.1016 -  | "zsplit0 (Sub a b) = (let (ia,a') =  zsplit0 a ; 
  1.1017 -                            (ib,b') =  zsplit0 b 
  1.1018 -                            in (ia-ib, Sub a' b'))"
  1.1019 -  | "zsplit0 (Mul i a) = (let (i',a') =  zsplit0 a in (i*i', Mul i a'))"
  1.1020 +| "zsplit0 (Bound n) = (if n=0 then (1, C 0) else (0,Bound n))"
  1.1021 +| "zsplit0 (CN n i a) =
  1.1022 +    (let (i',a') =  zsplit0 a
  1.1023 +     in if n=0 then (i+i', a') else (i',CN n i a'))"
  1.1024 +| "zsplit0 (Neg a) = (let (i',a') =  zsplit0 a in (-i', Neg a'))"
  1.1025 +| "zsplit0 (Add a b) = (let (ia,a') =  zsplit0 a ;
  1.1026 +                          (ib,b') =  zsplit0 b
  1.1027 +                          in (ia+ib, Add a' b'))"
  1.1028 +| "zsplit0 (Sub a b) = (let (ia,a') =  zsplit0 a ;
  1.1029 +                          (ib,b') =  zsplit0 b
  1.1030 +                          in (ia-ib, Sub a' b'))"
  1.1031 +| "zsplit0 (Mul i a) = (let (i',a') =  zsplit0 a in (i*i', Mul i a'))"
  1.1032  
  1.1033  lemma zsplit0_I:
  1.1034 -  shows "\<And> n a. zsplit0 t = (n,a) \<Longrightarrow> (Inum ((x::int) #bs) (CN 0 n a) = Inum (x #bs) t) \<and> numbound0 a"
  1.1035 -  (is "\<And> n a. ?S t = (n,a) \<Longrightarrow> (?I x (CN 0 n a) = ?I x t) \<and> ?N a")
  1.1036 -proof(induct t rule: zsplit0.induct)
  1.1037 -  case (1 c n a) thus ?case by auto 
  1.1038 +  shows "\<And>n a. zsplit0 t = (n,a) \<Longrightarrow> (Inum ((x::int) #bs) (CN 0 n a) = Inum (x #bs) t) \<and> numbound0 a"
  1.1039 +  (is "\<And>n a. ?S t = (n,a) \<Longrightarrow> (?I x (CN 0 n a) = ?I x t) \<and> ?N a")
  1.1040 +proof (induct t rule: zsplit0.induct)
  1.1041 +  case (1 c n a) thus ?case by auto
  1.1042  next
  1.1043    case (2 m n a) thus ?case by (cases "m=0") auto
  1.1044  next
  1.1045    case (3 m i a n a')
  1.1046    let ?j = "fst (zsplit0 a)"
  1.1047    let ?b = "snd (zsplit0 a)"
  1.1048 -  have abj: "zsplit0 a = (?j,?b)" by simp 
  1.1049 -  {assume "m\<noteq>0" 
  1.1050 +  have abj: "zsplit0 a = (?j,?b)" by simp
  1.1051 +  {assume "m\<noteq>0"
  1.1052      with 3(1)[OF abj] 3(2) have ?case by (auto simp add: Let_def split_def)}
  1.1053    moreover
  1.1054    {assume m0: "m =0"
  1.1055 -    with abj have th: "a'=?b \<and> n=i+?j" using 3 
  1.1056 +    with abj have th: "a'=?b \<and> n=i+?j" using 3
  1.1057        by (simp add: Let_def split_def)
  1.1058      from abj 3 m0 have th2: "(?I x (CN 0 ?j ?b) = ?I x a) \<and> ?N ?b" by blast
  1.1059      from th have "?I x (CN 0 n a') = ?I x (CN 0 (i+?j) ?b)" by simp
  1.1060      also from th2 have "\<dots> = ?I x (CN 0 i (CN 0 ?j ?b))" by (simp add: distrib_right)
  1.1061    finally have "?I x (CN 0 n a') = ?I  x (CN 0 i a)" using th2 by simp
  1.1062 -  with th2 th have ?case using m0 by blast} 
  1.1063 +  with th2 th have ?case using m0 by blast}
  1.1064  ultimately show ?case by blast
  1.1065  next
  1.1066    case (4 t n a)
  1.1067 @@ -745,15 +827,15 @@
  1.1068    let ?as = "snd (zsplit0 s)"
  1.1069    let ?nt = "fst (zsplit0 t)"
  1.1070    let ?at = "snd (zsplit0 t)"
  1.1071 -  have abjs: "zsplit0 s = (?ns,?as)" by simp 
  1.1072 -  moreover have abjt:  "zsplit0 t = (?nt,?at)" by simp 
  1.1073 +  have abjs: "zsplit0 s = (?ns,?as)" by simp
  1.1074 +  moreover have abjt:  "zsplit0 t = (?nt,?at)" by simp
  1.1075    ultimately have th: "a=Add ?as ?at \<and> n=?ns + ?nt" using 5
  1.1076      by (simp add: Let_def split_def)
  1.1077 -  from abjs[symmetric] have bluddy: "\<exists> x y. (x,y) = zsplit0 s" by blast
  1.1078 -  from 5 have "(\<exists> x y. (x,y) = zsplit0 s) \<longrightarrow> (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t \<and> numbound0 xb)" by auto
  1.1079 +  from abjs[symmetric] have bluddy: "\<exists>x y. (x,y) = zsplit0 s" by blast
  1.1080 +  from 5 have "(\<exists>x y. (x,y) = zsplit0 s) \<longrightarrow> (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t \<and> numbound0 xb)" by auto
  1.1081    with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
  1.1082    from abjs 5 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast
  1.1083 -  from th3[simplified] th2[simplified] th[simplified] show ?case 
  1.1084 +  from th3[simplified] th2[simplified] th[simplified] show ?case
  1.1085      by (simp add: distrib_right)
  1.1086  next
  1.1087    case (6 s t n a)
  1.1088 @@ -761,21 +843,24 @@
  1.1089    let ?as = "snd (zsplit0 s)"
  1.1090    let ?nt = "fst (zsplit0 t)"
  1.1091    let ?at = "snd (zsplit0 t)"
  1.1092 -  have abjs: "zsplit0 s = (?ns,?as)" by simp 
  1.1093 -  moreover have abjt:  "zsplit0 t = (?nt,?at)" by simp 
  1.1094 +  have abjs: "zsplit0 s = (?ns,?as)" by simp
  1.1095 +  moreover have abjt:  "zsplit0 t = (?nt,?at)" by simp
  1.1096    ultimately have th: "a=Sub ?as ?at \<and> n=?ns - ?nt" using 6
  1.1097      by (simp add: Let_def split_def)
  1.1098 -  from abjs[symmetric] have bluddy: "\<exists> x y. (x,y) = zsplit0 s" by blast
  1.1099 -  from 6 have "(\<exists> x y. (x,y) = zsplit0 s) \<longrightarrow> (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t \<and> numbound0 xb)" by auto
  1.1100 +  from abjs[symmetric] have bluddy: "\<exists>x y. (x,y) = zsplit0 s" by blast
  1.1101 +  from 6 have "(\<exists>x y. (x,y) = zsplit0 s) \<longrightarrow>
  1.1102 +    (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (x # bs) (CN 0 xa xb) = Inum (x # bs) t \<and> numbound0 xb)"
  1.1103 +    by auto
  1.1104    with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
  1.1105    from abjs 6 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast
  1.1106 -  from th3[simplified] th2[simplified] th[simplified] show ?case 
  1.1107 +  from th3[simplified] th2[simplified] th[simplified] show ?case
  1.1108      by (simp add: left_diff_distrib)
  1.1109  next
  1.1110    case (7 i t n a)
  1.1111    let ?nt = "fst (zsplit0 t)"
  1.1112    let ?at = "snd (zsplit0 t)"
  1.1113 -  have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Mul i ?at \<and> n=i*?nt" using 7
  1.1114 +  have abj: "zsplit0 t = (?nt,?at)" by simp
  1.1115 +  hence th: "a=Mul i ?at \<and> n=i*?nt" using 7
  1.1116      by (simp add: Let_def split_def)
  1.1117    from abj 7 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
  1.1118    hence "?I x (Mul i t) = i * ?I x (CN 0 ?nt ?at)" by simp
  1.1119 @@ -783,59 +868,57 @@
  1.1120    finally show ?case using th th2 by simp
  1.1121  qed
  1.1122  
  1.1123 -consts
  1.1124 -  iszlfm :: "fm \<Rightarrow> bool"   (* Linearity test for fm *)
  1.1125 +consts iszlfm :: "fm \<Rightarrow> bool"  -- {* Linearity test for fm *}
  1.1126  recdef iszlfm "measure size"
  1.1127 -  "iszlfm (And p q) = (iszlfm p \<and> iszlfm q)" 
  1.1128 -  "iszlfm (Or p q) = (iszlfm p \<and> iszlfm q)" 
  1.1129 +  "iszlfm (And p q) = (iszlfm p \<and> iszlfm q)"
  1.1130 +  "iszlfm (Or p q) = (iszlfm p \<and> iszlfm q)"
  1.1131    "iszlfm (Eq  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
  1.1132    "iszlfm (NEq (CN 0 c e)) = (c>0 \<and> numbound0 e)"
  1.1133    "iszlfm (Lt  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
  1.1134    "iszlfm (Le  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
  1.1135    "iszlfm (Gt  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
  1.1136    "iszlfm (Ge  (CN 0 c e)) = ( c>0 \<and> numbound0 e)"
  1.1137 -  "iszlfm (Dvd i (CN 0 c e)) = 
  1.1138 +  "iszlfm (Dvd i (CN 0 c e)) =
  1.1139                   (c>0 \<and> i>0 \<and> numbound0 e)"
  1.1140 -  "iszlfm (NDvd i (CN 0 c e))= 
  1.1141 +  "iszlfm (NDvd i (CN 0 c e))=
  1.1142                   (c>0 \<and> i>0 \<and> numbound0 e)"
  1.1143    "iszlfm p = (isatom p \<and> (bound0 p))"
  1.1144  
  1.1145  lemma zlin_qfree: "iszlfm p \<Longrightarrow> qfree p"
  1.1146    by (induct p rule: iszlfm.induct) auto
  1.1147  
  1.1148 -consts
  1.1149 -  zlfm :: "fm \<Rightarrow> fm"       (* Linearity transformation for fm *)
  1.1150 +consts zlfm :: "fm \<Rightarrow> fm"  -- {* Linearity transformation for fm *}
  1.1151  recdef zlfm "measure fmsize"
  1.1152    "zlfm (And p q) = And (zlfm p) (zlfm q)"
  1.1153    "zlfm (Or p q) = Or (zlfm p) (zlfm q)"
  1.1154    "zlfm (Imp p q) = Or (zlfm (NOT p)) (zlfm q)"
  1.1155    "zlfm (Iff p q) = Or (And (zlfm p) (zlfm q)) (And (zlfm (NOT p)) (zlfm (NOT q)))"
  1.1156 -  "zlfm (Lt a) = (let (c,r) = zsplit0 a in 
  1.1157 -     if c=0 then Lt r else 
  1.1158 +  "zlfm (Lt a) = (let (c,r) = zsplit0 a in
  1.1159 +     if c=0 then Lt r else
  1.1160       if c>0 then (Lt (CN 0 c r)) else (Gt (CN 0 (- c) (Neg r))))"
  1.1161 -  "zlfm (Le a) = (let (c,r) = zsplit0 a in 
  1.1162 -     if c=0 then Le r else 
  1.1163 +  "zlfm (Le a) = (let (c,r) = zsplit0 a in
  1.1164 +     if c=0 then Le r else
  1.1165       if c>0 then (Le (CN 0 c r)) else (Ge (CN 0 (- c) (Neg r))))"
  1.1166 -  "zlfm (Gt a) = (let (c,r) = zsplit0 a in 
  1.1167 -     if c=0 then Gt r else 
  1.1168 +  "zlfm (Gt a) = (let (c,r) = zsplit0 a in
  1.1169 +     if c=0 then Gt r else
  1.1170       if c>0 then (Gt (CN 0 c r)) else (Lt (CN 0 (- c) (Neg r))))"
  1.1171 -  "zlfm (Ge a) = (let (c,r) = zsplit0 a in 
  1.1172 -     if c=0 then Ge r else 
  1.1173 +  "zlfm (Ge a) = (let (c,r) = zsplit0 a in
  1.1174 +     if c=0 then Ge r else
  1.1175       if c>0 then (Ge (CN 0 c r)) else (Le (CN 0 (- c) (Neg r))))"
  1.1176 -  "zlfm (Eq a) = (let (c,r) = zsplit0 a in 
  1.1177 -     if c=0 then Eq r else 
  1.1178 +  "zlfm (Eq a) = (let (c,r) = zsplit0 a in
  1.1179 +     if c=0 then Eq r else
  1.1180       if c>0 then (Eq (CN 0 c r)) else (Eq (CN 0 (- c) (Neg r))))"
  1.1181 -  "zlfm (NEq a) = (let (c,r) = zsplit0 a in 
  1.1182 -     if c=0 then NEq r else 
  1.1183 +  "zlfm (NEq a) = (let (c,r) = zsplit0 a in
  1.1184 +     if c=0 then NEq r else
  1.1185       if c>0 then (NEq (CN 0 c r)) else (NEq (CN 0 (- c) (Neg r))))"
  1.1186 -  "zlfm (Dvd i a) = (if i=0 then zlfm (Eq a) 
  1.1187 -        else (let (c,r) = zsplit0 a in 
  1.1188 -              if c=0 then (Dvd (abs i) r) else 
  1.1189 +  "zlfm (Dvd i a) = (if i=0 then zlfm (Eq a)
  1.1190 +        else (let (c,r) = zsplit0 a in
  1.1191 +              if c=0 then (Dvd (abs i) r) else
  1.1192        if c>0 then (Dvd (abs i) (CN 0 c r))
  1.1193        else (Dvd (abs i) (CN 0 (- c) (Neg r)))))"
  1.1194 -  "zlfm (NDvd i a) = (if i=0 then zlfm (NEq a) 
  1.1195 -        else (let (c,r) = zsplit0 a in 
  1.1196 -              if c=0 then (NDvd (abs i) r) else 
  1.1197 +  "zlfm (NDvd i a) = (if i=0 then zlfm (NEq a)
  1.1198 +        else (let (c,r) = zsplit0 a in
  1.1199 +              if c=0 then (NDvd (abs i) r) else
  1.1200        if c>0 then (NDvd (abs i) (CN 0 c r))
  1.1201        else (NDvd (abs i) (CN 0 (- c) (Neg r)))))"
  1.1202    "zlfm (NOT (And p q)) = Or (zlfm (NOT p)) (zlfm (NOT q))"
  1.1203 @@ -861,154 +944,149 @@
  1.1204    assumes qfp: "qfree p"
  1.1205    shows "(Ifm bbs (i#bs) (zlfm p) = Ifm bbs (i# bs) p) \<and> iszlfm (zlfm p)"
  1.1206    (is "(?I (?l p) = ?I p) \<and> ?L (?l p)")
  1.1207 -using qfp
  1.1208 -proof(induct p rule: zlfm.induct)
  1.1209 -  case (5 a) 
  1.1210 +  using qfp
  1.1211 +proof (induct p rule: zlfm.induct)
  1.1212 +  case (5 a)
  1.1213    let ?c = "fst (zsplit0 a)"
  1.1214    let ?r = "snd (zsplit0 a)"
  1.1215    have spl: "zsplit0 a = (?c,?r)" by simp
  1.1216 -  from zsplit0_I[OF spl, where x="i" and bs="bs"] 
  1.1217 -  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 
  1.1218 -  let ?N = "\<lambda> t. Inum (i#bs) t"
  1.1219 -  from 5 Ia nb  show ?case 
  1.1220 -    apply (auto simp add: Let_def split_def algebra_simps) 
  1.1221 +  from zsplit0_I[OF spl, where x="i" and bs="bs"]
  1.1222 +  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto
  1.1223 +  let ?N = "\<lambda>t. Inum (i#bs) t"
  1.1224 +  from 5 Ia nb  show ?case
  1.1225 +    apply (auto simp add: Let_def split_def algebra_simps)
  1.1226      apply (cases "?r", auto)
  1.1227      apply (case_tac nat, auto)
  1.1228      done
  1.1229  next
  1.1230 -  case (6 a)  
  1.1231 +  case (6 a)
  1.1232    let ?c = "fst (zsplit0 a)"
  1.1233    let ?r = "snd (zsplit0 a)"
  1.1234    have spl: "zsplit0 a = (?c,?r)" by simp
  1.1235 -  from zsplit0_I[OF spl, where x="i" and bs="bs"] 
  1.1236 -  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 
  1.1237 -  let ?N = "\<lambda> t. Inum (i#bs) t"
  1.1238 -  from 6 Ia nb show ?case 
  1.1239 -    apply (auto simp add: Let_def split_def algebra_simps) 
  1.1240 +  from zsplit0_I[OF spl, where x="i" and bs="bs"]
  1.1241 +  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto
  1.1242 +  let ?N = "\<lambda>t. Inum (i#bs) t"
  1.1243 +  from 6 Ia nb show ?case
  1.1244 +    apply (auto simp add: Let_def split_def algebra_simps)
  1.1245      apply (cases "?r", auto)
  1.1246      apply (case_tac nat, auto)
  1.1247      done
  1.1248  next
  1.1249 -  case (7 a)  
  1.1250 +  case (7 a)
  1.1251    let ?c = "fst (zsplit0 a)"
  1.1252    let ?r = "snd (zsplit0 a)"
  1.1253    have spl: "zsplit0 a = (?c,?r)" by simp
  1.1254 -  from zsplit0_I[OF spl, where x="i" and bs="bs"] 
  1.1255 -  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 
  1.1256 -  let ?N = "\<lambda> t. Inum (i#bs) t"
  1.1257 -  from 7 Ia nb show ?case 
  1.1258 -    apply (auto simp add: Let_def split_def algebra_simps) 
  1.1259 +  from zsplit0_I[OF spl, where x="i" and bs="bs"]
  1.1260 +  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto
  1.1261 +  let ?N = "\<lambda>t. Inum (i#bs) t"
  1.1262 +  from 7 Ia nb show ?case
  1.1263 +    apply (auto simp add: Let_def split_def algebra_simps)
  1.1264      apply (cases "?r", auto)
  1.1265      apply (case_tac nat, auto)
  1.1266      done
  1.1267  next
  1.1268 -  case (8 a)  
  1.1269 +  case (8 a)
  1.1270    let ?c = "fst (zsplit0 a)"
  1.1271    let ?r = "snd (zsplit0 a)"
  1.1272    have spl: "zsplit0 a = (?c,?r)" by simp
  1.1273 -  from zsplit0_I[OF spl, where x="i" and bs="bs"] 
  1.1274 -  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 
  1.1275 -  let ?N = "\<lambda> t. Inum (i#bs) t"
  1.1276 +  from zsplit0_I[OF spl, where x="i" and bs="bs"]
  1.1277 +  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto
  1.1278 +  let ?N = "\<lambda>t. Inum (i#bs) t"
  1.1279    from 8 Ia nb  show ?case
  1.1280 -    apply (auto simp add: Let_def split_def algebra_simps) 
  1.1281 +    apply (auto simp add: Let_def split_def algebra_simps)
  1.1282      apply (cases "?r", auto)
  1.1283      apply (case_tac nat, auto)
  1.1284      done
  1.1285  next
  1.1286 -  case (9 a)  
  1.1287 +  case (9 a)
  1.1288    let ?c = "fst (zsplit0 a)"
  1.1289    let ?r = "snd (zsplit0 a)"
  1.1290    have spl: "zsplit0 a = (?c,?r)" by simp
  1.1291 -  from zsplit0_I[OF spl, where x="i" and bs="bs"] 
  1.1292 -  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 
  1.1293 -  let ?N = "\<lambda> t. Inum (i#bs) t"
  1.1294 +  from zsplit0_I[OF spl, where x="i" and bs="bs"]
  1.1295 +  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto
  1.1296 +  let ?N = "\<lambda>t. Inum (i#bs) t"
  1.1297    from 9 Ia nb  show ?case
  1.1298 -    apply (auto simp add: Let_def split_def algebra_simps) 
  1.1299 +    apply (auto simp add: Let_def split_def algebra_simps)
  1.1300      apply (cases "?r", auto)
  1.1301      apply (case_tac nat, auto)
  1.1302      done
  1.1303  next
  1.1304 -  case (10 a)  
  1.1305 +  case (10 a)
  1.1306    let ?c = "fst (zsplit0 a)"
  1.1307    let ?r = "snd (zsplit0 a)"
  1.1308    have spl: "zsplit0 a = (?c,?r)" by simp
  1.1309 -  from zsplit0_I[OF spl, where x="i" and bs="bs"] 
  1.1310 -  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 
  1.1311 -  let ?N = "\<lambda> t. Inum (i#bs) t"
  1.1312 +  from zsplit0_I[OF spl, where x="i" and bs="bs"]
  1.1313 +  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto
  1.1314 +  let ?N = "\<lambda>t. Inum (i#bs) t"
  1.1315    from 10 Ia nb  show ?case
  1.1316 -    apply (auto simp add: Let_def split_def algebra_simps) 
  1.1317 +    apply (auto simp add: Let_def split_def algebra_simps)
  1.1318      apply (cases "?r",auto)
  1.1319      apply (case_tac nat, auto)
  1.1320      done
  1.1321  next
  1.1322 -  case (11 j a)  
  1.1323 +  case (11 j a)
  1.1324    let ?c = "fst (zsplit0 a)"
  1.1325    let ?r = "snd (zsplit0 a)"
  1.1326    have spl: "zsplit0 a = (?c,?r)" by simp
  1.1327 -  from zsplit0_I[OF spl, where x="i" and bs="bs"] 
  1.1328 -  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 
  1.1329 -  let ?N = "\<lambda> t. Inum (i#bs) t"
  1.1330 +  from zsplit0_I[OF spl, where x="i" and bs="bs"]
  1.1331 +  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto
  1.1332 +  let ?N = "\<lambda>t. Inum (i#bs) t"
  1.1333    have "j=0 \<or> (j\<noteq>0 \<and> ?c = 0) \<or> (j\<noteq>0 \<and> ?c >0) \<or> (j\<noteq> 0 \<and> ?c<0)" by arith
  1.1334    moreover
  1.1335 -  {assume "j=0" hence z: "zlfm (Dvd j a) = (zlfm (Eq a))" by (simp add: Let_def) 
  1.1336 +  {assume "j=0" hence z: "zlfm (Dvd j a) = (zlfm (Eq a))" by (simp add: Let_def)
  1.1337      hence ?case using 11 `j = 0` by (simp del: zlfm.simps) }
  1.1338    moreover
  1.1339 -  {assume "?c=0" and "j\<noteq>0" hence ?case 
  1.1340 +  {assume "?c=0" and "j\<noteq>0" hence ?case
  1.1341        using zsplit0_I[OF spl, where x="i" and bs="bs"]
  1.1342 -    apply (auto simp add: Let_def split_def algebra_simps) 
  1.1343 +    apply (auto simp add: Let_def split_def algebra_simps)
  1.1344      apply (cases "?r",auto)
  1.1345      apply (case_tac nat, auto)
  1.1346      done}
  1.1347    moreover
  1.1348 -  {assume cp: "?c > 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))" 
  1.1349 +  {assume cp: "?c > 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))"
  1.1350        by (simp add: nb Let_def split_def)
  1.1351      hence ?case using Ia cp jnz by (simp add: Let_def split_def)}
  1.1352    moreover
  1.1353 -  {assume cn: "?c < 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))" 
  1.1354 +  {assume cn: "?c < 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))"
  1.1355        by (simp add: nb Let_def split_def)
  1.1356      hence ?case using Ia cn jnz dvd_minus_iff[of "abs j" "?c*i + ?N ?r" ]
  1.1357        by (simp add: Let_def split_def) }
  1.1358    ultimately show ?case by blast
  1.1359  next
  1.1360 -  case (12 j a) 
  1.1361 +  case (12 j a)
  1.1362    let ?c = "fst (zsplit0 a)"
  1.1363    let ?r = "snd (zsplit0 a)"
  1.1364    have spl: "zsplit0 a = (?c,?r)" by simp
  1.1365 -  from zsplit0_I[OF spl, where x="i" and bs="bs"] 
  1.1366 -  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 
  1.1367 -  let ?N = "\<lambda> t. Inum (i#bs) t"
  1.1368 +  from zsplit0_I[OF spl, where x="i" and bs="bs"]
  1.1369 +  have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto
  1.1370 +  let ?N = "\<lambda>t. Inum (i#bs) t"
  1.1371    have "j=0 \<or> (j\<noteq>0 \<and> ?c = 0) \<or> (j\<noteq>0 \<and> ?c >0) \<or> (j\<noteq> 0 \<and> ?c<0)" by arith
  1.1372    moreover
  1.1373 -  {assume "j=0" hence z: "zlfm (NDvd j a) = (zlfm (NEq a))" by (simp add: Let_def) 
  1.1374 +  {assume "j=0" hence z: "zlfm (NDvd j a) = (zlfm (NEq a))" by (simp add: Let_def)
  1.1375      hence ?case using assms 12 `j = 0` by (simp del: zlfm.simps)}
  1.1376    moreover
  1.1377 -  {assume "?c=0" and "j\<noteq>0" hence ?case 
  1.1378 +  {assume "?c=0" and "j\<noteq>0" hence ?case
  1.1379        using zsplit0_I[OF spl, where x="i" and bs="bs"]
  1.1380 -    apply (auto simp add: Let_def split_def algebra_simps) 
  1.1381 +    apply (auto simp add: Let_def split_def algebra_simps)
  1.1382      apply (cases "?r",auto)
  1.1383      apply (case_tac nat, auto)
  1.1384      done}
  1.1385    moreover
  1.1386 -  {assume cp: "?c > 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))" 
  1.1387 +  {assume cp: "?c > 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))"
  1.1388        by (simp add: nb Let_def split_def)
  1.1389      hence ?case using Ia cp jnz by (simp add: Let_def split_def) }
  1.1390    moreover
  1.1391 -  {assume cn: "?c < 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))" 
  1.1392 +  {assume cn: "?c < 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))"
  1.1393        by (simp add: nb Let_def split_def)
  1.1394      hence ?case using Ia cn jnz dvd_minus_iff[of "abs j" "?c*i + ?N ?r"]
  1.1395        by (simp add: Let_def split_def)}
  1.1396    ultimately show ?case by blast
  1.1397  qed auto
  1.1398  
  1.1399 -consts 
  1.1400 -  plusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of +\<infinity>*)
  1.1401 -  minusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of -\<infinity>*)
  1.1402 -  \<delta> :: "fm \<Rightarrow> int" (* Compute lcm {d| N\<^isup>? Dvd c*x+t \<in> p}*)
  1.1403 -  d_\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool" (* checks if a given l divides all the ds above*)
  1.1404 -
  1.1405 +consts minusinf :: "fm \<Rightarrow> fm" -- {* Virtual substitution of @{text "-\<infinity>"} *}
  1.1406  recdef minusinf "measure size"
  1.1407 -  "minusinf (And p q) = And (minusinf p) (minusinf q)" 
  1.1408 -  "minusinf (Or p q) = Or (minusinf p) (minusinf q)" 
  1.1409 +  "minusinf (And p q) = And (minusinf p) (minusinf q)"
  1.1410 +  "minusinf (Or p q) = Or (minusinf p) (minusinf q)"
  1.1411    "minusinf (Eq  (CN 0 c e)) = F"
  1.1412    "minusinf (NEq (CN 0 c e)) = T"
  1.1413    "minusinf (Lt  (CN 0 c e)) = T"
  1.1414 @@ -1018,11 +1096,12 @@
  1.1415    "minusinf p = p"
  1.1416  
  1.1417  lemma minusinf_qfree: "qfree p \<Longrightarrow> qfree (minusinf p)"
  1.1418 -  by (induct p rule: minusinf.induct, auto)
  1.1419 +  by (induct p rule: minusinf.induct) auto
  1.1420  
  1.1421 +consts plusinf :: "fm \<Rightarrow> fm"  -- {* Virtual substitution of @{text "+\<infinity>"} *}
  1.1422  recdef plusinf "measure size"
  1.1423 -  "plusinf (And p q) = And (plusinf p) (plusinf q)" 
  1.1424 -  "plusinf (Or p q) = Or (plusinf p) (plusinf q)" 
  1.1425 +  "plusinf (And p q) = And (plusinf p) (plusinf q)"
  1.1426 +  "plusinf (Or p q) = Or (plusinf p) (plusinf q)"
  1.1427    "plusinf (Eq  (CN 0 c e)) = F"
  1.1428    "plusinf (NEq (CN 0 c e)) = T"
  1.1429    "plusinf (Lt  (CN 0 c e)) = F"
  1.1430 @@ -1031,27 +1110,29 @@
  1.1431    "plusinf (Ge  (CN 0 c e)) = T"
  1.1432    "plusinf p = p"
  1.1433  
  1.1434 +consts \<delta> :: "fm \<Rightarrow> int"  -- {* Compute @{text "lcm {d| N\<^isup>? Dvd c*x+t \<in> p}"} *}
  1.1435  recdef \<delta> "measure size"
  1.1436 -  "\<delta> (And p q) = lcm (\<delta> p) (\<delta> q)" 
  1.1437 -  "\<delta> (Or p q) = lcm (\<delta> p) (\<delta> q)" 
  1.1438 +  "\<delta> (And p q) = lcm (\<delta> p) (\<delta> q)"
  1.1439 +  "\<delta> (Or p q) = lcm (\<delta> p) (\<delta> q)"
  1.1440    "\<delta> (Dvd i (CN 0 c e)) = i"
  1.1441    "\<delta> (NDvd i (CN 0 c e)) = i"
  1.1442    "\<delta> p = 1"
  1.1443  
  1.1444 +consts d_\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool"  -- {* check if a given l divides all the ds above *}
  1.1445  recdef d_\<delta> "measure size"
  1.1446 -  "d_\<delta> (And p q) = (\<lambda> d. d_\<delta> p d \<and> d_\<delta> q d)" 
  1.1447 -  "d_\<delta> (Or p q) = (\<lambda> d. d_\<delta> p d \<and> d_\<delta> q d)" 
  1.1448 -  "d_\<delta> (Dvd i (CN 0 c e)) = (\<lambda> d. i dvd d)"
  1.1449 -  "d_\<delta> (NDvd i (CN 0 c e)) = (\<lambda> d. i dvd d)"
  1.1450 -  "d_\<delta> p = (\<lambda> d. True)"
  1.1451 +  "d_\<delta> (And p q) = (\<lambda>d. d_\<delta> p d \<and> d_\<delta> q d)"
  1.1452 +  "d_\<delta> (Or p q) = (\<lambda>d. d_\<delta> p d \<and> d_\<delta> q d)"
  1.1453 +  "d_\<delta> (Dvd i (CN 0 c e)) = (\<lambda>d. i dvd d)"
  1.1454 +  "d_\<delta> (NDvd i (CN 0 c e)) = (\<lambda>d. i dvd d)"
  1.1455 +  "d_\<delta> p = (\<lambda>d. True)"
  1.1456  
  1.1457 -lemma delta_mono: 
  1.1458 +lemma delta_mono:
  1.1459    assumes lin: "iszlfm p"
  1.1460 -  and d: "d dvd d'"
  1.1461 -  and ad: "d_\<delta> p d"
  1.1462 +    and d: "d dvd d'"
  1.1463 +    and ad: "d_\<delta> p d"
  1.1464    shows "d_\<delta> p d'"
  1.1465    using lin ad d
  1.1466 -proof(induct p rule: iszlfm.induct)
  1.1467 +proof (induct p rule: iszlfm.induct)
  1.1468    case (9 i c e)  thus ?case using d
  1.1469      by (simp add: dvd_trans[of "i" "d" "d'"])
  1.1470  next
  1.1471 @@ -1059,11 +1140,12 @@
  1.1472      by (simp add: dvd_trans[of "i" "d" "d'"])
  1.1473  qed simp_all
  1.1474  
  1.1475 -lemma \<delta> : assumes lin:"iszlfm p"
  1.1476 +lemma \<delta>:
  1.1477 +  assumes lin:"iszlfm p"
  1.1478    shows "d_\<delta> p (\<delta> p) \<and> \<delta> p >0"
  1.1479 -using lin
  1.1480 +  using lin
  1.1481  proof (induct p rule: iszlfm.induct)
  1.1482 -  case (1 p q) 
  1.1483 +  case (1 p q)
  1.1484    let ?d = "\<delta> (And p q)"
  1.1485    from 1 lcm_pos_int have dp: "?d >0" by simp
  1.1486    have d1: "\<delta> p dvd \<delta> (And p q)" using 1 by simp
  1.1487 @@ -1072,7 +1154,7 @@
  1.1488    hence th': "d_\<delta> q ?d" using delta_mono 1 by(simp only: iszlfm.simps)
  1.1489    from th th' dp show ?case by simp
  1.1490  next
  1.1491 -  case (2 p q)  
  1.1492 +  case (2 p q)
  1.1493    let ?d = "\<delta> (And p q)"
  1.1494    from 2 lcm_pos_int have dp: "?d >0" by simp
  1.1495    have "\<delta> p dvd \<delta> (And p q)" using 2 by simp
  1.1496 @@ -1083,42 +1165,38 @@
  1.1497  qed simp_all
  1.1498  
  1.1499  
  1.1500 -consts 
  1.1501 -  a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" (* adjusts the coeffitients of a formula *)
  1.1502 -  d_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool" (* tests if all coeffs c of c divide a given l*)
  1.1503 -  \<zeta>  :: "fm \<Rightarrow> int" (* computes the lcm of all coefficients of x*)
  1.1504 -  \<beta> :: "fm \<Rightarrow> num list"
  1.1505 -  \<alpha> :: "fm \<Rightarrow> num list"
  1.1506 -
  1.1507 +consts a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm"  -- {* adjust the coeffitients of a formula *}
  1.1508  recdef a_\<beta> "measure size"
  1.1509 -  "a_\<beta> (And p q) = (\<lambda> k. And (a_\<beta> p k) (a_\<beta> q k))" 
  1.1510 -  "a_\<beta> (Or p q) = (\<lambda> k. Or (a_\<beta> p k) (a_\<beta> q k))" 
  1.1511 -  "a_\<beta> (Eq  (CN 0 c e)) = (\<lambda> k. Eq (CN 0 1 (Mul (k div c) e)))"
  1.1512 -  "a_\<beta> (NEq (CN 0 c e)) = (\<lambda> k. NEq (CN 0 1 (Mul (k div c) e)))"
  1.1513 -  "a_\<beta> (Lt  (CN 0 c e)) = (\<lambda> k. Lt (CN 0 1 (Mul (k div c) e)))"
  1.1514 -  "a_\<beta> (Le  (CN 0 c e)) = (\<lambda> k. Le (CN 0 1 (Mul (k div c) e)))"
  1.1515 -  "a_\<beta> (Gt  (CN 0 c e)) = (\<lambda> k. Gt (CN 0 1 (Mul (k div c) e)))"
  1.1516 -  "a_\<beta> (Ge  (CN 0 c e)) = (\<lambda> k. Ge (CN 0 1 (Mul (k div c) e)))"
  1.1517 -  "a_\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
  1.1518 -  "a_\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
  1.1519 -  "a_\<beta> p = (\<lambda> k. p)"
  1.1520 +  "a_\<beta> (And p q) = (\<lambda>k. And (a_\<beta> p k) (a_\<beta> q k))"
  1.1521 +  "a_\<beta> (Or p q) = (\<lambda>k. Or (a_\<beta> p k) (a_\<beta> q k))"
  1.1522 +  "a_\<beta> (Eq  (CN 0 c e)) = (\<lambda>k. Eq (CN 0 1 (Mul (k div c) e)))"
  1.1523 +  "a_\<beta> (NEq (CN 0 c e)) = (\<lambda>k. NEq (CN 0 1 (Mul (k div c) e)))"
  1.1524 +  "a_\<beta> (Lt  (CN 0 c e)) = (\<lambda>k. Lt (CN 0 1 (Mul (k div c) e)))"
  1.1525 +  "a_\<beta> (Le  (CN 0 c e)) = (\<lambda>k. Le (CN 0 1 (Mul (k div c) e)))"
  1.1526 +  "a_\<beta> (Gt  (CN 0 c e)) = (\<lambda>k. Gt (CN 0 1 (Mul (k div c) e)))"
  1.1527 +  "a_\<beta> (Ge  (CN 0 c e)) = (\<lambda>k. Ge (CN 0 1 (Mul (k div c) e)))"
  1.1528 +  "a_\<beta> (Dvd i (CN 0 c e)) =(\<lambda>k. Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
  1.1529 +  "a_\<beta> (NDvd i (CN 0 c e))=(\<lambda>k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
  1.1530 +  "a_\<beta> p = (\<lambda>k. p)"
  1.1531  
  1.1532 +consts d_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool"  -- {* test if all coeffs c of c divide a given l *}
  1.1533  recdef d_\<beta> "measure size"
  1.1534 -  "d_\<beta> (And p q) = (\<lambda> k. (d_\<beta> p k) \<and> (d_\<beta> q k))" 
  1.1535 -  "d_\<beta> (Or p q) = (\<lambda> k. (d_\<beta> p k) \<and> (d_\<beta> q k))" 
  1.1536 -  "d_\<beta> (Eq  (CN 0 c e)) = (\<lambda> k. c dvd k)"
  1.1537 -  "d_\<beta> (NEq (CN 0 c e)) = (\<lambda> k. c dvd k)"
  1.1538 -  "d_\<beta> (Lt  (CN 0 c e)) = (\<lambda> k. c dvd k)"
  1.1539 -  "d_\<beta> (Le  (CN 0 c e)) = (\<lambda> k. c dvd k)"
  1.1540 -  "d_\<beta> (Gt  (CN 0 c e)) = (\<lambda> k. c dvd k)"
  1.1541 -  "d_\<beta> (Ge  (CN 0 c e)) = (\<lambda> k. c dvd k)"
  1.1542 -  "d_\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. c dvd k)"
  1.1543 -  "d_\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. c dvd k)"
  1.1544 -  "d_\<beta> p = (\<lambda> k. True)"
  1.1545 +  "d_\<beta> (And p q) = (\<lambda>k. (d_\<beta> p k) \<and> (d_\<beta> q k))"
  1.1546 +  "d_\<beta> (Or p q) = (\<lambda>k. (d_\<beta> p k) \<and> (d_\<beta> q k))"
  1.1547 +  "d_\<beta> (Eq  (CN 0 c e)) = (\<lambda>k. c dvd k)"
  1.1548 +  "d_\<beta> (NEq (CN 0 c e)) = (\<lambda>k. c dvd k)"
  1.1549 +  "d_\<beta> (Lt  (CN 0 c e)) = (\<lambda>k. c dvd k)"
  1.1550 +  "d_\<beta> (Le  (CN 0 c e)) = (\<lambda>k. c dvd k)"
  1.1551 +  "d_\<beta> (Gt  (CN 0 c e)) = (\<lambda>k. c dvd k)"
  1.1552 +  "d_\<beta> (Ge  (CN 0 c e)) = (\<lambda>k. c dvd k)"
  1.1553 +  "d_\<beta> (Dvd i (CN 0 c e)) =(\<lambda>k. c dvd k)"
  1.1554 +  "d_\<beta> (NDvd i (CN 0 c e))=(\<lambda>k. c dvd k)"
  1.1555 +  "d_\<beta> p = (\<lambda>k. True)"
  1.1556  
  1.1557 +consts \<zeta> :: "fm \<Rightarrow> int"  -- {* computes the lcm of all coefficients of x *}
  1.1558  recdef \<zeta> "measure size"
  1.1559 -  "\<zeta> (And p q) = lcm (\<zeta> p) (\<zeta> q)" 
  1.1560 -  "\<zeta> (Or p q) = lcm (\<zeta> p) (\<zeta> q)" 
  1.1561 +  "\<zeta> (And p q) = lcm (\<zeta> p) (\<zeta> q)"
  1.1562 +  "\<zeta> (Or p q) = lcm (\<zeta> p) (\<zeta> q)"
  1.1563    "\<zeta> (Eq  (CN 0 c e)) = c"
  1.1564    "\<zeta> (NEq (CN 0 c e)) = c"
  1.1565    "\<zeta> (Lt  (CN 0 c e)) = c"
  1.1566 @@ -1129,9 +1207,10 @@
  1.1567    "\<zeta> (NDvd i (CN 0 c e))= c"
  1.1568    "\<zeta> p = 1"
  1.1569  
  1.1570 +consts \<beta> :: "fm \<Rightarrow> num list"
  1.1571  recdef \<beta> "measure size"
  1.1572 -  "\<beta> (And p q) = (\<beta> p @ \<beta> q)" 
  1.1573 -  "\<beta> (Or p q) = (\<beta> p @ \<beta> q)" 
  1.1574 +  "\<beta> (And p q) = (\<beta> p @ \<beta> q)"
  1.1575 +  "\<beta> (Or p q) = (\<beta> p @ \<beta> q)"
  1.1576    "\<beta> (Eq  (CN 0 c e)) = [Sub (C -1) e]"
  1.1577    "\<beta> (NEq (CN 0 c e)) = [Neg e]"
  1.1578    "\<beta> (Lt  (CN 0 c e)) = []"
  1.1579 @@ -1140,9 +1219,10 @@
  1.1580    "\<beta> (Ge  (CN 0 c e)) = [Sub (C -1) e]"
  1.1581    "\<beta> p = []"
  1.1582  
  1.1583 +consts \<alpha> :: "fm \<Rightarrow> num list"
  1.1584  recdef \<alpha> "measure size"
  1.1585 -  "\<alpha> (And p q) = (\<alpha> p @ \<alpha> q)" 
  1.1586 -  "\<alpha> (Or p q) = (\<alpha> p @ \<alpha> q)" 
  1.1587 +  "\<alpha> (And p q) = (\<alpha> p @ \<alpha> q)"
  1.1588 +  "\<alpha> (Or p q) = (\<alpha> p @ \<alpha> q)"
  1.1589    "\<alpha> (Eq  (CN 0 c e)) = [Add (C -1) e]"
  1.1590    "\<alpha> (NEq (CN 0 c e)) = [e]"
  1.1591    "\<alpha> (Lt  (CN 0 c e)) = [e]"
  1.1592 @@ -1150,10 +1230,11 @@
  1.1593    "\<alpha> (Gt  (CN 0 c e)) = []"
  1.1594    "\<alpha> (Ge  (CN 0 c e)) = []"
  1.1595    "\<alpha> p = []"
  1.1596 +
  1.1597  consts mirror :: "fm \<Rightarrow> fm"
  1.1598  recdef mirror "measure size"
  1.1599 -  "mirror (And p q) = And (mirror p) (mirror q)" 
  1.1600 -  "mirror (Or p q) = Or (mirror p) (mirror q)" 
  1.1601 +  "mirror (And p q) = And (mirror p) (mirror q)"
  1.1602 +  "mirror (Or p q) = Or (mirror p) (mirror q)"
  1.1603    "mirror (Eq  (CN 0 c e)) = Eq (CN 0 c (Neg e))"
  1.1604    "mirror (NEq (CN 0 c e)) = NEq (CN 0 c (Neg e))"
  1.1605    "mirror (Lt  (CN 0 c e)) = Gt (CN 0 c (Neg e))"
  1.1606 @@ -1163,26 +1244,28 @@
  1.1607    "mirror (Dvd i (CN 0 c e)) = Dvd i (CN 0 c (Neg e))"
  1.1608    "mirror (NDvd i (CN 0 c e)) = NDvd i (CN 0 c (Neg e))"
  1.1609    "mirror p = p"
  1.1610 -    (* Lemmas for the correctness of \<sigma>\<rho> *)
  1.1611 +
  1.1612 +text {* Lemmas for the correctness of @{text "\<sigma>_\<rho>"} *}
  1.1613 +
  1.1614  lemma dvd1_eq1: "x >0 \<Longrightarrow> (x::int) dvd 1 = (x = 1)"
  1.1615    by simp
  1.1616  
  1.1617  lemma minusinf_inf:
  1.1618    assumes linp: "iszlfm p"
  1.1619 -  and u: "d_\<beta> p 1"
  1.1620 -  shows "\<exists> (z::int). \<forall> x < z. Ifm bbs (x#bs) (minusinf p) = Ifm bbs (x#bs) p"
  1.1621 -  (is "?P p" is "\<exists> (z::int). \<forall> x < z. ?I x (?M p) = ?I x p")
  1.1622 -using linp u
  1.1623 +    and u: "d_\<beta> p 1"
  1.1624 +  shows "\<exists>(z::int). \<forall>x < z. Ifm bbs (x#bs) (minusinf p) = Ifm bbs (x#bs) p"
  1.1625 +  (is "?P p" is "\<exists>(z::int). \<forall>x < z. ?I x (?M p) = ?I x p")
  1.1626 +  using linp u
  1.1627  proof (induct p rule: minusinf.induct)
  1.1628 -  case (1 p q) thus ?case 
  1.1629 +  case (1 p q) thus ?case
  1.1630      by auto (rule_tac x="min z za" in exI,simp)
  1.1631  next
  1.1632 -  case (2 p q) thus ?case 
  1.1633 +  case (2 p q) thus ?case
  1.1634      by auto (rule_tac x="min z za" in exI,simp)
  1.1635  next
  1.1636 -  case (3 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
  1.1637 +  case (3 c e) hence c1: "c=1" and nb: "numbound0 e" by simp_all
  1.1638    fix a
  1.1639 -  from 3 have "\<forall> x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<noteq> 0"
  1.1640 +  from 3 have "\<forall>x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<noteq> 0"
  1.1641    proof(clarsimp)
  1.1642      fix x assume "x < (- Inum (a#bs) e)" and"x + Inum (x#bs) e = 0"
  1.1643      with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
  1.1644 @@ -1190,9 +1273,9 @@
  1.1645    qed
  1.1646    thus ?case by auto
  1.1647  next
  1.1648 -  case (4 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
  1.1649 +  case (4 c e) hence c1: "c=1" and nb: "numbound0 e" by simp_all
  1.1650    fix a
  1.1651 -  from 4 have "\<forall> x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<noteq> 0"
  1.1652 +  from 4 have "\<forall>x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<noteq> 0"
  1.1653    proof(clarsimp)
  1.1654      fix x assume "x < (- Inum (a#bs) e)" and"x + Inum (x#bs) e = 0"
  1.1655      with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
  1.1656 @@ -1200,29 +1283,29 @@
  1.1657    qed
  1.1658    thus ?case by auto
  1.1659  next
  1.1660 -  case (5 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
  1.1661 +  case (5 c e) hence c1: "c=1" and nb: "numbound0 e" by simp_all
  1.1662    fix a
  1.1663 -  from 5 have "\<forall> x<(- Inum (a#bs) e). c*x + Inum (x#bs) e < 0"
  1.1664 +  from 5 have "\<forall>x<(- Inum (a#bs) e). c*x + Inum (x#bs) e < 0"
  1.1665    proof(clarsimp)
  1.1666 -    fix x assume "x < (- Inum (a#bs) e)" 
  1.1667 +    fix x assume "x < (- Inum (a#bs) e)"
  1.1668      with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
  1.1669      show "x + Inum (x#bs) e < 0" by simp
  1.1670    qed
  1.1671    thus ?case by auto
  1.1672  next
  1.1673 -  case (6 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
  1.1674 +  case (6 c e) hence c1: "c=1" and nb: "numbound0 e" by simp_all
  1.1675    fix a
  1.1676 -  from 6 have "\<forall> x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<le> 0"
  1.1677 +  from 6 have "\<forall>x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<le> 0"
  1.1678    proof(clarsimp)
  1.1679 -    fix x assume "x < (- Inum (a#bs) e)" 
  1.1680 +    fix x assume "x < (- Inum (a#bs) e)"
  1.1681      with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
  1.1682      show "x + Inum (x#bs) e \<le> 0" by simp
  1.1683    qed
  1.1684    thus ?case by auto
  1.1685  next
  1.1686 -  case (7 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
  1.1687 +  case (7 c e) hence c1: "c=1" and nb: "numbound0 e" by simp_all
  1.1688    fix a
  1.1689 -  from 7 have "\<forall> x<(- Inum (a#bs) e). \<not> (c*x + Inum (x#bs) e > 0)"
  1.1690 +  from 7 have "\<forall>x<(- Inum (a#bs) e). \<not> (c*x + Inum (x#bs) e > 0)"
  1.1691    proof(clarsimp)
  1.1692      fix x assume "x < (- Inum (a#bs) e)" and"x + Inum (x#bs) e > 0"
  1.1693      with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
  1.1694 @@ -1230,9 +1313,9 @@
  1.1695    qed
  1.1696    thus ?case by auto
  1.1697  next
  1.1698 -  case (8 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
  1.1699 +  case (8 c e) hence c1: "c=1" and nb: "numbound0 e" by simp_all
  1.1700    fix a
  1.1701 -  from 8 have "\<forall> x<(- Inum (a#bs) e). \<not> (c*x + Inum (x#bs) e \<ge> 0)"
  1.1702 +  from 8 have "\<forall>x<(- Inum (a#bs) e). \<not> (c*x + Inum (x#bs) e \<ge> 0)"
  1.1703    proof(clarsimp)
  1.1704      fix x assume "x < (- Inum (a#bs) e)" and"x + Inum (x#bs) e \<ge> 0"
  1.1705      with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
  1.1706 @@ -1244,300 +1327,327 @@
  1.1707  lemma minusinf_repeats:
  1.1708    assumes d: "d_\<delta> p d" and linp: "iszlfm p"
  1.1709    shows "Ifm bbs ((x - k*d)#bs) (minusinf p) = Ifm bbs (x #bs) (minusinf p)"
  1.1710 -using linp d
  1.1711 -proof(induct p rule: iszlfm.induct) 
  1.1712 -  case (9 i c e) hence nbe: "numbound0 e"  and id: "i dvd d" by simp+
  1.1713 -    hence "\<exists> k. d=i*k" by (simp add: dvd_def)
  1.1714 -    then obtain "di" where di_def: "d=i*di" by blast
  1.1715 -    show ?case 
  1.1716 -    proof(simp add: numbound0_I[OF nbe,where bs="bs" and b="x - k * d" and b'="x"] right_diff_distrib, rule iffI)
  1.1717 -      assume 
  1.1718 -        "i dvd c * x - c*(k*d) + Inum (x # bs) e"
  1.1719 +  using linp d
  1.1720 +proof (induct p rule: iszlfm.induct)
  1.1721 +  case (9 i c e)
  1.1722 +  hence nbe: "numbound0 e" and id: "i dvd d" by simp_all
  1.1723 +  hence "\<exists>k. d=i*k" by (simp add: dvd_def)
  1.1724 +  then obtain "di" where di_def: "d=i*di" by blast
  1.1725 +  show ?case
  1.1726 +  proof (simp add: numbound0_I[OF nbe,where bs="bs" and b="x - k * d" and b'="x"] right_diff_distrib,
  1.1727 +      rule iffI)
  1.1728 +    assume "i dvd c * x - c*(k*d) + Inum (x # bs) e"
  1.1729        (is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt")
  1.1730 -      hence "\<exists> (l::int). ?rt = i * l" by (simp add: dvd_def)
  1.1731 -      hence "\<exists> (l::int). c*x+ ?I x e = i*l+c*(k * i*di)" 
  1.1732 -        by (simp add: algebra_simps di_def)
  1.1733 -      hence "\<exists> (l::int). c*x+ ?I x e = i*(l + c*k*di)"
  1.1734 -        by (simp add: algebra_simps)
  1.1735 -      hence "\<exists> (l::int). c*x+ ?I x e = i*l" by blast
  1.1736 -      thus "i dvd c*x + Inum (x # bs) e" by (simp add: dvd_def) 
  1.1737 -    next
  1.1738 -      assume 
  1.1739 -        "i dvd c*x + Inum (x # bs) e" (is "?ri dvd ?rc*?rx+?e")
  1.1740 -      hence "\<exists> (l::int). c*x+?e = i*l" by (simp add: dvd_def)
  1.1741 -      hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*l - c*(k*d)" by simp
  1.1742 -      hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*l - c*(k*i*di)" by (simp add: di_def)
  1.1743 -      hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: algebra_simps)
  1.1744 -      hence "\<exists> (l::int). c*x - c * (k*d) +?e = i*l"
  1.1745 -        by blast
  1.1746 -      thus "i dvd c*x - c*(k*d) + Inum (x # bs) e" by (simp add: dvd_def)
  1.1747 -    qed
  1.1748 +    hence "\<exists>(l::int). ?rt = i * l" by (simp add: dvd_def)
  1.1749 +    hence "\<exists>(l::int). c*x+ ?I x e = i*l+c*(k * i*di)"
  1.1750 +      by (simp add: algebra_simps di_def)
  1.1751 +    hence "\<exists>(l::int). c*x+ ?I x e = i*(l + c*k*di)"
  1.1752 +      by (simp add: algebra_simps)
  1.1753 +    hence "\<exists>(l::int). c*x+ ?I x e = i*l" by blast
  1.1754 +    thus "i dvd c*x + Inum (x # bs) e" by (simp add: dvd_def)
  1.1755 +  next
  1.1756 +    assume "i dvd c*x + Inum (x # bs) e" (is "?ri dvd ?rc*?rx+?e")
  1.1757 +    hence "\<exists>(l::int). c*x+?e = i*l" by (simp add: dvd_def)
  1.1758 +    hence "\<exists>(l::int). c*x - c*(k*d) +?e = i*l - c*(k*d)" by simp
  1.1759 +    hence "\<exists>(l::int). c*x - c*(k*d) +?e = i*l - c*(k*i*di)" by (simp add: di_def)
  1.1760 +    hence "\<exists>(l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: algebra_simps)
  1.1761 +    hence "\<exists>(l::int). c*x - c * (k*d) +?e = i*l" by blast
  1.1762 +    thus "i dvd c*x - c*(k*d) + Inum (x # bs) e" by (simp add: dvd_def)
  1.1763 +  qed
  1.1764  next
  1.1765 -  case (10 i c e)  hence nbe: "numbound0 e"  and id: "i dvd d" by simp+
  1.1766 -    hence "\<exists> k. d=i*k" by (simp add: dvd_def)
  1.1767 -    then obtain "di" where di_def: "d=i*di" by blast
  1.1768 -    show ?case 
  1.1769 -    proof(simp add: numbound0_I[OF nbe,where bs="bs" and b="x - k * d" and b'="x"] right_diff_distrib, rule iffI)
  1.1770 -      assume 
  1.1771 -        "i dvd c * x - c*(k*d) + Inum (x # bs) e"
  1.1772 +  case (10 i c e)
  1.1773 +  hence nbe: "numbound0 e"  and id: "i dvd d" by simp_all
  1.1774 +  hence "\<exists>k. d=i*k" by (simp add: dvd_def)
  1.1775 +  then obtain "di" where di_def: "d=i*di" by blast
  1.1776 +  show ?case
  1.1777 +  proof(simp add: numbound0_I[OF nbe,where bs="bs" and b="x - k * d" and b'="x"] right_diff_distrib, rule iffI)
  1.1778 +    assume "i dvd c * x - c*(k*d) + Inum (x # bs) e"
  1.1779        (is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt")
  1.1780 -      hence "\<exists> (l::int). ?rt = i * l" by (simp add: dvd_def)
  1.1781 -      hence "\<exists> (l::int). c*x+ ?I x e = i*l+c*(k * i*di)" 
  1.1782 -        by (simp add: algebra_simps di_def)
  1.1783 -      hence "\<exists> (l::int). c*x+ ?I x e = i*(l + c*k*di)"
  1.1784 -        by (simp add: algebra_simps)
  1.1785 -      hence "\<exists> (l::int). c*x+ ?I x e = i*l" by blast
  1.1786 -      thus "i dvd c*x + Inum (x # bs) e" by (simp add: dvd_def) 
  1.1787 -    next
  1.1788 -      assume 
  1.1789 -        "i dvd c*x + Inum (x # bs) e" (is "?ri dvd ?rc*?rx+?e")
  1.1790 -      hence "\<exists> (l::int). c*x+?e = i*l" by (simp add: dvd_def)
  1.1791 -      hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*l - c*(k*d)" by simp
  1.1792 -      hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*l - c*(k*i*di)" by (simp add: di_def)
  1.1793 -      hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: algebra_simps)
  1.1794 -      hence "\<exists> (l::int). c*x - c * (k*d) +?e = i*l"
  1.1795 -        by blast
  1.1796 -      thus "i dvd c*x - c*(k*d) + Inum (x # bs) e" by (simp add: dvd_def)
  1.1797 -    qed
  1.1798 +    hence "\<exists>(l::int). ?rt = i * l" by (simp add: dvd_def)
  1.1799 +    hence "\<exists>(l::int). c*x+ ?I x e = i*l+c*(k * i*di)"
  1.1800 +      by (simp add: algebra_simps di_def)
  1.1801 +    hence "\<exists>(l::int). c*x+ ?I x e = i*(l + c*k*di)"
  1.1802 +      by (simp add: algebra_simps)
  1.1803 +    hence "\<exists>(l::int). c*x+ ?I x e = i*l" by blast
  1.1804 +    thus "i dvd c*x + Inum (x # bs) e" by (simp add: dvd_def)
  1.1805 +  next
  1.1806 +    assume
  1.1807 +      "i dvd c*x + Inum (x # bs) e" (is "?ri dvd ?rc*?rx+?e")
  1.1808 +    hence "\<exists>(l::int). c*x+?e = i*l" by (simp add: dvd_def)
  1.1809 +    hence "\<exists>(l::int). c*x - c*(k*d) +?e = i*l - c*(k*d)" by simp
  1.1810 +    hence "\<exists>(l::int). c*x - c*(k*d) +?e = i*l - c*(k*i*di)" by (simp add: di_def)
  1.1811 +    hence "\<exists>(l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: algebra_simps)
  1.1812 +    hence "\<exists>(l::int). c*x - c * (k*d) +?e = i*l"
  1.1813 +      by blast
  1.1814 +    thus "i dvd c*x - c*(k*d) + Inum (x # bs) e" by (simp add: dvd_def)
  1.1815 +  qed
  1.1816  qed (auto simp add: gr0_conv_Suc numbound0_I[where bs="bs" and b="x - k*d" and b'="x"])
  1.1817  
  1.1818  lemma mirror_\<alpha>_\<beta>:
  1.1819    assumes lp: "iszlfm p"
  1.1820    shows "(Inum (i#bs)) ` set (\<alpha> p) = (Inum (i#bs)) ` set (\<beta> (mirror p))"
  1.1821 -using lp
  1.1822 -by (induct p rule: mirror.induct, auto)
  1.1823 +  using lp by (induct p rule: mirror.induct) auto
  1.1824  
  1.1825 -lemma mirror: 
  1.1826 +lemma mirror:
  1.1827    assumes lp: "iszlfm p"
  1.1828 -  shows "Ifm bbs (x#bs) (mirror p) = Ifm bbs ((- x)#bs) p" 
  1.1829 -using lp
  1.1830 -proof(induct p rule: iszlfm.induct)
  1.1831 -  case (9 j c e) hence nb: "numbound0 e" by simp
  1.1832 -  have "Ifm bbs (x#bs) (mirror (Dvd j (CN 0 c e))) = (j dvd c*x - Inum (x#bs) e)" (is "_ = (j dvd c*x - ?e)") by simp
  1.1833 -    also have "\<dots> = (j dvd (- (c*x - ?e)))"
  1.1834 +  shows "Ifm bbs (x#bs) (mirror p) = Ifm bbs ((- x)#bs) p"
  1.1835 +  using lp
  1.1836 +proof (induct p rule: iszlfm.induct)
  1.1837 +  case (9 j c e)
  1.1838 +  hence nb: "numbound0 e" by simp
  1.1839 +  have "Ifm bbs (x#bs) (mirror (Dvd j (CN 0 c e))) = (j dvd c*x - Inum (x#bs) e)"
  1.1840 +    (is "_ = (j dvd c*x - ?e)") by simp
  1.1841 +  also have "\<dots> = (j dvd (- (c*x - ?e)))"
  1.1842      by (simp only: dvd_minus_iff)
  1.1843    also have "\<dots> = (j dvd (c* (- x)) + ?e)"
  1.1844      apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_minus add_ac minus_add_distrib)
  1.1845 -    by (simp add: algebra_simps)
  1.1846 +    apply (simp add: algebra_simps)
  1.1847 +    done
  1.1848    also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))"
  1.1849 -    using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"]
  1.1850 -    by simp
  1.1851 +    using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] by simp
  1.1852    finally show ?case .
  1.1853  next
  1.1854 -    case (10 j c e) hence nb: "numbound0 e" by simp
  1.1855 -  have "Ifm bbs (x#bs) (mirror (Dvd j (CN 0 c e))) = (j dvd c*x - Inum (x#bs) e)" (is "_ = (j dvd c*x - ?e)") by simp
  1.1856 -    also have "\<dots> = (j dvd (- (c*x - ?e)))"
  1.1857 +  case (10 j c e) hence nb: "numbound0 e" by simp
  1.1858 +  have "Ifm bbs (x#bs) (mirror (Dvd j (CN 0 c e))) = (j dvd c*x - Inum (x#bs) e)"
  1.1859 +    (is "_ = (j dvd c*x - ?e)") by simp
  1.1860 +  also have "\<dots> = (j dvd (- (c*x - ?e)))"
  1.1861      by (simp only: dvd_minus_iff)
  1.1862    also have "\<dots> = (j dvd (c* (- x)) + ?e)"
  1.1863      apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_minus add_ac minus_add_distrib)
  1.1864 -    by (simp add: algebra_simps)
  1.1865 +    apply (simp add: algebra_simps)
  1.1866 +    done
  1.1867    also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))"
  1.1868 -    using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"]
  1.1869 -    by simp
  1.1870 +    using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] by simp
  1.1871    finally show ?case by simp
  1.1872  qed (auto simp add: numbound0_I[where bs="bs" and b="x" and b'="- x"] gr0_conv_Suc)
  1.1873  
  1.1874 -lemma mirror_l: "iszlfm p \<and> d_\<beta> p 1 
  1.1875 -  \<Longrightarrow> iszlfm (mirror p) \<and> d_\<beta> (mirror p) 1"
  1.1876 +lemma mirror_l: "iszlfm p \<and> d_\<beta> p 1 \<Longrightarrow> iszlfm (mirror p) \<and> d_\<beta> (mirror p) 1"
  1.1877    by (induct p rule: mirror.induct) auto
  1.1878  
  1.1879  lemma mirror_\<delta>: "iszlfm p \<Longrightarrow> \<delta> (mirror p) = \<delta> p"
  1.1880    by (induct p rule: mirror.induct) auto
  1.1881  
  1.1882 -lemma \<beta>_numbound0: assumes lp: "iszlfm p"
  1.1883 -  shows "\<forall> b\<in> set (\<beta> p). numbound0 b"
  1.1884 +lemma \<beta>_numbound0:
  1.1885 +  assumes lp: "iszlfm p"
  1.1886 +  shows "\<forall>b\<in> set (\<beta> p). numbound0 b"
  1.1887    using lp by (induct p rule: \<beta>.induct) auto
  1.1888  
  1.1889 -lemma d_\<beta>_mono: 
  1.1890 +lemma d_\<beta>_mono:
  1.1891    assumes linp: "iszlfm p"
  1.1892 -  and dr: "d_\<beta> p l"
  1.1893 -  and d: "l dvd l'"
  1.1894 +    and dr: "d_\<beta> p l"
  1.1895 +    and d: "l dvd l'"
  1.1896    shows "d_\<beta> p l'"
  1.1897 -using dr linp dvd_trans[of _ "l" "l'", simplified d]
  1.1898 +  using dr linp dvd_trans[of _ "l" "l'", simplified d]
  1.1899    by (induct p rule: iszlfm.induct) simp_all
  1.1900  
  1.1901 -lemma \<alpha>_l: assumes lp: "iszlfm p"
  1.1902 -  shows "\<forall> b\<in> set (\<alpha> p). numbound0 b"
  1.1903 -using lp
  1.1904 -  by(induct p rule: \<alpha>.induct) auto
  1.1905 +lemma \<alpha>_l:
  1.1906 +  assumes lp: "iszlfm p"
  1.1907 +  shows "\<forall>b \<in> set (\<alpha> p). numbound0 b"
  1.1908 +  using lp by (induct p rule: \<alpha>.induct) auto
  1.1909  
  1.1910 -lemma \<zeta>: 
  1.1911 +lemma \<zeta>:
  1.1912    assumes linp: "iszlfm p"
  1.1913    shows "\<zeta> p > 0 \<and> d_\<beta> p (\<zeta> p)"
  1.1914 -using linp
  1.1915 -proof(induct p rule: iszlfm.induct)
  1.1916 +  using linp
  1.1917 +proof (induct p rule: iszlfm.induct)
  1.1918    case (1 p q)
  1.1919    from 1 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
  1.1920    from 1 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
  1.1921 -  from 1 d_\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
  1.1922 -    d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
  1.1923 +  from 1 d_\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"]
  1.1924 +    d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"]
  1.1925      dl1 dl2 show ?case by (auto simp add: lcm_pos_int)
  1.1926  next
  1.1927    case (2 p q)
  1.1928    from 2 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
  1.1929    from 2 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
  1.1930 -  from 2 d_\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
  1.1931 -    d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
  1.1932 +  from 2 d_\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"]
  1.1933 +    d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"]
  1.1934      dl1 dl2 show ?case by (auto simp add: lcm_pos_int)
  1.1935  qed (auto simp add: lcm_pos_int)
  1.1936  
  1.1937 -lemma a_\<beta>: assumes linp: "iszlfm p" and d: "d_\<beta> p l" and lp: "l > 0"
  1.1938 +lemma a_\<beta>:
  1.1939 +  assumes linp: "iszlfm p" and d: "d_\<beta> p l" and lp: "l > 0"
  1.1940    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.1941 -using linp d
  1.1942 +  using linp d
  1.1943  proof (induct p rule: iszlfm.induct)
  1.1944 -  case (5 c e) hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp+
  1.1945 -    from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
  1.1946 -    from cp have cnz: "c \<noteq> 0" by simp
  1.1947 -    have "c div c\<le> l div c"
  1.1948 -      by (simp add: zdiv_mono1[OF clel cp])
  1.1949 -    then have ldcp:"0 < l div c" 
  1.1950 -      by (simp add: div_self[OF cnz])
  1.1951 -    have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
  1.1952 -    hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
  1.1953 -      by simp
  1.1954 -    hence "(l*x + (l div c) * Inum (x # bs) e < 0) =
  1.1955 -          ((c * (l div c)) * x + (l div c) * Inum (x # bs) e < 0)"
  1.1956 -      by simp
  1.1957 -    also have "\<dots> = ((l div c) * (c*x + Inum (x # bs) e) < (l div c) * 0)" by (simp add: algebra_simps)
  1.1958 -    also have "\<dots> = (c*x + Inum (x # bs) e < 0)"
  1.1959 +  case (5 c e)
  1.1960 +  hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all
  1.1961 +  from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
  1.1962 +  from cp have cnz: "c \<noteq> 0" by simp
  1.1963 +  have "c div c\<le> l div c"
  1.1964 +    by (simp add: zdiv_mono1[OF clel cp])
  1.1965 +  then have ldcp:"0 < l div c"
  1.1966 +    by (simp add: div_self[OF cnz])
  1.1967 +  have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"]
  1.1968 +    by simp
  1.1969 +  hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
  1.1970 +    by simp
  1.1971 +  hence "(l*x + (l div c) * Inum (x # bs) e < 0) =
  1.1972 +      ((c * (l div c)) * x + (l div c) * Inum (x # bs) e < 0)"
  1.1973 +    by simp
  1.1974 +  also have "\<dots> = ((l div c) * (c*x + Inum (x # bs) e) < (l div c) * 0)"
  1.1975 +    by (simp add: algebra_simps)
  1.1976 +  also have "\<dots> = (c*x + Inum (x # bs) e < 0)"
  1.1977      using mult_less_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp by simp
  1.1978 -  finally show ?case using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be  by simp
  1.1979 +  finally show ?case
  1.1980 +    using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be by simp
  1.1981  next
  1.1982 -  case (6 c e) hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp+
  1.1983 -    from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
  1.1984 -    from cp have cnz: "c \<noteq> 0" by simp
  1.1985 -    have "c div c\<le> l div c"
  1.1986 -      by (simp add: zdiv_mono1[OF clel cp])
  1.1987 -    then have ldcp:"0 < l div c" 
  1.1988 -      by (simp add: div_self[OF cnz])
  1.1989 -    have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
  1.1990 -    hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
  1.1991 -      by simp
  1.1992 -    hence "(l*x + (l div c) * Inum (x# bs) e \<le> 0) =
  1.1993 -          ((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<le> 0)"
  1.1994 -      by simp
  1.1995 -    also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<le> ((l div c)) * 0)" by (simp add: algebra_simps)
  1.1996 -    also have "\<dots> = (c*x + Inum (x # bs) e \<le> 0)"
  1.1997 +  case (6 c e)
  1.1998 +  hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all
  1.1999 +  from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
  1.2000 +  from cp have cnz: "c \<noteq> 0" by simp
  1.2001 +  have "c div c\<le> l div c"
  1.2002 +    by (simp add: zdiv_mono1[OF clel cp])
  1.2003 +  then have ldcp:"0 < l div c"
  1.2004 +    by (simp add: div_self[OF cnz])
  1.2005 +  have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"]
  1.2006 +    by simp
  1.2007 +  hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
  1.2008 +    by simp
  1.2009 +  hence "(l*x + (l div c) * Inum (x# bs) e \<le> 0) =
  1.2010 +      ((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<le> 0)" by simp
  1.2011 +  also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<le> ((l div c)) * 0)"
  1.2012 +    by (simp add: algebra_simps)
  1.2013 +  also have "\<dots> = (c*x + Inum (x # bs) e \<le> 0)"
  1.2014      using mult_le_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp by simp
  1.2015 -  finally show ?case using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"]  be by simp
  1.2016 +  finally show ?case
  1.2017 +    using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be by simp
  1.2018  next
  1.2019 -  case (7 c e) hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp+
  1.2020 -    from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
  1.2021 -    from cp have cnz: "c \<noteq> 0" by simp
  1.2022 -    have "c div c\<le> l div c"
  1.2023 -      by (simp add: zdiv_mono1[OF clel cp])
  1.2024 -    then have ldcp:"0 < l div c" 
  1.2025 -      by (simp add: div_self[OF cnz])
  1.2026 -    have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
  1.2027 -    hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
  1.2028 -      by simp
  1.2029 -    hence "(l*x + (l div c)* Inum (x # bs) e > 0) =
  1.2030 -          ((c * (l div c)) * x + (l div c) * Inum (x # bs) e > 0)"
  1.2031 -      by simp
  1.2032 -    also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) > ((l div c)) * 0)" by (simp add: algebra_simps)
  1.2033 -    also have "\<dots> = (c * x + Inum (x # bs) e > 0)"
  1.2034 +  case (7 c e)
  1.2035 +  hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all
  1.2036 +  from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
  1.2037 +  from cp have cnz: "c \<noteq> 0" by simp
  1.2038 +  have "c div c\<le> l div c"
  1.2039 +    by (simp add: zdiv_mono1[OF clel cp])
  1.2040 +  then have ldcp:"0 < l div c"
  1.2041 +    by (simp add: div_self[OF cnz])
  1.2042 +  have "c * (l div c) = c* (l div c) + l mod c"
  1.2043 +    using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
  1.2044 +  hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
  1.2045 +    by simp
  1.2046 +  hence "(l*x + (l div c)* Inum (x # bs) e > 0) =
  1.2047 +      ((c * (l div c)) * x + (l div c) * Inum (x # bs) e > 0)" by simp
  1.2048 +  also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) > ((l div c)) * 0)"
  1.2049 +    by (simp add: algebra_simps)
  1.2050 +  also have "\<dots> = (c * x + Inum (x # bs) e > 0)"
  1.2051      using zero_less_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp by simp
  1.2052 -  finally show ?case using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"]  be  by simp
  1.2053 +  finally show ?case
  1.2054 +    using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be by simp
  1.2055  next
  1.2056 -  case (8 c e) hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp+
  1.2057 -    from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
  1.2058 -    from cp have cnz: "c \<noteq> 0" by simp
  1.2059 -    have "c div c\<le> l div c"
  1.2060 -      by (simp add: zdiv_mono1[OF clel cp])
  1.2061 -    then have ldcp:"0 < l div c" 
  1.2062 -      by (simp add: div_self[OF cnz])
  1.2063 -    have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
  1.2064 -    hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
  1.2065 -      by simp
  1.2066 -    hence "(l*x + (l div c)* Inum (x # bs) e \<ge> 0) =
  1.2067 -          ((c*(l div c))*x + (l div c)* Inum (x # bs) e \<ge> 0)"
  1.2068 -      by simp
  1.2069 -    also have "\<dots> = ((l div c)*(c*x + Inum (x # bs) e) \<ge> ((l div c)) * 0)" 
  1.2070 -      by (simp add: algebra_simps)
  1.2071 -    also have "\<dots> = (c*x + Inum (x # bs) e \<ge> 0)" using ldcp 
  1.2072 -      zero_le_mult_iff [where a="l div c" and b="c*x + Inum (x # bs) e"] by simp
  1.2073 -  finally show ?case using be numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"]  
  1.2074 +  case (8 c e)
  1.2075 +  hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all
  1.2076 +  from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
  1.2077 +  from cp have cnz: "c \<noteq> 0" by simp
  1.2078 +  have "c div c\<le> l div c"
  1.2079 +    by (simp add: zdiv_mono1[OF clel cp])
  1.2080 +  then have ldcp:"0 < l div c"
  1.2081 +    by (simp add: div_self[OF cnz])
  1.2082 +  have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"]
  1.2083 +    by simp
  1.2084 +  hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
  1.2085      by simp
  1.2086 +  hence "(l*x + (l div c)* Inum (x # bs) e \<ge> 0) =
  1.2087 +      ((c*(l div c))*x + (l div c)* Inum (x # bs) e \<ge> 0)" by simp
  1.2088 +  also have "\<dots> = ((l div c)*(c*x + Inum (x # bs) e) \<ge> ((l div c)) * 0)"
  1.2089 +    by (simp add: algebra_simps)
  1.2090 +  also have "\<dots> = (c*x + Inum (x # bs) e \<ge> 0)"
  1.2091 +    using ldcp zero_le_mult_iff [where a="l div c" and b="c*x + Inum (x # bs) e"] by simp
  1.2092 +  finally show ?case
  1.2093 +    using be numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] by simp
  1.2094  next
  1.2095 -  case (3 c e) hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp+
  1.2096 -    from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
  1.2097 -    from cp have cnz: "c \<noteq> 0" by simp
  1.2098 -    have "c div c\<le> l div c"
  1.2099 -      by (simp add: zdiv_mono1[OF clel cp])
  1.2100 -    then have ldcp:"0 < l div c" 
  1.2101 -      by (simp add: div_self[OF cnz])
  1.2102 -    have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
  1.2103 -    hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
  1.2104 -      by simp
  1.2105 -    hence "(l * x + (l div c) * Inum (x # bs) e = 0) =
  1.2106 -          ((c * (l div c)) * x + (l div c) * Inum (x # bs) e = 0)"
  1.2107 -      by simp
  1.2108 -    also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) = ((l div c)) * 0)" by (simp add: algebra_simps)
  1.2109 -    also have "\<dots> = (c * x + Inum (x # bs) e = 0)"
  1.2110 +  case (3 c e)
  1.2111 +  hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all
  1.2112 +  from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
  1.2113 +  from cp have cnz: "c \<noteq> 0" by simp
  1.2114 +  have "c div c\<le> l div c"
  1.2115 +    by (simp add: zdiv_mono1[OF clel cp])
  1.2116 +  then have ldcp:"0 < l div c"
  1.2117 +    by (simp add: div_self[OF cnz])
  1.2118 +  have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"]
  1.2119 +    by simp
  1.2120 +  hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
  1.2121 +    by simp
  1.2122 +  hence "(l * x + (l div c) * Inum (x # bs) e = 0) =
  1.2123 +      ((c * (l div c)) * x + (l div c) * Inum (x # bs) e = 0)" by simp
  1.2124 +  also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) = ((l div c)) * 0)"
  1.2125 +    by (simp add: algebra_simps)
  1.2126 +  also have "\<dots> = (c * x + Inum (x # bs) e = 0)"
  1.2127      using mult_eq_0_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp by simp
  1.2128 -  finally show ?case using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"]  be  by simp
  1.2129 +  finally show ?case
  1.2130 +    using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be by simp
  1.2131  next
  1.2132 -  case (4 c e) hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp+
  1.2133 -    from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
  1.2134 -    from cp have cnz: "c \<noteq> 0" by simp
  1.2135 -    have "c div c\<le> l div c"
  1.2136 -      by (simp add: zdiv_mono1[OF clel cp])
  1.2137 -    then have ldcp:"0 < l div c" 
  1.2138 -      by (simp add: div_self[OF cnz])
  1.2139 -    have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
  1.2140 -    hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
  1.2141 -      by simp
  1.2142 -    hence "(l * x + (l div c) * Inum (x # bs) e \<noteq> 0) =
  1.2143 -          ((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<noteq> 0)"
  1.2144 -      by simp
  1.2145 -    also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<noteq> ((l div c)) * 0)" by (simp add: algebra_simps)
  1.2146 -    also have "\<dots> = (c * x + Inum (x # bs) e \<noteq> 0)"
  1.2147 +  case (4 c e)
  1.2148 +  hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all
  1.2149 +  from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
  1.2150 +  from cp have cnz: "c \<noteq> 0" by simp
  1.2151 +  have "c div c\<le> l div c"
  1.2152 +    by (simp add: zdiv_mono1[OF clel cp])
  1.2153 +  then have ldcp:"0 < l div c"
  1.2154 +    by (simp add: div_self[OF cnz])
  1.2155 +  have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"]
  1.2156 +    by simp
  1.2157 +  hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
  1.2158 +    by simp
  1.2159 +  hence "(l * x + (l div c) * Inum (x # bs) e \<noteq> 0) =
  1.2160 +      ((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<noteq> 0)" by simp
  1.2161 +  also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<noteq> ((l div c)) * 0)"
  1.2162 +    by (simp add: algebra_simps)
  1.2163 +  also have "\<dots> = (c * x + Inum (x # bs) e \<noteq> 0)"
  1.2164      using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp by simp
  1.2165 -  finally show ?case using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"]  be  by simp
  1.2166 +  finally show ?case
  1.2167 +    using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be by simp
  1.2168  next
  1.2169 -  case (9 j c e) hence cp: "c>0" and be: "numbound0 e" and jp: "j > 0" and d': "c dvd l" by simp+
  1.2170 -    from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
  1.2171 -    from cp have cnz: "c \<noteq> 0" by simp
  1.2172 -    have "c div c\<le> l div c"
  1.2173 -      by (simp add: zdiv_mono1[OF clel cp])
  1.2174 -    then have ldcp:"0 < l div c" 
  1.2175 -      by (simp add: div_self[OF cnz])
  1.2176 -    have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
  1.2177 -    hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
  1.2178 -      by simp
  1.2179 -    hence "(\<exists> (k::int). l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) = (\<exists> (k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)"  by simp
  1.2180 -    also have "\<dots> = (\<exists> (k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)" by (simp add: algebra_simps)
  1.2181 -    also fix k have "\<dots> = (\<exists> (k::int). c * x + Inum (x # bs) e - j * k = 0)"
  1.2182 +  case (9 j c e)
  1.2183 +  hence cp: "c>0" and be: "numbound0 e" and jp: "j > 0" and d': "c dvd l" by simp_all
  1.2184 +  from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
  1.2185 +  from cp have cnz: "c \<noteq> 0" by simp
  1.2186 +  have "c div c\<le> l div c"
  1.2187 +    by (simp add: zdiv_mono1[OF clel cp])
  1.2188 +  then have ldcp:"0 < l div c"
  1.2189 +    by (simp add: div_self[OF cnz])
  1.2190 +  have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"]
  1.2191 +    by simp
  1.2192 +  hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
  1.2193 +    by simp
  1.2194 +  hence "(\<exists>(k::int). l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) =
  1.2195 +    (\<exists>(k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)" by simp
  1.2196 +  also have "\<dots> = (\<exists>(k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)"
  1.2197 +    by (simp add: algebra_simps)
  1.2198 +  also have "\<dots> = (\<exists>(k::int). c * x + Inum (x # bs) e - j * k = 0)"
  1.2199 +    using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp
  1.2200 +    by simp
  1.2201 +  also have "\<dots> = (\<exists>(k::int). c * x + Inum (x # bs) e = j * k)" by simp
  1.2202 +  finally show ?case
  1.2203 +    using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be mult_strict_mono[OF ldcp jp ldcp ]
  1.2204 +    by (simp add: dvd_def)
  1.2205 +next
  1.2206 +  case (10 j c e)
  1.2207 +  hence cp: "c>0" and be: "numbound0 e" and jp: "j > 0" and d': "c dvd l" by simp_all
  1.2208 +  from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
  1.2209 +  from cp have cnz: "c \<noteq> 0" by simp
  1.2210 +  have "c div c\<le> l div c"
  1.2211 +    by (simp add: zdiv_mono1[OF clel cp])
  1.2212 +  then have ldcp:"0 < l div c"
  1.2213 +    by (simp add: div_self[OF cnz])
  1.2214 +  have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
  1.2215 +  hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric]
  1.2216 +    by simp
  1.2217 +  hence "(\<exists>(k::int). l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) = (\<exists>(k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)"  by simp
  1.2218 +  also have "\<dots> = (\<exists>(k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)" by (simp add: algebra_simps)
  1.2219 +  also fix k have "\<dots> = (\<exists>(k::int). c * x + Inum (x # bs) e - j * k = 0)"
  1.2220      using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp by simp
  1.2221 -  also have "\<dots> = (\<exists> (k::int). c * x + Inum (x # bs) e = j * k)" by simp
  1.2222 -  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.2223 -next
  1.2224 -  case (10 j c e) hence cp: "c>0" and be: "numbound0 e" and jp: "j > 0" and d': "c dvd l" by simp+
  1.2225 -    from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
  1.2226 -    from cp have cnz: "c \<noteq> 0" by simp
  1.2227 -    have "c div c\<le> l div c"
  1.2228 -      by (simp add: zdiv_mono1[OF clel cp])
  1.2229 -    then have ldcp:"0 < l div c" 
  1.2230 -      by (simp add: div_self[OF cnz])
  1.2231 -    have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
  1.2232 -    hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
  1.2233 -      by simp
  1.2234 -    hence "(\<exists> (k::int). l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) = (\<exists> (k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)"  by simp
  1.2235 -    also have "\<dots> = (\<exists> (k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)" by (simp add: algebra_simps)
  1.2236 -    also fix k have "\<dots> = (\<exists> (k::int). c * x + Inum (x # bs) e - j * k = 0)"
  1.2237 -    using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp by simp
  1.2238 -  also have "\<dots> = (\<exists> (k::int). c * x + Inum (x # bs) e = j * k)" by simp
  1.2239 +  also have "\<dots> = (\<exists>(k::int). c * x + Inum (x # bs) e = j * k)" by simp
  1.2240    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.2241  qed (auto simp add: gr0_conv_Suc numbound0_I[where bs="bs" and b="(l * x)" and b'="x"])
  1.2242  
  1.2243  lemma a_\<beta>_ex: assumes linp: "iszlfm p" and d: "d_\<beta> p l" and lp: "l>0"
  1.2244 -  shows "(\<exists> x. l dvd x \<and> Ifm bbs (x #bs) (a_\<beta> p l)) = (\<exists> (x::int). Ifm bbs (x#bs) p)"
  1.2245 -  (is "(\<exists> x. l dvd x \<and> ?P x) = (\<exists> x. ?P' x)")
  1.2246 +  shows "(\<exists>x. l dvd x \<and> Ifm bbs (x #bs) (a_\<beta> p l)) = (\<exists>(x::int). Ifm bbs (x#bs) p)"
  1.2247 +  (is "(\<exists>x. l dvd x \<and> ?P x) = (\<exists>x. ?P' x)")
  1.2248  proof-
  1.2249 -  have "(\<exists> x. l dvd x \<and> ?P x) = (\<exists> (x::int). ?P (l*x))"
  1.2250 +  have "(\<exists>x. l dvd x \<and> ?P x) = (\<exists>(x::int). ?P (l*x))"
  1.2251      using unity_coeff_ex[where l="l" and P="?P", simplified] by simp
  1.2252 -  also have "\<dots> = (\<exists> (x::int). ?P' x)" using a_\<beta>[OF linp d lp] by simp
  1.2253 -  finally show ?thesis  . 
  1.2254 +  also have "\<dots> = (\<exists>(x::int). ?P' x)" using a_\<beta>[OF linp d lp] by simp
  1.2255 +  finally show ?thesis  .
  1.2256  qed
  1.2257  
  1.2258  lemma \<beta>:
  1.2259 @@ -1545,7 +1655,7 @@
  1.2260    and u: "d_\<beta> p 1"
  1.2261    and d: "d_\<delta> p d"
  1.2262    and dp: "d > 0"
  1.2263 -  and nob: "\<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists> b\<in> (Inum (a#bs)) ` set(\<beta> p). x = b + j)"
  1.2264 +  and nob: "\<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists>b\<in> (Inum (a#bs)) ` set(\<beta> p). x = b + j)"
  1.2265    and p: "Ifm bbs (x#bs) p" (is "?P x")
  1.2266    shows "?P (x - d)"
  1.2267  using lp u d dp nob p
  1.2268 @@ -1560,42 +1670,42 @@
  1.2269  next
  1.2270    case (7 c e) hence p: "Ifm bbs (x #bs) (Gt (CN 0 c e))" and c1: "c=1" and bn:"numbound0 e" by simp_all
  1.2271    let ?e = "Inum (x # bs) e"
  1.2272 -  {assume "(x-d) +?e > 0" hence ?case using c1 
  1.2273 +  {assume "(x-d) +?e > 0" hence ?case using c1
  1.2274      numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] by simp}
  1.2275    moreover
  1.2276 -  {assume H: "\<not> (x-d) + ?e > 0" 
  1.2277 +  {assume H: "\<not> (x-d) + ?e > 0"
  1.2278      let ?v="Neg e"
  1.2279      have vb: "?v \<in> set (\<beta> (Gt (CN 0 c e)))" by simp
  1.2280 -    from 7(5)[simplified simp_thms Inum.simps \<beta>.simps set.simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]] 
  1.2281 -    have nob: "\<not> (\<exists> j\<in> {1 ..d}. x =  - ?e + j)" by auto 
  1.2282 +    from 7(5)[simplified simp_thms Inum.simps \<beta>.simps set.simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]]
  1.2283 +    have nob: "\<not> (\<exists>j\<in> {1 ..d}. x =  - ?e + j)" by auto
  1.2284      from H p have "x + ?e > 0 \<and> x + ?e \<le> d" by (simp add: c1)
  1.2285      hence "x + ?e \<ge> 1 \<and> x + ?e \<le> d"  by simp
  1.2286 -    hence "\<exists> (j::int) \<in> {1 .. d}. j = x + ?e" by simp
  1.2287 -    hence "\<exists> (j::int) \<in> {1 .. d}. x = (- ?e + j)" 
  1.2288 +    hence "\<exists>(j::int) \<in> {1 .. d}. j = x + ?e" by simp
  1.2289 +    hence "\<exists>(j::int) \<in> {1 .. d}. x = (- ?e + j)"
  1.2290        by (simp add: algebra_simps)
  1.2291      with nob have ?case by auto}
  1.2292    ultimately show ?case by blast
  1.2293  next
  1.2294 -  case (8 c e) hence p: "Ifm bbs (x #bs) (Ge (CN 0 c e))" and c1: "c=1" and bn:"numbound0 e" 
  1.2295 -    by simp+
  1.2296 +  case (8 c e) hence p: "Ifm bbs (x #bs) (Ge (CN 0 c e))" and c1: "c=1" and bn:"numbound0 e"
  1.2297 +    by simp_all
  1.2298      let ?e = "Inum (x # bs) e"
  1.2299 -    {assume "(x-d) +?e \<ge> 0" hence ?case using  c1 
  1.2300 +    {assume "(x-d) +?e \<ge> 0" hence ?case using  c1
  1.2301        numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"]
  1.2302          by simp}
  1.2303      moreover
  1.2304 -    {assume H: "\<not> (x-d) + ?e \<ge> 0" 
  1.2305 +    {assume H: "\<not> (x-d) + ?e \<ge> 0"
  1.2306        let ?v="Sub (C -1) e"
  1.2307        have vb: "?v \<in> set (\<beta> (Ge (CN 0 c e)))" by simp
  1.2308 -      from 8(5)[simplified simp_thms Inum.simps \<beta>.simps set.simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]] 
  1.2309 -      have nob: "\<not> (\<exists> j\<in> {1 ..d}. x =  - ?e - 1 + j)" by auto 
  1.2310 +      from 8(5)[simplified simp_thms Inum.simps \<beta>.simps set.simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]]
  1.2311 +      have nob: "\<not> (\<exists>j\<in> {1 ..d}. x =  - ?e - 1 + j)" by auto
  1.2312        from H p have "x + ?e \<ge> 0 \<and> x + ?e < d" by (simp add: c1)
  1.2313        hence "x + ?e +1 \<ge> 1 \<and> x + ?e + 1 \<le> d"  by simp
  1.2314 -      hence "\<exists> (j::int) \<in> {1 .. d}. j = x + ?e + 1" by simp
  1.2315 -      hence "\<exists> (j::int) \<in> {1 .. d}. x= - ?e - 1 + j" by (simp add: algebra_simps)
  1.2316 +      hence "\<exists>(j::int) \<in> {1 .. d}. j = x + ?e + 1" by simp
  1.2317 +      hence "\<exists>(j::int) \<in> {1 .. d}. x= - ?e - 1 + j" by (simp add: algebra_simps)
  1.2318        with nob have ?case by simp }
  1.2319      ultimately show ?case by blast
  1.2320  next
  1.2321 -  case (3 c e) hence p: "Ifm bbs (x #bs) (Eq (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp+
  1.2322 +  case (3 c e) hence p: "Ifm bbs (x #bs) (Eq (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp_all
  1.2323      let ?e = "Inum (x # bs) e"
  1.2324      let ?v="(Sub (C -1) e)"
  1.2325      have vb: "?v \<in> set (\<beta> (Eq (CN 0 c e)))" by simp
  1.2326 @@ -1603,11 +1713,11 @@
  1.2327        by simp (erule ballE[where x="1"],
  1.2328          simp_all add:algebra_simps numbound0_I[OF bn,where b="x"and b'="a"and bs="bs"])
  1.2329  next
  1.2330 -  case (4 c e)hence p: "Ifm bbs (x #bs) (NEq (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp+
  1.2331 +  case (4 c e)hence p: "Ifm bbs (x #bs) (NEq (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp_all
  1.2332      let ?e = "Inum (x # bs) e"
  1.2333      let ?v="Neg e"
  1.2334      have vb: "?v \<in> set (\<beta> (NEq (CN 0 c e)))" by simp
  1.2335 -    {assume "x - d + Inum (((x -d)) # bs) e \<noteq> 0" 
  1.2336 +    {assume "x - d + Inum (((x -d)) # bs) e \<noteq> 0"
  1.2337        hence ?case by (simp add: c1)}
  1.2338      moreover
  1.2339      {assume H: "x - d + Inum (((x -d)) # bs) e = 0"
  1.2340 @@ -1616,40 +1726,40 @@
  1.2341          by (simp add: numbound0_I[OF bn,where b="x - d"and b'="a"and bs="bs"])
  1.2342         with 4(5) have ?case using dp by simp}
  1.2343    ultimately show ?case by blast
  1.2344 -next 
  1.2345 -  case (9 j c e) hence p: "Ifm bbs (x #bs) (Dvd j (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp+
  1.2346 +next
  1.2347 +  case (9 j c e) hence p: "Ifm bbs (x #bs) (Dvd j (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp_all
  1.2348      let ?e = "Inum (x # bs) e"
  1.2349      from 9 have id: "j dvd d" by simp
  1.2350      from c1 have "?p x = (j dvd (x+ ?e))" by simp
  1.2351 -    also have "\<dots> = (j dvd x - d + ?e)" 
  1.2352 +    also have "\<dots> = (j dvd x - d + ?e)"
  1.2353        using zdvd_period[OF id, where x="x" and c="-1" and t="?e"] by simp
  1.2354 -    finally show ?case 
  1.2355 +    finally show ?case
  1.2356        using numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] c1 p by simp
  1.2357  next
  1.2358 -  case (10 j c e) hence p: "Ifm bbs (x #bs) (NDvd j (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp+
  1.2359 +  case (10 j c e) hence p: "Ifm bbs (x #bs) (NDvd j (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp_all
  1.2360      let ?e = "Inum (x # bs) e"
  1.2361      from 10 have id: "j dvd d" by simp
  1.2362      from c1 have "?p x = (\<not> j dvd (x+ ?e))" by simp
  1.2363 -    also have "\<dots> = (\<not> j dvd x - d + ?e)" 
  1.2364 +    also have "\<dots> = (\<not> j dvd x - d + ?e)"
  1.2365        using zdvd_period[OF id, where x="x" and c="-1" and t="?e"] by simp
  1.2366      finally show ?case using numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] c1 p by simp
  1.2367  qed (auto simp add: numbound0_I[where bs="bs" and b="(x - d)" and b'="x"] gr0_conv_Suc)
  1.2368  
  1.2369 -lemma \<beta>':   
  1.2370 +lemma \<beta>':
  1.2371    assumes lp: "iszlfm p"
  1.2372    and u: "d_\<beta> p 1"
  1.2373    and d: "d_\<delta> p d"
  1.2374    and dp: "d > 0"
  1.2375 -  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.2376 +  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.2377  proof(clarify)
  1.2378 -  fix x 
  1.2379 -  assume nb:"?b" and px: "?P x" 
  1.2380 -  hence nb2: "\<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists> b\<in> (Inum (a#bs)) ` set(\<beta> p). x = b + j)"
  1.2381 +  fix x
  1.2382 +  assume nb:"?b" and px: "?P x"
  1.2383 +  hence nb2: "\<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists>b\<in> (Inum (a#bs)) ` set(\<beta> p). x = b + j)"
  1.2384      by auto
  1.2385    from  \<beta>[OF lp u d dp nb2 px] show "?P (x -d )" .
  1.2386  qed
  1.2387  lemma cpmi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. x < z --> (P x = P1 x))
  1.2388 -==> ALL x.~(EX (j::int) : {1..D}. EX (b::int) : B. P(b+j)) --> P (x) --> P (x - D) 
  1.2389 +==> ALL x.~(EX (j::int) : {1..D}. EX (b::int) : B. P(b+j)) --> P (x) --> P (x - D)
  1.2390  ==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x-k*D))))
  1.2391  ==> (EX (x::int). P(x)) = ((EX (j::int) : {1..D} . (P1(j))) | (EX (j::int) : {1..D}. EX (b::int) : B. P (b+j)))"
  1.2392  apply(rule iffI)
  1.2393 @@ -1675,55 +1785,57 @@
  1.2394    and u: "d_\<beta> p 1"
  1.2395    and d: "d_\<delta> p d"
  1.2396    and dp: "d > 0"
  1.2397 -  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.2398 -  (is "(\<exists> (x::int). ?P (x)) = (\<exists> j\<in> ?D. ?M j \<or> (\<exists> b\<in> ?B. ?P (?I b + j)))")
  1.2399 +  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.2400 +  (is "(\<exists>(x::int). ?P (x)) = (\<exists>j\<in> ?D. ?M j \<or> (\<exists>b\<in> ?B. ?P (?I b + j)))")
  1.2401  proof-
  1.2402 -  from minusinf_inf[OF lp u] 
  1.2403 +  from minusinf_inf[OF lp u]
  1.2404    have th: "\<exists>(z::int). \<forall>x<z. ?P (x) = ?M x" by blast
  1.2405    let ?B' = "{?I b | b. b\<in> ?B}"
  1.2406 -  have BB': "(\<exists>j\<in>?D. \<exists>b\<in> ?B. ?P (?I b +j)) = (\<exists> j \<in> ?D. \<exists> b \<in> ?B'. ?P (b + j))" by auto
  1.2407 -  hence th2: "\<forall> x. \<not> (\<exists> j \<in> ?D. \<exists> b \<in> ?B'. ?P ((b + j))) \<longrightarrow> ?P (x) \<longrightarrow> ?P ((x - d))" 
  1.2408 +  have BB': "(\<exists>j\<in>?D. \<exists>b\<in> ?B. ?P (?I b +j)) = (\<exists>j \<in> ?D. \<exists>b \<in> ?B'. ?P (b + j))" by auto
  1.2409 +  hence th2: "\<forall>x. \<not> (\<exists>j \<in> ?D. \<exists>b \<in> ?B'. ?P ((b + j))) \<longrightarrow> ?P (x) \<longrightarrow> ?P ((x - d))"
  1.2410      using \<beta>'[OF lp u d dp, where a="i" and bbs = "bbs"] by blast
  1.2411    from minusinf_repeats[OF d lp]
  1.2412 -  have th3: "\<forall> x k. ?M x = ?M (x-k*d)" by simp
  1.2413 +  have th3: "\<forall>x k. ?M x = ?M (x-k*d)" by simp
  1.2414    from cpmi_eq[OF dp th th2 th3] BB' show ?thesis by blast
  1.2415  qed
  1.2416  
  1.2417      (* Implement the right hand sides of Cooper's theorem and Ferrante and Rackoff. *)
  1.2418 -lemma mirror_ex: 
  1.2419 +lemma mirror_ex:
  1.2420    assumes lp: "iszlfm p"
  1.2421 -  shows "(\<exists> x. Ifm bbs (x#bs) (mirror p)) = (\<exists> x. Ifm bbs (x#bs) p)"
  1.2422 -  (is "(\<exists> x. ?I x ?mp) = (\<exists> x. ?I x p)")
  1.2423 +  shows "(\<exists>x. Ifm bbs (x#bs) (mirror p)) = (\<exists>x. Ifm bbs (x#bs) p)"
  1.2424 +  (is "(\<exists>x. ?I x ?mp) = (\<exists>x. ?I x p)")
  1.2425  proof(auto)
  1.2426    fix x assume "?I x ?mp" hence "?I (- x) p" using mirror[OF lp] by blast
  1.2427 -  thus "\<exists> x. ?I x p" by blast
  1.2428 +  thus "\<exists>x. ?I x p" by blast
  1.2429  next
  1.2430 -  fix x assume "?I x p" hence "?I (- x) ?mp" 
  1.2431 +  fix x assume "?I x p" hence "?I (- x) ?mp"
  1.2432      using mirror[OF lp, where x="- x", symmetric] by auto
  1.2433 -  thus "\<exists> x. ?I x ?mp" by blast
  1.2434 +  thus "\<exists>x. ?I x ?mp" by blast
  1.2435  qed
  1.2436  
  1.2437  
  1.2438 -lemma cp_thm': 
  1.2439 +lemma cp_thm':
  1.2440    assumes lp: "iszlfm p"
  1.2441    and up: "d_\<beta> p 1" and dd: "d_\<delta> p d" and dp: "d > 0"
  1.2442 -  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.2443 +  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.2444    using cp_thm[OF lp up dd dp,where i="i"] by auto
  1.2445  
  1.2446 -definition unit :: "fm \<Rightarrow> fm \<times> num list \<times> int" where
  1.2447 -  "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.2448 +definition unit :: "fm \<Rightarrow> fm \<times> num list \<times> int"
  1.2449 +where
  1.2450 +  "unit p = (let p' = zlfm p ; l = \<zeta> p' ; q = And (Dvd l (CN 0 1 (C 0))) (a_\<beta> p' l); d = \<delta> q;
  1.2451               B = remdups (map simpnum (\<beta> q)) ; a = remdups (map simpnum (\<alpha> q))
  1.2452               in if length B \<le> length a then (q,B,d) else (mirror q, a,d))"
  1.2453  
  1.2454 -lemma unit: assumes qf: "qfree p"
  1.2455 -  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.2456 -proof-
  1.2457 -  fix q B d 
  1.2458 +lemma unit:
  1.2459 +  assumes qf: "qfree p"
  1.2460 +  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.2461 +proof -
  1.2462 +  fix q B d
  1.2463    assume qBd: "unit p = (q,B,d)"
  1.2464 -  let ?thes = "((\<exists> x. Ifm bbs (x#bs) p) = (\<exists> x. Ifm bbs (x#bs) q)) \<and>
  1.2465 +  let ?thes = "((\<exists>x. Ifm bbs (x#bs) p) = (\<exists>x. Ifm bbs (x#bs) q)) \<and>
  1.2466      Inum (i#bs) ` set B = Inum (i#bs) ` set (\<beta> q) \<and>
  1.2467 -    d_\<beta> q 1 \<and> d_\<delta> q d \<and> 0 < d \<and> iszlfm q \<and> (\<forall> b\<in> set B. numbound0 b)"
  1.2468 -  let ?I = "\<lambda> x p. Ifm bbs (x#bs) p"
  1.2469 +    d_\<beta> q 1 \<and> d_\<delta> q d \<and> 0 < d \<and> iszlfm q \<and> (\<forall>b\<in> set B. numbound0 b)"
  1.2470 +  let ?I = "\<lambda>x p. Ifm bbs (x#bs) p"
  1.2471    let ?p' = "zlfm p"
  1.2472    let ?l = "\<zeta> ?p'"
  1.2473    let ?q = "And (Dvd ?l (CN 0 1 (C 0))) (a_\<beta> ?p' ?l)"
  1.2474 @@ -1732,40 +1844,40 @@
  1.2475    let ?B'= "remdups (map simpnum (\<beta> ?q))"
  1.2476    let ?A = "set (\<alpha> ?q)"
  1.2477    let ?A'= "remdups (map simpnum (\<alpha> ?q))"
  1.2478 -  from conjunct1[OF zlfm_I[OF qf, where bs="bs"]] 
  1.2479 -  have pp': "\<forall> i. ?I i ?p' = ?I i p" by auto
  1.2480 +  from conjunct1[OF zlfm_I[OF qf, where bs="bs"]]
  1.2481 +  have pp': "\<forall>i. ?I i ?p' = ?I i p" by auto
  1.2482    from conjunct2[OF zlfm_I[OF qf, where bs="bs" and i="i"]]
  1.2483 -  have lp': "iszlfm ?p'" . 
  1.2484 +  have lp': "iszlfm ?p'" .
  1.2485    from lp' \<zeta>[where p="?p'"] have lp: "?l >0" and dl: "d_\<beta> ?p' ?l" by auto
  1.2486    from a_\<beta>_ex[where p="?p'" and l="?l" and bs="bs", OF lp' dl lp] pp'
  1.2487 -  have pq_ex:"(\<exists> (x::int). ?I x p) = (\<exists> x. ?I x ?q)" by simp 
  1.2488 +  have pq_ex:"(\<exists>(x::int). ?I x p) = (\<exists>x. ?I x ?q)" by simp
  1.2489    from lp' lp a_\<beta>[OF lp' dl lp] have lq:"iszlfm ?q" and uq: "d_\<beta> ?q 1"  by auto
  1.2490    from \<delta>[OF lq] have dp:"?d >0" and dd: "d_\<delta> ?q ?d" by blast+
  1.2491 -  let ?N = "\<lambda> t. Inum (i#bs) t"
  1.2492 -  have "?N ` set ?B' = ((?N o simpnum) ` ?B)" by auto 
  1.2493 +  let ?N = "\<lambda>t. Inum (i#bs) t"
  1.2494 +  have "?N ` set ?B' = ((?N o simpnum) ` ?B)" by auto
  1.2495    also have "\<dots> = ?N ` ?B" using simpnum_ci[where bs="i#bs"] by auto
  1.2496    finally have BB': "?N ` set ?B' = ?N ` ?B" .
  1.2497 -  have "?N ` set ?A' = ((?N o simpnum) ` ?A)" by auto 
  1.2498 +  have "?N ` set ?A' = ((?N o simpnum) ` ?A)" by auto
  1.2499    also have "\<dots> = ?N ` ?A" using simpnum_ci[where bs="i#bs"] by auto
  1.2500    finally have AA': "?N ` set ?A' = ?N ` ?A" .
  1.2501 -  from \<beta>_numbound0[OF lq] have B_nb:"\<forall> b\<in> set ?B'. numbound0 b"
  1.2502 +  from \<beta>_numbound0[OF lq] have B_nb:"\<forall>b\<in> set ?B'. numbound0 b"
  1.2503      by (simp add: simpnum_numbound0)
  1.2504 -  from \<alpha>_l[OF lq] have A_nb: "\<forall> b\<in> set ?A'. numbound0 b"
  1.2505 +  from \<alpha>_l[OF lq] have A_nb: "\<forall>b\<in> set ?A'. numbound0 b"
  1.2506      by (simp add: simpnum_numbound0)
  1.2507      {assume "length ?B' \<le> length ?A'"
  1.2508      hence q:"q=?q" and "B = ?B'" and d:"d = ?d"
  1.2509        using qBd by (auto simp add: Let_def unit_def)
  1.2510 -    with BB' B_nb have b: "?N ` (set B) = ?N ` set (\<beta> q)" 
  1.2511 -      and bn: "\<forall>b\<in> set B. numbound0 b" by simp+ 
  1.2512 +    with BB' B_nb have b: "?N ` (set B) = ?N ` set (\<beta> q)"
  1.2513 +      and bn: "\<forall>b\<in> set B. numbound0 b" by simp_all
  1.2514    with pq_ex dp uq dd lq q d have ?thes by simp}
  1.2515 -  moreover 
  1.2516 +  moreover
  1.2517    {assume "\<not> (length ?B' \<le> length ?A')"
  1.2518      hence q:"q=mirror ?q" and "B = ?A'" and d:"d = ?d"
  1.2519        using qBd by (auto simp add: Let_def unit_def)
  1.2520 -    with AA' mirror_\<alpha>_\<beta>[OF lq] A_nb have b:"?N ` (set B) = ?N ` set (\<beta> q)" 
  1.2521 -      and bn: "\<forall>b\<in> set B. numbound0 b" by simp+
  1.2522 -    from mirror_ex[OF lq] pq_ex q 
  1.2523 -    have pqm_eq:"(\<exists> (x::int). ?I x p) = (\<exists> (x::int). ?I x q)" by simp
  1.2524 +    with AA' mirror_\<alpha>_\<beta>[OF lq] A_nb have b:"?N ` (set B) = ?N ` set (\<beta> q)"
  1.2525 +      and bn: "\<forall>b\<in> set B. numbound0 b" by simp_all
  1.2526 +    from mirror_ex[OF lq] pq_ex q
  1.2527 +    have pqm_eq:"(\<exists>(x::int). ?I x p) = (\<exists>(x::int). ?I x q)" by simp
  1.2528      from lq uq q mirror_l[where p="?q"]
  1.2529      have lq': "iszlfm q" and uq: "d_\<beta> q 1" by auto
  1.2530      from \<delta>[OF lq'] mirror_\<delta>[OF lq] q d have dq:"d_\<delta> q d " by auto
  1.2531 @@ -1773,84 +1885,99 @@
  1.2532    }
  1.2533    ultimately show ?thes by blast
  1.2534  qed
  1.2535 -    (* Cooper's Algorithm *)
  1.2536 +
  1.2537 +
  1.2538 +text {* Cooper's Algorithm *}
  1.2539  
  1.2540  definition cooper :: "fm \<Rightarrow> fm" where
  1.2541 -  "cooper p \<equiv> 
  1.2542 -  (let (q,B,d) = unit p; js = [1..d];
  1.2543 -       mq = simpfm (minusinf q);
  1.2544 -       md = evaldjf (\<lambda> j. simpfm (subst0 (C j) mq)) js
  1.2545 -   in if md = T then T else
  1.2546 -    (let qd = evaldjf (\<lambda> (b,j). simpfm (subst0 (Add b (C j)) q)) 
  1.2547 -                               [(b,j). b\<leftarrow>B,j\<leftarrow>js]
  1.2548 -     in decr (disj md qd)))"
  1.2549 -lemma cooper: assumes qf: "qfree p"
  1.2550 -  shows "((\<exists> x. Ifm bbs (x#bs) p) = (Ifm bbs bs (cooper p))) \<and> qfree (cooper p)" 
  1.2551 +  "cooper p =
  1.2552 +    (let
  1.2553 +      (q, B, d) = unit p;
  1.2554 +      js = [1..d];
  1.2555 +      mq = simpfm (minusinf q);
  1.2556 +      md = evaldjf (\<lambda>j. simpfm (subst0 (C j) mq)) js
  1.2557 +     in
  1.2558 +      if md = T then T
  1.2559 +      else
  1.2560 +        (let
  1.2561 +          qd = evaldjf (\<lambda>(b, j). simpfm (subst0 (Add b (C j)) q)) [(b, j). b \<leftarrow> B, j \<leftarrow> js]
  1.2562 +         in decr (disj md qd)))"
  1.2563 +
  1.2564 +lemma cooper:
  1.2565 +  assumes qf: "qfree p"
  1.2566 +  shows "((\<exists>x. Ifm bbs (x#bs) p) = (Ifm bbs bs (cooper p))) \<and> qfree (cooper p)"
  1.2567    (is "(?lhs = ?rhs) \<and> _")
  1.2568 -proof-
  1.2569 -  let ?I = "\<lambda> x p. Ifm bbs (x#bs) p"
  1.2570 +proof -
  1.2571 +  let ?I = "\<lambda>x p. Ifm bbs (x#bs) p"
  1.2572    let ?q = "fst (unit p)"
  1.2573    let ?B = "fst (snd(unit p))"
  1.2574    let ?d = "snd (snd (unit p))"
  1.2575    let ?js = "[1..?d]"
  1.2576    let ?mq = "minusinf ?q"
  1.2577    let ?smq = "simpfm ?mq"
  1.2578 -  let ?md = "evaldjf (\<lambda> j. simpfm (subst0 (C j) ?smq)) ?js"
  1.2579 +  let ?md = "evaldjf (\<lambda>j. simpfm (subst0 (C j) ?smq)) ?js"
  1.2580    fix i
  1.2581 -  let ?N = "\<lambda> t. Inum (i#bs) t"
  1.2582 +  let ?N = "\<lambda>t. Inum (i#bs) t"
  1.2583    let ?Bjs = "[(b,j). b\<leftarrow>?B,j\<leftarrow>?js]"
  1.2584 -  let ?qd = "evaldjf (\<lambda> (b,j). simpfm (subst0 (Add b (C j)) ?q)) ?Bjs"
  1.2585 +  let ?qd = "evaldjf (\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)) ?Bjs"
  1.2586    have qbf:"unit p = (?q,?B,?d)" by simp
  1.2587 -  from unit[OF qf qbf] have pq_ex: "(\<exists>(x::int). ?I x p) = (\<exists> (x::int). ?I x ?q)" and 
  1.2588 -    B:"?N ` set ?B = ?N ` set (\<beta> ?q)" and 
  1.2589 -    uq:"d_\<beta> ?q 1" and dd: "d_\<delta> ?q ?d" and dp: "?d > 0" and 
  1.2590 -    lq: "iszlfm ?q" and 
  1.2591 -    Bn: "\<forall> b\<in> set ?B. numbound0 b" by auto
  1.2592 +  from unit[OF qf qbf] have pq_ex: "(\<exists>(x::int). ?I x p) = (\<exists>(x::int). ?I x ?q)" and
  1.2593 +    B:"?N ` set ?B = ?N ` set (\<beta> ?q)" and
  1.2594 +    uq:"d_\<beta> ?q 1" and dd: "d_\<delta> ?q ?d" and dp: "?d > 0" and
  1.2595 +    lq: "iszlfm ?q" and
  1.2596 +    Bn: "\<forall>b\<in> set ?B. numbound0 b" by auto
  1.2597    from zlin_qfree[OF lq] have qfq: "qfree ?q" .
  1.2598    from simpfm_qf[OF minusinf_qfree[OF qfq]] have qfmq: "qfree ?smq".
  1.2599 -  have jsnb: "\<forall> j \<in> set ?js. numbound0 (C j)" by simp
  1.2600 -  hence "\<forall> j\<in> set ?js. bound0 (subst0 (C j) ?smq)" 
  1.2601 +  have jsnb: "\<forall>j \<in> set ?js. numbound0 (C j)" by simp
  1.2602 +  hence "\<forall>j\<in> set ?js. bound0 (subst0 (C j) ?smq)"
  1.2603      by (auto simp only: subst0_bound0[OF qfmq])
  1.2604 -  hence th: "\<forall> j\<in> set ?js. bound0 (simpfm (subst0 (C j) ?smq))"
  1.2605 +  hence th: "\<forall>j\<in> set ?js. bound0 (simpfm (subst0 (C j) ?smq))"
  1.2606      by (auto simp add: simpfm_bound0)
  1.2607 -  from evaldjf_bound0[OF th] have mdb: "bound0 ?md" by simp 
  1.2608 -  from Bn jsnb have "\<forall> (b,j) \<in> set ?Bjs. numbound0 (Add b (C j))"
  1.2609 +  from evaldjf_bound0[OF th] have mdb: "bound0 ?md" by simp
  1.2610 +  from Bn jsnb have "\<forall>(b,j) \<in> set ?Bjs. numbound0 (Add b (C j))"
  1.2611      by simp
  1.2612 -  hence "\<forall> (b,j) \<in> set ?Bjs. bound0 (subst0 (Add b (C j)) ?q)"
  1.2613 +  hence "\<forall>(b,j) \<in> set ?Bjs. bound0 (subst0 (Add b (C j)) ?q)"
  1.2614      using subst0_bound0[OF qfq] by blast
  1.2615 -  hence "\<forall> (b,j) \<in> set ?Bjs. bound0 (simpfm (subst0 (Add b (C j)) ?q))"
  1.2616 +  hence "\<forall>(b,j) \<in> set ?Bjs. bound0 (simpfm (subst0 (Add b (C j)) ?q))"
  1.2617      using simpfm_bound0  by blast
  1.2618 -  hence th': "\<forall> x \<in> set ?Bjs. bound0 ((\<lambda> (b,j). simpfm (subst0 (Add b (C j)) ?q)) x)"
  1.2619 -    by auto 
  1.2620 +  hence th': "\<forall>x \<in> set ?Bjs. bound0 ((\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)) x)"
  1.2621 +    by auto
  1.2622    from evaldjf_bound0 [OF th'] have qdb: "bound0 ?qd" by simp
  1.2623 -  from mdb qdb 
  1.2624 -  have mdqdb: "bound0 (disj ?md ?qd)" by (simp only: disj_def, cases "?md=T \<or> ?qd=T", simp_all)
  1.2625 +  from mdb qdb
  1.2626 +  have mdqdb: "bound0 (disj ?md ?qd)" unfolding disj_def by (cases "?md=T \<or> ?qd=T") simp_all
  1.2627    from trans [OF pq_ex cp_thm'[OF lq uq dd dp,where i="i"]] B
  1.2628 -  have "?lhs = (\<exists> j\<in> {1.. ?d}. ?I j ?mq \<or> (\<exists> b\<in> ?N ` set ?B. Ifm bbs ((b+ j)#bs) ?q))" by auto
  1.2629 -  also have "\<dots> = (\<exists> j\<in> {1.. ?d}. ?I j ?mq \<or> (\<exists> b\<in> set ?B. Ifm bbs ((?N b+ j)#bs) ?q))" by simp
  1.2630 -  also have "\<dots> = ((\<exists> j\<in> {1.. ?d}. ?I j ?mq ) \<or> (\<exists> j\<in> {1.. ?d}. \<exists> b\<in> set ?B. Ifm bbs ((?N (Add b (C j)))#bs) ?q))" by (simp only: Inum.simps) blast
  1.2631 -  also have "\<dots> = ((\<exists> j\<in> {1.. ?d}. ?I j ?smq ) \<or> (\<exists> j\<in> {1.. ?d}. \<exists> b\<in> set ?B. Ifm bbs ((?N (Add b (C j)))#bs) ?q))" by (simp add: simpfm) 
  1.2632 -  also have "\<dots> = ((\<exists> j\<in> set ?js. (\<lambda> j. ?I i (simpfm (subst0 (C j) ?smq))) j) \<or> (\<exists> j\<in> set ?js. \<exists> b\<in> set ?B. Ifm bbs ((?N (Add b (C j)))#bs) ?q))"
  1.2633 +  have "?lhs = (\<exists>j\<in> {1.. ?d}. ?I j ?mq \<or> (\<exists>b\<in> ?N ` set ?B. Ifm bbs ((b+ j)#bs) ?q))" by auto
  1.2634 +  also have "\<dots> = (\<exists>j\<in> {1.. ?d}. ?I j ?mq \<or> (\<exists>b\<in> set ?B. Ifm bbs ((?N b+ j)#bs) ?q))" by simp
  1.2635 +  also have "\<dots> = ((\<exists>j\<in> {1.. ?d}. ?I j ?mq ) \<or>
  1.2636 +      (\<exists>j\<in> {1.. ?d}. \<exists>b\<in> set ?B. Ifm bbs ((?N (Add b (C j)))#bs) ?q))"
  1.2637 +    by (simp only: Inum.simps) blast
  1.2638 +  also have "\<dots> = ((\<exists>j\<in> {1.. ?d}. ?I j ?smq ) \<or>
  1.2639 +      (\<exists>j\<in> {1.. ?d}. \<exists>b\<in> set ?B. Ifm bbs ((?N (Add b (C j)))#bs) ?q))"
  1.2640 +    by (simp add: simpfm)
  1.2641 +  also have "\<dots> = ((\<exists>j\<in> set ?js. (\<lambda>j. ?I i (simpfm (subst0 (C j) ?smq))) j) \<or>
  1.2642 +      (\<exists>j\<in> set ?js. \<exists>b\<in> set ?B. Ifm bbs ((?N (Add b (C j)))#bs) ?q))"
  1.2643      by (simp only: simpfm subst0_I[OF qfmq] set_upto) auto
  1.2644 -  also have "\<dots> = (?I i (evaldjf (\<lambda> j. simpfm (subst0 (C j) ?smq)) ?js) \<or> (\<exists> j\<in> set ?js. \<exists> b\<in> set ?B. ?I i (subst0 (Add b (C j)) ?q)))" 
  1.2645 -   by (simp only: evaldjf_ex subst0_I[OF qfq])
  1.2646 - 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.2647 -   by (simp only: simpfm set_concat set_map concat_map_singleton UN_simps) blast
  1.2648 - also have "\<dots> = (?I i ?md \<or> (?I i (evaldjf (\<lambda> (b,j). simpfm (subst0 (Add b (C j)) ?q)) ?Bjs)))"
  1.2649 -   by (simp only: evaldjf_ex[where bs="i#bs" and f="\<lambda> (b,j). simpfm (subst0 (Add b (C j)) ?q)" and ps="?Bjs"]) (auto simp add: split_def)
  1.2650 - finally have mdqd: "?lhs = (?I i ?md \<or> ?I i ?qd)" by simp  
  1.2651 +  also have "\<dots> = (?I i (evaldjf (\<lambda>j. simpfm (subst0 (C j) ?smq)) ?js) \<or>
  1.2652 +      (\<exists>j\<in> set ?js. \<exists>b\<in> set ?B. ?I i (subst0 (Add b (C j)) ?q)))"
  1.2653 +    by (simp only: evaldjf_ex subst0_I[OF qfq])
  1.2654 +  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.2655 +    by (simp only: simpfm set_concat set_map concat_map_singleton UN_simps) blast
  1.2656 +  also have "\<dots> = (?I i ?md \<or> (?I i (evaldjf (\<lambda>(b,j). simpfm (subst0 (Add b (C j)) ?q)) ?Bjs)))"
  1.2657 +    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.2658 +      (auto simp add: split_def)
  1.2659 +  finally have mdqd: "?lhs = (?I i ?md \<or> ?I i ?qd)" by simp
  1.2660    also have "\<dots> = (?I i (disj ?md ?qd))" by (simp add: disj)
  1.2661 -  also have "\<dots> = (Ifm bbs bs (decr (disj ?md ?qd)))" by (simp only: decr [OF mdqdb]) 
  1.2662 -  finally have mdqd2: "?lhs = (Ifm bbs bs (decr (disj ?md ?qd)))" . 
  1.2663 -  {assume mdT: "?md = T"
  1.2664 -    hence cT:"cooper p = T" 
  1.2665 +  also have "\<dots> = (Ifm bbs bs (decr (disj ?md ?qd)))" by (simp only: decr [OF mdqdb])
  1.2666 +  finally have mdqd2: "?lhs = (Ifm bbs bs (decr (disj ?md ?qd)))" .
  1.2667 +  { assume mdT: "?md = T"
  1.2668 +    hence cT:"cooper p = T"
  1.2669        by (simp only: cooper_def unit_def split_def Let_def if_True) simp
  1.2670 -    from mdT have lhs:"?lhs" using mdqd by simp 
  1.2671 +    from mdT have lhs:"?lhs" using mdqd by simp
  1.2672      from mdT have "?rhs" by (simp add: cooper_def unit_def split_def)
  1.2673      with lhs cT have ?thesis by simp }
  1.2674    moreover
  1.2675 -  {assume mdT: "?md \<noteq> T" hence "cooper p = decr (disj ?md ?qd)" 
  1.2676 -      by (simp only: cooper_def unit_def split_def Let_def if_False) 
  1.2677 +  { assume mdT: "?md \<noteq> T" hence "cooper p = decr (disj ?md ?qd)"
  1.2678 +      by (simp only: cooper_def unit_def split_def Let_def if_False)
  1.2679      with mdqd2 decr_qf[OF mdqdb] have ?thesis by simp }
  1.2680    ultimately show ?thesis by blast
  1.2681  qed
  1.2682 @@ -1861,12 +1988,11 @@
  1.2683  theorem mirqe: "(Ifm bbs bs (pa p) = Ifm bbs bs p) \<and> qfree (pa p)"
  1.2684    using qelim_ci cooper prep by (auto simp add: pa_def)
  1.2685  
  1.2686 -definition
  1.2687 -  cooper_test :: "unit \<Rightarrow> fm"
  1.2688 -where
  1.2689 -  "cooper_test u = pa (E (A (Imp (Ge (Sub (Bound 0) (Bound 1)))
  1.2690 -    (E (E (Eq (Sub (Add (Mul 3 (Bound 1)) (Mul 5 (Bound 0)))
  1.2691 -      (Bound 2))))))))"
  1.2692 +definition cooper_test :: "unit \<Rightarrow> fm"
  1.2693 +  where
  1.2694 +    "cooper_test u =
  1.2695 +      pa (E (A (Imp (Ge (Sub (Bound 0) (Bound 1)))
  1.2696 +        (E (E (Eq (Sub (Add (Mul 3 (Bound 1)) (Mul 5 (Bound 0))) (Bound 2))))))))"
  1.2697  
  1.2698  ML {* @{code cooper_test} () *}
  1.2699  
  1.2700 @@ -1905,7 +2031,7 @@
  1.2701    | fm_of_term ps vs (@{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"} $ t1 $ t2) =
  1.2702        @{code Le} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
  1.2703    | fm_of_term ps vs (@{term "op = :: int \<Rightarrow> int \<Rightarrow> bool"} $ t1 $ t2) =
  1.2704 -      @{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2)) 
  1.2705 +      @{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
  1.2706    | fm_of_term ps vs (@{term "op dvd :: int \<Rightarrow> int \<Rightarrow> bool"} $ t1 $ t2) =
  1.2707        (case try HOLogic.dest_number t1
  1.2708         of SOME (_, i) => @{code Dvd} (i, num_of_term vs t2)
  1.2709 @@ -1943,7 +2069,7 @@
  1.2710        term_of_num vs (@{code C} i) $ term_of_num vs t2
  1.2711    | term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t));
  1.2712  
  1.2713 -fun term_of_fm ps vs @{code T} = @{term True} 
  1.2714 +fun term_of_fm ps vs @{code T} = @{term True}
  1.2715    | term_of_fm ps vs @{code F} = @{term False}
  1.2716    | term_of_fm ps vs (@{code Lt} t) =
  1.2717        @{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"} $ term_of_num vs t $ @{term "0::int"}
  1.2718 @@ -1980,11 +2106,11 @@
  1.2719        @{term "op = :: int => _"}, @{term "op < :: int => _"},
  1.2720        @{term "op <= :: int => _"}, @{term "Not"}, @{term "All :: (int => _) => _"},
  1.2721        @{term "Ex :: (int => _) => _"}, @{term "True"}, @{term "False"}]
  1.2722 -    fun is_ty t = not (fastype_of t = HOLogic.boolT) 
  1.2723 +    fun is_ty t = not (fastype_of t = HOLogic.boolT)
  1.2724    in case t
  1.2725 -   of (l as f $ a) $ b => if is_ty t orelse is_op t then term_bools (term_bools acc l)b 
  1.2726 +   of (l as f $ a) $ b => if is_ty t orelse is_op t then term_bools (term_bools acc l)b
  1.2727          else insert (op aconv) t acc
  1.2728 -    | f $ a => if is_ty t orelse is_op t then term_bools (term_bools acc f) a  
  1.2729 +    | f $ a => if is_ty t orelse is_op t then term_bools (term_bools acc f) a
  1.2730          else insert (op aconv) t acc
  1.2731      | Abs p => term_bools acc (snd (Syntax_Trans.variant_abs p))  (* FIXME !? *)
  1.2732      | _ => if is_ty t orelse is_op t then acc else insert (op aconv) t acc
  1.2733 @@ -2013,7 +2139,7 @@
  1.2734  
  1.2735  text {* Tests *}
  1.2736  
  1.2737 -lemma "\<exists> (j::int). \<forall> x\<ge>j. (\<exists> a b. x = 3*a+5*b)"
  1.2738 +lemma "\<exists>(j::int). \<forall>x\<ge>j. (\<exists>a b. x = 3*a+5*b)"
  1.2739    by cooper
  1.2740  
  1.2741  lemma "ALL (x::int) >=8. EX i j. 5*i + 3*j = x"
  1.2742 @@ -2034,7 +2160,7 @@
  1.2743    by cooper
  1.2744  
  1.2745  lemma "ALL (x::int) >=8. EX i j. 5*i + 3*j = x"
  1.2746 -  by cooper 
  1.2747 +  by cooper
  1.2748  
  1.2749  lemma "ALL (y::int) (z::int) (n::int). 3 dvd z --> 2 dvd (y::int) --> (EX (x::int).  2*x =  y) & (EX (k::int). 3*k = z)"
  1.2750    by cooper
  1.2751 @@ -2063,7 +2189,7 @@
  1.2752  lemma "~ (ALL(x::int). ((2 dvd x) = (ALL(y::int). x ~= 2*y+1) | (EX(q::int) (u::int) i. 3*i + 2*q - u < 17) --> 0 < x | ((~ 3 dvd x) &(x + 8 = 0))))"
  1.2753    by cooper
  1.2754  
  1.2755 -lemma "~ (ALL(i::int). 4 <= i --> (EX x y. 0 <= x & 0 <= y & 3 * x + 5 * y = i))" 
  1.2756 +lemma "~ (ALL(i::int). 4 <= i --> (EX x y. 0 <= x & 0 <= y & 3 * x + 5 * y = i))"
  1.2757    by cooper
  1.2758  
  1.2759  lemma "EX j. ALL (x::int) >= j. EX i j. 5*i + 3*j = x"
  1.2760 @@ -2091,10 +2217,10 @@
  1.2761  
  1.2762  theorem "\<forall>(x::int) y. x < y --> 2 * x + 1 < 2 * y"
  1.2763    by cooper
  1.2764 - 
  1.2765 +
  1.2766  theorem "\<forall>(x::int) y. 2 * x + 1 \<noteq> 2 * y"
  1.2767    by cooper
  1.2768 - 
  1.2769 +
  1.2770  theorem "\<exists>(x::int) y. 0 < x  & 0 \<le> y  & 3 * x - 5 * y = 1"
  1.2771    by cooper
  1.2772  
  1.2773 @@ -2105,23 +2231,23 @@
  1.2774    by cooper
  1.2775  
  1.2776  theorem "\<forall>(x::int). (2 dvd x) --> (\<exists>(y::int). x = 2*y)"
  1.2777 -  by cooper 
  1.2778 +  by cooper
  1.2779  
  1.2780  theorem "\<forall>(x::int). (2 dvd x) --> (\<exists>(y::int). x = 2*y)"
  1.2781 -  by cooper 
  1.2782 +  by cooper
  1.2783  
  1.2784  theorem "\<forall>(x::int). (2 dvd x) = (\<exists>(y::int). x = 2*y)"
  1.2785 -  by cooper 
  1.2786 +  by cooper
  1.2787  
  1.2788  theorem "\<forall>(x::int). ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y + 1))"
  1.2789 -  by cooper 
  1.2790 +  by cooper
  1.2791  
  1.2792 -theorem "~ (\<forall>(x::int). 
  1.2793 -            ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y+1) | 
  1.2794 +theorem "~ (\<forall>(x::int).
  1.2795 +            ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y+1) |
  1.2796               (\<exists>(q::int) (u::int) i. 3*i + 2*q - u < 17)
  1.2797               --> 0 < x | ((~ 3 dvd x) &(x + 8 = 0))))"
  1.2798    by cooper
  1.2799 - 
  1.2800 +
  1.2801  theorem "~ (\<forall>(i::int). 4 \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i))"
  1.2802    by cooper
  1.2803