Quelle MIR.thy Sprache: Isabelle

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

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

section \<open>Prelude\<close>

abbreviation (input) UNION :: "'a set \ ('a \ 'b set) \ 'b set"
  where "UNION A f \ \ (f ` A)" \ \legacy\

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

declare of_int_floor_cancel [simp del]

lemma myle:
  fixes a b :: "'a::{ordered_ab_group_add}"
  shows "(a \ b) = (0 \ b - a)"
  by (metis add_0_left add_le_cancel_right diff_add_cancel)

lemma myless:
  fixes a b :: "'a::{ordered_ab_group_add}"
  shows "(a < b) = (0 < b - a)"
  by (metis le_iff_diff_le_0 less_le_not_le myle)

(* Periodicity of dvd *)
lemmas dvd_period = zdvd_period

(* The Divisibility relation between reals *)
definition rdvd:: "real \ real \ bool" (infixl \rdvd\ 50)
  where "x rdvd y \ (\k::int. y = x * real_of_int k)"

lemma int_rdvd_real:
  "real_of_int (i::int) rdvd x = (i dvd \x\ \ real_of_int \x\ = x)" (is "?l = ?r")
proof
  assume "?l"
  hence th: "\ k. x=real_of_int (i*k)" by (simp add: rdvd_def)
  hence th': "real_of_int \x\ = x" by (auto simp del: of_int_mult)
  with th have "\ k. real_of_int \x\ = real_of_int (i*k)" by simp
  hence "\k. \x\ = i*k" by presburger
  thus ?r using th' by (simp add: dvd_def)
next
  assume "?r" hence "(i::int) dvd \x::real\" ..
  hence "\k. real_of_int \x\ = real_of_int (i*k)"
    by (metis (no_types) dvd_def)
  thus ?l using \<open>?r\<close> by (simp add: rdvd_def)
qed

lemma int_rdvd_iff: "(real_of_int (i::int) rdvd real_of_int t) = (i dvd t)"
  by (auto simp add: rdvd_def dvd_def) (rule_tac x="k" in exI, simp only: of_int_mult[symmetric])

lemma rdvd_abs1: "(\real_of_int d\ rdvd t) = (real_of_int (d ::int) rdvd t)"
proof
  assume d: "real_of_int d rdvd t"
  from d int_rdvd_real have d2: "d dvd \t\" and ti: "real_of_int \t\ = t"
    by auto

  from iffD2[OF abs_dvd_iff] d2 have "\d\ dvd \t\" by blast
  with ti int_rdvd_real[symmetric] have "real_of_int \d\ rdvd t" by blast
  thus "\real_of_int d\ rdvd t" by simp
