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