Quelle Ferrack.thy Sprache: Isabelle

(*  Title:      HOL/Decision_Procs/Ferrack.thy
    Author:     Amine Chaieb
*)

theory Ferrack
imports Complex_Main Dense_Linear_Order DP_Library
  "HOL-Library.Code_Target_Numeral"
begin

section \<open>Quantifier elimination for \<open>\<real> (0, 1, +, <)\<close>\<close>

  (*********************************************************************************)
  (****                            SHADOW SYNTAX AND SEMANTICS                  ****)
  (*********************************************************************************)

datatype (plugins del: size) num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num
  | Mul int num

instantiation num :: size
begin

primrec size_num :: "num \ nat"
where
  "size_num (C c) = 1"
| "size_num (Bound n) = 1"
| "size_num (Neg a) = 1 + size_num a"
| "size_num (Add a b) = 1 + size_num a + size_num b"
| "size_num (Sub a b) = 3 + size_num a + size_num b"
| "size_num (Mul c a) = 1 + size_num a"
| "size_num (CN n c a) = 3 + size_num a "

instance ..

end

  (* Semantics of numeral terms (num) *)
primrec Inum :: "real list \ num \ real"
where
  "Inum bs (C c) = (real_of_int c)"
| "Inum bs (Bound n) = bs!n"
| "Inum bs (CN n c a) = (real_of_int c) * (bs!n) + (Inum bs a)"
| "Inum bs (Neg a) = -(Inum bs a)"
| "Inum bs (Add a b) = Inum bs a + Inum bs b"
| "Inum bs (Sub a b) = Inum bs a - Inum bs b"
| "Inum bs (Mul c a) = (real_of_int c) * Inum bs a"
    (* FORMULAE *)
datatype (plugins del: size) fm  =
  T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num|
  Not fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm

instantiation fm :: size
begin

primrec size_fm :: "fm \ nat"
where
  "size_fm (Not p) = 1 + size_fm p"
| "size_fm (And p q) = 1 + size_fm p + size_fm q"
| "size_fm (Or p q) = 1 + size_fm p + size_fm q"
| "size_fm (Imp p q) = 3 + size_fm p + size_fm q"
| "size_fm (Iff p q) = 3 + 2 * (size_fm p + size_fm q)"
| "size_fm (E p) = 1 + size_fm p"
| "size_fm (A p) = 4 + size_fm p"
| "size_fm T = 1"
| "size_fm F = 1"
| "size_fm (Lt _) = 1"
| "size_fm (Le _) = 1"
| "size_fm (Gt _) = 1"
| "size_fm (Ge _) = 1"
| "size_fm (Eq _) = 1"
| "size_fm (NEq _) = 1"

instance ..

end

lemma size_fm_pos [simp]: "size p > 0" for p :: fm
  by (induct p) simp_all

  (* Semantics of formulae (fm) *)
primrec Ifm ::"real list \ fm \ bool"
where
  "Ifm bs T = True"
| "Ifm bs F = False"
| "Ifm bs (Lt a) = (Inum bs a < 0)"
| "Ifm bs (Gt a) = (Inum bs a > 0)"
| "Ifm bs (Le a) = (Inum bs a \ 0)"
| "Ifm bs (Ge a) = (Inum bs a \ 0)"
| "Ifm bs (Eq a) = (Inum bs a = 0)"
| "Ifm bs (NEq a) = (Inum bs a \ 0)"
| "Ifm bs (Not p) = (\ (Ifm bs p))"
| "Ifm bs (And p q) = (Ifm bs p \ Ifm bs q)"
| "Ifm bs (Or p q) = (Ifm bs p \ Ifm bs q)"
| "Ifm bs (Imp p q) = ((Ifm bs p) \ (Ifm bs q))"
| "Ifm bs (Iff p q) = (Ifm bs p = Ifm bs q)"
| "Ifm bs (E p) = (\x. Ifm (x#bs) p)"
| "Ifm bs (A p) = (\x. Ifm (x#bs) p)"

lemma IfmLeSub: "\ Inum bs s = s' ; Inum bs t = t' \ \ Ifm bs (Le (Sub s t)) = (s' \ t')"
  by simp

lemma IfmLtSub: "\ Inum bs s = s' ; Inum bs t = t' \ \ Ifm bs (Lt (Sub s t)) = (s' < t')"
  by simp

lemma IfmEqSub: "\ Inum bs s = s' ; Inum bs t = t' \ \ Ifm bs (Eq (Sub s t)) = (s' = t')"
  by simp

lemma IfmNot: " (Ifm bs p = P) \ (Ifm bs (Not p) = (\P))"
  by simp

lemma IfmAnd: " \ Ifm bs p = P ; Ifm bs q = Q\ \ (Ifm bs (And p q) = (P \ Q))"
  by simp

lemma IfmOr: " \ Ifm bs p = P ; Ifm bs q = Q\ \ (Ifm bs (Or p q) = (P \ Q))"
  by simp

lemma IfmImp: " \ Ifm bs p = P ; Ifm bs q = Q\ \ (Ifm bs (Imp p q) = (P \ Q))"
  by simp

lemma IfmIff: " \ Ifm bs p = P ; Ifm bs q = Q\ \ (Ifm bs (Iff p q) = (P = Q))"
  by simp

lemma IfmE: " (!! x. Ifm (x#bs) p = P x) \ (Ifm bs (E p) = (\x. P x))"
  by simp

lemma IfmA: " (!! x. Ifm (x#bs) p = P x) \ (Ifm bs (A p) = (\x. P x))"
  by simp

fun not:: "fm \ fm"
where
  "not (Not p) = p"
| "not T = F"
| "not F = T"
| "not p = Not p"

lemma not[simp]: "Ifm bs (not p) = Ifm bs (Not p)"
  by (cases p) auto

definition conj :: "fm \ fm \ fm"
where
  "conj p q =
   (if p = F \<or> q = F then F
    else if p = T then q
    else if q = T then p
    else if p = q then p else And p q)"

lemma conj[simp]: "Ifm bs (conj p q) = Ifm bs (And p q)"
  by (cases "p = F \ q = F", simp_all add: conj_def) (cases p, simp_all)

definition disj :: "fm \ fm \ fm"
where
  "disj p q =
   (if p = T \<or> q = T then T
    else if p = F then q
    else if q = F then p
    else if p = q then p else Or p q)"

lemma disj[simp]: "Ifm bs (disj p q) = Ifm bs (Or p q)"
  by (cases "p = T \ q = T", simp_all add: disj_def) (cases p, simp_all)

definition imp :: "fm \ fm \ fm"
where
  "imp p q =
   (if p = F \<or> q = T \<or> p = q then T
    else if p = T then q
    else if q = F then not p
    else Imp p q)"

lemma imp[simp]: "Ifm bs (imp p q) = Ifm bs (Imp p q)"
  by (cases "p = F \ q = T") (simp_all add: imp_def)

definition iff :: "fm \ fm \ fm"
where
  "iff p q =
   (if p = q then T
    else if p = Not q \<or> Not p = q then F
    else if p = F then not q
    else if q = F then not p
    else if p = T then q
    else if q = T then p
    else Iff p q)"

lemma iff[simp]: "Ifm bs (iff p q) = Ifm bs (Iff p q)"
  by (unfold iff_def, cases "p = q", simp, cases "p = Not q", simp) (cases "Not p = q", auto)

lemma conj_simps:
  "conj F Q = F"
  "conj P F = F"
  "conj T Q = Q"
  "conj P T = P"
  "conj P P = P"
  "P \ T \ P \ F \ Q \ T \ Q \ F \ P \ Q \ conj P Q = And P Q"
  by (simp_all add: conj_def)

lemma disj_simps:
  "disj T Q = T"
  "disj P T = T"
  "disj F Q = Q"
  "disj P F = P"
  "disj P P = P"
  "P \ T \ P \ F \ Q \ T \ Q \ F \ P \ Q \ disj P Q = Or P Q"
  by (simp_all add: disj_def)

lemma imp_simps:
  "imp F Q = T"
  "imp P T = T"
  "imp T Q = Q"
  "imp P F = not P"
  "imp P P = T"
  "P \ T \ P \ F \ P \ Q \ Q \ T \ Q \ F \ imp P Q = Imp P Q"
  by (simp_all add: imp_def)

lemma trivNot: "p \ Not p" "Not p \ p"
  by (induct p) auto

lemma iff_simps:
  "iff p p = T"
  "iff p (Not p) = F"
  "iff (Not p) p = F"
  "iff p F = not p"
  "iff F p = not p"
  "p \ Not T \ iff T p = p"
  "p\ Not T \ iff p T = p"
  "p\q \ p\ Not q \ q\ Not p \ p\ F \ q\ F \ p \ T \ q \ T \ iff p q = Iff p q"
  using trivNot
  by (simp_all add: iff_def, cases p, auto)

  (* Quantifier freeness *)
fun qfree:: "fm \ bool"
where
  "qfree (E p) = False"
| "qfree (A p) = False"
| "qfree (Not p) = qfree p"
| "qfree (And p q) = (qfree p \ qfree q)"
| "qfree (Or p q) = (qfree p \ qfree q)"
| "qfree (Imp p q) = (qfree p \ qfree q)"
| "qfree (Iff p q) = (qfree p \ qfree q)"
| "qfree p = True"

  (* Boundedness and substitution *)
primrec numbound0:: "num \ bool" (* a num is INDEPENDENT of Bound 0 *)
where
  "numbound0 (C c) = True"
| "numbound0 (Bound n) = (n > 0)"
| "numbound0 (CN n c a) = (n \ 0 \ numbound0 a)"
| "numbound0 (Neg a) = numbound0 a"
| "numbound0 (Add a b) = (numbound0 a \ numbound0 b)"
| "numbound0 (Sub a b) = (numbound0 a \ numbound0 b)"
| "numbound0 (Mul i a) = numbound0 a"

lemma numbound0_I:
  assumes nb: "numbound0 a"
  shows "Inum (b#bs) a = Inum (b'#bs) a"
  using nb by (induct a) simp_all

