20 setup Ferrante_Rackoff_Data.setup |
20 setup Ferrante_Rackoff_Data.setup |
21 |
21 |
22 context linorder |
22 context linorder |
23 begin |
23 begin |
24 |
24 |
25 lemma less_not_permute: "\<not> (x \<sqsubset> y \<and> y \<sqsubset> x)" by (simp add: not_less linear) |
25 lemma less_not_permute: "\<not> (x \<^loc>< y \<and> y \<^loc>< x)" by (simp add: not_less linear) |
26 |
26 |
27 lemma gather_simps: |
27 lemma gather_simps: |
28 shows |
28 shows |
29 "(\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y) \<and> x \<sqsubset> u \<and> P x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> (insert u U). x \<sqsubset> y) \<and> P x)" |
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 \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y) \<and> l \<sqsubset> x \<and> P x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> (insert l L). y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y) \<and> P x)" |
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 \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y) \<and> x \<sqsubset> u) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> (insert u U). x \<sqsubset> y))" |
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 \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y) \<and> l \<sqsubset> x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> (insert l L). y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y))" by auto |
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 |
33 |
33 |
34 lemma |
34 lemma |
35 gather_start: "(\<exists>x. P x) \<equiv> (\<exists>x. (\<forall>y \<in> {}. y \<^loc>< x) \<and> (\<forall>y\<in> {}. x \<sqsubset> y) \<and> P x)" |
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)" |
36 by simp |
36 by simp |
37 |
37 |
38 text{* Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"}*} |
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 \<sqsubset> z \<longrightarrow> (x \<sqsubset> t \<longleftrightarrow> True)" by auto |
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 \<sqsubset> z \<longrightarrow> (t \<sqsubset> x \<longleftrightarrow> False)" |
40 lemma minf_gt: "\<exists>z . \<forall>x. x \<^loc>< z \<longrightarrow> (t \<^loc>< x \<longleftrightarrow> False)" |
41 by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le) |
41 by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le) |
42 |
42 |
43 lemma minf_le: "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (x \<sqsubseteq> t \<longleftrightarrow> True)" by (auto simp add: less_le) |
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 \<sqsubset> z \<longrightarrow> (t \<sqsubseteq> x \<longleftrightarrow> False)" |
44 lemma minf_ge: "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (t \<^loc>\<le> x \<longleftrightarrow> False)" |
45 by (auto simp add: less_le not_less not_le) |
45 by (auto simp add: less_le not_less not_le) |
46 lemma minf_eq: "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto |
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 \<sqsubset> z \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" 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 \<sqsubset> z \<longrightarrow> (P \<longleftrightarrow> P)" by blast |
48 lemma minf_P: "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (P \<longleftrightarrow> P)" by blast |
49 |
49 |
50 text{* Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"}*} |
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 \<sqsubset> x \<longrightarrow> (t \<sqsubset> x \<longleftrightarrow> True)" by auto |
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 \<sqsubset> x \<longrightarrow> (x \<sqsubset> t \<longleftrightarrow> False)" |
52 lemma pinf_lt: "\<exists>z . \<forall>x. z \<^loc>< x \<longrightarrow> (x \<^loc>< t \<longleftrightarrow> False)" |
53 by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le) |
53 by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le) |
54 |
54 |
55 lemma pinf_ge: "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (t \<sqsubseteq> x \<longleftrightarrow> True)" by (auto simp add: less_le) |
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 \<sqsubset> x \<longrightarrow> (x \<sqsubseteq> t \<longleftrightarrow> False)" |
56 lemma pinf_le: "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> (x \<^loc>\<le> t \<longleftrightarrow> False)" |
57 by (auto simp add: less_le not_less not_le) |
57 by (auto simp add: less_le not_less not_le) |
58 lemma pinf_eq: "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto |
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 \<sqsubset> x \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" 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 \<sqsubset> x \<longrightarrow> (P \<longleftrightarrow> P)" by blast |
60 lemma pinf_P: "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> (P \<longleftrightarrow> P)" by blast |
61 |
61 |
62 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 |
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 \<sqsubset> x \<longrightarrow> (\<exists> u\<in> U. u \<sqsubseteq> x)" |
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)" |
64 by (auto simp add: le_less) |
64 by (auto simp add: le_less) |
65 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 |
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\<sqsubseteq> x \<longrightarrow> (\<exists> u\<in> U. u \<sqsubseteq> 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 \<sqsubseteq> 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 \<sqsubseteq> 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 \<sqsubseteq> 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 \<sqsubseteq> x) ; |
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 \<sqsubseteq> x)\<rbrakk> \<Longrightarrow> |
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 \<sqsubseteq> x)" by auto |
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 \<sqsubseteq> x) ; |
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 \<sqsubseteq> x)\<rbrakk> \<Longrightarrow> |
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 \<sqsubseteq> x)" by auto |
75 \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x)" by auto |
76 |
76 |
77 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) |
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 \<sqsubset> x \<longrightarrow> (\<exists> u\<in> U. x \<sqsubseteq> u)" by auto |
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 \<sqsubseteq> t \<longrightarrow> (\<exists> u\<in> U. x \<sqsubseteq> 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 \<sqsubseteq> x \<longrightarrow> (\<exists> u\<in> U. x \<sqsubseteq> 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 \<sqsubseteq> 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 \<sqsubseteq> 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 \<sqsubseteq> 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 \<sqsubseteq> u) ; \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow> (\<exists> u\<in> U. x \<sqsubseteq> u)\<rbrakk> |
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 \<sqsubseteq> u)" by auto |
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 \<sqsubseteq> u) ; \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow> (\<exists> u\<in> U. x \<sqsubseteq> u)\<rbrakk> |
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 \<sqsubseteq> u)" by auto |
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 |
88 |
88 |
89 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)" |
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)" |
90 proof(clarsimp) |
90 proof(clarsimp) |
91 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" |
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\<sqsubset>u" and px: "x \<sqsubset> t" and ly: "l\<sqsubset>y" and yu:"y \<sqsubset> u" |
92 and xu: "x\<^loc><u" and px: "x \<^loc>< t" and ly: "l\<^loc><y" and yu:"y \<^loc>< u" |
93 from tU noU ly yu have tny: "t\<noteq>y" by auto |
93 from tU noU ly yu have tny: "t\<noteq>y" by auto |
94 {assume H: "t \<sqsubset> y" |
94 {assume H: "t \<^loc>< y" |
95 from less_trans[OF lx px] less_trans[OF H yu] |
95 from less_trans[OF lx px] less_trans[OF H yu] |
96 have "l \<sqsubset> t \<and> t \<sqsubset> u" by simp |
96 have "l \<^loc>< t \<and> t \<^loc>< u" by simp |
97 with tU noU have "False" by auto} |
97 with tU noU have "False" by auto} |
98 hence "\<not> t \<sqsubset> y" by auto hence "y \<sqsubseteq> t" by (simp add: not_less) |
98 hence "\<not> t \<^loc>< y" by auto hence "y \<^loc>\<le> t" by (simp add: not_less) |
99 thus "y \<sqsubset> t" using tny by (simp add: less_le) |
99 thus "y \<^loc>< t" using tny by (simp add: less_le) |
100 qed |
100 qed |
101 |
101 |
102 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)" |
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)" |
103 proof(clarsimp) |
103 proof(clarsimp) |
104 fix x l u y |
104 fix x l u y |
105 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" |
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 \<sqsubset> x" and ly: "l\<sqsubset>y" and yu:"y \<sqsubset> u" |
106 and px: "t \<^loc>< x" and ly: "l\<^loc><y" and yu:"y \<^loc>< u" |
107 from tU noU ly yu have tny: "t\<noteq>y" by auto |
107 from tU noU ly yu have tny: "t\<noteq>y" by auto |
108 {assume H: "y\<sqsubset> t" |
108 {assume H: "y\<^loc>< t" |
109 from less_trans[OF ly H] less_trans[OF px xu] have "l \<sqsubset> t \<and> t \<sqsubset> u" by simp |
109 from less_trans[OF ly H] less_trans[OF px xu] have "l \<^loc>< t \<and> t \<^loc>< u" by simp |
110 with tU noU have "False" by auto} |
110 with tU noU have "False" by auto} |
111 hence "\<not> y\<sqsubset>t" by auto hence "t \<sqsubseteq> y" by (auto simp add: not_less) |
111 hence "\<not> y\<^loc><t" by auto hence "t \<^loc>\<le> y" by (auto simp add: not_less) |
112 thus "t \<sqsubset> y" using tny by (simp add:less_le) |
112 thus "t \<^loc>< y" using tny by (simp add:less_le) |
113 qed |
113 qed |
114 |
114 |
115 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)" |
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)" |
116 proof(clarsimp) |
116 proof(clarsimp) |
117 fix x l u y |
117 fix x l u y |
118 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" |
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 \<sqsubseteq> t" and ly: "l\<sqsubset>y" and yu:"y \<sqsubset> u" |
119 and px: "x \<^loc>\<le> t" and ly: "l\<^loc><y" and yu:"y \<^loc>< u" |
120 from tU noU ly yu have tny: "t\<noteq>y" by auto |
120 from tU noU ly yu have tny: "t\<noteq>y" by auto |
121 {assume H: "t \<sqsubset> y" |
121 {assume H: "t \<^loc>< y" |
122 from less_le_trans[OF lx px] less_trans[OF H yu] |
122 from less_le_trans[OF lx px] less_trans[OF H yu] |
123 have "l \<sqsubset> t \<and> t \<sqsubset> u" by simp |
123 have "l \<^loc>< t \<and> t \<^loc>< u" by simp |
124 with tU noU have "False" by auto} |
124 with tU noU have "False" by auto} |
125 hence "\<not> t \<sqsubset> y" by auto thus "y \<sqsubseteq> t" by (simp add: not_less) |
125 hence "\<not> t \<^loc>< y" by auto thus "y \<^loc>\<le> t" by (simp add: not_less) |
126 qed |
126 qed |
127 |
127 |
128 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)" |
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)" |
129 proof(clarsimp) |
129 proof(clarsimp) |
130 fix x l u y |
130 fix x l u y |
131 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" |
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 \<sqsubseteq> x" and ly: "l\<sqsubset>y" and yu:"y \<sqsubset> u" |
132 and px: "t \<^loc>\<le> x" and ly: "l\<^loc><y" and yu:"y \<^loc>< u" |
133 from tU noU ly yu have tny: "t\<noteq>y" by auto |
133 from tU noU ly yu have tny: "t\<noteq>y" by auto |
134 {assume H: "y\<sqsubset> t" |
134 {assume H: "y\<^loc>< t" |
135 from less_trans[OF ly H] le_less_trans[OF px xu] |
135 from less_trans[OF ly H] le_less_trans[OF px xu] |
136 have "l \<sqsubset> t \<and> t \<sqsubset> u" by simp |
136 have "l \<^loc>< t \<and> t \<^loc>< u" by simp |
137 with tU noU have "False" by auto} |
137 with tU noU have "False" by auto} |
138 hence "\<not> y\<sqsubset>t" by auto thus "t \<sqsubseteq> y" by (simp add: not_less) |
138 hence "\<not> y\<^loc><t" by auto thus "t \<^loc>\<le> y" by (simp add: not_less) |
139 qed |
139 qed |
140 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 |
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 \<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 |
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 \<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 |
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 |
143 |
143 |
144 lemma lin_dense_conj: |
144 lemma lin_dense_conj: |
145 "\<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 |
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 \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P1 y) ; |
146 \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> P1 y) ; |
147 \<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 |
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 \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow> |
148 \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow> |
149 \<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) |
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 \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> (P1 y \<and> P2 y))" |
150 \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> (P1 y \<and> P2 y))" |
151 by blast |
151 by blast |
152 lemma lin_dense_disj: |
152 lemma lin_dense_disj: |
153 "\<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 |
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 \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P1 y) ; |
154 \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> P1 y) ; |
155 \<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 |
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 \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow> |
156 \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow> |
157 \<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) |
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 \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> (P1 y \<or> P2 y))" |
158 \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> (P1 y \<or> P2 y))" |
159 by blast |
159 by blast |
160 |
160 |
161 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> |
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 \<sqsubseteq> x \<and> x \<sqsubseteq> u')" |
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')" |
163 by auto |
163 by auto |
164 |
164 |
165 lemma finite_set_intervals: |
165 lemma finite_set_intervals: |
166 assumes px: "P x" and lx: "l \<sqsubseteq> x" and xu: "x \<sqsubseteq> u" and linS: "l\<in> S" |
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 \<sqsubseteq> x" and Su: "\<forall> x\<in> S. x \<sqsubseteq> u" |
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 \<sqsubset> y \<and> y \<sqsubset> b \<longrightarrow> y \<notin> S) \<and> a \<sqsubseteq> x \<and> x \<sqsubseteq> b \<and> P x" |
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" |
169 proof- |
169 proof- |
170 let ?Mx = "{y. y\<in> S \<and> y \<sqsubseteq> x}" |
170 let ?Mx = "{y. y\<in> S \<and> y \<^loc>\<le> x}" |
171 let ?xM = "{y. y\<in> S \<and> x \<sqsubseteq> y}" |
171 let ?xM = "{y. y\<in> S \<and> x \<^loc>\<le> y}" |
172 let ?a = "Max ?Mx" |
172 let ?a = "Max ?Mx" |
173 let ?b = "Min ?xM" |
173 let ?b = "Min ?xM" |
174 have MxS: "?Mx \<subseteq> S" by blast |
174 have MxS: "?Mx \<subseteq> S" by blast |
175 hence fMx: "finite ?Mx" using fS finite_subset by auto |
175 hence fMx: "finite ?Mx" using fS finite_subset by auto |
176 from lx linS have linMx: "l \<in> ?Mx" by blast |
176 from lx linS have linMx: "l \<in> ?Mx" by blast |
177 hence Mxne: "?Mx \<noteq> {}" by blast |
177 hence Mxne: "?Mx \<noteq> {}" by blast |
178 have xMS: "?xM \<subseteq> S" by blast |
178 have xMS: "?xM \<subseteq> S" by blast |
179 hence fxM: "finite ?xM" using fS finite_subset by auto |
179 hence fxM: "finite ?xM" using fS finite_subset by auto |
180 from xu uinS have linxM: "u \<in> ?xM" by blast |
180 from xu uinS have linxM: "u \<in> ?xM" by blast |
181 hence xMne: "?xM \<noteq> {}" by blast |
181 hence xMne: "?xM \<noteq> {}" by blast |
182 have ax:"?a \<sqsubseteq> x" using Mxne fMx by auto |
182 have ax:"?a \<^loc>\<le> x" using Mxne fMx by auto |
183 have xb:"x \<sqsubseteq> ?b" using xMne fxM by auto |
183 have xb:"x \<^loc>\<le> ?b" using xMne fxM by auto |
184 have "?a \<in> ?Mx" using Max_in[OF fMx Mxne] by simp hence ainS: "?a \<in> S" using MxS by blast |
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 |
185 have "?b \<in> ?xM" using Min_in[OF fxM xMne] by simp hence binS: "?b \<in> S" using xMS by blast |
186 have noy:"\<forall> y. ?a \<sqsubset> y \<and> y \<sqsubset> ?b \<longrightarrow> y \<notin> S" |
186 have noy:"\<forall> y. ?a \<^loc>< y \<and> y \<^loc>< ?b \<longrightarrow> y \<notin> S" |
187 proof(clarsimp) |
187 proof(clarsimp) |
188 fix y assume ay: "?a \<sqsubset> y" and yb: "y \<sqsubset> ?b" and yS: "y \<in> S" |
188 fix y assume ay: "?a \<^loc>< y" and yb: "y \<^loc>< ?b" and yS: "y \<in> S" |
189 from yS have "y\<in> ?Mx \<or> y\<in> ?xM" by (auto simp add: linear) |
189 from yS have "y\<in> ?Mx \<or> y\<in> ?xM" by (auto simp add: linear) |
190 moreover {assume "y \<in> ?Mx" hence "y \<sqsubseteq> ?a" using Mxne fMx by auto with ay have "False" by (simp add: not_le[symmetric])} |
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 \<sqsubseteq> y" using xMne fxM by auto with yb 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])} |
192 ultimately show "False" by blast |
192 ultimately show "False" by blast |
193 qed |
193 qed |
194 from ainS binS noy ax xb px show ?thesis by blast |
194 from ainS binS noy ax xb px show ?thesis by blast |
195 qed |
195 qed |
196 |
196 |
197 lemma finite_set_intervals2: |
197 lemma finite_set_intervals2: |
198 assumes px: "P x" and lx: "l \<sqsubseteq> x" and xu: "x \<sqsubseteq> u" and linS: "l\<in> S" |
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 \<sqsubseteq> x" and Su: "\<forall> x\<in> S. x \<sqsubseteq> u" |
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 \<sqsubset> y \<and> y \<sqsubset> b \<longrightarrow> y \<notin> S) \<and> a \<sqsubset> x \<and> x \<sqsubset> b \<and> P x)" |
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)" |
201 proof- |
201 proof- |
202 from finite_set_intervals[where P="P", OF px lx xu linS uinS fS lS Su] |
202 from finite_set_intervals[where P="P", OF px lx xu linS uinS fS lS Su] |
203 obtain a and b where |
203 obtain a and b where |
204 as: "a\<in> S" and bs: "b\<in> S" and noS:"\<forall>y. a \<sqsubset> y \<and> y \<sqsubset> b \<longrightarrow> y \<notin> S" |
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 \<sqsubseteq> x \<and> x \<sqsubseteq> b \<and> P x" by auto |
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 \<sqsubset> x \<and> x \<sqsubset> b)" by (auto simp add: le_less) |
206 from axb have "x= a \<or> x= b \<or> (a \<^loc>< x \<and> x \<^loc>< b)" by (auto simp add: le_less) |
207 thus ?thesis using px as bs noS by blast |
207 thus ?thesis using px as bs noS by blast |
208 qed |
208 qed |
209 |
209 |
210 end |
210 end |
211 |
211 |
214 context dense_linear_order |
214 context dense_linear_order |
215 begin |
215 begin |
216 |
216 |
217 lemma dlo_qe_bnds: |
217 lemma dlo_qe_bnds: |
218 assumes ne: "L \<noteq> {}" and neU: "U \<noteq> {}" and fL: "finite L" and fU: "finite U" |
218 assumes ne: "L \<noteq> {}" and neU: "U \<noteq> {}" and fL: "finite L" and fU: "finite U" |
219 shows "(\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y)) \<equiv> (\<forall> l \<in> L. \<forall>u \<in> U. l \<sqsubset> u)" |
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)" |
220 proof (simp only: atomize_eq, rule iffI) |
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)" |
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 |
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" |
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]] |
224 from less_trans[OF xL[rule_format, OF l] xU[rule_format, OF u]] |
225 have "l \<sqsubset> u" .} |
225 have "l \<^loc>< u" .} |
226 thus "\<forall>l\<in>L. \<forall>u\<in>U. l \<^loc>< u" by blast |
226 thus "\<forall>l\<in>L. \<forall>u\<in>U. l \<^loc>< u" by blast |
227 next |
227 next |
228 assume H: "\<forall>l\<in>L. \<forall>u\<in>U. l \<^loc>< u" |
228 assume H: "\<forall>l\<in>L. \<forall>u\<in>U. l \<^loc>< u" |
229 let ?ML = "Max L" |
229 let ?ML = "Max L" |
230 let ?MU = "Min U" |
230 let ?MU = "Min U" |
231 from fL ne have th1: "?ML \<in> L" and th1': "\<forall>l\<in>L. l \<sqsubseteq> ?ML" by auto |
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 \<sqsubseteq> u" 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 \<sqsubset> ?MU" by auto |
233 from th1 th2 H have "?ML \<^loc>< ?MU" by auto |
234 with dense obtain w where th3: "?ML \<sqsubset> w" and th4: "w \<sqsubset> ?MU" by blast |
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 \<sqsubset> w" by auto |
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 \<sqsubset> u" by auto |
236 moreover from th4 th2' have "\<forall>u \<in> U. w \<^loc>< u" by auto |
237 ultimately show "\<exists>x. (\<forall>y\<in>L. y \<^loc>< x) \<and> (\<forall>y\<in>U. x \<^loc>< y)" by auto |
237 ultimately show "\<exists>x. (\<forall>y\<in>L. y \<^loc>< x) \<and> (\<forall>y\<in>U. x \<^loc>< y)" by auto |
238 qed |
238 qed |
239 |
239 |
240 lemma dlo_qe_noub: |
240 lemma dlo_qe_noub: |
241 assumes ne: "L \<noteq> {}" and fL: "finite L" |
241 assumes ne: "L \<noteq> {}" and fL: "finite L" |
242 shows "(\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> {}. x \<sqsubset> y)) \<equiv> True" |
242 shows "(\<exists>x. (\<forall>y \<in> L. y \<^loc>< x) \<and> (\<forall>y \<in> {}. x \<^loc>< y)) \<equiv> True" |
243 proof(simp add: atomize_eq) |
243 proof(simp add: atomize_eq) |
244 from gt_ex[rule_format, of "Max L"] obtain M where M: "Max L \<sqsubset> M" by blast |
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 \<sqsubseteq> Max L" by simp |
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 \<sqsubset> M" by (auto intro: le_less_trans) |
246 with M have "\<forall>x\<in>L. x \<^loc>< M" by (auto intro: le_less_trans) |
247 thus "\<exists>x. \<forall>y\<in>L. y \<^loc>< x" by blast |
247 thus "\<exists>x. \<forall>y\<in>L. y \<^loc>< x" by blast |
248 qed |
248 qed |
249 |
249 |
250 lemma dlo_qe_nolb: |
250 lemma dlo_qe_nolb: |
251 assumes ne: "U \<noteq> {}" and fU: "finite U" |
251 assumes ne: "U \<noteq> {}" and fU: "finite U" |
252 shows "(\<exists>x. (\<forall>y \<in> {}. y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y)) \<equiv> True" |
252 shows "(\<exists>x. (\<forall>y \<in> {}. y \<^loc>< x) \<and> (\<forall>y \<in> U. x \<^loc>< y)) \<equiv> True" |
253 proof(simp add: atomize_eq) |
253 proof(simp add: atomize_eq) |
254 from lt_ex[rule_format, of "Min U"] obtain M where M: "M \<sqsubset> Min U" by blast |
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 \<sqsubseteq> x" by simp |
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 \<sqsubset> x" by (auto intro: less_le_trans) |
256 with M have "\<forall>x\<in>U. M \<^loc>< x" by (auto intro: less_le_trans) |
257 thus "\<exists>x. \<forall>y\<in>U. x \<^loc>< y" by blast |
257 thus "\<exists>x. \<forall>y\<in>U. x \<^loc>< y" by blast |
258 qed |
258 qed |
259 |
259 |
260 lemma exists_neq: "\<exists>(x::'a). x \<noteq> t" "\<exists>(x::'a). t \<noteq> x" |
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 |
261 using gt_ex[rule_format, of t] by auto |
262 |
262 |
263 lemmas dlo_simps = order_refl less_irrefl not_less not_le exists_neq |
263 lemmas dlo_simps = order_refl less_irrefl not_less not_le exists_neq |
264 le_less neq_iff linear less_not_permute |
264 le_less neq_iff linear less_not_permute |
265 |
265 |
266 lemma axiom: "dense_linear_order (op \<sqsubseteq>) (op \<sqsubset>)" . |
266 lemma axiom: "dense_linear_order (op \<^loc>\<le>) (op \<^loc><)" . |
267 lemma atoms: includes meta_term_syntax |
267 lemma atoms: |
268 shows "TERM (op \<sqsubset> :: 'a \<Rightarrow> _)" and "TERM (op \<sqsubseteq>)" and "TERM (op = :: 'a \<Rightarrow> _)" . |
268 includes meta_term_syntax |
|
269 shows "TERM (less :: 'a \<Rightarrow> _)" |
|
270 and "TERM (less_eq :: 'a \<Rightarrow> _)" |
|
271 and "TERM (op = :: 'a \<Rightarrow> _)" . |
269 |
272 |
270 declare axiom[langford qe: dlo_qe_bnds dlo_qe_nolb dlo_qe_noub gather: gather_start gather_simps atoms: atoms] |
273 declare axiom[langford qe: dlo_qe_bnds dlo_qe_nolb dlo_qe_noub gather: gather_start gather_simps atoms: atoms] |
271 declare dlo_simps[langfordsimp] |
274 declare dlo_simps[langfordsimp] |
272 |
275 |
273 end |
276 end |
298 section {* Contructive dense linear orders yield QE for linear arithmetic over ordered Fields -- see @{text "Arith_Tools.thy"} *} |
301 section {* Contructive dense linear orders yield QE for linear arithmetic over ordered Fields -- see @{text "Arith_Tools.thy"} *} |
299 |
302 |
300 text {* Linear order without upper bounds *} |
303 text {* Linear order without upper bounds *} |
301 |
304 |
302 class linorder_no_ub = linorder + |
305 class linorder_no_ub = linorder + |
303 assumes gt_ex: "\<exists>y. x \<sqsubset> y" |
306 assumes gt_ex: "\<exists>y. x \<^loc>< y" |
304 begin |
307 begin |
305 |
308 |
306 lemma ge_ex: "\<exists>y. x \<sqsubseteq> y" using gt_ex by auto |
309 lemma ge_ex: "\<exists>y. x \<^loc>\<le> y" using gt_ex by auto |
307 |
310 |
308 text {* Theorems for @{text "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"} *} |
311 text {* Theorems for @{text "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"} *} |
309 lemma pinf_conj: |
312 lemma pinf_conj: |
310 assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')" |
313 assumes ex1: "\<exists>z1. \<forall>x. z1 \<^loc>< x \<longrightarrow> (P1 x \<longleftrightarrow> P1')" |
311 and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" |
314 and ex2: "\<exists>z2. \<forall>x. z2 \<^loc>< x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" |
312 shows "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))" |
315 shows "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))" |
313 proof- |
316 proof- |
314 from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')" |
317 from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 \<^loc>< x \<longrightarrow> (P1 x \<longleftrightarrow> P1')" |
315 and z2: "\<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast |
318 and z2: "\<forall>x. z2 \<^loc>< x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast |
316 from gt_ex obtain z where z:"max z1 z2 \<sqsubset> z" by blast |
319 from gt_ex obtain z where z:"max z1 z2 \<^loc>< z" by blast |
317 from z have zz1: "z1 \<sqsubset> z" and zz2: "z2 \<sqsubset> z" by simp_all |
320 from z have zz1: "z1 \<^loc>< z" and zz2: "z2 \<^loc>< z" by simp_all |
318 {fix x assume H: "z \<sqsubset> x" |
321 {fix x assume H: "z \<^loc>< x" |
319 from less_trans[OF zz1 H] less_trans[OF zz2 H] |
322 from less_trans[OF zz1 H] less_trans[OF zz2 H] |
320 have "(P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2')" using z1 zz1 z2 zz2 by auto |
323 have "(P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2')" using z1 zz1 z2 zz2 by auto |
321 } |
324 } |
322 thus ?thesis by blast |
325 thus ?thesis by blast |
323 qed |
326 qed |
324 |
327 |
325 lemma pinf_disj: |
328 lemma pinf_disj: |
326 assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')" |
329 assumes ex1: "\<exists>z1. \<forall>x. z1 \<^loc>< x \<longrightarrow> (P1 x \<longleftrightarrow> P1')" |
327 and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" |
330 and ex2: "\<exists>z2. \<forall>x. z2 \<^loc>< x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" |
328 shows "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))" |
331 shows "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))" |
329 proof- |
332 proof- |
330 from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')" |
333 from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 \<^loc>< x \<longrightarrow> (P1 x \<longleftrightarrow> P1')" |
331 and z2: "\<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast |
334 and z2: "\<forall>x. z2 \<^loc>< x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast |
332 from gt_ex obtain z where z:"max z1 z2 \<sqsubset> z" by blast |
335 from gt_ex obtain z where z:"max z1 z2 \<^loc>< z" by blast |
333 from z have zz1: "z1 \<sqsubset> z" and zz2: "z2 \<sqsubset> z" by simp_all |
336 from z have zz1: "z1 \<^loc>< z" and zz2: "z2 \<^loc>< z" by simp_all |
334 {fix x assume H: "z \<sqsubset> x" |
337 {fix x assume H: "z \<^loc>< x" |
335 from less_trans[OF zz1 H] less_trans[OF zz2 H] |
338 from less_trans[OF zz1 H] less_trans[OF zz2 H] |
336 have "(P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2')" using z1 zz1 z2 zz2 by auto |
339 have "(P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2')" using z1 zz1 z2 zz2 by auto |
337 } |
340 } |
338 thus ?thesis by blast |
341 thus ?thesis by blast |
339 qed |
342 qed |
340 |
343 |
341 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" |
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" |
342 proof- |
345 proof- |
343 from ex obtain z where z: "\<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast |
346 from ex obtain z where z: "\<forall>x. z \<^loc>< x \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast |
344 from gt_ex obtain x where x: "z \<sqsubset> x" by blast |
347 from gt_ex obtain x where x: "z \<^loc>< x" by blast |
345 from z x p1 show ?thesis by blast |
348 from z x p1 show ?thesis by blast |
346 qed |
349 qed |
347 |
350 |
348 end |
351 end |
349 |
352 |
350 text {* Linear order without upper bounds *} |
353 text {* Linear order without upper bounds *} |
351 |
354 |
352 class linorder_no_lb = linorder + |
355 class linorder_no_lb = linorder + |
353 assumes lt_ex: "\<exists>y. y \<sqsubset> x" |
356 assumes lt_ex: "\<exists>y. y \<^loc>< x" |
354 begin |
357 begin |
355 |
358 |
356 lemma le_ex: "\<exists>y. y \<sqsubseteq> x" using lt_ex by auto |
359 lemma le_ex: "\<exists>y. y \<^loc>\<le> x" using lt_ex by auto |
357 |
360 |
358 |
361 |
359 text {* Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"} *} |
362 text {* Theorems for @{text "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"} *} |
360 lemma minf_conj: |
363 lemma minf_conj: |
361 assumes ex1: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')" |
364 assumes ex1: "\<exists>z1. \<forall>x. x \<^loc>< z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')" |
362 and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')" |
365 and ex2: "\<exists>z2. \<forall>x. x \<^loc>< z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')" |
363 shows "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))" |
366 shows "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))" |
364 proof- |
367 proof- |
365 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 |
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 |
366 from lt_ex obtain z where z:"z \<sqsubset> min z1 z2" by blast |
369 from lt_ex obtain z where z:"z \<^loc>< min z1 z2" by blast |
367 from z have zz1: "z \<sqsubset> z1" and zz2: "z \<sqsubset> z2" by simp_all |
370 from z have zz1: "z \<^loc>< z1" and zz2: "z \<^loc>< z2" by simp_all |
368 {fix x assume H: "x \<sqsubset> z" |
371 {fix x assume H: "x \<^loc>< z" |
369 from less_trans[OF H zz1] less_trans[OF H zz2] |
372 from less_trans[OF H zz1] less_trans[OF H zz2] |
370 have "(P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2')" using z1 zz1 z2 zz2 by auto |
373 have "(P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2')" using z1 zz1 z2 zz2 by auto |
371 } |
374 } |
372 thus ?thesis by blast |
375 thus ?thesis by blast |
373 qed |
376 qed |
374 |
377 |
375 lemma minf_disj: |
378 lemma minf_disj: |
376 assumes ex1: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')" |
379 assumes ex1: "\<exists>z1. \<forall>x. x \<^loc>< z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')" |
377 and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')" |
380 and ex2: "\<exists>z2. \<forall>x. x \<^loc>< z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')" |
378 shows "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))" |
381 shows "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))" |
379 proof- |
382 proof- |
380 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 |
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 |
381 from lt_ex obtain z where z:"z \<sqsubset> min z1 z2" by blast |
384 from lt_ex obtain z where z:"z \<^loc>< min z1 z2" by blast |
382 from z have zz1: "z \<sqsubset> z1" and zz2: "z \<sqsubset> z2" by simp_all |
385 from z have zz1: "z \<^loc>< z1" and zz2: "z \<^loc>< z2" by simp_all |
383 {fix x assume H: "x \<sqsubset> z" |
386 {fix x assume H: "x \<^loc>< z" |
384 from less_trans[OF H zz1] less_trans[OF H zz2] |
387 from less_trans[OF H zz1] less_trans[OF H zz2] |
385 have "(P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2')" using z1 zz1 z2 zz2 by auto |
388 have "(P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2')" using z1 zz1 z2 zz2 by auto |
386 } |
389 } |
387 thus ?thesis by blast |
390 thus ?thesis by blast |
388 qed |
391 qed |
389 |
392 |
390 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" |
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" |
391 proof- |
394 proof- |
392 from ex obtain z where z: "\<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast |
395 from ex obtain z where z: "\<forall>x. x \<^loc>< z \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast |
393 from lt_ex obtain x where x: "x \<sqsubset> z" by blast |
396 from lt_ex obtain x where x: "x \<^loc>< z" by blast |
394 from z x p1 show ?thesis by blast |
397 from z x p1 show ?thesis by blast |
395 qed |
398 qed |
396 |
399 |
397 end |
400 end |
398 |
401 |
399 |
402 |
400 class constr_dense_linear_order = linorder_no_lb + linorder_no_ub + |
403 class constr_dense_linear_order = linorder_no_lb + linorder_no_ub + |
401 fixes between |
404 fixes between |
402 assumes between_less: "x \<sqsubset> y \<Longrightarrow> x \<sqsubset> between x y \<and> between x y \<sqsubset> y" |
405 assumes between_less: "x \<^loc>< y \<Longrightarrow> x \<^loc>< between x y \<and> between x y \<^loc>< y" |
403 and between_same: "between x x = x" |
406 and between_same: "between x x = x" |
404 |
407 |
405 instance advanced constr_dense_linear_order < dense_linear_order |
408 instance advanced constr_dense_linear_order < dense_linear_order |
406 apply unfold_locales |
409 apply unfold_locales |
407 using gt_ex lt_ex between_less |
410 using gt_ex lt_ex between_less |
414 context constr_dense_linear_order |
417 context constr_dense_linear_order |
415 begin |
418 begin |
416 |
419 |
417 lemma rinf_U: |
420 lemma rinf_U: |
418 assumes fU: "finite U" |
421 assumes fU: "finite U" |
419 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 |
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 |
420 \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P y )" |
423 \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> P y )" |
421 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')" |
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')" |
422 and nmi: "\<not> MP" and npi: "\<not> PP" and ex: "\<exists> x. P x" |
425 and nmi: "\<not> MP" and npi: "\<not> PP" and ex: "\<exists> x. P x" |
423 shows "\<exists> u\<in> U. \<exists> u' \<in> U. P (between u u')" |
426 shows "\<exists> u\<in> U. \<exists> u' \<in> U. P (between u u')" |
424 proof- |
427 proof- |
425 from ex obtain x where px: "P x" by blast |
428 from ex obtain x where px: "P x" by blast |
426 from px nmi npi nmpiU have "\<exists> u\<in> U. \<exists> u' \<in> U. u \<sqsubseteq> x \<and> x \<sqsubseteq> u'" by auto |
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 |
427 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 |
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 |
428 from uU have Une: "U \<noteq> {}" by auto |
431 from uU have Une: "U \<noteq> {}" by auto |
429 let ?l = "Min U" |
432 let ?l = "Min U" |
430 let ?u = "Max U" |
433 let ?u = "Max U" |
431 have linM: "?l \<in> U" using fU Une by simp |
434 have linM: "?l \<in> U" using fU Une by simp |
432 have uinM: "?u \<in> U" using fU Une by simp |
435 have uinM: "?u \<in> U" using fU Une by simp |
433 have lM: "\<forall> t\<in> U. ?l \<sqsubseteq> t" using Une fU by auto |
436 have lM: "\<forall> t\<in> U. ?l \<^loc>\<le> t" using Une fU by auto |
434 have Mu: "\<forall> t\<in> U. t \<sqsubseteq> ?u" using Une fU by auto |
437 have Mu: "\<forall> t\<in> U. t \<^loc>\<le> ?u" using Une fU by auto |
435 have th:"?l \<sqsubseteq> u" using uU Une lM by auto |
438 have th:"?l \<^loc>\<le> u" using uU Une lM by auto |
436 from order_trans[OF th ux] have lx: "?l \<sqsubseteq> x" . |
439 from order_trans[OF th ux] have lx: "?l \<^loc>\<le> x" . |
437 have th: "u' \<sqsubseteq> ?u" using uU' Une Mu by simp |
440 have th: "u' \<^loc>\<le> ?u" using uU' Une Mu by simp |
438 from order_trans[OF xu' th] have xu: "x \<sqsubseteq> ?u" . |
441 from order_trans[OF xu' th] have xu: "x \<^loc>\<le> ?u" . |
439 from finite_set_intervals2[where P="P",OF px lx xu linM uinM fU lM Mu] |
442 from finite_set_intervals2[where P="P",OF px lx xu linM uinM fU lM Mu] |
440 have "(\<exists> s\<in> U. P s) \<or> |
443 have "(\<exists> s\<in> U. P s) \<or> |
441 (\<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)" . |
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)" . |
442 moreover { fix u assume um: "u\<in>U" and pu: "P u" |
445 moreover { fix u assume um: "u\<in>U" and pu: "P u" |
443 have "between u u = u" by (simp add: between_same) |
446 have "between u u = u" by (simp add: between_same) |
444 with um pu have "P (between u u)" by simp |
447 with um pu have "P (between u u)" by simp |
445 with um have ?thesis by blast} |
448 with um have ?thesis by blast} |
446 moreover{ |
449 moreover{ |
447 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" |
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" |
448 then obtain t1 and t2 where t1M: "t1 \<in> U" and t2M: "t2\<in> U" |
451 then obtain t1 and t2 where t1M: "t1 \<in> U" and t2M: "t2\<in> U" |
449 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" |
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" |
450 by blast |
453 by blast |
451 from less_trans[OF t1x xt2] have t1t2: "t1 \<sqsubset> t2" . |
454 from less_trans[OF t1x xt2] have t1t2: "t1 \<^loc>< t2" . |
452 let ?u = "between t1 t2" |
455 let ?u = "between t1 t2" |
453 from between_less t1t2 have t1lu: "t1 \<sqsubset> ?u" and ut2: "?u \<sqsubset> t2" by auto |
456 from between_less t1t2 have t1lu: "t1 \<^loc>< ?u" and ut2: "?u \<^loc>< t2" by auto |
454 from lin_dense[rule_format, OF] noM t1x xt2 px t1lu ut2 have "P ?u" by blast |
457 from lin_dense[rule_format, OF] noM t1x xt2 px t1lu ut2 have "P ?u" by blast |
455 with t1M t2M have ?thesis by blast} |
458 with t1M t2M have ?thesis by blast} |
456 ultimately show ?thesis by blast |
459 ultimately show ?thesis by blast |
457 qed |
460 qed |
458 |
461 |
459 theorem fr_eq: |
462 theorem fr_eq: |
460 assumes fU: "finite U" |
463 assumes fU: "finite U" |
461 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 |
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 |
462 \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P y )" |
465 \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> P y )" |
463 and nmibnd: "\<forall>x. \<not> MP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<sqsubseteq> x)" |
466 and nmibnd: "\<forall>x. \<not> MP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x)" |
464 and npibnd: "\<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. x \<sqsubseteq> u)" |
467 and npibnd: "\<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. x \<^loc>\<le> u)" |
465 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)" |
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)" |
466 shows "(\<exists> x. P x) \<equiv> (MP \<or> PP \<or> (\<exists> u \<in> U. \<exists> u'\<in> U. P (between u u')))" |
469 shows "(\<exists> x. P x) \<equiv> (MP \<or> PP \<or> (\<exists> u \<in> U. \<exists> u'\<in> U. P (between u u')))" |
467 (is "_ \<equiv> (_ \<or> _ \<or> ?F)" is "?E \<equiv> ?D") |
470 (is "_ \<equiv> (_ \<or> _ \<or> ?F)" is "?E \<equiv> ?D") |
468 proof- |
471 proof- |
469 { |
472 { |
470 assume px: "\<exists> x. P x" |
473 assume px: "\<exists> x. P x" |
471 have "MP \<or> PP \<or> (\<not> MP \<and> \<not> PP)" by blast |
474 have "MP \<or> PP \<or> (\<not> MP \<and> \<not> PP)" by blast |
472 moreover {assume "MP \<or> PP" hence "?D" by blast} |
475 moreover {assume "MP \<or> PP" hence "?D" by blast} |
473 moreover {assume nmi: "\<not> MP" and npi: "\<not> PP" |
476 moreover {assume nmi: "\<not> MP" and npi: "\<not> PP" |
474 from npmibnd[OF nmibnd npibnd] |
477 from npmibnd[OF nmibnd npibnd] |
475 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')" . |
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')" . |
476 from rinf_U[OF fU lin_dense nmpiU nmi npi px] have "?D" by blast} |
479 from rinf_U[OF fU lin_dense nmpiU nmi npi px] have "?D" by blast} |
477 ultimately have "?D" by blast} |
480 ultimately have "?D" by blast} |
478 moreover |
481 moreover |
479 { assume "?D" |
482 { assume "?D" |
480 moreover {assume m:"MP" from minf_ex[OF mi m] have "?E" .} |
483 moreover {assume m:"MP" from minf_ex[OF mi m] have "?E" .} |