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