1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "basic_2/notation/relations/colon_6.ma".
16 include "basic_2/dynamic/cnv.ma".
18 (* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************)
20 definition nta (h) (a): relation4 genv lenv term term ≝
21 λG,L,T,U. ❨G,L❩ ⊢ ⓝU.T ![h,a].
23 interpretation "native type assignment (term)"
24 'Colon h a G L T U = (nta h a G L T U).
26 (* Basic properties *********************************************************)
28 (* Basic_1: was by definition: ty3_sort *)
29 (* Basic_2A1: was by definition: nta_sort ntaa_sort *)
30 lemma nta_sort (h) (a) (G) (L): ∀s. ❨G,L❩ ⊢ ⋆s :[h,a] ⋆(⫯[h]s).
31 #h #a #G #L #s /2 width=3 by cnv_sort, cnv_cast, cpms_sort/
34 lemma nta_bind_cnv (h) (a) (G) (K):
35 ∀V. ❨G,K❩ ⊢ V ![h,a] →
36 ∀I,T,U. ❨G,K.ⓑ[I]V❩ ⊢ T :[h,a] U →
37 ∀p. ❨G,K❩ ⊢ ⓑ[p,I]V.T :[h,a] ⓑ[p,I]V.U.
38 #h #a #G #K #V #HV #I #T #U #H #p
39 elim (cnv_inv_cast … H) -H #X #HU #HT #HUX #HTX
40 /3 width=5 by cnv_bind, cnv_cast, cpms_bind_dx/
43 (* Basic_2A1: was by definition: nta_cast *)
44 lemma nta_cast (h) (a) (G) (L):
45 ∀T,U. ❨G,L❩ ⊢ T :[h,a] U → ❨G,L❩ ⊢ ⓝU.T :[h,a] U.
47 elim (cnv_inv_cast … H) #X #HU #HT #HUX #HTX
48 /3 width=3 by cnv_cast, cpms_eps/
51 (* Basic_1: was by definition: ty3_cast *)
52 lemma nta_cast_old (h) (a) (G) (L):
53 ∀T0,T1. ❨G,L❩ ⊢ T0 :[h,a] T1 →
54 ∀T2. ❨G,L❩ ⊢ T1 :[h,a] T2 → ❨G,L❩ ⊢ ⓝT1.T0 :[h,a] ⓝT2.T1.
55 #h #a #G #L #T0 #T1 #H1 #T2 #H2
56 elim (cnv_inv_cast … H1) #X1 #_ #_ #HTX1 #HTX01
57 elim (cnv_inv_cast … H2) #X2 #_ #_ #HTX2 #HTX12
58 /3 width=3 by cnv_cast, cpms_eps/
61 (* Basic inversion lemmas ***************************************************)
63 lemma nta_inv_gref_sn (h) (a) (G) (L):
64 ∀X2,l. ❨G,L❩ ⊢ §l :[h,a] X2 → ⊥.
66 elim (cnv_inv_cast … H) -H #X #_ #H #_ #_
67 elim (cnv_inv_gref … H)
70 (* Basic_forward lemmas *****************************************************)
72 lemma nta_fwd_cnv_sn (h) (a) (G) (L):
73 ∀T,U. ❨G,L❩ ⊢ T :[h,a] U → ❨G,L❩ ⊢ T ![h,a].
75 elim (cnv_inv_cast … H) -H #X #_ #HT #_ #_ //
78 (* Note: this is nta_fwd_correct_cnv *)
79 lemma nta_fwd_cnv_dx (h) (a) (G) (L):
80 ∀T,U. ❨G,L❩ ⊢ T :[h,a] U → ❨G,L❩ ⊢ U ![h,a].
82 elim (cnv_inv_cast … H) -H #X #HU #_ #_ #_ //
85 (* Basic_1: removed theorems 4:
86 ty3_getl_subst0 ty3_fsubst0 ty3_csubst0 ty3_subst0
88 (* Basic_2A1: removed theorems 2: