# HG changeset patch
# User haftmann
# Date 1187957658 -7200
# Node ID c0b5ff9e9e4dea813ed1319424cab92ef76f91cc
# Parent  acfb2413faa39522df841ef1c9fea129b828cd69
moved class dense_linear_order to Orderings.thy

diff -r acfb2413faa3 -r c0b5ff9e9e4d NEWS
--- a/NEWS	Fri Aug 24 14:14:17 2007 +0200
+++ b/NEWS	Fri Aug 24 14:14:18 2007 +0200
@@ -635,6 +635,9 @@
 
 *** HOL ***
 
+* Formulation of theorem "dense" changed slightly due to integration with new
+class dense_linear_order.
+
 * theory Finite_Set: "name-space" locales Lattice, Distrib_lattice, Linorder etc.
 have disappeared; operations defined in terms of fold_set now are named
 Inf_fin, Sup_fin.  INCOMPATIBILITY.
diff -r acfb2413faa3 -r c0b5ff9e9e4d src/HOL/Dense_Linear_Order.thy
--- a/src/HOL/Dense_Linear_Order.thy	Fri Aug 24 14:14:17 2007 +0200
+++ b/src/HOL/Dense_Linear_Order.thy	Fri Aug 24 14:14:18 2007 +0200
@@ -211,10 +211,7 @@
 
 section {* The classical QE after Langford for dense linear orders *}
 
-class dense_linear_order = linorder + 
-  assumes gt_ex: "\<exists>y. x \<sqsubset> y" 
-  and lt_ex: "\<exists>y. y \<sqsubset> x"
-  and dense: "x \<sqsubset> y \<Longrightarrow> (\<exists>z. x \<sqsubset> z \<and> z \<sqsubset> y)"
+context dense_linear_order
 begin
 
 lemma dlo_qe_bnds: 
@@ -304,21 +301,9 @@
   Method.ctxt_args (Method.SIMPLE_METHOD' o LangfordQE.dlo_tac)
 *} "Langford's algorithm for quantifier elimination in dense linear orders"
 
-interpretation dlo_ordring_class: dense_linear_order ["op \<le> \<Colon> 'a\<Colon>ordered_field \<Rightarrow> _" "op <"]
-apply unfold_locales
-apply (rule_tac x = "x + 1" in exI, simp)
-apply (rule_tac x = "x - 1" in exI, simp)
-apply (rule_tac x = "(x + y) / (1 + 1)" in exI)
-apply (rule conjI)
-apply (rule less_half_sum, simp)
-apply (rule gt_half_sum, simp)
-done
-
 
 section {* Contructive dense linear orders yield QE for linear arithmetic over ordered Fields -- see @{text "Arith_Tools.thy"} *}
 
-
-
 text {* Linear order without upper bounds *}
 
 class linorder_no_ub = linorder +
@@ -428,6 +413,10 @@
   apply unfold_locales
   using gt_ex lt_ex between_less
     by (auto, rule_tac x="between x y" in exI, simp)
+(*FIXME*)
+lemmas gt_ex = dense_linear_order_class.less_eq_less.gt_ex
+lemmas lt_ex = dense_linear_order_class.less_eq_less.lt_ex
+lemmas dense = dense_linear_order_class.less_eq_less.dense
 
 context constr_dense_linear_order
 begin
@@ -556,8 +545,4 @@
   Method.ctxt_args (Method.SIMPLE_METHOD' o FerranteRackoff.dlo_tac)
 *} "Ferrante and Rackoff's algorithm for quantifier elimination in dense linear orders"
 
-
-(*FIXME: synchronize dense orders with existing algebra*)
-lemmas dense = Ring_and_Field.dense
-
 end 
diff -r acfb2413faa3 -r c0b5ff9e9e4d src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Fri Aug 24 14:14:17 2007 +0200
+++ b/src/HOL/Orderings.thy	Fri Aug 24 14:14:18 2007 +0200
@@ -236,53 +236,6 @@
 end
 
 
