src/HOL/Decision_Procs/Cooper.thy
author wenzelm
Wed Nov 28 15:59:18 2012 +0100 (2012-11-28)
changeset 50252 4aa34bd43228
parent 49962 a8cc904a6820
child 50313 5b49cfd43a37
permissions -rw-r--r--
eliminated slightly odd identifiers;
     1 (*  Title:      HOL/Decision_Procs/Cooper.thy
     2     Author:     Amine Chaieb
     3 *)
     4 
     5 theory Cooper
     6 imports Complex_Main "~~/src/HOL/Library/Efficient_Nat" "~~/src/HOL/Library/Old_Recdef"
     7 begin
     8 
     9 (* Periodicity of dvd *)
    10 
    11   (*********************************************************************************)
    12   (****                            SHADOW SYNTAX AND SEMANTICS                  ****)
    13   (*********************************************************************************)
    14 
    15 datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num 
    16   | Mul int num
    17 
    18   (* A size for num to make inductive proofs simpler*)
    19 primrec num_size :: "num \<Rightarrow> nat" where
    20   "num_size (C c) = 1"
    21 | "num_size (Bound n) = 1"
    22 | "num_size (Neg a) = 1 + num_size a"
    23 | "num_size (Add a b) = 1 + num_size a + num_size b"
    24 | "num_size (Sub a b) = 3 + num_size a + num_size b"
    25 | "num_size (CN n c a) = 4 + num_size a"
    26 | "num_size (Mul c a) = 1 + num_size a"
    27 
    28 primrec Inum :: "int list \<Rightarrow> num \<Rightarrow> int" where
    29   "Inum bs (C c) = c"
    30 | "Inum bs (Bound n) = bs!n"
    31 | "Inum bs (CN n c a) = c * (bs!n) + (Inum bs a)"
    32 | "Inum bs (Neg a) = -(Inum bs a)"
    33 | "Inum bs (Add a b) = Inum bs a + Inum bs b"
    34 | "Inum bs (Sub a b) = Inum bs a - Inum bs b"
    35 | "Inum bs (Mul c a) = c* Inum bs a"
    36 
    37 datatype fm  = 
    38   T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| Dvd int num| NDvd int num|
    39   NOT fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm 
    40   | Closed nat | NClosed nat
    41 
    42 
    43   (* A size for fm *)
    44 fun fmsize :: "fm \<Rightarrow> nat" where
    45   "fmsize (NOT p) = 1 + fmsize p"
    46 | "fmsize (And p q) = 1 + fmsize p + fmsize q"
    47 | "fmsize (Or p q) = 1 + fmsize p + fmsize q"
    48 | "fmsize (Imp p q) = 3 + fmsize p + fmsize q"
    49 | "fmsize (Iff p q) = 3 + 2*(fmsize p + fmsize q)"
    50 | "fmsize (E p) = 1 + fmsize p"
    51 | "fmsize (A p) = 4+ fmsize p"
    52 | "fmsize (Dvd i t) = 2"
    53 | "fmsize (NDvd i t) = 2"
    54 | "fmsize p = 1"
    55   (* several lemmas about fmsize *)
    56 lemma fmsize_pos: "fmsize p > 0"
    57   by (induct p rule: fmsize.induct) simp_all
    58 
    59   (* Semantics of formulae (fm) *)
    60 primrec Ifm ::"bool list \<Rightarrow> int list \<Rightarrow> fm \<Rightarrow> bool" where
    61   "Ifm bbs bs T = True"
    62 | "Ifm bbs bs F = False"
    63 | "Ifm bbs bs (Lt a) = (Inum bs a < 0)"
    64 | "Ifm bbs bs (Gt a) = (Inum bs a > 0)"
    65 | "Ifm bbs bs (Le a) = (Inum bs a \<le> 0)"
    66 | "Ifm bbs bs (Ge a) = (Inum bs a \<ge> 0)"
    67 | "Ifm bbs bs (Eq a) = (Inum bs a = 0)"
    68 | "Ifm bbs bs (NEq a) = (Inum bs a \<noteq> 0)"
    69 | "Ifm bbs bs (Dvd i b) = (i dvd Inum bs b)"
    70 | "Ifm bbs bs (NDvd i b) = (\<not>(i dvd Inum bs b))"
    71 | "Ifm bbs bs (NOT p) = (\<not> (Ifm bbs bs p))"
    72 | "Ifm bbs bs (And p q) = (Ifm bbs bs p \<and> Ifm bbs bs q)"
    73 | "Ifm bbs bs (Or p q) = (Ifm bbs bs p \<or> Ifm bbs bs q)"
    74 | "Ifm bbs bs (Imp p q) = ((Ifm bbs bs p) \<longrightarrow> (Ifm bbs bs q))"
    75 | "Ifm bbs bs (Iff p q) = (Ifm bbs bs p = Ifm bbs bs q)"
    76 | "Ifm bbs bs (E p) = (\<exists> x. Ifm bbs (x#bs) p)"
    77 | "Ifm bbs bs (A p) = (\<forall> x. Ifm bbs (x#bs) p)"
    78 | "Ifm bbs bs (Closed n) = bbs!n"
    79 | "Ifm bbs bs (NClosed n) = (\<not> bbs!n)"
    80 
    81 consts prep :: "fm \<Rightarrow> fm"
    82 recdef prep "measure fmsize"
    83   "prep (E T) = T"
    84   "prep (E F) = F"
    85   "prep (E (Or p q)) = Or (prep (E p)) (prep (E q))"
    86   "prep (E (Imp p q)) = Or (prep (E (NOT p))) (prep (E q))"
    87   "prep (E (Iff p q)) = Or (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))" 
    88   "prep (E (NOT (And p q))) = Or (prep (E (NOT p))) (prep (E(NOT q)))"
    89   "prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))"
    90   "prep (E (NOT (Iff p q))) = Or (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))"
    91   "prep (E p) = E (prep p)"
    92   "prep (A (And p q)) = And (prep (A p)) (prep (A q))"
    93   "prep (A p) = prep (NOT (E (NOT p)))"
    94   "prep (NOT (NOT p)) = prep p"
    95   "prep (NOT (And p q)) = Or (prep (NOT p)) (prep (NOT q))"
    96   "prep (NOT (A p)) = prep (E (NOT p))"
    97   "prep (NOT (Or p q)) = And (prep (NOT p)) (prep (NOT q))"
    98   "prep (NOT (Imp p q)) = And (prep p) (prep (NOT q))"
    99   "prep (NOT (Iff p q)) = Or (prep (And p (NOT q))) (prep (And (NOT p) q))"
   100   "prep (NOT p) = NOT (prep p)"
   101   "prep (Or p q) = Or (prep p) (prep q)"
   102   "prep (And p q) = And (prep p) (prep q)"
   103   "prep (Imp p q) = prep (Or (NOT p) q)"
   104   "prep (Iff p q) = Or (prep (And p q)) (prep (And (NOT p) (NOT q)))"
   105   "prep p = p"
   106 (hints simp add: fmsize_pos)
   107 lemma prep: "Ifm bbs bs (prep p) = Ifm bbs bs p"
   108 by (induct p arbitrary: bs rule: prep.induct, auto)
   109 
   110 
   111   (* Quantifier freeness *)
   112 fun qfree:: "fm \<Rightarrow> bool" where
   113   "qfree (E p) = False"
   114 | "qfree (A p) = False"
   115 | "qfree (NOT p) = qfree p" 
   116 | "qfree (And p q) = (qfree p \<and> qfree q)" 
   117 | "qfree (Or  p q) = (qfree p \<and> qfree q)" 
   118 | "qfree (Imp p q) = (qfree p \<and> qfree q)" 
   119 | "qfree (Iff p q) = (qfree p \<and> qfree q)"
   120 | "qfree p = True"
   121 
   122   (* Boundedness and substitution *)
   123     
   124 primrec numbound0:: "num \<Rightarrow> bool" (* a num is INDEPENDENT of Bound 0 *) where
   125   "numbound0 (C c) = True"
   126 | "numbound0 (Bound n) = (n>0)"
   127 | "numbound0 (CN n i a) = (n >0 \<and> numbound0 a)"
   128 | "numbound0 (Neg a) = numbound0 a"
   129 | "numbound0 (Add a b) = (numbound0 a \<and> numbound0 b)"
   130 | "numbound0 (Sub a b) = (numbound0 a \<and> numbound0 b)" 
   131 | "numbound0 (Mul i a) = numbound0 a"
   132 
   133 lemma numbound0_I:
   134   assumes nb: "numbound0 a"
   135   shows "Inum (b#bs) a = Inum (b'#bs) a"
   136 using nb
   137 by (induct a rule: num.induct) (auto simp add: gr0_conv_Suc)
   138 
   139 primrec bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *) where
   140   "bound0 T = True"
   141 | "bound0 F = True"
   142 | "bound0 (Lt a) = numbound0 a"
   143 | "bound0 (Le a) = numbound0 a"
   144 | "bound0 (Gt a) = numbound0 a"
   145 | "bound0 (Ge a) = numbound0 a"
   146 | "bound0 (Eq a) = numbound0 a"
   147 | "bound0 (NEq a) = numbound0 a"
   148 | "bound0 (Dvd i a) = numbound0 a"
   149 | "bound0 (NDvd i a) = numbound0 a"
   150 | "bound0 (NOT p) = bound0 p"
   151 | "bound0 (And p q) = (bound0 p \<and> bound0 q)"
   152 | "bound0 (Or p q) = (bound0 p \<and> bound0 q)"
   153 | "bound0 (Imp p q) = ((bound0 p) \<and> (bound0 q))"
   154 | "bound0 (Iff p q) = (bound0 p \<and> bound0 q)"
   155 | "bound0 (E p) = False"
   156 | "bound0 (A p) = False"
   157 | "bound0 (Closed P) = True"
   158 | "bound0 (NClosed P) = True"
   159 lemma bound0_I:
   160   assumes bp: "bound0 p"
   161   shows "Ifm bbs (b#bs) p = Ifm bbs (b'#bs) p"
   162 using bp numbound0_I[where b="b" and bs="bs" and b'="b'"]
   163 by (induct p rule: fm.induct) (auto simp add: gr0_conv_Suc)
   164 
   165 fun numsubst0:: "num \<Rightarrow> num \<Rightarrow> num" where
   166   "numsubst0 t (C c) = (C c)"
   167 | "numsubst0 t (Bound n) = (if n=0 then t else Bound n)"
   168 | "numsubst0 t (CN 0 i a) = Add (Mul i t) (numsubst0 t a)"
   169 | "numsubst0 t (CN n i a) = CN n i (numsubst0 t a)"
   170 | "numsubst0 t (Neg a) = Neg (numsubst0 t a)"
   171 | "numsubst0 t (Add a b) = Add (numsubst0 t a) (numsubst0 t b)"
   172 | "numsubst0 t (Sub a b) = Sub (numsubst0 t a) (numsubst0 t b)" 
   173 | "numsubst0 t (Mul i a) = Mul i (numsubst0 t a)"
   174 
   175 lemma numsubst0_I:
   176   "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b#bs) a)#bs) t"
   177 by (induct t rule: numsubst0.induct,auto simp:nth_Cons')
   178 
   179 lemma numsubst0_I':
   180   "numbound0 a \<Longrightarrow> Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b'#bs) a)#bs) t"
   181 by (induct t rule: numsubst0.induct, auto simp: nth_Cons' numbound0_I[where b="b" and b'="b'"])
   182 
   183 primrec subst0:: "num \<Rightarrow> fm \<Rightarrow> fm" (* substitue a num into a formula for Bound 0 *) where
   184   "subst0 t T = T"
   185 | "subst0 t F = F"
   186 | "subst0 t (Lt a) = Lt (numsubst0 t a)"
   187 | "subst0 t (Le a) = Le (numsubst0 t a)"
   188 | "subst0 t (Gt a) = Gt (numsubst0 t a)"
   189 | "subst0 t (Ge a) = Ge (numsubst0 t a)"
   190 | "subst0 t (Eq a) = Eq (numsubst0 t a)"
   191 | "subst0 t (NEq a) = NEq (numsubst0 t a)"
   192 | "subst0 t (Dvd i a) = Dvd i (numsubst0 t a)"
   193 | "subst0 t (NDvd i a) = NDvd i (numsubst0 t a)"
   194 | "subst0 t (NOT p) = NOT (subst0 t p)"
   195 | "subst0 t (And p q) = And (subst0 t p) (subst0 t q)"
   196 | "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)"
   197 | "subst0 t (Imp p q) = Imp (subst0 t p) (subst0 t q)"
   198 | "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)"
   199 | "subst0 t (Closed P) = (Closed P)"
   200 | "subst0 t (NClosed P) = (NClosed P)"
   201 
   202 lemma subst0_I: assumes qfp: "qfree p"
   203   shows "Ifm bbs (b#bs) (subst0 a p) = Ifm bbs ((Inum (b#bs) a)#bs) p"
   204   using qfp numsubst0_I[where b="b" and bs="bs" and a="a"]
   205   by (induct p) (simp_all add: gr0_conv_Suc)
   206 
   207 fun decrnum:: "num \<Rightarrow> num" where
   208   "decrnum (Bound n) = Bound (n - 1)"
   209 | "decrnum (Neg a) = Neg (decrnum a)"
   210 | "decrnum (Add a b) = Add (decrnum a) (decrnum b)"
   211 | "decrnum (Sub a b) = Sub (decrnum a) (decrnum b)"
   212 | "decrnum (Mul c a) = Mul c (decrnum a)"
   213 | "decrnum (CN n i a) = (CN (n - 1) i (decrnum a))"
   214 | "decrnum a = a"
   215 
   216 fun decr :: "fm \<Rightarrow> fm" where
   217   "decr (Lt a) = Lt (decrnum a)"
   218 | "decr (Le a) = Le (decrnum a)"
   219 | "decr (Gt a) = Gt (decrnum a)"
   220 | "decr (Ge a) = Ge (decrnum a)"
   221 | "decr (Eq a) = Eq (decrnum a)"
   222 | "decr (NEq a) = NEq (decrnum a)"
   223 | "decr (Dvd i a) = Dvd i (decrnum a)"
   224 | "decr (NDvd i a) = NDvd i (decrnum a)"
   225 | "decr (NOT p) = NOT (decr p)" 
   226 | "decr (And p q) = And (decr p) (decr q)"
   227 | "decr (Or p q) = Or (decr p) (decr q)"
   228 | "decr (Imp p q) = Imp (decr p) (decr q)"
   229 | "decr (Iff p q) = Iff (decr p) (decr q)"
   230 | "decr p = p"
   231 
   232 lemma decrnum: assumes nb: "numbound0 t"
   233   shows "Inum (x#bs) t = Inum bs (decrnum t)"
   234   using nb by (induct t rule: decrnum.induct, auto simp add: gr0_conv_Suc)
   235 
   236 lemma decr: assumes nb: "bound0 p"
   237   shows "Ifm bbs (x#bs) p = Ifm bbs bs (decr p)"
   238   using nb 
   239   by (induct p rule: decr.induct, simp_all add: gr0_conv_Suc decrnum)
   240 
   241 lemma decr_qf: "bound0 p \<Longrightarrow> qfree (decr p)"
   242 by (induct p, simp_all)
   243 
   244 fun isatom :: "fm \<Rightarrow> bool" (* test for atomicity *) where
   245   "isatom T = True"
   246 | "isatom F = True"
   247 | "isatom (Lt a) = True"
   248 | "isatom (Le a) = True"
   249 | "isatom (Gt a) = True"
   250 | "isatom (Ge a) = True"
   251 | "isatom (Eq a) = True"
   252 | "isatom (NEq a) = True"
   253 | "isatom (Dvd i b) = True"
   254 | "isatom (NDvd i b) = True"
   255 | "isatom (Closed P) = True"
   256 | "isatom (NClosed P) = True"
   257 | "isatom p = False"
   258 
   259 lemma numsubst0_numbound0: assumes nb: "numbound0 t"
   260   shows "numbound0 (numsubst0 t a)"
   261 using nb apply (induct a)
   262 apply simp_all
   263 apply (case_tac nat, simp_all)
   264 done
   265 
   266 lemma subst0_bound0: assumes qf: "qfree p" and nb: "numbound0 t"
   267   shows "bound0 (subst0 t p)"
   268 using qf numsubst0_numbound0[OF nb] by (induct p) auto
   269 
   270 lemma bound0_qf: "bound0 p \<Longrightarrow> qfree p"
   271 by (induct p, simp_all)
   272 
   273 
   274 definition djf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a \<Rightarrow> fm \<Rightarrow> fm" where
   275   "djf f p q \<equiv> (if q=T then T else if q=F then f p else 
   276   (let fp = f p in case fp of T \<Rightarrow> T | F \<Rightarrow> q | _ \<Rightarrow> Or (f p) q))"
   277 definition evaldjf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a list \<Rightarrow> fm" where
   278   "evaldjf f ps \<equiv> foldr (djf f) ps F"
   279 
   280 lemma djf_Or: "Ifm bbs bs (djf f p q) = Ifm bbs bs (Or (f p) q)"
   281 by (cases "q=T", simp add: djf_def,cases "q=F",simp add: djf_def) 
   282 (cases "f p", simp_all add: Let_def djf_def) 
   283 
   284 lemma evaldjf_ex: "Ifm bbs bs (evaldjf f ps) = (\<exists> p \<in> set ps. Ifm bbs bs (f p))"
   285   by(induct ps, simp_all add: evaldjf_def djf_Or)
   286 
   287 lemma evaldjf_bound0: 
   288   assumes nb: "\<forall> x\<in> set xs. bound0 (f x)"
   289   shows "bound0 (evaldjf f xs)"
   290   using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto) 
   291 
   292 lemma evaldjf_qf: 
   293   assumes nb: "\<forall> x\<in> set xs. qfree (f x)"
   294   shows "qfree (evaldjf f xs)"
   295   using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto) 
   296 
   297 fun disjuncts :: "fm \<Rightarrow> fm list" where
   298   "disjuncts (Or p q) = (disjuncts p) @ (disjuncts q)"
   299 | "disjuncts F = []"
   300 | "disjuncts p = [p]"
   301 
   302 lemma disjuncts: "(\<exists> q\<in> set (disjuncts p). Ifm bbs bs q) = Ifm bbs bs p"
   303 by(induct p rule: disjuncts.induct, auto)
   304 
   305 lemma disjuncts_nb: "bound0 p \<Longrightarrow> \<forall> q\<in> set (disjuncts p). bound0 q"
   306 proof-
   307   assume nb: "bound0 p"
   308   hence "list_all bound0 (disjuncts p)" by (induct p rule:disjuncts.induct,auto)
   309   thus ?thesis by (simp only: list_all_iff)
   310 qed
   311 
   312 lemma disjuncts_qf: "qfree p \<Longrightarrow> \<forall> q\<in> set (disjuncts p). qfree q"
   313 proof-
   314   assume qf: "qfree p"
   315   hence "list_all qfree (disjuncts p)"
   316     by (induct p rule: disjuncts.induct, auto)
   317   thus ?thesis by (simp only: list_all_iff)
   318 qed
   319 
   320 definition DJ :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm" where
   321   "DJ f p \<equiv> evaldjf f (disjuncts p)"
   322 
   323 lemma DJ: assumes fdj: "\<forall> p q. f (Or p q) = Or (f p) (f q)"
   324   and fF: "f F = F"
   325   shows "Ifm bbs bs (DJ f p) = Ifm bbs bs (f p)"
   326 proof-
   327   have "Ifm bbs bs (DJ f p) = (\<exists> q \<in> set (disjuncts p). Ifm bbs bs (f q))"
   328     by (simp add: DJ_def evaldjf_ex) 
   329   also have "\<dots> = Ifm bbs bs (f p)" using fdj fF by (induct p rule: disjuncts.induct, auto)
   330   finally show ?thesis .
   331 qed
   332 
   333 lemma DJ_qf: assumes 
   334   fqf: "\<forall> p. qfree p \<longrightarrow> qfree (f p)"
   335   shows "\<forall>p. qfree p \<longrightarrow> qfree (DJ f p) "
   336 proof(clarify)
   337   fix  p assume qf: "qfree p"
   338   have th: "DJ f p = evaldjf f (disjuncts p)" by (simp add: DJ_def)
   339   from disjuncts_qf[OF qf] have "\<forall> q\<in> set (disjuncts p). qfree q" .
   340   with fqf have th':"\<forall> q\<in> set (disjuncts p). qfree (f q)" by blast
   341   
   342   from evaldjf_qf[OF th'] th show "qfree (DJ f p)" by simp
   343 qed
   344 
   345 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))"
   346   shows "\<forall> bs p. qfree p \<longrightarrow> qfree (DJ qe p) \<and> (Ifm bbs bs ((DJ qe p)) = Ifm bbs bs (E p))"
   347 proof(clarify)
   348   fix p::fm and bs
   349   assume qf: "qfree p"
   350   from qe have qth: "\<forall> p. qfree p \<longrightarrow> qfree (qe p)" by blast
   351   from DJ_qf[OF qth] qf have qfth:"qfree (DJ qe p)" by auto
   352   have "Ifm bbs bs (DJ qe p) = (\<exists> q\<in> set (disjuncts p). Ifm bbs bs (qe q))"
   353     by (simp add: DJ_def evaldjf_ex)
   354   also have "\<dots> = (\<exists> q \<in> set(disjuncts p). Ifm bbs bs (E q))" using qe disjuncts_qf[OF qf] by auto
   355   also have "\<dots> = Ifm bbs bs (E p)" by (induct p rule: disjuncts.induct, auto)
   356   finally show "qfree (DJ qe p) \<and> Ifm bbs bs (DJ qe p) = Ifm bbs bs (E p)" using qfth by blast
   357 qed
   358   (* Simplification *)
   359 
   360   (* Algebraic simplifications for nums *)
   361 
   362 fun bnds:: "num \<Rightarrow> nat list" where
   363   "bnds (Bound n) = [n]"
   364 | "bnds (CN n c a) = n#(bnds a)"
   365 | "bnds (Neg a) = bnds a"
   366 | "bnds (Add a b) = (bnds a)@(bnds b)"
   367 | "bnds (Sub a b) = (bnds a)@(bnds b)"
   368 | "bnds (Mul i a) = bnds a"
   369 | "bnds a = []"
   370 
   371 fun lex_ns:: "nat list \<Rightarrow> nat list \<Rightarrow> bool" where
   372   "lex_ns [] ms = True"
   373 | "lex_ns ns [] = False"
   374 | "lex_ns (n#ns) (m#ms) = (n<m \<or> ((n = m) \<and> lex_ns ns ms)) "
   375 definition lex_bnd :: "num \<Rightarrow> num \<Rightarrow> bool" where
   376   "lex_bnd t s \<equiv> lex_ns (bnds t) (bnds s)"
   377 
   378 consts
   379   numadd:: "num \<times> num \<Rightarrow> num"
   380 recdef numadd "measure (\<lambda> (t,s). num_size t + num_size s)"
   381   "numadd (CN n1 c1 r1 ,CN n2 c2 r2) =
   382   (if n1=n2 then 
   383   (let c = c1 + c2
   384   in (if c=0 then numadd(r1,r2) else CN n1 c (numadd (r1,r2))))
   385   else if n1 \<le> n2 then CN n1 c1 (numadd (r1,Add (Mul c2 (Bound n2)) r2))
   386   else CN n2 c2 (numadd (Add (Mul c1 (Bound n1)) r1,r2)))"
   387   "numadd (CN n1 c1 r1, t) = CN n1 c1 (numadd (r1, t))"  
   388   "numadd (t,CN n2 c2 r2) = CN n2 c2 (numadd (t,r2))" 
   389   "numadd (C b1, C b2) = C (b1+b2)"
   390   "numadd (a,b) = Add a b"
   391 
   392 (*function (sequential)
   393   numadd :: "num \<Rightarrow> num \<Rightarrow> num"
   394 where
   395   "numadd (Add (Mul c1 (Bound n1)) r1) (Add (Mul c2 (Bound n2)) r2) =
   396       (if n1 = n2 then (let c = c1 + c2
   397       in (if c = 0 then numadd r1 r2 else
   398         Add (Mul c (Bound n1)) (numadd r1 r2)))
   399       else if n1 \<le> n2 then
   400         Add (Mul c1 (Bound n1)) (numadd r1 (Add (Mul c2 (Bound n2)) r2))
   401       else
   402         Add (Mul c2 (Bound n2)) (numadd (Add (Mul c1 (Bound n1)) r1) r2))"
   403   | "numadd (Add (Mul c1 (Bound n1)) r1) t =
   404       Add (Mul c1 (Bound n1)) (numadd r1 t)"  
   405   | "numadd t (Add (Mul c2 (Bound n2)) r2) =
   406       Add (Mul c2 (Bound n2)) (numadd t r2)" 
   407   | "numadd (C b1) (C b2) = C (b1 + b2)"
   408   | "numadd a b = Add a b"
   409 apply pat_completeness apply auto*)
   410   
   411 lemma numadd: "Inum bs (numadd (t,s)) = Inum bs (Add t s)"
   412 apply (induct t s rule: numadd.induct, simp_all add: Let_def)
   413 apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
   414  apply (case_tac "n1 = n2")
   415   apply(simp_all add: algebra_simps)
   416 apply(simp add: distrib_right[symmetric])
   417 done
   418 
   419 lemma numadd_nb: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))"
   420 by (induct t s rule: numadd.induct, auto simp add: Let_def)
   421 
   422 fun nummul :: "int \<Rightarrow> num \<Rightarrow> num" where
   423   "nummul i (C j) = C (i * j)"
   424 | "nummul i (CN n c t) = CN n (c*i) (nummul i t)"
   425 | "nummul i t = Mul i t"
   426 
   427 lemma nummul: "\<And> i. Inum bs (nummul i t) = Inum bs (Mul i t)"
   428 by (induct t rule: nummul.induct, auto simp add: algebra_simps numadd)
   429 
   430 lemma nummul_nb: "\<And> i. numbound0 t \<Longrightarrow> numbound0 (nummul i t)"
   431 by (induct t rule: nummul.induct, auto simp add: numadd_nb)
   432 
   433 definition numneg :: "num \<Rightarrow> num" where
   434   "numneg t \<equiv> nummul (- 1) t"
   435 
   436 definition numsub :: "num \<Rightarrow> num \<Rightarrow> num" where
   437   "numsub s t \<equiv> (if s = t then C 0 else numadd (s, numneg t))"
   438 
   439 lemma numneg: "Inum bs (numneg t) = Inum bs (Neg t)"
   440 using numneg_def nummul by simp
   441 
   442 lemma numneg_nb: "numbound0 t \<Longrightarrow> numbound0 (numneg t)"
   443 using numneg_def nummul_nb by simp
   444 
   445 lemma numsub: "Inum bs (numsub a b) = Inum bs (Sub a b)"
   446 using numneg numadd numsub_def by simp
   447 
   448 lemma numsub_nb: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numsub t s)"
   449 using numsub_def numadd_nb numneg_nb by simp
   450 
   451 fun
   452   simpnum :: "num \<Rightarrow> num"
   453 where
   454   "simpnum (C j) = C j"
   455   | "simpnum (Bound n) = CN n 1 (C 0)"
   456   | "simpnum (Neg t) = numneg (simpnum t)"
   457   | "simpnum (Add t s) = numadd (simpnum t, simpnum s)"
   458   | "simpnum (Sub t s) = numsub (simpnum t) (simpnum s)"
   459   | "simpnum (Mul i t) = (if i = 0 then C 0 else nummul i (simpnum t))"
   460   | "simpnum t = t"
   461 
   462 lemma simpnum_ci: "Inum bs (simpnum t) = Inum bs t"
   463 by (induct t rule: simpnum.induct, auto simp add: numneg numadd numsub nummul)
   464 
   465 lemma simpnum_numbound0: 
   466   "numbound0 t \<Longrightarrow> numbound0 (simpnum t)"
   467 by (induct t rule: simpnum.induct, auto simp add: numadd_nb numsub_nb nummul_nb numneg_nb)
   468 
   469 fun
   470   not :: "fm \<Rightarrow> fm"
   471 where
   472   "not (NOT p) = p"
   473   | "not T = F"
   474   | "not F = T"
   475   | "not p = NOT p"
   476 lemma not: "Ifm bbs bs (not p) = Ifm bbs bs (NOT p)"
   477   by (cases p) auto
   478 lemma not_qf: "qfree p \<Longrightarrow> qfree (not p)"
   479   by (cases p) auto
   480 lemma not_bn: "bound0 p \<Longrightarrow> bound0 (not p)"
   481   by (cases p) auto
   482 
   483 definition conj :: "fm \<Rightarrow> fm \<Rightarrow> fm" where
   484   "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)"
   485 lemma conj: "Ifm bbs bs (conj p q) = Ifm bbs bs (And p q)"
   486 by (cases "p=F \<or> q=F",simp_all add: conj_def) (cases p,simp_all)
   487 
   488 lemma conj_qf: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (conj p q)"
   489 using conj_def by auto 
   490 lemma conj_nb: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (conj p q)"
   491 using conj_def by auto 
   492 
   493 definition disj :: "fm \<Rightarrow> fm \<Rightarrow> fm" where
   494   "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)"
   495 
   496 lemma disj: "Ifm bbs bs (disj p q) = Ifm bbs bs (Or p q)"
   497 by (cases "p=T \<or> q=T",simp_all add: disj_def) (cases p,simp_all)
   498 lemma disj_qf: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (disj p q)"
   499 using disj_def by auto 
   500 lemma disj_nb: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (disj p q)"
   501 using disj_def by auto 
   502 
   503 definition imp :: "fm \<Rightarrow> fm \<Rightarrow> fm" where
   504   "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)"
   505 lemma imp: "Ifm bbs bs (imp p q) = Ifm bbs bs (Imp p q)"
   506 by (cases "p=F \<or> q=T",simp_all add: imp_def,cases p) (simp_all add: not)
   507 lemma imp_qf: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (imp p q)"
   508 using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def,cases p) (simp_all add: not_qf) 
   509 lemma imp_nb: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (imp p q)"
   510 using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def,cases p) simp_all
   511 
   512 definition iff :: "fm \<Rightarrow> fm \<Rightarrow> fm" where
   513   "iff p q \<equiv> (if (p = q) then T else if (p = not q \<or> not p = q) then F else 
   514        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 
   515   Iff p q)"
   516 lemma iff: "Ifm bbs bs (iff p q) = Ifm bbs bs (Iff p q)"
   517   by (unfold iff_def,cases "p=q", simp,cases "p=not q", simp add:not) 
   518 (cases "not p= q", auto simp add:not)
   519 lemma iff_qf: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (iff p q)"
   520   by (unfold iff_def,cases "p=q", auto simp add: not_qf)
   521 lemma iff_nb: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (iff p q)"
   522 using iff_def by (unfold iff_def,cases "p=q", auto simp add: not_bn)
   523 
   524 function (sequential)
   525   simpfm :: "fm \<Rightarrow> fm"
   526 where
   527   "simpfm (And p q) = conj (simpfm p) (simpfm q)"
   528   | "simpfm (Or p q) = disj (simpfm p) (simpfm q)"
   529   | "simpfm (Imp p q) = imp (simpfm p) (simpfm q)"
   530   | "simpfm (Iff p q) = iff (simpfm p) (simpfm q)"
   531   | "simpfm (NOT p) = not (simpfm p)"
   532   | "simpfm (Lt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v < 0) then T else F 
   533       | _ \<Rightarrow> Lt a')"
   534   | "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')"
   535   | "simpfm (Gt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v > 0)  then T else F | _ \<Rightarrow> Gt a')"
   536   | "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')"
   537   | "simpfm (Eq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v = 0)  then T else F | _ \<Rightarrow> Eq a')"
   538   | "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')"
   539   | "simpfm (Dvd i a) = (if i=0 then simpfm (Eq a)
   540              else if (abs i = 1) then T
   541              else let a' = simpnum a in case a' of C v \<Rightarrow> if (i dvd v)  then T else F | _ \<Rightarrow> Dvd i a')"
   542   | "simpfm (NDvd i a) = (if i=0 then simpfm (NEq a) 
   543              else if (abs i = 1) then F
   544              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')"
   545   | "simpfm p = p"
   546 by pat_completeness auto
   547 termination by (relation "measure fmsize") auto
   548 
   549 lemma simpfm: "Ifm bbs bs (simpfm p) = Ifm bbs bs p"
   550 proof(induct p rule: simpfm.induct)
   551   case (6 a) let ?sa = "simpnum a" from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
   552   {fix v assume "?sa = C v" hence ?case using sa by simp }
   553   moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa 
   554       by (cases ?sa, simp_all add: Let_def)}
   555   ultimately show ?case by blast
   556 next
   557   case (7 a)  let ?sa = "simpnum a" 
   558   from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
   559   {fix v assume "?sa = C v" hence ?case using sa by simp }
   560   moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa 
   561       by (cases ?sa, simp_all add: Let_def)}
   562   ultimately show ?case by blast
   563 next
   564   case (8 a)  let ?sa = "simpnum a" 
   565   from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
   566   {fix v assume "?sa = C v" hence ?case using sa by simp }
   567   moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa 
   568       by (cases ?sa, simp_all add: Let_def)}
   569   ultimately show ?case by blast
   570 next
   571   case (9 a)  let ?sa = "simpnum a" 
   572   from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
   573   {fix v assume "?sa = C v" hence ?case using sa by simp }
   574   moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa 
   575       by (cases ?sa, simp_all add: Let_def)}
   576   ultimately show ?case by blast
   577 next
   578   case (10 a)  let ?sa = "simpnum a" 
   579   from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
   580   {fix v assume "?sa = C v" hence ?case using sa by simp }
   581   moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa 
   582       by (cases ?sa, simp_all add: Let_def)}
   583   ultimately show ?case by blast
   584 next
   585   case (11 a)  let ?sa = "simpnum a" 
   586   from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp
   587   {fix v assume "?sa = C v" hence ?case using sa by simp }
   588   moreover {assume "\<not> (\<exists> v. ?sa = C v)" hence ?case using sa 
   589       by (cases ?sa, simp_all add: Let_def)}
   590   ultimately show ?case by blast
   591 next
   592   case (12 i a)  let ?sa = "simpnum a" from simpnum_ci 
   593   have sa: "Inum bs ?sa = Inum bs a" by simp
   594   have "i=0 \<or> abs i = 1 \<or> (i\<noteq>0 \<and> (abs i \<noteq> 1))" by auto
   595   {assume "i=0" hence ?case using "12.hyps" by (simp add: dvd_def Let_def)}
   596   moreover 
   597   {assume i1: "abs i = 1"
   598       from one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
   599       have ?case using i1 apply (cases "i=0", simp_all add: Let_def) 
   600         by (cases "i > 0", simp_all)}
   601   moreover   
   602   {assume inz: "i\<noteq>0" and cond: "abs i \<noteq> 1"
   603     {fix v assume "?sa = C v" hence ?case using sa[symmetric] inz cond
   604         by (cases "abs i = 1", auto) }
   605     moreover {assume "\<not> (\<exists> v. ?sa = C v)" 
   606       hence "simpfm (Dvd i a) = Dvd i ?sa" using inz cond 
   607         by (cases ?sa, auto simp add: Let_def)
   608       hence ?case using sa by simp}
   609     ultimately have ?case by blast}
   610   ultimately show ?case by blast
   611 next
   612   case (13 i a)  let ?sa = "simpnum a" from simpnum_ci 
   613   have sa: "Inum bs ?sa = Inum bs a" by simp
   614   have "i=0 \<or> abs i = 1 \<or> (i\<noteq>0 \<and> (abs i \<noteq> 1))" by auto
   615   {assume "i=0" hence ?case using "13.hyps" by (simp add: dvd_def Let_def)}
   616   moreover 
   617   {assume i1: "abs i = 1"
   618       from one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
   619       have ?case using i1 apply (cases "i=0", simp_all add: Let_def)
   620       apply (cases "i > 0", simp_all) done}
   621   moreover   
   622   {assume inz: "i\<noteq>0" and cond: "abs i \<noteq> 1"
   623     {fix v assume "?sa = C v" hence ?case using sa[symmetric] inz cond
   624         by (cases "abs i = 1", auto) }
   625     moreover {assume "\<not> (\<exists> v. ?sa = C v)" 
   626       hence "simpfm (NDvd i a) = NDvd i ?sa" using inz cond 
   627         by (cases ?sa, auto simp add: Let_def)
   628       hence ?case using sa by simp}
   629     ultimately have ?case by blast}
   630   ultimately show ?case by blast
   631 qed (induct p rule: simpfm.induct, simp_all add: conj disj imp iff not)
   632 
   633 lemma simpfm_bound0: "bound0 p \<Longrightarrow> bound0 (simpfm p)"
   634 proof(induct p rule: simpfm.induct)
   635   case (6 a) hence nb: "numbound0 a" by simp
   636   hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
   637   thus ?case by (cases "simpnum a", auto simp add: Let_def)
   638 next
   639   case (7 a) hence nb: "numbound0 a" by simp
   640   hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
   641   thus ?case by (cases "simpnum a", auto simp add: Let_def)
   642 next
   643   case (8 a) hence nb: "numbound0 a" by simp
   644   hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
   645   thus ?case by (cases "simpnum a", auto simp add: Let_def)
   646 next
   647   case (9 a) hence nb: "numbound0 a" by simp
   648   hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
   649   thus ?case by (cases "simpnum a", auto simp add: Let_def)
   650 next
   651   case (10 a) hence nb: "numbound0 a" by simp
   652   hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
   653   thus ?case by (cases "simpnum a", auto simp add: Let_def)
   654 next
   655   case (11 a) hence nb: "numbound0 a" by simp
   656   hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
   657   thus ?case by (cases "simpnum a", auto simp add: Let_def)
   658 next
   659   case (12 i a) hence nb: "numbound0 a" by simp
   660   hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
   661   thus ?case by (cases "simpnum a", auto simp add: Let_def)
   662 next
   663   case (13 i a) hence nb: "numbound0 a" by simp
   664   hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
   665   thus ?case by (cases "simpnum a", auto simp add: Let_def)
   666 qed(auto simp add: disj_def imp_def iff_def conj_def not_bn)
   667 
   668 lemma simpfm_qf: "qfree p \<Longrightarrow> qfree (simpfm p)"
   669 by (induct p rule: simpfm.induct, auto simp add: disj_qf imp_qf iff_qf conj_qf not_qf Let_def)
   670  (case_tac "simpnum a",auto)+
   671 
   672   (* Generic quantifier elimination *)
   673 function (sequential) qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm" where
   674   "qelim (E p) = (\<lambda> qe. DJ qe (qelim p qe))"
   675 | "qelim (A p) = (\<lambda> qe. not (qe ((qelim (NOT p) qe))))"
   676 | "qelim (NOT p) = (\<lambda> qe. not (qelim p qe))"
   677 | "qelim (And p q) = (\<lambda> qe. conj (qelim p qe) (qelim q qe))" 
   678 | "qelim (Or  p q) = (\<lambda> qe. disj (qelim p qe) (qelim q qe))" 
   679 | "qelim (Imp p q) = (\<lambda> qe. imp (qelim p qe) (qelim q qe))"
   680 | "qelim (Iff p q) = (\<lambda> qe. iff (qelim p qe) (qelim q qe))"
   681 | "qelim p = (\<lambda> y. simpfm p)"
   682 by pat_completeness auto
   683 termination by (relation "measure fmsize") auto
   684 
   685 lemma qelim_ci:
   686   assumes qe_inv: "\<forall> bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bbs bs (qe p) = Ifm bbs bs (E p))"
   687   shows "\<And> bs. qfree (qelim p qe) \<and> (Ifm bbs bs (qelim p qe) = Ifm bbs bs p)"
   688 using qe_inv DJ_qe[OF qe_inv] 
   689 by(induct p rule: qelim.induct) 
   690 (auto simp add: not disj conj iff imp not_qf disj_qf conj_qf imp_qf iff_qf 
   691   simpfm simpfm_qf simp del: simpfm.simps)
   692   (* Linearity for fm where Bound 0 ranges over \<int> *)
   693 
   694 fun zsplit0 :: "num \<Rightarrow> int \<times> num" (* splits the bounded from the unbounded part*)
   695 where
   696   "zsplit0 (C c) = (0,C c)"
   697   | "zsplit0 (Bound n) = (if n=0 then (1, C 0) else (0,Bound n))"
   698   | "zsplit0 (CN n i a) = 
   699       (let (i',a') =  zsplit0 a 
   700        in if n=0 then (i+i', a') else (i',CN n i a'))"
   701   | "zsplit0 (Neg a) = (let (i',a') =  zsplit0 a in (-i', Neg a'))"
   702   | "zsplit0 (Add a b) = (let (ia,a') =  zsplit0 a ; 
   703                             (ib,b') =  zsplit0 b 
   704                             in (ia+ib, Add a' b'))"
   705   | "zsplit0 (Sub a b) = (let (ia,a') =  zsplit0 a ; 
   706                             (ib,b') =  zsplit0 b 
   707                             in (ia-ib, Sub a' b'))"
   708   | "zsplit0 (Mul i a) = (let (i',a') =  zsplit0 a in (i*i', Mul i a'))"
   709 
   710 lemma zsplit0_I:
   711   shows "\<And> n a. zsplit0 t = (n,a) \<Longrightarrow> (Inum ((x::int) #bs) (CN 0 n a) = Inum (x #bs) t) \<and> numbound0 a"
   712   (is "\<And> n a. ?S t = (n,a) \<Longrightarrow> (?I x (CN 0 n a) = ?I x t) \<and> ?N a")
   713 proof(induct t rule: zsplit0.induct)
   714   case (1 c n a) thus ?case by auto 
   715 next
   716   case (2 m n a) thus ?case by (cases "m=0") auto
   717 next
   718   case (3 m i a n a')
   719   let ?j = "fst (zsplit0 a)"
   720   let ?b = "snd (zsplit0 a)"
   721   have abj: "zsplit0 a = (?j,?b)" by simp 
   722   {assume "m\<noteq>0" 
   723     with 3(1)[OF abj] 3(2) have ?case by (auto simp add: Let_def split_def)}
   724   moreover
   725   {assume m0: "m =0"
   726     with abj have th: "a'=?b \<and> n=i+?j" using 3 
   727       by (simp add: Let_def split_def)
   728     from abj 3 m0 have th2: "(?I x (CN 0 ?j ?b) = ?I x a) \<and> ?N ?b" by blast
   729     from th have "?I x (CN 0 n a') = ?I x (CN 0 (i+?j) ?b)" by simp
   730     also from th2 have "\<dots> = ?I x (CN 0 i (CN 0 ?j ?b))" by (simp add: distrib_right)
   731   finally have "?I x (CN 0 n a') = ?I  x (CN 0 i a)" using th2 by simp
   732   with th2 th have ?case using m0 by blast} 
   733 ultimately show ?case by blast
   734 next
   735   case (4 t n a)
   736   let ?nt = "fst (zsplit0 t)"
   737   let ?at = "snd (zsplit0 t)"
   738   have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Neg ?at \<and> n=-?nt" using 4
   739     by (simp add: Let_def split_def)
   740   from abj 4 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
   741   from th2[simplified] th[simplified] show ?case by simp
   742 next
   743   case (5 s t n a)
   744   let ?ns = "fst (zsplit0 s)"
   745   let ?as = "snd (zsplit0 s)"
   746   let ?nt = "fst (zsplit0 t)"
   747   let ?at = "snd (zsplit0 t)"
   748   have abjs: "zsplit0 s = (?ns,?as)" by simp 
   749   moreover have abjt:  "zsplit0 t = (?nt,?at)" by simp 
   750   ultimately have th: "a=Add ?as ?at \<and> n=?ns + ?nt" using 5
   751     by (simp add: Let_def split_def)
   752   from abjs[symmetric] have bluddy: "\<exists> x y. (x,y) = zsplit0 s" by blast
   753   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
   754   with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
   755   from abjs 5 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast
   756   from th3[simplified] th2[simplified] th[simplified] show ?case 
   757     by (simp add: distrib_right)
   758 next
   759   case (6 s t n a)
   760   let ?ns = "fst (zsplit0 s)"
   761   let ?as = "snd (zsplit0 s)"
   762   let ?nt = "fst (zsplit0 t)"
   763   let ?at = "snd (zsplit0 t)"
   764   have abjs: "zsplit0 s = (?ns,?as)" by simp 
   765   moreover have abjt:  "zsplit0 t = (?nt,?at)" by simp 
   766   ultimately have th: "a=Sub ?as ?at \<and> n=?ns - ?nt" using 6
   767     by (simp add: Let_def split_def)
   768   from abjs[symmetric] have bluddy: "\<exists> x y. (x,y) = zsplit0 s" by blast
   769   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
   770   with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
   771   from abjs 6 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast
   772   from th3[simplified] th2[simplified] th[simplified] show ?case 
   773     by (simp add: left_diff_distrib)
   774 next
   775   case (7 i t n a)
   776   let ?nt = "fst (zsplit0 t)"
   777   let ?at = "snd (zsplit0 t)"
   778   have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Mul i ?at \<and> n=i*?nt" using 7
   779     by (simp add: Let_def split_def)
   780   from abj 7 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast
   781   hence "?I x (Mul i t) = i * ?I x (CN 0 ?nt ?at)" by simp
   782   also have "\<dots> = ?I x (CN 0 (i*?nt) (Mul i ?at))" by (simp add: distrib_left)
   783   finally show ?case using th th2 by simp
   784 qed
   785 
   786 consts
   787   iszlfm :: "fm \<Rightarrow> bool"   (* Linearity test for fm *)
   788 recdef iszlfm "measure size"
   789   "iszlfm (And p q) = (iszlfm p \<and> iszlfm q)" 
   790   "iszlfm (Or p q) = (iszlfm p \<and> iszlfm q)" 
   791   "iszlfm (Eq  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
   792   "iszlfm (NEq (CN 0 c e)) = (c>0 \<and> numbound0 e)"
   793   "iszlfm (Lt  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
   794   "iszlfm (Le  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
   795   "iszlfm (Gt  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
   796   "iszlfm (Ge  (CN 0 c e)) = ( c>0 \<and> numbound0 e)"
   797   "iszlfm (Dvd i (CN 0 c e)) = 
   798                  (c>0 \<and> i>0 \<and> numbound0 e)"
   799   "iszlfm (NDvd i (CN 0 c e))= 
   800                  (c>0 \<and> i>0 \<and> numbound0 e)"
   801   "iszlfm p = (isatom p \<and> (bound0 p))"
   802 
   803 lemma zlin_qfree: "iszlfm p \<Longrightarrow> qfree p"
   804   by (induct p rule: iszlfm.induct) auto
   805 
   806 consts
   807   zlfm :: "fm \<Rightarrow> fm"       (* Linearity transformation for fm *)
   808 recdef zlfm "measure fmsize"
   809   "zlfm (And p q) = And (zlfm p) (zlfm q)"
   810   "zlfm (Or p q) = Or (zlfm p) (zlfm q)"
   811   "zlfm (Imp p q) = Or (zlfm (NOT p)) (zlfm q)"
   812   "zlfm (Iff p q) = Or (And (zlfm p) (zlfm q)) (And (zlfm (NOT p)) (zlfm (NOT q)))"
   813   "zlfm (Lt a) = (let (c,r) = zsplit0 a in 
   814      if c=0 then Lt r else 
   815      if c>0 then (Lt (CN 0 c r)) else (Gt (CN 0 (- c) (Neg r))))"
   816   "zlfm (Le a) = (let (c,r) = zsplit0 a in 
   817      if c=0 then Le r else 
   818      if c>0 then (Le (CN 0 c r)) else (Ge (CN 0 (- c) (Neg r))))"
   819   "zlfm (Gt a) = (let (c,r) = zsplit0 a in 
   820      if c=0 then Gt r else 
   821      if c>0 then (Gt (CN 0 c r)) else (Lt (CN 0 (- c) (Neg r))))"
   822   "zlfm (Ge a) = (let (c,r) = zsplit0 a in 
   823      if c=0 then Ge r else 
   824      if c>0 then (Ge (CN 0 c r)) else (Le (CN 0 (- c) (Neg r))))"
   825   "zlfm (Eq a) = (let (c,r) = zsplit0 a in 
   826      if c=0 then Eq r else 
   827      if c>0 then (Eq (CN 0 c r)) else (Eq (CN 0 (- c) (Neg r))))"
   828   "zlfm (NEq a) = (let (c,r) = zsplit0 a in 
   829      if c=0 then NEq r else 
   830      if c>0 then (NEq (CN 0 c r)) else (NEq (CN 0 (- c) (Neg r))))"
   831   "zlfm (Dvd i a) = (if i=0 then zlfm (Eq a) 
   832         else (let (c,r) = zsplit0 a in 
   833               if c=0 then (Dvd (abs i) r) else 
   834       if c>0 then (Dvd (abs i) (CN 0 c r))
   835       else (Dvd (abs i) (CN 0 (- c) (Neg r)))))"
   836   "zlfm (NDvd i a) = (if i=0 then zlfm (NEq a) 
   837         else (let (c,r) = zsplit0 a in 
   838               if c=0 then (NDvd (abs i) r) else 
   839       if c>0 then (NDvd (abs i) (CN 0 c r))
   840       else (NDvd (abs i) (CN 0 (- c) (Neg r)))))"
   841   "zlfm (NOT (And p q)) = Or (zlfm (NOT p)) (zlfm (NOT q))"
   842   "zlfm (NOT (Or p q)) = And (zlfm (NOT p)) (zlfm (NOT q))"
   843   "zlfm (NOT (Imp p q)) = And (zlfm p) (zlfm (NOT q))"
   844   "zlfm (NOT (Iff p q)) = Or (And(zlfm p) (zlfm(NOT q))) (And (zlfm(NOT p)) (zlfm q))"
   845   "zlfm (NOT (NOT p)) = zlfm p"
   846   "zlfm (NOT T) = F"
   847   "zlfm (NOT F) = T"
   848   "zlfm (NOT (Lt a)) = zlfm (Ge a)"
   849   "zlfm (NOT (Le a)) = zlfm (Gt a)"
   850   "zlfm (NOT (Gt a)) = zlfm (Le a)"
   851   "zlfm (NOT (Ge a)) = zlfm (Lt a)"
   852   "zlfm (NOT (Eq a)) = zlfm (NEq a)"
   853   "zlfm (NOT (NEq a)) = zlfm (Eq a)"
   854   "zlfm (NOT (Dvd i a)) = zlfm (NDvd i a)"
   855   "zlfm (NOT (NDvd i a)) = zlfm (Dvd i a)"
   856   "zlfm (NOT (Closed P)) = NClosed P"
   857   "zlfm (NOT (NClosed P)) = Closed P"
   858   "zlfm p = p" (hints simp add: fmsize_pos)
   859 
   860 lemma zlfm_I:
   861   assumes qfp: "qfree p"
   862   shows "(Ifm bbs (i#bs) (zlfm p) = Ifm bbs (i# bs) p) \<and> iszlfm (zlfm p)"
   863   (is "(?I (?l p) = ?I p) \<and> ?L (?l p)")
   864 using qfp
   865 proof(induct p rule: zlfm.induct)
   866   case (5 a) 
   867   let ?c = "fst (zsplit0 a)"
   868   let ?r = "snd (zsplit0 a)"
   869   have spl: "zsplit0 a = (?c,?r)" by simp
   870   from zsplit0_I[OF spl, where x="i" and bs="bs"] 
   871   have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 
   872   let ?N = "\<lambda> t. Inum (i#bs) t"
   873   from 5 Ia nb  show ?case 
   874     apply (auto simp add: Let_def split_def algebra_simps) 
   875     apply (cases "?r", auto)
   876     apply (case_tac nat, auto)
   877     done
   878 next
   879   case (6 a)  
   880   let ?c = "fst (zsplit0 a)"
   881   let ?r = "snd (zsplit0 a)"
   882   have spl: "zsplit0 a = (?c,?r)" by simp
   883   from zsplit0_I[OF spl, where x="i" and bs="bs"] 
   884   have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 
   885   let ?N = "\<lambda> t. Inum (i#bs) t"
   886   from 6 Ia nb show ?case 
   887     apply (auto simp add: Let_def split_def algebra_simps) 
   888     apply (cases "?r", auto)
   889     apply (case_tac nat, auto)
   890     done
   891 next
   892   case (7 a)  
   893   let ?c = "fst (zsplit0 a)"
   894   let ?r = "snd (zsplit0 a)"
   895   have spl: "zsplit0 a = (?c,?r)" by simp
   896   from zsplit0_I[OF spl, where x="i" and bs="bs"] 
   897   have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 
   898   let ?N = "\<lambda> t. Inum (i#bs) t"
   899   from 7 Ia nb show ?case 
   900     apply (auto simp add: Let_def split_def algebra_simps) 
   901     apply (cases "?r", auto)
   902     apply (case_tac nat, auto)
   903     done
   904 next
   905   case (8 a)  
   906   let ?c = "fst (zsplit0 a)"
   907   let ?r = "snd (zsplit0 a)"
   908   have spl: "zsplit0 a = (?c,?r)" by simp
   909   from zsplit0_I[OF spl, where x="i" and bs="bs"] 
   910   have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 
   911   let ?N = "\<lambda> t. Inum (i#bs) t"
   912   from 8 Ia nb  show ?case
   913     apply (auto simp add: Let_def split_def algebra_simps) 
   914     apply (cases "?r", auto)
   915     apply (case_tac nat, auto)
   916     done
   917 next
   918   case (9 a)  
   919   let ?c = "fst (zsplit0 a)"
   920   let ?r = "snd (zsplit0 a)"
   921   have spl: "zsplit0 a = (?c,?r)" by simp
   922   from zsplit0_I[OF spl, where x="i" and bs="bs"] 
   923   have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 
   924   let ?N = "\<lambda> t. Inum (i#bs) t"
   925   from 9 Ia nb  show ?case
   926     apply (auto simp add: Let_def split_def algebra_simps) 
   927     apply (cases "?r", auto)
   928     apply (case_tac nat, auto)
   929     done
   930 next
   931   case (10 a)  
   932   let ?c = "fst (zsplit0 a)"
   933   let ?r = "snd (zsplit0 a)"
   934   have spl: "zsplit0 a = (?c,?r)" by simp
   935   from zsplit0_I[OF spl, where x="i" and bs="bs"] 
   936   have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 
   937   let ?N = "\<lambda> t. Inum (i#bs) t"
   938   from 10 Ia nb  show ?case
   939     apply (auto simp add: Let_def split_def algebra_simps) 
   940     apply (cases "?r",auto)
   941     apply (case_tac nat, auto)
   942     done
   943 next
   944   case (11 j a)  
   945   let ?c = "fst (zsplit0 a)"
   946   let ?r = "snd (zsplit0 a)"
   947   have spl: "zsplit0 a = (?c,?r)" by simp
   948   from zsplit0_I[OF spl, where x="i" and bs="bs"] 
   949   have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 
   950   let ?N = "\<lambda> t. Inum (i#bs) t"
   951   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
   952   moreover
   953   {assume "j=0" hence z: "zlfm (Dvd j a) = (zlfm (Eq a))" by (simp add: Let_def) 
   954     hence ?case using 11 `j = 0` by (simp del: zlfm.simps) }
   955   moreover
   956   {assume "?c=0" and "j\<noteq>0" hence ?case 
   957       using zsplit0_I[OF spl, where x="i" and bs="bs"]
   958     apply (auto simp add: Let_def split_def algebra_simps) 
   959     apply (cases "?r",auto)
   960     apply (case_tac nat, auto)
   961     done}
   962   moreover
   963   {assume cp: "?c > 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))" 
   964       by (simp add: nb Let_def split_def)
   965     hence ?case using Ia cp jnz by (simp add: Let_def split_def)}
   966   moreover
   967   {assume cn: "?c < 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))" 
   968       by (simp add: nb Let_def split_def)
   969     hence ?case using Ia cn jnz dvd_minus_iff[of "abs j" "?c*i + ?N ?r" ]
   970       by (simp add: Let_def split_def) }
   971   ultimately show ?case by blast
   972 next
   973   case (12 j a) 
   974   let ?c = "fst (zsplit0 a)"
   975   let ?r = "snd (zsplit0 a)"
   976   have spl: "zsplit0 a = (?c,?r)" by simp
   977   from zsplit0_I[OF spl, where x="i" and bs="bs"] 
   978   have Ia:"Inum (i # bs) a = Inum (i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 
   979   let ?N = "\<lambda> t. Inum (i#bs) t"
   980   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
   981   moreover
   982   {assume "j=0" hence z: "zlfm (NDvd j a) = (zlfm (NEq a))" by (simp add: Let_def) 
   983     hence ?case using assms 12 `j = 0` by (simp del: zlfm.simps)}
   984   moreover
   985   {assume "?c=0" and "j\<noteq>0" hence ?case 
   986       using zsplit0_I[OF spl, where x="i" and bs="bs"]
   987     apply (auto simp add: Let_def split_def algebra_simps) 
   988     apply (cases "?r",auto)
   989     apply (case_tac nat, auto)
   990     done}
   991   moreover
   992   {assume cp: "?c > 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))" 
   993       by (simp add: nb Let_def split_def)
   994     hence ?case using Ia cp jnz by (simp add: Let_def split_def) }
   995   moreover
   996   {assume cn: "?c < 0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))" 
   997       by (simp add: nb Let_def split_def)
   998     hence ?case using Ia cn jnz dvd_minus_iff[of "abs j" "?c*i + ?N ?r"]
   999       by (simp add: Let_def split_def)}
  1000   ultimately show ?case by blast
  1001 qed auto
  1002 
  1003 consts 
  1004   plusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of +\<infinity>*)
  1005   minusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of -\<infinity>*)
  1006   \<delta> :: "fm \<Rightarrow> int" (* Compute lcm {d| N\<^isup>? Dvd c*x+t \<in> p}*)
  1007   d_\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool" (* checks if a given l divides all the ds above*)
  1008 
  1009 recdef minusinf "measure size"
  1010   "minusinf (And p q) = And (minusinf p) (minusinf q)" 
  1011   "minusinf (Or p q) = Or (minusinf p) (minusinf q)" 
  1012   "minusinf (Eq  (CN 0 c e)) = F"
  1013   "minusinf (NEq (CN 0 c e)) = T"
  1014   "minusinf (Lt  (CN 0 c e)) = T"
  1015   "minusinf (Le  (CN 0 c e)) = T"
  1016   "minusinf (Gt  (CN 0 c e)) = F"
  1017   "minusinf (Ge  (CN 0 c e)) = F"
  1018   "minusinf p = p"
  1019 
  1020 lemma minusinf_qfree: "qfree p \<Longrightarrow> qfree (minusinf p)"
  1021   by (induct p rule: minusinf.induct, auto)
  1022 
  1023 recdef plusinf "measure size"
  1024   "plusinf (And p q) = And (plusinf p) (plusinf q)" 
  1025   "plusinf (Or p q) = Or (plusinf p) (plusinf q)" 
  1026   "plusinf (Eq  (CN 0 c e)) = F"
  1027   "plusinf (NEq (CN 0 c e)) = T"
  1028   "plusinf (Lt  (CN 0 c e)) = F"
  1029   "plusinf (Le  (CN 0 c e)) = F"
  1030   "plusinf (Gt  (CN 0 c e)) = T"
  1031   "plusinf (Ge  (CN 0 c e)) = T"
  1032   "plusinf p = p"
  1033 
  1034 recdef \<delta> "measure size"
  1035   "\<delta> (And p q) = lcm (\<delta> p) (\<delta> q)" 
  1036   "\<delta> (Or p q) = lcm (\<delta> p) (\<delta> q)" 
  1037   "\<delta> (Dvd i (CN 0 c e)) = i"
  1038   "\<delta> (NDvd i (CN 0 c e)) = i"
  1039   "\<delta> p = 1"
  1040 
  1041 recdef d_\<delta> "measure size"
  1042   "d_\<delta> (And p q) = (\<lambda> d. d_\<delta> p d \<and> d_\<delta> q d)" 
  1043   "d_\<delta> (Or p q) = (\<lambda> d. d_\<delta> p d \<and> d_\<delta> q d)" 
  1044   "d_\<delta> (Dvd i (CN 0 c e)) = (\<lambda> d. i dvd d)"
  1045   "d_\<delta> (NDvd i (CN 0 c e)) = (\<lambda> d. i dvd d)"
  1046   "d_\<delta> p = (\<lambda> d. True)"
  1047 
  1048 lemma delta_mono: 
  1049   assumes lin: "iszlfm p"
  1050   and d: "d dvd d'"
  1051   and ad: "d_\<delta> p d"
  1052   shows "d_\<delta> p d'"
  1053   using lin ad d
  1054 proof(induct p rule: iszlfm.induct)
  1055   case (9 i c e)  thus ?case using d
  1056     by (simp add: dvd_trans[of "i" "d" "d'"])
  1057 next
  1058   case (10 i c e) thus ?case using d
  1059     by (simp add: dvd_trans[of "i" "d" "d'"])
  1060 qed simp_all
  1061 
  1062 lemma \<delta> : assumes lin:"iszlfm p"
  1063   shows "d_\<delta> p (\<delta> p) \<and> \<delta> p >0"
  1064 using lin
  1065 proof (induct p rule: iszlfm.induct)
  1066   case (1 p q) 
  1067   let ?d = "\<delta> (And p q)"
  1068   from 1 lcm_pos_int have dp: "?d >0" by simp
  1069   have d1: "\<delta> p dvd \<delta> (And p q)" using 1 by simp
  1070   hence th: "d_\<delta> p ?d" using delta_mono 1(2,3) by(simp only: iszlfm.simps)
  1071   have "\<delta> q dvd \<delta> (And p q)" using 1 by simp
  1072   hence th': "d_\<delta> q ?d" using delta_mono 1 by(simp only: iszlfm.simps)
  1073   from th th' dp show ?case by simp
  1074 next
  1075   case (2 p q)  
  1076   let ?d = "\<delta> (And p q)"
  1077   from 2 lcm_pos_int have dp: "?d >0" by simp
  1078   have "\<delta> p dvd \<delta> (And p q)" using 2 by simp
  1079   hence th: "d_\<delta> p ?d" using delta_mono 2 by(simp only: iszlfm.simps)
  1080   have "\<delta> q dvd \<delta> (And p q)" using 2 by simp
  1081   hence th': "d_\<delta> q ?d" using delta_mono 2 by(simp only: iszlfm.simps)
  1082   from th th' dp show ?case by simp
  1083 qed simp_all
  1084 
  1085 
  1086 consts 
  1087   a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" (* adjusts the coeffitients of a formula *)
  1088   d_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool" (* tests if all coeffs c of c divide a given l*)
  1089   \<zeta>  :: "fm \<Rightarrow> int" (* computes the lcm of all coefficients of x*)
  1090   \<beta> :: "fm \<Rightarrow> num list"
  1091   \<alpha> :: "fm \<Rightarrow> num list"
  1092 
  1093 recdef a_\<beta> "measure size"
  1094   "a_\<beta> (And p q) = (\<lambda> k. And (a_\<beta> p k) (a_\<beta> q k))" 
  1095   "a_\<beta> (Or p q) = (\<lambda> k. Or (a_\<beta> p k) (a_\<beta> q k))" 
  1096   "a_\<beta> (Eq  (CN 0 c e)) = (\<lambda> k. Eq (CN 0 1 (Mul (k div c) e)))"
  1097   "a_\<beta> (NEq (CN 0 c e)) = (\<lambda> k. NEq (CN 0 1 (Mul (k div c) e)))"
  1098   "a_\<beta> (Lt  (CN 0 c e)) = (\<lambda> k. Lt (CN 0 1 (Mul (k div c) e)))"
  1099   "a_\<beta> (Le  (CN 0 c e)) = (\<lambda> k. Le (CN 0 1 (Mul (k div c) e)))"
  1100   "a_\<beta> (Gt  (CN 0 c e)) = (\<lambda> k. Gt (CN 0 1 (Mul (k div c) e)))"
  1101   "a_\<beta> (Ge  (CN 0 c e)) = (\<lambda> k. Ge (CN 0 1 (Mul (k div c) e)))"
  1102   "a_\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
  1103   "a_\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
  1104   "a_\<beta> p = (\<lambda> k. p)"
  1105 
  1106 recdef d_\<beta> "measure size"
  1107   "d_\<beta> (And p q) = (\<lambda> k. (d_\<beta> p k) \<and> (d_\<beta> q k))" 
  1108   "d_\<beta> (Or p q) = (\<lambda> k. (d_\<beta> p k) \<and> (d_\<beta> q k))" 
  1109   "d_\<beta> (Eq  (CN 0 c e)) = (\<lambda> k. c dvd k)"
  1110   "d_\<beta> (NEq (CN 0 c e)) = (\<lambda> k. c dvd k)"
  1111   "d_\<beta> (Lt  (CN 0 c e)) = (\<lambda> k. c dvd k)"
  1112   "d_\<beta> (Le  (CN 0 c e)) = (\<lambda> k. c dvd k)"
  1113   "d_\<beta> (Gt  (CN 0 c e)) = (\<lambda> k. c dvd k)"
  1114   "d_\<beta> (Ge  (CN 0 c e)) = (\<lambda> k. c dvd k)"
  1115   "d_\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. c dvd k)"
  1116   "d_\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. c dvd k)"
  1117   "d_\<beta> p = (\<lambda> k. True)"
  1118 
  1119 recdef \<zeta> "measure size"
  1120   "\<zeta> (And p q) = lcm (\<zeta> p) (\<zeta> q)" 
  1121   "\<zeta> (Or p q) = lcm (\<zeta> p) (\<zeta> q)" 
  1122   "\<zeta> (Eq  (CN 0 c e)) = c"
  1123   "\<zeta> (NEq (CN 0 c e)) = c"
  1124   "\<zeta> (Lt  (CN 0 c e)) = c"
  1125   "\<zeta> (Le  (CN 0 c e)) = c"
  1126   "\<zeta> (Gt  (CN 0 c e)) = c"
  1127   "\<zeta> (Ge  (CN 0 c e)) = c"
  1128   "\<zeta> (Dvd i (CN 0 c e)) = c"
  1129   "\<zeta> (NDvd i (CN 0 c e))= c"
  1130   "\<zeta> p = 1"
  1131 
  1132 recdef \<beta> "measure size"
  1133   "\<beta> (And p q) = (\<beta> p @ \<beta> q)" 
  1134   "\<beta> (Or p q) = (\<beta> p @ \<beta> q)" 
  1135   "\<beta> (Eq  (CN 0 c e)) = [Sub (C -1) e]"
  1136   "\<beta> (NEq (CN 0 c e)) = [Neg e]"
  1137   "\<beta> (Lt  (CN 0 c e)) = []"
  1138   "\<beta> (Le  (CN 0 c e)) = []"
  1139   "\<beta> (Gt  (CN 0 c e)) = [Neg e]"
  1140   "\<beta> (Ge  (CN 0 c e)) = [Sub (C -1) e]"
  1141   "\<beta> p = []"
  1142 
  1143 recdef \<alpha> "measure size"
  1144   "\<alpha> (And p q) = (\<alpha> p @ \<alpha> q)" 
  1145   "\<alpha> (Or p q) = (\<alpha> p @ \<alpha> q)" 
  1146   "\<alpha> (Eq  (CN 0 c e)) = [Add (C -1) e]"
  1147   "\<alpha> (NEq (CN 0 c e)) = [e]"
  1148   "\<alpha> (Lt  (CN 0 c e)) = [e]"
  1149   "\<alpha> (Le  (CN 0 c e)) = [Add (C -1) e]"
  1150   "\<alpha> (Gt  (CN 0 c e)) = []"
  1151   "\<alpha> (Ge  (CN 0 c e)) = []"
  1152   "\<alpha> p = []"
  1153 consts mirror :: "fm \<Rightarrow> fm"
  1154 recdef mirror "measure size"
  1155   "mirror (And p q) = And (mirror p) (mirror q)" 
  1156   "mirror (Or p q) = Or (mirror p) (mirror q)" 
  1157   "mirror (Eq  (CN 0 c e)) = Eq (CN 0 c (Neg e))"
  1158   "mirror (NEq (CN 0 c e)) = NEq (CN 0 c (Neg e))"
  1159   "mirror (Lt  (CN 0 c e)) = Gt (CN 0 c (Neg e))"
  1160   "mirror (Le  (CN 0 c e)) = Ge (CN 0 c (Neg e))"
  1161   "mirror (Gt  (CN 0 c e)) = Lt (CN 0 c (Neg e))"
  1162   "mirror (Ge  (CN 0 c e)) = Le (CN 0 c (Neg e))"
  1163   "mirror (Dvd i (CN 0 c e)) = Dvd i (CN 0 c (Neg e))"
  1164   "mirror (NDvd i (CN 0 c e)) = NDvd i (CN 0 c (Neg e))"
  1165   "mirror p = p"
  1166     (* Lemmas for the correctness of \<sigma>\<rho> *)
  1167 lemma dvd1_eq1: "x >0 \<Longrightarrow> (x::int) dvd 1 = (x = 1)"
  1168   by simp
  1169 
  1170 lemma minusinf_inf:
  1171   assumes linp: "iszlfm p"
  1172   and u: "d_\<beta> p 1"
  1173   shows "\<exists> (z::int). \<forall> x < z. Ifm bbs (x#bs) (minusinf p) = Ifm bbs (x#bs) p"
  1174   (is "?P p" is "\<exists> (z::int). \<forall> x < z. ?I x (?M p) = ?I x p")
  1175 using linp u
  1176 proof (induct p rule: minusinf.induct)
  1177   case (1 p q) thus ?case 
  1178     by auto (rule_tac x="min z za" in exI,simp)
  1179 next
  1180   case (2 p q) thus ?case 
  1181     by auto (rule_tac x="min z za" in exI,simp)
  1182 next
  1183   case (3 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
  1184   fix a
  1185   from 3 have "\<forall> x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<noteq> 0"
  1186   proof(clarsimp)
  1187     fix x assume "x < (- Inum (a#bs) e)" and"x + Inum (x#bs) e = 0"
  1188     with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
  1189     show "False" by simp
  1190   qed
  1191   thus ?case by auto
  1192 next
  1193   case (4 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
  1194   fix a
  1195   from 4 have "\<forall> x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<noteq> 0"
  1196   proof(clarsimp)
  1197     fix x assume "x < (- Inum (a#bs) e)" and"x + Inum (x#bs) e = 0"
  1198     with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
  1199     show "False" by simp
  1200   qed
  1201   thus ?case by auto
  1202 next
  1203   case (5 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
  1204   fix a
  1205   from 5 have "\<forall> x<(- Inum (a#bs) e). c*x + Inum (x#bs) e < 0"
  1206   proof(clarsimp)
  1207     fix x assume "x < (- Inum (a#bs) e)" 
  1208     with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
  1209     show "x + Inum (x#bs) e < 0" by simp
  1210   qed
  1211   thus ?case by auto
  1212 next
  1213   case (6 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
  1214   fix a
  1215   from 6 have "\<forall> x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<le> 0"
  1216   proof(clarsimp)
  1217     fix x assume "x < (- Inum (a#bs) e)" 
  1218     with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
  1219     show "x + Inum (x#bs) e \<le> 0" by simp
  1220   qed
  1221   thus ?case by auto
  1222 next
  1223   case (7 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
  1224   fix a
  1225   from 7 have "\<forall> x<(- Inum (a#bs) e). \<not> (c*x + Inum (x#bs) e > 0)"
  1226   proof(clarsimp)
  1227     fix x assume "x < (- Inum (a#bs) e)" and"x + Inum (x#bs) e > 0"
  1228     with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
  1229     show "False" by simp
  1230   qed
  1231   thus ?case by auto
  1232 next
  1233   case (8 c e) hence c1: "c=1" and nb: "numbound0 e" by simp+
  1234   fix a
  1235   from 8 have "\<forall> x<(- Inum (a#bs) e). \<not> (c*x + Inum (x#bs) e \<ge> 0)"
  1236   proof(clarsimp)
  1237     fix x assume "x < (- Inum (a#bs) e)" and"x + Inum (x#bs) e \<ge> 0"
  1238     with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"]
  1239     show "False" by simp
  1240   qed
  1241   thus ?case by auto
  1242 qed auto
  1243 
  1244 lemma minusinf_repeats:
  1245   assumes d: "d_\<delta> p d" and linp: "iszlfm p"
  1246   shows "Ifm bbs ((x - k*d)#bs) (minusinf p) = Ifm bbs (x #bs) (minusinf p)"
  1247 using linp d
  1248 proof(induct p rule: iszlfm.induct) 
  1249   case (9 i c e) hence nbe: "numbound0 e"  and id: "i dvd d" by simp+
  1250     hence "\<exists> k. d=i*k" by (simp add: dvd_def)
  1251     then obtain "di" where di_def: "d=i*di" by blast
  1252     show ?case 
  1253     proof(simp add: numbound0_I[OF nbe,where bs="bs" and b="x - k * d" and b'="x"] right_diff_distrib, rule iffI)
  1254       assume 
  1255         "i dvd c * x - c*(k*d) + Inum (x # bs) e"
  1256       (is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt")
  1257       hence "\<exists> (l::int). ?rt = i * l" by (simp add: dvd_def)
  1258       hence "\<exists> (l::int). c*x+ ?I x e = i*l+c*(k * i*di)" 
  1259         by (simp add: algebra_simps di_def)
  1260       hence "\<exists> (l::int). c*x+ ?I x e = i*(l + c*k*di)"
  1261         by (simp add: algebra_simps)
  1262       hence "\<exists> (l::int). c*x+ ?I x e = i*l" by blast
  1263       thus "i dvd c*x + Inum (x # bs) e" by (simp add: dvd_def) 
  1264     next
  1265       assume 
  1266         "i dvd c*x + Inum (x # bs) e" (is "?ri dvd ?rc*?rx+?e")
  1267       hence "\<exists> (l::int). c*x+?e = i*l" by (simp add: dvd_def)
  1268       hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*l - c*(k*d)" by simp
  1269       hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*l - c*(k*i*di)" by (simp add: di_def)
  1270       hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: algebra_simps)
  1271       hence "\<exists> (l::int). c*x - c * (k*d) +?e = i*l"
  1272         by blast
  1273       thus "i dvd c*x - c*(k*d) + Inum (x # bs) e" by (simp add: dvd_def)
  1274     qed
  1275 next
  1276   case (10 i c e)  hence nbe: "numbound0 e"  and id: "i dvd d" by simp+
  1277     hence "\<exists> k. d=i*k" by (simp add: dvd_def)
  1278     then obtain "di" where di_def: "d=i*di" by blast
  1279     show ?case 
  1280     proof(simp add: numbound0_I[OF nbe,where bs="bs" and b="x - k * d" and b'="x"] right_diff_distrib, rule iffI)
  1281       assume 
  1282         "i dvd c * x - c*(k*d) + Inum (x # bs) e"
  1283       (is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt")
  1284       hence "\<exists> (l::int). ?rt = i * l" by (simp add: dvd_def)
  1285       hence "\<exists> (l::int). c*x+ ?I x e = i*l+c*(k * i*di)" 
  1286         by (simp add: algebra_simps di_def)
  1287       hence "\<exists> (l::int). c*x+ ?I x e = i*(l + c*k*di)"
  1288         by (simp add: algebra_simps)
  1289       hence "\<exists> (l::int). c*x+ ?I x e = i*l" by blast
  1290       thus "i dvd c*x + Inum (x # bs) e" by (simp add: dvd_def) 
  1291     next
  1292       assume 
  1293         "i dvd c*x + Inum (x # bs) e" (is "?ri dvd ?rc*?rx+?e")
  1294       hence "\<exists> (l::int). c*x+?e = i*l" by (simp add: dvd_def)
  1295       hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*l - c*(k*d)" by simp
  1296       hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*l - c*(k*i*di)" by (simp add: di_def)
  1297       hence "\<exists> (l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: algebra_simps)
  1298       hence "\<exists> (l::int). c*x - c * (k*d) +?e = i*l"
  1299         by blast
  1300       thus "i dvd c*x - c*(k*d) + Inum (x # bs) e" by (simp add: dvd_def)
  1301     qed
  1302 qed (auto simp add: gr0_conv_Suc numbound0_I[where bs="bs" and b="x - k*d" and b'="x"])
  1303 
  1304 lemma mirror_\<alpha>_\<beta>:
  1305   assumes lp: "iszlfm p"
  1306   shows "(Inum (i#bs)) ` set (\<alpha> p) = (Inum (i#bs)) ` set (\<beta> (mirror p))"
  1307 using lp
  1308 by (induct p rule: mirror.induct, auto)
  1309 
  1310 lemma mirror: 
  1311   assumes lp: "iszlfm p"
  1312   shows "Ifm bbs (x#bs) (mirror p) = Ifm bbs ((- x)#bs) p" 
  1313 using lp
  1314 proof(induct p rule: iszlfm.induct)
  1315   case (9 j c e) hence nb: "numbound0 e" by simp
  1316   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
  1317     also have "\<dots> = (j dvd (- (c*x - ?e)))"
  1318     by (simp only: dvd_minus_iff)
  1319   also have "\<dots> = (j dvd (c* (- x)) + ?e)"
  1320     apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_minus add_ac minus_add_distrib)
  1321     by (simp add: algebra_simps)
  1322   also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))"
  1323     using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"]
  1324     by simp
  1325   finally show ?case .
  1326 next
  1327     case (10 j c e) hence nb: "numbound0 e" by simp
  1328   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
  1329     also have "\<dots> = (j dvd (- (c*x - ?e)))"
  1330     by (simp only: dvd_minus_iff)
  1331   also have "\<dots> = (j dvd (c* (- x)) + ?e)"
  1332     apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_minus add_ac minus_add_distrib)
  1333     by (simp add: algebra_simps)
  1334   also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))"
  1335     using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"]
  1336     by simp
  1337   finally show ?case by simp
  1338 qed (auto simp add: numbound0_I[where bs="bs" and b="x" and b'="- x"] gr0_conv_Suc)
  1339 
  1340 lemma mirror_l: "iszlfm p \<and> d_\<beta> p 1 
  1341   \<Longrightarrow> iszlfm (mirror p) \<and> d_\<beta> (mirror p) 1"
  1342   by (induct p rule: mirror.induct) auto
  1343 
  1344 lemma mirror_\<delta>: "iszlfm p \<Longrightarrow> \<delta> (mirror p) = \<delta> p"
  1345   by (induct p rule: mirror.induct) auto
  1346 
  1347 lemma \<beta>_numbound0: assumes lp: "iszlfm p"
  1348   shows "\<forall> b\<in> set (\<beta> p). numbound0 b"
  1349   using lp by (induct p rule: \<beta>.induct) auto
  1350 
  1351 lemma d_\<beta>_mono: 
  1352   assumes linp: "iszlfm p"
  1353   and dr: "d_\<beta> p l"
  1354   and d: "l dvd l'"
  1355   shows "d_\<beta> p l'"
  1356 using dr linp dvd_trans[of _ "l" "l'", simplified d]
  1357   by (induct p rule: iszlfm.induct) simp_all
  1358 
  1359 lemma \<alpha>_l: assumes lp: "iszlfm p"
  1360   shows "\<forall> b\<in> set (\<alpha> p). numbound0 b"
  1361 using lp
  1362   by(induct p rule: \<alpha>.induct) auto
  1363 
  1364 lemma \<zeta>: 
  1365   assumes linp: "iszlfm p"
  1366   shows "\<zeta> p > 0 \<and> d_\<beta> p (\<zeta> p)"
  1367 using linp
  1368 proof(induct p rule: iszlfm.induct)
  1369   case (1 p q)
  1370   from 1 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
  1371   from 1 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
  1372   from 1 d_\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
  1373     d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
  1374     dl1 dl2 show ?case by (auto simp add: lcm_pos_int)
  1375 next
  1376   case (2 p q)
  1377   from 2 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
  1378   from 2 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
  1379   from 2 d_\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
  1380     d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
  1381     dl1 dl2 show ?case by (auto simp add: lcm_pos_int)
  1382 qed (auto simp add: lcm_pos_int)
  1383 
  1384 lemma a_\<beta>: assumes linp: "iszlfm p" and d: "d_\<beta> p l" and lp: "l > 0"
  1385   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)"
  1386 using linp d
  1387 proof (induct p rule: iszlfm.induct)
  1388   case (5 c e) hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp+
  1389     from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
  1390     from cp have cnz: "c \<noteq> 0" by simp
  1391     have "c div c\<le> l div c"
  1392       by (simp add: zdiv_mono1[OF clel cp])
  1393     then have ldcp:"0 < l div c" 
  1394       by (simp add: div_self[OF cnz])
  1395     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
  1396     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
  1397       by simp
  1398     hence "(l*x + (l div c) * Inum (x # bs) e < 0) =
  1399           ((c * (l div c)) * x + (l div c) * Inum (x # bs) e < 0)"
  1400       by simp
  1401     also have "\<dots> = ((l div c) * (c*x + Inum (x # bs) e) < (l div c) * 0)" by (simp add: algebra_simps)
  1402     also have "\<dots> = (c*x + Inum (x # bs) e < 0)"
  1403     using mult_less_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp by simp
  1404   finally show ?case using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be  by simp
  1405 next
  1406   case (6 c e) hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp+
  1407     from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
  1408     from cp have cnz: "c \<noteq> 0" by simp
  1409     have "c div c\<le> l div c"
  1410       by (simp add: zdiv_mono1[OF clel cp])
  1411     then have ldcp:"0 < l div c" 
  1412       by (simp add: div_self[OF cnz])
  1413     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
  1414     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
  1415       by simp
  1416     hence "(l*x + (l div c) * Inum (x# bs) e \<le> 0) =
  1417           ((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<le> 0)"
  1418       by simp
  1419     also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<le> ((l div c)) * 0)" by (simp add: algebra_simps)
  1420     also have "\<dots> = (c*x + Inum (x # bs) e \<le> 0)"
  1421     using mult_le_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp by simp
  1422   finally show ?case using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"]  be by simp
  1423 next
  1424   case (7 c e) hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp+
  1425     from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
  1426     from cp have cnz: "c \<noteq> 0" by simp
  1427     have "c div c\<le> l div c"
  1428       by (simp add: zdiv_mono1[OF clel cp])
  1429     then have ldcp:"0 < l div c" 
  1430       by (simp add: div_self[OF cnz])
  1431     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
  1432     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
  1433       by simp
  1434     hence "(l*x + (l div c)* Inum (x # bs) e > 0) =
  1435           ((c * (l div c)) * x + (l div c) * Inum (x # bs) e > 0)"
  1436       by simp
  1437     also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) > ((l div c)) * 0)" by (simp add: algebra_simps)
  1438     also have "\<dots> = (c * x + Inum (x # bs) e > 0)"
  1439     using zero_less_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp by simp
  1440   finally show ?case using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"]  be  by simp
  1441 next
  1442   case (8 c e) hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp+
  1443     from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
  1444     from cp have cnz: "c \<noteq> 0" by simp
  1445     have "c div c\<le> l div c"
  1446       by (simp add: zdiv_mono1[OF clel cp])
  1447     then have ldcp:"0 < l div c" 
  1448       by (simp add: div_self[OF cnz])
  1449     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
  1450     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
  1451       by simp
  1452     hence "(l*x + (l div c)* Inum (x # bs) e \<ge> 0) =
  1453           ((c*(l div c))*x + (l div c)* Inum (x # bs) e \<ge> 0)"
  1454       by simp
  1455     also have "\<dots> = ((l div c)*(c*x + Inum (x # bs) e) \<ge> ((l div c)) * 0)" 
  1456       by (simp add: algebra_simps)
  1457     also have "\<dots> = (c*x + Inum (x # bs) e \<ge> 0)" using ldcp 
  1458       zero_le_mult_iff [where a="l div c" and b="c*x + Inum (x # bs) e"] by simp
  1459   finally show ?case using be numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"]  
  1460     by simp
  1461 next
  1462   case (3 c e) hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp+
  1463     from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
  1464     from cp have cnz: "c \<noteq> 0" by simp
  1465     have "c div c\<le> l div c"
  1466       by (simp add: zdiv_mono1[OF clel cp])
  1467     then have ldcp:"0 < l div c" 
  1468       by (simp add: div_self[OF cnz])
  1469     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
  1470     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
  1471       by simp
  1472     hence "(l * x + (l div c) * Inum (x # bs) e = 0) =
  1473           ((c * (l div c)) * x + (l div c) * Inum (x # bs) e = 0)"
  1474       by simp
  1475     also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) = ((l div c)) * 0)" by (simp add: algebra_simps)
  1476     also have "\<dots> = (c * x + Inum (x # bs) e = 0)"
  1477     using mult_eq_0_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp by simp
  1478   finally show ?case using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"]  be  by simp
  1479 next
  1480   case (4 c e) hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp+
  1481     from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
  1482     from cp have cnz: "c \<noteq> 0" by simp
  1483     have "c div c\<le> l div c"
  1484       by (simp add: zdiv_mono1[OF clel cp])
  1485     then have ldcp:"0 < l div c" 
  1486       by (simp add: div_self[OF cnz])
  1487     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
  1488     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
  1489       by simp
  1490     hence "(l * x + (l div c) * Inum (x # bs) e \<noteq> 0) =
  1491           ((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<noteq> 0)"
  1492       by simp
  1493     also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<noteq> ((l div c)) * 0)" by (simp add: algebra_simps)
  1494     also have "\<dots> = (c * x + Inum (x # bs) e \<noteq> 0)"
  1495     using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp by simp
  1496   finally show ?case using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"]  be  by simp
  1497 next
  1498   case (9 j c e) hence cp: "c>0" and be: "numbound0 e" and jp: "j > 0" and d': "c dvd l" by simp+
  1499     from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
  1500     from cp have cnz: "c \<noteq> 0" by simp
  1501     have "c div c\<le> l div c"
  1502       by (simp add: zdiv_mono1[OF clel cp])
  1503     then have ldcp:"0 < l div c" 
  1504       by (simp add: div_self[OF cnz])
  1505     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
  1506     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
  1507       by simp
  1508     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
  1509     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)
  1510     also fix k have "\<dots> = (\<exists> (k::int). c * x + Inum (x # bs) e - j * k = 0)"
  1511     using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp by simp
  1512   also have "\<dots> = (\<exists> (k::int). c * x + Inum (x # bs) e = j * k)" by simp
  1513   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)
  1514 next
  1515   case (10 j c e) hence cp: "c>0" and be: "numbound0 e" and jp: "j > 0" and d': "c dvd l" by simp+
  1516     from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])
  1517     from cp have cnz: "c \<noteq> 0" by simp
  1518     have "c div c\<le> l div c"
  1519       by (simp add: zdiv_mono1[OF clel cp])
  1520     then have ldcp:"0 < l div c" 
  1521       by (simp add: div_self[OF cnz])
  1522     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp
  1523     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 
  1524       by simp
  1525     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
  1526     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)
  1527     also fix k have "\<dots> = (\<exists> (k::int). c * x + Inum (x # bs) e - j * k = 0)"
  1528     using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp by simp
  1529   also have "\<dots> = (\<exists> (k::int). c * x + Inum (x # bs) e = j * k)" by simp
  1530   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)
  1531 qed (auto simp add: gr0_conv_Suc numbound0_I[where bs="bs" and b="(l * x)" and b'="x"])
  1532 
  1533 lemma a_\<beta>_ex: assumes linp: "iszlfm p" and d: "d_\<beta> p l" and lp: "l>0"
  1534   shows "(\<exists> x. l dvd x \<and> Ifm bbs (x #bs) (a_\<beta> p l)) = (\<exists> (x::int). Ifm bbs (x#bs) p)"
  1535   (is "(\<exists> x. l dvd x \<and> ?P x) = (\<exists> x. ?P' x)")
  1536 proof-
  1537   have "(\<exists> x. l dvd x \<and> ?P x) = (\<exists> (x::int). ?P (l*x))"
  1538     using unity_coeff_ex[where l="l" and P="?P", simplified] by simp
  1539   also have "\<dots> = (\<exists> (x::int). ?P' x)" using a_\<beta>[OF linp d lp] by simp
  1540   finally show ?thesis  . 
  1541 qed
  1542 
  1543 lemma \<beta>:
  1544   assumes lp: "iszlfm p"
  1545   and u: "d_\<beta> p 1"
  1546   and d: "d_\<delta> p d"
  1547   and dp: "d > 0"
  1548   and nob: "\<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists> b\<in> (Inum (a#bs)) ` set(\<beta> p). x = b + j)"
  1549   and p: "Ifm bbs (x#bs) p" (is "?P x")
  1550   shows "?P (x - d)"
  1551 using lp u d dp nob p
  1552 proof(induct p rule: iszlfm.induct)
  1553   case (5 c e) hence c1: "c=1" and  bn:"numbound0 e" by simp_all
  1554   with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] 5
  1555   show ?case by simp
  1556 next
  1557   case (6 c e)  hence c1: "c=1" and  bn:"numbound0 e" by simp_all
  1558   with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] 6
  1559   show ?case by simp
  1560 next
  1561   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
  1562   let ?e = "Inum (x # bs) e"
  1563   {assume "(x-d) +?e > 0" hence ?case using c1 
  1564     numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] by simp}
  1565   moreover
  1566   {assume H: "\<not> (x-d) + ?e > 0" 
  1567     let ?v="Neg e"
  1568     have vb: "?v \<in> set (\<beta> (Gt (CN 0 c e)))" by simp
  1569     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"]] 
  1570     have nob: "\<not> (\<exists> j\<in> {1 ..d}. x =  - ?e + j)" by auto 
  1571     from H p have "x + ?e > 0 \<and> x + ?e \<le> d" by (simp add: c1)
  1572     hence "x + ?e \<ge> 1 \<and> x + ?e \<le> d"  by simp
  1573     hence "\<exists> (j::int) \<in> {1 .. d}. j = x + ?e" by simp
  1574     hence "\<exists> (j::int) \<in> {1 .. d}. x = (- ?e + j)" 
  1575       by (simp add: algebra_simps)
  1576     with nob have ?case by auto}
  1577   ultimately show ?case by blast
  1578 next
  1579   case (8 c e) hence p: "Ifm bbs (x #bs) (Ge (CN 0 c e))" and c1: "c=1" and bn:"numbound0 e" 
  1580     by simp+
  1581     let ?e = "Inum (x # bs) e"
  1582     {assume "(x-d) +?e \<ge> 0" hence ?case using  c1 
  1583       numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"]
  1584         by simp}
  1585     moreover
  1586     {assume H: "\<not> (x-d) + ?e \<ge> 0" 
  1587       let ?v="Sub (C -1) e"
  1588       have vb: "?v \<in> set (\<beta> (Ge (CN 0 c e)))" by simp
  1589       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"]] 
  1590       have nob: "\<not> (\<exists> j\<in> {1 ..d}. x =  - ?e - 1 + j)" by auto 
  1591       from H p have "x + ?e \<ge> 0 \<and> x + ?e < d" by (simp add: c1)
  1592       hence "x + ?e +1 \<ge> 1 \<and> x + ?e + 1 \<le> d"  by simp
  1593       hence "\<exists> (j::int) \<in> {1 .. d}. j = x + ?e + 1" by simp
  1594       hence "\<exists> (j::int) \<in> {1 .. d}. x= - ?e - 1 + j" by (simp add: algebra_simps)
  1595       with nob have ?case by simp }
  1596     ultimately show ?case by blast
  1597 next
  1598   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+
  1599     let ?e = "Inum (x # bs) e"
  1600     let ?v="(Sub (C -1) e)"
  1601     have vb: "?v \<in> set (\<beta> (Eq (CN 0 c e)))" by simp
  1602     from p have "x= - ?e" by (simp add: c1) with 3(5) show ?case using dp
  1603       by simp (erule ballE[where x="1"],
  1604         simp_all add:algebra_simps numbound0_I[OF bn,where b="x"and b'="a"and bs="bs"])
  1605 next
  1606   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+
  1607     let ?e = "Inum (x # bs) e"
  1608     let ?v="Neg e"
  1609     have vb: "?v \<in> set (\<beta> (NEq (CN 0 c e)))" by simp
  1610     {assume "x - d + Inum (((x -d)) # bs) e \<noteq> 0" 
  1611       hence ?case by (simp add: c1)}
  1612     moreover
  1613     {assume H: "x - d + Inum (((x -d)) # bs) e = 0"
  1614       hence "x = - Inum (((x -d)) # bs) e + d" by simp
  1615       hence "x = - Inum (a # bs) e + d"
  1616         by (simp add: numbound0_I[OF bn,where b="x - d"and b'="a"and bs="bs"])
  1617        with 4(5) have ?case using dp by simp}
  1618   ultimately show ?case by blast
  1619 next 
  1620   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+
  1621     let ?e = "Inum (x # bs) e"
  1622     from 9 have id: "j dvd d" by simp
  1623     from c1 have "?p x = (j dvd (x+ ?e))" by simp
  1624     also have "\<dots> = (j dvd x - d + ?e)" 
  1625       using zdvd_period[OF id, where x="x" and c="-1" and t="?e"] by simp
  1626     finally show ?case 
  1627       using numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] c1 p by simp
  1628 next
  1629   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+
  1630     let ?e = "Inum (x # bs) e"
  1631     from 10 have id: "j dvd d" by simp
  1632     from c1 have "?p x = (\<not> j dvd (x+ ?e))" by simp
  1633     also have "\<dots> = (\<not> j dvd x - d + ?e)" 
  1634       using zdvd_period[OF id, where x="x" and c="-1" and t="?e"] by simp
  1635     finally show ?case using numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] c1 p by simp
  1636 qed (auto simp add: numbound0_I[where bs="bs" and b="(x - d)" and b'="x"] gr0_conv_Suc)
  1637 
  1638 lemma \<beta>':   
  1639   assumes lp: "iszlfm p"
  1640   and u: "d_\<beta> p 1"
  1641   and d: "d_\<delta> p d"
  1642   and dp: "d > 0"
  1643   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)")
  1644 proof(clarify)
  1645   fix x 
  1646   assume nb:"?b" and px: "?P x" 
  1647   hence nb2: "\<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists> b\<in> (Inum (a#bs)) ` set(\<beta> p). x = b + j)"
  1648     by auto
  1649   from  \<beta>[OF lp u d dp nb2 px] show "?P (x -d )" .
  1650 qed
  1651 lemma cpmi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. x < z --> (P x = P1 x))
  1652 ==> ALL x.~(EX (j::int) : {1..D}. EX (b::int) : B. P(b+j)) --> P (x) --> P (x - D) 
  1653 ==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x-k*D))))
  1654 ==> (EX (x::int). P(x)) = ((EX (j::int) : {1..D} . (P1(j))) | (EX (j::int) : {1..D}. EX (b::int) : B. P (b+j)))"
  1655 apply(rule iffI)
  1656 prefer 2
  1657 apply(drule minusinfinity)
  1658 apply assumption+
  1659 apply(fastforce)
  1660 apply clarsimp
  1661 apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x - k*D)")
  1662 apply(frule_tac x = x and z=z in decr_lemma)
  1663 apply(subgoal_tac "P1(x - (\<bar>x - z\<bar> + 1) * D)")
  1664 prefer 2
  1665 apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)")
  1666 prefer 2 apply arith
  1667  apply fastforce
  1668 apply(drule (1)  periodic_finite_ex)
  1669 apply blast
  1670 apply(blast dest:decr_mult_lemma)
  1671 done
  1672 
  1673 theorem cp_thm:
  1674   assumes lp: "iszlfm p"
  1675   and u: "d_\<beta> p 1"
  1676   and d: "d_\<delta> p d"
  1677   and dp: "d > 0"
  1678   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))"
  1679   (is "(\<exists> (x::int). ?P (x)) = (\<exists> j\<in> ?D. ?M j \<or> (\<exists> b\<in> ?B. ?P (?I b + j)))")
  1680 proof-
  1681   from minusinf_inf[OF lp u] 
  1682   have th: "\<exists>(z::int). \<forall>x<z. ?P (x) = ?M x" by blast
  1683   let ?B' = "{?I b | b. b\<in> ?B}"
  1684   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
  1685   hence th2: "\<forall> x. \<not> (\<exists> j \<in> ?D. \<exists> b \<in> ?B'. ?P ((b + j))) \<longrightarrow> ?P (x) \<longrightarrow> ?P ((x - d))" 
  1686     using \<beta>'[OF lp u d dp, where a="i" and bbs = "bbs"] by blast
  1687   from minusinf_repeats[OF d lp]
  1688   have th3: "\<forall> x k. ?M x = ?M (x-k*d)" by simp
  1689   from cpmi_eq[OF dp th th2 th3] BB' show ?thesis by blast
  1690 qed
  1691 
  1692     (* Implement the right hand sides of Cooper's theorem and Ferrante and Rackoff. *)
  1693 lemma mirror_ex: 
  1694   assumes lp: "iszlfm p"
  1695   shows "(\<exists> x. Ifm bbs (x#bs) (mirror p)) = (\<exists> x. Ifm bbs (x#bs) p)"
  1696   (is "(\<exists> x. ?I x ?mp) = (\<exists> x. ?I x p)")
  1697 proof(auto)
  1698   fix x assume "?I x ?mp" hence "?I (- x) p" using mirror[OF lp] by blast
  1699   thus "\<exists> x. ?I x p" by blast
  1700 next
  1701   fix x assume "?I x p" hence "?I (- x) ?mp" 
  1702     using mirror[OF lp, where x="- x", symmetric] by auto
  1703   thus "\<exists> x. ?I x ?mp" by blast
  1704 qed
  1705 
  1706 
  1707 lemma cp_thm': 
  1708   assumes lp: "iszlfm p"
  1709   and up: "d_\<beta> p 1" and dd: "d_\<delta> p d" and dp: "d > 0"
  1710   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))"
  1711   using cp_thm[OF lp up dd dp,where i="i"] by auto
  1712 
  1713 definition unit :: "fm \<Rightarrow> fm \<times> num list \<times> int" where
  1714   "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;
  1715              B = remdups (map simpnum (\<beta> q)) ; a = remdups (map simpnum (\<alpha> q))
  1716              in if length B \<le> length a then (q,B,d) else (mirror q, a,d))"
  1717 
  1718 lemma unit: assumes qf: "qfree p"
  1719   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)"
  1720 proof-
  1721   fix q B d 
  1722   assume qBd: "unit p = (q,B,d)"
  1723   let ?thes = "((\<exists> x. Ifm bbs (x#bs) p) = (\<exists> x. Ifm bbs (x#bs) q)) \<and>
  1724     Inum (i#bs) ` set B = Inum (i#bs) ` set (\<beta> q) \<and>
  1725     d_\<beta> q 1 \<and> d_\<delta> q d \<and> 0 < d \<and> iszlfm q \<and> (\<forall> b\<in> set B. numbound0 b)"
  1726   let ?I = "\<lambda> x p. Ifm bbs (x#bs) p"
  1727   let ?p' = "zlfm p"
  1728   let ?l = "\<zeta> ?p'"
  1729   let ?q = "And (Dvd ?l (CN 0 1 (C 0))) (a_\<beta> ?p' ?l)"
  1730   let ?d = "\<delta> ?q"
  1731   let ?B = "set (\<beta> ?q)"
  1732   let ?B'= "remdups (map simpnum (\<beta> ?q))"
  1733   let ?A = "set (\<alpha> ?q)"
  1734   let ?A'= "remdups (map simpnum (\<alpha> ?q))"
  1735   from conjunct1[OF zlfm_I[OF qf, where bs="bs"]] 
  1736   have pp': "\<forall> i. ?I i ?p' = ?I i p" by auto
  1737   from conjunct2[OF zlfm_I[OF qf, where bs="bs" and i="i"]]
  1738   have lp': "iszlfm ?p'" . 
  1739   from lp' \<zeta>[where p="?p'"] have lp: "?l >0" and dl: "d_\<beta> ?p' ?l" by auto
  1740   from a_\<beta>_ex[where p="?p'" and l="?l" and bs="bs", OF lp' dl lp] pp'
  1741   have pq_ex:"(\<exists> (x::int). ?I x p) = (\<exists> x. ?I x ?q)" by simp 
  1742   from lp' lp a_\<beta>[OF lp' dl lp] have lq:"iszlfm ?q" and uq: "d_\<beta> ?q 1"  by auto
  1743   from \<delta>[OF lq] have dp:"?d >0" and dd: "d_\<delta> ?q ?d" by blast+
  1744   let ?N = "\<lambda> t. Inum (i#bs) t"
  1745   have "?N ` set ?B' = ((?N o simpnum) ` ?B)" by auto 
  1746   also have "\<dots> = ?N ` ?B" using simpnum_ci[where bs="i#bs"] by auto
  1747   finally have BB': "?N ` set ?B' = ?N ` ?B" .
  1748   have "?N ` set ?A' = ((?N o simpnum) ` ?A)" by auto 
  1749   also have "\<dots> = ?N ` ?A" using simpnum_ci[where bs="i#bs"] by auto
  1750   finally have AA': "?N ` set ?A' = ?N ` ?A" .
  1751   from \<beta>_numbound0[OF lq] have B_nb:"\<forall> b\<in> set ?B'. numbound0 b"
  1752     by (simp add: simpnum_numbound0)
  1753   from \<alpha>_l[OF lq] have A_nb: "\<forall> b\<in> set ?A'. numbound0 b"
  1754     by (simp add: simpnum_numbound0)
  1755     {assume "length ?B' \<le> length ?A'"
  1756     hence q:"q=?q" and "B = ?B'" and d:"d = ?d"
  1757       using qBd by (auto simp add: Let_def unit_def)
  1758     with BB' B_nb have b: "?N ` (set B) = ?N ` set (\<beta> q)" 
  1759       and bn: "\<forall>b\<in> set B. numbound0 b" by simp+ 
  1760   with pq_ex dp uq dd lq q d have ?thes by simp}
  1761   moreover 
  1762   {assume "\<not> (length ?B' \<le> length ?A')"
  1763     hence q:"q=mirror ?q" and "B = ?A'" and d:"d = ?d"
  1764       using qBd by (auto simp add: Let_def unit_def)
  1765     with AA' mirror_\<alpha>_\<beta>[OF lq] A_nb have b:"?N ` (set B) = ?N ` set (\<beta> q)" 
  1766       and bn: "\<forall>b\<in> set B. numbound0 b" by simp+
  1767     from mirror_ex[OF lq] pq_ex q 
  1768     have pqm_eq:"(\<exists> (x::int). ?I x p) = (\<exists> (x::int). ?I x q)" by simp
  1769     from lq uq q mirror_l[where p="?q"]
  1770     have lq': "iszlfm q" and uq: "d_\<beta> q 1" by auto
  1771     from \<delta>[OF lq'] mirror_\<delta>[OF lq] q d have dq:"d_\<delta> q d " by auto
  1772     from pqm_eq b bn uq lq' dp dq q dp d have ?thes by simp
  1773   }
  1774   ultimately show ?thes by blast
  1775 qed
  1776     (* Cooper's Algorithm *)
  1777 
  1778 definition cooper :: "fm \<Rightarrow> fm" where
  1779   "cooper p \<equiv> 
  1780   (let (q,B,d) = unit p; js = [1..d];
  1781        mq = simpfm (minusinf q);
  1782        md = evaldjf (\<lambda> j. simpfm (subst0 (C j) mq)) js
  1783    in if md = T then T else
  1784     (let qd = evaldjf (\<lambda> (b,j). simpfm (subst0 (Add b (C j)) q)) 
  1785                                [(b,j). b\<leftarrow>B,j\<leftarrow>js]
  1786      in decr (disj md qd)))"
  1787 lemma cooper: assumes qf: "qfree p"
  1788   shows "((\<exists> x. Ifm bbs (x#bs) p) = (Ifm bbs bs (cooper p))) \<and> qfree (cooper p)" 
  1789   (is "(?lhs = ?rhs) \<and> _")
  1790 proof-
  1791   let ?I = "\<lambda> x p. Ifm bbs (x#bs) p"
  1792   let ?q = "fst (unit p)"
  1793   let ?B = "fst (snd(unit p))"
  1794   let ?d = "snd (snd (unit p))"
  1795   let ?js = "[1..?d]"
  1796   let ?mq = "minusinf ?q"
  1797   let ?smq = "simpfm ?mq"
  1798   let ?md = "evaldjf (\<lambda> j. simpfm (subst0 (C j) ?smq)) ?js"
  1799   fix i
  1800   let ?N = "\<lambda> t. Inum (i#bs) t"
  1801   let ?Bjs = "[(b,j). b\<leftarrow>?B,j\<leftarrow>?js]"
  1802   let ?qd = "evaldjf (\<lambda> (b,j). simpfm (subst0 (Add b (C j)) ?q)) ?Bjs"
  1803   have qbf:"unit p = (?q,?B,?d)" by simp
  1804   from unit[OF qf qbf] have pq_ex: "(\<exists>(x::int). ?I x p) = (\<exists> (x::int). ?I x ?q)" and 
  1805     B:"?N ` set ?B = ?N ` set (\<beta> ?q)" and 
  1806     uq:"d_\<beta> ?q 1" and dd: "d_\<delta> ?q ?d" and dp: "?d > 0" and 
  1807     lq: "iszlfm ?q" and 
  1808     Bn: "\<forall> b\<in> set ?B. numbound0 b" by auto
  1809   from zlin_qfree[OF lq] have qfq: "qfree ?q" .
  1810   from simpfm_qf[OF minusinf_qfree[OF qfq]] have qfmq: "qfree ?smq".
  1811   have jsnb: "\<forall> j \<in> set ?js. numbound0 (C j)" by simp
  1812   hence "\<forall> j\<in> set ?js. bound0 (subst0 (C j) ?smq)" 
  1813     by (auto simp only: subst0_bound0[OF qfmq])
  1814   hence th: "\<forall> j\<in> set ?js. bound0 (simpfm (subst0 (C j) ?smq))"
  1815     by (auto simp add: simpfm_bound0)
  1816   from evaldjf_bound0[OF th] have mdb: "bound0 ?md" by simp 
  1817   from Bn jsnb have "\<forall> (b,j) \<in> set ?Bjs. numbound0 (Add b (C j))"
  1818     by simp
  1819   hence "\<forall> (b,j) \<in> set ?Bjs. bound0 (subst0 (Add b (C j)) ?q)"
  1820     using subst0_bound0[OF qfq] by blast
  1821   hence "\<forall> (b,j) \<in> set ?Bjs. bound0 (simpfm (subst0 (Add b (C j)) ?q))"
  1822     using simpfm_bound0  by blast
  1823   hence th': "\<forall> x \<in> set ?Bjs. bound0 ((\<lambda> (b,j). simpfm (subst0 (Add b (C j)) ?q)) x)"
  1824     by auto 
  1825   from evaldjf_bound0 [OF th'] have qdb: "bound0 ?qd" by simp
  1826   from mdb qdb 
  1827   have mdqdb: "bound0 (disj ?md ?qd)" by (simp only: disj_def, cases "?md=T \<or> ?qd=T", simp_all)
  1828   from trans [OF pq_ex cp_thm'[OF lq uq dd dp,where i="i"]] B
  1829   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
  1830   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
  1831   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
  1832   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) 
  1833   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))"
  1834     by (simp only: simpfm subst0_I[OF qfmq] set_upto) auto
  1835   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)))" 
  1836    by (simp only: evaldjf_ex subst0_I[OF qfq])
  1837  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)))"
  1838    by (simp only: simpfm set_concat set_map concat_map_singleton UN_simps) blast
  1839  also have "\<dots> = (?I i ?md \<or> (?I i (evaldjf (\<lambda> (b,j). simpfm (subst0 (Add b (C j)) ?q)) ?Bjs)))"
  1840    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)
  1841  finally have mdqd: "?lhs = (?I i ?md \<or> ?I i ?qd)" by simp  
  1842   also have "\<dots> = (?I i (disj ?md ?qd))" by (simp add: disj)
  1843   also have "\<dots> = (Ifm bbs bs (decr (disj ?md ?qd)))" by (simp only: decr [OF mdqdb]) 
  1844   finally have mdqd2: "?lhs = (Ifm bbs bs (decr (disj ?md ?qd)))" . 
  1845   {assume mdT: "?md = T"
  1846     hence cT:"cooper p = T" 
  1847       by (simp only: cooper_def unit_def split_def Let_def if_True) simp
  1848     from mdT have lhs:"?lhs" using mdqd by simp 
  1849     from mdT have "?rhs" by (simp add: cooper_def unit_def split_def)
  1850     with lhs cT have ?thesis by simp }
  1851   moreover
  1852   {assume mdT: "?md \<noteq> T" hence "cooper p = decr (disj ?md ?qd)" 
  1853       by (simp only: cooper_def unit_def split_def Let_def if_False) 
  1854     with mdqd2 decr_qf[OF mdqdb] have ?thesis by simp }
  1855   ultimately show ?thesis by blast
  1856 qed
  1857 
  1858 definition pa :: "fm \<Rightarrow> fm" where
  1859   "pa p = qelim (prep p) cooper"
  1860 
  1861 theorem mirqe: "(Ifm bbs bs (pa p) = Ifm bbs bs p) \<and> qfree (pa p)"
  1862   using qelim_ci cooper prep by (auto simp add: pa_def)
  1863 
  1864 definition
  1865   cooper_test :: "unit \<Rightarrow> fm"
  1866 where
  1867   "cooper_test u = pa (E (A (Imp (Ge (Sub (Bound 0) (Bound 1)))
  1868     (E (E (Eq (Sub (Add (Mul 3 (Bound 1)) (Mul 5 (Bound 0)))
  1869       (Bound 2))))))))"
  1870 
  1871 ML {* @{code cooper_test} () *}
  1872 
  1873 (* code_reflect Cooper_Procedure
  1874   functions pa
  1875   file "~~/src/HOL/Tools/Qelim/cooper_procedure.ML" *)
  1876 
  1877 oracle linzqe_oracle = {*
  1878 let
  1879 
  1880 fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (op =) vs t
  1881      of NONE => error "Variable not found in the list!"
  1882       | SOME n => @{code Bound} n)
  1883   | num_of_term vs @{term "0::int"} = @{code C} 0
  1884   | num_of_term vs @{term "1::int"} = @{code C} 1
  1885   | num_of_term vs (@{term "numeral :: _ \<Rightarrow> int"} $ t) = @{code C} (HOLogic.dest_num t)
  1886   | num_of_term vs (@{term "neg_numeral :: _ \<Rightarrow> int"} $ t) = @{code C} (~(HOLogic.dest_num t))
  1887   | num_of_term vs (Bound i) = @{code Bound} i
  1888   | num_of_term vs (@{term "uminus :: int \<Rightarrow> int"} $ t') = @{code Neg} (num_of_term vs t')
  1889   | num_of_term vs (@{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} $ t1 $ t2) =
  1890       @{code Add} (num_of_term vs t1, num_of_term vs t2)
  1891   | num_of_term vs (@{term "op - :: int \<Rightarrow> int \<Rightarrow> int"} $ t1 $ t2) =
  1892       @{code Sub} (num_of_term vs t1, num_of_term vs t2)
  1893   | num_of_term vs (@{term "op * :: int \<Rightarrow> int \<Rightarrow> int"} $ t1 $ t2) =
  1894       (case try HOLogic.dest_number t1
  1895        of SOME (_, i) => @{code Mul} (i, num_of_term vs t2)
  1896         | NONE => (case try HOLogic.dest_number t2
  1897                 of SOME (_, i) => @{code Mul} (i, num_of_term vs t1)
  1898                  | NONE => error "num_of_term: unsupported multiplication"))
  1899   | num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term @{context} t);
  1900 
  1901 fun fm_of_term ps vs @{term True} = @{code T}
  1902   | fm_of_term ps vs @{term False} = @{code F}
  1903   | fm_of_term ps vs (@{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"} $ t1 $ t2) =
  1904       @{code Lt} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
  1905   | fm_of_term ps vs (@{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"} $ t1 $ t2) =
  1906       @{code Le} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
  1907   | fm_of_term ps vs (@{term "op = :: int \<Rightarrow> int \<Rightarrow> bool"} $ t1 $ t2) =
  1908       @{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2)) 
  1909   | fm_of_term ps vs (@{term "op dvd :: int \<Rightarrow> int \<Rightarrow> bool"} $ t1 $ t2) =
  1910       (case try HOLogic.dest_number t1
  1911        of SOME (_, i) => @{code Dvd} (i, num_of_term vs t2)
  1912         | NONE => error "num_of_term: unsupported dvd")
  1913   | fm_of_term ps vs (@{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) =
  1914       @{code Iff} (fm_of_term ps vs t1, fm_of_term ps vs t2)
  1915   | fm_of_term ps vs (@{term HOL.conj} $ t1 $ t2) =
  1916       @{code And} (fm_of_term ps vs t1, fm_of_term ps vs t2)
  1917   | fm_of_term ps vs (@{term HOL.disj} $ t1 $ t2) =
  1918       @{code Or} (fm_of_term ps vs t1, fm_of_term ps vs t2)
  1919   | fm_of_term ps vs (@{term HOL.implies} $ t1 $ t2) =
  1920       @{code Imp} (fm_of_term ps vs t1, fm_of_term ps vs t2)
  1921   | fm_of_term ps vs (@{term "Not"} $ t') =
  1922       @{code NOT} (fm_of_term ps vs t')
  1923   | fm_of_term ps vs (Const (@{const_name Ex}, _) $ Abs (xn, xT, p)) =
  1924       let
  1925         val (xn', p') = Syntax_Trans.variant_abs (xn, xT, p);  (* FIXME !? *)
  1926         val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
  1927       in @{code E} (fm_of_term ps vs' p) end
  1928   | fm_of_term ps vs (Const (@{const_name All}, _) $ Abs (xn, xT, p)) =
  1929       let
  1930         val (xn', p') = Syntax_Trans.variant_abs (xn, xT, p);  (* FIXME !? *)
  1931         val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
  1932       in @{code A} (fm_of_term ps vs' p) end
  1933   | fm_of_term ps vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t);
  1934 
  1935 fun term_of_num vs (@{code C} i) = HOLogic.mk_number HOLogic.intT i
  1936   | term_of_num vs (@{code Bound} n) = fst (the (find_first (fn (_, m) => n = m) vs))
  1937   | term_of_num vs (@{code Neg} t') = @{term "uminus :: int \<Rightarrow> int"} $ term_of_num vs t'
  1938   | term_of_num vs (@{code Add} (t1, t2)) = @{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} $
  1939       term_of_num vs t1 $ term_of_num vs t2
  1940   | term_of_num vs (@{code Sub} (t1, t2)) = @{term "op - :: int \<Rightarrow> int \<Rightarrow> int"} $
  1941       term_of_num vs t1 $ term_of_num vs t2
  1942   | term_of_num vs (@{code Mul} (i, t2)) = @{term "op * :: int \<Rightarrow> int \<Rightarrow> int"} $
  1943       term_of_num vs (@{code C} i) $ term_of_num vs t2
  1944   | term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t));
  1945 
  1946 fun term_of_fm ps vs @{code T} = @{term True} 
  1947   | term_of_fm ps vs @{code F} = @{term False}
  1948   | term_of_fm ps vs (@{code Lt} t) =
  1949       @{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"} $ term_of_num vs t $ @{term "0::int"}
  1950   | term_of_fm ps vs (@{code Le} t) =
  1951       @{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"} $ term_of_num vs t $ @{term "0::int"}
  1952   | term_of_fm ps vs (@{code Gt} t) =
  1953       @{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"} $ @{term "0::int"} $ term_of_num vs t
  1954   | term_of_fm ps vs (@{code Ge} t) =
  1955       @{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"} $ @{term "0::int"} $ term_of_num vs t
  1956   | term_of_fm ps vs (@{code Eq} t) =
  1957       @{term "op = :: int \<Rightarrow> int \<Rightarrow> bool"} $ term_of_num vs t $ @{term "0::int"}
  1958   | term_of_fm ps vs (@{code NEq} t) =
  1959       term_of_fm ps vs (@{code NOT} (@{code Eq} t))
  1960   | term_of_fm ps vs (@{code Dvd} (i, t)) =
  1961       @{term "op dvd :: int \<Rightarrow> int \<Rightarrow> bool"} $ term_of_num vs (@{code C} i) $ term_of_num vs t
  1962   | term_of_fm ps vs (@{code NDvd} (i, t)) =
  1963       term_of_fm ps vs (@{code NOT} (@{code Dvd} (i, t)))
  1964   | term_of_fm ps vs (@{code NOT} t') =
  1965       HOLogic.Not $ term_of_fm ps vs t'
  1966   | term_of_fm ps vs (@{code And} (t1, t2)) =
  1967       HOLogic.conj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
  1968   | term_of_fm ps vs (@{code Or} (t1, t2)) =
  1969       HOLogic.disj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
  1970   | term_of_fm ps vs (@{code Imp} (t1, t2)) =
  1971       HOLogic.imp $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
  1972   | term_of_fm ps vs (@{code Iff} (t1, t2)) =
  1973       @{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
  1974   | term_of_fm ps vs (@{code Closed} n) = (fst o the) (find_first (fn (_, m) => m = n) ps)
  1975   | term_of_fm ps vs (@{code NClosed} n) = term_of_fm ps vs (@{code NOT} (@{code Closed} n));
  1976 
  1977 fun term_bools acc t =
  1978   let
  1979     val is_op = member (op =) [@{term HOL.conj}, @{term HOL.disj}, @{term HOL.implies}, @{term "op = :: bool => _"},
  1980       @{term "op = :: int => _"}, @{term "op < :: int => _"},
  1981       @{term "op <= :: int => _"}, @{term "Not"}, @{term "All :: (int => _) => _"},
  1982       @{term "Ex :: (int => _) => _"}, @{term "True"}, @{term "False"}]
  1983     fun is_ty t = not (fastype_of t = HOLogic.boolT) 
  1984   in case t
  1985    of (l as f $ a) $ b => if is_ty t orelse is_op t then term_bools (term_bools acc l)b 
  1986         else insert (op aconv) t acc
  1987     | f $ a => if is_ty t orelse is_op t then term_bools (term_bools acc f) a  
  1988         else insert (op aconv) t acc
  1989     | Abs p => term_bools acc (snd (Syntax_Trans.variant_abs p))  (* FIXME !? *)
  1990     | _ => if is_ty t orelse is_op t then acc else insert (op aconv) t acc
  1991   end;
  1992 
  1993 in fn ct =>
  1994   let
  1995     val thy = Thm.theory_of_cterm ct;
  1996     val t = Thm.term_of ct;
  1997     val fs = Misc_Legacy.term_frees t;
  1998     val bs = term_bools [] t;
  1999     val vs = map_index swap fs;
  2000     val ps = map_index swap bs;
  2001     val t' = (term_of_fm ps vs o @{code pa} o fm_of_term ps vs) t;
  2002   in (Thm.cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
  2003 end;
  2004 *}
  2005 
  2006 ML_file "cooper_tac.ML"
  2007 
  2008 method_setup cooper = {*
  2009   Args.mode "no_quantify" >>
  2010     (fn q => fn ctxt => SIMPLE_METHOD' (Cooper_Tac.linz_tac ctxt (not q)))
  2011 *} "decision procedure for linear integer arithmetic"
  2012 
  2013 
  2014 text {* Tests *}
  2015 
  2016 lemma "\<exists> (j::int). \<forall> x\<ge>j. (\<exists> a b. x = 3*a+5*b)"
  2017   by cooper
  2018 
  2019 lemma "ALL (x::int) >=8. EX i j. 5*i + 3*j = x"
  2020   by cooper
  2021 
  2022 theorem "(\<forall>(y::int). 3 dvd y) ==> \<forall>(x::int). b < x --> a \<le> x"
  2023   by cooper
  2024 
  2025 theorem "!! (y::int) (z::int) (n::int). 3 dvd z ==> 2 dvd (y::int) ==>
  2026   (\<exists>(x::int).  2*x =  y) & (\<exists>(k::int). 3*k = z)"
  2027   by cooper
  2028 
  2029 theorem "!! (y::int) (z::int) n. Suc(n::nat) < 6 ==>  3 dvd z ==>
  2030   2 dvd (y::int) ==> (\<exists>(x::int).  2*x =  y) & (\<exists>(k::int). 3*k = z)"
  2031   by cooper
  2032 
  2033 theorem "\<forall>(x::nat). \<exists>(y::nat). (0::nat) \<le> 5 --> y = 5 + x "
  2034   by cooper
  2035 
  2036 lemma "ALL (x::int) >=8. EX i j. 5*i + 3*j = x"
  2037   by cooper 
  2038 
  2039 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)"
  2040   by cooper
  2041 
  2042 lemma "ALL(x::int) y. x < y --> 2 * x + 1 < 2 * y"
  2043   by cooper
  2044 
  2045 lemma "ALL(x::int) y. 2 * x + 1 ~= 2 * y"
  2046   by cooper
  2047 
  2048 lemma "EX(x::int) y. 0 < x  & 0 <= y  & 3 * x - 5 * y = 1"
  2049   by cooper
  2050 
  2051 lemma "~ (EX(x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)"
  2052   by cooper
  2053 
  2054 lemma "ALL(x::int). (2 dvd x) --> (EX(y::int). x = 2*y)"
  2055   by cooper
  2056 
  2057 lemma "ALL(x::int). (2 dvd x) = (EX(y::int). x = 2*y)"
  2058   by cooper
  2059 
  2060 lemma "ALL(x::int). ((2 dvd x) = (ALL(y::int). x ~= 2*y + 1))"
  2061   by cooper
  2062 
  2063 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))))"
  2064   by cooper
  2065 
  2066 lemma "~ (ALL(i::int). 4 <= i --> (EX x y. 0 <= x & 0 <= y & 3 * x + 5 * y = i))" 
  2067   by cooper
  2068 
  2069 lemma "EX j. ALL (x::int) >= j. EX i j. 5*i + 3*j = x"
  2070   by cooper
  2071 
  2072 theorem "(\<forall>(y::int). 3 dvd y) ==> \<forall>(x::int). b < x --> a \<le> x"
  2073   by cooper
  2074 
  2075 theorem "!! (y::int) (z::int) (n::int). 3 dvd z ==> 2 dvd (y::int) ==>
  2076   (\<exists>(x::int).  2*x =  y) & (\<exists>(k::int). 3*k = z)"
  2077   by cooper
  2078 
  2079 theorem "!! (y::int) (z::int) n. Suc(n::nat) < 6 ==>  3 dvd z ==>
  2080   2 dvd (y::int) ==> (\<exists>(x::int).  2*x =  y) & (\<exists>(k::int). 3*k = z)"
  2081   by cooper
  2082 
  2083 theorem "\<forall>(x::nat). \<exists>(y::nat). (0::nat) \<le> 5 --> y = 5 + x "
  2084   by cooper
  2085 
  2086 theorem "\<forall>(x::nat). \<exists>(y::nat). y = 5 + x | x div 6 + 1= 2"
  2087   by cooper
  2088 
  2089 theorem "\<exists>(x::int). 0 < x"
  2090   by cooper
  2091 
  2092 theorem "\<forall>(x::int) y. x < y --> 2 * x + 1 < 2 * y"
  2093   by cooper
  2094  
  2095 theorem "\<forall>(x::int) y. 2 * x + 1 \<noteq> 2 * y"
  2096   by cooper
  2097  
  2098 theorem "\<exists>(x::int) y. 0 < x  & 0 \<le> y  & 3 * x - 5 * y = 1"
  2099   by cooper
  2100 
  2101 theorem "~ (\<exists>(x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)"
  2102   by cooper
  2103 
  2104 theorem "~ (\<exists>(x::int). False)"
  2105   by cooper
  2106 
  2107 theorem "\<forall>(x::int). (2 dvd x) --> (\<exists>(y::int). x = 2*y)"
  2108   by cooper 
  2109 
  2110 theorem "\<forall>(x::int). (2 dvd x) --> (\<exists>(y::int). x = 2*y)"
  2111   by cooper 
  2112 
  2113 theorem "\<forall>(x::int). (2 dvd x) = (\<exists>(y::int). x = 2*y)"
  2114   by cooper 
  2115 
  2116 theorem "\<forall>(x::int). ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y + 1))"
  2117   by cooper 
  2118 
  2119 theorem "~ (\<forall>(x::int). 
  2120             ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y+1) | 
  2121              (\<exists>(q::int) (u::int) i. 3*i + 2*q - u < 17)
  2122              --> 0 < x | ((~ 3 dvd x) &(x + 8 = 0))))"
  2123   by cooper
  2124  
  2125 theorem "~ (\<forall>(i::int). 4 \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i))"
  2126   by cooper
  2127 
  2128 theorem "\<forall>(i::int). 8 \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i)"
  2129   by cooper
  2130 
  2131 theorem "\<exists>(j::int). \<forall>i. j \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i)"
  2132   by cooper
  2133 
  2134 theorem "~ (\<forall>j (i::int). j \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i))"
  2135   by cooper
  2136 
  2137 theorem "(\<exists>m::nat. n = 2 * m) --> (n + 1) div 2 = n div 2"
  2138   by cooper
  2139 
  2140 end