(*  Title:      HOL/Decision_Procs/MIR.thy

     Author:     Amine Chaieb

 *)

 theory MIR

 imports Complex_Main Dense_Linear_Order Efficient_Nat

 uses ("mir_tac.ML")

 begin

 section {* Quantifier elimination for @{text "\<real> (0, 1, +, floor, <)"} *}

 declare real_of_int_floor_cancel [simp del]

 primrec alluopairs:: "'a list \<Rightarrow> ('a \<times> 'a) list" where 

   "alluopairs [] = []"

 | "alluopairs (x#xs) = (map (Pair x) (x#xs))@(alluopairs xs)"

 lemma alluopairs_set1: "set (alluopairs xs) \<le> {(x,y). x\<in> set xs \<and> y\<in> set xs}"

 by (induct xs, auto)

 lemma alluopairs_set:

   "\<lbrakk>x\<in> set xs ; y \<in> set xs\<rbrakk> \<Longrightarrow> (x,y) \<in> set (alluopairs xs) \<or> (y,x) \<in> set (alluopairs xs) "

 by (induct xs, auto)

 lemma alluopairs_ex:

   assumes Pc: "\<forall> x y. P x y = P y x"

   shows "(\<exists> x \<in> set xs. \<exists> y \<in> set xs. P x y) = (\<exists> (x,y) \<in> set (alluopairs xs). P x y)"

 proof

   assume "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y"

   then obtain x y where x: "x \<in> set xs" and y:"y \<in> set xs" and P: "P x y"  by blast

   from alluopairs_set[OF x y] P Pc show"\<exists>(x, y)\<in>set (alluopairs xs). P x y" 

     by auto

 next

   assume "\<exists>(x, y)\<in>set (alluopairs xs). P x y"

   then obtain "x" and "y"  where xy:"(x,y) \<in> set (alluopairs xs)" and P: "P x y" by blast+

   from xy have "x \<in> set xs \<and> y\<in> set xs" using alluopairs_set1 by blast

   with P show "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y" by blast

 qed

   (* generate a list from i to j*)

 consts iupt :: "int \<times> int \<Rightarrow> int list"

 recdef iupt "measure (\<lambda> (i,j). nat (j-i +1))" 

   "iupt (i,j) = (if j <i then [] else (i# iupt(i+1, j)))"

 lemma iupt_set: "set (iupt(i,j)) = {i .. j}"

 proof(induct rule: iupt.induct)

   case (1 a b)

   show ?case

     using prems by (simp add: simp_from_to)

 qed

 lemma nth_pos2: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)"

 using Nat.gr0_conv_Suc

 by clarsimp

 lemma myl: "\<forall> (a::'a::{ordered_ab_group_add}) (b::'a). (a \<le> b) = (0 \<le> b - a)" 

 proof(clarify)

   fix x y ::"'a"

   have "(x \<le> y) = (x - y \<le> 0)" by (simp only: le_iff_diff_le_0[where a="x" and b="y"])

   also have "\<dots> = (- (y - x) \<le> 0)" by simp

   also have "\<dots> = (0 \<le> y - x)" by (simp only: neg_le_0_iff_le[where a="y-x"])

   finally show "(x \<le> y) = (0 \<le> y - x)" .

 qed

 lemma myless: "\<forall> (a::'a::{ordered_ab_group_add}) (b::'a). (a < b) = (0 < b - a)" 

 proof(clarify)

   fix x y ::"'a"

   have "(x < y) = (x - y < 0)" by (simp only: less_iff_diff_less_0[where a="x" and b="y"])

   also have "\<dots> = (- (y - x) < 0)" by simp

   also have "\<dots> = (0 < y - x)" by (simp only: neg_less_0_iff_less[where a="y-x"])

   finally show "(x < y) = (0 < y - x)" .

 qed

 lemma myeq: "\<forall> (a::'a::{ordered_ab_group_add}) (b::'a). (a = b) = (0 = b - a)"

   by auto

   (* Maybe should be added to the library \<dots> *)

 lemma floor_int_eq: "(real n\<le> x \<and> x < real (n+1)) = (floor x = n)"

 proof( auto)

   assume lb: "real n \<le> x"

     and ub: "x < real n + 1"

   have "real (floor x) \<le> x" by simp 

   hence "real (floor x) < real (n + 1) " using ub by arith

   hence "floor x < n+1" by simp

   moreover from lb have "n \<le> floor x" using floor_mono[where x="real n" and y="x"] 

     by simp ultimately show "floor x = n" by simp

 qed

 (* Periodicity of dvd *)

 lemma dvd_period:

   assumes advdd: "(a::int) dvd d"

   shows "(a dvd (x + t)) = (a dvd ((x+ c*d) + t))"

   using advdd  

 proof-

   {fix x k

     from inf_period(3)[OF advdd, rule_format, where x=x and k="-k"]  

     have " ((a::int) dvd (x + t)) = (a dvd (x+k*d + t))" by simp}

   hence "\<forall>x.\<forall>k. ((a::int) dvd (x + t)) = (a dvd (x+k*d + t))"  by simp

   then show ?thesis by simp

 qed

 (* The Divisibility relation between reals *)

 definition

   rdvd:: "real \<Rightarrow> real \<Rightarrow> bool" (infixl "rdvd" 50)

 where

   rdvd_def: "x rdvd y \<longleftrightarrow> (\<exists>k\<Colon>int. y = x * real k)"

 lemma int_rdvd_real: 

   shows "real (i::int) rdvd x = (i dvd (floor x) \<and> real (floor x) = x)" (is "?l = ?r")

 proof

   assume "?l" 

   hence th: "\<exists> k. x=real (i*k)" by (simp add: rdvd_def)

   hence th': "real (floor x) = x" by (auto simp del: real_of_int_mult)

   with th have "\<exists> k. real (floor x) = real (i*k)" by simp

   hence "\<exists> k. floor x = i*k" by (simp only: real_of_int_inject)

   thus ?r  using th' by (simp add: dvd_def) 

 next

   assume "?r" hence "(i\<Colon>int) dvd \<lfloor>x\<Colon>real\<rfloor>" ..

   hence "\<exists> k. real (floor x) = real (i*k)" 

     by (simp only: real_of_int_inject) (simp add: dvd_def)

   thus ?l using prems by (simp add: rdvd_def)

 qed

 lemma int_rdvd_iff: "(real (i::int) rdvd real t) = (i dvd t)"

 by (auto simp add: rdvd_def dvd_def) (rule_tac x="k" in exI, simp only :real_of_int_mult[symmetric])

 lemma rdvd_abs1: 

   "(abs (real d) rdvd t) = (real (d ::int) rdvd t)"

 proof

   assume d: "real d rdvd t"

   from d int_rdvd_real have d2: "d dvd (floor t)" and ti: "real (floor t) = t" by auto

   from iffD2[OF abs_dvd_iff] d2 have "(abs d) dvd (floor t)" by blast

   with ti int_rdvd_real[symmetric] have "real (abs d) rdvd t" by blast 

   thus "abs (real d) rdvd t" by simp

 next

   assume "abs (real d) rdvd t" hence "real (abs d) rdvd t" by simp

   with int_rdvd_real[where i="abs d" and x="t"] have d2: "abs d dvd floor t" and ti: "real (floor t) =t" by auto

   from iffD1[OF abs_dvd_iff] d2 have "d dvd floor t" by blast

   with ti int_rdvd_real[symmetric] show "real d rdvd t" by blast

 qed

 lemma rdvd_minus: "(real (d::int) rdvd t) = (real d rdvd -t)"

   apply (auto simp add: rdvd_def)

   apply (rule_tac x="-k" in exI, simp) 

   apply (rule_tac x="-k" in exI, simp)

 done

 lemma rdvd_left_0_eq: "(0 rdvd t) = (t=0)"

 by (auto simp add: rdvd_def)

 lemma rdvd_mult: 

   assumes knz: "k\<noteq>0"

   shows "(real (n::int) * real (k::int) rdvd x * real k) = (real n rdvd x)"

 using knz by (simp add:rdvd_def)

 lemma rdvd_trans: assumes mn:"m rdvd n" and  nk:"n rdvd k" 

   shows "m rdvd k"

 proof-

   from rdvd_def mn obtain c where nmc:"n = m * real (c::int)" by auto

   from rdvd_def nk obtain c' where nkc:"k = n * real (c'::int)" by auto

   hence "k = m * real (c * c')" using nmc by simp

   thus ?thesis using rdvd_def by blast

 qed

   (*********************************************************************************)

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

   (*********************************************************************************)

 datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num 

   | Mul int num | Floor num| CF int num num

   (* A size for num to make inductive proofs simpler*)

 primrec num_size :: "num \<Rightarrow> nat" where

  "num_size (C c) = 1"

 | "num_size (Bound n) = 1"

 | "num_size (Neg a) = 1 + num_size a"

 | "num_size (Add a b) = 1 + num_size a + num_size b"

 | "num_size (Sub a b) = 3 + num_size a + num_size b"

 | "num_size (CN n c a) = 4 + num_size a "

 | "num_size (CF c a b) = 4 + num_size a + num_size b"

 | "num_size (Mul c a) = 1 + num_size a"

 | "num_size (Floor a) = 1 + num_size a"

   (* Semantics of numeral terms (num) *)

 primrec Inum :: "real list \<Rightarrow> num \<Rightarrow> real" where

   "Inum bs (C c) = (real c)"

 | "Inum bs (Bound n) = bs!n"

 | "Inum bs (CN n c a) = (real 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 c) * Inum bs a"

 | "Inum bs (Floor a) = real (floor (Inum bs a))"

 | "Inum bs (CF c a b) = real c * real (floor (Inum bs a)) + Inum bs b"

 definition "isint t bs \<equiv> real (floor (Inum bs t)) = Inum bs t"

 lemma isint_iff: "isint n bs = (real (floor (Inum bs n)) = Inum bs n)"

 by (simp add: isint_def)

 lemma isint_Floor: "isint (Floor n) bs"

   by (simp add: isint_iff)

 lemma isint_Mul: "isint e bs \<Longrightarrow> isint (Mul c e) bs"

 proof-

   let ?e = "Inum bs e"

   let ?fe = "floor ?e"

   assume be: "isint e bs" hence efe:"real ?fe = ?e" by (simp add: isint_iff)

   have "real ((floor (Inum bs (Mul c e)))) = real (floor (real (c * ?fe)))" using efe by simp

   also have "\<dots> = real (c* ?fe)" by (simp only: floor_real_of_int) 

   also have "\<dots> = real c * ?e" using efe by simp

   finally show ?thesis using isint_iff by simp

 qed

 lemma isint_neg: "isint e bs \<Longrightarrow> isint (Neg e) bs"

 proof-

   let ?I = "\<lambda> t. Inum bs t"

   assume ie: "isint e bs"

   hence th: "real (floor (?I e)) = ?I e" by (simp add: isint_def)  

   have "real (floor (?I (Neg e))) = real (floor (- (real (floor (?I e)))))" by (simp add: th)

   also have "\<dots> = - real (floor (?I e))" by(simp add: floor_minus_real_of_int) 

   finally show "isint (Neg e) bs" by (simp add: isint_def th)

 qed

 lemma isint_sub: 

   assumes ie: "isint e bs" shows "isint (Sub (C c) e) bs"

 proof-

   let ?I = "\<lambda> t. Inum bs t"

   from ie have th: "real (floor (?I e)) = ?I e" by (simp add: isint_def)  

   have "real (floor (?I (Sub (C c) e))) = real (floor ((real (c -floor (?I e)))))" by (simp add: th)

   also have "\<dots> = real (c- floor (?I e))" by(simp add: floor_minus_real_of_int) 

   finally show "isint (Sub (C c) e) bs" by (simp add: isint_def th)

 qed

 lemma isint_add: assumes

   ai:"isint a bs" and bi: "isint b bs" shows "isint (Add a b) bs"

 proof-

   let ?a = "Inum bs a"

   let ?b = "Inum bs b"

   from ai bi isint_iff have "real (floor (?a + ?b)) = real (floor (real (floor ?a) + real (floor ?b)))" by simp

   also have "\<dots> = real (floor ?a) + real (floor ?b)" by simp

   also have "\<dots> = ?a + ?b" using ai bi isint_iff by simp

   finally show "isint (Add a b) bs" by (simp add: isint_iff)

 qed

 lemma isint_c: "isint (C j) bs"

   by (simp add: isint_iff)

     (* FORMULAE *)

 datatype fm  = 

   T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| Dvd int num| NDvd int num|

   NOT fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm

   (* A size for fm *)

 fun fmsize :: "fm \<Rightarrow> nat" where

  "fmsize (NOT p) = 1 + fmsize p"

 | "fmsize (And p q) = 1 + fmsize p + fmsize q"

 | "fmsize (Or p q) = 1 + fmsize p + fmsize q"

 | "fmsize (Imp p q) = 3 + fmsize p + fmsize q"

 | "fmsize (Iff p q) = 3 + 2*(fmsize p + fmsize q)"

 | "fmsize (E p) = 1 + fmsize p"

 | "fmsize (A p) = 4+ fmsize p"

 | "fmsize (Dvd i t) = 2"

 | "fmsize (NDvd i t) = 2"

 | "fmsize p = 1"

   (* several lemmas about fmsize *)

 lemma fmsize_pos: "fmsize p > 0"

 by (induct p rule: fmsize.induct) simp_all

   (* Semantics of formulae (fm) *)

 primrec Ifm ::"real list \<Rightarrow> fm \<Rightarrow> 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 \<le> 0)"

 | "Ifm bs (Ge a) = (Inum bs a \<ge> 0)"

 | "Ifm bs (Eq a) = (Inum bs a = 0)"

 | "Ifm bs (NEq a) = (Inum bs a \<noteq> 0)"

 | "Ifm bs (Dvd i b) = (real i rdvd Inum bs b)"

 | "Ifm bs (NDvd i b) = (\<not>(real i rdvd Inum bs b))"

 | "Ifm bs (NOT p) = (\<not> (Ifm bs p))"

 | "Ifm bs (And p q) = (Ifm bs p \<and> Ifm bs q)"

 | "Ifm bs (Or p q) = (Ifm bs p \<or> Ifm bs q)"

 | "Ifm bs (Imp p q) = ((Ifm bs p) \<longrightarrow> (Ifm bs q))"

 | "Ifm bs (Iff p q) = (Ifm bs p = Ifm bs q)"

 | "Ifm bs (E p) = (\<exists> x. Ifm (x#bs) p)"

 | "Ifm bs (A p) = (\<forall> x. Ifm (x#bs) p)"

 consts prep :: "fm \<Rightarrow> fm"

 recdef prep "measure fmsize"

   "prep (E T) = T"

   "prep (E F) = F"

   "prep (E (Or p q)) = Or (prep (E p)) (prep (E q))"

   "prep (E (Imp p q)) = Or (prep (E (NOT p))) (prep (E q))"

   "prep (E (Iff p q)) = Or (prep (E (And p q))) (prep (E (And (NOT p) (NOT q))))" 

   "prep (E (NOT (And p q))) = Or (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))) = Or (prep (E (And p (NOT q)))) (prep (E(And (NOT p) q)))"

   "prep (E p) = E (prep p)"

   "prep (A (And p q)) = And (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)) = Or (prep (NOT p)) (prep (NOT q))"

   "prep (NOT (A p)) = prep (E (NOT p))"

   "prep (NOT (Or p q)) = And (prep (NOT p)) (prep (NOT q))"

   "prep (NOT (Imp p q)) = And (prep p) (prep (NOT q))"

   "prep (NOT (Iff p q)) = Or (prep (And p (NOT q))) (prep (And (NOT p) q))"

   "prep (NOT p) = NOT (prep p)"

   "prep (Or p q) = Or (prep p) (prep q)"

   "prep (And p q) = And (prep p) (prep q)"

   "prep (Imp p q) = prep (Or (NOT p) q)"

   "prep (Iff p q) = Or (prep (And p q)) (prep (And (NOT p) (NOT q)))"

   "prep p = p"

 (hints simp add: fmsize_pos)

 lemma prep: "\<And> bs. Ifm bs (prep p) = Ifm bs p"

 by (induct p rule: prep.induct, auto)

   (* Quantifier freeness *)

 fun qfree:: "fm \<Rightarrow> bool" where

   "qfree (E p) = False"

   | "qfree (A p) = False"

   | "qfree (NOT p) = qfree p" 

   | "qfree (And p q) = (qfree p \<and> qfree q)" 

   | "qfree (Or  p q) = (qfree p \<and> qfree q)" 

   | "qfree (Imp p q) = (qfree p \<and> qfree q)" 

   | "qfree (Iff p q) = (qfree p \<and> qfree q)"

   | "qfree p = True"

   (* Boundedness and substitution *)

 primrec numbound0 :: "num \<Rightarrow> bool" (* a num is INDEPENDENT of Bound 0 *) where

   "numbound0 (C c) = True"

   | "numbound0 (Bound n) = (n>0)"

   | "numbound0 (CN n i a) = (n > 0 \<and> numbound0 a)"

   | "numbound0 (Neg a) = numbound0 a"

   | "numbound0 (Add a b) = (numbound0 a \<and> numbound0 b)"

   | "numbound0 (Sub a b) = (numbound0 a \<and> numbound0 b)" 

   | "numbound0 (Mul i a) = numbound0 a"

   | "numbound0 (Floor a) = numbound0 a"

   | "numbound0 (CF c a b) = (numbound0 a \<and> numbound0 b)" 

 lemma numbound0_I:

   assumes nb: "numbound0 a"

   shows "Inum (b#bs) a = Inum (b'#bs) a"

   using nb by (induct a) (auto simp add: nth_pos2)

 lemma numbound0_gen: 

   assumes nb: "numbound0 t" and ti: "isint t (x#bs)"

   shows "\<forall> y. isint t (y#bs)"

 using nb ti 

 proof(clarify)

   fix y

   from numbound0_I[OF nb, where bs="bs" and b="y" and b'="x"] ti[simplified isint_def]

   show "isint t (y#bs)"

     by (simp add: isint_def)

 qed

 primrec bound0:: "fm \<Rightarrow> 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 (Dvd i a) = numbound0 a"

   | "bound0 (NDvd i a) = numbound0 a"

   | "bound0 (NOT p) = bound0 p"

   | "bound0 (And p q) = (bound0 p \<and> bound0 q)"

   | "bound0 (Or p q) = (bound0 p \<and> bound0 q)"

   | "bound0 (Imp p q) = ((bound0 p) \<and> (bound0 q))"

   | "bound0 (Iff p q) = (bound0 p \<and> 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 simp add: nth_pos2)

 primrec numsubst0:: "num \<Rightarrow> num \<Rightarrow> num" (* substitute a num into a num for Bound 0 *) where

   "numsubst0 t (C c) = (C c)"

   | "numsubst0 t (Bound n) = (if n=0 then t else Bound n)"

   | "numsubst0 t (CN n i a) = (if n=0 then Add (Mul i t) (numsubst0 t a) else CN n i (numsubst0 t a))"

   | "numsubst0 t (CF i a b) = CF i (numsubst0 t a) (numsubst0 t b)"

   | "numsubst0 t (Neg a) = Neg (numsubst0 t a)"

   | "numsubst0 t (Add a b) = Add (numsubst0 t a) (numsubst0 t b)"

   | "numsubst0 t (Sub a b) = Sub (numsubst0 t a) (numsubst0 t b)" 

   | "numsubst0 t (Mul i a) = Mul i (numsubst0 t a)"

   | "numsubst0 t (Floor a) = Floor (numsubst0 t a)"

 lemma numsubst0_I:

   shows "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b#bs) a)#bs) t"

   by (induct t) (simp_all add: nth_pos2)

 lemma numsubst0_I':

   assumes nb: "numbound0 a"

   shows "Inum (b#bs) (numsubst0 a t) = Inum ((Inum (b'#bs) a)#bs) t"

   by (induct t) (simp_all add: nth_pos2 numbound0_I[OF nb, where b="b" and b'="b'"])

 primrec subst0:: "num \<Rightarrow> fm \<Rightarrow> fm" (* substitue a num into a formula for Bound 0 *) where

   "subst0 t T = T"

   | "subst0 t F = F"

   | "subst0 t (Lt a) = Lt (numsubst0 t a)"

   | "subst0 t (Le a) = Le (numsubst0 t a)"

   | "subst0 t (Gt a) = Gt (numsubst0 t a)"

   | "subst0 t (Ge a) = Ge (numsubst0 t a)"

   | "subst0 t (Eq a) = Eq (numsubst0 t a)"

   | "subst0 t (NEq a) = NEq (numsubst0 t a)"

   | "subst0 t (Dvd i a) = Dvd i (numsubst0 t a)"

   | "subst0 t (NDvd i a) = NDvd i (numsubst0 t a)"

   | "subst0 t (NOT p) = NOT (subst0 t p)"

   | "subst0 t (And p q) = And (subst0 t p) (subst0 t q)"

   | "subst0 t (Or p q) = Or (subst0 t p) (subst0 t q)"

   | "subst0 t (Imp p q) = Imp (subst0 t p) (subst0 t q)"

   | "subst0 t (Iff p q) = Iff (subst0 t p) (subst0 t q)"

 lemma subst0_I: assumes qfp: "qfree p"

   shows "Ifm (b#bs) (subst0 a p) = Ifm ((Inum (b#bs) a)#bs) p"

   using qfp numsubst0_I[where b="b" and bs="bs" and a="a"]

   by (induct p) (simp_all add: nth_pos2 )

 consts

   decrnum:: "num \<Rightarrow> num" 

   decr :: "fm \<Rightarrow> fm"

 recdef decrnum "measure size"

   "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 (Floor a) = Floor (decrnum a)"

   "decrnum (CN n c a) = CN (n - 1) c (decrnum a)"

   "decrnum (CF c a b) = CF c (decrnum a) (decrnum b)"

   "decrnum a = a"

 recdef decr "measure size"

   "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 (Dvd i a) = Dvd i (decrnum a)"

   "decr (NDvd i a) = NDvd i (decrnum a)"

   "decr (NOT p) = NOT (decr p)" 

   "decr (And p q) = And (decr p) (decr q)"

   "decr (Or p q) = Or (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 add: nth_pos2)

 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: nth_pos2 decrnum)

 lemma decr_qf: "bound0 p \<Longrightarrow> qfree (decr p)"

 by (induct p, simp_all)

 consts 

   isatom :: "fm \<Rightarrow> bool" (* test for atomicity *)

 recdef isatom "measure size"

   "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 (Dvd i b) = True"

   "isatom (NDvd i b) = True"

   "isatom p = False"

 lemma numsubst0_numbound0: assumes nb: "numbound0 t"

   shows "numbound0 (numsubst0 t a)"

 using nb by (induct a, auto)

 lemma subst0_bound0: assumes qf: "qfree p" and nb: "numbound0 t"

   shows "bound0 (subst0 t p)"

 using qf numsubst0_numbound0[OF nb] by (induct p, auto)

 lemma bound0_qf: "bound0 p \<Longrightarrow> qfree p"

 by (induct p, simp_all)

 definition djf:: "('a \<Rightarrow> fm) \<Rightarrow> 'a \<Rightarrow> fm \<Rightarrow> 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 fp q))"

 definition evaldjf:: "('a \<Rightarrow> fm) \<Rightarrow> 'a list \<Rightarrow> 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 evaldjf_ex: "Ifm bs (evaldjf f ps) = (\<exists> p \<in> set ps. Ifm bs (f p))"

   by(induct ps, simp_all add: evaldjf_def djf_Or)

 lemma evaldjf_bound0: 

   assumes nb: "\<forall> x\<in> 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: "\<forall> x\<in> 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) 

 consts 

   disjuncts :: "fm \<Rightarrow> fm list" 

   conjuncts :: "fm \<Rightarrow> fm list"

 recdef disjuncts "measure size"

   "disjuncts (Or p q) = (disjuncts p) @ (disjuncts q)"

   "disjuncts F = []"

   "disjuncts p = [p]"

 recdef conjuncts "measure size"

   "conjuncts (And p q) = (conjuncts p) @ (conjuncts q)"

   "conjuncts T = []"

   "conjuncts p = [p]"

 lemma disjuncts: "(\<exists> q\<in> set (disjuncts p). Ifm bs q) = Ifm bs p"

 by(induct p rule: disjuncts.induct, auto)

 lemma conjuncts: "(\<forall> q\<in> set (conjuncts p). Ifm bs q) = Ifm bs p"

 by(induct p rule: conjuncts.induct, auto)

 lemma disjuncts_nb: "bound0 p \<Longrightarrow> \<forall> q\<in> set (disjuncts p). bound0 q"

 proof-

   assume nb: "bound0 p"

   hence "list_all bound0 (disjuncts p)" by (induct p rule:disjuncts.induct,auto)

   thus ?thesis by (simp only: list_all_iff)

 qed

 lemma conjuncts_nb: "bound0 p \<Longrightarrow> \<forall> q\<in> set (conjuncts p). bound0 q"

 proof-

   assume nb: "bound0 p"

   hence "list_all bound0 (conjuncts p)" by (induct p rule:conjuncts.induct,auto)

   thus ?thesis by (simp only: list_all_iff)

 qed

 lemma disjuncts_qf: "qfree p \<Longrightarrow> \<forall> q\<in> set (disjuncts p). qfree q"

 proof-

   assume qf: "qfree p"

   hence "list_all qfree (disjuncts p)"

     by (induct p rule: disjuncts.induct, auto)

   thus ?thesis by (simp only: list_all_iff)

 qed

 lemma conjuncts_qf: "qfree p \<Longrightarrow> \<forall> q\<in> set (conjuncts p). qfree q"

 proof-

   assume qf: "qfree p"

   hence "list_all qfree (conjuncts p)"

     by (induct p rule: conjuncts.induct, auto)

   thus ?thesis by (simp only: list_all_iff)

 qed

 definition DJ :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm" where

   "DJ f p \<equiv> evaldjf f (disjuncts p)"

 lemma DJ: assumes fdj: "\<forall> p q. f (Or p q) = 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) = (\<exists> q \<in> set (disjuncts p). Ifm bs (f q))"

     by (simp add: DJ_def evaldjf_ex) 

   also have "\<dots> = Ifm bs (f p)" using fdj fF by (induct p rule: disjuncts.induct, auto)

   finally show ?thesis .

 qed

 lemma DJ_qf: assumes 

   fqf: "\<forall> p. qfree p \<longrightarrow> qfree (f p)"

   shows "\<forall>p. qfree p \<longrightarrow> 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 "\<forall> q\<in> set (disjuncts p). qfree q" .

   with fqf have th':"\<forall> q\<in> 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: "\<forall> bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bs (qe p) = Ifm bs (E p))"

   shows "\<forall> bs p. qfree p \<longrightarrow> qfree (DJ qe p) \<and> (Ifm bs ((DJ qe p)) = Ifm bs (E p))"

 proof(clarify)

   fix p::fm and bs

   assume qf: "qfree p"

   from qe have qth: "\<forall> p. qfree p \<longrightarrow> 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) = (\<exists> q\<in> set (disjuncts p). Ifm bs (qe q))"

     by (simp add: DJ_def evaldjf_ex)

   also have "\<dots> = (\<exists> q \<in> set(disjuncts p). Ifm bs (E q))" using qe disjuncts_qf[OF qf] by auto

   also have "\<dots> = Ifm bs (E p)" by (induct p rule: disjuncts.induct, auto)

   finally show "qfree (DJ qe p) \<and> Ifm bs (DJ qe p) = Ifm bs (E p)" using qfth by blast

 qed

   (* Simplification *)

   (* Algebraic simplifications for nums *)

 consts bnds:: "num \<Rightarrow> nat list"

   lex_ns:: "nat list \<times> nat list \<Rightarrow> bool"

 recdef bnds "measure size"

   "bnds (Bound n) = [n]"

   "bnds (CN n c a) = n#(bnds a)"

   "bnds (Neg a) = bnds a"

   "bnds (Add a b) = (bnds a)@(bnds b)"

   "bnds (Sub a b) = (bnds a)@(bnds b)"

   "bnds (Mul i a) = bnds a"

   "bnds (Floor a) = bnds a"

   "bnds (CF c a b) = (bnds a)@(bnds b)"

   "bnds a = []"

 recdef lex_ns "measure (\<lambda> (xs,ys). length xs + length ys)"

   "lex_ns ([], ms) = True"

   "lex_ns (ns, []) = False"

   "lex_ns (n#ns, m#ms) = (n<m \<or> ((n = m) \<and> lex_ns (ns,ms))) "

 definition lex_bnd :: "num \<Rightarrow> num \<Rightarrow> bool" where

   "lex_bnd t s \<equiv> lex_ns (bnds t, bnds s)"

 consts 

   numgcdh:: "num \<Rightarrow> int \<Rightarrow> int"

   reducecoeffh:: "num \<Rightarrow> int \<Rightarrow> num"

   dvdnumcoeff:: "num \<Rightarrow> int \<Rightarrow> bool"

 consts maxcoeff:: "num \<Rightarrow> int"

 recdef maxcoeff "measure size"

   "maxcoeff (C i) = abs i"

   "maxcoeff (CN n c t) = max (abs c) (maxcoeff t)"

   "maxcoeff (CF c t s) = max (abs c) (maxcoeff s)"

   "maxcoeff t = 1"

 lemma maxcoeff_pos: "maxcoeff t \<ge> 0"

   apply (induct t rule: maxcoeff.induct, auto) 

   done

 recdef numgcdh "measure size"

   "numgcdh (C i) = (\<lambda>g. gcd i g)"

   "numgcdh (CN n c t) = (\<lambda>g. gcd c (numgcdh t g))"

   "numgcdh (CF c s t) = (\<lambda>g. gcd c (numgcdh t g))"

   "numgcdh t = (\<lambda>g. 1)"

 definition

   numgcd :: "num \<Rightarrow> int"

 where

   numgcd_def: "numgcd t = numgcdh t (maxcoeff t)"

 recdef reducecoeffh "measure size"

   "reducecoeffh (C i) = (\<lambda> g. C (i div g))"

   "reducecoeffh (CN n c t) = (\<lambda> g. CN n (c div g) (reducecoeffh t g))"

   "reducecoeffh (CF c s t) = (\<lambda> g. CF (c div g)  s (reducecoeffh t g))"

   "reducecoeffh t = (\<lambda>g. t)"

 definition

   reducecoeff :: "num \<Rightarrow> num"

 where

   reducecoeff_def: "reducecoeff t =

   (let g = numgcd t in 

   if g = 0 then C 0 else if g=1 then t else reducecoeffh t g)"

 recdef dvdnumcoeff "measure size"

   "dvdnumcoeff (C i) = (\<lambda> g. g dvd i)"

   "dvdnumcoeff (CN n c t) = (\<lambda> g. g dvd c \<and> (dvdnumcoeff t g))"

   "dvdnumcoeff (CF c s t) = (\<lambda> g. g dvd c \<and> (dvdnumcoeff t g))"

   "dvdnumcoeff t = (\<lambda>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 (abs x) = 0) = (x = 0)"

 by arith

 lemma numgcd0:

   assumes g0: "numgcd t = 0"

   shows "Inum bs t = 0"

 proof-

   have "\<And>x. numgcdh t x= 0 \<Longrightarrow> Inum bs t = 0"

     by (induct t rule: numgcdh.induct, auto)

   thus ?thesis using g0[simplified numgcd_def] by blast

 qed

 lemma numgcdh_pos: assumes gp: "g \<ge> 0" shows "numgcdh t g \<ge> 0"

   using gp

   by (induct t rule: numgcdh.induct, auto)

 lemma numgcd_pos: "numgcd t \<ge>0"

   by (simp add: numgcd_def numgcdh_pos maxcoeff_pos)

 lemma reducecoeffh:

   assumes gt: "dvdnumcoeff t g" and gp: "g > 0" 

   shows "real g *(Inum bs (reducecoeffh t g)) = Inum bs t"

   using gt

 proof(induct t rule: reducecoeffh.induct) 

   case (1 i) hence gd: "g dvd i" by simp

   from gp have gnz: "g \<noteq> 0" by simp

   from prems show ?case by (simp add: real_of_int_div[OF gnz gd])

 next

   case (2 n c t)  hence gd: "g dvd c" by simp

   from gp have gnz: "g \<noteq> 0" by simp

   from prems show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps)

 next

   case (3 c s t)  hence gd: "g dvd c" by simp

   from gp have gnz: "g \<noteq> 0" by simp

   from prems show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps) 

 qed (auto simp add: numgcd_def gp)

 consts ismaxcoeff:: "num \<Rightarrow> int \<Rightarrow> bool"

 recdef ismaxcoeff "measure size"

   "ismaxcoeff (C i) = (\<lambda> x. abs i \<le> x)"

   "ismaxcoeff (CN n c t) = (\<lambda>x. abs c \<le> x \<and> (ismaxcoeff t x))"

   "ismaxcoeff (CF c s t) = (\<lambda>x. abs c \<le> x \<and> (ismaxcoeff t x))"

   "ismaxcoeff t = (\<lambda>x. True)"

 lemma ismaxcoeff_mono: "ismaxcoeff t c \<Longrightarrow> c \<le> c' \<Longrightarrow> 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)

   hence H:"ismaxcoeff t (maxcoeff t)" .

   have thh: "maxcoeff t \<le> max (abs c) (maxcoeff t)" by (simp add: le_maxI2)

   from ismaxcoeff_mono[OF H thh] show ?case by (simp add: le_maxI1)

 next

   case (3 c t s) 

   hence H1:"ismaxcoeff s (maxcoeff s)" by auto

   have thh1: "maxcoeff s \<le> max \<bar>c\<bar> (maxcoeff s)" by (simp add: max_def)

   from ismaxcoeff_mono[OF H1 thh1] show ?case by (simp add: le_maxI1)

 qed simp_all

 lemma zgcd_gt1: "gcd i j > (1::int) \<Longrightarrow> ((abs i > 1 \<and> abs j > 1) \<or> (abs i = 0 \<and> abs j > 1) \<or> (abs i > 1 \<and> abs j = 0))"

   apply (unfold gcd_int_def)

   apply (cases "i = 0", simp_all)

   apply (cases "j = 0", simp_all)

   apply (cases "abs i = 1", simp_all)

   apply (cases "abs j = 1", simp_all)

   apply auto

   done

 lemma numgcdh0:"numgcdh t m = 0 \<Longrightarrow>  m =0"

   by (induct t rule: numgcdh.induct, auto)

 lemma dvdnumcoeff_aux:

   assumes "ismaxcoeff t m" and mp:"m \<ge> 0" and "numgcdh t m > 1"

   shows "dvdnumcoeff t (numgcdh t m)"

 using prems

 proof(induct t rule: numgcdh.induct)

   case (2 n c t) 

   let ?g = "numgcdh t m"

   from prems have th:"gcd c ?g > 1" by simp

   from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]

   have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp

   moreover {assume "abs c > 1" and gp: "?g > 1" with prems

     have th: "dvdnumcoeff t ?g" by simp

     have th': "gcd c ?g dvd ?g" by simp

     from dvdnumcoeff_trans[OF th' th] have ?case by simp }

   moreover {assume "abs c = 0 \<and> ?g > 1"

     with prems have th: "dvdnumcoeff t ?g" by simp

     have th': "gcd c ?g dvd ?g" by simp

     from dvdnumcoeff_trans[OF th' th] have ?case by simp

     hence ?case by simp }

   moreover {assume "abs c > 1" and g0:"?g = 0" 

     from numgcdh0[OF g0] have "m=0". with prems   have ?case by simp }

   ultimately show ?case by blast

 next

   case (3 c s t) 

   let ?g = "numgcdh t m"

   from prems have th:"gcd c ?g > 1" by simp

   from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]

   have "(abs c > 1 \<and> ?g > 1) \<or> (abs c = 0 \<and> ?g > 1) \<or> (abs c > 1 \<and> ?g = 0)" by simp

   moreover {assume "abs c > 1" and gp: "?g > 1" with prems

     have th: "dvdnumcoeff t ?g" by simp

     have th': "gcd c ?g dvd ?g" by simp

     from dvdnumcoeff_trans[OF th' th] have ?case by simp }

   moreover {assume "abs c = 0 \<and> ?g > 1"

     with prems have th: "dvdnumcoeff t ?g" by simp

     have th': "gcd c ?g dvd ?g" by simp

     from dvdnumcoeff_trans[OF th' th] have ?case by simp

     hence ?case by simp }

   moreover {assume "abs c > 1" and g0:"?g = 0" 

     from numgcdh0[OF g0] have "m=0". with prems   have ?case by simp }

   ultimately show ?case by blast

 qed auto

 lemma dvdnumcoeff_aux2:

   assumes "numgcd t > 1" shows "dvdnumcoeff t (numgcd t) \<and> numgcd t > 0"

   using prems 

 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 \<ge> 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 (numgcd t) * (Inum bs (reducecoeff t)) = Inum bs t"

 proof-

   let ?g = "numgcd t"

   have "?g \<ge> 0"  by (simp add: numgcd_pos)

   hence "?g = 0 \<or> ?g = 1 \<or> ?g > 1" by auto

   moreover {assume "?g = 0" hence ?thesis by (simp add: numgcd0)} 

   moreover {assume "?g = 1" hence ?thesis by (simp add: reducecoeff_def)} 

   moreover { assume g1:"?g > 1"

     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 have ?thesis 

       by (simp add: reducecoeff_def Let_def)} 

   ultimately show ?thesis by blast

 qed

 lemma reducecoeffh_numbound0: "numbound0 t \<Longrightarrow> numbound0 (reducecoeffh t g)"

 by (induct t rule: reducecoeffh.induct, auto)

 lemma reducecoeff_numbound0: "numbound0 t \<Longrightarrow> numbound0 (reducecoeff t)"

 using reducecoeffh_numbound0 by (simp add: reducecoeff_def Let_def)

 consts

   simpnum:: "num \<Rightarrow> num"

   numadd:: "num \<times> num \<Rightarrow> num"

   nummul:: "num \<Rightarrow> int \<Rightarrow> num"

 recdef numadd "measure (\<lambda> (t,s). size t + size s)"

   "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 (CF c1 t1 r1,CF c2 t2 r2) = 

    (if t1 = t2 then 

     (let c=c1+c2; s= numadd(r1,r2) in (if c=0 then s else CF c t1 s))

    else if lex_bnd t1 t2 then CF c1 t1 (numadd(r1,CF c2 t2 r2))

    else CF c2 t2 (numadd(CF c1 t1 r1,r2)))"

   "numadd (CF c1 t1 r1,C c) = CF c1 t1 (numadd (r1, C c))"

   "numadd (C c,CF c1 t1 r1) = CF c1 t1 (numadd (r1, C c))"

   "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)"

 apply (induct t s rule: numadd.induct, simp_all add: Let_def)

  apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)

   apply (case_tac "n1 = n2", simp_all add: algebra_simps)

   apply (simp only: left_distrib[symmetric])

  apply simp

 apply (case_tac "lex_bnd t1 t2", simp_all)

  apply (case_tac "c1+c2 = 0")

   by (case_tac "t1 = t2", simp_all add: algebra_simps left_distrib[symmetric] real_of_int_mult[symmetric] real_of_int_add[symmetric]del: real_of_int_mult real_of_int_add left_distrib)

 lemma numadd_nb[simp]: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numadd (t,s))"

 by (induct t s rule: numadd.induct, auto simp add: Let_def)

 recdef nummul "measure size"

   "nummul (C j) = (\<lambda> i. C (i*j))"

   "nummul (CN n c t) = (\<lambda> i. CN n (c*i) (nummul t i))"

   "nummul (CF c t s) = (\<lambda> i. CF (c*i) t (nummul s i))"

   "nummul (Mul c t) = (\<lambda> i. nummul t (i*c))"

   "nummul t = (\<lambda> i. Mul i t)"

 lemma nummul[simp]: "\<And> 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]: "\<And> i. numbound0 t \<Longrightarrow> numbound0 (nummul t i)"

 by (induct t rule: nummul.induct, auto)

 definition numneg :: "num \<Rightarrow> num" where

   "numneg t \<equiv> nummul t (- 1)"

 definition numsub :: "num \<Rightarrow> num \<Rightarrow> num" where

   "numsub s t \<equiv> (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 nummul by simp

 lemma numneg_nb[simp]: "numbound0 t \<Longrightarrow> 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]: "\<lbrakk> numbound0 t ; numbound0 s\<rbrakk> \<Longrightarrow> numbound0 (numsub t s)"

 using numsub_def by simp

 lemma isint_CF: assumes si: "isint s bs" shows "isint (CF c t s) bs"

 proof-

   have cti: "isint (Mul c (Floor t)) bs" by (simp add: isint_Mul isint_Floor)

   have "?thesis = isint (Add (Mul c (Floor t)) s) bs" by (simp add: isint_def)

   also have "\<dots>" by (simp add: isint_add cti si)

   finally show ?thesis .

 qed

 consts split_int:: "num \<Rightarrow> num\<times>num"

 recdef split_int "measure num_size"

   "split_int (C c) = (C 0, C c)"

   "split_int (CN n c b) = 

      (let (bv,bi) = split_int b 

        in (CN n c bv, bi))"

   "split_int (CF c a b) = 

      (let (bv,bi) = split_int b 

        in (bv, CF c a bi))"

   "split_int a = (a,C 0)"

 lemma split_int:"\<And> tv ti. split_int t = (tv,ti) \<Longrightarrow> (Inum bs (Add tv ti) = Inum bs t) \<and> isint ti bs"

 proof (induct t rule: split_int.induct)

   case (2 c n b tv ti)

   let ?bv = "fst (split_int b)"

   let ?bi = "snd (split_int b)"

   have "split_int b = (?bv,?bi)" by simp

   with prems(1) have b:"Inum bs (Add ?bv ?bi) = Inum bs b" and bii: "isint ?bi bs" by blast+

   from prems(2) have tibi: "ti = ?bi" by (simp add: Let_def split_def)

   from prems(2) b[symmetric] bii show ?case by (auto simp add: Let_def split_def)

 next

   case (3 c a b tv ti) 

   let ?bv = "fst (split_int b)"

   let ?bi = "snd (split_int b)"

   have "split_int b = (?bv,?bi)" by simp

   with prems(1) have b:"Inum bs (Add ?bv ?bi) = Inum bs b" and bii: "isint ?bi bs" by blast+

   from prems(2) have tibi: "ti = CF c a ?bi" by (simp add: Let_def split_def)

   from prems(2) b[symmetric] bii show ?case by (auto simp add: Let_def split_def isint_Floor isint_add isint_Mul isint_CF)

 qed (auto simp add: Let_def isint_iff isint_Floor isint_add isint_Mul split_def algebra_simps)

 lemma split_int_nb: "numbound0 t \<Longrightarrow> numbound0 (fst (split_int t)) \<and> numbound0 (snd (split_int t)) "

 by (induct t rule: split_int.induct, auto simp add: Let_def split_def)

 definition

   numfloor:: "num \<Rightarrow> num"

 where

   numfloor_def: "numfloor t = (let (tv,ti) = split_int t in 

   (case tv of C i \<Rightarrow> numadd (tv,ti) 

   | _ \<Rightarrow> numadd(CF 1 tv (C 0),ti)))"

 lemma numfloor[simp]: "Inum bs (numfloor t) = Inum bs (Floor t)" (is "?n t = ?N (Floor t)")

 proof-

   let ?tv = "fst (split_int t)"

   let ?ti = "snd (split_int t)"

   have tvti:"split_int t = (?tv,?ti)" by simp

   {assume H: "\<forall> v. ?tv \<noteq> C v"

     hence th1: "?n t = ?N (Add (Floor ?tv) ?ti)" 

       by (cases ?tv, auto simp add: numfloor_def Let_def split_def numadd)

     from split_int[OF tvti] have "?N (Floor t) = ?N (Floor(Add ?tv ?ti))" and tii:"isint ?ti bs" by simp+

     hence "?N (Floor t) = real (floor (?N (Add ?tv ?ti)))" by simp 

     also have "\<dots> = real (floor (?N ?tv) + (floor (?N ?ti)))"

       by (simp,subst tii[simplified isint_iff, symmetric]) simp

     also have "\<dots> = ?N (Add (Floor ?tv) ?ti)" by (simp add: tii[simplified isint_iff])

     finally have ?thesis using th1 by simp}

   moreover {fix v assume H:"?tv = C v" 

     from split_int[OF tvti] have "?N (Floor t) = ?N (Floor(Add ?tv ?ti))" and tii:"isint ?ti bs" by simp+

     hence "?N (Floor t) = real (floor (?N (Add ?tv ?ti)))" by simp 

     also have "\<dots> = real (floor (?N ?tv) + (floor (?N ?ti)))"

       by (simp,subst tii[simplified isint_iff, symmetric]) simp

     also have "\<dots> = ?N (Add (Floor ?tv) ?ti)" by (simp add: tii[simplified isint_iff])

     finally have ?thesis by (simp add: H numfloor_def Let_def split_def numadd) }

   ultimately show ?thesis by auto

 qed

 lemma numfloor_nb[simp]: "numbound0 t \<Longrightarrow> numbound0 (numfloor t)"

   using split_int_nb[where t="t"]

   by (cases "fst(split_int t)" , auto simp add: numfloor_def Let_def split_def  numadd_nb)

 recdef simpnum "measure num_size"

   "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 (Floor t) = numfloor (simpnum t)"

   "simpnum (CN n c t) = (if c=0 then simpnum t else CN n c (simpnum t))"

   "simpnum (CF c t s) = simpnum(Add (Mul c (Floor t)) s)"

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

 by (induct t rule: simpnum.induct, auto)

 lemma simpnum_numbound0[simp]: 

   "numbound0 t \<Longrightarrow> numbound0 (simpnum t)"

 by (induct t rule: simpnum.induct, auto)

 consts nozerocoeff:: "num \<Rightarrow> bool"

 recdef nozerocoeff "measure size"

   "nozerocoeff (C c) = True"

   "nozerocoeff (CN n c t) = (c\<noteq>0 \<and> nozerocoeff t)"

   "nozerocoeff (CF c s t) = (c \<noteq> 0 \<and> nozerocoeff t)"

   "nozerocoeff (Mul c t) = (c\<noteq>0 \<and> nozerocoeff t)"

   "nozerocoeff t = True"

 lemma numadd_nz : "nozerocoeff a \<Longrightarrow> nozerocoeff b \<Longrightarrow> nozerocoeff (numadd (a,b))"

 by (induct a b rule: numadd.induct,auto simp add: Let_def)

 lemma nummul_nz : "\<And> i. i\<noteq>0 \<Longrightarrow> nozerocoeff a \<Longrightarrow> nozerocoeff (nummul a i)"

   by (induct a rule: nummul.induct,auto simp add: Let_def numadd_nz)

 lemma numneg_nz : "nozerocoeff a \<Longrightarrow> nozerocoeff (numneg a)"

 by (simp add: numneg_def nummul_nz)

 lemma numsub_nz: "nozerocoeff a \<Longrightarrow> nozerocoeff b \<Longrightarrow> nozerocoeff (numsub a b)"

 by (simp add: numsub_def numneg_nz numadd_nz)

 lemma split_int_nz: "nozerocoeff t \<Longrightarrow> nozerocoeff (fst (split_int t)) \<and> nozerocoeff (snd (split_int t))"

 by (induct t rule: split_int.induct,auto simp add: Let_def split_def)

 lemma numfloor_nz: "nozerocoeff t \<Longrightarrow> nozerocoeff (numfloor t)"

 by (simp add: numfloor_def Let_def split_def)

 (cases "fst (split_int t)", simp_all add: split_int_nz numadd_nz)

 lemma simpnum_nz: "nozerocoeff (simpnum t)"

 by(induct t rule: simpnum.induct, auto simp add: numadd_nz numneg_nz numsub_nz nummul_nz numfloor_nz)

 lemma maxcoeff_nz: "nozerocoeff t \<Longrightarrow> maxcoeff t = 0 \<Longrightarrow> t = C 0"

 proof (induct t rule: maxcoeff.induct)

   case (2 n c t)

   hence cnz: "c \<noteq>0" and mx: "max (abs c) (maxcoeff t) = 0" by simp+

   have "max (abs c) (maxcoeff t) \<ge> abs c" by (simp add: le_maxI1)

   with cnz have "max (abs c) (maxcoeff t) > 0" by arith

   with prems show ?case by simp

 next

   case (3 c s t) 

   hence cnz: "c \<noteq>0" and mx: "max (abs c) (maxcoeff t) = 0" by simp+

   have "max (abs c) (maxcoeff t) \<ge> abs c" by (simp add: le_maxI1)

   with cnz have "max (abs c) (maxcoeff t) > 0" by arith

   with prems show ?case by simp

 qed 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 \<times> int) \<Rightarrow> num \<times> int" where

   "simp_num_pair \<equiv> (\<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 "((\<lambda> (t,n). Inum bs t / real n) (simp_num_pair (t,n))) = ((\<lambda> (t,n). Inum bs t / real n) (t,n))"

   (is "?lhs = ?rhs")

 proof-

   let ?t' = "simpnum t"

   let ?g = "numgcd ?t'"

   let ?g' = "gcd n ?g"

   {assume nz: "n = 0" hence ?thesis by (simp add: Let_def simp_num_pair_def)}

   moreover

   { assume nnz: "n \<noteq> 0"

     {assume "\<not> ?g > 1" hence ?thesis by (simp add: Let_def simp_num_pair_def)}

     moreover

     {assume g1:"?g>1" hence g0: "?g > 0" by simp

       from g1 nnz have gp0: "?g' \<noteq> 0" by simp

       hence g'p: "?g' > 0" using gcd_ge_0_int[where x="n" and y="numgcd ?t'"] by arith

       hence "?g'= 1 \<or> ?g' > 1" by arith

       moreover {assume "?g'=1" hence ?thesis by (simp add: Let_def simp_num_pair_def)}

       moreover {assume g'1:"?g'>1"

         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 ?g' * ?t = Inum bs ?t'" by simp

         from prems have "?lhs = ?t / real (n div ?g')" by (simp add: simp_num_pair_def Let_def)

         also have "\<dots> = (real ?g' * ?t) / (real ?g' * (real (n div ?g')))" by simp

         also have "\<dots> = (Inum bs ?t' / real n)"

           using real_of_int_div[OF gp0 gpdd] th2 gp0 by simp

         finally have "?lhs = Inum bs t / real n" by simp

         then have ?thesis using prems by (simp add: simp_num_pair_def)}

       ultimately have ?thesis by blast}

     ultimately have ?thesis by blast} 

   ultimately show ?thesis by blast

 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' \<and> n' >0"

 proof-

     let ?t' = "simpnum t"

   let ?g = "numgcd ?t'"

   let ?g' = "gcd n ?g"

   {assume nz: "n = 0" hence ?thesis using prems by (simp add: Let_def simp_num_pair_def)}

   moreover

   { assume nnz: "n \<noteq> 0"

     {assume "\<not> ?g > 1" hence ?thesis  using prems by (auto simp add: Let_def simp_num_pair_def)}

     moreover

     {assume g1:"?g>1" hence g0: "?g > 0" by simp

       from g1 nnz have gp0: "?g' \<noteq> 0" by simp

       hence g'p: "?g' > 0" using gcd_ge_0_int[where x="n" and y="numgcd ?t'"] by arith

       hence "?g'= 1 \<or> ?g' > 1" by arith

       moreover {assume "?g'=1" hence ?thesis using prems 

           by (auto simp add: Let_def simp_num_pair_def)}

       moreover {assume g'1:"?g'>1"

         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 zdiv_self[OF gp0]]

         have "n div ?g' >0" by simp

         hence ?thesis using prems 

           by(auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0)}

       ultimately have ?thesis by blast}

     ultimately have ?thesis by blast} 

   ultimately show ?thesis by blast

 qed

 consts not:: "fm \<Rightarrow> fm"

 recdef not "measure size"

   "not (NOT p) = p"

   "not T = F"

   "not F = T"

   "not (Lt t) = Ge t"

   "not (Le t) = Gt t"

   "not (Gt t) = Le t"

   "not (Ge t) = Lt t"

   "not (Eq t) = NEq t"

   "not (NEq t) = Eq t"

   "not (Dvd i t) = NDvd i t"

   "not (NDvd i t) = Dvd i t"

   "not (And p q) = Or (not p) (not q)"

   "not (Or p q) = And (not p) (not q)"

   "not p = NOT p"

 lemma not[simp]: "Ifm bs (not p) = Ifm bs (NOT p)"

 by (induct p) auto

 lemma not_qf[simp]: "qfree p \<Longrightarrow> qfree (not p)"

 by (induct p, auto)

 lemma not_nb[simp]: "bound0 p \<Longrightarrow> bound0 (not p)"

 by (induct p, auto)

 definition conj :: "fm \<Rightarrow> fm \<Rightarrow> fm" where

   "conj p q \<equiv> (if (p = F \<or> q=F) then F else if p=T then q else if q=T then p else 

    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 \<or> q=F",simp_all add: conj_def) (cases p,simp_all)

 lemma conj_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (conj p q)"

 using conj_def by auto 

 lemma conj_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (conj p q)"

 using conj_def by auto 

 definition disj :: "fm \<Rightarrow> fm \<Rightarrow> fm" where

   "disj p q \<equiv> (if (p = T \<or> q=T) then T else if p=F then q else if q=F then p 

        else 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 \<or> q=T",simp_all add: disj_def) (cases p,simp_all)

 lemma disj_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (disj p q)"

 using disj_def by auto 

 lemma disj_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (disj p q)"

 using disj_def by auto 

 definition imp :: "fm \<Rightarrow> fm \<Rightarrow> fm" where

   "imp p q \<equiv> (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 \<or> q=T",simp_all add: imp_def)

 lemma imp_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (imp p q)"

 using imp_def by (cases "p=F \<or> q=T",simp_all add: imp_def)

 lemma imp_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (imp p q)"

 using imp_def by (cases "p=F \<or> q=T \<or> p=q",simp_all add: imp_def) 

 definition iff :: "fm \<Rightarrow> fm \<Rightarrow> fm" where

   "iff p q \<equiv> (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 add:not) 

 (cases "not p= q", auto simp add:not)

 lemma iff_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (iff p q)"

   by (unfold iff_def,cases "p=q", auto)

 lemma iff_nb[simp]: "\<lbrakk>bound0 p ; bound0 q\<rbrakk> \<Longrightarrow> bound0 (iff p q)"

 using iff_def by (unfold iff_def,cases "p=q", auto)

 consts check_int:: "num \<Rightarrow> bool"

 recdef check_int "measure size"

   "check_int (C i) = True"

   "check_int (Floor t) = True"

   "check_int (Mul i t) = check_int t"

   "check_int (Add t s) = (check_int t \<and> check_int s)"

   "check_int (Neg t) = check_int t"

   "check_int (CF c t s) = check_int s"

   "check_int t = False"

 lemma check_int: "check_int t \<Longrightarrow> isint t bs"

 by (induct t, auto simp add: isint_add isint_Floor isint_Mul isint_neg isint_c isint_CF)

 lemma rdvd_left1_int: "real \<lfloor>t\<rfloor> = t \<Longrightarrow> 1 rdvd t"

   by (simp add: rdvd_def,rule_tac x="\<lfloor>t\<rfloor>" in exI) simp

 lemma rdvd_reduce: 

   assumes gd:"g dvd d" and gc:"g dvd c" and gp: "g > 0"

   shows "real (d::int) rdvd real (c::int)*t = (real (d div g) rdvd real (c div g)*t)"

 proof

   assume d: "real d rdvd real c * t"

   from d rdvd_def obtain k where k_def: "real c * t = real d* real (k::int)" by auto

   from gd dvd_def obtain kd where kd_def: "d = g * kd" by auto

   from gc dvd_def obtain kc where kc_def: "c = g * kc" by auto

   from k_def kd_def kc_def have "real g * real kc * t = real g * real kd * real k" by simp

   hence "real kc * t = real kd * real k" using gp by simp

   hence th:"real kd rdvd real kc * t" using rdvd_def by blast

   from kd_def gp have th':"kd = d div g" by simp

   from kc_def gp have "kc = c div g" by simp

   with th th' show "real (d div g) rdvd real (c div g) * t" by simp

 next

   assume d: "real (d div g) rdvd real (c div g) * t"

   from gp have gnz: "g \<noteq> 0" by simp

   thus "real d rdvd real c * t" using d rdvd_mult[OF gnz, where n="d div g" and x="real (c div g) * t"] real_of_int_div[OF gnz gd] real_of_int_div[OF gnz gc] by simp

 qed

 definition simpdvd :: "int \<Rightarrow> num \<Rightarrow> (int \<times> num)" where

   "simpdvd d t \<equiv> 

    (let g = numgcd t in 

       if g > 1 then (let g' = gcd d g in 

         if g' = 1 then (d, t) 

         else (d div g',reducecoeffh t g')) 

       else (d, t))"

 lemma simpdvd: 

   assumes tnz: "nozerocoeff t" and dnz: "d \<noteq> 0"

   shows "Ifm bs (Dvd (fst (simpdvd d t)) (snd (simpdvd d t))) = Ifm bs (Dvd d t)"

 proof-

   let ?g = "numgcd t"

   let ?g' = "gcd d ?g"

   {assume "\<not> ?g > 1" hence ?thesis by (simp add: Let_def simpdvd_def)}

   moreover

   {assume g1:"?g>1" hence g0: "?g > 0" by simp

     from g1 dnz have gp0: "?g' \<noteq> 0" by simp

     hence g'p: "?g' > 0" using gcd_ge_0_int[where x="d" and y="numgcd t"] by arith

     hence "?g'= 1 \<or> ?g' > 1" by arith

     moreover {assume "?g'=1" hence ?thesis by (simp add: Let_def simpdvd_def)}

     moreover {assume g'1:"?g'>1"

       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 d" by simp

       have gpdgp: "?g' dvd ?g'" by simp

       from reducecoeffh[OF dvdnumcoeff_trans[OF gpdg th1] g'p] 

       have th2:"real ?g' * ?t = Inum bs t" by simp

       from prems have "Ifm bs (Dvd (fst (simpdvd d t)) (snd(simpdvd d t))) = Ifm bs (Dvd (d div ?g') ?tt)"

         by (simp add: simpdvd_def Let_def)

       also have "\<dots> = (real d rdvd (Inum bs t))"

         using rdvd_reduce[OF gpdd gpdgp g'p, where t="?t", simplified zdiv_self[OF gp0]] 

           th2[symmetric] by simp

       finally have ?thesis by simp  }

     ultimately have ?thesis by blast

   }

   ultimately show ?thesis by blast

 qed

 consts simpfm :: "fm \<Rightarrow> fm"

 recdef simpfm "measure fmsize"

   "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 \<Rightarrow> if (v < 0) then T else F 

   | _ \<Rightarrow> Lt (reducecoeff a'))"

   "simpfm (Le a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<le> 0)  then T else F | _ \<Rightarrow> Le (reducecoeff a'))"

   "simpfm (Gt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v > 0)  then T else F | _ \<Rightarrow> Gt (reducecoeff a'))"

   "simpfm (Ge a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<ge> 0)  then T else F | _ \<Rightarrow> Ge (reducecoeff a'))"

   "simpfm (Eq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v = 0)  then T else F | _ \<Rightarrow> Eq (reducecoeff a'))"

   "simpfm (NEq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<noteq> 0)  then T else F | _ \<Rightarrow> NEq (reducecoeff a'))"

   "simpfm (Dvd i a) = (if i=0 then simpfm (Eq a)

              else if (abs i = 1) \<and> check_int a then T

              else let a' = simpnum a in case a' of C v \<Rightarrow> if (i dvd v)  then T else F | _ \<Rightarrow> (let (d,t) = simpdvd i a' in Dvd d t))"

   "simpfm (NDvd i a) = (if i=0 then simpfm (NEq a) 

              else if (abs i = 1) \<and> check_int a then F

              else let a' = simpnum a in case a' of C v \<Rightarrow> if (\<not>(i dvd v)) then T else F | _ \<Rightarrow> (let (d,t) = simpdvd i a' in NDvd d t))"

   "simpfm p = p"

 lemma simpfm[simp]: "Ifm bs (simpfm p) = Ifm bs p"

 proof(induct p rule: simpfm.induct)

   case (6 a) let ?sa = "simpnum a" have sa: "Inum bs ?sa = Inum bs a" by simp

   {fix v assume "?sa = C v" hence ?case using sa by simp }

   moreover {assume H:"\<not> (\<exists> v. ?sa = C v)"

     let ?g = "numgcd ?sa"

     let ?rsa = "reducecoeff ?sa"

     let ?r = "Inum bs ?rsa"

     have sa_nz: "nozerocoeff ?sa" by (rule simpnum_nz)

     {assume gz: "?g=0" from numgcd_nz[OF sa_nz gz] H have "False" by auto}

     with numgcd_pos[where t="?sa"] have "?g > 0" by (cases "?g=0", auto)

     hence gp: "real ?g > 0" by simp

     have "Inum bs ?sa = real ?g* ?r" by (simp add: reducecoeff)

     with sa have "Inum bs a < 0 = (real ?g * ?r < real ?g * 0)" by simp

     also have "\<dots> = (?r < 0)" using gp

       by (simp only: mult_less_cancel_left) simp

     finally have ?case using H by (cases "?sa" , simp_all add: Let_def)}

   ultimately show ?case by blast

 next

   case (7 a)  let ?sa = "simpnum a" have sa: "Inum bs ?sa = Inum bs a" by simp

   {fix v assume "?sa = C v" hence ?case using sa by simp }

   moreover {assume H:"\<not> (\<exists> v. ?sa = C v)"

     let ?g = "numgcd ?sa"

     let ?rsa = "reducecoeff ?sa"

     let ?r = "Inum bs ?rsa"

     have sa_nz: "nozerocoeff ?sa" by (rule simpnum_nz)

     {assume gz: "?g=0" from numgcd_nz[OF sa_nz gz] H have "False" by auto}

     with numgcd_pos[where t="?sa"] have "?g > 0" by (cases "?g=0", auto)

     hence gp: "real ?g > 0" by simp

     have "Inum bs ?sa = real ?g* ?r" by (simp add: reducecoeff)

     with sa have "Inum bs a \<le> 0 = (real ?g * ?r \<le> real ?g * 0)" by simp

     also have "\<dots> = (?r \<le> 0)" using gp

       by (simp only: mult_le_cancel_left) simp

     finally have ?case using H by (cases "?sa" , simp_all add: Let_def)}

   ultimately show ?case by blast

 next

   case (8 a)  let ?sa = "simpnum a" have sa: "Inum bs ?sa = Inum bs a" by simp

   {fix v assume "?sa = C v" hence ?case using sa by simp }

   moreover {assume H:"\<not> (\<exists> v. ?sa = C v)"

     let ?g = "numgcd ?sa"

     let ?rsa = "reducecoeff ?sa"

     let ?r = "Inum bs ?rsa"

     have sa_nz: "nozerocoeff ?sa" by (rule simpnum_nz)

     {assume gz: "?g=0" from numgcd_nz[OF sa_nz gz] H have "False" by auto}

     with numgcd_pos[where t="?sa"] have "?g > 0" by (cases "?g=0", auto)

     hence gp: "real ?g > 0" by simp

     have "Inum bs ?sa = real ?g* ?r" by (simp add: reducecoeff)

     with sa have "Inum bs a > 0 = (real ?g * ?r > real ?g * 0)" by simp

     also have "\<dots> = (?r > 0)" using gp

       by (simp only: mult_less_cancel_left) simp

     finally have ?case using H by (cases "?sa" , simp_all add: Let_def)}

   ultimately show ?case by blast

 next

   case (9 a)  let ?sa = "simpnum a" have sa: "Inum bs ?sa = Inum bs a" by simp

   {fix v assume "?sa = C v" hence ?case using sa by simp }

   moreover {assume H:"\<not> (\<exists> v. ?sa = C v)"

     let ?g = "numgcd ?sa"

     let ?rsa = "reducecoeff ?sa"

     let ?r = "Inum bs ?rsa"

     have sa_nz: "nozerocoeff ?sa" by (rule simpnum_nz)

     {assume gz: "?g=0" from numgcd_nz[OF sa_nz gz] H have "False" by auto}

     with numgcd_pos[where t="?sa"] have "?g > 0" by (cases "?g=0", auto)

     hence gp: "real ?g > 0" by simp

     have "Inum bs ?sa = real ?g* ?r" by (simp add: reducecoeff)

     with sa have "Inum bs a \<ge> 0 = (real ?g * ?r \<ge> real ?g * 0)" by simp

     also have "\<dots> = (?r \<ge> 0)" using gp

       by (simp only: mult_le_cancel_left) simp

     finally have ?case using H by (cases "?sa" , simp_all add: Let_def)}

   ultimately show ?case by blast

 next

   case (10 a)  let ?sa = "simpnum a" have sa: "Inum bs ?sa = Inum bs a" by simp

   {fix v assume "?sa = C v" hence ?case using sa by simp }

   moreover {assume H:"\<not> (\<exists> v. ?sa = C v)"

     let ?g = "numgcd ?sa"

     let ?rsa = "reducecoeff ?sa"

     let ?r = "Inum bs ?rsa"

     have sa_nz: "nozerocoeff ?sa" by (rule simpnum_nz)

     {assume gz: "?g=0" from numgcd_nz[OF sa_nz gz] H have "False" by auto}

     with numgcd_pos[where t="?sa"] have "?g > 0" by (cases "?g=0", auto)

     hence gp: "real ?g > 0" by simp

     have "Inum bs ?sa = real ?g* ?r" by (simp add: reducecoeff)

     with sa have "Inum bs a = 0 = (real ?g * ?r = 0)" by simp

     also have "\<dots> = (?r = 0)" using gp

       by (simp add: mult_eq_0_iff)

     finally have ?case using H by (cases "?sa" , simp_all add: Let_def)}

   ultimately show ?case by blast

 next

   case (11 a)  let ?sa = "simpnum a" have sa: "Inum bs ?sa = Inum bs a" by simp

   {fix v assume "?sa = C v" hence ?case using sa by simp }

   moreover {assume H:"\<not> (\<exists> v. ?sa = C v)"

     let ?g = "numgcd ?sa"

     let ?rsa = "reducecoeff ?sa"

     let ?r = "Inum bs ?rsa"

     have sa_nz: "nozerocoeff ?sa" by (rule simpnum_nz)

     {assume gz: "?g=0" from numgcd_nz[OF sa_nz gz] H have "False" by auto}

     with numgcd_pos[where t="?sa"] have "?g > 0" by (cases "?g=0", auto)

     hence gp: "real ?g > 0" by simp

     have "Inum bs ?sa = real ?g* ?r" by (simp add: reducecoeff)

     with sa have "Inum bs a \<noteq> 0 = (real ?g * ?r \<noteq> 0)" by simp

     also have "\<dots> = (?r \<noteq> 0)" using gp

       by (simp add: mult_eq_0_iff)

     finally have ?case using H by (cases "?sa" , simp_all add: Let_def)}

   ultimately show ?case by blast

 next

   case (12 i a)  let ?sa = "simpnum a"   have sa: "Inum bs ?sa = Inum bs a" by simp

   have "i=0 \<or> (abs i = 1 \<and> check_int a) \<or> (i\<noteq>0 \<and> ((abs i \<noteq> 1) \<or> (\<not> check_int a)))" by auto

   {assume "i=0" hence ?case using "12.hyps" by (simp add: rdvd_left_0_eq Let_def)}

   moreover 

   {assume ai1: "abs i = 1" and ai: "check_int a" 

     hence "i=1 \<or> i= - 1" by arith

     moreover {assume i1: "i = 1" 

       from rdvd_left1_int[OF check_int[OF ai, simplified isint_iff]] 

       have ?case using i1 ai by simp }

     moreover {assume i1: "i = - 1" 

       from rdvd_left1_int[OF check_int[OF ai, simplified isint_iff]] 

         rdvd_abs1[where d="- 1" and t="Inum bs a"]

       have ?case using i1 ai by simp }

     ultimately have ?case by blast}

   moreover   

   {assume inz: "i\<noteq>0" and cond: "(abs i \<noteq> 1) \<or> (\<not> check_int a)"

     {fix v assume "?sa = C v" hence ?case using sa[symmetric] inz cond

         by (cases "abs i = 1", auto simp add: int_rdvd_iff) }

     moreover {assume H:"\<not> (\<exists> v. ?sa = C v)" 

       hence th: "simpfm (Dvd i a) = Dvd (fst (simpdvd i ?sa)) (snd (simpdvd i ?sa))" using inz cond by (cases ?sa, auto simp add: Let_def split_def)

       from simpnum_nz have nz:"nozerocoeff ?sa" by simp

       from simpdvd [OF nz inz] th have ?case using sa by simp}

     ultimately have ?case by blast}

   ultimately show ?case by blast

 next

   case (13 i a)  let ?sa = "simpnum a"   have sa: "Inum bs ?sa = Inum bs a" by simp

   have "i=0 \<or> (abs i = 1 \<and> check_int a) \<or> (i\<noteq>0 \<and> ((abs i \<noteq> 1) \<or> (\<not> check_int a)))" by auto

   {assume "i=0" hence ?case using "13.hyps" by (simp add: rdvd_left_0_eq Let_def)}

   moreover 

   {assume ai1: "abs i = 1" and ai: "check_int a" 

     hence "i=1 \<or> i= - 1" by arith

     moreover {assume i1: "i = 1" 

       from rdvd_left1_int[OF check_int[OF ai, simplified isint_iff]] 

       have ?case using i1 ai by simp }

     moreover {assume i1: "i = - 1" 

       from rdvd_left1_int[OF check_int[OF ai, simplified isint_iff]] 

         rdvd_abs1[where d="- 1" and t="Inum bs a"]

       have ?case using i1 ai by simp }

     ultimately have ?case by blast}

   moreover   

   {assume inz: "i\<noteq>0" and cond: "(abs i \<noteq> 1) \<or> (\<not> check_int a)"

     {fix v assume "?sa = C v" hence ?case using sa[symmetric] inz cond

         by (cases "abs i = 1", auto simp add: int_rdvd_iff) }

     moreover {assume H:"\<not> (\<exists> v. ?sa = C v)" 

       hence th: "simpfm (NDvd i a) = NDvd (fst (simpdvd i ?sa)) (snd (simpdvd i ?sa))" using inz cond 

         by (cases ?sa, auto simp add: Let_def split_def)

       from simpnum_nz have nz:"nozerocoeff ?sa" by simp

       from simpdvd [OF nz inz] th have ?case using sa by simp}

     ultimately have ?case by blast}

   ultimately show ?case by blast

 qed (induct p rule: simpfm.induct, simp_all)

 lemma simpdvd_numbound0: "numbound0 t \<Longrightarrow> numbound0 (snd (simpdvd d t))"

   by (simp add: simpdvd_def Let_def split_def reducecoeffh_numbound0)

 lemma simpfm_bound0[simp]: "bound0 p \<Longrightarrow> bound0 (simpfm p)"

 proof(induct p rule: simpfm.induct)

   case (6 a) hence nb: "numbound0 a" by simp

   hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])

   thus ?case by (cases "simpnum a", auto simp add: Let_def reducecoeff_numbound0)

 next

   case (7 a) hence nb: "numbound0 a" by simp

   hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])

   thus ?case by (cases "simpnum a", auto simp add: Let_def reducecoeff_numbound0)

 next

   case (8 a) hence nb: "numbound0 a" by simp

   hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])

   thus ?case by (cases "simpnum a", auto simp add: Let_def reducecoeff_numbound0)

 next

   case (9 a) hence nb: "numbound0 a" by simp

   hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])

   thus ?case by (cases "simpnum a", auto simp add: Let_def reducecoeff_numbound0)

 next

   case (10 a) hence nb: "numbound0 a" by simp

   hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])

   thus ?case by (cases "simpnum a", auto simp add: Let_def reducecoeff_numbound0)

 next

   case (11 a) hence nb: "numbound0 a" by simp

   hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])

   thus ?case by (cases "simpnum a", auto simp add: Let_def reducecoeff_numbound0)

 next

   case (12 i a) hence nb: "numbound0 a" by simp

   hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])

   thus ?case by (cases "simpnum a", auto simp add: Let_def reducecoeff_numbound0 simpdvd_numbound0 split_def)

 next

   case (13 i a) hence nb: "numbound0 a" by simp

   hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])

   thus ?case by (cases "simpnum a", auto simp add: Let_def reducecoeff_numbound0 simpdvd_numbound0 split_def)

 qed(auto simp add: disj_def imp_def iff_def conj_def)

 lemma simpfm_qf[simp]: "qfree p \<Longrightarrow> qfree (simpfm p)"

 by (induct p rule: simpfm.induct, auto simp add: Let_def)

 (case_tac "simpnum a",auto simp add: split_def Let_def)+

   (* Generic quantifier elimination *)

 definition list_conj :: "fm list \<Rightarrow> fm" where

   "list_conj ps \<equiv> foldr conj ps T"

 lemma list_conj: "Ifm bs (list_conj ps) = (\<forall>p\<in> set ps. Ifm bs p)"

   by (induct ps, auto simp add: list_conj_def)

 lemma list_conj_qf: " \<forall>p\<in> set ps. qfree p \<Longrightarrow> qfree (list_conj ps)"

   by (induct ps, auto simp add: list_conj_def)

 lemma list_conj_nb: " \<forall>p\<in> set ps. bound0 p \<Longrightarrow> bound0 (list_conj ps)"

   by (induct ps, auto simp add: list_conj_def)

 definition CJNB :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm" where

   "CJNB f p \<equiv> (let cjs = conjuncts p ; (yes,no) = List.partition bound0 cjs

                    in conj (decr (list_conj yes)) (f (list_conj no)))"

 lemma CJNB_qe: 

   assumes qe: "\<forall> bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bs (qe p) = Ifm bs (E p))"

   shows "\<forall> bs p. qfree p \<longrightarrow> qfree (CJNB qe p) \<and> (Ifm bs ((CJNB qe p)) = Ifm bs (E p))"

 proof(clarify)

   fix bs p

   assume qfp: "qfree p"

   let ?cjs = "conjuncts p"

   let ?yes = "fst (List.partition bound0 ?cjs)"

   let ?no = "snd (List.partition bound0 ?cjs)"

   let ?cno = "list_conj ?no"

   let ?cyes = "list_conj ?yes"

   have part: "List.partition bound0 ?cjs = (?yes,?no)" by simp

   from partition_P[OF part] have "\<forall> q\<in> set ?yes. bound0 q" by blast 

   hence yes_nb: "bound0 ?cyes" by (simp add: list_conj_nb) 

   hence yes_qf: "qfree (decr ?cyes )" by (simp add: decr_qf)

   from conjuncts_qf[OF qfp] partition_set[OF part] 

   have " \<forall>q\<in> set ?no. qfree q" by auto

   hence no_qf: "qfree ?cno"by (simp add: list_conj_qf)

   with qe have cno_qf:"qfree (qe ?cno )" 

     and noE: "Ifm bs (qe ?cno) = Ifm bs (E ?cno)" by blast+

   from cno_qf yes_qf have qf: "qfree (CJNB qe p)" 

     by (simp add: CJNB_def Let_def conj_qf split_def)

   {fix bs

     from conjuncts have "Ifm bs p = (\<forall>q\<in> set ?cjs. Ifm bs q)" by blast

     also have "\<dots> = ((\<forall>q\<in> set ?yes. Ifm bs q) \<and> (\<forall>q\<in> set ?no. Ifm bs q))"

       using partition_set[OF part] by auto

     finally have "Ifm bs p = ((Ifm bs ?cyes) \<and> (Ifm bs ?cno))" using list_conj by simp}

   hence "Ifm bs (E p) = (\<exists>x. (Ifm (x#bs) ?cyes) \<and> (Ifm (x#bs) ?cno))" by simp

   also fix y have "\<dots> = (\<exists>x. (Ifm (y#bs) ?cyes) \<and> (Ifm (x#bs) ?cno))"

     using bound0_I[OF yes_nb, where bs="bs" and b'="y"] by blast

   also have "\<dots> = (Ifm bs (decr ?cyes) \<and> Ifm bs (E ?cno))"

     by (auto simp add: decr[OF yes_nb] simp del: partition_filter_conv)

   also have "\<dots> = (Ifm bs (conj (decr ?cyes) (qe ?cno)))"

     using qe[rule_format, OF no_qf] by auto

   finally have "Ifm bs (E p) = Ifm bs (CJNB qe p)" 

     by (simp add: Let_def CJNB_def split_def)

   with qf show "qfree (CJNB qe p) \<and> Ifm bs (CJNB qe p) = Ifm bs (E p)" by blast

 qed

 consts qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm"

 recdef qelim "measure fmsize"

   "qelim (E p) = (\<lambda> qe. DJ (CJNB qe) (qelim p qe))"

   "qelim (A p) = (\<lambda> qe. not (qe ((qelim (NOT p) qe))))"

   "qelim (NOT p) = (\<lambda> qe. not (qelim p qe))"

   "qelim (And p q) = (\<lambda> qe. conj (qelim p qe) (qelim q qe))" 

   "qelim (Or  p q) = (\<lambda> qe. disj (qelim p qe) (qelim q qe))" 

   "qelim (Imp p q) = (\<lambda> qe. disj (qelim (NOT p) qe) (qelim q qe))"

   "qelim (Iff p q) = (\<lambda> qe. iff (qelim p qe) (qelim q qe))"

   "qelim p = (\<lambda> y. simpfm p)"

 lemma qelim_ci:

   assumes qe_inv: "\<forall> bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bs (qe p) = Ifm bs (E p))"

   shows "\<And> bs. qfree (qelim p qe) \<and> (Ifm bs (qelim p qe) = Ifm bs p)"

 using qe_inv DJ_qe[OF CJNB_qe[OF qe_inv]] 

 by(induct p rule: qelim.induct) 

 (auto simp del: simpfm.simps)

 text {* The @{text "\<int>"} Part *}

 text{* Linearity for fm where Bound 0 ranges over @{text "\<int>"} *}

 consts

   zsplit0 :: "num \<Rightarrow> int \<times> num" (* splits the bounded from the unbounded part*)

 recdef zsplit0 "measure num_size"

   "zsplit0 (C c) = (0,C c)"

   "zsplit0 (Bound n) = (if n=0 then (1, C 0) else (0,Bound n))"

   "zsplit0 (CN n c a) = zsplit0 (Add (Mul c (Bound n)) a)"

   "zsplit0 (CF c a b) = zsplit0 (Add (Mul c (Floor a)) b)"

   "zsplit0 (Neg a) = (let (i',a') =  zsplit0 a in (-i', Neg a'))"

   "zsplit0 (Add a b) = (let (ia,a') =  zsplit0 a ; 

                             (ib,b') =  zsplit0 b 

                             in (ia+ib, Add a' b'))"

   "zsplit0 (Sub a b) = (let (ia,a') =  zsplit0 a ; 

                             (ib,b') =  zsplit0 b 

                             in (ia-ib, Sub a' b'))"

   "zsplit0 (Mul i a) = (let (i',a') =  zsplit0 a in (i*i', Mul i a'))"

   "zsplit0 (Floor a) = (let (i',a') =  zsplit0 a in (i',Floor a'))"

 (hints simp add: Let_def)

 lemma zsplit0_I:

   shows "\<And> n a. zsplit0 t = (n,a) \<Longrightarrow> (Inum ((real (x::int)) #bs) (CN 0 n a) = Inum (real x #bs) t) \<and> numbound0 a"

   (is "\<And> n a. ?S t = (n,a) \<Longrightarrow> (?I x (CN 0 n a) = ?I x t) \<and> ?N a")

 proof(induct t rule: zsplit0.induct)

   case (1 c n a) thus ?case by auto 

 next

   case (2 m n a) thus ?case by (cases "m=0") auto

 next

   case (3 n i a n a') thus ?case by auto

 next 

   case (4 c a b n a') thus ?case by auto

 next

   case (5 t n a)

   let ?nt = "fst (zsplit0 t)"

   let ?at = "snd (zsplit0 t)"

   have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Neg ?at \<and> n=-?nt" using prems 

     by (simp add: Let_def split_def)

   from abj prems  have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast

   from th2[simplified] th[simplified] show ?case by simp

 next

   case (6 s t n a)

   let ?ns = "fst (zsplit0 s)"

   let ?as = "snd (zsplit0 s)"

   let ?nt = "fst (zsplit0 t)"

   let ?at = "snd (zsplit0 t)"

   have abjs: "zsplit0 s = (?ns,?as)" by simp 

   moreover have abjt:  "zsplit0 t = (?nt,?at)" by simp 

   ultimately have th: "a=Add ?as ?at \<and> n=?ns + ?nt" using prems 

     by (simp add: Let_def split_def)

   from abjs[symmetric] have bluddy: "\<exists> x y. (x,y) = zsplit0 s" by blast

   from prems have "(\<exists> x y. (x,y) = zsplit0 s) \<longrightarrow> (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (real x # bs) (CN 0 xa xb) = Inum (real x # bs) t \<and> numbound0 xb)" by simp

   with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast

   from abjs prems  have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast

   from th3[simplified] th2[simplified] th[simplified] show ?case 

     by (simp add: left_distrib)

 next

   case (7 s t n a)

   let ?ns = "fst (zsplit0 s)"

   let ?as = "snd (zsplit0 s)"

   let ?nt = "fst (zsplit0 t)"

   let ?at = "snd (zsplit0 t)"

   have abjs: "zsplit0 s = (?ns,?as)" by simp 

   moreover have abjt:  "zsplit0 t = (?nt,?at)" by simp 

   ultimately have th: "a=Sub ?as ?at \<and> n=?ns - ?nt" using prems 

     by (simp add: Let_def split_def)

   from abjs[symmetric] have bluddy: "\<exists> x y. (x,y) = zsplit0 s" by blast

   from prems have "(\<exists> x y. (x,y) = zsplit0 s) \<longrightarrow> (\<forall>xa xb. zsplit0 t = (xa, xb) \<longrightarrow> Inum (real x # bs) (CN 0 xa xb) = Inum (real x # bs) t \<and> numbound0 xb)" by simp

   with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast

   from abjs prems  have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) \<and> ?N ?as" by blast

   from th3[simplified] th2[simplified] th[simplified] show ?case 

     by (simp add: left_diff_distrib)

 next

   case (8 i t n a)

   let ?nt = "fst (zsplit0 t)"

   let ?at = "snd (zsplit0 t)"

   have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a=Mul i ?at \<and> n=i*?nt" using prems 

     by (simp add: Let_def split_def)

   from abj prems  have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast

   hence " ?I x (Mul i t) = (real i) * ?I x (CN 0 ?nt ?at)" by simp

   also have "\<dots> = ?I x (CN 0 (i*?nt) (Mul i ?at))" by (simp add: right_distrib)

   finally show ?case using th th2 by simp

 next

   case (9 t n a)

   let ?nt = "fst (zsplit0 t)"

   let ?at = "snd (zsplit0 t)"

   have abj: "zsplit0 t = (?nt,?at)" by simp hence th: "a= Floor ?at \<and> n=?nt" using prems 

     by (simp add: Let_def split_def)

   from abj prems  have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \<and> ?N ?at" by blast

   hence na: "?N a" using th by simp

   have th': "(real ?nt)*(real x) = real (?nt * x)" by simp

   have "?I x (Floor t) = ?I x (Floor (CN 0 ?nt ?at))" using th2 by simp

   also have "\<dots> = real (floor ((real ?nt)* real(x) + ?I x ?at))" by simp

   also have "\<dots> = real (floor (?I x ?at + real (?nt* x)))" by (simp add: add_ac)

   also have "\<dots> = real (floor (?I x ?at) + (?nt* x))" 

     using floor_add[where x="?I x ?at" and a="?nt* x"] by simp 

   also have "\<dots> = real (?nt)*(real x) + real (floor (?I x ?at))" by (simp add: add_ac)

   finally have "?I x (Floor t) = ?I x (CN 0 n a)" using th by simp

   with na show ?case by simp

 qed

 consts

   iszlfm :: "fm \<Rightarrow> real list \<Rightarrow> bool"   (* Linearity test for fm *)

   zlfm :: "fm \<Rightarrow> fm"       (* Linearity transformation for fm *)

 recdef iszlfm "measure size"

   "iszlfm (And p q) = (\<lambda> bs. iszlfm p bs \<and> iszlfm q bs)" 

   "iszlfm (Or p q) = (\<lambda> bs. iszlfm p bs \<and> iszlfm q bs)" 

   "iszlfm (Eq  (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"

   "iszlfm (NEq (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"

   "iszlfm (Lt  (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"

   "iszlfm (Le  (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"

   "iszlfm (Gt  (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"

   "iszlfm (Ge  (CN 0 c e)) = (\<lambda> bs. c>0 \<and> numbound0 e \<and> isint e bs)"

   "iszlfm (Dvd i (CN 0 c e)) = 

                  (\<lambda> bs. c>0 \<and> i>0 \<and> numbound0 e \<and> isint e bs)"

   "iszlfm (NDvd i (CN 0 c e))= 

                  (\<lambda> bs. c>0 \<and> i>0 \<and> numbound0 e \<and> isint e bs)"

   "iszlfm p = (\<lambda> bs. isatom p \<and> (bound0 p))"

 lemma zlin_qfree: "iszlfm p bs \<Longrightarrow> qfree p"

   by (induct p rule: iszlfm.induct) auto

 lemma iszlfm_gen:

   assumes lp: "iszlfm p (x#bs)"

   shows "\<forall> y. iszlfm p (y#bs)"

 proof

   fix y

   show "iszlfm p (y#bs)"

     using lp

   by(induct p rule: iszlfm.induct, simp_all add: numbound0_gen[rule_format, where x="x" and y="y"])

 qed

 lemma conj_zl[simp]: "iszlfm p bs \<Longrightarrow> iszlfm q bs \<Longrightarrow> iszlfm (conj p q) bs"

   using conj_def by (cases p,auto)

 lemma disj_zl[simp]: "iszlfm p bs \<Longrightarrow> iszlfm q bs \<Longrightarrow> iszlfm (disj p q) bs"

   using disj_def by (cases p,auto)

 lemma not_zl[simp]: "iszlfm p bs \<Longrightarrow> iszlfm (not p) bs"

   by (induct p rule:iszlfm.induct ,auto)

 recdef zlfm "measure fmsize"

   "zlfm (And p q) = conj (zlfm p) (zlfm q)"

   "zlfm (Or p q) = disj (zlfm p) (zlfm q)"

   "zlfm (Imp p q) = disj (zlfm (NOT p)) (zlfm q)"

   "zlfm (Iff p q) = disj (conj (zlfm p) (zlfm q)) (conj (zlfm (NOT p)) (zlfm (NOT q)))"

   "zlfm (Lt a) = (let (c,r) = zsplit0 a in 

      if c=0 then Lt r else 

      if c>0 then Or (Lt (CN 0 c (Neg (Floor (Neg r))))) (And (Eq (CN 0 c (Neg (Floor (Neg r))))) (Lt (Add (Floor (Neg r)) r))) 

      else Or (Gt (CN 0 (-c) (Floor(Neg r)))) (And (Eq(CN 0 (-c) (Floor(Neg r)))) (Lt (Add (Floor (Neg r)) r))))"

   "zlfm (Le a) = (let (c,r) = zsplit0 a in 

      if c=0 then Le r else 

      if c>0 then Or (Le (CN 0 c (Neg (Floor (Neg r))))) (And (Eq (CN 0 c (Neg (Floor (Neg r))))) (Lt (Add (Floor (Neg r)) r))) 

      else Or (Ge (CN 0 (-c) (Floor(Neg r)))) (And (Eq(CN 0 (-c) (Floor(Neg r)))) (Lt (Add (Floor (Neg r)) r))))"

   "zlfm (Gt a) = (let (c,r) = zsplit0 a in 

      if c=0 then Gt r else 

      if c>0 then Or (Gt (CN 0 c (Floor r))) (And (Eq (CN 0 c (Floor r))) (Lt (Sub (Floor r) r))) 

      else Or (Lt (CN 0 (-c) (Neg (Floor r)))) (And (Eq(CN 0 (-c) (Neg (Floor r)))) (Lt (Sub (Floor r) r))))"

   "zlfm (Ge a) = (let (c,r) = zsplit0 a in 

      if c=0 then Ge r else 

      if c>0 then Or (Ge (CN 0 c (Floor r))) (And (Eq (CN 0 c (Floor r))) (Lt (Sub (Floor r) r))) 

      else Or (Le (CN 0 (-c) (Neg (Floor r)))) (And (Eq(CN 0 (-c) (Neg (Floor r)))) (Lt (Sub (Floor r) r))))"

   "zlfm (Eq a) = (let (c,r) = zsplit0 a in 

               if c=0 then Eq r else 

       if c>0 then (And (Eq (CN 0 c (Neg (Floor (Neg r))))) (Eq (Add (Floor (Neg r)) r)))

       else (And (Eq (CN 0 (-c) (Floor (Neg r)))) (Eq (Add (Floor (Neg r)) r))))"

   "zlfm (NEq a) = (let (c,r) = zsplit0 a in 

               if c=0 then NEq r else 

       if c>0 then (Or (NEq (CN 0 c (Neg (Floor (Neg r))))) (NEq (Add (Floor (Neg r)) r)))

       else (Or (NEq (CN 0 (-c) (Floor (Neg r)))) (NEq (Add (Floor (Neg r)) r))))"

   "zlfm (Dvd i a) = (if i=0 then zlfm (Eq a) 

   else (let (c,r) = zsplit0 a in 

               if c=0 then Dvd (abs i) r else 

       if c>0 then And (Eq (Sub (Floor r) r)) (Dvd (abs i) (CN 0 c (Floor r))) 

       else And (Eq (Sub (Floor r) r)) (Dvd (abs i) (CN 0 (-c) (Neg (Floor r))))))"

   "zlfm (NDvd i a) = (if i=0 then zlfm (NEq a) 

   else (let (c,r) = zsplit0 a in 

               if c=0 then NDvd (abs i) r else 

       if c>0 then Or (NEq (Sub (Floor r) r)) (NDvd (abs i) (CN 0 c (Floor r))) 

       else Or (NEq (Sub (Floor r) r)) (NDvd (abs i) (CN 0 (-c) (Neg (Floor r))))))"

   "zlfm (NOT (And p q)) = disj (zlfm (NOT p)) (zlfm (NOT q))"

   "zlfm (NOT (Or p q)) = conj (zlfm (NOT p)) (zlfm (NOT q))"

   "zlfm (NOT (Imp p q)) = conj (zlfm p) (zlfm (NOT q))"

   "zlfm (NOT (Iff p q)) = disj (conj(zlfm p) (zlfm(NOT q))) (conj (zlfm(NOT p)) (zlfm q))"

   "zlfm (NOT (NOT p)) = zlfm p"

   "zlfm (NOT T) = F"

   "zlfm (NOT F) = T"

   "zlfm (NOT (Lt a)) = zlfm (Ge a)"

   "zlfm (NOT (Le a)) = zlfm (Gt a)"

   "zlfm (NOT (Gt a)) = zlfm (Le a)"

   "zlfm (NOT (Ge a)) = zlfm (Lt a)"

   "zlfm (NOT (Eq a)) = zlfm (NEq a)"

   "zlfm (NOT (NEq a)) = zlfm (Eq a)"

   "zlfm (NOT (Dvd i a)) = zlfm (NDvd i a)"

   "zlfm (NOT (NDvd i a)) = zlfm (Dvd i a)"

   "zlfm p = p" (hints simp add: fmsize_pos)

 lemma split_int_less_real: 

   "(real (a::int) < b) = (a < floor b \<or> (a = floor b \<and> real (floor b) < b))"

 proof( auto)

   assume alb: "real a < b" and agb: "\<not> a < floor b"

   from agb have "floor b \<le> a" by simp hence th: "b < real a + 1" by (simp only: floor_le_eq)

   from floor_eq[OF alb th] show "a= floor b" by simp 

 next

   assume alb: "a < floor b"

   hence "real a < real (floor b)" by simp

   moreover have "real (floor b) \<le> b" by simp ultimately show  "real a < b" by arith 

 qed

 lemma split_int_less_real': 

   "(real (a::int) + b < 0) = (real a - real (floor(-b)) < 0 \<or> (real a - real (floor (-b)) = 0 \<and> real (floor (-b)) + b < 0))"

 proof- 

   have "(real a + b <0) = (real a < -b)" by arith

   with split_int_less_real[where a="a" and b="-b"] show ?thesis by arith  

 qed

 lemma split_int_gt_real': 

   "(real (a::int) + b > 0) = (real a + real (floor b) > 0 \<or> (real a + real (floor b) = 0 \<and> real (floor b) - b < 0))"

 proof- 

   have th: "(real a + b >0) = (real (-a) + (-b)< 0)" by arith

   show ?thesis using myless[rule_format, where b="real (floor b)"] 

     by (simp only:th split_int_less_real'[where a="-a" and b="-b"]) 

     (simp add: algebra_simps diff_def[symmetric],arith)

 qed

 lemma split_int_le_real: 

   "(real (a::int) \<le> b) = (a \<le> floor b \<or> (a = floor b \<and> real (floor b) < b))"

 proof( auto)

   assume alb: "real a \<le> b" and agb: "\<not> a \<le> floor b"

   from alb have "floor (real a) \<le> floor b " by (simp only: floor_mono) 

   hence "a \<le> floor b" by simp with agb show "False" by simp

 next

   assume alb: "a \<le> floor b"

   hence "real a \<le> real (floor b)" by (simp only: floor_mono)

   also have "\<dots>\<le> b" by simp  finally show  "real a \<le> b" . 

 qed

 lemma split_int_le_real': 

   "(real (a::int) + b \<le> 0) = (real a - real (floor(-b)) \<le> 0 \<or> (real a - real (floor (-b)) = 0 \<and> real (floor (-b)) + b < 0))"

 proof- 

   have "(real a + b \<le>0) = (real a \<le> -b)" by arith

   with split_int_le_real[where a="a" and b="-b"] show ?thesis by arith  

 qed

 lemma split_int_ge_real': 

   "(real (a::int) + b \<ge> 0) = (real a + real (floor b) \<ge> 0 \<or> (real a + real (floor b) = 0 \<and> real (floor b) - b < 0))"

 proof- 

   have th: "(real a + b \<ge>0) = (real (-a) + (-b) \<le> 0)" by arith

   show ?thesis by (simp only: th split_int_le_real'[where a="-a" and b="-b"])

     (simp add: algebra_simps diff_def[symmetric],arith)

 qed

 lemma split_int_eq_real: "(real (a::int) = b) = ( a = floor b \<and> b = real (floor b))" (is "?l = ?r")

 by auto

 lemma split_int_eq_real': "(real (a::int) + b = 0) = ( a - floor (-b) = 0 \<and> real (floor (-b)) + b = 0)" (is "?l = ?r")

 proof-

   have "?l = (real a = -b)" by arith

   with split_int_eq_real[where a="a" and b="-b"] show ?thesis by simp arith

 qed

 lemma zlfm_I:

   assumes qfp: "qfree p"

   shows "(Ifm (real i #bs) (zlfm p) = Ifm (real i# bs) p) \<and> iszlfm (zlfm p) (real (i::int) #bs)"

   (is "(?I (?l p) = ?I p) \<and> ?L (?l p)")

 using qfp

 proof(induct p rule: zlfm.induct)

   case (5 a) 

   let ?c = "fst (zsplit0 a)"

   let ?r = "snd (zsplit0 a)"

   have spl: "zsplit0 a = (?c,?r)" by simp

   from zsplit0_I[OF spl, where x="i" and bs="bs"] 

   have Ia:"Inum (real i # bs) a = Inum (real i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 

   let ?N = "\<lambda> t. Inum (real i#bs) t"

   have "?c = 0 \<or> (?c >0 \<and> ?c\<noteq>0) \<or> (?c<0 \<and> ?c\<noteq>0)" by arith

   moreover

   {assume "?c=0" hence ?case using zsplit0_I[OF spl, where x="i" and bs="bs"] 

       by (cases "?r", simp_all add: Let_def split_def,case_tac "nat", simp_all)}

   moreover

   {assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Lt a))" 

       by (simp add: nb Let_def split_def isint_Floor isint_neg)

     have "?I (Lt a) = (real (?c * i) + (?N ?r) < 0)" using Ia by (simp add: Let_def split_def)

     also have "\<dots> = (?I (?l (Lt a)))" apply (simp only: split_int_less_real'[where a="?c*i" and b="?N ?r"]) by (simp add: Ia cp cnz Let_def split_def diff_def)

     finally have ?case using l by simp}

   moreover

   {assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Lt a))" 

       by (simp add: nb Let_def split_def isint_Floor isint_neg)

     have "?I (Lt a) = (real (?c * i) + (?N ?r) < 0)" using Ia by (simp add: Let_def split_def)

     also from cn cnz have "\<dots> = (?I (?l (Lt a)))" by (simp only: split_int_less_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def diff_def[symmetric] add_ac, arith)

     finally have ?case using l by simp}

   ultimately show ?case by blast

 next

   case (6 a)

   let ?c = "fst (zsplit0 a)"

   let ?r = "snd (zsplit0 a)"

   have spl: "zsplit0 a = (?c,?r)" by simp

   from zsplit0_I[OF spl, where x="i" and bs="bs"] 

   have Ia:"Inum (real i # bs) a = Inum (real i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 

   let ?N = "\<lambda> t. Inum (real i#bs) t"

   have "?c = 0 \<or> (?c >0 \<and> ?c\<noteq>0) \<or> (?c<0 \<and> ?c\<noteq>0)" by arith

   moreover

   {assume "?c=0" hence ?case using zsplit0_I[OF spl, where x="i" and bs="bs"] 

       by (cases "?r", simp_all add: Let_def split_def, case_tac "nat",simp_all)}

   moreover

   {assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Le a))" 

       by (simp add: nb Let_def split_def isint_Floor isint_neg)

     have "?I (Le a) = (real (?c * i) + (?N ?r) \<le> 0)" using Ia by (simp add: Let_def split_def)

     also have "\<dots> = (?I (?l (Le a)))" by (simp only: split_int_le_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia cp cnz Let_def split_def diff_def)

     finally have ?case using l by simp}

   moreover

   {assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Le a))" 

       by (simp add: nb Let_def split_def isint_Floor isint_neg)

     have "?I (Le a) = (real (?c * i) + (?N ?r) \<le> 0)" using Ia by (simp add: Let_def split_def)

     also from cn cnz have "\<dots> = (?I (?l (Le a)))" by (simp only: split_int_le_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def diff_def[symmetric] add_ac ,arith)

     finally have ?case using l by simp}

   ultimately show ?case by blast

 next

   case (7 a) 

   let ?c = "fst (zsplit0 a)"

   let ?r = "snd (zsplit0 a)"

   have spl: "zsplit0 a = (?c,?r)" by simp

   from zsplit0_I[OF spl, where x="i" and bs="bs"] 

   have Ia:"Inum (real i # bs) a = Inum (real i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 

   let ?N = "\<lambda> t. Inum (real i#bs) t"

   have "?c = 0 \<or> (?c >0 \<and> ?c\<noteq>0) \<or> (?c<0 \<and> ?c\<noteq>0)" by arith

   moreover

   {assume "?c=0" hence ?case using zsplit0_I[OF spl, where x="i" and bs="bs"] 

       by (cases "?r", simp_all add: Let_def split_def, case_tac "nat", simp_all)}

   moreover

   {assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Gt a))" 

       by (simp add: nb Let_def split_def isint_Floor isint_neg)

     have "?I (Gt a) = (real (?c * i) + (?N ?r) > 0)" using Ia by (simp add: Let_def split_def)

     also have "\<dots> = (?I (?l (Gt a)))" by (simp only: split_int_gt_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia cp cnz Let_def split_def diff_def)

     finally have ?case using l by simp}

   moreover

   {assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Gt a))" 

       by (simp add: nb Let_def split_def isint_Floor isint_neg)

     have "?I (Gt a) = (real (?c * i) + (?N ?r) > 0)" using Ia by (simp add: Let_def split_def)

     also from cn cnz have "\<dots> = (?I (?l (Gt a)))" by (simp only: split_int_gt_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def diff_def[symmetric] add_ac, arith)

     finally have ?case using l by simp}

   ultimately show ?case by blast

 next

   case (8 a)

    let ?c = "fst (zsplit0 a)"

   let ?r = "snd (zsplit0 a)"

   have spl: "zsplit0 a = (?c,?r)" by simp

   from zsplit0_I[OF spl, where x="i" and bs="bs"] 

   have Ia:"Inum (real i # bs) a = Inum (real i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 

   let ?N = "\<lambda> t. Inum (real i#bs) t"

   have "?c = 0 \<or> (?c >0 \<and> ?c\<noteq>0) \<or> (?c<0 \<and> ?c\<noteq>0)" by arith

   moreover

   {assume "?c=0" hence ?case using zsplit0_I[OF spl, where x="i" and bs="bs"] 

       by (cases "?r", simp_all add: Let_def split_def, case_tac "nat", simp_all)}

   moreover

   {assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Ge a))" 

       by (simp add: nb Let_def split_def isint_Floor isint_neg)

     have "?I (Ge a) = (real (?c * i) + (?N ?r) \<ge> 0)" using Ia by (simp add: Let_def split_def)

     also have "\<dots> = (?I (?l (Ge a)))" by (simp only: split_int_ge_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia cp cnz Let_def split_def diff_def)

     finally have ?case using l by simp}

   moreover

   {assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Ge a))" 

       by (simp add: nb Let_def split_def isint_Floor isint_neg)

     have "?I (Ge a) = (real (?c * i) + (?N ?r) \<ge> 0)" using Ia by (simp add: Let_def split_def)

     also from cn cnz have "\<dots> = (?I (?l (Ge a)))" by (simp only: split_int_ge_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def diff_def[symmetric] add_ac, arith)

     finally have ?case using l by simp}

   ultimately show ?case by blast

 next

   case (9 a)

   let ?c = "fst (zsplit0 a)"

   let ?r = "snd (zsplit0 a)"

   have spl: "zsplit0 a = (?c,?r)" by simp

   from zsplit0_I[OF spl, where x="i" and bs="bs"] 

   have Ia:"Inum (real i # bs) a = Inum (real i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 

   let ?N = "\<lambda> t. Inum (real i#bs) t"

   have "?c = 0 \<or> (?c >0 \<and> ?c\<noteq>0) \<or> (?c<0 \<and> ?c\<noteq>0)" by arith

   moreover

   {assume "?c=0" hence ?case using zsplit0_I[OF spl, where x="i" and bs="bs"] 

       by (cases "?r", simp_all add: Let_def split_def, case_tac "nat", simp_all)}

   moreover

   {assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Eq a))" 

       by (simp add: nb Let_def split_def isint_Floor isint_neg)

     have "?I (Eq a) = (real (?c * i) + (?N ?r) = 0)" using Ia by (simp add: Let_def split_def)

     also have "\<dots> = (?I (?l (Eq a)))" using cp cnz  by (simp only: split_int_eq_real'[where a="?c*i" and b="?N ?r"]) (simp add: Let_def split_def Ia real_of_int_mult[symmetric] del: real_of_int_mult)

     finally have ?case using l by simp}

   moreover

   {assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Eq a))" 

       by (simp add: nb Let_def split_def isint_Floor isint_neg)

     have "?I (Eq a) = (real (?c * i) + (?N ?r) = 0)" using Ia by (simp add: Let_def split_def)

     also from cn cnz have "\<dots> = (?I (?l (Eq a)))" by (simp only: split_int_eq_real'[where a="?c*i" and b="?N ?r"]) (simp add: Let_def split_def Ia real_of_int_mult[symmetric] del: real_of_int_mult,arith)

     finally have ?case using l by simp}

   ultimately show ?case by blast

 next

   case (10 a)

   let ?c = "fst (zsplit0 a)"

   let ?r = "snd (zsplit0 a)"

   have spl: "zsplit0 a = (?c,?r)" by simp

   from zsplit0_I[OF spl, where x="i" and bs="bs"] 

   have Ia:"Inum (real i # bs) a = Inum (real i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 

   let ?N = "\<lambda> t. Inum (real i#bs) t"

   have "?c = 0 \<or> (?c >0 \<and> ?c\<noteq>0) \<or> (?c<0 \<and> ?c\<noteq>0)" by arith

   moreover

   {assume "?c=0" hence ?case using zsplit0_I[OF spl, where x="i" and bs="bs"] 

       by (cases "?r", simp_all add: Let_def split_def, case_tac "nat", simp_all)}

   moreover

   {assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (NEq a))" 

       by (simp add: nb Let_def split_def isint_Floor isint_neg)

     have "?I (NEq a) = (real (?c * i) + (?N ?r) \<noteq> 0)" using Ia by (simp add: Let_def split_def)

     also have "\<dots> = (?I (?l (NEq a)))" using cp cnz  by (simp only: split_int_eq_real'[where a="?c*i" and b="?N ?r"]) (simp add: Let_def split_def Ia real_of_int_mult[symmetric] del: real_of_int_mult)

     finally have ?case using l by simp}

   moreover

   {assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (NEq a))" 

       by (simp add: nb Let_def split_def isint_Floor isint_neg)

     have "?I (NEq a) = (real (?c * i) + (?N ?r) \<noteq> 0)" using Ia by (simp add: Let_def split_def)

     also from cn cnz have "\<dots> = (?I (?l (NEq a)))" by (simp only: split_int_eq_real'[where a="?c*i" and b="?N ?r"]) (simp add: Let_def split_def Ia real_of_int_mult[symmetric] del: real_of_int_mult,arith)

     finally have ?case using l by simp}

   ultimately show ?case by blast

 next

   case (11 j a)

   let ?c = "fst (zsplit0 a)"

   let ?r = "snd (zsplit0 a)"

   have spl: "zsplit0 a = (?c,?r)" by simp

   from zsplit0_I[OF spl, where x="i" and bs="bs"] 

   have Ia:"Inum (real i # bs) a = Inum (real i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 

   let ?N = "\<lambda> t. Inum (real i#bs) t"

   have "j=0 \<or> (j\<noteq>0 \<and> ?c = 0) \<or> (j\<noteq>0 \<and> ?c >0 \<and> ?c\<noteq>0) \<or> (j\<noteq> 0 \<and> ?c<0 \<and> ?c\<noteq>0)" by arith

   moreover

   {assume "j=0" hence z: "zlfm (Dvd j a) = (zlfm (Eq a))" by (simp add: Let_def) 

     hence ?case using prems by (simp del: zlfm.simps add: rdvd_left_0_eq)}

   moreover

   {assume "?c=0" and "j\<noteq>0" hence ?case 

       using zsplit0_I[OF spl, where x="i" and bs="bs"] rdvd_abs1[where d="j"]

       by (cases "?r", simp_all add: Let_def split_def, case_tac "nat", simp_all)}

   moreover

   {assume cp: "?c > 0" and cnz: "?c\<noteq>0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))" 

       by (simp add: nb Let_def split_def isint_Floor isint_neg)

     have "?I (Dvd j a) = (real j rdvd (real (?c * i) + (?N ?r)))" 

       using Ia by (simp add: Let_def split_def)

     also have "\<dots> = (real (abs j) rdvd real (?c*i) + (?N ?r))" 

       by (simp only: rdvd_abs1[where d="j" and t="real (?c*i) + ?N ?r", symmetric]) simp

     also have "\<dots> = ((abs j) dvd (floor ((?N ?r) + real (?c*i))) \<and> 

        (real (floor ((?N ?r) + real (?c*i))) = (real (?c*i) + (?N ?r))))" 

       by(simp only: int_rdvd_real[where i="abs j" and x="real (?c*i) + (?N ?r)"]) (simp only: add_ac)

     also have "\<dots> = (?I (?l (Dvd j a)))" using cp cnz jnz  

       by (simp add: Let_def split_def int_rdvd_iff[symmetric]  

         del: real_of_int_mult) (auto simp add: add_ac)

     finally have ?case using l jnz  by simp }

   moreover

   {assume cn: "?c < 0" and cnz: "?c\<noteq>0" and jnz: "j\<noteq>0" hence l: "?L (?l (Dvd j a))" 

       by (simp add: nb Let_def split_def isint_Floor isint_neg)

     have "?I (Dvd j a) = (real j rdvd (real (?c * i) + (?N ?r)))" 

       using Ia by (simp add: Let_def split_def)

     also have "\<dots> = (real (abs j) rdvd real (?c*i) + (?N ?r))" 

       by (simp only: rdvd_abs1[where d="j" and t="real (?c*i) + ?N ?r", symmetric]) simp

     also have "\<dots> = ((abs j) dvd (floor ((?N ?r) + real (?c*i))) \<and> 

        (real (floor ((?N ?r) + real (?c*i))) = (real (?c*i) + (?N ?r))))" 

       by(simp only: int_rdvd_real[where i="abs j" and x="real (?c*i) + (?N ?r)"]) (simp only: add_ac)

     also have "\<dots> = (?I (?l (Dvd j a)))" using cn cnz jnz

       using rdvd_minus [where d="abs j" and t="real (?c*i + floor (?N ?r))", simplified, symmetric]

       by (simp add: Let_def split_def int_rdvd_iff[symmetric]  

         del: real_of_int_mult) (auto simp add: add_ac)

     finally have ?case using l jnz by blast }

   ultimately show ?case by blast

 next

   case (12 j a)

   let ?c = "fst (zsplit0 a)"

   let ?r = "snd (zsplit0 a)"

   have spl: "zsplit0 a = (?c,?r)" by simp

   from zsplit0_I[OF spl, where x="i" and bs="bs"] 

   have Ia:"Inum (real i # bs) a = Inum (real i #bs) (CN 0 ?c ?r)" and nb: "numbound0 ?r" by auto 

   let ?N = "\<lambda> t. Inum (real i#bs) t"

   have "j=0 \<or> (j\<noteq>0 \<and> ?c = 0) \<or> (j\<noteq>0 \<and> ?c >0 \<and> ?c\<noteq>0) \<or> (j\<noteq> 0 \<and> ?c<0 \<and> ?c\<noteq>0)" by arith

   moreover

   {assume "j=0" hence z: "zlfm (NDvd j a) = (zlfm (NEq a))" by (simp add: Let_def) 

     hence ?case using prems by (simp del: zlfm.simps add: rdvd_left_0_eq)}

   moreover

   {assume "?c=0" and "j\<noteq>0" hence ?case 

       using zsplit0_I[OF spl, where x="i" and bs="bs"] rdvd_abs1[where d="j"]

       by (cases "?r", simp_all add: Let_def split_def, case_tac "nat", simp_all)}

   moreover

   {assume cp: "?c > 0" and cnz: "?c\<noteq>0" and jnz: "j\<noteq>0" hence l: "?L (?l (NDvd j a))" 

       by (simp add: nb Let_def split_def isint_Floor isint_neg)

     have "?I (NDvd j a) = (\<not> (real j rdvd (real (?c * i) + (?N ?r))))" 

       using Ia by (simp add: Let_def split_def)

     also have "\<dots> = (\<not> (real (abs j) rdvd real (?c*i) + (?N ?r)))" 

       by (simp only: rdvd_abs1[where d="j" and t="real (?c*i) + ?N ?r", symmetric]) simp

     also have "\<dots> = (\<not> ((abs j) dvd (floor ((?N ?r) + real (?c*i))) \<and> 

        (real (floor ((?N ?r) + real (?c*i))) = (real (?c*i) + (?N ?r)))))" 

       by(simp only: int_rdvd_real[where i="abs j" and x="real (?c*i) + (?N ?r)"]) (simp only: add_ac)

     also have "\<dots> = (?I (?l (NDvd j a)))" using cp cnz jnz  

       by (simp add: Let_def split_def int_rdvd_iff[symmetric]  

         del: real_of_int_mult) (auto simp add: add_ac)

     finally have ?case using l jnz  by simp }

   moreover

   {assume cn: "?c < 0" and cnz: "?c\<noteq>0" and jnz: "j\<noteq>0" hence l: "?L (?l (NDvd j a))" 

       by (simp add: nb Let_def split_def isint_Floor isint_neg)

     have "?I (NDvd j a) = (\<not> (real j rdvd (real (?c * i) + (?N ?r))))" 

       using Ia by (simp add: Let_def split_def)

     also have "\<dots> = (\<not> (real (abs j) rdvd real (?c*i) + (?N ?r)))" 

       by (simp only: rdvd_abs1[where d="j" and t="real (?c*i) + ?N ?r", symmetric]) simp

     also have "\<dots> = (\<not> ((abs j) dvd (floor ((?N ?r) + real (?c*i))) \<and> 

        (real (floor ((?N ?r) + real (?c*i))) = (real (?c*i) + (?N ?r)))))" 

       by(simp only: int_rdvd_real[where i="abs j" and x="real (?c*i) + (?N ?r)"]) (simp only: add_ac)

     also have "\<dots> = (?I (?l (NDvd j a)))" using cn cnz jnz

       using rdvd_minus [where d="abs j" and t="real (?c*i + floor (?N ?r))", simplified, symmetric]

       by (simp add: Let_def split_def int_rdvd_iff[symmetric]  

         del: real_of_int_mult) (auto simp add: add_ac)

     finally have ?case using l jnz by blast }

   ultimately show ?case by blast

 qed auto

 text{* plusinf : Virtual substitution of @{text "+\<infinity>"}

        minusinf: Virtual substitution of @{text "-\<infinity>"}

        @{text "\<delta>"} Compute lcm @{text "d| Dvd d  c*x+t \<in> p"}

        @{text "d\<delta>"} checks if a given l divides all the ds above*}

 consts 

   plusinf:: "fm \<Rightarrow> fm" 

   minusinf:: "fm \<Rightarrow> fm"

   \<delta> :: "fm \<Rightarrow> int" 

   d\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool"

 recdef minusinf "measure size"

   "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"

 lemma minusinf_qfree: "qfree p \<Longrightarrow> qfree (minusinf p)"

   by (induct p rule: minusinf.induct, auto)

 recdef plusinf "measure size"

   "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"

 recdef \<delta> "measure size"

   "\<delta> (And p q) = lcm (\<delta> p) (\<delta> q)" 

   "\<delta> (Or p q) = lcm (\<delta> p) (\<delta> q)" 

   "\<delta> (Dvd i (CN 0 c e)) = i"

   "\<delta> (NDvd i (CN 0 c e)) = i"

   "\<delta> p = 1"

 recdef d\<delta> "measure size"

   "d\<delta> (And p q) = (\<lambda> d. d\<delta> p d \<and> d\<delta> q d)" 

   "d\<delta> (Or p q) = (\<lambda> d. d\<delta> p d \<and> d\<delta> q d)" 

   "d\<delta> (Dvd i (CN 0 c e)) = (\<lambda> d. i dvd d)"

   "d\<delta> (NDvd i (CN 0 c e)) = (\<lambda> d. i dvd d)"

   "d\<delta> p = (\<lambda> d. True)"

 lemma delta_mono: 

   assumes lin: "iszlfm p bs"

   and d: "d dvd d'"

   and ad: "d\<delta> p d"

   shows "d\<delta> p d'"

   using lin ad d

 proof(induct p rule: iszlfm.induct)

   case (9 i c e)  thus ?case using d

     by (simp add: dvd_trans[of "i" "d" "d'"])

 next

   case (10 i c e) thus ?case using d

     by (simp add: dvd_trans[of "i" "d" "d'"])

 qed simp_all

 lemma \<delta> : assumes lin:"iszlfm p bs"

   shows "d\<delta> p (\<delta> p) \<and> \<delta> p >0"

 using lin

 proof (induct p rule: iszlfm.induct)

   case (1 p q) 

   let ?d = "\<delta> (And p q)"

   from prems lcm_pos_int have dp: "?d >0" by simp

   have d1: "\<delta> p dvd \<delta> (And p q)" using prems by simp 

    hence th: "d\<delta> p ?d" 

      using delta_mono prems by(simp only: iszlfm.simps) blast

   have "\<delta> q dvd \<delta> (And p q)" using prems  by simp 

   hence th': "d\<delta> q ?d" using delta_mono prems by(simp only: iszlfm.simps) blast

   from th th' dp show ?case by simp 

 next

   case (2 p q)  

   let ?d = "\<delta> (And p q)"

   from prems lcm_pos_int have dp: "?d >0" by simp

   have "\<delta> p dvd \<delta> (And p q)" using prems by simp hence th: "d\<delta> p ?d" using delta_mono prems 

     by(simp only: iszlfm.simps) blast

   have "\<delta> q dvd \<delta> (And p q)" using prems by simp hence th': "d\<delta> q ?d" using delta_mono prems by(simp only: iszlfm.simps) blast

   from th th' dp show ?case by simp

 qed simp_all

 lemma minusinf_inf:

   assumes linp: "iszlfm p (a # bs)"

   shows "\<exists> (z::int). \<forall> x < z. Ifm ((real x)#bs) (minusinf p) = Ifm ((real x)#bs) p"

   (is "?P p" is "\<exists> (z::int). \<forall> x < z. ?I x (?M p) = ?I x p")

 using linp

 proof (induct p rule: minusinf.induct)

   case (1 f g)

   from prems have "?P f" by simp

   then obtain z1 where z1_def: "\<forall> x < z1. ?I x (?M f) = ?I x f" by blast

   from prems have "?P g" by simp

   then obtain z2 where z2_def: "\<forall> x < z2. ?I x (?M g) = ?I x g" by blast

   let ?z = "min z1 z2"

   from z1_def z2_def have "\<forall> x < ?z. ?I x (?M (And f g)) = ?I x (And f g)" by simp

   thus ?case by blast

 next

   case (2 f g)   from prems have "?P f" by simp

   then obtain z1 where z1_def: "\<forall> x < z1. ?I x (?M f) = ?I x f" by blast

   from prems have "?P g" by simp

   then obtain z2 where z2_def: "\<forall> x < z2. ?I x (?M g) = ?I x g" by blast

   let ?z = "min z1 z2"

   from z1_def z2_def have "\<forall> x < ?z. ?I x (?M (Or f g)) = ?I x (Or f g)" by simp

   thus ?case by blast

 next

   case (3 c e) 

   from prems have "c > 0" by simp hence rcpos: "real c > 0" by simp

   from prems have nbe: "numbound0 e" by simp

   fix y

   have "\<forall> x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (Eq (CN 0 c e))) = ?I x (Eq (CN 0 c e))"

   proof (simp add: less_floor_eq , rule allI, rule impI) 

     fix x

     assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"

     hence th1:"real x < - (Inum (y # bs) e / real c)" by simp

     with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"

       by (simp only:  real_mult_less_mono2[OF rcpos th1])

     hence "real c * real x + Inum (y # bs) e \<noteq> 0"using rcpos  by simp

     thus "real c * real x + Inum (real x # bs) e \<noteq> 0" 

       using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"]  by simp

   qed

   thus ?case by blast

 next

   case (4 c e) 

   from prems have "c > 0" by simp hence rcpos: "real c > 0" by simp

   from prems have nbe: "numbound0 e" by simp

   fix y

   have "\<forall> x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (NEq (CN 0 c e))) = ?I x (NEq (CN 0 c e))"

   proof (simp add: less_floor_eq , rule allI, rule impI) 

     fix x

     assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"

     hence th1:"real x < - (Inum (y # bs) e / real c)" by simp

     with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"

       by (simp only:  real_mult_less_mono2[OF rcpos th1])

     hence "real c * real x + Inum (y # bs) e \<noteq> 0"using rcpos  by simp

     thus "real c * real x + Inum (real x # bs) e \<noteq> 0" 

       using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"]  by simp

   qed

   thus ?case by blast

 next

   case (5 c e) 

   from prems have "c > 0" by simp hence rcpos: "real c > 0" by simp

   from prems have nbe: "numbound0 e" by simp

   fix y

   have "\<forall> x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (Lt (CN 0 c e))) = ?I x (Lt (CN 0 c e))"

   proof (simp add: less_floor_eq , rule allI, rule impI) 

     fix x

     assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"

     hence th1:"real x < - (Inum (y # bs) e / real c)" by simp

     with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"

       by (simp only:  real_mult_less_mono2[OF rcpos th1])

     thus "real c * real x + Inum (real x # bs) e < 0" 

       using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] rcpos by simp

   qed

   thus ?case by blast

 next

   case (6 c e) 

   from prems have "c > 0" by simp hence rcpos: "real c > 0" by simp

   from prems have nbe: "numbound0 e" by simp

   fix y

   have "\<forall> x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (Le (CN 0 c e))) = ?I x (Le (CN 0 c e))"

   proof (simp add: less_floor_eq , rule allI, rule impI) 

     fix x

     assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"

     hence th1:"real x < - (Inum (y # bs) e / real c)" by simp

     with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"

       by (simp only:  real_mult_less_mono2[OF rcpos th1])

     thus "real c * real x + Inum (real x # bs) e \<le> 0" 

       using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] rcpos by simp

   qed

   thus ?case by blast

 next

   case (7 c e) 

   from prems have "c > 0" by simp hence rcpos: "real c > 0" by simp

   from prems have nbe: "numbound0 e" by simp

   fix y

   have "\<forall> x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (Gt (CN 0 c e))) = ?I x (Gt (CN 0 c e))"

   proof (simp add: less_floor_eq , rule allI, rule impI) 

     fix x

     assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"

     hence th1:"real x < - (Inum (y # bs) e / real c)" by simp

     with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"

       by (simp only:  real_mult_less_mono2[OF rcpos th1])

     thus "\<not> (real c * real x + Inum (real x # bs) e>0)" 

       using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] rcpos by simp

   qed

   thus ?case by blast

 next

   case (8 c e) 

   from prems have "c > 0" by simp hence rcpos: "real c > 0" by simp

   from prems have nbe: "numbound0 e" by simp

   fix y

   have "\<forall> x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (Ge (CN 0 c e))) = ?I x (Ge (CN 0 c e))"

   proof (simp add: less_floor_eq , rule allI, rule impI) 

     fix x

     assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"

     hence th1:"real x < - (Inum (y # bs) e / real c)" by simp

     with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"

       by (simp only:  real_mult_less_mono2[OF rcpos th1])

     thus "\<not> real c * real x + Inum (real x # bs) e \<ge> 0" 

       using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] rcpos by simp

   qed

   thus ?case by blast

 qed simp_all

 lemma minusinf_repeats:

   assumes d: "d\<delta> p d" and linp: "iszlfm p (a # bs)"

   shows "Ifm ((real(x - k*d))#bs) (minusinf p) = Ifm (real x #bs) (minusinf p)"

 using linp d

 proof(induct p rule: iszlfm.induct) 

   case (9 i c e) hence nbe: "numbound0 e"  and id: "i dvd d" by simp+

     hence "\<exists> k. d=i*k" by (simp add: dvd_def)

     then obtain "di" where di_def: "d=i*di" by blast

     show ?case 

     proof(simp add: numbound0_I[OF nbe,where bs="bs" and b="real x - real k * real d" and b'="real x"] right_diff_distrib, rule iffI)

       assume 

         "real i rdvd real c * real x - real c * (real k * real d) + Inum (real x # bs) e"

       (is "?ri rdvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri rdvd ?rt")

       hence "\<exists> (l::int). ?rt = ?ri * (real l)" by (simp add: rdvd_def)

       hence "\<exists> (l::int). ?rc*?rx+ ?I x e = ?ri*(real l)+?rc*(?rk * (real i) * (real di))" 

         by (simp add: algebra_simps di_def)

       hence "\<exists> (l::int). ?rc*?rx+ ?I x e = ?ri*(real (l + c*k*di))"

         by (simp add: algebra_simps)

       hence "\<exists> (l::int). ?rc*?rx+ ?I x e = ?ri* (real l)" by blast

       thus "real i rdvd real c * real x + Inum (real x # bs) e" using rdvd_def by simp

     next

       assume 

         "real i rdvd real c * real x + Inum (real x # bs) e" (is "?ri rdvd ?rc*?rx+?e")

       hence "\<exists> (l::int). ?rc*?rx+?e = ?ri * (real l)" by (simp add: rdvd_def)

       hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real l) - real c * (real k * real d)" by simp

       hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real l) - real c * (real k * real i * real di)" by (simp add: di_def)

       hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real (l - c*k*di))" by (simp add: algebra_simps)

       hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real l)"

         by blast

       thus "real i rdvd real c * real x - real c * (real k * real d) + Inum (real x # bs) e" using rdvd_def by simp

     qed

 next

   case (10 i c e) hence nbe: "numbound0 e"  and id: "i dvd d" by simp+

     hence "\<exists> k. d=i*k" by (simp add: dvd_def)

     then obtain "di" where di_def: "d=i*di" by blast

     show ?case 

     proof(simp add: numbound0_I[OF nbe,where bs="bs" and b="real x - real k * real d" and b'="real x"] right_diff_distrib, rule iffI)

       assume 

         "real i rdvd real c * real x - real c * (real k * real d) + Inum (real x # bs) e"

       (is "?ri rdvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri rdvd ?rt")

       hence "\<exists> (l::int). ?rt = ?ri * (real l)" by (simp add: rdvd_def)

       hence "\<exists> (l::int). ?rc*?rx+ ?I x e = ?ri*(real l)+?rc*(?rk * (real i) * (real di))" 

         by (simp add: algebra_simps di_def)

       hence "\<exists> (l::int). ?rc*?rx+ ?I x e = ?ri*(real (l + c*k*di))"

         by (simp add: algebra_simps)

       hence "\<exists> (l::int). ?rc*?rx+ ?I x e = ?ri* (real l)" by blast

       thus "real i rdvd real c * real x + Inum (real x # bs) e" using rdvd_def by simp

     next

       assume 

         "real i rdvd real c * real x + Inum (real x # bs) e" (is "?ri rdvd ?rc*?rx+?e")

       hence "\<exists> (l::int). ?rc*?rx+?e = ?ri * (real l)" by (simp add: rdvd_def)

       hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real l) - real c * (real k * real d)" by simp

       hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real l) - real c * (real k * real i * real di)" by (simp add: di_def)

       hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real (l - c*k*di))" by (simp add: algebra_simps)

       hence "\<exists> (l::int). ?rc*?rx - real c * (real k * real d) +?e = ?ri * (real l)"

         by blast

       thus "real i rdvd real c * real x - real c * (real k * real d) + Inum (real x # bs) e" using rdvd_def by simp

     qed

 qed (auto simp add: nth_pos2 numbound0_I[where bs="bs" and b="real(x - k*d)" and b'="real x"] simp del: real_of_int_mult real_of_int_diff)

 lemma minusinf_ex:

   assumes lin: "iszlfm p (real (a::int) #bs)"

   and exmi: "\<exists> (x::int). Ifm (real x#bs) (minusinf p)" (is "\<exists> x. ?P1 x")

   shows "\<exists> (x::int). Ifm (real x#bs) p" (is "\<exists> x. ?P x")

 proof-

   let ?d = "\<delta> p"

   from \<delta> [OF lin] have dpos: "?d >0" by simp

   from \<delta> [OF lin] have alld: "d\<delta> p ?d" by simp

   from minusinf_repeats[OF alld lin] have th1:"\<forall> x k. ?P1 x = ?P1 (x - (k * ?d))" by simp

   from minusinf_inf[OF lin] have th2:"\<exists> z. \<forall> x. x<z \<longrightarrow> (?P x = ?P1 x)" by blast

   from minusinfinity [OF dpos th1 th2] exmi show ?thesis by blast

 qed

 lemma minusinf_bex:

   assumes lin: "iszlfm p (real (a::int) #bs)"

   shows "(\<exists> (x::int). Ifm (real x#bs) (minusinf p)) = 

          (\<exists> (x::int)\<in> {1..\<delta> p}. Ifm (real x#bs) (minusinf p))"

   (is "(\<exists> x. ?P x) = _")

 proof-

   let ?d = "\<delta> p"

   from \<delta> [OF lin] have dpos: "?d >0" by simp

   from \<delta> [OF lin] have alld: "d\<delta> p ?d" by simp

   from minusinf_repeats[OF alld lin] have th1:"\<forall> x k. ?P x = ?P (x - (k * ?d))" by simp

   from periodic_finite_ex[OF dpos th1] show ?thesis by blast

 qed

 lemma dvd1_eq1: "x >0 \<Longrightarrow> (x::int) dvd 1 = (x = 1)" by auto

 consts 

   a\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" (* adjusts the coeffitients of a formula *)

   d\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool" (* tests if all coeffs c of c divide a given l*)

   \<zeta>  :: "fm \<Rightarrow> int" (* computes the lcm of all coefficients of x*)

   \<beta> :: "fm \<Rightarrow> num list"

   \<alpha> :: "fm \<Rightarrow> num list"

 recdef a\<beta> "measure size"

   "a\<beta> (And p q) = (\<lambda> k. And (a\<beta> p k) (a\<beta> q k))" 

   "a\<beta> (Or p q) = (\<lambda> k. Or (a\<beta> p k) (a\<beta> q k))" 

   "a\<beta> (Eq  (CN 0 c e)) = (\<lambda> k. Eq (CN 0 1 (Mul (k div c) e)))"

   "a\<beta> (NEq (CN 0 c e)) = (\<lambda> k. NEq (CN 0 1 (Mul (k div c) e)))"

   "a\<beta> (Lt  (CN 0 c e)) = (\<lambda> k. Lt (CN 0 1 (Mul (k div c) e)))"

   "a\<beta> (Le  (CN 0 c e)) = (\<lambda> k. Le (CN 0 1 (Mul (k div c) e)))"

   "a\<beta> (Gt  (CN 0 c e)) = (\<lambda> k. Gt (CN 0 1 (Mul (k div c) e)))"

   "a\<beta> (Ge  (CN 0 c e)) = (\<lambda> k. Ge (CN 0 1 (Mul (k div c) e)))"

   "a\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"

   "a\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"

   "a\<beta> p = (\<lambda> k. p)"

 recdef d\<beta> "measure size"

   "d\<beta> (And p q) = (\<lambda> k. (d\<beta> p k) \<and> (d\<beta> q k))" 

   "d\<beta> (Or p q) = (\<lambda> k. (d\<beta> p k) \<and> (d\<beta> q k))" 

   "d\<beta> (Eq  (CN 0 c e)) = (\<lambda> k. c dvd k)"

   "d\<beta> (NEq (CN 0 c e)) = (\<lambda> k. c dvd k)"

   "d\<beta> (Lt  (CN 0 c e)) = (\<lambda> k. c dvd k)"

   "d\<beta> (Le  (CN 0 c e)) = (\<lambda> k. c dvd k)"

   "d\<beta> (Gt  (CN 0 c e)) = (\<lambda> k. c dvd k)"

   "d\<beta> (Ge  (CN 0 c e)) = (\<lambda> k. c dvd k)"

   "d\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. c dvd k)"

   "d\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. c dvd k)"

   "d\<beta> p = (\<lambda> k. True)"

 recdef \<zeta> "measure size"

   "\<zeta> (And p q) = lcm (\<zeta> p) (\<zeta> q)" 

   "\<zeta> (Or p q) = lcm (\<zeta> p) (\<zeta> q)" 

   "\<zeta> (Eq  (CN 0 c e)) = c"

   "\<zeta> (NEq (CN 0 c e)) = c"

   "\<zeta> (Lt  (CN 0 c e)) = c"

   "\<zeta> (Le  (CN 0 c e)) = c"

   "\<zeta> (Gt  (CN 0 c e)) = c"

   "\<zeta> (Ge  (CN 0 c e)) = c"

   "\<zeta> (Dvd i (CN 0 c e)) = c"

   "\<zeta> (NDvd i (CN 0 c e))= c"

   "\<zeta> p = 1"

 recdef \<beta> "measure size"

   "\<beta> (And p q) = (\<beta> p @ \<beta> q)" 

   "\<beta> (Or p q) = (\<beta> p @ \<beta> q)" 

   "\<beta> (Eq  (CN 0 c e)) = [Sub (C -1) e]"

   "\<beta> (NEq (CN 0 c e)) = [Neg e]"

   "\<beta> (Lt  (CN 0 c e)) = []"

   "\<beta> (Le  (CN 0 c e)) = []"

   "\<beta> (Gt  (CN 0 c e)) = [Neg e]"

   "\<beta> (Ge  (CN 0 c e)) = [Sub (C -1) e]"

   "\<beta> p = []"

 recdef \<alpha> "measure size"

   "\<alpha> (And p q) = (\<alpha> p @ \<alpha> q)" 

   "\<alpha> (Or p q) = (\<alpha> p @ \<alpha> q)" 

   "\<alpha> (Eq  (CN 0 c e)) = [Add (C -1) e]"

   "\<alpha> (NEq (CN 0 c e)) = [e]"

   "\<alpha> (Lt  (CN 0 c e)) = [e]"

   "\<alpha> (Le  (CN 0 c e)) = [Add (C -1) e]"

   "\<alpha> (Gt  (CN 0 c e)) = []"

   "\<alpha> (Ge  (CN 0 c e)) = []"

   "\<alpha> p = []"

 consts mirror :: "fm \<Rightarrow> fm"

 recdef mirror "measure size"

   "mirror (And p q) = And (mirror p) (mirror q)" 

   "mirror (Or p q) = Or (mirror p) (mirror q)" 

   "mirror (Eq  (CN 0 c e)) = Eq (CN 0 c (Neg e))"

   "mirror (NEq (CN 0 c e)) = NEq (CN 0 c (Neg e))"

   "mirror (Lt  (CN 0 c e)) = Gt (CN 0 c (Neg e))"

   "mirror (Le  (CN 0 c e)) = Ge (CN 0 c (Neg e))"

   "mirror (Gt  (CN 0 c e)) = Lt (CN 0 c (Neg e))"

   "mirror (Ge  (CN 0 c e)) = Le (CN 0 c (Neg e))"

   "mirror (Dvd i (CN 0 c e)) = Dvd i (CN 0 c (Neg e))"

   "mirror (NDvd i (CN 0 c e)) = NDvd i (CN 0 c (Neg e))"

   "mirror p = p"

 lemma mirror\<alpha>\<beta>:

   assumes lp: "iszlfm p (a#bs)"

   shows "(Inum (real (i::int)#bs)) ` set (\<alpha> p) = (Inum (real i#bs)) ` set (\<beta> (mirror p))"

 using lp

 by (induct p rule: mirror.induct, auto)

 lemma mirror: 

   assumes lp: "iszlfm p (a#bs)"

   shows "Ifm (real (x::int)#bs) (mirror p) = Ifm (real (- x)#bs) p" 

 using lp

 proof(induct p rule: iszlfm.induct)

   case (9 j c e)

   have th: "(real j rdvd real c * real x - Inum (real x # bs) e) =

        (real j rdvd - (real c * real x - Inum (real x # bs) e))"

     by (simp only: rdvd_minus[symmetric])

   from prems th show  ?case

     by (simp add: algebra_simps

       numbound0_I[where bs="bs" and b'="real x" and b="- real x"])

 next

     case (10 j c e)

   have th: "(real j rdvd real c * real x - Inum (real x # bs) e) =

        (real j rdvd - (real c * real x - Inum (real x # bs) e))"

     by (simp only: rdvd_minus[symmetric])

   from prems th show  ?case

     by (simp add: algebra_simps

       numbound0_I[where bs="bs" and b'="real x" and b="- real x"])

 qed (auto simp add: numbound0_I[where bs="bs" and b="real x" and b'="- real x"] nth_pos2)

 lemma mirror_l: "iszlfm p (a#bs) \<Longrightarrow> iszlfm (mirror p) (a#bs)"

 by (induct p rule: mirror.induct, auto simp add: isint_neg)

 lemma mirror_d\<beta>: "iszlfm p (a#bs) \<and> d\<beta> p 1 

   \<Longrightarrow> iszlfm (mirror p) (a#bs) \<and> d\<beta> (mirror p) 1"

 by (induct p rule: mirror.induct, auto simp add: isint_neg)

 lemma mirror_\<delta>: "iszlfm p (a#bs) \<Longrightarrow> \<delta> (mirror p) = \<delta> p"

 by (induct p rule: mirror.induct,auto)

 lemma mirror_ex: 

   assumes lp: "iszlfm p (real (i::int)#bs)"

   shows "(\<exists> (x::int). Ifm (real x#bs) (mirror p)) = (\<exists> (x::int). Ifm (real x#bs) p)"

   (is "(\<exists> x. ?I x ?mp) = (\<exists> x. ?I x p)")

 proof(auto)

   fix x assume "?I x ?mp" hence "?I (- x) p" using mirror[OF lp] by blast

   thus "\<exists> x. ?I x p" by blast

 next

   fix x assume "?I x p" hence "?I (- x) ?mp" 

     using mirror[OF lp, where x="- x", symmetric] by auto

   thus "\<exists> x. ?I x ?mp" by blast

 qed

 lemma \<beta>_numbound0: assumes lp: "iszlfm p bs"

   shows "\<forall> b\<in> set (\<beta> p). numbound0 b"

   using lp by (induct p rule: \<beta>.induct,auto)

 lemma d\<beta>_mono: 

   assumes linp: "iszlfm p (a #bs)"

   and dr: "d\<beta> p l"

   and d: "l dvd l'"

   shows "d\<beta> p l'"

 using dr linp dvd_trans[of _ "l" "l'", simplified d]

 by (induct p rule: iszlfm.induct) simp_all

 lemma \<alpha>_l: assumes lp: "iszlfm p (a#bs)"

   shows "\<forall> b\<in> set (\<alpha> p). numbound0 b \<and> isint b (a#bs)"

 using lp

 by(induct p rule: \<alpha>.induct, auto simp add: isint_add isint_c)

 lemma \<zeta>: 

   assumes linp: "iszlfm p (a #bs)"

   shows "\<zeta> p > 0 \<and> d\<beta> p (\<zeta> p)"

 using linp

 proof(induct p rule: iszlfm.induct)

   case (1 p q)

   from prems have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp

   from prems have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp

   from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] 

     d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] 

     dl1 dl2 show ?case by (auto simp add: lcm_pos_int)

 next

   case (2 p q)

   from prems have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp

   from prems have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp

   from prems d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] 

     d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] 

     dl1 dl2 show ?case by (auto simp add: lcm_pos_int)

 qed (auto simp add: lcm_pos_int)

 lemma a\<beta>: assumes linp: "iszlfm p (a #bs)" and d: "d\<beta> p l" and lp: "l > 0"

   shows "iszlfm (a\<beta> p l) (a #bs) \<and> d\<beta> (a\<beta> p l) 1 \<and> (Ifm (real (l * x) #bs) (a\<beta> p l) = Ifm ((real x)#bs) p)"

 using linp d

 proof (induct p rule: iszlfm.induct)

   case (5 c e) hence cp: "c>0" and be: "numbound0 e" and ei:"isint e (a#bs)" and d': "c dvd l" by simp+

     from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])

     from cp have cnz: "c \<noteq> 0" by simp

     have "c div c\<le> l div c"

       by (simp add: zdiv_mono1[OF clel cp])

     then have ldcp:"0 < l div c" 

       by (simp add: zdiv_self[OF cnz])

     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp

     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 

       by simp

     hence "(real l * real x + real (l div c) * Inum (real x # bs) e < (0\<Colon>real)) =

           (real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e < 0)"

       by simp

     also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) < (real (l div c)) * 0)" by (simp add: algebra_simps)

     also have "\<dots> = (real c * real x + Inum (real x # bs) e < 0)"

     using mult_less_0_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e"] ldcp by simp

   finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"] be  isint_Mul[OF ei] by simp

 next

   case (6 c e) hence cp: "c>0" and be: "numbound0 e" and ei:"isint e (a#bs)" and d': "c dvd l" by simp+

     from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])

     from cp have cnz: "c \<noteq> 0" by simp

     have "c div c\<le> l div c"

       by (simp add: zdiv_mono1[OF clel cp])

     then have ldcp:"0 < l div c" 

       by (simp add: zdiv_self[OF cnz])

     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp

     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 

       by simp

     hence "(real l * real x + real (l div c) * Inum (real x # bs) e \<le> (0\<Colon>real)) =

           (real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e \<le> 0)"

       by simp

     also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) \<le> (real (l div c)) * 0)" by (simp add: algebra_simps)

     also have "\<dots> = (real c * real x + Inum (real x # bs) e \<le> 0)"

     using mult_le_0_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e"] ldcp by simp

   finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"]  be  isint_Mul[OF ei] by simp

 next

   case (7 c e) hence cp: "c>0" and be: "numbound0 e" and ei:"isint e (a#bs)" and d': "c dvd l" by simp+

     from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])

     from cp have cnz: "c \<noteq> 0" by simp

     have "c div c\<le> l div c"

       by (simp add: zdiv_mono1[OF clel cp])

     then have ldcp:"0 < l div c" 

       by (simp add: zdiv_self[OF cnz])

     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp

     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 

       by simp

     hence "(real l * real x + real (l div c) * Inum (real x # bs) e > (0\<Colon>real)) =

           (real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e > 0)"

       by simp

     also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) > (real (l div c)) * 0)" by (simp add: algebra_simps)

     also have "\<dots> = (real c * real x + Inum (real x # bs) e > 0)"

     using zero_less_mult_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e"] ldcp by simp

   finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"]  be  isint_Mul[OF ei] by simp

 next

   case (8 c e) hence cp: "c>0" and be: "numbound0 e"  and ei:"isint e (a#bs)" and d': "c dvd l" by simp+

     from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])

     from cp have cnz: "c \<noteq> 0" by simp

     have "c div c\<le> l div c"

       by (simp add: zdiv_mono1[OF clel cp])

     then have ldcp:"0 < l div c" 

       by (simp add: zdiv_self[OF cnz])

     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp

     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 

       by simp

     hence "(real l * real x + real (l div c) * Inum (real x # bs) e \<ge> (0\<Colon>real)) =

           (real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e \<ge> 0)"

       by simp

     also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) \<ge> (real (l div c)) * 0)" by (simp add: algebra_simps)

     also have "\<dots> = (real c * real x + Inum (real x # bs) e \<ge> 0)"

     using zero_le_mult_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e"] ldcp by simp

   finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"]  be  isint_Mul[OF ei] by simp

 next

   case (3 c e) hence cp: "c>0" and be: "numbound0 e" and ei:"isint e (a#bs)" and d': "c dvd l" by simp+

     from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])

     from cp have cnz: "c \<noteq> 0" by simp

     have "c div c\<le> l div c"

       by (simp add: zdiv_mono1[OF clel cp])

     then have ldcp:"0 < l div c" 

       by (simp add: zdiv_self[OF cnz])

     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp

     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 

       by simp

     hence "(real l * real x + real (l div c) * Inum (real x # bs) e = (0\<Colon>real)) =

           (real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e = 0)"

       by simp

     also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) = (real (l div c)) * 0)" by (simp add: algebra_simps)

     also have "\<dots> = (real c * real x + Inum (real x # bs) e = 0)"

     using mult_eq_0_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e"] ldcp by simp

   finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"]  be  isint_Mul[OF ei] by simp

 next

   case (4 c e) hence cp: "c>0" and be: "numbound0 e" and ei:"isint e (a#bs)" and d': "c dvd l" by simp+

     from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])

     from cp have cnz: "c \<noteq> 0" by simp

     have "c div c\<le> l div c"

       by (simp add: zdiv_mono1[OF clel cp])

     then have ldcp:"0 < l div c" 

       by (simp add: zdiv_self[OF cnz])

     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp

     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 

       by simp

     hence "(real l * real x + real (l div c) * Inum (real x # bs) e \<noteq> (0\<Colon>real)) =

           (real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e \<noteq> 0)"

       by simp

     also have "\<dots> = (real (l div c) * (real c * real x + Inum (real x # bs) e) \<noteq> (real (l div c)) * 0)" by (simp add: algebra_simps)

     also have "\<dots> = (real c * real x + Inum (real x # bs) e \<noteq> 0)"

     using zero_le_mult_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e"] ldcp by simp

   finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"]  be  isint_Mul[OF ei] by simp

 next

   case (9 j c e) hence cp: "c>0" and be: "numbound0 e" and ei:"isint e (a#bs)" and jp: "j > 0" and d': "c dvd l" by simp+

     from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp])

     from cp have cnz: "c \<noteq> 0" by simp

     have "c div c\<le> l div c"

       by (simp add: zdiv_mono1[OF clel cp])

     then have ldcp:"0 < l div c" 

       by (simp add: zdiv_self[OF cnz])

     have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] by simp

     hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] 

       by simp

     hence "(\<exists> (k::int). real l * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k) = (\<exists> (k::int). real (c * (l div c)) * real x + real (l div c) * Inum (real x # bs) e = (real (l div c) * real j) * real k)"  by simp

     also have "\<dots> = (\<exists> (k::int). real (l div c) * (real c * real x + Inum (real x # bs) e - real j * real k) = real (l div c)*0)" by (simp add: algebra_simps)

     also fix k have "\<dots> = (\<exists> (k::int). real c * real x + Inum (real x # bs) e - real j * real k = 0)"

     using zero_le_mult_iff [where a="real (l div c)" and b="real c * real x + Inum (real x # bs) e - real j * real k"] ldcp by simp