-subsection {* Name duplicates *}
-
-lemmas order_less_le = less_le
-lemmas order_eq_refl = order_class.eq_refl
-lemmas order_less_irrefl = order_class.less_irrefl
-lemmas order_le_less = order_class.le_less
-lemmas order_le_imp_less_or_eq = order_class.le_imp_less_or_eq
-lemmas order_less_imp_le = order_class.less_imp_le
-lemmas order_less_imp_not_eq = order_class.less_imp_not_eq
-lemmas order_less_imp_not_eq2 = order_class.less_imp_not_eq2
-lemmas order_neq_le_trans = order_class.neq_le_trans
-lemmas order_le_neq_trans = order_class.le_neq_trans
-
-lemmas order_antisym = antisym
-lemmas order_less_not_sym = order_class.less_not_sym
-lemmas order_less_asym = order_class.less_asym
-lemmas order_eq_iff = order_class.eq_iff
-lemmas order_antisym_conv = order_class.antisym_conv
-lemmas order_less_trans = order_class.less_trans
-lemmas order_le_less_trans = order_class.le_less_trans
-lemmas order_less_le_trans = order_class.less_le_trans
-lemmas order_less_imp_not_less = order_class.less_imp_not_less
-lemmas order_less_imp_triv = order_class.less_imp_triv
-lemmas order_less_asym' = order_class.less_asym'
-
-lemmas linorder_linear = linear
-lemmas linorder_less_linear = linorder_class.less_linear
-lemmas linorder_le_less_linear = linorder_class.le_less_linear
-lemmas linorder_le_cases = linorder_class.le_cases
-lemmas linorder_not_less = linorder_class.not_less
-lemmas linorder_not_le = linorder_class.not_le
-lemmas linorder_neq_iff = linorder_class.neq_iff
-lemmas linorder_neqE = linorder_class.neqE
-lemmas linorder_antisym_conv1 = linorder_class.antisym_conv1
-lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
-lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
-
-lemmas min_le_iff_disj = linorder_class.min_le_iff_disj
-lemmas le_max_iff_disj = linorder_class.le_max_iff_disj
-lemmas min_less_iff_disj = linorder_class.min_less_iff_disj
-lemmas less_max_iff_disj = linorder_class.less_max_iff_disj
-lemmas min_less_iff_conj [simp] = linorder_class.min_less_iff_conj
-lemmas max_less_iff_conj [simp] = linorder_class.max_less_iff_conj
-lemmas split_min = linorder_class.split_min
-lemmas split_max = linorder_class.split_max
-
-
 subsection {* Reasoning tools setup *}
 
 ML {*
@@ -336,25 +289,25 @@
 
 structure Order_Tac = Order_Tac_Fun (
 struct
-  val less_reflE = thm "order_less_irrefl" RS thm "notE";
-  val le_refl = thm "order_refl";
-  val less_imp_le = thm "order_less_imp_le";
-  val not_lessI = thm "linorder_not_less" RS thm "iffD2";
-  val not_leI = thm "linorder_not_le" RS thm "iffD2";
-  val not_lessD = thm "linorder_not_less" RS thm "iffD1";
-  val not_leD = thm "linorder_not_le" RS thm "iffD1";
-  val eqI = thm "order_antisym";
-  val eqD1 = thm "order_eq_refl";
-  val eqD2 = thm "sym" RS thm "order_eq_refl";
-  val less_trans = thm "order_less_trans";
-  val less_le_trans = thm "order_less_le_trans";
-  val le_less_trans = thm "order_le_less_trans";
-  val le_trans = thm "order_trans";
-  val le_neq_trans = thm "order_le_neq_trans";
-  val neq_le_trans = thm "order_neq_le_trans";
-  val less_imp_neq = thm "less_imp_neq";
-  val eq_neq_eq_imp_neq = thm "eq_neq_eq_imp_neq";
-  val not_sym = thm "not_sym";
+  val less_reflE = @{thm less_irrefl} RS @{thm notE};
+  val le_refl = @{thm order_refl};
+  val less_imp_le = @{thm less_imp_le};
+  val not_lessI = @{thm not_less} RS @{thm iffD2};
+  val not_leI = @{thm not_le} RS @{thm iffD2};
+  val not_lessD = @{thm not_less} RS @{thm iffD1};
+  val not_leD = @{thm not_le} RS @{thm iffD1};
+  val eqI = @{thm antisym};
+  val eqD1 = @{thm eq_refl};
+  val eqD2 = @{thm sym} RS @{thm eq_refl};
+  val less_trans = @{thm less_trans};
+  val less_le_trans = @{thm less_le_trans};
+  val le_less_trans = @{thm le_less_trans};
+  val le_trans = @{thm order_trans};
+  val le_neq_trans = @{thm le_neq_trans};
+  val neq_le_trans = @{thm neq_le_trans};
+  val less_imp_neq = @{thm less_imp_neq};
+  val eq_neq_eq_imp_neq = @{thm eq_neq_eq_imp_neq};
+  val not_sym = @{thm not_sym};
   val decomp_part = decomp_gen ["Orderings.order"];
   val decomp_lin = decomp_gen ["Orderings.linorder"];
 end);
@@ -376,9 +329,9 @@
          let val t = HOLogic.mk_Trueprop(HOLogic.Not $ (less $ r $ s))
          in case find_first (prp t) prems of
               NONE => NONE
-            | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_antisym_conv1}))
+            | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv1}))
          end
