src/HOL/Decision_Procs/Dense_Linear_Order.thy
author wenzelm
Fri, 22 Nov 2013 20:37:19 +0100
changeset 54560 7f36da77130d
parent 53215 5e47c31c6f7c
child 54868 bab6cade3cc5
permissions -rw-r--r--
more .hgignore;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30439
57c68b3af2ea Updated paths in Decision_Procs comments and NEWS
hoelzl
parents: 29841
diff changeset
     1
(*  Title       : HOL/Decision_Procs/Dense_Linear_Order.thy
29655
ac31940cfb69 Plain, Main form meeting points in import hierarchy
haftmann
parents: 29509
diff changeset
     2
    Author      : Amine Chaieb, TU Muenchen
ac31940cfb69 Plain, Main form meeting points in import hierarchy
haftmann
parents: 29509
diff changeset
     3
*)
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
     4
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
     5
header {* Dense linear order without endpoints
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
     6
  and a quantifier elimination procedure in Ferrante and Rackoff style *}
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
     7
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
     8
theory Dense_Linear_Order
30738
0842e906300c normalized imports
haftmann
parents: 30652
diff changeset
     9
imports Main
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
    10
begin
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
    11
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47108
diff changeset
    12
ML_file "langford_data.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47108
diff changeset
    13
ML_file "ferrante_rackoff_data.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47108
diff changeset
    14
28402
09e4aa3ddc25 clarified dependencies between arith tools
haftmann
parents: 27825
diff changeset
    15
setup {* Langford_Data.setup #> Ferrante_Rackoff_Data.setup *}
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
    16
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
    17
context linorder
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
    18
begin
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
    19
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
    20
lemma less_not_permute[no_atp]: "\<not> (x < y \<and> y < x)"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
    21
  by (simp add: not_less linear)
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
    22
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
    23
lemma gather_simps[no_atp]: 
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
    24
  "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y) \<and> x < u \<and> P x) \<longleftrightarrow>
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
    25
    (\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> (insert u U). x < y) \<and> P x)"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
    26
  "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y) \<and> l < x \<and> P x) \<longleftrightarrow>
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
    27
    (\<exists>x. (\<forall>y \<in> (insert l L). y < x) \<and> (\<forall>y \<in> U. x < y) \<and> P x)"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
    28
  "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y) \<and> x < u) \<longleftrightarrow>
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
    29
    (\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> (insert u U). x < y))"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
    30
  "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y) \<and> l < x) \<longleftrightarrow>
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
    31
    (\<exists>x. (\<forall>y \<in> (insert l L). y < x) \<and> (\<forall>y \<in> U. x < y))"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
    32
  by auto
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
    33
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
    34
lemma gather_start [no_atp]: "(\<exists>x. P x) \<equiv> (\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y\<in> {}. x < y) \<and> P x)" 
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
    35
  by simp
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
    36
53072
acc495621d72 prefer plain subscript;
wenzelm
parents: 52090
diff changeset
    37
text{* Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>-\<^sub>\<infinity>)"}*}
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
    38
lemma minf_lt[no_atp]:  "\<exists>z . \<forall>x. x < z \<longrightarrow> (x < t \<longleftrightarrow> True)" by auto
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
    39
lemma minf_gt[no_atp]: "\<exists>z . \<forall>x. x < z \<longrightarrow>  (t < x \<longleftrightarrow>  False)"
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
    40
  by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le)
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
    41
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
    42
lemma minf_le[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<le> t \<longleftrightarrow> True)" by (auto simp add: less_le)
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
    43
