author  haftmann 
Tue, 04 May 2010 08:55:43 +0200  
changeset 36635  080b755377c0 
parent 35828  46cfc4b8112e 
child 36753  5cf4e9128f22 
permissions  rwrr 
30439  1 
(* Title : HOL/Decision_Procs/Dense_Linear_Order.thy 
29655
ac31940cfb69
Plain, Main form meeting points in import hierarchy
haftmann
parents:
29509
diff
changeset

2 
Author : Amine Chaieb, TU Muenchen 
ac31940cfb69
Plain, Main form meeting points in import hierarchy
haftmann
parents:
29509
diff
changeset

3 
*) 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

4 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

5 
header {* Dense linear order without endpoints 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

6 
and a quantifier elimination procedure in Ferrante and Rackoff style *} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

7 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

8 
theory Dense_Linear_Order 
30738  9 
imports Main 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

10 
uses 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

11 
"~~/src/HOL/Tools/Qelim/langford_data.ML" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

12 
"~~/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

13 
("~~/src/HOL/Tools/Qelim/langford.ML") 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

14 
("~~/src/HOL/Tools/Qelim/ferrante_rackoff.ML") 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

15 
begin 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

16 

28402  17 
setup {* Langford_Data.setup #> Ferrante_Rackoff_Data.setup *} 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

18 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

19 
context linorder 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

20 
begin 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

21 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

22 
lemma less_not_permute[no_atp]: "\<not> (x < y \<and> y < x)" by (simp add: not_less linear) 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

23 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

24 
lemma gather_simps[no_atp]: 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

25 
shows 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

26 
"(\<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)" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

27 
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)" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

28 
"(\<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))" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

29 
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 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

30 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

31 
lemma 
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

32 
gather_start[no_atp]: "(\<exists>x. P x) \<equiv> (\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y\<in> {}. x < y) \<and> P x)" 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

33 
by simp 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

34 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

35 
text{* Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>\<infinity>\<^esub>)"}*} 
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

36 
lemma minf_lt[no_atp]: "\<exists>z . \<forall>x. x < z \<longrightarrow> (x < t \<longleftrightarrow> True)" by auto 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

37 
lemma minf_gt[no_atp]: "\<exists>z . \<forall>x. x < z \<longrightarrow> (t < x \<longleftrightarrow> False)" 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

38 
by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

39 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

40 
lemma minf_le[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<le> t \<longleftrightarrow> True)" by (auto simp add: less_le) 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

