(* Title : HOL/Decision_Procs/Dense_Linear_Order.thy Author : Amine Chaieb, TU Muenchen *) section ‹Dense linear order without endpoints and a quantifier elimination procedure in Ferrante and Rackoff style› theory Dense_Linear_Order imports Main begin ML_file ‹langford_data.ML› ML_file ‹ferrante_rackoff_data.ML› context linorder begin lemma less_not_permute[no_atp]: "¬ (x < y ∧ y < x)" by (simp add: not_less linear) lemma gather_simps[no_atp]: "(∃x. (∀y ∈ L. y < x) ∧ (∀y ∈ U. x < y) ∧ x < u ∧ P x) ⟷ (∃x. (∀y ∈ L. y < x) ∧ (∀y ∈ (insert u U). x < y) ∧ P x)" "(∃x. (∀y ∈ L. y < x) ∧ (∀y ∈ U. x < y) ∧ l < x ∧ P x) ⟷ (∃x. (∀y ∈ (insert l L). y < x) ∧ (∀y ∈ U. x < y) ∧ P x)" "(∃x. (∀y ∈ L. y < x) ∧ (∀y ∈ U. x < y) ∧ x < u) ⟷ (∃x. (∀y ∈ L. y < x) ∧ (∀y ∈ (insert u U). x < y))" "(∃x. (∀y ∈ L. y < x) ∧ (∀y ∈ U. x < y) ∧ l < x) ⟷ (∃x. (∀y ∈ (insert l L). y < x) ∧ (∀y ∈ U. x < y))" by auto lemma gather_start [no_atp]: "(∃x. P x) ≡ (∃x. (∀y ∈ {}. y < x) ∧ (∀y∈ {}. x < y) ∧ P x)" by simp text‹Theorems for ‹∃z. ∀x. x < z ⟶ (P x ⟷ P⇩_{-}⇩_{∞})›› lemma minf_lt[no_atp]: "∃z . ∀x. x < z ⟶ (x < t ⟷ True)" by auto lemma minf_gt[no_atp]: "∃z . ∀x. x < z ⟶ (t < x ⟷ False)" by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le) lemma minf_le[no_atp]: "∃z. ∀x. x < z ⟶ (x ≤ t ⟷ True)" by (auto simp add: less_le) lemma minf_ge[no_atp]: "∃z. ∀x. x < z ⟶ (t ≤ x ⟷ False)" by (auto simp add: less_le not_less not_le) lemma minf_eq[no_atp]: "∃z. ∀x. x < z ⟶ (x = t ⟷ False)" by auto lemma minf_neq[no_atp]: "∃z. ∀x. x < z ⟶ (x ≠ t ⟷ True)" by auto lemma minf_P[no_atp]: "∃z. ∀x. x < z ⟶ (P ⟷ P)" by blast text‹Theorems for ‹∃z. ∀x. x < z ⟶ (P x ⟷ P⇩_{+}⇩_{∞})›› lemma pinf_gt[no_atp]: "∃z. ∀x. z < x ⟶ (t < x ⟷ True)" by auto lemma pinf_lt[no_atp]: "∃z. ∀x. z < x ⟶ (x < t ⟷ False)" by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le) lemma pinf_ge[no_atp]: "∃z. ∀x. z < x ⟶ (t ≤ x ⟷ True)" by (auto simp add: less_le) lemma pinf_le[no_atp]: "∃z. ∀x. z < x ⟶ (x ≤ t ⟷ False)" by (auto simp add: less_le not_less not_le) lemma pinf_eq[no_atp]: "∃z. ∀x. z < x ⟶ (x = t ⟷ False)" by auto lemma pinf_neq[no_atp]: "∃z. ∀x. z < x ⟶ (x ≠ t ⟷ True)" by auto lemma pinf_P[no_atp]: "∃z. ∀x. z < x ⟶ (P ⟷ P)" by blast lemma nmi_lt[no_atp]: "t ∈ U ⟹ ∀x. ¬True ∧ x < t ⟶ (∃u∈ U. u ≤ x)" by auto lemma nmi_gt[no_atp]: "t ∈ U ⟹ ∀x. ¬False ∧ t < x ⟶ (∃u∈ U. u ≤ x)" by (auto simp add: le_less) lemma nmi_le[no_atp]: "t ∈ U ⟹ ∀x. ¬True ∧ x≤ t ⟶ (∃u∈ U. u ≤ x)" by auto lemma nmi_ge[no_atp]: "t ∈ U ⟹ ∀x. ¬False ∧ t≤ x ⟶ (∃u∈ U. u ≤ x)" by auto lemma nmi_eq[no_atp]: "t ∈ U ⟹ ∀x. ¬False ∧ x = t ⟶ (∃u∈ U. u ≤ x)" by auto lemma nmi_neq[no_atp]: "t ∈ U ⟹∀x. ¬True ∧ x ≠ t ⟶ (∃u∈ U. u ≤ x)" by auto lemma nmi_P[no_atp]: "∀x. ~P ∧ P ⟶ (∃u∈ U. u ≤ x)" by auto lemma nmi_conj[no_atp]: "⟦∀x. ¬P1' ∧ P1 x ⟶ (∃u∈ U. u ≤ x) ; ∀x. ¬P2' ∧ P2 x ⟶ (∃u∈ U. u ≤ x)⟧ ⟹ ∀x. ¬(P1' ∧ P2') ∧ (P1 x ∧ P2 x) ⟶ (∃u∈ U. u ≤ x)" by auto lemma nmi_disj[no_atp]: "⟦∀x. ¬P1' ∧ P1 x ⟶ (∃u∈ U. u ≤ x) ; ∀x. ¬P2' ∧ P2 x ⟶ (∃u∈ U. u ≤ x)⟧ ⟹ ∀x. ¬(P1' ∨ P2') ∧ (P1 x ∨ P2 x) ⟶ (∃u∈ U. u ≤ x)" by auto lemma npi_lt[no_atp]: "t ∈ U ⟹ ∀x. ¬False ∧ x < t ⟶ (∃u∈ U. x ≤ u)" by (auto simp add: le_less) lemma npi_gt[no_atp]: "t ∈ U ⟹ ∀x. ¬True ∧ t < x ⟶ (∃u∈ U. x ≤ u)" by auto lemma npi_le[no_atp]: "t ∈ U ⟹ ∀x. ¬False ∧ x ≤ t ⟶ (∃u∈ U. x ≤ u)" by auto lemma npi_ge[no_atp]: "t ∈ U ⟹ ∀x. ¬True ∧ t ≤ x ⟶ (∃u∈ U. x ≤ u)" by auto lemma npi_eq[no_atp]: "t ∈ U ⟹ ∀x. ¬False ∧ x = t ⟶ (∃u∈ U. x ≤ u)" by auto lemma npi_neq[no_atp]: "t ∈ U ⟹ ∀x. ¬True ∧ x ≠ t ⟶ (∃u∈ U. x ≤ u )" by auto lemma npi_P[no_atp]: "∀x. ~P ∧ P ⟶ (∃u∈ U. x ≤ u)" by auto lemma npi_conj[no_atp]: "⟦∀x. ¬P1' ∧ P1 x ⟶ (∃u∈ U. x ≤ u) ; ∀x. ¬P2' ∧ P2 x ⟶ (∃u∈ U. x ≤ u)⟧ ⟹ ∀x. ¬(P1' ∧ P2') ∧ (P1 x ∧ P2 x) ⟶ (∃u∈ U. x ≤ u)" by auto lemma npi_disj[no_atp]: "⟦∀x. ¬P1' ∧ P1 x ⟶ (∃u∈ U. x ≤ u) ; ∀x. ¬P2' ∧ P2 x ⟶ (∃u∈ U. x ≤ u)⟧ ⟹ ∀x. ¬(P1' ∨ P2') ∧ (P1 x ∨ P2 x) ⟶ (∃u∈ U. x ≤ u)" by auto lemma lin_dense_lt[no_atp]: "t ∈ U ⟹ ∀x l u. (∀t. l < t ∧ t < u ⟶ t ∉ U) ∧ l < x ∧ x < u ∧ x < t ⟶ (∀y. l < y ∧ y < u ⟶ y < t)" proof clarsimp fix x l u y assume tU: "t ∈ U" and noU: "∀t. l < t ∧ t < u ⟶ t ∉ U" and lx: "l < x" and xu: "x < u" and px: "x < t" and ly: "l < y" and yu: "y < u" from tU noU ly yu have tny: "t ≠ y" by auto have False if H: "t < y" proof - from less_trans[OF lx px] less_trans[OF H yu] have "l < t ∧ t < u" by simp with tU noU show ?thesis by auto qed then have "¬ t < y" by auto then have "y ≤ t" by (simp add: not_less) then show "y < t" using tny by (simp add: less_le) qed lemma lin_dense_gt[no_atp]: "t ∈ U ⟹ ∀x l u. (∀t. l < t ∧ t < u ⟶ t ∉ U) ∧ l < x ∧ x < u ∧ t < x ⟶ (∀y. l < y ∧ y < u ⟶ t < y)" proof clarsimp fix x l u y assume tU: "t ∈ U" and noU: "∀t. l < t ∧ t < u ⟶ t ∉ U" and lx: "l < x" and xu: "x < u" and px: "t < x" and ly: "l < y" and yu: "y < u" from tU noU ly yu have tny: "t ≠ y" by auto have False if H: "y < t" proof - from less_trans[OF ly H] less_trans[OF px xu] have "l < t ∧ t < u" by simp with tU noU show ?thesis by auto qed then have "¬ y < t" by auto then have "t ≤ y" by (auto simp add: not_less) then show "t < y" using tny by (simp add: less_le) qed lemma lin_dense_le[no_atp]: "t ∈ U ⟹ ∀x l u. (∀t. l < t ∧ t < u ⟶ t ∉ U) ∧ l < x ∧ x < u ∧ x ≤ t ⟶ (∀y. l < y ∧ y < u ⟶ y ≤ t)" proof clarsimp fix x l u y assume tU: "t ∈ U" and noU: "∀t. l < t ∧ t < u ⟶ t ∉ U" and lx: "l < x" and xu: "x < u" and px: "x ≤ t" and ly: "l < y" and yu: "y < u" from tU noU ly yu have tny: "t ≠ y" by auto have False if H: "t < y" proof - from less_le_trans[OF lx px] less_trans[OF H yu] have "l < t ∧ t < u" by simp with tU noU show ?thesis by auto qed then have "¬ t < y" by auto then show "y ≤ t" by (simp add: not_less) qed lemma lin_dense_ge[no_atp]: "t ∈ U ⟹ ∀x l u. (∀t. l < t ∧ t < u ⟶ t ∉ U) ∧ l < x ∧ x < u ∧ t ≤ x ⟶ (∀y. l < y ∧ y < u ⟶ t ≤ y)" proof clarsimp fix x l u y assume tU: "t ∈ U" and noU: "∀t. l < t ∧ t < u ⟶ t ∉ U" and lx: "l < x" and xu: "x < u" and px: "t ≤ x" and ly: "l < y" and yu: "y < u" from tU noU ly yu have tny: "t ≠ y" by auto have False if H: "y < t" proof - from less_trans[OF ly H] le_less_trans[OF px xu] have "l < t ∧ t < u" by simp with tU noU show ?thesis by auto qed then have "¬ y < t" by auto then show "t ≤ y" by (simp add: not_less) qed lemma lin_dense_eq[no_atp]: "t ∈ U ⟹ ∀x l u. (∀t. l < t ∧ t < u ⟶ t ∉ U) ∧ l < x ∧ x < u ∧ x = t ⟶ (∀y. l < y ∧ y < u ⟶ y = t)" by auto lemma lin_dense_neq[no_atp]: "t ∈ U ⟹ ∀x l u. (∀t. l < t ∧ t < u ⟶ t ∉ U) ∧ l < x ∧ x < u ∧ x ≠ t ⟶ (∀y. l < y ∧ y < u ⟶ y ≠ t)" by auto lemma lin_dense_P[no_atp]: "∀x l u. (∀t. l < t ∧ t < u ⟶ t ∉ U) ∧ l < x ∧ x < u ∧ P ⟶ (∀y. l < y ∧ y < u ⟶ P)" by auto lemma lin_dense_conj[no_atp]: "⟦∀x l u. (∀t. l < t ∧ t < u ⟶ t ∉ U) ∧ l < x ∧ x < u ∧ P1 x ⟶ (∀y. l < y ∧ y < u ⟶ P1 y) ; ∀x l u. (∀t. l < t ∧ t < u ⟶ t ∉ U) ∧ l < x ∧ x < u ∧ P2 x ⟶ (∀y. l < y ∧ y < u ⟶ P2 y)⟧ ⟹ ∀x l u. (∀t. l < t ∧ t < u ⟶ t ∉ U) ∧ l < x ∧ x < u ∧ (P1 x ∧ P2 x) ⟶ (∀y. l < y ∧ y < u ⟶ (P1 y ∧ P2 y))" by blast lemma lin_dense_disj[no_atp]: "⟦∀x l u. (∀t. l < t ∧ t < u ⟶ t ∉ U) ∧ l < x ∧ x < u ∧ P1 x ⟶ (∀y. l < y ∧ y < u ⟶ P1 y) ; ∀x l u. (∀t. l < t ∧ t < u ⟶ t ∉ U) ∧ l < x ∧ x < u ∧ P2 x ⟶ (∀y. l < y ∧ y < u ⟶ P2 y)⟧ ⟹ ∀x l u. (∀t. l < t ∧ t < u ⟶ t ∉ U) ∧ l < x ∧ x < u ∧ (P1 x ∨ P2 x) ⟶ (∀y. l < y ∧ y < u ⟶ (P1 y ∨ P2 y))" by blast lemma npmibnd[no_atp]: "⟦∀x. ¬ MP ∧ P x ⟶ (∃u∈ U. u ≤ x); ∀x. ¬PP ∧ P x ⟶ (∃u∈ U. x ≤ u)⟧ ⟹ ∀x. ¬ MP ∧ ¬PP ∧ P x ⟶ (∃u∈ U. ∃u' ∈ U. u ≤ x ∧ x ≤ u')" by auto lemma finite_set_intervals[no_atp]: assumes px: "P x" and lx: "l ≤ x" and xu: "x ≤ u" and linS: "l∈ S" and uinS: "u ∈ S" and fS:"finite S" and lS: "∀x∈ S. l ≤ x" and Su: "∀x∈ S. x ≤ u" shows "∃a ∈ S. ∃b ∈ S. (∀y. a < y ∧ y < b ⟶ y ∉ S) ∧ a ≤ x ∧ x ≤ b ∧ P x" proof - let ?Mx = "{y. y∈ S ∧ y ≤ x}" let ?xM = "{y. y∈ S ∧ x ≤ y}" let ?a = "Max ?Mx" let ?b = "Min ?xM" have MxS: "?Mx ⊆ S" by blast then have fMx: "finite ?Mx" using fS finite_subset by auto from lx linS have linMx: "l ∈ ?Mx" by blast then have Mxne: "?Mx ≠ {}" by blast have xMS: "?xM ⊆ S" by blast then have fxM: "finite ?xM" using fS finite_subset by auto from xu uinS have linxM: "u ∈ ?xM" by blast then have xMne: "?xM ≠ {}" by blast have ax: "?a ≤ x" using Mxne fMx by auto have xb: "x ≤ ?b" using xMne fxM by auto have "?a ∈ ?Mx" using Max_in[OF fMx Mxne] by simp then have ainS: "?a ∈ S" using MxS by blast have "?b ∈ ?xM" using Min_in[OF fxM xMne] by simp then have binS: "?b ∈ S" using xMS by blast have noy: "∀y. ?a < y ∧ y < ?b ⟶ y ∉ S" proof clarsimp fix y assume ay: "?a < y" and yb: "y < ?b" and yS: "y ∈ S" from yS have "y ∈ ?Mx ∨ y ∈ ?xM" by (auto simp add: linear) then show False proof assume "y ∈ ?Mx" then have "y ≤ ?a" using Mxne fMx by auto with ay show ?thesis by (simp add: not_le[symmetric]) next assume "y ∈ ?xM" then have "?b ≤ y" using xMne fxM by auto with yb show ?thesis by (simp add: not_le[symmetric]) qed qed from ainS binS noy ax xb px show ?thesis by blast qed lemma finite_set_intervals2[no_atp]: assumes px: "P x" and lx: "l ≤ x" and xu: "x ≤ u" and linS: "l∈ S" and uinS: "u ∈ S" and fS: "finite S" and lS: "∀x∈ S. l ≤ x" and Su: "∀x∈ S. x ≤ u" shows "(∃s∈ S. P s) ∨ (∃a ∈ S. ∃b ∈ S. (∀y. a < y ∧ y < b ⟶ y ∉ S) ∧ a < x ∧ x < b ∧ P x)" proof - from finite_set_intervals[where P="P", OF px lx xu linS uinS fS lS Su] obtain a and b where as: "a ∈ S" and bs: "b ∈ S" and noS: "∀y. a < y ∧ y < b ⟶ y ∉ S" and axb: "a ≤ x ∧ x ≤ b ∧ P x" by auto from axb have "x = a ∨ x = b ∨ (a < x ∧ x < b)" by (auto simp add: le_less) then show ?thesis using px as bs noS by blast qed end section ‹The classical QE after Langford for dense linear orders› context unbounded_dense_linorder begin lemma interval_empty_iff: "{y. x < y ∧ y < z} = {} ⟷ ¬ x < z" by (auto dest: dense) lemma dlo_qe_bnds[no_atp]: assumes ne: "L ≠ {}" and neU: "U ≠ {}" and fL: "finite L" and fU: "finite U" shows "(∃x. (∀y ∈ L. y < x) ∧ (∀y ∈ U. x < y)) ≡ (∀l ∈ L. ∀u ∈ U. l < u)" proof (simp only: atomize_eq, rule iffI) assume H: "∃x. (∀y∈L. y < x) ∧ (∀y∈U. x < y)" then obtain x where xL: "∀y∈L. y < x" and xU: "∀y∈U. x < y" by blast have "l < u" if l: "l ∈ L" and u: "u ∈ U" for l u proof - have "l < x" using xL l by blast also have "x < u" using xU u by blast finally show ?thesis . qed then show "∀l∈L. ∀u∈U. l < u" by blast next assume H: "∀l∈L. ∀u∈U. l < u" let ?ML = "Max L" let ?MU = "Min U" from fL ne have th1: "?ML ∈ L" and th1': "∀l∈L. l ≤ ?ML" by auto from fU neU have th2: "?MU ∈ U" and th2': "∀u∈U. ?MU ≤ u" by auto from th1 th2 H have "?ML < ?MU" by auto with dense obtain w where th3: "?ML < w" and th4: "w < ?MU" by blast from th3 th1' have "∀l ∈ L. l < w" by auto moreover from th4 th2' have "∀u ∈ U. w < u" by auto ultimately show "∃x. (∀y∈L. y < x) ∧ (∀y∈U. x < y)" by auto qed lemma dlo_qe_noub[no_atp]: assumes ne: "L ≠ {}" and fL: "finite L" shows "(∃x. (∀y ∈ L. y < x) ∧ (∀y ∈ {}. x < y)) ≡ True" proof (simp add: atomize_eq) from gt_ex[of "Max L"] obtain M where M: "Max L < M" by blast from ne fL have "∀x ∈ L. x ≤ Max L" by simp with M have "∀x∈L. x < M" by (auto intro: le_less_trans) then show "∃x. ∀y∈L. y < x" by blast qed lemma dlo_qe_nolb[no_atp]: assumes ne: "U ≠ {}" and fU: "finite U" shows "(∃x. (∀y ∈ {}. y < x) ∧ (∀y ∈ U. x < y)) ≡ True" proof (simp add: atomize_eq) from lt_ex[of "Min U"] obtain M where M: "M < Min U" by blast from ne fU have "∀x ∈ U. Min U ≤ x" by simp with M have "∀x∈U. M < x" by (auto intro: less_le_trans) then show "∃x. ∀y∈U. x < y" by blast qed lemma exists_neq[no_atp]: "∃(x::'a). x ≠ t" "∃(x::'a). t ≠ x" using gt_ex[of t] by auto lemmas dlo_simps[no_atp] = order_refl less_irrefl not_less not_le exists_neq le_less neq_iff linear less_not_permute lemma axiom[no_atp]: "class.unbounded_dense_linorder (≤) (<)" by (rule unbounded_dense_linorder_axioms) lemma atoms[no_atp]: shows "TERM (less :: 'a ⇒ _)" and "TERM (less_eq :: 'a ⇒ _)" and "TERM ((=) :: 'a ⇒ _)" . declare axiom[langford qe: dlo_qe_bnds dlo_qe_nolb dlo_qe_noub gather: gather_start gather_simps atoms: atoms] declare dlo_simps[langfordsimp] end (* FIXME: Move to HOL -- together with the conj_aci_rule in langford.ML *) lemmas dnf[no_atp] = conj_disj_distribL conj_disj_distribR lemmas weak_dnf_simps[no_atp] = simp_thms dnf lemma nnf_simps[no_atp]: "(¬ (P ∧ Q)) ⟷ (¬ P ∨ ¬ Q)" "(¬ (P ∨ Q)) ⟷ (¬ P ∧ ¬ Q)" "(P ⟶ Q) ⟷ (¬ P ∨ Q)" "(P ⟷ Q) ⟷ ((P ∧ Q) ∨ (¬ P ∧ ¬ Q))" "(¬ ¬ P) ⟷ P" by blast+ lemma ex_distrib[no_atp]: "(∃x. P x ∨ Q x) ⟷ ((∃x. P x) ∨ (∃x. Q x))" by blast lemmas dnf_simps[no_atp] = weak_dnf_simps nnf_simps ex_distrib ML_file ‹langford.ML› method_setup dlo = ‹ Scan.succeed (SIMPLE_METHOD' o Langford.dlo_tac) › "Langford's algorithm for quantifier elimination in dense linear orders" section ‹Contructive dense linear orders yield QE for linear arithmetic over ordered Fields› text ‹Linear order without upper bounds› locale linorder_stupid_syntax = linorder begin notation less_eq ("'(⊑')") and less_eq ("(_/ ⊑ _)" [51, 51] 50) and less ("'(⊏')") and less ("(_/ ⊏ _)" [51, 51] 50) end locale linorder_no_ub = linorder_stupid_syntax + assumes gt_ex: "∃y. less x y" begin lemma ge_ex[no_atp]: "∃y. x ⊑ y" using gt_ex by auto text ‹Theorems for ‹∃z. ∀x. z ⊏ x ⟶ (P x ⟷ P⇩_{+}⇩_{∞})›› lemma pinf_conj[no_atp]: assumes ex1: "∃z1. ∀x. z1 ⊏ x ⟶ (P1 x ⟷ P1')" and ex2: "∃z2. ∀x. z2 ⊏ x ⟶ (P2 x ⟷ P2')" shows "∃z. ∀x. z ⊏ x ⟶ ((P1 x ∧ P2 x) ⟷ (P1' ∧ P2'))" proof - from ex1 ex2 obtain z1 and z2 where z1: "∀x. z1 ⊏ x ⟶ (P1 x ⟷ P1')" and z2: "∀x. z2 ⊏ x ⟶ (P2 x ⟷ P2')" by blast from gt_ex obtain z where z:"ord.max less_eq z1 z2 ⊏ z" by blast from z have zz1: "z1 ⊏ z" and zz2: "z2 ⊏ z" by simp_all have "(P1 x ∧ P2 x) ⟷ (P1' ∧ P2')" if H: "z ⊏ x" for x using less_trans[OF zz1 H] less_trans[OF zz2 H] z1 zz1 z2 zz2 by auto then show ?thesis by blast qed lemma pinf_disj[no_atp]: assumes ex1: "∃z1. ∀x. z1 ⊏ x ⟶ (P1 x ⟷ P1')" and ex2: "∃z2. ∀x. z2 ⊏ x ⟶ (P2 x ⟷ P2')" shows "∃z. ∀x. z ⊏ x ⟶ ((P1 x ∨ P2 x) ⟷ (P1' ∨ P2'))" proof- from ex1 ex2 obtain z1 and z2 where z1: "∀x. z1 ⊏ x ⟶ (P1 x ⟷ P1')" and z2: "∀x. z2 ⊏ x ⟶ (P2 x ⟷ P2')" by blast from gt_ex obtain z where z: "ord.max less_eq z1 z2 ⊏ z" by blast from z have zz1: "z1 ⊏ z" and zz2: "z2 ⊏ z" by simp_all have "(P1 x ∨ P2 x) ⟷ (P1' ∨ P2')" if H: "z ⊏ x" for x using less_trans[OF zz1 H] less_trans[OF zz2 H] z1 zz1 z2 zz2 by auto then show ?thesis by blast qed lemma pinf_ex[no_atp]: assumes ex: "∃z. ∀x. z ⊏ x ⟶ (P x ⟷ P1)" and p1: P1 shows "∃x. P x" proof - from ex obtain z where z: "∀x. z ⊏ x ⟶ (P x ⟷ P1)" by blast from gt_ex obtain x where x: "z ⊏ x" by blast from z x p1 show ?thesis by blast qed end text ‹Linear order without upper bounds› locale linorder_no_lb = linorder_stupid_syntax + assumes lt_ex: "∃y. less y x" begin lemma le_ex[no_atp]: "∃y. y ⊑ x" using lt_ex by auto text ‹Theorems for ‹∃z. ∀x. x ⊏ z ⟶ (P x ⟷ P⇩_{-}⇩_{∞})›› lemma minf_conj[no_atp]: assumes ex1: "∃z1. ∀x. x ⊏ z1 ⟶ (P1 x ⟷ P1')" and ex2: "∃z2. ∀x. x ⊏ z2 ⟶ (P2 x ⟷ P2')" shows "∃z. ∀x. x ⊏ z ⟶ ((P1 x ∧ P2 x) ⟷ (P1' ∧ P2'))" proof - from ex1 ex2 obtain z1 and z2 where z1: "∀x. x ⊏ z1 ⟶ (P1 x ⟷ P1')" and z2: "∀x. x ⊏ z2 ⟶ (P2 x ⟷ P2')" by blast from lt_ex obtain z where z: "z ⊏ ord.min less_eq z1 z2" by blast from z have zz1: "z ⊏ z1" and zz2: "z ⊏ z2" by simp_all have "(P1 x ∧ P2 x) ⟷ (P1' ∧ P2')" if H: "x ⊏ z" for x using less_trans[OF H zz1] less_trans[OF H zz2] z1 zz1 z2 zz2 by auto then show ?thesis by blast qed lemma minf_disj[no_atp]: assumes ex1: "∃z1. ∀x. x ⊏ z1 ⟶ (P1 x ⟷ P1')" and ex2: "∃z2. ∀x. x ⊏ z2 ⟶ (P2 x ⟷ P2')" shows "∃z. ∀x. x ⊏ z ⟶ ((P1 x ∨ P2 x) ⟷ (P1' ∨ P2'))" proof - from ex1 ex2 obtain z1 and z2 where z1: "∀x. x ⊏ z1 ⟶ (P1 x ⟷ P1')" and z2: "∀x. x ⊏ z2 ⟶ (P2 x ⟷ P2')" by blast from lt_ex obtain z where z: "z ⊏ ord.min less_eq z1 z2" by blast from z have zz1: "z ⊏ z1" and zz2: "z ⊏ z2" by simp_all have "(P1 x ∨ P2 x) ⟷ (P1' ∨ P2')" if H: "x ⊏ z" for x using less_trans[OF H zz1] less_trans[OF H zz2] z1 zz1 z2 zz2 by auto then show ?thesis by blast qed lemma minf_ex[no_atp]: assumes ex: "∃z. ∀x. x ⊏ z ⟶ (P x ⟷ P1)" and p1: P1 shows "∃x. P x" proof - from ex obtain z where z: "∀x. x ⊏ z ⟶ (P x ⟷ P1)" by blast from lt_ex obtain x where x: "x ⊏ z" by blast from z x p1 show ?thesis by blast qed end locale constr_dense_linorder = linorder_no_lb + linorder_no_ub + fixes between assumes between_less: "less x y ⟹ less x (between x y) ∧ less (between x y) y" and between_same: "between x x = x" begin sublocale dlo: unbounded_dense_linorder proof (unfold_locales, goal_cases) case (1 x y) then show ?case using between_less [of x y] by auto next case 2 then show ?case by (rule lt_ex) next case 3 then show ?case by (rule gt_ex) qed lemma rinf_U[no_atp]: assumes fU: "finite U" and lin_dense: "∀x l u. (∀t. l ⊏ t ∧ t⊏ u ⟶ t ∉ U) ∧ l⊏ x ∧ x ⊏ u ∧ P x ⟶ (∀y. l ⊏ y ∧ y ⊏ u ⟶ P y )" and nmpiU: "∀x. ¬ MP ∧ ¬PP ∧ P x ⟶ (∃u∈ U. ∃u' ∈ U. u ⊑ x ∧ x ⊑ u')" and nmi: "¬ MP" and npi: "¬ PP" and ex: "∃x. P x" shows "∃u∈ U. ∃u' ∈ U. P (between u u')" proof - from ex obtain x where px: "P x" by blast from px nmi npi nmpiU have "∃u∈ U. ∃u' ∈ U. u ⊑ x ∧ x ⊑ u'" by auto then obtain u and u' where uU: "u∈ U" and uU': "u' ∈ U" and ux: "u ⊑ x" and xu': "x ⊑ u'" by auto from uU have Une: "U ≠ {}" by auto let ?l = "linorder.Min less_eq U" let ?u = "linorder.Max less_eq U" have linM: "?l ∈ U" using fU Une by simp have uinM: "?u ∈ U" using fU Une by simp have lM: "∀t∈ U. ?l ⊑ t" using Une fU by auto have Mu: "∀t∈ U. t ⊑ ?u" using Une fU by auto have th: "?l ⊑ u" using uU Une lM by auto from order_trans[OF th ux] have lx: "?l ⊑ x" . have th: "u' ⊑ ?u" using uU' Une Mu by simp from order_trans[OF xu' th] have xu: "x ⊑ ?u" . from finite_set_intervals2[where P="P",OF px lx xu linM uinM fU lM Mu] consider u where "u ∈ U" "P u" | t1 t2 where "t1 ∈ U" "t2 ∈ U" "∀y. t1 ⊏ y ∧ y ⊏ t2 ⟶ y ∉ U" "t1 ⊏ x" "x ⊏ t2" "P x" by blast then show ?thesis proof cases case u: 1 have "between u u = u" by (simp add: between_same) with u have "P (between u u)" by simp with u show ?thesis by blast next case 2 note t1M = ‹t1 ∈ U› and t2M = ‹t2∈ U› and noM = ‹∀y. t1 ⊏ y ∧ y ⊏ t2 ⟶ y ∉ U› and t1x = ‹t1 ⊏ x› and xt2 = ‹x ⊏ t2› and px = ‹P x› from less_trans[OF t1x xt2] have t1t2: "t1 ⊏ t2" . let ?u = "between t1 t2" from between_less t1t2 have t1lu: "t1 ⊏ ?u" and ut2: "?u ⊏ t2" by auto from lin_dense noM t1x xt2 px t1lu ut2 have "P ?u" by blast with t1M t2M show ?thesis by blast qed qed theorem fr_eq[no_atp]: assumes fU: "finite U" and lin_dense: "∀x l u. (∀t. l ⊏ t ∧ t⊏ u ⟶ t ∉ U) ∧ l⊏ x ∧ x ⊏ u ∧ P x ⟶ (∀y. l ⊏ y ∧ y ⊏ u ⟶ P y )" and nmibnd: "∀x. ¬ MP ∧ P x ⟶ (∃u∈ U. u ⊑ x)" and npibnd: "∀x. ¬PP ∧ P x ⟶ (∃u∈ U. x ⊑ u)" and mi: "∃z. ∀x. x ⊏ z ⟶ (P x = MP)" and pi: "∃z. ∀x. z ⊏ x ⟶ (P x = PP)" shows "(∃x. P x) ≡ (MP ∨ PP ∨ (∃u ∈ U. ∃u'∈ U. P (between u u')))" (is "_ ≡ (_ ∨ _ ∨ ?F)" is "?E ≡ ?D") proof - have "?E ⟷ ?D" proof show ?D if px: ?E proof - consider "MP ∨ PP" | "¬ MP" "¬ PP" by blast then show ?thesis proof cases case 1 then show ?thesis by blast next case 2 from npmibnd[OF nmibnd npibnd] have nmpiU: "∀x. ¬ MP ∧ ¬PP ∧ P x ⟶ (∃u∈ U. ∃u' ∈ U. u ⊑ x ∧ x ⊑ u')" . from rinf_U[OF fU lin_dense nmpiU ‹¬ MP› ‹¬ PP› px] show ?thesis by blast qed qed show ?E if ?D proof - from that consider MP | PP | ?F by blast then show ?thesis proof cases case 1 from minf_ex[OF mi this] show ?thesis . next case 2 from pinf_ex[OF pi this] show ?thesis . next case 3 then show ?thesis by blast qed qed qed then show "?E ≡ ?D" by simp qed lemmas minf_thms[no_atp] = minf_conj minf_disj minf_eq minf_neq minf_lt minf_le minf_gt minf_ge minf_P lemmas pinf_thms[no_atp] = pinf_conj pinf_disj pinf_eq pinf_neq pinf_lt pinf_le pinf_gt pinf_ge pinf_P lemmas nmi_thms[no_atp] = nmi_conj nmi_disj nmi_eq nmi_neq nmi_lt nmi_le nmi_gt nmi_ge nmi_P lemmas npi_thms[no_atp] = npi_conj npi_disj npi_eq npi_neq npi_lt npi_le npi_gt npi_ge npi_P lemmas lin_dense_thms[no_atp] = lin_dense_conj lin_dense_disj lin_dense_eq lin_dense_neq lin_dense_lt lin_dense_le lin_dense_gt lin_dense_ge lin_dense_P lemma ferrack_axiom[no_atp]: "constr_dense_linorder less_eq less between" by (rule constr_dense_linorder_axioms) lemma atoms[no_atp]: shows "TERM (less :: 'a ⇒ _)" and "TERM (less_eq :: 'a ⇒ _)" and "TERM ((=) :: 'a ⇒ _)" . declare ferrack_axiom [ferrack minf: minf_thms pinf: pinf_thms nmi: nmi_thms npi: npi_thms lindense: lin_dense_thms qe: fr_eq atoms: atoms] declaration ‹ let fun simps phi = map (Morphism.thm phi) [@{thm "not_less"}, @{thm "not_le"}] fun generic_whatis phi = let val [lt, le] = map (Morphism.term phi) [\<^term>‹(⊏)›, \<^term>‹(⊑)›] fun h x t = case Thm.term_of t of \<^Const_>‹HOL.eq _ for y z› => if Thm.term_of x aconv y then Ferrante_Rackoff_Data.Eq else Ferrante_Rackoff_Data.Nox | \<^Const_>‹Not for \<^Const>‹HOL.eq _ for y z›› => if Thm.term_of x aconv y then Ferrante_Rackoff_Data.NEq else Ferrante_Rackoff_Data.Nox | b$y$z => if Term.could_unify (b, lt) then if Thm.term_of x aconv y then Ferrante_Rackoff_Data.Lt else if Thm.term_of x aconv z then Ferrante_Rackoff_Data.Gt else Ferrante_Rackoff_Data.Nox else if Term.could_unify (b, le) then if Thm.term_of x aconv y then Ferrante_Rackoff_Data.Le else if Thm.term_of x aconv z then Ferrante_Rackoff_Data.Ge else Ferrante_Rackoff_Data.Nox else Ferrante_Rackoff_Data.Nox | _ => Ferrante_Rackoff_Data.Nox in h end fun ss phi ctxt = simpset_of (put_simpset HOL_ss ctxt addsimps (simps phi)) in Ferrante_Rackoff_Data.funs @{thm "ferrack_axiom"} {isolate_conv = K (K (K Thm.reflexive)), whatis = generic_whatis, simpset = ss} end › end ML_file ‹ferrante_rackoff.ML› method_setup ferrack = ‹ Scan.succeed (SIMPLE_METHOD' o FerranteRackoff.dlo_tac) › "Ferrante and Rackoff's algorithm for quantifier elimination in dense linear orders" subsection ‹Ferrante and Rackoff algorithm over ordered fields› lemma neg_prod_lt: fixes c :: "'a::linordered_field" assumes "c < 0" shows "c * x < 0 ≡ x > 0" proof - have "c * x < 0 ⟷ 0 / c < x" by (simp only: neg_divide_less_eq[OF ‹c < 0›] algebra_simps) also have "… ⟷ 0 < x" by simp finally show "PROP ?thesis" by simp qed lemma pos_prod_lt: fixes c :: "'a::linordered_field" assumes "c > 0" shows "c * x < 0 ≡ x < 0" proof - have "c * x < 0 ⟷ 0 /c > x" by (simp only: pos_less_divide_eq[OF ‹c > 0›] algebra_simps) also have "… ⟷ 0 > x" by simp finally show "PROP ?thesis" by simp qed lemma neg_prod_sum_lt: fixes c :: "'a::linordered_field" assumes "c < 0" shows "c * x + t < 0 ≡ x > (- 1 / c) * t" proof - have "c * x + t < 0 ⟷ c * x < - t" by (subst less_iff_diff_less_0 [of "c * x" "- t"]) simp also have "… ⟷ - t / c < x" by (simp only: neg_divide_less_eq[OF ‹c < 0›] algebra_simps) also have "… ⟷ (- 1 / c) * t < x" by simp finally show "PROP ?thesis" by simp qed lemma pos_prod_sum_lt: fixes c :: "'a::linordered_field" assumes "c > 0" shows "c * x + t < 0 ≡ x < (- 1 / c) * t" proof - have "c * x + t < 0 ⟷ c * x < - t" by (subst less_iff_diff_less_0 [of "c * x" "- t"]) simp also have "… ⟷ - t / c > x" by (simp only: pos_less_divide_eq[OF ‹c > 0›] algebra_simps) also have "… ⟷ (- 1 / c) * t > x" by simp finally show "PROP ?thesis" by simp qed lemma sum_lt: fixes x :: "'a::ordered_ab_group_add" shows "x + t < 0 ≡ x < - t" using less_diff_eq[where a= x and b=t and c=0] by simp lemma neg_prod_le: fixes c :: "'a::linordered_field" assumes "c < 0" shows "c * x ≤ 0 ≡ x ≥ 0" proof - have "c * x ≤ 0 ⟷ 0 / c ≤ x" by (simp only: neg_divide_le_eq[OF ‹c < 0›] algebra_simps) also have "… ⟷ 0 ≤ x" by simp finally show "PROP ?thesis" by simp qed lemma pos_prod_le: fixes c :: "'a::linordered_field" assumes "c > 0" shows "c * x ≤ 0 ≡ x ≤ 0" proof - have "c * x ≤ 0 ⟷ 0 / c ≥ x" by (simp only: pos_le_divide_eq[OF ‹c > 0›] algebra_simps) also have "… ⟷ 0 ≥ x" by simp finally show "PROP ?thesis" by simp qed lemma neg_prod_sum_le: fixes c :: "'a::linordered_field" assumes "c < 0" shows "c * x + t ≤ 0 ≡ x ≥ (- 1 / c) * t" proof - have "c * x + t ≤ 0 ⟷ c * x ≤ -t" by (subst le_iff_diff_le_0 [of "c*x" "-t"]) simp also have "… ⟷ - t / c ≤ x" by (simp only: neg_divide_le_eq[OF ‹c < 0›] algebra_simps) also have "… ⟷ (- 1 / c) * t ≤ x" by simp finally show "PROP ?thesis" by simp qed lemma pos_prod_sum_le: fixes c :: "'a::linordered_field" assumes "c > 0" shows "c * x + t ≤ 0 ≡ x ≤ (- 1 / c) * t" proof - have "c * x + t ≤ 0 ⟷ c * x ≤ - t" by (subst le_iff_diff_le_0 [of "c*x" "-t"]) simp also have "… ⟷ - t / c ≥ x" by (simp only: pos_le_divide_eq[OF ‹c > 0›] algebra_simps) also have "… ⟷ (- 1 / c) * t ≥ x" by simp finally show "PROP ?thesis" by simp qed lemma sum_le: fixes x :: "'a::ordered_ab_group_add" shows "x + t ≤ 0 ≡ x ≤ - t" using le_diff_eq[where a= x and b=t and c=0] by simp lemma nz_prod_eq: fixes c :: "'a::linordered_field" assumes "c ≠ 0" shows "c * x = 0 ≡ x = 0" using assms by simp lemma nz_prod_sum_eq: fixes c :: "'a::linordered_field" assumes "c ≠ 0" shows "c * x + t = 0 ≡ x = (- 1/c) * t" proof - have "c * x + t = 0 ⟷ c * x = - t" by (subst eq_iff_diff_eq_0 [of "c*x" "-t"]) simp also have "… ⟷ x = - t / c" by (simp only: nonzero_eq_divide_eq[OF ‹c ≠ 0›] algebra_simps) finally show "PROP ?thesis" by simp qed lemma sum_eq: fixes x :: "'a::ordered_ab_group_add" shows "x + t = 0 ≡ x = - t" using eq_diff_eq[where a= x and b=t and c=0] by simp