author | wenzelm |
Sat, 20 Jun 2015 22:20:27 +0200 | |
changeset 60539 | f909f1a5cb22 |
parent 60533 | 1e7ccd864b62 |
child 60567 | 19c277ea65ae |
permissions | -rw-r--r-- |
30439 | 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 |
|
60533 | 5 |
section \<open>Dense linear order without endpoints |
6 |
and a quantifier elimination procedure in Ferrante and Rackoff style\<close> |
|
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
|
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 | 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 | 12 |
ML_file "langford_data.ML" |
13 |
ML_file "ferrante_rackoff_data.ML" |
|
14 |
||
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
|
15 |
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
|
16 |
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
|
17 |
|
49519 | 18 |
lemma less_not_permute[no_atp]: "\<not> (x < y \<and> y < x)" |
19 |
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
|
20 |
|
60539 | 21 |
lemma gather_simps[no_atp]: |
49519 | 22 |
"(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y) \<and> x < u \<and> P x) \<longleftrightarrow> |
23 |
(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> (insert u U). x < y) \<and> P x)" |
|
24 |
"(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y) \<and> l < x \<and> P x) \<longleftrightarrow> |
|
25 |
(\<exists>x. (\<forall>y \<in> (insert l L). y < x) \<and> (\<forall>y \<in> U. x < y) \<and> P x)" |
|
26 |
"(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y) \<and> x < u) \<longleftrightarrow> |
|
27 |
(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> (insert u U). x < y))" |
|
28 |
"(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y) \<and> l < x) \<longleftrightarrow> |
|
29 |
(\<exists>x. (\<forall>y \<in> (insert l L). y < x) \<and> (\<forall>y \<in> U. x < y))" |
|
30 |
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
|
31 |
|
60539 | 32 |
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
|
33 |
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
|
34 |
|
60533 | 35 |
text\<open>Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>-\<^sub>\<infinity>)"}\<close> |
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset
|
36 |
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
|
37 |
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
|
38 |
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
|
39 |
|
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset
|
40 |
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
|
41 |
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
|
42 |
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
|
43 |
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
|
44 |
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
|
45 |
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
|
46 |
|
60533 | 47 |
text\<open>Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>+\<^sub>\<infinity>)"}\<close> |
49519 | 48 |
lemma pinf_gt[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (t < x \<longleftrightarrow> True)" by auto |
49 |
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
|
50 |
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
|
51 |
|
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset
|
52 |
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
|
53 |
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
|
54 |
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
|
55 |
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
|
56 |
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
|
57 |
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
|
58 |
|
60539 | 59 |
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 |
60 |
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
|
61 |
by (auto simp add: le_less) |
60539 | 62 |
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 |
63 |
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 |
|
64 |
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 |
|
65 |
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 |
|
66 |
lemma nmi_P[no_atp]: "\<forall>x. ~P \<and> P \<longrightarrow> (\<exists>u\<in> U. u \<le> x)" by auto |
|
67 |
lemma nmi_conj[no_atp]: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow> (\<exists>u\<in> U. u \<le> x) ; |
|
68 |
\<forall>x. \<not>P2' \<and> P2 x \<longrightarrow> (\<exists>u\<in> U. u \<le> x)\<rbrakk> \<Longrightarrow> |
|
69 |
\<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow> (\<exists>u\<in> U. u \<le> x)" by auto |
|
70 |
lemma nmi_disj[no_atp]: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow> (\<exists>u\<in> U. u \<le> x) ; |
|
71 |
\<forall>x. \<not>P2' \<and> P2 x \<longrightarrow> (\<exists>u\<in> U. u \<le> x)\<rbrakk> \<Longrightarrow> |
|
72 |
\<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow> (\<exists>u\<in> U. u \<le> 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
|
73 |
|
60539 | 74 |
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) |
75 |
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 |
|
76 |
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 |
|
77 |
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 |
|
78 |
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 |
|
79 |
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 |
|
80 |
lemma npi_P[no_atp]: "\<forall>x. ~P \<and> P \<longrightarrow> (\<exists>u\<in> U. x \<le> u)" by auto |
|
81 |
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> |
|
82 |
\<Longrightarrow> \<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow> (\<exists>u\<in> U. x \<le> u)" by auto |
|
83 |
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> |
|
84 |
\<Longrightarrow> \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow> (\<exists>u\<in> U. x \<le> u)" 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
|
85 |
|
49519 | 86 |
lemma lin_dense_lt[no_atp]: |
87 |
"t \<in> U \<Longrightarrow> |
|
60539 | 88 |
\<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)" |
89 |
proof clarsimp |
|
49519 | 90 |
fix x l u y |
60539 | 91 |
assume tU: "t \<in> U" |
92 |
and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U" |
|
93 |
and lx: "l < x" |
|
94 |
and xu: "x < u" |
|
95 |
and px: "x < t" |
|
96 |
and ly: "l < y" |
|
97 |
and yu: "y < u" |
|
98 |
from tU noU ly yu have tny: "t \<noteq> y" by auto |
|
99 |
have False if H: "t < y" |
|
100 |
proof - |
|
101 |
from less_trans[OF lx px] less_trans[OF H yu] have "l < t \<and> t < u" |
|
102 |
by simp |
|
103 |
with tU noU show ?thesis |
|
104 |
by auto |
|
105 |
qed |
|
106 |
then have "\<not> t < y" |
|
107 |
by auto |
|
108 |
then have "y \<le> t" |
|
109 |
by (simp add: not_less) |
|
110 |
then show "y < t" |
|
111 |
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
|
112 |
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
|
113 |
|
49519 | 114 |
lemma lin_dense_gt[no_atp]: |
115 |
"t \<in> U \<Longrightarrow> |
|
60539 | 116 |
\<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)" |
117 |
proof clarsimp |
|
49519 | 118 |
fix x l u y |
60539 | 119 |
assume tU: "t \<in> U" |
120 |
and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U" |
|
121 |
and lx: "l < x" |
|
122 |
and xu: "x < u" |
|
123 |
and px: "t < x" |
|
124 |
and ly: "l < y" |
|
125 |
and yu: "y < u" |
|
126 |
from tU noU ly yu have tny: "t \<noteq> y" by auto |
|
127 |
have False if H: "y < t" |
|
128 |
proof - |
|
129 |
from less_trans[OF ly H] less_trans[OF px xu] have "l < t \<and> t < u" |
|
130 |
by simp |
|
131 |
with tU noU show ?thesis |
|
132 |
by auto |
|
133 |
qed |
|
134 |
then have "\<not> y < t" |
|
135 |
by auto |
|
136 |
then have "t \<le> y" |
|
137 |
by (auto simp add: not_less) |
|
138 |
then show "t < y" |
|
139 |
using tny by (simp add: less_le) |
|
49519 | 140 |
qed |
141 |
||
142 |
lemma lin_dense_le[no_atp]: |
|
143 |
"t \<in> U \<Longrightarrow> |
|
60539 | 144 |
\<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)" |
145 |
proof clarsimp |
|
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
|
146 |
fix x l u y |
60539 | 147 |
assume tU: "t \<in> U" |
148 |
and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U" |
|
149 |
and lx: "l < x" |
|
150 |
and xu: "x < u" |
|
151 |
and px: "x \<le> t" |
|
152 |
and ly: "l < y" |
|
153 |
and yu: "y < u" |
|
154 |
from tU noU ly yu have tny: "t \<noteq> y" by auto |
|
155 |
have False if H: "t < y" |
|
156 |
proof - |
|
49519 | 157 |
from less_le_trans[OF lx px] less_trans[OF H yu] |
158 |
have "l < t \<and> t < u" by simp |
|
60539 | 159 |
with tU noU show ?thesis by auto |
160 |
qed |
|
49519 | 161 |
then have "\<not> t < y" by auto |
162 |
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
|
163 |
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
|
164 |
|
49519 | 165 |
lemma lin_dense_ge[no_atp]: |
166 |
"t \<in> U \<Longrightarrow> |
|
60539 | 167 |
\<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)" |
168 |
proof clarsimp |
|
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
|
169 |
fix x l u y |
60539 | 170 |
assume tU: "t \<in> U" |
171 |
and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U" |
|
172 |
and lx: "l < x" |
|
173 |
and xu: "x < u" |
|
174 |
and px: "t \<le> x" |
|
175 |
and ly: "l < y" |
|
176 |
and yu: "y < u" |
|
177 |
from tU noU ly yu have tny: "t \<noteq> y" by auto |
|
178 |
have False if H: "y < t" |
|
179 |
proof - |
|
49519 | 180 |
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
|
181 |
have "l < t \<and> t < u" by simp |
60539 | 182 |
with tU noU show ?thesis by auto |
183 |
qed |
|
184 |
then have "\<not> y < t" by auto |
|
49519 | 185 |
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
|
186 |
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
|
187 |
|
49519 | 188 |
lemma lin_dense_eq[no_atp]: |
189 |
"t \<in> U \<Longrightarrow> |
|
60539 | 190 |
\<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)" |
49519 | 191 |
by auto |
192 |
||
193 |
lemma lin_dense_neq[no_atp]: |
|
194 |
"t \<in> U \<Longrightarrow> |
|
60539 | 195 |
\<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)" |
49519 | 196 |
by auto |
197 |
||
198 |
lemma lin_dense_P[no_atp]: |
|
60539 | 199 |
"\<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)" |
49519 | 200 |
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
|
201 |
|
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset
|
202 |
lemma lin_dense_conj[no_atp]: |
60539 | 203 |
"\<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 |
204 |
\<longrightarrow> (\<forall>y. l < y \<and> y < u \<longrightarrow> P1 y) ; |
|
205 |
\<forall>x l u. (\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U) \<and> l < x \<and> x < u \<and> P2 x |
|
206 |
\<longrightarrow> (\<forall>y. l < y \<and> y < u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow> |
|
207 |
\<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) |
|
208 |
\<longrightarrow> (\<forall>y. l < y \<and> y < u \<longrightarrow> (P1 y \<and> P2 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
|
209 |
by blast |
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset
|
210 |
lemma lin_dense_disj[no_atp]: |
60539 | 211 |
"\<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 |
212 |
\<longrightarrow> (\<forall>y. l < y \<and> y < u \<longrightarrow> P1 y) ; |
|
213 |
\<forall>x l u. (\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U) \<and> l < x \<and> x < u \<and> P2 x |
|
214 |
\<longrightarrow> (\<forall>y. l < y \<and> y < u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow> |
|
215 |
\<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) |
|
216 |
\<longrightarrow> (\<forall>y. l < y \<and> y < u \<longrightarrow> (P1 y \<or> P2 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
|
217 |
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
|
218 |
|
60539 | 219 |
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> |
220 |
\<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 | 221 |
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
|
222 |
|
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset
|
223 |
lemma finite_set_intervals[no_atp]: |
60539 | 224 |
assumes px: "P x" |
225 |
and lx: "l \<le> x" |
|
226 |
and xu: "x \<le> u" |
|
227 |
and linS: "l\<in> S" |
|
228 |
and uinS: "u \<in> S" |
|
229 |
and fS:"finite S" |
|
230 |
and lS: "\<forall>x\<in> S. l \<le> x" |
|
231 |
and Su: "\<forall>x\<in> S. x \<le> u" |
|
232 |
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 | 233 |
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
|
234 |
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
|
235 |
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
|
236 |
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
|
237 |
let ?b = "Min ?xM" |
60539 | 238 |
have MxS: "?Mx \<subseteq> S" |
239 |
by blast |
|
240 |
then have fMx: "finite ?Mx" |
|
241 |
using fS finite_subset by auto |
|
242 |
from lx linS have linMx: "l \<in> ?Mx" |
|
243 |
by blast |
|
244 |
then have Mxne: "?Mx \<noteq> {}" |
|
245 |
by blast |
|
246 |
have xMS: "?xM \<subseteq> S" |
|
247 |
by blast |
|
248 |
then have fxM: "finite ?xM" |
|
249 |
using fS finite_subset by auto |
|
250 |
from xu uinS have linxM: "u \<in> ?xM" |
|
251 |
by blast |
|
252 |
then have xMne: "?xM \<noteq> {}" |
|
253 |
by blast |
|
254 |
have ax: "?a \<le> x" |
|
255 |
using Mxne fMx by auto |
|
256 |
have xb: "x \<le> ?b" |
|
257 |
using xMne fxM by auto |
|
258 |
have "?a \<in> ?Mx" |
|
259 |
using Max_in[OF fMx Mxne] by simp then have ainS: "?a \<in> S" using MxS by blast |
|
260 |
have "?b \<in> ?xM" |
|
261 |
using Min_in[OF fxM xMne] by simp then have binS: "?b \<in> S" using xMS by blast |
|
262 |
have noy: "\<forall>y. ?a < y \<and> y < ?b \<longrightarrow> y \<notin> S" |
|
263 |
proof clarsimp |
|
49519 | 264 |
fix y |
265 |
assume ay: "?a < y" and yb: "y < ?b" and yS: "y \<in> S" |
|
60539 | 266 |
from yS have "y \<in> ?Mx \<or> y \<in> ?xM" by (auto simp add: linear) |
267 |
then show False |
|
268 |
proof |
|
49519 | 269 |
assume "y \<in> ?Mx" |
60539 | 270 |
then have "y \<le> ?a" using Mxne fMx by auto |
271 |
with ay show ?thesis by (simp add: not_le[symmetric]) |
|
272 |
next |
|
49519 | 273 |
assume "y \<in> ?xM" |
60539 | 274 |
then have "?b \<le> y" using xMne fxM by auto |
275 |
with yb show ?thesis by (simp add: not_le[symmetric]) |
|
276 |
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
|
277 |
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
|
278 |
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
|
279 |
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
|
280 |
|
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset
|
281 |
lemma finite_set_intervals2[no_atp]: |
60539 | 282 |
assumes px: "P x" |
283 |
and lx: "l \<le> x" |
|
284 |
and xu: "x \<le> u" |
|
285 |
and linS: "l\<in> S" |
|
286 |
and uinS: "u \<in> S" |
|
287 |
and fS: "finite S" |
|
288 |
and lS: "\<forall>x\<in> S. l \<le> x" |
|
289 |
and Su: "\<forall>x\<in> S. x \<le> u" |
|
290 |
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)" |
|
291 |
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
|
292 |
from finite_set_intervals[where P="P", OF px lx xu linS uinS fS lS Su] |
60539 | 293 |
obtain a and b where as: "a \<in> S" and bs: "b \<in> S" |
294 |
and noS: "\<forall>y. a < y \<and> y < b \<longrightarrow> y \<notin> S" |
|
295 |
and axb: "a \<le> x \<and> x \<le> b \<and> P x" |
|
296 |
by auto |
|
297 |
from axb have "x = a \<or> x = b \<or> (a < x \<and> x < b)" |
|
298 |
by (auto simp add: le_less) |
|
299 |
then show ?thesis |
|
300 |
using px as bs noS 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
|
301 |
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
|
302 |
|
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset
|
303 |
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
|
304 |
|
49519 | 305 |
|
60533 | 306 |
section \<open>The classical QE after Langford for dense linear orders\<close> |
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
|
307 |
|
53215
5e47c31c6f7c
renamed typeclass dense_linorder to unbounded_dense_linorder
hoelzl
parents:
53072
diff
changeset
|
308 |
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
|
309 |
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
|
310 |
|
49519 | 311 |
lemma interval_empty_iff: "{y. x < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z" |
27825 | 312 |
by (auto dest: dense) |
313 |
||
60539 | 314 |
lemma dlo_qe_bnds[no_atp]: |
315 |
assumes ne: "L \<noteq> {}" |
|
316 |
and neU: "U \<noteq> {}" |
|
317 |
and fL: "finite L" |
|
318 |
and fU: "finite U" |
|
319 |
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)" |
|
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 |
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
|
321 |
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
|
322 |
then obtain x where xL: "\<forall>y\<in>L. y < x" and xU: "\<forall>y\<in>U. x < y" by blast |
60539 | 323 |
have "l < u" if l: "l \<in> L" and u: "u \<in> U" for l u |
324 |
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
|
325 |
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
|
326 |
also have "x < u" using xU u by blast |
60539 | 327 |
finally show ?thesis . |
328 |
qed |
|
49519 | 329 |
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
|
330 |
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
|
331 |
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
|
332 |
let ?ML = "Max L" |
60539 | 333 |
let ?MU = "Min 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
|
334 |
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
|
335 |
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
|
336 |
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
|
337 |
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
|
338 |
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
|
339 |
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
|
340 |
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
|
341 |
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
|
342 |
|
60539 | 343 |
lemma dlo_qe_noub[no_atp]: |
344 |
assumes ne: "L \<noteq> {}" |
|
345 |
and fL: "finite L" |
|
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
|
346 |
shows "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> {}. x < y)) \<equiv> True" |
60539 | 347 |
proof (simp add: atomize_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
|
348 |
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
|
349 |
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
|
350 |
with M have "\<forall>x\<in>L. x < M" by (auto intro: le_less_trans) |
60539 | 351 |
then show "\<exists>x. \<forall>y\<in>L. y < 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
|
352 |
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
|
353 |
|
60539 | 354 |
lemma dlo_qe_nolb[no_atp]: |
355 |
assumes ne: "U \<noteq> {}" |
|
356 |
and fU: "finite 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
|
357 |
shows "(\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y \<in> U. x < y)) \<equiv> True" |
60539 | 358 |
proof (simp add: atomize_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
|
359 |
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
|
360 |
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
|
361 |
with M have "\<forall>x\<in>U. M < x" by (auto intro: less_le_trans) |
60539 | 362 |
then show "\<exists>x. \<forall>y\<in>U. x < y" 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
|
363 |
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
|
364 |
|
60539 | 365 |
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
|
366 |
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
|
367 |
|
60539 | 368 |
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
|
369 |
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
|
370 |
|
53215
5e47c31c6f7c
renamed typeclass dense_linorder to unbounded_dense_linorder
hoelzl
parents:
53072
diff
changeset
|
371 |
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
|
372 |
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
|
373 |
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
|
374 |
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
|
375 |
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
|
376 |
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
|
377 |
|
34cb0b457dcc
Old HOL/Dense_Linear_Order.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 |
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
|
379 |
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
|
380 |
|
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset
|
381 |
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
|
382 |
|
34cb0b457dcc
Old HOL/Dense_Linear_Order.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 |
(* FIXME: Move to HOL -- together with the conj_aci_rule in langford.ML *) |
41849 | 384 |
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
|
385 |
|
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset
|
386 |
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
|
387 |
|
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset
|
388 |
lemma nnf_simps[no_atp]: |
60539 | 389 |
"(\<not>(P \<and> Q)) = (\<not>P \<or> \<not>Q)" |
390 |
"(\<not>(P \<or> Q)) = (\<not>P \<and> \<not>Q)" |
|
391 |
"(P \<longrightarrow> Q) = (\<not>P \<or> Q)" |
|
392 |
"(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" |
|
393 |
"(\<not> \<not>(P)) = 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
|
394 |
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
|
395 |
|
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset
|
396 |
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
|
397 |
|
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset
|
398 |
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
|
399 |
|
48891 | 400 |
ML_file "langford.ML" |
60533 | 401 |
method_setup dlo = \<open> |
55848 | 402 |
Scan.succeed (SIMPLE_METHOD' o Langford.dlo_tac) |
60533 | 403 |
\<close> "Langford's algorithm for quantifier elimination in dense linear orders" |
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 |
|
60533 | 406 |
section \<open>Contructive dense linear orders yield QE for linear arithmetic over ordered Fields\<close> |
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
|
407 |
|
60533 | 408 |
text \<open>Linear order without upper bounds\<close> |
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
|
409 |
|
29509
1ff0f3f08a7b
migrated class package to new locale implementation
haftmann
parents:
29252
diff
changeset
|
410 |
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
|
411 |
begin |
49519 | 412 |
|
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
|
413 |
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
|
414 |
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
|
415 |
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
|
416 |
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
|
417 |
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
|
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 |
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
|
420 |
|
29509
1ff0f3f08a7b
migrated class package to new locale implementation
haftmann
parents:
29252
diff
changeset
|
421 |
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
|
422 |
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
|
423 |
begin |
49519 | 424 |
|
60539 | 425 |
lemma ge_ex[no_atp]: "\<exists>y. x \<sqsubseteq> y" |
426 |
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
|
427 |
|
60533 | 428 |
text \<open>Theorems for @{text "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>+\<^sub>\<infinity>)"}\<close> |
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset
|
429 |
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
|
430 |
assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')" |
60539 | 431 |
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
|
432 |
shows "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))" |
60539 | 433 |
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
|
434 |
from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')" |
60539 | 435 |
and z2: "\<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" |
436 |
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
|
437 |
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
|
438 |
from z have zz1: "z1 \<sqsubset> z" and zz2: "z2 \<sqsubset> z" by simp_all |
60539 | 439 |
have "(P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2')" if H: "z \<sqsubset> x" for x |
440 |
using less_trans[OF zz1 H] less_trans[OF zz2 H] z1 zz1 z2 zz2 by auto |
|
441 |
then show ?thesis 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
|
442 |
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
|
443 |
|
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset
|
444 |
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
|
445 |
assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')" |
49519 | 446 |
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
|
447 |
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
|
448 |
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
|
449 |
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
|
450 |
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
|
451 |
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
|
452 |
from z have zz1: "z1 \<sqsubset> z" and zz2: "z2 \<sqsubset> z" by simp_all |
60539 | 453 |
have "(P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2')" if H: "z \<sqsubset> x" for x |
454 |
using less_trans[OF zz1 H] less_trans[OF zz2 H] z1 zz1 z2 zz2 by auto |
|
455 |
then show ?thesis 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
|
456 |
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
|
457 |
|
60539 | 458 |
lemma pinf_ex[no_atp]: |
459 |
assumes ex: "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P1)" |
|
460 |
and p1: P1 |
|
461 |
shows "\<exists>x. P x" |
|
49519 | 462 |
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
|
463 |
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
|
464 |
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
|
465 |
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
|
466 |
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
|
467 |
|
34cb0b457dcc
Old HOL/Dense_Linear_Order.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 |
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
|
469 |
|
60533 | 470 |
text \<open>Linear order without upper bounds\<close> |
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
|
471 |
|
29509
1ff0f3f08a7b
migrated class package to new locale implementation
haftmann
parents:
29252
diff
changeset
|
472 |
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
|
473 |
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
|
474 |
begin |
49519 | 475 |
|
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset
|
476 |
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
|
477 |
|
34cb0b457dcc
Old HOL/Dense_Linear_Order.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 |
|
60533 | 479 |
text \<open>Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>-\<^sub>\<infinity>)"}\<close> |
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset
|
480 |
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
|
481 |
assumes ex1: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')" |
49519 | 482 |
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
|
483 |
shows "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))" |
60539 | 484 |
proof - |
485 |
from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')" |
|
486 |
and z2: "\<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')" |
|
487 |
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
|
488 |
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
|
489 |
from z have zz1: "z \<sqsubset> z1" and zz2: "z \<sqsubset> z2" by simp_all |
60539 | 490 |
have "(P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2')" if H: "x \<sqsubset> z" for x |
491 |
using less_trans[OF H zz1] less_trans[OF H zz2] z1 zz1 z2 zz2 by auto |
|
492 |
then show ?thesis 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
|
493 |
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
|
494 |
|
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset
|
495 |
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
|
496 |
assumes ex1: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')" |
49519 | 497 |
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
|
498 |
shows "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))" |
49519 | 499 |
proof - |
500 |
from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')" |
|
501 |
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
|
502 |
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
|
503 |
from z have zz1: "z \<sqsubset> z1" and zz2: "z \<sqsubset> z2" by simp_all |
60539 | 504 |
have "(P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2')" if H: "x \<sqsubset> z" for x |
505 |
using less_trans[OF H zz1] less_trans[OF H zz2] z1 zz1 z2 zz2 by auto |
|
506 |
then show ?thesis 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
|
507 |
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
|
508 |
|
49519 | 509 |
lemma minf_ex[no_atp]: |
510 |
assumes ex: "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P1)" |
|
511 |
and p1: P1 |
|
60539 | 512 |
shows "\<exists>x. P x" |
49519 | 513 |
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
|
514 |
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
|
515 |
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
|
516 |
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
|
517 |
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
|
518 |
|
34cb0b457dcc
Old HOL/Dense_Linear_Order.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 |
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
|
520 |
|
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset
|
521 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
522 |
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
|
523 |
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
|
524 |
assumes between_less: "less x y \<Longrightarrow> less x (between x y) \<and> less (between x y) y" |
49519 | 525 |
and between_same: "between x x = x" |
54868 | 526 |
begin |
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
|
527 |
|
60539 | 528 |
sublocale 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
|
529 |
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
|
530 |
using gt_ex lt_ex between_less |
49519 | 531 |
apply auto |
532 |
apply (rule_tac x="between x y" in exI) |
|
533 |
apply simp |
|
534 |
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
|
535 |
|
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset
|
536 |
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
|
537 |
assumes fU: "finite U" |
60539 | 538 |
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 |
539 |
\<longrightarrow> (\<forall>y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P y )" |
|
540 |
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')" |
|
541 |
and nmi: "\<not> MP" and npi: "\<not> PP" and ex: "\<exists>x. P x" |
|
542 |
shows "\<exists>u\<in> U. \<exists>u' \<in> U. P (between u u')" |
|
49519 | 543 |
proof - |
60539 | 544 |
from ex obtain x where px: "P x" |
545 |
by blast |
|
546 |
from px nmi npi nmpiU have "\<exists>u\<in> U. \<exists>u' \<in> U. u \<sqsubseteq> x \<and> x \<sqsubseteq> u'" |
|
547 |
by auto |
|
548 |
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'" |
|
549 |
by auto |
|
550 |
from uU have Une: "U \<noteq> {}" |
|
551 |
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
|
552 |
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
|
553 |
let ?u = "linorder.Max less_eq U" |
60539 | 554 |
have linM: "?l \<in> U" |
555 |
using fU Une by simp |
|
556 |
have uinM: "?u \<in> U" |
|
557 |
using fU Une by simp |
|
558 |
have lM: "\<forall>t\<in> U. ?l \<sqsubseteq> t" |
|
559 |
using Une fU by auto |
|
560 |
have Mu: "\<forall>t\<in> U. t \<sqsubseteq> ?u" |
|
561 |
using Une fU by auto |
|
562 |
have th: "?l \<sqsubseteq> u" |
|
563 |
using uU Une lM 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
|
564 |
from order_trans[OF th ux] have lx: "?l \<sqsubseteq> x" . |
60539 | 565 |
have th: "u' \<sqsubseteq> ?u" |
566 |
using uU' Une Mu 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
|
567 |
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
|
568 |
from finite_set_intervals2[where P="P",OF px lx xu linM uinM fU lM Mu] |
60539 | 569 |
consider u where "u \<in> U" "P u" | |
570 |
t1 t2 where "t1 \<in> U" "t2 \<in> U" "\<forall>y. t1 \<sqsubset> y \<and> y \<sqsubset> t2 \<longrightarrow> y \<notin> U" "t1 \<sqsubset> x" "x \<sqsubset> t2" "P x" |
|
571 |
by blast |
|
572 |
then show ?thesis |
|
573 |
proof cases |
|
574 |
case 1 |
|
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
|
575 |
have "between u u = u" by (simp add: between_same) |
60539 | 576 |
with 1 have "P (between u u)" by simp |
577 |
with 1 show ?thesis by blast |
|
578 |
next |
|
579 |
case 2 |
|
580 |
note t1M = \<open>t1 \<in> U\<close> and t2M = \<open>t2\<in> U\<close> |
|
581 |
and noM = \<open>\<forall>y. t1 \<sqsubset> y \<and> y \<sqsubset> t2 \<longrightarrow> y \<notin> U\<close> |
|
582 |
and t1x = \<open>t1 \<sqsubset> x\<close> and xt2 = \<open>x \<sqsubset> t2\<close> |
|
583 |
and px = \<open>P x\<close> |
|
49519 | 584 |
from less_trans[OF t1x xt2] have t1t2: "t1 \<sqsubset> t2" . |
585 |
let ?u = "between t1 t2" |
|
586 |
from between_less t1t2 have t1lu: "t1 \<sqsubset> ?u" and ut2: "?u \<sqsubset> t2" by auto |
|
587 |
from lin_dense noM t1x xt2 px t1lu ut2 have "P ?u" by blast |
|
60539 | 588 |
with t1M t2M show ?thesis by blast |
589 |
qed |
|
49519 | 590 |
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
|
591 |
|
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset
|
592 |
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
|
593 |
assumes fU: "finite U" |
60539 | 594 |
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 |
595 |
\<longrightarrow> (\<forall>y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P y )" |
|
596 |
and nmibnd: "\<forall>x. \<not> MP \<and> P x \<longrightarrow> (\<exists>u\<in> U. u \<sqsubseteq> x)" |
|
597 |
and npibnd: "\<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists>u\<in> U. x \<sqsubseteq> u)" |
|
49519 | 598 |
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)" |
60539 | 599 |
shows "(\<exists>x. P x) \<equiv> (MP \<or> PP \<or> (\<exists>u \<in> U. \<exists>u'\<in> U. P (between u 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
|
600 |
(is "_ \<equiv> (_ \<or> _ \<or> ?F)" is "?E \<equiv> ?D") |
49519 | 601 |
proof - |
60539 | 602 |
have "?E \<longleftrightarrow> ?D" |
603 |
proof |
|
604 |
show ?D if px: ?E |
|
605 |
proof - |
|
606 |
consider "MP \<or> PP" | "\<not> MP" "\<not> PP" by blast |
|
607 |
then show ?thesis |
|
608 |
proof cases |
|
609 |
case 1 |
|
610 |
then show ?thesis by blast |
|
611 |
next |
|
612 |
case 2 |
|
613 |
from npmibnd[OF nmibnd npibnd] |
|
614 |
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')" . |
|
615 |
from rinf_U[OF fU lin_dense nmpiU \<open>\<not> MP\<close> \<open>\<not> PP\<close> px] show ?thesis |
|
616 |
by blast |
|
617 |
qed |
|
618 |
qed |
|
619 |
show ?E if ?D |
|
620 |
proof - |
|
621 |
from that consider MP | PP | ?F by blast |
|
622 |
then show ?thesis |
|
623 |
proof cases |
|
624 |
case 1 |
|
625 |
show ?thesis by (rule minf_ex[OF mi 1]) |
|
626 |
next |
|
627 |
case 2 |
|
628 |
show ?thesis by (rule pinf_ex[OF pi 2]) |
|
629 |
next |
|
630 |
case 3 |
|
631 |
then show ?thesis by blast |
|
632 |
qed |
|
633 |
qed |
|
634 |
qed |
|
635 |
then show "?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
|
636 |
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
|
637 |
|
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset
|
638 |
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
|
639 |
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
|
640 |
|
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset
|
641 |
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
|
642 |
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
|
643 |
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
|
644 |
|
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset
|
645 |
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
|
646 |
by (rule constr_dense_linorder_axioms) |
49519 | 647 |
|
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset
|
648 |
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
|
649 |
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
|
650 |
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
|
651 |
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
|
652 |
|
34cb0b457dcc
Old HOL/Dense_Linear_Order.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 |
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
|
654 |
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
|
655 |
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
|
656 |
|
60533 | 657 |
declaration \<open> |
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
|
658 |
let |
49519 | 659 |
fun simps phi = map (Morphism.thm phi) [@{thm "not_less"}, @{thm "not_le"}] |
660 |
fun generic_whatis phi = |
|
661 |
let |
|
662 |
val [lt, le] = map (Morphism.term phi) [@{term "op \<sqsubset>"}, @{term "op \<sqsubseteq>"}] |
|
663 |
fun h x t = |
|
59582 | 664 |
case Thm.term_of t of |
49519 | 665 |
Const(@{const_name HOL.eq}, _)$y$z => |
59582 | 666 |
if Thm.term_of x aconv y then Ferrante_Rackoff_Data.Eq |
49519 | 667 |
else Ferrante_Rackoff_Data.Nox |
668 |
| @{term "Not"}$(Const(@{const_name HOL.eq}, _)$y$z) => |
|
59582 | 669 |
if Thm.term_of x aconv y then Ferrante_Rackoff_Data.NEq |
49519 | 670 |
else Ferrante_Rackoff_Data.Nox |
671 |
| b$y$z => if Term.could_unify (b, lt) then |
|
59582 | 672 |
if Thm.term_of x aconv y then Ferrante_Rackoff_Data.Lt |
673 |
else if Thm.term_of x aconv z then Ferrante_Rackoff_Data.Gt |
|
49519 | 674 |
else Ferrante_Rackoff_Data.Nox |
675 |
else if Term.could_unify (b, le) then |
|
59582 | 676 |
if Thm.term_of x aconv y then Ferrante_Rackoff_Data.Le |
677 |
else if Thm.term_of x aconv z then Ferrante_Rackoff_Data.Ge |
|
49519 | 678 |
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
|
679 |
else Ferrante_Rackoff_Data.Nox |
49519 | 680 |
| _ => Ferrante_Rackoff_Data.Nox |
681 |
in h end |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49756
diff
changeset
|
682 |
fun ss phi = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49756
diff
changeset
|
683 |
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
|
684 |
in |
49519 | 685 |
Ferrante_Rackoff_Data.funs @{thm "ferrack_axiom"} |
686 |
{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
|
687 |
end |
60533 | 688 |
\<close> |
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
|
689 |
|
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset
|
690 |
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
|
691 |
|
48891 | 692 |
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
|
693 |
|
60533 | 694 |
method_setup ferrack = \<open> |
30549 | 695 |
Scan.succeed (SIMPLE_METHOD' o FerranteRackoff.dlo_tac) |
60533 | 696 |
\<close> "Ferrante and Rackoff's algorithm for quantifier elimination in dense linear orders" |
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 |
|
49519 | 698 |
|
60533 | 699 |
subsection \<open>Ferrante and Rackoff algorithm over ordered fields\<close> |
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
|
700 |
|
60539 | 701 |
lemma neg_prod_lt: |
702 |
fixes c :: "'a::linordered_field" |
|
703 |
assumes "c < 0" |
|
704 |
shows "c * x < 0 \<equiv> x > 0" |
|
49519 | 705 |
proof - |
60539 | 706 |
have "c * x < 0 \<longleftrightarrow> 0 / c < x" |
707 |
by (simp only: neg_divide_less_eq[OF \<open>c < 0\<close>] algebra_simps) |
|
708 |
also have "\<dots> \<longleftrightarrow> 0 < x" by simp |
|
709 |
finally show "PROP ?thesis" 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
|
710 |
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
|
711 |
|
60539 | 712 |
lemma pos_prod_lt: |
713 |
fixes c :: "'a::linordered_field" |
|
714 |
assumes "c > 0" |
|
715 |
shows "c * x < 0 \<equiv> x < 0" |
|
49519 | 716 |
proof - |
60539 | 717 |
have "c * x < 0 \<longleftrightarrow> 0 /c > x" |
718 |
by (simp only: pos_less_divide_eq[OF \<open>c > 0\<close>] algebra_simps) |
|
719 |
also have "\<dots> \<longleftrightarrow> 0 > x" by simp |
|
720 |
finally show "PROP ?thesis" 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
|
721 |
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
|
722 |
|
60539 | 723 |
lemma neg_prod_sum_lt: |
724 |
fixes c :: "'a::linordered_field" |
|
725 |
assumes "c < 0" |
|
726 |
shows "c * x + t < 0 \<equiv> x > (- 1 / c) * t" |
|
49519 | 727 |
proof - |
60539 | 728 |
have "c * x + t < 0 \<longleftrightarrow> c * x < - t" |
729 |
by (subst less_iff_diff_less_0 [of "c * x" "- t"]) simp |
|
730 |
also have "\<dots> \<longleftrightarrow> - t / c < x" |
|
731 |
by (simp only: neg_divide_less_eq[OF \<open>c < 0\<close>] algebra_simps) |
|
732 |
also have "\<dots> \<longleftrightarrow> (- 1 / c) * t < x" by simp |
|
733 |
finally show "PROP ?thesis" 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
|
734 |
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
|
735 |
|
60539 | 736 |
lemma pos_prod_sum_lt: |
737 |
fixes c :: "'a::linordered_field" |
|
738 |
assumes "c > 0" |
|
739 |
shows "c * x + t < 0 \<equiv> x < (- 1 / c) * t" |
|
49519 | 740 |
proof - |
60539 | 741 |
have "c * x + t < 0 \<longleftrightarrow> c * x < - t" |
742 |
by (subst less_iff_diff_less_0 [of "c * x" "- t"]) simp |
|
743 |
also have "\<dots> \<longleftrightarrow> - t / c > x" |
|
744 |
by (simp only: pos_less_divide_eq[OF \<open>c > 0\<close>] algebra_simps) |
|
745 |
also have "\<dots> \<longleftrightarrow> (- 1 / c) * t > x" by simp |
|
746 |
finally show "PROP ?thesis" 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
|
747 |
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
|
748 |
|
60539 | 749 |
lemma sum_lt: |
750 |
fixes x :: "'a::ordered_ab_group_add" |
|
751 |
shows "x + t < 0 \<equiv> 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
|
752 |
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
|
753 |
|
60539 | 754 |
lemma neg_prod_le: |
755 |
fixes c :: "'a::linordered_field" |
|
756 |
assumes "c < 0" |
|
757 |
shows "c * x \<le> 0 \<equiv> x \<ge> 0" |
|
49519 | 758 |
proof - |
60539 | 759 |
have "c * x \<le> 0 \<longleftrightarrow> 0 / c \<le> x" |
760 |
by (simp only: neg_divide_le_eq[OF \<open>c < 0\<close>] algebra_simps) |
|
761 |
also have "\<dots> \<longleftrightarrow> 0 \<le> x" by simp |
|
762 |
finally show "PROP ?thesis" 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
|
763 |
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
|
764 |
|
60539 | 765 |
lemma pos_prod_le: |
766 |
fixes c :: "'a::linordered_field" |
|
767 |
assumes "c > 0" |
|
768 |
shows "c * x \<le> 0 \<equiv> x \<le> 0" |
|
49519 | 769 |
proof - |
60539 | 770 |
have "c * x \<le> 0 \<longleftrightarrow> 0 / c \<ge> x" |
771 |
by (simp only: pos_le_divide_eq[OF \<open>c > 0\<close>] algebra_simps) |
|
772 |
also have "\<dots> \<longleftrightarrow> 0 \<ge> x" by simp |
|
773 |
finally show "PROP ?thesis" by simp |
|
774 |
qed |
|
775 |
||
776 |
lemma neg_prod_sum_le: |
|
777 |
fixes c :: "'a::linordered_field" |
|
778 |
assumes "c < 0" |
|
779 |
shows "c * x + t \<le> 0 \<equiv> x \<ge> (- 1 / c) * t" |
|
780 |
proof - |
|
781 |
have "c * x + t \<le> 0 \<longleftrightarrow> c * x \<le> -t" |
|
782 |
by (subst le_iff_diff_le_0 [of "c*x" "-t"]) simp |
|
783 |
also have "\<dots> \<longleftrightarrow> - t / c \<le> x" |
|
784 |
by (simp only: neg_divide_le_eq[OF \<open>c < 0\<close>] algebra_simps) |
|
785 |
also have "\<dots> \<longleftrightarrow> (- 1 / c) * t \<le> x" by simp |
|
786 |
finally show "PROP ?thesis" 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
|
787 |
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
|
788 |
|
60539 | 789 |
lemma pos_prod_sum_le: |
790 |
fixes c :: "'a::linordered_field" |
|
791 |
assumes "c > 0" |
|
792 |
shows "c * x + t \<le> 0 \<equiv> x \<le> (- 1 / c) * t" |
|
49519 | 793 |
proof - |
60539 | 794 |
have "c * x + t \<le> 0 \<longleftrightarrow> c * x \<le> - t" |
795 |
by (subst le_iff_diff_le_0 [of "c*x" "-t"]) simp |
|
796 |
also have "\<dots> \<longleftrightarrow> - t / c \<ge> x" |
|
797 |
by (simp only: pos_le_divide_eq[OF \<open>c > 0\<close>] algebra_simps) |
|
798 |
also have "\<dots> \<longleftrightarrow> (- 1 / c) * t \<ge> x" by simp |
|
799 |
finally show "PROP ?thesis" 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
|
800 |
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
|
801 |
|
60539 | 802 |
lemma sum_le: |
803 |
fixes x :: "'a::ordered_ab_group_add" |
|
804 |
shows "x + t \<le> 0 \<equiv> x \<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
|
805 |
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
|
806 |
|
60539 | 807 |
lemma nz_prod_eq: |
808 |
fixes c :: "'a::linordered_field" |
|
809 |
assumes "c \<noteq> 0" |
|
810 |
shows "c * x = 0 \<equiv> x = 0" |
|
811 |
using assms by simp |
|
49519 | 812 |
|
60539 | 813 |
lemma nz_prod_sum_eq: |
814 |
fixes c :: "'a::linordered_field" |
|
815 |
assumes "c \<noteq> 0" |
|
816 |
shows "c * x + t = 0 \<equiv> x = (- 1/c) * t" |
|
49519 | 817 |
proof - |
60539 | 818 |
have "c * x + t = 0 \<longleftrightarrow> c * x = - t" |
819 |
by (subst eq_iff_diff_eq_0 [of "c*x" "-t"]) simp |
|
820 |
also have "\<dots> \<longleftrightarrow> x = - t / c" |
|
821 |
by (simp only: nonzero_eq_divide_eq[OF \<open>c \<noteq> 0\<close>] algebra_simps) |
|
822 |
finally show "PROP ?thesis" 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
|
823 |
qed |
49519 | 824 |
|
60539 | 825 |
lemma sum_eq: |
826 |
fixes x :: "'a::ordered_ab_group_add" |
|
827 |
shows "x + t = 0 \<equiv> 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
|
828 |
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
|
829 |
|
34cb0b457dcc
Old HOL/Dense_Linear_Order.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 |
|
35043
07dbdf60d5ad
dropped accidental duplication of "lin" prefix from cs. 108662d50512
haftmann
parents:
35028
diff
changeset
|
831 |
interpretation class_dense_linordered_field: constr_dense_linorder |
60539 | 832 |
"op \<le>" "op <" "\<lambda>x y. 1/2 * ((x::'a::linordered_field) + y)" |
49519 | 833 |
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
|
834 |
|
60539 | 835 |
declaration \<open> |
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
|
836 |
let |
49519 | 837 |
fun earlier [] x y = false |
838 |
| earlier (h::t) x y = |
|
839 |
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
|
840 |
|
49519 | 841 |
fun dest_frac ct = |
59582 | 842 |
case Thm.term_of ct of |
60352
d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
59586
diff
changeset
|
843 |
Const (@{const_name Rings.divide},_) $ a $ b=> |
49519 | 844 |
Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b)) |
845 |
| Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd) |
|
846 |
| 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
|
847 |
|
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset
|
848 |
fun mk_frac phi cT x = |
49519 | 849 |
let val (a, b) = Rat.quotient_of_rat x |
850 |
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
|
851 |
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
|
852 |
(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
|
853 |
(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
|
854 |
(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
|
855 |
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
|
856 |
|
59582 | 857 |
fun whatis x ct = case Thm.term_of ct of |
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
858 |
Const(@{const_name Groups.plus}, _)$(Const(@{const_name Groups.times},_)$_$y)$_ => |
59582 | 859 |
if y aconv Thm.term_of x then ("c*x+t",[(funpow 2 Thm.dest_arg1) ct, Thm.dest_arg 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
|
860 |
else ("Nox",[]) |
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
861 |
| Const(@{const_name Groups.plus}, _)$y$_ => |
59582 | 862 |
if y aconv Thm.term_of x then ("x+t",[Thm.dest_arg 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
|
863 |
else ("Nox",[]) |
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
864 |
| Const(@{const_name Groups.times}, _)$_$y => |
59582 | 865 |
if y aconv Thm.term_of x then ("c*x",[Thm.dest_arg1 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
|
866 |
else ("Nox",[]) |
59582 | 867 |
| t => if t aconv Thm.term_of x then ("x",[]) else ("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
|
868 |
|
36945 | 869 |
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
|
870 |
| xnormalize_conv ctxt (vs as (x::_)) ct = |
59582 | 871 |
case Thm.term_of ct of |
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
872 |
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
|
873 |
(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
|
874 |
("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
|
875 |
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
|
876 |
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
|
877 |
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
|
878 |
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
|
879 |
val neg = cr </ Rat.zero |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49756
diff
changeset
|
880 |
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
|
881 |
(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
|
882 |
(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
|
883 |
else Thm.apply (Thm.apply clt cz) c)) |
36945 | 884 |
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI |
59586 | 885 |
val th = Thm.implies_elim (instantiate' [SOME (Thm.ctyp_of_cterm 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
|
886 |
(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
|
887 |
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
|
888 |
(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
|
889 |
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
|
890 |
| ("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
|
891 |
let |
59586 | 892 |
val T = Thm.ctyp_of_cterm 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
|
893 |
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
|
894 |
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
|
895 |
(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
|
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 |
| ("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
|
898 |
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
|
899 |
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
|
900 |
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
|
901 |
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
|
902 |
val neg = cr </ Rat.zero |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49756
diff
changeset
|
903 |
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
|
904 |
(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
|
905 |
(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
|
906 |
else Thm.apply (Thm.apply clt cz) c)) |
36945 | 907 |
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI |
59586 | 908 |
val th = Thm.implies_elim (instantiate' [SOME (Thm.ctyp_of_cterm 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
|
909 |
(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
|
910 |
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
|
911 |
in rth end |
36945 | 912 |
| _ => 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
|
913 |
|
34cb0b457dcc
Old HOL/Dense_Linear_Order.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 |
|
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
915 |
| 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
|
916 |
(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
|
917 |
("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
|
918 |
let |
59586 | 919 |
val T = Thm.ctyp_of_cterm 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
|
920 |
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
|
921 |
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
|
922 |
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
|
923 |
val neg = cr </ Rat.zero |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49756
diff
changeset
|
924 |
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
|
925 |
(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
|
926 |
(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
|
927 |
else Thm.apply (Thm.apply clt cz) c)) |
36945 | 928 |
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI |
929 |
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
|
930 |
(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
|
931 |
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
|
932 |
(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
|
933 |
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
|
934 |
| ("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
|
935 |
let |
59586 | 936 |
val T = Thm.ctyp_of_cterm 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
|
937 |
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
|
938 |
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
|
939 |
(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
|
940 |
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
|
941 |
| ("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
|
942 |
let |
59586 | 943 |
val T = Thm.ctyp_of_cterm 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
|
944 |
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
|
945 |
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
|
946 |
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
|
947 |
val neg = cr </ Rat.zero |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49756
diff
changeset
|
948 |
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
|
949 |
(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
|
950 |
(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
|
951 |
else Thm.apply (Thm.apply clt cz) c)) |
36945 | 952 |
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI |
59586 | 953 |
val th = Thm.implies_elim (instantiate' [SOME (Thm.ctyp_of_cterm 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
|
954 |
(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
|
955 |
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
|
956 |
in rth end |
36945 | 957 |
| _ => 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
|
958 |
|
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38549
diff
changeset
|
959 |
| 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
|
960 |
(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
|
961 |
("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
|
962 |
let |
59586 | 963 |
val T = Thm.ctyp_of_cterm 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
|
964 |
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
|
965 |
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
|
966 |
val cz = Thm.dest_arg ct |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49756
diff
changeset
|
967 |
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
|
968 |
(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
|
969 |
(Thm.apply @{cterm "Not"} (Thm.apply (Thm.apply ceq c) cz))) |
36945 | 970 |
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI |
971 |
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
|
972 |
(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
|
973 |
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
|
974 |
(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
|
975 |
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
|
976 |
| ("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
|
977 |
let |
59586 | 978 |
val T = Thm.ctyp_of_cterm 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
|
979 |
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
|
980 |
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
|
981 |
(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
|
982 |
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
|
983 |
| ("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
|
984 |
let |
59586 | 985 |
val T = Thm.ctyp_of_cterm 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
|
986 |
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
|
987 |
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
|
988 |
val cz = Thm.dest_arg ct |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49756
diff
changeset
|
989 |
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
|
990 |
(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
|
991 |
(Thm.apply @{cterm "Not"} (Thm.apply (Thm.apply ceq c) cz))) |
36945 | 992 |
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI |
993 |
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
|
994 |
(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
|
995 |
in rth end |
36945 | 996 |
| _ => 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
|
997 |
|
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset
|
998 |
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
|
999 |
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
|
1000 |
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
|
1001 |
val eq_iff_diff_eq_0 = mk_meta_eq @{thm "eq_iff_diff_eq_0"} |
52090 | 1002 |
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
|
1003 |
in |
59582 | 1004 |
fun field_isolate_conv phi ctxt vs ct = case Thm.term_of ct of |
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35084
diff
changeset
|
1005 |
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
|
1006 |
let val (ca,cb) = Thm.dest_binop ct |
59586 | 1007 |
val T = Thm.ctyp_of_cterm ca |
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
|
1008 |
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
|
1009 |
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
|
1010 |
(Conv.arg_conv (Conv.arg1_conv |
52090 | 1011 |
(Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier vs)))) th |
36945 | 1012 |
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
|
1013 |
in rth end |
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35084
diff
changeset
|
1014 |
| 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
|
1015 |
let val (ca,cb) = Thm.dest_binop ct |
59586 | 1016 |
val T = Thm.ctyp_of_cterm ca |
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
|
1017 |
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
|
1018 |
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
|
1019 |
(Conv.arg_conv (Conv.arg1_conv |
52090 | 1020 |
(Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier vs)))) th |
36945 | 1021 |
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
|
1022 |
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
|
1023 |
|
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38549
diff
changeset
|
1024 |
| 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
|
1025 |
let val (ca,cb) = Thm.dest_binop ct |
59586 | 1026 |
val T = Thm.ctyp_of_cterm ca |
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
|
1027 |
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
|
1028 |
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
|
1029 |
(Conv.arg_conv (Conv.arg1_conv |
52090 | 1030 |
(Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier vs)))) th |
36945 | 1031 |
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
|
1032 |
in rth end |
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38549
diff
changeset
|
1033 |
| @{term "Not"} $(Const(@{const_name HOL.eq},_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct |
36945 | 1034 |
| _ => 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
|
1035 |
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
|
1036 |
|
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset
|
1037 |
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
|
1038 |
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
|
1039 |
fun h x t = |
59582 | 1040 |
case Thm.term_of t of |
1041 |
Const(@{const_name HOL.eq}, _)$y$z => |
|
1042 |
if Thm.term_of x aconv y then Ferrante_Rackoff_Data.Eq |
|
1043 |
else Ferrante_Rackoff_Data.Nox |
|
1044 |
| @{term "Not"}$(Const(@{const_name HOL.eq}, _)$y$z) => |
|
1045 |
if Thm.term_of x aconv y then Ferrante_Rackoff_Data.NEq |
|
1046 |
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
|
1047 |
| Const(@{const_name Orderings.less},_)$y$z => |
59582 | 1048 |
if Thm.term_of x aconv y then Ferrante_Rackoff_Data.Lt |
1049 |
else if Thm.term_of x aconv z then Ferrante_Rackoff_Data.Gt |
|
1050 |
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
|
1051 |
| Const (@{const_name Orderings.less_eq},_)$y$z => |
59582 | 1052 |
if Thm.term_of x aconv y then Ferrante_Rackoff_Data.Le |
1053 |
else if Thm.term_of x aconv z then Ferrante_Rackoff_Data.Ge |
|
1054 |
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
|
1055 |
| _ => 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
|
1056 |
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
|
1057 |
fun class_field_ss phi = |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49756
diff
changeset
|
1058 |
simpset_of (put_simpset HOL_basic_ss @{context} |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49756
diff
changeset
|
1059 |
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
|
1060 |
|> 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
|
1061 |
|
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset
|
1062 |
in |
35043
07dbdf60d5ad
dropped accidental duplication of "lin" prefix from cs. 108662d50512
haftmann
parents:
35028
diff
changeset
|
1063 |
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
|
1064 |
{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
|
1065 |
end |
60533 | 1066 |
\<close> |
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset
|
1067 |
|
60539 | 1068 |
end |