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