update in ground_2, static_2, basic_2, apps_2, alpha_1

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / i_dynamic / ntas.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas.ma b/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas.ma
index 3c65cbd7c6e204f3c1062811ba6e2531039331b2..7f74c5f063971899044f2ae726f2fef2c4f3002c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas.ma
@@ -12,27 +12,54 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/notation/relations/colon_7.ma".
-include "basic_2/notation/relations/colon_6.ma".
-include "basic_2/notation/relations/colonstar_6.ma".
+include "basic_2/notation/relations/colonstar_7.ma".
 include "basic_2/dynamic/cnv.ma".
 
 (* ITERATED NATIVE TYPE ASSIGNMENT FOR TERMS ********************************)
 
-definition ntas (a) (h) (n) (G) (L): relation term ≝ λT,U.
-           â\88\83â\88\83U0. â¦\83G,Lâ¦\84 â\8a¢ U ![a,h] & â¦\83G,Lâ¦\84 â\8a¢ T ![a,h] & â¦\83G,Lâ¦\84 â\8a¢ U â\9e¡*[h] U0 & â¦\83G, Lâ¦\84 ⊢ T ➡*[n,h] U0.
+definition ntas (h) (a) (n) (G) (L): relation term ≝ λT,U.
+           â\88\83â\88\83U0. â\9dªG,Lâ\9d« â\8a¢ U ![h,a] & â\9dªG,Lâ\9d« â\8a¢ T ![h,a] & â\9dªG,Lâ\9d« â\8a¢ U â\9e¡*[h] U0 & â\9dªG,Lâ\9d« ⊢ T ➡*[n,h] U0.
 
 interpretation "iterated native type assignment (term)"
-   'Colon a h n G L T U = (ntas a h n G L T U).
-
-interpretation "restricted iterated native type assignment (term)"
-   'Colon h n G L T U = (ntas true h n G L T U).
-
-interpretation "extended iterated native type assignment (term)"
-   'ColonStar h n G L T U = (ntas false h n G L T U).
+   'ColonStar h a n G L T U = (ntas h a n G L T U).
 
 (* Basic properties *********************************************************)
 
-lemma ntas_refl (a) (h) (G) (L):
-      ∀T. ⦃G,L⦄ ⊢ T ![a,h] → ⦃G,L⦄ ⊢ T :[a,h,0] T.
+lemma ntas_intro (h) (a) (n) (G) (L):
+      ∀U. ❪G,L❫ ⊢ U ![h,a] → ∀T. ❪G,L❫ ⊢ T ![h,a] →
+      ∀U0. ❪G,L❫ ⊢ U ➡*[h] U0 → ❪G,L❫ ⊢ T ➡*[n,h] U0 → ❪G,L❫ ⊢ T :*[h,a,n] U.
 /2 width=3 by ex4_intro/ qed.
+
+lemma ntas_refl (h) (a) (G) (L):
+      ∀T. ❪G,L❫ ⊢ T ![h,a] → ❪G,L❫ ⊢ T :*[h,a,0] T.
+/2 width=3 by ntas_intro/ qed.
+
+lemma ntas_sort (h) (a) (n) (G) (L):
+      ∀s. ❪G,L❫ ⊢ ⋆s :*[h,a,n] ⋆((next h)^n s).
+#h #a #n #G #L #s
+/2 width=3 by ntas_intro, cnv_sort, cpms_sort/
+qed.
+
+lemma ntas_bind_cnv (h) (a) (n) (G) (K):
+      ∀V. ❪G,K❫ ⊢ V ![h,a] →
+      ∀I,T,U. ❪G,K.ⓑ[I]V❫ ⊢ T :*[h,a,n] U →
+      ∀p. ❪G,K❫ ⊢ ⓑ[p,I]V.T :*[h,a,n] ⓑ[p,I]V.U.
+#h #a #n #G #K #V #HV #I #T #U
+* #X #HU #HT #HUX #HTX #p
+/3 width=5 by ntas_intro, cnv_bind, cpms_bind_dx/
+qed.
+
+(* Basic_forward lemmas *****************************************************)
+
+lemma ntas_fwd_cnv_sn (h) (a) (n) (G) (L):
+      ∀T,U. ❪G,L❫ ⊢ T :*[h,a,n] U → ❪G,L❫ ⊢ T ![h,a].
+#h #a #n #G #L #T #U
+* #X #_ #HT #_ #_ //
+qed-.
+
+(* Note: this is ntas_fwd_correct_cnv *)
+lemma ntas_fwd_cnv_dx (h) (a) (n) (G) (L):
+      ∀T,U. ❪G,L❫ ⊢ T :*[h,a,n] U → ❪G,L❫ ⊢ U ![h,a].
+#h #a #n #G #L #T #U
+* #X #HU #_ #_ #_ //
+qed-.