primrec bound0:: "fm \ bool" (* A Formula is independent of Bound 0 *)
where
  "bound0 T = True"
| "bound0 F = True"
| "bound0 (Lt a) = numbound0 a"
| "bound0 (Le a) = numbound0 a"
| "bound0 (Gt a) = numbound0 a"
| "bound0 (Ge a) = numbound0 a"
| "bound0 (Eq a) = numbound0 a"
| "bound0 (NEq a) = numbound0 a"
| "bound0 (Not p) = bound0 p"
| "bound0 (And p q) = (bound0 p \ bound0 q)"
| "bound0 (Or p q) = (bound0 p \ bound0 q)"
| "bound0 (Imp p q) = ((bound0 p) \ (bound0 q))"
| "bound0 (Iff p q) = (bound0 p \ bound0 q)"
| "bound0 (E p) = False"
| "bound0 (A p) = False"

lemma bound0_I:
  assumes bp: "bound0 p"
  shows "Ifm (b#bs) p = Ifm (b'#bs) p"
  using bp numbound0_I[where b="b" and bs="bs" and b'="b'"]
  by (induct p) auto

lemma not_qf[simp]: "qfree p \ qfree (not p)"
  by (cases p) auto

lemma not_bn[simp]: "bound0 p \ bound0 (not p)"
  by (cases p) auto

lemma conj_qf[simp]: "\qfree p ; qfree q\ \ qfree (conj p q)"
  using conj_def by auto
lemma conj_nb[simp]: "\bound0 p ; bound0 q\ \ bound0 (conj p q)"
  using conj_def by auto

lemma disj_qf[simp]: "\qfree p ; qfree q\ \ qfree (disj p q)"
  using disj_def by auto
lemma disj_nb[simp]: "\bound0 p ; bound0 q\ \ bound0 (disj p q)"
  using disj_def by auto

lemma imp_qf[simp]: "\qfree p ; qfree q\ \ qfree (imp p q)"
  using imp_def by (cases "p=F \ q=T",simp_all add: imp_def)
lemma imp_nb[simp]: "\bound0 p ; bound0 q\ \ bound0 (imp p q)"
  using imp_def by (cases "p=F \ q=T \ p=q",simp_all add: imp_def)

lemma iff_qf[simp]: "\qfree p ; qfree q\ \ qfree (iff p q)"
  unfolding iff_def by (cases "p = q") auto
lemma iff_nb[simp]: "\bound0 p ; bound0 q\ \ bound0 (iff p q)"
  using iff_def unfolding iff_def by (cases "p = q") auto

fun decrnum:: "num \ num"
where
  "decrnum (Bound n) = Bound (n - 1)"
| "decrnum (Neg a) = Neg (decrnum a)"
| "decrnum (Add a b) = Add (decrnum a) (decrnum b)"
| "decrnum (Sub a b) = Sub (decrnum a) (decrnum b)"
| "decrnum (Mul c a) = Mul c (decrnum a)"
| "decrnum (CN n c a) = CN (n - 1) c (decrnum a)"
| "decrnum a = a"

fun decr :: "fm \ fm"
where
  "decr (Lt a) = Lt (decrnum a)"
| "decr (Le a) = Le (decrnum a)"
| "decr (Gt a) = Gt (decrnum a)"
| "decr (Ge a) = Ge (decrnum a)"
| "decr (Eq a) = Eq (decrnum a)"
| "decr (NEq a) = NEq (decrnum a)"
| "decr (Not p) = Not (decr p)"
| "decr (And p q) = conj (decr p) (decr q)"
| "decr (Or p q) = disj (decr p) (decr q)"
| "decr (Imp p q) = imp (decr p) (decr q)"
| "decr (Iff p q) = iff (decr p) (decr q)"
| "decr p = p"

lemma decrnum:
  assumes nb: "numbound0 t"
  shows "Inum (x # bs) t = Inum bs (decrnum t)"
  using nb by (induct t rule: decrnum.induct) simp_all

lemma decr:
  assumes nb: "bound0 p"
  shows "Ifm (x # bs) p = Ifm bs (decr p)"
  using nb by (induct p rule: decr.induct) (simp_all add: decrnum)

lemma decr_qf: "bound0 p \ qfree (decr p)"
  by (induct p) simp_all

fun isatom :: "fm \ bool" (* test for atomicity *)
where
  "isatom T = True"
| "isatom F = True"
| "isatom (Lt a) = True"
| "isatom (Le a) = True"
| "isatom (Gt a) = True"
| "isatom (Ge a) = True"
| "isatom (Eq a) = True"
| "isatom (NEq a) = True"
| "isatom p = False"

lemma bound0_qf: "bound0 p \ qfree p"
  by (induct p) simp_all

definition djf :: "('a \ fm) \ 'a \ fm \ fm"
where
  "djf f p q =
   (if q = T then T
    else if q = F then f p
    else (let fp = f p in case fp of T \<Rightarrow> T | F \<Rightarrow> q | _ \<Rightarrow> Or (f p) q))"

definition evaldjf :: "('a \ fm) \ 'a list \ fm"
  where "evaldjf f ps = foldr (djf f) ps F"

lemma djf_Or: "Ifm bs (djf f p q) = Ifm bs (Or (f p) q)"
  by (cases "q = T", simp add: djf_def, cases "q = F", simp add: djf_def)
    (cases "f p", simp_all add: Let_def djf_def)

lemma djf_simps:
  "djf f p T = T"
  "djf f p F = f p"
  "q \ T \ q \ F \ djf f p q = (let fp = f p in case fp of T \ T | F \ q | _ \ Or (f p) q)"
  by (simp_all add: djf_def)

lemma evaldjf_ex: "Ifm bs (evaldjf f ps) \ (\p \ set ps. Ifm bs (f p))"
  by (induct ps) (simp_all add: evaldjf_def djf_Or)

lemma evaldjf_bound0:
  assumes nb: "\x\ set xs. bound0 (f x)"
  shows "bound0 (evaldjf f xs)"
  using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto)

lemma evaldjf_qf:
  assumes nb: "\x\ set xs. qfree (f x)"
  shows "qfree (evaldjf f xs)"
  using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto)

fun disjuncts :: "fm \ fm list"
where
  "disjuncts (Or p q) = disjuncts p @ disjuncts q"
| "disjuncts F = []"
| "disjuncts p = [p]"

lemma disjuncts: "(\q\ set (disjuncts p). Ifm bs q) = Ifm bs p"
  by (induct p rule: disjuncts.induct) auto

lemma disjuncts_nb: "bound0 p \ \q\ set (disjuncts p). bound0 q"
proof -
  assume nb: "bound0 p"
  then have "list_all bound0 (disjuncts p)"
    by (induct p rule: disjuncts.induct) auto
  then show ?thesis
    by (simp only: list_all_iff)
qed

lemma disjuncts_qf: "qfree p \ \q\ set (disjuncts p). qfree q"
proof -
  assume qf: "qfree p"
  then have "list_all qfree (disjuncts p)"
    by (induct p rule: disjuncts.induct) auto
  then show ?thesis
    by (simp only: list_all_iff)
qed

definition DJ :: "(fm \ fm) \ fm \ fm"
  where "DJ f p = evaldjf f (disjuncts p)"

lemma DJ:
  assumes fdj: "\p q. Ifm bs (f (Or p q)) = Ifm bs (Or (f p) (f q))"
    and fF: "f F = F"
  shows "Ifm bs (DJ f p) = Ifm bs (f p)"
proof -
  have "Ifm bs (DJ f p) = (\q \ set (disjuncts p). Ifm bs (f q))"
    by (simp add: DJ_def evaldjf_ex)
  also have "\ = Ifm bs (f p)"
    using fdj fF by (induct p rule: disjuncts.induct) auto
  finally show ?thesis .
qed

lemma DJ_qf:
  assumes fqf: "\p. qfree p \ qfree (f p)"
  shows "\p. qfree p \ qfree (DJ f p) "
