Most of the time, URIs can now be replaced with identifiers in "interpretation".

[helm.git] / helm / software / matita / contribs / dama / dama_duality / lattice.ma

diff --git a/helm/software/matita/contribs/dama/dama_duality/lattice.ma b/helm/software/matita/contribs/dama/dama_duality/lattice.ma
index adf751b8302c979bccb3d38e401546f40dd691b0..4da043bcc99dd99ff70b57b19820d8b8dc1ff2af 100644 (file)
--- 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.