X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama_duality%2Flattice.ma;h=4da043bcc99dd99ff70b57b19820d8b8dc1ff2af;hb=9eabe046c1182960de8cfdba96c5414224e3a61e;hp=adf751b8302c979bccb3d38e401546f40dd691b0;hpb=423bf7f85d0959689266cfc7ca57958a04618002;p=helm.git diff --git a/helm/software/matita/contribs/dama/dama_duality/lattice.ma b/helm/software/matita/contribs/dama/dama_duality/lattice.ma index adf751b83..4da043bcc 100644 --- a/helm/software/matita/contribs/dama/dama_duality/lattice.ma +++ b/helm/software/matita/contribs/dama/dama_duality/lattice.ma @@ -24,7 +24,7 @@ record semi_lattice_base : Type ≝ { }. notation "a \cross b" left associative with precedence 50 for @{ 'op $a $b }. -interpretation "semi lattice base operation" 'op a b = (cic:/matita/lattice/sl_op.con _ a b). +interpretation "semi lattice base operation" 'op a b = (sl_op _ a b). lemma excess_of_semi_lattice_base: semi_lattice_base → excess. intro l; @@ -80,7 +80,7 @@ record semi_lattice : Type ≝ { sl_lem: ∀x,y.(sl_meet x y) ≤ y }. -interpretation "semi lattice meet" 'and a b = (cic:/matita/lattice/sl_meet.con _ a b). +interpretation "semi lattice meet" 'and a b = (sl_meet _ a b). lemma sl_feq_ml: ∀ml:semi_lattice.∀a,b,c:ml. a ≈ b → (c ∧ a) ≈ (c ∧ b). intros (l a b c H); unfold eq in H ⊢ %; unfold Not in H ⊢ %; @@ -183,7 +183,7 @@ qed. definition hole ≝ λT:Type.λx:T.x. notation < "\ldots" non associative with precedence 50 for @{'hole}. -interpretation "hole" 'hole = (cic:/matita/lattice/hole.con _ _). +interpretation "hole" 'hole = (hole _ _). (* SL(E,M,H2-5(#),H67(≰)) → E' → c E = c E' → H67'(≰') → SL(E,M,p2-5,H67') *) lemma subst_excess: @@ -412,10 +412,10 @@ qed. coercion cic:/matita/lattice/latt_jcarr.con. interpretation "Lattice meet" 'and a b = - (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_mcarr.con _) a b). + (sl_meet (latt_mcarr _) a b). interpretation "Lattice join" 'or a b = - (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_jcarr.con _) a b). + (sl_meet (latt_jcarr _) a b). record lattice : Type ≝ { latt_carr:> lattice_; @@ -438,36 +438,35 @@ notation "'strong_extj'" non associative with precedence 50 for @{'strong_extj}. notation "'le_to_eqj'" non associative with precedence 50 for @{'le_to_eqj}. notation "'lej'" non associative with precedence 50 for @{'lej}. -interpretation "Lattice meet" 'meet = (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_mcarr.con _)). -interpretation "Lattice meet_refl" 'meet_refl = (cic:/matita/lattice/sl_meet_refl.con (cic:/matita/lattice/latt_mcarr.con _)). -interpretation "Lattice meet_comm" 'meet_comm = (cic:/matita/lattice/sl_meet_comm.con (cic:/matita/lattice/latt_mcarr.con _)). -interpretation "Lattice meet_assoc" 'meet_assoc = (cic:/matita/lattice/sl_meet_assoc.con (cic:/matita/lattice/latt_mcarr.con _)). -interpretation "Lattice strong_extm" 'strong_extm = (cic:/matita/lattice/sl_strong_extm.con (cic:/matita/lattice/latt_mcarr.con _)). -interpretation "Lattice le_to_eqm" 'le_to_eqm = (cic:/matita/lattice/sl_le_to_eqm.con (cic:/matita/lattice/latt_mcarr.con _)). -interpretation "Lattice lem" 'lem = (cic:/matita/lattice/sl_lem.con (cic:/matita/lattice/latt_mcarr.con _)). -interpretation "Lattice join" 'join = (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_jcarr.con _)). -interpretation "Lattice join_refl" 'join_refl = (cic:/matita/lattice/sl_meet_refl.con (cic:/matita/lattice/latt_jcarr.con _)). -interpretation "Lattice join_comm" 'join_comm = (cic:/matita/lattice/sl_meet_comm.con (cic:/matita/lattice/latt_jcarr.con _)). -interpretation "Lattice join_assoc" 'join_assoc = (cic:/matita/lattice/sl_meet_assoc.con (cic:/matita/lattice/latt_jcarr.con _)). -interpretation "Lattice strong_extm" 'strong_extj = (cic:/matita/lattice/sl_strong_extm.con (cic:/matita/lattice/latt_jcarr.con _)). -interpretation "Lattice le_to_eqj" 'le_to_eqj = (cic:/matita/lattice/sl_le_to_eqm.con (cic:/matita/lattice/latt_jcarr.con _)). -interpretation "Lattice lej" 'lej = (cic:/matita/lattice/sl_lem.con (cic:/matita/lattice/latt_jcarr.con _)). +interpretation "Lattice meet" 'meet = (sl_meet (latt_mcarr _)). +interpretation "Lattice meet_refl" 'meet_refl = (sl_meet_refl (latt_mcarr _)). +interpretation "Lattice meet_comm" 'meet_comm = (sl_meet_comm (latt_mcarr _)). +interpretation "Lattice meet_assoc" 'meet_assoc = (sl_meet_assoc (latt_mcarr _)). +interpretation "Lattice strong_extm" 'strong_extm = (sl_strong_extm (latt_mcarr _)). +interpretation "Lattice le_to_eqm" 'le_to_eqm = (sl_le_to_eqm (latt_mcarr _)). +interpretation "Lattice lem" 'lem = (sl_lem (latt_mcarr _)). +interpretation "Lattice join" 'join = (sl_meet (latt_jcarr _)). +interpretation "Lattice join_refl" 'join_refl = (sl_meet_refl (latt_jcarr _)). +interpretation "Lattice join_comm" 'join_comm = (sl_meet_comm (latt_jcarr _)). +interpretation "Lattice join_assoc" 'join_assoc = (sl_meet_assoc (latt_jcarr _)). +interpretation "Lattice strong_extm" 'strong_extj = (sl_strong_extm (latt_jcarr _)). +interpretation "Lattice le_to_eqj" 'le_to_eqj = (sl_le_to_eqm (latt_jcarr _)). +interpretation "Lattice lej" 'lej = (sl_lem (latt_jcarr _)). notation "'feq_jl'" non associative with precedence 50 for @{'feq_jl}. notation "'feq_jr'" non associative with precedence 50 for @{'feq_jr}. notation "'feq_ml'" non associative with precedence 50 for @{'feq_ml}. notation "'feq_mr'" non associative with precedence 50 for @{'feq_mr}. -interpretation "Lattice feq_jl" 'feq_jl = (cic:/matita/lattice/sl_feq_ml.con (cic:/matita/lattice/latt_jcarr.con _)). -interpretation "Lattice feq_jr" 'feq_jr = (cic:/matita/lattice/sl_feq_mr.con (cic:/matita/lattice/latt_jcarr.con _)). -interpretation "Lattice feq_ml" 'feq_ml = (cic:/matita/lattice/sl_feq_ml.con (cic:/matita/lattice/latt_mcarr.con _)). -interpretation "Lattice feq_mr" 'feq_mr = (cic:/matita/lattice/sl_feq_mr.con (cic:/matita/lattice/latt_mcarr.con _)). +interpretation "Lattice feq_jl" 'feq_jl = (sl_feq_ml (latt_jcarr _)). +interpretation "Lattice feq_jr" 'feq_jr = (sl_feq_mr (latt_jcarr _)). +interpretation "Lattice feq_ml" 'feq_ml = (sl_feq_ml (latt_mcarr _)). +interpretation "Lattice feq_mr" 'feq_mr = (sl_feq_mr (latt_mcarr _)). -interpretation "Lattive meet le" 'leq a b = - (cic:/matita/excess/le.con (cic:/matita/lattice/excess_OF_lattice1.con _) a b). +interpretation "Lattive meet le" 'leq a b = (le (excess_OF_lattice1 _) a b). interpretation "Lattive join le (aka ge)" 'geq a b = - (cic:/matita/excess/le.con (cic:/matita/lattice/excess_OF_lattice.con _) a b). + (le (excess_OF_lattice _) a b). (* these coercions help unification, handmaking a bit of conversion over an open term @@ -481,4 +480,4 @@ intros(l a b H); apply H; qed. coercion cic:/matita/lattice/le_to_ge.con nocomposites. -coercion cic:/matita/lattice/ge_to_le.con nocomposites. \ No newline at end of file +coercion cic:/matita/lattice/ge_to_le.con nocomposites.