41 
lemma minf_ge[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (t \<le> x \<longleftrightarrow> False)" 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

42 
by (auto simp add: less_le not_less not_le) 
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

43 
lemma minf_eq[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

44 
lemma minf_neq[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

45 
lemma minf_P[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (P \<longleftrightarrow> P)" by blast 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

46 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

47 
text{* Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"}*} 
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

48 
lemma pinf_gt[no_atp]: "\<exists>z . \<forall>x. z < x \<longrightarrow> (t < x \<longleftrightarrow> True)" by auto 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

49 
lemma pinf_lt[no_atp]: "\<exists>z . \<forall>x. z < x \<longrightarrow> (x < t \<longleftrightarrow> False)" 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

50 
by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

51 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

52 
lemma pinf_ge[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (t \<le> x \<longleftrightarrow> True)" by (auto simp add: less_le) 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

53 
lemma pinf_le[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x \<le> t \<longleftrightarrow> False)" 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

54 
by (auto simp add: less_le not_less not_le) 
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

55 
lemma pinf_eq[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

56 
lemma pinf_neq[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

57 
lemma pinf_P[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (P \<longleftrightarrow> P)" by blast 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

58 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

59 
lemma nmi_lt[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x < t \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

60 
lemma nmi_gt[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t < x \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

61 
by (auto simp add: le_less) 
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

62 
lemma nmi_le[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x\<le> t \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

63 
lemma nmi_ge[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t\<le> x \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

64 
lemma nmi_eq[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> x = t \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

65 
lemma nmi_neq[no_atp]: "t \<in> U \<Longrightarrow>\<forall>x. \<not>True \<and> x \<noteq> t \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

66 
lemma nmi_P[no_atp]: "\<forall> x. ~P \<and> P \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

67 
lemma nmi_conj[no_atp]: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow> (\<exists> u\<in> U. u \<le> x) ; 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

68 
\<forall>x. \<not>P2' \<and> P2 x \<longrightarrow> (\<exists> u\<in> U. u \<le> x)\<rbrakk> \<Longrightarrow> 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

69 
\<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto 
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

70 
lemma nmi_disj[no_atp]: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow> (\<exists> u\<in> U. u \<le> x) ; 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

71 
\<forall>x. \<not>P2' \<and> P2 x \<longrightarrow> (\<exists> u\<in> U. u \<le> x)\<rbrakk> \<Longrightarrow> 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

72 
\<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

73 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

74 
lemma npi_lt[no_atp]: "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) 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

75 
lemma npi_gt[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> t < x \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by auto 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

76 
lemma npi_le[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> x \<le> t \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by auto 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

77 
lemma npi_ge[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> t \<le> x \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by auto 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

78 
lemma npi_eq[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> x = t \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by auto 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

79 
lemma npi_neq[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x \<noteq> t \<longrightarrow> (\<exists> u\<in> U. x \<le> u )" by auto 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

80 
lemma npi_P[no_atp]: "\<forall> x. ~P \<and> P \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by auto 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

81 
lemma npi_conj[no_atp]: "\<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> 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

82 
\<Longrightarrow> \<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by auto 
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

83 
lemma npi_disj[no_atp]: "\<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> 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

84 
\<Longrightarrow> \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by auto 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

85 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

86 
lemma lin_dense_lt[no_atp]: "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)" 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

87 
proof(clarsimp) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

88 
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" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

89 
and xu: "x<u" and px: "x < t" and ly: "l<y" and yu:"y < u" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

90 
from tU noU ly yu have tny: "t\<noteq>y" by auto 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

91 
{assume H: "t < y" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

92 
from less_trans[OF lx px] less_trans[OF H yu] 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

93 
have "l < t \<and> t < u" by simp 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

94 
with tU noU have "False" by auto} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

95 
hence "\<not> t < y" by auto hence "y \<le> t" by (simp add: not_less) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

96 
thus "y < t" using tny by (simp add: less_le) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

97 
qed 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

98 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

99 
lemma lin_dense_gt[no_atp]: "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)" 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

100 
proof(clarsimp) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

101 
fix x l u y 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

102 
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" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

103 
and px: "t < x" and ly: "l<y" and yu:"y < u" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

104 
from tU noU ly yu have tny: "t\<noteq>y" by auto 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

105 
{assume H: "y< t" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

106 
from less_trans[OF ly H] less_trans[OF px xu] have "l < t \<and> t < u" by simp 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

107 
with tU noU have "False" by auto} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

108 
hence "\<not> y<t" by auto hence "t \<le> y" by (auto simp add: not_less) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

109 
thus "t < y" using tny by (simp add:less_le) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

110 
qed 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

111 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

112 
lemma lin_dense_le[no_atp]: "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)" 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

113 
proof(clarsimp) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

114 
fix x l u y 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

115 
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" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

116 
and px: "x \<le> t" and ly: "l<y" and yu:"y < u" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

117 
from tU noU ly yu have tny: "t\<noteq>y" by auto 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

118 
{assume H: "t < y" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

119 
from less_le_trans[OF lx px] less_trans[OF H yu] 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

120 
have "l < t \<and> t < u" by simp 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

121 
with tU noU have "False" by auto} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

122 
hence "\<not> t < y" by auto thus "y \<le> t" by (simp add: not_less) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

123 
qed 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

124 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

125 
lemma lin_dense_ge[no_atp]: "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)" 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

126 
proof(clarsimp) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

127 
fix x l u y 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

128 
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" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

129 
and px: "t \<le> x" and ly: "l<y" and yu:"y < u" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

130 
from tU noU ly yu have tny: "t\<noteq>y" by auto 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

131 
{assume H: "y< t" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

132 
from less_trans[OF ly H] le_less_trans[OF px xu] 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

133 
have "l < t \<and> t < u" by simp 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

134 
with tU noU have "False" by auto} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

135 
hence "\<not> y<t" by auto thus "t \<le> y" by (simp add: not_less) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

136 
qed 
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

137 
lemma lin_dense_eq[no_atp]: "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 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

138 
lemma lin_dense_neq[no_atp]: "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 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

139 
lemma lin_dense_P[no_atp]: "\<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 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

140 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

141 
lemma lin_dense_conj[no_atp]: 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

142 
"\<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 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

143 
\<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P1 y) ; 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

144 
\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P2 x 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

145 
\<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow> 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

146 
\<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) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

147 
\<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> (P1 y \<and> P2 y))" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

148 
by blast 
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

149 
lemma lin_dense_disj[no_atp]: 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

150 
"\<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 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

151 
\<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P1 y) ; 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

152 
\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P2 x 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

153 
\<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow> 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

154 
\<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) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

155 
\<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> (P1 y \<or> P2 y))" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

156 
by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

157 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

158 
lemma npmibnd[no_atp]: "\<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> 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

159 
\<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')" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

160 
by auto 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

161 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

162 
lemma finite_set_intervals[no_atp]: 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

163 
assumes px: "P x" and lx: "l \<le> x" and xu: "x \<le> u" and linS: "l\<in> S" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

164 
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" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

165 
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" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

166 
proof 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

167 
let ?Mx = "{y. y\<in> S \<and> y \<le> x}" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

168 
let ?xM = "{y. y\<in> S \<and> x \<le> y}" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

169 
let ?a = "Max ?Mx" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

170 
let ?b = "Min ?xM" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

171 
have MxS: "?Mx \<subseteq> S" by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

172 
hence fMx: "finite ?Mx" using fS finite_subset by auto 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

173 
from lx linS have linMx: "l \<in> ?Mx" by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

174 
hence Mxne: "?Mx \<noteq> {}" by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

175 
have xMS: "?xM \<subseteq> S" by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

176 
hence fxM: "finite ?xM" using fS finite_subset by auto 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

177 
from xu uinS have linxM: "u \<in> ?xM" by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

178 
hence xMne: "?xM \<noteq> {}" by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

179 
have ax:"?a \<le> x" using Mxne fMx by auto 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

180 
have xb:"x \<le> ?b" using xMne fxM by auto 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

181 
have "?a \<in> ?Mx" using Max_in[OF fMx Mxne] by simp hence ainS: "?a \<in> S" using MxS by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

182 
have "?b \<in> ?xM" using Min_in[OF fxM xMne] by simp hence binS: "?b \<in> S" using xMS by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

183 
have noy:"\<forall> y. ?a < y \<and> y < ?b \<longrightarrow> y \<notin> S" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

184 
proof(clarsimp) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

185 
fix y assume ay: "?a < y" and yb: "y < ?b" and yS: "y \<in> S" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

186 
from yS have "y\<in> ?Mx \<or> y\<in> ?xM" by (auto simp add: linear) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

187 
moreover {assume "y \<in> ?Mx" hence "y \<le> ?a" using Mxne fMx by auto with ay have "False" by (simp add: not_le[symmetric])} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

188 
moreover {assume "y \<in> ?xM" hence "?b \<le> y" using xMne fxM by auto with yb have "False" by (simp add: not_le[symmetric])} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

189 
ultimately show "False" by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

190 
qed 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

191 
from ainS binS noy ax xb px show ?thesis by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

192 
qed 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

193 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

194 
lemma finite_set_intervals2[no_atp]: 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

195 
assumes px: "P x" and lx: "l \<le> x" and xu: "x \<le> u" and linS: "l\<in> S" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

196 
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" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

197 
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)" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

198 
proof 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

199 
from finite_set_intervals[where P="P", OF px lx xu linS uinS fS lS Su] 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

200 
obtain a and b where 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

201 
as: "a\<in> S" and bs: "b\<in> S" and noS:"\<forall>y. a < y \<and> y < b \<longrightarrow> y \<notin> S" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

202 
and axb: "a \<le> x \<and> x \<le> b \<and> P x" by auto 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

203 
from axb have "x= a \<or> x= b \<or> (a < x \<and> x < b)" by (auto simp add: le_less) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

204 
thus ?thesis using px as bs noS by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

205 
qed 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

206 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

207 
end 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

208 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

209 
section {* The classical QE after Langford for dense linear orders *} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

210 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34974
diff
changeset

211 
context dense_linorder 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

212 
begin 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

213 

27825  214 
lemma interval_empty_iff: 
215 
"{y. x < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z" 

216 
by (auto dest: dense) 

217 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

218 
lemma dlo_qe_bnds[no_atp]: 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

219 
assumes ne: "L \<noteq> {}" and neU: "U \<noteq> {}" and fL: "finite L" and fU: "finite U" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

220 
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)" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

221 
proof (simp only: atomize_eq, rule iffI) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

222 
assume H: "\<exists>x. (\<forall>y\<in>L. y < x) \<and> (\<forall>y\<in>U. x < y)" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

223 
then obtain x where xL: "\<forall>y\<in>L. y < x" and xU: "\<forall>y\<in>U. x < y" by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

224 
{fix l u assume l: "l \<in> L" and u: "u \<in> U" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

225 
have "l < x" using xL l by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

226 
also have "x < u" using xU u by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

227 
finally (less_trans) have "l < u" .} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

228 
thus "\<forall>l\<in>L. \<forall>u\<in>U. l < u" by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

229 
next 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

230 
assume H: "\<forall>l\<in>L. \<forall>u\<in>U. l < u" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

231 
let ?ML = "Max L" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

232 
let ?MU = "Min U" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

233 
from fL ne have th1: "?ML \<in> L" and th1': "\<forall>l\<in>L. l \<le> ?ML" by auto 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

234 
from fU neU have th2: "?MU \<in> U" and th2': "\<forall>u\<in>U. ?MU \<le> u" by auto 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

235 
from th1 th2 H have "?ML < ?MU" by auto 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

236 
with dense obtain w where th3: "?ML < w" and th4: "w < ?MU" by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

237 
from th3 th1' have "\<forall>l \<in> L. l < w" by auto 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

238 
moreover from th4 th2' have "\<forall>u \<in> U. w < u" by auto 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

239 
ultimately show "\<exists>x. (\<forall>y\<in>L. y < x) \<and> (\<forall>y\<in>U. x < y)" by auto 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

240 
qed 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

241 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

242 
lemma dlo_qe_noub[no_atp]: 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

243 
assumes ne: "L \<noteq> {}" and fL: "finite L" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

244 
shows "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> {}. x < y)) \<equiv> True" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

245 
proof(simp add: atomize_eq) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

246 
from gt_ex[of "Max L"] obtain M where M: "Max L < M" by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

247 
from ne fL have "\<forall>x \<in> L. x \<le> Max L" by simp 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

248 
with M have "\<forall>x\<in>L. x < M" by (auto intro: le_less_trans) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

249 
thus "\<exists>x. \<forall>y\<in>L. y < x" by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

250 
qed 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

251 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

252 
lemma dlo_qe_nolb[no_atp]: 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

253 
assumes ne: "U \<noteq> {}" and fU: "finite U" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

254 
shows "(\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y \<in> U. x < y)) \<equiv> True" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

255 
proof(simp add: atomize_eq) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

256 
from lt_ex[of "Min U"] obtain M where M: "M < Min U" by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

257 
from ne fU have "\<forall>x \<in> U. Min U \<le> x" by simp 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

258 
with M have "\<forall>x\<in>U. M < x" by (auto intro: less_le_trans) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

259 
thus "\<exists>x. \<forall>y\<in>U. x < y" by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

260 
qed 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

261 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

262 
lemma exists_neq[no_atp]: "\<exists>(x::'a). x \<noteq> t" "\<exists>(x::'a). t \<noteq> x" 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

263 
using gt_ex[of t] by auto 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

264 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

265 
lemmas dlo_simps[no_atp] = order_refl less_irrefl not_less not_le exists_neq 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

266 
le_less neq_iff linear less_not_permute 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

267 

36635
080b755377c0
locale predicates of classes carry a mandatory "class" prefix
haftmann
parents:
35828
diff
changeset

268 
lemma axiom[no_atp]: "class.dense_linorder (op \<le>) (op <)" by (rule dense_linorder_axioms) 
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

269 
lemma atoms[no_atp]: 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

270 
shows "TERM (less :: 'a \<Rightarrow> _)" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

271 
and "TERM (less_eq :: 'a \<Rightarrow> _)" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

272 
and "TERM (op = :: 'a \<Rightarrow> _)" . 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

273 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

274 
declare axiom[langford qe: dlo_qe_bnds dlo_qe_nolb dlo_qe_noub gather: gather_start gather_simps atoms: atoms] 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

275 
declare dlo_simps[langfordsimp] 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

276 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

277 
end 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

278 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

279 
(* FIXME: Move to HOL  together with the conj_aci_rule in langford.ML *) 
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

280 
lemma dnf[no_atp]: 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

281 
"(P & (Q  R)) = ((P&Q)  (P&R))" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

282 
"((Q  R) & P) = ((Q&P)  (R&P))" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

283 
by blast+ 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

284 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

285 
lemmas weak_dnf_simps[no_atp] = simp_thms dnf 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

286 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

287 
lemma nnf_simps[no_atp]: 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

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)" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

289 
"(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

290 
by blast+ 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

291 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

292 
lemma ex_distrib[no_atp]: "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> ((\<exists>x. P x) \<or> (\<exists>x. Q x))" by blast 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

293 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

294 
lemmas dnf_simps[no_atp] = weak_dnf_simps nnf_simps ex_distrib 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

295 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

296 
use "~~/src/HOL/Tools/Qelim/langford.ML" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

297 
method_setup dlo = {* 
30549  298 
Scan.succeed (SIMPLE_METHOD' o LangfordQE.dlo_tac) 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

299 
*} "Langford's algorithm for quantifier elimination in dense linear orders" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

300 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

301 

30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30549
diff
changeset

302 
section {* Contructive dense linear orders yield QE for linear arithmetic over ordered Fields *} 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

303 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

304 
text {* Linear order without upper bounds *} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

305 

29509
1ff0f3f08a7b
migrated class package to new locale implementation
haftmann
parents:
29252
diff
changeset

306 
locale linorder_stupid_syntax = linorder 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

307 
begin 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

308 
notation 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

309 
less_eq ("op \<sqsubseteq>") and 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

310 
less_eq ("(_/ \<sqsubseteq> _)" [51, 51] 50) and 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

311 
less ("op \<sqsubset>") and 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

312 
less ("(_/ \<sqsubset> _)" [51, 51] 50) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

313 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

314 
end 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

315 

29509
1ff0f3f08a7b
migrated class package to new locale implementation
haftmann
parents:
29252
diff
changeset

316 
locale linorder_no_ub = linorder_stupid_syntax + 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

317 
assumes gt_ex: "\<exists>y. less x y" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

318 
begin 
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

319 
lemma ge_ex[no_atp]: "\<exists>y. x \<sqsubseteq> y" using gt_ex by auto 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

320 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

321 
text {* Theorems for @{text "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"} *} 
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

322 
lemma pinf_conj[no_atp]: 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

323 
assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

324 
and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

325 
shows "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

326 
proof 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

327 
from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

328 
and z2: "\<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

329 
from gt_ex obtain z where z:"ord.max less_eq z1 z2 \<sqsubset> z" by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

330 
from z have zz1: "z1 \<sqsubset> z" and zz2: "z2 \<sqsubset> z" by simp_all 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

331 
{fix x assume H: "z \<sqsubset> x" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

332 
from less_trans[OF zz1 H] less_trans[OF zz2 H] 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

333 
have "(P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2')" using z1 zz1 z2 zz2 by auto 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

334 
} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

335 
thus ?thesis by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

336 
qed 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

337 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

338 
lemma pinf_disj[no_atp]: 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

339 
assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

340 
and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

341 
shows "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

342 
proof 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

343 
from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

344 
and z2: "\<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

345 
from gt_ex obtain z where z:"ord.max less_eq z1 z2 \<sqsubset> z" by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

346 
from z have zz1: "z1 \<sqsubset> z" and zz2: "z2 \<sqsubset> z" by simp_all 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

347 
{fix x assume H: "z \<sqsubset> x" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

348 
from less_trans[OF zz1 H] less_trans[OF zz2 H] 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

349 
have "(P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2')" using z1 zz1 z2 zz2 by auto 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

350 
} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

351 
thus ?thesis by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

352 
qed 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

353 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

354 
lemma pinf_ex[no_atp]: assumes ex:"\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x" 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

355 
proof 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

356 
from ex obtain z where z: "\<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

357 
from gt_ex obtain x where x: "z \<sqsubset> x" by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

358 
from z x p1 show ?thesis by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

359 
qed 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

360 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

361 
end 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

362 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

363 
text {* Linear order without upper bounds *} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

364 

29509
1ff0f3f08a7b
migrated class package to new locale implementation
haftmann
parents:
29252
diff
changeset

365 
locale linorder_no_lb = linorder_stupid_syntax + 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

366 
assumes lt_ex: "\<exists>y. less y x" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

367 
begin 
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

368 
lemma le_ex[no_atp]: "\<exists>y. y \<sqsubseteq> x" using lt_ex by auto 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

369 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

370 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

371 
text {* Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>\<infinity>\<^esub>)"} *} 
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

372 
lemma minf_conj[no_atp]: 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

373 
assumes ex1: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

374 
and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

375 
shows "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

376 
proof 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

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 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

378 
from lt_ex obtain z where z:"z \<sqsubset> ord.min less_eq z1 z2" by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

379 
from z have zz1: "z \<sqsubset> z1" and zz2: "z \<sqsubset> z2" by simp_all 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

380 
{fix x assume H: "x \<sqsubset> z" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

381 
from less_trans[OF H zz1] less_trans[OF H zz2] 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

382 
have "(P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2')" using z1 zz1 z2 zz2 by auto 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

383 
} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

384 
thus ?thesis by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

385 
qed 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

386 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

387 
lemma minf_disj[no_atp]: 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

388 
assumes ex1: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

389 
and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

390 
shows "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

391 
proof 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

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 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

393 
from lt_ex obtain z where z:"z \<sqsubset> ord.min less_eq z1 z2" by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

394 
from z have zz1: "z \<sqsubset> z1" and zz2: "z \<sqsubset> z2" by simp_all 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

395 
{fix x assume H: "x \<sqsubset> z" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

396 
from less_trans[OF H zz1] less_trans[OF H zz2] 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

397 
have "(P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2')" using z1 zz1 z2 zz2 by auto 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

398 
} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

399 
thus ?thesis by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

400 
qed 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

401 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

402 
lemma minf_ex[no_atp]: assumes ex:"\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x" 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

403 
proof 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

404 
from ex obtain z where z: "\<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

405 
from lt_ex obtain x where x: "x \<sqsubset> z" by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

406 
from z x p1 show ?thesis by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

407 
qed 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

408 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

409 
end 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

410 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

411 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34974
diff
changeset

412 
locale constr_dense_linorder = linorder_no_lb + linorder_no_ub + 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

413 
fixes between 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

414 
assumes between_less: "less x y \<Longrightarrow> less x (between x y) \<and> less (between x y) y" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

415 
and between_same: "between x x = x" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

416 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34974
diff
changeset

417 
sublocale constr_dense_linorder < dense_linorder 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

418 
apply unfold_locales 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

419 
using gt_ex lt_ex between_less 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

420 
by (auto, rule_tac x="between x y" in exI, simp) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

421 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34974
diff
changeset

422 
context constr_dense_linorder 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

423 
begin 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

424 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

425 
lemma rinf_U[no_atp]: 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

426 
assumes fU: "finite U" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

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 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

428 
\<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P y )" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

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')" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

430 
and nmi: "\<not> MP" and npi: "\<not> PP" and ex: "\<exists> x. P x" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

431 
shows "\<exists> u\<in> U. \<exists> u' \<in> U. P (between u u')" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

432 
proof 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

433 
from ex obtain x where px: "P x" by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

434 
from px nmi npi nmpiU have "\<exists> u\<in> U. \<exists> u' \<in> U. u \<sqsubseteq> x \<and> x \<sqsubseteq> u'" by auto 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

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 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

436 
from uU have Une: "U \<noteq> {}" by auto 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

437 
term "linorder.Min less_eq" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

438 
let ?l = "linorder.Min less_eq U" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

439 
let ?u = "linorder.Max less_eq U" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

440 
have linM: "?l \<in> U" using fU Une by simp 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

441 
have uinM: "?u \<in> U" using fU Une by simp 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

442 
have lM: "\<forall> t\<in> U. ?l \<sqsubseteq> t" using Une fU by auto 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

443 
have Mu: "\<forall> t\<in> U. t \<sqsubseteq> ?u" using Une fU by auto 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

444 
have th:"?l \<sqsubseteq> u" using uU Une lM by auto 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

445 
from order_trans[OF th ux] have lx: "?l \<sqsubseteq> x" . 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

446 
have th: "u' \<sqsubseteq> ?u" using uU' Une Mu by simp 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

447 
from order_trans[OF xu' th] have xu: "x \<sqsubseteq> ?u" . 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

448 
from finite_set_intervals2[where P="P",OF px lx xu linM uinM fU lM Mu] 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

449 
have "(\<exists> s\<in> U. P s) \<or> 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

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)" . 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

451 
moreover { fix u assume um: "u\<in>U" and pu: "P u" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

452 
have "between u u = u" by (simp add: between_same) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

453 
with um pu have "P (between u u)" by simp 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

454 
with um have ?thesis by blast} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

455 
moreover{ 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

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" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

457 
then obtain t1 and t2 where t1M: "t1 \<in> U" and t2M: "t2\<in> U" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

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" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

459 
by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

460 
from less_trans[OF t1x xt2] have t1t2: "t1 \<sqsubset> t2" . 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

461 
let ?u = "between t1 t2" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

462 
from between_less t1t2 have t1lu: "t1 \<sqsubset> ?u" and ut2: "?u \<sqsubset> t2" by auto 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

463 
from lin_dense noM t1x xt2 px t1lu ut2 have "P ?u" by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

464 
with t1M t2M have ?thesis by blast} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

465 
ultimately show ?thesis by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

466 
qed 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

467 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

468 
theorem fr_eq[no_atp]: 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

469 
assumes fU: "finite U" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

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 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

471 
\<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P y )" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

472 
and nmibnd: "\<forall>x. \<not> MP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<sqsubseteq> x)" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

473 
and npibnd: "\<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. x \<sqsubseteq> u)" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

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)" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

475 
shows "(\<exists> x. P x) \<equiv> (MP \<or> PP \<or> (\<exists> u \<in> U. \<exists> u'\<in> U. P (between u u')))" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

476 
(is "_ \<equiv> (_ \<or> _ \<or> ?F)" is "?E \<equiv> ?D") 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

477 
proof 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

478 
{ 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

479 
assume px: "\<exists> x. P x" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

480 
have "MP \<or> PP \<or> (\<not> MP \<and> \<not> PP)" by blast 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

481 
moreover {assume "MP \<or> PP" hence "?D" by blast} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

482 
moreover {assume nmi: "\<not> MP" and npi: "\<not> PP" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

483 
from npmibnd[OF nmibnd npibnd] 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

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')" . 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

485 
from rinf_U[OF fU lin_dense nmpiU nmi npi px] have "?D" by blast} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

486 
ultimately have "?D" by blast} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

487 
moreover 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

488 
{ assume "?D" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

489 
moreover {assume m:"MP" from minf_ex[OF mi m] have "?E" .} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

490 
moreover {assume p: "PP" from pinf_ex[OF pi p] have "?E" . } 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

491 
moreover {assume f:"?F" hence "?E" by blast} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

492 
ultimately have "?E" by blast} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

493 
ultimately have "?E = ?D" by blast thus "?E \<equiv> ?D" by simp 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

494 
qed 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

495 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

496 
lemmas minf_thms[no_atp] = minf_conj minf_disj minf_eq minf_neq minf_lt minf_le minf_gt minf_ge minf_P 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

497 
lemmas pinf_thms[no_atp] = pinf_conj pinf_disj pinf_eq pinf_neq pinf_lt pinf_le pinf_gt pinf_ge pinf_P 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

498 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

499 
lemmas nmi_thms[no_atp] = nmi_conj nmi_disj nmi_eq nmi_neq nmi_lt nmi_le nmi_gt nmi_ge nmi_P 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

500 
lemmas npi_thms[no_atp] = npi_conj npi_disj npi_eq npi_neq npi_lt npi_le npi_gt npi_ge npi_P 
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

501 
lemmas lin_dense_thms[no_atp] = 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 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

502 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

503 
lemma ferrack_axiom[no_atp]: "constr_dense_linorder less_eq less between" 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34974
diff
changeset

504 
by (rule constr_dense_linorder_axioms) 
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35267
diff
changeset

505 
lemma atoms[no_atp]: 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

506 
shows "TERM (less :: 'a \<Rightarrow> _)" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

507 
and "TERM (less_eq :: 'a \<Rightarrow> _)" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

508 
and "TERM (op = :: 'a \<Rightarrow> _)" . 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

509 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

510 
declare ferrack_axiom [ferrack minf: minf_thms pinf: pinf_thms 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

511 
nmi: nmi_thms npi: npi_thms lindense: 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

512 
lin_dense_thms qe: fr_eq atoms: atoms] 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

513 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

514 
declaration {* 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

515 
let 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

516 
fun simps phi = map (Morphism.thm phi) [@{thm "not_less"}, @{thm "not_le"}] 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

517 
fun generic_whatis phi = 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

518 
let 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

519 
val [lt, le] = map (Morphism.term phi) [@{term "op \<sqsubset>"}, @{term "op \<sqsubseteq>"}] 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

520 
fun h x t = 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

521 
case term_of t of 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

522 
Const("op =", _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

523 
else Ferrante_Rackoff_Data.Nox 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

524 
 @{term "Not"}$(Const("op =", _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

525 
else Ferrante_Rackoff_Data.Nox 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

526 
 b$y$z => if Term.could_unify (b, lt) then 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

527 
if term_of x aconv y then Ferrante_Rackoff_Data.Lt 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

528 
else if term_of x aconv z then Ferrante_Rackoff_Data.Gt 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

529 
else Ferrante_Rackoff_Data.Nox 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

530 
else if Term.could_unify (b, le) then 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

531 
if term_of x aconv y then Ferrante_Rackoff_Data.Le 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

532 
else if term_of x aconv z then Ferrante_Rackoff_Data.Ge 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

533 
else Ferrante_Rackoff_Data.Nox 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

534 
else Ferrante_Rackoff_Data.Nox 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

535 
 _ => Ferrante_Rackoff_Data.Nox 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

536 
in h end 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

537 
fun ss phi = HOL_ss addsimps (simps phi) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

538 
in 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

539 
Ferrante_Rackoff_Data.funs @{thm "ferrack_axiom"} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

540 
{isolate_conv = K (K (K Thm.reflexive)), whatis = generic_whatis, simpset = ss} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

541 
end 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

542 
*} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

543 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

544 
end 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

545 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

546 
use "~~/src/HOL/Tools/Qelim/ferrante_rackoff.ML" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

547 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

548 
method_setup ferrack = {* 
30549  549 
Scan.succeed (SIMPLE_METHOD' o FerranteRackoff.dlo_tac) 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

550 
*} "Ferrante and Rackoff's algorithm for quantifier elimination in dense linear orders" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

551 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

552 
subsection {* Ferrante and Rackoff algorithm over ordered fields *} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

553 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34974
diff
changeset

554 
lemma neg_prod_lt:"(c\<Colon>'a\<Colon>linordered_field) < 0 \<Longrightarrow> ((c*x < 0) == (x > 0))" 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

555 
proof 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

556 
assume H: "c < 0" 
29667  557 
have "c*x < 0 = (0/c < x)" by (simp only: neg_divide_less_eq[OF H] algebra_simps) 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

558 
also have "\<dots> = (0 < x)" by simp 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

559 
finally show "(c*x < 0) == (x > 0)" by simp 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

560 
qed 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

561 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34974
diff
changeset

562 
lemma pos_prod_lt:"(c\<Colon>'a\<Colon>linordered_field) > 0 \<Longrightarrow> ((c*x < 0) == (x < 0))" 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

563 
proof 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

564 
assume H: "c > 0" 
29667  565 
hence "c*x < 0 = (0/c > x)" by (simp only: pos_less_divide_eq[OF H] algebra_simps) 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

566 
also have "\<dots> = (0 > x)" by simp 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

567 
finally show "(c*x < 0) == (x < 0)" by simp 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

568 
qed 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

569 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34974
diff
changeset

570 
lemma neg_prod_sum_lt: "(c\<Colon>'a\<Colon>linordered_field) < 0 \<Longrightarrow> ((c*x + t< 0) == (x > ( 1/c)*t))" 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

571 
proof 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

572 
assume H: "c < 0" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

573 
have "c*x + t< 0 = (c*x < t)" by (subst less_iff_diff_less_0 [of "c*x" "t"], simp) 
29667  574 
also have "\<dots> = (t/c < x)" by (simp only: neg_divide_less_eq[OF H] algebra_simps) 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

575 
also have "\<dots> = (( 1/c)*t < x)" by simp 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

576 
finally show "(c*x + t < 0) == (x > ( 1/c)*t)" by simp 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

577 
qed 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

578 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34974
diff
changeset

579 
lemma pos_prod_sum_lt:"(c\<Colon>'a\<Colon>linordered_field) > 0 \<Longrightarrow> ((c*x + t < 0) == (x < ( 1/c)*t))" 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

580 
proof 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

581 
assume H: "c > 0" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

582 
have "c*x + t< 0 = (c*x < t)" by (subst less_iff_diff_less_0 [of "c*x" "t"], simp) 
29667  583 
also have "\<dots> = (t/c > x)" by (simp only: pos_less_divide_eq[OF H] algebra_simps) 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

584 
also have "\<dots> = (( 1/c)*t > x)" by simp 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

585 
finally show "(c*x + t < 0) == (x < ( 1/c)*t)" by simp 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

586 
qed 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

587 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34974
diff
changeset

588 
lemma sum_lt:"((x::'a::ordered_ab_group_add) + t < 0) == (x <  t)" 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

589 
using less_diff_eq[where a= x and b=t and c=0] by simp 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

590 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34974
diff
changeset

591 
lemma neg_prod_le:"(c\<Colon>'a\<Colon>linordered_field) < 0 \<Longrightarrow> ((c*x <= 0) == (x >= 0))" 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

592 
proof 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

593 
assume H: "c < 0" 
29667  594 
have "c*x <= 0 = (0/c <= x)" by (simp only: neg_divide_le_eq[OF H] algebra_simps) 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

595 
also have "\<dots> = (0 <= x)" by simp 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

596 
finally show "(c*x <= 0) == (x >= 0)" by simp 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

597 
qed 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

598 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34974
diff
changeset

599 
lemma pos_prod_le:"(c\<Colon>'a\<Colon>linordered_field) > 0 \<Longrightarrow> ((c*x <= 0) == (x <= 0))" 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

600 
proof 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

601 
assume H: "c > 0" 
29667  602 
hence "c*x <= 0 = (0/c >= x)" by (simp only: pos_le_divide_eq[OF H] algebra_simps) 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

603 
also have "\<dots> = (0 >= x)" by simp 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

604 
finally show "(c*x <= 0) == (x <= 0)" by simp 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

605 
qed 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

606 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34974
diff
changeset

607 
lemma neg_prod_sum_le: "(c\<Colon>'a\<Colon>linordered_field) < 0 \<Longrightarrow> ((c*x + t <= 0) == (x >= ( 1/c)*t))" 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

608 
proof 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

609 
assume H: "c < 0" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

610 
have "c*x + t <= 0 = (c*x <= t)" by (subst le_iff_diff_le_0 [of "c*x" "t"], simp) 
29667  611 
also have "\<dots> = (t/c <= x)" by (simp only: neg_divide_le_eq[OF H] algebra_simps) 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

612 
also have "\<dots> = (( 1/c)*t <= x)" by simp 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

613 
finally show "(c*x + t <= 0) == (x >= ( 1/c)*t)" by simp 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

614 
qed 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

615 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34974
diff
changeset

616 
lemma pos_prod_sum_le:"(c\<Colon>'a\<Colon>linordered_field) > 0 \<Longrightarrow> ((c*x + t <= 0) == (x <= ( 1/c)*t))" 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

617 
proof 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

618 
assume H: "c > 0" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

619 
have "c*x + t <= 0 = (c*x <= t)" by (subst le_iff_diff_le_0 [of "c*x" "t"], simp) 
29667  620 
also have "\<dots> = (t/c >= x)" by (simp only: pos_le_divide_eq[OF H] algebra_simps) 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

621 
also have "\<dots> = (( 1/c)*t >= x)" by simp 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

622 
finally show "(c*x + t <= 0) == (x <= ( 1/c)*t)" by simp 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

623 
qed 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

624 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34974
diff
changeset

625 
lemma sum_le:"((x::'a::ordered_ab_group_add) + t <= 0) == (x <=  t)" 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

626 
using le_diff_eq[where a= x and b=t and c=0] by simp 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

627 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34974
diff
changeset

628 
lemma nz_prod_eq:"(c\<Colon>'a\<Colon>linordered_field) \<noteq> 0 \<Longrightarrow> ((c*x = 0) == (x = 0))" by simp 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34974
diff
changeset

629 
lemma nz_prod_sum_eq: "(c\<Colon>'a\<Colon>linordered_field) \<noteq> 0 \<Longrightarrow> ((c*x + t = 0) == (x = ( 1/c)*t))" 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

630 
proof 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

631 
assume H: "c \<noteq> 0" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

632 
have "c*x + t = 0 = (c*x = t)" by (subst eq_iff_diff_eq_0 [of "c*x" "t"], simp) 
29667  633 
also have "\<dots> = (x = t/c)" by (simp only: nonzero_eq_divide_eq[OF H] algebra_simps) 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

634 
finally show "(c*x + t = 0) == (x = ( 1/c)*t)" by simp 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

635 
qed 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34974
diff
changeset

636 
lemma sum_eq:"((x::'a::ordered_ab_group_add) + t = 0) == (x =  t)" 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

637 
using eq_diff_eq[where a= x and b=t and c=0] by simp 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

638 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

639 

35043
07dbdf60d5ad
dropped accidental duplication of "lin" prefix from cs. 108662d50512
haftmann
parents:
35028
diff
changeset

640 
interpretation class_dense_linordered_field: constr_dense_linorder 
29509
1ff0f3f08a7b
migrated class package to new locale implementation
haftmann
parents:
29252
diff
changeset

641 
"op <=" "op <" 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34974
diff
changeset

642 
"\<lambda> x y. 1/2 * ((x::'a::{linordered_field,number_ring}) + y)" 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

643 
proof (unfold_locales, dlo, dlo, auto) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

644 
fix x y::'a assume lt: "x < y" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

645 
from less_half_sum[OF lt] show "x < (x + y) /2" by simp 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

646 
next 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

647 
fix x y::'a assume lt: "x < y" 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

648 
from gt_half_sum[OF lt] show "(x + y) /2 < y" by simp 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

649 
qed 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

650 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

651 
declaration{* 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

652 
let 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

653 
fun earlier [] x y = false 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

654 
 earlier (h::t) x y = 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

655 
if h aconvc y then false else if h aconvc x then true else earlier t x y; 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

656 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

657 
fun dest_frac ct = case term_of ct of 
35084  658 
Const (@{const_name Rings.divide},_) $ a $ b=> 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

659 
Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b)) 
30868  660 
 Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a > snd) 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

661 
 t => Rat.rat_of_int (snd (HOLogic.dest_number t)) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

662 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

663 
fun mk_frac phi cT x = 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

664 
let val (a, b) = Rat.quotient_of_rat x 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

665 
in if b = 1 then Numeral.mk_cnumber cT a 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

666 
else Thm.capply 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

667 
(Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"}) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

668 
(Numeral.mk_cnumber cT a)) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

669 
(Numeral.mk_cnumber cT b) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

670 
end 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

671 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

672 
fun whatis x ct = case term_of ct of 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

673 
Const(@{const_name Groups.plus}, _)$(Const(@{const_name Groups.times},_)$_$y)$_ => 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

674 
if y aconv term_of x then ("c*x+t",[(funpow 2 Thm.dest_arg1) ct, Thm.dest_arg ct]) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

675 
else ("Nox",[]) 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

676 
 Const(@{const_name Groups.plus}, _)$y$_ => 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

677 
if y aconv term_of x then ("x+t",[Thm.dest_arg ct]) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

678 
else ("Nox",[]) 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

679 
 Const(@{const_name Groups.times}, _)$_$y => 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

680 
if y aconv term_of x then ("c*x",[Thm.dest_arg1 ct]) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

681 
else ("Nox",[]) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

682 
 t => if t aconv term_of x then ("x",[]) else ("Nox",[]); 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

683 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

684 
fun xnormalize_conv ctxt [] ct = reflexive ct 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

685 
 xnormalize_conv ctxt (vs as (x::_)) ct = 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

686 
case term_of ct of 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

687 
Const(@{const_name Orderings.less},_)$_$Const(@{const_name Groups.zero},_) => 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

688 
(case whatis x (Thm.dest_arg1 ct) of 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

689 
("c*x+t",[c,t]) => 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

690 
let 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

691 
val cr = dest_frac c 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

692 
val clt = Thm.dest_fun2 ct 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

693 
val cz = Thm.dest_arg ct 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

694 
val neg = cr </ Rat.zero 
32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
31021
diff
changeset

695 
val cthp = Simplifier.rewrite (simpset_of ctxt) 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

696 
(Thm.capply @{cterm "Trueprop"} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

697 
(if neg then Thm.capply (Thm.capply clt c) cz 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

698 
else Thm.capply (Thm.capply clt cz) c)) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

699 
val cth = equal_elim (symmetric cthp) TrueI 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

700 
val th = implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x,t]) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

701 
(if neg then @{thm neg_prod_sum_lt} else @{thm pos_prod_sum_lt})) cth 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

702 
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

703 
(Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

704 
in rth end 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

705 
 ("x+t",[t]) => 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

706 
let 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

707 
val T = ctyp_of_term x 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

708 
val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_lt"} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

709 
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

710 
(Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

711 
in rth end 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

712 
 ("c*x",[c]) => 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

713 
let 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

714 
val cr = dest_frac c 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

715 
val clt = Thm.dest_fun2 ct 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

716 
val cz = Thm.dest_arg ct 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

717 
val neg = cr </ Rat.zero 
32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
31021
diff
changeset

718 
val cthp = Simplifier.rewrite (simpset_of ctxt) 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

719 
(Thm.capply @{cterm "Trueprop"} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

720 
(if neg then Thm.capply (Thm.capply clt c) cz 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

721 
else Thm.capply (Thm.capply clt cz) c)) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

722 
val cth = equal_elim (symmetric cthp) TrueI 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

723 
val th = implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x]) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

724 
(if neg then @{thm neg_prod_lt} else @{thm pos_prod_lt})) cth 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

725 
val rth = th 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

726 
in rth end 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

727 
 _ => reflexive ct) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

728 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

729 

35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

730 
 Const(@{const_name Orderings.less_eq},_)$_$Const(@{const_name Groups.zero},_) => 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

731 
(case whatis x (Thm.dest_arg1 ct) of 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

732 
("c*x+t",[c,t]) => 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

733 
let 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

734 
val T = ctyp_of_term x 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

735 
val cr = dest_frac c 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

736 
val clt = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "op <"} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

737 
val cz = Thm.dest_arg ct 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

738 
val neg = cr </ Rat.zero 
32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
31021
diff
changeset

739 
val cthp = Simplifier.rewrite (simpset_of ctxt) 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

740 
(Thm.capply @{cterm "Trueprop"} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

741 
(if neg then Thm.capply (Thm.capply clt c) cz 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

742 
else Thm.capply (Thm.capply clt cz) c)) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

743 
val cth = equal_elim (symmetric cthp) TrueI 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

744 
val th = implies_elim (instantiate' [SOME T] (map SOME [c,x,t]) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

745 
(if neg then @{thm neg_prod_sum_le} else @{thm pos_prod_sum_le})) cth 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

746 
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

747 
(Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

748 
in rth end 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

749 
 ("x+t",[t]) => 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

750 
let 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

751 
val T = ctyp_of_term x 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

752 
val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_le"} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

753 
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

754 
(Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

755 
in rth end 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

756 
 ("c*x",[c]) => 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

757 
let 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

758 
val T = ctyp_of_term x 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

759 
val cr = dest_frac c 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

760 
val clt = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "op <"} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

761 
val cz = Thm.dest_arg ct 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

762 
val neg = cr </ Rat.zero 
32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
31021
diff
changeset

763 
val cthp = Simplifier.rewrite (simpset_of ctxt) 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

764 
(Thm.capply @{cterm "Trueprop"} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

765 
(if neg then Thm.capply (Thm.capply clt c) cz 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

766 
else Thm.capply (Thm.capply clt cz) c)) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

767 
val cth = equal_elim (symmetric cthp) TrueI 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

768 
val th = implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x]) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

769 
(if neg then @{thm neg_prod_le} else @{thm pos_prod_le})) cth 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

770 
val rth = th 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

771 
in rth end 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

772 
 _ => reflexive ct) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

773 

35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

774 
 Const("op =",_)$_$Const(@{const_name Groups.zero},_) => 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

775 
(case whatis x (Thm.dest_arg1 ct) of 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

776 
("c*x+t",[c,t]) => 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

777 
let 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

778 
val T = ctyp_of_term x 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

779 
val cr = dest_frac c 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

780 
val ceq = Thm.dest_fun2 ct 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

781 
val cz = Thm.dest_arg ct 
32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
31021
diff
changeset

782 
val cthp = Simplifier.rewrite (simpset_of ctxt) 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

783 
(Thm.capply @{cterm "Trueprop"} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

784 
(Thm.capply @{cterm "Not"} (Thm.capply (Thm.capply ceq c) cz))) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

785 
val cth = equal_elim (symmetric cthp) TrueI 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

786 
val th = implies_elim 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

787 
(instantiate' [SOME T] (map SOME [c,x,t]) @{thm nz_prod_sum_eq}) cth 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

788 
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

789 
(Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

790 
in rth end 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

791 
 ("x+t",[t]) => 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

792 
let 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

793 
val T = ctyp_of_term x 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

794 
val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_eq"} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

795 
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

796 
(Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

797 
in rth end 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

798 
 ("c*x",[c]) => 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

799 
let 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

800 
val T = ctyp_of_term x 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

801 
val cr = dest_frac c 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

802 
val ceq = Thm.dest_fun2 ct 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

803 
val cz = Thm.dest_arg ct 
32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
31021
diff
changeset

804 
val cthp = Simplifier.rewrite (simpset_of ctxt) 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

805 
(Thm.capply @{cterm "Trueprop"} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

806 
(Thm.capply @{cterm "Not"} (Thm.capply (Thm.capply ceq c) cz))) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

807 
val cth = equal_elim (symmetric cthp) TrueI 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

808 
val rth = implies_elim 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

809 
(instantiate' [SOME T] (map SOME [c,x]) @{thm nz_prod_eq}) cth 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

810 
in rth end 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

811 
 _ => reflexive ct); 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

812 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

813 
local 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

814 
val less_iff_diff_less_0 = mk_meta_eq @{thm "less_iff_diff_less_0"} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

815 
val le_iff_diff_le_0 = mk_meta_eq @{thm "le_iff_diff_le_0"} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

816 
val eq_iff_diff_eq_0 = mk_meta_eq @{thm "eq_iff_diff_eq_0"} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

817 
in 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

818 
fun field_isolate_conv phi ctxt vs ct = case term_of ct of 
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35084
diff
changeset

819 
Const(@{const_name Orderings.less},_)$a$b => 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

820 
let val (ca,cb) = Thm.dest_binop ct 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

821 
val T = ctyp_of_term ca 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

822 
val th = instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

823 
val nth = Conv.fconv_rule 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

824 
(Conv.arg_conv (Conv.arg1_conv 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

825 
(Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

826 
val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth)) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

827 
in rth end 
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35084
diff
changeset

828 
 Const(@{const_name Orderings.less_eq},_)$a$b => 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

829 
let val (ca,cb) = Thm.dest_binop ct 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

830 
val T = ctyp_of_term ca 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

831 
val th = instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

832 
val nth = Conv.fconv_rule 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

833 
(Conv.arg_conv (Conv.arg1_conv 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

834 
(Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

835 
val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth)) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

836 
in rth end 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

837 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

838 
 Const("op =",_)$a$b => 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

839 
let val (ca,cb) = Thm.dest_binop ct 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

840 
val T = ctyp_of_term ca 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

841 
val th = instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

842 
val nth = Conv.fconv_rule 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

843 
(Conv.arg_conv (Conv.arg1_conv 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

844 
(Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

845 
val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth)) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

846 
in rth end 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

847 
 @{term "Not"} $(Const("op =",_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

848 
 _ => reflexive ct 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

849 
end; 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

850 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

851 
fun classfield_whatis phi = 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

852 
let 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

853 
fun h x t = 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

854 
case term_of t of 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

855 
Const("op =", _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

856 
else Ferrante_Rackoff_Data.Nox 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

857 
 @{term "Not"}$(Const("op =", _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

858 
else Ferrante_Rackoff_Data.Nox 
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35084
diff
changeset

859 
 Const(@{const_name Orderings.less},_)$y$z => 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

860 
if term_of x aconv y then Ferrante_Rackoff_Data.Lt 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

861 
else if term_of x aconv z then Ferrante_Rackoff_Data.Gt 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

862 
else Ferrante_Rackoff_Data.Nox 
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35084
diff
changeset

863 
 Const (@{const_name Orderings.less_eq},_)$y$z => 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

864 
if term_of x aconv y then Ferrante_Rackoff_Data.Le 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

865 
else if term_of x aconv z then Ferrante_Rackoff_Data.Ge 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

866 
else Ferrante_Rackoff_Data.Nox 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

867 
 _ => Ferrante_Rackoff_Data.Nox 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

868 
in h end; 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

869 
fun class_field_ss phi = 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

870 
HOL_basic_ss addsimps ([@{thm "linorder_not_less"}, @{thm "linorder_not_le"}]) 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

871 
addsplits [@{thm "abs_split"},@{thm "split_max"}, @{thm "split_min"}] 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

872 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

873 
in 
35043
07dbdf60d5ad
dropped accidental duplication of "lin" prefix from cs. 108662d50512
haftmann
parents:
35028
diff
changeset

874 
Ferrante_Rackoff_Data.funs @{thm "class_dense_linordered_field.ferrack_axiom"} 
26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

875 
{isolate_conv = field_isolate_conv, whatis = classfield_whatis, simpset = class_field_ss} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

876 
end 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

877 
*} 
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

878 

29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

879 
lemma upper_bound_finite_set: 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

880 
assumes fS: "finite S" 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

881 
shows "\<exists>(a::'a::linorder). \<forall>x \<in> S. f x \<le> a" 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

882 
proof(induct rule: finite_induct[OF fS]) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

883 
case 1 thus ?case by simp 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

884 
next 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

885 
case (2 x F) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

886 
from "2.hyps" obtain a where a:"\<forall>x \<in>F. f x \<le> a" by blast 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

887 
let ?a = "max a (f x)" 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

888 
have m: "a \<le> ?a" "f x \<le> ?a" by simp_all 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

889 
{fix y assume y: "y \<in> insert x F" 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

890 
{assume "y = x" hence "f y \<le> ?a" using m by simp} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

891 
moreover 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

892 
{assume yF: "y\<in> F" from a[rule_format, OF yF] m have "f y \<le> ?a" by (simp add: max_def)} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

893 
ultimately have "f y \<le> ?a" using y by blast} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

894 
then show ?case by blast 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

895 
qed 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

896 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

897 
lemma lower_bound_finite_set: 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

898 
assumes fS: "finite S" 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

899 
shows "\<exists>(a::'a::linorder). \<forall>x \<in> S. f x \<ge> a" 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

900 
proof(induct rule: finite_induct[OF fS]) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

901 
case 1 thus ?case by simp 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

902 
next 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

903 
case (2 x F) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

904 
from "2.hyps" obtain a where a:"\<forall>x \<in>F. f x \<ge> a" by blast 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

905 
let ?a = "min a (f x)" 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

906 
have m: "a \<ge> ?a" "f x \<ge> ?a" by simp_all 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

907 
{fix y assume y: "y \<in> insert x F" 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

908 
{assume "y = x" hence "f y \<ge> ?a" using m by simp} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

909 
moreover 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

910 
{assume yF: "y\<in> F" from a[rule_format, OF yF] m have "f y \<ge> ?a" by (simp add: min_def)} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

911 
ultimately have "f y \<ge> ?a" using y by blast} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

912 
then show ?case by blast 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

913 
qed 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

914 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

915 
lemma bound_finite_set: assumes f: "finite S" 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

916 
shows "\<exists>a. \<forall>x \<in>S. (f x:: 'a::linorder) \<le> a" 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

917 
proof 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

918 
let ?F = "f ` S" 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

919 
from f have fF: "finite ?F" by simp 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

920 
let ?a = "Max ?F" 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

921 
{assume "S = {}" hence ?thesis by blast} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

922 
moreover 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

923 
{assume Se: "S \<noteq> {}" hence Fe: "?F \<noteq> {}" by simp 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

924 
{fix x assume x: "x \<in> S" 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

925 
hence th0: "f x \<in> ?F" by simp 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

926 
hence "f x \<le> ?a" using Max_ge[OF fF th0] ..} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

927 
hence ?thesis by blast} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

928 
ultimately show ?thesis by blast 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

929 
qed 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

930 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
29823
diff
changeset

931 

26161
34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

932 

34cb0b457dcc
Old HOL/Dense_Linear_Order.thy and the setup in Arith_Tools for Ferrante and Rackoff's Quantifier elimination for linear arithmetic over ordered Fields.
chaieb
parents:
diff
changeset

933 
end 