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