From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 19 Jun 2008 16:32:36 +0000 (+0000)
Subject: - notation fixed according to the new stricter semantics
X-Git-Tag: make_still_working~5012
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ada8695ba51b2ecbd4a955f990e8d06f038aac6b;p=helm.git

- notation fixed according to the new stricter semantics
- generalize no longer required before case
---

diff --git a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
index 9e0e4b5fb..aabf6e79e 100644
--- a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
+++ b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
@@ -28,14 +28,14 @@ interpretation "constructive and" 'and x y = (And x y).
 inductive And3 (A,B,C:CProp) : CProp ≝
  | Conj3 : A → B → C → And3 A B C.
 
-notation < "a ∧ b ∧ c" left associative with precedence 35 for @{'and3 $a $b $c}.
+notation < "a ∧ b ∧ c" with precedence 35 for @{'and3 $a $b $c}.
  
 interpretation "constructive ternary and" 'and3 x y z = (Conj3 x y z).
 
 inductive And4 (A,B,C,D:CProp) : CProp ≝
  | Conj4 : A → B → C → D → And4 A B C D.
 
-notation < "a ∧ b ∧ c ∧ d" left associative with precedence 35 for @{'and4 $a $b $c $d}.
+notation < "a ∧ b ∧ c ∧ d" with precedence 35 for @{'and4 $a $b $c $d}.
  
 interpretation "constructive quaternary and" 'and4 x y z t = (Conj4 x y z t).
 
diff --git a/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma b/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma
index 04b861d41..0908b6f70 100644
--- a/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma
+++ b/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma
@@ -52,11 +52,8 @@ letin m ≝ (hide ? (
    ∀i:nat.∃j:nat.spec i j));unfold spec in aux ⊢ %;
 [1: apply (H2 pred nP);
 |4: unfold X in H2; clear H4 n aux spec H3 H1 H X;
-    generalize in match H2;
-    generalize in match Hs;
-    generalize in match a;
-    clear H2 Hs a; cases u; intros (a Hs H);
-    [1: left; split; [apply le_n] 
+    cases u in H2 Hs a ⊢ %; intros (a Hs H);
+    [1: left; split; [apply le_n]
         generalize in match H;
         generalize in match Hs;
         rewrite > (?:s = O); 
@@ -68,7 +65,7 @@ letin m ≝ (hide ? (
         apply (trans_le ??? (os_le_to_nat_le ?? H1));
         apply le_plus_n_r;] 
 |2,3: clear H6;
-    generalize in match H5; clear H5; cases (aux n1); intros;
+    cases (aux n1) in H5 ⊢ %; intros;
     change in match (a 〈w,H5〉) in H6 ⊢ % with (a w);
     cases H5; clear H5; cases H7; clear H7;
     [1: left; split; [ apply (le_S ?? H5); | assumption]
diff --git a/helm/software/matita/contribs/dama/dama/models/nat_lebesgue.ma b/helm/software/matita/contribs/dama/dama/models/nat_lebesgue.ma
index 228392dda..7e059c03d 100644
--- a/helm/software/matita/contribs/dama/dama/models/nat_lebesgue.ma
+++ b/helm/software/matita/contribs/dama/dama/models/nat_lebesgue.ma
@@ -17,7 +17,7 @@ include "models/nat_order_continuous.ma".
 
 alias symbol "pair" = "dependent pair".
 theorem nat_lebesgue_oc:
-   ∀a:sequence ℕ.∀l,u:nat_ordered_uniform_space.∀H:∀i:nat.a i ∈ [l,u]. 
+   ∀a:sequence ℕ.∀l,u:ℕ.∀H:∀i:nat.a i ∈ [l,u]. 
      ∀x:ℕ.a order_converges x → 
       x ∈ [l,u] ∧ 
       ∀h:x ∈ [l,u].
diff --git a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
index 8aacb5b59..326681b26 100644
--- a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
@@ -96,7 +96,7 @@ lemma bs_of_ss:
  ∀O:ordered_set.∀u,v:O.{[u,v]} square → (bishop_set_of_ordered_set O) square ≝ 
   λO:ordered_set.λu,v:O.λb:{[u,v]} square.〈fst(fst b),fst(snd b)〉.
 
-notation < "x \sub \neq" left associative with precedence 91 for @{'bsss $x}.
+notation < "x \sub \neq" with precedence 91 for @{'bsss $x}.
 interpretation "bs_of_ss" 'bsss x = (bs_of_ss _ _ _ x).
 
 alias symbol "square" (instance 7) = "ordered set square".
@@ -108,7 +108,7 @@ lemma ss_of_bs:
  λO:ordered_set.λu,v:O.
   λb:(O:bishop_set) square.λH1,H2.〈〈fst b,H1〉,〈snd b,H2〉〉.
 
-notation < "x \sub \nleq" left associative with precedence 91 for @{'ssbs $x}.
+notation < "x \sub \nleq" with precedence 91 for @{'ssbs $x}.
 interpretation "ss_of_bs" 'ssbs x = (ss_of_bs _ _ _ x _ _).
 
 lemma segment_ordered_uniform_space: 
diff --git a/helm/software/matita/contribs/dama/dama/property_sigma.ma b/helm/software/matita/contribs/dama/dama/property_sigma.ma
index ba90bb0ab..672099281 100644
--- a/helm/software/matita/contribs/dama/dama/property_sigma.ma
+++ b/helm/software/matita/contribs/dama/dama/property_sigma.ma
@@ -77,9 +77,8 @@ letin m ≝ (hide ? (let rec aux (i:nat) : nat ≝
       intros; lapply (H5 i j) as H14;
         [2: apply (max_le_l ??? H6);|3:apply (max_le_l ??? H7);]
       cases (le_to_or_lt_eq ?? H10); [2: destruct H11; destruct H4; assumption]
-      generalize in match H6; generalize in match H7;
-      cases (aux n1); simplify in ⊢ (? (? ? %) ?→? (? ? %) ?→?); intros;
-      apply H12; [3: apply le_S_S_to_le; assumption]
+      cases (aux n1) in H6 H7 ⊢ %; simplify in ⊢ (? (? ? %) ?→? (? ? %) ?→?); intros;
+      apply H6; [3: apply le_S_S_to_le; assumption]
       apply lt_to_le; apply (max_le_r w1); assumption;
   |4: intros; clear H6; rewrite > H4 in H5; 
       rewrite < (le_n_O_to_eq ? H11); apply H5; assumption;] 
diff --git a/helm/software/matita/contribs/dama/dama/sequence.ma b/helm/software/matita/contribs/dama/dama/sequence.ma
index c64315481..39c40194b 100644
--- a/helm/software/matita/contribs/dama/dama/sequence.ma
+++ b/helm/software/matita/contribs/dama/dama/sequence.ma
@@ -22,16 +22,13 @@ definition fun_of_seq: ∀O:Type.sequence O → nat → O ≝
 
 coercion cic:/matita/dama/sequence/fun_of_seq.con 1.
 
-notation < "hvbox((\lfloor p \rfloor) \sub ident i)"
-  left associative with precedence 70
+notation < "hvbox((\lfloor p \rfloor) \sub ident i)" with precedence 70
 for @{ 'sequence (\lambda ${ident i} : $t . $p)}.
 
-notation > "hvbox((\lfloor p \rfloor) \sub ident i)"
-  left associative with precedence 70
+notation > "hvbox((\lfloor p \rfloor) \sub ident i)" with precedence 70
 for @{ 'sequence (\lambda ${ident i} . $p)}.
 
-notation > "hvbox(\lfloor ident i, p \rfloor)"
-  left associative with precedence 70
+notation > "hvbox(\lfloor ident i, p \rfloor)" with precedence 70
 for @{ 'sequence (\lambda ${ident i} . $p)}.
   
 notation "a \sub i" left associative with precedence 70 
diff --git a/helm/software/matita/contribs/dama/dama/uniform.ma b/helm/software/matita/contribs/dama/dama/uniform.ma
index faba6d83a..ed9e6fe5d 100644
--- a/helm/software/matita/contribs/dama/dama/uniform.ma
+++ b/helm/software/matita/contribs/dama/dama/uniform.ma
@@ -35,12 +35,10 @@ definition invert_bs_relation ≝
   λC:bishop_set.λU:C square → Prop.
     λx:C square. U 〈snd x,fst x〉.
     
-notation < "s \sup (-1)"  left associative with precedence 70
-  for @{ 'invert $s }.
-notation < "s \sup (-1) x"  left associative with precedence 70
+notation < "s \sup (-1)"  with precedence 70 for @{ 'invert $s }.
+notation < "s \sup (-1) x"  with precedence 70
   for @{ 'invert_appl $s $x}. 
-notation > "'inv'" right associative with precedence 70
-  for @{ 'invert_symbol  }.
+notation > "'inv'" with precedence 70 for @{ 'invert_symbol  }.
 interpretation "relation invertion" 'invert a = (invert_bs_relation _ a).
 interpretation "relation invertion" 'invert_symbol = (invert_bs_relation _).
 interpretation "relation invertion" 'invert_appl a x = (invert_bs_relation _ a x).