src/HOL/Decision_Procs/Ferrack.thy
 author wenzelm Thu Nov 08 15:49:56 2018 +0100 (7 months ago) changeset 69266 7cc2d66a92a6 parent 69064 5840724b1d71 child 69597 ff784d5a5bfb permissions -rw-r--r--
proper ML expressions, without trailing semicolons;
```     1 (*  Title:      HOL/Decision_Procs/Ferrack.thy
```
```     2     Author:     Amine Chaieb
```
```     3 *)
```
```     4
```
```     5 theory Ferrack
```
```     6 imports Complex_Main Dense_Linear_Order DP_Library
```
```     7   "HOL-Library.Code_Target_Numeral"
```
```     8 begin
```
```     9
```
```    10 section \<open>Quantifier elimination for \<open>\<real> (0, 1, +, <)\<close>\<close>
```
```    11
```
```    12   (*********************************************************************************)
```
```    13   (****                            SHADOW SYNTAX AND SEMANTICS                  ****)
```
```    14   (*********************************************************************************)
```
```    15
```
```    16 datatype (plugins del: size) num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num
```
```    17   | Mul int num
```
```    18
```
```    19 instantiation num :: size
```
```    20 begin
```
```    21
```
```    22 primrec size_num :: "num \<Rightarrow> nat"
```
```    23 where
```
```    24   "size_num (C c) = 1"
```
```    25 | "size_num (Bound n) = 1"
```
```    26 | "size_num (Neg a) = 1 + size_num a"
```
```    27 | "size_num (Add a b) = 1 + size_num a + size_num b"
```
```    28 | "size_num (Sub a b) = 3 + size_num a + size_num b"
```
```    29 | "size_num (Mul c a) = 1 + size_num a"
```
```    30 | "size_num (CN n c a) = 3 + size_num a "
```
```    31
```
```    32 instance ..
```
```    33
```
```    34 end
```
```    35
```
```    36   (* Semantics of numeral terms (num) *)
```
```    37 primrec Inum :: "real list \<Rightarrow> num \<Rightarrow> real"
```
```    38 where
```
```    39   "Inum bs (C c) = (real_of_int c)"
```
```    40 | "Inum bs (Bound n) = bs!n"
```
```    41 | "Inum bs (CN n c a) = (real_of_int c) * (bs!n) + (Inum bs a)"
```
```    42 | "Inum bs (Neg a) = -(Inum bs a)"
```
```    43 | "Inum bs (Add a b) = Inum bs a + Inum bs b"
```
```    44 | "Inum bs (Sub a b) = Inum bs a - Inum bs b"
```
```    45 | "Inum bs (Mul c a) = (real_of_int c) * Inum bs a"
```
```    46     (* FORMULAE *)
```
```    47 datatype (plugins del: size) fm  =
```
```    48   T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num|
```
```    49   NOT fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
```
```    50
```
```    51 instantiation fm :: size
```
```    52 begin
```
```    53
```
```    54 primrec size_fm :: "fm \<Rightarrow> nat"
```
```    55 where
```
```    56   "size_fm (NOT p) = 1 + size_fm p"
```
```    57 | "size_fm (And p q) = 1 + size_fm p + size_fm q"
```
```    58 | "size_fm (Or p q) = 1 + size_fm p + size_fm q"
```
```    59 | "size_fm (Imp p q) = 3 + size_fm p + size_fm q"
```
```    60 | "size_fm (Iff p q) = 3 + 2 * (size_fm p + size_fm q)"
```
```    61 | "size_fm (E p) = 1 + size_fm p"
```
```    62 | "size_fm (A p) = 4 + size_fm p"
```
```    63 | "size_fm T = 1"
```
```    64 | "size_fm F = 1"
```
```    65 | "size_fm (Lt _) = 1"
```
```    66 | "size_fm (Le _) = 1"
```
```    67 | "size_fm (Gt _) = 1"
```
```    68 | "size_fm (Ge _) = 1"
```
```    69 | "size_fm (Eq _) = 1"
```
```    70 | "size_fm (NEq _) = 1"
```
```    71
```
```    72 instance ..
```
```    73
```
```    74 end
```
```    75
```
```    76 lemma size_fm_pos [simp]: "size p > 0" for p :: fm
```
```    77   by (induct p) simp_all
```
```    78
```
```    79   (* Semantics of formulae (fm) *)
```
```    80 primrec Ifm ::"real list \<Rightarrow> fm \<Rightarrow> bool"
```
```    81 where
```
```    82   "Ifm bs T = True"
```
```    83 | "Ifm bs F = False"
```
```    84 | "Ifm bs (Lt a) = (Inum bs a < 0)"
```
```    85 | "Ifm bs (Gt a) = (Inum bs a > 0)"
```
```    86 | "Ifm bs (Le a) = (Inum bs a \<le> 0)"
```
```    87 | "Ifm bs (Ge a) = (Inum bs a \<ge> 0)"
```
```    88 | "Ifm bs (Eq a) = (Inum bs a = 0)"
```
```    89 | "Ifm bs (NEq a) = (Inum bs a \<noteq> 0)"
```
```    90 | "Ifm bs (NOT p) = (\<not> (Ifm bs p))"
```
```    91 | "Ifm bs (And p q) = (Ifm bs p \<and> Ifm bs q)"
```
```    92 | "Ifm bs (Or p q) = (Ifm bs p \<or> Ifm bs q)"
```
```    93 | "Ifm bs (Imp p q) = ((Ifm bs p) \<longrightarrow> (Ifm bs q))"
```
```    94 | "Ifm bs (Iff p q) = (Ifm bs p = Ifm bs q)"
```
```    95 | "Ifm bs (E p) = (\<exists>x. Ifm (x#bs) p)"
```
```    96 | "Ifm bs (A p) = (\<forall>x. Ifm (x#bs) p)"
```
```    97
```
```    98 lemma IfmLeSub: "\<lbrakk> Inum bs s = s' ; Inum bs t = t' \<rbrakk> \<Longrightarrow> Ifm bs (Le (Sub s t)) = (s' \<le> t')"
```
```    99   by simp
```
```   100
```
```   101 lemma IfmLtSub: "\<lbrakk> Inum bs s = s' ; Inum bs t = t' \<rbrakk> \<Longrightarrow> Ifm bs (Lt (Sub s t)) = (s' < t')"
```
```   102   by simp
```
```   103
```
```   104 lemma IfmEqSub: "\<lbrakk> Inum bs s = s' ; Inum bs t = t' \<rbrakk> \<Longrightarrow> Ifm bs (Eq (Sub s t)) = (s' = t')"
```
```   105   by simp
```
```   106
```
```   107 lemma IfmNOT: " (Ifm bs p = P) \<Longrightarrow> (Ifm bs (NOT p) = (\<not>P))"
```
```   108   by simp
```
```   109
```
```   110 lemma IfmAnd: " \<lbrakk> Ifm bs p = P ; Ifm bs q = Q\<rbrakk> \<Longrightarrow> (Ifm bs (And p q) = (P \<and> Q))"
```
```   111   by simp
```
```   112
```
```   113 lemma IfmOr: " \<lbrakk> Ifm bs p = P ; Ifm bs q = Q\<rbrakk> \<Longrightarrow> (Ifm bs (Or p q) = (P \<or> Q))"
```
```   114   by simp
```
```   115
```
```   116 lemma IfmImp: " \<lbrakk> Ifm bs p = P ; Ifm bs q = Q\<rbrakk> \<Longrightarrow> (Ifm bs (Imp p q) = (P \<longrightarrow> Q))"
```
```   117   by simp
```
```   118
```
```   119 lemma IfmIff: " \<lbrakk> Ifm bs p = P ; Ifm bs q = Q\<rbrakk> \<Longrightarrow> (Ifm bs (Iff p q) = (P = Q))"
```
```   120   by simp
```
```   121
```
```   122 lemma IfmE: " (!! x. Ifm (x#bs) p = P x) \<Longrightarrow> (Ifm bs (E p) = (\<exists>x. P x))"
```
```   123   by simp
```
```   124
```
```   125 lemma IfmA: " (!! x. Ifm (x#bs) p = P x) \<Longrightarrow> (Ifm bs (A p) = (\<forall>x. P x))"
```
```   126   by simp
```
```   127
```
```   128 fun not:: "fm \<Rightarrow> fm"
```
```   129 where
```
```   130   "not (NOT p) = p"
```
```   131 | "not T = F"
```
```   132 | "not F = T"
```
```   133 | "not p = NOT p"
```
```   134
```
```   135 lemma not[simp]: "Ifm bs (not p) = Ifm bs (NOT p)"
```
```   136   by (cases p) auto
```
```   137
```
```   138 definition conj :: "fm \<Rightarrow> fm \<Rightarrow> fm"
```
```   139 where
```
```   140   "conj p q =
```
```   141    (if p = F \<or> q = F then F
```
```   142     else if p = T then q
```
```   143     else if q = T then p
```
```   144     else if p = q then p else And p q)"
```
```   145
```
```   146 lemma conj[simp]: "Ifm bs (conj p q) = Ifm bs (And p q)"
```
```   147   by (cases "p = F \<or> q = F", simp_all add: conj_def) (cases p, simp_all)
```
```   148
```
```   149 definition disj :: "fm \<Rightarrow> fm \<Rightarrow> fm"
```
```   150 where
```
```   151   "disj p q =
```
```   152    (if p = T \<or> q = T then T
```
```   153     else if p = F then q
```
```   154     else if q = F then p
```
```   155     else if p = q then p else Or p q)"
```
```   156
```
```   157 lemma disj[simp]: "Ifm bs (disj p q) = Ifm bs (Or p q)"
```
```   158   by (cases "p = T \<or> q = T", simp_all add: disj_def) (cases p, simp_all)
```
```   159
```
```   160 definition imp :: "fm \<Rightarrow> fm \<Rightarrow> fm"
```
```   161 where
```
```   162   "imp p q =
```
```   163    (if p = F \<or> q = T \<or> p = q then T
```
```   164     else if p = T then q
```
```   165     else if q = F then not p
```
```   166     else Imp p q)"
```
```   167
```
```   168 lemma imp[simp]: "Ifm bs (imp p q) = Ifm bs (Imp p q)"
```
```   169   by (cases "p = F \<or> q = T") (simp_all add: imp_def)
```
```   170
```
```   171 definition iff :: "fm \<Rightarrow> fm \<Rightarrow> fm"
```
```   172 where
```
```   173   "iff p q =
```
```   174    (if p = q then T
```
```   175     else if p = NOT q \<or> NOT p = q then F
```
```   176     else if p = F then not q
```
```   177     else if q = F then not p
```
```   178     else if p = T then q
```
```   179     else if q = T then p
```
```   180     else Iff p q)"
```
```   181
```
```   182 lemma iff[simp]: "Ifm bs (iff p q) = Ifm bs (Iff p q)"
```
```   183   by (unfold iff_def, cases "p = q", simp, cases "p = NOT q", simp) (cases "NOT p = q", auto)
```
```   184
```
```   185 lemma conj_simps:
```
```   186   "conj F Q = F"
```
```   187   "conj P F = F"
```
```   188   "conj T Q = Q"
```
```   189   "conj P T = P"
```
```   190   "conj P P = P"
```
```   191   "P \<noteq> T \<Longrightarrow> P \<noteq> F \<Longrightarrow> Q \<noteq> T \<Longrightarrow> Q \<noteq> F \<Longrightarrow> P \<noteq> Q \<Longrightarrow> conj P Q = And P Q"
```
```   192   by (simp_all add: conj_def)
```
```   193
```
```   194 lemma disj_simps:
```
```   195   "disj T Q = T"
```
```   196   "disj P T = T"
```
```   197   "disj F Q = Q"
```
```   198   "disj P F = P"
```
```   199   "disj P P = P"
```
```   200   "P \<noteq> T \<Longrightarrow> P \<noteq> F \<Longrightarrow> Q \<noteq> T \<Longrightarrow> Q \<noteq> F \<Longrightarrow> P \<noteq> Q \<Longrightarrow> disj P Q = Or P Q"
```
```   201   by (simp_all add: disj_def)
```
```   202
```
```   203 lemma imp_simps:
```
```   204   "imp F Q = T"
```
```   205   "imp P T = T"
```
```   206   "imp T Q = Q"
```
```   207   "imp P F = not P"
```
```   208   "imp P P = T"
```
```   209   "P \<noteq> T \<Longrightarrow> P \<noteq> F \<Longrightarrow> P \<noteq> Q \<Longrightarrow> Q \<noteq> T \<Longrightarrow> Q \<noteq> F \<Longrightarrow> imp P Q = Imp P Q"
```
```   210   by (simp_all add: imp_def)
```
```   211
```
```   212 lemma trivNOT: "p \<noteq> NOT p" "NOT p \<noteq> p"
```
```   213   by (induct p) auto
```
```   214
```
```   215 lemma iff_simps:
```
```   216   "iff p p = T"
```
```   217   "iff p (NOT p) = F"
```
```   218   "iff (NOT p) p = F"
```
```   219   "iff p F = not p"
```
```   220   "iff F p = not p"
```
```   221   "p \<noteq> NOT T \<Longrightarrow> iff T p = p"
```
```   222   "p\<noteq> NOT T \<Longrightarrow> iff p T = p"
```
```   223   "p\<noteq>q \<Longrightarrow> p\<noteq> NOT q \<Longrightarrow> q\<noteq> NOT p \<Longrightarrow> p\<noteq> F \<Longrightarrow> q\<noteq> F \<Longrightarrow> p \<noteq> T \<Longrightarrow> q \<noteq> T \<Longrightarrow> iff p q = Iff p q"
```
```   224   using trivNOT
```
```   225   by (simp_all add: iff_def, cases p, auto)
```
```   226
```
```   227   (* Quantifier freeness *)
```
```   228 fun qfree:: "fm \<Rightarrow> bool"
```
```   229 where
```
```   230   "qfree (E p) = False"
```
```   231 | "qfree (A p) = False"
```
```   232 | "qfree (NOT p) = qfree p"
```
```   233 | "qfree (And p q) = (qfree p \<and> qfree q)"
```
```   234 | "qfree (Or  p q) = (qfree p \<and> qfree q)"
```
```   235 | "qfree (Imp p q) = (qfree p \<and> qfree q)"
```
```   236 | "qfree (Iff p q) = (qfree p \<and> qfree q)"
```
```   237 | "qfree p = True"
```
```   238
```
```   239   (* Boundedness and substitution *)
```
```   240 primrec numbound0:: "num \<Rightarrow> bool" (* a num is INDEPENDENT of Bound 0 *)
```
```   241 where
```
```   242   "numbound0 (C c) = True"
```
```   243 | "numbound0 (Bound n) = (n > 0)"
```
```   244 | "numbound0 (CN n c a) = (n \<noteq> 0 \<and> numbound0 a)"
```
```   245 | "numbound0 (Neg a) = numbound0 a"
```
```   246 | "numbound0 (Add a b) = (numbound0 a \<and> numbound0 b)"
```
```   247 | "numbound0 (Sub a b) = (numbound0 a \<and> numbound0 b)"
```
```   248 | "numbound0 (Mul i a) = numbound0 a"
```
```   249
```
```   250 lemma numbound0_I:
```
```   251   assumes nb: "numbound0 a"
```
```   252   shows "Inum (b#bs) a = Inum (b'#bs) a"
```
```   253   using nb by (induct a) simp_all
```
```   254
```
```   255 primrec bound0:: "fm \<Rightarrow> bool" (* A Formula is independent of Bound 0 *)
```
```   256 where
```
```   257   "bound0 T = True"
```
```   258 | "bound0 F = True"
```
```   259 | "bound0 (Lt a) = numbound0 a"
```
```   260 | "bound0 (Le a) = numbound0 a"
```
```   261 | "bound0 (Gt a) = numbound0 a"
```
```   262 | "bound0 (Ge a) = numbound0 a"
```
```   263 | "bound0 (Eq a) = numbound0 a"
```
```   264 | "bound0 (NEq a) = numbound0 a"
```
```   265 | "bound0 (NOT p) = bound0 p"
```
```   266 | "bound0 (And p q) = (bound0 p \<and> bound0 q)"
```
```   267 | "bound0 (Or p q) = (bound0 p \<and> bound0 q)"
```
```   268 | "bound0 (Imp p q) = ((bound0 p) \<and> (bound0 q))"
```
```   269 | "bound0 (Iff p q) = (bound0 p \<and> bound0 q)"
```
```   270 | "bound0 (E p) = False"
```
```   271 | "bound0 (A p) = False"
```
```   272
```
```   273 lemma bound0_I:
```
```   274   assumes bp: "bound0 p"
```
```   275   shows "Ifm (b#bs) p = Ifm (b'#bs) p"
```
```   276   using bp numbound0_I[where b="b" and bs="bs" and b'="b'"]
```
```   277   by (induct p) auto
```
```   278
```
```   279 lemma not_qf[simp]: "qfree p \<Longrightarrow> qfree (not p)"
```
```   280   by (cases p) auto
```
```   281
```
```   282 lemma not_bn[simp]: "bound0 p \<Longrightarrow> bound0 (not p)"
```
```   283   by (cases p) auto
```
```   284
```
```   285
```
```   286 lemma conj_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (conj p q)"
```
```   287   using conj_def by auto
```
```   288 lemma conj_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (conj p q)"
```
```   289   using conj_def by auto
```
```   290
```
```   291 lemma disj_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (disj p q)"
```
```   292   using disj_def by auto
```
```   293 lemma disj_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (disj p q)"
```
```   294   using disj_def by auto
```
```   295
```
```   296 lemma imp_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (imp p q)"
```
```   297   using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def)
```
```   298 lemma imp_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (imp p q)"
```
```   299   using imp_def by (cases "p=F \<or> q=T \<or> p=q",simp_all add: imp_def)
```
```   300
```
```   301 lemma iff_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (iff p q)"
```
```   302   unfolding iff_def by (cases "p = q") auto
```
```   303 lemma iff_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (iff p q)"
```
```   304   using iff_def unfolding iff_def by (cases "p = q") auto
```
```   305
```
```   306 fun decrnum:: "num \<Rightarrow> num"
```
```   307 where
```
```   308   "decrnum (Bound n) = Bound (n - 1)"
```
```   309 | "decrnum (Neg a) = Neg (decrnum a)"
```
```   310 | "decrnum (Add a b) = Add (decrnum a) (decrnum b)"
```
```   311 | "decrnum (Sub a b) = Sub (decrnum a) (decrnum b)"
```
```   312 | "decrnum (Mul c a) = Mul c (decrnum a)"
```
```   313 | "decrnum (CN n c a) = CN (n - 1) c (decrnum a)"
```
```   314 | "decrnum a = a"
```
```   315
```
```   316 fun decr :: "fm \<Rightarrow> fm"
```
```   317 where
```
```   318   "decr (Lt a) = Lt (decrnum a)"
```
```   319 | "decr (Le a) = Le (decrnum a)"
```
```   320 | "decr (Gt a) = Gt (decrnum a)"
```
```   321 | "decr (Ge a) = Ge (decrnum a)"
```
```   322 | "decr (Eq a) = Eq (decrnum a)"
```
```   323 | "decr (NEq a) = NEq (decrnum a)"
```
```   324 | "decr (NOT p) = NOT (decr p)"
```
```   325 | "decr (And p q) = conj (decr p) (decr q)"
```
```   326 | "decr (Or p q) = disj (decr p) (decr q)"
```
```   327 | "decr (Imp p q) = imp (decr p) (decr q)"
```
```   328 | "decr (Iff p q) = iff (decr p) (decr q)"
```
```   329 | "decr p = p"
```
```   330
```
```   331 lemma decrnum:
```
```   332   assumes nb: "numbound0 t"
```
```   333   shows "Inum (x # bs) t = Inum bs (decrnum t)"
```
```   334   using nb by (induct t rule: decrnum.induct) simp_all
```
```   335
```
```   336 lemma decr:
```
```   337   assumes nb: "bound0 p"
```
```   338   shows "Ifm (x # bs) p = Ifm bs (decr p)"
```
```   339   using nb by (induct p rule: decr.induct) (simp_all add: decrnum)
```
```   340
```
```   341 lemma decr_qf: "bound0 p \<Longrightarrow> qfree (decr p)"
```
```   342   by (induct p) simp_all
```
```   343
```
```   344 fun isatom :: "fm \<Rightarrow> bool" (* test for atomicity *)
```
```   345 where
```
```   346   "isatom T = True"
```
```   347 | "isatom F = True"
```
```   348 | "isatom (Lt a) = True"
```
```   349 | "isatom (Le a) = True"
```
```   350 | "isatom (Gt a) = True"
```
```   351 | "isatom (Ge a) = True"
```
```   352 | "isatom (Eq a) = True"
```
```   353 | "isatom (NEq a) = True"
```
```   354 | "isatom p = False"
```
```   355
```
```   356 lemma bound0_qf: "bound0 p \<Longrightarrow> qfree p"
```
```   357   by (induct p) simp_all
```
```   358
```
```   359 definition djf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a \<Rightarrow> fm \<Rightarrow> fm"
```
```   360 where
```
```   361   "djf f p q =
```
```   362    (if q = T then T
```
```   363     else if q = F then f p
```
```   364     else (let fp = f p in case fp of T \<Rightarrow> T | F \<Rightarrow> q | _ \<Rightarrow> Or (f p) q))"
```
```   365
```
```   366 definition evaldjf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a list \<Rightarrow> fm"
```
```   367   where "evaldjf f ps = foldr (djf f) ps F"
```
```   368
```
```   369 lemma djf_Or: "Ifm bs (djf f p q) = Ifm bs (Or (f p) q)"
```
```   370   by (cases "q = T", simp add: djf_def, cases "q = F", simp add: djf_def)
```
```   371     (cases "f p", simp_all add: Let_def djf_def)
```
```   372
```
```   373
```
```   374 lemma djf_simps:
```
```   375   "djf f p T = T"
```
```   376   "djf f p F = f p"
```
```   377   "q \<noteq> T \<Longrightarrow> q \<noteq> F \<Longrightarrow> djf f p q = (let fp = f p in case fp of T \<Rightarrow> T | F \<Rightarrow> q | _ \<Rightarrow> Or (f p) q)"
```
```   378   by (simp_all add: djf_def)
```
```   379
```
```   380 lemma evaldjf_ex: "Ifm bs (evaldjf f ps) \<longleftrightarrow> (\<exists>p \<in> set ps. Ifm bs (f p))"
```
```   381   by (induct ps) (simp_all add: evaldjf_def djf_Or)
```
```   382
```
```   383 lemma evaldjf_bound0:
```
```   384   assumes nb: "\<forall>x\<in> set xs. bound0 (f x)"
```
```   385   shows "bound0 (evaldjf f xs)"
```
```   386   using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto)
```
```   387
```
```   388 lemma evaldjf_qf:
```
```   389   assumes nb: "\<forall>x\<in> set xs. qfree (f x)"
```
```   390   shows "qfree (evaldjf f xs)"
```
```   391   using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto)
```
```   392
```
```   393 fun disjuncts :: "fm \<Rightarrow> fm list"
```
```   394 where
```
```   395   "disjuncts (Or p q) = disjuncts p @ disjuncts q"
```
```   396 | "disjuncts F = []"
```
```   397 | "disjuncts p = [p]"
```
```   398
```
```   399 lemma disjuncts: "(\<exists>q\<in> set (disjuncts p). Ifm bs q) = Ifm bs p"
```
```   400   by (induct p rule: disjuncts.induct) auto
```
```   401
```
```   402 lemma disjuncts_nb: "bound0 p \<Longrightarrow> \<forall>q\<in> set (disjuncts p). bound0 q"
```
```   403 proof -
```
```   404   assume nb: "bound0 p"
```
```   405   then have "list_all bound0 (disjuncts p)"
```
```   406     by (induct p rule: disjuncts.induct) auto
```
```   407   then show ?thesis
```
```   408     by (simp only: list_all_iff)
```
```   409 qed
```
```   410
```
```   411 lemma disjuncts_qf: "qfree p \<Longrightarrow> \<forall>q\<in> set (disjuncts p). qfree q"
```
```   412 proof -
```
```   413   assume qf: "qfree p"
```
```   414   then have "list_all qfree (disjuncts p)"
```
```   415     by (induct p rule: disjuncts.induct) auto
```
```   416   then show ?thesis
```
```   417     by (simp only: list_all_iff)
```
```   418 qed
```
```   419
```
```   420 definition DJ :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm"
```
```   421   where "DJ f p = evaldjf f (disjuncts p)"
```
```   422
```
```   423 lemma DJ:
```
```   424   assumes fdj: "\<forall>p q. Ifm bs (f (Or p q)) = Ifm bs (Or (f p) (f q))"
```
```   425     and fF: "f F = F"
```
```   426   shows "Ifm bs (DJ f p) = Ifm bs (f p)"
```
```   427 proof -
```
```   428   have "Ifm bs (DJ f p) = (\<exists>q \<in> set (disjuncts p). Ifm bs (f q))"
```
```   429     by (simp add: DJ_def evaldjf_ex)
```
```   430   also have "\<dots> = Ifm bs (f p)"
```
```   431     using fdj fF by (induct p rule: disjuncts.induct) auto
```
```   432   finally show ?thesis .
```
```   433 qed
```
```   434
```
```   435 lemma DJ_qf:
```
```   436   assumes fqf: "\<forall>p. qfree p \<longrightarrow> qfree (f p)"
```
```   437   shows "\<forall>p. qfree p \<longrightarrow> qfree (DJ f p) "
```
```   438 proof clarify
```
```   439   fix p
```
```   440   assume qf: "qfree p"
```
```   441   have th: "DJ f p = evaldjf f (disjuncts p)"
```
```   442     by (simp add: DJ_def)
```
```   443   from disjuncts_qf[OF qf] have "\<forall>q\<in> set (disjuncts p). qfree q" .
```
```   444   with fqf have th':"\<forall>q\<in> set (disjuncts p). qfree (f q)"
```
```   445     by blast
```
```   446   from evaldjf_qf[OF th'] th show "qfree (DJ f p)"
```
```   447     by simp
```
```   448 qed
```
```   449
```
```   450 lemma DJ_qe:
```
```   451   assumes qe: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bs (qe p) = Ifm bs (E p))"
```
```   452   shows "\<forall>bs p. qfree p \<longrightarrow> qfree (DJ qe p) \<and> (Ifm bs ((DJ qe p)) = Ifm bs (E p))"
```
```   453 proof clarify
```
```   454   fix p :: fm
```
```   455   fix bs
```
```   456   assume qf: "qfree p"
```
```   457   from qe have qth: "\<forall>p. qfree p \<longrightarrow> qfree (qe p)"
```
```   458     by blast
```
```   459   from DJ_qf[OF qth] qf have qfth: "qfree (DJ qe p)"
```
```   460     by auto
```
```   461   have "Ifm bs (DJ qe p) \<longleftrightarrow> (\<exists>q\<in> set (disjuncts p). Ifm bs (qe q))"
```
```   462     by (simp add: DJ_def evaldjf_ex)
```
```   463   also have "\<dots> \<longleftrightarrow> (\<exists>q \<in> set(disjuncts p). Ifm bs (E q))"
```
```   464     using qe disjuncts_qf[OF qf] by auto
```
```   465   also have "\<dots> = Ifm bs (E p)"
```
```   466     by (induct p rule: disjuncts.induct) auto
```
```   467   finally show "qfree (DJ qe p) \<and> Ifm bs (DJ qe p) = Ifm bs (E p)"
```
```   468     using qfth by blast
```
```   469 qed
```
```   470
```
```   471   (* Simplification *)
```
```   472
```
```   473 fun maxcoeff:: "num \<Rightarrow> int"
```
```   474 where
```
```   475   "maxcoeff (C i) = \<bar>i\<bar>"
```
```   476 | "maxcoeff (CN n c t) = max \<bar>c\<bar> (maxcoeff t)"
```
```   477 | "maxcoeff t = 1"
```
```   478
```
```   479 lemma maxcoeff_pos: "maxcoeff t \<ge> 0"
```
```   480   by (induct t rule: maxcoeff.induct, auto)
```
```   481
```
```   482 fun numgcdh:: "num \<Rightarrow> int \<Rightarrow> int"
```
```   483 where
```
```   484   "numgcdh (C i) = (\<lambda>g. gcd i g)"
```
```   485 | "numgcdh (CN n c t) = (\<lambda>g. gcd c (numgcdh t g))"
```
```   486 | "numgcdh t = (\<lambda>g. 1)"
```
```   487
```
```   488 definition numgcd :: "num \<Rightarrow> int"
```
```   489   where "numgcd t = numgcdh t (maxcoeff t)"
```
```   490
```
```   491 fun reducecoeffh:: "num \<Rightarrow> int \<Rightarrow> num"
```
```   492 where
```
```   493   "reducecoeffh (C i) = (\<lambda>g. C (i div g))"
```
```   494 | "reducecoeffh (CN n c t) = (\<lambda>g. CN n (c div g) (reducecoeffh t g))"
```
```   495 | "reducecoeffh t = (\<lambda>g. t)"
```
```   496
```
```   497 definition reducecoeff :: "num \<Rightarrow> num"
```
```   498 where
```
```   499   "reducecoeff t =
```
```   500    (let g = numgcd t
```
```   501     in if g = 0 then C 0 else if g = 1 then t else reducecoeffh t g)"
```
```   502
```
```   503 fun dvdnumcoeff:: "num \<Rightarrow> int \<Rightarrow> bool"
```
```   504 where
```
```   505   "dvdnumcoeff (C i) = (\<lambda>g. g dvd i)"
```
```   506 | "dvdnumcoeff (CN n c t) = (\<lambda>g. g dvd c \<and> dvdnumcoeff t g)"
```
```   507 | "dvdnumcoeff t = (\<lambda>g. False)"
```
```   508
```
```   509 lemma dvdnumcoeff_trans:
```
```   510   assumes gdg: "g dvd g'"
```
```   511     and dgt':"dvdnumcoeff t g'"
```
```   512   shows "dvdnumcoeff t g"
```
```   513   using dgt' gdg
```
```   514   by (induct t rule: dvdnumcoeff.induct) (simp_all add: gdg dvd_trans[OF gdg])
```
```   515
```
```   516 declare dvd_trans [trans add]
```
```   517
```
```   518 lemma natabs0: "nat \<bar>x\<bar> = 0 \<longleftrightarrow> x = 0"
```
```   519   by arith
```
```   520
```
```   521 lemma numgcd0:
```
```   522   assumes g0: "numgcd t = 0"
```
```   523   shows "Inum bs t = 0"
```
```   524   using g0[simplified numgcd_def]
```
```   525   by (induct t rule: numgcdh.induct) (auto simp add: natabs0 maxcoeff_pos max.absorb2)
```
```   526
```
```   527 lemma numgcdh_pos:
```
```   528   assumes gp: "g \<ge> 0"
```
```   529   shows "numgcdh t g \<ge> 0"
```
```   530   using gp by (induct t rule: numgcdh.induct) auto
```
```   531
```
```   532 lemma numgcd_pos: "numgcd t \<ge>0"
```
```   533   by (simp add: numgcd_def numgcdh_pos maxcoeff_pos)
```
```   534
```
```   535 lemma reducecoeffh:
```
```   536   assumes gt: "dvdnumcoeff t g"
```
```   537     and gp: "g > 0"
```
```   538   shows "real_of_int g *(Inum bs (reducecoeffh t g)) = Inum bs t"
```
```   539   using gt
```
```   540 proof (induct t rule: reducecoeffh.induct)
```
```   541   case (1 i)
```
```   542   then have gd: "g dvd i"
```
```   543     by simp
```
```   544   with assms show ?case
```
```   545     by (simp add: real_of_int_div[OF gd])
```
```   546 next
```
```   547   case (2 n c t)
```
```   548   then have gd: "g dvd c"
```
```   549     by simp
```
```   550   from assms 2 show ?case
```
```   551     by (simp add: real_of_int_div[OF gd] algebra_simps)
```
```   552 qed (auto simp add: numgcd_def gp)
```
```   553
```
```   554 fun ismaxcoeff:: "num \<Rightarrow> int \<Rightarrow> bool"
```
```   555 where
```
```   556   "ismaxcoeff (C i) = (\<lambda>x. \<bar>i\<bar> \<le> x)"
```
```   557 | "ismaxcoeff (CN n c t) = (\<lambda>x. \<bar>c\<bar> \<le> x \<and> ismaxcoeff t x)"
```
```   558 | "ismaxcoeff t = (\<lambda>x. True)"
```
```   559
```
```   560 lemma ismaxcoeff_mono: "ismaxcoeff t c \<Longrightarrow> c \<le> c' \<Longrightarrow> ismaxcoeff t c'"
```
```   561   by (induct t rule: ismaxcoeff.induct) auto
```
```   562
```
```   563 lemma maxcoeff_ismaxcoeff: "ismaxcoeff t (maxcoeff t)"
```
```   564 proof (induct t rule: maxcoeff.induct)
```
```   565   case (2 n c t)
```
```   566   then have H:"ismaxcoeff t (maxcoeff t)" .
```
```   567   have thh: "maxcoeff t \<le> max \<bar>c\<bar> (maxcoeff t)"
```
```   568     by simp
```
```   569   from ismaxcoeff_mono[OF H thh] show ?case
```
```   570     by simp
```
```   571 qed simp_all
```
```   572
```
```   573 lemma zgcd_gt1:
```
```   574   "\<bar>i\<bar> > 1 \<and> \<bar>j\<bar> > 1 \<or> \<bar>i\<bar> = 0 \<and> \<bar>j\<bar> > 1 \<or> \<bar>i\<bar> > 1 \<and> \<bar>j\<bar> = 0"
```
```   575   if "gcd i j > 1" for i j :: int
```
```   576 proof -
```
```   577   have "\<bar>k\<bar> \<le> 1 \<longleftrightarrow> k = - 1 \<or> k = 0 \<or> k = 1" for k :: int
```
```   578     by auto
```
```   579   with that show ?thesis
```
```   580     by (auto simp add: not_less)
```
```   581 qed
```
```   582
```
```   583 lemma numgcdh0:"numgcdh t m = 0 \<Longrightarrow>  m =0"
```
```   584   by (induct t rule: numgcdh.induct) auto
```
```   585
```
```   586 lemma dvdnumcoeff_aux:
```
```   587   assumes "ismaxcoeff t m"
```
```   588     and mp: "m \<ge> 0"
```
```   589     and "numgcdh t m > 1"
```
```   590   shows "dvdnumcoeff t (numgcdh t m)"
```
```   591   using assms
```
```   592 proof (induct t rule: numgcdh.induct)
```
```   593   case (2 n c t)
```
```   594   let ?g = "numgcdh t m"
```
```   595   from 2 have th: "gcd c ?g > 1"
```
```   596     by simp
```
```   597   from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
```
```   598   consider "\<bar>c\<bar> > 1" "?g > 1" | "\<bar>c\<bar> = 0" "?g > 1" | "?g = 0"
```
```   599     by auto
```
```   600   then show ?case
```
```   601   proof cases
```
```   602     case 1
```
```   603     with 2 have th: "dvdnumcoeff t ?g"
```
```   604       by simp
```
```   605     have th': "gcd c ?g dvd ?g"
```
```   606       by simp
```
```   607     from dvdnumcoeff_trans[OF th' th] show ?thesis
```
```   608       by simp
```
```   609   next
```
```   610     case "2'": 2
```
```   611     with 2 have th: "dvdnumcoeff t ?g"
```
```   612       by simp
```
```   613     have th': "gcd c ?g dvd ?g"
```
```   614       by simp
```
```   615     from dvdnumcoeff_trans[OF th' th] show ?thesis
```
```   616       by simp
```
```   617   next
```
```   618     case 3
```
```   619     then have "m = 0" by (rule numgcdh0)
```
```   620     with 2 3 show ?thesis by simp
```
```   621   qed
```
```   622 qed auto
```
```   623
```
```   624 lemma dvdnumcoeff_aux2:
```
```   625   assumes "numgcd t > 1"
```
```   626   shows "dvdnumcoeff t (numgcd t) \<and> numgcd t > 0"
```
```   627   using assms
```
```   628 proof (simp add: numgcd_def)
```
```   629   let ?mc = "maxcoeff t"
```
```   630   let ?g = "numgcdh t ?mc"
```
```   631   have th1: "ismaxcoeff t ?mc"
```
```   632     by (rule maxcoeff_ismaxcoeff)
```
```   633   have th2: "?mc \<ge> 0"
```
```   634     by (rule maxcoeff_pos)
```
```   635   assume H: "numgcdh t ?mc > 1"
```
```   636   from dvdnumcoeff_aux[OF th1 th2 H] show "dvdnumcoeff t ?g" .
```
```   637 qed
```
```   638
```
```   639 lemma reducecoeff: "real_of_int (numgcd t) * (Inum bs (reducecoeff t)) = Inum bs t"
```
```   640 proof -
```
```   641   let ?g = "numgcd t"
```
```   642   have "?g \<ge> 0"
```
```   643     by (simp add: numgcd_pos)
```
```   644   then consider "?g = 0" | "?g = 1" | "?g > 1" by atomize_elim auto
```
```   645   then show ?thesis
```
```   646   proof cases
```
```   647     case 1
```
```   648     then show ?thesis by (simp add: numgcd0)
```
```   649   next
```
```   650     case 2
```
```   651     then show ?thesis by (simp add: reducecoeff_def)
```
```   652   next
```
```   653     case g1: 3
```
```   654     from dvdnumcoeff_aux2[OF g1] have th1: "dvdnumcoeff t ?g" and g0: "?g > 0"
```
```   655       by blast+
```
```   656     from reducecoeffh[OF th1 g0, where bs="bs"] g1 show ?thesis
```
```   657       by (simp add: reducecoeff_def Let_def)
```
```   658   qed
```
```   659 qed
```
```   660
```
```   661 lemma reducecoeffh_numbound0: "numbound0 t \<Longrightarrow> numbound0 (reducecoeffh t g)"
```
```   662   by (induct t rule: reducecoeffh.induct) auto
```
```   663
```
```   664 lemma reducecoeff_numbound0: "numbound0 t \<Longrightarrow> numbound0 (reducecoeff t)"
```
```   665   using reducecoeffh_numbound0 by (simp add: reducecoeff_def Let_def)
```
```   666
```
```   667 fun numadd:: "num \<Rightarrow> num \<Rightarrow> num"
```
```   668 where
```
```   669   "numadd (CN n1 c1 r1) (CN n2 c2 r2) =
```
```   670    (if n1 = n2 then
```
```   671     (let c = c1 + c2
```
```   672      in (if c = 0 then numadd r1 r2 else CN n1 c (numadd r1 r2)))
```
```   673     else if n1 \<le> n2 then (CN n1 c1 (numadd r1 (CN n2 c2 r2)))
```
```   674     else (CN n2 c2 (numadd (CN n1 c1 r1) r2)))"
```
```   675 | "numadd (CN n1 c1 r1) t = CN n1 c1 (numadd r1 t)"
```
```   676 | "numadd t (CN n2 c2 r2) = CN n2 c2 (numadd t r2)"
```
```   677 | "numadd (C b1) (C b2) = C (b1 + b2)"
```
```   678 | "numadd a b = Add a b"
```
```   679
```
```   680 lemma numadd [simp]: "Inum bs (numadd t s) = Inum bs (Add t s)"
```
```   681   by (induct t s rule: numadd.induct) (simp_all add: Let_def algebra_simps add_eq_0_iff)
```
```   682
```
```   683 lemma numadd_nb [simp]: "numbound0 t \<Longrightarrow> numbound0 s \<Longrightarrow> numbound0 (numadd t s)"
```
```   684   by (induct t s rule: numadd.induct) (simp_all add: Let_def)
```
```   685
```
```   686 fun nummul:: "num \<Rightarrow> int \<Rightarrow> num"
```
```   687 where
```
```   688   "nummul (C j) = (\<lambda>i. C (i * j))"
```
```   689 | "nummul (CN n c a) = (\<lambda>i. CN n (i * c) (nummul a i))"
```
```   690 | "nummul t = (\<lambda>i. Mul i t)"
```
```   691
```
```   692 lemma nummul[simp]: "\<And>i. Inum bs (nummul t i) = Inum bs (Mul i t)"
```
```   693   by (induct t rule: nummul.induct) (auto simp add: algebra_simps)
```
```   694
```
```   695 lemma nummul_nb[simp]: "\<And>i. numbound0 t \<Longrightarrow> numbound0 (nummul t i)"
```
```   696   by (induct t rule: nummul.induct) auto
```
```   697
```
```   698 definition numneg :: "num \<Rightarrow> num"
```
```   699   where "numneg t = nummul t (- 1)"
```
```   700
```
```   701 definition numsub :: "num \<Rightarrow> num \<Rightarrow> num"
```
```   702   where "numsub s t = (if s = t then C 0 else numadd s (numneg t))"
```
```   703
```
```   704 lemma numneg[simp]: "Inum bs (numneg t) = Inum bs (Neg t)"
```
```   705   using numneg_def by simp
```
```   706
```
```   707 lemma numneg_nb[simp]: "numbound0 t \<Longrightarrow> numbound0 (numneg t)"
```
```   708   using numneg_def by simp
```
```   709
```
```   710 lemma numsub[simp]: "Inum bs (numsub a b) = Inum bs (Sub a b)"
```
```   711   using numsub_def by simp
```
```   712
```
```   713 lemma numsub_nb[simp]: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numsub t s)"
```
```   714   using numsub_def by simp
```
```   715
```
```   716 primrec simpnum:: "num \<Rightarrow> num"
```
```   717 where
```
```   718   "simpnum (C j) = C j"
```
```   719 | "simpnum (Bound n) = CN n 1 (C 0)"
```
```   720 | "simpnum (Neg t) = numneg (simpnum t)"
```
```   721 | "simpnum (Add t s) = numadd (simpnum t) (simpnum s)"
```
```   722 | "simpnum (Sub t s) = numsub (simpnum t) (simpnum s)"
```
```   723 | "simpnum (Mul i t) = (if i = 0 then C 0 else nummul (simpnum t) i)"
```
```   724 | "simpnum (CN n c t) = (if c = 0 then simpnum t else numadd (CN n c (C 0)) (simpnum t))"
```
```   725
```
```   726 lemma simpnum_ci[simp]: "Inum bs (simpnum t) = Inum bs t"
```
```   727   by (induct t) simp_all
```
```   728
```
```   729 lemma simpnum_numbound0[simp]: "numbound0 t \<Longrightarrow> numbound0 (simpnum t)"
```
```   730   by (induct t) simp_all
```
```   731
```
```   732 fun nozerocoeff:: "num \<Rightarrow> bool"
```
```   733 where
```
```   734   "nozerocoeff (C c) = True"
```
```   735 | "nozerocoeff (CN n c t) = (c \<noteq> 0 \<and> nozerocoeff t)"
```
```   736 | "nozerocoeff t = True"
```
```   737
```
```   738 lemma numadd_nz : "nozerocoeff a \<Longrightarrow> nozerocoeff b \<Longrightarrow> nozerocoeff (numadd a b)"
```
```   739   by (induct a b rule: numadd.induct) (simp_all add: Let_def)
```
```   740
```
```   741 lemma nummul_nz : "\<And>i. i\<noteq>0 \<Longrightarrow> nozerocoeff a \<Longrightarrow> nozerocoeff (nummul a i)"
```
```   742   by (induct a rule: nummul.induct) (auto simp add: Let_def numadd_nz)
```
```   743
```
```   744 lemma numneg_nz : "nozerocoeff a \<Longrightarrow> nozerocoeff (numneg a)"
```
```   745   by (simp add: numneg_def nummul_nz)
```
```   746
```
```   747 lemma numsub_nz: "nozerocoeff a \<Longrightarrow> nozerocoeff b \<Longrightarrow> nozerocoeff (numsub a b)"
```
```   748   by (simp add: numsub_def numneg_nz numadd_nz)
```
```   749
```
```   750 lemma simpnum_nz: "nozerocoeff (simpnum t)"
```
```   751   by (induct t) (simp_all add: numadd_nz numneg_nz numsub_nz nummul_nz)
```
```   752
```
```   753 lemma maxcoeff_nz: "nozerocoeff t \<Longrightarrow> maxcoeff t = 0 \<Longrightarrow> t = C 0"
```
```   754 proof (induct t rule: maxcoeff.induct)
```
```   755   case (2 n c t)
```
```   756   then have cnz: "c \<noteq> 0" and mx: "max \<bar>c\<bar> (maxcoeff t) = 0"
```
```   757     by simp_all
```
```   758   have "max \<bar>c\<bar> (maxcoeff t) \<ge> \<bar>c\<bar>"
```
```   759     by simp
```
```   760   with cnz have "max \<bar>c\<bar> (maxcoeff t) > 0"
```
```   761     by arith
```
```   762   with 2 show ?case
```
```   763     by simp
```
```   764 qed auto
```
```   765
```
```   766 lemma numgcd_nz:
```
```   767   assumes nz: "nozerocoeff t"
```
```   768     and g0: "numgcd t = 0"
```
```   769   shows "t = C 0"
```
```   770 proof -
```
```   771   from g0 have th:"numgcdh t (maxcoeff t) = 0"
```
```   772     by (simp add: numgcd_def)
```
```   773   from numgcdh0[OF th] have th:"maxcoeff t = 0" .
```
```   774   from maxcoeff_nz[OF nz th] show ?thesis .
```
```   775 qed
```
```   776
```
```   777 definition simp_num_pair :: "(num \<times> int) \<Rightarrow> num \<times> int"
```
```   778 where
```
```   779   "simp_num_pair =
```
```   780     (\<lambda>(t,n).
```
```   781      (if n = 0 then (C 0, 0)
```
```   782       else
```
```   783        (let t' = simpnum t ; g = numgcd t' in
```
```   784          if g > 1 then
```
```   785           (let g' = gcd n g
```
```   786            in if g' = 1 then (t', n) else (reducecoeffh t' g', n div g'))
```
```   787          else (t', n))))"
```
```   788
```
```   789 lemma simp_num_pair_ci:
```
```   790   shows "((\<lambda>(t,n). Inum bs t / real_of_int n) (simp_num_pair (t,n))) =
```
```   791     ((\<lambda>(t,n). Inum bs t / real_of_int n) (t, n))"
```
```   792   (is "?lhs = ?rhs")
```
```   793 proof -
```
```   794   let ?t' = "simpnum t"
```
```   795   let ?g = "numgcd ?t'"
```
```   796   let ?g' = "gcd n ?g"
```
```   797   show ?thesis
```
```   798   proof (cases "n = 0")
```
```   799     case True
```
```   800     then show ?thesis
```
```   801       by (simp add: Let_def simp_num_pair_def)
```
```   802   next
```
```   803     case nnz: False
```
```   804     show ?thesis
```
```   805     proof (cases "?g > 1")
```
```   806       case False
```
```   807       then show ?thesis by (simp add: Let_def simp_num_pair_def)
```
```   808     next
```
```   809       case g1: True
```
```   810       then have g0: "?g > 0"
```
```   811         by simp
```
```   812       from g1 nnz have gp0: "?g' \<noteq> 0"
```
```   813         by simp
```
```   814       then have g'p: "?g' > 0"
```
```   815         using gcd_ge_0_int[where x="n" and y="numgcd ?t'"] by arith
```
```   816       then consider "?g' = 1" | "?g' > 1" by arith
```
```   817       then show ?thesis
```
```   818       proof cases
```
```   819         case 1
```
```   820         then show ?thesis
```
```   821           by (simp add: Let_def simp_num_pair_def)
```
```   822       next
```
```   823         case g'1: 2
```
```   824         from dvdnumcoeff_aux2[OF g1] have th1: "dvdnumcoeff ?t' ?g" ..
```
```   825         let ?tt = "reducecoeffh ?t' ?g'"
```
```   826         let ?t = "Inum bs ?tt"
```
```   827         have gpdg: "?g' dvd ?g" by simp
```
```   828         have gpdd: "?g' dvd n" by simp
```
```   829         have gpdgp: "?g' dvd ?g'" by simp
```
```   830         from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p]
```
```   831         have th2:"real_of_int ?g' * ?t = Inum bs ?t'"
```
```   832           by simp
```
```   833         from g1 g'1 have "?lhs = ?t / real_of_int (n div ?g')"
```
```   834           by (simp add: simp_num_pair_def Let_def)
```
```   835         also have "\<dots> = (real_of_int ?g' * ?t) / (real_of_int ?g' * (real_of_int (n div ?g')))"
```
```   836           by simp
```
```   837         also have "\<dots> = (Inum bs ?t' / real_of_int n)"
```
```   838           using real_of_int_div[OF gpdd] th2 gp0 by simp
```
```   839         finally have "?lhs = Inum bs t / real_of_int n"
```
```   840           by simp
```
```   841         then show ?thesis
```
```   842           by (simp add: simp_num_pair_def)
```
```   843       qed
```
```   844     qed
```
```   845   qed
```
```   846 qed
```
```   847
```
```   848 lemma simp_num_pair_l:
```
```   849   assumes tnb: "numbound0 t"
```
```   850     and np: "n > 0"
```
```   851     and tn: "simp_num_pair (t, n) = (t', n')"
```
```   852   shows "numbound0 t' \<and> n' > 0"
```
```   853 proof -
```
```   854   let ?t' = "simpnum t"
```
```   855   let ?g = "numgcd ?t'"
```
```   856   let ?g' = "gcd n ?g"
```
```   857   show ?thesis
```
```   858   proof (cases "n = 0")
```
```   859     case True
```
```   860     then show ?thesis
```
```   861       using assms by (simp add: Let_def simp_num_pair_def)
```
```   862   next
```
```   863     case nnz: False
```
```   864     show ?thesis
```
```   865     proof (cases "?g > 1")
```
```   866       case False
```
```   867       then show ?thesis
```
```   868         using assms by (auto simp add: Let_def simp_num_pair_def)
```
```   869     next
```
```   870       case g1: True
```
```   871       then have g0: "?g > 0" by simp
```
```   872       from g1 nnz have gp0: "?g' \<noteq> 0" by simp
```
```   873       then have g'p: "?g' > 0" using gcd_ge_0_int[where x="n" and y="numgcd ?t'"]
```
```   874         by arith
```
```   875       then consider "?g'= 1" | "?g' > 1" by arith
```
```   876       then show ?thesis
```
```   877       proof cases
```
```   878         case 1
```
```   879         then show ?thesis
```
```   880           using assms g1 by (auto simp add: Let_def simp_num_pair_def)
```
```   881       next
```
```   882         case g'1: 2
```
```   883         have gpdg: "?g' dvd ?g" by simp
```
```   884         have gpdd: "?g' dvd n" by simp
```
```   885         have gpdgp: "?g' dvd ?g'" by simp
```
```   886         from zdvd_imp_le[OF gpdd np] have g'n: "?g' \<le> n" .
```
```   887         from zdiv_mono1[OF g'n g'p, simplified div_self[OF gp0]] have "n div ?g' > 0"
```
```   888           by simp
```
```   889         then show ?thesis
```
```   890           using assms g1 g'1
```
```   891           by (auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0)
```
```   892       qed
```
```   893     qed
```
```   894   qed
```
```   895 qed
```
```   896
```
```   897 fun simpfm :: "fm \<Rightarrow> fm"
```
```   898 where
```
```   899   "simpfm (And p q) = conj (simpfm p) (simpfm q)"
```
```   900 | "simpfm (Or p q) = disj (simpfm p) (simpfm q)"
```
```   901 | "simpfm (Imp p q) = imp (simpfm p) (simpfm q)"
```
```   902 | "simpfm (Iff p q) = iff (simpfm p) (simpfm q)"
```
```   903 | "simpfm (NOT p) = not (simpfm p)"
```
```   904 | "simpfm (Lt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v < 0) then T else F | _ \<Rightarrow> Lt a')"
```
```   905 | "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')"
```
```   906 | "simpfm (Gt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v > 0)  then T else F | _ \<Rightarrow> Gt a')"
```
```   907 | "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')"
```
```   908 | "simpfm (Eq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v = 0)  then T else F | _ \<Rightarrow> Eq a')"
```
```   909 | "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')"
```
```   910 | "simpfm p = p"
```
```   911
```
```   912 lemma simpfm: "Ifm bs (simpfm p) = Ifm bs p"
```
```   913 proof (induct p rule: simpfm.induct)
```
```   914   case (6 a)
```
```   915   let ?sa = "simpnum a"
```
```   916   from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
```
```   917     by simp
```
```   918   consider v where "?sa = C v" | "\<not> (\<exists>v. ?sa = C v)" by blast
```
```   919   then show ?case
```
```   920   proof cases
```
```   921     case 1
```
```   922     then show ?thesis using sa by simp
```
```   923   next
```
```   924     case 2
```
```   925     then show ?thesis using sa by (cases ?sa) (simp_all add: Let_def)
```
```   926   qed
```
```   927 next
```
```   928   case (7 a)
```
```   929   let ?sa = "simpnum a"
```
```   930   from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
```
```   931     by simp
```
```   932   consider v where "?sa = C v" | "\<not> (\<exists>v. ?sa = C v)" by blast
```
```   933   then show ?case
```
```   934   proof cases
```
```   935     case 1
```
```   936     then show ?thesis using sa by simp
```
```   937   next
```
```   938     case 2
```
```   939     then show ?thesis using sa by (cases ?sa) (simp_all add: Let_def)
```
```   940   qed
```
```   941 next
```
```   942   case (8 a)
```
```   943   let ?sa = "simpnum a"
```
```   944   from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
```
```   945     by simp
```
```   946   consider v where "?sa = C v" | "\<not> (\<exists>v. ?sa = C v)" by blast
```
```   947   then show ?case
```
```   948   proof cases
```
```   949     case 1
```
```   950     then show ?thesis using sa by simp
```
```   951   next
```
```   952     case 2
```
```   953     then show ?thesis using sa by (cases ?sa) (simp_all add: Let_def)
```
```   954   qed
```
```   955 next
```
```   956   case (9 a)
```
```   957   let ?sa = "simpnum a"
```
```   958   from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
```
```   959     by simp
```
```   960   consider v where "?sa = C v" | "\<not> (\<exists>v. ?sa = C v)" by blast
```
```   961   then show ?case
```
```   962   proof cases
```
```   963     case 1
```
```   964     then show ?thesis using sa by simp
```
```   965   next
```
```   966     case 2
```
```   967     then show ?thesis using sa by (cases ?sa) (simp_all add: Let_def)
```
```   968   qed
```
```   969 next
```
```   970   case (10 a)
```
```   971   let ?sa = "simpnum a"
```
```   972   from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
```
```   973     by simp
```
```   974   consider v where "?sa = C v" | "\<not> (\<exists>v. ?sa = C v)" by blast
```
```   975   then show ?case
```
```   976   proof cases
```
```   977     case 1
```
```   978     then show ?thesis using sa by simp
```
```   979   next
```
```   980     case 2
```
```   981     then show ?thesis using sa by (cases ?sa) (simp_all add: Let_def)
```
```   982   qed
```
```   983 next
```
```   984   case (11 a)
```
```   985   let ?sa = "simpnum a"
```
```   986   from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
```
```   987     by simp
```
```   988   consider v where "?sa = C v" | "\<not> (\<exists>v. ?sa = C v)" by blast
```
```   989   then show ?case
```
```   990   proof cases
```
```   991     case 1
```
```   992     then show ?thesis using sa by simp
```
```   993   next
```
```   994     case 2
```
```   995     then show ?thesis using sa by (cases ?sa) (simp_all add: Let_def)
```
```   996   qed
```
```   997 qed (induct p rule: simpfm.induct, simp_all)
```
```   998
```
```   999
```
```  1000 lemma simpfm_bound0: "bound0 p \<Longrightarrow> bound0 (simpfm p)"
```
```  1001 proof (induct p rule: simpfm.induct)
```
```  1002   case (6 a)
```
```  1003   then have nb: "numbound0 a" by simp
```
```  1004   then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
```
```  1005   then show ?case by (cases "simpnum a") (auto simp add: Let_def)
```
```  1006 next
```
```  1007   case (7 a)
```
```  1008   then have nb: "numbound0 a" by simp
```
```  1009   then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
```
```  1010   then show ?case by (cases "simpnum a") (auto simp add: Let_def)
```
```  1011 next
```
```  1012   case (8 a)
```
```  1013   then have nb: "numbound0 a" by simp
```
```  1014   then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
```
```  1015   then show ?case by (cases "simpnum a") (auto simp add: Let_def)
```
```  1016 next
```
```  1017   case (9 a)
```
```  1018   then have nb: "numbound0 a" by simp
```
```  1019   then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
```
```  1020   then show ?case by (cases "simpnum a") (auto simp add: Let_def)
```
```  1021 next
```
```  1022   case (10 a)
```
```  1023   then have nb: "numbound0 a" by simp
```
```  1024   then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
```
```  1025   then show ?case by (cases "simpnum a") (auto simp add: Let_def)
```
```  1026 next
```
```  1027   case (11 a)
```
```  1028   then have nb: "numbound0 a" by simp
```
```  1029   then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
```
```  1030   then show ?case by (cases "simpnum a") (auto simp add: Let_def)
```
```  1031 qed (auto simp add: disj_def imp_def iff_def conj_def)
```
```  1032
```
```  1033 lemma simpfm_qf: "qfree p \<Longrightarrow> qfree (simpfm p)"
```
```  1034   apply (induct p rule: simpfm.induct)
```
```  1035   apply (auto simp add: Let_def)
```
```  1036   apply (case_tac "simpnum a", auto)+
```
```  1037   done
```
```  1038
```
```  1039 fun prep :: "fm \<Rightarrow> fm"
```
```  1040 where
```
```  1041   "prep (E T) = T"
```
```  1042 | "prep (E F) = F"
```
```  1043 | "prep (E (Or p q)) = disj (prep (E p)) (prep (E q))"
```
```  1044 | "prep (E (Imp p q)) = disj (prep (E (NOT p))) (prep (E q))"
```
```  1045 | "prep (E (Iff p q)) = disj (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))"
```
```  1046 | "prep (E (NOT (And p q))) = disj (prep (E (NOT p))) (prep (E(NOT q)))"
```
```  1047 | "prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))"
```
```  1048 | "prep (E (NOT (Iff p q))) = disj (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))"
```
```  1049 | "prep (E p) = E (prep p)"
```
```  1050 | "prep (A (And p q)) = conj (prep (A p)) (prep (A q))"
```
```  1051 | "prep (A p) = prep (NOT (E (NOT p)))"
```
```  1052 | "prep (NOT (NOT p)) = prep p"
```
```  1053 | "prep (NOT (And p q)) = disj (prep (NOT p)) (prep (NOT q))"
```
```  1054 | "prep (NOT (A p)) = prep (E (NOT p))"
```
```  1055 | "prep (NOT (Or p q)) = conj (prep (NOT p)) (prep (NOT q))"
```
```  1056 | "prep (NOT (Imp p q)) = conj (prep p) (prep (NOT q))"
```
```  1057 | "prep (NOT (Iff p q)) = disj (prep (And p (NOT q))) (prep (And (NOT p) q))"
```
```  1058 | "prep (NOT p) = not (prep p)"
```
```  1059 | "prep (Or p q) = disj (prep p) (prep q)"
```
```  1060 | "prep (And p q) = conj (prep p) (prep q)"
```
```  1061 | "prep (Imp p q) = prep (Or (NOT p) q)"
```
```  1062 | "prep (Iff p q) = disj (prep (And p q)) (prep (And (NOT p) (NOT q)))"
```
```  1063 | "prep p = p"
```
```  1064
```
```  1065 lemma prep: "\<And>bs. Ifm bs (prep p) = Ifm bs p"
```
```  1066   by (induct p rule: prep.induct) auto
```
```  1067
```
```  1068   (* Generic quantifier elimination *)
```
```  1069 fun qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm"
```
```  1070 where
```
```  1071   "qelim (E p) = (\<lambda>qe. DJ qe (qelim p qe))"
```
```  1072 | "qelim (A p) = (\<lambda>qe. not (qe ((qelim (NOT p) qe))))"
```
```  1073 | "qelim (NOT p) = (\<lambda>qe. not (qelim p qe))"
```
```  1074 | "qelim (And p q) = (\<lambda>qe. conj (qelim p qe) (qelim q qe))"
```
```  1075 | "qelim (Or  p q) = (\<lambda>qe. disj (qelim p qe) (qelim q qe))"
```
```  1076 | "qelim (Imp p q) = (\<lambda>qe. imp (qelim p qe) (qelim q qe))"
```
```  1077 | "qelim (Iff p q) = (\<lambda>qe. iff (qelim p qe) (qelim q qe))"
```
```  1078 | "qelim p = (\<lambda>y. simpfm p)"
```
```  1079
```
```  1080 lemma qelim_ci:
```
```  1081   assumes qe_inv: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bs (qe p) = Ifm bs (E p))"
```
```  1082   shows "\<And>bs. qfree (qelim p qe) \<and> (Ifm bs (qelim p qe) = Ifm bs p)"
```
```  1083   using qe_inv DJ_qe[OF qe_inv]
```
```  1084   by (induct p rule: qelim.induct)
```
```  1085     (auto simp add: simpfm simpfm_qf simp del: simpfm.simps)
```
```  1086
```
```  1087 fun minusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of -\<infinity>*)
```
```  1088 where
```
```  1089   "minusinf (And p q) = conj (minusinf p) (minusinf q)"
```
```  1090 | "minusinf (Or p q) = disj (minusinf p) (minusinf q)"
```
```  1091 | "minusinf (Eq  (CN 0 c e)) = F"
```
```  1092 | "minusinf (NEq (CN 0 c e)) = T"
```
```  1093 | "minusinf (Lt  (CN 0 c e)) = T"
```
```  1094 | "minusinf (Le  (CN 0 c e)) = T"
```
```  1095 | "minusinf (Gt  (CN 0 c e)) = F"
```
```  1096 | "minusinf (Ge  (CN 0 c e)) = F"
```
```  1097 | "minusinf p = p"
```
```  1098
```
```  1099 fun plusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of +\<infinity>*)
```
```  1100 where
```
```  1101   "plusinf (And p q) = conj (plusinf p) (plusinf q)"
```
```  1102 | "plusinf (Or p q) = disj (plusinf p) (plusinf q)"
```
```  1103 | "plusinf (Eq  (CN 0 c e)) = F"
```
```  1104 | "plusinf (NEq (CN 0 c e)) = T"
```
```  1105 | "plusinf (Lt  (CN 0 c e)) = F"
```
```  1106 | "plusinf (Le  (CN 0 c e)) = F"
```
```  1107 | "plusinf (Gt  (CN 0 c e)) = T"
```
```  1108 | "plusinf (Ge  (CN 0 c e)) = T"
```
```  1109 | "plusinf p = p"
```
```  1110
```
```  1111 fun isrlfm :: "fm \<Rightarrow> bool"   (* Linearity test for fm *)
```
```  1112 where
```
```  1113   "isrlfm (And p q) = (isrlfm p \<and> isrlfm q)"
```
```  1114 | "isrlfm (Or p q) = (isrlfm p \<and> isrlfm q)"
```
```  1115 | "isrlfm (Eq  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
```
```  1116 | "isrlfm (NEq (CN 0 c e)) = (c>0 \<and> numbound0 e)"
```
```  1117 | "isrlfm (Lt  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
```
```  1118 | "isrlfm (Le  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
```
```  1119 | "isrlfm (Gt  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
```
```  1120 | "isrlfm (Ge  (CN 0 c e)) = (c>0 \<and> numbound0 e)"
```
```  1121 | "isrlfm p = (isatom p \<and> (bound0 p))"
```
```  1122
```
```  1123   (* splits the bounded from the unbounded part*)
```
```  1124 fun rsplit0 :: "num \<Rightarrow> int \<times> num"
```
```  1125 where
```
```  1126   "rsplit0 (Bound 0) = (1,C 0)"
```
```  1127 | "rsplit0 (Add a b) = (let (ca,ta) = rsplit0 a; (cb,tb) = rsplit0 b in (ca + cb, Add ta tb))"
```
```  1128 | "rsplit0 (Sub a b) = rsplit0 (Add a (Neg b))"
```
```  1129 | "rsplit0 (Neg a) = (let (c,t) = rsplit0 a in (- c, Neg t))"
```
```  1130 | "rsplit0 (Mul c a) = (let (ca,ta) = rsplit0 a in (c * ca, Mul c ta))"
```
```  1131 | "rsplit0 (CN 0 c a) = (let (ca,ta) = rsplit0 a in (c + ca, ta))"
```
```  1132 | "rsplit0 (CN n c a) = (let (ca,ta) = rsplit0 a in (ca, CN n c ta))"
```
```  1133 | "rsplit0 t = (0,t)"
```
```  1134
```
```  1135 lemma rsplit0: "Inum bs ((case_prod (CN 0)) (rsplit0 t)) = Inum bs t \<and> numbound0 (snd (rsplit0 t))"
```
```  1136 proof (induct t rule: rsplit0.induct)
```
```  1137   case (2 a b)
```
```  1138   let ?sa = "rsplit0 a"
```
```  1139   let ?sb = "rsplit0 b"
```
```  1140   let ?ca = "fst ?sa"
```
```  1141   let ?cb = "fst ?sb"
```
```  1142   let ?ta = "snd ?sa"
```
```  1143   let ?tb = "snd ?sb"
```
```  1144   from 2 have nb: "numbound0 (snd(rsplit0 (Add a b)))"
```
```  1145     by (cases "rsplit0 a") (auto simp add: Let_def split_def)
```
```  1146   have "Inum bs ((case_prod (CN 0)) (rsplit0 (Add a b))) =
```
```  1147     Inum bs ((case_prod (CN 0)) ?sa)+Inum bs ((case_prod (CN 0)) ?sb)"
```
```  1148     by (simp add: Let_def split_def algebra_simps)
```
```  1149   also have "\<dots> = Inum bs a + Inum bs b"
```
```  1150     using 2 by (cases "rsplit0 a") auto
```
```  1151   finally show ?case
```
```  1152     using nb by simp
```
```  1153 qed (auto simp add: Let_def split_def algebra_simps, simp add: distrib_left[symmetric])
```
```  1154
```
```  1155     (* Linearize a formula*)
```
```  1156 definition lt :: "int \<Rightarrow> num \<Rightarrow> fm"
```
```  1157 where
```
```  1158   "lt c t = (if c = 0 then (Lt t) else if c > 0 then (Lt (CN 0 c t))
```
```  1159     else (Gt (CN 0 (-c) (Neg t))))"
```
```  1160
```
```  1161 definition le :: "int \<Rightarrow> num \<Rightarrow> fm"
```
```  1162 where
```
```  1163   "le c t = (if c = 0 then (Le t) else if c > 0 then (Le (CN 0 c t))
```
```  1164     else (Ge (CN 0 (-c) (Neg t))))"
```
```  1165
```
```  1166 definition gt :: "int \<Rightarrow> num \<Rightarrow> fm"
```
```  1167 where
```
```  1168   "gt c t = (if c = 0 then (Gt t) else if c > 0 then (Gt (CN 0 c t))
```
```  1169     else (Lt (CN 0 (-c) (Neg t))))"
```
```  1170
```
```  1171 definition ge :: "int \<Rightarrow> num \<Rightarrow> fm"
```
```  1172 where
```
```  1173   "ge c t = (if c = 0 then (Ge t) else if c > 0 then (Ge (CN 0 c t))
```
```  1174     else (Le (CN 0 (-c) (Neg t))))"
```
```  1175
```
```  1176 definition eq :: "int \<Rightarrow> num \<Rightarrow> fm"
```
```  1177 where
```
```  1178   "eq c t = (if c = 0 then (Eq t) else if c > 0 then (Eq (CN 0 c t))
```
```  1179     else (Eq (CN 0 (-c) (Neg t))))"
```
```  1180
```
```  1181 definition neq :: "int \<Rightarrow> num \<Rightarrow> fm"
```
```  1182 where
```
```  1183   "neq c t = (if c = 0 then (NEq t) else if c > 0 then (NEq (CN 0 c t))
```
```  1184     else (NEq (CN 0 (-c) (Neg t))))"
```
```  1185
```
```  1186 lemma lt: "numnoabs t \<Longrightarrow> Ifm bs (case_prod lt (rsplit0 t)) =
```
```  1187   Ifm bs (Lt t) \<and> isrlfm (case_prod lt (rsplit0 t))"
```
```  1188   using rsplit0[where bs = "bs" and t="t"]
```
```  1189   by (auto simp add: lt_def split_def, cases "snd(rsplit0 t)", auto,
```
```  1190     rename_tac nat a b, case_tac "nat", auto)
```
```  1191
```
```  1192 lemma le: "numnoabs t \<Longrightarrow> Ifm bs (case_prod le (rsplit0 t)) =
```
```  1193   Ifm bs (Le t) \<and> isrlfm (case_prod le (rsplit0 t))"
```
```  1194   using rsplit0[where bs = "bs" and t="t"]
```
```  1195   by (auto simp add: le_def split_def, cases "snd(rsplit0 t)", auto,
```
```  1196     rename_tac nat a b, case_tac "nat", auto)
```
```  1197
```
```  1198 lemma gt: "numnoabs t \<Longrightarrow> Ifm bs (case_prod gt (rsplit0 t)) =
```
```  1199   Ifm bs (Gt t) \<and> isrlfm (case_prod gt (rsplit0 t))"
```
```  1200   using rsplit0[where bs = "bs" and t="t"]
```
```  1201   by (auto simp add: gt_def split_def, cases "snd(rsplit0 t)", auto,
```
```  1202     rename_tac nat a b, case_tac "nat", auto)
```
```  1203
```
```  1204 lemma ge: "numnoabs t \<Longrightarrow> Ifm bs (case_prod ge (rsplit0 t)) =
```
```  1205   Ifm bs (Ge t) \<and> isrlfm (case_prod ge (rsplit0 t))"
```
```  1206   using rsplit0[where bs = "bs" and t="t"]
```
```  1207   by (auto simp add: ge_def split_def, cases "snd(rsplit0 t)", auto,
```
```  1208     rename_tac nat a b, case_tac "nat", auto)
```
```  1209
```
```  1210 lemma eq: "numnoabs t \<Longrightarrow> Ifm bs (case_prod eq (rsplit0 t)) =
```
```  1211   Ifm bs (Eq t) \<and> isrlfm (case_prod eq (rsplit0 t))"
```
```  1212   using rsplit0[where bs = "bs" and t="t"]
```
```  1213   by (auto simp add: eq_def split_def, cases "snd(rsplit0 t)", auto,
```
```  1214     rename_tac nat a b, case_tac "nat", auto)
```
```  1215
```
```  1216 lemma neq: "numnoabs t \<Longrightarrow> Ifm bs (case_prod neq (rsplit0 t)) =
```
```  1217   Ifm bs (NEq t) \<and> isrlfm (case_prod neq (rsplit0 t))"
```
```  1218   using rsplit0[where bs = "bs" and t="t"]
```
```  1219   by (auto simp add: neq_def split_def, cases "snd(rsplit0 t)", auto,
```
```  1220     rename_tac nat a b, case_tac "nat", auto)
```
```  1221
```
```  1222 lemma conj_lin: "isrlfm p \<Longrightarrow> isrlfm q \<Longrightarrow> isrlfm (conj p q)"
```
```  1223   by (auto simp add: conj_def)
```
```  1224
```
```  1225 lemma disj_lin: "isrlfm p \<Longrightarrow> isrlfm q \<Longrightarrow> isrlfm (disj p q)"
```
```  1226   by (auto simp add: disj_def)
```
```  1227
```
```  1228 fun rlfm :: "fm \<Rightarrow> fm"
```
```  1229 where
```
```  1230   "rlfm (And p q) = conj (rlfm p) (rlfm q)"
```
```  1231 | "rlfm (Or p q) = disj (rlfm p) (rlfm q)"
```
```  1232 | "rlfm (Imp p q) = disj (rlfm (NOT p)) (rlfm q)"
```
```  1233 | "rlfm (Iff p q) = disj (conj (rlfm p) (rlfm q)) (conj (rlfm (NOT p)) (rlfm (NOT q)))"
```
```  1234 | "rlfm (Lt a) = case_prod lt (rsplit0 a)"
```
```  1235 | "rlfm (Le a) = case_prod le (rsplit0 a)"
```
```  1236 | "rlfm (Gt a) = case_prod gt (rsplit0 a)"
```
```  1237 | "rlfm (Ge a) = case_prod ge (rsplit0 a)"
```
```  1238 | "rlfm (Eq a) = case_prod eq (rsplit0 a)"
```
```  1239 | "rlfm (NEq a) = case_prod neq (rsplit0 a)"
```
```  1240 | "rlfm (NOT (And p q)) = disj (rlfm (NOT p)) (rlfm (NOT q))"
```
```  1241 | "rlfm (NOT (Or p q)) = conj (rlfm (NOT p)) (rlfm (NOT q))"
```
```  1242 | "rlfm (NOT (Imp p q)) = conj (rlfm p) (rlfm (NOT q))"
```
```  1243 | "rlfm (NOT (Iff p q)) = disj (conj(rlfm p) (rlfm(NOT q))) (conj(rlfm(NOT p)) (rlfm q))"
```
```  1244 | "rlfm (NOT (NOT p)) = rlfm p"
```
```  1245 | "rlfm (NOT T) = F"
```
```  1246 | "rlfm (NOT F) = T"
```
```  1247 | "rlfm (NOT (Lt a)) = rlfm (Ge a)"
```
```  1248 | "rlfm (NOT (Le a)) = rlfm (Gt a)"
```
```  1249 | "rlfm (NOT (Gt a)) = rlfm (Le a)"
```
```  1250 | "rlfm (NOT (Ge a)) = rlfm (Lt a)"
```
```  1251 | "rlfm (NOT (Eq a)) = rlfm (NEq a)"
```
```  1252 | "rlfm (NOT (NEq a)) = rlfm (Eq a)"
```
```  1253 | "rlfm p = p"
```
```  1254
```
```  1255 lemma rlfm_I:
```
```  1256   assumes qfp: "qfree p"
```
```  1257   shows "(Ifm bs (rlfm p) = Ifm bs p) \<and> isrlfm (rlfm p)"
```
```  1258   using qfp
```
```  1259   by (induct p rule: rlfm.induct) (auto simp add: lt le gt ge eq neq conj_lin disj_lin)
```
```  1260
```
```  1261     (* Operations needed for Ferrante and Rackoff *)
```
```  1262 lemma rminusinf_inf:
```
```  1263   assumes lp: "isrlfm p"
```
```  1264   shows "\<exists>z. \<forall>x < z. Ifm (x#bs) (minusinf p) = Ifm (x#bs) p" (is "\<exists>z. \<forall>x. ?P z x p")
```
```  1265   using lp
```
```  1266 proof (induct p rule: minusinf.induct)
```
```  1267   case (1 p q)
```
```  1268   then show ?case
```
```  1269     apply auto
```
```  1270     apply (rule_tac x= "min z za" in exI)
```
```  1271     apply auto
```
```  1272     done
```
```  1273 next
```
```  1274   case (2 p q)
```
```  1275   then show ?case
```
```  1276     apply auto
```
```  1277     apply (rule_tac x= "min z za" in exI)
```
```  1278     apply auto
```
```  1279     done
```
```  1280 next
```
```  1281   case (3 c e)
```
```  1282   from 3 have nb: "numbound0 e" by simp
```
```  1283   from 3 have cp: "real_of_int c > 0" by simp
```
```  1284   fix a
```
```  1285   let ?e = "Inum (a#bs) e"
```
```  1286   let ?z = "(- ?e) / real_of_int c"
```
```  1287   {
```
```  1288     fix x
```
```  1289     assume xz: "x < ?z"
```
```  1290     then have "(real_of_int c * x < - ?e)"
```
```  1291       by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps)
```
```  1292     then have "real_of_int c * x + ?e < 0" by arith
```
```  1293     then have "real_of_int c * x + ?e \<noteq> 0" by simp
```
```  1294     with xz have "?P ?z x (Eq (CN 0 c e))"
```
```  1295       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp
```
```  1296   }
```
```  1297   then have "\<forall>x < ?z. ?P ?z x (Eq (CN 0 c e))" by simp
```
```  1298   then show ?case by blast
```
```  1299 next
```
```  1300   case (4 c e)
```
```  1301   from 4 have nb: "numbound0 e" by simp
```
```  1302   from 4 have cp: "real_of_int c > 0" by simp
```
```  1303   fix a
```
```  1304   let ?e = "Inum (a # bs) e"
```
```  1305   let ?z = "(- ?e) / real_of_int c"
```
```  1306   {
```
```  1307     fix x
```
```  1308     assume xz: "x < ?z"
```
```  1309     then have "(real_of_int c * x < - ?e)"
```
```  1310       by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps)
```
```  1311     then have "real_of_int c * x + ?e < 0" by arith
```
```  1312     then have "real_of_int c * x + ?e \<noteq> 0" by simp
```
```  1313     with xz have "?P ?z x (NEq (CN 0 c e))"
```
```  1314       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp
```
```  1315   }
```
```  1316   then have "\<forall>x < ?z. ?P ?z x (NEq (CN 0 c e))" by simp
```
```  1317   then show ?case by blast
```
```  1318 next
```
```  1319   case (5 c e)
```
```  1320   from 5 have nb: "numbound0 e" by simp
```
```  1321   from 5 have cp: "real_of_int c > 0" by simp
```
```  1322   fix a
```
```  1323   let ?e="Inum (a#bs) e"
```
```  1324   let ?z = "(- ?e) / real_of_int c"
```
```  1325   {
```
```  1326     fix x
```
```  1327     assume xz: "x < ?z"
```
```  1328     then have "(real_of_int c * x < - ?e)"
```
```  1329       by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps)
```
```  1330     then have "real_of_int c * x + ?e < 0" by arith
```
```  1331     with xz have "?P ?z x (Lt (CN 0 c e))"
```
```  1332       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"]  by simp
```
```  1333   }
```
```  1334   then have "\<forall>x < ?z. ?P ?z x (Lt (CN 0 c e))" by simp
```
```  1335   then show ?case by blast
```
```  1336 next
```
```  1337   case (6 c e)
```
```  1338   from 6 have nb: "numbound0 e" by simp
```
```  1339   from lp 6 have cp: "real_of_int c > 0" by simp
```
```  1340   fix a
```
```  1341   let ?e = "Inum (a # bs) e"
```
```  1342   let ?z = "(- ?e) / real_of_int c"
```
```  1343   {
```
```  1344     fix x
```
```  1345     assume xz: "x < ?z"
```
```  1346     then have "(real_of_int c * x < - ?e)"
```
```  1347       by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps)
```
```  1348     then have "real_of_int c * x + ?e < 0" by arith
```
```  1349     with xz have "?P ?z x (Le (CN 0 c e))"
```
```  1350       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp
```
```  1351   }
```
```  1352   then have "\<forall>x < ?z. ?P ?z x (Le (CN 0 c e))" by simp
```
```  1353   then show ?case by blast
```
```  1354 next
```
```  1355   case (7 c e)
```
```  1356   from 7 have nb: "numbound0 e" by simp
```
```  1357   from 7 have cp: "real_of_int c > 0" by simp
```
```  1358   fix a
```
```  1359   let ?e = "Inum (a # bs) e"
```
```  1360   let ?z = "(- ?e) / real_of_int c"
```
```  1361   {
```
```  1362     fix x
```
```  1363     assume xz: "x < ?z"
```
```  1364     then have "(real_of_int c * x < - ?e)"
```
```  1365       by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps)
```
```  1366     then have "real_of_int c * x + ?e < 0" by arith
```
```  1367     with xz have "?P ?z x (Gt (CN 0 c e))"
```
```  1368       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp
```
```  1369   }
```
```  1370   then have "\<forall>x < ?z. ?P ?z x (Gt (CN 0 c e))" by simp
```
```  1371   then show ?case by blast
```
```  1372 next
```
```  1373   case (8 c e)
```
```  1374   from 8 have nb: "numbound0 e" by simp
```
```  1375   from 8 have cp: "real_of_int c > 0" by simp
```
```  1376   fix a
```
```  1377   let ?e="Inum (a#bs) e"
```
```  1378   let ?z = "(- ?e) / real_of_int c"
```
```  1379   {
```
```  1380     fix x
```
```  1381     assume xz: "x < ?z"
```
```  1382     then have "(real_of_int c * x < - ?e)"
```
```  1383       by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps)
```
```  1384     then have "real_of_int c * x + ?e < 0" by arith
```
```  1385     with xz have "?P ?z x (Ge (CN 0 c e))"
```
```  1386       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp
```
```  1387   }
```
```  1388   then have "\<forall>x < ?z. ?P ?z x (Ge (CN 0 c e))" by simp
```
```  1389   then show ?case by blast
```
```  1390 qed simp_all
```
```  1391
```
```  1392 lemma rplusinf_inf:
```
```  1393   assumes lp: "isrlfm p"
```
```  1394   shows "\<exists>z. \<forall>x > z. Ifm (x#bs) (plusinf p) = Ifm (x#bs) p" (is "\<exists>z. \<forall>x. ?P z x p")
```
```  1395 using lp
```
```  1396 proof (induct p rule: isrlfm.induct)
```
```  1397   case (1 p q)
```
```  1398   then show ?case
```
```  1399     apply auto
```
```  1400     apply (rule_tac x= "max z za" in exI)
```
```  1401     apply auto
```
```  1402     done
```
```  1403 next
```
```  1404   case (2 p q)
```
```  1405   then show ?case
```
```  1406     apply auto
```
```  1407     apply (rule_tac x= "max z za" in exI)
```
```  1408     apply auto
```
```  1409     done
```
```  1410 next
```
```  1411   case (3 c e)
```
```  1412   from 3 have nb: "numbound0 e" by simp
```
```  1413   from 3 have cp: "real_of_int c > 0" by simp
```
```  1414   fix a
```
```  1415   let ?e = "Inum (a # bs) e"
```
```  1416   let ?z = "(- ?e) / real_of_int c"
```
```  1417   {
```
```  1418     fix x
```
```  1419     assume xz: "x > ?z"
```
```  1420     with mult_strict_right_mono [OF xz cp] cp
```
```  1421     have "(real_of_int c * x > - ?e)" by (simp add: ac_simps)
```
```  1422     then have "real_of_int c * x + ?e > 0" by arith
```
```  1423     then have "real_of_int c * x + ?e \<noteq> 0" by simp
```
```  1424     with xz have "?P ?z x (Eq (CN 0 c e))"
```
```  1425       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp
```
```  1426   }
```
```  1427   then have "\<forall>x > ?z. ?P ?z x (Eq (CN 0 c e))" by simp
```
```  1428   then show ?case by blast
```
```  1429 next
```
```  1430   case (4 c e)
```
```  1431   from 4 have nb: "numbound0 e" by simp
```
```  1432   from 4 have cp: "real_of_int c > 0" by simp
```
```  1433   fix a
```
```  1434   let ?e = "Inum (a # bs) e"
```
```  1435   let ?z = "(- ?e) / real_of_int c"
```
```  1436   {
```
```  1437     fix x
```
```  1438     assume xz: "x > ?z"
```
```  1439     with mult_strict_right_mono [OF xz cp] cp
```
```  1440     have "(real_of_int c * x > - ?e)" by (simp add: ac_simps)
```
```  1441     then have "real_of_int c * x + ?e > 0" by arith
```
```  1442     then have "real_of_int c * x + ?e \<noteq> 0" by simp
```
```  1443     with xz have "?P ?z x (NEq (CN 0 c e))"
```
```  1444       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp
```
```  1445   }
```
```  1446   then have "\<forall>x > ?z. ?P ?z x (NEq (CN 0 c e))" by simp
```
```  1447   then show ?case by blast
```
```  1448 next
```
```  1449   case (5 c e)
```
```  1450   from 5 have nb: "numbound0 e" by simp
```
```  1451   from 5 have cp: "real_of_int c > 0" by simp
```
```  1452   fix a
```
```  1453   let ?e = "Inum (a # bs) e"
```
```  1454   let ?z = "(- ?e) / real_of_int c"
```
```  1455   {
```
```  1456     fix x
```
```  1457     assume xz: "x > ?z"
```
```  1458     with mult_strict_right_mono [OF xz cp] cp
```
```  1459     have "(real_of_int c * x > - ?e)" by (simp add: ac_simps)
```
```  1460     then have "real_of_int c * x + ?e > 0" by arith
```
```  1461     with xz have "?P ?z x (Lt (CN 0 c e))"
```
```  1462       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp
```
```  1463   }
```
```  1464   then have "\<forall>x > ?z. ?P ?z x (Lt (CN 0 c e))" by simp
```
```  1465   then show ?case by blast
```
```  1466 next
```
```  1467   case (6 c e)
```
```  1468   from 6 have nb: "numbound0 e" by simp
```
```  1469   from 6 have cp: "real_of_int c > 0" by simp
```
```  1470   fix a
```
```  1471   let ?e = "Inum (a # bs) e"
```
```  1472   let ?z = "(- ?e) / real_of_int c"
```
```  1473   {
```
```  1474     fix x
```
```  1475     assume xz: "x > ?z"
```
```  1476     with mult_strict_right_mono [OF xz cp] cp
```
```  1477     have "(real_of_int c * x > - ?e)" by (simp add: ac_simps)
```
```  1478     then have "real_of_int c * x + ?e > 0" by arith
```
```  1479     with xz have "?P ?z x (Le (CN 0 c e))"
```
```  1480       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp
```
```  1481   }
```
```  1482   then have "\<forall>x > ?z. ?P ?z x (Le (CN 0 c e))" by simp
```
```  1483   then show ?case by blast
```
```  1484 next
```
```  1485   case (7 c e)
```
```  1486   from 7 have nb: "numbound0 e" by simp
```
```  1487   from 7 have cp: "real_of_int c > 0" by simp
```
```  1488   fix a
```
```  1489   let ?e = "Inum (a # bs) e"
```
```  1490   let ?z = "(- ?e) / real_of_int c"
```
```  1491   {
```
```  1492     fix x
```
```  1493     assume xz: "x > ?z"
```
```  1494     with mult_strict_right_mono [OF xz cp] cp
```
```  1495     have "(real_of_int c * x > - ?e)" by (simp add: ac_simps)
```
```  1496     then have "real_of_int c * x + ?e > 0" by arith
```
```  1497     with xz have "?P ?z x (Gt (CN 0 c e))"
```
```  1498       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp
```
```  1499   }
```
```  1500   then have "\<forall>x > ?z. ?P ?z x (Gt (CN 0 c e))" by simp
```
```  1501   then show ?case by blast
```
```  1502 next
```
```  1503   case (8 c e)
```
```  1504   from 8 have nb: "numbound0 e" by simp
```
```  1505   from 8 have cp: "real_of_int c > 0" by simp
```
```  1506   fix a
```
```  1507   let ?e="Inum (a#bs) e"
```
```  1508   let ?z = "(- ?e) / real_of_int c"
```
```  1509   {
```
```  1510     fix x
```
```  1511     assume xz: "x > ?z"
```
```  1512     with mult_strict_right_mono [OF xz cp] cp
```
```  1513     have "(real_of_int c * x > - ?e)" by (simp add: ac_simps)
```
```  1514     then have "real_of_int c * x + ?e > 0" by arith
```
```  1515     with xz have "?P ?z x (Ge (CN 0 c e))"
```
```  1516       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp
```
```  1517   }
```
```  1518   then have "\<forall>x > ?z. ?P ?z x (Ge (CN 0 c e))" by simp
```
```  1519   then show ?case by blast
```
```  1520 qed simp_all
```
```  1521
```
```  1522 lemma rminusinf_bound0:
```
```  1523   assumes lp: "isrlfm p"
```
```  1524   shows "bound0 (minusinf p)"
```
```  1525   using lp by (induct p rule: minusinf.induct) simp_all
```
```  1526
```
```  1527 lemma rplusinf_bound0:
```
```  1528   assumes lp: "isrlfm p"
```
```  1529   shows "bound0 (plusinf p)"
```
```  1530   using lp by (induct p rule: plusinf.induct) simp_all
```
```  1531
```
```  1532 lemma rminusinf_ex:
```
```  1533   assumes lp: "isrlfm p"
```
```  1534     and ex: "Ifm (a#bs) (minusinf p)"
```
```  1535   shows "\<exists>x. Ifm (x#bs) p"
```
```  1536 proof -
```
```  1537   from bound0_I [OF rminusinf_bound0[OF lp], where b="a" and bs ="bs"] ex
```
```  1538   have th: "\<forall>x. Ifm (x#bs) (minusinf p)" by auto
```
```  1539   from rminusinf_inf[OF lp, where bs="bs"]
```
```  1540   obtain z where z_def: "\<forall>x<z. Ifm (x # bs) (minusinf p) = Ifm (x # bs) p" by blast
```
```  1541   from th have "Ifm ((z - 1) # bs) (minusinf p)" by simp
```
```  1542   moreover have "z - 1 < z" by simp
```
```  1543   ultimately show ?thesis using z_def by auto
```
```  1544 qed
```
```  1545
```
```  1546 lemma rplusinf_ex:
```
```  1547   assumes lp: "isrlfm p"
```
```  1548     and ex: "Ifm (a # bs) (plusinf p)"
```
```  1549   shows "\<exists>x. Ifm (x # bs) p"
```
```  1550 proof -
```
```  1551   from bound0_I [OF rplusinf_bound0[OF lp], where b="a" and bs ="bs"] ex
```
```  1552   have th: "\<forall>x. Ifm (x # bs) (plusinf p)" by auto
```
```  1553   from rplusinf_inf[OF lp, where bs="bs"]
```
```  1554   obtain z where z_def: "\<forall>x>z. Ifm (x # bs) (plusinf p) = Ifm (x # bs) p" by blast
```
```  1555   from th have "Ifm ((z + 1) # bs) (plusinf p)" by simp
```
```  1556   moreover have "z + 1 > z" by simp
```
```  1557   ultimately show ?thesis using z_def by auto
```
```  1558 qed
```
```  1559
```
```  1560 fun uset :: "fm \<Rightarrow> (num \<times> int) list"
```
```  1561 where
```
```  1562   "uset (And p q) = (uset p @ uset q)"
```
```  1563 | "uset (Or p q) = (uset p @ uset q)"
```
```  1564 | "uset (Eq  (CN 0 c e)) = [(Neg e,c)]"
```
```  1565 | "uset (NEq (CN 0 c e)) = [(Neg e,c)]"
```
```  1566 | "uset (Lt  (CN 0 c e)) = [(Neg e,c)]"
```
```  1567 | "uset (Le  (CN 0 c e)) = [(Neg e,c)]"
```
```  1568 | "uset (Gt  (CN 0 c e)) = [(Neg e,c)]"
```
```  1569 | "uset (Ge  (CN 0 c e)) = [(Neg e,c)]"
```
```  1570 | "uset p = []"
```
```  1571
```
```  1572 fun usubst :: "fm \<Rightarrow> num \<times> int \<Rightarrow> fm"
```
```  1573 where
```
```  1574   "usubst (And p q) = (\<lambda>(t,n). And (usubst p (t,n)) (usubst q (t,n)))"
```
```  1575 | "usubst (Or p q) = (\<lambda>(t,n). Or (usubst p (t,n)) (usubst q (t,n)))"
```
```  1576 | "usubst (Eq (CN 0 c e)) = (\<lambda>(t,n). Eq (Add (Mul c t) (Mul n e)))"
```
```  1577 | "usubst (NEq (CN 0 c e)) = (\<lambda>(t,n). NEq (Add (Mul c t) (Mul n e)))"
```
```  1578 | "usubst (Lt (CN 0 c e)) = (\<lambda>(t,n). Lt (Add (Mul c t) (Mul n e)))"
```
```  1579 | "usubst (Le (CN 0 c e)) = (\<lambda>(t,n). Le (Add (Mul c t) (Mul n e)))"
```
```  1580 | "usubst (Gt (CN 0 c e)) = (\<lambda>(t,n). Gt (Add (Mul c t) (Mul n e)))"
```
```  1581 | "usubst (Ge (CN 0 c e)) = (\<lambda>(t,n). Ge (Add (Mul c t) (Mul n e)))"
```
```  1582 | "usubst p = (\<lambda>(t, n). p)"
```
```  1583
```
```  1584 lemma usubst_I:
```
```  1585   assumes lp: "isrlfm p"
```
```  1586     and np: "real_of_int n > 0"
```
```  1587     and nbt: "numbound0 t"
```
```  1588   shows "(Ifm (x # bs) (usubst p (t,n)) =
```
```  1589     Ifm (((Inum (x # bs) t) / (real_of_int n)) # bs) p) \<and> bound0 (usubst p (t, n))"
```
```  1590   (is "(?I x (usubst p (t, n)) = ?I ?u p) \<and> ?B p"
```
```  1591    is "(_ = ?I (?t/?n) p) \<and> _"
```
```  1592    is "(_ = ?I (?N x t /_) p) \<and> _")
```
```  1593   using lp
```
```  1594 proof (induct p rule: usubst.induct)
```
```  1595   case (5 c e)
```
```  1596   with assms have cp: "c > 0" and nb: "numbound0 e" by simp_all
```
```  1597   have "?I ?u (Lt (CN 0 c e)) \<longleftrightarrow> real_of_int c * (?t / ?n) + ?N x e < 0"
```
```  1598     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
```
```  1599   also have "\<dots> \<longleftrightarrow> ?n * (real_of_int c * (?t / ?n)) + ?n*(?N x e) < 0"
```
```  1600     by (simp only: pos_less_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
```
```  1601       and b="0", simplified div_0]) (simp only: algebra_simps)
```
```  1602   also have "\<dots> \<longleftrightarrow> real_of_int c * ?t + ?n * (?N x e) < 0" using np by simp
```
```  1603   finally show ?case using nbt nb by (simp add: algebra_simps)
```
```  1604 next
```
```  1605   case (6 c e)
```
```  1606   with assms have cp: "c > 0" and nb: "numbound0 e" by simp_all
```
```  1607   have "?I ?u (Le (CN 0 c e)) \<longleftrightarrow> real_of_int c * (?t / ?n) + ?N x e \<le> 0"
```
```  1608     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
```
```  1609   also have "\<dots> = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) \<le> 0)"
```
```  1610     by (simp only: pos_le_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
```
```  1611       and b="0", simplified div_0]) (simp only: algebra_simps)
```
```  1612   also have "\<dots> = (real_of_int c *?t + ?n* (?N x e) \<le> 0)" using np by simp
```
```  1613   finally show ?case using nbt nb by (simp add: algebra_simps)
```
```  1614 next
```
```  1615   case (7 c e)
```
```  1616   with assms have cp: "c >0" and nb: "numbound0 e" by simp_all
```
```  1617   have "?I ?u (Gt (CN 0 c e)) \<longleftrightarrow> real_of_int c *(?t / ?n) + ?N x e > 0"
```
```  1618     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
```
```  1619   also have "\<dots> \<longleftrightarrow> ?n * (real_of_int c * (?t / ?n)) + ?n * ?N x e > 0"
```
```  1620     by (simp only: pos_divide_less_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
```
```  1621       and b="0", simplified div_0]) (simp only: algebra_simps)
```
```  1622   also have "\<dots> \<longleftrightarrow> real_of_int c * ?t + ?n * ?N x e > 0" using np by simp
```
```  1623   finally show ?case using nbt nb by (simp add: algebra_simps)
```
```  1624 next
```
```  1625   case (8 c e)
```
```  1626   with assms have cp: "c > 0" and nb: "numbound0 e" by simp_all
```
```  1627   have "?I ?u (Ge (CN 0 c e)) \<longleftrightarrow> real_of_int c * (?t / ?n) + ?N x e \<ge> 0"
```
```  1628     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
```
```  1629   also have "\<dots> \<longleftrightarrow> ?n * (real_of_int c * (?t / ?n)) + ?n * ?N x e \<ge> 0"
```
```  1630     by (simp only: pos_divide_le_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
```
```  1631       and b="0", simplified div_0]) (simp only: algebra_simps)
```
```  1632   also have "\<dots> \<longleftrightarrow> real_of_int c * ?t + ?n * ?N x e \<ge> 0" using np by simp
```
```  1633   finally show ?case using nbt nb by (simp add: algebra_simps)
```
```  1634 next
```
```  1635   case (3 c e)
```
```  1636   with assms have cp: "c > 0" and nb: "numbound0 e" by simp_all
```
```  1637   from np have np: "real_of_int n \<noteq> 0" by simp
```
```  1638   have "?I ?u (Eq (CN 0 c e)) \<longleftrightarrow> real_of_int c * (?t / ?n) + ?N x e = 0"
```
```  1639     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
```
```  1640   also have "\<dots> \<longleftrightarrow> ?n * (real_of_int c * (?t / ?n)) + ?n * ?N x e = 0"
```
```  1641     by (simp only: nonzero_eq_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
```
```  1642       and b="0", simplified div_0]) (simp only: algebra_simps)
```
```  1643   also have "\<dots> \<longleftrightarrow> real_of_int c * ?t + ?n * ?N x e = 0" using np by simp
```
```  1644   finally show ?case using nbt nb by (simp add: algebra_simps)
```
```  1645 next
```
```  1646   case (4 c e) with assms have cp: "c >0" and nb: "numbound0 e" by simp_all
```
```  1647   from np have np: "real_of_int n \<noteq> 0" by simp
```
```  1648   have "?I ?u (NEq (CN 0 c e)) \<longleftrightarrow> real_of_int c * (?t / ?n) + ?N x e \<noteq> 0"
```
```  1649     using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
```
```  1650   also have "\<dots> \<longleftrightarrow> ?n * (real_of_int c * (?t / ?n)) + ?n * ?N x e \<noteq> 0"
```
```  1651     by (simp only: nonzero_eq_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
```
```  1652       and b="0", simplified div_0]) (simp only: algebra_simps)
```
```  1653   also have "\<dots> \<longleftrightarrow> real_of_int c * ?t + ?n * ?N x e \<noteq> 0" using np by simp
```
```  1654   finally show ?case using nbt nb by (simp add: algebra_simps)
```
```  1655 qed(simp_all add: nbt numbound0_I[where bs ="bs" and b="(Inum (x#bs) t)/ real_of_int n" and b'="x"])
```
```  1656
```
```  1657 lemma uset_l:
```
```  1658   assumes lp: "isrlfm p"
```
```  1659   shows "\<forall>(t,k) \<in> set (uset p). numbound0 t \<and> k > 0"
```
```  1660   using lp by (induct p rule: uset.induct) auto
```
```  1661
```
```  1662 lemma rminusinf_uset:
```
```  1663   assumes lp: "isrlfm p"
```
```  1664     and nmi: "\<not> (Ifm (a # bs) (minusinf p))" (is "\<not> (Ifm (a # bs) (?M p))")
```
```  1665     and ex: "Ifm (x#bs) p" (is "?I x p")
```
```  1666   shows "\<exists>(s,m) \<in> set (uset p). x \<ge> Inum (a#bs) s / real_of_int m"
```
```  1667     (is "\<exists>(s,m) \<in> ?U p. x \<ge> ?N a s / real_of_int m")
```
```  1668 proof -
```
```  1669   have "\<exists>(s,m) \<in> set (uset p). real_of_int m * x \<ge> Inum (a#bs) s"
```
```  1670     (is "\<exists>(s,m) \<in> ?U p. real_of_int m *x \<ge> ?N a s")
```
```  1671     using lp nmi ex
```
```  1672     by (induct p rule: minusinf.induct) (auto simp add:numbound0_I[where bs="bs" and b="a" and b'="x"])
```
```  1673   then obtain s m where smU: "(s,m) \<in> set (uset p)" and mx: "real_of_int m * x \<ge> ?N a s"
```
```  1674     by blast
```
```  1675   from uset_l[OF lp] smU have mp: "real_of_int m > 0"
```
```  1676     by auto
```
```  1677   from pos_divide_le_eq[OF mp, where a="x" and b="?N a s", symmetric] mx have "x \<ge> ?N a s / real_of_int m"
```
```  1678     by (auto simp add: mult.commute)
```
```  1679   then show ?thesis
```
```  1680     using smU by auto
```
```  1681 qed
```
```  1682
```
```  1683 lemma rplusinf_uset:
```
```  1684   assumes lp: "isrlfm p"
```
```  1685     and nmi: "\<not> (Ifm (a # bs) (plusinf p))" (is "\<not> (Ifm (a # bs) (?M p))")
```
```  1686     and ex: "Ifm (x # bs) p" (is "?I x p")
```
```  1687   shows "\<exists>(s,m) \<in> set (uset p). x \<le> Inum (a#bs) s / real_of_int m"
```
```  1688     (is "\<exists>(s,m) \<in> ?U p. x \<le> ?N a s / real_of_int m")
```
```  1689 proof -
```
```  1690   have "\<exists>(s,m) \<in> set (uset p). real_of_int m * x \<le> Inum (a#bs) s"
```
```  1691     (is "\<exists>(s,m) \<in> ?U p. real_of_int m *x \<le> ?N a s")
```
```  1692     using lp nmi ex
```
```  1693     by (induct p rule: minusinf.induct)
```
```  1694       (auto simp add:numbound0_I[where bs="bs" and b="a" and b'="x"])
```
```  1695   then obtain s m where smU: "(s,m) \<in> set (uset p)" and mx: "real_of_int m * x \<le> ?N a s"
```
```  1696     by blast
```
```  1697   from uset_l[OF lp] smU have mp: "real_of_int m > 0"
```
```  1698     by auto
```
```  1699   from pos_le_divide_eq[OF mp, where a="x" and b="?N a s", symmetric] mx have "x \<le> ?N a s / real_of_int m"
```
```  1700     by (auto simp add: mult.commute)
```
```  1701   then show ?thesis
```
```  1702     using smU by auto
```
```  1703 qed
```
```  1704
```
```  1705 lemma lin_dense:
```
```  1706   assumes lp: "isrlfm p"
```
```  1707     and noS: "\<forall>t. l < t \<and> t< u \<longrightarrow> t \<notin> (\<lambda>(t,n). Inum (x#bs) t / real_of_int n) ` set (uset p)"
```
```  1708       (is "\<forall>t. _ \<and> _ \<longrightarrow> t \<notin> (\<lambda>(t,n). ?N x t / real_of_int n ) ` (?U p)")
```
```  1709     and lx: "l < x"
```
```  1710     and xu:"x < u"
```
```  1711     and px:" Ifm (x#bs) p"
```
```  1712     and ly: "l < y" and yu: "y < u"
```
```  1713   shows "Ifm (y#bs) p"
```
```  1714   using lp px noS
```
```  1715 proof (induct p rule: isrlfm.induct)
```
```  1716   case (5 c e)
```
```  1717   then have cp: "real_of_int c > 0" and nb: "numbound0 e"
```
```  1718     by simp_all
```
```  1719   from 5 have "x * real_of_int c + ?N x e < 0"
```
```  1720     by (simp add: algebra_simps)
```
```  1721   then have pxc: "x < (- ?N x e) / real_of_int c"
```
```  1722     by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="-?N x e"])
```
```  1723   from 5 have noSc:"\<forall>t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real_of_int c"
```
```  1724     by auto
```
```  1725   with ly yu have yne: "y \<noteq> - ?N x e / real_of_int c"
```
```  1726     by auto
```
```  1727   then consider "y < (-?N x e)/ real_of_int c" | "y > (- ?N x e) / real_of_int c"
```
```  1728     by atomize_elim auto
```
```  1729   then show ?case
```
```  1730   proof cases
```
```  1731     case 1
```
```  1732     then have "y * real_of_int c < - ?N x e"
```
```  1733       by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric])
```
```  1734     then have "real_of_int c * y + ?N x e < 0"
```
```  1735       by (simp add: algebra_simps)
```
```  1736     then show ?thesis
```
```  1737       using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp
```
```  1738   next
```
```  1739     case 2
```
```  1740     with yu have eu: "u > (- ?N x e) / real_of_int c"
```
```  1741       by auto
```
```  1742     with noSc ly yu have "(- ?N x e) / real_of_int c \<le> l"
```
```  1743       by (cases "(- ?N x e) / real_of_int c > l") auto
```
```  1744     with lx pxc have False
```
```  1745       by auto
```
```  1746     then show ?thesis ..
```
```  1747   qed
```
```  1748 next
```
```  1749   case (6 c e)
```
```  1750   then have cp: "real_of_int c > 0" and nb: "numbound0 e"
```
```  1751     by simp_all
```
```  1752   from 6 have "x * real_of_int c + ?N x e \<le> 0"
```
```  1753     by (simp add: algebra_simps)
```
```  1754   then have pxc: "x \<le> (- ?N x e) / real_of_int c"
```
```  1755     by (simp only: pos_le_divide_eq[OF cp, where a="x" and b="-?N x e"])
```
```  1756   from 6 have noSc:"\<forall>t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real_of_int c"
```
```  1757     by auto
```
```  1758   with ly yu have yne: "y \<noteq> - ?N x e / real_of_int c"
```
```  1759     by auto
```
```  1760   then consider "y < (- ?N x e) / real_of_int c" | "y > (-?N x e) / real_of_int c"
```
```  1761     by atomize_elim auto
```
```  1762   then show ?case
```
```  1763   proof cases
```
```  1764     case 1
```
```  1765     then have "y * real_of_int c < - ?N x e"
```
```  1766       by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric])
```
```  1767     then have "real_of_int c * y + ?N x e < 0"
```
```  1768       by (simp add: algebra_simps)
```
```  1769     then show ?thesis
```
```  1770       using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp
```
```  1771   next
```
```  1772     case 2
```
```  1773     with yu have eu: "u > (- ?N x e) / real_of_int c"
```
```  1774       by auto
```
```  1775     with noSc ly yu have "(- ?N x e) / real_of_int c \<le> l"
```
```  1776       by (cases "(- ?N x e) / real_of_int c > l") auto
```
```  1777     with lx pxc have False
```
```  1778       by auto
```
```  1779     then show ?thesis ..
```
```  1780   qed
```
```  1781 next
```
```  1782   case (7 c e)
```
```  1783   then have cp: "real_of_int c > 0" and nb: "numbound0 e"
```
```  1784     by simp_all
```
```  1785   from 7 have "x * real_of_int c + ?N x e > 0"
```
```  1786     by (simp add: algebra_simps)
```
```  1787   then have pxc: "x > (- ?N x e) / real_of_int c"
```
```  1788     by (simp only: pos_divide_less_eq[OF cp, where a="x" and b="-?N x e"])
```
```  1789   from 7 have noSc: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real_of_int c"
```
```  1790     by auto
```
```  1791   with ly yu have yne: "y \<noteq> - ?N x e / real_of_int c"
```
```  1792     by auto
```
```  1793   then consider "y > (- ?N x e) / real_of_int c" | "y < (-?N x e) / real_of_int c"
```
```  1794     by atomize_elim auto
```
```  1795   then show ?case
```
```  1796   proof cases
```
```  1797     case 1
```
```  1798     then have "y * real_of_int c > - ?N x e"
```
```  1799       by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric])
```
```  1800     then have "real_of_int c * y + ?N x e > 0"
```
```  1801       by (simp add: algebra_simps)
```
```  1802     then show ?thesis
```
```  1803       using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp
```
```  1804   next
```
```  1805     case 2
```
```  1806     with ly have eu: "l < (- ?N x e) / real_of_int c"
```
```  1807       by auto
```
```  1808     with noSc ly yu have "(- ?N x e) / real_of_int c \<ge> u"
```
```  1809       by (cases "(- ?N x e) / real_of_int c > l") auto
```
```  1810     with xu pxc have False by auto
```
```  1811     then show ?thesis ..
```
```  1812   qed
```
```  1813 next
```
```  1814   case (8 c e)
```
```  1815   then have cp: "real_of_int c > 0" and nb: "numbound0 e"
```
```  1816     by simp_all
```
```  1817   from 8 have "x * real_of_int c + ?N x e \<ge> 0"
```
```  1818     by (simp add: algebra_simps)
```
```  1819   then have pxc: "x \<ge> (- ?N x e) / real_of_int c"
```
```  1820     by (simp only: pos_divide_le_eq[OF cp, where a="x" and b="-?N x e"])
```
```  1821   from 8 have noSc:"\<forall>t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real_of_int c"
```
```  1822     by auto
```
```  1823   with ly yu have yne: "y \<noteq> - ?N x e / real_of_int c"
```
```  1824     by auto
```
```  1825   then consider "y > (- ?N x e) / real_of_int c" | "y < (-?N x e) / real_of_int c"
```
```  1826     by atomize_elim auto
```
```  1827   then show ?case
```
```  1828   proof cases
```
```  1829     case 1
```
```  1830     then have "y * real_of_int c > - ?N x e"
```
```  1831       by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric])
```
```  1832     then have "real_of_int c * y + ?N x e > 0" by (simp add: algebra_simps)
```
```  1833     then show ?thesis
```
```  1834       using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp
```
```  1835   next
```
```  1836     case 2
```
```  1837     with ly have eu: "l < (- ?N x e) / real_of_int c"
```
```  1838       by auto
```
```  1839     with noSc ly yu have "(- ?N x e) / real_of_int c \<ge> u"
```
```  1840       by (cases "(- ?N x e) / real_of_int c > l") auto
```
```  1841     with xu pxc have False
```
```  1842       by auto
```
```  1843     then show ?thesis ..
```
```  1844   qed
```
```  1845 next
```
```  1846   case (3 c e)
```
```  1847   then have cp: "real_of_int c > 0" and nb: "numbound0 e"
```
```  1848     by simp_all
```
```  1849   from cp have cnz: "real_of_int c \<noteq> 0"
```
```  1850     by simp
```
```  1851   from 3 have "x * real_of_int c + ?N x e = 0"
```
```  1852     by (simp add: algebra_simps)
```
```  1853   then have pxc: "x = (- ?N x e) / real_of_int c"
```
```  1854     by (simp only: nonzero_eq_divide_eq[OF cnz, where a="x" and b="-?N x e"])
```
```  1855   from 3 have noSc:"\<forall>t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real_of_int c"
```
```  1856     by auto
```
```  1857   with lx xu have yne: "x \<noteq> - ?N x e / real_of_int c"
```
```  1858     by auto
```
```  1859   with pxc show ?case
```
```  1860     by simp
```
```  1861 next
```
```  1862   case (4 c e)
```
```  1863   then have cp: "real_of_int c > 0" and nb: "numbound0 e"
```
```  1864     by simp_all
```
```  1865   from cp have cnz: "real_of_int c \<noteq> 0"
```
```  1866     by simp
```
```  1867   from 4 have noSc:"\<forall>t. l < t \<and> t < u \<longrightarrow> t \<noteq> (- ?N x e) / real_of_int c"
```
```  1868     by auto
```
```  1869   with ly yu have yne: "y \<noteq> - ?N x e / real_of_int c"
```
```  1870     by auto
```
```  1871   then have "y* real_of_int c \<noteq> -?N x e"
```
```  1872     by (simp only: nonzero_eq_divide_eq[OF cnz, where a="y" and b="-?N x e"]) simp
```
```  1873   then have "y* real_of_int c + ?N x e \<noteq> 0"
```
```  1874     by (simp add: algebra_simps)
```
```  1875   then show ?case using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"]
```
```  1876     by (simp add: algebra_simps)
```
```  1877 qed (auto simp add: numbound0_I[where bs="bs" and b="y" and b'="x"])
```
```  1878
```
```  1879 lemma finite_set_intervals:
```
```  1880   fixes x :: real
```
```  1881   assumes px: "P x"
```
```  1882     and lx: "l \<le> x"
```
```  1883     and xu: "x \<le> u"
```
```  1884     and linS: "l\<in> S"
```
```  1885     and uinS: "u \<in> S"
```
```  1886     and fS: "finite S"
```
```  1887     and lS: "\<forall>x\<in> S. l \<le> x"
```
```  1888     and Su: "\<forall>x\<in> S. x \<le> u"
```
```  1889   shows "\<exists>a \<in> S. \<exists>b \<in> S. (\<forall>y. a < y \<and> y < b \<longrightarrow> y \<notin> S) \<and> a \<le> x \<and> x \<le> b \<and> P x"
```
```  1890 proof -
```
```  1891   let ?Mx = "{y. y\<in> S \<and> y \<le> x}"
```
```  1892   let ?xM = "{y. y\<in> S \<and> x \<le> y}"
```
```  1893   let ?a = "Max ?Mx"
```
```  1894   let ?b = "Min ?xM"
```
```  1895   have MxS: "?Mx \<subseteq> S"
```
```  1896     by blast
```
```  1897   then have fMx: "finite ?Mx"
```
```  1898     using fS finite_subset by auto
```
```  1899   from lx linS have linMx: "l \<in> ?Mx"
```
```  1900     by blast
```
```  1901   then have Mxne: "?Mx \<noteq> {}"
```
```  1902     by blast
```
```  1903   have xMS: "?xM \<subseteq> S"
```
```  1904     by blast
```
```  1905   then have fxM: "finite ?xM"
```
```  1906     using fS finite_subset by auto
```
```  1907   from xu uinS have linxM: "u \<in> ?xM"
```
```  1908     by blast
```
```  1909   then have xMne: "?xM \<noteq> {}"
```
```  1910     by blast
```
```  1911   have ax:"?a \<le> x"
```
```  1912     using Mxne fMx by auto
```
```  1913   have xb:"x \<le> ?b"
```
```  1914     using xMne fxM by auto
```
```  1915   have "?a \<in> ?Mx"
```
```  1916     using Max_in[OF fMx Mxne] by simp
```
```  1917   then have ainS: "?a \<in> S"
```
```  1918     using MxS by blast
```
```  1919   have "?b \<in> ?xM"
```
```  1920     using Min_in[OF fxM xMne] by simp
```
```  1921   then have binS: "?b \<in> S"
```
```  1922     using xMS by blast
```
```  1923   have noy: "\<forall>y. ?a < y \<and> y < ?b \<longrightarrow> y \<notin> S"
```
```  1924   proof clarsimp
```
```  1925     fix y
```
```  1926     assume ay: "?a < y" and yb: "y < ?b" and yS: "y \<in> S"
```
```  1927     from yS consider "y \<in> ?Mx" | "y \<in> ?xM"
```
```  1928       by atomize_elim auto
```
```  1929     then show False
```
```  1930     proof cases
```
```  1931       case 1
```
```  1932       then have "y \<le> ?a"
```
```  1933         using Mxne fMx by auto
```
```  1934       with ay show ?thesis by simp
```
```  1935     next
```
```  1936       case 2
```
```  1937       then have "y \<ge> ?b"
```
```  1938         using xMne fxM by auto
```
```  1939       with yb show ?thesis by simp
```
```  1940     qed
```
```  1941   qed
```
```  1942   from ainS binS noy ax xb px show ?thesis
```
```  1943     by blast
```
```  1944 qed
```
```  1945
```
```  1946 lemma rinf_uset:
```
```  1947   assumes lp: "isrlfm p"
```
```  1948     and nmi: "\<not> (Ifm (x # bs) (minusinf p))"  (is "\<not> (Ifm (x # bs) (?M p))")
```
```  1949     and npi: "\<not> (Ifm (x # bs) (plusinf p))"  (is "\<not> (Ifm (x # bs) (?P p))")
```
```  1950     and ex: "\<exists>x. Ifm (x # bs) p"  (is "\<exists>x. ?I x p")
```
```  1951   shows "\<exists>(l,n) \<in> set (uset p). \<exists>(s,m) \<in> set (uset p).
```
```  1952     ?I ((Inum (x#bs) l / real_of_int n + Inum (x#bs) s / real_of_int m) / 2) p"
```
```  1953 proof -
```
```  1954   let ?N = "\<lambda>x t. Inum (x # bs) t"
```
```  1955   let ?U = "set (uset p)"
```
```  1956   from ex obtain a where pa: "?I a p"
```
```  1957     by blast
```
```  1958   from bound0_I[OF rminusinf_bound0[OF lp], where bs="bs" and b="x" and b'="a"] nmi
```
```  1959   have nmi': "\<not> (?I a (?M p))"
```
```  1960     by simp
```
```  1961   from bound0_I[OF rplusinf_bound0[OF lp], where bs="bs" and b="x" and b'="a"] npi
```
```  1962   have npi': "\<not> (?I a (?P p))"
```
```  1963     by simp
```
```  1964   have "\<exists>(l,n) \<in> set (uset p). \<exists>(s,m) \<in> set (uset p). ?I ((?N a l/real_of_int n + ?N a s /real_of_int m) / 2) p"
```
```  1965   proof -
```
```  1966     let ?M = "(\<lambda>(t,c). ?N a t / real_of_int c) ` ?U"
```
```  1967     have fM: "finite ?M"
```
```  1968       by auto
```
```  1969     from rminusinf_uset[OF lp nmi pa] rplusinf_uset[OF lp npi pa]
```
```  1970     have "\<exists>(l,n) \<in> set (uset p). \<exists>(s,m) \<in> set (uset p). a \<le> ?N x l / real_of_int n \<and> a \<ge> ?N x s / real_of_int m"
```
```  1971       by blast
```
```  1972     then obtain "t" "n" "s" "m"
```
```  1973       where tnU: "(t,n) \<in> ?U"
```
```  1974         and smU: "(s,m) \<in> ?U"
```
```  1975         and xs1: "a \<le> ?N x s / real_of_int m"
```
```  1976         and tx1: "a \<ge> ?N x t / real_of_int n"
```
```  1977       by blast
```
```  1978     from uset_l[OF lp] tnU smU numbound0_I[where bs="bs" and b="x" and b'="a"] xs1 tx1
```
```  1979     have xs: "a \<le> ?N a s / real_of_int m" and tx: "a \<ge> ?N a t / real_of_int n"
```
```  1980       by auto
```
```  1981     from tnU have Mne: "?M \<noteq> {}"
```
```  1982       by auto
```
```  1983     then have Une: "?U \<noteq> {}"
```
```  1984       by simp
```
```  1985     let ?l = "Min ?M"
```
```  1986     let ?u = "Max ?M"
```
```  1987     have linM: "?l \<in> ?M"
```
```  1988       using fM Mne by simp
```
```  1989     have uinM: "?u \<in> ?M"
```
```  1990       using fM Mne by simp
```
```  1991     have tnM: "?N a t / real_of_int n \<in> ?M"
```
```  1992       using tnU by auto
```
```  1993     have smM: "?N a s / real_of_int m \<in> ?M"
```
```  1994       using smU by auto
```
```  1995     have lM: "\<forall>t\<in> ?M. ?l \<le> t"
```
```  1996       using Mne fM by auto
```
```  1997     have Mu: "\<forall>t\<in> ?M. t \<le> ?u"
```
```  1998       using Mne fM by auto
```
```  1999     have "?l \<le> ?N a t / real_of_int n"
```
```  2000       using tnM Mne by simp
```
```  2001     then have lx: "?l \<le> a"
```
```  2002       using tx by simp
```
```  2003     have "?N a s / real_of_int m \<le> ?u"
```
```  2004       using smM Mne by simp
```
```  2005     then have xu: "a \<le> ?u"
```
```  2006       using xs by simp
```
```  2007     from finite_set_intervals2[where P="\<lambda>x. ?I x p",OF pa lx xu linM uinM fM lM Mu]
```
```  2008     consider u where "u \<in> ?M" "?I u p"
```
```  2009       | t1 t2 where "t1 \<in> ?M" "t2 \<in> ?M" "\<forall>y. t1 < y \<and> y < t2 \<longrightarrow> y \<notin> ?M" "t1 < a" "a < t2" "?I a p"
```
```  2010       by blast
```
```  2011     then show ?thesis
```
```  2012     proof cases
```
```  2013       case 1
```
```  2014       note um = \<open>u \<in> ?M\<close> and pu = \<open>?I u p\<close>
```
```  2015       then have "\<exists>(tu,nu) \<in> ?U. u = ?N a tu / real_of_int nu"
```
```  2016         by auto
```
```  2017       then obtain tu nu where tuU: "(tu, nu) \<in> ?U" and tuu: "u= ?N a tu / real_of_int nu"
```
```  2018         by blast
```
```  2019       have "(u + u) / 2 = u"
```
```  2020         by auto
```
```  2021       with pu tuu have "?I (((?N a tu / real_of_int nu) + (?N a tu / real_of_int nu)) / 2) p"
```
```  2022         by simp
```
```  2023       with tuU show ?thesis by blast
```
```  2024     next
```
```  2025       case 2
```
```  2026       note t1M = \<open>t1 \<in> ?M\<close> and t2M = \<open>t2\<in> ?M\<close>
```
```  2027         and noM = \<open>\<forall>y. t1 < y \<and> y < t2 \<longrightarrow> y \<notin> ?M\<close>
```
```  2028         and t1x = \<open>t1 < a\<close> and xt2 = \<open>a < t2\<close> and px = \<open>?I a p\<close>
```
```  2029       from t1M have "\<exists>(t1u,t1n) \<in> ?U. t1 = ?N a t1u / real_of_int t1n"
```
```  2030         by auto
```
```  2031       then obtain t1u t1n where t1uU: "(t1u, t1n) \<in> ?U" and t1u: "t1 = ?N a t1u / real_of_int t1n"
```
```  2032         by blast
```
```  2033       from t2M have "\<exists>(t2u,t2n) \<in> ?U. t2 = ?N a t2u / real_of_int t2n"
```
```  2034         by auto
```
```  2035       then obtain t2u t2n where t2uU: "(t2u, t2n) \<in> ?U" and t2u: "t2 = ?N a t2u / real_of_int t2n"
```
```  2036         by blast
```
```  2037       from t1x xt2 have t1t2: "t1 < t2"
```
```  2038         by simp
```
```  2039       let ?u = "(t1 + t2) / 2"
```
```  2040       from less_half_sum[OF t1t2] gt_half_sum[OF t1t2] have t1lu: "t1 < ?u" and ut2: "?u < t2"
```
```  2041         by auto
```
```  2042       from lin_dense[OF lp noM t1x xt2 px t1lu ut2] have "?I ?u p" .
```
```  2043       with t1uU t2uU t1u t2u show ?thesis
```
```  2044         by blast
```
```  2045     qed
```
```  2046   qed
```
```  2047   then obtain l n s m where lnU: "(l, n) \<in> ?U" and smU:"(s, m) \<in> ?U"
```
```  2048     and pu: "?I ((?N a l / real_of_int n + ?N a s / real_of_int m) / 2) p"
```
```  2049     by blast
```
```  2050   from lnU smU uset_l[OF lp] have nbl: "numbound0 l" and nbs: "numbound0 s"
```
```  2051     by auto
```
```  2052   from numbound0_I[OF nbl, where bs="bs" and b="a" and b'="x"]
```
```  2053     numbound0_I[OF nbs, where bs="bs" and b="a" and b'="x"] pu
```
```  2054   have "?I ((?N x l / real_of_int n + ?N x s / real_of_int m) / 2) p"
```
```  2055     by simp
```
```  2056   with lnU smU show ?thesis
```
```  2057     by auto
```
```  2058 qed
```
```  2059
```
```  2060
```
```  2061     (* The Ferrante - Rackoff Theorem *)
```
```  2062
```
```  2063 theorem fr_eq:
```
```  2064   assumes lp: "isrlfm p"
```
```  2065   shows "(\<exists>x. Ifm (x#bs) p) \<longleftrightarrow>
```
```  2066     Ifm (x # bs) (minusinf p) \<or> Ifm (x # bs) (plusinf p) \<or>
```
```  2067       (\<exists>(t,n) \<in> set (uset p). \<exists>(s,m) \<in> set (uset p).
```
```  2068         Ifm ((((Inum (x # bs) t) / real_of_int n + (Inum (x # bs) s) / real_of_int m) / 2) # bs) p)"
```
```  2069   (is "(\<exists>x. ?I x p) \<longleftrightarrow> (?M \<or> ?P \<or> ?F)" is "?E = ?D")
```
```  2070 proof
```
```  2071   assume px: "\<exists>x. ?I x p"
```
```  2072   consider "?M \<or> ?P" | "\<not> ?M" "\<not> ?P" by blast
```
```  2073   then show ?D
```
```  2074   proof cases
```
```  2075     case 1
```
```  2076     then show ?thesis by blast
```
```  2077   next
```
```  2078     case 2
```
```  2079     from rinf_uset[OF lp this] have ?F
```
```  2080       using px by blast
```
```  2081     then show ?thesis by blast
```
```  2082   qed
```
```  2083 next
```
```  2084   assume ?D
```
```  2085   then consider ?M | ?P | ?F by blast
```
```  2086   then show ?E
```
```  2087   proof cases
```
```  2088     case 1
```
```  2089     from rminusinf_ex[OF lp this] show ?thesis .
```
```  2090   next
```
```  2091     case 2
```
```  2092     from rplusinf_ex[OF lp this] show ?thesis .
```
```  2093   next
```
```  2094     case 3
```
```  2095     then show ?thesis by blast
```
```  2096   qed
```
```  2097 qed
```
```  2098
```
```  2099
```
```  2100 lemma fr_equsubst:
```
```  2101   assumes lp: "isrlfm p"
```
```  2102   shows "(\<exists>x. Ifm (x # bs) p) \<longleftrightarrow>
```
```  2103     (Ifm (x # bs) (minusinf p) \<or> Ifm (x # bs) (plusinf p) \<or>
```
```  2104       (\<exists>(t,k) \<in> set (uset p). \<exists>(s,l) \<in> set (uset p).
```
```  2105         Ifm (x#bs) (usubst p (Add (Mul l t) (Mul k s), 2 * k * l))))"
```
```  2106   (is "(\<exists>x. ?I x p) \<longleftrightarrow> ?M \<or> ?P \<or> ?F" is "?E = ?D")
```
```  2107 proof
```
```  2108   assume px: "\<exists>x. ?I x p"
```
```  2109   consider "?M \<or> ?P" | "\<not> ?M" "\<not> ?P" by blast
```
```  2110   then show ?D
```
```  2111   proof cases
```
```  2112     case 1
```
```  2113     then show ?thesis by blast
```
```  2114   next
```
```  2115     case 2
```
```  2116     let ?f = "\<lambda>(t,n). Inum (x # bs) t / real_of_int n"
```
```  2117     let ?N = "\<lambda>t. Inum (x # bs) t"
```
```  2118     {
```
```  2119       fix t n s m
```
```  2120       assume "(t, n) \<in> set (uset p)" and "(s, m) \<in> set (uset p)"
```
```  2121       with uset_l[OF lp] have tnb: "numbound0 t"
```
```  2122         and np: "real_of_int n > 0" and snb: "numbound0 s" and mp: "real_of_int m > 0"
```
```  2123         by auto
```
```  2124       let ?st = "Add (Mul m t) (Mul n s)"
```
```  2125       from np mp have mnp: "real_of_int (2 * n * m) > 0"
```
```  2126         by (simp add: mult.commute)
```
```  2127       from tnb snb have st_nb: "numbound0 ?st"
```
```  2128         by simp
```
```  2129       have st: "(?N t / real_of_int n + ?N s / real_of_int m) / 2 = ?N ?st / real_of_int (2 * n * m)"
```
```  2130         using mnp mp np by (simp add: algebra_simps add_divide_distrib)
```
```  2131       from usubst_I[OF lp mnp st_nb, where x="x" and bs="bs"]
```
```  2132       have "?I x (usubst p (?st, 2 * n * m)) = ?I ((?N t / real_of_int n + ?N s / real_of_int m) / 2) p"
```
```  2133         by (simp only: st[symmetric])
```
```  2134     }
```
```  2135     with rinf_uset[OF lp 2 px] have ?F
```
```  2136       by blast
```
```  2137     then show ?thesis
```
```  2138       by blast
```
```  2139   qed
```
```  2140 next
```
```  2141   assume ?D
```
```  2142   then consider ?M | ?P | t k s l where "(t, k) \<in> set (uset p)" "(s, l) \<in> set (uset p)"
```
```  2143     "?I x (usubst p (Add (Mul l t) (Mul k s), 2 * k * l))"
```
```  2144     by blast
```
```  2145   then show ?E
```
```  2146   proof cases
```
```  2147     case 1
```
```  2148     from rminusinf_ex[OF lp this] show ?thesis .
```
```  2149   next
```
```  2150     case 2
```
```  2151     from rplusinf_ex[OF lp this] show ?thesis .
```
```  2152   next
```
```  2153     case 3
```
```  2154     with uset_l[OF lp] have tnb: "numbound0 t" and np: "real_of_int k > 0"
```
```  2155       and snb: "numbound0 s" and mp: "real_of_int l > 0"
```
```  2156       by auto
```
```  2157     let ?st = "Add (Mul l t) (Mul k s)"
```
```  2158     from np mp have mnp: "real_of_int (2 * k * l) > 0"
```
```  2159       by (simp add: mult.commute)
```
```  2160     from tnb snb have st_nb: "numbound0 ?st"
```
```  2161       by simp
```
```  2162     from usubst_I[OF lp mnp st_nb, where bs="bs"]
```
```  2163       \<open>?I x (usubst p (Add (Mul l t) (Mul k s), 2 * k * l))\<close> show ?thesis
```
```  2164       by auto
```
```  2165   qed
```
```  2166 qed
```
```  2167
```
```  2168
```
```  2169     (* Implement the right hand side of Ferrante and Rackoff's Theorem. *)
```
```  2170 definition ferrack :: "fm \<Rightarrow> fm"
```
```  2171 where
```
```  2172   "ferrack p =
```
```  2173    (let
```
```  2174       p' = rlfm (simpfm p);
```
```  2175       mp = minusinf p';
```
```  2176       pp = plusinf p'
```
```  2177     in
```
```  2178       if mp = T \<or> pp = T then T
```
```  2179       else
```
```  2180        (let U = remdups (map simp_num_pair
```
```  2181          (map (\<lambda>((t,n),(s,m)). (Add (Mul m t) (Mul n s) , 2 * n * m))
```
```  2182                (alluopairs (uset p'))))
```
```  2183         in decr (disj mp (disj pp (evaldjf (simpfm \<circ> usubst p') U)))))"
```
```  2184
```
```  2185 lemma uset_cong_aux:
```
```  2186   assumes Ul: "\<forall>(t,n) \<in> set U. numbound0 t \<and> n > 0"
```
```  2187   shows "((\<lambda>(t,n). Inum (x # bs) t / real_of_int n) `
```
```  2188     (set (map (\<lambda>((t,n),(s,m)). (Add (Mul m t) (Mul n s), 2 * n * m)) (alluopairs U)))) =
```
```  2189     ((\<lambda>((t,n),(s,m)). (Inum (x # bs) t / real_of_int n + Inum (x # bs) s / real_of_int m) / 2) ` (set U \<times> set U))"
```
```  2190   (is "?lhs = ?rhs")
```
```  2191 proof auto
```
```  2192   fix t n s m
```
```  2193   assume "((t, n), (s, m)) \<in> set (alluopairs U)"
```
```  2194   then have th: "((t, n), (s, m)) \<in> set U \<times> set U"
```
```  2195     using alluopairs_set1[where xs="U"] by blast
```
```  2196   let ?N = "\<lambda>t. Inum (x # bs) t"
```
```  2197   let ?st = "Add (Mul m t) (Mul n s)"
```
```  2198   from Ul th have mnz: "m \<noteq> 0"
```
```  2199     by auto
```
```  2200   from Ul th have nnz: "n \<noteq> 0"
```
```  2201     by auto
```
```  2202   have st: "(?N t / real_of_int n + ?N s / real_of_int m) / 2 = ?N ?st / real_of_int (2 * n * m)"
```
```  2203     using mnz nnz by (simp add: algebra_simps add_divide_distrib)
```
```  2204   then show "(real_of_int m *  Inum (x # bs) t + real_of_int n * Inum (x # bs) s) / (2 * real_of_int n * real_of_int m)
```
```  2205       \<in> (\<lambda>((t, n), s, m). (Inum (x # bs) t / real_of_int n + Inum (x # bs) s / real_of_int m) / 2) `
```
```  2206          (set U \<times> set U)"
```
```  2207     using mnz nnz th
```
```  2208     apply (auto simp add: th add_divide_distrib algebra_simps split_def image_def)
```
```  2209     apply (rule_tac x="(s,m)" in bexI)
```
```  2210     apply simp_all
```
```  2211     apply (rule_tac x="(t,n)" in bexI)
```
```  2212     apply (simp_all add: mult.commute)
```
```  2213     done
```
```  2214 next
```
```  2215   fix t n s m
```
```  2216   assume tnU: "(t, n) \<in> set U" and smU: "(s, m) \<in> set U"
```
```  2217   let ?N = "\<lambda>t. Inum (x # bs) t"
```
```  2218   let ?st = "Add (Mul m t) (Mul n s)"
```
```  2219   from Ul smU have mnz: "m \<noteq> 0"
```
```  2220     by auto
```
```  2221   from Ul tnU have nnz: "n \<noteq> 0"
```
```  2222     by auto
```
```  2223   have st: "(?N t / real_of_int n + ?N s / real_of_int m) / 2 = ?N ?st / real_of_int (2 * n * m)"
```
```  2224     using mnz nnz by (simp add: algebra_simps add_divide_distrib)
```
```  2225   let ?P = "\<lambda>(t',n') (s',m'). (Inum (x # bs) t / real_of_int n + Inum (x # bs) s / real_of_int m)/2 =
```
```  2226     (Inum (x # bs) t' / real_of_int n' + Inum (x # bs) s' / real_of_int m') / 2"
```
```  2227   have Pc:"\<forall>a b. ?P a b = ?P b a"
```
```  2228     by auto
```
```  2229   from Ul alluopairs_set1 have Up:"\<forall>((t,n),(s,m)) \<in> set (alluopairs U). n \<noteq> 0 \<and> m \<noteq> 0"
```
```  2230     by blast
```
```  2231   from alluopairs_ex[OF Pc, where xs="U"] tnU smU
```
```  2232   have th':"\<exists>((t',n'),(s',m')) \<in> set (alluopairs U). ?P (t',n') (s',m')"
```
```  2233     by blast
```
```  2234   then obtain t' n' s' m' where ts'_U: "((t',n'),(s',m')) \<in> set (alluopairs U)"
```
```  2235     and Pts': "?P (t', n') (s', m')"
```
```  2236     by blast
```
```  2237   from ts'_U Up have mnz': "m' \<noteq> 0" and nnz': "n'\<noteq> 0"
```
```  2238     by auto
```
```  2239   let ?st' = "Add (Mul m' t') (Mul n' s')"
```
```  2240   have st': "(?N t' / real_of_int n' + ?N s' / real_of_int m') / 2 = ?N ?st' / real_of_int (2 * n' * m')"
```
```  2241     using mnz' nnz' by (simp add: algebra_simps add_divide_distrib)
```
```  2242   from Pts' have "(Inum (x # bs) t / real_of_int n + Inum (x # bs) s / real_of_int m) / 2 =
```
```  2243     (Inum (x # bs) t' / real_of_int n' + Inum (x # bs) s' / real_of_int m') / 2"
```
```  2244     by simp
```
```  2245   also have "\<dots> = (\<lambda>(t, n). Inum (x # bs) t / real_of_int n)
```
```  2246       ((\<lambda>((t, n), s, m). (Add (Mul m t) (Mul n s), 2 * n * m)) ((t', n'), (s', m')))"
```
```  2247     by (simp add: st')
```
```  2248   finally show "(Inum (x # bs) t / real_of_int n + Inum (x # bs) s / real_of_int m) / 2
```
```  2249     \<in> (\<lambda>(t, n). Inum (x # bs) t / real_of_int n) `
```
```  2250       (\<lambda>((t, n), s, m). (Add (Mul m t) (Mul n s), 2 * n * m)) ` set (alluopairs U)"
```
```  2251     using ts'_U by blast
```
```  2252 qed
```
```  2253
```
```  2254 lemma uset_cong:
```
```  2255   assumes lp: "isrlfm p"
```
```  2256     and UU': "((\<lambda>(t,n). Inum (x # bs) t / real_of_int n) ` U') =
```
```  2257       ((\<lambda>((t,n),(s,m)). (Inum (x # bs) t / real_of_int n + Inum (x # bs) s / real_of_int m) / 2) ` (U \<times> U))"
```
```  2258       (is "?f ` U' = ?g ` (U \<times> U)")
```
```  2259     and U: "\<forall>(t,n) \<in> U. numbound0 t \<and> n > 0"
```
```  2260     and U': "\<forall>(t,n) \<in> U'. numbound0 t \<and> n > 0"
```
```  2261   shows "(\<exists>(t,n) \<in> U. \<exists>(s,m) \<in> U. Ifm (x # bs) (usubst p (Add (Mul m t) (Mul n s), 2 * n * m))) =
```
```  2262     (\<exists>(t,n) \<in> U'. Ifm (x # bs) (usubst p (t, n)))"
```
```  2263     (is "?lhs \<longleftrightarrow> ?rhs")
```
```  2264 proof
```
```  2265   show ?rhs if ?lhs
```
```  2266   proof -
```
```  2267     from that obtain t n s m where tnU: "(t, n) \<in> U" and smU: "(s, m) \<in> U"
```
```  2268       and Pst: "Ifm (x # bs) (usubst p (Add (Mul m t) (Mul n s), 2 * n * m))"
```
```  2269       by blast
```
```  2270     let ?N = "\<lambda>t. Inum (x#bs) t"
```
```  2271     from tnU smU U have tnb: "numbound0 t" and np: "n > 0"
```
```  2272       and snb: "numbound0 s" and mp: "m > 0"
```
```  2273       by auto
```
```  2274     let ?st = "Add (Mul m t) (Mul n s)"
```
```  2275     from np mp have mnp: "real_of_int (2 * n * m) > 0"
```
```  2276       by (simp add: mult.commute of_int_mult[symmetric] del: of_int_mult)
```
```  2277     from tnb snb have stnb: "numbound0 ?st"
```
```  2278       by simp
```
```  2279     have st: "(?N t / real_of_int n + ?N s / real_of_int m) / 2 = ?N ?st / real_of_int (2 * n * m)"
```
```  2280       using mp np by (simp add: algebra_simps add_divide_distrib)
```
```  2281     from tnU smU UU' have "?g ((t, n), (s, m)) \<in> ?f ` U'"
```
```  2282       by blast
```
```  2283     then have "\<exists>(t',n') \<in> U'. ?g ((t, n), (s, m)) = ?f (t', n')"
```
```  2284       apply auto
```
```  2285       apply (rule_tac x="(a, b)" in bexI)
```
```  2286       apply auto
```
```  2287       done
```
```  2288     then obtain t' n' where tnU': "(t',n') \<in> U'" and th: "?g ((t, n), (s, m)) = ?f (t', n')"
```
```  2289       by blast
```
```  2290     from U' tnU' have tnb': "numbound0 t'" and np': "real_of_int n' > 0"
```
```  2291       by auto
```
```  2292     from usubst_I[OF lp mnp stnb, where bs="bs" and x="x"] Pst
```
```  2293     have Pst2: "Ifm (Inum (x # bs) (Add (Mul m t) (Mul n s)) / real_of_int (2 * n * m) # bs) p"
```
```  2294       by simp
```
```  2295     from conjunct1[OF usubst_I[OF lp np' tnb', where bs="bs" and x="x"], symmetric]
```
```  2296       th[simplified split_def fst_conv snd_conv,symmetric] Pst2[simplified st[symmetric]]
```
```  2297     have "Ifm (x # bs) (usubst p (t', n'))"
```
```  2298       by (simp only: st)
```
```  2299     then show ?thesis
```
```  2300       using tnU' by auto
```
```  2301   qed
```
```  2302   show ?lhs if ?rhs
```
```  2303   proof -
```
```  2304     from that obtain t' n' where tnU': "(t', n') \<in> U'" and Pt': "Ifm (x # bs) (usubst p (t', n'))"
```
```  2305       by blast
```
```  2306     from tnU' UU' have "?f (t', n') \<in> ?g ` (U \<times> U)"
```
```  2307       by blast
```
```  2308     then have "\<exists>((t,n),(s,m)) \<in> U \<times> U. ?f (t', n') = ?g ((t, n), (s, m))"
```
```  2309       apply auto
```
```  2310       apply (rule_tac x="(a,b)" in bexI)
```
```  2311       apply auto
```
```  2312       done
```
```  2313     then obtain t n s m where tnU: "(t, n) \<in> U" and smU: "(s, m) \<in> U" and
```
```  2314       th: "?f (t', n') = ?g ((t, n), (s, m))"
```
```  2315       by blast
```
```  2316     let ?N = "\<lambda>t. Inum (x # bs) t"
```
```  2317     from tnU smU U have tnb: "numbound0 t" and np: "n > 0"
```
```  2318       and snb: "numbound0 s" and mp: "m > 0"
```
```  2319       by auto
```
```  2320     let ?st = "Add (Mul m t) (Mul n s)"
```
```  2321     from np mp have mnp: "real_of_int (2 * n * m) > 0"
```
```  2322       by (simp add: mult.commute of_int_mult[symmetric] del: of_int_mult)
```
```  2323     from tnb snb have stnb: "numbound0 ?st"
```
```  2324       by simp
```
```  2325     have st: "(?N t / real_of_int n + ?N s / real_of_int m) / 2 = ?N ?st / real_of_int (2 * n * m)"
```
```  2326       using mp np by (simp add: algebra_simps add_divide_distrib)
```
```  2327     from U' tnU' have tnb': "numbound0 t'" and np': "real_of_int n' > 0"
```
```  2328       by auto
```
```  2329     from usubst_I[OF lp np' tnb', where bs="bs" and x="x",simplified
```
```  2330       th[simplified split_def fst_conv snd_conv] st] Pt'
```
```  2331     have Pst2: "Ifm (Inum (x # bs) (Add (Mul m t) (Mul n s)) / real_of_int (2 * n * m) # bs) p"
```
```  2332       by simp
```
```  2333     with usubst_I[OF lp mnp stnb, where x="x" and bs="bs"] tnU smU
```
```  2334     show ?thesis by blast
```
```  2335   qed
```
```  2336 qed
```
```  2337
```
```  2338 lemma ferrack:
```
```  2339   assumes qf: "qfree p"
```
```  2340   shows "qfree (ferrack p) \<and> (Ifm bs (ferrack p) \<longleftrightarrow> (\<exists>x. Ifm (x # bs) p))"
```
```  2341   (is "_ \<and> (?rhs \<longleftrightarrow> ?lhs)")
```
```  2342 proof -
```
```  2343   let ?I = "\<lambda>x p. Ifm (x # bs) p"
```
```  2344   fix x
```
```  2345   let ?N = "\<lambda>t. Inum (x # bs) t"
```
```  2346   let ?q = "rlfm (simpfm p)"
```
```  2347   let ?U = "uset ?q"
```
```  2348   let ?Up = "alluopairs ?U"
```
```  2349   let ?g = "\<lambda>((t,n),(s,m)). (Add (Mul m t) (Mul n s), 2 * n * m)"
```
```  2350   let ?S = "map ?g ?Up"
```
```  2351   let ?SS = "map simp_num_pair ?S"
```
```  2352   let ?Y = "remdups ?SS"
```
```  2353   let ?f = "\<lambda>(t,n). ?N t / real_of_int n"
```
```  2354   let ?h = "\<lambda>((t,n),(s,m)). (?N t / real_of_int n + ?N s / real_of_int m) / 2"
```
```  2355   let ?F = "\<lambda>p. \<exists>a \<in> set (uset p). \<exists>b \<in> set (uset p). ?I x (usubst p (?g (a, b)))"
```
```  2356   let ?ep = "evaldjf (simpfm \<circ> (usubst ?q)) ?Y"
```
```  2357   from rlfm_I[OF simpfm_qf[OF qf]] have lq: "isrlfm ?q"
```
```  2358     by blast
```
```  2359   from alluopairs_set1[where xs="?U"] have UpU: "set ?Up \<subseteq> set ?U \<times> set ?U"
```
```  2360     by simp
```
```  2361   from uset_l[OF lq] have U_l: "\<forall>(t,n) \<in> set ?U. numbound0 t \<and> n > 0" .
```
```  2362   from U_l UpU
```
```  2363   have "\<forall>((t,n),(s,m)) \<in> set ?Up. numbound0 t \<and> n> 0 \<and> numbound0 s \<and> m > 0"
```
```  2364     by auto
```
```  2365   then have Snb: "\<forall>(t,n) \<in> set ?S. numbound0 t \<and> n > 0 "
```
```  2366     by auto
```
```  2367   have Y_l: "\<forall>(t,n) \<in> set ?Y. numbound0 t \<and> n > 0"
```
```  2368   proof -
```
```  2369     have "numbound0 t \<and> n > 0" if tnY: "(t, n) \<in> set ?Y" for t n
```
```  2370     proof -
```
```  2371       from that have "(t,n) \<in> set ?SS"
```
```  2372         by simp
```
```  2373       then have "\<exists>(t',n') \<in> set ?S. simp_num_pair (t', n') = (t, n)"
```
```  2374         apply (auto simp add: split_def simp del: map_map)
```
```  2375         apply (rule_tac x="((aa,ba),(ab,bb))" in bexI)
```
```  2376         apply simp_all
```
```  2377         done
```
```  2378       then obtain t' n' where tn'S: "(t', n') \<in> set ?S" and tns: "simp_num_pair (t', n') = (t, n)"
```
```  2379         by blast
```
```  2380       from tn'S Snb have tnb: "numbound0 t'" and np: "n' > 0"
```
```  2381         by auto
```
```  2382       from simp_num_pair_l[OF tnb np tns] show ?thesis .
```
```  2383     qed
```
```  2384     then show ?thesis by blast
```
```  2385   qed
```
```  2386
```
```  2387   have YU: "(?f ` set ?Y) = (?h ` (set ?U \<times> set ?U))"
```
```  2388   proof -
```
```  2389     from simp_num_pair_ci[where bs="x#bs"] have "\<forall>x. (?f \<circ> simp_num_pair) x = ?f x"
```
```  2390       by auto
```
```  2391     then have th: "?f \<circ> simp_num_pair = ?f"
```
```  2392       by auto
```
```  2393     have "(?f ` set ?Y) = ((?f \<circ> simp_num_pair) ` set ?S)"
```
```  2394       by (simp add: comp_assoc image_comp)
```
```  2395     also have "\<dots> = ?f ` set ?S"
```
```  2396       by (simp add: th)
```
```  2397     also have "\<dots> = (?f \<circ> ?g) ` set ?Up"
```
```  2398       by (simp only: set_map o_def image_comp)
```
```  2399     also have "\<dots> = ?h ` (set ?U \<times> set ?U)"
```
```  2400       using uset_cong_aux[OF U_l, where x="x" and bs="bs", simplified set_map image_comp]
```
```  2401       by blast
```
```  2402     finally show ?thesis .
```
```  2403   qed
```
```  2404   have "\<forall>(t,n) \<in> set ?Y. bound0 (simpfm (usubst ?q (t, n)))"
```
```  2405   proof -
```
```  2406     have "bound0 (simpfm (usubst ?q (t, n)))" if tnY: "(t,n) \<in> set ?Y" for t n
```
```  2407     proof -
```
```  2408       from Y_l that have tnb: "numbound0 t" and np: "real_of_int n > 0"
```
```  2409         by auto
```
```  2410       from usubst_I[OF lq np tnb] have "bound0 (usubst ?q (t, n))"
```
```  2411         by simp
```
```  2412       then show ?thesis
```
```  2413         using simpfm_bound0 by simp
```
```  2414     qed
```
```  2415     then show ?thesis by blast
```
```  2416   qed
```
```  2417   then have ep_nb: "bound0 ?ep"
```
```  2418     using evaldjf_bound0[where xs="?Y" and f="simpfm \<circ> (usubst ?q)"] by auto
```
```  2419   let ?mp = "minusinf ?q"
```
```  2420   let ?pp = "plusinf ?q"
```
```  2421   let ?M = "?I x ?mp"
```
```  2422   let ?P = "?I x ?pp"
```
```  2423   let ?res = "disj ?mp (disj ?pp ?ep)"
```
```  2424   from rminusinf_bound0[OF lq] rplusinf_bound0[OF lq] ep_nb have nbth: "bound0 ?res"
```
```  2425     by auto
```
```  2426
```
```  2427   from conjunct1[OF rlfm_I[OF simpfm_qf[OF qf]]] simpfm have th: "?lhs = (\<exists>x. ?I x ?q)"
```
```  2428     by auto
```
```  2429   from th fr_equsubst[OF lq, where bs="bs" and x="x"] have lhfr: "?lhs = (?M \<or> ?P \<or> ?F ?q)"
```
```  2430     by (simp only: split_def fst_conv snd_conv)
```
```  2431   also have "\<dots> = (?M \<or> ?P \<or> (\<exists>(t,n) \<in> set ?Y. ?I x (simpfm (usubst ?q (t,n)))))"
```
```  2432     using uset_cong[OF lq YU U_l Y_l] by (simp only: split_def fst_conv snd_conv simpfm)
```
```  2433   also have "\<dots> = (Ifm (x#bs) ?res)"
```
```  2434     using evaldjf_ex[where ps="?Y" and bs = "x#bs" and f="simpfm \<circ> (usubst ?q)",symmetric]
```
```  2435     by (simp add: split_def prod.collapse)
```
```  2436   finally have lheq: "?lhs = Ifm bs (decr ?res)"
```
```  2437     using decr[OF nbth] by blast
```
```  2438   then have lr: "?lhs = ?rhs"
```
```  2439     unfolding ferrack_def Let_def
```
```  2440     by (cases "?mp = T \<or> ?pp = T", auto) (simp add: disj_def)+
```
```  2441   from decr_qf[OF nbth] have "qfree (ferrack p)"
```
```  2442     by (auto simp add: Let_def ferrack_def)
```
```  2443   with lr show ?thesis
```
```  2444     by blast
```
```  2445 qed
```
```  2446
```
```  2447 definition linrqe:: "fm \<Rightarrow> fm"
```
```  2448   where "linrqe p = qelim (prep p) ferrack"
```
```  2449
```
```  2450 theorem linrqe: "Ifm bs (linrqe p) = Ifm bs p \<and> qfree (linrqe p)"
```
```  2451   using ferrack qelim_ci prep
```
```  2452   unfolding linrqe_def by auto
```
```  2453
```
```  2454 definition ferrack_test :: "unit \<Rightarrow> fm"
```
```  2455 where
```
```  2456   "ferrack_test u =
```
```  2457     linrqe (A (A (Imp (Lt (Sub (Bound 1) (Bound 0)))
```
```  2458       (E (Eq (Sub (Add (Bound 0) (Bound 2)) (Bound 1)))))))"
```
```  2459
```
```  2460 ML_val \<open>@{code ferrack_test} ()\<close>
```
```  2461
```
```  2462 oracle linr_oracle = \<open>
```
```  2463 let
```
```  2464
```
```  2465 val mk_C = @{code C} o @{code int_of_integer};
```
```  2466 val mk_Bound = @{code Bound} o @{code nat_of_integer};
```
```  2467
```
```  2468 fun num_of_term vs (Free vT) = mk_Bound (find_index (fn vT' => vT = vT') vs)
```
```  2469   | num_of_term vs @{term "real_of_int (0::int)"} = mk_C 0
```
```  2470   | num_of_term vs @{term "real_of_int (1::int)"} = mk_C 1
```
```  2471   | num_of_term vs @{term "0::real"} = mk_C 0
```
```  2472   | num_of_term vs @{term "1::real"} = mk_C 1
```
```  2473   | num_of_term vs (Bound i) = mk_Bound i
```
```  2474   | num_of_term vs (@{term "uminus :: real \<Rightarrow> real"} \$ t') = @{code Neg} (num_of_term vs t')
```
```  2475   | num_of_term vs (@{term "(+) :: real \<Rightarrow> real \<Rightarrow> real"} \$ t1 \$ t2) =
```
```  2476      @{code Add} (num_of_term vs t1, num_of_term vs t2)
```
```  2477   | num_of_term vs (@{term "(-) :: real \<Rightarrow> real \<Rightarrow> real"} \$ t1 \$ t2) =
```
```  2478      @{code Sub} (num_of_term vs t1, num_of_term vs t2)
```
```  2479   | num_of_term vs (@{term "(*) :: real \<Rightarrow> real \<Rightarrow> real"} \$ t1 \$ t2) = (case num_of_term vs t1
```
```  2480      of @{code C} i => @{code Mul} (i, num_of_term vs t2)
```
```  2481       | _ => error "num_of_term: unsupported multiplication")
```
```  2482   | num_of_term vs (@{term "real_of_int :: int \<Rightarrow> real"} \$ t') =
```
```  2483      (mk_C (snd (HOLogic.dest_number t'))
```
```  2484        handle TERM _ => error ("num_of_term: unknown term"))
```
```  2485   | num_of_term vs t' =
```
```  2486      (mk_C (snd (HOLogic.dest_number t'))
```
```  2487        handle TERM _ => error ("num_of_term: unknown term"));
```
```  2488
```
```  2489 fun fm_of_term vs @{term True} = @{code T}
```
```  2490   | fm_of_term vs @{term False} = @{code F}
```
```  2491   | fm_of_term vs (@{term "(<) :: real \<Rightarrow> real \<Rightarrow> bool"} \$ t1 \$ t2) =
```
```  2492       @{code Lt} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
```
```  2493   | fm_of_term vs (@{term "(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool"} \$ t1 \$ t2) =
```
```  2494       @{code Le} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
```
```  2495   | fm_of_term vs (@{term "(=) :: real \<Rightarrow> real \<Rightarrow> bool"} \$ t1 \$ t2) =
```
```  2496       @{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
```
```  2497   | fm_of_term vs (@{term "(\<longleftrightarrow>) :: bool \<Rightarrow> bool \<Rightarrow> bool"} \$ t1 \$ t2) =
```
```  2498       @{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
```
```  2499   | fm_of_term vs (@{term HOL.conj} \$ t1 \$ t2) = @{code And} (fm_of_term vs t1, fm_of_term vs t2)
```
```  2500   | fm_of_term vs (@{term HOL.disj} \$ t1 \$ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
```
```  2501   | fm_of_term vs (@{term HOL.implies} \$ t1 \$ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
```
```  2502   | fm_of_term vs (@{term "Not"} \$ t') = @{code NOT} (fm_of_term vs t')
```
```  2503   | fm_of_term vs (Const (@{const_name Ex}, _) \$ Abs (xn, xT, p)) =
```
```  2504       @{code E} (fm_of_term (("", dummyT) :: vs) p)
```
```  2505   | fm_of_term vs (Const (@{const_name All}, _) \$ Abs (xn, xT, p)) =
```
```  2506       @{code A} (fm_of_term (("", dummyT) ::  vs) p)
```
```  2507   | fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t);
```
```  2508
```
```  2509 fun term_of_num vs (@{code C} i) = @{term "real_of_int :: int \<Rightarrow> real"} \$
```
```  2510       HOLogic.mk_number HOLogic.intT (@{code integer_of_int} i)
```
```  2511   | term_of_num vs (@{code Bound} n) = Free (nth vs (@{code integer_of_nat} n))
```
```  2512   | term_of_num vs (@{code Neg} t') = @{term "uminus :: real \<Rightarrow> real"} \$ term_of_num vs t'
```
```  2513   | term_of_num vs (@{code Add} (t1, t2)) = @{term "(+) :: real \<Rightarrow> real \<Rightarrow> real"} \$
```
```  2514       term_of_num vs t1 \$ term_of_num vs t2
```
```  2515   | term_of_num vs (@{code Sub} (t1, t2)) = @{term "(-) :: real \<Rightarrow> real \<Rightarrow> real"} \$
```
```  2516       term_of_num vs t1 \$ term_of_num vs t2
```
```  2517   | term_of_num vs (@{code Mul} (i, t2)) = @{term "(*) :: real \<Rightarrow> real \<Rightarrow> real"} \$
```
```  2518       term_of_num vs (@{code C} i) \$ term_of_num vs t2
```
```  2519   | term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t));
```
```  2520
```
```  2521 fun term_of_fm vs @{code T} = @{term True}
```
```  2522   | term_of_fm vs @{code F} = @{term False}
```
```  2523   | term_of_fm vs (@{code Lt} t) = @{term "(<) :: real \<Rightarrow> real \<Rightarrow> bool"} \$
```
```  2524       term_of_num vs t \$ @{term "0::real"}
```
```  2525   | term_of_fm vs (@{code Le} t) = @{term "(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool"} \$
```
```  2526       term_of_num vs t \$ @{term "0::real"}
```
```  2527   | term_of_fm vs (@{code Gt} t) = @{term "(<) :: real \<Rightarrow> real \<Rightarrow> bool"} \$
```
```  2528       @{term "0::real"} \$ term_of_num vs t
```
```  2529   | term_of_fm vs (@{code Ge} t) = @{term "(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool"} \$
```
```  2530       @{term "0::real"} \$ term_of_num vs t
```
```  2531   | term_of_fm vs (@{code Eq} t) = @{term "(=) :: real \<Rightarrow> real \<Rightarrow> bool"} \$
```
```  2532       term_of_num vs t \$ @{term "0::real"}
```
```  2533   | term_of_fm vs (@{code NEq} t) = term_of_fm vs (@{code NOT} (@{code Eq} t))
```
```  2534   | term_of_fm vs (@{code NOT} t') = HOLogic.Not \$ term_of_fm vs t'
```
```  2535   | term_of_fm vs (@{code And} (t1, t2)) = HOLogic.conj \$ term_of_fm vs t1 \$ term_of_fm vs t2
```
```  2536   | term_of_fm vs (@{code Or} (t1, t2)) = HOLogic.disj \$ term_of_fm vs t1 \$ term_of_fm vs t2
```
```  2537   | term_of_fm vs (@{code Imp}  (t1, t2)) = HOLogic.imp \$ term_of_fm vs t1 \$ term_of_fm vs t2
```
```  2538   | term_of_fm vs (@{code Iff} (t1, t2)) = @{term "(\<longleftrightarrow>) :: bool \<Rightarrow> bool \<Rightarrow> bool"} \$
```
```  2539       term_of_fm vs t1 \$ term_of_fm vs t2;
```
```  2540
```
```  2541 in fn (ctxt, t) =>
```
```  2542   let
```
```  2543     val vs = Term.add_frees t [];
```
```  2544     val t' = (term_of_fm vs o @{code linrqe} o fm_of_term vs) t;
```
```  2545   in (Thm.cterm_of ctxt o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
```
```  2546 end
```
```  2547 \<close>
```
```  2548
```
```  2549 ML_file "ferrack_tac.ML"
```
```  2550
```
```  2551 method_setup rferrack = \<open>
```
```  2552   Scan.lift (Args.mode "no_quantify") >>
```
```  2553     (fn q => fn ctxt => SIMPLE_METHOD' (Ferrack_Tac.linr_tac ctxt (not q)))
```
```  2554 \<close> "decision procedure for linear real arithmetic"
```
```  2555
```
```  2556
```
```  2557 lemma
```
```  2558   fixes x :: real
```
```  2559   shows "2 * x \<le> 2 * x \<and> 2 * x \<le> 2 * x + 1"
```
```  2560   by rferrack
```
```  2561
```
```  2562 lemma
```
```  2563   fixes x :: real
```
```  2564   shows "\<exists>y \<le> x. x = y + 1"
```
```  2565   by rferrack
```
```  2566
```
```  2567 lemma
```
```  2568   fixes x :: real
```
```  2569   shows "\<not> (\<exists>z. x + z = x + z + 1)"
```
```  2570   by rferrack
```
```  2571
```
```  2572 end
```