proof clarify
  fix p
  assume qf: "qfree p"
  have th: "DJ f p = evaldjf f (disjuncts p)"
    by (simp add: DJ_def)
  from disjuncts_qf[OF qf] have "\q\ set (disjuncts p). qfree q" .
  with fqf have th':"\q\ set (disjuncts p). qfree (f q)"
    by blast
  from evaldjf_qf[OF th'] th show "qfree (DJ f p)"
    by simp
qed

lemma DJ_qe:
  assumes qe: "\bs p. qfree p \ qfree (qe p) \ (Ifm bs (qe p) = Ifm bs (E p))"
  shows "\bs p. qfree p \ qfree (DJ qe p) \ (Ifm bs ((DJ qe p)) = Ifm bs (E p))"
proof clarify
  fix p :: fm
  fix bs
  assume qf: "qfree p"
  from qe have qth: "\p. qfree p \ qfree (qe p)"
    by blast
  from DJ_qf[OF qth] qf have qfth: "qfree (DJ qe p)"
    by auto
  have "Ifm bs (DJ qe p) \ (\q\ set (disjuncts p). Ifm bs (qe q))"
    by (simp add: DJ_def evaldjf_ex)
  also have "\ \ (\q \ set(disjuncts p). Ifm bs (E q))"
    using qe disjuncts_qf[OF qf] by auto
  also have "\ = Ifm bs (E p)"
    by (induct p rule: disjuncts.induct) auto
  finally show "qfree (DJ qe p) \ Ifm bs (DJ qe p) = Ifm bs (E p)"
    using qfth by blast
qed

  (* Simplification *)

fun maxcoeff:: "num \ int"
where
  "maxcoeff (C i) = \i\"
| "maxcoeff (CN n c t) = max \c\ (maxcoeff t)"
| "maxcoeff t = 1"

lemma maxcoeff_pos: "maxcoeff t \ 0"
  by (induct t rule: maxcoeff.induct, auto)

fun numgcdh:: "num \ int \ int"
where
  "numgcdh (C i) = (\g. gcd i g)"
| "numgcdh (CN n c t) = (\g. gcd c (numgcdh t g))"
| "numgcdh t = (\g. 1)"

definition numgcd :: "num \ int"
  where "numgcd t = numgcdh t (maxcoeff t)"

fun reducecoeffh:: "num \ int \ num"
where
  "reducecoeffh (C i) = (\g. C (i div g))"
| "reducecoeffh (CN n c t) = (\g. CN n (c div g) (reducecoeffh t g))"
| "reducecoeffh t = (\g. t)"

definition reducecoeff :: "num \ num"
where
  "reducecoeff t =
   (let g = numgcd t
    in if g = 0 then C 0 else if g = 1 then t else reducecoeffh t g)"

fun dvdnumcoeff:: "num \ int \ bool"
where
  "dvdnumcoeff (C i) = (\g. g dvd i)"
| "dvdnumcoeff (CN n c t) = (\g. g dvd c \ dvdnumcoeff t g)"
| "dvdnumcoeff t = (\g. False)"

lemma dvdnumcoeff_trans:
  assumes gdg: "g dvd g'"
    and dgt':"dvdnumcoeff t g'"
  shows "dvdnumcoeff t g"
  using dgt' gdg
  by (induct t rule: dvdnumcoeff.induct) (simp_all add: gdg dvd_trans[OF gdg])

declare dvd_trans [trans add]

lemma natabs0: "nat \x\ = 0 \ x = 0"
  by arith

lemma numgcd0:
  assumes g0: "numgcd t = 0"
  shows "Inum bs t = 0"
  using g0[simplified numgcd_def]
  by (induct t rule: numgcdh.induct) (auto simp add: natabs0 maxcoeff_pos max.absorb2)

lemma numgcdh_pos:
  assumes gp: "g \ 0"
  shows "numgcdh t g \ 0"
  using gp by (induct t rule: numgcdh.induct) auto

lemma numgcd_pos: "numgcd t \0"
  by (simp add: numgcd_def numgcdh_pos maxcoeff_pos)

lemma reducecoeffh:
  assumes gt: "dvdnumcoeff t g"
    and gp: "g > 0"
  shows "real_of_int g *(Inum bs (reducecoeffh t g)) = Inum bs t"
  using gt
proof (induct t rule: reducecoeffh.induct)
  case (1 i)
  then have gd: "g dvd i"
    by simp
  with assms show ?case
    by (simp add: real_of_int_div[OF gd])
next
  case (2 n c t)
  then have gd: "g dvd c"
    by simp
  from assms 2 show ?case
    by (simp add: real_of_int_div[OF gd] algebra_simps)
qed (auto simp add: numgcd_def gp)

fun ismaxcoeff:: "num \ int \ bool"
where
  "ismaxcoeff (C i) = (\x. \i\ \ x)"
| "ismaxcoeff (CN n c t) = (\x. \c\ \ x \ ismaxcoeff t x)"
| "ismaxcoeff t = (\x. True)"

lemma ismaxcoeff_mono: "ismaxcoeff t c \ c \ c' \ ismaxcoeff t c'"
  by (induct t rule: ismaxcoeff.induct) auto

lemma maxcoeff_ismaxcoeff: "ismaxcoeff t (maxcoeff t)"
proof (induct t rule: maxcoeff.induct)
  case (2 n c t)
  then have H:"ismaxcoeff t (maxcoeff t)" .
  have thh: "maxcoeff t \ max \c\ (maxcoeff t)"
    by simp
  from ismaxcoeff_mono[OF H thh] show ?case
    by simp
qed simp_all

lemma zgcd_gt1:
  "\i\ > 1 \ \j\ > 1 \ \i\ = 0 \ \j\ > 1 \ \i\ > 1 \ \j\ = 0"
  if "gcd i j > 1" for i j :: int
proof -
  have "\k\ \ 1 \ k = - 1 \ k = 0 \ k = 1" for k :: int
    by auto
  with that show ?thesis
    by (auto simp add: not_less)
qed

lemma numgcdh0:"numgcdh t m = 0 \ m =0"
  by (induct t rule: numgcdh.induct) auto

lemma dvdnumcoeff_aux:
  assumes "ismaxcoeff t m"
    and mp: "m \ 0"
    and "numgcdh t m > 1"
  shows "dvdnumcoeff t (numgcdh t m)"
  using assms
proof (induct t rule: numgcdh.induct)
  case (2 n c t)
  let ?g = "numgcdh t m"
  from 2 have th: "gcd c ?g > 1"
    by simp
  from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
  consider "\c\ > 1" "?g > 1" | "\c\ = 0" "?g > 1" | "?g = 0"
    by auto
  then show ?case
  proof cases
    case 1
    with 2 have th: "dvdnumcoeff t ?g"
      by simp
    have th': "gcd c ?g dvd ?g"
      by simp
    from dvdnumcoeff_trans[OF th' th] show ?thesis
      by simp
  next
    case "2'": 2
    with 2 have th: "dvdnumcoeff t ?g"
      by simp
    have th': "gcd c ?g dvd ?g"
      by simp
    from dvdnumcoeff_trans[OF th' th] show ?thesis
      by simp
  next
    case 3
    then have "m = 0" by (rule numgcdh0)
    with 2 3 show ?thesis by simp
  qed
qed auto

lemma dvdnumcoeff_aux2:
  assumes "numgcd t > 1"
  shows "dvdnumcoeff t (numgcd t) \ numgcd t > 0"
  using assms
proof (simp add: numgcd_def)
  let ?mc = "maxcoeff t"
  let ?g = "numgcdh t ?mc"
  have th1: "ismaxcoeff t ?mc"
    by (rule maxcoeff_ismaxcoeff)
  have th2: "?mc \ 0"
    by (rule maxcoeff_pos)
  assume H: "numgcdh t ?mc > 1"
  from dvdnumcoeff_aux[OF th1 th2 H] show "dvdnumcoeff t ?g" .
qed

lemma reducecoeff: "real_of_int (numgcd t) * (Inum bs (reducecoeff t)) = Inum bs t"
proof -
  let ?g = "numgcd t"
  have "?g \ 0"
    by (simp add: numgcd_pos)
  then consider "?g = 0" | "?g = 1" | "?g > 1" by atomize_elim auto
  then show ?thesis
  proof cases
    case 1
    then show ?thesis by (simp add: numgcd0)
  next
    case 2
    then show ?thesis by (simp add: reducecoeff_def)
  next
    case g1: 3
    from dvdnumcoeff_aux2[OF g1] have th1: "dvdnumcoeff t ?g" and g0: "?g > 0"
      by blast+
    from reducecoeffh[OF th1 g0, where bs="bs"] g1 show ?thesis
      by (simp add: reducecoeff_def Let_def)
  qed
qed

lemma reducecoeffh_numbound0: "numbound0 t \ numbound0 (reducecoeffh t g)"
  by (induct t rule: reducecoeffh.induct) auto

lemma reducecoeff_numbound0: "numbound0 t \ numbound0 (reducecoeff t)"
  using reducecoeffh_numbound0 by (simp add: reducecoeff_def Let_def)

fun numadd:: "num \ num \ num"
where
  "numadd (CN n1 c1 r1) (CN n2 c2 r2) =
   (if n1 = n2 then
    (let c = c1 + c2
     in (if c = 0 then numadd r1 r2 else CN n1 c (numadd r1 r2)))
    else if n1 \<le> n2 then (CN n1 c1 (numadd r1 (CN n2 c2 r2)))
    else (CN n2 c2 (numadd (CN n1 c1 r1) r2)))"
| "numadd (CN n1 c1 r1) t = CN n1 c1 (numadd r1 t)"
| "numadd t (CN n2 c2 r2) = CN n2 c2 (numadd t r2)"
| "numadd (C b1) (C b2) = C (b1 + b2)"
| "numadd a b = Add a b"

lemma numadd [simp]: "Inum bs (numadd t s) = Inum bs (Add t s)"
  by (induct t s rule: numadd.induct) (simp_all add: Let_def algebra_simps add_eq_0_iff)

lemma numadd_nb [simp]: "numbound0 t \ numbound0 s \ numbound0 (numadd t s)"
  by (induct t s rule: numadd.induct) (simp_all add: Let_def)

fun nummul:: "num \ int \ num"
where
  "nummul (C j) = (\i. C (i * j))"
| "nummul (CN n c a) = (\i. CN n (i * c) (nummul a i))"
| "nummul t = (\i. Mul i t)"

lemma nummul[simp]: "\i. Inum bs (nummul t i) = Inum bs (Mul i t)"
  by (induct t rule: nummul.induct) (auto simp add: algebra_simps)

lemma nummul_nb[simp]: "\i. numbound0 t \ numbound0 (nummul t i)"
  by (induct t rule: nummul.induct) auto

definition numneg :: "num \ num"
  where "numneg t = nummul t (- 1)"

definition numsub :: "num \ num \ num"
  where "numsub s t = (if s = t then C 0 else numadd s (numneg t))"

lemma numneg[simp]: "Inum bs (numneg t) = Inum bs (Neg t)"
  using numneg_def by simp

lemma numneg_nb[simp]: "numbound0 t \ numbound0 (numneg t)"
  using numneg_def by simp

lemma numsub[simp]: "Inum bs (numsub a b) = Inum bs (Sub a b)"
  using numsub_def by simp

lemma numsub_nb[simp]: "\ numbound0 t ; numbound0 s\ \ numbound0 (numsub t s)"
  using numsub_def by simp

primrec simpnum:: "num \ num"
where
  "simpnum (C j) = C j"
| "simpnum (Bound n) = CN n 1 (C 0)"
| "simpnum (Neg t) = numneg (simpnum t)"
| "simpnum (Add t s) = numadd (simpnum t) (simpnum s)"
| "simpnum (Sub t s) = numsub (simpnum t) (simpnum s)"
| "simpnum (Mul i t) = (if i = 0 then C 0 else nummul (simpnum t) i)"
| "simpnum (CN n c t) = (if c = 0 then simpnum t else numadd (CN n c (C 0)) (simpnum t))"

lemma simpnum_ci[simp]: "Inum bs (simpnum t) = Inum bs t"
  by (induct t) simp_all

lemma simpnum_numbound0[simp]: "numbound0 t \ numbound0 (simpnum t)"
  by (induct t) simp_all

fun nozerocoeff:: "num \ bool"
where
  "nozerocoeff (C c) = True"
| "nozerocoeff (CN n c t) = (c \ 0 \ nozerocoeff t)"
| "nozerocoeff t = True"

lemma numadd_nz : "nozerocoeff a \ nozerocoeff b \ nozerocoeff (numadd a b)"
  by (induct a b rule: numadd.induct) (simp_all add: Let_def)

lemma nummul_nz : "\i. i\0 \ nozerocoeff a \ nozerocoeff (nummul a i)"
  by (induct a rule: nummul.induct) (auto simp add: Let_def numadd_nz)

lemma numneg_nz : "nozerocoeff a \ nozerocoeff (numneg a)"
  by (simp add: numneg_def nummul_nz)

lemma numsub_nz: "nozerocoeff a \ nozerocoeff b \ nozerocoeff (numsub a b)"
  by (simp add: numsub_def numneg_nz numadd_nz)

lemma simpnum_nz: "nozerocoeff (simpnum t)"
  by (induct t) (simp_all add: numadd_nz numneg_nz numsub_nz nummul_nz)

lemma maxcoeff_nz: "nozerocoeff t \ maxcoeff t = 0 \ t = C 0"
  by (induction t rule: maxcoeff.induct) auto

lemma numgcd_nz:
  assumes nz: "nozerocoeff t"
    and g0: "numgcd t = 0"
  shows "t = C 0"
proof -
  from g0 have th:"numgcdh t (maxcoeff t) = 0"
    by (simp add: numgcd_def)
  from numgcdh0[OF th] have th:"maxcoeff t = 0" .
  from maxcoeff_nz[OF nz th] show ?thesis .
qed

definition simp_num_pair :: "(num \ int) \ num \ int"
where
  "simp_num_pair =
    (\<lambda>(t,n).
     (if n = 0 then (C 0, 0)
      else
       (let t' = simpnum t ; g = numgcd t' in
         if g > 1 then
          (let g' = gcd n g
           in if g' = 1 then (t', n) else (reducecoeffh t' g', n div g'))
         else (t', n))))"

lemma simp_num_pair_ci:
  shows "((\(t,n). Inum bs t / real_of_int n) (simp_num_pair (t,n))) =
    ((\<lambda>(t,n). Inum bs t / real_of_int n) (t, n))"
  (is "?lhs = ?rhs")
proof -
  let ?t' = "simpnum t"
  let ?g = "numgcd ?t'"
  let ?g' = "gcd n ?g"
  show ?thesis
  proof (cases "n = 0")
    case True
    then show ?thesis
      by (simp add: Let_def simp_num_pair_def)
  next
    case nnz: False
    show ?thesis
    proof (cases "?g > 1")
      case False
      then show ?thesis by (simp add: Let_def simp_num_pair_def)
    next
      case g1: True
      then have g0: "?g > 0"
        by simp
      from g1 nnz have gp0: "?g' \ 0"
        by simp
      then have g'p: "?g' > 0"
        using gcd_ge_0_int[where x="n" and y="numgcd ?t'"] by arith
      then consider "?g' = 1" | "?g' > 1" by arith
      then show ?thesis
      proof cases
        case 1
        then show ?thesis
          by (simp add: Let_def simp_num_pair_def)
      next
        case g'1: 2
        from dvdnumcoeff_aux2[OF g1] have th1: "dvdnumcoeff ?t' ?g" ..
        let ?tt = "reducecoeffh ?t' ?g'"
        let ?t = "Inum bs ?tt"
        have gpdg: "?g' dvd ?g" by simp
        have gpdd: "?g' dvd n" by simp
        have gpdgp: "?g' dvd ?g'" by simp
        from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p]
        have th2:"real_of_int ?g' * ?t = Inum bs ?t'"
          by simp
        from g1 g'1 have "?lhs = ?t / real_of_int (n div ?g')"
          by (simp add: simp_num_pair_def Let_def)
        also have "\ = (real_of_int ?g' * ?t) / (real_of_int ?g' * (real_of_int (n div ?g')))"
          by simp
        also have "\ = (Inum bs ?t' / real_of_int n)"
          using real_of_int_div[OF gpdd] th2 gp0 by simp
        finally have "?lhs = Inum bs t / real_of_int n"
          by simp
        then show ?thesis
          by (simp add: simp_num_pair_def)
      qed
    qed
  qed
qed

lemma simp_num_pair_l:
  assumes tnb: "numbound0 t"
    and np: "n > 0"
    and tn: "simp_num_pair (t, n) = (t', n')"
  shows "numbound0 t' \ n' > 0"
proof -
  let ?t' = "simpnum t"
  let ?g = "numgcd ?t'"
  let ?g' = "gcd n ?g"
  show ?thesis
  proof (cases "n = 0")
    case True
    then show ?thesis
      using assms by (simp add: Let_def simp_num_pair_def)
  next
    case nnz: False
    show ?thesis
    proof (cases "?g > 1")
      case False
      then show ?thesis
        using assms by (auto simp add: Let_def simp_num_pair_def)
    next
      case g1: True
      then have g0: "?g > 0" by simp
      from g1 nnz have gp0: "?g' \ 0" by simp
      then have g'p: "?g' > 0" using gcd_ge_0_int[where x="n" and y="numgcd ?t'"]
        by arith
      then consider "?g'= 1" | "?g' > 1" by arith
      then show ?thesis
      proof cases
        case 1
        then show ?thesis
          using assms g1 by (auto simp add: Let_def simp_num_pair_def)
      next
        case g'1: 2
        have gpdg: "?g' dvd ?g" by simp
        have gpdd: "?g' dvd n" by simp
        have gpdgp: "?g' dvd ?g'" by simp
        from zdvd_imp_le[OF gpdd np] have g'n: "?g' \<le> n" .
        from zdiv_mono1[OF g'n g'p, simplified div_self[OF gp0]] have "n div ?g' > 0"
          by simp
        then show ?thesis
          using assms g1 g'1
          by (auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0)
      qed
    qed
  qed
qed

fun simpfm :: "fm \ fm"
where
  "simpfm (And p q) = conj (simpfm p) (simpfm q)"
| "simpfm (Or p q) = disj (simpfm p) (simpfm q)"
| "simpfm (Imp p q) = imp (simpfm p) (simpfm q)"
| "simpfm (Iff p q) = iff (simpfm p) (simpfm q)"
| "simpfm (Not p) = not (simpfm p)"
| "simpfm (Lt a) = (let a' = simpnum a in case a' of C v \ if (v < 0) then T else F | _ \ Lt a')"
| "simpfm (Le a) = (let a' = simpnum a in case a' of C v \ if (v \ 0) then T else F | _ \ Le a')"
| "simpfm (Gt a) = (let a' = simpnum a in case a' of C v \ if (v > 0) then T else F | _ \ Gt a')"
| "simpfm (Ge a) = (let a' = simpnum a in case a' of C v \ if (v \ 0) then T else F | _ \ Ge a')"
| "simpfm (Eq a) = (let a' = simpnum a in case a' of C v \ if (v = 0) then T else F | _ \ Eq a')"
| "simpfm (NEq a) = (let a' = simpnum a in case a' of C v \ if (v \ 0) then T else F | _ \ NEq a')"
| "simpfm p = p"

lemma simpfm: "Ifm bs (simpfm p) = Ifm bs p"
proof (induct p rule: simpfm.induct)
  case (6 a)
  let ?sa = "simpnum a"
  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
    by simp
  consider v where "?sa = C v" | "\ (\v. ?sa = C v)" by blast
  then show ?case
  proof cases
    case 1
    then show ?thesis using sa by simp
  next
    case 2
    then show ?thesis using sa by (cases ?sa) (simp_all add: Let_def)
  qed
next
  case (7 a)
  let ?sa = "simpnum a"
  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
    by simp
  consider v where "?sa = C v" | "\ (\v. ?sa = C v)" by blast
  then show ?case
  proof cases
    case 1
    then show ?thesis using sa by simp
  next
    case 2
    then show ?thesis using sa by (cases ?sa) (simp_all add: Let_def)
  qed
next
  case (8 a)
  let ?sa = "simpnum a"
  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
    by simp
  consider v where "?sa = C v" | "\ (\v. ?sa = C v)" by blast
  then show ?case
  proof cases
    case 1
    then show ?thesis using sa by simp
  next
    case 2
    then show ?thesis using sa by (cases ?sa) (simp_all add: Let_def)
  qed
next
  case (9 a)
  let ?sa = "simpnum a"
  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
    by simp
  consider v where "?sa = C v" | "\ (\v. ?sa = C v)" by blast
  then show ?case
  proof cases
    case 1
    then show ?thesis using sa by simp
  next
    case 2
    then show ?thesis using sa by (cases ?sa) (simp_all add: Let_def)
  qed
next
  case (10 a)
  let ?sa = "simpnum a"
  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
    by simp
  consider v where "?sa = C v" | "\ (\v. ?sa = C v)" by blast
  then show ?case
  proof cases
    case 1
    then show ?thesis using sa by simp
  next
    case 2
    then show ?thesis using sa by (cases ?sa) (simp_all add: Let_def)
  qed
next
  case (11 a)
  let ?sa = "simpnum a"
  from simpnum_ci have sa: "Inum bs ?sa = Inum bs a"
    by simp
  consider v where "?sa = C v" | "\ (\v. ?sa = C v)" by blast
  then show ?case
  proof cases
    case 1
    then show ?thesis using sa by simp
  next
    case 2
    then show ?thesis using sa by (cases ?sa) (simp_all add: Let_def)
  qed
qed (induct p rule: simpfm.induct, simp_all)

lemma simpfm_bound0: "bound0 p \ bound0 (simpfm p)"
proof (induct p rule: simpfm.induct)
  case (6 a)
  then have nb: "numbound0 a" by simp
  then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
  then show ?case by (cases "simpnum a") (auto simp add: Let_def)
next
  case (7 a)
  then have nb: "numbound0 a" by simp
  then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
  then show ?case by (cases "simpnum a") (auto simp add: Let_def)
next
  case (8 a)
  then have nb: "numbound0 a" by simp
  then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
  then show ?case by (cases "simpnum a") (auto simp add: Let_def)
next
  case (9 a)
  then have nb: "numbound0 a" by simp
  then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
  then show ?case by (cases "simpnum a") (auto simp add: Let_def)
next
  case (10 a)
  then have nb: "numbound0 a" by simp
  then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
  then show ?case by (cases "simpnum a") (auto simp add: Let_def)
next
  case (11 a)
  then have nb: "numbound0 a" by simp
  then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
  then show ?case by (cases "simpnum a") (auto simp add: Let_def)
qed (auto simp add: disj_def imp_def iff_def conj_def)

lemma simpfm_qf: "qfree p \ qfree (simpfm p)"
  by (induct p rule: simpfm.induct) (auto simp: Let_def split: num.splits)

fun prep :: "fm \ fm"
where
  "prep (E T) = T"
| "prep (E F) = F"
| "prep (E (Or p q)) = disj (prep (E p)) (prep (E q))"
| "prep (E (Imp p q)) = disj (prep (E (Not p))) (prep (E q))"
| "prep (E (Iff p q)) = disj (prep (E (And p q))) (prep (E (And (Not p) (Not q))))"
| "prep (E (Not (And p q))) = disj (prep (E (Not p))) (prep (E(Not q)))"
| "prep (E (Not (Imp p q))) = prep (E (And p (Not q)))"
| "prep (E (Not (Iff p q))) = disj (prep (E (And p (Not q)))) (prep (E(And (Not p) q)))"
| "prep (E p) = E (prep p)"
| "prep (A (And p q)) = conj (prep (A p)) (prep (A q))"
| "prep (A p) = prep (Not (E (Not p)))"
| "prep (Not (Not p)) = prep p"
| "prep (Not (And p q)) = disj (prep (Not p)) (prep (Not q))"
| "prep (Not (A p)) = prep (E (Not p))"
| "prep (Not (Or p q)) = conj (prep (Not p)) (prep (Not q))"
| "prep (Not (Imp p q)) = conj (prep p) (prep (Not q))"
| "prep (Not (Iff p q)) = disj (prep (And p (Not q))) (prep (And (Not p) q))"
| "prep (Not p) = not (prep p)"
| "prep (Or p q) = disj (prep p) (prep q)"
| "prep (And p q) = conj (prep p) (prep q)"
| "prep (Imp p q) = prep (Or (Not p) q)"
| "prep (Iff p q) = disj (prep (And p q)) (prep (And (Not p) (Not q)))"
| "prep p = p"

lemma prep: "\bs. Ifm bs (prep p) = Ifm bs p"
  by (induct p rule: prep.induct) auto

  (* Generic quantifier elimination *)
fun qelim :: "fm \ (fm \ fm) \ fm"
where
  "qelim (E p) = (\qe. DJ qe (qelim p qe))"
| "qelim (A p) = (\qe. not (qe ((qelim (Not p) qe))))"
| "qelim (Not p) = (\qe. not (qelim p qe))"
| "qelim (And p q) = (\qe. conj (qelim p qe) (qelim q qe))"
| "qelim (Or p q) = (\qe. disj (qelim p qe) (qelim q qe))"
| "qelim (Imp p q) = (\qe. imp (qelim p qe) (qelim q qe))"
| "qelim (Iff p q) = (\qe. iff (qelim p qe) (qelim q qe))"
| "qelim p = (\y. simpfm p)"

lemma qelim_ci:
  assumes qe_inv: "\bs p. qfree p \ qfree (qe p) \ (Ifm bs (qe p) = Ifm bs (E p))"
  shows "\bs. qfree (qelim p qe) \ (Ifm bs (qelim p qe) = Ifm bs p)"
  using qe_inv DJ_qe[OF qe_inv]
  by (induct p rule: qelim.induct)
    (auto simp add: simpfm simpfm_qf simp del: simpfm.simps)

fun minusinf:: "fm \ fm" (* Virtual substitution of -\*)
where
  "minusinf (And p q) = conj (minusinf p) (minusinf q)"
| "minusinf (Or p q) = disj (minusinf p) (minusinf q)"
| "minusinf (Eq (CN 0 c e)) = F"
| "minusinf (NEq (CN 0 c e)) = T"
| "minusinf (Lt (CN 0 c e)) = T"
| "minusinf (Le (CN 0 c e)) = T"
| "minusinf (Gt (CN 0 c e)) = F"
| "minusinf (Ge (CN 0 c e)) = F"
| "minusinf p = p"

fun plusinf:: "fm \ fm" (* Virtual substitution of +\*)
where
  "plusinf (And p q) = conj (plusinf p) (plusinf q)"
| "plusinf (Or p q) = disj (plusinf p) (plusinf q)"
| "plusinf (Eq (CN 0 c e)) = F"
| "plusinf (NEq (CN 0 c e)) = T"
| "plusinf (Lt (CN 0 c e)) = F"
| "plusinf (Le (CN 0 c e)) = F"
| "plusinf (Gt (CN 0 c e)) = T"
| "plusinf (Ge (CN 0 c e)) = T"
| "plusinf p = p"

fun isrlfm :: "fm \ bool" (* Linearity test for fm *)
where
  "isrlfm (And p q) = (isrlfm p \ isrlfm q)"
| "isrlfm (Or p q) = (isrlfm p \ isrlfm q)"
| "isrlfm (Eq (CN 0 c e)) = (c>0 \ numbound0 e)"
| "isrlfm (NEq (CN 0 c e)) = (c>0 \ numbound0 e)"
| "isrlfm (Lt (CN 0 c e)) = (c>0 \ numbound0 e)"
| "isrlfm (Le (CN 0 c e)) = (c>0 \ numbound0 e)"
| "isrlfm (Gt (CN 0 c e)) = (c>0 \ numbound0 e)"
| "isrlfm (Ge (CN 0 c e)) = (c>0 \ numbound0 e)"
| "isrlfm p = (isatom p \ (bound0 p))"

  (* splits the bounded from the unbounded part*)
fun rsplit0 :: "num \ int \ num"
where
  "rsplit0 (Bound 0) = (1,C 0)"
| "rsplit0 (Add a b) = (let (ca,ta) = rsplit0 a; (cb,tb) = rsplit0 b in (ca + cb, Add ta tb))"
| "rsplit0 (Sub a b) = rsplit0 (Add a (Neg b))"
| "rsplit0 (Neg a) = (let (c,t) = rsplit0 a in (- c, Neg t))"
| "rsplit0 (Mul c a) = (let (ca,ta) = rsplit0 a in (c * ca, Mul c ta))"
| "rsplit0 (CN 0 c a) = (let (ca,ta) = rsplit0 a in (c + ca, ta))"
| "rsplit0 (CN n c a) = (let (ca,ta) = rsplit0 a in (ca, CN n c ta))"
| "rsplit0 t = (0,t)"

lemma rsplit0: "Inum bs ((case_prod (CN 0)) (rsplit0 t)) = Inum bs t \ numbound0 (snd (rsplit0 t))"
proof (induct t rule: rsplit0.induct)
  case (2 a b)
  let ?sa = "rsplit0 a"
  let ?sb = "rsplit0 b"
  let ?ca = "fst ?sa"
  let ?cb = "fst ?sb"
  let ?ta = "snd ?sa"
  let ?tb = "snd ?sb"
  from 2 have nb: "numbound0 (snd(rsplit0 (Add a b)))"
    by (cases "rsplit0 a") (auto simp add: Let_def split_def)
  have "Inum bs ((case_prod (CN 0)) (rsplit0 (Add a b))) =
    Inum bs ((case_prod (CN 0)) ?sa)+Inum bs ((case_prod (CN 0)) ?sb)"
    by (simp add: Let_def split_def algebra_simps)
  also have "\ = Inum bs a + Inum bs b"
    using 2 by (cases "rsplit0 a") auto
  finally show ?case
    using nb by simp
qed (auto simp add: Let_def split_def algebra_simps, simp add: distrib_left[symmetric])

    (* Linearize a formula*)
definition lt :: "int \ num \ fm"
where
  "lt c t = (if c = 0 then (Lt t) else if c > 0 then (Lt (CN 0 c t))
    else (Gt (CN 0 (-c) (Neg t))))"

definition le :: "int \ num \ fm"
where
  "le c t = (if c = 0 then (Le t) else if c > 0 then (Le (CN 0 c t))
    else (Ge (CN 0 (-c) (Neg t))))"

definition gt :: "int \ num \ fm"
where
  "gt c t = (if c = 0 then (Gt t) else if c > 0 then (Gt (CN 0 c t))
    else (Lt (CN 0 (-c) (Neg t))))"

definition ge :: "int \ num \ fm"
where
  "ge c t = (if c = 0 then (Ge t) else if c > 0 then (Ge (CN 0 c t))
    else (Le (CN 0 (-c) (Neg t))))"

definition eq :: "int \ num \ fm"
where
  "eq c t = (if c = 0 then (Eq t) else if c > 0 then (Eq (CN 0 c t))
    else (Eq (CN 0 (-c) (Neg t))))"

definition neq :: "int \ num \ fm"
where
  "neq c t = (if c = 0 then (NEq t) else if c > 0 then (NEq (CN 0 c t))
    else (NEq (CN 0 (-c) (Neg t))))"

