Added quantifier elimination in dense linear orders after Langford; locale dense_linear_order renamed to constr_dense_linear_order (since it requires the beween constant). locale dense_linear_order is now the classical definition of DLO. constr_dense_linear_order is an instance of dense_linear_order; Method dlo now applies the langford QE, odl Method dlo renamed to ferrack, since it ia a QE only in interpretations where between is interpreted in a manner to vanish after substitution.
1.1 --- a/src/HOL/Dense_Linear_Order.thy Sun Jul 22 17:53:42 2007 +0200
1.2 +++ b/src/HOL/Dense_Linear_Order.thy Sun Jul 22 17:53:45 2007 +0200
1.3 @@ -10,12 +10,144 @@
1.4 imports Finite_Set
1.5 uses
1.6 "Tools/Qelim/qelim.ML"
1.7 + "Tools/Qelim/langford_data.ML"
1.8 "Tools/Qelim/ferrante_rackoff_data.ML"
1.9 + ("Tools/Qelim/langford.ML")
1.10 ("Tools/Qelim/ferrante_rackoff.ML")
1.11 begin
1.12
1.13 +
1.14 +setup Langford_Data.setup
1.15 setup Ferrante_Rackoff_Data.setup
1.16
1.17 +section {* The classical QE after Langford for dense linear orders *}
1.18 +
1.19 +locale dense_linear_order = Linorder +
1.20 + assumes gt_ex: "\<forall>x. \<exists>y. x \<sqsubset> y"
1.21 + and lt_ex: "\<forall>x. \<exists>y. y \<sqsubset> x"
1.22 + and dense: "\<forall>x y. x \<sqsubset> y \<longrightarrow> (\<exists>z. x \<sqsubset> z \<and> z \<sqsubset> y)"
1.23 +begin
1.24 +
1.25 +lemma dlo_qe_bnds:
1.26 + assumes ne: "L \<noteq> {}" and neU: "U \<noteq> {}" and fL: "finite L" and fU: "finite U"
1.27 + shows "(\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y)) \<equiv> (\<forall> l \<in> L. \<forall>u \<in> U. l \<sqsubset> u)"
1.28 +proof (simp only: atomize_eq, rule iffI)
1.29 + assume H: "\<exists>x. (\<forall>y\<in>L. y \<^loc>< x) \<and> (\<forall>y\<in>U. x \<^loc>< y)"
1.30 + then obtain x where xL: "\<forall>y\<in>L. y \<^loc>< x" and xU: "\<forall>y\<in>U. x \<^loc>< y" by blast
1.31 + {fix l u assume l: "l \<in> L" and u: "u \<in> U"
1.32 + from less_trans[OF xL[rule_format, OF l] xU[rule_format, OF u]]
1.33 + have "l \<sqsubset> u" .}
1.34 + thus "\<forall>l\<in>L. \<forall>u\<in>U. l \<^loc>< u" by blast
1.35 +next
1.36 + assume H: "\<forall>l\<in>L. \<forall>u\<in>U. l \<^loc>< u"
1.37 + let ?ML = "Max L"
1.38 + let ?MU = "Min U"
1.39 + from fL ne have th1: "?ML \<in> L" and th1': "\<forall>l\<in>L. l \<sqsubseteq> ?ML" by auto
1.40 + from fU neU have th2: "?MU \<in> U" and th2': "\<forall>u\<in>U. ?MU \<sqsubseteq> u" by auto
1.41 + from th1 th2 H have "?ML \<sqsubset> ?MU" by auto
1.42 + with dense obtain w where th3: "?ML \<sqsubset> w" and th4: "w \<sqsubset> ?MU" by blast
1.43 + from th3 th1' have "\<forall>l \<in> L. l \<sqsubset> w"
1.44 + apply auto
1.45 + apply (erule_tac x="l" in ballE)
1.46 + by (auto intro: le_less_trans)
1.47 +
1.48 + moreover from th4 th2' have "\<forall>u \<in> U. w \<sqsubset> u"
1.49 + apply auto
1.50 + apply (erule_tac x="u" in ballE)
1.51 + by (auto intro: less_le_trans)
1.52 + ultimately show "\<exists>x. (\<forall>y\<in>L. y \<^loc>< x) \<and> (\<forall>y\<in>U. x \<^loc>< y)" by auto
1.53 +qed
1.54 +
1.55 +lemma dlo_qe_noub:
1.56 + assumes ne: "L \<noteq> {}" and fL: "finite L"
1.57 + shows "(\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> {}. x \<sqsubset> y)) \<equiv> True"
1.58 +proof(simp add: atomize_eq)
1.59 + from gt_ex[rule_format, of "Max L"] obtain M where M: "Max L \<sqsubset> M" by blast
1.60 + from ne fL have "\<forall>x \<in> L. x \<sqsubseteq> Max L" by simp
1.61 + with M have "\<forall>x\<in>L. x \<sqsubset> M" by (auto intro: le_less_trans)
1.62 + thus "\<exists>x. \<forall>y\<in>L. y \<^loc>< x" by blast
1.63 +qed
1.64 +
1.65 +lemma dlo_qe_nolb:
1.66 + assumes ne: "U \<noteq> {}" and fU: "finite U"
1.67 + shows "(\<exists>x. (\<forall>y \<in> {}. y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y)) \<equiv> True"
1.68 +proof(simp add: atomize_eq)
1.69 + from lt_ex[rule_format, of "Min U"] obtain M where M: "M \<sqsubset> Min U" by blast
1.70 + from ne fU have "\<forall>x \<in> U. Min U \<sqsubseteq> x" by simp
1.71 + with M have "\<forall>x\<in>U. M \<sqsubset> x" by (auto intro: less_le_trans)
1.72 + thus "\<exists>x. \<forall>y\<in>U. x \<^loc>< y" by blast
1.73 +qed
1.74 +
1.75 +lemma gather_simps:
1.76 + shows
1.77 + "(\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y) \<and> x \<sqsubset> u \<and> P x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> (insert u U). x \<sqsubset> y) \<and> P x)"
1.78 + and "(\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y) \<and> l \<sqsubset> x \<and> P x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> (insert l L). y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y) \<and> P x)"
1.79 + "(\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y) \<and> x \<sqsubset> u) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> (insert u U). x \<sqsubset> y))"
1.80 + and "(\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y) \<and> l \<sqsubset> x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> (insert l L). y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y))" by auto
1.81 +
1.82 +lemma
1.83 + gather_start: "(\<exists>x. P x) \<equiv> (\<exists>x. (\<forall>y \<in> {}. y \<^loc>< x) \<and> (\<forall>y\<in> {}. x \<sqsubset> y) \<and> P x)"
1.84 + by simp
1.85 +
1.86 +lemma exists_neq: "\<exists>(x::'a). x \<noteq> t" "\<exists>(x::'a). t \<noteq> x"
1.87 + using gt_ex[rule_format, of t] by auto
1.88 +
1.89 +lemma less_not_permute: "\<not> (x \<sqsubset> y \<and> y \<sqsubset> x)" by (simp add: not_less linear)
1.90 +
1.91 +lemmas dlo_simps = order_refl less_irrefl not_less not_le exists_neq
1.92 + le_less neq_iff linear less_not_permute
1.93 +
1.94 +lemma axiom: "dense_linear_order (op \<sqsubseteq>) (op \<sqsubset>)" .
1.95 +lemma atoms: includes meta_term_syntax
1.96 + shows "TERM (op \<sqsubset> :: 'a \<Rightarrow> _)" and "TERM (op \<sqsubseteq>)" and "TERM (op = :: 'a \<Rightarrow> _)" .
1.97 +
1.98 +declare axiom[langford qe: dlo_qe_bnds dlo_qe_nolb dlo_qe_noub gather: gather_start gather_simps atoms: atoms]
1.99 +declare dlo_simps[langfordsimp]
1.100 +end
1.101 + (* FIXME: Move to HOL -- together with the conj_aci_rule in langford.ML *)
1.102 +
1.103 +lemma dnf:
1.104 + "(P & (Q | R)) = ((P&Q) | (P&R))"
1.105 + "((Q | R) & P) = ((Q&P) | (R&P))"
1.106 + by blast+
1.107 +
1.108 +lemmas weak_dnf_simps = simp_thms dnf
1.109 +
1.110 +
1.111 +lemma nnf_simps:
1.112 + "(\<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.113 + "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"
1.114 + by blast+
1.115 +
1.116 +lemma ex_distrib: "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> ((\<exists>x. P x) \<or> (\<exists>x. Q x))" by blast
1.117 +
1.118 +lemmas dnf_simps = weak_dnf_simps nnf_simps ex_distrib
1.119 +
1.120 +use "Tools/Qelim/langford.ML"
1.121 +
1.122 +method_setup dlo = {*
1.123 + Method.ctxt_args (Method.SIMPLE_METHOD' o LangfordQE.dlo_tac)
1.124 +*} "Langford's algorithm for quantifier elimination in dense linear orders"
1.125 +
1.126 +interpretation dlo_ordring_class: dense_linear_order["op \<le> :: 'a::{ordered_field} \<Rightarrow> _" "op <"]
1.127 +apply unfold_locales
1.128 +apply auto
1.129 +apply (rule_tac x = "x + 1" in exI, simp)
1.130 +apply (rule_tac x = "x - 1" in exI, simp)
1.131 +apply (rule_tac x = "(x + y) / (1 + 1)" in exI)
1.132 +apply (rule conjI)
1.133 +apply (rule less_half_sum, simp)
1.134 +apply (rule gt_half_sum, simp)
1.135 +done
1.136 +
1.137 +lemma (in dense_linear_order) "\<forall>a b. (\<exists>x. a \<sqsubset> x \<and> x\<sqsubset> b) \<longleftrightarrow> (a \<sqsubset> b)"
1.138 + by dlo
1.139 +
1.140 +lemma "\<forall>(a::'a::ordered_field) b. (\<exists>x. a < x \<and> x< b) \<longleftrightarrow> (a < b)"
1.141 + by dlo
1.142 +
1.143 +section {* Contructive dense linear orders yield QE for linear arithmetic over ordered Fields -- see Arith_Tools.thy *}
1.144 +
1.145 context Linorder
1.146 begin
1.147
1.148 @@ -291,10 +423,17 @@
1.149
1.150 end
1.151
1.152 -locale dense_linear_order = linorder_no_lb + linorder_no_ub +
1.153 +locale constr_dense_linear_order = linorder_no_lb + linorder_no_ub +
1.154 fixes between
1.155 assumes between_less: "\<forall>x y. x \<sqsubset> y \<longrightarrow> x \<sqsubset> between x y \<and> between x y \<sqsubset> y"
1.156 and between_same: "\<forall>x. between x x = x"
1.157 +
1.158 +interpretation constr_dense_linear_order < dense_linear_order
1.159 + apply unfold_locales
1.160 + using gt_ex lt_ex between_less
1.161 + by (auto, rule_tac x="between x y" in exI, simp)
1.162 +
1.163 +context constr_dense_linear_order
1.164 begin
1.165
1.166 lemma rinf_U:
1.167 @@ -374,21 +513,21 @@
1.168 lemmas npi_thms = npi_conj npi_disj npi_eq npi_neq npi_lt npi_le npi_gt npi_ge npi_P
1.169 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.170
1.171 -lemma ferrack_axiom: "dense_linear_order less_eq less between" by fact
1.172 +lemma ferrack_axiom: "constr_dense_linear_order less_eq less between" by fact
1.173 lemma atoms: includes meta_term_syntax
1.174 shows "TERM (op \<sqsubset> :: 'a \<Rightarrow> _)" and "TERM (op \<sqsubseteq>)" and "TERM (op = :: 'a \<Rightarrow> _)" .
1.175
1.176 -declare ferrack_axiom [dlo minf: minf_thms pinf: pinf_thms
1.177 +declare ferrack_axiom [ferrack minf: minf_thms pinf: pinf_thms
1.178 nmi: nmi_thms npi: npi_thms lindense:
1.179 lin_dense_thms qe: fr_eq atoms: atoms]
1.180
1.181 declaration {*
1.182 let
1.183 +fun simps phi = map (Morphism.thm phi) [@{thm "not_less"}, @{thm "not_le"}]
1.184 fun generic_whatis phi =
1.185 let
1.186 val [lt, le] = map (Morphism.term phi)
1.187 (ProofContext.read_term_pats @{typ "dummy"} @{context} ["op \<sqsubset>", "op \<sqsubseteq>"]) (* FIXME avoid read? *)
1.188 - val le = Morphism.term phi @{term "op \<sqsubseteq>"}
1.189 fun h x t =
1.190 case term_of t of
1.191 Const("op =", _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
1.192 @@ -406,7 +545,7 @@
1.193 else Ferrante_Rackoff_Data.Nox
1.194 | _ => Ferrante_Rackoff_Data.Nox
1.195 in h end
1.196 - val ss = K (HOL_ss addsimps [@{thm "not_less"}, @{thm "not_le"}])
1.197 + fun ss phi = HOL_ss addsimps (simps phi)
1.198 in
1.199 Ferrante_Rackoff_Data.funs @{thm "ferrack_axiom"}
1.200 {isolate_conv = K (K (K Thm.reflexive)), whatis = generic_whatis, simpset = ss}
1.201 @@ -415,9 +554,10 @@
1.202
1.203 end
1.204
1.205 +
1.206 use "Tools/Qelim/ferrante_rackoff.ML"
1.207
1.208 -method_setup dlo = {*
1.209 +method_setup ferrack = {*
1.210 Method.ctxt_args (Method.SIMPLE_METHOD' o FerranteRackoff.dlo_tac)
1.211 *} "Ferrante and Rackoff's algorithm for quantifier elimination in dense linear orders"
1.212