--- a/src/HOL/Dense_Linear_Order.thy Mon Aug 20 18:07:26 2007 +0200
+++ b/src/HOL/Dense_Linear_Order.thy Mon Aug 20 18:07:28 2007 +0200
@@ -16,67 +16,13 @@
("Tools/Qelim/ferrante_rackoff.ML")
begin
-
setup Langford_Data.setup
setup Ferrante_Rackoff_Data.setup
-section {* The classical QE after Langford for dense linear orders *}
-
-locale dense_linear_order = Linorder +
- assumes gt_ex: "\<forall>x. \<exists>y. x \<sqsubset> y"
- and lt_ex: "\<forall>x. \<exists>y. y \<sqsubset> x"
- and dense: "\<forall>x y. x \<sqsubset> y \<longrightarrow> (\<exists>z. x \<sqsubset> z \<and> z \<sqsubset> y)"
+context linorder
begin
-lemma dlo_qe_bnds:
- assumes ne: "L \<noteq> {}" and neU: "U \<noteq> {}" and fL: "finite L" and fU: "finite U"
- 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)"
-proof (simp only: atomize_eq, rule iffI)
- assume H: "\<exists>x. (\<forall>y\<in>L. y \<^loc>< x) \<and> (\<forall>y\<in>U. x \<^loc>< y)"
- then obtain x where xL: "\<forall>y\<in>L. y \<^loc>< x" and xU: "\<forall>y\<in>U. x \<^loc>< y" by blast
- {fix l u assume l: "l \<in> L" and u: "u \<in> U"
- from less_trans[OF xL[rule_format, OF l] xU[rule_format, OF u]]
- have "l \<sqsubset> u" .}
- thus "\<forall>l\<in>L. \<forall>u\<in>U. l \<^loc>< u" by blast
-next
- assume H: "\<forall>l\<in>L. \<forall>u\<in>U. l \<^loc>< u"
- let ?ML = "Max L"
- let ?MU = "Min U"
- from fL ne have th1: "?ML \<in> L" and th1': "\<forall>l\<in>L. l \<sqsubseteq> ?ML" by auto
- from fU neU have th2: "?MU \<in> U" and th2': "\<forall>u\<in>U. ?MU \<sqsubseteq> u" by auto
- from th1 th2 H have "?ML \<sqsubset> ?MU" by auto
- with dense obtain w where th3: "?ML \<sqsubset> w" and th4: "w \<sqsubset> ?MU" by blast
- from th3 th1' have "\<forall>l \<in> L. l \<sqsubset> w"
- apply auto
- apply (erule_tac x="l" in ballE)
- by (auto intro: le_less_trans)
-
- moreover from th4 th2' have "\<forall>u \<in> U. w \<sqsubset> u"
- apply auto
- apply (erule_tac x="u" in ballE)
- by (auto intro: less_le_trans)
- ultimately show "\<exists>x. (\<forall>y\<in>L. y \<^loc>< x) \<and> (\<forall>y\<in>U. x \<^loc>< y)" by auto
-qed
-
-lemma dlo_qe_noub:
- assumes ne: "L \<noteq> {}" and fL: "finite L"
- shows "(\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> {}. x \<sqsubset> y)) \<equiv> True"
-proof(simp add: atomize_eq)
- from gt_ex[rule_format, of "Max L"] obtain M where M: "Max L \<sqsubset> M" by blast
- from ne fL have "\<forall>x \<in> L. x \<sqsubseteq> Max L" by simp
- with M have "\<forall>x\<in>L. x \<sqsubset> M" by (auto intro: le_less_trans)
- thus "\<exists>x. \<forall>y\<in>L. y \<^loc>< x" by blast
-qed
-
-lemma dlo_qe_nolb:
- assumes ne: "U \<noteq> {}" and fU: "finite U"
- shows "(\<exists>x. (\<forall>y \<in> {}. y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y)) \<equiv> True"
-proof(simp add: atomize_eq)
- from lt_ex[rule_format, of "Min U"] obtain M where M: "M \<sqsubset> Min U" by blast
- from ne fU have "\<forall>x \<in> U. Min U \<sqsubseteq> x" by simp
- with M have "\<forall>x\<in>U. M \<sqsubset> x" by (auto intro: less_le_trans)
- thus "\<exists>x. \<forall>y\<in>U. x \<^loc>< y" by blast
-qed
+lemma less_not_permute: "\<not> (x \<sqsubset> y \<and> y \<sqsubset> x)" by (simp add: not_less linear)
lemma gather_simps:
shows
@@ -89,61 +35,6 @@
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)"
by simp
-lemma exists_neq: "\<exists>(x::'a). x \<noteq> t" "\<exists>(x::'a). t \<noteq> x"
- using gt_ex[rule_format, of t] by auto
-
-lemma less_not_permute: "\<not> (x \<sqsubset> y \<and> y \<sqsubset> x)" by (simp add: not_less linear)
-
-lemmas dlo_simps = order_refl less_irrefl not_less not_le exists_neq
- le_less neq_iff linear less_not_permute
-
-lemma axiom: "dense_linear_order (op \<sqsubseteq>) (op \<sqsubset>)" .
-lemma atoms: includes meta_term_syntax
- shows "TERM (op \<sqsubset> :: 'a \<Rightarrow> _)" and "TERM (op \<sqsubseteq>)" and "TERM (op = :: 'a \<Rightarrow> _)" .
-
-declare axiom[langford qe: dlo_qe_bnds dlo_qe_nolb dlo_qe_noub gather: gather_start gather_simps atoms: atoms]
-declare dlo_simps[langfordsimp]
-end
- (* FIXME: Move to HOL -- together with the conj_aci_rule in langford.ML *)
-
-lemma dnf:
- "(P & (Q | R)) = ((P&Q) | (P&R))"
- "((Q | R) & P) = ((Q&P) | (R&P))"
- by blast+
-
-lemmas weak_dnf_simps = simp_thms dnf
-
-
-lemma nnf_simps:
- "(\<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)"
- "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"
- by blast+
-
-lemma ex_distrib: "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> ((\<exists>x. P x) \<or> (\<exists>x. Q x))" by blast
-
-lemmas dnf_simps = weak_dnf_simps nnf_simps ex_distrib
-
-use "Tools/Qelim/langford.ML"
-method_setup dlo = {*
- Method.ctxt_args (Method.SIMPLE_METHOD' o LangfordQE.dlo_tac)
-*} "Langford's algorithm for quantifier elimination in dense linear orders"
-
-interpretation dlo_ordring_class: dense_linear_order["op \<le> :: 'a::{ordered_field} \<Rightarrow> _" "op <"]
-apply unfold_locales
-apply auto
-apply (rule_tac x = "x + 1" in exI, simp)
-apply (rule_tac x = "x - 1" in exI, simp)
-apply (rule_tac x = "(x + y) / (1 + 1)" in exI)
-apply (rule conjI)
-apply (rule less_half_sum, simp)
-apply (rule gt_half_sum, simp)
-done
-
-section {* Contructive dense linear orders yield QE for linear arithmetic over ordered Fields -- see @{text "Arith_Tools.thy"} *}
-
-context Linorder
-begin
-
text{* Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"}*}
lemma minf_lt: "\<exists>z . \<forall>x. x \<sqsubset> z \<longrightarrow> (x \<sqsubset> t \<longleftrightarrow> True)" by auto
lemma minf_gt: "\<exists>z . \<forall>x. x \<sqsubset> z \<longrightarrow> (t \<sqsubset> x \<longleftrightarrow> False)"
@@ -303,7 +194,6 @@
from ainS binS noy ax xb px show ?thesis by blast
qed
-
lemma finite_set_intervals2:
assumes px: "P x" and lx: "l \<sqsubseteq> x" and xu: "x \<sqsubseteq> u" and linS: "l\<in> S"
and uinS: "u \<in> S" and fS:"finite S" and lS: "\<forall> x\<in> S. l \<sqsubseteq> x" and Su: "\<forall> x\<in> S. x \<sqsubseteq> u"
@@ -319,9 +209,121 @@
end
+section {* The classical QE after Langford for dense linear orders *}
+
+class dense_linear_order = linorder +
+ assumes gt_ex: "\<forall>x. \<exists>y. x \<sqsubset> y"
+ and lt_ex: "\<forall>x. \<exists>y. y \<sqsubset> x"
+ and dense: "\<forall>x y. x \<sqsubset> y \<longrightarrow> (\<exists>z. x \<sqsubset> z \<and> z \<sqsubset> y)"
+begin
+
+lemma dlo_qe_bnds:
+ assumes ne: "L \<noteq> {}" and neU: "U \<noteq> {}" and fL: "finite L" and fU: "finite U"
+ 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)"
+proof (simp only: atomize_eq, rule iffI)
+ assume H: "\<exists>x. (\<forall>y\<in>L. y \<^loc>< x) \<and> (\<forall>y\<in>U. x \<^loc>< y)"
+ then obtain x where xL: "\<forall>y\<in>L. y \<^loc>< x" and xU: "\<forall>y\<in>U. x \<^loc>< y" by blast
+ {fix l u assume l: "l \<in> L" and u: "u \<in> U"
+ from less_trans[OF xL[rule_format, OF l] xU[rule_format, OF u]]
+ have "l \<sqsubset> u" .}
+ thus "\<forall>l\<in>L. \<forall>u\<in>U. l \<^loc>< u" by blast
+next
+ assume H: "\<forall>l\<in>L. \<forall>u\<in>U. l \<^loc>< u"
+ let ?ML = "Max L"
+ let ?MU = "Min U"
+ from fL ne have th1: "?ML \<in> L" and th1': "\<forall>l\<in>L. l \<sqsubseteq> ?ML" by auto
+ from fU neU have th2: "?MU \<in> U" and th2': "\<forall>u\<in>U. ?MU \<sqsubseteq> u" by auto
+ from th1 th2 H have "?ML \<sqsubset> ?MU" by auto
+ with dense obtain w where th3: "?ML \<sqsubset> w" and th4: "w \<sqsubset> ?MU" by blast
+ from th3 th1' have "\<forall>l \<in> L. l \<sqsubset> w"
+ apply auto
+ apply (erule_tac x="l" in ballE)
+ by (auto intro: le_less_trans)
+
+ moreover from th4 th2' have "\<forall>u \<in> U. w \<sqsubset> u"
+ apply auto
+ apply (erule_tac x="u" in ballE)
+ by (auto intro: less_le_trans)
+ ultimately show "\<exists>x. (\<forall>y\<in>L. y \<^loc>< x) \<and> (\<forall>y\<in>U. x \<^loc>< y)" by auto
+qed
+
+lemma dlo_qe_noub:
+ assumes ne: "L \<noteq> {}" and fL: "finite L"
+ shows "(\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> {}. x \<sqsubset> y)) \<equiv> True"
+proof(simp add: atomize_eq)
+ from gt_ex[rule_format, of "Max L"] obtain M where M: "Max L \<sqsubset> M" by blast
+ from ne fL have "\<forall>x \<in> L. x \<sqsubseteq> Max L" by simp
+ with M have "\<forall>x\<in>L. x \<sqsubset> M" by (auto intro: le_less_trans)
+ thus "\<exists>x. \<forall>y\<in>L. y \<^loc>< x" by blast
+qed
+
+lemma dlo_qe_nolb:
+ assumes ne: "U \<noteq> {}" and fU: "finite U"
+ shows "(\<exists>x. (\<forall>y \<in> {}. y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y)) \<equiv> True"
+proof(simp add: atomize_eq)
+ from lt_ex[rule_format, of "Min U"] obtain M where M: "M \<sqsubset> Min U" by blast
+ from ne fU have "\<forall>x \<in> U. Min U \<sqsubseteq> x" by simp
+ with M have "\<forall>x\<in>U. M \<sqsubset> x" by (auto intro: less_le_trans)
+ thus "\<exists>x. \<forall>y\<in>U. x \<^loc>< y" by blast
+qed
+
+lemma exists_neq: "\<exists>(x::'a). x \<noteq> t" "\<exists>(x::'a). t \<noteq> x"
+ using gt_ex[rule_format, of t] by auto
+
+lemmas dlo_simps = order_refl less_irrefl not_less not_le exists_neq
+ le_less neq_iff linear less_not_permute
+
+lemma axiom: "dense_linear_order (op \<sqsubseteq>) (op \<sqsubset>)" .
+lemma atoms: includes meta_term_syntax
+ shows "TERM (op \<sqsubset> :: 'a \<Rightarrow> _)" and "TERM (op \<sqsubseteq>)" and "TERM (op = :: 'a \<Rightarrow> _)" .
+
+declare axiom[langford qe: dlo_qe_bnds dlo_qe_nolb dlo_qe_noub gather: gather_start gather_simps atoms: atoms]
+declare dlo_simps[langfordsimp]
+
+end
+
+(* FIXME: Move to HOL -- together with the conj_aci_rule in langford.ML *)
+lemma dnf:
+ "(P & (Q | R)) = ((P&Q) | (P&R))"
+ "((Q | R) & P) = ((Q&P) | (R&P))"
+ by blast+
+
+lemmas weak_dnf_simps = simp_thms dnf
+
+lemma nnf_simps:
+ "(\<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)"
+ "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"
+ by blast+
+
+lemma ex_distrib: "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> ((\<exists>x. P x) \<or> (\<exists>x. Q x))" by blast
+
+lemmas dnf_simps = weak_dnf_simps nnf_simps ex_distrib
+
+use "Tools/Qelim/langford.ML"
+method_setup dlo = {*
+ Method.ctxt_args (Method.SIMPLE_METHOD' o LangfordQE.dlo_tac)
+*} "Langford's algorithm for quantifier elimination in dense linear orders"
+
+interpretation dlo_ordring_class: dense_linear_order ["op \<le> \<Colon> 'a\<Colon>ordered_field \<Rightarrow> _" "op <"]
+apply unfold_locales
+apply auto
+apply (rule_tac x = "x + 1" in exI, simp)
+apply (rule_tac x = "x - 1" in exI, simp)
+apply (rule_tac x = "(x + y) / (1 + 1)" in exI)
+apply (rule conjI)
+apply (rule less_half_sum, simp)
+apply (rule gt_half_sum, simp)
+done
+
+
+section {* Contructive dense linear orders yield QE for linear arithmetic over ordered Fields -- see @{text "Arith_Tools.thy"} *}
+
+
+
text {* Linear order without upper bounds *}
-locale linorder_no_ub = Linorder + assumes gt_ex: "\<forall>x. \<exists>y. x \<sqsubset> y"
+class linorder_no_ub = linorder +
+ assumes gt_ex: "\<forall>x. \<exists>y. x \<sqsubset> y"
begin
lemma ge_ex: "\<forall>x. \<exists>y. x \<sqsubseteq> y" using gt_ex by auto
@@ -370,7 +372,8 @@
text {* Linear order without upper bounds *}
-locale linorder_no_lb = Linorder + assumes lt_ex: "\<forall>x. \<exists>y. y \<sqsubset> x"
+class linorder_no_lb = linorder +
+ assumes lt_ex: "\<forall>x. \<exists>y. y \<sqsubset> x"
begin
lemma le_ex: "\<forall>x. \<exists>y. y \<sqsubseteq> x" using lt_ex by auto
@@ -416,12 +419,13 @@
end
-locale constr_dense_linear_order = linorder_no_lb + linorder_no_ub +
+
+class constr_dense_linear_order = linorder_no_lb + linorder_no_ub +
fixes between
assumes between_less: "\<forall>x y. x \<sqsubset> y \<longrightarrow> x \<sqsubset> between x y \<and> between x y \<sqsubset> y"
and between_same: "\<forall>x. between x x = x"
-interpretation constr_dense_linear_order < dense_linear_order
+instance advanced constr_dense_linear_order < dense_linear_order
apply unfold_locales
using gt_ex lt_ex between_less
by (auto, rule_tac x="between x y" in exI, simp)
@@ -547,11 +551,14 @@
end
-
use "Tools/Qelim/ferrante_rackoff.ML"
method_setup ferrack = {*
Method.ctxt_args (Method.SIMPLE_METHOD' o FerranteRackoff.dlo_tac)
*} "Ferrante and Rackoff's algorithm for quantifier elimination in dense linear orders"
+
+(*FIXME: synchronize dense orders with existing algebra*)
+lemmas dense = Ring_and_Field.dense
+
end
--- a/src/HOL/ex/Meson_Test.thy Mon Aug 20 18:07:26 2007 +0200
+++ b/src/HOL/ex/Meson_Test.thy Mon Aug 20 18:07:28 2007 +0200
@@ -11,7 +11,7 @@
below and constants declared in HOL!
*}
-hide const subset member quotient
+hide const subset member quotient between
text {*