next
  assume "\real_of_int d\ rdvd t" hence "real_of_int \d\ rdvd t" by simp
  with int_rdvd_real[where i="\d\" and x="t"]
  have d2: "\d\ dvd \t\" and ti: "real_of_int \t\ = t"
    by auto
  from iffD1[OF abs_dvd_iff] d2 have "d dvd \t\" by blast
  with ti int_rdvd_real[symmetric] show "real_of_int d rdvd t" by blast
qed

lemma rdvd_minus: "(real_of_int (d::int) rdvd t) = (real_of_int d rdvd -t)"
  by (metis equation_minus_iff mult_minus_right of_int_minus rdvd_def)

lemma rdvd_left_0_eq: "(0 rdvd t) = (t=0)"
  by (auto simp add: rdvd_def)

lemma rdvd_mult:
  assumes knz: "k\0"
  shows "(real_of_int (n::int) * real_of_int (k::int) rdvd x * real_of_int k) = (real_of_int n rdvd x)"
  using knz by (simp add: rdvd_def)

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

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

instantiation num :: size
begin

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

instance ..

end

  (* Semantics of numeral terms (num) *)
primrec Inum :: "real list \ num \ real"
where
  "Inum bs (C c) = (real_of_int c)"
| "Inum bs (Bound n) = bs!n"
| "Inum bs (CN n c a) = (real_of_int c) * (bs!n) + (Inum bs a)"
| "Inum bs (Neg a) = -(Inum bs a)"
| "Inum bs (Add a b) = Inum bs a + Inum bs b"
| "Inum bs (Sub a b) = Inum bs a - Inum bs b"
| "Inum bs (Mul c a) = (real_of_int c) * Inum bs a"
| "Inum bs (Floor a) = real_of_int \Inum bs a\"
| "Inum bs (CF c a b) = real_of_int c * real_of_int \Inum bs a\ + Inum bs b"
definition "isint t bs \ real_of_int \Inum bs t\ = Inum bs t"

lemma isint_iff: "isint n bs = (real_of_int \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 \ isint (Mul c e) bs"
proof-
  let ?e = "Inum bs e"
  assume be: "isint e bs" hence efe:"real_of_int \?e\ = ?e" by (simp add: isint_iff)
  have "real_of_int \Inum bs (Mul c e)\ = real_of_int \real_of_int (c * \?e\)\"
    using efe by simp
  also have "\ = real_of_int (c* \?e\)" by (metis floor_of_int)
  also have "\ = real_of_int c * ?e" using efe by simp
  finally show ?thesis using isint_iff by simp
qed

lemma isint_neg: "isint e bs \ isint (Neg e) bs"
proof-
  let ?I = "\ t. Inum bs t"
  assume ie: "isint e bs"
  hence th: "real_of_int \?I e\ = ?I e" by (simp add: isint_def)
  have "real_of_int \?I (Neg e)\ = real_of_int \- (real_of_int \?I e\)\"
    by (simp add: th)
  also have "\ = - real_of_int \?I e\" by simp
  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 = "\ t. Inum bs t"
  from ie have th: "real_of_int \?I e\ = ?I e" by (simp add: isint_def)
  have "real_of_int \?I (Sub (C c) e)\ = real_of_int \real_of_int (c - \?I e\)\"
    by (simp add: th)
  also have "\ = real_of_int (c - \?I e\)" by simp
  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_of_int \?a + ?b\ = real_of_int \real_of_int \?a\ + real_of_int \?b\\"
    by simp
  also have "\ = real_of_int \?a\ + real_of_int \?b\" by simp
  also have "\ = ?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 (plugins del: size) 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

instantiation fm :: size
begin

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

instance ..

end

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

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

fun prep :: "fm \ fm"
where
  "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"

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

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

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

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

lemma numbound0_gen:
  assumes nb: "numbound0 t" and ti: "isint t (x#bs)"
  shows "\ 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 \ 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 \ bound0 q)"
| "bound0 (Or p q) = (bound0 p \ bound0 q)"
| "bound0 (Imp p q) = ((bound0 p) \ (bound0 q))"
| "bound0 (Iff p q) = (bound0 p \ bound0 q)"
| "bound0 (E p) = False"
| "bound0 (A p) = False"

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

primrec numsubst0:: "num \ num \ 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

primrec subst0:: "num \ fm \ 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

fun decrnum:: "num \ num"
where
  "decrnum (Bound n) = Bound (n - 1)"
| "decrnum (Neg a) = Neg (decrnum a)"
| "decrnum (Add a b) = Add (decrnum a) (decrnum b)"
| "decrnum (Sub a b) = Sub (decrnum a) (decrnum b)"
| "decrnum (Mul c a) = Mul c (decrnum a)"
| "decrnum (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"

fun decr :: "fm \ fm"
where
  "decr (Lt a) = Lt (decrnum a)"
| "decr (Le a) = Le (decrnum a)"
| "decr (Gt a) = Gt (decrnum a)"
| "decr (Ge a) = Ge (decrnum a)"
| "decr (Eq a) = Eq (decrnum a)"
| "decr (NEq a) = NEq (decrnum a)"
| "decr (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

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

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

fun isatom :: "fm \ bool" (* test for atomicity *)
where
  "isatom T = True"
| "isatom F = True"
| "isatom (Lt a) = True"
| "isatom (Le a) = True"
| "isatom (Gt a) = True"
| "isatom (Ge a) = True"
| "isatom (Eq a) = True"
| "isatom (NEq a) = True"
| "isatom (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 \ qfree p"
  by (induct p) simp_all

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

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

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

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

lemma evaldjf_bound0:
  assumes "\x \ set xs. bound0 (f x)"
  shows "bound0 (evaldjf f xs)"
  using assms
  by (induct xs) (auto simp add: evaldjf_def djf_def Let_def split: fm.split)

lemma evaldjf_qf:
  assumes "\x \ set xs. qfree (f x)"
  shows "qfree (evaldjf f xs)"
  using assms
  by (induct xs) (auto simp add: evaldjf_def djf_def Let_def split: fm.split)

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

fun conjuncts :: "fm \ fm list"
where
  "conjuncts (And p q) = (conjuncts p) @ (conjuncts q)"
| "conjuncts T = []"
| "conjuncts p = [p]"

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

lemma disjuncts_qf: "qfree p \ \ q\ 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 \ \ q\ 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 \ fm) \ fm \ fm" where
  "DJ f p \ evaldjf f (disjuncts p)"

lemma DJ: assumes fdj: "\ 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) = (\ q \ set (disjuncts p). Ifm bs (f q))"
    by (simp add: DJ_def evaldjf_ex)
  also have "\ = Ifm bs (f p)" using fdj fF by (induct p rule: disjuncts.induct, auto)
  finally show ?thesis .
qed

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

  from evaldjf_qf[OF th'] th show "qfree (DJ f p)" by simp
qed

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

  (* Algebraic simplifications for nums *)
fun bnds:: "num \ nat list"
where
  "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 = []"

fun lex_ns:: "nat list \ nat list \ bool"
where
  "lex_ns [] ms = True"
| "lex_ns ns [] = False"
| "lex_ns (n#ns) (m#ms) = (n ((n = m) \ lex_ns ns ms)) "
definition lex_bnd :: "num \ num \ bool" where
  "lex_bnd t s \ lex_ns (bnds t) (bnds s)"

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

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

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

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

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

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

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

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

declare dvd_trans [trans add]

lemma numgcd0:
  assumes g0: "numgcd t = 0"
  shows "Inum bs t = 0"
proof-
  have "\x. numgcdh t x= 0 \ 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 \ 0" shows "numgcdh t g \ 0"
  using gp by (induct t rule: numgcdh.induct) auto

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

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

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

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

lemma maxcoeff_ismaxcoeff: "ismaxcoeff t (maxcoeff t)"
proof (induct t rule: maxcoeff.induct)
  case (2 n c t)
  hence H:"ismaxcoeff t (maxcoeff t)" .
  have thh: "maxcoeff t \ max \c\ (maxcoeff t)" by simp
  from ismaxcoeff_mono[OF H thh] show ?case by simp
next
  case (3 c t s)
  hence H1:"ismaxcoeff s (maxcoeff s)" by auto
  have thh1: "maxcoeff s \ max \c\ (maxcoeff s)" by (simp add: max_def)
  from ismaxcoeff_mono[OF H1 thh1] show ?case by simp
qed simp_all

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

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

lemma dvdnumcoeff_aux:
  assumes "ismaxcoeff t m" and mp:"m \ 0" and "numgcdh t m > 1"
  shows "dvdnumcoeff t (numgcdh t m)"
using assms
proof(induct t rule: numgcdh.induct)
  case (2 n c t)
  let ?g = "numgcdh t m"
  from 2 have th:"gcd c ?g > 1" by simp
  from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
  have "(\c\ > 1 \ ?g > 1) \ (\c\ = 0 \ ?g > 1) \ (\c\ > 1 \ ?g = 0)" by simp
  moreover {assume "\c\ > 1" and gp: "?g > 1" with 2
    have th: "dvdnumcoeff t ?g" by simp
    have th': "gcd c ?g dvd ?g" by simp
    from dvdnumcoeff_trans[OF th' th] have ?case by simp }
  moreover {assume "\c\ = 0 \ ?g > 1"
    with 2 have th: "dvdnumcoeff t ?g" by simp
    have th': "gcd c ?g dvd ?g" by simp
    from dvdnumcoeff_trans[OF th' th] have ?case by simp
    hence ?case by simp }
  moreover {assume "\c\ > 1" and g0:"?g = 0"
    from numgcdh0[OF g0] have "m=0". with 2 g0 have ?case by simp }
  ultimately show ?case by blast
next
  case (3 c s t)
  let ?g = "numgcdh t m"
  from 3 have th:"gcd c ?g > 1" by simp
  from zgcd_gt1[OF th] numgcdh_pos[OF mp, where t="t"]
  have "(\c\ > 1 \ ?g > 1) \ (\c\ = 0 \ ?g > 1) \ (\c\ > 1 \ ?g = 0)" by simp
  moreover {assume "\c\ > 1" and gp: "?g > 1" with 3
    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 "\c\ = 0 \ ?g > 1"
    with 3 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 "\c\ > 1" and g0:"?g = 0"
    from numgcdh0[OF g0] have "m=0". with 3 g0 have ?case by simp }
  ultimately show ?case by blast
qed auto

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

lemma reducecoeff: "real_of_int (numgcd t) * (Inum bs (reducecoeff t)) = Inum bs t"
proof-
  let ?g = "numgcd t"
  have "?g \ 0" by (simp add: numgcd_pos)
  hence "?g = 0 \ ?g = 1 \ ?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 \ numbound0 (reducecoeffh t g)"
  by (induct t rule: reducecoeffh.induct) auto

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

consts numadd:: "num \ num \ num"
recdef numadd "measure (\(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)"
  by (induct t s rule: numadd.induct) (simp_all add: Let_def algebra_simps add_eq_0_iff)

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

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

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

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

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

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

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

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

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

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

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 "\" by (simp add: isint_add cti si)
  finally show ?thesis .
qed

fun split_int:: "num \ num \ num"
where
  "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: "\tv ti. split_int t = (tv,ti) \ (Inum bs (Add tv ti) = Inum bs t) \ 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 2(1) have b:"Inum bs (Add ?bv ?bi) = Inum bs b" and bii: "isint ?bi bs" by blast+
  from 2(2) have tibi: "ti = ?bi" by (simp add: Let_def split_def)
  from 2(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 3(1) have b:"Inum bs (Add ?bv ?bi) = Inum bs b" and bii: "isint ?bi bs" by blast+
  from 3(2) have tibi: "ti = CF c a ?bi"
    by (simp add: Let_def split_def)
  from 3(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 \ numbound0 (fst (split_int t)) \ numbound0 (snd (split_int t)) "
  by (induct t rule: split_int.induct) (auto simp add: Let_def split_def)

definition numfloor:: "num \ num"
where
  "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: "\ v. ?tv \ C v"
    hence th1: "?n t = ?N (Add (Floor ?tv) ?ti)"
      by (cases ?tv) (auto simp add: numfloor_def Let_def split_def)
    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_of_int \?N (Add ?tv ?ti)\" by simp
    also have "\ = real_of_int (\?N ?tv\ + \?N ?ti\)"
      by (simp,subst tii[simplified isint_iff, symmetric]) simp
    also have "\ = ?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_of_int \?N (Add ?tv ?ti)\" by simp
    also have "\ = real_of_int (\?N ?tv\ + \?N ?ti\)"
      by (simp,subst tii[simplified isint_iff, symmetric]) simp
    also have "\ = ?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) }
  ultimately show ?thesis by auto
qed

lemma numfloor_nb[simp]: "numbound0 t \ 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)

fun simpnum:: "num \ num"
where
  "simpnum (C j) = C j"
| "simpnum (Bound n) = CN n 1 (C 0)"
| "simpnum (Neg t) = numneg (simpnum t)"
| "simpnum (Add t s) = numadd (simpnum t,simpnum s)"
| "simpnum (Sub t s) = numsub (simpnum t) (simpnum s)"
| "simpnum (Mul i t) = (if i = 0 then (C 0) else nummul (simpnum t) i)"
| "simpnum (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 \ numbound0 (simpnum t)"
  by (induct t rule: simpnum.induct) auto

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

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

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

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

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

lemma split_int_nz: "nozerocoeff t \ nozerocoeff (fst (split_int t)) \ nozerocoeff (snd (split_int t))"
  by (induct t rule: split_int.induct) (auto simp add: Let_def split_def)

lemma numfloor_nz: "nozerocoeff t \ 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 \ maxcoeff t = 0 \ t = C 0"
proof (induct t rule: maxcoeff.induct)
  case (2 n c t)
  hence cnz: "c \0" and mx: "max \c\ (maxcoeff t) = 0" by simp+
  have "max \c\ (maxcoeff t) \ \c\" by simp
  with cnz have "max \c\ (maxcoeff t) > 0" by arith
  with 2 show ?case by simp
next
  case (3 c s t)
  hence cnz: "c \0" and mx: "max \c\ (maxcoeff t) = 0" by simp+
  have "max \c\ (maxcoeff t) \ \c\" by simp
  with cnz have "max \c\ (maxcoeff t) > 0" by arith
  with 3 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 \ int) \ num \ int" where
  "simp_num_pair \ (\ (t,n). (if n = 0 then (C 0, 0) else
   (let t' = simpnum t ; g = numgcd t' in
      if g > 1 then (let g' = gcd n g in
        if g' = 1 then (t',n)
        else (reducecoeffh t' g', n div g'))
      else (t',n))))"

lemma simp_num_pair_ci:
  shows "((\ (t,n). Inum bs t / real_of_int n) (simp_num_pair (t,n))) = ((\ (t,n). Inum bs t / real_of_int n) (t,n))"
  (is "?lhs = ?rhs")
proof-
  let ?t' = "simpnum t"
  let ?g = "numgcd ?t'"
  let ?g' = "gcd n ?g"
  {assume nz: "n = 0" hence ?thesis by (simp add: Let_def simp_num_pair_def)}
  moreover
  { assume nnz: "n \ 0"
    {assume "\ ?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' \ 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 \ ?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_of_int ?g' * ?t = Inum bs ?t'" by simp
        from nnz g1 g'1 have "?lhs = ?t / real_of_int (n div ?g')" by (simp add: simp_num_pair_def Let_def)
        also have "\ = (real_of_int ?g' * ?t) / (real_of_int ?g' * (real_of_int (n div ?g')))" by simp
        also have "\ = (Inum bs ?t' / real_of_int n)"
          using real_of_int_div[OF gpdd] th2 gp0 by simp
        finally have "?lhs = Inum bs t / real_of_int n" by simp
        then have ?thesis using nnz g1 g'1 by (simp add: simp_num_pair_def) }
      ultimately have ?thesis by auto }
    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' \ n' >0"
proof-
  let ?t' = "simpnum t"
  let ?g = "numgcd ?t'"
  let ?g' = "gcd n ?g"
  { assume nz: "n = 0" hence ?thesis using assms by (simp add: Let_def simp_num_pair_def) }
  moreover
  { assume nnz: "n \ 0"
    {assume "\ ?g > 1" hence ?thesis using assms 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' \ 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 \ ?g' > 1" by arith
      moreover {assume "?g'=1" hence ?thesis using assms g1 g0
          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 div_self[OF gp0]]
        have "n div ?g' >0" by simp
        hence ?thesis using assms g1 g'1
          by(auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0)}
      ultimately have ?thesis by auto }
    ultimately have ?thesis by blast }
  ultimately show ?thesis by blast
qed

fun not:: "fm \ fm"
where
  "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 \ qfree (not p)"
  by (induct p) auto
lemma not_nb[simp]: "bound0 p \ bound0 (not p)"
  by (induct p) auto

definition conj :: "fm \ fm \ fm" where
  "conj p q \ (if (p = F \ q=F) then F else if p=T then q else if q=T then p else
   if p = q then p else And p q)"
lemma conj[simp]: "Ifm bs (conj p q) = Ifm bs (And p q)"
  by (cases "p=F \ q=F", simp_all add: conj_def) (cases p, simp_all)

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

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

lemma disj[simp]: "Ifm bs (disj p q) = Ifm bs (Or p q)"
  by (cases "p=T \ q=T",simp_all add: disj_def) (cases p,simp_all)
lemma disj_qf[simp]: "\qfree p ; qfree q\ \ qfree (disj p q)"
  using disj_def by auto
lemma disj_nb[simp]: "\bound0 p ; bound0 q\ \ bound0 (disj p q)"
  using disj_def by auto

definition imp :: "fm \ fm \ fm" where
  "imp p q \ (if (p = F \ q=T \ p=q) then T else if p=T then q else if q=F then not p
    else Imp p q)"
lemma imp[simp]: "Ifm bs (imp p q) = Ifm bs (Imp p q)"
  by (cases "p=F \ q=T",simp_all add: imp_def)
lemma imp_qf[simp]: "\qfree p ; qfree q\ \ qfree (imp p q)"
  using imp_def by (cases "p=F \ q=T",simp_all add: imp_def)

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

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

lemma iff_qf[simp]: "\qfree p ; qfree q\ \ qfree (iff p q)"
  by (unfold iff_def,cases "p=q", auto)

fun check_int:: "num \ bool"
where
  "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 \ 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 \ 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_of_int \t\ = t \ 1 rdvd t"
  by (simp add: rdvd_def,rule_tac x="\t\" in exI) simp

lemma rdvd_reduce:
  assumes gd:"g dvd d" and gc:"g dvd c" and gp: "g > 0"
  shows "real_of_int (d::int) rdvd real_of_int (c::int)*t = (real_of_int (d div g) rdvd real_of_int (c div g)*t)"
proof
  assume d: "real_of_int d rdvd real_of_int c * t"
  from d rdvd_def obtain k where k_def: "real_of_int c * t = real_of_int d* real_of_int (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_of_int g * real_of_int kc * t = real_of_int g * real_of_int kd * real_of_int k" by simp
  hence "real_of_int kc * t = real_of_int kd * real_of_int k" using gp by simp
  hence th:"real_of_int kd rdvd real_of_int 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_of_int (d div g) rdvd real_of_int (c div g) * t" by simp
next
  assume d: "real_of_int (d div g) rdvd real_of_int (c div g) * t"
  from gp have gnz: "g \ 0" by simp
  thus "real_of_int d rdvd real_of_int c * t" using d rdvd_mult[OF gnz, where n="d div g" and x="real_of_int (c div g) * t"] real_of_int_div[OF gd] real_of_int_div[OF gc] by simp
qed

definition simpdvd :: "int \ num \ (int \ num)" where
  "simpdvd d t \
   (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 \ 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 "\ ?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' \ 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 \ ?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_of_int ?g' * ?t = Inum bs t" by simp
      from assms g1 g0 g'1
      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 "\ = (real_of_int d rdvd (Inum bs t))"
        using rdvd_reduce[OF gpdd gpdgp g'p, where t="?t", simplified div_self[OF gp0]]
          th2[symmetric] by simp
      finally have ?thesis by simp  }
    ultimately have ?thesis by auto
  }
  ultimately show ?thesis by blast
qed

fun simpfm :: "fm \ fm"
where
  "simpfm (And p q) = conj (simpfm p) (simpfm q)"
| "simpfm (Or p q) = disj (simpfm p) (simpfm q)"
| "simpfm (Imp p q) = imp (simpfm p) (simpfm q)"
| "simpfm (Iff p q) = iff (simpfm p) (simpfm q)"
| "simpfm (Not p) = not (simpfm p)"
| "simpfm (Lt a) = (let a' = simpnum a in case a' of C v \ if (v < 0) then T else F
    | _ \<Rightarrow> Lt (reducecoeff a'))"
| "simpfm (Le a) = (let a' = simpnum a in case a' of C v \ if (v \ 0) then T else F | _ \ Le (reducecoeff a'))"
| "simpfm (Gt a) = (let a' = simpnum a in case a' of C v \ if (v > 0) then T else F | _ \ Gt (reducecoeff a'))"
| "simpfm (Ge a) = (let a' = simpnum a in case a' of C v \ if (v \ 0) then T else F | _ \ Ge (reducecoeff a'))"
| "simpfm (Eq a) = (let a' = simpnum a in case a' of C v \ if (v = 0) then T else F | _ \ Eq (reducecoeff a'))"
| "simpfm (NEq a) = (let a' = simpnum a in case a' of C v \ if (v \ 0) then T else F | _ \ NEq (reducecoeff a'))"
| "simpfm (Dvd i a) = (if i=0 then simpfm (Eq a)
             else if (\<bar>i\<bar> = 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 (\<bar>i\<bar> = 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:"\ (\ 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_of_int ?g > 0" by simp
    have "Inum bs ?sa = real_of_int ?g* ?r" by (simp add: reducecoeff)
    with sa have "Inum bs a < 0 = (real_of_int ?g * ?r < real_of_int ?g * 0)" by simp
    also have "\ = (?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:"\ (\ 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_of_int ?g > 0" by simp
    have "Inum bs ?sa = real_of_int ?g* ?r" by (simp add: reducecoeff)
    with sa have "Inum bs a \ 0 = (real_of_int ?g * ?r \ real_of_int ?g * 0)" by simp
    also have "\ = (?r \ 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:"\ (\ 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_of_int ?g > 0" by simp
    have "Inum bs ?sa = real_of_int ?g* ?r" by (simp add: reducecoeff)
    with sa have "Inum bs a > 0 = (real_of_int ?g * ?r > real_of_int ?g * 0)" by simp
    also have "\ = (?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:"\ (\ 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_of_int ?g > 0" by simp
    have "Inum bs ?sa = real_of_int ?g* ?r" by (simp add: reducecoeff)
    with sa have "Inum bs a \ 0 = (real_of_int ?g * ?r \ real_of_int ?g * 0)" by simp
    also have "\ = (?r \ 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:"\ (\ 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_of_int ?g > 0" by simp
    have "Inum bs ?sa = real_of_int ?g* ?r" by (simp add: reducecoeff)
    with sa have "Inum bs a = 0 = (real_of_int ?g * ?r = 0)" by simp
    also have "\ = (?r = 0)" using gp
      by simp
    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:"\ (\ 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_of_int ?g > 0" by simp
    have "Inum bs ?sa = real_of_int ?g* ?r" by (simp add: reducecoeff)
    with sa have "Inum bs a \ 0 = (real_of_int ?g * ?r \ 0)" by simp
    also have "\ = (?r \ 0)" using gp
      by simp
    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 \ (\i\ = 1 \ check_int a) \ (i\0 \ ((\i\ \ 1) \ (\ 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: "\i\ = 1" and ai: "check_int a"
    hence "i=1 \ 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\0" and cond: "(\i\ \ 1) \ (\ check_int a)"
    {fix v assume "?sa = C v" hence ?case using sa[symmetric] inz cond
        by (cases "\i\ = 1", auto simp add: int_rdvd_iff) }
    moreover {assume H:"\ (\ 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 \ (\i\ = 1 \ check_int a) \ (i\0 \ ((\i\ \ 1) \ (\ 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: "\i\ = 1" and ai: "check_int a"
    hence "i=1 \ 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\0" and cond: "(\i\ \ 1) \ (\ check_int a)"
    {fix v assume "?sa = C v" hence ?case using sa[symmetric] inz cond
        by (cases "\i\ = 1", auto simp add: int_rdvd_iff) }
    moreover {assume H:"\ (\ 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 \ numbound0 (snd (simpdvd d t))"
  by (simp add: simpdvd_def Let_def split_def reducecoeffh_numbound0)

lemma simpfm_bound0[simp]: "bound0 p \ 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 \ 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 \ fm" where
  "list_conj ps \ foldr conj ps T"
lemma list_conj: "Ifm bs (list_conj ps) = (\p\ set ps. Ifm bs p)"
  by (induct ps, auto simp add: list_conj_def)
lemma list_conj_qf: " \p\ set ps. qfree p \ qfree (list_conj ps)"
  by (induct ps, auto simp add: list_conj_def)
lemma list_conj_nb: " \p\ set ps. bound0 p \ bound0 (list_conj ps)"
  by (induct ps, auto simp add: list_conj_def)
definition CJNB :: "(fm \ fm) \ fm \ fm" where
  "CJNB f p \ (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: "\ bs p. qfree p \ qfree (qe p) \ (Ifm bs (qe p) = Ifm bs (E p))"
  shows "\ bs p. qfree p \ qfree (CJNB qe p) \ (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 "\ q\ 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 " \q\ 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 split_def)
  {fix bs
    from conjuncts have "Ifm bs p = (\q\ set ?cjs. Ifm bs q)" by blast
    also have "\ = ((\q\ set ?yes. Ifm bs q) \ (\q\ set ?no. Ifm bs q))"
      using partition_set[OF part] by auto
    finally have "Ifm bs p = ((Ifm bs ?cyes) \ (Ifm bs ?cno))" using list_conj by simp}
  hence "Ifm bs (E p) = (\x. (Ifm (x#bs) ?cyes) \ (Ifm (x#bs) ?cno))" by simp
  also fix y have "\ = (\x. (Ifm (y#bs) ?cyes) \ (Ifm (x#bs) ?cno))"
    using bound0_I[OF yes_nb, where bs="bs" and b'="y"] by blast
  also have "\ = (Ifm bs (decr ?cyes) \ Ifm bs (E ?cno))"
    by (auto simp add: decr[OF yes_nb] simp del: partition_filter_conv)
  also have "\ = (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) \ Ifm bs (CJNB qe p) = Ifm bs (E p)" by blast
qed

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

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

text \<open>The \<open>\<int>\<close> Part\<close>
text\<open>Linearity for fm where Bound 0 ranges over \<open>\<int>\<close>\<close>

fun zsplit0 :: "num \ int \ num" (* splits the bounded from the unbounded part*)
where
  "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'))"

lemma zsplit0_I:
  shows "\ n a. zsplit0 t = (n,a) \ (Inum ((real_of_int (x::int)) #bs) (CN 0 n a) = Inum (real_of_int x #bs) t) \ numbound0 a"
  (is "\ n a. ?S t = (n,a) \ (?I x (CN 0 n a) = ?I x t) \ ?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 \ n=-?nt" using 5
    by (simp add: Let_def split_def)
  from abj 5 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) \ ?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
--> --------------------

--> maximum size reached

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

quality100%

¤ Dauer der Verarbeitung: 0.32 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.