lemma minf_ge[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (t \<le> x \<longleftrightarrow> False)"
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
    44
  by (auto simp add: less_le not_less not_le)
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
    45
lemma minf_eq[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
    46
lemma minf_neq[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
    47
lemma minf_P[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (P \<longleftrightarrow> P)" by blast
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
    48
53072
acc495621d72 prefer plain subscript;
wenzelm
parents: 52090
diff changeset
    49
text{* Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>+\<^sub>\<infinity>)"}*}
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
    50
lemma pinf_gt[no_atp]:  "\<exists>z. \<forall>x. z < x \<longrightarrow> (t < x \<longleftrightarrow> True)" by auto
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
    51
lemma pinf_lt[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow>  (x < t \<longleftrightarrow>  False)"
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
    52
  by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le)
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
    53
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
    54
lemma pinf_ge[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (t \<le> x \<longleftrightarrow> True)" by (auto simp add: less_le)
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
    55
lemma pinf_le[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x \<le> t \<longleftrightarrow> False)"
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
    56
  by (auto simp add: less_le not_less not_le)
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
    57
lemma pinf_eq[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
    58
lemma pinf_neq[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
    59
lemma pinf_P[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (P \<longleftrightarrow> P)" by blast
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
    60
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
    61
lemma nmi_lt[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x < t \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
    62
lemma nmi_gt[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t < x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)"
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
    63
  by (auto simp add: le_less)
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
    64
lemma  nmi_le[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x\<le> t \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
    65
lemma  nmi_ge[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t\<le> x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
    66
lemma  nmi_eq[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  x = t \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
    67
lemma  nmi_neq[no_atp]: "t \<in> U \<Longrightarrow>\<forall>x. \<not>True \<and> x \<noteq> t \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
    68
lemma  nmi_P[no_atp]: "\<forall> x. ~P \<and> P \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
    69
lemma  nmi_conj[no_atp]: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x) ;
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
    70
  \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)\<rbrakk> \<Longrightarrow>
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
    71
  \<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
    72
lemma  nmi_disj[no_atp]: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x) ;
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
    73
  \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)\<rbrakk> \<Longrightarrow>
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
    74
  \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
    75
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
    76
lemma  npi_lt[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  x < t \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by (auto simp add: le_less)
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
    77
lemma  npi_gt[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> t < x \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
    78
lemma  npi_le[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  x \<le> t \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
    79
lemma  npi_ge[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> t \<le> x \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
    80
lemma  npi_eq[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  x = t \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
    81
lemma  npi_neq[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x \<noteq> t \<longrightarrow>  (\<exists> u\<in> U. x \<le> u )" by auto
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
    82
lemma  npi_P[no_atp]: "\<forall> x. ~P \<and> P \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
    83
lemma  npi_conj[no_atp]: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. x \<le> u) ;  \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)\<rbrakk>
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
    84
  \<Longrightarrow>  \<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
    85
lemma  npi_disj[no_atp]: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. x \<le> u) ; \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)\<rbrakk>
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
    86
  \<Longrightarrow> \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
    87
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
    88
lemma lin_dense_lt[no_atp]:
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
    89
  "t \<in> U \<Longrightarrow>
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
    90
    \<forall>x l u. (\<forall> t. l < t \<and> t < u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> x < t \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y < t)"
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
    91
proof(clarsimp)
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
    92
  fix x l u y
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
    93
  assume tU: "t \<in> U" and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x"
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
    94
    and xu: "x<u"  and px: "x < t" and ly: "l<y" and yu:"y < u"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
    95
  from tU noU ly yu have tny: "t\<noteq>y" by auto
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
    96
  { assume H: "t < y"
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
    97
    from less_trans[OF lx px] less_trans[OF H yu]
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
    98
    have "l < t \<and> t < u" by simp
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
    99
    with tU noU have "False" by auto }
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   100
  then have "\<not> t < y" by auto
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   101
  then have "y \<le> t" by (simp add: not_less)
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   102
  then show "y < t" using tny by (simp add: less_le)
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   103
qed
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   104
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   105
lemma lin_dense_gt[no_atp]:
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   106
  "t \<in> U \<Longrightarrow>
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   107
    \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l < x \<and> x < u \<and> t < x \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> t < y)"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   108
proof(clarsimp)
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   109
  fix x l u y
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   110
  assume tU: "t \<in> U" and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x" and xu: "x<u"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   111
    and px: "t < x" and ly: "l<y" and yu:"y < u"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   112
  from tU noU ly yu have tny: "t\<noteq>y" by auto
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   113
  { assume H: "y< t"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   114
    from less_trans[OF ly H] less_trans[OF px xu] have "l < t \<and> t < u" by simp
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   115
    with tU noU have "False" by auto }
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   116
  then have "\<not> y<t" by auto
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   117
  then have "t \<le> y" by (auto simp add: not_less)
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   118
  then show "t < y" using tny by (simp add: less_le)
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   119
qed
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   120
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   121
lemma lin_dense_le[no_atp]:
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   122
  "t \<in> U \<Longrightarrow>
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   123
    \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> x \<le> t \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y\<le> t)"
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   124
proof(clarsimp)
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   125
  fix x l u y
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   126
  assume tU: "t \<in> U" and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x" and xu: "x<u"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   127
    and px: "x \<le> t" and ly: "l<y" and yu:"y < u"
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   128
  from tU noU ly yu have tny: "t\<noteq>y" by auto
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   129
  { assume H: "t < y"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   130
    from less_le_trans[OF lx px] less_trans[OF H yu]
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   131
    have "l < t \<and> t < u" by simp
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   132
    with tU noU have "False" by auto }
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   133
  then have "\<not> t < y" by auto
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   134
  then show "y \<le> t" by (simp add: not_less)
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   135
qed
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   136
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   137
lemma lin_dense_ge[no_atp]:
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   138
  "t \<in> U \<Longrightarrow>
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   139
    \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> t \<le> x \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> t \<le> y)"
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   140
proof(clarsimp)
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   141
  fix x l u y
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   142
  assume tU: "t \<in> U" and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x" and xu: "x<u"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   143
    and px: "t \<le> x" and ly: "l<y" and yu:"y < u"
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   144
  from tU noU ly yu have tny: "t\<noteq>y" by auto
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   145
  { assume H: "y< t"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   146
    from less_trans[OF ly H] le_less_trans[OF px xu]
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   147
    have "l < t \<and> t < u" by simp
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   148
    with tU noU have "False" by auto }
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   149
  then have "\<not> y<t" by auto
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   150
  then show "t \<le> y" by (simp add: not_less)
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   151
qed
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   152
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   153
lemma lin_dense_eq[no_atp]:
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   154
  "t \<in> U \<Longrightarrow>
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   155
    \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> x = t   \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y= t)"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   156
  by auto
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   157
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   158
lemma lin_dense_neq[no_atp]:
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   159
  "t \<in> U \<Longrightarrow>
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   160
    \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> x \<noteq> t   \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y\<noteq> t)"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   161
  by auto
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   162
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   163
lemma lin_dense_P[no_atp]:
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   164
  "\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P   \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P)"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   165
  by auto
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   166
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
   167
lemma lin_dense_conj[no_atp]:
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   168
  "\<lbrakk>\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P1 x
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   169
  \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P1 y) ;
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   170
  \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P2 x
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   171
  \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow>
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   172
  \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> (P1 x \<and> P2 x)
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   173
  \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> (P1 y \<and> P2 y))"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   174
  by blast
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
   175
lemma lin_dense_disj[no_atp]:
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   176
  "\<lbrakk>\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P1 x
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   177
  \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P1 y) ;
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   178
  \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P2 x
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   179
  \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow>
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   180
  \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> (P1 x \<or> P2 x)
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   181
  \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> (P1 y \<or> P2 y))"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   182
  by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   183
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
   184
lemma npmibnd[no_atp]: "\<lbrakk>\<forall>x. \<not> MP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<le> x); \<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. x \<le> u)\<rbrakk>
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   185
  \<Longrightarrow> \<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<le> x \<and> x \<le> u')"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   186
  by auto
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   187
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
   188
lemma finite_set_intervals[no_atp]:
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   189
  assumes px: "P x" and lx: "l \<le> x" and xu: "x \<le> u" and linS: "l\<in> S"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   190
    and uinS: "u \<in> S" and fS:"finite S" and lS: "\<forall> x\<in> S. l \<le> x" and Su: "\<forall> x\<in> S. x \<le> u"
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   191
  shows "\<exists> a \<in> S. \<exists> b \<in> S. (\<forall> y. a < y \<and> y < b \<longrightarrow> y \<notin> S) \<and> a \<le> x \<and> x \<le> b \<and> P x"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   192
proof -
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   193
  let ?Mx = "{y. y\<in> S \<and> y \<le> x}"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   194
  let ?xM = "{y. y\<in> S \<and> x \<le> y}"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   195
  let ?a = "Max ?Mx"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   196
  let ?b = "Min ?xM"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   197
  have MxS: "?Mx \<subseteq> S" by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   198
  hence fMx: "finite ?Mx" using fS finite_subset by auto
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   199
  from lx linS have linMx: "l \<in> ?Mx" by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   200
  hence Mxne: "?Mx \<noteq> {}" by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   201
  have xMS: "?xM \<subseteq> S" by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   202
  hence fxM: "finite ?xM" using fS finite_subset by auto
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   203
  from xu uinS have linxM: "u \<in> ?xM" by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   204
  hence xMne: "?xM \<noteq> {}" by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   205
  have ax:"?a \<le> x" using Mxne fMx by auto
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   206
  have xb:"x \<le> ?b" using xMne fxM by auto
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   207
  have "?a \<in> ?Mx" using Max_in[OF fMx Mxne] by simp hence ainS: "?a \<in> S" using MxS by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   208
  have "?b \<in> ?xM" using Min_in[OF fxM xMne] by simp hence binS: "?b \<in> S" using xMS by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   209
  have noy:"\<forall> y. ?a < y \<and> y < ?b \<longrightarrow> y \<notin> S"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   210
  proof(clarsimp)
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   211
    fix y
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   212
    assume ay: "?a < y" and yb: "y < ?b" and yS: "y \<in> S"
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   213
    from yS have "y\<in> ?Mx \<or> y\<in> ?xM" by (auto simp add: linear)
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   214
    moreover {
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   215
      assume "y \<in> ?Mx"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   216
      hence "y \<le> ?a" using Mxne fMx by auto
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   217
      with ay have "False" by (simp add: not_le[symmetric])
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   218
    }
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   219
    moreover {
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   220
      assume "y \<in> ?xM"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   221
      hence "?b \<le> y" using xMne fxM by auto
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   222
      with yb have "False" by (simp add: not_le[symmetric])
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   223
    }
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   224
    ultimately show False by blast
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   225
  qed
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   226
  from ainS binS noy ax xb px show ?thesis by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   227
qed
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   228
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
   229
lemma finite_set_intervals2[no_atp]:
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   230
  assumes px: "P x" and lx: "l \<le> x" and xu: "x \<le> u" and linS: "l\<in> S"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   231
    and uinS: "u \<in> S" and fS:"finite S" and lS: "\<forall> x\<in> S. l \<le> x" and Su: "\<forall> x\<in> S. x \<le> u"
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   232
  shows "(\<exists> s\<in> S. P s) \<or> (\<exists> a \<in> S. \<exists> b \<in> S. (\<forall> y. a < y \<and> y < b \<longrightarrow> y \<notin> S) \<and> a < x \<and> x < b \<and> P x)"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   233
proof-
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   234
  from finite_set_intervals[where P="P", OF px lx xu linS uinS fS lS Su]
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   235
  obtain a and b where as: "a\<in> S" and bs: "b\<in> S" and noS:"\<forall>y. a < y \<and> y < b \<longrightarrow> y \<notin> S"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   236
    and axb: "a \<le> x \<and> x \<le> b \<and> P x" by auto
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   237
  from axb have "x= a \<or> x= b \<or> (a < x \<and> x < b)" by (auto simp add: le_less)
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   238
  thus ?thesis using px as bs noS by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   239
qed
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   240
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   241
end
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   242
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   243
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   244
section {* The classical QE after Langford for dense linear orders *}
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   245
53215
5e47c31c6f7c renamed typeclass dense_linorder to unbounded_dense_linorder
hoelzl
parents: 53072
diff changeset
   246
context unbounded_dense_linorder
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   247
begin
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   248
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   249
lemma interval_empty_iff: "{y. x < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
27825
12254665fc41 re-arranged class dense_linear_order
haftmann
parents: 27487
diff changeset
   250
  by (auto dest: dense)
12254665fc41 re-arranged class dense_linear_order
haftmann
parents: 27487
diff changeset
   251
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
   252
lemma dlo_qe_bnds[no_atp]: 
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   253
  assumes ne: "L \<noteq> {}" and neU: "U \<noteq> {}" and fL: "finite L" and fU: "finite U"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   254
  shows "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y)) \<equiv> (\<forall> l \<in> L. \<forall>u \<in> U. l < u)"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   255
proof (simp only: atomize_eq, rule iffI)
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   256
  assume H: "\<exists>x. (\<forall>y\<in>L. y < x) \<and> (\<forall>y\<in>U. x < y)"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   257
  then obtain x where xL: "\<forall>y\<in>L. y < x" and xU: "\<forall>y\<in>U. x < y" by blast
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   258
  { fix l u assume l: "l \<in> L" and u: "u \<in> U"
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   259
    have "l < x" using xL l by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   260
    also have "x < u" using xU u by blast
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   261
    finally (less_trans) have "l < u" . }
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   262
  then show "\<forall>l\<in>L. \<forall>u\<in>U. l < u" by blast
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   263
next
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   264
  assume H: "\<forall>l\<in>L. \<forall>u\<in>U. l < u"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   265
  let ?ML = "Max L"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   266
  let ?MU = "Min U"  
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   267
  from fL ne have th1: "?ML \<in> L" and th1': "\<forall>l\<in>L. l \<le> ?ML" by auto
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   268
  from fU neU have th2: "?MU \<in> U" and th2': "\<forall>u\<in>U. ?MU \<le> u" by auto
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   269
  from th1 th2 H have "?ML < ?MU" by auto
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   270
  with dense obtain w where th3: "?ML < w" and th4: "w < ?MU" by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   271
  from th3 th1' have "\<forall>l \<in> L. l < w" by auto
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   272
  moreover from th4 th2' have "\<forall>u \<in> U. w < u" by auto
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   273
  ultimately show "\<exists>x. (\<forall>y\<in>L. y < x) \<and> (\<forall>y\<in>U. x < y)" by auto
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   274
qed
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   275
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
   276
lemma dlo_qe_noub[no_atp]: 
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   277
  assumes ne: "L \<noteq> {}" and fL: "finite L"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   278
  shows "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> {}. x < y)) \<equiv> True"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   279
proof(simp add: atomize_eq)
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   280
  from gt_ex[of "Max L"] obtain M where M: "Max L < M" by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   281
  from ne fL have "\<forall>x \<in> L. x \<le> Max L" by simp
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   282
  with M have "\<forall>x\<in>L. x < M" by (auto intro: le_less_trans)
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   283
  thus "\<exists>x. \<forall>y\<in>L. y < x" by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   284
qed
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   285
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
   286
lemma dlo_qe_nolb[no_atp]: 
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   287
  assumes ne: "U \<noteq> {}" and fU: "finite U"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   288
  shows "(\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y \<in> U. x < y)) \<equiv> True"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   289
proof(simp add: atomize_eq)
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   290
  from lt_ex[of "Min U"] obtain M where M: "M < Min U" by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   291
  from ne fU have "\<forall>x \<in> U. Min U \<le> x" by simp
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   292
  with M have "\<forall>x\<in>U. M < x" by (auto intro: less_le_trans)
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   293
  thus "\<exists>x. \<forall>y\<in>U. x < y" by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   294
qed
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   295
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
   296
lemma exists_neq[no_atp]: "\<exists>(x::'a). x \<noteq> t" "\<exists>(x::'a). t \<noteq> x" 
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   297
  using gt_ex[of t] by auto
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   298
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
   299
lemmas dlo_simps[no_atp] = order_refl less_irrefl not_less not_le exists_neq 
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   300
  le_less neq_iff linear less_not_permute
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   301
53215
5e47c31c6f7c renamed typeclass dense_linorder to unbounded_dense_linorder
hoelzl
parents: 53072
diff changeset
   302
lemma axiom[no_atp]: "class.unbounded_dense_linorder (op \<le>) (op <)"
5e47c31c6f7c renamed typeclass dense_linorder to unbounded_dense_linorder
hoelzl
parents: 53072
diff changeset
   303
  by (rule unbounded_dense_linorder_axioms)
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
   304
lemma atoms[no_atp]:
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   305
  shows "TERM (less :: 'a \<Rightarrow> _)"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   306
    and "TERM (less_eq :: 'a \<Rightarrow> _)"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   307
    and "TERM (op = :: 'a \<Rightarrow> _)" .
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   308
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   309
declare axiom[langford qe: dlo_qe_bnds dlo_qe_nolb dlo_qe_noub gather: gather_start gather_simps atoms: atoms]
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   310
declare dlo_simps[langfordsimp]
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   311
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   312
end
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   313
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   314
(* FIXME: Move to HOL -- together with the conj_aci_rule in langford.ML *)
41849
1a65b780bd56 Some cleaning up
nipkow
parents: 38864
diff changeset
   315
lemmas dnf[no_atp] = conj_disj_distribL conj_disj_distribR
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   316
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
   317
lemmas weak_dnf_simps[no_atp] = simp_thms dnf
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   318
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
   319
lemma nnf_simps[no_atp]:
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   320
    "(\<not>(P \<and> Q)) = (\<not>P \<or> \<not>Q)" "(\<not>(P \<or> Q)) = (\<not>P \<and> \<not>Q)" "(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   321
    "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   322
  by blast+
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   323
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
   324
lemma ex_distrib[no_atp]: "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> ((\<exists>x. P x) \<or> (\<exists>x. Q x))" by blast
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   325
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
   326
lemmas dnf_simps[no_atp] = weak_dnf_simps nnf_simps ex_distrib
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   327
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47108
diff changeset
   328
ML_file "langford.ML"
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   329
method_setup dlo = {*
30549
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
   330
  Scan.succeed (SIMPLE_METHOD' o LangfordQE.dlo_tac)
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   331
*} "Langford's algorithm for quantifier elimination in dense linear orders"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   332
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   333
30652
752329615264 distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents: 30549
diff changeset
   334
section {* Contructive dense linear orders yield QE for linear arithmetic over ordered Fields *}
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   335
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   336
text {* Linear order without upper bounds *}
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   337
29509
1ff0f3f08a7b migrated class package to new locale implementation
haftmann
parents: 29252
diff changeset
   338
locale linorder_stupid_syntax = linorder
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   339
begin
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   340
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   341
notation
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   342
  less_eq  ("op \<sqsubseteq>") and
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   343
  less_eq  ("(_/ \<sqsubseteq> _)" [51, 51] 50) and
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   344
  less  ("op \<sqsubset>") and
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   345
  less  ("(_/ \<sqsubset> _)"  [51, 51] 50)
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   346
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   347
end
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   348
29509
1ff0f3f08a7b migrated class package to new locale implementation
haftmann
parents: 29252
diff changeset
   349
locale linorder_no_ub = linorder_stupid_syntax +
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   350
  assumes gt_ex: "\<exists>y. less x y"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   351
begin
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   352
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
   353
lemma ge_ex[no_atp]: "\<exists>y. x \<sqsubseteq> y" using gt_ex by auto
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   354
53072
acc495621d72 prefer plain subscript;
wenzelm
parents: 52090
diff changeset
   355
text {* Theorems for @{text "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>+\<^sub>\<infinity>)"} *}
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
   356
lemma pinf_conj[no_atp]:
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   357
  assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   358
  and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   359
  shows "\<exists>z. \<forall>x. z \<sqsubset>  x \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   360
proof-
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   361
  from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   362
     and z2: "\<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   363
  from gt_ex obtain z where z:"ord.max less_eq z1 z2 \<sqsubset> z" by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   364
  from z have zz1: "z1 \<sqsubset> z" and zz2: "z2 \<sqsubset> z" by simp_all
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   365
  { fix x assume H: "z \<sqsubset> x"
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   366
    from less_trans[OF zz1 H] less_trans[OF zz2 H]
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   367
    have "(P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2')"  using z1 zz1 z2 zz2 by auto
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   368
  }
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   369
  thus ?thesis by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   370
qed
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   371
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
   372
lemma pinf_disj[no_atp]:
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   373
  assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   374
    and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   375
  shows "\<exists>z. \<forall>x. z \<sqsubset>  x \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   376
proof-
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   377
  from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   378
     and z2: "\<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   379
  from gt_ex obtain z where z:"ord.max less_eq z1 z2 \<sqsubset> z" by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   380
  from z have zz1: "z1 \<sqsubset> z" and zz2: "z2 \<sqsubset> z" by simp_all
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   381
  { fix x assume H: "z \<sqsubset> x"
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   382
    from less_trans[OF zz1 H] less_trans[OF zz2 H]
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   383
    have "(P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2')"  using z1 zz1 z2 zz2 by auto
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   384
  }
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   385
  thus ?thesis by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   386
qed
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   387
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
   388
lemma pinf_ex[no_atp]: assumes ex:"\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   389
proof -
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   390
  from ex obtain z where z: "\<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   391
  from gt_ex obtain x where x: "z \<sqsubset> x" by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   392
  from z x p1 show ?thesis by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   393
qed
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   394
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   395
end
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   396
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   397
text {* Linear order without upper bounds *}
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   398
29509
1ff0f3f08a7b migrated class package to new locale implementation
haftmann
parents: 29252
diff changeset
   399
locale linorder_no_lb = linorder_stupid_syntax +
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   400
  assumes lt_ex: "\<exists>y. less y x"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   401
begin
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   402
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
   403
lemma le_ex[no_atp]: "\<exists>y. y \<sqsubseteq> x" using lt_ex by auto
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   404
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   405
53072
acc495621d72 prefer plain subscript;
wenzelm
parents: 52090
diff changeset
   406
text {* Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>-\<^sub>\<infinity>)"} *}
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
   407
lemma minf_conj[no_atp]:
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   408
  assumes ex1: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   409
    and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   410
  shows "\<exists>z. \<forall>x. x \<sqsubset>  z \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   411
proof-
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   412
  from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"and z2: "\<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   413
  from lt_ex obtain z where z:"z \<sqsubset> ord.min less_eq z1 z2" by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   414
  from z have zz1: "z \<sqsubset> z1" and zz2: "z \<sqsubset> z2" by simp_all
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   415
  { fix x assume H: "x \<sqsubset> z"
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   416
    from less_trans[OF H zz1] less_trans[OF H zz2]
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   417
    have "(P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2')"  using z1 zz1 z2 zz2 by auto
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   418
  }
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   419
  thus ?thesis by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   420
qed
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   421
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
   422
lemma minf_disj[no_atp]:
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   423
  assumes ex1: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   424
    and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   425
  shows "\<exists>z. \<forall>x. x \<sqsubset>  z \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   426
proof -
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   427
  from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   428
    and z2: "\<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   429
  from lt_ex obtain z where z:"z \<sqsubset> ord.min less_eq z1 z2" by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   430
  from z have zz1: "z \<sqsubset> z1" and zz2: "z \<sqsubset> z2" by simp_all
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   431
  { fix x assume H: "x \<sqsubset> z"
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   432
    from less_trans[OF H zz1] less_trans[OF H zz2]
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   433
    have "(P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2')"  using z1 zz1 z2 zz2 by auto
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   434
  }
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   435
  thus ?thesis by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   436
qed
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   437
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   438
lemma minf_ex[no_atp]:
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   439
  assumes ex: "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P1)"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   440
    and p1: P1
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   441
  shows "\<exists> x. P x"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   442
proof -
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   443
  from ex obtain z where z: "\<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   444
  from lt_ex obtain x where x: "x \<sqsubset> z" by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   445
  from z x p1 show ?thesis by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   446
qed
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   447
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   448
end
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   449
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   450
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   451
locale constr_dense_linorder = linorder_no_lb + linorder_no_ub +
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   452
  fixes between
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   453
  assumes between_less: "less x y \<Longrightarrow> less x (between x y) \<and> less (between x y) y"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   454
    and between_same: "between x x = x"
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   455
53215
5e47c31c6f7c renamed typeclass dense_linorder to unbounded_dense_linorder
hoelzl
parents: 53072
diff changeset
   456
sublocale  constr_dense_linorder < dlo: unbounded_dense_linorder 
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   457
  apply unfold_locales
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   458
  using gt_ex lt_ex between_less
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   459
  apply auto
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   460
  apply (rule_tac x="between x y" in exI)
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   461
  apply simp
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   462
  done
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   463
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   464
context constr_dense_linorder
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   465
begin
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   466
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
   467
lemma rinf_U[no_atp]:
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   468
  assumes fU: "finite U"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   469
    and lin_dense: "\<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> P x
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   470
      \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P y )"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   471
    and nmpiU: "\<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<sqsubseteq> x \<and> x \<sqsubseteq> u')"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   472
    and nmi: "\<not> MP"  and npi: "\<not> PP"  and ex: "\<exists> x.  P x"
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   473
  shows "\<exists> u\<in> U. \<exists> u' \<in> U. P (between u u')"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   474
proof -
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   475
  from ex obtain x where px: "P x" by blast
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   476
  from px nmi npi nmpiU have "\<exists> u\<in> U. \<exists> u' \<in> U. u \<sqsubseteq> x \<and> x \<sqsubseteq> u'" by auto
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   477
  then obtain u and u' where uU:"u\<in> U" and uU': "u' \<in> U" and ux:"u \<sqsubseteq> x" and xu':"x \<sqsubseteq> u'" by auto
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   478
  from uU have Une: "U \<noteq> {}" by auto
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   479
  let ?l = "linorder.Min less_eq U"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   480
  let ?u = "linorder.Max less_eq U"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   481
  have linM: "?l \<in> U" using fU Une by simp
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   482
  have uinM: "?u \<in> U" using fU Une by simp
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   483
  have lM: "\<forall> t\<in> U. ?l \<sqsubseteq> t" using Une fU by auto
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   484
  have Mu: "\<forall> t\<in> U. t \<sqsubseteq> ?u" using Une fU by auto
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   485
  have th:"?l \<sqsubseteq> u" using uU Une lM by auto
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   486
  from order_trans[OF th ux] have lx: "?l \<sqsubseteq> x" .
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   487
  have th: "u' \<sqsubseteq> ?u" using uU' Une Mu by simp
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   488
  from order_trans[OF xu' th] have xu: "x \<sqsubseteq> ?u" .
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   489
  from finite_set_intervals2[where P="P",OF px lx xu linM uinM fU lM Mu]
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   490
  have "(\<exists> s\<in> U. P s) \<or>
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   491
      (\<exists> t1\<in> U. \<exists> t2 \<in> U. (\<forall> y. t1 \<sqsubset> y \<and> y \<sqsubset> t2 \<longrightarrow> y \<notin> U) \<and> t1 \<sqsubset> x \<and> x \<sqsubset> t2 \<and> P x)" .
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   492
  moreover {
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   493
    fix u assume um: "u\<in>U" and pu: "P u"
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   494
    have "between u u = u" by (simp add: between_same)
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   495
    with um pu have "P (between u u)" by simp
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   496
    with um have ?thesis by blast }
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   497
  moreover {
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   498
    assume "\<exists> t1\<in> U. \<exists> t2 \<in> U. (\<forall> y. t1 \<sqsubset> y \<and> y \<sqsubset> t2 \<longrightarrow> y \<notin> U) \<and> t1 \<sqsubset> x \<and> x \<sqsubset> t2 \<and> P x"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   499
    then obtain t1 and t2 where t1M: "t1 \<in> U" and t2M: "t2\<in> U"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   500
      and noM: "\<forall> y. t1 \<sqsubset> y \<and> y \<sqsubset> t2 \<longrightarrow> y \<notin> U"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   501
      and t1x: "t1 \<sqsubset> x" and xt2: "x \<sqsubset> t2" and px: "P x" by blast
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   502
    from less_trans[OF t1x xt2] have t1t2: "t1 \<sqsubset> t2" .
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   503
    let ?u = "between t1 t2"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   504
    from between_less t1t2 have t1lu: "t1 \<sqsubset> ?u" and ut2: "?u \<sqsubset> t2" by auto
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   505
    from lin_dense noM t1x xt2 px t1lu ut2 have "P ?u" by blast
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   506
    with t1M t2M have ?thesis by blast
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   507
  }
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   508
  ultimately show ?thesis by blast
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   509
qed
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   510
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
   511
theorem fr_eq[no_atp]:
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   512
  assumes fU: "finite U"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   513
    and lin_dense: "\<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> P x
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   514
     \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P y )"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   515
    and nmibnd: "\<forall>x. \<not> MP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<sqsubseteq> x)"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   516
    and npibnd: "\<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. x \<sqsubseteq> u)"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   517
    and mi: "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x = MP)"  and pi: "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x = PP)"
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   518
  shows "(\<exists> x. P x) \<equiv> (MP \<or> PP \<or> (\<exists> u \<in> U. \<exists> u'\<in> U. P (between u u')))"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   519
  (is "_ \<equiv> (_ \<or> _ \<or> ?F)" is "?E \<equiv> ?D")
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   520
proof -
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   521
  { assume px: "\<exists> x. P x"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   522
    have "MP \<or> PP \<or> (\<not> MP \<and> \<not> PP)" by blast
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   523
    moreover { assume "MP \<or> PP" hence "?D" by blast }
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   524
    moreover {
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   525
      assume nmi: "\<not> MP" and npi: "\<not> PP"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   526
      from npmibnd[OF nmibnd npibnd]
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   527
      have nmpiU: "\<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<sqsubseteq> x \<and> x \<sqsubseteq> u')" .
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   528
      from rinf_U[OF fU lin_dense nmpiU nmi npi px] have "?D" by blast }
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   529
    ultimately have "?D" by blast }
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   530
  moreover
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   531
  { assume "?D"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   532
    moreover { assume m:"MP" from minf_ex[OF mi m] have "?E" . }
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   533
    moreover { assume p: "PP" from pinf_ex[OF pi p] have "?E" . }
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   534
    moreover { assume f:"?F" hence "?E" by blast }
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   535
    ultimately have "?E" by blast }
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   536
  ultimately have "?E = ?D" by blast thus "?E \<equiv> ?D" by simp
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   537
qed
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   538
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
   539
lemmas minf_thms[no_atp] = minf_conj minf_disj minf_eq minf_neq minf_lt minf_le minf_gt minf_ge minf_P
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
   540
lemmas pinf_thms[no_atp] = pinf_conj pinf_disj pinf_eq pinf_neq pinf_lt pinf_le pinf_gt pinf_ge pinf_P
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   541
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
   542
lemmas nmi_thms[no_atp] = nmi_conj nmi_disj nmi_eq nmi_neq nmi_lt nmi_le nmi_gt nmi_ge nmi_P
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
   543
lemmas npi_thms[no_atp] = npi_conj npi_disj npi_eq npi_neq npi_lt npi_le npi_gt npi_ge npi_P
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
   544
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
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   545
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
   546
lemma ferrack_axiom[no_atp]: "constr_dense_linorder less_eq less between"
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   547
  by (rule constr_dense_linorder_axioms)
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   548
35828
46cfc4b8112e now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents: 35267
diff changeset
   549
lemma atoms[no_atp]:
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   550
  shows "TERM (less :: 'a \<Rightarrow> _)"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   551
    and "TERM (less_eq :: 'a \<Rightarrow> _)"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   552
    and "TERM (op = :: 'a \<Rightarrow> _)" .
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   553
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   554
declare ferrack_axiom [ferrack minf: minf_thms pinf: pinf_thms
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   555
    nmi: nmi_thms npi: npi_thms lindense:
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   556
    lin_dense_thms qe: fr_eq atoms: atoms]
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   557
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   558
declaration {*
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   559
let
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   560
  fun simps phi = map (Morphism.thm phi) [@{thm "not_less"}, @{thm "not_le"}]
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   561
  fun generic_whatis phi =
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   562
    let
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   563
      val [lt, le] = map (Morphism.term phi) [@{term "op \<sqsubset>"}, @{term "op \<sqsubseteq>"}]
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   564
      fun h x t =
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   565
        case term_of t of
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   566
          Const(@{const_name HOL.eq}, _)$y$z =>
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   567
            if term_of x aconv y then Ferrante_Rackoff_Data.Eq
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   568
            else Ferrante_Rackoff_Data.Nox
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   569
       | @{term "Not"}$(Const(@{const_name HOL.eq}, _)$y$z) =>
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   570
            if term_of x aconv y then Ferrante_Rackoff_Data.NEq
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   571
            else Ferrante_Rackoff_Data.Nox
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   572
       | b$y$z => if Term.could_unify (b, lt) then
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   573
                     if term_of x aconv y then Ferrante_Rackoff_Data.Lt
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   574
                     else if term_of x aconv z then Ferrante_Rackoff_Data.Gt
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   575
                     else Ferrante_Rackoff_Data.Nox
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   576
                 else if Term.could_unify (b, le) then
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   577
                     if term_of x aconv y then Ferrante_Rackoff_Data.Le
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   578
                     else if term_of x aconv z then Ferrante_Rackoff_Data.Ge
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   579
                     else Ferrante_Rackoff_Data.Nox
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   580
                 else Ferrante_Rackoff_Data.Nox
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   581
       | _ => Ferrante_Rackoff_Data.Nox
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   582
  in h end
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 49756
diff changeset
   583
  fun ss phi =
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 49756
diff changeset
   584
    simpset_of (put_simpset HOL_ss @{context} addsimps (simps phi))
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   585
in
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   586
  Ferrante_Rackoff_Data.funs  @{thm "ferrack_axiom"}
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   587
    {isolate_conv = K (K (K Thm.reflexive)), whatis = generic_whatis, simpset = ss}
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   588
end
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   589
*}
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   590
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   591
end
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   592
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47108
diff changeset
   593
ML_file "ferrante_rackoff.ML"
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   594
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   595
method_setup ferrack = {*
30549
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
   596
  Scan.succeed (SIMPLE_METHOD' o FerranteRackoff.dlo_tac)
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   597
*} "Ferrante and Rackoff's algorithm for quantifier elimination in dense linear orders"
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   598
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   599
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   600
subsection {* Ferrante and Rackoff algorithm over ordered fields *}
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   601
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   602
lemma neg_prod_lt:"(c\<Colon>'a\<Colon>linordered_field) < 0 \<Longrightarrow> ((c*x < 0) == (x > 0))"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   603
proof -
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   604
  assume H: "c < 0"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   605
  have "c*x < 0 = (0/c < x)"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   606
    by (simp only: neg_divide_less_eq[OF H] algebra_simps)
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   607
  also have "\<dots> = (0 < x)" by simp
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   608
  finally show  "(c*x < 0) == (x > 0)" by simp
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   609
qed
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   610
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   611
lemma pos_prod_lt:"(c\<Colon>'a\<Colon>linordered_field) > 0 \<Longrightarrow> ((c*x < 0) == (x < 0))"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   612
proof -
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   613
  assume H: "c > 0"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   614
  then have "c*x < 0 = (0/c > x)"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   615
    by (simp only: pos_less_divide_eq[OF H] algebra_simps)
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   616
  also have "\<dots> = (0 > x)" by simp
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   617
  finally show  "(c*x < 0) == (x < 0)" by simp
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   618
qed
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   619
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   620
lemma neg_prod_sum_lt: "(c\<Colon>'a\<Colon>linordered_field) < 0 \<Longrightarrow> ((c*x + t< 0) == (x > (- 1/c)*t))"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   621
proof -
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   622
  assume H: "c < 0"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   623
  have "c*x + t< 0 = (c*x < -t)"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   624
    by (subst less_iff_diff_less_0 [of "c*x" "-t"], simp)
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   625
  also have "\<dots> = (-t/c < x)"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   626
    by (simp only: neg_divide_less_eq[OF H] algebra_simps)
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   627
  also have "\<dots> = ((- 1/c)*t < x)" by simp
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   628
  finally show "(c*x + t < 0) == (x > (- 1/c)*t)" by simp
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   629
qed
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   630
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   631
lemma pos_prod_sum_lt:"(c\<Colon>'a\<Colon>linordered_field) > 0 \<Longrightarrow> ((c*x + t < 0) == (x < (- 1/c)*t))"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   632
proof -
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   633
  assume H: "c > 0"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   634
  have "c*x + t< 0 = (c*x < -t)"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   635
    by (subst less_iff_diff_less_0 [of "c*x" "-t"], simp)
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   636
  also have "\<dots> = (-t/c > x)"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   637
    by (simp only: pos_less_divide_eq[OF H] algebra_simps)
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   638
  also have "\<dots> = ((- 1/c)*t > x)" by simp
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   639
  finally show  "(c*x + t < 0) == (x < (- 1/c)*t)" by simp
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   640
qed
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   641
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   642
lemma sum_lt:"((x::'a::ordered_ab_group_add) + t < 0) == (x < - t)"
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   643
  using less_diff_eq[where a= x and b=t and c=0] by simp
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   644
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   645
lemma neg_prod_le:"(c\<Colon>'a\<Colon>linordered_field) < 0 \<Longrightarrow> ((c*x <= 0) == (x >= 0))"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   646
proof -
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   647
  assume H: "c < 0"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   648
  have "c*x <= 0 = (0/c <= x)"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   649
    by (simp only: neg_divide_le_eq[OF H] algebra_simps)
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   650
  also have "\<dots> = (0 <= x)" by simp
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   651
  finally show  "(c*x <= 0) == (x >= 0)" by simp
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   652
qed
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   653
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   654
lemma pos_prod_le:"(c\<Colon>'a\<Colon>linordered_field) > 0 \<Longrightarrow> ((c*x <= 0) == (x <= 0))"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   655
proof -
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   656
  assume H: "c > 0"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   657
  hence "c*x <= 0 = (0/c >= x)"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   658
    by (simp only: pos_le_divide_eq[OF H] algebra_simps)
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   659
  also have "\<dots> = (0 >= x)" by simp
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   660
  finally show  "(c*x <= 0) == (x <= 0)" by simp
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   661
qed
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   662
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   663
lemma neg_prod_sum_le: "(c\<Colon>'a\<Colon>linordered_field) < 0 \<Longrightarrow> ((c*x + t <= 0) == (x >= (- 1/c)*t))"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   664
proof -
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   665
  assume H: "c < 0"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   666
  have "c*x + t <= 0 = (c*x <= -t)"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   667
    by (subst le_iff_diff_le_0 [of "c*x" "-t"], simp)
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   668
  also have "\<dots> = (-t/c <= x)"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   669
    by (simp only: neg_divide_le_eq[OF H] algebra_simps)
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   670
  also have "\<dots> = ((- 1/c)*t <= x)" by simp
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   671
  finally show "(c*x + t <= 0) == (x >= (- 1/c)*t)" by simp
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   672
qed
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   673
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   674
lemma pos_prod_sum_le:"(c\<Colon>'a\<Colon>linordered_field) > 0 \<Longrightarrow> ((c*x + t <= 0) == (x <= (- 1/c)*t))"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   675
proof -
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   676
  assume H: "c > 0"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   677
  have "c*x + t <= 0 = (c*x <= -t)"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   678
    by (subst le_iff_diff_le_0 [of "c*x" "-t"], simp)
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   679
  also have "\<dots> = (-t/c >= x)"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   680
    by (simp only: pos_le_divide_eq[OF H] algebra_simps)
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   681
  also have "\<dots> = ((- 1/c)*t >= x)" by simp
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   682
  finally show "(c*x + t <= 0) == (x <= (- 1/c)*t)" by simp
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   683
qed
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   684
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   685
lemma sum_le:"((x::'a::ordered_ab_group_add) + t <= 0) == (x <= - t)"
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   686
  using le_diff_eq[where a= x and b=t and c=0] by simp
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   687
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   688
lemma nz_prod_eq:"(c\<Colon>'a\<Colon>linordered_field) \<noteq> 0 \<Longrightarrow> ((c*x = 0) == (x = 0))" by simp
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   689
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   690
lemma nz_prod_sum_eq: "(c\<Colon>'a\<Colon>linordered_field) \<noteq> 0 \<Longrightarrow> ((c*x + t = 0) == (x = (- 1/c)*t))"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   691
proof -
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   692
  assume H: "c \<noteq> 0"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   693
  have "c*x + t = 0 = (c*x = -t)"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   694
    by (subst eq_iff_diff_eq_0 [of "c*x" "-t"], simp)
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   695
  also have "\<dots> = (x = -t/c)"
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   696
    by (simp only: nonzero_eq_divide_eq[OF H] algebra_simps)
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   697
  finally show  "(c*x + t = 0) == (x = (- 1/c)*t)" by simp
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   698
qed
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   699
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   700
lemma sum_eq:"((x::'a::ordered_ab_group_add) + t = 0) == (x = - t)"
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   701
  using eq_diff_eq[where a= x and b=t and c=0] by simp
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   702
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   703
35043
07dbdf60d5ad dropped accidental duplication of "lin" prefix from cs. 108662d50512
haftmann
parents: 35028
diff changeset
   704
interpretation class_dense_linordered_field: constr_dense_linorder
29509
1ff0f3f08a7b migrated class package to new locale implementation
haftmann
parents: 29252
diff changeset
   705
 "op <=" "op <"
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   706
   "\<lambda> x y. 1/2 * ((x::'a::{linordered_field}) + y)"
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   707
  by unfold_locales (dlo, dlo, auto)
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   708
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   709
declaration{*
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   710
let
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   711
  fun earlier [] x y = false
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   712
    | earlier (h::t) x y =
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   713
        if h aconvc y then false else if h aconvc x then true else earlier t x y;
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   714
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   715
fun dest_frac ct =
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   716
  case term_of ct of
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   717
    Const (@{const_name Fields.divide},_) $ a $ b=>
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   718
      Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   719
  | Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd)
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   720
  | t => Rat.rat_of_int (snd (HOLogic.dest_number t))
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   721
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   722
fun mk_frac phi cT x =
49519
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   723
  let val (a, b) = Rat.quotient_of_rat x
4d2c93e1d9c8 misc tuning;
wenzelm
parents: 48891
diff changeset
   724
  in if b = 1 then Numeral.mk_cnumber cT a
46497
89ccf66aa73d renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents: 45620
diff changeset
   725
    else Thm.apply
89ccf66aa73d renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents: 45620
diff changeset
   726
         (Thm.apply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   727
                     (Numeral.mk_cnumber cT a))
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   728
         (Numeral.mk_cnumber cT b)
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   729
 end
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   730
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   731
fun whatis x ct = case term_of ct of
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   732
  Const(@{const_name Groups.plus}, _)$(Const(@{const_name Groups.times},_)$_$y)$_ =>
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   733
     if y aconv term_of x then ("c*x+t",[(funpow 2 Thm.dest_arg1) ct, Thm.dest_arg ct])
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   734
     else ("Nox",[])
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   735
| Const(@{const_name Groups.plus}, _)$y$_ =>
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   736
     if y aconv term_of x then ("x+t",[Thm.dest_arg ct])
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   737
     else ("Nox",[])
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   738
| Const(@{const_name Groups.times}, _)$_$y =>
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   739
     if y aconv term_of x then ("c*x",[Thm.dest_arg1 ct])
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   740
     else ("Nox",[])
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   741
| t => if t aconv term_of x then ("x",[]) else ("Nox",[]);
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   742
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36753
diff changeset
   743
fun xnormalize_conv ctxt [] ct = Thm.reflexive ct
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   744
| xnormalize_conv ctxt (vs as (x::_)) ct =
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   745
   case term_of ct of
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   746
   Const(@{const_name Orderings.less},_)$_$Const(@{const_name Groups.zero},_) =>
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   747
    (case whatis x (Thm.dest_arg1 ct) of
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   748
    ("c*x+t",[c,t]) =>
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   749
       let
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   750
        val cr = dest_frac c
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   751
        val clt = Thm.dest_fun2 ct
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   752
        val cz = Thm.dest_arg ct
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   753
        val neg = cr </ Rat.zero
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 49756
diff changeset
   754
        val cthp = Simplifier.rewrite ctxt
46497
89ccf66aa73d renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents: 45620
diff changeset
   755
               (Thm.apply @{cterm "Trueprop"}
89ccf66aa73d renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents: 45620
diff changeset
   756
                  (if neg then Thm.apply (Thm.apply clt c) cz
89ccf66aa73d renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents: 45620
diff changeset
   757
                    else Thm.apply (Thm.apply clt cz) c))
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36753
diff changeset
   758
        val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36753
diff changeset
   759
        val th = Thm.implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x,t])
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   760
             (if neg then @{thm neg_prod_sum_lt} else @{thm pos_prod_sum_lt})) cth
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   761
        val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
