Theory Dense_Linear_Order

(*  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)"

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)"

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)"

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)"
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"
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"
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"
then show False
proof
assume "y  ?Mx"
then have "y  ?a"
using Mxne fMx by auto
with ay show ?thesis
next
assume "y  ?xM"
then have "?b  y"
using xMne fxM by auto
with yb show ?thesis
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)"
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. (yL. y < x)  (yU. x < y)"
then obtain x where xL: "yL. y < x" and xU: "yU. 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 "lL. uU. l < u" by blast
next
assume H: "lL. uU. l < u"
let ?ML = "Max L"
let ?MU = "Min U"
from fL ne have th1: "?ML  L" and th1': "lL. l  ?ML"
by auto
from fU neU have th2: "?MU  U" and th2': "uU. ?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. (yL. y < x)  (yU. 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"
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 "xL. x < M"
by (auto intro: le_less_trans)
then show "x. yL. 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"
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 "xU. M < x"
by (auto intro: less_le_trans)
then show "x. yU. 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]:
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 ConstHOL.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:
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 "cx" "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 "cx" "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:
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 "cx" "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:
shows "x + t = 0  x = - t"
using eq_diff_eq[where a= x and b=t and c=0] by simp

interpretation class_dense_linordered_field: constr_dense_linorder
"(≤)" "(<)" "λx y. 1/2 * ((x::'a::linordered_field) + y)"
by unfold_locales (dlo, dlo, auto)

declaration let
fun earlier [] _ = false
| earlier (h::t) (x, y) =
if h aconvc y then false else if h aconvc x then true else earlier t (x, y);

fun earlier_ord vs (x, y) =
if x aconvc y then EQUAL
else if earlier vs (x, y) then LESS
else GREATER;

fun dest_frac ct =
case Thm.term_of ct of
Const_Rings.divide _ for a b =>
Rat.make (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
| Const_inverse _ for a => Rat.make(1, HOLogic.dest_number a |> snd)
| t => Rat.of_int (snd (HOLogic.dest_number t))

fun whatis x ct = case Thm.term_of ct of
Const_plus _ for Const_times _ for _ y _ =>
if y aconv Thm.term_of x then ("c*x+t",[(funpow 2 Thm.dest_arg1) ct, Thm.dest_arg ct])
else ("Nox",[])
| Const_plus _ for y _ =>
if y aconv Thm.term_of x then ("x+t",[Thm.dest_arg ct])
else ("Nox",[])
| Const_times _ for _ y =>
if y aconv Thm.term_of x then ("c*x",[Thm.dest_arg1 ct])
else ("Nox",[])
| t => if t aconv Thm.term_of x then ("x",[]) else ("Nox",[]);

fun xnormalize_conv ctxt [] ct = Thm.reflexive ct
| xnormalize_conv ctxt (vs as (x::_)) ct =
case Thm.term_of ct of
Const_less _ for _ Const_zero_class.zero _ =>
(case whatis x (Thm.dest_arg1 ct) of
("c*x+t",[c,t]) =>
let
val cr = dest_frac c
val clt = Thm.dest_fun2 ct
val cz = Thm.dest_arg ct
val neg = cr < @0
val cthp = Simplifier.rewrite ctxt
(Thm.apply ctermTrueprop
(if neg then Thm.apply (Thm.apply clt c) cz
else Thm.apply (Thm.apply clt cz) c))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
val th = Thm.implies_elim (Thm.instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x,t])
(if neg then @{thm neg_prod_sum_lt} else @{thm pos_prod_sum_lt})) cth
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
(Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier_ord vs)))) th
in rth end
| ("x+t",[t]) =>
let
val T = Thm.ctyp_of_cterm x
val th = Thm.instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_lt"}
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
(Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier_ord vs)))) th
in  rth end
| ("c*x",[c]) =>
let
val cr = dest_frac c
val clt = Thm.dest_fun2 ct
val cz = Thm.dest_arg ct
val neg = cr < @0
val cthp = Simplifier.rewrite ctxt
(Thm.apply ctermTrueprop
(if neg then Thm.apply (Thm.apply clt c) cz
else Thm.apply (Thm.apply clt cz) c))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
val th = Thm.implies_elim (Thm.instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x])
(if neg then @{thm neg_prod_lt} else @{thm pos_prod_lt})) cth
val rth = th
in rth end
| _ => Thm.reflexive ct)