-     | SOME thm => SOME(mk_meta_eq(thm RS @{thm order_antisym_conv}))
+     | SOME thm => SOME(mk_meta_eq(thm RS @{thm order_class.antisym_conv}))
   end
   handle THM _ => NONE;
 
@@ -391,9 +344,9 @@
          let val t = HOLogic.mk_Trueprop(NotC $ (less $ s $ r))
          in case find_first (prp t) prems of
               NONE => NONE
-            | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_antisym_conv3}))
+            | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv3}))
          end
-     | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_antisym_conv2}))
+     | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv2}))
   end
   handle THM _ => NONE;
 
@@ -420,6 +373,66 @@
 *}
 
 
+subsection {* Dense orders *}
+
+class dense_linear_order = linorder + 
+  assumes gt_ex: "\<exists>y. x \<sqsubset> y" 
+  and lt_ex: "\<exists>y. y \<sqsubset> x"
+  and dense: "x \<sqsubset> y \<Longrightarrow> (\<exists>z. x \<sqsubset> z \<and> z \<sqsubset> y)"
+  (*see further theory Dense_Linear_Order*)
+
+lemma interval_empty_iff:
+  fixes x y z :: "'a\<Colon>dense_linear_order"
+  shows "{y. x < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
+  by (auto dest: dense)
+
+subsection {* Name duplicates *}
+
+lemmas order_less_le = less_le
+lemmas order_eq_refl = order_class.eq_refl
+lemmas order_less_irrefl = order_class.less_irrefl
+lemmas order_le_less = order_class.le_less
+lemmas order_le_imp_less_or_eq = order_class.le_imp_less_or_eq
+lemmas order_less_imp_le = order_class.less_imp_le
+lemmas order_less_imp_not_eq = order_class.less_imp_not_eq
+lemmas order_less_imp_not_eq2 = order_class.less_imp_not_eq2
+lemmas order_neq_le_trans = order_class.neq_le_trans
+lemmas order_le_neq_trans = order_class.le_neq_trans
+
+lemmas order_antisym = antisym
+lemmas order_less_not_sym = order_class.less_not_sym
+lemmas order_less_asym = order_class.less_asym
+lemmas order_eq_iff = order_class.eq_iff
+lemmas order_antisym_conv = order_class.antisym_conv
+lemmas order_less_trans = order_class.less_trans
+lemmas order_le_less_trans = order_class.le_less_trans
+lemmas order_less_le_trans = order_class.less_le_trans
+lemmas order_less_imp_not_less = order_class.less_imp_not_less
+lemmas order_less_imp_triv = order_class.less_imp_triv
+lemmas order_less_asym' = order_class.less_asym'
+
+lemmas linorder_linear = linear
+lemmas linorder_less_linear = linorder_class.less_linear
+lemmas linorder_le_less_linear = linorder_class.le_less_linear
+lemmas linorder_le_cases = linorder_class.le_cases
+lemmas linorder_not_less = linorder_class.not_less
+lemmas linorder_not_le = linorder_class.not_le
+lemmas linorder_neq_iff = linorder_class.neq_iff
+lemmas linorder_neqE = linorder_class.neqE
+lemmas linorder_antisym_conv1 = linorder_class.antisym_conv1
+lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
+lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
+
+lemmas min_le_iff_disj = linorder_class.min_le_iff_disj
+lemmas le_max_iff_disj = linorder_class.le_max_iff_disj
+lemmas min_less_iff_disj = linorder_class.min_less_iff_disj
+lemmas less_max_iff_disj = linorder_class.less_max_iff_disj
+lemmas min_less_iff_conj [simp] = linorder_class.min_less_iff_conj
+lemmas max_less_iff_conj [simp] = linorder_class.max_less_iff_conj
+lemmas split_min = linorder_class.split_min
+lemmas split_max = linorder_class.split_max
+
+
 subsection {* Bounded quantifiers *}
 
 syntax
