turned locales intro classes
authorhaftmann
Mon Aug 20 18:07:28 2007 +0200 (2007-08-20)
changeset 24344a0fd8c2db293
parent 24343 acc0f7aac619
child 24345 86a3557a9ebb
turned locales intro classes
src/HOL/Dense_Linear_Order.thy
src/HOL/ex/Meson_Test.thy
     1.1 --- a/src/HOL/Dense_Linear_Order.thy	Mon Aug 20 18:07:26 2007 +0200
     1.2 +++ b/src/HOL/Dense_Linear_Order.thy	Mon Aug 20 18:07:28 2007 +0200
     1.3 @@ -16,67 +16,13 @@
     1.4    ("Tools/Qelim/ferrante_rackoff.ML")
     1.5  begin
     1.6  
     1.7 -
     1.8  setup Langford_Data.setup
     1.9  setup Ferrante_Rackoff_Data.setup
    1.10  
    1.11 -section {* The classical QE after Langford for dense linear orders *}
    1.12 -
    1.13 -locale dense_linear_order = Linorder + 
    1.14 -  assumes gt_ex: "\<forall>x. \<exists>y. x \<sqsubset> y" 
    1.15 -  and lt_ex: "\<forall>x. \<exists>y. y \<sqsubset> x"
    1.16 -  and dense: "\<forall>x y. x \<sqsubset> y \<longrightarrow> (\<exists>z. x \<sqsubset> z \<and> z \<sqsubset> y)"
    1.17 +context linorder
    1.18  begin
    1.19  
    1.20 -lemma dlo_qe_bnds: 
    1.21 -  assumes ne: "L \<noteq> {}" and neU: "U \<noteq> {}" and fL: "finite L" and fU: "finite U"
    1.22 -  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)"
    1.23 -proof (simp only: atomize_eq, rule iffI)
    1.24 -  assume H: "\<exists>x. (\<forall>y\<in>L. y \<^loc>< x) \<and> (\<forall>y\<in>U. x \<^loc>< y)"
    1.25 -  then obtain x where xL: "\<forall>y\<in>L. y \<^loc>< x" and xU: "\<forall>y\<in>U. x \<^loc>< y" by blast
    1.26 -  {fix l u assume l: "l \<in> L" and u: "u \<in> U"
    1.27 -    from less_trans[OF xL[rule_format, OF l] xU[rule_format, OF u]]
    1.28 -    have "l \<sqsubset> u" .}
    1.29 -  thus "\<forall>l\<in>L. \<forall>u\<in>U. l \<^loc>< u" by blast
    1.30 -next
    1.31 -  assume H: "\<forall>l\<in>L. \<forall>u\<in>U. l \<^loc>< u"
    1.32 -  let ?ML = "Max L"
    1.33 -  let ?MU = "Min U"  
    1.34 -  from fL ne have th1: "?ML \<in> L" and th1': "\<forall>l\<in>L. l \<sqsubseteq> ?ML" by auto
    1.35 -  from fU neU have th2: "?MU \<in> U" and th2': "\<forall>u\<in>U. ?MU \<sqsubseteq> u" by auto
    1.36 -  from th1 th2 H have "?ML \<sqsubset> ?MU" by auto
    1.37 -  with dense obtain w where th3: "?ML \<sqsubset> w" and th4: "w \<sqsubset> ?MU" by blast
    1.38 -  from th3 th1' have "\<forall>l \<in> L. l \<sqsubset> w" 
    1.39 -    apply auto
    1.40 -    apply (erule_tac x="l" in ballE)
    1.41 -    by (auto intro: le_less_trans)
    1.42 -
    1.43 -  moreover from th4 th2' have "\<forall>u \<in> U. w \<sqsubset> u" 
    1.44 -    apply auto
    1.45 -    apply (erule_tac x="u" in ballE)
    1.46 -    by (auto intro: less_le_trans)
    1.47 -  ultimately show "\<exists>x. (\<forall>y\<in>L. y \<^loc>< x) \<and> (\<forall>y\<in>U. x \<^loc>< y)" by auto
    1.48 -qed
    1.49 -
    1.50 -lemma dlo_qe_noub: 
    1.51 -  assumes ne: "L \<noteq> {}" and fL: "finite L"
    1.52 -  shows "(\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> {}. x \<sqsubset> y)) \<equiv> True"
    1.53 -proof(simp add: atomize_eq)
    1.54 -  from gt_ex[rule_format, of "Max L"] obtain M where M: "Max L \<sqsubset> M" by blast
    1.55 -  from ne fL have "\<forall>x \<in> L. x \<sqsubseteq> Max L" by simp
    1.56 -  with M have "\<forall>x\<in>L. x \<sqsubset> M" by (auto intro: le_less_trans)
    1.57 -  thus "\<exists>x. \<forall>y\<in>L. y \<^loc>< x" by blast
    1.58 -qed
    1.59 -
    1.60 -lemma dlo_qe_nolb: 
    1.61 -  assumes ne: "U \<noteq> {}" and fU: "finite U"
    1.62 -  shows "(\<exists>x. (\<forall>y \<in> {}. y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y)) \<equiv> True"
    1.63 -proof(simp add: atomize_eq)
    1.64 -  from lt_ex[rule_format, of "Min U"] obtain M where M: "M \<sqsubset> Min U" by blast
    1.65 -  from ne fU have "\<forall>x \<in> U. Min U \<sqsubseteq> x" by simp
    1.66 -  with M have "\<forall>x\<in>U. M \<sqsubset> x" by (auto intro: less_le_trans)
    1.67 -  thus "\<exists>x. \<forall>y\<in>U. x \<^loc>< y" by blast
    1.68 -qed
    1.69 +lemma less_not_permute: "\<not> (x \<sqsubset> y \<and> y \<sqsubset> x)" by (simp add: not_less linear)
    1.70  
    1.71  lemma gather_simps: 
    1.72    shows 
    1.73 @@ -89,61 +35,6 @@
    1.74    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)" 
    1.75    by simp
    1.76  
    1.77 -lemma exists_neq: "\<exists>(x::'a). x \<noteq> t" "\<exists>(x::'a). t \<noteq> x" 
    1.78 -  using gt_ex[rule_format, of t] by auto
    1.79 -
    1.80 -lemma less_not_permute: "\<not> (x \<sqsubset> y \<and> y \<sqsubset> x)" by (simp add: not_less linear)
    1.81 -
    1.82 -lemmas dlo_simps = order_refl less_irrefl not_less not_le exists_neq 
    1.83 -  le_less neq_iff linear less_not_permute
    1.84 -
    1.85 -lemma axiom: "dense_linear_order (op \<sqsubseteq>) (op \<sqsubset>)" .
    1.86 -lemma atoms: includes meta_term_syntax
    1.87 -  shows "TERM (op \<sqsubset> :: 'a \<Rightarrow> _)" and "TERM (op \<sqsubseteq>)" and "TERM (op = :: 'a \<Rightarrow> _)" .
    1.88 -
    1.89 -declare axiom[langford qe: dlo_qe_bnds dlo_qe_nolb dlo_qe_noub gather: gather_start gather_simps atoms: atoms]
    1.90 -declare dlo_simps[langfordsimp]
    1.91 -end
    1.92 -  (* FIXME: Move to HOL -- together with the conj_aci_rule in langford.ML *)
    1.93 -
    1.94 -lemma dnf:
    1.95 -  "(P & (Q | R)) = ((P&Q) | (P&R))" 
    1.96 -  "((Q | R) & P) = ((Q&P) | (R&P))"
    1.97 -  by blast+
    1.98 -
    1.99 -lemmas weak_dnf_simps = simp_thms dnf
   1.100 -
   1.101 -
   1.102 -lemma nnf_simps:
   1.103 -    "(\<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)"
   1.104 -    "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"
   1.105 -  by blast+
   1.106 -
   1.107 -lemma ex_distrib: "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> ((\<exists>x. P x) \<or> (\<exists>x. Q x))" by blast
   1.108 -
   1.109 -lemmas dnf_simps = weak_dnf_simps nnf_simps ex_distrib
   1.110 -
   1.111 -use "Tools/Qelim/langford.ML"
   1.112 -method_setup dlo = {*
   1.113 -  Method.ctxt_args (Method.SIMPLE_METHOD' o LangfordQE.dlo_tac)
   1.114 -*} "Langford's algorithm for quantifier elimination in dense linear orders"
   1.115 -
   1.116 -interpretation dlo_ordring_class: dense_linear_order["op \<le> :: 'a::{ordered_field} \<Rightarrow> _" "op <"]
   1.117 -apply unfold_locales
   1.118 -apply auto
   1.119 -apply (rule_tac x = "x + 1" in exI, simp)
   1.120 -apply (rule_tac x = "x - 1" in exI, simp)
   1.121 -apply (rule_tac x = "(x + y) / (1 + 1)" in exI)
   1.122 -apply (rule conjI)
   1.123 -apply (rule less_half_sum, simp)
   1.124 -apply (rule gt_half_sum, simp)
   1.125 -done
   1.126 -
   1.127 -section {* Contructive dense linear orders yield QE for linear arithmetic over ordered Fields -- see @{text "Arith_Tools.thy"} *}
   1.128 -
   1.129 -context Linorder
   1.130 -begin
   1.131 -
   1.132  text{* Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"}*}
   1.133  lemma minf_lt:  "\<exists>z . \<forall>x. x \<sqsubset> z \<longrightarrow> (x \<sqsubset> t \<longleftrightarrow> True)" by auto
   1.134  lemma minf_gt: "\<exists>z . \<forall>x. x \<sqsubset> z \<longrightarrow>  (t \<sqsubset> x \<longleftrightarrow>  False)"
   1.135 @@ -303,7 +194,6 @@
   1.136    from ainS binS noy ax xb px show ?thesis by blast
   1.137  qed
   1.138  
   1.139 -
   1.140  lemma finite_set_intervals2:
   1.141    assumes px: "P x" and lx: "l \<sqsubseteq> x" and xu: "x \<sqsubseteq> u" and linS: "l\<in> S"
   1.142    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"
   1.143 @@ -319,9 +209,121 @@
   1.144  
   1.145  end
   1.146  
   1.147 +section {* The classical QE after Langford for dense linear orders *}
   1.148 +
   1.149 +class dense_linear_order = linorder + 
   1.150 +  assumes gt_ex: "\<forall>x. \<exists>y. x \<sqsubset> y" 
   1.151 +  and lt_ex: "\<forall>x. \<exists>y. y \<sqsubset> x"
   1.152 +  and dense: "\<forall>x y. x \<sqsubset> y \<longrightarrow> (\<exists>z. x \<sqsubset> z \<and> z \<sqsubset> y)"
   1.153 +begin
   1.154 +
   1.155 +lemma dlo_qe_bnds: 
   1.156 +  assumes ne: "L \<noteq> {}" and neU: "U \<noteq> {}" and fL: "finite L" and fU: "finite U"
   1.157 +  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)"
   1.158 +proof (simp only: atomize_eq, rule iffI)
   1.159 +  assume H: "\<exists>x. (\<forall>y\<in>L. y \<^loc>< x) \<and> (\<forall>y\<in>U. x \<^loc>< y)"
   1.160 +  then obtain x where xL: "\<forall>y\<in>L. y \<^loc>< x" and xU: "\<forall>y\<in>U. x \<^loc>< y" by blast
   1.161 +  {fix l u assume l: "l \<in> L" and u: "u \<in> U"
   1.162 +    from less_trans[OF xL[rule_format, OF l] xU[rule_format, OF u]]
   1.163 +    have "l \<sqsubset> u" .}
   1.164 +  thus "\<forall>l\<in>L. \<forall>u\<in>U. l \<^loc>< u" by blast
   1.165 +next
   1.166 +  assume H: "\<forall>l\<in>L. \<forall>u\<in>U. l \<^loc>< u"
   1.167 +  let ?ML = "Max L"
   1.168 +  let ?MU = "Min U"  
   1.169 +  from fL ne have th1: "?ML \<in> L" and th1': "\<forall>l\<in>L. l \<sqsubseteq> ?ML" by auto
   1.170 +  from fU neU have th2: "?MU \<in> U" and th2': "\<forall>u\<in>U. ?MU \<sqsubseteq> u" by auto
   1.171 +  from th1 th2 H have "?ML \<sqsubset> ?MU" by auto
   1.172 +  with dense obtain w where th3: "?ML \<sqsubset> w" and th4: "w \<sqsubset> ?MU" by blast
   1.173 +  from th3 th1' have "\<forall>l \<in> L. l \<sqsubset> w" 
   1.174 +    apply auto
   1.175 +    apply (erule_tac x="l" in ballE)
   1.176 +    by (auto intro: le_less_trans)
   1.177 +
   1.178 +  moreover from th4 th2' have "\<forall>u \<in> U. w \<sqsubset> u" 
   1.179 +    apply auto
   1.180 +    apply (erule_tac x="u" in ballE)
   1.181 +    by (auto intro: less_le_trans)
   1.182 +  ultimately show "\<exists>x. (\<forall>y\<in>L. y \<^loc>< x) \<and> (\<forall>y\<in>U. x \<^loc>< y)" by auto
   1.183 +qed
   1.184 +
   1.185 +lemma dlo_qe_noub: 
   1.186 +  assumes ne: "L \<noteq> {}" and fL: "finite L"
   1.187 +  shows "(\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> {}. x \<sqsubset> y)) \<equiv> True"
   1.188 +proof(simp add: atomize_eq)
   1.189 +  from gt_ex[rule_format, of "Max L"] obtain M where M: "Max L \<sqsubset> M" by blast
   1.190 +  from ne fL have "\<forall>x \<in> L. x \<sqsubseteq> Max L" by simp
   1.191 +  with M have "\<forall>x\<in>L. x \<sqsubset> M" by (auto intro: le_less_trans)
   1.192 +  thus "\<exists>x. \<forall>y\<in>L. y \<^loc>< x" by blast
   1.193 +qed
   1.194 +
   1.195 +lemma dlo_qe_nolb: 
   1.196 +  assumes ne: "U \<noteq> {}" and fU: "finite U"
   1.197 +  shows "(\<exists>x. (\<forall>y \<in> {}. y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y)) \<equiv> True"
   1.198 +proof(simp add: atomize_eq)
   1.199 +  from lt_ex[rule_format, of "Min U"] obtain M where M: "M \<sqsubset> Min U" by blast
   1.200 +  from ne fU have "\<forall>x \<in> U. Min U \<sqsubseteq> x" by simp
   1.201 +  with M have "\<forall>x\<in>U. M \<sqsubset> x" by (auto intro: less_le_trans)
   1.202 +  thus "\<exists>x. \<forall>y\<in>U. x \<^loc>< y" by blast
   1.203 +qed
   1.204 +
   1.205 +lemma exists_neq: "\<exists>(x::'a). x \<noteq> t" "\<exists>(x::'a). t \<noteq> x" 
   1.206 +  using gt_ex[rule_format, of t] by auto
   1.207 +
   1.208 +lemmas dlo_simps = order_refl less_irrefl not_less not_le exists_neq 
   1.209 +  le_less neq_iff linear less_not_permute
   1.210 +
   1.211 +lemma axiom: "dense_linear_order (op \<sqsubseteq>) (op \<sqsubset>)" .
   1.212 +lemma atoms: includes meta_term_syntax
   1.213 +  shows "TERM (op \<sqsubset> :: 'a \<Rightarrow> _)" and "TERM (op \<sqsubseteq>)" and "TERM (op = :: 'a \<Rightarrow> _)" .
   1.214 +
   1.215 +declare axiom[langford qe: dlo_qe_bnds dlo_qe_nolb dlo_qe_noub gather: gather_start gather_simps atoms: atoms]
   1.216 +declare dlo_simps[langfordsimp]
   1.217 +
   1.218 +end
   1.219 +
   1.220 +(* FIXME: Move to HOL -- together with the conj_aci_rule in langford.ML *)
   1.221 +lemma dnf:
   1.222 +  "(P & (Q | R)) = ((P&Q) | (P&R))" 
   1.223 +  "((Q | R) & P) = ((Q&P) | (R&P))"
   1.224 +  by blast+
   1.225 +
   1.226 +lemmas weak_dnf_simps = simp_thms dnf
   1.227 +
   1.228 +lemma nnf_simps:
   1.229 +    "(\<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)"
   1.230 +    "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"
   1.231 +  by blast+
   1.232 +
   1.233 +lemma ex_distrib: "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> ((\<exists>x. P x) \<or> (\<exists>x. Q x))" by blast
   1.234 +
   1.235 +lemmas dnf_simps = weak_dnf_simps nnf_simps ex_distrib
   1.236 +
   1.237 +use "Tools/Qelim/langford.ML"
   1.238 +method_setup dlo = {*
   1.239 +  Method.ctxt_args (Method.SIMPLE_METHOD' o LangfordQE.dlo_tac)
   1.240 +*} "Langford's algorithm for quantifier elimination in dense linear orders"
   1.241 +
   1.242 +interpretation dlo_ordring_class: dense_linear_order ["op \<le> \<Colon> 'a\<Colon>ordered_field \<Rightarrow> _" "op <"]
   1.243 +apply unfold_locales
   1.244 +apply auto
   1.245 +apply (rule_tac x = "x + 1" in exI, simp)
   1.246 +apply (rule_tac x = "x - 1" in exI, simp)
   1.247 +apply (rule_tac x = "(x + y) / (1 + 1)" in exI)
   1.248 +apply (rule conjI)
   1.249 +apply (rule less_half_sum, simp)
   1.250 +apply (rule gt_half_sum, simp)
   1.251 +done
   1.252 +
   1.253 +
   1.254 +section {* Contructive dense linear orders yield QE for linear arithmetic over ordered Fields -- see @{text "Arith_Tools.thy"} *}
   1.255 +
   1.256 +
   1.257 +
   1.258  text {* Linear order without upper bounds *}
   1.259  
   1.260 -locale linorder_no_ub = Linorder + assumes gt_ex: "\<forall>x. \<exists>y. x \<sqsubset> y"
   1.261 +class linorder_no_ub = linorder +
   1.262 +  assumes gt_ex: "\<forall>x. \<exists>y. x \<sqsubset> y"
   1.263  begin
   1.264  
   1.265  lemma ge_ex: "\<forall>x. \<exists>y. x \<sqsubseteq> y" using gt_ex by auto
   1.266 @@ -370,7 +372,8 @@
   1.267  
   1.268  text {* Linear order without upper bounds *}
   1.269  
   1.270 -locale linorder_no_lb = Linorder + assumes lt_ex: "\<forall>x. \<exists>y. y \<sqsubset> x"
   1.271 +class linorder_no_lb = linorder +
   1.272 +  assumes lt_ex: "\<forall>x. \<exists>y. y \<sqsubset> x"
   1.273  begin
   1.274  
   1.275  lemma le_ex: "\<forall>x. \<exists>y. y \<sqsubseteq> x" using lt_ex by auto
   1.276 @@ -416,12 +419,13 @@
   1.277  
   1.278  end
   1.279  
   1.280 -locale constr_dense_linear_order = linorder_no_lb + linorder_no_ub +
   1.281 +
   1.282 +class constr_dense_linear_order = linorder_no_lb + linorder_no_ub +
   1.283    fixes between
   1.284    assumes between_less: "\<forall>x y. x \<sqsubset> y \<longrightarrow> x \<sqsubset> between x y \<and> between x y \<sqsubset> y"
   1.285       and  between_same: "\<forall>x. between x x = x"
   1.286  
   1.287 -interpretation constr_dense_linear_order < dense_linear_order
   1.288 +instance advanced constr_dense_linear_order < dense_linear_order
   1.289    apply unfold_locales
   1.290    using gt_ex lt_ex between_less
   1.291      by (auto, rule_tac x="between x y" in exI, simp)
   1.292 @@ -547,11 +551,14 @@
   1.293  
   1.294  end
   1.295  
   1.296 -
   1.297  use "Tools/Qelim/ferrante_rackoff.ML"
   1.298  
   1.299  method_setup ferrack = {*
   1.300    Method.ctxt_args (Method.SIMPLE_METHOD' o FerranteRackoff.dlo_tac)
   1.301  *} "Ferrante and Rackoff's algorithm for quantifier elimination in dense linear orders"
   1.302  
   1.303 +
   1.304 +(*FIXME: synchronize dense orders with existing algebra*)
   1.305 +lemmas dense = Ring_and_Field.dense
   1.306 +
   1.307  end 
     2.1 --- a/src/HOL/ex/Meson_Test.thy	Mon Aug 20 18:07:26 2007 +0200
     2.2 +++ b/src/HOL/ex/Meson_Test.thy	Mon Aug 20 18:07:28 2007 +0200
     2.3 @@ -11,7 +11,7 @@
     2.4    below and constants declared in HOL!
     2.5  *}
     2.6  
     2.7 -hide const subset member quotient
     2.8 +hide const subset member quotient between
     2.9  
    2.10  
    2.11  text {*