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