1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Dense_Linear_Order.thy Tue Dec 30 11:10:01 2008 +0100
1.3 @@ -0,0 +1,877 @@
1.4 +(* Author: Amine Chaieb, TU Muenchen *)
1.5 +
1.6 +header {* Dense linear order without endpoints
1.7 + and a quantifier elimination procedure in Ferrante and Rackoff style *}
1.8 +
1.9 +theory Dense_Linear_Order
1.10 +imports Plain Groebner_Basis
1.11 +uses
1.12 + "~~/src/HOL/Tools/Qelim/langford_data.ML"
1.13 + "~~/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML"
1.14 + ("~~/src/HOL/Tools/Qelim/langford.ML")
1.15 + ("~~/src/HOL/Tools/Qelim/ferrante_rackoff.ML")
1.16 +begin
1.17 +
1.18 +setup {* Langford_Data.setup #> Ferrante_Rackoff_Data.setup *}
1.19 +
1.20 +context linorder
1.21 +begin
1.22 +
1.23 +lemma less_not_permute: "\<not> (x < y \<and> y < x)" by (simp add: not_less linear)
1.24 +
1.25 +lemma gather_simps:
1.26 + shows
1.27 + "(\<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)"
1.28 + 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)"
1.29 + "(\<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))"
1.30 + 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
1.31 +
1.32 +lemma
1.33 + gather_start: "(\<exists>x. P x) \<equiv> (\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y\<in> {}. x < y) \<and> P x)"
1.34 + by simp
1.35 +
1.36 +text{* Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"}*}
1.37 +lemma minf_lt: "\<exists>z . \<forall>x. x < z \<longrightarrow> (x < t \<longleftrightarrow> True)" by auto
1.38 +lemma minf_gt: "\<exists>z . \<forall>x. x < z \<longrightarrow> (t < x \<longleftrightarrow> False)"
1.39 + by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le)
1.40 +
1.41 +lemma minf_le: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<le> t \<longleftrightarrow> True)" by (auto simp add: less_le)
1.42 +lemma minf_ge: "\<exists>z. \<forall>x. x < z \<longrightarrow> (t \<le> x \<longleftrightarrow> False)"
1.43 + by (auto simp add: less_le not_less not_le)
1.44 +lemma minf_eq: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
1.45 +lemma minf_neq: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
1.46 +lemma minf_P: "\<exists>z. \<forall>x. x < z \<longrightarrow> (P \<longleftrightarrow> P)" by blast
1.47 +
1.48 +text{* Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"}*}
1.49 +lemma pinf_gt: "\<exists>z . \<forall>x. z < x \<longrightarrow> (t < x \<longleftrightarrow> True)" by auto
1.50 +lemma pinf_lt: "\<exists>z . \<forall>x. z < x \<longrightarrow> (x < t \<longleftrightarrow> False)"
1.51 + by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le)
1.52 +
1.53 +lemma pinf_ge: "\<exists>z. \<forall>x. z < x \<longrightarrow> (t \<le> x \<longleftrightarrow> True)" by (auto simp add: less_le)
1.54 +lemma pinf_le: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x \<le> t \<longleftrightarrow> False)"
1.55 + by (auto simp add: less_le not_less not_le)
1.56 +lemma pinf_eq: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
1.57 +lemma pinf_neq: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
1.58 +lemma pinf_P: "\<exists>z. \<forall>x. z < x \<longrightarrow> (P \<longleftrightarrow> P)" by blast
1.59 +
1.60 +lemma nmi_lt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x < t \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto
1.61 +lemma nmi_gt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t < x \<longrightarrow> (\<exists> u\<in> U. u \<le> x)"
1.62 + by (auto simp add: le_less)
1.63 +lemma nmi_le: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x\<le> t \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto
1.64 +lemma nmi_ge: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t\<le> x \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto
1.65 +lemma nmi_eq: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> x = t \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto
1.66 +lemma nmi_neq: "t \<in> U \<Longrightarrow>\<forall>x. \<not>True \<and> x \<noteq> t \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto
1.67 +lemma nmi_P: "\<forall> x. ~P \<and> P \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto
1.68 +lemma nmi_conj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow> (\<exists> u\<in> U. u \<le> x) ;
1.69 + \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow> (\<exists> u\<in> U. u \<le> x)\<rbrakk> \<Longrightarrow>
1.70 + \<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto
1.71 +lemma nmi_disj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow> (\<exists> u\<in> U. u \<le> x) ;
1.72 + \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow> (\<exists> u\<in> U. u \<le> x)\<rbrakk> \<Longrightarrow>
1.73 + \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto
1.74 +
1.75 +lemma npi_lt: "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)
1.76 +lemma npi_gt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> t < x \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by auto
1.77 +lemma npi_le: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> x \<le> t \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by auto
1.78 +lemma npi_ge: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> t \<le> x \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by auto
1.79 +lemma npi_eq: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> x = t \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by auto
1.80 +lemma npi_neq: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x \<noteq> t \<longrightarrow> (\<exists> u\<in> U. x \<le> u )" by auto
1.81 +lemma npi_P: "\<forall> x. ~P \<and> P \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by auto
1.82 +lemma npi_conj: "\<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>
1.83 + \<Longrightarrow> \<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by auto
1.84 +lemma npi_disj: "\<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>
1.85 + \<Longrightarrow> \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by auto
1.86 +
1.87 +lemma lin_dense_lt: "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)"
1.88 +proof(clarsimp)
1.89 + 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"
1.90 + and xu: "x<u" and px: "x < t" and ly: "l<y" and yu:"y < u"
1.91 + from tU noU ly yu have tny: "t\<noteq>y" by auto
1.92 + {assume H: "t < y"
1.93 + from less_trans[OF lx px] less_trans[OF H yu]
1.94 + have "l < t \<and> t < u" by simp
1.95 + with tU noU have "False" by auto}
1.96 + hence "\<not> t < y" by auto hence "y \<le> t" by (simp add: not_less)
1.97 + thus "y < t" using tny by (simp add: less_le)
1.98 +qed
1.99 +
1.100 +lemma lin_dense_gt: "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)"
1.101 +proof(clarsimp)
1.102 + fix x l u y
1.103 + 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"
1.104 + and px: "t < x" and ly: "l<y" and yu:"y < u"
1.105 + from tU noU ly yu have tny: "t\<noteq>y" by auto
1.106 + {assume H: "y< t"
1.107 + from less_trans[OF ly H] less_trans[OF px xu] have "l < t \<and> t < u" by simp
1.108 + with tU noU have "False" by auto}
1.109 + hence "\<not> y<t" by auto hence "t \<le> y" by (auto simp add: not_less)
1.110 + thus "t < y" using tny by (simp add:less_le)
1.111 +qed
1.112 +
1.113 +lemma lin_dense_le: "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)"
1.114 +proof(clarsimp)
1.115 + fix x l u y
1.116 + 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"
1.117 + and px: "x \<le> t" and ly: "l<y" and yu:"y < u"
1.118 + from tU noU ly yu have tny: "t\<noteq>y" by auto
1.119 + {assume H: "t < y"
1.120 + from less_le_trans[OF lx px] less_trans[OF H yu]
1.121 + have "l < t \<and> t < u" by simp
1.122 + with tU noU have "False" by auto}
1.123 + hence "\<not> t < y" by auto thus "y \<le> t" by (simp add: not_less)
1.124 +qed
1.125 +
1.126 +lemma lin_dense_ge: "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)"
1.127 +proof(clarsimp)
1.128 + fix x l u y
1.129 + 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"
1.130 + and px: "t \<le> x" and ly: "l<y" and yu:"y < u"
1.131 + from tU noU ly yu have tny: "t\<noteq>y" by auto
1.132 + {assume H: "y< t"
1.133 + from less_trans[OF ly H] le_less_trans[OF px xu]
1.134 + have "l < t \<and> t < u" by simp
1.135 + with tU noU have "False" by auto}
1.136 + hence "\<not> y<t" by auto thus "t \<le> y" by (simp add: not_less)
1.137 +qed
1.138 +lemma lin_dense_eq: "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
1.139 +lemma lin_dense_neq: "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
1.140 +lemma lin_dense_P: "\<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
1.141 +
1.142 +lemma lin_dense_conj:
1.143 + "\<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
1.144 + \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P1 y) ;
1.145 + \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P2 x
1.146 + \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow>
1.147 + \<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)
1.148 + \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> (P1 y \<and> P2 y))"
1.149 + by blast
1.150 +lemma lin_dense_disj:
1.151 + "\<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
1.152 + \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P1 y) ;
1.153 + \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P2 x
1.154 + \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow>
1.155 + \<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)
1.156 + \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> (P1 y \<or> P2 y))"
1.157 + by blast
1.158 +
1.159 +lemma npmibnd: "\<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>
1.160 + \<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')"
1.161 +by auto
1.162 +
1.163 +lemma finite_set_intervals:
1.164 + assumes px: "P x" and lx: "l \<le> x" and xu: "x \<le> u" and linS: "l\<in> S"
1.165 + 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"
1.166 + 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"
1.167 +proof-
1.168 + let ?Mx = "{y. y\<in> S \<and> y \<le> x}"
1.169 + let ?xM = "{y. y\<in> S \<and> x \<le> y}"
1.170 + let ?a = "Max ?Mx"
1.171 + let ?b = "Min ?xM"
1.172 + have MxS: "?Mx \<subseteq> S" by blast
1.173 + hence fMx: "finite ?Mx" using fS finite_subset by auto
1.174 + from lx linS have linMx: "l \<in> ?Mx" by blast
1.175 + hence Mxne: "?Mx \<noteq> {}" by blast
1.176 + have xMS: "?xM \<subseteq> S" by blast
1.177 + hence fxM: "finite ?xM" using fS finite_subset by auto
1.178 + from xu uinS have linxM: "u \<in> ?xM" by blast
1.179 + hence xMne: "?xM \<noteq> {}" by blast
1.180 + have ax:"?a \<le> x" using Mxne fMx by auto
1.181 + have xb:"x \<le> ?b" using xMne fxM by auto
1.182 + have "?a \<in> ?Mx" using Max_in[OF fMx Mxne] by simp hence ainS: "?a \<in> S" using MxS by blast
1.183 + have "?b \<in> ?xM" using Min_in[OF fxM xMne] by simp hence binS: "?b \<in> S" using xMS by blast
1.184 + have noy:"\<forall> y. ?a < y \<and> y < ?b \<longrightarrow> y \<notin> S"
1.185 + proof(clarsimp)
1.186 + fix y assume ay: "?a < y" and yb: "y < ?b" and yS: "y \<in> S"
1.187 + from yS have "y\<in> ?Mx \<or> y\<in> ?xM" by (auto simp add: linear)
1.188 + moreover {assume "y \<in> ?Mx" hence "y \<le> ?a" using Mxne fMx by auto with ay have "False" by (simp add: not_le[symmetric])}
1.189 + moreover {assume "y \<in> ?xM" hence "?b \<le> y" using xMne fxM by auto with yb have "False" by (simp add: not_le[symmetric])}
1.190 + ultimately show "False" by blast
1.191 + qed
1.192 + from ainS binS noy ax xb px show ?thesis by blast
1.193 +qed
1.194 +
1.195 +lemma finite_set_intervals2:
1.196 + assumes px: "P x" and lx: "l \<le> x" and xu: "x \<le> u" and linS: "l\<in> S"
1.197 + 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"
1.198 + 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)"
1.199 +proof-
1.200 + from finite_set_intervals[where P="P", OF px lx xu linS uinS fS lS Su]
1.201 + obtain a and b where
1.202 + as: "a\<in> S" and bs: "b\<in> S" and noS:"\<forall>y. a < y \<and> y < b \<longrightarrow> y \<notin> S"
1.203 + and axb: "a \<le> x \<and> x \<le> b \<and> P x" by auto
1.204 + from axb have "x= a \<or> x= b \<or> (a < x \<and> x < b)" by (auto simp add: le_less)
1.205 + thus ?thesis using px as bs noS by blast
1.206 +qed
1.207 +
1.208 +end
1.209 +
1.210 +section {* The classical QE after Langford for dense linear orders *}
1.211 +
1.212 +context dense_linear_order
1.213 +begin
1.214 +
1.215 +lemma interval_empty_iff:
1.216 + "{y. x < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
1.217 + by (auto dest: dense)
1.218 +
1.219 +lemma dlo_qe_bnds:
1.220 + assumes ne: "L \<noteq> {}" and neU: "U \<noteq> {}" and fL: "finite L" and fU: "finite U"
1.221 + 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)"
1.222 +proof (simp only: atomize_eq, rule iffI)
1.223 + assume H: "\<exists>x. (\<forall>y\<in>L. y < x) \<and> (\<forall>y\<in>U. x < y)"
1.224 + then obtain x where xL: "\<forall>y\<in>L. y < x" and xU: "\<forall>y\<in>U. x < y" by blast
1.225 + {fix l u assume l: "l \<in> L" and u: "u \<in> U"
1.226 + have "l < x" using xL l by blast
1.227 + also have "x < u" using xU u by blast
1.228 + finally (less_trans) have "l < u" .}
1.229 + thus "\<forall>l\<in>L. \<forall>u\<in>U. l < u" by blast
1.230 +next
1.231 + assume H: "\<forall>l\<in>L. \<forall>u\<in>U. l < u"
1.232 + let ?ML = "Max L"
1.233 + let ?MU = "Min U"
1.234 + from fL ne have th1: "?ML \<in> L" and th1': "\<forall>l\<in>L. l \<le> ?ML" by auto
1.235 + from fU neU have th2: "?MU \<in> U" and th2': "\<forall>u\<in>U. ?MU \<le> u" by auto
1.236 + from th1 th2 H have "?ML < ?MU" by auto
1.237 + with dense obtain w where th3: "?ML < w" and th4: "w < ?MU" by blast
1.238 + from th3 th1' have "\<forall>l \<in> L. l < w" by auto
1.239 + moreover from th4 th2' have "\<forall>u \<in> U. w < u" by auto
1.240 + ultimately show "\<exists>x. (\<forall>y\<in>L. y < x) \<and> (\<forall>y\<in>U. x < y)" by auto
1.241 +qed
1.242 +
1.243 +lemma dlo_qe_noub:
1.244 + assumes ne: "L \<noteq> {}" and fL: "finite L"
1.245 + shows "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> {}. x < y)) \<equiv> True"
1.246 +proof(simp add: atomize_eq)
1.247 + from gt_ex[of "Max L"] obtain M where M: "Max L < M" by blast
1.248 + from ne fL have "\<forall>x \<in> L. x \<le> Max L" by simp
1.249 + with M have "\<forall>x\<in>L. x < M" by (auto intro: le_less_trans)
1.250 + thus "\<exists>x. \<forall>y\<in>L. y < x" by blast
1.251 +qed
1.252 +
1.253 +lemma dlo_qe_nolb:
1.254 + assumes ne: "U \<noteq> {}" and fU: "finite U"
1.255 + shows "(\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y \<in> U. x < y)) \<equiv> True"
1.256 +proof(simp add: atomize_eq)
1.257 + from lt_ex[of "Min U"] obtain M where M: "M < Min U" by blast
1.258 + from ne fU have "\<forall>x \<in> U. Min U \<le> x" by simp
1.259 + with M have "\<forall>x\<in>U. M < x" by (auto intro: less_le_trans)
1.260 + thus "\<exists>x. \<forall>y\<in>U. x < y" by blast
1.261 +qed
1.262 +
1.263 +lemma exists_neq: "\<exists>(x::'a). x \<noteq> t" "\<exists>(x::'a). t \<noteq> x"
1.264 + using gt_ex[of t] by auto
1.265 +
1.266 +lemmas dlo_simps = order_refl less_irrefl not_less not_le exists_neq
1.267 + le_less neq_iff linear less_not_permute
1.268 +
1.269 +lemma axiom: "dense_linear_order (op \<le>) (op <)" by (rule dense_linear_order_axioms)
1.270 +lemma atoms:
1.271 + shows "TERM (less :: 'a \<Rightarrow> _)"
1.272 + and "TERM (less_eq :: 'a \<Rightarrow> _)"
1.273 + and "TERM (op = :: 'a \<Rightarrow> _)" .
1.274 +
1.275 +declare axiom[langford qe: dlo_qe_bnds dlo_qe_nolb dlo_qe_noub gather: gather_start gather_simps atoms: atoms]
1.276 +declare dlo_simps[langfordsimp]
1.277 +
1.278 +end
1.279 +
1.280 +(* FIXME: Move to HOL -- together with the conj_aci_rule in langford.ML *)
1.281 +lemma dnf:
1.282 + "(P & (Q | R)) = ((P&Q) | (P&R))"
1.283 + "((Q | R) & P) = ((Q&P) | (R&P))"
1.284 + by blast+
1.285 +
1.286 +lemmas weak_dnf_simps = simp_thms dnf
1.287 +
1.288 +lemma nnf_simps:
1.289 + "(\<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)"
1.290 + "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"
1.291 + by blast+
1.292 +
1.293 +lemma ex_distrib: "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> ((\<exists>x. P x) \<or> (\<exists>x. Q x))" by blast
1.294 +
1.295 +lemmas dnf_simps = weak_dnf_simps nnf_simps ex_distrib
1.296 +
1.297 +use "~~/src/HOL/Tools/Qelim/langford.ML"
1.298 +method_setup dlo = {*
1.299 + Method.ctxt_args (Method.SIMPLE_METHOD' o LangfordQE.dlo_tac)
1.300 +*} "Langford's algorithm for quantifier elimination in dense linear orders"
1.301 +
1.302 +
1.303 +section {* Contructive dense linear orders yield QE for linear arithmetic over ordered Fields -- see @{text "Arith_Tools.thy"} *}
1.304 +
1.305 +text {* Linear order without upper bounds *}
1.306 +
1.307 +class_locale linorder_stupid_syntax = linorder
1.308 +begin
1.309 +notation
1.310 + less_eq ("op \<sqsubseteq>") and
1.311 + less_eq ("(_/ \<sqsubseteq> _)" [51, 51] 50) and
1.312 + less ("op \<sqsubset>") and
1.313 + less ("(_/ \<sqsubset> _)" [51, 51] 50)
1.314 +
1.315 +end
1.316 +
1.317 +class_locale linorder_no_ub = linorder_stupid_syntax +
1.318 + assumes gt_ex: "\<exists>y. less x y"
1.319 +begin
1.320 +lemma ge_ex: "\<exists>y. x \<sqsubseteq> y" using gt_ex by auto
1.321 +
1.322 +text {* Theorems for @{text "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"} *}
1.323 +lemma pinf_conj:
1.324 + assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
1.325 + and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
1.326 + shows "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
1.327 +proof-
1.328 + from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
1.329 + and z2: "\<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
1.330 + from gt_ex obtain z where z:"ord.max less_eq z1 z2 \<sqsubset> z" by blast
1.331 + from z have zz1: "z1 \<sqsubset> z" and zz2: "z2 \<sqsubset> z" by simp_all
1.332 + {fix x assume H: "z \<sqsubset> x"
1.333 + from less_trans[OF zz1 H] less_trans[OF zz2 H]
1.334 + have "(P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2')" using z1 zz1 z2 zz2 by auto
1.335 + }
1.336 + thus ?thesis by blast
1.337 +qed
1.338 +
1.339 +lemma pinf_disj:
1.340 + assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
1.341 + and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
1.342 + shows "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
1.343 +proof-
1.344 + from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
1.345 + and z2: "\<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
1.346 + from gt_ex obtain z where z:"ord.max less_eq z1 z2 \<sqsubset> z" by blast
1.347 + from z have zz1: "z1 \<sqsubset> z" and zz2: "z2 \<sqsubset> z" by simp_all
1.348 + {fix x assume H: "z \<sqsubset> x"
1.349 + from less_trans[OF zz1 H] less_trans[OF zz2 H]
1.350 + have "(P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2')" using z1 zz1 z2 zz2 by auto
1.351 + }
1.352 + thus ?thesis by blast
1.353 +qed
1.354 +
1.355 +lemma pinf_ex: assumes ex:"\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x"
1.356 +proof-
1.357 + from ex obtain z where z: "\<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast
1.358 + from gt_ex obtain x where x: "z \<sqsubset> x" by blast
1.359 + from z x p1 show ?thesis by blast
1.360 +qed
1.361 +
1.362 +end
1.363 +
1.364 +text {* Linear order without upper bounds *}
1.365 +
1.366 +class_locale linorder_no_lb = linorder_stupid_syntax +
1.367 + assumes lt_ex: "\<exists>y. less y x"
1.368 +begin
1.369 +lemma le_ex: "\<exists>y. y \<sqsubseteq> x" using lt_ex by auto
1.370 +
1.371 +
1.372 +text {* Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"} *}
1.373 +lemma minf_conj:
1.374 + assumes ex1: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
1.375 + and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
1.376 + shows "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
1.377 +proof-
1.378 + 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
1.379 + from lt_ex obtain z where z:"z \<sqsubset> ord.min less_eq z1 z2" by blast
1.380 + from z have zz1: "z \<sqsubset> z1" and zz2: "z \<sqsubset> z2" by simp_all
1.381 + {fix x assume H: "x \<sqsubset> z"
1.382 + from less_trans[OF H zz1] less_trans[OF H zz2]
1.383 + have "(P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2')" using z1 zz1 z2 zz2 by auto
1.384 + }
1.385 + thus ?thesis by blast
1.386 +qed
1.387 +
1.388 +lemma minf_disj:
1.389 + assumes ex1: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
1.390 + and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
1.391 + shows "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
1.392 +proof-
1.393 + 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
1.394 + from lt_ex obtain z where z:"z \<sqsubset> ord.min less_eq z1 z2" by blast
1.395 + from z have zz1: "z \<sqsubset> z1" and zz2: "z \<sqsubset> z2" by simp_all
1.396 + {fix x assume H: "x \<sqsubset> z"
1.397 + from less_trans[OF H zz1] less_trans[OF H zz2]
1.398 + have "(P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2')" using z1 zz1 z2 zz2 by auto
1.399 + }
1.400 + thus ?thesis by blast
1.401 +qed
1.402 +
1.403 +lemma minf_ex: assumes ex:"\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x"
1.404 +proof-
1.405 + from ex obtain z where z: "\<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast
1.406 + from lt_ex obtain x where x: "x \<sqsubset> z" by blast
1.407 + from z x p1 show ?thesis by blast
1.408 +qed
1.409 +
1.410 +end
1.411 +
1.412 +
1.413 +class_locale constr_dense_linear_order = linorder_no_lb + linorder_no_ub +
1.414 + fixes between
1.415 + assumes between_less: "less x y \<Longrightarrow> less x (between x y) \<and> less (between x y) y"
1.416 + and between_same: "between x x = x"
1.417 +
1.418 +class_interpretation constr_dense_linear_order < dense_linear_order
1.419 + apply unfold_locales
1.420 + using gt_ex lt_ex between_less
1.421 + by (auto, rule_tac x="between x y" in exI, simp)
1.422 +
1.423 +context constr_dense_linear_order
1.424 +begin
1.425 +
1.426 +lemma rinf_U:
1.427 + assumes fU: "finite U"
1.428 + 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
1.429 + \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P y )"
1.430 + 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')"
1.431 + and nmi: "\<not> MP" and npi: "\<not> PP" and ex: "\<exists> x. P x"
1.432 + shows "\<exists> u\<in> U. \<exists> u' \<in> U. P (between u u')"
1.433 +proof-
1.434 + from ex obtain x where px: "P x" by blast
1.435 + from px nmi npi nmpiU have "\<exists> u\<in> U. \<exists> u' \<in> U. u \<sqsubseteq> x \<and> x \<sqsubseteq> u'" by auto
1.436 + 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
1.437 + from uU have Une: "U \<noteq> {}" by auto
1.438 + term "linorder.Min less_eq"
1.439 + let ?l = "linorder.Min less_eq U"
1.440 + let ?u = "linorder.Max less_eq U"
1.441 + have linM: "?l \<in> U" using fU Une by simp
1.442 + have uinM: "?u \<in> U" using fU Une by simp
1.443 + have lM: "\<forall> t\<in> U. ?l \<sqsubseteq> t" using Une fU by auto
1.444 + have Mu: "\<forall> t\<in> U. t \<sqsubseteq> ?u" using Une fU by auto
1.445 + have th:"?l \<sqsubseteq> u" using uU Une lM by auto
1.446 + from order_trans[OF th ux] have lx: "?l \<sqsubseteq> x" .
1.447 + have th: "u' \<sqsubseteq> ?u" using uU' Une Mu by simp
1.448 + from order_trans[OF xu' th] have xu: "x \<sqsubseteq> ?u" .
1.449 + from finite_set_intervals2[where P="P",OF px lx xu linM uinM fU lM Mu]
1.450 + have "(\<exists> s\<in> U. P s) \<or>
1.451 + (\<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)" .
1.452 + moreover { fix u assume um: "u\<in>U" and pu: "P u"
1.453 + have "between u u = u" by (simp add: between_same)
1.454 + with um pu have "P (between u u)" by simp
1.455 + with um have ?thesis by blast}
1.456 + moreover{
1.457 + 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"
1.458 + then obtain t1 and t2 where t1M: "t1 \<in> U" and t2M: "t2\<in> U"
1.459 + 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"
1.460 + by blast
1.461 + from less_trans[OF t1x xt2] have t1t2: "t1 \<sqsubset> t2" .
1.462 + let ?u = "between t1 t2"
1.463 + from between_less t1t2 have t1lu: "t1 \<sqsubset> ?u" and ut2: "?u \<sqsubset> t2" by auto
1.464 + from lin_dense noM t1x xt2 px t1lu ut2 have "P ?u" by blast
1.465 + with t1M t2M have ?thesis by blast}
1.466 + ultimately show ?thesis by blast
1.467 + qed
1.468 +
1.469 +theorem fr_eq:
1.470 + assumes fU: "finite U"
1.471 + 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
1.472 + \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P y )"
1.473 + and nmibnd: "\<forall>x. \<not> MP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<sqsubseteq> x)"
1.474 + and npibnd: "\<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. x \<sqsubseteq> u)"
1.475 + 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)"
1.476 + shows "(\<exists> x. P x) \<equiv> (MP \<or> PP \<or> (\<exists> u \<in> U. \<exists> u'\<in> U. P (between u u')))"
1.477 + (is "_ \<equiv> (_ \<or> _ \<or> ?F)" is "?E \<equiv> ?D")
1.478 +proof-
1.479 + {
1.480 + assume px: "\<exists> x. P x"
1.481 + have "MP \<or> PP \<or> (\<not> MP \<and> \<not> PP)" by blast
1.482 + moreover {assume "MP \<or> PP" hence "?D" by blast}
1.483 + moreover {assume nmi: "\<not> MP" and npi: "\<not> PP"
1.484 + from npmibnd[OF nmibnd npibnd]
1.485 + 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')" .
1.486 + from rinf_U[OF fU lin_dense nmpiU nmi npi px] have "?D" by blast}
1.487 + ultimately have "?D" by blast}
1.488 + moreover
1.489 + { assume "?D"
1.490 + moreover {assume m:"MP" from minf_ex[OF mi m] have "?E" .}
1.491 + moreover {assume p: "PP" from pinf_ex[OF pi p] have "?E" . }
1.492 + moreover {assume f:"?F" hence "?E" by blast}
1.493 + ultimately have "?E" by blast}
1.494 + ultimately have "?E = ?D" by blast thus "?E \<equiv> ?D" by simp
1.495 +qed
1.496 +
1.497 +lemmas minf_thms = minf_conj minf_disj minf_eq minf_neq minf_lt minf_le minf_gt minf_ge minf_P
1.498 +lemmas pinf_thms = pinf_conj pinf_disj pinf_eq pinf_neq pinf_lt pinf_le pinf_gt pinf_ge pinf_P
1.499 +
1.500 +lemmas nmi_thms = nmi_conj nmi_disj nmi_eq nmi_neq nmi_lt nmi_le nmi_gt nmi_ge nmi_P
1.501 +lemmas npi_thms = npi_conj npi_disj npi_eq npi_neq npi_lt npi_le npi_gt npi_ge npi_P
1.502 +lemmas lin_dense_thms = 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
1.503 +
1.504 +lemma ferrack_axiom: "constr_dense_linear_order less_eq less between"
1.505 + by (rule constr_dense_linear_order_axioms)
1.506 +lemma atoms:
1.507 + shows "TERM (less :: 'a \<Rightarrow> _)"
1.508 + and "TERM (less_eq :: 'a \<Rightarrow> _)"
1.509 + and "TERM (op = :: 'a \<Rightarrow> _)" .
1.510 +
1.511 +declare ferrack_axiom [ferrack minf: minf_thms pinf: pinf_thms
1.512 + nmi: nmi_thms npi: npi_thms lindense:
1.513 + lin_dense_thms qe: fr_eq atoms: atoms]
1.514 +
1.515 +declaration {*
1.516 +let
1.517 +fun simps phi = map (Morphism.thm phi) [@{thm "not_less"}, @{thm "not_le"}]
1.518 +fun generic_whatis phi =
1.519 + let
1.520 + val [lt, le] = map (Morphism.term phi) [@{term "op \<sqsubset>"}, @{term "op \<sqsubseteq>"}]
1.521 + fun h x t =
1.522 + case term_of t of
1.523 + Const("op =", _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
1.524 + else Ferrante_Rackoff_Data.Nox
1.525 + | @{term "Not"}$(Const("op =", _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
1.526 + else Ferrante_Rackoff_Data.Nox
1.527 + | b$y$z => if Term.could_unify (b, lt) then
1.528 + if term_of x aconv y then Ferrante_Rackoff_Data.Lt
1.529 + else if term_of x aconv z then Ferrante_Rackoff_Data.Gt
1.530 + else Ferrante_Rackoff_Data.Nox
1.531 + else if Term.could_unify (b, le) then
1.532 + if term_of x aconv y then Ferrante_Rackoff_Data.Le
1.533 + else if term_of x aconv z then Ferrante_Rackoff_Data.Ge
1.534 + else Ferrante_Rackoff_Data.Nox
1.535 + else Ferrante_Rackoff_Data.Nox
1.536 + | _ => Ferrante_Rackoff_Data.Nox
1.537 + in h end
1.538 + fun ss phi = HOL_ss addsimps (simps phi)
1.539 +in
1.540 + Ferrante_Rackoff_Data.funs @{thm "ferrack_axiom"}
1.541 + {isolate_conv = K (K (K Thm.reflexive)), whatis = generic_whatis, simpset = ss}
1.542 +end
1.543 +*}
1.544 +
1.545 +end
1.546 +
1.547 +use "~~/src/HOL/Tools/Qelim/ferrante_rackoff.ML"
1.548 +
1.549 +method_setup ferrack = {*
1.550 + Method.ctxt_args (Method.SIMPLE_METHOD' o FerranteRackoff.dlo_tac)
1.551 +*} "Ferrante and Rackoff's algorithm for quantifier elimination in dense linear orders"
1.552 +
1.553 +subsection {* Ferrante and Rackoff algorithm over ordered fields *}
1.554 +
1.555 +lemma neg_prod_lt:"(c\<Colon>'a\<Colon>ordered_field) < 0 \<Longrightarrow> ((c*x < 0) == (x > 0))"
1.556 +proof-
1.557 + assume H: "c < 0"
1.558 + have "c*x < 0 = (0/c < x)" by (simp only: neg_divide_less_eq[OF H] ring_simps)
1.559 + also have "\<dots> = (0 < x)" by simp
1.560 + finally show "(c*x < 0) == (x > 0)" by simp
1.561 +qed
1.562 +
1.563 +lemma pos_prod_lt:"(c\<Colon>'a\<Colon>ordered_field) > 0 \<Longrightarrow> ((c*x < 0) == (x < 0))"
1.564 +proof-
1.565 + assume H: "c > 0"
1.566 + hence "c*x < 0 = (0/c > x)" by (simp only: pos_less_divide_eq[OF H] ring_simps)
1.567 + also have "\<dots> = (0 > x)" by simp
1.568 + finally show "(c*x < 0) == (x < 0)" by simp
1.569 +qed
1.570 +
1.571 +lemma neg_prod_sum_lt: "(c\<Colon>'a\<Colon>ordered_field) < 0 \<Longrightarrow> ((c*x + t< 0) == (x > (- 1/c)*t))"
1.572 +proof-
1.573 + assume H: "c < 0"
1.574 + have "c*x + t< 0 = (c*x < -t)" by (subst less_iff_diff_less_0 [of "c*x" "-t"], simp)
1.575 + also have "\<dots> = (-t/c < x)" by (simp only: neg_divide_less_eq[OF H] ring_simps)
1.576 + also have "\<dots> = ((- 1/c)*t < x)" by simp
1.577 + finally show "(c*x + t < 0) == (x > (- 1/c)*t)" by simp
1.578 +qed
1.579 +
1.580 +lemma pos_prod_sum_lt:"(c\<Colon>'a\<Colon>ordered_field) > 0 \<Longrightarrow> ((c*x + t < 0) == (x < (- 1/c)*t))"
1.581 +proof-
1.582 + assume H: "c > 0"
1.583 + have "c*x + t< 0 = (c*x < -t)" by (subst less_iff_diff_less_0 [of "c*x" "-t"], simp)
1.584 + also have "\<dots> = (-t/c > x)" by (simp only: pos_less_divide_eq[OF H] ring_simps)
1.585 + also have "\<dots> = ((- 1/c)*t > x)" by simp
1.586 + finally show "(c*x + t < 0) == (x < (- 1/c)*t)" by simp
1.587 +qed
1.588 +
1.589 +lemma sum_lt:"((x::'a::pordered_ab_group_add) + t < 0) == (x < - t)"
1.590 + using less_diff_eq[where a= x and b=t and c=0] by simp
1.591 +
1.592 +lemma neg_prod_le:"(c\<Colon>'a\<Colon>ordered_field) < 0 \<Longrightarrow> ((c*x <= 0) == (x >= 0))"
1.593 +proof-
1.594 + assume H: "c < 0"
1.595 + have "c*x <= 0 = (0/c <= x)" by (simp only: neg_divide_le_eq[OF H] ring_simps)
1.596 + also have "\<dots> = (0 <= x)" by simp
1.597 + finally show "(c*x <= 0) == (x >= 0)" by simp
1.598 +qed
1.599 +
1.600 +lemma pos_prod_le:"(c\<Colon>'a\<Colon>ordered_field) > 0 \<Longrightarrow> ((c*x <= 0) == (x <= 0))"
1.601 +proof-
1.602 + assume H: "c > 0"
1.603 + hence "c*x <= 0 = (0/c >= x)" by (simp only: pos_le_divide_eq[OF H] ring_simps)
1.604 + also have "\<dots> = (0 >= x)" by simp
1.605 + finally show "(c*x <= 0) == (x <= 0)" by simp
1.606 +qed
1.607 +
1.608 +lemma neg_prod_sum_le: "(c\<Colon>'a\<Colon>ordered_field) < 0 \<Longrightarrow> ((c*x + t <= 0) == (x >= (- 1/c)*t))"
1.609 +proof-
1.610 + assume H: "c < 0"
1.611 + have "c*x + t <= 0 = (c*x <= -t)" by (subst le_iff_diff_le_0 [of "c*x" "-t"], simp)
1.612 + also have "\<dots> = (-t/c <= x)" by (simp only: neg_divide_le_eq[OF H] ring_simps)
1.613 + also have "\<dots> = ((- 1/c)*t <= x)" by simp
1.614 + finally show "(c*x + t <= 0) == (x >= (- 1/c)*t)" by simp
1.615 +qed
1.616 +
1.617 +lemma pos_prod_sum_le:"(c\<Colon>'a\<Colon>ordered_field) > 0 \<Longrightarrow> ((c*x + t <= 0) == (x <= (- 1/c)*t))"
1.618 +proof-
1.619 + assume H: "c > 0"
1.620 + have "c*x + t <= 0 = (c*x <= -t)" by (subst le_iff_diff_le_0 [of "c*x" "-t"], simp)
1.621 + also have "\<dots> = (-t/c >= x)" by (simp only: pos_le_divide_eq[OF H] ring_simps)
1.622 + also have "\<dots> = ((- 1/c)*t >= x)" by simp
1.623 + finally show "(c*x + t <= 0) == (x <= (- 1/c)*t)" by simp
1.624 +qed
1.625 +
1.626 +lemma sum_le:"((x::'a::pordered_ab_group_add) + t <= 0) == (x <= - t)"
1.627 + using le_diff_eq[where a= x and b=t and c=0] by simp
1.628 +
1.629 +lemma nz_prod_eq:"(c\<Colon>'a\<Colon>ordered_field) \<noteq> 0 \<Longrightarrow> ((c*x = 0) == (x = 0))" by simp
1.630 +lemma nz_prod_sum_eq: "(c\<Colon>'a\<Colon>ordered_field) \<noteq> 0 \<Longrightarrow> ((c*x + t = 0) == (x = (- 1/c)*t))"
1.631 +proof-
1.632 + assume H: "c \<noteq> 0"
1.633 + have "c*x + t = 0 = (c*x = -t)" by (subst eq_iff_diff_eq_0 [of "c*x" "-t"], simp)
1.634 + also have "\<dots> = (x = -t/c)" by (simp only: nonzero_eq_divide_eq[OF H] ring_simps)
1.635 + finally show "(c*x + t = 0) == (x = (- 1/c)*t)" by simp
1.636 +qed
1.637 +lemma sum_eq:"((x::'a::pordered_ab_group_add) + t = 0) == (x = - t)"
1.638 + using eq_diff_eq[where a= x and b=t and c=0] by simp
1.639 +
1.640 +
1.641 +class_interpretation class_ordered_field_dense_linear_order: constr_dense_linear_order
1.642 + ["op <=" "op <"
1.643 + "\<lambda> x y. 1/2 * ((x::'a::{ordered_field,recpower,number_ring}) + y)"]
1.644 +proof (unfold_locales, dlo, dlo, auto)
1.645 + fix x y::'a assume lt: "x < y"
1.646 + from less_half_sum[OF lt] show "x < (x + y) /2" by simp
1.647 +next
1.648 + fix x y::'a assume lt: "x < y"
1.649 + from gt_half_sum[OF lt] show "(x + y) /2 < y" by simp
1.650 +qed
1.651 +
1.652 +declaration{*
1.653 +let
1.654 +fun earlier [] x y = false
1.655 + | earlier (h::t) x y =
1.656 + if h aconvc y then false else if h aconvc x then true else earlier t x y;
1.657 +
1.658 +fun dest_frac ct = case term_of ct of
1.659 + Const (@{const_name "HOL.divide"},_) $ a $ b=>
1.660 + Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
1.661 + | t => Rat.rat_of_int (snd (HOLogic.dest_number t))
1.662 +
1.663 +fun mk_frac phi cT x =
1.664 + let val (a, b) = Rat.quotient_of_rat x
1.665 + in if b = 1 then Numeral.mk_cnumber cT a
1.666 + else Thm.capply
1.667 + (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
1.668 + (Numeral.mk_cnumber cT a))
1.669 + (Numeral.mk_cnumber cT b)
1.670 + end
1.671 +
1.672 +fun whatis x ct = case term_of ct of
1.673 + Const(@{const_name "HOL.plus"}, _)$(Const(@{const_name "HOL.times"},_)$_$y)$_ =>
1.674 + if y aconv term_of x then ("c*x+t",[(funpow 2 Thm.dest_arg1) ct, Thm.dest_arg ct])
1.675 + else ("Nox",[])
1.676 +| Const(@{const_name "HOL.plus"}, _)$y$_ =>
1.677 + if y aconv term_of x then ("x+t",[Thm.dest_arg ct])
1.678 + else ("Nox",[])
1.679 +| Const(@{const_name "HOL.times"}, _)$_$y =>
1.680 + if y aconv term_of x then ("c*x",[Thm.dest_arg1 ct])
1.681 + else ("Nox",[])
1.682 +| t => if t aconv term_of x then ("x",[]) else ("Nox",[]);
1.683 +
1.684 +fun xnormalize_conv ctxt [] ct = reflexive ct
1.685 +| xnormalize_conv ctxt (vs as (x::_)) ct =
1.686 + case term_of ct of
1.687 + Const(@{const_name HOL.less},_)$_$Const(@{const_name "HOL.zero"},_) =>
1.688 + (case whatis x (Thm.dest_arg1 ct) of
1.689 + ("c*x+t",[c,t]) =>
1.690 + let
1.691 + val cr = dest_frac c
1.692 + val clt = Thm.dest_fun2 ct
1.693 + val cz = Thm.dest_arg ct
1.694 + val neg = cr </ Rat.zero
1.695 + val cthp = Simplifier.rewrite (local_simpset_of ctxt)
1.696 + (Thm.capply @{cterm "Trueprop"}
1.697 + (if neg then Thm.capply (Thm.capply clt c) cz
1.698 + else Thm.capply (Thm.capply clt cz) c))
1.699 + val cth = equal_elim (symmetric cthp) TrueI
1.700 + val th = implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x,t])
1.701 + (if neg then @{thm neg_prod_sum_lt} else @{thm pos_prod_sum_lt})) cth
1.702 + val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
1.703 + (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
1.704 + in rth end
1.705 + | ("x+t",[t]) =>
1.706 + let
1.707 + val T = ctyp_of_term x
1.708 + val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_lt"}
1.709 + val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
1.710 + (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
1.711 + in rth end
1.712 + | ("c*x",[c]) =>
1.713 + let
1.714 + val cr = dest_frac c
1.715 + val clt = Thm.dest_fun2 ct
1.716 + val cz = Thm.dest_arg ct
1.717 + val neg = cr </ Rat.zero
1.718 + val cthp = Simplifier.rewrite (local_simpset_of ctxt)
1.719 + (Thm.capply @{cterm "Trueprop"}
1.720 + (if neg then Thm.capply (Thm.capply clt c) cz
1.721 + else Thm.capply (Thm.capply clt cz) c))
1.722 + val cth = equal_elim (symmetric cthp) TrueI
1.723 + val th = implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x])
1.724 + (if neg then @{thm neg_prod_lt} else @{thm pos_prod_lt})) cth
1.725 + val rth = th
1.726 + in rth end
1.727 + | _ => reflexive ct)
1.728 +
1.729 +
1.730 +| Const(@{const_name HOL.less_eq},_)$_$Const(@{const_name "HOL.zero"},_) =>
1.731 + (case whatis x (Thm.dest_arg1 ct) of
1.732 + ("c*x+t",[c,t]) =>
1.733 + let
1.734 + val T = ctyp_of_term x
1.735 + val cr = dest_frac c
1.736 + val clt = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "op <"}
1.737 + val cz = Thm.dest_arg ct
1.738 + val neg = cr </ Rat.zero
1.739 + val cthp = Simplifier.rewrite (local_simpset_of ctxt)
1.740 + (Thm.capply @{cterm "Trueprop"}
1.741 + (if neg then Thm.capply (Thm.capply clt c) cz
1.742 + else Thm.capply (Thm.capply clt cz) c))
1.743 + val cth = equal_elim (symmetric cthp) TrueI
1.744 + val th = implies_elim (instantiate' [SOME T] (map SOME [c,x,t])
1.745 + (if neg then @{thm neg_prod_sum_le} else @{thm pos_prod_sum_le})) cth
1.746 + val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
1.747 + (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
1.748 + in rth end
1.749 + | ("x+t",[t]) =>
1.750 + let
1.751 + val T = ctyp_of_term x
1.752 + val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_le"}
1.753 + val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
1.754 + (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
1.755 + in rth end
1.756 + | ("c*x",[c]) =>
1.757 + let
1.758 + val T = ctyp_of_term x
1.759 + val cr = dest_frac c
1.760 + val clt = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "op <"}
1.761 + val cz = Thm.dest_arg ct
1.762 + val neg = cr </ Rat.zero
1.763 + val cthp = Simplifier.rewrite (local_simpset_of ctxt)
1.764 + (Thm.capply @{cterm "Trueprop"}
1.765 + (if neg then Thm.capply (Thm.capply clt c) cz
1.766 + else Thm.capply (Thm.capply clt cz) c))
1.767 + val cth = equal_elim (symmetric cthp) TrueI
1.768 + val th = implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x])
1.769 + (if neg then @{thm neg_prod_le} else @{thm pos_prod_le})) cth
1.770 + val rth = th
1.771 + in rth end
1.772 + | _ => reflexive ct)
1.773 +
1.774 +| Const("op =",_)$_$Const(@{const_name "HOL.zero"},_) =>
1.775 + (case whatis x (Thm.dest_arg1 ct) of
1.776 + ("c*x+t",[c,t]) =>
1.777 + let
1.778 + val T = ctyp_of_term x
1.779 + val cr = dest_frac c
1.780 + val ceq = Thm.dest_fun2 ct
1.781 + val cz = Thm.dest_arg ct
1.782 + val cthp = Simplifier.rewrite (local_simpset_of ctxt)
1.783 + (Thm.capply @{cterm "Trueprop"}
1.784 + (Thm.capply @{cterm "Not"} (Thm.capply (Thm.capply ceq c) cz)))
1.785 + val cth = equal_elim (symmetric cthp) TrueI
1.786 + val th = implies_elim
1.787 + (instantiate' [SOME T] (map SOME [c,x,t]) @{thm nz_prod_sum_eq}) cth
1.788 + val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
1.789 + (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
1.790 + in rth end
1.791 + | ("x+t",[t]) =>
1.792 + let
1.793 + val T = ctyp_of_term x
1.794 + val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_eq"}
1.795 + val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
1.796 + (Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
1.797 + in rth end
1.798 + | ("c*x",[c]) =>
1.799 + let
1.800 + val T = ctyp_of_term x
1.801 + val cr = dest_frac c
1.802 + val ceq = Thm.dest_fun2 ct
1.803 + val cz = Thm.dest_arg ct
1.804 + val cthp = Simplifier.rewrite (local_simpset_of ctxt)
1.805 + (Thm.capply @{cterm "Trueprop"}
1.806 + (Thm.capply @{cterm "Not"} (Thm.capply (Thm.capply ceq c) cz)))
1.807 + val cth = equal_elim (symmetric cthp) TrueI
1.808 + val rth = implies_elim
1.809 + (instantiate' [SOME T] (map SOME [c,x]) @{thm nz_prod_eq}) cth
1.810 + in rth end
1.811 + | _ => reflexive ct);
1.812 +
1.813 +local
1.814 + val less_iff_diff_less_0 = mk_meta_eq @{thm "less_iff_diff_less_0"}
1.815 + val le_iff_diff_le_0 = mk_meta_eq @{thm "le_iff_diff_le_0"}
1.816 + val eq_iff_diff_eq_0 = mk_meta_eq @{thm "eq_iff_diff_eq_0"}
1.817 +in
1.818 +fun field_isolate_conv phi ctxt vs ct = case term_of ct of
1.819 + Const(@{const_name HOL.less},_)$a$b =>
1.820 + let val (ca,cb) = Thm.dest_binop ct
1.821 + val T = ctyp_of_term ca
1.822 + val th = instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0
1.823 + val nth = Conv.fconv_rule
1.824 + (Conv.arg_conv (Conv.arg1_conv
1.825 + (Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
1.826 + val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
1.827 + in rth end
1.828 +| Const(@{const_name HOL.less_eq},_)$a$b =>
1.829 + let val (ca,cb) = Thm.dest_binop ct
1.830 + val T = ctyp_of_term ca
1.831 + val th = instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0
1.832 + val nth = Conv.fconv_rule
1.833 + (Conv.arg_conv (Conv.arg1_conv
1.834 + (Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
1.835 + val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
1.836 + in rth end
1.837 +
1.838 +| Const("op =",_)$a$b =>
1.839 + let val (ca,cb) = Thm.dest_binop ct
1.840 + val T = ctyp_of_term ca
1.841 + val th = instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0
1.842 + val nth = Conv.fconv_rule
1.843 + (Conv.arg_conv (Conv.arg1_conv
1.844 + (Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
1.845 + val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
1.846 + in rth end
1.847 +| @{term "Not"} $(Const("op =",_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
1.848 +| _ => reflexive ct
1.849 +end;
1.850 +
1.851 +fun classfield_whatis phi =
1.852 + let
1.853 + fun h x t =
1.854 + case term_of t of
1.855 + Const("op =", _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
1.856 + else Ferrante_Rackoff_Data.Nox
1.857 + | @{term "Not"}$(Const("op =", _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
1.858 + else Ferrante_Rackoff_Data.Nox
1.859 + | Const(@{const_name HOL.less},_)$y$z =>
1.860 + if term_of x aconv y then Ferrante_Rackoff_Data.Lt
1.861 + else if term_of x aconv z then Ferrante_Rackoff_Data.Gt
1.862 + else Ferrante_Rackoff_Data.Nox
1.863 + | Const (@{const_name HOL.less_eq},_)$y$z =>
1.864 + if term_of x aconv y then Ferrante_Rackoff_Data.Le
1.865 + else if term_of x aconv z then Ferrante_Rackoff_Data.Ge
1.866 + else Ferrante_Rackoff_Data.Nox
1.867 + | _ => Ferrante_Rackoff_Data.Nox
1.868 + in h end;
1.869 +fun class_field_ss phi =
1.870 + HOL_basic_ss addsimps ([@{thm "linorder_not_less"}, @{thm "linorder_not_le"}])
1.871 + addsplits [@{thm "abs_split"},@{thm "split_max"}, @{thm "split_min"}]
1.872 +
1.873 +in
1.874 +Ferrante_Rackoff_Data.funs @{thm "class_ordered_field_dense_linear_order.ferrack_axiom"}
1.875 + {isolate_conv = field_isolate_conv, whatis = classfield_whatis, simpset = class_field_ss}
1.876 +end
1.877 +*}
1.878 +
1.879 +
1.880 +end