23453
|
1 |
(*
|
|
2 |
ID: $Id$
|
|
3 |
Author: Amine Chaieb, TU Muenchen
|
|
4 |
*)
|
|
5 |
|
|
6 |
header {* Dense linear order witout endpoints
|
|
7 |
and a quantifier elimination procedure in Ferrante and Rackoff style *}
|
|
8 |
|
|
9 |
theory Dense_Linear_Order
|
|
10 |
imports Finite_Set
|
|
11 |
uses
|
|
12 |
"Tools/qelim.ML"
|
|
13 |
"Tools/Ferrante_Rackoff/ferrante_rackoff_data.ML"
|
|
14 |
("Tools/Ferrante_Rackoff/ferrante_rackoff.ML")
|
|
15 |
begin
|
|
16 |
|
|
17 |
setup Ferrante_Rackoff_Data.setup
|
|
18 |
|
|
19 |
context Linorder
|
|
20 |
begin
|
|
21 |
|
|
22 |
text{* Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"}*}
|
|
23 |
lemma minf_lt: "\<exists>z . \<forall>x. x \<sqsubset> z \<longrightarrow> (x \<sqsubset> t \<longleftrightarrow> True)" by auto
|
|
24 |
lemma minf_gt: "\<exists>z . \<forall>x. x \<sqsubset> z \<longrightarrow> (t \<sqsubset> x \<longleftrightarrow> False)"
|
|
25 |
by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le)
|
|
26 |
|
|
27 |
lemma minf_le: "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (x \<sqsubseteq> t \<longleftrightarrow> True)" by (auto simp add: less_le)
|
|
28 |
lemma minf_ge: "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (t \<sqsubseteq> x \<longleftrightarrow> False)"
|
|
29 |
by (auto simp add: less_le not_less not_le)
|
|
30 |
lemma minf_eq: "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
|
|
31 |
lemma minf_neq: "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
|
|
32 |
lemma minf_P: "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P \<longleftrightarrow> P)" by blast
|
|
33 |
|
|
34 |
text{* Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"}*}
|
|
35 |
lemma pinf_gt: "\<exists>z . \<forall>x. z \<sqsubset> x \<longrightarrow> (t \<sqsubset> x \<longleftrightarrow> True)" by auto
|
|
36 |
lemma pinf_lt: "\<exists>z . \<forall>x. z \<sqsubset> x \<longrightarrow> (x \<sqsubset> t \<longleftrightarrow> False)"
|
|
37 |
by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le)
|
|
38 |
|
|
39 |
lemma pinf_ge: "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (t \<sqsubseteq> x \<longleftrightarrow> True)" by (auto simp add: less_le)
|
|
40 |
lemma pinf_le: "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (x \<sqsubseteq> t \<longleftrightarrow> False)"
|
|
41 |
by (auto simp add: less_le not_less not_le)
|
|
42 |
lemma pinf_eq: "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
|
|
43 |
lemma pinf_neq: "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
|
|
44 |
lemma pinf_P: "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P \<longleftrightarrow> P)" by blast
|
|
45 |
|
|
46 |
lemma nmi_lt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x \<sqsubset> t \<longrightarrow> (\<exists> u\<in> U. u \<sqsubseteq> x)" by auto
|
|
47 |
lemma nmi_gt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t \<sqsubset> x \<longrightarrow> (\<exists> u\<in> U. u \<sqsubseteq> x)"
|
|
48 |
by (auto simp add: le_less)
|
|
49 |
lemma nmi_le: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x\<sqsubseteq> t \<longrightarrow> (\<exists> u\<in> U. u \<sqsubseteq> x)" by auto
|
|
50 |
lemma nmi_ge: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t\<sqsubseteq> x \<longrightarrow> (\<exists> u\<in> U. u \<sqsubseteq> x)" by auto
|
|
51 |
lemma nmi_eq: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> x = t \<longrightarrow> (\<exists> u\<in> U. u \<sqsubseteq> x)" by auto
|
|
52 |
lemma nmi_neq: "t \<in> U \<Longrightarrow>\<forall>x. \<not>True \<and> x \<noteq> t \<longrightarrow> (\<exists> u\<in> U. u \<sqsubseteq> x)" by auto
|
|
53 |
lemma nmi_P: "\<forall> x. ~P \<and> P \<longrightarrow> (\<exists> u\<in> U. u \<sqsubseteq> x)" by auto
|
|
54 |
lemma nmi_conj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow> (\<exists> u\<in> U. u \<sqsubseteq> x) ;
|
|
55 |
\<forall>x. \<not>P2' \<and> P2 x \<longrightarrow> (\<exists> u\<in> U. u \<sqsubseteq> x)\<rbrakk> \<Longrightarrow>
|
|
56 |
\<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow> (\<exists> u\<in> U. u \<sqsubseteq> x)" by auto
|
|
57 |
lemma nmi_disj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow> (\<exists> u\<in> U. u \<sqsubseteq> x) ;
|
|
58 |
\<forall>x. \<not>P2' \<and> P2 x \<longrightarrow> (\<exists> u\<in> U. u \<sqsubseteq> x)\<rbrakk> \<Longrightarrow>
|
|
59 |
\<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow> (\<exists> u\<in> U. u \<sqsubseteq> x)" by auto
|
|
60 |
|
|
61 |
lemma npi_lt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> x \<sqsubset> t \<longrightarrow> (\<exists> u\<in> U. x \<sqsubseteq> u)" by (auto simp add: le_less)
|
|
62 |
lemma npi_gt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> t \<sqsubset> x \<longrightarrow> (\<exists> u\<in> U. x \<sqsubseteq> u)" by auto
|
|
63 |
lemma npi_le: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> x \<sqsubseteq> t \<longrightarrow> (\<exists> u\<in> U. x \<sqsubseteq> u)" by auto
|
|
64 |
lemma npi_ge: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> t \<sqsubseteq> x \<longrightarrow> (\<exists> u\<in> U. x \<sqsubseteq> u)" by auto
|
|
65 |
lemma npi_eq: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> x = t \<longrightarrow> (\<exists> u\<in> U. x \<sqsubseteq> u)" by auto
|
|
66 |
lemma npi_neq: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x \<noteq> t \<longrightarrow> (\<exists> u\<in> U. x \<sqsubseteq> u )" by auto
|
|
67 |
lemma npi_P: "\<forall> x. ~P \<and> P \<longrightarrow> (\<exists> u\<in> U. x \<sqsubseteq> u)" by auto
|
|
68 |
lemma npi_conj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow> (\<exists> u\<in> U. x \<sqsubseteq> u) ; \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow> (\<exists> u\<in> U. x \<sqsubseteq> u)\<rbrakk>
|
|
69 |
\<Longrightarrow> \<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow> (\<exists> u\<in> U. x \<sqsubseteq> u)" by auto
|
|
70 |
lemma npi_disj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow> (\<exists> u\<in> U. x \<sqsubseteq> u) ; \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow> (\<exists> u\<in> U. x \<sqsubseteq> u)\<rbrakk>
|
|
71 |
\<Longrightarrow> \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow> (\<exists> u\<in> U. x \<sqsubseteq> u)" by auto
|
|
72 |
|
|
73 |
lemma lin_dense_lt: "t \<in> U \<Longrightarrow> \<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> x \<sqsubset> t \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> y \<sqsubset> t)"
|
|
74 |
proof(clarsimp)
|
|
75 |
fix x l u y assume tU: "t \<in> U" and noU: "\<forall>t. l \<sqsubset> t \<and> t \<sqsubset> u \<longrightarrow> t \<notin> U" and lx: "l \<sqsubset> x"
|
|
76 |
and xu: "x\<sqsubset>u" and px: "x \<sqsubset> t" and ly: "l\<sqsubset>y" and yu:"y \<sqsubset> u"
|
|
77 |
from tU noU ly yu have tny: "t\<noteq>y" by auto
|
|
78 |
{assume H: "t \<sqsubset> y"
|
|
79 |
from less_trans[OF lx px] less_trans[OF H yu]
|
|
80 |
have "l \<sqsubset> t \<and> t \<sqsubset> u" by simp
|
|
81 |
with tU noU have "False" by auto}
|
|
82 |
hence "\<not> t \<sqsubset> y" by auto hence "y \<sqsubseteq> t" by (simp add: not_less)
|
|
83 |
thus "y \<sqsubset> t" using tny by (simp add: less_le)
|
|
84 |
qed
|
|
85 |
|
|
86 |
lemma lin_dense_gt: "t \<in> U \<Longrightarrow> \<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> t \<sqsubset> x \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> t \<sqsubset> y)"
|
|
87 |
proof(clarsimp)
|
|
88 |
fix x l u y
|
|
89 |
assume tU: "t \<in> U" and noU: "\<forall>t. l \<sqsubset> t \<and> t \<sqsubset> u \<longrightarrow> t \<notin> U" and lx: "l \<sqsubset> x" and xu: "x\<sqsubset>u"
|
|
90 |
and px: "t \<sqsubset> x" and ly: "l\<sqsubset>y" and yu:"y \<sqsubset> u"
|
|
91 |
from tU noU ly yu have tny: "t\<noteq>y" by auto
|
|
92 |
{assume H: "y\<sqsubset> t"
|
|
93 |
from less_trans[OF ly H] less_trans[OF px xu] have "l \<sqsubset> t \<and> t \<sqsubset> u" by simp
|
|
94 |
with tU noU have "False" by auto}
|
|
95 |
hence "\<not> y\<sqsubset>t" by auto hence "t \<sqsubseteq> y" by (auto simp add: not_less)
|
|
96 |
thus "t \<sqsubset> y" using tny by (simp add:less_le)
|
|
97 |
qed
|
|
98 |
|
|
99 |
lemma lin_dense_le: "t \<in> U \<Longrightarrow> \<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> x \<sqsubseteq> t \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> y\<sqsubseteq> t)"
|
|
100 |
proof(clarsimp)
|
|
101 |
fix x l u y
|
|
102 |
assume tU: "t \<in> U" and noU: "\<forall>t. l \<sqsubset> t \<and> t \<sqsubset> u \<longrightarrow> t \<notin> U" and lx: "l \<sqsubset> x" and xu: "x\<sqsubset>u"
|
|
103 |
and px: "x \<sqsubseteq> t" and ly: "l\<sqsubset>y" and yu:"y \<sqsubset> u"
|
|
104 |
from tU noU ly yu have tny: "t\<noteq>y" by auto
|
|
105 |
{assume H: "t \<sqsubset> y"
|
|
106 |
from less_le_trans[OF lx px] less_trans[OF H yu]
|
|
107 |
have "l \<sqsubset> t \<and> t \<sqsubset> u" by simp
|
|
108 |
with tU noU have "False" by auto}
|
|
109 |
hence "\<not> t \<sqsubset> y" by auto thus "y \<sqsubseteq> t" by (simp add: not_less)
|
|
110 |
qed
|
|
111 |
|
|
112 |
lemma lin_dense_ge: "t \<in> U \<Longrightarrow> \<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> t \<sqsubseteq> x \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> t \<sqsubseteq> y)"
|
|
113 |
proof(clarsimp)
|
|
114 |
fix x l u y
|
|
115 |
assume tU: "t \<in> U" and noU: "\<forall>t. l \<sqsubset> t \<and> t \<sqsubset> u \<longrightarrow> t \<notin> U" and lx: "l \<sqsubset> x" and xu: "x\<sqsubset>u"
|
|
116 |
and px: "t \<sqsubseteq> x" and ly: "l\<sqsubset>y" and yu:"y \<sqsubset> u"
|
|
117 |
from tU noU ly yu have tny: "t\<noteq>y" by auto
|
|
118 |
{assume H: "y\<sqsubset> t"
|
|
119 |
from less_trans[OF ly H] le_less_trans[OF px xu]
|
|
120 |
have "l \<sqsubset> t \<and> t \<sqsubset> u" by simp
|
|
121 |
with tU noU have "False" by auto}
|
|
122 |
hence "\<not> y\<sqsubset>t" by auto thus "t \<sqsubseteq> y" by (simp add: not_less)
|
|
123 |
qed
|
|
124 |
lemma lin_dense_eq: "t \<in> U \<Longrightarrow> \<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> x = t \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> y= t)" by auto
|
|
125 |
lemma lin_dense_neq: "t \<in> U \<Longrightarrow> \<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> x \<noteq> t \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> y\<noteq> t)" by auto
|
|
126 |
lemma lin_dense_P: "\<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 \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P)" by auto
|
|
127 |
|
|
128 |
lemma lin_dense_conj:
|
|
129 |
"\<lbrakk>\<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> P1 x
|
|
130 |
\<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P1 y) ;
|
|
131 |
\<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> P2 x
|
|
132 |
\<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow>
|
|
133 |
\<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> (P1 x \<and> P2 x)
|
|
134 |
\<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> (P1 y \<and> P2 y))"
|
|
135 |
by blast
|
|
136 |
lemma lin_dense_disj:
|
|
137 |
"\<lbrakk>\<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> P1 x
|
|
138 |
\<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P1 y) ;
|
|
139 |
\<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> P2 x
|
|
140 |
\<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow>
|
|
141 |
\<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> (P1 x \<or> P2 x)
|
|
142 |
\<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> (P1 y \<or> P2 y))"
|
|
143 |
by blast
|
|
144 |
|
|
145 |
lemma npmibnd: "\<lbrakk>\<forall>x. \<not> MP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<sqsubseteq> x); \<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. x \<sqsubseteq> u)\<rbrakk>
|
|
146 |
\<Longrightarrow> \<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')"
|
|
147 |
by auto
|
|
148 |
|
|
149 |
lemma finite_set_intervals:
|
|
150 |
assumes px: "P x" and lx: "l \<sqsubseteq> x" and xu: "x \<sqsubseteq> u" and linS: "l\<in> S"
|
|
151 |
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"
|
|
152 |
shows "\<exists> a \<in> S. \<exists> b \<in> S. (\<forall> y. a \<sqsubset> y \<and> y \<sqsubset> b \<longrightarrow> y \<notin> S) \<and> a \<sqsubseteq> x \<and> x \<sqsubseteq> b \<and> P x"
|
|
153 |
proof-
|
|
154 |
let ?Mx = "{y. y\<in> S \<and> y \<sqsubseteq> x}"
|
|
155 |
let ?xM = "{y. y\<in> S \<and> x \<sqsubseteq> y}"
|
|
156 |
let ?a = "Max ?Mx"
|
|
157 |
let ?b = "Min ?xM"
|
|
158 |
have MxS: "?Mx \<subseteq> S" by blast
|
|
159 |
hence fMx: "finite ?Mx" using fS finite_subset by auto
|
|
160 |
from lx linS have linMx: "l \<in> ?Mx" by blast
|
|
161 |
hence Mxne: "?Mx \<noteq> {}" by blast
|
|
162 |
have xMS: "?xM \<subseteq> S" by blast
|
|
163 |
hence fxM: "finite ?xM" using fS finite_subset by auto
|
|
164 |
from xu uinS have linxM: "u \<in> ?xM" by blast
|
|
165 |
hence xMne: "?xM \<noteq> {}" by blast
|
|
166 |
have ax:"?a \<sqsubseteq> x" using Mxne fMx by auto
|
|
167 |
have xb:"x \<sqsubseteq> ?b" using xMne fxM by auto
|
|
168 |
have "?a \<in> ?Mx" using Max_in[OF fMx Mxne] by simp hence ainS: "?a \<in> S" using MxS by blast
|
|
169 |
have "?b \<in> ?xM" using Min_in[OF fxM xMne] by simp hence binS: "?b \<in> S" using xMS by blast
|
|
170 |
have noy:"\<forall> y. ?a \<sqsubset> y \<and> y \<sqsubset> ?b \<longrightarrow> y \<notin> S"
|
|
171 |
proof(clarsimp)
|
|
172 |
fix y assume ay: "?a \<sqsubset> y" and yb: "y \<sqsubset> ?b" and yS: "y \<in> S"
|
|
173 |
from yS have "y\<in> ?Mx \<or> y\<in> ?xM" by (auto simp add: linear)
|
|
174 |
moreover {assume "y \<in> ?Mx" hence "y \<sqsubseteq> ?a" using Mxne fMx by auto with ay have "False" by (simp add: not_le[symmetric])}
|
|
175 |
moreover {assume "y \<in> ?xM" hence "?b \<sqsubseteq> y" using xMne fxM by auto with yb have "False" by (simp add: not_le[symmetric])}
|
|
176 |
ultimately show "False" by blast
|
|
177 |
qed
|
|
178 |
from ainS binS noy ax xb px show ?thesis by blast
|
|
179 |
qed
|
|
180 |
|
|
181 |
|
|
182 |
lemma finite_set_intervals2:
|
|
183 |
assumes px: "P x" and lx: "l \<sqsubseteq> x" and xu: "x \<sqsubseteq> u" and linS: "l\<in> S"
|
|
184 |
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"
|
|
185 |
shows "(\<exists> s\<in> S. P s) \<or> (\<exists> a \<in> S. \<exists> b \<in> S. (\<forall> y. a \<sqsubset> y \<and> y \<sqsubset> b \<longrightarrow> y \<notin> S) \<and> a \<sqsubset> x \<and> x \<sqsubset> b \<and> P x)"
|
|
186 |
proof-
|
|
187 |
from finite_set_intervals[where P="P", OF px lx xu linS uinS fS lS Su]
|
|
188 |
obtain a and b where
|
|
189 |
as: "a\<in> S" and bs: "b\<in> S" and noS:"\<forall>y. a \<sqsubset> y \<and> y \<sqsubset> b \<longrightarrow> y \<notin> S"
|
|
190 |
and axb: "a \<sqsubseteq> x \<and> x \<sqsubseteq> b \<and> P x" by auto
|
|
191 |
from axb have "x= a \<or> x= b \<or> (a \<sqsubset> x \<and> x \<sqsubset> b)" by (auto simp add: le_less)
|
|
192 |
thus ?thesis using px as bs noS by blast
|
|
193 |
qed
|
|
194 |
|
|
195 |
end
|
|
196 |
|
|
197 |
text {* Linear order without upper bounds *}
|
|
198 |
|
|
199 |
locale linorder_no_ub = Linorder + assumes gt_ex: "\<forall>x. \<exists>y. x \<sqsubset> y"
|
|
200 |
begin
|
|
201 |
|
|
202 |
lemma ge_ex: "\<forall>x. \<exists>y. x \<sqsubseteq> y" using gt_ex by auto
|
|
203 |
|
|
204 |
text {* Theorems for @{text "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"} *}
|
|
205 |
lemma pinf_conj:
|
|
206 |
assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
|
|
207 |
and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
|
|
208 |
shows "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
|
|
209 |
proof-
|
|
210 |
from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
|
|
211 |
and z2: "\<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
|
|
212 |
from gt_ex obtain z where z:"max z1 z2 \<sqsubset> z" by blast
|
|
213 |
from z have zz1: "z1 \<sqsubset> z" and zz2: "z2 \<sqsubset> z" by simp_all
|
|
214 |
{fix x assume H: "z \<sqsubset> x"
|
|
215 |
from less_trans[OF zz1 H] less_trans[OF zz2 H]
|
|
216 |
have "(P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2')" using z1 zz1 z2 zz2 by auto
|
|
217 |
}
|
|
218 |
thus ?thesis by blast
|
|
219 |
qed
|
|
220 |
|
|
221 |
lemma pinf_disj:
|
|
222 |
assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
|
|
223 |
and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
|
|
224 |
shows "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
|
|
225 |
proof-
|
|
226 |
from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
|
|
227 |
and z2: "\<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
|
|
228 |
from gt_ex obtain z where z:"max z1 z2 \<sqsubset> z" by blast
|
|
229 |
from z have zz1: "z1 \<sqsubset> z" and zz2: "z2 \<sqsubset> z" by simp_all
|
|
230 |
{fix x assume H: "z \<sqsubset> x"
|
|
231 |
from less_trans[OF zz1 H] less_trans[OF zz2 H]
|
|
232 |
have "(P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2')" using z1 zz1 z2 zz2 by auto
|
|
233 |
}
|
|
234 |
thus ?thesis by blast
|
|
235 |
qed
|
|
236 |
|
|
237 |
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"
|
|
238 |
proof-
|
|
239 |
from ex obtain z where z: "\<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast
|
|
240 |
from gt_ex obtain x where x: "z \<sqsubset> x" by blast
|
|
241 |
from z x p1 show ?thesis by blast
|
|
242 |
qed
|
|
243 |
|
|
244 |
end
|
|
245 |
|
|
246 |
text {* Linear order without upper bounds *}
|
|
247 |
|
|
248 |
locale linorder_no_lb = Linorder + assumes lt_ex: "\<forall>x. \<exists>y. y \<sqsubset> x"
|
|
249 |
begin
|
|
250 |
|
|
251 |
lemma le_ex: "\<forall>x. \<exists>y. y \<sqsubseteq> x" using lt_ex by auto
|
|
252 |
|
|
253 |
|
|
254 |
text {* Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"} *}
|
|
255 |
lemma minf_conj:
|
|
256 |
assumes ex1: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
|
|
257 |
and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
|
|
258 |
shows "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
|
|
259 |
proof-
|
|
260 |
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
|
|
261 |
from lt_ex obtain z where z:"z \<sqsubset> min z1 z2" by blast
|
|
262 |
from z have zz1: "z \<sqsubset> z1" and zz2: "z \<sqsubset> z2" by simp_all
|
|
263 |
{fix x assume H: "x \<sqsubset> z"
|
|
264 |
from less_trans[OF H zz1] less_trans[OF H zz2]
|
|
265 |
have "(P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2')" using z1 zz1 z2 zz2 by auto
|
|
266 |
}
|
|
267 |
thus ?thesis by blast
|
|
268 |
qed
|
|
269 |
|
|
270 |
lemma minf_disj:
|
|
271 |
assumes ex1: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
|
|
272 |
and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
|
|
273 |
shows "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
|
|
274 |
proof-
|
|
275 |
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
|
|
276 |
from lt_ex obtain z where z:"z \<sqsubset> min z1 z2" by blast
|
|
277 |
from z have zz1: "z \<sqsubset> z1" and zz2: "z \<sqsubset> z2" by simp_all
|
|
278 |
{fix x assume H: "x \<sqsubset> z"
|
|
279 |
from less_trans[OF H zz1] less_trans[OF H zz2]
|
|
280 |
have "(P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2')" using z1 zz1 z2 zz2 by auto
|
|
281 |
}
|
|
282 |
thus ?thesis by blast
|
|
283 |
qed
|
|
284 |
|
|
285 |
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"
|
|
286 |
proof-
|
|
287 |
from ex obtain z where z: "\<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast
|
|
288 |
from lt_ex obtain x where x: "x \<sqsubset> z" by blast
|
|
289 |
from z x p1 show ?thesis by blast
|
|
290 |
qed
|
|
291 |
|
|
292 |
end
|
|
293 |
|
|
294 |
locale dense_linear_order = linorder_no_lb + linorder_no_ub +
|
|
295 |
fixes between
|
|
296 |
assumes between_less: "\<forall>x y. x \<sqsubset> y \<longrightarrow> x \<sqsubset> between x y \<and> between x y \<sqsubset> y"
|
|
297 |
and between_same: "\<forall>x. between x x = x"
|
|
298 |
begin
|
|
299 |
|
|
300 |
lemma rinf_U:
|
|
301 |
assumes fU: "finite U"
|
|
302 |
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
|
|
303 |
\<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P y )"
|
|
304 |
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')"
|
|
305 |
and nmi: "\<not> MP" and npi: "\<not> PP" and ex: "\<exists> x. P x"
|
|
306 |
shows "\<exists> u\<in> U. \<exists> u' \<in> U. P (between u u')"
|
|
307 |
proof-
|
|
308 |
from ex obtain x where px: "P x" by blast
|
|
309 |
from px nmi npi nmpiU have "\<exists> u\<in> U. \<exists> u' \<in> U. u \<sqsubseteq> x \<and> x \<sqsubseteq> u'" by auto
|
|
310 |
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
|
|
311 |
from uU have Une: "U \<noteq> {}" by auto
|
|
312 |
let ?l = "Min U"
|
|
313 |
let ?u = "Max U"
|
|
314 |
have linM: "?l \<in> U" using fU Une by simp
|
|
315 |
have uinM: "?u \<in> U" using fU Une by simp
|
|
316 |
have lM: "\<forall> t\<in> U. ?l \<sqsubseteq> t" using Une fU by auto
|
|
317 |
have Mu: "\<forall> t\<in> U. t \<sqsubseteq> ?u" using Une fU by auto
|
|
318 |
have th:"?l \<sqsubseteq> u" using uU Une lM by auto
|
|
319 |
from order_trans[OF th ux] have lx: "?l \<sqsubseteq> x" .
|
|
320 |
have th: "u' \<sqsubseteq> ?u" using uU' Une Mu by simp
|
|
321 |
from order_trans[OF xu' th] have xu: "x \<sqsubseteq> ?u" .
|
|
322 |
from finite_set_intervals2[where P="P",OF px lx xu linM uinM fU lM Mu]
|
|
323 |
have "(\<exists> s\<in> U. P s) \<or>
|
|
324 |
(\<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)" .
|
|
325 |
moreover { fix u assume um: "u\<in>U" and pu: "P u"
|
|
326 |
have "between u u = u" by (simp add: between_same)
|
|
327 |
with um pu have "P (between u u)" by simp
|
|
328 |
with um have ?thesis by blast}
|
|
329 |
moreover{
|
|
330 |
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"
|
|
331 |
then obtain t1 and t2 where t1M: "t1 \<in> U" and t2M: "t2\<in> U"
|
|
332 |
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"
|
|
333 |
by blast
|
|
334 |
from less_trans[OF t1x xt2] have t1t2: "t1 \<sqsubset> t2" .
|
|
335 |
let ?u = "between t1 t2"
|
|
336 |
from between_less t1t2 have t1lu: "t1 \<sqsubset> ?u" and ut2: "?u \<sqsubset> t2" by auto
|
|
337 |
from lin_dense[rule_format, OF] noM t1x xt2 px t1lu ut2 have "P ?u" by blast
|
|
338 |
with t1M t2M have ?thesis by blast}
|
|
339 |
ultimately show ?thesis by blast
|
|
340 |
qed
|
|
341 |
|
|
342 |
theorem fr_eq:
|
|
343 |
assumes fU: "finite U"
|
|
344 |
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
|
|
345 |
\<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P y )"
|
|
346 |
and nmibnd: "\<forall>x. \<not> MP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<sqsubseteq> x)"
|
|
347 |
and npibnd: "\<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. x \<sqsubseteq> u)"
|
|
348 |
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)"
|
|
349 |
shows "(\<exists> x. P x) \<equiv> (MP \<or> PP \<or> (\<exists> u \<in> U. \<exists> u'\<in> U. P (between u u')))"
|
|
350 |
(is "_ \<equiv> (_ \<or> _ \<or> ?F)" is "?E \<equiv> ?D")
|
|
351 |
proof-
|
|
352 |
{
|
|
353 |
assume px: "\<exists> x. P x"
|
|
354 |
have "MP \<or> PP \<or> (\<not> MP \<and> \<not> PP)" by blast
|
|
355 |
moreover {assume "MP \<or> PP" hence "?D" by blast}
|
|
356 |
moreover {assume nmi: "\<not> MP" and npi: "\<not> PP"
|
|
357 |
from npmibnd[OF nmibnd npibnd]
|
|
358 |
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')" .
|
|
359 |
from rinf_U[OF fU lin_dense nmpiU nmi npi px] have "?D" by blast}
|
|
360 |
ultimately have "?D" by blast}
|
|
361 |
moreover
|
|
362 |
{ assume "?D"
|
|
363 |
moreover {assume m:"MP" from minf_ex[OF mi m] have "?E" .}
|
|
364 |
moreover {assume p: "PP" from pinf_ex[OF pi p] have "?E" . }
|
|
365 |
moreover {assume f:"?F" hence "?E" by blast}
|
|
366 |
ultimately have "?E" by blast}
|
|
367 |
ultimately have "?E = ?D" by blast thus "?E \<equiv> ?D" by simp
|
|
368 |
qed
|
|
369 |
|
|
370 |
lemmas minf_thms = minf_conj minf_disj minf_eq minf_neq minf_lt minf_le minf_gt minf_ge minf_P
|
|
371 |
lemmas pinf_thms = pinf_conj pinf_disj pinf_eq pinf_neq pinf_lt pinf_le pinf_gt pinf_ge pinf_P
|
|
372 |
|
|
373 |
lemmas nmi_thms = nmi_conj nmi_disj nmi_eq nmi_neq nmi_lt nmi_le nmi_gt nmi_ge nmi_P
|
|
374 |
lemmas npi_thms = npi_conj npi_disj npi_eq npi_neq npi_lt npi_le npi_gt npi_ge npi_P
|
|
375 |
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
|
|
376 |
|
|
377 |
lemma ferrack_axiom: "dense_linear_order less_eq less between" by fact
|
|
378 |
lemma atoms: includes meta_term_syntax
|
|
379 |
shows "TERM (op \<sqsubset> :: 'a \<Rightarrow> _)" and "TERM (op \<sqsubseteq>)" and "TERM (op = :: 'a \<Rightarrow> _)" .
|
|
380 |
|
|
381 |
declare ferrack_axiom [dlo minf: minf_thms pinf: pinf_thms
|
|
382 |
nmi: nmi_thms npi: npi_thms lindense:
|
|
383 |
lin_dense_thms qe: fr_eq atoms: atoms]
|
|
384 |
|
|
385 |
declaration {*
|
|
386 |
let
|
|
387 |
fun generic_whatis phi =
|
|
388 |
let
|
|
389 |
val [lt, le] = map (Morphism.term phi)
|
|
390 |
(ProofContext.read_term_pats @{typ "dummy"} @{context} ["op \<sqsubset>", "op \<sqsubseteq>"]) (* FIXME avoid read? *)
|
|
391 |
val le = Morphism.term phi @{term "op \<sqsubseteq>"}
|
|
392 |
fun h x t =
|
|
393 |
case term_of t of
|
|
394 |
Const("op =", _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
|
|
395 |
else Ferrante_Rackoff_Data.Nox
|
|
396 |
| @{term "Not"}$(Const("op =", _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
|
|
397 |
else Ferrante_Rackoff_Data.Nox
|
|
398 |
| b$y$z => if Term.could_unify (b, lt) then
|
|
399 |
if term_of x aconv y then Ferrante_Rackoff_Data.Lt
|
|
400 |
else if term_of x aconv z then Ferrante_Rackoff_Data.Gt
|
|
401 |
else Ferrante_Rackoff_Data.Nox
|
|
402 |
else if Term.could_unify (b, le) then
|
|
403 |
if term_of x aconv y then Ferrante_Rackoff_Data.Le
|
|
404 |
else if term_of x aconv z then Ferrante_Rackoff_Data.Ge
|
|
405 |
else Ferrante_Rackoff_Data.Nox
|
|
406 |
else Ferrante_Rackoff_Data.Nox
|
|
407 |
| _ => Ferrante_Rackoff_Data.Nox
|
|
408 |
in h end
|
|
409 |
val ss = K (HOL_ss addsimps [@{thm "not_less"}, @{thm "not_le"}])
|
|
410 |
in
|
|
411 |
Ferrante_Rackoff_Data.funs @{thm "ferrack_axiom"}
|
|
412 |
{isolate_conv = K (K (K Thm.reflexive)), whatis = generic_whatis, simpset = ss}
|
|
413 |
end
|
|
414 |
*}
|
|
415 |
|
|
416 |
end
|
|
417 |
|
|
418 |
use "Tools/Ferrante_Rackoff/ferrante_rackoff.ML"
|
|
419 |
|
|
420 |
method_setup dlo = {*
|
|
421 |
Method.ctxt_args (Method.SIMPLE_METHOD' o FerranteRackoff.dlo_tac)
|
|
422 |
*} "Ferrante and Rackoff's algorithm for quantifier elimination in dense linear orders"
|
|
423 |
|
|
424 |
end
|