Up to index of Isabelle/HOL/Decision_Procs
theory MIR(* Title: HOL/Decision_Procs/MIR.thy
Author: Amine Chaieb
*)
theory MIR
imports Complex_Main Dense_Linear_Order DP_Library
"~~/src/HOL/Library/Efficient_Nat" "~~/src/HOL/Library/Old_Recdef"
uses ("mir_tac.ML")
begin
section {* Quantifier elimination for @{text "\<real> (0, 1, +, floor, <)"} *}
declare real_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)
(* Maybe should be added to the library … *)
lemma floor_int_eq: "(real n≤ x ∧ x < real (n+1)) = (floor x = n)"
proof( auto)
assume lb: "real n ≤ x"
and ub: "x < real n + 1"
have "real (floor x) ≤ 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 ≤ 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 "∀x.∀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 => real => bool" (infixl "rdvd" 50)
where
rdvd_def: "x rdvd y <-> (∃k::int. y = x * real k)"
lemma int_rdvd_real:
shows "real (i::int) rdvd x = (i dvd (floor x) ∧ real (floor x) = x)" (is "?l = ?r")
proof
assume "?l"
hence th: "∃ 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 "∃ k. real (floor x) = real (i*k)" by simp
hence "∃ 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::int) dvd ⌊x::real⌋" ..
hence "∃ k. real (floor x) = real (i*k)"
by (simp only: real_of_int_inject) (simp add: dvd_def)
thus ?l using `?r` 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≠0"
shows "(real (n::int) * real (k::int) rdvd x * real k) = (real n rdvd x)"
using knz by (simp add:rdvd_def)
(*********************************************************************************)
(**** 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 => 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 => num => 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 ≡ 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 ==> 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 "… = real (c* ?fe)" by (simp only: floor_real_of_int)
also have "… = real 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 (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 "… = - 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 = "λ 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 "… = 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 "… = real (floor ?a) + real (floor ?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 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 => 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 => 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 i rdvd Inum bs b)"
| "Ifm bs (NDvd i b) = (¬(real 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)"
consts prep :: "fm => 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: "!! 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 => T | F => q | _ => 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 nb: "∀ x∈ set xs. bound0 (f x)"
shows "bound0 (evaldjf f xs)"
using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto)
lemma evaldjf_qf:
assumes nb: "∀ x∈ set xs. qfree (f x)"
shows "qfree (evaldjf f xs)"
using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto)
fun disjuncts :: "fm => fm list" where
"disjuncts (Or p q) = (disjuncts p) @ (disjuncts q)"
| "disjuncts F = []"
| "disjuncts p = [p]"
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<m ∨ ((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) = 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 ≥ 0"
apply (induct t rule: maxcoeff.induct, auto)
done
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_def: "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_def: "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 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 ≠ 0" by simp
from assms 1 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 ≠ 0" by simp
from assms 2 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 ≠ 0" by simp
from assms 3 show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps)
qed (auto simp add: numgcd_def gp)
fun ismaxcoeff:: "num => int => bool" where
"ismaxcoeff (C i) = (λ x. abs i ≤ x)"
| "ismaxcoeff (CN n c t) = (λx. abs c ≤ x ∧ (ismaxcoeff t x))"
| "ismaxcoeff (CF c s t) = (λx. abs 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 (abs c) (maxcoeff t)" by simp
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 ≤ max ¦c¦ (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) ==> ((abs i > 1 ∧ abs j > 1) ∨ (abs i = 0 ∧ abs j > 1) ∨ (abs i > 1 ∧ 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 ==> 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 "(abs c > 1 ∧ ?g > 1) ∨ (abs c = 0 ∧ ?g > 1) ∨ (abs c > 1 ∧ ?g = 0)" by simp
moreover {assume "abs 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 "abs 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 "abs 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 "(abs c > 1 ∧ ?g > 1) ∨ (abs c = 0 ∧ ?g > 1) ∨ (abs c > 1 ∧ ?g = 0)" by simp
moreover {assume "abs 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 "abs 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 "abs 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 (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 ≤ 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 ≤ 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]: "[| numbound0 t ; numbound0 s|] ==> numbound0 (numadd (t,s))"
by (induct t s rule: numadd.induct, auto simp 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 => numadd (tv,ti)
| _ => 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 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 "… = real (floor (?N ?tv) + (floor (?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 (floor (?N (Add ?tv ?ti)))" by simp
also have "… = real (floor (?N ?tv) + (floor (?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 numadd) }
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 numadd_nb)
function 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)"
by pat_completeness auto
termination by (relation "measure num_size") auto
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 (abs c) (maxcoeff t) = 0" by simp+
have "max (abs c) (maxcoeff t) ≥ abs c" by (simp add: le_maxI1)
with cnz have "max (abs 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 (abs c) (maxcoeff t) = 0" by simp+
have "max (abs c) (maxcoeff t) ≥ abs c" by (simp add: le_maxI1)
with cnz have "max (abs 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 n) (simp_num_pair (t,n))) = ((λ (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 ≠ 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 ?g' * ?t = Inum bs ?t'" by simp
from nnz g1 g'1 have "?lhs = ?t / real (n div ?g')" by (simp add: simp_num_pair_def Let_def)
also have "… = (real ?g' * ?t) / (real ?g' * (real (n div ?g')))" by simp
also have "… = (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 nnz g1 g'1 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' ∧ 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' ≤ n" .
from zdiv_mono1[OF g'n g'p, simplified zdiv_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 blast }
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 add:not)
(cases "not p= q", auto simp add:not)
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 ⌊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 (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 ≠ 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 => 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 ?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 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
function (sequential) simpfm :: "fm => fm" where
"simpfm (And p q) = conj (simpfm p) (simpfm q)"
| "simpfm (Or p q) = disj (simpfm p) (simpfm q)"
| "simpfm (Imp p q) = imp (simpfm p) (simpfm q)"
| "simpfm (Iff p q) = iff (simpfm p) (simpfm q)"
| "simpfm (NOT p) = not (simpfm p)"
| "simpfm (Lt a) = (let a' = simpnum a in case a' of C v => if (v < 0) then T else F
| _ => Lt (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 (abs i = 1) ∧ check_int a then T
else let a' = simpnum a in case a' of C v => if (i dvd v) then T else F | _ => (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) ∧ check_int a then F
else let a' = simpnum a in case a' of C v => if (¬(i dvd v)) then T else F | _ => (let (d,t) = simpdvd i a' in NDvd d t))"
| "simpfm p = p"
by pat_completeness auto
termination by (relation "measure fmsize") auto
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 ?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 "… = (?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 ?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 "… = (?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 ?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 "… = (?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 ?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 "… = (?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 ?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 "… = (?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:"¬ (∃ 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 "… = (?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 (12 i a) let ?sa = "simpnum a" have sa: "Inum bs ?sa = Inum bs a" by simp
have "i=0 ∨ (abs i = 1 ∧ check_int a) ∨ (i≠0 ∧ ((abs 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: "abs 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: "(abs i ≠ 1) ∨ (¬ 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:"¬ (∃ 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 ∨ (abs i = 1 ∧ check_int a) ∨ (i≠0 ∧ ((abs 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: "abs 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: "(abs i ≠ 1) ∨ (¬ 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:"¬ (∃ 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 conj_qf 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
function (sequential) 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)"
by pat_completeness auto
termination by (relation "measure fmsize") auto
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 {* The @{text "\<int>"} Part *}
text{* Linearity for fm where Bound 0 ranges over @{text "\<int>"} *}
function 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'))"
by pat_completeness auto
termination by (relation "measure num_size") auto
lemma zsplit0_I:
shows "!! n a. zsplit0 t = (n,a) ==> (Inum ((real (x::int)) #bs) (CN 0 n a) = Inum (real 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
ultimately have th: "a=Add ?as ?at ∧ n=?ns + ?nt" using 6
by (simp add: Let_def split_def)
from abjs[symmetric] have bluddy: "∃ x y. (x,y) = zsplit0 s" by blast
from 6 have "(∃ x y. (x,y) = zsplit0 s) --> (∀xa xb. zsplit0 t = (xa, xb) --> Inum (real x # bs) (CN 0 xa xb) = Inum (real x # bs) t ∧ numbound0 xb)" by blast (*FIXME*)
with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) ∧ ?N ?at" by blast
from abjs 6 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) ∧ ?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 ∧ n=?ns - ?nt" using 7
by (simp add: Let_def split_def)
from abjs[symmetric] have bluddy: "∃ x y. (x,y) = zsplit0 s" by blast
from 7 have "(∃ x y. (x,y) = zsplit0 s) --> (∀xa xb. zsplit0 t = (xa, xb) --> Inum (real x # bs) (CN 0 xa xb) = Inum (real x # bs) t ∧ numbound0 xb)" by blast (*FIXME*)
with bluddy abjt have th3: "(?I x (CN 0 ?nt ?at) = ?I x t) ∧ ?N ?at" by blast
from abjs 7 have th2: "(?I x (CN 0 ?ns ?as) = ?I x s) ∧ ?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 ∧ n=i*?nt" using 8
by (simp add: Let_def split_def)
from abj 8 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) ∧ ?N ?at" by blast
hence "?I x (Mul i t) = (real i) * ?I x (CN 0 ?nt ?at)" by simp
also have "… = ?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 ∧ n=?nt" using 9
by (simp add: Let_def split_def)
from abj 9 have th2: "(?I x (CN 0 ?nt ?at) = ?I x t) ∧ ?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 "… = real (floor ((real ?nt)* real(x) + ?I x ?at))" by simp
also have "… = real (floor (?I x ?at + real (?nt* x)))" by (simp add: add_ac)
also have "… = real (floor (?I x ?at) + (?nt* x))"
using floor_add[where x="?I x ?at" and a="?nt* x"] by simp
also have "… = 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 => real list => bool" (* Linearity test for fm *)
zlfm :: "fm => fm" (* Linearity transformation for fm *)
recdef iszlfm "measure size"
"iszlfm (And p q) = (λ bs. iszlfm p bs ∧ iszlfm q bs)"
"iszlfm (Or p q) = (λ bs. iszlfm p bs ∧ iszlfm q bs)"
"iszlfm (Eq (CN 0 c e)) = (λ bs. c>0 ∧ numbound0 e ∧ isint e bs)"
"iszlfm (NEq (CN 0 c e)) = (λ bs. c>0 ∧ numbound0 e ∧ isint e bs)"
"iszlfm (Lt (CN 0 c e)) = (λ bs. c>0 ∧ numbound0 e ∧ isint e bs)"
"iszlfm (Le (CN 0 c e)) = (λ bs. c>0 ∧ numbound0 e ∧ isint e bs)"
"iszlfm (Gt (CN 0 c e)) = (λ bs. c>0 ∧ numbound0 e ∧ isint e bs)"
"iszlfm (Ge (CN 0 c e)) = (λ bs. c>0 ∧ numbound0 e ∧ isint e bs)"
"iszlfm (Dvd i (CN 0 c e)) =
(λ bs. c>0 ∧ i>0 ∧ numbound0 e ∧ isint e bs)"
"iszlfm (NDvd i (CN 0 c e))=
(λ bs. c>0 ∧ i>0 ∧ numbound0 e ∧ isint e bs)"
"iszlfm p = (λ bs. isatom p ∧ (bound0 p))"
lemma zlin_qfree: "iszlfm p bs ==> qfree p"
by (induct p rule: iszlfm.induct) auto
lemma iszlfm_gen:
assumes lp: "iszlfm p (x#bs)"
shows "∀ 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 ==> iszlfm q bs ==> iszlfm (conj p q) bs"
using conj_def by (cases p,auto)
lemma disj_zl[simp]: "iszlfm p bs ==> iszlfm q bs ==> iszlfm (disj p q) bs"
using disj_def by (cases p,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 ∨ (a = floor b ∧ real (floor b) < b))"
proof( auto)
assume alb: "real a < b" and agb: "¬ a < floor b"
from agb have "floor b ≤ 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) ≤ 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 ∨ (real a - real (floor (-b)) = 0 ∧ 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 ∨ (real a + real (floor b) = 0 ∧ real (floor b) - b < 0))"
proof-
have th: "(real a + b >0) = (real (-a) + (-b)< 0)" by arith
show ?thesis using myless[of _ "real (floor b)"]
by (simp only:th split_int_less_real'[where a="-a" and b="-b"])
(simp add: algebra_simps diff_minus[symmetric],arith)
qed
lemma split_int_le_real:
"(real (a::int) ≤ b) = (a ≤ floor b ∨ (a = floor b ∧ real (floor b) < b))"
proof( auto)
assume alb: "real a ≤ b" and agb: "¬ a ≤ floor b"
from alb have "floor (real a) ≤ floor b " by (simp only: floor_mono)
hence "a ≤ floor b" by simp with agb show "False" by simp
next
assume alb: "a ≤ floor b"
hence "real a ≤ real (floor b)" by (simp only: floor_mono)
also have "…≤ b" by simp finally show "real a ≤ b" .
qed
lemma split_int_le_real':
"(real (a::int) + b ≤ 0) = (real a - real (floor(-b)) ≤ 0 ∨ (real a - real (floor (-b)) = 0 ∧ real (floor (-b)) + b < 0))"
proof-
have "(real a + b ≤0) = (real a ≤ -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 ≥ 0) = (real a + real (floor b) ≥ 0 ∨ (real a + real (floor b) = 0 ∧ real (floor b) - b < 0))"
proof-
have th: "(real a + b ≥0) = (real (-a) + (-b) ≤ 0)" by arith
show ?thesis by (simp only: th split_int_le_real'[where a="-a" and b="-b"])
(simp add: algebra_simps diff_minus[symmetric],arith)
qed
lemma split_int_eq_real: "(real (a::int) = b) = ( a = floor b ∧ b = real (floor b))" (is "?l = ?r")
by auto
lemma split_int_eq_real': "(real (a::int) + b = 0) = ( a - floor (-b) = 0 ∧ 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) ∧ iszlfm (zlfm p) (real (i::int) #bs)"
(is "(?I (?l p) = ?I p) ∧ ?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 = "λ t. Inum (real i#bs) t"
have "?c = 0 ∨ (?c >0 ∧ ?c≠0) ∨ (?c<0 ∧ ?c≠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≠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 "… = (?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_minus)
finally have ?case using l by simp}
moreover
{assume cn: "?c < 0" and cnz: "?c≠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 "… = (?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_minus[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 = "λ t. Inum (real i#bs) t"
have "?c = 0 ∨ (?c >0 ∧ ?c≠0) ∨ (?c<0 ∧ ?c≠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≠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) ≤ 0)" using Ia by (simp add: Let_def split_def)
also have "… = (?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_minus)
finally have ?case using l by simp}
moreover
{assume cn: "?c < 0" and cnz: "?c≠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) ≤ 0)" using Ia by (simp add: Let_def split_def)
also from cn cnz have "… = (?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_minus[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 = "λ t. Inum (real i#bs) t"
have "?c = 0 ∨ (?c >0 ∧ ?c≠0) ∨ (?c<0 ∧ ?c≠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≠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 "… = (?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_minus)
finally have ?case using l by simp}
moreover
{assume cn: "?c < 0" and cnz: "?c≠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 "… = (?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_minus[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 = "λ t. Inum (real i#bs) t"
have "?c = 0 ∨ (?c >0 ∧ ?c≠0) ∨ (?c<0 ∧ ?c≠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≠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) ≥ 0)" using Ia by (simp add: Let_def split_def)
also have "… = (?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_minus)
finally have ?case using l by simp}
moreover
{assume cn: "?c < 0" and cnz: "?c≠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) ≥ 0)" using Ia by (simp add: Let_def split_def)
also from cn cnz have "… = (?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_minus[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 = "λ t. Inum (real i#bs) t"
have "?c = 0 ∨ (?c >0 ∧ ?c≠0) ∨ (?c<0 ∧ ?c≠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≠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 "… = (?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≠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 "… = (?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 = "λ t. Inum (real i#bs) t"
have "?c = 0 ∨ (?c >0 ∧ ?c≠0) ∨ (?c<0 ∧ ?c≠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≠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) ≠ 0)" using Ia by (simp add: Let_def split_def)
also have "… = (?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≠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) ≠ 0)" using Ia by (simp add: Let_def split_def)
also from cn cnz have "… = (?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 = "λ t. Inum (real i#bs) t"
have "j=0 ∨ (j≠0 ∧ ?c = 0) ∨ (j≠0 ∧ ?c >0 ∧ ?c≠0) ∨ (j≠ 0 ∧ ?c<0 ∧ ?c≠0)" by arith
moreover
{ assume j: "j=0" hence z: "zlfm (Dvd j a) = (zlfm (Eq a))" by (simp add: Let_def)
hence ?case using 11 j by (simp del: zlfm.simps add: rdvd_left_0_eq)}
moreover
{assume "?c=0" and "j≠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≠0" and jnz: "j≠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 "… = (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 "… = ((abs j) dvd (floor ((?N ?r) + real (?c*i))) ∧
(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 "… = (?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≠0" and jnz: "j≠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 "… = (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 "… = ((abs j) dvd (floor ((?N ?r) + real (?c*i))) ∧
(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 "… = (?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 = "λ t. Inum (real i#bs) t"
have "j=0 ∨ (j≠0 ∧ ?c = 0) ∨ (j≠0 ∧ ?c >0 ∧ ?c≠0) ∨ (j≠ 0 ∧ ?c<0 ∧ ?c≠0)" by arith
moreover
{assume j: "j=0" hence z: "zlfm (NDvd j a) = (zlfm (NEq a))" by (simp add: Let_def)
hence ?case using 12 j by (simp del: zlfm.simps add: rdvd_left_0_eq)}
moreover
{assume "?c=0" and "j≠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≠0" and jnz: "j≠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) = (¬ (real j rdvd (real (?c * i) + (?N ?r))))"
using Ia by (simp add: Let_def split_def)
also have "… = (¬ (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 "… = (¬ ((abs j) dvd (floor ((?N ?r) + real (?c*i))) ∧
(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 "… = (?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≠0" and jnz: "j≠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) = (¬ (real j rdvd (real (?c * i) + (?N ?r))))"
using Ia by (simp add: Let_def split_def)
also have "… = (¬ (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 "… = (¬ ((abs j) dvd (floor ((?N ?r) + real (?c*i))) ∧
(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 "… = (?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 "+∞"}
minusinf: Virtual substitution of @{text "-∞"}
@{text "δ"} Compute lcm @{text "d| Dvd d c*x+t ∈ p"}
@{text "dδ"} checks if a given l divides all the ds above*}
fun minusinf:: "fm => fm" where
"minusinf (And p q) = conj (minusinf p) (minusinf q)"
| "minusinf (Or p q) = disj (minusinf p) (minusinf q)"
| "minusinf (Eq (CN 0 c e)) = F"
| "minusinf (NEq (CN 0 c e)) = T"
| "minusinf (Lt (CN 0 c e)) = T"
| "minusinf (Le (CN 0 c e)) = T"
| "minusinf (Gt (CN 0 c e)) = F"
| "minusinf (Ge (CN 0 c e)) = F"
| "minusinf p = p"
lemma minusinf_qfree: "qfree p ==> qfree (minusinf p)"
by (induct p rule: minusinf.induct, auto)
fun plusinf:: "fm => fm" where
"plusinf (And p q) = conj (plusinf p) (plusinf q)"
| "plusinf (Or p q) = disj (plusinf p) (plusinf q)"
| "plusinf (Eq (CN 0 c e)) = F"
| "plusinf (NEq (CN 0 c e)) = T"
| "plusinf (Lt (CN 0 c e)) = F"
| "plusinf (Le (CN 0 c e)) = F"
| "plusinf (Gt (CN 0 c e)) = T"
| "plusinf (Ge (CN 0 c e)) = T"
| "plusinf p = p"
fun δ :: "fm => int" where
"δ (And p q) = lcm (δ p) (δ q)"
| "δ (Or p q) = lcm (δ p) (δ q)"
| "δ (Dvd i (CN 0 c e)) = i"
| "δ (NDvd i (CN 0 c e)) = i"
| "δ p = 1"
fun dδ :: "fm => int => bool" where
"dδ (And p q) = (λ d. dδ p d ∧ dδ q d)"
| "dδ (Or p q) = (λ d. dδ p d ∧ dδ q d)"
| "dδ (Dvd i (CN 0 c e)) = (λ d. i dvd d)"
| "dδ (NDvd i (CN 0 c e)) = (λ d. i dvd d)"
| "dδ p = (λ d. True)"
lemma delta_mono:
assumes lin: "iszlfm p bs"
and d: "d dvd d'"
and ad: "dδ p d"
shows "dδ 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 δ : assumes lin:"iszlfm p bs"
shows "dδ p (δ p) ∧ δ p >0"
using lin
proof (induct p rule: iszlfm.induct)
case (1 p q)
let ?d = "δ (And p q)"
from 1 lcm_pos_int have dp: "?d >0" by simp
have d1: "δ p dvd δ (And p q)" using 1 by simp
hence th: "dδ p ?d"
using delta_mono 1 by (simp only: iszlfm.simps) blast
have "δ q dvd δ (And p q)" using 1 by simp
hence th': "dδ q ?d" using delta_mono 1 by (simp only: iszlfm.simps) blast
from th th' dp show ?case by simp
next
case (2 p q)
let ?d = "δ (And p q)"
from 2 lcm_pos_int have dp: "?d >0" by simp
have "δ p dvd δ (And p q)" using 2 by simp
hence th: "dδ p ?d" using delta_mono 2 by (simp only: iszlfm.simps) blast
have "δ q dvd δ (And p q)" using 2 by simp
hence th': "dδ q ?d" using delta_mono 2 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 "∃ (z::int). ∀ x < z. Ifm ((real x)#bs) (minusinf p) = Ifm ((real x)#bs) p"
(is "?P p" is "∃ (z::int). ∀ x < z. ?I x (?M p) = ?I x p")
using linp
proof (induct p rule: minusinf.induct)
case (1 f g)
then have "?P f" by simp
then obtain z1 where z1_def: "∀ x < z1. ?I x (?M f) = ?I x f" by blast
with 1 have "?P g" by simp
then obtain z2 where z2_def: "∀ x < z2. ?I x (?M g) = ?I x g" by blast
let ?z = "min z1 z2"
from z1_def z2_def have "∀ x < ?z. ?I x (?M (And f g)) = ?I x (And f g)" by simp
thus ?case by blast
next
case (2 f g)
then have "?P f" by simp
then obtain z1 where z1_def: "∀ x < z1. ?I x (?M f) = ?I x f" by blast
with 2 have "?P g" by simp
then obtain z2 where z2_def: "∀ x < z2. ?I x (?M g) = ?I x g" by blast
let ?z = "min z1 z2"
from z1_def z2_def have "∀ x < ?z. ?I x (?M (Or f g)) = ?I x (Or f g)" by simp
thus ?case by blast
next
case (3 c e)
then have "c > 0" by simp
hence rcpos: "real c > 0" by simp
from 3 have nbe: "numbound0 e" by simp
fix y
have "∀ 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::real) ≤ - (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: mult_strict_left_mono [OF th1 rcpos])
hence "real c * real x + Inum (y # bs) e ≠ 0"using rcpos by simp
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"] by simp
qed
thus ?case by blast
next
case (4 c e)
then have "c > 0" by simp hence rcpos: "real c > 0" by simp
from 4 have nbe: "numbound0 e" by simp
fix y
have "∀ 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::real) ≤ - (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: mult_strict_left_mono [OF th1 rcpos])
hence "real c * real x + Inum (y # bs) e ≠ 0"using rcpos by simp
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"] by simp
qed
thus ?case by blast
next
case (5 c e)
then have "c > 0" by simp hence rcpos: "real c > 0" by simp
from 5 have nbe: "numbound0 e" by simp
fix y
have "∀ 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::real) ≤ - (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: mult_strict_left_mono [OF th1 rcpos])
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)
then have "c > 0" by simp hence rcpos: "real c > 0" by simp
from 6 have nbe: "numbound0 e" by simp
fix y
have "∀ 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::real) ≤ - (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: mult_strict_left_mono [OF th1 rcpos])
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 (7 c e)
then have "c > 0" by simp hence rcpos: "real c > 0" by simp
from 7 have nbe: "numbound0 e" by simp
fix y
have "∀ 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::real) ≤ - (Inum (y # bs) e / real c)"