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