# HG changeset patch
# User haftmann
# Date 1187626048 -7200
# Node ID a0fd8c2db29364c9b398bb8db089bcc581b82b3a
# Parent  acc0f7aac6190fdd11eed81380cb906a6988754e
turned locales intro classes

diff -r acc0f7aac619 -r a0fd8c2db293 src/HOL/Dense_Linear_Order.thy
--- a/src/HOL/Dense_Linear_Order.thy	Mon Aug 20 18:07:26 2007 +0200
+++ b/src/HOL/Dense_Linear_Order.thy	Mon Aug 20 18:07:28 2007 +0200
@@ -16,67 +16,13 @@
   ("Tools/Qelim/ferrante_rackoff.ML")
 begin
 
-
 setup Langford_Data.setup
 setup Ferrante_Rackoff_Data.setup
 
-section {* The classical QE after Langford for dense linear orders *}
-
-locale dense_linear_order = Linorder + 
-  assumes gt_ex: "\<forall>x. \<exists>y. x \<sqsubset> y" 
-  and lt_ex: "\<forall>x. \<exists>y. y \<sqsubset> x"
-  and dense: "\<forall>x y. x \<sqsubset> y \<longrightarrow> (\<exists>z. x \<sqsubset> z \<and> z \<sqsubset> y)"
+context linorder
 begin
 
-lemma dlo_qe_bnds: 
-  assumes ne: "L \<noteq> {}" and neU: "U \<noteq> {}" and fL: "finite L" and fU: "finite U"
-  shows "(\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y)) \<equiv> (\<forall> l \<in> L. \<forall>u \<in> U. l \<sqsubset> u)"
-proof (simp only: atomize_eq, rule iffI)
-  assume H: "\<exists>x. (\<forall>y\<in>L. y \<^loc>< x) \<and> (\<forall>y\<in>U. x \<^loc>< y)"
-  then obtain x where xL: "\<forall>y\<in>L. y \<^loc>< x" and xU: "\<forall>y\<in>U. x \<^loc>< y" by blast
-  {fix l u assume l: "l \<in> L" and u: "u \<in> U"
-    from less_trans[OF xL[rule_format, OF l] xU[rule_format, OF u]]
-    have "l \<sqsubset> u" .}
-  thus "\<forall>l\<in>L. \<forall>u\<in>U. l \<^loc>< u" by blast
-next
-  assume H: "\<forall>l\<in>L. \<forall>u\<in>U. l \<^loc>< u"
-  let ?ML = "Max L"
-  let ?MU = "Min U"  
-  from fL ne have th1: "?ML \<in> L" and th1': "\<forall>l\<in>L. l \<sqsubseteq> ?ML" by auto
-  from fU neU have th2: "?MU \<in> U" and th2': "\<forall>u\<in>U. ?MU \<sqsubseteq> u" by auto
-  from th1 th2 H have "?ML \<sqsubset> ?MU" by auto
-  with dense obtain w where th3: "?ML \<sqsubset> w" and th4: "w \<sqsubset> ?MU" by blast
-  from th3 th1' have "\<forall>l \<in> L. l \<sqsubset> w" 
-    apply auto
-    apply (erule_tac x="l" in ballE)
-    by (auto intro: le_less_trans)
-
-  moreover from th4 th2' have "\<forall>u \<in> U. w \<sqsubset> u" 
-    apply auto
-    apply (erule_tac x="u" in ballE)
-    by (auto intro: less_le_trans)
-  ultimately show "\<exists>x. (\<forall>y\<in>L. y \<^loc>< x) \<and> (\<forall>y\<in>U. x \<^loc>< y)" by auto
-qed
-
-lemma dlo_qe_noub: 
-  assumes ne: "L \<noteq> {}" and fL: "finite L"
-  shows "(\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> {}. x \<sqsubset> y)) \<equiv> True"
-proof(simp add: atomize_eq)
-  from gt_ex[rule_format, of "Max L"] obtain M where M: "Max L \<sqsubset> M" by blast
-  from ne fL have "\<forall>x \<in> L. x \<sqsubseteq> Max L" by simp
-  with M have "\<forall>x\<in>L. x \<sqsubset> M" by (auto intro: le_less_trans)
-  thus "\<exists>x. \<forall>y\<in>L. y \<^loc>< x" by blast
-qed
-
-lemma dlo_qe_nolb: 
-  assumes ne: "U \<noteq> {}" and fU: "finite U"
-  shows "(\<exists>x. (\<forall>y \<in> {}. y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y)) \<equiv> True"
-proof(simp add: atomize_eq)
-  from lt_ex[rule_format, of "Min U"] obtain M where M: "M \<sqsubset> Min U" by blast
-  from ne fU have "\<forall>x \<in> U. Min U \<sqsubseteq> x" by simp
-  with M have "\<forall>x\<in>U. M \<sqsubset> x" by (auto intro: less_le_trans)
-  thus "\<exists>x. \<forall>y\<in>U. x \<^loc>< y" by blast
-qed
+lemma less_not_permute: "\<not> (x \<sqsubset> y \<and> y \<sqsubset> x)" by (simp add: not_less linear)
 
 lemma gather_simps: 
   shows 
