equal
deleted
inserted
replaced
299 |
299 |
300 section {* Contructive dense linear orders yield QE for linear arithmetic over ordered Fields -- see @{text "Arith_Tools.thy"} *} |
300 section {* Contructive dense linear orders yield QE for linear arithmetic over ordered Fields -- see @{text "Arith_Tools.thy"} *} |
301 |
301 |
302 text {* Linear order without upper bounds *} |
302 text {* Linear order without upper bounds *} |
303 |
303 |
304 class_locale linorder_stupid_syntax = linorder |
304 locale linorder_stupid_syntax = linorder |
305 begin |
305 begin |
306 notation |
306 notation |
307 less_eq ("op \<sqsubseteq>") and |
307 less_eq ("op \<sqsubseteq>") and |
308 less_eq ("(_/ \<sqsubseteq> _)" [51, 51] 50) and |
308 less_eq ("(_/ \<sqsubseteq> _)" [51, 51] 50) and |
309 less ("op \<sqsubset>") and |
309 less ("op \<sqsubset>") and |
310 less ("(_/ \<sqsubset> _)" [51, 51] 50) |
310 less ("(_/ \<sqsubset> _)" [51, 51] 50) |
311 |
311 |
312 end |
312 end |
313 |
313 |
314 class_locale linorder_no_ub = linorder_stupid_syntax + |
314 locale linorder_no_ub = linorder_stupid_syntax + |
315 assumes gt_ex: "\<exists>y. less x y" |
315 assumes gt_ex: "\<exists>y. less x y" |
316 begin |
316 begin |
317 lemma ge_ex: "\<exists>y. x \<sqsubseteq> y" using gt_ex by auto |
317 lemma ge_ex: "\<exists>y. x \<sqsubseteq> y" using gt_ex by auto |
318 |
318 |
319 text {* Theorems for @{text "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"} *} |
319 text {* Theorems for @{text "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"} *} |
358 |
358 |
359 end |
359 end |
360 |
360 |
361 text {* Linear order without upper bounds *} |
361 text {* Linear order without upper bounds *} |
362 |
362 |
363 class_locale linorder_no_lb = linorder_stupid_syntax + |
363 locale linorder_no_lb = linorder_stupid_syntax + |
364 assumes lt_ex: "\<exists>y. less y x" |
364 assumes lt_ex: "\<exists>y. less y x" |
365 begin |
365 begin |
366 lemma le_ex: "\<exists>y. y \<sqsubseteq> x" using lt_ex by auto |
366 lemma le_ex: "\<exists>y. y \<sqsubseteq> x" using lt_ex by auto |
367 |
367 |
368 |
368 |
405 qed |
405 qed |
406 |
406 |
407 end |
407 end |
408 |
408 |
409 |
409 |
410 class_locale constr_dense_linear_order = linorder_no_lb + linorder_no_ub + |
410 locale constr_dense_linear_order = linorder_no_lb + linorder_no_ub + |
411 fixes between |
411 fixes between |
412 assumes between_less: "less x y \<Longrightarrow> less x (between x y) \<and> less (between x y) y" |
412 assumes between_less: "less x y \<Longrightarrow> less x (between x y) \<and> less (between x y) y" |
413 and between_same: "between x x = x" |
413 and between_same: "between x x = x" |
414 |
414 |
415 class_interpretation constr_dense_linear_order < dense_linear_order |
415 sublocale constr_dense_linear_order < dense_linear_order |
416 apply unfold_locales |
416 apply unfold_locales |
417 using gt_ex lt_ex between_less |
417 using gt_ex lt_ex between_less |
418 by (auto, rule_tac x="between x y" in exI, simp) |
418 by (auto, rule_tac x="between x y" in exI, simp) |
419 |
419 |
420 context constr_dense_linear_order |
420 context constr_dense_linear_order |
633 qed |
633 qed |
634 lemma sum_eq:"((x::'a::pordered_ab_group_add) + t = 0) == (x = - t)" |
634 lemma sum_eq:"((x::'a::pordered_ab_group_add) + t = 0) == (x = - t)" |
635 using eq_diff_eq[where a= x and b=t and c=0] by simp |
635 using eq_diff_eq[where a= x and b=t and c=0] by simp |
636 |
636 |
637 |
637 |
638 class_interpretation class_ordered_field_dense_linear_order: constr_dense_linear_order |
638 interpretation class_ordered_field_dense_linear_order!: constr_dense_linear_order |
639 ["op <=" "op <" |
639 "op <=" "op <" |
640 "\<lambda> x y. 1/2 * ((x::'a::{ordered_field,recpower,number_ring}) + y)"] |
640 "\<lambda> x y. 1/2 * ((x::'a::{ordered_field,recpower,number_ring}) + y)" |
641 proof (unfold_locales, dlo, dlo, auto) |
641 proof (unfold_locales, dlo, dlo, auto) |
642 fix x y::'a assume lt: "x < y" |
642 fix x y::'a assume lt: "x < y" |
643 from less_half_sum[OF lt] show "x < (x + y) /2" by simp |
643 from less_half_sum[OF lt] show "x < (x + y) /2" by simp |
644 next |
644 next |
645 fix x y::'a assume lt: "x < y" |
645 fix x y::'a assume lt: "x < y" |