- "grammar" component updated to new syntax ...

- notation for lthin
- bugfix in replace.sh

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma
index 0414499a59de0aee49a610b8bf83394a6388d970..c5e93ce16be674a846375d4d484870317f91ecdc 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma
@@ -38,7 +38,7 @@ qed.
 lemma tw_shift: ∀L,T. #[L, T] ≤ #[L @ T].
 #L elim L //
 #K #I #V #IHL #T
-@transitive_le [3: @IHL |2: /2/ | skip ]
+@transitive_le [3: @IHL |2: /2 width=1/ | skip ]
 qed.
 
 (* Basic_1: removed theorems 6:

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma
index 56c5a2b8c1ef9738a638a05b144a31e1b8076fb7..48ff1ec9acf8448c1f48773a571343c298f1e628 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma
@@ -13,10 +13,10 @@
 (**************************************************************************)
 
 (* THE FORMAL SYSTEM λδ - MATITA SOURCE FILES
- * Specification started: 2011 April 17
  * Confluence of context-sensitive parallel reduction closed: 2011 September 21
  * Confluence of context-free parallel reduction closed: 2011 September 6
- * - Patience on me so that I gain peace and perfection! -
+ * Specification started: 2011 April 17
+ * - Patience on me to gain peace and perfection! -
  * [ suggested invocation to start formal specifications with ]
  *)
 

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma
index cf90a6134590c41c8ffc50b511cf5123e4fa3e49..1f750064ebd139eb0c9d472ef31dbda24c79e99e 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma
@@ -27,7 +27,9 @@ inductive lsubs: nat → nat → relation lenv ≝
               lsubs d e L1 L2 → lsubs (d + 1) e (L1. 𝕓{I1} V1) (L2. 𝕓{I2} V2)
 .
 
-interpretation "local environment refinement (substitution)" 'SubEq L1 d e L2 = (lsubs d e L1 L2).
+interpretation
+  "local environment refinement (substitution)"
+  'SubEq L1 d e L2 = (lsubs d e L1 L2).
 
 definition lsubs_conf: ∀S. (lenv → relation S) → Prop ≝ λS,R.
                        ∀L1,s1,s2. R L1 s1 s2 →
@@ -36,29 +38,29 @@ definition lsubs_conf: ∀S. (lenv → relation S) → Prop ≝ λS,R.
 (* Basic properties *********************************************************)
 
 lemma TC_lsubs_conf: ∀S,R. lsubs_conf S R → lsubs_conf S (λL. (TC … (R L))).
-#S #R #HR #L1 #s1 #s2 #H elim H -H s2
+#S #R #HR #L1 #s1 #s2 #H elim H -s2
 [ /3 width=5/
 | #s #s2 #_ #Hs2 #IHs1 #L2 #d #e #HL12
-  lapply (HR … Hs2 … HL12) -HR Hs2 HL12 /3/
+  lapply (HR … Hs2 … HL12) -HR -Hs2 -HL12 /3 width=3/
 ]
 qed.
 
 lemma lsubs_bind_eq: ∀L1,L2,e. L1 [0, e] ≼ L2 → ∀I,V.
                      L1. 𝕓{I} V [0, e + 1] ≼ L2.𝕓{I} V.
-#L1 #L2 #e #HL12 #I #V elim I -I /2/
+#L1 #L2 #e #HL12 #I #V elim I -I /2 width=1/
 qed.
 
 lemma lsubs_refl: ∀d,e,L. L [d, e] ≼ L.
 #d elim d -d
-[ #e elim e -e // #e #IHe #L elim L -L /2/
-| #d #IHd #e #L elim L -L /2/
+[ #e elim e -e // #e #IHe #L elim L -L // /2 width=1/
+| #d #IHd #e #L elim L -L // /2 width=1/
 ]
 qed.
 
 lemma lsubs_skip_lt: ∀L1,L2,d,e. L1 [d - 1, e] ≼ L2 → 0 < d →
                      ∀I1,I2,V1,V2. L1. 𝕓{I1} V1 [d, e] ≼ L2. 𝕓{I2} V2.
 
-#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) /2/
+#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) // /2 width=1/
 qed.
 
 (* Basic inversion lemmas ***************************************************)
@@ -67,14 +69,14 @@ qed.
 
 fact lsubs_fwd_length_full1_aux: ∀L1,L2,d,e. L1 [d, e] ≼ L2 →
                                  d = 0 → e = |L1| → |L1| ≤ |L2|.
-#L1 #L2 #d #e #H elim H -H L1 L2 d e; normalize
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize
 [ //
-| /2/
-| /3/
-| /3/
+| /2 width=1/
+| /3 width=1/
+| /3 width=1/
 | #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ #H
   elim (plus_S_eq_O_false … H)
-]   
+]
 qed.
 
 lemma lsubs_fwd_length_full1: ∀L1,L2. L1 [0, |L1|] ≼ L2 → |L1| ≤ |L2|.
@@ -82,14 +84,14 @@ lemma lsubs_fwd_length_full1: ∀L1,L2. L1 [0, |L1|] ≼ L2 → |L1| ≤ |L2|.
 
 fact lsubs_fwd_length_full2_aux: ∀L1,L2,d,e. L1 [d, e] ≼ L2 →
                                  d = 0 → e = |L2| → |L2| ≤ |L1|.
-#L1 #L2 #d #e #H elim H -H L1 L2 d e; normalize
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize
 [ //
-| /2/
-| /3/
-| /3/
+| /2 width=1/
+| /3 width=1/
+| /3 width=1/
 | #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ #H
   elim (plus_S_eq_O_false … H)
-]   
+]
 qed.
 
 lemma lsubs_fwd_length_full2: ∀L1,L2. L1 [0, |L2|] ≼ L2 → |L2| ≤ |L1|.

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma
index 376061b70bb52cef59e3b11c08cb920ab6ba42ff..f3f307cd62cdd9c41f09c789882a50c9a8f80104 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma
@@ -42,9 +42,8 @@ lemma discr_tpair_xy_x: ∀I,T,V. 𝕔{I} V. T = V → False.
 #I #T #V elim V -V
 [ #J #H destruct
 | #J #W #U #IHW #_ #H destruct
-(*
- (generalize in match e1) -e1 >e0 normalize
-*) -I /2/ (**) (* destruct: one quality is not simplified, the destucted equality is not erased *)
+  -H >e0 in e1; normalize (**) (* destruct: one quality is not simplified, the destucted equality is not erased *)
+  /2 width=1/ 
 ]
 qed-.
 
