equal
deleted
inserted
replaced
450 |
450 |
451 locale constr_dense_linorder = linorder_no_lb + linorder_no_ub + |
451 locale constr_dense_linorder = linorder_no_lb + linorder_no_ub + |
452 fixes between |
452 fixes between |
453 assumes between_less: "less x y \<Longrightarrow> less x (between x y) \<and> less (between x y) y" |
453 assumes between_less: "less x y \<Longrightarrow> less x (between x y) \<and> less (between x y) y" |
454 and between_same: "between x x = x" |
454 and between_same: "between x x = x" |
455 |
455 begin |
456 sublocale constr_dense_linorder < dlo: unbounded_dense_linorder |
456 |
|
457 sublocale dlo: unbounded_dense_linorder |
457 apply unfold_locales |
458 apply unfold_locales |
458 using gt_ex lt_ex between_less |
459 using gt_ex lt_ex between_less |
459 apply auto |
460 apply auto |
460 apply (rule_tac x="between x y" in exI) |
461 apply (rule_tac x="between x y" in exI) |
461 apply simp |
462 apply simp |
462 done |
463 done |
463 |
|
464 context constr_dense_linorder |
|
465 begin |
|
466 |
464 |
467 lemma rinf_U[no_atp]: |
465 lemma rinf_U[no_atp]: |
468 assumes fU: "finite U" |
466 assumes fU: "finite U" |
469 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 |
467 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 |
470 \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P y )" |
468 \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P y )" |