lemma lt: "numnoabs t \ Ifm bs (case_prod lt (rsplit0 t)) =
  Ifm bs (Lt t) \<and> isrlfm (case_prod lt (rsplit0 t))"
  using rsplit0[where bs = "bs" and t="t"]
  by (auto simp add: lt_def split_def, cases "snd(rsplit0 t)", auto,
    rename_tac nat a b, case_tac "nat", auto)

lemma le: "numnoabs t \ Ifm bs (case_prod le (rsplit0 t)) =
  Ifm bs (Le t) \<and> isrlfm (case_prod le (rsplit0 t))"
  using rsplit0[where bs = "bs" and t="t"]
  by (auto simp add: le_def split_def, cases "snd(rsplit0 t)", auto,
    rename_tac nat a b, case_tac "nat", auto)

lemma gt: "numnoabs t \ Ifm bs (case_prod gt (rsplit0 t)) =
  Ifm bs (Gt t) \<and> isrlfm (case_prod gt (rsplit0 t))"
  using rsplit0[where bs = "bs" and t="t"]
  by (auto simp add: gt_def split_def, cases "snd(rsplit0 t)", auto,
    rename_tac nat a b, case_tac "nat", auto)

lemma ge: "numnoabs t \ Ifm bs (case_prod ge (rsplit0 t)) =
  Ifm bs (Ge t) \<and> isrlfm (case_prod ge (rsplit0 t))"
  using rsplit0[where bs = "bs" and t="t"]
  by (auto simp add: ge_def split_def, cases "snd(rsplit0 t)", auto,
    rename_tac nat a b, case_tac "nat", auto)