@@ -52,7 +51,9 @@ qed-.
 lemma discr_tpair_xy_y: ∀I,V,T. 𝕔{I} V. T = T → False.
 #I #V #T elim T -T
 [ #J #H destruct
-| #J #W #U #_ #IHU #H destruct -I V /2/ (**) (* destruct: the destucted equality is not erased *)
+| #J #W #U #_ #IHU #H destruct
+  -H (**) (* destruct: the destucted equality is not erased *)
+  /2 width=1/
 ]
 qed-.
 

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_weight.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_weight.ma
index 8eaa24acad195dbe26bb4c8eb0437c5f72ece6c1..1cf414b38b1533e32daf42574d7b229bcf0150f8 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_weight.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_weight.ma
@@ -27,7 +27,7 @@ interpretation "weight (term)" 'Weight T = (tw T).
 
 (* Basic_1: was: tweight_lt *)
 lemma tw_pos: ∀T. 1 ≤ #[T].
-#T elim T -T /2/ 
+#T elim T -T //
 qed.
 
 (* Basic eliminators ********************************************************)
@@ -38,6 +38,6 @@ axiom tw_wf_ind: ∀R:predicate term.
 
 (* Basic_1: removed theorems 11:
             wadd_le wadd_lt wadd_O weight_le weight_eq weight_add_O
-           weight_add_S tlt_trans tlt_head_sx tlt_head_dx tlt_wf_ind
+                 weight_add_S tlt_trans tlt_head_sx tlt_head_dx tlt_wf_ind
             removed local theorems 1: q_ind
 *)

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma
index 4bb9748d2aa7f62c379c4cce0af57aabaaedc8dc..aaade3b54324f39304ce3343af8cbddd5cd93e2d 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma
@@ -28,32 +28,32 @@ interpretation "homomorphic (term)" 'napart T1 T2 = (thom T1 T2).
 (* Basic properties *********************************************************)
 
 lemma thom_sym: ∀T1,T2. T1 ≈ T2 → T2 ≈ T1.
-#T1 #T2 #H elim H -H T1 T2 /2/
+#T1 #T2 #H elim H -T1 -T2 /2 width=1/
 qed.
 
 lemma thom_refl2: ∀T1,T2. T1 ≈ T2 → T2 ≈ T2.
-#T1 #T2 #H elim H -H T1 T2 /2/
+#T1 #T2 #H elim H -T1 -T2 // /2 width=1/
 qed.
 
 lemma thom_refl1: ∀T1,T2. T1 ≈ T2 → T1 ≈ T1.