36753
5cf4e9128f22 renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents: 36635
diff changeset
   762
                   (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   763
      in rth end
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   764
    | ("x+t",[t]) =>
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   765
       let
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   766
        val T = ctyp_of_term x
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   767
        val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_lt"}
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   768
        val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
36753
5cf4e9128f22 renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents: 36635
diff changeset
   769
              (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   770
       in  rth end
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   771
    | ("c*x",[c]) =>
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   772
       let
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   773
        val cr = dest_frac c
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   774
        val clt = Thm.dest_fun2 ct
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   775
        val cz = Thm.dest_arg ct
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   776
        val neg = cr </ Rat.zero
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 49756
diff changeset
   777
        val cthp = Simplifier.rewrite ctxt
46497
89ccf66aa73d renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents: 45620
diff changeset
   778
               (Thm.apply @{cterm "Trueprop"}
89ccf66aa73d renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents: 45620
diff changeset
   779
                  (if neg then Thm.apply (Thm.apply clt c) cz
89ccf66aa73d renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents: 45620
diff changeset
   780
                    else Thm.apply (Thm.apply clt cz) c))
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36753
diff changeset
   781
        val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36753
diff changeset
   782
        val th = Thm.implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x])
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   783
             (if neg then @{thm neg_prod_lt} else @{thm pos_prod_lt})) cth
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   784
        val rth = th
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   785
      in rth end
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36753
diff changeset
   786
    | _ => Thm.reflexive ct)
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   787
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   788
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   789
|  Const(@{const_name Orderings.less_eq},_)$_$Const(@{const_name Groups.zero},_) =>
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   790
   (case whatis x (Thm.dest_arg1 ct) of
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   791
    ("c*x+t",[c,t]) =>
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   792
       let
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   793
        val T = ctyp_of_term x
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   794
        val cr = dest_frac c
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   795
        val clt = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "op <"}
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   796
        val cz = Thm.dest_arg ct
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   797
        val neg = cr </ Rat.zero
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 49756
diff changeset
   798
        val cthp = Simplifier.rewrite ctxt
