Theory HOL-Decision_Procs.Dense_Linear_Order
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)"
by (metis antisym_conv3 order.strict_trans)
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)"
by (metis antisym_conv3 order.strict_trans)
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)"
by (metis local.less_le_trans local.less_trans local.not_less)
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)"
by (metis local.le_less_trans local.nle_le not_le)
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"
using Mxne fMx fxM local.linear xMne by auto
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)"
using finite_set_intervals[where P="P", OF px lx xu linS uinS fS lS Su]
by (metis local.neq_le_trans)
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
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
using local.dual_order.strict_trans that(1) u xL xU by blast
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"
using fL local.Max_less_iff local.gt_ex by fastforce
lemma dlo_qe_nolb[no_atp]:
assumes ne: "U ≠ {}"
and fU: "finite U"
shows "(∃x. (∀y ∈ {}. y < x) ∧ (∀y ∈ U. x < y)) = True"
proof -
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 ?thesis
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
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'))"
by (metis ex1 ex2 local.max_less_iff_conj)
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'))"
by (metis ex1 ex2 local.max.strict_boundedE)
lemma pinf_ex[no_atp]:
assumes ex: "∃z. ∀x. z ⊏ x ⟶ (P x ⟷ P1)"
and p1: P1
shows "∃x. P x"
using ex local.gt_ex p1 by auto
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'))"
by (metis ex1 ex2 local.min_less_iff_conj)
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'))"
by (metis ex1 ex2 local.min_less_iff_conj)
lemma minf_ex[no_atp]:
assumes ex: "∃z. ∀x. x ⊏ z ⟶ (P x ⟷ P1)"
and p1: P1
shows "∃x. P x"
using ex local.lt_ex p1 by auto
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
obtain u 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 1 then show ?thesis
by (metis between_same)
next
case 2
then have t1t2: "t1 ⊏ t2"
by order
let ?u = "between t1 t2"
from between_less t1t2 have t1lu: "t1 ⊏ ?u" and ut2: "?u ⊏ t2" by auto
then show ?thesis
using "2" lin_dense px 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"?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
using local.gt_ex local.lt_ex mi pi that by blast
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 |> Simplifier.add_simps (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"
by (metis assms mult_less_0_iff mult_neg_neg zero_less_mult_pos)
lemma pos_prod_lt:
fixes c :: "'a::linordered_field"
assumes "c > 0"
shows "c * x < 0 ⟷ x < 0"
by (meson assms mult_less_0_iff order_less_imp_not_less)
lemma neg_prod_sum_lt:
fixes c :: "'a::linordered_field"
assumes "c < 0"
shows "c * x + t < 0 ⟷ x > (- 1 / c) * t"
using assms by (auto simp add: mult.commute divide_simps)
lemma pos_prod_sum_lt:
fixes c :: "'a::linordered_field"
assumes "c > 0"
shows "c * x + t < 0 ⟷ x < (- 1 / c) * t"
using assms by (auto simp add: mult.commute divide_simps)
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"
using assms linorder_not_less mult_le_0_iff by auto
lemma pos_prod_le:
fixes c :: "'a::linordered_field"
assumes "c > 0"
shows "c * x ≤ 0 ⟷ x ≤ 0"
using assms linorder_not_less mult_le_0_iff by auto
lemma neg_prod_sum_le:
fixes c :: "'a::linordered_field"
assumes "c < 0"
shows "c * x + t ≤ 0 ⟷ x ≥ (- 1 / c) * t"
using assms by (auto simp add: mult.commute divide_simps)
lemma pos_prod_sum_le:
fixes c :: "'a::linordered_field"
assumes "c > 0"
shows "c * x + t ≤ 0 ⟷ x ≤ (- 1 / c) * t"
using assms by (auto simp add: mult.commute divide_simps)
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"
using assms by (auto simp add: mult.commute divide_simps)
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