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