|  Const_less_eq _ for _ Const_zero_class.zero _ =>
(case whatis x (Thm.dest_arg1 ct) of
("c*x+t",[c,t]) =>
let
val T = Thm.typ_of_cterm x
val cT = Thm.ctyp_of_cterm x
val cr = dest_frac c
val clt = Thm.cterm_of ctxt Constless T
val cz = Thm.dest_arg ct
val neg = cr < @0
val cthp = Simplifier.rewrite ctxt
(Thm.apply ctermTrueprop
(if neg then Thm.apply (Thm.apply clt c) cz
else Thm.apply (Thm.apply clt cz) c))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
val th = Thm.implies_elim (Thm.instantiate' [SOME cT] (map SOME [c,x,t])
(if neg then @{thm neg_prod_sum_le} else @{thm pos_prod_sum_le})) cth
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
(Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier_ord vs)))) th
in rth end
| ("x+t",[t]) =>
let
val T = Thm.ctyp_of_cterm x
val th = Thm.instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_le"}
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
(Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier_ord vs)))) th
in  rth end
| ("c*x",[c]) =>
let
val T = Thm.typ_of_cterm x
val cT = Thm.ctyp_of_cterm x
val cr = dest_frac c
val clt = Thm.cterm_of ctxt Constless T
val cz = Thm.dest_arg ct
val neg = cr < @0
val cthp = Simplifier.rewrite ctxt
(Thm.apply ctermTrueprop
(if neg then Thm.apply (Thm.apply clt c) cz
else Thm.apply (Thm.apply clt cz) c))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
val th = Thm.implies_elim (Thm.instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x])
(if neg then @{thm neg_prod_le} else @{thm pos_prod_le})) cth
val rth = th
in rth end
| _ => Thm.reflexive ct)

|  Const_HOL.eq _ for _ Const_zero_class.zero _ =>
(case whatis x (Thm.dest_arg1 ct) of
("c*x+t",[c,t]) =>
let
val T = Thm.ctyp_of_cterm x
val cr = dest_frac c
val ceq = Thm.dest_fun2 ct
val cz = Thm.dest_arg ct
val cthp = Simplifier.rewrite ctxt
(Thm.apply ctermTrueprop
(Thm.apply ctermNot (Thm.apply (Thm.apply ceq c) cz)))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
val th = Thm.implies_elim
(Thm.instantiate' [SOME T] (map SOME [c,x,t]) @{thm nz_prod_sum_eq}) cth
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
(Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier_ord vs)))) th
in rth end
| ("x+t",[t]) =>
let
val T = Thm.ctyp_of_cterm x
val th = Thm.instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_eq"}
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
(Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier_ord vs)))) th
in  rth end
| ("c*x",[c]) =>
let
val T = Thm.ctyp_of_cterm x
val cr = dest_frac c
val ceq = Thm.dest_fun2 ct
val cz = Thm.dest_arg ct
val cthp = Simplifier.rewrite ctxt
(Thm.apply ctermTrueprop
(Thm.apply ctermNot (Thm.apply (Thm.apply ceq c) cz)))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
val rth = Thm.implies_elim
(Thm.instantiate' [SOME T] (map SOME [c,x]) @{thm nz_prod_eq}) cth
in rth end
| _ => Thm.reflexive ct);

local
val less_iff_diff_less_0 = mk_meta_eq @{thm "less_iff_diff_less_0"}
val le_iff_diff_le_0 = mk_meta_eq @{thm "le_iff_diff_le_0"}
val eq_iff_diff_eq_0 = mk_meta_eq @{thm "eq_iff_diff_eq_0"}
val ss = simpset_of context
in
fun field_isolate_conv phi ctxt vs ct = case Thm.term_of ct of
Const_less _ for a b =>
let val (ca,cb) = Thm.dest_binop ct
val T = Thm.ctyp_of_cterm ca
val th = Thm.instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0
val nth = Conv.fconv_rule
(Conv.arg_conv (Conv.arg1_conv
(Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier_ord vs)))) th
val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
in rth end
| Const_less_eq _ for a b =>
let val (ca,cb) = Thm.dest_binop ct
val T = Thm.ctyp_of_cterm ca
val th = Thm.instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0
val nth = Conv.fconv_rule
(Conv.arg_conv (Conv.arg1_conv
(Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier_ord vs)))) th
val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
in rth end

| Const_HOL.eq _ for a b =>
let val (ca,cb) = Thm.dest_binop ct
val T = Thm.ctyp_of_cterm ca
val th = Thm.instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0
val nth = Conv.fconv_rule
(Conv.arg_conv (Conv.arg1_conv
(Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier_ord vs)))) th
val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
in rth end
| Const_Not for Const_HOL.eq _ for a b => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
| _ => Thm.reflexive ct
end;

fun classfield_whatis phi =
let
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
| Const_less _ for y z =>
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
| Const_less_eq _ for y z =>
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
| _ => Ferrante_Rackoff_Data.Nox
in h end;
fun class_field_ss phi ctxt =
simpset_of (put_simpset HOL_basic_ss ctxt