lemma eq: "numnoabs t \ Ifm bs (case_prod eq (rsplit0 t)) =
  Ifm bs (Eq t) \<and> isrlfm (case_prod eq (rsplit0 t))"
  using rsplit0[where bs = "bs" and t="t"]
  by (auto simp add: eq_def split_def, cases "snd(rsplit0 t)", auto,
    rename_tac nat a b, case_tac "nat", auto)

lemma neq: "numnoabs t \ Ifm bs (case_prod neq (rsplit0 t)) =
  Ifm bs (NEq t) \<and> isrlfm (case_prod neq (rsplit0 t))"
  using rsplit0[where bs = "bs" and t="t"]
  by (auto simp add: neq_def split_def, cases "snd(rsplit0 t)", auto,
    rename_tac nat a b, case_tac "nat", auto)

lemma conj_lin: "isrlfm p \ isrlfm q \ isrlfm (conj p q)"
  by (auto simp add: conj_def)

lemma disj_lin: "isrlfm p \ isrlfm q \ isrlfm (disj p q)"
  by (auto simp add: disj_def)

fun rlfm :: "fm \ fm"
where
  "rlfm (And p q) = conj (rlfm p) (rlfm q)"
| "rlfm (Or p q) = disj (rlfm p) (rlfm q)"
| "rlfm (Imp p q) = disj (rlfm (Not p)) (rlfm q)"
| "rlfm (Iff p q) = disj (conj (rlfm p) (rlfm q)) (conj (rlfm (Not p)) (rlfm (Not q)))"
| "rlfm (Lt a) = case_prod lt (rsplit0 a)"
| "rlfm (Le a) = case_prod le (rsplit0 a)"
| "rlfm (Gt a) = case_prod gt (rsplit0 a)"
| "rlfm (Ge a) = case_prod ge (rsplit0 a)"
| "rlfm (Eq a) = case_prod eq (rsplit0 a)"
| "rlfm (NEq a) = case_prod neq (rsplit0 a)"
| "rlfm (Not (And p q)) = disj (rlfm (Not p)) (rlfm (Not q))"
| "rlfm (Not (Or p q)) = conj (rlfm (Not p)) (rlfm (Not q))"
| "rlfm (Not (Imp p q)) = conj (rlfm p) (rlfm (Not q))"
| "rlfm (Not (Iff p q)) = disj (conj(rlfm p) (rlfm(Not q))) (conj(rlfm(Not p)) (rlfm q))"
| "rlfm (Not (Not p)) = rlfm p"
| "rlfm (Not T) = F"
| "rlfm (Not F) = T"
| "rlfm (Not (Lt a)) = rlfm (Ge a)"
| "rlfm (Not (Le a)) = rlfm (Gt a)"
| "rlfm (Not (Gt a)) = rlfm (Le a)"
| "rlfm (Not (Ge a)) = rlfm (Lt a)"
| "rlfm (Not (Eq a)) = rlfm (NEq a)"
| "rlfm (Not (NEq a)) = rlfm (Eq a)"
| "rlfm p = p"