46497
89ccf66aa73d renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents: 45620
diff changeset
   799
               (Thm.apply @{cterm "Trueprop"}
89ccf66aa73d renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents: 45620
diff changeset
   800
                  (if neg then Thm.apply (Thm.apply clt c) cz
89ccf66aa73d renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents: 45620
diff changeset
   801
                    else Thm.apply (Thm.apply clt cz) c))
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36753
diff changeset
   802
        val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36753
diff changeset
   803
        val th = Thm.implies_elim (instantiate' [SOME T] (map SOME [c,x,t])
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   804
             (if neg then @{thm neg_prod_sum_le} else @{thm pos_prod_sum_le})) cth
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   805
        val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
36753
5cf4e9128f22 renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents: 36635
diff changeset
   806
                   (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   807
      in rth end
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   808
    | ("x+t",[t]) =>
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   809
       let
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   810
        val T = ctyp_of_term x
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   811
        val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_le"}
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   812
        val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
36753
5cf4e9128f22 renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents: 36635
diff changeset
   813
              (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   814
       in  rth end
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   815
    | ("c*x",[c]) =>
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   816
       let
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   817
        val T = ctyp_of_term x
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   818
        val cr = dest_frac c
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   819
        val clt = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "op <"}
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   820
        val cz = Thm.dest_arg ct
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   821
        val neg = cr </ Rat.zero
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 49756
diff changeset
   822
        val cthp = Simplifier.rewrite ctxt
46497
89ccf66aa73d renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents: 45620
diff changeset
   823
               (Thm.apply @{cterm "Trueprop"}
89ccf66aa73d renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents: 45620
diff changeset
   824
                  (if neg then Thm.apply (Thm.apply clt c) cz
89ccf66aa73d renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents: 45620
diff changeset
   825
                    else Thm.apply (Thm.apply clt cz) c))
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36753
diff changeset
   826
        val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36753
diff changeset
   827
        val th = Thm.implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x])
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   828
             (if neg then @{thm neg_prod_le} else @{thm pos_prod_le})) cth
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   829
        val rth = th
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   830
      in rth end
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36753
diff changeset
   831
    | _ => Thm.reflexive ct)
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   832
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38549
diff changeset
   833
