1 (* Title : HOL/Dense_Linear_Order.thy |
|
2 Author : Amine Chaieb, TU Muenchen |
|
3 *) |
|
4 |
|
5 header {* Dense linear order without endpoints |
|
6 and a quantifier elimination procedure in Ferrante and Rackoff style *} |
|
7 |
|
8 theory Dense_Linear_Order |
|
9 imports Plain Groebner_Basis Main |
|
10 uses |
|
11 "~~/src/HOL/Tools/Qelim/langford_data.ML" |
|
12 "~~/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML" |
|
13 ("~~/src/HOL/Tools/Qelim/langford.ML") |
|
14 ("~~/src/HOL/Tools/Qelim/ferrante_rackoff.ML") |
|
15 begin |
|
16 |
|
17 setup {* Langford_Data.setup #> Ferrante_Rackoff_Data.setup *} |
|
18 |
|
19 context linorder |
|
20 begin |
|
21 |
|
22 lemma less_not_permute[noatp]: "\<not> (x < y \<and> y < x)" by (simp add: not_less linear) |
|
23 |
|
24 lemma gather_simps[noatp]: |
|
25 shows |
|
26 "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y) \<and> x < u \<and> P x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> (insert u U). x < y) \<and> P x)" |
|
27 and "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y) \<and> l < x \<and> P x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> (insert l L). y < x) \<and> (\<forall>y \<in> U. x < y) \<and> P x)" |
|
28 "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y) \<and> x < u) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> (insert u U). x < y))" |
|
29 and "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y) \<and> l < x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> (insert l L). y < x) \<and> (\<forall>y \<in> U. x < y))" by auto |
|
30 |
|
31 lemma |
|
32 gather_start[noatp]: "(\<exists>x. P x) \<equiv> (\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y\<in> {}. x < y) \<and> P x)" |
|
33 by simp |
|
34 |
|
35 text{* Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"}*} |
|
36 lemma minf_lt[noatp]: "\<exists>z . \<forall>x. x < z \<longrightarrow> (x < t \<longleftrightarrow> True)" by auto |
|
37 lemma minf_gt[noatp]: "\<exists>z . \<forall>x. x < z \<longrightarrow> (t < x \<longleftrightarrow> False)" |
|
38 by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le) |
|
39 |
|
40 lemma minf_le[noatp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<le> t \<longleftrightarrow> True)" by (auto simp add: less_le) |
|
41 lemma minf_ge[noatp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (t \<le> x \<longleftrightarrow> False)" |
|
42 by (auto simp add: less_le not_less not_le) |
|
43 lemma minf_eq[noatp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto |
|
44 lemma minf_neq[noatp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto |
|
45 lemma minf_P[noatp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (P \<longleftrightarrow> P)" by blast |
|
46 |
|
47 text{* Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"}*} |
|
48 lemma pinf_gt[noatp]: "\<exists>z . \<forall>x. z < x \<longrightarrow> (t < x \<longleftrightarrow> True)" by auto |
|
49 lemma pinf_lt[noatp]: "\<exists>z . \<forall>x. z < x \<longrightarrow> (x < t \<longleftrightarrow> False)" |
|
50 by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le) |
|
51 |
|
52 lemma pinf_ge[noatp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (t \<le> x \<longleftrightarrow> True)" by (auto simp add: less_le) |
|
53 lemma pinf_le[noatp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x \<le> t \<longleftrightarrow> False)" |
|
54 by (auto simp add: less_le not_less not_le) |
|
55 lemma pinf_eq[noatp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto |
|
56 lemma pinf_neq[noatp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto |
|
57 lemma pinf_P[noatp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (P \<longleftrightarrow> P)" by blast |
|
58 |
|
59 lemma nmi_lt[noatp]: "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[noatp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t < x \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" |
|
61 by (auto simp add: le_less) |
|
62 lemma nmi_le[noatp]: "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[noatp]: "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[noatp]: "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[noatp]: "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[noatp]: "\<forall> x. ~P \<and> P \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto |
|
67 lemma nmi_conj[noatp]: "\<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[noatp]: "\<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 |
|
73 |
|
74 lemma npi_lt[noatp]: "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[noatp]: "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[noatp]: "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[noatp]: "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[noatp]: "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[noatp]: "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[noatp]: "\<forall> x. ~P \<and> P \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by auto |
|
81 lemma npi_conj[noatp]: "\<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[noatp]: "\<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 |
|
85 |
|
86 lemma lin_dense_lt[noatp]: "t \<in> U \<Longrightarrow> \<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)" |
|
87 proof(clarsimp) |
|
88 fix x l u y assume tU: "t \<in> U" and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x" |
|
89 and xu: "x<u" and px: "x < t" and ly: "l<y" and yu:"y < u" |
|
90 from tU noU ly yu have tny: "t\<noteq>y" by auto |
|
91 {assume H: "t < y" |
|
92 from less_trans[OF lx px] less_trans[OF H yu] |
|
93 have "l < t \<and> t < u" by simp |
|
94 with tU noU have "False" by auto} |
|
95 hence "\<not> t < y" by auto hence "y \<le> t" by (simp add: not_less) |
|
96 thus "y < t" using tny by (simp add: less_le) |
|
97 qed |
|
98 |
|
99 lemma lin_dense_gt[noatp]: "t \<in> U \<Longrightarrow> \<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)" |
|
100 proof(clarsimp) |
|
101 fix x l u y |
|
102 assume tU: "t \<in> U" and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x" and xu: "x<u" |
|
103 and px: "t < x" and ly: "l<y" and yu:"y < u" |
|
104 from tU noU ly yu have tny: "t\<noteq>y" by auto |
|
105 {assume H: "y< t" |
|
106 from less_trans[OF ly H] less_trans[OF px xu] have "l < t \<and> t < u" by simp |
|
107 with tU noU have "False" by auto} |
|
108 hence "\<not> y<t" by auto hence "t \<le> y" by (auto simp add: not_less) |
|
109 thus "t < y" using tny by (simp add:less_le) |
|
110 qed |
|
111 |
|
112 lemma lin_dense_le[noatp]: "t \<in> U \<Longrightarrow> \<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)" |
|
113 proof(clarsimp) |
|
114 fix x l u y |
|
115 assume tU: "t \<in> U" and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x" and xu: "x<u" |
|
116 and px: "x \<le> t" and ly: "l<y" and yu:"y < u" |
|
117 from tU noU ly yu have tny: "t\<noteq>y" by auto |
|
118 {assume H: "t < y" |
|
119 from less_le_trans[OF lx px] less_trans[OF H yu] |
|
120 have "l < t \<and> t < u" by simp |
|
121 with tU noU have "False" by auto} |
|
122 hence "\<not> t < y" by auto thus "y \<le> t" by (simp add: not_less) |
|
123 qed |
|
124 |
|
125 lemma lin_dense_ge[noatp]: "t \<in> U \<Longrightarrow> \<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)" |
|
126 proof(clarsimp) |
|
127 fix x l u y |
|
128 assume tU: "t \<in> U" and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x" and xu: "x<u" |
|
129 and px: "t \<le> x" and ly: "l<y" and yu:"y < u" |
|
130 from tU noU ly yu have tny: "t\<noteq>y" by auto |
|
131 {assume H: "y< t" |
|
132 from less_trans[OF ly H] le_less_trans[OF px xu] |
|
133 have "l < t \<and> t < u" by simp |
|
134 with tU noU have "False" by auto} |
|
135 hence "\<not> y<t" by auto thus "t \<le> y" by (simp add: not_less) |
|
136 qed |
|
137 lemma lin_dense_eq[noatp]: "t \<in> U \<Longrightarrow> \<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)" by auto |
|
138 lemma lin_dense_neq[noatp]: "t \<in> U \<Longrightarrow> \<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)" by auto |
|
139 lemma lin_dense_P[noatp]: "\<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)" by auto |
|
140 |
|
141 lemma lin_dense_conj[noatp]: |
|
142 "\<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 |
|
143 \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P1 y) ; |
|
144 \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P2 x |
|
145 \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow> |
|
146 \<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) |
|
147 \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> (P1 y \<and> P2 y))" |
|
148 by blast |
|
149 lemma lin_dense_disj[noatp]: |
|
150 "\<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 |
|
151 \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P1 y) ; |
|
152 \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P2 x |
|
153 \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow> |
|
154 \<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) |
|
155 \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> (P1 y \<or> P2 y))" |
|
156 by blast |
|
157 |
|
158 lemma npmibnd[noatp]: "\<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> |
|
159 \<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')" |
|
160 by auto |
|
161 |
|
162 lemma finite_set_intervals[noatp]: |
|
163 assumes px: "P x" and lx: "l \<le> x" and xu: "x \<le> u" and linS: "l\<in> S" |
|
164 and uinS: "u \<in> S" and fS:"finite S" and lS: "\<forall> x\<in> S. l \<le> x" and Su: "\<forall> x\<in> S. x \<le> u" |
|
165 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" |
|
166 proof- |
|
167 let ?Mx = "{y. y\<in> S \<and> y \<le> x}" |
|
168 let ?xM = "{y. y\<in> S \<and> x \<le> y}" |
|
169 let ?a = "Max ?Mx" |
|
170 let ?b = "Min ?xM" |
|
171 have MxS: "?Mx \<subseteq> S" by blast |
|
172 hence fMx: "finite ?Mx" using fS finite_subset by auto |
|
173 from lx linS have linMx: "l \<in> ?Mx" by blast |
|
174 hence Mxne: "?Mx \<noteq> {}" by blast |
|
175 have xMS: "?xM \<subseteq> S" by blast |
|
176 hence fxM: "finite ?xM" using fS finite_subset by auto |
|
177 from xu uinS have linxM: "u \<in> ?xM" by blast |
|
178 hence xMne: "?xM \<noteq> {}" by blast |
|
179 have ax:"?a \<le> x" using Mxne fMx by auto |
|
180 have xb:"x \<le> ?b" using xMne fxM by auto |
|
181 have "?a \<in> ?Mx" using Max_in[OF fMx Mxne] by simp hence ainS: "?a \<in> S" using MxS by blast |
|
182 have "?b \<in> ?xM" using Min_in[OF fxM xMne] by simp hence binS: "?b \<in> S" using xMS by blast |
|
183 have noy:"\<forall> y. ?a < y \<and> y < ?b \<longrightarrow> y \<notin> S" |
|
184 proof(clarsimp) |
|
185 fix y assume ay: "?a < y" and yb: "y < ?b" and yS: "y \<in> S" |
|
186 from yS have "y\<in> ?Mx \<or> y\<in> ?xM" by (auto simp add: linear) |
|
187 moreover {assume "y \<in> ?Mx" hence "y \<le> ?a" using Mxne fMx by auto with ay have "False" by (simp add: not_le[symmetric])} |
|
188 moreover {assume "y \<in> ?xM" hence "?b \<le> y" using xMne fxM by auto with yb have "False" by (simp add: not_le[symmetric])} |
|
189 ultimately show "False" by blast |
|
190 qed |
|
191 from ainS binS noy ax xb px show ?thesis by blast |
|
192 qed |
|
193 |
|
194 lemma finite_set_intervals2[noatp]: |
|
195 assumes px: "P x" and lx: "l \<le> x" and xu: "x \<le> u" and linS: "l\<in> S" |
|
196 and uinS: "u \<in> S" and fS:"finite S" and lS: "\<forall> x\<in> S. l \<le> x" and Su: "\<forall> x\<in> S. x \<le> u" |
|
197 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)" |
|
198 proof- |
|
199 from finite_set_intervals[where P="P", OF px lx xu linS uinS fS lS Su] |
|
200 obtain a and b where |
|
201 as: "a\<in> S" and bs: "b\<in> S" and noS:"\<forall>y. a < y \<and> y < b \<longrightarrow> y \<notin> S" |
|
202 and axb: "a \<le> x \<and> x \<le> b \<and> P x" by auto |
|
203 from axb have "x= a \<or> x= b \<or> (a < x \<and> x < b)" by (auto simp add: le_less) |
|
204 thus ?thesis using px as bs noS by blast |
|
205 qed |
|
206 |
|
207 end |
|
208 |
|
209 section {* The classical QE after Langford for dense linear orders *} |
|
210 |
|
211 context dense_linear_order |
|
212 begin |
|
213 |
|
214 lemma interval_empty_iff: |
|
215 "{y. x < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z" |
|
216 by (auto dest: dense) |
|
217 |
|
218 lemma dlo_qe_bnds[noatp]: |
|
219 assumes ne: "L \<noteq> {}" and neU: "U \<noteq> {}" and fL: "finite L" and fU: "finite U" |
|
220 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)" |
|
221 proof (simp only: atomize_eq, rule iffI) |
|
222 assume H: "\<exists>x. (\<forall>y\<in>L. y < x) \<and> (\<forall>y\<in>U. x < y)" |
|
223 then obtain x where xL: "\<forall>y\<in>L. y < x" and xU: "\<forall>y\<in>U. x < y" by blast |
|
224 {fix l u assume l: "l \<in> L" and u: "u \<in> U" |
|
225 have "l < x" using xL l by blast |
|
226 also have "x < u" using xU u by blast |
|
227 finally (less_trans) have "l < u" .} |
|
228 thus "\<forall>l\<in>L. \<forall>u\<in>U. l < u" by blast |
|
229 next |
|
230 assume H: "\<forall>l\<in>L. \<forall>u\<in>U. l < u" |
|
231 let ?ML = "Max L" |
|
232 let ?MU = "Min U" |
|
233 from fL ne have th1: "?ML \<in> L" and th1': "\<forall>l\<in>L. l \<le> ?ML" by auto |
|
234 from fU neU have th2: "?MU \<in> U" and th2': "\<forall>u\<in>U. ?MU \<le> u" by auto |
|
235 from th1 th2 H have "?ML < ?MU" by auto |
|
236 with dense obtain w where th3: "?ML < w" and th4: "w < ?MU" by blast |
|
237 from th3 th1' have "\<forall>l \<in> L. l < w" by auto |
|
238 moreover from th4 th2' have "\<forall>u \<in> U. w < u" by auto |
|
239 ultimately show "\<exists>x. (\<forall>y\<in>L. y < x) \<and> (\<forall>y\<in>U. x < y)" by auto |
|
240 qed |
|
241 |
|
242 lemma dlo_qe_noub[noatp]: |
|
243 assumes ne: "L \<noteq> {}" and fL: "finite L" |
|
244 shows "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> {}. x < y)) \<equiv> True" |
|
245 proof(simp add: atomize_eq) |
|
246 from gt_ex[of "Max L"] obtain M where M: "Max L < M" by blast |
|
247 from ne fL have "\<forall>x \<in> L. x \<le> Max L" by simp |
|
248 with M have "\<forall>x\<in>L. x < M" by (auto intro: le_less_trans) |
|
249 thus "\<exists>x. \<forall>y\<in>L. y < x" by blast |
|
250 qed |
|
251 |
|
252 lemma dlo_qe_nolb[noatp]: |
|
253 assumes ne: "U \<noteq> {}" and fU: "finite U" |
|
254 shows "(\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y \<in> U. x < y)) \<equiv> True" |
|
255 proof(simp add: atomize_eq) |
|
256 from lt_ex[of "Min U"] obtain M where M: "M < Min U" by blast |
|
257 from ne fU have "\<forall>x \<in> U. Min U \<le> x" by simp |
|
258 with M have "\<forall>x\<in>U. M < x" by (auto intro: less_le_trans) |
|
259 thus "\<exists>x. \<forall>y\<in>U. x < y" by blast |
|
260 qed |
|
261 |
|
262 lemma exists_neq[noatp]: "\<exists>(x::'a). x \<noteq> t" "\<exists>(x::'a). t \<noteq> x" |
|
263 using gt_ex[of t] by auto |
|
264 |
|
265 lemmas dlo_simps[noatp] = order_refl less_irrefl not_less not_le exists_neq |
|
266 le_less neq_iff linear less_not_permute |
|
267 |
|
268 lemma axiom[noatp]: "dense_linear_order (op \<le>) (op <)" by (rule dense_linear_order_axioms) |
|
269 lemma atoms[noatp]: |
|
270 shows "TERM (less :: 'a \<Rightarrow> _)" |
|
271 and "TERM (less_eq :: 'a \<Rightarrow> _)" |
|
272 and "TERM (op = :: 'a \<Rightarrow> _)" . |
|
273 |
|
274 declare axiom[langford qe: dlo_qe_bnds dlo_qe_nolb dlo_qe_noub gather: gather_start gather_simps atoms: atoms] |
|
275 declare dlo_simps[langfordsimp] |
|
276 |
|
277 end |
|
278 |
|
279 (* FIXME: Move to HOL -- together with the conj_aci_rule in langford.ML *) |
|
280 lemma dnf[noatp]: |
|
281 "(P & (Q | R)) = ((P&Q) | (P&R))" |
|
282 "((Q | R) & P) = ((Q&P) | (R&P))" |
|
283 by blast+ |
|
284 |
|
285 lemmas weak_dnf_simps[noatp] = simp_thms dnf |
|
286 |
|
287 lemma nnf_simps[noatp]: |
|
288 "(\<not>(P \<and> Q)) = (\<not>P \<or> \<not>Q)" "(\<not>(P \<or> Q)) = (\<not>P \<and> \<not>Q)" "(P \<longrightarrow> Q) = (\<not>P \<or> Q)" |
|
289 "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P" |
|
290 by blast+ |
|
291 |
|
292 lemma ex_distrib[noatp]: "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> ((\<exists>x. P x) \<or> (\<exists>x. Q x))" by blast |
|
293 |
|
294 lemmas dnf_simps[noatp] = weak_dnf_simps nnf_simps ex_distrib |
|
295 |
|
296 use "~~/src/HOL/Tools/Qelim/langford.ML" |
|
297 method_setup dlo = {* |
|
298 Method.ctxt_args (Method.SIMPLE_METHOD' o LangfordQE.dlo_tac) |
|
299 *} "Langford's algorithm for quantifier elimination in dense linear orders" |
|
300 |
|
301 |
|
302 section {* Contructive dense linear orders yield QE for linear arithmetic over ordered Fields -- see @{text "Arith_Tools.thy"} *} |
|
303 |
|
304 text {* Linear order without upper bounds *} |
|
305 |
|
306 locale linorder_stupid_syntax = linorder |
|
307 begin |
|
308 notation |
|
309 less_eq ("op \<sqsubseteq>") and |
|
310 less_eq ("(_/ \<sqsubseteq> _)" [51, 51] 50) and |
|
311 less ("op \<sqsubset>") and |
|
312 less ("(_/ \<sqsubset> _)" [51, 51] 50) |
|
313 |
|
314 end |
|
315 |
|
316 locale linorder_no_ub = linorder_stupid_syntax + |
|
317 assumes gt_ex: "\<exists>y. less x y" |
|
318 begin |
|
319 lemma ge_ex[noatp]: "\<exists>y. x \<sqsubseteq> y" using gt_ex by auto |
|
320 |
|
321 text {* Theorems for @{text "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"} *} |
|
322 lemma pinf_conj[noatp]: |
|
323 assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')" |
|
324 and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" |
|
325 shows "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))" |
|
326 proof- |
|
327 from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')" |
|
328 and z2: "\<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast |
|
329 from gt_ex obtain z where z:"ord.max less_eq z1 z2 \<sqsubset> z" by blast |
|
330 from z have zz1: "z1 \<sqsubset> z" and zz2: "z2 \<sqsubset> z" by simp_all |
|
331 {fix x assume H: "z \<sqsubset> x" |
|
332 from less_trans[OF zz1 H] less_trans[OF zz2 H] |
|
333 have "(P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2')" using z1 zz1 z2 zz2 by auto |
|
334 } |
|
335 thus ?thesis by blast |
|
336 qed |
|
337 |
|
338 lemma pinf_disj[noatp]: |
|
339 assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')" |
|
340 and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" |
|
341 shows "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))" |
|
342 proof- |
|
343 from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')" |
|
344 and z2: "\<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast |
|
345 from gt_ex obtain z where z:"ord.max less_eq z1 z2 \<sqsubset> z" by blast |
|
346 from z have zz1: "z1 \<sqsubset> z" and zz2: "z2 \<sqsubset> z" by simp_all |
|
347 {fix x assume H: "z \<sqsubset> x" |
|
348 from less_trans[OF zz1 H] less_trans[OF zz2 H] |
|
349 have "(P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2')" using z1 zz1 z2 zz2 by auto |
|
350 } |
|
351 thus ?thesis by blast |
|
352 qed |
|
353 |
|
354 lemma pinf_ex[noatp]: assumes ex:"\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x" |
|
355 proof- |
|
356 from ex obtain z where z: "\<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast |
|
357 from gt_ex obtain x where x: "z \<sqsubset> x" by blast |
|
358 from z x p1 show ?thesis by blast |
|
359 qed |
|
360 |
|
361 end |
|
362 |
|
363 text {* Linear order without upper bounds *} |
|
364 |
|
365 locale linorder_no_lb = linorder_stupid_syntax + |
|
366 assumes lt_ex: "\<exists>y. less y x" |
|
367 begin |
|
368 lemma le_ex[noatp]: "\<exists>y. y \<sqsubseteq> x" using lt_ex by auto |
|
369 |
|
370 |
|
371 text {* Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"} *} |
|
372 lemma minf_conj[noatp]: |
|
373 assumes ex1: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')" |
|
374 and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')" |
|
375 shows "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))" |
|
376 proof- |
|
377 from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"and z2: "\<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast |
|
378 from lt_ex obtain z where z:"z \<sqsubset> ord.min less_eq z1 z2" by blast |
|
379 from z have zz1: "z \<sqsubset> z1" and zz2: "z \<sqsubset> z2" by simp_all |
|
380 {fix x assume H: "x \<sqsubset> z" |
|
381 from less_trans[OF H zz1] less_trans[OF H zz2] |
|
382 have "(P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2')" using z1 zz1 z2 zz2 by auto |
|
383 } |
|
384 thus ?thesis by blast |
|
385 qed |
|
386 |
|
387 lemma minf_disj[noatp]: |
|
388 assumes ex1: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')" |
|
389 and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')" |
|
390 shows "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))" |
|
391 proof- |
|
392 from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"and z2: "\<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast |
|
393 from lt_ex obtain z where z:"z \<sqsubset> ord.min less_eq z1 z2" by blast |
|
394 from z have zz1: "z \<sqsubset> z1" and zz2: "z \<sqsubset> z2" by simp_all |
|
395 {fix x assume H: "x \<sqsubset> z" |
|
396 from less_trans[OF H zz1] less_trans[OF H zz2] |
|
397 have "(P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2')" using z1 zz1 z2 zz2 by auto |
|
398 } |
|
399 thus ?thesis by blast |
|
400 qed |
|
401 |
|
402 lemma minf_ex[noatp]: assumes ex:"\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x" |
|
403 proof- |
|
404 from ex obtain z where z: "\<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast |
|
405 from lt_ex obtain x where x: "x \<sqsubset> z" by blast |
|
406 from z x p1 show ?thesis by blast |
|
407 qed |
|
408 |
|
409 end |
|
410 |
|
411 |
|
412 locale constr_dense_linear_order = linorder_no_lb + linorder_no_ub + |
|
413 fixes between |
|
414 assumes between_less: "less x y \<Longrightarrow> less x (between x y) \<and> less (between x y) y" |
|
415 and between_same: "between x x = x" |
|
416 |
|
417 sublocale constr_dense_linear_order < dense_linear_order |
|
418 apply unfold_locales |
|
419 using gt_ex lt_ex between_less |
|
420 by (auto, rule_tac x="between x y" in exI, simp) |
|
421 |
|
422 context constr_dense_linear_order |
|
423 begin |
|
424 |
|
425 lemma rinf_U[noatp]: |
|
426 assumes fU: "finite U" |
|
427 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 |
|
428 \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P y )" |
|
429 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')" |
|
430 and nmi: "\<not> MP" and npi: "\<not> PP" and ex: "\<exists> x. P x" |
|
431 shows "\<exists> u\<in> U. \<exists> u' \<in> U. P (between u u')" |
|
432 proof- |
|
433 from ex obtain x where px: "P x" by blast |
|
434 from px nmi npi nmpiU have "\<exists> u\<in> U. \<exists> u' \<in> U. u \<sqsubseteq> x \<and> x \<sqsubseteq> u'" by auto |
|
435 then obtain u and u' where uU:"u\<in> U" and uU': "u' \<in> U" and ux:"u \<sqsubseteq> x" and xu':"x \<sqsubseteq> u'" by auto |
|
436 from uU have Une: "U \<noteq> {}" by auto |
|
437 term "linorder.Min less_eq" |
|
438 let ?l = "linorder.Min less_eq U" |
|
439 let ?u = "linorder.Max less_eq U" |
|
440 have linM: "?l \<in> U" using fU Une by simp |
|
441 have uinM: "?u \<in> U" using fU Une by simp |
|
442 have lM: "\<forall> t\<in> U. ?l \<sqsubseteq> t" using Une fU by auto |
|
443 have Mu: "\<forall> t\<in> U. t \<sqsubseteq> ?u" using Une fU by auto |
|
444 have th:"?l \<sqsubseteq> u" using uU Une lM by auto |
|
445 from order_trans[OF th ux] have lx: "?l \<sqsubseteq> x" . |
|
446 have th: "u' \<sqsubseteq> ?u" using uU' Une Mu by simp |
|
447 from order_trans[OF xu' th] have xu: "x \<sqsubseteq> ?u" . |
|
448 from finite_set_intervals2[where P="P",OF px lx xu linM uinM fU lM Mu] |
|
449 have "(\<exists> s\<in> U. P s) \<or> |
|
450 (\<exists> t1\<in> U. \<exists> t2 \<in> U. (\<forall> y. t1 \<sqsubset> y \<and> y \<sqsubset> t2 \<longrightarrow> y \<notin> U) \<and> t1 \<sqsubset> x \<and> x \<sqsubset> t2 \<and> P x)" . |
|
451 moreover { fix u assume um: "u\<in>U" and pu: "P u" |
|
452 have "between u u = u" by (simp add: between_same) |
|
453 with um pu have "P (between u u)" by simp |
|
454 with um have ?thesis by blast} |
|
455 moreover{ |
|
456 assume "\<exists> t1\<in> U. \<exists> t2 \<in> U. (\<forall> y. t1 \<sqsubset> y \<and> y \<sqsubset> t2 \<longrightarrow> y \<notin> U) \<and> t1 \<sqsubset> x \<and> x \<sqsubset> t2 \<and> P x" |
|
457 then obtain t1 and t2 where t1M: "t1 \<in> U" and t2M: "t2\<in> U" |
|
458 and noM: "\<forall> y. t1 \<sqsubset> y \<and> y \<sqsubset> t2 \<longrightarrow> y \<notin> U" and t1x: "t1 \<sqsubset> x" and xt2: "x \<sqsubset> t2" and px: "P x" |
|
459 by blast |
|
460 from less_trans[OF t1x xt2] have t1t2: "t1 \<sqsubset> t2" . |
|
461 let ?u = "between t1 t2" |
|
462 from between_less t1t2 have t1lu: "t1 \<sqsubset> ?u" and ut2: "?u \<sqsubset> t2" by auto |
|
463 from lin_dense noM t1x xt2 px t1lu ut2 have "P ?u" by blast |
|
464 with t1M t2M have ?thesis by blast} |
|
465 ultimately show ?thesis by blast |
|
466 qed |
|
467 |
|
468 theorem fr_eq[noatp]: |
|
469 assumes fU: "finite U" |
|
470 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 |
|
471 \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P y )" |
|
472 and nmibnd: "\<forall>x. \<not> MP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<sqsubseteq> x)" |
|
473 and npibnd: "\<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. x \<sqsubseteq> u)" |
|
474 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)" |
|
475 shows "(\<exists> x. P x) \<equiv> (MP \<or> PP \<or> (\<exists> u \<in> U. \<exists> u'\<in> U. P (between u u')))" |
|
476 (is "_ \<equiv> (_ \<or> _ \<or> ?F)" is "?E \<equiv> ?D") |
|
477 proof- |
|
478 { |
|
479 assume px: "\<exists> x. P x" |
|
480 have "MP \<or> PP \<or> (\<not> MP \<and> \<not> PP)" by blast |
|
481 moreover {assume "MP \<or> PP" hence "?D" by blast} |
|
482 moreover {assume nmi: "\<not> MP" and npi: "\<not> PP" |
|
483 from npmibnd[OF nmibnd npibnd] |
|
484 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')" . |
|
485 from rinf_U[OF fU lin_dense nmpiU nmi npi px] have "?D" by blast} |
|
486 ultimately have "?D" by blast} |
|
487 moreover |
|
488 { assume "?D" |
|
489 moreover {assume m:"MP" from minf_ex[OF mi m] have "?E" .} |
|
490 moreover {assume p: "PP" from pinf_ex[OF pi p] have "?E" . } |
|
491 moreover {assume f:"?F" hence "?E" by blast} |
|
492 ultimately have "?E" by blast} |
|
493 ultimately have "?E = ?D" by blast thus "?E \<equiv> ?D" by simp |
|
494 qed |
|
495 |
|
496 lemmas minf_thms[noatp] = minf_conj minf_disj minf_eq minf_neq minf_lt minf_le minf_gt minf_ge minf_P |
|
497 lemmas pinf_thms[noatp] = pinf_conj pinf_disj pinf_eq pinf_neq pinf_lt pinf_le pinf_gt pinf_ge pinf_P |
|
498 |
|
499 lemmas nmi_thms[noatp] = nmi_conj nmi_disj nmi_eq nmi_neq nmi_lt nmi_le nmi_gt nmi_ge nmi_P |
|
500 lemmas npi_thms[noatp] = npi_conj npi_disj npi_eq npi_neq npi_lt npi_le npi_gt npi_ge npi_P |
|
501 lemmas lin_dense_thms[noatp] = 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 |
|
502 |
|
503 lemma ferrack_axiom[noatp]: "constr_dense_linear_order less_eq less between" |
|
504 by (rule constr_dense_linear_order_axioms) |
|
505 lemma atoms[noatp]: |
|
506 shows "TERM (less :: 'a \<Rightarrow> _)" |
|
507 and "TERM (less_eq :: 'a \<Rightarrow> _)" |
|
508 and "TERM (op = :: 'a \<Rightarrow> _)" . |
|
509 |
|
510 declare ferrack_axiom [ferrack minf: minf_thms pinf: pinf_thms |
|
511 nmi: nmi_thms npi: npi_thms lindense: |
|
512 lin_dense_thms qe: fr_eq atoms: atoms] |
|
513 |
|
514 declaration {* |
|
515 let |
|
516 fun simps phi = map (Morphism.thm phi) [@{thm "not_less"}, @{thm "not_le"}] |
|
517 fun generic_whatis phi = |
|
518 let |
|
519 val [lt, le] = map (Morphism.term phi) [@{term "op \<sqsubset>"}, @{term "op \<sqsubseteq>"}] |
|
520 fun h x t = |
|
521 case term_of t of |
|
522 Const("op =", _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq |
|
523 else Ferrante_Rackoff_Data.Nox |
|
524 | @{term "Not"}$(Const("op =", _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq |
|
525 else Ferrante_Rackoff_Data.Nox |
|
526 | b$y$z => if Term.could_unify (b, lt) then |
|
527 if term_of x aconv y then Ferrante_Rackoff_Data.Lt |
|
528 else if term_of x aconv z then Ferrante_Rackoff_Data.Gt |
|
529 else Ferrante_Rackoff_Data.Nox |
|
530 else if Term.could_unify (b, le) then |
|
531 if term_of x aconv y then Ferrante_Rackoff_Data.Le |
|
532 else if term_of x aconv z then Ferrante_Rackoff_Data.Ge |
|
533 else Ferrante_Rackoff_Data.Nox |
|
534 else Ferrante_Rackoff_Data.Nox |
|
535 | _ => Ferrante_Rackoff_Data.Nox |
|
536 in h end |
|
537 fun ss phi = HOL_ss addsimps (simps phi) |
|
538 in |
|
539 Ferrante_Rackoff_Data.funs @{thm "ferrack_axiom"} |
|
540 {isolate_conv = K (K (K Thm.reflexive)), whatis = generic_whatis, simpset = ss} |
|
541 end |
|
542 *} |
|
543 |
|
544 end |
|
545 |
|
546 use "~~/src/HOL/Tools/Qelim/ferrante_rackoff.ML" |
|
547 |
|
548 method_setup ferrack = {* |
|
549 Method.ctxt_args (Method.SIMPLE_METHOD' o FerranteRackoff.dlo_tac) |
|
550 *} "Ferrante and Rackoff's algorithm for quantifier elimination in dense linear orders" |
|
551 |
|
552 subsection {* Ferrante and Rackoff algorithm over ordered fields *} |
|
553 |
|
554 lemma neg_prod_lt:"(c\<Colon>'a\<Colon>ordered_field) < 0 \<Longrightarrow> ((c*x < 0) == (x > 0))" |
|
555 proof- |
|
556 assume H: "c < 0" |
|
557 have "c*x < 0 = (0/c < x)" by (simp only: neg_divide_less_eq[OF H] algebra_simps) |
|
558 also have "\<dots> = (0 < x)" by simp |
|
559 finally show "(c*x < 0) == (x > 0)" by simp |
|
560 qed |
|
561 |
|
562 lemma pos_prod_lt:"(c\<Colon>'a\<Colon>ordered_field) > 0 \<Longrightarrow> ((c*x < 0) == (x < 0))" |
|
563 proof- |
|
564 assume H: "c > 0" |
|
565 hence "c*x < 0 = (0/c > x)" by (simp only: pos_less_divide_eq[OF H] algebra_simps) |
|
566 also have "\<dots> = (0 > x)" by simp |
|
567 finally show "(c*x < 0) == (x < 0)" by simp |
|
568 qed |
|
569 |
|
570 lemma neg_prod_sum_lt: "(c\<Colon>'a\<Colon>ordered_field) < 0 \<Longrightarrow> ((c*x + t< 0) == (x > (- 1/c)*t))" |
|
571 proof- |
|
572 assume H: "c < 0" |
|
573 have "c*x + t< 0 = (c*x < -t)" by (subst less_iff_diff_less_0 [of "c*x" "-t"], simp) |
|
574 also have "\<dots> = (-t/c < x)" by (simp only: neg_divide_less_eq[OF H] algebra_simps) |
|
575 also have "\<dots> = ((- 1/c)*t < x)" by simp |
|
576 finally show "(c*x + t < 0) == (x > (- 1/c)*t)" by simp |
|
577 qed |
|
578 |
|
579 lemma pos_prod_sum_lt:"(c\<Colon>'a\<Colon>ordered_field) > 0 \<Longrightarrow> ((c*x + t < 0) == (x < (- 1/c)*t))" |
|
580 proof- |
|
581 assume H: "c > 0" |
|
582 have "c*x + t< 0 = (c*x < -t)" by (subst less_iff_diff_less_0 [of "c*x" "-t"], simp) |
|
583 also have "\<dots> = (-t/c > x)" by (simp only: pos_less_divide_eq[OF H] algebra_simps) |
|
584 also have "\<dots> = ((- 1/c)*t > x)" by simp |
|
585 finally show "(c*x + t < 0) == (x < (- 1/c)*t)" by simp |
|
586 qed |
|
587 |
|
588 lemma sum_lt:"((x::'a::pordered_ab_group_add) + t < 0) == (x < - t)" |
|
589 using less_diff_eq[where a= x and b=t and c=0] by simp |
|
590 |
|
591 lemma neg_prod_le:"(c\<Colon>'a\<Colon>ordered_field) < 0 \<Longrightarrow> ((c*x <= 0) == (x >= 0))" |
|
592 proof- |
|
593 assume H: "c < 0" |
|
594 have "c*x <= 0 = (0/c <= x)" by (simp only: neg_divide_le_eq[OF H] algebra_simps) |
|
595 also have "\<dots> = (0 <= x)" by simp |
|
596 finally show "(c*x <= 0) == (x >= 0)" by simp |
|
597 qed |
|
598 |
|
599 lemma pos_prod_le:"(c\<Colon>'a\<Colon>ordered_field) > 0 \<Longrightarrow> ((c*x <= 0) == (x <= 0))" |
|
600 proof- |
|
601 assume H: "c > 0" |
|
602 hence "c*x <= 0 = (0/c >= x)" by (simp only: pos_le_divide_eq[OF H] algebra_simps) |
|
603 also have "\<dots> = (0 >= x)" by simp |
|
604 finally show "(c*x <= 0) == (x <= 0)" by simp |
|
605 qed |
|
606 |
|
607 lemma neg_prod_sum_le: "(c\<Colon>'a\<Colon>ordered_field) < 0 \<Longrightarrow> ((c*x + t <= 0) == (x >= (- 1/c)*t))" |
|
608 proof- |
|
609 assume H: "c < 0" |
|
610 have "c*x + t <= 0 = (c*x <= -t)" by (subst le_iff_diff_le_0 [of "c*x" "-t"], simp) |
|
611 also have "\<dots> = (-t/c <= x)" by (simp only: neg_divide_le_eq[OF H] algebra_simps) |
|
612 also have "\<dots> = ((- 1/c)*t <= x)" by simp |
|
613 finally show "(c*x + t <= 0) == (x >= (- 1/c)*t)" by simp |
|
614 qed |
|
615 |
|
616 lemma pos_prod_sum_le:"(c\<Colon>'a\<Colon>ordered_field) > 0 \<Longrightarrow> ((c*x + t <= 0) == (x <= (- 1/c)*t))" |
|
617 proof- |
|
618 assume H: "c > 0" |
|
619 have "c*x + t <= 0 = (c*x <= -t)" by (subst le_iff_diff_le_0 [of "c*x" "-t"], simp) |
|
620 also have "\<dots> = (-t/c >= x)" by (simp only: pos_le_divide_eq[OF H] algebra_simps) |
|
621 also have "\<dots> = ((- 1/c)*t >= x)" by simp |
|
622 finally show "(c*x + t <= 0) == (x <= (- 1/c)*t)" by simp |
|
623 qed |
|
624 |
|
625 lemma sum_le:"((x::'a::pordered_ab_group_add) + t <= 0) == (x <= - t)" |
|
626 using le_diff_eq[where a= x and b=t and c=0] by simp |
|
627 |
|
628 lemma nz_prod_eq:"(c\<Colon>'a\<Colon>ordered_field) \<noteq> 0 \<Longrightarrow> ((c*x = 0) == (x = 0))" by simp |
|
629 lemma nz_prod_sum_eq: "(c\<Colon>'a\<Colon>ordered_field) \<noteq> 0 \<Longrightarrow> ((c*x + t = 0) == (x = (- 1/c)*t))" |
|
630 proof- |
|
631 assume H: "c \<noteq> 0" |
|
632 have "c*x + t = 0 = (c*x = -t)" by (subst eq_iff_diff_eq_0 [of "c*x" "-t"], simp) |
|
633 also have "\<dots> = (x = -t/c)" by (simp only: nonzero_eq_divide_eq[OF H] algebra_simps) |
|
634 finally show "(c*x + t = 0) == (x = (- 1/c)*t)" by simp |
|
635 qed |
|
636 lemma sum_eq:"((x::'a::pordered_ab_group_add) + t = 0) == (x = - t)" |
|
637 using eq_diff_eq[where a= x and b=t and c=0] by simp |
|
638 |
|
639 |
|
640 interpretation class_ordered_field_dense_linear_order!: constr_dense_linear_order |
|
641 "op <=" "op <" |
|
642 "\<lambda> x y. 1/2 * ((x::'a::{ordered_field,recpower,number_ring}) + y)" |
|
643 proof (unfold_locales, dlo, dlo, auto) |
|
644 fix x y::'a assume lt: "x < y" |
|
645 from less_half_sum[OF lt] show "x < (x + y) /2" by simp |
|
646 next |
|
647 fix x y::'a assume lt: "x < y" |
|
648 from gt_half_sum[OF lt] show "(x + y) /2 < y" by simp |
|
649 qed |
|
650 |
|
651 declaration{* |
|
652 let |
|
653 fun earlier [] x y = false |
|
654 | earlier (h::t) x y = |
|
655 if h aconvc y then false else if h aconvc x then true else earlier t x y; |
|
656 |
|
657 fun dest_frac ct = case term_of ct of |
|
658 Const (@{const_name "HOL.divide"},_) $ a $ b=> |
|
659 Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b)) |
|
660 | t => Rat.rat_of_int (snd (HOLogic.dest_number t)) |
|
661 |
|
662 fun mk_frac phi cT x = |
|
663 let val (a, b) = Rat.quotient_of_rat x |
|
664 in if b = 1 then Numeral.mk_cnumber cT a |
|
665 else Thm.capply |
|
666 (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"}) |
|
667 (Numeral.mk_cnumber cT a)) |
|
668 (Numeral.mk_cnumber cT b) |
|
669 end |
|
670 |
|
671 fun whatis x ct = case term_of ct of |
|
672 Const(@{const_name "HOL.plus"}, _)$(Const(@{const_name "HOL.times"},_)$_$y)$_ => |
|
673 if y aconv term_of x then ("c*x+t",[(funpow 2 Thm.dest_arg1) ct, Thm.dest_arg ct]) |
|
674 else ("Nox",[]) |
|
675 | Const(@{const_name "HOL.plus"}, _)$y$_ => |
|
676 if y aconv term_of x then ("x+t",[Thm.dest_arg ct]) |
|
677 else ("Nox",[]) |
|
678 | Const(@{const_name "HOL.times"}, _)$_$y => |
|
679 if y aconv term_of x then ("c*x",[Thm.dest_arg1 ct]) |
|
680 else ("Nox",[]) |
|
681 | t => if t aconv term_of x then ("x",[]) else ("Nox",[]); |
|
682 |
|
683 fun xnormalize_conv ctxt [] ct = reflexive ct |
|
684 | xnormalize_conv ctxt (vs as (x::_)) ct = |
|
685 case term_of ct of |
|
686 Const(@{const_name HOL.less},_)$_$Const(@{const_name "HOL.zero"},_) => |
|
687 (case whatis x (Thm.dest_arg1 ct) of |
|
688 ("c*x+t",[c,t]) => |
|
689 let |
|
690 val cr = dest_frac c |
|
691 val clt = Thm.dest_fun2 ct |
|
692 val cz = Thm.dest_arg ct |
|
693 val neg = cr </ Rat.zero |
|
694 val cthp = Simplifier.rewrite (local_simpset_of ctxt) |
|
695 (Thm.capply @{cterm "Trueprop"} |
|
696 (if neg then Thm.capply (Thm.capply clt c) cz |
|
697 else Thm.capply (Thm.capply clt cz) c)) |
|
698 val cth = equal_elim (symmetric cthp) TrueI |
|
699 val th = implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x,t]) |
|
700 (if neg then @{thm neg_prod_sum_lt} else @{thm pos_prod_sum_lt})) cth |
|
701 val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv |
|
702 (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th |
|
703 in rth end |
|
704 | ("x+t",[t]) => |
|
705 let |
|
706 val T = ctyp_of_term x |
|
707 val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_lt"} |
|
708 val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv |
|
709 (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th |
|
710 in rth end |
|
711 | ("c*x",[c]) => |
|
712 let |
|
713 val cr = dest_frac c |
|
714 val clt = Thm.dest_fun2 ct |
|
715 val cz = Thm.dest_arg ct |
|
716 val neg = cr </ Rat.zero |
|
717 val cthp = Simplifier.rewrite (local_simpset_of ctxt) |
|
718 (Thm.capply @{cterm "Trueprop"} |
|
719 (if neg then Thm.capply (Thm.capply clt c) cz |
|
720 else Thm.capply (Thm.capply clt cz) c)) |
|
721 val cth = equal_elim (symmetric cthp) TrueI |
|
722 val th = implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x]) |
|
723 (if neg then @{thm neg_prod_lt} else @{thm pos_prod_lt})) cth |
|
724 val rth = th |
|
725 in rth end |
|
726 | _ => reflexive ct) |
|
727 |
|
728 |
|
729 | Const(@{const_name HOL.less_eq},_)$_$Const(@{const_name "HOL.zero"},_) => |
|
730 (case whatis x (Thm.dest_arg1 ct) of |
|
731 ("c*x+t",[c,t]) => |
|
732 let |
|
733 val T = ctyp_of_term x |
|
734 val cr = dest_frac c |
|
735 val clt = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "op <"} |
|
736 val cz = Thm.dest_arg ct |
|
737 val neg = cr </ Rat.zero |
|
738 val cthp = Simplifier.rewrite (local_simpset_of ctxt) |
|
739 (Thm.capply @{cterm "Trueprop"} |
|
740 (if neg then Thm.capply (Thm.capply clt c) cz |
|
741 else Thm.capply (Thm.capply clt cz) c)) |
|
742 val cth = equal_elim (symmetric cthp) TrueI |
|
743 val th = implies_elim (instantiate' [SOME T] (map SOME [c,x,t]) |
|
744 (if neg then @{thm neg_prod_sum_le} else @{thm pos_prod_sum_le})) cth |
|
745 val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv |
|
746 (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th |
|
747 in rth end |
|
748 | ("x+t",[t]) => |
|
749 let |
|
750 val T = ctyp_of_term x |
|
751 val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_le"} |
|
752 val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv |
|
753 (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th |
|
754 in rth end |
|
755 | ("c*x",[c]) => |
|
756 let |
|
757 val T = ctyp_of_term x |
|
758 val cr = dest_frac c |
|
759 val clt = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "op <"} |
|
760 val cz = Thm.dest_arg ct |
|
761 val neg = cr </ Rat.zero |
|
762 val cthp = Simplifier.rewrite (local_simpset_of ctxt) |
|
763 (Thm.capply @{cterm "Trueprop"} |
|
764 (if neg then Thm.capply (Thm.capply clt c) cz |
|
765 else Thm.capply (Thm.capply clt cz) c)) |
|
766 val cth = equal_elim (symmetric cthp) TrueI |
|
767 val th = implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x]) |
|
768 (if neg then @{thm neg_prod_le} else @{thm pos_prod_le})) cth |
|
769 val rth = th |
|
770 in rth end |
|
771 | _ => reflexive ct) |
|
772 |
|
773 | Const("op =",_)$_$Const(@{const_name "HOL.zero"},_) => |
|
774 (case whatis x (Thm.dest_arg1 ct) of |
|
775 ("c*x+t",[c,t]) => |
|
776 let |
|
777 val T = ctyp_of_term x |
|
778 val cr = dest_frac c |
|
779 val ceq = Thm.dest_fun2 ct |
|
780 val cz = Thm.dest_arg ct |
|
781 val cthp = Simplifier.rewrite (local_simpset_of ctxt) |
|
782 (Thm.capply @{cterm "Trueprop"} |
|
783 (Thm.capply @{cterm "Not"} (Thm.capply (Thm.capply ceq c) cz))) |
|
784 val cth = equal_elim (symmetric cthp) TrueI |
|
785 val th = implies_elim |
|
786 (instantiate' [SOME T] (map SOME [c,x,t]) @{thm nz_prod_sum_eq}) cth |
|
787 val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv |
|
788 (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th |
|
789 in rth end |
|
790 | ("x+t",[t]) => |
|
791 let |
|
792 val T = ctyp_of_term x |
|
793 val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_eq"} |
|
794 val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv |
|
795 (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th |
|
796 in rth end |
|
797 | ("c*x",[c]) => |
|
798 let |
|
799 val T = ctyp_of_term x |
|
800 val cr = dest_frac c |
|
801 val ceq = Thm.dest_fun2 ct |
|
802 val cz = Thm.dest_arg ct |
|
803 val cthp = Simplifier.rewrite (local_simpset_of ctxt) |
|
804 (Thm.capply @{cterm "Trueprop"} |
|
805 (Thm.capply @{cterm "Not"} (Thm.capply (Thm.capply ceq c) cz))) |
|
806 val cth = equal_elim (symmetric cthp) TrueI |
|
807 val rth = implies_elim |
|
808 (instantiate' [SOME T] (map SOME [c,x]) @{thm nz_prod_eq}) cth |
|
809 in rth end |
|
810 | _ => reflexive ct); |
|
811 |
|
812 local |
|
813 val less_iff_diff_less_0 = mk_meta_eq @{thm "less_iff_diff_less_0"} |
|
814 val le_iff_diff_le_0 = mk_meta_eq @{thm "le_iff_diff_le_0"} |
|
815 val eq_iff_diff_eq_0 = mk_meta_eq @{thm "eq_iff_diff_eq_0"} |
|
816 in |
|
817 fun field_isolate_conv phi ctxt vs ct = case term_of ct of |
|
818 Const(@{const_name HOL.less},_)$a$b => |
|
819 let val (ca,cb) = Thm.dest_binop ct |
|
820 val T = ctyp_of_term ca |
|
821 val th = instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0 |
|
822 val nth = Conv.fconv_rule |
|
823 (Conv.arg_conv (Conv.arg1_conv |
|
824 (Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th |
|
825 val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth)) |
|
826 in rth end |
|
827 | Const(@{const_name HOL.less_eq},_)$a$b => |
|
828 let val (ca,cb) = Thm.dest_binop ct |
|
829 val T = ctyp_of_term ca |
|
830 val th = instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0 |
|
831 val nth = Conv.fconv_rule |
|
832 (Conv.arg_conv (Conv.arg1_conv |
|
833 (Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th |
|
834 val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth)) |
|
835 in rth end |
|
836 |
|
837 | Const("op =",_)$a$b => |
|
838 let val (ca,cb) = Thm.dest_binop ct |
|
839 val T = ctyp_of_term ca |
|
840 val th = instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0 |
|
841 val nth = Conv.fconv_rule |
|
842 (Conv.arg_conv (Conv.arg1_conv |
|
843 (Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th |
|
844 val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth)) |
|
845 in rth end |
|
846 | @{term "Not"} $(Const("op =",_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct |
|
847 | _ => reflexive ct |
|
848 end; |
|
849 |
|
850 fun classfield_whatis phi = |
|
851 let |
|
852 fun h x t = |
|
853 case term_of t of |
|
854 Const("op =", _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq |
|
855 else Ferrante_Rackoff_Data.Nox |
|
856 | @{term "Not"}$(Const("op =", _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq |
|
857 else Ferrante_Rackoff_Data.Nox |
|
858 | Const(@{const_name HOL.less},_)$y$z => |
|
859 if term_of x aconv y then Ferrante_Rackoff_Data.Lt |
|
860 else if term_of x aconv z then Ferrante_Rackoff_Data.Gt |
|
861 else Ferrante_Rackoff_Data.Nox |
|
862 | Const (@{const_name HOL.less_eq},_)$y$z => |
|
863 if term_of x aconv y then Ferrante_Rackoff_Data.Le |
|
864 else if term_of x aconv z then Ferrante_Rackoff_Data.Ge |
|
865 else Ferrante_Rackoff_Data.Nox |
|
866 | _ => Ferrante_Rackoff_Data.Nox |
|
867 in h end; |
|
868 fun class_field_ss phi = |
|
869 HOL_basic_ss addsimps ([@{thm "linorder_not_less"}, @{thm "linorder_not_le"}]) |
|
870 addsplits [@{thm "abs_split"},@{thm "split_max"}, @{thm "split_min"}] |
|
871 |
|
872 in |
|
873 Ferrante_Rackoff_Data.funs @{thm "class_ordered_field_dense_linear_order.ferrack_axiom"} |
|
874 {isolate_conv = field_isolate_conv, whatis = classfield_whatis, simpset = class_field_ss} |
|
875 end |
|
876 *} |
|
877 |
|
878 |
|
879 end |
|