1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "bishop_set.ma".
17 coercion cic:/matita/dama/bishop_set/eq_sym.con.
19 lemma eq_trans:∀E:bishop_set.∀x,z,y:E.x ≈ y → y ≈ z → x ≈ z ≝
20 λE,x,y,z.eq_trans_ E x z y.
22 notation > "'Eq'≈" non associative with precedence 50
25 interpretation "eq_rew" 'eqrewrite =
26 (cic:/matita/dama/bishop_set/eq_trans.con _ _ _).
28 lemma le_rewl: ∀E:ordered_set.∀z,y,x:E. x ≈ y → x ≤ z → y ≤ z.
29 intros (E z y x Exy Lxz); apply (le_transitive ???? ? Lxz);
30 intro Xyz; apply Exy; right; assumption;
33 lemma le_rewr: ∀E:ordered_set.∀z,y,x:E. x ≈ y → z ≤ x → z ≤ y.
34 intros (E z y x Exy Lxz); apply (le_transitive ???? Lxz);
35 intro Xyz; apply Exy; left; assumption;
38 notation > "'Le'≪" non associative with precedence 50 for @{'lerewritel}.
39 interpretation "le_rewl" 'lerewritel = (cic:/matita/dama/bishop_set_rewrite/le_rewl.con _ _ _).
40 notation > "'Le'≫" non associative with precedence 50 for @{'lerewriter}.
41 interpretation "le_rewr" 'lerewriter = (cic:/matita/dama/bishop_set_rewrite/le_rewr.con _ _ _).
43 lemma ap_rewl: ∀A:bishop_set.∀x,z,y:A. x ≈ y → y # z → x # z.
44 intros (A x z y Exy Ayz); cases (bs_cotransitive ???x Ayz); [2:assumption]
45 cases (eq_sym ??? Exy H);
48 lemma ap_rewr: ∀A:bishop_set.∀x,z,y:A. x ≈ y → z # y → z # x.
49 intros (A x z y Exy Azy); apply bs_symmetric; apply (ap_rewl ???? Exy);
50 apply bs_symmetric; assumption;
53 notation > "'Ap'≪" non associative with precedence 50 for @{'aprewritel}.
54 interpretation "ap_rewl" 'aprewritel = (cic:/matita/dama/bishop_set_rewrite/ap_rewl.con _ _ _).
55 notation > "'Ap'≫" non associative with precedence 50 for @{'aprewriter}.
56 interpretation "ap_rewr" 'aprewriter = (cic:/matita/dama/bishop_set_rewrite/ap_rewr.con _ _ _).
58 lemma exc_rewl: ∀A:ordered_set.∀x,z,y:A. x ≈ y → y ≰ z → x ≰ z.
59 intros (A x z y Exy Ayz); cases (os_cotransitive ??? x Ayz); [2:assumption]
60 cases Exy; right; assumption;
63 lemma exc_rewr: ∀A:ordered_set.∀x,z,y:A. x ≈ y → z ≰ y → z ≰ x.
64 intros (A x z y Exy Azy); cases (os_cotransitive ???x Azy); [assumption]
65 cases (Exy); left; assumption;
68 notation > "'Ex'≪" non associative with precedence 50 for @{'ordered_setrewritel}.
69 interpretation "exc_rewl" 'ordered_setrewritel = (cic:/matita/dama/bishop_set_rewrite/exc_rewl.con _ _ _).
70 notation > "'Ex'≫" non associative with precedence 50 for @{'ordered_setrewriter}.
71 interpretation "exc_rewr" 'ordered_setrewriter = (cic:/matita/dama/bishop_set_rewrite/exc_rewr.con _ _ _).