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