# HG changeset patch # User wenzelm # Date 1393431127 -3600 # Node ID 72c6ce5aea2ac46a6516616ff3a633a6decd7c85 # Parent 96ddf9bf12ac8c4933481acaabe19a3fff92293d tuned specifications and proofs; diff -r 96ddf9bf12ac -r 72c6ce5aea2a src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Wed Feb 26 14:59:24 2014 +0100 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Wed Feb 26 17:12:07 2014 +0100 @@ -158,30 +158,46 @@ else []!(m - (length xs - 1)))" proof (induct xs arbitrary: n m) case Nil - thus ?case by simp + then show ?case by simp next case (Cons x xs n m) - {assume nxs: "n \ length (x#xs)" hence ?case using removen_same[OF nxs] by simp} + { + assume nxs: "n \ length (x#xs)" + then have ?case using removen_same[OF nxs] by simp + } moreover - {assume nxs: "\ (n \ length (x#xs))" - {assume mln: "m < n" hence ?case using Cons by (cases m, auto)} + { + assume nxs: "\ (n \ length (x#xs))" + { + assume mln: "m < n" + then have ?case using Cons by (cases m) auto + } moreover - {assume mln: "\ (m < n)" - {assume mxs: "m \ length (x#xs)" hence ?case using Cons by (cases m, auto)} + { + assume mln: "\ (m < n)" + { + assume mxs: "m \ length (x#xs)" + then have ?case using Cons by (cases m) auto + } moreover - {assume mxs: "\ (m \ length (x#xs))" + { + assume mxs: "\ (m \ length (x#xs))" have th: "length (removen n (x#xs)) = length xs" using removen_length[where n="n" and xs="x#xs"] nxs by simp - with mxs have mxs':"m \ length (removen n (x#xs))" by auto - hence "(removen n (x#xs))!m = [] ! (m - length xs)" + with mxs have mxs':"m \ length (removen n (x#xs))" + by auto + then have "(removen n (x#xs))!m = [] ! (m - length xs)" using th nth_length_exceeds[OF mxs'] by auto - hence th: "(removen n (x#xs))!m = [] ! (m - (length (x#xs) - 1))" + then have th: "(removen n (x#xs))!m = [] ! (m - (length (x#xs) - 1))" by auto - hence ?case using nxs mln mxs by auto } + then have ?case + using nxs mln mxs by auto + } ultimately have ?case by blast } ultimately have ?case by blast - } ultimately show ?case by blast + } + ultimately show ?case by blast qed lemma decrtm: @@ -243,7 +259,7 @@ (* Simplification *) consts tmadd:: "tm \ tm \ tm" -recdef tmadd "measure (\ (t,s). size t + size s)" +recdef tmadd "measure (\(t,s). size t + size s)" "tmadd (CNP n1 c1 r1,CNP n2 c2 r2) = (if n1 = n2 then let c = c1 +\<^sub>p c2 @@ -278,9 +294,9 @@ fun tmmul:: "tm \ poly \ tm" where - "tmmul (CP j) = (\ i. CP (i *\<^sub>p j))" -| "tmmul (CNP n c a) = (\ i. CNP n (i *\<^sub>p c) (tmmul a i))" -| "tmmul t = (\ i. Mul i t)" + "tmmul (CP j) = (\i. CP (i *\<^sub>p j))" +| "tmmul (CNP n c a) = (\i. CNP n (i *\<^sub>p c) (tmmul a i))" +| "tmmul t = (\i. Mul i t)" lemma tmmul[simp]: "Itm vs bs (tmmul t i) = Itm vs bs (Mul i t)" by (induct t arbitrary: i rule: tmmul.induct) (simp_all add: field_simps) @@ -362,8 +378,7 @@ done lemma simptm_ci[simp]: "Itm vs bs (simptm t) = Itm vs bs t" - by (induct t rule: simptm.induct) - (auto simp add: tmneg tmadd tmsub tmmul Let_def polynate_stupid) + by (induct t rule: simptm.induct) (auto simp add: Let_def polynate_stupid) lemma simptm_tmbound0[simp]: "tmbound0 t \ tmbound0 (simptm t)" by (induct t rule: simptm.induct) (auto simp add: Let_def) @@ -422,9 +437,10 @@ proof - fix c' t' assume "split0 t = (c', t')" - hence "c' = fst (split0 t)" and "t' = snd (split0 t)" + then have "c' = fst (split0 t)" and "t' = snd (split0 t)" by auto - with split0[where t="t" and bs="bs"] show "Itm vs bs t = Itm vs bs (CNP 0 c' t')" + with split0[where t="t" and bs="bs"] + show "Itm vs bs t = Itm vs bs (CNP 0 c' t')" by simp qed @@ -434,7 +450,7 @@ proof - fix c' t' assume "split0 t = (c', t')" - hence "c' = fst (split0 t)" and "t' = snd (split0 t)" + then have "c' = fst (split0 t)" and "t' = snd (split0 t)" by auto with conjunct1[OF split0[where t="t"]] show "tmbound 0 t'" by simp @@ -498,7 +514,8 @@ by (induct p rule: fmsize.induct) simp_all (* Semantics of formulae (fm) *) -primrec Ifm ::"'a::{linordered_field_inverse_zero} list \ 'a list \ fm \ bool" where +primrec Ifm ::"'a::{linordered_field_inverse_zero} list \ 'a list \ fm \ bool" +where "Ifm vs bs T = True" | "Ifm vs bs F = False" | "Ifm vs bs (Lt a) = (Itm vs bs a < 0)" @@ -513,7 +530,8 @@ | "Ifm vs bs (E p) = (\x. Ifm vs (x#bs) p)" | "Ifm vs bs (A p) = (\x. Ifm vs (x#bs) p)" -fun not:: "fm \ fm" where +fun not:: "fm \ fm" +where "not (NOT (NOT p)) = not p" | "not (NOT p) = p" | "not T = F" @@ -549,7 +567,7 @@ else Or p q)" lemma disj[simp]: "Ifm vs bs (disj p q) = Ifm vs bs (Or p q)" - by (cases "p=T \ q=T", simp_all add: disj_def) (cases p, simp_all) + by (cases "p = T \ q = T", simp_all add: disj_def) (cases p, simp_all) definition imp :: "fm \ fm \ fm" where @@ -560,7 +578,7 @@ else Imp p q)" lemma imp[simp]: "Ifm vs bs (imp p q) = Ifm vs bs (Imp p q)" - by (cases "p=F \ q=T") (simp_all add: imp_def) + by (cases "p = F \ q = T") (simp_all add: imp_def) definition iff :: "fm \ fm \ fm" where @@ -574,7 +592,7 @@ else Iff p q)" lemma iff[simp]: "Ifm vs bs (iff p q) = Ifm vs bs (Iff p q)" - by (unfold iff_def,cases "p=q", simp,cases "p=NOT q", simp) (cases "NOT p= q", auto) + by (unfold iff_def, cases "p = q", simp, cases "p = NOT q", simp) (cases "NOT p= q", auto) (* Quantifier freeness *) fun qfree:: "fm \ bool" @@ -593,10 +611,10 @@ where "boundslt n T = True" | "boundslt n F = True" -| "boundslt n (Lt t) = (tmboundslt n t)" -| "boundslt n (Le t) = (tmboundslt n t)" -| "boundslt n (Eq t) = (tmboundslt n t)" -| "boundslt n (NEq t) = (tmboundslt n t)" +| "boundslt n (Lt t) = tmboundslt n t" +| "boundslt n (Le t) = tmboundslt n t" +| "boundslt n (Eq t) = tmboundslt n t" +| "boundslt n (NEq t) = tmboundslt n t" | "boundslt n (NOT p) = boundslt n p" | "boundslt n (And p q) = (boundslt n p \ boundslt n q)" | "boundslt n (Or p q) = (boundslt n p \ boundslt n q)" @@ -656,7 +674,7 @@ and nb: "bound (Suc n) p" and le: "Suc n \ length (y#bs)" by simp+ from E.hyps[OF bnd nb le tmbound_I] have "Ifm vs ((y#bs)[Suc n:=x]) p = Ifm vs (y#bs) p" . } - thus ?case by simp + then show ?case by simp next case (A p bs n) { @@ -667,10 +685,11 @@ by simp_all from A.hyps[OF bnd nb le tmbound_I] have "Ifm vs ((y#bs)[Suc n:=x]) p = Ifm vs (y#bs) p" . } - thus ?case by simp + then show ?case by simp qed auto -fun decr0 :: "fm \ fm" where +fun decr0 :: "fm \ fm" +where "decr0 (Lt a) = Lt (decrtm0 a)" | "decr0 (Le a) = Le (decrtm0 a)" | "decr0 (Eq a) = Eq (decrtm0 a)" @@ -721,7 +740,7 @@ from E(1)[OF bnd nb nle] have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p" . } - thus ?case by auto + then show ?case by auto next case (A p bs m) { fix x @@ -733,7 +752,7 @@ from A(1)[OF bnd nb nle] have "Ifm vs (removen (Suc m) (x#bs)) (decr (Suc m) p) = Ifm vs (x#bs) p" . } - thus ?case by auto + then show ?case by auto qed (auto simp add: decrtm removen_nth) primrec subst0 :: "tm \ fm \ fm" @@ -795,12 +814,14 @@ from E have nlm: "Suc n \ length (x#bs)" by simp from E(1)[OF bn nlm] - have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = Ifm vs ((x#bs)[Suc n:= Itm vs (x#bs) (incrtm0 t)]) p" + have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = + Ifm vs ((x#bs)[Suc n:= Itm vs (x#bs) (incrtm0 t)]) p" by simp - hence "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = Ifm vs (x#bs[n:= Itm vs bs t]) p" + then have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = + Ifm vs (x#bs[n:= Itm vs bs t]) p" by (simp add: incrtm0[where x="x" and bs="bs" and t="t"]) } - thus ?case by simp + then show ?case by simp next case (A p bs n) { @@ -810,12 +831,14 @@ from A have nlm: "Suc n \ length (x#bs)" by simp from A(1)[OF bn nlm] - have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = Ifm vs ((x#bs)[Suc n:= Itm vs (x#bs) (incrtm0 t)]) p" + have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = + Ifm vs ((x#bs)[Suc n:= Itm vs (x#bs) (incrtm0 t)]) p" by simp - hence "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = Ifm vs (x#bs[n:= Itm vs bs t]) p" + then have "Ifm vs (x#bs) (subst (Suc n) (incrtm0 t) p) = + Ifm vs (x#bs[n:= Itm vs bs t]) p" by (simp add: incrtm0[where x="x" and bs="bs" and t="t"]) } - thus ?case by simp + then show ?case by simp qed (auto simp add: tmsubst) lemma subst_nb: @@ -852,11 +875,11 @@ using disj_def by auto lemma imp_qf[simp]: "qfree p \ qfree q \ qfree (imp p q)" - using imp_def by (cases "p=F \ q=T") (simp_all add: imp_def) + using imp_def by (cases "p = F \ q = T") (simp_all add: imp_def) lemma imp_nb0[simp]: "bound0 p \ bound0 q \ bound0 (imp p q)" - using imp_def by (cases "p=F \ q=T \ p=q") (simp_all add: imp_def) + using imp_def by (cases "p = F \ q = T \ p = q") (simp_all add: imp_def) lemma imp_nb[simp]: "bound n p \ bound n q \ bound n (imp p q)" - using imp_def by (cases "p=F \ q=T \ p=q") (simp_all add: imp_def) + using imp_def by (cases "p = F \ q = T \ p = q") (simp_all add: imp_def) lemma imp_blt[simp]: "boundslt n p \ boundslt n q \ boundslt n (imp p q)" using imp_def by auto @@ -895,7 +918,7 @@ where "evaldjf f ps \ foldr (djf f) ps F" lemma djf_Or: "Ifm vs bs (djf f p q) = Ifm vs bs (Or (f p) q)" - by (cases "q=T", simp add: djf_def,cases "q=F",simp add: djf_def) + 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 vs bs (evaldjf f ps) \ (\p \ set ps. Ifm vs bs (f p))" @@ -923,89 +946,109 @@ lemma disjuncts_nb: "bound0 p \ \q \ set (disjuncts p). bound0 q" proof - assume nb: "bound0 p" - hence "list_all bound0 (disjuncts p)" - by (induct p rule:disjuncts.induct,auto) - thus ?thesis by (simp only: list_all_iff) + then have "list_all bound0 (disjuncts p)" + by (induct p rule:disjuncts.induct) auto + then show ?thesis + by (simp only: list_all_iff) qed lemma disjuncts_qf: "qfree p \ \q\ set (disjuncts p). qfree q" proof- assume qf: "qfree p" - hence "list_all qfree (disjuncts p)" - by (induct p rule: disjuncts.induct, auto) - thus ?thesis by (simp only: list_all_iff) + then have "list_all qfree (disjuncts p)" + by (induct p rule: disjuncts.induct) auto + then show ?thesis by (simp only: list_all_iff) qed -definition DJ :: "(fm \ fm) \ fm \ fm" where - "DJ f p \ evaldjf f (disjuncts p)" - -lemma DJ: assumes fdj: "\p q. Ifm vs bs (f (Or p q)) = Ifm vs bs (Or (f p) (f q))" - and fF: "f F = F" +definition DJ :: "(fm \ fm) \ fm \ fm" + where "DJ f p \ evaldjf f (disjuncts p)" + +lemma DJ: + assumes fdj: "\p q. Ifm vs bs (f (Or p q)) = Ifm vs bs (Or (f p) (f q))" + and fF: "f F = F" shows "Ifm vs bs (DJ f p) = Ifm vs bs (f p)" -proof- +proof - have "Ifm vs bs (DJ f p) = (\q \ set (disjuncts p). Ifm vs bs (f q))" by (simp add: DJ_def evaldjf_ex) - also have "\ = Ifm vs bs (f p)" using fdj fF by (induct p rule: disjuncts.induct, auto) + also have "\ = Ifm vs 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) +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 + 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 vs bs (qe p) = Ifm vs bs (E p))" +lemma DJ_qe: + assumes qe: "\bs p. qfree p \ qfree (qe p) \ (Ifm vs bs (qe p) = Ifm vs bs (E p))" shows "\bs p. qfree p \ qfree (DJ qe p) \ (Ifm vs bs ((DJ qe p)) = Ifm vs bs (E p))" -proof(clarify) - fix p::fm and bs +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 vs bs (DJ qe p) = (\q\ set (disjuncts p). Ifm vs bs (qe q))" + 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 vs bs (DJ qe p) \ (\q\ set (disjuncts p). Ifm vs bs (qe q))" by (simp add: DJ_def evaldjf_ex) - also have "\ = (\q \ set(disjuncts p). Ifm vs bs (E q))" using qe disjuncts_qf[OF qf] by auto - also have "\ = Ifm vs bs (E p)" by (induct p rule: disjuncts.induct, auto) - finally show "qfree (DJ qe p) \ Ifm vs bs (DJ qe p) = Ifm vs bs (E p)" using qfth by blast + also have "\ = (\q \ set(disjuncts p). Ifm vs bs (E q))" + using qe disjuncts_qf[OF qf] by auto + also have "\ = Ifm vs bs (E p)" + by (induct p rule: disjuncts.induct) auto + finally show "qfree (DJ qe p) \ Ifm vs bs (DJ qe p) = Ifm vs bs (E p)" + using qfth by blast qed -fun conjuncts :: "fm \ fm list" where - "conjuncts (And p q) = (conjuncts p) @ (conjuncts q)" +fun conjuncts :: "fm \ fm list" +where + "conjuncts (And p q) = conjuncts p @ conjuncts q" | "conjuncts T = []" | "conjuncts p = [p]" -definition list_conj :: "fm list \ fm" where - "list_conj ps \ foldr conj ps T" - -definition CJNB :: "(fm \ fm) \ fm \ fm" where - "CJNB f p \ (let cjs = conjuncts p ; (yes,no) = partition bound0 cjs - in conj (decr0 (list_conj yes)) (f (list_conj no)))" +definition list_conj :: "fm list \ fm" + where "list_conj ps \ foldr conj ps T" + +definition CJNB :: "(fm \ fm) \ fm \ fm" +where + "CJNB f p \ + (let cjs = conjuncts p; + (yes, no) = partition bound0 cjs + in conj (decr0 (list_conj yes)) (f (list_conj no)))" lemma conjuncts_qf: "qfree p \ \q\ set (conjuncts p). qfree q" -proof- +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) + then have "list_all qfree (conjuncts p)" + by (induct p rule: conjuncts.induct) auto + then show ?thesis + by (simp only: list_all_iff) qed lemma conjuncts: "(\q\ set (conjuncts p). Ifm vs bs q) = Ifm vs bs p" -by(induct p rule: conjuncts.induct, auto) + by (induct p rule: conjuncts.induct) auto lemma conjuncts_nb: "bound0 p \ \q\ set (conjuncts p). bound0 q" -proof- +proof - assume nb: "bound0 p" - hence "list_all bound0 (conjuncts p)" by (induct p rule:conjuncts.induct,auto) - thus ?thesis by (simp only: list_all_iff) + then have "list_all bound0 (conjuncts p)" + by (induct p rule:conjuncts.induct) auto + then show ?thesis + by (simp only: list_all_iff) qed -fun islin :: "fm \ bool" where +fun islin :: "fm \ bool" +where "islin (And p q) = (islin p \ islin q \ p \ T \ p \ F \ q \ T \ q \ F)" | "islin (Or p q) = (islin p \ islin q \ p \ T \ p \ F \ q \ T \ q \ F)" | "islin (Eq (CNP 0 c s)) = (isnpoly c \ c \ 0\<^sub>p \ tmbound0 s \ allpolys isnpoly s)" @@ -1017,62 +1060,84 @@ | "islin (Iff p q) = False" | "islin p = bound0 p" -lemma islin_stupid: assumes nb: "tmbound0 p" - shows "islin (Lt p)" and "islin (Le p)" and "islin (Eq p)" and "islin (NEq p)" +lemma islin_stupid: + assumes nb: "tmbound0 p" + shows "islin (Lt p)" + and "islin (Le p)" + and "islin (Eq p)" + and "islin (NEq p)" using nb by (cases p, auto, case_tac nat, auto)+ definition "lt p = (case p of CP (C c) \ if 0>\<^sub>N c then T else F| _ \ Lt p)" definition "le p = (case p of CP (C c) \ if 0\\<^sub>N c then T else F | _ \ Le p)" -definition eq where "eq p = (case p of CP (C c) \ if c = 0\<^sub>N then T else F | _ \ Eq p)" +definition "eq p = (case p of CP (C c) \ if c = 0\<^sub>N then T else F | _ \ Eq p)" definition "neq p = not (eq p)" lemma lt: "allpolys isnpoly p \ Ifm vs bs (lt p) = Ifm vs bs (Lt p)" - apply(simp add: lt_def) - apply(cases p, simp_all) - apply (case_tac poly, simp_all add: isnpoly_def) + apply (simp add: lt_def) + apply (cases p) + apply simp_all + apply (case_tac poly) + apply (simp_all add: isnpoly_def) done lemma le: "allpolys isnpoly p \ Ifm vs bs (le p) = Ifm vs bs (Le p)" - apply(simp add: le_def) - apply(cases p, simp_all) - apply (case_tac poly, simp_all add: isnpoly_def) + apply (simp add: le_def) + apply (cases p) + apply simp_all + apply (case_tac poly) + apply (simp_all add: isnpoly_def) done lemma eq: "allpolys isnpoly p \ Ifm vs bs (eq p) = Ifm vs bs (Eq p)" - apply(simp add: eq_def) - apply(cases p, simp_all) - apply (case_tac poly, simp_all add: isnpoly_def) + apply (simp add: eq_def) + apply (cases p) + apply simp_all + apply (case_tac poly) + apply (simp_all add: isnpoly_def) done lemma neq: "allpolys isnpoly p \ Ifm vs bs (neq p) = Ifm vs bs (NEq p)" - by(simp add: neq_def eq) + by (simp add: neq_def eq) lemma lt_lin: "tmbound0 p \ islin (lt p)" apply (simp add: lt_def) - apply (cases p, simp_all) - apply (case_tac poly, simp_all) - apply (case_tac nat, simp_all) + apply (cases p) + apply simp_all + apply (case_tac poly) + apply simp_all + apply (case_tac nat) + apply simp_all done lemma le_lin: "tmbound0 p \ islin (le p)" apply (simp add: le_def) - apply (cases p, simp_all) - apply (case_tac poly, simp_all) - apply (case_tac nat, simp_all) + apply (cases p) + apply simp_all + apply (case_tac poly) + apply simp_all + apply (case_tac nat) + apply simp_all done lemma eq_lin: "tmbound0 p \ islin (eq p)" apply (simp add: eq_def) - apply (cases p, simp_all) - apply (case_tac poly, simp_all) - apply (case_tac nat, simp_all) + apply (cases p) + apply simp_all + apply (case_tac poly) + apply simp_all + apply (case_tac nat) + apply simp_all done lemma neq_lin: "tmbound0 p \ islin (neq p)" apply (simp add: neq_def eq_def) - apply (cases p, simp_all) - apply (case_tac poly, simp_all) - apply (case_tac nat, simp_all) + apply (cases p) + apply simp_all + apply (case_tac poly) + apply simp_all + apply (case_tac nat) + apply simp_all done definition "simplt t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then lt s else Lt (CNP 0 c s))" @@ -1080,203 +1145,269 @@ definition "simpeq t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then eq s else Eq (CNP 0 c s))" definition "simpneq t = (let (c,s) = split0 (simptm t) in if c= 0\<^sub>p then neq s else NEq (CNP 0 c s))" -lemma simplt_islin[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" +lemma simplt_islin[simp]: + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "islin (simplt t)" unfolding simplt_def using split0_nb0' -by (auto simp add: lt_lin Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly] islin_stupid allpolys_split0[OF simptm_allpolys_npoly]) - -lemma simple_islin[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + by (auto simp add: lt_lin Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly] + islin_stupid allpolys_split0[OF simptm_allpolys_npoly]) + +lemma simple_islin[simp]: + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "islin (simple t)" unfolding simple_def using split0_nb0' -by (auto simp add: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly] islin_stupid allpolys_split0[OF simptm_allpolys_npoly] le_lin) -lemma simpeq_islin[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + by (auto simp add: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly] + islin_stupid allpolys_split0[OF simptm_allpolys_npoly] le_lin) + +lemma simpeq_islin[simp]: + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "islin (simpeq t)" unfolding simpeq_def using split0_nb0' -by (auto simp add: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly] islin_stupid allpolys_split0[OF simptm_allpolys_npoly] eq_lin) - -lemma simpneq_islin[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + by (auto simp add: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly] + islin_stupid allpolys_split0[OF simptm_allpolys_npoly] eq_lin) + +lemma simpneq_islin[simp]: + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "islin (simpneq t)" unfolding simpneq_def using split0_nb0' -by (auto simp add: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly] islin_stupid allpolys_split0[OF simptm_allpolys_npoly] neq_lin) + by (auto simp add: Let_def split_def isnpoly_fst_split0[OF simptm_allpolys_npoly] + islin_stupid allpolys_split0[OF simptm_allpolys_npoly] neq_lin) lemma really_stupid: "\ (\c1 s'. (c1, s') \ split0 s)" - by (cases "split0 s", auto) -lemma split0_npoly: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" - and n: "allpolys isnpoly t" - shows "isnpoly (fst (split0 t))" and "allpolys isnpoly (snd (split0 t))" + by (cases "split0 s") auto + +lemma split0_npoly: + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + and n: "allpolys isnpoly t" + shows "isnpoly (fst (split0 t))" + and "allpolys isnpoly (snd (split0 t))" using n - by (induct t rule: split0.induct, auto simp add: Let_def split_def polyadd_norm polymul_norm polyneg_norm polysub_norm really_stupid) -lemma simplt[simp]: - shows "Ifm vs bs (simplt t) = Ifm vs bs (Lt t)" -proof- - have n: "allpolys isnpoly (simptm t)" by simp + by (induct t rule: split0.induct) + (auto simp add: Let_def split_def polyadd_norm polymul_norm polyneg_norm + polysub_norm really_stupid) + +lemma simplt[simp]: "Ifm vs bs (simplt t) = Ifm vs bs (Lt t)" +proof - + have n: "allpolys isnpoly (simptm t)" + by simp let ?t = "simptm t" - {assume "fst (split0 ?t) = 0\<^sub>p" hence ?thesis + { + assume "fst (split0 ?t) = 0\<^sub>p" + then have ?thesis using split0[of "simptm t" vs bs] lt[OF split0_npoly(2)[OF n], of vs bs] - by (simp add: simplt_def Let_def split_def lt)} + by (simp add: simplt_def Let_def split_def lt) + } moreover - {assume "fst (split0 ?t) \ 0\<^sub>p" - hence ?thesis using split0[of "simptm t" vs bs] by (simp add: simplt_def Let_def split_def) + { + assume "fst (split0 ?t) \ 0\<^sub>p" + then have ?thesis + using split0[of "simptm t" vs bs] + by (simp add: simplt_def Let_def split_def) } ultimately show ?thesis by blast qed -lemma simple[simp]: - shows "Ifm vs bs (simple t) = Ifm vs bs (Le t)" -proof- - have n: "allpolys isnpoly (simptm t)" by simp +lemma simple[simp]: "Ifm vs bs (simple t) = Ifm vs bs (Le t)" +proof - + have n: "allpolys isnpoly (simptm t)" + by simp let ?t = "simptm t" - {assume "fst (split0 ?t) = 0\<^sub>p" hence ?thesis + { + assume "fst (split0 ?t) = 0\<^sub>p" + then have ?thesis using split0[of "simptm t" vs bs] le[OF split0_npoly(2)[OF n], of vs bs] - by (simp add: simple_def Let_def split_def le)} + by (simp add: simple_def Let_def split_def le) + } moreover - {assume "fst (split0 ?t) \ 0\<^sub>p" - hence ?thesis using split0[of "simptm t" vs bs] by (simp add: simple_def Let_def split_def) + { + assume "fst (split0 ?t) \ 0\<^sub>p" + then have ?thesis + using split0[of "simptm t" vs bs] + by (simp add: simple_def Let_def split_def) } ultimately show ?thesis by blast qed -lemma simpeq[simp]: - shows "Ifm vs bs (simpeq t) = Ifm vs bs (Eq t)" -proof- - have n: "allpolys isnpoly (simptm t)" by simp +lemma simpeq[simp]: "Ifm vs bs (simpeq t) = Ifm vs bs (Eq t)" +proof - + have n: "allpolys isnpoly (simptm t)" + by simp let ?t = "simptm t" - {assume "fst (split0 ?t) = 0\<^sub>p" hence ?thesis + { + assume "fst (split0 ?t) = 0\<^sub>p" + then have ?thesis using split0[of "simptm t" vs bs] eq[OF split0_npoly(2)[OF n], of vs bs] - by (simp add: simpeq_def Let_def split_def)} + by (simp add: simpeq_def Let_def split_def) + } moreover - {assume "fst (split0 ?t) \ 0\<^sub>p" - hence ?thesis using split0[of "simptm t" vs bs] by (simp add: simpeq_def Let_def split_def) + { + assume "fst (split0 ?t) \ 0\<^sub>p" + then have ?thesis using split0[of "simptm t" vs bs] + by (simp add: simpeq_def Let_def split_def) } ultimately show ?thesis by blast qed -lemma simpneq[simp]: - shows "Ifm vs bs (simpneq t) = Ifm vs bs (NEq t)" -proof- - have n: "allpolys isnpoly (simptm t)" by simp +lemma simpneq[simp]: "Ifm vs bs (simpneq t) = Ifm vs bs (NEq t)" +proof - + have n: "allpolys isnpoly (simptm t)" + by simp let ?t = "simptm t" - {assume "fst (split0 ?t) = 0\<^sub>p" hence ?thesis + { + assume "fst (split0 ?t) = 0\<^sub>p" + then have ?thesis using split0[of "simptm t" vs bs] neq[OF split0_npoly(2)[OF n], of vs bs] - by (simp add: simpneq_def Let_def split_def )} + by (simp add: simpneq_def Let_def split_def) + } moreover - {assume "fst (split0 ?t) \ 0\<^sub>p" - hence ?thesis using split0[of "simptm t" vs bs] by (simp add: simpneq_def Let_def split_def) + { + assume "fst (split0 ?t) \ 0\<^sub>p" + then have ?thesis + using split0[of "simptm t" vs bs] by (simp add: simpneq_def Let_def split_def) } ultimately show ?thesis by blast qed lemma lt_nb: "tmbound0 t \ bound0 (lt t)" apply (simp add: lt_def) - apply (cases t, auto) - apply (case_tac poly, auto) + apply (cases t) + apply auto + apply (case_tac poly) + apply auto done lemma le_nb: "tmbound0 t \ bound0 (le t)" apply (simp add: le_def) - apply (cases t, auto) - apply (case_tac poly, auto) + apply (cases t) + apply auto + apply (case_tac poly) + apply auto done lemma eq_nb: "tmbound0 t \ bound0 (eq t)" apply (simp add: eq_def) - apply (cases t, auto) - apply (case_tac poly, auto) + apply (cases t) + apply auto + apply (case_tac poly) + apply auto done lemma neq_nb: "tmbound0 t \ bound0 (neq t)" apply (simp add: neq_def eq_def) - apply (cases t, auto) - apply (case_tac poly, auto) + apply (cases t) + apply auto + apply (case_tac poly) + apply auto done -lemma simplt_nb[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" +lemma simplt_nb[simp]: + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "tmbound0 t \ bound0 (simplt t)" - using split0 [of "simptm t" "vs::'a list" bs] -proof(simp add: simplt_def Let_def split_def) +proof (simp add: simplt_def Let_def split_def) assume nb: "tmbound0 t" - hence nb': "tmbound0 (simptm t)" by simp + then have nb': "tmbound0 (simptm t)" + by simp let ?c = "fst (split0 (simptm t))" from tmbound_split0[OF nb'[unfolded tmbound0_tmbound_iff[symmetric]]] - have th: "\bs. Ipoly bs ?c = Ipoly bs 0\<^sub>p" by auto + have th: "\bs. Ipoly bs ?c = Ipoly bs 0\<^sub>p" + by auto from isnpoly_fst_split0[OF simptm_allpolys_npoly[of t]] - have ths: "isnpolyh ?c 0" "isnpolyh 0\<^sub>p 0" by (simp_all add: isnpoly_def) + have ths: "isnpolyh ?c 0" "isnpolyh 0\<^sub>p 0" + by (simp_all add: isnpoly_def) from iffD1[OF isnpolyh_unique[OF ths] th] have "fst (split0 (simptm t)) = 0\<^sub>p" . - thus "(fst (split0 (simptm t)) = 0\<^sub>p \ bound0 (lt (snd (split0 (simptm t))))) \ - fst (split0 (simptm t)) = 0\<^sub>p" by (simp add: simplt_def Let_def split_def lt_nb) + then show "(fst (split0 (simptm t)) = 0\<^sub>p \ bound0 (lt (snd (split0 (simptm t))))) \ + fst (split0 (simptm t)) = 0\<^sub>p" + by (simp add: simplt_def Let_def split_def lt_nb) qed -lemma simple_nb[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" +lemma simple_nb[simp]: + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "tmbound0 t \ bound0 (simple t)" - using split0 [of "simptm t" "vs::'a list" bs] proof(simp add: simple_def Let_def split_def) assume nb: "tmbound0 t" - hence nb': "tmbound0 (simptm t)" by simp + then have nb': "tmbound0 (simptm t)" + by simp let ?c = "fst (split0 (simptm t))" from tmbound_split0[OF nb'[unfolded tmbound0_tmbound_iff[symmetric]]] - have th: "\bs. Ipoly bs ?c = Ipoly bs 0\<^sub>p" by auto + have th: "\bs. Ipoly bs ?c = Ipoly bs 0\<^sub>p" + by auto from isnpoly_fst_split0[OF simptm_allpolys_npoly[of t]] - have ths: "isnpolyh ?c 0" "isnpolyh 0\<^sub>p 0" by (simp_all add: isnpoly_def) + have ths: "isnpolyh ?c 0" "isnpolyh 0\<^sub>p 0" + by (simp_all add: isnpoly_def) from iffD1[OF isnpolyh_unique[OF ths] th] have "fst (split0 (simptm t)) = 0\<^sub>p" . - thus "(fst (split0 (simptm t)) = 0\<^sub>p \ bound0 (le (snd (split0 (simptm t))))) \ - fst (split0 (simptm t)) = 0\<^sub>p" by (simp add: simplt_def Let_def split_def le_nb) + then show "(fst (split0 (simptm t)) = 0\<^sub>p \ bound0 (le (snd (split0 (simptm t))))) \ + fst (split0 (simptm t)) = 0\<^sub>p" + by (simp add: simplt_def Let_def split_def le_nb) qed -lemma simpeq_nb[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" +lemma simpeq_nb[simp]: + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "tmbound0 t \ bound0 (simpeq t)" - using split0 [of "simptm t" "vs::'a list" bs] -proof(simp add: simpeq_def Let_def split_def) +proof (simp add: simpeq_def Let_def split_def) assume nb: "tmbound0 t" - hence nb': "tmbound0 (simptm t)" by simp + then have nb': "tmbound0 (simptm t)" + by simp let ?c = "fst (split0 (simptm t))" from tmbound_split0[OF nb'[unfolded tmbound0_tmbound_iff[symmetric]]] - have th: "\bs. Ipoly bs ?c = Ipoly bs 0\<^sub>p" by auto + have th: "\bs. Ipoly bs ?c = Ipoly bs 0\<^sub>p" + by auto from isnpoly_fst_split0[OF simptm_allpolys_npoly[of t]] - have ths: "isnpolyh ?c 0" "isnpolyh 0\<^sub>p 0" by (simp_all add: isnpoly_def) + have ths: "isnpolyh ?c 0" "isnpolyh 0\<^sub>p 0" + by (simp_all add: isnpoly_def) from iffD1[OF isnpolyh_unique[OF ths] th] have "fst (split0 (simptm t)) = 0\<^sub>p" . - thus "(fst (split0 (simptm t)) = 0\<^sub>p \ bound0 (eq (snd (split0 (simptm t))))) \ - fst (split0 (simptm t)) = 0\<^sub>p" by (simp add: simpeq_def Let_def split_def eq_nb) + then show "(fst (split0 (simptm t)) = 0\<^sub>p \ bound0 (eq (snd (split0 (simptm t))))) \ + fst (split0 (simptm t)) = 0\<^sub>p" + by (simp add: simpeq_def Let_def split_def eq_nb) qed -lemma simpneq_nb[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" +lemma simpneq_nb[simp]: + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "tmbound0 t \ bound0 (simpneq t)" - using split0 [of "simptm t" "vs::'a list" bs] -proof(simp add: simpneq_def Let_def split_def) +proof (simp add: simpneq_def Let_def split_def) assume nb: "tmbound0 t" - hence nb': "tmbound0 (simptm t)" by simp + then have nb': "tmbound0 (simptm t)" + by simp let ?c = "fst (split0 (simptm t))" from tmbound_split0[OF nb'[unfolded tmbound0_tmbound_iff[symmetric]]] - have th: "\bs. Ipoly bs ?c = Ipoly bs 0\<^sub>p" by auto + have th: "\bs. Ipoly bs ?c = Ipoly bs 0\<^sub>p" + by auto from isnpoly_fst_split0[OF simptm_allpolys_npoly[of t]] - have ths: "isnpolyh ?c 0" "isnpolyh 0\<^sub>p 0" by (simp_all add: isnpoly_def) + have ths: "isnpolyh ?c 0" "isnpolyh 0\<^sub>p 0" + by (simp_all add: isnpoly_def) from iffD1[OF isnpolyh_unique[OF ths] th] have "fst (split0 (simptm t)) = 0\<^sub>p" . - thus "(fst (split0 (simptm t)) = 0\<^sub>p \ bound0 (neq (snd (split0 (simptm t))))) \ - fst (split0 (simptm t)) = 0\<^sub>p" by (simp add: simpneq_def Let_def split_def neq_nb) + then show "(fst (split0 (simptm t)) = 0\<^sub>p \ bound0 (neq (snd (split0 (simptm t))))) \ + fst (split0 (simptm t)) = 0\<^sub>p" + by (simp add: simpneq_def Let_def split_def neq_nb) qed -fun conjs :: "fm \ fm list" where - "conjs (And p q) = (conjs p)@(conjs q)" +fun conjs :: "fm \ fm list" +where + "conjs (And p q) = conjs p @ conjs q" | "conjs T = []" | "conjs p = [p]" + lemma conjs_ci: "(\q \ set (conjs p). Ifm vs bs q) = Ifm vs bs p" -by (induct p rule: conjs.induct, auto) -definition list_disj :: "fm list \ fm" where - "list_disj ps \ foldr disj ps F" + by (induct p rule: conjs.induct) auto + +definition list_disj :: "fm list \ fm" + where "list_disj ps \ foldr disj ps F" lemma list_conj: "Ifm vs bs (list_conj ps) = (\p\ set ps. Ifm vs bs p)" - by (induct ps, auto simp add: list_conj_def) + 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) + by (induct ps) (auto simp add: list_conj_def) + lemma list_disj: "Ifm vs bs (list_disj ps) = (\p\ set ps. Ifm vs bs p)" - by (induct ps, auto simp add: list_disj_def) + by (induct ps) (auto simp add: list_disj_def) lemma conj_boundslt: "boundslt n p \ boundslt n q \ boundslt n (conj p q)" unfolding conj_def by auto @@ -1297,25 +1428,27 @@ apply (unfold ball_Un) apply (unfold boundslt.simps) apply blast -by simp_all + apply simp_all + done lemma list_conj_boundslt: " \p\ set ps. boundslt n p \ boundslt n (list_conj ps)" unfolding list_conj_def - by (induct ps, auto simp add: conj_boundslt) - -lemma list_conj_nb: assumes bnd: "\p\ set ps. bound n p" + by (induct ps) auto + +lemma list_conj_nb: + assumes bnd: "\p\ set ps. bound n p" shows "bound n (list_conj ps)" using bnd unfolding list_conj_def - by (induct ps, auto simp add: conj_nb) + by (induct ps) auto lemma list_conj_nb': "\p\set ps. bound0 p \ bound0 (list_conj ps)" -unfolding list_conj_def by (induct ps , auto) + unfolding list_conj_def by (induct ps) auto lemma CJNB_qe: assumes qe: "\bs p. qfree p \ qfree (qe p) \ (Ifm vs bs (qe p) = Ifm vs bs (E p))" shows "\bs p. qfree p \ qfree (CJNB qe p) \ (Ifm vs bs ((CJNB qe p)) = Ifm vs bs (E p))" -proof(clarify) +proof clarify fix bs p assume qfp: "qfree p" let ?cjs = "conjuncts p" @@ -1323,24 +1456,36 @@ let ?no = "snd (partition bound0 ?cjs)" let ?cno = "list_conj ?no" let ?cyes = "list_conj ?yes" - have part: "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 (decr0 ?cyes )" by (simp add: decr0_qf) + have part: "partition bound0 ?cjs = (?yes,?no)" + by simp + from partition_P[OF part] have "\q\ set ?yes. bound0 q" + by blast + then have yes_nb: "bound0 ?cyes" + by (simp add: list_conj_nb') + then have yes_qf: "qfree (decr0 ?cyes)" + by (simp add: decr0_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 vs bs (qe ?cno) = Ifm vs bs (E ?cno)" by blast+ + have " \q\ set ?no. qfree q" + by auto + then have no_qf: "qfree ?cno" + by (simp add: list_conj_qf) + with qe have cno_qf:"qfree (qe ?cno)" + and noE: "Ifm vs bs (qe ?cno) = Ifm vs 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 vs bs p = (\q\ set ?cjs. Ifm vs bs q)" by blast + by (simp add: CJNB_def Let_def split_def) + { + fix bs + from conjuncts have "Ifm vs bs p = (\q\ set ?cjs. Ifm vs bs q)" + by blast also have "\ = ((\q\ set ?yes. Ifm vs bs q) \ (\q\ set ?no. Ifm vs bs q))" using partition_set[OF part] by auto - finally have "Ifm vs bs p = ((Ifm vs bs ?cyes) \ (Ifm vs bs ?cno))" using list_conj[of vs bs] by simp} - hence "Ifm vs bs (E p) = (\x. (Ifm vs (x#bs) ?cyes) \ (Ifm vs (x#bs) ?cno))" by simp - also have "\ = (\x. (Ifm vs (y#bs) ?cyes) \ (Ifm vs (x#bs) ?cno))" + finally have "Ifm vs bs p = ((Ifm vs bs ?cyes) \ (Ifm vs bs ?cno))" + using list_conj[of vs bs] by simp + } + then have "Ifm vs bs (E p) = (\x. (Ifm vs (x#bs) ?cyes) \ (Ifm vs (x#bs) ?cno))" + by simp + also fix y have "\ = (\x. (Ifm vs (y#bs) ?cyes) \ (Ifm vs (x#bs) ?cno))" using bound0_I[OF yes_nb, where bs="bs" and b'="y"] by blast also have "\ = (Ifm vs bs (decr0 ?cyes) \ Ifm vs bs (E ?cno))" by (auto simp add: decr0[OF yes_nb] simp del: partition_filter_conv) @@ -1348,7 +1493,8 @@ using qe[rule_format, OF no_qf] by auto finally have "Ifm vs bs (E p) = Ifm vs bs (CJNB qe p)" by (simp add: Let_def CJNB_def split_def) - with qf show "qfree (CJNB qe p) \ Ifm vs bs (CJNB qe p) = Ifm vs bs (E p)" by blast + with qf show "qfree (CJNB qe p) \ Ifm vs bs (CJNB qe p) = Ifm vs bs (E p)" + by blast qed consts simpfm :: "fm \ fm" @@ -1360,11 +1506,13 @@ "simpfm (And p q) = conj (simpfm p) (simpfm q)" "simpfm (Or p q) = disj (simpfm p) (simpfm q)" "simpfm (Imp p q) = disj (simpfm (NOT p)) (simpfm q)" - "simpfm (Iff p q) = disj (conj (simpfm p) (simpfm q)) (conj (simpfm (NOT p)) (simpfm (NOT q)))" + "simpfm (Iff p q) = + disj (conj (simpfm p) (simpfm q)) (conj (simpfm (NOT p)) (simpfm (NOT q)))" "simpfm (NOT (And p q)) = disj (simpfm (NOT p)) (simpfm (NOT q))" "simpfm (NOT (Or p q)) = conj (simpfm (NOT p)) (simpfm (NOT q))" "simpfm (NOT (Imp p q)) = conj (simpfm p) (simpfm (NOT q))" - "simpfm (NOT (Iff p q)) = disj (conj (simpfm p) (simpfm (NOT q))) (conj (simpfm (NOT p)) (simpfm q))" + "simpfm (NOT (Iff p q)) = + disj (conj (simpfm p) (simpfm (NOT q))) (conj (simpfm (NOT p)) (simpfm q))" "simpfm (NOT (Eq t)) = simpneq t" "simpfm (NOT (NEq t)) = simpeq t" "simpfm (NOT (Le t)) = simplt (Neg t)" @@ -1375,23 +1523,33 @@ "simpfm p = p" lemma simpfm[simp]: "Ifm vs bs (simpfm p) = Ifm vs bs p" -by(induct p arbitrary: bs rule: simpfm.induct, auto) - -lemma simpfm_bound0: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + by (induct p arbitrary: bs rule: simpfm.induct) auto + +lemma simpfm_bound0: + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "bound0 p \ bound0 (simpfm p)" -by (induct p rule: simpfm.induct, auto) + by (induct p rule: simpfm.induct) auto lemma lt_qf[simp]: "qfree (lt t)" - apply (cases t, auto simp add: lt_def) - by (case_tac poly, auto) + apply (cases t) + apply (auto simp add: lt_def) + apply (case_tac poly) + apply auto + done lemma le_qf[simp]: "qfree (le t)" - apply (cases t, auto simp add: le_def) - by (case_tac poly, auto) + apply (cases t) + apply (auto simp add: le_def) + apply (case_tac poly) + apply auto + done lemma eq_qf[simp]: "qfree (eq t)" - apply (cases t, auto simp add: eq_def) - by (case_tac poly, auto) + apply (cases t) + apply (auto simp add: eq_def) + apply (case_tac poly) + apply auto + done lemma neq_qf[simp]: "qfree (neq t)" by (simp add: neq_def) @@ -1401,16 +1559,17 @@ lemma simpneq_qf[simp]: "qfree (simpneq t)" by (simp add: simpneq_def Let_def split_def) lemma simpfm_qf[simp]: "qfree p \ qfree (simpfm p)" -by (induct p rule: simpfm.induct, auto simp add: disj_qf imp_qf iff_qf conj_qf not_qf Let_def) - -lemma disj_lin: "islin p \ islin q \ islin (disj p q)" by (simp add: disj_def) -lemma conj_lin: "islin p \ islin q \ islin (conj p q)" by (simp add: conj_def) - -lemma assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + by (induct p rule: simpfm.induct) auto + +lemma disj_lin: "islin p \ islin q \ islin (disj p q)" + by (simp add: disj_def) +lemma conj_lin: "islin p \ islin q \ islin (conj p q)" + by (simp add: conj_def) + +lemma + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "qfree p \ islin (simpfm p)" - apply (induct p rule: simpfm.induct) - apply (simp_all add: conj_lin disj_lin) - done + by (induct p rule: simpfm.induct) (simp_all add: conj_lin disj_lin) consts prep :: "fm \ fm" recdef prep "measure fmsize" @@ -1438,33 +1597,36 @@ "prep (Iff p q) = disj (prep (And p q)) (prep (And (NOT p) (NOT q)))" "prep p = p" (hints simp add: fmsize_pos) + lemma prep: "Ifm vs bs (prep p) = Ifm vs bs p" -by (induct p arbitrary: bs rule: prep.induct, auto) - - - - (* Generic quantifier elimination *) -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. imp (qelim p qe) (qelim q qe))" -| "qelim (Iff p q) = (\ qe. iff (qelim p qe) (qelim q qe))" -| "qelim p = (\ y. simpfm p)" + by (induct p arbitrary: bs rule: prep.induct) auto + + +(* Generic quantifier elimination *) +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. imp (qelim 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 simp_all termination by (relation "measure fmsize") auto lemma qelim: assumes qe_inv: "\bs p. qfree p \ qfree (qe p) \ (Ifm vs bs (qe p) = Ifm vs bs (E p))" shows "\ bs. qfree (qelim p qe) \ (Ifm vs bs (qelim p qe) = Ifm vs bs p)" -using qe_inv DJ_qe[OF CJNB_qe[OF qe_inv]] -by (induct p rule: qelim.induct) auto - -subsection{* Core Procedure *} - -fun minusinf:: "fm \ fm" (* Virtual substitution of -\*) where + using qe_inv DJ_qe[OF CJNB_qe[OF qe_inv]] + by (induct p rule: qelim.induct) auto + + +subsection {* Core Procedure *} + +fun minusinf:: "fm \ fm" (* Virtual substitution of -\*) +where "minusinf (And p q) = conj (minusinf p) (minusinf q)" | "minusinf (Or p q) = disj (minusinf p) (minusinf q)" | "minusinf (Eq (CNP 0 c e)) = conj (eq (CP c)) (eq e)" @@ -1473,7 +1635,8 @@ | "minusinf (Le (CNP 0 c e)) = disj (conj (eq (CP c)) (le e)) (lt (CP (~\<^sub>p c)))" | "minusinf p = p" -fun plusinf:: "fm \ fm" (* Virtual substitution of +\*) where +fun plusinf:: "fm \ fm" (* Virtual substitution of +\*) +where "plusinf (And p q) = conj (plusinf p) (plusinf q)" | "plusinf (Or p q) = disj (plusinf p) (plusinf q)" | "plusinf (Eq (CNP 0 c e)) = conj (eq (CP c)) (eq e)" @@ -1482,443 +1645,811 @@ | "plusinf (Le (CNP 0 c e)) = disj (conj (eq (CP c)) (le e)) (lt (CP c))" | "plusinf p = p" -lemma minusinf_inf: assumes lp:"islin p" +lemma minusinf_inf: + assumes lp: "islin p" shows "\z. \x < z. Ifm vs (x#bs) (minusinf p) \ Ifm vs (x#bs) p" using lp proof (induct p rule: minusinf.induct) - case 1 thus ?case by (auto,rule_tac x="min z za" in exI, auto) + case 1 + then show ?case + apply auto + apply (rule_tac x="min z za" in exI) + apply auto + done next - case 2 thus ?case by (auto,rule_tac x="min z za" in exI, auto) + case 2 + then show ?case + apply auto + apply (rule_tac x="min z za" in exI) + apply auto + done next - case (3 c e) hence nbe: "tmbound0 e" by simp - from 3 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all + case (3 c e) + then have nbe: "tmbound0 e" + by simp + from 3 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" + by simp_all note eqs = eq[OF nc(1), where ?'a = 'a] eq[OF nc(2), where ?'a = 'a] let ?c = "Ipoly vs c" + fix y let ?e = "Itm vs (y#bs) e" - have "?c=0 \ ?c > 0 \ ?c < 0" by arith - moreover {assume "?c = 0" hence ?case - using eq[OF nc(2), of vs] eq[OF nc(1), of vs] by auto} - moreover {assume cp: "?c > 0" - {fix x assume xz: "x < -?e / ?c" hence "?c * x < - ?e" - using pos_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute) - hence "?c * x + ?e < 0" by simp - hence "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Eq (CNP 0 c e)))" - using eqs tmbound0_I[OF nbe, where b="y" and b'="x" and vs=vs and bs=bs] by auto} hence ?case by auto} - moreover {assume cp: "?c < 0" - {fix x assume xz: "x < -?e / ?c" hence "?c * x > - ?e" - using neg_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute) - hence "?c * x + ?e > 0" by simp - hence "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Eq (CNP 0 c e)))" - using tmbound0_I[OF nbe, where b="y" and b'="x"] eqs by auto} hence ?case by auto} - ultimately show ?case by blast -next - case (4 c e) hence nbe: "tmbound0 e" by simp - from 4 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all - note eqs = eq[OF nc(1), where ?'a = 'a] eq[OF nc(2), where ?'a = 'a] - let ?c = "Ipoly vs c" - let ?e = "Itm vs (y#bs) e" - have "?c=0 \ ?c > 0 \ ?c < 0" by arith - moreover {assume "?c = 0" hence ?case using eqs by auto} - moreover {assume cp: "?c > 0" - {fix x assume xz: "x < -?e / ?c" hence "?c * x < - ?e" - using pos_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute) - hence "?c * x + ?e < 0" by simp - hence "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (NEq (CNP 0 c e)))" - using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto} hence ?case by auto} - moreover {assume cp: "?c < 0" - {fix x assume xz: "x < -?e / ?c" hence "?c * x > - ?e" - using neg_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute) - hence "?c * x + ?e > 0" by simp - hence "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (NEq (CNP 0 c e)))" - using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto} hence ?case by auto} + have "?c = 0 \ ?c > 0 \ ?c < 0" by arith + moreover { + assume "?c = 0" + then have ?case + using eq[OF nc(2), of vs] eq[OF nc(1), of vs] by auto + } + moreover { + assume cp: "?c > 0" + { + fix x + assume xz: "x < -?e / ?c" + then have "?c * x < - ?e" + using pos_less_divide_eq[OF cp, where a="x" and b="-?e"] + by (simp add: mult_commute) + then have "?c * x + ?e < 0" + by simp + then have "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Eq (CNP 0 c e)))" + using eqs tmbound0_I[OF nbe, where b="y" and b'="x" and vs=vs and bs=bs] by auto + } + then have ?case by auto + } + moreover { + assume cp: "?c < 0" + { + fix x + assume xz: "x < -?e / ?c" + then have "?c * x > - ?e" + using neg_less_divide_eq[OF cp, where a="x" and b="-?e"] + by (simp add: mult_commute) + then have "?c * x + ?e > 0" + by simp + then have "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Eq (CNP 0 c e)))" + using tmbound0_I[OF nbe, where b="y" and b'="x"] eqs by auto + } + then have ?case by auto + } ultimately show ?case by blast next - case (5 c e) hence nbe: "tmbound0 e" by simp - from 5 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all - hence nc': "allpolys isnpoly (CP (~\<^sub>p c))" by (simp add: polyneg_norm) - note eqs = lt[OF nc', where ?'a = 'a] eq [OF nc(1), where ?'a = 'a] lt[OF nc(2), where ?'a = 'a] + case (4 c e) + then have nbe: "tmbound0 e" + by simp + from 4 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" + by simp_all + note eqs = eq[OF nc(1), where ?'a = 'a] eq[OF nc(2), where ?'a = 'a] let ?c = "Ipoly vs c" + fix y let ?e = "Itm vs (y#bs) e" - have "?c=0 \ ?c > 0 \ ?c < 0" by arith - moreover {assume "?c = 0" hence ?case using eqs by auto} - moreover {assume cp: "?c > 0" - {fix x assume xz: "x < -?e / ?c" hence "?c * x < - ?e" - using pos_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute) - hence "?c * x + ?e < 0" by simp - hence "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Lt (CNP 0 c e)))" - using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto} - moreover {assume cp: "?c < 0" - {fix x assume xz: "x < -?e / ?c" hence "?c * x > - ?e" - using neg_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute) - hence "?c * x + ?e > 0" by simp - hence "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Lt (CNP 0 c e)))" - using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] cp by auto} hence ?case by auto} + have "?c=0 \ ?c > 0 \ ?c < 0" + by arith + moreover { + assume "?c = 0" + then have ?case + using eqs by auto + } + moreover { + assume cp: "?c > 0" + { + fix x + assume xz: "x < -?e / ?c" + then have "?c * x < - ?e" + using pos_less_divide_eq[OF cp, where a="x" and b="-?e"] + by (simp add: mult_commute) + then have "?c * x + ?e < 0" + by simp + then have "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (NEq (CNP 0 c e)))" + using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto + } + then have ?case by auto + } + moreover { + assume cp: "?c < 0" + { + fix x + assume xz: "x < -?e / ?c" + then have "?c * x > - ?e" + using neg_less_divide_eq[OF cp, where a="x" and b="-?e"] + by (simp add: mult_commute) + then have "?c * x + ?e > 0" + by simp + then have "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (NEq (CNP 0 c e)))" + using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto + } + then have ?case by auto + } ultimately show ?case by blast next - case (6 c e) hence nbe: "tmbound0 e" by simp - from 6 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all - hence nc': "allpolys isnpoly (CP (~\<^sub>p c))" by (simp add: polyneg_norm) + case (5 c e) + then have nbe: "tmbound0 e" + by simp + from 5 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" + by simp_all + then have nc': "allpolys isnpoly (CP (~\<^sub>p c))" + by (simp add: polyneg_norm) + note eqs = lt[OF nc', where ?'a = 'a] eq [OF nc(1), where ?'a = 'a] lt[OF nc(2), where ?'a = 'a] + let ?c = "Ipoly vs c" + fix y + let ?e = "Itm vs (y#bs) e" + have "?c=0 \ ?c > 0 \ ?c < 0" + by arith + moreover { + assume "?c = 0" + then have ?case using eqs by auto + } + moreover { + assume cp: "?c > 0" + { + fix x + assume xz: "x < -?e / ?c" + then have "?c * x < - ?e" + using pos_less_divide_eq[OF cp, where a="x" and b="-?e"] + by (simp add: mult_commute) + then have "?c * x + ?e < 0" by simp + then have "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Lt (CNP 0 c e)))" + using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto + } + then have ?case by auto + } + moreover { + assume cp: "?c < 0" + { + fix x + assume xz: "x < -?e / ?c" + then have "?c * x > - ?e" + using neg_less_divide_eq[OF cp, where a="x" and b="-?e"] + by (simp add: mult_commute) + then have "?c * x + ?e > 0" + by simp + then have "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Lt (CNP 0 c e)))" + using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] cp by auto + } + then have ?case by auto + } + ultimately show ?case by blast +next + case (6 c e) + then have nbe: "tmbound0 e" + by simp + from 6 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" + by simp_all + then have nc': "allpolys isnpoly (CP (~\<^sub>p c))" + by (simp add: polyneg_norm) note eqs = lt[OF nc', where ?'a = 'a] eq [OF nc(1), where ?'a = 'a] le[OF nc(2), where ?'a = 'a] let ?c = "Ipoly vs c" + fix y let ?e = "Itm vs (y#bs) e" - have "?c=0 \ ?c > 0 \ ?c < 0" by arith - moreover {assume "?c = 0" hence ?case using eqs by auto} - moreover {assume cp: "?c > 0" - {fix x assume xz: "x < -?e / ?c" hence "?c * x < - ?e" - using pos_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute) - hence "?c * x + ?e < 0" by simp - hence "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Le (CNP 0 c e)))" - using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto} - moreover {assume cp: "?c < 0" - {fix x assume xz: "x < -?e / ?c" hence "?c * x > - ?e" - using neg_less_divide_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute) - hence "?c * x + ?e > 0" by simp - hence "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Le (CNP 0 c e)))" - using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto} + have "?c = 0 \ ?c > 0 \ ?c < 0" by arith + moreover { + assume "?c = 0" + then have ?case using eqs by auto + } + moreover { + assume cp: "?c > 0" + { + fix x + assume xz: "x < -?e / ?c" + then have "?c * x < - ?e" + using pos_less_divide_eq[OF cp, where a="x" and b="-?e"] + by (simp add: mult_commute) + then have "?c * x + ?e < 0" + by simp + then have "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Le (CNP 0 c e)))" + using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs + by auto + } + then have ?case by auto + } + moreover { + assume cp: "?c < 0" + { + fix x + assume xz: "x < -?e / ?c" + then have "?c * x > - ?e" + using neg_less_divide_eq[OF cp, where a="x" and b="-?e"] + by (simp add: mult_commute) + then have "?c * x + ?e > 0" + by simp + then have "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (minusinf (Le (CNP 0 c e)))" + using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs + by auto + } + then have ?case by auto + } ultimately show ?case by blast -qed (auto) - -lemma plusinf_inf: assumes lp:"islin p" +qed auto + +lemma plusinf_inf: + assumes lp: "islin p" shows "\z. \x > z. Ifm vs (x#bs) (plusinf p) \ Ifm vs (x#bs) p" using lp proof (induct p rule: plusinf.induct) - case 1 thus ?case by (auto,rule_tac x="max z za" in exI, auto) + case 1 + then show ?case + apply auto + apply (rule_tac x="max z za" in exI) + apply auto + done next - case 2 thus ?case by (auto,rule_tac x="max z za" in exI, auto) + case 2 + then show ?case + apply auto + apply (rule_tac x="max z za" in exI) + apply auto + done next - case (3 c e) hence nbe: "tmbound0 e" by simp - from 3 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all + case (3 c e) + then have nbe: "tmbound0 e" + by simp + from 3 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" + by simp_all note eqs = eq[OF nc(1), where ?'a = 'a] eq[OF nc(2), where ?'a = 'a] let ?c = "Ipoly vs c" + fix y let ?e = "Itm vs (y#bs) e" have "?c=0 \ ?c > 0 \ ?c < 0" by arith - moreover {assume "?c = 0" hence ?case - using eq[OF nc(2), of vs] eq[OF nc(1), of vs] by auto} - moreover {assume cp: "?c > 0" - {fix x assume xz: "x > -?e / ?c" hence "?c * x > - ?e" - using pos_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute) - hence "?c * x + ?e > 0" by simp - hence "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Eq (CNP 0 c e)))" - using eqs tmbound0_I[OF nbe, where b="y" and b'="x" and vs=vs and bs=bs] by auto} hence ?case by auto} - moreover {assume cp: "?c < 0" - {fix x assume xz: "x > -?e / ?c" hence "?c * x < - ?e" - using neg_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute) - hence "?c * x + ?e < 0" by simp - hence "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Eq (CNP 0 c e)))" - using tmbound0_I[OF nbe, where b="y" and b'="x"] eqs by auto} hence ?case by auto} + moreover { + assume "?c = 0" + then have ?case + using eq[OF nc(2), of vs] eq[OF nc(1), of vs] by auto + } + moreover { + assume cp: "?c > 0" + { + fix x + assume xz: "x > -?e / ?c" + then have "?c * x > - ?e" + using pos_divide_less_eq[OF cp, where a="x" and b="-?e"] + by (simp add: mult_commute) + then have "?c * x + ?e > 0" + by simp + then have "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Eq (CNP 0 c e)))" + using eqs tmbound0_I[OF nbe, where b="y" and b'="x" and vs=vs and bs=bs] by auto + } + then have ?case by auto + } + moreover { + assume cp: "?c < 0" + { + fix x + assume xz: "x > -?e / ?c" + then have "?c * x < - ?e" + using neg_divide_less_eq[OF cp, where a="x" and b="-?e"] + by (simp add: mult_commute) + then have "?c * x + ?e < 0" by simp + then have "Ifm vs (x#bs) (Eq (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Eq (CNP 0 c e)))" + using tmbound0_I[OF nbe, where b="y" and b'="x"] eqs by auto + } + then have ?case by auto + } ultimately show ?case by blast next - case (4 c e) hence nbe: "tmbound0 e" by simp - from 4 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all + case (4 c e) + then have nbe: "tmbound0 e" + by simp + from 4 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" + by simp_all note eqs = eq[OF nc(1), where ?'a = 'a] eq[OF nc(2), where ?'a = 'a] let ?c = "Ipoly vs c" - let ?e = "Itm vs (y#bs) e" - have "?c=0 \ ?c > 0 \ ?c < 0" by arith - moreover {assume "?c = 0" hence ?case using eqs by auto} - moreover {assume cp: "?c > 0" - {fix x assume xz: "x > -?e / ?c" hence "?c * x > - ?e" - using pos_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute) - hence "?c * x + ?e > 0" by simp - hence "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (NEq (CNP 0 c e)))" - using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto} hence ?case by auto} - moreover {assume cp: "?c < 0" - {fix x assume xz: "x > -?e / ?c" hence "?c * x < - ?e" - using neg_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute) - hence "?c * x + ?e < 0" by simp - hence "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (NEq (CNP 0 c e)))" - using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto} hence ?case by auto} - ultimately show ?case by blast -next - case (5 c e) hence nbe: "tmbound0 e" by simp - from 5 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all - hence nc': "allpolys isnpoly (CP (~\<^sub>p c))" by (simp add: polyneg_norm) - note eqs = lt[OF nc(1), where ?'a = 'a] lt[OF nc', where ?'a = 'a] eq [OF nc(1), where ?'a = 'a] lt[OF nc(2), where ?'a = 'a] - let ?c = "Ipoly vs c" + fix y let ?e = "Itm vs (y#bs) e" have "?c=0 \ ?c > 0 \ ?c < 0" by arith - moreover {assume "?c = 0" hence ?case using eqs by auto} - moreover {assume cp: "?c > 0" - {fix x assume xz: "x > -?e / ?c" hence "?c * x > - ?e" - using pos_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute) - hence "?c * x + ?e > 0" by simp - hence "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Lt (CNP 0 c e)))" - using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto} - moreover {assume cp: "?c < 0" - {fix x assume xz: "x > -?e / ?c" hence "?c * x < - ?e" - using neg_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute) - hence "?c * x + ?e < 0" by simp - hence "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Lt (CNP 0 c e)))" - using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] cp by auto} hence ?case by auto} + moreover { + assume "?c = 0" + then have ?case using eqs by auto + } + moreover { + assume cp: "?c > 0" + { + fix x + assume xz: "x > -?e / ?c" + then have "?c * x > - ?e" + using pos_divide_less_eq[OF cp, where a="x" and b="-?e"] + by (simp add: mult_commute) + then have "?c * x + ?e > 0" + by simp + then have "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (NEq (CNP 0 c e)))" + using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto + } + then have ?case by auto + } + moreover { + assume cp: "?c < 0" + { + fix x + assume xz: "x > -?e / ?c" + then have "?c * x < - ?e" + using neg_divide_less_eq[OF cp, where a="x" and b="-?e"] + by (simp add: mult_commute) + then have "?c * x + ?e < 0" + by simp + then have "Ifm vs (x#bs) (NEq (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (NEq (CNP 0 c e)))" + using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] by auto + } + then have ?case by auto + } ultimately show ?case by blast next - case (6 c e) hence nbe: "tmbound0 e" by simp - from 6 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" by simp_all - hence nc': "allpolys isnpoly (CP (~\<^sub>p c))" by (simp add: polyneg_norm) + case (5 c e) + then have nbe: "tmbound0 e" + by simp + from 5 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" + by simp_all + then have nc': "allpolys isnpoly (CP (~\<^sub>p c))" + by (simp add: polyneg_norm) + note eqs = lt[OF nc(1), where ?'a = 'a] lt[OF nc', where ?'a = 'a] eq [OF nc(1), where ?'a = 'a] lt[OF nc(2), where ?'a = 'a] + let ?c = "Ipoly vs c" + fix y + let ?e = "Itm vs (y#bs) e" + have "?c = 0 \ ?c > 0 \ ?c < 0" by arith + moreover { + assume "?c = 0" + then have ?case using eqs by auto + } + moreover { + assume cp: "?c > 0" + { + fix x + assume xz: "x > -?e / ?c" + then have "?c * x > - ?e" + using pos_divide_less_eq[OF cp, where a="x" and b="-?e"] + by (simp add: mult_commute) + then have "?c * x + ?e > 0" + by simp + then have "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Lt (CNP 0 c e)))" + using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto + } + then have ?case by auto + } + moreover { + assume cp: "?c < 0" + { + fix x + assume xz: "x > -?e / ?c" + then have "?c * x < - ?e" + using neg_divide_less_eq[OF cp, where a="x" and b="-?e"] + by (simp add: mult_commute) + then have "?c * x + ?e < 0" + by simp + then have "Ifm vs (x#bs) (Lt (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Lt (CNP 0 c e)))" + using eqs tmbound0_I[OF nbe, where b="y" and b'="x"] cp by auto + } + then have ?case by auto + } + ultimately show ?case by blast +next + case (6 c e) + then have nbe: "tmbound0 e" + by simp + from 6 have nc: "allpolys isnpoly (CP c)" "allpolys isnpoly e" + by simp_all + then have nc': "allpolys isnpoly (CP (~\<^sub>p c))" + by (simp add: polyneg_norm) note eqs = lt[OF nc(1), where ?'a = 'a] eq [OF nc(1), where ?'a = 'a] le[OF nc(2), where ?'a = 'a] let ?c = "Ipoly vs c" + fix y let ?e = "Itm vs (y#bs) e" - have "?c=0 \ ?c > 0 \ ?c < 0" by arith - moreover {assume "?c = 0" hence ?case using eqs by auto} - moreover {assume cp: "?c > 0" - {fix x assume xz: "x > -?e / ?c" hence "?c * x > - ?e" - using pos_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute) - hence "?c * x + ?e > 0" by simp - hence "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Le (CNP 0 c e)))" - using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto} - moreover {assume cp: "?c < 0" - {fix x assume xz: "x > -?e / ?c" hence "?c * x < - ?e" - using neg_divide_less_eq[OF cp, where a="x" and b="-?e"] by (simp add: mult_commute) - hence "?c * x + ?e < 0" by simp - hence "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Le (CNP 0 c e)))" - using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto} hence ?case by auto} + have "?c = 0 \ ?c > 0 \ ?c < 0" by arith + moreover { + assume "?c = 0" + then have ?case using eqs by auto + } + moreover { + assume cp: "?c > 0" + { + fix x + assume xz: "x > -?e / ?c" + then have "?c * x > - ?e" + using pos_divide_less_eq[OF cp, where a="x" and b="-?e"] + by (simp add: mult_commute) + then have "?c * x + ?e > 0" + by simp + then have "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Le (CNP 0 c e)))" + using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto + } + then have ?case by auto + } + moreover { + assume cp: "?c < 0" + { + fix x + assume xz: "x > -?e / ?c" + then have "?c * x < - ?e" + using neg_divide_less_eq[OF cp, where a="x" and b="-?e"] + by (simp add: mult_commute) + then have "?c * x + ?e < 0" + by simp + then have "Ifm vs (x#bs) (Le (CNP 0 c e)) = Ifm vs (x#bs) (plusinf (Le (CNP 0 c e)))" + using tmbound0_I[OF nbe, where b="y" and b'="x"] cp eqs by auto + } + then have ?case by auto + } ultimately show ?case by blast -qed (auto) +qed auto lemma minusinf_nb: "islin p \ bound0 (minusinf p)" - by (induct p rule: minusinf.induct, auto simp add: eq_nb lt_nb le_nb) + by (induct p rule: minusinf.induct) (auto simp add: eq_nb lt_nb le_nb) + lemma plusinf_nb: "islin p \ bound0 (plusinf p)" - by (induct p rule: minusinf.induct, auto simp add: eq_nb lt_nb le_nb) - -lemma minusinf_ex: assumes lp: "islin p" and ex: "Ifm vs (x#bs) (minusinf p)" + by (induct p rule: minusinf.induct) (auto simp add: eq_nb lt_nb le_nb) + +lemma minusinf_ex: + assumes lp: "islin p" + and ex: "Ifm vs (x#bs) (minusinf p)" shows "\x. Ifm vs (x#bs) p" -proof- - from bound0_I [OF minusinf_nb[OF lp], where b="a" and bs ="bs"] ex - have th: "\x. Ifm vs (x#bs) (minusinf p)" by auto +proof - + from bound0_I [OF minusinf_nb[OF lp], where bs ="bs"] ex + have th: "\x. Ifm vs (x#bs) (minusinf p)" + by auto from minusinf_inf[OF lp, where bs="bs"] - obtain z where z_def: "\xxx. Ifm vs (x#bs) p" -proof- - from bound0_I [OF plusinf_nb[OF lp], where b="a" and bs ="bs"] ex - have th: "\x. Ifm vs (x#bs) (plusinf p)" by auto +proof - + from bound0_I [OF plusinf_nb[OF lp], where bs ="bs"] ex + have th: "\x. Ifm vs (x#bs) (plusinf p)" + by auto from plusinf_inf[OF lp, where bs="bs"] - obtain z where z_def: "\x>z. Ifm vs (x # bs) (plusinf p) = Ifm vs (x # bs) p" by blast - from th have "Ifm vs ((z + 1)#bs) (plusinf p)" by simp - moreover have "z + 1 > z" by simp - ultimately show ?thesis using z_def by auto + obtain z where z: "\x>z. Ifm vs (x # bs) (plusinf p) = Ifm vs (x # bs) p" + by blast + from th have "Ifm vs ((z + 1)#bs) (plusinf p)" + by simp + moreover have "z + 1 > z" + by simp + ultimately show ?thesis + using z by auto qed -fun uset :: "fm \ (poly \ tm) list" where +fun uset :: "fm \ (poly \ tm) list" +where "uset (And p q) = uset p @ uset q" | "uset (Or p q) = uset p @ uset q" -| "uset (Eq (CNP 0 a e)) = [(a,e)]" -| "uset (Le (CNP 0 a e)) = [(a,e)]" -| "uset (Lt (CNP 0 a e)) = [(a,e)]" -| "uset (NEq (CNP 0 a e)) = [(a,e)]" +| "uset (Eq (CNP 0 a e)) = [(a, e)]" +| "uset (Le (CNP 0 a e)) = [(a, e)]" +| "uset (Lt (CNP 0 a e)) = [(a, e)]" +| "uset (NEq (CNP 0 a e)) = [(a, e)]" | "uset p = []" lemma uset_l: assumes lp: "islin p" shows "\(c,s) \ set (uset p). isnpoly c \ c \ 0\<^sub>p \ tmbound0 s \ allpolys isnpoly s" -using lp by(induct p rule: uset.induct,auto) + using lp by (induct p rule: uset.induct) auto lemma minusinf_uset0: assumes lp: "islin p" - and nmi: "\ (Ifm vs (x#bs) (minusinf p))" - and ex: "Ifm vs (x#bs) p" (is "?I x p") - shows "\(c,s) \ set (uset p). x \ - Itm vs (x#bs) s / Ipoly vs c" -proof- - have "\(c,s) \ set (uset p). (Ipoly vs c < 0 \ Ipoly vs c * x \ - Itm vs (x#bs) s) \ (Ipoly vs c > 0 \ Ipoly vs c * x \ - Itm vs (x#bs) s)" + and nmi: "\ (Ifm vs (x#bs) (minusinf p))" + and ex: "Ifm vs (x#bs) p" (is "?I x p") + shows "\(c, s) \ set (uset p). x \ - Itm vs (x#bs) s / Ipoly vs c" +proof - + have "\(c, s) \ set (uset p). + Ipoly vs c < 0 \ Ipoly vs c * x \ - Itm vs (x#bs) s \ + Ipoly vs c > 0 \ Ipoly vs c * x \ - Itm vs (x#bs) s" using lp nmi ex - apply (induct p rule: minusinf.induct, auto simp add: eq le lt polyneg_norm) + apply (induct p rule: minusinf.induct) + apply (auto simp add: eq le lt polyneg_norm) apply (auto simp add: linorder_not_less order_le_less) done - then obtain c s where csU: "(c,s) \ set (uset p)" and x: "(Ipoly vs c < 0 \ Ipoly vs c * x \ - Itm vs (x#bs) s) \ (Ipoly vs c > 0 \ Ipoly vs c * x \ - Itm vs (x#bs) s)" by blast - hence "x \ (- Itm vs (x#bs) s) / Ipoly vs c" + then obtain c s where csU: "(c, s) \ set (uset p)" + and x: "(Ipoly vs c < 0 \ Ipoly vs c * x \ - Itm vs (x#bs) s) \ + (Ipoly vs c > 0 \ Ipoly vs c * x \ - Itm vs (x#bs) s)" by blast + then have "x \ (- Itm vs (x#bs) s) / Ipoly vs c" using divide_le_eq[of "- Itm vs (x#bs) s" "Ipoly vs c" x] - by (auto simp add: mult_commute) - thus ?thesis using csU by auto + by (auto simp add: mult_commute) + then show ?thesis + using csU by auto qed lemma minusinf_uset: assumes lp: "islin p" - and nmi: "\ (Ifm vs (a#bs) (minusinf p))" - and ex: "Ifm vs (x#bs) p" (is "?I x p") + and nmi: "\ (Ifm vs (a#bs) (minusinf p))" + and ex: "Ifm vs (x#bs) p" (is "?I x p") shows "\(c,s) \ set (uset p). x \ - Itm vs (a#bs) s / Ipoly vs c" -proof- - from nmi have nmi': "\ (Ifm vs (x#bs) (minusinf p))" +proof - + from nmi have nmi': "\ Ifm vs (x#bs) (minusinf p)" by (simp add: bound0_I[OF minusinf_nb[OF lp], where b=x and b'=a]) from minusinf_uset0[OF lp nmi' ex] - obtain c s where csU: "(c,s) \ set (uset p)" and th: "x \ - Itm vs (x#bs) s / Ipoly vs c" by blast - from uset_l[OF lp, rule_format, OF csU] have nb: "tmbound0 s" by simp - from th tmbound0_I[OF nb, of vs x bs a] csU show ?thesis by auto + obtain c s where csU: "(c,s) \ set (uset p)" + and th: "x \ - Itm vs (x#bs) s / Ipoly vs c" + by blast + from uset_l[OF lp, rule_format, OF csU] have nb: "tmbound0 s" + by simp + from th tmbound0_I[OF nb, of vs x bs a] csU show ?thesis + by auto qed lemma plusinf_uset0: assumes lp: "islin p" - and nmi: "\ (Ifm vs (x#bs) (plusinf p))" - and ex: "Ifm vs (x#bs) p" (is "?I x p") - shows "\(c,s) \ set (uset p). x \ - Itm vs (x#bs) s / Ipoly vs c" + and nmi: "\ (Ifm vs (x#bs) (plusinf p))" + and ex: "Ifm vs (x#bs) p" (is "?I x p") + shows "\(c, s) \ set (uset p). x \ - Itm vs (x#bs) s / Ipoly vs c" proof- - have "\(c,s) \ set (uset p). (Ipoly vs c < 0 \ Ipoly vs c * x \ - Itm vs (x#bs) s) \ (Ipoly vs c > 0 \ Ipoly vs c * x \ - Itm vs (x#bs) s)" + have "\(c, s) \ set (uset p). + Ipoly vs c < 0 \ Ipoly vs c * x \ - Itm vs (x#bs) s \ + Ipoly vs c > 0 \ Ipoly vs c * x \ - Itm vs (x#bs) s" using lp nmi ex - apply (induct p rule: minusinf.induct, auto simp add: eq le lt polyneg_norm) + apply (induct p rule: minusinf.induct) + apply (auto simp add: eq le lt polyneg_norm) apply (auto simp add: linorder_not_less order_le_less) done - then obtain c s where csU: "(c,s) \ set (uset p)" and x: "(Ipoly vs c < 0 \ Ipoly vs c * x \ - Itm vs (x#bs) s) \ (Ipoly vs c > 0 \ Ipoly vs c * x \ - Itm vs (x#bs) s)" by blast - hence "x \ (- Itm vs (x#bs) s) / Ipoly vs c" + then obtain c s where csU: "(c, s) \ set (uset p)" + and x: "Ipoly vs c < 0 \ Ipoly vs c * x \ - Itm vs (x#bs) s \ + Ipoly vs c > 0 \ Ipoly vs c * x \ - Itm vs (x#bs) s" + by blast + then have "x \ (- Itm vs (x#bs) s) / Ipoly vs c" using le_divide_eq[of x "- Itm vs (x#bs) s" "Ipoly vs c"] - by (auto simp add: mult_commute del: divide_minus_left) - thus ?thesis using csU by auto + by (auto simp add: mult_commute) + then show ?thesis + using csU by auto qed lemma plusinf_uset: assumes lp: "islin p" - and nmi: "\ (Ifm vs (a#bs) (plusinf p))" - and ex: "Ifm vs (x#bs) p" (is "?I x p") + and nmi: "\ (Ifm vs (a#bs) (plusinf p))" + and ex: "Ifm vs (x#bs) p" (is "?I x p") shows "\(c,s) \ set (uset p). x \ - Itm vs (a#bs) s / Ipoly vs c" -proof- +proof - from nmi have nmi': "\ (Ifm vs (x#bs) (plusinf p))" by (simp add: bound0_I[OF plusinf_nb[OF lp], where b=x and b'=a]) from plusinf_uset0[OF lp nmi' ex] - obtain c s where csU: "(c,s) \ set (uset p)" and th: "x \ - Itm vs (x#bs) s / Ipoly vs c" by blast - from uset_l[OF lp, rule_format, OF csU] have nb: "tmbound0 s" by simp - from th tmbound0_I[OF nb, of vs x bs a] csU show ?thesis by auto + obtain c s where csU: "(c,s) \ set (uset p)" + and th: "x \ - Itm vs (x#bs) s / Ipoly vs c" + by blast + from uset_l[OF lp, rule_format, OF csU] have nb: "tmbound0 s" + by simp + from th tmbound0_I[OF nb, of vs x bs a] csU show ?thesis + by auto qed lemma lin_dense: assumes lp: "islin p" - and noS: "\t. l < t \ t< u \ t \ (\ (c,t). - Itm vs (x#bs) t / Ipoly vs c) ` set (uset p)" - (is "\t. _ \ _ \ t \ (\ (c,t). - ?Nt x t / ?N c) ` ?U p") - and lx: "l < x" and xu:"x < u" and px:" Ifm vs (x#bs) p" - and ly: "l < y" and yu: "y < u" + and noS: "\t. l < t \ t< u \ t \ (\(c,t). - Itm vs (x#bs) t / Ipoly vs c) ` set (uset p)" + (is "\t. _ \ _ \ t \ (\(c,t). - ?Nt x t / ?N c) ` ?U p") + and lx: "l < x" and xu:"x < u" and px:" Ifm vs (x#bs) p" + and ly: "l < y" and yu: "y < u" shows "Ifm vs (y#bs) p" -using lp px noS + using lp px noS proof (induct p rule: islin.induct) case (5 c s) from "5.prems" have lin: "isnpoly c" "c \ 0\<^sub>p" "tmbound0 s" "allpolys isnpoly s" and px: "Ifm vs (x # bs) (Lt (CNP 0 c s))" - and noS: "\t. l < t \ t < u \ t \ - Itm vs (x # bs) s / \c\\<^sub>p\<^bsup>vs\<^esup>" by simp_all - from ly yu noS have yne: "y \ - ?Nt x s / \c\\<^sub>p\<^bsup>vs\<^esup>" by simp - hence ycs: "y < - ?Nt x s / ?N c \ y > -?Nt x s / ?N c" by auto - have ccs: "?N c = 0 \ ?N c < 0 \ ?N c > 0" by dlo - moreover - {assume "?N c = 0" hence ?case using px by (simp add: tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"])} + and noS: "\t. l < t \ t < u \ t \ - Itm vs (x # bs) s / \c\\<^sub>p\<^bsup>vs\<^esup>" + by simp_all + from ly yu noS have yne: "y \ - ?Nt x s / \c\\<^sub>p\<^bsup>vs\<^esup>" + by simp + then have ycs: "y < - ?Nt x s / ?N c \ y > -?Nt x s / ?N c" + by auto + have ccs: "?N c = 0 \ ?N c < 0 \ ?N c > 0" + by dlo moreover - {assume c: "?N c > 0" - from px pos_less_divide_eq[OF c, where a="x" and b="-?Nt x s"] - have px': "x < - ?Nt x s / ?N c" - by (auto simp add: not_less field_simps) - {assume y: "y < - ?Nt x s / ?N c" - hence "y * ?N c < - ?Nt x s" - by (simp add: pos_less_divide_eq[OF c, where a="y" and b="-?Nt x s", symmetric]) - hence "?N c * y + ?Nt x s < 0" by (simp add: field_simps) - hence ?case using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"] by simp} - moreover - {assume y: "y > -?Nt x s / ?N c" - with yu have eu: "u > - ?Nt x s / ?N c" by auto - with noS ly yu have th: "- ?Nt x s / ?N c \ l" by (cases "- ?Nt x s / ?N c > l", auto) - with lx px' have "False" by simp hence ?case by simp } - ultimately have ?case using ycs by blast + { + assume "?N c = 0" + then have ?case + using px by (simp add: tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"]) } moreover - {assume c: "?N c < 0" - from px neg_divide_less_eq[OF c, where a="x" and b="-?Nt x s"] - have px': "x > - ?Nt x s / ?N c" - by (auto simp add: not_less field_simps) - {assume y: "y > - ?Nt x s / ?N c" - hence "y * ?N c < - ?Nt x s" + { + assume c: "?N c > 0" + from px pos_less_divide_eq[OF c, where a="x" and b="-?Nt x s"] + have px': "x < - ?Nt x s / ?N c" + by (auto simp add: not_less field_simps) + { + assume y: "y < - ?Nt x s / ?N c" + then have "y * ?N c < - ?Nt x s" + by (simp add: pos_less_divide_eq[OF c, where a="y" and b="-?Nt x s", symmetric]) + then have "?N c * y + ?Nt x s < 0" + by (simp add: field_simps) + then have ?case using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"] + by simp + } + moreover + { + assume y: "y > -?Nt x s / ?N c" + with yu have eu: "u > - ?Nt x s / ?N c" + by auto + with noS ly yu have th: "- ?Nt x s / ?N c \ l" + by (cases "- ?Nt x s / ?N c > l") auto + with lx px' have False + by simp + then have ?case .. + } + ultimately have ?case + using ycs by blast + } + moreover + { + assume c: "?N c < 0" + from px neg_divide_less_eq[OF c, where a="x" and b="-?Nt x s"] + have px': "x > - ?Nt x s / ?N c" + by (auto simp add: not_less field_simps) + { + assume y: "y > - ?Nt x s / ?N c" + then have "y * ?N c < - ?Nt x s" by (simp add: neg_divide_less_eq[OF c, where a="y" and b="-?Nt x s", symmetric]) - hence "?N c * y + ?Nt x s < 0" by (simp add: field_simps) - hence ?case using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"] by simp} + then have "?N c * y + ?Nt x s < 0" + by (simp add: field_simps) + then have ?case using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"] + by simp + } moreover - {assume y: "y < -?Nt x s / ?N c" - with ly have eu: "l < - ?Nt x s / ?N c" by auto - with noS ly yu have th: "- ?Nt x s / ?N c \ u" by (cases "- ?Nt x s / ?N c < u", auto) - with xu px' have "False" by simp hence ?case by simp } - ultimately have ?case using ycs by blast + { + assume y: "y < -?Nt x s / ?N c" + with ly have eu: "l < - ?Nt x s / ?N c" + by auto + with noS ly yu have th: "- ?Nt x s / ?N c \ u" + by (cases "- ?Nt x s / ?N c < u") auto + with xu px' have False + by simp + then have ?case .. + } + ultimately have ?case + using ycs by blast } - ultimately show ?case by blast + ultimately show ?case + by blast next case (6 c s) from "6.prems" have lin: "isnpoly c" "c \ 0\<^sub>p" "tmbound0 s" "allpolys isnpoly s" and px: "Ifm vs (x # bs) (Le (CNP 0 c s))" - and noS: "\t. l < t \ t < u \ t \ - Itm vs (x # bs) s / \c\\<^sub>p\<^bsup>vs\<^esup>" by simp_all - from ly yu noS have yne: "y \ - ?Nt x s / \c\\<^sub>p\<^bsup>vs\<^esup>" by simp - hence ycs: "y < - ?Nt x s / ?N c \ y > -?Nt x s / ?N c" by auto + and noS: "\t. l < t \ t < u \ t \ - Itm vs (x # bs) s / \c\\<^sub>p\<^bsup>vs\<^esup>" + by simp_all + from ly yu noS have yne: "y \ - ?Nt x s / \c\\<^sub>p\<^bsup>vs\<^esup>" + by simp + then have ycs: "y < - ?Nt x s / ?N c \ y > -?Nt x s / ?N c" + by auto have ccs: "?N c = 0 \ ?N c < 0 \ ?N c > 0" by dlo moreover - {assume "?N c = 0" hence ?case using px by (simp add: tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"])} - moreover - {assume c: "?N c > 0" - from px pos_le_divide_eq[OF c, where a="x" and b="-?Nt x s"] - have px': "x <= - ?Nt x s / ?N c" by (simp add: not_less field_simps) - {assume y: "y < - ?Nt x s / ?N c" - hence "y * ?N c < - ?Nt x s" - by (simp add: pos_less_divide_eq[OF c, where a="y" and b="-?Nt x s", symmetric]) - hence "?N c * y + ?Nt x s < 0" by (simp add: field_simps) - hence ?case using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"] by simp} - moreover - {assume y: "y > -?Nt x s / ?N c" - with yu have eu: "u > - ?Nt x s / ?N c" by auto - with noS ly yu have th: "- ?Nt x s / ?N c \ l" by (cases "- ?Nt x s / ?N c > l", auto) - with lx px' have "False" by simp hence ?case by simp } - ultimately have ?case using ycs by blast + { + assume "?N c = 0" + then have ?case + using px by (simp add: tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"]) } moreover - {assume c: "?N c < 0" - from px neg_divide_le_eq[OF c, where a="x" and b="-?Nt x s"] - have px': "x >= - ?Nt x s / ?N c" by (simp add: field_simps) - {assume y: "y > - ?Nt x s / ?N c" - hence "y * ?N c < - ?Nt x s" - by (simp add: neg_divide_less_eq[OF c, where a="y" and b="-?Nt x s", symmetric]) - hence "?N c * y + ?Nt x s < 0" by (simp add: field_simps) - hence ?case using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"] by simp} + { + assume c: "?N c > 0" + from px pos_le_divide_eq[OF c, where a="x" and b="-?Nt x s"] + have px': "x \ - ?Nt x s / ?N c" + by (simp add: not_less field_simps) + { + assume y: "y < - ?Nt x s / ?N c" + then have "y * ?N c < - ?Nt x s" + by (simp add: pos_less_divide_eq[OF c, where a="y" and b="-?Nt x s", symmetric]) + then have "?N c * y + ?Nt x s < 0" + by (simp add: field_simps) + then have ?case + using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"] by simp + } moreover - {assume y: "y < -?Nt x s / ?N c" - with ly have eu: "l < - ?Nt x s / ?N c" by auto - with noS ly yu have th: "- ?Nt x s / ?N c \ u" by (cases "- ?Nt x s / ?N c < u", auto) - with xu px' have "False" by simp hence ?case by simp } - ultimately have ?case using ycs by blast + { + assume y: "y > -?Nt x s / ?N c" + with yu have eu: "u > - ?Nt x s / ?N c" + by auto + with noS ly yu have th: "- ?Nt x s / ?N c \ l" + by (cases "- ?Nt x s / ?N c > l") auto + with lx px' have False + by simp + then have ?case .. + } + ultimately have ?case + using ycs by blast } - ultimately show ?case by blast + moreover + { + assume c: "?N c < 0" + from px neg_divide_le_eq[OF c, where a="x" and b="-?Nt x s"] + have px': "x >= - ?Nt x s / ?N c" + by (simp add: field_simps) + { + assume y: "y > - ?Nt x s / ?N c" + then have "y * ?N c < - ?Nt x s" + by (simp add: neg_divide_less_eq[OF c, where a="y" and b="-?Nt x s", symmetric]) + then have "?N c * y + ?Nt x s < 0" + by (simp add: field_simps) + then have ?case + using tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"] by simp + } + moreover + { + assume y: "y < -?Nt x s / ?N c" + with ly have eu: "l < - ?Nt x s / ?N c" + by auto + with noS ly yu have th: "- ?Nt x s / ?N c \ u" + by (cases "- ?Nt x s / ?N c < u") auto + with xu px' have False by simp + then have ?case .. + } + ultimately have ?case + using ycs by blast + } + ultimately show ?case + by blast next - case (3 c s) + case (3 c s) from "3.prems" have lin: "isnpoly c" "c \ 0\<^sub>p" "tmbound0 s" "allpolys isnpoly s" and px: "Ifm vs (x # bs) (Eq (CNP 0 c s))" - and noS: "\t. l < t \ t < u \ t \ - Itm vs (x # bs) s / \c\\<^sub>p\<^bsup>vs\<^esup>" by simp_all - from ly yu noS have yne: "y \ - ?Nt x s / \c\\<^sub>p\<^bsup>vs\<^esup>" by simp - hence ycs: "y < - ?Nt x s / ?N c \ y > -?Nt x s / ?N c" by auto + and noS: "\t. l < t \ t < u \ t \ - Itm vs (x # bs) s / \c\\<^sub>p\<^bsup>vs\<^esup>" + by simp_all + from ly yu noS have yne: "y \ - ?Nt x s / \c\\<^sub>p\<^bsup>vs\<^esup>" + by simp + then have ycs: "y < - ?Nt x s / ?N c \ y > -?Nt x s / ?N c" + by auto have ccs: "?N c = 0 \ ?N c < 0 \ ?N c > 0" by dlo moreover - {assume "?N c = 0" hence ?case using px by (simp add: tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"])} - moreover - {assume c: "?N c > 0" hence cnz: "?N c \ 0" by simp - from px eq_divide_eq[of "x" "-?Nt x s" "?N c"] cnz - have px': "x = - ?Nt x s / ?N c" by (simp add: field_simps) - {assume y: "y < -?Nt x s / ?N c" - with ly have eu: "l < - ?Nt x s / ?N c" by auto - with noS ly yu have th: "- ?Nt x s / ?N c \ u" by (cases "- ?Nt x s / ?N c < u", auto) - with xu px' have "False" by simp hence ?case by simp } - moreover - {assume y: "y > -?Nt x s / ?N c" - with yu have eu: "u > - ?Nt x s / ?N c" by auto - with noS ly yu have th: "- ?Nt x s / ?N c \ l" by (cases "- ?Nt x s / ?N c > l", auto) - with lx px' have "False" by simp hence ?case by simp } - ultimately have ?case using ycs by blast + { + assume "?N c = 0" + then have ?case + using px by (simp add: tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"]) } moreover - {assume c: "?N c < 0" hence cnz: "?N c \ 0" by simp - from px eq_divide_eq[of "x" "-?Nt x s" "?N c"] cnz - have px': "x = - ?Nt x s / ?N c" by (simp add: field_simps) - {assume y: "y < -?Nt x s / ?N c" - with ly have eu: "l < - ?Nt x s / ?N c" by auto - with noS ly yu have th: "- ?Nt x s / ?N c \ u" by (cases "- ?Nt x s / ?N c < u", auto) - with xu px' have "False" by simp hence ?case by simp } + { + assume c: "?N c > 0" + then have cnz: "?N c \ 0" + by simp + from px eq_divide_eq[of "x" "-?Nt x s" "?N c"] cnz + have px': "x = - ?Nt x s / ?N c" + by (simp add: field_simps) + { + assume y: "y < -?Nt x s / ?N c" + with ly have eu: "l < - ?Nt x s / ?N c" + by auto + with noS ly yu have th: "- ?Nt x s / ?N c \ u" + by (cases "- ?Nt x s / ?N c < u") auto + with xu px' have False by simp + then have ?case .. + } moreover - {assume y: "y > -?Nt x s / ?N c" - with yu have eu: "u > - ?Nt x s / ?N c" by auto - with noS ly yu have th: "- ?Nt x s / ?N c \ l" by (cases "- ?Nt x s / ?N c > l", auto) - with lx px' have "False" by simp hence ?case by simp } + { + assume y: "y > -?Nt x s / ?N c" + with yu have eu: "u > - ?Nt x s / ?N c" + by auto + with noS ly yu have th: "- ?Nt x s / ?N c \ l" + by (cases "- ?Nt x s / ?N c > l") auto + with lx px' have False by simp + then have ?case .. + } + ultimately have ?case + using ycs by blast + } + moreover + { + assume c: "?N c < 0" + then have cnz: "?N c \ 0" + by simp + from px eq_divide_eq[of "x" "-?Nt x s" "?N c"] cnz + have px': "x = - ?Nt x s / ?N c" + by (simp add: field_simps) + { + assume y: "y < -?Nt x s / ?N c" + with ly have eu: "l < - ?Nt x s / ?N c" + by auto + with noS ly yu have th: "- ?Nt x s / ?N c \ u" + by (cases "- ?Nt x s / ?N c < u") auto + with xu px' have False by simp + then have ?case .. + } + moreover + { + assume y: "y > -?Nt x s / ?N c" + with yu have eu: "u > - ?Nt x s / ?N c" + by auto + with noS ly yu have th: "- ?Nt x s / ?N c \ l" + by (cases "- ?Nt x s / ?N c > l") auto + with lx px' have False by simp + then have ?case .. + } ultimately have ?case using ycs by blast } ultimately show ?case by blast @@ -1927,136 +2458,228 @@ from "4.prems" have lin: "isnpoly c" "c \ 0\<^sub>p" "tmbound0 s" "allpolys isnpoly s" and px: "Ifm vs (x # bs) (NEq (CNP 0 c s))" - and noS: "\t. l < t \ t < u \ t \ - Itm vs (x # bs) s / \c\\<^sub>p\<^bsup>vs\<^esup>" by simp_all - from ly yu noS have yne: "y \ - ?Nt x s / \c\\<^sub>p\<^bsup>vs\<^esup>" by simp - hence ycs: "y < - ?Nt x s / ?N c \ y > -?Nt x s / ?N c" by auto + and noS: "\t. l < t \ t < u \ t \ - Itm vs (x # bs) s / \c\\<^sub>p\<^bsup>vs\<^esup>" + by simp_all + from ly yu noS have yne: "y \ - ?Nt x s / \c\\<^sub>p\<^bsup>vs\<^esup>" + by simp + then have ycs: "y < - ?Nt x s / ?N c \ y > -?Nt x s / ?N c" + by auto have ccs: "?N c = 0 \ ?N c \ 0" by dlo moreover - {assume "?N c = 0" hence ?case using px by (simp add: tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"])} + { + assume "?N c = 0" + then have ?case + using px by (simp add: tmbound0_I[OF lin(3), where bs="bs" and b="x" and b'="y"]) + } moreover - {assume c: "?N c \ 0" - from yne c eq_divide_eq[of "y" "- ?Nt x s" "?N c"] have ?case - by (simp add: field_simps tmbound0_I[OF lin(3), of vs x bs y] sum_eq[symmetric]) } - ultimately show ?case by blast + { + assume c: "?N c \ 0" + from yne c eq_divide_eq[of "y" "- ?Nt x s" "?N c"] + have ?case + by (simp add: field_simps tmbound0_I[OF lin(3), of vs x bs y] sum_eq[symmetric]) + } + ultimately show ?case + by blast qed (auto simp add: tmbound0_I[where vs=vs and bs="bs" and b="y" and b'="x"] bound0_I[where vs=vs and bs="bs" and b="y" and b'="x"]) lemma inf_uset: assumes lp: "islin p" - and nmi: "\ (Ifm vs (x#bs) (minusinf p))" (is "\ (Ifm vs (x#bs) (?M p))") - and npi: "\ (Ifm vs (x#bs) (plusinf p))" (is "\ (Ifm vs (x#bs) (?P p))") - and ex: "\x. Ifm vs (x#bs) p" (is "\x. ?I x p") - shows "\(c,t) \ set (uset p). \(d,s) \ set (uset p). ?I ((- Itm vs (x#bs) t / Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) / 2) p" -proof- - let ?Nt = "\ x t. Itm vs (x#bs) t" + and nmi: "\ (Ifm vs (x#bs) (minusinf p))" (is "\ (Ifm vs (x#bs) (?M p))") + and npi: "\ (Ifm vs (x#bs) (plusinf p))" (is "\ (Ifm vs (x#bs) (?P p))") + and ex: "\x. Ifm vs (x#bs) p" (is "\x. ?I x p") + shows "\(c, t) \ set (uset p). \(d, s) \ set (uset p). + ?I ((- Itm vs (x#bs) t / Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) / 2) p" +proof - + let ?Nt = "\x t. Itm vs (x#bs) t" let ?N = "Ipoly vs" let ?U = "set (uset p)" - from ex obtain a where pa: "?I a p" by blast + from ex obtain a where pa: "?I a p" + by blast from bound0_I[OF minusinf_nb[OF lp], where bs="bs" and b="x" and b'="a"] nmi - have nmi': "\ (?I a (?M p))" by simp + have nmi': "\ (?I a (?M p))" + by simp from bound0_I[OF plusinf_nb[OF lp], where bs="bs" and b="x" and b'="a"] npi - have npi': "\ (?I a (?P p))" by simp + have npi': "\ (?I a (?P p))" + by simp have "\(c,t) \ set (uset p). \(d,s) \ set (uset p). ?I ((- ?Nt a t/?N c + - ?Nt a s /?N d) / 2) p" - proof- - let ?M = "(\ (c,t). - ?Nt a t / ?N c) ` ?U" - have fM: "finite ?M" by auto + proof - + let ?M = "(\(c,t). - ?Nt a t / ?N c) ` ?U" + have fM: "finite ?M" + by auto from minusinf_uset[OF lp nmi pa] plusinf_uset[OF lp npi pa] - have "\(c,t) \ set (uset p). \(d,s) \ set (uset p). a \ - ?Nt x t / ?N c \ a \ - ?Nt x s / ?N d" by blast - then obtain "c" "t" "d" "s" where - ctU: "(c,t) \ ?U" and dsU: "(d,s) \ ?U" - and xs1: "a \ - ?Nt x s / ?N d" and tx1: "a \ - ?Nt x t / ?N c" by blast + have "\(c, t) \ set (uset p). \(d, s) \ set (uset p). + a \ - ?Nt x t / ?N c \ a \ - ?Nt x s / ?N d" + by blast + then obtain "c" "t" "d" "s" + where ctU: "(c,t) \ ?U" + and dsU: "(d,s) \ ?U" + and xs1: "a \ - ?Nt x s / ?N d" + and tx1: "a \ - ?Nt x t / ?N c" + by blast from uset_l[OF lp] ctU dsU tmbound0_I[where bs="bs" and b="x" and b'="a"] xs1 tx1 - have xs: "a \ - ?Nt a s / ?N d" and tx: "a \ - ?Nt a t / ?N c" by auto + have xs: "a \ - ?Nt a s / ?N d" and tx: "a \ - ?Nt a t / ?N c" + by auto from ctU have Mne: "?M \ {}" by auto - hence Une: "?U \ {}" by simp + then have Une: "?U \ {}" by simp let ?l = "Min ?M" let ?u = "Max ?M" - have linM: "?l \ ?M" using fM Mne by simp - have uinM: "?u \ ?M" using fM Mne by simp - have ctM: "- ?Nt a t / ?N c \ ?M" using ctU by auto - have dsM: "- ?Nt a s / ?N d \ ?M" using dsU by auto - have lM: "\t\ ?M. ?l \ t" using Mne fM by auto - have Mu: "\t\ ?M. t \ ?u" using Mne fM by auto - have "?l \ - ?Nt a t / ?N c" using ctM Mne by simp hence lx: "?l \ a" using tx by simp - have "- ?Nt a s / ?N d \ ?u" using dsM Mne by simp hence xu: "a \ ?u" using xs by simp - from finite_set_intervals2[where P="\ x. ?I x p",OF pa lx xu linM uinM fM lM Mu] + have linM: "?l \ ?M" + using fM Mne by simp + have uinM: "?u \ ?M" + using fM Mne by simp + have ctM: "- ?Nt a t / ?N c \ ?M" + using ctU by auto + have dsM: "- ?Nt a s / ?N d \ ?M" + using dsU by auto + have lM: "\t\ ?M. ?l \ t" + using Mne fM by auto + have Mu: "\t\ ?M. t \ ?u" + using Mne fM by auto + have "?l \ - ?Nt a t / ?N c" + using ctM Mne by simp + then have lx: "?l \ a" + using tx by simp + have "- ?Nt a s / ?N d \ ?u" + using dsM Mne by simp + then have xu: "a \ ?u" + using xs by simp + from finite_set_intervals2[where P="\x. ?I x p",OF pa lx xu linM uinM fM lM Mu] have "(\s\ ?M. ?I s p) \ (\t1\ ?M. \t2 \ ?M. (\y. t1 < y \ y < t2 \ y \ ?M) \ t1 < a \ a < t2 \ ?I a p)" . - moreover {fix u assume um: "u\ ?M" and pu: "?I u p" - hence "\(nu,tu) \ ?U. u = - ?Nt a tu / ?N nu" by auto - then obtain "tu" "nu" where tuU: "(nu,tu) \ ?U" and tuu:"u= - ?Nt a tu / ?N nu" by blast - from pu tuu - have "?I (((- ?Nt a tu / ?N nu) + (- ?Nt a tu / ?N nu)) / 2) p" by simp - with tuU have ?thesis by blast} - moreover{ + moreover { + fix u + assume um: "u\ ?M" + and pu: "?I u p" + then have "\(nu,tu) \ ?U. u = - ?Nt a tu / ?N nu" + by auto + then obtain tu nu where tuU: "(nu, tu) \ ?U" + and tuu:"u= - ?Nt a tu / ?N nu" + by blast + from pu tuu have "?I (((- ?Nt a tu / ?N nu) + (- ?Nt a tu / ?N nu)) / 2) p" + by simp + with tuU have ?thesis by blast + } + moreover { assume "\t1\ ?M. \t2 \ ?M. (\y. t1 < y \ y < t2 \ y \ ?M) \ t1 < a \ a < t2 \ ?I a p" - then obtain t1 and t2 where t1M: "t1 \ ?M" and t2M: "t2\ ?M" - and noM: "\y. t1 < y \ y < t2 \ y \ ?M" and t1x: "t1 < a" and xt2: "a < t2" and px: "?I a p" + then obtain t1 t2 + where t1M: "t1 \ ?M" + and t2M: "t2\ ?M" + and noM: "\y. t1 < y \ y < t2 \ y \ ?M" + and t1x: "t1 < a" + and xt2: "a < t2" + and px: "?I a p" by blast - from t1M have "\(t1n,t1u) \ ?U. t1 = - ?Nt a t1u / ?N t1n" by auto - then obtain "t1u" "t1n" where t1uU: "(t1n,t1u) \ ?U" and t1u: "t1 = - ?Nt a t1u / ?N t1n" by blast - from t2M have "\(t2n,t2u) \ ?U. t2 = - ?Nt a t2u / ?N t2n" by auto - then obtain "t2u" "t2n" where t2uU: "(t2n,t2u) \ ?U" and t2u: "t2 = - ?Nt a t2u / ?N t2n" by blast + from t1M have "\(t1n, t1u) \ ?U. t1 = - ?Nt a t1u / ?N t1n" + by auto + then obtain t1u t1n where t1uU: "(t1n, t1u) \ ?U" + and t1u: "t1 = - ?Nt a t1u / ?N t1n" + by blast + from t2M have "\(t2n, t2u) \ ?U. t2 = - ?Nt a t2u / ?N t2n" + by auto + then obtain t2u t2n where t2uU: "(t2n, t2u) \ ?U" + and t2u: "t2 = - ?Nt a t2u / ?N t2n" + by blast from t1x xt2 have t1t2: "t1 < t2" by simp let ?u = "(t1 + t2) / 2" - from less_half_sum[OF t1t2] gt_half_sum[OF t1t2] have t1lu: "t1 < ?u" and ut2: "?u < t2" by auto + from less_half_sum[OF t1t2] gt_half_sum[OF t1t2] have t1lu: "t1 < ?u" and ut2: "?u < t2" + by auto from lin_dense[OF lp noM t1x xt2 px t1lu ut2] have "?I ?u p" . - with t1uU t2uU t1u t2u have ?thesis by blast} + with t1uU t2uU t1u t2u have ?thesis by blast + } ultimately show ?thesis by blast qed - then obtain "l" "n" "s" "m" where lnU: "(n,l) \ ?U" and smU:"(m,s) \ ?U" - and pu: "?I ((- ?Nt a l / ?N n + - ?Nt a s / ?N m) / 2) p" by blast - from lnU smU uset_l[OF lp] have nbl: "tmbound0 l" and nbs: "tmbound0 s" by auto + then obtain l n s m + where lnU: "(n, l) \ ?U" + and smU:"(m,s) \ ?U" + and pu: "?I ((- ?Nt a l / ?N n + - ?Nt a s / ?N m) / 2) p" + by blast + from lnU smU uset_l[OF lp] have nbl: "tmbound0 l" and nbs: "tmbound0 s" + by auto from tmbound0_I[OF nbl, where bs="bs" and b="a" and b'="x"] tmbound0_I[OF nbs, where bs="bs" and b="a" and b'="x"] pu - have "?I ((- ?Nt x l / ?N n + - ?Nt x s / ?N m) / 2) p" by simp - with lnU smU - show ?thesis by auto + have "?I ((- ?Nt x l / ?N n + - ?Nt x s / ?N m) / 2) p" + by simp + with lnU smU show ?thesis by auto qed - (* The Ferrante - Rackoff Theorem *) +(* The Ferrante - Rackoff Theorem *) theorem fr_eq: assumes lp: "islin p" - shows "(\x. Ifm vs (x#bs) p) = ((Ifm vs (x#bs) (minusinf p)) \ (Ifm vs (x#bs) (plusinf p)) \ (\(n,t) \ set (uset p). \(m,s) \ set (uset p). Ifm vs (((- Itm vs (x#bs) t / Ipoly vs n + - Itm vs (x#bs) s / Ipoly vs m) / 2)#bs) p))" + shows "(\x. Ifm vs (x#bs) p) \ + (Ifm vs (x#bs) (minusinf p) \ + Ifm vs (x#bs) (plusinf p) \ + (\(n, t) \ set (uset p). \(m, s) \ set (uset p). + Ifm vs (((- Itm vs (x#bs) t / Ipoly vs n + - Itm vs (x#bs) s / Ipoly vs m) / 2)#bs) p))" (is "(\x. ?I x p) = (?M \ ?P \ ?F)" is "?E = ?D") proof assume px: "\x. ?I x p" - have "?M \ ?P \ (\ ?M \ \ ?P)" by blast - moreover {assume "?M \ ?P" hence "?D" by blast} - moreover {assume nmi: "\ ?M" and npi: "\ ?P" - from inf_uset[OF lp nmi npi] have "?F" using px by blast hence "?D" by blast} - ultimately show "?D" by blast + have "?M \ ?P \ (\ ?M \ \ ?P)" + by blast + moreover { + assume "?M \ ?P" + then have "?D" by blast + } + moreover { + assume nmi: "\ ?M" + and npi: "\ ?P" + from inf_uset[OF lp nmi npi] have ?F + using px by blast + then have ?D by blast + } + ultimately show ?D by blast next - assume "?D" - moreover {assume m:"?M" from minusinf_ex[OF lp m] have "?E" .} - moreover {assume p: "?P" from plusinf_ex[OF lp p] have "?E" . } - moreover {assume f:"?F" hence "?E" by blast} - ultimately show "?E" by blast + assume ?D + moreover { + assume m: ?M + from minusinf_ex[OF lp m] have ?E . + } + moreover { + assume p: ?P + from plusinf_ex[OF lp p] have ?E . + } + moreover { + assume f: ?F + then have ?E by blast + } + ultimately show ?E by blast qed -section{* First implementation : Naive by encoding all case splits locally *} + +section {* First implementation : Naive by encoding all case splits locally *} + definition "msubsteq c t d s a r = evaldjf (split conj) - [(let cd = c *\<^sub>p d in (NEq (CP cd), Eq (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), - (conj (Eq (CP c)) (NEq (CP d)) , Eq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), - (conj (NEq (CP c)) (Eq (CP d)) , Eq (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), - (conj (Eq (CP c)) (Eq (CP d)) , Eq r)]" - -lemma msubsteq_nb: assumes lp: "islin (Eq (CNP 0 a r))" and t: "tmbound0 t" and s: "tmbound0 s" + [(let cd = c *\<^sub>p d + in (NEq (CP cd), Eq (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), + (conj (Eq (CP c)) (NEq (CP d)), Eq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), + (conj (NEq (CP c)) (Eq (CP d)), Eq (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), + (conj (Eq (CP c)) (Eq (CP d)), Eq r)]" + +lemma msubsteq_nb: + assumes lp: "islin (Eq (CNP 0 a r))" + and t: "tmbound0 t" + and s: "tmbound0 s" shows "bound0 (msubsteq c t d s a r)" -proof- - have th: "\x\ set [(let cd = c *\<^sub>p d in (NEq (CP cd), Eq (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), - (conj (Eq (CP c)) (NEq (CP d)) , Eq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), - (conj (NEq (CP c)) (Eq (CP d)) , Eq (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), - (conj (Eq (CP c)) (Eq (CP d)) , Eq r)]. bound0 (split conj x)" - using lp by (simp add: Let_def t s ) - from evaldjf_bound0[OF th] show ?thesis by (simp add: msubsteq_def) +proof - + have th: "\x \ set + [(let cd = c *\<^sub>p d + in (NEq (CP cd), Eq (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), + (conj (Eq (CP c)) (NEq (CP d)), Eq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), + (conj (NEq (CP c)) (Eq (CP d)), Eq (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), + (conj (Eq (CP c)) (Eq (CP d)), Eq r)]. bound0 (split conj x)" + using lp by (simp add: Let_def t s) + from evaldjf_bound0[OF th] show ?thesis + by (simp add: msubsteq_def) qed -lemma msubsteq: assumes lp: "islin (Eq (CNP 0 a r))" - shows "Ifm vs (x#bs) (msubsteq c t d s a r) = Ifm vs (((- Itm vs (x#bs) t / Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) / 2)#bs) (Eq (CNP 0 a r))" (is "?lhs = ?rhs") -proof- - let ?Nt = "\(x::'a) t. Itm vs (x#bs) t" +lemma msubsteq: + assumes lp: "islin (Eq (CNP 0 a r))" + shows "Ifm vs (x#bs) (msubsteq c t d s a r) = + Ifm vs (((- Itm vs (x#bs) t / Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) / 2)#bs) (Eq (CNP 0 a r))" + (is "?lhs = ?rhs") +proof - + let ?Nt = "\x t. Itm vs (x#bs) t" let ?N = "\p. Ipoly vs p" let ?c = "?N c" let ?d = "?N d" @@ -2064,81 +2687,116 @@ let ?s = "?Nt x s" let ?a = "?N a" let ?r = "?Nt x r" - from lp have lin:"isnpoly a" "a \ 0\<^sub>p" "tmbound0 r" "allpolys isnpoly r" by simp_all + from lp have lin:"isnpoly a" "a \ 0\<^sub>p" "tmbound0 r" "allpolys isnpoly r" + by simp_all note r= tmbound0_I[OF lin(3), of vs _ bs x] - have cd_cs: "?c * ?d \ 0 \ (?c = 0 \ ?d = 0) \ (?c = 0 \ ?d \ 0) \ (?c \ 0 \ ?d = 0)" by auto + have cd_cs: "?c * ?d \ 0 \ (?c = 0 \ ?d = 0) \ (?c = 0 \ ?d \ 0) \ (?c \ 0 \ ?d = 0)" + by auto moreover - {assume c: "?c = 0" and d: "?d=0" - hence ?thesis by (simp add: r[of 0] msubsteq_def Let_def evaldjf_ex)} + { + assume c: "?c = 0" + and d: "?d=0" + then have ?thesis + by (simp add: r[of 0] msubsteq_def Let_def evaldjf_ex) + } moreover - {assume c: "?c = 0" and d: "?d\0" - from c have th: "(- ?t / ?c + - ?s / ?d)/2 = -?s / (2*?d)" by simp - have "?rhs = Ifm vs (-?s / (2*?d) # bs) (Eq (CNP 0 a r))" by (simp only: th) - also have "\ \ ?a * (-?s / (2*?d)) + ?r = 0" by (simp add: r[of "- (Itm vs (x # bs) s / (2 * \d\\<^sub>p\<^bsup>vs\<^esup>))"]) - also have "\ \ 2*?d * (?a * (-?s / (2*?d)) + ?r) = 0" + { + assume c: "?c = 0" + and d: "?d\0" + from c have th: "(- ?t / ?c + - ?s / ?d)/2 = -?s / (2*?d)" + by simp + have "?rhs = Ifm vs (-?s / (2*?d) # bs) (Eq (CNP 0 a r))" + by (simp only: th) + also have "\ \ ?a * (-?s / (2*?d)) + ?r = 0" + by (simp add: r[of "- (Itm vs (x # bs) s / (2 * \d\\<^sub>p\<^bsup>vs\<^esup>))"]) + also have "\ \ 2 * ?d * (?a * (-?s / (2*?d)) + ?r) = 0" using d mult_cancel_left[of "2*?d" "(?a * (-?s / (2*?d)) + ?r)" 0] by simp - also have "\ \ (- ?a * ?s) * (2*?d / (2*?d)) + 2*?d*?r= 0" + also have "\ \ (- ?a * ?s) * (2*?d / (2*?d)) + 2 * ?d * ?r= 0" by (simp add: field_simps distrib_left[of "2*?d"] del: distrib_left) - - also have "\ \ - (?a * ?s) + 2*?d*?r = 0" using d by simp - finally have ?thesis using c d + also have "\ \ - (?a * ?s) + 2*?d*?r = 0" + using d by simp + finally have ?thesis + using c d by (simp add: r[of "- (Itm vs (x # bs) s / (2 * \d\\<^sub>p\<^bsup>vs\<^esup>))"] msubsteq_def Let_def evaldjf_ex) } moreover - {assume c: "?c \ 0" and d: "?d=0" - from d have th: "(- ?t / ?c + - ?s / ?d)/2 = -?t / (2*?c)" by simp - have "?rhs = Ifm vs (-?t / (2*?c) # bs) (Eq (CNP 0 a r))" by (simp only: th) - also have "\ \ ?a * (-?t / (2*?c)) + ?r = 0" by (simp add: r[of "- (?t/ (2 * ?c))"]) - also have "\ \ 2*?c * (?a * (-?t / (2*?c)) + ?r) = 0" - using c mult_cancel_left[of "2*?c" "(?a * (-?t / (2*?c)) + ?r)" 0] by simp - also have "\ \ (?a * -?t)* (2*?c) / (2*?c) + 2*?c*?r= 0" - by (simp add: field_simps distrib_left[of "2*?c"] del: distrib_left) - also have "\ \ - (?a * ?t) + 2*?c*?r = 0" using c by simp + { + assume c: "?c \ 0" + and d: "?d = 0" + from d have th: "(- ?t / ?c + - ?s / ?d)/2 = -?t / (2 * ?c)" + by simp + have "?rhs = Ifm vs (-?t / (2*?c) # bs) (Eq (CNP 0 a r))" + by (simp only: th) + also have "\ \ ?a * (-?t / (2*?c)) + ?r = 0" + by (simp add: r[of "- (?t/ (2 * ?c))"]) + also have "\ \ 2 * ?c * (?a * (-?t / (2 * ?c)) + ?r) = 0" + using c mult_cancel_left[of "2 * ?c" "(?a * (-?t / (2 * ?c)) + ?r)" 0] by simp + also have "\ \ (?a * -?t)* (2 * ?c) / (2 * ?c) + 2 * ?c * ?r= 0" + by (simp add: field_simps distrib_left[of "2 * ?c"] del: distrib_left) + also have "\ \ - (?a * ?t) + 2 * ?c * ?r = 0" using c by simp finally have ?thesis using c d - by (simp add: r[of "- (?t/ (2*?c))"] msubsteq_def Let_def evaldjf_ex) + by (simp add: r[of "- (?t/ (2 * ?c))"] msubsteq_def Let_def evaldjf_ex) } moreover - {assume c: "?c \ 0" and d: "?d\0" hence dc: "?c * ?d *2 \ 0" by simp + { + assume c: "?c \ 0" + and d: "?d \ 0" + then have dc: "?c * ?d * 2 \ 0" + by simp from add_frac_eq[OF c d, of "- ?t" "- ?s"] - have th: "(- ?t / ?c + - ?s / ?d)/2 = - (?d * ?t + ?c* ?s )/ (2*?c*?d)" + have th: "(- ?t / ?c + - ?s / ?d)/2 = - (?d * ?t + ?c* ?s )/ (2 * ?c * ?d)" by (simp add: field_simps) - have "?rhs \ Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (Eq (CNP 0 a r))" by (simp only: th) + have "?rhs \ Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (Eq (CNP 0 a r))" + by (simp only: th) also have "\ \ ?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r = 0" by (simp add: r [of "(- (?d * ?t) - (?c *?s)) / (2 * ?c * ?d)"]) - also have "\ \ (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) =0 " - using c d mult_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0] by simp - also have "\ \ ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r =0" + also have "\ \ (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) = 0" + using c d mult_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2 * ?c * ?d)) + ?r" 0] + by simp + also have "\ \ ?a * (- (?d * ?t + ?c* ?s )) + 2 * ?c * ?d * ?r = 0" using nonzero_mult_divide_cancel_left [OF dc] c d by (simp add: algebra_simps diff_divide_distrib del: distrib_right) finally have ?thesis using c d - by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubsteq_def Let_def evaldjf_ex field_simps) + by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] + msubsteq_def Let_def evaldjf_ex field_simps) } - ultimately show ?thesis by blast + ultimately show ?thesis + by blast qed definition "msubstneq c t d s a r = evaldjf (split conj) - [(let cd = c *\<^sub>p d in (NEq (CP cd), NEq (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), - (conj (Eq (CP c)) (NEq (CP d)) , NEq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), - (conj (NEq (CP c)) (Eq (CP d)) , NEq (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), - (conj (Eq (CP c)) (Eq (CP d)) , NEq r)]" - -lemma msubstneq_nb: assumes lp: "islin (NEq (CNP 0 a r))" and t: "tmbound0 t" and s: "tmbound0 s" + [(let cd = c *\<^sub>p d + in (NEq (CP cd), NEq (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), + (conj (Eq (CP c)) (NEq (CP d)), NEq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), + (conj (NEq (CP c)) (Eq (CP d)), NEq (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), + (conj (Eq (CP c)) (Eq (CP d)), NEq r)]" + +lemma msubstneq_nb: + assumes lp: "islin (NEq (CNP 0 a r))" + and t: "tmbound0 t" + and s: "tmbound0 s" shows "bound0 (msubstneq c t d s a r)" -proof- - have th: "\x\ set [(let cd = c *\<^sub>p d in (NEq (CP cd), NEq (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), - (conj (Eq (CP c)) (NEq (CP d)) , NEq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), - (conj (NEq (CP c)) (Eq (CP d)) , NEq (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), - (conj (Eq (CP c)) (Eq (CP d)) , NEq r)]. bound0 (split conj x)" - using lp by (simp add: Let_def t s ) - from evaldjf_bound0[OF th] show ?thesis by (simp add: msubstneq_def) +proof - + have th: "\x\ set + [(let cd = c *\<^sub>p d + in (NEq (CP cd), NEq (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), + (conj (Eq (CP c)) (NEq (CP d)), NEq (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), + (conj (NEq (CP c)) (Eq (CP d)), NEq (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), + (conj (Eq (CP c)) (Eq (CP d)), NEq r)]. bound0 (split conj x)" + using lp by (simp add: Let_def t s) + from evaldjf_bound0[OF th] show ?thesis + by (simp add: msubstneq_def) qed -lemma msubstneq: assumes lp: "islin (Eq (CNP 0 a r))" - shows "Ifm vs (x#bs) (msubstneq c t d s a r) = Ifm vs (((- Itm vs (x#bs) t / Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) /2)#bs) (NEq (CNP 0 a r))" (is "?lhs = ?rhs") -proof- - let ?Nt = "\(x::'a) t. Itm vs (x#bs) t" +lemma msubstneq: + assumes lp: "islin (Eq (CNP 0 a r))" + shows "Ifm vs (x#bs) (msubstneq c t d s a r) = + Ifm vs (((- Itm vs (x#bs) t / Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) /2)#bs) (NEq (CNP 0 a r))" + (is "?lhs = ?rhs") +proof - + let ?Nt = "\x t. Itm vs (x#bs) t" let ?N = "\p. Ipoly vs p" let ?c = "?N c" let ?d = "?N d" @@ -2146,87 +2804,125 @@ let ?s = "?Nt x s" let ?a = "?N a" let ?r = "?Nt x r" - from lp have lin:"isnpoly a" "a \ 0\<^sub>p" "tmbound0 r" "allpolys isnpoly r" by simp_all - note r= tmbound0_I[OF lin(3), of vs _ bs x] - have cd_cs: "?c * ?d \ 0 \ (?c = 0 \ ?d = 0) \ (?c = 0 \ ?d \ 0) \ (?c \ 0 \ ?d = 0)" by auto + from lp have lin:"isnpoly a" "a \ 0\<^sub>p" "tmbound0 r" "allpolys isnpoly r" + by simp_all + note r = tmbound0_I[OF lin(3), of vs _ bs x] + have cd_cs: "?c * ?d \ 0 \ (?c = 0 \ ?d = 0) \ (?c = 0 \ ?d \ 0) \ (?c \ 0 \ ?d = 0)" + by auto moreover - {assume c: "?c = 0" and d: "?d=0" - hence ?thesis by (simp add: r[of 0] msubstneq_def Let_def evaldjf_ex)} + { + assume c: "?c = 0" + and d: "?d=0" + then have ?thesis + by (simp add: r[of 0] msubstneq_def Let_def evaldjf_ex) + } moreover - {assume c: "?c = 0" and d: "?d\0" - from c have th: "(- ?t / ?c + - ?s / ?d)/2 = -?s / (2*?d)" by simp - have "?rhs = Ifm vs (-?s / (2*?d) # bs) (NEq (CNP 0 a r))" by (simp only: th) - also have "\ \ ?a * (-?s / (2*?d)) + ?r \ 0" by (simp add: r[of "- (Itm vs (x # bs) s / (2 * \d\\<^sub>p\<^bsup>vs\<^esup>))"]) + { + assume c: "?c = 0" + and d: "?d\0" + from c have th: "(- ?t / ?c + - ?s / ?d)/2 = -?s / (2 * ?d)" + by simp + have "?rhs = Ifm vs (-?s / (2*?d) # bs) (NEq (CNP 0 a r))" + by (simp only: th) + also have "\ \ ?a * (-?s / (2*?d)) + ?r \ 0" + by (simp add: r[of "- (Itm vs (x # bs) s / (2 * \d\\<^sub>p\<^bsup>vs\<^esup>))"]) also have "\ \ 2*?d * (?a * (-?s / (2*?d)) + ?r) \ 0" using d mult_cancel_left[of "2*?d" "(?a * (-?s / (2*?d)) + ?r)" 0] by simp also have "\ \ (- ?a * ?s) * (2*?d / (2*?d)) + 2*?d*?r\ 0" by (simp add: field_simps distrib_left[of "2*?d"] del: distrib_left) - - also have "\ \ - (?a * ?s) + 2*?d*?r \ 0" using d by simp - finally have ?thesis using c d + also have "\ \ - (?a * ?s) + 2*?d*?r \ 0" + using d by simp + finally have ?thesis + using c d by (simp add: r[of "- (Itm vs (x # bs) s / (2 * \d\\<^sub>p\<^bsup>vs\<^esup>))"] msubstneq_def Let_def evaldjf_ex) } moreover - {assume c: "?c \ 0" and d: "?d=0" - from d have th: "(- ?t / ?c + - ?s / ?d)/2 = -?t / (2*?c)" by simp - have "?rhs = Ifm vs (-?t / (2*?c) # bs) (NEq (CNP 0 a r))" by (simp only: th) - also have "\ \ ?a * (-?t / (2*?c)) + ?r \ 0" by (simp add: r[of "- (?t/ (2 * ?c))"]) + { + assume c: "?c \ 0" + and d: "?d=0" + from d have th: "(- ?t / ?c + - ?s / ?d)/2 = -?t / (2*?c)" + by simp + have "?rhs = Ifm vs (-?t / (2*?c) # bs) (NEq (CNP 0 a r))" + by (simp only: th) + also have "\ \ ?a * (-?t / (2*?c)) + ?r \ 0" + by (simp add: r[of "- (?t/ (2 * ?c))"]) also have "\ \ 2*?c * (?a * (-?t / (2*?c)) + ?r) \ 0" using c mult_cancel_left[of "2*?c" "(?a * (-?t / (2*?c)) + ?r)" 0] by simp also have "\ \ (?a * -?t)* (2*?c) / (2*?c) + 2*?c*?r \ 0" by (simp add: field_simps distrib_left[of "2*?c"] del: distrib_left) - also have "\ \ - (?a * ?t) + 2*?c*?r \ 0" using c by simp - finally have ?thesis using c d - by (simp add: r[of "- (?t/ (2*?c))"] msubstneq_def Let_def evaldjf_ex) + also have "\ \ - (?a * ?t) + 2*?c*?r \ 0" + using c by simp + finally have ?thesis + using c d by (simp add: r[of "- (?t/ (2*?c))"] msubstneq_def Let_def evaldjf_ex) } moreover - {assume c: "?c \ 0" and d: "?d\0" hence dc: "?c * ?d *2 \ 0" by simp + { + assume c: "?c \ 0" + and d: "?d \ 0" + then have dc: "?c * ?d *2 \ 0" + by simp from add_frac_eq[OF c d, of "- ?t" "- ?s"] - have th: "(- ?t / ?c + - ?s / ?d)/2 = - (?d * ?t + ?c* ?s )/ (2*?c*?d)" + have th: "(- ?t / ?c + - ?s / ?d)/2 = - (?d * ?t + ?c * ?s )/ (2 * ?c * ?d)" by (simp add: field_simps) - have "?rhs \ Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (NEq (CNP 0 a r))" by (simp only: th) + have "?rhs \ Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (NEq (CNP 0 a r))" + by (simp only: th) also have "\ \ ?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r \ 0" by (simp add: r [of "(- (?d * ?t) - (?c *?s)) / (2 * ?c * ?d)"]) - also have "\ \ (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) \ 0 " - using c d mult_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0] by simp + also have "\ \ (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) \ 0" + using c d mult_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0] + by simp also have "\ \ ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r \ 0" using nonzero_mult_divide_cancel_left[OF dc] c d by (simp add: algebra_simps diff_divide_distrib del: distrib_right) - finally have ?thesis using c d - by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstneq_def Let_def evaldjf_ex field_simps) + finally have ?thesis + using c d + by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] + msubstneq_def Let_def evaldjf_ex field_simps) } ultimately show ?thesis by blast qed definition "msubstlt c t d s a r = evaldjf (split conj) - [(let cd = c *\<^sub>p d in (lt (CP (~\<^sub>p cd)), Lt (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), - (let cd = c *\<^sub>p d in (lt (CP cd), Lt (Sub (Mul a (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), - (conj (lt (CP (~\<^sub>p c))) (Eq (CP d)) , Lt (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), - (conj (lt (CP c)) (Eq (CP d)) , Lt (Sub (Mul a t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), - (conj (lt (CP (~\<^sub>p d))) (Eq (CP c)) , Lt (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), - (conj (lt (CP d)) (Eq (CP c)) , Lt (Sub (Mul a s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), - (conj (Eq (CP c)) (Eq (CP d)) , Lt r)]" - -lemma msubstlt_nb: assumes lp: "islin (Lt (CNP 0 a r))" and t: "tmbound0 t" and s: "tmbound0 s" + [(let cd = c *\<^sub>p d + in (lt (CP (~\<^sub>p cd)), Lt (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), + (let cd = c *\<^sub>p d + in (lt (CP cd), Lt (Sub (Mul a (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), + (conj (lt (CP (~\<^sub>p c))) (Eq (CP d)), Lt (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), + (conj (lt (CP c)) (Eq (CP d)), Lt (Sub (Mul a t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), + (conj (lt (CP (~\<^sub>p d))) (Eq (CP c)), Lt (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), + (conj (lt (CP d)) (Eq (CP c)), Lt (Sub (Mul a s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), + (conj (Eq (CP c)) (Eq (CP d)), Lt r)]" + +lemma msubstlt_nb: + assumes lp: "islin (Lt (CNP 0 a r))" + and t: "tmbound0 t" + and s: "tmbound0 s" shows "bound0 (msubstlt c t d s a r)" -proof- - have th: "\x\ set [(let cd = c *\<^sub>p d in (lt (CP (~\<^sub>p cd)), Lt (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), - (let cd = c *\<^sub>p d in (lt (CP cd), Lt (Sub (Mul a (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), - (conj (lt (CP (~\<^sub>p c))) (Eq (CP d)) , Lt (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), - (conj (lt (CP c)) (Eq (CP d)) , Lt (Sub (Mul a t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), - (conj (lt (CP (~\<^sub>p d))) (Eq (CP c)) , Lt (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), - (conj (lt (CP d)) (Eq (CP c)) , Lt (Sub (Mul a s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), - (conj (Eq (CP c)) (Eq (CP d)) , Lt r)]. bound0 (split conj x)" - using lp by (simp add: Let_def t s lt_nb ) - from evaldjf_bound0[OF th] show ?thesis by (simp add: msubstlt_def) +proof - + have th: "\x\ set + [(let cd = c *\<^sub>p d + in (lt (CP (~\<^sub>p cd)), Lt (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), + (let cd = c *\<^sub>p d + in (lt (CP cd), Lt (Sub (Mul a (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), + (conj (lt (CP (~\<^sub>p c))) (Eq (CP d)), Lt (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), + (conj (lt (CP c)) (Eq (CP d)), Lt (Sub (Mul a t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), + (conj (lt (CP (~\<^sub>p d))) (Eq (CP c)), Lt (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), + (conj (lt (CP d)) (Eq (CP c)), Lt (Sub (Mul a s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), + (conj (Eq (CP c)) (Eq (CP d)), Lt r)]. bound0 (split conj x)" + using lp by (simp add: Let_def t s lt_nb) + from evaldjf_bound0[OF th] show ?thesis + by (simp add: msubstlt_def) qed - -lemma msubstlt: assumes nc: "isnpoly c" and nd: "isnpoly d" and lp: "islin (Lt (CNP 0 a r))" +lemma msubstlt: + assumes nc: "isnpoly c" + and nd: "isnpoly d" + and lp: "islin (Lt (CNP 0 a r))" shows "Ifm vs (x#bs) (msubstlt c t d s a r) \ - Ifm vs (((- Itm vs (x#bs) t / Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) /2)#bs) (Lt (CNP 0 a r))" (is "?lhs = ?rhs") -proof- + Ifm vs (((- Itm vs (x#bs) t / Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) /2)#bs) (Lt (CNP 0 a r))" + (is "?lhs = ?rhs") +proof - let ?Nt = "\x t. Itm vs (x#bs) t" let ?N = "\p. Ipoly vs p" let ?c = "?N c" @@ -2235,143 +2931,210 @@ let ?s = "?Nt x s" let ?a = "?N a" let ?r = "?Nt x r" - from lp have lin:"isnpoly a" "a \ 0\<^sub>p" "tmbound0 r" "allpolys isnpoly r" by simp_all - note r= tmbound0_I[OF lin(3), of vs _ bs x] - have cd_cs: "?c * ?d < 0 \ ?c * ?d > 0 \ (?c = 0 \ ?d = 0) \ (?c = 0 \ ?d < 0) \ (?c = 0 \ ?d > 0) \ (?c < 0 \ ?d = 0) \ (?c > 0 \ ?d = 0)" by auto + from lp have lin:"isnpoly a" "a \ 0\<^sub>p" "tmbound0 r" "allpolys isnpoly r" + by simp_all + note r = tmbound0_I[OF lin(3), of vs _ bs x] + have cd_cs: "?c * ?d < 0 \ ?c * ?d > 0 \ (?c = 0 \ ?d = 0) \ (?c = 0 \ ?d < 0) \ (?c = 0 \ ?d > 0) \ (?c < 0 \ ?d = 0) \ (?c > 0 \ ?d = 0)" + by auto moreover - {assume c: "?c=0" and d: "?d=0" - hence ?thesis using nc nd by (simp add: polyneg_norm lt r[of 0] msubstlt_def Let_def evaldjf_ex)} + { + assume c: "?c=0" and d: "?d=0" + then have ?thesis + using nc nd by (simp add: polyneg_norm lt r[of 0] msubstlt_def Let_def evaldjf_ex) + } moreover - {assume dc: "?c*?d > 0" - from dc have dc': "2*?c *?d > 0" by simp - hence c:"?c \ 0" and d: "?d\ 0" by auto + { + assume dc: "?c*?d > 0" + from dc have dc': "2*?c *?d > 0" + by simp + then have c:"?c \ 0" and d: "?d \ 0" + by auto from dc' have dc'': "\ 2*?c *?d < 0" by simp from add_frac_eq[OF c d, of "- ?t" "- ?s"] - have th: "(- ?t / ?c + - ?s / ?d)/2 = - (?d * ?t + ?c* ?s )/ (2*?c*?d)" + have th: "(- ?t / ?c + - ?s / ?d)/2 = - (?d * ?t + ?c* ?s )/ (2 * ?c * ?d)" by (simp add: field_simps) - have "?rhs \ Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (Lt (CNP 0 a r))" by (simp only: th) + have "?rhs \ Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (Lt (CNP 0 a r))" + by (simp only: th) also have "\ \ ?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r < 0" by (simp add: r[of "(- (?d * ?t) - (?c *?s)) / (2 * ?c * ?d)"]) also have "\ \ (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) < 0" - - using dc' dc'' mult_less_cancel_left_disj[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0] by simp + using dc' dc'' + mult_less_cancel_left_disj[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0] + by simp also have "\ \ ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r < 0" using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d by (simp add: algebra_simps diff_divide_distrib del: distrib_right) finally have ?thesis using dc c d nc nd dc' - by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) + by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] + msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) } moreover - {assume dc: "?c*?d < 0" - + { + assume dc: "?c * ?d < 0" from dc have dc': "2*?c *?d < 0" by (simp add: mult_less_0_iff field_simps) - hence c:"?c \ 0" and d: "?d\ 0" by auto + then have c:"?c \ 0" and d: "?d \ 0" + by auto from add_frac_eq[OF c d, of "- ?t" "- ?s"] - have th: "(- ?t / ?c + - ?s / ?d)/2 = - (?d * ?t + ?c* ?s )/ (2*?c*?d)" + have th: "(- ?t / ?c + - ?s / ?d)/2 = - (?d * ?t + ?c* ?s )/ (2 * ?c * ?d)" by (simp add: field_simps) - have "?rhs \ Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (Lt (CNP 0 a r))" by (simp only: th) - also have "\ \ ?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r < 0" + have "?rhs \ Ifm vs (- (?d * ?t + ?c* ?s )/ (2 * ?c * ?d) # bs) (Lt (CNP 0 a r))" + by (simp only: th) + also have "\ \ ?a * (- (?d * ?t + ?c* ?s )/ (2 * ?c * ?d)) + ?r < 0" by (simp add: r[of "(- (?d * ?t) - (?c *?s)) / (2 * ?c * ?d)"]) - - also have "\ \ (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) > 0" - - using dc' order_less_not_sym[OF dc'] mult_less_cancel_left_disj[of "2 * ?c * ?d" 0 "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r"] by simp - also have "\ \ ?a * ((?d * ?t + ?c* ?s )) - 2*?c*?d*?r < 0" - using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d + also have "\ \ (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c * ?s )/ (2 * ?c * ?d)) + ?r) > 0" + using dc' order_less_not_sym[OF dc'] + mult_less_cancel_left_disj[of "2 * ?c * ?d" 0 "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r"] + by simp + also have "\ \ ?a * ((?d * ?t + ?c* ?s )) - 2 * ?c * ?d * ?r < 0" + using nonzero_mult_divide_cancel_left[of "2 * ?c * ?d"] c d by (simp add: algebra_simps diff_divide_distrib del: distrib_right) - finally have ?thesis using dc c d nc nd - by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) + finally have ?thesis using dc c d nc nd + by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] + msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) } moreover - {assume c: "?c > 0" and d: "?d=0" - from c have c'': "2*?c > 0" by (simp add: zero_less_mult_iff) - from c have c': "2*?c \ 0" by simp - from d have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?t / (2*?c)" by (simp add: field_simps) - have "?rhs \ Ifm vs (- ?t / (2*?c) # bs) (Lt (CNP 0 a r))" by (simp only: th) - also have "\ \ ?a* (- ?t / (2*?c))+ ?r < 0" by (simp add: r[of "- (?t / (2*?c))"]) - also have "\ \ 2*?c * (?a* (- ?t / (2*?c))+ ?r) < 0" - using c mult_less_cancel_left_disj[of "2 * ?c" "?a* (- ?t / (2*?c))+ ?r" 0] c' c'' order_less_not_sym[OF c''] by simp - also have "\ \ - ?a*?t+ 2*?c *?r < 0" + { + assume c: "?c > 0" and d: "?d = 0" + from c have c'': "2*?c > 0" + by (simp add: zero_less_mult_iff) + from c have c': "2 * ?c \ 0" + by simp + from d have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?t / (2 * ?c)" + by (simp add: field_simps) + have "?rhs \ Ifm vs (- ?t / (2 * ?c) # bs) (Lt (CNP 0 a r))" + by (simp only: th) + also have "\ \ ?a * (- ?t / (2 * ?c))+ ?r < 0" + by (simp add: r[of "- (?t / (2 * ?c))"]) + also have "\ \ 2 * ?c * (?a * (- ?t / (2 * ?c))+ ?r) < 0" + using c mult_less_cancel_left_disj[of "2 * ?c" "?a* (- ?t / (2*?c))+ ?r" 0] c' c'' + order_less_not_sym[OF c''] + by simp + also have "\ \ - ?a * ?t + 2 * ?c * ?r < 0" using nonzero_mult_divide_cancel_left[OF c'] c by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right) finally have ?thesis using c d nc nd - by(simp add: r[of "- (?t / (2*?c))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) + by (simp add: r[of "- (?t / (2*?c))"] msubstlt_def Let_def evaldjf_ex field_simps + lt polyneg_norm polymul_norm) } moreover - {assume c: "?c < 0" and d: "?d=0" hence c': "2*?c \ 0" by simp - from c have c'': "2*?c < 0" by (simp add: mult_less_0_iff) - from d have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?t / (2*?c)" by (simp add: field_simps) - have "?rhs \ Ifm vs (- ?t / (2*?c) # bs) (Lt (CNP 0 a r))" by (simp only: th) - also have "\ \ ?a* (- ?t / (2*?c))+ ?r < 0" by (simp add: r[of "- (?t / (2*?c))"]) - also have "\ \ 2*?c * (?a* (- ?t / (2*?c))+ ?r) > 0" - using c order_less_not_sym[OF c''] less_imp_neq[OF c''] c'' mult_less_cancel_left_disj[of "2 * ?c" 0 "?a* (- ?t / (2*?c))+ ?r"] by simp + { + assume c: "?c < 0" and d: "?d = 0" + then have c': "2 * ?c \ 0" + by simp + from c have c'': "2 * ?c < 0" + by (simp add: mult_less_0_iff) + from d have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?t / (2 * ?c)" + by (simp add: field_simps) + have "?rhs \ Ifm vs (- ?t / (2*?c) # bs) (Lt (CNP 0 a r))" + by (simp only: th) + also have "\ \ ?a * (- ?t / (2*?c))+ ?r < 0" + by (simp add: r[of "- (?t / (2*?c))"]) + also have "\ \ 2 * ?c * (?a * (- ?t / (2 * ?c))+ ?r) > 0" + using c order_less_not_sym[OF c''] less_imp_neq[OF c''] c'' + mult_less_cancel_left_disj[of "2 * ?c" 0 "?a* (- ?t / (2*?c))+ ?r"] + by simp also have "\ \ ?a*?t - 2*?c *?r < 0" - using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c''] less_imp_neq[OF c''] c'' - by (simp add: algebra_simps diff_divide_distrib del: distrib_right) + using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c''] + less_imp_neq[OF c''] c'' + by (simp add: algebra_simps diff_divide_distrib del: distrib_right) finally have ?thesis using c d nc nd - by(simp add: r[of "- (?t / (2*?c))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) + by (simp add: r[of "- (?t / (2*?c))"] msubstlt_def Let_def evaldjf_ex field_simps + lt polyneg_norm polymul_norm) } moreover - {assume c: "?c = 0" and d: "?d>0" - from d have d'': "2*?d > 0" by (simp add: zero_less_mult_iff) - from d have d': "2*?d \ 0" by simp - from c have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?s / (2*?d)" by (simp add: field_simps) - have "?rhs \ Ifm vs (- ?s / (2*?d) # bs) (Lt (CNP 0 a r))" by (simp only: th) - also have "\ \ ?a* (- ?s / (2*?d))+ ?r < 0" by (simp add: r[of "- (?s / (2*?d))"]) - also have "\ \ 2*?d * (?a* (- ?s / (2*?d))+ ?r) < 0" - using d mult_less_cancel_left_disj[of "2 * ?d" "?a* (- ?s / (2*?d))+ ?r" 0] d' d'' order_less_not_sym[OF d''] by simp - also have "\ \ - ?a*?s+ 2*?d *?r < 0" + { + assume c: "?c = 0" and d: "?d > 0" + from d have d'': "2 * ?d > 0" + by (simp add: zero_less_mult_iff) + from d have d': "2 * ?d \ 0" + by simp + from c have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?s / (2 * ?d)" + by (simp add: field_simps) + have "?rhs \ Ifm vs (- ?s / (2 * ?d) # bs) (Lt (CNP 0 a r))" + by (simp only: th) + also have "\ \ ?a * (- ?s / (2 * ?d))+ ?r < 0" + by (simp add: r[of "- (?s / (2 * ?d))"]) + also have "\ \ 2 * ?d * (?a * (- ?s / (2 * ?d))+ ?r) < 0" + using d mult_less_cancel_left_disj[of "2 * ?d" "?a * (- ?s / (2 * ?d))+ ?r" 0] d' d'' + order_less_not_sym[OF d''] + by simp + also have "\ \ - ?a * ?s+ 2 * ?d * ?r < 0" using nonzero_mult_divide_cancel_left[OF d'] d by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right) finally have ?thesis using c d nc nd - by(simp add: r[of "- (?s / (2*?d))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) + by (simp add: r[of "- (?s / (2*?d))"] msubstlt_def Let_def evaldjf_ex field_simps + lt polyneg_norm polymul_norm) } moreover - {assume c: "?c = 0" and d: "?d<0" hence d': "2*?d \ 0" by simp - from d have d'': "2*?d < 0" by (simp add: mult_less_0_iff) - from c have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?s / (2*?d)" by (simp add: field_simps) - have "?rhs \ Ifm vs (- ?s / (2*?d) # bs) (Lt (CNP 0 a r))" by (simp only: th) - also have "\ \ ?a* (- ?s / (2*?d))+ ?r < 0" by (simp add: r[of "- (?s / (2*?d))"]) - also have "\ \ 2*?d * (?a* (- ?s / (2*?d))+ ?r) > 0" - using d order_less_not_sym[OF d''] less_imp_neq[OF d''] d'' mult_less_cancel_left_disj[of "2 * ?d" 0 "?a* (- ?s / (2*?d))+ ?r"] by simp - also have "\ \ ?a*?s - 2*?d *?r < 0" - using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d''] less_imp_neq[OF d''] d'' - by (simp add: algebra_simps diff_divide_distrib del: distrib_right) + { + assume c: "?c = 0" and d: "?d < 0" + then have d': "2 * ?d \ 0" + by simp + from d have d'': "2 * ?d < 0" + by (simp add: mult_less_0_iff) + from c have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?s / (2*?d)" + by (simp add: field_simps) + have "?rhs \ Ifm vs (- ?s / (2 * ?d) # bs) (Lt (CNP 0 a r))" + by (simp only: th) + also have "\ \ ?a * (- ?s / (2 * ?d)) + ?r < 0" + by (simp add: r[of "- (?s / (2 * ?d))"]) + also have "\ \ 2 * ?d * (?a * (- ?s / (2 * ?d)) + ?r) > 0" + using d order_less_not_sym[OF d''] less_imp_neq[OF d''] d'' + mult_less_cancel_left_disj[of "2 * ?d" 0 "?a* (- ?s / (2*?d))+ ?r"] + by simp + also have "\ \ ?a * ?s - 2 * ?d * ?r < 0" + using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d''] + less_imp_neq[OF d''] d'' + by (simp add: algebra_simps diff_divide_distrib del: distrib_right) finally have ?thesis using c d nc nd - by(simp add: r[of "- (?s / (2*?d))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) + by (simp add: r[of "- (?s / (2*?d))"] msubstlt_def Let_def evaldjf_ex field_simps + lt polyneg_norm polymul_norm) } -ultimately show ?thesis by blast + ultimately show ?thesis by blast qed definition "msubstle c t d s a r = evaldjf (split conj) - [(let cd = c *\<^sub>p d in (lt (CP (~\<^sub>p cd)), Le (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), - (let cd = c *\<^sub>p d in (lt (CP cd), Le (Sub (Mul a (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), - (conj (lt (CP (~\<^sub>p c))) (Eq (CP d)) , Le (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), - (conj (lt (CP c)) (Eq (CP d)) , Le (Sub (Mul a t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), - (conj (lt (CP (~\<^sub>p d))) (Eq (CP c)) , Le (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), - (conj (lt (CP d)) (Eq (CP c)) , Le (Sub (Mul a s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), - (conj (Eq (CP c)) (Eq (CP d)) , Le r)]" - -lemma msubstle_nb: assumes lp: "islin (Le (CNP 0 a r))" and t: "tmbound0 t" and s: "tmbound0 s" + [(let cd = c *\<^sub>p d + in (lt (CP (~\<^sub>p cd)), Le (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), + (let cd = c *\<^sub>p d + in (lt (CP cd), Le (Sub (Mul a (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), + (conj (lt (CP (~\<^sub>p c))) (Eq (CP d)), Le (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), + (conj (lt (CP c)) (Eq (CP d)), Le (Sub (Mul a t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), + (conj (lt (CP (~\<^sub>p d))) (Eq (CP c)), Le (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), + (conj (lt (CP d)) (Eq (CP c)), Le (Sub (Mul a s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), + (conj (Eq (CP c)) (Eq (CP d)), Le r)]" + +lemma msubstle_nb: + assumes lp: "islin (Le (CNP 0 a r))" + and t: "tmbound0 t" + and s: "tmbound0 s" shows "bound0 (msubstle c t d s a r)" -proof- - have th: "\x\ set [(let cd = c *\<^sub>p d in (lt (CP (~\<^sub>p cd)), Le (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), - (let cd = c *\<^sub>p d in (lt (CP cd), Le (Sub (Mul a (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), - (conj (lt (CP (~\<^sub>p c))) (Eq (CP d)) , Le (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), - (conj (lt (CP c)) (Eq (CP d)) , Le (Sub (Mul a t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), - (conj (lt (CP (~\<^sub>p d))) (Eq (CP c)) , Le (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), - (conj (lt (CP d)) (Eq (CP c)) , Le (Sub (Mul a s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), - (conj (Eq (CP c)) (Eq (CP d)) , Le r)]. bound0 (split conj x)" - using lp by (simp add: Let_def t s lt_nb ) - from evaldjf_bound0[OF th] show ?thesis by (simp add: msubstle_def) +proof - + have th: "\x\ set + [(let cd = c *\<^sub>p d + in (lt (CP (~\<^sub>p cd)), Le (Add (Mul (~\<^sub>p a) (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), + (let cd = c *\<^sub>p d + in (lt (CP cd), Le (Sub (Mul a (Add (Mul d t) (Mul c s))) (Mul ((2)\<^sub>p *\<^sub>p cd) r)))), + (conj (lt (CP (~\<^sub>p c))) (Eq (CP d)) , Le (Add (Mul (~\<^sub>p a) t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), + (conj (lt (CP c)) (Eq (CP d)) , Le (Sub (Mul a t) (Mul ((2)\<^sub>p *\<^sub>p c) r))), + (conj (lt (CP (~\<^sub>p d))) (Eq (CP c)) , Le (Add (Mul (~\<^sub>p a) s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), + (conj (lt (CP d)) (Eq (CP c)) , Le (Sub (Mul a s) (Mul ((2)\<^sub>p *\<^sub>p d) r))), + (conj (Eq (CP c)) (Eq (CP d)) , Le r)]. bound0 (split conj x)" + using lp by (simp add: Let_def t s lt_nb) + from evaldjf_bound0[OF th] show ?thesis + by (simp add: msubstle_def) qed -lemma msubstle: assumes nc: "isnpoly c" and nd: "isnpoly d" and lp: "islin (Le (CNP 0 a r))" +lemma msubstle: + assumes nc: "isnpoly c" + and nd: "isnpoly d" + and lp: "islin (Le (CNP 0 a r))" shows "Ifm vs (x#bs) (msubstle c t d s a r) \ - Ifm vs (((- Itm vs (x#bs) t / Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) /2)#bs) (Le (CNP 0 a r))" (is "?lhs = ?rhs") -proof- + Ifm vs (((- Itm vs (x#bs) t / Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) /2)#bs) (Le (CNP 0 a r))" + (is "?lhs = ?rhs") +proof - let ?Nt = "\x t. Itm vs (x#bs) t" let ?N = "\p. Ipoly vs p" let ?c = "?N c" @@ -2380,269 +3143,424 @@ let ?s = "?Nt x s" let ?a = "?N a" let ?r = "?Nt x r" - from lp have lin:"isnpoly a" "a \ 0\<^sub>p" "tmbound0 r" "allpolys isnpoly r" by simp_all - note r= tmbound0_I[OF lin(3), of vs _ bs x] - have cd_cs: "?c * ?d < 0 \ ?c * ?d > 0 \ (?c = 0 \ ?d = 0) \ (?c = 0 \ ?d < 0) \ (?c = 0 \ ?d > 0) \ (?c < 0 \ ?d = 0) \ (?c > 0 \ ?d = 0)" by auto + from lp have lin:"isnpoly a" "a \ 0\<^sub>p" "tmbound0 r" "allpolys isnpoly r" + by simp_all + note r = tmbound0_I[OF lin(3), of vs _ bs x] + have cd_cs: "?c * ?d < 0 \ ?c * ?d > 0 \ (?c = 0 \ ?d = 0) \ (?c = 0 \ ?d < 0) \ (?c = 0 \ ?d > 0) \ (?c < 0 \ ?d = 0) \ (?c > 0 \ ?d = 0)" + by auto moreover - {assume c: "?c=0" and d: "?d=0" - hence ?thesis using nc nd by (simp add: polyneg_norm polymul_norm lt r[of 0] msubstle_def Let_def evaldjf_ex)} + { + assume c: "?c = 0" and d: "?d = 0" + then have ?thesis + using nc nd + by (simp add: polyneg_norm polymul_norm lt r[of 0] msubstle_def Let_def evaldjf_ex) + } moreover - {assume dc: "?c*?d > 0" - from dc have dc': "2*?c *?d > 0" by simp - hence c:"?c \ 0" and d: "?d\ 0" by auto - from dc' have dc'': "\ 2*?c *?d < 0" by simp + { + assume dc: "?c * ?d > 0" + from dc have dc': "2 * ?c * ?d > 0" + by simp + then have c: "?c \ 0" and d: "?d \ 0" + by auto + from dc' have dc'': "\ 2 * ?c * ?d < 0" + by simp from add_frac_eq[OF c d, of "- ?t" "- ?s"] - have th: "(- ?t / ?c + - ?s / ?d)/2 = - (?d * ?t + ?c* ?s )/ (2*?c*?d)" + have th: "(- ?t / ?c + - ?s / ?d)/2 = - (?d * ?t + ?c * ?s )/ (2 * ?c * ?d)" by (simp add: field_simps) - have "?rhs \ Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (Le (CNP 0 a r))" by (simp only: th) - also have "\ \ ?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r <= 0" + have "?rhs \ Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (Le (CNP 0 a r))" + by (simp only: th) + also have "\ \ ?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r \ 0" by (simp add: r[of "(- (?d * ?t) - (?c *?s)) / (2 * ?c * ?d)"]) - also have "\ \ (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) <= 0" - - using dc' dc'' mult_le_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0] by simp - also have "\ \ ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r <= 0" + also have "\ \ (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) \ 0" + using dc' dc'' + mult_le_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0] + by simp + also have "\ \ ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r \ 0" using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d by (simp add: algebra_simps diff_divide_distrib del: distrib_right) finally have ?thesis using dc c d nc nd dc' - by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) + by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstle_def + Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) } moreover - {assume dc: "?c*?d < 0" - - from dc have dc': "2*?c *?d < 0" + { + assume dc: "?c * ?d < 0" + from dc have dc': "2 * ?c * ?d < 0" by (simp add: mult_less_0_iff field_simps add_neg_neg add_pos_pos) - hence c:"?c \ 0" and d: "?d\ 0" by auto + then have c: "?c \ 0" and d: "?d \ 0" + by auto from add_frac_eq[OF c d, of "- ?t" "- ?s"] - have th: "(- ?t / ?c + - ?s / ?d)/2 = - (?d * ?t + ?c* ?s )/ (2*?c*?d)" + have th: "(- ?t / ?c + - ?s / ?d)/2 = - (?d * ?t + ?c* ?s )/ (2 * ?c * ?d)" by (simp add: field_simps) - have "?rhs \ Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (Le (CNP 0 a r))" by (simp only: th) - also have "\ \ ?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r <= 0" + have "?rhs \ Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (Le (CNP 0 a r))" + by (simp only: th) + also have "\ \ ?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r \ 0" by (simp add: r[of "(- (?d * ?t) - (?c *?s)) / (2 * ?c * ?d)"]) - - also have "\ \ (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) >= 0" - - using dc' order_less_not_sym[OF dc'] mult_le_cancel_left[of "2 * ?c * ?d" 0 "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r"] by simp - also have "\ \ ?a * ((?d * ?t + ?c* ?s )) - 2*?c*?d*?r <= 0" - using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d + also have "\ \ (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) \ 0" + using dc' order_less_not_sym[OF dc'] + mult_le_cancel_left[of "2 * ?c * ?d" 0 "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r"] + by simp + also have "\ \ ?a * ((?d * ?t + ?c* ?s )) - 2 * ?c * ?d * ?r \ 0" + using nonzero_mult_divide_cancel_left[of "2 * ?c * ?d"] c d by (simp add: algebra_simps diff_divide_distrib del: distrib_right) finally have ?thesis using dc c d nc nd - by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) + by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstle_def + Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) } moreover - {assume c: "?c > 0" and d: "?d=0" - from c have c'': "2*?c > 0" by (simp add: zero_less_mult_iff) - from c have c': "2*?c \ 0" by simp - from d have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?t / (2*?c)" by (simp add: field_simps) - have "?rhs \ Ifm vs (- ?t / (2*?c) # bs) (Le (CNP 0 a r))" by (simp only: th) - also have "\ \ ?a* (- ?t / (2*?c))+ ?r <= 0" by (simp add: r[of "- (?t / (2*?c))"]) - also have "\ \ 2*?c * (?a* (- ?t / (2*?c))+ ?r) <= 0" - using c mult_le_cancel_left[of "2 * ?c" "?a* (- ?t / (2*?c))+ ?r" 0] c' c'' order_less_not_sym[OF c''] by simp - also have "\ \ - ?a*?t+ 2*?c *?r <= 0" + { + assume c: "?c > 0" and d: "?d = 0" + from c have c'': "2 * ?c > 0" + by (simp add: zero_less_mult_iff) + from c have c': "2 * ?c \ 0" + by simp + from d have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?t / (2*?c)" + by (simp add: field_simps) + have "?rhs \ Ifm vs (- ?t / (2 * ?c) # bs) (Le (CNP 0 a r))" + by (simp only: th) + also have "\ \ ?a * (- ?t / (2 * ?c))+ ?r \ 0" + by (simp add: r[of "- (?t / (2 * ?c))"]) + also have "\ \ 2 * ?c * (?a * (- ?t / (2 * ?c))+ ?r) \ 0" + using c mult_le_cancel_left[of "2 * ?c" "?a* (- ?t / (2*?c))+ ?r" 0] c' c'' + order_less_not_sym[OF c''] + by simp + also have "\ \ - ?a*?t+ 2*?c *?r \ 0" using nonzero_mult_divide_cancel_left[OF c'] c by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right) finally have ?thesis using c d nc nd - by(simp add: r[of "- (?t / (2*?c))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) + by (simp add: r[of "- (?t / (2*?c))"] msubstle_def Let_def + evaldjf_ex field_simps lt polyneg_norm polymul_norm) } moreover - {assume c: "?c < 0" and d: "?d=0" hence c': "2*?c \ 0" by simp - from c have c'': "2*?c < 0" by (simp add: mult_less_0_iff) - from d have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?t / (2*?c)" by (simp add: field_simps) - have "?rhs \ Ifm vs (- ?t / (2*?c) # bs) (Le (CNP 0 a r))" by (simp only: th) - also have "\ \ ?a* (- ?t / (2*?c))+ ?r <= 0" by (simp add: r[of "- (?t / (2*?c))"]) - also have "\ \ 2*?c * (?a* (- ?t / (2*?c))+ ?r) >= 0" - using c order_less_not_sym[OF c''] less_imp_neq[OF c''] c'' mult_le_cancel_left[of "2 * ?c" 0 "?a* (- ?t / (2*?c))+ ?r"] by simp - also have "\ \ ?a*?t - 2*?c *?r <= 0" - using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c''] less_imp_neq[OF c''] c'' - by (simp add: algebra_simps diff_divide_distrib del: distrib_right) + { + assume c: "?c < 0" and d: "?d = 0" + then have c': "2 * ?c \ 0" + by simp + from c have c'': "2 * ?c < 0" + by (simp add: mult_less_0_iff) + from d have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?t / (2*?c)" + by (simp add: field_simps) + have "?rhs \ Ifm vs (- ?t / (2 * ?c) # bs) (Le (CNP 0 a r))" + by (simp only: th) + also have "\ \ ?a * (- ?t / (2*?c))+ ?r \ 0" + by (simp add: r[of "- (?t / (2*?c))"]) + also have "\ \ 2 * ?c * (?a * (- ?t / (2 * ?c))+ ?r) \ 0" + using c order_less_not_sym[OF c''] less_imp_neq[OF c''] c'' + mult_le_cancel_left[of "2 * ?c" 0 "?a* (- ?t / (2*?c))+ ?r"] + by simp + also have "\ \ ?a * ?t - 2 * ?c * ?r \ 0" + using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c''] + less_imp_neq[OF c''] c'' + by (simp add: algebra_simps diff_divide_distrib del: distrib_right) finally have ?thesis using c d nc nd - by(simp add: r[of "- (?t / (2*?c))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) + by (simp add: r[of "- (?t / (2*?c))"] msubstle_def Let_def + evaldjf_ex field_simps lt polyneg_norm polymul_norm) } moreover - {assume c: "?c = 0" and d: "?d>0" - from d have d'': "2*?d > 0" by (simp add: zero_less_mult_iff) - from d have d': "2*?d \ 0" by simp - from c have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?s / (2*?d)" by (simp add: field_simps) - have "?rhs \ Ifm vs (- ?s / (2*?d) # bs) (Le (CNP 0 a r))" by (simp only: th) - also have "\ \ ?a* (- ?s / (2*?d))+ ?r <= 0" by (simp add: r[of "- (?s / (2*?d))"]) - also have "\ \ 2*?d * (?a* (- ?s / (2*?d))+ ?r) <= 0" - using d mult_le_cancel_left[of "2 * ?d" "?a* (- ?s / (2*?d))+ ?r" 0] d' d'' order_less_not_sym[OF d''] by simp - also have "\ \ - ?a*?s+ 2*?d *?r <= 0" + { + assume c: "?c = 0" and d: "?d > 0" + from d have d'': "2 * ?d > 0" + by (simp add: zero_less_mult_iff) + from d have d': "2 * ?d \ 0" + by simp + from c have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?s / (2 * ?d)" + by (simp add: field_simps) + have "?rhs \ Ifm vs (- ?s / (2 * ?d) # bs) (Le (CNP 0 a r))" + by (simp only: th) + also have "\ \ ?a * (- ?s / (2 * ?d))+ ?r \ 0" + by (simp add: r[of "- (?s / (2*?d))"]) + also have "\ \ 2 * ?d * (?a * (- ?s / (2 * ?d)) + ?r) \ 0" + using d mult_le_cancel_left[of "2 * ?d" "?a* (- ?s / (2*?d))+ ?r" 0] d' d'' + order_less_not_sym[OF d''] + by simp + also have "\ \ - ?a * ?s + 2 * ?d * ?r \ 0" using nonzero_mult_divide_cancel_left[OF d'] d by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right) finally have ?thesis using c d nc nd - by(simp add: r[of "- (?s / (2*?d))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) + by (simp add: r[of "- (?s / (2*?d))"] msubstle_def Let_def + evaldjf_ex field_simps lt polyneg_norm polymul_norm) } moreover - {assume c: "?c = 0" and d: "?d<0" hence d': "2*?d \ 0" by simp - from d have d'': "2*?d < 0" by (simp add: mult_less_0_iff) - from c have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?s / (2*?d)" by (simp add: field_simps) - have "?rhs \ Ifm vs (- ?s / (2*?d) # bs) (Le (CNP 0 a r))" by (simp only: th) - also have "\ \ ?a* (- ?s / (2*?d))+ ?r <= 0" by (simp add: r[of "- (?s / (2*?d))"]) - also have "\ \ 2*?d * (?a* (- ?s / (2*?d))+ ?r) >= 0" - using d order_less_not_sym[OF d''] less_imp_neq[OF d''] d'' mult_le_cancel_left[of "2 * ?d" 0 "?a* (- ?s / (2*?d))+ ?r"] by simp - also have "\ \ ?a*?s - 2*?d *?r <= 0" - using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d''] less_imp_neq[OF d''] d'' - by (simp add: algebra_simps diff_divide_distrib del: distrib_right) + { + assume c: "?c = 0" and d: "?d < 0" + then have d': "2 * ?d \ 0" + by simp + from d have d'': "2 * ?d < 0" + by (simp add: mult_less_0_iff) + from c have th: "(- ?t / ?c + - ?s / ?d)/2 = - ?s / (2*?d)" + by (simp add: field_simps) + have "?rhs \ Ifm vs (- ?s / (2*?d) # bs) (Le (CNP 0 a r))" + by (simp only: th) + also have "\ \ ?a* (- ?s / (2*?d))+ ?r \ 0" + by (simp add: r[of "- (?s / (2*?d))"]) + also have "\ \ 2*?d * (?a* (- ?s / (2*?d))+ ?r) \ 0" + using d order_less_not_sym[OF d''] less_imp_neq[OF d''] d'' + mult_le_cancel_left[of "2 * ?d" 0 "?a* (- ?s / (2*?d))+ ?r"] + by simp + also have "\ \ ?a * ?s - 2 * ?d * ?r \ 0" + using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d''] + less_imp_neq[OF d''] d'' + by (simp add: algebra_simps diff_divide_distrib del: distrib_right) finally have ?thesis using c d nc nd - by(simp add: r[of "- (?s / (2*?d))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) + by (simp add: r[of "- (?s / (2*?d))"] msubstle_def Let_def + evaldjf_ex field_simps lt polyneg_norm polymul_norm) } -ultimately show ?thesis by blast + ultimately show ?thesis by blast qed - -fun msubst :: "fm \ (poly \ tm) \ (poly \ tm) \ fm" where - "msubst (And p q) ((c,t), (d,s)) = conj (msubst p ((c,t),(d,s))) (msubst q ((c,t),(d,s)))" -| "msubst (Or p q) ((c,t), (d,s)) = disj (msubst p ((c,t),(d,s))) (msubst q ((c,t), (d,s)))" -| "msubst (Eq (CNP 0 a r)) ((c,t),(d,s)) = msubsteq c t d s a r" -| "msubst (NEq (CNP 0 a r)) ((c,t),(d,s)) = msubstneq c t d s a r" -| "msubst (Lt (CNP 0 a r)) ((c,t),(d,s)) = msubstlt c t d s a r" -| "msubst (Le (CNP 0 a r)) ((c,t),(d,s)) = msubstle c t d s a r" -| "msubst p ((c,t),(d,s)) = p" - -lemma msubst_I: assumes lp: "islin p" and nc: "isnpoly c" and nd: "isnpoly d" - shows "Ifm vs (x#bs) (msubst p ((c,t),(d,s))) = Ifm vs (((- Itm vs (x#bs) t / Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) /2)#bs) p" - using lp by (induct p rule: islin.induct) +fun msubst :: "fm \ (poly \ tm) \ (poly \ tm) \ fm" +where + "msubst (And p q) ((c, t), (d, s)) = conj (msubst p ((c,t),(d,s))) (msubst q ((c, t), (d, s)))" +| "msubst (Or p q) ((c, t), (d, s)) = disj (msubst p ((c,t),(d,s))) (msubst q ((c, t), (d, s)))" +| "msubst (Eq (CNP 0 a r)) ((c, t), (d, s)) = msubsteq c t d s a r" +| "msubst (NEq (CNP 0 a r)) ((c, t), (d, s)) = msubstneq c t d s a r" +| "msubst (Lt (CNP 0 a r)) ((c, t), (d, s)) = msubstlt c t d s a r" +| "msubst (Le (CNP 0 a r)) ((c, t), (d, s)) = msubstle c t d s a r" +| "msubst p ((c, t), (d, s)) = p" + +lemma msubst_I: + assumes lp: "islin p" + and nc: "isnpoly c" + and nd: "isnpoly d" + shows "Ifm vs (x#bs) (msubst p ((c,t),(d,s))) = + Ifm vs (((- Itm vs (x#bs) t / Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) /2)#bs) p" + using lp + by (induct p rule: islin.induct) (auto simp add: tmbound0_I - [where b = "(- (Itm vs (x # bs) t / \c\\<^sub>p\<^bsup>vs\<^esup>) - (Itm vs (x # bs) s / \d\\<^sub>p\<^bsup>vs\<^esup>)) / 2" - and b' = x and bs = bs and vs = vs] - msubsteq msubstneq msubstlt [OF nc nd] msubstle [OF nc nd]) - -lemma msubst_nb: assumes lp: "islin p" and t: "tmbound0 t" and s: "tmbound0 s" + [where b = "(- (Itm vs (x # bs) t / \c\\<^sub>p\<^bsup>vs\<^esup>) - (Itm vs (x # bs) s / \d\\<^sub>p\<^bsup>vs\<^esup>)) / 2" + and b' = x and bs = bs and vs = vs] + msubsteq msubstneq msubstlt [OF nc nd] msubstle [OF nc nd]) + +lemma msubst_nb: + assumes lp: "islin p" + and t: "tmbound0 t" + and s: "tmbound0 s" shows "bound0 (msubst p ((c,t),(d,s)))" using lp t s by (induct p rule: islin.induct, auto simp add: msubsteq_nb msubstneq_nb msubstlt_nb msubstle_nb) lemma fr_eq_msubst: assumes lp: "islin p" - shows "(\x. Ifm vs (x#bs) p) = ((Ifm vs (x#bs) (minusinf p)) \ (Ifm vs (x#bs) (plusinf p)) \ (\(c,t) \ set (uset p). \(d,s) \ set (uset p). Ifm vs (x#bs) (msubst p ((c,t),(d,s)))))" + shows "(\x. Ifm vs (x#bs) p) \ + (Ifm vs (x#bs) (minusinf p) \ + Ifm vs (x#bs) (plusinf p) \ + (\(c, t) \ set (uset p). \(d, s) \ set (uset p). + Ifm vs (x#bs) (msubst p ((c, t), (d, s)))))" (is "(\x. ?I x p) = (?M \ ?P \ ?F)" is "?E = ?D") -proof- -from uset_l[OF lp] have th: "\(c, s)\set (uset p). isnpoly c \ tmbound0 s" by blast -{fix c t d s assume ctU: "(c,t) \set (uset p)" and dsU: "(d,s) \set (uset p)" - and pts: "Ifm vs ((- Itm vs (x # bs) t / \c\\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \d\\<^sub>p\<^bsup>vs\<^esup>) / 2 # bs) p" - from th[rule_format, OF ctU] th[rule_format, OF dsU] have norm:"isnpoly c" "isnpoly d" by simp_all - from msubst_I[OF lp norm, of vs x bs t s] pts - have "Ifm vs (x # bs) (msubst p ((c, t), d, s))" ..} -moreover -{fix c t d s assume ctU: "(c,t) \set (uset p)" and dsU: "(d,s) \set (uset p)" - and pts: "Ifm vs (x # bs) (msubst p ((c, t), d, s))" - from th[rule_format, OF ctU] th[rule_format, OF dsU] have norm:"isnpoly c" "isnpoly d" by simp_all - from msubst_I[OF lp norm, of vs x bs t s] pts - have "Ifm vs ((- Itm vs (x # bs) t / \c\\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \d\\<^sub>p\<^bsup>vs\<^esup>) / 2 # bs) p" ..} -ultimately have th': "(\(c,t) \ set (uset p). \(d,s) \ set (uset p). Ifm vs ((- Itm vs (x # bs) t / \c\\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \d\\<^sub>p\<^bsup>vs\<^esup>) / 2 # bs) p) \ ?F" by blast -from fr_eq[OF lp, of vs bs x, simplified th'] show ?thesis . +proof - + from uset_l[OF lp] + have th: "\(c, s)\set (uset p). isnpoly c \ tmbound0 s" + by blast + { + fix c t d s + assume ctU: "(c, t) \set (uset p)" + and dsU: "(d,s) \set (uset p)" + and pts: "Ifm vs ((- Itm vs (x # bs) t / \c\\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \d\\<^sub>p\<^bsup>vs\<^esup>) / 2 # bs) p" + from th[rule_format, OF ctU] th[rule_format, OF dsU] have norm:"isnpoly c" "isnpoly d" + by simp_all + from msubst_I[OF lp norm, of vs x bs t s] pts + have "Ifm vs (x # bs) (msubst p ((c, t), d, s))" .. + } + moreover + { + fix c t d s + assume ctU: "(c, t) \ set (uset p)" + and dsU: "(d,s) \set (uset p)" + and pts: "Ifm vs (x # bs) (msubst p ((c, t), d, s))" + from th[rule_format, OF ctU] th[rule_format, OF dsU] have norm:"isnpoly c" "isnpoly d" + by simp_all + from msubst_I[OF lp norm, of vs x bs t s] pts + have "Ifm vs ((- Itm vs (x # bs) t / \c\\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \d\\<^sub>p\<^bsup>vs\<^esup>) / 2 # bs) p" .. + } + ultimately have th': "(\(c, t) \ set (uset p). \(d, s) \ set (uset p). + Ifm vs ((- Itm vs (x # bs) t / \c\\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \d\\<^sub>p\<^bsup>vs\<^esup>) / 2 # bs) p) \ ?F" + by blast + from fr_eq[OF lp, of vs bs x, simplified th'] show ?thesis . qed -lemma simpfm_lin: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" +lemma simpfm_lin: + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "qfree p \ islin (simpfm p)" - by (induct p rule: simpfm.induct, auto simp add: conj_lin disj_lin) - -definition - "ferrack p \ let q = simpfm p ; mp = minusinf q ; pp = plusinf q - in if (mp = T \ pp = T) then T - else (let U = alluopairs (remdups (uset q)) - in decr0 (disj mp (disj pp (evaldjf (simpfm o (msubst q)) U ))))" + by (induct p rule: simpfm.induct) (auto simp add: conj_lin disj_lin) + +definition "ferrack p \ + let + q = simpfm p; + mp = minusinf q; + pp = plusinf q + in + if (mp = T \ pp = T) then T + else + (let U = alluopairs (remdups (uset q)) + in decr0 (disj mp (disj pp (evaldjf (simpfm o (msubst q)) U ))))" lemma ferrack: assumes qf: "qfree p" - shows "qfree (ferrack p) \ ((Ifm vs bs (ferrack p)) = (Ifm vs bs (E p)))" - (is "_ \ (?rhs = ?lhs)") -proof- - let ?I = "\ x p. Ifm vs (x#bs) p" - let ?N = "\ t. Ipoly vs t" + shows "qfree (ferrack p) \ Ifm vs bs (ferrack p) = Ifm vs bs (E p)" + (is "_ \ ?rhs = ?lhs") +proof - + let ?I = "\x p. Ifm vs (x#bs) p" + let ?N = "\t. Ipoly vs t" let ?Nt = "\x t. Itm vs (x#bs) t" let ?q = "simpfm p" let ?U = "remdups(uset ?q)" let ?Up = "alluopairs ?U" let ?mp = "minusinf ?q" let ?pp = "plusinf ?q" + fix x let ?I = "\p. Ifm vs (x#bs) p" from simpfm_lin[OF qf] simpfm_qf[OF qf] have lq: "islin ?q" and q_qf: "qfree ?q" . from minusinf_nb[OF lq] plusinf_nb[OF lq] have mp_nb: "bound0 ?mp" and pp_nb: "bound0 ?pp" . from bound0_qf[OF mp_nb] bound0_qf[OF pp_nb] have mp_qf: "qfree ?mp" and pp_qf: "qfree ?pp" . from uset_l[OF lq] have U_l: "\(c, s)\set ?U. isnpoly c \ c \ 0\<^sub>p \ tmbound0 s \ allpolys isnpoly s" by simp - {fix c t d s assume ctU: "(c,t) \ set ?U" and dsU: "(d,s) \ set ?U" - from U_l ctU dsU have norm: "isnpoly c" "isnpoly d" by auto + { + fix c t d s + assume ctU: "(c, t) \ set ?U" + and dsU: "(d,s) \ set ?U" + from U_l ctU dsU have norm: "isnpoly c" "isnpoly d" + by auto from msubst_I[OF lq norm, of vs x bs t s] msubst_I[OF lq norm(2,1), of vs x bs s t] - have "?I (msubst ?q ((c,t),(d,s))) = ?I (msubst ?q ((d,s),(c,t)))" by (simp add: field_simps)} - hence th0: "\x \ set ?U. \y \ set ?U. ?I (msubst ?q (x, y)) \ ?I (msubst ?q (y, x))" by clarsimp - {fix x assume xUp: "x \ set ?Up" - then obtain c t d s where ctU: "(c,t) \ set ?U" and dsU: "(d,s) \ set ?U" - and x: "x = ((c,t),(d,s))" using alluopairs_set1[of ?U] by auto + have "?I (msubst ?q ((c,t),(d,s))) = ?I (msubst ?q ((d,s),(c,t)))" + by (simp add: field_simps) + } + then have th0: "\x \ set ?U. \y \ set ?U. ?I (msubst ?q (x, y)) \ ?I (msubst ?q (y, x))" + by auto + { + fix x + assume xUp: "x \ set ?Up" + then obtain c t d s + where ctU: "(c, t) \ set ?U" + and dsU: "(d,s) \ set ?U" + and x: "x = ((c, t),(d, s))" + using alluopairs_set1[of ?U] by auto from U_l[rule_format, OF ctU] U_l[rule_format, OF dsU] have nbs: "tmbound0 t" "tmbound0 s" by simp_all from simpfm_bound0[OF msubst_nb[OF lq nbs, of c d]] - have "bound0 ((simpfm o (msubst (simpfm p))) x)" using x by simp} + have "bound0 ((simpfm o (msubst (simpfm p))) x)" + using x by simp + } with evaldjf_bound0[of ?Up "(simpfm o (msubst (simpfm p)))"] have "bound0 (evaldjf (simpfm o (msubst (simpfm p))) ?Up)" by blast with mp_nb pp_nb - have th1: "bound0 (disj ?mp (disj ?pp (evaldjf (simpfm o (msubst ?q)) ?Up )))" by simp - from decr0_qf[OF th1] have thqf: "qfree (ferrack p)" by (simp add: ferrack_def Let_def) - have "?lhs \ (\x. Ifm vs (x#bs) ?q)" by simp - also have "\ \ ?I ?mp \ ?I ?pp \ (\(c, t)\set ?U. \(d, s)\set ?U. ?I (msubst (simpfm p) ((c, t), d, s)))" using fr_eq_msubst[OF lq, of vs bs x] by simp - also have "\ \ ?I ?mp \ ?I ?pp \ (\(x,y) \ set ?Up. ?I ((simpfm o (msubst ?q)) (x,y)))" using alluopairs_bex[OF th0] by simp - also have "\ \ ?I ?mp \ ?I ?pp \ ?I (evaldjf (simpfm o (msubst ?q)) ?Up)" + have th1: "bound0 (disj ?mp (disj ?pp (evaldjf (simpfm o (msubst ?q)) ?Up )))" + by simp + from decr0_qf[OF th1] have thqf: "qfree (ferrack p)" + by (simp add: ferrack_def Let_def) + have "?lhs \ (\x. Ifm vs (x#bs) ?q)" + by simp + also have "\ \ ?I ?mp \ ?I ?pp \ + (\(c, t)\set ?U. \(d, s)\set ?U. ?I (msubst (simpfm p) ((c, t), d, s)))" + using fr_eq_msubst[OF lq, of vs bs x] by simp + also have "\ \ ?I ?mp \ ?I ?pp \ + (\(x, y) \ set ?Up. ?I ((simpfm \ msubst ?q) (x, y)))" + using alluopairs_bex[OF th0] by simp + also have "\ \ ?I ?mp \ ?I ?pp \ ?I (evaldjf (simpfm \ msubst ?q) ?Up)" by (simp add: evaldjf_ex) - also have "\ \ ?I (disj ?mp (disj ?pp (evaldjf (simpfm o (msubst ?q)) ?Up)))" by simp - also have "\ \ ?rhs" using decr0[OF th1, of vs x bs] + also have "\ \ ?I (disj ?mp (disj ?pp (evaldjf (simpfm \ msubst ?q) ?Up)))" + by simp + also have "\ \ ?rhs" + using decr0[OF th1, of vs x bs] apply (simp add: ferrack_def Let_def) - by (cases "?mp = T \ ?pp = T", auto) - finally show ?thesis using thqf by blast + apply (cases "?mp = T \ ?pp = T") + apply auto + done + finally show ?thesis + using thqf by blast qed definition "frpar p = simpfm (qelim p ferrack)" + lemma frpar: "qfree (frpar p) \ (Ifm vs bs (frpar p) \ Ifm vs bs p)" -proof- - from ferrack have th: "\bs p. qfree p \ qfree (ferrack p) \ Ifm vs bs (ferrack p) = Ifm vs bs (E p)" by blast - from qelim[OF th, of p bs] show ?thesis unfolding frpar_def by auto +proof - + from ferrack + have th: "\bs p. qfree p \ qfree (ferrack p) \ Ifm vs bs (ferrack p) = Ifm vs bs (E p)" + by blast + from qelim[OF th, of p bs] show ?thesis + unfolding frpar_def by auto qed -section{* Second implemenation: Case splits not local *} - -lemma fr_eq2: assumes lp: "islin p" +section {* Second implemenation: Case splits not local *} + +lemma fr_eq2: + assumes lp: "islin p" shows "(\x. Ifm vs (x#bs) p) \ - ((Ifm vs (x#bs) (minusinf p)) \ (Ifm vs (x#bs) (plusinf p)) \ - (Ifm vs (0#bs) p) \ - (\(n,t) \ set (uset p). Ipoly vs n \ 0 \ Ifm vs ((- Itm vs (x#bs) t / (Ipoly vs n * 2))#bs) p) \ - (\(n,t) \ set (uset p). \(m,s) \ set (uset p). Ipoly vs n \ 0 \ Ipoly vs m \ 0 \ Ifm vs (((- Itm vs (x#bs) t / Ipoly vs n + - Itm vs (x#bs) s / Ipoly vs m) /2)#bs) p))" + (Ifm vs (x#bs) (minusinf p) \ + Ifm vs (x#bs) (plusinf p) \ + Ifm vs (0#bs) p \ + (\(n, t) \ set (uset p). + Ipoly vs n \ 0 \ Ifm vs ((- Itm vs (x#bs) t / (Ipoly vs n * 2))#bs) p) \ + (\(n, t) \ set (uset p). \(m, s) \ set (uset p). + Ipoly vs n \ 0 \ + Ipoly vs m \ 0 \ + Ifm vs (((- Itm vs (x#bs) t / Ipoly vs n + - Itm vs (x#bs) s / Ipoly vs m) /2)#bs) p))" (is "(\x. ?I x p) = (?M \ ?P \ ?Z \ ?U \ ?F)" is "?E = ?D") proof assume px: "\x. ?I x p" have "?M \ ?P \ (\ ?M \ \ ?P)" by blast - moreover {assume "?M \ ?P" hence "?D" by blast} - moreover {assume nmi: "\ ?M" and npi: "\ ?P" + moreover { + assume "?M \ ?P" + then have "?D" by blast + } + moreover { + assume nmi: "\ ?M" + and npi: "\ ?P" from inf_uset[OF lp nmi npi, OF px] - obtain c t d s where ct: "(c,t) \ set (uset p)" "(d,s) \ set (uset p)" "?I ((- Itm vs (x # bs) t / \c\\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \d\\<^sub>p\<^bsup>vs\<^esup>) / ((1\'a) + (1\'a))) p" + obtain c t d s where ct: + "(c, t) \ set (uset p)" + "(d, s) \ set (uset p)" + "?I ((- Itm vs (x # bs) t / \c\\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \d\\<^sub>p\<^bsup>vs\<^esup>) / (1 + 1)) p" by auto let ?c = "\c\\<^sub>p\<^bsup>vs\<^esup>" let ?d = "\d\\<^sub>p\<^bsup>vs\<^esup>" let ?s = "Itm vs (x # bs) s" let ?t = "Itm vs (x # bs) t" have eq2: "\(x::'a). x + x = 2 * x" - by (simp add: field_simps) - {assume "?c = 0 \ ?d = 0" - with ct have ?D by simp} + by (simp add: field_simps) + { + assume "?c = 0 \ ?d = 0" + with ct have ?D by simp + } moreover - {assume z: "?c = 0" "?d \ 0" - from z have ?D using ct by auto} + { + assume z: "?c = 0" "?d \ 0" + from z have ?D using ct by auto + } moreover - {assume z: "?c \ 0" "?d = 0" - with ct have ?D by auto } + { + assume z: "?c \ 0" "?d = 0" + with ct have ?D by auto + } moreover - {assume z: "?c \ 0" "?d \ 0" + { + assume z: "?c \ 0" "?d \ 0" from z have ?F using ct - apply - apply (rule bexI[where x = "(c,t)"], simp_all) - by (rule bexI[where x = "(d,s)"], simp_all) - hence ?D by blast} - ultimately have ?D by auto} + apply - + apply (rule bexI[where x = "(c,t)"]) + apply simp_all + apply (rule bexI[where x = "(d,s)"]) + apply simp_all + done + then have ?D by blast + } + ultimately have ?D by auto + } ultimately show "?D" by blast next assume "?D" - moreover {assume m:"?M" from minusinf_ex[OF lp m] have "?E" .} - moreover {assume p: "?P" from plusinf_ex[OF lp p] have "?E" . } - moreover {assume f:"?F" hence "?E" by blast} + moreover { + assume m: "?M" + from minusinf_ex[OF lp m] have "?E" . + } + moreover { + assume p: "?P" + from plusinf_ex[OF lp p] have "?E" . + } + moreover { + assume f:"?F" + then have "?E" by blast + } ultimately show "?E" by blast qed @@ -2653,36 +3571,47 @@ definition "msubstleneg c t a b = Le (Neg (Add (Mul a t) (Mul c b)))" lemma msubsteq2: - assumes nz: "Ipoly vs c \ 0" and l: "islin (Eq (CNP 0 a b))" - shows "Ifm vs (x#bs) (msubsteq2 c t a b) = Ifm vs (((Itm vs (x#bs) t / Ipoly vs c ))#bs) (Eq (CNP 0 a b))" (is "?lhs = ?rhs") - using nz l tmbound0_I[of b vs x bs "Itm vs (x # bs) t / \c\\<^sub>p\<^bsup>vs\<^esup>" , symmetric] + assumes nz: "Ipoly vs c \ 0" + and l: "islin (Eq (CNP 0 a b))" + shows "Ifm vs (x#bs) (msubsteq2 c t a b) = + Ifm vs (((Itm vs (x#bs) t / Ipoly vs c ))#bs) (Eq (CNP 0 a b))" + using nz l tmbound0_I[of b vs x bs "Itm vs (x # bs) t / \c\\<^sub>p\<^bsup>vs\<^esup>", symmetric] by (simp add: msubsteq2_def field_simps) lemma msubstltpos: - assumes nz: "Ipoly vs c > 0" and l: "islin (Lt (CNP 0 a b))" - shows "Ifm vs (x#bs) (msubstltpos c t a b) = Ifm vs (((Itm vs (x#bs) t / Ipoly vs c ))#bs) (Lt (CNP 0 a b))" (is "?lhs = ?rhs") - using nz l tmbound0_I[of b vs x bs "Itm vs (x # bs) t / \c\\<^sub>p\<^bsup>vs\<^esup>" , symmetric] + assumes nz: "Ipoly vs c > 0" + and l: "islin (Lt (CNP 0 a b))" + shows "Ifm vs (x#bs) (msubstltpos c t a b) = + Ifm vs (((Itm vs (x#bs) t / Ipoly vs c ))#bs) (Lt (CNP 0 a b))" + using nz l tmbound0_I[of b vs x bs "Itm vs (x # bs) t / \c\\<^sub>p\<^bsup>vs\<^esup>", symmetric] by (simp add: msubstltpos_def field_simps) lemma msubstlepos: - assumes nz: "Ipoly vs c > 0" and l: "islin (Le (CNP 0 a b))" - shows "Ifm vs (x#bs) (msubstlepos c t a b) = Ifm vs (((Itm vs (x#bs) t / Ipoly vs c ))#bs) (Le (CNP 0 a b))" (is "?lhs = ?rhs") - using nz l tmbound0_I[of b vs x bs "Itm vs (x # bs) t / \c\\<^sub>p\<^bsup>vs\<^esup>" , symmetric] + assumes nz: "Ipoly vs c > 0" + and l: "islin (Le (CNP 0 a b))" + shows "Ifm vs (x#bs) (msubstlepos c t a b) = + Ifm vs (((Itm vs (x#bs) t / Ipoly vs c ))#bs) (Le (CNP 0 a b))" + using nz l tmbound0_I[of b vs x bs "Itm vs (x # bs) t / \c\\<^sub>p\<^bsup>vs\<^esup>", symmetric] by (simp add: msubstlepos_def field_simps) lemma msubstltneg: - assumes nz: "Ipoly vs c < 0" and l: "islin (Lt (CNP 0 a b))" - shows "Ifm vs (x#bs) (msubstltneg c t a b) = Ifm vs (((Itm vs (x#bs) t / Ipoly vs c ))#bs) (Lt (CNP 0 a b))" (is "?lhs = ?rhs") - using nz l tmbound0_I[of b vs x bs "Itm vs (x # bs) t / \c\\<^sub>p\<^bsup>vs\<^esup>" , symmetric] + assumes nz: "Ipoly vs c < 0" + and l: "islin (Lt (CNP 0 a b))" + shows "Ifm vs (x#bs) (msubstltneg c t a b) = + Ifm vs (((Itm vs (x#bs) t / Ipoly vs c ))#bs) (Lt (CNP 0 a b))" + using nz l tmbound0_I[of b vs x bs "Itm vs (x # bs) t / \c\\<^sub>p\<^bsup>vs\<^esup>", symmetric] by (simp add: msubstltneg_def field_simps del: minus_add_distrib) lemma msubstleneg: - assumes nz: "Ipoly vs c < 0" and l: "islin (Le (CNP 0 a b))" - shows "Ifm vs (x#bs) (msubstleneg c t a b) = Ifm vs (((Itm vs (x#bs) t / Ipoly vs c ))#bs) (Le (CNP 0 a b))" (is "?lhs = ?rhs") - using nz l tmbound0_I[of b vs x bs "Itm vs (x # bs) t / \c\\<^sub>p\<^bsup>vs\<^esup>" , symmetric] + assumes nz: "Ipoly vs c < 0" + and l: "islin (Le (CNP 0 a b))" + shows "Ifm vs (x#bs) (msubstleneg c t a b) = + Ifm vs (((Itm vs (x#bs) t / Ipoly vs c ))#bs) (Le (CNP 0 a b))" + using nz l tmbound0_I[of b vs x bs "Itm vs (x # bs) t / \c\\<^sub>p\<^bsup>vs\<^esup>", symmetric] by (simp add: msubstleneg_def field_simps del: minus_add_distrib) -fun msubstpos :: "fm \ poly \ tm \ fm" where +fun msubstpos :: "fm \ poly \ tm \ fm" +where "msubstpos (And p q) c t = And (msubstpos p c t) (msubstpos q c t)" | "msubstpos (Or p q) c t = Or (msubstpos p c t) (msubstpos q c t)" | "msubstpos (Eq (CNP 0 a r)) c t = msubsteq2 c t a r" @@ -2692,12 +3621,18 @@ | "msubstpos p c t = p" lemma msubstpos_I: - assumes lp: "islin p" and pos: "Ipoly vs c > 0" - shows "Ifm vs (x#bs) (msubstpos p c t) = Ifm vs (Itm vs (x#bs) t / Ipoly vs c #bs) p" + assumes lp: "islin p" + and pos: "Ipoly vs c > 0" + shows "Ifm vs (x#bs) (msubstpos p c t) = + Ifm vs (Itm vs (x#bs) t / Ipoly vs c #bs) p" using lp pos - by (induct p rule: islin.induct, auto simp add: msubsteq2 msubstltpos[OF pos] msubstlepos[OF pos] tmbound0_I[of _ vs "Itm vs (x # bs) t / \c\\<^sub>p\<^bsup>vs\<^esup>" bs x] bound0_I[of _ vs "Itm vs (x # bs) t / \c\\<^sub>p\<^bsup>vs\<^esup>" bs x] field_simps) - -fun msubstneg :: "fm \ poly \ tm \ fm" where + by (induct p rule: islin.induct) + (auto simp add: msubsteq2 msubstltpos[OF pos] msubstlepos[OF pos] + tmbound0_I[of _ vs "Itm vs (x # bs) t / \c\\<^sub>p\<^bsup>vs\<^esup>" bs x] + bound0_I[of _ vs "Itm vs (x # bs) t / \c\\<^sub>p\<^bsup>vs\<^esup>" bs x] field_simps) + +fun msubstneg :: "fm \ poly \ tm \ fm" +where "msubstneg (And p q) c t = And (msubstneg p c t) (msubstneg q c t)" | "msubstneg (Or p q) c t = Or (msubstneg p c t) (msubstneg q c t)" | "msubstneg (Eq (CNP 0 a r)) c t = msubsteq2 c t a r" @@ -2707,33 +3642,46 @@ | "msubstneg p c t = p" lemma msubstneg_I: - assumes lp: "islin p" and pos: "Ipoly vs c < 0" + assumes lp: "islin p" + and pos: "Ipoly vs c < 0" shows "Ifm vs (x#bs) (msubstneg p c t) = Ifm vs (Itm vs (x#bs) t / Ipoly vs c #bs) p" using lp pos - by (induct p rule: islin.induct, auto simp add: msubsteq2 msubstltneg[OF pos] msubstleneg[OF pos] tmbound0_I[of _ vs "Itm vs (x # bs) t / \c\\<^sub>p\<^bsup>vs\<^esup>" bs x] bound0_I[of _ vs "Itm vs (x # bs) t / \c\\<^sub>p\<^bsup>vs\<^esup>" bs x] field_simps) - - -definition "msubst2 p c t = disj (conj (lt (CP (polyneg c))) (simpfm (msubstpos p c t))) (conj (lt (CP c)) (simpfm (msubstneg p c t)))" - -lemma msubst2: assumes lp: "islin p" and nc: "isnpoly c" and nz: "Ipoly vs c \ 0" + by (induct p rule: islin.induct) + (auto simp add: msubsteq2 msubstltneg[OF pos] msubstleneg[OF pos] + tmbound0_I[of _ vs "Itm vs (x # bs) t / \c\\<^sub>p\<^bsup>vs\<^esup>" bs x] + bound0_I[of _ vs "Itm vs (x # bs) t / \c\\<^sub>p\<^bsup>vs\<^esup>" bs x] field_simps) + +definition + "msubst2 p c t = + disj + (conj (lt (CP (polyneg c))) (simpfm (msubstpos p c t))) + (conj (lt (CP c)) (simpfm (msubstneg p c t)))" + +lemma msubst2: + assumes lp: "islin p" + and nc: "isnpoly c" + and nz: "Ipoly vs c \ 0" shows "Ifm vs (x#bs) (msubst2 p c t) = Ifm vs (Itm vs (x#bs) t / Ipoly vs c #bs) p" -proof- +proof - let ?c = "Ipoly vs c" from nc have anc: "allpolys isnpoly (CP c)" "allpolys isnpoly (CP (~\<^sub>p c))" by (simp_all add: polyneg_norm) from nz have "?c > 0 \ ?c < 0" by arith moreover - {assume c: "?c < 0" + { + assume c: "?c < 0" from c msubstneg_I[OF lp c, of x bs t] lt[OF anc(1), of vs "x#bs"] lt[OF anc(2), of vs "x#bs"] - have ?thesis by (auto simp add: msubst2_def)} + have ?thesis by (auto simp add: msubst2_def) + } moreover - {assume c: "?c > 0" + { + assume c: "?c > 0" from c msubstpos_I[OF lp c, of x bs t] lt[OF anc(1), of vs "x#bs"] lt[OF anc(2), of vs "x#bs"] - have ?thesis by (auto simp add: msubst2_def)} + have ?thesis by (auto simp add: msubst2_def) + } ultimately show ?thesis by blast qed -term msubsteq2 lemma msubsteq2_nb: "tmbound0 t \ islin (Eq (CNP 0 a r)) \ bound0 (msubsteq2 c t a r)" by (simp add: msubsteq2_def) @@ -2747,20 +3695,30 @@ lemma msubstleneg_nb: "tmbound0 t \ islin (Le (CNP 0 a r)) \ bound0 (msubstleneg c t a r)" by (simp add: msubstleneg_def) -lemma msubstpos_nb: assumes lp: "islin p" and tnb: "tmbound0 t" +lemma msubstpos_nb: + assumes lp: "islin p" + and tnb: "tmbound0 t" shows "bound0 (msubstpos p c t)" -using lp tnb -by (induct p c t rule: msubstpos.induct, auto simp add: msubsteq2_nb msubstltpos_nb msubstlepos_nb) - -lemma msubstneg_nb: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" and lp: "islin p" and tnb: "tmbound0 t" + using lp tnb + by (induct p c t rule: msubstpos.induct) + (auto simp add: msubsteq2_nb msubstltpos_nb msubstlepos_nb) + +lemma msubstneg_nb: + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + and lp: "islin p" + and tnb: "tmbound0 t" shows "bound0 (msubstneg p c t)" -using lp tnb -by (induct p c t rule: msubstneg.induct, auto simp add: msubsteq2_nb msubstltneg_nb msubstleneg_nb) - -lemma msubst2_nb: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" and lp: "islin p" and tnb: "tmbound0 t" + using lp tnb + by (induct p c t rule: msubstneg.induct) + (auto simp add: msubsteq2_nb msubstltneg_nb msubstleneg_nb) + +lemma msubst2_nb: + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" + and lp: "islin p" + and tnb: "tmbound0 t" shows "bound0 (msubst2 p c t)" -using lp tnb -by (simp add: msubst2_def msubstneg_nb msubstpos_nb lt_nb simpfm_bound0) + using lp tnb + by (simp add: msubst2_def msubstneg_nb msubstpos_nb lt_nb simpfm_bound0) lemma mult_minus2_left: "-2 * (x::'a::comm_ring_1) = - (2 * x)" by simp @@ -2769,58 +3727,104 @@ by simp lemma islin_qf: "islin p \ qfree p" - by (induct p rule: islin.induct, auto simp add: bound0_qf) + by (induct p rule: islin.induct) (auto simp add: bound0_qf) + lemma fr_eq_msubst2: assumes lp: "islin p" - shows "(\x. Ifm vs (x#bs) p) \ ((Ifm vs (x#bs) (minusinf p)) \ (Ifm vs (x#bs) (plusinf p)) \ Ifm vs (x#bs) (subst0 (CP 0\<^sub>p) p) \ (\(n, t)\set (uset p). Ifm vs (x# bs) (msubst2 p (n *\<^sub>p (C (-2,1))) t)) \ (\(c,t) \ set (uset p). \(d,s) \ set (uset p). Ifm vs (x#bs) (msubst2 p (C (-2, 1) *\<^sub>p c*\<^sub>p d) (Add (Mul d t) (Mul c s)))))" + shows "(\x. Ifm vs (x#bs) p) \ + ((Ifm vs (x#bs) (minusinf p)) \ + (Ifm vs (x#bs) (plusinf p)) \ + Ifm vs (x#bs) (subst0 (CP 0\<^sub>p) p) \ + (\(n, t) \ set (uset p). + Ifm vs (x# bs) (msubst2 p (n *\<^sub>p (C (-2,1))) t)) \ + (\(c, t) \ set (uset p). \(d, s) \ set (uset p). + Ifm vs (x#bs) (msubst2 p (C (-2, 1) *\<^sub>p c*\<^sub>p d) (Add (Mul d t) (Mul c s)))))" (is "(\x. ?I x p) = (?M \ ?P \ ?Pz \ ?PU \ ?F)" is "?E = ?D") -proof- - from uset_l[OF lp] have th: "\(c, s)\set (uset p). isnpoly c \ tmbound0 s" by blast +proof - + from uset_l[OF lp] have th: "\(c, s)\set (uset p). isnpoly c \ tmbound0 s" + by blast let ?I = "\p. Ifm vs (x#bs) p" - have n2: "isnpoly (C (-2,1))" by (simp add: isnpoly_def) + have n2: "isnpoly (C (-2,1))" + by (simp add: isnpoly_def) note eq0 = subst0[OF islin_qf[OF lp], of vs x bs "CP 0\<^sub>p", simplified] - have eq1: "(\(n, t)\set (uset p). ?I (msubst2 p (n *\<^sub>p (C (-2,1))) t)) \ (\(n, t)\set (uset p). \n\\<^sub>p\<^bsup>vs\<^esup> \ 0 \ Ifm vs (- Itm vs (x # bs) t / (\n\\<^sub>p\<^bsup>vs\<^esup> * 2) # bs) p)" - proof- - {fix n t assume H: "(n, t)\set (uset p)" "?I(msubst2 p (n *\<^sub>p C (-2, 1)) t)" - from H(1) th have "isnpoly n" by blast - hence nn: "isnpoly (n *\<^sub>p (C (-2,1)))" by (simp_all add: polymul_norm n2) + have eq1: "(\(n, t) \ set (uset p). ?I (msubst2 p (n *\<^sub>p (C (-2,1))) t)) \ + (\(n, t) \ set (uset p). + \n\\<^sub>p\<^bsup>vs\<^esup> \ 0 \ + Ifm vs (- Itm vs (x # bs) t / (\n\\<^sub>p\<^bsup>vs\<^esup> * 2) # bs) p)" + proof - + { + fix n t + assume H: "(n, t) \ set (uset p)" "?I(msubst2 p (n *\<^sub>p C (-2, 1)) t)" + from H(1) th have "isnpoly n" + by blast + then have nn: "isnpoly (n *\<^sub>p (C (-2,1)))" + by (simp_all add: polymul_norm n2) have nn': "allpolys isnpoly (CP (~\<^sub>p (n *\<^sub>p C (-2, 1))))" by (simp add: polyneg_norm nn) - hence nn2: "\n *\<^sub>p(C (-2,1)) \\<^sub>p\<^bsup>vs\<^esup> \ 0" "\n \\<^sub>p\<^bsup>vs\<^esup> \ 0" using H(2) nn' nn + then have nn2: "\n *\<^sub>p(C (-2,1)) \\<^sub>p\<^bsup>vs\<^esup> \ 0" "\n \\<^sub>p\<^bsup>vs\<^esup> \ 0" + using H(2) nn' nn by (auto simp add: msubst2_def lt zero_less_mult_iff mult_less_0_iff) from msubst2[OF lp nn nn2(1), of x bs t] have "\n\\<^sub>p\<^bsup>vs\<^esup> \ 0 \ Ifm vs (- Itm vs (x # bs) t / (\n\\<^sub>p\<^bsup>vs\<^esup> * 2) # bs) p" - using H(2) nn2 by (simp add: mult_minus2_right)} + using H(2) nn2 by (simp add: mult_minus2_right) + } moreover - {fix n t assume H: "(n, t)\set (uset p)" "\n\\<^sub>p\<^bsup>vs\<^esup> \ 0" "Ifm vs (- Itm vs (x # bs) t / (\n\\<^sub>p\<^bsup>vs\<^esup> * 2) # bs) p" - from H(1) th have "isnpoly n" by blast - hence nn: "isnpoly (n *\<^sub>p (C (-2,1)))" "\n *\<^sub>p(C (-2,1)) \\<^sub>p\<^bsup>vs\<^esup> \ 0" + { + fix n t + assume H: + "(n, t) \ set (uset p)" "\n\\<^sub>p\<^bsup>vs\<^esup> \ 0" + "Ifm vs (- Itm vs (x # bs) t / (\n\\<^sub>p\<^bsup>vs\<^esup> * 2) # bs) p" + from H(1) th have "isnpoly n" + by blast + then have nn: "isnpoly (n *\<^sub>p (C (-2,1)))" "\n *\<^sub>p(C (-2,1)) \\<^sub>p\<^bsup>vs\<^esup> \ 0" using H(2) by (simp_all add: polymul_norm n2) - from msubst2[OF lp nn, of x bs t] have "?I (msubst2 p (n *\<^sub>p (C (-2,1))) t)" using H(2,3) by (simp add: mult_minus2_right)} + from msubst2[OF lp nn, of x bs t] have "?I (msubst2 p (n *\<^sub>p (C (-2,1))) t)" + using H(2,3) by (simp add: mult_minus2_right) + } ultimately show ?thesis by blast qed - have eq2: "(\(c,t) \ set (uset p). \(d,s) \ set (uset p). Ifm vs (x#bs) (msubst2 p (C (-2, 1) *\<^sub>p c*\<^sub>p d) (Add (Mul d t) (Mul c s)))) \ (\(n, t)\set (uset p). - \(m, s)\set (uset p). \n\\<^sub>p\<^bsup>vs\<^esup> \ 0 \ \m\\<^sub>p\<^bsup>vs\<^esup> \ 0 \ Ifm vs ((- Itm vs (x # bs) t / \n\\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \m\\<^sub>p\<^bsup>vs\<^esup>) / 2 # bs) p)" - proof- - {fix c t d s assume H: "(c,t) \ set (uset p)" "(d,s) \ set (uset p)" - "Ifm vs (x#bs) (msubst2 p (C (-2, 1) *\<^sub>p c*\<^sub>p d) (Add (Mul d t) (Mul c s)))" - from H(1,2) th have "isnpoly c" "isnpoly d" by blast+ - hence nn: "isnpoly (C (-2, 1) *\<^sub>p c*\<^sub>p d)" + have eq2: "(\(c, t) \ set (uset p). \(d, s) \ set (uset p). + Ifm vs (x#bs) (msubst2 p (C (-2, 1) *\<^sub>p c*\<^sub>p d) (Add (Mul d t) (Mul c s)))) \ + (\(n, t)\set (uset p). \(m, s)\set (uset p). + \n\\<^sub>p\<^bsup>vs\<^esup> \ 0 \ + \m\\<^sub>p\<^bsup>vs\<^esup> \ 0 \ + Ifm vs ((- Itm vs (x # bs) t / \n\\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \m\\<^sub>p\<^bsup>vs\<^esup>) / 2 # bs) p)" + proof - + { + fix c t d s + assume H: + "(c,t) \ set (uset p)" "(d,s) \ set (uset p)" + "Ifm vs (x#bs) (msubst2 p (C (-2, 1) *\<^sub>p c*\<^sub>p d) (Add (Mul d t) (Mul c s)))" + from H(1,2) th have "isnpoly c" "isnpoly d" + by blast+ + then have nn: "isnpoly (C (-2, 1) *\<^sub>p c*\<^sub>p d)" by (simp_all add: polymul_norm n2) - have stupid: "allpolys isnpoly (CP (~\<^sub>p (C (-2, 1) *\<^sub>p c *\<^sub>p d)))" "allpolys isnpoly (CP ((C (-2, 1) *\<^sub>p c *\<^sub>p d)))" + have stupid: + "allpolys isnpoly (CP (~\<^sub>p (C (-2, 1) *\<^sub>p c *\<^sub>p d)))" + "allpolys isnpoly (CP ((C (-2, 1) *\<^sub>p c *\<^sub>p d)))" by (simp_all add: polyneg_norm nn) have nn': "\(C (-2, 1) *\<^sub>p c*\<^sub>p d)\\<^sub>p\<^bsup>vs\<^esup> \ 0" "\c\\<^sub>p\<^bsup>vs\<^esup> \ 0" "\d\\<^sub>p\<^bsup>vs\<^esup> \ 0" - using H(3) by (auto simp add: msubst2_def lt[OF stupid(1)] lt[OF stupid(2)] zero_less_mult_iff mult_less_0_iff) + using H(3) + by (auto simp add: msubst2_def lt[OF stupid(1)] + lt[OF stupid(2)] zero_less_mult_iff mult_less_0_iff) from msubst2[OF lp nn nn'(1), of x bs ] H(3) nn' - have "\c\\<^sub>p\<^bsup>vs\<^esup> \ 0 \ \d\\<^sub>p\<^bsup>vs\<^esup> \ 0 \ Ifm vs ((- Itm vs (x # bs) t / \c\\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \d\\<^sub>p\<^bsup>vs\<^esup>) / 2 # bs) p" + have "\c\\<^sub>p\<^bsup>vs\<^esup> \ 0 \ \d\\<^sub>p\<^bsup>vs\<^esup> \ 0 \ + Ifm vs ((- Itm vs (x # bs) t / \c\\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \d\\<^sub>p\<^bsup>vs\<^esup>) / 2 # bs) p" by (simp add: add_divide_distrib diff_divide_distrib mult_minus2_left mult_commute) } moreover - {fix c t d s assume H: "(c,t) \ set (uset p)" "(d,s) \ set (uset p)" - "\c\\<^sub>p\<^bsup>vs\<^esup> \ 0" "\d\\<^sub>p\<^bsup>vs\<^esup> \ 0" "Ifm vs ((- Itm vs (x # bs) t / \c\\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \d\\<^sub>p\<^bsup>vs\<^esup>) / 2 # bs) p" - from H(1,2) th have "isnpoly c" "isnpoly d" by blast+ - hence nn: "isnpoly (C (-2, 1) *\<^sub>p c*\<^sub>p d)" "\(C (-2, 1) *\<^sub>p c*\<^sub>p d)\\<^sub>p\<^bsup>vs\<^esup> \ 0" + { + fix c t d s + assume H: + "(c, t) \ set (uset p)" + "(d, s) \ set (uset p)" + "\c\\<^sub>p\<^bsup>vs\<^esup> \ 0" + "\d\\<^sub>p\<^bsup>vs\<^esup> \ 0" + "Ifm vs ((- Itm vs (x # bs) t / \c\\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \d\\<^sub>p\<^bsup>vs\<^esup>) / 2 # bs) p" + from H(1,2) th have "isnpoly c" "isnpoly d" + by blast+ + then have nn: "isnpoly (C (-2, 1) *\<^sub>p c*\<^sub>p d)" "\(C (-2, 1) *\<^sub>p c*\<^sub>p d)\\<^sub>p\<^bsup>vs\<^esup> \ 0" using H(3,4) by (simp_all add: polymul_norm n2) from msubst2[OF lp nn, of x bs ] H(3,4,5) have "Ifm vs (x#bs) (msubst2 p (C (-2, 1) *\<^sub>p c*\<^sub>p d) (Add (Mul d t) (Mul c s)))" @@ -2833,20 +3837,34 @@ qed definition -"ferrack2 p \ let q = simpfm p ; mp = minusinf q ; pp = plusinf q - in if (mp = T \ pp = T) then T - else (let U = remdups (uset q) - in decr0 (list_disj [mp, pp, simpfm (subst0 (CP 0\<^sub>p) q), evaldjf (\(c,t). msubst2 q (c *\<^sub>p C (-2, 1)) t) U, - evaldjf (\((b,a),(d,c)). msubst2 q (C (-2, 1) *\<^sub>p b*\<^sub>p d) (Add (Mul d a) (Mul b c))) (alluopairs U)]))" + "ferrack2 p \ + let + q = simpfm p; + mp = minusinf q; + pp = plusinf q + in + if (mp = T \ pp = T) then T + else + (let U = remdups (uset q) + in + decr0 + (list_disj + [mp, + pp, + simpfm (subst0 (CP 0\<^sub>p) q), + evaldjf (\(c, t). msubst2 q (c *\<^sub>p C (-2, 1)) t) U, + evaldjf (\((b, a),(d, c)). + msubst2 q (C (-2, 1) *\<^sub>p b*\<^sub>p d) (Add (Mul d a) (Mul b c))) (alluopairs U)]))" definition "frpar2 p = simpfm (qelim (prep p) ferrack2)" -lemma ferrack2: assumes qf: "qfree p" - shows "qfree (ferrack2 p) \ ((Ifm vs bs (ferrack2 p)) = (Ifm vs bs (E p)))" +lemma ferrack2: + assumes qf: "qfree p" + shows "qfree (ferrack2 p) \ Ifm vs bs (ferrack2 p) = Ifm vs bs (E p)" (is "_ \ (?rhs = ?lhs)") -proof- - let ?J = "\ x p. Ifm vs (x#bs) p" - let ?N = "\ t. Ipoly vs t" +proof - + let ?J = "\x p. Ifm vs (x#bs) p" + let ?N = "\t. Ipoly vs t" let ?Nt = "\x t. Itm vs (x#bs) t" let ?q = "simpfm p" let ?qz = "subst0 (CP 0\<^sub>p) ?q" @@ -2854,68 +3872,109 @@ let ?Up = "alluopairs ?U" let ?mp = "minusinf ?q" let ?pp = "plusinf ?q" + fix x let ?I = "\p. Ifm vs (x#bs) p" from simpfm_lin[OF qf] simpfm_qf[OF qf] have lq: "islin ?q" and q_qf: "qfree ?q" . from minusinf_nb[OF lq] plusinf_nb[OF lq] have mp_nb: "bound0 ?mp" and pp_nb: "bound0 ?pp" . from bound0_qf[OF mp_nb] bound0_qf[OF pp_nb] have mp_qf: "qfree ?mp" and pp_qf: "qfree ?pp" . - from uset_l[OF lq] have U_l: "\(c, s)\set ?U. isnpoly c \ c \ 0\<^sub>p \ tmbound0 s \ allpolys isnpoly s" + from uset_l[OF lq] + have U_l: "\(c, s)\set ?U. isnpoly c \ c \ 0\<^sub>p \ tmbound0 s \ allpolys isnpoly s" by simp have bnd0: "\x \ set ?U. bound0 ((\(c,t). msubst2 ?q (c *\<^sub>p C (-2, 1)) t) x)" - proof- - {fix c t assume ct: "(c,t) \ set ?U" - hence tnb: "tmbound0 t" using U_l by blast + proof - + { + fix c t + assume ct: "(c, t) \ set ?U" + then have tnb: "tmbound0 t" + using U_l by blast from msubst2_nb[OF lq tnb] - have "bound0 ((\(c,t). msubst2 ?q (c *\<^sub>p C (-2, 1)) t) (c,t))" by simp} - thus ?thesis by auto + have "bound0 ((\(c,t). msubst2 ?q (c *\<^sub>p C (-2, 1)) t) (c,t))" by simp + } + then show ?thesis by auto qed - have bnd1: "\x \ set ?Up. bound0 ((\((b,a),(d,c)). msubst2 ?q (C (-2, 1) *\<^sub>p b*\<^sub>p d) (Add (Mul d a) (Mul b c))) x)" - proof- - {fix b a d c assume badc: "((b,a),(d,c)) \ set ?Up" + have bnd1: "\x \ set ?Up. bound0 ((\((b, a), (d, c)). + msubst2 ?q (C (-2, 1) *\<^sub>p b*\<^sub>p d) (Add (Mul d a) (Mul b c))) x)" + proof - + { + fix b a d c + assume badc: "((b,a),(d,c)) \ set ?Up" from badc U_l alluopairs_set1[of ?U] - have nb: "tmbound0 (Add (Mul d a) (Mul b c))" by auto - from msubst2_nb[OF lq nb] have "bound0 ((\((b,a),(d,c)). msubst2 ?q (C (-2, 1) *\<^sub>p b*\<^sub>p d) (Add (Mul d a) (Mul b c))) ((b,a),(d,c)))" by simp} - thus ?thesis by auto + have nb: "tmbound0 (Add (Mul d a) (Mul b c))" + by auto + from msubst2_nb[OF lq nb] + have "bound0 ((\((b, a),(d, c)). + msubst2 ?q (C (-2, 1) *\<^sub>p b*\<^sub>p d) (Add (Mul d a) (Mul b c))) ((b,a),(d,c)))" + by simp + } + then show ?thesis by auto qed - have stupid: "bound0 F" by simp - let ?R = "list_disj [?mp, ?pp, simpfm (subst0 (CP 0\<^sub>p) ?q), evaldjf (\(c,t). msubst2 ?q (c *\<^sub>p C (-2, 1)) t) ?U, - evaldjf (\((b,a),(d,c)). msubst2 ?q (C (-2, 1) *\<^sub>p b*\<^sub>p d) (Add (Mul d a) (Mul b c))) (alluopairs ?U)]" - from subst0_nb[of "CP 0\<^sub>p" ?q] q_qf evaldjf_bound0[OF bnd1] evaldjf_bound0[OF bnd0] mp_nb pp_nb stupid - have nb: "bound0 ?R " + have stupid: "bound0 F" + by simp + let ?R = + "list_disj + [?mp, + ?pp, + simpfm (subst0 (CP 0\<^sub>p) ?q), + evaldjf (\(c,t). msubst2 ?q (c *\<^sub>p C (-2, 1)) t) ?U, + evaldjf (\((b,a),(d,c)). + msubst2 ?q (C (-2, 1) *\<^sub>p b*\<^sub>p d) (Add (Mul d a) (Mul b c))) (alluopairs ?U)]" + from subst0_nb[of "CP 0\<^sub>p" ?q] q_qf + evaldjf_bound0[OF bnd1] evaldjf_bound0[OF bnd0] mp_nb pp_nb stupid + have nb: "bound0 ?R" by (simp add: list_disj_def simpfm_bound0) - let ?s = "\((b,a),(d,c)). msubst2 ?q (C (-2, 1) *\<^sub>p b*\<^sub>p d) (Add (Mul d a) (Mul b c))" - - {fix b a d c assume baU: "(b,a) \ set ?U" and dcU: "(d,c) \ set ?U" + let ?s = "\((b, a),(d, c)). msubst2 ?q (C (-2, 1) *\<^sub>p b*\<^sub>p d) (Add (Mul d a) (Mul b c))" + + { + fix b a d c + assume baU: "(b,a) \ set ?U" and dcU: "(d,c) \ set ?U" from U_l baU dcU have norm: "isnpoly b" "isnpoly d" "isnpoly (C (-2, 1))" by auto (simp add: isnpoly_def) have norm2: "isnpoly (C (-2, 1) *\<^sub>p b*\<^sub>p d)" "isnpoly (C (-2, 1) *\<^sub>p d*\<^sub>p b)" using norm by (simp_all add: polymul_norm) - have stupid: "allpolys isnpoly (CP (C (-2, 1) *\<^sub>p b*\<^sub>p d))" "allpolys isnpoly (CP (C (-2, 1) *\<^sub>p d*\<^sub>p b))" "allpolys isnpoly (CP (~\<^sub>p(C (-2, 1) *\<^sub>p b*\<^sub>p d)))" "allpolys isnpoly (CP (~\<^sub>p(C (-2, 1) *\<^sub>p d*\<^sub>p b)))" + have stupid: + "allpolys isnpoly (CP (C (-2, 1) *\<^sub>p b *\<^sub>p d))" + "allpolys isnpoly (CP (C (-2, 1) *\<^sub>p d *\<^sub>p b))" + "allpolys isnpoly (CP (~\<^sub>p(C (-2, 1) *\<^sub>p b *\<^sub>p d)))" + "allpolys isnpoly (CP (~\<^sub>p(C (-2, 1) *\<^sub>p d*\<^sub>p b)))" by (simp_all add: polyneg_norm norm2) - have "?I (msubst2 ?q (C (-2, 1) *\<^sub>p b*\<^sub>p d) (Add (Mul d a) (Mul b c))) = ?I (msubst2 ?q (C (-2, 1) *\<^sub>p d*\<^sub>p b) (Add (Mul b c) (Mul d a)))" (is "?lhs \ ?rhs") + have "?I (msubst2 ?q (C (-2, 1) *\<^sub>p b*\<^sub>p d) (Add (Mul d a) (Mul b c))) = + ?I (msubst2 ?q (C (-2, 1) *\<^sub>p d*\<^sub>p b) (Add (Mul b c) (Mul d a)))" + (is "?lhs \ ?rhs") proof assume H: ?lhs - hence z: "\C (-2, 1) *\<^sub>p b *\<^sub>p d\\<^sub>p\<^bsup>vs\<^esup> \ 0" "\C (-2, 1) *\<^sub>p d *\<^sub>p b\\<^sub>p\<^bsup>vs\<^esup> \ 0" - by (auto simp add: msubst2_def lt[OF stupid(3)] lt[OF stupid(1)] mult_less_0_iff zero_less_mult_iff) - from msubst2[OF lq norm2(1) z(1), of x bs] - msubst2[OF lq norm2(2) z(2), of x bs] H - show ?rhs by (simp add: field_simps) + then have z: "\C (-2, 1) *\<^sub>p b *\<^sub>p d\\<^sub>p\<^bsup>vs\<^esup> \ 0" "\C (-2, 1) *\<^sub>p d *\<^sub>p b\\<^sub>p\<^bsup>vs\<^esup> \ 0" + by (auto simp add: msubst2_def lt[OF stupid(3)] lt[OF stupid(1)] + mult_less_0_iff zero_less_mult_iff) + from msubst2[OF lq norm2(1) z(1), of x bs] msubst2[OF lq norm2(2) z(2), of x bs] H + show ?rhs + by (simp add: field_simps) next assume H: ?rhs - hence z: "\C (-2, 1) *\<^sub>p b *\<^sub>p d\\<^sub>p\<^bsup>vs\<^esup> \ 0" "\C (-2, 1) *\<^sub>p d *\<^sub>p b\\<^sub>p\<^bsup>vs\<^esup> \ 0" - by (auto simp add: msubst2_def lt[OF stupid(4)] lt[OF stupid(2)] mult_less_0_iff zero_less_mult_iff) - from msubst2[OF lq norm2(1) z(1), of x bs] - msubst2[OF lq norm2(2) z(2), of x bs] H - show ?lhs by (simp add: field_simps) - qed} - hence th0: "\x \ set ?U. \y \ set ?U. ?I (?s (x, y)) \ ?I (?s (y, x))" - by clarsimp - - have "?lhs \ (\x. Ifm vs (x#bs) ?q)" by simp - also have "\ \ ?I ?mp \ ?I ?pp \ ?I (subst0 (CP 0\<^sub>p) ?q) \ (\(n,t) \ set ?U. ?I (msubst2 ?q (n *\<^sub>p C (-2, 1)) t)) \ (\(b, a)\set ?U. \(d, c)\set ?U. ?I (msubst2 ?q (C (-2, 1) *\<^sub>p b*\<^sub>p d) (Add (Mul d a) (Mul b c))))" + then have z: "\C (-2, 1) *\<^sub>p b *\<^sub>p d\\<^sub>p\<^bsup>vs\<^esup> \ 0" "\C (-2, 1) *\<^sub>p d *\<^sub>p b\\<^sub>p\<^bsup>vs\<^esup> \ 0" + by (auto simp add: msubst2_def lt[OF stupid(4)] lt[OF stupid(2)] + mult_less_0_iff zero_less_mult_iff) + from msubst2[OF lq norm2(1) z(1), of x bs] msubst2[OF lq norm2(2) z(2), of x bs] H + show ?lhs + by (simp add: field_simps) + qed + } + then have th0: "\x \ set ?U. \y \ set ?U. ?I (?s (x, y)) \ ?I (?s (y, x))" + by auto + + have "?lhs \ (\x. Ifm vs (x#bs) ?q)" + by simp + also have "\ \ ?I ?mp \ ?I ?pp \ ?I (subst0 (CP 0\<^sub>p) ?q) \ + (\(n, t) \ set ?U. ?I (msubst2 ?q (n *\<^sub>p C (-2, 1)) t)) \ + (\(b, a) \ set ?U. \(d, c) \ set ?U. + ?I (msubst2 ?q (C (-2, 1) *\<^sub>p b*\<^sub>p d) (Add (Mul d a) (Mul b c))))" using fr_eq_msubst2[OF lq, of vs bs x] by simp - also have "\ \ ?I ?mp \ ?I ?pp \ ?I (subst0 (CP 0\<^sub>p) ?q) \ (\(n,t) \ set ?U. ?I (msubst2 ?q (n *\<^sub>p C (-2, 1)) t)) \ (\x\set ?U. \y \set ?U. ?I (?s (x,y)))" + also have "\ \ ?I ?mp \ ?I ?pp \ ?I (subst0 (CP 0\<^sub>p) ?q) \ + (\(n, t) \ set ?U. ?I (msubst2 ?q (n *\<^sub>p C (-2, 1)) t)) \ + (\x \ set ?U. \y \set ?U. ?I (?s (x, y)))" by (simp add: split_def) - also have "\ \ ?I ?mp \ ?I ?pp \ ?I (subst0 (CP 0\<^sub>p) ?q) \ (\(n,t) \ set ?U. ?I (msubst2 ?q (n *\<^sub>p C (-2, 1)) t)) \ (\(x,y) \ set ?Up. ?I (?s (x,y)))" + also have "\ \ ?I ?mp \ ?I ?pp \ ?I (subst0 (CP 0\<^sub>p) ?q) \ + (\(n, t) \ set ?U. ?I (msubst2 ?q (n *\<^sub>p C (-2, 1)) t)) \ + (\(x, y) \ set ?Up. ?I (?s (x, y)))" using alluopairs_bex[OF th0] by simp also have "\ \ ?I ?R" by (simp add: list_disj_def evaldjf_ex split_def) @@ -2925,9 +3984,10 @@ apply (simp add: list_disj_def) apply (cases "?pp = T") apply (simp add: list_disj_def) - by (simp_all add: Let_def decr0[OF nb]) + apply (simp_all add: Let_def decr0[OF nb]) + done finally show ?thesis using decr0_qf[OF nb] - by (simp add: ferrack2_def Let_def) + by (simp add: ferrack2_def Let_def) qed lemma frpar2: "qfree (frpar2 p) \ (Ifm vs bs (frpar2 p) \ Ifm vs bs p)" @@ -2936,7 +3996,8 @@ have th: "\bs p. qfree p \ qfree (ferrack2 p) \ Ifm vs bs (ferrack2 p) = Ifm vs bs (E p)" by blast from qelim[OF th, of "prep p" bs] - show ?thesis unfolding frpar2_def by (auto simp add: prep) + show ?thesis + unfolding frpar2_def by (auto simp add: prep) qed oracle frpar_oracle = {* @@ -2962,31 +4023,47 @@ val k = find_index (fn t' => t aconv t') ts; in if k < 0 then raise General.Subscript else k end; -fun num_of_term ps (Const (@{const_name Groups.uminus}, _) $ t) = @{code poly.Neg} (num_of_term ps t) - | num_of_term ps (Const (@{const_name Groups.plus}, _) $ a $ b) = @{code poly.Add} (num_of_term ps a, num_of_term ps b) - | num_of_term ps (Const (@{const_name Groups.minus}, _) $ a $ b) = @{code poly.Sub} (num_of_term ps a, num_of_term ps b) - | num_of_term ps (Const (@{const_name Groups.times}, _) $ a $ b) = @{code poly.Mul} (num_of_term ps a, num_of_term ps b) - | num_of_term ps (Const (@{const_name Power.power}, _) $ a $ n) = @{code poly.Pw} (num_of_term ps a, @{code nat_of_integer} (dest_nat n)) - | num_of_term ps (Const (@{const_name Fields.divide}, _) $ a $ b) = mk_C (dest_num a, dest_num b) - | num_of_term ps t = (case try_dest_num t - of SOME k => mk_C (k, 1) +fun num_of_term ps (Const (@{const_name Groups.uminus}, _) $ t) = + @{code poly.Neg} (num_of_term ps t) + | num_of_term ps (Const (@{const_name Groups.plus}, _) $ a $ b) = + @{code poly.Add} (num_of_term ps a, num_of_term ps b) + | num_of_term ps (Const (@{const_name Groups.minus}, _) $ a $ b) = + @{code poly.Sub} (num_of_term ps a, num_of_term ps b) + | num_of_term ps (Const (@{const_name Groups.times}, _) $ a $ b) = + @{code poly.Mul} (num_of_term ps a, num_of_term ps b) + | num_of_term ps (Const (@{const_name Power.power}, _) $ a $ n) = + @{code poly.Pw} (num_of_term ps a, @{code nat_of_integer} (dest_nat n)) + | num_of_term ps (Const (@{const_name Fields.divide}, _) $ a $ b) = + mk_C (dest_num a, dest_num b) + | num_of_term ps t = + (case try_dest_num t of + SOME k => mk_C (k, 1) | NONE => mk_poly_Bound (the_index ps t)); -fun tm_of_term fs ps (Const(@{const_name Groups.uminus}, _) $ t) = @{code Neg} (tm_of_term fs ps t) - | tm_of_term fs ps (Const(@{const_name Groups.plus}, _) $ a $ b) = @{code Add} (tm_of_term fs ps a, tm_of_term fs ps b) - | tm_of_term fs ps (Const(@{const_name Groups.minus}, _) $ a $ b) = @{code Sub} (tm_of_term fs ps a, tm_of_term fs ps b) - | tm_of_term fs ps (Const(@{const_name Groups.times}, _) $ a $ b) = @{code Mul} (num_of_term ps a, tm_of_term fs ps b) +fun tm_of_term fs ps (Const(@{const_name Groups.uminus}, _) $ t) = + @{code Neg} (tm_of_term fs ps t) + | tm_of_term fs ps (Const(@{const_name Groups.plus}, _) $ a $ b) = + @{code Add} (tm_of_term fs ps a, tm_of_term fs ps b) + | tm_of_term fs ps (Const(@{const_name Groups.minus}, _) $ a $ b) = + @{code Sub} (tm_of_term fs ps a, tm_of_term fs ps b) + | tm_of_term fs ps (Const(@{const_name Groups.times}, _) $ a $ b) = + @{code Mul} (num_of_term ps a, tm_of_term fs ps b) | tm_of_term fs ps t = (@{code CP} (num_of_term ps t) handle TERM _ => mk_Bound (the_index fs t) - | General.Subscript => mk_Bound (the_index fs t)); + | General.Subscript => mk_Bound (the_index fs t)); fun fm_of_term fs ps @{term True} = @{code T} | fm_of_term fs ps @{term False} = @{code F} - | fm_of_term fs ps (Const (@{const_name Not}, _) $ p) = @{code NOT} (fm_of_term fs ps p) - | fm_of_term fs ps (Const (@{const_name HOL.conj}, _) $ p $ q) = @{code And} (fm_of_term fs ps p, fm_of_term fs ps q) - | fm_of_term fs ps (Const (@{const_name HOL.disj}, _) $ p $ q) = @{code Or} (fm_of_term fs ps p, fm_of_term fs ps q) - | fm_of_term fs ps (Const (@{const_name HOL.implies}, _) $ p $ q) = @{code Imp} (fm_of_term fs ps p, fm_of_term fs ps q) - | fm_of_term fs ps (@{term HOL.iff} $ p $ q) = @{code Iff} (fm_of_term fs ps p, fm_of_term fs ps q) + | fm_of_term fs ps (Const (@{const_name Not}, _) $ p) = + @{code NOT} (fm_of_term fs ps p) + | fm_of_term fs ps (Const (@{const_name HOL.conj}, _) $ p $ q) = + @{code And} (fm_of_term fs ps p, fm_of_term fs ps q) + | fm_of_term fs ps (Const (@{const_name HOL.disj}, _) $ p $ q) = + @{code Or} (fm_of_term fs ps p, fm_of_term fs ps q) + | fm_of_term fs ps (Const (@{const_name HOL.implies}, _) $ p $ q) = + @{code Imp} (fm_of_term fs ps p, fm_of_term fs ps q) + | fm_of_term fs ps (@{term HOL.iff} $ p $ q) = + @{code Iff} (fm_of_term fs ps p, fm_of_term fs ps q) | fm_of_term fs ps (Const (@{const_name HOL.eq}, T) $ p $ q) = @{code Eq} (@{code Sub} (tm_of_term fs ps p, tm_of_term fs ps q)) | fm_of_term fs ps (Const (@{const_name Orderings.less}, _) $ p $ q) = @@ -3009,38 +4086,62 @@ in (if d = 1 then HOLogic.mk_number T c else if d = 0 then Const (@{const_name Groups.zero}, T) - else Const (@{const_name Fields.divide}, binopT T) $ HOLogic.mk_number T c $ HOLogic.mk_number T d) + else + Const (@{const_name Fields.divide}, binopT T) $ + HOLogic.mk_number T c $ HOLogic.mk_number T d) end | term_of_num T ps (@{code poly.Bound} i) = nth ps (@{code integer_of_nat} i) - | term_of_num T ps (@{code poly.Add} (a, b)) = Const (@{const_name Groups.plus}, binopT T) $ term_of_num T ps a $ term_of_num T ps b - | term_of_num T ps (@{code poly.Mul} (a, b)) = Const (@{const_name Groups.times}, binopT T) $ term_of_num T ps a $ term_of_num T ps b - | term_of_num T ps (@{code poly.Sub} (a, b)) = Const (@{const_name Groups.minus}, binopT T) $ term_of_num T ps a $ term_of_num T ps b - | term_of_num T ps (@{code poly.Neg} a) = Const (@{const_name Groups.uminus}, T --> T) $ term_of_num T ps a - | term_of_num T ps (@{code poly.Pw} (a, n)) = Const (@{const_name Power.power}, - T --> @{typ nat} --> T) $ term_of_num T ps a $ HOLogic.mk_number HOLogic.natT (@{code integer_of_nat} n) + | term_of_num T ps (@{code poly.Add} (a, b)) = + Const (@{const_name Groups.plus}, binopT T) $ term_of_num T ps a $ term_of_num T ps b + | term_of_num T ps (@{code poly.Mul} (a, b)) = + Const (@{const_name Groups.times}, binopT T) $ term_of_num T ps a $ term_of_num T ps b + | term_of_num T ps (@{code poly.Sub} (a, b)) = + Const (@{const_name Groups.minus}, binopT T) $ term_of_num T ps a $ term_of_num T ps b + | term_of_num T ps (@{code poly.Neg} a) = + Const (@{const_name Groups.uminus}, T --> T) $ term_of_num T ps a + | term_of_num T ps (@{code poly.Pw} (a, n)) = + Const (@{const_name Power.power}, T --> @{typ nat} --> T) $ + term_of_num T ps a $ HOLogic.mk_number HOLogic.natT (@{code integer_of_nat} n) | term_of_num T ps (@{code poly.CN} (c, n, p)) = term_of_num T ps (@{code poly.Add} (c, @{code poly.Mul} (@{code poly.Bound} n, p))); fun term_of_tm T fs ps (@{code CP} p) = term_of_num T ps p | term_of_tm T fs ps (@{code Bound} i) = nth fs (@{code integer_of_nat} i) - | term_of_tm T fs ps (@{code Add} (a, b)) = Const (@{const_name Groups.plus}, binopT T) $ term_of_tm T fs ps a $ term_of_tm T fs ps b - | term_of_tm T fs ps (@{code Mul} (a, b)) = Const (@{const_name Groups.times}, binopT T) $ term_of_num T ps a $ term_of_tm T fs ps b - | term_of_tm T fs ps (@{code Sub} (a, b)) = Const (@{const_name Groups.minus}, binopT T) $ term_of_tm T fs ps a $ term_of_tm T fs ps b - | term_of_tm T fs ps (@{code Neg} a) = Const (@{const_name Groups.uminus}, T --> T) $ term_of_tm T fs ps a - | term_of_tm T fs ps (@{code CNP} (n, c, p)) = term_of_tm T fs ps - (@{code Add} (@{code Mul} (c, @{code Bound} n), p)); + | term_of_tm T fs ps (@{code Add} (a, b)) = + Const (@{const_name Groups.plus}, binopT T) $ term_of_tm T fs ps a $ term_of_tm T fs ps b + | term_of_tm T fs ps (@{code Mul} (a, b)) = + Const (@{const_name Groups.times}, binopT T) $ term_of_num T ps a $ term_of_tm T fs ps b + | term_of_tm T fs ps (@{code Sub} (a, b)) = + Const (@{const_name Groups.minus}, binopT T) $ term_of_tm T fs ps a $ term_of_tm T fs ps b + | term_of_tm T fs ps (@{code Neg} a) = + Const (@{const_name Groups.uminus}, T --> T) $ term_of_tm T fs ps a + | term_of_tm T fs ps (@{code CNP} (n, c, p)) = + term_of_tm T fs ps (@{code Add} (@{code Mul} (c, @{code Bound} n), p)); fun term_of_fm T fs ps @{code T} = @{term True} | term_of_fm T fs ps @{code F} = @{term False} | term_of_fm T fs ps (@{code NOT} p) = @{term Not} $ term_of_fm T fs ps p - | term_of_fm T fs ps (@{code And} (p, q)) = @{term HOL.conj} $ term_of_fm T fs ps p $ term_of_fm T fs ps q - | term_of_fm T fs ps (@{code Or} (p, q)) = @{term HOL.disj} $ term_of_fm T fs ps p $ term_of_fm T fs ps q - | term_of_fm T fs ps (@{code Imp} (p, q)) = @{term HOL.implies} $ term_of_fm T fs ps p $ term_of_fm T fs ps q - | term_of_fm T fs ps (@{code Iff} (p, q)) = @{term HOL.iff} $ term_of_fm T fs ps p $ term_of_fm T fs ps q - | term_of_fm T fs ps (@{code Lt} p) = Const (@{const_name Orderings.less}, relT T) $ term_of_tm T fs ps p $ Const (@{const_name Groups.zero}, T) - | term_of_fm T fs ps (@{code Le} p) = Const (@{const_name Orderings.less_eq}, relT T) $ term_of_tm T fs ps p $ Const (@{const_name Groups.zero}, T) - | term_of_fm T fs ps (@{code Eq} p) = Const (@{const_name HOL.eq}, relT T) $ term_of_tm T fs ps p $ Const (@{const_name Groups.zero}, T) - | term_of_fm T fs ps (@{code NEq} p) = @{term Not} $ (Const (@{const_name HOL.eq}, relT T) $ term_of_tm T fs ps p $ Const (@{const_name Groups.zero}, T)) + | term_of_fm T fs ps (@{code And} (p, q)) = + @{term HOL.conj} $ term_of_fm T fs ps p $ term_of_fm T fs ps q + | term_of_fm T fs ps (@{code Or} (p, q)) = + @{term HOL.disj} $ term_of_fm T fs ps p $ term_of_fm T fs ps q + | term_of_fm T fs ps (@{code Imp} (p, q)) = + @{term HOL.implies} $ term_of_fm T fs ps p $ term_of_fm T fs ps q + | term_of_fm T fs ps (@{code Iff} (p, q)) = + @{term HOL.iff} $ term_of_fm T fs ps p $ term_of_fm T fs ps q + | term_of_fm T fs ps (@{code Lt} p) = + Const (@{const_name Orderings.less}, relT T) $ + term_of_tm T fs ps p $ Const (@{const_name Groups.zero}, T) + | term_of_fm T fs ps (@{code Le} p) = + Const (@{const_name Orderings.less_eq}, relT T) $ + term_of_tm T fs ps p $ Const (@{const_name Groups.zero}, T) + | term_of_fm T fs ps (@{code Eq} p) = + Const (@{const_name HOL.eq}, relT T) $ + term_of_tm T fs ps p $ Const (@{const_name Groups.zero}, T) + | term_of_fm T fs ps (@{code NEq} p) = + @{term Not} $ + (Const (@{const_name HOL.eq}, relT T) $ + term_of_tm T fs ps p $ Const (@{const_name Groups.zero}, T)) | term_of_fm T fs ps _ = error "term_of_fm: quantifiers"; fun frpar_procedure alternative T ps fm = @@ -3049,9 +4150,7 @@ val fs = subtract (op aconv) (map Free (Term.add_frees fm [])) ps; val eval = term_of_fm T fs ps o frpar o fm_of_term fs ps; val t = HOLogic.dest_Trueprop fm; - in - (HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, eval t) - end; + in HOLogic.mk_Trueprop (HOLogic.mk_eq (t, eval t)) end; in @@ -3070,21 +4169,21 @@ Object_Logic.full_atomize_tac ctxt THEN' CSUBGOAL (fn (g, i) => let - val th = frpar_oracle (ctxt, alternative, T, ps, g) + val th = frpar_oracle (ctxt, alternative, T, ps, g); in rtac (th RS iffD2) i end); fun method alternative = let - fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K () - val parsN = "pars" - val typN = "type" - val any_keyword = keyword parsN || keyword typN - val terms = Scan.repeat (Scan.unless any_keyword Args.term) - val typ = Scan.unless any_keyword Args.typ + fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K (); + val parsN = "pars"; + val typN = "type"; + val any_keyword = keyword parsN || keyword typN; + val terms = Scan.repeat (Scan.unless any_keyword Args.term); + val typ = Scan.unless any_keyword Args.typ; in (keyword typN |-- typ) -- (keyword parsN |-- terms) >> (fn (T, ps) => fn ctxt => SIMPLE_METHOD' (tactic ctxt alternative T ps)) - end + end; end; *} @@ -3097,19 +4196,19 @@ Parametric_Ferrante_Rackoff.method true *} "parametric QE for linear Arithmetic over fields, Version 2" -lemma "\(x::'a::{linordered_field_inverse_zero}). y \ -1 \ (y + 1)*x < 0" - apply (frpar type: "'a::{linordered_field_inverse_zero}" pars: "y::'a::{linordered_field_inverse_zero}") +lemma "\(x::'a::{linordered_field_inverse_zero}). y \ -1 \ (y + 1) * x < 0" + apply (frpar type: 'a pars: y) apply (simp add: field_simps) apply (rule spec[where x=y]) - apply (frpar type: "'a::{linordered_field_inverse_zero}" pars: "z::'a::{linordered_field_inverse_zero}") + apply (frpar type: 'a pars: "z::'a") apply simp done lemma "\(x::'a::{linordered_field_inverse_zero}). y \ -1 \ (y + 1)*x < 0" - apply (frpar2 type: "'a::{linordered_field_inverse_zero}" pars: "y::'a::{linordered_field_inverse_zero}") + apply (frpar2 type: 'a pars: y) apply (simp add: field_simps) apply (rule spec[where x=y]) - apply (frpar2 type: "'a::{linordered_field_inverse_zero}" pars: "z::'a::{linordered_field_inverse_zero}") + apply (frpar2 type: 'a pars: "z::'a") apply simp done