|  Const(@{const_name HOL.eq},_)$_$Const(@{const_name Groups.zero},_) =>
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   834
   (case whatis x (Thm.dest_arg1 ct) of
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   835
    ("c*x+t",[c,t]) =>
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   836
       let
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   837
        val T = ctyp_of_term x
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   838
        val cr = dest_frac c
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   839
        val ceq = Thm.dest_fun2 ct
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   840
        val cz = Thm.dest_arg ct
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 49756
diff changeset
   841
        val cthp = Simplifier.rewrite ctxt
46497
89ccf66aa73d renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents: 45620
diff changeset
   842
            (Thm.apply @{cterm "Trueprop"}
89ccf66aa73d renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents: 45620
diff changeset
   843
             (Thm.apply @{cterm "Not"} (Thm.apply (Thm.apply ceq c) cz)))
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36753
diff changeset
   844
        val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36753
diff changeset
   845
        val th = Thm.implies_elim
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   846
                 (instantiate' [SOME T] (map SOME [c,x,t]) @{thm nz_prod_sum_eq}) cth
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   847
        val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
36753
5cf4e9128f22 renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents: 36635
diff changeset
   848
                   (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   849
      in rth end
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   850
    | ("x+t",[t]) =>
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   851
       let
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   852
        val T = ctyp_of_term x
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   853
        val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_eq"}
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   854
        val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
36753
5cf4e9128f22 renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents: 36635
diff changeset
   855
              (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   856
       in  rth end
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   857
    | ("c*x",[c]) =>
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   858
       let
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   859
        val T = ctyp_of_term x
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   860
        val cr = dest_frac c
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   861
        val ceq = Thm.dest_fun2 ct
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   862
        val cz = Thm.dest_arg ct
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 49756
diff changeset
   863
        val cthp = Simplifier.rewrite ctxt
46497
89ccf66aa73d renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents: 45620
diff changeset
   864
            (Thm.apply @{cterm "Trueprop"}
89ccf66aa73d renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents: 45620
diff changeset
   865
             (Thm.apply @{cterm "Not"} (Thm.apply (Thm.apply ceq c) cz)))
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36753
diff changeset
   866
        val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36753
diff changeset
   867
        val rth = Thm.implies_elim
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   868
                 (instantiate' [SOME T] (map SOME [c,x]) @{thm nz_prod_eq}) cth
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   869
      in rth end
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36753
diff changeset
   870
    | _ => Thm.reflexive ct);
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   871
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   872
local
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   873
  val less_iff_diff_less_0 = mk_meta_eq @{thm "less_iff_diff_less_0"}
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   874
  val le_iff_diff_le_0 = mk_meta_eq @{thm "le_iff_diff_le_0"}
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   875
  val eq_iff_diff_eq_0 = mk_meta_eq @{thm "eq_iff_diff_eq_0"}
52090
ff1ec795604b proper context;
wenzelm
parents: 51717
diff changeset
   876
  val ss = simpset_of @{context}
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   877
in
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   878
fun field_isolate_conv phi ctxt vs ct = case term_of ct of
35092
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35084
diff changeset
   879
  Const(@{const_name Orderings.less},_)$a$b =>
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   880
   let val (ca,cb) = Thm.dest_binop ct
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   881
       val T = ctyp_of_term ca
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   882
       val th = instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   883
       val nth = Conv.fconv_rule
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   884
         (Conv.arg_conv (Conv.arg1_conv
52090
ff1ec795604b proper context;
wenzelm
parents: 51717
diff changeset
   885
              (Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier vs)))) th
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36753
diff changeset
   886
       val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   887
   in rth end
35092
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35084
diff changeset
   888
| Const(@{const_name Orderings.less_eq},_)$a$b =>
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   889
   let val (ca,cb) = Thm.dest_binop ct
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   890
       val T = ctyp_of_term ca
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   891
       val th = instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   892
       val nth = Conv.fconv_rule
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   893
         (Conv.arg_conv (Conv.arg1_conv
52090
ff1ec795604b proper context;
wenzelm
parents: 51717
diff changeset
   894
              (Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier vs)))) th
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36753
diff changeset
   895
       val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   896
   in rth end
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   897
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38549
diff changeset
   898
| Const(@{const_name HOL.eq},_)$a$b =>
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   899
   let val (ca,cb) = Thm.dest_binop ct
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   900
       val T = ctyp_of_term ca
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   901
       val th = instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   902
       val nth = Conv.fconv_rule
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   903
         (Conv.arg_conv (Conv.arg1_conv
52090
ff1ec795604b proper context;
wenzelm
parents: 51717
diff changeset
   904
              (Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier vs)))) th
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36753
diff changeset
   905
       val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   906
   in rth end
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38549
diff changeset
   907
| @{term "Not"} $(Const(@{const_name HOL.eq},_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36753
diff changeset
   908
| _ => Thm.reflexive ct
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   909
end;
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   910
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   911
fun classfield_whatis phi =
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   912
 let
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   913
  fun h x t =
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   914
   case term_of t of
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38549
diff changeset
   915
     Const(@{const_name HOL.eq}, _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   916
                            else Ferrante_Rackoff_Data.Nox
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38549
diff changeset
   917
   | @{term "Not"}$(Const(@{const_name HOL.eq}, _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   918
                            else Ferrante_Rackoff_Data.Nox
35092
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35084
diff changeset
   919
   | Const(@{const_name Orderings.less},_)$y$z =>
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   920
       if term_of x aconv y then Ferrante_Rackoff_Data.Lt
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   921
        else if term_of x aconv z then Ferrante_Rackoff_Data.Gt
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   922
        else Ferrante_Rackoff_Data.Nox
35092
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35084
diff changeset
   923
   | Const (@{const_name Orderings.less_eq},_)$y$z =>
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   924
         if term_of x aconv y then Ferrante_Rackoff_Data.Le
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   925
         else if term_of x aconv z then Ferrante_Rackoff_Data.Ge
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   926
         else Ferrante_Rackoff_Data.Nox
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   927
   | _ => Ferrante_Rackoff_Data.Nox
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   928
 in h end;
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   929
fun class_field_ss phi =
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 49756
diff changeset
   930
  simpset_of (put_simpset HOL_basic_ss @{context}
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 49756
diff changeset
   931
    addsimps ([@{thm "linorder_not_less"}, @{thm "linorder_not_le"}])
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 49756
diff changeset
   932
    |> fold Splitter.add_split [@{thm "abs_split"}, @{thm "split_max"}, @{thm "split_min"}])
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   933
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   934
in
35043
07dbdf60d5ad dropped accidental duplication of "lin" prefix from cs. 108662d50512
haftmann
parents: 35028
diff changeset
   935
Ferrante_Rackoff_Data.funs @{thm "class_dense_linordered_field.ferrack_axiom"}
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   936
  {isolate_conv = field_isolate_conv, whatis = classfield_whatis, simpset = class_field_ss}
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   937
end
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   938
*}
41849
1a65b780bd56 Some cleaning up
nipkow
parents: 38864
diff changeset
   939
(*
29841
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   940
lemma upper_bound_finite_set:
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   941
  assumes fS: "finite S"
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   942
  shows "\<exists>(a::'a::linorder). \<forall>x \<in> S. f x \<le> a"
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   943
proof(induct rule: finite_induct[OF fS])
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   944
  case 1 thus ?case by simp
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   945
next
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   946
  case (2 x F)
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   947
  from "2.hyps" obtain a where a:"\<forall>x \<in>F. f x \<le> a" by blast
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   948
  let ?a = "max a (f x)"
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   949
  have m: "a \<le> ?a" "f x \<le> ?a" by simp_all
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   950
  {fix y assume y: "y \<in> insert x F"
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   951
    {assume "y = x" hence "f y \<le> ?a" using m by simp}
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   952
    moreover
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   953
    {assume yF: "y\<in> F" from a[rule_format, OF yF] m have "f y \<le> ?a" by (simp add: max_def)}
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   954
    ultimately have "f y \<le> ?a" using y by blast}
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   955
  then show ?case by blast
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   956
qed
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   957
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   958
lemma lower_bound_finite_set:
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   959
  assumes fS: "finite S"
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   960
  shows "\<exists>(a::'a::linorder). \<forall>x \<in> S. f x \<ge> a"
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   961
proof(induct rule: finite_induct[OF fS])
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   962
  case 1 thus ?case by simp
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   963
next
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   964
  case (2 x F)
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   965
  from "2.hyps" obtain a where a:"\<forall>x \<in>F. f x \<ge> a" by blast
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   966
  let ?a = "min a (f x)"
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   967
  have m: "a \<ge> ?a" "f x \<ge> ?a" by simp_all
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   968
  {fix y assume y: "y \<in> insert x F"
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   969
    {assume "y = x" hence "f y \<ge> ?a" using m by simp}
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   970
    moreover
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   971
    {assume yF: "y\<in> F" from a[rule_format, OF yF] m have "f y \<ge> ?a" by (simp add: min_def)}
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   972
    ultimately have "f y \<ge> ?a" using y by blast}
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   973
  then show ?case by blast
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   974
qed
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   975
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   976
lemma bound_finite_set: assumes f: "finite S"
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   977
  shows "\<exists>a. \<forall>x \<in>S. (f x:: 'a::linorder) \<le> a"
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   978
proof-
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   979
  let ?F = "f ` S"
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   980
  from f have fF: "finite ?F" by simp
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   981
  let ?a = "Max ?F"
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   982
  {assume "S = {}" hence ?thesis by blast}
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   983
  moreover
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   984
  {assume Se: "S \<noteq> {}" hence Fe: "?F \<noteq> {}" by simp
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   985
  {fix x assume x: "x \<in> S"
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   986
    hence th0: "f x \<in> ?F" by simp
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   987
    hence "f x \<le> ?a" using Max_ge[OF fF th0] ..}
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   988
  hence ?thesis by blast}
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   989
ultimately show ?thesis by blast
86d94bb79226 A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents: 29823
diff changeset
   990
qed
41849
1a65b780bd56 Some cleaning up
nipkow
parents: 38864
diff changeset
   991
*)
26161
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   992
34cb0b457dcc Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff changeset
   993
end