lemma rlfm_I:
  assumes qfp: "qfree p"
  shows "(Ifm bs (rlfm p) = Ifm bs p) \ isrlfm (rlfm p)"
  using qfp
  by (induct p rule: rlfm.induct) (auto simp add: lt le gt ge eq neq conj_lin disj_lin)

    (* Operations needed for Ferrante and Rackoff *)
lemma rminusinf_inf:
  assumes lp: "isrlfm p"
  shows "\z. \x < z. Ifm (x#bs) (minusinf p) = Ifm (x#bs) p" (is "\z. \x. ?P z x p")
  using lp
proof (induct p rule: minusinf.induct)
  case (1 p q)
  then show ?case
    by (fastforce simp: intro: exI [where x= "min _ _"])
next
  case (2 p q)
  then show ?case
    by (fastforce simp: intro: exI [where x= "min _ _"])
next
  case (3 c e)
  from 3 have nb: "numbound0 e" by simp
  from 3 have cp: "real_of_int c > 0" by simp
  fix a
  let ?e = "Inum (a#bs) e"
  let ?z = "(- ?e) / real_of_int c"
  {
    fix x
    assume xz: "x < ?z"
    then have "(real_of_int c * x < - ?e)"
      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps)
    then have "real_of_int c * x + ?e < 0" by arith
    then have "real_of_int c * x + ?e \ 0" by simp
    with xz have "?P ?z x (Eq (CN 0 c e))"
      using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp
  }
  then have "\x < ?z. ?P ?z x (Eq (CN 0 c e))" by simp
  then show ?case by blast
next
  case (4 c e)
  from 4 have nb: "numbound0 e" by simp
  from 4 have cp: "real_of_int c > 0" by simp
  fix a
  let ?e = "Inum (a # bs) e"
  let ?z = "(- ?e) / real_of_int c"
  {
    fix x
    assume xz: "x < ?z"
    then have "(real_of_int c * x < - ?e)"
      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps)
    then have "real_of_int c * x + ?e < 0" by arith
    then have "real_of_int c * x + ?e \ 0" by simp
    with xz have "?P ?z x (NEq (CN 0 c e))"
      using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp
  }
  then have "\x < ?z. ?P ?z x (NEq (CN 0 c e))" by simp
  then show ?case by blast
next
  case (5 c e)
  from 5 have nb: "numbound0 e" by simp
  from 5 have cp: "real_of_int c > 0" by simp
  fix a
  let ?e="Inum (a#bs) e"
  let ?z = "(- ?e) / real_of_int c"
  {
    fix x
    assume xz: "x < ?z"
    then have "(real_of_int c * x < - ?e)"
      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps)
    then have "real_of_int c * x + ?e < 0" by arith
    with xz have "?P ?z x (Lt (CN 0 c e))"
      using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp
  }
  then have "\x < ?z. ?P ?z x (Lt (CN 0 c e))" by simp
  then show ?case by blast
next
  case (6 c e)
  from 6 have nb: "numbound0 e" by simp
  from lp 6 have cp: "real_of_int c > 0" by simp
  fix a
  let ?e = "Inum (a # bs) e"
  let ?z = "(- ?e) / real_of_int c"
  {
    fix x
    assume xz: "x < ?z"
    then have "(real_of_int c * x < - ?e)"
      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps)
    then have "real_of_int c * x + ?e < 0" by arith
    with xz have "?P ?z x (Le (CN 0 c e))"
      using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp
  }
  then have "\x < ?z. ?P ?z x (Le (CN 0 c e))" by simp
  then show ?case by blast
next
  case (7 c e)
  from 7 have nb: "numbound0 e" by simp
  from 7 have cp: "real_of_int c > 0" by simp
  fix a
  let ?e = "Inum (a # bs) e"
  let ?z = "(- ?e) / real_of_int c"
  {
    fix x
    assume xz: "x < ?z"
    then have "(real_of_int c * x < - ?e)"
      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps)
    then have "real_of_int c * x + ?e < 0" by arith
    with xz have "?P ?z x (Gt (CN 0 c e))"
      using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp
  }
  then have "\x < ?z. ?P ?z x (Gt (CN 0 c e))" by simp
  then show ?case by blast
next
  case (8 c e)
  from 8 have nb: "numbound0 e" by simp
  from 8 have cp: "real_of_int c > 0" by simp
  fix a
  let ?e="Inum (a#bs) e"
  let ?z = "(- ?e) / real_of_int c"
  {
    fix x
    assume xz: "x < ?z"
    then have "(real_of_int c * x < - ?e)"
      by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="- ?e"] ac_simps)
    then have "real_of_int c * x + ?e < 0" by arith
    with xz have "?P ?z x (Ge (CN 0 c e))"
      using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp
  }
  then have "\x < ?z. ?P ?z x (Ge (CN 0 c e))" by simp
  then show ?case by blast
qed simp_all

lemma rplusinf_inf:
  assumes lp: "isrlfm p"
  shows "\z. \x > z. Ifm (x#bs) (plusinf p) = Ifm (x#bs) p" (is "\z. \x. ?P z x p")
using lp
proof (induct p rule: isrlfm.induct)
  case (1 p q)
  then show ?case
    by (fastforce simp: intro: exI [where x= "max _ _"])
next
  case (2 p q)
  then show ?case
    by (fastforce simp: intro: exI [where x= "max _ _"])