-/3/ qed.
+/3 width=2/ qed.
 
 lemma simple_thom_repl_dx: ∀T1,T2. T1 ≈ T2 → 𝕊[T1] → 𝕊[T2].
-#T1 #T2 #H elim H -H T1 T2 //
+#T1 #T2 #H elim H -T1 -T2 //
 #V1 #V2 #T1 #T2 #H
 elim (simple_inv_bind … H)
 qed. (**) (* remove from index *)
 
 lemma simple_thom_repl_sn: ∀T1,T2. T1 ≈ T2 → 𝕊[T2] → 𝕊[T1].
-/3/ qed-.
+/3 width=3/ qed-.
 
 (* Basic inversion lemmas ***************************************************)
 
 fact thom_inv_bind1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = 𝕓{I}W1.U1 →
                          ∃∃W2,U2. I = Abst & T2 = 𝕔{Abst} W2. U2.
-#T1 #T2 * -T1 T2
+#T1 #T2 * -T1 -T2
 [ #J #I #W1 #U1 #H destruct
-| #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct -V1 T1 /2/
+| #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct /2 width=3/
 | #V1 #V2 #T1 #T2 #H_ #_ #_ #I #W1 #U1 #H destruct
 ]
 qed.
@@ -65,17 +65,17 @@ lemma thom_inv_bind1: ∀I,W1,U1,T2. 𝕓{I}W1.U1 ≈ T2 →
 fact thom_inv_flat1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = 𝕗{I}W1.U1 →
                          ∃∃W2,U2. U1 ≈ U2 & 𝕊[U1] & 𝕊[U2] &
                                   I = Appl & T2 = 𝕔{Appl} W2. U2.
-#T1 #T2 * -T1 T2
+#T1 #T2 * -T1 -T2
 [ #J #I #W1 #U1 #H destruct
 | #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct
-| #V1 #V2 #T1 #T2 #HT12 #HT1 #HT2 #I #W1 #U1 #H destruct -V1 T1 /2 width=5/
+| #V1 #V2 #T1 #T2 #HT12 #HT1 #HT2 #I #W1 #U1 #H destruct /2 width=5/
 ]
 qed.
 
 lemma thom_inv_flat1: ∀I,W1,U1,T2. 𝕗{I}W1.U1 ≈ T2 →
                       ∃∃W2,U2. U1 ≈ U2 & 𝕊[U1] & 𝕊[U2] &
                                I = Appl & T2 = 𝕔{Appl} W2. U2.
-/2/ qed-.
+/2 width=4/ qed-.
 
 (* Basic_1: removed theorems 7:
             iso_gen_sort iso_gen_lref iso_gen_head iso_refl iso_trans

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma
index 5fcf588334ad6043c19303cb5a31dea641864b24..dcbbbffed309ec7ffc8ffa53fa94af025651045f 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma
@@ -100,6 +100,10 @@ notation "hvbox( L ⊢ break term 90 T1 break [ d , break e ] ≫* break T2 )"
    non associative with precedence 45
    for @{ 'PSubstStar $L $T1 $d $e $T2 }.
 
+notation "hvbox( T1 break [ d , break e ] ≡ break T2 )"
+   non associative with precedence 45
+   for @{ 'TSubst $T1 $d $e $T2 }.
+
 notation "hvbox( L ⊢ break term 90 T1 break [ d , break e ] ≡ break T2 )"
    non associative with precedence 45
    for @{ 'TSubst $L $T1 $d $e $T2 }.

diff --git a/matita/matita/contribs/lambda_delta/replace.sh b/matita/matita/contribs/lambda_delta/replace.sh
index 33bf0e3a1b73300404f223287fd7ca45978ca54e..5e281b251228abd56e37bd8cb6125acede3902c4 100644 (file)
--- a/matita/matita/contribs/lambda_delta/replace.sh
+++ b/matita/matita/contribs/lambda_delta/replace.sh
@@ -1,8 +1,10 @@
 #!/bin/sh
 for MA in `find -name "*.ma"`; do
-   echo ${MA}; sed "s/$1/$2/g" ${MA} > ${MA}.new
+   echo ${MA}; sed "s!$1!$2!g" ${MA} > ${MA}.new
    if diff ${MA} ${MA}.new > /dev/null; 
-      then rm -f ${MA}.new; else mv -f ${MA}.new ${MA}; fi
+      then rm -f ${MA}.new; 
+      else mv -f ${MA} ${MA}.old; mv -f ${MA}.new ${MA};
+   fi
 done
 
 unset MA