@@ -89,61 +35,6 @@
   gather_start: "(\<exists>x. P x) \<equiv> (\<exists>x. (\<forall>y \<in> {}. y \<^loc>< x) \<and> (\<forall>y\<in> {}. x \<sqsubset> y) \<and> P x)" 
   by simp
 
-lemma exists_neq: "\<exists>(x::'a). x \<noteq> t" "\<exists>(x::'a). t \<noteq> x" 
-  using gt_ex[rule_format, of t] by auto
-
-lemma less_not_permute: "\<not> (x \<sqsubset> y \<and> y \<sqsubset> x)" by (simp add: not_less linear)
-
-lemmas dlo_simps = order_refl less_irrefl not_less not_le exists_neq 
-  le_less neq_iff linear less_not_permute
-
-lemma axiom: "dense_linear_order (op \<sqsubseteq>) (op \<sqsubset>)" .
-lemma atoms: includes meta_term_syntax
-  shows "TERM (op \<sqsubset> :: 'a \<Rightarrow> _)" and "TERM (op \<sqsubseteq>)" and "TERM (op = :: 'a \<Rightarrow> _)" .
-
-declare axiom[langford qe: dlo_qe_bnds dlo_qe_nolb dlo_qe_noub gather: gather_start gather_simps atoms: atoms]
-declare dlo_simps[langfordsimp]
-end
-  (* FIXME: Move to HOL -- together with the conj_aci_rule in langford.ML *)
-
-lemma dnf:
-  "(P & (Q | R)) = ((P&Q) | (P&R))" 
-  "((Q | R) & P) = ((Q&P) | (R&P))"
-  by blast+
-
-lemmas weak_dnf_simps = simp_thms dnf
-
-
-lemma nnf_simps:
-    "(\<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)"
-    "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"
-  by blast+
-
-lemma ex_distrib: "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> ((\<exists>x. P x) \<or> (\<exists>x. Q x))" by blast
-
-lemmas dnf_simps = weak_dnf_simps nnf_simps ex_distrib
-
-use "Tools/Qelim/langford.ML"
-method_setup dlo = {*
-  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> :: 'a::{ordered_field} \<Rightarrow> _" "op <"]
-apply unfold_locales
-apply auto
-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"} *}
-
-context Linorder
-begin
-
 text{* Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"}*}
 lemma minf_lt:  "\<exists>z . \<forall>x. x \<sqsubset> z \<longrightarrow> (x \<sqsubset> t \<longleftrightarrow> True)" by auto
 lemma minf_gt: "\<exists>z . \<forall>x. x \<sqsubset> z \<longrightarrow>  (t \<sqsubset> x \<longleftrightarrow>  False)"
@@ -303,7 +194,6 @@
   from ainS binS noy ax xb px show ?thesis by blast
 qed
 
-
 lemma finite_set_intervals2:
   assumes px: "P x" and lx: "l \<sqsubseteq> x" and xu: "x \<sqsubseteq> u" and linS: "l\<in> S"
   and uinS: "u \<in> S" and fS:"finite S" and lS: "\<forall> x\<in> S. l \<sqsubseteq> x" and Su: "\<forall> x\<in> S. x \<sqsubseteq> u"
@@ -319,9 +209,121 @@
 
 end
 
+section {* The classical QE after Langford for dense linear orders *}
+
+class dense_linear_order = linorder + 
+  assumes gt_ex: "\<forall>x. \<exists>y. x \<sqsubset> y" 
+  and lt_ex: "\<forall>x. \<exists>y. y \<sqsubset> x"
+  and dense: "\<forall>x y. x \<sqsubset> y \<longrightarrow> (\<exists>z. x \<sqsubset> z \<and> z \<sqsubset> y)"
+begin
+
+lemma dlo_qe_bnds: 
+  assumes ne: "L \<noteq> {}" and neU: "U \<noteq> {}" and fL: "finite L" and fU: "finite U"
+  shows "(\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y)) \<equiv> (\<forall> l \<in> L. \<forall>u \<in> U. l \<sqsubset> u)"
+proof (simp only: atomize_eq, rule iffI)
+  assume H: "\<exists>x. (\<forall>y\<in>L. y \<^loc>< x) \<and> (\<forall>y\<in>U. x \<^loc>< y)"
+  then obtain x where xL: "\<forall>y\<in>L. y \<^loc>< x" and xU: "\<forall>y\<in>U. x \<^loc>< y" by blast
+  {fix l u assume l: "l \<in> L" and u: "u \<in> U"
+    from less_trans[OF xL[rule_format, OF l] xU[rule_format, OF u]]
+    have "l \<sqsubset> u" .}
+  thus "\<forall>l\<in>L. \<forall>u\<in>U. l \<^loc>< u" by blast
+next
+  assume H: "\<forall>l\<in>L. \<forall>u\<in>U. l \<^loc>< u"
+  let ?ML = "Max L"
+  let ?MU = "Min U"  
+  from fL ne have th1: "?ML \<in> L" and th1': "\<forall>l\<in>L. l \<sqsubseteq> ?ML" by auto
+  from fU neU have th2: "?MU \<in> U" and th2': "\<forall>u\<in>U. ?MU \<sqsubseteq> u" by auto
+  from th1 th2 H have "?ML \<sqsubset> ?MU" by auto
+  with dense obtain w where th3: "?ML \<sqsubset> w" and th4: "w \<sqsubset> ?MU" by blast
+  from th3 th1' have "\<forall>l \<in> L. l \<sqsubset> w" 
+    apply auto
+    apply (erule_tac x="l" in ballE)
+    by (auto intro: le_less_trans)
+
+  moreover from th4 th2' have "\<forall>u \<in> U. w \<sqsubset> u" 
+    apply auto
+    apply (erule_tac x="u" in ballE)
+    by (auto intro: less_le_trans)
+  ultimately show "\<exists>x. (\<forall>y\<in>L. y \<^loc>< x) \<and> (\<forall>y\<in>U. x \<^loc>< y)" by auto
+qed
+
+lemma dlo_qe_noub: 
+  assumes ne: "L \<noteq> {}" and fL: "finite L"
+  shows "(\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> {}. x \<sqsubset> y)) \<equiv> True"
+proof(simp add: atomize_eq)
+  from gt_ex[rule_format, of "Max L"] obtain M where M: "Max L \<sqsubset> M" by blast
+  from ne fL have "\<forall>x \<in> L. x \<sqsubseteq> Max L" by simp
+  with M have "\<forall>x\<in>L. x \<sqsubset> M" by (auto intro: le_less_trans)
+  thus "\<exists>x. \<forall>y\<in>L. y \<^loc>< x" by blast
+qed
+
+lemma dlo_qe_nolb: 
+  assumes ne: "U \<noteq> {}" and fU: "finite U"
+  shows "(\<exists>x. (\<forall>y \<in> {}. y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y)) \<equiv> True"
+proof(simp add: atomize_eq)
+  from lt_ex[rule_format, of "Min U"] obtain M where M: "M \<sqsubset> Min U" by blast
+  from ne fU have "\<forall>x \<in> U. Min U \<sqsubseteq> x" by simp
+  with M have "\<forall>x\<in>U. M \<sqsubset> x" by (auto intro: less_le_trans)
+  thus "\<exists>x. \<forall>y\<in>U. x \<^loc>< y" by blast
+qed
+
+lemma exists_neq: "\<exists>(x::'a). x \<noteq> t" "\<exists>(x::'a). t \<noteq> x" 
+  using gt_ex[rule_format, of t] by auto
+
+lemmas dlo_simps = order_refl less_irrefl not_less not_le exists_neq 
+  le_less neq_iff linear less_not_permute
+
+lemma axiom: "dense_linear_order (op \<sqsubseteq>) (op \<sqsubset>)" .
+lemma atoms: includes meta_term_syntax
+  shows "TERM (op \<sqsubset> :: 'a \<Rightarrow> _)" and "TERM (op \<sqsubseteq>)" and "TERM (op = :: 'a \<Rightarrow> _)" .
+
+declare axiom[langford qe: dlo_qe_bnds dlo_qe_nolb dlo_qe_noub gather: gather_start gather_simps atoms: atoms]
+declare dlo_simps[langfordsimp]
+
+end
+
+(* FIXME: Move to HOL -- together with the conj_aci_rule in langford.ML *)
+lemma dnf:
+  "(P & (Q | R)) = ((P&Q) | (P&R))" 
+  "((Q | R) & P) = ((Q&P) | (R&P))"
+  by blast+
+
+lemmas weak_dnf_simps = simp_thms dnf
+
+lemma nnf_simps:
+    "(\<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)"
+    "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"
+  by blast+
+
+lemma ex_distrib: "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> ((\<exists>x. P x) \<or> (\<exists>x. Q x))" by blast
+
+lemmas dnf_simps = weak_dnf_simps nnf_simps ex_distrib
+
+use "Tools/Qelim/langford.ML"
+method_setup dlo = {*
+  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 auto
+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 *}
 
-locale linorder_no_ub = Linorder + assumes gt_ex: "\<forall>x. \<exists>y. x \<sqsubset> y"
+class linorder_no_ub = linorder +
+  assumes gt_ex: "\<forall>x. \<exists>y. x \<sqsubset> y"
 begin
 
 lemma ge_ex: "\<forall>x. \<exists>y. x \<sqsubseteq> y" using gt_ex by auto
@@ -370,7 +372,8 @@
 
 text {* Linear order without upper bounds *}
 
-locale linorder_no_lb = Linorder + assumes lt_ex: "\<forall>x. \<exists>y. y \<sqsubset> x"
+class linorder_no_lb = linorder +
+  assumes lt_ex: "\<forall>x. \<exists>y. y \<sqsubset> x"
 begin
 
 lemma le_ex: "\<forall>x. \<exists>y. y \<sqsubseteq> x" using lt_ex by auto
@@ -416,12 +419,13 @@
 
 end
 
-locale constr_dense_linear_order = linorder_no_lb + linorder_no_ub +
+
+class constr_dense_linear_order = linorder_no_lb + linorder_no_ub +
   fixes between
   assumes between_less: "\<forall>x y. x \<sqsubset> y \<longrightarrow> x \<sqsubset> between x y \<and> between x y \<sqsubset> y"
      and  between_same: "\<forall>x. between x x = x"
 
-interpretation constr_dense_linear_order < dense_linear_order
+instance advanced constr_dense_linear_order < dense_linear_order
   apply unfold_locales
   using gt_ex lt_ex between_less
     by (auto, rule_tac x="between x y" in exI, simp)
@@ -547,11 +551,14 @@
 
 end
 
-
 use "Tools/Qelim/ferrante_rackoff.ML"
 
 method_setup ferrack = {*
   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 acc0f7aac619 -r a0fd8c2db293 src/HOL/ex/Meson_Test.thy
--- a/src/HOL/ex/Meson_Test.thy	Mon Aug 20 18:07:26 2007 +0200
+++ b/src/HOL/ex/Meson_Test.thy	Mon Aug 20 18:07:28 2007 +0200
@@ -11,7 +11,7 @@
   below and constants declared in HOL!
 *}
 
-hide const subset member quotient
+hide const subset member quotient between
 
 
 text {*