next
  case (3 c e)
  from 3 have nb: "numbound0 e" by simp
  from 3 have cp: "real_of_int c > 0" by simp
  fix a
  let ?e = "Inum (a # bs) e"
  let ?z = "(- ?e) / real_of_int c"
  {
    fix x
    assume xz: "x > ?z"
    with mult_strict_right_mono [OF xz cp] cp
    have "(real_of_int c * x > - ?e)" by (simp add: ac_simps)
    then have "real_of_int c * x + ?e > 0" by arith
    then have "real_of_int c * x + ?e \ 0" by simp
    with xz have "?P ?z x (Eq (CN 0 c e))"
      using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp
  }
  then have "\x > ?z. ?P ?z x (Eq (CN 0 c e))" by simp
  then show ?case by blast
next
  case (4 c e)
  from 4 have nb: "numbound0 e" by simp
  from 4 have cp: "real_of_int c > 0" by simp
  fix a
  let ?e = "Inum (a # bs) e"
  let ?z = "(- ?e) / real_of_int c"
  {
    fix x
    assume xz: "x > ?z"
    with mult_strict_right_mono [OF xz cp] cp
    have "(real_of_int c * x > - ?e)" by (simp add: ac_simps)
    then have "real_of_int c * x + ?e > 0" by arith
    then have "real_of_int c * x + ?e \ 0" by simp
    with xz have "?P ?z x (NEq (CN 0 c e))"
      using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp
  }
  then have "\x > ?z. ?P ?z x (NEq (CN 0 c e))" by simp
  then show ?case by blast
next
  case (5 c e)
  from 5 have nb: "numbound0 e" by simp
  from 5 have cp: "real_of_int c > 0" by simp
  fix a
  let ?e = "Inum (a # bs) e"
  let ?z = "(- ?e) / real_of_int c"
  {
    fix x
    assume xz: "x > ?z"
    with mult_strict_right_mono [OF xz cp] cp
    have "(real_of_int c * x > - ?e)" by (simp add: ac_simps)
    then have "real_of_int c * x + ?e > 0" by arith
    with xz have "?P ?z x (Lt (CN 0 c e))"
      using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp
  }
  then have "\x > ?z. ?P ?z x (Lt (CN 0 c e))" by simp
  then show ?case by blast
next
  case (6 c e)
  from 6 have nb: "numbound0 e" by simp
  from 6 have cp: "real_of_int c > 0" by simp
  fix a
  let ?e = "Inum (a # bs) e"
  let ?z = "(- ?e) / real_of_int c"
  {
    fix x
    assume xz: "x > ?z"
    with mult_strict_right_mono [OF xz cp] cp
    have "(real_of_int c * x > - ?e)" by (simp add: ac_simps)
    then have "real_of_int c * x + ?e > 0" by arith
    with xz have "?P ?z x (Le (CN 0 c e))"
      using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp
  }
  then have "\x > ?z. ?P ?z x (Le (CN 0 c e))" by simp
  then show ?case by blast
next
  case (7 c e)
  from 7 have nb: "numbound0 e" by simp
  from 7 have cp: "real_of_int c > 0" by simp
  fix a
  let ?e = "Inum (a # bs) e"
  let ?z = "(- ?e) / real_of_int c"
  {
    fix x
    assume xz: "x > ?z"
    with mult_strict_right_mono [OF xz cp] cp
    have "(real_of_int c * x > - ?e)" by (simp add: ac_simps)
    then have "real_of_int c * x + ?e > 0" by arith
    with xz have "?P ?z x (Gt (CN 0 c e))"
      using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp
  }
  then have "\x > ?z. ?P ?z x (Gt (CN 0 c e))" by simp
  then show ?case by blast
next
  case (8 c e)
  from 8 have nb: "numbound0 e" by simp
  from 8 have cp: "real_of_int c > 0" by simp
  fix a
  let ?e="Inum (a#bs) e"
  let ?z = "(- ?e) / real_of_int c"
  {
    fix x
    assume xz: "x > ?z"
    with mult_strict_right_mono [OF xz cp] cp
    have "(real_of_int c * x > - ?e)" by (simp add: ac_simps)
    then have "real_of_int c * x + ?e > 0" by arith
    with xz have "?P ?z x (Ge (CN 0 c e))"
      using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp
  }
  then have "\x > ?z. ?P ?z x (Ge (CN 0 c e))" by simp
  then show ?case by blast
qed simp_all

lemma rminusinf_bound0:
  assumes lp: "isrlfm p"
  shows "bound0 (minusinf p)"
  using lp by (induct p rule: minusinf.induct) simp_all

lemma rplusinf_bound0:
  assumes lp: "isrlfm p"
  shows "bound0 (plusinf p)"
  using lp by (induct p rule: plusinf.induct) simp_all

lemma rminusinf_ex:
  assumes lp: "isrlfm p"
    and ex: "Ifm (a#bs) (minusinf p)"
  shows "\x. Ifm (x#bs) p"
proof -
  from bound0_I [OF rminusinf_bound0[OF lp], where b="a" and bs ="bs"] ex
  have th: "\x. Ifm (x#bs) (minusinf p)" by auto
  from rminusinf_inf[OF lp, where bs="bs"]
  obtain z where z_def: "\x
  from th have "Ifm ((z - 1) # bs) (minusinf p)" by simp
  moreover have "z - 1 < z" by simp
  ultimately show ?thesis using z_def by auto
qed

lemma rplusinf_ex:
  assumes lp: "isrlfm p"
    and ex: "Ifm (a # bs) (plusinf p)"
  shows "\x. Ifm (x # bs) p"
proof -
  from bound0_I [OF rplusinf_bound0[OF lp], where b="a" and bs ="bs"] ex
  have th: "\x. Ifm (x # bs) (plusinf p)" by auto
  from rplusinf_inf[OF lp, where bs="bs"]
  obtain z where z_def: "\x>z. Ifm (x # bs) (plusinf p) = Ifm (x # bs) p" by blast
  from th have "Ifm ((z + 1) # bs) (plusinf p)" by simp
  moreover have "z + 1 > z" by simp
  ultimately show ?thesis using z_def by auto
qed

fun uset :: "fm \ (num \ int) list"
where
  "uset (And p q) = (uset p @ uset q)"
| "uset (Or p q) = (uset p @ uset q)"
| "uset (Eq (CN 0 c e)) = [(Neg e,c)]"
| "uset (NEq (CN 0 c e)) = [(Neg e,c)]"
| "uset (Lt (CN 0 c e)) = [(Neg e,c)]"
| "uset (Le (CN 0 c e)) = [(Neg e,c)]"
| "uset (Gt (CN 0 c e)) = [(Neg e,c)]"
| "uset (Ge (CN 0 c e)) = [(Neg e,c)]"
| "uset p = []"

fun usubst :: "fm \ num \ int \ fm"
where
  "usubst (And p q) = (\(t,n). And (usubst p (t,n)) (usubst q (t,n)))"
| "usubst (Or p q) = (\(t,n). Or (usubst p (t,n)) (usubst q (t,n)))"
| "usubst (Eq (CN 0 c e)) = (\(t,n). Eq (Add (Mul c t) (Mul n e)))"
| "usubst (NEq (CN 0 c e)) = (\(t,n). NEq (Add (Mul c t) (Mul n e)))"
| "usubst (Lt (CN 0 c e)) = (\(t,n). Lt (Add (Mul c t) (Mul n e)))"
| "usubst (Le (CN 0 c e)) = (\(t,n). Le (Add (Mul c t) (Mul n e)))"
| "usubst (Gt (CN 0 c e)) = (\(t,n). Gt (Add (Mul c t) (Mul n e)))"
| "usubst (Ge (CN 0 c e)) = (\(t,n). Ge (Add (Mul c t) (Mul n e)))"
| "usubst p = (\(t, n). p)"

lemma usubst_I:
  assumes lp: "isrlfm p"
    and np: "real_of_int n > 0"
    and nbt: "numbound0 t"
  shows "(Ifm (x # bs) (usubst p (t,n)) =
    Ifm (((Inum (x # bs) t) / (real_of_int n)) # bs) p) \<and> bound0 (usubst p (t, n))"
  (is "(?I x (usubst p (t, n)) = ?I ?u p) \ ?B p"
   is "(_ = ?I (?t/?n) p) \ _"
   is "(_ = ?I (?N x t /_) p) \ _")
  using lp
proof (induct p rule: usubst.induct)
  case (5 c e)
  with assms have cp: "c > 0" and nb: "numbound0 e" by simp_all
  have "?I ?u (Lt (CN 0 c e)) \ real_of_int c * (?t / ?n) + ?N x e < 0"
    using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
  also have "\ \ ?n * (real_of_int c * (?t / ?n)) + ?n*(?N x e) < 0"
    by (simp only: pos_less_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
      and b="0", simplified div_0]) (simp only: algebra_simps)
  also have "\ \ real_of_int c * ?t + ?n * (?N x e) < 0" using np by simp
  finally show ?case using nbt nb by (simp add: algebra_simps)
next
  case (6 c e)
  with assms have cp: "c > 0" and nb: "numbound0 e" by simp_all
  have "?I ?u (Le (CN 0 c e)) \ real_of_int c * (?t / ?n) + ?N x e \ 0"
    using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
  also have "\ = (?n*(real_of_int c *(?t/?n)) + ?n*(?N x e) \ 0)"
    by (simp only: pos_le_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
      and b="0", simplified div_0]) (simp only: algebra_simps)
  also have "\ = (real_of_int c *?t + ?n* (?N x e) \ 0)" using np by simp
  finally show ?case using nbt nb by (simp add: algebra_simps)
next
  case (7 c e)
  with assms have cp: "c >0" and nb: "numbound0 e" by simp_all
  have "?I ?u (Gt (CN 0 c e)) \ real_of_int c *(?t / ?n) + ?N x e > 0"
    using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
  also have "\ \ ?n * (real_of_int c * (?t / ?n)) + ?n * ?N x e > 0"
    by (simp only: pos_divide_less_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
      and b="0", simplified div_0]) (simp only: algebra_simps)
  also have "\ \ real_of_int c * ?t + ?n * ?N x e > 0" using np by simp
  finally show ?case using nbt nb by (simp add: algebra_simps)
next
  case (8 c e)
  with assms have cp: "c > 0" and nb: "numbound0 e" by simp_all
  have "?I ?u (Ge (CN 0 c e)) \ real_of_int c * (?t / ?n) + ?N x e \ 0"
    using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
  also have "\ \ ?n * (real_of_int c * (?t / ?n)) + ?n * ?N x e \ 0"
    by (simp only: pos_divide_le_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
      and b="0", simplified div_0]) (simp only: algebra_simps)
  also have "\ \ real_of_int c * ?t + ?n * ?N x e \ 0" using np by simp
  finally show ?case using nbt nb by (simp add: algebra_simps)