@@ -754,6 +767,7 @@
   le_bool_def: "P \<le> Q \<equiv> P \<longrightarrow> Q"
   less_bool_def: "P < Q \<equiv> P \<le> Q \<and> P \<noteq> Q"
   by intro_classes (auto simp add: le_bool_def less_bool_def)
+lemmas [code func del] = le_bool_def less_bool_def
 
 lemma le_boolI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<le> Q"
 by (simp add: le_bool_def)
diff -r acfb2413faa3 -r c0b5ff9e9e4d src/HOL/Real/PReal.thy
--- a/src/HOL/Real/PReal.thy	Fri Aug 24 14:14:17 2007 +0200
+++ b/src/HOL/Real/PReal.thy	Fri Aug 24 14:14:18 2007 +0200
@@ -17,23 +17,12 @@
 lemma add_eq_exists: "\<exists>x. a+x = (b::rat)"
 by (rule_tac x="b-a" in exI, simp)
 
-text{*As a special case, the sum of two positives is positive.  One of the
-premises could be weakened to the relation @{text "\<le>"}.*}
-lemma pos_add_strict: "[|0<a; b<c|] ==> b < a + (c::'a::ordered_semidom)"
-by (insert add_strict_mono [of 0 a b c], simp)
-
-lemma interval_empty_iff:
-     "({y::'a::ordered_field. x < y & y < z} = {}) = (~(x < z))"
-by (auto dest: dense)
-
-
 definition
   cut :: "rat set => bool" where
   "cut A = ({} \<subset> A &
             A < {r. 0 < r} &
             (\<forall>y \<in> A. ((\<forall>z. 0<z & z < y --> z \<in> A) & (\<exists>u \<in> A. y < u))))"
 
-
 lemma cut_of_rat: 
   assumes q: "0 < q" shows "cut {r::rat. 0 < r & r < q}" (is "cut ?A")
 proof -
diff -r acfb2413faa3 -r c0b5ff9e9e4d src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Fri Aug 24 14:14:17 2007 +0200
+++ b/src/HOL/Ring_and_Field.thy	Fri Aug 24 14:14:18 2007 +0200
@@ -325,6 +325,11 @@
   (*previously ordered_semiring*)
   assumes zero_less_one [simp]: "\<^loc>0 \<sqsubset> \<^loc>1"
 
+lemma pos_add_strict:
+  fixes a b c :: "'a\<Colon>ordered_semidom"
+  shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
+  using add_strict_mono [of 0 a b c] by simp
+
 class ordered_idom = comm_ring_1 + ordered_comm_semiring_strict + lordered_ab_group + abs_if
   (*previously ordered_ring*)
 
@@ -1878,8 +1883,15 @@
 lemma gt_half_sum: "a < b ==> (a+b)/(1+1::'a::ordered_field) < b"
 by (simp add: field_simps zero_less_two)
 
-lemma dense: "a < b ==> \<exists>r::'a::ordered_field. a < r & r < b"
-by (blast intro!: less_half_sum gt_half_sum)
+instance ordered_field < dense_linear_order
+proof
+  fix x y :: 'a
+  have "x < x + 1" by simp
+  then show "\<exists>y. x < y" .. 
+  have "x - 1 < x" by simp
+  then show "\<exists>y. y < x" ..
+  show "x < y \<Longrightarrow> \<exists>z>x. z < y" by (blast intro!: less_half_sum gt_half_sum)
+qed
 
 
 subsection {* Absolute Value *}