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