next
  case (3 c e)
  with assms have cp: "c > 0" and nb: "numbound0 e" by simp_all
  from np have np: "real_of_int n \ 0" by simp
  have "?I ?u (Eq (CN 0 c e)) \ real_of_int c * (?t / ?n) + ?N x e = 0"
    using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
  also have "\ \ ?n * (real_of_int c * (?t / ?n)) + ?n * ?N x e = 0"
    by (simp only: nonzero_eq_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
      and b="0", simplified div_0]) (simp only: algebra_simps)
  also have "\ \ real_of_int c * ?t + ?n * ?N x e = 0" using np by simp
  finally show ?case using nbt nb by (simp add: algebra_simps)
next
  case (4 c e) with assms have cp: "c >0" and nb: "numbound0 e" by simp_all
  from np have np: "real_of_int n \ 0" by simp
  have "?I ?u (NEq (CN 0 c e)) \ real_of_int c * (?t / ?n) + ?N x e \ 0"
    using numbound0_I[OF nb, where bs="bs" and b="?u" and b'="x"] by simp
  also have "\ \ ?n * (real_of_int c * (?t / ?n)) + ?n * ?N x e \ 0"
    by (simp only: nonzero_eq_divide_eq[OF np, where a="real_of_int c *(?t/?n) + (?N x e)"
      and b="0", simplified div_0]) (simp only: algebra_simps)
  also have "\ \ real_of_int c * ?t + ?n * ?N x e \ 0" using np by simp
  finally show ?case using nbt nb by (simp add: algebra_simps)
qed(simp_all add: nbt numbound0_I[where bs ="bs" and b="(Inum (x#bs) t)/ real_of_int n" and b'="x"])

lemma uset_l:
  assumes lp: "isrlfm p"
  shows "\(t,k) \ set (uset p). numbound0 t \ k > 0"
  using lp by (induct p rule: uset.induct) auto

lemma rminusinf_uset:
  assumes lp: "isrlfm p"
    and nmi: "\ (Ifm (a # bs) (minusinf p))" (is "\ (Ifm (a # bs) (?M p))")
    and ex: "Ifm (x#bs) p" (is "?I x p")
  shows "\(s,m) \ set (uset p). x \ Inum (a#bs) s / real_of_int m"
    (is "\(s,m) \ ?U p. x \ ?N a s / real_of_int m")
proof -
  have "\(s,m) \ set (uset p). real_of_int m * x \ Inum (a#bs) s"
    (is "\(s,m) \ ?U p. real_of_int m *x \ ?N a s")
    using lp nmi ex
    by (induct p rule: minusinf.induct) (auto simp add:numbound0_I[where bs="bs" and b="a" and b'="x"])
  then obtain s m where smU: "(s,m) \ set (uset p)" and mx: "real_of_int m * x \ ?N a s"
    by blast
  from uset_l[OF lp] smU have mp: "real_of_int m > 0"
    by auto
  from pos_divide_le_eq[OF mp, where a="x" and b="?N a s", symmetric] mx have "x \ ?N a s / real_of_int m"
    by (auto simp add: mult.commute)
  then show ?thesis
    using smU by auto
qed

lemma rplusinf_uset:
  assumes lp: "isrlfm p"
    and nmi: "\ (Ifm (a # bs) (plusinf p))" (is "\ (Ifm (a # bs) (?M p))")
    and ex: "Ifm (x # bs) p" (is "?I x p")
  shows "\(s,m) \ set (uset p). x \ Inum (a#bs) s / real_of_int m"
    (is "\(s,m) \ ?U p. x \ ?N a s / real_of_int m")
proof -
  have "\(s,m) \ set (uset p). real_of_int m * x \ Inum (a#bs) s"
    (is "\(s,m) \ ?U p. real_of_int m *x \ ?N a s")
    using lp nmi ex
    by (induct p rule: minusinf.induct)
      (auto simp add:numbound0_I[where bs="bs" and b="a" and b'="x"])
  then obtain s m where smU: "(s,m) \ set (uset p)" and mx: "real_of_int m * x \ ?N a s"
    by blast
  from uset_l[OF lp] smU have mp: "real_of_int m > 0"
    by auto
  from pos_le_divide_eq[OF mp, where a="x" and b="?N a s", symmetric] mx have "x \ ?N a s / real_of_int m"
    by (auto simp add: mult.commute)
  then show ?thesis
    using smU by auto
qed

lemma lin_dense:
  assumes lp: "isrlfm p"
    and noS: "\t. l < t \ t< u \ t \ (\(t,n). Inum (x#bs) t / real_of_int n) ` set (uset p)"
      (is "\t. _ \ _ \ t \ (\(t,n). ?N x t / real_of_int n ) ` (?U p)")
    and lx: "l < x"
    and xu:"x < u"
    and px:" Ifm (x#bs) p"
    and ly: "l < y" and yu: "y < u"
  shows "Ifm (y#bs) p"
  using lp px noS
proof (induct p rule: isrlfm.induct)
  case (5 c e)
  then have cp: "real_of_int c > 0" and nb: "numbound0 e"
    by simp_all
  from 5 have "x * real_of_int c + ?N x e < 0"
    by (simp add: algebra_simps)
  then have pxc: "x < (- ?N x e) / real_of_int c"
    by (simp only: pos_less_divide_eq[OF cp, where a="x" and b="-?N x e"])
  from 5 have noSc:"\t. l < t \ t < u \ t \ (- ?N x e) / real_of_int c"
    by auto
  with ly yu have yne: "y \ - ?N x e / real_of_int c"
    by auto
  then consider "y < (-?N x e)/ real_of_int c" | "y > (- ?N x e) / real_of_int c"
    by atomize_elim auto
  then show ?case
  proof cases
    case 1
    then have "y * real_of_int c < - ?N x e"
      by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric])
    then have "real_of_int c * y + ?N x e < 0"
      by (simp add: algebra_simps)
    then show ?thesis
      using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp
  next
    case 2
    with yu have eu: "u > (- ?N x e) / real_of_int c"
      by auto
    with noSc ly yu have "(- ?N x e) / real_of_int c \ l"
      by (cases "(- ?N x e) / real_of_int c > l") auto
    with lx pxc have False
      by auto
    then show ?thesis ..
  qed
next
  case (6 c e)
  then have cp: "real_of_int c > 0" and nb: "numbound0 e"
    by simp_all
  from 6 have "x * real_of_int c + ?N x e \ 0"
    by (simp add: algebra_simps)
  then have pxc: "x \ (- ?N x e) / real_of_int c"
    by (simp only: pos_le_divide_eq[OF cp, where a="x" and b="-?N x e"])
  from 6 have noSc:"\t. l < t \ t < u \ t \ (- ?N x e) / real_of_int c"
    by auto
  with ly yu have yne: "y \ - ?N x e / real_of_int c"
    by auto
  then consider "y < (- ?N x e) / real_of_int c" | "y > (-?N x e) / real_of_int c"
    by atomize_elim auto
  then show ?case
  proof cases
    case 1
    then have "y * real_of_int c < - ?N x e"
      by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric])
    then have "real_of_int c * y + ?N x e < 0"
      by (simp add: algebra_simps)
    then show ?thesis
      using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp
  next
    case 2
    with yu have eu: "u > (- ?N x e) / real_of_int c"
      by auto
    with noSc ly yu have "(- ?N x e) / real_of_int c \ l"
      by (cases "(- ?N x e) / real_of_int c > l") auto
    with lx pxc have False
      by auto
    then show ?thesis ..
  qed
next
  case (7 c e)
  then have cp: "real_of_int c > 0" and nb: "numbound0 e"
    by simp_all
  from 7 have "x * real_of_int c + ?N x e > 0"
    by (simp add: algebra_simps)
  then have pxc: "x > (- ?N x e) / real_of_int c"
    by (simp only: pos_divide_less_eq[OF cp, where a="x" and b="-?N x e"])
  from 7 have noSc: "\t. l < t \ t < u \ t \ (- ?N x e) / real_of_int c"
    by auto
  with ly yu have yne: "y \ - ?N x e / real_of_int c"
    by auto
  then consider "y > (- ?N x e) / real_of_int c" | "y < (-?N x e) / real_of_int c"
    by atomize_elim auto
  then show ?case
  proof cases
    case 1
    then have "y * real_of_int c > - ?N x e"
      by (simp add: pos_divide_less_eq[OF cp, where a="y" and b="-?N x e", symmetric])
    then have "real_of_int c * y + ?N x e > 0"
      by (simp add: algebra_simps)
    then show ?thesis
      using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp
  next
    case 2
    with ly have eu: "l < (- ?N x e) / real_of_int c"
      by auto
    with noSc ly yu have "(- ?N x e) / real_of_int c \ u"
      by (cases "(- ?N x e) / real_of_int c > l") auto
    with xu pxc have False by auto
    then show ?thesis ..
  qed
next
  case (8 c e)
  then have cp: "real_of_int c > 0" and nb: "numbound0 e"
    by simp_all
  from 8 have "x * real_of_int c + ?N x e \ 0"
    by (simp add: algebra_simps)
  then have pxc: "x \ (- ?N x e) / real_of_int c"
    by (simp only: pos_divide_le_eq[OF cp, where a="x" and b="-?N x e"])
  from 8 have noSc:"\t. l < t \ t < u \ t \ (- ?N x e) / real_of_int c"
    by auto
--> --------------------

--> maximum size reached

--> --------------------

quality100%

¤ Dauer der Verarbeitung: 0.30 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.