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