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