|
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 |