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