From e57099824bce7206a8d60c2b05ced28f4e90933a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 6 Dec 2007 09:57:03 +0000
Subject: [PATCH] weight -> value

---
 ...ighted_lattice.ma => prevalued_lattice.ma} | 30 +++++++++----------
 1 file changed, 15 insertions(+), 15 deletions(-)
 rename helm/software/matita/dama/{preweighted_lattice.ma => prevalued_lattice.ma} (93%)

diff --git a/helm/software/matita/dama/preweighted_lattice.ma b/helm/software/matita/dama/prevalued_lattice.ma
similarity index 93%
rename from helm/software/matita/dama/preweighted_lattice.ma
rename to helm/software/matita/dama/prevalued_lattice.ma
index 5dbaf51ec..5f1a062e0 100644
--- a/helm/software/matita/dama/preweighted_lattice.ma
+++ b/helm/software/matita/dama/prevalued_lattice.ma
@@ -12,11 +12,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/preweighted_lattice/".
+set "baseuri" "cic:/matita/prevalued_lattice/".
 
 include "ordered_group.ma".
 
-record wlattice (R : ogroup) : Type ≝ {
+record vlattice (R : togroup) : Type ≝ {
   wl_carr:> Type;
   value: wl_carr → R;
   join: wl_carr → wl_carr → wl_carr;
@@ -35,18 +35,18 @@ record wlattice (R : ogroup) : Type ≝ {
 }. 
 
 interpretation "valued lattice meet" 'and a b =
- (cic:/matita/preweighted_lattice/meet.con _ _ a b).
+ (cic:/matita/prevalued_lattice/meet.con _ _ a b).
 
 interpretation "valued lattice join" 'or a b =
- (cic:/matita/preweighted_lattice/join.con _ _ a b).
+ (cic:/matita/prevalued_lattice/join.con _ _ a b).
  
 notation < "\nbsp \mu a" non associative with precedence 80 for @{ 'value2 $a}.
-interpretation "lattice value" 'value2 a = (cic:/matita/preweighted_lattice/value.con _ _ a).
+interpretation "lattice value" 'value2 a = (cic:/matita/prevalued_lattice/value.con _ _ a).
 
 notation "\mu" non associative with precedence 80 for @{ 'value }.
-interpretation "lattice value" 'value = (cic:/matita/preweighted_lattice/value.con _ _).
+interpretation "lattice value" 'value = (cic:/matita/prevalued_lattice/value.con _ _).
 
-lemma feq_joinr: ∀R.∀L:wlattice R.∀x,y,z:L. 
+lemma feq_joinr: ∀R.∀L:vlattice R.∀x,y,z:L. 
   μ x ≈ μ y → μ (z ∧ x) ≈ μ (z ∧ y) → μ (z ∨ x) ≈ μ (z ∨ y).
 intros (R L x y z H H1);
 apply (plus_cancr ??? (μ(z∧x)));
@@ -62,7 +62,7 @@ apply (Eq≈ (0+ μ(z∧x)) ? (opp_inverse ??));
 apply (Eq≈ (μ (z ∧ x)) H1 (zero_neutral ??));
 qed.
 
-lemma modularj: ∀R.∀L:wlattice R.∀y,z:L. μ(y∨z) ≈ μy + μz + -μ (y ∧ z).
+lemma modularj: ∀R.∀L:vlattice R.∀y,z:L. μ(y∨z) ≈ μy + μz + -μ (y ∧ z).
 intros (R L y z);
 lapply (modular_mjp ?? y z) as H1;
 apply (plus_cancr ??? (μ(y ∧ z)));
@@ -74,7 +74,7 @@ apply (Eq≈ (μy + μz) ? (eq_sym ??? (zero_neutral ??)));
 apply eq_reflexive.
 qed.
 
-lemma modularm: ∀R.∀L:wlattice R.∀y,z:L. μ(y∧z) ≈ μy + μz + -μ (y ∨ z).
+lemma modularm: ∀R.∀L:vlattice R.∀y,z:L. μ(y∧z) ≈ μy + μz + -μ (y ∨ z).
 (* CSC: questa è la causa per cui la hint per cercare i duplicati ci sta 1 mese *)
 (* exact modularj; *)
 intros (R L y z);
@@ -89,7 +89,7 @@ apply (Eq≈ (μy + μz) ? (eq_sym ??? (zero_neutral ??)));
 apply eq_reflexive.
 qed.
 
-lemma modularmj: ∀R.∀L:wlattice R.∀x,y,z:L.μ(x∧(y∨z))≈(μx + μ(y ∨ z) + - μ(x∨(y∨z))).
+lemma modularmj: ∀R.∀L:vlattice R.∀x,y,z:L.μ(x∧(y∨z))≈(μx + μ(y ∨ z) + - μ(x∨(y∨z))).
 intros (R L x y z);
 lapply (modular_mjp ?? x (y ∨ z)) as H1;
 apply (Eq≈ (μ(x∨(y∨z))+ μ(x∧(y∨z)) +-μ(x∨(y∨z))) ? (feq_plusr ???? H1)); clear H1;
@@ -100,7 +100,7 @@ apply (Eq≈ (μ(x∧(y∨z))) ? (zero_neutral ??));
 apply eq_reflexive.
 qed.
 
-lemma modularjm: ∀R.∀L:wlattice R.∀x,y,z:L.μ(x∨(y∧z))≈(μx + μ(y ∧ z) + - μ(x∧(y∧z))).
+lemma modularjm: ∀R.∀L:vlattice R.∀x,y,z:L.μ(x∨(y∧z))≈(μx + μ(y ∧ z) + - μ(x∧(y∧z))).
 intros (R L x y z);
 lapply (modular_mjp ?? x (y ∧ z)) as H1;
 apply (Eq≈ (μ(x∧(y∧z))+ μ(x∨(y∧z)) +-μ(x∧(y∧z)))); [2: apply feq_plusr; apply (eq_trans ???? (plus_comm ???)); apply H1] clear H1;
@@ -110,7 +110,7 @@ apply (Eq≈ (0+ μ(x∨y∧z)) ? (opp_inverse ??));
 apply eq_sym; apply zero_neutral;
 qed.
 
-lemma step1_3_57': ∀R.∀L:wlattice R.∀x,y,z:L.
+lemma step1_3_57': ∀R.∀L:vlattice R.∀x,y,z:L.
   μ(x ∨ (y ∧ z)) ≈ (μ x) + (μ y) + μ z + -μ (y ∨ z) + -μ (z ∧ (x ∧ y)).
 intros (R L x y z);
 apply (Eq≈ ? (modularjm ?? x y z));
@@ -125,7 +125,7 @@ apply feq_plusr; apply (Eq≈ ? (plus_assoc ????));
 apply feq_plusr; apply plus_assoc;
 qed.
 
-lemma step1_3_57: ∀R.∀L:wlattice R.∀x,y,z:L.
+lemma step1_3_57: ∀R.∀L:vlattice R.∀x,y,z:L.
   μ(x ∧ (y ∨ z)) ≈ (μ x) + (μ y) + μ z + -μ (y ∧ z) + -μ (z ∨ (x ∨ y)).
 intros (R L x y z);
 apply (Eq≈ ? (modularmj ?? x y z));
@@ -142,7 +142,7 @@ qed.
 
 (* LEMMA 3.57 *) 
 
-lemma join_meet_le_join: ∀R.∀L:wlattice R.∀x,y,z:L.μ (x ∨ (y ∧ z)) ≤ μ (x ∨ z). 
+lemma join_meet_le_join: ∀R.∀L:vlattice R.∀x,y,z:L.μ (x ∨ (y ∧ z)) ≤ μ (x ∨ z). 
 intros (R L x y z);
 apply (le_rewl ??? ? (eq_sym ??? (step1_3_57' ?????)));
 apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+ -μ(z∧x∧y))); [
@@ -192,7 +192,7 @@ apply (le_rewr ??? (μ(z∨x) + (-μ(y∨z) + μ(y∨z)))); [ apply feq_plusr; a
 repeat apply fle_plusl; apply join_meet_le;
 qed.
 
-lemma meet_le_meet_join: ∀R.∀L:wlattice R.∀x,y,z:L.μ (x ∧ z) ≤ μ (x ∧ (y ∨ z)). 
+lemma meet_le_meet_join: ∀R.∀L:vlattice R.∀x,y,z:L.μ (x ∧ z) ≤ μ (x ∧ (y ∨ z)). 
 intros (R L x y z);
 apply (le_rewr ??? ? (eq_sym ??? (step1_3_57 ?????)));
 apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+ -μ(z∨x∨y))); [
-- 
2.39.2