From ada8695ba51b2ecbd4a955f990e8d06f038aac6b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 19 Jun 2008 16:32:36 +0000 Subject: [PATCH] - notation fixed according to the new stricter semantics - generalize no longer required before case --- .../matita/contribs/dama/dama/cprop_connectives.ma | 4 ++-- .../dama/dama/models/nat_dedekind_sigma_complete.ma | 9 +++------ .../matita/contribs/dama/dama/models/nat_lebesgue.ma | 2 +- .../matita/contribs/dama/dama/ordered_uniform.ma | 4 ++-- .../software/matita/contribs/dama/dama/property_sigma.ma | 5 ++--- helm/software/matita/contribs/dama/dama/sequence.ma | 9 +++------ helm/software/matita/contribs/dama/dama/uniform.ma | 8 +++----- 7 files changed, 16 insertions(+), 25 deletions(-) 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). -- 2.39.2