author | haftmann |
Sat, 29 Sep 2007 08:58:51 +0200 | |
changeset 24748 | ee0a0eb6b738 |
parent 24679 | 5b168969ffe0 |
child 24914 | 95cda5dd58d5 |
permissions | -rw-r--r-- |
23453 | 1 |
(* |
2 |
ID: $Id$ |
|
3 |
Author: Amine Chaieb, TU Muenchen |
|
4 |
*) |
|
5 |
||
23470 | 6 |
header {* Dense linear order without endpoints |
23453 | 7 |
and a quantifier elimination procedure in Ferrante and Rackoff style *} |
8 |
||
9 |
theory Dense_Linear_Order |
|
10 |
imports Finite_Set |
|
11 |
uses |
|
23466
886655a150f6
moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
23453
diff
changeset
|
12 |
"Tools/Qelim/qelim.ML" |
23902
c69069242a51
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.
chaieb
parents:
23470
diff
changeset
|
13 |
"Tools/Qelim/langford_data.ML" |
23466
886655a150f6
moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
23453
diff
changeset
|
14 |
"Tools/Qelim/ferrante_rackoff_data.ML" |
23902
c69069242a51
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.
chaieb
parents:
23470
diff
changeset
|
15 |
("Tools/Qelim/langford.ML") |
23466
886655a150f6
moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
23453
diff
changeset
|
16 |
("Tools/Qelim/ferrante_rackoff.ML") |
23453 | 17 |
begin |
18 |
||
23902
c69069242a51
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.
chaieb
parents:
23470
diff
changeset
|
19 |
setup Langford_Data.setup |
23453 | 20 |
setup Ferrante_Rackoff_Data.setup |
21 |
||
24344 | 22 |
context linorder |
23902
c69069242a51
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.
chaieb
parents:
23470
diff
changeset
|
23 |
begin |
c69069242a51
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.
chaieb
parents:
23470
diff
changeset
|
24 |
|
24748 | 25 |
lemma less_not_permute: "\<not> (x \<^loc>< y \<and> y \<^loc>< x)" by (simp add: not_less linear) |
23902
c69069242a51
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.
chaieb
parents:
23470
diff
changeset
|
26 |
|
c69069242a51
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.
chaieb
parents:
23470
diff
changeset
|
27 |
lemma gather_simps: |
c69069242a51
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.
chaieb
parents:
23470
diff
changeset
|
28 |
shows |
24748 | 29 |
"(\<exists>x. (\<forall>y \<in> L. y \<^loc>< x) \<and> (\<forall>y \<in> U. x \<^loc>< y) \<and> x \<^loc>< u \<and> P x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> L. y \<^loc>< x) \<and> (\<forall>y \<in> (insert u U). x \<^loc>< y) \<and> P x)" |
30 |
and "(\<exists>x. (\<forall>y \<in> L. y \<^loc>< x) \<and> (\<forall>y \<in> U. x \<^loc>< y) \<and> l \<^loc>< x \<and> P x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> (insert l L). y \<^loc>< x) \<and> (\<forall>y \<in> U. x \<^loc>< y) \<and> P x)" |
|
31 |
"(\<exists>x. (\<forall>y \<in> L. y \<^loc>< x) \<and> (\<forall>y \<in> U. x \<^loc>< y) \<and> x \<^loc>< u) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> L. y \<^loc>< x) \<and> (\<forall>y \<in> (insert u U). x \<^loc>< y))" |
|
32 |
and "(\<exists>x. (\<forall>y \<in> L. y \<^loc>< x) \<and> (\<forall>y \<in> U. x \<^loc>< y) \<and> l \<^loc>< x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> (insert l L). y \<^loc>< x) \<and> (\<forall>y \<in> U. x \<^loc>< y))" by auto |
|
23902
c69069242a51
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.
chaieb
parents:
23470
diff
changeset
|
33 |
|
c69069242a51
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.
chaieb
parents:
23470
diff
changeset
|
34 |
lemma |
24748 | 35 |
gather_start: "(\<exists>x. P x) \<equiv> (\<exists>x. (\<forall>y \<in> {}. y \<^loc>< x) \<and> (\<forall>y\<in> {}. x \<^loc>< y) \<and> P x)" |
23902
c69069242a51
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.
chaieb
parents:
23470
diff
changeset
|
36 |
by simp |
c69069242a51
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.
chaieb
parents:
23470
diff
changeset
|
37 |
|
24748 | 38 |
text{* Theorems for @{text "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"}*} |
39 |
lemma minf_lt: "\<exists>z . \<forall>x. x \<^loc>< z \<longrightarrow> (x \<^loc>< t \<longleftrightarrow> True)" by auto |
|
40 |
lemma minf_gt: "\<exists>z . \<forall>x. x \<^loc>< z \<longrightarrow> (t \<^loc>< x \<longleftrightarrow> False)" |
|
23453 | 41 |
by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le) |
42 |
||
24748 | 43 |
lemma minf_le: "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (x \<^loc>\<le> t \<longleftrightarrow> True)" by (auto simp add: less_le) |
44 |
lemma minf_ge: "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (t \<^loc>\<le> x \<longleftrightarrow> False)" |
|
23453 | 45 |
by (auto simp add: less_le not_less not_le) |
24748 | 46 |
lemma minf_eq: "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto |
47 |
lemma minf_neq: "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto |
|
48 |
lemma minf_P: "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (P \<longleftrightarrow> P)" by blast |
|
23453 | 49 |
|
24748 | 50 |
text{* Theorems for @{text "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"}*} |
51 |
lemma pinf_gt: "\<exists>z . \<forall>x. z \<^loc>< x \<longrightarrow> (t \<^loc>< x \<longleftrightarrow> True)" by auto |
|
52 |
lemma pinf_lt: "\<exists>z . \<forall>x. z \<^loc>< x \<longrightarrow> (x \<^loc>< t \<longleftrightarrow> False)" |
|
23453 | 53 |
by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le) |
54 |
||
24748 | 55 |
lemma pinf_ge: "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> (t \<^loc>\<le> x \<longleftrightarrow> True)" by (auto simp add: less_le) |
56 |
lemma pinf_le: "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> (x \<^loc>\<le> t \<longleftrightarrow> False)" |
|
23453 | 57 |
by (auto simp add: less_le not_less not_le) |
24748 | 58 |
lemma pinf_eq: "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto |
59 |
lemma pinf_neq: "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto |
|
60 |
lemma pinf_P: "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> (P \<longleftrightarrow> P)" by blast |
|
23453 | 61 |
|
24748 | 62 |
lemma nmi_lt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x \<^loc>< t \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x)" by auto |
63 |
lemma nmi_gt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t \<^loc>< x \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x)" |
|
23453 | 64 |
by (auto simp add: le_less) |
24748 | 65 |
lemma nmi_le: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x\<^loc>\<le> t \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x)" by auto |
66 |
lemma nmi_ge: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t\<^loc>\<le> x \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x)" by auto |
|
67 |
lemma nmi_eq: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> x = t \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x)" by auto |
|
68 |
lemma nmi_neq: "t \<in> U \<Longrightarrow>\<forall>x. \<not>True \<and> x \<noteq> t \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x)" by auto |
|
69 |
lemma nmi_P: "\<forall> x. ~P \<and> P \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x)" by auto |
|
70 |
lemma nmi_conj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x) ; |
|
71 |
\<forall>x. \<not>P2' \<and> P2 x \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x)\<rbrakk> \<Longrightarrow> |
|
72 |
\<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x)" by auto |
|
73 |
lemma nmi_disj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x) ; |
|
74 |
\<forall>x. \<not>P2' \<and> P2 x \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x)\<rbrakk> \<Longrightarrow> |
|
75 |
\<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x)" by auto |
|
23453 | 76 |
|
24748 | 77 |
lemma npi_lt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> x \<^loc>< t \<longrightarrow> (\<exists> u\<in> U. x \<^loc>\<le> u)" by (auto simp add: le_less) |
78 |
lemma npi_gt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> t \<^loc>< x \<longrightarrow> (\<exists> u\<in> U. x \<^loc>\<le> u)" by auto |
|
79 |
lemma npi_le: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> x \<^loc>\<le> t \<longrightarrow> (\<exists> u\<in> U. x \<^loc>\<le> u)" by auto |
|
80 |
lemma npi_ge: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> t \<^loc>\<le> x \<longrightarrow> (\<exists> u\<in> U. x \<^loc>\<le> u)" by auto |
|
81 |
lemma npi_eq: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> x = t \<longrightarrow> (\<exists> u\<in> U. x \<^loc>\<le> u)" by auto |
|
82 |
lemma npi_neq: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x \<noteq> t \<longrightarrow> (\<exists> u\<in> U. x \<^loc>\<le> u )" by auto |
|
83 |
lemma npi_P: "\<forall> x. ~P \<and> P \<longrightarrow> (\<exists> u\<in> U. x \<^loc>\<le> u)" by auto |
|
84 |
lemma npi_conj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow> (\<exists> u\<in> U. x \<^loc>\<le> u) ; \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow> (\<exists> u\<in> U. x \<^loc>\<le> u)\<rbrakk> |
|
85 |
\<Longrightarrow> \<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow> (\<exists> u\<in> U. x \<^loc>\<le> u)" by auto |
|
86 |
lemma npi_disj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow> (\<exists> u\<in> U. x \<^loc>\<le> u) ; \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow> (\<exists> u\<in> U. x \<^loc>\<le> u)\<rbrakk> |
|
87 |
\<Longrightarrow> \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow> (\<exists> u\<in> U. x \<^loc>\<le> u)" by auto |
|
23453 | 88 |
|
24748 | 89 |
lemma lin_dense_lt: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t \<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> x \<^loc>< t \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> y \<^loc>< t)" |
23453 | 90 |
proof(clarsimp) |
24748 | 91 |
fix x l u y assume tU: "t \<in> U" and noU: "\<forall>t. l \<^loc>< t \<and> t \<^loc>< u \<longrightarrow> t \<notin> U" and lx: "l \<^loc>< x" |
92 |
and xu: "x\<^loc><u" and px: "x \<^loc>< t" and ly: "l\<^loc><y" and yu:"y \<^loc>< u" |
|
23453 | 93 |
from tU noU ly yu have tny: "t\<noteq>y" by auto |
24748 | 94 |
{assume H: "t \<^loc>< y" |
23453 | 95 |
from less_trans[OF lx px] less_trans[OF H yu] |
24748 | 96 |
have "l \<^loc>< t \<and> t \<^loc>< u" by simp |
23453 | 97 |
with tU noU have "False" by auto} |
24748 | 98 |
hence "\<not> t \<^loc>< y" by auto hence "y \<^loc>\<le> t" by (simp add: not_less) |
99 |
thus "y \<^loc>< t" using tny by (simp add: less_le) |
|
23453 | 100 |
qed |
101 |
||
24748 | 102 |
lemma lin_dense_gt: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l \<^loc>< x \<and> x \<^loc>< u \<and> t \<^loc>< x \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> t \<^loc>< y)" |
23453 | 103 |
proof(clarsimp) |
104 |
fix x l u y |
|
24748 | 105 |
assume tU: "t \<in> U" and noU: "\<forall>t. l \<^loc>< t \<and> t \<^loc>< u \<longrightarrow> t \<notin> U" and lx: "l \<^loc>< x" and xu: "x\<^loc><u" |
106 |
and px: "t \<^loc>< x" and ly: "l\<^loc><y" and yu:"y \<^loc>< u" |
|
23453 | 107 |
from tU noU ly yu have tny: "t\<noteq>y" by auto |
24748 | 108 |
{assume H: "y\<^loc>< t" |
109 |
from less_trans[OF ly H] less_trans[OF px xu] have "l \<^loc>< t \<and> t \<^loc>< u" by simp |
|
23453 | 110 |
with tU noU have "False" by auto} |
24748 | 111 |
hence "\<not> y\<^loc><t" by auto hence "t \<^loc>\<le> y" by (auto simp add: not_less) |
112 |
thus "t \<^loc>< y" using tny by (simp add:less_le) |
|
23453 | 113 |
qed |
114 |
||
24748 | 115 |
lemma lin_dense_le: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> x \<^loc>\<le> t \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> y\<^loc>\<le> t)" |
23453 | 116 |
proof(clarsimp) |
117 |
fix x l u y |
|
24748 | 118 |
assume tU: "t \<in> U" and noU: "\<forall>t. l \<^loc>< t \<and> t \<^loc>< u \<longrightarrow> t \<notin> U" and lx: "l \<^loc>< x" and xu: "x\<^loc><u" |
119 |
and px: "x \<^loc>\<le> t" and ly: "l\<^loc><y" and yu:"y \<^loc>< u" |
|
23453 | 120 |
from tU noU ly yu have tny: "t\<noteq>y" by auto |
24748 | 121 |
{assume H: "t \<^loc>< y" |
23453 | 122 |
from less_le_trans[OF lx px] less_trans[OF H yu] |
24748 | 123 |
have "l \<^loc>< t \<and> t \<^loc>< u" by simp |
23453 | 124 |
with tU noU have "False" by auto} |
24748 | 125 |
hence "\<not> t \<^loc>< y" by auto thus "y \<^loc>\<le> t" by (simp add: not_less) |
23453 | 126 |
qed |
127 |
||
24748 | 128 |
lemma lin_dense_ge: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> t \<^loc>\<le> x \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> t \<^loc>\<le> y)" |
23453 | 129 |
proof(clarsimp) |
130 |
fix x l u y |
|
24748 | 131 |
assume tU: "t \<in> U" and noU: "\<forall>t. l \<^loc>< t \<and> t \<^loc>< u \<longrightarrow> t \<notin> U" and lx: "l \<^loc>< x" and xu: "x\<^loc><u" |
132 |
and px: "t \<^loc>\<le> x" and ly: "l\<^loc><y" and yu:"y \<^loc>< u" |
|
23453 | 133 |
from tU noU ly yu have tny: "t\<noteq>y" by auto |
24748 | 134 |
{assume H: "y\<^loc>< t" |
23453 | 135 |
from less_trans[OF ly H] le_less_trans[OF px xu] |
24748 | 136 |
have "l \<^loc>< t \<and> t \<^loc>< u" by simp |
23453 | 137 |
with tU noU have "False" by auto} |
24748 | 138 |
hence "\<not> y\<^loc><t" by auto thus "t \<^loc>\<le> y" by (simp add: not_less) |
23453 | 139 |
qed |
24748 | 140 |
lemma lin_dense_eq: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> x = t \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> y= t)" by auto |
141 |
lemma lin_dense_neq: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> x \<noteq> t \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> y\<noteq> t)" by auto |
|
142 |
lemma lin_dense_P: "\<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> P \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> P)" by auto |
|
23453 | 143 |
|
144 |
lemma lin_dense_conj: |
|
24748 | 145 |
"\<lbrakk>\<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> P1 x |
146 |
\<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> P1 y) ; |
|
147 |
\<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> P2 x |
|
148 |
\<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow> |
|
149 |
\<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> (P1 x \<and> P2 x) |
|
150 |
\<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> (P1 y \<and> P2 y))" |
|
23453 | 151 |
by blast |
152 |
lemma lin_dense_disj: |
|
24748 | 153 |
"\<lbrakk>\<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> P1 x |
154 |
\<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> P1 y) ; |
|
155 |
\<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> P2 x |
|
156 |
\<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow> |
|
157 |
\<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> (P1 x \<or> P2 x) |
|
158 |
\<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> (P1 y \<or> P2 y))" |
|
23453 | 159 |
by blast |
160 |
||
24748 | 161 |
lemma npmibnd: "\<lbrakk>\<forall>x. \<not> MP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x); \<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. x \<^loc>\<le> u)\<rbrakk> |
162 |
\<Longrightarrow> \<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<^loc>\<le> x \<and> x \<^loc>\<le> u')" |
|
23453 | 163 |
by auto |
164 |
||
165 |
lemma finite_set_intervals: |
|
24748 | 166 |
assumes px: "P x" and lx: "l \<^loc>\<le> x" and xu: "x \<^loc>\<le> u" and linS: "l\<in> S" |
167 |
and uinS: "u \<in> S" and fS:"finite S" and lS: "\<forall> x\<in> S. l \<^loc>\<le> x" and Su: "\<forall> x\<in> S. x \<^loc>\<le> u" |
|
168 |
shows "\<exists> a \<in> S. \<exists> b \<in> S. (\<forall> y. a \<^loc>< y \<and> y \<^loc>< b \<longrightarrow> y \<notin> S) \<and> a \<^loc>\<le> x \<and> x \<^loc>\<le> b \<and> P x" |
|
23453 | 169 |
proof- |
24748 | 170 |
let ?Mx = "{y. y\<in> S \<and> y \<^loc>\<le> x}" |
171 |
let ?xM = "{y. y\<in> S \<and> x \<^loc>\<le> y}" |
|
23453 | 172 |
let ?a = "Max ?Mx" |
173 |
let ?b = "Min ?xM" |
|
174 |
have MxS: "?Mx \<subseteq> S" by blast |
|
175 |
hence fMx: "finite ?Mx" using fS finite_subset by auto |
|
176 |
from lx linS have linMx: "l \<in> ?Mx" by blast |
|
177 |
hence Mxne: "?Mx \<noteq> {}" by blast |
|
178 |
have xMS: "?xM \<subseteq> S" by blast |
|
179 |
hence fxM: "finite ?xM" using fS finite_subset by auto |
|
180 |
from xu uinS have linxM: "u \<in> ?xM" by blast |
|
181 |
hence xMne: "?xM \<noteq> {}" by blast |
|
24748 | 182 |
have ax:"?a \<^loc>\<le> x" using Mxne fMx by auto |
183 |
have xb:"x \<^loc>\<le> ?b" using xMne fxM by auto |
|
23453 | 184 |
have "?a \<in> ?Mx" using Max_in[OF fMx Mxne] by simp hence ainS: "?a \<in> S" using MxS by blast |
185 |
have "?b \<in> ?xM" using Min_in[OF fxM xMne] by simp hence binS: "?b \<in> S" using xMS by blast |
|
24748 | 186 |
have noy:"\<forall> y. ?a \<^loc>< y \<and> y \<^loc>< ?b \<longrightarrow> y \<notin> S" |
23453 | 187 |
proof(clarsimp) |
24748 | 188 |
fix y assume ay: "?a \<^loc>< y" and yb: "y \<^loc>< ?b" and yS: "y \<in> S" |
23453 | 189 |
from yS have "y\<in> ?Mx \<or> y\<in> ?xM" by (auto simp add: linear) |
24748 | 190 |
moreover {assume "y \<in> ?Mx" hence "y \<^loc>\<le> ?a" using Mxne fMx by auto with ay have "False" by (simp add: not_le[symmetric])} |
191 |
moreover {assume "y \<in> ?xM" hence "?b \<^loc>\<le> y" using xMne fxM by auto with yb have "False" by (simp add: not_le[symmetric])} |
|
23453 | 192 |
ultimately show "False" by blast |
193 |
qed |
|
194 |
from ainS binS noy ax xb px show ?thesis by blast |
|
195 |
qed |
|
196 |
||
197 |
lemma finite_set_intervals2: |
|
24748 | 198 |
assumes px: "P x" and lx: "l \<^loc>\<le> x" and xu: "x \<^loc>\<le> u" and linS: "l\<in> S" |
199 |
and uinS: "u \<in> S" and fS:"finite S" and lS: "\<forall> x\<in> S. l \<^loc>\<le> x" and Su: "\<forall> x\<in> S. x \<^loc>\<le> u" |
|
200 |
shows "(\<exists> s\<in> S. P s) \<or> (\<exists> a \<in> S. \<exists> b \<in> S. (\<forall> y. a \<^loc>< y \<and> y \<^loc>< b \<longrightarrow> y \<notin> S) \<and> a \<^loc>< x \<and> x \<^loc>< b \<and> P x)" |
|
23453 | 201 |
proof- |
202 |
from finite_set_intervals[where P="P", OF px lx xu linS uinS fS lS Su] |
|
203 |
obtain a and b where |
|
24748 | 204 |
as: "a\<in> S" and bs: "b\<in> S" and noS:"\<forall>y. a \<^loc>< y \<and> y \<^loc>< b \<longrightarrow> y \<notin> S" |
205 |
and axb: "a \<^loc>\<le> x \<and> x \<^loc>\<le> b \<and> P x" by auto |
|
206 |
from axb have "x= a \<or> x= b \<or> (a \<^loc>< x \<and> x \<^loc>< b)" by (auto simp add: le_less) |
|
23453 | 207 |
thus ?thesis using px as bs noS by blast |
208 |
qed |
|
209 |
||
210 |
end |
|
211 |
||
24344 | 212 |
section {* The classical QE after Langford for dense linear orders *} |
213 |
||
24422 | 214 |
context dense_linear_order |
24344 | 215 |
begin |
216 |
||
217 |
lemma dlo_qe_bnds: |
|
218 |
assumes ne: "L \<noteq> {}" and neU: "U \<noteq> {}" and fL: "finite L" and fU: "finite U" |
|
24748 | 219 |
shows "(\<exists>x. (\<forall>y \<in> L. y \<^loc>< x) \<and> (\<forall>y \<in> U. x \<^loc>< y)) \<equiv> (\<forall> l \<in> L. \<forall>u \<in> U. l \<^loc>< u)" |
24344 | 220 |
proof (simp only: atomize_eq, rule iffI) |
221 |
assume H: "\<exists>x. (\<forall>y\<in>L. y \<^loc>< x) \<and> (\<forall>y\<in>U. x \<^loc>< y)" |
|
222 |
then obtain x where xL: "\<forall>y\<in>L. y \<^loc>< x" and xU: "\<forall>y\<in>U. x \<^loc>< y" by blast |
|
223 |
{fix l u assume l: "l \<in> L" and u: "u \<in> U" |
|
224 |
from less_trans[OF xL[rule_format, OF l] xU[rule_format, OF u]] |
|
24748 | 225 |
have "l \<^loc>< u" .} |
24344 | 226 |
thus "\<forall>l\<in>L. \<forall>u\<in>U. l \<^loc>< u" by blast |
227 |
next |
|
228 |
assume H: "\<forall>l\<in>L. \<forall>u\<in>U. l \<^loc>< u" |
|
229 |
let ?ML = "Max L" |
|
230 |
let ?MU = "Min U" |
|
24748 | 231 |
from fL ne have th1: "?ML \<in> L" and th1': "\<forall>l\<in>L. l \<^loc>\<le> ?ML" by auto |
232 |
from fU neU have th2: "?MU \<in> U" and th2': "\<forall>u\<in>U. ?MU \<^loc>\<le> u" by auto |
|
233 |
from th1 th2 H have "?ML \<^loc>< ?MU" by auto |
|
234 |
with dense obtain w where th3: "?ML \<^loc>< w" and th4: "w \<^loc>< ?MU" by blast |
|
235 |
from th3 th1' have "\<forall>l \<in> L. l \<^loc>< w" by auto |
|
236 |
moreover from th4 th2' have "\<forall>u \<in> U. w \<^loc>< u" by auto |
|
24344 | 237 |
ultimately show "\<exists>x. (\<forall>y\<in>L. y \<^loc>< x) \<and> (\<forall>y\<in>U. x \<^loc>< y)" by auto |
238 |
qed |
|
239 |
||
240 |
lemma dlo_qe_noub: |
|
241 |
assumes ne: "L \<noteq> {}" and fL: "finite L" |
|
24748 | 242 |
shows "(\<exists>x. (\<forall>y \<in> L. y \<^loc>< x) \<and> (\<forall>y \<in> {}. x \<^loc>< y)) \<equiv> True" |
24344 | 243 |
proof(simp add: atomize_eq) |
24748 | 244 |
from gt_ex[rule_format, of "Max L"] obtain M where M: "Max L \<^loc>< M" by blast |
245 |
from ne fL have "\<forall>x \<in> L. x \<^loc>\<le> Max L" by simp |
|
246 |
with M have "\<forall>x\<in>L. x \<^loc>< M" by (auto intro: le_less_trans) |
|
24344 | 247 |
thus "\<exists>x. \<forall>y\<in>L. y \<^loc>< x" by blast |
248 |
qed |
|
249 |
||
250 |
lemma dlo_qe_nolb: |
|
251 |
assumes ne: "U \<noteq> {}" and fU: "finite U" |
|
24748 | 252 |
shows "(\<exists>x. (\<forall>y \<in> {}. y \<^loc>< x) \<and> (\<forall>y \<in> U. x \<^loc>< y)) \<equiv> True" |
24344 | 253 |
proof(simp add: atomize_eq) |
24748 | 254 |
from lt_ex[rule_format, of "Min U"] obtain M where M: "M \<^loc>< Min U" by blast |
255 |
from ne fU have "\<forall>x \<in> U. Min U \<^loc>\<le> x" by simp |
|
256 |
with M have "\<forall>x\<in>U. M \<^loc>< x" by (auto intro: less_le_trans) |
|
24344 | 257 |
thus "\<exists>x. \<forall>y\<in>U. x \<^loc>< y" by blast |
258 |
qed |
|
259 |
||
260 |
lemma exists_neq: "\<exists>(x::'a). x \<noteq> t" "\<exists>(x::'a). t \<noteq> x" |
|
261 |
using gt_ex[rule_format, of t] by auto |
|
262 |
||
263 |
lemmas dlo_simps = order_refl less_irrefl not_less not_le exists_neq |
|
264 |
le_less neq_iff linear less_not_permute |
|
265 |
||
24748 | 266 |
lemma axiom: "dense_linear_order (op \<^loc>\<le>) (op \<^loc><)" . |
267 |
lemma atoms: |
|
268 |
includes meta_term_syntax |
|
269 |
shows "TERM (less :: 'a \<Rightarrow> _)" |
|
270 |
and "TERM (less_eq :: 'a \<Rightarrow> _)" |
|
271 |
and "TERM (op = :: 'a \<Rightarrow> _)" . |
|
24344 | 272 |
|
273 |
declare axiom[langford qe: dlo_qe_bnds dlo_qe_nolb dlo_qe_noub gather: gather_start gather_simps atoms: atoms] |
|
274 |
declare dlo_simps[langfordsimp] |
|
275 |
||
276 |
end |
|
277 |
||
278 |
(* FIXME: Move to HOL -- together with the conj_aci_rule in langford.ML *) |
|
279 |
lemma dnf: |
|
280 |
"(P & (Q | R)) = ((P&Q) | (P&R))" |
|
281 |
"((Q | R) & P) = ((Q&P) | (R&P))" |
|
282 |
by blast+ |
|
283 |
||
284 |
lemmas weak_dnf_simps = simp_thms dnf |
|
285 |
||
286 |
lemma nnf_simps: |
|
287 |
"(\<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)" |
|
288 |
"(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P" |
|
289 |
by blast+ |
|
290 |
||
291 |
lemma ex_distrib: "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> ((\<exists>x. P x) \<or> (\<exists>x. Q x))" by blast |
|
292 |
||
293 |
lemmas dnf_simps = weak_dnf_simps nnf_simps ex_distrib |
|
294 |
||
295 |
use "Tools/Qelim/langford.ML" |
|
296 |
method_setup dlo = {* |
|
297 |
Method.ctxt_args (Method.SIMPLE_METHOD' o LangfordQE.dlo_tac) |
|
298 |
*} "Langford's algorithm for quantifier elimination in dense linear orders" |
|
299 |
||
300 |
||
301 |
section {* Contructive dense linear orders yield QE for linear arithmetic over ordered Fields -- see @{text "Arith_Tools.thy"} *} |
|
302 |
||
23453 | 303 |
text {* Linear order without upper bounds *} |
304 |
||
24344 | 305 |
class linorder_no_ub = linorder + |
24748 | 306 |
assumes gt_ex: "\<exists>y. x \<^loc>< y" |
23453 | 307 |
begin |
308 |
||
24748 | 309 |
lemma ge_ex: "\<exists>y. x \<^loc>\<le> y" using gt_ex by auto |
23453 | 310 |
|
24748 | 311 |
text {* Theorems for @{text "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"} *} |
23453 | 312 |
lemma pinf_conj: |
24748 | 313 |
assumes ex1: "\<exists>z1. \<forall>x. z1 \<^loc>< x \<longrightarrow> (P1 x \<longleftrightarrow> P1')" |
314 |
and ex2: "\<exists>z2. \<forall>x. z2 \<^loc>< x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" |
|
315 |
shows "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))" |
|
23453 | 316 |
proof- |
24748 | 317 |
from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 \<^loc>< x \<longrightarrow> (P1 x \<longleftrightarrow> P1')" |
318 |
and z2: "\<forall>x. z2 \<^loc>< x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast |
|
319 |
from gt_ex obtain z where z:"max z1 z2 \<^loc>< z" by blast |
|
320 |
from z have zz1: "z1 \<^loc>< z" and zz2: "z2 \<^loc>< z" by simp_all |
|
321 |
{fix x assume H: "z \<^loc>< x" |
|
23453 | 322 |
from less_trans[OF zz1 H] less_trans[OF zz2 H] |
323 |
have "(P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2')" using z1 zz1 z2 zz2 by auto |
|
324 |
} |
|
325 |
thus ?thesis by blast |
|
326 |
qed |
|
327 |
||
328 |
lemma pinf_disj: |
|
24748 | 329 |
assumes ex1: "\<exists>z1. \<forall>x. z1 \<^loc>< x \<longrightarrow> (P1 x \<longleftrightarrow> P1')" |
330 |
and ex2: "\<exists>z2. \<forall>x. z2 \<^loc>< x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" |
|
331 |
shows "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))" |
|
23453 | 332 |
proof- |
24748 | 333 |
from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 \<^loc>< x \<longrightarrow> (P1 x \<longleftrightarrow> P1')" |
334 |
and z2: "\<forall>x. z2 \<^loc>< x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast |
|
335 |
from gt_ex obtain z where z:"max z1 z2 \<^loc>< z" by blast |
|
336 |
from z have zz1: "z1 \<^loc>< z" and zz2: "z2 \<^loc>< z" by simp_all |
|
337 |
{fix x assume H: "z \<^loc>< x" |
|
23453 | 338 |
from less_trans[OF zz1 H] less_trans[OF zz2 H] |
339 |
have "(P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2')" using z1 zz1 z2 zz2 by auto |
|
340 |
} |
|
341 |
thus ?thesis by blast |
|
342 |
qed |
|
343 |
||
24748 | 344 |
lemma pinf_ex: assumes ex:"\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x" |
23453 | 345 |
proof- |
24748 | 346 |
from ex obtain z where z: "\<forall>x. z \<^loc>< x \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast |
347 |
from gt_ex obtain x where x: "z \<^loc>< x" by blast |
|
23453 | 348 |
from z x p1 show ?thesis by blast |
349 |
qed |
|
350 |
||
351 |
end |
|
352 |
||
353 |
text {* Linear order without upper bounds *} |
|
354 |
||
24344 | 355 |
class linorder_no_lb = linorder + |
24748 | 356 |
assumes lt_ex: "\<exists>y. y \<^loc>< x" |
23453 | 357 |
begin |
358 |
||
24748 | 359 |
lemma le_ex: "\<exists>y. y \<^loc>\<le> x" using lt_ex by auto |
23453 | 360 |
|
361 |
||
24748 | 362 |
text {* Theorems for @{text "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"} *} |
23453 | 363 |
lemma minf_conj: |
24748 | 364 |
assumes ex1: "\<exists>z1. \<forall>x. x \<^loc>< z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')" |
365 |
and ex2: "\<exists>z2. \<forall>x. x \<^loc>< z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')" |
|
366 |
shows "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))" |
|
23453 | 367 |
proof- |
24748 | 368 |
from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. x \<^loc>< z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"and z2: "\<forall>x. x \<^loc>< z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast |
369 |
from lt_ex obtain z where z:"z \<^loc>< min z1 z2" by blast |
|
370 |
from z have zz1: "z \<^loc>< z1" and zz2: "z \<^loc>< z2" by simp_all |
|
371 |
{fix x assume H: "x \<^loc>< z" |
|
23453 | 372 |
from less_trans[OF H zz1] less_trans[OF H zz2] |
373 |
have "(P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2')" using z1 zz1 z2 zz2 by auto |
|
374 |
} |
|
375 |
thus ?thesis by blast |
|
376 |
qed |
|
377 |
||
378 |
lemma minf_disj: |
|
24748 | 379 |
assumes ex1: "\<exists>z1. \<forall>x. x \<^loc>< z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')" |
380 |
and ex2: "\<exists>z2. \<forall>x. x \<^loc>< z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')" |
|
381 |
shows "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))" |
|
23453 | 382 |
proof- |
24748 | 383 |
from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. x \<^loc>< z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"and z2: "\<forall>x. x \<^loc>< z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast |
384 |
from lt_ex obtain z where z:"z \<^loc>< min z1 z2" by blast |
|
385 |
from z have zz1: "z \<^loc>< z1" and zz2: "z \<^loc>< z2" by simp_all |
|
386 |
{fix x assume H: "x \<^loc>< z" |
|
23453 | 387 |
from less_trans[OF H zz1] less_trans[OF H zz2] |
388 |
have "(P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2')" using z1 zz1 z2 zz2 by auto |
|
389 |
} |
|
390 |
thus ?thesis by blast |
|
391 |
qed |
|
392 |
||
24748 | 393 |
lemma minf_ex: assumes ex:"\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x" |
23453 | 394 |
proof- |
24748 | 395 |
from ex obtain z where z: "\<forall>x. x \<^loc>< z \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast |
396 |
from lt_ex obtain x where x: "x \<^loc>< z" by blast |
|
23453 | 397 |
from z x p1 show ?thesis by blast |
398 |
qed |
|
399 |
||
400 |
end |
|
401 |
||
24344 | 402 |
|
403 |
class constr_dense_linear_order = linorder_no_lb + linorder_no_ub + |
|
23453 | 404 |
fixes between |
24748 | 405 |
assumes between_less: "x \<^loc>< y \<Longrightarrow> x \<^loc>< between x y \<and> between x y \<^loc>< y" |
24398
8d83b1e7c3dd
Axioms for class no longer use object-universal quantifiers
chaieb
parents:
24344
diff
changeset
|
406 |
and between_same: "between x x = x" |
23902
c69069242a51
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.
chaieb
parents:
23470
diff
changeset
|
407 |
|
24344 | 408 |
instance advanced constr_dense_linear_order < dense_linear_order |
23902
c69069242a51
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.
chaieb
parents:
23470
diff
changeset
|
409 |
apply unfold_locales |
c69069242a51
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.
chaieb
parents:
23470
diff
changeset
|
410 |
using gt_ex lt_ex between_less |
c69069242a51
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.
chaieb
parents:
23470
diff
changeset
|
411 |
by (auto, rule_tac x="between x y" in exI, simp) |
24422 | 412 |
(*FIXME*) |
413 |
lemmas gt_ex = dense_linear_order_class.less_eq_less.gt_ex |
|
414 |
lemmas lt_ex = dense_linear_order_class.less_eq_less.lt_ex |
|
415 |
lemmas dense = dense_linear_order_class.less_eq_less.dense |
|
23902
c69069242a51
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.
chaieb
parents:
23470
diff
changeset
|
416 |
|
c69069242a51
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.
chaieb
parents:
23470
diff
changeset
|
417 |
context constr_dense_linear_order |
23453 | 418 |
begin |
419 |
||
420 |
lemma rinf_U: |
|
421 |
assumes fU: "finite U" |
|
24748 | 422 |
and lin_dense: "\<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> P x |
423 |
\<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> P y )" |
|
424 |
and nmpiU: "\<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<^loc>\<le> x \<and> x \<^loc>\<le> u')" |
|
23453 | 425 |
and nmi: "\<not> MP" and npi: "\<not> PP" and ex: "\<exists> x. P x" |
426 |
shows "\<exists> u\<in> U. \<exists> u' \<in> U. P (between u u')" |
|
427 |
proof- |
|
428 |
from ex obtain x where px: "P x" by blast |
|
24748 | 429 |
from px nmi npi nmpiU have "\<exists> u\<in> U. \<exists> u' \<in> U. u \<^loc>\<le> x \<and> x \<^loc>\<le> u'" by auto |
430 |
then obtain u and u' where uU:"u\<in> U" and uU': "u' \<in> U" and ux:"u \<^loc>\<le> x" and xu':"x \<^loc>\<le> u'" by auto |
|
23453 | 431 |
from uU have Une: "U \<noteq> {}" by auto |
432 |
let ?l = "Min U" |
|
433 |
let ?u = "Max U" |
|
434 |
have linM: "?l \<in> U" using fU Une by simp |
|
435 |
have uinM: "?u \<in> U" using fU Une by simp |
|
24748 | 436 |
have lM: "\<forall> t\<in> U. ?l \<^loc>\<le> t" using Une fU by auto |
437 |
have Mu: "\<forall> t\<in> U. t \<^loc>\<le> ?u" using Une fU by auto |
|
438 |
have th:"?l \<^loc>\<le> u" using uU Une lM by auto |
|
439 |
from order_trans[OF th ux] have lx: "?l \<^loc>\<le> x" . |
|
440 |
have th: "u' \<^loc>\<le> ?u" using uU' Une Mu by simp |
|
441 |
from order_trans[OF xu' th] have xu: "x \<^loc>\<le> ?u" . |
|
23453 | 442 |
from finite_set_intervals2[where P="P",OF px lx xu linM uinM fU lM Mu] |
443 |
have "(\<exists> s\<in> U. P s) \<or> |
|
24748 | 444 |
(\<exists> t1\<in> U. \<exists> t2 \<in> U. (\<forall> y. t1 \<^loc>< y \<and> y \<^loc>< t2 \<longrightarrow> y \<notin> U) \<and> t1 \<^loc>< x \<and> x \<^loc>< t2 \<and> P x)" . |
23453 | 445 |
moreover { fix u assume um: "u\<in>U" and pu: "P u" |
446 |
have "between u u = u" by (simp add: between_same) |
|
447 |
with um pu have "P (between u u)" by simp |
|
448 |
with um have ?thesis by blast} |
|
449 |
moreover{ |
|
24748 | 450 |
assume "\<exists> t1\<in> U. \<exists> t2 \<in> U. (\<forall> y. t1 \<^loc>< y \<and> y \<^loc>< t2 \<longrightarrow> y \<notin> U) \<and> t1 \<^loc>< x \<and> x \<^loc>< t2 \<and> P x" |
23453 | 451 |
then obtain t1 and t2 where t1M: "t1 \<in> U" and t2M: "t2\<in> U" |
24748 | 452 |
and noM: "\<forall> y. t1 \<^loc>< y \<and> y \<^loc>< t2 \<longrightarrow> y \<notin> U" and t1x: "t1 \<^loc>< x" and xt2: "x \<^loc>< t2" and px: "P x" |
23453 | 453 |
by blast |
24748 | 454 |
from less_trans[OF t1x xt2] have t1t2: "t1 \<^loc>< t2" . |
23453 | 455 |
let ?u = "between t1 t2" |
24748 | 456 |
from between_less t1t2 have t1lu: "t1 \<^loc>< ?u" and ut2: "?u \<^loc>< t2" by auto |
23453 | 457 |
from lin_dense[rule_format, OF] noM t1x xt2 px t1lu ut2 have "P ?u" by blast |
458 |
with t1M t2M have ?thesis by blast} |
|
459 |
ultimately show ?thesis by blast |
|
460 |
qed |
|
461 |
||
462 |
theorem fr_eq: |
|
463 |
assumes fU: "finite U" |
|
24748 | 464 |
and lin_dense: "\<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> P x |
465 |
\<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> P y )" |
|
466 |
and nmibnd: "\<forall>x. \<not> MP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x)" |
|
467 |
and npibnd: "\<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. x \<^loc>\<le> u)" |
|
468 |
and mi: "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (P x = MP)" and pi: "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> (P x = PP)" |
|
23453 | 469 |
shows "(\<exists> x. P x) \<equiv> (MP \<or> PP \<or> (\<exists> u \<in> U. \<exists> u'\<in> U. P (between u u')))" |
470 |
(is "_ \<equiv> (_ \<or> _ \<or> ?F)" is "?E \<equiv> ?D") |
|
471 |
proof- |
|
472 |
{ |
|
473 |
assume px: "\<exists> x. P x" |
|
474 |
have "MP \<or> PP \<or> (\<not> MP \<and> \<not> PP)" by blast |
|
475 |
moreover {assume "MP \<or> PP" hence "?D" by blast} |
|
476 |
moreover {assume nmi: "\<not> MP" and npi: "\<not> PP" |
|
477 |
from npmibnd[OF nmibnd npibnd] |
|
24748 | 478 |
have nmpiU: "\<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<^loc>\<le> x \<and> x \<^loc>\<le> u')" . |
23453 | 479 |
from rinf_U[OF fU lin_dense nmpiU nmi npi px] have "?D" by blast} |
480 |
ultimately have "?D" by blast} |
|
481 |
moreover |
|
482 |
{ assume "?D" |
|
483 |
moreover {assume m:"MP" from minf_ex[OF mi m] have "?E" .} |
|
484 |
moreover {assume p: "PP" from pinf_ex[OF pi p] have "?E" . } |
|
485 |
moreover {assume f:"?F" hence "?E" by blast} |
|
486 |
ultimately have "?E" by blast} |
|
487 |
ultimately have "?E = ?D" by blast thus "?E \<equiv> ?D" by simp |
|
488 |
qed |
|
489 |
||
490 |
lemmas minf_thms = minf_conj minf_disj minf_eq minf_neq minf_lt minf_le minf_gt minf_ge minf_P |
|
491 |
lemmas pinf_thms = pinf_conj pinf_disj pinf_eq pinf_neq pinf_lt pinf_le pinf_gt pinf_ge pinf_P |
|
492 |
||
493 |
lemmas nmi_thms = nmi_conj nmi_disj nmi_eq nmi_neq nmi_lt nmi_le nmi_gt nmi_ge nmi_P |
|
494 |
lemmas npi_thms = npi_conj npi_disj npi_eq npi_neq npi_lt npi_le npi_gt npi_ge npi_P |
|
495 |
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 |
|
496 |
||
23902
c69069242a51
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.
chaieb
parents:
23470
diff
changeset
|
497 |
lemma ferrack_axiom: "constr_dense_linear_order less_eq less between" by fact |
24748 | 498 |
lemma atoms: |
499 |
includes meta_term_syntax |
|
500 |
shows "TERM (less :: 'a \<Rightarrow> _)" |
|
501 |
and "TERM (less_eq :: 'a \<Rightarrow> _)" |
|
502 |
and "TERM (op = :: 'a \<Rightarrow> _)" . |
|
23453 | 503 |
|
23902
c69069242a51
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.
chaieb
parents:
23470
diff
changeset
|
504 |
declare ferrack_axiom [ferrack minf: minf_thms pinf: pinf_thms |
23453 | 505 |
nmi: nmi_thms npi: npi_thms lindense: |
506 |
lin_dense_thms qe: fr_eq atoms: atoms] |
|
507 |
||
508 |
declaration {* |
|
509 |
let |
|
23902
c69069242a51
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.
chaieb
parents:
23470
diff
changeset
|
510 |
fun simps phi = map (Morphism.thm phi) [@{thm "not_less"}, @{thm "not_le"}] |
23453 | 511 |
fun generic_whatis phi = |
512 |
let |
|
24748 | 513 |
val [lt, le] = map (Morphism.term phi) [@{term "op \<^loc><"}, @{term "op \<^loc>\<le>"}] |
23453 | 514 |
fun h x t = |
515 |
case term_of t of |
|
516 |
Const("op =", _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq |
|
517 |
else Ferrante_Rackoff_Data.Nox |
|
518 |
| @{term "Not"}$(Const("op =", _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq |
|
519 |
else Ferrante_Rackoff_Data.Nox |
|
520 |
| b$y$z => if Term.could_unify (b, lt) then |
|
521 |
if term_of x aconv y then Ferrante_Rackoff_Data.Lt |
|
522 |
else if term_of x aconv z then Ferrante_Rackoff_Data.Gt |
|
523 |
else Ferrante_Rackoff_Data.Nox |
|
524 |
else if Term.could_unify (b, le) then |
|
525 |
if term_of x aconv y then Ferrante_Rackoff_Data.Le |
|
526 |
else if term_of x aconv z then Ferrante_Rackoff_Data.Ge |
|
527 |
else Ferrante_Rackoff_Data.Nox |
|
528 |
else Ferrante_Rackoff_Data.Nox |
|
529 |
| _ => Ferrante_Rackoff_Data.Nox |
|
530 |
in h end |
|
23902
c69069242a51
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.
chaieb
parents:
23470
diff
changeset
|
531 |
fun ss phi = HOL_ss addsimps (simps phi) |
23453 | 532 |
in |
533 |
Ferrante_Rackoff_Data.funs @{thm "ferrack_axiom"} |
|
534 |
{isolate_conv = K (K (K Thm.reflexive)), whatis = generic_whatis, simpset = ss} |
|
535 |
end |
|
536 |
*} |
|
537 |
||
538 |
end |
|
539 |
||
23466
886655a150f6
moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents:
23453
diff
changeset
|
540 |
use "Tools/Qelim/ferrante_rackoff.ML" |
23453 | 541 |
|
23902
c69069242a51
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.
chaieb
parents:
23470
diff
changeset
|
542 |
method_setup ferrack = {* |
23453 | 543 |
Method.ctxt_args (Method.SIMPLE_METHOD' o FerranteRackoff.dlo_tac) |
544 |
*} "Ferrante and Rackoff's algorithm for quantifier elimination in dense linear orders" |
|
545 |
||
24081 | 546 |
end |